Updated

1 files changed, 2669 insertions, 2673 deletions

diff --git a/TAGS b/TAGS
index 0b4561f1..59ccefc1 100644
--- a/TAGS
+++ b/TAGS
@@ -1,6 +1,6 @@
 
 coq/coq-abbrev.el,495
-(defun holes-show-doc 10,310
+(defun holes-show-doc 10,309
 (defun coq-local-vars-list-show-doc 14,386
 (defconst coq-tactics-menu19,486
 (defconst coq-tactics-abbrev-table24,663
@@ -12,416 +12,415 @@ coq/coq-abbrev.el,495
 (defconst coq-terms-abbrev-table49,1430
 (defun coq-install-abbrevs 56,1624
 (defpgdefault menu-entries76,2361
-(defpgdefault help-menu-entries169,5947
-
-coq/coq-db.el,601
-(defconst coq-syntax-db 22,534
-(defvar coq-user-tactics-db58,1907
-(defun coq-insert-from-db 68,2256
-(defun coq-build-regexp-list-from-db 86,3037
-(defun max-length-db 108,4090
-(defun coq-build-menu-from-db-internal 120,4365
-(defun coq-build-title-menu 155,5988
-(defun coq-sort-menu-entries 164,6356
-(defun coq-build-menu-from-db 170,6486
-(defcustom coq-holes-minor-mode 192,7323
-(defun coq-build-abbrev-table-from-db 198,7467
-(defun filter-state-preserving 217,8105
-(defun filter-state-changing 222,8259
-(defface coq-solve-tactics-face 229,8480
-(defconst coq-solve-tactics-face 237,8737
-
-coq/coq.el,6556
-(defcustom coq-translate-to-v8 45,1301
-(defun coq-build-prog-args 51,1481
-(defcustom coq-compile-file-command 64,1861
-(defcustom coq-use-makefile 72,2180
-(defcustom coq-default-undo-limit 80,2403
-(defconst coq-shell-init-cmd 85,2531
-(defcustom coq-prog-env 97,2809
-(defconst coq-shell-restart-cmd 105,3061
-(defvar coq-shell-prompt-pattern 112,3321
-(defvar coq-shell-cd 122,3714
-(defvar coq-shell-abort-goal-regexp 126,3874
-(defvar coq-shell-proof-completed-regexp 129,4000
-(defvar coq-goal-regexp132,4152
-(defun coq-library-directory 139,4266
-(defcustom coq-tags 146,4446
-(defconst coq-interrupt-regexp 151,4596
-(defcustom coq-www-home-page 156,4717
-(defvar coq-outline-regexp166,4888
-(defvar coq-outline-heading-end-regexp 173,5102
-(defvar coq-shell-outline-regexp 175,5156
-(defvar coq-shell-outline-heading-end-regexp 176,5206
-(defconst coq-kill-goal-command 181,5316
-(defconst coq-forget-id-command 182,5359
-(defconst coq-back-n-command 183,5406
-(defconst coq-state-preserving-tactics-regexp 187,5550
-(defconst coq-state-changing-commands-regexp189,5651
-(defconst coq-state-preserving-commands-regexp 191,5758
-(defconst coq-commands-regexp 193,5870
-(defvar coq-retractable-instruct-regexp 195,5948
-(defvar coq-non-retractable-instruct-regexp 197,6039
-(defvar coq-keywords-section201,6179
-(defvar coq-section-regexp 204,6273
-(defun coq-set-undo-limit 241,7419
-(defconst coq-keywords-decl-defn-regexp252,7858
-(defun coq-proof-mode-p 256,8008
-(defun coq-is-comment-or-proverprocp 267,8416
-(defun coq-is-goalsave-p 269,8520
-(defun coq-is-module-equal-p 270,8595
-(defun coq-is-def-p 273,8791
-(defun coq-is-decl-defn-p 275,8899
-(defun coq-state-preserving-command-p 280,9066
-(defun coq-command-p 283,9200
-(defun coq-state-preserving-tactic-p 286,9300
-(defun coq-state-changing-tactic-p 291,9448
-(defun coq-state-changing-command-p 298,9682
-(defun coq-section-or-module-start-p 305,10028
-(defun build-list-id-from-string 314,10269
-(defun coq-last-prompt-info 327,10799
-(defun coq-last-prompt-info-safe 339,11340
-(defvar coq-last-but-one-statenum 345,11597
-(defvar coq-last-but-one-proofnum 351,11895
-(defvar coq-last-but-one-proofstack 354,11993
-(defun coq-get-span-statenum 357,12103
-(defun coq-get-span-proofnum 362,12218
-(defun coq-get-span-proofstack 367,12333
-(defun coq-set-span-statenum 372,12477
-(defun coq-get-span-goalcmd 377,12608
-(defun coq-set-span-goalcmd 382,12722
-(defun coq-set-span-proofnum 387,12852
-(defun coq-set-span-proofstack 392,12983
-(defun proof-last-locked-span 397,13143
-(defun coq-set-state-infos 412,13747
-(defun count-not-intersection 452,15826
-(defun  coq-find-and-forget-v81 483,17080
-(defun coq-find-and-forget-v80 511,18212
-(defun coq-find-and-forget 606,22911
-(defvar coq-current-goal 619,23451
-(defun coq-goal-hyp 622,23516
-(defun coq-state-preserving-p 635,23949
-(defconst notation-print-kinds-table 649,24454
-(defun coq-PrintScope 653,24622
-(defun coq-guess-or-ask-for-string 671,25177
-(defun coq-ask-do 685,25745
-(defun coq-SearchIsos 694,26133
-(defun coq-SearchConstant 700,26366
-(defun coq-SearchRewrite 704,26459
-(defun coq-SearchAbout 708,26557
-(defun coq-Print 712,26649
-(defun coq-About 716,26771
-(defun coq-LocateConstant 720,26888
-(defun coq-LocateLibrary 726,27023
-(defun coq-addquotes 732,27173
-(defun coq-LocateNotation 734,27221
-(defun coq-Pwd 741,27420
-(defun coq-Inspect 747,27552
-(defun coq-PrintSection(751,27652
-(defun coq-Print-implicit 755,27745
-(defun coq-Check 760,27896
-(defun coq-Show 765,28004
-(defun coq-Compile 779,28447
-(defun coq-guess-command-line 793,28767
-(defpacustom use-editing-holes 832,30474
-(defun coq-mode-config 842,30811
-(defvar coq-last-hybrid-pre-string 950,34765
-(defun coq-hybrid-ouput-goals-response-p 953,34944
-(defun coq-hybrid-ouput-goals-response 959,35203
-(defun coq-shell-mode-config 980,36165
-(defun coq-goals-mode-config 1025,38281
-(defun coq-response-config 1032,38525
-(defpacustom print-fully-explicit 1057,39350
-(defpacustom print-implicit 1062,39498
-(defpacustom print-coercions 1067,39664
-(defpacustom print-match-wildcards 1072,39808
-(defpacustom print-elim-types 1077,39988
-(defpacustom printing-depth 1082,40154
-(defpacustom undo-depth 1087,40315
-(defpacustom time-commands 1092,40462
-(defpacustom undo-limit 1096,40572
-(defpacustom auto-compile-vos 1101,40674
-(defun coq-maybe-compile-buffer 1130,41790
-(defun coq-ancestors-of 1167,43324
-(defun coq-all-ancestors-of 1190,44291
-(defconst coq-require-command-regexp 1202,44684
-(defun coq-process-require-command 1207,44893
-(defun coq-included-children 1212,45020
-(defun coq-process-file 1233,45859
-(defun coq-preprocessing 1248,46398
-(defun coq-fake-constant-markup 1263,46817
-(defun coq-create-span-menu 1284,47623
-(defconst module-kinds-table 1301,48122
-(defconst modtype-kinds-table1305,48272
-(defun coq-insert-section-or-module 1309,48401
-(defconst reqkinds-kinds-table1332,49261
-(defun coq-insert-requires 1337,49406
-(defun coq-end-Section 1353,49912
-(defun coq-insert-intros 1371,50496
-(defun coq-insert-infoH-hook 1384,51021
-(defun coq-insert-as 1388,51099
-(defun coq-insert-match 1409,51848
-(defun coq-insert-tactic 1441,53026
-(defun coq-insert-tactical 1447,53265
-(defun coq-insert-command 1453,53514
-(defun coq-insert-term 1459,53758
-(define-key coq-keymap 1465,53955
-(define-key coq-keymap 1466,54013
-(define-key coq-keymap 1467,54070
-(define-key coq-keymap 1468,54139
-(define-key coq-keymap 1469,54195
-(define-key coq-keymap 1470,54244
-(define-key coq-keymap 1471,54302
-(define-key coq-keymap 1473,54363
-(define-key coq-keymap 1474,54422
-(define-key coq-keymap 1476,54486
-(define-key coq-keymap 1477,54546
-(define-key coq-keymap 1479,54602
-(define-key coq-keymap 1480,54652
-(define-key coq-keymap 1481,54702
-(define-key coq-keymap 1482,54752
-(define-key coq-keymap 1483,54806
-(define-key coq-keymap 1484,54865
-(defvar last-coq-error-location 1492,54996
-(defun coq-get-last-error-location 1501,55395
-(defun coq-highlight-error 1548,57733
-(defvar coq-allow-highlight-error 1583,58952
-(defun coq-decide-highlight-error 1590,59279
-(defun coq-highlight-error-hook 1594,59401
-(defun first-word-of-buffer 1605,59794
-(defun coq-show-first-goal 1613,59997
-(defvar coq-modeline-string2 1630,60692
-(defvar coq-modeline-string1 1631,60736
-(defvar coq-modeline-string0 1632,60779
-(defun coq-build-subgoals-string 1633,60824
-(defun coq-update-minor-mode-alist 1638,60992
-(defun is-not-split-vertic 1664,62060
-(defun optim-resp-windows 1673,62499
+(defpgdefault help-menu-entries149,4975
+
+coq/coq-db.el,600
+(defconst coq-syntax-db 22,533
+(defvar coq-user-tactics-db58,1906
+(defun coq-insert-from-db 68,2255
+(defun coq-build-regexp-list-from-db 86,2987
+(defun max-length-db 108,3970
+(defun coq-build-menu-from-db-internal 120,4245
+(defun coq-build-title-menu 155,5868
+(defun coq-sort-menu-entries 164,6236
+(defun coq-build-menu-from-db 170,6363
+(defcustom coq-holes-minor-mode 192,7198
+(defun coq-build-abbrev-table-from-db 198,7342
+(defun filter-state-preserving 217,7980
+(defun filter-state-changing 222,8134
+(defface coq-solve-tactics-face229,8355
+(defconst coq-solve-tactics-face 237,8611
+
+coq/coq.el,6544
+(defcustom coq-translate-to-v8 45,1299
+(defun coq-build-prog-args 51,1479
+(defcustom coq-compile-file-command 64,1857
+(defcustom coq-use-makefile 72,2176
+(defcustom coq-default-undo-limit 80,2399
+(defconst coq-shell-init-cmd85,2527
+(defcustom coq-prog-env 97,2803
+(defconst coq-shell-restart-cmd 105,3053
+(defvar coq-shell-prompt-pattern112,3311
+(defvar coq-shell-cd 122,3702
+(defvar coq-shell-abort-goal-regexp 126,3862
+(defvar coq-shell-proof-completed-regexp 129,3988
+(defvar coq-goal-regexp132,4140
+(defun coq-library-directory 139,4254
+(defcustom coq-tags 146,4433
+(defconst coq-interrupt-regexp 151,4583
+(defcustom coq-www-home-page 156,4704
+(defvar coq-outline-regexp166,4875
+(defvar coq-outline-heading-end-regexp 173,5087
+(defvar coq-shell-outline-regexp 175,5141
+(defvar coq-shell-outline-heading-end-regexp 176,5191
+(defconst coq-kill-goal-command 181,5301
+(defconst coq-forget-id-command 182,5344
+(defconst coq-back-n-command 183,5391
+(defconst coq-state-preserving-tactics-regexp187,5535
+(defconst coq-state-changing-commands-regexp189,5635
+(defconst coq-state-preserving-commands-regexp191,5742
+(defconst coq-commands-regexp193,5853
+(defvar coq-retractable-instruct-regexp195,5930
+(defvar coq-non-retractable-instruct-regexp197,6020
+(defvar coq-keywords-section201,6159
+(defvar coq-section-regexp204,6253
+(defun coq-set-undo-limit 241,7394
+(defconst coq-keywords-decl-defn-regexp252,7832
+(defun coq-proof-mode-p 256,7982
+(defun coq-is-comment-or-proverprocp 267,8389
+(defun coq-is-goalsave-p 269,8492
+(defun coq-is-module-equal-p 270,8567
+(defun coq-is-def-p 273,8763
+(defun coq-is-decl-defn-p 275,8870
+(defun coq-state-preserving-command-p 280,9035
+(defun coq-command-p 283,9169
+(defun coq-state-preserving-tactic-p 286,9269
+(defun coq-state-changing-tactic-p 291,9415
+(defun coq-state-changing-command-p 298,9648
+(defun coq-section-or-module-start-p 305,9993
+(defun build-list-id-from-string 314,10231
+(defun coq-last-prompt-info 327,10761
+(defun coq-last-prompt-info-safe 339,11301
+(defvar coq-last-but-one-statenum 345,11558
+(defvar coq-last-but-one-proofnum 351,11855
+(defvar coq-last-but-one-proofstack 354,11953
+(defun coq-get-span-statenum 357,12063
+(defun coq-get-span-proofnum 362,12178
+(defun coq-get-span-proofstack 367,12293
+(defun coq-set-span-statenum 372,12437
+(defun coq-get-span-goalcmd 377,12568
+(defun coq-set-span-goalcmd 382,12682
+(defun coq-set-span-proofnum 387,12812
+(defun coq-set-span-proofstack 392,12943
+(defun proof-last-locked-span 397,13103
+(defun coq-set-state-infos 412,13706
+(defun count-not-intersection 452,15780
+(defun  coq-find-and-forget-v81 483,17030
+(defun coq-find-and-forget-v80 510,18182
+(defun coq-find-and-forget 605,22885
+(defvar coq-current-goal 618,23422
+(defun coq-goal-hyp 621,23487
+(defun coq-state-preserving-p 634,23919
+(defconst notation-print-kinds-table648,24420
+(defun coq-PrintScope 652,24587
+(defun coq-guess-or-ask-for-string 670,25136
+(defun coq-ask-do 684,25704
+(defun coq-SearchIsos 693,26089
+(defun coq-SearchConstant 699,26322
+(defun coq-SearchRewrite 703,26415
+(defun coq-SearchAbout 707,26513
+(defun coq-Print 711,26605
+(defun coq-About 715,26727
+(defun coq-LocateConstant 719,26844
+(defun coq-LocateLibrary 725,26979
+(defun coq-addquotes 731,27129
+(defun coq-LocateNotation 733,27177
+(defun coq-Pwd 740,27375
+(defun coq-Inspect 746,27507
+(defun coq-PrintSection(750,27607
+(defun coq-Print-implicit 754,27700
+(defun coq-Check 759,27851
+(defun coq-Show 764,27959
+(defun coq-Compile 778,28402
+(defun coq-guess-command-line 792,28722
+(defpacustom use-editing-holes 831,30428
+(defun coq-mode-config 841,30765
+(defvar coq-last-hybrid-pre-string 949,34712
+(defun coq-hybrid-ouput-goals-response-p 952,34891
+(defun coq-hybrid-ouput-goals-response 958,35141
+(defun coq-shell-mode-config 979,36100
+(defun coq-goals-mode-config 1026,38065
+(defun coq-response-config 1033,38309
+(defpacustom print-fully-explicit 1058,39134
+(defpacustom print-implicit 1063,39282
+(defpacustom print-coercions 1068,39448
+(defpacustom print-match-wildcards 1073,39592
+(defpacustom print-elim-types 1078,39772
+(defpacustom printing-depth 1083,39938
+(defpacustom undo-depth 1088,40099
+(defpacustom time-commands 1093,40246
+(defpacustom undo-limit 1097,40356
+(defpacustom auto-compile-vos 1102,40458
+(defun coq-maybe-compile-buffer 1131,41572
+(defun coq-ancestors-of 1168,43101
+(defun coq-all-ancestors-of 1191,44065
+(defconst coq-require-command-regexp1203,44458
+(defun coq-process-require-command 1208,44664
+(defun coq-included-children 1213,44791
+(defun coq-process-file 1234,45630
+(defun coq-preprocessing 1249,46169
+(defun coq-fake-constant-markup 1264,46582
+(defun coq-create-span-menu 1285,47386
+(defconst module-kinds-table1302,47883
+(defconst modtype-kinds-table1306,48032
+(defun coq-insert-section-or-module 1310,48161
+(defconst reqkinds-kinds-table1333,49019
+(defun coq-insert-requires 1338,49164
+(defun coq-end-Section 1354,49667
+(defun coq-insert-intros 1372,50245
+(defun coq-insert-infoH-hook 1385,50777
+(defun coq-insert-as 1389,50855
+(defun coq-insert-match 1410,51602
+(defun coq-insert-tactic 1442,52784
+(defun coq-insert-tactical 1448,53023
+(defun coq-insert-command 1454,53272
+(defun coq-insert-term 1460,53516
+(define-key coq-keymap 1466,53713
+(define-key coq-keymap 1467,53771
+(define-key coq-keymap 1468,53828
+(define-key coq-keymap 1469,53897
+(define-key coq-keymap 1470,53953
+(define-key coq-keymap 1471,54002
+(define-key coq-keymap 1472,54060
+(define-key coq-keymap 1474,54121
+(define-key coq-keymap 1475,54180
+(define-key coq-keymap 1477,54244
+(define-key coq-keymap 1478,54304
+(define-key coq-keymap 1480,54360
+(define-key coq-keymap 1481,54410
+(define-key coq-keymap 1482,54460
+(define-key coq-keymap 1483,54510
+(define-key coq-keymap 1484,54564
+(define-key coq-keymap 1485,54623
+(defvar last-coq-error-location 1493,54754
+(defun coq-get-last-error-location 1502,55153
+(defun coq-highlight-error 1549,57491
+(defvar coq-allow-highlight-error 1584,58710
+(defun coq-decide-highlight-error 1591,59037
+(defun coq-highlight-error-hook 1595,59159
+(defun first-word-of-buffer 1606,59552
+(defun coq-show-first-goal 1614,59755
+(defvar coq-modeline-string2 1631,60450
+(defvar coq-modeline-string1 1632,60494
+(defvar coq-modeline-string0 1633,60537
+(defun coq-build-subgoals-string 1634,60582
+(defun coq-update-minor-mode-alist 1639,60748
+(defun is-not-split-vertic 1665,61819
+(defun optim-resp-windows 1674,62258
 
 coq/coq-indent.el,2222
-(defconst coq-any-command-regexp17,315
-(defconst coq-indent-inner-regexp20,406
-(defconst coq-comment-start-regexp 31,794
-(defconst coq-comment-end-regexp 32,837
-(defconst coq-comment-start-or-end-regexp33,878
-(defconst coq-indent-open-regexp35,986
-(defconst coq-indent-close-regexp40,1160
-(defconst coq-indent-closepar-regexp 45,1341
-(defconst coq-indent-closematch-regexp 46,1386
-(defconst coq-indent-openpar-regexp 47,1457
-(defconst coq-indent-openmatch-regexp 48,1501
-(defconst coq-indent-any-regexp49,1581
-(defconst coq-indent-kw54,1859
-(defconst coq-indent-pattern-regexp 64,2313
-(defun coq-indent-goal-command-p 68,2416
-(defconst coq-end-command-regexp90,3471
-(defun coq-search-comment-delimiter-forward 95,3623
-(defun coq-search-comment-delimiter-backward 104,3953
-(defun coq-skip-until-one-comment-backward 111,4227
-(defun coq-skip-until-one-comment-forward 126,4934
-(defun coq-looking-at-comment 137,5452
-(defun coq-find-comment-start 141,5593
-(defun coq-find-comment-end 152,6026
-(defun coq-looking-at-syntactic-context 164,6519
-(defconst coq-end-command-or-comment-regexp170,6741
-(defconst coq-end-command-or-comment-start-regexp173,6850
-(defun coq-find-not-in-comment-backward 177,6968
-(defun coq-find-not-in-comment-forward 197,7869
-(defun coq-find-command-end-backward 221,9011
-(defun coq-find-command-end-forward 230,9402
-(defun coq-find-command-end 239,9779
-(defun coq-find-current-start 247,10111
-(defun coq-find-real-start 256,10402
-(defun coq-command-at-point 263,10621
-(defun coq-indent-only-spaces-on-line 270,10898
-(defun coq-indent-find-reg 276,11175
-(defun coq-find-no-syntactic-on-line 290,11711
-(defun coq-back-to-indentation-prevline 303,12184
-(defun coq-find-unclosed 347,14098
-(defun coq-find-at-same-level-zero 377,15399
-(defun coq-find-unopened 405,16564
-(defun coq-find-last-unopened 448,18014
-(defun coq-end-offset 459,18411
-(defun coq-indent-command-offset 484,19202
-(defun coq-indent-expr-offset 531,21026
-(defun coq-indent-comment-offset 647,25729
-(defun coq-indent-offset 679,27187
-(defun coq-indent-calculate 697,28050
-(defun coq-indent-line 700,28138
-(defun coq-indent-line-not-comments 710,28504
-(defun coq-indent-region 720,28893
+(defconst coq-any-command-regexp17,314
+(defconst coq-indent-inner-regexp20,405
+(defconst coq-comment-start-regexp 30,759
+(defconst coq-comment-end-regexp 31,802
+(defconst coq-comment-start-or-end-regexp32,843
+(defconst coq-indent-open-regexp34,951
+(defconst coq-indent-close-regexp39,1125
+(defconst coq-indent-closepar-regexp 44,1306
+(defconst coq-indent-closematch-regexp 45,1351
+(defconst coq-indent-openpar-regexp 46,1422
+(defconst coq-indent-openmatch-regexp 47,1466
+(defconst coq-indent-any-regexp48,1546
+(defconst coq-indent-kw53,1824
+(defconst coq-indent-pattern-regexp 63,2278
+(defun coq-indent-goal-command-p 67,2381
+(defconst coq-end-command-regexp89,3432
+(defun coq-search-comment-delimiter-forward 94,3584
+(defun coq-search-comment-delimiter-backward 103,3914
+(defun coq-skip-until-one-comment-backward 110,4188
+(defun coq-skip-until-one-comment-forward 125,4895
+(defun coq-looking-at-comment 136,5413
+(defun coq-find-comment-start 140,5554
+(defun coq-find-comment-end 151,5987
+(defun coq-looking-at-syntactic-context 163,6480
+(defconst coq-end-command-or-comment-regexp169,6702
+(defconst coq-end-command-or-comment-start-regexp172,6811
+(defun coq-find-not-in-comment-backward 176,6929
+(defun coq-find-not-in-comment-forward 196,7830
+(defun coq-find-command-end-backward 220,8969
+(defun coq-find-command-end-forward 229,9360
+(defun coq-find-command-end 238,9737
+(defun coq-find-current-start 246,10069
+(defun coq-find-real-start 255,10360
+(defun coq-command-at-point 262,10579
+(defun coq-indent-only-spaces-on-line 269,10856
+(defun coq-indent-find-reg 275,11133
+(defun coq-find-no-syntactic-on-line 289,11669
+(defun coq-back-to-indentation-prevline 302,12142
+(defun coq-find-unclosed 346,14050
+(defun coq-find-at-same-level-zero 376,15346
+(defun coq-find-unopened 404,16504
+(defun coq-find-last-unopened 447,17938
+(defun coq-end-offset 458,18335
+(defun coq-indent-command-offset 483,19105
+(defun coq-indent-expr-offset 530,20929
+(defun coq-indent-comment-offset 646,25612
+(defun coq-indent-offset 678,27061
+(defun coq-indent-calculate 696,27923
+(defun coq-indent-line 699,28011
+(defun coq-indent-line-not-comments 709,28377
+(defun coq-indent-region 719,28766
 
 coq/coq-local-vars.el,280
-(defconst coq-local-vars-doc 17,305
-(defun coq-insert-coq-prog-name 75,2833
-(defun coq-read-directory 86,3306
-(defun coq-extract-directories-from-args 110,4409
-(defun coq-ask-prog-args 125,4961
-(defun coq-ask-prog-name 147,6065
-(defun coq-ask-insert-coq-prog-name 165,6820
-
-coq/coq-syntax.el,2666
-(defcustom coq-prog-name 13,431
-(defvar coq-version-is-V8 34,1430
-(defvar coq-version-is-V8-0 36,1509
-(defvar coq-version-is-V8-1 43,1887
-(defun coq-determine-version 52,2320
-(defcustom coq-user-tactics-db 97,4178
-(defcustom coq-user-commands-db 114,4691
-(defcustom coq-user-tacticals-db 130,5210
-(defcustom coq-user-solve-tactics-db 146,5731
-(defcustom coq-user-reserved-db 164,6252
-(defvar coq-tactics-db182,6783
-(defvar coq-solve-tactics-db337,14851
-(defvar coq-tacticals-db361,15698
-(defvar coq-decl-db385,16585
-(defvar coq-defn-db407,17803
-(defvar coq-goal-starters-db460,21789
-(defvar coq-other-commands-db487,23344
-(defvar coq-commands-db611,32541
-(defvar coq-terms-db618,32767
-(defun coq-count-match 682,35419
-(defun coq-goal-command-str-v80-p 701,36282
-(defun coq-module-opening-p 724,37155
-(defun coq-section-command-p 735,37571
-(defun coq-goal-command-str-v81-p 739,37668
-(defun coq-goal-command-p-v81 754,38337
-(defun coq-goal-command-str-p 764,38677
-(defun coq-goal-command-p 774,39043
-(defvar coq-keywords-save-strict782,39355
-(defvar coq-keywords-save791,39468
-(defun coq-save-command-p 795,39546
-(defvar coq-keywords-kill-goal 804,39840
-(defvar coq-keywords-state-changing-misc-commands808,39931
-(defvar coq-keywords-goal811,40056
-(defvar coq-keywords-decl814,40139
-(defvar coq-keywords-defn817,40213
-(defvar coq-keywords-state-changing-commands821,40288
-(defvar coq-keywords-state-preserving-commands830,40549
-(defvar coq-keywords-commands835,40765
-(defvar coq-solve-tactics840,40914
-(defvar coq-tacticals844,41035
-(defvar coq-reserved850,41174
-(defvar coq-state-changing-tactics861,41503
-(defvar coq-state-preserving-tactics864,41612
-(defvar coq-tactics868,41726
-(defvar coq-retractable-instruct871,41815
-(defvar coq-non-retractable-instruct874,41925
-(defvar coq-keywords878,42053
-(defvar coq-symbols885,42221
-(defvar coq-error-regexp 904,42434
-(defvar coq-id 907,42662
-(defvar coq-id-shy 908,42687
-(defvar coq-ids 910,42741
-(defun coq-first-abstr-regexp 912,42782
-(defcustom coq-variable-highlight-enable 915,42878
-(defvar coq-font-lock-terms921,43005
-(defconst coq-save-command-regexp-strict942,44005
-(defconst coq-save-command-regexp946,44172
-(defconst coq-save-with-hole-regexp950,44325
-(defconst coq-goal-command-regexp954,44484
-(defconst coq-goal-with-hole-regexp957,44584
-(defconst coq-decl-with-hole-regexp961,44717
-(defconst coq-defn-with-hole-regexp968,44966
-(defconst coq-with-with-hole-regexp978,45255
-(defvar coq-font-lock-keywords-1984,45548
-(defvar coq-font-lock-keywords 1011,46878
-(defun coq-init-syntax-table 1013,46936
-(defconst coq-generic-expression1042,47835
-
-coq/coq-unicode-tokens.el,413
+(defconst coq-local-vars-doc 17,303
+(defun coq-insert-coq-prog-name 75,2831
+(defun coq-read-directory 86,3304
+(defun coq-extract-directories-from-args 110,4407
+(defun coq-ask-prog-args 125,4959
+(defun coq-ask-prog-name 147,6063
+(defun coq-ask-insert-coq-prog-name 165,6818
+
+coq/coq-syntax.el,2665
+(defcustom coq-prog-name 13,428
+(defvar coq-version-is-V8 34,1427
+(defvar coq-version-is-V8-0 36,1506
+(defvar coq-version-is-V8-1 43,1883
+(defun coq-determine-version 52,2315
+(defcustom coq-user-tactics-db 97,4172
+(defcustom coq-user-commands-db 114,4685
+(defcustom coq-user-tacticals-db 130,5204
+(defcustom coq-user-solve-tactics-db 146,5725
+(defcustom coq-user-reserved-db 164,6246
+(defvar coq-tactics-db182,6777
+(defvar coq-solve-tactics-db337,14844
+(defvar coq-tacticals-db361,15690
+(defvar coq-decl-db385,16576
+(defvar coq-defn-db407,17793
+(defvar coq-goal-starters-db460,21777
+(defvar coq-other-commands-db487,23332
+(defvar coq-commands-db611,32526
+(defvar coq-terms-db618,32746
+(defun coq-count-match 682,35395
+(defun coq-goal-command-str-v80-p 701,36257
+(defun coq-module-opening-p 724,37122
+(defun coq-section-command-p 735,37533
+(defun coq-goal-command-str-v81-p 739,37630
+(defun coq-goal-command-p-v81 754,38299
+(defun coq-goal-command-str-p 764,38637
+(defun coq-goal-command-p 774,39002
+(defvar coq-keywords-save-strict782,39313
+(defvar coq-keywords-save791,39426
+(defun coq-save-command-p 795,39504
+(defvar coq-keywords-kill-goal804,39798
+(defvar coq-keywords-state-changing-misc-commands808,39888
+(defvar coq-keywords-goal811,40013
+(defvar coq-keywords-decl814,40096
+(defvar coq-keywords-defn817,40170
+(defvar coq-keywords-state-changing-commands821,40245
+(defvar coq-keywords-state-preserving-commands830,40505
+(defvar coq-keywords-commands835,40721
+(defvar coq-solve-tactics840,40869
+(defvar coq-tacticals844,40990
+(defvar coq-reserved850,41129
+(defvar coq-state-changing-tactics861,41457
+(defvar coq-state-preserving-tactics864,41566
+(defvar coq-tactics868,41680
+(defvar coq-retractable-instruct871,41769
+(defvar coq-non-retractable-instruct874,41879
+(defvar coq-keywords878,42007
+(defvar coq-symbols885,42174
+(defvar coq-error-regexp 904,42387
+(defvar coq-id 907,42615
+(defvar coq-id-shy 908,42640
+(defvar coq-ids 910,42694
+(defun coq-first-abstr-regexp 912,42735
+(defcustom coq-variable-highlight-enable 915,42830
+(defvar coq-font-lock-terms921,42957
+(defconst coq-save-command-regexp-strict942,43956
+(defconst coq-save-command-regexp946,44122
+(defconst coq-save-with-hole-regexp950,44274
+(defconst coq-goal-command-regexp954,44432
+(defconst coq-goal-with-hole-regexp957,44532
+(defconst coq-decl-with-hole-regexp961,44664
+(defconst coq-defn-with-hole-regexp968,44912
+(defconst coq-with-with-hole-regexp978,45200
+(defvar coq-font-lock-keywords-1984,45492
+(defvar coq-font-lock-keywords 1011,46821
+(defun coq-init-syntax-table 1013,46879
+(defconst coq-generic-expression1042,47777
+
+coq/coq-unicode-tokens.el,410
 (defconst coq-token-format 18,631
 (defconst coq-token-match 19,664
 (defconst coq-hexcode-match 20,695
 (defcustom coq-token-symbol-map22,729
 (defcustom coq-shortcut-alist88,2382
-(defconst coq-control-char-format-regexp 177,4396
-(defconst coq-control-char-format 181,4522
-(defconst coq-control-characters 183,4565
-(defconst coq-control-region-format-regexp 187,4659
-(defconst coq-control-regions 189,4742
+(defconst coq-control-char-format-regexp177,4388
+(defconst coq-control-char-format 181,4513
+(defconst coq-control-characters183,4556
+(defconst coq-control-region-format-regexp 187,4648
+(defconst coq-control-regions189,4731
 
 demoisa/demoisa.el,349
-(defcustom isabelledemo-prog-name 54,1810
-(defcustom isabelledemo-web-page59,1932
-(defun demoisa-config 70,2162
-(defun demoisa-shell-config 91,2954
-(define-derived-mode demoisa-mode 117,3931
-(define-derived-mode demoisa-shell-mode 122,4054
-(define-derived-mode demoisa-response-mode 127,4197
-(define-derived-mode demoisa-goals-mode 131,4324
-
-isar/isabelle-system.el,1347
-(defgroup isabelle 26,782
-(defcustom isabelle-web-page30,910
-(defcustom isa-isabelle-command39,1127
-(defvar isabelle-not-found 57,1810
-(defun isa-set-isabelle-command 60,1925
-(defun isa-shell-command-to-string 83,2933
-(defun isa-getenv 89,3157
-(defcustom isabelle-program-name-override 109,3849
-(defvar isabelle-prog-name 120,4195
-(defun isa-tool-list-logics 123,4305
-(defcustom isabelle-logics-available 130,4544
-(defcustom isabelle-chosen-logic 140,4881
-(defvar isabelle-chosen-logic-prev 156,5465
-(defun isabelle-hack-local-variables-function 159,5587
-(defun isabelle-set-prog-name 171,6028
-(defun isabelle-choose-logic 196,7220
-(defun isa-view-doc 215,7982
-(defun isa-tool-list-docs 224,8248
-(defconst isabelle-verbatim-regexp 242,8971
-(defun isabelle-verbatim 245,9113
-(defcustom isabelle-refresh-logics 252,9274
-(defvar isabelle-docs-menu 260,9602
-(defvar isabelle-logics-menu-entries 267,9888
-(defun isabelle-logics-menu-calculate 270,9961
-(defvar isabelle-time-to-refresh-logics 291,10603
-(defun isabelle-logics-menu-refresh 295,10698
-(defun isabelle-menu-bar-update-logics 310,11331
-(defun isabelle-load-isar-keywords 326,11961
-(defun isabelle-convert-idmarkup-to-subterm 347,12677
-(defun isabelle-create-span-menu 371,13688
-(defun isabelle-xml-sml-escapes 387,14130
-(defun isabelle-process-pgip 390,14231
-
-isar/isar.el,1523
-(defcustom isar-keywords-name 33,765
-(defpgdefault completion-table 50,1288
-(defcustom isar-web-page52,1341
-(defun isar-strip-terminators 66,1691
-(defun isar-markup-ml 79,2068
-(defun isar-mode-config-set-variables 84,2203
-(defun isar-shell-mode-config-set-variables 157,5307
-(defun isar-configure-from-settings 242,8678
-(defpacustom use-find-theorems-form 245,8760
-(defun isar-set-proof-find-theorems-command 250,8926
-(defun isar-remove-file 260,9148
-(defun isar-shell-compute-new-files-list 270,9545
-(define-derived-mode isar-shell-mode 288,10131
-(define-derived-mode isar-response-mode 293,10254
-(define-derived-mode isar-goals-mode 298,10382
-(define-derived-mode isar-mode 303,10503
-(defpgdefault menu-entries360,12525
-(defalias 'isar-set-command isar-set-command
390,13808
-(defpgdefault help-menu-entries 392,13864
-(defun isar-count-undos 395,13940
-(defun isar-find-and-forget 422,15054
-(defun isar-goal-command-p 461,16634
-(defun isar-global-save-command-p 466,16811
-(defvar isar-current-goal 487,17672
-(defun isar-state-preserving-p 490,17738
-(defvar isar-shell-current-line-width 515,18935
-(defun isar-shell-adjust-line-width 520,19127
-(defconst isar-nonwrap-regexp545,20024
-(defun isar-string-wrapping 550,20209
-(defun isar-positions-of 559,20406
-(defun isar-command-wrapping 583,21149
-(defun isar-preprocessing 592,21465
-(defun isar-mode-config 610,22015
-(defun isar-shell-mode-config 621,22573
-(defun isar-response-mode-config 627,22770
-(defun isar-goals-mode-config 637,23105
+(defcustom isabelledemo-prog-name 54,1805
+(defcustom isabelledemo-web-page59,1927
+(defun demoisa-config 70,2157
+(defun demoisa-shell-config 91,2949
+(define-derived-mode demoisa-mode 116,3878
+(define-derived-mode demoisa-shell-mode 121,4001
+(define-derived-mode demoisa-response-mode 126,4144
+(define-derived-mode demoisa-goals-mode 130,4271
+
+isar/isabelle-system.el,1291
+(defgroup isabelle 26,776
+(defcustom isabelle-web-page30,904
+(defcustom isa-isabelle-command39,1121
+(defvar isabelle-not-found 57,1803
+(defun isa-set-isabelle-command 60,1918
+(defun isa-shell-command-to-string 83,2936
+(defun isa-getenv 89,3160
+(defcustom isabelle-program-name-override 109,3852
+(defvar isabelle-prog-name 120,4198
+(defun isa-tool-list-logics 123,4308
+(defcustom isabelle-logics-available 130,4547
+(defcustom isabelle-chosen-logic 140,4884
+(defvar isabelle-chosen-logic-prev 156,5468
+(defun isabelle-hack-local-variables-function 159,5588
+(defun isabelle-set-prog-name 171,6027
+(defun isabelle-choose-logic 196,7217
+(defun isa-view-doc 215,7979
+(defun isa-tool-list-docs 224,8244
+(defconst isabelle-verbatim-regexp 242,8967
+(defun isabelle-verbatim 245,9109
+(defcustom isabelle-refresh-logics 252,9270
+(defvar isabelle-docs-menu260,9598
+(defvar isabelle-logics-menu-entries 267,9883
+(defun isabelle-logics-menu-calculate 270,9956
+(defvar isabelle-time-to-refresh-logics 291,10598
+(defun isabelle-logics-menu-refresh 295,10693
+(defun isabelle-menu-bar-update-logics 310,11326
+(defun isabelle-load-isar-keywords 326,11955
+(defun isabelle-create-span-menu 347,12683
+(defun isabelle-xml-sml-escapes 363,13125
+(defun isabelle-process-pgip 366,13226
+
+isar/isar.el,1530
+(defcustom isar-keywords-name 33,762
+(defpgdefault completion-table 50,1285
+(defcustom isar-web-page52,1338
+(defun isar-strip-terminators 66,1688
+(defun isar-markup-ml 79,2065
+(defun isar-mode-config-set-variables 84,2200
+(defun isar-shell-mode-config-set-variables 157,5304
+(defun isar-configure-from-settings 239,8493
+(defpacustom use-find-theorems-form 242,8575
+(defun isar-set-proof-find-theorems-command 247,8741
+(defun isar-remove-file 257,8963
+(defun isar-shell-compute-new-files-list 267,9318
+(define-derived-mode isar-shell-mode 285,9890
+(define-derived-mode isar-response-mode 290,10013
+(define-derived-mode isar-goals-mode 295,10141
+(define-derived-mode isar-mode 300,10262
+(defpgdefault menu-entries357,12284
+(defalias 'isar-set-command isar-set-command
387,13441
+(defpgdefault help-menu-entries 389,13497
+(defun isar-count-undos 392,13573
+(defun isar-find-and-forget 418,14508
+(defun isar-goal-command-p 458,16035
+(defun isar-global-save-command-p 463,16212
+(defvar isar-current-goal 484,16996
+(defun isar-state-preserving-p 487,17062
+(defvar isar-shell-current-line-width 512,18259
+(defun isar-shell-adjust-line-width 517,18451
+(defun isar-string-wrapping 542,19250
+(defun isar-positions-of 551,19447
+(defun isar-command-wrapping 575,20151
+(defcustom isar-wrap-commands-singly 584,20495
+(defun isar-preprocessing 590,20691
+(defun isar-mode-config 610,21345
+(defun isar-shell-mode-config 621,21903
+(defun isar-response-mode-config 627,22100
+(defun isar-goals-mode-config 637,22435
 
 isar/isar-find-theorems.el,778
 (defun isar-find-theorems-minibuffer 18,713
@@ -435,1623 +434,1630 @@ isar/isar-find-theorems.el,778
 (defvar isar-find-theorems-widget-name 103,3911
 (defvar isar-find-theorems-widget-simp 106,3998
 (defun isar-find-theorems-create-searchform111,4144
-(defun isar-find-theorems-create-help 251,8759
-(defun isar-find-theorems-submit-searchform294,10931
-(defun isar-find-theorems-parse-criteria 372,13308
-(defun isar-find-theorems-parse-number 465,16408
-(defun isar-find-theorems-filter-empty 475,16685
+(defun isar-find-theorems-create-help 251,8687
+(defun isar-find-theorems-submit-searchform294,10859
+(defun isar-find-theorems-parse-criteria 372,13229
+(defun isar-find-theorems-parse-number 465,16210
+(defun isar-find-theorems-filter-empty 475,16487
 
 isar/isar-keywords.el,1052
-(defconst isar-keywords-major13,482
-(defconst isar-keywords-minor206,3642
-(defconst isar-keywords-control262,4396
-(defconst isar-keywords-diag282,4873
-(defconst isar-keywords-theory-begin338,5832
-(defconst isar-keywords-theory-switch341,5885
-(defconst isar-keywords-theory-end344,5940
-(defconst isar-keywords-theory-heading347,5988
-(defconst isar-keywords-theory-decl353,6095
-(defconst isar-keywords-theory-script412,7076
-(defconst isar-keywords-theory-goal416,7153
-(defconst isar-keywords-qed429,7370
-(defconst isar-keywords-qed-block436,7456
-(defconst isar-keywords-qed-global439,7503
-(defconst isar-keywords-proof-heading442,7552
-(defconst isar-keywords-proof-goal447,7635
-(defconst isar-keywords-proof-block454,7734
-(defconst isar-keywords-proof-open458,7796
-(defconst isar-keywords-proof-close461,7842
-(defconst isar-keywords-proof-chain464,7889
-(defconst isar-keywords-proof-decl471,7992
-(defconst isar-keywords-proof-asm480,8113
-(defconst isar-keywords-proof-asm-goal487,8208
-(defconst isar-keywords-proof-script490,8263
-
-isar/isar-mmm.el,83
-(defconst isar-start-latex-regexp 23,698
-(defconst isar-start-sml-regexp 35,1131
-
-isar/isar-syntax.el,3656
+(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,81
+(defconst isar-start-latex-regexp24,744
+(defconst isar-start-sml-regexp36,1172
+
+isar/isar-syntax.el,3653
 (defconst isar-script-syntax-table-entries18,424
 (defconst isar-script-syntax-table-alist42,826
-(defun isar-init-syntax-table 51,1116
-(defun isar-init-output-syntax-table 59,1363
-(defconst isar-keyword-begin 75,1810
-(defconst isar-keyword-end 76,1848
-(defconst isar-keywords-theory-enclose78,1883
-(defconst isar-keywords-theory83,2028
-(defconst isar-keywords-save88,2173
-(defconst isar-keywords-proof-enclose93,2302
-(defconst isar-keywords-proof99,2484
-(defconst isar-keywords-proof-context106,2689
-(defconst isar-keywords-local-goal110,2803
-(defconst isar-keywords-proper114,2915
-(defconst isar-keywords-improper119,3048
-(defconst isar-keywords-outline124,3194
-(defconst isar-keywords-fume127,3259
-(defconst isar-keywords-indent-open134,3477
-(defconst isar-keywords-indent-close140,3661
-(defconst isar-keywords-indent-enclose144,3766
-(defun isar-regexp-simple-alt 153,3981
-(defun isar-ids-to-regexp 173,4741
-(defconst isar-ext-first 207,6147
-(defconst isar-ext-rest 208,6214
-(defconst isar-long-id-stuff 210,6286
-(defconst isar-id 211,6360
-(defconst isar-idx 212,6430
-(defconst isar-string 214,6489
-(defconst isar-any-command-regexp216,6549
-(defconst isar-name-regexp220,6683
-(defconst isar-improper-regexp226,6978
-(defconst isar-save-command-regexp230,7126
-(defconst isar-global-save-command-regexp233,7227
-(defconst isar-goal-command-regexp236,7341
-(defconst isar-local-goal-command-regexp239,7449
-(defconst isar-comment-start 242,7562
-(defconst isar-comment-end 243,7597
-(defconst isar-comment-start-regexp 244,7630
-(defconst isar-comment-end-regexp 245,7701
-(defconst isar-string-start-regexp 247,7769
-(defconst isar-string-end-regexp 248,7821
-(defun isar-syntactic-context 250,7872
-(defconst isar-antiq-regexp 265,8270
-(defconst isar-nesting-regexp271,8423
-(defun isar-nesting 274,8521
-(defun isar-match-nesting 286,8942
-(defface isabelle-class-name-face298,9273
-(defface isabelle-tfree-name-face306,9456
-(defface isabelle-tvar-name-face314,9645
-(defface isabelle-free-name-face322,9833
-(defface isabelle-bound-name-face330,10017
-(defface isabelle-var-name-face338,10204
-(defconst isabelle-class-name-face 346,10391
-(defconst isabelle-tfree-name-face 347,10453
-(defconst isabelle-tvar-name-face 348,10515
-(defconst isabelle-free-name-face 349,10576
-(defconst isabelle-bound-name-face 350,10637
-(defconst isabelle-var-name-face 351,10699
-(defvar isar-font-lock-keywords-1354,10761
-(defun isar-output-flkprops 372,11771
-(defun isar-output-flk 378,12023
-(defvar isar-output-font-lock-keywords-1381,12132
-(defun isar-strip-output-markup 417,13569
-(defvar isar-goals-font-lock-keywords421,13705
-(defconst isar-linear-undo 455,14384
-(defconst isar-undo 457,14427
-(defun isar-remove 459,14470
-(defun isar-undos 462,14545
-(defun isar-cannot-undo 466,14651
-(defconst isar-undo-commands469,14721
-(defconst isar-theory-start-regexp477,14860
-(defconst isar-end-regexp483,15025
-(defconst isar-undo-fail-regexp487,15126
-(defconst isar-undo-skip-regexp491,15230
-(defconst isar-undo-ignore-regexp494,15351
-(defconst isar-undo-remove-regexp497,15416
-(defconst isar-any-entity-regexp505,15591
-(defconst isar-named-entity-regexp510,15778
-(defconst isar-unnamed-entity-regexp515,15955
-(defconst isar-next-entity-regexps518,16057
-(defconst isar-generic-expression526,16368
-(defconst isar-indent-any-regexp537,16685
-(defconst isar-indent-inner-regexp539,16778
-(defconst isar-indent-enclose-regexp541,16844
-(defconst isar-indent-open-regexp543,16960
-(defconst isar-indent-close-regexp545,17070
-(defconst isar-outline-regexp551,17207
-(defconst isar-outline-heading-end-regexp 555,17360
-
-isar/isar-unicode-tokens.el,1188
+(defun isar-init-syntax-table 51,1109
+(defun isar-init-output-syntax-table 59,1356
+(defconst isar-keyword-begin 75,1803
+(defconst isar-keyword-end 76,1841
+(defconst isar-keywords-theory-enclose78,1876
+(defconst isar-keywords-theory83,2014
+(defconst isar-keywords-save88,2145
+(defconst isar-keywords-proof-enclose93,2260
+(defconst isar-keywords-proof99,2421
+(defconst isar-keywords-proof-context106,2598
+(defconst isar-keywords-local-goal110,2705
+(defconst isar-keywords-proper114,2810
+(defconst isar-keywords-improper119,2929
+(defconst isar-keywords-outline124,3061
+(defconst isar-keywords-fume127,3126
+(defconst isar-keywords-indent-open134,3316
+(defconst isar-keywords-indent-close140,3479
+(defconst isar-keywords-indent-enclose144,3577
+(defun isar-regexp-simple-alt 153,3771
+(defun isar-ids-to-regexp 173,4531
+(defconst isar-ext-first 207,5916
+(defconst isar-ext-rest 208,5983
+(defconst isar-long-id-stuff 210,6055
+(defconst isar-id 211,6129
+(defconst isar-idx 212,6199
+(defconst isar-string 214,6258
+(defconst isar-any-command-regexp216,6318
+(defconst isar-name-regexp220,6452
+(defconst isar-improper-regexp226,6747
+(defconst isar-save-command-regexp230,6895
+(defconst isar-global-save-command-regexp233,6996
+(defconst isar-goal-command-regexp236,7110
+(defconst isar-local-goal-command-regexp239,7218
+(defconst isar-comment-start 242,7331
+(defconst isar-comment-end 243,7366
+(defconst isar-comment-start-regexp 244,7399
+(defconst isar-comment-end-regexp 245,7470
+(defconst isar-string-start-regexp 247,7538
+(defconst isar-string-end-regexp 248,7590
+(defun isar-syntactic-context 250,7641
+(defconst isar-antiq-regexp265,8036
+(defconst isar-nesting-regexp271,8187
+(defun isar-nesting 274,8285
+(defun isar-match-nesting 286,8678
+(defface isabelle-class-name-face298,9009
+(defface isabelle-tfree-name-face306,9192
+(defface isabelle-tvar-name-face314,9381
+(defface isabelle-free-name-face322,9569
+(defface isabelle-bound-name-face330,9753
+(defface isabelle-var-name-face338,9940
+(defconst isabelle-class-name-face 346,10127
+(defconst isabelle-tfree-name-face 347,10189
+(defconst isabelle-tvar-name-face 348,10251
+(defconst isabelle-free-name-face 349,10312
+(defconst isabelle-bound-name-face 350,10373
+(defconst isabelle-var-name-face 351,10435
+(defvar isar-font-lock-keywords-1354,10497
+(defun isar-output-flkprops 372,11505
+(defun isar-output-flk 378,11757
+(defvar isar-output-font-lock-keywords-1381,11866
+(defun isar-strip-output-markup 417,13289
+(defvar isar-goals-font-lock-keywords421,13425
+(defconst isar-linear-undo 455,14104
+(defconst isar-undo 457,14147
+(defun isar-remove 459,14190
+(defun isar-undos 462,14265
+(defun isar-cannot-undo 466,14382
+(defconst isar-undo-commands469,14452
+(defconst isar-theory-start-regexp477,14589
+(defconst isar-end-regexp483,14747
+(defconst isar-undo-fail-regexp487,14848
+(defconst isar-undo-skip-regexp491,14952
+(defconst isar-undo-ignore-regexp494,15073
+(defconst isar-undo-remove-regexp497,15138
+(defconst isar-any-entity-regexp505,15313
+(defconst isar-named-entity-regexp510,15486
+(defconst isar-unnamed-entity-regexp515,15649
+(defconst isar-next-entity-regexps518,15751
+(defconst isar-generic-expression526,16055
+(defconst isar-indent-any-regexp537,16288
+(defconst isar-indent-inner-regexp539,16381
+(defconst isar-indent-enclose-regexp541,16447
+(defconst isar-indent-open-regexp543,16563
+(defconst isar-indent-close-regexp545,16673
+(defconst isar-outline-regexp551,16810
+(defconst isar-outline-heading-end-regexp 555,16963
+
+isar/isar-unicode-tokens.el,1289
 (defgroup isabelle-tokens 20,510
 (defun isar-set-and-restart-tokens 25,650
 (defconst isar-control-region-format-regexp38,1003
-(defconst isar-control-char-format-regexp 41,1097
-(defconst isar-control-char-format	44,1193
-(defconst isar-control-region-format-start 45,1242
-(defconst isar-control-region-format-end 46,1296
-(defcustom isar-control-characters49,1352
-(defcustom isar-control-regions62,1727
-(defconst isar-token-format 86,2448
-(defconst isar-token-variant-format-regexp 90,2600
-(defcustom isar-greek-letters-tokens93,2715
-(defcustom isar-misc-letters-tokens133,3556
-(defcustom isar-symbols-tokens145,3860
-(defun isar-try-char 419,10132
-(defcustom isar-symbols-tokens-fallbacks423,10276
-(defcustom isar-bold-nums-tokens 450,11209
-(defun isar-map-letters 466,11599
-(defconst isar-script-letters-tokens472,11748
-(defconst isar-roman-letters-tokens477,11886
-(defconst isar-fraktur-letters-tokens482,12022
-(defcustom isar-token-symbol-map 487,12164
-(defcustom isar-user-tokens 503,12629
-(defun isar-init-token-symbol-map 509,12841
-(defcustom isar-symbol-shortcuts529,13298
-(defcustom isar-shortcut-alist 600,15435
-(defun isar-init-shortcut-alists 608,15694
+(defconst isar-control-char-format-regexp41,1097
+(defconst isar-control-char-format	44,1192
+(defconst isar-control-region-format-start 45,1241
+(defconst isar-control-region-format-end 46,1295
+(defcustom isar-control-characters49,1351
+(defcustom isar-control-regions62,1723
+(defconst isar-token-format 86,2439
+(defconst isar-token-variant-format-regexp90,2590
+(defcustom isar-greek-letters-tokens93,2704
+(defcustom isar-misc-letters-tokens133,3562
+(defcustom isar-symbols-tokens145,3880
+(defcustom isar-extended-symbols-tokens351,8702
+(defun isar-try-char 420,10357
+(defcustom isar-symbols-tokens-fallbacks424,10501
+(defcustom isar-bold-nums-tokens451,11431
+(defun isar-map-letters 467,11820
+(defconst isar-script-letters-tokens473,11968
+(defconst isar-roman-letters-tokens478,12106
+(defconst isar-fraktur-letters-tokens483,12242
+(defcustom isar-token-symbol-map 488,12384
+(defcustom isar-user-tokens 504,12853
+(defun isar-init-token-symbol-map 511,13090
+(defcustom isar-symbol-shortcuts534,13645
+(defcustom isar-shortcut-alist 607,15871
+(defun isar-init-shortcut-alists 615,16130
+(defconst isar-tokens-customizable-variables636,16760
 
 lclam/lclam.el,524
-(defcustom lclam-prog-name 15,386
-(defcustom lclam-web-page21,534
-(defun lclam-config 32,764
-(defun lclam-shell-config 54,1558
-(define-derived-mode lclam-proofscript-mode 74,2217
-(define-derived-mode lclam-shell-mode 79,2340
-(define-derived-mode lclam-response-mode 84,2474
-(define-derived-mode lclam-goals-mode 88,2597
-(defun lclam-mode 96,2825
-(define-derived-mode thy-mode 133,3671
-(defvar thy-mode-map 136,3769
-(defun thy-add-menus 138,3796
-(defun process-thy-file 177,5682
-(defun update-thy-only 183,5883
-
-lego/lego.el,1727
-(defcustom lego-tags 19,494
-(defcustom lego-test-all-name 24,630
-(defpgdefault help-menu-entries30,788
-(defpgdefault menu-entries34,948
-(defvar lego-shell-process-output45,1250
-(defconst lego-process-config53,1573
-(defconst lego-pretty-set-width 64,2004
-(defconst lego-interrupt-regexp 68,2147
-(defcustom lego-www-home-page 73,2264
-(defcustom lego-www-latest-release78,2388
-(defcustom lego-www-refcard84,2566
-(defcustom lego-library-www-page90,2715
-(defvar lego-prog-name 99,2931
-(defvar lego-shell-prompt-pattern 102,3000
-(defvar lego-shell-cd 105,3121
-(defvar lego-shell-abort-goal-regexp 108,3221
-(defvar lego-shell-proof-completed-regexp 113,3413
-(defvar lego-save-command-regexp116,3553
-(defvar lego-goal-command-regexp118,3643
-(defvar lego-kill-goal-command 121,3734
-(defvar lego-forget-id-command 122,3777
-(defvar lego-undoable-commands-regexp124,3823
-(defvar lego-goal-regexp 133,4197
-(defvar lego-outline-regexp135,4242
-(defvar lego-outline-heading-end-regexp 141,4418
-(defvar lego-shell-outline-regexp 143,4471
-(defvar lego-shell-outline-heading-end-regexp 144,4523
-(define-derived-mode lego-shell-mode 150,4802
-(define-derived-mode lego-mode 157,4963
-(define-derived-mode lego-goals-mode 168,5260
-(defun lego-count-undos 179,5686
-(defun lego-goal-command-p 199,6505
-(defun lego-find-and-forget 204,6676
-(defun lego-goal-hyp 246,8512
-(defun lego-state-preserving-p 255,8710
-(defvar lego-shell-current-line-width 271,9413
-(defun lego-shell-adjust-line-width 279,9720
-(defun lego-mode-config 298,10459
-(defun lego-equal-module-filename 366,12520
-(defun lego-shell-compute-new-files-list 372,12795
-(defun lego-shell-mode-config 386,13321
-(defun lego-goals-mode-config 435,15257
+(defcustom lclam-prog-name 15,373
+(defcustom lclam-web-page21,521
+(defun lclam-config 32,751
+(defun lclam-shell-config 54,1542
+(define-derived-mode lclam-proofscript-mode 73,2157
+(define-derived-mode lclam-shell-mode 78,2280
+(define-derived-mode lclam-response-mode 83,2414
+(define-derived-mode lclam-goals-mode 87,2537
+(defun lclam-mode 95,2765
+(define-derived-mode thy-mode 132,3611
+(defvar thy-mode-map 135,3709
+(defun thy-add-menus 137,3736
+(defun process-thy-file 176,5217
+(defun update-thy-only 182,5418
+
+lego/lego.el,1683
+(defcustom lego-tags 21,534
+(defcustom lego-test-all-name 26,670
+(defpgdefault help-menu-entries32,828
+(defpgdefault menu-entries36,988
+(defvar lego-shell-process-output47,1289
+(defconst lego-process-config55,1612
+(defconst lego-pretty-set-width 66,2043
+(defconst lego-interrupt-regexp 70,2185
+(defcustom lego-www-home-page 75,2302
+(defcustom lego-www-latest-release80,2426
+(defcustom lego-www-refcard86,2601
+(defcustom lego-library-www-page92,2750
+(defvar lego-prog-name 101,2966
+(defvar lego-shell-cd 104,3035
+(defvar lego-shell-abort-goal-regexp107,3134
+(defvar lego-shell-proof-completed-regexp 112,3325
+(defvar lego-save-command-regexp115,3465
+(defvar lego-goal-command-regexp117,3555
+(defvar lego-kill-goal-command 120,3646
+(defvar lego-forget-id-command 121,3689
+(defvar lego-undoable-commands-regexp123,3735
+(defvar lego-goal-regexp 132,4109
+(defvar lego-outline-regexp134,4154
+(defvar lego-outline-heading-end-regexp 140,4329
+(defvar lego-shell-outline-regexp 142,4382
+(defvar lego-shell-outline-heading-end-regexp 143,4434
+(define-derived-mode lego-shell-mode 149,4713
+(define-derived-mode lego-mode 156,4874
+(define-derived-mode lego-goals-mode 167,5169
+(defun lego-count-undos 178,5595
+(defun lego-goal-command-p 198,6413
+(defun lego-find-and-forget 203,6584
+(defun lego-goal-hyp 245,8400
+(defun lego-state-preserving-p 254,8597
+(defvar lego-shell-current-line-width 270,9300
+(defun lego-shell-adjust-line-width 278,9607
+(defun lego-mode-config 297,10344
+(defun lego-equal-module-filename 365,12393
+(defun lego-shell-compute-new-files-list 371,12668
+(defun lego-shell-mode-config 381,13051
+(defun lego-goals-mode-config 428,14766
 
 lego/lego-syntax.el,600
-(defconst lego-keywords-goal 15,359
-(defconst lego-keywords-save 17,402
-(defconst lego-commands19,473
-(defconst lego-keywords31,1033
-(defconst lego-tacticals 36,1210
-(defconst lego-error-regexp 39,1318
-(defvar lego-id 42,1477
-(defvar lego-ids 44,1504
-(defconst lego-arg-list-regexp 48,1700
-(defun lego-decl-defn-regexp 51,1816
-(defconst lego-definiendum-alternative-regexp59,2188
-(defvar lego-font-lock-terms63,2372
-(defconst lego-goal-with-hole-regexp89,3228
-(defconst lego-save-with-hole-regexp94,3451
-(defvar lego-font-lock-keywords-199,3668
-(defun lego-init-syntax-table 110,4135
-
-phox/phox.el,602
-(defcustom phox-prog-name 31,917
-(defcustom phox-sym-lock-enabled 36,1019
-(defcustom phox-web-page42,1128
-(defcustom phox-doc-dir 48,1278
-(defcustom phox-lib-dir 54,1426
-(defcustom phox-tags-program 60,1570
-(defcustom phox-tags-doc 66,1750
-(defcustom phox-etags 72,1888
-(defpgdefault menu-entries93,2340
-(defun phox-config 107,2533
-(defun phox-shell-config 148,4424
-(define-derived-mode phox-mode 173,5353
-(define-derived-mode phox-shell-mode 189,5819
-(define-derived-mode phox-response-mode 194,5947
-(define-derived-mode phox-goals-mode 207,6389
-(defpgdefault completion-table233,7273
+(defconst lego-keywords-goal 15,358
+(defconst lego-keywords-save 17,401
+(defconst lego-commands19,472
+(defconst lego-keywords31,1030
+(defconst lego-tacticals 36,1207
+(defconst lego-error-regexp 39,1315
+(defvar lego-id 42,1473
+(defvar lego-ids 44,1500
+(defconst lego-arg-list-regexp 48,1696
+(defun lego-decl-defn-regexp 51,1812
+(defconst lego-definiendum-alternative-regexp59,2184
+(defvar lego-font-lock-terms63,2368
+(defconst lego-goal-with-hole-regexp89,3221
+(defconst lego-save-with-hole-regexp94,3443
+(defvar lego-font-lock-keywords-199,3660
+(defun lego-init-syntax-table 110,4122
+
+phox/phox.el,597
+(defcustom phox-prog-name 31,915
+(defcustom phox-sym-lock-enabled 36,1017
+(defcustom phox-web-page42,1126
+(defcustom phox-doc-dir48,1276
+(defcustom phox-lib-dir54,1423
+(defcustom phox-tags-program60,1566
+(defcustom phox-tags-doc66,1745
+(defcustom phox-etags72,1882
+(defpgdefault menu-entries93,2332
+(defun phox-config 107,2525
+(defun phox-shell-config 151,4449
+(define-derived-mode phox-mode 175,5311
+(define-derived-mode phox-shell-mode 191,5774
+(define-derived-mode phox-response-mode 196,5902
+(define-derived-mode phox-goals-mode 206,6263
+(defpgdefault completion-table229,7049
 
 phox/phox-extraction.el,382
-(defvar phox-prog-orig 11,481
-(defun phox-prog-flags-modify(13,549
-(defun phox-prog-flags-extract(42,1353
-(defun phox-prog-flags-erase(53,1644
-(defun phox-toggle-extraction(61,1840
-(defun phox-compile-theorem(73,2242
-(defun phox-compile-theorem-on-cursor(79,2468
-(defun phox-output 95,2947
-(defun phox-output-theorem 105,3161
-(defun phox-output-theorem-on-cursor(112,3461
+(defvar phox-prog-orig 11,480
+(defun phox-prog-flags-modify(13,548
+(defun phox-prog-flags-extract(42,1349
+(defun phox-prog-flags-erase(53,1639
+(defun phox-toggle-extraction(61,1835
+(defun phox-compile-theorem(73,2237
+(defun phox-compile-theorem-on-cursor(79,2462
+(defun phox-output 95,2940
+(defun phox-output-theorem 105,3152
+(defun phox-output-theorem-on-cursor(112,3451
 
 phox/phox-font.el,123
 (defconst phox-font-lock-keywords6,282
-(defconst phox-sym-lock-keywords-table65,2401
-(defun phox-sym-lock-start 88,2975
-
-phox/phox-fun.el,679
-(defun phox-init-syntax-table 67,2393
-(defvar phox-top-keywords83,2866
-(defvar phox-proof-keywords131,3321
-(defun phox-find-and-forget 172,3671
-(defun phox-assert-next-command-interactive 251,6096
-(defun phox-depend-theorem(270,6927
-(defun phox-eshow-extlist(279,7217
-(defun phox-flag-name(293,7816
-(defun phox-path(304,8119
-(defun phox-print-expression(315,8356
-(defun phox-print-sort-expression(328,8814
-(defun phox-priority-symbols-list(339,9127
-(defun phox-search-string(351,9500
-(defun phox-constraints(366,10028
-(defun phox-goals(377,10285
-(defvar phox-state-menu389,10495
-(defun phox-delete-symbol(414,11485
-(defun phox-delete-symbol-on-cursor(420,11694
-
-phox/phox-lang.el,283
-(defvar phox-lang8,279
-(defun phox-lang-absurd 17,496
-(defun phox-lang-suppress 22,591
-(defun phox-lang-opendef 27,790
-(defun phox-lang-instance 32,909
-(defun phox-lang-lock 37,1038
-(defun phox-lang-unlock 42,1175
-(defun phox-lang-prove 47,1318
-(defun phox-lang-let 52,1455
+(defconst phox-sym-lock-keywords-table65,2399
+(defun phox-sym-lock-start 88,2973
+
+phox/phox-fun.el,678
+(defun phox-init-syntax-table 67,2384
+(defvar phox-top-keywords83,2856
+(defvar phox-proof-keywords131,3311
+(defun phox-find-and-forget 172,3661
+(defun phox-assert-next-command-interactive 251,6059
+(defun phox-depend-theorem(269,6863
+(defun phox-eshow-extlist(278,7152
+(defun phox-flag-name(292,7749
+(defun phox-path(303,8051
+(defun phox-print-expression(314,8287
+(defun phox-print-sort-expression(327,8743
+(defun phox-priority-symbols-list(338,9055
+(defun phox-search-string(350,9427
+(defun phox-constraints(365,9952
+(defun phox-goals(376,10208
+(defvar phox-state-menu388,10417
+(defun phox-delete-symbol(413,11407
+(defun phox-delete-symbol-on-cursor(419,11615
+
+phox/phox-lang.el,323
+(defvar phox-lang9,306
+(defun phox-lang-absurd 17,535
+(defun phox-lang-suppress 22,629
+(defun phox-lang-opendef 27,826
+(defun phox-lang-instance 32,944
+(defun phox-lang-open-instance 37,1073
+(defun phox-lang-lock 42,1222
+(defun phox-lang-unlock 47,1352
+(defun phox-lang-prove 52,1488
+(defun phox-lang-let 57,1622
 
 phox/phox-outline.el,70
-(defun phox-outline-level(32,1113
-(defun phox-setup-outline 46,1587
+(defun phox-outline-level(32,1102
+(defun phox-setup-outline 46,1576
 
 phox/phox-pbrpm.el,512
-(defun phox-pbrpm-left-paren-p 27,1189
-(defun phox-pbrpm-right-paren-p 34,1392
-(defun phox-pbrpm-menu-from-string 42,1596
-(defun phox-pbrpm-rename-in-cmd 51,1930
-(defun phox-pbrpm-get-region-name 84,3184
-(defun  phox-pbrpm-escape-string 87,3311
-(defun phox-pbrpm-generate-menu 91,3446
-(defalias 'proof-pbrpm-generate-menu proof-pbrpm-generate-menu
289,10635
-(defalias 'proof-pbrpm-left-paren-p proof-pbrpm-left-paren-p
290,10699
-(defalias 'proof-pbrpm-right-paren-p proof-pbrpm-right-paren-p
291,10761
+(defun phox-pbrpm-left-paren-p 27,1188
+(defun phox-pbrpm-right-paren-p 34,1391
+(defun phox-pbrpm-menu-from-string 42,1595
+(defun phox-pbrpm-rename-in-cmd 51,1927
+(defun phox-pbrpm-get-region-name 84,3175
+(defun  phox-pbrpm-escape-string 87,3302
+(defun phox-pbrpm-generate-menu 91,3437
+(defalias 'proof-pbrpm-generate-menu proof-pbrpm-generate-menu
298,10917
+(defalias 'proof-pbrpm-left-paren-p proof-pbrpm-left-paren-p
299,10981
+(defalias 'proof-pbrpm-right-paren-p proof-pbrpm-right-paren-p
300,11043
 
 phox/phox-sym-lock.el,1353
-(defvar phox-sym-lock-sym-count 34,1598
-(defvar phox-sym-lock-ext-start 37,1668
-(defvar phox-sym-lock-ext-end 39,1790
-(defvar phox-sym-lock-font-size 42,1909
-(defvar phox-sym-lock-keywords 47,2099
-(defvar phox-sym-lock-enabled 52,2275
-(defvar phox-sym-lock-color 57,2437
-(defvar phox-sym-lock-mouse-face 62,2655
-(defvar phox-sym-lock-mouse-face-enabled 67,2845
-(defconst phox-sym-lock-with-mule 72,3035
-(defun phox-sym-lock-gen-symbol 75,3119
-(defun phox-sym-lock-make-symbols-atomic 83,3422
-(defun phox-sym-lock-compute-font-size 110,4364
-(defvar phox-sym-lock-font-name148,5784
-(defun phox-sym-lock-set-foreground 190,7270
-(defun phox-sym-lock-translate-char 204,7879
-(defun phox-sym-lock-translate-char-or-string 212,8147
-(defun phox-sym-lock-remap-face 219,8374
-(defvar phox-sym-lock-clear-face239,9364
-(defun phox-sym-lock 251,9786
-(defun phox-sym-lock-rec 260,10190
-(defun phox-sym-lock-atom-face 266,10343
-(defun phox-sym-lock-pre-idle-hook-first 271,10639
-(defun phox-sym-lock-pre-idle-hook-last 279,10997
-(defun phox-sym-lock-enable 288,11372
-(defun phox-sym-lock-disable 301,11785
-(defun phox-sym-lock-mouse-face-enable 314,12203
-(defun phox-sym-lock-mouse-face-disable 321,12418
-(defun phox-sym-lock-font-lock-hook 328,12637
-(defun font-lock-set-defaults 343,13330
-(defun phox-sym-lock-patch-keywords 354,13708
+(defvar phox-sym-lock-sym-count 34,1596
+(defvar phox-sym-lock-ext-start 37,1666
+(defvar phox-sym-lock-ext-end 39,1788
+(defvar phox-sym-lock-font-size 42,1907
+(defvar phox-sym-lock-keywords 47,2097
+(defvar phox-sym-lock-enabled 52,2273
+(defvar phox-sym-lock-color 57,2435
+(defvar phox-sym-lock-mouse-face 62,2653
+(defvar phox-sym-lock-mouse-face-enabled 67,2843
+(defconst phox-sym-lock-with-mule 72,3033
+(defun phox-sym-lock-gen-symbol 75,3117
+(defun phox-sym-lock-make-symbols-atomic 83,3419
+(defun phox-sym-lock-compute-font-size 110,4360
+(defvar phox-sym-lock-font-name148,5779
+(defun phox-sym-lock-set-foreground 190,7258
+(defun phox-sym-lock-translate-char 204,7867
+(defun phox-sym-lock-translate-char-or-string 212,8135
+(defun phox-sym-lock-remap-face 219,8362
+(defvar phox-sym-lock-clear-face239,9352
+(defun phox-sym-lock 251,9773
+(defun phox-sym-lock-rec 260,10177
+(defun phox-sym-lock-atom-face 266,10322
+(defun phox-sym-lock-pre-idle-hook-first 271,10618
+(defun phox-sym-lock-pre-idle-hook-last 279,10976
+(defun phox-sym-lock-enable 288,11351
+(defun phox-sym-lock-disable 301,11764
+(defun phox-sym-lock-mouse-face-enable 314,12182
+(defun phox-sym-lock-mouse-face-disable 321,12397
+(defun phox-sym-lock-font-lock-hook 328,12616
+(defun font-lock-set-defaults 343,13307
+(defun phox-sym-lock-patch-keywords 354,13671
 
 phox/phox-tags.el,305
-(defun phox-tags-add-table(21,767
-(defun phox-tags-reset-table(29,1096
-(defun phox-tags-add-doc-table(34,1206
-(defun phox-tags-add-lib-table(40,1355
-(defun phox-tags-add-local-table(46,1491
-(defun phox-tags-create-local-table(52,1674
-(defun phox-complete-tag(63,1926
-(defvar phox-tags-menu70,2035
-
-plastic/plastic.el,2863
-(defcustom plastic-tags 22,491
-(defcustom plastic-test-all-name 27,623
-(defvar plastic-lit-string 34,814
-(defcustom plastic-help-menu-list38,928
-(defvar plastic-shell-process-output52,1422
-(defconst plastic-process-config 60,1748
-(defconst plastic-pretty-set-width 67,1998
-(defconst plastic-interrupt-regexp 71,2147
-(defcustom plastic-www-home-page 77,2268
-(defcustom plastic-www-latest-release82,2405
-(defcustom plastic-www-refcard88,2578
-(defcustom plastic-library-www-page94,2709
-(defcustom plastic-base 104,2924
-(defvar plastic-prog-name 112,3096
-(defun plastic-set-default-env-vars 116,3204
-(defvar plastic-shell-prompt-pattern 124,3442
-(defvar plastic-shell-cd 127,3567
-(defvar plastic-shell-abort-goal-regexp 131,3709
-(defvar plastic-shell-proof-completed-regexp 135,3877
-(defvar plastic-save-command-regexp138,4020
-(defvar plastic-goal-command-regexp140,4116
-(defvar plastic-kill-goal-command 143,4213
-(defvar plastic-forget-id-command 145,4314
-(defvar plastic-undoable-commands-regexp148,4395
-(defvar plastic-goal-regexp 160,4842
-(defvar plastic-outline-regexp162,4890
-(defvar plastic-outline-heading-end-regexp 168,5069
-(defvar plastic-shell-outline-regexp 170,5125
-(defvar plastic-shell-outline-heading-end-regexp 171,5183
-(defvar plastic-error-occurred 173,5254
-(define-derived-mode plastic-shell-mode 182,5586
-(define-derived-mode plastic-mode 188,5768
-(define-derived-mode plastic-goals-mode 204,6288
-(defun plastic-count-undos 213,6633
-(defun plastic-goal-command-p 233,7509
-(defun plastic-find-and-forget 238,7702
-(defun plastic-goal-hyp 273,9050
-(defun plastic-state-preserving-p 284,9300
-(defvar plastic-shell-current-line-width 307,10276
-(defun plastic-shell-adjust-line-width 315,10592
-(defun plastic-mode-config 342,11687
-(defun plastic-show-shell-buffer 431,14962
-(defun plastic-equal-module-filename 437,15065
-(defun plastic-shell-compute-new-files-list 443,15343
-(defun plastic-shell-mode-config 459,15880
-(defun plastic-goals-mode-config 510,18086
-(defun plastic-small-bar 522,18380
-(defun plastic-large-bar 524,18469
-(defun plastic-preprocessing 526,18607
-(defun plastic-all-ctxt 577,20435
-(defun plastic-send-one-undo 584,20613
-(defun plastic-minibuf-cmd 594,20941
-(defun plastic-minibuf 606,21420
-(defun plastic-synchro 613,21626
-(defun plastic-send-minibuf 618,21767
-(defun plastic-had-error 626,22096
-(defun plastic-reset-error 630,22271
-(defun plastic-call-if-no-error 633,22410
-(defun plastic-show-shell 638,22614
-(define-key plastic-keymap 647,22876
-(define-key plastic-keymap 648,22937
-(define-key plastic-keymap 649,22998
-(define-key plastic-keymap 650,23058
-(define-key plastic-keymap 651,23117
-(define-key plastic-keymap 652,23176
-(defalias 'proof-toolbar-command proof-toolbar-command
662,23426
-(defalias 'proof-minibuffer-cmd proof-minibuffer-cmd
663,23477
+(defun phox-tags-add-table(21,766
+(defun phox-tags-reset-table(30,1161
+(defun phox-tags-add-doc-table(35,1271
+(defun phox-tags-add-lib-table(41,1420
+(defun phox-tags-add-local-table(47,1555
+(defun phox-tags-create-local-table(53,1738
+(defun phox-complete-tag(64,1988
+(defvar phox-tags-menu71,2097
+
+plastic/plastic.el,2808
+(defcustom plastic-tags 22,490
+(defcustom plastic-test-all-name 27,622
+(defvar plastic-lit-string34,813
+(defcustom plastic-help-menu-list38,925
+(defvar plastic-shell-process-output52,1418
+(defconst plastic-process-config60,1744
+(defconst plastic-pretty-set-width 67,1992
+(defconst plastic-interrupt-regexp 71,2140
+(defcustom plastic-www-home-page 77,2261
+(defcustom plastic-www-latest-release82,2398
+(defcustom plastic-www-refcard88,2568
+(defcustom plastic-library-www-page94,2699
+(defcustom plastic-base104,2914
+(defvar plastic-prog-name112,3085
+(defun plastic-set-default-env-vars 116,3192
+(defvar plastic-shell-cd124,3429
+(defvar plastic-shell-abort-goal-regexp 128,3569
+(defvar plastic-shell-proof-completed-regexp 132,3737
+(defvar plastic-save-command-regexp135,3880
+(defvar plastic-goal-command-regexp137,3976
+(defvar plastic-kill-goal-command140,4073
+(defvar plastic-forget-id-command142,4173
+(defvar plastic-undoable-commands-regexp145,4253
+(defvar plastic-goal-regexp 157,4700
+(defvar plastic-outline-regexp159,4748
+(defvar plastic-outline-heading-end-regexp 165,4926
+(defvar plastic-shell-outline-regexp 167,4982
+(defvar plastic-shell-outline-heading-end-regexp 168,5040
+(defvar plastic-error-occurred170,5111
+(define-derived-mode plastic-shell-mode 179,5428
+(define-derived-mode plastic-mode 185,5610
+(define-derived-mode plastic-goals-mode 201,6127
+(defun plastic-count-undos 210,6472
+(defun plastic-goal-command-p 230,7347
+(defun plastic-find-and-forget 235,7539
+(defun plastic-goal-hyp 270,8814
+(defun plastic-state-preserving-p 281,9063
+(defvar plastic-shell-current-line-width 304,10038
+(defun plastic-shell-adjust-line-width 312,10354
+(defun plastic-mode-config 339,11392
+(defun plastic-show-shell-buffer 428,14651
+(defun plastic-equal-module-filename 434,14754
+(defun plastic-shell-compute-new-files-list 440,15032
+(defun plastic-shell-mode-config 452,15426
+(defun plastic-goals-mode-config 501,17279
+(defun plastic-small-bar 513,17566
+(defun plastic-large-bar 515,17655
+(defun plastic-preprocessing 517,17793
+(defun plastic-all-ctxt 568,19574
+(defun plastic-send-one-undo 575,19743
+(defun plastic-minibuf-cmd 585,20049
+(defun plastic-minibuf 597,20521
+(defun plastic-synchro 604,20727
+(defun plastic-send-minibuf 609,20868
+(defun plastic-had-error 617,21176
+(defun plastic-reset-error 621,21351
+(defun plastic-call-if-no-error 624,21490
+(defun plastic-show-shell 629,21694
+(define-key plastic-keymap 638,21956
+(define-key plastic-keymap 639,22017
+(define-key plastic-keymap 640,22078
+(define-key plastic-keymap 641,22138
+(define-key plastic-keymap 642,22197
+(define-key plastic-keymap 643,22256
+(defalias 'proof-toolbar-command proof-toolbar-command
653,22505
+(defalias 'proof-minibuffer-cmd proof-minibuffer-cmd
654,22556
 
 plastic/plastic-syntax.el,648
-(defconst plastic-keywords-goal 18,537
-(defconst plastic-keywords-save 20,583
-(defconst plastic-commands22,657
-(defconst plastic-keywords35,1267
-(defconst plastic-tacticals 40,1450
-(defconst plastic-error-regexp 43,1561
-(defvar plastic-id 46,1695
-(defvar plastic-ids 48,1725
-(defconst plastic-arg-list-regexp 52,1933
-(defun plastic-decl-defn-regexp 55,2052
-(defconst plastic-definiendum-alternative-regexp63,2433
-(defvar plastic-font-lock-terms67,2626
-(defconst plastic-goal-with-hole-regexp89,3339
-(defconst plastic-save-with-hole-regexp94,3566
-(defvar plastic-font-lock-keywords-199,3792
-(defun plastic-init-syntax-table 108,4184
-
-twelf/twelf.el,463
-(defcustom twelf-root-dir25,592
-(defcustom twelf-info-dir31,750
-(defun twelf-add-read-declaration 100,3260
-(defun twelf-set-syntax 113,3595
-(defun twelf-set-word 115,3692
-(defun twelf-set-symbol 116,3754
-(defun twelf-map-string 118,3818
-(defun twelf-mode-extra-config 165,5880
-(defconst twelf-syntax-menu171,6086
-(defpacustom chatter 185,6453
-(defpacustom double-check 190,6546
-(defpacustom print-implicit 194,6683
-(defpgdefault menu-entries206,6827
+(defconst plastic-keywords-goal 18,536
+(defconst plastic-keywords-save 20,582
+(defconst plastic-commands22,656
+(defconst plastic-keywords35,1263
+(defconst plastic-tacticals 40,1446
+(defconst plastic-error-regexp 43,1557
+(defvar plastic-id 46,1690
+(defvar plastic-ids 48,1720
+(defconst plastic-arg-list-regexp 52,1928
+(defun plastic-decl-defn-regexp 55,2047
+(defconst plastic-definiendum-alternative-regexp63,2428
+(defvar plastic-font-lock-terms67,2621
+(defconst plastic-goal-with-hole-regexp89,3331
+(defconst plastic-save-with-hole-regexp94,3557
+(defvar plastic-font-lock-keywords-199,3783
+(defun plastic-init-syntax-table 108,4175
+
+twelf/twelf.el,462
+(defcustom twelf-root-dir25,589
+(defcustom twelf-info-dir31,747
+(defun twelf-add-read-declaration 99,3198
+(defun twelf-set-syntax 112,3533
+(defun twelf-set-word 114,3630
+(defun twelf-set-symbol 115,3692
+(defun twelf-map-string 117,3756
+(defun twelf-mode-extra-config 164,5816
+(defconst twelf-syntax-menu170,6021
+(defpacustom chatter 184,6388
+(defpacustom double-check 189,6481
+(defpacustom print-implicit 193,6618
+(defpgdefault menu-entries205,6762
 
 twelf/twelf-font.el,917
-(defun twelf-font-create-face 31,837
-(defvar twelf-font-dark-background 38,1095
-(defvar twelf-font-patterns64,2453
-(defun twelf-font-fontify-decl 105,4303
-(defun twelf-font-fontify-buffer 115,4600
-(defun twelf-font-unfontify 122,4859
-(defvar font-lock-message-threshold 127,5033
-(defun twelf-font-fontify-region 129,5111
-(defun twelf-font-highlight 195,7611
-(defun twelf-font-find-delimited-comment 204,8068
-(defun twelf-font-find-decl 223,8748
-(defun twelf-font-find-binder 239,9238
-(defun twelf-font-find-parm 301,11095
-(defun twelf-font-find-evar 308,11418
-(defun twelf-current-decl 330,12160
-(defun twelf-next-decl 357,13316
-(defconst *whitespace* 382,14338
-(defconst *twelf-comment-start* 385,14436
-(defconst *twelf-id-chars* 388,14565
-(defun skip-twelf-comments-and-whitespace 391,14683
-(defun twelf-end-of-par 403,15157
-(defun skip-ahead 426,15931
-(defun current-line-absolute 438,16353
-
-twelf/twelf-old.el,6958
-(defvar twelf-indent 212,8772
-(defvar twelf-infix-regexp 215,8832
-(defvar twelf-server-program 219,9027
-(defvar twelf-info-file 222,9108
-(defvar twelf-server-display-commands 225,9181
-(defvar twelf-highlight-range-function 230,9429
-(defvar twelf-focus-function 235,9712
-(defvar twelf-server-echo-commands 241,9992
-(defvar twelf-save-silently 244,10113
-(defvar twelf-server-timeout 248,10285
-(defvar twelf-sml-program 252,10432
-(defvar twelf-sml-args 255,10504
-(defvar twelf-sml-display-queries 258,10570
-(defvar twelf-mode-hook 261,10678
-(defvar twelf-server-mode-hook 264,10772
-(defvar twelf-config-mode-hook 267,10880
-(defvar twelf-sml-mode-hook 270,10994
-(defvar twelf-to-twelf-sml-mode 273,11075
-(defvar twelf-config-mode 276,11167
-(defvar *twelf-server-buffer-name* 283,11431
-(defvar *twelf-server-buffer* 286,11535
-(defvar *twelf-server-process-name* 289,11623
-(defvar *twelf-config-buffer* 292,11714
-(defvar *twelf-config-time* 295,11808
-(defvar *twelf-config-list* 298,11921
-(defvar *twelf-server-last-process-mark* 301,12033
-(defvar *twelf-last-region-sent* 304,12151
-(defvar *twelf-last-input-buffer* 311,12475
-(defvar *twelf-error-pos* 315,12598
-(defconst *twelf-read-functions*318,12674
-(defconst *twelf-parm-table*325,12912
-(defvar twelf-chatter 338,13288
-(defvar twelf-double-check 346,13505
-(defvar twelf-print-implicit 349,13592
-(defconst *twelf-track-parms*352,13684
-(defun install-basic-twelf-keybindings 363,14108
-(defun install-twelf-keybindings 388,15077
-(defvar twelf-mode-map 404,15842
-(defvar twelf-mode-syntax-table 416,16278
-(defun set-twelf-syntax 419,16357
-(defun set-word 421,16454
-(defun set-symbol 422,16509
-(defun map-string 424,16567
-(defconst *whitespace* 456,18044
-(defconst *twelf-comment-start* 459,18142
-(defconst *twelf-id-chars* 462,18271
-(defun skip-twelf-comments-and-whitespace 465,18389
-(defun twelf-end-of-par 477,18863
-(defun twelf-current-decl 500,19637
-(defun twelf-mark-decl 527,20793
-(defun twelf-indent-decl 536,21059
-(defun twelf-indent-region 545,21345
-(defun twelf-indent-lines 556,21669
-(defun twelf-comment-indent 564,21842
-(defun looked-at 575,22198
-(defun twelf-indent-line 580,22370
-(defun twelf-indent-line-to 613,24113
-(defun twelf-calculate-indent 626,24568
-(defun twelf-dsb 641,25192
-(defun twelf-mode-variables 667,26604
-(defun twelf-mode 689,27417
-(defun twelf-info 904,35799
-(defconst twelf-error-regexp918,36339
-(defconst twelf-error-fields-regexp922,36450
-(defconst twelf-error-decl-regexp928,36663
-(defun looked-at-nth 932,36812
-(defun looked-at-nth-int 938,36994
-(defun twelf-error-parser 943,37112
-(defun twelf-error-decl 957,37715
-(defun twelf-mark-relative 963,37894
-(defun twelf-mark-absolute 979,38564
-(defun twelf-find-decl 1004,39450
-(defun twelf-next-error 1019,40006
-(defun twelf-goto-error 1087,42816
-(defun twelf-convert-standard-filename 1101,43354
-(defun string-member 1113,43849
-(defun twelf-config-proceed-p 1125,44341
-(defun twelf-save-if-config 1132,44603
-(defun twelf-config-save-some-buffers 1145,45075
-(defun twelf-save-check-config 1149,45240
-(defun twelf-check-config 1164,45796
-(defun twelf-save-check-file 1176,46236
-(defun twelf-buffer-substring 1192,46959
-(defun twelf-buffer-substring-dot 1198,47221
-(defun twelf-check-declaration 1204,47487
-(defun twelf-highlight-range-zmacs 1227,48547
-(defun twelf-focus 1233,48797
-(defun twelf-focus-noop 1239,49063
-(defun twelf-type-const 1322,52685
-(defvar twelf-server-mode-map 1439,57827
-(defconst twelf-server-cd-regexp 1451,58379
-(defun looked-at-string 1454,58519
-(defun twelf-server-directory-tracker 1458,58660
-(defun twelf-input-filter 1480,59840
-(defun twelf-server-mode 1486,60095
-(defun twelf-parse-config 1519,61312
-(defun twelf-server-read-config 1537,62204
-(defun twelf-server-sync-config 1546,62541
-(defun twelf-get-server-buffer 1576,64047
-(defun twelf-init-variables 1593,64721
-(defun twelf-server 1600,64934
-(defun twelf-server-process 1642,66848
-(defun twelf-server-display 1651,67254
-(defun display-server-buffer 1658,67528
-(defun twelf-server-send-command 1673,68260
-(defun twelf-accept-process-output 1694,69220
-(defun twelf-server-wait 1703,69659
-(defun twelf-server-quit 1745,71797
-(defun twelf-server-interrupt 1750,71918
-(defun twelf-reset 1755,72054
-(defun twelf-config-directory 1760,72198
-(defun twelf-server-configure 1771,72612
-(defun natp 1844,75904
-(defun twelf-read-nat 1848,76005
-(defun twelf-read-bool 1857,76272
-(defun twelf-read-limit 1863,76420
-(defun twelf-read-strategy 1873,76723
-(defun twelf-read-value 1879,76875
-(defun twelf-set 1883,77038
-(defun twelf-set-parm 1896,77515
-(defun track-parm 1905,77812
-(defun twelf-toggle-double-check 1910,77986
-(defun twelf-toggle-print-implicit 1916,78189
-(defun twelf-get 1922,78402
-(defun twelf-timers-reset 1936,79028
-(defun twelf-timers-show 1941,79148
-(defun twelf-timers-check 1947,79299
-(defun twelf-server-restart 1953,79464
-(defun twelf-config-mode 1969,80141
-(defun twelf-config-mode-check 1985,80740
-(defun twelf-tag 1994,81190
-(defun twelf-tag-files 2022,82454
-(default: *tags-errors*)2026,82757
-(defun twelf-tag-file 2047,83508
-(defun twelf-next-decl 2082,84730
-(defun skip-ahead 2107,85752
-(defun current-line-absolute 2119,86174
-(defun new-temp-buffer 2124,86384
-(defun rev-relativize 2135,86768
-(defvar twelf-sml-mode-map 2149,87228
-(defconst twelf-sml-prompt-regexp 2159,87606
-(defun expand-dir 2161,87661
-(defun twelf-sml-cd 2168,87922
-(defconst twelf-sml-cd-regexp 2180,88411
-(defun twelf-sml-directory-tracker 2183,88545
-(defun twelf-sml-mode 2199,89390
-(defun twelf-sml 2250,91324
-(defun switch-to-twelf-sml 2270,92284
-(defun display-twelf-sml-buffer 2281,92633
-(defun twelf-sml-send-string 2297,93349
-(defun twelf-sml-send-region 2302,93553
-(defun twelf-sml-send-query 2326,94759
-(defun twelf-sml-send-newline 2336,95156
-(defun twelf-sml-send-semicolon 2344,95484
-(defun twelf-sml-status 2352,95818
-(defvar twelf-sml-init 2374,96765
-(defun twelf-sml-set-mode 2377,96942
-(defun twelf-sml-quit 2403,98119
-(defun twelf-sml-process-buffer 2408,98231
-(defun twelf-sml-process 2412,98347
-(defvar twelf-to-twelf-sml-mode 2424,98863
-(defun install-twelf-to-twelf-sml-keybindings 2427,98948
-(defvar twelf-to-twelf-sml-mode-map 2437,99333
-(defun twelf-to-twelf-sml-mode 2448,99846
-(defconst twelf-at-point-menu2498,101713
-(defconst twelf-server-state-menu2508,102085
-(defconst twelf-error-menu2518,102402
-(defconst twelf-tags-menu2524,102546
-(defun twelf-toggle-server-display-commands 2534,102831
-(defconst twelf-options-menu2537,102955
-(defconst twelf-timers-menu2572,104693
-(defconst twelf-syntax-menu2585,105187
-(defun twelf-add-menu 2612,106053
-(defun twelf-remove-menu 2616,106155
-(defun twelf-reset-menu 2620,106253
-(defun twelf-server-add-menu 2647,107152
-(defun twelf-server-remove-menu 2651,107275
-(defun twelf-server-reset-menu 2655,107387
+(defun twelf-font-create-face 31,836
+(defvar twelf-font-dark-background 38,1094
+(defvar twelf-font-patterns64,2451
+(defun twelf-font-fontify-decl 105,4300
+(defun twelf-font-fontify-buffer 115,4597
+(defun twelf-font-unfontify 122,4856
+(defvar font-lock-message-threshold 127,5030
+(defun twelf-font-fontify-region 129,5108
+(defun twelf-font-highlight 195,7607
+(defun twelf-font-find-delimited-comment 204,8064
+(defun twelf-font-find-decl 223,8744
+(defun twelf-font-find-binder 239,9234
+(defun twelf-font-find-parm 301,11091
+(defun twelf-font-find-evar 308,11414
+(defun twelf-current-decl 330,12155
+(defun twelf-next-decl 357,13283
+(defconst *whitespace* 382,14200
+(defconst *twelf-comment-start* 385,14298
+(defconst *twelf-id-chars* 388,14427
+(defun skip-twelf-comments-and-whitespace 391,14545
+(defun twelf-end-of-par 403,15005
+(defun skip-ahead 426,15737
+(defun current-line-absolute 438,16159
+
+twelf/twelf-old.el,6952
+(defvar twelf-indent 212,8762
+(defvar twelf-infix-regexp 215,8822
+(defvar twelf-server-program 219,9017
+(defvar twelf-info-file 222,9098
+(defvar twelf-server-display-commands 225,9171
+(defvar twelf-highlight-range-function 230,9419
+(defvar twelf-focus-function 235,9702
+(defvar twelf-server-echo-commands 241,9982
+(defvar twelf-save-silently 244,10103
+(defvar twelf-server-timeout 248,10275
+(defvar twelf-sml-program 252,10422
+(defvar twelf-sml-args 255,10494
+(defvar twelf-sml-display-queries 258,10560
+(defvar twelf-mode-hook 261,10668
+(defvar twelf-server-mode-hook 264,10762
+(defvar twelf-config-mode-hook 267,10870
+(defvar twelf-sml-mode-hook 270,10984
+(defvar twelf-to-twelf-sml-mode 273,11065
+(defvar twelf-config-mode 276,11157
+(defvar *twelf-server-buffer-name* 283,11421
+(defvar *twelf-server-buffer* 286,11525
+(defvar *twelf-server-process-name* 289,11613
+(defvar *twelf-config-buffer* 292,11704
+(defvar *twelf-config-time* 295,11798
+(defvar *twelf-config-list* 298,11911
+(defvar *twelf-server-last-process-mark* 301,12023
+(defvar *twelf-last-region-sent* 304,12141
+(defvar *twelf-last-input-buffer* 311,12465
+(defvar *twelf-error-pos* 315,12588
+(defconst *twelf-read-functions*318,12664
+(defconst *twelf-parm-table*325,12902
+(defvar twelf-chatter 338,13278
+(defvar twelf-double-check 346,13495
+(defvar twelf-print-implicit 349,13582
+(defconst *twelf-track-parms*352,13674
+(defun install-basic-twelf-keybindings 363,14098
+(defun install-twelf-keybindings 388,15067
+(defvar twelf-mode-map 404,15832
+(defvar twelf-mode-syntax-table 416,16268
+(defun set-twelf-syntax 419,16347
+(defun set-word 421,16444
+(defun set-symbol 422,16499
+(defun map-string 424,16557
+(defconst *whitespace* 456,18034
+(defconst *twelf-comment-start* 459,18132
+(defconst *twelf-id-chars* 462,18261
+(defun skip-twelf-comments-and-whitespace 465,18379
+(defun twelf-end-of-par 477,18839
+(defun twelf-current-decl 500,19571
+(defun twelf-mark-decl 527,20699
+(defun twelf-indent-decl 536,20951
+(defun twelf-indent-region 545,21223
+(defun twelf-indent-lines 556,21505
+(defun twelf-comment-indent 564,21678
+(defun looked-at 575,21992
+(defun twelf-indent-line 580,22164
+(defun twelf-indent-line-to 613,23746
+(defun twelf-calculate-indent 626,24180
+(defun twelf-dsb 641,24734
+(defun twelf-mode-variables 667,25985
+(defun twelf-mode 689,26798
+(defun twelf-info 904,35180
+(defconst twelf-error-regexp918,35720
+(defconst twelf-error-fields-regexp922,35831
+(defconst twelf-error-decl-regexp928,36044
+(defun looked-at-nth 932,36191
+(defun looked-at-nth-int 938,36366
+(defun twelf-error-parser 943,36484
+(defun twelf-error-decl 957,37052
+(defun twelf-mark-relative 963,37231
+(defun twelf-mark-absolute 979,37845
+(defun twelf-find-decl 1004,38731
+(defun twelf-next-error 1019,39287
+(defun twelf-goto-error 1087,42062
+(defun twelf-convert-standard-filename 1101,42586
+(defun string-member 1113,43081
+(defun twelf-config-proceed-p 1125,43573
+(defun twelf-save-if-config 1132,43835
+(defun twelf-config-save-some-buffers 1145,44307
+(defun twelf-save-check-config 1149,44472
+(defun twelf-check-config 1164,45028
+(defun twelf-save-check-file 1176,45468
+(defun twelf-buffer-substring 1192,46191
+(defun twelf-buffer-substring-dot 1198,46453
+(defun twelf-check-declaration 1204,46719
+(defun twelf-highlight-range-zmacs 1227,47758
+(defun twelf-focus 1233,48008
+(defun twelf-focus-noop 1239,48274
+(defun twelf-type-const 1322,51896
+(defvar twelf-server-mode-map 1439,56960
+(defconst twelf-server-cd-regexp 1451,57512
+(defun looked-at-string 1454,57652
+(defun twelf-server-directory-tracker 1458,57793
+(defun twelf-input-filter 1480,58952
+(defun twelf-server-mode 1486,59207
+(defun twelf-parse-config 1519,60424
+(defun twelf-server-read-config 1537,61190
+(defun twelf-server-sync-config 1546,61520
+(defun twelf-get-server-buffer 1576,62892
+(defun twelf-init-variables 1593,63510
+(defun twelf-server 1600,63723
+(defun twelf-server-process 1642,65357
+(defun twelf-server-display 1651,65721
+(defun display-server-buffer 1658,65995
+(defun twelf-server-send-command 1673,66650
+(defun twelf-accept-process-output 1694,67526
+(defun twelf-server-wait 1703,67965
+(defun twelf-server-quit 1745,69718
+(defun twelf-server-interrupt 1750,69839
+(defun twelf-reset 1755,69975
+(defun twelf-config-directory 1760,70119
+(defun twelf-server-configure 1771,70533
+(defun natp 1844,73650
+(defun twelf-read-nat 1848,73751
+(defun twelf-read-bool 1857,74018
+(defun twelf-read-limit 1863,74166
+(defun twelf-read-strategy 1873,74469
+(defun twelf-read-value 1879,74621
+(defun twelf-set 1883,74784
+(defun twelf-set-parm 1896,75260
+(defun track-parm 1905,75557
+(defun twelf-toggle-double-check 1910,75731
+(defun twelf-toggle-print-implicit 1916,75934
+(defun twelf-get 1922,76147
+(defun twelf-timers-reset 1936,76773
+(defun twelf-timers-show 1941,76893
+(defun twelf-timers-check 1947,77044
+(defun twelf-server-restart 1953,77209
+(defun twelf-config-mode 1969,77823
+(defun twelf-config-mode-check 1985,78422
+(defun twelf-tag 1994,78872
+(defun twelf-tag-files 2022,80059
+(default: *tags-errors*)2026,80362
+(defun twelf-tag-file 2047,81057
+(defun twelf-next-decl 2082,82265
+(defun skip-ahead 2107,83182
+(defun current-line-absolute 2119,83604
+(defun new-temp-buffer 2124,83814
+(defun rev-relativize 2135,84177
+(defvar twelf-sml-mode-map 2149,84630
+(defconst twelf-sml-prompt-regexp 2159,85008
+(defun expand-dir 2161,85063
+(defun twelf-sml-cd 2168,85317
+(defconst twelf-sml-cd-regexp 2180,85806
+(defun twelf-sml-directory-tracker 2183,85940
+(defun twelf-sml-mode 2199,86680
+(defun twelf-sml 2250,88605
+(defun switch-to-twelf-sml 2270,89565
+(defun display-twelf-sml-buffer 2281,89900
+(defun twelf-sml-send-string 2297,90546
+(defun twelf-sml-send-region 2302,90750
+(defun twelf-sml-send-query 2326,91942
+(defun twelf-sml-send-newline 2336,92325
+(defun twelf-sml-send-semicolon 2344,92653
+(defun twelf-sml-status 2352,92987
+(defvar twelf-sml-init 2374,93822
+(defun twelf-sml-set-mode 2377,93999
+(defun twelf-sml-quit 2403,95092
+(defun twelf-sml-process-buffer 2408,95204
+(defun twelf-sml-process 2412,95320
+(defvar twelf-to-twelf-sml-mode 2424,95829
+(defun install-twelf-to-twelf-sml-keybindings 2427,95914
+(defvar twelf-to-twelf-sml-mode-map 2437,96299
+(defun twelf-to-twelf-sml-mode 2448,96812
+(defconst twelf-at-point-menu2498,98609
+(defconst twelf-server-state-menu2508,98981
+(defconst twelf-error-menu2518,99298
+(defconst twelf-tags-menu2524,99442
+(defun twelf-toggle-server-display-commands 2534,99727
+(defconst twelf-options-menu2537,99851
+(defconst twelf-timers-menu2572,101589
+(defconst twelf-syntax-menu2585,102083
+(defun twelf-add-menu 2612,102949
+(defun twelf-remove-menu 2616,103051
+(defun twelf-reset-menu 2620,103149
+(defun twelf-server-add-menu 2647,104048
+(defun twelf-server-remove-menu 2651,104171
+(defun twelf-server-reset-menu 2655,104283
 
 generic/pg-assoc.el,82
-(defun proof-associated-buffers 36,1066
-(defun proof-associated-windows 46,1278
+(defun proof-associated-buffers 36,1063
+(defun proof-associated-windows 46,1273
 
 generic/pg-autotest.el,442
-(defvar pg-autotest-success 24,544
-(defun pg-autotest-find-file 28,628
-(defun pg-autotest-find-file-restart 35,908
-(defmacro pg-autotest 48,1356
-(defun pg-autotest-script-wholefile 62,1703
-(defun pg-autotest-retract-file 79,2316
-(defun pg-autotest-assert-processed 85,2452
-(defun pg-autotest-assert-unprocessed 92,2706
-(defun pg-autotest-message 99,2966
-(defun pg-autotest-quit-prover 106,3159
-(defun pg-autotest-finished 112,3340
+(defvar pg-autotest-success 24,542
+(defun pg-autotest-find-file 28,626
+(defun pg-autotest-find-file-restart 35,906
+(defmacro pg-autotest 48,1354
+(defun pg-autotest-script-wholefile 62,1701
+(defun pg-autotest-retract-file 79,2314
+(defun pg-autotest-assert-processed 85,2450
+(defun pg-autotest-assert-unprocessed 92,2704
+(defun pg-autotest-message 99,2964
+(defun pg-autotest-quit-prover 106,3157
+(defun pg-autotest-finished 112,3338
 
 generic/pg-custom.el,554
-(defpgcustom maths-menu-enable 36,1137
-(defpgcustom unicode-tokens-enable 42,1317
-(defpgcustom mmm-enable 48,1494
-(defpgcustom script-indent 57,1848
-(defconst proof-toolbar-entries-default62,1985
-(defpgcustom toolbar-entries 90,3757
-(defpgcustom prog-args 109,4490
-(defpgcustom prog-env 122,5065
-(defpgcustom favourites 131,5491
-(defpgcustom menu-entries 136,5680
-(defpgcustom help-menu-entries 143,5916
-(defpgcustom keymap 150,6179
-(defpgcustom completion-table 155,6351
-(defpgcustom tags-program 166,6725
-(defpgcustom use-holes 175,7109
+(defpgcustom maths-menu-enable 36,1134
+(defpgcustom unicode-tokens-enable 42,1314
+(defpgcustom mmm-enable 48,1491
+(defpgcustom script-indent 57,1845
+(defconst proof-toolbar-entries-default62,1982
+(defpgcustom toolbar-entries 90,3754
+(defpgcustom prog-args 109,4487
+(defpgcustom prog-env 122,5062
+(defpgcustom favourites 131,5488
+(defpgcustom menu-entries 136,5677
+(defpgcustom help-menu-entries 143,5913
+(defpgcustom keymap 150,6176
+(defpgcustom completion-table 155,6347
+(defpgcustom tags-program 166,6721
+(defpgcustom use-holes 175,7105
 
 generic/pg-goals.el,285
 (define-derived-mode proof-goals-mode 30,654
 (define-key proof-goals-mode-map 58,1529
 (define-key proof-goals-mode-map 60,1645
 (define-key proof-goals-mode-map 61,1713
-(defun proof-goals-config-done 70,1859
-(defun pg-goals-display 78,2125
-(defun pg-goals-button-action 117,3449
-
-generic/pg-pbrpm.el,1803
-(defvar pg-pbrpm-use-buffer-menu 22,548
-(defvar pg-pbrpm-start-goal-regexp 25,670
-(defvar pg-pbrpm-start-goal-regexp-par-num 29,827
-(defvar pg-pbrpm-end-goal-regexp 32,950
-(defvar pg-pbrpm-start-hyp-regexp 36,1102
-(defvar pg-pbrpm-start-hyp-regexp-par-num 40,1263
-(defvar pg-pbrpm-start-concl-regexp 44,1470
-(defvar pg-pbrpm-auto-select-regexp 48,1634
-(defvar pg-pbrpm-buffer-menu 55,1795
-(defvar pg-pbrpm-spans 56,1829
-(defvar pg-pbrpm-goal-description 57,1857
-(defvar pg-pbrpm-windows-dialog-bug 58,1896
-(defvar pbrpm-menu-desc 59,1937
-(defun pg-pbrpm-erase-buffer-menu 61,1967
-(defun pg-pbrpm-menu-change-hook 68,2151
-(defun pg-pbrpm-create-reset-buffer-menu 86,2727
-(defun pg-pbrpm-analyse-goal-buffer 101,3356
-(defun pg-pbrpm-button-action 161,5766
-(defun pg-pbrpm-exists 168,5992
-(defun pg-pbrpm-eliminate-id 172,6104
-(defun pg-pbrpm-build-menu 180,6350
-(defun pg-pbrpm-setup-span 243,8676
-(defun pg-pbrpm-run-command 303,10994
-(defun pg-pbrpm-get-pos-info 332,12304
-(defun pg-pbrpm-get-region-info 374,13611
-(defun pg-pbrpm-auto-select-around-point 385,14025
-(defun pg-pbrpm-translate-position 400,14555
-(defun pg-pbrpm-process-click 408,14813
-(defvar pg-pbrpm-remember-region-selected-region 428,15838
-(defvar pg-pbrpm-regions-list 429,15892
-(defun pg-pbrpm-erase-regions-list 431,15928
-(defun pg-pbrpm-filter-regions-list 440,16236
-(defface pg-pbrpm-multiple-selection-face447,16499
-(defface pg-pbrpm-menu-input-face455,16701
-(defun pg-pbrpm-do-remember-region 463,16891
-(defun pg-pbrpm-remember-region-drag-up-hook 484,17739
-(defun pg-pbrpm-remember-region-click-hook 488,17910
-(defun pg-pbrpm-remember-region 493,18095
-(defun pg-pbrpm-process-region 507,18810
-(defun pg-pbrpm-process-regions-list 525,19539
-(defun pg-pbrpm-region-expression 529,19722
-
-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,1720
-(defvar pg-pgip-last-seen-seq 54,1754
-(defun pg-pgip-process-pgip 56,1790
-(defun pg-pgip-process-msg 75,2721
-(defvar pg-pgip-post-process-functions89,3291
-(defun pg-pgip-post-process 99,3779
-(defun pg-pgip-process-askpgip 115,4390
-(defun pg-pgip-process-usespgip 121,4595
-(defun pg-pgip-process-usespgml 125,4759
-(defun pg-pgip-process-pgmlconfig 129,4923
-(defun pg-pgip-process-proverinfo 145,5540
-(defun pg-pgip-process-hasprefs 162,6205
-(defun pg-pgip-haspref 176,6837
-(defun pg-pgip-process-prefval 193,7539
-(defun pg-pgip-process-guiconfig 220,8248
-(defvar proof-assistant-idtables 227,8365
-(defun pg-pgip-process-ids 230,8482
-(defun pg-complete-idtable-symbol 256,9554
-(defalias 'pg-pgip-process-setids pg-pgip-process-setids
261,9646
-(defalias 'pg-pgip-process-addids pg-pgip-process-addids
262,9702
-(defalias 'pg-pgip-process-delids pg-pgip-process-delids
263,9758
-(defun pg-pgip-process-idvalue 266,9816
-(defun pg-pgip-process-menuadd 278,10152
-(defun pg-pgip-process-menudel 281,10195
-(defun pg-pgip-process-ready 290,10428
-(defun pg-pgip-process-cleardisplay 293,10469
-(defun pg-pgip-process-proofstate 307,10926
-(defun pg-pgip-process-normalresponse 311,11003
-(defun pg-pgip-process-errorresponse 315,11127
-(defun pg-pgip-process-scriptinsert 319,11250
-(defun pg-pgip-process-metainforesponse 324,11384
-(defun pg-pgip-process-informfileloaded 333,11625
-(defun pg-pgip-process-informfileretracted 339,11891
-(defun pg-pgip-process-brokerstatus 352,12368
-(defun pg-pgip-process-proveravailmsg 355,12416
-(defun pg-pgip-process-newprovermsg 358,12466
-(defun pg-pgip-process-proverstatusmsg 361,12514
-(defvar pg-pgip-srcids 370,12761
-(defun pg-pgip-process-newfile 374,12868
-(defun pg-pgip-process-filestatus 390,13456
-(defun pg-pgip-process-newobj 410,14111
-(defun pg-pgip-process-delobj 413,14153
-(defun pg-pgip-process-objectstatus 416,14195
-(defun pg-pgip-process-parsescript 430,14550
-(defun pg-pgip-get-pgiptype 453,15425
-(defun pg-pgip-default-for 473,16218
-(defun pg-pgip-subst-for 486,16613
-(defun pg-pgip-interpret-value 498,16956
-(defun pg-pgip-interpret-choice 516,17641
-(defun pg-pgip-string-of-command 547,18658
-(defconst pg-pgip-id564,19419
-(defvar pg-pgip-refseq 570,19699
-(defvar pg-pgip-refid 572,19796
-(defvar pg-pgip-seq 575,19888
-(defun pg-pgip-assemble-packet 577,19952
-(defun pg-pgip-issue 595,20764
-(defun pg-pgip-maybe-askpgip 612,21376
-(defun pg-pgip-askprefs 618,21567
-(defun pg-pgip-askids 622,21681
-(defun pg-pgip-reset 635,21969
-(defconst pg-pgip-start-element-regexp 666,22667
-(defconst pg-pgip-end-element-regexp 667,22719
+(defun proof-goals-config-done 70,1858
+(defun pg-goals-display 78,2124
+(defun pg-goals-button-action 119,3428
+
+generic/pg-pbrpm.el,1804
+(defvar pg-pbrpm-use-buffer-menu 29,720
+(defvar pg-pbrpm-start-goal-regexp 32,842
+(defvar pg-pbrpm-start-goal-regexp-par-num 36,999
+(defvar pg-pbrpm-end-goal-regexp 39,1122
+(defvar pg-pbrpm-start-hyp-regexp 43,1274
+(defvar pg-pbrpm-start-hyp-regexp-par-num 47,1435
+(defvar pg-pbrpm-start-concl-regexp 51,1642
+(defvar pg-pbrpm-auto-select-regexp 55,1806
+(defvar pg-pbrpm-buffer-menu 62,1967
+(defvar pg-pbrpm-spans 63,2001
+(defvar pg-pbrpm-goal-description 64,2029
+(defvar pg-pbrpm-windows-dialog-bug 65,2068
+(defvar pbrpm-menu-desc 66,2109
+(defun pg-pbrpm-erase-buffer-menu 68,2139
+(defun pg-pbrpm-menu-change-hook 75,2323
+(defun pg-pbrpm-create-reset-buffer-menu 93,2898
+(defun pg-pbrpm-analyse-goal-buffer 110,3643
+(defun pg-pbrpm-button-action 170,6041
+(defun pg-pbrpm-exists 177,6267
+(defun pg-pbrpm-eliminate-id 181,6379
+(defun pg-pbrpm-build-menu 189,6625
+(defun pg-pbrpm-setup-span 252,8945
+(defun pg-pbrpm-run-command 312,11260
+(defun pg-pbrpm-get-pos-info 341,12570
+(defun pg-pbrpm-get-region-info 383,13869
+(defun pg-pbrpm-auto-select-around-point 394,14281
+(defun pg-pbrpm-translate-position 409,14805
+(defun pg-pbrpm-process-click 417,15062
+(defvar pg-pbrpm-remember-region-selected-region 437,16087
+(defvar pg-pbrpm-regions-list 438,16141
+(defun pg-pbrpm-erase-regions-list 440,16177
+(defun pg-pbrpm-filter-regions-list 449,16485
+(defface pg-pbrpm-multiple-selection-face456,16748
+(defface pg-pbrpm-menu-input-face464,16950
+(defun pg-pbrpm-do-remember-region 472,17140
+(defun pg-pbrpm-remember-region-drag-up-hook 493,17988
+(defun pg-pbrpm-remember-region-click-hook 497,18159
+(defun pg-pbrpm-remember-region 502,18344
+(defun pg-pbrpm-process-region 516,19058
+(defun pg-pbrpm-process-regions-list 534,19787
+(defun pg-pbrpm-region-expression 538,19970
+
+generic/pg-pgip.el,2927
+(defalias 'pg-pgip-debug pg-pgip-debug
35,913
+(defalias 'pg-pgip-error pg-pgip-error
36,954
+(defalias 'pg-pgip-warning pg-pgip-warning
37,989
+(defconst pg-pgip-version-supported 39,1039
+(defun pg-pgip-process-packet 43,1145
+(defvar pg-pgip-last-seen-id 53,1713
+(defvar pg-pgip-last-seen-seq 54,1747
+(defun pg-pgip-process-pgip 56,1783
+(defun pg-pgip-process-msg 75,2714
+(defvar pg-pgip-post-process-functions89,3284
+(defun pg-pgip-post-process 99,3772
+(defun pg-pgip-process-askpgip 115,4382
+(defun pg-pgip-process-usespgip 121,4586
+(defun pg-pgip-process-usespgml 125,4750
+(defun pg-pgip-process-pgmlconfig 129,4914
+(defun pg-pgip-process-proverinfo 145,5531
+(defun pg-pgip-process-hasprefs 162,6196
+(defun pg-pgip-haspref 176,6828
+(defun pg-pgip-process-prefval 193,7530
+(defun pg-pgip-process-guiconfig 220,8238
+(defvar proof-assistant-idtables 227,8355
+(defun pg-pgip-process-ids 230,8472
+(defun pg-complete-idtable-symbol 256,9544
+(defalias 'pg-pgip-process-setids pg-pgip-process-setids
261,9636
+(defalias 'pg-pgip-process-addids pg-pgip-process-addids
262,9692
+(defalias 'pg-pgip-process-delids pg-pgip-process-delids
263,9748
+(defun pg-pgip-process-idvalue 266,9806
+(defun pg-pgip-process-menuadd 278,10142
+(defun pg-pgip-process-menudel 281,10185
+(defun pg-pgip-process-ready 290,10417
+(defun pg-pgip-process-cleardisplay 293,10458
+(defun pg-pgip-process-proofstate 307,10915
+(defun pg-pgip-process-normalresponse 311,10992
+(defun pg-pgip-process-errorresponse 315,11116
+(defun pg-pgip-process-scriptinsert 319,11239
+(defun pg-pgip-process-metainforesponse 324,11373
+(defun pg-pgip-file-of-url 333,11613
+(defun pg-pgip-process-informfileloaded 338,11748
+(defun pg-pgip-process-informfileretracted 344,11980
+(defun pg-pgip-process-brokerstatus 357,12431
+(defun pg-pgip-process-proveravailmsg 360,12479
+(defun pg-pgip-process-newprovermsg 363,12529
+(defun pg-pgip-process-proverstatusmsg 366,12577
+(defvar pg-pgip-srcids 375,12823
+(defun pg-pgip-process-newfile 379,12930
+(defun pg-pgip-process-filestatus 395,13512
+(defun pg-pgip-process-newobj 415,14166
+(defun pg-pgip-process-delobj 418,14208
+(defun pg-pgip-process-objectstatus 421,14250
+(defun pg-pgip-process-parsescript 435,14602
+(defun pg-pgip-get-pgiptype 458,15476
+(defun pg-pgip-default-for 478,16268
+(defun pg-pgip-subst-for 491,16663
+(defun pg-pgip-interpret-value 503,17006
+(defun pg-pgip-interpret-choice 521,17687
+(defun pg-pgip-string-of-command 552,18704
+(defconst pg-pgip-id569,19465
+(defvar pg-pgip-refseq 575,19745
+(defvar pg-pgip-refid 577,19842
+(defvar pg-pgip-seq 580,19934
+(defun pg-pgip-assemble-packet 582,19998
+(defun pg-pgip-issue 600,20809
+(defun pg-pgip-maybe-askpgip 617,21421
+(defun pg-pgip-askprefs 623,21612
+(defun pg-pgip-askids 627,21726
+(defun pg-pgip-reset 640,22014
+(defconst pg-pgip-start-element-regexp 671,22712
+(defconst pg-pgip-end-element-regexp 672,22764
 
 generic/pg-response.el,1214
-(deflocal pg-response-eagerly-raise 31,731
-(define-derived-mode proof-response-mode 41,956
-(define-key proof-response-mode-map 68,1882
-(define-key proof-response-mode-map 69,1953
-(define-key proof-response-mode-map 70,2007
-(defun proof-response-config-done 74,2093
-(defvar pg-response-special-display-regexp 85,2440
-(defconst proof-multiframe-parameters89,2607
-(defun proof-multiple-frames-enable 98,2906
-(defun proof-three-window-enable 108,3235
-(defun proof-select-three-b 111,3298
-(defun proof-display-three-b 126,3767
-(defvar pg-frame-configuration 138,4176
-(defun pg-cache-frame-configuration 142,4323
-(defun proof-layout-windows 146,4494
-(defun proof-delete-other-frames 186,6281
-(defvar pg-response-erase-flag 217,7371
-(defun pg-response-maybe-erase221,7500
-(defun pg-response-display 252,8685
-(defun pg-response-display-with-face 277,9472
-(defun pg-response-clear-displays 307,10398
-(defun proof-next-error 326,10985
-(defun pg-response-has-error-location 407,13901
-(defvar proof-trace-last-fontify-pos 430,14734
-(defun proof-trace-fontify-pos 432,14777
-(defun proof-trace-buffer-display 440,15090
-(defun proof-trace-buffer-finish 465,16036
-(defun pg-thms-buffer-clear 487,16607
+(deflocal pg-response-eagerly-raise 31,729
+(define-derived-mode proof-response-mode 41,954
+(define-key proof-response-mode-map 68,1880
+(define-key proof-response-mode-map 69,1951
+(define-key proof-response-mode-map 70,2005
+(defun proof-response-config-done 74,2091
+(defvar pg-response-special-display-regexp 85,2437
+(defconst proof-multiframe-parameters89,2604
+(defun proof-multiple-frames-enable 98,2903
+(defun proof-three-window-enable 108,3231
+(defun proof-select-three-b 111,3294
+(defun proof-display-three-b 126,3763
+(defvar pg-frame-configuration 138,4169
+(defun pg-cache-frame-configuration 142,4316
+(defun proof-layout-windows 146,4487
+(defun proof-delete-other-frames 186,6274
+(defvar pg-response-erase-flag 217,7362
+(defun pg-response-maybe-erase221,7491
+(defun pg-response-display 251,8587
+(defun pg-response-display-with-face 276,9370
+(defun pg-response-clear-displays 306,10292
+(defun proof-next-error 325,10879
+(defun pg-response-has-error-location 406,13795
+(defvar proof-trace-last-fontify-pos 429,14627
+(defun proof-trace-fontify-pos 431,14670
+(defun proof-trace-buffer-display 439,14983
+(defun proof-trace-buffer-finish 464,15923
+(defun pg-thms-buffer-clear 486,16490
 
 generic/pg-thymodes.el,152
-(defmacro pg-defthymode 23,500
-(defmacro pg-do-unless-null 71,2311
-(defun pg-symval 76,2398
-(defun pg-modesym 82,2553
-(defun pg-modesymval 86,2667
-
-generic/pg-user.el,3221
-(defun proof-maybe-follow-locked-end 32,793
-(defun proof-assert-next-command-interactive 53,1412
-(defun proof-process-buffer 63,1777
-(defun proof-undo-last-successful-command 77,2088
-(defun proof-undo-and-delete-last-successful-command 82,2250
-(defun proof-undo-last-successful-command-1 96,2813
-(defun proof-retract-buffer 113,3426
-(defun proof-retract-current-goal 122,3710
-(defun proof-goto-command-start 141,4271
-(defun proof-goto-command-end 164,5211
-(defun proof-mouse-goto-point 181,5592
-(defvar proof-minibuffer-history 196,5870
-(defun proof-minibuffer-cmd 199,5965
-(defun proof-frob-locked-end 243,7580
-(defmacro proof-if-setting-configured 304,9508
-(defmacro proof-define-assistant-command 312,9777
-(defmacro proof-define-assistant-command-witharg 325,10232
-(defun proof-issue-new-command 345,11055
-(defun proof-cd-sync 389,12498
-(defun proof-electric-terminator-enable 443,14218
-(defun proof-electric-term-incomment-fn 451,14520
-(defun proof-process-electric-terminator 471,15307
-(defun proof-electric-terminator 496,16372
-(defun proof-add-completions 518,17018
-(defun proof-script-complete 542,17878
-(defun pg-insert-last-output-as-comment 556,18264
-(defun pg-copy-span-contents 570,18662
-(defun pg-numth-span-higher-or-lower 587,19220
-(defun pg-control-span-of 613,19966
-(defun pg-move-span-contents 619,20170
-(defun pg-fixup-children-spans 671,22346
-(defun pg-move-region-down 681,22609
-(defun pg-move-region-up 690,22902
-(defun proof-forward-command 720,23740
-(defun proof-backward-command 741,24461
-(defun pg-pos-for-event 763,24812
-(defun pg-span-for-event 769,25033
-(defun pg-span-context-menu 773,25177
-(defun pg-toggle-visibility 788,25632
-(defun pg-create-in-span-context-menu 798,25954
-(defun pg-span-undo 828,27163
-(defun pg-goals-buffers-hint 874,28573
-(defun pg-slow-fontify-tracing-hint 878,28755
-(defun pg-response-buffers-hint 882,28926
-(defun pg-jump-to-end-hint 892,29288
-(defun pg-processing-complete-hint 896,29419
-(defun pg-next-error-hint 913,30118
-(defun pg-hint 918,30270
-(defun pg-identifier-under-mouse-query 934,30860
-(defun pg-identifier-near-point-query 943,31103
-(defvar proof-query-identifier-collection 968,31835
-(defvar proof-query-identifier-history 969,31882
-(defun proof-query-identifier 971,31927
-(defun pg-identifier-query 981,32197
-(defun proof-imenu-enable 1012,33275
-(defvar pg-input-ring 1043,34321
-(defvar pg-input-ring-index 1046,34378
-(defvar pg-stored-incomplete-input 1049,34450
-(defun pg-previous-input 1052,34553
-(defun pg-next-input 1066,35010
-(defun pg-delete-input 1071,35132
-(defun pg-get-old-input 1084,35470
-(defun pg-restore-input 1098,35861
-(defun pg-search-start 1109,36151
-(defun pg-regexp-arg 1121,36643
-(defun pg-search-arg 1133,37091
-(defun pg-previous-matching-input-string-position 1147,37508
-(defun pg-previous-matching-input 1174,38673
-(defun pg-next-matching-input 1193,39523
-(defvar pg-matching-input-from-input-string 1201,39906
-(defun pg-previous-matching-input-from-input 1205,40020
-(defun pg-next-matching-input-from-input 1223,40785
-(defun pg-add-to-input-history 1234,41164
-(defun pg-remove-from-input-history 1246,41617
-(defun  pg-clear-input-ring 1257,41999
+(defmacro pg-defthymode 23,499
+(defmacro pg-do-unless-null 71,2310
+(defun pg-symval 76,2393
+(defun pg-modesym 82,2548
+(defun pg-modesymval 86,2662
+
+generic/pg-user.el,3486
+(defun proof-script-next-command-advance 31,762
+(defun proof-script-new-command-advance 43,1226
+(defun proof-maybe-follow-locked-end 86,2968
+(defun proof-goto-point 110,3737
+(defun proof-assert-next-command-interactive 124,4171
+(defun proof-assert-until-point-interactive 137,4696
+(defun proof-process-buffer 143,4926
+(defun proof-undo-last-successful-command 158,5303
+(defun proof-undo-and-delete-last-successful-command 163,5465
+(defun proof-undo-last-successful-command-1 176,6019
+(defun proof-retract-buffer 193,6631
+(defun proof-retract-current-goal 202,6915
+(defun proof-goto-command-start 221,7476
+(defun proof-goto-command-end 244,8416
+(defun proof-mouse-goto-point 264,8865
+(defvar proof-minibuffer-history 279,9141
+(defun proof-minibuffer-cmd 282,9236
+(defun proof-frob-locked-end 326,10858
+(defmacro proof-if-setting-configured 387,12782
+(defmacro proof-define-assistant-command 395,13051
+(defmacro proof-define-assistant-command-witharg 408,13506
+(defun proof-issue-new-command 428,14328
+(defun proof-cd-sync 474,15825
+(defun proof-electric-terminator-enable 528,17545
+(defun proof-process-electric-terminator 536,17835
+(defun proof-electric-terminator 571,19174
+(defun proof-add-completions 593,19820
+(defun proof-script-complete 617,20680
+(defun pg-insert-last-output-as-comment 631,21066
+(defun pg-copy-span-contents 645,21464
+(defun pg-numth-span-higher-or-lower 662,22022
+(defun pg-control-span-of 688,22768
+(defun pg-move-span-contents 694,22972
+(defun pg-fixup-children-spans 746,25148
+(defun pg-move-region-down 756,25405
+(defun pg-move-region-up 765,25698
+(defun proof-forward-command 795,26526
+(defun proof-backward-command 816,27247
+(defun pg-pos-for-event 838,27591
+(defun pg-span-for-event 844,27812
+(defun pg-span-context-menu 848,27956
+(defun pg-toggle-visibility 863,28411
+(defun pg-create-in-span-context-menu 873,28733
+(defun pg-span-undo 903,29942
+(defun pg-goals-buffers-hint 949,31344
+(defun pg-slow-fontify-tracing-hint 953,31526
+(defun pg-response-buffers-hint 957,31697
+(defun pg-jump-to-end-hint 967,32059
+(defun pg-processing-complete-hint 971,32188
+(defun pg-next-error-hint 988,32887
+(defun pg-hint 993,33039
+(defun pg-identifier-under-mouse-query 1009,33629
+(defun pg-identifier-near-point-query 1018,33872
+(defvar proof-query-identifier-collection 1043,34588
+(defvar proof-query-identifier-history 1044,34635
+(defun proof-query-identifier 1046,34680
+(defun pg-identifier-query 1056,34949
+(defun proof-imenu-enable 1087,36027
+(defvar pg-input-ring 1118,37088
+(defvar pg-input-ring-index 1121,37145
+(defvar pg-stored-incomplete-input 1124,37217
+(defun pg-previous-input 1127,37320
+(defun pg-next-input 1141,37777
+(defun pg-delete-input 1146,37899
+(defun pg-get-old-input 1159,38237
+(defun pg-restore-input 1173,38628
+(defun pg-search-start 1184,38918
+(defun pg-regexp-arg 1196,39410
+(defun pg-search-arg 1208,39858
+(defun pg-previous-matching-input-string-position 1222,40275
+(defun pg-previous-matching-input 1249,41440
+(defun pg-next-matching-input 1268,42290
+(defvar pg-matching-input-from-input-string 1276,42673
+(defun pg-previous-matching-input-from-input 1280,42787
+(defun pg-next-matching-input-from-input 1298,43552
+(defun pg-add-to-input-history 1309,43931
+(defun pg-remove-from-input-history 1321,44384
+(defun  pg-clear-input-ring 1332,44764
+(define-key proof-mode-map 1346,45114
+(define-key proof-mode-map 1347,45174
+(defun pg-protected-undo 1349,45246
 
 generic/pg-vars.el,1326
-(defvar proof-assistant-cusgrp 22,383
-(defvar proof-assistant-internals-cusgrp 28,645
-(defvar proof-assistant 34,916
-(defvar proof-assistant-symbol 39,1138
-(defvar proof-mode-for-shell 52,1682
-(defvar proof-mode-for-response 57,1874
-(defvar proof-mode-for-goals 62,2101
-(defvar proof-mode-for-script 67,2291
-(defvar proof-ready-for-assistant-hook 72,2469
-(defvar proof-shell-busy 83,2758
-(defvar proof-included-files-list 88,2914
-(defvar proof-script-buffer 110,3927
-(defvar proof-previous-script-buffer 113,4019
-(defvar proof-shell-buffer 117,4190
-(defvar proof-goals-buffer 120,4276
-(defvar proof-response-buffer 123,4331
-(defvar proof-trace-buffer 126,4392
-(defvar proof-thms-buffer 130,4546
-(defvar proof-shell-error-or-interrupt-seen 134,4701
-(defvar proof-shell-interrupt-pending 139,4925
-(defvar pg-response-next-error 143,5091
-(defvar proof-shell-proof-completed 146,5198
-(defvar proof-terminal-string 158,5742
-(defvar proof-shell-last-output 169,5934
-(defvar proof-assistant-settings 173,6075
-(defvar pg-tracing-slow-mode 181,6524
-(defvar proof-nesting-depth 184,6613
-(defvar proof-last-theorem-dependencies 191,6848
-(defcustom proof-general-name 200,7084
-(defcustom proof-general-home-page205,7241
-(defcustom proof-unnamed-theorem-name211,7401
-(defcustom proof-universal-keys217,7585
-
-generic/pg-xml.el,1140
+(defvar proof-assistant-cusgrp 22,382
+(defvar proof-assistant-internals-cusgrp 28,642
+(defvar proof-assistant 34,912
+(defvar proof-assistant-symbol 39,1133
+(defvar proof-mode-for-shell 52,1675
+(defvar proof-mode-for-response 57,1865
+(defvar proof-mode-for-goals 62,2091
+(defvar proof-mode-for-script 67,2280
+(defvar proof-ready-for-assistant-hook 72,2457
+(defvar proof-shell-busy 83,2745
+(defvar proof-included-files-list 88,2901
+(defvar proof-script-buffer 110,3914
+(defvar proof-previous-script-buffer 113,4006
+(defvar proof-shell-buffer 117,4177
+(defvar proof-goals-buffer 120,4263
+(defvar proof-response-buffer 123,4318
+(defvar proof-trace-buffer 126,4379
+(defvar proof-thms-buffer 130,4533
+(defvar proof-shell-error-or-interrupt-seen 134,4688
+(defvar proof-shell-interrupt-pending 139,4912
+(defvar pg-response-next-error 143,5078
+(defvar proof-shell-proof-completed 146,5185
+(defvar proof-terminal-string 158,5729
+(defvar proof-shell-last-output 169,5920
+(defvar proof-assistant-settings 173,6060
+(defvar pg-tracing-slow-mode 181,6508
+(defvar proof-nesting-depth 184,6597
+(defvar proof-last-theorem-dependencies 191,6832
+(defcustom proof-general-name 200,7068
+(defcustom proof-general-home-page205,7225
+(defcustom proof-unnamed-theorem-name211,7385
+(defcustom proof-universal-keys217,7569
+
+generic/pg-xml.el,1177
 (defalias 'pg-xml-error pg-xml-error
16,366
 (defun pg-xml-parse-string 39,1008
 (defun pg-xml-parse-buffer 50,1334
-(defun pg-xml-get-attr 72,2067
-(defun pg-xml-child-elts 80,2369
-(defun pg-xml-child-elt 85,2574
-(defun pg-xml-get-child 93,2856
-(defun pg-xml-get-text-content 103,3228
-(defmacro pg-xml-attr 114,3578
-(defmacro pg-xml-node 116,3640
-(defconst pg-xml-header119,3732
-(defun pg-xml-string-of 123,3808
-(defun pg-xml-output-internal 134,4175
-(defun pg-xml-cdata 168,5325
-(defun pg-pgip-get-icon 176,5518
-(defsubst pg-pgip-get-name 180,5666
-(defsubst pg-pgip-get-version 183,5783
-(defsubst pg-pgip-get-descr 186,5906
-(defsubst pg-pgip-get-thmname 189,6025
-(defsubst pg-pgip-get-thyname 192,6148
-(defsubst pg-pgip-get-url 195,6271
-(defsubst pg-pgip-get-srcid 198,6386
-(defsubst pg-pgip-get-proverid 201,6505
-(defsubst pg-pgip-get-symname 204,6630
-(defsubst pg-pgip-get-prefcat 207,6750
-(defsubst pg-pgip-get-default 210,6878
-(defsubst pg-pgip-get-objtype 213,7001
-(defsubst pg-pgip-get-value 216,7124
-(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext
219,7194
-(defun pg-pgip-get-pgmltext 221,7253
+(defun pg-xml-get-attr 69,1949
+(defun pg-xml-child-elts 77,2251
+(defun pg-xml-child-elt 82,2456
+(defun pg-xml-get-child 90,2738
+(defun pg-xml-get-text-content 100,3105
+(defmacro pg-xml-attr 111,3455
+(defmacro pg-xml-node 113,3517
+(defconst pg-xml-header116,3609
+(defun pg-xml-string-of 120,3685
+(defun pg-xml-output-internal 131,4052
+(defun pg-xml-cdata 165,5191
+(defsubst pg-pgip-get-area 173,5384
+(defun pg-pgip-get-icon 176,5501
+(defsubst pg-pgip-get-name 180,5649
+(defsubst pg-pgip-get-version 183,5766
+(defsubst pg-pgip-get-descr 186,5889
+(defsubst pg-pgip-get-thmname 189,6008
+(defsubst pg-pgip-get-thyname 192,6131
+(defsubst pg-pgip-get-url 195,6254
+(defsubst pg-pgip-get-srcid 198,6369
+(defsubst pg-pgip-get-proverid 201,6488
+(defsubst pg-pgip-get-symname 204,6613
+(defsubst pg-pgip-get-prefcat 207,6733
+(defsubst pg-pgip-get-default 210,6861
+(defsubst pg-pgip-get-objtype 213,6984
+(defsubst pg-pgip-get-value 216,7107
+(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext
219,7177
+(defun pg-pgip-get-pgmltext 221,7236
+
+generic/proof-autoloads.el,45
+(defsubst proof-shell-live-buffer 618,20501
 
 generic/proof-auxmodes.el,149
-(defun proof-mmm-support-available 21,550
-(defun proof-maths-menu-support-available 45,1168
-(defun proof-unicode-tokens-support-available 59,1586
-
-generic/proof-config.el,7974
-(defgroup prover-config 79,2604
-(defcustom proof-guess-command-line 99,3456
-(defcustom proof-assistant-home-page 114,3951
-(defcustom proof-context-command 120,4121
-(defcustom proof-info-command 125,4255
-(defcustom proof-showproof-command 132,4526
-(defcustom proof-goal-command 137,4662
-(defcustom proof-save-command 145,4959
-(defcustom proof-find-theorems-command 153,5268
-(defcustom proof-query-identifier-command 160,5576
-(defcustom proof-assistant-true-value 174,6265
-(defcustom proof-assistant-false-value 180,6455
-(defcustom proof-assistant-format-int-fn 186,6649
-(defcustom proof-assistant-format-string-fn 193,6898
-(defcustom proof-assistant-setting-format 200,7165
-(defgroup proof-script 222,7860
-(defcustom proof-terminal-char 227,7990
-(defcustom proof-electric-terminator-noterminator 237,8377
-(defcustom proof-script-sexp-commands 242,8549
-(defcustom proof-script-command-end-regexp 253,9006
-(defcustom proof-script-command-start-regexp 271,9825
-(defcustom proof-script-use-old-parser 282,10286
-(defcustom proof-script-integral-proofs 294,10772
-(defcustom proof-script-fly-past-comments 309,11428
-(defcustom proof-script-parse-function 314,11599
-(defcustom proof-script-comment-start 332,12242
-(defcustom proof-script-comment-start-regexp 343,12679
-(defcustom proof-script-comment-end 351,12998
-(defcustom proof-script-comment-end-regexp 363,13420
-(defcustom proof-string-start-regexp 371,13731
-(defcustom proof-string-end-regexp 376,13896
-(defcustom proof-case-fold-search 381,14057
-(defcustom proof-save-command-regexp 390,14469
-(defcustom proof-save-with-hole-regexp 395,14579
-(defcustom proof-save-with-hole-result 407,15033
-(defcustom proof-goal-command-regexp 417,15481
-(defcustom proof-goal-with-hole-regexp 426,15869
-(defcustom proof-goal-with-hole-result 438,16312
-(defcustom proof-non-undoables-regexp 447,16696
-(defcustom proof-nested-undo-regexp 458,17151
-(defcustom proof-ignore-for-undo-count 474,17863
-(defcustom proof-script-next-entity-regexps 482,18166
-(defcustom proof-script-find-next-entity-fn526,19907
-(defcustom proof-script-imenu-generic-expression 546,20747
-(defcustom proof-goal-command-p 554,21086
-(defcustom proof-really-save-command-p 565,21577
-(defcustom proof-completed-proof-behaviour 574,21884
-(defcustom proof-count-undos-fn 602,23240
-(defconst proof-no-command 614,23789
-(defcustom proof-find-and-forget-fn 619,23996
-(defcustom proof-forget-id-command 636,24710
-(defcustom pg-topterm-goalhyplit-fn 646,25068
-(defcustom proof-kill-goal-command 658,25603
-(defcustom proof-undo-n-times-cmd 672,26106
-(defcustom proof-nested-goals-history-p 686,26654
-(defcustom proof-state-preserving-p 695,26991
-(defcustom proof-activate-scripting-hook 705,27463
-(defcustom proof-deactivate-scripting-hook 724,28244
-(defcustom proof-indent 737,28609
-(defcustom proof-indent-hang 742,28716
-(defcustom proof-indent-enclose-offset 747,28842
-(defcustom proof-indent-open-offset 752,28984
-(defcustom proof-indent-close-offset 757,29121
-(defcustom proof-indent-any-regexp 762,29259
-(defcustom proof-indent-inner-regexp 767,29419
-(defcustom proof-indent-enclose-regexp 772,29573
-(defcustom proof-indent-open-regexp 777,29727
-(defcustom proof-indent-close-regexp 782,29879
-(defcustom proof-script-font-lock-keywords 788,30033
-(defcustom proof-script-syntax-table-entries 796,30385
-(defcustom proof-script-span-context-menu-extensions 814,30782
-(defgroup proof-shell 840,31542
-(defcustom proof-prog-name 850,31713
-(defcustom proof-shell-auto-terminate-commands 861,32133
-(defcustom proof-shell-pre-sync-init-cmd 870,32534
-(defcustom proof-shell-init-cmd 884,33092
-(defcustom proof-shell-init-hook 896,33621
-(defcustom proof-shell-restart-cmd 901,33760
-(defcustom proof-shell-quit-cmd 906,33915
-(defcustom proof-shell-quit-timeout 911,34082
-(defcustom proof-shell-cd-cmd 921,34532
-(defcustom proof-shell-start-silent-cmd 938,35203
-(defcustom proof-shell-stop-silent-cmd 947,35579
-(defcustom proof-shell-silent-threshold 956,35914
-(defcustom  proof-shell-inform-file-processed-cmd 964,36248
-(defcustom  proof-shell-inform-file-retracted-cmd 985,37176
-(defcustom proof-auto-multiple-files 1013,38448
-(defcustom proof-cannot-reopen-processed-files 1028,39169
-(defcustom proof-shell-require-command-regexp 1042,39835
-(defcustom proof-done-advancing-require-function 1053,40297
-(defcustom proof-shell-quiet-errors 1059,40532
-(defcustom proof-shell-prompt-pattern 1072,40866
-(defcustom proof-shell-wakeup-char 1082,41287
-(defcustom proof-shell-annotated-prompt-regexp 1088,41518
-(defcustom proof-shell-abort-goal-regexp 1104,42154
-(defcustom proof-shell-error-regexp 1109,42289
-(defcustom proof-shell-truncate-before-error 1129,43089
-(defcustom pg-next-error-regexp 1143,43628
-(defcustom pg-next-error-filename-regexp 1158,44237
-(defcustom pg-next-error-extract-filename 1182,45270
-(defcustom proof-shell-interrupt-regexp 1189,45513
-(defcustom proof-shell-proof-completed-regexp 1203,46108
-(defcustom proof-shell-clear-response-regexp 1216,46616
-(defcustom proof-shell-clear-goals-regexp 1223,46915
-(defcustom proof-shell-start-goals-regexp 1230,47208
-(defcustom proof-shell-end-goals-regexp 1238,47575
-(defcustom proof-shell-eager-annotation-start 1244,47819
-(defcustom proof-shell-eager-annotation-start-length 1267,48838
-(defcustom proof-shell-eager-annotation-end 1278,49264
-(defcustom proof-shell-strip-output-markup 1294,49939
-(defcustom proof-shell-assumption-regexp 1303,50325
-(defcustom proof-shell-process-file 1313,50729
-(defcustom proof-shell-retract-files-regexp 1335,51685
-(defcustom proof-shell-compute-new-files-list 1344,52021
-(defcustom pg-use-specials-for-fontify 1356,52569
-(defcustom pg-special-char-regexp 1364,52917
-(defcustom proof-shell-set-elisp-variable-regexp 1370,53062
-(defcustom proof-shell-match-pgip-cmd 1403,54575
-(defcustom proof-shell-issue-pgip-cmd 1412,54904
-(defcustom proof-use-pgip-askprefs 1417,55069
-(defcustom proof-shell-query-dependencies-cmd 1425,55416
-(defcustom proof-shell-theorem-dependency-list-regexp 1432,55676
-(defcustom proof-shell-theorem-dependency-list-split 1448,56336
-(defcustom proof-shell-show-dependency-cmd 1457,56759
-(defcustom proof-shell-trace-output-regexp 1479,57665
-(defcustom proof-shell-thms-output-regexp 1493,58123
-(defcustom proof-tokens-activate-command 1506,58506
-(defcustom proof-tokens-deactivate-command 1513,58747
-(defcustom proof-tokens-extra-modes 1520,58994
-(defcustom proof-shell-unicode 1535,59501
-(defcustom proof-shell-filename-escapes 1543,59821
-(defcustom proof-shell-process-connection-type1560,60501
-(defcustom proof-shell-strip-crs-from-input 1583,61547
-(defcustom proof-shell-strip-crs-from-output 1595,62032
-(defcustom proof-shell-insert-hook 1603,62400
-(defcustom proof-shell-handle-delayed-output-hook1641,64260
-(defcustom proof-shell-handle-error-or-interrupt-hook1647,64475
-(defcustom proof-shell-pre-interrupt-hook1665,65228
-(defcustom proof-shell-classify-output-system-specific 1673,65499
-(defcustom proof-state-change-hook 1692,66367
-(defcustom proof-shell-syntax-table-entries 1702,66748
-(defgroup proof-goals 1720,67120
-(defcustom pg-subterm-first-special-char 1725,67241
-(defcustom pg-subterm-anns-use-stack 1733,67553
-(defcustom pg-goals-change-goal 1742,67852
-(defcustom pbp-goal-command 1747,67968
-(defcustom pbp-hyp-command 1752,68124
-(defcustom pg-subterm-help-cmd 1757,68286
-(defcustom pg-goals-error-regexp 1764,68522
-(defcustom proof-shell-result-start 1769,68682
-(defcustom proof-shell-result-end 1775,68916
-(defcustom pg-subterm-start-char 1781,69129
-(defcustom pg-subterm-sep-char 1795,69715
-(defcustom pg-subterm-end-char 1801,69894
-(defcustom pg-topterm-regexp 1807,70051
-(defcustom proof-goals-font-lock-keywords 1822,70651
-(defcustom proof-response-font-lock-keywords 1830,71010
-(defcustom pg-before-fontify-output-hook 1838,71372
-(defcustom pg-after-fontify-output-hook 1846,71733
+(defun proof-mmm-support-available 21,549
+(defun proof-maths-menu-support-available 45,1160
+(defun proof-unicode-tokens-support-available 59,1577
+
+generic/proof-config.el,7853
+(defgroup prover-config 79,2594
+(defcustom proof-guess-command-line 97,3444
+(defcustom proof-assistant-home-page 112,3939
+(defcustom proof-context-command 118,4109
+(defcustom proof-info-command 123,4243
+(defcustom proof-showproof-command 130,4514
+(defcustom proof-goal-command 135,4650
+(defcustom proof-save-command 143,4947
+(defcustom proof-find-theorems-command 151,5256
+(defcustom proof-query-identifier-command 158,5564
+(defcustom proof-assistant-true-value 172,6253
+(defcustom proof-assistant-false-value 178,6443
+(defcustom proof-assistant-format-int-fn 184,6637
+(defcustom proof-assistant-format-string-fn 191,6886
+(defcustom proof-assistant-setting-format 198,7153
+(defgroup proof-script 220,7848
+(defcustom proof-terminal-char 225,7978
+(defcustom proof-electric-terminator-noterminator 235,8365
+(defcustom proof-script-sexp-commands 240,8537
+(defcustom proof-script-command-end-regexp 251,8994
+(defcustom proof-script-command-start-regexp 269,9813
+(defcustom proof-script-use-old-parser 280,10274
+(defcustom proof-script-integral-proofs 292,10760
+(defcustom proof-script-fly-past-comments 307,11416
+(defcustom proof-script-parse-function 312,11587
+(defcustom proof-script-comment-start 330,12230
+(defcustom proof-script-comment-start-regexp 341,12667
+(defcustom proof-script-comment-end 349,12986
+(defcustom proof-script-comment-end-regexp 361,13408
+(defcustom proof-string-start-regexp 369,13719
+(defcustom proof-string-end-regexp 374,13884
+(defcustom proof-case-fold-search 379,14045
+(defcustom proof-save-command-regexp 388,14457
+(defcustom proof-save-with-hole-regexp 393,14567
+(defcustom proof-save-with-hole-result 405,15022
+(defcustom proof-goal-command-regexp 415,15470
+(defcustom proof-goal-with-hole-regexp 424,15858
+(defcustom proof-goal-with-hole-result 436,16301
+(defcustom proof-non-undoables-regexp 445,16685
+(defcustom proof-nested-undo-regexp 456,17140
+(defcustom proof-ignore-for-undo-count 472,17852
+(defcustom proof-script-next-entity-regexps 480,18155
+(defcustom proof-script-find-next-entity-fn524,19896
+(defcustom proof-script-imenu-generic-expression 544,20736
+(defcustom proof-goal-command-p 552,21075
+(defcustom proof-really-save-command-p 563,21566
+(defcustom proof-completed-proof-behaviour 572,21873
+(defcustom proof-count-undos-fn 600,23222
+(defcustom proof-find-and-forget-fn 612,23771
+(defcustom proof-forget-id-command 629,24474
+(defcustom pg-topterm-goalhyplit-fn 639,24832
+(defcustom proof-kill-goal-command 651,25367
+(defcustom proof-undo-n-times-cmd 665,25870
+(defcustom proof-nested-goals-history-p 679,26418
+(defcustom proof-state-preserving-p 688,26755
+(defcustom proof-activate-scripting-hook 698,27227
+(defcustom proof-deactivate-scripting-hook 717,28008
+(defcustom proof-script-evaluate-elisp-comment-regexp 726,28338
+(defcustom proof-indent 744,28924
+(defcustom proof-indent-hang 749,29031
+(defcustom proof-indent-enclose-offset 754,29157
+(defcustom proof-indent-open-offset 759,29299
+(defcustom proof-indent-close-offset 764,29436
+(defcustom proof-indent-any-regexp 769,29574
+(defcustom proof-indent-inner-regexp 774,29734
+(defcustom proof-indent-enclose-regexp 779,29888
+(defcustom proof-indent-open-regexp 784,30042
+(defcustom proof-indent-close-regexp 789,30194
+(defcustom proof-script-font-lock-keywords 795,30348
+(defcustom proof-script-syntax-table-entries 803,30700
+(defcustom proof-script-span-context-menu-extensions 821,31096
+(defgroup proof-shell 847,31854
+(defcustom proof-prog-name 857,32024
+(defcustom proof-shell-auto-terminate-commands 868,32444
+(defcustom proof-shell-pre-sync-init-cmd 877,32845
+(defcustom proof-shell-init-cmd 891,33403
+(defcustom proof-shell-init-hook 903,33932
+(defcustom proof-shell-restart-cmd 908,34071
+(defcustom proof-shell-quit-cmd 913,34226
+(defcustom proof-shell-quit-timeout 918,34393
+(defcustom proof-shell-cd-cmd 928,34843
+(defcustom proof-shell-start-silent-cmd 945,35514
+(defcustom proof-shell-stop-silent-cmd 954,35890
+(defcustom proof-shell-silent-threshold 963,36225
+(defcustom  proof-shell-inform-file-processed-cmd 971,36559
+(defcustom  proof-shell-inform-file-retracted-cmd 992,37487
+(defcustom proof-auto-multiple-files 1020,38759
+(defcustom proof-cannot-reopen-processed-files 1035,39480
+(defcustom proof-shell-require-command-regexp 1049,40146
+(defcustom proof-done-advancing-require-function 1060,40608
+(defcustom proof-shell-quiet-errors 1066,40843
+(defcustom proof-shell-annotated-prompt-regexp 1079,41177
+(defcustom proof-shell-abort-goal-regexp 1094,41742
+(defcustom proof-shell-error-regexp 1099,41877
+(defcustom proof-shell-truncate-before-error 1119,42679
+(defcustom pg-next-error-regexp 1133,43218
+(defcustom pg-next-error-filename-regexp 1148,43827
+(defcustom pg-next-error-extract-filename 1172,44860
+(defcustom proof-shell-interrupt-regexp 1179,45103
+(defcustom proof-shell-proof-completed-regexp 1193,45698
+(defcustom proof-shell-clear-response-regexp 1206,46206
+(defcustom proof-shell-clear-goals-regexp 1218,46658
+(defcustom proof-shell-start-goals-regexp 1230,47104
+(defcustom proof-shell-end-goals-regexp 1238,47471
+(defcustom proof-shell-eager-annotation-start 1252,48046
+(defcustom proof-shell-eager-annotation-start-length 1275,49065
+(defcustom proof-shell-eager-annotation-end 1286,49491
+(defcustom proof-shell-strip-output-markup 1302,50166
+(defcustom proof-shell-assumption-regexp 1311,50551
+(defcustom proof-shell-process-file 1321,50955
+(defcustom proof-shell-retract-files-regexp 1347,52033
+(defcustom proof-shell-compute-new-files-list 1360,52521
+(defcustom pg-special-char-regexp 1375,53090
+(defcustom proof-shell-set-elisp-variable-regexp 1380,53234
+(defcustom proof-shell-match-pgip-cmd 1418,54900
+(defcustom proof-shell-issue-pgip-cmd 1432,55382
+(defcustom proof-use-pgip-askprefs 1437,55547
+(defcustom proof-shell-query-dependencies-cmd 1445,55894
+(defcustom proof-shell-theorem-dependency-list-regexp 1452,56154
+(defcustom proof-shell-theorem-dependency-list-split 1468,56814
+(defcustom proof-shell-show-dependency-cmd 1477,57237
+(defcustom proof-shell-trace-output-regexp 1499,58143
+(defcustom proof-shell-thms-output-regexp 1517,58738
+(defcustom proof-tokens-activate-command 1530,59121
+(defcustom proof-tokens-deactivate-command 1537,59361
+(defcustom proof-tokens-extra-modes 1544,59606
+(defcustom proof-shell-unicode 1559,60111
+(defcustom proof-shell-filename-escapes 1568,60501
+(defcustom proof-shell-process-connection-type1585,61181
+(defcustom proof-shell-strip-crs-from-input 1608,62185
+(defcustom proof-shell-strip-crs-from-output 1620,62668
+(defcustom proof-shell-insert-hook 1628,63036
+(defcustom proof-shell-handle-delayed-output-hook1666,64896
+(defcustom proof-shell-handle-error-or-interrupt-hook1672,65111
+(defcustom proof-shell-pre-interrupt-hook1690,65864
+(defcustom proof-shell-classify-output-system-specific 1698,66135
+(defcustom proof-state-change-hook 1717,67003
+(defcustom proof-shell-syntax-table-entries 1727,67396
+(defgroup proof-goals 1745,67767
+(defcustom pg-subterm-first-special-char 1750,67888
+(defcustom pg-subterm-anns-use-stack 1758,68200
+(defcustom pg-goals-change-goal 1767,68499
+(defcustom pbp-goal-command 1772,68615
+(defcustom pbp-hyp-command 1777,68771
+(defcustom pg-subterm-help-cmd 1782,68933
+(defcustom pg-goals-error-regexp 1789,69169
+(defcustom proof-shell-result-start 1794,69329
+(defcustom proof-shell-result-end 1800,69563
+(defcustom pg-subterm-start-char 1806,69776
+(defcustom pg-subterm-sep-char 1820,70361
+(defcustom pg-subterm-end-char 1826,70540
+(defcustom pg-topterm-regexp 1832,70697
+(defcustom proof-goals-font-lock-keywords 1847,71297
+(defcustom proof-response-font-lock-keywords 1855,71656
+(defcustom pg-before-fontify-output-hook 1863,72018
+(defcustom pg-after-fontify-output-hook 1871,72379
 
 generic/proof-depends.el,824
-(defvar proof-thm-names-of-files 23,625
-(defvar proof-def-names-of-files 29,909
-(defun proof-depends-module-name-for-buffer 38,1213
-(defun proof-depends-module-of 48,1655
-(defun proof-depends-names-in-same-file 56,1949
-(defun proof-depends-process-dependencies 75,2569
-(defun proof-dependency-in-span-context-menu 128,4318
-(defun proof-dep-alldeps-menu 151,5221
-(defun proof-dep-make-alldeps-menu 157,5448
-(defun proof-dep-split-deps 175,5944
-(defun proof-dep-make-submenu 196,6643
-(defun proof-make-highlight-depts-menu 206,6996
-(defun proof-goto-dependency 216,7300
-(defun proof-show-dependency 222,7523
-(defconst pg-dep-span-priority 229,7813
-(defconst pg-ordinary-span-priority 230,7849
-(defun proof-highlight-depcs 232,7891
-(defun proof-highlight-depts 242,8321
-(defun proof-dep-unhighlight 253,8795
+(defvar proof-thm-names-of-files 23,622
+(defvar proof-def-names-of-files 29,906
+(defun proof-depends-module-name-for-buffer 38,1210
+(defun proof-depends-module-of 48,1651
+(defun proof-depends-names-in-same-file 56,1944
+(defun proof-depends-process-dependencies 75,2552
+(defun proof-dependency-in-span-context-menu 128,4287
+(defun proof-dep-alldeps-menu 151,5189
+(defun proof-dep-make-alldeps-menu 157,5415
+(defun proof-dep-split-deps 175,5910
+(defun proof-dep-make-submenu 196,6606
+(defun proof-make-highlight-depts-menu 206,6956
+(defun proof-goto-dependency 216,7259
+(defun proof-show-dependency 222,7482
+(defconst pg-dep-span-priority 229,7771
+(defconst pg-ordinary-span-priority 230,7807
+(defun proof-highlight-depcs 232,7849
+(defun proof-highlight-depts 242,8279
+(defun proof-dep-unhighlight 253,8753
 
 generic/proof-easy-config.el,192
 (defconst proof-easy-config-derived-modes-table16,544
 (defun proof-easy-config-define-derived-modes 23,950
-(defun proof-easy-config-check-setup 52,2133
-(defmacro proof-easy-config 84,3468
+(defun proof-easy-config-check-setup 52,2131
+(defmacro proof-easy-config 84,3461
 
 generic/proof-faces.el,1344
-(defgroup proof-faces 28,748
-(defconst pg-defface-window-systems35,930
-(defmacro proof-face-specs 48,1492
-(defface proof-queue-face63,1944
-(defface proof-locked-face71,2222
-(defface proof-declaration-name-face81,2543
-(defface proof-tacticals-name-face90,2829
-(defface proof-tactics-name-face99,3091
-(defface proof-error-face108,3356
-(defface proof-warning-face116,3546
-(defface proof-eager-annotation-face125,3803
-(defface proof-debug-message-face133,4021
-(defface proof-boring-face141,4220
-(defface proof-mouse-highlight-face149,4412
-(defface proof-highlight-dependent-face157,4608
-(defface proof-highlight-dependency-face165,4817
-(defface proof-active-area-face173,5014
-(defconst proof-face-compat-doc 184,5406
-(defconst proof-queue-face 185,5486
-(defconst proof-locked-face 186,5554
-(defconst proof-declaration-name-face 187,5624
-(defconst proof-tacticals-name-face 188,5714
-(defconst proof-tactics-name-face 189,5800
-(defconst proof-error-face 190,5882
-(defconst proof-warning-face 191,5950
-(defconst proof-eager-annotation-face 192,6022
-(defconst proof-debug-message-face 193,6112
-(defconst proof-boring-face 194,6196
-(defconst proof-mouse-highlight-face 195,6266
-(defconst proof-highlight-dependent-face 196,6354
-(defconst proof-highlight-dependency-face 197,6450
-(defconst proof-active-area-face 198,6548
+(defgroup proof-faces 28,747
+(defconst pg-defface-window-systems35,927
+(defmacro proof-face-specs 48,1489
+(defface proof-queue-face63,1941
+(defface proof-locked-face71,2219
+(defface proof-declaration-name-face81,2540
+(defface proof-tacticals-name-face90,2826
+(defface proof-tactics-name-face99,3088
+(defface proof-error-face108,3353
+(defface proof-warning-face116,3543
+(defface proof-eager-annotation-face125,3800
+(defface proof-debug-message-face133,4018
+(defface proof-boring-face141,4217
+(defface proof-mouse-highlight-face149,4409
+(defface proof-highlight-dependent-face157,4605
+(defface proof-highlight-dependency-face165,4812
+(defface proof-active-area-face173,5009
+(defconst proof-face-compat-doc 184,5401
+(defconst proof-queue-face 185,5481
+(defconst proof-locked-face 186,5549
+(defconst proof-declaration-name-face 187,5619
+(defconst proof-tacticals-name-face 188,5709
+(defconst proof-tactics-name-face 189,5795
+(defconst proof-error-face 190,5877
+(defconst proof-warning-face 191,5945
+(defconst proof-eager-annotation-face 192,6017
+(defconst proof-debug-message-face 193,6107
+(defconst proof-boring-face 194,6191
+(defconst proof-mouse-highlight-face 195,6261
+(defconst proof-highlight-dependent-face 196,6349
+(defconst proof-highlight-dependency-face 197,6445
+(defconst proof-active-area-face 198,6543
 
 generic/proof-indent.el,219
 (defun proof-indent-indent 14,412
 (defun proof-indent-offset 23,678
 (defun proof-indent-inner-p 40,1278
-(defun proof-indent-goto-prev 49,1585
-(defun proof-indent-calculate 56,1918
-(defun proof-indent-line 76,2640
+(defun proof-indent-goto-prev 49,1578
+(defun proof-indent-calculate 56,1911
+(defun proof-indent-line 76,2611
 
 generic/proof-maths-menu.el,83
 (defun proof-maths-menu-set-global 30,959
-(defun proof-maths-menu-enable 44,1415
-
-generic/proof-menu.el,2148
-(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 135,5494
-(defvar proof-menu-favourites 144,5682
-(defun proof-menu-define-specific 148,5804
-(defun proof-assistant-menu-update 191,7013
-(defvar proof-help-menu205,7446
-(defvar proof-show-hide-menu213,7724
-(defvar proof-buffer-menu222,8037
-(defun proof-retract-on-edit-toggle 283,10267
-(defun proof-keep-response-history 290,10445
-(defconst proof-quick-opts-menu298,10755
-(defun proof-quick-opts-vars 465,17706
-(defun proof-quick-opts-changed-from-defaults-p 493,18542
-(defun proof-quick-opts-changed-from-saved-p 497,18647
-(defun proof-quick-opts-save 508,18999
-(defun proof-quick-opts-reset 513,19167
-(defconst proof-config-menu525,19435
-(defconst proof-advanced-menu532,19614
-(defvar proof-menu 545,20049
-(defun proof-main-menu 554,20333
-(defun proof-aux-menu 565,20599
-(defun proof-menu-define-favourites-menu 581,20946
-(defun proof-def-favourite 601,21602
-(defvar proof-make-favourite-cmd-history 624,22577
-(defvar proof-make-favourite-menu-history 627,22662
-(defun proof-save-favourites 630,22748
-(defun proof-del-favourite 635,22896
-(defun proof-read-favourite 652,23457
-(defun proof-add-favourite 676,24241
-(defvar proof-menu-settings 703,25292
-(defun proof-menu-define-settings-menu 706,25366
-(defun proof-menu-entry-name 739,26498
-(defun proof-menu-entry-for-setting 749,26840
-(defun proof-settings-vars 768,27375
-(defun proof-settings-changed-from-defaults-p 773,27552
-(defun proof-settings-changed-from-saved-p 777,27658
-(defun proof-settings-save 781,27761
-(defun proof-settings-reset 786,27928
-(defun proof-defpacustom-fn 793,28173
-(defmacro defpacustom 859,30465
-(defun proof-assistant-invisible-command-ifposs 874,31292
-(defun proof-maybe-askprefs 896,32267
-(defun proof-assistant-settings-cmd 902,32461
-(defvar proof-assistant-format-table 919,33121
-(defun proof-assistant-format-bool 927,33490
-(defun proof-assistant-format-int 930,33603
-(defun proof-assistant-format-string 933,33695
-(defun proof-assistant-format 936,33793
+(defun proof-maths-menu-enable 44,1410
+
+generic/proof-menu.el,2146
+(defvar proof-display-some-buffers-count 19,452
+(defun proof-display-some-buffers 21,497
+(defun proof-menu-define-keys 80,2693
+(defun proof-menu-define-main 137,5498
+(defvar proof-menu-favourites 146,5683
+(defun proof-menu-define-specific 150,5805
+(defun proof-assistant-menu-update 193,7073
+(defvar proof-help-menu207,7506
+(defvar proof-show-hide-menu215,7776
+(defvar proof-buffer-menu224,8089
+(defun proof-retract-on-edit-toggle 285,10312
+(defun proof-keep-response-history 292,10488
+(defconst proof-quick-opts-menu300,10798
+(defun proof-quick-opts-vars 467,17723
+(defun proof-quick-opts-changed-from-defaults-p 494,18524
+(defun proof-quick-opts-changed-from-saved-p 498,18629
+(defun proof-quick-opts-save 509,18980
+(defun proof-quick-opts-reset 514,19148
+(defconst proof-config-menu526,19416
+(defconst proof-advanced-menu533,19595
+(defvar proof-menu546,20030
+(defun proof-main-menu 555,20312
+(defun proof-aux-menu 566,20578
+(defun proof-menu-define-favourites-menu 582,20924
+(defun proof-def-favourite 602,21573
+(defvar proof-make-favourite-cmd-history 625,22547
+(defvar proof-make-favourite-menu-history 628,22632
+(defun proof-save-favourites 631,22718
+(defun proof-del-favourite 636,22866
+(defun proof-read-favourite 653,23422
+(defun proof-add-favourite 677,24198
+(defvar proof-menu-settings 704,25243
+(defun proof-menu-define-settings-menu 707,25317
+(defun proof-menu-entry-name 740,26438
+(defun proof-menu-entry-for-setting 750,26788
+(defun proof-settings-vars 769,27320
+(defun proof-settings-changed-from-defaults-p 774,27497
+(defun proof-settings-changed-from-saved-p 778,27603
+(defun proof-settings-save 782,27706
+(defun proof-settings-reset 787,27873
+(defun proof-defpacustom-fn 794,28118
+(defmacro defpacustom 860,30399
+(defun proof-assistant-invisible-command-ifposs 875,31226
+(defun proof-maybe-askprefs 897,32196
+(defun proof-assistant-settings-cmd 903,32388
+(defvar proof-assistant-format-table920,33043
+(defun proof-assistant-format-bool 928,33411
+(defun proof-assistant-format-int 931,33524
+(defun proof-assistant-format-string 934,33616
+(defun proof-assistant-format 937,33714
 
 generic/proof-mmm.el,70
 (defun proof-mmm-set-global 41,1517
-(defun proof-mmm-enable 56,2058
-
-generic/proof-script.el,5766
-(defvar proof-element-counters 32,857
-(deflocal proof-active-buffer-fake-minor-mode 38,997
-(deflocal proof-script-buffer-file-name 41,1123
-(deflocal pg-script-portions 48,1533
-(defun proof-next-element-count 58,1769
-(defun proof-element-id 67,2104
-(defun proof-next-element-id 71,2273
-(deflocal proof-script-last-entity 85,2590
-(defun proof-script-find-next-entity 92,2870
-(deflocal proof-locked-span 168,5612
-(deflocal proof-queue-span 175,5878
-(deflocal proof-overlay-arrow 184,6364
-(defun proof-span-give-warning 190,6491
-(defun proof-span-read-only 195,6640
-(defun proof-strict-read-only 204,7081
-(defun proof-set-overlay-arrow 242,8820
-(defsubst proof-set-locked-endpoints 253,9158
-(defsubst proof-detach-queue 258,9334
-(defsubst proof-detach-locked 263,9473
-(defsubst proof-set-queue-start 270,9698
-(defsubst proof-set-locked-end 274,9824
-(defsubst proof-set-queue-end 286,10294
-(defun proof-init-segmentation 297,10591
-(defun proof-colour-locked 331,12089
-(defun proof-restart-buffers 342,12523
-(defun proof-script-buffers-with-spans 363,13351
-(defun proof-script-remove-all-spans-and-deactivate 373,13707
-(defun proof-script-clear-queue-spans 377,13897
-(defun proof-script-delete-spans 387,14339
-(defun proof-unprocessed-begin 402,14656
-(defun proof-script-end 410,14910
-(defun proof-queue-or-locked-end 419,15213
-(defun proof-locked-end 434,15891
-(defun proof-locked-region-full-p 451,16276
-(defun proof-locked-region-empty-p 460,16548
-(defun proof-only-whitespace-to-locked-region-p 464,16698
-(defun proof-in-locked-region-p 477,17320
-(defun proof-goto-end-of-locked 489,17583
-(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 506,18342
-(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 517,18823
-(defun proof-end-of-locked-visible-p 531,19443
-(defvar pg-idioms 549,20066
-(defvar pg-visibility-specs 552,20162
-(defconst pg-default-invisibility-spec557,20369
-(defun pg-clear-script-portions 561,20508
-(defun pg-add-script-element 568,20755
-(defun pg-remove-script-element 571,20831
-(defsubst pg-visname 579,21125
-(defun pg-add-element 583,21270
-(defun pg-open-invisible-span 617,22899
-(defun pg-remove-element 628,23262
-(defun pg-make-element-invisible 635,23532
-(defun pg-make-element-visible 641,23776
-(defun pg-toggle-element-visibility 645,23919
-(defun pg-redisplay-for-gnuemacs 652,24206
-(defun pg-show-all-portions 656,24353
-(defun pg-show-all-proofs 674,25050
-(defun pg-hide-all-proofs 679,25178
-(defun pg-add-proof-element 684,25309
-(defun pg-span-name 698,25968
-(defvar pg-span-context-menu-keymap719,26675
-(defun pg-last-output-displayform 726,26913
-(defun pg-set-span-helphighlights 739,27390
-(defun proof-complete-buffer-atomic 776,28707
-(defun proof-register-possibly-new-processed-file 817,30613
-(defun proof-inform-prover-file-retracted 868,32741
-(defun proof-auto-retract-dependencies 888,33592
-(defun proof-unregister-buffer-file-name 942,36136
-(defun proof-protected-process-or-retract 988,37961
-(defun proof-deactivate-scripting-auto 1015,39131
-(defun proof-deactivate-scripting 1024,39489
-(defun proof-activate-scripting 1157,44762
-(defun proof-toggle-active-scripting 1277,50140
-(defun proof-done-advancing 1318,51501
-(defun proof-done-advancing-comment 1414,55164
-(defun proof-done-advancing-save 1433,55936
-(defun proof-make-goalsave 1526,59581
-(defun proof-get-name-from-goal 1542,60366
-(defun proof-done-advancing-autosave 1561,61392
-(defun proof-done-advancing-other 1626,63936
-(defun proof-segment-up-to-parser 1654,64895
-(defun proof-script-generic-parse-find-comment-end 1718,66979
-(defun proof-script-generic-parse-cmdend 1727,67395
-(defun proof-script-generic-parse-cmdstart 1752,68290
-(defun proof-script-generic-parse-sexp 1815,70998
-(defun proof-cmdstart-add-segment-for-cmd 1839,71934
-(defun proof-segment-up-to-cmdstart 1891,74147
-(defun proof-segment-up-to-cmdend 1952,76507
-(defun proof-semis-to-vanillas 2024,79186
-(defun proof-script-new-command-advance 2063,80515
-(defun proof-script-next-command-advance 2105,82256
-(defun proof-assert-until-point-interactive 2117,82697
-(defun proof-assert-until-point 2146,83822
-(defun proof-assert-next-command2199,86266
-(defun proof-retract-before-change 2247,88516
-(defun proof-inside-comment 2256,88854
-(defun proof-goto-point 2261,88980
-(defun proof-insert-pbp-command 2279,89525
-(defun proof-insert-sendback-command 2293,90004
-(defun proof-done-retracting 2319,90907
-(defun proof-setup-retract-action 2354,92355
-(defun proof-last-goal-or-goalsave 2364,92838
-(defun proof-retract-target 2388,93743
-(defun proof-retract-until-point-interactive 2473,97384
-(defun proof-retract-until-point 2481,97769
-(define-derived-mode proof-mode 2524,99518
-(defun proof-script-set-visited-file-name 2561,100886
-(defun proof-script-set-buffer-hooks 2585,101895
-(defun proof-script-kill-buffer-fn 2593,102313
-(defun proof-config-done-related 2625,103631
-(defun proof-generic-goal-command-p 2693,106159
-(defun proof-generic-state-preserving-p 2698,106372
-(defun proof-generic-count-undos 2707,106889
-(defun proof-generic-find-and-forget 2736,107917
-(defconst proof-script-important-settings2787,109742
-(defun proof-config-done 2802,110295
-(defun proof-setup-parsing-mechanism 2871,112601
-(defun proof-setup-imenu 2915,114454
-(defun proof-setup-func-menu 2932,115058
-(deflocal proof-segment-up-to-cache 2994,117284
-(deflocal proof-segment-up-to-cache-start 2995,117325
-(deflocal proof-last-edited-low-watermark 2996,117370
-(defun proof-segment-up-to-using-cache 3006,117857
-(defun proof-segment-cache-contents-for 3035,119005
-(defun proof-script-after-change-function 3047,119374
-(defun proof-script-set-after-change-functions 3059,119888
-
-generic/proof-shell.el,3401
-(defvar proof-marker 36,808
-(defvar proof-action-list 39,904
-(defvar proof-shell-silent 57,1554
-(defvar proof-shell-last-prompt 64,1845
-(defvar proof-shell-last-output-kind 68,2016
-(defvar proof-shell-delayed-output 89,2843
-(defvar proof-shell-delayed-output-kind 92,2965
-(defvar proof-shell-delayed-output-flags 95,3098
-(defcustom proof-shell-active-scripting-indicator104,3295
-(defun proof-shell-ready-prover 154,4681
-(defun proof-shell-live-buffer 168,5220
-(defun proof-shell-available-p 175,5455
-(defun proof-grab-lock 181,5677
-(defun proof-release-lock 194,6279
-(defcustom proof-shell-fiddle-frames 209,6676
-(defun proof-shell-set-text-representation 215,6898
-(defun proof-shell-start 226,7359
-(defvar proof-shell-kill-function-hooks 409,13579
-(defun proof-shell-kill-function 412,13679
-(defun proof-shell-clear-state 501,17482
-(defun proof-shell-exit 516,17925
-(defun proof-shell-bail-out 528,18370
-(defun proof-shell-restart 537,18847
-(defvar proof-shell-urgent-message-marker 577,20134
-(defvar proof-shell-urgent-message-scanner 580,20255
-(defun proof-shell-handle-output 584,20382
-(defsubst proof-shell-strip-output-markup 621,21702
-(defvar proof-shell-no-error-display 633,22068
-(defun proof-shell-handle-error 639,22271
-(defun proof-shell-handle-interrupt 656,23079
-(defun proof-shell-error-or-interrupt-action 671,23752
-(defun proof-goals-pos 701,24948
-(defun proof-pbp-focus-on-first-goal 706,25159
-(defsubst proof-shell-string-match-safe 718,25586
-(defun proof-shell-classify-output 723,25754
-(defvar proof-shell-expecting-output 840,30641
-(defvar proof-shell-interrupt-pending 844,30800
-(defun proof-interrupt-process 850,31025
-(defun proof-shell-insert 888,32480
-(defun proof-shell-action-list-item 950,34844
-(defun proof-shell-set-silent 956,35089
-(defun proof-shell-start-silent-item 962,35308
-(defun proof-shell-clear-silent 968,35497
-(defun proof-shell-stop-silent-item 974,35719
-(defun proof-shell-should-be-silent 981,35988
-(defsubst proof-shell-invoke-callback 995,36582
-(defun proof-append-alist 999,36748
-(defun proof-start-queue 1058,38990
-(defun proof-extend-queue 1069,39339
-(defun proof-shell-exec-loop 1078,39718
-(defun proof-shell-insert-loopback-cmd 1149,42161
-(defun proof-shell-message 1177,43483
-(defun proof-shell-process-urgent-message 1184,43735
-(defun proof-shell-strip-eager-annotations 1314,48852
-(defvar proof-shell-minibuffer-urgent-interactive-input-history 1325,49187
-(defun proof-shell-minibuffer-urgent-interactive-input 1327,49257
-(defun proof-shell-filter 1344,49725
-(defun proof-shell-process-urgent-messages 1496,55694
-(defun proof-shell-filter-manage-output 1573,58637
-(defun proof-shell-handle-delayed-output 1610,60102
-(defvar pg-last-tracing-output-time 1651,61651
-(defconst pg-slow-mode-duration 1654,61757
-(defconst pg-fast-tracing-mode-threshold 1657,61839
-(defvar pg-tracing-cleanup-timer 1660,61967
-(defun pg-tracing-tight-loop 1662,62006
-(defun pg-finish-tracing-display 1705,63719
-(defun proof-shell-wait 1723,64083
-(defun proof-done-invisible 1742,64991
-(defun proof-shell-invisible-command 1748,65161
-(defun proof-shell-invisible-cmd-get-result 1795,66705
-(defun proof-shell-invisible-command-invisible-result 1807,67141
-(define-derived-mode proof-shell-mode 1826,67580
-(defconst proof-shell-important-settings1884,69872
-(defun proof-shell-config-done 1890,69987
-
-generic/proof-site.el,504
-(defconst proof-assistant-table-default22,728
-(defconst proof-general-short-version 60,2144
-(defconst proof-general-version-year 66,2332
-(defgroup proof-general 73,2485
-(defgroup proof-general-internals 78,2593
-(defun proof-home-directory-fn 91,2981
-(defcustom proof-home-directory102,3352
-(defcustom proof-images-directory111,3719
-(defcustom proof-info-directory117,3921
-(defcustom proof-assistant-table145,5108
-(defcustom proof-assistants 180,6224
-(defun proof-ready-for-assistant 208,7369
-
-generic/proof-splash.el,764
-(defcustom proof-splash-enable 17,320
-(defcustom proof-splash-time 22,472
-(defcustom proof-splash-contents30,757
-(defconst proof-splash-startup-msg 70,2102
-(defconst proof-splash-welcome 79,2481
-(defsubst proof-emacs-imagep 86,2656
-(defun proof-get-image 91,2781
-(defvar proof-splash-timeout-conf 116,3741
-(defun proof-splash-centre-spaces 119,3854
-(defun proof-splash-remove-screen 144,4940
-(defun proof-splash-remove-buffer 161,5596
-(defvar proof-splash-seen 177,6260
-(defun proof-splash-display-screen 181,6377
-(defun proof-splash-message 263,9713
-(defun proof-splash-timeout-waiter 276,10157
-(defvar proof-splash-old-frame-title-format 289,10715
-(defun proof-splash-set-frame-titles 291,10765
-(defun proof-splash-unset-frame-titles 300,11081
-
-generic/proof-syntax.el,1041
-(defun proof-ids-to-regexp 15,436
-(defun proof-anchor-regexp 19,605
-(defconst proof-no-regexp23,707
-(defun proof-regexp-alt 28,800
-(defun proof-regexp-region 37,1106
-(defun proof-re-search-forward-region 46,1529
-(defun proof-search-forward 59,2024
-(defun proof-replace-regexp-in-string 65,2276
-(defun proof-re-search-forward 71,2530
-(defun proof-re-search-backward 77,2791
-(defun proof-string-match 83,3055
-(defun proof-string-match-safe 89,3287
-(defun proof-stringfn-match 93,3492
-(defun proof-looking-at 100,3752
-(defun proof-looking-at-safe 106,3942
-(defun proof-looking-at-syntactic-context-default 110,4082
-(defun proof-looking-at-syntactic-context 119,4435
-(defsubst proof-replace-string 131,4921
-(defsubst proof-replace-regexp 136,5125
-(defsubst proof-replace-regexp-nocasefold 141,5334
-(defvar proof-id 149,5616
-(defun proof-ids 155,5836
-(defun proof-zap-commas 168,6392
-(defun proof-format 184,6888
-(defun proof-format-filename 203,7527
-(defun proof-insert 250,8927
-(defun proof-splice-separator 287,9943
+(defun proof-mmm-enable 56,2056
+
+generic/proof-script.el,5377
+(deflocal proof-active-buffer-fake-minor-mode 32,852
+(deflocal proof-script-buffer-file-name 35,978
+(deflocal pg-script-portions 42,1388
+(defun proof-next-element-count 52,1608
+(defun proof-element-id 58,1850
+(defun proof-next-element-id 62,2019
+(deflocal proof-locked-span 97,3273
+(deflocal proof-queue-span 104,3539
+(deflocal proof-overlay-arrow 113,4025
+(defun proof-span-give-warning 119,4152
+(defun proof-span-read-only 124,4301
+(defun proof-strict-read-only 133,4674
+(defsubst proof-set-queue-endpoints 143,5052
+(defun proof-set-overlay-arrow 147,5193
+(defsubst proof-set-locked-endpoints 158,5531
+(defsubst proof-detach-queue 163,5707
+(defsubst proof-detach-locked 168,5846
+(defsubst proof-set-queue-start 175,6071
+(defsubst proof-set-locked-end 179,6197
+(defsubst proof-set-queue-end 191,6667
+(defun proof-init-segmentation 202,6964
+(defun proof-colour-locked 236,8462
+(defun proof-restart-buffers 247,8894
+(defun proof-script-buffers-with-spans 268,9645
+(defun proof-script-remove-all-spans-and-deactivate 278,10001
+(defun proof-script-clear-queue-spans 282,10191
+(defun proof-script-delete-spans 292,10633
+(defun proof-unprocessed-begin 307,10948
+(defun proof-script-end 315,11202
+(defun proof-queue-or-locked-end 324,11505
+(defun proof-locked-end 339,12183
+(defun proof-locked-region-full-p 353,12464
+(defun proof-locked-region-empty-p 362,12736
+(defun proof-only-whitespace-to-locked-region-p 366,12886
+(defun proof-in-locked-region-p 376,13213
+(defun proof-goto-end-of-locked 388,13470
+(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 405,14229
+(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 416,14710
+(defun proof-end-of-locked-visible-p 430,15330
+(defvar pg-idioms 448,15948
+(defvar pg-visibility-specs 451,16044
+(defconst pg-default-invisibility-spec456,16251
+(defun pg-clear-script-portions 459,16320
+(defun pg-remove-script-element 466,16594
+(defsubst pg-visname 471,16783
+(defun pg-add-element 475,16928
+(defun pg-open-invisible-span 511,18621
+(defun pg-remove-element 522,18984
+(defun pg-make-element-invisible 529,19254
+(defun pg-make-element-visible 535,19498
+(defun pg-toggle-element-visibility 539,19641
+(defun pg-redisplay-for-gnuemacs 546,19928
+(defun pg-show-all-portions 550,20075
+(defun pg-show-all-proofs 570,20793
+(defun pg-hide-all-proofs 575,20921
+(defun pg-add-proof-element 580,21052
+(defun pg-span-name 594,21710
+(defvar pg-span-context-menu-keymap615,22410
+(defun pg-last-output-displayform 622,22648
+(defun pg-set-span-helphighlights 635,23125
+(defun proof-complete-buffer-atomic 672,24467
+(defun proof-register-possibly-new-processed-file713,26372
+(defun proof-inform-prover-file-retracted 759,28203
+(defun proof-auto-retract-dependencies 779,29054
+(defun proof-unregister-buffer-file-name 833,31598
+(defun proof-protected-process-or-retract 879,33423
+(defun proof-deactivate-scripting-auto 906,34593
+(defun proof-deactivate-scripting 915,34951
+(defun proof-activate-scripting 1048,40207
+(defun proof-toggle-active-scripting 1163,45312
+(defun proof-done-advancing 1202,46557
+(defun proof-done-advancing-comment 1281,49542
+(defun proof-done-advancing-save 1315,50918
+(defun proof-make-goalsave 1403,54309
+(defun proof-get-name-from-goal 1419,55092
+(defun proof-done-advancing-autosave 1439,56117
+(defun proof-done-advancing-other 1504,58661
+(defun proof-segment-up-to-parser 1532,59614
+(defun proof-script-generic-parse-find-comment-end 1596,61697
+(defun proof-script-generic-parse-cmdend 1605,62111
+(defun proof-script-generic-parse-cmdstart 1630,62998
+(defun proof-script-generic-parse-sexp 1693,65691
+(defun proof-cmdstart-add-segment-for-cmd 1717,66623
+(defun proof-segment-up-to-cmdstart 1769,68836
+(defun proof-segment-up-to-cmdend 1830,71196
+(defun proof-semis-to-vanillas 1902,73875
+(defun proof-assert-until-point 1934,74974
+(defun proof-assert-semis 1949,75567
+(defun proof-retract-before-change 1957,75912
+(defun proof-inside-comment 1966,76230
+(defun proof-insert-pbp-command 1980,76465
+(defun proof-insert-sendback-command 1994,76944
+(defun proof-done-retracting 2020,77847
+(defun proof-setup-retract-action 2055,79288
+(defun proof-last-goal-or-goalsave 2065,79771
+(defun proof-retract-target 2089,80676
+(defun proof-retract-until-point-interactive 2174,84318
+(defun proof-retract-until-point 2182,84703
+(define-derived-mode proof-mode 2225,86429
+(defun proof-script-set-visited-file-name 2262,87797
+(defun proof-script-set-buffer-hooks 2286,88806
+(defun proof-script-kill-buffer-fn 2294,89224
+(defun proof-config-done-related 2326,90541
+(defun proof-generic-goal-command-p 2394,93064
+(defun proof-generic-state-preserving-p 2399,93277
+(defun proof-generic-count-undos 2408,93794
+(defun proof-generic-find-and-forget 2437,94832
+(defconst proof-script-important-settings2490,96671
+(defun proof-config-done 2505,97217
+(defun proof-setup-parsing-mechanism 2573,99495
+(defun proof-setup-imenu 2617,101348
+(deflocal proof-segment-up-to-cache 2641,102122
+(deflocal proof-segment-up-to-cache-start 2642,102163
+(deflocal proof-last-edited-low-watermark 2643,102208
+(defun proof-segment-up-to-using-cache 2653,102695
+(defun proof-segment-cache-contents-for 2682,103843
+(defun proof-script-after-change-function 2694,104212
+(defun proof-script-set-after-change-functions 2706,104719
+
+generic/proof-shell.el,3801
+(defvar proof-marker 36,824
+(defvar proof-action-list 39,920
+(defvar proof-shell-silent 57,1570
+(defvar proof-shell-last-prompt 64,1861
+(defvar proof-shell-last-output-kind 68,2031
+(defvar proof-shell-delayed-output 89,2829
+(defvar proof-shell-delayed-output-kind 92,2951
+(defvar proof-shell-delayed-output-flags 95,3084
+(defcustom proof-shell-active-scripting-indicator104,3280
+(defun proof-shell-ready-prover 154,4664
+(defsubst proof-shell-live-buffer 168,5203
+(defun proof-shell-available-p 175,5442
+(defun proof-grab-lock 181,5664
+(defun proof-release-lock 194,6266
+(defcustom proof-shell-fiddle-frames 209,6663
+(defun proof-shell-set-text-representation 215,6885
+(defun proof-shell-start 226,7346
+(defvar proof-shell-kill-function-hooks 411,13611
+(defun proof-shell-kill-function 414,13709
+(defun proof-shell-clear-state 503,17513
+(defun proof-shell-exit 518,17953
+(defun proof-shell-bail-out 530,18398
+(defun proof-shell-restart 539,18875
+(defvar proof-shell-urgent-message-marker 579,20162
+(defvar proof-shell-urgent-message-scanner 582,20283
+(defun proof-shell-handle-output 586,20410
+(defsubst proof-shell-strip-output-markup 623,21724
+(defvar proof-shell-no-error-display 635,22089
+(defun proof-shell-handle-error 641,22292
+(defun proof-shell-handle-interrupt 658,23100
+(defun proof-shell-error-or-interrupt-action 673,23766
+(defun proof-goals-pos 703,24962
+(defun proof-pbp-focus-on-first-goal 708,25173
+(defsubst proof-shell-string-match-safe 720,25589
+(defun proof-shell-classify-output 725,25751
+(defvar proof-shell-expecting-output 831,29860
+(defvar proof-shell-interrupt-pending 835,30019
+(defun proof-interrupt-process 841,30244
+(defun proof-shell-insert 879,31677
+(defun proof-shell-action-list-item 927,33311
+(defun proof-shell-set-silent 933,33556
+(defun proof-shell-start-silent-item 939,33775
+(defun proof-shell-clear-silent 945,33964
+(defun proof-shell-stop-silent-item 951,34186
+(defun proof-shell-should-be-silent 958,34455
+(defsubst proof-shell-invoke-callback 972,35042
+(defun proof-append-alist 978,35252
+(defun proof-start-queue 1036,37460
+(defun proof-extend-queue 1047,37809
+(defun proof-shell-exec-loop 1056,38188
+(defun proof-shell-insert-loopback-cmd 1135,40845
+(defun proof-shell-process-urgent-message 1163,42167
+(defun proof-shell-process-urgent-message-default 1221,44390
+(defun proof-shell-process-urgent-message-trace 1239,45080
+(defun proof-shell-process-urgent-message-retract 1252,45640
+(defun proof-shell-process-urgent-message-elisp 1273,46488
+(defun proof-shell-process-urgent-message-thmdeps 1288,46983
+(defun proof-shell-message 1302,47363
+(defun proof-shell-strip-eager-annotations 1309,47615
+(defvar proof-shell-minibuffer-urgent-interactive-input-history 1324,48148
+(defun proof-shell-minibuffer-urgent-interactive-input 1326,48218
+(defun proof-shell-filter 1342,48685
+(defun proof-shell-filter-first-command 1437,51779
+(defun proof-shell-cleanup 1452,52322
+(defun proof-shell-process-urgent-messages 1457,52470
+(defun proof-shell-filter-manage-output 1524,54933
+(defun proof-shell-handle-delayed-output 1561,56397
+(defvar pg-last-tracing-output-time 1602,57946
+(defconst pg-slow-mode-duration 1605,58052
+(defconst pg-fast-tracing-mode-threshold 1608,58134
+(defvar pg-tracing-cleanup-timer 1611,58262
+(defun pg-tracing-tight-loop 1613,58301
+(defun pg-finish-tracing-display 1656,60013
+(defun proof-shell-wait 1674,60377
+(defun proof-done-invisible 1693,61285
+(defun proof-shell-invisible-command 1699,61455
+(defun proof-shell-invisible-cmd-get-result 1746,62999
+(defun proof-shell-invisible-command-invisible-result 1758,63435
+(define-derived-mode proof-shell-mode 1777,63872
+(defconst proof-shell-important-settings1819,65265
+(defun proof-shell-config-done 1825,65380
+
+generic/proof-site.el,503
+(defconst proof-assistant-table-default22,725
+(defconst proof-general-short-version60,2122
+(defconst proof-general-version-year 66,2309
+(defgroup proof-general 73,2462
+(defgroup proof-general-internals 78,2570
+(defun proof-home-directory-fn 91,2958
+(defcustom proof-home-directory102,3328
+(defcustom proof-images-directory111,3694
+(defcustom proof-info-directory117,3896
+(defcustom proof-assistant-table141,4817
+(defcustom proof-assistants 176,5930
+(defun proof-ready-for-assistant 205,7086
+
+generic/proof-splash.el,800
+(defcustom proof-splash-enable 17,318
+(defcustom proof-splash-time 22,470
+(defcustom proof-splash-contents30,754
+(defconst proof-splash-startup-msg70,2128
+(defconst proof-splash-welcome 79,2506
+(defsubst proof-emacs-imagep 86,2681
+(defun proof-get-image 91,2806
+(defvar proof-splash-timeout-conf 113,3606
+(defun proof-splash-centre-spaces 116,3692
+(defun proof-splash-remove-screen 131,4315
+(defvar proof-splash-seen 145,4774
+(defun proof-splash-insert-contents 148,4876
+(defun proof-splash-display-screen 187,6070
+(defalias 'pg-about pg-about
204,6729
+(defun proof-splash-message 207,6795
+(defun proof-splash-timeout-waiter 220,7239
+(defvar proof-splash-old-frame-title-format 229,7625
+(defun proof-splash-set-frame-titles 231,7675
+(defun proof-splash-unset-frame-titles 240,7990
+
+generic/proof-syntax.el,996
+(defsubst proof-ids-to-regexp 17,445
+(defsubst proof-anchor-regexp 21,618
+(defconst proof-no-regexp 25,723
+(defsubst proof-regexp-alt 28,814
+(defsubst proof-re-search-forward-region 37,1123
+(defsubst proof-search-forward 50,1621
+(defsubst proof-replace-regexp-in-string 56,1876
+(defsubst proof-re-search-forward 61,2127
+(defsubst proof-re-search-backward 66,2385
+(defsubst proof-string-match 71,2646
+(defsubst proof-string-match-safe 76,2875
+(defsubst proof-stringfn-match 80,3079
+(defsubst proof-looking-at 87,3342
+(defsubst proof-looking-at-safe 92,3529
+(defsubst proof-looking-at-syntactic-context-default 96,3674
+(defsubst proof-replace-string 107,4051
+(defsubst proof-replace-regexp 112,4255
+(defsubst proof-replace-regexp-nocasefold 117,4464
+(defvar proof-id 125,4746
+(defsubst proof-ids 131,4966
+(defun proof-zap-commas 145,5458
+(defun proof-format 161,5954
+(defun proof-format-filename 180,6593
+(defun proof-insert 227,7995
+(defun proof-splice-separator 264,9012
 
 generic/proof-toolbar.el,2357
-(defun proof-toolbar-function 35,839
-(defun proof-toolbar-icon 38,936
-(defun proof-toolbar-enabler 41,1037
-(defun proof-toolbar-make-icon 48,1190
-(defun proof-toolbar-make-toolbar-items 57,1498
-(defvar proof-toolbar-map 82,2304
-(defun proof-toolbar-available-p 85,2403
-(defun proof-toolbar-setup 94,2679
-(defalias 'proof-toolbar-enable proof-toolbar-enable
112,3468
-(defalias 'proof-toolbar-undo proof-toolbar-undo
142,4448
-(defun proof-toolbar-undo-enable-p 144,4516
-(defalias 'proof-toolbar-delete proof-toolbar-delete
151,4674
-(defun proof-toolbar-delete-enable-p 153,4755
-(defalias 'proof-toolbar-home proof-toolbar-home
161,4937
-(defalias 'proof-toolbar-next proof-toolbar-next
165,5004
-(defun proof-toolbar-next-enable-p 167,5075
-(defalias 'proof-toolbar-goto proof-toolbar-goto
173,5191
-(defun proof-toolbar-goto-enable-p 175,5241
-(defalias 'proof-toolbar-retract proof-toolbar-retract
180,5326
-(defun proof-toolbar-retract-enable-p 182,5383
-(defalias 'proof-toolbar-use proof-toolbar-use
188,5502
-(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p
189,5554
-(defalias 'proof-toolbar-restart proof-toolbar-restart
193,5635
-(defalias 'proof-toolbar-goal proof-toolbar-goal
197,5700
-(defalias 'proof-toolbar-qed proof-toolbar-qed
201,5758
-(defun proof-toolbar-qed-enable-p 203,5807
-(defalias 'proof-toolbar-state proof-toolbar-state
211,5969
-(defalias 'proof-toolbar-state-enable-p proof-toolbar-state-enable-p
212,6012
-(defalias 'proof-toolbar-context proof-toolbar-context
216,6091
-(defalias 'proof-toolbar-context-enable-p proof-toolbar-context-enable-p
217,6137
-(defalias 'proof-toolbar-command proof-toolbar-command
221,6218
-(defalias 'proof-toolbar-command-enable-p proof-toolbar-command-enable-p
222,6274
-(defun proof-toolbar-help 226,6380
-(defalias 'proof-toolbar-find proof-toolbar-find
232,6461
-(defalias 'proof-toolbar-find-enable-p proof-toolbar-find-enable-p
233,6513
-(defalias 'proof-toolbar-info proof-toolbar-info
237,6589
-(defalias 'proof-toolbar-info-enable-p proof-toolbar-info-enable-p
238,6644
-(defalias 'proof-toolbar-visibility proof-toolbar-visibility
242,6742
-(defun proof-toolbar-visibility-enable-p 244,6802
-(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt
249,6916
-(defun proof-toolbar-interrupt-enable-p 250,6977
-(defun proof-toolbar-scripting-menu 258,7130
+(defun proof-toolbar-function 33,837
+(defun proof-toolbar-icon 36,934
+(defun proof-toolbar-enabler 39,1035
+(defun proof-toolbar-make-icon 46,1187
+(defun proof-toolbar-make-toolbar-items 55,1495
+(defvar proof-toolbar-map 80,2300
+(defun proof-toolbar-available-p 83,2399
+(defun proof-toolbar-setup 92,2675
+(defalias 'proof-toolbar-enable proof-toolbar-enable
110,3471
+(defalias 'proof-toolbar-undo proof-toolbar-undo
140,4451
+(defun proof-toolbar-undo-enable-p 142,4519
+(defalias 'proof-toolbar-delete proof-toolbar-delete
149,4677
+(defun proof-toolbar-delete-enable-p 151,4758
+(defalias 'proof-toolbar-home proof-toolbar-home
159,4940
+(defalias 'proof-toolbar-next proof-toolbar-next
163,5007
+(defun proof-toolbar-next-enable-p 165,5078
+(defalias 'proof-toolbar-goto proof-toolbar-goto
171,5194
+(defun proof-toolbar-goto-enable-p 173,5244
+(defalias 'proof-toolbar-retract proof-toolbar-retract
178,5329
+(defun proof-toolbar-retract-enable-p 180,5386
+(defalias 'proof-toolbar-use proof-toolbar-use
186,5505
+(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p
187,5557
+(defalias 'proof-toolbar-restart proof-toolbar-restart
191,5638
+(defalias 'proof-toolbar-goal proof-toolbar-goal
195,5703
+(defalias 'proof-toolbar-qed proof-toolbar-qed
199,5761
+(defun proof-toolbar-qed-enable-p 201,5810
+(defalias 'proof-toolbar-state proof-toolbar-state
209,5972
+(defalias 'proof-toolbar-state-enable-p proof-toolbar-state-enable-p
210,6015
+(defalias 'proof-toolbar-context proof-toolbar-context
214,6094
+(defalias 'proof-toolbar-context-enable-p proof-toolbar-context-enable-p
215,6140
+(defalias 'proof-toolbar-command proof-toolbar-command
219,6221
+(defalias 'proof-toolbar-command-enable-p proof-toolbar-command-enable-p
220,6277
+(defun proof-toolbar-help 224,6382
+(defalias 'proof-toolbar-find proof-toolbar-find
230,6462
+(defalias 'proof-toolbar-find-enable-p proof-toolbar-find-enable-p
231,6514
+(defalias 'proof-toolbar-info proof-toolbar-info
235,6589
+(defalias 'proof-toolbar-info-enable-p proof-toolbar-info-enable-p
236,6644
+(defalias 'proof-toolbar-visibility proof-toolbar-visibility
240,6742
+(defun proof-toolbar-visibility-enable-p 242,6802
+(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt
247,6916
+(defun proof-toolbar-interrupt-enable-p 248,6977
+(defun proof-toolbar-scripting-menu 256,7130
 
 generic/proof-unicode-tokens.el,496
-(defvar proof-unicode-tokens-initialised 28,761
-(defun proof-unicode-tokens-init 31,868
-(defun proof-unicode-tokens-configure 45,1370
-(defun proof-unicode-tokens-enable 57,1818
-(defun proof-unicode-tokens-mode-if-enabled 71,2505
-(defun proof-unicode-tokens-set-global 77,2704
-(defun proof-unicode-tokens-reconfigure 95,3344
-(defun proof-unicode-tokens-configure-prover 121,4232
-(defun proof-unicode-tokens-activate-prover 126,4413
-(defun proof-unicode-tokens-deactivate-prover 133,4659
+(defvar proof-unicode-tokens-initialised 28,760
+(defun proof-unicode-tokens-init 31,867
+(defun proof-unicode-tokens-configure 45,1369
+(defun proof-unicode-tokens-enable 57,1815
+(defun proof-unicode-tokens-mode-if-enabled 71,2502
+(defun proof-unicode-tokens-set-global 77,2701
+(defun proof-unicode-tokens-reconfigure 95,3339
+(defun proof-unicode-tokens-configure-prover 121,4227
+(defun proof-unicode-tokens-activate-prover 126,4408
+(defun proof-unicode-tokens-deactivate-prover 133,4654
 
 generic/proof-useropts.el,1416
 (defgroup proof-user-options 21,552
@@ -2060,429 +2066,455 @@ generic/proof-useropts.el,1416
 (defcustom proof-toolbar-enable 74,2386
 (defcustom proof-imenu-enable 80,2559
 (defcustom pg-show-hints 86,2730
-(defcustom proof-trace-output-slow-catchup 92,2925
-(defcustom proof-strict-state-preserving 102,3422
-(defcustom proof-strict-read-only 115,4031
-(defcustom proof-allow-undo-in-read-only 127,4541
-(defcustom proof-three-window-enable 135,4819
-(defcustom proof-multiple-frames-enable 154,5569
-(defcustom proof-delete-empty-windows 163,5902
-(defcustom proof-shrink-windows-tofit 174,6433
-(defcustom proof-auto-raise-buffers 181,6705
-(defcustom proof-colour-locked 188,6940
-(defcustom proof-query-file-save-when-activating-scripting196,7190
-(defcustom proof-one-command-per-line212,7910
-(defcustom proof-prog-name-ask219,8134
-(defcustom proof-prog-name-guess225,8294
-(defcustom proof-tidy-response233,8559
-(defcustom proof-keep-response-history247,9022
-(defcustom pg-input-ring-size 257,9410
-(defcustom proof-general-debug 262,9562
-(defcustom proof-use-parser-cache 273,9971
-(defcustom proof-follow-mode 283,10268
-(defcustom proof-auto-action-when-deactivating-scripting 307,11445
-(defcustom proof-script-command-separator 330,12394
-(defcustom proof-rsh-command 338,12686
-(defcustom proof-disappearing-proofs 354,13236
-(defcustom proof-full-annotation 359,13397
-
-generic/proof-utils.el,1911
-(defmacro deflocal 62,1812
-(defmacro proof-with-current-buffer-if-exists 69,2050
-(deflocal proof-buffer-type 75,2260
-(defmacro proof-with-script-buffer 81,2540
-(defmacro proof-map-buffers 92,2927
-(defmacro proof-sym 97,3112
-(defsubst proof-try-require 102,3273
-(defun proof-save-some-buffers 115,3604
-(defmacro proof-ass-sym 164,5205
-(defmacro proof-ass-symv 170,5464
-(defmacro proof-ass 176,5722
-(defun proof-defpgcustom-fn 182,5974
-(defun undefpgcustom 203,6845
-(defmacro defpgcustom 209,7069
-(defun proof-defpgdefault-fn 220,7487
-(defmacro defpgdefault 234,7945
-(defmacro defpgfun 245,8307
-(defmacro proof-eval-when-ready-for-assistant 255,8572
-(defun proof-file-truename 268,8967
-(defun proof-file-to-buffer 272,9150
-(defun proof-files-to-buffers 283,9479
-(defun proof-buffers-in-mode 290,9762
-(defun pg-save-from-death 304,10212
-(defun proof-define-keys 323,10829
-(defun pg-remove-specials 334,11121
-(defun pg-remove-specials-in-string 344,11459
-(defun proof-warn-if-unset 355,11687
-(defun proof-get-window-for-buffer 360,11905
-(defun proof-display-and-keep-buffer 411,14213
-(defun proof-clean-buffer 453,16104
-(defun proof-message 468,16725
-(defun proof-warning 473,16938
-(defun pg-internal-warning 479,17220
-(defun proof-debug 487,17539
-(defun proof-switch-to-buffer 496,17889
-(defun proof-resize-window-tofit 518,19015
-(defun proof-submit-bug-report 612,23190
-(defun proof-deftoggle-fn 647,24547
-(defmacro proof-deftoggle 662,25200
-(defun proof-defintset-fn 669,25574
-(defmacro proof-defintset 685,26278
-(defun proof-defstringset-fn 692,26655
-(defmacro proof-defstringset 705,27281
-(defun proof-escape-keymap-doc 718,27737
-(defmacro proof-defshortcut 722,27870
-(defmacro proof-definvisible 737,28468
-(defun pg-custom-save-vars 764,29389
-(defun pg-custom-reset-vars 780,30034
-(defun proof-locate-executable 793,30371
-(defun pg-current-word-pos 817,31151
+(defcustom proof-trace-output-slow-catchup 92,2923
+(defcustom proof-strict-state-preserving 102,3420
+(defcustom proof-strict-read-only 115,4029
+(defcustom proof-allow-undo-in-read-only 127,4539
+(defcustom proof-three-window-enable 134,4821
+(defcustom proof-multiple-frames-enable 153,5571
+(defcustom proof-delete-empty-windows 162,5904
+(defcustom proof-shrink-windows-tofit 173,6435
+(defcustom proof-auto-raise-buffers 180,6707
+(defcustom proof-colour-locked 187,6942
+(defcustom proof-query-file-save-when-activating-scripting195,7192
+(defcustom proof-one-command-per-line211,7912
+(defcustom proof-prog-name-ask218,8136
+(defcustom proof-prog-name-guess224,8296
+(defcustom proof-tidy-response232,8561
+(defcustom proof-keep-response-history246,9024
+(defcustom pg-input-ring-size 256,9412
+(defcustom proof-general-debug 261,9564
+(defcustom proof-use-parser-cache 272,9973
+(defcustom proof-follow-mode 282,10270
+(defcustom proof-auto-action-when-deactivating-scripting 306,11447
+(defcustom proof-script-command-separator 329,12396
+(defcustom proof-rsh-command 337,12688
+(defcustom proof-disappearing-proofs 353,13238
+(defcustom proof-full-annotation 358,13399
+
+generic/proof-utils.el,1925
+(defmacro deflocal 62,1802
+(defmacro proof-with-current-buffer-if-exists 69,2040
+(deflocal proof-buffer-type 75,2250
+(defmacro proof-with-script-buffer 81,2530
+(defmacro proof-map-buffers 92,2911
+(defmacro proof-sym 97,3096
+(defsubst proof-try-require 102,3257
+(defun proof-save-some-buffers 115,3588
+(defmacro proof-ass-sym 164,5189
+(defmacro proof-ass-symv 170,5448
+(defmacro proof-ass 176,5706
+(defun proof-defpgcustom-fn 182,5958
+(defun undefpgcustom 203,6828
+(defmacro defpgcustom 209,7052
+(defun proof-defpgdefault-fn 220,7470
+(defmacro defpgdefault 234,7928
+(defmacro defpgfun 245,8290
+(defmacro proof-eval-when-ready-for-assistant 255,8554
+(defun proof-file-truename 268,8945
+(defun proof-files-to-buffers 272,9128
+(defun proof-buffers-in-mode 280,9368
+(defun pg-save-from-death 294,9818
+(defun proof-define-keys 313,10435
+(defun pg-remove-specials 324,10720
+(defun pg-remove-specials-in-string 334,11056
+(defun proof-warn-if-unset 345,11282
+(defun proof-get-window-for-buffer 350,11500
+(defun proof-display-and-keep-buffer 401,13808
+(defun proof-clean-buffer 443,15531
+(defun proof-message 459,16187
+(defun proof-warning 464,16400
+(defun pg-internal-warning 470,16682
+(defun proof-debug 477,16949
+(defun proof-switch-to-buffer 485,17298
+(defun proof-resize-window-tofit 507,18422
+(defun proof-submit-bug-report 601,22268
+(defun proof-deftoggle-fn 636,23625
+(defmacro proof-deftoggle 651,24278
+(defun proof-defintset-fn 658,24652
+(defmacro proof-defintset 674,25356
+(defun proof-defstringset-fn 681,25733
+(defmacro proof-defstringset 694,26359
+(defun proof-escape-keymap-doc 707,26815
+(defmacro proof-defshortcut 711,26955
+(defmacro proof-definvisible 726,27553
+(defun pg-custom-save-vars 753,28480
+(defun pg-custom-reset-vars 769,29124
+(defun proof-locate-executable 782,29461
+(defun pg-current-word-pos 797,30016
+(defun proof-looking-at-syntactic-context 844,31732
 
 lib/bufhist.el,1099
-(defun bufhist-ring-update 34,1244
-(defgroup bufhist 43,1566
-(defcustom bufhist-ring-size 47,1647
-(defvar bufhist-ring 52,1758
-(defvar bufhist-ring-pos 55,1832
-(defvar bufhist-lastswitch-modified-tick 58,1911
-(defvar bufhist-read-only-history 61,2017
-(defvar bufhist-saved-mode-line-format 64,2088
-(defun bufhist-mode-line-format-entry 67,2189
-(defun bufhist-get-buffer-contents 99,3465
-(defun bufhist-restore-buffer-contents 111,3949
-(defun bufhist-checkpoint 119,4236
-(defun bufhist-erase-buffer 127,4605
-(defun bufhist-checkpoint-and-erase 137,4950
-(defun bufhist-switch-to-index 143,5136
-(defun bufhist-first 182,6740
-(defun bufhist-last 187,6899
-(defun bufhist-prev 192,7045
-(defun bufhist-next 200,7268
-(defun bufhist-delete 205,7408
-(defun bufhist-clear 217,7951
-(defun bufhist-init 232,8347
-(defun bufhist-exit 257,9284
-(defun bufhist-set-readwrite 267,9548
-(defun bufhist-before-change-function 282,10168
-(defun bufhist-make-buttons 294,10584
-(defconst bufhist-minor-mode-map308,10902
-(define-minor-mode bufhist-mode321,11379
-(defun bufhist-toggle-fn 341,12164
-
-lib/holes.el,2447
-(defvar holes-doc 38,1074
-(defvar holes-default-hole 133,4672
-(defvar holes-active-hole 137,4841
-(defcustom holes-empty-hole-string 144,5050
-(defcustom holes-empty-hole-regexp 147,5161
-(defcustom holes-search-limit 154,5452
-(defface active-hole-face166,5828
-(defface inactive-hole-face175,6228
-(defun holes-region-beginning-or-nil 187,6655
-(defun holes-region-end-or-nil 191,6750
-(defun holes-copy-active-region 195,6833
-(defun holes-is-hole-p 201,7017
-(defun holes-hole-start-position 206,7121
-(defun holes-hole-end-position 212,7307
-(defun holes-hole-buffer 219,7491
-(defun holes-hole-at 226,7666
-(defun holes-active-hole-exist-p 233,7841
-(defun holes-active-hole-start-position 243,8099
-(defun holes-active-hole-end-position 253,8471
-(defun holes-active-hole-buffer 264,8840
-(defun holes-goto-active-hole 275,9146
-(defun holes-highlight-hole-as-active 287,9414
-(defun holes-highlight-hole 297,9726
-(defun holes-disable-active-hole 308,10018
-(defun holes-set-active-hole 326,10561
-(defun holes-is-in-hole-p 339,10907
-(defun holes-make-hole 346,11050
-(defun holes-make-hole-at 372,11796
-(defun holes-clear-hole 392,12272
-(defun holes-clear-hole-at 404,12561
-(defun holes-map-holes 413,12820
-(defun holes-mapcar-holes 421,13003
-(defun holes-clear-all-buffer-holes 427,13175
-(defun holes-next 438,13475
-(defun holes-next-after-active-hole 445,13726
-(defun holes-set-active-hole-next 453,13945
-(defun holes-replace-segment 475,14498
-(defun holes-replace 485,14852
-(defun holes-replace-active-hole 516,16047
-(defun holes-replace-update-active-hole 525,16343
-(defun holes-delete-update-active-hole 546,17016
-(defun holes-set-make-active-hole 555,17246
-(defun holes-mouse-replace-active-hole 602,18971
-(defun holes-destroy-hole 622,19481
-(defun holes-hole-at-event 639,19892
-(defun holes-mouse-destroy-hole 644,20005
-(defun holes-mouse-forget-hole 654,20245
-(defun holes-mouse-set-make-active-hole 670,20555
-(defun holes-mouse-set-active-hole 692,21092
-(defun holes-set-point-next-hole-destroy 704,21356
-(defvar hole-map720,21806
-(defvar holes-mode-map730,22189
-(defun holes-replace-string-by-holes-backward 767,23664
-(defun holes-skeleton-end-hook 785,24365
-(defconst holes-jump-doc 794,24803
-(defun holes-replace-string-by-holes-backward-jump 801,25010
-(defun holes-abbrev-complete 818,25692
-(defun holes-insert-and-expand 827,26013
-(defvar holes-mode 838,26445
-(defun holes-mode 844,26641
+(defun bufhist-ring-update 34,1239
+(defgroup bufhist 43,1561
+(defcustom bufhist-ring-size 47,1642
+(defvar bufhist-ring 52,1753
+(defvar bufhist-ring-pos 55,1827
+(defvar bufhist-lastswitch-modified-tick 58,1906
+(defvar bufhist-read-only-history 61,2012
+(defvar bufhist-saved-mode-line-format 64,2083
+(defun bufhist-mode-line-format-entry 67,2184
+(defun bufhist-get-buffer-contents 99,3452
+(defun bufhist-restore-buffer-contents 111,3935
+(defun bufhist-checkpoint 119,4222
+(defun bufhist-erase-buffer 127,4591
+(defun bufhist-checkpoint-and-erase 137,4935
+(defun bufhist-switch-to-index 143,5121
+(defun bufhist-first 182,6720
+(defun bufhist-last 187,6879
+(defun bufhist-prev 192,7023
+(defun bufhist-next 200,7246
+(defun bufhist-delete 205,7386
+(defun bufhist-clear 217,7927
+(defun bufhist-init 232,8322
+(defun bufhist-exit 257,9255
+(defun bufhist-set-readwrite 267,9519
+(defun bufhist-before-change-function 282,10139
+(defun bufhist-make-buttons 294,10554
+(defconst bufhist-minor-mode-map308,10813
+(define-minor-mode bufhist-mode321,11290
+(defun bufhist-toggle-fn 341,12070
+
+lib/holes.el,2465
+(defvar holes-default-hole 44,1121
+(defvar holes-active-hole 50,1299
+(defgroup holes 60,1496
+(defcustom holes-empty-hole-string 65,1595
+(defcustom holes-empty-hole-regexp 70,1738
+(defface active-hole-face92,2440
+(defface inactive-hole-face102,2856
+(defvar hole-map116,3297
+(defvar holes-mode-map126,3688
+(defun holes-region-beginning-or-nil 172,5425
+(defun holes-region-end-or-nil 176,5561
+(defun holes-copy-active-region 180,5679
+(defun holes-is-hole-p 186,5889
+(defun holes-hole-start-position 190,5981
+(defun holes-hole-end-position 196,6164
+(defun holes-hole-buffer 201,6335
+(defun holes-hole-at 207,6509
+(defun holes-active-hole-exist-p 212,6679
+(defun holes-active-hole-start-position 219,6932
+(defun holes-active-hole-end-position 227,7300
+(defun holes-active-hole-buffer 236,7663
+(defun holes-goto-active-hole 244,7964
+(defun holes-highlight-hole-as-active 253,8223
+(defun holes-highlight-hole 261,8531
+(defun holes-disable-active-hole 269,8818
+(defun holes-set-active-hole 282,9350
+(defun holes-is-in-hole-p 292,9695
+(defun holes-make-hole 296,9833
+(defun holes-make-hole-at 314,10489
+(defun holes-clear-hole 328,10942
+(defun holes-clear-hole-at 337,11200
+(defun holes-map-holes 345,11456
+(defun holes-clear-all-buffer-holes 349,11610
+(defun holes-next 359,11911
+(defun holes-next-after-active-hole 366,12163
+(defun holes-set-active-hole-next 373,12379
+(defun holes-replace-segment 392,12916
+(defun holes-replace 401,13269
+(defun holes-replace-active-hole 429,14447
+(defun holes-replace-update-active-hole 436,14738
+(defun holes-delete-update-active-hole 454,15385
+(defun holes-set-make-active-hole 462,15612
+(defalias 'holes-track-mouse-selection holes-track-mouse-selection
477,16167
+(defsubst holes-track-mouse-clicks 478,16225
+(defun holes-mouse-replace-active-hole 482,16335
+(defun holes-destroy-hole 496,16806
+(defsubst holes-hole-at-event 510,17188
+(defun holes-mouse-destroy-hole 514,17288
+(defun holes-mouse-forget-hole 521,17509
+(defun holes-mouse-set-make-active-hole 531,17801
+(defun holes-mouse-set-active-hole 547,18300
+(defun holes-set-point-next-hole-destroy 556,18551
+(defun holes-replace-string-by-holes-backward 582,19532
+(defun holes-skeleton-end-hook 600,20232
+(defconst holes-jump-doc609,20670
+(defun holes-replace-string-by-holes-backward-jump 616,20876
+(define-minor-mode holes-mode 633,21558
+(defun holes-abbrev-complete 728,25040
+(defun holes-insert-and-expand 738,25383
 
 lib/local-vars-list.el,373
-(defconst local-vars-list-doc 28,828
-(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
+(defconst local-vars-list-doc 28,825
+(defun local-vars-list-insert-empty-zone 44,1387
+(defun local-vars-list-find 82,2090
+(defun local-vars-list-goto-var 101,2861
+(defun local-vars-list-get-current 127,3908
+(defun local-vars-list-set-current 148,4758
+(defun local-vars-list-get 171,5473
+(defun local-vars-list-get-safe 188,6003
+(defun local-vars-list-set 193,6197
 
 lib/maths-menu.el,242
 (defvar maths-menu-filter-predicate 56,2317
 (defvar maths-menu-tokenise-insert 59,2426
-(defun maths-menu-build-menu 62,2565
-(defvar maths-menu-menu84,3329
-(defvar maths-menu-mode-map344,12887
-(define-minor-mode maths-menu-mode352,13106
-
-lib/pg-dev.el,102
-(defconst pg-dev-lisp-font-lock-keywords36,1103
-(defun unload-pg 70,2040
-(defun profile-pg 98,2901
-
-lib/pg-fontsets.el,176
-(defcustom pg-fontsets-default-fontset 28,782
-(defun pg-fontsets-make-fontsetsizes 33,928
-(defconst pg-fontsets-base-fonts 52,1692
-(defun pg-fontsets-make-fontsets 58,1824
-
-lib/proof-compat.el,412
-(defvar proof-running-on-win32 31,978
-(defun pg-custom-undeclare-variable 51,1756
-(defmacro save-selected-frame 83,2532
-(defun proof-buffer-syntactic-context-emulate 99,3182
-(defvar read-shell-command-map127,4392
-(defun read-shell-command 145,5080
-(defun frames-of-buffer 155,5508
-(defmacro with-selected-window 199,6921
-(defalias 'proof-buffer-syntactic-context proof-buffer-syntactic-context
236,8026
-
-lib/span.el,1353
-(defalias 'span-start span-start
22,612
-(defalias 'span-end span-end
23,650
-(defalias 'span-set-property span-set-property
24,684
-(defalias 'span-property span-property
25,727
-(defalias 'span-make span-make
26,766
-(defalias 'span-detach span-detach
27,802
-(defalias 'span-set-endpoints span-set-endpoints
28,842
-(defalias 'span-buffer span-buffer
29,887
-(defun span-read-only-hook 31,928
-(defun span-read-only 36,1118
-(defun span-read-write 43,1425
-(defun span-give-warning 48,1592
-(defun span-write-warning 53,1735
-(defun span-lt 65,2319
-(defun spans-at-point-prop 70,2460
-(defun spans-at-region-prop 76,2625
-(defun span-at 85,2937
-(defsubst span-delete 91,3153
-(defsubst span-mapcar-spans 98,3375
-(defun span-at-before 103,3634
-(defun prev-span 120,4360
-(defun next-span 126,4511
-(defsubst span-live-p 133,4723
-(defun span-raise 139,4889
-(defalias 'span-object span-object
143,5019
-(defun span-string 145,5060
-(defun set-span-properties 150,5198
-(defun span-find-span 160,5445
-(defsubst span-at-event 167,5751
-(defun make-detached-span 171,5872
-(defun fold-spans 176,5968
-(defsubst span-detached-p 190,6501
-(defsubst set-span-face 194,6617
-(defun set-span-keymap 198,6715
-(defsubst span-delete-spans 207,6918
-(defsubst span-property-safe 211,7082
-(defsubst span-set-start 215,7221
-(defsubst span-set-end 219,7353
+(defun maths-menu-build-menu 62,2563
+(defvar maths-menu-menu84,3324
+(defvar maths-menu-mode-map344,12882
+(define-minor-mode maths-menu-mode352,13101
+
+lib/pg-dev.el,138
+(defconst pg-dev-lisp-font-lock-keywords48,1477
+(defun unload-pg 75,2271
+(defun profile-pg 103,3134
+(defun pg-bug-references 120,3560
+
+lib/pg-fontsets.el,210
+(defcustom pg-fontsets-default-fontset 28,780
+(defvar pg-fontsets-names 33,926
+(defun pg-fontsets-make-fontsetsizes 36,1007
+(defconst pg-fontsets-base-fonts55,1768
+(defun pg-fontsets-make-fontsets 61,1898
+
+lib/proof-compat.el,260
+(defvar proof-running-on-win32 32,975
+(defun pg-custom-undeclare-variable 53,1777
+(defmacro save-selected-frame 85,2548
+(defun proof-buffer-syntactic-context-emulate 95,2925
+(defalias 'proof-buffer-syntactic-contextproof-buffer-syntactic-context
163,5191
+
+lib/scomint.el,873
+(defface scomint-highlight-input 19,492
+(defface scomint-highlight-prompt23,608
+(defvar scomint-buffer-maximum-size 30,846
+(defvar scomint-output-filter-functions 35,1037
+(defvar scomint-mode-map39,1148
+(defvar scomint-last-input-start 45,1327
+(defvar scomint-last-input-end 46,1365
+(defvar scomint-last-output-start 47,1401
+(defvar scomint-exec-hook 49,1441
+(define-derived-mode scomint-mode 59,1823
+(defun scomint-check-proc 78,2722
+(defun scomint-make-in-buffer 86,3059
+(defun scomint-make 110,4326
+(defun scomint-exec 123,5037
+(defun scomint-exec-1 160,6630
+(defalias 'scomint-send-string scomint-send-string
210,8760
+(defun scomint-send-eof 212,8814
+(defun scomint-send-input 218,8956
+(defun scomint-truncate-buffer 261,10457
+(defun scomint-strip-ctrl-m 274,10851
+(defun scomint-output-filter 288,11414
+(defun scomint-interrupt-process 360,14146
+
+lib/span.el,1354
+(defalias 'span-start span-start
22,609
+(defalias 'span-end span-end
23,647
+(defalias 'span-set-property span-set-property
24,681
+(defalias 'span-property span-property
25,724
+(defalias 'span-make span-make
26,763
+(defalias 'span-detach span-detach
27,799
+(defalias 'span-set-endpoints span-set-endpoints
28,839
+(defalias 'span-buffer span-buffer
29,884
+(defun span-read-only-hook 31,925
+(defsubst span-read-only 36,1115
+(defsubst span-read-write 43,1425
+(defsubst span-give-warning 48,1595
+(defsubst span-write-warning 53,1741
+(defsubst span-lt 65,2307
+(defsubst spans-at-point-prop 70,2451
+(defsubst spans-at-region-prop 79,2642
+(defsubst span-at 89,2908
+(defsubst span-delete 93,3034
+(defsubst span-mapcar-spans 100,3256
+(defsubst span-mapc-spans 104,3431
+(defun span-at-before 108,3602
+(defsubst prev-span 125,4326
+(defsubst next-span 131,4479
+(defsubst span-live-p 137,4693
+(defsubst span-raise 143,4859
+(defsubst span-string 147,4992
+(defsubst set-span-properties 152,5152
+(defsubst span-find-span 158,5346
+(defsubst span-at-event 166,5658
+(defun fold-spans 172,5855
+(defsubst span-detached-p 186,6388
+(defsubst set-span-face 190,6504
+(defsubst set-span-keymap 194,6602
+(defsubst span-delete-spans 202,6771
+(defsubst span-property-safe 206,6933
+(defsubst span-set-start 210,7070
+(defsubst span-set-end 214,7202
 
 lib/texi-docstring-magic.el,584
-(defun texi-docstring-magic-find-face 88,3035
-(defun texi-docstring-magic-splice-sep 93,3200
-(defconst texi-docstring-magic-munge-table103,3505
-(defun texi-docstring-magic-untabify 193,7272
-(defun texi-docstring-magic-munge-docstring 203,7587
-(defun texi-docstring-magic-texi 242,8874
-(defun texi-docstring-magic-format-default 255,9314
-(defun texi-docstring-magic-texi-for 271,9949
-(defconst texi-docstring-magic-comment329,11909
-(defun texi-docstring-magic 335,12063
-(defun texi-docstring-magic-face-at-point 369,13143
-(defun texi-docstring-magic-insert-magic 384,13666
+(defun texi-docstring-magic-find-face 88,3027
+(defun texi-docstring-magic-splice-sep 93,3192
+(defconst texi-docstring-magic-munge-table103,3497
+(defun texi-docstring-magic-untabify 193,7260
+(defun texi-docstring-magic-munge-docstring 203,7575
+(defun texi-docstring-magic-texi 242,8856
+(defun texi-docstring-magic-format-default 255,9296
+(defun texi-docstring-magic-texi-for 271,9929
+(defconst texi-docstring-magic-comment329,11888
+(defun texi-docstring-magic 335,12042
+(defun texi-docstring-magic-face-at-point 369,13121
+(defun texi-docstring-magic-insert-magic 384,13644
 
 lib/unicode-chars.el,80
-(defvar unicode-chars-alist12,349
-(defun unicode-chars-list-chars 5050,245961
-
-lib/unicode-tokens.el,4802
-(defvar unicode-tokens-token-symbol-map 55,1770
-(defvar unicode-tokens-token-format 74,2393
-(defvar unicode-tokens-token-variant-format-regexp 80,2642
-(defvar unicode-tokens-shortcut-alist 91,3024
-(defvar unicode-tokens-shortcut-replacement-alist 97,3302
-(defvar unicode-tokens-control-region-format-regexp 105,3508
-(defvar unicode-tokens-control-char-format-regexp 112,3876
-(defvar unicode-tokens-control-regions 119,4237
-(defvar unicode-tokens-control-characters 122,4313
-(defvar unicode-tokens-control-char-format 125,4395
-(defvar unicode-tokens-control-region-format-start 128,4508
-(defvar unicode-tokens-control-region-format-end 131,4625
-(defconst unicode-tokens-configuration-variables138,4778
-(defun unicode-tokens-config 152,5143
-(defun unicode-tokens-config-var 156,5288
-(defun unicode-tokens-copy-configuration-variables 168,5729
-(defun unicode-tokens-customize 185,6613
-(defvar unicode-tokens-token-list 198,6943
-(defvar unicode-tokens-hash-table 201,7063
-(defvar unicode-tokens-token-match-regexp 204,7179
-(defvar unicode-tokens-uchar-hash-table 207,7291
-(defvar unicode-tokens-uchar-regexp 211,7478
-(defgroup unicode-tokens-faces 236,8084
-(defconst unicode-tokens-font-family-alternatives246,8381
-(defface unicode-tokens-symbol-font-face260,8832
-(defface unicode-tokens-script-font-face278,9472
-(defface unicode-tokens-fraktur-font-face283,9616
-(defface unicode-tokens-serif-font-face288,9741
-(defface unicode-tokens-sans-font-face293,9868
-(defface unicode-tokens-highlight-face298,9990
-(defconst unicode-tokens-fonts307,10352
-(defconst unicode-tokens-fontsymb-properties 316,10569
-(define-widget 'unicode-tokens-token-symbol-map unicode-tokens-token-symbol-map
342,12106
-(define-widget 'unicode-tokens-shortcut-alist unicode-tokens-shortcut-alist
360,12668
-(defconst unicode-tokens-font-lock-extra-managed-props373,12999
-(defun unicode-tokens-font-lock-keywords 377,13153
-(defun unicode-tokens-usable-composition 417,14806
-(defun unicode-tokens-help-echo 430,15185
-(defvar unicode-tokens-show-symbols 434,15349
-(defun unicode-tokens-font-lock-compose-symbol 437,15463
-(defun unicode-tokens-prepend-text-properties-in-match 465,16641
-(defun unicode-tokens-prepend-text-property 479,17220
-(defun unicode-tokens-show-symbols 504,18389
-(defun unicode-tokens-symbs-to-props 512,18699
-(defvar unicode-tokens-show-controls 532,19399
-(defun unicode-tokens-show-controls 535,19490
-(defun unicode-tokens-control-char 548,20075
-(defun unicode-tokens-control-region 557,20514
-(defun unicode-tokens-control-font-lock-keywords 567,21056
-(defvar unicode-tokens-use-shortcuts 578,21386
-(defun unicode-tokens-use-shortcuts 581,21489
-(defun unicode-tokens-map-ordering 599,22095
-(defun unicode-tokens-quail-define-rules 603,22245
-(defun unicode-tokens-insert-token 626,22922
-(defun unicode-tokens-annotate-region 635,23226
-(defun unicode-tokens-insert-control 659,24064
-(defun unicode-tokens-insert-uchar-as-token 669,24513
-(defun unicode-tokens-delete-token-near-point 675,24734
-(defun unicode-tokens-prev-token 689,25296
-(defun unicode-tokens-rotate-token-forward 698,25646
-(defun unicode-tokens-rotate-token-backward 725,26537
-(defun unicode-tokens-replace-shortcut-match 730,26739
-(defun unicode-tokens-replace-shortcuts 738,27041
-(defun unicode-tokens-copy-token 755,27658
-(define-button-type 'unicode-tokens-listunicode-tokens-list
762,27879
-(defun unicode-tokens-list-tokens 768,28083
-(defun unicode-tokens-list-shortcuts 807,29269
-(defun unicode-tokens-encode-in-temp-buffer 827,29912
-(defun unicode-tokens-encode 847,30674
-(defun unicode-tokens-encode-str 852,30895
-(defun unicode-tokens-copy 856,31057
-(defun unicode-tokens-paste 865,31463
-(defvar unicode-tokens-highlight-unicode 881,32006
-(defconst unicode-tokens-unicode-highlight-patterns884,32098
-(defun unicode-tokens-highlight-unicode 888,32267
-(defun unicode-tokens-highlight-unicode-setkeywords 900,32730
-(defun unicode-tokens-initialise 912,33100
-(defvar unicode-tokens-mode-map 924,33552
-(define-minor-mode unicode-tokens-mode927,33649
-(defun unicode-tokens-set-font-var 1016,36674
-(defun unicode-tokens-mouse-set-font 1055,38125
-(defsubst unicode-tokens-face-font-sym 1068,38640
-(defun unicode-tokens-set-font-restart 1072,38820
-(defun unicode-tokens-save-fonts 1079,39100
-(defun unicode-tokens-custom-save-faces 1088,39382
-(define-key unicode-tokens-mode-map 1104,39839
-(define-key unicode-tokens-mode-map 1106,39931
-(define-key unicode-tokens-mode-map1108,40022
-(define-key unicode-tokens-mode-map1110,40128
-(define-key unicode-tokens-mode-map1113,40243
-(define-key unicode-tokens-mode-map1115,40352
-(define-key unicode-tokens-mode-map1117,40460
-(define-key unicode-tokens-mode-map1119,40566
-(defun unicode-tokens-define-menu 1127,40694
+(defvar unicode-chars-alist12,348
+(defun unicode-chars-list-chars 5051,245975
+
+lib/unicode-tokens.el,5174
+(defvar unicode-tokens-token-symbol-map 56,1828
+(defvar unicode-tokens-token-format 75,2450
+(defvar unicode-tokens-token-variant-format-regexp 81,2699
+(defvar unicode-tokens-shortcut-alist 92,3081
+(defvar unicode-tokens-shortcut-replacement-alist 98,3358
+(defvar unicode-tokens-control-region-format-regexp 106,3564
+(defvar unicode-tokens-control-char-format-regexp 113,3932
+(defvar unicode-tokens-control-regions 120,4293
+(defvar unicode-tokens-control-characters 123,4369
+(defvar unicode-tokens-control-char-format 126,4451
+(defvar unicode-tokens-control-region-format-start 129,4564
+(defvar unicode-tokens-control-region-format-end 132,4681
+(defvar unicode-tokens-tokens-customizable-variables 135,4794
+(defconst unicode-tokens-configuration-variables142,4962
+(defun unicode-tokens-config 157,5361
+(defun unicode-tokens-config-var 161,5506
+(defun unicode-tokens-copy-configuration-variables 173,5946
+(defvar unicode-tokens-token-list 201,7162
+(defvar unicode-tokens-hash-table 204,7282
+(defvar unicode-tokens-token-match-regexp 207,7398
+(defvar unicode-tokens-uchar-hash-table 210,7510
+(defvar unicode-tokens-uchar-regexp 214,7697
+(defgroup unicode-tokens-faces 222,7882
+(defconst unicode-tokens-font-family-alternatives232,8179
+(defface unicode-tokens-symbol-font-face246,8627
+(defface unicode-tokens-script-font-face264,9267
+(defface unicode-tokens-fraktur-font-face269,9411
+(defface unicode-tokens-serif-font-face274,9536
+(defface unicode-tokens-sans-font-face279,9663
+(defface unicode-tokens-highlight-face284,9785
+(defconst unicode-tokens-fonts293,10147
+(defconst unicode-tokens-fontsymb-properties302,10364
+(define-widget 'unicode-tokens-token-symbol-map unicode-tokens-token-symbol-map
328,11809
+(define-widget 'unicode-tokens-shortcut-alist unicode-tokens-shortcut-alist
346,12361
+(defconst unicode-tokens-font-lock-extra-managed-props359,12692
+(defun unicode-tokens-font-lock-keywords 363,12846
+(defun unicode-tokens-usable-composition 403,14499
+(defun unicode-tokens-help-echo 416,14876
+(defvar unicode-tokens-show-symbols 420,15040
+(defun unicode-tokens-interpret-composition 423,15154
+(defun unicode-tokens-font-lock-compose-symbol 441,15667
+(defun unicode-tokens-prepend-text-properties-in-match 471,16898
+(defun unicode-tokens-prepend-text-property 485,17476
+(defun unicode-tokens-show-symbols 510,18621
+(defun unicode-tokens-symbs-to-props 518,18931
+(defvar unicode-tokens-show-controls 538,19630
+(defun unicode-tokens-show-controls 541,19721
+(defun unicode-tokens-control-char 554,20306
+(defun unicode-tokens-control-region 563,20745
+(defun unicode-tokens-control-font-lock-keywords 574,21292
+(defvar unicode-tokens-use-shortcuts 585,21616
+(defun unicode-tokens-use-shortcuts 588,21719
+(defun unicode-tokens-map-ordering 606,22325
+(defun unicode-tokens-quail-define-rules 615,22678
+(defun unicode-tokens-insert-token 638,23355
+(defun unicode-tokens-annotate-region 647,23659
+(defun unicode-tokens-insert-control 671,24497
+(defun unicode-tokens-insert-uchar-as-token 681,24946
+(defun unicode-tokens-delete-token-near-point 687,25167
+(defun unicode-tokens-prev-token 701,25729
+(defun unicode-tokens-rotate-token-forward 710,26079
+(defun unicode-tokens-rotate-token-backward 737,26969
+(defun unicode-tokens-replace-shortcut-match 742,27171
+(defun unicode-tokens-replace-shortcuts 751,27541
+(defun unicode-tokens-replace-unicode-match 764,28120
+(defun unicode-tokens-replace-unicode 771,28421
+(defun unicode-tokens-copy-token 787,29001
+(define-button-type 'unicode-tokens-listunicode-tokens-list
794,29222
+(defun unicode-tokens-list-tokens 800,29426
+(defun unicode-tokens-list-shortcuts 839,30610
+(defalias 'unicode-tokens-list-unicode-chars unicode-tokens-list-unicode-chars
857,31248
+(defun unicode-tokens-encode-in-temp-buffer 859,31321
+(defun unicode-tokens-encode 879,32083
+(defun unicode-tokens-encode-str 884,32304
+(defun unicode-tokens-copy 888,32466
+(defun unicode-tokens-paste 897,32872
+(defvar unicode-tokens-highlight-unicode 916,33593
+(defconst unicode-tokens-unicode-highlight-patterns919,33685
+(defun unicode-tokens-highlight-unicode 923,33854
+(defun unicode-tokens-highlight-unicode-setkeywords 935,34317
+(defun unicode-tokens-initialise 947,34686
+(defvar unicode-tokens-mode-map 959,35138
+(define-minor-mode unicode-tokens-mode962,35235
+(defun unicode-tokens-set-font-var 1089,39479
+(defun unicode-tokens-set-font-var-aux 1105,39970
+(defun unicode-tokens-mouse-set-font 1130,41012
+(defsubst unicode-tokens-face-font-sym 1143,41526
+(defun unicode-tokens-set-font-restart 1147,41706
+(defun unicode-tokens-save-fonts 1158,42016
+(defun unicode-tokens-custom-save-faces 1166,42272
+(define-key unicode-tokens-mode-map 1183,42728
+(define-key unicode-tokens-mode-map 1185,42820
+(define-key unicode-tokens-mode-map1187,42911
+(define-key unicode-tokens-mode-map1189,43017
+(define-key unicode-tokens-mode-map1192,43132
+(define-key unicode-tokens-mode-map1194,43241
+(define-key unicode-tokens-mode-map1196,43349
+(define-key unicode-tokens-mode-map1198,43455
+(defun unicode-tokens-customize-submenu 1206,43579
+(defun unicode-tokens-define-menu 1213,43802
 
 mmm/mmm-auto.el,343
 (defvar mmm-autoloaded-classes67,2676
 (defun mmm-autoload-class 89,3439
-(defvar mmm-changed-buffers-list 129,5006
-(defun mmm-major-mode-change 132,5113
-(defun mmm-check-changed-buffers 145,5634
-(defun mmm-mode-on-maybe 155,6007
-(defalias 'mmm-add-find-file-hooks mmm-add-find-file-hooks
167,6425
-(defun mmm-add-find-file-hook 168,6485
-
-mmm/mmm-class.el,416
+(defvar mmm-changed-buffers-list 129,4992
+(defun mmm-major-mode-change 132,5099
+(defun mmm-check-changed-buffers 145,5620
+(defun mmm-mode-on-maybe 155,5979
+(defalias 'mmm-add-find-file-hooks mmm-add-find-file-hooks
167,6383
+(defun mmm-add-find-file-hook 168,6443
+
+mmm/mmm-class.el,414
 (defun mmm-get-class-spec 42,1296
-(defun mmm-get-class-parameter 59,2009
-(defun mmm-set-class-parameter 63,2175
-(defun* mmm-apply-class75,2539
-(defun* mmm-apply-classes90,3177
-(defun* mmm-apply-all 110,3943
-(defun* mmm-ify124,4390
-(defun* mmm-match-region206,7473
-(defun mmm-match->point 267,10162
-(defun mmm-match-and-verify 281,10684
-(defun mmm-get-form 307,11742
-(defun mmm-default-get-form 318,12238
+(defun mmm-get-class-parameter 59,1939
+(defun mmm-set-class-parameter 63,2105
+(defun* mmm-apply-class75,2455
+(defun* mmm-apply-classes90,3072
+(defun* mmm-apply-all 110,3803
+(defun* mmm-ify124,4250
+(defun* mmm-match-region206,7095
+(defun mmm-match->point 267,9384
+(defun mmm-match-and-verify 281,9892
+(defun mmm-get-form 307,10943
+(defun mmm-default-get-form 318,11418
 
 mmm/mmm-cmds.el,712
 (defun mmm-ify-by-class 41,1210
-(defun mmm-ify-region 63,1934
-(defun mmm-ify-by-regexp75,2362
-(defun mmm-parse-buffer 97,3038
-(defun mmm-parse-region 106,3374
-(defun mmm-parse-block 115,3753
-(defun mmm-get-block 132,4504
-(defun mmm-reparse-current-region 146,4835
-(defun mmm-clear-current-region 167,5509
-(defun mmm-clear-regions 172,5673
-(defun mmm-clear-all-regions 177,5819
-(defun* mmm-end-current-region 185,5979
-(defun mmm-narrow-to-submode-region 220,7402
-(defun mmm-insert-region 239,8016
-(defun mmm-insert-by-key 258,8878
-(defun mmm-get-insertion-spec 342,12438
-(defun mmm-insertion-help 369,13517
-(defun mmm-display-insertion-key 379,13887
-(defun mmm-get-all-insertion-keys 401,14709
+(defun mmm-ify-region 63,1822
+(defun mmm-ify-by-regexp75,2243
+(defun mmm-parse-buffer 97,2886
+(defun mmm-parse-region 106,3222
+(defun mmm-parse-block 115,3601
+(defun mmm-get-block 132,4352
+(defun mmm-reparse-current-region 146,4634
+(defun mmm-clear-current-region 167,5210
+(defun mmm-clear-regions 172,5374
+(defun mmm-clear-all-regions 177,5520
+(defun* mmm-end-current-region 185,5680
+(defun mmm-narrow-to-submode-region 220,6928
+(defun mmm-insert-region 239,7542
+(defun mmm-insert-by-key 258,8348
+(defun mmm-get-insertion-spec 342,11613
+(defun mmm-insertion-help 369,12573
+(defun mmm-display-insertion-key 379,12936
+(defun mmm-get-all-insertion-keys 401,13723
 
 mmm/mmm-compat.el,418
 (defvar mmm-xemacs 40,1313
 (defvar mmm-keywords-used49,1616
-(defmacro mmm-regexp-opt 91,2662
-(defvar mmm-evaporate-property110,3311
-(defmacro mmm-set-keymap-default 128,4077
-(defmacro mmm-event-key 137,4519
-(defvar skeleton-positions 146,4738
-(defun mmm-fixup-skeleton 147,4769
-(defmacro mmm-make-temp-buffer 159,5206
-(defvar mmm-font-lock-available-p 172,5602
-(defmacro mmm-set-font-lock-defaults 179,5816
+(defmacro mmm-regexp-opt 91,2632
+(defvar mmm-evaporate-property110,3281
+(defmacro mmm-set-keymap-default 128,4047
+(defmacro mmm-event-key 137,4489
+(defvar skeleton-positions 146,4708
+(defun mmm-fixup-skeleton 147,4739
+(defmacro mmm-make-temp-buffer 159,5162
+(defvar mmm-font-lock-available-p 172,5558
+(defmacro mmm-set-font-lock-defaults 179,5772
 
 mmm/mmm-cweb.el,228
 (defvar mmm-cweb-section-tags38,1117
@@ -2500,72 +2532,38 @@ mmm/mmm-mason.el,410
 (defvar mmm-mason-pseudo-perl-tags-regexp56,1749
 (defvar mmm-mason-tag-names-regexp61,1966
 (defun mmm-mason-verify-inline 66,2186
-(defun mmm-mason-start-line 156,5090
-(defun mmm-mason-end-line 161,5155
-(defun mmm-mason-set-mode-line 168,5249
+(defun mmm-mason-start-line 156,4838
+(defun mmm-mason-end-line 161,4903
+(defun mmm-mason-set-mode-line 168,4997
 
-mmm/mmm-mode.el,1024
+mmm/mmm-mode.el,1023
 (defun mmm-mode 101,3867
 (defun mmm-mode-on 140,5372
-(defun mmm-mode-off 181,7132
-(defvar mmm-mode-map 206,7865
-(defvar mmm-mode-prefix-map 209,7940
-(defvar mmm-mode-menu-map 212,8050
-(defun mmm-define-key 215,8141
-(define-key mmm-mode-prefix-map 239,8896
-(define-key mmm-mode-prefix-map 246,9154
-(define-key mmm-mode-map 249,9265
-(define-key mmm-mode-menu-map 252,9367
-(define-key mmm-mode-menu-map 254,9439
-(define-key mmm-mode-menu-map 256,9498
-(define-key mmm-mode-menu-map 258,9579
-(define-key mmm-mode-menu-map 260,9660
-(define-key mmm-mode-menu-map 262,9747
-(define-key mmm-mode-menu-map 265,9841
-(define-key mmm-mode-menu-map 267,9901
-(define-key mmm-mode-menu-map 270,9992
-(define-key mmm-mode-menu-map 272,10052
-(define-key mmm-mode-menu-map 274,10159
-(define-key mmm-mode-menu-map 276,10244
-(define-key mmm-mode-menu-map 279,10330
-(define-key mmm-mode-menu-map 281,10390
-(define-key mmm-mode-menu-map 283,10503
-(define-key mmm-mode-menu-map 285,10588
-(define-key mmm-mode-map 288,10671
-
-mmm/mmm-noweb.el,1291
-(defvar mmm-noweb-code-mode 44,1352
-(defvar mmm-noweb-quote-mode 50,1649
-(defvar mmm-noweb-quote-string 54,1806
-(defvar mmm-noweb-quote-number 58,1929
-(defvar mmm-noweb-narrowing 62,2045
-(defun mmm-noweb-chunk 68,2176
-(defun mmm-noweb-quote 84,2876
-(defun mmm-noweb-quote-name 89,3042
-(defun mmm-noweb-chunk-name 95,3302
-(defun mmm-noweb-regions 140,4748
-(defun mmm-noweb-narrow-to-doc-chunk 166,5616
-(defun mmm-noweb-fill-chunk 189,6386
-(defun mmm-noweb-fill-paragraph-chunk 208,7070
-(defun mmm-noweb-fill-named-chunk 222,7487
-(defun mmm-noweb-auto-fill-doc-chunk 238,8064
-(defun mmm-noweb-auto-fill-doc-mode 246,8283
-(defun mmm-noweb-auto-fill-code-mode 251,8473
-(defun mmm-noweb-complete-chunk 259,8685
-(defvar mmm-noweb-chunk-history 292,9689
-(defun mmm-noweb-goto-chunk 295,9767
-(defun mmm-noweb-goto-next 307,10091
-(defun mmm-noweb-goto-previous 319,10448
-(defvar mmm-noweb-map 336,10852
-(defvar mmm-noweb-prefix-map 337,10896
-(define-key mmm-noweb-map 338,10947
-(define-key mmm-noweb-prefix-map 347,11390
-(defun mmm-noweb-bind-keys 352,11656
-(defun mmm-syntax-region-list 368,12070
-(defun mmm-syntax-other-regions 377,12426
-(defun mmm-word-other-regions 389,12897
-(defun mmm-space-other-regions 395,13066
-(defun mmm-undo-syntax-other-regions 401,13237
+(defun mmm-mode-off 181,7048
+(defvar mmm-mode-map 206,7760
+(defvar mmm-mode-prefix-map 209,7835
+(defvar mmm-mode-menu-map 212,7945
+(defun mmm-define-key 215,8036
+(define-key mmm-mode-prefix-map 239,8791
+(define-key mmm-mode-prefix-map 246,9049
+(define-key mmm-mode-map 249,9160
+(define-key mmm-mode-menu-map 252,9262
+(define-key mmm-mode-menu-map 254,9334
+(define-key mmm-mode-menu-map 256,9393
+(define-key mmm-mode-menu-map 258,9474
+(define-key mmm-mode-menu-map 260,9555
+(define-key mmm-mode-menu-map 262,9642
+(define-key mmm-mode-menu-map 265,9736
+(define-key mmm-mode-menu-map 267,9796
+(define-key mmm-mode-menu-map 270,9887
+(define-key mmm-mode-menu-map 272,9947
+(define-key mmm-mode-menu-map 274,10054
+(define-key mmm-mode-menu-map 276,10139
+(define-key mmm-mode-menu-map 279,10225
+(define-key mmm-mode-menu-map 281,10285
+(define-key mmm-mode-menu-map 283,10398
+(define-key mmm-mode-menu-map 285,10483
+(define-key mmm-mode-map 288,10566
 
 mmm/mmm-region.el,1643
 (defsubst mmm-overlay-at 54,1749
@@ -2575,42 +2573,42 @@ mmm/mmm-region.el,1643
 (defun mmm-overlays-contained-in 125,4314
 (defun mmm-overlays-overlapping 138,4754
 (defun mmm-sort-overlays 149,5117
-(defvar mmm-current-overlay 158,5387
-(defvar mmm-previous-overlay 163,5602
-(defvar mmm-current-submode 168,5790
-(defvar mmm-previous-submode 173,5990
-(defun mmm-update-current-submode 178,6163
-(defun mmm-set-current-submode 199,6979
-(defun mmm-submode-at 210,7471
-(defun mmm-match-front 219,7746
-(defun mmm-match-back 238,8507
-(defun mmm-front-start 257,9252
-(defun mmm-back-end 265,9556
-(defun mmm-valid-submode-region 278,9903
-(defun* mmm-make-region305,11059
-(defun mmm-make-overlay 431,16430
-(defun mmm-get-face 459,17563
-(defun mmm-clear-overlays 470,17855
-(defun mmm-update-mode-info 486,18322
-(defun mmm-update-submode-region 571,22607
-(defun mmm-add-hooks 588,23365
-(defun mmm-remove-hooks 592,23500
-(defun mmm-get-local-variables-list 598,23627
-(defun mmm-get-locals 618,24547
-(defun mmm-get-saved-local 631,25128
-(defun mmm-set-local-variables 635,25293
-(defun mmm-get-saved-local-variables 646,25734
-(defun mmm-save-changed-local-variables 654,26051
-(defun mmm-clear-local-variables 673,26909
-(defun mmm-enable-font-lock 684,27188
-(defun mmm-update-font-lock-buffer 692,27448
-(defun mmm-refontify-maybe 705,27880
-(defun mmm-submode-changes-in 720,28402
-(defun mmm-regions-in 731,28850
-(defun mmm-regions-alist 745,29420
-(defun mmm-fontify-region 762,30066
-(defun mmm-fontify-region-list 782,31097
-(defun mmm-beginning-of-syntax 804,32013
+(defvar mmm-current-overlay 158,5359
+(defvar mmm-previous-overlay 163,5574
+(defvar mmm-current-submode 168,5762
+(defvar mmm-previous-submode 173,5962
+(defun mmm-update-current-submode 178,6135
+(defun mmm-set-current-submode 199,6930
+(defun mmm-submode-at 210,7373
+(defun mmm-match-front 219,7648
+(defun mmm-match-back 238,8409
+(defun mmm-front-start 257,9154
+(defun mmm-back-end 265,9458
+(defun mmm-valid-submode-region 278,9805
+(defun* mmm-make-region305,10961
+(defun mmm-make-overlay 431,16311
+(defun mmm-get-face 459,17444
+(defun mmm-clear-overlays 470,17736
+(defun mmm-update-mode-info 486,18201
+(defun mmm-update-submode-region 572,21856
+(defun mmm-add-hooks 589,22586
+(defun mmm-remove-hooks 592,22683
+(defun mmm-get-local-variables-list 598,22810
+(defun mmm-get-locals 618,23506
+(defun mmm-get-saved-local 631,24003
+(defun mmm-set-local-variables 635,24168
+(defun mmm-get-saved-local-variables 646,24546
+(defun mmm-save-changed-local-variables 654,24821
+(defun mmm-clear-local-variables 673,25525
+(defun mmm-enable-font-lock 684,25790
+(defun mmm-update-font-lock-buffer 692,26050
+(defun mmm-refontify-maybe 705,26461
+(defun mmm-submode-changes-in 720,26941
+(defun mmm-regions-in 731,27298
+(defun mmm-regions-alist 745,27776
+(defun mmm-fontify-region 762,28303
+(defun mmm-fontify-region-list 782,29299
+(defun mmm-beginning-of-syntax 804,30047
 
 mmm/mmm-rpm.el,154
 (defconst mmm-rpm-sh-start-tags48,1618
@@ -2619,250 +2617,248 @@ mmm/mmm-rpm.el,154
 (defvar mmm-rpm-sh-end-regexp61,2194
 
 mmm/mmm-sample.el,168
-(defvar mmm-here-doc-mode-alist 84,2615
-(defun mmm-here-doc-get-mode 93,3100
-(defun mmm-file-variables-verify 208,6818
-(defun mmm-file-variables-find-back 232,7854
+(defvar mmm-here-doc-mode-alist 84,2601
+(defun mmm-here-doc-get-mode 93,3086
+(defun mmm-file-variables-verify 208,6343
+(defun mmm-file-variables-find-back 232,7148
 
 mmm/mmm-univ.el,34
 (defun mmm-univ-get-mode 38,1205
 
 mmm/mmm-utils.el,282
-(defmacro mmm-valid-buffer 41,1310
-(defmacro mmm-save-all 60,1954
-(defun mmm-format-string 73,2243
-(defun mmm-format-matches 84,2695
-(defmacro mmm-save-keyword 107,3488
-(defmacro mmm-save-keywords 115,3815
-(defun mmm-looking-back-at 128,4348
-(defun mmm-make-marker 145,4916
-
-mmm/mmm-vars.el,2667
-(defgroup mmm 99,3073
-(defvar mmm-c-derived-modes106,3183
-(defvar mmm-save-local-variables 110,3302
-(defvar mmm-buffer-saved-locals 336,10162
-(defvar mmm-region-saved-locals-defaults 341,10362
-(defvar mmm-region-saved-locals-for-dominant 347,10622
-(defgroup mmm-faces 357,10999
-(defcustom mmm-submode-decoration-level 363,11170
-(defface mmm-init-submode-face 381,12042
-(defface mmm-cleanup-submode-face 385,12182
-(defface mmm-declaration-submode-face 389,12319
-(defface mmm-comment-submode-face 393,12465
-(defface mmm-output-submode-face 397,12618
-(defface mmm-special-submode-face 401,12767
-(defface mmm-code-submode-face 405,12931
-(defface mmm-default-submode-face 409,13070
-(defface mmm-delimiter-face 414,13278
-(defcustom mmm-mode-string 421,13404
-(defcustom mmm-submode-mode-line-format 426,13535
-(defvar mmm-primary-mode-display-name 443,14190
-(defvar mmm-buffer-mode-display-name 448,14404
-(defun mmm-set-mode-line 454,14703
-(defvar mmm-classes 478,15511
-(defvar mmm-global-classes 484,15756
-(defcustom mmm-mode-ext-classes-alist 491,15938
-(defun mmm-add-mode-ext-class 510,16756
-(defcustom mmm-major-mode-preferences519,17081
-(defun mmm-add-to-major-mode-preferences 537,17879
-(defun mmm-ensure-modename 553,18665
-(defun mmm-modename->function 562,18975
-(defcustom mmm-delimiter-mode 576,19438
-(defcustom mmm-mode-prefix-key 586,19707
-(defcustom mmm-command-modifiers 591,19834
-(defcustom mmm-insert-modifiers 605,20467
-(defcustom mmm-use-old-command-keys 620,21145
-(defun mmm-use-old-command-keys 630,21609
-(defcustom mmm-mode-hook 638,21808
-(defun mmm-run-constructed-hook 658,22615
-(defun mmm-run-major-hook 666,23001
-(defun mmm-run-submode-hook 669,23078
-(defvar mmm-class-hooks-run 672,23165
-(defun mmm-run-class-hook 677,23337
-(defvar mmm-primary-mode-entry-hook 682,23509
-(defcustom mmm-major-mode-hook 697,24156
-(defun mmm-run-major-mode-hook 711,24787
-(defcustom mmm-global-mode 724,25328
-(defcustom mmm-never-modes740,26023
-(defvar mmm-set-file-name-for-modes 758,26323
-(defvar mmm-mode 769,26682
-(defvar mmm-primary-mode 777,26890
-(defvar mmm-classes-alist 788,27256
-(defun mmm-add-classes 943,35463
-(defun mmm-add-group 948,35628
-(defun mmm-add-to-group 958,36078
-(defconst mmm-version 972,36575
-(defun mmm-version 975,36640
-(defvar mmm-temp-buffer-name 982,36783
-(defvar mmm-interactive-history 988,36913
-(defun mmm-add-to-history 994,37182
-(defun mmm-clear-history 997,37265
-(defvar mmm-mode-ext-classes 1005,37450
-(defun mmm-get-mode-ext-classes 1010,37661
-(defun mmm-clear-mode-ext-classes 1019,38037
-(defun mmm-mode-ext-applies 1023,38162
-(defun mmm-get-all-classes 1037,38646
+(defmacro mmm-valid-buffer 42,1332
+(defmacro mmm-save-all 61,1941
+(defun mmm-format-string 74,2223
+(defun mmm-format-matches 85,2661
+(defmacro mmm-save-keyword 108,3419
+(defmacro mmm-save-keywords 116,3746
+(defun mmm-looking-back-at 129,4244
+(defun mmm-make-marker 146,4784
+
+mmm/mmm-vars.el,2668
+(defgroup mmm 102,3169
+(defvar mmm-c-derived-modes109,3279
+(defvar mmm-save-local-variables113,3398
+(defvar mmm-buffer-saved-locals 339,10179
+(defvar mmm-region-saved-locals-defaults 344,10379
+(defvar mmm-region-saved-locals-for-dominant 350,10639
+(defgroup mmm-faces 360,11016
+(defcustom mmm-submode-decoration-level 366,11187
+(defface mmm-init-submode-face 384,12031
+(defface mmm-cleanup-submode-face 388,12171
+(defface mmm-declaration-submode-face 392,12308
+(defface mmm-comment-submode-face 396,12454
+(defface mmm-output-submode-face 400,12607
+(defface mmm-special-submode-face 404,12756
+(defface mmm-code-submode-face 408,12920
+(defface mmm-default-submode-face 412,13059
+(defface mmm-delimiter-face 417,13267
+(defcustom mmm-mode-string 424,13393
+(defcustom mmm-submode-mode-line-format 429,13524
+(defvar mmm-primary-mode-display-name 446,14179
+(defvar mmm-buffer-mode-display-name 451,14393
+(defun mmm-set-mode-line 457,14692
+(defvar mmm-classes 481,15500
+(defvar mmm-global-classes 487,15745
+(defcustom mmm-mode-ext-classes-alist 494,15927
+(defun mmm-add-mode-ext-class 513,16717
+(defcustom mmm-major-mode-preferences522,17042
+(defun mmm-add-to-major-mode-preferences 540,17770
+(defun mmm-ensure-modename 556,18528
+(defun mmm-modename->function 565,18831
+(defcustom mmm-delimiter-mode 579,19280
+(defcustom mmm-mode-prefix-key 589,19549
+(defcustom mmm-command-modifiers 594,19676
+(defcustom mmm-insert-modifiers 608,20309
+(defcustom mmm-use-old-command-keys 623,20987
+(defun mmm-use-old-command-keys 633,21451
+(defcustom mmm-mode-hook 641,21643
+(defun mmm-run-constructed-hook 661,22450
+(defun mmm-run-major-hook 669,22794
+(defun mmm-run-submode-hook 672,22871
+(defvar mmm-class-hooks-run 675,22958
+(defun mmm-run-class-hook 680,23130
+(defvar mmm-primary-mode-entry-hook 685,23302
+(defcustom mmm-major-mode-hook 700,23949
+(defun mmm-run-major-mode-hook 714,24580
+(defcustom mmm-global-mode 727,25121
+(defcustom mmm-never-modes743,25788
+(defvar mmm-set-file-name-for-modes 761,26088
+(defvar mmm-mode 772,26447
+(defvar mmm-primary-mode 780,26655
+(defvar mmm-classes-alist 791,27021
+(defun mmm-add-classes 946,35228
+(defun mmm-add-group 951,35393
+(defun mmm-add-to-group 961,35766
+(defconst mmm-version 975,36193
+(defun mmm-version 978,36258
+(defvar mmm-temp-buffer-name 985,36401
+(defvar mmm-interactive-history 991,36531
+(defun mmm-add-to-history 997,36800
+(defun mmm-clear-history 1000,36883
+(defvar mmm-mode-ext-classes 1008,37068
+(defun mmm-get-mode-ext-classes 1013,37279
+(defun mmm-clear-mode-ext-classes 1022,37606
+(defun mmm-mode-ext-applies 1026,37731
+(defun mmm-get-all-classes 1040,38110
 
 doc/ProofGeneral.texi,5693
-@node Top164,4909
-@node Preface201,6016
-@node News for Version 4.0News for Version 4.0
224,6605
-@node Future249,7453
-@node Credits280,8752
-@node Introducing Proof GeneralIntroducing Proof General
385,12394
-@node Installing Proof GeneralInstalling Proof General
440,14372
-@node Quick start guideQuick start guide
454,14821
-@node Features of Proof GeneralFeatures of Proof General
498,16942
-@node Supported proof assistantsSupported proof assistants
587,20879
-@node Prerequisites for this manualPrerequisites for this manual
636,22768
-@node Organization of this manualOrganization of this manual
680,24387
-@node Basic Script ManagementBasic Script Management
706,25215
-@node Walkthrough example in IsabelleWalkthrough example in Isabelle
725,25815
-@node Proof scriptsProof scripts
991,36048
-@node Script buffersScript buffers
1034,38168
-@node Locked queue and editing regionsLocked queue and editing regions
1056,38745
-@node Goal-save sequencesGoal-save sequences
1112,40892
-@node Active scripting bufferActive scripting buffer
1149,42378
-@node Summary of Proof General buffersSummary of Proof General buffers
1218,45798
-@node Script editing commandsScript editing commands
1281,48538
-@node Script processing commandsScript processing commands
1361,51496
-@node Proof assistant commandsProof assistant commands
1489,56810
-@node Toolbar commandsToolbar commands
1661,62916
-@node Interrupting during trace outputInterrupting during trace output
1685,63845
-@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
1724,65766
-@node Goals buffer commandsGoals buffer commands
1738,66266
-@node Advanced Script Management and EditingAdvanced Script Management and Editing
1827,69830
-@node Document centred workingDocument centred working
1859,71045
-@node Visibility of completed proofsVisibility of completed proofs
1923,72976
-@node Switching between proof scriptsSwitching between proof scripts
1978,74899
-@node View of processed files View of processed files 
2015,76871
-@node Retracting across filesRetracting across files
2075,79922
-@node Asserting across filesAsserting across files
2088,80553
-@node Automatic multiple file handlingAutomatic multiple file handling
2101,81119
-@node Escaping script managementEscaping script management
2126,82153
-@node Editing featuresEditing features
2184,84356
-@node Support for other PackagesSupport for other Packages
2255,87148
-@node Syntax highlightingSyntax highlighting
2287,88022
-@node Unicode supportUnicode support
2316,89026
-@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)
2472,95261
-@node Support for outline modeSupport for outline mode
2527,97305
-@node Support for completionSupport for completion
2552,98434
-@node Support for tagsSupport for tags
2609,100596
-@node Customizing Proof GeneralCustomizing Proof General
2661,102924
-@node Basic optionsBasic options
2701,104594
-@node How to customizeHow to customize
2725,105352
-@node Display customizationDisplay customization
2772,107319
-@node User optionsUser options
2926,113719
-@node Changing facesChanging faces
3168,122255
-@node Tweaking configuration settingsTweaking configuration settings
3243,124924
-@node Hints and TipsHints and Tips
3300,127450
-@node Adding your own keybindingsAdding your own keybindings
3319,128051
-@node Using file variablesUsing file variables
3383,130638
-@node Using abbreviationsUsing abbreviations
3442,132824
-@node LEGO Proof GeneralLEGO Proof General
3481,134239
-@node LEGO specific commandsLEGO specific commands
3522,135608
-@node LEGO tagsLEGO tags
3542,136063
-@node LEGO customizationsLEGO customizations
3552,136310
-@node Coq Proof GeneralCoq Proof General
3584,137229
-@node Coq-specific commandsCoq-specific commands
3600,137638
-@node Coq-specific variablesCoq-specific variables
3622,138145
-@node Editing multiple proofsEditing multiple proofs
3644,138803
-@node User-loaded tacticsUser-loaded tactics
3668,139911
-@node Holes featureHoles feature
3732,142385
-@node Isabelle Proof GeneralIsabelle Proof General
3759,143672
-@node Choosing logic and starting isabelleChoosing logic and starting isabelle
3790,144841
-@node Isabelle commandsIsabelle commands
3859,147649
-@node Isabelle settingsIsabelle settings
4002,151802
-@node Isabelle customizationsIsabelle customizations
4016,152384
-@node HOL Proof GeneralHOL Proof General
4039,152871
-@node Shell Proof GeneralShell Proof General
4081,154693
-@node Obtaining and InstallingObtaining and Installing
4117,156152
-@node Obtaining Proof GeneralObtaining Proof General
4133,156565
-@node Installing Proof General from tarballInstalling Proof General from tarball
4164,157804
-@node Installing Proof General from RPM packageInstalling Proof General from RPM package
4189,158636
-@node Setting the names of binariesSetting the names of binaries
4204,159044
-@node Notes for syssiesNotes for syssies
4232,159984
-@node Bugs and EnhancementsBugs and Enhancements
4307,163020
-@node References4328,163835
-@node History of Proof GeneralHistory of Proof General
4368,164858
-@node Old News for 3.0Old News for 3.0
4462,169023
-@node Old News for 3.1Old News for 3.1
4532,172717
-@node Old News for 3.2Old News for 3.2
4558,173889
-@node Old News for 3.3Old News for 3.3
4619,176892
-@node Old News for 3.4Old News for 3.4
4638,177789
-@node Old News for 3.5Old News for 3.5
4660,178844
-@node Old News for 3.6Old News for 3.6
4664,178901
-@node Old News for 3.7Old News for 3.7
4669,179001
-@node Function IndexFunction Index
4713,180899
-@node Variable IndexVariable Index
4717,180975
-@node Keystroke IndexKeystroke Index
4721,181055
-@node Concept IndexConcept Index
4725,181121
+@node Top164,4937
+@node Preface201,6044
+@node News for Version 4.0News for Version 4.0
224,6633
+@node Future241,7193
+@node Credits270,8528
+@node Introducing Proof GeneralIntroducing Proof General
380,12340
+@node Installing Proof GeneralInstalling Proof General
435,14318
+@node Quick start guideQuick start guide
449,14767
+@node Features of Proof GeneralFeatures of Proof General
493,16888
+@node Supported proof assistantsSupported proof assistants
582,20825
+@node Prerequisites for this manualPrerequisites for this manual
631,22714
+@node Organization of this manualOrganization of this manual
675,24333
+@node Basic Script ManagementBasic Script Management
701,25161
+@node Walkthrough example in IsabelleWalkthrough example in Isabelle
720,25761
+@node Proof scriptsProof scripts
986,35994
+@node Script buffersScript buffers
1029,38114
+@node Locked queue and editing regionsLocked queue and editing regions
1051,38691
+@node Goal-save sequencesGoal-save sequences
1107,40838
+@node Active scripting bufferActive scripting buffer
1144,42324
+@node Summary of Proof General buffersSummary of Proof General buffers
1213,45744
+@node Script editing commandsScript editing commands
1276,48484
+@node Script processing commandsScript processing commands
1356,51442
+@node Proof assistant commandsProof assistant commands
1483,56735
+@node Toolbar commandsToolbar commands
1655,62840
+@node Interrupting during trace outputInterrupting during trace output
1679,63769
+@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
1718,65690
+@node Goals buffer commandsGoals buffer commands
1733,66202
+@node Advanced Script Management and EditingAdvanced Script Management and Editing
1822,69766
+@node Document centred workingDocument centred working
1854,70981
+@node Visibility of completed proofsVisibility of completed proofs
1920,73085
+@node Switching between proof scriptsSwitching between proof scripts
1975,75008
+@node View of processed files View of processed files 
2012,76980
+@node Retracting across filesRetracting across files
2072,80031
+@node Asserting across filesAsserting across files
2085,80662
+@node Automatic multiple file handlingAutomatic multiple file handling
2098,81228
+@node Escaping script managementEscaping script management
2123,82262
+@node Editing featuresEditing features
2180,84374
+@node Support for other PackagesSupport for other Packages
2251,87166
+@node Syntax highlightingSyntax highlighting
2283,88040
+@node Unicode supportUnicode support
2312,89044
+@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)
2468,95279
+@node Support for outline modeSupport for outline mode
2523,97323
+@node Support for completionSupport for completion
2548,98452
+@node Support for tagsSupport for tags
2605,100614
+@node Customizing Proof GeneralCustomizing Proof General
2657,102942
+@node Basic optionsBasic options
2697,104612
+@node How to customizeHow to customize
2721,105370
+@node Display customizationDisplay customization
2768,107337
+@node User optionsUser options
2922,113736
+@node Changing facesChanging faces
3163,122214
+@node Tweaking configuration settingsTweaking configuration settings
3238,124883
+@node Hints and TipsHints and Tips
3295,127409
+@node Adding your own keybindingsAdding your own keybindings
3314,128010
+@node Using file variablesUsing file variables
3378,130597
+@node Using abbreviationsUsing abbreviations
3437,132783
+@node LEGO Proof GeneralLEGO Proof General
3476,134198
+@node LEGO specific commandsLEGO specific commands
3517,135567
+@node LEGO tagsLEGO tags
3537,136022
+@node LEGO customizationsLEGO customizations
3547,136269
+@node Coq Proof GeneralCoq Proof General
3579,137188
+@node Coq-specific commandsCoq-specific commands
3595,137597
+@node Coq-specific variablesCoq-specific variables
3617,138104
+@node Editing multiple proofsEditing multiple proofs
3639,138762
+@node User-loaded tacticsUser-loaded tactics
3663,139870
+@node Holes featureHoles feature
3727,142344
+@node Isabelle Proof GeneralIsabelle Proof General
3754,143631
+@node Choosing logic and starting isabelleChoosing logic and starting isabelle
3785,144800
+@node Isabelle commandsIsabelle commands
3854,147608
+@node Isabelle settingsIsabelle settings
3997,151761
+@node Isabelle customizationsIsabelle customizations
4011,152343
+@node HOL Proof GeneralHOL Proof General
4034,152830
+@node Shell Proof GeneralShell Proof General
4076,154652
+@node Obtaining and InstallingObtaining and Installing
4112,156111
+@node Obtaining Proof GeneralObtaining Proof General
4128,156524
+@node Installing Proof General from tarballInstalling Proof General from tarball
4159,157763
+@node Installing Proof General from RPM packageInstalling Proof General from RPM package
4184,158595
+@node Setting the names of binariesSetting the names of binaries
4199,159003
+@node Notes for syssiesNotes for syssies
4227,159943
+@node Bugs and EnhancementsBugs and Enhancements
4302,162979
+@node References4323,163794
+@node History of Proof GeneralHistory of Proof General
4363,164817
+@node Old News for 3.0Old News for 3.0
4457,168982
+@node Old News for 3.1Old News for 3.1
4527,172676
+@node Old News for 3.2Old News for 3.2
4553,173848
+@node Old News for 3.3Old News for 3.3
4614,176851
+@node Old News for 3.4Old News for 3.4
4633,177748
+@node Old News for 3.5Old News for 3.5
4655,178803
+@node Old News for 3.6Old News for 3.6
4659,178860
+@node Old News for 3.7Old News for 3.7
4664,178960
+@node Function IndexFunction Index
4708,180858
+@node Variable IndexVariable Index
4712,180934
+@node Keystroke IndexKeystroke Index
4716,181014
+@node Concept IndexConcept Index
4720,181080
 
 doc/PG-adapting.texi,3772
-@node Top155,4687
-@node Introduction192,5796
-@node Future233,7449
-@node Credits269,9045
-@node Beginning with a New ProverBeginning with a New Prover
279,9337
-@node Overview of adding a new proverOverview of adding a new prover
319,11279
-@node Demonstration instance and easy configurationDemonstration instance and easy configuration
397,14587
-@node Major modes used by Proof GeneralMajor modes used by Proof General
466,17978
-@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands
509,19688
-@node Settings for generic user-level commandsSettings for generic user-level commands
524,20234
-@node Menu configurationMenu configuration
569,21966
-@node Toolbar configurationToolbar configuration
593,22883
-@node Proof Script SettingsProof Script Settings
652,25120
-@node Recognizing commands and commentsRecognizing commands and comments
674,25700
-@node Recognizing proofsRecognizing proofs
811,32137
-@node Recognizing other elementsRecognizing other elements
920,36818
-@node Configuring undo behaviourConfiguring undo behaviour
1046,42357
-@node Nested proofsNested proofs
1183,47769
-@node Safe (state-preserving) commandsSafe (state-preserving) commands
1223,49395
-@node Activate scripting hookActivate scripting hook
1246,50348
-@node Automatic multiple filesAutomatic multiple files
1270,51218
-@node Completions1292,52065
-@node Proof Shell SettingsProof Shell Settings
1333,53555
-@node Proof shell commandsProof shell commands
1364,54837
-@node Script input to the shellScript input to the shell
1528,61881
-@node Settings for matching various output from proof processSettings for matching various output from proof process
1593,64839
-@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process
1724,70624
-@node Hooks and other settingsHooks and other settings
1939,80501
-@node Goals Buffer SettingsGoals Buffer Settings
2020,83888
-@node Splash Screen SettingsSplash Screen Settings
2097,86995
-@node Global ConstantsGlobal Constants
2123,87753
-@node Handling Multiple FilesHandling Multiple Files
2149,88594
-@node Configuring Editing SyntaxConfiguring Editing Syntax
2301,96377
-@node Configuring Font LockConfiguring Font Lock
2360,98498
-@node Configuring TokensConfiguring Tokens
2432,101992
-@node Writing More Lisp CodeWriting More Lisp Code
2470,103493
-@node Default values for generic settingsDefault values for generic settings
2487,104138
-@node Adding prover-specific configurationsAdding prover-specific configurations
2517,105221
-@node Useful variablesUseful variables
2560,106503
-@node Useful functions and macrosUseful functions and macros
2575,107002
-@node Internals of Proof GeneralInternals of Proof General
2684,111218
-@node Spans2712,112114
-@node Proof General site configurationProof General site configuration
2724,112436
-@node Configuration variable mechanismsConfiguration variable mechanisms
2804,115482
-@node Global variablesGlobal variables
2925,120926
-@node Proof script modeProof script mode
2995,123474
-@node Proof shell modeProof shell mode
3254,135140
-@node Debugging3684,152105
-@node Plans and IdeasPlans and Ideas
3727,152981
-@node Proof by pointing and similar featuresProof by pointing and similar features
3748,153703
-@node Granularity of atomic command sequencesGranularity of atomic command sequences
3786,155361
-@node Browser mode for script files and theoriesBrowser mode for script files and theories
3831,157586
-@node Demonstration InstantiationsDemonstration Instantiations
3861,158617
-@node demoisa-easy.el3877,159048
-@node demoisa.el3940,161287
-@node Function IndexFunction Index
4095,166272
-@node Variable IndexVariable Index
4099,166348
-@node Concept IndexConcept Index
4108,166527
+@node Top155,4689
+@node Introduction192,5798
+@node Future233,7451
+@node Credits269,9047
+@node Beginning with a New ProverBeginning with a New Prover
279,9339
+@node Overview of adding a new proverOverview of adding a new prover
319,11281
+@node Demonstration instance and easy configurationDemonstration instance and easy configuration
396,14587
+@node Major modes used by Proof GeneralMajor modes used by Proof General
465,17978
+@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands
508,19688
+@node Settings for generic user-level commandsSettings for generic user-level commands
523,20234
+@node Menu configurationMenu configuration
568,21966
+@node Toolbar configurationToolbar configuration
592,22883
+@node Proof Script SettingsProof Script Settings
651,25120
+@node Recognizing commands and commentsRecognizing commands and comments
673,25700
+@node Recognizing proofsRecognizing proofs
810,32137
+@node Recognizing other elementsRecognizing other elements
919,36812
+@node Configuring undo behaviourConfiguring undo behaviour
1045,42344
+@node Nested proofsNested proofs
1182,47733
+@node Safe (state-preserving) commandsSafe (state-preserving) commands
1222,49359
+@node Activate scripting hookActivate scripting hook
1245,50312
+@node Automatic multiple filesAutomatic multiple files
1269,51182
+@node Completions1291,52029
+@node Proof Shell SettingsProof Shell Settings
1332,53519
+@node Proof shell commandsProof shell commands
1363,54801
+@node Script input to the shellScript input to the shell
1527,61845
+@node Settings for matching various output from proof processSettings for matching various output from proof process
1592,64803
+@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process
1709,69932
+@node Hooks and other settingsHooks and other settings
1924,79809
+@node Goals Buffer SettingsGoals Buffer Settings
2005,83196
+@node Splash Screen SettingsSplash Screen Settings
2082,86302
+@node Global ConstantsGlobal Constants
2108,87057
+@node Handling Multiple FilesHandling Multiple Files
2134,87898
+@node Configuring Editing SyntaxConfiguring Editing Syntax
2286,95681
+@node Configuring Font LockConfiguring Font Lock
2343,97798
+@node Configuring TokensConfiguring Tokens
2415,101292
+@node Writing More Lisp CodeWriting More Lisp Code
2453,102793
+@node Default values for generic settingsDefault values for generic settings
2470,103438
+@node Adding prover-specific configurationsAdding prover-specific configurations
2500,104521
+@node Useful variablesUseful variables
2543,105803
+@node Useful functions and macrosUseful functions and macros
2558,106302
+@node Internals of Proof GeneralInternals of Proof General
2667,110525
+@node Spans2695,111421
+@node Proof General site configurationProof General site configuration
2707,111743
+@node Configuration variable mechanismsConfiguration variable mechanisms
2787,114788
+@node Global variablesGlobal variables
2908,120232
+@node Proof script modeProof script mode
2978,122780
+@node Proof shell modeProof shell mode
3216,133387
+@node Debugging3653,150663
+@node Plans and IdeasPlans and Ideas
3696,151539
+@node Proof by pointing and similar featuresProof by pointing and similar features
3717,152261
+@node Granularity of atomic command sequencesGranularity of atomic command sequences
3755,153919
+@node Browser mode for script files and theoriesBrowser mode for script files and theories
3800,156144
+@node Demonstration InstantiationsDemonstration Instantiations
3830,157175
+@node demoisa-easy.el3846,157606
+@node demoisa.el3908,159798
+@node Function IndexFunction Index
4062,164738
+@node Variable IndexVariable Index
4066,164814
+@node Concept IndexConcept Index
4075,164993
 
 generic/proof.el,0
 
-generic/proof-autoloads.el,0
-
 pgshell/pgshell.el,0
 
 isar/isar-autotest.el,0