Updated.

author: David Aspinall <da@inf.ed.ac.uk> 2004-08-25 21:05:53 +0000
committer: David Aspinall <da@inf.ed.ac.uk> 2004-08-25 21:05:53 +0000
commit: 882e453a0921295e95201a57ed55517ad66e9342 (patch)
tree: e9678e5fe096024b8be35d0830a699c4e3ced7b7 /TAGS
parent: c0ba98b45ed0c886e5bbfbc76c79aeeaf388fd64 (diff)
1 files changed, 1257 insertions, 1156 deletions
diff --git a/TAGS b/TAGS
index 83d96951..4a0eebdf 100644
--- a/TAGS
+++ b/TAGS
@@ -11,97 +11,97 @@ coq/coq-abbrev-V7.el,49
 (defpgdefault menu-entriesmenu-entries119,5878
 
 coq/coq.el,5468
-(defcustom coq-prog-name coq-prog-name13,355
-(defcustom coq-compile-file-command coq-compile-file-command18,464
-(defcustom coq-default-undo-limit coq-default-undo-limit28,833
-(defconst coq-shell-init-cmd coq-shell-init-cmd33,961
-(defconst coq-shell-restart-cmd coq-shell-restart-cmd46,1384
-(defvar coq-shell-prompt-pattern coq-shell-prompt-pattern53,1642
-(defvar coq-shell-cd coq-shell-cd58,1850
-(defvar coq-shell-abort-goal-regexp coq-shell-abort-goal-regexp64,2051
-(defvar coq-shell-proof-completed-regexp coq-shell-proof-completed-regexp67,2177
-(defvar coq-goal-regexpcoq-goal-regexp70,2308
-(defun coq-library-directory coq-library-directory79,2497
-(defcustom coq-tags coq-tags86,2677
-(defconst coq-interrupt-regexp coq-interrupt-regexp91,2826
-(defcustom coq-www-home-page coq-www-home-page96,2946
-(defun coq-insert-section coq-insert-section112,3196
-(defconst module-kinds-table module-kinds-table121,3453
-(defconst modtype-kinds-tablemodtype-kinds-table125,3589
-(defun coq-insert-module coq-insert-module129,3718
-(defvar coq-outline-regexpcoq-outline-regexp150,4475
-(defvar coq-outline-heading-end-regexp coq-outline-heading-end-regexp155,4884
-(defvar coq-shell-outline-regexp coq-shell-outline-regexp157,4943
-(defvar coq-shell-outline-heading-end-regexp coq-shell-outline-heading-end-regexp158,4993
-(defconst coq-kill-goal-command coq-kill-goal-command160,5056
-(defconst coq-forget-id-command coq-forget-id-command161,5099
-(defconst coq-back-n-command coq-back-n-command162,5145
-(defconst coq-state-changing-tactics-regexp coq-state-changing-tactics-regexp166,5207
-(defconst coq-state-preserving-tactics-regexp coq-state-preserving-tactics-regexp168,5304
-(defconst coq-tactics-regexpcoq-tactics-regexp170,5405
-(defconst coq-state-changing-commands-regexpcoq-state-changing-commands-regexp172,5471
-(defconst coq-state-preserving-commands-regexp coq-state-preserving-commands-regexp174,5578
-(defvar coq-retractable-instruct-regexp coq-retractable-instruct-regexp176,5690
-(defvar coq-non-retractable-instruct-regexpcoq-non-retractable-instruct-regexp178,5781
-(defvar coq-keywords-sectioncoq-keywords-section181,5880
-(defvar coq-section-regexp coq-section-regexp186,6025
-(defun coq-set-undo-limit coq-set-undo-limit219,7092
-(defconst coq-keywords-decl-defn-regexpcoq-keywords-decl-defn-regexp230,7435
-(defun coq-proof-mode-p coq-proof-mode-p238,7823
-(defun coq-is-comment-or-proverprocp coq-is-comment-or-proverprocp253,8329
-(defun coq-is-goalsave-p coq-is-goalsave-p255,8433
-(defun coq-is-module-equal-p coq-is-module-equal-p256,8508
-(defun coq-is-def-p coq-is-def-p259,8704
-(defun coq-is-decl-defn-p coq-is-decl-defn-p261,8812
-(defun coq-state-preserving-command-p coq-state-preserving-command-p266,8979
-(defun coq-state-preserving-tactic-p coq-state-preserving-tactic-p269,9113
-(defun coq-state-changing-command-p coq-state-changing-command-p272,9245
-(defun coq-section-or-module-start-p coq-section-or-module-start-p278,9553
-(defun coq-find-and-forget coq-find-and-forget286,9806
-(defvar coq-current-goal coq-current-goal378,14373
-(defun coq-goal-hyp coq-goal-hyp381,14438
-(defun coq-state-preserving-p coq-state-preserving-p394,14868
-(defun coq-SearchIsos coq-SearchIsos401,15185
-(defun coq-guess-or-ask-for-string coq-guess-or-ask-for-string415,15619
-(defun coq-Print coq-Print425,15913
-(defun coq-Check coq-Check434,16171
-(defun coq-Show coq-Show443,16413
-(defun coq-PrintHint coq-PrintHint464,17099
-(defun coq-end-Section coq-end-Section470,17242
-(defun coq-Compile coq-Compile488,17826
-(defun coq-intros coq-intros495,18006
-(define-key coq-keymap coq-keymap512,18683
-(define-key coq-keymap coq-keymap513,18734
-(define-key coq-keymap coq-keymap514,18793
-(define-key coq-keymap coq-keymap515,18851
-(define-key coq-keymap coq-keymap516,18907
-(define-key coq-keymap coq-keymap517,18962
-(define-key coq-keymap coq-keymap518,19012
-(define-key coq-keymap coq-keymap519,19062
-(define-key global-map global-map528,19571
-(defun coq-guess-command-line coq-guess-command-line587,21565
-(defun coq-pre-shell-start coq-pre-shell-start609,22371
-(defun coq-mode-config coq-mode-config620,22892
-(defun coq-shell-mode-config coq-shell-mode-config726,26637
-(defun coq-goals-mode-config coq-goals-mode-config765,28272
-(defun coq-response-config coq-response-config772,28503
-(defun coq-maybe-compile-buffer coq-maybe-compile-buffer792,29219
-(defun coq-ancestors-of coq-ancestors-of829,30753
-(defun coq-all-ancestors-of coq-all-ancestors-of852,31720
-(defconst coq-require-command-regexp coq-require-command-regexp864,32113
-(defun coq-process-require-command coq-process-require-command869,32322
-(defun coq-included-children coq-included-children874,32449
-(defun coq-process-file coq-process-file895,33288
-(defpacustom print-only-first-subgoal print-only-first-subgoal909,33786
-(defpacustom print-fully-explicit print-fully-explicit914,33937
-(defpacustom print-coercions print-coercions919,34084
-(defpacustom print-match-wildcards print-match-wildcards924,34227
-(defpacustom time-commands time-commands930,34409
-(defpacustom auto-compile-vos auto-compile-vos934,34520
-(defpacustom translate-to-v8 translate-to-v8956,35475
-(defun coq-preprocessing coq-preprocessing965,35691
-(defun coq-fake-constant-markup coq-fake-constant-markup980,36110
-(defun coq-create-span-menu coq-create-span-menu1002,36917
+(defcustom coq-prog-name coq-prog-name13,353
+(defcustom coq-compile-file-command coq-compile-file-command18,462
+(defcustom coq-default-undo-limit coq-default-undo-limit28,831
+(defconst coq-shell-init-cmd coq-shell-init-cmd33,959
+(defconst coq-shell-restart-cmd coq-shell-restart-cmd46,1382
+(defvar coq-shell-prompt-pattern coq-shell-prompt-pattern53,1640
+(defvar coq-shell-cd coq-shell-cd58,1848
+(defvar coq-shell-abort-goal-regexp coq-shell-abort-goal-regexp64,2049
+(defvar coq-shell-proof-completed-regexp coq-shell-proof-completed-regexp67,2175
+(defvar coq-goal-regexpcoq-goal-regexp70,2306
+(defun coq-library-directory coq-library-directory79,2495
+(defcustom coq-tags coq-tags86,2675
+(defconst coq-interrupt-regexp coq-interrupt-regexp91,2824
+(defcustom coq-www-home-page coq-www-home-page96,2944
+(defun coq-insert-section coq-insert-section112,3194
+(defconst module-kinds-table module-kinds-table121,3451
+(defconst modtype-kinds-tablemodtype-kinds-table125,3587
+(defun coq-insert-module coq-insert-module129,3716
+(defvar coq-outline-regexpcoq-outline-regexp150,4473
+(defvar coq-outline-heading-end-regexp coq-outline-heading-end-regexp155,4882
+(defvar coq-shell-outline-regexp coq-shell-outline-regexp157,4941
+(defvar coq-shell-outline-heading-end-regexp coq-shell-outline-heading-end-regexp158,4991
+(defconst coq-kill-goal-command coq-kill-goal-command160,5054
+(defconst coq-forget-id-command coq-forget-id-command161,5097
+(defconst coq-back-n-command coq-back-n-command162,5143
+(defconst coq-state-changing-tactics-regexp coq-state-changing-tactics-regexp166,5205
+(defconst coq-state-preserving-tactics-regexp coq-state-preserving-tactics-regexp168,5302
+(defconst coq-tactics-regexpcoq-tactics-regexp170,5403
+(defconst coq-state-changing-commands-regexpcoq-state-changing-commands-regexp172,5469
+(defconst coq-state-preserving-commands-regexp coq-state-preserving-commands-regexp174,5576
+(defvar coq-retractable-instruct-regexp coq-retractable-instruct-regexp176,5688
+(defvar coq-non-retractable-instruct-regexpcoq-non-retractable-instruct-regexp178,5779
+(defvar coq-keywords-sectioncoq-keywords-section181,5878
+(defvar coq-section-regexp coq-section-regexp186,6023
+(defun coq-set-undo-limit coq-set-undo-limit219,7090
+(defconst coq-keywords-decl-defn-regexpcoq-keywords-decl-defn-regexp230,7433
+(defun coq-proof-mode-p coq-proof-mode-p238,7821
+(defun coq-is-comment-or-proverprocp coq-is-comment-or-proverprocp253,8327
+(defun coq-is-goalsave-p coq-is-goalsave-p255,8431
+(defun coq-is-module-equal-p coq-is-module-equal-p256,8506
+(defun coq-is-def-p coq-is-def-p259,8702
+(defun coq-is-decl-defn-p coq-is-decl-defn-p261,8810
+(defun coq-state-preserving-command-p coq-state-preserving-command-p266,8977
+(defun coq-state-preserving-tactic-p coq-state-preserving-tactic-p269,9111
+(defun coq-state-changing-command-p coq-state-changing-command-p272,9243
+(defun coq-section-or-module-start-p coq-section-or-module-start-p278,9551
+(defun coq-find-and-forget coq-find-and-forget286,9804
+(defvar coq-current-goal coq-current-goal378,14371
+(defun coq-goal-hyp coq-goal-hyp381,14436
+(defun coq-state-preserving-p coq-state-preserving-p394,14866
+(defun coq-SearchIsos coq-SearchIsos401,15183
+(defun coq-guess-or-ask-for-string coq-guess-or-ask-for-string415,15617
+(defun coq-Print coq-Print425,15911
+(defun coq-Check coq-Check434,16169
+(defun coq-Show coq-Show443,16411
+(defun coq-PrintHint coq-PrintHint464,17097
+(defun coq-end-Section coq-end-Section470,17240
+(defun coq-Compile coq-Compile488,17824
+(defun coq-intros coq-intros495,18004
+(define-key coq-keymap coq-keymap512,18681
+(define-key coq-keymap coq-keymap513,18732
+(define-key coq-keymap coq-keymap514,18791
+(define-key coq-keymap coq-keymap515,18849
+(define-key coq-keymap coq-keymap516,18905
+(define-key coq-keymap coq-keymap517,18960
+(define-key coq-keymap coq-keymap518,19010
+(define-key coq-keymap coq-keymap519,19060
+(define-key global-map global-map528,19569
+(defun coq-guess-command-line coq-guess-command-line587,21563
+(defun coq-pre-shell-start coq-pre-shell-start609,22369
+(defun coq-mode-config coq-mode-config620,22890
+(defun coq-shell-mode-config coq-shell-mode-config727,26705
+(defun coq-goals-mode-config coq-goals-mode-config766,28340
+(defun coq-response-config coq-response-config773,28571
+(defun coq-maybe-compile-buffer coq-maybe-compile-buffer793,29287
+(defun coq-ancestors-of coq-ancestors-of830,30821
+(defun coq-all-ancestors-of coq-all-ancestors-of853,31788
+(defconst coq-require-command-regexp coq-require-command-regexp865,32181
+(defun coq-process-require-command coq-process-require-command870,32390
+(defun coq-included-children coq-included-children875,32517
+(defun coq-process-file coq-process-file896,33356
+(defpacustom print-only-first-subgoal print-only-first-subgoal910,33854
+(defpacustom print-fully-explicit print-fully-explicit915,34005
+(defpacustom print-coercions print-coercions920,34152
+(defpacustom print-match-wildcards print-match-wildcards925,34295
+(defpacustom time-commands time-commands931,34477
+(defpacustom auto-compile-vos auto-compile-vos935,34588
+(defpacustom translate-to-v8 translate-to-v8957,35543
+(defun coq-preprocessing coq-preprocessing966,35759
+(defun coq-fake-constant-markup coq-fake-constant-markup981,36178
+(defun coq-create-span-menu coq-create-span-menu1003,36985
 
 coq/coq-indent.el,1791
 (defconst coq-any-command-regexpcoq-any-command-regexp11,262
@@ -141,51 +141,51 @@ coq/coq-syntax.el,3214
 (defvar coq-version-is-V7 coq-version-is-V732,1119
 (defvar coq-version-is-V74 coq-version-is-V7440,1529
 (defvar coq-version-is-V8 coq-version-is-V849,1988
-(defvar coq-keywords-declcoq-keywords-decl124,4579
-(defvar coq-keywords-defncoq-keywords-defn139,4935
-(defun coq-count-match coq-count-match213,7291
-(defun coq-goal-command-p coq-goal-command-p225,7711
-(defvar coq-keywords-save-strictcoq-keywords-save-strict245,8295
-(defvar coq-keywords-savecoq-keywords-save253,8392
-(defun coq-save-command-p coq-save-command-p257,8468
-(defvar coq-keywords-kill-goal coq-keywords-kill-goal265,8747
-(defcustom coq-user-state-changing-commands coq-user-state-changing-commands271,8797
-(defcustom coq-user-state-preserving-commands coq-user-state-preserving-commands283,9194
-(defvar coq-keywords-state-preserving-commandscoq-keywords-state-preserving-commands296,9634
-(defvar coq-keywords-state-changing-misc-commandscoq-keywords-state-changing-misc-commands343,10745
-(defvar coq-keywords-state-changing-commandscoq-keywords-state-changing-commands417,12763
-(defvar coq-keywords-commandscoq-keywords-commands427,12960
-(defcustom coq-user-state-changing-tactics coq-user-state-changing-tactics433,13110
-(defvar coq-state-changing-tacticscoq-state-changing-tactics444,13536
-(defcustom coq-user-state-preserving-tactics coq-user-state-preserving-tactics645,16861
-(defvar coq-state-preserving-tacticscoq-state-preserving-tactics656,17275
-(defvar coq-tacticscoq-tactics660,17373
-(defvar coq-retractable-instructcoq-retractable-instruct663,17462
-(defvar coq-non-retractable-instructcoq-non-retractable-instruct666,17572
-(defvar coq-keywordscoq-keywords670,17694
-(defvar coq-tacticalscoq-tacticals675,17859
-(defvar coq-reserved-commoncoq-reserved-common697,18242
-(defvar coq-reserved-V8coq-reserved-V8713,18435
-(defvar coq-reserved-V7coq-reserved-V7724,18539
-(defvar coq-reserved coq-reserved729,18614
-(defvar coq-symbolscoq-symbols737,18770
-(defvar coq-error-regexp coq-error-regexp755,18974
-(defvar coq-id coq-id758,19190
-(defvar coq-ids coq-ids760,19216
-(defun coq-first-abstr-regexp coq-first-abstr-regexp762,19253
-(defun coq-next-abstr-regexp coq-next-abstr-regexp765,19341
-(defvar coq-font-lock-termscoq-font-lock-terms768,19419
-(defconst coq-save-command-regexp-strictcoq-save-command-regexp-strict783,20072
-(defconst coq-save-command-regexpcoq-save-command-regexp785,20185
-(defconst coq-save-with-hole-regexpcoq-save-with-hole-regexp787,20284
-(defconst coq-goal-command-regexpcoq-goal-command-regexp790,20422
-(defconst coq-goal-with-hole-regexpcoq-goal-with-hole-regexp792,20521
-(defconst coq-decl-with-hole-regexpcoq-decl-with-hole-regexp798,20810
-(defconst coq-defn-with-hole-regexpcoq-defn-with-hole-regexp801,20943
-(defvar coq-font-lock-keywords-1coq-font-lock-keywords-1804,21083
-(defvar coq-font-lock-keywords coq-font-lock-keywords825,22126
-(defun coq-init-syntax-table coq-init-syntax-table827,22184
-(defconst coq-generic-expressioncoq-generic-expression856,23082
+(defvar coq-keywords-declcoq-keywords-decl124,4542
+(defvar coq-keywords-defncoq-keywords-defn139,4898
+(defun coq-count-match coq-count-match213,7254
+(defun coq-goal-command-p coq-goal-command-p225,7674
+(defvar coq-keywords-save-strictcoq-keywords-save-strict245,8258
+(defvar coq-keywords-savecoq-keywords-save253,8355
+(defun coq-save-command-p coq-save-command-p257,8431
+(defvar coq-keywords-kill-goal coq-keywords-kill-goal265,8710
+(defcustom coq-user-state-changing-commands coq-user-state-changing-commands271,8760
+(defcustom coq-user-state-preserving-commands coq-user-state-preserving-commands283,9157
+(defvar coq-keywords-state-preserving-commandscoq-keywords-state-preserving-commands296,9597
+(defvar coq-keywords-state-changing-misc-commandscoq-keywords-state-changing-misc-commands344,10722
+(defvar coq-keywords-state-changing-commandscoq-keywords-state-changing-commands418,12740
+(defvar coq-keywords-commandscoq-keywords-commands428,12937
+(defcustom coq-user-state-changing-tactics coq-user-state-changing-tactics434,13087
+(defvar coq-state-changing-tacticscoq-state-changing-tactics445,13513
+(defcustom coq-user-state-preserving-tactics coq-user-state-preserving-tactics646,16838
+(defvar coq-state-preserving-tacticscoq-state-preserving-tactics657,17252
+(defvar coq-tacticscoq-tactics661,17350
+(defvar coq-retractable-instructcoq-retractable-instruct664,17439
+(defvar coq-non-retractable-instructcoq-non-retractable-instruct667,17549
+(defvar coq-keywordscoq-keywords671,17671
+(defvar coq-tacticalscoq-tacticals676,17836
+(defvar coq-reserved-commoncoq-reserved-common698,18219
+(defvar coq-reserved-V8coq-reserved-V8714,18412
+(defvar coq-reserved-V7coq-reserved-V7725,18516
+(defvar coq-reserved coq-reserved730,18591
+(defvar coq-symbolscoq-symbols738,18747
+(defvar coq-error-regexp coq-error-regexp756,18951
+(defvar coq-id coq-id759,19180
+(defvar coq-ids coq-ids761,19206
+(defun coq-first-abstr-regexp coq-first-abstr-regexp763,19243
+(defun coq-next-abstr-regexp coq-next-abstr-regexp766,19331
+(defvar coq-font-lock-termscoq-font-lock-terms769,19409
+(defconst coq-save-command-regexp-strictcoq-save-command-regexp-strict784,20062
+(defconst coq-save-command-regexpcoq-save-command-regexp786,20175
+(defconst coq-save-with-hole-regexpcoq-save-with-hole-regexp788,20274
+(defconst coq-goal-command-regexpcoq-goal-command-regexp791,20412
+(defconst coq-goal-with-hole-regexpcoq-goal-with-hole-regexp793,20511
+(defconst coq-decl-with-hole-regexpcoq-decl-with-hole-regexp799,20800
+(defconst coq-defn-with-hole-regexpcoq-defn-with-hole-regexp802,20933
+(defvar coq-font-lock-keywords-1coq-font-lock-keywords-1805,21073
+(defvar coq-font-lock-keywords coq-font-lock-keywords826,22116
+(defun coq-init-syntax-table coq-init-syntax-table828,22174
+(defconst coq-generic-expressioncoq-generic-expression857,23072
 
 coq/x-symbol-coq.el,2822
 (defvar x-symbol-coq-required-fonts x-symbol-coq-required-fonts16,384
@@ -239,69 +239,6 @@ demoisa/demoisa.el,568
 (define-derived-mode demoisa-goals-mode demoisa-goals-mode133,4387
 (defun demoisa-pre-shell-start demoisa-pre-shell-start152,5169
 
-generic/holes.el,3536
-(defun holes-short-doc holes-short-doc24,736
-(defcustom empty-hole-string empty-hole-string149,5370
-(defcustom empty-hole-regexp empty-hole-regexp152,5475
-(defcustom hole-search-limit hole-search-limit155,6075
-(defface active-hole-faceactive-hole-face168,6441
-(defface inactive-hole-faceinactive-hole-face178,6898
-(defun region-beginning-or-nil region-beginning-or-nil197,7434
-(defun region-end-or-nil region-end-or-nil201,7523
-(defun copy-active-region copy-active-region205,7602
-(defun is-hole-p is-hole-p211,7780
-(defun hole-start-position hole-start-position216,7840
-(defun hole-end-position hole-end-position221,7977
-(defun hole-buffer hole-buffer226,8107
-(defun hole-at hole-at231,8229
-(defun active-hole-exist-p active-hole-exist-p240,8417
-(defun active-hole-start-position active-hole-start-position250,8668
-(defun active-hole-end-position active-hole-end-position261,9018
-(defun active-hole-buffer active-hole-buffer273,9364
-(defun goto-active-hole goto-active-hole284,9644
-(defun highlight-hole-as-active highlight-hole-as-active296,9917
-(defun highlight-hole highlight-hole306,10224
-(defun disable-active-hole disable-active-hole317,10519
-(defun set-active-hole set-active-hole335,11028
-(defun is-in-hole-p is-in-hole-p347,11329
-(defun make-hole make-hole357,11474
-(defun make-hole-at make-hole-at382,12289
-(defun clear-hole clear-hole401,12731
-(defun clear-hole-at clear-hole-at411,12948
-(defun map-holes map-holes420,13177
-(defun mapcar-holes mapcar-holes426,13291
-(defun clear-all-buffer-holes clear-all-buffer-holes430,13390
-(defun next-hole next-hole442,13624
-(defun next-after-active-hole next-after-active-hole451,13888
-(defun set-active-hole-next set-active-hole-next458,14068
-(defun set-active-hole-next-after-active set-active-hole-next-after-active475,14425
-(defun replace-segment replace-segment486,14583
-(defun replace-hole replace-hole502,14899
-(defun replace-active-hole replace-active-hole536,16055
-(defun replace-update-active-hole replace-update-active-hole545,16338
-(defun delete-update-active-hole delete-update-active-hole568,16964
-(defun set-make-active-hole set-make-active-hole577,17161
-(defun mouse-replace-active-hole mouse-replace-active-hole624,18508
-(defun destroy-hole destroy-hole642,18984
-(defun hole-at-event hole-at-event657,19295
-(defun mouse-destroy-hole mouse-destroy-hole659,19354
-(defun mouse-forget-hole mouse-forget-hole667,19528
-(defun mouse-set-make-active-hole mouse-set-make-active-hole681,19769
-(defun mouse-set-active-hole mouse-set-active-hole701,20220
-(defun set-point-next-hole-destroy set-point-next-hole-destroy711,20414
-(defun count-char-in-string count-char-in-string775,22661
-(defun count-re-in-string count-re-in-string785,22866
-(defun count-chars-in-last-expand count-chars-in-last-expand795,23077
-(defun count-newlines-in-last-expand count-newlines-in-last-expand799,23166
-(defun indent-last-expand indent-last-expand803,23277
-(defun count-holes-in-last-expand count-holes-in-last-expand818,23603
-(defun replace-string-by-holes replace-string-by-holes822,23722
-(defun replace-string-by-holes-backward replace-string-by-holes-backward841,24148
-(defun replace-string-by-holes-move-point replace-string-by-holes-move-point872,24966
-(defun replace-string-by-holes-backward-move-point replace-string-by-holes-backward-move-point879,25120
-(defun holes-abbrev-complete holes-abbrev-complete889,25296
-(defun insert-and-expand insert-and-expand911,26098
-
 generic/pg-assoc.el,408
 (define-derived-mode proof-universal-keys-only-mode proof-universal-keys-only-mode20,563
 (defun proof-associated-buffers proof-associated-buffers32,987
@@ -328,63 +265,131 @@ generic/pg-goals.el,1074
 (defun pg-goals-construct-command pg-goals-construct-command348,12775
 (defun pg-goals-get-subterm-help pg-goals-get-subterm-help372,13627
 
-generic/pg-init.el,0
-
 generic/pg-metadata.el,204
 (defcustom pg-metadata-default-directory pg-metadata-default-directory23,628
 (defface proof-preparsed-span proof-preparsed-span28,802
 (defun pg-metadata-filename-for pg-metadata-filename-for39,1065
 
-generic/pg-nxml.el,66
-(defun pg-nxml-support-available pg-nxml-support-available9,236
-
-generic/pg-pgip.el,1154
-(defalias 'pg-pgip-error pg-pgip-error17,544
-(defun pg-pgip-process-packet pg-pgip-process-packet20,593
-(defun pg-pgip-process-cmds pg-pgip-process-cmds28,981
-(defun pg-pgip-post-process pg-pgip-post-process88,2599
-(defun pg-pgip-haspref pg-pgip-haspref125,3616
-(defun pg-pgip-default-for pg-pgip-default-for188,5899
-(defun pg-pgip-subst-for pg-pgip-subst-for199,6211
-(defun pg-pgip-get-type pg-pgip-get-type206,6372
-(defun pg-pgip-pgiptype pg-pgip-pgiptype213,6594
-(defun pg-pgip-interpret-bool pg-pgip-interpret-bool237,7458
-(defun pg-pgip-interpret-int pg-pgip-interpret-int246,7734
-(defun pg-pgip-interpret-string pg-pgip-interpret-string251,7897
-(defun pg-pgip-interpret-choice pg-pgip-interpret-choice254,7947
-(defun pg-pgip-interpret-value pg-pgip-interpret-value274,8642
-(defun pg-pgip-get-attr pg-pgip-get-attr297,9267
-(defun pg-pgip-get-version pg-pgip-get-version304,9480
-(defun pg-prover-interpret-pgip-command pg-prover-interpret-pgip-command312,9712
-(defun pg-issue-pgip pg-issue-pgip329,10134
-(defun pg-pgip-askprefs pg-pgip-askprefs337,10406
-(defun pg-pgip-parsescript pg-pgip-parsescript346,10618
-
-generic/pg-response.el,1673
+generic/pg-pgip.el,4870
+(defalias 'pg-pgip-debug pg-pgip-debug22,725
+(defalias 'pg-pgip-error pg-pgip-error23,766
+(defalias 'pg-pgip-warning pg-pgip-warning24,801
+(defun pg-pgip-process-packet pg-pgip-process-packet27,866
+(defvar pg-pgip-last-seen-id pg-pgip-last-seen-id37,1439
+(defvar pg-pgip-last-seen-seq pg-pgip-last-seen-seq38,1473
+(defun pg-pgip-process-pgip pg-pgip-process-pgip40,1509
+(defun pg-pgip-process-msg pg-pgip-process-msg56,2224
+(defvar pg-pgip-post-process-functionspg-pgip-post-process-functions69,2770
+(defun pg-pgip-post-process pg-pgip-post-process78,3164
+(defun pg-pgip-process-usespgip pg-pgip-process-usespgip94,3775
+(defun pg-pgip-process-usespgml pg-pgip-process-usespgml98,3939
+(defun pg-pgip-process-pgmlconfig pg-pgip-process-pgmlconfig102,4103
+(defun pg-pgip-process-proverinfo pg-pgip-process-proverinfo118,4711
+(defun pg-pgip-process-hasprefs pg-pgip-process-hasprefs135,5365
+(defun pg-pgip-haspref pg-pgip-haspref149,5997
+(defun pg-pgip-process-prefval pg-pgip-process-prefval168,6776
+(defun pg-pgip-process-guiconfig pg-pgip-process-guiconfig195,7485
+(defun pg-pgip-process-ids pg-pgip-process-ids202,7602
+(defalias 'pg-pgip-process-setids pg-pgip-process-setids224,8508
+(defalias 'pg-pgip-process-addids pg-pgip-process-addids225,8564
+(defalias 'pg-pgip-process-delids pg-pgip-process-delids226,8620
+(defun pg-pgip-process-idvalue pg-pgip-process-idvalue229,8678
+(defun pg-pgip-process-menuadd pg-pgip-process-menuadd241,9015
+(defun pg-pgip-process-menudel pg-pgip-process-menudel244,9058
+(defun pg-pgip-process-ready pg-pgip-process-ready253,9291
+(defun pg-pgip-process-cleardisplay pg-pgip-process-cleardisplay256,9332
+(defun pg-pgip-process-proofstate pg-pgip-process-proofstate270,9809
+(defun pg-pgip-process-normalresponse pg-pgip-process-normalresponse274,9886
+(defun pg-pgip-process-errorresponse pg-pgip-process-errorresponse278,10010
+(defun pg-pgip-process-scriptinsert pg-pgip-process-scriptinsert282,10133
+(defun pg-pgip-process-metainforesponse pg-pgip-process-metainforesponse287,10267
+(defun pg-pgip-process-parseresult pg-pgip-process-parseresult290,10319
+(defun pg-pgip-process-informfileloaded pg-pgip-process-informfileloaded299,10555
+(defun pg-pgip-process-informfileretracted pg-pgip-process-informfileretracted305,10821
+(defun pg-pgip-process-brokerstatus pg-pgip-process-brokerstatus318,11295
+(defun pg-pgip-process-proveravailmsg pg-pgip-process-proveravailmsg321,11343
+(defun pg-pgip-process-newprovermsg pg-pgip-process-newprovermsg324,11393
+(defun pg-pgip-process-proverstatusmsg pg-pgip-process-proverstatusmsg327,11441
+(defvar pg-pgip-srcids pg-pgip-srcids336,11688
+(defun pg-pgip-process-newfile pg-pgip-process-newfile340,11795
+(defun pg-pgip-process-filestatus pg-pgip-process-filestatus356,12383
+(defun pg-pgip-process-newobj pg-pgip-process-newobj376,13038
+(defun pg-pgip-process-delobj pg-pgip-process-delobj379,13080
+(defun pg-pgip-process-objectstatus pg-pgip-process-objectstatus382,13122
+(defun pg-pgip-process-parsescript pg-pgip-process-parsescript396,13478
+(defun pg-pgip-get-pgiptype pg-pgip-get-pgiptype419,14354
+(defun pg-pgip-default-for pg-pgip-default-for439,15149
+(defun pg-pgip-subst-for pg-pgip-subst-for452,15544
+(defun pg-pgip-interpret-value pg-pgip-interpret-value464,15887
+(defun pg-pgip-interpret-choice pg-pgip-interpret-choice482,16570
+(defun pg-pgip-get-icon pg-pgip-get-icon513,17643
+(defsubst pg-pgip-get-name pg-pgip-get-name517,17791
+(defsubst pg-pgip-get-version pg-pgip-get-version520,17908
+(defsubst pg-pgip-get-descr pg-pgip-get-descr523,18031
+(defsubst pg-pgip-get-thmname pg-pgip-get-thmname526,18150
+(defsubst pg-pgip-get-thyname pg-pgip-get-thyname529,18273
+(defsubst pg-pgip-get-url pg-pgip-get-url532,18396
+(defsubst pg-pgip-get-srcid pg-pgip-get-srcid535,18511
+(defsubst pg-pgip-get-proverid pg-pgip-get-proverid538,18630
+(defsubst pg-pgip-get-symname pg-pgip-get-symname541,18755
+(defsubst pg-pgip-get-prefcat pg-pgip-get-prefcat544,18875
+(defsubst pg-pgip-get-default pg-pgip-get-default547,19003
+(defsubst pg-pgip-get-objtype pg-pgip-get-objtype550,19126
+(defsubst pg-pgip-get-value pg-pgip-get-value553,19249
+(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext556,19311
+(defun pg-pgip-get-pgmltext pg-pgip-get-pgmltext558,19370
+(defun pg-pgip-string-of-command pg-pgip-string-of-command567,19597
+(defconst pg-pgip-idpg-pgip-id584,20358
+(defvar pg-pgip-refseq pg-pgip-refseq590,20638
+(defvar pg-pgip-refid pg-pgip-refid592,20736
+(defvar pg-pgip-seq pg-pgip-seq595,20830
+(defun pg-pgip-assemble-packet pg-pgip-assemble-packet597,20894
+(defun pg-pgip-issue pg-pgip-issue615,21709
+(defun pg-pgip-askprefs pg-pgip-askprefs632,22322
+(defun pg-pgip-askids pg-pgip-askids636,22436
+(defun pg-pgip-reset pg-pgip-reset649,22727
+
+generic/pg-pgip-old.el,734
+(defun pg-pgip-process-oldhaspref pg-pgip-process-oldhaspref18,633
+(defun pg-pgip-process-haspref pg-pgip-process-haspref21,730
+(defun pg-pgip-old-interpret-bool pg-pgip-old-interpret-bool58,2245
+(defun pg-pgip-old-interpret-int pg-pgip-old-interpret-int67,2529
+(defun pg-pgip-old-interpret-string pg-pgip-old-interpret-string72,2696
+(defun pg-pgip-old-interpret-choice pg-pgip-old-interpret-choice75,2750
+(defun pg-pgip-old-interpret-value pg-pgip-old-interpret-value95,3469
+(defun pg-pgip-old-default-for pg-pgip-old-default-for114,4015
+(defun pg-pgip-old-subst-for pg-pgip-old-subst-for125,4339
+(defun pg-pgip-old-get-type pg-pgip-old-get-type132,4504
+(defun pg-pgip-old-pgiptype pg-pgip-old-pgiptype139,4726
+
+generic/pg-response.el,1890
 (define-derived-mode proof-response-mode proof-response-mode24,597
 (defun proof-response-config-done proof-response-config-done47,1490
 (defvar proof-shell-special-display-regexp proof-shell-special-display-regexp68,2265
 (defconst proof-multiframe-specifiers proof-multiframe-specifiers76,2670
 (defun proof-map-multiple-frame-specifiers proof-map-multiple-frame-specifiers85,3034
 (defconst proof-multiframe-parametersproof-multiframe-parameters95,3496
-(defun proof-multiple-frames-enable proof-multiple-frames-enable103,3730
-(defun proof-three-window-enable proof-three-window-enable125,4450
-(defun proof-select-three-b proof-select-three-b129,4514
-(defun proof-display-three-b proof-display-three-b144,4983
-(defvar pg-frame-configuration pg-frame-configuration158,5477
-(defun pg-cache-frame-configuration pg-cache-frame-configuration162,5624
-(defun proof-layout-windows proof-layout-windows166,5795
-(defun proof-delete-other-frames proof-delete-other-frames207,7608
-(defvar pg-response-erase-flag pg-response-erase-flag238,8703
-(defun proof-shell-maybe-erase-responseproof-shell-maybe-erase-response241,8818
-(defun pg-response-display pg-response-display271,9968
-(defun pg-response-display-with-face pg-response-display-with-face288,10790
-(defun pg-response-clear-displays pg-response-clear-displays323,12147
-(defvar pg-response-next-error pg-response-next-error340,12677
-(defun proof-next-error proof-next-error344,12799
-(defvar proof-trace-last-fontify-pos proof-trace-last-fontify-pos439,16212
-(defun proof-trace-buffer-display proof-trace-buffer-display442,16304
-(defun pg-thms-buffer-clear pg-thms-buffer-clear482,17517
+(defun proof-multiple-frames-enable proof-multiple-frames-enable104,3795
+(defun proof-three-window-enable proof-three-window-enable126,4515
+(defun proof-select-three-b proof-select-three-b130,4579
+(defun proof-display-three-b proof-display-three-b145,5048
+(defvar pg-frame-configuration pg-frame-configuration159,5542
+(defun pg-cache-frame-configuration pg-cache-frame-configuration163,5689
+(defun proof-layout-windows proof-layout-windows167,5860
+(defun proof-delete-other-frames proof-delete-other-frames208,7673
+(defvar pg-response-erase-flag pg-response-erase-flag239,8768
+(defun proof-shell-maybe-erase-responseproof-shell-maybe-erase-response242,8883
+(defun pg-response-display pg-response-display272,10033
+(defun pg-response-display-with-face pg-response-display-with-face289,10855
+(defun pg-response-clear-displays pg-response-clear-displays324,12212
+(defvar pg-response-next-error pg-response-next-error341,12742
+(defun proof-next-error proof-next-error345,12864
+(defun pg-response-has-error-location pg-response-has-error-location425,15798
+(defvar proof-trace-last-fontify-pos proof-trace-last-fontify-pos448,16631
+(defun proof-trace-fontify-pos proof-trace-fontify-pos450,16674
+(defun proof-trace-buffer-display proof-trace-buffer-display458,16988
+(defun proof-trace-buffer-finish proof-trace-buffer-finish482,17961
+(defun pg-thms-buffer-clear pg-thms-buffer-clear503,18486
 
 generic/pg-thymodes.el,219
 (defmacro pg-defthymode pg-defthymode19,466
@@ -393,7 +398,7 @@ generic/pg-thymodes.el,219
 (defun pg-modesym pg-modesym78,2520
 (defun pg-modesymval pg-modesymval82,2634
 
-generic/pg-user.el,3521
+generic/pg-user.el,3655
 (defmacro proof-maybe-save-point proof-maybe-save-point21,410
 (defun proof-maybe-follow-locked-end proof-maybe-follow-locked-end29,612
 (defun proof-assert-next-command-interactive proof-assert-next-command-interactive43,977
@@ -439,12 +444,14 @@ generic/pg-user.el,3521
 (defun pg-toggle-visibility pg-toggle-visibility938,31093
 (defun pg-create-in-span-context-menu pg-create-in-span-context-menu948,31415
 (defun pg-goals-buffers-hint pg-goals-buffers-hint1020,33968
-(defun pg-response-buffers-hint pg-response-buffers-hint1023,34135
-(defun pg-jump-to-end-hint pg-jump-to-end-hint1032,34484
-(defun pg-processing-complete-hint pg-processing-complete-hint1035,34600
-(defun pg-hint pg-hint1051,35286
-(defun pg-identifier-under-mouse-query pg-identifier-under-mouse-query1070,35962
-(defun proof-imenu-enable proof-imenu-enable1115,37589
+(defun pg-slow-fontify-tracing-hint pg-slow-fontify-tracing-hint1023,34135
+(defun pg-response-buffers-hint pg-response-buffers-hint1026,34291
+(defun pg-jump-to-end-hint pg-jump-to-end-hint1035,34640
+(defun pg-processing-complete-hint pg-processing-complete-hint1038,34756
+(defun pg-next-error-hint pg-next-error-hint1054,35442
+(defun pg-hint pg-hint1058,35579
+(defun pg-identifier-under-mouse-query pg-identifier-under-mouse-query1077,36255
+(defun proof-imenu-enable proof-imenu-enable1122,37882
 
 generic/pg-xhtml.el,573
 (defvar pg-xhtml-dir pg-xhtml-dir17,423
@@ -458,60 +465,25 @@ generic/pg-xhtml.el,573
 (defun pg-xhtml-display-file-mozilla pg-xhtml-display-file-mozilla79,2229
 (defalias 'pg-xhtml-display-file pg-xhtml-display-file84,2402
 
-generic/pg-xml.el,1487
-(defconst pg-xml-name pg-xml-name32,848
-(defconst pg-xml-space pg-xml-space33,901
-(defconst pg-xml-ref pg-xml-ref34,936
-(defconst pg-xml-start-open-elt-regexp pg-xml-start-open-elt-regexp36,1012
-(defconst pg-xml-end-open-elt-regexp pg-xml-end-open-elt-regexp38,1106
-(defconst pg-xml-close-elt-regexp pg-xml-close-elt-regexp40,1185
-(defconst pg-xml-attribute-regexp pg-xml-attribute-regexp42,1276
-(defconst pg-xml-attribute-val-regexp pg-xml-attribute-val-regexp44,1364
-(defconst pg-xml-comment-start-regexp pg-xml-comment-start-regexp47,1515
-(defconst pg-xml-comment-end-regexp pg-xml-comment-end-regexp48,1561
-(defconst pg-xml-anymarkup-regexp pg-xml-anymarkup-regexp49,1604
-(defconst pg-xml-special-eltspg-xml-special-elts50,1643
-(defvar xmlparse xmlparse54,1742
-(defun pg-xml-add-text pg-xml-add-text57,1797
-(defun pg-xml-parse-buffer pg-xml-parse-buffer64,2009
-(defun pg-xml-parse-string pg-xml-parse-string171,5979
-(defconst pg-xml-header pg-xml-header188,6468
-(defvar pg-xml-doc pg-xml-doc191,6544
-(defvar pg-xml-openelts pg-xml-openelts194,6634
-(defvar pg-xml-indentp pg-xml-indentp197,6690
-(defun pg-xml-encode-entities pg-xml-encode-entities200,6763
-(defun pg-xml-begin-write pg-xml-begin-write210,7252
-(defun pg-xml-indent pg-xml-indent215,7444
-(defun pg-xml-openelt pg-xml-openelt221,7583
-(defun pg-xml-closeelt pg-xml-closeelt240,8129
-(defun pg-xml-writetext pg-xml-writetext252,8399
-(defun pg-xml-doc pg-xml-doc255,8500
+generic/pg-xml.el,627
+(defun pg-xml-parse-string pg-xml-parse-string38,1118
+(defun pg-xml-parse-buffer pg-xml-parse-buffer49,1452
+(defun pg-xml-get-attr pg-xml-get-attr71,2185
+(defun pg-xml-child-elts pg-xml-child-elts79,2489
+(defun pg-xml-child-elt pg-xml-child-elt84,2694
+(defun pg-xml-get-child pg-xml-get-child92,2977
+(defun pg-xml-get-text-content pg-xml-get-text-content102,3349
+(defmacro pg-xml-attr pg-xml-attr113,3699
+(defmacro pg-xml-node pg-xml-node115,3761
+(defconst pg-xml-header pg-xml-header118,3854
+(defun pg-xml-string-of pg-xml-string-of122,3931
+(defun pg-xml-output-internal pg-xml-output-internal133,4303
 
 generic/_pkg.el,0
 
 generic/proof-autoloads.el,0
 
-generic/proof-compat.el,999
-(defun pg-custom-undeclare-variable pg-custom-undeclare-variable28,1002
-(defun subst-char-in-string subst-char-in-string99,3142
-(defun replace-regexp-in-string replace-regexp-in-string112,3633
-(defconst menuvisiblep menuvisiblep174,6346
-(defun set-window-text-height set-window-text-height191,6965
-(defmacro save-selected-frame save-selected-frame217,7915
-(defun warn warn256,9217
-(defun redraw-modeline redraw-modeline263,9472
-(defun replace-in-string replace-in-string278,10039
-(defun proof-buffer-syntactic-context-emulate proof-buffer-syntactic-context-emulate327,11557
-(defvar read-shell-command-mapread-shell-command-map360,12864
-(defun read-shell-command read-shell-command378,13566
-(defun remassq remassq390,14047
-(defun remassoc remassoc402,14436
-(defun frames-of-buffer frames-of-buffer415,14881
-(defmacro with-selected-window with-selected-window454,16144
-(defun pg-pop-to-buffer pg-pop-to-buffer490,17269
-(defun process-live-p process-live-p541,19121
-
-generic/proof-config.el,16702
+generic/proof-config.el,16775
 (defgroup proof-user-options proof-user-options84,3173
 (defcustom proof-electric-terminator-enable proof-electric-terminator-enable89,3287
 (defcustom proof-toolbar-enable proof-toolbar-enable101,3821
@@ -544,196 +516,197 @@ generic/proof-config.el,16702
 (defgroup proof-faces proof-faces433,16394
 (defmacro proof-face-specs proof-face-specs438,16500
 (defface proof-queue-face proof-queue-face453,16946
-(defface proof-locked-faceproof-locked-face461,17219
-(defface proof-declaration-name-faceproof-declaration-name-face469,17477
-(defconst proof-declaration-name-face proof-declaration-name-face481,17870
-(defface proof-tacticals-name-faceproof-tacticals-name-face486,18106
-(defconst proof-tacticals-name-face proof-tacticals-name-face495,18368
-(defface proof-tactics-name-faceproof-tactics-name-face500,18598
-(defconst proof-tactics-name-face proof-tactics-name-face509,18863
-(defface proof-error-face proof-error-face514,19087
-(defface proof-warning-faceproof-warning-face522,19294
-(defface proof-eager-annotation-faceproof-eager-annotation-face531,19551
-(defface proof-debug-message-faceproof-debug-message-face539,19769
-(defface proof-boring-faceproof-boring-face547,19968
-(defface proof-mouse-highlight-faceproof-mouse-highlight-face555,20160
-(defface proof-highlight-dependent-faceproof-highlight-dependent-face563,20356
-(defface proof-highlight-dependency-faceproof-highlight-dependency-face571,20565
-(defgroup prover-config prover-config589,20824
-(defcustom proof-mode-for-shell proof-mode-for-shell623,21943
-(defcustom proof-mode-for-response proof-mode-for-response630,22190
-(defcustom proof-mode-for-goals proof-mode-for-goals637,22473
-(defcustom proof-mode-for-script proof-mode-for-script644,22728
-(defcustom proof-guess-command-line proof-guess-command-line655,23162
-(defcustom proof-assistant-home-page proof-assistant-home-page670,23659
-(defcustom proof-context-command proof-context-command676,23829
-(defcustom proof-info-command proof-info-command681,23963
-(defcustom proof-showproof-command proof-showproof-command688,24235
-(defcustom proof-goal-command proof-goal-command693,24371
-(defcustom proof-save-command proof-save-command701,24669
-(defcustom proof-find-theorems-command proof-find-theorems-command709,24979
-(defconst proof-toolbar-entries-defaultproof-toolbar-entries-default716,25288
-(defpgcustom toolbar-entries toolbar-entries747,27020
-(defcustom proof-assistant-true-value proof-assistant-true-value765,27741
-(defcustom proof-assistant-false-value proof-assistant-false-value771,27931
-(defcustom proof-assistant-format-int-fn proof-assistant-format-int-fn777,28125
-(defcustom proof-assistant-format-string-fn proof-assistant-format-string-fn784,28374
-(defcustom proof-assistant-setting-format proof-assistant-setting-format791,28641
-(defgroup proof-script proof-script813,29336
-(defcustom proof-terminal-char proof-terminal-char818,29466
-(defcustom proof-script-sexp-commands proof-script-sexp-commands828,29870
-(defcustom proof-script-command-end-regexp proof-script-command-end-regexp839,30340
-(defcustom proof-script-command-start-regexp proof-script-command-start-regexp857,31159
-(defcustom proof-script-use-old-parser proof-script-use-old-parser868,31621
-(defcustom proof-script-integral-proofs proof-script-integral-proofs880,32110
-(defcustom proof-script-fly-past-comments proof-script-fly-past-comments895,32766
-(defcustom proof-script-parse-function proof-script-parse-function902,33083
-(defcustom proof-script-comment-start proof-script-comment-start920,33729
-(defcustom proof-script-comment-start-regexp proof-script-comment-start-regexp931,34164
-(defcustom proof-script-comment-end proof-script-comment-end939,34481
-(defcustom proof-script-comment-end-regexp proof-script-comment-end-regexp951,34899
-(defcustom pg-insert-output-as-comment-fn pg-insert-output-as-comment-fn959,35210
-(defcustom proof-string-start-regexp proof-string-start-regexp965,35462
-(defcustom proof-string-end-regexp proof-string-end-regexp970,35627
-(defcustom proof-case-fold-search proof-case-fold-search975,35788
-(defcustom proof-save-command-regexp proof-save-command-regexp984,36204
-(defcustom proof-save-with-hole-regexp proof-save-with-hole-regexp989,36315
-(defcustom proof-save-with-hole-result proof-save-with-hole-result1001,36767
-(defcustom proof-goal-command-regexp proof-goal-command-regexp1012,37231
-(defcustom proof-goal-with-hole-regexp proof-goal-with-hole-regexp1021,37623
-(defcustom proof-goal-with-hole-result proof-goal-with-hole-result1033,38067
-(defcustom proof-non-undoables-regexp proof-non-undoables-regexp1043,38466
-(defcustom proof-nested-undo-regexp proof-nested-undo-regexp1054,38922
-(defcustom proof-ignore-for-undo-count proof-ignore-for-undo-count1070,39634
-(defcustom proof-script-next-entity-regexps proof-script-next-entity-regexps1078,39937
-(defcustom proof-script-find-next-entity-fnproof-script-find-next-entity-fn1122,41671
-(defcustom proof-script-imenu-generic-expression proof-script-imenu-generic-expression1142,42501
-(defcustom proof-goal-command-p proof-goal-command-p1157,43162
-(defcustom proof-really-save-command-p proof-really-save-command-p1184,44598
-(defcustom proof-completed-proof-behaviour proof-completed-proof-behaviour1196,45059
-(defcustom proof-count-undos-fn proof-count-undos-fn1224,46419
-(defconst proof-no-command proof-no-command1259,48020
-(defcustom proof-find-and-forget-fn proof-find-and-forget-fn1264,48224
-(defcustom proof-forget-id-command proof-forget-id-command1281,48935
-(defcustom pg-topterm-goalhyp-fn pg-topterm-goalhyp-fn1291,49293
-(defcustom proof-kill-goal-command proof-kill-goal-command1303,49774
-(defcustom proof-undo-n-times-cmd proof-undo-n-times-cmd1317,50284
-(defcustom proof-nested-goals-history-p proof-nested-goals-history-p1331,50833
-(defcustom proof-state-preserving-p proof-state-preserving-p1340,51171
-(defcustom proof-activate-scripting-hook proof-activate-scripting-hook1350,51641
-(defcustom proof-deactivate-scripting-hook proof-deactivate-scripting-hook1369,52419
-(defcustom proof-indent proof-indent1382,52784
-(defcustom proof-indent-pad-eol proof-indent-pad-eol1388,52958
-(defcustom proof-indent-hang proof-indent-hang1395,53198
-(defcustom proof-indent-enclose-offset proof-indent-enclose-offset1400,53324
-(defcustom proof-indent-open-offset proof-indent-open-offset1405,53466
-(defcustom proof-indent-close-offset proof-indent-close-offset1410,53603
-(defcustom proof-indent-any-regexp proof-indent-any-regexp1415,53741
-(defcustom proof-indent-inner-regexp proof-indent-inner-regexp1420,53901
-(defcustom proof-indent-enclose-regexp proof-indent-enclose-regexp1425,54055
-(defcustom proof-indent-open-regexp proof-indent-open-regexp1430,54209
-(defcustom proof-indent-close-regexp proof-indent-close-regexp1435,54361
-(defcustom proof-script-font-lock-keywords proof-script-font-lock-keywords1441,54515
-(defcustom proof-script-syntax-table-entries proof-script-syntax-table-entries1449,54838
-(defcustom proof-script-span-context-menu-extensions proof-script-span-context-menu-extensions1467,55235
-(defgroup proof-shell proof-shell1493,56024
-(defcustom proof-prog-name proof-prog-name1503,56195
-(defcustom proof-shell-auto-terminate-commands proof-shell-auto-terminate-commands1512,56550
-(defcustom proof-shell-pre-sync-init-cmd proof-shell-pre-sync-init-cmd1521,56947
-(defcustom proof-shell-init-cmd proof-shell-init-cmd1535,57506
-(defcustom proof-shell-restart-cmd proof-shell-restart-cmd1546,57976
-(defcustom proof-shell-quit-cmd proof-shell-quit-cmd1551,58131
-(defcustom proof-shell-quit-timeout proof-shell-quit-timeout1556,58298
-(defcustom proof-shell-cd-cmd proof-shell-cd-cmd1566,58746
-(defcustom proof-shell-start-silent-cmd proof-shell-start-silent-cmd1583,59413
-(defcustom proof-shell-stop-silent-cmd proof-shell-stop-silent-cmd1592,59789
-(defcustom proof-shell-silent-threshold proof-shell-silent-threshold1601,60126
-(defcustom  proof-shell-inform-file-processed-cmd proof-shell-inform-file-processed-cmd1609,60460
-(defcustom  proof-shell-inform-file-retracted-cmd proof-shell-inform-file-retracted-cmd1630,61383
-(defcustom proof-auto-multiple-files proof-auto-multiple-files1658,62654
-(defcustom proof-cannot-reopen-processed-files proof-cannot-reopen-processed-files1673,63375
-(defcustom proof-shell-require-command-regexp proof-shell-require-command-regexp1687,64042
-(defcustom proof-done-advancing-require-function proof-done-advancing-require-function1698,64504
-(defcustom proof-shell-prompt-pattern proof-shell-prompt-pattern1716,64877
-(defcustom proof-shell-wakeup-char proof-shell-wakeup-char1726,65299
-(defcustom proof-shell-annotated-prompt-regexp proof-shell-annotated-prompt-regexp1732,65530
-(defcustom proof-shell-abort-goal-regexp proof-shell-abort-goal-regexp1748,66170
-(defcustom proof-shell-error-regexp proof-shell-error-regexp1753,66305
-(defcustom proof-shell-truncate-before-error proof-shell-truncate-before-error1773,67099
-(defcustom pg-next-error-regexp pg-next-error-regexp1787,67642
-(defcustom pg-next-error-filename-regexp pg-next-error-filename-regexp1802,68252
-(defcustom pg-next-error-extract-filename pg-next-error-extract-filename1826,69290
-(defcustom proof-shell-interrupt-regexp proof-shell-interrupt-regexp1833,69533
-(defcustom proof-shell-proof-completed-regexp proof-shell-proof-completed-regexp1847,70125
-(defcustom proof-shell-clear-response-regexp proof-shell-clear-response-regexp1860,70633
-(defcustom proof-shell-clear-goals-regexp proof-shell-clear-goals-regexp1867,70932
-(defcustom proof-shell-start-goals-regexp proof-shell-start-goals-regexp1874,71225
-(defcustom proof-shell-end-goals-regexp proof-shell-end-goals-regexp1882,71592
-(defcustom proof-shell-eager-annotation-start proof-shell-eager-annotation-start1888,71834
-(defcustom proof-shell-eager-annotation-start-length proof-shell-eager-annotation-start-length1906,72572
-(defcustom proof-shell-eager-annotation-end proof-shell-eager-annotation-end1917,72999
-(defcustom proof-shell-assumption-regexp proof-shell-assumption-regexp1933,73675
-(defcustom proof-shell-process-file proof-shell-process-file1943,74087
-(defcustom proof-shell-retract-files-regexp proof-shell-retract-files-regexp1965,75039
-(defcustom proof-shell-compute-new-files-list proof-shell-compute-new-files-list1974,75375
-(defcustom pg-use-specials-for-fontify pg-use-specials-for-fontify1986,75920
-(defcustom proof-shell-set-elisp-variable-regexp proof-shell-set-elisp-variable-regexp1994,76244
-(defcustom proof-shell-match-pgip-cmd proof-shell-match-pgip-cmd2027,77716
-(defcustom proof-shell-issue-pgip-cmd proof-shell-issue-pgip-cmd2036,78046
-(defcustom proof-shell-query-dependencies-cmd proof-shell-query-dependencies-cmd2045,78402
-(defcustom proof-shell-theorem-dependency-list-regexp proof-shell-theorem-dependency-list-regexp2052,78662
-(defcustom proof-shell-theorem-dependency-list-split proof-shell-theorem-dependency-list-split2068,79322
-(defcustom proof-shell-show-dependency-cmd proof-shell-show-dependency-cmd2077,79747
-(defcustom proof-shell-identifier-under-mouse-cmd proof-shell-identifier-under-mouse-cmd2084,80016
-(defcustom proof-shell-trace-output-regexp proof-shell-trace-output-regexp2107,81097
-(defcustom proof-shell-thms-output-regexp proof-shell-thms-output-regexp2123,81641
-(defcustom proof-shell-filename-escapes proof-shell-filename-escapes2135,82026
-(defcustom proof-shell-process-connection-type proof-shell-process-connection-type2152,82706
-(defcustom proof-shell-strip-crs-from-input proof-shell-strip-crs-from-input2172,83584
-(defcustom proof-shell-strip-crs-from-output proof-shell-strip-crs-from-output2184,84073
-(defcustom proof-shell-insert-hook proof-shell-insert-hook2192,84441
-(defcustom proof-pre-shell-start-hook proof-pre-shell-start-hook2232,86405
-(defcustom proof-shell-handle-delayed-output-hookproof-shell-handle-delayed-output-hook2248,86877
-(defcustom proof-shell-handle-error-or-interrupt-hookproof-shell-handle-error-or-interrupt-hook2254,87092
-(defcustom proof-shell-pre-interrupt-hookproof-shell-pre-interrupt-hook2269,87706
-(defcustom proof-shell-process-output-system-specific proof-shell-process-output-system-specific2279,88076
-(defcustom proof-state-change-hook proof-state-change-hook2298,88941
-(defcustom proof-shell-font-lock-keywords proof-shell-font-lock-keywords2309,89323
-(defcustom proof-shell-syntax-table-entries proof-shell-syntax-table-entries2317,89651
-(defgroup proof-goals proof-goals2335,90023
-(defcustom pg-subterm-first-special-char pg-subterm-first-special-char2340,90144
-(defcustom pg-subterm-anns-use-stack pg-subterm-anns-use-stack2348,90456
-(defcustom pg-goals-change-goal pg-goals-change-goal2357,90760
-(defcustom pbp-goal-command pbp-goal-command2362,90875
-(defcustom pbp-hyp-command pbp-hyp-command2367,91031
-(defcustom pg-subterm-help-cmd pg-subterm-help-cmd2372,91193
-(defcustom pg-goals-error-regexp pg-goals-error-regexp2379,91429
-(defcustom proof-shell-result-start proof-shell-result-start2384,91589
-(defcustom proof-shell-result-end proof-shell-result-end2390,91823
-(defcustom pg-subterm-start-char pg-subterm-start-char2396,92036
-(defcustom pg-subterm-sep-char pg-subterm-sep-char2410,92618
-(defcustom pg-subterm-end-char pg-subterm-end-char2416,92797
-(defcustom pg-topterm-char pg-topterm-char2422,92954
-(defcustom proof-goals-font-lock-keywords proof-goals-font-lock-keywords2439,93560
-(defcustom proof-resp-font-lock-keywords proof-resp-font-lock-keywords2453,94239
-(defcustom pg-before-fontify-output-hook pg-before-fontify-output-hook2465,94817
-(defcustom pg-after-fontify-output-hook pg-after-fontify-output-hook2473,95177
-(defgroup proof-x-symbol proof-x-symbol2485,95431
-(defcustom proof-xsym-extra-modes proof-xsym-extra-modes2490,95559
-(defcustom proof-xsym-font-lock-keywords proof-xsym-font-lock-keywords2503,96188
-(defcustom proof-xsym-activate-command proof-xsym-activate-command2511,96565
-(defcustom proof-xsym-deactivate-command proof-xsym-deactivate-command2518,96801
-(defpgcustom x-symbol-language x-symbol-language2525,97043
-(defpgcustom favourites favourites2540,97490
-(defpgcustom menu-entries menu-entries2545,97680
-(defpgcustom help-menu-entries help-menu-entries2552,97917
-(defpgcustom keymap keymap2559,98180
-(defpgcustom completion-table completion-table2564,98351
-(defpgcustom tags-program tags-program2574,98716
-(defcustom proof-general-name proof-general-name2586,98889
-(defcustom proof-general-home-pageproof-general-home-page2591,99046
-(defcustom proof-unnamed-theorem-nameproof-unnamed-theorem-name2597,99205
-(defcustom proof-universal-keysproof-universal-keys2605,99481
+(defface proof-locked-faceproof-locked-face461,17226
+(defface proof-declaration-name-faceproof-declaration-name-face474,17729
+(defconst proof-declaration-name-face proof-declaration-name-face486,18122
+(defface proof-tacticals-name-faceproof-tacticals-name-face491,18358
+(defconst proof-tacticals-name-face proof-tacticals-name-face500,18620
+(defface proof-tactics-name-faceproof-tactics-name-face505,18850
+(defconst proof-tactics-name-face proof-tactics-name-face514,19115
+(defface proof-error-face proof-error-face519,19339
+(defface proof-warning-faceproof-warning-face527,19546
+(defface proof-eager-annotation-faceproof-eager-annotation-face536,19803
+(defface proof-debug-message-faceproof-debug-message-face544,20021
+(defface proof-boring-faceproof-boring-face552,20220
+(defface proof-mouse-highlight-faceproof-mouse-highlight-face560,20412
+(defface proof-highlight-dependent-faceproof-highlight-dependent-face568,20608
+(defface proof-highlight-dependency-faceproof-highlight-dependency-face576,20817
+(defgroup prover-config prover-config594,21076
+(defcustom proof-mode-for-shell proof-mode-for-shell628,22195
+(defcustom proof-mode-for-response proof-mode-for-response635,22442
+(defcustom proof-mode-for-goals proof-mode-for-goals642,22725
+(defcustom proof-mode-for-script proof-mode-for-script649,22980
+(defcustom proof-guess-command-line proof-guess-command-line660,23414
+(defcustom proof-assistant-home-page proof-assistant-home-page675,23911
+(defcustom proof-context-command proof-context-command681,24081
+(defcustom proof-info-command proof-info-command686,24215
+(defcustom proof-showproof-command proof-showproof-command693,24487
+(defcustom proof-goal-command proof-goal-command698,24623
+(defcustom proof-save-command proof-save-command706,24921
+(defcustom proof-find-theorems-command proof-find-theorems-command714,25231
+(defconst proof-toolbar-entries-defaultproof-toolbar-entries-default721,25540
+(defpgcustom toolbar-entries toolbar-entries752,27272
+(defcustom proof-assistant-true-value proof-assistant-true-value770,27993
+(defcustom proof-assistant-false-value proof-assistant-false-value776,28183
+(defcustom proof-assistant-format-int-fn proof-assistant-format-int-fn782,28377
+(defcustom proof-assistant-format-string-fn proof-assistant-format-string-fn789,28626
+(defcustom proof-assistant-setting-format proof-assistant-setting-format796,28893
+(defgroup proof-script proof-script818,29588
+(defcustom proof-terminal-char proof-terminal-char823,29718
+(defcustom proof-script-sexp-commands proof-script-sexp-commands833,30122
+(defcustom proof-script-command-end-regexp proof-script-command-end-regexp844,30592
+(defcustom proof-script-command-start-regexp proof-script-command-start-regexp862,31411
+(defcustom proof-script-use-old-parser proof-script-use-old-parser873,31873
+(defcustom proof-script-integral-proofs proof-script-integral-proofs885,32362
+(defcustom proof-script-fly-past-comments proof-script-fly-past-comments900,33018
+(defcustom proof-script-parse-function proof-script-parse-function907,33335
+(defcustom proof-script-comment-start proof-script-comment-start925,33981
+(defcustom proof-script-comment-start-regexp proof-script-comment-start-regexp936,34416
+(defcustom proof-script-comment-end proof-script-comment-end944,34733
+(defcustom proof-script-comment-end-regexp proof-script-comment-end-regexp956,35151
+(defcustom pg-insert-output-as-comment-fn pg-insert-output-as-comment-fn964,35462
+(defcustom proof-string-start-regexp proof-string-start-regexp970,35714
+(defcustom proof-string-end-regexp proof-string-end-regexp975,35879
+(defcustom proof-case-fold-search proof-case-fold-search980,36040
+(defcustom proof-save-command-regexp proof-save-command-regexp989,36456
+(defcustom proof-save-with-hole-regexp proof-save-with-hole-regexp994,36567
+(defcustom proof-save-with-hole-result proof-save-with-hole-result1006,37019
+(defcustom proof-goal-command-regexp proof-goal-command-regexp1017,37483
+(defcustom proof-goal-with-hole-regexp proof-goal-with-hole-regexp1026,37875
+(defcustom proof-goal-with-hole-result proof-goal-with-hole-result1038,38319
+(defcustom proof-non-undoables-regexp proof-non-undoables-regexp1048,38718
+(defcustom proof-nested-undo-regexp proof-nested-undo-regexp1059,39174
+(defcustom proof-ignore-for-undo-count proof-ignore-for-undo-count1075,39886
+(defcustom proof-script-next-entity-regexps proof-script-next-entity-regexps1083,40189
+(defcustom proof-script-find-next-entity-fnproof-script-find-next-entity-fn1127,41923
+(defcustom proof-script-imenu-generic-expression proof-script-imenu-generic-expression1147,42753
+(defcustom proof-goal-command-p proof-goal-command-p1162,43414
+(defcustom proof-really-save-command-p proof-really-save-command-p1189,44850
+(defcustom proof-completed-proof-behaviour proof-completed-proof-behaviour1201,45311
+(defcustom proof-count-undos-fn proof-count-undos-fn1229,46671
+(defconst proof-no-command proof-no-command1264,48272
+(defcustom proof-find-and-forget-fn proof-find-and-forget-fn1269,48476
+(defcustom proof-forget-id-command proof-forget-id-command1286,49187
+(defcustom pg-topterm-goalhyp-fn pg-topterm-goalhyp-fn1296,49545
+(defcustom proof-kill-goal-command proof-kill-goal-command1308,50026
+(defcustom proof-undo-n-times-cmd proof-undo-n-times-cmd1322,50536
+(defcustom proof-nested-goals-history-p proof-nested-goals-history-p1336,51085
+(defcustom proof-state-preserving-p proof-state-preserving-p1345,51423
+(defcustom proof-activate-scripting-hook proof-activate-scripting-hook1355,51893
+(defcustom proof-deactivate-scripting-hook proof-deactivate-scripting-hook1374,52671
+(defcustom proof-indent proof-indent1387,53036
+(defcustom proof-indent-pad-eol proof-indent-pad-eol1393,53210
+(defcustom proof-indent-hang proof-indent-hang1400,53450
+(defcustom proof-indent-enclose-offset proof-indent-enclose-offset1405,53576
+(defcustom proof-indent-open-offset proof-indent-open-offset1410,53718
+(defcustom proof-indent-close-offset proof-indent-close-offset1415,53855
+(defcustom proof-indent-any-regexp proof-indent-any-regexp1420,53993
+(defcustom proof-indent-inner-regexp proof-indent-inner-regexp1425,54153
+(defcustom proof-indent-enclose-regexp proof-indent-enclose-regexp1430,54307
+(defcustom proof-indent-open-regexp proof-indent-open-regexp1435,54461
+(defcustom proof-indent-close-regexp proof-indent-close-regexp1440,54613
+(defcustom proof-script-font-lock-keywords proof-script-font-lock-keywords1446,54767
+(defcustom proof-script-syntax-table-entries proof-script-syntax-table-entries1454,55090
+(defcustom proof-script-span-context-menu-extensions proof-script-span-context-menu-extensions1472,55487
+(defgroup proof-shell proof-shell1498,56276
+(defcustom proof-prog-name proof-prog-name1508,56447
+(defcustom proof-shell-auto-terminate-commands proof-shell-auto-terminate-commands1517,56802
+(defcustom proof-shell-pre-sync-init-cmd proof-shell-pre-sync-init-cmd1526,57199
+(defcustom proof-shell-init-cmd proof-shell-init-cmd1540,57758
+(defcustom proof-shell-restart-cmd proof-shell-restart-cmd1551,58228
+(defcustom proof-shell-quit-cmd proof-shell-quit-cmd1556,58383
+(defcustom proof-shell-quit-timeout proof-shell-quit-timeout1561,58550
+(defcustom proof-shell-cd-cmd proof-shell-cd-cmd1571,58998
+(defcustom proof-shell-start-silent-cmd proof-shell-start-silent-cmd1588,59665
+(defcustom proof-shell-stop-silent-cmd proof-shell-stop-silent-cmd1597,60041
+(defcustom proof-shell-silent-threshold proof-shell-silent-threshold1606,60378
+(defcustom  proof-shell-inform-file-processed-cmd proof-shell-inform-file-processed-cmd1614,60712
+(defcustom  proof-shell-inform-file-retracted-cmd proof-shell-inform-file-retracted-cmd1635,61635
+(defcustom proof-auto-multiple-files proof-auto-multiple-files1663,62906
+(defcustom proof-cannot-reopen-processed-files proof-cannot-reopen-processed-files1678,63627
+(defcustom proof-shell-require-command-regexp proof-shell-require-command-regexp1692,64294
+(defcustom proof-done-advancing-require-function proof-done-advancing-require-function1703,64756
+(defcustom proof-shell-quiet-errors proof-shell-quiet-errors1709,64996
+(defcustom proof-shell-prompt-pattern proof-shell-prompt-pattern1726,65334
+(defcustom proof-shell-wakeup-char proof-shell-wakeup-char1736,65756
+(defcustom proof-shell-annotated-prompt-regexp proof-shell-annotated-prompt-regexp1742,65987
+(defcustom proof-shell-abort-goal-regexp proof-shell-abort-goal-regexp1758,66627
+(defcustom proof-shell-error-regexp proof-shell-error-regexp1763,66762
+(defcustom proof-shell-truncate-before-error proof-shell-truncate-before-error1783,67556
+(defcustom pg-next-error-regexp pg-next-error-regexp1797,68099
+(defcustom pg-next-error-filename-regexp pg-next-error-filename-regexp1812,68709
+(defcustom pg-next-error-extract-filename pg-next-error-extract-filename1836,69747
+(defcustom proof-shell-interrupt-regexp proof-shell-interrupt-regexp1843,69990
+(defcustom proof-shell-proof-completed-regexp proof-shell-proof-completed-regexp1857,70582
+(defcustom proof-shell-clear-response-regexp proof-shell-clear-response-regexp1870,71090
+(defcustom proof-shell-clear-goals-regexp proof-shell-clear-goals-regexp1877,71389
+(defcustom proof-shell-start-goals-regexp proof-shell-start-goals-regexp1884,71682
+(defcustom proof-shell-end-goals-regexp proof-shell-end-goals-regexp1892,72049
+(defcustom proof-shell-eager-annotation-start proof-shell-eager-annotation-start1898,72291
+(defcustom proof-shell-eager-annotation-start-length proof-shell-eager-annotation-start-length1916,73029
+(defcustom proof-shell-eager-annotation-end proof-shell-eager-annotation-end1927,73456
+(defcustom proof-shell-assumption-regexp proof-shell-assumption-regexp1943,74132
+(defcustom proof-shell-process-file proof-shell-process-file1953,74544
+(defcustom proof-shell-retract-files-regexp proof-shell-retract-files-regexp1975,75496
+(defcustom proof-shell-compute-new-files-list proof-shell-compute-new-files-list1984,75832
+(defcustom pg-use-specials-for-fontify pg-use-specials-for-fontify1996,76377
+(defcustom proof-shell-set-elisp-variable-regexp proof-shell-set-elisp-variable-regexp2004,76701
+(defcustom proof-shell-match-pgip-cmd proof-shell-match-pgip-cmd2037,78173
+(defcustom proof-shell-issue-pgip-cmd proof-shell-issue-pgip-cmd2046,78503
+(defcustom proof-shell-query-dependencies-cmd proof-shell-query-dependencies-cmd2055,78859
+(defcustom proof-shell-theorem-dependency-list-regexp proof-shell-theorem-dependency-list-regexp2062,79119
+(defcustom proof-shell-theorem-dependency-list-split proof-shell-theorem-dependency-list-split2078,79779
+(defcustom proof-shell-show-dependency-cmd proof-shell-show-dependency-cmd2087,80204
+(defcustom proof-shell-identifier-under-mouse-cmd proof-shell-identifier-under-mouse-cmd2094,80473
+(defcustom proof-shell-trace-output-regexp proof-shell-trace-output-regexp2117,81554
+(defcustom proof-shell-thms-output-regexp proof-shell-thms-output-regexp2133,82098
+(defcustom proof-shell-filename-escapes proof-shell-filename-escapes2145,82483
+(defcustom proof-shell-process-connection-type proof-shell-process-connection-type2162,83163
+(defcustom proof-shell-strip-crs-from-input proof-shell-strip-crs-from-input2182,84041
+(defcustom proof-shell-strip-crs-from-output proof-shell-strip-crs-from-output2194,84530
+(defcustom proof-shell-insert-hook proof-shell-insert-hook2202,84898
+(defcustom proof-pre-shell-start-hook proof-pre-shell-start-hook2242,86862
+(defcustom proof-shell-handle-delayed-output-hookproof-shell-handle-delayed-output-hook2258,87334
+(defcustom proof-shell-handle-error-or-interrupt-hookproof-shell-handle-error-or-interrupt-hook2264,87549
+(defcustom proof-shell-pre-interrupt-hookproof-shell-pre-interrupt-hook2279,88163
+(defcustom proof-shell-process-output-system-specific proof-shell-process-output-system-specific2289,88533
+(defcustom proof-state-change-hook proof-state-change-hook2308,89398
+(defcustom proof-shell-font-lock-keywords proof-shell-font-lock-keywords2319,89780
+(defcustom proof-shell-syntax-table-entries proof-shell-syntax-table-entries2327,90108
+(defgroup proof-goals proof-goals2345,90480
+(defcustom pg-subterm-first-special-char pg-subterm-first-special-char2350,90601
+(defcustom pg-subterm-anns-use-stack pg-subterm-anns-use-stack2358,90913
+(defcustom pg-goals-change-goal pg-goals-change-goal2367,91217
+(defcustom pbp-goal-command pbp-goal-command2372,91332
+(defcustom pbp-hyp-command pbp-hyp-command2377,91488
+(defcustom pg-subterm-help-cmd pg-subterm-help-cmd2382,91650
+(defcustom pg-goals-error-regexp pg-goals-error-regexp2389,91886
+(defcustom proof-shell-result-start proof-shell-result-start2394,92046
+(defcustom proof-shell-result-end proof-shell-result-end2400,92280
+(defcustom pg-subterm-start-char pg-subterm-start-char2406,92493
+(defcustom pg-subterm-sep-char pg-subterm-sep-char2420,93075
+(defcustom pg-subterm-end-char pg-subterm-end-char2426,93254
+(defcustom pg-topterm-char pg-topterm-char2432,93411
+(defcustom proof-goals-font-lock-keywords proof-goals-font-lock-keywords2449,94017
+(defcustom proof-resp-font-lock-keywords proof-resp-font-lock-keywords2463,94696
+(defcustom pg-before-fontify-output-hook pg-before-fontify-output-hook2475,95274
+(defcustom pg-after-fontify-output-hook pg-after-fontify-output-hook2483,95634
+(defgroup proof-x-symbol proof-x-symbol2495,95888
+(defcustom proof-xsym-extra-modes proof-xsym-extra-modes2500,96016
+(defcustom proof-xsym-font-lock-keywords proof-xsym-font-lock-keywords2513,96645
+(defcustom proof-xsym-activate-command proof-xsym-activate-command2521,97022
+(defcustom proof-xsym-deactivate-command proof-xsym-deactivate-command2528,97258
+(defpgcustom x-symbol-language x-symbol-language2535,97500
+(defpgcustom favourites favourites2550,97947
+(defpgcustom menu-entries menu-entries2555,98137
+(defpgcustom help-menu-entries help-menu-entries2562,98374
+(defpgcustom keymap keymap2569,98637
+(defpgcustom completion-table completion-table2574,98808
+(defpgcustom tags-program tags-program2584,99173
+(defcustom proof-general-name proof-general-name2596,99346
+(defcustom proof-general-home-pageproof-general-home-page2601,99503
+(defcustom proof-unnamed-theorem-nameproof-unnamed-theorem-name2607,99662
+(defcustom proof-universal-keysproof-universal-keys2615,99938
 
 generic/proof-depends.el,1325
 (defvar proof-thm-names-of-files proof-thm-names-of-files19,540
@@ -837,33 +810,33 @@ generic/proof-menu.el,4166
 (defun proof-menu-define-favourites-menu proof-menu-define-favourites-menu496,17589
 (defmacro proof-defshortcut proof-defshortcut517,18260
 (defmacro proof-definvisible proof-definvisible533,18915
-(defun proof-def-favourite proof-def-favourite548,19534
-(defvar proof-make-favourite-cmd-history proof-make-favourite-cmd-history571,20509
-(defvar proof-make-favourite-menu-history proof-make-favourite-menu-history574,20594
-(defun proof-save-favourites proof-save-favourites577,20680
-(defun proof-del-favourite proof-del-favourite582,20828
-(defun proof-read-favourite proof-read-favourite599,21389
-(defun proof-add-favourite proof-add-favourite624,22192
-(defvar proof-assistant-settings proof-assistant-settings651,23243
-(defvar proof-menu-settings proof-menu-settings658,23606
-(defun proof-menu-define-settings-menu proof-menu-define-settings-menu661,23680
-(defun proof-menu-entry-name proof-menu-entry-name679,24324
-(defun proof-menu-entry-for-setting proof-menu-entry-for-setting684,24483
-(defun proof-settings-vars proof-settings-vars702,24973
-(defun proof-settings-changed-from-defaults-p proof-settings-changed-from-defaults-p707,25150
-(defun proof-settings-changed-from-saved-p proof-settings-changed-from-saved-p711,25256
-(defun proof-settings-save proof-settings-save715,25359
-(defun proof-settings-reset proof-settings-reset720,25526
-(defun proof-defpacustom-fn proof-defpacustom-fn728,25772
-(defmacro defpacustom defpacustom793,28165
-(defun proof-assistant-invisible-command-ifposs proof-assistant-invisible-command-ifposs804,28805
-(defun proof-maybe-askprefs proof-maybe-askprefs826,29780
-(defun proof-assistant-settings-cmd proof-assistant-settings-cmd833,29984
-(defun proof-assistant-format proof-assistant-format850,30644
-(defvar proof-assistant-format-table proof-assistant-format-table867,31386
-(defun proof-assistant-format-bool proof-assistant-format-bool875,31755
-(defun proof-assistant-format-int proof-assistant-format-int878,31868
-(defun proof-assistant-format-string proof-assistant-format-string881,31960
+(defun proof-def-favourite proof-def-favourite554,19740
+(defvar proof-make-favourite-cmd-history proof-make-favourite-cmd-history577,20715
+(defvar proof-make-favourite-menu-history proof-make-favourite-menu-history580,20800
+(defun proof-save-favourites proof-save-favourites583,20886
+(defun proof-del-favourite proof-del-favourite588,21034
+(defun proof-read-favourite proof-read-favourite605,21595
+(defun proof-add-favourite proof-add-favourite630,22398
+(defvar proof-assistant-settings proof-assistant-settings657,23449
+(defvar proof-menu-settings proof-menu-settings664,23812
+(defun proof-menu-define-settings-menu proof-menu-define-settings-menu667,23886
+(defun proof-menu-entry-name proof-menu-entry-name687,24630
+(defun proof-menu-entry-for-setting proof-menu-entry-for-setting699,25102
+(defun proof-settings-vars proof-settings-vars717,25592
+(defun proof-settings-changed-from-defaults-p proof-settings-changed-from-defaults-p722,25769
+(defun proof-settings-changed-from-saved-p proof-settings-changed-from-saved-p726,25875
+(defun proof-settings-save proof-settings-save730,25978
+(defun proof-settings-reset proof-settings-reset735,26145
+(defun proof-defpacustom-fn proof-defpacustom-fn743,26391
+(defmacro defpacustom defpacustom819,29275
+(defun proof-assistant-invisible-command-ifposs proof-assistant-invisible-command-ifposs830,29916
+(defun proof-maybe-askprefs proof-maybe-askprefs852,30891
+(defun proof-assistant-settings-cmd proof-assistant-settings-cmd859,31095
+(defun proof-assistant-format proof-assistant-format876,31755
+(defvar proof-assistant-format-table proof-assistant-format-table900,32814
+(defun proof-assistant-format-bool proof-assistant-format-bool908,33183
+(defun proof-assistant-format-int proof-assistant-format-int911,33296
+(defun proof-assistant-format-string proof-assistant-format-string914,33388
 
 generic/proof-mmm.el,179
 (defun proof-mmm-support-available proof-mmm-support-available25,909
@@ -906,85 +879,85 @@ generic/proof-script.el,8107
 (defun proof-only-whitespace-to-locked-region-p proof-only-whitespace-to-locked-region-p420,14842
 (defun proof-in-locked-region-p proof-in-locked-region-p433,15478
 (defun proof-goto-end-of-locked proof-goto-end-of-locked445,15741
-(defun proof-goto-end-of-locked-if-pos-not-visible-in-window proof-goto-end-of-locked-if-pos-not-visible-in-window459,16352
-(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window470,16833
-(defun proof-end-of-locked-visible-p proof-end-of-locked-visible-p484,17486
-(defun proof-goto-end-of-queue-or-locked-if-not-visible proof-goto-end-of-queue-or-locked-if-not-visible493,17937
-(defvar pg-idioms pg-idioms512,18587
-(defvar pg-visibility-specs pg-visibility-specs515,18683
-(deflocal pg-script-portions pg-script-portions520,18890
-(defun pg-clear-script-portions pg-clear-script-portions523,19012
-(defun pg-add-script-element pg-add-script-element541,19676
-(defun pg-remove-script-element pg-remove-script-element544,19752
-(defsubst pg-visname pg-visname552,20030
-(defun pg-add-element pg-add-element556,20175
-(defun pg-open-invisible-span pg-open-invisible-span590,21804
-(defun pg-remove-element pg-remove-element601,22167
-(defun pg-make-element-invisible pg-make-element-invisible608,22437
-(defun pg-make-element-visible pg-make-element-visible614,22694
-(defun pg-toggle-element-visibility pg-toggle-element-visibility619,22873
-(defun pg-redisplay-for-gnuemacs pg-redisplay-for-gnuemacs627,23203
-(defun pg-show-all-portions pg-show-all-portions634,23474
-(defun pg-show-all-proofs pg-show-all-proofs652,24145
-(defun pg-hide-all-proofs pg-hide-all-proofs657,24273
-(defun pg-add-proof-element pg-add-proof-element662,24404
-(defun pg-span-name pg-span-name676,25024
-(defun pg-set-span-helphighlights pg-set-span-helphighlights697,25731
-(defun proof-complete-buffer-atomic proof-complete-buffer-atomic722,26555
-(defun proof-register-possibly-new-processed-file proof-register-possibly-new-processed-file763,28470
-(defun proof-inform-prover-file-retracted proof-inform-prover-file-retracted814,30598
-(defun proof-auto-retract-dependencies proof-auto-retract-dependencies833,31384
-(defun proof-unregister-buffer-file-name proof-unregister-buffer-file-name887,33924
-(defun proof-protected-process-or-retract proof-protected-process-or-retract933,35747
-(defun proof-deactivate-scripting-auto proof-deactivate-scripting-auto960,36917
-(defun proof-deactivate-scripting proof-deactivate-scripting969,37275
-(defun proof-activate-scripting proof-activate-scripting1106,42680
-(defun proof-toggle-active-scripting proof-toggle-active-scripting1234,48434
-(defun proof-done-advancing proof-done-advancing1275,49795
-(defun proof-done-advancing-comment proof-done-advancing-comment1360,53200
-(defun proof-done-advancing-save proof-done-advancing-save1379,53942
-(defun proof-make-goalsave proof-make-goalsave1472,57555
-(defun proof-get-name-from-goal proof-get-name-from-goal1487,58298
-(defun proof-done-advancing-autosave proof-done-advancing-autosave1506,59324
-(defun proof-done-advancing-other proof-done-advancing-other1570,61841
-(defun proof-segment-up-to-parser proof-segment-up-to-parser1598,62821
-(defun proof-script-generic-parse-find-comment-end proof-script-generic-parse-find-comment-end1661,64897
-(defun proof-script-generic-parse-cmdend proof-script-generic-parse-cmdend1670,65313
-(defun proof-script-generic-parse-cmdstart proof-script-generic-parse-cmdstart1695,66208
-(defun proof-script-generic-parse-sexp proof-script-generic-parse-sexp1758,68916
-(defun proof-cmdstart-add-segment-for-cmd proof-cmdstart-add-segment-for-cmd1782,69852
-(defun proof-segment-up-to-cmdstart proof-segment-up-to-cmdstart1834,72051
-(defun proof-segment-up-to-cmdend proof-segment-up-to-cmdend1895,74411
-(defun proof-semis-to-vanillas proof-semis-to-vanillas1966,77056
-(defun proof-script-new-command-advance proof-script-new-command-advance2005,78382
-(defun proof-script-next-command-advance proof-script-next-command-advance2047,80123
-(defun proof-assert-until-point-interactive proof-assert-until-point-interactive2059,80564
-(defun proof-assert-until-point proof-assert-until-point2085,81686
-(defun proof-assert-next-commandproof-assert-next-command2138,84118
-(defun proof-goto-point proof-goto-point2186,86381
-(defun proof-insert-pbp-command proof-insert-pbp-command2203,86907
-(defun proof-done-retracting proof-done-retracting2235,87980
-(defun proof-setup-retract-action proof-setup-retract-action2262,89091
-(defun proof-last-goal-or-goalsave proof-last-goal-or-goalsave2272,89574
-(defun proof-retract-target proof-retract-target2296,90443
-(defun proof-retract-until-point-interactive proof-retract-until-point-interactive2381,94084
-(defun proof-retract-until-point proof-retract-until-point2389,94469
-(define-derived-mode proof-mode proof-mode2434,96330
-(defun proof-script-set-visited-file-name proof-script-set-visited-file-name2470,97816
-(defun proof-script-set-buffer-hooks proof-script-set-buffer-hooks2494,98818
-(defun proof-script-kill-buffer-fn proof-script-kill-buffer-fn2504,99314
-(defun proof-config-done-related proof-config-done-related2548,101136
-(defun proof-generic-goal-command-p proof-generic-goal-command-p2618,103702
-(defun proof-generic-state-preserving-p proof-generic-state-preserving-p2622,103877
-(defun proof-generic-count-undos proof-generic-count-undos2631,104394
-(defun proof-generic-find-and-forget proof-generic-find-and-forget2660,105424
-(defconst proof-script-important-settingsproof-script-important-settings2711,107249
-(defun proof-config-done proof-config-done2724,107786
-(defun proof-setup-parsing-mechanism proof-setup-parsing-mechanism2821,111334
-(defun proof-setup-imenu proof-setup-imenu2865,113187
-(defun proof-setup-func-menu proof-setup-func-menu2882,113792
-
-generic/proof-shell.el,5288
+(defun proof-goto-end-of-locked-if-pos-not-visible-in-window proof-goto-end-of-locked-if-pos-not-visible-in-window462,16500
+(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window473,16981
+(defun proof-end-of-locked-visible-p proof-end-of-locked-visible-p487,17634
+(defun proof-goto-end-of-queue-or-locked-if-not-visible proof-goto-end-of-queue-or-locked-if-not-visible496,18085
+(defvar pg-idioms pg-idioms515,18735
+(defvar pg-visibility-specs pg-visibility-specs518,18831
+(deflocal pg-script-portions pg-script-portions523,19038
+(defun pg-clear-script-portions pg-clear-script-portions526,19160
+(defun pg-add-script-element pg-add-script-element544,19824
+(defun pg-remove-script-element pg-remove-script-element547,19900
+(defsubst pg-visname pg-visname555,20178
+(defun pg-add-element pg-add-element559,20323
+(defun pg-open-invisible-span pg-open-invisible-span593,21952
+(defun pg-remove-element pg-remove-element604,22315
+(defun pg-make-element-invisible pg-make-element-invisible611,22585
+(defun pg-make-element-visible pg-make-element-visible617,22842
+(defun pg-toggle-element-visibility pg-toggle-element-visibility622,23021
+(defun pg-redisplay-for-gnuemacs pg-redisplay-for-gnuemacs630,23351
+(defun pg-show-all-portions pg-show-all-portions637,23622
+(defun pg-show-all-proofs pg-show-all-proofs655,24293
+(defun pg-hide-all-proofs pg-hide-all-proofs660,24421
+(defun pg-add-proof-element pg-add-proof-element665,24552
+(defun pg-span-name pg-span-name679,25172
+(defun pg-set-span-helphighlights pg-set-span-helphighlights700,25879
+(defun proof-complete-buffer-atomic proof-complete-buffer-atomic725,26703
+(defun proof-register-possibly-new-processed-file proof-register-possibly-new-processed-file766,28618
+(defun proof-inform-prover-file-retracted proof-inform-prover-file-retracted817,30746
+(defun proof-auto-retract-dependencies proof-auto-retract-dependencies836,31532
+(defun proof-unregister-buffer-file-name proof-unregister-buffer-file-name890,34072
+(defun proof-protected-process-or-retract proof-protected-process-or-retract936,35895
+(defun proof-deactivate-scripting-auto proof-deactivate-scripting-auto963,37065
+(defun proof-deactivate-scripting proof-deactivate-scripting972,37423
+(defun proof-activate-scripting proof-activate-scripting1109,42828
+(defun proof-toggle-active-scripting proof-toggle-active-scripting1237,48582
+(defun proof-done-advancing proof-done-advancing1278,49943
+(defun proof-done-advancing-comment proof-done-advancing-comment1363,53348
+(defun proof-done-advancing-save proof-done-advancing-save1382,54090
+(defun proof-make-goalsave proof-make-goalsave1475,57703
+(defun proof-get-name-from-goal proof-get-name-from-goal1490,58446
+(defun proof-done-advancing-autosave proof-done-advancing-autosave1509,59472
+(defun proof-done-advancing-other proof-done-advancing-other1573,61989
+(defun proof-segment-up-to-parser proof-segment-up-to-parser1601,62969
+(defun proof-script-generic-parse-find-comment-end proof-script-generic-parse-find-comment-end1664,65045
+(defun proof-script-generic-parse-cmdend proof-script-generic-parse-cmdend1673,65461
+(defun proof-script-generic-parse-cmdstart proof-script-generic-parse-cmdstart1698,66356
+(defun proof-script-generic-parse-sexp proof-script-generic-parse-sexp1761,69064
+(defun proof-cmdstart-add-segment-for-cmd proof-cmdstart-add-segment-for-cmd1785,70000
+(defun proof-segment-up-to-cmdstart proof-segment-up-to-cmdstart1837,72199
+(defun proof-segment-up-to-cmdend proof-segment-up-to-cmdend1898,74559
+(defun proof-semis-to-vanillas proof-semis-to-vanillas1969,77204
+(defun proof-script-new-command-advance proof-script-new-command-advance2008,78530
+(defun proof-script-next-command-advance proof-script-next-command-advance2050,80271
+(defun proof-assert-until-point-interactive proof-assert-until-point-interactive2062,80712
+(defun proof-assert-until-point proof-assert-until-point2088,81834
+(defun proof-assert-next-commandproof-assert-next-command2141,84266
+(defun proof-goto-point proof-goto-point2189,86529
+(defun proof-insert-pbp-command proof-insert-pbp-command2206,87055
+(defun proof-done-retracting proof-done-retracting2238,88128
+(defun proof-setup-retract-action proof-setup-retract-action2265,89239
+(defun proof-last-goal-or-goalsave proof-last-goal-or-goalsave2275,89722
+(defun proof-retract-target proof-retract-target2299,90591
+(defun proof-retract-until-point-interactive proof-retract-until-point-interactive2384,94232
+(defun proof-retract-until-point proof-retract-until-point2392,94617
+(define-derived-mode proof-mode proof-mode2437,96478
+(defun proof-script-set-visited-file-name proof-script-set-visited-file-name2473,97964
+(defun proof-script-set-buffer-hooks proof-script-set-buffer-hooks2497,98966
+(defun proof-script-kill-buffer-fn proof-script-kill-buffer-fn2507,99462
+(defun proof-config-done-related proof-config-done-related2551,101284
+(defun proof-generic-goal-command-p proof-generic-goal-command-p2621,103850
+(defun proof-generic-state-preserving-p proof-generic-state-preserving-p2625,104025
+(defun proof-generic-count-undos proof-generic-count-undos2634,104542
+(defun proof-generic-find-and-forget proof-generic-find-and-forget2663,105572
+(defconst proof-script-important-settingsproof-script-important-settings2714,107397
+(defun proof-config-done proof-config-done2727,107934
+(defun proof-setup-parsing-mechanism proof-setup-parsing-mechanism2824,111482
+(defun proof-setup-imenu proof-setup-imenu2868,113335
+(defun proof-setup-func-menu proof-setup-func-menu2885,113940
+
+generic/proof-shell.el,5296
 (defvar proof-shell-last-output proof-shell-last-output19,458
 (defvar proof-marker proof-marker63,1714
 (defvar proof-action-list proof-action-list66,1811
@@ -1013,88 +986,86 @@ generic/proof-shell.el,5288
 (defvar proof-shell-urgent-message-scanner proof-shell-urgent-message-scanner615,22050
 (defun proof-shell-handle-output proof-shell-handle-output619,22177
 (defun proof-shell-handle-delayed-output proof-shell-handle-delayed-output693,25514
-(defvar proof-shell-ignore-errors proof-shell-ignore-errors728,26936
-(defun proof-shell-handle-error proof-shell-handle-error734,27138
-(defun proof-shell-handle-interrupt proof-shell-handle-interrupt752,27982
-(defun proof-shell-error-or-interrupt-action proof-shell-error-or-interrupt-action766,28598
-(defun proof-goals-pos proof-goals-pos784,29424
-(defun proof-pbp-focus-on-first-goal proof-pbp-focus-on-first-goal789,29629
-(defsubst proof-shell-string-match-safe proof-shell-string-match-safe801,30164
-(defun proof-shell-process-output proof-shell-process-output806,30332
-(defvar proof-shell-insert-space-fudge proof-shell-insert-space-fudge917,34972
-(defun proof-shell-insert proof-shell-insert926,35281
-(defun proof-shell-command-queue-item proof-shell-command-queue-item994,37815
-(defun proof-shell-set-silent proof-shell-set-silent999,37972
-(defun proof-shell-start-silent-item proof-shell-start-silent-item1005,38191
-(defun proof-shell-clear-silent proof-shell-clear-silent1011,38383
-(defun proof-shell-stop-silent-item proof-shell-stop-silent-item1017,38605
-(defun proof-shell-should-be-silent proof-shell-should-be-silent1024,38877
-(defun proof-append-alist proof-append-alist1037,39433
-(defun proof-start-queue proof-start-queue1093,41560
-(defun proof-extend-queue proof-extend-queue1104,41909
-(defun proof-shell-exec-loop proof-shell-exec-loop1115,42290
-(defun proof-shell-insert-loopback-cmd proof-shell-insert-loopback-cmd1177,44757
-(defun proof-shell-message proof-shell-message1215,46480
-(defun proof-shell-process-urgent-message proof-shell-process-urgent-message1221,46696
-(defvar proof-shell-minibuffer-urgent-interactive-input-history proof-shell-minibuffer-urgent-interactive-input-history1432,55614
-(defun proof-shell-minibuffer-urgent-interactive-input proof-shell-minibuffer-urgent-interactive-input1434,55684
-(defun proof-shell-process-urgent-messages proof-shell-process-urgent-messages1446,56054
-(defun proof-shell-filter proof-shell-filter1515,59110
-(defun proof-shell-filter-process-output proof-shell-filter-process-output1668,65447
-(defvar pg-last-tracing-output-time pg-last-tracing-output-time1721,67501
-(defvar pg-tracing-slow-mode pg-tracing-slow-mode1724,67607
-(defconst pg-slow-mode-duration pg-slow-mode-duration1727,67696
-(defconst pg-fast-tracing-mode-threshold pg-fast-tracing-mode-threshold1730,67778
-(defvar pg-tracing-cleanup-timer pg-tracing-cleanup-timer1733,67906
-(defun pg-tracing-tight-loop pg-tracing-tight-loop1735,67945
-(defun pg-finish-tracing-display pg-finish-tracing-display1778,69698
-(defun proof-shell-dont-show-annotations proof-shell-dont-show-annotations1789,69968
-(defun proof-shell-show-annotations proof-shell-show-annotations1805,70503
-(defun proof-shell-wait proof-shell-wait1826,71000
-(defun proof-done-invisible proof-done-invisible1846,71910
-(defun proof-shell-invisible-command proof-shell-invisible-command1889,73633
-(defun proof-shell-invisible-cmd-get-result proof-shell-invisible-cmd-get-result1922,74883
-(defun proof-shell-invisible-command-invisible-result proof-shell-invisible-command-invisible-result1939,75564
-(define-derived-mode proof-shell-mode proof-shell-mode1959,76068
-(defconst proof-shell-important-settingsproof-shell-important-settings2029,78671
-(defun proof-shell-config-done proof-shell-config-done2034,78771
-
-generic/proof-site.el,1154
-(defgroup proof-general proof-general20,593
-(defgroup proof-general-internals proof-general-internals33,1009
-(defun proof-home-directory-fn proof-home-directory-fn42,1202
-(defcustom proof-home-directoryproof-home-directory53,1572
-(defcustom proof-images-directoryproof-images-directory62,1938
-(defcustom proof-info-directoryproof-info-directory68,2139
-(defcustom proof-assistant-tableproof-assistant-table97,3388
-(defun proof-string-to-list proof-string-to-list156,5375
-(defcustom proof-assistants proof-assistants172,5866
-(defun proof-ready-for-assistant proof-ready-for-assistant220,7691
-(defconst proof-general-version proof-general-version335,11984
-(defcustom proof-assistant-cusgrp proof-assistant-cusgrp350,12549
-(defcustom proof-assistant-internals-cusgrp proof-assistant-internals-cusgrp358,12852
-(defcustom proof-assistant proof-assistant366,13164
-(defcustom proof-assistant-symbol proof-assistant-symbol374,13433
-(defvar proof-running-on-XEmacs proof-running-on-XEmacs391,13981
-(defvar proof-running-on-Emacs21 proof-running-on-Emacs21393,14103
-(defvar proof-running-on-win32 proof-running-on-win32397,14350
+(defvar proof-shell-no-error-display proof-shell-no-error-display728,26936
+(defun proof-shell-handle-error proof-shell-handle-error734,27142
+(defun proof-shell-handle-interrupt proof-shell-handle-interrupt752,27978
+(defun proof-shell-error-or-interrupt-action proof-shell-error-or-interrupt-action766,28600
+(defun proof-goals-pos proof-goals-pos793,29805
+(defun proof-pbp-focus-on-first-goal proof-pbp-focus-on-first-goal798,30010
+(defsubst proof-shell-string-match-safe proof-shell-string-match-safe810,30545
+(defun proof-shell-process-output proof-shell-process-output815,30713
+(defvar proof-shell-insert-space-fudge proof-shell-insert-space-fudge926,35353
+(defun proof-shell-insert proof-shell-insert935,35662
+(defun proof-shell-command-queue-item proof-shell-command-queue-item1003,38196
+(defun proof-shell-set-silent proof-shell-set-silent1008,38353
+(defun proof-shell-start-silent-item proof-shell-start-silent-item1014,38572
+(defun proof-shell-clear-silent proof-shell-clear-silent1020,38764
+(defun proof-shell-stop-silent-item proof-shell-stop-silent-item1026,38986
+(defun proof-shell-should-be-silent proof-shell-should-be-silent1033,39258
+(defun proof-append-alist proof-append-alist1046,39814
+(defun proof-start-queue proof-start-queue1102,41941
+(defun proof-extend-queue proof-extend-queue1113,42290
+(defun proof-shell-exec-loop proof-shell-exec-loop1124,42671
+(defun proof-shell-insert-loopback-cmd proof-shell-insert-loopback-cmd1189,45259
+(defun proof-shell-message proof-shell-message1227,46982
+(defun proof-shell-process-urgent-message proof-shell-process-urgent-message1233,47198
+(defvar proof-shell-minibuffer-urgent-interactive-input-history proof-shell-minibuffer-urgent-interactive-input-history1442,56063
+(defun proof-shell-minibuffer-urgent-interactive-input proof-shell-minibuffer-urgent-interactive-input1444,56133
+(defun proof-shell-process-urgent-messages proof-shell-process-urgent-messages1456,56503
+(defun proof-shell-filter proof-shell-filter1525,59559
+(defun proof-shell-filter-process-output proof-shell-filter-process-output1678,65896
+(defvar pg-last-tracing-output-time pg-last-tracing-output-time1731,67950
+(defvar pg-tracing-slow-mode pg-tracing-slow-mode1734,68056
+(defconst pg-slow-mode-duration pg-slow-mode-duration1737,68145
+(defconst pg-fast-tracing-mode-threshold pg-fast-tracing-mode-threshold1740,68227
+(defvar pg-tracing-cleanup-timer pg-tracing-cleanup-timer1743,68355
+(defun pg-tracing-tight-loop pg-tracing-tight-loop1745,68394
+(defun pg-finish-tracing-display pg-finish-tracing-display1788,70112
+(defun proof-shell-dont-show-annotations proof-shell-dont-show-annotations1801,70418
+(defun proof-shell-show-annotations proof-shell-show-annotations1817,70953
+(defun proof-shell-wait proof-shell-wait1838,71450
+(defun proof-done-invisible proof-done-invisible1858,72360
+(defun proof-shell-invisible-command proof-shell-invisible-command1901,74083
+(defun proof-shell-invisible-cmd-get-result proof-shell-invisible-cmd-get-result1934,75333
+(defun proof-shell-invisible-command-invisible-result proof-shell-invisible-command-invisible-result1951,76014
+(define-derived-mode proof-shell-mode proof-shell-mode1971,76518
+(defconst proof-shell-important-settingsproof-shell-important-settings2039,79071
+(defun proof-shell-config-done proof-shell-config-done2044,79171
+
+generic/proof-site.el,1030
+(defgroup proof-general proof-general20,594
+(defgroup proof-general-internals proof-general-internals33,1010
+(defun proof-home-directory-fn proof-home-directory-fn42,1203
+(defcustom proof-home-directoryproof-home-directory53,1573
+(defcustom proof-images-directoryproof-images-directory62,1939
+(defcustom proof-info-directoryproof-info-directory68,2140
+(defcustom proof-assistant-tableproof-assistant-table97,3389
+(defun proof-string-to-list proof-string-to-list163,5568
+(defcustom proof-assistants proof-assistants179,6059
+(defun proof-ready-for-assistant proof-ready-for-assistant215,7472
+(defconst proof-general-version proof-general-version328,11681
+(defconst proof-general-short-version proof-general-short-version331,11824
+(defcustom proof-assistant-cusgrp proof-assistant-cusgrp348,12406
+(defcustom proof-assistant-internals-cusgrp proof-assistant-internals-cusgrp356,12709
+(defcustom proof-assistant proof-assistant364,13021
+(defcustom proof-assistant-symbol proof-assistant-symbol372,13290
 
 generic/proof-splash.el,976
 (defcustom proof-splash-enable proof-splash-enable14,379
 (defcustom proof-splash-time proof-splash-time19,531
 (defcustom proof-splash-contentsproof-splash-contents27,816
-(defconst proof-splash-startup-msg proof-splash-startup-msg59,1970
-(defconst proof-splash-welcome proof-splash-welcome68,2349
-(defun proof-get-image proof-get-image87,2913
-(defvar proof-splash-timeout-conf proof-splash-timeout-conf139,4737
-(defun proof-splash-centre-spaces proof-splash-centre-spaces142,4850
-(defun proof-splash-remove-screen proof-splash-remove-screen170,6019
-(defun proof-splash-remove-buffer proof-splash-remove-buffer191,6736
-(defvar proof-splash-seen proof-splash-seen207,7400
-(defun proof-splash-display-screen proof-splash-display-screen211,7517
-(defun proof-splash-message proof-splash-message286,10676
-(defun proof-splash-timeout-waiter proof-splash-timeout-waiter296,11039
-(defun proof-splash-set-frame-titles proof-splash-set-frame-titles313,11778
+(defconst proof-splash-startup-msg proof-splash-startup-msg56,1895
+(defconst proof-splash-welcome proof-splash-welcome65,2274
+(defun proof-get-image proof-get-image84,2838
+(defvar proof-splash-timeout-conf proof-splash-timeout-conf136,4662
+(defun proof-splash-centre-spaces proof-splash-centre-spaces139,4775
+(defun proof-splash-remove-screen proof-splash-remove-screen167,5944
+(defun proof-splash-remove-buffer proof-splash-remove-buffer188,6661
+(defvar proof-splash-seen proof-splash-seen204,7325
+(defun proof-splash-display-screen proof-splash-display-screen208,7442
+(defun proof-splash-message proof-splash-message283,10601
+(defun proof-splash-timeout-waiter proof-splash-timeout-waiter293,10964
+(defun proof-splash-set-frame-titles proof-splash-set-frame-titles310,11703
 
 generic/proof-syntax.el,1296
 (defun proof-ids-to-regexp proof-ids-to-regexp16,445
@@ -1181,7 +1152,7 @@ generic/proof-toolbar.el,3888
 (defun proof-toolbar-make-menu-item proof-toolbar-make-menu-item558,16193
 (defconst proof-toolbar-scripting-menuproof-toolbar-scripting-menu580,16881
 
-generic/proof-utils.el,3092
+generic/proof-utils.el,3150
 (defmacro deflocal deflocal18,471
 (defmacro proof-with-current-buffer-if-exists proof-with-current-buffer-if-exists25,709
 (defmacro proof-with-script-buffer proof-with-script-buffer34,1086
@@ -1211,145 +1182,44 @@ generic/proof-utils.el,3092
 (defun proof-font-lock-clear-font-lock-vars proof-font-lock-clear-font-lock-vars387,13915
 (defun proof-font-lock-set-font-lock-vars proof-font-lock-set-font-lock-vars398,14288
 (defun proof-fontify-region proof-fontify-region405,14501
-(defconst pg-special-char-regexp pg-special-char-regexp459,16467
-(defun pg-remove-specials pg-remove-specials463,16579
-(defun proof-fontify-buffer proof-fontify-buffer477,17004
-(defun proof-warn-if-unset proof-warn-if-unset490,17245
-(defun proof-get-window-for-buffer proof-get-window-for-buffer495,17463
-(defun proof-display-and-keep-buffer proof-display-and-keep-buffer532,19115
-(defun proof-clean-buffer proof-clean-buffer563,20391
-(defun proof-message proof-message575,20869
-(defun proof-warning proof-warning580,21082
-(defun proof-debug proof-debug587,21416
-(defun proof-switch-to-buffer proof-switch-to-buffer600,21907
-(defun proof-resize-window-tofit proof-resize-window-tofit633,23599
-(defun proof-submit-bug-report proof-submit-bug-report733,27627
-(defun proof-deftoggle-fn proof-deftoggle-fn756,28406
-(defmacro proof-deftoggle proof-deftoggle771,29061
-(defun proof-defintset-fn proof-defintset-fn778,29435
-(defmacro proof-defintset proof-defintset792,30090
-(defun proof-defstringset-fn proof-defstringset-fn799,30467
-(defmacro proof-defstringset proof-defstringset812,31094
-(defun pg-custom-save-vars pg-custom-save-vars826,31559
-(defun pg-custom-reset-vars pg-custom-reset-vars844,32285
-(defun proof-locate-executable proof-locate-executable857,32622
-(defconst proof-extra-flsproof-extra-fls889,34035
+(defconst pg-special-char-regexp pg-special-char-regexp464,16730
+(defun pg-remove-specials pg-remove-specials468,16842
+(defun proof-fontify-buffer proof-fontify-buffer482,17267
+(defun proof-warn-if-unset proof-warn-if-unset495,17508
+(defun proof-get-window-for-buffer proof-get-window-for-buffer500,17726
+(defun proof-display-and-keep-buffer proof-display-and-keep-buffer537,19378
+(defun proof-clean-buffer proof-clean-buffer568,20654
+(defun proof-message proof-message582,21191
+(defun proof-warning proof-warning587,21404
+(defun pg-internal-warning pg-internal-warning593,21686
+(defun proof-debug proof-debug601,22005
+(defun proof-switch-to-buffer proof-switch-to-buffer616,22678
+(defun proof-resize-window-tofit proof-resize-window-tofit649,24370
+(defun proof-submit-bug-report proof-submit-bug-report749,28398
+(defun proof-deftoggle-fn proof-deftoggle-fn773,29200
+(defmacro proof-deftoggle proof-deftoggle788,29855
+(defun proof-defintset-fn proof-defintset-fn795,30229
+(defmacro proof-defintset proof-defintset809,30884
+(defun proof-defstringset-fn proof-defstringset-fn816,31261
+(defmacro proof-defstringset proof-defstringset829,31888
+(defun pg-custom-save-vars pg-custom-save-vars843,32353
+(defun pg-custom-reset-vars pg-custom-reset-vars861,33079
+(defun proof-locate-executable proof-locate-executable874,33416
+(defconst proof-extra-flsproof-extra-fls906,34829
 
 generic/proof-x-symbol.el,960
-(defvar proof-x-symbol-initialized proof-x-symbol-initialized53,2149
-(defun proof-x-symbol-tokenlang-file proof-x-symbol-tokenlang-file56,2244
-(defun proof-x-symbol-support-maybe-available proof-x-symbol-support-maybe-available62,2426
-(defun proof-x-symbol-initialize proof-x-symbol-initialize82,3171
-(defun proof-x-symbol-enable proof-x-symbol-enable177,7034
-(defun proof-x-symbol-refresh-output-buffers proof-x-symbol-refresh-output-buffers199,8003
-(defun proof-x-symbol-mode-associated-buffers proof-x-symbol-mode-associated-buffers214,8757
-(defalias 'proof-x-symbol-decode-region proof-x-symbol-decode-region236,9461
-(defun proof-x-symbol-encode-shell-input proof-x-symbol-encode-shell-input238,9527
-(defun proof-x-symbol-set-language proof-x-symbol-set-language255,10118
-(defun proof-x-symbol-shell-config proof-x-symbol-shell-config260,10289
-(defun proof-x-symbol-config-output-buffer proof-x-symbol-config-output-buffer308,12456
-
-generic/span.el,192
-(defsubst delete-spans delete-spans22,471
-(defsubst span-property-safe span-property-safe26,625
-(defsubst set-span-start set-span-start30,764
-(defsubst set-span-end set-span-end34,896
-
-generic/span-extent.el,1346
-(defsubst make-span make-span16,557
-(defsubst detach-span detach-span20,679
-(defsubst set-span-endpoints set-span-endpoints24,766
-(defsubst set-span-property set-span-property28,899
-(defsubst span-read-only span-read-only32,1026
-(defsubst span-read-write span-read-write36,1130
-(defun span-give-warning span-give-warning40,1237
-(defun span-write-warning span-write-warning44,1335
-(defsubst span-property span-property49,1535
-(defsubst delete-span delete-span53,1650
-(defsubst mapcar-spans mapcar-spans59,1821
-(defsubst span-at span-at63,2027
-(defsubst span-at-before span-at-before67,2144
-(defsubst span-start span-start72,2341
-(defsubst span-end span-end76,2470
-(defsubst prev-span prev-span80,2593
-(defsubst next-span next-span84,2739
-(defsubst span-live-p span-live-p88,2881
-(defun span-raise span-raise96,3153
-(defalias 'span-object span-object100,3252
-(defalias 'span-string span-string101,3291
-(defsubst make-detached-span make-detached-span104,3377
-(defsubst span-buffer span-buffer110,3474
-(defsubst span-detached-p span-detached-p115,3566
-(defsubst set-span-face set-span-face120,3678
-(defsubst fold-spans fold-spans125,3774
-(defsubst set-span-properties set-span-properties130,3972
-(defsubst set-span-keymap set-span-keymap135,4081
-(defsubst span-at-event span-at-event140,4196
-
-generic/span-overlay.el,2198
-(defvar before-list before-list20,771
-(defun foldr foldr27,906
-(defun foldl foldl39,1239
-(defsubst span-start span-start51,1556
-(defsubst span-end span-end55,1648
-(defun set-span-property set-span-property59,1734
-(defsubst span-property span-property63,1850
-(defun span-read-only-hook span-read-only-hook67,1961
-(defun span-read-only span-read-only71,2093
-(defun span-read-write span-read-write86,2871
-(defun span-give-warning span-give-warning92,3090
-(defun span-write-warning span-write-warning96,3198
-(defun int-nil-lt int-nil-lt101,3421
-(defun span-lt span-lt110,3624
-(defun span-traverse span-traverse115,3783
-(defun add-span add-span131,4230
-(defun make-span make-span145,4632
-(defun remove-span remove-span149,4763
-(defun spans-at-point spans-at-point162,5216
-(defun append-unique append-unique176,5696
-(defun spans-at-region spans-at-region179,5783
-(defun spans-at-point-prop spans-at-point-prop186,6005
-(defun spans-at-region-prop spans-at-region-prop194,6255
-(defun span-at span-at206,6602
-(defsubst detach-span detach-span212,6816
-(defsubst delete-span delete-span218,6943
-(defsubst set-span-endpoints set-span-endpoints226,7186
-(defsubst mapcar-spans mapcar-spans233,7402
-(defun map-spans-aux map-spans-aux237,7606
-(defsubst map-spans map-spans241,7721
-(defun find-span-aux find-span-aux244,7779
-(defun find-span find-span249,7905
-(defun span-at-before span-at-before252,7970
-(defun prev-span prev-span265,8412
-(defun next-span next-span274,8694
-(defsubst span-live-p span-live-p299,9678
-(defun span-raise span-raise305,9844
-(defalias 'span-object span-object311,10075
-(defun span-string span-string313,10116
-(defun set-span-properties set-span-properties319,10298
-(defun span-find-span span-find-span331,10553
-(defsubst span-at-event span-at-event342,10912
-(defun make-detached-span make-detached-span347,11036
-(defun fold-spans-aux fold-spans-aux353,11170
-(defun fold-spans fold-spans361,11426
-(defsubst span-buffer span-buffer368,11634
-(defsubst span-detached-p span-detached-p373,11726
-(defsubst set-span-face set-span-face381,11922
-(defsubst set-span-keymap set-span-keymap386,12022
-
-generic/texi-docstring-magic.el,958
-(defun texi-docstring-magic-find-face texi-docstring-magic-find-face85,2996
-(defun texi-docstring-magic-splice-sep texi-docstring-magic-splice-sep90,3161
-(defconst texi-docstring-magic-munge-tabletexi-docstring-magic-munge-table100,3466
-(defun texi-docstring-magic-untabify texi-docstring-magic-untabify190,7185
-(defun texi-docstring-magic-munge-docstring texi-docstring-magic-munge-docstring200,7500
-(defun texi-docstring-magic-texi texi-docstring-magic-texi239,8787
-(defun texi-docstring-magic-format-default texi-docstring-magic-format-default252,9227
-(defun texi-docstring-magic-texi-for texi-docstring-magic-texi-for268,9862
-(defconst texi-docstring-magic-commenttexi-docstring-magic-comment326,11822
-(defun texi-docstring-magic texi-docstring-magic332,11976
-(defun texi-docstring-magic-face-at-point texi-docstring-magic-face-at-point366,13056
-(defun texi-docstring-magic-insert-magic texi-docstring-magic-insert-magic381,13579
+(defvar proof-x-symbol-initialized proof-x-symbol-initialized54,2151
+(defun proof-x-symbol-tokenlang-file proof-x-symbol-tokenlang-file57,2246
+(defun proof-x-symbol-support-maybe-available proof-x-symbol-support-maybe-available63,2428
+(defun proof-x-symbol-initialize proof-x-symbol-initialize83,3173
+(defun proof-x-symbol-enable proof-x-symbol-enable178,7036
+(defun proof-x-symbol-refresh-output-buffers proof-x-symbol-refresh-output-buffers200,8005
+(defun proof-x-symbol-mode-associated-buffers proof-x-symbol-mode-associated-buffers215,8759
+(defalias 'proof-x-symbol-decode-region proof-x-symbol-decode-region237,9463
+(defun proof-x-symbol-encode-shell-input proof-x-symbol-encode-shell-input239,9529
+(defun proof-x-symbol-set-language proof-x-symbol-set-language256,10120
+(defun proof-x-symbol-shell-config proof-x-symbol-shell-config261,10291
+(defun proof-x-symbol-config-output-buffer proof-x-symbol-config-output-buffer309,12458
 
 hol98/hol98.el,0
 
@@ -1447,11 +1317,11 @@ isa/isa.el,2283
 (defun isa-state-preserving-p isa-state-preserving-p550,20655
 (defun isa-pre-shell-start isa-pre-shell-start559,21023
 (defun isa-mode-config isa-mode-config566,21300
-(defun isa-shell-mode-config isa-shell-mode-config593,22373
-(defun isa-response-mode-config isa-response-mode-config600,22622
-(defun isa-goals-mode-config isa-goals-mode-config605,22783
-(defun isa-preprocessing isa-preprocessing613,23107
-(defpgdefault completion-tablecompletion-table627,23611
+(defun isa-shell-mode-config isa-shell-mode-config594,22443
+(defun isa-response-mode-config isa-response-mode-config601,22692
+(defun isa-goals-mode-config isa-goals-mode-config606,22853
+(defun isa-preprocessing isa-preprocessing614,23177
+(defpgdefault completion-tablecompletion-table628,23681
 
 isa/isa-syntax.el,3046
 (defun isa-init-syntax-table isa-init-syntax-table14,312
@@ -1599,36 +1469,36 @@ isa/x-symbol-isabelle.el,3169
 isa/x-symbol-isa.el,0
 
 isar/isar.el,1883
-(defcustom isar-keywords-name isar-keywords-name28,631
-(defpgdefault completion-table completion-table45,1155
-(defcustom isar-web-pageisar-web-page47,1208
-(defun isar-detect-header isar-detect-header65,1572
-(defun isar-strip-terminators isar-strip-terminators100,2835
-(defun isar-markup-ml isar-markup-ml113,3206
-(defun isar-mode-config-set-variables isar-mode-config-set-variables118,3341
-(defun isar-shell-mode-config-set-variables isar-shell-mode-config-set-variables182,6172
-(defun isar-remove-file isar-remove-file296,10961
-(defun isar-shell-compute-new-files-list isar-shell-compute-new-files-list306,11324
-(defun isar-activate-scripting isar-activate-scripting317,11790
-(define-derived-mode isar-shell-mode isar-shell-mode326,11960
-(define-derived-mode isar-response-mode isar-response-mode331,12083
-(define-derived-mode isar-goals-mode isar-goals-mode336,12265
-(define-derived-mode isar-mode isar-mode341,12440
-(defpgdefault menu-entriesmenu-entries374,13796
-(defun isar-count-undos isar-count-undos398,14818
-(defun isar-find-and-forget isar-find-and-forget424,15919
-(defun isar-goal-command-p isar-goal-command-p471,17764
-(defun isar-global-save-command-p isar-global-save-command-p475,17896
-(defvar isar-current-goal isar-current-goal496,18733
-(defun isar-state-preserving-p isar-state-preserving-p499,18799
-(defvar isar-shell-current-line-width isar-shell-current-line-width522,19833
-(defun isar-shell-adjust-line-width isar-shell-adjust-line-width528,20051
-(defun isar-pre-shell-start isar-pre-shell-start548,20934
-(defun isar-preprocessing isar-preprocessing560,21270
-(defun isar-mode-config isar-mode-config583,22481
-(defun isar-shell-mode-config isar-shell-mode-config594,22984
-(defun isar-response-mode-config isar-response-mode-config605,23354
-(defun isar-goals-mode-config isar-goals-mode-config614,23611
+(defcustom isar-keywords-name isar-keywords-name28,630
+(defpgdefault completion-table completion-table45,1154
+(defcustom isar-web-pageisar-web-page47,1207
+(defun isar-detect-header isar-detect-header65,1571
+(defun isar-strip-terminators isar-strip-terminators100,2834
+(defun isar-markup-ml isar-markup-ml113,3205
+(defun isar-mode-config-set-variables isar-mode-config-set-variables118,3340
+(defun isar-shell-mode-config-set-variables isar-shell-mode-config-set-variables182,6171
+(defun isar-remove-file isar-remove-file296,10966
+(defun isar-shell-compute-new-files-list isar-shell-compute-new-files-list306,11329
+(defun isar-activate-scripting isar-activate-scripting317,11795
+(define-derived-mode isar-shell-mode isar-shell-mode326,11965
+(define-derived-mode isar-response-mode isar-response-mode331,12088
+(define-derived-mode isar-goals-mode isar-goals-mode336,12270
+(define-derived-mode isar-mode isar-mode341,12445
+(defpgdefault menu-entriesmenu-entries388,14264
+(defun isar-count-undos isar-count-undos419,15622
+(defun isar-find-and-forget isar-find-and-forget445,16723
+(defun isar-goal-command-p isar-goal-command-p492,18568
+(defun isar-global-save-command-p isar-global-save-command-p496,18700
+(defvar isar-current-goal isar-current-goal517,19537
+(defun isar-state-preserving-p isar-state-preserving-p520,19603
+(defvar isar-shell-current-line-width isar-shell-current-line-width543,20637
+(defun isar-shell-adjust-line-width isar-shell-adjust-line-width549,20855
+(defun isar-pre-shell-start isar-pre-shell-start569,21738
+(defun isar-preprocessing isar-preprocessing581,22074
+(defun isar-mode-config isar-mode-config604,23285
+(defun isar-shell-mode-config isar-shell-mode-config616,23855
+(defun isar-response-mode-config isar-response-mode-config627,24225
+(defun isar-goals-mode-config isar-goals-mode-config636,24482
 
 isar/isar-keywords.el,1650
 (defconst isar-keywords-majorisar-keywords-major14,378
@@ -1660,83 +1530,83 @@ isar/isar-mmm.el,129
 (defconst isar-start-latex-regexp isar-start-latex-regexp23,697
 (defconst isar-start-sml-regexp isar-start-sml-regexp35,1130
 
-isar/isar-syntax.el,4918
+isar/isar-syntax.el,4921
 (defconst isar-script-syntax-table-entries isar-script-syntax-table-entries18,414
-(defconst isar-script-syntax-table-alistisar-script-syntax-table-alist57,1326
-(defun isar-init-syntax-table isar-init-syntax-table66,1609
-(defun isar-init-output-syntax-table isar-init-output-syntax-table74,1857
-(defconst isar-keywords-theory-encloseisar-keywords-theory-enclose89,2272
-(defconst isar-keywords-theoryisar-keywords-theory94,2424
-(defconst isar-keywords-saveisar-keywords-save99,2569
-(defconst isar-keywords-proof-encloseisar-keywords-proof-enclose104,2698
-(defconst isar-keywords-proofisar-keywords-proof110,2880
-(defconst isar-keywords-proof-contextisar-keywords-proof-context117,3078
-(defconst isar-keywords-local-goalisar-keywords-local-goal121,3192
-(defconst isar-keywords-improperisar-keywords-improper125,3304
-(defconst isar-keywords-outlineisar-keywords-outline130,3443
-(defconst isar-keywords-fumeisar-keywords-fume133,3508
-(defconst isar-keywords-indent-openisar-keywords-indent-open140,3726
-(defconst isar-keywords-indent-closeisar-keywords-indent-close146,3910
-(defconst isar-keywords-indent-encloseisar-keywords-indent-enclose150,4015
-(defun isar-regexp-simple-alt isar-regexp-simple-alt158,4194
-(defun isar-ids-to-regexp isar-ids-to-regexp178,4955
-(defconst isar-ext-first isar-ext-first212,6223
-(defconst isar-ext-rest isar-ext-rest213,6290
-(defconst isar-long-id-stuff isar-long-id-stuff215,6362
-(defconst isar-id isar-id216,6436
-(defconst isar-idx isar-idx217,6506
-(defconst isar-string isar-string219,6565
-(defconst isar-any-command-regexpisar-any-command-regexp221,6627
-(defconst isar-name-regexpisar-name-regexp225,6761
-(defconst isar-tac-regexpisar-tac-regexp229,6930
-(defconst isar-save-command-regexpisar-save-command-regexp233,7038
-(defconst isar-global-save-command-regexpisar-global-save-command-regexp236,7139
-(defconst isar-goal-command-regexpisar-goal-command-regexp239,7253
-(defconst isar-local-goal-command-regexpisar-local-goal-command-regexp242,7361
-(defconst isar-comment-start isar-comment-start245,7474
-(defconst isar-comment-end isar-comment-end246,7509
-(defconst isar-comment-start-regexp isar-comment-start-regexp247,7542
-(defconst isar-comment-end-regexp isar-comment-end-regexp248,7613
-(defconst isar-string-start-regexp isar-string-start-regexp250,7681
-(defconst isar-string-end-regexp isar-string-end-regexp251,7729
-(defconst isar-antiq-regexpisar-antiq-regexp260,7979
-(defface isabelle-class-name-faceisabelle-class-name-face267,8159
-(defface isabelle-tfree-name-faceisabelle-tfree-name-face277,8434
-(defface isabelle-tvar-name-faceisabelle-tvar-name-face287,8715
-(defface isabelle-free-name-faceisabelle-free-name-face297,8995
-(defface isabelle-bound-name-faceisabelle-bound-name-face307,9271
-(defface isabelle-var-name-faceisabelle-var-name-face317,9550
-(defconst isabelle-class-name-face isabelle-class-name-face327,9829
-(defconst isabelle-tfree-name-face isabelle-tfree-name-face328,9891
-(defconst isabelle-tvar-name-face isabelle-tvar-name-face329,9953
-(defconst isabelle-free-name-face isabelle-free-name-face330,10014
-(defconst isabelle-bound-name-face isabelle-bound-name-face331,10075
-(defconst isabelle-var-name-face isabelle-var-name-face332,10137
-(defvar isar-font-lock-keywords-1isar-font-lock-keywords-1334,10198
-(defvar isar-output-font-lock-keywords-1isar-output-font-lock-keywords-1348,11127
-(defvar isar-goals-font-lock-keywordsisar-goals-font-lock-keywords360,11783
-(defconst isar-undo isar-undo391,12417
-(defconst isar-kill isar-kill392,12479
-(defun isar-remove isar-remove394,12509
-(defun isar-undos isar-undos397,12588
-(defun isar-cannot-undo isar-cannot-undo401,12694
-(defconst isar-undo-fail-regexpisar-undo-fail-regexp405,12765
-(defconst isar-undo-skip-regexpisar-undo-skip-regexp409,12903
-(defconst isar-undo-ignore-regexpisar-undo-ignore-regexp412,13024
-(defconst isar-undo-remove-regexpisar-undo-remove-regexp415,13089
-(defconst isar-undo-kill-regexpisar-undo-kill-regexp420,13229
-(defconst isar-any-entity-regexpisar-any-entity-regexp426,13371
-(defconst isar-named-entity-regexpisar-named-entity-regexp431,13558
-(defconst isar-unnamed-entity-regexpisar-unnamed-entity-regexp436,13735
-(defconst isar-next-entity-regexpsisar-next-entity-regexps439,13837
-(defconst isar-generic-expressionisar-generic-expression447,14144
-(defconst isar-indent-any-regexpisar-indent-any-regexp458,14378
-(defconst isar-indent-inner-regexpisar-indent-inner-regexp460,14471
-(defconst isar-indent-enclose-regexpisar-indent-enclose-regexp462,14537
-(defconst isar-indent-open-regexpisar-indent-open-regexp464,14653
-(defconst isar-indent-close-regexpisar-indent-close-regexp466,14763
-(defconst isar-outline-regexpisar-outline-regexp472,14900
-(defconst isar-outline-heading-end-regexp isar-outline-heading-end-regexp476,15053
+(defconst isar-script-syntax-table-alistisar-script-syntax-table-alist58,1362
+(defun isar-init-syntax-table isar-init-syntax-table67,1645
+(defun isar-init-output-syntax-table isar-init-output-syntax-table75,1893
+(defconst isar-keywords-theory-encloseisar-keywords-theory-enclose90,2308
+(defconst isar-keywords-theoryisar-keywords-theory95,2460
+(defconst isar-keywords-saveisar-keywords-save100,2605
+(defconst isar-keywords-proof-encloseisar-keywords-proof-enclose105,2734
+(defconst isar-keywords-proofisar-keywords-proof111,2916
+(defconst isar-keywords-proof-contextisar-keywords-proof-context118,3114
+(defconst isar-keywords-local-goalisar-keywords-local-goal122,3228
+(defconst isar-keywords-improperisar-keywords-improper126,3340
+(defconst isar-keywords-outlineisar-keywords-outline131,3479
+(defconst isar-keywords-fumeisar-keywords-fume134,3544
+(defconst isar-keywords-indent-openisar-keywords-indent-open141,3762
+(defconst isar-keywords-indent-closeisar-keywords-indent-close147,3946
+(defconst isar-keywords-indent-encloseisar-keywords-indent-enclose151,4051
+(defun isar-regexp-simple-alt isar-regexp-simple-alt159,4230
+(defun isar-ids-to-regexp isar-ids-to-regexp179,4991
+(defconst isar-ext-first isar-ext-first213,6259
+(defconst isar-ext-rest isar-ext-rest214,6326
+(defconst isar-long-id-stuff isar-long-id-stuff216,6398
+(defconst isar-id isar-id217,6472
+(defconst isar-idx isar-idx218,6542
+(defconst isar-string isar-string220,6601
+(defconst isar-any-command-regexpisar-any-command-regexp222,6661
+(defconst isar-name-regexpisar-name-regexp226,6795
+(defconst isar-tac-regexpisar-tac-regexp232,7090
+(defconst isar-save-command-regexpisar-save-command-regexp236,7198
+(defconst isar-global-save-command-regexpisar-global-save-command-regexp239,7299
+(defconst isar-goal-command-regexpisar-goal-command-regexp242,7413
+(defconst isar-local-goal-command-regexpisar-local-goal-command-regexp245,7521
+(defconst isar-comment-start isar-comment-start248,7634
+(defconst isar-comment-end isar-comment-end249,7669
+(defconst isar-comment-start-regexp isar-comment-start-regexp250,7702
+(defconst isar-comment-end-regexp isar-comment-end-regexp251,7773
+(defconst isar-string-start-regexp isar-string-start-regexp253,7841
+(defconst isar-string-end-regexp isar-string-end-regexp254,7889
+(defconst isar-antiq-regexpisar-antiq-regexp263,8139
+(defface isabelle-class-name-faceisabelle-class-name-face270,8319
+(defface isabelle-tfree-name-faceisabelle-tfree-name-face280,8594
+(defface isabelle-tvar-name-faceisabelle-tvar-name-face290,8875
+(defface isabelle-free-name-faceisabelle-free-name-face300,9155
+(defface isabelle-bound-name-faceisabelle-bound-name-face310,9431
+(defface isabelle-var-name-faceisabelle-var-name-face320,9710
+(defconst isabelle-class-name-face isabelle-class-name-face330,9989
+(defconst isabelle-tfree-name-face isabelle-tfree-name-face331,10051
+(defconst isabelle-tvar-name-face isabelle-tvar-name-face332,10113
+(defconst isabelle-free-name-face isabelle-free-name-face333,10174
+(defconst isabelle-bound-name-face isabelle-bound-name-face334,10235
+(defconst isabelle-var-name-face isabelle-var-name-face335,10297
+(defvar isar-font-lock-keywords-1isar-font-lock-keywords-1337,10358
+(defvar isar-output-font-lock-keywords-1isar-output-font-lock-keywords-1351,11287
+(defvar isar-goals-font-lock-keywordsisar-goals-font-lock-keywords365,12077
+(defconst isar-undo isar-undo396,12711
+(defconst isar-kill isar-kill397,12773
+(defun isar-remove isar-remove399,12803
+(defun isar-undos isar-undos402,12878
+(defun isar-cannot-undo isar-cannot-undo406,12984
+(defconst isar-undo-fail-regexpisar-undo-fail-regexp410,13055
+(defconst isar-undo-skip-regexpisar-undo-skip-regexp414,13193
+(defconst isar-undo-ignore-regexpisar-undo-ignore-regexp417,13314
+(defconst isar-undo-remove-regexpisar-undo-remove-regexp420,13379
+(defconst isar-undo-kill-regexpisar-undo-kill-regexp425,13519
+(defconst isar-any-entity-regexpisar-any-entity-regexp431,13661
+(defconst isar-named-entity-regexpisar-named-entity-regexp436,13848
+(defconst isar-unnamed-entity-regexpisar-unnamed-entity-regexp441,14025
+(defconst isar-next-entity-regexpsisar-next-entity-regexps444,14127
+(defconst isar-generic-expressionisar-generic-expression452,14434
+(defconst isar-indent-any-regexpisar-indent-any-regexp463,14668
+(defconst isar-indent-inner-regexpisar-indent-inner-regexp465,14761
+(defconst isar-indent-enclose-regexpisar-indent-enclose-regexp467,14827
+(defconst isar-indent-open-regexpisar-indent-open-regexp469,14943
+(defconst isar-indent-close-regexpisar-indent-close-regexp471,15053
+(defconst isar-outline-regexpisar-outline-regexp477,15190
+(defconst isar-outline-heading-end-regexp isar-outline-heading-end-regexp481,15343
 
 isar/x-symbol-isar.el,0
 
@@ -1822,6 +1692,233 @@ lego/lego-syntax.el,919
 
 lego/x-symbol-lego.el,0
 
+lib/holes.el,3536
+(defun holes-short-doc holes-short-doc24,736
+(defcustom empty-hole-string empty-hole-string149,5370
+(defcustom empty-hole-regexp empty-hole-regexp152,5475
+(defcustom hole-search-limit hole-search-limit155,6075
+(defface active-hole-faceactive-hole-face168,6441
+(defface inactive-hole-faceinactive-hole-face178,6898
+(defun region-beginning-or-nil region-beginning-or-nil197,7434
+(defun region-end-or-nil region-end-or-nil201,7523
+(defun copy-active-region copy-active-region205,7602
+(defun is-hole-p is-hole-p211,7780
+(defun hole-start-position hole-start-position216,7840
+(defun hole-end-position hole-end-position221,7977
+(defun hole-buffer hole-buffer226,8107
+(defun hole-at hole-at231,8229
+(defun active-hole-exist-p active-hole-exist-p240,8417
+(defun active-hole-start-position active-hole-start-position250,8668
+(defun active-hole-end-position active-hole-end-position261,9018
+(defun active-hole-buffer active-hole-buffer273,9364
+(defun goto-active-hole goto-active-hole284,9644
+(defun highlight-hole-as-active highlight-hole-as-active296,9917
+(defun highlight-hole highlight-hole306,10224
+(defun disable-active-hole disable-active-hole317,10519
+(defun set-active-hole set-active-hole335,11028
+(defun is-in-hole-p is-in-hole-p347,11329
+(defun make-hole make-hole357,11474
+(defun make-hole-at make-hole-at382,12289
+(defun clear-hole clear-hole401,12731
+(defun clear-hole-at clear-hole-at411,12948
+(defun map-holes map-holes420,13177
+(defun mapcar-holes mapcar-holes426,13291
+(defun clear-all-buffer-holes clear-all-buffer-holes430,13390
+(defun next-hole next-hole442,13624
+(defun next-after-active-hole next-after-active-hole451,13888
+(defun set-active-hole-next set-active-hole-next458,14068
+(defun set-active-hole-next-after-active set-active-hole-next-after-active475,14425
+(defun replace-segment replace-segment486,14583
+(defun replace-hole replace-hole502,14899
+(defun replace-active-hole replace-active-hole536,16055
+(defun replace-update-active-hole replace-update-active-hole545,16338
+(defun delete-update-active-hole delete-update-active-hole568,16964
+(defun set-make-active-hole set-make-active-hole577,17161
+(defun mouse-replace-active-hole mouse-replace-active-hole624,18508
+(defun destroy-hole destroy-hole642,18984
+(defun hole-at-event hole-at-event657,19295
+(defun mouse-destroy-hole mouse-destroy-hole659,19354
+(defun mouse-forget-hole mouse-forget-hole667,19528
+(defun mouse-set-make-active-hole mouse-set-make-active-hole681,19769
+(defun mouse-set-active-hole mouse-set-active-hole701,20220
+(defun set-point-next-hole-destroy set-point-next-hole-destroy711,20414
+(defun count-char-in-string count-char-in-string775,22661
+(defun count-re-in-string count-re-in-string785,22866
+(defun count-chars-in-last-expand count-chars-in-last-expand795,23077
+(defun count-newlines-in-last-expand count-newlines-in-last-expand799,23166
+(defun indent-last-expand indent-last-expand803,23277
+(defun count-holes-in-last-expand count-holes-in-last-expand818,23603
+(defun replace-string-by-holes replace-string-by-holes822,23722
+(defun replace-string-by-holes-backward replace-string-by-holes-backward841,24148
+(defun replace-string-by-holes-move-point replace-string-by-holes-move-point872,24966
+(defun replace-string-by-holes-backward-move-point replace-string-by-holes-backward-move-point879,25120
+(defun holes-abbrev-complete holes-abbrev-complete889,25296
+(defun insert-and-expand insert-and-expand911,26098
+
+lib/proof-compat.el,1194
+(defvar proof-running-on-XEmacs proof-running-on-XEmacs24,760
+(defvar proof-running-on-Emacs21 proof-running-on-Emacs2126,882
+(defvar proof-running-on-win32 proof-running-on-win3230,1129
+(defun pg-custom-undeclare-variable pg-custom-undeclare-variable41,1562
+(defun subst-char-in-string subst-char-in-string112,3702
+(defun replace-regexp-in-string replace-regexp-in-string126,4256
+(defconst menuvisiblep menuvisiblep188,6969
+(defun set-window-text-height set-window-text-height205,7588
+(defmacro save-selected-frame save-selected-frame231,8538
+(defun warn warn270,9840
+(defun redraw-modeline redraw-modeline277,10095
+(defun replace-in-string replace-in-string292,10662
+(defun proof-buffer-syntactic-context-emulate proof-buffer-syntactic-context-emulate341,12180
+(defvar read-shell-command-mapread-shell-command-map374,13487
+(defun read-shell-command read-shell-command392,14189
+(defun remassq remassq404,14670
+(defun remassoc remassoc416,15059
+(defun frames-of-buffer frames-of-buffer429,15504
+(defmacro with-selected-window with-selected-window468,16767
+(defun pg-pop-to-buffer pg-pop-to-buffer504,17892
+(defun process-live-p process-live-p555,19744
+
+lib/span.el,192
+(defsubst delete-spans delete-spans22,471
+(defsubst span-property-safe span-property-safe26,625
+(defsubst set-span-start set-span-start30,764
+(defsubst set-span-end set-span-end34,896
+
+lib/span-extent.el,1346
+(defsubst make-span make-span16,557
+(defsubst detach-span detach-span20,679
+(defsubst set-span-endpoints set-span-endpoints24,766
+(defsubst set-span-property set-span-property28,899
+(defsubst span-read-only span-read-only32,1026
+(defsubst span-read-write span-read-write36,1130
+(defun span-give-warning span-give-warning40,1237
+(defun span-write-warning span-write-warning44,1335
+(defsubst span-property span-property49,1535
+(defsubst delete-span delete-span53,1650
+(defsubst mapcar-spans mapcar-spans59,1821
+(defsubst span-at span-at63,2027
+(defsubst span-at-before span-at-before67,2144
+(defsubst span-start span-start72,2341
+(defsubst span-end span-end76,2470
+(defsubst prev-span prev-span80,2593
+(defsubst next-span next-span84,2739
+(defsubst span-live-p span-live-p88,2881
+(defun span-raise span-raise96,3153
+(defalias 'span-object span-object100,3252
+(defalias 'span-string span-string101,3291
+(defsubst make-detached-span make-detached-span104,3377
+(defsubst span-buffer span-buffer110,3474
+(defsubst span-detached-p span-detached-p115,3566
+(defsubst set-span-face set-span-face120,3678
+(defsubst fold-spans fold-spans125,3774
+(defsubst set-span-properties set-span-properties130,3972
+(defsubst set-span-keymap set-span-keymap135,4081
+(defsubst span-at-event span-at-event140,4196
+
+lib/span-overlay.el,2198
+(defvar before-list before-list20,771
+(defun foldr foldr27,906
+(defun foldl foldl39,1239
+(defsubst span-start span-start51,1556
+(defsubst span-end span-end55,1648
+(defun set-span-property set-span-property59,1734
+(defsubst span-property span-property63,1850
+(defun span-read-only-hook span-read-only-hook67,1961
+(defun span-read-only span-read-only71,2093
+(defun span-read-write span-read-write86,2871
+(defun span-give-warning span-give-warning92,3090
+(defun span-write-warning span-write-warning96,3198
+(defun int-nil-lt int-nil-lt101,3421
+(defun span-lt span-lt110,3624
+(defun span-traverse span-traverse115,3783
+(defun add-span add-span131,4230
+(defun make-span make-span145,4632
+(defun remove-span remove-span149,4763
+(defun spans-at-point spans-at-point162,5216
+(defun append-unique append-unique176,5696
+(defun spans-at-region spans-at-region179,5783
+(defun spans-at-point-prop spans-at-point-prop186,6005
+(defun spans-at-region-prop spans-at-region-prop194,6255
+(defun span-at span-at206,6602
+(defsubst detach-span detach-span212,6816
+(defsubst delete-span delete-span218,6943
+(defsubst set-span-endpoints set-span-endpoints226,7186
+(defsubst mapcar-spans mapcar-spans233,7402
+(defun map-spans-aux map-spans-aux237,7606
+(defsubst map-spans map-spans241,7721
+(defun find-span-aux find-span-aux244,7779
+(defun find-span find-span249,7905
+(defun span-at-before span-at-before252,7970
+(defun prev-span prev-span265,8412
+(defun next-span next-span274,8694
+(defsubst span-live-p span-live-p299,9678
+(defun span-raise span-raise305,9844
+(defalias 'span-object span-object311,10075
+(defun span-string span-string313,10116
+(defun set-span-properties set-span-properties319,10298
+(defun span-find-span span-find-span331,10553
+(defsubst span-at-event span-at-event342,10912
+(defun make-detached-span make-detached-span347,11036
+(defun fold-spans-aux fold-spans-aux353,11170
+(defun fold-spans fold-spans361,11426
+(defsubst span-buffer span-buffer368,11634
+(defsubst span-detached-p span-detached-p373,11726
+(defsubst set-span-face set-span-face381,11922
+(defsubst set-span-keymap set-span-keymap386,12022
+
+lib/texi-docstring-magic.el,958
+(defun texi-docstring-magic-find-face texi-docstring-magic-find-face85,2996
+(defun texi-docstring-magic-splice-sep texi-docstring-magic-splice-sep90,3161
+(defconst texi-docstring-magic-munge-tabletexi-docstring-magic-munge-table100,3466
+(defun texi-docstring-magic-untabify texi-docstring-magic-untabify190,7186
+(defun texi-docstring-magic-munge-docstring texi-docstring-magic-munge-docstring200,7501
+(defun texi-docstring-magic-texi texi-docstring-magic-texi239,8788
+(defun texi-docstring-magic-format-default texi-docstring-magic-format-default252,9228
+(defun texi-docstring-magic-texi-for texi-docstring-magic-texi-for268,9863
+(defconst texi-docstring-magic-commenttexi-docstring-magic-comment326,11823
+(defun texi-docstring-magic texi-docstring-magic332,11977
+(defun texi-docstring-magic-face-at-point texi-docstring-magic-face-at-point366,13057
+(defun texi-docstring-magic-insert-magic texi-docstring-magic-insert-magic381,13580
+
+lib/url-parse.el,921
+(defmacro url-type url-type28,1226
+(defmacro url-user url-user31,1282
+(defmacro url-password url-password34,1338
+(defmacro url-host url-host37,1398
+(defmacro url-port url-port40,1454
+(defmacro url-filename url-filename45,1613
+(defmacro url-target url-target48,1673
+(defmacro url-attributes url-attributes51,1731
+(defmacro url-fullness url-fullness54,1793
+(defmacro url-set-type url-set-type57,1853
+(defmacro url-set-user url-set-user60,1927
+(defmacro url-set-password url-set-password63,2001
+(defmacro url-set-host url-set-host66,2079
+(defmacro url-set-port url-set-port69,2153
+(defmacro url-set-filename url-set-filename72,2227
+(defmacro url-set-target url-set-target75,2305
+(defmacro url-set-attributes url-set-attributes78,2381
+(defmacro url-set-full url-set-full81,2461
+(defun url-recreate-url url-recreate-url84,2535
+(defun url-generic-parse-url url-generic-parse-url109,3289
+
+lib/xml.el,790
+(defsubst xml-node-name xml-node-name82,2907
+(defsubst xml-node-attributes xml-node-attributes87,3026
+(defsubst xml-node-children xml-node-children92,3144
+(defun xml-get-children xml-get-children97,3280
+(defun xml-get-attribute xml-get-attribute107,3603
+(defun xml-parse-file xml-parse-file123,4067
+(defun xml-parse-region xml-parse-region144,4651
+(defun xml-parse-tag xml-parse-tag179,5696
+(defun xml-parse-attlist xml-parse-attlist284,9165
+(defun xml-skip-dtd xml-skip-dtd321,10555
+(defun xml-parse-dtd xml-parse-dtd338,11191
+(defun xml-parse-elem-type xml-parse-elem-type408,13269
+(defun xml-substitute-special xml-substitute-special449,14424
+(defun xml-debug-print xml-debug-print470,15231
+(defun xml-debug-print-internal xml-debug-print-internal474,15323
+
 mmm/mmm-auto.el,499
 (defvar mmm-autoloaded-classesmmm-autoloaded-classes67,2675
 (defun mmm-autoload-class mmm-autoload-class85,3320
@@ -2045,24 +2142,26 @@ mmm/mmm-vars.el,3586
 (defun mmm-mode-ext-applies mmm-mode-ext-applies737,28391
 (defun mmm-get-all-classes mmm-get-all-classes751,28875
 
-phox/phox.el,886
+phox/phox.el,1008
 (defcustom phox-prog-name phox-prog-name30,907
 (defcustom phox-sym-lock phox-sym-lock35,1009
-(defcustom phox-web-pagephox-web-page40,1107
-(defcustom phox-doc-dir phox-doc-dir46,1257
-(defcustom phox-lib-dir phox-lib-dir52,1405
-(defcustom phox-tags-program phox-tags-program58,1549
-(defcustom phox-tags-doc phox-tags-doc64,1729
-(defcustom phox-etags phox-etags70,1867
-(defpgdefault menu-entriesmenu-entries90,2297
-(defun phox-config phox-config107,2626
-(defun phox-shell-config phox-shell-config149,4550
-(define-derived-mode phox-mode phox-mode189,6130
-(define-derived-mode phox-shell-mode phox-shell-mode204,6574
-(define-derived-mode phox-response-mode phox-response-mode209,6702
-(define-derived-mode phox-goals-mode phox-goals-mode221,7121
-(defun phox-pre-shell-start phox-pre-shell-start247,8180
-(defpgdefault completion-tablecompletion-table261,8694
+(defcustom phox-x-symbol-enable phox-x-symbol-enable40,1133
+(defcustom phox-web-pagephox-web-page45,1238
+(defcustom phox-doc-dir phox-doc-dir51,1388
+(defcustom phox-lib-dir phox-lib-dir57,1536
+(defcustom phox-tags-program phox-tags-program63,1680
+(defcustom phox-tags-doc phox-tags-doc69,1860
+(defcustom phox-etags phox-etags75,1998
+(defpgdefault menu-entriesmenu-entries95,2428
+(defun phox-config phox-config112,2757
+(defun phox-shell-config phox-shell-config154,4681
+(define-derived-mode phox-mode phox-mode194,6261
+(define-derived-mode phox-shell-mode phox-shell-mode209,6705
+(define-derived-mode phox-response-mode phox-response-mode214,6833
+(define-derived-mode phox-goals-mode phox-goals-mode226,7252
+(defun phox-pre-shell-start phox-pre-shell-start252,8311
+(defpgdefault completion-tablecompletion-table266,8825
+(defpgdefault x-symbol-language x-symbol-language286,9405
 
 phox/phox-extraction.el,603
 (defvar phox-prog-orig phox-prog-orig11,480
@@ -2148,42 +2247,43 @@ phox/phox-tags.el,483
 (defun phox-complete-tag(phox-complete-tag77,2349
 (defvar phox-tags-menuphox-tags-menu96,2904
 
-phox/x-symbol-phox.el,2672
-(defvar x-symbol-phox-required-fonts x-symbol-phox-required-fonts21,705
-(defvar x-symbol-phox-name x-symbol-phox-name31,1204
-(defvar x-symbol-phox-modeline-name x-symbol-phox-modeline-name32,1246
-(defcustom x-symbol-phox-header-groups-alist x-symbol-phox-header-groups-alist34,1291
-(defcustom x-symbol-phox-electric-ignore x-symbol-phox-electric-ignore41,1511
-(defvar x-symbol-phox-required-fonts x-symbol-phox-required-fonts48,1759
-(defvar x-symbol-phox-extra-menu-items x-symbol-phox-extra-menu-items51,1860
-(defvar x-symbol-phox-token-grammarx-symbol-phox-token-grammar55,1950
-(defvar x-symbol-phox-input-token-grammarx-symbol-phox-input-token-grammar66,2456
-(defun x-symbol-phox-default-token-list x-symbol-phox-default-token-list72,2711
-(defvar x-symbol-phox-user-table x-symbol-phox-user-table84,3000
-(defvar x-symbol-phox-generated-data x-symbol-phox-generated-data87,3109
-(defvar x-symbol-phox-master-directory x-symbol-phox-master-directory95,3348
-(defvar x-symbol-phox-image-searchpath x-symbol-phox-image-searchpath96,3397
-(defvar x-symbol-phox-image-cached-dirs x-symbol-phox-image-cached-dirs97,3445
-(defvar x-symbol-phox-image-file-truename-alist x-symbol-phox-image-file-truename-alist98,3511
-(defvar x-symbol-phox-image-keywords x-symbol-phox-image-keywords99,3564
-(defcustom x-symbol-phox-class-alistx-symbol-phox-class-alist105,3784
-(defcustom x-symbol-phox-class-face-alist x-symbol-phox-class-face-alist116,4166
-(defvar x-symbol-phox-font-lock-keywords x-symbol-phox-font-lock-keywords126,4479
-(defvar x-symbol-phox-font-lock-allowed-faces x-symbol-phox-font-lock-allowed-faces128,4526
-(defvar x-symbol-phox-case-insensitive x-symbol-phox-case-insensitive134,4751
-(defvar x-symbol-phox-token-shape x-symbol-phox-token-shape135,4795
-(defvar x-symbol-phox-input-token-ignore x-symbol-phox-input-token-ignore136,4834
-(defvar x-symbol-phox-token-list x-symbol-phox-token-list143,5073
-(defvar x-symbol-phox-xsymb0-table x-symbol-phox-xsymb0-table145,5118
-(defun x-symbol-phox-prepare-table x-symbol-phox-prepare-table166,5573
-(defvar x-symbol-phox-tablex-symbol-phox-table173,5744
-(defvar x-symbol-phox-menu-alist x-symbol-phox-menu-alist184,6116
-(defvar x-symbol-phox-grid-alist x-symbol-phox-grid-alist186,6206
-(defvar x-symbol-phox-decode-atree x-symbol-phox-decode-atree189,6297
-(defvar x-symbol-phox-decode-alist x-symbol-phox-decode-alist191,6390
-(defvar x-symbol-phox-encode-alist x-symbol-phox-encode-alist193,6487
-(defvar x-symbol-phox-nomule-decode-exec x-symbol-phox-nomule-decode-exec197,6644
-(defvar x-symbol-phox-nomule-encode-exec x-symbol-phox-nomule-encode-exec199,6744
+phox/x-symbol-phox.el,2739
+(defvar x-symbol-phox-required-fonts x-symbol-phox-required-fonts14,449
+(defvar x-symbol-phox-name x-symbol-phox-name24,946
+(defvar x-symbol-phox-modeline-name x-symbol-phox-modeline-name25,988
+(defcustom x-symbol-phox-header-groups-alist x-symbol-phox-header-groups-alist27,1033
+(defcustom x-symbol-phox-electric-ignore x-symbol-phox-electric-ignore34,1253
+(defvar x-symbol-phox-required-fonts x-symbol-phox-required-fonts41,1501
+(defvar x-symbol-phox-extra-menu-items x-symbol-phox-extra-menu-items44,1602
+(defvar x-symbol-phox-token-grammarx-symbol-phox-token-grammar47,1691
+(defvar x-symbol-phox-input-token-grammarx-symbol-phox-input-token-grammar59,2220
+(defun x-symbol-phox-default-token-list x-symbol-phox-default-token-list65,2475
+(defvar x-symbol-phox-user-table x-symbol-phox-user-table77,2764
+(defvar x-symbol-phox-generated-data x-symbol-phox-generated-data80,2873
+(defvar x-symbol-phox-master-directory x-symbol-phox-master-directory88,3112
+(defvar x-symbol-phox-image-searchpath x-symbol-phox-image-searchpath89,3161
+(defvar x-symbol-phox-image-cached-dirs x-symbol-phox-image-cached-dirs90,3209
+(defvar x-symbol-phox-image-file-truename-alist x-symbol-phox-image-file-truename-alist91,3275
+(defvar x-symbol-phox-image-keywords x-symbol-phox-image-keywords92,3328
+(defcustom x-symbol-phox-class-alistx-symbol-phox-class-alist99,3549
+(defcustom x-symbol-phox-class-face-alist x-symbol-phox-class-face-alist110,3931
+(defvar x-symbol-phox-font-lock-keywords x-symbol-phox-font-lock-keywords120,4244
+(defvar x-symbol-phox-font-lock-allowed-faces x-symbol-phox-font-lock-allowed-faces122,4291
+(defvar x-symbol-phox-case-insensitive x-symbol-phox-case-insensitive128,4516
+(defvar x-symbol-phox-token-shape x-symbol-phox-token-shape129,4560
+(defvar x-symbol-phox-input-token-ignore x-symbol-phox-input-token-ignore130,4599
+(defvar x-symbol-phox-token-list x-symbol-phox-token-list137,4838
+(defvar x-symbol-phox-xsymb0-table x-symbol-phox-xsymb0-table139,4883
+(defun x-symbol-phox-prepare-table x-symbol-phox-prepare-table160,5342
+(defvar x-symbol-phox-tablex-symbol-phox-table167,5513
+(defcustom x-symbol-phox-auto-stylex-symbol-phox-auto-style178,5831
+(defvar x-symbol-phox-menu-alist x-symbol-phox-menu-alist204,6781
+(defvar x-symbol-phox-grid-alist x-symbol-phox-grid-alist206,6871
+(defvar x-symbol-phox-decode-atree x-symbol-phox-decode-atree209,6962
+(defvar x-symbol-phox-decode-alist x-symbol-phox-decode-alist211,7055
+(defvar x-symbol-phox-encode-alist x-symbol-phox-encode-alist213,7152
+(defvar x-symbol-phox-nomule-decode-exec x-symbol-phox-nomule-decode-exec217,7309
+(defvar x-symbol-phox-nomule-encode-exec x-symbol-phox-nomule-encode-exec219,7409
 
 plastic/plastic.el,4425
 (defcustom plastic-tags plastic-tags28,805
@@ -2496,186 +2596,187 @@ twelf/twelf-old.el,10513
 twelf/x-symbol-twelf.el,0
 
 todo,1297
-   function to to373,15257
+   function to to383,15505
 $Id: todo,2,21
 This is an outline file.   Use C-c C-n,4,67
-X 41,1156
-*** C Improved configurability of command settings,172,6638
-  We should let command settings,173,6695
-  We should let command settings, etc,173,6695
-  - XEmacs pg forces on font-lock,323,12844
-    Save foo;399,16380
-*** A Doc new bits: font lock keywords,469,19081
-*** A Doc new bits: font lock keywords, filename %e,469,19081
-  Added proof-{script,470,19138
-  Added proof-{script,shell,470,19138
-  Added proof-{script,shell,goals,470,19138
-  Presently used only in proof-easy-config,471,19198
-  - Mention configuring function menus,482,19534
-  - document mouse functions,484,19620
-  - document mouse functions, proof-cd,484,19620
-  - document mouse functions, proof-cd, process quit timeout,484,19620
-    X-Symbol,485,19683
-    X-Symbol, prog-name-guess,485,19683
-*** D Fix INFO-DIR-ENTRY in 499,20191
-*** C Fixing up errors caused by pbp-generated commands; currently,565,22668
-  should mean generates an error.  With LEGO pbp,568,22874
-  tactic which always succeeds,569,22938
-  decodes annotations eagerly. Lazily would be faster,577,23294
-  the tech report claims --- djs: probably not much faster,578,23363
-***  6. Update Emacs and prover versions in texi,667,26366
-
-doc/ProofGeneral.texi,5815
-@node TopTop166,5018
-@node PrefacePreface203,6141
-@node Latest news for 3.5Latest news for 3.5226,6729
-@node FutureFuture264,8387
-@node CreditsCredits299,9937
-@node Introducing Proof GeneralIntroducing Proof General397,13352
-@node Quick start guideQuick start guide452,15344
-@node Features of Proof GeneralFeatures of Proof General506,17913
-@node Supported proof assistantsSupported proof assistants595,21838
-@node Prerequisites for this manualPrerequisites for this manual647,23834
-@node Organization of this manualOrganization of this manual691,25460
-@node Basic Script ManagementBasic Script Management717,26287
-@node Walkthrough example in Isabelle/IsarWalkthrough example in Isabelle/Isar736,26892
-@node Proof scriptsProof scripts963,35427
-@node Script buffersScript buffers1006,37547
-@node Locked queue and editing regionsLocked queue and editing regions1028,38124
-@node Goal-save sequencesGoal-save sequences1084,40271
-@node Active scripting bufferActive scripting buffer1121,41757
-@node Summary of Proof General buffersSummary of Proof General buffers1190,45177
-@node Script editing commandsScript editing commands1252,47851
-@node Script processing commandsScript processing commands1329,50614
-@node Proof assistant commandsProof assistant commands1457,55915
-@node Toolbar commandsToolbar commands1603,60802
-@node Interrupting during trace outputInterrupting during trace output1627,61731
-@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing1666,63654
-@node Goals buffer commandsGoals buffer commands1680,64154
-@node Advanced Script ManagementAdvanced Script Management1769,67686
-@node Visibility of completed proofsVisibility of completed proofs1800,68840
-@node Switching between proof scriptsSwitching between proof scripts1855,70763
-@node View of processed files View of processed files 1892,72735
-@node Retracting across filesRetracting across files1952,75786
-@node Asserting across filesAsserting across files1965,76417
-@node Automatic multiple file handlingAutomatic multiple file handling1978,76983
-@node Escaping script managementEscaping script management2003,78017
-@node Experimental featuresExperimental features2061,80220
-@node Support for other PackagesSupport for other Packages2095,81482
-@node Syntax highlightingSyntax highlighting2127,82357
-@node X-Symbol supportX-Symbol support2166,83966
-@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)2225,86512
-@node Support for outline modeSupport for outline mode2284,88642
-@node Support for completionSupport for completion2310,89772
-@node Support for tagsSupport for tags2367,91935
-@node Customizing Proof GeneralCustomizing Proof General2419,94263
-@node Basic optionsBasic options2459,95933
-@node How to customizeHow to customize2483,96691
-@node Display customizationDisplay customization2534,98781
-@node User optionsUser options2659,104015
-@node Changing facesChanging faces2913,113021
-@node Tweaking configuration settingsTweaking configuration settings2988,115690
-@node Hints and TipsHints and Tips3045,118215
-@node Adding your own keybindingsAdding your own keybindings3064,118816
-@node Using file variablesUsing file variables3120,121349
-@node Using abbreviationsUsing abbreviations3173,123172
-@node LEGO Proof GeneralLEGO Proof General3212,124587
-@node LEGO specific commandsLEGO specific commands3253,125956
-@node LEGO tagsLEGO tags3273,126411
-@node LEGO customizationsLEGO customizations3283,126658
-@node Coq Proof GeneralCoq Proof General3315,127576
-@node Coq-specific commandsCoq-specific commands3331,127985
-@node Coq-specific variablesCoq-specific variables3353,128492
-@node Editing multiple proofsEditing multiple proofs3391,129707
-@node User-loaded tacticsUser-loaded tactics3415,130815
-@node Holes featureHoles feature3480,133342
-@node Isabelle Proof GeneralIsabelle Proof General3507,134628
-@node Classic IsabelleClassic Isabelle3576,137951
-@node ML filesML files3592,138389
-@node Theory filesTheory files3663,140814
-@node General commands for IsabelleGeneral commands for Isabelle3717,143285
-@node Specific commands for IsabelleSpecific commands for Isabelle3729,143767
-@node Isabelle customizationsIsabelle customizations3758,144707
-@node Isabelle/IsarIsabelle/Isar3823,146805
-@node General commands for Isabelle/IsarGeneral commands for Isabelle/Isar3844,147568
-@node Specific commands for Isabelle/IsarSpecific commands for Isabelle/Isar3851,147822
-@node Logics and SettingsLogics and Settings3938,150350
-@node HOL Proof GeneralHOL Proof General3979,152038
-@node Shell Proof GeneralShell Proof General4020,153822
-@node Obtaining and InstallingObtaining and Installing4056,155280
-@node Obtaining Proof GeneralObtaining Proof General4072,155693
-@node Installing Proof General from tarballInstalling Proof General from tarball4103,156932
-@node Installing Proof General from RPM packageInstalling Proof General from RPM package4128,157764
-@node Setting the names of binariesSetting the names of binaries4143,158172
-@node Notes for syssiesNotes for syssies4171,159100
-@node Known bugs and workaroundsKnown bugs and workarounds4244,162049
-@node ReferencesReferences4257,162482
-@node History of Proof GeneralHistory of Proof General4297,163506
-@node Old News for 3.0Old News for 3.04388,167608
-@node Old News for 3.1Old News for 3.14458,171302
-@node Old News for 3.2Old News for 3.24484,172474
-@node Old News for 3.3Old News for 3.34545,175477
-@node Old News for 3.4Old News for 3.44564,176374
-@node Function IndexFunction Index4587,177430
-@node Variable IndexVariable Index4591,177506
-@node Keystroke IndexKeystroke Index4595,177586
-@node Concept IndexConcept Index4599,177652
-
-doc/PG-adapting.texi,3791
-@node TopTop157,4774
-@node IntroductionIntroduction194,5888
-@node FutureFuture235,7541
-@node CreditsCredits271,9137
-@node Beginning with a new proverBeginning with a new prover281,9429
-@node Overview of adding a new proverOverview of adding a new prover322,11378
-@node Demonstration instance and easy configurationDemonstration instance and easy configuration396,14799
-@node Major modes used by Proof GeneralMajor modes used by Proof General465,18190
-@node Menus and toolbar and user-level commandsMenus and toolbar and user-level commands538,21273
-@node Settings for generic user-level commandsSettings for generic user-level commands553,21819
-@node Menu configurationMenu configuration598,23555
-@node Toolbar configurationToolbar configuration622,24473
-@node Proof script settingsProof script settings680,26718
-@node Recognizing commands and commentsRecognizing commands and comments702,27298
-@node Recognizing proofsRecognizing proofs823,32825
-@node Recognizing other elementsRecognizing other elements935,37639
-@node Configuring undo behaviourConfiguring undo behaviour1061,43117
-@node Nested proofsNested proofs1199,48458
-@node Safe (state-preserving) commandsSafe (state-preserving) commands1239,50085
-@node Activate scripting hookActivate scripting hook1262,51031
-@node Automatic multiple filesAutomatic multiple files1286,51895
-@node CompletionsCompletions1308,52742
-@node Proof shell settingsProof shell settings1348,54218
-@node Proof shell commandsProof shell commands1379,55500
-@node Script input to the shellScript input to the shell1542,62375
-@node Settings for matching various output from proof processSettings for matching various output from proof process1609,65418
-@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process1740,71182
-@node Hooks and other settingsHooks and other settings1950,80735
-@node Goals buffer settingsGoals buffer settings2046,84568
-@node Splash screen settingsSplash screen settings2123,87676
-@node Global constantsGlobal constants2149,88434
-@node Handling multiple filesHandling multiple files2175,89283
-@node Configuring Font LockConfiguring Font Lock2327,97067
-@node Configuring X-SymbolConfiguring X-Symbol2370,98960
-@node Writing more lisp codeWriting more lisp code2430,101483
-@node Default values for generic settingsDefault values for generic settings2447,102128
-@node Adding prover-specific configurationsAdding prover-specific configurations2477,103211
-@node Useful variablesUseful variables2520,104481
-@node Useful functions and macrosUseful functions and macros2546,105275
-@node Internals of Proof GeneralInternals of Proof General2648,109152
-@node SpansSpans2676,110060
-@node Proof General site configurationProof General site configuration2689,110434
-@node Configuration variable mechanismsConfiguration variable mechanisms2769,113578
-@node Global variablesGlobal variables2887,118814
-@node Proof script modeProof script mode2957,121364
-@node Proof shell modeProof shell mode3216,133019
-@node DebuggingDebugging3622,149066
-@node Plans and ideasPlans and ideas3665,149961
-@node Proof by pointing and similar featuresProof by pointing and similar features3686,150683
-@node Granularity of atomic command sequencesGranularity of atomic command sequences3724,152341
-@node Browser mode for script files and theoriesBrowser mode for script files and theories3769,154566
-@node Demonstration InstantiationsDemonstration Instantiations3799,155597
-@node demoisa-easy.eldemoisa-easy.el3815,156028
-@node demoisa.eldemoisa.el3878,158266
-@node Function IndexFunction Index4046,163782
-@node Variable IndexVariable Index4050,163858
-@node Concept IndexConcept Index4059,164037
+X 51,1404
+*** C Improved configurability of command settings,182,6886
+  We should let command settings,183,6943
+  We should let command settings, etc,183,6943
+  - XEmacs pg forces on font-lock,333,13092
+    Save foo;409,16628
+*** A Doc new bits: font lock keywords,479,19329
+*** A Doc new bits: font lock keywords, filename %e,479,19329
+  Added proof-{script,480,19386
+  Added proof-{script,shell,480,19386
+  Added proof-{script,shell,goals,480,19386
+  Presently used only in proof-easy-config,481,19446
+  - Mention configuring function menus,492,19782
+  - document mouse functions,494,19868
+  - document mouse functions, proof-cd,494,19868
+  - document mouse functions, proof-cd, process quit timeout,494,19868
+    X-Symbol,495,19931
+    X-Symbol, prog-name-guess,495,19931
+*** D Fix INFO-DIR-ENTRY in 509,20439
+*** C Fixing up errors caused by pbp-generated commands; currently,575,22916
+  should mean generates an error.  With LEGO pbp,578,23122
+  tactic which always succeeds,579,23186
+  decodes annotations eagerly. Lazily would be faster,587,23542
+  the tech report claims --- djs: probably not much faster,588,23611
+***  6. Update Emacs and prover versions in texi,677,26614
+
+doc/ProofGeneral.texi,5783
+@node TopTop166,5019
+@node PrefacePreface203,6126
+@node Latest news for 3.5Latest news for 3.5226,6714
+@node FutureFuture264,8372
+@node CreditsCredits299,9922
+@node Introducing Proof GeneralIntroducing Proof General397,13337
+@node Quick start guideQuick start guide452,15329
+@node Features of Proof GeneralFeatures of Proof General506,17898
+@node Supported proof assistantsSupported proof assistants595,21823
+@node Prerequisites for this manualPrerequisites for this manual647,23819
+@node Organization of this manualOrganization of this manual691,25445
+@node Basic Script ManagementBasic Script Management717,26272
+@node Walkthrough example in Isabelle/IsarWalkthrough example in Isabelle/Isar736,26877
+@node Proof scriptsProof scripts963,35412
+@node Script buffersScript buffers1006,37532
+@node Locked queue and editing regionsLocked queue and editing regions1028,38109
+@node Goal-save sequencesGoal-save sequences1084,40256
+@node Active scripting bufferActive scripting buffer1121,41742
+@node Summary of Proof General buffersSummary of Proof General buffers1190,45162
+@node Script editing commandsScript editing commands1252,47836
+@node Script processing commandsScript processing commands1330,50694
+@node Proof assistant commandsProof assistant commands1458,55995
+@node Toolbar commandsToolbar commands1604,60882
+@node Interrupting during trace outputInterrupting during trace output1628,61811
+@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing1667,63734
+@node Goals buffer commandsGoals buffer commands1681,64234
+@node Advanced Script ManagementAdvanced Script Management1770,67766
+@node Visibility of completed proofsVisibility of completed proofs1801,68920
+@node Switching between proof scriptsSwitching between proof scripts1856,70843
+@node View of processed files View of processed files 1893,72815
+@node Retracting across filesRetracting across files1953,75866
+@node Asserting across filesAsserting across files1966,76497
+@node Automatic multiple file handlingAutomatic multiple file handling1979,77063
+@node Escaping script managementEscaping script management2004,78097
+@node Experimental featuresExperimental features2062,80300
+@node Support for other PackagesSupport for other Packages2096,81562
+@node Syntax highlightingSyntax highlighting2128,82437
+@node X-Symbol supportX-Symbol support2167,84046
+@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)2226,86592
+@node Support for outline modeSupport for outline mode2285,88722
+@node Support for completionSupport for completion2311,89852
+@node Support for tagsSupport for tags2368,92017
+@node Customizing Proof GeneralCustomizing Proof General2420,94345
+@node Basic optionsBasic options2460,96015
+@node How to customizeHow to customize2484,96773
+@node Display customizationDisplay customization2535,98863
+@node User optionsUser options2660,104097
+@node Changing facesChanging faces2914,113103
+@node Tweaking configuration settingsTweaking configuration settings2989,115772
+@node Hints and TipsHints and Tips3046,118297
+@node Adding your own keybindingsAdding your own keybindings3065,118898
+@node Using file variablesUsing file variables3121,121431
+@node Using abbreviationsUsing abbreviations3174,123254
+@node LEGO Proof GeneralLEGO Proof General3213,124669
+@node LEGO specific commandsLEGO specific commands3254,126038
+@node LEGO tagsLEGO tags3274,126493
+@node LEGO customizationsLEGO customizations3284,126740
+@node Coq Proof GeneralCoq Proof General3316,127658
+@node Coq-specific commandsCoq-specific commands3332,128067
+@node Coq-specific variablesCoq-specific variables3354,128574
+@node Editing multiple proofsEditing multiple proofs3392,129789
+@node User-loaded tacticsUser-loaded tactics3416,130897
+@node Holes featureHoles feature3481,133424
+@node Isabelle Proof GeneralIsabelle Proof General3508,134710
+@node Classic IsabelleClassic Isabelle3577,138033
+@node ML filesML files3593,138471
+@node Theory filesTheory files3664,140896
+@node General commands for IsabelleGeneral commands for Isabelle3718,143367
+@node Specific commands for IsabelleSpecific commands for Isabelle3730,143849
+@node Isabelle customizationsIsabelle customizations3759,144789
+@node Isabelle/IsarIsabelle/Isar3824,146887
+@node General commands for Isabelle/IsarGeneral commands for Isabelle/Isar3845,147650
+@node Specific commands for Isabelle/IsarSpecific commands for Isabelle/Isar3852,147904
+@node Logics and SettingsLogics and Settings3939,150432
+@node HOL Proof GeneralHOL Proof General3980,152120
+@node Shell Proof GeneralShell Proof General4021,153904
+@node Obtaining and InstallingObtaining and Installing4057,155362
+@node Obtaining Proof GeneralObtaining Proof General4073,155775
+@node Installing Proof General from tarballInstalling Proof General from tarball4104,157014
+@node Installing Proof General from RPM packageInstalling Proof General from RPM package4129,157846
+@node Setting the names of binariesSetting the names of binaries4144,158254
+@node Notes for syssiesNotes for syssies4172,159182
+@node Known BugsKnown Bugs4245,162115
+@node ReferencesReferences4258,162516
+@node History of Proof GeneralHistory of Proof General4298,163540
+@node Old News for 3.0Old News for 3.04389,167642
+@node Old News for 3.1Old News for 3.14459,171336
+@node Old News for 3.2Old News for 3.24485,172508
+@node Old News for 3.3Old News for 3.34546,175511
+@node Old News for 3.4Old News for 3.44565,176408
+@node Function IndexFunction Index4588,177464
+@node Variable IndexVariable Index4592,177540
+@node Keystroke IndexKeystroke Index4596,177620
+@node Concept IndexConcept Index4600,177686
+
+doc/PG-adapting.texi,3863
+@node TopTop157,4775
+@node IntroductionIntroduction195,5920
+@node FutureFuture236,7573
+@node CreditsCredits272,9169
+@node Beginning with a New ProverBeginning with a New Prover282,9461
+@node Overview of adding a new proverOverview of adding a new prover323,11410
+@node Demonstration instance and easy configurationDemonstration instance and easy configuration397,14831
+@node Major modes used by Proof GeneralMajor modes used by Proof General466,18222
+@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands539,21305
+@node Settings for generic user-level commandsSettings for generic user-level commands554,21851
+@node Menu configurationMenu configuration599,23587
+@node Toolbar configurationToolbar configuration623,24505
+@node Proof Script SettingsProof Script Settings681,26750
+@node Recognizing commands and commentsRecognizing commands and comments703,27330
+@node Recognizing proofsRecognizing proofs824,32857
+@node Recognizing other elementsRecognizing other elements936,37671
+@node Configuring undo behaviourConfiguring undo behaviour1062,43149
+@node Nested proofsNested proofs1200,48490
+@node Safe (state-preserving) commandsSafe (state-preserving) commands1240,50117
+@node Activate scripting hookActivate scripting hook1263,51063
+@node Automatic multiple filesAutomatic multiple files1287,51927
+@node CompletionsCompletions1309,52774
+@node Proof Shell SettingsProof Shell Settings1349,54252
+@node Proof shell commandsProof shell commands1380,55534
+@node Script input to the shellScript input to the shell1543,62409
+@node Settings for matching various output from proof processSettings for matching various output from proof process1610,65452
+@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process1741,71216
+@node Hooks and other settingsHooks and other settings1951,80769
+@node Goals Buffer SettingsGoals Buffer Settings2047,84602
+@node Splash Screen SettingsSplash Screen Settings2124,87710
+@node Global ConstantsGlobal Constants2150,88468
+@node Handling Multiple FilesHandling Multiple Files2176,89317
+@node Configuring Editing SyntaxConfiguring Editing Syntax2328,97101
+@node Configuring Font LockConfiguring Font Lock2385,99218
+@node Configuring X-SymbolConfiguring X-Symbol2472,103461
+@node Writing More Lisp CodeWriting More Lisp Code2532,105984
+@node Default values for generic settingsDefault values for generic settings2549,106629
+@node Adding prover-specific configurationsAdding prover-specific configurations2579,107712
+@node Useful variablesUseful variables2622,108982
+@node Useful functions and macrosUseful functions and macros2648,109776
+@node Internals of Proof GeneralInternals of Proof General2750,113653
+@node SpansSpans2778,114561
+@node Proof General site configurationProof General site configuration2791,114935
+@node Configuration variable mechanismsConfiguration variable mechanisms2871,118079
+@node Global variablesGlobal variables2989,123315
+@node Proof script modeProof script mode3059,125865
+@node Proof shell modeProof shell mode3318,137520
+@node DebuggingDebugging3724,153567
+@node Plans and IdeasPlans and Ideas3767,154462
+@node Proof by pointing and similar featuresProof by pointing and similar features3788,155184
+@node Granularity of atomic command sequencesGranularity of atomic command sequences3826,156842
+@node Browser mode for script files and theoriesBrowser mode for script files and theories3871,159067
+@node Demonstration InstantiationsDemonstration Instantiations3901,160098
+@node demoisa-easy.eldemoisa-easy.el3917,160529
+@node demoisa.eldemoisa.el3980,162767
+@node Function IndexFunction Index4148,168283
+@node Variable IndexVariable Index4152,168359
+@node Concept IndexConcept Index4161,168538
author	David Aspinall <da@inf.ed.ac.uk>	2004-08-25 21:05:53 +0000
committer	David Aspinall <da@inf.ed.ac.uk>	2004-08-25 21:05:53 +0000
commit	882e453a0921295e95201a57ed55517ad66e9342 (patch)
tree	e9678e5fe096024b8be35d0830a699c4e3ced7b7 /TAGS
parent	c0ba98b45ed0c886e5bbfbc76c79aeeaf388fd64 (diff)