Updated.

1 files changed, 1174 insertions, 1157 deletions

diff --git a/TAGS b/TAGS
index 08419c40..51059b47 100644
--- a/TAGS
+++ b/TAGS
@@ -122,68 +122,68 @@ coq/coq.el,6066
 (defun coq-Compile 768,28189
 (defun coq-guess-command-line 782,28509
 (defun coq-mode-config 803,29362
-(defun coq-hybrid-ouput-goals-response-p 916,33486
-(defun coq-hybrid-ouput-goals-response 922,33744
-(defun coq-shell-mode-config 944,34656
-(defun coq-goals-mode-config 988,36727
-(defun coq-response-config 995,36959
-(defpacustom print-fully-explicit 1018,37668
-(defpacustom print-implicit 1023,37817
-(defpacustom print-coercions 1028,37984
-(defpacustom print-match-wildcards 1033,38129
-(defpacustom print-elim-types 1038,38310
-(defpacustom printing-depth 1043,38477
-(defpacustom time-commands 1048,38639
-(defpacustom auto-compile-vos 1052,38750
-(defun coq-maybe-compile-buffer 1081,39866
-(defun coq-ancestors-of 1118,41400
-(defun coq-all-ancestors-of 1141,42367
-(defconst coq-require-command-regexp 1153,42760
-(defun coq-process-require-command 1158,42969
-(defun coq-included-children 1163,43096
-(defun coq-process-file 1184,43935
-(defun coq-preprocessing 1199,44474
-(defun coq-fake-constant-markup 1214,44893
-(defun coq-create-span-menu 1236,45700
-(defconst module-kinds-table 1256,46277
-(defconst modtype-kinds-table1260,46427
-(defun coq-insert-section-or-module 1264,46556
-(defconst reqkinds-kinds-table1287,47416
-(defun coq-insert-requires 1292,47561
-(defun coq-end-Section 1308,48067
-(defun coq-insert-intros 1326,48651
-(defun coq-insert-match 1338,49175
-(defun coq-insert-tactic 1370,50353
-(defun coq-insert-tactical 1376,50592
-(defun coq-insert-command 1382,50841
-(defun coq-insert-term 1388,51085
-(define-key coq-keymap 1395,51283
-(define-key coq-keymap 1396,51341
-(define-key coq-keymap 1397,51398
-(define-key coq-keymap 1398,51467
-(define-key coq-keymap 1399,51523
-(define-key coq-keymap 1400,51572
-(define-key coq-keymap 1401,51630
-(define-key coq-keymap 1403,51691
-(define-key coq-keymap 1404,51750
-(define-key coq-keymap 1406,51814
-(define-key coq-keymap 1407,51874
-(define-key coq-keymap 1409,51930
-(define-key coq-keymap 1410,51980
-(define-key coq-keymap 1411,52030
-(define-key coq-keymap 1412,52080
-(define-key coq-keymap 1413,52134
-(define-key coq-keymap 1414,52193
-(defvar last-coq-error-location 1424,52376
-(defun coq-get-last-error-location 1433,52775
-(defun coq-highlight-error 1466,54172
-(defvar coq-allow-highlight-error 1531,56727
-(defun coq-decide-highlight-error 1537,56993
-(defun coq-highlight-error-hook 1542,57155
-(defun first-word-of-buffer 1553,57548
-(defun coq-show-first-goal 1562,57779
-(defun is-not-split-vertic 1587,58668
-(defun optim-resp-windows 1596,59107
+(defun coq-hybrid-ouput-goals-response-p 916,33517
+(defun coq-hybrid-ouput-goals-response 922,33775
+(defun coq-shell-mode-config 944,34687
+(defun coq-goals-mode-config 988,36758
+(defun coq-response-config 995,36990
+(defpacustom print-fully-explicit 1018,37699
+(defpacustom print-implicit 1023,37848
+(defpacustom print-coercions 1028,38015
+(defpacustom print-match-wildcards 1033,38160
+(defpacustom print-elim-types 1038,38341
+(defpacustom printing-depth 1043,38508
+(defpacustom time-commands 1048,38670
+(defpacustom auto-compile-vos 1052,38781
+(defun coq-maybe-compile-buffer 1081,39897
+(defun coq-ancestors-of 1118,41431
+(defun coq-all-ancestors-of 1141,42398
+(defconst coq-require-command-regexp 1153,42791
+(defun coq-process-require-command 1158,43000
+(defun coq-included-children 1163,43127
+(defun coq-process-file 1184,43966
+(defun coq-preprocessing 1199,44505
+(defun coq-fake-constant-markup 1214,44924
+(defun coq-create-span-menu 1236,45731
+(defconst module-kinds-table 1256,46308
+(defconst modtype-kinds-table1260,46458
+(defun coq-insert-section-or-module 1264,46587
+(defconst reqkinds-kinds-table1287,47447
+(defun coq-insert-requires 1292,47592
+(defun coq-end-Section 1308,48098
+(defun coq-insert-intros 1326,48682
+(defun coq-insert-match 1338,49206
+(defun coq-insert-tactic 1370,50384
+(defun coq-insert-tactical 1376,50623
+(defun coq-insert-command 1382,50872
+(defun coq-insert-term 1388,51116
+(define-key coq-keymap 1394,51313
+(define-key coq-keymap 1395,51371
+(define-key coq-keymap 1396,51428
+(define-key coq-keymap 1397,51497
+(define-key coq-keymap 1398,51553
+(define-key coq-keymap 1399,51602
+(define-key coq-keymap 1400,51660
+(define-key coq-keymap 1402,51721
+(define-key coq-keymap 1403,51780
+(define-key coq-keymap 1405,51844
+(define-key coq-keymap 1406,51904
+(define-key coq-keymap 1408,51960
+(define-key coq-keymap 1409,52010
+(define-key coq-keymap 1410,52060
+(define-key coq-keymap 1411,52110
+(define-key coq-keymap 1412,52164
+(define-key coq-keymap 1413,52223
+(defvar last-coq-error-location 1423,52406
+(defun coq-get-last-error-location 1432,52805
+(defun coq-highlight-error 1465,54202
+(defvar coq-allow-highlight-error 1530,56757
+(defun coq-decide-highlight-error 1536,57023
+(defun coq-highlight-error-hook 1541,57185
+(defun first-word-of-buffer 1552,57578
+(defun coq-show-first-goal 1561,57809
+(defun is-not-split-vertic 1586,58698
+(defun optim-resp-windows 1595,59137
 
 coq/coq-indent.el,2241
 (defconst coq-any-command-regexp11,262
@@ -882,35 +882,35 @@ plastic/plastic.el,2866
 (defun plastic-find-and-forget 243,7965
 (defun plastic-goal-hyp 278,9313
 (defun plastic-state-preserving-p 289,9563
-(defvar plastic-shell-current-line-width 312,10506
-(defun plastic-shell-adjust-line-width 320,10822
-(defun plastic-mode-config 347,11917
-(defun plastic-show-shell-buffer 436,15158
-(defun plastic-equal-module-filename 442,15261
-(defun plastic-shell-compute-new-files-list 448,15539
-(defun plastic-shell-mode-config 464,16076
-(defun plastic-goals-mode-config 515,18269
-(defun plastic-small-bar 527,18551
-(defun plastic-large-bar 529,18640
-(defun plastic-preprocessing 531,18778
-(defun plastic-all-ctxt 582,20606
-(defun plastic-send-one-undo 589,20784
-(defun plastic-minibuf-cmd 599,21112
-(defun plastic-minibuf 611,21591
-(defun plastic-synchro 618,21797
-(defun plastic-send-minibuf 623,21938
-(defun plastic-had-error 631,22267
-(defun plastic-reset-error 635,22442
-(defun plastic-call-if-no-error 638,22581
-(defun plastic-show-shell 643,22785
-(define-key plastic-keymap 652,23047
-(define-key plastic-keymap 653,23108
-(define-key plastic-keymap 654,23169
-(define-key plastic-keymap 655,23229
-(define-key plastic-keymap 656,23288
-(define-key plastic-keymap 657,23347
-(defalias 'proof-toolbar-command proof-toolbar-command
667,23597
-(defalias 'proof-minibuffer-cmd proof-minibuffer-cmd
668,23648
+(defvar plastic-shell-current-line-width 312,10539
+(defun plastic-shell-adjust-line-width 320,10855
+(defun plastic-mode-config 347,11950
+(defun plastic-show-shell-buffer 436,15191
+(defun plastic-equal-module-filename 442,15294
+(defun plastic-shell-compute-new-files-list 448,15572
+(defun plastic-shell-mode-config 464,16109
+(defun plastic-goals-mode-config 515,18302
+(defun plastic-small-bar 527,18584
+(defun plastic-large-bar 529,18673
+(defun plastic-preprocessing 531,18811
+(defun plastic-all-ctxt 582,20639
+(defun plastic-send-one-undo 589,20817
+(defun plastic-minibuf-cmd 599,21145
+(defun plastic-minibuf 611,21624
+(defun plastic-synchro 618,21830
+(defun plastic-send-minibuf 623,21971
+(defun plastic-had-error 631,22300
+(defun plastic-reset-error 635,22475
+(defun plastic-call-if-no-error 638,22614
+(defun plastic-show-shell 643,22818
+(define-key plastic-keymap 652,23080
+(define-key plastic-keymap 653,23141
+(define-key plastic-keymap 654,23202
+(define-key plastic-keymap 655,23262
+(define-key plastic-keymap 656,23321
+(define-key plastic-keymap 657,23380
+(defalias 'proof-toolbar-command proof-toolbar-command
667,23630
+(defalias 'proof-minibuffer-cmd proof-minibuffer-cmd
668,23681
 
 plastic/plastic-syntax.el,648
 (defconst plastic-keywords-goal 18,537
@@ -1151,14 +1151,14 @@ twelf/twelf-old.el,6958
 (defun twelf-server-reset-menu 2655,107386
 
 generic/pg-assoc.el,354
-(defun proof-associated-buffers 37,1081
-(defun proof-associated-windows 46,1278
-(defun pg-assoc-strip-subterm-markup 63,1759
-(defvar pg-assoc-ann-regexp 89,2692
-(defun pg-assoc-strip-subterm-markup-buf 92,2787
-(defun pg-assoc-strip-subterm-markup-buf-old 115,3506
-(defun pg-assoc-make-top-span 144,4361
-(defun pg-assoc-analyse-structure 173,5580
+(defun proof-associated-buffers 38,1096
+(defun proof-associated-windows 48,1308
+(defun pg-assoc-strip-subterm-markup 65,1789
+(defvar pg-assoc-ann-regexp 91,2722
+(defun pg-assoc-strip-subterm-markup-buf 94,2817
+(defun pg-assoc-strip-subterm-markup-buf-old 117,3536
+(defun pg-assoc-make-top-span 146,4391
+(defun pg-assoc-analyse-structure 175,5610
 
 generic/pg-autotest.el,443
 (defvar pg-autotest-success 26,573
@@ -1206,130 +1206,130 @@ generic/pg-metadata.el,127
 (defface proof-preparsed-span34,919
 (defun pg-metadata-filename-for 45,1181
 
-generic/pg-pbrpm.el,1801
-(defvar pg-pbrpm-use-buffer-menu 14,297
-(defvar pg-pbrpm-start-goal-regexp 17,419
-(defvar pg-pbrpm-start-goal-regexp-par-num 21,576
-(defvar pg-pbrpm-end-goal-regexp 24,699
-(defvar pg-pbrpm-start-hyp-regexp 28,851
-(defvar pg-pbrpm-start-hyp-regexp-par-num 32,1012
-(defvar pg-pbrpm-start-concl-regexp 36,1219
-(defvar pg-pbrpm-auto-select-regexp 40,1383
-(defvar pg-pbrpm-buffer-menu 47,1544
-(defvar pg-pbrpm-spans 48,1578
-(defvar pg-pbrpm-goal-description 49,1606
-(defvar pg-pbrpm-windows-dialog-bug 50,1645
-(defvar pbrpm-menu-desc 51,1686
-(defun pg-pbrpm-erase-buffer-menu 53,1716
-(defun pg-pbrpm-menu-change-hook 60,1900
-(defun pg-pbrpm-create-reset-buffer-menu 78,2476
-(defun pg-pbrpm-analyse-goal-buffer 93,3105
-(defun pg-pbrpm-button-action 153,5515
-(defun pg-pbrpm-exists 160,5741
-(defun pg-pbrpm-eliminate-id 164,5853
-(defun pg-pbrpm-build-menu 172,6099
-(defun pg-pbrpm-setup-span 239,8667
-(defun pg-pbrpm-run-command 299,10984
-(defun pg-pbrpm-get-pos-info 328,12294
-(defun pg-pbrpm-get-region-info 368,13528
-(defun pg-pbrpm-auto-select-around-point 379,13942
-(defun pg-pbrpm-translate-position 394,14472
-(defun pg-pbrpm-process-click 400,14695
-(defvar pg-pbrpm-remember-region-selected-region 420,15720
-(defvar pg-pbrpm-regions-list 421,15774
-(defun pg-pbrpm-erase-regions-list 423,15810
-(defun pg-pbrpm-filter-regions-list 432,16118
-(defface pg-pbrpm-multiple-selection-face439,16381
-(defface pg-pbrpm-menu-input-face447,16583
-(defun pg-pbrpm-do-remember-region 455,16773
-(defun pg-pbrpm-remember-region-drag-up-hook 476,17621
-(defun pg-pbrpm-remember-region-click-hook 480,17792
-(defun pg-pbrpm-remember-region 485,17977
-(defun pg-pbrpm-process-region 499,18692
-(defun pg-pbrpm-process-regions-list 516,19417
-(defun pg-pbrpm-region-expression 520,19600
-
-generic/pg-pgip.el,2890
-(defalias 'pg-pgip-debug pg-pgip-debug
35,939
-(defalias 'pg-pgip-error pg-pgip-error
36,980
-(defalias 'pg-pgip-warning pg-pgip-warning
37,1015
-(defconst pg-pgip-version-supported 39,1065
-(defun pg-pgip-process-packet 43,1171
-(defvar pg-pgip-last-seen-id 53,1743
-(defvar pg-pgip-last-seen-seq 54,1777
-(defun pg-pgip-process-pgip 56,1813
-(defun pg-pgip-process-msg 75,2744
-(defvar pg-pgip-post-process-functions89,3311
-(defun pg-pgip-post-process 99,3799
-(defun pg-pgip-process-askpgip 115,4410
-(defun pg-pgip-process-usespgip 120,4569
-(defun pg-pgip-process-usespgml 124,4733
-(defun pg-pgip-process-pgmlconfig 128,4897
-(defun pg-pgip-process-proverinfo 144,5514
-(defun pg-pgip-process-hasprefs 161,6179
-(defun pg-pgip-haspref 175,6811
-(defun pg-pgip-process-prefval 194,7587
-(defun pg-pgip-process-guiconfig 221,8296
-(defvar proof-assistant-idtables 228,8413
-(defun pg-pgip-process-ids 231,8530
-(defun pg-complete-idtable-symbol 257,9606
-(defalias 'pg-pgip-process-setids pg-pgip-process-setids
262,9698
-(defalias 'pg-pgip-process-addids pg-pgip-process-addids
263,9754
-(defalias 'pg-pgip-process-delids pg-pgip-process-delids
264,9810
-(defun pg-pgip-process-idvalue 267,9868
-(defun pg-pgip-process-menuadd 279,10204
-(defun pg-pgip-process-menudel 282,10247
-(defun pg-pgip-process-ready 291,10480
-(defun pg-pgip-process-cleardisplay 294,10521
-(defun pg-pgip-process-proofstate 308,10978
-(defun pg-pgip-process-normalresponse 312,11055
-(defun pg-pgip-process-errorresponse 316,11179
-(defun pg-pgip-process-scriptinsert 320,11302
-(defun pg-pgip-process-metainforesponse 325,11436
-(defun pg-pgip-process-informfileloaded 334,11677
-(defun pg-pgip-process-informfileretracted 340,11943
-(defun pg-pgip-process-brokerstatus 353,12420
-(defun pg-pgip-process-proveravailmsg 356,12468
-(defun pg-pgip-process-newprovermsg 359,12518
-(defun pg-pgip-process-proverstatusmsg 362,12566
-(defvar pg-pgip-srcids 371,12813
-(defun pg-pgip-process-newfile 375,12920
-(defun pg-pgip-process-filestatus 391,13508
-(defun pg-pgip-process-newobj 411,14163
-(defun pg-pgip-process-delobj 414,14205
-(defun pg-pgip-process-objectstatus 417,14247
-(defun pg-pgip-process-parsescript 431,14602
-(defun pg-pgip-get-pgiptype 454,15477
-(defun pg-pgip-default-for 474,16270
-(defun pg-pgip-subst-for 487,16665
-(defun pg-pgip-interpret-value 499,17008
-(defun pg-pgip-interpret-choice 517,17693
-(defun pg-pgip-string-of-command 548,18710
-(defconst pg-pgip-id565,19471
-(defvar pg-pgip-refseq 571,19751
-(defvar pg-pgip-refid 573,19848
-(defvar pg-pgip-seq 576,19940
-(defun pg-pgip-assemble-packet 578,20004
-(defun pg-pgip-issue 596,20816
-(defun pg-pgip-maybe-askpgip 613,21428
-(defun pg-pgip-askprefs 619,21619
-(defun pg-pgip-askids 623,21733
-(defun pg-pgip-reset 636,22021
-(defconst pg-pgip-start-element-regexp 667,22719
-(defconst pg-pgip-end-element-regexp 668,22771
+generic/pg-pbrpm.el,1802
+(defvar pg-pbrpm-use-buffer-menu 20,489
+(defvar pg-pbrpm-start-goal-regexp 23,611
+(defvar pg-pbrpm-start-goal-regexp-par-num 27,768
+(defvar pg-pbrpm-end-goal-regexp 30,891
+(defvar pg-pbrpm-start-hyp-regexp 34,1043
+(defvar pg-pbrpm-start-hyp-regexp-par-num 38,1204
+(defvar pg-pbrpm-start-concl-regexp 42,1411
+(defvar pg-pbrpm-auto-select-regexp 46,1575
+(defvar pg-pbrpm-buffer-menu 53,1736
+(defvar pg-pbrpm-spans 54,1770
+(defvar pg-pbrpm-goal-description 55,1798
+(defvar pg-pbrpm-windows-dialog-bug 56,1837
+(defvar pbrpm-menu-desc 57,1878
+(defun pg-pbrpm-erase-buffer-menu 59,1908
+(defun pg-pbrpm-menu-change-hook 66,2092
+(defun pg-pbrpm-create-reset-buffer-menu 84,2668
+(defun pg-pbrpm-analyse-goal-buffer 99,3297
+(defun pg-pbrpm-button-action 159,5707
+(defun pg-pbrpm-exists 166,5933
+(defun pg-pbrpm-eliminate-id 170,6045
+(defun pg-pbrpm-build-menu 178,6291
+(defun pg-pbrpm-setup-span 251,8918
+(defun pg-pbrpm-run-command 311,11236
+(defun pg-pbrpm-get-pos-info 340,12546
+(defun pg-pbrpm-get-region-info 382,13853
+(defun pg-pbrpm-auto-select-around-point 393,14267
+(defun pg-pbrpm-translate-position 408,14797
+(defun pg-pbrpm-process-click 416,15055
+(defvar pg-pbrpm-remember-region-selected-region 436,16080
+(defvar pg-pbrpm-regions-list 437,16134
+(defun pg-pbrpm-erase-regions-list 439,16170
+(defun pg-pbrpm-filter-regions-list 448,16478
+(defface pg-pbrpm-multiple-selection-face455,16741
+(defface pg-pbrpm-menu-input-face463,16943
+(defun pg-pbrpm-do-remember-region 471,17133
+(defun pg-pbrpm-remember-region-drag-up-hook 492,17981
+(defun pg-pbrpm-remember-region-click-hook 496,18152
+(defun pg-pbrpm-remember-region 501,18337
+(defun pg-pbrpm-process-region 515,19052
+(defun pg-pbrpm-process-regions-list 533,19781
+(defun pg-pbrpm-region-expression 537,19964
+
+generic/pg-pgip.el,2892
+(defalias 'pg-pgip-debug pg-pgip-debug
36,985
+(defalias 'pg-pgip-error pg-pgip-error
37,1026
+(defalias 'pg-pgip-warning pg-pgip-warning
38,1061
+(defconst pg-pgip-version-supported 40,1111
+(defun pg-pgip-process-packet 44,1217
+(defvar pg-pgip-last-seen-id 54,1789
+(defvar pg-pgip-last-seen-seq 55,1823
+(defun pg-pgip-process-pgip 57,1859
+(defun pg-pgip-process-msg 76,2790
+(defvar pg-pgip-post-process-functions90,3360
+(defun pg-pgip-post-process 100,3848
+(defun pg-pgip-process-askpgip 116,4459
+(defun pg-pgip-process-usespgip 122,4664
+(defun pg-pgip-process-usespgml 126,4828
+(defun pg-pgip-process-pgmlconfig 130,4992
+(defun pg-pgip-process-proverinfo 146,5609
+(defun pg-pgip-process-hasprefs 163,6274
+(defun pg-pgip-haspref 177,6906
+(defun pg-pgip-process-prefval 196,7682
+(defun pg-pgip-process-guiconfig 223,8391
+(defvar proof-assistant-idtables 230,8508
+(defun pg-pgip-process-ids 233,8625
+(defun pg-complete-idtable-symbol 259,9701
+(defalias 'pg-pgip-process-setids pg-pgip-process-setids
264,9793
+(defalias 'pg-pgip-process-addids pg-pgip-process-addids
265,9849
+(defalias 'pg-pgip-process-delids pg-pgip-process-delids
266,9905
+(defun pg-pgip-process-idvalue 269,9963
+(defun pg-pgip-process-menuadd 281,10299
+(defun pg-pgip-process-menudel 284,10342
+(defun pg-pgip-process-ready 293,10575
+(defun pg-pgip-process-cleardisplay 296,10616
+(defun pg-pgip-process-proofstate 310,11073
+(defun pg-pgip-process-normalresponse 314,11150
+(defun pg-pgip-process-errorresponse 318,11274
+(defun pg-pgip-process-scriptinsert 322,11397
+(defun pg-pgip-process-metainforesponse 327,11531
+(defun pg-pgip-process-informfileloaded 336,11772
+(defun pg-pgip-process-informfileretracted 342,12038
+(defun pg-pgip-process-brokerstatus 355,12515
+(defun pg-pgip-process-proveravailmsg 358,12563
+(defun pg-pgip-process-newprovermsg 361,12613
+(defun pg-pgip-process-proverstatusmsg 364,12661
+(defvar pg-pgip-srcids 373,12908
+(defun pg-pgip-process-newfile 377,13015
+(defun pg-pgip-process-filestatus 393,13603
+(defun pg-pgip-process-newobj 413,14258
+(defun pg-pgip-process-delobj 416,14300
+(defun pg-pgip-process-objectstatus 419,14342
+(defun pg-pgip-process-parsescript 433,14697
+(defun pg-pgip-get-pgiptype 456,15572
+(defun pg-pgip-default-for 476,16365
+(defun pg-pgip-subst-for 489,16760
+(defun pg-pgip-interpret-value 501,17103
+(defun pg-pgip-interpret-choice 519,17788
+(defun pg-pgip-string-of-command 550,18805
+(defconst pg-pgip-id567,19566
+(defvar pg-pgip-refseq 573,19846
+(defvar pg-pgip-refid 575,19943
+(defvar pg-pgip-seq 578,20035
+(defun pg-pgip-assemble-packet 580,20099
+(defun pg-pgip-issue 598,20911
+(defun pg-pgip-maybe-askpgip 615,21523
+(defun pg-pgip-askprefs 621,21714
+(defun pg-pgip-askids 625,21828
+(defun pg-pgip-reset 638,22116
+(defconst pg-pgip-start-element-regexp 669,22814
+(defconst pg-pgip-end-element-regexp 670,22866
 
 generic/pg-pgip-old.el,456
-(defun pg-pgip-process-oldhaspref 18,633
-(defun pg-pgip-process-haspref 21,730
-(defun pg-pgip-old-interpret-bool 57,2158
-(defun pg-pgip-old-interpret-int 66,2442
-(defun pg-pgip-old-interpret-string 71,2615
-(defun pg-pgip-old-interpret-choice 74,2669
-(defun pg-pgip-old-interpret-value 94,3388
-(defun pg-pgip-old-default-for 113,3934
-(defun pg-pgip-old-subst-for 124,4258
-(defun pg-pgip-old-get-type 131,4423
-(defun pg-pgip-old-pgiptype 138,4639
+(defun pg-pgip-process-oldhaspref 19,617
+(defun pg-pgip-process-haspref 22,714
+(defun pg-pgip-old-interpret-bool 58,2142
+(defun pg-pgip-old-interpret-int 67,2426
+(defun pg-pgip-old-interpret-string 72,2599
+(defun pg-pgip-old-interpret-choice 75,2653
+(defun pg-pgip-old-interpret-value 95,3372
+(defun pg-pgip-old-default-for 114,3918
+(defun pg-pgip-old-subst-for 125,4242
+(defun pg-pgip-old-get-type 132,4407
+(defun pg-pgip-old-pgiptype 139,4623
 
 generic/pg-response.el,1182
 (deflocal pg-response-eagerly-raise 31,731
@@ -1350,15 +1350,15 @@ generic/pg-response.el,1182
 (defvar pg-response-erase-flag 256,9339
 (defun pg-response-maybe-erase260,9468
 (defun pg-response-display 291,10653
-(defun pg-response-display-with-face 309,11486
-(defun pg-response-clear-displays 345,12716
-(defun proof-next-error 364,13303
-(defun pg-response-has-error-location 445,16219
-(defvar proof-trace-last-fontify-pos 468,17052
-(defun proof-trace-fontify-pos 470,17095
-(defun proof-trace-buffer-display 478,17408
-(defun proof-trace-buffer-finish 502,18408
-(defun pg-thms-buffer-clear 523,18988
+(defun pg-response-display-with-face 310,11501
+(defun pg-response-clear-displays 346,12731
+(defun proof-next-error 365,13318
+(defun pg-response-has-error-location 446,16234
+(defvar proof-trace-last-fontify-pos 469,17067
+(defun proof-trace-fontify-pos 471,17110
+(defun proof-trace-buffer-display 479,17423
+(defun proof-trace-buffer-finish 503,18395
+(defun pg-thms-buffer-clear 524,18975
 
 generic/pg-thymodes.el,152
 (defmacro pg-defthymode 23,499
@@ -1367,63 +1367,82 @@ generic/pg-thymodes.el,152
 (defun pg-modesym 82,2549
 (defun pg-modesymval 86,2663
 
-generic/pg-user.el,2336
-(defmacro proof-maybe-save-point 22,441
-(defun proof-maybe-follow-locked-end 30,643
-(defun proof-assert-next-command-interactive 44,1008
-(defun proof-process-buffer 54,1379
-(defun proof-undo-last-successful-command 68,1696
-(defun proof-undo-and-delete-last-successful-command 73,1858
-(defun proof-undo-last-successful-command-1 95,2829
-(defun proof-retract-buffer 111,3394
-(defun proof-retract-current-goal 120,3674
-(defun proof-interrupt-process 138,4165
-(defun proof-goto-command-start 165,5146
-(defun proof-goto-command-end 188,6086
-(defun proof-mouse-goto-point 213,6864
-(defun proof-mouse-track-insert 228,7435
-(defvar proof-minibuffer-history 263,8543
-(defun proof-minibuffer-cmd 266,8638
-(defun proof-frob-locked-end 314,10436
-(defmacro proof-if-setting-configured 407,13352
-(defmacro proof-define-assistant-command 415,13621
-(defmacro proof-define-assistant-command-witharg 428,14084
-(defun proof-issue-new-command 448,14907
-(defun proof-cd-sync 493,16402
-(deflocal proof-electric-terminator 544,17867
-(defun proof-electric-terminator-enable 554,18214
-(defun proof-electric-term-incomment-fn 565,18700
-(defun proof-process-electric-terminator 585,19451
-(defun proof-electric-terminator 612,20599
-(defun proof-add-completions 634,21234
-(defun proof-script-complete 654,21988
-(defun pg-insert-last-output-as-comment 682,22579
-(defun pg-copy-span-contents 713,23805
-(defun pg-numth-span-higher-or-lower 730,24363
-(defun pg-control-span-of 756,25109
-(defun pg-move-span-contents 762,25313
-(defun pg-fixup-children-span 816,27536
-(defun pg-move-region-down 823,27739
-(defun pg-move-region-up 832,28032
-(defun proof-forward-command 862,28870
-(defun proof-backward-command 883,29591
-(defvar pg-span-context-menu-keymap899,29835
-(defun pg-span-for-event 915,30257
-(defun pg-span-context-menu 926,30635
-(defun pg-toggle-visibility 941,31090
-(defun pg-create-in-span-context-menu 951,31412
-(defun pg-span-undo 984,32756
-(defun pg-goals-buffers-hint 1030,34166
-(defun pg-slow-fontify-tracing-hint 1033,34333
-(defun pg-response-buffers-hint 1036,34489
-(defun pg-jump-to-end-hint 1045,34836
-(defun pg-processing-complete-hint 1048,34952
-(defun pg-next-error-hint 1064,35636
-(defun pg-hint 1068,35773
-(defun pg-identifier-under-mouse-query 1087,36443
-(defun proof-imenu-enable 1132,38065
-
-generic/pg-vars.el,936
+generic/pg-user.el,3126
+(defmacro proof-maybe-save-point 31,794
+(defun proof-maybe-follow-locked-end 39,996
+(defun proof-assert-next-command-interactive 53,1361
+(defun proof-process-buffer 63,1732
+(defun proof-undo-last-successful-command 77,2049
+(defun proof-undo-and-delete-last-successful-command 82,2211
+(defun proof-undo-last-successful-command-1 104,3182
+(defun proof-retract-buffer 120,3747
+(defun proof-retract-current-goal 129,4027
+(defun proof-interrupt-process 148,4533
+(defun proof-goto-command-start 175,5487
+(defun proof-goto-command-end 198,6427
+(defun proof-mouse-goto-point 223,7205
+(defun proof-mouse-track-insert 239,7837
+(defvar proof-minibuffer-history 275,8974
+(defun proof-minibuffer-cmd 278,9069
+(defun proof-frob-locked-end 326,10863
+(defmacro proof-if-setting-configured 387,12793
+(defmacro proof-define-assistant-command 395,13062
+(defmacro proof-define-assistant-command-witharg 408,13517
+(defun proof-issue-new-command 428,14340
+(defun proof-cd-sync 473,15835
+(defun proof-electric-terminator-enable 532,17594
+(defun proof-electric-term-incomment-fn 540,17889
+(defun proof-process-electric-terminator 560,18640
+(defun proof-electric-terminator 587,19788
+(defun proof-add-completions 609,20425
+(defun proof-script-complete 629,21179
+(defun pg-insert-last-output-as-comment 657,21770
+(defun pg-copy-span-contents 688,23004
+(defun pg-numth-span-higher-or-lower 705,23562
+(defun pg-control-span-of 731,24308
+(defun pg-move-span-contents 737,24512
+(defun pg-fixup-children-spans 789,26692
+(defun pg-move-region-down 799,26955
+(defun pg-move-region-up 808,27248
+(defun proof-forward-command 838,28086
+(defun proof-backward-command 859,28807
+(defun pg-pos-for-event 881,29158
+(defun pg-span-for-event 893,29519
+(defun pg-span-context-menu 897,29663
+(defun pg-toggle-visibility 912,30118
+(defun pg-create-in-span-context-menu 922,30440
+(defun pg-span-undo 955,31784
+(defun pg-goals-buffers-hint 1001,33194
+(defun pg-slow-fontify-tracing-hint 1005,33376
+(defun pg-response-buffers-hint 1009,33547
+(defun pg-jump-to-end-hint 1019,33909
+(defun pg-processing-complete-hint 1023,34040
+(defun pg-next-error-hint 1040,34739
+(defun pg-hint 1045,34891
+(defun pg-identifier-under-mouse-query 1064,35560
+(defun proof-imenu-enable 1110,37215
+(defvar pg-input-ring 1143,38355
+(defvar pg-input-ring-index 1146,38411
+(defvar pg-stored-incomplete-input 1149,38482
+(defun pg-previous-input 1152,38584
+(defun pg-next-input 1166,39041
+(defun pg-delete-input 1171,39163
+(defun pg-get-old-input 1184,39501
+(defun pg-restore-input 1198,39892
+(defun pg-search-start 1209,40182
+(defun pg-regexp-arg 1221,40674
+(defun pg-search-arg 1233,41122
+(defun pg-previous-matching-input-string-position 1247,41539
+(defun pg-previous-matching-input 1274,42704
+(defun pg-next-matching-input 1293,43540
+(defvar pg-matching-input-from-input-string 1301,43923
+(defun pg-previous-matching-input-from-input 1305,44037
+(defun pg-next-matching-input-from-input 1323,44802
+(defun pg-add-to-input-history 1334,45181
+(defun pg-remove-from-input-history 1346,45634
+(defun  pg-clear-input-ring 1357,46017
+
+generic/pg-vars.el,1106
 (defvar proof-assistant-cusgrp 18,322
 (defvar proof-assistant-internals-cusgrp 24,584
 (defvar proof-assistant 30,855
@@ -1445,53 +1464,58 @@ generic/pg-vars.el,936
 (defvar proof-shell-error-or-interrupt-seen 129,4638
 (defvar pg-response-next-error 134,4862
 (defvar proof-shell-proof-completed 137,4969
-(defvar proof-shell-last-output 142,5174
-(defvar proof-terminal-string 153,5654
+(defvar proof-terminal-string 149,5513
+(defvar proof-shell-last-output 159,5703
+(defvar proof-assistant-settings 163,5844
+(defvar pg-tracing-slow-mode 170,6207
+(defvar proof-nesting-depth 173,6296
+(defvar proof-last-theorem-dependencies 180,6531
 
 generic/pg-xhtml.el,390
 (defvar pg-xhtml-dir 24,472
 (defun pg-xhtml-dir 27,538
-(defvar pg-xhtml-file-count 39,905
-(defun pg-xhtml-next-file 42,977
-(defvar pg-xhtml-header54,1207
-(defmacro pg-xhtml-write-tempfile 60,1447
-(defun pg-xhtml-cleanup-tempdir 78,2042
-(defvar pg-mozilla-prog-name82,2173
-(defun pg-xhtml-display-file-mozilla 86,2280
-(defalias 'pg-xhtml-display-file pg-xhtml-display-file
91,2449
-
-generic/pg-xml.el,1095
-(defun pg-xml-parse-string 40,1165
-(defun pg-xml-parse-buffer 51,1498
-(defun pg-xml-get-attr 73,2231
-(defun pg-xml-child-elts 81,2534
-(defun pg-xml-child-elt 86,2739
-(defun pg-xml-get-child 94,3021
-(defun pg-xml-get-text-content 104,3393
-(defmacro pg-xml-attr 115,3743
-(defmacro pg-xml-node 117,3805
-(defconst pg-xml-header120,3897
-(defun pg-xml-string-of 124,3973
-(defun pg-xml-output-internal 135,4344
-(defun pg-xml-cdata 169,5494
-(defun pg-pgip-get-icon 177,5687
-(defsubst pg-pgip-get-name 181,5835
-(defsubst pg-pgip-get-version 184,5952
-(defsubst pg-pgip-get-descr 187,6075
-(defsubst pg-pgip-get-thmname 190,6194
-(defsubst pg-pgip-get-thyname 193,6317
-(defsubst pg-pgip-get-url 196,6440
-(defsubst pg-pgip-get-srcid 199,6555
-(defsubst pg-pgip-get-proverid 202,6674
-(defsubst pg-pgip-get-symname 205,6799
-(defsubst pg-pgip-get-prefcat 208,6919
-(defsubst pg-pgip-get-default 211,7047
-(defsubst pg-pgip-get-objtype 214,7170
-(defsubst pg-pgip-get-value 217,7293
-(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext
220,7363
-(defun pg-pgip-get-pgmltext 222,7422
-
-generic/proof-config.el,10914
+(defvar pg-xhtml-file-count 39,873
+(defun pg-xhtml-next-file 42,945
+(defvar pg-xhtml-header54,1175
+(defmacro pg-xhtml-write-tempfile 60,1415
+(defun pg-xhtml-cleanup-tempdir 78,2010
+(defvar pg-mozilla-prog-name82,2141
+(defun pg-xhtml-display-file-mozilla 86,2248
+(defalias 'pg-xhtml-display-file pg-xhtml-display-file
91,2417
+
+generic/pg-xml.el,1141
+(defalias 'pg-xml-error pg-xml-error
24,625
+(defun pg-xml-parse-string 47,1267
+(defun pg-xml-parse-buffer 58,1593
+(defun pg-xml-get-attr 80,2326
+(defun pg-xml-child-elts 88,2628
+(defun pg-xml-child-elt 93,2833
+(defun pg-xml-get-child 101,3115
+(defun pg-xml-get-text-content 111,3487
+(defmacro pg-xml-attr 122,3837
+(defmacro pg-xml-node 124,3899
+(defconst pg-xml-header127,3991
+(defun pg-xml-string-of 131,4067
+(defun pg-xml-output-internal 142,4434
+(defun pg-xml-cdata 176,5584
+(defun pg-pgip-get-icon 184,5777
+(defsubst pg-pgip-get-name 188,5925
+(defsubst pg-pgip-get-version 191,6042
+(defsubst pg-pgip-get-descr 194,6165
+(defsubst pg-pgip-get-thmname 197,6284
+(defsubst pg-pgip-get-thyname 200,6407
+(defsubst pg-pgip-get-url 203,6530
+(defsubst pg-pgip-get-srcid 206,6645
+(defsubst pg-pgip-get-proverid 209,6764
+(defsubst pg-pgip-get-symname 212,6889
+(defsubst pg-pgip-get-prefcat 215,7009
+(defsubst pg-pgip-get-default 218,7137
+(defsubst pg-pgip-get-objtype 221,7260
+(defsubst pg-pgip-get-value 224,7383
+(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext
227,7453
+(defun pg-pgip-get-pgmltext 229,7512
+
+generic/proof-config.el,10956
 (defgroup proof-user-options 87,3099
 (defun proof-set-value 96,3296
 (defcustom proof-electric-terminator-enable 126,4358
@@ -1508,426 +1532,425 @@ generic/proof-config.el,10914
 (defcustom proof-shrink-windows-tofit 237,8822
 (defcustom proof-toolbar-use-button-enablers 244,9094
 (defcustom proof-query-file-save-when-activating-scripting252,9429
-(defcustom proof-one-command-per-line271,10202
-(defcustom proof-prog-name-ask279,10421
-(defcustom proof-prog-name-guess285,10581
-(defcustom proof-tidy-response293,10840
-(defcustom proof-keep-response-history307,11303
-(defcustom proof-general-debug 317,11691
-(defcustom proof-experimental-features326,12062
-(defcustom proof-follow-mode 344,12821
-(defcustom proof-auto-action-when-deactivating-scripting 368,14001
-(defcustom proof-script-command-separator 391,14950
-(defcustom proof-rsh-command 399,15242
-(defcustom proof-disappearing-proofs 415,15792
-(defgroup proof-faces 442,16438
-(defconst pg-defface-window-systems 447,16544
-(defmacro proof-face-specs 459,17061
-(defface proof-queue-face475,17581
-(defface proof-locked-face483,17859
-(defface proof-declaration-name-face496,18362
-(defface proof-tacticals-name-face505,18648
-(defface proof-tactics-name-face514,18910
-(defface proof-error-face523,19175
-(defface proof-warning-face531,19381
-(defface proof-eager-annotation-face540,19638
-(defface proof-debug-message-face548,19856
-(defface proof-boring-face556,20055
-(defface proof-mouse-highlight-face564,20247
-(defface proof-highlight-dependent-face572,20443
-(defface proof-highlight-dependency-face580,20652
-(defface proof-active-area-face588,20849
-(defconst proof-face-compat-doc 598,21142
-(defconst proof-queue-face 599,21222
-(defconst proof-locked-face 600,21290
-(defconst proof-declaration-name-face 601,21360
-(defconst proof-tacticals-name-face 602,21450
-(defconst proof-tactics-name-face 603,21536
-(defconst proof-error-face 604,21618
-(defconst proof-warning-face 605,21686
-(defconst proof-eager-annotation-face 606,21758
-(defconst proof-debug-message-face 607,21848
-(defconst proof-boring-face 608,21932
-(defconst proof-mouse-highlight-face 609,22002
-(defconst proof-highlight-dependent-face 610,22090
-(defconst proof-highlight-dependency-face 611,22186
-(defconst proof-active-area-face 612,22284
-(defgroup prover-config 622,22425
-(defcustom proof-guess-command-line 664,23736
-(defcustom proof-assistant-home-page 679,24231
-(defcustom proof-context-command 685,24401
-(defcustom proof-info-command 690,24535
-(defcustom proof-showproof-command 697,24806
-(defcustom proof-goal-command 702,24942
-(defcustom proof-save-command 710,25239
-(defcustom proof-find-theorems-command 718,25548
-(defcustom proof-assistant-true-value 725,25858
-(defcustom proof-assistant-false-value 731,26048
-(defcustom proof-assistant-format-int-fn 737,26242
-(defcustom proof-assistant-format-string-fn 744,26491
-(defcustom proof-assistant-setting-format 751,26758
-(defgroup proof-script 773,27453
-(defcustom proof-terminal-char 778,27583
-(defcustom proof-script-sexp-commands 788,27970
-(defcustom proof-script-command-end-regexp 799,28427
-(defcustom proof-script-command-start-regexp 817,29246
-(defcustom proof-script-use-old-parser 828,29707
-(defcustom proof-script-integral-proofs 840,30193
-(defcustom proof-script-fly-past-comments 855,30849
-(defcustom proof-script-parse-function 860,31020
-(defcustom proof-script-comment-start 878,31663
-(defcustom proof-script-comment-start-regexp 889,32100
-(defcustom proof-script-comment-end 897,32417
-(defcustom proof-script-comment-end-regexp 909,32839
-(defcustom pg-insert-output-as-comment-fn 917,33150
-(defcustom proof-string-start-regexp 923,33402
-(defcustom proof-string-end-regexp 928,33567
-(defcustom proof-case-fold-search 933,33728
-(defcustom proof-save-command-regexp 942,34138
-(defcustom proof-save-with-hole-regexp 947,34248
-(defcustom proof-save-with-hole-result 959,34702
-(defcustom proof-goal-command-regexp 969,35153
-(defcustom proof-goal-with-hole-regexp 978,35541
-(defcustom proof-goal-with-hole-result 990,35982
-(defcustom proof-non-undoables-regexp 999,36369
-(defcustom proof-nested-undo-regexp 1010,36824
-(defcustom proof-ignore-for-undo-count 1026,37536
-(defcustom proof-script-next-entity-regexps 1034,37839
-(defcustom proof-script-find-next-entity-fn1078,39574
-(defcustom proof-script-imenu-generic-expression 1098,40412
-(defcustom proof-goal-command-p 1116,41265
-(defcustom proof-really-save-command-p 1143,42702
-(defcustom proof-completed-proof-behaviour 1155,43164
-(defcustom proof-count-undos-fn 1183,44520
-(defconst proof-no-command 1195,45069
-(defcustom proof-find-and-forget-fn 1200,45274
-(defcustom proof-forget-id-command 1217,45986
-(defcustom pg-topterm-goalhyplit-fn 1227,46344
-(defcustom proof-kill-goal-command 1239,46879
-(defcustom proof-undo-n-times-cmd 1253,47380
-(defcustom proof-nested-goals-history-p 1267,47928
-(defcustom proof-state-preserving-p 1276,48265
-(defcustom proof-activate-scripting-hook 1286,48735
-(defcustom proof-deactivate-scripting-hook 1305,49514
-(defcustom proof-indent 1318,49879
-(defcustom proof-indent-hang 1323,49986
-(defcustom proof-indent-enclose-offset 1328,50112
-(defcustom proof-indent-open-offset 1333,50254
-(defcustom proof-indent-close-offset 1338,50391
-(defcustom proof-indent-any-regexp 1343,50529
-(defcustom proof-indent-inner-regexp 1348,50689
-(defcustom proof-indent-enclose-regexp 1353,50843
-(defcustom proof-indent-open-regexp 1358,50997
-(defcustom proof-indent-close-regexp 1363,51149
-(defcustom proof-script-font-lock-keywords 1369,51303
-(defcustom proof-script-syntax-table-entries 1377,51632
-(defcustom proof-script-span-context-menu-extensions 1395,52029
-(defgroup proof-shell 1421,52789
-(defcustom proof-prog-name 1431,52960
-(defcustom proof-shell-auto-terminate-commands 1442,53378
-(defcustom proof-shell-pre-sync-init-cmd 1451,53775
-(defcustom proof-shell-init-cmd 1465,54333
-(defcustom proof-shell-restart-cmd 1476,54802
-(defcustom proof-shell-quit-cmd 1481,54957
-(defcustom proof-shell-quit-timeout 1486,55124
-(defcustom proof-shell-cd-cmd 1496,55572
-(defcustom proof-shell-start-silent-cmd 1513,56237
-(defcustom proof-shell-stop-silent-cmd 1522,56611
-(defcustom proof-shell-silent-threshold 1531,56944
-(defcustom  proof-shell-inform-file-processed-cmd 1539,57278
-(defcustom  proof-shell-inform-file-retracted-cmd 1560,58200
-(defcustom proof-auto-multiple-files 1588,59466
-(defcustom proof-cannot-reopen-processed-files 1603,60187
-(defcustom proof-shell-require-command-regexp 1617,60853
-(defcustom proof-done-advancing-require-function 1628,61315
-(defcustom proof-shell-quiet-errors 1634,61550
-(defcustom proof-shell-prompt-pattern 1647,61884
-(defcustom proof-shell-wakeup-char 1657,62305
-(defcustom proof-shell-annotated-prompt-regexp 1663,62536
-(defcustom proof-shell-abort-goal-regexp 1679,63170
-(defcustom proof-shell-error-regexp 1684,63305
-(defcustom proof-shell-truncate-before-error 1704,64099
-(defcustom pg-next-error-regexp 1718,64642
-(defcustom pg-next-error-filename-regexp 1733,65251
-(defcustom pg-next-error-extract-filename 1757,66284
-(defcustom proof-shell-interrupt-regexp 1764,66527
-(defcustom proof-shell-proof-completed-regexp 1778,67118
-(defcustom proof-shell-clear-response-regexp 1791,67626
-(defcustom proof-shell-clear-goals-regexp 1798,67925
-(defcustom proof-shell-start-goals-regexp 1805,68218
-(defcustom proof-shell-end-goals-regexp 1813,68585
-(defcustom proof-shell-eager-annotation-start 1819,68827
-(defcustom proof-shell-eager-annotation-start-length 1842,69847
-(defcustom proof-shell-eager-annotation-end 1853,70273
-(defcustom proof-shell-assumption-regexp 1869,70948
-(defcustom proof-shell-process-file 1879,71351
-(defcustom proof-shell-retract-files-regexp 1901,72307
-(defcustom proof-shell-compute-new-files-list 1910,72643
-(defcustom pg-use-specials-for-fontify 1922,73191
-(defcustom pg-special-char-regexp 1930,73539
-(defcustom proof-shell-set-elisp-variable-regexp 1936,73684
-(defcustom proof-shell-match-pgip-cmd 1969,75195
-(defcustom proof-shell-issue-pgip-cmd 1978,75524
-(defcustom proof-shell-query-dependencies-cmd 1987,75880
-(defcustom proof-shell-theorem-dependency-list-regexp 1994,76140
-(defcustom proof-shell-theorem-dependency-list-split 2010,76800
-(defcustom proof-shell-show-dependency-cmd 2019,77223
-(defcustom proof-shell-identifier-under-mouse-cmd 2026,77492
-(defcustom proof-shell-trace-output-regexp 2049,78573
-(defcustom proof-shell-thms-output-regexp 2063,79031
-(defcustom proof-shell-unicode 2076,79417
-(defcustom proof-shell-filename-escapes 2084,79737
-(defcustom proof-shell-process-connection-type2101,80417
-(defcustom proof-shell-strip-crs-from-input 2124,81463
-(defcustom proof-shell-strip-crs-from-output 2136,81948
-(defcustom proof-shell-insert-hook 2144,82316
-(defcustom proof-shell-handle-delayed-output-hook2184,84273
-(defcustom proof-shell-handle-error-or-interrupt-hook2190,84488
-(defcustom proof-shell-pre-interrupt-hook2208,85237
-(defcustom proof-shell-process-output-system-specific 2216,85509
-(defcustom proof-state-change-hook 2235,86373
-(defcustom proof-shell-font-lock-keywords 2246,86755
-(defcustom proof-shell-syntax-table-entries 2254,87087
-(defgroup proof-goals 2272,87459
-(defcustom pg-subterm-first-special-char 2277,87580
-(defcustom pg-subterm-anns-use-stack 2285,87892
-(defcustom pg-goals-change-goal 2294,88191
-(defcustom pbp-goal-command 2299,88307
-(defcustom pbp-hyp-command 2304,88463
-(defcustom pg-subterm-help-cmd 2309,88625
-(defcustom pg-goals-error-regexp 2316,88861
-(defcustom proof-shell-result-start 2321,89021
-(defcustom proof-shell-result-end 2327,89255
-(defcustom pg-subterm-start-char 2333,89468
-(defcustom pg-subterm-sep-char 2347,90048
-(defcustom pg-subterm-end-char 2353,90227
-(defcustom pg-topterm-regexp 2359,90384
-(defcustom proof-goals-font-lock-keywords 2376,90986
-(defcustom proof-resp-font-lock-keywords 2390,91671
-(defcustom pg-before-fontify-output-hook 2402,92251
-(defcustom pg-after-fontify-output-hook 2410,92611
-(defgroup proof-x-symbol 2422,92891
-(defcustom proof-xsym-extra-modes 2427,93019
-(defcustom proof-xsym-font-lock-keywords 2440,93647
-(defcustom proof-xsym-activate-command 2448,94024
-(defcustom proof-xsym-deactivate-command 2455,94259
-(defcustom proof-general-name 2472,94544
-(defcustom proof-general-home-page2477,94701
-(defcustom proof-unnamed-theorem-name2483,94861
-(defcustom proof-universal-keys2489,95045
+(defcustom proof-one-command-per-line268,10149
+(defcustom proof-prog-name-ask275,10376
+(defcustom proof-prog-name-guess281,10536
+(defcustom proof-tidy-response289,10795
+(defcustom proof-keep-response-history303,11258
+(defcustom pg-input-ring-size 313,11646
+(defcustom proof-general-debug 318,11798
+(defcustom proof-experimental-features327,12169
+(defcustom proof-follow-mode 349,13079
+(defcustom proof-auto-action-when-deactivating-scripting 373,14259
+(defcustom proof-script-command-separator 396,15208
+(defcustom proof-rsh-command 404,15500
+(defcustom proof-disappearing-proofs 420,16050
+(defgroup proof-faces 447,16696
+(defconst pg-defface-window-systems 452,16802
+(defmacro proof-face-specs 464,17319
+(defface proof-queue-face480,17839
+(defface proof-locked-face488,18117
+(defface proof-declaration-name-face501,18620
+(defface proof-tacticals-name-face510,18906
+(defface proof-tactics-name-face519,19168
+(defface proof-error-face528,19433
+(defface proof-warning-face536,19639
+(defface proof-eager-annotation-face545,19896
+(defface proof-debug-message-face553,20114
+(defface proof-boring-face561,20313
+(defface proof-mouse-highlight-face569,20505
+(defface proof-highlight-dependent-face577,20701
+(defface proof-highlight-dependency-face585,20910
+(defface proof-active-area-face593,21107
+(defconst proof-face-compat-doc 603,21400
+(defconst proof-queue-face 604,21480
+(defconst proof-locked-face 605,21548
+(defconst proof-declaration-name-face 606,21618
+(defconst proof-tacticals-name-face 607,21708
+(defconst proof-tactics-name-face 608,21794
+(defconst proof-error-face 609,21876
+(defconst proof-warning-face 610,21944
+(defconst proof-eager-annotation-face 611,22016
+(defconst proof-debug-message-face 612,22106
+(defconst proof-boring-face 613,22190
+(defconst proof-mouse-highlight-face 614,22260
+(defconst proof-highlight-dependent-face 615,22348
+(defconst proof-highlight-dependency-face 616,22444
+(defconst proof-active-area-face 617,22542
+(defgroup prover-config 627,22683
+(defcustom proof-guess-command-line 669,23994
+(defcustom proof-assistant-home-page 684,24489
+(defcustom proof-context-command 690,24659
+(defcustom proof-info-command 695,24793
+(defcustom proof-showproof-command 702,25064
+(defcustom proof-goal-command 707,25200
+(defcustom proof-save-command 715,25497
+(defcustom proof-find-theorems-command 723,25806
+(defcustom proof-assistant-true-value 730,26116
+(defcustom proof-assistant-false-value 736,26306
+(defcustom proof-assistant-format-int-fn 742,26500
+(defcustom proof-assistant-format-string-fn 749,26749
+(defcustom proof-assistant-setting-format 756,27016
+(defgroup proof-script 778,27711
+(defcustom proof-terminal-char 783,27841
+(defcustom proof-script-sexp-commands 793,28228
+(defcustom proof-script-command-end-regexp 804,28685
+(defcustom proof-script-command-start-regexp 822,29504
+(defcustom proof-script-use-old-parser 833,29965
+(defcustom proof-script-integral-proofs 845,30451
+(defcustom proof-script-fly-past-comments 860,31107
+(defcustom proof-script-parse-function 865,31278
+(defcustom proof-script-comment-start 883,31921
+(defcustom proof-script-comment-start-regexp 894,32358
+(defcustom proof-script-comment-end 902,32675
+(defcustom proof-script-comment-end-regexp 914,33097
+(defcustom pg-insert-output-as-comment-fn 922,33408
+(defcustom proof-string-start-regexp 928,33660
+(defcustom proof-string-end-regexp 933,33825
+(defcustom proof-case-fold-search 938,33986
+(defcustom proof-save-command-regexp 947,34396
+(defcustom proof-save-with-hole-regexp 952,34506
+(defcustom proof-save-with-hole-result 964,34960
+(defcustom proof-goal-command-regexp 974,35411
+(defcustom proof-goal-with-hole-regexp 983,35799
+(defcustom proof-goal-with-hole-result 995,36240
+(defcustom proof-non-undoables-regexp 1004,36627
+(defcustom proof-nested-undo-regexp 1015,37082
+(defcustom proof-ignore-for-undo-count 1031,37794
+(defcustom proof-script-next-entity-regexps 1039,38097
+(defcustom proof-script-find-next-entity-fn1083,39832
+(defcustom proof-script-imenu-generic-expression 1103,40670
+(defcustom proof-goal-command-p 1121,41523
+(defcustom proof-really-save-command-p 1148,42960
+(defcustom proof-completed-proof-behaviour 1160,43422
+(defcustom proof-count-undos-fn 1188,44778
+(defconst proof-no-command 1200,45327
+(defcustom proof-find-and-forget-fn 1205,45532
+(defcustom proof-forget-id-command 1222,46244
+(defcustom pg-topterm-goalhyplit-fn 1232,46602
+(defcustom proof-kill-goal-command 1244,47137
+(defcustom proof-undo-n-times-cmd 1258,47638
+(defcustom proof-nested-goals-history-p 1272,48186
+(defcustom proof-state-preserving-p 1281,48523
+(defcustom proof-activate-scripting-hook 1291,48993
+(defcustom proof-deactivate-scripting-hook 1310,49772
+(defcustom proof-indent 1323,50137
+(defcustom proof-indent-hang 1328,50244
+(defcustom proof-indent-enclose-offset 1333,50370
+(defcustom proof-indent-open-offset 1338,50512
+(defcustom proof-indent-close-offset 1343,50649
+(defcustom proof-indent-any-regexp 1348,50787
+(defcustom proof-indent-inner-regexp 1353,50947
+(defcustom proof-indent-enclose-regexp 1358,51101
+(defcustom proof-indent-open-regexp 1363,51255
+(defcustom proof-indent-close-regexp 1368,51407
+(defcustom proof-script-font-lock-keywords 1374,51561
+(defcustom proof-script-syntax-table-entries 1382,51890
+(defcustom proof-script-span-context-menu-extensions 1400,52287
+(defgroup proof-shell 1426,53047
+(defcustom proof-prog-name 1436,53218
+(defcustom proof-shell-auto-terminate-commands 1447,53636
+(defcustom proof-shell-pre-sync-init-cmd 1456,54033
+(defcustom proof-shell-init-cmd 1470,54591
+(defcustom proof-shell-restart-cmd 1481,55060
+(defcustom proof-shell-quit-cmd 1486,55215
+(defcustom proof-shell-quit-timeout 1491,55382
+(defcustom proof-shell-cd-cmd 1501,55830
+(defcustom proof-shell-start-silent-cmd 1518,56495
+(defcustom proof-shell-stop-silent-cmd 1527,56869
+(defcustom proof-shell-silent-threshold 1536,57202
+(defcustom  proof-shell-inform-file-processed-cmd 1544,57536
+(defcustom  proof-shell-inform-file-retracted-cmd 1565,58458
+(defcustom proof-auto-multiple-files 1593,59724
+(defcustom proof-cannot-reopen-processed-files 1608,60445
+(defcustom proof-shell-require-command-regexp 1622,61111
+(defcustom proof-done-advancing-require-function 1633,61573
+(defcustom proof-shell-quiet-errors 1639,61808
+(defcustom proof-shell-prompt-pattern 1652,62142
+(defcustom proof-shell-wakeup-char 1662,62563
+(defcustom proof-shell-annotated-prompt-regexp 1668,62794
+(defcustom proof-shell-abort-goal-regexp 1684,63428
+(defcustom proof-shell-error-regexp 1689,63563
+(defcustom proof-shell-truncate-before-error 1709,64357
+(defcustom pg-next-error-regexp 1723,64900
+(defcustom pg-next-error-filename-regexp 1738,65509
+(defcustom pg-next-error-extract-filename 1762,66542
+(defcustom proof-shell-interrupt-regexp 1769,66785
+(defcustom proof-shell-proof-completed-regexp 1783,67376
+(defcustom proof-shell-clear-response-regexp 1796,67884
+(defcustom proof-shell-clear-goals-regexp 1803,68183
+(defcustom proof-shell-start-goals-regexp 1810,68476
+(defcustom proof-shell-end-goals-regexp 1818,68843
+(defcustom proof-shell-eager-annotation-start 1824,69085
+(defcustom proof-shell-eager-annotation-start-length 1847,70105
+(defcustom proof-shell-eager-annotation-end 1858,70531
+(defcustom proof-shell-assumption-regexp 1874,71206
+(defcustom proof-shell-process-file 1884,71609
+(defcustom proof-shell-retract-files-regexp 1906,72565
+(defcustom proof-shell-compute-new-files-list 1915,72901
+(defcustom pg-use-specials-for-fontify 1927,73449
+(defcustom pg-special-char-regexp 1935,73797
+(defcustom proof-shell-set-elisp-variable-regexp 1941,73942
+(defcustom proof-shell-match-pgip-cmd 1974,75453
+(defcustom proof-shell-issue-pgip-cmd 1983,75782
+(defcustom proof-shell-query-dependencies-cmd 1992,76138
+(defcustom proof-shell-theorem-dependency-list-regexp 1999,76398
+(defcustom proof-shell-theorem-dependency-list-split 2015,77058
+(defcustom proof-shell-show-dependency-cmd 2024,77481
+(defcustom proof-shell-identifier-under-mouse-cmd 2031,77750
+(defcustom proof-shell-trace-output-regexp 2054,78831
+(defcustom proof-shell-thms-output-regexp 2068,79289
+(defcustom proof-shell-unicode 2081,79675
+(defcustom proof-shell-filename-escapes 2089,79995
+(defcustom proof-shell-process-connection-type2106,80675
+(defcustom proof-shell-strip-crs-from-input 2129,81721
+(defcustom proof-shell-strip-crs-from-output 2141,82206
+(defcustom proof-shell-insert-hook 2149,82574
+(defcustom proof-shell-handle-delayed-output-hook2189,84531
+(defcustom proof-shell-handle-error-or-interrupt-hook2195,84746
+(defcustom proof-shell-pre-interrupt-hook2213,85495
+(defcustom proof-shell-process-output-system-specific 2221,85767
+(defcustom proof-state-change-hook 2240,86631
+(defcustom proof-shell-font-lock-keywords 2251,87013
+(defcustom proof-shell-syntax-table-entries 2259,87345
+(defgroup proof-goals 2277,87717
+(defcustom pg-subterm-first-special-char 2282,87838
+(defcustom pg-subterm-anns-use-stack 2290,88150
+(defcustom pg-goals-change-goal 2299,88449
+(defcustom pbp-goal-command 2304,88565
+(defcustom pbp-hyp-command 2309,88721
+(defcustom pg-subterm-help-cmd 2314,88883
+(defcustom pg-goals-error-regexp 2321,89119
+(defcustom proof-shell-result-start 2326,89279
+(defcustom proof-shell-result-end 2332,89513
+(defcustom pg-subterm-start-char 2338,89726
+(defcustom pg-subterm-sep-char 2352,90306
+(defcustom pg-subterm-end-char 2358,90485
+(defcustom pg-topterm-regexp 2364,90642
+(defcustom proof-goals-font-lock-keywords 2381,91244
+(defcustom proof-resp-font-lock-keywords 2395,91929
+(defcustom pg-before-fontify-output-hook 2407,92509
+(defcustom pg-after-fontify-output-hook 2415,92869
+(defgroup proof-x-symbol 2427,93149
+(defcustom proof-xsym-extra-modes 2432,93277
+(defcustom proof-xsym-font-lock-keywords 2445,93905
+(defcustom proof-xsym-activate-command 2453,94282
+(defcustom proof-xsym-deactivate-command 2460,94517
+(defcustom proof-general-name 2477,94802
+(defcustom proof-general-home-page2482,94959
+(defcustom proof-unnamed-theorem-name2488,95119
+(defcustom proof-universal-keys2494,95303
 
 generic/proof-depends.el,824
-(defvar proof-thm-names-of-files 19,540
-(defvar proof-def-names-of-files 25,824
-(defun proof-depends-module-name-for-buffer 34,1128
-(defun proof-depends-module-of 44,1570
-(defun proof-depends-names-in-same-file 52,1864
-(defun proof-depends-process-dependencies 71,2484
-(defun proof-dependency-in-span-context-menu 124,4231
-(defun proof-dep-alldeps-menu 147,5134
-(defun proof-dep-make-alldeps-menu 153,5361
-(defun proof-dep-split-deps 171,5857
-(defun proof-dep-make-submenu 192,6556
-(defun proof-make-highlight-depts-menu 202,6909
-(defun proof-goto-dependency 212,7213
-(defun proof-show-dependency 218,7436
-(defconst pg-dep-span-priority 225,7726
-(defconst pg-ordinary-span-priority 226,7762
-(defun proof-highlight-depcs 228,7804
-(defun proof-highlight-depts 238,8234
-(defun proof-dep-unhighlight 249,8708
+(defvar proof-thm-names-of-files 23,624
+(defvar proof-def-names-of-files 29,908
+(defun proof-depends-module-name-for-buffer 38,1212
+(defun proof-depends-module-of 48,1654
+(defun proof-depends-names-in-same-file 56,1948
+(defun proof-depends-process-dependencies 75,2568
+(defun proof-dependency-in-span-context-menu 128,4317
+(defun proof-dep-alldeps-menu 151,5220
+(defun proof-dep-make-alldeps-menu 157,5447
+(defun proof-dep-split-deps 175,5943
+(defun proof-dep-make-submenu 196,6642
+(defun proof-make-highlight-depts-menu 206,6995
+(defun proof-goto-dependency 216,7299
+(defun proof-show-dependency 222,7522
+(defconst pg-dep-span-priority 229,7812
+(defconst pg-ordinary-span-priority 230,7848
+(defun proof-highlight-depcs 232,7890
+(defun proof-highlight-depts 242,8320
+(defun proof-dep-unhighlight 253,8794
 
 generic/proof-easy-config.el,192
-(defconst proof-easy-config-derived-modes-table14,475
-(defun proof-easy-config-define-derived-modes 21,881
-(defun proof-easy-config-check-setup 54,2291
-(defmacro proof-easy-config 86,3616
-
-generic/proof-indent.el,218
-(defun proof-indent-indent 9,226
-(defun proof-indent-offset 18,492
-(defun proof-indent-inner-p 35,1092
-(defun proof-indent-goto-prev 44,1399
-(defun proof-indent-calculate 51,1732
-(defun proof-indent-line 70,2448
+(defconst proof-easy-config-derived-modes-table16,543
+(defun proof-easy-config-define-derived-modes 23,949
+(defun proof-easy-config-check-setup 56,2359
+(defmacro proof-easy-config 88,3694
+
+generic/proof-indent.el,219
+(defun proof-indent-indent 14,411
+(defun proof-indent-offset 23,677
+(defun proof-indent-inner-p 40,1277
+(defun proof-indent-goto-prev 49,1584
+(defun proof-indent-calculate 56,1917
+(defun proof-indent-line 75,2633
 
 generic/proof-maths-menu.el,134
-(defun proof-maths-menu-support-available 26,854
-(defun proof-maths-menu-set-global 37,1283
-(defun proof-maths-menu-enable 51,1739
-
-generic/proof-menu.el,2146
-(defvar proof-display-some-buffers-count 19,521
-(defun proof-display-some-buffers 21,566
-(defun proof-menu-define-keys 80,2768
-(defun proof-menu-define-main 143,5787
-(defun proof-menu-define-specific 153,5990
-(defun proof-assistant-menu-update 191,7016
-(defvar proof-help-menu207,7599
-(defvar proof-show-hide-menu215,7877
-(defvar proof-buffer-menu224,8190
-(defun proof-keep-response-history 282,10333
-(defconst proof-quick-opts-menu290,10643
-(defun proof-quick-opts-vars 417,15708
-(defun proof-quick-opts-changed-from-defaults-p 442,16459
-(defun proof-quick-opts-changed-from-saved-p 446,16564
-(defun proof-quick-opts-save 457,16916
-(defun proof-quick-opts-reset 462,17084
-(defconst proof-config-menu474,17352
-(defconst proof-advanced-menu481,17531
-(defvar proof-menu 494,17966
-(defun proof-main-menu 503,18250
-(defun proof-aux-menu 514,18516
-(defvar proof-menu-favourites 530,18863
-(defun proof-menu-define-favourites-menu 533,18970
-(defun proof-def-favourite 553,19626
-(defvar proof-make-favourite-cmd-history 576,20601
-(defvar proof-make-favourite-menu-history 579,20686
-(defun proof-save-favourites 582,20772
-(defun proof-del-favourite 587,20920
-(defun proof-read-favourite 604,21481
-(defun proof-add-favourite 629,22284
-(defvar proof-assistant-settings 656,23335
-(defvar proof-menu-settings 663,23698
-(defun proof-menu-define-settings-menu 666,23772
-(defun proof-menu-entry-name 686,24516
-(defun proof-menu-entry-for-setting 698,24988
-(defun proof-settings-vars 716,25478
-(defun proof-settings-changed-from-defaults-p 721,25655
-(defun proof-settings-changed-from-saved-p 725,25761
-(defun proof-settings-save 729,25864
-(defun proof-settings-reset 734,26031
-(defun proof-defpacustom-fn 741,26276
-(defmacro defpacustom 817,29160
-(defun proof-assistant-invisible-command-ifposs 832,29987
-(defun proof-maybe-askprefs 854,30962
-(defun proof-assistant-settings-cmd 861,31166
-(defun proof-assistant-format 878,31826
-(defvar proof-assistant-format-table 902,32885
-(defun proof-assistant-format-bool 910,33254
-(defun proof-assistant-format-int 913,33367
-(defun proof-assistant-format-string 916,33459
+(defun proof-maths-menu-support-available 30,959
+(defun proof-maths-menu-set-global 41,1388
+(defun proof-maths-menu-enable 55,1844
+
+generic/proof-menu.el,2101
+(defvar proof-display-some-buffers-count 17,438
+(defun proof-display-some-buffers 19,483
+(defun proof-menu-define-keys 78,2685
+(defun proof-menu-define-main 141,5721
+(defvar proof-menu-favourites 150,5909
+(defun proof-menu-define-specific 154,6031
+(defun proof-assistant-menu-update 192,7057
+(defvar proof-help-menu208,7640
+(defvar proof-show-hide-menu216,7918
+(defvar proof-buffer-menu225,8231
+(defun proof-keep-response-history 283,10374
+(defconst proof-quick-opts-menu291,10684
+(defun proof-quick-opts-vars 418,15749
+(defun proof-quick-opts-changed-from-defaults-p 443,16500
+(defun proof-quick-opts-changed-from-saved-p 447,16605
+(defun proof-quick-opts-save 458,16957
+(defun proof-quick-opts-reset 463,17125
+(defconst proof-config-menu475,17393
+(defconst proof-advanced-menu482,17572
+(defvar proof-menu 495,18007
+(defun proof-main-menu 504,18291
+(defun proof-aux-menu 515,18557
+(defun proof-menu-define-favourites-menu 531,18904
+(defun proof-def-favourite 551,19560
+(defvar proof-make-favourite-cmd-history 574,20535
+(defvar proof-make-favourite-menu-history 577,20620
+(defun proof-save-favourites 580,20706
+(defun proof-del-favourite 585,20854
+(defun proof-read-favourite 602,21415
+(defun proof-add-favourite 627,22218
+(defvar proof-menu-settings 654,23269
+(defun proof-menu-define-settings-menu 657,23343
+(defun proof-menu-entry-name 677,24087
+(defun proof-menu-entry-for-setting 689,24559
+(defun proof-settings-vars 707,25049
+(defun proof-settings-changed-from-defaults-p 712,25226
+(defun proof-settings-changed-from-saved-p 716,25332
+(defun proof-settings-save 720,25435
+(defun proof-settings-reset 725,25602
+(defun proof-defpacustom-fn 732,25847
+(defmacro defpacustom 808,28731
+(defun proof-assistant-invisible-command-ifposs 823,29558
+(defun proof-maybe-askprefs 845,30533
+(defun proof-assistant-settings-cmd 852,30737
+(defvar proof-assistant-format-table 869,31397
+(defun proof-assistant-format-bool 877,31766
+(defun proof-assistant-format-int 880,31879
+(defun proof-assistant-format-string 883,31971
+(defun proof-assistant-format 886,32069
 
 generic/proof-mmm.el,114
-(defun proof-mmm-support-available 30,1031
-(defun proof-mmm-set-global 54,1879
-(defun proof-mmm-enable 69,2420
-
-generic/proof-script.el,5103
-(defvar proof-last-theorem-dependencies 33,848
-(defvar proof-nesting-depth 37,1010
-(defvar proof-element-counters 44,1241
-(deflocal proof-active-buffer-fake-minor-mode 50,1381
-(deflocal proof-script-buffer-file-name 53,1507
-(defun proof-next-element-count 67,2031
-(defun proof-element-id 76,2358
-(defun proof-next-element-id 80,2527
-(deflocal proof-script-last-entity 94,2844
-(defun proof-script-find-next-entity 101,3124
-(deflocal proof-locked-span 177,5866
-(deflocal proof-queue-span 184,6132
-(defun proof-span-read-only 196,6646
-(defun proof-strict-read-only 203,6903
-(defsubst proof-set-queue-endpoints 218,7573
-(defsubst proof-set-locked-endpoints 222,7714
-(defsubst proof-detach-queue 226,7858
-(defsubst proof-detach-locked 230,7990
-(defsubst proof-set-queue-start 234,8126
-(defsubst proof-set-locked-end 238,8252
-(defsubst proof-set-queue-end 253,8831
-(defun proof-init-segmentation 263,9087
-(defun proof-restart-buffers 295,10458
-(defun proof-script-buffers-with-spans 317,11390
-(defun proof-script-remove-all-spans-and-deactivate 327,11746
-(defun proof-script-clear-queue-spans 331,11934
-(defun proof-unprocessed-begin 349,12480
-(defun proof-script-end 357,12734
-(defun proof-queue-or-locked-end 366,13035
-(defun proof-locked-end 380,13698
-(defun proof-locked-region-full-p 396,14068
-(defun proof-locked-region-empty-p 404,14325
-(defun proof-only-whitespace-to-locked-region-p 408,14475
-(defun proof-in-locked-region-p 421,15111
-(defun proof-goto-end-of-locked 433,15374
-(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 450,16133
-(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 461,16614
-(defun proof-end-of-locked-visible-p 475,17267
-(defun proof-goto-end-of-queue-or-locked-if-not-visible 484,17718
-(defvar pg-idioms 503,18368
-(defvar pg-visibility-specs 506,18464
-(deflocal pg-script-portions 511,18671
-(defun pg-clear-script-portions 514,18793
-(defun pg-add-script-element 528,19322
-(defun pg-remove-script-element 531,19398
-(defsubst pg-visname 539,19676
-(defun pg-add-element 543,19821
-(defun pg-open-invisible-span 577,21450
-(defun pg-remove-element 588,21813
-(defun pg-make-element-invisible 595,22083
-(defun pg-make-element-visible 601,22340
-(defun pg-toggle-element-visibility 606,22519
-(defun pg-redisplay-for-gnuemacs 614,22849
-(defun pg-show-all-portions 621,23120
-(defun pg-show-all-proofs 639,23791
-(defun pg-hide-all-proofs 644,23919
-(defun pg-add-proof-element 649,24050
-(defun pg-span-name 663,24670
-(defun pg-set-span-helphighlights 684,25377
-(defun proof-complete-buffer-atomic 709,26201
-(defun proof-register-possibly-new-processed-file 750,28116
-(defun proof-inform-prover-file-retracted 801,30244
-(defun proof-auto-retract-dependencies 820,31030
-(defun proof-unregister-buffer-file-name 874,33570
-(defun proof-protected-process-or-retract 920,35393
-(defun proof-deactivate-scripting-auto 947,36563
-(defun proof-deactivate-scripting 956,36921
-(defun proof-activate-scripting 1093,42326
-(defun proof-toggle-active-scripting 1221,48080
-(defun proof-done-advancing 1262,49441
-(defun proof-done-advancing-comment 1348,52808
-(defun proof-done-advancing-save 1367,53550
-(defun proof-make-goalsave 1460,57165
-(defun proof-get-name-from-goal 1475,57908
-(defun proof-done-advancing-autosave 1494,58934
-(defun proof-done-advancing-other 1559,61480
-(defun proof-segment-up-to-parser 1587,62439
-(defun proof-script-generic-parse-find-comment-end 1650,64515
-(defun proof-script-generic-parse-cmdend 1659,64931
-(defun proof-script-generic-parse-cmdstart 1684,65826
-(defun proof-script-generic-parse-sexp 1747,68534
-(defun proof-cmdstart-add-segment-for-cmd 1771,69470
-(defun proof-segment-up-to-cmdstart 1823,71669
-(defun proof-segment-up-to-cmdend 1884,74029
-(defun proof-semis-to-vanillas 1955,76676
-(defun proof-script-new-command-advance 1994,78002
-(defun proof-script-next-command-advance 2036,79743
-(defun proof-assert-until-point-interactive 2048,80184
-(defun proof-assert-until-point 2074,81306
-(defun proof-assert-next-command2127,83738
-(defun proof-goto-point 2175,86001
-(defun proof-insert-pbp-command 2193,86542
-(defun proof-done-retracting 2226,87655
-(defun proof-setup-retract-action 2253,88776
-(defun proof-last-goal-or-goalsave 2263,89259
-(defun proof-retract-target 2286,90099
-(defun proof-retract-until-point-interactive 2371,93740
-(defun proof-retract-until-point 2379,94125
-(define-derived-mode proof-mode 2422,95874
-(defun proof-script-set-visited-file-name 2467,97635
-(defun proof-script-set-buffer-hooks 2491,98637
-(defun proof-script-kill-buffer-fn 2499,99055
-(defun proof-config-done-related 2543,100877
-(defun proof-generic-goal-command-p 2613,103355
-(defun proof-generic-state-preserving-p 2618,103567
-(defun proof-generic-count-undos 2627,104084
-(defun proof-generic-find-and-forget 2656,105114
-(defconst proof-script-important-settings2707,106939
-(defun proof-config-done 2722,107492
-(defun proof-setup-parsing-mechanism 2815,110895
-(defun proof-setup-imenu 2859,112748
-(defun proof-setup-func-menu 2876,113353
-
-generic/proof-shell.el,3356
+(defun proof-mmm-support-available 34,1131
+(defun proof-mmm-set-global 58,1979
+(defun proof-mmm-enable 73,2520
+
+generic/proof-script.el,5058
+(defvar proof-element-counters 28,719
+(deflocal proof-active-buffer-fake-minor-mode 34,859
+(deflocal proof-script-buffer-file-name 37,985
+(deflocal pg-script-portions 44,1395
+(defun proof-next-element-count 54,1631
+(defun proof-element-id 63,1958
+(defun proof-next-element-id 67,2127
+(deflocal proof-script-last-entity 81,2444
+(defun proof-script-find-next-entity 88,2724
+(deflocal proof-locked-span 164,5466
+(deflocal proof-queue-span 171,5732
+(defun proof-span-read-only 183,6246
+(defun proof-strict-read-only 190,6503
+(defsubst proof-set-queue-endpoints 205,7173
+(defsubst proof-set-locked-endpoints 209,7314
+(defsubst proof-detach-queue 213,7458
+(defsubst proof-detach-locked 217,7590
+(defsubst proof-set-queue-start 221,7726
+(defsubst proof-set-locked-end 225,7852
+(defsubst proof-set-queue-end 238,8356
+(defun proof-init-segmentation 249,8653
+(defun proof-restart-buffers 282,10048
+(defun proof-script-buffers-with-spans 304,10980
+(defun proof-script-remove-all-spans-and-deactivate 314,11336
+(defun proof-script-clear-queue-spans 318,11524
+(defun proof-unprocessed-begin 337,12085
+(defun proof-script-end 345,12339
+(defun proof-queue-or-locked-end 354,12640
+(defun proof-locked-end 369,13318
+(defun proof-locked-region-full-p 386,13703
+(defun proof-locked-region-empty-p 395,13975
+(defun proof-only-whitespace-to-locked-region-p 399,14125
+(defun proof-in-locked-region-p 412,14761
+(defun proof-goto-end-of-locked 424,15024
+(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 441,15783
+(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 452,16264
+(defun proof-end-of-locked-visible-p 466,16917
+(defun proof-goto-end-of-queue-or-locked-if-not-visible 475,17368
+(defvar pg-idioms 494,18018
+(defvar pg-visibility-specs 497,18114
+(defun pg-clear-script-portions 502,18321
+(defun pg-add-script-element 516,18850
+(defun pg-remove-script-element 519,18926
+(defsubst pg-visname 527,19204
+(defun pg-add-element 531,19349
+(defun pg-open-invisible-span 565,20978
+(defun pg-remove-element 576,21341
+(defun pg-make-element-invisible 583,21611
+(defun pg-make-element-visible 589,21868
+(defun pg-toggle-element-visibility 594,22047
+(defun pg-redisplay-for-gnuemacs 602,22377
+(defun pg-show-all-portions 609,22648
+(defun pg-show-all-proofs 627,23319
+(defun pg-hide-all-proofs 632,23447
+(defun pg-add-proof-element 637,23578
+(defun pg-span-name 651,24198
+(defvar pg-span-context-menu-keymap672,24905
+(defun pg-set-span-helphighlights 685,25276
+(defun proof-complete-buffer-atomic 713,26205
+(defun proof-register-possibly-new-processed-file 754,28120
+(defun proof-inform-prover-file-retracted 805,30248
+(defun proof-auto-retract-dependencies 824,31034
+(defun proof-unregister-buffer-file-name 878,33574
+(defun proof-protected-process-or-retract 924,35397
+(defun proof-deactivate-scripting-auto 951,36567
+(defun proof-deactivate-scripting 960,36925
+(defun proof-activate-scripting 1097,42330
+(defun proof-toggle-active-scripting 1219,47762
+(defun proof-done-advancing 1260,49123
+(defun proof-done-advancing-comment 1350,52631
+(defun proof-done-advancing-save 1369,53373
+(defun proof-make-goalsave 1462,56988
+(defun proof-get-name-from-goal 1477,57731
+(defun proof-done-advancing-autosave 1496,58757
+(defun proof-done-advancing-other 1561,61303
+(defun proof-segment-up-to-parser 1589,62262
+(defun proof-script-generic-parse-find-comment-end 1652,64338
+(defun proof-script-generic-parse-cmdend 1661,64754
+(defun proof-script-generic-parse-cmdstart 1686,65649
+(defun proof-script-generic-parse-sexp 1749,68357
+(defun proof-cmdstart-add-segment-for-cmd 1773,69293
+(defun proof-segment-up-to-cmdstart 1825,71492
+(defun proof-segment-up-to-cmdend 1886,73852
+(defun proof-semis-to-vanillas 1958,76517
+(defun proof-script-new-command-advance 1997,77843
+(defun proof-script-next-command-advance 2039,79584
+(defun proof-assert-until-point-interactive 2051,80025
+(defun proof-assert-until-point 2077,81147
+(defun proof-assert-next-command2130,83579
+(defun proof-goto-point 2178,85842
+(defun proof-insert-pbp-command 2196,86383
+(defun proof-done-retracting 2228,87483
+(defun proof-setup-retract-action 2263,88897
+(defun proof-last-goal-or-goalsave 2273,89380
+(defun proof-retract-target 2296,90220
+(defun proof-retract-until-point-interactive 2381,93861
+(defun proof-retract-until-point 2389,94246
+(define-derived-mode proof-mode 2432,95995
+(defun proof-script-set-visited-file-name 2477,97756
+(defun proof-script-set-buffer-hooks 2501,98758
+(defun proof-script-kill-buffer-fn 2509,99176
+(defun proof-config-done-related 2553,100998
+(defun proof-generic-goal-command-p 2623,103476
+(defun proof-generic-state-preserving-p 2628,103688
+(defun proof-generic-count-undos 2637,104205
+(defun proof-generic-find-and-forget 2666,105235
+(defconst proof-script-important-settings2717,107060
+(defun proof-config-done 2732,107613
+(defun proof-setup-parsing-mechanism 2823,110827
+(defun proof-setup-imenu 2867,112680
+(defun proof-setup-func-menu 2884,113285
+
+generic/proof-shell.el,3315
 (defvar proof-marker 28,643
 (defvar proof-action-list 31,740
 (defvar proof-shell-silent 39,916
@@ -1985,220 +2008,210 @@ generic/proof-shell.el,3356
 (defun proof-shell-filter 1437,54929
 (defun proof-shell-filter-process-output 1596,61518
 (defvar pg-last-tracing-output-time 1649,63572
-(defvar pg-tracing-slow-mode 1652,63678
-(defconst pg-slow-mode-duration 1655,63767
-(defconst pg-fast-tracing-mode-threshold 1658,63849
-(defvar pg-tracing-cleanup-timer 1661,63977
-(defun pg-tracing-tight-loop 1663,64016
-(defun pg-finish-tracing-display 1706,65734
-(defun proof-shell-dont-show-annotations 1719,66040
-(defun proof-shell-show-annotations 1735,66561
-(defun proof-shell-wait 1757,67088
-(defun proof-done-invisible 1777,67998
-(defun proof-shell-invisible-command 1820,69721
-(defun proof-shell-invisible-cmd-get-result 1854,70986
-(defun proof-shell-invisible-command-invisible-result 1872,71682
-(define-derived-mode proof-shell-mode 1891,72112
-(defconst proof-shell-important-settings1961,74778
-(defun proof-shell-config-done 1967,74893
+(defconst pg-slow-mode-duration 1652,63678
+(defconst pg-fast-tracing-mode-threshold 1655,63760
+(defvar pg-tracing-cleanup-timer 1658,63888
+(defun pg-tracing-tight-loop 1660,63927
+(defun pg-finish-tracing-display 1703,65645
+(defun proof-shell-dont-show-annotations 1716,65951
+(defun proof-shell-show-annotations 1732,66472
+(defun proof-shell-wait 1754,66999
+(defun proof-done-invisible 1774,67909
+(defun proof-shell-invisible-command 1817,69632
+(defun proof-shell-invisible-cmd-get-result 1851,70897
+(defun proof-shell-invisible-command-invisible-result 1869,71593
+(define-derived-mode proof-shell-mode 1888,72023
+(defconst proof-shell-important-settings1958,74689
+(defun proof-shell-config-done 1964,74804
 
 generic/proof-site.el,505
 (defconst proof-assistant-table-default23,728
-(defconst proof-general-short-version 80,2914
-(defconst proof-general-version-year 86,3102
-(defgroup proof-general 93,3255
-(defgroup proof-general-internals 98,3363
-(defun proof-home-directory-fn 111,3751
-(defcustom proof-home-directory122,4122
-(defcustom proof-images-directory131,4489
-(defcustom proof-info-directory137,4691
-(defcustom proof-assistant-table164,5837
-(defcustom proof-assistants 199,6953
-(defun proof-ready-for-assistant 227,8098
+(defconst proof-general-short-version 80,2911
+(defconst proof-general-version-year 86,3099
+(defgroup proof-general 93,3252
+(defgroup proof-general-internals 98,3360
+(defun proof-home-directory-fn 111,3748
+(defcustom proof-home-directory122,4119
+(defcustom proof-images-directory131,4486
+(defcustom proof-info-directory137,4688
+(defcustom proof-assistant-table164,5834
+(defcustom proof-assistants 199,6950
+(defun proof-ready-for-assistant 227,8095
 
 generic/proof-splash.el,726
-(defcustom proof-splash-enable 14,379
-(defcustom proof-splash-time 19,531
-(defcustom proof-splash-contents27,816
-(defconst proof-splash-startup-msg 53,1776
-(defconst proof-splash-welcome 62,2155
-(defun proof-get-image 81,2702
-(defvar proof-splash-timeout-conf 120,4053
-(defun proof-splash-centre-spaces 123,4166
-(defun proof-splash-remove-screen 151,5336
-(defun proof-splash-remove-buffer 171,6057
-(defvar proof-splash-seen 187,6721
-(defun proof-splash-display-screen 191,6838
-(defun proof-splash-message 266,9992
-(defun proof-splash-timeout-waiter 276,10353
-(defvar proof-splash-old-frame-title-format 292,11049
-(defun proof-splash-set-frame-titles 294,11099
-(defun proof-splash-unset-frame-titles 303,11415
+(defcustom proof-splash-enable 17,320
+(defcustom proof-splash-time 22,472
+(defcustom proof-splash-contents30,757
+(defconst proof-splash-startup-msg 58,1776
+(defconst proof-splash-welcome 67,2155
+(defun proof-get-image 86,2702
+(defvar proof-splash-timeout-conf 125,4053
+(defun proof-splash-centre-spaces 128,4166
+(defun proof-splash-remove-screen 156,5336
+(defun proof-splash-remove-buffer 176,6057
+(defvar proof-splash-seen 192,6721
+(defun proof-splash-display-screen 196,6838
+(defun proof-splash-message 271,9992
+(defun proof-splash-timeout-waiter 284,10436
+(defvar proof-splash-old-frame-title-format 300,11132
+(defun proof-splash-set-frame-titles 302,11182
+(defun proof-splash-unset-frame-titles 311,11498
 
 generic/proof-syntax.el,981
-(defun proof-ids-to-regexp 15,421
-(defun proof-anchor-regexp 21,677
-(defconst proof-no-regexp25,779
-(defun proof-regexp-alt 30,874
-(defun proof-regexp-region 39,1160
-(defun proof-re-search-forward-region 48,1583
-(defun proof-search-forward 61,2078
-(defun proof-replace-regexp-in-string 67,2330
-(defun proof-re-search-forward 73,2584
-(defun proof-re-search-backward 79,2845
-(defun proof-string-match 85,3109
-(defun proof-string-match-safe 91,3341
-(defun proof-stringfn-match 95,3546
-(defun proof-looking-at 102,3806
-(defun proof-looking-at-safe 108,3996
-(defun proof-looking-at-syntactic-context 112,4136
-(defsubst proof-replace-string 124,4499
-(defsubst proof-replace-regexp 129,4703
-(defsubst proof-replace-regexp-nocasefold 134,4912
-(defvar proof-id 142,5194
-(defun proof-ids 148,5414
-(defun proof-zap-commas 161,5975
-(defun proof-format 179,6544
-(defun proof-format-filename 198,7183
-(defun proof-insert 247,8661
-(defun proof-splice-separator 283,9670
+(defun proof-ids-to-regexp 17,530
+(defun proof-anchor-regexp 23,786
+(defconst proof-no-regexp27,888
+(defun proof-regexp-alt 32,983
+(defun proof-regexp-region 41,1269
+(defun proof-re-search-forward-region 50,1692
+(defun proof-search-forward 63,2187
+(defun proof-replace-regexp-in-string 69,2439
+(defun proof-re-search-forward 75,2693
+(defun proof-re-search-backward 81,2954
+(defun proof-string-match 87,3218
+(defun proof-string-match-safe 93,3450
+(defun proof-stringfn-match 97,3655
+(defun proof-looking-at 104,3915
+(defun proof-looking-at-safe 110,4105
+(defun proof-looking-at-syntactic-context 114,4245
+(defsubst proof-replace-string 126,4608
+(defsubst proof-replace-regexp 131,4812
+(defsubst proof-replace-regexp-nocasefold 136,5021
+(defvar proof-id 144,5303
+(defun proof-ids 150,5523
+(defun proof-zap-commas 163,6084
+(defun proof-format 181,6653
+(defun proof-format-filename 200,7292
+(defun proof-insert 249,8770
+(defun proof-splice-separator 286,9794
 
 generic/proof-toolbar.el,2874
-(defun proof-toolbar-function 37,1256
-(defun proof-toolbar-icon 40,1353
-(defun proof-toolbar-enabler 43,1454
-(defun proof-toolbar-function-with-enabler 46,1562
-(defun proof-toolbar-make-icon 53,1735
-(defun proof-toolbar-make-toolbar-item 71,2335
-(defvar proof-toolbar 110,3711
-(deflocal proof-toolbar-itimer 114,3840
-(defun proof-toolbar-setup 118,3950
-(defun proof-toolbar-build 161,5493
-(defalias 'proof-toolbar-enable proof-toolbar-enable
226,7691
-(defun proof-toolbar-setup-refresh 237,7995
-(defun proof-toolbar-disable-refresh 258,8765
-(deflocal proof-toolbar-refresh-flag 265,9087
-(defun proof-toolbar-refresh 271,9358
-(defvar proof-toolbar-enablers275,9503
-(defvar proof-toolbar-enablers-last-state281,9679
-(defun proof-toolbar-really-refresh 285,9770
-(defun proof-toolbar-undo-enable-p 338,11600
-(defalias 'proof-toolbar-undo proof-toolbar-undo
343,11748
-(defun proof-toolbar-delete-enable-p 349,11867
-(defalias 'proof-toolbar-delete proof-toolbar-delete
355,12041
-(defun proof-toolbar-lockedend-enable-p 362,12177
-(defalias 'proof-toolbar-lockedend proof-toolbar-lockedend
365,12227
-(defun proof-toolbar-next-enable-p 374,12315
-(defalias 'proof-toolbar-next proof-toolbar-next
378,12422
-(defun proof-toolbar-goto-enable-p 385,12516
-(defalias 'proof-toolbar-goto proof-toolbar-goto
388,12589
-(defun proof-toolbar-retract-enable-p 395,12665
-(defalias 'proof-toolbar-retract proof-toolbar-retract
399,12776
-(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p
406,12855
-(defalias 'proof-toolbar-use proof-toolbar-use
407,12923
-(defun proof-toolbar-restart-enable-p 413,13001
-(defalias 'proof-toolbar-restart proof-toolbar-restart
418,13162
-(defun proof-toolbar-goal-enable-p 424,13240
-(defalias 'proof-toolbar-goal proof-toolbar-goal
431,13473
-(defun proof-toolbar-qed-enable-p 438,13545
-(defalias 'proof-toolbar-qed proof-toolbar-qed
444,13697
-(defun proof-toolbar-state-enable-p 450,13769
-(defalias 'proof-toolbar-state proof-toolbar-state
453,13840
-(defun proof-toolbar-context-enable-p 459,13909
-(defalias 'proof-toolbar-context proof-toolbar-context
462,13982
-(defun proof-toolbar-info-enable-p 470,14142
-(defalias 'proof-toolbar-info proof-toolbar-info
473,14186
-(defun proof-toolbar-command-enable-p 479,14255
-(defalias 'proof-toolbar-command proof-toolbar-command
482,14326
-(defun proof-toolbar-help-enable-p 488,14406
-(defun proof-toolbar-help 491,14451
-(defun proof-toolbar-find-enable-p 499,14545
-(defalias 'proof-toolbar-find proof-toolbar-find
502,14614
-(defun proof-toolbar-visibility-enable-p 508,14712
-(defalias 'proof-toolbar-visibility proof-toolbar-visibility
511,14812
-(defun proof-toolbar-interrupt-enable-p 517,14900
-(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt
520,14964
-(defun proof-toolbar-make-menu-item 529,15153
-(defun proof-toolbar-scripting-menu 552,15853
-
-generic/proof-utils.el,2111
-(defmacro deflocal 27,893
-(defmacro proof-with-current-buffer-if-exists 34,1131
-(deflocal proof-buffer-type 40,1341
-(defmacro proof-with-script-buffer 46,1621
-(defmacro proof-map-buffers 57,2008
-(defmacro proof-sym 62,2193
-(defsubst proof-try-require 67,2354
-(defun proof-save-some-buffers 80,2685
-(defmacro proof-ass-sym 129,4286
-(defmacro proof-ass-symv 135,4545
-(defmacro proof-ass 141,4803
-(defun proof-defpgcustom-fn 147,5055
-(defun undefpgcustom 168,5926
-(defmacro defpgcustom 174,6150
-(defun proof-defpgdefault-fn 185,6568
-(defmacro defpgdefault 199,7026
-(defmacro defpgfun 210,7388
-(defmacro proof-eval-when-ready-for-assistant 220,7653
-(defun proof-file-truename 233,8048
-(defun proof-file-to-buffer 237,8231
-(defun proof-files-to-buffers 248,8560
-(defun proof-buffers-in-mode 255,8843
-(defun pg-save-from-death 269,9293
-(defun proof-define-keys 288,9910
-(deflocal proof-font-lock-keywords 317,10909
-(defun proof-font-lock-configure-defaults 323,11166
-(defun proof-font-lock-clear-font-lock-vars 369,13317
-(defun proof-font-lock-set-font-lock-vars 375,13529
-(defun proof-fontify-region 379,13685
-(defun pg-remove-specials 439,15986
-(defun pg-remove-specials-in-string 449,16324
-(defun proof-fontify-buffer 456,16511
-(defun proof-warn-if-unset 469,16752
-(defun proof-get-window-for-buffer 474,16970
-(defun proof-display-and-keep-buffer 525,19278
-(defun proof-clean-buffer 557,20585
-(defun proof-message 572,21206
-(defun proof-warning 577,21419
-(defun pg-internal-warning 583,21701
-(defun proof-debug 591,22020
-(defun proof-switch-to-buffer 606,22691
-(defun proof-resize-window-tofit 639,24380
-(defun proof-submit-bug-report 739,28392
-(defun proof-deftoggle-fn 775,29771
-(defmacro proof-deftoggle 790,30424
-(defun proof-defintset-fn 797,30798
-(defmacro proof-defintset 813,31502
-(defun proof-defstringset-fn 820,31879
-(defmacro proof-defstringset 833,32505
-(defmacro proof-defshortcut 847,32962
-(defmacro proof-definvisible 862,33601
-(defun pg-custom-save-vars 890,34578
-(defun pg-custom-reset-vars 908,35301
-(defun proof-locate-executable 921,35638
-
-generic/proof-x-symbol.el,579
-(defvar proof-x-symbol-initialized 55,2172
-(defun proof-x-symbol-tokenlang-file 58,2267
-(defun proof-x-symbol-support-maybe-available 64,2449
-(defun proof-x-symbol-initialize 84,3178
-(defun proof-x-symbol-enable 167,6444
-(defun proof-x-symbol-refresh-output-buffers 194,7519
-(defun proof-x-symbol-mode-associated-buffers 209,8261
-(defun proof-x-symbol-decode-region 227,8799
-(defun proof-x-symbol-encode-shell-input 241,9406
-(defun proof-x-symbol-set-language 258,9997
-(defun proof-x-symbol-shell-config 263,10168
-(defun proof-x-symbol-config-output-buffer 310,12309
-
-generic/test-compile.el,21
-(defconst bar 8,139
-
-generic/test-mac.el,21
-(defvar testme 3,26
-
-generic/test-req2.el,48
-(define-derived-mode proof-response-mode 9,160
+(defun proof-toolbar-function 42,1325
+(defun proof-toolbar-icon 45,1422
+(defun proof-toolbar-enabler 48,1523
+(defun proof-toolbar-function-with-enabler 51,1631
+(defun proof-toolbar-make-icon 58,1804
+(defun proof-toolbar-make-toolbar-item 76,2404
+(defvar proof-toolbar 115,3780
+(deflocal proof-toolbar-itimer 119,3909
+(defun proof-toolbar-setup 123,4019
+(defun proof-toolbar-build 166,5562
+(defalias 'proof-toolbar-enable proof-toolbar-enable
231,7760
+(defun proof-toolbar-setup-refresh 242,8064
+(defun proof-toolbar-disable-refresh 263,8885
+(deflocal proof-toolbar-refresh-flag 271,9275
+(defun proof-toolbar-refresh 277,9546
+(defvar proof-toolbar-enablers281,9691
+(defvar proof-toolbar-enablers-last-state287,9867
+(defun proof-toolbar-really-refresh 291,9958
+(defun proof-toolbar-undo-enable-p 346,11852
+(defalias 'proof-toolbar-undo proof-toolbar-undo
351,12000
+(defun proof-toolbar-delete-enable-p 357,12119
+(defalias 'proof-toolbar-delete proof-toolbar-delete
363,12293
+(defun proof-toolbar-lockedend-enable-p 370,12429
+(defalias 'proof-toolbar-lockedend proof-toolbar-lockedend
373,12479
+(defun proof-toolbar-next-enable-p 382,12567
+(defalias 'proof-toolbar-next proof-toolbar-next
386,12674
+(defun proof-toolbar-goto-enable-p 393,12768
+(defalias 'proof-toolbar-goto proof-toolbar-goto
396,12841
+(defun proof-toolbar-retract-enable-p 403,12917
+(defalias 'proof-toolbar-retract proof-toolbar-retract
407,13028
+(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p
414,13107
+(defalias 'proof-toolbar-use proof-toolbar-use
415,13175
+(defun proof-toolbar-restart-enable-p 421,13253
+(defalias 'proof-toolbar-restart proof-toolbar-restart
426,13414
+(defun proof-toolbar-goal-enable-p 432,13492
+(defalias 'proof-toolbar-goal proof-toolbar-goal
439,13725
+(defun proof-toolbar-qed-enable-p 446,13797
+(defalias 'proof-toolbar-qed proof-toolbar-qed
452,13949
+(defun proof-toolbar-state-enable-p 458,14021
+(defalias 'proof-toolbar-state proof-toolbar-state
461,14092
+(defun proof-toolbar-context-enable-p 467,14161
+(defalias 'proof-toolbar-context proof-toolbar-context
470,14234
+(defun proof-toolbar-info-enable-p 478,14394
+(defalias 'proof-toolbar-info proof-toolbar-info
481,14438
+(defun proof-toolbar-command-enable-p 487,14507
+(defalias 'proof-toolbar-command proof-toolbar-command
490,14578
+(defun proof-toolbar-help-enable-p 496,14658
+(defun proof-toolbar-help 499,14703
+(defun proof-toolbar-find-enable-p 507,14797
+(defalias 'proof-toolbar-find proof-toolbar-find
510,14866
+(defun proof-toolbar-visibility-enable-p 516,14964
+(defalias 'proof-toolbar-visibility proof-toolbar-visibility
519,15064
+(defun proof-toolbar-interrupt-enable-p 525,15152
+(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt
528,15216
+(defun proof-toolbar-make-menu-item 537,15405
+(defun proof-toolbar-scripting-menu 560,16105
+
+generic/proof-utils.el,2113
+(defmacro deflocal 32,1051
+(defmacro proof-with-current-buffer-if-exists 39,1289
+(deflocal proof-buffer-type 45,1499
+(defmacro proof-with-script-buffer 51,1779
+(defmacro proof-map-buffers 62,2166
+(defmacro proof-sym 67,2351
+(defsubst proof-try-require 72,2512
+(defun proof-save-some-buffers 85,2843
+(defmacro proof-ass-sym 134,4444
+(defmacro proof-ass-symv 140,4703
+(defmacro proof-ass 146,4961
+(defun proof-defpgcustom-fn 152,5213
+(defun undefpgcustom 173,6084
+(defmacro defpgcustom 179,6308
+(defun proof-defpgdefault-fn 190,6726
+(defmacro defpgdefault 204,7184
+(defmacro defpgfun 215,7546
+(defmacro proof-eval-when-ready-for-assistant 225,7811
+(defun proof-file-truename 238,8206
+(defun proof-file-to-buffer 242,8389
+(defun proof-files-to-buffers 253,8718
+(defun proof-buffers-in-mode 260,9001
+(defun pg-save-from-death 274,9451
+(defun proof-define-keys 293,10068
+(deflocal proof-font-lock-keywords 322,11067
+(defun proof-font-lock-configure-defaults 328,11324
+(defun proof-font-lock-clear-font-lock-vars 374,13475
+(defun proof-font-lock-set-font-lock-vars 380,13687
+(defun proof-fontify-region 384,13843
+(defun pg-remove-specials 444,16144
+(defun pg-remove-specials-in-string 454,16482
+(defun proof-fontify-buffer 461,16669
+(defun proof-warn-if-unset 474,16910
+(defun proof-get-window-for-buffer 479,17128
+(defun proof-display-and-keep-buffer 530,19436
+(defun proof-clean-buffer 562,20743
+(defun proof-message 577,21364
+(defun proof-warning 582,21577
+(defun pg-internal-warning 588,21859
+(defun proof-debug 596,22178
+(defun proof-switch-to-buffer 611,22849
+(defun proof-resize-window-tofit 644,24538
+(defun proof-submit-bug-report 744,28550
+(defun proof-deftoggle-fn 780,29929
+(defmacro proof-deftoggle 795,30582
+(defun proof-defintset-fn 802,30956
+(defmacro proof-defintset 818,31660
+(defun proof-defstringset-fn 825,32037
+(defmacro proof-defstringset 838,32663
+(defmacro proof-defshortcut 852,33120
+(defmacro proof-definvisible 867,33759
+(defun pg-custom-save-vars 895,34736
+(defun pg-custom-reset-vars 913,35459
+(defun proof-locate-executable 926,35796
+
+generic/proof-x-symbol.el,580
+(defvar proof-x-symbol-initialized 52,2006
+(defun proof-x-symbol-tokenlang-file 55,2101
+(defun proof-x-symbol-support-maybe-available 61,2283
+(defun proof-x-symbol-initialize 81,3012
+(defun proof-x-symbol-enable 164,6278
+(defun proof-x-symbol-refresh-output-buffers 191,7353
+(defun proof-x-symbol-mode-associated-buffers 206,8095
+(defun proof-x-symbol-decode-region 224,8633
+(defun proof-x-symbol-encode-shell-input 245,9630
+(defun proof-x-symbol-set-language 262,10221
+(defun proof-x-symbol-shell-config 267,10392
+(defun proof-x-symbol-config-output-buffer 314,12533
 
 lib/bufhist.el,1100
 (defun bufhist-ring-update 32,1226
@@ -2315,33 +2328,33 @@ lib/pg-dev.el,75
 (defun unload-pg 69,1986
 
 lib/proof-compat.el,748
-(defvar proof-running-on-win32 26,856
-(defun pg-custom-undeclare-variable 38,1313
-(defun subst-char-in-string 100,2958
-(defun replace-regexp-in-string 115,3547
-(defconst menuvisiblep 177,6260
-(defun set-window-text-height 194,6873
-(defmacro save-selected-frame 220,7823
-(defun warn 259,9120
-(defun redraw-modeline 266,9375
-(defun proof-buffer-syntactic-context-emulate 277,9813
-(defvar read-shell-command-map310,11120
-(defun read-shell-command 328,11822
-(defun remassq 340,12303
-(defun remassoc 352,12692
-(defun frames-of-buffer 365,13137
-(defmacro with-selected-window 404,14399
-(defun pg-pop-to-buffer 447,15777
-(defun process-live-p 498,17610
-(defalias 'proof-buffer-syntactic-context proof-buffer-syntactic-context
515,18113
+(defvar proof-running-on-win32 29,914
+(defun pg-custom-undeclare-variable 41,1371
+(defun subst-char-in-string 103,3016
+(defun replace-regexp-in-string 118,3605
+(defconst menuvisiblep 180,6318
+(defun set-window-text-height 197,6931
+(defmacro save-selected-frame 223,7881
+(defun warn 262,9178
+(defun redraw-modeline 269,9433
+(defun proof-buffer-syntactic-context-emulate 280,9871
+(defvar read-shell-command-map313,11178
+(defun read-shell-command 331,11866
+(defun remassq 343,12347
+(defun remassoc 355,12736
+(defun frames-of-buffer 368,13181
+(defmacro with-selected-window 407,14443
+(defun pg-pop-to-buffer 450,15821
+(defun process-live-p 501,17654
+(defalias 'proof-buffer-syntactic-context proof-buffer-syntactic-context
518,18157
 
 lib/span.el,137
-(defsubst span-delete-spans 22,471
-(defsubst span-property-safe 26,635
-(defsubst span-set-start 30,774
-(defsubst span-set-end 34,906
+(defsubst span-delete-spans 22,479
+(defsubst span-property-safe 26,643
+(defsubst span-set-start 30,782
+(defsubst span-set-end 34,914
 
-lib/span-extent.el,973
+lib/span-extent.el,1015
 (defsubst span-make 12,367
 (defsubst span-detach 16,489
 (defsubst span-set-endpoints 20,576
@@ -2353,24 +2366,25 @@ lib/span-extent.el,973
 (defsubst span-property 45,1355
 (defsubst span-delete 49,1470
 (defsubst span-mapcar-spans 55,1641
-(defsubst span-at 59,1852
-(defsubst span-at-before 63,1969
-(defsubst span-start 68,2166
-(defsubst span-end 72,2295
-(defsubst prev-span 76,2418
-(defsubst next-span 80,2564
-(defsubst span-live-p 84,2706
-(defun span-raise 92,2978
-(defalias 'span-object span-object
96,3077
-(defalias 'span-string span-string
97,3116
-(defsubst make-detached-span 100,3202
-(defsubst span-buffer 105,3264
-(defsubst span-detached-p 110,3356
-(defsubst set-span-face 115,3468
-(defsubst fold-spans 119,3563
-(defsubst set-span-properties 123,3760
-(defsubst set-span-keymap 127,3868
-(defsubst span-at-event 132,4012
+(defsubst spans-at-region-prop 59,1852
+(defsubst span-at 63,2040
+(defsubst span-at-before 67,2157
+(defsubst span-start 72,2354
+(defsubst span-end 76,2483
+(defsubst prev-span 80,2606
+(defsubst next-span 84,2752
+(defsubst span-live-p 88,2894
+(defun span-raise 96,3166
+(defalias 'span-object span-object
100,3265
+(defalias 'span-string span-string
101,3304
+(defsubst make-detached-span 104,3390
+(defsubst span-buffer 109,3452
+(defsubst span-detached-p 114,3544
+(defsubst set-span-face 119,3656
+(defsubst fold-spans 123,3751
+(defsubst set-span-properties 127,3948
+(defsubst set-span-keymap 131,4056
+(defsubst span-at-event 136,4200
 
 lib/span-overlay.el,1206
 (defalias 'span-start span-start
12,370
@@ -2389,24 +2403,24 @@ lib/span-overlay.el,1206
 (defun span-lt 57,2247
 (defun spans-at-point-prop 62,2388
 (defun spans-at-region-prop 68,2553
-(defun span-at 76,2797
-(defsubst span-delete 82,3011
-(defsubst span-mapcar-spans 89,3233
-(defun span-at-before 93,3442
-(defun prev-span 110,4168
-(defun next-span 116,4319
-(defsubst span-live-p 145,5544
-(defun span-raise 151,5710
-(defalias 'span-object span-object
157,5953
-(defun span-string 159,5994
-(defun set-span-properties 165,6176
-(defun span-find-span 177,6431
-(defsubst span-at-event 184,6738
-(defun make-detached-span 189,6862
-(defun fold-spans 194,6958
-(defsubst span-detached-p 209,7492
-(defsubst set-span-face 213,7607
-(defun set-span-keymap 217,7704
+(defun span-at 77,2865
+(defsubst span-delete 83,3079
+(defsubst span-mapcar-spans 90,3301
+(defun span-at-before 94,3510
+(defun prev-span 111,4236
+(defun next-span 117,4387
+(defsubst span-live-p 146,5612
+(defun span-raise 152,5778
+(defalias 'span-object span-object
158,6021
+(defun span-string 160,6062
+(defun set-span-properties 166,6244
+(defun span-find-span 178,6499
+(defsubst span-at-event 185,6806
+(defun make-detached-span 189,6927
+(defun fold-spans 194,7023
+(defsubst span-detached-p 209,7557
+(defsubst set-span-face 213,7672
+(defun set-span-keymap 217,7769
 
 lib/texi-docstring-magic.el,584
 (defun texi-docstring-magic-find-face 88,3034
@@ -3504,155 +3518,156 @@ x-symbol/lisp/x-symbol-xmacs.el,522
 (defun x-symbol-event-matches-key-specifier-p 163,7016
 (defun x-symbol-window-width 173,7418
 
-doc/ProofGeneral.texi,5379
-@node Top166,5052
-@node Preface203,6168
-@node Latest news for version 3.7Latest news for version 3.7
226,6764
-@node Future265,8413
-@node Credits296,9712
-@node Introducing Proof GeneralIntroducing Proof General
395,13146
-@node Installing Proof GeneralInstalling Proof General
451,15188
-@node Quick start guideQuick start guide
465,15636
-@node Features of Proof GeneralFeatures of Proof General
509,17744
-@node Supported proof assistantsSupported proof assistants
598,21669
-@node Prerequisites for this manualPrerequisites for this manual
647,23575
-@node Organization of this manualOrganization of this manual
691,25201
-@node Basic Script ManagementBasic Script Management
717,26029
-@node Walkthrough example in IsabelleWalkthrough example in Isabelle
736,26629
-@node Proof scriptsProof scripts
987,36282
-@node Script buffersScript buffers
1030,38402
-@node Locked queue and editing regionsLocked queue and editing regions
1052,38979
-@node Goal-save sequencesGoal-save sequences
1108,41126
-@node Active scripting bufferActive scripting buffer
1145,42612
-@node Summary of Proof General buffersSummary of Proof General buffers
1214,46032
-@node Script editing commandsScript editing commands
1276,48706
-@node Script processing commandsScript processing commands
1354,51557
-@node Proof assistant commandsProof assistant commands
1482,56858
-@node Toolbar commandsToolbar commands
1632,61862
-@node Interrupting during trace outputInterrupting during trace output
1656,62791
-@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
1695,64715
-@node Goals buffer commandsGoals buffer commands
1709,65215
-@node Advanced Script ManagementAdvanced Script Management
1798,68748
-@node Visibility of completed proofsVisibility of completed proofs
1829,69902
-@node Switching between proof scriptsSwitching between proof scripts
1884,71825
-@node View of processed files View of processed files 
1921,73797
-@node Retracting across filesRetracting across files
1981,76848
-@node Asserting across filesAsserting across files
1994,77479
-@node Automatic multiple file handlingAutomatic multiple file handling
2007,78045
-@node Escaping script managementEscaping script management
2032,79079
-@node Experimental featuresExperimental features
2090,81282
-@node Support for other PackagesSupport for other Packages
2124,82544
-@node Syntax highlightingSyntax highlighting
2156,83419
-@node X-Symbol supportX-Symbol support
2195,85040
-@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)
2254,87586
-@node Support for outline modeSupport for outline mode
2313,89716
-@node Support for completionSupport for completion
2339,90846
-@node Support for tagsSupport for tags
2397,93022
-@node Customizing Proof GeneralCustomizing Proof General
2449,95351
-@node Basic optionsBasic options
2489,97021
-@node How to customizeHow to customize
2513,97779
-@node Display customizationDisplay customization
2564,99881
-@node User optionsUser options
2689,105119
-@node Changing facesChanging faces
2953,114509
-@node Tweaking configuration settingsTweaking configuration settings
3028,117178
-@node Hints and TipsHints and Tips
3085,119704
-@node Adding your own keybindingsAdding your own keybindings
3104,120305
-@node Using file variablesUsing file variables
3160,122838
-@node Using abbreviationsUsing abbreviations
3219,125024
-@node LEGO Proof GeneralLEGO Proof General
3258,126440
-@node LEGO specific commandsLEGO specific commands
3299,127809
-@node LEGO tagsLEGO tags
3319,128264
-@node LEGO customizationsLEGO customizations
3329,128511
-@node Coq Proof GeneralCoq Proof General
3361,129430
-@node Coq-specific commandsCoq-specific commands
3377,129839
-@node Coq-specific variablesCoq-specific variables
3399,130346
-@node Editing multiple proofsEditing multiple proofs
3421,131004
-@node User-loaded tacticsUser-loaded tactics
3445,132112
-@node Holes featureHoles feature
3509,134586
-@node Isabelle Proof GeneralIsabelle Proof General
3536,135873
-@node Isabelle commandsIsabelle commands
3566,137003
-@node Logics and SettingsLogics and Settings
3673,140051
-@node Isabelle customizationsIsabelle customizations
3707,141591
-@node HOL Proof GeneralHOL Proof General
3731,142073
-@node Shell Proof GeneralShell Proof General
3773,143895
-@node Obtaining and InstallingObtaining and Installing
3809,145354
-@node Obtaining Proof GeneralObtaining Proof General
3825,145767
-@node Installing Proof General from tarballInstalling Proof General from tarball
3856,147006
-@node Installing Proof General from RPM packageInstalling Proof General from RPM package
3881,147838
-@node Setting the names of binariesSetting the names of binaries
3896,148246
-@node Notes for syssiesNotes for syssies
3924,149186
-@node Bugs and EnhancementsBugs and Enhancements
3999,152222
-@node References4020,153037
-@node History of Proof GeneralHistory of Proof General
4060,154061
-@node Old News for 3.0Old News for 3.0
4151,158163
-@node Old News for 3.1Old News for 3.1
4221,161857
-@node Old News for 3.2Old News for 3.2
4247,163029
-@node Old News for 3.3Old News for 3.3
4308,166032
-@node Old News for 3.4Old News for 3.4
4327,166929
-@node Function IndexFunction Index
4350,167985
-@node Variable IndexVariable Index
4354,168061
-@node Keystroke IndexKeystroke Index
4358,168141
-@node Concept IndexConcept Index
4362,168207
+doc/ProofGeneral.texi,5457
+@node Top166,5053
+@node Preface203,6181
+@node Latest news for version 3.7Latest news for version 3.7
226,6777
+@node Future267,8596
+@node Credits298,9895
+@node Introducing Proof GeneralIntroducing Proof General
398,13342
+@node Installing Proof GeneralInstalling Proof General
454,15384
+@node Quick start guideQuick start guide
468,15833
+@node Features of Proof GeneralFeatures of Proof General
512,17954
+@node Supported proof assistantsSupported proof assistants
601,21891
+@node Prerequisites for this manualPrerequisites for this manual
650,23797
+@node Organization of this manualOrganization of this manual
694,25423
+@node Basic Script ManagementBasic Script Management
720,26251
+@node Walkthrough example in IsabelleWalkthrough example in Isabelle
739,26851
+@node Proof scriptsProof scripts
990,36504
+@node Script buffersScript buffers
1033,38624
+@node Locked queue and editing regionsLocked queue and editing regions
1055,39201
+@node Goal-save sequencesGoal-save sequences
1111,41348
+@node Active scripting bufferActive scripting buffer
1148,42834
+@node Summary of Proof General buffersSummary of Proof General buffers
1217,46254
+@node Script editing commandsScript editing commands
1279,48928
+@node Script processing commandsScript processing commands
1357,51787
+@node Proof assistant commandsProof assistant commands
1485,57088
+@node Toolbar commandsToolbar commands
1651,62867
+@node Interrupting during trace outputInterrupting during trace output
1675,63796
+@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
1714,65720
+@node Goals buffer commandsGoals buffer commands
1728,66220
+@node Advanced Script Management and EditingAdvanced Script Management and Editing
1817,69759
+@node Visibility of completed proofsVisibility of completed proofs
1849,70971
+@node Switching between proof scriptsSwitching between proof scripts
1904,72894
+@node View of processed files View of processed files 
1941,74866
+@node Retracting across filesRetracting across files
2001,77917
+@node Asserting across filesAsserting across files
2014,78548
+@node Automatic multiple file handlingAutomatic multiple file handling
2027,79114
+@node Escaping script managementEscaping script management
2052,80148
+@node Editing featuresEditing features
2110,82351
+@node Experimental featuresExperimental features
2172,84974
+@node Support for other PackagesSupport for other Packages
2209,86345
+@node Syntax highlightingSyntax highlighting
2241,87220
+@node X-Symbol supportX-Symbol support
2280,88841
+@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)
2339,91387
+@node Support for outline modeSupport for outline mode
2398,93517
+@node Support for completionSupport for completion
2424,94647
+@node Support for tagsSupport for tags
2482,96823
+@node Customizing Proof GeneralCustomizing Proof General
2534,99152
+@node Basic optionsBasic options
2574,100822
+@node How to customizeHow to customize
2598,101580
+@node Display customizationDisplay customization
2649,103682
+@node User optionsUser options
2774,108920
+@node Changing facesChanging faces
3036,118160
+@node Tweaking configuration settingsTweaking configuration settings
3111,120829
+@node Hints and TipsHints and Tips
3168,123355
+@node Adding your own keybindingsAdding your own keybindings
3187,123956
+@node Using file variablesUsing file variables
3243,126489
+@node Using abbreviationsUsing abbreviations
3302,128675
+@node LEGO Proof GeneralLEGO Proof General
3341,130091
+@node LEGO specific commandsLEGO specific commands
3382,131460
+@node LEGO tagsLEGO tags
3402,131915
+@node LEGO customizationsLEGO customizations
3412,132162
+@node Coq Proof GeneralCoq Proof General
3444,133081
+@node Coq-specific commandsCoq-specific commands
3460,133490
+@node Coq-specific variablesCoq-specific variables
3482,133997
+@node Editing multiple proofsEditing multiple proofs
3504,134655
+@node User-loaded tacticsUser-loaded tactics
3528,135763
+@node Holes featureHoles feature
3592,138237
+@node Isabelle Proof GeneralIsabelle Proof General
3619,139524
+@node Isabelle commandsIsabelle commands
3649,140654
+@node Logics and SettingsLogics and Settings
3756,143702
+@node Isabelle customizationsIsabelle customizations
3790,145242
+@node HOL Proof GeneralHOL Proof General
3814,145724
+@node Shell Proof GeneralShell Proof General
3856,147546
+@node Obtaining and InstallingObtaining and Installing
3892,149005
+@node Obtaining Proof GeneralObtaining Proof General
3908,149418
+@node Installing Proof General from tarballInstalling Proof General from tarball
3939,150657
+@node Installing Proof General from RPM packageInstalling Proof General from RPM package
3964,151489
+@node Setting the names of binariesSetting the names of binaries
3979,151897
+@node Notes for syssiesNotes for syssies
4007,152837
+@node Bugs and EnhancementsBugs and Enhancements
4082,155873
+@node References4103,156688
+@node History of Proof GeneralHistory of Proof General
4143,157712
+@node Old News for 3.0Old News for 3.0
4234,161814
+@node Old News for 3.1Old News for 3.1
4304,165508
+@node Old News for 3.2Old News for 3.2
4330,166680
+@node Old News for 3.3Old News for 3.3
4391,169683
+@node Old News for 3.4Old News for 3.4
4410,170580
+@node Function IndexFunction Index
4433,171636
+@node Variable IndexVariable Index
4437,171712
+@node Keystroke IndexKeystroke Index
4441,171792
+@node Concept IndexConcept Index
4445,171858
 
 doc/PG-adapting.texi,3776
-@node Top157,4775
-@node Introduction195,5920
-@node Future236,7573
-@node Credits272,9169
-@node Beginning with a New ProverBeginning with a New Prover
282,9461
-@node Overview of adding a new proverOverview of adding a new prover
323,11410
-@node Demonstration instance and easy configurationDemonstration instance and easy configuration
398,14707
-@node Major modes used by Proof GeneralMajor modes used by Proof General
467,18098
-@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands
500,19449
-@node Settings for generic user-level commandsSettings for generic user-level commands
515,19995
-@node Menu configurationMenu configuration
560,21729
-@node Toolbar configurationToolbar configuration
584,22646
-@node Proof Script SettingsProof Script Settings
642,24888
-@node Recognizing commands and commentsRecognizing commands and comments
664,25468
-@node Recognizing proofsRecognizing proofs
785,31003
-@node Recognizing other elementsRecognizing other elements
897,35821
-@node Configuring undo behaviourConfiguring undo behaviour
1023,41332
-@node Nested proofsNested proofs
1160,46743
-@node Safe (state-preserving) commandsSafe (state-preserving) commands
1200,48369
-@node Activate scripting hookActivate scripting hook
1223,49315
-@node Automatic multiple filesAutomatic multiple files
1247,50178
-@node Completions1269,51025
-@node Proof Shell SettingsProof Shell Settings
1310,52514
-@node Proof shell commandsProof shell commands
1341,53796
-@node Script input to the shellScript input to the shell
1508,60959
-@node Settings for matching various output from proof processSettings for matching various output from proof process
1575,63999
-@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process
1706,69760
-@node Hooks and other settingsHooks and other settings
1916,79353
-@node Goals Buffer SettingsGoals Buffer Settings
1997,82722
-@node Splash Screen SettingsSplash Screen Settings
2074,85821
-@node Global ConstantsGlobal Constants
2100,86579
-@node Handling Multiple FilesHandling Multiple Files
2126,87420
-@node Configuring Editing SyntaxConfiguring Editing Syntax
2278,95204
-@node Configuring Font LockConfiguring Font Lock
2337,97325
-@node Configuring X-SymbolConfiguring X-Symbol
2424,101610
-@node Writing More Lisp CodeWriting More Lisp Code
2484,104130
-@node Default values for generic settingsDefault values for generic settings
2501,104775
-@node Adding prover-specific configurationsAdding prover-specific configurations
2531,105858
-@node Useful variablesUseful variables
2574,107140
-@node Useful functions and macrosUseful functions and macros
2589,107629
-@node Internals of Proof GeneralInternals of Proof General
2692,111592
-@node Spans2720,112500
-@node Proof General site configurationProof General site configuration
2733,112874
-@node Configuration variable mechanismsConfiguration variable mechanisms
2813,115962
-@node Global variablesGlobal variables
2931,121198
-@node Proof script modeProof script mode
3001,123748
-@node Proof shell modeProof shell mode
3260,135403
-@node Debugging3665,151380
-@node Plans and IdeasPlans and Ideas
3708,152256
-@node Proof by pointing and similar featuresProof by pointing and similar features
3729,152978
-@node Granularity of atomic command sequencesGranularity of atomic command sequences
3767,154636
-@node Browser mode for script files and theoriesBrowser mode for script files and theories
3812,156861
-@node Demonstration InstantiationsDemonstration Instantiations
3842,157892
-@node demoisa-easy.el3858,158323
-@node demoisa.el3921,160562
-@node Function IndexFunction Index
4089,166091
-@node Variable IndexVariable Index
4093,166167
-@node Concept IndexConcept Index
4102,166346
+@node Top157,4778
+@node Introduction195,5923
+@node Future236,7576
+@node Credits272,9172
+@node Beginning with a New ProverBeginning with a New Prover
282,9464
+@node Overview of adding a new proverOverview of adding a new prover
323,11413
+@node Demonstration instance and easy configurationDemonstration instance and easy configuration
401,14721
+@node Major modes used by Proof GeneralMajor modes used by Proof General
470,18112
+@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands
503,19463
+@node Settings for generic user-level commandsSettings for generic user-level commands
518,20009
+@node Menu configurationMenu configuration
563,21743
+@node Toolbar configurationToolbar configuration
587,22660
+@node Proof Script SettingsProof Script Settings
645,24902
+@node Recognizing commands and commentsRecognizing commands and comments
667,25482
+@node Recognizing proofsRecognizing proofs
788,30989
+@node Recognizing other elementsRecognizing other elements
900,35802
+@node Configuring undo behaviourConfiguring undo behaviour
1026,41313
+@node Nested proofsNested proofs
1163,46707
+@node Safe (state-preserving) commandsSafe (state-preserving) commands
1203,48333
+@node Activate scripting hookActivate scripting hook
1226,49279
+@node Automatic multiple filesAutomatic multiple files
1250,50142
+@node Completions1272,50989
+@node Proof Shell SettingsProof Shell Settings
1313,52478
+@node Proof shell commandsProof shell commands
1344,53760
+@node Script input to the shellScript input to the shell
1508,60699
+@node Settings for matching various output from proof processSettings for matching various output from proof process
1575,63739
+@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process
1706,69488
+@node Hooks and other settingsHooks and other settings
1921,79359
+@node Goals Buffer SettingsGoals Buffer Settings
2002,82728
+@node Splash Screen SettingsSplash Screen Settings
2079,85827
+@node Global ConstantsGlobal Constants
2105,86585
+@node Handling Multiple FilesHandling Multiple Files
2131,87426
+@node Configuring Editing SyntaxConfiguring Editing Syntax
2283,95209
+@node Configuring Font LockConfiguring Font Lock
2342,97330
+@node Configuring X-SymbolConfiguring X-Symbol
2429,101615
+@node Writing More Lisp CodeWriting More Lisp Code
2489,104135
+@node Default values for generic settingsDefault values for generic settings
2506,104780
+@node Adding prover-specific configurationsAdding prover-specific configurations
2536,105863
+@node Useful variablesUseful variables
2579,107145
+@node Useful functions and macrosUseful functions and macros
2594,107644
+@node Internals of Proof GeneralInternals of Proof General
2697,111599
+@node Spans2725,112507
+@node Proof General site configurationProof General site configuration
2738,112881
+@node Configuration variable mechanismsConfiguration variable mechanisms
2818,115927
+@node Global variablesGlobal variables
2939,121357
+@node Proof script modeProof script mode
3009,123905
+@node Proof shell modeProof shell mode
3268,135560
+@node Debugging3674,151582
+@node Plans and IdeasPlans and Ideas
3717,152458
+@node Proof by pointing and similar featuresProof by pointing and similar features
3738,153180
+@node Granularity of atomic command sequencesGranularity of atomic command sequences
3776,154838
+@node Browser mode for script files and theoriesBrowser mode for script files and theories
3821,157063
+@node Demonstration InstantiationsDemonstration Instantiations
3851,158094
+@node demoisa-easy.el3867,158525
+@node demoisa.el3930,160764
+@node Function IndexFunction Index
4085,165749
+@node Variable IndexVariable Index
4089,165825
+@node Concept IndexConcept Index
4098,166004
 
 x-symbol/lisp/_pkg.el,0
 
@@ -3660,14 +3675,16 @@ x-symbol/lisp/custom-load.el,0
 
 lib/holes-load.el,0
 
-generic/test-req.el,0
-
-generic/test-mac2.el,0
+generic/test.el,0
 
 generic/proof.el,0
 
 generic/proof-autoloads.el,0
 
+generic/pg-cmdhist.el,0
+
+generic/comptest.el,0
+
 twelf/x-symbol-twelf.el,0
 
 pgshell/pgshell.el,0