Updated.

1 files changed, 2365 insertions, 2359 deletions

diff --git a/TAGS b/TAGS
index 06951ed1..94e63aeb 100644
--- a/TAGS
+++ b/TAGS
@@ -28,173 +28,173 @@ coq/coq-db.el,559
 (defun filter-state-preserving 209,7881
 (defun filter-state-changing 214,8035
 (defface coq-solve-tactics-face 221,8256
-(defconst coq-solve-tactics-face 229,8518
-
-coq/coq.el,6513
-(defcustom coq-translate-to-v8 45,1299
-(defun coq-build-prog-args 51,1479
-(defcustom coq-compile-file-command 64,1859
-(defcustom coq-use-makefile 72,2178
-(defcustom coq-default-undo-limit 80,2401
-(defconst coq-shell-init-cmd 85,2529
-(defcustom coq-prog-env 97,2807
-(defconst coq-shell-restart-cmd 105,3059
-(defvar coq-shell-prompt-pattern 112,3319
-(defvar coq-shell-cd 120,3648
-(defvar coq-shell-abort-goal-regexp 124,3803
-(defvar coq-shell-proof-completed-regexp 127,3929
-(defvar coq-goal-regexp130,4081
-(defun coq-library-directory 137,4195
-(defcustom coq-tags 144,4375
-(defconst coq-interrupt-regexp 149,4525
-(defcustom coq-www-home-page 154,4646
-(defvar coq-outline-regexp164,4817
-(defvar coq-outline-heading-end-regexp 171,5031
-(defvar coq-shell-outline-regexp 173,5085
-(defvar coq-shell-outline-heading-end-regexp 174,5135
-(defconst coq-kill-goal-command 179,5245
-(defconst coq-forget-id-command 180,5288
-(defconst coq-back-n-command 181,5335
-(defconst coq-state-preserving-tactics-regexp 185,5479
-(defconst coq-state-changing-commands-regexp187,5580
-(defconst coq-state-preserving-commands-regexp 189,5687
-(defconst coq-commands-regexp 191,5799
-(defvar coq-retractable-instruct-regexp 193,5877
-(defvar coq-non-retractable-instruct-regexp 195,5968
-(defvar coq-keywords-section199,6108
-(defvar coq-section-regexp 202,6202
-(defun coq-set-undo-limit 239,7348
-(defconst coq-keywords-decl-defn-regexp250,7787
-(defun coq-proof-mode-p 254,7937
-(defun coq-is-comment-or-proverprocp 265,8345
-(defun coq-is-goalsave-p 267,8449
-(defun coq-is-module-equal-p 268,8524
-(defun coq-is-def-p 271,8720
-(defun coq-is-decl-defn-p 273,8828
-(defun coq-state-preserving-command-p 278,8995
-(defun coq-command-p 281,9129
-(defun coq-state-preserving-tactic-p 284,9229
-(defun coq-state-changing-tactic-p 289,9377
-(defun coq-state-changing-command-p 296,9611
-(defun coq-section-or-module-start-p 303,9957
-(defun build-list-id-from-string 312,10198
-(defun coq-last-prompt-info 325,10728
-(defun coq-last-prompt-info-safe 337,11269
-(defvar coq-last-but-one-statenum 343,11526
-(defvar coq-last-but-one-proofnum 349,11824
-(defvar coq-last-but-one-proofstack 352,11922
-(defun coq-get-span-statenum 355,12032
-(defun coq-get-span-proofnum 360,12147
-(defun coq-get-span-proofstack 365,12262
-(defun coq-set-span-statenum 370,12406
-(defun coq-get-span-goalcmd 375,12537
-(defun coq-set-span-goalcmd 380,12651
-(defun coq-set-span-proofnum 385,12781
-(defun coq-set-span-proofstack 390,12912
-(defun proof-last-locked-span 395,13072
-(defun coq-set-state-infos 410,13676
-(defun count-not-intersection 450,15755
-(defun  coq-find-and-forget-v81 481,17009
-(defun coq-find-and-forget-v80 509,18141
-(defun coq-find-and-forget 604,22840
-(defvar coq-current-goal 617,23380
-(defun coq-goal-hyp 620,23445
-(defun coq-state-preserving-p 633,23878
-(defconst notation-print-kinds-table 647,24383
-(defun coq-PrintScope 651,24551
-(defun coq-guess-or-ask-for-string 670,25107
-(defun coq-ask-do 684,25650
-(defun coq-SearchIsos 693,26038
-(defun coq-SearchConstant 699,26271
-(defun coq-SearchRewrite 703,26364
-(defun coq-SearchAbout 707,26462
-(defun coq-Print 711,26554
-(defun coq-About 715,26676
-(defun coq-LocateConstant 719,26793
-(defun coq-LocateLibrary 725,26928
-(defun coq-addquotes 731,27078
-(defun coq-LocateNotation 733,27126
-(defun coq-Pwd 740,27325
-(defun coq-Inspect 746,27457
-(defun coq-PrintSection(750,27557
-(defun coq-Print-implicit 754,27650
-(defun coq-Check 759,27801
-(defun coq-Show 764,27909
-(defun coq-Compile 778,28352
-(defun coq-guess-command-line 792,28672
-(defun coq-mode-config 828,30322
-(defvar coq-last-hybrid-pre-string 936,34276
-(defun coq-hybrid-ouput-goals-response-p 939,34455
-(defun coq-hybrid-ouput-goals-response 945,34713
-(defun coq-shell-mode-config 966,35673
-(defun coq-goals-mode-config 1011,37788
-(defun coq-response-config 1018,38032
-(defpacustom print-fully-explicit 1043,38857
-(defpacustom print-implicit 1048,39006
-(defpacustom print-coercions 1053,39173
-(defpacustom print-match-wildcards 1058,39318
-(defpacustom print-elim-types 1063,39499
-(defpacustom printing-depth 1068,39666
-(defpacustom undo-depth 1073,39828
-(defpacustom time-commands 1078,39976
-(defpacustom undo-limit 1082,40087
-(defpacustom auto-compile-vos 1087,40190
-(defun coq-maybe-compile-buffer 1116,41306
-(defun coq-ancestors-of 1153,42840
-(defun coq-all-ancestors-of 1176,43807
-(defconst coq-require-command-regexp 1188,44200
-(defun coq-process-require-command 1193,44409
-(defun coq-included-children 1198,44536
-(defun coq-process-file 1219,45375
-(defun coq-preprocessing 1234,45914
-(defun coq-fake-constant-markup 1249,46333
-(defun coq-create-span-menu 1270,47139
-(defconst module-kinds-table 1287,47638
-(defconst modtype-kinds-table1291,47788
-(defun coq-insert-section-or-module 1295,47917
-(defconst reqkinds-kinds-table1318,48777
-(defun coq-insert-requires 1323,48922
-(defun coq-end-Section 1339,49428
-(defun coq-insert-intros 1357,50012
-(defun coq-insert-infoH-hook 1370,50537
-(defun coq-insert-as 1374,50615
-(defun coq-insert-match 1395,51364
-(defun coq-insert-tactic 1427,52542
-(defun coq-insert-tactical 1433,52781
-(defun coq-insert-command 1439,53030
-(defun coq-insert-term 1445,53274
-(define-key coq-keymap 1451,53471
-(define-key coq-keymap 1452,53529
-(define-key coq-keymap 1453,53586
-(define-key coq-keymap 1454,53655
-(define-key coq-keymap 1455,53711
-(define-key coq-keymap 1456,53760
-(define-key coq-keymap 1457,53818
-(define-key coq-keymap 1459,53879
-(define-key coq-keymap 1460,53938
-(define-key coq-keymap 1462,54002
-(define-key coq-keymap 1463,54062
-(define-key coq-keymap 1465,54118
-(define-key coq-keymap 1466,54168
-(define-key coq-keymap 1467,54218
-(define-key coq-keymap 1468,54268
-(define-key coq-keymap 1469,54322
-(define-key coq-keymap 1470,54381
-(defvar last-coq-error-location 1478,54512
-(defun coq-get-last-error-location 1487,54911
-(defun coq-highlight-error 1534,57296
-(defvar coq-allow-highlight-error 1570,58599
-(defun coq-decide-highlight-error 1576,58865
-(defun coq-highlight-error-hook 1580,58987
-(defun first-word-of-buffer 1591,59380
-(defun coq-show-first-goal 1599,59583
-(defvar coq-modeline-string2 1616,60278
-(defvar coq-modeline-string1 1617,60322
-(defvar coq-modeline-string0 1618,60365
-(defun coq-build-subgoals-string 1619,60410
-(defun coq-update-minor-mode-alist 1624,60578
-(defun is-not-split-vertic 1650,61646
-(defun optim-resp-windows 1659,62085
+(defconst coq-solve-tactics-face 229,8513
+
+coq/coq.el,6514
+(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 681,25392
+(defun coq-ask-do 695,25935
+(defun coq-SearchIsos 704,26323
+(defun coq-SearchConstant 710,26556
+(defun coq-SearchRewrite 714,26649
+(defun coq-SearchAbout 718,26747
+(defun coq-Print 722,26839
+(defun coq-About 726,26961
+(defun coq-LocateConstant 730,27078
+(defun coq-LocateLibrary 736,27213
+(defun coq-addquotes 742,27363
+(defun coq-LocateNotation 744,27411
+(defun coq-Pwd 751,27610
+(defun coq-Inspect 757,27742
+(defun coq-PrintSection(761,27842
+(defun coq-Print-implicit 765,27935
+(defun coq-Check 770,28086
+(defun coq-Show 775,28194
+(defun coq-Compile 789,28637
+(defun coq-guess-command-line 803,28957
+(defun coq-mode-config 841,30673
+(defvar coq-last-hybrid-pre-string 949,34627
+(defun coq-hybrid-ouput-goals-response-p 952,34806
+(defun coq-hybrid-ouput-goals-response 958,35064
+(defun coq-shell-mode-config 979,36024
+(defun coq-goals-mode-config 1024,38139
+(defun coq-response-config 1031,38383
+(defpacustom print-fully-explicit 1056,39208
+(defpacustom print-implicit 1061,39357
+(defpacustom print-coercions 1066,39524
+(defpacustom print-match-wildcards 1071,39669
+(defpacustom print-elim-types 1076,39850
+(defpacustom printing-depth 1081,40017
+(defpacustom undo-depth 1086,40179
+(defpacustom time-commands 1091,40327
+(defpacustom undo-limit 1095,40438
+(defpacustom auto-compile-vos 1100,40541
+(defun coq-maybe-compile-buffer 1129,41657
+(defun coq-ancestors-of 1166,43191
+(defun coq-all-ancestors-of 1189,44158
+(defconst coq-require-command-regexp 1201,44551
+(defun coq-process-require-command 1206,44760
+(defun coq-included-children 1211,44887
+(defun coq-process-file 1232,45726
+(defun coq-preprocessing 1247,46265
+(defun coq-fake-constant-markup 1262,46684
+(defun coq-create-span-menu 1283,47490
+(defconst module-kinds-table 1300,47989
+(defconst modtype-kinds-table1304,48139
+(defun coq-insert-section-or-module 1308,48268
+(defconst reqkinds-kinds-table1331,49128
+(defun coq-insert-requires 1336,49273
+(defun coq-end-Section 1352,49779
+(defun coq-insert-intros 1370,50363
+(defun coq-insert-infoH-hook 1383,50888
+(defun coq-insert-as 1387,50966
+(defun coq-insert-match 1408,51715
+(defun coq-insert-tactic 1440,52893
+(defun coq-insert-tactical 1446,53132
+(defun coq-insert-command 1452,53381
+(defun coq-insert-term 1458,53625
+(define-key coq-keymap 1464,53822
+(define-key coq-keymap 1465,53880
+(define-key coq-keymap 1466,53937
+(define-key coq-keymap 1467,54006
+(define-key coq-keymap 1468,54062
+(define-key coq-keymap 1469,54111
+(define-key coq-keymap 1470,54169
+(define-key coq-keymap 1472,54230
+(define-key coq-keymap 1473,54289
+(define-key coq-keymap 1475,54353
+(define-key coq-keymap 1476,54413
+(define-key coq-keymap 1478,54469
+(define-key coq-keymap 1479,54519
+(define-key coq-keymap 1480,54569
+(define-key coq-keymap 1481,54619
+(define-key coq-keymap 1482,54673
+(define-key coq-keymap 1483,54732
+(defvar last-coq-error-location 1491,54863
+(defun coq-get-last-error-location 1500,55262
+(defun coq-highlight-error 1547,57647
+(defvar coq-allow-highlight-error 1583,58950
+(defun coq-decide-highlight-error 1589,59216
+(defun coq-highlight-error-hook 1593,59338
+(defun first-word-of-buffer 1604,59731
+(defun coq-show-first-goal 1612,59934
+(defvar coq-modeline-string2 1629,60629
+(defvar coq-modeline-string1 1630,60673
+(defvar coq-modeline-string0 1631,60716
+(defun coq-build-subgoals-string 1632,60761
+(defun coq-update-minor-mode-alist 1637,60929
+(defun is-not-split-vertic 1663,61997
+(defun optim-resp-windows 1672,62436
 
 coq/coq-indent.el,2222
 (defconst coq-any-command-regexp17,315
@@ -250,82 +250,82 @@ coq/coq-indent.el,2222
 (defun coq-indent-region 720,28893
 
 coq/coq-local-vars.el,280
-(defconst coq-local-vars-doc 17,306
-(defun coq-insert-coq-prog-name 75,2832
-(defun coq-read-directory 86,3305
-(defun coq-extract-directories-from-args 110,4408
-(defun coq-ask-prog-args 125,4960
-(defun coq-ask-prog-name 147,6064
-(defun coq-ask-insert-coq-prog-name 165,6819
+(defconst coq-local-vars-doc 17,305
+(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,2666
-(defcustom coq-prog-name 13,422
-(defvar coq-version-is-V8 34,1421
-(defvar coq-version-is-V8-0 36,1500
-(defvar coq-version-is-V8-1 43,1878
-(defun coq-determine-version 52,2311
-(defcustom coq-user-tactics-db 98,4217
-(defcustom coq-user-commands-db 115,4730
-(defcustom coq-user-tacticals-db 131,5249
-(defcustom coq-user-solve-tactics-db 147,5770
-(defcustom coq-user-reserved-db 165,6291
-(defvar coq-tactics-db183,6822
-(defvar coq-solve-tactics-db338,14890
-(defvar coq-tacticals-db362,15737
-(defvar coq-decl-db386,16624
-(defvar coq-defn-db408,17842
-(defvar coq-goal-starters-db461,21828
-(defvar coq-other-commands-db488,23383
-(defvar coq-commands-db612,32580
-(defvar coq-terms-db619,32806
-(defun coq-count-match 683,35458
-(defun coq-goal-command-str-v80-p 702,36321
-(defun coq-module-opening-p 725,37194
-(defun coq-section-command-p 736,37610
-(defun coq-goal-command-str-v81-p 740,37707
-(defun coq-goal-command-p-v81 755,38376
-(defun coq-goal-command-str-p 765,38716
-(defun coq-goal-command-p 775,39082
-(defvar coq-keywords-save-strict783,39394
-(defvar coq-keywords-save792,39507
-(defun coq-save-command-p 796,39585
-(defvar coq-keywords-kill-goal 805,39879
-(defvar coq-keywords-state-changing-misc-commands809,39970
-(defvar coq-keywords-goal812,40095
-(defvar coq-keywords-decl815,40178
-(defvar coq-keywords-defn818,40252
-(defvar coq-keywords-state-changing-commands822,40327
-(defvar coq-keywords-state-preserving-commands831,40588
-(defvar coq-keywords-commands836,40804
-(defvar coq-solve-tactics841,40953
-(defvar coq-tacticals845,41074
-(defvar coq-reserved851,41213
-(defvar coq-state-changing-tactics862,41542
-(defvar coq-state-preserving-tactics865,41651
-(defvar coq-tactics869,41765
-(defvar coq-retractable-instruct872,41854
-(defvar coq-non-retractable-instruct875,41964
-(defvar coq-keywords879,42092
-(defvar coq-symbols886,42260
-(defvar coq-error-regexp 905,42473
-(defvar coq-id 908,42701
-(defvar coq-id-shy 909,42726
-(defvar coq-ids 911,42780
-(defun coq-first-abstr-regexp 913,42821
-(defcustom coq-variable-highlight-enable 916,42916
-(defvar coq-font-lock-terms922,43043
-(defconst coq-save-command-regexp-strict943,44043
-(defconst coq-save-command-regexp947,44210
-(defconst coq-save-with-hole-regexp951,44363
-(defconst coq-goal-command-regexp955,44522
-(defconst coq-goal-with-hole-regexp958,44622
-(defconst coq-decl-with-hole-regexp962,44755
-(defconst coq-defn-with-hole-regexp969,45004
-(defconst coq-with-with-hole-regexp979,45293
-(defvar coq-font-lock-keywords-1985,45586
-(defvar coq-font-lock-keywords 1011,46902
-(defun coq-init-syntax-table 1013,46960
-(defconst coq-generic-expression1042,47859
+(defcustom coq-prog-name 13,421
+(defvar coq-version-is-V8 34,1420
+(defvar coq-version-is-V8-0 36,1499
+(defvar coq-version-is-V8-1 43,1877
+(defun coq-determine-version 52,2310
+(defcustom coq-user-tactics-db 98,4216
+(defcustom coq-user-commands-db 115,4729
+(defcustom coq-user-tacticals-db 131,5248
+(defcustom coq-user-solve-tactics-db 147,5769
+(defcustom coq-user-reserved-db 165,6290
+(defvar coq-tactics-db183,6821
+(defvar coq-solve-tactics-db338,14889
+(defvar coq-tacticals-db362,15736
+(defvar coq-decl-db386,16623
+(defvar coq-defn-db408,17841
+(defvar coq-goal-starters-db461,21827
+(defvar coq-other-commands-db488,23382
+(defvar coq-commands-db612,32579
+(defvar coq-terms-db619,32805
+(defun coq-count-match 683,35457
+(defun coq-goal-command-str-v80-p 702,36320
+(defun coq-module-opening-p 725,37193
+(defun coq-section-command-p 736,37609
+(defun coq-goal-command-str-v81-p 740,37706
+(defun coq-goal-command-p-v81 755,38375
+(defun coq-goal-command-str-p 765,38715
+(defun coq-goal-command-p 775,39081
+(defvar coq-keywords-save-strict783,39393
+(defvar coq-keywords-save792,39506
+(defun coq-save-command-p 796,39584
+(defvar coq-keywords-kill-goal 805,39878
+(defvar coq-keywords-state-changing-misc-commands809,39969
+(defvar coq-keywords-goal812,40094
+(defvar coq-keywords-decl815,40177
+(defvar coq-keywords-defn818,40251
+(defvar coq-keywords-state-changing-commands822,40326
+(defvar coq-keywords-state-preserving-commands831,40587
+(defvar coq-keywords-commands836,40803
+(defvar coq-solve-tactics841,40952
+(defvar coq-tacticals845,41073
+(defvar coq-reserved851,41212
+(defvar coq-state-changing-tactics862,41541
+(defvar coq-state-preserving-tactics865,41650
+(defvar coq-tactics869,41764
+(defvar coq-retractable-instruct872,41853
+(defvar coq-non-retractable-instruct875,41963
+(defvar coq-keywords879,42091
+(defvar coq-symbols886,42259
+(defvar coq-error-regexp 905,42472
+(defvar coq-id 908,42700
+(defvar coq-id-shy 909,42725
+(defvar coq-ids 911,42779
+(defun coq-first-abstr-regexp 913,42820
+(defcustom coq-variable-highlight-enable 916,42915
+(defvar coq-font-lock-terms922,43042
+(defconst coq-save-command-regexp-strict943,44042
+(defconst coq-save-command-regexp947,44209
+(defconst coq-save-with-hole-regexp951,44362
+(defconst coq-goal-command-regexp955,44521
+(defconst coq-goal-with-hole-regexp958,44621
+(defconst coq-decl-with-hole-regexp962,44754
+(defconst coq-defn-with-hole-regexp969,45003
+(defconst coq-with-with-hole-regexp979,45292
+(defvar coq-font-lock-keywords-1985,45585
+(defvar coq-font-lock-keywords 1011,46901
+(defun coq-init-syntax-table 1013,46959
+(defconst coq-generic-expression1042,47858
 
 coq/coq-unicode-tokens.el,290
 (defconst coq-token-format 18,631
@@ -338,345 +338,344 @@ coq/coq-unicode-tokens.el,290
 (defcustom coq-shortcut-alist44,1557
 
 demoisa/demoisa.el,349
-(defcustom isabelledemo-prog-name 54,1809
-(defcustom isabelledemo-web-page59,1931
-(defun demoisa-config 70,2161
-(defun demoisa-shell-config 91,2953
-(define-derived-mode demoisa-mode 117,3930
-(define-derived-mode demoisa-shell-mode 122,4053
-(define-derived-mode demoisa-response-mode 127,4196
-(define-derived-mode demoisa-goals-mode 131,4323
+(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,775
-(defcustom isabelle-web-page30,903
-(defcustom isa-isatool-command39,1120
-(defvar isatool-not-found 57,1779
-(defun isa-set-isatool-command 60,1892
-(defun isa-shell-command-to-string 83,2888
-(defun isa-getenv 89,3112
-(defcustom isabelle-program-name-override 109,3799
-(defvar isabelle-prog-name 126,4383
-(defun isa-tool-list-logics 129,4493
-(defcustom isabelle-logics-available 136,4730
-(defcustom isabelle-chosen-logic 146,5066
-(defvar isabelle-chosen-logic-prev 162,5650
-(defun isabelle-hack-local-variables-function 165,5772
-(defun isabelle-set-prog-name 177,6213
-(defun isabelle-choose-logic 202,7372
-(defun isa-view-doc 221,8134
-(defun isa-tool-list-docs 230,8398
-(defconst isabelle-verbatim-regexp 257,9430
-(defun isabelle-verbatim 260,9572
-(defcustom isabelle-refresh-logics 267,9733
-(defvar isabelle-docs-menu 275,10060
-(defvar isabelle-logics-menu-entries 282,10346
-(defun isabelle-logics-menu-calculate 285,10419
-(defvar isabelle-time-to-refresh-logics 304,10982
-(defun isabelle-logics-menu-refresh 308,11077
-(defun isabelle-menu-bar-update-logics 323,11710
-(defun isabelle-load-isar-keywords 339,12340
-(defun isabelle-convert-idmarkup-to-subterm 360,13056
-(defun isabelle-create-span-menu 384,14067
-(defun isabelle-xml-sml-escapes 400,14509
-(defun isabelle-process-pgip 403,14610
-
-isar/isar.el,1204
-(defcustom isar-keywords-name 31,724
-(defpgdefault completion-table 48,1247
-(defcustom isar-web-page50,1300
-(defun isar-strip-terminators 64,1650
-(defun isar-markup-ml 77,2027
-(defun isar-mode-config-set-variables 82,2162
-(defun isar-shell-mode-config-set-variables 151,5341
-(defun isar-remove-file 242,9084
-(defun isar-shell-compute-new-files-list 252,9447
-(define-derived-mode isar-shell-mode 268,9968
-(define-derived-mode isar-response-mode 273,10091
-(define-derived-mode isar-goals-mode 278,10273
-(define-derived-mode isar-mode 283,10448
-(defpgdefault menu-entries340,12483
-(defpgdefault help-menu-entries 370,13765
-(defun isar-count-undos 373,13841
-(defun isar-find-and-forget 400,14955
-(defun isar-goal-command-p 439,16535
-(defun isar-global-save-command-p 444,16712
-(defvar isar-current-goal 465,17573
-(defun isar-state-preserving-p 468,17639
-(defvar isar-shell-current-line-width 493,18836
-(defun isar-shell-adjust-line-width 498,19028
-(defun isar-preprocessing 523,19932
-(defun isar-mode-config 546,21199
-(defun isar-shell-mode-config 557,21757
-(defun isar-response-mode-config 563,21954
-(defun isar-goals-mode-config 569,22135
-(defun isar-goalhyplit-test 577,22402
+(defgroup isabelle 26,776
+(defcustom isabelle-web-page30,904
+(defcustom isa-isatool-command39,1121
+(defvar isatool-not-found 57,1780
+(defun isa-set-isatool-command 60,1893
+(defun isa-shell-command-to-string 83,2889
+(defun isa-getenv 89,3113
+(defcustom isabelle-program-name-override 109,3800
+(defvar isabelle-prog-name 126,4384
+(defun isa-tool-list-logics 129,4494
+(defcustom isabelle-logics-available 136,4731
+(defcustom isabelle-chosen-logic 146,5067
+(defvar isabelle-chosen-logic-prev 162,5651
+(defun isabelle-hack-local-variables-function 165,5773
+(defun isabelle-set-prog-name 177,6214
+(defun isabelle-choose-logic 202,7373
+(defun isa-view-doc 221,8135
+(defun isa-tool-list-docs 230,8399
+(defconst isabelle-verbatim-regexp 257,9431
+(defun isabelle-verbatim 260,9573
+(defcustom isabelle-refresh-logics 267,9734
+(defvar isabelle-docs-menu 275,10061
+(defvar isabelle-logics-menu-entries 282,10347
+(defun isabelle-logics-menu-calculate 285,10420
+(defvar isabelle-time-to-refresh-logics 306,11062
+(defun isabelle-logics-menu-refresh 310,11157
+(defun isabelle-menu-bar-update-logics 325,11790
+(defun isabelle-load-isar-keywords 341,12420
+(defun isabelle-convert-idmarkup-to-subterm 362,13136
+(defun isabelle-create-span-menu 386,14147
+(defun isabelle-xml-sml-escapes 402,14589
+(defun isabelle-process-pgip 405,14690
+
+isar/isar.el,1202
+(defcustom isar-keywords-name 31,727
+(defpgdefault completion-table 48,1250
+(defcustom isar-web-page50,1303
+(defun isar-strip-terminators 64,1653
+(defun isar-markup-ml 77,2030
+(defun isar-mode-config-set-variables 82,2165
+(defun isar-shell-mode-config-set-variables 151,5337
+(defun isar-remove-file 239,8775
+(defun isar-shell-compute-new-files-list 249,9138
+(define-derived-mode isar-shell-mode 265,9659
+(define-derived-mode isar-response-mode 270,9782
+(define-derived-mode isar-goals-mode 275,9964
+(define-derived-mode isar-mode 280,10139
+(defpgdefault menu-entries337,12174
+(defpgdefault help-menu-entries 367,13456
+(defun isar-count-undos 370,13532
+(defun isar-find-and-forget 397,14646
+(defun isar-goal-command-p 436,16226
+(defun isar-global-save-command-p 441,16403
+(defvar isar-current-goal 462,17264
+(defun isar-state-preserving-p 465,17330
+(defvar isar-shell-current-line-width 490,18527
+(defun isar-shell-adjust-line-width 495,18719
+(defun isar-preprocessing 520,19623
+(defun isar-mode-config 543,20890
+(defun isar-shell-mode-config 554,21448
+(defun isar-response-mode-config 560,21645
+(defun isar-goals-mode-config 566,21826
+(defun isar-goalhyplit-test 574,22093
 
 isar/isar-find-theorems.el,778
-(defun isar-find-theorems-minibuffer 18,712
-(defun isar-find-theorems-form 32,1331
-(defvar isar-find-theorems-data 74,3131
-(defvar isar-find-theorems-widget-number 88,3466
-(defvar isar-find-theorems-widget-pattern 91,3564
-(defvar isar-find-theorems-widget-intro 94,3656
-(defvar isar-find-theorems-widget-elim 97,3742
-(defvar isar-find-theorems-widget-dest 100,3826
-(defvar isar-find-theorems-widget-name 103,3910
-(defvar isar-find-theorems-widget-simp 106,3997
-(defun isar-find-theorems-create-searchform111,4143
-(defun isar-find-theorems-create-help 251,8758
-(defun isar-find-theorems-submit-searchform294,10930
-(defun isar-find-theorems-parse-criteria 372,13307
-(defun isar-find-theorems-parse-number 465,16407
-(defun isar-find-theorems-filter-empty 475,16684
+(defun isar-find-theorems-minibuffer 18,713
+(defun isar-find-theorems-form 32,1332
+(defvar isar-find-theorems-data 74,3132
+(defvar isar-find-theorems-widget-number 88,3467
+(defvar isar-find-theorems-widget-pattern 91,3565
+(defvar isar-find-theorems-widget-intro 94,3657
+(defvar isar-find-theorems-widget-elim 97,3743
+(defvar isar-find-theorems-widget-dest 100,3827
+(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
 
 isar/isar-keywords.el,1052
-(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
+(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,697
-(defconst isar-start-sml-regexp 35,1130
-
-isar/isar-syntax.el,3456
-(defconst isar-script-syntax-table-entries20,475
-(defconst isar-script-syntax-table-alist44,877
-(defun isar-init-syntax-table 53,1167
-(defun isar-init-output-syntax-table 61,1414
-(defconst isar-keyword-begin 77,1861
-(defconst isar-keyword-end 78,1899
-(defconst isar-keywords-theory-enclose80,1934
-(defconst isar-keywords-theory85,2079
-(defconst isar-keywords-save90,2224
-(defconst isar-keywords-proof-enclose95,2353
-(defconst isar-keywords-proof101,2535
-(defconst isar-keywords-proof-context108,2740
-(defconst isar-keywords-local-goal112,2854
-(defconst isar-keywords-proper116,2966
-(defconst isar-keywords-improper121,3099
-(defconst isar-keywords-outline126,3245
-(defconst isar-keywords-fume129,3310
-(defconst isar-keywords-indent-open136,3528
-(defconst isar-keywords-indent-close142,3712
-(defconst isar-keywords-indent-enclose146,3817
-(defun isar-regexp-simple-alt 155,4032
-(defun isar-ids-to-regexp 175,4792
-(defconst isar-ext-first 209,6198
-(defconst isar-ext-rest 210,6265
-(defconst isar-long-id-stuff 212,6337
-(defconst isar-id 213,6411
-(defconst isar-idx 214,6481
-(defconst isar-string 216,6540
-(defconst isar-any-command-regexp218,6600
-(defconst isar-name-regexp222,6734
-(defconst isar-improper-regexp228,7029
-(defconst isar-save-command-regexp232,7177
-(defconst isar-global-save-command-regexp235,7278
-(defconst isar-goal-command-regexp238,7392
-(defconst isar-local-goal-command-regexp241,7500
-(defconst isar-comment-start 244,7613
-(defconst isar-comment-end 245,7648
-(defconst isar-comment-start-regexp 246,7681
-(defconst isar-comment-end-regexp 247,7752
-(defconst isar-string-start-regexp 249,7820
-(defconst isar-string-end-regexp 250,7872
-(defconst isar-antiq-regexp259,8125
-(defconst isar-nesting-regexp266,8286
-(defun isar-nesting 269,8384
-(defun isar-match-nesting 281,8805
-(defface isabelle-class-name-face293,9136
-(defface isabelle-tfree-name-face301,9319
-(defface isabelle-tvar-name-face309,9508
-(defface isabelle-free-name-face317,9696
-(defface isabelle-bound-name-face325,9880
-(defface isabelle-var-name-face333,10067
-(defconst isabelle-class-name-face 341,10254
-(defconst isabelle-tfree-name-face 342,10316
-(defconst isabelle-tvar-name-face 343,10378
-(defconst isabelle-free-name-face 344,10439
-(defconst isabelle-bound-name-face 345,10500
-(defconst isabelle-var-name-face 346,10562
-(defvar isar-font-lock-keywords-1349,10624
-(defun isar-output-flk 366,11675
-(defvar isar-output-font-lock-keywords-1372,11927
-(defvar isar-goals-font-lock-keywords390,13029
-(defconst isar-undo 424,13708
-(defun isar-remove 426,13751
-(defun isar-undos 429,13826
-(defun isar-cannot-undo 433,13932
-(defconst isar-theory-start-regexp436,14002
-(defconst isar-end-regexp442,14167
-(defconst isar-undo-fail-regexp446,14268
-(defconst isar-undo-skip-regexp450,14372
-(defconst isar-undo-ignore-regexp453,14493
-(defconst isar-undo-remove-regexp456,14558
-(defconst isar-any-entity-regexp464,14733
-(defconst isar-named-entity-regexp469,14920
-(defconst isar-unnamed-entity-regexp474,15097
-(defconst isar-next-entity-regexps477,15199
-(defconst isar-generic-expression485,15510
-(defconst isar-indent-any-regexp496,15827
-(defconst isar-indent-inner-regexp498,15920
-(defconst isar-indent-enclose-regexp500,15986
-(defconst isar-indent-open-regexp502,16102
-(defconst isar-indent-close-regexp504,16212
-(defconst isar-outline-regexp510,16349
-(defconst isar-outline-heading-end-regexp 514,16502
-
-isar/isar-unicode-tokens.el,1008
+(defconst isar-start-latex-regexp 23,698
+(defconst isar-start-sml-regexp 35,1131
+
+isar/isar-syntax.el,3494
+(defconst isar-script-syntax-table-entries20,478
+(defconst isar-script-syntax-table-alist44,880
+(defun isar-init-syntax-table 53,1170
+(defun isar-init-output-syntax-table 61,1417
+(defconst isar-keyword-begin 77,1864
+(defconst isar-keyword-end 78,1902
+(defconst isar-keywords-theory-enclose80,1937
+(defconst isar-keywords-theory85,2082
+(defconst isar-keywords-save90,2227
+(defconst isar-keywords-proof-enclose95,2356
+(defconst isar-keywords-proof101,2538
+(defconst isar-keywords-proof-context108,2743
+(defconst isar-keywords-local-goal112,2857
+(defconst isar-keywords-proper116,2969
+(defconst isar-keywords-improper121,3102
+(defconst isar-keywords-outline126,3248
+(defconst isar-keywords-fume129,3313
+(defconst isar-keywords-indent-open136,3531
+(defconst isar-keywords-indent-close142,3715
+(defconst isar-keywords-indent-enclose146,3820
+(defun isar-regexp-simple-alt 155,4035
+(defun isar-ids-to-regexp 175,4795
+(defconst isar-ext-first 209,6201
+(defconst isar-ext-rest 210,6268
+(defconst isar-long-id-stuff 212,6340
+(defconst isar-id 213,6414
+(defconst isar-idx 214,6484
+(defconst isar-string 216,6543
+(defconst isar-any-command-regexp218,6603
+(defconst isar-name-regexp222,6737
+(defconst isar-improper-regexp228,7032
+(defconst isar-save-command-regexp232,7180
+(defconst isar-global-save-command-regexp235,7281
+(defconst isar-goal-command-regexp238,7395
+(defconst isar-local-goal-command-regexp241,7503
+(defconst isar-comment-start 244,7616
+(defconst isar-comment-end 245,7651
+(defconst isar-comment-start-regexp 246,7684
+(defconst isar-comment-end-regexp 247,7755
+(defconst isar-string-start-regexp 249,7823
+(defconst isar-string-end-regexp 250,7875
+(defconst isar-antiq-regexp 255,7946
+(defconst isar-nesting-regexp261,8099
+(defun isar-nesting 264,8197
+(defun isar-match-nesting 276,8618
+(defface isabelle-class-name-face288,8949
+(defface isabelle-tfree-name-face296,9132
+(defface isabelle-tvar-name-face304,9321
+(defface isabelle-free-name-face312,9509
+(defface isabelle-bound-name-face320,9693
+(defface isabelle-var-name-face328,9880
+(defconst isabelle-class-name-face 336,10067
+(defconst isabelle-tfree-name-face 337,10129
+(defconst isabelle-tvar-name-face 338,10191
+(defconst isabelle-free-name-face 339,10252
+(defconst isabelle-bound-name-face 340,10313
+(defconst isabelle-var-name-face 341,10375
+(defvar isar-font-lock-keywords-1344,10437
+(defun isar-output-flk 361,11488
+(defvar isar-output-font-lock-keywords-1367,11740
+(defvar isar-goals-font-lock-keywords385,12810
+(defconst isar-linear-undo 419,13489
+(defconst isar-undo 421,13532
+(defun isar-remove 423,13575
+(defun isar-undos 426,13650
+(defun isar-cannot-undo 430,13756
+(defconst isar-theory-start-regexp433,13826
+(defconst isar-end-regexp439,13991
+(defconst isar-undo-fail-regexp443,14092
+(defconst isar-undo-skip-regexp447,14196
+(defconst isar-undo-ignore-regexp450,14317
+(defconst isar-undo-remove-regexp453,14382
+(defconst isar-any-entity-regexp461,14557
+(defconst isar-named-entity-regexp466,14744
+(defconst isar-unnamed-entity-regexp471,14921
+(defconst isar-next-entity-regexps474,15023
+(defconst isar-generic-expression482,15334
+(defconst isar-indent-any-regexp493,15651
+(defconst isar-indent-inner-regexp495,15744
+(defconst isar-indent-enclose-regexp497,15810
+(defconst isar-indent-open-regexp499,15926
+(defconst isar-indent-close-regexp501,16036
+(defconst isar-outline-regexp507,16173
+(defconst isar-outline-heading-end-regexp 511,16326
+
+isar/isar-unicode-tokens.el,909
 (defconst isar-control-region-format-regexp20,505
 (defconst isar-control-char-format-regexp 23,599
-(defconst isar-control-region-format-beg 26,695
-(defconst isar-control-region-format-end 27,747
-(defconst isar-control-char-format 28,799
-(defconst isar-control-characters31,847
-(defconst isar-control-regions40,1102
-(defcustom isar-fontsymb-properties 50,1427
-(defconst isar-token-format 66,1938
-(defconst isar-token-variant-format-regexp 70,2090
-(defconst isar-greek-letters-tokens73,2212
-(defconst isar-misc-letters-tokens109,2908
-(defconst isar-symbols-tokens117,3059
-(defun isar-try-char 386,9191
-(defconst isar-symbols-tokens-fallbacks390,9335
-(defconst isar-bold-nums-tokens 414,10166
-(defun isar-map-letters 426,10422
-(defconst isar-script-letters-tokens432,10571
-(defconst isar-roman-letters-tokens437,10709
-(defconst isar-fraktur-letters-tokens442,10845
-(defcustom isar-token-symbol-map447,10989
-(defconst isar-symbol-shortcuts472,11805
-(defcustom isar-shortcut-alist528,13363
+(defconst isar-control-char-format 26,695
+(defconst isar-control-characters28,742
+(defconst isar-control-regions37,997
+(defcustom isar-fontsymb-properties 47,1322
+(defconst isar-token-format 63,1833
+(defconst isar-token-variant-format-regexp 67,1985
+(defconst isar-greek-letters-tokens70,2100
+(defconst isar-misc-letters-tokens106,2796
+(defconst isar-symbols-tokens114,2947
+(defun isar-try-char 383,9079
+(defconst isar-symbols-tokens-fallbacks387,9223
+(defconst isar-bold-nums-tokens 411,10052
+(defun isar-map-letters 423,10308
+(defconst isar-script-letters-tokens429,10457
+(defconst isar-roman-letters-tokens434,10595
+(defconst isar-fraktur-letters-tokens439,10731
+(defcustom isar-token-symbol-map444,10875
+(defconst isar-symbol-shortcuts469,11691
+(defcustom isar-shortcut-alist525,13249
 
 lclam/lclam.el,524
-(defcustom lclam-prog-name 15,389
-(defcustom lclam-web-page21,537
-(defun lclam-config 32,767
-(defun lclam-shell-config 54,1561
-(define-derived-mode lclam-proofscript-mode 74,2220
-(define-derived-mode lclam-shell-mode 79,2343
-(define-derived-mode lclam-response-mode 84,2477
-(define-derived-mode lclam-goals-mode 88,2600
-(defun lclam-mode 96,2828
-(define-derived-mode thy-mode 133,3674
-(defvar thy-mode-map 136,3772
-(defun thy-add-menus 138,3799
-(defun process-thy-file 177,5685
-(defun update-thy-only 183,5886
+(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,497
-(defcustom lego-test-all-name 24,633
-(defpgdefault help-menu-entries30,791
-(defpgdefault menu-entries34,951
-(defvar lego-shell-process-output45,1253
-(defconst lego-process-config53,1576
-(defconst lego-pretty-set-width 64,2007
-(defconst lego-interrupt-regexp 68,2150
-(defcustom lego-www-home-page 73,2267
-(defcustom lego-www-latest-release78,2391
-(defcustom lego-www-refcard84,2569
-(defcustom lego-library-www-page90,2718
-(defvar lego-prog-name 99,2934
-(defvar lego-shell-prompt-pattern 102,3003
-(defvar lego-shell-cd 105,3124
-(defvar lego-shell-abort-goal-regexp 108,3224
-(defvar lego-shell-proof-completed-regexp 113,3416
-(defvar lego-save-command-regexp116,3556
-(defvar lego-goal-command-regexp118,3646
-(defvar lego-kill-goal-command 121,3737
-(defvar lego-forget-id-command 122,3780
-(defvar lego-undoable-commands-regexp124,3826
-(defvar lego-goal-regexp 133,4200
-(defvar lego-outline-regexp135,4245
-(defvar lego-outline-heading-end-regexp 141,4421
-(defvar lego-shell-outline-regexp 143,4474
-(defvar lego-shell-outline-heading-end-regexp 144,4526
-(define-derived-mode lego-shell-mode 150,4805
-(define-derived-mode lego-mode 157,4966
-(define-derived-mode lego-goals-mode 168,5263
-(defun lego-count-undos 179,5689
-(defun lego-goal-command-p 199,6508
-(defun lego-find-and-forget 204,6679
-(defun lego-goal-hyp 246,8515
-(defun lego-state-preserving-p 255,8713
-(defvar lego-shell-current-line-width 271,9416
-(defun lego-shell-adjust-line-width 279,9723
-(defun lego-mode-config 298,10462
-(defun lego-equal-module-filename 366,12523
-(defun lego-shell-compute-new-files-list 372,12798
-(defun lego-shell-mode-config 386,13324
-(defun lego-goals-mode-config 435,15260
+(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
 
 lego/lego-syntax.el,600
-(defconst lego-keywords-goal 15,358
-(defconst lego-keywords-save 17,401
-(defconst lego-commands19,472
-(defconst lego-keywords31,1032
-(defconst lego-tacticals 36,1209
-(defconst lego-error-regexp 39,1317
-(defvar lego-id 42,1476
-(defvar lego-ids 44,1503
-(defconst lego-arg-list-regexp 48,1699
-(defun lego-decl-defn-regexp 51,1815
-(defconst lego-definiendum-alternative-regexp59,2187
-(defvar lego-font-lock-terms63,2371
-(defconst lego-goal-with-hole-regexp89,3227
-(defconst lego-save-with-hole-regexp94,3450
-(defvar lego-font-lock-keywords-199,3667
-(defun lego-init-syntax-table 110,4134
+(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,920
-(defcustom phox-sym-lock-enabled 36,1022
-(defcustom phox-web-page42,1131
-(defcustom phox-doc-dir 48,1281
-(defcustom phox-lib-dir 54,1429
-(defcustom phox-tags-program 60,1573
-(defcustom phox-tags-doc 66,1753
-(defcustom phox-etags 72,1891
-(defpgdefault menu-entries93,2343
-(defun phox-config 107,2536
-(defun phox-shell-config 148,4427
-(define-derived-mode phox-mode 173,5356
-(define-derived-mode phox-shell-mode 189,5822
-(define-derived-mode phox-response-mode 194,5950
-(define-derived-mode phox-goals-mode 207,6392
-(defpgdefault completion-table233,7276
+(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
 
 phox/phox-extraction.el,382
-(defvar phox-prog-orig 11,480
-(defun phox-prog-flags-modify(13,548
-(defun phox-prog-flags-extract(42,1352
-(defun phox-prog-flags-erase(53,1643
-(defun phox-toggle-extraction(61,1839
-(defun phox-compile-theorem(73,2241
-(defun phox-compile-theorem-on-cursor(79,2467
-(defun phox-output 95,2946
-(defun phox-output-theorem 105,3160
-(defun phox-output-theorem-on-cursor(112,3460
+(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
 
 phox/phox-font.el,123
 (defconst phox-font-lock-keywords6,282
@@ -684,51 +683,51 @@ phox/phox-font.el,123
 (defun phox-sym-lock-start 88,2975
 
 phox/phox-fun.el,679
-(defun phox-init-syntax-table 67,2392
-(defvar phox-top-keywords83,2865
-(defvar phox-proof-keywords131,3320
-(defun phox-find-and-forget 172,3670
-(defun phox-assert-next-command-interactive 251,6095
-(defun phox-depend-theorem(270,6926
-(defun phox-eshow-extlist(279,7216
-(defun phox-flag-name(293,7815
-(defun phox-path(304,8118
-(defun phox-print-expression(315,8355
-(defun phox-print-sort-expression(328,8813
-(defun phox-priority-symbols-list(339,9126
-(defun phox-search-string(351,9499
-(defun phox-constraints(366,10027
-(defun phox-goals(377,10284
-(defvar phox-state-menu389,10494
-(defun phox-delete-symbol(414,11484
-(defun phox-delete-symbol-on-cursor(420,11693
+(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,278
-(defun phox-lang-absurd 17,495
-(defun phox-lang-suppress 22,590
-(defun phox-lang-opendef 27,789
-(defun phox-lang-instance 32,908
-(defun phox-lang-lock 37,1037
-(defun phox-lang-unlock 42,1174
-(defun phox-lang-prove 47,1317
-(defun phox-lang-let 52,1454
+(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
 
 phox/phox-outline.el,70
 (defun phox-outline-level(32,1113
 (defun phox-setup-outline 46,1587
 
 phox/phox-pbrpm.el,512
-(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,1929
-(defun phox-pbrpm-get-region-name 84,3183
-(defun  phox-pbrpm-escape-string 87,3310
-(defun phox-pbrpm-generate-menu 91,3445
-(defalias 'proof-pbrpm-generate-menu proof-pbrpm-generate-menu
289,10634
-(defalias 'proof-pbrpm-left-paren-p proof-pbrpm-left-paren-p
290,10698
-(defalias 'proof-pbrpm-right-paren-p proof-pbrpm-right-paren-p
291,10760
+(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
 
 phox/phox-sym-lock.el,1353
 (defvar phox-sym-lock-sym-count 34,1598
@@ -764,14 +763,14 @@ phox/phox-sym-lock.el,1353
 (defun phox-sym-lock-patch-keywords 354,13708
 
 phox/phox-tags.el,305
-(defun phox-tags-add-table(21,770
-(defun phox-tags-reset-table(29,1099
-(defun phox-tags-add-doc-table(34,1209
-(defun phox-tags-add-lib-table(40,1358
-(defun phox-tags-add-local-table(46,1494
-(defun phox-tags-create-local-table(52,1677
-(defun phox-complete-tag(63,1929
-(defvar phox-tags-menu70,2038
+(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,2866
 (defcustom plastic-tags 29,821
@@ -861,1057 +860,1057 @@ plastic/plastic-syntax.el,648
 (defun plastic-init-syntax-table 108,4184
 
 twelf/twelf.el,463
-(defcustom twelf-root-dir25,591
-(defcustom twelf-info-dir31,749
-(defun twelf-add-read-declaration 100,3259
-(defun twelf-set-syntax 113,3594
-(defun twelf-set-word 115,3691
-(defun twelf-set-symbol 116,3753
-(defun twelf-map-string 118,3817
-(defun twelf-mode-extra-config 165,5879
-(defconst twelf-syntax-menu171,6085
-(defpacustom chatter 185,6452
-(defpacustom double-check 190,6545
-(defpacustom print-implicit 194,6682
-(defpgdefault menu-entries206,6826
+(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
 
 twelf/twelf-font.el,917
-(defun twelf-font-create-face 31,836
-(defvar twelf-font-dark-background 38,1094
-(defvar twelf-font-patterns64,2452
-(defun twelf-font-fontify-decl 105,4302
-(defun twelf-font-fontify-buffer 115,4599
-(defun twelf-font-unfontify 122,4858
-(defvar font-lock-message-threshold 127,5032
-(defun twelf-font-fontify-region 129,5110
-(defun twelf-font-highlight 195,7610
-(defun twelf-font-find-delimited-comment 204,8067
-(defun twelf-font-find-decl 223,8747
-(defun twelf-font-find-binder 239,9237
-(defun twelf-font-find-parm 301,11094
-(defun twelf-font-find-evar 308,11417
-(defun twelf-current-decl 330,12159
-(defun twelf-next-decl 357,13315
-(defconst *whitespace* 382,14337
-(defconst *twelf-comment-start* 385,14435
-(defconst *twelf-id-chars* 388,14564
-(defun skip-twelf-comments-and-whitespace 391,14682
-(defun twelf-end-of-par 403,15156
-(defun skip-ahead 426,15930
-(defun current-line-absolute 438,16352
+(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,8771
-(defvar twelf-infix-regexp 215,8831
-(defvar twelf-server-program 219,9026
-(defvar twelf-info-file 222,9107
-(defvar twelf-server-display-commands 225,9180
-(defvar twelf-highlight-range-function 230,9428
-(defvar twelf-focus-function 235,9711
-(defvar twelf-server-echo-commands 241,9991
-(defvar twelf-save-silently 244,10112
-(defvar twelf-server-timeout 248,10284
-(defvar twelf-sml-program 252,10431
-(defvar twelf-sml-args 255,10503
-(defvar twelf-sml-display-queries 258,10569
-(defvar twelf-mode-hook 261,10677
-(defvar twelf-server-mode-hook 264,10771
-(defvar twelf-config-mode-hook 267,10879
-(defvar twelf-sml-mode-hook 270,10993
-(defvar twelf-to-twelf-sml-mode 273,11074
-(defvar twelf-config-mode 276,11166
-(defvar *twelf-server-buffer-name* 283,11430
-(defvar *twelf-server-buffer* 286,11534
-(defvar *twelf-server-process-name* 289,11622
-(defvar *twelf-config-buffer* 292,11713
-(defvar *twelf-config-time* 295,11807
-(defvar *twelf-config-list* 298,11920
-(defvar *twelf-server-last-process-mark* 301,12032
-(defvar *twelf-last-region-sent* 304,12150
-(defvar *twelf-last-input-buffer* 311,12474
-(defvar *twelf-error-pos* 315,12597
-(defconst *twelf-read-functions*318,12673
-(defconst *twelf-parm-table*325,12911
-(defvar twelf-chatter 338,13287
-(defvar twelf-double-check 346,13504
-(defvar twelf-print-implicit 349,13591
-(defconst *twelf-track-parms*352,13683
-(defun install-basic-twelf-keybindings 363,14107
-(defun install-twelf-keybindings 388,15076
-(defvar twelf-mode-map 404,15841
-(defvar twelf-mode-syntax-table 416,16277
-(defun set-twelf-syntax 419,16356
-(defun set-word 421,16453
-(defun set-symbol 422,16508
-(defun map-string 424,16566
-(defconst *whitespace* 456,18043
-(defconst *twelf-comment-start* 459,18141
-(defconst *twelf-id-chars* 462,18270
-(defun skip-twelf-comments-and-whitespace 465,18388
-(defun twelf-end-of-par 477,18862
-(defun twelf-current-decl 500,19636
-(defun twelf-mark-decl 527,20792
-(defun twelf-indent-decl 536,21058
-(defun twelf-indent-region 545,21344
-(defun twelf-indent-lines 556,21668
-(defun twelf-comment-indent 564,21841
-(defun looked-at 575,22197
-(defun twelf-indent-line 580,22369
-(defun twelf-indent-line-to 613,24112
-(defun twelf-calculate-indent 626,24567
-(defun twelf-dsb 641,25191
-(defun twelf-mode-variables 667,26603
-(defun twelf-mode 689,27416
-(defun twelf-info 904,35798
-(defconst twelf-error-regexp918,36338
-(defconst twelf-error-fields-regexp922,36449
-(defconst twelf-error-decl-regexp928,36662
-(defun looked-at-nth 932,36811
-(defun looked-at-nth-int 938,36993
-(defun twelf-error-parser 943,37111
-(defun twelf-error-decl 957,37714
-(defun twelf-mark-relative 963,37893
-(defun twelf-mark-absolute 979,38563
-(defun twelf-find-decl 1004,39449
-(defun twelf-next-error 1019,40005
-(defun twelf-goto-error 1087,42815
-(defun twelf-convert-standard-filename 1101,43353
-(defun string-member 1113,43848
-(defun twelf-config-proceed-p 1125,44340
-(defun twelf-save-if-config 1132,44602
-(defun twelf-config-save-some-buffers 1145,45074
-(defun twelf-save-check-config 1149,45239
-(defun twelf-check-config 1164,45795
-(defun twelf-save-check-file 1176,46235
-(defun twelf-buffer-substring 1192,46958
-(defun twelf-buffer-substring-dot 1198,47220
-(defun twelf-check-declaration 1204,47486
-(defun twelf-highlight-range-zmacs 1227,48546
-(defun twelf-focus 1233,48796
-(defun twelf-focus-noop 1239,49062
-(defun twelf-type-const 1322,52684
-(defvar twelf-server-mode-map 1439,57826
-(defconst twelf-server-cd-regexp 1451,58378
-(defun looked-at-string 1454,58518
-(defun twelf-server-directory-tracker 1458,58659
-(defun twelf-input-filter 1480,59839
-(defun twelf-server-mode 1486,60094
-(defun twelf-parse-config 1519,61311
-(defun twelf-server-read-config 1537,62203
-(defun twelf-server-sync-config 1546,62540
-(defun twelf-get-server-buffer 1576,64046
-(defun twelf-init-variables 1593,64720
-(defun twelf-server 1600,64933
-(defun twelf-server-process 1642,66847
-(defun twelf-server-display 1651,67253
-(defun display-server-buffer 1658,67527
-(defun twelf-server-send-command 1673,68259
-(defun twelf-accept-process-output 1694,69219
-(defun twelf-server-wait 1703,69658
-(defun twelf-server-quit 1745,71796
-(defun twelf-server-interrupt 1750,71917
-(defun twelf-reset 1755,72053
-(defun twelf-config-directory 1760,72197
-(defun twelf-server-configure 1771,72611
-(defun natp 1844,75903
-(defun twelf-read-nat 1848,76004
-(defun twelf-read-bool 1857,76271
-(defun twelf-read-limit 1863,76419
-(defun twelf-read-strategy 1873,76722
-(defun twelf-read-value 1879,76874
-(defun twelf-set 1883,77037
-(defun twelf-set-parm 1896,77514
-(defun track-parm 1905,77811
-(defun twelf-toggle-double-check 1910,77985
-(defun twelf-toggle-print-implicit 1916,78188
-(defun twelf-get 1922,78401
-(defun twelf-timers-reset 1936,79027
-(defun twelf-timers-show 1941,79147
-(defun twelf-timers-check 1947,79298
-(defun twelf-server-restart 1953,79463
-(defun twelf-config-mode 1969,80140
-(defun twelf-config-mode-check 1985,80739
-(defun twelf-tag 1994,81189
-(defun twelf-tag-files 2022,82453
-(default: *tags-errors*)2026,82756
-(defun twelf-tag-file 2047,83507
-(defun twelf-next-decl 2082,84729
-(defun skip-ahead 2107,85751
-(defun current-line-absolute 2119,86173
-(defun new-temp-buffer 2124,86383
-(defun rev-relativize 2135,86767
-(defvar twelf-sml-mode-map 2149,87227
-(defconst twelf-sml-prompt-regexp 2159,87605
-(defun expand-dir 2161,87660
-(defun twelf-sml-cd 2168,87921
-(defconst twelf-sml-cd-regexp 2180,88410
-(defun twelf-sml-directory-tracker 2183,88544
-(defun twelf-sml-mode 2199,89389
-(defun twelf-sml 2250,91323
-(defun switch-to-twelf-sml 2270,92283
-(defun display-twelf-sml-buffer 2281,92632
-(defun twelf-sml-send-string 2297,93348
-(defun twelf-sml-send-region 2302,93552
-(defun twelf-sml-send-query 2326,94758
-(defun twelf-sml-send-newline 2336,95155
-(defun twelf-sml-send-semicolon 2344,95483
-(defun twelf-sml-status 2352,95817
-(defvar twelf-sml-init 2374,96764
-(defun twelf-sml-set-mode 2377,96941
-(defun twelf-sml-quit 2403,98118
-(defun twelf-sml-process-buffer 2408,98230
-(defun twelf-sml-process 2412,98346
-(defvar twelf-to-twelf-sml-mode 2424,98862
-(defun install-twelf-to-twelf-sml-keybindings 2427,98947
-(defvar twelf-to-twelf-sml-mode-map 2437,99332
-(defun twelf-to-twelf-sml-mode 2448,99845
-(defconst twelf-at-point-menu2498,101712
-(defconst twelf-server-state-menu2508,102084
-(defconst twelf-error-menu2518,102401
-(defconst twelf-tags-menu2524,102545
-(defun twelf-toggle-server-display-commands 2534,102830
-(defconst twelf-options-menu2537,102954
-(defconst twelf-timers-menu2572,104692
-(defconst twelf-syntax-menu2585,105186
-(defun twelf-add-menu 2612,106052
-(defun twelf-remove-menu 2616,106154
-(defun twelf-reset-menu 2620,106252
-(defun twelf-server-add-menu 2647,107151
-(defun twelf-server-remove-menu 2651,107274
-(defun twelf-server-reset-menu 2655,107386
+(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
 
 generic/pg-assoc.el,82
-(defun proof-associated-buffers 36,1069
-(defun proof-associated-windows 46,1281
+(defun proof-associated-buffers 36,1066
+(defun proof-associated-windows 46,1278
 
 generic/pg-autotest.el,442
-(defvar pg-autotest-success 24,543
-(defun pg-autotest-find-file 28,627
-(defun pg-autotest-find-file-restart 35,907
-(defmacro pg-autotest 48,1355
-(defun pg-autotest-script-wholefile 62,1702
-(defun pg-autotest-retract-file 79,2315
-(defun pg-autotest-assert-processed 85,2451
-(defun pg-autotest-assert-unprocessed 92,2705
-(defun pg-autotest-message 99,2965
-(defun pg-autotest-quit-prover 106,3158
-(defun pg-autotest-finished 112,3339
+(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
 
 generic/pg-custom.el,554
-(defpgcustom maths-menu-enable 32,1069
-(defpgcustom unicode-tokens-enable 38,1249
-(defpgcustom mmm-enable 44,1426
-(defpgcustom script-indent 53,1780
-(defconst proof-toolbar-entries-default58,1917
-(defpgcustom toolbar-entries 85,3576
-(defpgcustom prog-args 104,4309
-(defpgcustom prog-env 117,4884
-(defpgcustom favourites 126,5310
-(defpgcustom menu-entries 131,5499
-(defpgcustom help-menu-entries 138,5735
-(defpgcustom keymap 145,5998
-(defpgcustom completion-table 150,6170
-(defpgcustom tags-program 161,6544
-(defpgcustom use-holes 170,6928
+(defpgcustom maths-menu-enable 32,1066
+(defpgcustom unicode-tokens-enable 38,1246
+(defpgcustom mmm-enable 44,1423
+(defpgcustom script-indent 53,1777
+(defconst proof-toolbar-entries-default58,1914
+(defpgcustom toolbar-entries 85,3573
+(defpgcustom prog-args 104,4306
+(defpgcustom prog-env 117,4881
+(defpgcustom favourites 126,5307
+(defpgcustom menu-entries 131,5496
+(defpgcustom help-menu-entries 138,5732
+(defpgcustom keymap 145,5995
+(defpgcustom completion-table 150,6167
+(defpgcustom tags-program 161,6541
+(defpgcustom use-holes 170,6925
 
 generic/pg-goals.el,287
-(define-derived-mode proof-goals-mode 30,642
-(define-key proof-goals-mode-map 59,1518
-(define-key proof-goals-mode-map 61,1570
-(define-key proof-goals-mode-map 62,1638
-(define-key proof-goals-mode-map 68,2071
-(defun proof-goals-config-done 76,2188
-(defun pg-goals-display 84,2454
+(define-derived-mode proof-goals-mode 30,639
+(define-key proof-goals-mode-map 59,1515
+(define-key proof-goals-mode-map 61,1567
+(define-key proof-goals-mode-map 62,1635
+(define-key proof-goals-mode-map 68,2068
+(defun proof-goals-config-done 76,2185
+(defun pg-goals-display 84,2451
 
 generic/pg-pbrpm.el,1803
-(defvar pg-pbrpm-use-buffer-menu 22,551
-(defvar pg-pbrpm-start-goal-regexp 25,673
-(defvar pg-pbrpm-start-goal-regexp-par-num 29,830
-(defvar pg-pbrpm-end-goal-regexp 32,953
-(defvar pg-pbrpm-start-hyp-regexp 36,1105
-(defvar pg-pbrpm-start-hyp-regexp-par-num 40,1266
-(defvar pg-pbrpm-start-concl-regexp 44,1473
-(defvar pg-pbrpm-auto-select-regexp 48,1637
-(defvar pg-pbrpm-buffer-menu 55,1798
-(defvar pg-pbrpm-spans 56,1832
-(defvar pg-pbrpm-goal-description 57,1860
-(defvar pg-pbrpm-windows-dialog-bug 58,1899
-(defvar pbrpm-menu-desc 59,1940
-(defun pg-pbrpm-erase-buffer-menu 61,1970
-(defun pg-pbrpm-menu-change-hook 68,2154
-(defun pg-pbrpm-create-reset-buffer-menu 86,2730
-(defun pg-pbrpm-analyse-goal-buffer 101,3359
-(defun pg-pbrpm-button-action 161,5769
-(defun pg-pbrpm-exists 168,5995
-(defun pg-pbrpm-eliminate-id 172,6107
-(defun pg-pbrpm-build-menu 180,6353
-(defun pg-pbrpm-setup-span 243,8679
-(defun pg-pbrpm-run-command 303,10997
-(defun pg-pbrpm-get-pos-info 332,12307
-(defun pg-pbrpm-get-region-info 374,13614
-(defun pg-pbrpm-auto-select-around-point 385,14028
-(defun pg-pbrpm-translate-position 400,14558
-(defun pg-pbrpm-process-click 408,14816
-(defvar pg-pbrpm-remember-region-selected-region 428,15841
-(defvar pg-pbrpm-regions-list 429,15895
-(defun pg-pbrpm-erase-regions-list 431,15931
-(defun pg-pbrpm-filter-regions-list 440,16239
-(defface pg-pbrpm-multiple-selection-face447,16502
-(defface pg-pbrpm-menu-input-face455,16704
-(defun pg-pbrpm-do-remember-region 463,16894
-(defun pg-pbrpm-remember-region-drag-up-hook 484,17742
-(defun pg-pbrpm-remember-region-click-hook 488,17913
-(defun pg-pbrpm-remember-region 493,18098
-(defun pg-pbrpm-process-region 507,18813
-(defun pg-pbrpm-process-regions-list 525,19542
-(defun pg-pbrpm-region-expression 529,19725
+(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,919
-(defalias 'pg-pgip-error pg-pgip-error
36,960
-(defalias 'pg-pgip-warning pg-pgip-warning
37,995
-(defconst pg-pgip-version-supported 39,1045
-(defun pg-pgip-process-packet 43,1151
-(defvar pg-pgip-last-seen-id 53,1723
-(defvar pg-pgip-last-seen-seq 54,1757
-(defun pg-pgip-process-pgip 56,1793
-(defun pg-pgip-process-msg 75,2724
-(defvar pg-pgip-post-process-functions89,3294
-(defun pg-pgip-post-process 99,3782
-(defun pg-pgip-process-askpgip 115,4393
-(defun pg-pgip-process-usespgip 121,4598
-(defun pg-pgip-process-usespgml 125,4762
-(defun pg-pgip-process-pgmlconfig 129,4926
-(defun pg-pgip-process-proverinfo 145,5543
-(defun pg-pgip-process-hasprefs 162,6208
-(defun pg-pgip-haspref 176,6840
-(defun pg-pgip-process-prefval 195,7616
-(defun pg-pgip-process-guiconfig 222,8325
-(defvar proof-assistant-idtables 229,8442
-(defun pg-pgip-process-ids 232,8559
-(defun pg-complete-idtable-symbol 258,9635
-(defalias 'pg-pgip-process-setids pg-pgip-process-setids
263,9727
-(defalias 'pg-pgip-process-addids pg-pgip-process-addids
264,9783
-(defalias 'pg-pgip-process-delids pg-pgip-process-delids
265,9839
-(defun pg-pgip-process-idvalue 268,9897
-(defun pg-pgip-process-menuadd 280,10233
-(defun pg-pgip-process-menudel 283,10276
-(defun pg-pgip-process-ready 292,10509
-(defun pg-pgip-process-cleardisplay 295,10550
-(defun pg-pgip-process-proofstate 309,11007
-(defun pg-pgip-process-normalresponse 313,11084
-(defun pg-pgip-process-errorresponse 317,11208
-(defun pg-pgip-process-scriptinsert 321,11331
-(defun pg-pgip-process-metainforesponse 326,11465
-(defun pg-pgip-process-informfileloaded 335,11706
-(defun pg-pgip-process-informfileretracted 341,11972
-(defun pg-pgip-process-brokerstatus 354,12449
-(defun pg-pgip-process-proveravailmsg 357,12497
-(defun pg-pgip-process-newprovermsg 360,12547
-(defun pg-pgip-process-proverstatusmsg 363,12595
-(defvar pg-pgip-srcids 372,12842
-(defun pg-pgip-process-newfile 376,12949
-(defun pg-pgip-process-filestatus 392,13537
-(defun pg-pgip-process-newobj 412,14192
-(defun pg-pgip-process-delobj 415,14234
-(defun pg-pgip-process-objectstatus 418,14276
-(defun pg-pgip-process-parsescript 432,14631
-(defun pg-pgip-get-pgiptype 455,15506
-(defun pg-pgip-default-for 475,16299
-(defun pg-pgip-subst-for 488,16694
-(defun pg-pgip-interpret-value 500,17037
-(defun pg-pgip-interpret-choice 518,17722
-(defun pg-pgip-string-of-command 549,18739
-(defconst pg-pgip-id566,19500
-(defvar pg-pgip-refseq 572,19780
-(defvar pg-pgip-refid 574,19877
-(defvar pg-pgip-seq 577,19969
-(defun pg-pgip-assemble-packet 579,20033
-(defun pg-pgip-issue 597,20845
-(defun pg-pgip-maybe-askpgip 614,21457
-(defun pg-pgip-askprefs 620,21648
-(defun pg-pgip-askids 624,21762
-(defun pg-pgip-reset 637,22050
-(defconst pg-pgip-start-element-regexp 668,22748
-(defconst pg-pgip-end-element-regexp 669,22800
+(defalias 'pg-pgip-debug pg-pgip-debug
35,920
+(defalias 'pg-pgip-error pg-pgip-error
36,961
+(defalias 'pg-pgip-warning pg-pgip-warning
37,996
+(defconst pg-pgip-version-supported 39,1046
+(defun pg-pgip-process-packet 43,1152
+(defvar pg-pgip-last-seen-id 53,1724
+(defvar pg-pgip-last-seen-seq 54,1758
+(defun pg-pgip-process-pgip 56,1794
+(defun pg-pgip-process-msg 75,2725
+(defvar pg-pgip-post-process-functions89,3295
+(defun pg-pgip-post-process 99,3783
+(defun pg-pgip-process-askpgip 115,4394
+(defun pg-pgip-process-usespgip 121,4599
+(defun pg-pgip-process-usespgml 125,4763
+(defun pg-pgip-process-pgmlconfig 129,4927
+(defun pg-pgip-process-proverinfo 145,5544
+(defun pg-pgip-process-hasprefs 162,6209
+(defun pg-pgip-haspref 176,6841
+(defun pg-pgip-process-prefval 195,7617
+(defun pg-pgip-process-guiconfig 222,8326
+(defvar proof-assistant-idtables 229,8443
+(defun pg-pgip-process-ids 232,8560
+(defun pg-complete-idtable-symbol 258,9636
+(defalias 'pg-pgip-process-setids pg-pgip-process-setids
263,9728
+(defalias 'pg-pgip-process-addids pg-pgip-process-addids
264,9784
+(defalias 'pg-pgip-process-delids pg-pgip-process-delids
265,9840
+(defun pg-pgip-process-idvalue 268,9898
+(defun pg-pgip-process-menuadd 280,10234
+(defun pg-pgip-process-menudel 283,10277
+(defun pg-pgip-process-ready 292,10510
+(defun pg-pgip-process-cleardisplay 295,10551
+(defun pg-pgip-process-proofstate 309,11008
+(defun pg-pgip-process-normalresponse 313,11085
+(defun pg-pgip-process-errorresponse 317,11209
+(defun pg-pgip-process-scriptinsert 321,11332
+(defun pg-pgip-process-metainforesponse 326,11466
+(defun pg-pgip-process-informfileloaded 335,11707
+(defun pg-pgip-process-informfileretracted 341,11973
+(defun pg-pgip-process-brokerstatus 354,12450
+(defun pg-pgip-process-proveravailmsg 357,12498
+(defun pg-pgip-process-newprovermsg 360,12548
+(defun pg-pgip-process-proverstatusmsg 363,12596
+(defvar pg-pgip-srcids 372,12843
+(defun pg-pgip-process-newfile 376,12950
+(defun pg-pgip-process-filestatus 392,13538
+(defun pg-pgip-process-newobj 412,14193
+(defun pg-pgip-process-delobj 415,14235
+(defun pg-pgip-process-objectstatus 418,14277
+(defun pg-pgip-process-parsescript 432,14632
+(defun pg-pgip-get-pgiptype 455,15507
+(defun pg-pgip-default-for 475,16300
+(defun pg-pgip-subst-for 488,16695
+(defun pg-pgip-interpret-value 500,17038
+(defun pg-pgip-interpret-choice 518,17723
+(defun pg-pgip-string-of-command 549,18740
+(defconst pg-pgip-id566,19501
+(defvar pg-pgip-refseq 572,19781
+(defvar pg-pgip-refid 574,19878
+(defvar pg-pgip-seq 577,19970
+(defun pg-pgip-assemble-packet 579,20034
+(defun pg-pgip-issue 597,20846
+(defun pg-pgip-maybe-askpgip 614,21458
+(defun pg-pgip-askprefs 620,21649
+(defun pg-pgip-askids 624,21763
+(defun pg-pgip-reset 637,22051
+(defconst pg-pgip-start-element-regexp 668,22749
+(defconst pg-pgip-end-element-regexp 669,22801
 
 generic/pg-response.el,1078
-(deflocal pg-response-eagerly-raise 31,734
-(define-derived-mode proof-response-mode 41,959
-(defun proof-response-config-done 65,1969
-(defvar pg-response-special-display-regexp 76,2316
-(defconst proof-multiframe-parameters80,2483
-(defun proof-multiple-frames-enable 89,2782
-(defun proof-three-window-enable 99,3111
-(defun proof-select-three-b 102,3174
-(defun proof-display-three-b 117,3643
-(defvar pg-frame-configuration 129,4052
-(defun pg-cache-frame-configuration 133,4199
-(defun proof-layout-windows 137,4370
-(defun proof-delete-other-frames 177,6135
-(defvar pg-response-erase-flag 208,7225
-(defun pg-response-maybe-erase212,7354
-(defun pg-response-display 243,8539
-(defun pg-response-display-with-face 273,9627
-(defun pg-response-clear-displays 299,10421
-(defun proof-next-error 318,11008
-(defun pg-response-has-error-location 399,13924
-(defvar proof-trace-last-fontify-pos 422,14757
-(defun proof-trace-fontify-pos 424,14800
-(defun proof-trace-buffer-display 432,15113
-(defun proof-trace-buffer-finish 457,16059
-(defun pg-thms-buffer-clear 479,16630
+(deflocal pg-response-eagerly-raise 31,731
+(define-derived-mode proof-response-mode 41,956
+(defun proof-response-config-done 65,1966
+(defvar pg-response-special-display-regexp 76,2313
+(defconst proof-multiframe-parameters80,2480
+(defun proof-multiple-frames-enable 89,2779
+(defun proof-three-window-enable 99,3108
+(defun proof-select-three-b 102,3171
+(defun proof-display-three-b 117,3640
+(defvar pg-frame-configuration 129,4049
+(defun pg-cache-frame-configuration 133,4196
+(defun proof-layout-windows 137,4367
+(defun proof-delete-other-frames 177,6132
+(defvar pg-response-erase-flag 208,7222
+(defun pg-response-maybe-erase212,7351
+(defun pg-response-display 243,8536
+(defun pg-response-display-with-face 275,9661
+(defun pg-response-clear-displays 301,10455
+(defun proof-next-error 320,11042
+(defun pg-response-has-error-location 401,13958
+(defvar proof-trace-last-fontify-pos 424,14791
+(defun proof-trace-fontify-pos 426,14834
+(defun proof-trace-buffer-display 434,15147
+(defun proof-trace-buffer-finish 459,16093
+(defun pg-thms-buffer-clear 481,16664
 
 generic/pg-thymodes.el,152
-(defmacro pg-defthymode 23,503
-(defmacro pg-do-unless-null 71,2314
-(defun pg-symval 76,2401
-(defun pg-modesym 82,2556
-(defun pg-modesymval 86,2670
+(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,3075
-(defmacro proof-maybe-save-point 31,810
-(defun proof-maybe-follow-locked-end 41,1107
-(defun proof-assert-next-command-interactive 55,1472
-(defun proof-process-buffer 65,1843
-(defun proof-undo-last-successful-command 79,2160
-(defun proof-undo-and-delete-last-successful-command 84,2322
-(defun proof-undo-last-successful-command-1 98,2885
-(defun proof-retract-buffer 114,3450
-(defun proof-retract-current-goal 123,3730
-(defun proof-interrupt-process 142,4236
-(defun proof-goto-command-start 169,5225
-(defun proof-goto-command-end 192,6165
-(defun proof-mouse-goto-point 213,6800
-(defvar proof-minibuffer-history 229,7043
-(defun proof-minibuffer-cmd 232,7138
-(defun proof-frob-locked-end 276,8753
-(defmacro proof-if-setting-configured 337,10681
-(defmacro proof-define-assistant-command 345,10950
-(defmacro proof-define-assistant-command-witharg 358,11405
-(defun proof-issue-new-command 378,12228
-(defun proof-cd-sync 422,13671
-(defun proof-electric-terminator-enable 481,15436
-(defun proof-electric-term-incomment-fn 489,15738
-(defun proof-process-electric-terminator 509,16491
-(defun proof-electric-terminator 536,17639
-(defun proof-add-completions 558,18285
-(defun proof-script-complete 578,19039
-(defun pg-insert-last-output-as-comment 606,19630
-(defun pg-copy-span-contents 625,20236
-(defun pg-numth-span-higher-or-lower 642,20794
-(defun pg-control-span-of 668,21540
-(defun pg-move-span-contents 674,21744
-(defun pg-fixup-children-spans 726,23924
-(defun pg-move-region-down 736,24187
-(defun pg-move-region-up 745,24480
-(defun proof-forward-command 775,25318
-(defun proof-backward-command 796,26039
-(defun pg-pos-for-event 818,26390
-(defun pg-span-for-event 824,26611
-(defun pg-span-context-menu 828,26755
-(defun pg-toggle-visibility 843,27210
-(defun pg-create-in-span-context-menu 853,27532
-(defun pg-span-undo 886,28876
-(defun pg-goals-buffers-hint 932,30286
-(defun pg-slow-fontify-tracing-hint 936,30468
-(defun pg-response-buffers-hint 940,30639
-(defun pg-jump-to-end-hint 950,31001
-(defun pg-processing-complete-hint 954,31132
-(defun pg-next-error-hint 971,31831
-(defun pg-hint 976,31983
-(defun pg-identifier-under-mouse-query 991,32517
-(defun proof-imenu-enable 1032,34001
-(defvar pg-input-ring 1063,35047
-(defvar pg-input-ring-index 1066,35104
-(defvar pg-stored-incomplete-input 1069,35176
-(defun pg-previous-input 1072,35279
-(defun pg-next-input 1086,35736
-(defun pg-delete-input 1091,35858
-(defun pg-get-old-input 1104,36196
-(defun pg-restore-input 1118,36587
-(defun pg-search-start 1129,36877
-(defun pg-regexp-arg 1141,37369
-(defun pg-search-arg 1153,37817
-(defun pg-previous-matching-input-string-position 1167,38234
-(defun pg-previous-matching-input 1194,39399
-(defun pg-next-matching-input 1213,40249
-(defvar pg-matching-input-from-input-string 1221,40632
-(defun pg-previous-matching-input-from-input 1225,40746
-(defun pg-next-matching-input-from-input 1243,41511
-(defun pg-add-to-input-history 1254,41890
-(defun pg-remove-from-input-history 1266,42343
-(defun  pg-clear-input-ring 1277,42725
+(defmacro proof-maybe-save-point 31,807
+(defun proof-maybe-follow-locked-end 41,1104
+(defun proof-assert-next-command-interactive 55,1469
+(defun proof-process-buffer 65,1840
+(defun proof-undo-last-successful-command 79,2157
+(defun proof-undo-and-delete-last-successful-command 84,2319
+(defun proof-undo-last-successful-command-1 98,2882
+(defun proof-retract-buffer 114,3447
+(defun proof-retract-current-goal 123,3727
+(defun proof-interrupt-process 142,4233
+(defun proof-goto-command-start 169,5222
+(defun proof-goto-command-end 192,6162
+(defun proof-mouse-goto-point 213,6797
+(defvar proof-minibuffer-history 229,7040
+(defun proof-minibuffer-cmd 232,7135
+(defun proof-frob-locked-end 276,8750
+(defmacro proof-if-setting-configured 337,10678
+(defmacro proof-define-assistant-command 345,10947
+(defmacro proof-define-assistant-command-witharg 358,11402
+(defun proof-issue-new-command 378,12225
+(defun proof-cd-sync 422,13668
+(defun proof-electric-terminator-enable 481,15433
+(defun proof-electric-term-incomment-fn 489,15735
+(defun proof-process-electric-terminator 509,16488
+(defun proof-electric-terminator 536,17636
+(defun proof-add-completions 558,18282
+(defun proof-script-complete 578,19036
+(defun pg-insert-last-output-as-comment 606,19627
+(defun pg-copy-span-contents 625,20233
+(defun pg-numth-span-higher-or-lower 642,20791
+(defun pg-control-span-of 668,21537
+(defun pg-move-span-contents 674,21741
+(defun pg-fixup-children-spans 726,23921
+(defun pg-move-region-down 736,24184
+(defun pg-move-region-up 745,24477
+(defun proof-forward-command 775,25315
+(defun proof-backward-command 796,26036
+(defun pg-pos-for-event 818,26387
+(defun pg-span-for-event 824,26608
+(defun pg-span-context-menu 828,26752
+(defun pg-toggle-visibility 843,27207
+(defun pg-create-in-span-context-menu 853,27529
+(defun pg-span-undo 886,28873
+(defun pg-goals-buffers-hint 932,30283
+(defun pg-slow-fontify-tracing-hint 936,30465
+(defun pg-response-buffers-hint 940,30636
+(defun pg-jump-to-end-hint 950,30998
+(defun pg-processing-complete-hint 954,31129
+(defun pg-next-error-hint 971,31828
+(defun pg-hint 976,31980
+(defun pg-identifier-under-mouse-query 991,32514
+(defun proof-imenu-enable 1032,33998
+(defvar pg-input-ring 1063,35044
+(defvar pg-input-ring-index 1066,35101
+(defvar pg-stored-incomplete-input 1069,35173
+(defun pg-previous-input 1072,35276
+(defun pg-next-input 1086,35733
+(defun pg-delete-input 1091,35855
+(defun pg-get-old-input 1104,36193
+(defun pg-restore-input 1118,36584
+(defun pg-search-start 1129,36874
+(defun pg-regexp-arg 1141,37366
+(defun pg-search-arg 1153,37814
+(defun pg-previous-matching-input-string-position 1167,38231
+(defun pg-previous-matching-input 1194,39396
+(defun pg-next-matching-input 1213,40246
+(defvar pg-matching-input-from-input-string 1221,40629
+(defun pg-previous-matching-input-from-input 1225,40743
+(defun pg-next-matching-input-from-input 1243,41508
+(defun pg-add-to-input-history 1254,41887
+(defun pg-remove-from-input-history 1266,42340
+(defun  pg-clear-input-ring 1277,42722
 
 generic/pg-vars.el,1106
-(defvar proof-assistant-cusgrp 20,379
-(defvar proof-assistant-internals-cusgrp 26,641
-(defvar proof-assistant 32,912
-(defvar proof-assistant-symbol 37,1134
-(defvar proof-mode-for-shell 50,1678
-(defvar proof-mode-for-response 55,1870
-(defvar proof-mode-for-goals 60,2097
-(defvar proof-mode-for-script 65,2287
-(defvar proof-ready-for-assistant-hook 70,2465
-(defvar proof-shell-busy 80,2752
-(defvar proof-included-files-list 85,2908
-(defvar proof-script-buffer 107,3921
-(defvar proof-previous-script-buffer 110,4013
-(defvar proof-shell-buffer 114,4184
-(defvar proof-goals-buffer 117,4270
-(defvar proof-response-buffer 120,4325
-(defvar proof-trace-buffer 123,4386
-(defvar proof-thms-buffer 127,4540
-(defvar proof-shell-error-or-interrupt-seen 131,4695
-(defvar pg-response-next-error 136,4919
-(defvar proof-shell-proof-completed 139,5026
-(defvar proof-terminal-string 151,5570
-(defvar proof-shell-last-output 161,5760
-(defvar proof-assistant-settings 165,5901
-(defvar pg-tracing-slow-mode 172,6264
-(defvar proof-nesting-depth 175,6353
-(defvar proof-last-theorem-dependencies 182,6588
+(defvar proof-assistant-cusgrp 20,380
+(defvar proof-assistant-internals-cusgrp 26,642
+(defvar proof-assistant 32,913
+(defvar proof-assistant-symbol 37,1135
+(defvar proof-mode-for-shell 50,1679
+(defvar proof-mode-for-response 55,1871
+(defvar proof-mode-for-goals 60,2098
+(defvar proof-mode-for-script 65,2288
+(defvar proof-ready-for-assistant-hook 70,2466
+(defvar proof-shell-busy 80,2753
+(defvar proof-included-files-list 85,2909
+(defvar proof-script-buffer 107,3922
+(defvar proof-previous-script-buffer 110,4014
+(defvar proof-shell-buffer 114,4185
+(defvar proof-goals-buffer 117,4271
+(defvar proof-response-buffer 120,4326
+(defvar proof-trace-buffer 123,4387
+(defvar proof-thms-buffer 127,4541
+(defvar proof-shell-error-or-interrupt-seen 131,4696
+(defvar pg-response-next-error 136,4920
+(defvar proof-shell-proof-completed 139,5027
+(defvar proof-terminal-string 151,5571
+(defvar proof-shell-last-output 161,5761
+(defvar proof-assistant-settings 165,5902
+(defvar pg-tracing-slow-mode 172,6265
+(defvar proof-nesting-depth 175,6354
+(defvar proof-last-theorem-dependencies 182,6589
 
 generic/pg-xml.el,1140
-(defalias 'pg-xml-error pg-xml-error
16,369
-(defun pg-xml-parse-string 39,1011
-(defun pg-xml-parse-buffer 50,1337
-(defun pg-xml-get-attr 72,2070
-(defun pg-xml-child-elts 80,2372
-(defun pg-xml-child-elt 85,2577
-(defun pg-xml-get-child 93,2859
-(defun pg-xml-get-text-content 103,3231
-(defmacro pg-xml-attr 114,3581
-(defmacro pg-xml-node 116,3643
-(defconst pg-xml-header119,3735
-(defun pg-xml-string-of 123,3811
-(defun pg-xml-output-internal 134,4178
-(defun pg-xml-cdata 168,5328
-(defun pg-pgip-get-icon 176,5521
-(defsubst pg-pgip-get-name 180,5669
-(defsubst pg-pgip-get-version 183,5786
-(defsubst pg-pgip-get-descr 186,5909
-(defsubst pg-pgip-get-thmname 189,6028
-(defsubst pg-pgip-get-thyname 192,6151
-(defsubst pg-pgip-get-url 195,6274
-(defsubst pg-pgip-get-srcid 198,6389
-(defsubst pg-pgip-get-proverid 201,6508
-(defsubst pg-pgip-get-symname 204,6633
-(defsubst pg-pgip-get-prefcat 207,6753
-(defsubst pg-pgip-get-default 210,6881
-(defsubst pg-pgip-get-objtype 213,7004
-(defsubst pg-pgip-get-value 216,7127
-(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext
219,7197
-(defun pg-pgip-get-pgmltext 221,7256
+(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
 
 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 63,1729
-
-generic/proof-config.el,10808
-(defgroup proof-user-options 88,3074
-(defun proof-set-value 96,3253
-(defcustom proof-electric-terminator-enable 129,4376
-(defcustom proof-toolbar-enable 141,4908
-(defcustom proof-imenu-enable 147,5081
-(defcustom pg-show-hints 153,5252
-(defcustom proof-trace-output-slow-catchup 159,5447
-(defcustom proof-strict-state-preserving 169,5944
-(defcustom proof-strict-read-only 182,6553
-(defcustom proof-allow-undo-in-read-only 191,6946
-(defcustom proof-three-window-enable 199,7279
-(defcustom proof-multiple-frames-enable 218,8029
-(defcustom proof-delete-empty-windows 227,8362
-(defcustom proof-shrink-windows-tofit 238,8893
-(defcustom proof-query-file-save-when-activating-scripting245,9165
-(defcustom proof-one-command-per-line261,9885
-(defcustom proof-prog-name-ask268,10112
-(defcustom proof-prog-name-guess274,10272
-(defcustom proof-tidy-response282,10537
-(defcustom proof-keep-response-history296,11000
-(defcustom pg-input-ring-size 306,11388
-(defcustom proof-general-debug 311,11540
-(defcustom proof-experimental-features 321,11912
-(defcustom proof-follow-mode 335,12447
-(defcustom proof-auto-action-when-deactivating-scripting 359,13624
-(defcustom proof-script-command-separator 382,14573
-(defcustom proof-rsh-command 390,14865
-(defcustom proof-disappearing-proofs 406,15415
-(defgroup proof-faces 433,16061
-(defconst pg-defface-window-systems440,16243
-(defmacro proof-face-specs 453,16796
-(defface proof-queue-face468,17248
-(defface proof-locked-face476,17526
-(defface proof-declaration-name-face489,18029
-(defface proof-tacticals-name-face498,18315
-(defface proof-tactics-name-face507,18577
-(defface proof-error-face516,18842
-(defface proof-warning-face524,19032
-(defface proof-eager-annotation-face533,19289
-(defface proof-debug-message-face541,19507
-(defface proof-boring-face549,19706
-(defface proof-mouse-highlight-face557,19898
-(defface proof-highlight-dependent-face565,20094
-(defface proof-highlight-dependency-face573,20303
-(defface proof-active-area-face581,20500
-(defconst proof-face-compat-doc 590,20890
-(defconst proof-queue-face 591,20970
-(defconst proof-locked-face 592,21038
-(defconst proof-declaration-name-face 593,21108
-(defconst proof-tacticals-name-face 594,21198
-(defconst proof-tactics-name-face 595,21284
-(defconst proof-error-face 596,21366
-(defconst proof-warning-face 597,21434
-(defconst proof-eager-annotation-face 598,21506
-(defconst proof-debug-message-face 599,21596
-(defconst proof-boring-face 600,21680
-(defconst proof-mouse-highlight-face 601,21750
-(defconst proof-highlight-dependent-face 602,21838
-(defconst proof-highlight-dependency-face 603,21934
-(defconst proof-active-area-face 604,22032
-(defgroup prover-config 617,22176
-(defcustom proof-guess-command-line 659,23505
-(defcustom proof-assistant-home-page 674,24000
-(defcustom proof-context-command 680,24170
-(defcustom proof-info-command 685,24304
-(defcustom proof-showproof-command 692,24575
-(defcustom proof-goal-command 697,24711
-(defcustom proof-save-command 705,25008
-(defcustom proof-find-theorems-command 713,25317
-(defcustom proof-assistant-true-value 720,25627
-(defcustom proof-assistant-false-value 726,25817
-(defcustom proof-assistant-format-int-fn 732,26011
-(defcustom proof-assistant-format-string-fn 739,26260
-(defcustom proof-assistant-setting-format 746,26527
-(defgroup proof-script 768,27222
-(defcustom proof-terminal-char 773,27352
-(defcustom proof-script-sexp-commands 783,27739
-(defcustom proof-script-command-end-regexp 794,28196
-(defcustom proof-script-command-start-regexp 812,29015
-(defcustom proof-script-use-old-parser 823,29476
-(defcustom proof-script-integral-proofs 835,29962
-(defcustom proof-script-fly-past-comments 850,30618
-(defcustom proof-script-parse-function 855,30789
-(defcustom proof-script-comment-start 873,31432
-(defcustom proof-script-comment-start-regexp 884,31869
-(defcustom proof-script-comment-end 892,32188
-(defcustom proof-script-comment-end-regexp 904,32610
-(defcustom pg-insert-output-as-comment-fn 912,32921
-(defcustom proof-string-start-regexp 918,33173
-(defcustom proof-string-end-regexp 923,33338
-(defcustom proof-case-fold-search 928,33499
-(defcustom proof-save-command-regexp 937,33911
-(defcustom proof-save-with-hole-regexp 942,34021
-(defcustom proof-save-with-hole-result 954,34475
-(defcustom proof-goal-command-regexp 964,34923
-(defcustom proof-goal-with-hole-regexp 973,35311
-(defcustom proof-goal-with-hole-result 985,35754
-(defcustom proof-non-undoables-regexp 994,36138
-(defcustom proof-nested-undo-regexp 1005,36593
-(defcustom proof-ignore-for-undo-count 1021,37305
-(defcustom proof-script-next-entity-regexps 1029,37608
-(defcustom proof-script-find-next-entity-fn1073,39349
-(defcustom proof-script-imenu-generic-expression 1093,40189
-(defcustom proof-goal-command-p 1101,40528
-(defcustom proof-really-save-command-p 1112,41019
-(defcustom proof-completed-proof-behaviour 1121,41326
-(defcustom proof-count-undos-fn 1149,42682
-(defconst proof-no-command 1161,43231
-(defcustom proof-find-and-forget-fn 1166,43438
-(defcustom proof-forget-id-command 1183,44152
-(defcustom pg-topterm-goalhyplit-fn 1193,44510
-(defcustom proof-kill-goal-command 1205,45045
-(defcustom proof-undo-n-times-cmd 1219,45548
-(defcustom proof-nested-goals-history-p 1233,46096
-(defcustom proof-state-preserving-p 1242,46433
-(defcustom proof-activate-scripting-hook 1252,46905
-(defcustom proof-deactivate-scripting-hook 1271,47686
-(defcustom proof-indent 1284,48051
-(defcustom proof-indent-hang 1289,48158
-(defcustom proof-indent-enclose-offset 1294,48284
-(defcustom proof-indent-open-offset 1299,48426
-(defcustom proof-indent-close-offset 1304,48563
-(defcustom proof-indent-any-regexp 1309,48701
-(defcustom proof-indent-inner-regexp 1314,48861
-(defcustom proof-indent-enclose-regexp 1319,49015
-(defcustom proof-indent-open-regexp 1324,49169
-(defcustom proof-indent-close-regexp 1329,49321
-(defcustom proof-script-font-lock-keywords 1335,49475
-(defcustom proof-script-syntax-table-entries 1343,49792
-(defcustom proof-script-span-context-menu-extensions 1361,50189
-(defgroup proof-shell 1387,50949
-(defcustom proof-prog-name 1397,51120
-(defcustom proof-shell-auto-terminate-commands 1408,51540
-(defcustom proof-shell-pre-sync-init-cmd 1417,51941
-(defcustom proof-shell-init-cmd 1431,52499
-(defcustom proof-shell-init-hook 1443,53028
-(defcustom proof-shell-restart-cmd 1448,53167
-(defcustom proof-shell-quit-cmd 1453,53322
-(defcustom proof-shell-quit-timeout 1458,53489
-(defcustom proof-shell-cd-cmd 1468,53939
-(defcustom proof-shell-start-silent-cmd 1485,54610
-(defcustom proof-shell-stop-silent-cmd 1494,54986
-(defcustom proof-shell-silent-threshold 1503,55321
-(defcustom  proof-shell-inform-file-processed-cmd 1511,55655
-(defcustom  proof-shell-inform-file-retracted-cmd 1532,56583
-(defcustom proof-auto-multiple-files 1560,57855
-(defcustom proof-cannot-reopen-processed-files 1575,58576
-(defcustom proof-shell-require-command-regexp 1589,59242
-(defcustom proof-done-advancing-require-function 1600,59704
-(defcustom proof-shell-quiet-errors 1606,59939
-(defcustom proof-shell-prompt-pattern 1619,60273
-(defcustom proof-shell-wakeup-char 1629,60694
-(defcustom proof-shell-annotated-prompt-regexp 1635,60925
-(defcustom proof-shell-abort-goal-regexp 1651,61561
-(defcustom proof-shell-error-regexp 1656,61696
-(defcustom proof-shell-truncate-before-error 1676,62496
-(defcustom pg-next-error-regexp 1690,63035
-(defcustom pg-next-error-filename-regexp 1705,63644
-(defcustom pg-next-error-extract-filename 1729,64677
-(defcustom proof-shell-interrupt-regexp 1736,64920
-(defcustom proof-shell-proof-completed-regexp 1750,65515
-(defcustom proof-shell-clear-response-regexp 1763,66023
-(defcustom proof-shell-clear-goals-regexp 1770,66322
-(defcustom proof-shell-start-goals-regexp 1777,66615
-(defcustom proof-shell-end-goals-regexp 1785,66982
-(defcustom proof-shell-eager-annotation-start 1791,67226
-(defcustom proof-shell-eager-annotation-start-length 1814,68245
-(defcustom proof-shell-eager-annotation-end 1825,68671
-(defcustom proof-shell-assumption-regexp 1841,69346
-(defcustom proof-shell-process-file 1851,69749
-(defcustom proof-shell-retract-files-regexp 1873,70705
-(defcustom proof-shell-compute-new-files-list 1882,71041
-(defcustom pg-use-specials-for-fontify 1894,71589
-(defcustom pg-special-char-regexp 1902,71937
-(defcustom proof-shell-set-elisp-variable-regexp 1908,72082
-(defcustom proof-shell-match-pgip-cmd 1941,73595
-(defcustom proof-shell-issue-pgip-cmd 1950,73924
-(defcustom proof-shell-query-dependencies-cmd 1959,74280
-(defcustom proof-shell-theorem-dependency-list-regexp 1966,74540
-(defcustom proof-shell-theorem-dependency-list-split 1982,75200
-(defcustom proof-shell-show-dependency-cmd 1991,75623
-(defcustom proof-shell-identifier-under-mouse-cmd 1998,75892
-(defcustom proof-shell-trace-output-regexp 2021,76973
-(defcustom proof-shell-thms-output-regexp 2035,77431
-(defcustom proof-tokens-activate-command 2048,77814
-(defcustom proof-tokens-deactivate-command 2055,78055
-(defcustom proof-tokens-extra-modes 2062,78302
-(defcustom proof-shell-unicode 2077,78809
-(defcustom proof-shell-filename-escapes 2085,79129
-(defcustom proof-shell-process-connection-type2102,79809
-(defcustom proof-shell-strip-crs-from-input 2125,80855
-(defcustom proof-shell-strip-crs-from-output 2137,81340
-(defcustom proof-shell-insert-hook 2145,81708
-(defcustom proof-shell-handle-delayed-output-hook2183,83568
-(defcustom proof-shell-handle-error-or-interrupt-hook2189,83783
-(defcustom proof-shell-pre-interrupt-hook2207,84536
-(defcustom proof-shell-process-output-system-specific 2215,84807
-(defcustom proof-state-change-hook 2234,85671
-(defcustom proof-shell-syntax-table-entries 2244,86052
-(defgroup proof-goals 2262,86424
-(defcustom pg-subterm-first-special-char 2267,86545
-(defcustom pg-subterm-anns-use-stack 2275,86857
-(defcustom pg-goals-change-goal 2284,87156
-(defcustom pbp-goal-command 2289,87272
-(defcustom pbp-hyp-command 2294,87428
-(defcustom pg-subterm-help-cmd 2299,87590
-(defcustom pg-goals-error-regexp 2306,87826
-(defcustom proof-shell-result-start 2311,87986
-(defcustom proof-shell-result-end 2317,88220
-(defcustom pg-subterm-start-char 2323,88433
-(defcustom pg-subterm-sep-char 2337,89019
-(defcustom pg-subterm-end-char 2343,89198
-(defcustom pg-topterm-regexp 2349,89355
-(defcustom proof-goals-font-lock-keywords 2364,89955
-(defcustom proof-resp-font-lock-keywords 2372,90282
-(defcustom pg-before-fontify-output-hook 2380,90611
-(defcustom pg-after-fontify-output-hook 2388,90972
-(defcustom proof-general-name 2400,91221
-(defcustom proof-general-home-page2405,91378
-(defcustom proof-unnamed-theorem-name2411,91538
-(defcustom proof-universal-keys2417,91722
+(defun proof-unicode-tokens-support-available 59,1586
+
+generic/proof-config.el,10807
+(defgroup proof-user-options 84,2964
+(defun proof-set-value 92,3143
+(defcustom proof-electric-terminator-enable 125,4266
+(defcustom proof-toolbar-enable 137,4798
+(defcustom proof-imenu-enable 143,4971
+(defcustom pg-show-hints 149,5142
+(defcustom proof-trace-output-slow-catchup 155,5337
+(defcustom proof-strict-state-preserving 165,5834
+(defcustom proof-strict-read-only 178,6443
+(defcustom proof-allow-undo-in-read-only 187,6836
+(defcustom proof-three-window-enable 195,7169
+(defcustom proof-multiple-frames-enable 214,7919
+(defcustom proof-delete-empty-windows 223,8252
+(defcustom proof-shrink-windows-tofit 234,8783
+(defcustom proof-query-file-save-when-activating-scripting241,9055
+(defcustom proof-one-command-per-line257,9775
+(defcustom proof-prog-name-ask264,10002
+(defcustom proof-prog-name-guess270,10162
+(defcustom proof-tidy-response278,10427
+(defcustom proof-keep-response-history292,10890
+(defcustom pg-input-ring-size 302,11278
+(defcustom proof-general-debug 307,11430
+(defcustom proof-experimental-features 317,11802
+(defcustom proof-follow-mode 331,12337
+(defcustom proof-auto-action-when-deactivating-scripting 355,13514
+(defcustom proof-script-command-separator 378,14463
+(defcustom proof-rsh-command 386,14755
+(defcustom proof-disappearing-proofs 402,15305
+(defgroup proof-faces 429,15951
+(defconst pg-defface-window-systems436,16133
+(defmacro proof-face-specs 449,16686
+(defface proof-queue-face464,17138
+(defface proof-locked-face472,17416
+(defface proof-declaration-name-face482,17737
+(defface proof-tacticals-name-face491,18023
+(defface proof-tactics-name-face500,18285
+(defface proof-error-face509,18550
+(defface proof-warning-face517,18740
+(defface proof-eager-annotation-face526,18997
+(defface proof-debug-message-face534,19215
+(defface proof-boring-face542,19414
+(defface proof-mouse-highlight-face550,19606
+(defface proof-highlight-dependent-face558,19802
+(defface proof-highlight-dependency-face566,20011
+(defface proof-active-area-face574,20208
+(defconst proof-face-compat-doc 583,20598
+(defconst proof-queue-face 584,20678
+(defconst proof-locked-face 585,20746
+(defconst proof-declaration-name-face 586,20816
+(defconst proof-tacticals-name-face 587,20906
+(defconst proof-tactics-name-face 588,20992
+(defconst proof-error-face 589,21074
+(defconst proof-warning-face 590,21142
+(defconst proof-eager-annotation-face 591,21214
+(defconst proof-debug-message-face 592,21304
+(defconst proof-boring-face 593,21388
+(defconst proof-mouse-highlight-face 594,21458
+(defconst proof-highlight-dependent-face 595,21546
+(defconst proof-highlight-dependency-face 596,21642
+(defconst proof-active-area-face 597,21740
+(defgroup prover-config 610,21884
+(defcustom proof-guess-command-line 652,23213
+(defcustom proof-assistant-home-page 667,23708
+(defcustom proof-context-command 673,23878
+(defcustom proof-info-command 678,24012
+(defcustom proof-showproof-command 685,24283
+(defcustom proof-goal-command 690,24419
+(defcustom proof-save-command 698,24716
+(defcustom proof-find-theorems-command 706,25025
+(defcustom proof-assistant-true-value 713,25335
+(defcustom proof-assistant-false-value 719,25525
+(defcustom proof-assistant-format-int-fn 725,25719
+(defcustom proof-assistant-format-string-fn 732,25968
+(defcustom proof-assistant-setting-format 739,26235
+(defgroup proof-script 761,26930
+(defcustom proof-terminal-char 766,27060
+(defcustom proof-script-sexp-commands 776,27447
+(defcustom proof-script-command-end-regexp 787,27904
+(defcustom proof-script-command-start-regexp 805,28723
+(defcustom proof-script-use-old-parser 816,29184
+(defcustom proof-script-integral-proofs 828,29670
+(defcustom proof-script-fly-past-comments 843,30326
+(defcustom proof-script-parse-function 848,30497
+(defcustom proof-script-comment-start 866,31140
+(defcustom proof-script-comment-start-regexp 877,31577
+(defcustom proof-script-comment-end 885,31896
+(defcustom proof-script-comment-end-regexp 897,32318
+(defcustom pg-insert-output-as-comment-fn 905,32629
+(defcustom proof-string-start-regexp 911,32881
+(defcustom proof-string-end-regexp 916,33046
+(defcustom proof-case-fold-search 921,33207
+(defcustom proof-save-command-regexp 930,33619
+(defcustom proof-save-with-hole-regexp 935,33729
+(defcustom proof-save-with-hole-result 947,34183
+(defcustom proof-goal-command-regexp 957,34631
+(defcustom proof-goal-with-hole-regexp 966,35019
+(defcustom proof-goal-with-hole-result 978,35462
+(defcustom proof-non-undoables-regexp 987,35846
+(defcustom proof-nested-undo-regexp 998,36301
+(defcustom proof-ignore-for-undo-count 1014,37013
+(defcustom proof-script-next-entity-regexps 1022,37316
+(defcustom proof-script-find-next-entity-fn1066,39057
+(defcustom proof-script-imenu-generic-expression 1086,39897
+(defcustom proof-goal-command-p 1094,40236
+(defcustom proof-really-save-command-p 1105,40727
+(defcustom proof-completed-proof-behaviour 1114,41034
+(defcustom proof-count-undos-fn 1142,42390
+(defconst proof-no-command 1154,42939
+(defcustom proof-find-and-forget-fn 1159,43146
+(defcustom proof-forget-id-command 1176,43860
+(defcustom pg-topterm-goalhyplit-fn 1186,44218
+(defcustom proof-kill-goal-command 1198,44753
+(defcustom proof-undo-n-times-cmd 1212,45256
+(defcustom proof-nested-goals-history-p 1226,45804
+(defcustom proof-state-preserving-p 1235,46141
+(defcustom proof-activate-scripting-hook 1245,46613
+(defcustom proof-deactivate-scripting-hook 1264,47394
+(defcustom proof-indent 1277,47759
+(defcustom proof-indent-hang 1282,47866
+(defcustom proof-indent-enclose-offset 1287,47992
+(defcustom proof-indent-open-offset 1292,48134
+(defcustom proof-indent-close-offset 1297,48271
+(defcustom proof-indent-any-regexp 1302,48409
+(defcustom proof-indent-inner-regexp 1307,48569
+(defcustom proof-indent-enclose-regexp 1312,48723
+(defcustom proof-indent-open-regexp 1317,48877
+(defcustom proof-indent-close-regexp 1322,49029
+(defcustom proof-script-font-lock-keywords 1328,49183
+(defcustom proof-script-syntax-table-entries 1336,49500
+(defcustom proof-script-span-context-menu-extensions 1354,49897
+(defgroup proof-shell 1380,50657
+(defcustom proof-prog-name 1390,50828
+(defcustom proof-shell-auto-terminate-commands 1401,51248
+(defcustom proof-shell-pre-sync-init-cmd 1410,51649
+(defcustom proof-shell-init-cmd 1424,52207
+(defcustom proof-shell-init-hook 1436,52736
+(defcustom proof-shell-restart-cmd 1441,52875
+(defcustom proof-shell-quit-cmd 1446,53030
+(defcustom proof-shell-quit-timeout 1451,53197
+(defcustom proof-shell-cd-cmd 1461,53647
+(defcustom proof-shell-start-silent-cmd 1478,54318
+(defcustom proof-shell-stop-silent-cmd 1487,54694
+(defcustom proof-shell-silent-threshold 1496,55029
+(defcustom  proof-shell-inform-file-processed-cmd 1504,55363
+(defcustom  proof-shell-inform-file-retracted-cmd 1525,56291
+(defcustom proof-auto-multiple-files 1553,57563
+(defcustom proof-cannot-reopen-processed-files 1568,58284
+(defcustom proof-shell-require-command-regexp 1582,58950
+(defcustom proof-done-advancing-require-function 1593,59412
+(defcustom proof-shell-quiet-errors 1599,59647
+(defcustom proof-shell-prompt-pattern 1612,59981
+(defcustom proof-shell-wakeup-char 1622,60402
+(defcustom proof-shell-annotated-prompt-regexp 1628,60633
+(defcustom proof-shell-abort-goal-regexp 1644,61269
+(defcustom proof-shell-error-regexp 1649,61404
+(defcustom proof-shell-truncate-before-error 1669,62204
+(defcustom pg-next-error-regexp 1683,62743
+(defcustom pg-next-error-filename-regexp 1698,63352
+(defcustom pg-next-error-extract-filename 1722,64385
+(defcustom proof-shell-interrupt-regexp 1729,64628
+(defcustom proof-shell-proof-completed-regexp 1743,65223
+(defcustom proof-shell-clear-response-regexp 1756,65731
+(defcustom proof-shell-clear-goals-regexp 1763,66030
+(defcustom proof-shell-start-goals-regexp 1770,66323
+(defcustom proof-shell-end-goals-regexp 1778,66690
+(defcustom proof-shell-eager-annotation-start 1784,66934
+(defcustom proof-shell-eager-annotation-start-length 1807,67953
+(defcustom proof-shell-eager-annotation-end 1818,68379
+(defcustom proof-shell-assumption-regexp 1834,69054
+(defcustom proof-shell-process-file 1844,69457
+(defcustom proof-shell-retract-files-regexp 1866,70413
+(defcustom proof-shell-compute-new-files-list 1875,70749
+(defcustom pg-use-specials-for-fontify 1887,71297
+(defcustom pg-special-char-regexp 1895,71645
+(defcustom proof-shell-set-elisp-variable-regexp 1901,71790
+(defcustom proof-shell-match-pgip-cmd 1934,73303
+(defcustom proof-shell-issue-pgip-cmd 1943,73632
+(defcustom proof-shell-query-dependencies-cmd 1952,73988
+(defcustom proof-shell-theorem-dependency-list-regexp 1959,74248
+(defcustom proof-shell-theorem-dependency-list-split 1975,74908
+(defcustom proof-shell-show-dependency-cmd 1984,75331
+(defcustom proof-shell-identifier-under-mouse-cmd 1991,75600
+(defcustom proof-shell-trace-output-regexp 2014,76681
+(defcustom proof-shell-thms-output-regexp 2028,77139
+(defcustom proof-tokens-activate-command 2041,77522
+(defcustom proof-tokens-deactivate-command 2048,77763
+(defcustom proof-tokens-extra-modes 2055,78010
+(defcustom proof-shell-unicode 2070,78517
+(defcustom proof-shell-filename-escapes 2078,78837
+(defcustom proof-shell-process-connection-type2095,79517
+(defcustom proof-shell-strip-crs-from-input 2118,80563
+(defcustom proof-shell-strip-crs-from-output 2130,81048
+(defcustom proof-shell-insert-hook 2138,81416
+(defcustom proof-shell-handle-delayed-output-hook2176,83276
+(defcustom proof-shell-handle-error-or-interrupt-hook2182,83491
+(defcustom proof-shell-pre-interrupt-hook2200,84244
+(defcustom proof-shell-process-output-system-specific 2208,84515
+(defcustom proof-state-change-hook 2227,85379
+(defcustom proof-shell-syntax-table-entries 2237,85760
+(defgroup proof-goals 2255,86132
+(defcustom pg-subterm-first-special-char 2260,86253
+(defcustom pg-subterm-anns-use-stack 2268,86565
+(defcustom pg-goals-change-goal 2277,86864
+(defcustom pbp-goal-command 2282,86980
+(defcustom pbp-hyp-command 2287,87136
+(defcustom pg-subterm-help-cmd 2292,87298
+(defcustom pg-goals-error-regexp 2299,87534
+(defcustom proof-shell-result-start 2304,87694
+(defcustom proof-shell-result-end 2310,87928
+(defcustom pg-subterm-start-char 2316,88141
+(defcustom pg-subterm-sep-char 2330,88727
+(defcustom pg-subterm-end-char 2336,88906
+(defcustom pg-topterm-regexp 2342,89063
+(defcustom proof-goals-font-lock-keywords 2357,89663
+(defcustom proof-resp-font-lock-keywords 2365,89990
+(defcustom pg-before-fontify-output-hook 2373,90319
+(defcustom pg-after-fontify-output-hook 2381,90680
+(defcustom proof-general-name 2393,90929
+(defcustom proof-general-home-page2398,91086
+(defcustom proof-unnamed-theorem-name2404,91246
+(defcustom proof-universal-keys2410,91430
 
 generic/proof-depends.el,824
-(defvar proof-thm-names-of-files 23,624
-(defvar proof-def-names-of-files 29,908
-(defun proof-depends-module-name-for-buffer 38,1212
-(defun proof-depends-module-of 48,1654
-(defun proof-depends-names-in-same-file 56,1948
-(defun proof-depends-process-dependencies 75,2568
-(defun proof-dependency-in-span-context-menu 128,4317
-(defun proof-dep-alldeps-menu 151,5220
-(defun proof-dep-make-alldeps-menu 157,5447
-(defun proof-dep-split-deps 175,5943
-(defun proof-dep-make-submenu 196,6642
-(defun proof-make-highlight-depts-menu 206,6995
-(defun proof-goto-dependency 216,7299
-(defun proof-show-dependency 222,7522
-(defconst pg-dep-span-priority 229,7812
-(defconst pg-ordinary-span-priority 230,7848
-(defun proof-highlight-depcs 232,7890
-(defun proof-highlight-depts 242,8320
-(defun proof-dep-unhighlight 253,8794
+(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
 
 generic/proof-easy-config.el,192
-(defconst proof-easy-config-derived-modes-table16,547
-(defun proof-easy-config-define-derived-modes 23,953
-(defun proof-easy-config-check-setup 52,2136
-(defmacro proof-easy-config 84,3471
+(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
 
 generic/proof-indent.el,219
-(defun proof-indent-indent 14,411
-(defun proof-indent-offset 23,677
-(defun proof-indent-inner-p 40,1277
-(defun proof-indent-goto-prev 49,1584
-(defun proof-indent-calculate 56,1917
-(defun proof-indent-line 76,2639
+(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
 
 generic/proof-maths-menu.el,83
-(defun proof-maths-menu-set-global 30,962
-(defun proof-maths-menu-enable 44,1418
+(defun proof-maths-menu-set-global 30,959
+(defun proof-maths-menu-enable 44,1415
 
 generic/proof-menu.el,2100
-(defvar proof-display-some-buffers-count 17,440
-(defun proof-display-some-buffers 19,485
-(defun proof-menu-define-keys 78,2687
-(defun proof-menu-define-main 137,5516
-(defvar proof-menu-favourites 146,5704
-(defun proof-menu-define-specific 150,5826
-(defun proof-assistant-menu-update 188,6844
-(defvar proof-help-menu202,7277
-(defvar proof-show-hide-menu210,7555
-(defvar proof-buffer-menu219,7868
-(defun proof-keep-response-history 278,9954
-(defconst proof-quick-opts-menu286,10264
-(defun proof-quick-opts-vars 435,16396
-(defun proof-quick-opts-changed-from-defaults-p 460,17153
-(defun proof-quick-opts-changed-from-saved-p 464,17258
-(defun proof-quick-opts-save 475,17610
-(defun proof-quick-opts-reset 480,17778
-(defconst proof-config-menu492,18046
-(defconst proof-advanced-menu499,18225
-(defvar proof-menu 512,18660
-(defun proof-main-menu 521,18944
-(defun proof-aux-menu 532,19210
-(defun proof-menu-define-favourites-menu 548,19557
-(defun proof-def-favourite 568,20213
-(defvar proof-make-favourite-cmd-history 591,21188
-(defvar proof-make-favourite-menu-history 594,21273
-(defun proof-save-favourites 597,21359
-(defun proof-del-favourite 602,21507
-(defun proof-read-favourite 619,22068
-(defun proof-add-favourite 644,22871
-(defvar proof-menu-settings 671,23922
-(defun proof-menu-define-settings-menu 674,23996
-(defun proof-menu-entry-name 694,24740
-(defun proof-menu-entry-for-setting 706,25212
-(defun proof-settings-vars 724,25702
-(defun proof-settings-changed-from-defaults-p 729,25879
-(defun proof-settings-changed-from-saved-p 733,25985
-(defun proof-settings-save 737,26088
-(defun proof-settings-reset 742,26255
-(defun proof-defpacustom-fn 749,26500
-(defmacro defpacustom 825,29391
-(defun proof-assistant-invisible-command-ifposs 840,30218
-(defun proof-maybe-askprefs 862,31193
-(defun proof-assistant-settings-cmd 869,31397
-(defvar proof-assistant-format-table 886,32057
-(defun proof-assistant-format-bool 894,32426
-(defun proof-assistant-format-int 897,32539
-(defun proof-assistant-format-string 900,32631
-(defun proof-assistant-format 903,32729
+(defvar proof-display-some-buffers-count 17,437
+(defun proof-display-some-buffers 19,482
+(defun proof-menu-define-keys 78,2684
+(defun proof-menu-define-main 137,5513
+(defvar proof-menu-favourites 146,5701
+(defun proof-menu-define-specific 150,5823
+(defun proof-assistant-menu-update 188,6841
+(defvar proof-help-menu202,7274
+(defvar proof-show-hide-menu210,7552
+(defvar proof-buffer-menu219,7865
+(defun proof-keep-response-history 278,9951
+(defconst proof-quick-opts-menu286,10261
+(defun proof-quick-opts-vars 437,16483
+(defun proof-quick-opts-changed-from-defaults-p 462,17240
+(defun proof-quick-opts-changed-from-saved-p 466,17345
+(defun proof-quick-opts-save 477,17697
+(defun proof-quick-opts-reset 482,17865
+(defconst proof-config-menu494,18133
+(defconst proof-advanced-menu501,18312
+(defvar proof-menu 514,18747
+(defun proof-main-menu 523,19031
+(defun proof-aux-menu 534,19297
+(defun proof-menu-define-favourites-menu 550,19644
+(defun proof-def-favourite 570,20300
+(defvar proof-make-favourite-cmd-history 593,21275
+(defvar proof-make-favourite-menu-history 596,21360
+(defun proof-save-favourites 599,21446
+(defun proof-del-favourite 604,21594
+(defun proof-read-favourite 621,22155
+(defun proof-add-favourite 646,22958
+(defvar proof-menu-settings 673,24009
+(defun proof-menu-define-settings-menu 676,24083
+(defun proof-menu-entry-name 696,24827
+(defun proof-menu-entry-for-setting 708,25299
+(defun proof-settings-vars 726,25789
+(defun proof-settings-changed-from-defaults-p 731,25966
+(defun proof-settings-changed-from-saved-p 735,26072
+(defun proof-settings-save 739,26175
+(defun proof-settings-reset 744,26342
+(defun proof-defpacustom-fn 751,26587
+(defmacro defpacustom 827,29478
+(defun proof-assistant-invisible-command-ifposs 842,30305
+(defun proof-maybe-askprefs 864,31280
+(defun proof-assistant-settings-cmd 871,31484
+(defvar proof-assistant-format-table 888,32144
+(defun proof-assistant-format-bool 896,32513
+(defun proof-assistant-format-int 899,32626
+(defun proof-assistant-format-string 902,32718
+(defun proof-assistant-format 905,32816
 
 generic/proof-mmm.el,70
-(defun proof-mmm-set-global 41,1516
-(defun proof-mmm-enable 56,2057
+(defun proof-mmm-set-global 41,1517
+(defun proof-mmm-enable 56,2058
 
 generic/proof-script.el,5199
-(defvar proof-element-counters 28,717
-(deflocal proof-active-buffer-fake-minor-mode 34,857
-(deflocal proof-script-buffer-file-name 37,983
-(deflocal pg-script-portions 44,1393
-(defun proof-next-element-count 54,1629
-(defun proof-element-id 63,1964
-(defun proof-next-element-id 67,2133
-(deflocal proof-script-last-entity 81,2450
-(defun proof-script-find-next-entity 88,2730
-(deflocal proof-locked-span 164,5472
-(deflocal proof-queue-span 171,5738
-(defun proof-span-give-warning 183,6252
-(defun proof-span-read-only 187,6366
-(defun proof-strict-read-only 196,6798
-(defsubst proof-set-locked-endpoints 234,8529
-(defsubst proof-detach-queue 238,8673
-(defsubst proof-detach-locked 242,8805
-(defsubst proof-set-queue-start 246,8941
-(defsubst proof-set-locked-end 250,9067
-(defsubst proof-set-queue-end 263,9552
-(defun proof-init-segmentation 274,9849
-(defun proof-restart-buffers 307,11244
-(defun proof-script-buffers-with-spans 329,12176
-(defun proof-script-remove-all-spans-and-deactivate 339,12532
-(defun proof-script-clear-queue-spans 343,12720
-(defun proof-unprocessed-begin 362,13281
-(defun proof-script-end 370,13535
-(defun proof-queue-or-locked-end 379,13836
-(defun proof-locked-end 394,14514
-(defun proof-locked-region-full-p 411,14899
-(defun proof-locked-region-empty-p 420,15171
-(defun proof-only-whitespace-to-locked-region-p 424,15321
-(defun proof-in-locked-region-p 437,15957
-(defun proof-goto-end-of-locked 449,16220
-(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 466,16979
-(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 477,17460
-(defun proof-end-of-locked-visible-p 491,18113
-(defun proof-goto-end-of-queue-or-locked-if-not-visible 500,18564
-(defvar pg-idioms 519,19214
-(defvar pg-visibility-specs 522,19310
-(defconst pg-default-invisibility-spec 527,19517
-(defun pg-clear-script-portions 531,19657
-(defun pg-add-script-element 538,19905
-(defun pg-remove-script-element 541,19981
-(defsubst pg-visname 549,20275
-(defun pg-add-element 553,20420
-(defun pg-open-invisible-span 587,22049
-(defun pg-remove-element 598,22412
-(defun pg-make-element-invisible 605,22682
-(defun pg-make-element-visible 611,22926
-(defun pg-toggle-element-visibility 615,23069
-(defun pg-redisplay-for-gnuemacs 622,23356
-(defun pg-show-all-portions 626,23502
-(defun pg-show-all-proofs 644,24173
-(defun pg-hide-all-proofs 649,24301
-(defun pg-add-proof-element 654,24432
-(defun pg-span-name 668,25052
-(defvar pg-span-context-menu-keymap689,25759
-(defun pg-set-span-helphighlights 698,26013
-(defun proof-complete-buffer-atomic 724,26880
-(defun proof-register-possibly-new-processed-file 765,28795
-(defun proof-inform-prover-file-retracted 816,30923
-(defun proof-auto-retract-dependencies 835,31709
-(defun proof-unregister-buffer-file-name 889,34249
-(defun proof-protected-process-or-retract 935,36072
-(defun proof-deactivate-scripting-auto 962,37242
-(defun proof-deactivate-scripting 971,37600
-(defun proof-activate-scripting 1104,42873
-(defun proof-toggle-active-scripting 1224,48251
-(defun proof-done-advancing 1265,49612
-(defun proof-done-advancing-comment 1360,53260
-(defun proof-done-advancing-save 1379,54002
-(defun proof-make-goalsave 1472,57617
-(defun proof-get-name-from-goal 1487,58360
-(defun proof-done-advancing-autosave 1506,59386
-(defun proof-done-advancing-other 1571,61932
-(defun proof-segment-up-to-parser 1599,62891
-(defun proof-script-generic-parse-find-comment-end 1663,64961
-(defun proof-script-generic-parse-cmdend 1672,65377
-(defun proof-script-generic-parse-cmdstart 1697,66272
-(defun proof-script-generic-parse-sexp 1760,68980
-(defun proof-cmdstart-add-segment-for-cmd 1784,69916
-(defun proof-segment-up-to-cmdstart 1836,72115
-(defun proof-segment-up-to-cmdend 1897,74475
-(defun proof-semis-to-vanillas 1969,77140
-(defun proof-script-new-command-advance 2008,78466
-(defun proof-script-next-command-advance 2050,80207
-(defun proof-assert-until-point-interactive 2062,80648
-(defun proof-assert-until-point 2088,81770
-(defun proof-assert-next-command2141,84202
-(defun proof-retract-before-change 2189,86440
-(defun proof-goto-point 2196,86659
-(defun proof-insert-pbp-command 2214,87200
-(defun proof-insert-sendback-command 2228,87669
-(defun proof-done-retracting 2254,88559
-(defun proof-setup-retract-action 2290,90045
-(defun proof-last-goal-or-goalsave 2300,90528
-(defun proof-retract-target 2323,91368
-(defun proof-retract-until-point-interactive 2408,95009
-(defun proof-retract-until-point 2416,95394
-(define-derived-mode proof-mode 2459,97143
-(defun proof-script-set-visited-file-name 2492,98368
-(defun proof-script-set-buffer-hooks 2516,99370
-(defun proof-script-kill-buffer-fn 2524,99788
-(defun proof-config-done-related 2556,101102
-(defun proof-generic-goal-command-p 2624,103630
-(defun proof-generic-state-preserving-p 2629,103842
-(defun proof-generic-count-undos 2638,104359
-(defun proof-generic-find-and-forget 2667,105389
-(defconst proof-script-important-settings2718,107214
-(defun proof-config-done 2733,107767
-(defun proof-setup-parsing-mechanism 2802,110073
-(defun proof-setup-imenu 2846,111926
-(defun proof-setup-func-menu 2863,112531
+(defvar proof-element-counters 28,714
+(deflocal proof-active-buffer-fake-minor-mode 34,854
+(deflocal proof-script-buffer-file-name 37,980
+(deflocal pg-script-portions 44,1390
+(defun proof-next-element-count 54,1626
+(defun proof-element-id 63,1961
+(defun proof-next-element-id 67,2130
+(deflocal proof-script-last-entity 81,2447
+(defun proof-script-find-next-entity 88,2727
+(deflocal proof-locked-span 164,5469
+(deflocal proof-queue-span 171,5735
+(defun proof-span-give-warning 183,6249
+(defun proof-span-read-only 187,6363
+(defun proof-strict-read-only 196,6795
+(defsubst proof-set-locked-endpoints 234,8526
+(defsubst proof-detach-queue 238,8670
+(defsubst proof-detach-locked 242,8802
+(defsubst proof-set-queue-start 246,8938
+(defsubst proof-set-locked-end 250,9064
+(defsubst proof-set-queue-end 263,9549
+(defun proof-init-segmentation 274,9846
+(defun proof-restart-buffers 307,11241
+(defun proof-script-buffers-with-spans 329,12173
+(defun proof-script-remove-all-spans-and-deactivate 339,12529
+(defun proof-script-clear-queue-spans 343,12717
+(defun proof-unprocessed-begin 362,13278
+(defun proof-script-end 370,13532
+(defun proof-queue-or-locked-end 379,13833
+(defun proof-locked-end 394,14511
+(defun proof-locked-region-full-p 411,14896
+(defun proof-locked-region-empty-p 420,15168
+(defun proof-only-whitespace-to-locked-region-p 424,15318
+(defun proof-in-locked-region-p 437,15954
+(defun proof-goto-end-of-locked 449,16217
+(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 466,16976
+(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 477,17457
+(defun proof-end-of-locked-visible-p 491,18110
+(defun proof-goto-end-of-queue-or-locked-if-not-visible 500,18561
+(defvar pg-idioms 519,19211
+(defvar pg-visibility-specs 522,19307
+(defconst pg-default-invisibility-spec 527,19514
+(defun pg-clear-script-portions 531,19654
+(defun pg-add-script-element 538,19902
+(defun pg-remove-script-element 541,19978
+(defsubst pg-visname 549,20272
+(defun pg-add-element 553,20417
+(defun pg-open-invisible-span 587,22046
+(defun pg-remove-element 598,22409
+(defun pg-make-element-invisible 605,22679
+(defun pg-make-element-visible 611,22923
+(defun pg-toggle-element-visibility 615,23066
+(defun pg-redisplay-for-gnuemacs 622,23353
+(defun pg-show-all-portions 626,23499
+(defun pg-show-all-proofs 644,24170
+(defun pg-hide-all-proofs 649,24298
+(defun pg-add-proof-element 654,24429
+(defun pg-span-name 668,25049
+(defvar pg-span-context-menu-keymap689,25756
+(defun pg-set-span-helphighlights 698,26010
+(defun proof-complete-buffer-atomic 724,26877
+(defun proof-register-possibly-new-processed-file 765,28792
+(defun proof-inform-prover-file-retracted 816,30920
+(defun proof-auto-retract-dependencies 835,31706
+(defun proof-unregister-buffer-file-name 889,34246
+(defun proof-protected-process-or-retract 935,36069
+(defun proof-deactivate-scripting-auto 962,37239
+(defun proof-deactivate-scripting 971,37597
+(defun proof-activate-scripting 1104,42870
+(defun proof-toggle-active-scripting 1224,48248
+(defun proof-done-advancing 1265,49609
+(defun proof-done-advancing-comment 1360,53257
+(defun proof-done-advancing-save 1379,53999
+(defun proof-make-goalsave 1472,57614
+(defun proof-get-name-from-goal 1487,58357
+(defun proof-done-advancing-autosave 1506,59383
+(defun proof-done-advancing-other 1571,61929
+(defun proof-segment-up-to-parser 1599,62888
+(defun proof-script-generic-parse-find-comment-end 1663,64958
+(defun proof-script-generic-parse-cmdend 1672,65374
+(defun proof-script-generic-parse-cmdstart 1697,66269
+(defun proof-script-generic-parse-sexp 1760,68977
+(defun proof-cmdstart-add-segment-for-cmd 1784,69913
+(defun proof-segment-up-to-cmdstart 1836,72112
+(defun proof-segment-up-to-cmdend 1897,74472
+(defun proof-semis-to-vanillas 1969,77137
+(defun proof-script-new-command-advance 2008,78463
+(defun proof-script-next-command-advance 2050,80204
+(defun proof-assert-until-point-interactive 2062,80645
+(defun proof-assert-until-point 2088,81767
+(defun proof-assert-next-command2141,84199
+(defun proof-retract-before-change 2189,86437
+(defun proof-goto-point 2196,86656
+(defun proof-insert-pbp-command 2214,87197
+(defun proof-insert-sendback-command 2228,87666
+(defun proof-done-retracting 2254,88556
+(defun proof-setup-retract-action 2290,90042
+(defun proof-last-goal-or-goalsave 2300,90525
+(defun proof-retract-target 2323,91365
+(defun proof-retract-until-point-interactive 2408,95006
+(defun proof-retract-until-point 2416,95391
+(define-derived-mode proof-mode 2459,97140
+(defun proof-script-set-visited-file-name 2492,98365
+(defun proof-script-set-buffer-hooks 2516,99367
+(defun proof-script-kill-buffer-fn 2524,99785
+(defun proof-config-done-related 2556,101099
+(defun proof-generic-goal-command-p 2624,103627
+(defun proof-generic-state-preserving-p 2629,103839
+(defun proof-generic-count-undos 2638,104356
+(defun proof-generic-find-and-forget 2667,105386
+(defconst proof-script-important-settings2718,107211
+(defun proof-config-done 2733,107764
+(defun proof-setup-parsing-mechanism 2802,110070
+(defun proof-setup-imenu 2846,111923
+(defun proof-setup-func-menu 2863,112528
 
 generic/proof-shell.el,3159
-(defvar proof-marker 28,653
-(defvar proof-action-list 31,750
-(defvar proof-shell-silent 39,926
-(defvar proof-shell-last-prompt 46,1217
-(defvar proof-shell-last-output-kind 50,1388
-(defvar proof-shell-delayed-output 71,2210
-(defvar proof-shell-delayed-output-kind 74,2331
-(defcustom proof-shell-active-scripting-indicator83,2534
-(defun proof-shell-ready-prover 133,3925
-(defun proof-shell-live-buffer 147,4465
-(defun proof-shell-available-p 154,4700
-(defun proof-grab-lock 160,4923
-(defun proof-release-lock 172,5482
-(defcustom proof-shell-fiddle-frames 187,5881
-(defun proof-shell-set-text-representation 193,6104
-(defun proof-shell-start 204,6566
-(defvar proof-shell-kill-function-hooks 405,13770
-(defun proof-shell-kill-function 408,13868
-(defun proof-shell-clear-state 497,17671
-(defun proof-shell-exit 512,18114
-(defun proof-shell-bail-out 524,18559
-(defun proof-shell-restart 533,19036
-(defvar proof-shell-no-response-display 575,20420
-(defvar proof-shell-urgent-message-marker 578,20524
-(defvar proof-shell-urgent-message-scanner 581,20645
-(defun proof-shell-handle-output 585,20772
-(defun proof-shell-handle-delayed-output 620,22091
-(defvar proof-shell-no-error-display 648,23134
-(defun proof-shell-handle-error 654,23338
-(defun proof-shell-handle-interrupt 670,24071
-(defun proof-shell-error-or-interrupt-action 684,24684
-(defun proof-goals-pos 709,25829
-(defun proof-pbp-focus-on-first-goal 714,26034
-(defsubst proof-shell-string-match-safe 726,26461
-(defun proof-shell-process-output 731,26629
-(defun proof-shell-insert 843,31284
-(defun proof-shell-command-queue-item 896,33385
-(defun proof-shell-set-silent 901,33542
-(defun proof-shell-start-silent-item 907,33761
-(defun proof-shell-clear-silent 913,33953
-(defun proof-shell-stop-silent-item 919,34175
-(defun proof-shell-should-be-silent 926,34447
-(defun proof-append-alist 939,35003
-(defun proof-start-queue 998,37240
-(defun proof-extend-queue 1009,37589
-(defun proof-shell-exec-loop 1018,37968
-(defun proof-shell-insert-loopback-cmd 1083,40556
-(defun proof-shell-message 1111,41882
-(defun proof-shell-process-urgent-message 1117,42098
-(defun proof-shell-strip-eager-annotations 1244,47164
-(defvar proof-shell-minibuffer-urgent-interactive-input-history 1255,47500
-(defun proof-shell-minibuffer-urgent-interactive-input 1257,47570
-(defun proof-shell-process-urgent-messages 1267,47929
-(defun proof-shell-filter 1341,51033
-(defun proof-shell-filter-process-output 1497,57397
-(defvar pg-last-tracing-output-time 1550,59451
-(defconst pg-slow-mode-duration 1553,59557
-(defconst pg-fast-tracing-mode-threshold 1556,59639
-(defvar pg-tracing-cleanup-timer 1559,59767
-(defun pg-tracing-tight-loop 1561,59806
-(defun pg-finish-tracing-display 1604,61524
-(defun proof-shell-wait 1626,61894
-(defun proof-done-invisible 1645,62803
-(defun proof-shell-invisible-command 1651,62975
-(defun proof-shell-invisible-cmd-get-result 1685,64240
-(defun proof-shell-invisible-command-invisible-result 1703,64936
-(define-derived-mode proof-shell-mode 1722,65366
-(defconst proof-shell-important-settings1777,67537
-(defun proof-shell-config-done 1783,67652
+(defvar proof-marker 28,656
+(defvar proof-action-list 31,753
+(defvar proof-shell-silent 39,929
+(defvar proof-shell-last-prompt 46,1220
+(defvar proof-shell-last-output-kind 50,1391
+(defvar proof-shell-delayed-output 71,2213
+(defvar proof-shell-delayed-output-kind 74,2334
+(defcustom proof-shell-active-scripting-indicator83,2537
+(defun proof-shell-ready-prover 133,3928
+(defun proof-shell-live-buffer 147,4468
+(defun proof-shell-available-p 154,4703
+(defun proof-grab-lock 160,4926
+(defun proof-release-lock 172,5485
+(defcustom proof-shell-fiddle-frames 187,5884
+(defun proof-shell-set-text-representation 193,6107
+(defun proof-shell-start 204,6569
+(defvar proof-shell-kill-function-hooks 405,13773
+(defun proof-shell-kill-function 408,13871
+(defun proof-shell-clear-state 497,17674
+(defun proof-shell-exit 512,18117
+(defun proof-shell-bail-out 524,18562
+(defun proof-shell-restart 533,19039
+(defvar proof-shell-no-response-display 575,20423
+(defvar proof-shell-urgent-message-marker 578,20527
+(defvar proof-shell-urgent-message-scanner 581,20648
+(defun proof-shell-handle-output 585,20775
+(defun proof-shell-handle-delayed-output 620,22094
+(defvar proof-shell-no-error-display 648,23137
+(defun proof-shell-handle-error 654,23341
+(defun proof-shell-handle-interrupt 670,24074
+(defun proof-shell-error-or-interrupt-action 684,24687
+(defun proof-goals-pos 709,25832
+(defun proof-pbp-focus-on-first-goal 714,26037
+(defsubst proof-shell-string-match-safe 726,26464
+(defun proof-shell-process-output 731,26632
+(defun proof-shell-insert 844,31349
+(defun proof-shell-command-queue-item 897,33450
+(defun proof-shell-set-silent 902,33607
+(defun proof-shell-start-silent-item 908,33826
+(defun proof-shell-clear-silent 914,34018
+(defun proof-shell-stop-silent-item 920,34240
+(defun proof-shell-should-be-silent 927,34512
+(defun proof-append-alist 940,35068
+(defun proof-start-queue 999,37305
+(defun proof-extend-queue 1010,37654
+(defun proof-shell-exec-loop 1019,38033
+(defun proof-shell-insert-loopback-cmd 1084,40621
+(defun proof-shell-message 1112,41947
+(defun proof-shell-process-urgent-message 1118,42163
+(defun proof-shell-strip-eager-annotations 1248,47300
+(defvar proof-shell-minibuffer-urgent-interactive-input-history 1259,47636
+(defun proof-shell-minibuffer-urgent-interactive-input 1261,47706
+(defun proof-shell-process-urgent-messages 1271,48065
+(defun proof-shell-filter 1345,51169
+(defun proof-shell-filter-process-output 1501,57533
+(defvar pg-last-tracing-output-time 1554,59587
+(defconst pg-slow-mode-duration 1557,59693
+(defconst pg-fast-tracing-mode-threshold 1560,59775
+(defvar pg-tracing-cleanup-timer 1563,59903
+(defun pg-tracing-tight-loop 1565,59942
+(defun pg-finish-tracing-display 1608,61660
+(defun proof-shell-wait 1630,62030
+(defun proof-done-invisible 1649,62939
+(defun proof-shell-invisible-command 1655,63111
+(defun proof-shell-invisible-cmd-get-result 1689,64376
+(defun proof-shell-invisible-command-invisible-result 1707,65072
+(define-derived-mode proof-shell-mode 1726,65502
+(defconst proof-shell-important-settings1781,67673
+(defun proof-shell-config-done 1787,67788
 
 generic/proof-site.el,504
 (defconst proof-assistant-table-default22,727
@@ -1927,523 +1926,525 @@ generic/proof-site.el,504
 (defcustom proof-assistants 180,6223
 (defun proof-ready-for-assistant 208,7368
 
-generic/proof-splash.el,761
-(defcustom proof-splash-enable 17,323
-(defcustom proof-splash-time 22,475
-(defcustom proof-splash-contents30,760
-(defconst proof-splash-startup-msg 58,1779
-(defconst proof-splash-welcome 67,2158
-(defsubst proof-emacs-imagep 74,2333
-(defun proof-get-image 79,2458
-(defvar proof-splash-timeout-conf 104,3418
-(defun proof-splash-centre-spaces 107,3531
-(defun proof-splash-remove-screen 132,4617
-(defun proof-splash-remove-buffer 149,5273
-(defvar proof-splash-seen 165,5937
-(defun proof-splash-display-screen 169,6054
-(defun proof-splash-message 236,8891
-(defun proof-splash-timeout-waiter 249,9335
-(defvar proof-splash-old-frame-title-format 262,9893
-(defun proof-splash-set-frame-titles 264,9943
-(defun proof-splash-unset-frame-titles 273,10259
+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,981
-(defun proof-ids-to-regexp 15,435
-(defun proof-anchor-regexp 19,604
-(defconst proof-no-regexp23,706
-(defun proof-regexp-alt 28,799
-(defun proof-regexp-region 37,1085
-(defun proof-re-search-forward-region 46,1508
-(defun proof-search-forward 59,2003
-(defun proof-replace-regexp-in-string 65,2255
-(defun proof-re-search-forward 71,2509
-(defun proof-re-search-backward 77,2770
-(defun proof-string-match 83,3034
-(defun proof-string-match-safe 89,3266
-(defun proof-stringfn-match 93,3471
-(defun proof-looking-at 100,3731
-(defun proof-looking-at-safe 106,3921
-(defun proof-looking-at-syntactic-context 110,4061
-(defsubst proof-replace-string 122,4424
-(defsubst proof-replace-regexp 127,4628
-(defsubst proof-replace-regexp-nocasefold 132,4837
-(defvar proof-id 140,5119
-(defun proof-ids 146,5339
-(defun proof-zap-commas 159,5895
-(defun proof-format 175,6391
-(defun proof-format-filename 194,7030
-(defun proof-insert 241,8430
-(defun proof-splice-separator 278,9446
+(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,1086
+(defun proof-re-search-forward-region 46,1509
+(defun proof-search-forward 59,2004
+(defun proof-replace-regexp-in-string 65,2256
+(defun proof-re-search-forward 71,2510
+(defun proof-re-search-backward 77,2771
+(defun proof-string-match 83,3035
+(defun proof-string-match-safe 89,3267
+(defun proof-stringfn-match 93,3472
+(defun proof-looking-at 100,3732
+(defun proof-looking-at-safe 106,3922
+(defun proof-looking-at-syntactic-context 110,4062
+(defsubst proof-replace-string 122,4425
+(defsubst proof-replace-regexp 127,4629
+(defsubst proof-replace-regexp-nocasefold 132,4838
+(defvar proof-id 140,5120
+(defun proof-ids 146,5340
+(defun proof-zap-commas 159,5896
+(defun proof-format 175,6392
+(defun proof-format-filename 194,7031
+(defun proof-insert 241,8431
+(defun proof-splice-separator 278,9447
 
 generic/proof-toolbar.el,2290
-(defun proof-toolbar-function 35,842
-(defun proof-toolbar-icon 38,939
-(defun proof-toolbar-enabler 41,1040
-(defun proof-toolbar-make-icon 48,1193
-(defun proof-toolbar-make-toolbar-items 57,1501
-(defvar proof-toolbar-map 82,2307
-(defun proof-toolbar-available-p 85,2406
-(defun proof-toolbar-setup 94,2682
-(defalias 'proof-toolbar-enable proof-toolbar-enable
112,3473
-(defalias 'proof-toolbar-undo proof-toolbar-undo
142,4453
-(defun proof-toolbar-undo-enable-p 144,4521
-(defalias 'proof-toolbar-delete proof-toolbar-delete
151,4679
-(defun proof-toolbar-delete-enable-p 153,4760
-(defalias 'proof-toolbar-lockedend proof-toolbar-lockedend
161,4947
-(defalias 'proof-toolbar-next proof-toolbar-next
165,5019
-(defun proof-toolbar-next-enable-p 167,5090
-(defalias 'proof-toolbar-goto proof-toolbar-goto
173,5206
-(defun proof-toolbar-goto-enable-p 175,5256
-(defalias 'proof-toolbar-retract proof-toolbar-retract
180,5341
-(defun proof-toolbar-retract-enable-p 182,5398
-(defalias 'proof-toolbar-use proof-toolbar-use
188,5517
-(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p
189,5569
-(defalias 'proof-toolbar-restart proof-toolbar-restart
193,5650
-(defalias 'proof-toolbar-goal proof-toolbar-goal
197,5715
-(defalias 'proof-toolbar-qed proof-toolbar-qed
201,5773
-(defun proof-toolbar-qed-enable-p 203,5822
-(defalias 'proof-toolbar-state proof-toolbar-state
211,5984
-(defalias 'proof-toolbar-state-enable-p proof-toolbar-state-enable-p
212,6027
-(defalias 'proof-toolbar-context proof-toolbar-context
216,6106
-(defalias 'proof-toolbar-context-enable-p proof-toolbar-context-enable-p
217,6152
-(defalias 'proof-toolbar-info proof-toolbar-info
221,6230
-(defalias 'proof-toolbar-command proof-toolbar-command
225,6286
-(defalias 'proof-toolbar-command-enable-p proof-toolbar-command-enable-p
226,6342
-(defun proof-toolbar-help 230,6421
-(defalias 'proof-toolbar-find proof-toolbar-find
236,6502
-(defalias 'proof-toolbar-find-enable-p proof-toolbar-find-enable-p
237,6554
-(defalias 'proof-toolbar-visibility proof-toolbar-visibility
241,6652
-(defun proof-toolbar-visibility-enable-p 243,6712
-(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt
248,6826
-(defun proof-toolbar-interrupt-enable-p 249,6887
-(defun proof-toolbar-scripting-menu 257,7040
+(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,3470
+(defalias 'proof-toolbar-undo proof-toolbar-undo
142,4450
+(defun proof-toolbar-undo-enable-p 144,4518
+(defalias 'proof-toolbar-delete proof-toolbar-delete
151,4676
+(defun proof-toolbar-delete-enable-p 153,4757
+(defalias 'proof-toolbar-lockedend proof-toolbar-lockedend
161,4944
+(defalias 'proof-toolbar-next proof-toolbar-next
165,5016
+(defun proof-toolbar-next-enable-p 167,5087
+(defalias 'proof-toolbar-goto proof-toolbar-goto
173,5203
+(defun proof-toolbar-goto-enable-p 175,5253
+(defalias 'proof-toolbar-retract proof-toolbar-retract
180,5338
+(defun proof-toolbar-retract-enable-p 182,5395
+(defalias 'proof-toolbar-use proof-toolbar-use
188,5514
+(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p
189,5566
+(defalias 'proof-toolbar-restart proof-toolbar-restart
193,5647
+(defalias 'proof-toolbar-goal proof-toolbar-goal
197,5712
+(defalias 'proof-toolbar-qed proof-toolbar-qed
201,5770
+(defun proof-toolbar-qed-enable-p 203,5819
+(defalias 'proof-toolbar-state proof-toolbar-state
211,5981
+(defalias 'proof-toolbar-state-enable-p proof-toolbar-state-enable-p
212,6024
+(defalias 'proof-toolbar-context proof-toolbar-context
216,6103
+(defalias 'proof-toolbar-context-enable-p proof-toolbar-context-enable-p
217,6149
+(defalias 'proof-toolbar-info proof-toolbar-info
221,6227
+(defalias 'proof-toolbar-command proof-toolbar-command
225,6283
+(defalias 'proof-toolbar-command-enable-p proof-toolbar-command-enable-p
226,6339
+(defun proof-toolbar-help 230,6418
+(defalias 'proof-toolbar-find proof-toolbar-find
236,6499
+(defalias 'proof-toolbar-find-enable-p proof-toolbar-find-enable-p
237,6551
+(defalias 'proof-toolbar-visibility proof-toolbar-visibility
241,6649
+(defun proof-toolbar-visibility-enable-p 243,6709
+(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt
248,6823
+(defun proof-toolbar-interrupt-enable-p 249,6884
+(defun proof-toolbar-scripting-menu 257,7037
 
 generic/proof-unicode-tokens.el,496
-(defvar proof-unicode-tokens-initialised 28,764
-(defun proof-unicode-tokens-init 31,871
-(defun proof-unicode-tokens-configure 45,1373
-(defun proof-unicode-tokens-enable 58,1837
-(defun proof-unicode-tokens-mode-if-enabled 72,2524
-(defun proof-unicode-tokens-set-global 78,2723
-(defun proof-unicode-tokens-reconfigure 96,3363
-(defun proof-unicode-tokens-configure-prover 121,4207
-(defun proof-unicode-tokens-activate-prover 126,4388
-(defun proof-unicode-tokens-deactivate-prover 133,4634
+(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 58,1834
+(defun proof-unicode-tokens-mode-if-enabled 72,2521
+(defun proof-unicode-tokens-set-global 78,2720
+(defun proof-unicode-tokens-reconfigure 96,3360
+(defun proof-unicode-tokens-configure-prover 122,4248
+(defun proof-unicode-tokens-activate-prover 127,4429
+(defun proof-unicode-tokens-deactivate-prover 134,4675
 
 generic/proof-utils.el,1873
-(defmacro deflocal 62,1815
-(defmacro proof-with-current-buffer-if-exists 69,2053
-(deflocal proof-buffer-type 75,2263
-(defmacro proof-with-script-buffer 81,2543
-(defmacro proof-map-buffers 92,2930
-(defmacro proof-sym 97,3115
-(defsubst proof-try-require 102,3276
-(defun proof-save-some-buffers 115,3607
-(defmacro proof-ass-sym 164,5208
-(defmacro proof-ass-symv 170,5467
-(defmacro proof-ass 176,5725
-(defun proof-defpgcustom-fn 182,5977
-(defun undefpgcustom 203,6848
-(defmacro defpgcustom 209,7072
-(defun proof-defpgdefault-fn 220,7490
-(defmacro defpgdefault 234,7948
-(defmacro defpgfun 245,8310
-(defmacro proof-eval-when-ready-for-assistant 255,8575
-(defun proof-file-truename 268,8970
-(defun proof-file-to-buffer 272,9153
-(defun proof-files-to-buffers 283,9482
-(defun proof-buffers-in-mode 290,9765
-(defun pg-save-from-death 304,10215
-(defun proof-define-keys 323,10832
-(defun pg-remove-specials 334,11124
-(defun pg-remove-specials-in-string 344,11462
-(defun proof-warn-if-unset 355,11690
-(defun proof-get-window-for-buffer 360,11908
-(defun proof-display-and-keep-buffer 411,14216
-(defun proof-clean-buffer 452,16056
-(defun proof-message 467,16677
-(defun proof-warning 472,16890
-(defun pg-internal-warning 478,17172
-(defun proof-debug 486,17491
-(defun proof-switch-to-buffer 495,17841
-(defun proof-resize-window-tofit 517,18967
-(defun proof-submit-bug-report 611,23142
-(defun proof-deftoggle-fn 646,24499
-(defmacro proof-deftoggle 661,25152
-(defun proof-defintset-fn 668,25526
-(defmacro proof-defintset 684,26230
-(defun proof-defstringset-fn 691,26607
-(defmacro proof-defstringset 704,27233
-(defun proof-escape-keymap-doc 717,27689
-(defmacro proof-defshortcut 721,27822
-(defmacro proof-definvisible 736,28420
-(defun pg-custom-save-vars 764,29397
-(defun pg-custom-reset-vars 782,30120
-(defun proof-locate-executable 795,30457
+(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 452,16053
+(defun proof-message 467,16674
+(defun proof-warning 472,16887
+(defun pg-internal-warning 478,17169
+(defun proof-debug 486,17488
+(defun proof-switch-to-buffer 495,17838
+(defun proof-resize-window-tofit 517,18964
+(defun proof-submit-bug-report 611,23139
+(defun proof-deftoggle-fn 646,24496
+(defmacro proof-deftoggle 661,25149
+(defun proof-defintset-fn 668,25523
+(defmacro proof-defintset 684,26227
+(defun proof-defstringset-fn 691,26604
+(defmacro proof-defstringset 704,27230
+(defun proof-escape-keymap-doc 717,27686
+(defmacro proof-defshortcut 721,27819
+(defmacro proof-definvisible 736,28417
+(defun pg-custom-save-vars 764,29394
+(defun pg-custom-reset-vars 782,30117
+(defun proof-locate-executable 795,30454
 
 lib/bufhist.el,1099
-(defun bufhist-ring-update 32,1230
-(defgroup bufhist 41,1552
-(defcustom bufhist-ring-size 45,1633
-(defvar bufhist-ring 50,1744
-(defvar bufhist-ring-pos 53,1818
-(defvar bufhist-lastswitch-modified-tick 56,1897
-(defvar bufhist-read-only-history 59,2003
-(defvar bufhist-saved-mode-line-format 62,2074
-(defun bufhist-mode-line-format-entry 65,2175
-(defun bufhist-get-buffer-contents 97,3451
-(defun bufhist-restore-buffer-contents 109,3935
-(defun bufhist-checkpoint 117,4222
-(defun bufhist-erase-buffer 125,4591
-(defun bufhist-checkpoint-and-erase 135,4936
-(defun bufhist-switch-to-index 141,5122
-(defun bufhist-first 180,6726
-(defun bufhist-last 185,6885
-(defun bufhist-prev 190,7031
-(defun bufhist-next 198,7254
-(defun bufhist-delete 203,7394
-(defun bufhist-clear 215,7937
-(defun bufhist-init 230,8333
-(defun bufhist-exit 255,9270
-(defun bufhist-set-readwrite 265,9534
-(defun bufhist-before-change-function 280,10154
-(defun bufhist-make-buttons 292,10570
-(defconst bufhist-minor-mode-map310,11009
-(define-minor-mode bufhist-mode322,11471
-(defun bufhist-toggle-fn 342,12256
+(defun bufhist-ring-update 32,1227
+(defgroup bufhist 41,1549
+(defcustom bufhist-ring-size 45,1630
+(defvar bufhist-ring 50,1741
+(defvar bufhist-ring-pos 53,1815
+(defvar bufhist-lastswitch-modified-tick 56,1894
+(defvar bufhist-read-only-history 59,2000
+(defvar bufhist-saved-mode-line-format 62,2071
+(defun bufhist-mode-line-format-entry 65,2172
+(defun bufhist-get-buffer-contents 97,3448
+(defun bufhist-restore-buffer-contents 109,3932
+(defun bufhist-checkpoint 117,4219
+(defun bufhist-erase-buffer 125,4588
+(defun bufhist-checkpoint-and-erase 135,4933
+(defun bufhist-switch-to-index 141,5119
+(defun bufhist-first 180,6723
+(defun bufhist-last 185,6882
+(defun bufhist-prev 190,7028
+(defun bufhist-next 198,7251
+(defun bufhist-delete 203,7391
+(defun bufhist-clear 215,7934
+(defun bufhist-init 230,8330
+(defun bufhist-exit 255,9267
+(defun bufhist-set-readwrite 265,9531
+(defun bufhist-before-change-function 280,10151
+(defun bufhist-make-buttons 292,10567
+(defconst bufhist-minor-mode-map310,11006
+(define-minor-mode bufhist-mode322,11468
+(defun bufhist-toggle-fn 342,12253
 
 lib/holes.el,2447
-(defvar holes-doc 38,1073
-(defvar holes-default-hole 133,4671
-(defvar holes-active-hole 137,4840
-(defcustom holes-empty-hole-string 144,5049
-(defcustom holes-empty-hole-regexp 147,5160
-(defcustom holes-search-limit 154,5451
-(defface active-hole-face166,5827
-(defface inactive-hole-face178,6275
-(defun holes-region-beginning-or-nil 193,6751
-(defun holes-region-end-or-nil 198,6849
-(defun holes-copy-active-region 203,6935
-(defun holes-is-hole-p 210,7122
-(defun holes-hole-start-position 216,7229
-(defun holes-hole-end-position 223,7418
-(defun holes-hole-buffer 230,7602
-(defun holes-hole-at 237,7777
-(defun holes-active-hole-exist-p 244,7952
-(defun holes-active-hole-start-position 254,8210
-(defun holes-active-hole-end-position 264,8582
-(defun holes-active-hole-buffer 275,8951
-(defun holes-goto-active-hole 286,9257
-(defun holes-highlight-hole-as-active 298,9525
-(defun holes-highlight-hole 308,9837
-(defun holes-disable-active-hole 319,10129
-(defun holes-set-active-hole 337,10672
-(defun holes-is-in-hole-p 350,11018
-(defun holes-make-hole 357,11161
-(defun holes-make-hole-at 383,11907
-(defun holes-clear-hole 403,12383
-(defun holes-clear-hole-at 415,12672
-(defun holes-map-holes 424,12931
-(defun holes-mapcar-holes 432,13114
-(defun holes-clear-all-buffer-holes 438,13286
-(defun holes-next 449,13586
-(defun holes-next-after-active-hole 456,13837
-(defun holes-set-active-hole-next 464,14056
-(defun holes-replace-segment 486,14609
-(defun holes-replace 496,14963
-(defun holes-replace-active-hole 527,16158
-(defun holes-replace-update-active-hole 536,16454
-(defun holes-delete-update-active-hole 557,17127
-(defun holes-set-make-active-hole 566,17357
-(defun holes-mouse-replace-active-hole 613,19082
-(defun holes-destroy-hole 633,19592
-(defun holes-hole-at-event 650,20003
-(defun holes-mouse-destroy-hole 655,20116
-(defun holes-mouse-forget-hole 665,20356
-(defun holes-mouse-set-make-active-hole 681,20666
-(defun holes-mouse-set-active-hole 703,21203
-(defun holes-set-point-next-hole-destroy 715,21467
-(defvar hole-map731,21917
-(defvar holes-mode-map741,22300
-(defun holes-replace-string-by-holes-backward 778,23775
-(defun holes-skeleton-end-hook 796,24476
-(defconst holes-jump-doc 805,24914
-(defun holes-replace-string-by-holes-backward-jump 812,25121
-(defun holes-abbrev-complete 830,25767
-(defun holes-insert-and-expand 839,26088
-(defvar holes-mode 850,26520
-(defun holes-mode 856,26716
+(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
 
 lib/local-vars-list.el,373
-(defconst local-vars-list-doc 28,831
-(defun local-vars-list-insert-empty-zone 44,1394
-(defun local-vars-list-find 82,2102
-(defun local-vars-list-goto-var 101,2877
-(defun local-vars-list-get-current 127,3927
-(defun local-vars-list-set-current 148,4777
-(defun local-vars-list-get 171,5494
-(defun local-vars-list-get-safe 188,6026
-(defun local-vars-list-set 193,6220
+(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
 
 lib/maths-menu.el,242
-(defvar maths-menu-filter-predicate 53,2240
-(defvar maths-menu-tokenise-insert 56,2349
-(defun maths-menu-build-menu 59,2488
-(defvar maths-menu-menu76,3098
-(defvar maths-menu-mode-map336,12656
-(define-minor-mode maths-menu-mode344,12875
+(defvar maths-menu-filter-predicate 53,2237
+(defvar maths-menu-tokenise-insert 56,2346
+(defun maths-menu-build-menu 59,2485
+(defvar maths-menu-menu76,3095
+(defvar maths-menu-mode-map336,12653
+(define-minor-mode maths-menu-mode344,12872
 
 lib/pg-dev.el,75
-(defconst pg-dev-lisp-font-lock-keywords36,1106
-(defun unload-pg 70,2043
+(defconst pg-dev-lisp-font-lock-keywords36,1103
+(defun unload-pg 70,2040
 
 lib/pg-fontsets.el,176
-(defcustom pg-fontsets-default-fontset 28,785
-(defun pg-fontsets-make-fontsetsizes 33,931
-(defconst pg-fontsets-base-fonts 52,1715
-(defun pg-fontsets-make-fontsets 57,1820
+(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 57,1797
 
 lib/proof-compat.el,445
-(defvar proof-running-on-win32 31,981
-(defun pg-custom-undeclare-variable 51,1759
-(defmacro save-selected-frame 97,2925
-(defun proof-buffer-syntactic-context-emulate 123,3886
-(defvar read-shell-command-map151,5096
-(defun read-shell-command 169,5784
-(defun frames-of-buffer 179,6212
-(defmacro with-selected-window 223,7625
-(defun process-live-p 255,8644
-(defalias 'proof-buffer-syntactic-context proof-buffer-syntactic-context
266,8916
+(defvar proof-running-on-win32 31,978
+(defun pg-custom-undeclare-variable 51,1756
+(defmacro save-selected-frame 97,2922
+(defun proof-buffer-syntactic-context-emulate 123,3883
+(defvar read-shell-command-map151,5093
+(defun read-shell-command 169,5781
+(defun frames-of-buffer 179,6209
+(defmacro with-selected-window 223,7622
+(defun process-live-p 255,8641
+(defalias 'proof-buffer-syntactic-context proof-buffer-syntactic-context
266,8913
 
 lib/span.el,1353
-(defalias 'span-start span-start
22,615
-(defalias 'span-end span-end
23,653
-(defalias 'span-set-property span-set-property
24,687
-(defalias 'span-property span-property
25,730
-(defalias 'span-make span-make
26,769
-(defalias 'span-detach span-detach
27,805
-(defalias 'span-set-endpoints span-set-endpoints
28,845
-(defalias 'span-buffer span-buffer
29,890
-(defun span-read-only-hook 31,931
-(defun span-read-only 36,1121
-(defun span-read-write 43,1428
-(defun span-give-warning 48,1595
-(defun span-write-warning 53,1738
-(defun span-lt 65,2322
-(defun spans-at-point-prop 70,2463
-(defun spans-at-region-prop 76,2628
-(defun span-at 85,2940
-(defsubst span-delete 91,3156
-(defsubst span-mapcar-spans 98,3378
-(defun span-at-before 103,3637
-(defun prev-span 120,4363
-(defun next-span 126,4514
-(defsubst span-live-p 133,4726
-(defun span-raise 139,4892
-(defalias 'span-object span-object
143,5022
-(defun span-string 145,5063
-(defun set-span-properties 150,5201
-(defun span-find-span 160,5448
-(defsubst span-at-event 167,5754
-(defun make-detached-span 171,5875
-(defun fold-spans 176,5971
-(defsubst span-detached-p 190,6504
-(defsubst set-span-face 194,6620
-(defun set-span-keymap 198,6718
-(defsubst span-delete-spans 207,6921
-(defsubst span-property-safe 211,7085
-(defsubst span-set-start 215,7224
-(defsubst span-set-end 219,7356
+(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
 
 lib/texi-docstring-magic.el,584
-(defun texi-docstring-magic-find-face 88,3034
-(defun texi-docstring-magic-splice-sep 93,3199
-(defconst texi-docstring-magic-munge-table103,3504
-(defun texi-docstring-magic-untabify 193,7271
-(defun texi-docstring-magic-munge-docstring 203,7586
-(defun texi-docstring-magic-texi 242,8873
-(defun texi-docstring-magic-format-default 255,9313
-(defun texi-docstring-magic-texi-for 271,9948
-(defconst texi-docstring-magic-comment329,11908
-(defun texi-docstring-magic 335,12062
-(defun texi-docstring-magic-face-at-point 369,13142
-(defun texi-docstring-magic-insert-magic 384,13665
+(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
 
 lib/unicode-chars.el,80
-(defvar unicode-chars-alist12,348
-(defun unicode-chars-list-chars 5050,245960
-
-lib/unicode-tokens.el,3137
-(defvar unicode-tokens-token-symbol-map 46,1575
-(defvar unicode-tokens-token-format 59,2004
-(defvar unicode-tokens-token-variant-format-regexp 65,2253
-(defvar unicode-tokens-fontsymb-properties 78,2730
-(defvar unicode-tokens-shortcut-alist 83,2964
-(defvar unicode-tokens-control-region-format-regexp 94,3230
-(defvar unicode-tokens-control-char-format-regexp 95,3287
-(defvar unicode-tokens-control-regions 96,3342
-(defvar unicode-tokens-control-characters 97,3386
-(defvar unicode-tokens-control-region-format-beg 99,3434
-(defvar unicode-tokens-control-region-format-end 100,3488
-(defvar unicode-tokens-control-char-format 101,3542
-(defconst unicode-tokens-configuration-variables107,3631
-(defvar unicode-tokens-token-list 125,4024
-(defvar unicode-tokens-hash-table 128,4144
-(defvar unicode-tokens-token-match-regexp 131,4260
-(defvar unicode-tokens-uchar-hash-table 134,4366
-(defvar unicode-tokens-uchar-regexp 138,4553
-(defgroup unicode-tokens-faces 148,4744
-(defface unicode-tokens-script-font-face152,4840
-(defface unicode-tokens-fraktur-font-face163,5138
-(defface unicode-tokens-serif-font-face174,5463
-(defconst unicode-tokens-font-lock-extra-managed-props 185,5756
-(defun unicode-tokens-font-lock-keywords 193,5928
-(defun unicode-tokens-usable-composition 233,7583
-(defun unicode-tokens-help-echo 244,7859
-(defvar unicode-tokens-show-symbols 248,8022
-(defun unicode-tokens-font-lock-compose-symbol 251,8136
-(defun unicode-tokens-show-symbols 268,8852
-(defun unicode-tokens-symbs-to-props 276,9153
-(defvar unicode-tokens-show-controls 294,9674
-(defun unicode-tokens-show-controls 297,9765
-(defun unicode-tokens-control-char 308,10250
-(defun unicode-tokens-control-region 313,10492
-(defun unicode-tokens-control-font-lock-keywords 319,10821
-(defvar unicode-tokens-use-shortcuts 330,11151
-(defun unicode-tokens-use-shortcuts 333,11254
-(defun unicode-tokens-map-ordering 351,11851
-(defun unicode-tokens-quail-define-rules 355,12001
-(defun unicode-tokens-insert-token 378,12680
-(defun unicode-tokens-annotate-region 388,12979
-(defun unicode-tokens-insert-control 411,13747
-(defun unicode-tokens-insert-uchar-as-token 417,13971
-(defun unicode-tokens-delete-token-at-point 424,14201
-(defvar unicode-tokens-rotate-token-last-token 429,14374
-(defun unicode-tokens-prev-token 431,14427
-(defun unicode-tokens-rotate-token-forward 439,14697
-(defun unicode-tokens-rotate-token-backward 464,15622
-(defun unicode-tokens-copy-token 469,15824
-(define-button-type 'unicode-tokens-listunicode-tokens-list
475,15999
-(defun unicode-tokens-list-tokens 482,16245
-(defun unicode-tokens-copy 503,16862
-(defun unicode-tokens-paste 530,18013
-(defun unicode-tokens-initialise 550,18517
-(defvar unicode-tokens-mode-map 557,18734
-(define-minor-mode unicode-tokens-mode561,18846
-(define-key unicode-tokens-mode-map 617,20799
-(define-key unicode-tokens-mode-map 619,20891
-(define-key unicode-tokens-mode-map 621,20982
-(define-key unicode-tokens-mode-map 623,21089
-(define-key unicode-tokens-mode-map 625,21199
-(define-key unicode-tokens-mode-map 627,21308
-(define-key unicode-tokens-mode-map 629,21415
+(defvar unicode-chars-alist12,349
+(defun unicode-chars-list-chars 5050,245961
+
+lib/unicode-tokens.el,3219
+(defvar unicode-tokens-token-symbol-map 46,1554
+(defvar unicode-tokens-token-format 59,1983
+(defvar unicode-tokens-token-variant-format-regexp 65,2232
+(defvar unicode-tokens-fontsymb-properties 78,2709
+(defvar unicode-tokens-shortcut-alist 83,2943
+(defvar unicode-tokens-control-region-format-regexp 94,3209
+(defvar unicode-tokens-control-char-format-regexp 95,3266
+(defvar unicode-tokens-control-regions 96,3321
+(defvar unicode-tokens-control-characters 97,3365
+(defvar unicode-tokens-control-char-format 98,3412
+(defconst unicode-tokens-configuration-variables104,3501
+(defvar unicode-tokens-token-list 120,3834
+(defvar unicode-tokens-hash-table 123,3954
+(defvar unicode-tokens-token-match-regexp 126,4070
+(defvar unicode-tokens-uchar-hash-table 129,4182
+(defvar unicode-tokens-uchar-regexp 133,4369
+(defgroup unicode-tokens-faces 143,4560
+(defface unicode-tokens-script-font-face147,4656
+(defface unicode-tokens-fraktur-font-face158,4954
+(defface unicode-tokens-serif-font-face169,5279
+(defface unicode-tokens-highlight-face180,5572
+(defconst unicode-tokens-font-lock-extra-managed-props 189,5934
+(defun unicode-tokens-font-lock-keywords 197,6106
+(defun unicode-tokens-usable-composition 237,7766
+(defun unicode-tokens-help-echo 248,8042
+(defvar unicode-tokens-show-symbols 252,8205
+(defun unicode-tokens-font-lock-compose-symbol 255,8319
+(defun unicode-tokens-show-symbols 272,9035
+(defun unicode-tokens-symbs-to-props 280,9336
+(defvar unicode-tokens-show-controls 298,9857
+(defun unicode-tokens-show-controls 301,9948
+(defun unicode-tokens-control-char 314,10524
+(defun unicode-tokens-control-region 319,10766
+(defun unicode-tokens-control-font-lock-keywords 325,11095
+(defvar unicode-tokens-use-shortcuts 336,11425
+(defun unicode-tokens-use-shortcuts 339,11528
+(defun unicode-tokens-map-ordering 357,12125
+(defun unicode-tokens-quail-define-rules 361,12275
+(defun unicode-tokens-insert-token 384,12954
+(defun unicode-tokens-annotate-region 393,13259
+(defun unicode-tokens-insert-control 416,14027
+(defun unicode-tokens-insert-uchar-as-token 425,14389
+(defun unicode-tokens-delete-token-at-point 432,14619
+(defun unicode-tokens-prev-token 439,14914
+(defun unicode-tokens-rotate-token-forward 447,15179
+(defun unicode-tokens-rotate-token-backward 474,16071
+(defun unicode-tokens-copy-token 479,16273
+(define-button-type 'unicode-tokens-listunicode-tokens-list
485,16448
+(defun unicode-tokens-list-tokens 491,16653
+(defun unicode-tokens-copy 514,17385
+(defun unicode-tokens-paste 541,18536
+(defvar unicode-tokens-highlight-unicode 556,19003
+(defconst unicode-tokens-unicode-highlight-patterns559,19095
+(defun unicode-tokens-highlight-unicode 563,19264
+(defun unicode-tokens-initialise 579,19709
+(defvar unicode-tokens-mode-map 587,19959
+(define-minor-mode unicode-tokens-mode590,20056
+(define-key unicode-tokens-mode-map 661,22479
+(define-key unicode-tokens-mode-map 663,22571
+(define-key unicode-tokens-mode-map 665,22662
+(define-key unicode-tokens-mode-map 667,22769
+(define-key unicode-tokens-mode-map 669,22879
+(define-key unicode-tokens-mode-map 671,22988
+(define-key unicode-tokens-mode-map 673,23095
+(defun unicode-tokens-define-menu 681,23224
 
 mmm/mmm-auto.el,343
-(defvar mmm-autoloaded-classes67,2675
-(defun mmm-autoload-class 89,3438
-(defvar mmm-changed-buffers-list 129,5005
-(defun mmm-major-mode-change 132,5112
-(defun mmm-check-changed-buffers 145,5633
-(defun mmm-mode-on-maybe 155,6006
-(defalias 'mmm-add-find-file-hooks mmm-add-find-file-hooks
167,6424
-(defun mmm-add-find-file-hook 168,6484
+(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
-(defun mmm-get-class-spec 42,1295
-(defun mmm-get-class-parameter 59,2008
-(defun mmm-set-class-parameter 63,2174
-(defun* mmm-apply-class75,2538
-(defun* mmm-apply-classes90,3176
-(defun* mmm-apply-all 110,3942
-(defun* mmm-ify124,4389
-(defun* mmm-match-region206,7472
-(defun mmm-match->point 267,10161
-(defun mmm-match-and-verify 281,10683
-(defun mmm-get-form 307,11741
-(defun mmm-default-get-form 318,12237
+(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
 
 mmm/mmm-cmds.el,712
-(defun mmm-ify-by-class 41,1209
-(defun mmm-ify-region 63,1933
-(defun mmm-ify-by-regexp75,2361
-(defun mmm-parse-buffer 97,3037
-(defun mmm-parse-region 106,3373
-(defun mmm-parse-block 115,3752
-(defun mmm-get-block 132,4503
-(defun mmm-reparse-current-region 146,4834
-(defun mmm-clear-current-region 167,5508
-(defun mmm-clear-regions 172,5672
-(defun mmm-clear-all-regions 177,5818
-(defun* mmm-end-current-region 185,5978
-(defun mmm-narrow-to-submode-region 220,7401
-(defun mmm-insert-region 239,8015
-(defun mmm-insert-by-key 258,8877
-(defun mmm-get-insertion-spec 342,12437
-(defun mmm-insertion-help 369,13516
-(defun mmm-display-insertion-key 379,13886
-(defun mmm-get-all-insertion-keys 401,14708
+(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
 
 mmm/mmm-compat.el,418
-(defvar mmm-xemacs 40,1312
-(defvar mmm-keywords-used49,1615
-(defmacro mmm-regexp-opt 91,2661
-(defvar mmm-evaporate-property110,3310
-(defmacro mmm-set-keymap-default 128,4076
-(defmacro mmm-event-key 137,4518
-(defvar skeleton-positions 146,4737
-(defun mmm-fixup-skeleton 147,4768
-(defmacro mmm-make-temp-buffer 159,5205
-(defvar mmm-font-lock-available-p 172,5601
-(defmacro mmm-set-font-lock-defaults 179,5815
+(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
 
 mmm/mmm-cweb.el,228
-(defvar mmm-cweb-section-tags38,1116
-(defvar mmm-cweb-section-regexp41,1163
-(defvar mmm-cweb-c-part-tags44,1253
-(defvar mmm-cweb-c-part-regexp47,1312
-(defun mmm-cweb-in-limbo 50,1396
-(defun mmm-cweb-verify-brief-c 57,1621
+(defvar mmm-cweb-section-tags38,1117
+(defvar mmm-cweb-section-regexp41,1164
+(defvar mmm-cweb-c-part-tags44,1254
+(defvar mmm-cweb-c-part-regexp47,1313
+(defun mmm-cweb-in-limbo 50,1397
+(defun mmm-cweb-verify-brief-c 57,1622
 
 mmm/mmm-mason.el,410
-(defvar mmm-mason-perl-tags41,1235
-(defvar mmm-mason-pseudo-perl-tags45,1376
-(defvar mmm-mason-non-perl-tags48,1452
-(defvar mmm-mason-perl-tags-regexp51,1553
-(defvar mmm-mason-pseudo-perl-tags-regexp56,1748
-(defvar mmm-mason-tag-names-regexp61,1965
-(defun mmm-mason-verify-inline 66,2185
-(defun mmm-mason-start-line 156,5089
-(defun mmm-mason-end-line 161,5154
-(defun mmm-mason-set-mode-line 168,5248
+(defvar mmm-mason-perl-tags41,1236
+(defvar mmm-mason-pseudo-perl-tags45,1377
+(defvar mmm-mason-non-perl-tags48,1453
+(defvar mmm-mason-perl-tags-regexp51,1554
+(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
 
 mmm/mmm-mode.el,1024
-(defun mmm-mode 101,3866
-(defun mmm-mode-on 140,5371
-(defun mmm-mode-off 181,7131
-(defvar mmm-mode-map 206,7864
-(defvar mmm-mode-prefix-map 209,7939
-(defvar mmm-mode-menu-map 212,8049
-(defun mmm-define-key 215,8140
-(define-key mmm-mode-prefix-map 239,8895
-(define-key mmm-mode-prefix-map 246,9153
-(define-key mmm-mode-map 249,9264
-(define-key mmm-mode-menu-map 252,9366
-(define-key mmm-mode-menu-map 254,9438
-(define-key mmm-mode-menu-map 256,9497
-(define-key mmm-mode-menu-map 258,9578
-(define-key mmm-mode-menu-map 260,9659
-(define-key mmm-mode-menu-map 262,9746
-(define-key mmm-mode-menu-map 265,9840
-(define-key mmm-mode-menu-map 267,9900
-(define-key mmm-mode-menu-map 270,9991
-(define-key mmm-mode-menu-map 272,10051
-(define-key mmm-mode-menu-map 274,10158
-(define-key mmm-mode-menu-map 276,10243
-(define-key mmm-mode-menu-map 279,10329
-(define-key mmm-mode-menu-map 281,10389
-(define-key mmm-mode-menu-map 283,10502
-(define-key mmm-mode-menu-map 285,10587
-(define-key mmm-mode-map 288,10670
+(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
@@ -2480,296 +2481,301 @@ mmm/mmm-noweb.el,1291
 (defun mmm-undo-syntax-other-regions 401,13237
 
 mmm/mmm-region.el,1643
-(defsubst mmm-overlay-at 54,1748
-(defun mmm-overlays-at 59,1933
-(defun mmm-included-p 72,2386
-(defun mmm-overlays-containing 112,3875
-(defun mmm-overlays-contained-in 125,4313
-(defun mmm-overlays-overlapping 138,4753
-(defun mmm-sort-overlays 149,5116
-(defvar mmm-current-overlay 158,5386
-(defvar mmm-previous-overlay 163,5601
-(defvar mmm-current-submode 168,5789
-(defvar mmm-previous-submode 173,5989
-(defun mmm-update-current-submode 178,6162
-(defun mmm-set-current-submode 199,6978
-(defun mmm-submode-at 210,7470
-(defun mmm-match-front 219,7745
-(defun mmm-match-back 238,8506
-(defun mmm-front-start 257,9251
-(defun mmm-back-end 265,9555
-(defun mmm-valid-submode-region 278,9902
-(defun* mmm-make-region305,11058
-(defun mmm-make-overlay 431,16429
-(defun mmm-get-face 459,17562
-(defun mmm-clear-overlays 470,17854
-(defun mmm-update-mode-info 486,18321
-(defun mmm-update-submode-region 571,22606
-(defun mmm-add-hooks 588,23364
-(defun mmm-remove-hooks 592,23499
-(defun mmm-get-local-variables-list 598,23626
-(defun mmm-get-locals 618,24546
-(defun mmm-get-saved-local 631,25127
-(defun mmm-set-local-variables 635,25292
-(defun mmm-get-saved-local-variables 646,25733
-(defun mmm-save-changed-local-variables 654,26050
-(defun mmm-clear-local-variables 673,26908
-(defun mmm-enable-font-lock 684,27187
-(defun mmm-update-font-lock-buffer 692,27447
-(defun mmm-refontify-maybe 705,27879
-(defun mmm-submode-changes-in 720,28401
-(defun mmm-regions-in 731,28849
-(defun mmm-regions-alist 745,29419
-(defun mmm-fontify-region 762,30065
-(defun mmm-fontify-region-list 782,31096
-(defun mmm-beginning-of-syntax 804,32012
+(defsubst mmm-overlay-at 54,1749
+(defun mmm-overlays-at 59,1934
+(defun mmm-included-p 72,2387
+(defun mmm-overlays-containing 112,3876
+(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
 
 mmm/mmm-rpm.el,154
-(defconst mmm-rpm-sh-start-tags48,1617
-(defvar mmm-rpm-sh-end-tags53,1841
-(defvar mmm-rpm-sh-start-regexp57,2015
-(defvar mmm-rpm-sh-end-regexp61,2193
+(defconst mmm-rpm-sh-start-tags48,1618
+(defvar mmm-rpm-sh-end-tags53,1842
+(defvar mmm-rpm-sh-start-regexp57,2016
+(defvar mmm-rpm-sh-end-regexp61,2194
 
 mmm/mmm-sample.el,168
-(defvar mmm-here-doc-mode-alist 84,2614
-(defun mmm-here-doc-get-mode 93,3099
-(defun mmm-file-variables-verify 208,6817
-(defun mmm-file-variables-find-back 232,7853
+(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
 
 mmm/mmm-univ.el,34
 (defun mmm-univ-get-mode 38,1205
 
 mmm/mmm-utils.el,282
-(defmacro mmm-valid-buffer 41,1309
-(defmacro mmm-save-all 60,1953
-(defun mmm-format-string 73,2242
-(defun mmm-format-matches 84,2694
-(defmacro mmm-save-keyword 107,3487
-(defmacro mmm-save-keywords 115,3814
-(defun mmm-looking-back-at 128,4347
-(defun mmm-make-marker 145,4915
+(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,3072
-(defvar mmm-c-derived-modes106,3182
-(defvar mmm-save-local-variables 110,3301
-(defvar mmm-buffer-saved-locals 336,10161
-(defvar mmm-region-saved-locals-defaults 341,10361
-(defvar mmm-region-saved-locals-for-dominant 347,10621
-(defgroup mmm-faces 357,10998
-(defcustom mmm-submode-decoration-level 363,11169
-(defface mmm-init-submode-face 381,12041
-(defface mmm-cleanup-submode-face 385,12181
-(defface mmm-declaration-submode-face 389,12318
-(defface mmm-comment-submode-face 393,12464
-(defface mmm-output-submode-face 397,12617
-(defface mmm-special-submode-face 401,12766
-(defface mmm-code-submode-face 405,12930
-(defface mmm-default-submode-face 409,13069
-(defface mmm-delimiter-face 414,13277
-(defcustom mmm-mode-string 421,13403
-(defcustom mmm-submode-mode-line-format 426,13534
-(defvar mmm-primary-mode-display-name 443,14189
-(defvar mmm-buffer-mode-display-name 448,14403
-(defun mmm-set-mode-line 454,14702
-(defvar mmm-classes 478,15510
-(defvar mmm-global-classes 484,15755
-(defcustom mmm-mode-ext-classes-alist 491,15937
-(defun mmm-add-mode-ext-class 510,16755
-(defcustom mmm-major-mode-preferences519,17080
-(defun mmm-add-to-major-mode-preferences 537,17878
-(defun mmm-ensure-modename 553,18664
-(defun mmm-modename->function 562,18974
-(defcustom mmm-delimiter-mode 576,19437
-(defcustom mmm-mode-prefix-key 586,19706
-(defcustom mmm-command-modifiers 591,19833
-(defcustom mmm-insert-modifiers 605,20466
-(defcustom mmm-use-old-command-keys 620,21144
-(defun mmm-use-old-command-keys 630,21608
-(defcustom mmm-mode-hook 638,21807
-(defun mmm-run-constructed-hook 658,22614
-(defun mmm-run-major-hook 666,23000
-(defun mmm-run-submode-hook 669,23077
-(defvar mmm-class-hooks-run 672,23164
-(defun mmm-run-class-hook 677,23336
-(defvar mmm-primary-mode-entry-hook 682,23508
-(defcustom mmm-major-mode-hook 697,24155
-(defun mmm-run-major-mode-hook 711,24786
-(defcustom mmm-global-mode 724,25327
-(defcustom mmm-never-modes740,26022
-(defvar mmm-set-file-name-for-modes 758,26322
-(defvar mmm-mode 769,26681
-(defvar mmm-primary-mode 777,26889
-(defvar mmm-classes-alist 788,27255
-(defun mmm-add-classes 943,35462
-(defun mmm-add-group 948,35627
-(defun mmm-add-to-group 958,36077
-(defconst mmm-version 972,36574
-(defun mmm-version 975,36639
-(defvar mmm-temp-buffer-name 982,36782
-(defvar mmm-interactive-history 988,36912
-(defun mmm-add-to-history 994,37181
-(defun mmm-clear-history 997,37264
-(defvar mmm-mode-ext-classes 1005,37449
-(defun mmm-get-mode-ext-classes 1010,37660
-(defun mmm-clear-mode-ext-classes 1019,38036
-(defun mmm-mode-ext-applies 1023,38161
-(defun mmm-get-all-classes 1037,38645
-
-doc/ProofGeneral.texi,5548
-@node Top166,5060
-@node Preface203,6165
-@node Latest news for version 3.7.1Latest news for version 3.7.1
226,6763
-@node Future269,8708
-@node Credits300,10007
-@node Introducing Proof GeneralIntroducing Proof General
406,13776
-@node Installing Proof GeneralInstalling Proof General
462,15818
-@node Quick start guideQuick start guide
476,16267
-@node Features of Proof GeneralFeatures of Proof General
520,18388
-@node Supported proof assistantsSupported proof assistants
609,22325
-@node Prerequisites for this manualPrerequisites for this manual
658,24245
-@node Organization of this manualOrganization of this manual
702,25871
-@node Basic Script ManagementBasic Script Management
728,26699
-@node Walkthrough example in IsabelleWalkthrough example in Isabelle
747,27299
-@node Proof scriptsProof scripts
998,36952
-@node Script buffersScript buffers
1041,39072
-@node Locked queue and editing regionsLocked queue and editing regions
1063,39649
-@node Goal-save sequencesGoal-save sequences
1119,41796
-@node Active scripting bufferActive scripting buffer
1156,43282
-@node Summary of Proof General buffersSummary of Proof General buffers
1225,46702
-@node Script editing commandsScript editing commands
1287,49376
-@node Script processing commandsScript processing commands
1365,52235
-@node Proof assistant commandsProof assistant commands
1493,57536
-@node Toolbar commandsToolbar commands
1659,63315
-@node Interrupting during trace outputInterrupting during trace output
1683,64244
-@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
1722,66168
-@node Goals buffer commandsGoals buffer commands
1736,66668
-@node Advanced Script Management and EditingAdvanced Script Management and Editing
1825,70232
-@node Visibility of completed proofsVisibility of completed proofs
1857,71444
-@node Switching between proof scriptsSwitching between proof scripts
1912,73367
-@node View of processed files View of processed files 
1949,75339
-@node Retracting across filesRetracting across files
2009,78390
-@node Asserting across filesAsserting across files
2022,79021
-@node Automatic multiple file handlingAutomatic multiple file handling
2035,79587
-@node Escaping script managementEscaping script management
2060,80621
-@node Editing featuresEditing features
2118,82824
-@node Experimental featuresExperimental features
2182,85496
-@node Support for other PackagesSupport for other Packages
2216,86760
-@node Syntax highlightingSyntax highlighting
2248,87634
-@node Unicode supportUnicode support
2277,88638
-@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)
2363,91749
-@node Support for outline modeSupport for outline mode
2422,93879
-@node Support for completionSupport for completion
2448,95009
-@node Support for tagsSupport for tags
2506,97185
-@node Customizing Proof GeneralCustomizing Proof General
2558,99514
-@node Basic optionsBasic options
2598,101184
-@node How to customizeHow to customize
2622,101942
-@node Display customizationDisplay customization
2673,104044
-@node User optionsUser options
2798,109282
-@node Changing facesChanging faces
3040,117873
-@node Tweaking configuration settingsTweaking configuration settings
3115,120542
-@node Hints and TipsHints and Tips
3172,123068
-@node Adding your own keybindingsAdding your own keybindings
3191,123669
-@node Using file variablesUsing file variables
3248,126268
-@node Using abbreviationsUsing abbreviations
3307,128454
-@node LEGO Proof GeneralLEGO Proof General
3346,129870
-@node LEGO specific commandsLEGO specific commands
3387,131239
-@node LEGO tagsLEGO tags
3407,131694
-@node LEGO customizationsLEGO customizations
3417,131941
-@node Coq Proof GeneralCoq Proof General
3449,132860
-@node Coq-specific commandsCoq-specific commands
3465,133269
-@node Coq-specific variablesCoq-specific variables
3487,133776
-@node Editing multiple proofsEditing multiple proofs
3509,134434
-@node User-loaded tacticsUser-loaded tactics
3533,135542
-@node Holes featureHoles feature
3597,138016
-@node Isabelle Proof GeneralIsabelle Proof General
3624,139303
-@node Choosing logic and starting isabelleChoosing logic and starting isabelle
3655,140472
-@node Isabelle commandsIsabelle commands
3730,143521
-@node Isabelle settingsIsabelle settings
3873,147674
-@node Isabelle customizationsIsabelle customizations
3887,148256
-@node HOL Proof GeneralHOL Proof General
3910,148743
-@node Shell Proof GeneralShell Proof General
3952,150565
-@node Obtaining and InstallingObtaining and Installing
3988,152024
-@node Obtaining Proof GeneralObtaining Proof General
4004,152437
-@node Installing Proof General from tarballInstalling Proof General from tarball
4035,153676
-@node Installing Proof General from RPM packageInstalling Proof General from RPM package
4060,154508
-@node Setting the names of binariesSetting the names of binaries
4075,154916
-@node Notes for syssiesNotes for syssies
4103,155856
-@node Bugs and EnhancementsBugs and Enhancements
4178,158892
-@node References4199,159707
-@node History of Proof GeneralHistory of Proof General
4239,160730
-@node Old News for 3.0Old News for 3.0
4330,164832
-@node Old News for 3.1Old News for 3.1
4400,168526
-@node Old News for 3.2Old News for 3.2
4426,169698
-@node Old News for 3.3Old News for 3.3
4487,172701
-@node Old News for 3.4Old News for 3.4
4506,173598
-@node Function IndexFunction Index
4529,174654
-@node Variable IndexVariable Index
4533,174730
-@node Keystroke IndexKeystroke Index
4537,174810
-@node Concept IndexConcept Index
4541,174876
+(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
+
+doc/ProofGeneral.texi,5684
+@node Top164,4911
+@node Preface201,6018
+@node News for Version 4.0News for Version 4.0
224,6607
+@node Future248,7368
+@node Credits279,8667
+@node Introducing Proof GeneralIntroducing Proof General
385,12436
+@node Installing Proof GeneralInstalling Proof General
440,14414
+@node Quick start guideQuick start guide
454,14863
+@node Features of Proof GeneralFeatures of Proof General
498,16984
+@node Supported proof assistantsSupported proof assistants
587,20921
+@node Prerequisites for this manualPrerequisites for this manual
636,22841
+@node Organization of this manualOrganization of this manual
680,24460
+@node Basic Script ManagementBasic Script Management
706,25288
+@node Walkthrough example in IsabelleWalkthrough example in Isabelle
725,25888
+@node Proof scriptsProof scripts
979,35666
+@node Script buffersScript buffers
1022,37786
+@node Locked queue and editing regionsLocked queue and editing regions
1044,38363
+@node Goal-save sequencesGoal-save sequences
1100,40510
+@node Active scripting bufferActive scripting buffer
1137,41996
+@node Summary of Proof General buffersSummary of Proof General buffers
1206,45416
+@node Script editing commandsScript editing commands
1268,48090
+@node Script processing commandsScript processing commands
1346,50949
+@node Proof assistant commandsProof assistant commands
1474,56249
+@node Toolbar commandsToolbar commands
1640,62028
+@node Interrupting during trace outputInterrupting during trace output
1664,62957
+@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
1703,64881
+@node Goals buffer commandsGoals buffer commands
1717,65381
+@node Advanced Script Management and EditingAdvanced Script Management and Editing
1806,68945
+@node Visibility of completed proofsVisibility of completed proofs
1838,70157
+@node Switching between proof scriptsSwitching between proof scripts
1893,72080
+@node View of processed files View of processed files 
1930,74052
+@node Retracting across filesRetracting across files
1990,77103
+@node Asserting across filesAsserting across files
2003,77734
+@node Automatic multiple file handlingAutomatic multiple file handling
2016,78300
+@node Escaping script managementEscaping script management
2041,79334
+@node Editing featuresEditing features
2099,81537
+@node Experimental featuresExperimental features
2163,84209
+@node Support for other PackagesSupport for other Packages
2197,85473
+@node Syntax highlightingSyntax highlighting
2229,86347
+@node Unicode supportUnicode support
2258,87351
+@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)
2344,90462
+@node Support for outline modeSupport for outline mode
2399,92506
+@node Support for completionSupport for completion
2424,93635
+@node Support for tagsSupport for tags
2481,95796
+@node Customizing Proof GeneralCustomizing Proof General
2533,98124
+@node Basic optionsBasic options
2573,99794
+@node How to customizeHow to customize
2597,100552
+@node Display customizationDisplay customization
2644,102519
+@node User optionsUser options
2769,107757
+@node Changing facesChanging faces
3011,116348
+@node Tweaking configuration settingsTweaking configuration settings
3086,119017
+@node Hints and TipsHints and Tips
3143,121543
+@node Adding your own keybindingsAdding your own keybindings
3162,122144
+@node Using file variablesUsing file variables
3219,124715
+@node Using abbreviationsUsing abbreviations
3278,126901
+@node LEGO Proof GeneralLEGO Proof General
3317,128316
+@node LEGO specific commandsLEGO specific commands
3358,129685
+@node LEGO tagsLEGO tags
3378,130140
+@node LEGO customizationsLEGO customizations
3388,130387
+@node Coq Proof GeneralCoq Proof General
3420,131306
+@node Coq-specific commandsCoq-specific commands
3436,131715
+@node Coq-specific variablesCoq-specific variables
3458,132222
+@node Editing multiple proofsEditing multiple proofs
3480,132880
+@node User-loaded tacticsUser-loaded tactics
3504,133988
+@node Holes featureHoles feature
3568,136462
+@node Isabelle Proof GeneralIsabelle Proof General
3595,137749
+@node Choosing logic and starting isabelleChoosing logic and starting isabelle
3626,138918
+@node Isabelle commandsIsabelle commands
3701,141967
+@node Isabelle settingsIsabelle settings
3844,146120
+@node Isabelle customizationsIsabelle customizations
3858,146702
+@node HOL Proof GeneralHOL Proof General
3881,147189
+@node Shell Proof GeneralShell Proof General
3923,149011
+@node Obtaining and InstallingObtaining and Installing
3959,150470
+@node Obtaining Proof GeneralObtaining Proof General
3975,150883
+@node Installing Proof General from tarballInstalling Proof General from tarball
4006,152122
+@node Installing Proof General from RPM packageInstalling Proof General from RPM package
4031,152954
+@node Setting the names of binariesSetting the names of binaries
4046,153362
+@node Notes for syssiesNotes for syssies
4074,154302
+@node Bugs and EnhancementsBugs and Enhancements
4149,157338
+@node References4170,158153
+@node History of Proof GeneralHistory of Proof General
4210,159176
+@node Old News for 3.0Old News for 3.0
4304,163341
+@node Old News for 3.1Old News for 3.1
4374,167035
+@node Old News for 3.2Old News for 3.2
4400,168207
+@node Old News for 3.3Old News for 3.3
4461,171210
+@node Old News for 3.4Old News for 3.4
4480,172107
+@node Old News for 3.5Old News for 3.5
4502,173162
+@node Old News for 3.6Old News for 3.6
4506,173219
+@node Old News for 3.7Old News for 3.7
4511,173319
+@node Function IndexFunction Index
4555,175217
+@node Variable IndexVariable Index
4559,175293
+@node Keystroke IndexKeystroke Index
4563,175373
+@node Concept IndexConcept Index
4567,175439
 
 doc/PG-adapting.texi,3772
-@node Top156,4734
-@node Introduction194,5877
-@node Future235,7530
-@node Credits271,9126
-@node Beginning with a New ProverBeginning with a New Prover
281,9418
-@node Overview of adding a new proverOverview of adding a new prover
322,11367
-@node Demonstration instance and easy configurationDemonstration instance and easy configuration
400,14675
-@node Major modes used by Proof GeneralMajor modes used by Proof General
469,18066
-@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands
502,19417
-@node Settings for generic user-level commandsSettings for generic user-level commands
517,19963
-@node Menu configurationMenu configuration
562,21697
-@node Toolbar configurationToolbar configuration
586,22614
-@node Proof Script SettingsProof Script Settings
644,24863
-@node Recognizing commands and commentsRecognizing commands and comments
666,25443
-@node Recognizing proofsRecognizing proofs
787,30964
-@node Recognizing other elementsRecognizing other elements
896,35645
-@node Configuring undo behaviourConfiguring undo behaviour
1022,41184
-@node Nested proofsNested proofs
1159,46592
-@node Safe (state-preserving) commandsSafe (state-preserving) commands
1199,48218
-@node Activate scripting hookActivate scripting hook
1222,49171
-@node Automatic multiple filesAutomatic multiple files
1246,50041
-@node Completions1268,50888
-@node Proof Shell SettingsProof Shell Settings
1309,52377
-@node Proof shell commandsProof shell commands
1340,53659
-@node Script input to the shellScript input to the shell
1504,60703
-@node Settings for matching various output from proof processSettings for matching various output from proof process
1569,63661
-@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process
1700,69445
-@node Hooks and other settingsHooks and other settings
1915,79322
-@node Goals Buffer SettingsGoals Buffer Settings
1996,82704
-@node Splash Screen SettingsSplash Screen Settings
2073,85811
-@node Global ConstantsGlobal Constants
2099,86569
-@node Handling Multiple FilesHandling Multiple Files
2125,87410
-@node Configuring Editing SyntaxConfiguring Editing Syntax
2277,95193
-@node Configuring Font LockConfiguring Font Lock
2336,97314
-@node Configuring TokensConfiguring Tokens
2408,100669
-@node Writing More Lisp CodeWriting More Lisp Code
2450,102342
-@node Default values for generic settingsDefault values for generic settings
2467,102987
-@node Adding prover-specific configurationsAdding prover-specific configurations
2497,104070
-@node Useful variablesUseful variables
2540,105352
-@node Useful functions and macrosUseful functions and macros
2555,105851
-@node Internals of Proof GeneralInternals of Proof General
2658,109806
-@node Spans2686,110714
-@node Proof General site configurationProof General site configuration
2699,111088
-@node Configuration variable mechanismsConfiguration variable mechanisms
2779,114134
-@node Global variablesGlobal variables
2900,119578
-@node Proof script modeProof script mode
2970,122126
-@node Proof shell modeProof shell mode
3229,133781
-@node Debugging3636,149863
-@node Plans and IdeasPlans and Ideas
3679,150739
-@node Proof by pointing and similar featuresProof by pointing and similar features
3700,151461
-@node Granularity of atomic command sequencesGranularity of atomic command sequences
3738,153119
-@node Browser mode for script files and theoriesBrowser mode for script files and theories
3783,155344
-@node Demonstration InstantiationsDemonstration Instantiations
3813,156375
-@node demoisa-easy.el3829,156806
-@node demoisa.el3892,159048
-@node Function IndexFunction Index
4047,164036
-@node Variable IndexVariable Index
4051,164112
-@node Concept IndexConcept Index
4060,164291
+@node Top155,4691
+@node Introduction192,5800
+@node Future233,7453
+@node Credits269,9049
+@node Beginning with a New ProverBeginning with a New Prover
279,9341
+@node Overview of adding a new proverOverview of adding a new prover
320,11290
+@node Demonstration instance and easy configurationDemonstration instance and easy configuration
398,14598
+@node Major modes used by Proof GeneralMajor modes used by Proof General
467,17989
+@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands
500,19340
+@node Settings for generic user-level commandsSettings for generic user-level commands
515,19886
+@node Menu configurationMenu configuration
560,21620
+@node Toolbar configurationToolbar configuration
584,22537
+@node Proof Script SettingsProof Script Settings
642,24786
+@node Recognizing commands and commentsRecognizing commands and comments
664,25366
+@node Recognizing proofsRecognizing proofs
785,30887
+@node Recognizing other elementsRecognizing other elements
894,35568
+@node Configuring undo behaviourConfiguring undo behaviour
1020,41107
+@node Nested proofsNested proofs
1157,46515
+@node Safe (state-preserving) commandsSafe (state-preserving) commands
1197,48141
+@node Activate scripting hookActivate scripting hook
1220,49094
+@node Automatic multiple filesAutomatic multiple files
1244,49964
+@node Completions1266,50811
+@node Proof Shell SettingsProof Shell Settings
1307,52300
+@node Proof shell commandsProof shell commands
1338,53582
+@node Script input to the shellScript input to the shell
1502,60626
+@node Settings for matching various output from proof processSettings for matching various output from proof process
1567,63584
+@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process
1698,69368
+@node Hooks and other settingsHooks and other settings
1913,79245
+@node Goals Buffer SettingsGoals Buffer Settings
1994,82627
+@node Splash Screen SettingsSplash Screen Settings
2071,85734
+@node Global ConstantsGlobal Constants
2097,86492
+@node Handling Multiple FilesHandling Multiple Files
2123,87333
+@node Configuring Editing SyntaxConfiguring Editing Syntax
2275,95116
+@node Configuring Font LockConfiguring Font Lock
2334,97237
+@node Configuring TokensConfiguring Tokens
2406,100592
+@node Writing More Lisp CodeWriting More Lisp Code
2444,102093
+@node Default values for generic settingsDefault values for generic settings
2461,102738
+@node Adding prover-specific configurationsAdding prover-specific configurations
2491,103821
+@node Useful variablesUseful variables
2534,105103
+@node Useful functions and macrosUseful functions and macros
2549,105602
+@node Internals of Proof GeneralInternals of Proof General
2652,109557
+@node Spans2680,110465
+@node Proof General site configurationProof General site configuration
2692,110787
+@node Configuration variable mechanismsConfiguration variable mechanisms
2772,113833
+@node Global variablesGlobal variables
2893,119277
+@node Proof script modeProof script mode
2963,121825
+@node Proof shell modeProof shell mode
3222,133480
+@node Debugging3629,149562
+@node Plans and IdeasPlans and Ideas
3672,150438
+@node Proof by pointing and similar featuresProof by pointing and similar features
3693,151160
+@node Granularity of atomic command sequencesGranularity of atomic command sequences
3731,152818
+@node Browser mode for script files and theoriesBrowser mode for script files and theories
3776,155043
+@node Demonstration InstantiationsDemonstration Instantiations
3806,156074
+@node demoisa-easy.el3822,156505
+@node demoisa.el3885,158744
+@node Function IndexFunction Index
4040,163729
+@node Variable IndexVariable Index
4044,163805
+@node Concept IndexConcept Index
4053,163984
 
 generic/proof.el,0
 
+generic/proof-autoloads.el,0
+
 pgshell/pgshell.el,0
 
 isar/isar-autotest.el,0