Updated.

author: David Aspinall <da@inf.ed.ac.uk> 2005-05-17 20:12:37 +0000
committer: David Aspinall <da@inf.ed.ac.uk> 2005-05-17 20:12:37 +0000
commit: c8a0872fe1ea8cbd0169c96a5794dce5133851c4 (patch)
tree: 44f2b02e3bb0c620ef9e71271f2410fdceedc2b1 /TAGS
parent: c9058b248b0fbed4fd9db2c55e8741d645a320d0 (diff)
1 files changed, 1365 insertions, 1343 deletions
diff --git a/TAGS b/TAGS
index 4a0eebdf..a02042d7 100644
--- a/TAGS
+++ b/TAGS
@@ -3,105 +3,127 @@ acl2/acl2.el,0
 
 acl2/x-symbol-acl2.el,0
 
-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,5468
-(defcustom coq-prog-name coq-prog-name13,353
-(defcustom coq-compile-file-command coq-compile-file-command18,462
-(defcustom coq-default-undo-limit coq-default-undo-limit28,831
-(defconst coq-shell-init-cmd coq-shell-init-cmd33,959
-(defconst coq-shell-restart-cmd coq-shell-restart-cmd46,1382
-(defvar coq-shell-prompt-pattern coq-shell-prompt-pattern53,1640
-(defvar coq-shell-cd coq-shell-cd58,1848
-(defvar coq-shell-abort-goal-regexp coq-shell-abort-goal-regexp64,2049
-(defvar coq-shell-proof-completed-regexp coq-shell-proof-completed-regexp67,2175
-(defvar coq-goal-regexpcoq-goal-regexp70,2306
-(defun coq-library-directory coq-library-directory79,2495
-(defcustom coq-tags coq-tags86,2675
-(defconst coq-interrupt-regexp coq-interrupt-regexp91,2824
-(defcustom coq-www-home-page coq-www-home-page96,2944
-(defun coq-insert-section coq-insert-section112,3194
-(defconst module-kinds-table module-kinds-table121,3451
-(defconst modtype-kinds-tablemodtype-kinds-table125,3587
-(defun coq-insert-module coq-insert-module129,3716
-(defvar coq-outline-regexpcoq-outline-regexp150,4473
-(defvar coq-outline-heading-end-regexp coq-outline-heading-end-regexp155,4882
-(defvar coq-shell-outline-regexp coq-shell-outline-regexp157,4941
-(defvar coq-shell-outline-heading-end-regexp coq-shell-outline-heading-end-regexp158,4991
-(defconst coq-kill-goal-command coq-kill-goal-command160,5054
-(defconst coq-forget-id-command coq-forget-id-command161,5097
-(defconst coq-back-n-command coq-back-n-command162,5143
-(defconst coq-state-changing-tactics-regexp coq-state-changing-tactics-regexp166,5205
-(defconst coq-state-preserving-tactics-regexp coq-state-preserving-tactics-regexp168,5302
-(defconst coq-tactics-regexpcoq-tactics-regexp170,5403
-(defconst coq-state-changing-commands-regexpcoq-state-changing-commands-regexp172,5469
-(defconst coq-state-preserving-commands-regexp coq-state-preserving-commands-regexp174,5576
-(defvar coq-retractable-instruct-regexp coq-retractable-instruct-regexp176,5688
-(defvar coq-non-retractable-instruct-regexpcoq-non-retractable-instruct-regexp178,5779
-(defvar coq-keywords-sectioncoq-keywords-section181,5878
-(defvar coq-section-regexp coq-section-regexp186,6023
-(defun coq-set-undo-limit coq-set-undo-limit219,7090
-(defconst coq-keywords-decl-defn-regexpcoq-keywords-decl-defn-regexp230,7433
-(defun coq-proof-mode-p coq-proof-mode-p238,7821
-(defun coq-is-comment-or-proverprocp coq-is-comment-or-proverprocp253,8327
-(defun coq-is-goalsave-p coq-is-goalsave-p255,8431
-(defun coq-is-module-equal-p coq-is-module-equal-p256,8506
-(defun coq-is-def-p coq-is-def-p259,8702
-(defun coq-is-decl-defn-p coq-is-decl-defn-p261,8810
-(defun coq-state-preserving-command-p coq-state-preserving-command-p266,8977
-(defun coq-state-preserving-tactic-p coq-state-preserving-tactic-p269,9111
-(defun coq-state-changing-command-p coq-state-changing-command-p272,9243
-(defun coq-section-or-module-start-p coq-section-or-module-start-p278,9551
-(defun coq-find-and-forget coq-find-and-forget286,9804
-(defvar coq-current-goal coq-current-goal378,14371
-(defun coq-goal-hyp coq-goal-hyp381,14436
-(defun coq-state-preserving-p coq-state-preserving-p394,14866
-(defun coq-SearchIsos coq-SearchIsos401,15183
-(defun coq-guess-or-ask-for-string coq-guess-or-ask-for-string415,15617
-(defun coq-Print coq-Print425,15911
-(defun coq-Check coq-Check434,16169
-(defun coq-Show coq-Show443,16411
-(defun coq-PrintHint coq-PrintHint464,17097
-(defun coq-end-Section coq-end-Section470,17240
-(defun coq-Compile coq-Compile488,17824
-(defun coq-intros coq-intros495,18004
-(define-key coq-keymap coq-keymap512,18681
-(define-key coq-keymap coq-keymap513,18732
-(define-key coq-keymap coq-keymap514,18791
-(define-key coq-keymap coq-keymap515,18849
-(define-key coq-keymap coq-keymap516,18905
-(define-key coq-keymap coq-keymap517,18960
-(define-key coq-keymap coq-keymap518,19010
-(define-key coq-keymap coq-keymap519,19060
-(define-key global-map global-map528,19569
-(defun coq-guess-command-line coq-guess-command-line587,21563
-(defun coq-pre-shell-start coq-pre-shell-start609,22369
-(defun coq-mode-config coq-mode-config620,22890
-(defun coq-shell-mode-config coq-shell-mode-config727,26705
-(defun coq-goals-mode-config coq-goals-mode-config766,28340
-(defun coq-response-config coq-response-config773,28571
-(defun coq-maybe-compile-buffer coq-maybe-compile-buffer793,29287
-(defun coq-ancestors-of coq-ancestors-of830,30821
-(defun coq-all-ancestors-of coq-all-ancestors-of853,31788
-(defconst coq-require-command-regexp coq-require-command-regexp865,32181
-(defun coq-process-require-command coq-process-require-command870,32390
-(defun coq-included-children coq-included-children875,32517
-(defun coq-process-file coq-process-file896,33356
-(defpacustom print-only-first-subgoal print-only-first-subgoal910,33854
-(defpacustom print-fully-explicit print-fully-explicit915,34005
-(defpacustom print-coercions print-coercions920,34152
-(defpacustom print-match-wildcards print-match-wildcards925,34295
-(defpacustom time-commands time-commands931,34477
-(defpacustom auto-compile-vos auto-compile-vos935,34588
-(defpacustom translate-to-v8 translate-to-v8957,35543
-(defun coq-preprocessing coq-preprocessing966,35759
-(defun coq-fake-constant-markup coq-fake-constant-markup981,36178
-(defun coq-create-span-menu coq-create-span-menu1003,36985
+coq/coq-abbrev.el,152
+(defun holes-show-doc holes-show-doc4,90
+(defpgdefault menu-entriesmenu-entries151,7985
+(defpgdefault help-menu-entrieshelp-menu-entries349,19008
+
+coq/coq-autotest.el,0
+
+coq/coq.el,6716
+(defun proofstack proofstack23,436
+(defun proofstack proofstack24,508
+(defun proofstack proofstack25,580
+(defcustom coq-prog-name coq-prog-name28,670
+(defcustom coq-compile-file-command coq-compile-file-command33,779
+(defcustom coq-default-undo-limit coq-default-undo-limit43,1148
+(defconst coq-shell-init-cmd coq-shell-init-cmd48,1276
+(defconst coq-shell-restart-cmd coq-shell-restart-cmd58,1535
+(defvar coq-shell-prompt-pattern coq-shell-prompt-pattern66,1836
+(defvar coq-shell-cd coq-shell-cd73,2112
+(defvar coq-shell-abort-goal-regexp coq-shell-abort-goal-regexp77,2267
+(defvar coq-shell-proof-completed-regexp coq-shell-proof-completed-regexp80,2393
+(defvar coq-goal-regexpcoq-goal-regexp83,2524
+(defun coq-library-directory coq-library-directory92,2713
+(defcustom coq-tags coq-tags99,2893
+(defconst coq-interrupt-regexp coq-interrupt-regexp104,3043
+(defcustom coq-www-home-page coq-www-home-page109,3164
+(defun coq-insert-section coq-insert-section119,3351
+(defconst module-kinds-table module-kinds-table128,3591
+(defconst modtype-kinds-tablemodtype-kinds-table132,3727
+(defun coq-insert-module coq-insert-module136,3856
+(defvar coq-outline-regexpcoq-outline-regexp156,4534
+(defvar coq-outline-heading-end-regexp coq-outline-heading-end-regexp161,4943
+(defvar coq-shell-outline-regexp coq-shell-outline-regexp163,5002
+(defvar coq-shell-outline-heading-end-regexp coq-shell-outline-heading-end-regexp164,5052
+(defconst coq-kill-goal-command coq-kill-goal-command169,5162
+(defconst coq-forget-id-command coq-forget-id-command170,5205
+(defconst coq-back-n-command coq-back-n-command171,5251
+(defconst coq-state-preserving-tactics-regexp coq-state-preserving-tactics-regexp174,5295
+(defconst coq-state-changing-commands-regexpcoq-state-changing-commands-regexp176,5396
+(defconst coq-state-preserving-commands-regexp coq-state-preserving-commands-regexp178,5503
+(defconst coq-commands-regexp coq-commands-regexp180,5615
+(defvar coq-retractable-instruct-regexp coq-retractable-instruct-regexp182,5693
+(defvar coq-keywords-sectioncoq-keywords-section185,5785
+(defvar coq-section-regexp coq-section-regexp188,5878
+(defun coq-set-undo-limit coq-set-undo-limit222,6977
+(defconst coq-keywords-decl-defn-regexpcoq-keywords-decl-defn-regexp233,7415
+(defun coq-proof-mode-p coq-proof-mode-p237,7565
+(defun coq-is-comment-or-proverprocp coq-is-comment-or-proverprocp248,7975
+(defun coq-is-goalsave-p coq-is-goalsave-p250,8079
+(defun coq-is-module-equal-p coq-is-module-equal-p251,8154
+(defun coq-is-def-p coq-is-def-p254,8350
+(defun coq-is-decl-defn-p coq-is-decl-defn-p256,8458
+(defun coq-state-preserving-command-p coq-state-preserving-command-p261,8625
+(defun coq-command-p coq-command-p264,8759
+(defun coq-state-preserving-tactic-p coq-state-preserving-tactic-p267,8859
+(defun coq-state-changing-tactic-p coq-state-changing-tactic-p272,9007
+(defun coq-state-changing-command-p coq-state-changing-command-p279,9241
+(defun coq-section-or-module-start-p coq-section-or-module-start-p285,9549
+(defun build-list-id-from-string build-list-id-from-string294,9790
+(defun coq-last-prompt-info coq-last-prompt-info307,10320
+(defun coq-last-prompt-info-safe coq-last-prompt-info-safe324,10937
+(defvar coq-last-but-one-statenum coq-last-but-one-statenum334,11452
+(defvar coq-last-but-one-proofnum coq-last-but-one-proofnum336,11519
+(defvar coq-last-but-one-proofstack coq-last-but-one-proofstack338,11582
+(defun coq-get-span-statenum coq-get-span-statenum340,11624
+(defun coq-get-span-proofnum coq-get-span-proofnum345,11739
+(defun coq-get-span-proofstack coq-get-span-proofstack350,11854
+(defun coq-set-span-statenum coq-set-span-statenum355,11998
+(defun coq-set-span-proofnum coq-set-span-proofnum360,12129
+(defun coq-set-span-proofstack coq-set-span-proofstack365,12260
+(defun proof-last-locked-span proof-last-locked-span370,12420
+(defun coq-set-state-infos coq-set-state-infos385,13024
+(defun count-not-intersection count-not-intersection416,14627
+(defun  coq-find-and-forget-v81 coq-find-and-forget-v81447,15881
+(defun coq-find-and-forget-v80 coq-find-and-forget-v80471,16748
+(defun coq-find-and-forget coq-find-and-forget566,21443
+(defvar coq-current-goal coq-current-goal578,21897
+(defun coq-goal-hyp coq-goal-hyp581,21962
+(defun coq-state-preserving-p coq-state-preserving-p595,22425
+(defun coq-SearchIsos coq-SearchIsos602,22742
+(defun coq-guess-or-ask-for-string coq-guess-or-ask-for-string612,23094
+(defun coq-ask-do coq-ask-do622,23415
+(defun coq-Print coq-Print631,23676
+(defun coq-About coq-About635,23800
+(defun coq-Print-implicit coq-Print-implicit639,23919
+(defun coq-Check coq-Check644,24072
+(defun coq-Show coq-Show649,24182
+(defun coq-PrintHint coq-PrintHint664,24619
+(defun coq-end-Section coq-end-Section670,24763
+(defun coq-Compile coq-Compile688,25347
+(defun coq-intros coq-intros695,25528
+(define-key coq-keymap coq-keymap712,26205
+(define-key coq-keymap coq-keymap713,26256
+(define-key coq-keymap coq-keymap714,26315
+(define-key coq-keymap coq-keymap715,26373
+(define-key coq-keymap coq-keymap716,26429
+(define-key coq-keymap coq-keymap717,26484
+(define-key coq-keymap coq-keymap718,26534
+(define-key coq-keymap coq-keymap719,26584
+(define-key coq-keymap coq-keymap720,26634
+(defun coq-guess-command-line coq-guess-command-line739,27486
+(defun coq-pre-shell-start coq-pre-shell-start761,28293
+(defun coq-mode-config coq-mode-config773,28817
+(defun coq-shell-mode-config coq-shell-mode-config873,32330
+(defun coq-goals-mode-config coq-goals-mode-config912,33981
+(defun coq-response-config coq-response-config920,34229
+(defun coq-maybe-compile-buffer coq-maybe-compile-buffer941,34956
+(defun coq-ancestors-of coq-ancestors-of978,36490
+(defun coq-all-ancestors-of coq-all-ancestors-of1001,37457
+(defconst coq-require-command-regexp coq-require-command-regexp1013,37850
+(defun coq-process-require-command coq-process-require-command1018,38059
+(defun coq-included-children coq-included-children1023,38186
+(defun coq-process-file coq-process-file1044,39025
+(defpacustom print-fully-explicit print-fully-explicit1066,39823
+(defpacustom print-coercions print-coercions1071,39972
+(defpacustom print-match-wildcards print-match-wildcards1076,40117
+(defpacustom time-commands time-commands1082,40301
+(defpacustom auto-compile-vos auto-compile-vos1086,40412
+(defpacustom translate-to-v8 translate-to-v81108,41367
+(defun coq-preprocessing coq-preprocessing1117,41583
+(defun coq-fake-constant-markup coq-fake-constant-markup1132,42002
+(defun coq-create-span-menu coq-create-span-menu1154,42809
 
 coq/coq-indent.el,1791
 (defconst coq-any-command-regexpcoq-any-command-regexp11,262
@@ -116,76 +138,72 @@ coq/coq-indent.el,1791
 (defconst coq-indent-kw coq-indent-kw70,1914
 (defconst coq-indent-pattern-regexp coq-indent-pattern-regexp81,2331
 (defun coq-find-command-start coq-find-command-start86,2418
-(defun coq-find-real-start coq-find-real-start95,2691
-(defun coq-find-end coq-find-end107,3085
-(defun coq-current-command-string coq-current-command-string117,3356
-(defun is-at-a-space-or-tab is-at-a-space-or-tab125,3555
-(defun only-spaces-on-line only-spaces-on-line131,3759
-(defun find-reg find-reg138,4007
-(defun coq-back-to-indentation-prevline coq-back-to-indentation-prevline152,4382
-(defun coq-find-unclosed coq-find-unclosed181,5618
-(defun coq-find-at-same-level-zero coq-find-at-same-level-zero208,6799
-(defun coq-find-unopened coq-find-unopened236,7883
-(defun coq-find-last-unopened coq-find-last-unopened282,9236
-(defun coq-end-offset coq-end-offset295,9640
-(defun coq-indent-command-offset coq-indent-command-offset323,10459
-(defun coq-indent-expr-offset coq-indent-expr-offset368,12219
-(defun coq-indent-offset coq-indent-offset480,16422
-(defun coq-indent-calculate coq-indent-calculate500,17085
-(defun proof-indent-line proof-indent-line514,17532
-
-coq/coq-syntax.el,3214
-(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,4542
-(defvar coq-keywords-defncoq-keywords-defn139,4898
-(defun coq-count-match coq-count-match213,7254
-(defun coq-goal-command-p coq-goal-command-p225,7674
-(defvar coq-keywords-save-strictcoq-keywords-save-strict245,8258
-(defvar coq-keywords-savecoq-keywords-save253,8355
-(defun coq-save-command-p coq-save-command-p257,8431
-(defvar coq-keywords-kill-goal coq-keywords-kill-goal265,8710
-(defcustom coq-user-state-changing-commands coq-user-state-changing-commands271,8760
-(defcustom coq-user-state-preserving-commands coq-user-state-preserving-commands283,9157
-(defvar coq-keywords-state-preserving-commandscoq-keywords-state-preserving-commands296,9597
-(defvar coq-keywords-state-changing-misc-commandscoq-keywords-state-changing-misc-commands344,10722
-(defvar coq-keywords-state-changing-commandscoq-keywords-state-changing-commands418,12740
-(defvar coq-keywords-commandscoq-keywords-commands428,12937
-(defcustom coq-user-state-changing-tactics coq-user-state-changing-tactics434,13087
-(defvar coq-state-changing-tacticscoq-state-changing-tactics445,13513
-(defcustom coq-user-state-preserving-tactics coq-user-state-preserving-tactics646,16838
-(defvar coq-state-preserving-tacticscoq-state-preserving-tactics657,17252
-(defvar coq-tacticscoq-tactics661,17350
-(defvar coq-retractable-instructcoq-retractable-instruct664,17439
-(defvar coq-non-retractable-instructcoq-non-retractable-instruct667,17549
-(defvar coq-keywordscoq-keywords671,17671
-(defvar coq-tacticalscoq-tacticals676,17836
-(defvar coq-reserved-commoncoq-reserved-common698,18219
-(defvar coq-reserved-V8coq-reserved-V8714,18412
-(defvar coq-reserved-V7coq-reserved-V7725,18516
-(defvar coq-reserved coq-reserved730,18591
-(defvar coq-symbolscoq-symbols738,18747
-(defvar coq-error-regexp coq-error-regexp756,18951
-(defvar coq-id coq-id759,19180
-(defvar coq-ids coq-ids761,19206
-(defun coq-first-abstr-regexp coq-first-abstr-regexp763,19243
-(defun coq-next-abstr-regexp coq-next-abstr-regexp766,19331
-(defvar coq-font-lock-termscoq-font-lock-terms769,19409
-(defconst coq-save-command-regexp-strictcoq-save-command-regexp-strict784,20062
-(defconst coq-save-command-regexpcoq-save-command-regexp786,20175
-(defconst coq-save-with-hole-regexpcoq-save-with-hole-regexp788,20274
-(defconst coq-goal-command-regexpcoq-goal-command-regexp791,20412
-(defconst coq-goal-with-hole-regexpcoq-goal-with-hole-regexp793,20511
-(defconst coq-decl-with-hole-regexpcoq-decl-with-hole-regexp799,20800
-(defconst coq-defn-with-hole-regexpcoq-defn-with-hole-regexp802,20933
-(defvar coq-font-lock-keywords-1coq-font-lock-keywords-1805,21073
-(defvar coq-font-lock-keywords coq-font-lock-keywords826,22116
-(defun coq-init-syntax-table coq-init-syntax-table828,22174
-(defconst coq-generic-expressioncoq-generic-expression857,23072
+(defun coq-find-real-start coq-find-real-start95,2694
+(defun coq-find-end coq-find-end107,3088
+(defun coq-current-command-string coq-current-command-string118,3486
+(defun is-at-a-space-or-tab is-at-a-space-or-tab126,3685
+(defun only-spaces-on-line only-spaces-on-line132,3889
+(defun find-reg find-reg139,4137
+(defun coq-back-to-indentation-prevline coq-back-to-indentation-prevline154,4534
+(defun coq-find-unclosed coq-find-unclosed183,5787
+(defun coq-find-at-same-level-zero coq-find-at-same-level-zero210,6968
+(defun coq-find-unopened coq-find-unopened238,8052
+(defun coq-find-last-unopened coq-find-last-unopened284,9405
+(defun coq-end-offset coq-end-offset297,9809
+(defun coq-indent-command-offset coq-indent-command-offset325,10628
+(defun coq-indent-expr-offset coq-indent-expr-offset370,12387
+(defun coq-indent-offset coq-indent-offset482,16590
+(defun coq-indent-calculate coq-indent-calculate502,17253
+(defun proof-indent-line proof-indent-line516,17700
+
+coq/coq-syntax.el,2992
+(defvar coq-version-is-V8 coq-version-is-V819,648
+(defvar coq-version-is-V8-0 coq-version-is-V8-021,727
+(defvar coq-version-is-V8-1 coq-version-is-V8-128,1099
+(defvar coq-keywords-declcoq-keywords-decl75,2947
+(defvar coq-keywords-defncoq-keywords-defn90,3303
+(defvar coq-keywords-goalcoq-keywords-goal109,3728
+(defun coq-count-match coq-count-match152,5363
+(defun coq-goal-command-p coq-goal-command-p164,5783
+(defvar coq-keywords-save-strictcoq-keywords-save-strict182,6365
+(defvar coq-keywords-savecoq-keywords-save190,6462
+(defun coq-save-command-p coq-save-command-p194,6538
+(defvar coq-keywords-kill-goal coq-keywords-kill-goal202,6817
+(defcustom coq-user-state-changing-commands coq-user-state-changing-commands208,6867
+(defcustom coq-user-state-preserving-commands coq-user-state-preserving-commands220,7264
+(defvar coq-keywords-state-preserving-commandscoq-keywords-state-preserving-commands233,7704
+(defvar coq-keywords-state-changing-misc-commandscoq-keywords-state-changing-misc-commands281,8831
+(defvar coq-keywords-state-changing-commandscoq-keywords-state-changing-commands354,10812
+(defvar coq-keywords-commandscoq-keywords-commands364,11009
+(defvar coq-tacticalscoq-tacticals369,11158
+(defvar coq-reservedcoq-reserved381,11359
+(defcustom coq-user-state-changing-tactics coq-user-state-changing-tactics406,11618
+(defvar coq-state-changing-tacticscoq-state-changing-tactics417,12044
+(defcustom coq-user-state-preserving-tactics coq-user-state-preserving-tactics525,13628
+(defvar coq-state-preserving-tacticscoq-state-preserving-tactics536,14042
+(defvar coq-tacticscoq-tactics540,14140
+(defvar coq-retractable-instructcoq-retractable-instruct543,14229
+(defvar coq-non-retractable-instructcoq-non-retractable-instruct546,14339
+(defvar coq-keywordscoq-keywords550,14461
+(defvar coq-symbolscoq-symbols557,14628
+(defvar coq-error-regexp coq-error-regexp575,14832
+(defvar coq-id coq-id578,15061
+(defvar coq-id-shy coq-id-shy579,15086
+(defvar coq-ids coq-ids581,15140
+(defun coq-first-abstr-regexp coq-first-abstr-regexp583,15177
+(defun coq-next-abstr-regexp coq-next-abstr-regexp586,15265
+(defvar coq-font-lock-termscoq-font-lock-terms589,15343
+(defconst coq-save-command-regexp-strictcoq-save-command-regexp-strict604,15996
+(defconst coq-save-command-regexpcoq-save-command-regexp606,16109
+(defconst coq-save-with-hole-regexpcoq-save-with-hole-regexp608,16208
+(defconst coq-goal-command-regexpcoq-goal-command-regexp611,16346
+(defconst coq-goal-with-hole-regexpcoq-goal-with-hole-regexp613,16445
+(defconst coq-decl-with-hole-regexpcoq-decl-with-hole-regexp619,16734
+(defconst coq-defn-with-hole-regexpcoq-defn-with-hole-regexp622,16867
+(defvar coq-font-lock-keywords-1coq-font-lock-keywords-1625,17007
+(defvar coq-font-lock-keywords coq-font-lock-keywords646,18050
+(defun coq-init-syntax-table coq-init-syntax-table648,18108
+(defconst coq-generic-expressioncoq-generic-expression677,19006
 
 coq/x-symbol-coq.el,2822
 (defvar x-symbol-coq-required-fonts x-symbol-coq-required-fonts16,384
@@ -246,121 +264,182 @@ generic/pg-assoc.el,408
 (defun pg-assoc-strip-subterm-markup-buf pg-assoc-strip-subterm-markup-buf72,2220
 (defun pg-assoc-strip-subterm-markup-buf-old pg-assoc-strip-subterm-markup-buf-old94,2969
 
-generic/pg-goals.el,1074
-(define-derived-mode proof-goals-mode proof-goals-mode28,650
-(define-key proof-goals-mode-map proof-goals-mode-map48,1340
-(define-key proof-goals-mode-map proof-goals-mode-map51,1423
-(define-key proof-goals-mode-map proof-goals-mode-map52,1493
-(define-key proof-goals-mode-map proof-goals-mode-map57,1909
-(define-key proof-goals-mode-map proof-goals-mode-map59,1982
-(define-key proof-goals-mode-map proof-goals-mode-map60,2050
-(define-key proof-goals-mode-map proof-goals-mode-map63,2310
-(defun proof-goals-config-done proof-goals-config-done78,2574
-(defun pg-goals-display pg-goals-display88,2862
-(defun pg-goals-analyse-structure pg-goals-analyse-structure137,4805
-(defun pg-goals-make-top-span pg-goals-make-top-span261,9651
-(defun pg-goals-yank-subterm pg-goals-yank-subterm291,10658
-(defun pg-goals-button-action pg-goals-button-action318,11558
-(defun proof-expand-path proof-expand-path339,12531
-(defun pg-goals-construct-command pg-goals-construct-command348,12775
-(defun pg-goals-get-subterm-help pg-goals-get-subterm-help372,13627
+generic/pg-autotest.el,705
+(defvar pg-autotest-success pg-autotest-success20,514
+(defun pg-autotest-find-file pg-autotest-find-file24,598
+(defun pg-autotest-find-file-restart pg-autotest-find-file-restart31,869
+(defmacro pg-autotest pg-autotest44,1317
+(defun pg-autotest-script-wholefile pg-autotest-script-wholefile58,1665
+(defun pg-autotest-retract-file pg-autotest-retract-file75,2278
+(defun pg-autotest-assert-processed pg-autotest-assert-processed81,2414
+(defun pg-autotest-assert-unprocessed pg-autotest-assert-unprocessed88,2660
+(defun pg-autotest-message pg-autotest-message95,2907
+(defun pg-autotest-quit-prover pg-autotest-quit-prover102,3100
+(defun pg-autotest-finished pg-autotest-finished108,3282
+
+generic/pg-goals.el,1075
+(define-derived-mode proof-goals-mode proof-goals-mode28,651
+(define-key proof-goals-mode-map proof-goals-mode-map48,1341
+(define-key proof-goals-mode-map proof-goals-mode-map51,1424
+(define-key proof-goals-mode-map proof-goals-mode-map52,1494
+(define-key proof-goals-mode-map proof-goals-mode-map60,2084
+(define-key proof-goals-mode-map proof-goals-mode-map62,2157
+(define-key proof-goals-mode-map proof-goals-mode-map63,2225
+(define-key proof-goals-mode-map proof-goals-mode-map69,2659
+(defun proof-goals-config-done proof-goals-config-done84,2923
+(defun pg-goals-display pg-goals-display94,3211
+(defun pg-goals-analyse-structure pg-goals-analyse-structure143,5154
+(defun pg-goals-make-top-span pg-goals-make-top-span267,10000
+(defun pg-goals-yank-subterm pg-goals-yank-subterm297,11007
+(defun pg-goals-button-action pg-goals-button-action324,11907
+(defun proof-expand-path proof-expand-path345,12880
+(defun pg-goals-construct-command pg-goals-construct-command354,13124
+(defun pg-goals-get-subterm-help pg-goals-get-subterm-help378,13976
 
 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-pgip.el,4870
-(defalias 'pg-pgip-debug pg-pgip-debug22,725
-(defalias 'pg-pgip-error pg-pgip-error23,766
-(defalias 'pg-pgip-warning pg-pgip-warning24,801
-(defun pg-pgip-process-packet pg-pgip-process-packet27,866
-(defvar pg-pgip-last-seen-id pg-pgip-last-seen-id37,1439
-(defvar pg-pgip-last-seen-seq pg-pgip-last-seen-seq38,1473
-(defun pg-pgip-process-pgip pg-pgip-process-pgip40,1509
-(defun pg-pgip-process-msg pg-pgip-process-msg56,2224
-(defvar pg-pgip-post-process-functionspg-pgip-post-process-functions69,2770
-(defun pg-pgip-post-process pg-pgip-post-process78,3164
-(defun pg-pgip-process-usespgip pg-pgip-process-usespgip94,3775
-(defun pg-pgip-process-usespgml pg-pgip-process-usespgml98,3939
-(defun pg-pgip-process-pgmlconfig pg-pgip-process-pgmlconfig102,4103
-(defun pg-pgip-process-proverinfo pg-pgip-process-proverinfo118,4711
-(defun pg-pgip-process-hasprefs pg-pgip-process-hasprefs135,5365
-(defun pg-pgip-haspref pg-pgip-haspref149,5997
-(defun pg-pgip-process-prefval pg-pgip-process-prefval168,6776
-(defun pg-pgip-process-guiconfig pg-pgip-process-guiconfig195,7485
-(defun pg-pgip-process-ids pg-pgip-process-ids202,7602
-(defalias 'pg-pgip-process-setids pg-pgip-process-setids224,8508
-(defalias 'pg-pgip-process-addids pg-pgip-process-addids225,8564
-(defalias 'pg-pgip-process-delids pg-pgip-process-delids226,8620
-(defun pg-pgip-process-idvalue pg-pgip-process-idvalue229,8678
-(defun pg-pgip-process-menuadd pg-pgip-process-menuadd241,9015
-(defun pg-pgip-process-menudel pg-pgip-process-menudel244,9058
-(defun pg-pgip-process-ready pg-pgip-process-ready253,9291
-(defun pg-pgip-process-cleardisplay pg-pgip-process-cleardisplay256,9332
-(defun pg-pgip-process-proofstate pg-pgip-process-proofstate270,9809
-(defun pg-pgip-process-normalresponse pg-pgip-process-normalresponse274,9886
-(defun pg-pgip-process-errorresponse pg-pgip-process-errorresponse278,10010
-(defun pg-pgip-process-scriptinsert pg-pgip-process-scriptinsert282,10133
-(defun pg-pgip-process-metainforesponse pg-pgip-process-metainforesponse287,10267
-(defun pg-pgip-process-parseresult pg-pgip-process-parseresult290,10319
-(defun pg-pgip-process-informfileloaded pg-pgip-process-informfileloaded299,10555
-(defun pg-pgip-process-informfileretracted pg-pgip-process-informfileretracted305,10821
-(defun pg-pgip-process-brokerstatus pg-pgip-process-brokerstatus318,11295
-(defun pg-pgip-process-proveravailmsg pg-pgip-process-proveravailmsg321,11343
-(defun pg-pgip-process-newprovermsg pg-pgip-process-newprovermsg324,11393
-(defun pg-pgip-process-proverstatusmsg pg-pgip-process-proverstatusmsg327,11441
-(defvar pg-pgip-srcids pg-pgip-srcids336,11688
-(defun pg-pgip-process-newfile pg-pgip-process-newfile340,11795
-(defun pg-pgip-process-filestatus pg-pgip-process-filestatus356,12383
-(defun pg-pgip-process-newobj pg-pgip-process-newobj376,13038
-(defun pg-pgip-process-delobj pg-pgip-process-delobj379,13080
-(defun pg-pgip-process-objectstatus pg-pgip-process-objectstatus382,13122
-(defun pg-pgip-process-parsescript pg-pgip-process-parsescript396,13478
-(defun pg-pgip-get-pgiptype pg-pgip-get-pgiptype419,14354
-(defun pg-pgip-default-for pg-pgip-default-for439,15149
-(defun pg-pgip-subst-for pg-pgip-subst-for452,15544
-(defun pg-pgip-interpret-value pg-pgip-interpret-value464,15887
-(defun pg-pgip-interpret-choice pg-pgip-interpret-choice482,16570
-(defun pg-pgip-get-icon pg-pgip-get-icon513,17643
-(defsubst pg-pgip-get-name pg-pgip-get-name517,17791
-(defsubst pg-pgip-get-version pg-pgip-get-version520,17908
-(defsubst pg-pgip-get-descr pg-pgip-get-descr523,18031
-(defsubst pg-pgip-get-thmname pg-pgip-get-thmname526,18150
-(defsubst pg-pgip-get-thyname pg-pgip-get-thyname529,18273
-(defsubst pg-pgip-get-url pg-pgip-get-url532,18396
-(defsubst pg-pgip-get-srcid pg-pgip-get-srcid535,18511
-(defsubst pg-pgip-get-proverid pg-pgip-get-proverid538,18630
-(defsubst pg-pgip-get-symname pg-pgip-get-symname541,18755
-(defsubst pg-pgip-get-prefcat pg-pgip-get-prefcat544,18875
-(defsubst pg-pgip-get-default pg-pgip-get-default547,19003
-(defsubst pg-pgip-get-objtype pg-pgip-get-objtype550,19126
-(defsubst pg-pgip-get-value pg-pgip-get-value553,19249
-(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext556,19311
-(defun pg-pgip-get-pgmltext pg-pgip-get-pgmltext558,19370
-(defun pg-pgip-string-of-command pg-pgip-string-of-command567,19597
-(defconst pg-pgip-idpg-pgip-id584,20358
-(defvar pg-pgip-refseq pg-pgip-refseq590,20638
-(defvar pg-pgip-refid pg-pgip-refid592,20736
-(defvar pg-pgip-seq pg-pgip-seq595,20830
-(defun pg-pgip-assemble-packet pg-pgip-assemble-packet597,20894
-(defun pg-pgip-issue pg-pgip-issue615,21709
-(defun pg-pgip-askprefs pg-pgip-askprefs632,22322
-(defun pg-pgip-askids pg-pgip-askids636,22436
-(defun pg-pgip-reset pg-pgip-reset649,22727
+generic/pg-pbrpm.el,2734
+(defvar pg-pbrpm-use-buffer-menu pg-pbrpm-use-buffer-menu11,259
+(defvar pg-pbrpm-buffer-menu pg-pbrpm-buffer-menu13,378
+(defvar pg-pbrpm-spans pg-pbrpm-spans14,412
+(defvar pg-pbrpm-goal-description pg-pbrpm-goal-description15,440
+(defun pg-pbrpm-erase-buffer-menu pg-pbrpm-erase-buffer-menu17,480
+(defun pg-pbrpm-menu-change-hook pg-pbrpm-menu-change-hook24,685
+(defun pg-pbrpm-create-reset-buffer-menu pg-pbrpm-create-reset-buffer-menu42,1262
+(defun pg-pbrpm-analyse-goal-buffer pg-pbrpm-analyse-goal-buffer57,1914
+(defun pg-pbrpm-button-action pg-pbrpm-button-action118,4334
+(defun pg-pbrpm-exists pg-pbrpm-exists125,4560
+(defun pg-pbrpm-eliminate-id pg-pbrpm-eliminate-id129,4672
+(defun pg-pbrpm-build-menu pg-pbrpm-build-menu137,4920
+(defun pg-pbrpm-setup-span pg-pbrpm-setup-span193,7110
+(defun pg-pbrpm-run-command pg-pbrpm-run-command253,9477
+(defun pg-pbrpm-get-pos-info pg-pbrpm-get-pos-info281,10753
+(defun pg-pbrpm-get-region-info pg-pbrpm-get-region-info317,11895
+(defun auto-select-arround-pos auto-select-arround-pos327,12220
+(defun pg-pbrpm-translate-position pg-pbrpm-translate-position339,12664
+(defun pg-pbrpm-process-click pg-pbrpm-process-click345,12888
+(defvar pg-pbrpm-remember-region-selected-region pg-pbrpm-remember-region-selected-region365,13892
+(defvar pg-pbrpm-regions-list pg-pbrpm-regions-list366,13946
+(defun pg-pbrpm-erase-regions-list pg-pbrpm-erase-regions-list368,13982
+(defun pg-pbrpm-filter-regions-list pg-pbrpm-filter-regions-list377,14291
+(defface pg-pbrpm-multiple-selection-facepg-pbrpm-multiple-selection-face384,14554
+(defface pg-pbrpm-menu-input-facepg-pbrpm-menu-input-face392,14759
+(defun pg-pbrpm-do-remember-region pg-pbrpm-do-remember-region400,14952
+(defun pg-pbrpm-remember-region-drag-up-hook pg-pbrpm-remember-region-drag-up-hook421,15793
+(defun pg-pbrpm-remember-region-click-hook pg-pbrpm-remember-region-click-hook425,15964
+(defun pg-pbrpm-remember-region pg-pbrpm-remember-region430,16149
+(defun pg-pbrpm-process-region pg-pbrpm-process-region444,16864
+(defun pg-pbrpm-process-regions-list pg-pbrpm-process-regions-list461,17587
+(defun pg-pbrpm-region-expression pg-pbrpm-region-expression465,17770
+(define-key proof-goals-mode-map proof-goals-mode-map489,18706
+(define-key proof-goals-mode-map proof-goals-mode-map490,18776
+(define-key proof-goals-mode-map proof-goals-mode-map491,18853
+(define-key pg-span-context-menu-keymap pg-span-context-menu-keymap492,18933
+(define-key pg-span-context-menu-keymap pg-span-context-menu-keymap493,19010
+(define-key proof-mode-map proof-mode-map494,19093
+(define-key proof-mode-map proof-mode-map495,19157
+(define-key proof-mode-map proof-mode-map496,19228
+
+generic/pg-pgip.el,5296
+(defalias 'pg-pgip-debug pg-pgip-debug29,894
+(defalias 'pg-pgip-error pg-pgip-error30,935
+(defalias 'pg-pgip-warning pg-pgip-warning31,970
+(defconst pg-pgip-version-supported pg-pgip-version-supported33,1020
+(defun pg-pgip-process-packet pg-pgip-process-packet37,1126
+(defvar pg-pgip-last-seen-id pg-pgip-last-seen-id47,1699
+(defvar pg-pgip-last-seen-seq pg-pgip-last-seen-seq48,1733
+(defun pg-pgip-process-pgip pg-pgip-process-pgip50,1769
+(defun pg-pgip-process-msg pg-pgip-process-msg69,2696
+(defvar pg-pgip-post-process-functionspg-pgip-post-process-functions83,3266
+(defun pg-pgip-post-process pg-pgip-post-process93,3750
+(defun pg-pgip-process-askpgip pg-pgip-process-askpgip109,4361
+(defun pg-pgip-process-usespgip pg-pgip-process-usespgip114,4520
+(defun pg-pgip-process-usespgml pg-pgip-process-usespgml118,4684
+(defun pg-pgip-process-pgmlconfig pg-pgip-process-pgmlconfig122,4848
+(defun pg-pgip-process-proverinfo pg-pgip-process-proverinfo138,5456
+(defun pg-pgip-process-hasprefs pg-pgip-process-hasprefs155,6121
+(defun pg-pgip-haspref pg-pgip-haspref169,6753
+(defun pg-pgip-process-prefval pg-pgip-process-prefval188,7532
+(defun pg-pgip-process-guiconfig pg-pgip-process-guiconfig215,8241
+(defvar proof-assistant-idtables proof-assistant-idtables222,8358
+(defun pg-pgip-process-ids pg-pgip-process-ids225,8475
+(defun pg-complete-idtable-symbol pg-complete-idtable-symbol251,9554
+(defalias 'pg-pgip-process-setids pg-pgip-process-setids256,9646
+(defalias 'pg-pgip-process-addids pg-pgip-process-addids257,9702
+(defalias 'pg-pgip-process-delids pg-pgip-process-delids258,9758
+(defun pg-pgip-process-idvalue pg-pgip-process-idvalue261,9816
+(defun pg-pgip-process-menuadd pg-pgip-process-menuadd273,10153
+(defun pg-pgip-process-menudel pg-pgip-process-menudel276,10196
+(defun pg-pgip-process-ready pg-pgip-process-ready285,10429
+(defun pg-pgip-process-cleardisplay pg-pgip-process-cleardisplay288,10470
+(defun pg-pgip-process-proofstate pg-pgip-process-proofstate302,10947
+(defun pg-pgip-process-normalresponse pg-pgip-process-normalresponse306,11024
+(defun pg-pgip-process-errorresponse pg-pgip-process-errorresponse310,11148
+(defun pg-pgip-process-scriptinsert pg-pgip-process-scriptinsert314,11271
+(defun pg-pgip-process-metainforesponse pg-pgip-process-metainforesponse319,11405
+(defun pg-pgip-process-informfileloaded pg-pgip-process-informfileloaded328,11646
+(defun pg-pgip-process-informfileretracted pg-pgip-process-informfileretracted334,11912
+(defun pg-pgip-process-brokerstatus pg-pgip-process-brokerstatus347,12386
+(defun pg-pgip-process-proveravailmsg pg-pgip-process-proveravailmsg350,12434
+(defun pg-pgip-process-newprovermsg pg-pgip-process-newprovermsg353,12484
+(defun pg-pgip-process-proverstatusmsg pg-pgip-process-proverstatusmsg356,12532
+(defvar pg-pgip-srcids pg-pgip-srcids365,12779
+(defun pg-pgip-process-newfile pg-pgip-process-newfile369,12886
+(defun pg-pgip-process-filestatus pg-pgip-process-filestatus385,13474
+(defun pg-pgip-process-newobj pg-pgip-process-newobj405,14129
+(defun pg-pgip-process-delobj pg-pgip-process-delobj408,14171
+(defun pg-pgip-process-objectstatus pg-pgip-process-objectstatus411,14213
+(defun pg-pgip-process-parsescript pg-pgip-process-parsescript425,14569
+(defun pg-pgip-get-pgiptype pg-pgip-get-pgiptype448,15444
+(defun pg-pgip-default-for pg-pgip-default-for468,16239
+(defun pg-pgip-subst-for pg-pgip-subst-for481,16634
+(defun pg-pgip-interpret-value pg-pgip-interpret-value493,16977
+(defun pg-pgip-interpret-choice pg-pgip-interpret-choice511,17660
+(defun pg-pgip-get-icon pg-pgip-get-icon542,18733
+(defsubst pg-pgip-get-name pg-pgip-get-name546,18881
+(defsubst pg-pgip-get-version pg-pgip-get-version549,18998
+(defsubst pg-pgip-get-descr pg-pgip-get-descr552,19121
+(defsubst pg-pgip-get-thmname pg-pgip-get-thmname555,19240
+(defsubst pg-pgip-get-thyname pg-pgip-get-thyname558,19363
+(defsubst pg-pgip-get-url pg-pgip-get-url561,19486
+(defsubst pg-pgip-get-srcid pg-pgip-get-srcid564,19601
+(defsubst pg-pgip-get-proverid pg-pgip-get-proverid567,19720
+(defsubst pg-pgip-get-symname pg-pgip-get-symname570,19845
+(defsubst pg-pgip-get-prefcat pg-pgip-get-prefcat573,19965
+(defsubst pg-pgip-get-default pg-pgip-get-default576,20093
+(defsubst pg-pgip-get-objtype pg-pgip-get-objtype579,20216
+(defsubst pg-pgip-get-value pg-pgip-get-value582,20339
+(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext585,20409
+(defun pg-pgip-get-pgmltext pg-pgip-get-pgmltext587,20468
+(defun pg-pgip-string-of-command pg-pgip-string-of-command596,20703
+(defconst pg-pgip-idpg-pgip-id613,21464
+(defvar pg-pgip-refseq pg-pgip-refseq619,21744
+(defvar pg-pgip-refid pg-pgip-refid621,21842
+(defvar pg-pgip-seq pg-pgip-seq624,21936
+(defun pg-pgip-assemble-packet pg-pgip-assemble-packet626,22000
+(defun pg-pgip-issue pg-pgip-issue644,22815
+(defun pg-pgip-maybe-askpgip pg-pgip-maybe-askpgip661,23428
+(defun pg-pgip-askprefs pg-pgip-askprefs667,23619
+(defun pg-pgip-askids pg-pgip-askids671,23733
+(defun pg-pgip-reset pg-pgip-reset684,24024
+(defconst pg-pgip-start-element-regexp pg-pgip-start-element-regexp715,24722
+(defconst pg-pgip-end-element-regexp pg-pgip-end-element-regexp716,24774
 
 generic/pg-pgip-old.el,734
 (defun pg-pgip-process-oldhaspref pg-pgip-process-oldhaspref18,633
 (defun pg-pgip-process-haspref pg-pgip-process-haspref21,730
-(defun pg-pgip-old-interpret-bool pg-pgip-old-interpret-bool58,2245
-(defun pg-pgip-old-interpret-int pg-pgip-old-interpret-int67,2529
-(defun pg-pgip-old-interpret-string pg-pgip-old-interpret-string72,2696
-(defun pg-pgip-old-interpret-choice pg-pgip-old-interpret-choice75,2750
-(defun pg-pgip-old-interpret-value pg-pgip-old-interpret-value95,3469
-(defun pg-pgip-old-default-for pg-pgip-old-default-for114,4015
-(defun pg-pgip-old-subst-for pg-pgip-old-subst-for125,4339
-(defun pg-pgip-old-get-type pg-pgip-old-get-type132,4504
-(defun pg-pgip-old-pgiptype pg-pgip-old-pgiptype139,4726
+(defun pg-pgip-old-interpret-bool pg-pgip-old-interpret-bool57,2158
+(defun pg-pgip-old-interpret-int pg-pgip-old-interpret-int66,2442
+(defun pg-pgip-old-interpret-string pg-pgip-old-interpret-string71,2609
+(defun pg-pgip-old-interpret-choice pg-pgip-old-interpret-choice74,2663
+(defun pg-pgip-old-interpret-value pg-pgip-old-interpret-value94,3382
+(defun pg-pgip-old-default-for pg-pgip-old-default-for113,3928
+(defun pg-pgip-old-subst-for pg-pgip-old-subst-for124,4252
+(defun pg-pgip-old-get-type pg-pgip-old-get-type131,4417
+(defun pg-pgip-old-pgiptype pg-pgip-old-pgiptype138,4633
 
 generic/pg-response.el,1890
 (define-derived-mode proof-response-mode proof-response-mode24,597
@@ -417,41 +496,41 @@ generic/pg-user.el,3655
 (defun proof-minibuffer-cmd proof-minibuffer-cmd265,8620
 (defun proof-frob-locked-end proof-frob-locked-end313,10426
 (defmacro proof-if-setting-configured proof-if-setting-configured406,13340
-(defmacro proof-define-assistant-command proof-define-assistant-command413,13595
-(defmacro proof-define-assistant-command-witharg proof-define-assistant-command-witharg425,14046
-(defun proof-issue-new-command proof-issue-new-command445,14852
-(defun proof-cd-sync proof-cd-sync490,16351
-(deflocal proof-electric-terminator proof-electric-terminator541,17820
-(defun proof-electric-terminator-enable proof-electric-terminator-enable551,18167
-(defun proof-electric-term-incomment-fn proof-electric-term-incomment-fn562,18654
-(defun proof-process-electric-terminator proof-process-electric-terminator582,19410
-(defun proof-electric-terminator proof-electric-terminator609,20561
-(defun proof-add-completions proof-add-completions631,21199
-(defun proof-script-complete proof-script-complete651,21956
-(defun pg-insert-last-output-as-comment pg-insert-last-output-as-comment679,22547
-(defun pg-copy-span-contents pg-copy-span-contents710,23775
-(defun pg-numth-span-higher-or-lower pg-numth-span-higher-or-lower727,24335
-(defun pg-control-span-of pg-control-span-of753,25086
-(defun pg-move-span-contents pg-move-span-contents759,25290
-(defun pg-fixup-children-span pg-fixup-children-span813,27514
-(defun pg-move-region-down pg-move-region-down820,27722
-(defun pg-move-region-up pg-move-region-up829,28016
-(defun proof-forward-command proof-forward-command859,28856
-(defun proof-backward-command proof-backward-command880,29578
-(defvar pg-span-context-menu-keymappg-span-context-menu-keymap896,29822
-(defun pg-span-for-event pg-span-for-event912,30249
-(defun pg-span-context-menu pg-span-context-menu923,30633
-(defun pg-toggle-visibility pg-toggle-visibility938,31093
-(defun pg-create-in-span-context-menu pg-create-in-span-context-menu948,31415
-(defun pg-goals-buffers-hint pg-goals-buffers-hint1020,33968
-(defun pg-slow-fontify-tracing-hint pg-slow-fontify-tracing-hint1023,34135
-(defun pg-response-buffers-hint pg-response-buffers-hint1026,34291
-(defun pg-jump-to-end-hint pg-jump-to-end-hint1035,34640
-(defun pg-processing-complete-hint pg-processing-complete-hint1038,34756
-(defun pg-next-error-hint pg-next-error-hint1054,35442
-(defun pg-hint pg-hint1058,35579
-(defun pg-identifier-under-mouse-query pg-identifier-under-mouse-query1077,36255
-(defun proof-imenu-enable proof-imenu-enable1122,37882
+(defmacro proof-define-assistant-command proof-define-assistant-command414,13610
+(defmacro proof-define-assistant-command-witharg proof-define-assistant-command-witharg427,14076
+(defun proof-issue-new-command proof-issue-new-command447,14901
+(defun proof-cd-sync proof-cd-sync492,16400
+(deflocal proof-electric-terminator proof-electric-terminator543,17869
+(defun proof-electric-terminator-enable proof-electric-terminator-enable553,18216
+(defun proof-electric-term-incomment-fn proof-electric-term-incomment-fn564,18703
+(defun proof-process-electric-terminator proof-process-electric-terminator584,19459
+(defun proof-electric-terminator proof-electric-terminator611,20610
+(defun proof-add-completions proof-add-completions633,21248
+(defun proof-script-complete proof-script-complete653,22005
+(defun pg-insert-last-output-as-comment pg-insert-last-output-as-comment681,22596
+(defun pg-copy-span-contents pg-copy-span-contents712,23824
+(defun pg-numth-span-higher-or-lower pg-numth-span-higher-or-lower729,24384
+(defun pg-control-span-of pg-control-span-of755,25135
+(defun pg-move-span-contents pg-move-span-contents761,25339
+(defun pg-fixup-children-span pg-fixup-children-span815,27563
+(defun pg-move-region-down pg-move-region-down822,27771
+(defun pg-move-region-up pg-move-region-up831,28065
+(defun proof-forward-command proof-forward-command861,28905
+(defun proof-backward-command proof-backward-command882,29627
+(defvar pg-span-context-menu-keymappg-span-context-menu-keymap898,29871
+(defun pg-span-for-event pg-span-for-event914,30298
+(defun pg-span-context-menu pg-span-context-menu925,30682
+(defun pg-toggle-visibility pg-toggle-visibility940,31142
+(defun pg-create-in-span-context-menu pg-create-in-span-context-menu950,31464
+(defun pg-goals-buffers-hint pg-goals-buffers-hint1022,34017
+(defun pg-slow-fontify-tracing-hint pg-slow-fontify-tracing-hint1025,34184
+(defun pg-response-buffers-hint pg-response-buffers-hint1028,34340
+(defun pg-jump-to-end-hint pg-jump-to-end-hint1037,34689
+(defun pg-processing-complete-hint pg-processing-complete-hint1040,34805
+(defun pg-next-error-hint pg-next-error-hint1056,35491
+(defun pg-hint pg-hint1060,35628
+(defun pg-identifier-under-mouse-query pg-identifier-under-mouse-query1079,36304
+(defun proof-imenu-enable proof-imenu-enable1124,37931
 
 generic/pg-xhtml.el,573
 (defvar pg-xhtml-dir pg-xhtml-dir17,423
@@ -465,7 +544,7 @@ generic/pg-xhtml.el,573
 (defun pg-xhtml-display-file-mozilla pg-xhtml-display-file-mozilla79,2229
 (defalias 'pg-xhtml-display-file pg-xhtml-display-file84,2402
 
-generic/pg-xml.el,627
+generic/pg-xml.el,670
 (defun pg-xml-parse-string pg-xml-parse-string38,1118
 (defun pg-xml-parse-buffer pg-xml-parse-buffer49,1452
 (defun pg-xml-get-attr pg-xml-get-attr71,2185
@@ -478,12 +557,14 @@ generic/pg-xml.el,627
 (defconst pg-xml-header pg-xml-header118,3854
 (defun pg-xml-string-of pg-xml-string-of122,3931
 (defun pg-xml-output-internal pg-xml-output-internal133,4303
+(defun pg-xml-cdata pg-xml-cdata167,5453
 
 generic/_pkg.el,0
 
-generic/proof-autoloads.el,0
+generic/proof-autoloads.el,79
+(defalias 'proof-x-symbol-decode-region proof-x-symbol-decode-region246,9930
 
-generic/proof-config.el,16775
+generic/proof-config.el,16776
 (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
@@ -662,51 +743,51 @@ generic/proof-config.el,16775
 (defcustom proof-shell-thms-output-regexp proof-shell-thms-output-regexp2133,82098
 (defcustom proof-shell-filename-escapes proof-shell-filename-escapes2145,82483
 (defcustom proof-shell-process-connection-type proof-shell-process-connection-type2162,83163
-(defcustom proof-shell-strip-crs-from-input proof-shell-strip-crs-from-input2182,84041
-(defcustom proof-shell-strip-crs-from-output proof-shell-strip-crs-from-output2194,84530
-(defcustom proof-shell-insert-hook proof-shell-insert-hook2202,84898
-(defcustom proof-pre-shell-start-hook proof-pre-shell-start-hook2242,86862
-(defcustom proof-shell-handle-delayed-output-hookproof-shell-handle-delayed-output-hook2258,87334
-(defcustom proof-shell-handle-error-or-interrupt-hookproof-shell-handle-error-or-interrupt-hook2264,87549
-(defcustom proof-shell-pre-interrupt-hookproof-shell-pre-interrupt-hook2279,88163
-(defcustom proof-shell-process-output-system-specific proof-shell-process-output-system-specific2289,88533
-(defcustom proof-state-change-hook proof-state-change-hook2308,89398
-(defcustom proof-shell-font-lock-keywords proof-shell-font-lock-keywords2319,89780
-(defcustom proof-shell-syntax-table-entries proof-shell-syntax-table-entries2327,90108
-(defgroup proof-goals proof-goals2345,90480
-(defcustom pg-subterm-first-special-char pg-subterm-first-special-char2350,90601
-(defcustom pg-subterm-anns-use-stack pg-subterm-anns-use-stack2358,90913
-(defcustom pg-goals-change-goal pg-goals-change-goal2367,91217
-(defcustom pbp-goal-command pbp-goal-command2372,91332
-(defcustom pbp-hyp-command pbp-hyp-command2377,91488
-(defcustom pg-subterm-help-cmd pg-subterm-help-cmd2382,91650
-(defcustom pg-goals-error-regexp pg-goals-error-regexp2389,91886
-(defcustom proof-shell-result-start proof-shell-result-start2394,92046
-(defcustom proof-shell-result-end proof-shell-result-end2400,92280
-(defcustom pg-subterm-start-char pg-subterm-start-char2406,92493
-(defcustom pg-subterm-sep-char pg-subterm-sep-char2420,93075
-(defcustom pg-subterm-end-char pg-subterm-end-char2426,93254
-(defcustom pg-topterm-char pg-topterm-char2432,93411
-(defcustom proof-goals-font-lock-keywords proof-goals-font-lock-keywords2449,94017
-(defcustom proof-resp-font-lock-keywords proof-resp-font-lock-keywords2463,94696
-(defcustom pg-before-fontify-output-hook pg-before-fontify-output-hook2475,95274
-(defcustom pg-after-fontify-output-hook pg-after-fontify-output-hook2483,95634
-(defgroup proof-x-symbol proof-x-symbol2495,95888
-(defcustom proof-xsym-extra-modes proof-xsym-extra-modes2500,96016
-(defcustom proof-xsym-font-lock-keywords proof-xsym-font-lock-keywords2513,96645
-(defcustom proof-xsym-activate-command proof-xsym-activate-command2521,97022
-(defcustom proof-xsym-deactivate-command proof-xsym-deactivate-command2528,97258
-(defpgcustom x-symbol-language x-symbol-language2535,97500
-(defpgcustom favourites favourites2550,97947
-(defpgcustom menu-entries menu-entries2555,98137
-(defpgcustom help-menu-entries help-menu-entries2562,98374
-(defpgcustom keymap keymap2569,98637
-(defpgcustom completion-table completion-table2574,98808
-(defpgcustom tags-program tags-program2584,99173
-(defcustom proof-general-name proof-general-name2596,99346
-(defcustom proof-general-home-pageproof-general-home-page2601,99503
-(defcustom proof-unnamed-theorem-nameproof-unnamed-theorem-name2607,99662
-(defcustom proof-universal-keysproof-universal-keys2615,99938
+(defcustom proof-shell-strip-crs-from-input proof-shell-strip-crs-from-input2185,84210
+(defcustom proof-shell-strip-crs-from-output proof-shell-strip-crs-from-output2197,84699
+(defcustom proof-shell-insert-hook proof-shell-insert-hook2205,85067
+(defcustom proof-pre-shell-start-hook proof-pre-shell-start-hook2245,87031
+(defcustom proof-shell-handle-delayed-output-hookproof-shell-handle-delayed-output-hook2261,87503
+(defcustom proof-shell-handle-error-or-interrupt-hookproof-shell-handle-error-or-interrupt-hook2267,87718
+(defcustom proof-shell-pre-interrupt-hookproof-shell-pre-interrupt-hook2282,88332
+(defcustom proof-shell-process-output-system-specific proof-shell-process-output-system-specific2292,88702
+(defcustom proof-state-change-hook proof-state-change-hook2311,89567
+(defcustom proof-shell-font-lock-keywords proof-shell-font-lock-keywords2322,89949
+(defcustom proof-shell-syntax-table-entries proof-shell-syntax-table-entries2330,90277
+(defgroup proof-goals proof-goals2348,90649
+(defcustom pg-subterm-first-special-char pg-subterm-first-special-char2353,90770
+(defcustom pg-subterm-anns-use-stack pg-subterm-anns-use-stack2361,91082
+(defcustom pg-goals-change-goal pg-goals-change-goal2370,91386
+(defcustom pbp-goal-command pbp-goal-command2375,91501
+(defcustom pbp-hyp-command pbp-hyp-command2380,91657
+(defcustom pg-subterm-help-cmd pg-subterm-help-cmd2385,91819
+(defcustom pg-goals-error-regexp pg-goals-error-regexp2392,92055
+(defcustom proof-shell-result-start proof-shell-result-start2397,92215
+(defcustom proof-shell-result-end proof-shell-result-end2403,92449
+(defcustom pg-subterm-start-char pg-subterm-start-char2409,92662
+(defcustom pg-subterm-sep-char pg-subterm-sep-char2423,93244
+(defcustom pg-subterm-end-char pg-subterm-end-char2429,93423
+(defcustom pg-topterm-char pg-topterm-char2435,93580
+(defcustom proof-goals-font-lock-keywords proof-goals-font-lock-keywords2452,94186
+(defcustom proof-resp-font-lock-keywords proof-resp-font-lock-keywords2466,94865
+(defcustom pg-before-fontify-output-hook pg-before-fontify-output-hook2478,95443
+(defcustom pg-after-fontify-output-hook pg-after-fontify-output-hook2486,95803
+(defgroup proof-x-symbol proof-x-symbol2498,96057
+(defcustom proof-xsym-extra-modes proof-xsym-extra-modes2503,96185
+(defcustom proof-xsym-font-lock-keywords proof-xsym-font-lock-keywords2516,96814
+(defcustom proof-xsym-activate-command proof-xsym-activate-command2524,97191
+(defcustom proof-xsym-deactivate-command proof-xsym-deactivate-command2531,97427
+(defpgcustom x-symbol-language x-symbol-language2538,97669
+(defpgcustom favourites favourites2553,98116
+(defpgcustom menu-entries menu-entries2558,98306
+(defpgcustom help-menu-entries help-menu-entries2565,98543
+(defpgcustom keymap keymap2572,98806
+(defpgcustom completion-table completion-table2577,98977
+(defpgcustom tags-program tags-program2587,99342
+(defcustom proof-general-name proof-general-name2599,99515
+(defcustom proof-general-home-pageproof-general-home-page2604,99672
+(defcustom proof-unnamed-theorem-nameproof-unnamed-theorem-name2610,99831
+(defcustom proof-universal-keysproof-universal-keys2618,100107
 
 generic/proof-depends.el,1325
 (defvar proof-thm-names-of-files proof-thm-names-of-files19,540
@@ -737,18 +818,18 @@ generic/proof-easy-config.el,317
 
 generic/proof.el,809
 (deflocal proof-buffer-type proof-buffer-type35,900
-(defvar proof-shell-busy proof-shell-busy38,1014
-(defvar proof-included-files-list proof-included-files-list43,1171
-(defvar proof-script-buffer proof-script-buffer66,2186
-(defvar proof-previous-script-buffer proof-previous-script-buffer70,2326
-(defvar proof-shell-buffer proof-shell-buffer75,2580
-(defvar proof-goals-buffer proof-goals-buffer78,2666
-(defvar proof-response-buffer proof-response-buffer81,2721
-(defvar proof-trace-buffer proof-trace-buffer84,2782
-(defvar proof-thms-buffer proof-thms-buffer88,2936
-(defvar proof-shell-error-or-interrupt-seen proof-shell-error-or-interrupt-seen92,3091
-(defvar proof-shell-proof-completed proof-shell-proof-completed97,3316
-(defvar proof-terminal-string proof-terminal-string109,3861
+(defvar proof-shell-busy proof-shell-busy38,1013
+(defvar proof-included-files-list proof-included-files-list43,1169
+(defvar proof-script-buffer proof-script-buffer66,2185
+(defvar proof-previous-script-buffer proof-previous-script-buffer70,2325
+(defvar proof-shell-buffer proof-shell-buffer75,2579
+(defvar proof-goals-buffer proof-goals-buffer78,2665
+(defvar proof-response-buffer proof-response-buffer81,2720
+(defvar proof-trace-buffer proof-trace-buffer84,2781
+(defvar proof-thms-buffer proof-thms-buffer88,2935
+(defvar proof-shell-error-or-interrupt-seen proof-shell-error-or-interrupt-seen92,3090
+(defvar proof-shell-proof-completed proof-shell-proof-completed97,3315
+(defvar proof-terminal-string proof-terminal-string109,3860
 
 generic/proof-indent.el,475
 (defun proof-indent-indent proof-indent-indent13,353
@@ -928,109 +1009,109 @@ generic/proof-script.el,8107
 (defun proof-cmdstart-add-segment-for-cmd proof-cmdstart-add-segment-for-cmd1785,70000
 (defun proof-segment-up-to-cmdstart proof-segment-up-to-cmdstart1837,72199
 (defun proof-segment-up-to-cmdend proof-segment-up-to-cmdend1898,74559
-(defun proof-semis-to-vanillas proof-semis-to-vanillas1969,77204
-(defun proof-script-new-command-advance proof-script-new-command-advance2008,78530
-(defun proof-script-next-command-advance proof-script-next-command-advance2050,80271
-(defun proof-assert-until-point-interactive proof-assert-until-point-interactive2062,80712
-(defun proof-assert-until-point proof-assert-until-point2088,81834
-(defun proof-assert-next-commandproof-assert-next-command2141,84266
-(defun proof-goto-point proof-goto-point2189,86529
-(defun proof-insert-pbp-command proof-insert-pbp-command2206,87055
-(defun proof-done-retracting proof-done-retracting2238,88128
-(defun proof-setup-retract-action proof-setup-retract-action2265,89239
-(defun proof-last-goal-or-goalsave proof-last-goal-or-goalsave2275,89722
-(defun proof-retract-target proof-retract-target2299,90591
-(defun proof-retract-until-point-interactive proof-retract-until-point-interactive2384,94232
-(defun proof-retract-until-point proof-retract-until-point2392,94617
-(define-derived-mode proof-mode proof-mode2437,96478
-(defun proof-script-set-visited-file-name proof-script-set-visited-file-name2473,97964
-(defun proof-script-set-buffer-hooks proof-script-set-buffer-hooks2497,98966
-(defun proof-script-kill-buffer-fn proof-script-kill-buffer-fn2507,99462
-(defun proof-config-done-related proof-config-done-related2551,101284
-(defun proof-generic-goal-command-p proof-generic-goal-command-p2621,103850
-(defun proof-generic-state-preserving-p proof-generic-state-preserving-p2625,104025
-(defun proof-generic-count-undos proof-generic-count-undos2634,104542
-(defun proof-generic-find-and-forget proof-generic-find-and-forget2663,105572
-(defconst proof-script-important-settingsproof-script-important-settings2714,107397
-(defun proof-config-done proof-config-done2727,107934
-(defun proof-setup-parsing-mechanism proof-setup-parsing-mechanism2824,111482
-(defun proof-setup-imenu proof-setup-imenu2868,113335
-(defun proof-setup-func-menu proof-setup-func-menu2885,113940
+(defun proof-semis-to-vanillas proof-semis-to-vanillas1969,77206
+(defun proof-script-new-command-advance proof-script-new-command-advance2008,78532
+(defun proof-script-next-command-advance proof-script-next-command-advance2050,80273
+(defun proof-assert-until-point-interactive proof-assert-until-point-interactive2062,80714
+(defun proof-assert-until-point proof-assert-until-point2088,81836
+(defun proof-assert-next-commandproof-assert-next-command2141,84268
+(defun proof-goto-point proof-goto-point2189,86531
+(defun proof-insert-pbp-command proof-insert-pbp-command2206,87057
+(defun proof-done-retracting proof-done-retracting2238,88130
+(defun proof-setup-retract-action proof-setup-retract-action2265,89241
+(defun proof-last-goal-or-goalsave proof-last-goal-or-goalsave2275,89724
+(defun proof-retract-target proof-retract-target2299,90593
+(defun proof-retract-until-point-interactive proof-retract-until-point-interactive2384,94234
+(defun proof-retract-until-point proof-retract-until-point2392,94619
+(define-derived-mode proof-mode proof-mode2437,96480
+(defun proof-script-set-visited-file-name proof-script-set-visited-file-name2473,97966
+(defun proof-script-set-buffer-hooks proof-script-set-buffer-hooks2497,98968
+(defun proof-script-kill-buffer-fn proof-script-kill-buffer-fn2507,99464
+(defun proof-config-done-related proof-config-done-related2551,101286
+(defun proof-generic-goal-command-p proof-generic-goal-command-p2623,103854
+(defun proof-generic-state-preserving-p proof-generic-state-preserving-p2627,104029
+(defun proof-generic-count-undos proof-generic-count-undos2636,104546
+(defun proof-generic-find-and-forget proof-generic-find-and-forget2665,105576
+(defconst proof-script-important-settingsproof-script-important-settings2716,107401
+(defun proof-config-done proof-config-done2729,107938
+(defun proof-setup-parsing-mechanism proof-setup-parsing-mechanism2826,111486
+(defun proof-setup-imenu proof-setup-imenu2870,113339
+(defun proof-setup-func-menu proof-setup-func-menu2887,113944
 
 generic/proof-shell.el,5296
-(defvar proof-shell-last-output proof-shell-last-output19,458
-(defvar proof-marker proof-marker63,1714
-(defvar proof-action-list proof-action-list66,1811
-(defvar proof-shell-silent proof-shell-silent74,1987
-(defvar proof-shell-last-prompt proof-shell-last-prompt88,2470
-(defvar proof-shell-last-output-kind proof-shell-last-output-kind93,2700
-(defvar proof-shell-delayed-output proof-shell-delayed-output114,3522
-(defvar proof-shell-delayed-output-kind proof-shell-delayed-output-kind117,3643
-(defcustom proof-shell-active-scripting-indicatorproof-shell-active-scripting-indicator126,3846
-(defun proof-shell-ready-prover proof-shell-ready-prover179,5322
-(defun proof-shell-live-buffer proof-shell-live-buffer193,5862
-(defun proof-shell-available-p proof-shell-available-p200,6097
-(defun proof-grab-lock proof-grab-lock206,6320
-(defun proof-release-lock proof-release-lock223,7037
-(defcustom proof-shell-fiddle-frames proof-shell-fiddle-frames243,7593
-(deflocal proof-eagerly-raise proof-eagerly-raise250,7834
-(defun proof-shell-start proof-shell-start253,7940
-(defvar proof-shell-kill-function-hooks proof-shell-kill-function-hooks437,15128
-(defun proof-shell-kill-function proof-shell-kill-function440,15226
-(defun proof-shell-clear-state proof-shell-clear-state531,19076
-(defun proof-shell-exit proof-shell-exit546,19519
-(defun proof-shell-bail-out proof-shell-bail-out558,19964
-(defun proof-shell-restart proof-shell-restart567,20441
-(defvar proof-shell-no-response-display proof-shell-no-response-display609,21825
-(defvar proof-shell-urgent-message-marker proof-shell-urgent-message-marker612,21929
-(defvar proof-shell-urgent-message-scanner proof-shell-urgent-message-scanner615,22050
-(defun proof-shell-handle-output proof-shell-handle-output619,22177
-(defun proof-shell-handle-delayed-output proof-shell-handle-delayed-output693,25514
-(defvar proof-shell-no-error-display proof-shell-no-error-display728,26936
-(defun proof-shell-handle-error proof-shell-handle-error734,27142
-(defun proof-shell-handle-interrupt proof-shell-handle-interrupt752,27978
-(defun proof-shell-error-or-interrupt-action proof-shell-error-or-interrupt-action766,28600
-(defun proof-goals-pos proof-goals-pos793,29805
-(defun proof-pbp-focus-on-first-goal proof-pbp-focus-on-first-goal798,30010
-(defsubst proof-shell-string-match-safe proof-shell-string-match-safe810,30545
-(defun proof-shell-process-output proof-shell-process-output815,30713
-(defvar proof-shell-insert-space-fudge proof-shell-insert-space-fudge926,35353
-(defun proof-shell-insert proof-shell-insert935,35662
-(defun proof-shell-command-queue-item proof-shell-command-queue-item1003,38196
-(defun proof-shell-set-silent proof-shell-set-silent1008,38353
-(defun proof-shell-start-silent-item proof-shell-start-silent-item1014,38572
-(defun proof-shell-clear-silent proof-shell-clear-silent1020,38764
-(defun proof-shell-stop-silent-item proof-shell-stop-silent-item1026,38986
-(defun proof-shell-should-be-silent proof-shell-should-be-silent1033,39258
-(defun proof-append-alist proof-append-alist1046,39814
-(defun proof-start-queue proof-start-queue1102,41941
-(defun proof-extend-queue proof-extend-queue1113,42290
-(defun proof-shell-exec-loop proof-shell-exec-loop1124,42671
-(defun proof-shell-insert-loopback-cmd proof-shell-insert-loopback-cmd1189,45259
-(defun proof-shell-message proof-shell-message1227,46982
-(defun proof-shell-process-urgent-message proof-shell-process-urgent-message1233,47198
-(defvar proof-shell-minibuffer-urgent-interactive-input-history proof-shell-minibuffer-urgent-interactive-input-history1442,56063
-(defun proof-shell-minibuffer-urgent-interactive-input proof-shell-minibuffer-urgent-interactive-input1444,56133
-(defun proof-shell-process-urgent-messages proof-shell-process-urgent-messages1456,56503
-(defun proof-shell-filter proof-shell-filter1525,59559
-(defun proof-shell-filter-process-output proof-shell-filter-process-output1678,65896
-(defvar pg-last-tracing-output-time pg-last-tracing-output-time1731,67950
-(defvar pg-tracing-slow-mode pg-tracing-slow-mode1734,68056
-(defconst pg-slow-mode-duration pg-slow-mode-duration1737,68145
-(defconst pg-fast-tracing-mode-threshold pg-fast-tracing-mode-threshold1740,68227
-(defvar pg-tracing-cleanup-timer pg-tracing-cleanup-timer1743,68355
-(defun pg-tracing-tight-loop pg-tracing-tight-loop1745,68394
-(defun pg-finish-tracing-display pg-finish-tracing-display1788,70112
-(defun proof-shell-dont-show-annotations proof-shell-dont-show-annotations1801,70418
-(defun proof-shell-show-annotations proof-shell-show-annotations1817,70953
-(defun proof-shell-wait proof-shell-wait1838,71450
-(defun proof-done-invisible proof-done-invisible1858,72360
-(defun proof-shell-invisible-command proof-shell-invisible-command1901,74083
-(defun proof-shell-invisible-cmd-get-result proof-shell-invisible-cmd-get-result1934,75333
-(defun proof-shell-invisible-command-invisible-result proof-shell-invisible-command-invisible-result1951,76014
-(define-derived-mode proof-shell-mode proof-shell-mode1971,76518
-(defconst proof-shell-important-settingsproof-shell-important-settings2039,79071
-(defun proof-shell-config-done proof-shell-config-done2044,79171
+(defvar proof-shell-last-output proof-shell-last-output19,464
+(defvar proof-marker proof-marker63,1720
+(defvar proof-action-list proof-action-list66,1817
+(defvar proof-shell-silent proof-shell-silent74,1993
+(defvar proof-shell-last-prompt proof-shell-last-prompt88,2476
+(defvar proof-shell-last-output-kind proof-shell-last-output-kind93,2706
+(defvar proof-shell-delayed-output proof-shell-delayed-output114,3528
+(defvar proof-shell-delayed-output-kind proof-shell-delayed-output-kind117,3649
+(defcustom proof-shell-active-scripting-indicatorproof-shell-active-scripting-indicator126,3852
+(defun proof-shell-ready-prover proof-shell-ready-prover179,5328
+(defun proof-shell-live-buffer proof-shell-live-buffer193,5868
+(defun proof-shell-available-p proof-shell-available-p200,6103
+(defun proof-grab-lock proof-grab-lock206,6326
+(defun proof-release-lock proof-release-lock223,7043
+(defcustom proof-shell-fiddle-frames proof-shell-fiddle-frames243,7599
+(deflocal proof-eagerly-raise proof-eagerly-raise250,7840
+(defun proof-shell-start proof-shell-start253,7946
+(defvar proof-shell-kill-function-hooks proof-shell-kill-function-hooks445,15498
+(defun proof-shell-kill-function proof-shell-kill-function448,15596
+(defun proof-shell-clear-state proof-shell-clear-state539,19456
+(defun proof-shell-exit proof-shell-exit554,19899
+(defun proof-shell-bail-out proof-shell-bail-out566,20344
+(defun proof-shell-restart proof-shell-restart575,20821
+(defvar proof-shell-no-response-display proof-shell-no-response-display617,22205
+(defvar proof-shell-urgent-message-marker proof-shell-urgent-message-marker620,22309
+(defvar proof-shell-urgent-message-scanner proof-shell-urgent-message-scanner623,22430
+(defun proof-shell-handle-output proof-shell-handle-output627,22557
+(defun proof-shell-handle-delayed-output proof-shell-handle-delayed-output700,25880
+(defvar proof-shell-no-error-display proof-shell-no-error-display735,27302
+(defun proof-shell-handle-error proof-shell-handle-error741,27508
+(defun proof-shell-handle-interrupt proof-shell-handle-interrupt759,28344
+(defun proof-shell-error-or-interrupt-action proof-shell-error-or-interrupt-action773,28966
+(defun proof-goals-pos proof-goals-pos800,30171
+(defun proof-pbp-focus-on-first-goal proof-pbp-focus-on-first-goal805,30376
+(defsubst proof-shell-string-match-safe proof-shell-string-match-safe817,30911
+(defun proof-shell-process-output proof-shell-process-output822,31079
+(defvar proof-shell-insert-space-fudge proof-shell-insert-space-fudge933,35719
+(defun proof-shell-insert proof-shell-insert942,36028
+(defun proof-shell-command-queue-item proof-shell-command-queue-item1016,38940
+(defun proof-shell-set-silent proof-shell-set-silent1021,39097
+(defun proof-shell-start-silent-item proof-shell-start-silent-item1027,39316
+(defun proof-shell-clear-silent proof-shell-clear-silent1033,39508
+(defun proof-shell-stop-silent-item proof-shell-stop-silent-item1039,39730
+(defun proof-shell-should-be-silent proof-shell-should-be-silent1046,40002
+(defun proof-append-alist proof-append-alist1059,40558
+(defun proof-start-queue proof-start-queue1115,42685
+(defun proof-extend-queue proof-extend-queue1126,43034
+(defun proof-shell-exec-loop proof-shell-exec-loop1137,43415
+(defun proof-shell-insert-loopback-cmd proof-shell-insert-loopback-cmd1202,46003
+(defun proof-shell-message proof-shell-message1239,47711
+(defun proof-shell-process-urgent-message proof-shell-process-urgent-message1245,47927
+(defvar proof-shell-minibuffer-urgent-interactive-input-history proof-shell-minibuffer-urgent-interactive-input-history1453,56775
+(defun proof-shell-minibuffer-urgent-interactive-input proof-shell-minibuffer-urgent-interactive-input1455,56845
+(defun proof-shell-process-urgent-messages proof-shell-process-urgent-messages1467,57215
+(defun proof-shell-filter proof-shell-filter1539,60385
+(defun proof-shell-filter-process-output proof-shell-filter-process-output1692,66722
+(defvar pg-last-tracing-output-time pg-last-tracing-output-time1745,68776
+(defvar pg-tracing-slow-mode pg-tracing-slow-mode1748,68882
+(defconst pg-slow-mode-duration pg-slow-mode-duration1751,68971
+(defconst pg-fast-tracing-mode-threshold pg-fast-tracing-mode-threshold1754,69053
+(defvar pg-tracing-cleanup-timer pg-tracing-cleanup-timer1757,69181
+(defun pg-tracing-tight-loop pg-tracing-tight-loop1759,69220
+(defun pg-finish-tracing-display pg-finish-tracing-display1802,70938
+(defun proof-shell-dont-show-annotations proof-shell-dont-show-annotations1815,71244
+(defun proof-shell-show-annotations proof-shell-show-annotations1831,71779
+(defun proof-shell-wait proof-shell-wait1852,72276
+(defun proof-done-invisible proof-done-invisible1872,73186
+(defun proof-shell-invisible-command proof-shell-invisible-command1915,74909
+(defun proof-shell-invisible-cmd-get-result proof-shell-invisible-cmd-get-result1948,76159
+(defun proof-shell-invisible-command-invisible-result proof-shell-invisible-command-invisible-result1965,76840
+(define-derived-mode proof-shell-mode proof-shell-mode1985,77344
+(defconst proof-shell-important-settingsproof-shell-important-settings2053,79897
+(defun proof-shell-config-done proof-shell-config-done2058,79997
 
 generic/proof-site.el,1030
 (defgroup proof-general proof-general20,594
@@ -1040,17 +1121,17 @@ generic/proof-site.el,1030
 (defcustom proof-images-directoryproof-images-directory62,1939
 (defcustom proof-info-directoryproof-info-directory68,2140
 (defcustom proof-assistant-tableproof-assistant-table97,3389
-(defun proof-string-to-list proof-string-to-list163,5568
-(defcustom proof-assistants proof-assistants179,6059
-(defun proof-ready-for-assistant proof-ready-for-assistant215,7472
-(defconst proof-general-version proof-general-version328,11681
-(defconst proof-general-short-version proof-general-short-version331,11824
-(defcustom proof-assistant-cusgrp proof-assistant-cusgrp348,12406
-(defcustom proof-assistant-internals-cusgrp proof-assistant-internals-cusgrp356,12709
-(defcustom proof-assistant proof-assistant364,13021
-(defcustom proof-assistant-symbol proof-assistant-symbol372,13290
-
-generic/proof-splash.el,976
+(defun proof-string-to-list proof-string-to-list163,5571
+(defcustom proof-assistants proof-assistants179,6062
+(defun proof-ready-for-assistant proof-ready-for-assistant215,7475
+(defconst proof-general-version proof-general-version328,11684
+(defconst proof-general-short-version proof-general-short-version331,11825
+(defcustom proof-assistant-cusgrp proof-assistant-cusgrp348,12407
+(defcustom proof-assistant-internals-cusgrp proof-assistant-internals-cusgrp356,12710
+(defcustom proof-assistant proof-assistant364,13022
+(defcustom proof-assistant-symbol proof-assistant-symbol372,13291
+
+generic/proof-splash.el,1149
 (defcustom proof-splash-enable proof-splash-enable14,379
 (defcustom proof-splash-time proof-splash-time19,531
 (defcustom proof-splash-contentsproof-splash-contents27,816
@@ -1060,37 +1141,39 @@ generic/proof-splash.el,976
 (defvar proof-splash-timeout-conf proof-splash-timeout-conf136,4662
 (defun proof-splash-centre-spaces proof-splash-centre-spaces139,4775
 (defun proof-splash-remove-screen proof-splash-remove-screen167,5944
-(defun proof-splash-remove-buffer proof-splash-remove-buffer188,6661
-(defvar proof-splash-seen proof-splash-seen204,7325
-(defun proof-splash-display-screen proof-splash-display-screen208,7442
-(defun proof-splash-message proof-splash-message283,10601
-(defun proof-splash-timeout-waiter proof-splash-timeout-waiter293,10964
-(defun proof-splash-set-frame-titles proof-splash-set-frame-titles310,11703
-
-generic/proof-syntax.el,1296
+(defun proof-splash-remove-buffer proof-splash-remove-buffer188,6693
+(defvar proof-splash-seen proof-splash-seen204,7357
+(defun proof-splash-display-screen proof-splash-display-screen208,7474
+(defun proof-splash-message proof-splash-message283,10633
+(defun proof-splash-timeout-waiter proof-splash-timeout-waiter293,10996
+(defvar proof-splash-old-frame-title-format proof-splash-old-frame-title-format310,11735
+(defun proof-splash-set-frame-titles proof-splash-set-frame-titles312,11785
+(defun proof-splash-unset-frame-titles proof-splash-unset-frame-titles321,12101
+
+generic/proof-syntax.el,1297
 (defun proof-ids-to-regexp proof-ids-to-regexp16,445
-(defun proof-anchor-regexp proof-anchor-regexp20,609
-(defconst proof-no-regexpproof-no-regexp24,711
-(defun proof-regexp-alt proof-regexp-alt29,806
-(defun proof-regexp-region proof-regexp-region38,1092
-(defun proof-re-search-forward-region proof-re-search-forward-region47,1515
-(defun proof-re-search-forward proof-re-search-forward60,2010
-(defun proof-re-search-backward proof-re-search-backward66,2271
-(defun proof-string-match proof-string-match72,2535
-(defun proof-string-match-safe proof-string-match-safe78,2767
-(defun proof-stringfn-match proof-stringfn-match82,2972
-(defun proof-looking-at proof-looking-at89,3232
-(defun proof-looking-at-safe proof-looking-at-safe95,3422
-(defun proof-looking-at-syntactic-context proof-looking-at-syntactic-context99,3562
-(defun proof-replace-string proof-replace-string111,3894
-(defun proof-replace-regexp proof-replace-regexp116,4079
-(defvar proof-id proof-id124,4292
-(defun proof-ids proof-ids130,4512
-(defun proof-zap-commas proof-zap-commas143,5073
-(defun proof-format proof-format161,5636
-(defun proof-format-filename proof-format-filename180,6275
-(defun proof-insert proof-insert229,7753
-(defun proof-splice-separator proof-splice-separator265,8762
+(defun proof-anchor-regexp proof-anchor-regexp22,701
+(defconst proof-no-regexpproof-no-regexp26,803
+(defun proof-regexp-alt proof-regexp-alt31,898
+(defun proof-regexp-region proof-regexp-region40,1184
+(defun proof-re-search-forward-region proof-re-search-forward-region49,1607
+(defun proof-re-search-forward proof-re-search-forward62,2102
+(defun proof-re-search-backward proof-re-search-backward68,2363
+(defun proof-string-match proof-string-match74,2627
+(defun proof-string-match-safe proof-string-match-safe80,2859
+(defun proof-stringfn-match proof-stringfn-match84,3064
+(defun proof-looking-at proof-looking-at91,3324
+(defun proof-looking-at-safe proof-looking-at-safe97,3514
+(defun proof-looking-at-syntactic-context proof-looking-at-syntactic-context101,3654
+(defun proof-replace-string proof-replace-string113,3986
+(defun proof-replace-regexp proof-replace-regexp118,4171
+(defvar proof-id proof-id126,4384
+(defun proof-ids proof-ids132,4604
+(defun proof-zap-commas proof-zap-commas145,5165
+(defun proof-format proof-format163,5728
+(defun proof-format-filename proof-format-filename182,6367
+(defun proof-insert proof-insert231,7845
+(defun proof-splice-separator proof-splice-separator267,8854
 
 generic/proof-system.el,0
 
@@ -1187,25 +1270,25 @@ generic/proof-utils.el,3150
 (defun proof-fontify-buffer proof-fontify-buffer482,17267
 (defun proof-warn-if-unset proof-warn-if-unset495,17508
 (defun proof-get-window-for-buffer proof-get-window-for-buffer500,17726
-(defun proof-display-and-keep-buffer proof-display-and-keep-buffer537,19378
-(defun proof-clean-buffer proof-clean-buffer568,20654
-(defun proof-message proof-message582,21191
-(defun proof-warning proof-warning587,21404
-(defun pg-internal-warning pg-internal-warning593,21686
-(defun proof-debug proof-debug601,22005
-(defun proof-switch-to-buffer proof-switch-to-buffer616,22678
-(defun proof-resize-window-tofit proof-resize-window-tofit649,24370
-(defun proof-submit-bug-report proof-submit-bug-report749,28398
-(defun proof-deftoggle-fn proof-deftoggle-fn773,29200
-(defmacro proof-deftoggle proof-deftoggle788,29855
-(defun proof-defintset-fn proof-defintset-fn795,30229
-(defmacro proof-defintset proof-defintset809,30884
-(defun proof-defstringset-fn proof-defstringset-fn816,31261
-(defmacro proof-defstringset proof-defstringset829,31888
-(defun pg-custom-save-vars pg-custom-save-vars843,32353
-(defun pg-custom-reset-vars pg-custom-reset-vars861,33079
-(defun proof-locate-executable proof-locate-executable874,33416
-(defconst proof-extra-flsproof-extra-fls906,34829
+(defun proof-display-and-keep-buffer proof-display-and-keep-buffer537,19364
+(defun proof-clean-buffer proof-clean-buffer569,20673
+(defun proof-message proof-message583,21210
+(defun proof-warning proof-warning588,21423
+(defun pg-internal-warning pg-internal-warning594,21705
+(defun proof-debug proof-debug602,22024
+(defun proof-switch-to-buffer proof-switch-to-buffer617,22707
+(defun proof-resize-window-tofit proof-resize-window-tofit650,24399
+(defun proof-submit-bug-report proof-submit-bug-report750,28411
+(defun proof-deftoggle-fn proof-deftoggle-fn775,29277
+(defmacro proof-deftoggle proof-deftoggle790,29932
+(defun proof-defintset-fn proof-defintset-fn797,30306
+(defmacro proof-defintset proof-defintset811,30961
+(defun proof-defstringset-fn proof-defstringset-fn818,31338
+(defmacro proof-defstringset proof-defstringset831,31965
+(defun pg-custom-save-vars pg-custom-save-vars845,32430
+(defun pg-custom-reset-vars pg-custom-reset-vars863,33156
+(defun proof-locate-executable proof-locate-executable876,33493
+(defconst proof-extra-flsproof-extra-fls905,34674
 
 generic/proof-x-symbol.el,960
 (defvar proof-x-symbol-initialized proof-x-symbol-initialized54,2151
@@ -1213,13 +1296,13 @@ generic/proof-x-symbol.el,960
 (defun proof-x-symbol-support-maybe-available proof-x-symbol-support-maybe-available63,2428
 (defun proof-x-symbol-initialize proof-x-symbol-initialize83,3173
 (defun proof-x-symbol-enable proof-x-symbol-enable178,7036
-(defun proof-x-symbol-refresh-output-buffers proof-x-symbol-refresh-output-buffers200,8005
-(defun proof-x-symbol-mode-associated-buffers proof-x-symbol-mode-associated-buffers215,8759
-(defalias 'proof-x-symbol-decode-region proof-x-symbol-decode-region237,9463
-(defun proof-x-symbol-encode-shell-input proof-x-symbol-encode-shell-input239,9529
-(defun proof-x-symbol-set-language proof-x-symbol-set-language256,10120
-(defun proof-x-symbol-shell-config proof-x-symbol-shell-config261,10291
-(defun proof-x-symbol-config-output-buffer proof-x-symbol-config-output-buffer309,12458
+(defun proof-x-symbol-refresh-output-buffers proof-x-symbol-refresh-output-buffers208,8353
+(defun proof-x-symbol-mode-associated-buffers proof-x-symbol-mode-associated-buffers223,9107
+(defalias 'proof-x-symbol-decode-region proof-x-symbol-decode-region245,9811
+(defun proof-x-symbol-encode-shell-input proof-x-symbol-encode-shell-input247,9877
+(defun proof-x-symbol-set-language proof-x-symbol-set-language264,10468
+(defun proof-x-symbol-shell-config proof-x-symbol-shell-config269,10639
+(defun proof-x-symbol-config-output-buffer proof-x-symbol-config-output-buffer317,12806
 
 hol98/hol98.el,0
 
@@ -1232,57 +1315,57 @@ isa/isabelle-system.el,3268
 (defgroup isabelle isabelle23,719
 (defcustom isabelle-web-pageisabelle-web-page27,848
 (defcustom isa-isatool-commandisa-isatool-command38,1143
-(defvar isatool-not-found isatool-not-found64,2062
-(defun isa-set-isatool-command isa-set-isatool-command67,2175
-(defun isa-shell-command-to-string isa-shell-command-to-string87,2959
-(defun isa-getenv isa-getenv95,3411
-(defcustom isabelle-program-name isabelle-program-name114,4068
-(defvar isabelle-prog-name isabelle-prog-name140,5016
-(defun isabelle-command-line isabelle-command-line143,5143
-(defun isabelle-choose-logic isabelle-choose-logic166,6051
-(defun isa-tool-list-logics isa-tool-list-logics188,7023
-(defun isa-view-doc isa-view-doc195,7261
-(defvar isabelle-version-string isabelle-version-string202,7485
-(defun isa-version isa-version204,7526
-(defconst isa-supports-pgip isa-supports-pgip217,8009
-(defun isa-tool-list-docs isa-tool-list-docs225,8239
-(defun isa-quit isa-quit243,8961
-(defconst isabelle-verbatim-regexp isabelle-verbatim-regexp250,9156
-(defun isabelle-verbatim isabelle-verbatim253,9297
-(defcustom isabelle-refresh-logics isabelle-refresh-logics269,9888
-(defcustom isabelle-logics-available isabelle-logics-available277,10215
-(defcustom isabelle-chosen-logic isabelle-chosen-logic285,10515
-(defconst isabelle-docs-menu isabelle-docs-menu298,10983
-(defun isabelle-logics-menu-calculate isabelle-logics-menu-calculate308,11376
-(defvar isabelle-time-to-refresh-logics isabelle-time-to-refresh-logics324,11885
-(defun isabelle-logics-menu-refresh isabelle-logics-menu-refresh327,11978
-(defun isabelle-logics-menu-filter isabelle-logics-menu-filter344,12677
-(defun isabelle-menu-bar-update-logics isabelle-menu-bar-update-logics350,12887
-(defvar isabelle-logics-menu-entries isabelle-logics-menu-entries361,13243
-(defvar isabelle-logics-menu isabelle-logics-menu363,13315
-(defun isabelle-load-isar-keywords isabelle-load-isar-keywords376,13933
-(defpacustom show-types show-types403,14888
-(defpacustom show-sorts show-sorts408,15004
-(defpacustom show-consts show-consts413,15120
-(defpacustom long-names long-names418,15254
-(defpacustom eta-contract eta-contract423,15386
-(defpacustom trace-simplifier trace-simplifier428,15527
-(defpacustom trace-rules trace-rules433,15659
-(defpacustom quick-and-dirty quick-and-dirty438,15791
-(defpacustom full-proofs full-proofs443,15927
-(defpacustom global-timing global-timing449,16236
-(defpacustom theorem-dependencies theorem-dependencies455,16394
-(defpacustom goals-limit goals-limit461,16659
-(defpacustom prems-limit prems-limit466,16798
-(defpacustom print-depth print-depth471,16958
-(defpgdefault menu-entriesmenu-entries483,17247
-(defpgdefault help-menu-entries help-menu-entries490,17409
-(defpgdefault x-symbol-language x-symbol-language498,17603
-(defun isabelle-convert-idmarkup-to-subterm isabelle-convert-idmarkup-to-subterm521,18218
-(defun isabelle-create-span-menu isabelle-create-span-menu546,19257
-(defun isabelle-xml-sml-escapes isabelle-xml-sml-escapes563,19751
-(defun isabelle-process-pgip isabelle-process-pgip566,19852
-(defun isabelle-parse-syntax-dump isabelle-parse-syntax-dump583,20438
+(defvar isatool-not-found isatool-not-found65,2088
+(defun isa-set-isatool-command isa-set-isatool-command68,2201
+(defun isa-shell-command-to-string isa-shell-command-to-string88,2985
+(defun isa-getenv isa-getenv94,3209
+(defcustom isabelle-program-name isabelle-program-name113,3866
+(defvar isabelle-prog-name isabelle-prog-name139,4814
+(defun isabelle-command-line isabelle-command-line142,4941
+(defun isabelle-choose-logic isabelle-choose-logic165,5849
+(defun isa-tool-list-logics isa-tool-list-logics187,6821
+(defun isa-view-doc isa-view-doc194,7059
+(defvar isabelle-version-string isabelle-version-string201,7283
+(defun isa-version isa-version203,7324
+(defconst isa-supports-pgip isa-supports-pgip216,7807
+(defun isa-tool-list-docs isa-tool-list-docs224,8037
+(defun isa-quit isa-quit242,8759
+(defconst isabelle-verbatim-regexp isabelle-verbatim-regexp249,8954
+(defun isabelle-verbatim isabelle-verbatim252,9095
+(defcustom isabelle-refresh-logics isabelle-refresh-logics268,9686
+(defcustom isabelle-logics-available isabelle-logics-available276,10013
+(defcustom isabelle-chosen-logic isabelle-chosen-logic284,10313
+(defconst isabelle-docs-menu isabelle-docs-menu297,10781
+(defun isabelle-logics-menu-calculate isabelle-logics-menu-calculate307,11174
+(defvar isabelle-time-to-refresh-logics isabelle-time-to-refresh-logics323,11683
+(defun isabelle-logics-menu-refresh isabelle-logics-menu-refresh326,11776
+(defun isabelle-logics-menu-filter isabelle-logics-menu-filter343,12475
+(defun isabelle-menu-bar-update-logics isabelle-menu-bar-update-logics349,12685
+(defvar isabelle-logics-menu-entries isabelle-logics-menu-entries360,13041
+(defvar isabelle-logics-menu isabelle-logics-menu362,13113
+(defun isabelle-load-isar-keywords isabelle-load-isar-keywords375,13731
+(defpacustom show-types show-types402,14686
+(defpacustom show-sorts show-sorts407,14802
+(defpacustom show-consts show-consts412,14918
+(defpacustom long-names long-names417,15052
+(defpacustom eta-contract eta-contract422,15184
+(defpacustom trace-simplifier trace-simplifier427,15325
+(defpacustom trace-rules trace-rules432,15457
+(defpacustom quick-and-dirty quick-and-dirty437,15589
+(defpacustom full-proofs full-proofs442,15725
+(defpacustom global-timing global-timing448,16034
+(defpacustom theorem-dependencies theorem-dependencies454,16192
+(defpacustom goals-limit goals-limit460,16457
+(defpacustom prems-limit prems-limit465,16596
+(defpacustom print-depth print-depth470,16756
+(defpgdefault menu-entriesmenu-entries482,17045
+(defpgdefault help-menu-entries help-menu-entries489,17207
+(defpgdefault x-symbol-language x-symbol-language497,17401
+(defun isabelle-convert-idmarkup-to-subterm isabelle-convert-idmarkup-to-subterm520,18016
+(defun isabelle-create-span-menu isabelle-create-span-menu545,19055
+(defun isabelle-xml-sml-escapes isabelle-xml-sml-escapes562,19549
+(defun isabelle-process-pgip isabelle-process-pgip565,19650
+(defun isabelle-parse-syntax-dump isabelle-parse-syntax-dump582,20236
 
 isa/isa.el,2283
 (defcustom isa-outline-regexpisa-outline-regexp43,1354
@@ -1468,37 +1551,40 @@ isa/x-symbol-isabelle.el,3169
 
 isa/x-symbol-isa.el,0
 
-isar/isar.el,1883
-(defcustom isar-keywords-name isar-keywords-name28,630
-(defpgdefault completion-table completion-table45,1154
-(defcustom isar-web-pageisar-web-page47,1207
-(defun isar-detect-header isar-detect-header65,1571
-(defun isar-strip-terminators isar-strip-terminators100,2834
-(defun isar-markup-ml isar-markup-ml113,3205
-(defun isar-mode-config-set-variables isar-mode-config-set-variables118,3340
-(defun isar-shell-mode-config-set-variables isar-shell-mode-config-set-variables182,6171
-(defun isar-remove-file isar-remove-file296,10966
-(defun isar-shell-compute-new-files-list isar-shell-compute-new-files-list306,11329
-(defun isar-activate-scripting isar-activate-scripting317,11795
-(define-derived-mode isar-shell-mode isar-shell-mode326,11965
-(define-derived-mode isar-response-mode isar-response-mode331,12088
-(define-derived-mode isar-goals-mode isar-goals-mode336,12270
-(define-derived-mode isar-mode isar-mode341,12445
-(defpgdefault menu-entriesmenu-entries388,14264
-(defun isar-count-undos isar-count-undos419,15622
-(defun isar-find-and-forget isar-find-and-forget445,16723
-(defun isar-goal-command-p isar-goal-command-p492,18568
-(defun isar-global-save-command-p isar-global-save-command-p496,18700
-(defvar isar-current-goal isar-current-goal517,19537
-(defun isar-state-preserving-p isar-state-preserving-p520,19603
-(defvar isar-shell-current-line-width isar-shell-current-line-width543,20637
-(defun isar-shell-adjust-line-width isar-shell-adjust-line-width549,20855
-(defun isar-pre-shell-start isar-pre-shell-start569,21738
-(defun isar-preprocessing isar-preprocessing581,22074
-(defun isar-mode-config isar-mode-config604,23285
-(defun isar-shell-mode-config isar-shell-mode-config616,23855
-(defun isar-response-mode-config isar-response-mode-config627,24225
-(defun isar-goals-mode-config isar-goals-mode-config636,24482
+isar/isar-autotest.el,0
+
+isar/isar.el,1927
+(defcustom isar-keywords-name isar-keywords-name28,631
+(defpgdefault completion-table completion-table45,1155
+(defcustom isar-web-pageisar-web-page47,1208
+(defun isar-detect-header isar-detect-header65,1572
+(defun isar-strip-terminators isar-strip-terminators100,2835
+(defun isar-markup-ml isar-markup-ml113,3206
+(defun isar-mode-config-set-variables isar-mode-config-set-variables118,3341
+(defun isar-shell-mode-config-set-variables isar-shell-mode-config-set-variables182,6172
+(defun isar-remove-file isar-remove-file296,10939
+(defun isar-shell-compute-new-files-list isar-shell-compute-new-files-list306,11302
+(defun isar-activate-scripting isar-activate-scripting317,11768
+(define-derived-mode isar-shell-mode isar-shell-mode326,11938
+(define-derived-mode isar-response-mode isar-response-mode331,12061
+(define-derived-mode isar-goals-mode isar-goals-mode336,12243
+(define-derived-mode isar-mode isar-mode341,12418
+(define-key (proof-ass proof-ass363,12999
+(defpgdefault menu-entriesmenu-entries398,14550
+(defun isar-count-undos isar-count-undos428,15872
+(defun isar-find-and-forget isar-find-and-forget454,16973
+(defun isar-goal-command-p isar-goal-command-p501,18818
+(defun isar-global-save-command-p isar-global-save-command-p505,18950
+(defvar isar-current-goal isar-current-goal526,19787
+(defun isar-state-preserving-p isar-state-preserving-p529,19853
+(defvar isar-shell-current-line-width isar-shell-current-line-width552,20887
+(defun isar-shell-adjust-line-width isar-shell-adjust-line-width558,21105
+(defun isar-pre-shell-start isar-pre-shell-start578,21988
+(defun isar-preprocessing isar-preprocessing590,22324
+(defun isar-mode-config isar-mode-config613,23535
+(defun isar-shell-mode-config isar-shell-mode-config625,24105
+(defun isar-response-mode-config isar-response-mode-config636,24475
+(defun isar-goals-mode-config isar-goals-mode-config645,24732
 
 isar/isar-keywords.el,1650
 (defconst isar-keywords-majorisar-keywords-major14,378
@@ -1692,476 +1778,24 @@ lego/lego-syntax.el,919
 
 lego/x-symbol-lego.el,0
 
-lib/holes.el,3536
-(defun holes-short-doc holes-short-doc24,736
-(defcustom empty-hole-string empty-hole-string149,5370
-(defcustom empty-hole-regexp empty-hole-regexp152,5475
-(defcustom hole-search-limit hole-search-limit155,6075
-(defface active-hole-faceactive-hole-face168,6441
-(defface inactive-hole-faceinactive-hole-face178,6898
-(defun region-beginning-or-nil region-beginning-or-nil197,7434
-(defun region-end-or-nil region-end-or-nil201,7523
-(defun copy-active-region copy-active-region205,7602
-(defun is-hole-p is-hole-p211,7780
-(defun hole-start-position hole-start-position216,7840
-(defun hole-end-position hole-end-position221,7977
-(defun hole-buffer hole-buffer226,8107
-(defun hole-at hole-at231,8229
-(defun active-hole-exist-p active-hole-exist-p240,8417
-(defun active-hole-start-position active-hole-start-position250,8668
-(defun active-hole-end-position active-hole-end-position261,9018
-(defun active-hole-buffer active-hole-buffer273,9364
-(defun goto-active-hole goto-active-hole284,9644
-(defun highlight-hole-as-active highlight-hole-as-active296,9917
-(defun highlight-hole highlight-hole306,10224
-(defun disable-active-hole disable-active-hole317,10519
-(defun set-active-hole set-active-hole335,11028
-(defun is-in-hole-p is-in-hole-p347,11329
-(defun make-hole make-hole357,11474
-(defun make-hole-at make-hole-at382,12289
-(defun clear-hole clear-hole401,12731
-(defun clear-hole-at clear-hole-at411,12948
-(defun map-holes map-holes420,13177
-(defun mapcar-holes mapcar-holes426,13291
-(defun clear-all-buffer-holes clear-all-buffer-holes430,13390
-(defun next-hole next-hole442,13624
-(defun next-after-active-hole next-after-active-hole451,13888
-(defun set-active-hole-next set-active-hole-next458,14068
-(defun set-active-hole-next-after-active set-active-hole-next-after-active475,14425
-(defun replace-segment replace-segment486,14583
-(defun replace-hole replace-hole502,14899
-(defun replace-active-hole replace-active-hole536,16055
-(defun replace-update-active-hole replace-update-active-hole545,16338
-(defun delete-update-active-hole delete-update-active-hole568,16964
-(defun set-make-active-hole set-make-active-hole577,17161
-(defun mouse-replace-active-hole mouse-replace-active-hole624,18508
-(defun destroy-hole destroy-hole642,18984
-(defun hole-at-event hole-at-event657,19295
-(defun mouse-destroy-hole mouse-destroy-hole659,19354
-(defun mouse-forget-hole mouse-forget-hole667,19528
-(defun mouse-set-make-active-hole mouse-set-make-active-hole681,19769
-(defun mouse-set-active-hole mouse-set-active-hole701,20220
-(defun set-point-next-hole-destroy set-point-next-hole-destroy711,20414
-(defun count-char-in-string count-char-in-string775,22661
-(defun count-re-in-string count-re-in-string785,22866
-(defun count-chars-in-last-expand count-chars-in-last-expand795,23077
-(defun count-newlines-in-last-expand count-newlines-in-last-expand799,23166
-(defun indent-last-expand indent-last-expand803,23277
-(defun count-holes-in-last-expand count-holes-in-last-expand818,23603
-(defun replace-string-by-holes replace-string-by-holes822,23722
-(defun replace-string-by-holes-backward replace-string-by-holes-backward841,24148
-(defun replace-string-by-holes-move-point replace-string-by-holes-move-point872,24966
-(defun replace-string-by-holes-backward-move-point replace-string-by-holes-backward-move-point879,25120
-(defun holes-abbrev-complete holes-abbrev-complete889,25296
-(defun insert-and-expand insert-and-expand911,26098
-
-lib/proof-compat.el,1194
-(defvar proof-running-on-XEmacs proof-running-on-XEmacs24,760
-(defvar proof-running-on-Emacs21 proof-running-on-Emacs2126,882
-(defvar proof-running-on-win32 proof-running-on-win3230,1129
-(defun pg-custom-undeclare-variable pg-custom-undeclare-variable41,1562
-(defun subst-char-in-string subst-char-in-string112,3702
-(defun replace-regexp-in-string replace-regexp-in-string126,4256
-(defconst menuvisiblep menuvisiblep188,6969
-(defun set-window-text-height set-window-text-height205,7588
-(defmacro save-selected-frame save-selected-frame231,8538
-(defun warn warn270,9840
-(defun redraw-modeline redraw-modeline277,10095
-(defun replace-in-string replace-in-string292,10662
-(defun proof-buffer-syntactic-context-emulate proof-buffer-syntactic-context-emulate341,12180
-(defvar read-shell-command-mapread-shell-command-map374,13487
-(defun read-shell-command read-shell-command392,14189
-(defun remassq remassq404,14670
-(defun remassoc remassoc416,15059
-(defun frames-of-buffer frames-of-buffer429,15504
-(defmacro with-selected-window with-selected-window468,16767
-(defun pg-pop-to-buffer pg-pop-to-buffer504,17892
-(defun process-live-p process-live-p555,19744
-
-lib/span.el,192
-(defsubst delete-spans delete-spans22,471
-(defsubst span-property-safe span-property-safe26,625
-(defsubst set-span-start set-span-start30,764
-(defsubst set-span-end set-span-end34,896
-
-lib/span-extent.el,1346
-(defsubst make-span make-span16,557
-(defsubst detach-span detach-span20,679
-(defsubst set-span-endpoints set-span-endpoints24,766
-(defsubst set-span-property set-span-property28,899
-(defsubst span-read-only span-read-only32,1026
-(defsubst span-read-write span-read-write36,1130
-(defun span-give-warning span-give-warning40,1237
-(defun span-write-warning span-write-warning44,1335
-(defsubst span-property span-property49,1535
-(defsubst delete-span delete-span53,1650
-(defsubst mapcar-spans mapcar-spans59,1821
-(defsubst span-at span-at63,2027
-(defsubst span-at-before span-at-before67,2144
-(defsubst span-start span-start72,2341
-(defsubst span-end span-end76,2470
-(defsubst prev-span prev-span80,2593
-(defsubst next-span next-span84,2739
-(defsubst span-live-p span-live-p88,2881
-(defun span-raise span-raise96,3153
-(defalias 'span-object span-object100,3252
-(defalias 'span-string span-string101,3291
-(defsubst make-detached-span make-detached-span104,3377
-(defsubst span-buffer span-buffer110,3474
-(defsubst span-detached-p span-detached-p115,3566
-(defsubst set-span-face set-span-face120,3678
-(defsubst fold-spans fold-spans125,3774
-(defsubst set-span-properties set-span-properties130,3972
-(defsubst set-span-keymap set-span-keymap135,4081
-(defsubst span-at-event span-at-event140,4196
-
-lib/span-overlay.el,2198
-(defvar before-list before-list20,771
-(defun foldr foldr27,906
-(defun foldl foldl39,1239
-(defsubst span-start span-start51,1556
-(defsubst span-end span-end55,1648
-(defun set-span-property set-span-property59,1734
-(defsubst span-property span-property63,1850
-(defun span-read-only-hook span-read-only-hook67,1961
-(defun span-read-only span-read-only71,2093
-(defun span-read-write span-read-write86,2871
-(defun span-give-warning span-give-warning92,3090
-(defun span-write-warning span-write-warning96,3198
-(defun int-nil-lt int-nil-lt101,3421
-(defun span-lt span-lt110,3624
-(defun span-traverse span-traverse115,3783
-(defun add-span add-span131,4230
-(defun make-span make-span145,4632
-(defun remove-span remove-span149,4763
-(defun spans-at-point spans-at-point162,5216
-(defun append-unique append-unique176,5696
-(defun spans-at-region spans-at-region179,5783
-(defun spans-at-point-prop spans-at-point-prop186,6005
-(defun spans-at-region-prop spans-at-region-prop194,6255
-(defun span-at span-at206,6602
-(defsubst detach-span detach-span212,6816
-(defsubst delete-span delete-span218,6943
-(defsubst set-span-endpoints set-span-endpoints226,7186
-(defsubst mapcar-spans mapcar-spans233,7402
-(defun map-spans-aux map-spans-aux237,7606
-(defsubst map-spans map-spans241,7721
-(defun find-span-aux find-span-aux244,7779
-(defun find-span find-span249,7905
-(defun span-at-before span-at-before252,7970
-(defun prev-span prev-span265,8412
-(defun next-span next-span274,8694
-(defsubst span-live-p span-live-p299,9678
-(defun span-raise span-raise305,9844
-(defalias 'span-object span-object311,10075
-(defun span-string span-string313,10116
-(defun set-span-properties set-span-properties319,10298
-(defun span-find-span span-find-span331,10553
-(defsubst span-at-event span-at-event342,10912
-(defun make-detached-span make-detached-span347,11036
-(defun fold-spans-aux fold-spans-aux353,11170
-(defun fold-spans fold-spans361,11426
-(defsubst span-buffer span-buffer368,11634
-(defsubst span-detached-p span-detached-p373,11726
-(defsubst set-span-face set-span-face381,11922
-(defsubst set-span-keymap set-span-keymap386,12022
-
-lib/texi-docstring-magic.el,958
-(defun texi-docstring-magic-find-face texi-docstring-magic-find-face85,2996
-(defun texi-docstring-magic-splice-sep texi-docstring-magic-splice-sep90,3161
-(defconst texi-docstring-magic-munge-tabletexi-docstring-magic-munge-table100,3466
-(defun texi-docstring-magic-untabify texi-docstring-magic-untabify190,7186
-(defun texi-docstring-magic-munge-docstring texi-docstring-magic-munge-docstring200,7501
-(defun texi-docstring-magic-texi texi-docstring-magic-texi239,8788
-(defun texi-docstring-magic-format-default texi-docstring-magic-format-default252,9228
-(defun texi-docstring-magic-texi-for texi-docstring-magic-texi-for268,9863
-(defconst texi-docstring-magic-commenttexi-docstring-magic-comment326,11823
-(defun texi-docstring-magic texi-docstring-magic332,11977
-(defun texi-docstring-magic-face-at-point texi-docstring-magic-face-at-point366,13057
-(defun texi-docstring-magic-insert-magic texi-docstring-magic-insert-magic381,13580
-
-lib/url-parse.el,921
-(defmacro url-type url-type28,1226
-(defmacro url-user url-user31,1282
-(defmacro url-password url-password34,1338
-(defmacro url-host url-host37,1398
-(defmacro url-port url-port40,1454
-(defmacro url-filename url-filename45,1613
-(defmacro url-target url-target48,1673
-(defmacro url-attributes url-attributes51,1731
-(defmacro url-fullness url-fullness54,1793
-(defmacro url-set-type url-set-type57,1853
-(defmacro url-set-user url-set-user60,1927
-(defmacro url-set-password url-set-password63,2001
-(defmacro url-set-host url-set-host66,2079
-(defmacro url-set-port url-set-port69,2153
-(defmacro url-set-filename url-set-filename72,2227
-(defmacro url-set-target url-set-target75,2305
-(defmacro url-set-attributes url-set-attributes78,2381
-(defmacro url-set-full url-set-full81,2461
-(defun url-recreate-url url-recreate-url84,2535
-(defun url-generic-parse-url url-generic-parse-url109,3289
-
-lib/xml.el,790
-(defsubst xml-node-name xml-node-name82,2907
-(defsubst xml-node-attributes xml-node-attributes87,3026
-(defsubst xml-node-children xml-node-children92,3144
-(defun xml-get-children xml-get-children97,3280
-(defun xml-get-attribute xml-get-attribute107,3603
-(defun xml-parse-file xml-parse-file123,4067
-(defun xml-parse-region xml-parse-region144,4651
-(defun xml-parse-tag xml-parse-tag179,5696
-(defun xml-parse-attlist xml-parse-attlist284,9165
-(defun xml-skip-dtd xml-skip-dtd321,10555
-(defun xml-parse-dtd xml-parse-dtd338,11191
-(defun xml-parse-elem-type xml-parse-elem-type408,13269
-(defun xml-substitute-special xml-substitute-special449,14424
-(defun xml-debug-print xml-debug-print470,15231
-(defun xml-debug-print-internal xml-debug-print-internal474,15323
-
-mmm/mmm-auto.el,499
-(defvar mmm-autoloaded-classesmmm-autoloaded-classes67,2675
-(defun mmm-autoload-class mmm-autoload-class85,3320
-(defvar mmm-changed-buffers-list mmm-changed-buffers-list125,4887
-(defun mmm-major-mode-change mmm-major-mode-change128,4994
-(defun mmm-check-changed-buffers mmm-check-changed-buffers141,5515
-(defun mmm-mode-on-maybe mmm-mode-on-maybe151,5888
-(defalias 'mmm-add-find-file-hooks mmm-add-find-file-hooks163,6306
-(defun mmm-add-find-file-hook mmm-add-find-file-hook164,6366
-
-mmm/mmm-class.el,626
-(defun mmm-get-class-spec mmm-get-class-spec41,1254
-(defun mmm-get-class-parameter mmm-get-class-parameter58,1967
-(defun mmm-set-class-parameter mmm-set-class-parameter62,2133
-(defun* mmm-apply-classmmm-apply-class74,2497
-(defun* mmm-apply-classesmmm-apply-classes86,3010
-(defun* mmm-apply-all mmm-apply-all106,3776
-(defun* mmm-ifymmm-ify118,4203
-(defun* mmm-match-regionmmm-match-region184,6890
-(defun mmm-match->point mmm-match->point228,8982
-(defun mmm-match-and-verify mmm-match-and-verify241,9525
-(defun mmm-get-form mmm-get-form267,10583
-(defun mmm-default-get-form mmm-default-get-form278,11079
-
-mmm/mmm-cmds.el,1027
-(defun mmm-ify-by-class mmm-ify-by-class40,1179
-(defun mmm-ify-region mmm-ify-region68,2165
-(defun mmm-ify-by-regexpmmm-ify-by-regexp80,2593
-(defun mmm-parse-buffer mmm-parse-buffer100,3244
-(defun mmm-parse-region mmm-parse-region109,3580
-(defun mmm-parse-block mmm-parse-block118,3959
-(defun mmm-get-block mmm-get-block135,4710
-(defun mmm-clear-current-region mmm-clear-current-region151,5095
-(defun mmm-clear-regions mmm-clear-regions156,5259
-(defun mmm-clear-all-regions mmm-clear-all-regions161,5405
-(defun mmm-reparse-current-region mmm-reparse-current-region169,5569
-(defun* mmm-end-current-region mmm-end-current-region188,6185
-(defun mmm-insert-region mmm-insert-region226,7768
-(defun mmm-insert-by-key mmm-insert-by-key245,8630
-(defun mmm-get-insertion-spec mmm-get-insertion-spec291,10888
-(defun mmm-insertion-help mmm-insertion-help318,11967
-(defun mmm-display-insertion-key mmm-display-insertion-key328,12337
-(defun mmm-get-all-insertion-keys mmm-get-all-insertion-keys350,13159
-
-mmm/mmm-compat.el,634
-(defvar mmm-xemacs mmm-xemacs40,1291
-(defvar mmm-keywords-usedmmm-keywords-used49,1594
-(defmacro mmm-regexp-opt mmm-regexp-opt90,2591
-(defvar mmm-evaporate-propertymmm-evaporate-property109,3240
-(defmacro mmm-set-keymap-default mmm-set-keymap-default127,4006
-(defmacro mmm-event-key mmm-event-key136,4448
-(defvar skeleton-positions skeleton-positions145,4667
-(defun mmm-fixup-skeleton mmm-fixup-skeleton146,4698
-(defmacro mmm-make-temp-buffer mmm-make-temp-buffer158,5135
-(defvar mmm-font-lock-available-p mmm-font-lock-available-p171,5531
-(defmacro mmm-set-font-lock-defaults mmm-set-font-lock-defaults178,5745
-
-mmm/mmm-mason.el,592
-(defvar mmm-mason-perl-tagsmmm-mason-perl-tags41,1225
-(defvar mmm-mason-pseudo-perl-tagsmmm-mason-pseudo-perl-tags45,1366
-(defvar mmm-mason-non-perl-tagsmmm-mason-non-perl-tags48,1442
-(defvar mmm-mason-perl-tags-regexpmmm-mason-perl-tags-regexp51,1543
-(defvar mmm-mason-pseudo-perl-tags-regexpmmm-mason-pseudo-perl-tags-regexp56,1738
-(defvar mmm-mason-tag-names-regexpmmm-mason-tag-names-regexp61,1955
-(defun mmm-mason-verify-inline mmm-mason-verify-inline66,2175
-(defun mmm-mason-start-line mmm-mason-start-line154,5041
-(defun mmm-mason-end-line mmm-mason-end-line159,5106
-
-mmm/mmm-mode.el,1496
-(defun mmm-mode mmm-mode106,4116
-(defun mmm-mode-on mmm-mode-on312,13247
-(defun mmm-mode-off mmm-mode-off352,14969
-(defvar mmm-mode-map mmm-mode-map375,15634
-(defvar mmm-mode-prefix-map mmm-mode-prefix-map378,15709
-(defvar mmm-mode-menu-map mmm-mode-menu-map381,15819
-(defun mmm-define-key mmm-define-key384,15910
-(define-key mmm-mode-prefix-map mmm-mode-prefix-map406,16585
-(define-key mmm-mode-prefix-map mmm-mode-prefix-map413,16843
-(define-key mmm-mode-map mmm-mode-map416,16954
-(define-key mmm-mode-menu-map mmm-mode-menu-map419,17056
-(define-key mmm-mode-menu-map mmm-mode-menu-map421,17128
-(define-key mmm-mode-menu-map mmm-mode-menu-map423,17187
-(define-key mmm-mode-menu-map mmm-mode-menu-map425,17268
-(define-key mmm-mode-menu-map mmm-mode-menu-map427,17349
-(define-key mmm-mode-menu-map mmm-mode-menu-map429,17436
-(define-key mmm-mode-menu-map mmm-mode-menu-map432,17530
-(define-key mmm-mode-menu-map mmm-mode-menu-map434,17590
-(define-key mmm-mode-menu-map mmm-mode-menu-map437,17681
-(define-key mmm-mode-menu-map mmm-mode-menu-map439,17741
-(define-key mmm-mode-menu-map mmm-mode-menu-map441,17848
-(define-key mmm-mode-menu-map mmm-mode-menu-map443,17933
-(define-key mmm-mode-menu-map mmm-mode-menu-map446,18019
-(define-key mmm-mode-menu-map mmm-mode-menu-map448,18079
-(define-key mmm-mode-menu-map mmm-mode-menu-map450,18192
-(define-key mmm-mode-menu-map mmm-mode-menu-map452,18277
-(define-key mmm-mode-map mmm-mode-map455,18360
-
-mmm/mmm-region.el,2300
-(defun mmm-overlay-at mmm-overlay-at51,1642
-(defun mmm-overlays-at mmm-overlays-at56,1843
-(defun mmm-included-p mmm-included-p69,2525
-(defun mmm-overlays-in mmm-overlays-in82,2903
-(defun mmm-sort-overlays mmm-sort-overlays100,3840
-(defvar mmm-current-overlay mmm-current-overlay109,4110
-(defvar mmm-previous-overlay mmm-previous-overlay114,4325
-(defvar mmm-current-submode mmm-current-submode119,4513
-(defvar mmm-previous-submode mmm-previous-submode124,4713
-(defun mmm-update-current-submode mmm-update-current-submode129,4886
-(defun mmm-set-current-submode mmm-set-current-submode141,5364
-(defun mmm-submode-at mmm-submode-at152,5856
-(defun mmm-match-front mmm-match-front161,6139
-(defun mmm-match-back mmm-match-back177,6780
-(defun mmm-front-start mmm-front-start195,7402
-(defun mmm-back-end mmm-back-end203,7672
-(defun mmm-make-marker mmm-make-marker216,7969
-(defun* mmm-make-regionmmm-make-region228,8428
-(defun mmm-get-face mmm-get-face286,11150
-(defun mmm-clear-overlays mmm-clear-overlays300,11459
-(defun mmm-update-mode-info mmm-update-mode-info314,11871
-(defun mmm-update-submode-region mmm-update-submode-region397,16038
-(defun mmm-add-hooks mmm-add-hooks417,16958
-(defun mmm-remove-hooks mmm-remove-hooks421,17093
-(defun mmm-get-local-variables-list mmm-get-local-variables-list427,17220
-(defun mmm-get-locals mmm-get-locals447,18140
-(defun mmm-get-saved-local mmm-get-saved-local460,18721
-(defun mmm-set-local-variables mmm-set-local-variables464,18886
-(defun mmm-get-saved-local-variables mmm-get-saved-local-variables475,19327
-(defun mmm-save-changed-local-variables mmm-save-changed-local-variables483,19644
-(defun mmm-clear-local-variables mmm-clear-local-variables502,20502
-(defun mmm-enable-font-lock mmm-enable-font-lock513,20781
-(defun mmm-update-font-lock-buffer mmm-update-font-lock-buffer521,21041
-(defun mmm-refontify-maybe mmm-refontify-maybe534,21564
-(defun mmm-submode-changes-in mmm-submode-changes-in545,21921
-(defun mmm-regions-in mmm-regions-in558,22406
-(defun mmm-regions-alist mmm-regions-alist572,22954
-(defun mmm-fontify-region mmm-fontify-region589,23600
-(defun mmm-fontify-region-list mmm-fontify-region-list607,24494
-(defun mmm-beginning-of-syntax mmm-beginning-of-syntax629,25412
-
-mmm/mmm-rpm.el,242
-(defconst mmm-rpm-sh-start-tagsmmm-rpm-sh-start-tags48,1617
-(defvar mmm-rpm-sh-end-tagsmmm-rpm-sh-end-tags53,1841
-(defvar mmm-rpm-sh-start-regexpmmm-rpm-sh-start-regexp57,2015
-(defvar mmm-rpm-sh-end-regexpmmm-rpm-sh-end-regexp61,2193
-
-mmm/mmm-sample.el,269
-(defvar mmm-here-doc-mode-alist mmm-here-doc-mode-alist81,2448
-(defun mmm-here-doc-get-mode mmm-here-doc-get-mode90,2933
-(defun mmm-file-variables-verify mmm-file-variables-verify196,6459
-(defun mmm-file-variables-find-back mmm-file-variables-find-back220,7495
-
-mmm/mmm-univ.el,52
-(defun mmm-univ-get-mode mmm-univ-get-mode38,1205
-
-mmm/mmm-utils.el,371
-(defmacro mmm-valid-buffer mmm-valid-buffer41,1299
-(defmacro mmm-save-all mmm-save-all60,1943
-(defun mmm-format-string mmm-format-string73,2232
-(defun mmm-format-matches mmm-format-matches84,2684
-(defmacro mmm-save-keyword mmm-save-keyword105,3362
-(defmacro mmm-save-keywords mmm-save-keywords113,3690
-(defun mmm-looking-back-at mmm-looking-back-at126,4224
-
-mmm/mmm-vars.el,3586
-(defgroup mmm mmm86,2527
-(defvar mmm-c-derived-modesmmm-c-derived-modes93,2637
-(defvar mmm-save-local-variables mmm-save-local-variables96,2743
-(defvar mmm-buffer-saved-locals mmm-buffer-saved-locals176,6248
-(defvar mmm-region-saved-locals-defaults mmm-region-saved-locals-defaults181,6448
-(defvar mmm-region-saved-locals-for-dominant mmm-region-saved-locals-for-dominant187,6708
-(defgroup mmm-faces mmm-faces197,7085
-(defcustom mmm-submode-decoration-level mmm-submode-decoration-level203,7256
-(defface mmm-init-submode-face mmm-init-submode-face217,7966
-(defface mmm-cleanup-submode-face mmm-cleanup-submode-face221,8106
-(defface mmm-declaration-submode-face mmm-declaration-submode-face225,8243
-(defface mmm-comment-submode-face mmm-comment-submode-face229,8389
-(defface mmm-output-submode-face mmm-output-submode-face233,8542
-(defface mmm-special-submode-face mmm-special-submode-face237,8691
-(defface mmm-code-submode-face mmm-code-submode-face241,8855
-(defface mmm-default-submode-face mmm-default-submode-face245,8994
-(defcustom mmm-mode-string mmm-mode-string253,9232
-(defcustom mmm-submode-mode-line-format mmm-submode-mode-line-format258,9363
-(defvar mmm-classes mmm-classes268,9635
-(defvar mmm-global-classes mmm-global-classes274,9880
-(defcustom mmm-mode-ext-classes-alist mmm-mode-ext-classes-alist281,10062
-(defun mmm-add-mode-ext-class mmm-add-mode-ext-class300,10880
-(defcustom mmm-major-mode-preferencesmmm-major-mode-preferences309,11205
-(defun mmm-add-to-major-mode-preferences mmm-add-to-major-mode-preferences327,12003
-(defun mmm-ensure-modename mmm-ensure-modename343,12789
-(defun mmm-modename->function mmm-modename->function352,13099
-(defcustom mmm-mode-prefix-key mmm-mode-prefix-key366,13557
-(defcustom mmm-command-modifiers mmm-command-modifiers371,13684
-(defcustom mmm-insert-modifiers mmm-insert-modifiers385,14317
-(defcustom mmm-use-old-command-keys mmm-use-old-command-keys400,14995
-(defun mmm-use-old-command-keys mmm-use-old-command-keys410,15459
-(defcustom mmm-mode-hook mmm-mode-hook418,15658
-(defun mmm-run-constructed-hook mmm-run-constructed-hook438,16468
-(defun mmm-run-major-hook mmm-run-major-hook446,16854
-(defun mmm-run-submode-hook mmm-run-submode-hook449,16931
-(defvar mmm-class-hooks-run mmm-class-hooks-run452,17018
-(defun mmm-run-class-hook mmm-run-class-hook457,17190
-(defcustom mmm-major-mode-hook mmm-major-mode-hook465,17391
-(defun mmm-run-major-mode-hook mmm-run-major-mode-hook479,18022
-(defcustom mmm-global-mode mmm-global-mode486,18160
-(defcustom mmm-never-modesmmm-never-modes503,18748
-(defvar mmm-set-file-name-for-modes mmm-set-file-name-for-modes521,19048
-(defvar mmm-mode mmm-mode532,19369
-(defvar mmm-primary-mode mmm-primary-mode540,19577
-(defvar mmm-classes-alist mmm-classes-alist548,19795
-(defun mmm-add-classes mmm-add-classes668,26175
-(defun mmm-add-group mmm-add-group673,26340
-(defconst mmm-version mmm-version686,26804
-(defun mmm-version mmm-version689,26869
-(defvar mmm-temp-buffer-name mmm-temp-buffer-name696,27012
-(defvar mmm-interactive-history mmm-interactive-history702,27142
-(defun mmm-add-to-history mmm-add-to-history708,27411
-(defun mmm-clear-history mmm-clear-history711,27494
-(defvar mmm-mode-ext-classes mmm-mode-ext-classes719,27679
-(defun mmm-get-mode-ext-classes mmm-get-mode-ext-classes724,27890
-(defun mmm-clear-mode-ext-classes mmm-clear-mode-ext-classes733,28266
-(defun mmm-mode-ext-applies mmm-mode-ext-applies737,28391
-(defun mmm-get-all-classes mmm-get-all-classes751,28875
-
-phox/phox.el,1008
-(defcustom phox-prog-name phox-prog-name30,907
-(defcustom phox-sym-lock phox-sym-lock35,1009
-(defcustom phox-x-symbol-enable phox-x-symbol-enable40,1133
-(defcustom phox-web-pagephox-web-page45,1238
-(defcustom phox-doc-dir phox-doc-dir51,1388
-(defcustom phox-lib-dir phox-lib-dir57,1536
-(defcustom phox-tags-program phox-tags-program63,1680
-(defcustom phox-tags-doc phox-tags-doc69,1860
-(defcustom phox-etags phox-etags75,1998
-(defpgdefault menu-entriesmenu-entries95,2428
-(defun phox-config phox-config112,2757
-(defun phox-shell-config phox-shell-config154,4681
-(define-derived-mode phox-mode phox-mode194,6261
-(define-derived-mode phox-shell-mode phox-shell-mode209,6705
-(define-derived-mode phox-response-mode phox-response-mode214,6833
-(define-derived-mode phox-goals-mode phox-goals-mode226,7252
-(defun phox-pre-shell-start phox-pre-shell-start252,8311
-(defpgdefault completion-tablecompletion-table266,8825
-(defpgdefault x-symbol-language x-symbol-language286,9405
+phox/phox.el,898
+(defcustom phox-prog-name phox-prog-name31,931
+(defcustom phox-web-pagephox-web-page44,1329
+(defcustom phox-doc-dir phox-doc-dir50,1479
+(defcustom phox-lib-dir phox-lib-dir56,1627
+(defcustom phox-tags-program phox-tags-program62,1771
+(defcustom phox-tags-doc phox-tags-doc68,1951
+(defcustom phox-etags phox-etags74,2089
+(defpgdefault menu-entriesmenu-entries95,2541
+(defun phox-config phox-config109,2734
+(defun phox-shell-config phox-shell-config151,4658
+(define-derived-mode phox-mode phox-mode176,5584
+(define-derived-mode phox-shell-mode phox-shell-mode190,6002
+(define-derived-mode phox-response-mode phox-response-mode195,6130
+(define-derived-mode phox-goals-mode phox-goals-mode202,6377
+(defun phox-pre-shell-start phox-pre-shell-start224,7278
+(defpgdefault completion-tablecompletion-table238,7792
+(defpgdefault x-symbol-language x-symbol-language246,7897
 
 phox/phox-extraction.el,603
 (defvar phox-prog-orig phox-prog-orig11,480
@@ -2175,10 +1809,8 @@ phox/phox-extraction.el,603
 (defun phox-output-theorem phox-output-theorem105,3160
 (defun phox-output-theorem-on-cursor(phox-output-theorem-on-cursor112,3460
 
-phox/phox-font.el,196
+phox/phox-font.el,64
 (defconst phox-font-lock-keywordsphox-font-lock-keywords6,282
-(defconst phox-sym-lock-keywords-tablephox-sym-lock-keywords-table66,2407
-(defun phox-sym-lock-start phox-sym-lock-start89,2988
 
 phox/phox-fun.el,1049
 (defun phox-init-syntax-table phox-init-syntax-table67,2392
@@ -2200,42 +1832,21 @@ phox/phox-fun.el,1049
 (defun phox-delete-symbol(phox-delete-symbol414,11484
 (defun phox-delete-symbol-on-cursor(phox-delete-symbol-on-cursor420,11693
 
+phox/phox-lang.el,0
+
 phox/phox-outline.el,108
 (defun phox-outline-level(phox-outline-level32,1113
 (defun phox-setup-outline phox-setup-outline46,1587
 
-phox/phox-sym-lock.el,2167
-(defvar phox-sym-lock-sym-count phox-sym-lock-sym-count34,1669
-(defvar phox-sym-lock-ext-start phox-sym-lock-ext-start37,1739
-(defvar phox-sym-lock-ext-end phox-sym-lock-ext-end39,1861
-(defvar phox-sym-lock-font-size phox-sym-lock-font-size42,1980
-(defvar phox-sym-lock-keywords phox-sym-lock-keywords47,2170
-(defvar phox-sym-lock-enabled phox-sym-lock-enabled52,2346
-(defvar phox-sym-lock-color phox-sym-lock-color57,2508
-(defvar phox-sym-lock-mouse-face phox-sym-lock-mouse-face62,2726
-(defvar phox-sym-lock-mouse-face-enabled phox-sym-lock-mouse-face-enabled67,2916
-(defconst phox-sym-lock-with-mule phox-sym-lock-with-mule72,3106
-(defun phox-sym-lock-gen-symbol phox-sym-lock-gen-symbol75,3190
-(defun phox-sym-lock-make-symbols-atomic phox-sym-lock-make-symbols-atomic83,3493
-(defun phox-sym-lock-compute-font-size phox-sym-lock-compute-font-size110,4435
-(defvar phox-sym-lock-font-namephox-sym-lock-font-name147,5781
-(defun phox-sym-lock-set-foreground phox-sym-lock-set-foreground185,7066
-(defun phox-sym-lock-translate-char phox-sym-lock-translate-char199,7675
-(defun phox-sym-lock-translate-char-or-string phox-sym-lock-translate-char-or-string207,7943
-(defun phox-sym-lock-remap-face phox-sym-lock-remap-face214,8170
-(defvar phox-sym-lock-clear-facephox-sym-lock-clear-face234,9160
-(defun phox-sym-lock phox-sym-lock246,9582
-(defun phox-sym-lock-rec phox-sym-lock-rec255,9986
-(defun phox-sym-lock-atom-face phox-sym-lock-atom-face261,10139
-(defun phox-sym-lock-pre-idle-hook-first phox-sym-lock-pre-idle-hook-first266,10435
-(defun phox-sym-lock-pre-idle-hook-last phox-sym-lock-pre-idle-hook-last274,10793
-(defun phox-sym-lock-enable phox-sym-lock-enable283,11168
-(defun phox-sym-lock-disable phox-sym-lock-disable296,11581
-(defun phox-sym-lock-mouse-face-enable phox-sym-lock-mouse-face-enable309,11999
-(defun phox-sym-lock-mouse-face-disable phox-sym-lock-mouse-face-disable316,12214
-(defun phox-sym-lock-font-lock-hook phox-sym-lock-font-lock-hook323,12433
-(defun font-lock-set-defaults font-lock-set-defaults338,13126
-(defun phox-sym-lock-patch-keywords phox-sym-lock-patch-keywords349,13504
+phox/phox-pbrpm.el,551
+(defun phox-pbrpm-left-paren-p phox-pbrpm-left-paren-p25,1169
+(defun phox-pbrpm-right-paren-p phox-pbrpm-right-paren-p32,1372
+(defun phox-pbrpm-menu-from-string phox-pbrpm-menu-from-string40,1576
+(defun phox-pbrpm-rename-in-cmd phox-pbrpm-rename-in-cmd49,1910
+(defun phox-pbrpm-generate-menu phox-pbrpm-generate-menu82,3166
+(defalias 'proof-pbrpm-generate-menu proof-pbrpm-generate-menu250,8785
+(defalias 'proof-pbrpm-left-paren-p proof-pbrpm-left-paren-p251,8849
+(defalias 'proof-pbrpm-right-paren-p proof-pbrpm-right-paren-p252,8911
 
 phox/phox-tags.el,483
 (defun phox-tags-add-table(phox-tags-add-table21,766
@@ -2247,43 +1858,41 @@ phox/phox-tags.el,483
 (defun phox-complete-tag(phox-complete-tag77,2349
 (defvar phox-tags-menuphox-tags-menu96,2904
 
-phox/x-symbol-phox.el,2739
+phox/x-symbol-phox.el,2614
 (defvar x-symbol-phox-required-fonts x-symbol-phox-required-fonts14,449
-(defvar x-symbol-phox-name x-symbol-phox-name24,946
-(defvar x-symbol-phox-modeline-name x-symbol-phox-modeline-name25,988
-(defcustom x-symbol-phox-header-groups-alist x-symbol-phox-header-groups-alist27,1033
-(defcustom x-symbol-phox-electric-ignore x-symbol-phox-electric-ignore34,1253
-(defvar x-symbol-phox-required-fonts x-symbol-phox-required-fonts41,1501
-(defvar x-symbol-phox-extra-menu-items x-symbol-phox-extra-menu-items44,1602
-(defvar x-symbol-phox-token-grammarx-symbol-phox-token-grammar47,1691
-(defvar x-symbol-phox-input-token-grammarx-symbol-phox-input-token-grammar59,2220
-(defun x-symbol-phox-default-token-list x-symbol-phox-default-token-list65,2475
-(defvar x-symbol-phox-user-table x-symbol-phox-user-table77,2764
-(defvar x-symbol-phox-generated-data x-symbol-phox-generated-data80,2873
-(defvar x-symbol-phox-master-directory x-symbol-phox-master-directory88,3112
-(defvar x-symbol-phox-image-searchpath x-symbol-phox-image-searchpath89,3161
-(defvar x-symbol-phox-image-cached-dirs x-symbol-phox-image-cached-dirs90,3209
-(defvar x-symbol-phox-image-file-truename-alist x-symbol-phox-image-file-truename-alist91,3275
-(defvar x-symbol-phox-image-keywords x-symbol-phox-image-keywords92,3328
-(defcustom x-symbol-phox-class-alistx-symbol-phox-class-alist99,3549
-(defcustom x-symbol-phox-class-face-alist x-symbol-phox-class-face-alist110,3931
-(defvar x-symbol-phox-font-lock-keywords x-symbol-phox-font-lock-keywords120,4244
-(defvar x-symbol-phox-font-lock-allowed-faces x-symbol-phox-font-lock-allowed-faces122,4291
-(defvar x-symbol-phox-case-insensitive x-symbol-phox-case-insensitive128,4516
-(defvar x-symbol-phox-token-shape x-symbol-phox-token-shape129,4560
-(defvar x-symbol-phox-input-token-ignore x-symbol-phox-input-token-ignore130,4599
-(defvar x-symbol-phox-token-list x-symbol-phox-token-list137,4838
-(defvar x-symbol-phox-xsymb0-table x-symbol-phox-xsymb0-table139,4883
-(defun x-symbol-phox-prepare-table x-symbol-phox-prepare-table160,5342
-(defvar x-symbol-phox-tablex-symbol-phox-table167,5513
-(defcustom x-symbol-phox-auto-stylex-symbol-phox-auto-style178,5831
-(defvar x-symbol-phox-menu-alist x-symbol-phox-menu-alist204,6781
-(defvar x-symbol-phox-grid-alist x-symbol-phox-grid-alist206,6871
-(defvar x-symbol-phox-decode-atree x-symbol-phox-decode-atree209,6962
-(defvar x-symbol-phox-decode-alist x-symbol-phox-decode-alist211,7055
-(defvar x-symbol-phox-encode-alist x-symbol-phox-encode-alist213,7152
-(defvar x-symbol-phox-nomule-decode-exec x-symbol-phox-nomule-decode-exec217,7309
-(defvar x-symbol-phox-nomule-encode-exec x-symbol-phox-nomule-encode-exec219,7409
+(defcustom x-symbol-phox-header-groups-alist x-symbol-phox-header-groups-alist29,1056
+(defcustom x-symbol-phox-electric-ignore x-symbol-phox-electric-ignore36,1276
+(defvar x-symbol-phox-required-fonts x-symbol-phox-required-fonts43,1492
+(defvar x-symbol-phox-extra-menu-items x-symbol-phox-extra-menu-items46,1593
+(defvar x-symbol-phox-token-grammarx-symbol-phox-token-grammar49,1682
+(defvar x-symbol-phox-input-token-grammarx-symbol-phox-input-token-grammar63,2473
+(defun x-symbol-phox-default-token-list x-symbol-phox-default-token-list69,2728
+(defvar x-symbol-phox-user-table x-symbol-phox-user-table81,3046
+(defvar x-symbol-phox-generated-data x-symbol-phox-generated-data84,3155
+(defvar x-symbol-phox-master-directory x-symbol-phox-master-directory92,3394
+(defvar x-symbol-phox-image-searchpath x-symbol-phox-image-searchpath93,3443
+(defvar x-symbol-phox-image-cached-dirs x-symbol-phox-image-cached-dirs94,3491
+(defvar x-symbol-phox-image-file-truename-alist x-symbol-phox-image-file-truename-alist95,3557
+(defvar x-symbol-phox-image-keywords x-symbol-phox-image-keywords96,3610
+(defcustom x-symbol-phox-class-alistx-symbol-phox-class-alist103,3831
+(defcustom x-symbol-phox-class-face-alist x-symbol-phox-class-face-alist114,4213
+(defvar x-symbol-phox-font-lock-keywords x-symbol-phox-font-lock-keywords124,4526
+(defvar x-symbol-phox-font-lock-allowed-faces x-symbol-phox-font-lock-allowed-faces126,4573
+(defvar x-symbol-phox-case-insensitive x-symbol-phox-case-insensitive132,4798
+(defvar x-symbol-phox-token-shape x-symbol-phox-token-shape133,4842
+(defvar x-symbol-phox-input-token-ignore x-symbol-phox-input-token-ignore134,4881
+(defvar x-symbol-phox-token-list x-symbol-phox-token-list141,5120
+(defvar x-symbol-phox-xsymb0-table x-symbol-phox-xsymb0-table143,5165
+(defun x-symbol-phox-prepare-table x-symbol-phox-prepare-table164,5624
+(defvar x-symbol-phox-tablex-symbol-phox-table172,5800
+(defcustom x-symbol-phox-auto-stylex-symbol-phox-auto-style183,6118
+(defvar x-symbol-phox-menu-alist x-symbol-phox-menu-alist209,7068
+(defvar x-symbol-phox-grid-alist x-symbol-phox-grid-alist211,7158
+(defvar x-symbol-phox-decode-atree x-symbol-phox-decode-atree214,7249
+(defvar x-symbol-phox-decode-alist x-symbol-phox-decode-alist216,7342
+(defvar x-symbol-phox-encode-alist x-symbol-phox-encode-alist218,7439
+(defvar x-symbol-phox-nomule-decode-exec x-symbol-phox-nomule-decode-exec222,7596
+(defvar x-symbol-phox-nomule-encode-exec x-symbol-phox-nomule-encode-exec224,7696
 
 plastic/plastic.el,4425
 (defcustom plastic-tags plastic-tags28,805
@@ -2595,188 +2204,601 @@ twelf/twelf-old.el,10513
 
 twelf/x-symbol-twelf.el,0
 
-todo,1297
-   function to to383,15505
-$Id: todo,2,21
-This is an outline file.   Use C-c C-n,4,67
-X 51,1404
-*** C Improved configurability of command settings,182,6886
-  We should let command settings,183,6943
-  We should let command settings, etc,183,6943
-  - XEmacs pg forces on font-lock,333,13092
-    Save foo;409,16628
-*** A Doc new bits: font lock keywords,479,19329
-*** A Doc new bits: font lock keywords, filename %e,479,19329
-  Added proof-{script,480,19386
-  Added proof-{script,shell,480,19386
-  Added proof-{script,shell,goals,480,19386
-  Presently used only in proof-easy-config,481,19446
-  - Mention configuring function menus,492,19782
-  - document mouse functions,494,19868
-  - document mouse functions, proof-cd,494,19868
-  - document mouse functions, proof-cd, process quit timeout,494,19868
-    X-Symbol,495,19931
-    X-Symbol, prog-name-guess,495,19931
-*** D Fix INFO-DIR-ENTRY in 509,20439
-*** C Fixing up errors caused by pbp-generated commands; currently,575,22916
-  should mean generates an error.  With LEGO pbp,578,23122
-  tactic which always succeeds,579,23186
-  decodes annotations eagerly. Lazily would be faster,587,23542
-  the tech report claims --- djs: probably not much faster,588,23611
-***  6. Update Emacs and prover versions in texi,677,26614
-
-doc/ProofGeneral.texi,5783
-@node TopTop166,5019
-@node PrefacePreface203,6126
-@node Latest news for 3.5Latest news for 3.5226,6714
-@node FutureFuture264,8372
-@node CreditsCredits299,9922
-@node Introducing Proof GeneralIntroducing Proof General397,13337
-@node Quick start guideQuick start guide452,15329
-@node Features of Proof GeneralFeatures of Proof General506,17898
-@node Supported proof assistantsSupported proof assistants595,21823
-@node Prerequisites for this manualPrerequisites for this manual647,23819
-@node Organization of this manualOrganization of this manual691,25445
-@node Basic Script ManagementBasic Script Management717,26272
-@node Walkthrough example in Isabelle/IsarWalkthrough example in Isabelle/Isar736,26877
-@node Proof scriptsProof scripts963,35412
-@node Script buffersScript buffers1006,37532
-@node Locked queue and editing regionsLocked queue and editing regions1028,38109
-@node Goal-save sequencesGoal-save sequences1084,40256
-@node Active scripting bufferActive scripting buffer1121,41742
-@node Summary of Proof General buffersSummary of Proof General buffers1190,45162
-@node Script editing commandsScript editing commands1252,47836
-@node Script processing commandsScript processing commands1330,50694
-@node Proof assistant commandsProof assistant commands1458,55995
-@node Toolbar commandsToolbar commands1604,60882
-@node Interrupting during trace outputInterrupting during trace output1628,61811
-@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing1667,63734
-@node Goals buffer commandsGoals buffer commands1681,64234
-@node Advanced Script ManagementAdvanced Script Management1770,67766
-@node Visibility of completed proofsVisibility of completed proofs1801,68920
-@node Switching between proof scriptsSwitching between proof scripts1856,70843
-@node View of processed files View of processed files 1893,72815
-@node Retracting across filesRetracting across files1953,75866
-@node Asserting across filesAsserting across files1966,76497
-@node Automatic multiple file handlingAutomatic multiple file handling1979,77063
-@node Escaping script managementEscaping script management2004,78097
-@node Experimental featuresExperimental features2062,80300
-@node Support for other PackagesSupport for other Packages2096,81562
-@node Syntax highlightingSyntax highlighting2128,82437
-@node X-Symbol supportX-Symbol support2167,84046
-@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)2226,86592
-@node Support for outline modeSupport for outline mode2285,88722
-@node Support for completionSupport for completion2311,89852
-@node Support for tagsSupport for tags2368,92017
-@node Customizing Proof GeneralCustomizing Proof General2420,94345
-@node Basic optionsBasic options2460,96015
-@node How to customizeHow to customize2484,96773
-@node Display customizationDisplay customization2535,98863
-@node User optionsUser options2660,104097
-@node Changing facesChanging faces2914,113103
-@node Tweaking configuration settingsTweaking configuration settings2989,115772
-@node Hints and TipsHints and Tips3046,118297
-@node Adding your own keybindingsAdding your own keybindings3065,118898
-@node Using file variablesUsing file variables3121,121431
-@node Using abbreviationsUsing abbreviations3174,123254
-@node LEGO Proof GeneralLEGO Proof General3213,124669
-@node LEGO specific commandsLEGO specific commands3254,126038
-@node LEGO tagsLEGO tags3274,126493
-@node LEGO customizationsLEGO customizations3284,126740
-@node Coq Proof GeneralCoq Proof General3316,127658
-@node Coq-specific commandsCoq-specific commands3332,128067
-@node Coq-specific variablesCoq-specific variables3354,128574
-@node Editing multiple proofsEditing multiple proofs3392,129789
-@node User-loaded tacticsUser-loaded tactics3416,130897
-@node Holes featureHoles feature3481,133424
-@node Isabelle Proof GeneralIsabelle Proof General3508,134710
-@node Classic IsabelleClassic Isabelle3577,138033
-@node ML filesML files3593,138471
-@node Theory filesTheory files3664,140896
-@node General commands for IsabelleGeneral commands for Isabelle3718,143367
-@node Specific commands for IsabelleSpecific commands for Isabelle3730,143849
-@node Isabelle customizationsIsabelle customizations3759,144789
-@node Isabelle/IsarIsabelle/Isar3824,146887
-@node General commands for Isabelle/IsarGeneral commands for Isabelle/Isar3845,147650
-@node Specific commands for Isabelle/IsarSpecific commands for Isabelle/Isar3852,147904
-@node Logics and SettingsLogics and Settings3939,150432
-@node HOL Proof GeneralHOL Proof General3980,152120
-@node Shell Proof GeneralShell Proof General4021,153904
-@node Obtaining and InstallingObtaining and Installing4057,155362
-@node Obtaining Proof GeneralObtaining Proof General4073,155775
-@node Installing Proof General from tarballInstalling Proof General from tarball4104,157014
-@node Installing Proof General from RPM packageInstalling Proof General from RPM package4129,157846
-@node Setting the names of binariesSetting the names of binaries4144,158254
-@node Notes for syssiesNotes for syssies4172,159182
-@node Known BugsKnown Bugs4245,162115
-@node ReferencesReferences4258,162516
-@node History of Proof GeneralHistory of Proof General4298,163540
-@node Old News for 3.0Old News for 3.04389,167642
-@node Old News for 3.1Old News for 3.14459,171336
-@node Old News for 3.2Old News for 3.24485,172508
-@node Old News for 3.3Old News for 3.34546,175511
-@node Old News for 3.4Old News for 3.44565,176408
-@node Function IndexFunction Index4588,177464
-@node Variable IndexVariable Index4592,177540
-@node Keystroke IndexKeystroke Index4596,177620
-@node Concept IndexConcept Index4600,177686
+lib/holes.el,3711
+(defvar holes-doc holes-doc35,993
+(defvar holes-default-hole holes-default-hole143,4976
+(defvar holes-active-hole holes-active-hole147,5145
+(defcustom holes-empty-hole-string holes-empty-hole-string154,5354
+(defcustom holes-empty-hole-regexp holes-empty-hole-regexp157,5465
+(defcustom holes-search-limit holes-search-limit164,5756
+(defface active-hole-faceactive-hole-face176,6132
+(defface inactive-hole-faceinactive-hole-face188,6580
+(defun holes-region-beginning-or-nil holes-region-beginning-or-nil203,7056
+(defun holes-region-end-or-nil holes-region-end-or-nil208,7166
+(defun holes-copy-active-region holes-copy-active-region213,7264
+(defun holes-is-hole-p holes-is-hole-p220,7463
+(defun holes-hole-start-position holes-hole-start-position226,7570
+(defun holes-hole-end-position holes-hole-end-position233,7759
+(defun holes-hole-buffer holes-hole-buffer240,7943
+(defun holes-hole-at holes-hole-at247,8118
+(defun holes-active-hole-exist-p holes-active-hole-exist-p254,8293
+(defun holes-active-hole-start-position holes-active-hole-start-position264,8551
+(defun holes-active-hole-end-position holes-active-hole-end-position274,8923
+(defun holes-active-hole-buffer holes-active-hole-buffer285,9292
+(defun holes-goto-active-hole holes-goto-active-hole296,9598
+(defun holes-highlight-hole-as-active holes-highlight-hole-as-active308,9866
+(defun holes-highlight-hole holes-highlight-hole318,10178
+(defun holes-disable-active-hole holes-disable-active-hole329,10470
+(defun holes-set-active-hole holes-set-active-hole347,11013
+(defun holes-is-in-hole-p holes-is-in-hole-p360,11359
+(defun holes-make-hole holes-make-hole367,11502
+(defun holes-make-hole-at holes-make-hole-at393,12248
+(defun holes-clear-hole holes-clear-hole413,12724
+(defun holes-clear-hole-at holes-clear-hole-at425,13013
+(defun holes-map-holes holes-map-holes434,13272
+(defun holes-mapcar-holes holes-mapcar-holes442,13455
+(defun holes-clear-all-buffer-holes holes-clear-all-buffer-holes448,13622
+(defun holes-next holes-next459,13922
+(defun holes-next-after-active-hole holes-next-after-active-hole466,14173
+(defun holes-set-active-hole-next holes-set-active-hole-next474,14392
+(defun holes-replace-segment holes-replace-segment496,14945
+(defun holes-replace holes-replace506,15299
+(defun holes-replace-active-hole holes-replace-active-hole537,16494
+(defun holes-replace-update-active-hole holes-replace-update-active-hole546,16795
+(defun holes-delete-update-active-hole holes-delete-update-active-hole567,17485
+(defun holes-set-make-active-hole holes-set-make-active-hole574,17699
+(defun holes-mouse-replace-active-hole holes-mouse-replace-active-hole609,18825
+(defun holes-destroy-hole holes-destroy-hole629,19364
+(defun holes-hole-at-event holes-hole-at-event646,19775
+(defun holes-mouse-destroy-hole holes-mouse-destroy-hole651,19888
+(defun holes-mouse-forget-hole holes-mouse-forget-hole661,20128
+(defun holes-mouse-set-make-active-hole holes-mouse-set-make-active-hole677,20438
+(defun holes-mouse-set-active-hole holes-mouse-set-active-hole699,20999
+(defun holes-set-point-next-hole-destroy holes-set-point-next-hole-destroy711,21263
+(defvar hole-maphole-map727,21713
+(defvar holes-mode-mapholes-mode-map743,22333
+(defun holes-replace-string-by-holes-backward holes-replace-string-by-holes-backward780,23798
+(defun holes-skeleton-end-hook holes-skeleton-end-hook798,24499
+(defconst holes-jump-doc holes-jump-doc806,24863
+(defun holes-abbrev-complete holes-abbrev-complete811,25068
+(defun holes-insert-and-expand holes-insert-and-expand829,25764
+(defvar holes-mode holes-mode839,26183
+(defun holes-mode holes-mode845,26379
+
+lib/holes-load.el,0
+
+lib/proof-compat.el,1194
+(defvar proof-running-on-XEmacs proof-running-on-XEmacs24,760
+(defvar proof-running-on-Emacs21 proof-running-on-Emacs2126,882
+(defvar proof-running-on-win32 proof-running-on-win3230,1129
+(defun pg-custom-undeclare-variable pg-custom-undeclare-variable41,1562
+(defun subst-char-in-string subst-char-in-string112,3702
+(defun replace-regexp-in-string replace-regexp-in-string126,4256
+(defconst menuvisiblep menuvisiblep188,6969
+(defun set-window-text-height set-window-text-height205,7588
+(defmacro save-selected-frame save-selected-frame231,8538
+(defun warn warn270,9840
+(defun redraw-modeline redraw-modeline277,10095
+(defun replace-in-string replace-in-string292,10662
+(defun proof-buffer-syntactic-context-emulate proof-buffer-syntactic-context-emulate341,12180
+(defvar read-shell-command-mapread-shell-command-map374,13487
+(defun read-shell-command read-shell-command392,14189
+(defun remassq remassq404,14670
+(defun remassoc remassoc416,15059
+(defun frames-of-buffer frames-of-buffer429,15504
+(defmacro with-selected-window with-selected-window468,16767
+(defun pg-pop-to-buffer pg-pop-to-buffer504,17892
+(defun process-live-p process-live-p555,19744
+
+lib/span.el,192
+(defsubst delete-spans delete-spans24,499
+(defsubst span-property-safe span-property-safe28,653
+(defsubst set-span-start set-span-start32,792
+(defsubst set-span-end set-span-end36,924
+
+lib/span-extent.el,1346
+(defsubst make-span make-span16,557
+(defsubst detach-span detach-span20,679
+(defsubst set-span-endpoints set-span-endpoints24,766
+(defsubst set-span-property set-span-property28,899
+(defsubst span-read-only span-read-only32,1026
+(defsubst span-read-write span-read-write36,1130
+(defun span-give-warning span-give-warning40,1237
+(defun span-write-warning span-write-warning44,1335
+(defsubst span-property span-property49,1535
+(defsubst delete-span delete-span53,1650
+(defsubst mapcar-spans mapcar-spans59,1821
+(defsubst span-at span-at63,2027
+(defsubst span-at-before span-at-before67,2144
+(defsubst span-start span-start72,2341
+(defsubst span-end span-end76,2470
+(defsubst prev-span prev-span80,2593
+(defsubst next-span next-span84,2739
+(defsubst span-live-p span-live-p88,2881
+(defun span-raise span-raise96,3153
+(defalias 'span-object span-object100,3252
+(defalias 'span-string span-string101,3291
+(defsubst make-detached-span make-detached-span104,3377
+(defsubst span-buffer span-buffer109,3439
+(defsubst span-detached-p span-detached-p114,3531
+(defsubst set-span-face set-span-face119,3643
+(defsubst fold-spans fold-spans124,3739
+(defsubst set-span-properties set-span-properties129,3937
+(defsubst set-span-keymap set-span-keymap134,4046
+(defsubst span-at-event span-at-event139,4161
+
+lib/span-overlay.el,1566
+(defalias 'span-start span-start16,543
+(defalias 'span-end span-end17,581
+(defalias 'set-span-property set-span-property18,615
+(defalias 'span-property span-property19,658
+(defalias 'make-span make-span20,697
+(defalias 'detach-span detach-span21,733
+(defalias 'set-span-endpoints set-span-endpoints22,773
+(defalias 'span-buffer span-buffer23,818
+(defun span-read-only-hook span-read-only-hook25,859
+(defun span-read-only span-read-only29,991
+(defun span-read-write span-read-write44,1767
+(defun span-give-warning span-give-warning50,1986
+(defun span-write-warning span-write-warning54,2094
+(defun span-lt span-lt61,2420
+(defun spans-at-point-prop spans-at-point-prop66,2561
+(defun spans-at-region-prop spans-at-region-prop72,2726
+(defun span-at span-at80,2970
+(defsubst delete-span delete-span86,3184
+(defsubst mapcar-spans mapcar-spans93,3406
+(defun span-at-before span-at-before97,3610
+(defun prev-span prev-span114,4336
+(defun next-span next-span120,4487
+(defsubst span-live-p span-live-p149,5712
+(defun span-raise span-raise155,5878
+(defalias 'span-object span-object161,6121
+(defun span-string span-string163,6162
+(defun set-span-properties set-span-properties169,6344
+(defun span-find-span span-find-span181,6599
+(defsubst span-at-event span-at-event188,6906
+(defun make-detached-span make-detached-span193,7030
+(defun fold-spans fold-spans198,7126
+(defsubst span-detached-p span-detached-p213,7660
+(defsubst set-span-face set-span-face217,7775
+(defun set-span-keymap set-span-keymap221,7872
+
+lib/texi-docstring-magic.el,958
+(defun texi-docstring-magic-find-face texi-docstring-magic-find-face85,2996
+(defun texi-docstring-magic-splice-sep texi-docstring-magic-splice-sep90,3161
+(defconst texi-docstring-magic-munge-tabletexi-docstring-magic-munge-table100,3466
+(defun texi-docstring-magic-untabify texi-docstring-magic-untabify190,7186
+(defun texi-docstring-magic-munge-docstring texi-docstring-magic-munge-docstring200,7501
+(defun texi-docstring-magic-texi texi-docstring-magic-texi239,8788
+(defun texi-docstring-magic-format-default texi-docstring-magic-format-default252,9228
+(defun texi-docstring-magic-texi-for texi-docstring-magic-texi-for268,9863
+(defconst texi-docstring-magic-commenttexi-docstring-magic-comment326,11823
+(defun texi-docstring-magic texi-docstring-magic332,11977
+(defun texi-docstring-magic-face-at-point texi-docstring-magic-face-at-point366,13057
+(defun texi-docstring-magic-insert-magic texi-docstring-magic-insert-magic381,13580
+
+lib/xml.el,790
+(defsubst xml-node-name xml-node-name82,2907
+(defsubst xml-node-attributes xml-node-attributes87,3026
+(defsubst xml-node-children xml-node-children92,3144
+(defun xml-get-children xml-get-children97,3280
+(defun xml-get-attribute xml-get-attribute107,3603
+(defun xml-parse-file xml-parse-file123,4067
+(defun xml-parse-region xml-parse-region144,4651
+(defun xml-parse-tag xml-parse-tag179,5696
+(defun xml-parse-attlist xml-parse-attlist284,9165
+(defun xml-skip-dtd xml-skip-dtd321,10555
+(defun xml-parse-dtd xml-parse-dtd338,11191
+(defun xml-parse-elem-type xml-parse-elem-type408,13269
+(defun xml-substitute-special xml-substitute-special449,14424
+(defun xml-debug-print xml-debug-print470,15231
+(defun xml-debug-print-internal xml-debug-print-internal474,15323
+
+mmm/mmm-auto.el,499
+(defvar mmm-autoloaded-classesmmm-autoloaded-classes67,2675
+(defun mmm-autoload-class mmm-autoload-class85,3320
+(defvar mmm-changed-buffers-list mmm-changed-buffers-list125,4887
+(defun mmm-major-mode-change mmm-major-mode-change128,4994
+(defun mmm-check-changed-buffers mmm-check-changed-buffers141,5515
+(defun mmm-mode-on-maybe mmm-mode-on-maybe151,5888
+(defalias 'mmm-add-find-file-hooks mmm-add-find-file-hooks163,6306
+(defun mmm-add-find-file-hook mmm-add-find-file-hook164,6366
+
+mmm/mmm-class.el,626
+(defun mmm-get-class-spec mmm-get-class-spec41,1254
+(defun mmm-get-class-parameter mmm-get-class-parameter58,1967
+(defun mmm-set-class-parameter mmm-set-class-parameter62,2133
+(defun* mmm-apply-classmmm-apply-class74,2497
+(defun* mmm-apply-classesmmm-apply-classes86,3010
+(defun* mmm-apply-all mmm-apply-all106,3776
+(defun* mmm-ifymmm-ify118,4203
+(defun* mmm-match-regionmmm-match-region184,6890
+(defun mmm-match->point mmm-match->point228,8982
+(defun mmm-match-and-verify mmm-match-and-verify241,9525
+(defun mmm-get-form mmm-get-form267,10583
+(defun mmm-default-get-form mmm-default-get-form278,11079
+
+mmm/mmm-cmds.el,1027
+(defun mmm-ify-by-class mmm-ify-by-class40,1179
+(defun mmm-ify-region mmm-ify-region68,2165
+(defun mmm-ify-by-regexpmmm-ify-by-regexp80,2593
+(defun mmm-parse-buffer mmm-parse-buffer100,3244
+(defun mmm-parse-region mmm-parse-region109,3580
+(defun mmm-parse-block mmm-parse-block118,3959
+(defun mmm-get-block mmm-get-block135,4710
+(defun mmm-clear-current-region mmm-clear-current-region151,5095
+(defun mmm-clear-regions mmm-clear-regions156,5259
+(defun mmm-clear-all-regions mmm-clear-all-regions161,5405
+(defun mmm-reparse-current-region mmm-reparse-current-region169,5569
+(defun* mmm-end-current-region mmm-end-current-region188,6185
+(defun mmm-insert-region mmm-insert-region226,7768
+(defun mmm-insert-by-key mmm-insert-by-key245,8630
+(defun mmm-get-insertion-spec mmm-get-insertion-spec291,10888
+(defun mmm-insertion-help mmm-insertion-help318,11967
+(defun mmm-display-insertion-key mmm-display-insertion-key328,12337
+(defun mmm-get-all-insertion-keys mmm-get-all-insertion-keys350,13159
+
+mmm/mmm-compat.el,634
+(defvar mmm-xemacs mmm-xemacs40,1291
+(defvar mmm-keywords-usedmmm-keywords-used49,1594
+(defmacro mmm-regexp-opt mmm-regexp-opt90,2591
+(defvar mmm-evaporate-propertymmm-evaporate-property109,3240
+(defmacro mmm-set-keymap-default mmm-set-keymap-default127,4006
+(defmacro mmm-event-key mmm-event-key136,4448
+(defvar skeleton-positions skeleton-positions145,4667
+(defun mmm-fixup-skeleton mmm-fixup-skeleton146,4698
+(defmacro mmm-make-temp-buffer mmm-make-temp-buffer158,5135
+(defvar mmm-font-lock-available-p mmm-font-lock-available-p171,5531
+(defmacro mmm-set-font-lock-defaults mmm-set-font-lock-defaults178,5745
+
+mmm/mmm-mason.el,592
+(defvar mmm-mason-perl-tagsmmm-mason-perl-tags41,1225
+(defvar mmm-mason-pseudo-perl-tagsmmm-mason-pseudo-perl-tags45,1366
+(defvar mmm-mason-non-perl-tagsmmm-mason-non-perl-tags48,1442
+(defvar mmm-mason-perl-tags-regexpmmm-mason-perl-tags-regexp51,1543
+(defvar mmm-mason-pseudo-perl-tags-regexpmmm-mason-pseudo-perl-tags-regexp56,1738
+(defvar mmm-mason-tag-names-regexpmmm-mason-tag-names-regexp61,1955
+(defun mmm-mason-verify-inline mmm-mason-verify-inline66,2175
+(defun mmm-mason-start-line mmm-mason-start-line154,5041
+(defun mmm-mason-end-line mmm-mason-end-line159,5106
+
+mmm/mmm-mode.el,1496
+(defun mmm-mode mmm-mode106,4116
+(defun mmm-mode-on mmm-mode-on312,13247
+(defun mmm-mode-off mmm-mode-off352,14969
+(defvar mmm-mode-map mmm-mode-map375,15634
+(defvar mmm-mode-prefix-map mmm-mode-prefix-map378,15709
+(defvar mmm-mode-menu-map mmm-mode-menu-map381,15819
+(defun mmm-define-key mmm-define-key384,15910
+(define-key mmm-mode-prefix-map mmm-mode-prefix-map406,16585
+(define-key mmm-mode-prefix-map mmm-mode-prefix-map413,16843
+(define-key mmm-mode-map mmm-mode-map416,16954
+(define-key mmm-mode-menu-map mmm-mode-menu-map419,17056
+(define-key mmm-mode-menu-map mmm-mode-menu-map421,17128
+(define-key mmm-mode-menu-map mmm-mode-menu-map423,17187
+(define-key mmm-mode-menu-map mmm-mode-menu-map425,17268
+(define-key mmm-mode-menu-map mmm-mode-menu-map427,17349
+(define-key mmm-mode-menu-map mmm-mode-menu-map429,17436
+(define-key mmm-mode-menu-map mmm-mode-menu-map432,17530
+(define-key mmm-mode-menu-map mmm-mode-menu-map434,17590
+(define-key mmm-mode-menu-map mmm-mode-menu-map437,17681
+(define-key mmm-mode-menu-map mmm-mode-menu-map439,17741
+(define-key mmm-mode-menu-map mmm-mode-menu-map441,17848
+(define-key mmm-mode-menu-map mmm-mode-menu-map443,17933
+(define-key mmm-mode-menu-map mmm-mode-menu-map446,18019
+(define-key mmm-mode-menu-map mmm-mode-menu-map448,18079
+(define-key mmm-mode-menu-map mmm-mode-menu-map450,18192
+(define-key mmm-mode-menu-map mmm-mode-menu-map452,18277
+(define-key mmm-mode-map mmm-mode-map455,18360
+
+mmm/mmm-region.el,2300
+(defun mmm-overlay-at mmm-overlay-at51,1642
+(defun mmm-overlays-at mmm-overlays-at56,1843
+(defun mmm-included-p mmm-included-p69,2525
+(defun mmm-overlays-in mmm-overlays-in82,2903
+(defun mmm-sort-overlays mmm-sort-overlays100,3840
+(defvar mmm-current-overlay mmm-current-overlay109,4110
+(defvar mmm-previous-overlay mmm-previous-overlay114,4325
+(defvar mmm-current-submode mmm-current-submode119,4513
+(defvar mmm-previous-submode mmm-previous-submode124,4713
+(defun mmm-update-current-submode mmm-update-current-submode129,4886
+(defun mmm-set-current-submode mmm-set-current-submode141,5364
+(defun mmm-submode-at mmm-submode-at152,5856
+(defun mmm-match-front mmm-match-front161,6139
+(defun mmm-match-back mmm-match-back177,6780
+(defun mmm-front-start mmm-front-start195,7402
+(defun mmm-back-end mmm-back-end203,7672
+(defun mmm-make-marker mmm-make-marker216,7969
+(defun* mmm-make-regionmmm-make-region228,8428
+(defun mmm-get-face mmm-get-face286,11150
+(defun mmm-clear-overlays mmm-clear-overlays300,11459
+(defun mmm-update-mode-info mmm-update-mode-info314,11871
+(defun mmm-update-submode-region mmm-update-submode-region397,16038
+(defun mmm-add-hooks mmm-add-hooks417,16958
+(defun mmm-remove-hooks mmm-remove-hooks421,17093
+(defun mmm-get-local-variables-list mmm-get-local-variables-list427,17220
+(defun mmm-get-locals mmm-get-locals447,18140
+(defun mmm-get-saved-local mmm-get-saved-local460,18721
+(defun mmm-set-local-variables mmm-set-local-variables464,18886
+(defun mmm-get-saved-local-variables mmm-get-saved-local-variables475,19327
+(defun mmm-save-changed-local-variables mmm-save-changed-local-variables483,19644
+(defun mmm-clear-local-variables mmm-clear-local-variables502,20502
+(defun mmm-enable-font-lock mmm-enable-font-lock513,20781
+(defun mmm-update-font-lock-buffer mmm-update-font-lock-buffer521,21041
+(defun mmm-refontify-maybe mmm-refontify-maybe534,21564
+(defun mmm-submode-changes-in mmm-submode-changes-in545,21921
+(defun mmm-regions-in mmm-regions-in558,22406
+(defun mmm-regions-alist mmm-regions-alist572,22954
+(defun mmm-fontify-region mmm-fontify-region589,23600
+(defun mmm-fontify-region-list mmm-fontify-region-list607,24494
+(defun mmm-beginning-of-syntax mmm-beginning-of-syntax629,25412
+
+mmm/mmm-rpm.el,242
+(defconst mmm-rpm-sh-start-tagsmmm-rpm-sh-start-tags48,1617
+(defvar mmm-rpm-sh-end-tagsmmm-rpm-sh-end-tags53,1841
+(defvar mmm-rpm-sh-start-regexpmmm-rpm-sh-start-regexp57,2015
+(defvar mmm-rpm-sh-end-regexpmmm-rpm-sh-end-regexp61,2193
+
+mmm/mmm-sample.el,269
+(defvar mmm-here-doc-mode-alist mmm-here-doc-mode-alist81,2448
+(defun mmm-here-doc-get-mode mmm-here-doc-get-mode90,2933
+(defun mmm-file-variables-verify mmm-file-variables-verify196,6459
+(defun mmm-file-variables-find-back mmm-file-variables-find-back220,7495
+
+mmm/mmm-univ.el,52
+(defun mmm-univ-get-mode mmm-univ-get-mode38,1205
+
+mmm/mmm-utils.el,371
+(defmacro mmm-valid-buffer mmm-valid-buffer41,1299
+(defmacro mmm-save-all mmm-save-all60,1943
+(defun mmm-format-string mmm-format-string73,2232
+(defun mmm-format-matches mmm-format-matches84,2684
+(defmacro mmm-save-keyword mmm-save-keyword105,3362
+(defmacro mmm-save-keywords mmm-save-keywords113,3690
+(defun mmm-looking-back-at mmm-looking-back-at126,4224
+
+mmm/mmm-vars.el,3586
+(defgroup mmm mmm86,2527
+(defvar mmm-c-derived-modesmmm-c-derived-modes93,2637
+(defvar mmm-save-local-variables mmm-save-local-variables96,2743
+(defvar mmm-buffer-saved-locals mmm-buffer-saved-locals176,6248
+(defvar mmm-region-saved-locals-defaults mmm-region-saved-locals-defaults181,6448
+(defvar mmm-region-saved-locals-for-dominant mmm-region-saved-locals-for-dominant187,6708
+(defgroup mmm-faces mmm-faces197,7085
+(defcustom mmm-submode-decoration-level mmm-submode-decoration-level203,7256
+(defface mmm-init-submode-face mmm-init-submode-face217,7966
+(defface mmm-cleanup-submode-face mmm-cleanup-submode-face221,8106
+(defface mmm-declaration-submode-face mmm-declaration-submode-face225,8243
+(defface mmm-comment-submode-face mmm-comment-submode-face229,8389
+(defface mmm-output-submode-face mmm-output-submode-face233,8542
+(defface mmm-special-submode-face mmm-special-submode-face237,8691
+(defface mmm-code-submode-face mmm-code-submode-face241,8855
+(defface mmm-default-submode-face mmm-default-submode-face245,8994
+(defcustom mmm-mode-string mmm-mode-string253,9232
+(defcustom mmm-submode-mode-line-format mmm-submode-mode-line-format258,9363
+(defvar mmm-classes mmm-classes268,9635
+(defvar mmm-global-classes mmm-global-classes274,9880
+(defcustom mmm-mode-ext-classes-alist mmm-mode-ext-classes-alist281,10062
+(defun mmm-add-mode-ext-class mmm-add-mode-ext-class300,10880
+(defcustom mmm-major-mode-preferencesmmm-major-mode-preferences309,11205
+(defun mmm-add-to-major-mode-preferences mmm-add-to-major-mode-preferences327,12003
+(defun mmm-ensure-modename mmm-ensure-modename343,12789
+(defun mmm-modename->function mmm-modename->function352,13099
+(defcustom mmm-mode-prefix-key mmm-mode-prefix-key366,13557
+(defcustom mmm-command-modifiers mmm-command-modifiers371,13684
+(defcustom mmm-insert-modifiers mmm-insert-modifiers385,14317
+(defcustom mmm-use-old-command-keys mmm-use-old-command-keys400,14995
+(defun mmm-use-old-command-keys mmm-use-old-command-keys410,15459
+(defcustom mmm-mode-hook mmm-mode-hook418,15658
+(defun mmm-run-constructed-hook mmm-run-constructed-hook438,16468
+(defun mmm-run-major-hook mmm-run-major-hook446,16854
+(defun mmm-run-submode-hook mmm-run-submode-hook449,16931
+(defvar mmm-class-hooks-run mmm-class-hooks-run452,17018
+(defun mmm-run-class-hook mmm-run-class-hook457,17190
+(defcustom mmm-major-mode-hook mmm-major-mode-hook465,17391
+(defun mmm-run-major-mode-hook mmm-run-major-mode-hook479,18022
+(defcustom mmm-global-mode mmm-global-mode486,18160
+(defcustom mmm-never-modesmmm-never-modes503,18748
+(defvar mmm-set-file-name-for-modes mmm-set-file-name-for-modes521,19048
+(defvar mmm-mode mmm-mode532,19369
+(defvar mmm-primary-mode mmm-primary-mode540,19577
+(defvar mmm-classes-alist mmm-classes-alist548,19795
+(defun mmm-add-classes mmm-add-classes668,26175
+(defun mmm-add-group mmm-add-group673,26340
+(defconst mmm-version mmm-version686,26804
+(defun mmm-version mmm-version689,26869
+(defvar mmm-temp-buffer-name mmm-temp-buffer-name696,27012
+(defvar mmm-interactive-history mmm-interactive-history702,27142
+(defun mmm-add-to-history mmm-add-to-history708,27411
+(defun mmm-clear-history mmm-clear-history711,27494
+(defvar mmm-mode-ext-classes mmm-mode-ext-classes719,27679
+(defun mmm-get-mode-ext-classes mmm-get-mode-ext-classes724,27890
+(defun mmm-clear-mode-ext-classes mmm-clear-mode-ext-classes733,28266
+(defun mmm-mode-ext-applies mmm-mode-ext-applies737,28391
+(defun mmm-get-all-classes mmm-get-all-classes751,28875
+
+TODO.developer,1307
+   function to to387,15630
+$Id: TODO.developer,2,21
+This is an outline file.   Use C-c C-n,4,77
+X 55,1529
+*** C Improved configurability of command settings,186,7011
+  We should let command settings,187,7068
+  We should let command settings, etc,187,7068
+  - XEmacs pg forces on font-lock,337,13217
+    Save foo;413,16753
+*** A Doc new bits: font lock keywords,483,19454
+*** A Doc new bits: font lock keywords, filename %e,483,19454
+  Added proof-{script,484,19511
+  Added proof-{script,shell,484,19511
+  Added proof-{script,shell,goals,484,19511
+  Presently used only in proof-easy-config,485,19571
+  - Mention configuring function menus,496,19907
+  - document mouse functions,498,19993
+  - document mouse functions, proof-cd,498,19993
+  - document mouse functions, proof-cd, process quit timeout,498,19993
+    X-Symbol,499,20056
+    X-Symbol, prog-name-guess,499,20056
+*** D Fix INFO-DIR-ENTRY in 513,20564
+*** C Fixing up errors caused by pbp-generated commands; currently,579,23041
+  should mean generates an error.  With LEGO pbp,582,23247
+  tactic which always succeeds,583,23311
+  decodes annotations eagerly. Lazily would be faster,591,23667
+  the tech report claims --- djs: probably not much faster,592,23736
+***  6. Update Emacs and prover versions in texi,681,26739
+
+doc/ProofGeneral.texi,5799
+@node TopTop166,5021
+@node PrefacePreface203,6128
+@node Latest news for 3.5 and 3.6Latest news for 3.5 and 3.6226,6724
+@node FutureFuture265,8412
+@node CreditsCredits300,9962
+@node Introducing Proof GeneralIntroducing Proof General398,13377
+@node Quick start guideQuick start guide453,15369
+@node Features of Proof GeneralFeatures of Proof General507,17938
+@node Supported proof assistantsSupported proof assistants596,21863
+@node Prerequisites for this manualPrerequisites for this manual648,23859
+@node Organization of this manualOrganization of this manual692,25485
+@node Basic Script ManagementBasic Script Management718,26312
+@node Walkthrough example in Isabelle/IsarWalkthrough example in Isabelle/Isar737,26917
+@node Proof scriptsProof scripts964,35452
+@node Script buffersScript buffers1007,37572
+@node Locked queue and editing regionsLocked queue and editing regions1029,38149
+@node Goal-save sequencesGoal-save sequences1085,40296
+@node Active scripting bufferActive scripting buffer1122,41782
+@node Summary of Proof General buffersSummary of Proof General buffers1191,45202
+@node Script editing commandsScript editing commands1253,47876
+@node Script processing commandsScript processing commands1331,50734
+@node Proof assistant commandsProof assistant commands1459,56035
+@node Toolbar commandsToolbar commands1605,60922
+@node Interrupting during trace outputInterrupting during trace output1629,61851
+@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing1668,63774
+@node Goals buffer commandsGoals buffer commands1682,64274
+@node Advanced Script ManagementAdvanced Script Management1771,67806
+@node Visibility of completed proofsVisibility of completed proofs1802,68960
+@node Switching between proof scriptsSwitching between proof scripts1857,70883
+@node View of processed files View of processed files 1894,72855
+@node Retracting across filesRetracting across files1954,75906
+@node Asserting across filesAsserting across files1967,76537
+@node Automatic multiple file handlingAutomatic multiple file handling1980,77103
+@node Escaping script managementEscaping script management2005,78137
+@node Experimental featuresExperimental features2063,80340
+@node Support for other PackagesSupport for other Packages2097,81602
+@node Syntax highlightingSyntax highlighting2129,82477
+@node X-Symbol supportX-Symbol support2168,84098
+@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)2227,86644
+@node Support for outline modeSupport for outline mode2286,88774
+@node Support for completionSupport for completion2312,89904
+@node Support for tagsSupport for tags2369,92069
+@node Customizing Proof GeneralCustomizing Proof General2421,94397
+@node Basic optionsBasic options2461,96067
+@node How to customizeHow to customize2485,96825
+@node Display customizationDisplay customization2536,98927
+@node User optionsUser options2661,104161
+@node Changing facesChanging faces2915,113167
+@node Tweaking configuration settingsTweaking configuration settings2990,115836
+@node Hints and TipsHints and Tips3047,118361
+@node Adding your own keybindingsAdding your own keybindings3066,118962
+@node Using file variablesUsing file variables3122,121495
+@node Using abbreviationsUsing abbreviations3175,123318
+@node LEGO Proof GeneralLEGO Proof General3214,124733
+@node LEGO specific commandsLEGO specific commands3255,126102
+@node LEGO tagsLEGO tags3275,126557
+@node LEGO customizationsLEGO customizations3285,126804
+@node Coq Proof GeneralCoq Proof General3317,127722
+@node Coq-specific commandsCoq-specific commands3333,128131
+@node Coq-specific variablesCoq-specific variables3355,128638
+@node Editing multiple proofsEditing multiple proofs3377,129296
+@node User-loaded tacticsUser-loaded tactics3401,130404
+@node Holes featureHoles feature3465,132878
+@node Isabelle Proof GeneralIsabelle Proof General3492,134164
+@node Classic IsabelleClassic Isabelle3561,137487
+@node ML filesML files3577,137925
+@node Theory filesTheory files3648,140350
+@node General commands for IsabelleGeneral commands for Isabelle3702,142821
+@node Specific commands for IsabelleSpecific commands for Isabelle3714,143303
+@node Isabelle customizationsIsabelle customizations3743,144243
+@node Isabelle/IsarIsabelle/Isar3808,146341
+@node General commands for Isabelle/IsarGeneral commands for Isabelle/Isar3829,147104
+@node Specific commands for Isabelle/IsarSpecific commands for Isabelle/Isar3836,147358
+@node Logics and SettingsLogics and Settings3923,149886
+@node HOL Proof GeneralHOL Proof General3964,151574
+@node Shell Proof GeneralShell Proof General4005,153358
+@node Obtaining and InstallingObtaining and Installing4041,154816
+@node Obtaining Proof GeneralObtaining Proof General4057,155229
+@node Installing Proof General from tarballInstalling Proof General from tarball4088,156468
+@node Installing Proof General from RPM packageInstalling Proof General from RPM package4113,157300
+@node Setting the names of binariesSetting the names of binaries4128,157708
+@node Notes for syssiesNotes for syssies4156,158648
+@node Known BugsKnown Bugs4229,161581
+@node ReferencesReferences4242,161982
+@node History of Proof GeneralHistory of Proof General4282,163006
+@node Old News for 3.0Old News for 3.04373,167108
+@node Old News for 3.1Old News for 3.14443,170802
+@node Old News for 3.2Old News for 3.24469,171974
+@node Old News for 3.3Old News for 3.34530,174977
+@node Old News for 3.4Old News for 3.44549,175874
+@node Function IndexFunction Index4572,176930
+@node Variable IndexVariable Index4576,177006
+@node Keystroke IndexKeystroke Index4580,177086
+@node Concept IndexConcept Index4584,177152
 
 doc/PG-adapting.texi,3863
-@node TopTop157,4775
-@node IntroductionIntroduction195,5920
-@node FutureFuture236,7573
-@node CreditsCredits272,9169
-@node Beginning with a New ProverBeginning with a New Prover282,9461
-@node Overview of adding a new proverOverview of adding a new prover323,11410
-@node Demonstration instance and easy configurationDemonstration instance and easy configuration397,14831
-@node Major modes used by Proof GeneralMajor modes used by Proof General466,18222
-@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands539,21305
-@node Settings for generic user-level commandsSettings for generic user-level commands554,21851
-@node Menu configurationMenu configuration599,23587
-@node Toolbar configurationToolbar configuration623,24505
-@node Proof Script SettingsProof Script Settings681,26750
-@node Recognizing commands and commentsRecognizing commands and comments703,27330
-@node Recognizing proofsRecognizing proofs824,32857
-@node Recognizing other elementsRecognizing other elements936,37671
-@node Configuring undo behaviourConfiguring undo behaviour1062,43149
-@node Nested proofsNested proofs1200,48490
-@node Safe (state-preserving) commandsSafe (state-preserving) commands1240,50117
-@node Activate scripting hookActivate scripting hook1263,51063
-@node Automatic multiple filesAutomatic multiple files1287,51927
-@node CompletionsCompletions1309,52774
-@node Proof Shell SettingsProof Shell Settings1349,54252
-@node Proof shell commandsProof shell commands1380,55534
-@node Script input to the shellScript input to the shell1543,62409
-@node Settings for matching various output from proof processSettings for matching various output from proof process1610,65452
-@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process1741,71216
-@node Hooks and other settingsHooks and other settings1951,80769
-@node Goals Buffer SettingsGoals Buffer Settings2047,84602
-@node Splash Screen SettingsSplash Screen Settings2124,87710
-@node Global ConstantsGlobal Constants2150,88468
-@node Handling Multiple FilesHandling Multiple Files2176,89317
-@node Configuring Editing SyntaxConfiguring Editing Syntax2328,97101
-@node Configuring Font LockConfiguring Font Lock2385,99218
-@node Configuring X-SymbolConfiguring X-Symbol2472,103461
-@node Writing More Lisp CodeWriting More Lisp Code2532,105984
-@node Default values for generic settingsDefault values for generic settings2549,106629
-@node Adding prover-specific configurationsAdding prover-specific configurations2579,107712
-@node Useful variablesUseful variables2622,108982
-@node Useful functions and macrosUseful functions and macros2648,109776
-@node Internals of Proof GeneralInternals of Proof General2750,113653
-@node SpansSpans2778,114561
-@node Proof General site configurationProof General site configuration2791,114935
-@node Configuration variable mechanismsConfiguration variable mechanisms2871,118079
-@node Global variablesGlobal variables2989,123315
-@node Proof script modeProof script mode3059,125865
-@node Proof shell modeProof shell mode3318,137520
-@node DebuggingDebugging3724,153567
-@node Plans and IdeasPlans and Ideas3767,154462
-@node Proof by pointing and similar featuresProof by pointing and similar features3788,155184
-@node Granularity of atomic command sequencesGranularity of atomic command sequences3826,156842
-@node Browser mode for script files and theoriesBrowser mode for script files and theories3871,159067
-@node Demonstration InstantiationsDemonstration Instantiations3901,160098
-@node demoisa-easy.eldemoisa-easy.el3917,160529
-@node demoisa.eldemoisa.el3980,162767
-@node Function IndexFunction Index4148,168283
-@node Variable IndexVariable Index4152,168359
-@node Concept IndexConcept Index4161,168538
+@node TopTop157,4773
+@node IntroductionIntroduction195,5918
+@node FutureFuture236,7571
+@node CreditsCredits272,9167
+@node Beginning with a New ProverBeginning with a New Prover282,9459
+@node Overview of adding a new proverOverview of adding a new prover323,11408
+@node Demonstration instance and easy configurationDemonstration instance and easy configuration397,14829
+@node Major modes used by Proof GeneralMajor modes used by Proof General466,18220
+@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands539,21303
+@node Settings for generic user-level commandsSettings for generic user-level commands554,21849
+@node Menu configurationMenu configuration599,23585
+@node Toolbar configurationToolbar configuration623,24503
+@node Proof Script SettingsProof Script Settings681,26748
+@node Recognizing commands and commentsRecognizing commands and comments703,27328
+@node Recognizing proofsRecognizing proofs824,32855
+@node Recognizing other elementsRecognizing other elements936,37669
+@node Configuring undo behaviourConfiguring undo behaviour1062,43147
+@node Nested proofsNested proofs1200,48488
+@node Safe (state-preserving) commandsSafe (state-preserving) commands1240,50115
+@node Activate scripting hookActivate scripting hook1263,51061
+@node Automatic multiple filesAutomatic multiple files1287,51925
+@node CompletionsCompletions1309,52772
+@node Proof Shell SettingsProof Shell Settings1349,54250
+@node Proof shell commandsProof shell commands1380,55532
+@node Script input to the shellScript input to the shell1543,62407
+@node Settings for matching various output from proof processSettings for matching various output from proof process1610,65450
+@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process1741,71214
+@node Hooks and other settingsHooks and other settings1951,80767
+@node Goals Buffer SettingsGoals Buffer Settings2047,84600
+@node Splash Screen SettingsSplash Screen Settings2124,87708
+@node Global ConstantsGlobal Constants2150,88466
+@node Handling Multiple FilesHandling Multiple Files2176,89315
+@node Configuring Editing SyntaxConfiguring Editing Syntax2328,97099
+@node Configuring Font LockConfiguring Font Lock2385,99216
+@node Configuring X-SymbolConfiguring X-Symbol2472,103459
+@node Writing More Lisp CodeWriting More Lisp Code2532,105982
+@node Default values for generic settingsDefault values for generic settings2549,106627
+@node Adding prover-specific configurationsAdding prover-specific configurations2579,107710
+@node Useful variablesUseful variables2622,108980
+@node Useful functions and macrosUseful functions and macros2648,109774
+@node Internals of Proof GeneralInternals of Proof General2750,113651
+@node SpansSpans2778,114559
+@node Proof General site configurationProof General site configuration2791,114933
+@node Configuration variable mechanismsConfiguration variable mechanisms2871,118077
+@node Global variablesGlobal variables2989,123313
+@node Proof script modeProof script mode3059,125863
+@node Proof shell modeProof shell mode3318,137518
+@node DebuggingDebugging3724,153565
+@node Plans and IdeasPlans and Ideas3767,154460
+@node Proof by pointing and similar featuresProof by pointing and similar features3788,155182
+@node Granularity of atomic command sequencesGranularity of atomic command sequences3826,156840
+@node Browser mode for script files and theoriesBrowser mode for script files and theories3871,159065
+@node Demonstration InstantiationsDemonstration Instantiations3901,160096
+@node demoisa-easy.eldemoisa-easy.el3917,160527
+@node demoisa.eldemoisa.el3980,162765
+@node Function IndexFunction Index4148,168281
+@node Variable IndexVariable Index4152,168357
+@node Concept IndexConcept Index4161,168536
author	David Aspinall <da@inf.ed.ac.uk>	2005-05-17 20:12:37 +0000
committer	David Aspinall <da@inf.ed.ac.uk>	2005-05-17 20:12:37 +0000
commit	c8a0872fe1ea8cbd0169c96a5794dce5133851c4 (patch)
tree	44f2b02e3bb0c620ef9e71271f2410fdceedc2b1 /TAGS
parent	c9058b248b0fbed4fd9db2c55e8741d645a320d0 (diff)