Updated.

1 files changed, 1696 insertions, 1711 deletions

diff --git a/TAGS b/TAGS
index 3256aa14..dd9d8d2c 100644
--- a/TAGS
+++ b/TAGS
@@ -31,164 +31,164 @@ coq/coq-db.el,559
 (defconst coq-solve-tactics-face 229,8518
 
 coq/coq.el,6283
-(defcustom coq-translate-to-v8 41,1205
-(defun coq-build-prog-args 47,1385
-(defcustom coq-compile-file-command 60,1765
-(defcustom coq-default-undo-limit 70,2134
-(defconst coq-shell-init-cmd 75,2262
-(defcustom coq-prog-env 93,2863
-(defconst coq-shell-restart-cmd 101,3115
-(defvar coq-shell-prompt-pattern 108,3375
-(defvar coq-shell-cd 116,3704
-(defvar coq-shell-abort-goal-regexp 120,3859
-(defvar coq-shell-proof-completed-regexp 123,3985
-(defvar coq-goal-regexp126,4137
-(defun coq-library-directory 135,4326
-(defcustom coq-tags 142,4506
-(defconst coq-interrupt-regexp 147,4656
-(defcustom coq-www-home-page 152,4777
-(defvar coq-outline-regexp162,4948
-(defvar coq-outline-heading-end-regexp 169,5162
-(defvar coq-shell-outline-regexp 171,5216
-(defvar coq-shell-outline-heading-end-regexp 172,5266
-(defconst coq-kill-goal-command 177,5376
-(defconst coq-forget-id-command 178,5419
-(defconst coq-back-n-command 179,5466
-(defconst coq-state-preserving-tactics-regexp 183,5610
-(defconst coq-state-changing-commands-regexp185,5711
-(defconst coq-state-preserving-commands-regexp 187,5818
-(defconst coq-commands-regexp 189,5930
-(defvar coq-retractable-instruct-regexp 191,6008
-(defvar coq-non-retractable-instruct-regexp 193,6099
-(defvar coq-keywords-section197,6239
-(defvar coq-section-regexp 200,6333
-(defun coq-set-undo-limit 234,7433
-(defconst coq-keywords-decl-defn-regexp245,7872
-(defun coq-proof-mode-p 249,8022
-(defun coq-is-comment-or-proverprocp 260,8430
-(defun coq-is-goalsave-p 262,8534
-(defun coq-is-module-equal-p 263,8609
-(defun coq-is-def-p 266,8805
-(defun coq-is-decl-defn-p 268,8913
-(defun coq-state-preserving-command-p 273,9080
-(defun coq-command-p 276,9214
-(defun coq-state-preserving-tactic-p 279,9314
-(defun coq-state-changing-tactic-p 284,9462
-(defun coq-state-changing-command-p 291,9696
-(defun coq-section-or-module-start-p 298,10042
-(defun build-list-id-from-string 307,10283
-(defun coq-last-prompt-info 320,10813
-(defun coq-last-prompt-info-safe 332,11354
-(defvar coq-last-but-one-statenum 338,11611
-(defvar coq-last-but-one-proofnum 344,11909
-(defvar coq-last-but-one-proofstack 347,12007
-(defun coq-get-span-statenum 350,12117
-(defun coq-get-span-proofnum 355,12232
-(defun coq-get-span-proofstack 360,12347
-(defun coq-set-span-statenum 365,12491
-(defun coq-get-span-goalcmd 370,12622
-(defun coq-set-span-goalcmd 375,12736
-(defun coq-set-span-proofnum 380,12866
-(defun coq-set-span-proofstack 385,12997
-(defun proof-last-locked-span 390,13157
-(defun coq-set-state-infos 405,13761
-(defun count-not-intersection 445,15840
-(defun  coq-find-and-forget-v81 476,17094
-(defun coq-find-and-forget-v80 504,18226
-(defun coq-find-and-forget 599,22925
-(defvar coq-current-goal 612,23465
-(defun coq-goal-hyp 615,23530
-(defun coq-state-preserving-p 628,23963
-(defconst notation-print-kinds-table 643,24469
-(defun coq-PrintScope 647,24637
-(defun coq-guess-or-ask-for-string 666,25193
-(defun coq-ask-do 677,25578
-(defun coq-SearchIsos 686,25966
-(defun coq-SearchConstant 692,26199
-(defun coq-SearchRewrite 696,26292
-(defun coq-SearchAbout 700,26390
-(defun coq-Print 704,26482
-(defun coq-About 708,26604
-(defun coq-LocateConstant 712,26721
-(defun coq-LocateLibrary 718,26856
-(defun coq-addquotes 724,27006
-(defun coq-LocateNotation 726,27054
-(defun coq-Pwd 733,27253
-(defun coq-Inspect 739,27385
-(defun coq-PrintSection(743,27485
-(defun coq-Print-implicit 747,27578
-(defun coq-Check 752,27729
-(defun coq-Show 757,27837
-(defun coq-Compile 771,28280
-(defun coq-guess-command-line 785,28600
-(defun coq-mode-config 806,29453
-(defun coq-hybrid-ouput-goals-response-p 920,33649
-(defun coq-hybrid-ouput-goals-response 926,33907
-(defun coq-shell-mode-config 946,34817
-(defun coq-goals-mode-config 990,36888
-(defun coq-response-config 997,37120
-(defpacustom print-fully-explicit 1020,37829
-(defpacustom print-implicit 1025,37978
-(defpacustom print-coercions 1030,38145
-(defpacustom print-match-wildcards 1035,38290
-(defpacustom print-elim-types 1040,38471
-(defpacustom printing-depth 1045,38638
-(defpacustom time-commands 1050,38800
-(defpacustom auto-compile-vos 1054,38911
-(defun coq-maybe-compile-buffer 1083,40027
-(defun coq-ancestors-of 1120,41561
-(defun coq-all-ancestors-of 1143,42528
-(defconst coq-require-command-regexp 1155,42921
-(defun coq-process-require-command 1160,43130
-(defun coq-included-children 1165,43257
-(defun coq-process-file 1186,44096
-(defun coq-preprocessing 1201,44635
-(defun coq-fake-constant-markup 1216,45054
-(defun coq-create-span-menu 1238,45861
-(defconst module-kinds-table 1258,46438
-(defconst modtype-kinds-table1262,46588
-(defun coq-insert-section-or-module 1266,46717
-(defconst reqkinds-kinds-table1289,47577
-(defun coq-insert-requires 1294,47722
-(defun coq-end-Section 1310,48228
-(defun coq-insert-intros 1328,48812
-(defun coq-insert-match 1340,49336
-(defun coq-insert-tactic 1372,50514
-(defun coq-insert-tactical 1378,50753
-(defun coq-insert-command 1384,51002
-(defun coq-insert-term 1390,51246
-(define-key coq-keymap 1396,51443
-(define-key coq-keymap 1397,51501
-(define-key coq-keymap 1398,51558
-(define-key coq-keymap 1399,51627
-(define-key coq-keymap 1400,51683
-(define-key coq-keymap 1401,51732
-(define-key coq-keymap 1402,51790
-(define-key coq-keymap 1404,51851
-(define-key coq-keymap 1405,51910
-(define-key coq-keymap 1407,51974
-(define-key coq-keymap 1408,52034
-(define-key coq-keymap 1410,52090
-(define-key coq-keymap 1411,52140
-(define-key coq-keymap 1412,52190
-(define-key coq-keymap 1413,52240
-(define-key coq-keymap 1414,52294
-(define-key coq-keymap 1415,52353
-(defvar last-coq-error-location 1425,52536
-(defun coq-get-last-error-location 1434,52935
-(defun coq-highlight-error 1467,54332
-(defvar coq-allow-highlight-error 1532,56887
-(defun coq-decide-highlight-error 1538,57153
-(defun coq-highlight-error-hook 1543,57315
-(defun first-word-of-buffer 1554,57708
-(defun coq-show-first-goal 1564,57940
-(defvar coq-modeline-string2 1580,58609
-(defvar coq-modeline-string1 1581,58653
-(defvar coq-modeline-string0 1582,58696
-(defun coq-build-subgoals-string 1583,58741
-(defun coq-update-minor-mode-alist 1588,58909
-(defun is-not-split-vertic 1614,59977
-(defun optim-resp-windows 1623,60416
+(defcustom coq-translate-to-v8 41,1202
+(defun coq-build-prog-args 47,1382
+(defcustom coq-compile-file-command 60,1762
+(defcustom coq-default-undo-limit 70,2131
+(defconst coq-shell-init-cmd 75,2259
+(defcustom coq-prog-env 93,2860
+(defconst coq-shell-restart-cmd 101,3112
+(defvar coq-shell-prompt-pattern 108,3372
+(defvar coq-shell-cd 116,3701
+(defvar coq-shell-abort-goal-regexp 120,3856
+(defvar coq-shell-proof-completed-regexp 123,3982
+(defvar coq-goal-regexp126,4134
+(defun coq-library-directory 135,4323
+(defcustom coq-tags 142,4503
+(defconst coq-interrupt-regexp 147,4653
+(defcustom coq-www-home-page 152,4774
+(defvar coq-outline-regexp162,4945
+(defvar coq-outline-heading-end-regexp 169,5159
+(defvar coq-shell-outline-regexp 171,5213
+(defvar coq-shell-outline-heading-end-regexp 172,5263
+(defconst coq-kill-goal-command 177,5373
+(defconst coq-forget-id-command 178,5416
+(defconst coq-back-n-command 179,5463
+(defconst coq-state-preserving-tactics-regexp 183,5607
+(defconst coq-state-changing-commands-regexp185,5708
+(defconst coq-state-preserving-commands-regexp 187,5815
+(defconst coq-commands-regexp 189,5927
+(defvar coq-retractable-instruct-regexp 191,6005
+(defvar coq-non-retractable-instruct-regexp 193,6096
+(defvar coq-keywords-section197,6236
+(defvar coq-section-regexp 200,6330
+(defun coq-set-undo-limit 234,7430
+(defconst coq-keywords-decl-defn-regexp245,7869
+(defun coq-proof-mode-p 249,8019
+(defun coq-is-comment-or-proverprocp 260,8427
+(defun coq-is-goalsave-p 262,8531
+(defun coq-is-module-equal-p 263,8606
+(defun coq-is-def-p 266,8802
+(defun coq-is-decl-defn-p 268,8910
+(defun coq-state-preserving-command-p 273,9077
+(defun coq-command-p 276,9211
+(defun coq-state-preserving-tactic-p 279,9311
+(defun coq-state-changing-tactic-p 284,9459
+(defun coq-state-changing-command-p 291,9693
+(defun coq-section-or-module-start-p 298,10039
+(defun build-list-id-from-string 307,10280
+(defun coq-last-prompt-info 320,10810
+(defun coq-last-prompt-info-safe 332,11351
+(defvar coq-last-but-one-statenum 338,11608
+(defvar coq-last-but-one-proofnum 344,11906
+(defvar coq-last-but-one-proofstack 347,12004
+(defun coq-get-span-statenum 350,12114
+(defun coq-get-span-proofnum 355,12229
+(defun coq-get-span-proofstack 360,12344
+(defun coq-set-span-statenum 365,12488
+(defun coq-get-span-goalcmd 370,12619
+(defun coq-set-span-goalcmd 375,12733
+(defun coq-set-span-proofnum 380,12863
+(defun coq-set-span-proofstack 385,12994
+(defun proof-last-locked-span 390,13154
+(defun coq-set-state-infos 405,13758
+(defun count-not-intersection 445,15837
+(defun  coq-find-and-forget-v81 476,17091
+(defun coq-find-and-forget-v80 504,18223
+(defun coq-find-and-forget 599,22922
+(defvar coq-current-goal 612,23462
+(defun coq-goal-hyp 615,23527
+(defun coq-state-preserving-p 628,23960
+(defconst notation-print-kinds-table 643,24466
+(defun coq-PrintScope 647,24634
+(defun coq-guess-or-ask-for-string 666,25190
+(defun coq-ask-do 677,25575
+(defun coq-SearchIsos 686,25963
+(defun coq-SearchConstant 692,26196
+(defun coq-SearchRewrite 696,26289
+(defun coq-SearchAbout 700,26387
+(defun coq-Print 704,26479
+(defun coq-About 708,26601
+(defun coq-LocateConstant 712,26718
+(defun coq-LocateLibrary 718,26853
+(defun coq-addquotes 724,27003
+(defun coq-LocateNotation 726,27051
+(defun coq-Pwd 733,27250
+(defun coq-Inspect 739,27382
+(defun coq-PrintSection(743,27482
+(defun coq-Print-implicit 747,27575
+(defun coq-Check 752,27726
+(defun coq-Show 757,27834
+(defun coq-Compile 771,28277
+(defun coq-guess-command-line 785,28597
+(defun coq-mode-config 806,29450
+(defun coq-hybrid-ouput-goals-response-p 920,33646
+(defun coq-hybrid-ouput-goals-response 926,33904
+(defun coq-shell-mode-config 946,34814
+(defun coq-goals-mode-config 990,36885
+(defun coq-response-config 997,37117
+(defpacustom print-fully-explicit 1020,37826
+(defpacustom print-implicit 1025,37975
+(defpacustom print-coercions 1030,38142
+(defpacustom print-match-wildcards 1035,38287
+(defpacustom print-elim-types 1040,38468
+(defpacustom printing-depth 1045,38635
+(defpacustom time-commands 1050,38797
+(defpacustom auto-compile-vos 1054,38908
+(defun coq-maybe-compile-buffer 1083,40024
+(defun coq-ancestors-of 1120,41558
+(defun coq-all-ancestors-of 1143,42525
+(defconst coq-require-command-regexp 1155,42918
+(defun coq-process-require-command 1160,43127
+(defun coq-included-children 1165,43254
+(defun coq-process-file 1186,44093
+(defun coq-preprocessing 1201,44632
+(defun coq-fake-constant-markup 1216,45051
+(defun coq-create-span-menu 1238,45858
+(defconst module-kinds-table 1258,46435
+(defconst modtype-kinds-table1262,46585
+(defun coq-insert-section-or-module 1266,46714
+(defconst reqkinds-kinds-table1289,47574
+(defun coq-insert-requires 1294,47719
+(defun coq-end-Section 1310,48225
+(defun coq-insert-intros 1328,48809
+(defun coq-insert-match 1340,49333
+(defun coq-insert-tactic 1372,50511
+(defun coq-insert-tactical 1378,50750
+(defun coq-insert-command 1384,50999
+(defun coq-insert-term 1390,51243
+(define-key coq-keymap 1396,51440
+(define-key coq-keymap 1397,51498
+(define-key coq-keymap 1398,51555
+(define-key coq-keymap 1399,51624
+(define-key coq-keymap 1400,51680
+(define-key coq-keymap 1401,51729
+(define-key coq-keymap 1402,51787
+(define-key coq-keymap 1404,51848
+(define-key coq-keymap 1405,51907
+(define-key coq-keymap 1407,51971
+(define-key coq-keymap 1408,52031
+(define-key coq-keymap 1410,52087
+(define-key coq-keymap 1411,52137
+(define-key coq-keymap 1412,52187
+(define-key coq-keymap 1413,52237
+(define-key coq-keymap 1414,52291
+(define-key coq-keymap 1415,52350
+(defvar last-coq-error-location 1425,52533
+(defun coq-get-last-error-location 1434,52932
+(defun coq-highlight-error 1467,54329
+(defvar coq-allow-highlight-error 1532,56884
+(defun coq-decide-highlight-error 1538,57150
+(defun coq-highlight-error-hook 1543,57312
+(defun first-word-of-buffer 1554,57705
+(defun coq-show-first-goal 1564,57937
+(defvar coq-modeline-string2 1580,58606
+(defvar coq-modeline-string1 1581,58650
+(defvar coq-modeline-string0 1582,58693
+(defun coq-build-subgoals-string 1583,58738
+(defun coq-update-minor-mode-alist 1588,58906
+(defun is-not-split-vertic 1614,59974
+(defun optim-resp-windows 1623,60413
 
 coq/coq-indent.el,2259
 (defconst coq-any-command-regexp17,315
@@ -245,81 +245,91 @@ coq/coq-indent.el,2259
 (defun coq-indent-region 731,29199
 
 coq/coq-local-vars.el,279
-(defconst coq-local-vars-doc 17,306
-(defun coq-insert-coq-prog-name 75,2832
-(defun coq-read-directory 83,3185
-(defun coq-extract-directories-from-args 98,3874
-(defun coq-ask-prog-args 113,4384
-(defun coq-ask-prog-name 133,5426
-(defun coq-ask-insert-coq-prog-name 148,6067
-
-coq/coq-syntax.el,2612
-(defcustom coq-prog-name 12,357
-(defvar coq-version-is-V8 33,1303
-(defvar coq-version-is-V8-0 35,1382
-(defvar coq-version-is-V8-1 42,1760
-(defun coq-determine-version 51,2193
-(defcustom coq-user-tactics-db 96,4051
-(defcustom coq-user-commands-db 113,4564
-(defcustom coq-user-tacticals-db 129,5083
-(defcustom coq-user-solve-tactics-db 145,5604
-(defcustom coq-user-reserved-db 163,6125
-(defvar coq-tactics-db181,6656
-(defvar coq-solve-tactics-db336,14724
-(defvar coq-tacticals-db359,15522
-(defvar coq-decl-db384,16458
-(defvar coq-defn-db406,17676
-(defvar coq-goal-starters-db459,21662
-(defvar coq-other-commands-db486,23217
-(defvar coq-commands-db609,32371
-(defvar coq-terms-db616,32597
-(defun coq-count-match 680,35249
-(defun coq-goal-command-str-v80-p 699,36112
-(defun coq-module-opening-p 722,36985
-(defun coq-section-command-p 733,37401
-(defun coq-goal-command-str-v81-p 737,37498
-(defun coq-goal-command-p-v81 752,38167
-(defun coq-goal-command-str-p 762,38507
-(defun coq-goal-command-p 772,38873
-(defvar coq-keywords-save-strict780,39185
-(defvar coq-keywords-save789,39298
-(defun coq-save-command-p 793,39376
-(defvar coq-keywords-kill-goal 802,39670
-(defvar coq-keywords-state-changing-misc-commands806,39761
-(defvar coq-keywords-goal809,39886
-(defvar coq-keywords-decl812,39969
-(defvar coq-keywords-defn815,40043
-(defvar coq-keywords-state-changing-commands819,40118
-(defvar coq-keywords-state-preserving-commands828,40379
-(defvar coq-keywords-commands833,40595
-(defvar coq-solve-tactics838,40744
-(defvar coq-tacticals842,40865
-(defvar coq-reserved848,41004
-(defvar coq-state-changing-tactics859,41333
-(defvar coq-state-preserving-tactics862,41442
-(defvar coq-tactics866,41556
-(defvar coq-retractable-instruct869,41645
-(defvar coq-non-retractable-instruct872,41755
-(defvar coq-keywords876,41883
-(defvar coq-symbols883,42051
-(defvar coq-error-regexp 902,42264
-(defvar coq-id 905,42492
-(defvar coq-id-shy 906,42517
-(defvar coq-ids 908,42571
-(defun coq-first-abstr-regexp 910,42612
-(defvar coq-font-lock-terms913,42708
-(defconst coq-save-command-regexp-strict931,43669
-(defconst coq-save-command-regexp935,43836
-(defconst coq-save-with-hole-regexp939,43989
-(defconst coq-goal-command-regexp943,44148
-(defconst coq-goal-with-hole-regexp946,44248
-(defconst coq-decl-with-hole-regexp950,44381
-(defconst coq-defn-with-hole-regexp954,44514
-(defconst coq-with-with-hole-regexp964,44803
-(defvar coq-font-lock-keywords-1970,45096
-(defvar coq-font-lock-keywords 994,46360
-(defun coq-init-syntax-table 996,46418
-(defconst coq-generic-expression1025,47317
+(defconst coq-local-vars-doc 17,304
+(defun coq-insert-coq-prog-name 75,2830
+(defun coq-read-directory 83,3183
+(defun coq-extract-directories-from-args 98,3872
+(defun coq-ask-prog-args 113,4382
+(defun coq-ask-prog-name 133,5424
+(defun coq-ask-insert-coq-prog-name 148,6065
+
+coq/coq-syntax.el,2614
+(defcustom coq-prog-name 12,354
+(defvar coq-version-is-V8 33,1300
+(defvar coq-version-is-V8-0 35,1379
+(defvar coq-version-is-V8-1 42,1757
+(defun coq-determine-version 51,2190
+(defcustom coq-user-tactics-db 96,4048
+(defcustom coq-user-commands-db 113,4561
+(defcustom coq-user-tacticals-db 129,5080
+(defcustom coq-user-solve-tactics-db 145,5601
+(defcustom coq-user-reserved-db 163,6122
+(defvar coq-tactics-db181,6653
+(defvar coq-solve-tactics-db336,14721
+(defvar coq-tacticals-db360,15568
+(defvar coq-decl-db384,16455
+(defvar coq-defn-db406,17673
+(defvar coq-goal-starters-db459,21659
+(defvar coq-other-commands-db486,23214
+(defvar coq-commands-db610,32411
+(defvar coq-terms-db617,32637
+(defun coq-count-match 681,35289
+(defun coq-goal-command-str-v80-p 700,36152
+(defun coq-module-opening-p 723,37025
+(defun coq-section-command-p 734,37441
+(defun coq-goal-command-str-v81-p 738,37538
+(defun coq-goal-command-p-v81 753,38207
+(defun coq-goal-command-str-p 763,38547
+(defun coq-goal-command-p 773,38913
+(defvar coq-keywords-save-strict781,39225
+(defvar coq-keywords-save790,39338
+(defun coq-save-command-p 794,39416
+(defvar coq-keywords-kill-goal 803,39710
+(defvar coq-keywords-state-changing-misc-commands807,39801
+(defvar coq-keywords-goal810,39926
+(defvar coq-keywords-decl813,40009
+(defvar coq-keywords-defn816,40083
+(defvar coq-keywords-state-changing-commands820,40158
+(defvar coq-keywords-state-preserving-commands829,40419
+(defvar coq-keywords-commands834,40635
+(defvar coq-solve-tactics839,40784
+(defvar coq-tacticals843,40905
+(defvar coq-reserved849,41044
+(defvar coq-state-changing-tactics860,41373
+(defvar coq-state-preserving-tactics863,41482
+(defvar coq-tactics867,41596
+(defvar coq-retractable-instruct870,41685
+(defvar coq-non-retractable-instruct873,41795
+(defvar coq-keywords877,41923
+(defvar coq-symbols884,42091
+(defvar coq-error-regexp 903,42304
+(defvar coq-id 906,42532
+(defvar coq-id-shy 907,42557
+(defvar coq-ids 909,42611
+(defun coq-first-abstr-regexp 911,42652
+(defvar coq-font-lock-terms914,42748
+(defconst coq-save-command-regexp-strict934,43711
+(defconst coq-save-command-regexp938,43878
+(defconst coq-save-with-hole-regexp942,44031
+(defconst coq-goal-command-regexp946,44190
+(defconst coq-goal-with-hole-regexp949,44290
+(defconst coq-decl-with-hole-regexp953,44423
+(defconst coq-defn-with-hole-regexp960,44672
+(defconst coq-with-with-hole-regexp970,44961
+(defvar coq-font-lock-keywords-1976,45254
+(defvar coq-font-lock-keywords 1001,46519
+(defun coq-init-syntax-table 1003,46577
+(defconst coq-generic-expression1032,47476
+
+coq/coq-unicode-tokens.el,290
+(defconst coq-token-format 18,631
+(defconst coq-charref-format 19,664
+(defconst coq-token-prefix 20,698
+(defconst coq-token-suffix 21,730
+(defconst coq-token-match 22,762
+(defconst coq-hexcode-match 23,793
+(defcustom coq-token-name-alist 25,827
+(defcustom coq-shortcut-alist44,1557
 
 coq/x-symbol-coq.el,1748
 (defvar x-symbol-coq-required-fonts 19,510
@@ -371,214 +381,214 @@ demoisa/demoisa.el,349
 (define-derived-mode demoisa-goals-mode 131,4323
 
 isar/isabelle-system.el,1401
-(defgroup isabelle 26,776
-(defcustom isabelle-web-page30,904
-(defcustom isa-isatool-command41,1199
-(defvar isatool-not-found 71,2261
-(defun isa-set-isatool-command 74,2374
-(defun isa-shell-command-to-string 97,3318
-(defun isa-getenv 103,3542
-(defcustom isabelle-program-name123,4229
-(defvar isabelle-prog-name 149,5159
-(defun isa-tool-list-logics 152,5286
-(defcustom isabelle-logics-available 159,5523
-(defcustom isabelle-chosen-logic 170,5887
-(defun isabelle-command-line 183,6355
-(defun isabelle-choose-logic 206,7312
-(defun isa-view-doc 228,8278
-(defun isa-tool-list-docs 237,8542
-(defconst isabelle-verbatim-regexp 264,9574
-(defun isabelle-verbatim 267,9716
-(defcustom isabelle-refresh-logics 274,9877
-(defvar isabelle-docs-menu 282,10204
-(defvar isabelle-logics-menu-entries 290,10491
-(defun isabelle-logics-menu-calculate 293,10564
-(defvar isabelle-time-to-refresh-logics 312,11127
-(defun isabelle-logics-menu-refresh 316,11222
-(defun isabelle-logics-menu-filter 333,11919
-(defun isabelle-menu-bar-update-logics 339,12129
-(defvar isabelle-logics-menu350,12468
-(defun isabelle-load-isar-keywords 363,13080
-(defpgdefault menu-entries384,13821
-(defpgdefault help-menu-entries 387,13873
-(defun isabelle-convert-idmarkup-to-subterm 415,14631
-(defun isabelle-create-span-menu 439,15642
-(defun isabelle-xml-sml-escapes 455,16084
-(defun isabelle-process-pgip 458,16185
+(defgroup isabelle 26,775
+(defcustom isabelle-web-page30,903
+(defcustom isa-isatool-command41,1198
+(defvar isatool-not-found 71,2260
+(defun isa-set-isatool-command 74,2373
+(defun isa-shell-command-to-string 97,3317
+(defun isa-getenv 103,3541
+(defcustom isabelle-program-name123,4228
+(defvar isabelle-prog-name 149,5158
+(defun isa-tool-list-logics 152,5285
+(defcustom isabelle-logics-available 159,5522
+(defcustom isabelle-chosen-logic 170,5886
+(defun isabelle-command-line 183,6354
+(defun isabelle-choose-logic 206,7311
+(defun isa-view-doc 228,8277
+(defun isa-tool-list-docs 237,8541
+(defconst isabelle-verbatim-regexp 264,9573
+(defun isabelle-verbatim 267,9715
+(defcustom isabelle-refresh-logics 274,9876
+(defvar isabelle-docs-menu 282,10203
+(defvar isabelle-logics-menu-entries 290,10490
+(defun isabelle-logics-menu-calculate 293,10563
+(defvar isabelle-time-to-refresh-logics 312,11126
+(defun isabelle-logics-menu-refresh 316,11221
+(defun isabelle-logics-menu-filter 333,11918
+(defun isabelle-menu-bar-update-logics 339,12128
+(defvar isabelle-logics-menu350,12467
+(defun isabelle-load-isar-keywords 363,13079
+(defpgdefault menu-entries384,13820
+(defpgdefault help-menu-entries 387,13872
+(defun isabelle-convert-idmarkup-to-subterm 415,14630
+(defun isabelle-create-span-menu 439,15641
+(defun isabelle-xml-sml-escapes 455,16083
+(defun isabelle-process-pgip 458,16184
 
 isar/isar.el,1204
-(defcustom isar-keywords-name 31,721
-(defpgdefault completion-table 48,1244
-(defcustom isar-web-page50,1297
-(defun isar-strip-terminators 64,1633
-(defun isar-markup-ml 77,2010
-(defun isar-mode-config-set-variables 82,2145
-(defun isar-shell-mode-config-set-variables 149,5265
-(defun isar-remove-file 247,9414
-(defun isar-shell-compute-new-files-list 257,9777
-(defun isar-activate-scripting 268,10243
-(define-derived-mode isar-shell-mode 277,10413
-(define-derived-mode isar-response-mode 282,10536
-(define-derived-mode isar-goals-mode 287,10718
-(define-derived-mode isar-mode 292,10893
-(defpgdefault menu-entries346,12865
-(defun isar-count-undos 376,14104
-(defun isar-find-and-forget 403,15218
-(defun isar-goal-command-p 442,16798
-(defun isar-global-save-command-p 447,16975
-(defvar isar-current-goal 468,17836
-(defun isar-state-preserving-p 471,17902
-(defvar isar-shell-current-line-width 496,19099
-(defun isar-shell-adjust-line-width 501,19291
-(defun isar-preprocessing 524,20182
-(defun isar-mode-config 547,21449
-(defun isar-shell-mode-config 558,21950
-(defun isar-response-mode-config 569,22309
-(defun isar-goals-mode-config 578,22552
-(defun isar-goalhyplit-test 589,22884
+(defcustom isar-keywords-name 31,720
+(defpgdefault completion-table 48,1243
+(defcustom isar-web-page50,1296
+(defun isar-strip-terminators 64,1632
+(defun isar-markup-ml 77,2009
+(defun isar-mode-config-set-variables 82,2144
+(defun isar-shell-mode-config-set-variables 150,5325
+(defun isar-remove-file 247,9384
+(defun isar-shell-compute-new-files-list 257,9747
+(defun isar-activate-scripting 268,10213
+(define-derived-mode isar-shell-mode 277,10383
+(define-derived-mode isar-response-mode 282,10506
+(define-derived-mode isar-goals-mode 287,10688
+(define-derived-mode isar-mode 292,10863
+(defpgdefault menu-entries346,12835
+(defun isar-count-undos 376,14074
+(defun isar-find-and-forget 403,15188
+(defun isar-goal-command-p 442,16768
+(defun isar-global-save-command-p 447,16945
+(defvar isar-current-goal 468,17806
+(defun isar-state-preserving-p 471,17872
+(defvar isar-shell-current-line-width 496,19069
+(defun isar-shell-adjust-line-width 501,19261
+(defun isar-preprocessing 524,20152
+(defun isar-mode-config 547,21419
+(defun isar-shell-mode-config 558,21920
+(defun isar-response-mode-config 569,22279
+(defun isar-goals-mode-config 578,22522
+(defun isar-goalhyplit-test 589,22854
 
 isar/isar-find-theorems.el,778
-(defun isar-find-theorems-minibuffer 18,715
-(defun isar-find-theorems-form 32,1334
-(defvar isar-find-theorems-data 74,3134
-(defvar isar-find-theorems-widget-number 88,3469
-(defvar isar-find-theorems-widget-pattern 91,3567
-(defvar isar-find-theorems-widget-intro 94,3659
-(defvar isar-find-theorems-widget-elim 97,3745
-(defvar isar-find-theorems-widget-dest 100,3829
-(defvar isar-find-theorems-widget-name 103,3913
-(defvar isar-find-theorems-widget-simp 106,4000
-(defun isar-find-theorems-create-searchform111,4146
-(defun isar-find-theorems-create-help 251,8761
-(defun isar-find-theorems-submit-searchform294,10933
-(defun isar-find-theorems-parse-criteria 372,13310
-(defun isar-find-theorems-parse-number 465,16410
-(defun isar-find-theorems-filter-empty 475,16687
+(defun isar-find-theorems-minibuffer 18,712
+(defun isar-find-theorems-form 32,1331
+(defvar isar-find-theorems-data 74,3131
+(defvar isar-find-theorems-widget-number 88,3466
+(defvar isar-find-theorems-widget-pattern 91,3564
+(defvar isar-find-theorems-widget-intro 94,3656
+(defvar isar-find-theorems-widget-elim 97,3742
+(defvar isar-find-theorems-widget-dest 100,3826
+(defvar isar-find-theorems-widget-name 103,3910
+(defvar isar-find-theorems-widget-simp 106,3997
+(defun isar-find-theorems-create-searchform111,4143
+(defun isar-find-theorems-create-help 251,8758
+(defun isar-find-theorems-submit-searchform294,10930
+(defun isar-find-theorems-parse-criteria 372,13307
+(defun isar-find-theorems-parse-number 465,16407
+(defun isar-find-theorems-filter-empty 475,16684
 
 isar/isar-keywords.el,1052
-(defconst isar-keywords-major13,487
-(defconst isar-keywords-minor206,3647
-(defconst isar-keywords-control262,4401
-(defconst isar-keywords-diag282,4878
-(defconst isar-keywords-theory-begin338,5837
-(defconst isar-keywords-theory-switch341,5890
-(defconst isar-keywords-theory-end344,5945
-(defconst isar-keywords-theory-heading347,5993
-(defconst isar-keywords-theory-decl353,6100
-(defconst isar-keywords-theory-script412,7081
-(defconst isar-keywords-theory-goal416,7158
-(defconst isar-keywords-qed429,7375
-(defconst isar-keywords-qed-block436,7461
-(defconst isar-keywords-qed-global439,7508
-(defconst isar-keywords-proof-heading442,7557
-(defconst isar-keywords-proof-goal447,7640
-(defconst isar-keywords-proof-block454,7739
-(defconst isar-keywords-proof-open458,7801
-(defconst isar-keywords-proof-close461,7847
-(defconst isar-keywords-proof-chain464,7894
-(defconst isar-keywords-proof-decl471,7997
-(defconst isar-keywords-proof-asm480,8118
-(defconst isar-keywords-proof-asm-goal487,8213
-(defconst isar-keywords-proof-script490,8268
+(defconst isar-keywords-major13,481
+(defconst isar-keywords-minor206,3641
+(defconst isar-keywords-control262,4395
+(defconst isar-keywords-diag282,4872
+(defconst isar-keywords-theory-begin338,5831
+(defconst isar-keywords-theory-switch341,5884
+(defconst isar-keywords-theory-end344,5939
+(defconst isar-keywords-theory-heading347,5987
+(defconst isar-keywords-theory-decl353,6094
+(defconst isar-keywords-theory-script412,7075
+(defconst isar-keywords-theory-goal416,7152
+(defconst isar-keywords-qed429,7369
+(defconst isar-keywords-qed-block436,7455
+(defconst isar-keywords-qed-global439,7502
+(defconst isar-keywords-proof-heading442,7551
+(defconst isar-keywords-proof-goal447,7634
+(defconst isar-keywords-proof-block454,7733
+(defconst isar-keywords-proof-open458,7795
+(defconst isar-keywords-proof-close461,7841
+(defconst isar-keywords-proof-chain464,7888
+(defconst isar-keywords-proof-decl471,7991
+(defconst isar-keywords-proof-asm480,8112
+(defconst isar-keywords-proof-asm-goal487,8207
+(defconst isar-keywords-proof-script490,8262
 
 isar/isar-mmm.el,83
 (defconst isar-start-latex-regexp 23,697
 (defconst isar-start-sml-regexp 35,1130
 
 isar/isar-syntax.el,3471
-(defconst isar-script-syntax-table-entries20,472
-(defconst isar-script-syntax-table-alist61,1503
-(defun isar-init-syntax-table 70,1793
-(defun isar-init-output-syntax-table 78,2040
-(defconst isar-keyword-begin 94,2487
-(defconst isar-keyword-end 95,2525
-(defconst isar-keywords-theory-enclose97,2560
-(defconst isar-keywords-theory102,2705
-(defconst isar-keywords-save107,2850
-(defconst isar-keywords-proof-enclose112,2979
-(defconst isar-keywords-proof118,3161
-(defconst isar-keywords-proof-context125,3366
-(defconst isar-keywords-local-goal129,3480
-(defconst isar-keywords-proper133,3592
-(defconst isar-keywords-improper138,3725
-(defconst isar-keywords-outline143,3871
-(defconst isar-keywords-fume146,3936
-(defconst isar-keywords-indent-open153,4154
-(defconst isar-keywords-indent-close159,4338
-(defconst isar-keywords-indent-enclose163,4443
-(defun isar-regexp-simple-alt 172,4658
-(defun isar-ids-to-regexp 192,5418
-(defconst isar-ext-first 226,6824
-(defconst isar-ext-rest 227,6891
-(defconst isar-long-id-stuff 229,6963
-(defconst isar-id 230,7037
-(defconst isar-idx 231,7107
-(defconst isar-string 233,7166
-(defconst isar-any-command-regexp235,7226
-(defconst isar-name-regexp239,7360
-(defconst isar-improper-regexp245,7655
-(defconst isar-save-command-regexp249,7803
-(defconst isar-global-save-command-regexp252,7904
-(defconst isar-goal-command-regexp255,8018
-(defconst isar-local-goal-command-regexp258,8126
-(defconst isar-comment-start 261,8239
-(defconst isar-comment-end 262,8274
-(defconst isar-comment-start-regexp 263,8307
-(defconst isar-comment-end-regexp 264,8378
-(defconst isar-string-start-regexp 266,8446
-(defconst isar-string-end-regexp 267,8498
-(defconst isar-antiq-regexp276,8751
-(defconst isar-nesting-regexp283,8912
-(defun isar-nesting 286,9010
-(defun isar-match-nesting 298,9431
-(defface isabelle-class-name-face310,9762
-(defface isabelle-tfree-name-face320,10037
-(defface isabelle-tvar-name-face330,10318
-(defface isabelle-free-name-face340,10598
-(defface isabelle-bound-name-face350,10874
-(defface isabelle-var-name-face360,11153
-(defconst isabelle-class-name-face 370,11432
-(defconst isabelle-tfree-name-face 371,11494
-(defconst isabelle-tvar-name-face 372,11556
-(defconst isabelle-free-name-face 373,11617
-(defconst isabelle-bound-name-face 374,11678
-(defconst isabelle-var-name-face 375,11740
-(defconst isar-font-lock-local378,11802
-(defvar isar-font-lock-keywords-1383,11968
-(defvar isar-output-font-lock-keywords-1397,12834
-(defvar isar-goals-font-lock-keywords424,14458
-(defconst isar-undo 458,15137
-(defun isar-remove 460,15199
-(defun isar-undos 463,15274
-(defun isar-cannot-undo 467,15367
-(defconst isar-theory-start-regexp470,15437
-(defconst isar-end-regexp476,15602
-(defconst isar-undo-fail-regexp480,15703
-(defconst isar-undo-skip-regexp484,15807
-(defconst isar-undo-ignore-regexp487,15928
-(defconst isar-undo-remove-regexp490,15993
-(defconst isar-any-entity-regexp498,16168
-(defconst isar-named-entity-regexp503,16355
-(defconst isar-unnamed-entity-regexp508,16532
-(defconst isar-next-entity-regexps511,16634
-(defconst isar-generic-expression519,16945
-(defconst isar-indent-any-regexp530,17262
-(defconst isar-indent-inner-regexp532,17355
-(defconst isar-indent-enclose-regexp534,17421
-(defconst isar-indent-open-regexp536,17537
-(defconst isar-indent-close-regexp538,17647
-(defconst isar-outline-regexp544,17784
-(defconst isar-outline-heading-end-regexp 548,17937
-
-isar/isar-unicode-tokens.el,295
-(defconst isar-token-format 16,478
-(defconst isar-charref-format 17,516
-(defconst isar-token-prefix 18,558
-(defconst isar-token-suffix 19,593
-(defconst isar-token-match 20,626
-(defconst isar-hexcode-match 21,680
-(defcustom isar-token-name-alist23,742
-(defvar isar-shortcut-alist337,8354
+(defconst isar-script-syntax-table-entries20,471
+(defconst isar-script-syntax-table-alist61,1502
+(defun isar-init-syntax-table 70,1792
+(defun isar-init-output-syntax-table 78,2039
+(defconst isar-keyword-begin 94,2486
+(defconst isar-keyword-end 95,2524
+(defconst isar-keywords-theory-enclose97,2559
+(defconst isar-keywords-theory102,2704
+(defconst isar-keywords-save107,2849
+(defconst isar-keywords-proof-enclose112,2978
+(defconst isar-keywords-proof118,3160
+(defconst isar-keywords-proof-context125,3365
+(defconst isar-keywords-local-goal129,3479
+(defconst isar-keywords-proper133,3591
+(defconst isar-keywords-improper138,3724
+(defconst isar-keywords-outline143,3870
+(defconst isar-keywords-fume146,3935
+(defconst isar-keywords-indent-open153,4153
+(defconst isar-keywords-indent-close159,4337
+(defconst isar-keywords-indent-enclose163,4442
+(defun isar-regexp-simple-alt 172,4657
+(defun isar-ids-to-regexp 192,5417
+(defconst isar-ext-first 226,6823
+(defconst isar-ext-rest 227,6890
+(defconst isar-long-id-stuff 229,6962
+(defconst isar-id 230,7036
+(defconst isar-idx 231,7106
+(defconst isar-string 233,7165
+(defconst isar-any-command-regexp235,7225
+(defconst isar-name-regexp239,7359
+(defconst isar-improper-regexp245,7654
+(defconst isar-save-command-regexp249,7802
+(defconst isar-global-save-command-regexp252,7903
+(defconst isar-goal-command-regexp255,8017
+(defconst isar-local-goal-command-regexp258,8125
+(defconst isar-comment-start 261,8238
+(defconst isar-comment-end 262,8273
+(defconst isar-comment-start-regexp 263,8306
+(defconst isar-comment-end-regexp 264,8377
+(defconst isar-string-start-regexp 266,8445
+(defconst isar-string-end-regexp 267,8497
+(defconst isar-antiq-regexp276,8750
+(defconst isar-nesting-regexp283,8911
+(defun isar-nesting 286,9009
+(defun isar-match-nesting 298,9430
+(defface isabelle-class-name-face310,9761
+(defface isabelle-tfree-name-face320,10036
+(defface isabelle-tvar-name-face330,10317
+(defface isabelle-free-name-face340,10597
+(defface isabelle-bound-name-face350,10873
+(defface isabelle-var-name-face360,11152
+(defconst isabelle-class-name-face 370,11431
+(defconst isabelle-tfree-name-face 371,11493
+(defconst isabelle-tvar-name-face 372,11555
+(defconst isabelle-free-name-face 373,11616
+(defconst isabelle-bound-name-face 374,11677
+(defconst isabelle-var-name-face 375,11739
+(defconst isar-font-lock-local378,11801
+(defvar isar-font-lock-keywords-1383,11967
+(defvar isar-output-font-lock-keywords-1397,12833
+(defvar isar-goals-font-lock-keywords424,14457
+(defconst isar-undo 458,15136
+(defun isar-remove 460,15198
+(defun isar-undos 463,15273
+(defun isar-cannot-undo 467,15379
+(defconst isar-theory-start-regexp470,15449
+(defconst isar-end-regexp476,15614
+(defconst isar-undo-fail-regexp480,15715
+(defconst isar-undo-skip-regexp484,15819
+(defconst isar-undo-ignore-regexp487,15940
+(defconst isar-undo-remove-regexp490,16005
+(defconst isar-any-entity-regexp498,16180
+(defconst isar-named-entity-regexp503,16367
+(defconst isar-unnamed-entity-regexp508,16544
+(defconst isar-next-entity-regexps511,16646
+(defconst isar-generic-expression519,16957
+(defconst isar-indent-any-regexp530,17274
+(defconst isar-indent-inner-regexp532,17367
+(defconst isar-indent-enclose-regexp534,17433
+(defconst isar-indent-open-regexp536,17549
+(defconst isar-indent-close-regexp538,17659
+(defconst isar-outline-regexp544,17796
+(defconst isar-outline-heading-end-regexp 548,17949
+
+isar/isar-unicode-tokens.el,298
+(defconst isar-token-format 14,433
+(defconst isar-charref-format 15,471
+(defconst isar-token-prefix 16,513
+(defconst isar-token-suffix 17,548
+(defconst isar-token-match 18,581
+(defconst isar-hexcode-match 19,635
+(defcustom isar-token-name-alist21,697
+(defcustom isar-shortcut-alist354,8635
 
 isar/x-symbol-isar.el,1775
 (defvar x-symbol-isar-required-fonts 15,498
@@ -698,23 +708,23 @@ lego/lego-syntax.el,600
 (defun lego-init-syntax-table 110,4134
 
 phox/phox.el,644
-(defcustom phox-prog-name 31,910
-(defcustom phox-sym-lock-enabled 36,1012
-(defcustom phox-web-page42,1119
-(defcustom phox-doc-dir 48,1269
-(defcustom phox-lib-dir 54,1417
-(defcustom phox-tags-program 60,1561
-(defcustom phox-tags-doc 66,1741
-(defcustom phox-etags 72,1879
-(defpgdefault menu-entries93,2331
-(defun phox-config 107,2524
-(defun phox-shell-config 153,4561
-(define-derived-mode phox-mode 178,5490
-(define-derived-mode phox-shell-mode 198,6102
-(define-derived-mode phox-response-mode 203,6230
-(define-derived-mode phox-goals-mode 215,6657
-(defpgdefault completion-table240,7525
-(defpgdefault x-symbol-language 248,7630
+(defcustom phox-prog-name 31,909
+(defcustom phox-sym-lock-enabled 36,1011
+(defcustom phox-web-page42,1118
+(defcustom phox-doc-dir 48,1268
+(defcustom phox-lib-dir 54,1416
+(defcustom phox-tags-program 60,1560
+(defcustom phox-tags-doc 66,1740
+(defcustom phox-etags 72,1878
+(defpgdefault menu-entries93,2330
+(defun phox-config 107,2523
+(defun phox-shell-config 153,4560
+(define-derived-mode phox-mode 178,5489
+(define-derived-mode phox-shell-mode 198,6101
+(define-derived-mode phox-response-mode 203,6229
+(define-derived-mode phox-goals-mode 215,6656
+(defpgdefault completion-table240,7524
+(defpgdefault x-symbol-language 248,7629
 
 phox/phox-extraction.el,382
 (defvar phox-prog-orig 11,480
@@ -1166,15 +1176,16 @@ twelf/twelf-old.el,6958
 (defun twelf-server-remove-menu 2651,107274
 (defun twelf-server-reset-menu 2655,107386
 
-generic/pg-assoc.el,354
+generic/pg-assoc.el,402
 (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
+(defconst pg-assoc-active-area-keymap 146,4391
+(defun pg-assoc-make-top-span 153,4616
+(defun pg-assoc-analyse-structure 190,6081
 
 generic/pg-autotest.el,442
 (defvar pg-autotest-success 24,543
@@ -1190,22 +1201,22 @@ generic/pg-autotest.el,442
 (defun pg-autotest-finished 112,3339
 
 generic/pg-custom.el,600
-(defpgcustom x-symbol-enable 30,1004
-(defpgcustom x-symbol-language 40,1430
-(defpgcustom maths-menu-enable 45,1652
-(defpgcustom unicode-tokens-enable 51,1832
-(defpgcustom mmm-enable 57,2009
-(defpgcustom script-indent 66,2363
-(defconst proof-toolbar-entries-default71,2500
-(defpgcustom toolbar-entries 105,4413
-(defpgcustom prog-args 123,5133
-(defpgcustom prog-env 136,5708
-(defpgcustom favourites 145,6134
-(defpgcustom menu-entries 150,6323
-(defpgcustom help-menu-entries 157,6559
-(defpgcustom keymap 164,6822
-(defpgcustom completion-table 169,6994
-(defpgcustom tags-program 180,7368
+(defpgcustom x-symbol-enable 32,1065
+(defpgcustom x-symbol-language 42,1491
+(defpgcustom maths-menu-enable 47,1713
+(defpgcustom unicode-tokens-enable 53,1893
+(defpgcustom mmm-enable 59,2070
+(defpgcustom script-indent 68,2424
+(defconst proof-toolbar-entries-default73,2561
+(defpgcustom toolbar-entries 107,4474
+(defpgcustom prog-args 125,5194
+(defpgcustom prog-env 138,5769
+(defpgcustom favourites 147,6195
+(defpgcustom menu-entries 152,6384
+(defpgcustom help-menu-entries 159,6620
+(defpgcustom keymap 166,6883
+(defpgcustom completion-table 171,7055
+(defpgcustom tags-program 182,7429
 
 generic/pg-goals.el,363
 (define-derived-mode proof-goals-mode 30,632
@@ -1216,153 +1227,148 @@ generic/pg-goals.el,363
 (defun pg-goals-button-action 194,6715
 (defun proof-expand-path 215,7687
 (defun pg-goals-construct-command 224,7929
-(defun pg-goals-get-subterm-help 253,8950
-
-generic/pg-metadata.el,127
-(defcustom pg-metadata-default-directory 29,745
-(defface proof-preparsed-span34,919
-(defun pg-metadata-filename-for 45,1181
-
-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
+(defun pg-goals-get-subterm-help 256,9117
+
+generic/pg-pbrpm.el,1803
+(defvar pg-pbrpm-use-buffer-menu 22,547
+(defvar pg-pbrpm-start-goal-regexp 25,669
+(defvar pg-pbrpm-start-goal-regexp-par-num 29,826
+(defvar pg-pbrpm-end-goal-regexp 32,949
+(defvar pg-pbrpm-start-hyp-regexp 36,1101
+(defvar pg-pbrpm-start-hyp-regexp-par-num 40,1262
+(defvar pg-pbrpm-start-concl-regexp 44,1469
+(defvar pg-pbrpm-auto-select-regexp 48,1633
+(defvar pg-pbrpm-buffer-menu 55,1794
+(defvar pg-pbrpm-spans 56,1828
+(defvar pg-pbrpm-goal-description 57,1856
+(defvar pg-pbrpm-windows-dialog-bug 58,1895
+(defvar pbrpm-menu-desc 59,1936
+(defun pg-pbrpm-erase-buffer-menu 61,1966
+(defun pg-pbrpm-menu-change-hook 68,2150
+(defun pg-pbrpm-create-reset-buffer-menu 86,2726
+(defun pg-pbrpm-analyse-goal-buffer 101,3355
+(defun pg-pbrpm-button-action 161,5765
+(defun pg-pbrpm-exists 168,5991
+(defun pg-pbrpm-eliminate-id 172,6103
+(defun pg-pbrpm-build-menu 180,6349
+(defun pg-pbrpm-setup-span 253,8976
+(defun pg-pbrpm-run-command 313,11294
+(defun pg-pbrpm-get-pos-info 342,12604
+(defun pg-pbrpm-get-region-info 384,13911
+(defun pg-pbrpm-auto-select-around-point 395,14325
+(defun pg-pbrpm-translate-position 410,14855
+(defun pg-pbrpm-process-click 418,15113
+(defvar pg-pbrpm-remember-region-selected-region 438,16138
+(defvar pg-pbrpm-regions-list 439,16192
+(defun pg-pbrpm-erase-regions-list 441,16228
+(defun pg-pbrpm-filter-regions-list 450,16536
+(defface pg-pbrpm-multiple-selection-face457,16799
+(defface pg-pbrpm-menu-input-face465,17001
+(defun pg-pbrpm-do-remember-region 473,17191
+(defun pg-pbrpm-remember-region-drag-up-hook 494,18039
+(defun pg-pbrpm-remember-region-click-hook 498,18210
+(defun pg-pbrpm-remember-region 503,18395
+(defun pg-pbrpm-process-region 517,19110
+(defun pg-pbrpm-process-regions-list 535,19839
+(defun pg-pbrpm-region-expression 539,20022
 
 generic/pg-pgip.el,2889
-(defalias 'pg-pgip-debug pg-pgip-debug
35,920
-(defalias 'pg-pgip-error pg-pgip-error
36,961
-(defalias 'pg-pgip-warning pg-pgip-warning
37,996
-(defconst pg-pgip-version-supported 39,1046
-(defun pg-pgip-process-packet 43,1152
-(defvar pg-pgip-last-seen-id 53,1724
-(defvar pg-pgip-last-seen-seq 54,1758
-(defun pg-pgip-process-pgip 56,1794
-(defun pg-pgip-process-msg 75,2725
-(defvar pg-pgip-post-process-functions89,3295
-(defun pg-pgip-post-process 99,3783
-(defun pg-pgip-process-askpgip 115,4394
-(defun pg-pgip-process-usespgip 121,4599
-(defun pg-pgip-process-usespgml 125,4763
-(defun pg-pgip-process-pgmlconfig 129,4927
-(defun pg-pgip-process-proverinfo 145,5544
-(defun pg-pgip-process-hasprefs 162,6209
-(defun pg-pgip-haspref 176,6841
-(defun pg-pgip-process-prefval 195,7617
-(defun pg-pgip-process-guiconfig 222,8326
-(defvar proof-assistant-idtables 229,8443
-(defun pg-pgip-process-ids 232,8560
-(defun pg-complete-idtable-symbol 258,9636
-(defalias 'pg-pgip-process-setids pg-pgip-process-setids
263,9728
-(defalias 'pg-pgip-process-addids pg-pgip-process-addids
264,9784
-(defalias 'pg-pgip-process-delids pg-pgip-process-delids
265,9840
-(defun pg-pgip-process-idvalue 268,9898
-(defun pg-pgip-process-menuadd 280,10234
-(defun pg-pgip-process-menudel 283,10277
-(defun pg-pgip-process-ready 292,10510
-(defun pg-pgip-process-cleardisplay 295,10551
-(defun pg-pgip-process-proofstate 309,11008
-(defun pg-pgip-process-normalresponse 313,11085
-(defun pg-pgip-process-errorresponse 317,11209
-(defun pg-pgip-process-scriptinsert 321,11332
-(defun pg-pgip-process-metainforesponse 326,11466
-(defun pg-pgip-process-informfileloaded 335,11707
-(defun pg-pgip-process-informfileretracted 341,11973
-(defun pg-pgip-process-brokerstatus 354,12450
-(defun pg-pgip-process-proveravailmsg 357,12498
-(defun pg-pgip-process-newprovermsg 360,12548
-(defun pg-pgip-process-proverstatusmsg 363,12596
-(defvar pg-pgip-srcids 372,12843
-(defun pg-pgip-process-newfile 376,12950
-(defun pg-pgip-process-filestatus 392,13538
-(defun pg-pgip-process-newobj 412,14193
-(defun pg-pgip-process-delobj 415,14235
-(defun pg-pgip-process-objectstatus 418,14277
-(defun pg-pgip-process-parsescript 432,14632
-(defun pg-pgip-get-pgiptype 455,15507
-(defun pg-pgip-default-for 475,16300
-(defun pg-pgip-subst-for 488,16695
-(defun pg-pgip-interpret-value 500,17038
-(defun pg-pgip-interpret-choice 518,17723
-(defun pg-pgip-string-of-command 549,18740
-(defconst pg-pgip-id566,19501
-(defvar pg-pgip-refseq 572,19781
-(defvar pg-pgip-refid 574,19878
-(defvar pg-pgip-seq 577,19970
-(defun pg-pgip-assemble-packet 579,20034
-(defun pg-pgip-issue 597,20846
-(defun pg-pgip-maybe-askpgip 614,21458
-(defun pg-pgip-askprefs 620,21649
-(defun pg-pgip-askids 624,21763
-(defun pg-pgip-reset 637,22051
-(defconst pg-pgip-start-element-regexp 668,22749
-(defconst pg-pgip-end-element-regexp 669,22801
+(defalias 'pg-pgip-debug pg-pgip-debug
35,919
+(defalias 'pg-pgip-error pg-pgip-error
36,960
+(defalias 'pg-pgip-warning pg-pgip-warning
37,995
+(defconst pg-pgip-version-supported 39,1045
+(defun pg-pgip-process-packet 43,1151
+(defvar pg-pgip-last-seen-id 53,1723
+(defvar pg-pgip-last-seen-seq 54,1757
+(defun pg-pgip-process-pgip 56,1793
+(defun pg-pgip-process-msg 75,2724
+(defvar pg-pgip-post-process-functions89,3294
+(defun pg-pgip-post-process 99,3782
+(defun pg-pgip-process-askpgip 115,4393
+(defun pg-pgip-process-usespgip 121,4598
+(defun pg-pgip-process-usespgml 125,4762
+(defun pg-pgip-process-pgmlconfig 129,4926
+(defun pg-pgip-process-proverinfo 145,5543
+(defun pg-pgip-process-hasprefs 162,6208
+(defun pg-pgip-haspref 176,6840
+(defun pg-pgip-process-prefval 195,7616
+(defun pg-pgip-process-guiconfig 222,8325
+(defvar proof-assistant-idtables 229,8442
+(defun pg-pgip-process-ids 232,8559
+(defun pg-complete-idtable-symbol 258,9635
+(defalias 'pg-pgip-process-setids pg-pgip-process-setids
263,9727
+(defalias 'pg-pgip-process-addids pg-pgip-process-addids
264,9783
+(defalias 'pg-pgip-process-delids pg-pgip-process-delids
265,9839
+(defun pg-pgip-process-idvalue 268,9897
+(defun pg-pgip-process-menuadd 280,10233
+(defun pg-pgip-process-menudel 283,10276
+(defun pg-pgip-process-ready 292,10509
+(defun pg-pgip-process-cleardisplay 295,10550
+(defun pg-pgip-process-proofstate 309,11007
+(defun pg-pgip-process-normalresponse 313,11084
+(defun pg-pgip-process-errorresponse 317,11208
+(defun pg-pgip-process-scriptinsert 321,11331
+(defun pg-pgip-process-metainforesponse 326,11465
+(defun pg-pgip-process-informfileloaded 335,11706
+(defun pg-pgip-process-informfileretracted 341,11972
+(defun pg-pgip-process-brokerstatus 354,12449
+(defun pg-pgip-process-proveravailmsg 357,12497
+(defun pg-pgip-process-newprovermsg 360,12547
+(defun pg-pgip-process-proverstatusmsg 363,12595
+(defvar pg-pgip-srcids 372,12842
+(defun pg-pgip-process-newfile 376,12949
+(defun pg-pgip-process-filestatus 392,13537
+(defun pg-pgip-process-newobj 412,14192
+(defun pg-pgip-process-delobj 415,14234
+(defun pg-pgip-process-objectstatus 418,14276
+(defun pg-pgip-process-parsescript 432,14631
+(defun pg-pgip-get-pgiptype 455,15506
+(defun pg-pgip-default-for 475,16299
+(defun pg-pgip-subst-for 488,16694
+(defun pg-pgip-interpret-value 500,17037
+(defun pg-pgip-interpret-choice 518,17722
+(defun pg-pgip-string-of-command 549,18739
+(defconst pg-pgip-id566,19500
+(defvar pg-pgip-refseq 572,19780
+(defvar pg-pgip-refid 574,19877
+(defvar pg-pgip-seq 577,19969
+(defun pg-pgip-assemble-packet 579,20033
+(defun pg-pgip-issue 597,20845
+(defun pg-pgip-maybe-askpgip 614,21457
+(defun pg-pgip-askprefs 620,21648
+(defun pg-pgip-askids 624,21762
+(defun pg-pgip-reset 637,22050
+(defconst pg-pgip-start-element-regexp 668,22748
+(defconst pg-pgip-end-element-regexp 669,22800
 
 generic/pg-response.el,1182
-(deflocal pg-response-eagerly-raise 31,731
-(define-derived-mode proof-response-mode 41,956
-(defun proof-response-config-done 67,2080
-(defvar pg-response-special-display-regexp 88,2855
-(defconst proof-multiframe-specifiers96,3261
-(defun proof-map-multiple-frame-specifiers 105,3618
-(defconst proof-multiframe-parameters116,4140
-(defun proof-multiple-frames-enable 125,4439
-(defun proof-three-window-enable 143,5083
-(defun proof-select-three-b 147,5147
-(defun proof-display-three-b 162,5616
-(defvar pg-frame-configuration 176,6108
-(defun pg-cache-frame-configuration 180,6255
-(defun proof-layout-windows 184,6426
-(defun proof-delete-other-frames 225,8249
-(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 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
+(deflocal pg-response-eagerly-raise 31,730
+(define-derived-mode proof-response-mode 41,955
+(defun proof-response-config-done 67,2079
+(defvar pg-response-special-display-regexp 88,2854
+(defconst proof-multiframe-specifiers96,3260
+(defun proof-map-multiple-frame-specifiers 105,3617
+(defconst proof-multiframe-parameters116,4139
+(defun proof-multiple-frames-enable 125,4438
+(defun proof-three-window-enable 143,5082
+(defun proof-select-three-b 147,5146
+(defun proof-display-three-b 162,5615
+(defvar pg-frame-configuration 176,6107
+(defun pg-cache-frame-configuration 180,6254
+(defun proof-layout-windows 184,6425
+(defun proof-delete-other-frames 225,8248
+(defvar pg-response-erase-flag 256,9338
+(defun pg-response-maybe-erase260,9467
+(defun pg-response-display 291,10652
+(defun pg-response-display-with-face 310,11500
+(defun pg-response-clear-displays 346,12730
+(defun proof-next-error 365,13317
+(defun pg-response-has-error-location 446,16233
+(defvar proof-trace-last-fontify-pos 469,17066
+(defun proof-trace-fontify-pos 471,17109
+(defun proof-trace-buffer-display 479,17422
+(defun proof-trace-buffer-finish 503,18394
+(defun pg-thms-buffer-clear 524,18974
 
 generic/pg-thymodes.el,152
 (defmacro pg-defthymode 23,499
@@ -1371,121 +1377,109 @@ generic/pg-thymodes.el,152
 (defun pg-modesym 82,2549
 (defun pg-modesymval 86,2663
 
-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-user.el,3127
+(defmacro proof-maybe-save-point 31,805
+(defun proof-maybe-follow-locked-end 39,1007
+(defun proof-assert-next-command-interactive 53,1372
+(defun proof-process-buffer 63,1743
+(defun proof-undo-last-successful-command 77,2060
+(defun proof-undo-and-delete-last-successful-command 82,2222
+(defun proof-undo-last-successful-command-1 104,3193
+(defun proof-retract-buffer 120,3758
+(defun proof-retract-current-goal 129,4038
+(defun proof-interrupt-process 148,4544
+(defun proof-goto-command-start 175,5533
+(defun proof-goto-command-end 198,6473
+(defun proof-mouse-goto-point 223,7251
+(defun proof-mouse-track-insert 239,7883
+(defvar proof-minibuffer-history 275,9020
+(defun proof-minibuffer-cmd 278,9115
+(defun proof-frob-locked-end 326,10909
+(defmacro proof-if-setting-configured 387,12839
+(defmacro proof-define-assistant-command 395,13108
+(defmacro proof-define-assistant-command-witharg 408,13563
+(defun proof-issue-new-command 428,14386
+(defun proof-cd-sync 473,15881
+(defun proof-electric-terminator-enable 532,17640
+(defun proof-electric-term-incomment-fn 540,17935
+(defun proof-process-electric-terminator 560,18686
+(defun proof-electric-terminator 587,19834
+(defun proof-add-completions 609,20471
+(defun proof-script-complete 629,21225
+(defun pg-insert-last-output-as-comment 657,21816
+(defun pg-copy-span-contents 688,23050
+(defun pg-numth-span-higher-or-lower 705,23608
+(defun pg-control-span-of 731,24354
+(defun pg-move-span-contents 737,24558
+(defun pg-fixup-children-spans 789,26738
+(defun pg-move-region-down 799,27001
+(defun pg-move-region-up 808,27294
+(defun proof-forward-command 838,28132
+(defun proof-backward-command 859,28853
+(defun pg-pos-for-event 881,29204
+(defun pg-span-for-event 893,29565
+(defun pg-span-context-menu 897,29709
+(defun pg-toggle-visibility 912,30164
+(defun pg-create-in-span-context-menu 922,30486
+(defun pg-span-undo 955,31830
+(defun pg-goals-buffers-hint 1001,33240
+(defun pg-slow-fontify-tracing-hint 1005,33422
+(defun pg-response-buffers-hint 1009,33593
+(defun pg-jump-to-end-hint 1019,33955
+(defun pg-processing-complete-hint 1023,34086
+(defun pg-next-error-hint 1040,34785
+(defun pg-hint 1045,34937
+(defun pg-identifier-under-mouse-query 1064,35606
+(defun proof-imenu-enable 1110,37261
+(defvar pg-input-ring 1143,38401
+(defvar pg-input-ring-index 1146,38457
+(defvar pg-stored-incomplete-input 1149,38528
+(defun pg-previous-input 1152,38630
+(defun pg-next-input 1166,39087
+(defun pg-delete-input 1171,39209
+(defun pg-get-old-input 1184,39547
+(defun pg-restore-input 1198,39938
+(defun pg-search-start 1209,40228
+(defun pg-regexp-arg 1221,40720
+(defun pg-search-arg 1233,41168
+(defun pg-previous-matching-input-string-position 1247,41585
+(defun pg-previous-matching-input 1274,42750
+(defun pg-next-matching-input 1293,43586
+(defvar pg-matching-input-from-input-string 1301,43969
+(defun pg-previous-matching-input-from-input 1305,44083
+(defun pg-next-matching-input-from-input 1323,44848
+(defun pg-add-to-input-history 1334,45227
+(defun pg-remove-from-input-history 1346,45680
+(defun  pg-clear-input-ring 1357,46063
 
 generic/pg-vars.el,1106
-(defvar proof-assistant-cusgrp 18,322
-(defvar proof-assistant-internals-cusgrp 24,584
-(defvar proof-assistant 30,855
-(defvar proof-assistant-symbol 35,1077
-(defvar proof-mode-for-shell 48,1621
-(defvar proof-mode-for-response 53,1813
-(defvar proof-mode-for-goals 58,2040
-(defvar proof-mode-for-script 63,2230
-(defvar proof-ready-for-assistant-hook 68,2408
-(defvar proof-shell-busy 78,2695
-(defvar proof-included-files-list 83,2851
-(defvar proof-script-buffer 105,3864
-(defvar proof-previous-script-buffer 108,3956
-(defvar proof-shell-buffer 112,4127
-(defvar proof-goals-buffer 115,4213
-(defvar proof-response-buffer 118,4268
-(defvar proof-trace-buffer 121,4329
-(defvar proof-thms-buffer 125,4483
-(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-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,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
+(defvar proof-assistant-cusgrp 20,379
+(defvar proof-assistant-internals-cusgrp 26,641
+(defvar proof-assistant 32,912
+(defvar proof-assistant-symbol 37,1134
+(defvar proof-mode-for-shell 50,1678
+(defvar proof-mode-for-response 55,1870
+(defvar proof-mode-for-goals 60,2097
+(defvar proof-mode-for-script 65,2287
+(defvar proof-ready-for-assistant-hook 70,2465
+(defvar proof-shell-busy 80,2752
+(defvar proof-included-files-list 85,2908
+(defvar proof-script-buffer 107,3921
+(defvar proof-previous-script-buffer 110,4013
+(defvar proof-shell-buffer 114,4184
+(defvar proof-goals-buffer 117,4270
+(defvar proof-response-buffer 120,4325
+(defvar proof-trace-buffer 123,4386
+(defvar proof-thms-buffer 127,4540
+(defvar proof-shell-error-or-interrupt-seen 131,4695
+(defvar pg-response-next-error 136,4919
+(defvar proof-shell-proof-completed 139,5026
+(defvar proof-terminal-string 151,5570
+(defvar proof-shell-last-output 161,5760
+(defvar proof-assistant-settings 165,5901
+(defvar pg-tracing-slow-mode 172,6264
+(defvar proof-nesting-depth 175,6353
+(defvar proof-last-theorem-dependencies 182,6588
 
 generic/pg-xml.el,1141
 (defalias 'pg-xml-error pg-xml-error
24,625
@@ -1520,231 +1514,231 @@ generic/pg-xml.el,1141
 (defun pg-pgip-get-pgmltext 229,7512
 
 generic/proof-config.el,11008
-(defgroup proof-user-options 87,3099
-(defun proof-set-value 96,3296
-(defcustom proof-electric-terminator-enable 129,4415
-(defcustom proof-toolbar-enable 141,4947
-(defcustom proof-imenu-enable 147,5120
-(defcustom pg-show-hints 153,5291
-(defcustom proof-output-fontify-enable 158,5426
-(defcustom proof-trace-output-slow-catchup 168,5809
-(defcustom proof-strict-state-preserving 178,6306
-(defcustom proof-strict-read-only 191,6915
-(defcustom proof-allow-undo-in-read-only 200,7264
-(defcustom proof-three-window-enable 208,7645
-(defcustom proof-multiple-frames-enable 227,8395
-(defcustom proof-delete-empty-windows 236,8728
-(defcustom proof-shrink-windows-tofit 247,9259
-(defcustom proof-toolbar-use-button-enablers 254,9531
-(defcustom proof-query-file-save-when-activating-scripting262,9866
-(defcustom proof-one-command-per-line278,10586
-(defcustom proof-prog-name-ask285,10813
-(defcustom proof-prog-name-guess291,10973
-(defcustom proof-tidy-response299,11232
-(defcustom proof-keep-response-history313,11695
-(defcustom pg-input-ring-size 323,12083
-(defcustom proof-general-debug 328,12235
-(defcustom proof-experimental-features337,12606
-(defcustom proof-follow-mode 355,13298
-(defcustom proof-auto-action-when-deactivating-scripting 379,14478
-(defcustom proof-script-command-separator 402,15427
-(defcustom proof-rsh-command 410,15719
-(defcustom proof-disappearing-proofs 426,16269
-(defgroup proof-faces 453,16915
-(defconst pg-defface-window-systems 458,17021
-(defmacro proof-face-specs 470,17538
-(defface proof-queue-face486,18058
-(defface proof-locked-face494,18336
-(defface proof-declaration-name-face507,18839
-(defface proof-tacticals-name-face516,19125
-(defface proof-tactics-name-face525,19387
-(defface proof-error-face534,19652
-(defface proof-warning-face542,19858
-(defface proof-eager-annotation-face551,20115
-(defface proof-debug-message-face559,20333
-(defface proof-boring-face567,20532
-(defface proof-mouse-highlight-face575,20724
-(defface proof-highlight-dependent-face583,20920
-(defface proof-highlight-dependency-face591,21129
-(defface proof-active-area-face599,21326
-(defconst proof-face-compat-doc 609,21619
-(defconst proof-queue-face 610,21699
-(defconst proof-locked-face 611,21767
-(defconst proof-declaration-name-face 612,21837
-(defconst proof-tacticals-name-face 613,21927
-(defconst proof-tactics-name-face 614,22013
-(defconst proof-error-face 615,22095
-(defconst proof-warning-face 616,22163
-(defconst proof-eager-annotation-face 617,22235
-(defconst proof-debug-message-face 618,22325
-(defconst proof-boring-face 619,22409
-(defconst proof-mouse-highlight-face 620,22479
-(defconst proof-highlight-dependent-face 621,22567
-(defconst proof-highlight-dependency-face 622,22663
-(defconst proof-active-area-face 623,22761
-(defgroup prover-config 633,22902
-(defcustom proof-guess-command-line 675,24213
-(defcustom proof-assistant-home-page 690,24708
-(defcustom proof-context-command 696,24878
-(defcustom proof-info-command 701,25012
-(defcustom proof-showproof-command 708,25283
-(defcustom proof-goal-command 713,25419
-(defcustom proof-save-command 721,25716
-(defcustom proof-find-theorems-command 729,26025
-(defcustom proof-assistant-true-value 736,26335
-(defcustom proof-assistant-false-value 742,26525
-(defcustom proof-assistant-format-int-fn 748,26719
-(defcustom proof-assistant-format-string-fn 755,26968
-(defcustom proof-assistant-setting-format 762,27235
-(defgroup proof-script 784,27930
-(defcustom proof-terminal-char 789,28060
-(defcustom proof-script-sexp-commands 799,28447
-(defcustom proof-script-command-end-regexp 810,28904
-(defcustom proof-script-command-start-regexp 828,29723
-(defcustom proof-script-use-old-parser 839,30184
-(defcustom proof-script-integral-proofs 851,30670
-(defcustom proof-script-fly-past-comments 866,31326
-(defcustom proof-script-parse-function 871,31497
-(defcustom proof-script-comment-start 889,32140
-(defcustom proof-script-comment-start-regexp 900,32577
-(defcustom proof-script-comment-end 908,32894
-(defcustom proof-script-comment-end-regexp 920,33316
-(defcustom pg-insert-output-as-comment-fn 928,33627
-(defcustom proof-string-start-regexp 934,33879
-(defcustom proof-string-end-regexp 939,34044
-(defcustom proof-case-fold-search 944,34205
-(defcustom proof-save-command-regexp 953,34615
-(defcustom proof-save-with-hole-regexp 958,34725
-(defcustom proof-save-with-hole-result 970,35179
-(defcustom proof-goal-command-regexp 980,35630
-(defcustom proof-goal-with-hole-regexp 989,36018
-(defcustom proof-goal-with-hole-result 1001,36459
-(defcustom proof-non-undoables-regexp 1010,36846
-(defcustom proof-nested-undo-regexp 1021,37301
-(defcustom proof-ignore-for-undo-count 1037,38013
-(defcustom proof-script-next-entity-regexps 1045,38316
-(defcustom proof-script-find-next-entity-fn1089,40051
-(defcustom proof-script-imenu-generic-expression 1109,40889
-(defcustom proof-goal-command-p 1127,41742
-(defcustom proof-really-save-command-p 1154,43179
-(defcustom proof-completed-proof-behaviour 1166,43641
-(defcustom proof-count-undos-fn 1194,44997
-(defconst proof-no-command 1206,45546
-(defcustom proof-find-and-forget-fn 1211,45751
-(defcustom proof-forget-id-command 1228,46463
-(defcustom pg-topterm-goalhyplit-fn 1238,46821
-(defcustom proof-kill-goal-command 1250,47356
-(defcustom proof-undo-n-times-cmd 1264,47857
-(defcustom proof-nested-goals-history-p 1278,48405
-(defcustom proof-state-preserving-p 1287,48742
-(defcustom proof-activate-scripting-hook 1297,49212
-(defcustom proof-deactivate-scripting-hook 1316,49991
-(defcustom proof-indent 1329,50356
-(defcustom proof-indent-hang 1334,50463
-(defcustom proof-indent-enclose-offset 1339,50589
-(defcustom proof-indent-open-offset 1344,50731
-(defcustom proof-indent-close-offset 1349,50868
-(defcustom proof-indent-any-regexp 1354,51006
-(defcustom proof-indent-inner-regexp 1359,51166
-(defcustom proof-indent-enclose-regexp 1364,51320
-(defcustom proof-indent-open-regexp 1369,51474
-(defcustom proof-indent-close-regexp 1374,51626
-(defcustom proof-script-font-lock-keywords 1380,51780
-(defcustom proof-script-syntax-table-entries 1388,52109
-(defcustom proof-script-span-context-menu-extensions 1406,52506
-(defgroup proof-shell 1432,53266
-(defcustom proof-prog-name 1442,53437
-(defcustom proof-shell-auto-terminate-commands 1453,53855
-(defcustom proof-shell-pre-sync-init-cmd 1462,54252
-(defcustom proof-shell-init-cmd 1476,54810
-(defcustom proof-shell-restart-cmd 1487,55279
-(defcustom proof-shell-quit-cmd 1492,55434
-(defcustom proof-shell-quit-timeout 1497,55601
-(defcustom proof-shell-cd-cmd 1507,56049
-(defcustom proof-shell-start-silent-cmd 1524,56714
-(defcustom proof-shell-stop-silent-cmd 1533,57088
-(defcustom proof-shell-silent-threshold 1542,57421
-(defcustom  proof-shell-inform-file-processed-cmd 1550,57755
-(defcustom  proof-shell-inform-file-retracted-cmd 1571,58677
-(defcustom proof-auto-multiple-files 1599,59943
-(defcustom proof-cannot-reopen-processed-files 1614,60664
-(defcustom proof-shell-require-command-regexp 1628,61330
-(defcustom proof-done-advancing-require-function 1639,61792
-(defcustom proof-shell-quiet-errors 1645,62027
-(defcustom proof-shell-prompt-pattern 1658,62361
-(defcustom proof-shell-wakeup-char 1668,62782
-(defcustom proof-shell-annotated-prompt-regexp 1674,63013
-(defcustom proof-shell-abort-goal-regexp 1690,63647
-(defcustom proof-shell-error-regexp 1695,63782
-(defcustom proof-shell-truncate-before-error 1715,64576
-(defcustom pg-next-error-regexp 1729,65119
-(defcustom pg-next-error-filename-regexp 1744,65728
-(defcustom pg-next-error-extract-filename 1768,66761
-(defcustom proof-shell-interrupt-regexp 1775,67004
-(defcustom proof-shell-proof-completed-regexp 1789,67595
-(defcustom proof-shell-clear-response-regexp 1802,68103
-(defcustom proof-shell-clear-goals-regexp 1809,68402
-(defcustom proof-shell-start-goals-regexp 1816,68695
-(defcustom proof-shell-end-goals-regexp 1824,69062
-(defcustom proof-shell-eager-annotation-start 1830,69304
-(defcustom proof-shell-eager-annotation-start-length 1853,70324
-(defcustom proof-shell-eager-annotation-end 1864,70750
-(defcustom proof-shell-assumption-regexp 1880,71425
-(defcustom proof-shell-process-file 1890,71828
-(defcustom proof-shell-retract-files-regexp 1912,72784
-(defcustom proof-shell-compute-new-files-list 1921,73120
-(defcustom pg-use-specials-for-fontify 1933,73668
-(defcustom pg-special-char-regexp 1941,74016
-(defcustom proof-shell-set-elisp-variable-regexp 1947,74161
-(defcustom proof-shell-match-pgip-cmd 1980,75672
-(defcustom proof-shell-issue-pgip-cmd 1989,76001
-(defcustom proof-shell-query-dependencies-cmd 1998,76357
-(defcustom proof-shell-theorem-dependency-list-regexp 2005,76617
-(defcustom proof-shell-theorem-dependency-list-split 2021,77277
-(defcustom proof-shell-show-dependency-cmd 2030,77700
-(defcustom proof-shell-identifier-under-mouse-cmd 2037,77969
-(defcustom proof-shell-trace-output-regexp 2060,79050
-(defcustom proof-shell-thms-output-regexp 2074,79508
-(defcustom proof-shell-unicode 2087,79894
-(defcustom proof-shell-filename-escapes 2095,80214
-(defcustom proof-shell-process-connection-type2112,80894
-(defcustom proof-shell-strip-crs-from-input 2135,81940
-(defcustom proof-shell-strip-crs-from-output 2147,82425
-(defcustom proof-shell-insert-hook 2155,82793
-(defcustom proof-shell-handle-delayed-output-hook2195,84750
-(defcustom proof-shell-handle-error-or-interrupt-hook2201,84965
-(defcustom proof-shell-pre-interrupt-hook2219,85714
-(defcustom proof-shell-process-output-system-specific 2227,85986
-(defcustom proof-state-change-hook 2246,86850
-(defcustom proof-shell-font-lock-keywords 2257,87232
-(defcustom proof-shell-syntax-table-entries 2265,87564
-(defgroup proof-goals 2283,87936
-(defcustom pg-subterm-first-special-char 2288,88057
-(defcustom pg-subterm-anns-use-stack 2296,88369
-(defcustom pg-goals-change-goal 2305,88668
-(defcustom pbp-goal-command 2310,88784
-(defcustom pbp-hyp-command 2315,88940
-(defcustom pg-subterm-help-cmd 2320,89102
-(defcustom pg-goals-error-regexp 2327,89338
-(defcustom proof-shell-result-start 2332,89498
-(defcustom proof-shell-result-end 2338,89732
-(defcustom pg-subterm-start-char 2344,89945
-(defcustom pg-subterm-sep-char 2358,90525
-(defcustom pg-subterm-end-char 2364,90704
-(defcustom pg-topterm-regexp 2370,90861
-(defcustom proof-goals-font-lock-keywords 2387,91463
-(defcustom proof-resp-font-lock-keywords 2401,92148
-(defcustom pg-before-fontify-output-hook 2413,92728
-(defcustom pg-after-fontify-output-hook 2421,93088
-(defgroup proof-x-symbol 2433,93368
-(defcustom proof-xsym-extra-modes 2438,93496
-(defcustom proof-xsym-font-lock-keywords 2451,94124
-(defcustom proof-xsym-activate-command 2459,94501
-(defcustom proof-xsym-deactivate-command 2466,94736
-(defcustom proof-general-name 2483,95021
-(defcustom proof-general-home-page2488,95178
-(defcustom proof-unnamed-theorem-name2494,95338
-(defcustom proof-universal-keys2500,95522
+(defgroup proof-user-options 85,3024
+(defun proof-set-value 94,3221
+(defcustom proof-electric-terminator-enable 127,4340
+(defcustom proof-toolbar-enable 139,4872
+(defcustom proof-imenu-enable 145,5045
+(defcustom pg-show-hints 151,5216
+(defcustom proof-output-fontify-enable 156,5351
+(defcustom proof-trace-output-slow-catchup 166,5734
+(defcustom proof-strict-state-preserving 176,6231
+(defcustom proof-strict-read-only 189,6840
+(defcustom proof-allow-undo-in-read-only 198,7189
+(defcustom proof-three-window-enable 206,7570
+(defcustom proof-multiple-frames-enable 225,8320
+(defcustom proof-delete-empty-windows 234,8653
+(defcustom proof-shrink-windows-tofit 245,9184
+(defcustom proof-toolbar-use-button-enablers 252,9456
+(defcustom proof-query-file-save-when-activating-scripting260,9791
+(defcustom proof-one-command-per-line276,10511
+(defcustom proof-prog-name-ask283,10738
+(defcustom proof-prog-name-guess289,10898
+(defcustom proof-tidy-response297,11157
+(defcustom proof-keep-response-history311,11620
+(defcustom pg-input-ring-size 321,12008
+(defcustom proof-general-debug 326,12160
+(defcustom proof-experimental-features 336,12532
+(defcustom proof-follow-mode 350,13067
+(defcustom proof-auto-action-when-deactivating-scripting 374,14247
+(defcustom proof-script-command-separator 397,15196
+(defcustom proof-rsh-command 405,15488
+(defcustom proof-disappearing-proofs 421,16038
+(defgroup proof-faces 448,16684
+(defconst pg-defface-window-systems 453,16790
+(defmacro proof-face-specs 465,17307
+(defface proof-queue-face481,17827
+(defface proof-locked-face489,18105
+(defface proof-declaration-name-face502,18608
+(defface proof-tacticals-name-face511,18894
+(defface proof-tactics-name-face520,19156
+(defface proof-error-face529,19421
+(defface proof-warning-face537,19627
+(defface proof-eager-annotation-face546,19884
+(defface proof-debug-message-face554,20102
+(defface proof-boring-face562,20301
+(defface proof-mouse-highlight-face570,20493
+(defface proof-highlight-dependent-face578,20689
+(defface proof-highlight-dependency-face586,20898
+(defface proof-active-area-face594,21095
+(defconst proof-face-compat-doc 604,21486
+(defconst proof-queue-face 605,21566
+(defconst proof-locked-face 606,21634
+(defconst proof-declaration-name-face 607,21704
+(defconst proof-tacticals-name-face 608,21794
+(defconst proof-tactics-name-face 609,21880
+(defconst proof-error-face 610,21962
+(defconst proof-warning-face 611,22030
+(defconst proof-eager-annotation-face 612,22102
+(defconst proof-debug-message-face 613,22192
+(defconst proof-boring-face 614,22276
+(defconst proof-mouse-highlight-face 615,22346
+(defconst proof-highlight-dependent-face 616,22434
+(defconst proof-highlight-dependency-face 617,22530
+(defconst proof-active-area-face 618,22628
+(defgroup prover-config 628,22769
+(defcustom proof-guess-command-line 670,24080
+(defcustom proof-assistant-home-page 685,24575
+(defcustom proof-context-command 691,24745
+(defcustom proof-info-command 696,24879
+(defcustom proof-showproof-command 703,25150
+(defcustom proof-goal-command 708,25286
+(defcustom proof-save-command 716,25583
+(defcustom proof-find-theorems-command 724,25892
+(defcustom proof-assistant-true-value 731,26202
+(defcustom proof-assistant-false-value 737,26392
+(defcustom proof-assistant-format-int-fn 743,26586
+(defcustom proof-assistant-format-string-fn 750,26835
+(defcustom proof-assistant-setting-format 757,27102
+(defgroup proof-script 779,27797
+(defcustom proof-terminal-char 784,27927
+(defcustom proof-script-sexp-commands 794,28314
+(defcustom proof-script-command-end-regexp 805,28771
+(defcustom proof-script-command-start-regexp 823,29590
+(defcustom proof-script-use-old-parser 834,30051
+(defcustom proof-script-integral-proofs 846,30537
+(defcustom proof-script-fly-past-comments 861,31193
+(defcustom proof-script-parse-function 866,31364
+(defcustom proof-script-comment-start 884,32007
+(defcustom proof-script-comment-start-regexp 895,32444
+(defcustom proof-script-comment-end 903,32761
+(defcustom proof-script-comment-end-regexp 915,33183
+(defcustom pg-insert-output-as-comment-fn 923,33494
+(defcustom proof-string-start-regexp 929,33746
+(defcustom proof-string-end-regexp 934,33911
+(defcustom proof-case-fold-search 939,34072
+(defcustom proof-save-command-regexp 948,34482
+(defcustom proof-save-with-hole-regexp 953,34592
+(defcustom proof-save-with-hole-result 965,35046
+(defcustom proof-goal-command-regexp 975,35497
+(defcustom proof-goal-with-hole-regexp 984,35885
+(defcustom proof-goal-with-hole-result 996,36326
+(defcustom proof-non-undoables-regexp 1005,36713
+(defcustom proof-nested-undo-regexp 1016,37168
+(defcustom proof-ignore-for-undo-count 1032,37880
+(defcustom proof-script-next-entity-regexps 1040,38183
+(defcustom proof-script-find-next-entity-fn1084,39918
+(defcustom proof-script-imenu-generic-expression 1104,40756
+(defcustom proof-goal-command-p 1122,41609
+(defcustom proof-really-save-command-p 1149,43046
+(defcustom proof-completed-proof-behaviour 1161,43508
+(defcustom proof-count-undos-fn 1189,44864
+(defconst proof-no-command 1201,45413
+(defcustom proof-find-and-forget-fn 1206,45618
+(defcustom proof-forget-id-command 1223,46330
+(defcustom pg-topterm-goalhyplit-fn 1233,46688
+(defcustom proof-kill-goal-command 1245,47223
+(defcustom proof-undo-n-times-cmd 1259,47724
+(defcustom proof-nested-goals-history-p 1273,48272
+(defcustom proof-state-preserving-p 1282,48609
+(defcustom proof-activate-scripting-hook 1292,49079
+(defcustom proof-deactivate-scripting-hook 1311,49858
+(defcustom proof-indent 1324,50223
+(defcustom proof-indent-hang 1329,50330
+(defcustom proof-indent-enclose-offset 1334,50456
+(defcustom proof-indent-open-offset 1339,50598
+(defcustom proof-indent-close-offset 1344,50735
+(defcustom proof-indent-any-regexp 1349,50873
+(defcustom proof-indent-inner-regexp 1354,51033
+(defcustom proof-indent-enclose-regexp 1359,51187
+(defcustom proof-indent-open-regexp 1364,51341
+(defcustom proof-indent-close-regexp 1369,51493
+(defcustom proof-script-font-lock-keywords 1375,51647
+(defcustom proof-script-syntax-table-entries 1383,51976
+(defcustom proof-script-span-context-menu-extensions 1401,52373
+(defgroup proof-shell 1427,53133
+(defcustom proof-prog-name 1437,53304
+(defcustom proof-shell-auto-terminate-commands 1448,53722
+(defcustom proof-shell-pre-sync-init-cmd 1457,54119
+(defcustom proof-shell-init-cmd 1471,54677
+(defcustom proof-shell-restart-cmd 1482,55146
+(defcustom proof-shell-quit-cmd 1487,55301
+(defcustom proof-shell-quit-timeout 1492,55468
+(defcustom proof-shell-cd-cmd 1502,55916
+(defcustom proof-shell-start-silent-cmd 1519,56581
+(defcustom proof-shell-stop-silent-cmd 1528,56955
+(defcustom proof-shell-silent-threshold 1537,57288
+(defcustom  proof-shell-inform-file-processed-cmd 1545,57622
+(defcustom  proof-shell-inform-file-retracted-cmd 1566,58544
+(defcustom proof-auto-multiple-files 1594,59810
+(defcustom proof-cannot-reopen-processed-files 1609,60531
+(defcustom proof-shell-require-command-regexp 1623,61197
+(defcustom proof-done-advancing-require-function 1634,61659
+(defcustom proof-shell-quiet-errors 1640,61894
+(defcustom proof-shell-prompt-pattern 1653,62228
+(defcustom proof-shell-wakeup-char 1663,62649
+(defcustom proof-shell-annotated-prompt-regexp 1669,62880
+(defcustom proof-shell-abort-goal-regexp 1685,63514
+(defcustom proof-shell-error-regexp 1690,63649
+(defcustom proof-shell-truncate-before-error 1710,64443
+(defcustom pg-next-error-regexp 1724,64986
+(defcustom pg-next-error-filename-regexp 1739,65595
+(defcustom pg-next-error-extract-filename 1763,66628
+(defcustom proof-shell-interrupt-regexp 1770,66871
+(defcustom proof-shell-proof-completed-regexp 1784,67462
+(defcustom proof-shell-clear-response-regexp 1797,67970
+(defcustom proof-shell-clear-goals-regexp 1804,68269
+(defcustom proof-shell-start-goals-regexp 1811,68562
+(defcustom proof-shell-end-goals-regexp 1819,68929
+(defcustom proof-shell-eager-annotation-start 1825,69171
+(defcustom proof-shell-eager-annotation-start-length 1848,70191
+(defcustom proof-shell-eager-annotation-end 1859,70617
+(defcustom proof-shell-assumption-regexp 1875,71292
+(defcustom proof-shell-process-file 1885,71695
+(defcustom proof-shell-retract-files-regexp 1907,72651
+(defcustom proof-shell-compute-new-files-list 1916,72987
+(defcustom pg-use-specials-for-fontify 1928,73535
+(defcustom pg-special-char-regexp 1936,73883
+(defcustom proof-shell-set-elisp-variable-regexp 1942,74028
+(defcustom proof-shell-match-pgip-cmd 1975,75539
+(defcustom proof-shell-issue-pgip-cmd 1984,75868
+(defcustom proof-shell-query-dependencies-cmd 1993,76224
+(defcustom proof-shell-theorem-dependency-list-regexp 2000,76484
+(defcustom proof-shell-theorem-dependency-list-split 2016,77144
+(defcustom proof-shell-show-dependency-cmd 2025,77567
+(defcustom proof-shell-identifier-under-mouse-cmd 2032,77836
+(defcustom proof-shell-trace-output-regexp 2055,78917
+(defcustom proof-shell-thms-output-regexp 2069,79375
+(defcustom proof-shell-unicode 2082,79761
+(defcustom proof-shell-filename-escapes 2090,80081
+(defcustom proof-shell-process-connection-type2107,80761
+(defcustom proof-shell-strip-crs-from-input 2130,81807
+(defcustom proof-shell-strip-crs-from-output 2142,82292
+(defcustom proof-shell-insert-hook 2150,82660
+(defcustom proof-shell-handle-delayed-output-hook2190,84617
+(defcustom proof-shell-handle-error-or-interrupt-hook2196,84832
+(defcustom proof-shell-pre-interrupt-hook2214,85581
+(defcustom proof-shell-process-output-system-specific 2222,85853
+(defcustom proof-state-change-hook 2241,86717
+(defcustom proof-shell-font-lock-keywords 2252,87099
+(defcustom proof-shell-syntax-table-entries 2260,87431
+(defgroup proof-goals 2278,87803
+(defcustom pg-subterm-first-special-char 2283,87924
+(defcustom pg-subterm-anns-use-stack 2291,88236
+(defcustom pg-goals-change-goal 2300,88535
+(defcustom pbp-goal-command 2305,88651
+(defcustom pbp-hyp-command 2310,88807
+(defcustom pg-subterm-help-cmd 2315,88969
+(defcustom pg-goals-error-regexp 2322,89205
+(defcustom proof-shell-result-start 2327,89365
+(defcustom proof-shell-result-end 2333,89599
+(defcustom pg-subterm-start-char 2339,89812
+(defcustom pg-subterm-sep-char 2353,90392
+(defcustom pg-subterm-end-char 2359,90571
+(defcustom pg-topterm-regexp 2365,90728
+(defcustom proof-goals-font-lock-keywords 2382,91330
+(defcustom proof-resp-font-lock-keywords 2396,92015
+(defcustom pg-before-fontify-output-hook 2408,92595
+(defcustom pg-after-fontify-output-hook 2416,92955
+(defgroup proof-x-symbol 2428,93235
+(defcustom proof-xsym-extra-modes 2433,93363
+(defcustom proof-xsym-font-lock-keywords 2446,93991
+(defcustom proof-xsym-activate-command 2454,94368
+(defcustom proof-xsym-deactivate-command 2461,94603
+(defcustom proof-general-name 2478,94888
+(defcustom proof-general-home-page2483,95045
+(defcustom proof-unnamed-theorem-name2489,95205
+(defcustom proof-universal-keys2495,95389
 
 generic/proof-depends.el,824
 (defvar proof-thm-names-of-files 23,624
@@ -1787,280 +1781,281 @@ generic/proof-maths-menu.el,134
 (defun proof-maths-menu-enable 56,1879
 
 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 286,10399
-(defconst proof-quick-opts-menu294,10709
-(defun proof-quick-opts-vars 445,16657
-(defun proof-quick-opts-changed-from-defaults-p 470,17408
-(defun proof-quick-opts-changed-from-saved-p 474,17513
-(defun proof-quick-opts-save 485,17865
-(defun proof-quick-opts-reset 490,18033
-(defconst proof-config-menu502,18301
-(defconst proof-advanced-menu509,18480
-(defvar proof-menu 522,18915
-(defun proof-main-menu 531,19199
-(defun proof-aux-menu 542,19465
-(defun proof-menu-define-favourites-menu 558,19812
-(defun proof-def-favourite 578,20468
-(defvar proof-make-favourite-cmd-history 601,21443
-(defvar proof-make-favourite-menu-history 604,21528
-(defun proof-save-favourites 607,21614
-(defun proof-del-favourite 612,21762
-(defun proof-read-favourite 629,22323
-(defun proof-add-favourite 654,23126
-(defvar proof-menu-settings 681,24177
-(defun proof-menu-define-settings-menu 684,24251
-(defun proof-menu-entry-name 704,24995
-(defun proof-menu-entry-for-setting 716,25467
-(defun proof-settings-vars 734,25957
-(defun proof-settings-changed-from-defaults-p 739,26134
-(defun proof-settings-changed-from-saved-p 743,26240
-(defun proof-settings-save 747,26343
-(defun proof-settings-reset 752,26510
-(defun proof-defpacustom-fn 759,26755
-(defmacro defpacustom 835,29639
-(defun proof-assistant-invisible-command-ifposs 850,30466
-(defun proof-maybe-askprefs 872,31441
-(defun proof-assistant-settings-cmd 879,31645
-(defvar proof-assistant-format-table 896,32305
-(defun proof-assistant-format-bool 904,32674
-(defun proof-assistant-format-int 907,32787
-(defun proof-assistant-format-string 910,32879
-(defun proof-assistant-format 913,32977
+(defvar proof-display-some-buffers-count 17,437
+(defun proof-display-some-buffers 19,482
+(defun proof-menu-define-keys 78,2684
+(defun proof-menu-define-main 141,5720
+(defvar proof-menu-favourites 150,5908
+(defun proof-menu-define-specific 154,6030
+(defun proof-assistant-menu-update 192,7056
+(defvar proof-help-menu208,7639
+(defvar proof-show-hide-menu216,7917
+(defvar proof-buffer-menu225,8230
+(defun proof-keep-response-history 286,10398
+(defconst proof-quick-opts-menu294,10708
+(defun proof-quick-opts-vars 437,16385
+(defun proof-quick-opts-changed-from-defaults-p 462,17136
+(defun proof-quick-opts-changed-from-saved-p 466,17241
+(defun proof-quick-opts-save 477,17593
+(defun proof-quick-opts-reset 482,17761
+(defconst proof-config-menu494,18029
+(defconst proof-advanced-menu501,18208
+(defvar proof-menu 514,18643
+(defun proof-main-menu 523,18927
+(defun proof-aux-menu 534,19193
+(defun proof-menu-define-favourites-menu 550,19540
+(defun proof-def-favourite 570,20196
+(defvar proof-make-favourite-cmd-history 593,21171
+(defvar proof-make-favourite-menu-history 596,21256
+(defun proof-save-favourites 599,21342
+(defun proof-del-favourite 604,21490
+(defun proof-read-favourite 621,22051
+(defun proof-add-favourite 646,22854
+(defvar proof-menu-settings 673,23905
+(defun proof-menu-define-settings-menu 676,23979
+(defun proof-menu-entry-name 696,24723
+(defun proof-menu-entry-for-setting 708,25195
+(defun proof-settings-vars 726,25685
+(defun proof-settings-changed-from-defaults-p 731,25862
+(defun proof-settings-changed-from-saved-p 735,25968
+(defun proof-settings-save 739,26071
+(defun proof-settings-reset 744,26238
+(defun proof-defpacustom-fn 751,26483
+(defmacro defpacustom 827,29367
+(defun proof-assistant-invisible-command-ifposs 842,30194
+(defun proof-maybe-askprefs 864,31169
+(defun proof-assistant-settings-cmd 871,31373
+(defvar proof-assistant-format-table 888,32033
+(defun proof-assistant-format-bool 896,32402
+(defun proof-assistant-format-int 899,32515
+(defun proof-assistant-format-string 902,32607
+(defun proof-assistant-format 905,32705
 
 generic/proof-mmm.el,114
 (defun proof-mmm-support-available 34,1131
 (defun proof-mmm-set-global 58,1979
 (defun proof-mmm-enable 73,2520
 
-generic/proof-script.el,5063
-(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-locked-endpoints 219,7694
-(defsubst proof-detach-queue 223,7838
-(defsubst proof-detach-locked 227,7970
-(defsubst proof-set-queue-start 231,8106
-(defsubst proof-set-locked-end 235,8232
-(defsubst proof-set-queue-end 248,8717
-(defun proof-init-segmentation 259,9014
-(defun proof-restart-buffers 292,10409
-(defun proof-script-buffers-with-spans 314,11341
-(defun proof-script-remove-all-spans-and-deactivate 324,11697
-(defun proof-script-clear-queue-spans 328,11885
-(defun proof-unprocessed-begin 347,12446
-(defun proof-script-end 355,12700
-(defun proof-queue-or-locked-end 364,13001
-(defun proof-locked-end 379,13679
-(defun proof-locked-region-full-p 396,14064
-(defun proof-locked-region-empty-p 405,14336
-(defun proof-only-whitespace-to-locked-region-p 409,14486
-(defun proof-in-locked-region-p 422,15122
-(defun proof-goto-end-of-locked 434,15385
-(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 451,16144
-(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 462,16625
-(defun proof-end-of-locked-visible-p 476,17278
-(defun proof-goto-end-of-queue-or-locked-if-not-visible 485,17729
-(defvar pg-idioms 504,18379
-(defvar pg-visibility-specs 507,18475
-(defconst pg-default-invisibility-spec 512,18682
-(defun pg-clear-script-portions 516,18822
-(defun pg-add-script-element 530,19299
-(defun pg-remove-script-element 533,19375
-(defsubst pg-visname 541,19653
-(defun pg-add-element 545,19798
-(defun pg-open-invisible-span 579,21427
-(defun pg-remove-element 590,21790
-(defun pg-make-element-invisible 597,22060
-(defun pg-make-element-visible 603,22317
-(defun pg-toggle-element-visibility 608,22496
-(defun pg-redisplay-for-gnuemacs 616,22826
-(defun pg-show-all-portions 623,23097
-(defun pg-show-all-proofs 641,23768
-(defun pg-hide-all-proofs 646,23896
-(defun pg-add-proof-element 651,24027
-(defun pg-span-name 665,24647
-(defvar pg-span-context-menu-keymap686,25354
-(defun pg-set-span-helphighlights 699,25725
-(defun proof-complete-buffer-atomic 727,26654
-(defun proof-register-possibly-new-processed-file 768,28569
-(defun proof-inform-prover-file-retracted 819,30697
-(defun proof-auto-retract-dependencies 838,31483
-(defun proof-unregister-buffer-file-name 892,34023
-(defun proof-protected-process-or-retract 938,35846
-(defun proof-deactivate-scripting-auto 965,37016
-(defun proof-deactivate-scripting 974,37374
-(defun proof-activate-scripting 1111,42779
-(defun proof-toggle-active-scripting 1233,48211
-(defun proof-done-advancing 1274,49572
-(defun proof-done-advancing-comment 1369,53220
-(defun proof-done-advancing-save 1388,53962
-(defun proof-make-goalsave 1481,57577
-(defun proof-get-name-from-goal 1496,58320
-(defun proof-done-advancing-autosave 1515,59346
-(defun proof-done-advancing-other 1580,61892
-(defun proof-segment-up-to-parser 1608,62851
-(defun proof-script-generic-parse-find-comment-end 1671,64927
-(defun proof-script-generic-parse-cmdend 1680,65343
-(defun proof-script-generic-parse-cmdstart 1705,66238
-(defun proof-script-generic-parse-sexp 1768,68946
-(defun proof-cmdstart-add-segment-for-cmd 1792,69882
-(defun proof-segment-up-to-cmdstart 1844,72081
-(defun proof-segment-up-to-cmdend 1905,74441
-(defun proof-semis-to-vanillas 1977,77106
-(defun proof-script-new-command-advance 2016,78432
-(defun proof-script-next-command-advance 2058,80173
-(defun proof-assert-until-point-interactive 2070,80614
-(defun proof-assert-until-point 2096,81736
-(defun proof-assert-next-command2149,84168
-(defun proof-goto-point 2197,86431
-(defun proof-insert-pbp-command 2215,86972
-(defun proof-done-retracting 2247,88072
-(defun proof-setup-retract-action 2283,89558
-(defun proof-last-goal-or-goalsave 2293,90041
-(defun proof-retract-target 2316,90881
-(defun proof-retract-until-point-interactive 2401,94522
-(defun proof-retract-until-point 2409,94907
-(define-derived-mode proof-mode 2452,96656
-(defun proof-script-set-visited-file-name 2502,98583
-(defun proof-script-set-buffer-hooks 2526,99585
-(defun proof-script-kill-buffer-fn 2534,100003
-(defun proof-config-done-related 2578,101825
-(defun proof-generic-goal-command-p 2648,104303
-(defun proof-generic-state-preserving-p 2653,104515
-(defun proof-generic-count-undos 2662,105032
-(defun proof-generic-find-and-forget 2691,106062
-(defconst proof-script-important-settings2742,107887
-(defun proof-config-done 2757,108440
-(defun proof-setup-parsing-mechanism 2845,111558
-(defun proof-setup-imenu 2889,113411
-(defun proof-setup-func-menu 2906,114016
-
-generic/proof-shell.el,3315
-(defvar proof-marker 28,643
-(defvar proof-action-list 31,740
-(defvar proof-shell-silent 39,916
-(defvar proof-shell-last-prompt 53,1399
-(defvar proof-shell-last-output-kind 58,1629
-(defvar proof-shell-delayed-output 79,2451
-(defvar proof-shell-delayed-output-kind 82,2572
-(defcustom proof-shell-active-scripting-indicator91,2775
-(defun proof-shell-ready-prover 144,4246
-(defun proof-shell-live-buffer 158,4786
-(defun proof-shell-available-p 165,5021
-(defun proof-grab-lock 171,5244
-(defun proof-release-lock 188,5956
-(defcustom proof-shell-fiddle-frames 208,6507
-(defun proof-shell-set-text-representation 215,6748
-(defun proof-shell-start 228,7303
-(defvar proof-shell-kill-function-hooks 438,14850
-(defun proof-shell-kill-function 441,14948
-(defun proof-shell-clear-state 530,18751
-(defun proof-shell-exit 545,19194
-(defun proof-shell-bail-out 557,19639
-(defun proof-shell-restart 566,20116
-(defvar proof-shell-no-response-display 608,21500
-(defvar proof-shell-urgent-message-marker 611,21604
-(defvar proof-shell-urgent-message-scanner 614,21725
-(defun proof-shell-handle-output 618,21852
-(defun proof-shell-handle-delayed-output 678,24493
-(defvar proof-shell-no-error-display 706,25536
-(defun proof-shell-handle-error 712,25740
-(defun proof-shell-handle-interrupt 730,26576
-(defun proof-shell-error-or-interrupt-action 744,27189
-(defun proof-goals-pos 769,28334
-(defun proof-pbp-focus-on-first-goal 774,28539
-(defsubst proof-shell-string-match-safe 786,29069
-(defun proof-shell-process-output 791,29237
-(defvar proof-shell-insert-space-fudge 902,33877
-(defun proof-shell-insert 912,34196
-(defun proof-shell-command-queue-item 986,37107
-(defun proof-shell-set-silent 991,37264
-(defun proof-shell-start-silent-item 997,37483
-(defun proof-shell-clear-silent 1003,37675
-(defun proof-shell-stop-silent-item 1009,37897
-(defun proof-shell-should-be-silent 1016,38169
-(defun proof-append-alist 1029,38725
-(defun proof-start-queue 1088,40962
-(defun proof-extend-queue 1099,41311
-(defun proof-shell-exec-loop 1110,41692
-(defun proof-shell-insert-loopback-cmd 1175,44280
-(defun proof-shell-message 1203,45606
-(defun proof-shell-process-urgent-message 1209,45822
-(defun proof-shell-strip-eager-annotations 1341,51087
-(defvar proof-shell-minibuffer-urgent-interactive-input-history 1352,51423
-(defun proof-shell-minibuffer-urgent-interactive-input 1354,51493
-(defun proof-shell-process-urgent-messages 1364,51852
-(defun proof-shell-filter 1438,54951
-(defun proof-shell-filter-process-output 1597,61540
-(defvar pg-last-tracing-output-time 1650,63594
-(defconst pg-slow-mode-duration 1653,63700
-(defconst pg-fast-tracing-mode-threshold 1656,63782
-(defvar pg-tracing-cleanup-timer 1659,63910
-(defun pg-tracing-tight-loop 1661,63949
-(defun pg-finish-tracing-display 1704,65667
-(defun proof-shell-dont-show-annotations 1717,65973
-(defun proof-shell-show-annotations 1733,66494
-(defun proof-shell-wait 1755,67021
-(defun proof-done-invisible 1775,67931
-(defun proof-shell-invisible-command 1818,69654
-(defun proof-shell-invisible-cmd-get-result 1852,70919
-(defun proof-shell-invisible-command-invisible-result 1870,71615
-(define-derived-mode proof-shell-mode 1889,72045
-(defconst proof-shell-important-settings1959,74711
-(defun proof-shell-config-done 1965,74826
-
-generic/proof-site.el,505
-(defconst proof-assistant-table-default23,728
-(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-script.el,5112
+(defvar proof-element-counters 28,718
+(deflocal proof-active-buffer-fake-minor-mode 34,858
+(deflocal proof-script-buffer-file-name 37,984
+(deflocal pg-script-portions 44,1394
+(defun proof-next-element-count 54,1630
+(defun proof-element-id 63,1957
+(defun proof-next-element-id 67,2126
+(deflocal proof-script-last-entity 81,2443
+(defun proof-script-find-next-entity 88,2723
+(deflocal proof-locked-span 164,5465
+(deflocal proof-queue-span 171,5731
+(defun proof-span-read-only 183,6245
+(defun proof-strict-read-only 190,6502
+(defsubst proof-set-locked-endpoints 219,7693
+(defsubst proof-detach-queue 223,7837
+(defsubst proof-detach-locked 227,7969
+(defsubst proof-set-queue-start 231,8105
+(defsubst proof-set-locked-end 235,8231
+(defsubst proof-set-queue-end 248,8716
+(defun proof-init-segmentation 259,9013
+(defun proof-restart-buffers 292,10408
+(defun proof-script-buffers-with-spans 314,11340
+(defun proof-script-remove-all-spans-and-deactivate 324,11696
+(defun proof-script-clear-queue-spans 328,11884
+(defun proof-unprocessed-begin 347,12445
+(defun proof-script-end 355,12699
+(defun proof-queue-or-locked-end 364,13000
+(defun proof-locked-end 379,13678
+(defun proof-locked-region-full-p 396,14063
+(defun proof-locked-region-empty-p 405,14335
+(defun proof-only-whitespace-to-locked-region-p 409,14485
+(defun proof-in-locked-region-p 422,15121
+(defun proof-goto-end-of-locked 434,15384
+(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 451,16143
+(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 462,16624
+(defun proof-end-of-locked-visible-p 476,17277
+(defun proof-goto-end-of-queue-or-locked-if-not-visible 485,17728
+(defvar pg-idioms 504,18378
+(defvar pg-visibility-specs 507,18474
+(defconst pg-default-invisibility-spec 512,18681
+(defun pg-clear-script-portions 516,18821
+(defun pg-add-script-element 530,19298
+(defun pg-remove-script-element 533,19374
+(defsubst pg-visname 541,19652
+(defun pg-add-element 545,19797
+(defun pg-open-invisible-span 579,21426
+(defun pg-remove-element 590,21789
+(defun pg-make-element-invisible 597,22059
+(defun pg-make-element-visible 603,22316
+(defun pg-toggle-element-visibility 608,22495
+(defun pg-redisplay-for-gnuemacs 616,22825
+(defun pg-show-all-portions 623,23096
+(defun pg-show-all-proofs 641,23767
+(defun pg-hide-all-proofs 646,23895
+(defun pg-add-proof-element 651,24026
+(defun pg-span-name 665,24646
+(defvar pg-span-context-menu-keymap686,25353
+(defun pg-set-span-helphighlights 699,25724
+(defun proof-complete-buffer-atomic 727,26653
+(defun proof-register-possibly-new-processed-file 768,28568
+(defun proof-inform-prover-file-retracted 819,30696
+(defun proof-auto-retract-dependencies 838,31482
+(defun proof-unregister-buffer-file-name 892,34022
+(defun proof-protected-process-or-retract 938,35845
+(defun proof-deactivate-scripting-auto 965,37015
+(defun proof-deactivate-scripting 974,37373
+(defun proof-activate-scripting 1111,42778
+(defun proof-toggle-active-scripting 1233,48210
+(defun proof-done-advancing 1274,49571
+(defun proof-done-advancing-comment 1369,53219
+(defun proof-done-advancing-save 1388,53961
+(defun proof-make-goalsave 1481,57576
+(defun proof-get-name-from-goal 1496,58319
+(defun proof-done-advancing-autosave 1515,59345
+(defun proof-done-advancing-other 1580,61891
+(defun proof-segment-up-to-parser 1608,62850
+(defun proof-script-generic-parse-find-comment-end 1671,64940
+(defun proof-script-generic-parse-cmdend 1680,65356
+(defun proof-script-generic-parse-cmdstart 1705,66251
+(defun proof-script-generic-parse-sexp 1768,68959
+(defun proof-cmdstart-add-segment-for-cmd 1792,69895
+(defun proof-segment-up-to-cmdstart 1844,72108
+(defun proof-segment-up-to-cmdend 1905,74468
+(defun proof-semis-to-vanillas 1977,77147
+(defun proof-script-new-command-advance 2016,78473
+(defun proof-script-next-command-advance 2058,80214
+(defun proof-assert-until-point-interactive 2070,80655
+(defun proof-assert-until-point 2096,81777
+(defun proof-assert-next-command2149,84209
+(defun proof-goto-point 2197,86472
+(defun proof-insert-pbp-command 2215,87013
+(defun proof-insert-sendback-command 2229,87482
+(defun proof-done-retracting 2255,88372
+(defun proof-setup-retract-action 2291,89858
+(defun proof-last-goal-or-goalsave 2301,90341
+(defun proof-retract-target 2324,91181
+(defun proof-retract-until-point-interactive 2409,94822
+(defun proof-retract-until-point 2417,95207
+(define-derived-mode proof-mode 2460,96956
+(defun proof-script-set-visited-file-name 2510,98883
+(defun proof-script-set-buffer-hooks 2534,99885
+(defun proof-script-kill-buffer-fn 2542,100303
+(defun proof-config-done-related 2586,102125
+(defun proof-generic-goal-command-p 2656,104603
+(defun proof-generic-state-preserving-p 2661,104815
+(defun proof-generic-count-undos 2670,105332
+(defun proof-generic-find-and-forget 2699,106362
+(defconst proof-script-important-settings2750,108187
+(defun proof-config-done 2765,108740
+(defun proof-setup-parsing-mechanism 2853,111858
+(defun proof-setup-imenu 2897,113711
+(defun proof-setup-func-menu 2914,114316
+
+generic/proof-shell.el,3311
+(defvar proof-marker 28,649
+(defvar proof-action-list 31,746
+(defvar proof-shell-silent 39,922
+(defvar proof-shell-last-prompt 46,1213
+(defvar proof-shell-last-output-kind 50,1384
+(defvar proof-shell-delayed-output 71,2206
+(defvar proof-shell-delayed-output-kind 74,2327
+(defcustom proof-shell-active-scripting-indicator83,2530
+(defun proof-shell-ready-prover 135,3998
+(defun proof-shell-live-buffer 149,4538
+(defun proof-shell-available-p 156,4773
+(defun proof-grab-lock 162,4996
+(defun proof-release-lock 179,5708
+(defcustom proof-shell-fiddle-frames 199,6259
+(defun proof-shell-set-text-representation 205,6482
+(defun proof-shell-start 216,6944
+(defvar proof-shell-kill-function-hooks 426,14491
+(defun proof-shell-kill-function 429,14589
+(defun proof-shell-clear-state 518,18392
+(defun proof-shell-exit 533,18835
+(defun proof-shell-bail-out 545,19280
+(defun proof-shell-restart 554,19757
+(defvar proof-shell-no-response-display 596,21141
+(defvar proof-shell-urgent-message-marker 599,21245
+(defvar proof-shell-urgent-message-scanner 602,21366
+(defun proof-shell-handle-output 606,21493
+(defun proof-shell-handle-delayed-output 649,23186
+(defvar proof-shell-no-error-display 677,24229
+(defun proof-shell-handle-error 683,24433
+(defun proof-shell-handle-interrupt 701,25269
+(defun proof-shell-error-or-interrupt-action 715,25882
+(defun proof-goals-pos 740,27027
+(defun proof-pbp-focus-on-first-goal 745,27232
+(defsubst proof-shell-string-match-safe 757,27762
+(defun proof-shell-process-output 762,27930
+(defvar proof-shell-insert-space-fudge 873,32570
+(defun proof-shell-insert 883,32889
+(defun proof-shell-command-queue-item 956,35841
+(defun proof-shell-set-silent 961,35998
+(defun proof-shell-start-silent-item 967,36217
+(defun proof-shell-clear-silent 973,36409
+(defun proof-shell-stop-silent-item 979,36631
+(defun proof-shell-should-be-silent 986,36903
+(defun proof-append-alist 999,37459
+(defun proof-start-queue 1058,39696
+(defun proof-extend-queue 1069,40045
+(defun proof-shell-exec-loop 1078,40424
+(defun proof-shell-insert-loopback-cmd 1143,43012
+(defun proof-shell-message 1171,44338
+(defun proof-shell-process-urgent-message 1177,44554
+(defun proof-shell-strip-eager-annotations 1309,49819
+(defvar proof-shell-minibuffer-urgent-interactive-input-history 1320,50155
+(defun proof-shell-minibuffer-urgent-interactive-input 1322,50225
+(defun proof-shell-process-urgent-messages 1332,50584
+(defun proof-shell-filter 1406,53683
+(defun proof-shell-filter-process-output 1567,60316
+(defvar pg-last-tracing-output-time 1620,62370
+(defconst pg-slow-mode-duration 1623,62476
+(defconst pg-fast-tracing-mode-threshold 1626,62558
+(defvar pg-tracing-cleanup-timer 1629,62686
+(defun pg-tracing-tight-loop 1631,62725
+(defun pg-finish-tracing-display 1674,64443
+(defun proof-shell-dont-show-annotations 1687,64749
+(defun proof-shell-show-annotations 1703,65270
+(defun proof-shell-wait 1725,65797
+(defun proof-done-invisible 1744,66706
+(defun proof-shell-invisible-command 1750,66878
+(defun proof-shell-invisible-cmd-get-result 1784,68143
+(defun proof-shell-invisible-command-invisible-result 1802,68839
+(define-derived-mode proof-shell-mode 1821,69269
+(defconst proof-shell-important-settings1891,71935
+(defun proof-shell-config-done 1897,72050
+
+generic/proof-site.el,504
+(defconst proof-assistant-table-default23,727
+(defconst proof-general-short-version 61,2143
+(defconst proof-general-version-year 67,2331
+(defgroup proof-general 74,2484
+(defgroup proof-general-internals 79,2592
+(defun proof-home-directory-fn 92,2980
+(defcustom proof-home-directory103,3351
+(defcustom proof-images-directory112,3718
+(defcustom proof-info-directory118,3920
+(defcustom proof-assistant-table145,5066
+(defcustom proof-assistants 180,6182
+(defun proof-ready-for-assistant 208,7327
 
 generic/proof-splash.el,726
-(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
+(defcustom proof-splash-enable 17,319
+(defcustom proof-splash-time 22,471
+(defcustom proof-splash-contents30,756
+(defconst proof-splash-startup-msg 58,1775
+(defconst proof-splash-welcome 67,2154
+(defun proof-get-image 86,2701
+(defvar proof-splash-timeout-conf 125,4052
+(defun proof-splash-centre-spaces 128,4165
+(defun proof-splash-remove-screen 156,5335
+(defun proof-splash-remove-buffer 176,6056
+(defvar proof-splash-seen 192,6720
+(defun proof-splash-display-screen 196,6837
+(defun proof-splash-message 271,9991
+(defun proof-splash-timeout-waiter 284,10435
+(defvar proof-splash-old-frame-title-format 300,11131
+(defun proof-splash-set-frame-titles 302,11181
+(defun proof-splash-unset-frame-titles 311,11497
 
 generic/proof-syntax.el,981
 (defun proof-ids-to-regexp 17,530
@@ -2148,87 +2143,88 @@ generic/proof-toolbar.el,2874
 (defun proof-toolbar-make-menu-item 537,15405
 (defun proof-toolbar-scripting-menu 560,16105
 
-generic/proof-unicode-tokens.el,493
-(defun proof-unicode-tokens-support-available 18,478
-(defvar proof-unicode-tokens-initialised 27,851
-(defun proof-unicode-tokens-init 30,958
-(defun proof-unicode-tokens-set-global 49,1493
-(defun proof-unicode-tokens-enable 64,2009
-(defun proof-token-name-alist 81,2669
-(defun proof-unicode-tokens-activate-prover 100,3353
-(defun proof-unicode-tokens-deactivate-prover 107,3596
-(defun proof-unicode-tokens-shell-config 116,3919
-(defun proof-unicode-tokens-encode-shell-input 126,4316
-
-generic/proof-utils.el,2111
-(defmacro deflocal 30,837
-(defmacro proof-with-current-buffer-if-exists 37,1075
-(deflocal proof-buffer-type 43,1285
-(defmacro proof-with-script-buffer 49,1565
-(defmacro proof-map-buffers 60,1952
-(defmacro proof-sym 65,2137
-(defsubst proof-try-require 70,2298
-(defun proof-save-some-buffers 83,2629
-(defmacro proof-ass-sym 132,4230
-(defmacro proof-ass-symv 138,4489
-(defmacro proof-ass 144,4747
-(defun proof-defpgcustom-fn 150,4999
-(defun undefpgcustom 171,5870
-(defmacro defpgcustom 177,6094
-(defun proof-defpgdefault-fn 188,6512
-(defmacro defpgdefault 202,6970
-(defmacro defpgfun 213,7332
-(defmacro proof-eval-when-ready-for-assistant 223,7597
-(defun proof-file-truename 236,7992
-(defun proof-file-to-buffer 240,8175
-(defun proof-files-to-buffers 251,8504
-(defun proof-buffers-in-mode 258,8787
-(defun pg-save-from-death 272,9237
-(defun proof-define-keys 291,9854
-(deflocal proof-font-lock-keywords 320,10853
-(defun proof-font-lock-configure-defaults 326,11110
-(defun proof-font-lock-clear-font-lock-vars 372,13261
-(defun proof-font-lock-set-font-lock-vars 378,13473
-(defun proof-fontify-region 382,13629
-(defun pg-remove-specials 444,16031
-(defun pg-remove-specials-in-string 454,16369
-(defun proof-fontify-buffer 461,16556
-(defun proof-warn-if-unset 474,16797
-(defun proof-get-window-for-buffer 479,17015
-(defun proof-display-and-keep-buffer 530,19323
-(defun proof-clean-buffer 562,20630
-(defun proof-message 577,21251
-(defun proof-warning 582,21464
-(defun pg-internal-warning 588,21746
-(defun proof-debug 596,22065
-(defun proof-switch-to-buffer 611,22736
-(defun proof-resize-window-tofit 644,24425
-(defun proof-submit-bug-report 744,28437
-(defun proof-deftoggle-fn 780,29816
-(defmacro proof-deftoggle 795,30469
-(defun proof-defintset-fn 802,30843
-(defmacro proof-defintset 818,31547
-(defun proof-defstringset-fn 825,31924
-(defmacro proof-defstringset 838,32550
-(defmacro proof-defshortcut 852,33007
-(defmacro proof-definvisible 867,33646
-(defun pg-custom-save-vars 895,34623
-(defun pg-custom-reset-vars 913,35346
-(defun proof-locate-executable 926,35683
+generic/proof-unicode-tokens.el,531
+(defun proof-unicode-tokens-support-available 20,548
+(defvar proof-unicode-tokens-initialised 29,921
+(defun proof-unicode-tokens-init 32,1028
+(defun proof-unicode-tokens-set-global 51,1563
+(defun proof-unicode-tokens-enable 66,2079
+(defun proof-token-name-alist 83,2768
+(defun proof-shortcut-alist 98,3420
+(defun proof-unicode-tokens-activate-prover 109,3756
+(defun proof-unicode-tokens-deactivate-prover 116,3999
+(defun proof-unicode-tokens-shell-config 125,4322
+(defun proof-unicode-tokens-encode-shell-input 135,4719
+
+generic/proof-utils.el,2116
+(defmacro deflocal 63,1903
+(defmacro proof-with-current-buffer-if-exists 70,2141
+(deflocal proof-buffer-type 76,2351
+(defmacro proof-with-script-buffer 82,2631
+(defmacro proof-map-buffers 93,3018
+(defmacro proof-sym 98,3203
+(defsubst proof-try-require 103,3364
+(defun proof-save-some-buffers 116,3695
+(defmacro proof-ass-sym 165,5296
+(defmacro proof-ass-symv 171,5555
+(defmacro proof-ass 177,5813
+(defun proof-defpgcustom-fn 183,6065
+(defun undefpgcustom 204,6936
+(defmacro defpgcustom 210,7160
+(defun proof-defpgdefault-fn 221,7578
+(defmacro defpgdefault 235,8036
+(defmacro defpgfun 246,8398
+(defmacro proof-eval-when-ready-for-assistant 256,8663
+(defun proof-file-truename 269,9058
+(defun proof-file-to-buffer 273,9241
+(defun proof-files-to-buffers 284,9570
+(defun proof-buffers-in-mode 291,9853
+(defun pg-save-from-death 305,10303
+(defun proof-define-keys 324,10920
+(deflocal proof-font-lock-keywords 353,11919
+(defun proof-font-lock-configure-defaults 359,12176
+(defun proof-font-lock-clear-font-lock-vars 405,14327
+(defun proof-font-lock-set-font-lock-vars 411,14539
+(defun proof-fontify-region 415,14695
+(defun pg-remove-specials 477,17097
+(defun pg-remove-specials-in-string 487,17435
+(defun proof-fontify-buffer 494,17622
+(defun proof-warn-if-unset 507,17863
+(defun proof-get-window-for-buffer 512,18081
+(defun proof-display-and-keep-buffer 563,20389
+(defun proof-clean-buffer 595,21696
+(defun proof-message 610,22317
+(defun proof-warning 615,22530
+(defun pg-internal-warning 621,22812
+(defun proof-debug 629,23131
+(defun proof-switch-to-buffer 644,23802
+(defun proof-resize-window-tofit 677,25491
+(defun proof-submit-bug-report 777,29503
+(defun proof-deftoggle-fn 813,30882
+(defmacro proof-deftoggle 828,31535
+(defun proof-defintset-fn 835,31909
+(defmacro proof-defintset 851,32613
+(defun proof-defstringset-fn 858,32990
+(defmacro proof-defstringset 871,33616
+(defmacro proof-defshortcut 885,34073
+(defmacro proof-definvisible 900,34712
+(defun pg-custom-save-vars 928,35689
+(defun pg-custom-reset-vars 946,36412
+(defun proof-locate-executable 959,36749
 
 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 186,7159
-(defun proof-x-symbol-mode-associated-buffers 201,7901
-(defun proof-x-symbol-decode-region 219,8439
-(defun proof-x-symbol-encode-shell-input 240,9436
-(defun proof-x-symbol-set-language 257,10027
-(defun proof-x-symbol-shell-config 262,10198
-(defun proof-x-symbol-config-output-buffer 309,12339
+(defvar proof-x-symbol-initialized 52,2005
+(defun proof-x-symbol-tokenlang-file 55,2100
+(defun proof-x-symbol-support-maybe-available 61,2282
+(defun proof-x-symbol-initialize 81,3011
+(defun proof-x-symbol-enable 164,6277
+(defun proof-x-symbol-refresh-output-buffers 186,7158
+(defun proof-x-symbol-mode-associated-buffers 201,7900
+(defun proof-x-symbol-decode-region 219,8438
+(defun proof-x-symbol-encode-shell-input 240,9435
+(defun proof-x-symbol-set-language 257,10026
+(defun proof-x-symbol-shell-config 262,10197
+(defun proof-x-symbol-config-output-buffer 309,12338
 
 lib/bufhist.el,1100
 (defun bufhist-ring-update 32,1226
@@ -2261,109 +2257,109 @@ lib/bufhist.el,1100
 (define-minor-mode bufhist-mode326,11534
 (defun bufhist-toggle-fn 346,12319
 
-lib/holes.el,2447
-(defvar holes-doc 35,993
-(defvar holes-default-hole 143,4976
-(defvar holes-active-hole 147,5145
-(defcustom holes-empty-hole-string 154,5354
-(defcustom holes-empty-hole-regexp 157,5465
-(defcustom holes-search-limit 164,5756
-(defface active-hole-face176,6132
-(defface inactive-hole-face188,6580
-(defun holes-region-beginning-or-nil 203,7056
-(defun holes-region-end-or-nil 208,7166
-(defun holes-copy-active-region 213,7264
-(defun holes-is-hole-p 220,7463
-(defun holes-hole-start-position 226,7570
-(defun holes-hole-end-position 233,7759
-(defun holes-hole-buffer 240,7943
-(defun holes-hole-at 247,8118
-(defun holes-active-hole-exist-p 254,8293
-(defun holes-active-hole-start-position 264,8551
-(defun holes-active-hole-end-position 274,8923
-(defun holes-active-hole-buffer 285,9292
-(defun holes-goto-active-hole 296,9598
-(defun holes-highlight-hole-as-active 308,9866
-(defun holes-highlight-hole 318,10178
-(defun holes-disable-active-hole 329,10470
-(defun holes-set-active-hole 347,11013
-(defun holes-is-in-hole-p 360,11359
-(defun holes-make-hole 367,11502
-(defun holes-make-hole-at 393,12248
-(defun holes-clear-hole 413,12724
-(defun holes-clear-hole-at 425,13013
-(defun holes-map-holes 434,13272
-(defun holes-mapcar-holes 442,13455
-(defun holes-clear-all-buffer-holes 448,13627
-(defun holes-next 459,13927
-(defun holes-next-after-active-hole 466,14178
-(defun holes-set-active-hole-next 474,14397
-(defun holes-replace-segment 496,14950
-(defun holes-replace 506,15304
-(defun holes-replace-active-hole 537,16499
-(defun holes-replace-update-active-hole 546,16800
-(defun holes-delete-update-active-hole 567,17490
-(defun holes-set-make-active-hole 574,17704
-(defun holes-mouse-replace-active-hole 621,19429
-(defun holes-destroy-hole 641,19968
-(defun holes-hole-at-event 658,20379
-(defun holes-mouse-destroy-hole 663,20492
-(defun holes-mouse-forget-hole 673,20732
-(defun holes-mouse-set-make-active-hole 689,21042
-(defun holes-mouse-set-active-hole 711,21603
-(defun holes-set-point-next-hole-destroy 723,21867
-(defvar hole-map739,22317
-(defvar holes-mode-map755,22937
-(defun holes-replace-string-by-holes-backward 792,24402
-(defun holes-skeleton-end-hook 810,25103
-(defconst holes-jump-doc 819,25541
-(defun holes-replace-string-by-holes-backward-jump 826,25748
-(defun holes-abbrev-complete 843,26379
-(defun holes-insert-and-expand 852,26686
-(defvar holes-mode 863,27118
-(defun holes-mode 869,27314
-
-lib/local-vars-list.el,372
-(defconst local-vars-list-doc 25,759
-(defun local-vars-list-insert-empty-zone 41,1323
-(defun local-vars-list-find 79,2031
-(defun local-vars-list-goto-var 98,2806
-(defun local-vars-list-get-current 124,3856
-(defun local-vars-list-set-current 145,4706
-(defun local-vars-list-get 168,5423
-(defun local-vars-list-get-safe 185,5955
-(defun local-vars-list-set 190,6149
+lib/holes.el,2448
+(defvar holes-doc 37,1048
+(defvar holes-default-hole 145,5031
+(defvar holes-active-hole 149,5200
+(defcustom holes-empty-hole-string 156,5409
+(defcustom holes-empty-hole-regexp 159,5520
+(defcustom holes-search-limit 166,5811
+(defface active-hole-face178,6187
+(defface inactive-hole-face190,6635
+(defun holes-region-beginning-or-nil 205,7111
+(defun holes-region-end-or-nil 210,7221
+(defun holes-copy-active-region 215,7319
+(defun holes-is-hole-p 222,7518
+(defun holes-hole-start-position 228,7625
+(defun holes-hole-end-position 235,7814
+(defun holes-hole-buffer 242,7998
+(defun holes-hole-at 249,8173
+(defun holes-active-hole-exist-p 256,8348
+(defun holes-active-hole-start-position 266,8606
+(defun holes-active-hole-end-position 276,8978
+(defun holes-active-hole-buffer 287,9347
+(defun holes-goto-active-hole 298,9653
+(defun holes-highlight-hole-as-active 310,9921
+(defun holes-highlight-hole 320,10233
+(defun holes-disable-active-hole 331,10525
+(defun holes-set-active-hole 349,11068
+(defun holes-is-in-hole-p 362,11414
+(defun holes-make-hole 369,11557
+(defun holes-make-hole-at 395,12303
+(defun holes-clear-hole 415,12779
+(defun holes-clear-hole-at 427,13068
+(defun holes-map-holes 436,13327
+(defun holes-mapcar-holes 444,13510
+(defun holes-clear-all-buffer-holes 450,13682
+(defun holes-next 461,13982
+(defun holes-next-after-active-hole 468,14233
+(defun holes-set-active-hole-next 476,14452
+(defun holes-replace-segment 498,15005
+(defun holes-replace 508,15359
+(defun holes-replace-active-hole 539,16554
+(defun holes-replace-update-active-hole 548,16855
+(defun holes-delete-update-active-hole 569,17545
+(defun holes-set-make-active-hole 576,17759
+(defun holes-mouse-replace-active-hole 623,19484
+(defun holes-destroy-hole 643,20023
+(defun holes-hole-at-event 660,20434
+(defun holes-mouse-destroy-hole 665,20547
+(defun holes-mouse-forget-hole 675,20787
+(defun holes-mouse-set-make-active-hole 691,21097
+(defun holes-mouse-set-active-hole 713,21658
+(defun holes-set-point-next-hole-destroy 725,21922
+(defvar hole-map741,22372
+(defvar holes-mode-map757,22992
+(defun holes-replace-string-by-holes-backward 794,24457
+(defun holes-skeleton-end-hook 812,25158
+(defconst holes-jump-doc 821,25596
+(defun holes-replace-string-by-holes-backward-jump 828,25803
+(defun holes-abbrev-complete 845,26434
+(defun holes-insert-and-expand 854,26741
+(defvar holes-mode 865,27173
+(defun holes-mode 871,27369
+
+lib/local-vars-list.el,373
+(defconst local-vars-list-doc 28,827
+(defun local-vars-list-insert-empty-zone 44,1391
+(defun local-vars-list-find 82,2099
+(defun local-vars-list-goto-var 101,2874
+(defun local-vars-list-get-current 127,3924
+(defun local-vars-list-set-current 148,4774
+(defun local-vars-list-get 171,5491
+(defun local-vars-list-get-safe 188,6023
+(defun local-vars-list-set 193,6217
 
 lib/maths-menu.el,153
-(defun maths-menu-build-menu 48,2022
-(defvar maths-menu-menu67,2690
-(defvar maths-menu-mode-map312,11648
-(define-minor-mode maths-menu-mode340,12674
+(defun maths-menu-build-menu 51,2136
+(defvar maths-menu-menu70,2804
+(defvar maths-menu-mode-map315,11762
+(define-minor-mode maths-menu-mode323,11981
 
 lib/pg-dev.el,75
-(defconst pg-dev-lisp-font-lock-keywords35,1049
-(defun unload-pg 69,1986
+(defconst pg-dev-lisp-font-lock-keywords36,1102
+(defun unload-pg 70,2039
 
 lib/proof-compat.el,751
-(defvar proof-running-on-win32 29,914
-(defun pg-custom-undeclare-variable 49,1709
-(defun subst-char-in-string 139,4497
-(defun replace-regexp-in-string 154,5086
-(defconst menuvisiblep 216,7799
-(defun set-window-text-height 233,8412
-(defmacro save-selected-frame 259,9362
-(defun warn 298,10659
-(defun redraw-modeline 305,10914
-(defun proof-buffer-syntactic-context-emulate 316,11352
-(defvar read-shell-command-map349,12659
-(defun read-shell-command 367,13347
-(defun remassq 379,13828
-(defun remassoc 391,14217
-(defun frames-of-buffer 404,14662
-(defmacro with-selected-window 443,15924
-(defun pg-pop-to-buffer 486,17302
-(defun process-live-p 537,19135
-(defalias 'proof-buffer-syntactic-context proof-buffer-syntactic-context
554,19638
+(defvar proof-running-on-win32 29,913
+(defun pg-custom-undeclare-variable 49,1708
+(defun subst-char-in-string 139,4496
+(defun replace-regexp-in-string 154,5085
+(defconst menuvisiblep 216,7798
+(defun set-window-text-height 233,8411
+(defmacro save-selected-frame 259,9361
+(defun warn 298,10658
+(defun redraw-modeline 305,10913
+(defun proof-buffer-syntactic-context-emulate 316,11351
+(defvar read-shell-command-map349,12658
+(defun read-shell-command 367,13346
+(defun remassq 379,13827
+(defun remassoc 391,14216
+(defun frames-of-buffer 404,14661
+(defmacro with-selected-window 443,15923
+(defun pg-pop-to-buffer 486,17301
+(defun process-live-p 537,19163
+(defalias 'proof-buffer-syntactic-context proof-buffer-syntactic-context
556,19778
 
 lib/span.el,137
 (defsubst span-delete-spans 22,479
@@ -2457,38 +2453,38 @@ lib/unicode-chars.el,80
 (defvar unicode-chars-alist12,348
 (defun unicode-chars-list-chars 5050,245960
 
-lib/unicode-tokens.el,1481
-(defvar unicode-tokens-charref-format 44,1549
-(defvar unicode-tokens-token-format 47,1646
-(defvar unicode-tokens-token-name-alist 50,1737
-(defvar unicode-tokens-glyph-list 53,1830
-(defvar unicode-tokens-token-prefix 57,1974
-(defvar unicode-tokens-token-suffix 60,2058
-(defvar unicode-tokens-token-match 63,2140
-(defvar unicode-tokens-hexcode-match 66,2225
-(defvar unicode-tokens-shortcut-alist69,2332
-(defvar unicode-tokens-max-token-length 79,2570
-(defvar unicode-tokens-codept-charname-alist 82,2669
-(defvar unicode-tokens-token-alist 85,2777
-(defvar unicode-tokens-ustring-alist 88,2860
-(defun unicode-tokens-insert-char 96,2963
-(defun unicode-tokens-insert-string 106,3384
-(defun unicode-tokens-character-insert 116,3761
-(defun unicode-tokens-token-insert 138,4669
-(defun unicode-tokens-replace-token-after 159,5566
-(defun unicode-tokens-looking-backward-at 181,6315
-(defun unicode-tokens-electric-suffix 192,6777
-(defvar unicode-tokens-rotate-glyph-last-char 238,8343
-(defun unicode-tokens-rotate-glyph-forward 240,8395
-(defun unicode-tokens-rotate-glyph-backward 266,9377
-(defun unicode-tokens-map-ordering 283,9754
-(defun unicode-tokens-quail-define-rules 287,9904
-(defvar unicode-tokens-format-entry334,11510
-(defun unicode-tokens-tokens-to-unicode 342,11732
-(defun unicode-tokens-unicode-to-tokens 353,12106
-(defvar unicode-tokens-mode-map 367,12419
-(define-minor-mode unicode-tokens-mode370,12516
-(defun unicode-tokens-initialise 394,13284
+lib/unicode-tokens.el,1484
+(defvar unicode-tokens-charref-format 51,1831
+(defvar unicode-tokens-token-format 54,1928
+(defvar unicode-tokens-token-name-alist 57,2019
+(defvar unicode-tokens-glyph-list 60,2112
+(defvar unicode-tokens-token-prefix 64,2256
+(defvar unicode-tokens-token-suffix 67,2340
+(defvar unicode-tokens-token-match 70,2422
+(defvar unicode-tokens-hexcode-match 73,2507
+(defvar unicode-tokens-shortcut-alist76,2614
+(defvar unicode-tokens-max-token-length 86,2852
+(defvar unicode-tokens-codept-charname-alist 89,2951
+(defvar unicode-tokens-token-alist 92,3059
+(defvar unicode-tokens-ustring-alist 95,3142
+(defun unicode-tokens-insert-char 103,3245
+(defun unicode-tokens-insert-string 113,3666
+(defun unicode-tokens-character-insert 123,4043
+(defun unicode-tokens-token-insert 145,4951
+(defun unicode-tokens-replace-token-after 166,5848
+(defun unicode-tokens-looking-backward-at 188,6597
+(defun unicode-tokens-electric-suffix 199,7059
+(defvar unicode-tokens-rotate-glyph-last-char 245,8623
+(defun unicode-tokens-rotate-glyph-forward 247,8675
+(defun unicode-tokens-rotate-glyph-backward 276,9857
+(defun unicode-tokens-map-ordering 296,10435
+(defun unicode-tokens-quail-define-rules 300,10585
+(defvar unicode-tokens-format-entry347,12191
+(defun unicode-tokens-tokens-to-unicode 355,12413
+(defun unicode-tokens-unicode-to-tokens 366,12787
+(defvar unicode-tokens-mode-map 380,13100
+(define-minor-mode unicode-tokens-mode383,13197
+(defun unicode-tokens-initialise 407,13965
 
 lib/xml-fixed.el,528
 (defsubst xml-node-name 82,2904
@@ -2883,137 +2879,137 @@ x-symbol/lisp/x-symbol.el,9210
 (defun x-symbol-init-font-lock 1363,56734
 (defun x-symbol-set-image 1395,58322
 (defun x-symbol-mode-internal 1413,59068
-(defun nuke-x-symbol 1487,62171
-(defun x-symbol-options-filter 1500,62624
-(defun x-symbol-extra-filter 1536,63780
-(defun x-symbol-menu-filter 1544,64028
-(defvar x-symbol-list-mode-map1574,65007
-(defvar x-symbol-list-buffer 1600,66157
-(defvar x-symbol-list-win-config 1602,66233
-(defvar x-symbol-invisible-spec 1604,66344
-(defvar x-symbol-itimer 1608,66494
-(defvar x-symbol-invisible-display-table1611,66577
-(defvar x-symbol-invisible-font 1620,66813
-(defvar x-symbol-charsym-info-cache 1645,68000
-(defvar x-symbol-language-info-caches 1647,68091
-(defvar x-symbol-coding-info-cache 1649,68185
-(defvar x-symbol-keys-info-cache 1651,68274
-(defun x-symbol-list-bury 1659,68579
-(defun x-symbol-list-restore 1665,68775
-(defun x-symbol-list-store 1695,69993
-(defun x-symbol-list-mode 1704,70410
-(defun x-symbol-list-scroll 1725,71212
-(defun x-symbol-init-language-interactive 1748,71854
-(defun x-symbol-list-menu 1765,72568
-(defun x-symbol-list-selected 1820,74476
-(defun x-symbol-list-menu-selected 1846,75685
-(defun x-symbol-list-mouse-selected 1857,76138
-(defun x-symbol-charsym-info 1874,76860
-(defun x-symbol-language-info 1888,77461
-(defun x-symbol-coding-info 1920,78661
-(defun x-symbol-keys-info 1940,79433
-(defun x-symbol-info 1964,80356
-(defun x-symbol-list-info 1977,80894
-(defun x-symbol-highlight-echo 1991,81437
-(defun x-symbol-point-info 2002,81986
-(defun x-symbol-hide-revealed-at-point 2048,83908
-(defun x-symbol-reveal-invisible 2085,85575
-(defun x-symbol-show-info-and-invisible 2133,87767
-(defun x-symbol-start-itimer-once 2169,89309
-(defun x-symbol-setup-minibuffer 2185,89935
-(defvar x-symbol-language-history 2203,90506
-(defvar x-symbol-token-history 2206,90630
-(defvar x-symbol-last-abbrev 2209,90706
-(defvar x-symbol-electric-pos 2211,90802
-(defvar x-symbol-command-keys 2214,90884
-(defvar x-symbol-help-keys 2218,91015
-(defvar x-symbol-help-language 2220,91110
-(defvar x-symbol-help-completions 2222,91209
-(defvar x-symbol-help-completions1 2224,91301
-(defun x-symbol-map-default-binding 2232,91577
-(defun x-symbol-read-charsym-token 2263,92655
-(defun x-symbol-insert-command 2289,93578
-(defun x-symbol-read-language 2340,95585
-(defun x-symbol-read-token 2355,96263
-(defun x-symbol-read-token-direct 2394,97772
-(defun x-symbol-grid 2406,98172
-(defun x-symbol-replace-from 2494,101788
-(defvar x-symbol-token-search-prelude-size 2530,103289
-(defun x-symbol-replace-token 2532,103337
-(defun x-symbol-match-token-before 2557,104428
-(defun x-symbol-token-input 2601,106231
-(defun x-symbol-modify-key 2622,107061
-(defun x-symbol-rotate-key 2655,108390
-(defun x-symbol-electric-input 2709,110600
-(defun x-symbol-help-mapper 2751,112301
-(defun x-symbol-help-output 2774,113140
-(defun x-symbol-help 2817,114736
-(defvar x-symbol-face-docstrings2870,116805
-(defvar x-symbol-all-key-prefixes 2876,116993
-(defvar x-symbol-all-key-chain-alist 2878,117104
-(defvar x-symbol-all-horizontal-chain-alist 2880,117203
-(defvar x-symbol-all-chain-subchains-alist 2882,117316
-(defvar x-symbol-all-exclusive-context-alist 2884,117430
-(defalias 'x-symbol-table-grouping x-symbol-table-grouping
2892,117726
-(defalias 'x-symbol-table-aspects x-symbol-table-aspects
2893,117767
-(defalias 'x-symbol-table-score x-symbol-table-score
2894,117808
-(defalias 'x-symbol-table-input x-symbol-table-input
2895,117848
-(defsubst x-symbol-table-prefixes 2896,117889
-(defsubst x-symbol-table-junk 2897,117940
-(defsubst x-symbol-charsym-defined-p 2899,117991
-(defun x-symbol-try-font-name-0 2907,118292
-(defun x-symbol-try-font-name 2925,118848
-(defun x-symbol-set-cstrings 2942,119364
-(defun x-symbol-init-charsym-command 2987,121342
-(defun x-symbol-init-charsym-input 2995,121708
-(defun x-symbol-init-charsym-aspects 3064,124426
-(defun x-symbol-init-cset 3094,125706
-(defun x-symbol-make-atree 3244,132529
-(defun x-symbol-atree-push 3248,132609
-(defun x-symbol-component-root-p 3268,133298
-(defun x-symbol-component-elements 3272,133437
-(defun x-symbol-component-merge 3279,133685
-(defun x-symbol-component-space 3293,134233
-(defun x-symbol-modify-less-than 3307,134817
-(defun x-symbol-inherit-aspects 3312,135040
-(defun x-symbol-compute-aspects 3321,135479
-(defun x-symbol-init-aspects 3337,136197
-(defun x-symbol-sort-modify-chain 3382,138246
-(defun x-symbol-init-horizontal/key-alist 3397,138818
-(defun x-symbol-init-exclusive-alist 3413,139564
-(defun x-symbol-init-horizontal-chain 3451,141168
-(defun x-symbol-init-exclusive-chain 3459,141500
-(defun x-symbol-init-rotate-chain 3466,141827
-(defun x-symbol-init-context-atree 3487,142701
-(defun x-symbol-init-key-bindings 3532,144984
-(defun x-symbol-rotate-modify-less-than 3555,145907
-(defun x-symbol-subgroup-less-than 3563,146302
-(defun x-symbol-header-charsyms 3568,146559
-(defun x-symbol-init-grid/menu 3594,147609
-(defun x-symbol-init-input 3666,150265
-(defun x-symbol-init-latin-decoding 3796,156741
-(defun x-symbol-get-prime-for 3837,158612
-(defun x-symbol-alist-to-obarray 3846,158936
-(defun x-symbol-alist-to-hash-table 3852,159144
-(defun x-symbol-init-language 3862,159477
-(defvar x-symbol-latin1-cset3986,164942
-(defvar x-symbol-latin2-cset3992,165115
-(defvar x-symbol-latin3-cset3998,165288
-(defvar x-symbol-latin5-cset4004,165461
-(defvar x-symbol-latin9-cset4010,165633
-(defvar x-symbol-xsymb0-cset4016,165839
-(defvar x-symbol-xsymb1-cset4022,166094
-(defvar x-symbol-latin1-table4028,166336
-(defvar x-symbol-latin2-table4129,170806
-(defvar x-symbol-latin3-table4228,174007
-(defvar x-symbol-latin5-table4327,176888
-(defvar x-symbol-latin9-table4426,179198
-(defvar x-symbol-xsymb0-table4525,181588
-(defvar x-symbol-xsymb1-table4675,188984
-(defvar x-symbol-no-of-charsyms 4883,199619
-(defun x-symbol-mac-setup1 4891,199985
-(defun x-symbol-mac-setup2 4909,200630
-(defun x-symbol-startup 4934,201493
+(defun nuke-x-symbol 1487,62177
+(defun x-symbol-options-filter 1500,62630
+(defun x-symbol-extra-filter 1536,63786
+(defun x-symbol-menu-filter 1544,64034
+(defvar x-symbol-list-mode-map1574,65013
+(defvar x-symbol-list-buffer 1600,66163
+(defvar x-symbol-list-win-config 1602,66239
+(defvar x-symbol-invisible-spec 1604,66350
+(defvar x-symbol-itimer 1608,66500
+(defvar x-symbol-invisible-display-table1611,66583
+(defvar x-symbol-invisible-font 1620,66819
+(defvar x-symbol-charsym-info-cache 1645,68006
+(defvar x-symbol-language-info-caches 1647,68097
+(defvar x-symbol-coding-info-cache 1649,68191
+(defvar x-symbol-keys-info-cache 1651,68280
+(defun x-symbol-list-bury 1659,68585
+(defun x-symbol-list-restore 1665,68781
+(defun x-symbol-list-store 1695,69999
+(defun x-symbol-list-mode 1704,70416
+(defun x-symbol-list-scroll 1725,71218
+(defun x-symbol-init-language-interactive 1748,71860
+(defun x-symbol-list-menu 1765,72574
+(defun x-symbol-list-selected 1820,74482
+(defun x-symbol-list-menu-selected 1846,75691
+(defun x-symbol-list-mouse-selected 1857,76144
+(defun x-symbol-charsym-info 1874,76866
+(defun x-symbol-language-info 1888,77467
+(defun x-symbol-coding-info 1920,78667
+(defun x-symbol-keys-info 1940,79439
+(defun x-symbol-info 1964,80362
+(defun x-symbol-list-info 1977,80900
+(defun x-symbol-highlight-echo 1991,81443
+(defun x-symbol-point-info 2002,81992
+(defun x-symbol-hide-revealed-at-point 2048,83914
+(defun x-symbol-reveal-invisible 2085,85581
+(defun x-symbol-show-info-and-invisible 2133,87773
+(defun x-symbol-start-itimer-once 2169,89315
+(defun x-symbol-setup-minibuffer 2185,89941
+(defvar x-symbol-language-history 2203,90512
+(defvar x-symbol-token-history 2206,90636
+(defvar x-symbol-last-abbrev 2209,90712
+(defvar x-symbol-electric-pos 2211,90808
+(defvar x-symbol-command-keys 2214,90890
+(defvar x-symbol-help-keys 2218,91021
+(defvar x-symbol-help-language 2220,91116
+(defvar x-symbol-help-completions 2222,91215
+(defvar x-symbol-help-completions1 2224,91307
+(defun x-symbol-map-default-binding 2232,91583
+(defun x-symbol-read-charsym-token 2263,92661
+(defun x-symbol-insert-command 2289,93584
+(defun x-symbol-read-language 2340,95591
+(defun x-symbol-read-token 2355,96269
+(defun x-symbol-read-token-direct 2394,97778
+(defun x-symbol-grid 2406,98178
+(defun x-symbol-replace-from 2494,101794
+(defvar x-symbol-token-search-prelude-size 2530,103295
+(defun x-symbol-replace-token 2532,103343
+(defun x-symbol-match-token-before 2557,104434
+(defun x-symbol-token-input 2601,106237
+(defun x-symbol-modify-key 2622,107067
+(defun x-symbol-rotate-key 2655,108396
+(defun x-symbol-electric-input 2709,110606
+(defun x-symbol-help-mapper 2751,112307
+(defun x-symbol-help-output 2774,113146
+(defun x-symbol-help 2817,114742
+(defvar x-symbol-face-docstrings2870,116811
+(defvar x-symbol-all-key-prefixes 2876,116999
+(defvar x-symbol-all-key-chain-alist 2878,117110
+(defvar x-symbol-all-horizontal-chain-alist 2880,117209
+(defvar x-symbol-all-chain-subchains-alist 2882,117322
+(defvar x-symbol-all-exclusive-context-alist 2884,117436
+(defalias 'x-symbol-table-grouping x-symbol-table-grouping
2892,117732
+(defalias 'x-symbol-table-aspects x-symbol-table-aspects
2893,117773
+(defalias 'x-symbol-table-score x-symbol-table-score
2894,117814
+(defalias 'x-symbol-table-input x-symbol-table-input
2895,117854
+(defsubst x-symbol-table-prefixes 2896,117895
+(defsubst x-symbol-table-junk 2897,117946
+(defsubst x-symbol-charsym-defined-p 2899,117997
+(defun x-symbol-try-font-name-0 2907,118298
+(defun x-symbol-try-font-name 2925,118854
+(defun x-symbol-set-cstrings 2942,119370
+(defun x-symbol-init-charsym-command 2987,121348
+(defun x-symbol-init-charsym-input 2995,121714
+(defun x-symbol-init-charsym-aspects 3064,124432
+(defun x-symbol-init-cset 3094,125712
+(defun x-symbol-make-atree 3244,132535
+(defun x-symbol-atree-push 3248,132615
+(defun x-symbol-component-root-p 3268,133304
+(defun x-symbol-component-elements 3272,133443
+(defun x-symbol-component-merge 3279,133691
+(defun x-symbol-component-space 3293,134239
+(defun x-symbol-modify-less-than 3307,134823
+(defun x-symbol-inherit-aspects 3312,135046
+(defun x-symbol-compute-aspects 3321,135485
+(defun x-symbol-init-aspects 3337,136203
+(defun x-symbol-sort-modify-chain 3382,138252
+(defun x-symbol-init-horizontal/key-alist 3397,138824
+(defun x-symbol-init-exclusive-alist 3413,139570
+(defun x-symbol-init-horizontal-chain 3451,141174
+(defun x-symbol-init-exclusive-chain 3459,141506
+(defun x-symbol-init-rotate-chain 3466,141833
+(defun x-symbol-init-context-atree 3487,142707
+(defun x-symbol-init-key-bindings 3532,144990
+(defun x-symbol-rotate-modify-less-than 3555,145913
+(defun x-symbol-subgroup-less-than 3563,146308
+(defun x-symbol-header-charsyms 3568,146565
+(defun x-symbol-init-grid/menu 3594,147615
+(defun x-symbol-init-input 3666,150271
+(defun x-symbol-init-latin-decoding 3796,156747
+(defun x-symbol-get-prime-for 3837,158618
+(defun x-symbol-alist-to-obarray 3846,158942
+(defun x-symbol-alist-to-hash-table 3852,159150
+(defun x-symbol-init-language 3862,159483
+(defvar x-symbol-latin1-cset3986,164948
+(defvar x-symbol-latin2-cset3992,165121
+(defvar x-symbol-latin3-cset3998,165294
+(defvar x-symbol-latin5-cset4004,165467
+(defvar x-symbol-latin9-cset4010,165639
+(defvar x-symbol-xsymb0-cset4016,165845
+(defvar x-symbol-xsymb1-cset4022,166100
+(defvar x-symbol-latin1-table4028,166342
+(defvar x-symbol-latin2-table4129,170812
+(defvar x-symbol-latin3-table4228,174013
+(defvar x-symbol-latin5-table4327,176894
+(defvar x-symbol-latin9-table4426,179204
+(defvar x-symbol-xsymb0-table4525,181594
+(defvar x-symbol-xsymb1-table4675,188990
+(defvar x-symbol-no-of-charsyms 4883,199625
+(defun x-symbol-mac-setup1 4891,199991
+(defun x-symbol-mac-setup2 4909,200636
+(defun x-symbol-startup 4935,201502
 
 x-symbol/lisp/x-symbol-emacs.el,1126
 (defun emacs-version>=33,1289
@@ -3530,156 +3526,157 @@ 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,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
399,13374
-@node Installing Proof GeneralInstalling Proof General
455,15416
-@node Quick start guideQuick start guide
469,15865
-@node Features of Proof GeneralFeatures of Proof General
513,17986
-@node Supported proof assistantsSupported proof assistants
602,21923
-@node Prerequisites for this manualPrerequisites for this manual
651,23829
-@node Organization of this manualOrganization of this manual
695,25455
-@node Basic Script ManagementBasic Script Management
721,26283
-@node Walkthrough example in IsabelleWalkthrough example in Isabelle
740,26883
-@node Proof scriptsProof scripts
991,36536
-@node Script buffersScript buffers
1034,38656
-@node Locked queue and editing regionsLocked queue and editing regions
1056,39233
-@node Goal-save sequencesGoal-save sequences
1112,41380
-@node Active scripting bufferActive scripting buffer
1149,42866
-@node Summary of Proof General buffersSummary of Proof General buffers
1218,46286
-@node Script editing commandsScript editing commands
1280,48960
-@node Script processing commandsScript processing commands
1358,51819
-@node Proof assistant commandsProof assistant commands
1486,57120
-@node Toolbar commandsToolbar commands
1652,62899
-@node Interrupting during trace outputInterrupting during trace output
1676,63828
-@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
1715,65752
-@node Goals buffer commandsGoals buffer commands
1729,66252
-@node Advanced Script Management and EditingAdvanced Script Management and Editing
1818,69791
-@node Visibility of completed proofsVisibility of completed proofs
1850,71003
-@node Switching between proof scriptsSwitching between proof scripts
1905,72926
-@node View of processed files View of processed files 
1942,74898
-@node Retracting across filesRetracting across files
2002,77949
-@node Asserting across filesAsserting across files
2015,78580
-@node Automatic multiple file handlingAutomatic multiple file handling
2028,79146
-@node Escaping script managementEscaping script management
2053,80180
-@node Editing featuresEditing features
2111,82383
-@node Experimental featuresExperimental features
2175,85055
-@node Support for other PackagesSupport for other Packages
2212,86426
-@node Syntax highlightingSyntax highlighting
2244,87301
-@node X-Symbol supportX-Symbol support
2283,88922
-@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)
2342,91468
-@node Support for outline modeSupport for outline mode
2401,93598
-@node Support for completionSupport for completion
2427,94728
-@node Support for tagsSupport for tags
2485,96904
-@node Customizing Proof GeneralCustomizing Proof General
2537,99233
-@node Basic optionsBasic options
2577,100903
-@node How to customizeHow to customize
2601,101661
-@node Display customizationDisplay customization
2652,103763
-@node User optionsUser options
2777,109001
-@node Changing facesChanging faces
3049,118637
-@node Tweaking configuration settingsTweaking configuration settings
3124,121306
-@node Hints and TipsHints and Tips
3181,123832
-@node Adding your own keybindingsAdding your own keybindings
3200,124433
-@node Using file variablesUsing file variables
3256,126966
-@node Using abbreviationsUsing abbreviations
3315,129152
-@node LEGO Proof GeneralLEGO Proof General
3354,130568
-@node LEGO specific commandsLEGO specific commands
3395,131937
-@node LEGO tagsLEGO tags
3415,132392
-@node LEGO customizationsLEGO customizations
3425,132639
-@node Coq Proof GeneralCoq Proof General
3457,133558
-@node Coq-specific commandsCoq-specific commands
3473,133967
-@node Coq-specific variablesCoq-specific variables
3495,134474
-@node Editing multiple proofsEditing multiple proofs
3517,135132
-@node User-loaded tacticsUser-loaded tactics
3541,136240
-@node Holes featureHoles feature
3605,138714
-@node Isabelle Proof GeneralIsabelle Proof General
3632,140001
-@node Isabelle commandsIsabelle commands
3662,141131
-@node Logics and SettingsLogics and Settings
3807,145288
-@node Isabelle customizationsIsabelle customizations
3841,146828
-@node HOL Proof GeneralHOL Proof General
3865,147310
-@node Shell Proof GeneralShell Proof General
3907,149132
-@node Obtaining and InstallingObtaining and Installing
3943,150591
-@node Obtaining Proof GeneralObtaining Proof General
3959,151004
-@node Installing Proof General from tarballInstalling Proof General from tarball
3990,152243
-@node Installing Proof General from RPM packageInstalling Proof General from RPM package
4015,153075
-@node Setting the names of binariesSetting the names of binaries
4030,153483
-@node Notes for syssiesNotes for syssies
4058,154423
-@node Bugs and EnhancementsBugs and Enhancements
4133,157459
-@node References4154,158274
-@node History of Proof GeneralHistory of Proof General
4194,159298
-@node Old News for 3.0Old News for 3.0
4285,163400
-@node Old News for 3.1Old News for 3.1
4355,167094
-@node Old News for 3.2Old News for 3.2
4381,168266
-@node Old News for 3.3Old News for 3.3
4442,171269
-@node Old News for 3.4Old News for 3.4
4461,172166
-@node Function IndexFunction Index
4484,173222
-@node Variable IndexVariable Index
4488,173298
-@node Keystroke IndexKeystroke Index
4492,173378
-@node Concept IndexConcept Index
4496,173444
+doc/ProofGeneral.texi,5509
+@node Top167,5089
+@node Preface204,6217
+@node Latest news for version 3.7Latest news for version 3.7
227,6813
+@node Future269,8735
+@node Credits300,10034
+@node Introducing Proof GeneralIntroducing Proof General
406,13803
+@node Installing Proof GeneralInstalling Proof General
462,15845
+@node Quick start guideQuick start guide
476,16294
+@node Features of Proof GeneralFeatures of Proof General
520,18415
+@node Supported proof assistantsSupported proof assistants
609,22352
+@node Prerequisites for this manualPrerequisites for this manual
658,24258
+@node Organization of this manualOrganization of this manual
702,25884
+@node Basic Script ManagementBasic Script Management
728,26712
+@node Walkthrough example in IsabelleWalkthrough example in Isabelle
747,27312
+@node Proof scriptsProof scripts
998,36965
+@node Script buffersScript buffers
1041,39085
+@node Locked queue and editing regionsLocked queue and editing regions
1063,39662
+@node Goal-save sequencesGoal-save sequences
1119,41809
+@node Active scripting bufferActive scripting buffer
1156,43295
+@node Summary of Proof General buffersSummary of Proof General buffers
1225,46715
+@node Script editing commandsScript editing commands
1287,49389
+@node Script processing commandsScript processing commands
1365,52248
+@node Proof assistant commandsProof assistant commands
1493,57549
+@node Toolbar commandsToolbar commands
1659,63328
+@node Interrupting during trace outputInterrupting during trace output
1683,64257
+@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
1722,66181
+@node Goals buffer commandsGoals buffer commands
1736,66681
+@node Advanced Script Management and EditingAdvanced Script Management and Editing
1825,70220
+@node Visibility of completed proofsVisibility of completed proofs
1857,71432
+@node Switching between proof scriptsSwitching between proof scripts
1912,73355
+@node View of processed files View of processed files 
1949,75327
+@node Retracting across filesRetracting across files
2009,78378
+@node Asserting across filesAsserting across files
2022,79009
+@node Automatic multiple file handlingAutomatic multiple file handling
2035,79575
+@node Escaping script managementEscaping script management
2060,80609
+@node Editing featuresEditing features
2118,82812
+@node Experimental featuresExperimental features
2182,85484
+@node Support for other PackagesSupport for other Packages
2216,86748
+@node Syntax highlightingSyntax highlighting
2249,87643
+@node X-Symbol supportX-Symbol support
2288,89264
+@node Unicode supportUnicode support
2346,91804
+@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)
2461,96601
+@node Support for outline modeSupport for outline mode
2520,98731
+@node Support for completionSupport for completion
2546,99861
+@node Support for tagsSupport for tags
2604,102037
+@node Customizing Proof GeneralCustomizing Proof General
2656,104366
+@node Basic optionsBasic options
2696,106036
+@node How to customizeHow to customize
2720,106794
+@node Display customizationDisplay customization
2771,108896
+@node User optionsUser options
2896,114134
+@node Changing facesChanging faces
3168,123833
+@node Tweaking configuration settingsTweaking configuration settings
3243,126502
+@node Hints and TipsHints and Tips
3300,129028
+@node Adding your own keybindingsAdding your own keybindings
3319,129629
+@node Using file variablesUsing file variables
3375,132162
+@node Using abbreviationsUsing abbreviations
3434,134348
+@node LEGO Proof GeneralLEGO Proof General
3473,135764
+@node LEGO specific commandsLEGO specific commands
3514,137133
+@node LEGO tagsLEGO tags
3534,137588
+@node LEGO customizationsLEGO customizations
3544,137835
+@node Coq Proof GeneralCoq Proof General
3576,138754
+@node Coq-specific commandsCoq-specific commands
3592,139163
+@node Coq-specific variablesCoq-specific variables
3614,139670
+@node Editing multiple proofsEditing multiple proofs
3636,140328
+@node User-loaded tacticsUser-loaded tactics
3660,141436
+@node Holes featureHoles feature
3724,143910
+@node Isabelle Proof GeneralIsabelle Proof General
3751,145197
+@node Isabelle commandsIsabelle commands
3781,146327
+@node Logics and SettingsLogics and Settings
3926,150484
+@node Isabelle customizationsIsabelle customizations
3960,152024
+@node HOL Proof GeneralHOL Proof General
3984,152506
+@node Shell Proof GeneralShell Proof General
4026,154328
+@node Obtaining and InstallingObtaining and Installing
4062,155787
+@node Obtaining Proof GeneralObtaining Proof General
4078,156200
+@node Installing Proof General from tarballInstalling Proof General from tarball
4109,157439
+@node Installing Proof General from RPM packageInstalling Proof General from RPM package
4134,158271
+@node Setting the names of binariesSetting the names of binaries
4149,158679
+@node Notes for syssiesNotes for syssies
4177,159619
+@node Bugs and EnhancementsBugs and Enhancements
4252,162655
+@node References4273,163470
+@node History of Proof GeneralHistory of Proof General
4313,164494
+@node Old News for 3.0Old News for 3.0
4404,168596
+@node Old News for 3.1Old News for 3.1
4474,172290
+@node Old News for 3.2Old News for 3.2
4500,173462
+@node Old News for 3.3Old News for 3.3
4561,176465
+@node Old News for 3.4Old News for 3.4
4580,177362
+@node Function IndexFunction Index
4603,178418
+@node Variable IndexVariable Index
4607,178494
+@node Keystroke IndexKeystroke Index
4611,178574
+@node Concept IndexConcept Index
4615,178640
 
 doc/PG-adapting.texi,3776
-@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
+@node Top157,4776
+@node Introduction195,5921
+@node Future236,7574
+@node Credits272,9170
+@node Beginning with a New ProverBeginning with a New Prover
282,9462
+@node Overview of adding a new proverOverview of adding a new prover
323,11411
+@node Demonstration instance and easy configurationDemonstration instance and easy configuration
401,14719
+@node Major modes used by Proof GeneralMajor modes used by Proof General
470,18110
+@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands
503,19461
+@node Settings for generic user-level commandsSettings for generic user-level commands
518,20007
+@node Menu configurationMenu configuration
563,21741
+@node Toolbar configurationToolbar configuration
587,22658
+@node Proof Script SettingsProof Script Settings
645,24900
+@node Recognizing commands and commentsRecognizing commands and comments
667,25480
+@node Recognizing proofsRecognizing proofs
788,30987
+@node Recognizing other elementsRecognizing other elements
900,35800
+@node Configuring undo behaviourConfiguring undo behaviour
1026,41311
+@node Nested proofsNested proofs
1163,46705
+@node Safe (state-preserving) commandsSafe (state-preserving) commands
1203,48331
+@node Activate scripting hookActivate scripting hook
1226,49277
+@node Automatic multiple filesAutomatic multiple files
1250,50140
+@node Completions1272,50987
+@node Proof Shell SettingsProof Shell Settings
1313,52476
+@node Proof shell commandsProof shell commands
1344,53758
+@node Script input to the shellScript input to the shell
1508,60697
+@node Settings for matching various output from proof processSettings for matching various output from proof process
1575,63737
+@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process
1706,69486
+@node Hooks and other settingsHooks and other settings
1921,79357
+@node Goals Buffer SettingsGoals Buffer Settings
2002,82726
+@node Splash Screen SettingsSplash Screen Settings
2079,85825
+@node Global ConstantsGlobal Constants
2105,86583
+@node Handling Multiple FilesHandling Multiple Files
2131,87424
+@node Configuring Editing SyntaxConfiguring Editing Syntax
2283,95207
+@node Configuring Font LockConfiguring Font Lock
2342,97328
+@node Configuring X-SymbolConfiguring X-Symbol
2429,101613
+@node Writing More Lisp CodeWriting More Lisp Code
2489,104133
+@node Default values for generic settingsDefault values for generic settings
2506,104778
+@node Adding prover-specific configurationsAdding prover-specific configurations
2536,105861
+@node Useful variablesUseful variables
2579,107143
+@node Useful functions and macrosUseful functions and macros
2594,107642
+@node Internals of Proof GeneralInternals of Proof General
2697,111597
+@node Spans2725,112505
+@node Proof General site configurationProof General site configuration
2738,112879
+@node Configuration variable mechanismsConfiguration variable mechanisms
2818,115925
+@node Global variablesGlobal variables
2939,121355
+@node Proof script modeProof script mode
3009,123903
+@node Proof shell modeProof shell mode
3268,135558
+@node Debugging3675,151640
+@node Plans and IdeasPlans and Ideas
3718,152516
+@node Proof by pointing and similar featuresProof by pointing and similar features
3739,153238
+@node Granularity of atomic command sequencesGranularity of atomic command sequences
3777,154896
+@node Browser mode for script files and theoriesBrowser mode for script files and theories
3822,157121
+@node Demonstration InstantiationsDemonstration Instantiations
3852,158152
+@node demoisa-easy.el3868,158583
+@node demoisa.el3931,160821
+@node Function IndexFunction Index
4086,165805
+@node Variable IndexVariable Index
4090,165881
+@node Concept IndexConcept Index
4099,166060
 
 x-symbol/lisp/_pkg.el,0
 
@@ -3687,32 +3684,20 @@ x-symbol/lisp/custom-load.el,0
 
 lib/holes-load.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
 
 lego/x-symbol-lego.el,0
 
-isar/test.el,0
-
-isar/isar-templates.el,0
-
 isar/isar-autotest.el,0
 
 isar/interface-setup.el,0
 
-isar/comptest.el,0
-
 hol98/x-symbol-hol98.el,0
 
 hol98/hol98.el,0