Updated.

author: David Aspinall <da@inf.ed.ac.uk> 2004-05-07 11:16:59 +0000
committer: David Aspinall <da@inf.ed.ac.uk> 2004-05-07 11:16:59 +0000
commit: 255f394c87bdcd47e0d0d7b07bd830c750d4c29d (patch)
tree: eda902bf65cf4a0a8dd07009e45ac511ba1b053b /TAGS
parent: 334c7fd0210bbe065661ee8bf47fb38f5d85daf4 (diff)
1 files changed, 700 insertions, 677 deletions
diff --git a/TAGS b/TAGS
index 3074444b..83d96951 100644
--- a/TAGS
+++ b/TAGS
@@ -3,88 +3,105 @@ acl2/acl2.el,0
 
 acl2/x-symbol-acl2.el,0
 
-coq/coq-abbrev.el,49
+coq/coq-abbrev.el,109
 (defpgdefault menu-entriesmenu-entries147,7898
+(defpgdefault help-menu-entrieshelp-menu-entries341,18188
 
 coq/coq-abbrev-V7.el,49
 (defpgdefault menu-entriesmenu-entries119,5878
 
-coq/coq.el,4517
-(defcustom coq-prog-name coq-prog-name13,353
-(defcustom coq-default-undo-limit coq-default-undo-limit20,512
-(defconst coq-shell-init-cmd coq-shell-init-cmd25,640
-(defconst coq-shell-restart-cmd coq-shell-restart-cmd38,1063
-(defvar coq-shell-prompt-pattern coq-shell-prompt-pattern42,1145
-(defvar coq-shell-cd coq-shell-cd46,1320
-(defvar coq-shell-abort-goal-regexp coq-shell-abort-goal-regexp49,1420
-(defvar coq-shell-proof-completed-regexp coq-shell-proof-completed-regexp52,1546
-(defvar coq-goal-regexpcoq-goal-regexp55,1677
-(defun coq-library-directory coq-library-directory64,1866
-(defcustom coq-tags coq-tags71,2046
-(defconst coq-interrupt-regexp coq-interrupt-regexp76,2195
-(defcustom coq-www-home-page coq-www-home-page81,2315
-(defun coq-insert-section coq-insert-section97,2565
-(defconst module-kinds-table module-kinds-table106,2822
-(defconst modtype-kinds-tablemodtype-kinds-table110,2958
-(defun coq-insert-module coq-insert-module114,3087
-(defvar coq-outline-regexpcoq-outline-regexp135,3844
-(defvar coq-outline-heading-end-regexp coq-outline-heading-end-regexp140,4253
-(defvar coq-shell-outline-regexp coq-shell-outline-regexp142,4312
-(defvar coq-shell-outline-heading-end-regexp coq-shell-outline-heading-end-regexp143,4362
-(defconst coq-kill-goal-command coq-kill-goal-command145,4425
-(defconst coq-forget-id-command coq-forget-id-command146,4468
-(defconst coq-back-n-command coq-back-n-command147,4514
-(defconst coq-state-changing-tactics-regexp coq-state-changing-tactics-regexp151,4576
-(defconst coq-state-preserving-tactics-regexp coq-state-preserving-tactics-regexp153,4673
-(defconst coq-tactics-regexpcoq-tactics-regexp155,4774
-(defconst coq-state-changing-commands-regexpcoq-state-changing-commands-regexp157,4840
-(defconst coq-state-preserving-commands-regexp coq-state-preserving-commands-regexp159,4947
-(defvar coq-retractable-instruct-regexp coq-retractable-instruct-regexp161,5059
-(defvar coq-non-retractable-instruct-regexpcoq-non-retractable-instruct-regexp163,5150
-(defvar coq-keywords-sectioncoq-keywords-section166,5249
-(defvar coq-section-regexp coq-section-regexp171,5394
-(defun coq-set-undo-limit coq-set-undo-limit204,6461
-(defconst coq-keywords-decl-defn-regexpcoq-keywords-decl-defn-regexp215,6804
-(defun coq-proof-mode-p coq-proof-mode-p223,7192
-(defun coq-is-comment-or-proverprocp coq-is-comment-or-proverprocp238,7698
-(defun coq-is-goalsave-p coq-is-goalsave-p240,7802
-(defun coq-is-module-equal-p coq-is-module-equal-p241,7877
-(defun coq-is-def-p coq-is-def-p244,8073
-(defun coq-is-decl-defn-p coq-is-decl-defn-p246,8181
-(defun coq-state-preserving-command-p coq-state-preserving-command-p251,8348
-(defun coq-state-preserving-tactic-p coq-state-preserving-tactic-p254,8482
-(defun coq-state-changing-command-p coq-state-changing-command-p257,8614
-(defun coq-section-or-module-start-p coq-section-or-module-start-p263,8922
-(defun coq-find-and-forget coq-find-and-forget271,9175
-(defvar coq-current-goal coq-current-goal363,13742
-(defun coq-goal-hyp coq-goal-hyp366,13807
-(defun coq-state-preserving-p coq-state-preserving-p379,14237
-(defun coq-SearchIsos coq-SearchIsos386,14554
-(defun coq-guess-or-ask-for-string coq-guess-or-ask-for-string400,14988
-(defun coq-Print coq-Print410,15282
-(defun coq-Check coq-Check419,15540
-(defun coq-Show coq-Show428,15782
-(defun coq-PrintHint coq-PrintHint437,16056
-(defun coq-end-Section coq-end-Section443,16199
-(defun coq-Compile coq-Compile461,16783
-(define-key coq-keymap coq-keymap472,17157
-(define-key coq-keymap coq-keymap473,17216
-(define-key coq-keymap coq-keymap474,17274
-(define-key coq-keymap coq-keymap475,17330
-(define-key coq-keymap coq-keymap476,17385
-(define-key coq-keymap coq-keymap477,17435
-(define-key coq-keymap coq-keymap478,17485
-(define-key global-map global-map487,17993
-(defun coq-guess-command-line coq-guess-command-line545,19911
-(defun coq-pre-shell-start coq-pre-shell-start567,20717
-(defun coq-mode-config coq-mode-config578,21159
-(defun coq-shell-mode-config coq-shell-mode-config753,27574
-(defun coq-goals-mode-config coq-goals-mode-config792,29209
-(defun coq-response-config coq-response-config799,29440
-(defpacustom print-only-first-subgoal print-only-first-subgoal820,30030
-(defpacustom auto-compile-vos auto-compile-vos825,30181
-(defun coq-fake-constant-markup coq-fake-constant-markup846,31036
-(defun coq-create-span-menu coq-create-span-menu868,31843
+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
 
 coq/coq-indent.el,1791
 (defconst coq-any-command-regexpcoq-any-command-regexp11,262
@@ -118,96 +135,96 @@ coq/coq-indent.el,1791
 (defun proof-indent-line proof-indent-line514,17532
 
 coq/coq-syntax.el,3214
-(defvar coq-version-is-V74 coq-version-is-V7416,413
-(defvar coq-version-is-V7 coq-version-is-V717,445
-(defvar coq-version-is-V6 coq-version-is-V625,765
-(defvar coq-version-is-V7 coq-version-is-V732,1128
-(defvar coq-version-is-V74 coq-version-is-V7440,1533
-(defvar coq-version-is-V8 coq-version-is-V848,1907
-(defvar coq-keywords-declcoq-keywords-decl122,4413
-(defvar coq-keywords-defncoq-keywords-defn137,4769
-(defun coq-count-match coq-count-match211,7125
-(defun coq-goal-command-p coq-goal-command-p223,7545
-(defvar coq-keywords-save-strictcoq-keywords-save-strict243,8129
-(defvar coq-keywords-savecoq-keywords-save251,8226
-(defun coq-save-command-p coq-save-command-p255,8302
-(defvar coq-keywords-kill-goal coq-keywords-kill-goal263,8581
-(defcustom coq-user-state-changing-commands coq-user-state-changing-commands269,8631
-(defcustom coq-user-state-preserving-commands coq-user-state-preserving-commands281,9028
-(defvar coq-keywords-state-preserving-commandscoq-keywords-state-preserving-commands294,9468
-(defvar coq-keywords-state-changing-misc-commandscoq-keywords-state-changing-misc-commands341,10579
-(defvar coq-keywords-state-changing-commandscoq-keywords-state-changing-commands415,12597
-(defvar coq-keywords-commandscoq-keywords-commands425,12794
-(defcustom coq-user-state-changing-tactics coq-user-state-changing-tactics431,12944
-(defvar coq-state-changing-tacticscoq-state-changing-tactics442,13370
-(defcustom coq-user-state-preserving-tactics coq-user-state-preserving-tactics643,16695
-(defvar coq-state-preserving-tacticscoq-state-preserving-tactics654,17109
-(defvar coq-tacticscoq-tactics658,17207
-(defvar coq-retractable-instructcoq-retractable-instruct661,17296
-(defvar coq-non-retractable-instructcoq-non-retractable-instruct664,17406
-(defvar coq-keywordscoq-keywords668,17528
-(defvar coq-tacticalscoq-tacticals673,17693
-(defvar coq-reserved-commoncoq-reserved-common695,18076
-(defvar coq-reserved-V8coq-reserved-V8711,18269
-(defvar coq-reserved-V7coq-reserved-V7722,18373
-(defvar coq-reserved coq-reserved727,18448
-(defvar coq-symbolscoq-symbols735,18604
-(defvar coq-error-regexp coq-error-regexp753,18808
-(defvar coq-id coq-id756,19024
-(defvar coq-ids coq-ids758,19050
-(defun coq-first-abstr-regexp coq-first-abstr-regexp760,19087
-(defun coq-next-abstr-regexp coq-next-abstr-regexp763,19175
-(defvar coq-font-lock-termscoq-font-lock-terms766,19253
-(defconst coq-save-command-regexp-strictcoq-save-command-regexp-strict781,19906
-(defconst coq-save-command-regexpcoq-save-command-regexp783,20019
-(defconst coq-save-with-hole-regexpcoq-save-with-hole-regexp785,20118
-(defconst coq-goal-command-regexpcoq-goal-command-regexp788,20256
-(defconst coq-goal-with-hole-regexpcoq-goal-with-hole-regexp790,20355
-(defconst coq-decl-with-hole-regexpcoq-decl-with-hole-regexp796,20644
-(defconst coq-defn-with-hole-regexpcoq-defn-with-hole-regexp799,20777
-(defvar coq-font-lock-keywords-1coq-font-lock-keywords-1802,20917
-(defvar coq-font-lock-keywords coq-font-lock-keywords823,21960
-(defun coq-init-syntax-table coq-init-syntax-table825,22018
-(defconst coq-generic-expressioncoq-generic-expression854,22916
+(defvar coq-version-is-V74 coq-version-is-V7416,415
+(defvar coq-version-is-V7 coq-version-is-V717,447
+(defvar coq-version-is-V6 coq-version-is-V625,767
+(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
 
 coq/x-symbol-coq.el,2822
-(defvar x-symbol-coq-required-fonts x-symbol-coq-required-fonts16,382
-(defvar x-symbol-coq-name x-symbol-coq-name24,783
-(defvar x-symbol-coq-modeline-name x-symbol-coq-modeline-name25,823
-(defcustom x-symbol-coq-header-groups-alist x-symbol-coq-header-groups-alist27,866
-(defcustom x-symbol-coq-electric-ignore x-symbol-coq-electric-ignore34,1084
-(defvar x-symbol-coq-required-fonts x-symbol-coq-required-fonts41,1329
-(defvar x-symbol-coq-extra-menu-items x-symbol-coq-extra-menu-items44,1428
-(defvar x-symbol-coq-token-grammarx-symbol-coq-token-grammar48,1516
-(defun x-symbol-coq-default-token-list x-symbol-coq-default-token-list63,2165
-(defvar x-symbol-coq-user-table x-symbol-coq-user-table75,2453
-(defvar x-symbol-coq-generated-data x-symbol-coq-generated-data78,2559
-(defvar x-symbol-coq-master-directory x-symbol-coq-master-directory86,2797
-(defvar x-symbol-coq-image-searchpath x-symbol-coq-image-searchpath87,2845
-(defvar x-symbol-coq-image-cached-dirs x-symbol-coq-image-cached-dirs88,2892
-(defvar x-symbol-coq-image-file-truename-alist x-symbol-coq-image-file-truename-alist89,2957
-(defvar x-symbol-coq-image-keywords x-symbol-coq-image-keywords90,3009
-(defcustom x-symbol-coq-subscript-matcher x-symbol-coq-subscript-matcher98,3257
-(defcustom x-symbol-coq-font-lock-regexp x-symbol-coq-font-lock-regexp104,3489
-(defcustom x-symbol-coq-font-lock-limit-regexp x-symbol-coq-font-lock-limit-regexp109,3661
-(defcustom x-symbol-coq-font-lock-contents-regexp x-symbol-coq-font-lock-contents-regexp115,3849
-(defcustom x-symbol-coq-single-char-regexp x-symbol-coq-single-char-regexp122,4103
-(defun x-symbol-coq-subscript-matcher x-symbol-coq-subscript-matcher127,4251
-(defun coq-match-subscript coq-match-subscript161,5887
-(defvar x-symbol-coq-font-lock-allowed-faces x-symbol-coq-font-lock-allowed-faces168,6106
-(defcustom x-symbol-coq-class-alistx-symbol-coq-class-alist173,6331
-(defcustom x-symbol-coq-class-face-alist x-symbol-coq-class-face-alist184,6709
-(defvar x-symbol-coq-font-lock-keywords x-symbol-coq-font-lock-keywords194,7019
-(defvar x-symbol-coq-font-lock-allowed-faces x-symbol-coq-font-lock-allowed-faces196,7065
-(defvar x-symbol-coq-case-insensitive x-symbol-coq-case-insensitive202,7289
-(defvar x-symbol-coq-token-shape x-symbol-coq-token-shape203,7332
-(defvar x-symbol-coq-input-token-ignore x-symbol-coq-input-token-ignore204,7370
-(defvar x-symbol-coq-token-list x-symbol-coq-token-list205,7415
-(defvar x-symbol-coq-symbol-table x-symbol-coq-symbol-table207,7459
-(defvar x-symbol-coq-xsymbol-table x-symbol-coq-xsymbol-table311,9878
-(defun x-symbol-coq-prepare-table x-symbol-coq-prepare-table458,13746
-(defvar x-symbol-coq-tablex-symbol-coq-table467,14013
-(defcustom x-symbol-coq-auto-stylex-symbol-coq-auto-style474,14174
+(defvar x-symbol-coq-required-fonts x-symbol-coq-required-fonts16,384
+(defvar x-symbol-coq-name x-symbol-coq-name24,785
+(defvar x-symbol-coq-modeline-name x-symbol-coq-modeline-name25,825
+(defcustom x-symbol-coq-header-groups-alist x-symbol-coq-header-groups-alist27,868
+(defcustom x-symbol-coq-electric-ignore x-symbol-coq-electric-ignore34,1086
+(defvar x-symbol-coq-required-fonts x-symbol-coq-required-fonts41,1331
+(defvar x-symbol-coq-extra-menu-items x-symbol-coq-extra-menu-items44,1430
+(defvar x-symbol-coq-token-grammarx-symbol-coq-token-grammar48,1518
+(defun x-symbol-coq-default-token-list x-symbol-coq-default-token-list64,2184
+(defvar x-symbol-coq-user-table x-symbol-coq-user-table76,2472
+(defvar x-symbol-coq-generated-data x-symbol-coq-generated-data79,2578
+(defvar x-symbol-coq-master-directory x-symbol-coq-master-directory87,2816
+(defvar x-symbol-coq-image-searchpath x-symbol-coq-image-searchpath88,2864
+(defvar x-symbol-coq-image-cached-dirs x-symbol-coq-image-cached-dirs89,2911
+(defvar x-symbol-coq-image-file-truename-alist x-symbol-coq-image-file-truename-alist90,2976
+(defvar x-symbol-coq-image-keywords x-symbol-coq-image-keywords91,3028
+(defcustom x-symbol-coq-subscript-matcher x-symbol-coq-subscript-matcher98,3256
+(defcustom x-symbol-coq-font-lock-regexp x-symbol-coq-font-lock-regexp104,3488
+(defcustom x-symbol-coq-font-lock-limit-regexp x-symbol-coq-font-lock-limit-regexp109,3660
+(defcustom x-symbol-coq-font-lock-contents-regexp x-symbol-coq-font-lock-contents-regexp115,3848
+(defcustom x-symbol-coq-single-char-regexp x-symbol-coq-single-char-regexp122,4102
+(defun x-symbol-coq-subscript-matcher x-symbol-coq-subscript-matcher127,4250
+(defun coq-match-subscript coq-match-subscript162,5939
+(defvar x-symbol-coq-font-lock-allowed-faces x-symbol-coq-font-lock-allowed-faces169,6113
+(defcustom x-symbol-coq-class-alistx-symbol-coq-class-alist174,6338
+(defcustom x-symbol-coq-class-face-alist x-symbol-coq-class-face-alist185,6716
+(defvar x-symbol-coq-font-lock-keywords x-symbol-coq-font-lock-keywords195,7026
+(defvar x-symbol-coq-font-lock-allowed-faces x-symbol-coq-font-lock-allowed-faces197,7072
+(defvar x-symbol-coq-case-insensitive x-symbol-coq-case-insensitive203,7296
+(defvar x-symbol-coq-token-shape x-symbol-coq-token-shape204,7339
+(defvar x-symbol-coq-input-token-ignore x-symbol-coq-input-token-ignore205,7377
+(defvar x-symbol-coq-token-list x-symbol-coq-token-list206,7422
+(defvar x-symbol-coq-symbol-table x-symbol-coq-symbol-table208,7466
+(defvar x-symbol-coq-xsymbol-table x-symbol-coq-xsymbol-table312,9885
+(defun x-symbol-coq-prepare-table x-symbol-coq-prepare-table459,13753
+(defvar x-symbol-coq-tablex-symbol-coq-table468,14020
+(defcustom x-symbol-coq-auto-stylex-symbol-coq-auto-style475,14181
 
 demoisa/demoisa-easy.el,0
 
@@ -311,11 +328,16 @@ 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
@@ -348,21 +370,21 @@ generic/pg-response.el,1673
 (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-b142,4896
-(defvar pg-frame-configuration pg-frame-configuration154,5338
-(defun pg-cache-frame-configuration pg-cache-frame-configuration158,5485
-(defun proof-layout-windows proof-layout-windows162,5656
-(defun proof-delete-other-frames proof-delete-other-frames193,6906
-(defvar pg-response-erase-flag pg-response-erase-flag224,8001
-(defun proof-shell-maybe-erase-responseproof-shell-maybe-erase-response227,8116
-(defun pg-response-display pg-response-display257,9266
-(defun pg-response-display-with-face pg-response-display-with-face274,10088
-(defun pg-response-clear-displays pg-response-clear-displays309,11445
-(defvar pg-response-next-error pg-response-next-error326,11975
-(defun proof-next-error proof-next-error330,12097
-(defvar proof-trace-last-fontify-pos proof-trace-last-fontify-pos425,15510
-(defun proof-trace-buffer-display proof-trace-buffer-display428,15602
-(defun pg-thms-buffer-clear pg-thms-buffer-clear468,16822
+(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
 
 generic/pg-thymodes.el,219
 (defmacro pg-defthymode pg-defthymode19,466
@@ -418,11 +440,11 @@ generic/pg-user.el,3521
 (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,34489
-(defun pg-processing-complete-hint pg-processing-complete-hint1035,34605
-(defun pg-hint pg-hint1051,35291
-(defun pg-identifier-under-mouse-query pg-identifier-under-mouse-query1070,35967
-(defun proof-imenu-enable proof-imenu-enable1115,37594
+(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
 
 generic/pg-xhtml.el,573
 (defvar pg-xhtml-dir pg-xhtml-dir17,423
@@ -489,7 +511,7 @@ generic/proof-compat.el,999
 (defun pg-pop-to-buffer pg-pop-to-buffer490,17269
 (defun process-live-p process-live-p541,19121
 
-generic/proof-config.el,16423
+generic/proof-config.el,16702
 (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
@@ -599,116 +621,119 @@ generic/proof-config.el,16423
 (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-indent proof-indent1373,52454
-(defcustom proof-indent-pad-eol proof-indent-pad-eol1379,52628
-(defcustom proof-indent-hang proof-indent-hang1386,52868
-(defcustom proof-indent-enclose-offset proof-indent-enclose-offset1391,52994
-(defcustom proof-indent-open-offset proof-indent-open-offset1396,53136
-(defcustom proof-indent-close-offset proof-indent-close-offset1401,53273
-(defcustom proof-indent-any-regexp proof-indent-any-regexp1406,53411
-(defcustom proof-indent-inner-regexp proof-indent-inner-regexp1411,53571
-(defcustom proof-indent-enclose-regexp proof-indent-enclose-regexp1416,53725
-(defcustom proof-indent-open-regexp proof-indent-open-regexp1421,53879
-(defcustom proof-indent-close-regexp proof-indent-close-regexp1426,54031
-(defcustom proof-script-font-lock-keywords proof-script-font-lock-keywords1432,54185
-(defcustom proof-script-syntax-table-entries proof-script-syntax-table-entries1440,54508
-(defcustom proof-script-span-context-menu-extensions proof-script-span-context-menu-extensions1458,54905
-(defgroup proof-shell proof-shell1484,55694
-(defcustom proof-prog-name proof-prog-name1494,55865
-(defcustom proof-shell-auto-terminate-commands proof-shell-auto-terminate-commands1503,56220
-(defcustom proof-shell-pre-sync-init-cmd proof-shell-pre-sync-init-cmd1512,56617
-(defcustom proof-shell-init-cmd proof-shell-init-cmd1526,57176
-(defcustom proof-shell-restart-cmd proof-shell-restart-cmd1537,57646
-(defcustom proof-shell-quit-cmd proof-shell-quit-cmd1542,57801
-(defcustom proof-shell-quit-timeout proof-shell-quit-timeout1547,57968
-(defcustom proof-shell-cd-cmd proof-shell-cd-cmd1557,58416
-(defcustom proof-shell-start-silent-cmd proof-shell-start-silent-cmd1574,59083
-(defcustom proof-shell-stop-silent-cmd proof-shell-stop-silent-cmd1583,59459
-(defcustom proof-shell-silent-threshold proof-shell-silent-threshold1592,59796
-(defcustom  proof-shell-inform-file-processed-cmd proof-shell-inform-file-processed-cmd1600,60130
-(defcustom  proof-shell-inform-file-retracted-cmd proof-shell-inform-file-retracted-cmd1621,61053
-(defcustom proof-auto-multiple-files proof-auto-multiple-files1644,62094
-(defcustom proof-cannot-reopen-processed-files proof-cannot-reopen-processed-files1659,62815
-(defcustom proof-shell-prompt-pattern proof-shell-prompt-pattern1684,63612
-(defcustom proof-shell-wakeup-char proof-shell-wakeup-char1694,64034
-(defcustom proof-shell-annotated-prompt-regexp proof-shell-annotated-prompt-regexp1700,64265
-(defcustom proof-shell-abort-goal-regexp proof-shell-abort-goal-regexp1716,64905
-(defcustom proof-shell-error-regexp proof-shell-error-regexp1721,65040
-(defcustom proof-shell-truncate-before-error proof-shell-truncate-before-error1741,65834
-(defcustom pg-next-error-regexp pg-next-error-regexp1755,66377
-(defcustom pg-next-error-filename-regexp pg-next-error-filename-regexp1770,66987
-(defcustom pg-next-error-extract-filename pg-next-error-extract-filename1794,68025
-(defcustom proof-shell-interrupt-regexp proof-shell-interrupt-regexp1801,68268
-(defcustom proof-shell-proof-completed-regexp proof-shell-proof-completed-regexp1815,68860
-(defcustom proof-shell-clear-response-regexp proof-shell-clear-response-regexp1828,69368
-(defcustom proof-shell-clear-goals-regexp proof-shell-clear-goals-regexp1835,69667
-(defcustom proof-shell-start-goals-regexp proof-shell-start-goals-regexp1842,69960
-(defcustom proof-shell-end-goals-regexp proof-shell-end-goals-regexp1850,70327
-(defcustom proof-shell-eager-annotation-start proof-shell-eager-annotation-start1856,70569
-(defcustom proof-shell-eager-annotation-start-length proof-shell-eager-annotation-start-length1874,71307
-(defcustom proof-shell-eager-annotation-end proof-shell-eager-annotation-end1885,71734
-(defcustom proof-shell-assumption-regexp proof-shell-assumption-regexp1901,72410
-(defcustom proof-shell-process-file proof-shell-process-file1911,72822
-(defcustom proof-shell-retract-files-regexp proof-shell-retract-files-regexp1933,73774
-(defcustom proof-shell-compute-new-files-list proof-shell-compute-new-files-list1942,74110
-(defcustom pg-use-specials-for-fontify pg-use-specials-for-fontify1954,74655
-(defcustom proof-shell-set-elisp-variable-regexp proof-shell-set-elisp-variable-regexp1962,74979
-(defcustom proof-shell-match-pgip-cmd proof-shell-match-pgip-cmd1995,76451
-(defcustom proof-shell-issue-pgip-cmd proof-shell-issue-pgip-cmd2004,76781
-(defcustom proof-shell-query-dependencies-cmd proof-shell-query-dependencies-cmd2013,77137
-(defcustom proof-shell-theorem-dependency-list-regexp proof-shell-theorem-dependency-list-regexp2020,77397
-(defcustom proof-shell-theorem-dependency-list-split proof-shell-theorem-dependency-list-split2036,78057
-(defcustom proof-shell-show-dependency-cmd proof-shell-show-dependency-cmd2045,78482
-(defcustom proof-shell-identifier-under-mouse-cmd proof-shell-identifier-under-mouse-cmd2052,78751
-(defcustom proof-shell-trace-output-regexp proof-shell-trace-output-regexp2075,79832
-(defcustom proof-shell-thms-output-regexp proof-shell-thms-output-regexp2091,80376
-(defcustom proof-shell-filename-escapes proof-shell-filename-escapes2103,80761
-(defcustom proof-shell-process-connection-type proof-shell-process-connection-type2120,81441
-(defcustom proof-shell-strip-crs-from-input proof-shell-strip-crs-from-input2140,82319
-(defcustom proof-shell-strip-crs-from-output proof-shell-strip-crs-from-output2152,82808
-(defcustom proof-shell-insert-hook proof-shell-insert-hook2160,83176
-(defcustom proof-pre-shell-start-hook proof-pre-shell-start-hook2200,85140
-(defcustom proof-shell-handle-delayed-output-hookproof-shell-handle-delayed-output-hook2216,85612
-(defcustom proof-shell-handle-error-or-interrupt-hookproof-shell-handle-error-or-interrupt-hook2222,85827
-(defcustom proof-shell-pre-interrupt-hookproof-shell-pre-interrupt-hook2237,86441
-(defcustom proof-shell-process-output-system-specific proof-shell-process-output-system-specific2247,86811
-(defcustom proof-state-change-hook proof-state-change-hook2266,87676
-(defcustom proof-shell-font-lock-keywords proof-shell-font-lock-keywords2277,88058
-(defcustom proof-shell-syntax-table-entries proof-shell-syntax-table-entries2285,88386
-(defgroup proof-goals proof-goals2303,88758
-(defcustom pg-subterm-first-special-char pg-subterm-first-special-char2308,88879
-(defcustom pg-subterm-anns-use-stack pg-subterm-anns-use-stack2316,89191
-(defcustom pg-goals-change-goal pg-goals-change-goal2325,89495
-(defcustom pbp-goal-command pbp-goal-command2330,89610
-(defcustom pbp-hyp-command pbp-hyp-command2335,89766
-(defcustom pg-subterm-help-cmd pg-subterm-help-cmd2340,89928
-(defcustom pg-goals-error-regexp pg-goals-error-regexp2347,90164
-(defcustom proof-shell-result-start proof-shell-result-start2352,90324
-(defcustom proof-shell-result-end proof-shell-result-end2358,90558
-(defcustom pg-subterm-start-char pg-subterm-start-char2364,90771
-(defcustom pg-subterm-sep-char pg-subterm-sep-char2378,91353
-(defcustom pg-subterm-end-char pg-subterm-end-char2384,91532
-(defcustom pg-topterm-char pg-topterm-char2390,91689
-(defcustom proof-goals-font-lock-keywords proof-goals-font-lock-keywords2407,92295
-(defcustom proof-resp-font-lock-keywords proof-resp-font-lock-keywords2421,92974
-(defcustom pg-before-fontify-output-hook pg-before-fontify-output-hook2433,93552
-(defcustom pg-after-fontify-output-hook pg-after-fontify-output-hook2441,93912
-(defgroup proof-x-symbol proof-x-symbol2453,94166
-(defcustom proof-xsym-extra-modes proof-xsym-extra-modes2458,94294
-(defcustom proof-xsym-font-lock-keywords proof-xsym-font-lock-keywords2471,94923
-(defcustom proof-xsym-activate-command proof-xsym-activate-command2479,95300
-(defcustom proof-xsym-deactivate-command proof-xsym-deactivate-command2486,95536
-(defpgcustom x-symbol-language x-symbol-language2493,95778
-(defpgcustom favourites favourites2508,96225
-(defpgcustom menu-entries menu-entries2513,96415
-(defpgcustom help-menu-entries help-menu-entries2520,96652
-(defpgcustom keymap keymap2527,96915
-(defpgcustom completion-table completion-table2532,97086
-(defpgcustom tags-program tags-program2542,97451
-(defcustom proof-general-name proof-general-name2554,97624
-(defcustom proof-general-home-pageproof-general-home-page2559,97781
-(defcustom proof-unnamed-theorem-nameproof-unnamed-theorem-name2565,97940
-(defcustom proof-universal-keysproof-universal-keys2573,98216
+(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
 
 generic/proof-depends.el,1325
 (defvar proof-thm-names-of-files proof-thm-names-of-files19,540
@@ -762,7 +787,7 @@ generic/proof-indent.el,475
 (defun proof-indent-pad-eol proof-indent-pad-eol98,3376
 (defun proof-indent-pad-eol-region proof-indent-pad-eol-region116,3970
 
-generic/proof-menu.el,4254
+generic/proof-menu.el,4166
 (defvar proof-display-some-buffers-count proof-display-some-buffers-count19,467
 (defun proof-display-some-buffers proof-display-some-buffers21,512
 (defun proof-menu-define-keys proof-menu-define-keys80,2714
@@ -776,79 +801,76 @@ generic/proof-menu.el,4254
 (define-key map map90,3256
 (define-key map map92,3377
 (define-key map map93,3441
-(define-key map map94,3496
-(define-key map map95,3567
-(define-key map map96,3632
-(define-key map map97,3714
-(define-key map map98,3768
-(define-key map map99,3833
-(define-key map map100,3907
-(define-key map map101,3962
-(define-key map map103,4100
-(define-key map map104,4166
-(define-key map map106,4316
-(define-key map map107,4386
-(define-key map map108,4452
-(define-key map map110,4567
-(define-key map map111,4630
-(define-key map map113,4715
-(define-key map map120,5041
-(define-key map map121,5100
-(defun proof-menu-define-main proof-menu-define-main141,5690
-(defun proof-menu-define-specific proof-menu-define-specific151,5891
-(defun proof-assistant-menu-update proof-assistant-menu-update186,6908
-(defvar proof-help-menuproof-help-menu200,7339
-(defvar proof-show-hide-menuproof-show-hide-menu208,7617
-(defvar proof-buffer-menuproof-buffer-menu217,7930
-(defconst proof-quick-opts-menuproof-quick-opts-menu272,9922
-(defun proof-quick-opts-vars proof-quick-opts-vars380,14353
-(defun proof-quick-opts-changed-from-defaults-p proof-quick-opts-changed-from-defaults-p403,15035
-(defun proof-quick-opts-changed-from-saved-p proof-quick-opts-changed-from-saved-p407,15140
-(defun proof-quick-opts-save proof-quick-opts-save418,15492
-(defun proof-quick-opts-reset proof-quick-opts-reset423,15660
-(defconst proof-config-menuproof-config-menu435,15928
-(defconst proof-advanced-menuproof-advanced-menu442,16107
-(defvar proof-menu proof-menu461,16888
-(defvar proof-main-menuproof-main-menu470,17172
-(defvar proof-aux-menuproof-aux-menu480,17398
-(defvar proof-menu-favourites proof-menu-favourites496,17720
-(defun proof-menu-define-favourites-menu proof-menu-define-favourites-menu499,17827
-(defmacro proof-defshortcut proof-defshortcut520,18498
-(defmacro proof-definvisible proof-definvisible536,19153
-(defun proof-def-favourite proof-def-favourite551,19772
-(defvar proof-make-favourite-cmd-history proof-make-favourite-cmd-history574,20747
-(defvar proof-make-favourite-menu-history proof-make-favourite-menu-history577,20832
-(defun proof-save-favourites proof-save-favourites580,20918
-(defun proof-del-favourite proof-del-favourite585,21066
-(defun proof-read-favourite proof-read-favourite602,21627
-(defun proof-add-favourite proof-add-favourite627,22430
-(defvar proof-assistant-settings proof-assistant-settings654,23481
-(defvar proof-menu-settings proof-menu-settings661,23844
-(defun proof-menu-define-settings-menu proof-menu-define-settings-menu664,23918
-(defun proof-menu-entry-name proof-menu-entry-name682,24562
-(defun proof-menu-entry-for-setting proof-menu-entry-for-setting687,24721
-(defun proof-settings-vars proof-settings-vars705,25211
-(defun proof-settings-changed-from-defaults-p proof-settings-changed-from-defaults-p710,25388
-(defun proof-settings-changed-from-saved-p proof-settings-changed-from-saved-p714,25494
-(defun proof-settings-save proof-settings-save718,25597
-(defun proof-settings-reset proof-settings-reset723,25764
-(defun proof-defpacustom-fn proof-defpacustom-fn731,26010
-(defmacro defpacustom defpacustom791,28202
-(defun proof-assistant-invisible-command-ifposs proof-assistant-invisible-command-ifposs802,28842
-(defun proof-maybe-askprefs proof-maybe-askprefs821,29691
-(defun proof-assistant-settings-cmd proof-assistant-settings-cmd828,29895
-(defun proof-assistant-format proof-assistant-format845,30555
-(defvar proof-assistant-format-table proof-assistant-format-table862,31297
-(defun proof-assistant-format-bool proof-assistant-format-bool870,31666
-(defun proof-assistant-format-int proof-assistant-format-int873,31779
-(defun proof-assistant-format-string proof-assistant-format-string876,31871
+(define-key map map96,3619
+(define-key map map97,3690
+(define-key map map98,3744
+(define-key map map99,3809
+(define-key map map100,3883
+(define-key map map103,4064
+(define-key map map104,4130
+(define-key map map106,4280
+(define-key map map107,4350
+(define-key map map108,4416
+(define-key map map110,4531
+(define-key map map111,4594
+(define-key map map113,4679
+(define-key map map120,5005
+(define-key map map121,5064
+(defun proof-menu-define-main proof-menu-define-main141,5654
+(defun proof-menu-define-specific proof-menu-define-specific151,5855
+(defun proof-assistant-menu-update proof-assistant-menu-update186,6872
+(defvar proof-help-menuproof-help-menu200,7303
+(defvar proof-show-hide-menuproof-show-hide-menu208,7581
+(defvar proof-buffer-menuproof-buffer-menu217,7894
+(defconst proof-quick-opts-menuproof-quick-opts-menu272,9886
+(defun proof-quick-opts-vars proof-quick-opts-vars380,14317
+(defun proof-quick-opts-changed-from-defaults-p proof-quick-opts-changed-from-defaults-p403,14999
+(defun proof-quick-opts-changed-from-saved-p proof-quick-opts-changed-from-saved-p407,15104
+(defun proof-quick-opts-save proof-quick-opts-save418,15456
+(defun proof-quick-opts-reset proof-quick-opts-reset423,15624
+(defconst proof-config-menuproof-config-menu435,15892
+(defconst proof-advanced-menuproof-advanced-menu442,16071
+(defvar proof-menu proof-menu458,16650
+(defvar proof-main-menuproof-main-menu467,16934
+(defvar proof-aux-menuproof-aux-menu477,17160
+(defvar proof-menu-favourites proof-menu-favourites493,17482
+(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
 
 generic/proof-mmm.el,179
 (defun proof-mmm-support-available proof-mmm-support-available25,909
 (defun proof-mmm-set-global proof-mmm-set-global49,1757
 (defun proof-mmm-enable proof-mmm-enable64,2298
 
-generic/proof-script.el,8106
+generic/proof-script.el,8107
 (defvar proof-last-theorem-dependencies proof-last-theorem-dependencies41,1046
 (defvar proof-nesting-depth proof-nesting-depth45,1208
 (defvar proof-element-counters proof-element-counters52,1439
@@ -884,83 +906,83 @@ generic/proof-script.el,8106
 (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-window456,16237
-(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-window467,16718
-(defun proof-end-of-locked-visible-p proof-end-of-locked-visible-p481,17371
-(defun proof-goto-end-of-queue-or-locked-if-not-visible proof-goto-end-of-queue-or-locked-if-not-visible490,17822
-(defvar pg-idioms pg-idioms509,18472
-(defvar pg-visibility-specs pg-visibility-specs512,18568
-(deflocal pg-script-portions pg-script-portions517,18775
-(defun pg-clear-script-portions pg-clear-script-portions520,18897
-(defun pg-add-script-element pg-add-script-element538,19561
-(defun pg-remove-script-element pg-remove-script-element541,19637
-(defsubst pg-visname pg-visname549,19915
-(defun pg-add-element pg-add-element553,20060
-(defun pg-open-invisible-span pg-open-invisible-span587,21689
-(defun pg-remove-element pg-remove-element598,22052
-(defun pg-make-element-invisible pg-make-element-invisible605,22322
-(defun pg-make-element-visible pg-make-element-visible611,22579
-(defun pg-toggle-element-visibility pg-toggle-element-visibility616,22758
-(defun pg-redisplay-for-gnuemacs pg-redisplay-for-gnuemacs624,23088
-(defun pg-show-all-portions pg-show-all-portions631,23359
-(defun pg-show-all-proofs pg-show-all-proofs649,24030
-(defun pg-hide-all-proofs pg-hide-all-proofs654,24158
-(defun pg-add-proof-element pg-add-proof-element659,24289
-(defun pg-span-name pg-span-name673,24909
-(defun pg-set-span-helphighlights pg-set-span-helphighlights694,25616
-(defun proof-complete-buffer-atomic proof-complete-buffer-atomic719,26440
-(defun proof-register-possibly-new-processed-file proof-register-possibly-new-processed-file760,28355
-(defun proof-inform-prover-file-retracted proof-inform-prover-file-retracted811,30483
-(defun proof-auto-retract-dependencies proof-auto-retract-dependencies818,30715
-(defun proof-unregister-buffer-file-name proof-unregister-buffer-file-name872,33255
-(defun proof-protected-process-or-retract proof-protected-process-or-retract918,35078
-(defun proof-deactivate-scripting-auto proof-deactivate-scripting-auto945,36248
-(defun proof-deactivate-scripting proof-deactivate-scripting954,36606
-(defun proof-activate-scripting proof-activate-scripting1088,41898
-(defun proof-toggle-active-scripting proof-toggle-active-scripting1216,47652
-(defun proof-done-advancing proof-done-advancing1257,49013
-(defun proof-done-advancing-comment proof-done-advancing-comment1327,51784
-(defun proof-done-advancing-save proof-done-advancing-save1346,52526
-(defun proof-make-goalsave proof-make-goalsave1439,56139
-(defun proof-get-name-from-goal proof-get-name-from-goal1454,56882
-(defun proof-done-advancing-autosave proof-done-advancing-autosave1473,57908
-(defun proof-done-advancing-other proof-done-advancing-other1537,60425
-(defun proof-segment-up-to-parser proof-segment-up-to-parser1565,61405
-(defun proof-script-generic-parse-find-comment-end proof-script-generic-parse-find-comment-end1628,63481
-(defun proof-script-generic-parse-cmdend proof-script-generic-parse-cmdend1637,63897
-(defun proof-script-generic-parse-cmdstart proof-script-generic-parse-cmdstart1662,64792
-(defun proof-script-generic-parse-sexp proof-script-generic-parse-sexp1725,67500
-(defun proof-cmdstart-add-segment-for-cmd proof-cmdstart-add-segment-for-cmd1749,68436
-(defun proof-segment-up-to-cmdstart proof-segment-up-to-cmdstart1801,70635
-(defun proof-segment-up-to-cmdend proof-segment-up-to-cmdend1862,72995
-(defun proof-semis-to-vanillas proof-semis-to-vanillas1933,75640
-(defun proof-script-new-command-advance proof-script-new-command-advance1972,76966
-(defun proof-script-next-command-advance proof-script-next-command-advance2014,78707
-(defun proof-assert-until-point-interactive proof-assert-until-point-interactive2026,79148
-(defun proof-assert-until-point proof-assert-until-point2052,80270
-(defun proof-assert-next-commandproof-assert-next-command2105,82702
-(defun proof-goto-point proof-goto-point2153,84965
-(defun proof-insert-pbp-command proof-insert-pbp-command2170,85491
-(defun proof-done-retracting proof-done-retracting2202,86564
-(defun proof-setup-retract-action proof-setup-retract-action2229,87675
-(defun proof-last-goal-or-goalsave proof-last-goal-or-goalsave2239,88158
-(defun proof-retract-target proof-retract-target2263,89027
-(defun proof-retract-until-point-interactive proof-retract-until-point-interactive2348,92668
-(defun proof-retract-until-point proof-retract-until-point2356,93053
-(define-derived-mode proof-mode proof-mode2401,94914
-(defun proof-script-set-visited-file-name proof-script-set-visited-file-name2434,96231
-(defun proof-script-set-buffer-hooks proof-script-set-buffer-hooks2458,97233
-(defun proof-script-kill-buffer-fn proof-script-kill-buffer-fn2468,97729
-(defun proof-config-done-related proof-config-done-related2512,99551
-(defun proof-generic-goal-command-p proof-generic-goal-command-p2582,102117
-(defun proof-generic-state-preserving-p proof-generic-state-preserving-p2586,102292
-(defun proof-generic-count-undos proof-generic-count-undos2595,102809
-(defun proof-generic-find-and-forget proof-generic-find-and-forget2624,103839
-(defconst proof-script-important-settingsproof-script-important-settings2675,105664
-(defun proof-config-done proof-config-done2688,106201
-(defun proof-setup-parsing-mechanism proof-setup-parsing-mechanism2785,109749
-(defun proof-setup-imenu proof-setup-imenu2829,111602
-(defun proof-setup-func-menu proof-setup-func-menu2846,112207
+(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
 (defvar proof-shell-last-output proof-shell-last-output19,458
@@ -1025,17 +1047,17 @@ generic/proof-shell.el,5288
 (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,69687
-(defun proof-shell-dont-show-annotations proof-shell-dont-show-annotations1789,69957
-(defun proof-shell-show-annotations proof-shell-show-annotations1805,70492
-(defun proof-shell-wait proof-shell-wait1826,70989
-(defun proof-done-invisible proof-done-invisible1846,71899
-(defun proof-shell-invisible-command proof-shell-invisible-command1889,73622
-(defun proof-shell-invisible-cmd-get-result proof-shell-invisible-cmd-get-result1916,74811
-(defun proof-shell-invisible-command-invisible-result proof-shell-invisible-command-invisible-result1933,75492
-(define-derived-mode proof-shell-mode proof-shell-mode1953,75996
-(defconst proof-shell-important-settingsproof-shell-important-settings2023,78599
-(defun proof-shell-config-done proof-shell-config-done2028,78699
+(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
@@ -1045,17 +1067,17 @@ generic/proof-site.el,1154
 (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,5373
-(defcustom proof-assistants proof-assistants172,5864
-(defun proof-ready-for-assistant proof-ready-for-assistant220,7689
-(defconst proof-general-version proof-general-version335,11982
-(defcustom proof-assistant-cusgrp proof-assistant-cusgrp350,12555
-(defcustom proof-assistant-internals-cusgrp proof-assistant-internals-cusgrp358,12858
-(defcustom proof-assistant proof-assistant366,13170
-(defcustom proof-assistant-symbol proof-assistant-symbol374,13439
-(defvar proof-running-on-XEmacs proof-running-on-XEmacs391,13987
-(defvar proof-running-on-Emacs21 proof-running-on-Emacs21393,14109
-(defvar proof-running-on-win32 proof-running-on-win32397,14356
+(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
 
 generic/proof-splash.el,976
 (defcustom proof-splash-enable proof-splash-enable14,379
@@ -1159,58 +1181,59 @@ 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,3027
+generic/proof-utils.el,3092
 (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
 (defmacro proof-map-buffers proof-map-buffers45,1473
 (defmacro proof-sym proof-sym50,1658
 (defun proof-try-require proof-try-require55,1819
-(defun proof-set-value proof-set-value67,2160
-(defun proof-ass-symv proof-ass-symv127,4337
-(defmacro proof-ass-sym proof-ass-sym132,4524
-(defun proof-defpgcustom-fn proof-defpgcustom-fn136,4663
-(defun undefpgcustom undefpgcustom161,5747
-(defmacro defpgcustom defpgcustom167,5971
-(defmacro proof-ass proof-ass176,6388
-(defun proof-defpgdefault-fn proof-defpgdefault-fn181,6564
-(defmacro defpgdefault defpgdefault195,7023
-(defmacro defpgfun defpgfun206,7385
-(defun proof-file-truename proof-file-truename221,7679
-(defun proof-file-to-buffer proof-file-to-buffer225,7862
-(defun proof-files-to-buffers proof-files-to-buffers236,8191
-(defun proof-buffers-in-mode proof-buffers-in-mode243,8474
-(defun pg-save-from-death pg-save-from-death257,8925
-(defun proof-define-keys proof-define-keys276,9535
-(deflocal proof-font-lock-keywords proof-font-lock-keywords305,10536
-(deflocal proof-font-lock-keywords-case-fold-search proof-font-lock-keywords-case-fold-search311,10801
-(defun proof-font-lock-configure-defaults proof-font-lock-configure-defaults314,10924
-(defun proof-font-lock-clear-font-lock-vars proof-font-lock-clear-font-lock-vars362,13237
-(defun proof-font-lock-set-font-lock-vars proof-font-lock-set-font-lock-vars373,13610
-(defun proof-fontify-region proof-fontify-region380,13823
-(defconst pg-special-char-regexp pg-special-char-regexp434,15789
-(defun pg-remove-specials pg-remove-specials438,15901
-(defun proof-fontify-buffer proof-fontify-buffer452,16326
-(defun proof-warn-if-unset proof-warn-if-unset465,16567
-(defun proof-get-window-for-buffer proof-get-window-for-buffer470,16785
-(defun proof-display-and-keep-buffer proof-display-and-keep-buffer507,18437
-(defun proof-clean-buffer proof-clean-buffer538,19713
-(defun proof-message proof-message550,20191
-(defun proof-warning proof-warning555,20404
-(defun proof-debug proof-debug562,20738
-(defun proof-switch-to-buffer proof-switch-to-buffer575,21229
-(defun proof-resize-window-tofit proof-resize-window-tofit608,22921
-(defun proof-submit-bug-report proof-submit-bug-report708,26949
-(defun proof-deftoggle-fn proof-deftoggle-fn731,27728
-(defmacro proof-deftoggle proof-deftoggle746,28383
-(defun proof-defintset-fn proof-defintset-fn753,28757
-(defmacro proof-defintset proof-defintset767,29412
-(defun proof-defstringset-fn proof-defstringset-fn774,29789
-(defmacro proof-defstringset proof-defstringset787,30416
-(defun pg-custom-save-vars pg-custom-save-vars801,30881
-(defun pg-custom-reset-vars pg-custom-reset-vars819,31607
-(defun proof-locate-executable proof-locate-executable832,31944
-(defconst proof-extra-flsproof-extra-fls864,33357
+(defun proof-save-some-buffers proof-save-some-buffers68,2147
+(defun proof-set-value proof-set-value92,2838
+(defun proof-ass-symv proof-ass-symv152,5015
+(defmacro proof-ass-sym proof-ass-sym157,5202
+(defun proof-defpgcustom-fn proof-defpgcustom-fn161,5341
+(defun undefpgcustom undefpgcustom186,6425
+(defmacro defpgcustom defpgcustom192,6649
+(defmacro proof-ass proof-ass201,7066
+(defun proof-defpgdefault-fn proof-defpgdefault-fn206,7242
+(defmacro defpgdefault defpgdefault220,7701
+(defmacro defpgfun defpgfun231,8063
+(defun proof-file-truename proof-file-truename246,8357
+(defun proof-file-to-buffer proof-file-to-buffer250,8540
+(defun proof-files-to-buffers proof-files-to-buffers261,8869
+(defun proof-buffers-in-mode proof-buffers-in-mode268,9152
+(defun pg-save-from-death pg-save-from-death282,9603
+(defun proof-define-keys proof-define-keys301,10213
+(deflocal proof-font-lock-keywords proof-font-lock-keywords330,11214
+(deflocal proof-font-lock-keywords-case-fold-search proof-font-lock-keywords-case-fold-search336,11479
+(defun proof-font-lock-configure-defaults proof-font-lock-configure-defaults339,11602
+(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
 
 generic/proof-x-symbol.el,960
 (defvar proof-x-symbol-initialized proof-x-symbol-initialized53,2149
@@ -1323,10 +1346,10 @@ generic/texi-docstring-magic.el,958
 (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-comment323,11713
-(defun texi-docstring-magic texi-docstring-magic329,11867
-(defun texi-docstring-magic-face-at-point texi-docstring-magic-face-at-point353,12579
-(defun texi-docstring-magic-insert-magic texi-docstring-magic-insert-magic368,13102
+(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
 
 hol98/hol98.el,0
 
@@ -1567,11 +1590,11 @@ isa/x-symbol-isabelle.el,3169
 (defvar x-symbol-isabelle-input-token-ignore x-symbol-isabelle-input-token-ignore206,7902
 (defvar x-symbol-isabelle-token-list x-symbol-isabelle-token-list207,7952
 (defvar x-symbol-isabelle-symbol-table x-symbol-isabelle-symbol-table209,8001
-(defvar x-symbol-isabelle-xsymbol-table x-symbol-isabelle-xsymbol-table308,10712
-(defun x-symbol-isabelle-prepare-table x-symbol-isabelle-prepare-table453,15114
-(defvar x-symbol-isabelle-tablex-symbol-isabelle-table465,15525
-(defcustom x-symbol-isabelle-auto-stylex-symbol-isabelle-auto-style479,15878
-(defcustom x-symbol-isabelle-auto-coding-alist x-symbol-isabelle-auto-coding-alist493,16388
+(defvar x-symbol-isabelle-xsymbol-table x-symbol-isabelle-xsymbol-table309,10737
+(defun x-symbol-isabelle-prepare-table x-symbol-isabelle-prepare-table454,15139
+(defvar x-symbol-isabelle-tablex-symbol-isabelle-table466,15550
+(defcustom x-symbol-isabelle-auto-stylex-symbol-isabelle-auto-style480,15903
+(defcustom x-symbol-isabelle-auto-coding-alist x-symbol-isabelle-auto-coding-alist494,16413
 
 isa/x-symbol-isa.el,0
 
@@ -1598,14 +1621,14 @@ isar/isar.el,1883
 (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-width521,19757
-(defun isar-shell-adjust-line-width isar-shell-adjust-line-width527,19975
-(defun isar-pre-shell-start isar-pre-shell-start547,20858
-(defun isar-preprocessing isar-preprocessing559,21194
-(defun isar-mode-config isar-mode-config582,22405
-(defun isar-shell-mode-config isar-shell-mode-config593,22908
-(defun isar-response-mode-config isar-response-mode-config604,23278
-(defun isar-goals-mode-config isar-goals-mode-config613,23535
+(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
 
 isar/isar-keywords.el,1650
 (defconst isar-keywords-majorisar-keywords-major14,378
@@ -2223,14 +2246,14 @@ plastic/plastic.el,4425
 (defun plastic-reset-error plastic-reset-error648,23100
 (defun plastic-call-if-no-error plastic-call-if-no-error651,23239
 (defun plastic-show-shell plastic-show-shell656,23443
-(define-key plastic-keymap plastic-keymap664,23650
-(define-key plastic-keymap plastic-keymap665,23700
-(define-key plastic-keymap plastic-keymap666,23750
-(define-key plastic-keymap plastic-keymap667,23799
-(define-key plastic-keymap plastic-keymap668,23847
-(define-key plastic-keymap plastic-keymap669,23895
-(defalias 'proof-toolbar-command proof-toolbar-command679,24134
-(defalias 'proof-minibuffer-cmd proof-minibuffer-cmd680,24185
+(define-key plastic-keymap plastic-keymap665,23705
+(define-key plastic-keymap plastic-keymap666,23766
+(define-key plastic-keymap plastic-keymap667,23827
+(define-key plastic-keymap plastic-keymap668,23887
+(define-key plastic-keymap plastic-keymap669,23946
+(define-key plastic-keymap plastic-keymap670,24005
+(defalias 'proof-toolbar-command proof-toolbar-command680,24255
+(defalias 'proof-minibuffer-cmd proof-minibuffer-cmd681,24306
 
 plastic/plastic-syntax.el,1015
 (defconst plastic-keywords-goal plastic-keywords-goal18,537
@@ -2472,35 +2495,35 @@ twelf/twelf-old.el,10513
 
 twelf/x-symbol-twelf.el,0
 
-todo,1296
-   function to to364,15045
+todo,1297
+   function to to373,15257
 $Id: todo,2,21
 This is an outline file.   Use C-c C-n,4,67
-X 32,944
-*** C Improved configurability of command settings,163,6426
-  We should let command settings,164,6483
-  We should let command settings, etc,164,6483
-  - XEmacs pg forces on font-lock,314,12632
-    Save foo;390,16168
-*** A Doc new bits: font lock keywords,460,18869
-*** A Doc new bits: font lock keywords, filename %e,460,18869
-  Added proof-{script,461,18926
-  Added proof-{script,shell,461,18926
-  Added proof-{script,shell,goals,461,18926
-  Presently used only in proof-easy-config,462,18986
-  - Mention configuring function menus,473,19322
-  - document mouse functions,475,19408
-  - document mouse functions, proof-cd,475,19408
-  - document mouse functions, proof-cd, process quit timeout,475,19408
-    X-Symbol,476,19471
-    X-Symbol, prog-name-guess,476,19471
-*** D Fix INFO-DIR-ENTRY in 490,19979
-*** C Fixing up errors caused by pbp-generated commands; currently,556,22430
-  should mean generates an error.  With LEGO pbp,559,22636
-  tactic which always succeeds,560,22700
-  decodes annotations eagerly. Lazily would be faster,568,23056
-  the tech report claims --- djs: probably not much faster,569,23125
-***  6. Update Emacs and prover versions in texi,658,26128
+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
@@ -2523,80 +2546,80 @@ doc/ProofGeneral.texi,5815
 @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 commands1330,50615
-@node Proof assistant commandsProof assistant commands1458,55916
-@node Toolbar commandsToolbar commands1620,61579
-@node Interrupting during trace outputInterrupting during trace output1644,62508
-@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing1683,64431
-@node Goals buffer commandsGoals buffer commands1697,64931
-@node Advanced Script ManagementAdvanced Script Management1787,68464
-@node Visibility of completed proofsVisibility of completed proofs1818,69618
-@node Switching between proof scriptsSwitching between proof scripts1873,71541
-@node View of processed files View of processed files 1910,73513
-@node Retracting across filesRetracting across files1970,76564
-@node Asserting across filesAsserting across files1983,77195
-@node Automatic multiple file handlingAutomatic multiple file handling1996,77761
-@node Escaping script managementEscaping script management2021,78795
-@node Experimental featuresExperimental features2079,80998
-@node Support for other PackagesSupport for other Packages2113,82260
-@node Syntax highlightingSyntax highlighting2145,83135
-@node X-Symbol supportX-Symbol support2184,84744
-@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)2243,87290
-@node Support for outline modeSupport for outline mode2302,89420
-@node Support for completionSupport for completion2328,90550
-@node Support for tagsSupport for tags2385,92713
-@node Customizing Proof GeneralCustomizing Proof General2437,95041
-@node Basic optionsBasic options2477,96711
-@node How to customizeHow to customize2501,97469
-@node Display customizationDisplay customization2552,99559
-@node User optionsUser options2666,104169
-@node Changing facesChanging faces2920,113175
-@node Tweaking configuration settingsTweaking configuration settings2995,115844
-@node Hints and TipsHints and Tips3052,118369
-@node Adding your own keybindingsAdding your own keybindings3071,118970
-@node Using file variablesUsing file variables3127,121503
-@node Using abbreviationsUsing abbreviations3180,123326
-@node LEGO Proof GeneralLEGO Proof General3219,124741
-@node LEGO specific commandsLEGO specific commands3260,126110
-@node LEGO tagsLEGO tags3280,126565
-@node LEGO customizationsLEGO customizations3290,126812
-@node Coq Proof GeneralCoq Proof General3322,127730
-@node Coq-specific commandsCoq-specific commands3338,128139
-@node Coq-specific variablesCoq-specific variables3360,128646
-@node Editing multiple proofsEditing multiple proofs3398,129861
-@node User-loaded tacticsUser-loaded tactics3422,130969
-@node Holes featureHoles feature3487,133496
-@node Isabelle Proof GeneralIsabelle Proof General3514,134782
-@node Classic IsabelleClassic Isabelle3583,138105
-@node ML filesML files3599,138543
-@node Theory filesTheory files3670,140968
-@node General commands for IsabelleGeneral commands for Isabelle3724,143439
-@node Specific commands for IsabelleSpecific commands for Isabelle3736,143921
-@node Isabelle customizationsIsabelle customizations3765,144861
-@node Isabelle/IsarIsabelle/Isar3830,146959
-@node General commands for Isabelle/IsarGeneral commands for Isabelle/Isar3851,147722
-@node Specific commands for Isabelle/IsarSpecific commands for Isabelle/Isar3858,147976
-@node Logics and SettingsLogics and Settings3945,150504
-@node HOL Proof GeneralHOL Proof General3986,152192
-@node Shell Proof GeneralShell Proof General4027,153976
-@node Obtaining and InstallingObtaining and Installing4063,155434
-@node Obtaining Proof GeneralObtaining Proof General4079,155847
-@node Installing Proof General from tarballInstalling Proof General from tarball4110,157086
-@node Installing Proof General from RPM packageInstalling Proof General from RPM package4135,157918
-@node Setting the names of binariesSetting the names of binaries4150,158326
-@node Notes for syssiesNotes for syssies4178,159254
-@node Known bugs and workaroundsKnown bugs and workarounds4251,162203
-@node ReferencesReferences4264,162636
-@node History of Proof GeneralHistory of Proof General4304,163660
-@node Old News for 3.0Old News for 3.04395,167762
-@node Old News for 3.1Old News for 3.14465,171456
-@node Old News for 3.2Old News for 3.24491,172628
-@node Old News for 3.3Old News for 3.34552,175631
-@node Old News for 3.4Old News for 3.44571,176528
-@node Function IndexFunction Index4594,177584
-@node Variable IndexVariable Index4598,177660
-@node Keystroke IndexKeystroke Index4602,177740
-@node Concept IndexConcept Index4606,177806
+@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
@@ -2614,45 +2637,45 @@ doc/PG-adapting.texi,3791
 @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 elements936,37640
-@node Configuring undo behaviourConfiguring undo behaviour1062,43118
-@node Nested proofsNested proofs1201,48460
-@node Safe (state-preserving) commandsSafe (state-preserving) commands1241,50087
-@node Activate scripting hookActivate scripting hook1264,51033
-@node Automatic multiple filesAutomatic multiple files1288,51897
-@node CompletionsCompletions1310,52744
-@node Proof shell settingsProof shell settings1350,54220
-@node Proof shell commandsProof shell commands1381,55502
-@node Script input to the shellScript input to the shell1539,62157
-@node Settings for matching various output from proof processSettings for matching various output from proof process1606,65200
-@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process1737,70964
-@node Hooks and other settingsHooks and other settings1931,79717
-@node Goals buffer settingsGoals buffer settings2027,83550
-@node Splash screen settingsSplash screen settings2104,86658
-@node Global constantsGlobal constants2130,87416
-@node Handling multiple filesHandling multiple files2156,88265
-@node Configuring Font LockConfiguring Font Lock2308,96049
-@node Configuring X-SymbolConfiguring X-Symbol2351,97942
-@node Writing more lisp codeWriting more lisp code2411,100465
-@node Default values for generic settingsDefault values for generic settings2428,101110
-@node Adding prover-specific configurationsAdding prover-specific configurations2458,102193
-@node Useful variablesUseful variables2501,103463
-@node Useful functions and macrosUseful functions and macros2522,103968
-@node Internals of Proof GeneralInternals of Proof General2625,107795
-@node SpansSpans2653,108703
-@node Proof General site configurationProof General site configuration2666,109077
-@node Configuration variable mechanismsConfiguration variable mechanisms2746,112221
-@node Global variablesGlobal variables2864,117457
-@node Proof script modeProof script mode2934,120007
-@node Proof shell modeProof shell mode3193,131662
-@node DebuggingDebugging3607,147717
-@node Plans and ideasPlans and ideas3650,148612
-@node Proof by pointing and similar featuresProof by pointing and similar features3671,149334
-@node Granularity of atomic command sequencesGranularity of atomic command sequences3709,150992
-@node Browser mode for script files and theoriesBrowser mode for script files and theories3754,153217
-@node Demonstration InstantiationsDemonstration Instantiations3784,154248
-@node demoisa-easy.eldemoisa-easy.el3800,154679
-@node demoisa.eldemoisa.el3863,156917
-@node Function IndexFunction Index4031,162433
-@node Variable IndexVariable Index4035,162509
-@node Concept IndexConcept Index4044,162688
+@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
author	David Aspinall <da@inf.ed.ac.uk>	2004-05-07 11:16:59 +0000
committer	David Aspinall <da@inf.ed.ac.uk>	2004-05-07 11:16:59 +0000
commit	255f394c87bdcd47e0d0d7b07bd830c750d4c29d (patch)
tree	eda902bf65cf4a0a8dd07009e45ac511ba1b053b /TAGS
parent	334c7fd0210bbe065661ee8bf47fb38f5d85daf4 (diff)