Merge changes from Version4Branch.

1 files changed, 1755 insertions, 2721 deletions

diff --git a/TAGS b/TAGS
index 52baa9f3..06951ed1 100644
--- a/TAGS
+++ b/TAGS
@@ -30,171 +30,173 @@ coq/coq-db.el,559
 (defface coq-solve-tactics-face 221,8256
 (defconst coq-solve-tactics-face 229,8518
 
-coq/coq.el,6441
-(defcustom coq-translate-to-v8 45,1301
-(defun coq-build-prog-args 51,1481
-(defcustom coq-compile-file-command 64,1861
-(defcustom coq-default-undo-limit 74,2230
-(defconst coq-shell-init-cmd 79,2358
-(defcustom coq-prog-env 96,2958
-(defconst coq-shell-restart-cmd 104,3210
-(defvar coq-shell-prompt-pattern 111,3470
-(defvar coq-shell-cd 119,3799
-(defvar coq-shell-abort-goal-regexp 123,3954
-(defvar coq-shell-proof-completed-regexp 126,4080
-(defvar coq-goal-regexp129,4232
-(defun coq-library-directory 138,4421
-(defcustom coq-tags 145,4601
-(defconst coq-interrupt-regexp 150,4751
-(defcustom coq-www-home-page 155,4872
-(defvar coq-outline-regexp165,5043
-(defvar coq-outline-heading-end-regexp 172,5257
-(defvar coq-shell-outline-regexp 174,5311
-(defvar coq-shell-outline-heading-end-regexp 175,5361
-(defconst coq-kill-goal-command 180,5471
-(defconst coq-forget-id-command 181,5514
-(defconst coq-back-n-command 182,5561
-(defconst coq-state-preserving-tactics-regexp 186,5705
-(defconst coq-state-changing-commands-regexp188,5806
-(defconst coq-state-preserving-commands-regexp 190,5913
-(defconst coq-commands-regexp 192,6025
-(defvar coq-retractable-instruct-regexp 194,6103
-(defvar coq-non-retractable-instruct-regexp 196,6194
-(defvar coq-keywords-section200,6334
-(defvar coq-section-regexp 203,6428
-(defun coq-set-undo-limit 240,7574
-(defconst coq-keywords-decl-defn-regexp251,8013
-(defun coq-proof-mode-p 255,8163
-(defun coq-is-comment-or-proverprocp 266,8571
-(defun coq-is-goalsave-p 268,8675
-(defun coq-is-module-equal-p 269,8750
-(defun coq-is-def-p 272,8946
-(defun coq-is-decl-defn-p 274,9054
-(defun coq-state-preserving-command-p 279,9221
-(defun coq-command-p 282,9355
-(defun coq-state-preserving-tactic-p 285,9455
-(defun coq-state-changing-tactic-p 290,9603
-(defun coq-state-changing-command-p 297,9837
-(defun coq-section-or-module-start-p 304,10183
-(defun build-list-id-from-string 313,10424
-(defun coq-last-prompt-info 326,10954
-(defun coq-last-prompt-info-safe 338,11495
-(defvar coq-last-but-one-statenum 344,11752
-(defvar coq-last-but-one-proofnum 350,12050
-(defvar coq-last-but-one-proofstack 353,12148
-(defun coq-get-span-statenum 356,12258
-(defun coq-get-span-proofnum 361,12373
-(defun coq-get-span-proofstack 366,12488
-(defun coq-set-span-statenum 371,12632
-(defun coq-get-span-goalcmd 376,12763
-(defun coq-set-span-goalcmd 381,12877
-(defun coq-set-span-proofnum 386,13007
-(defun coq-set-span-proofstack 391,13138
-(defun proof-last-locked-span 396,13298
-(defun coq-set-state-infos 411,13902
-(defun count-not-intersection 451,15981
-(defun  coq-find-and-forget-v81 482,17235
-(defun coq-find-and-forget-v80 510,18367
-(defun coq-find-and-forget 605,23066
-(defvar coq-current-goal 618,23606
-(defun coq-goal-hyp 621,23671
-(defun coq-state-preserving-p 634,24104
-(defconst notation-print-kinds-table 648,24609
-(defun coq-PrintScope 652,24777
-(defun coq-guess-or-ask-for-string 671,25333
-(defun coq-ask-do 682,25720
-(defun coq-SearchIsos 691,26108
-(defun coq-SearchConstant 697,26341
-(defun coq-SearchRewrite 701,26434
-(defun coq-SearchAbout 705,26532
-(defun coq-Print 709,26624
-(defun coq-About 713,26746
-(defun coq-LocateConstant 717,26863
-(defun coq-LocateLibrary 723,26998
-(defun coq-addquotes 729,27148
-(defun coq-LocateNotation 731,27196
-(defun coq-Pwd 738,27395
-(defun coq-Inspect 744,27527
-(defun coq-PrintSection(748,27627
-(defun coq-Print-implicit 752,27720
-(defun coq-Check 757,27871
-(defun coq-Show 762,27979
-(defun coq-Compile 776,28422
-(defun coq-guess-command-line 790,28742
-(defun coq-mode-config 820,30152
-(defvar coq-last-hybrid-pre-string 932,34258
-(defun coq-hybrid-ouput-goals-response-p 935,34437
-(defun coq-hybrid-ouput-goals-response 941,34695
-(defun coq-shell-mode-config 962,35655
-(defun coq-goals-mode-config 1006,37726
-(defun coq-response-config 1013,37958
-(defpacustom print-fully-explicit 1036,38667
-(defpacustom print-implicit 1041,38816
-(defpacustom print-coercions 1046,38983
-(defpacustom print-match-wildcards 1051,39128
-(defpacustom print-elim-types 1056,39309
-(defpacustom printing-depth 1061,39476
-(defpacustom undo-depth 1066,39638
-(defpacustom time-commands 1071,39786
-(defpacustom auto-compile-vos 1075,39897
-(defun coq-maybe-compile-buffer 1104,41013
-(defun coq-ancestors-of 1141,42547
-(defun coq-all-ancestors-of 1164,43514
-(defconst coq-require-command-regexp 1176,43907
-(defun coq-process-require-command 1181,44116
-(defun coq-included-children 1186,44243
-(defun coq-process-file 1207,45082
-(defun coq-preprocessing 1222,45621
-(defun coq-fake-constant-markup 1237,46040
-(defun coq-create-span-menu 1258,46846
-(defconst module-kinds-table 1275,47345
-(defconst modtype-kinds-table1279,47495
-(defun coq-insert-section-or-module 1283,47624
-(defconst reqkinds-kinds-table1306,48484
-(defun coq-insert-requires 1311,48629
-(defun coq-end-Section 1327,49135
-(defun coq-insert-intros 1345,49719
-(defun coq-insert-infoH-hook 1358,50244
-(defun coq-insert-as 1362,50322
-(defun coq-insert-match 1383,51071
-(defun coq-insert-tactic 1415,52249
-(defun coq-insert-tactical 1421,52488
-(defun coq-insert-command 1427,52737
-(defun coq-insert-term 1433,52981
-(define-key coq-keymap 1439,53178
-(define-key coq-keymap 1440,53236
-(define-key coq-keymap 1441,53293
-(define-key coq-keymap 1442,53362
-(define-key coq-keymap 1443,53418
-(define-key coq-keymap 1444,53467
-(define-key coq-keymap 1445,53525
-(define-key coq-keymap 1447,53586
-(define-key coq-keymap 1448,53645
-(define-key coq-keymap 1450,53709
-(define-key coq-keymap 1451,53769
-(define-key coq-keymap 1453,53825
-(define-key coq-keymap 1454,53875
-(define-key coq-keymap 1455,53925
-(define-key coq-keymap 1456,53975
-(define-key coq-keymap 1457,54029
-(define-key coq-keymap 1458,54088
-(defvar last-coq-error-location 1466,54219
-(defun coq-get-last-error-location 1475,54618
-(defun coq-highlight-error 1508,56014
-(defvar coq-allow-highlight-error 1574,58694
-(defun coq-decide-highlight-error 1580,58960
-(defun coq-highlight-error-hook 1585,59122
-(defun first-word-of-buffer 1596,59515
-(defun coq-show-first-goal 1606,59747
-(defvar coq-modeline-string2 1623,60442
-(defvar coq-modeline-string1 1624,60486
-(defvar coq-modeline-string0 1625,60529
-(defun coq-build-subgoals-string 1626,60574
-(defun coq-update-minor-mode-alist 1631,60742
-(defun is-not-split-vertic 1657,61810
-(defun optim-resp-windows 1666,62249
-
-coq/coq-indent.el,2259
+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
+
+coq/coq-indent.el,2222
 (defconst coq-any-command-regexp17,315
 (defconst coq-indent-inner-regexp20,406
 (defconst coq-comment-start-regexp 31,794
@@ -218,35 +220,34 @@ coq/coq-indent.el,2259
 (defun coq-looking-at-comment 137,5452
 (defun coq-find-comment-start 141,5593
 (defun coq-find-comment-end 152,6026
-(defun coq-looking-at-syntactic-context 165,6572
-(defconst coq-end-command-or-comment-regexp171,6794
-(defconst coq-end-command-or-comment-start-regexp174,6903
-(defun coq-find-not-in-comment-backward 178,7021
-(defun coq-find-not-in-comment-forward 198,7922
-(defun coq-find-command-end-backward 222,9064
-(defun coq-find-command-end-forward 231,9455
-(defun coq-find-command-end 240,9832
-(defun coq-parse-function 249,10215
-(defun coq-find-current-start 258,10417
-(defun coq-find-real-start 267,10708
-(defun coq-command-at-point 274,10927
-(defun coq-indent-only-spaces-on-line 281,11204
-(defun coq-indent-find-reg 287,11481
-(defun coq-find-no-syntactic-on-line 301,12017
-(defun coq-back-to-indentation-prevline 314,12490
-(defun coq-find-unclosed 358,14404
-(defun coq-find-at-same-level-zero 388,15705
-(defun coq-find-unopened 416,16870
-(defun coq-find-last-unopened 459,18320
-(defun coq-end-offset 470,18717
-(defun coq-indent-command-offset 495,19508
-(defun coq-indent-expr-offset 542,21332
-(defun coq-indent-comment-offset 658,26035
-(defun coq-indent-offset 690,27493
-(defun coq-indent-calculate 708,28356
-(defun coq-indent-line 711,28444
-(defun coq-indent-line-not-comments 721,28810
-(defun coq-indent-region 731,29199
+(defun coq-looking-at-syntactic-context 164,6519
+(defconst coq-end-command-or-comment-regexp170,6741
+(defconst coq-end-command-or-comment-start-regexp173,6850
+(defun coq-find-not-in-comment-backward 177,6968
+(defun coq-find-not-in-comment-forward 197,7869
+(defun coq-find-command-end-backward 221,9011
+(defun coq-find-command-end-forward 230,9402
+(defun coq-find-command-end 239,9779
+(defun coq-find-current-start 247,10111
+(defun coq-find-real-start 256,10402
+(defun coq-command-at-point 263,10621
+(defun coq-indent-only-spaces-on-line 270,10898
+(defun coq-indent-find-reg 276,11175
+(defun coq-find-no-syntactic-on-line 290,11711
+(defun coq-back-to-indentation-prevline 303,12184
+(defun coq-find-unclosed 347,14098
+(defun coq-find-at-same-level-zero 377,15399
+(defun coq-find-unopened 405,16564
+(defun coq-find-last-unopened 448,18014
+(defun coq-end-offset 459,18411
+(defun coq-indent-command-offset 484,19202
+(defun coq-indent-expr-offset 531,21026
+(defun coq-indent-comment-offset 647,25729
+(defun coq-indent-offset 679,27187
+(defun coq-indent-calculate 697,28050
+(defun coq-indent-line 700,28138
+(defun coq-indent-line-not-comments 710,28504
+(defun coq-indent-region 720,28893
 
 coq/coq-local-vars.el,280
 (defconst coq-local-vars-doc 17,306
@@ -263,68 +264,68 @@ coq/coq-syntax.el,2666
 (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 97,4169
-(defcustom coq-user-commands-db 114,4682
-(defcustom coq-user-tacticals-db 130,5201
-(defcustom coq-user-solve-tactics-db 146,5722
-(defcustom coq-user-reserved-db 164,6243
-(defvar coq-tactics-db182,6774
-(defvar coq-solve-tactics-db337,14842
-(defvar coq-tacticals-db361,15689
-(defvar coq-decl-db385,16576
-(defvar coq-defn-db407,17794
-(defvar coq-goal-starters-db460,21780
-(defvar coq-other-commands-db487,23335
-(defvar coq-commands-db611,32532
-(defvar coq-terms-db618,32758
-(defun coq-count-match 682,35410
-(defun coq-goal-command-str-v80-p 701,36273
-(defun coq-module-opening-p 724,37146
-(defun coq-section-command-p 735,37562
-(defun coq-goal-command-str-v81-p 739,37659
-(defun coq-goal-command-p-v81 754,38328
-(defun coq-goal-command-str-p 764,38668
-(defun coq-goal-command-p 774,39034
-(defvar coq-keywords-save-strict782,39346
-(defvar coq-keywords-save791,39459
-(defun coq-save-command-p 795,39537
-(defvar coq-keywords-kill-goal 804,39831
-(defvar coq-keywords-state-changing-misc-commands808,39922
-(defvar coq-keywords-goal811,40047
-(defvar coq-keywords-decl814,40130
-(defvar coq-keywords-defn817,40204
-(defvar coq-keywords-state-changing-commands821,40279
-(defvar coq-keywords-state-preserving-commands830,40540
-(defvar coq-keywords-commands835,40756
-(defvar coq-solve-tactics840,40905
-(defvar coq-tacticals844,41026
-(defvar coq-reserved850,41165
-(defvar coq-state-changing-tactics861,41494
-(defvar coq-state-preserving-tactics864,41603
-(defvar coq-tactics868,41717
-(defvar coq-retractable-instruct871,41806
-(defvar coq-non-retractable-instruct874,41916
-(defvar coq-keywords878,42044
-(defvar coq-symbols885,42212
-(defvar coq-error-regexp 904,42425
-(defvar coq-id 907,42653
-(defvar coq-id-shy 908,42678
-(defvar coq-ids 910,42732
-(defun coq-first-abstr-regexp 912,42773
-(defcustom coq-variable-highlight-enable 915,42868
-(defvar coq-font-lock-terms921,42995
-(defconst coq-save-command-regexp-strict942,43995
-(defconst coq-save-command-regexp946,44162
-(defconst coq-save-with-hole-regexp950,44315
-(defconst coq-goal-command-regexp954,44474
-(defconst coq-goal-with-hole-regexp957,44574
-(defconst coq-decl-with-hole-regexp961,44707
-(defconst coq-defn-with-hole-regexp968,44956
-(defconst coq-with-with-hole-regexp978,45245
-(defvar coq-font-lock-keywords-1984,45538
-(defvar coq-font-lock-keywords 1010,46859
-(defun coq-init-syntax-table 1012,46917
-(defconst coq-generic-expression1041,47816
+(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
 
 coq/coq-unicode-tokens.el,290
 (defconst coq-token-format 18,631
@@ -336,45 +337,6 @@ coq/coq-unicode-tokens.el,290
 (defcustom coq-token-name-alist 25,827
 (defcustom coq-shortcut-alist44,1557
 
-coq/x-symbol-coq.el,1748
-(defvar x-symbol-coq-required-fonts 19,510
-(defvar x-symbol-coq-name 27,911
-(defvar x-symbol-coq-modeline-name 28,951
-(defcustom x-symbol-coq-header-groups-alist 30,994
-(defcustom x-symbol-coq-electric-ignore 37,1212
-(defvar x-symbol-coq-required-fonts 44,1457
-(defvar x-symbol-coq-extra-menu-items 47,1556
-(defvar x-symbol-coq-token-grammar51,1644
-(defun x-symbol-coq-default-token-list 67,2310
-(defvar x-symbol-coq-user-table 79,2598
-(defvar x-symbol-coq-generated-data 82,2704
-(defvar x-symbol-coq-master-directory 90,2942
-(defvar x-symbol-coq-image-searchpath 91,2990
-(defvar x-symbol-coq-image-cached-dirs 92,3037
-(defvar x-symbol-coq-image-file-truename-alist 93,3102
-(defvar x-symbol-coq-image-keywords 94,3154
-(defcustom x-symbol-coq-subscript-matcher 101,3382
-(defcustom x-symbol-coq-font-lock-regexp 107,3614
-(defcustom x-symbol-coq-font-lock-limit-regexp 112,3786
-(defcustom x-symbol-coq-font-lock-contents-regexp 118,3974
-(defcustom x-symbol-coq-single-char-regexp 125,4228
-(defun x-symbol-coq-subscript-matcher 130,4376
-(defun coq-match-subscript 165,6065
-(defvar x-symbol-coq-font-lock-allowed-faces 172,6231
-(defcustom x-symbol-coq-class-alist177,6456
-(defcustom x-symbol-coq-class-face-alist 188,6834
-(defvar x-symbol-coq-font-lock-keywords 198,7144
-(defvar x-symbol-coq-font-lock-allowed-faces 200,7190
-(defvar x-symbol-coq-case-insensitive 206,7414
-(defvar x-symbol-coq-token-shape 207,7457
-(defvar x-symbol-coq-input-token-ignore 208,7495
-(defvar x-symbol-coq-token-list 209,7540
-(defvar x-symbol-coq-symbol-table 211,7584
-(defvar x-symbol-coq-xsymbol-table 315,10006
-(defun x-symbol-coq-prepare-table 462,13874
-(defvar x-symbol-coq-table471,14141
-(defcustom x-symbol-coq-auto-style478,14302
-
 demoisa/demoisa.el,349
 (defcustom isabelledemo-prog-name 54,1809
 (defcustom isabelledemo-web-page59,1931
@@ -385,73 +347,70 @@ demoisa/demoisa.el,349
 (define-derived-mode demoisa-response-mode 127,4196
 (define-derived-mode demoisa-goals-mode 131,4323
 
-isar/isabelle-system.el,1512
+isar/isabelle-system.el,1347
 (defgroup isabelle 26,775
 (defcustom isabelle-web-page30,903
-(defcustom isa-isatool-command41,1198
-(defvar isatool-not-found 59,1857
-(defun isa-set-isatool-command 62,1970
-(defun isa-shell-command-to-string 85,2914
-(defun isa-getenv 91,3138
-(defcustom isabelle-program-name-override 111,3825
-(defvar isabelle-prog-name 128,4409
-(defun isa-tool-list-logics 131,4519
-(defcustom isabelle-logics-available 138,4756
-(defcustom isabelle-chosen-logic 148,5092
-(defvar isabelle-chosen-logic-prev 163,5617
-(defun isabelle-hack-local-variables-function 166,5739
-(defun isabelle-set-prog-name 178,6180
-(defun isabelle-choose-logic 203,7339
-(defun isa-view-doc 222,8101
-(defun isa-tool-list-docs 231,8365
-(defconst isabelle-verbatim-regexp 258,9397
-(defun isabelle-verbatim 261,9539
-(defcustom isabelle-refresh-logics 268,9700
-(defvar isabelle-docs-menu 276,10027
-(defvar isabelle-logics-menu-entries 283,10313
-(defun isabelle-logics-menu-calculate 286,10386
-(defvar isabelle-time-to-refresh-logics 305,10949
-(defun isabelle-logics-menu-refresh 309,11044
-(defun isabelle-logics-menu-filter 326,11741
-(defun isabelle-menu-bar-update-logics 332,11951
-(defvar isabelle-logics-menu343,12290
-(defun isabelle-load-isar-keywords 356,12902
-(defpgdefault menu-entries377,13643
-(defpgdefault help-menu-entries 380,13695
-(defun isabelle-convert-idmarkup-to-subterm 408,14453
-(defun isabelle-create-span-menu 432,15464
-(defun isabelle-xml-sml-escapes 448,15906
-(defun isabelle-process-pgip 451,16007
-
-isar/isar.el,1162
-(defcustom isar-keywords-name 31,720
-(defpgdefault completion-table 48,1243
-(defcustom isar-web-page50,1296
-(defun isar-strip-terminators 64,1632
-(defun isar-markup-ml 77,2009
-(defun isar-mode-config-set-variables 82,2144
-(defun isar-shell-mode-config-set-variables 152,5365
-(defun isar-remove-file 248,9355
-(defun isar-shell-compute-new-files-list 258,9718
-(define-derived-mode isar-shell-mode 274,10239
-(define-derived-mode isar-response-mode 279,10362
-(define-derived-mode isar-goals-mode 284,10544
-(define-derived-mode isar-mode 289,10719
-(defpgdefault menu-entries346,12754
-(defun isar-count-undos 376,13993
-(defun isar-find-and-forget 403,15107
-(defun isar-goal-command-p 442,16687
-(defun isar-global-save-command-p 447,16864
-(defvar isar-current-goal 468,17725
-(defun isar-state-preserving-p 471,17791
-(defvar isar-shell-current-line-width 496,18988
-(defun isar-shell-adjust-line-width 501,19180
-(defun isar-preprocessing 524,20071
-(defun isar-mode-config 547,21338
-(defun isar-shell-mode-config 558,21839
-(defun isar-response-mode-config 569,22198
-(defun isar-goals-mode-config 578,22441
-(defun isar-goalhyplit-test 589,22773
+(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
 
 isar/isar-find-theorems.el,778
 (defun isar-find-theorems-minibuffer 18,712
@@ -501,202 +460,175 @@ isar/isar-mmm.el,83
 (defconst isar-start-latex-regexp 23,697
 (defconst isar-start-sml-regexp 35,1130
 
-isar/isar-syntax.el,3470
-(defconst isar-script-syntax-table-entries20,477
-(defconst isar-script-syntax-table-alist61,1508
-(defun isar-init-syntax-table 70,1798
-(defun isar-init-output-syntax-table 78,2045
-(defconst isar-keyword-begin 94,2492
-(defconst isar-keyword-end 95,2530
-(defconst isar-keywords-theory-enclose97,2565
-(defconst isar-keywords-theory102,2710
-(defconst isar-keywords-save107,2855
-(defconst isar-keywords-proof-enclose112,2984
-(defconst isar-keywords-proof118,3166
-(defconst isar-keywords-proof-context125,3371
-(defconst isar-keywords-local-goal129,3485
-(defconst isar-keywords-proper133,3597
-(defconst isar-keywords-improper138,3730
-(defconst isar-keywords-outline143,3876
-(defconst isar-keywords-fume146,3941
-(defconst isar-keywords-indent-open153,4159
-(defconst isar-keywords-indent-close159,4343
-(defconst isar-keywords-indent-enclose163,4448
-(defun isar-regexp-simple-alt 172,4663
-(defun isar-ids-to-regexp 192,5423
-(defconst isar-ext-first 226,6829
-(defconst isar-ext-rest 227,6896
-(defconst isar-long-id-stuff 229,6968
-(defconst isar-id 230,7042
-(defconst isar-idx 231,7112
-(defconst isar-string 233,7171
-(defconst isar-any-command-regexp235,7231
-(defconst isar-name-regexp239,7365
-(defconst isar-improper-regexp245,7660
-(defconst isar-save-command-regexp249,7808
-(defconst isar-global-save-command-regexp252,7909
-(defconst isar-goal-command-regexp255,8023
-(defconst isar-local-goal-command-regexp258,8131
-(defconst isar-comment-start 261,8244
-(defconst isar-comment-end 262,8279
-(defconst isar-comment-start-regexp 263,8312
-(defconst isar-comment-end-regexp 264,8383
-(defconst isar-string-start-regexp 266,8451
-(defconst isar-string-end-regexp 267,8503
-(defconst isar-antiq-regexp276,8756
-(defconst isar-nesting-regexp283,8917
-(defun isar-nesting 286,9015
-(defun isar-match-nesting 298,9436
-(defface isabelle-class-name-face310,9767
-(defface isabelle-tfree-name-face318,9950
-(defface isabelle-tvar-name-face326,10139
-(defface isabelle-free-name-face334,10327
-(defface isabelle-bound-name-face342,10511
-(defface isabelle-var-name-face350,10698
-(defconst isabelle-class-name-face 358,10885
-(defconst isabelle-tfree-name-face 359,10947
-(defconst isabelle-tvar-name-face 360,11009
-(defconst isabelle-free-name-face 361,11070
-(defconst isabelle-bound-name-face 362,11131
-(defconst isabelle-var-name-face 363,11193
-(defconst isar-font-lock-local366,11255
-(defvar isar-font-lock-keywords-1371,11421
-(defvar isar-output-font-lock-keywords-1385,12287
-(defvar isar-goals-font-lock-keywords412,13911
-(defconst isar-undo 446,14590
-(defun isar-remove 448,14633
-(defun isar-undos 451,14708
-(defun isar-cannot-undo 455,14814
-(defconst isar-theory-start-regexp458,14884
-(defconst isar-end-regexp464,15049
-(defconst isar-undo-fail-regexp468,15150
-(defconst isar-undo-skip-regexp472,15254
-(defconst isar-undo-ignore-regexp475,15375
-(defconst isar-undo-remove-regexp478,15440
-(defconst isar-any-entity-regexp486,15615
-(defconst isar-named-entity-regexp491,15802
-(defconst isar-unnamed-entity-regexp496,15979
-(defconst isar-next-entity-regexps499,16081
-(defconst isar-generic-expression507,16392
-(defconst isar-indent-any-regexp518,16709
-(defconst isar-indent-inner-regexp520,16802
-(defconst isar-indent-enclose-regexp522,16868
-(defconst isar-indent-open-regexp524,16984
-(defconst isar-indent-close-regexp526,17094
-(defconst isar-outline-regexp532,17231
-(defconst isar-outline-heading-end-regexp 536,17384
-
-isar/isar-unicode-tokens.el,431
-(defconst isar-token-format 14,433
-(defconst isar-charref-format 15,471
-(defconst isar-token-prefix 16,513
-(defconst isar-token-suffix 17,548
-(defconst isar-token-match 18,581
-(defconst isar-control-token-match 19,646
-(defconst isar-control-token-format 20,720
-(defconst isar-hexcode-match 21,767
-(defconst isar-next-character-regexp 22,828
-(defcustom isar-token-name-alist24,897
-(defcustom isar-shortcut-alist496,13694
-
-isar/x-symbol-isar.el,1775
-(defvar x-symbol-isar-required-fonts 15,498
-(defvar x-symbol-isar-name 23,898
-(defvar x-symbol-isar-modeline-name 24,944
-(defcustom x-symbol-isar-header-groups-alist 26,988
-(defcustom x-symbol-isar-electric-ignore 33,1208
-(defvar x-symbol-isar-required-fonts 41,1456
-(defvar x-symbol-isar-extra-menu-items 44,1561
-(defvar x-symbol-isar-token-grammar48,1655
-(defun x-symbol-isar-token-list 55,1853
-(defvar x-symbol-isar-user-table 58,1938
-(defvar x-symbol-isar-generated-data 61,2051
-(defvar x-symbol-isar-master-directory 69,2290
-(defvar x-symbol-isar-image-searchpath 70,2339
-(defvar x-symbol-isar-image-cached-dirs 71,2387
-(defvar x-symbol-isar-image-file-truename-alist 72,2453
-(defvar x-symbol-isar-image-keywords 73,2506
-(defcustom x-symbol-isar-subscript-matcher 83,2846
-(defcustom x-symbol-isar-font-lock-regexp 89,3081
-(defcustom x-symbol-isar-font-lock-limit-regexp 94,3257
-(defcustom x-symbol-isar-font-lock-contents-regexp 100,3481
-(defcustom x-symbol-isar-single-char-regexp 110,3865
-(defun x-symbol-isar-subscript-matcher 116,4135
-(defun isabelle-match-subscript 158,5787
-(defvar x-symbol-isar-font-lock-keywords167,6163
-(defvar x-symbol-isar-font-lock-allowed-faces 174,6423
-(defcustom x-symbol-isar-class-alist181,6651
-(defcustom x-symbol-isar-class-face-alist 192,7072
-(defvar x-symbol-isar-case-insensitive 207,7592
-(defvar x-symbol-isar-token-shape 208,7636
-(defvar x-symbol-isar-input-token-ignore 209,7675
-(defvar x-symbol-isar-token-list 210,7721
-(defvar x-symbol-isar-symbol-table 212,7766
-(defvar x-symbol-isar-xsymbol-table 312,10498
-(defun x-symbol-isar-prepare-table 458,14928
-(defvar x-symbol-isar-table466,15124
-(defcustom x-symbol-isar-auto-style480,15457
-(defcustom x-symbol-isar-auto-coding-alist 494,15954
+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-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
 
 lclam/lclam.el,524
-(defcustom lclam-prog-name 15,385
-(defcustom lclam-web-page21,533
-(defun lclam-config 32,763
-(defun lclam-shell-config 54,1557
-(define-derived-mode lclam-proofscript-mode 74,2216
-(define-derived-mode lclam-shell-mode 79,2339
-(define-derived-mode lclam-response-mode 84,2473
-(define-derived-mode lclam-goals-mode 88,2596
-(defun lclam-mode 96,2824
-(define-derived-mode thy-mode 133,3635
-(defvar thy-mode-map 136,3733
-(defun thy-add-menus 138,3760
-(defun process-thy-file 178,5674
-(defun update-thy-only 184,5875
+(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
 
 lego/lego.el,1727
-(defcustom lego-tags 19,493
-(defcustom lego-test-all-name 24,629
-(defpgdefault help-menu-entries30,787
-(defpgdefault menu-entries34,947
-(defvar lego-shell-process-output45,1249
-(defconst lego-process-config53,1572
-(defconst lego-pretty-set-width 64,2003
-(defconst lego-interrupt-regexp 68,2146
-(defcustom lego-www-home-page 73,2263
-(defcustom lego-www-latest-release78,2387
-(defcustom lego-www-refcard84,2565
-(defcustom lego-library-www-page90,2714
-(defvar lego-prog-name 99,2930
-(defvar lego-shell-prompt-pattern 102,2999
-(defvar lego-shell-cd 105,3120
-(defvar lego-shell-abort-goal-regexp 108,3220
-(defvar lego-shell-proof-completed-regexp 113,3412
-(defvar lego-save-command-regexp116,3552
-(defvar lego-goal-command-regexp118,3642
-(defvar lego-kill-goal-command 121,3733
-(defvar lego-forget-id-command 122,3776
-(defvar lego-undoable-commands-regexp124,3822
-(defvar lego-goal-regexp 133,4196
-(defvar lego-outline-regexp135,4241
-(defvar lego-outline-heading-end-regexp 141,4417
-(defvar lego-shell-outline-regexp 143,4470
-(defvar lego-shell-outline-heading-end-regexp 144,4522
-(define-derived-mode lego-shell-mode 150,4801
-(define-derived-mode lego-mode 157,4962
-(define-derived-mode lego-goals-mode 168,5259
-(defun lego-count-undos 179,5685
-(defun lego-goal-command-p 199,6504
-(defun lego-find-and-forget 204,6675
-(defun lego-goal-hyp 246,8511
-(defun lego-state-preserving-p 255,8709
-(defvar lego-shell-current-line-width 271,9412
-(defun lego-shell-adjust-line-width 279,9719
-(defun lego-mode-config 298,10458
-(defun lego-equal-module-filename 366,12485
-(defun lego-shell-compute-new-files-list 372,12760
-(defun lego-shell-mode-config 386,13286
-(defun lego-goals-mode-config 435,15222
+(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
 
 lego/lego-syntax.el,600
 (defconst lego-keywords-goal 15,358
@@ -716,24 +648,23 @@ lego/lego-syntax.el,600
 (defvar lego-font-lock-keywords-199,3667
 (defun lego-init-syntax-table 110,4134
 
-phox/phox.el,644
-(defcustom phox-prog-name 31,909
-(defcustom phox-sym-lock-enabled 36,1011
-(defcustom phox-web-page42,1118
-(defcustom phox-doc-dir 48,1268
-(defcustom phox-lib-dir 54,1416
-(defcustom phox-tags-program 60,1560
-(defcustom phox-tags-doc 66,1740
-(defcustom phox-etags 72,1878
-(defpgdefault menu-entries93,2330
-(defun phox-config 107,2523
-(defun phox-shell-config 153,4560
-(define-derived-mode phox-mode 178,5489
-(define-derived-mode phox-shell-mode 201,6152
-(define-derived-mode phox-response-mode 206,6280
-(define-derived-mode phox-goals-mode 218,6707
-(defpgdefault completion-table243,7575
-(defpgdefault x-symbol-language 251,7680
+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
 
 phox/phox-extraction.el,382
 (defvar phox-prog-orig 11,480
@@ -833,50 +764,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,766
-(defun phox-tags-reset-table(38,1354
-(defun phox-tags-add-doc-table(48,1619
-(defun phox-tags-add-lib-table(54,1768
-(defun phox-tags-add-local-table(60,1904
-(defun phox-tags-create-local-table(66,2087
-(defun phox-complete-tag(77,2339
-(defvar phox-tags-menu96,2889
-
-phox/x-symbol-phox.el,1609
-(defvar x-symbol-phox-required-fonts 16,472
-(defcustom x-symbol-phox-header-groups-alist 31,1079
-(defcustom x-symbol-phox-electric-ignore 38,1299
-(defvar x-symbol-phox-required-fonts 45,1515
-(defvar x-symbol-phox-extra-menu-items 48,1616
-(defvar x-symbol-phox-token-grammar51,1705
-(defvar x-symbol-phox-input-token-grammar65,2496
-(defun x-symbol-phox-default-token-list 71,2751
-(defvar x-symbol-phox-user-table 83,3069
-(defvar x-symbol-phox-generated-data 86,3178
-(defvar x-symbol-phox-master-directory 94,3417
-(defvar x-symbol-phox-image-searchpath 95,3466
-(defvar x-symbol-phox-image-cached-dirs 96,3514
-(defvar x-symbol-phox-image-file-truename-alist 97,3580
-(defvar x-symbol-phox-image-keywords 98,3633
-(defcustom x-symbol-phox-class-alist105,3854
-(defcustom x-symbol-phox-class-face-alist 116,4236
-(defvar x-symbol-phox-font-lock-keywords 126,4549
-(defvar x-symbol-phox-font-lock-allowed-faces 128,4596
-(defvar x-symbol-phox-case-insensitive 134,4821
-(defvar x-symbol-phox-token-shape 135,4865
-(defvar x-symbol-phox-input-token-ignore 136,4904
-(defvar x-symbol-phox-token-list 143,5143
-(defvar x-symbol-phox-xsymb0-table 145,5188
-(defun x-symbol-phox-prepare-table 166,5647
-(defvar x-symbol-phox-table174,5823
-(defcustom x-symbol-phox-auto-style185,6141
-(defvar x-symbol-phox-menu-alist 211,7084
-(defvar x-symbol-phox-grid-alist 213,7174
-(defvar x-symbol-phox-decode-atree 216,7265
-(defvar x-symbol-phox-decode-alist 218,7358
-(defvar x-symbol-phox-encode-alist 220,7455
-(defvar x-symbol-phox-nomule-decode-exec 224,7612
-(defvar x-symbol-phox-nomule-encode-exec 226,7712
+(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
 
 plastic/plastic.el,2866
 (defcustom plastic-tags 29,821
@@ -920,32 +815,32 @@ plastic/plastic.el,2866
 (defvar plastic-shell-current-line-width 314,10606
 (defun plastic-shell-adjust-line-width 322,10922
 (defun plastic-mode-config 349,12017
-(defun plastic-show-shell-buffer 438,15258
-(defun plastic-equal-module-filename 444,15361
-(defun plastic-shell-compute-new-files-list 450,15639
-(defun plastic-shell-mode-config 466,16176
-(defun plastic-goals-mode-config 517,18369
-(defun plastic-small-bar 529,18651
-(defun plastic-large-bar 531,18740
-(defun plastic-preprocessing 533,18878
-(defun plastic-all-ctxt 584,20706
-(defun plastic-send-one-undo 591,20884
-(defun plastic-minibuf-cmd 601,21212
-(defun plastic-minibuf 613,21691
-(defun plastic-synchro 620,21897
-(defun plastic-send-minibuf 625,22038
-(defun plastic-had-error 633,22367
-(defun plastic-reset-error 637,22542
-(defun plastic-call-if-no-error 640,22681
-(defun plastic-show-shell 645,22885
-(define-key plastic-keymap 654,23147
-(define-key plastic-keymap 655,23208
-(define-key plastic-keymap 656,23269
-(define-key plastic-keymap 657,23329
-(define-key plastic-keymap 658,23388
-(define-key plastic-keymap 659,23447
-(defalias 'proof-toolbar-command proof-toolbar-command
669,23697
-(defalias 'proof-minibuffer-cmd proof-minibuffer-cmd
670,23748
+(defun plastic-show-shell-buffer 438,15292
+(defun plastic-equal-module-filename 444,15395
+(defun plastic-shell-compute-new-files-list 450,15673
+(defun plastic-shell-mode-config 466,16210
+(defun plastic-goals-mode-config 517,18415
+(defun plastic-small-bar 529,18709
+(defun plastic-large-bar 531,18798
+(defun plastic-preprocessing 533,18936
+(defun plastic-all-ctxt 584,20764
+(defun plastic-send-one-undo 591,20942
+(defun plastic-minibuf-cmd 601,21270
+(defun plastic-minibuf 613,21749
+(defun plastic-synchro 620,21955
+(defun plastic-send-minibuf 625,22096
+(defun plastic-had-error 633,22425
+(defun plastic-reset-error 637,22600
+(defun plastic-call-if-no-error 640,22739
+(defun plastic-show-shell 645,22943
+(define-key plastic-keymap 654,23205
+(define-key plastic-keymap 655,23266
+(define-key plastic-keymap 656,23327
+(define-key plastic-keymap 657,23387
+(define-key plastic-keymap 658,23446
+(define-key plastic-keymap 659,23505
+(defalias 'proof-toolbar-command proof-toolbar-command
669,23755
+(defalias 'proof-minibuffer-cmd proof-minibuffer-cmd
670,23806
 
 plastic/plastic-syntax.el,648
 (defconst plastic-keywords-goal 18,537
@@ -1185,16 +1080,9 @@ twelf/twelf-old.el,6958
 (defun twelf-server-remove-menu 2651,107274
 (defun twelf-server-reset-menu 2655,107386
 
-generic/pg-assoc.el,402
-(defun proof-associated-buffers 38,1096
-(defun proof-associated-windows 48,1308
-(defun pg-assoc-strip-subterm-markup 65,1789
-(defvar pg-assoc-ann-regexp 91,2722
-(defun pg-assoc-strip-subterm-markup-buf 94,2817
-(defun pg-assoc-strip-subterm-markup-buf-old 117,3536
-(defconst pg-assoc-active-area-keymap 146,4391
-(defun pg-assoc-make-top-span 153,4616
-(defun pg-assoc-analyse-structure 190,6081
+generic/pg-assoc.el,82
+(defun proof-associated-buffers 36,1069
+(defun proof-associated-windows 46,1281
 
 generic/pg-autotest.el,442
 (defvar pg-autotest-success 24,543
@@ -1209,79 +1097,74 @@ generic/pg-autotest.el,442
 (defun pg-autotest-quit-prover 106,3158
 (defun pg-autotest-finished 112,3339
 
-generic/pg-custom.el,678
-(defpgcustom x-symbol-enable 32,1065
-(defpgcustom x-symbol-language 42,1491
-(defpgcustom maths-menu-enable 47,1713
-(defpgcustom unicode-tokens-enable 53,1893
-(defpgcustom unicode-tokens2-enable 59,2070
-(defpgcustom mmm-enable 65,2248
-(defpgcustom script-indent 74,2602
-(defconst proof-toolbar-entries-default79,2739
-(defpgcustom toolbar-entries 113,4652
-(defpgcustom prog-args 131,5372
-(defpgcustom prog-env 144,5947
-(defpgcustom favourites 153,6373
-(defpgcustom menu-entries 158,6562
-(defpgcustom help-menu-entries 165,6798
-(defpgcustom keymap 172,7061
-(defpgcustom completion-table 177,7233
-(defpgcustom tags-program 188,7607
-(defpgcustom use-holes 197,7991
-
-generic/pg-goals.el,363
-(define-derived-mode proof-goals-mode 30,632
-(define-key proof-goals-mode-map 61,1623
-(defun proof-goals-config-done 91,3091
-(defun pg-goals-display 101,3379
-(defun pg-goals-yank-subterm 167,5816
-(defun pg-goals-button-action 194,6716
-(defun proof-expand-path 215,7688
-(defun pg-goals-construct-command 224,7930
-(defun pg-goals-get-subterm-help 256,9118
+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
+
+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
 
 generic/pg-pbrpm.el,1803
-(defvar pg-pbrpm-use-buffer-menu 22,547
-(defvar pg-pbrpm-start-goal-regexp 25,669
-(defvar pg-pbrpm-start-goal-regexp-par-num 29,826
-(defvar pg-pbrpm-end-goal-regexp 32,949
-(defvar pg-pbrpm-start-hyp-regexp 36,1101
-(defvar pg-pbrpm-start-hyp-regexp-par-num 40,1262
-(defvar pg-pbrpm-start-concl-regexp 44,1469
-(defvar pg-pbrpm-auto-select-regexp 48,1633
-(defvar pg-pbrpm-buffer-menu 55,1794
-(defvar pg-pbrpm-spans 56,1828
-(defvar pg-pbrpm-goal-description 57,1856
-(defvar pg-pbrpm-windows-dialog-bug 58,1895
-(defvar pbrpm-menu-desc 59,1936
-(defun pg-pbrpm-erase-buffer-menu 61,1966
-(defun pg-pbrpm-menu-change-hook 68,2150
-(defun pg-pbrpm-create-reset-buffer-menu 86,2726
-(defun pg-pbrpm-analyse-goal-buffer 101,3355
-(defun pg-pbrpm-button-action 161,5765
-(defun pg-pbrpm-exists 168,5991
-(defun pg-pbrpm-eliminate-id 172,6103
-(defun pg-pbrpm-build-menu 180,6349
-(defun pg-pbrpm-setup-span 253,8976
-(defun pg-pbrpm-run-command 313,11294
-(defun pg-pbrpm-get-pos-info 342,12604
-(defun pg-pbrpm-get-region-info 384,13911
-(defun pg-pbrpm-auto-select-around-point 395,14325
-(defun pg-pbrpm-translate-position 410,14855
-(defun pg-pbrpm-process-click 418,15113
-(defvar pg-pbrpm-remember-region-selected-region 438,16138
-(defvar pg-pbrpm-regions-list 439,16192
-(defun pg-pbrpm-erase-regions-list 441,16228
-(defun pg-pbrpm-filter-regions-list 450,16536
-(defface pg-pbrpm-multiple-selection-face457,16799
-(defface pg-pbrpm-menu-input-face465,17001
-(defun pg-pbrpm-do-remember-region 473,17191
-(defun pg-pbrpm-remember-region-drag-up-hook 494,18039
-(defun pg-pbrpm-remember-region-click-hook 498,18210
-(defun pg-pbrpm-remember-region 503,18395
-(defun pg-pbrpm-process-region 517,19110
-(defun pg-pbrpm-process-regions-list 535,19839
-(defun pg-pbrpm-region-expression 539,20022
+(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
 
 generic/pg-pgip.el,2889
 (defalias 'pg-pgip-debug pg-pgip-debug
35,919
@@ -1352,116 +1235,113 @@ generic/pg-pgip.el,2889
 (defconst pg-pgip-start-element-regexp 668,22748
 (defconst pg-pgip-end-element-regexp 669,22800
 
-generic/pg-response.el,1182
-(deflocal pg-response-eagerly-raise 31,730
-(define-derived-mode proof-response-mode 41,955
-(defun proof-response-config-done 67,2080
-(defvar pg-response-special-display-regexp 88,2855
-(defconst proof-multiframe-specifiers96,3261
-(defun proof-map-multiple-frame-specifiers 105,3618
-(defconst proof-multiframe-parameters116,4140
-(defun proof-multiple-frames-enable 125,4439
-(defun proof-three-window-enable 143,5083
-(defun proof-select-three-b 147,5147
-(defun proof-display-three-b 162,5616
-(defvar pg-frame-configuration 176,6108
-(defun pg-cache-frame-configuration 180,6255
-(defun proof-layout-windows 184,6426
-(defun proof-delete-other-frames 225,8249
-(defvar pg-response-erase-flag 256,9339
-(defun pg-response-maybe-erase260,9468
-(defun pg-response-display 291,10653
-(defun pg-response-display-with-face 310,11501
-(defun pg-response-clear-displays 346,12731
-(defun proof-next-error 365,13318
-(defun pg-response-has-error-location 446,16234
-(defvar proof-trace-last-fontify-pos 469,17067
-(defun proof-trace-fontify-pos 471,17110
-(defun proof-trace-buffer-display 479,17423
-(defun proof-trace-buffer-finish 503,18395
-(defun pg-thms-buffer-clear 524,18975
+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
 
 generic/pg-thymodes.el,152
-(defmacro pg-defthymode 23,499
-(defmacro pg-do-unless-null 71,2307
-(defun pg-symval 76,2394
-(defun pg-modesym 82,2549
-(defun pg-modesymval 86,2663
-
-generic/pg-user.el,3127
-(defmacro proof-maybe-save-point 31,805
-(defun proof-maybe-follow-locked-end 39,1007
-(defun proof-assert-next-command-interactive 53,1372
-(defun proof-process-buffer 63,1743
-(defun proof-undo-last-successful-command 77,2060
-(defun proof-undo-and-delete-last-successful-command 82,2222
-(defun proof-undo-last-successful-command-1 104,3193
-(defun proof-retract-buffer 120,3758
-(defun proof-retract-current-goal 129,4038
-(defun proof-interrupt-process 148,4544
-(defun proof-goto-command-start 175,5533
-(defun proof-goto-command-end 198,6473
-(defun proof-mouse-goto-point 223,7251
-(defun proof-mouse-track-insert 239,7883
-(defvar proof-minibuffer-history 275,9020
-(defun proof-minibuffer-cmd 278,9115
-(defun proof-frob-locked-end 326,10909
-(defmacro proof-if-setting-configured 387,12839
-(defmacro proof-define-assistant-command 395,13108
-(defmacro proof-define-assistant-command-witharg 408,13563
-(defun proof-issue-new-command 428,14386
-(defun proof-cd-sync 472,15829
-(defun proof-electric-terminator-enable 531,17588
-(defun proof-electric-term-incomment-fn 539,17883
-(defun proof-process-electric-terminator 559,18634
-(defun proof-electric-terminator 586,19782
-(defun proof-add-completions 608,20419
-(defun proof-script-complete 628,21173
-(defun pg-insert-last-output-as-comment 656,21764
-(defun pg-copy-span-contents 687,22998
-(defun pg-numth-span-higher-or-lower 704,23556
-(defun pg-control-span-of 730,24302
-(defun pg-move-span-contents 736,24506
-(defun pg-fixup-children-spans 788,26686
-(defun pg-move-region-down 798,26949
-(defun pg-move-region-up 807,27242
-(defun proof-forward-command 837,28080
-(defun proof-backward-command 858,28801
-(defun pg-pos-for-event 880,29152
-(defun pg-span-for-event 892,29513
-(defun pg-span-context-menu 896,29657
-(defun pg-toggle-visibility 911,30112
-(defun pg-create-in-span-context-menu 921,30434
-(defun pg-span-undo 954,31778
-(defun pg-goals-buffers-hint 1000,33188
-(defun pg-slow-fontify-tracing-hint 1004,33370
-(defun pg-response-buffers-hint 1008,33541
-(defun pg-jump-to-end-hint 1018,33903
-(defun pg-processing-complete-hint 1022,34034
-(defun pg-next-error-hint 1039,34733
-(defun pg-hint 1044,34885
-(defun pg-identifier-under-mouse-query 1063,35554
-(defun proof-imenu-enable 1109,37209
-(defvar pg-input-ring 1142,38349
-(defvar pg-input-ring-index 1145,38405
-(defvar pg-stored-incomplete-input 1148,38476
-(defun pg-previous-input 1151,38578
-(defun pg-next-input 1165,39035
-(defun pg-delete-input 1170,39157
-(defun pg-get-old-input 1183,39495
-(defun pg-restore-input 1197,39886
-(defun pg-search-start 1208,40176
-(defun pg-regexp-arg 1220,40668
-(defun pg-search-arg 1232,41116
-(defun pg-previous-matching-input-string-position 1246,41533
-(defun pg-previous-matching-input 1273,42698
-(defun pg-next-matching-input 1292,43534
-(defvar pg-matching-input-from-input-string 1300,43917
-(defun pg-previous-matching-input-from-input 1304,44031
-(defun pg-next-matching-input-from-input 1322,44796
-(defun pg-add-to-input-history 1333,45175
-(defun pg-remove-from-input-history 1345,45628
-(defun  pg-clear-input-ring 1356,46011
+(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
+
+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
 
 generic/pg-vars.el,1106
 (defvar proof-assistant-cusgrp 20,379
@@ -1492,269 +1372,265 @@ generic/pg-vars.el,1106
 (defvar proof-nesting-depth 175,6353
 (defvar proof-last-theorem-dependencies 182,6588
 
-generic/pg-xml.el,1141
-(defalias 'pg-xml-error pg-xml-error
24,625
-(defun pg-xml-parse-string 47,1267
-(defun pg-xml-parse-buffer 58,1593
-(defun pg-xml-get-attr 80,2326
-(defun pg-xml-child-elts 88,2628
-(defun pg-xml-child-elt 93,2833
-(defun pg-xml-get-child 101,3115
-(defun pg-xml-get-text-content 111,3487
-(defmacro pg-xml-attr 122,3837
-(defmacro pg-xml-node 124,3899
-(defconst pg-xml-header127,3991
-(defun pg-xml-string-of 131,4067
-(defun pg-xml-output-internal 142,4434
-(defun pg-xml-cdata 176,5584
-(defun pg-pgip-get-icon 184,5777
-(defsubst pg-pgip-get-name 188,5925
-(defsubst pg-pgip-get-version 191,6042
-(defsubst pg-pgip-get-descr 194,6165
-(defsubst pg-pgip-get-thmname 197,6284
-(defsubst pg-pgip-get-thyname 200,6407
-(defsubst pg-pgip-get-url 203,6530
-(defsubst pg-pgip-get-srcid 206,6645
-(defsubst pg-pgip-get-proverid 209,6764
-(defsubst pg-pgip-get-symname 212,6889
-(defsubst pg-pgip-get-prefcat 215,7009
-(defsubst pg-pgip-get-default 218,7137
-(defsubst pg-pgip-get-objtype 221,7260
-(defsubst pg-pgip-get-value 224,7383
-(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext
227,7453
-(defun pg-pgip-get-pgmltext 229,7512
+generic/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
 
 generic/proof-auxmodes.el,149
-(defun proof-mmm-support-available 23,575
-(defun proof-maths-menu-support-available 47,1193
-(defun proof-unicode-tokens-support-available 66,1807
-
-generic/proof-config.el,11009
-(defgroup proof-user-options 85,3024
-(defun proof-set-value 94,3221
-(defcustom proof-electric-terminator-enable 127,4340
-(defcustom proof-toolbar-enable 139,4872
-(defcustom proof-imenu-enable 145,5045
-(defcustom pg-show-hints 151,5216
-(defcustom proof-output-fontify-enable 156,5351
-(defcustom proof-trace-output-slow-catchup 166,5734
-(defcustom proof-strict-state-preserving 176,6231
-(defcustom proof-strict-read-only 189,6840
-(defcustom proof-allow-undo-in-read-only 198,7189
-(defcustom proof-three-window-enable 206,7522
-(defcustom proof-multiple-frames-enable 225,8272
-(defcustom proof-delete-empty-windows 234,8605
-(defcustom proof-shrink-windows-tofit 245,9136
-(defcustom proof-toolbar-use-button-enablers 252,9408
-(defcustom proof-query-file-save-when-activating-scripting260,9743
-(defcustom proof-one-command-per-line276,10463
-(defcustom proof-prog-name-ask283,10690
-(defcustom proof-prog-name-guess289,10850
-(defcustom proof-tidy-response297,11109
-(defcustom proof-keep-response-history311,11572
-(defcustom pg-input-ring-size 321,11960
-(defcustom proof-general-debug 326,12112
-(defcustom proof-experimental-features 336,12484
-(defcustom proof-follow-mode 350,13019
-(defcustom proof-auto-action-when-deactivating-scripting 374,14199
-(defcustom proof-script-command-separator 397,15148
-(defcustom proof-rsh-command 405,15440
-(defcustom proof-disappearing-proofs 421,15990
-(defgroup proof-faces 448,16636
-(defconst pg-defface-window-systems 455,16818
-(defmacro proof-face-specs 468,17363
-(defface proof-queue-face483,17815
-(defface proof-locked-face491,18093
-(defface proof-declaration-name-face504,18596
-(defface proof-tacticals-name-face513,18882
-(defface proof-tactics-name-face522,19144
-(defface proof-error-face531,19409
-(defface proof-warning-face539,19615
-(defface proof-eager-annotation-face548,19872
-(defface proof-debug-message-face556,20090
-(defface proof-boring-face564,20289
-(defface proof-mouse-highlight-face572,20481
-(defface proof-highlight-dependent-face580,20677
-(defface proof-highlight-dependency-face588,20886
-(defface proof-active-area-face596,21083
-(defconst proof-face-compat-doc 605,21479
-(defconst proof-queue-face 606,21559
-(defconst proof-locked-face 607,21627
-(defconst proof-declaration-name-face 608,21697
-(defconst proof-tacticals-name-face 609,21787
-(defconst proof-tactics-name-face 610,21873
-(defconst proof-error-face 611,21955
-(defconst proof-warning-face 612,22023
-(defconst proof-eager-annotation-face 613,22095
-(defconst proof-debug-message-face 614,22185
-(defconst proof-boring-face 615,22269
-(defconst proof-mouse-highlight-face 616,22339
-(defconst proof-highlight-dependent-face 617,22427
-(defconst proof-highlight-dependency-face 618,22523
-(defconst proof-active-area-face 619,22621
-(defgroup prover-config 632,22765
-(defcustom proof-guess-command-line 674,24076
-(defcustom proof-assistant-home-page 689,24571
-(defcustom proof-context-command 695,24741
-(defcustom proof-info-command 700,24875
-(defcustom proof-showproof-command 707,25146
-(defcustom proof-goal-command 712,25282
-(defcustom proof-save-command 720,25579
-(defcustom proof-find-theorems-command 728,25888
-(defcustom proof-assistant-true-value 735,26198
-(defcustom proof-assistant-false-value 741,26388
-(defcustom proof-assistant-format-int-fn 747,26582
-(defcustom proof-assistant-format-string-fn 754,26831
-(defcustom proof-assistant-setting-format 761,27098
-(defgroup proof-script 783,27793
-(defcustom proof-terminal-char 788,27923
-(defcustom proof-script-sexp-commands 798,28310
-(defcustom proof-script-command-end-regexp 809,28767
-(defcustom proof-script-command-start-regexp 827,29586
-(defcustom proof-script-use-old-parser 838,30047
-(defcustom proof-script-integral-proofs 850,30533
-(defcustom proof-script-fly-past-comments 865,31189
-(defcustom proof-script-parse-function 870,31360
-(defcustom proof-script-comment-start 888,32003
-(defcustom proof-script-comment-start-regexp 899,32440
-(defcustom proof-script-comment-end 907,32757
-(defcustom proof-script-comment-end-regexp 919,33179
-(defcustom pg-insert-output-as-comment-fn 927,33490
-(defcustom proof-string-start-regexp 933,33742
-(defcustom proof-string-end-regexp 938,33907
-(defcustom proof-case-fold-search 943,34068
-(defcustom proof-save-command-regexp 952,34478
-(defcustom proof-save-with-hole-regexp 957,34588
-(defcustom proof-save-with-hole-result 969,35042
-(defcustom proof-goal-command-regexp 979,35493
-(defcustom proof-goal-with-hole-regexp 988,35881
-(defcustom proof-goal-with-hole-result 1000,36322
-(defcustom proof-non-undoables-regexp 1009,36709
-(defcustom proof-nested-undo-regexp 1020,37164
-(defcustom proof-ignore-for-undo-count 1036,37876
-(defcustom proof-script-next-entity-regexps 1044,38179
-(defcustom proof-script-find-next-entity-fn1088,39914
-(defcustom proof-script-imenu-generic-expression 1108,40752
-(defcustom proof-goal-command-p 1126,41605
-(defcustom proof-really-save-command-p 1153,43042
-(defcustom proof-completed-proof-behaviour 1165,43504
-(defcustom proof-count-undos-fn 1193,44860
-(defconst proof-no-command 1205,45409
-(defcustom proof-find-and-forget-fn 1210,45614
-(defcustom proof-forget-id-command 1227,46326
-(defcustom pg-topterm-goalhyplit-fn 1237,46684
-(defcustom proof-kill-goal-command 1249,47219
-(defcustom proof-undo-n-times-cmd 1263,47720
-(defcustom proof-nested-goals-history-p 1277,48268
-(defcustom proof-state-preserving-p 1286,48605
-(defcustom proof-activate-scripting-hook 1296,49075
-(defcustom proof-deactivate-scripting-hook 1315,49854
-(defcustom proof-indent 1328,50219
-(defcustom proof-indent-hang 1333,50326
-(defcustom proof-indent-enclose-offset 1338,50452
-(defcustom proof-indent-open-offset 1343,50594
-(defcustom proof-indent-close-offset 1348,50731
-(defcustom proof-indent-any-regexp 1353,50869
-(defcustom proof-indent-inner-regexp 1358,51029
-(defcustom proof-indent-enclose-regexp 1363,51183
-(defcustom proof-indent-open-regexp 1368,51337
-(defcustom proof-indent-close-regexp 1373,51489
-(defcustom proof-script-font-lock-keywords 1379,51643
-(defcustom proof-script-syntax-table-entries 1387,51972
-(defcustom proof-script-span-context-menu-extensions 1405,52369
-(defgroup proof-shell 1431,53129
-(defcustom proof-prog-name 1441,53300
-(defcustom proof-shell-auto-terminate-commands 1452,53718
-(defcustom proof-shell-pre-sync-init-cmd 1461,54115
-(defcustom proof-shell-init-cmd 1475,54673
-(defcustom proof-shell-restart-cmd 1486,55142
-(defcustom proof-shell-quit-cmd 1491,55297
-(defcustom proof-shell-quit-timeout 1496,55464
-(defcustom proof-shell-cd-cmd 1506,55912
-(defcustom proof-shell-start-silent-cmd 1523,56577
-(defcustom proof-shell-stop-silent-cmd 1532,56951
-(defcustom proof-shell-silent-threshold 1541,57284
-(defcustom  proof-shell-inform-file-processed-cmd 1549,57618
-(defcustom  proof-shell-inform-file-retracted-cmd 1570,58540
-(defcustom proof-auto-multiple-files 1598,59806
-(defcustom proof-cannot-reopen-processed-files 1613,60527
-(defcustom proof-shell-require-command-regexp 1627,61193
-(defcustom proof-done-advancing-require-function 1638,61655
-(defcustom proof-shell-quiet-errors 1644,61890
-(defcustom proof-shell-prompt-pattern 1657,62224
-(defcustom proof-shell-wakeup-char 1667,62645
-(defcustom proof-shell-annotated-prompt-regexp 1673,62876
-(defcustom proof-shell-abort-goal-regexp 1689,63510
-(defcustom proof-shell-error-regexp 1694,63645
-(defcustom proof-shell-truncate-before-error 1714,64439
-(defcustom pg-next-error-regexp 1728,64982
-(defcustom pg-next-error-filename-regexp 1743,65591
-(defcustom pg-next-error-extract-filename 1767,66624
-(defcustom proof-shell-interrupt-regexp 1774,66867
-(defcustom proof-shell-proof-completed-regexp 1788,67458
-(defcustom proof-shell-clear-response-regexp 1801,67966
-(defcustom proof-shell-clear-goals-regexp 1808,68265
-(defcustom proof-shell-start-goals-regexp 1815,68558
-(defcustom proof-shell-end-goals-regexp 1823,68925
-(defcustom proof-shell-eager-annotation-start 1829,69167
-(defcustom proof-shell-eager-annotation-start-length 1852,70187
-(defcustom proof-shell-eager-annotation-end 1863,70613
-(defcustom proof-shell-assumption-regexp 1879,71288
-(defcustom proof-shell-process-file 1889,71691
-(defcustom proof-shell-retract-files-regexp 1911,72647
-(defcustom proof-shell-compute-new-files-list 1920,72983
-(defcustom pg-use-specials-for-fontify 1932,73531
-(defcustom pg-special-char-regexp 1940,73879
-(defcustom proof-shell-set-elisp-variable-regexp 1946,74024
-(defcustom proof-shell-match-pgip-cmd 1979,75535
-(defcustom proof-shell-issue-pgip-cmd 1988,75864
-(defcustom proof-shell-query-dependencies-cmd 1997,76220
-(defcustom proof-shell-theorem-dependency-list-regexp 2004,76480
-(defcustom proof-shell-theorem-dependency-list-split 2020,77140
-(defcustom proof-shell-show-dependency-cmd 2029,77563
-(defcustom proof-shell-identifier-under-mouse-cmd 2036,77832
-(defcustom proof-shell-trace-output-regexp 2059,78913
-(defcustom proof-shell-thms-output-regexp 2073,79371
-(defcustom proof-shell-unicode 2086,79757
-(defcustom proof-shell-filename-escapes 2094,80077
-(defcustom proof-shell-process-connection-type2111,80757
-(defcustom proof-shell-strip-crs-from-input 2134,81803
-(defcustom proof-shell-strip-crs-from-output 2146,82288
-(defcustom proof-shell-insert-hook 2154,82656
-(defcustom proof-shell-handle-delayed-output-hook2194,84615
-(defcustom proof-shell-handle-error-or-interrupt-hook2200,84830
-(defcustom proof-shell-pre-interrupt-hook2218,85579
-(defcustom proof-shell-process-output-system-specific 2226,85851
-(defcustom proof-state-change-hook 2245,86715
-(defcustom proof-shell-font-lock-keywords 2256,87097
-(defcustom proof-shell-syntax-table-entries 2264,87429
-(defgroup proof-goals 2282,87801
-(defcustom pg-subterm-first-special-char 2287,87922
-(defcustom pg-subterm-anns-use-stack 2295,88234
-(defcustom pg-goals-change-goal 2304,88533
-(defcustom pbp-goal-command 2309,88649
-(defcustom pbp-hyp-command 2314,88805
-(defcustom pg-subterm-help-cmd 2319,88967
-(defcustom pg-goals-error-regexp 2326,89203
-(defcustom proof-shell-result-start 2331,89363
-(defcustom proof-shell-result-end 2337,89597
-(defcustom pg-subterm-start-char 2343,89810
-(defcustom pg-subterm-sep-char 2357,90390
-(defcustom pg-subterm-end-char 2363,90569
-(defcustom pg-topterm-regexp 2369,90726
-(defcustom proof-goals-font-lock-keywords 2386,91328
-(defcustom proof-resp-font-lock-keywords 2400,92013
-(defcustom pg-before-fontify-output-hook 2412,92593
-(defcustom pg-after-fontify-output-hook 2420,92953
-(defgroup proof-x-symbol 2432,93233
-(defcustom proof-xsym-extra-modes 2437,93361
-(defcustom proof-xsym-font-lock-keywords 2450,93989
-(defcustom proof-xsym-activate-command 2458,94366
-(defcustom proof-xsym-deactivate-command 2465,94601
-(defcustom proof-general-name 2482,94886
-(defcustom proof-general-home-page2487,95043
-(defcustom proof-unnamed-theorem-name2493,95203
-(defcustom proof-universal-keys2499,95387
+(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
 
 generic/proof-depends.el,824
 (defvar proof-thm-names-of-files 23,624
@@ -1778,10 +1654,10 @@ generic/proof-depends.el,824
 (defun proof-dep-unhighlight 253,8794
 
 generic/proof-easy-config.el,192
-(defconst proof-easy-config-derived-modes-table16,543
-(defun proof-easy-config-define-derived-modes 23,949
-(defun proof-easy-config-check-setup 56,2359
-(defmacro proof-easy-config 88,3694
+(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
 
 generic/proof-indent.el,219
 (defun proof-indent-indent 14,411
@@ -1792,667 +1668,592 @@ generic/proof-indent.el,219
 (defun proof-indent-line 76,2639
 
 generic/proof-maths-menu.el,83
-(defun proof-maths-menu-set-global 31,994
-(defun proof-maths-menu-enable 45,1450
-
-generic/proof-menu.el,2101
-(defvar proof-display-some-buffers-count 17,437
-(defun proof-display-some-buffers 19,482
-(defun proof-menu-define-keys 78,2684
-(defun proof-menu-define-main 141,5720
-(defvar proof-menu-favourites 150,5908
-(defun proof-menu-define-specific 154,6030
-(defun proof-assistant-menu-update 192,7056
-(defvar proof-help-menu208,7639
-(defvar proof-show-hide-menu216,7917
-(defvar proof-buffer-menu225,8230
-(defun proof-keep-response-history 288,10496
-(defconst proof-quick-opts-menu296,10806
-(defun proof-quick-opts-vars 449,16899
-(defun proof-quick-opts-changed-from-defaults-p 475,17691
-(defun proof-quick-opts-changed-from-saved-p 479,17796
-(defun proof-quick-opts-save 490,18148
-(defun proof-quick-opts-reset 495,18316
-(defconst proof-config-menu507,18584
-(defconst proof-advanced-menu514,18763
-(defvar proof-menu 527,19198
-(defun proof-main-menu 536,19482
-(defun proof-aux-menu 547,19748
-(defun proof-menu-define-favourites-menu 563,20095
-(defun proof-def-favourite 583,20751
-(defvar proof-make-favourite-cmd-history 606,21726
-(defvar proof-make-favourite-menu-history 609,21811
-(defun proof-save-favourites 612,21897
-(defun proof-del-favourite 617,22045
-(defun proof-read-favourite 634,22606
-(defun proof-add-favourite 659,23409
-(defvar proof-menu-settings 686,24460
-(defun proof-menu-define-settings-menu 689,24534
-(defun proof-menu-entry-name 709,25278
-(defun proof-menu-entry-for-setting 721,25750
-(defun proof-settings-vars 739,26240
-(defun proof-settings-changed-from-defaults-p 744,26417
-(defun proof-settings-changed-from-saved-p 748,26523
-(defun proof-settings-save 752,26626
-(defun proof-settings-reset 757,26793
-(defun proof-defpacustom-fn 764,27038
-(defmacro defpacustom 840,29922
-(defun proof-assistant-invisible-command-ifposs 855,30749
-(defun proof-maybe-askprefs 877,31724
-(defun proof-assistant-settings-cmd 884,31928
-(defvar proof-assistant-format-table 901,32588
-(defun proof-assistant-format-bool 909,32957
-(defun proof-assistant-format-int 912,33070
-(defun proof-assistant-format-string 915,33162
-(defun proof-assistant-format 918,33260
+(defun proof-maths-menu-set-global 30,962
+(defun proof-maths-menu-enable 44,1418
+
+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
 
 generic/proof-mmm.el,70
 (defun proof-mmm-set-global 41,1516
 (defun proof-mmm-enable 56,2057
 
-generic/proof-script.el,5112
-(defvar proof-element-counters 28,718
-(deflocal proof-active-buffer-fake-minor-mode 34,858
-(deflocal proof-script-buffer-file-name 37,984
-(deflocal pg-script-portions 44,1394
-(defun proof-next-element-count 54,1630
-(defun proof-element-id 63,1957
-(defun proof-next-element-id 67,2126
-(deflocal proof-script-last-entity 81,2443
-(defun proof-script-find-next-entity 88,2723
-(deflocal proof-locked-span 164,5465
-(deflocal proof-queue-span 171,5731
-(defun proof-span-read-only 183,6245
-(defun proof-strict-read-only 190,6502
-(defsubst proof-set-locked-endpoints 219,7693
-(defsubst proof-detach-queue 223,7837
-(defsubst proof-detach-locked 227,7969
-(defsubst proof-set-queue-start 231,8105
-(defsubst proof-set-locked-end 235,8231
-(defsubst proof-set-queue-end 248,8716
-(defun proof-init-segmentation 259,9013
-(defun proof-restart-buffers 292,10408
-(defun proof-script-buffers-with-spans 314,11340
-(defun proof-script-remove-all-spans-and-deactivate 324,11696
-(defun proof-script-clear-queue-spans 328,11884
-(defun proof-unprocessed-begin 347,12445
-(defun proof-script-end 355,12699
-(defun proof-queue-or-locked-end 364,13000
-(defun proof-locked-end 379,13678
-(defun proof-locked-region-full-p 396,14063
-(defun proof-locked-region-empty-p 405,14335
-(defun proof-only-whitespace-to-locked-region-p 409,14485
-(defun proof-in-locked-region-p 422,15121
-(defun proof-goto-end-of-locked 434,15384
-(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 451,16143
-(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 462,16624
-(defun proof-end-of-locked-visible-p 476,17277
-(defun proof-goto-end-of-queue-or-locked-if-not-visible 485,17728
-(defvar pg-idioms 504,18378
-(defvar pg-visibility-specs 507,18474
-(defconst pg-default-invisibility-spec 512,18681
-(defun pg-clear-script-portions 516,18821
-(defun pg-add-script-element 530,19298
-(defun pg-remove-script-element 533,19374
-(defsubst pg-visname 541,19652
-(defun pg-add-element 545,19797
-(defun pg-open-invisible-span 579,21426
-(defun pg-remove-element 590,21789
-(defun pg-make-element-invisible 597,22059
-(defun pg-make-element-visible 603,22316
-(defun pg-toggle-element-visibility 608,22495
-(defun pg-redisplay-for-gnuemacs 616,22825
-(defun pg-show-all-portions 623,23096
-(defun pg-show-all-proofs 641,23767
-(defun pg-hide-all-proofs 646,23895
-(defun pg-add-proof-element 651,24026
-(defun pg-span-name 665,24646
-(defvar pg-span-context-menu-keymap686,25353
-(defun pg-set-span-helphighlights 699,25724
-(defun proof-complete-buffer-atomic 727,26653
-(defun proof-register-possibly-new-processed-file 768,28568
-(defun proof-inform-prover-file-retracted 819,30696
-(defun proof-auto-retract-dependencies 838,31482
-(defun proof-unregister-buffer-file-name 892,34022
-(defun proof-protected-process-or-retract 938,35845
-(defun proof-deactivate-scripting-auto 965,37015
-(defun proof-deactivate-scripting 974,37373
-(defun proof-activate-scripting 1111,42778
-(defun proof-toggle-active-scripting 1233,48210
-(defun proof-done-advancing 1274,49571
-(defun proof-done-advancing-comment 1369,53219
-(defun proof-done-advancing-save 1388,53961
-(defun proof-make-goalsave 1481,57576
-(defun proof-get-name-from-goal 1496,58319
-(defun proof-done-advancing-autosave 1515,59345
-(defun proof-done-advancing-other 1580,61891
-(defun proof-segment-up-to-parser 1608,62850
-(defun proof-script-generic-parse-find-comment-end 1671,64926
-(defun proof-script-generic-parse-cmdend 1680,65342
-(defun proof-script-generic-parse-cmdstart 1705,66237
-(defun proof-script-generic-parse-sexp 1768,68945
-(defun proof-cmdstart-add-segment-for-cmd 1792,69881
-(defun proof-segment-up-to-cmdstart 1844,72080
-(defun proof-segment-up-to-cmdend 1905,74440
-(defun proof-semis-to-vanillas 1977,77105
-(defun proof-script-new-command-advance 2016,78431
-(defun proof-script-next-command-advance 2058,80172
-(defun proof-assert-until-point-interactive 2070,80613
-(defun proof-assert-until-point 2096,81735
-(defun proof-assert-next-command2149,84167
-(defun proof-goto-point 2197,86430
-(defun proof-insert-pbp-command 2215,86971
-(defun proof-insert-sendback-command 2229,87440
-(defun proof-done-retracting 2255,88330
-(defun proof-setup-retract-action 2291,89816
-(defun proof-last-goal-or-goalsave 2301,90299
-(defun proof-retract-target 2324,91139
-(defun proof-retract-until-point-interactive 2409,94780
-(defun proof-retract-until-point 2417,95165
-(define-derived-mode proof-mode 2460,96914
-(defun proof-script-set-visited-file-name 2510,98841
-(defun proof-script-set-buffer-hooks 2534,99843
-(defun proof-script-kill-buffer-fn 2542,100261
-(defun proof-config-done-related 2586,102083
-(defun proof-generic-goal-command-p 2656,104561
-(defun proof-generic-state-preserving-p 2661,104773
-(defun proof-generic-count-undos 2670,105290
-(defun proof-generic-find-and-forget 2699,106320
-(defconst proof-script-important-settings2750,108145
-(defun proof-config-done 2765,108698
-(defun proof-setup-parsing-mechanism 2853,111816
-(defun proof-setup-imenu 2897,113669
-(defun proof-setup-func-menu 2914,114274
-
-generic/proof-shell.el,3314
-(defvar proof-marker 28,649
-(defvar proof-action-list 31,746
-(defvar proof-shell-silent 39,922
-(defvar proof-shell-last-prompt 46,1213
-(defvar proof-shell-last-output-kind 50,1384
-(defvar proof-shell-delayed-output 71,2206
-(defvar proof-shell-delayed-output-kind 74,2327
-(defcustom proof-shell-active-scripting-indicator83,2530
-(defun proof-shell-ready-prover 135,3998
-(defun proof-shell-live-buffer 149,4538
-(defun proof-shell-available-p 156,4773
-(defun proof-grab-lock 162,4996
-(defun proof-release-lock 179,5708
-(defcustom proof-shell-fiddle-frames 199,6259
-(defun proof-shell-set-text-representation 205,6482
-(defun proof-shell-start 216,6944
-(defvar proof-shell-kill-function-hooks 426,14491
-(defun proof-shell-kill-function 429,14589
-(defun proof-shell-clear-state 518,18392
-(defun proof-shell-exit 533,18835
-(defun proof-shell-bail-out 545,19280
-(defun proof-shell-restart 554,19757
-(defvar proof-shell-no-response-display 596,21141
-(defvar proof-shell-urgent-message-marker 599,21245
-(defvar proof-shell-urgent-message-scanner 602,21366
-(defun proof-shell-handle-output 606,21493
-(defun proof-shell-handle-delayed-output 649,23186
-(defvar proof-shell-no-error-display 677,24229
-(defun proof-shell-handle-error 683,24433
-(defun proof-shell-handle-interrupt 701,25269
-(defun proof-shell-error-or-interrupt-action 715,25882
-(defun proof-goals-pos 740,27027
-(defun proof-pbp-focus-on-first-goal 745,27232
-(defsubst proof-shell-string-match-safe 757,27762
-(defun proof-shell-process-output 762,27930
-(defconst proof-shell-insert-space-fudge 873,32570
-(defun proof-shell-insert 885,32922
-(defun proof-shell-command-queue-item 958,35874
-(defun proof-shell-set-silent 963,36031
-(defun proof-shell-start-silent-item 969,36250
-(defun proof-shell-clear-silent 975,36442
-(defun proof-shell-stop-silent-item 981,36664
-(defun proof-shell-should-be-silent 988,36936
-(defun proof-append-alist 1001,37492
-(defun proof-start-queue 1060,39729
-(defun proof-extend-queue 1071,40078
-(defun proof-shell-exec-loop 1080,40457
-(defun proof-shell-insert-loopback-cmd 1145,43045
-(defun proof-shell-message 1173,44371
-(defun proof-shell-process-urgent-message 1179,44587
-(defun proof-shell-strip-eager-annotations 1311,49852
-(defvar proof-shell-minibuffer-urgent-interactive-input-history 1322,50188
-(defun proof-shell-minibuffer-urgent-interactive-input 1324,50258
-(defun proof-shell-process-urgent-messages 1334,50617
-(defun proof-shell-filter 1408,53721
-(defun proof-shell-filter-process-output 1569,60354
-(defvar pg-last-tracing-output-time 1622,62408
-(defconst pg-slow-mode-duration 1625,62514
-(defconst pg-fast-tracing-mode-threshold 1628,62596
-(defvar pg-tracing-cleanup-timer 1631,62724
-(defun pg-tracing-tight-loop 1633,62763
-(defun pg-finish-tracing-display 1676,64481
-(defun proof-shell-dont-show-annotations 1689,64787
-(defun proof-shell-show-annotations 1705,65308
-(defun proof-shell-wait 1727,65835
-(defun proof-done-invisible 1746,66744
-(defun proof-shell-invisible-command 1752,66916
-(defun proof-shell-invisible-cmd-get-result 1786,68181
-(defun proof-shell-invisible-command-invisible-result 1804,68877
-(define-derived-mode proof-shell-mode 1823,69307
-(defconst proof-shell-important-settings1893,71973
-(defun proof-shell-config-done 1899,72088
+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
+
+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
 
 generic/proof-site.el,504
-(defconst proof-assistant-table-default23,728
-(defconst proof-general-short-version 61,2156
-(defconst proof-general-version-year 67,2344
-(defgroup proof-general 74,2497
-(defgroup proof-general-internals 79,2605
-(defun proof-home-directory-fn 92,2993
-(defcustom proof-home-directory103,3364
-(defcustom proof-images-directory112,3731
-(defcustom proof-info-directory118,3933
-(defcustom proof-assistant-table145,5079
-(defcustom proof-assistants 180,6195
-(defun proof-ready-for-assistant 208,7340
-
-generic/proof-splash.el,726
-(defcustom proof-splash-enable 17,319
-(defcustom proof-splash-time 22,471
-(defcustom proof-splash-contents30,756
-(defconst proof-splash-startup-msg 58,1775
-(defconst proof-splash-welcome 67,2154
-(defun proof-get-image 86,2701
-(defvar proof-splash-timeout-conf 125,4052
-(defun proof-splash-centre-spaces 128,4165
-(defun proof-splash-remove-screen 156,5335
-(defun proof-splash-remove-buffer 176,6056
-(defvar proof-splash-seen 192,6720
-(defun proof-splash-display-screen 196,6837
-(defun proof-splash-message 271,9991
-(defun proof-splash-timeout-waiter 284,10435
-(defvar proof-splash-old-frame-title-format 300,11131
-(defun proof-splash-set-frame-titles 302,11181
-(defun proof-splash-unset-frame-titles 311,11497
+(defconst proof-assistant-table-default22,727
+(defconst proof-general-short-version 60,2143
+(defconst proof-general-version-year 66,2331
+(defgroup proof-general 73,2484
+(defgroup proof-general-internals 78,2592
+(defun proof-home-directory-fn 91,2980
+(defcustom proof-home-directory102,3351
+(defcustom proof-images-directory111,3718
+(defcustom proof-info-directory117,3920
+(defcustom proof-assistant-table145,5107
+(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-syntax.el,981
 (defun proof-ids-to-regexp 15,435
-(defun proof-anchor-regexp 21,711
-(defconst proof-no-regexp25,813
-(defun proof-regexp-alt 30,906
-(defun proof-regexp-region 39,1192
-(defun proof-re-search-forward-region 48,1615
-(defun proof-search-forward 61,2110
-(defun proof-replace-regexp-in-string 67,2362
-(defun proof-re-search-forward 73,2616
-(defun proof-re-search-backward 79,2877
-(defun proof-string-match 85,3141
-(defun proof-string-match-safe 91,3373
-(defun proof-stringfn-match 95,3578
-(defun proof-looking-at 102,3838
-(defun proof-looking-at-safe 108,4028
-(defun proof-looking-at-syntactic-context 112,4168
-(defsubst proof-replace-string 124,4531
-(defsubst proof-replace-regexp 129,4735
-(defsubst proof-replace-regexp-nocasefold 134,4944
-(defvar proof-id 142,5226
-(defun proof-ids 148,5446
-(defun proof-zap-commas 161,6002
-(defun proof-format 179,6571
-(defun proof-format-filename 198,7210
-(defun proof-insert 247,8681
-(defun proof-splice-separator 284,9697
-
-generic/proof-toolbar.el,2874
-(defun proof-toolbar-function 42,1325
-(defun proof-toolbar-icon 45,1422
-(defun proof-toolbar-enabler 48,1523
-(defun proof-toolbar-function-with-enabler 51,1631
-(defun proof-toolbar-make-icon 58,1804
-(defun proof-toolbar-make-toolbar-item 76,2404
-(defvar proof-toolbar 115,3780
-(deflocal proof-toolbar-itimer 119,3909
-(defun proof-toolbar-setup 123,4019
-(defun proof-toolbar-build 166,5562
-(defalias 'proof-toolbar-enable proof-toolbar-enable
230,7673
-(defun proof-toolbar-setup-refresh 241,7977
-(defun proof-toolbar-disable-refresh 262,8798
-(deflocal proof-toolbar-refresh-flag 270,9188
-(defun proof-toolbar-refresh 276,9459
-(defvar proof-toolbar-enablers280,9604
-(defvar proof-toolbar-enablers-last-state286,9780
-(defun proof-toolbar-really-refresh 290,9871
-(defun proof-toolbar-undo-enable-p 345,11765
-(defalias 'proof-toolbar-undo proof-toolbar-undo
350,11913
-(defun proof-toolbar-delete-enable-p 356,12032
-(defalias 'proof-toolbar-delete proof-toolbar-delete
362,12206
-(defun proof-toolbar-lockedend-enable-p 369,12342
-(defalias 'proof-toolbar-lockedend proof-toolbar-lockedend
372,12392
-(defun proof-toolbar-next-enable-p 381,12480
-(defalias 'proof-toolbar-next proof-toolbar-next
385,12587
-(defun proof-toolbar-goto-enable-p 392,12681
-(defalias 'proof-toolbar-goto proof-toolbar-goto
395,12754
-(defun proof-toolbar-retract-enable-p 402,12830
-(defalias 'proof-toolbar-retract proof-toolbar-retract
406,12941
-(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p
413,13020
-(defalias 'proof-toolbar-use proof-toolbar-use
414,13088
-(defun proof-toolbar-restart-enable-p 420,13166
-(defalias 'proof-toolbar-restart proof-toolbar-restart
425,13327
-(defun proof-toolbar-goal-enable-p 431,13405
-(defalias 'proof-toolbar-goal proof-toolbar-goal
438,13638
-(defun proof-toolbar-qed-enable-p 445,13710
-(defalias 'proof-toolbar-qed proof-toolbar-qed
451,13862
-(defun proof-toolbar-state-enable-p 457,13934
-(defalias 'proof-toolbar-state proof-toolbar-state
460,14005
-(defun proof-toolbar-context-enable-p 466,14074
-(defalias 'proof-toolbar-context proof-toolbar-context
469,14147
-(defun proof-toolbar-info-enable-p 477,14307
-(defalias 'proof-toolbar-info proof-toolbar-info
480,14351
-(defun proof-toolbar-command-enable-p 486,14420
-(defalias 'proof-toolbar-command proof-toolbar-command
489,14491
-(defun proof-toolbar-help-enable-p 495,14571
-(defun proof-toolbar-help 498,14616
-(defun proof-toolbar-find-enable-p 506,14710
-(defalias 'proof-toolbar-find proof-toolbar-find
509,14779
-(defun proof-toolbar-visibility-enable-p 515,14877
-(defalias 'proof-toolbar-visibility proof-toolbar-visibility
518,14977
-(defun proof-toolbar-interrupt-enable-p 524,15065
-(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt
527,15129
-(defun proof-toolbar-make-menu-item 536,15318
-(defun proof-toolbar-scripting-menu 559,16018
-
-generic/proof-unicode-tokens.el,476
-(defvar proof-unicode-tokens-initialised 17,496
-(defun proof-unicode-tokens-init 20,603
-(defun proof-unicode-tokens-enable 43,1231
-(defun proof-unicode-tokens-set-global 57,1851
-(defun proof-token-name-alist 76,2512
-(defun proof-shortcut-alist 91,3164
-(defun proof-unicode-tokens-activate-prover 103,3501
-(defun proof-unicode-tokens-deactivate-prover 110,3744
-(defun proof-unicode-tokens-shell-config 121,4176
-(defun proof-unicode-tokens-encode-shell-input 131,4573
-
-generic/proof-utils.el,2116
-(defmacro deflocal 63,1874
-(defmacro proof-with-current-buffer-if-exists 70,2112
-(deflocal proof-buffer-type 76,2322
-(defmacro proof-with-script-buffer 82,2602
-(defmacro proof-map-buffers 93,2989
-(defmacro proof-sym 98,3174
-(defsubst proof-try-require 103,3335
-(defun proof-save-some-buffers 116,3666
-(defmacro proof-ass-sym 165,5267
-(defmacro proof-ass-symv 171,5526
-(defmacro proof-ass 177,5784
-(defun proof-defpgcustom-fn 183,6036
-(defun undefpgcustom 204,6907
-(defmacro defpgcustom 210,7131
-(defun proof-defpgdefault-fn 221,7549
-(defmacro defpgdefault 235,8007
-(defmacro defpgfun 246,8369
-(defmacro proof-eval-when-ready-for-assistant 256,8634
-(defun proof-file-truename 269,9029
-(defun proof-file-to-buffer 273,9212
-(defun proof-files-to-buffers 284,9541
-(defun proof-buffers-in-mode 291,9824
-(defun pg-save-from-death 305,10274
-(defun proof-define-keys 324,10891
-(deflocal proof-font-lock-keywords 353,11890
-(defun proof-font-lock-configure-defaults 359,12147
-(defun proof-font-lock-clear-font-lock-vars 405,14298
-(defun proof-font-lock-set-font-lock-vars 411,14510
-(defun proof-fontify-region 415,14666
-(defun pg-remove-specials 477,17068
-(defun pg-remove-specials-in-string 487,17406
-(defun proof-fontify-buffer 494,17593
-(defun proof-warn-if-unset 507,17834
-(defun proof-get-window-for-buffer 512,18052
-(defun proof-display-and-keep-buffer 563,20360
-(defun proof-clean-buffer 595,21667
-(defun proof-message 610,22288
-(defun proof-warning 615,22501
-(defun pg-internal-warning 621,22783
-(defun proof-debug 629,23102
-(defun proof-switch-to-buffer 644,23773
-(defun proof-resize-window-tofit 677,25462
-(defun proof-submit-bug-report 777,29474
-(defun proof-deftoggle-fn 813,30853
-(defmacro proof-deftoggle 828,31506
-(defun proof-defintset-fn 835,31880
-(defmacro proof-defintset 851,32584
-(defun proof-defstringset-fn 858,32961
-(defmacro proof-defstringset 871,33587
-(defmacro proof-defshortcut 885,34044
-(defmacro proof-definvisible 900,34683
-(defun pg-custom-save-vars 928,35660
-(defun pg-custom-reset-vars 946,36383
-(defun proof-locate-executable 959,36720
-
-generic/proof-x-symbol.el,580
-(defvar proof-x-symbol-initialized 52,2005
-(defun proof-x-symbol-tokenlang-file 55,2100
-(defun proof-x-symbol-support-maybe-available 61,2282
-(defun proof-x-symbol-initialize 81,3011
-(defun proof-x-symbol-enable 164,6277
-(defun proof-x-symbol-refresh-output-buffers 186,7158
-(defun proof-x-symbol-mode-associated-buffers 201,7900
-(defun proof-x-symbol-decode-region 219,8438
-(defun proof-x-symbol-encode-shell-input 240,9435
-(defun proof-x-symbol-set-language 257,10026
-(defun proof-x-symbol-shell-config 262,10197
-(defun proof-x-symbol-config-output-buffer 311,12443
-
-lib/bufhist.el,1100
-(defun bufhist-ring-update 32,1226
-(defgroup bufhist 41,1548
-(defcustom bufhist-ring-size 45,1629
-(defvar bufhist-ring 50,1740
-(defvar bufhist-ring-pos 53,1814
-(defvar bufhist-lastswitch-modified-tick 56,1893
-(defvar bufhist-read-only-history 59,1999
-(defvar bufhist-saved-mode-line-format 62,2070
-(defun bufhist-mode-line-format-entry 65,2171
-(defun bufhist-get-buffer-contents 101,3514
-(defun bufhist-restore-buffer-contents 113,3998
-(defun bufhist-checkpoint 121,4285
-(defun bufhist-erase-buffer 129,4654
-(defun bufhist-checkpoint-and-erase 139,4999
-(defun bufhist-switch-to-index 145,5185
-(defun bufhist-first 184,6789
-(defun bufhist-last 189,6948
-(defun bufhist-prev 194,7094
-(defun bufhist-next 202,7317
-(defun bufhist-delete 207,7457
-(defun bufhist-clear 219,8000
-(defun bufhist-init 234,8396
-(defun bufhist-exit 259,9333
-(defun bufhist-set-readwrite 269,9597
-(defun bufhist-before-change-function 284,10217
-(defun bufhist-make-buttons 296,10633
-(defconst bufhist-minor-mode-map314,11072
-(define-minor-mode bufhist-mode326,11534
-(defun bufhist-toggle-fn 346,12319
-
-lib/holes.el,2448
-(defvar holes-doc 37,1050
-(defvar holes-default-hole 145,5033
-(defvar holes-active-hole 149,5202
-(defcustom holes-empty-hole-string 156,5411
-(defcustom holes-empty-hole-regexp 159,5522
-(defcustom holes-search-limit 166,5813
-(defface active-hole-face178,6189
-(defface inactive-hole-face190,6637
-(defun holes-region-beginning-or-nil 205,7113
-(defun holes-region-end-or-nil 210,7223
-(defun holes-copy-active-region 215,7321
-(defun holes-is-hole-p 222,7520
-(defun holes-hole-start-position 228,7627
-(defun holes-hole-end-position 235,7816
-(defun holes-hole-buffer 242,8000
-(defun holes-hole-at 249,8175
-(defun holes-active-hole-exist-p 256,8350
-(defun holes-active-hole-start-position 266,8608
-(defun holes-active-hole-end-position 276,8980
-(defun holes-active-hole-buffer 287,9349
-(defun holes-goto-active-hole 298,9655
-(defun holes-highlight-hole-as-active 310,9923
-(defun holes-highlight-hole 320,10235
-(defun holes-disable-active-hole 331,10527
-(defun holes-set-active-hole 349,11070
-(defun holes-is-in-hole-p 362,11416
-(defun holes-make-hole 369,11559
-(defun holes-make-hole-at 395,12305
-(defun holes-clear-hole 415,12781
-(defun holes-clear-hole-at 427,13070
-(defun holes-map-holes 436,13329
-(defun holes-mapcar-holes 444,13512
-(defun holes-clear-all-buffer-holes 450,13684
-(defun holes-next 461,13984
-(defun holes-next-after-active-hole 468,14235
-(defun holes-set-active-hole-next 476,14454
-(defun holes-replace-segment 498,15007
-(defun holes-replace 508,15361
-(defun holes-replace-active-hole 539,16556
-(defun holes-replace-update-active-hole 548,16857
-(defun holes-delete-update-active-hole 569,17547
-(defun holes-set-make-active-hole 576,17761
-(defun holes-mouse-replace-active-hole 623,19486
-(defun holes-destroy-hole 643,20025
-(defun holes-hole-at-event 660,20436
-(defun holes-mouse-destroy-hole 665,20549
-(defun holes-mouse-forget-hole 675,20789
-(defun holes-mouse-set-make-active-hole 691,21099
-(defun holes-mouse-set-active-hole 713,21660
-(defun holes-set-point-next-hole-destroy 725,21924
-(defvar hole-map741,22374
-(defvar holes-mode-map757,22994
-(defun holes-replace-string-by-holes-backward 794,24469
-(defun holes-skeleton-end-hook 812,25170
-(defconst holes-jump-doc 821,25608
-(defun holes-replace-string-by-holes-backward-jump 828,25815
-(defun holes-abbrev-complete 845,26446
-(defun holes-insert-and-expand 854,26753
-(defvar holes-mode 865,27185
-(defun holes-mode 871,27381
+(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
+
+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
+
+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
+
+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
+
+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
+
+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
 
 lib/local-vars-list.el,373
-(defconst local-vars-list-doc 28,829
-(defun local-vars-list-insert-empty-zone 44,1393
-(defun local-vars-list-find 82,2101
-(defun local-vars-list-goto-var 101,2876
-(defun local-vars-list-get-current 127,3926
-(defun local-vars-list-set-current 148,4776
-(defun local-vars-list-get 171,5493
-(defun local-vars-list-get-safe 188,6025
-(defun local-vars-list-set 193,6219
-
-lib/maths-menu.el,153
-(defun maths-menu-build-menu 51,2136
-(defvar maths-menu-menu70,2804
-(defvar maths-menu-mode-map315,11762
-(define-minor-mode maths-menu-mode323,11981
+(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
+
+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
 
 lib/pg-dev.el,75
-(defconst pg-dev-lisp-font-lock-keywords36,1102
-(defun unload-pg 70,2039
+(defconst pg-dev-lisp-font-lock-keywords36,1106
+(defun unload-pg 70,2043
 
 lib/pg-fontsets.el,176
-(defcustom pg-fontsets-default-fontset 23,682
-(defun pg-fontsets-make-fontsetsizes 28,828
-(defconst pg-fontsets-base-fonts 47,1612
-(defun pg-fontsets-make-fontsets 52,1717
-
-lib/proof-compat.el,751
-(defvar proof-running-on-win32 29,913
-(defun pg-custom-undeclare-variable 49,1708
-(defun subst-char-in-string 139,4496
-(defun replace-regexp-in-string 154,5085
-(defconst menuvisiblep 216,7798
-(defun set-window-text-height 233,8411
-(defmacro save-selected-frame 259,9361
-(defun warn 298,10658
-(defun redraw-modeline 305,10913
-(defun proof-buffer-syntactic-context-emulate 316,11351
-(defvar read-shell-command-map349,12658
-(defun read-shell-command 367,13346
-(defun remassq 379,13827
-(defun remassoc 391,14216
-(defun frames-of-buffer 404,14661
-(defmacro with-selected-window 443,15923
-(defun pg-pop-to-buffer 486,17301
-(defun process-live-p 537,19163
-(defalias 'proof-buffer-syntactic-context proof-buffer-syntactic-context
556,19778
-
-lib/span.el,137
-(defsubst span-delete-spans 22,479
-(defsubst span-property-safe 26,643
-(defsubst span-set-start 30,782
-(defsubst span-set-end 34,914
-
-lib/span-extent.el,1015
-(defsubst span-make 12,367
-(defsubst span-detach 16,489
-(defsubst span-set-endpoints 20,576
-(defsubst span-set-property 24,709
-(defsubst span-read-only 28,836
-(defsubst span-read-write 32,940
-(defun span-give-warning 36,1047
-(defun span-write-warning 40,1155
-(defsubst span-property 45,1355
-(defsubst span-delete 49,1470
-(defsubst span-mapcar-spans 55,1641
-(defsubst spans-at-region-prop 59,1852
-(defsubst span-at 63,2040
-(defsubst span-at-before 67,2157
-(defsubst span-start 72,2354
-(defsubst span-end 76,2483
-(defsubst prev-span 80,2606
-(defsubst next-span 84,2752
-(defsubst span-live-p 88,2894
-(defun span-raise 96,3166
-(defalias 'span-object span-object
100,3265
-(defalias 'span-string span-string
101,3304
-(defsubst make-detached-span 104,3390
-(defsubst span-buffer 109,3452
-(defsubst span-detached-p 114,3544
-(defsubst set-span-face 119,3656
-(defsubst fold-spans 123,3751
-(defsubst set-span-properties 127,3948
-(defsubst set-span-keymap 131,4056
-(defsubst span-at-event 136,4200
-
-lib/span-overlay.el,1206
-(defalias 'span-start span-start
12,370
-(defalias 'span-end span-end
13,408
-(defalias 'span-set-property span-set-property
14,442
-(defalias 'span-property span-property
15,485
-(defalias 'span-make span-make
16,524
-(defalias 'span-detach span-detach
17,560
-(defalias 'span-set-endpoints span-set-endpoints
18,600
-(defalias 'span-buffer span-buffer
19,645
-(defun span-read-only-hook 21,686
-(defun span-read-only 25,818
-(defun span-read-write 40,1594
-(defun span-give-warning 46,1813
-(defun span-write-warning 50,1921
-(defun span-lt 57,2247
-(defun spans-at-point-prop 62,2388
-(defun spans-at-region-prop 68,2553
-(defun span-at 77,2865
-(defsubst span-delete 83,3079
-(defsubst span-mapcar-spans 90,3301
-(defun span-at-before 94,3510
-(defun prev-span 111,4236
-(defun next-span 117,4387
-(defsubst span-live-p 146,5612
-(defun span-raise 152,5778
-(defalias 'span-object span-object
158,6021
-(defun span-string 160,6062
-(defun set-span-properties 166,6244
-(defun span-find-span 178,6499
-(defsubst span-at-event 185,6806
-(defun make-detached-span 189,6927
-(defun fold-spans 194,7023
-(defsubst span-detached-p 209,7557
-(defsubst set-span-face 213,7672
-(defun set-span-keymap 217,7769
+(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
+
+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
+
+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
 
 lib/texi-docstring-magic.el,584
 (defun texi-docstring-magic-find-face 88,3034
@@ -2472,74 +2273,70 @@ lib/unicode-chars.el,80
 (defvar unicode-chars-alist12,348
 (defun unicode-chars-list-chars 5050,245960
 
-lib/unicode-tokens.el,2526
-(defvar unicode-tokens-charref-format 60,2307
-(defvar unicode-tokens-token-format 63,2404
-(defvar unicode-tokens-token-name-alist 66,2495
-(defvar unicode-tokens-glyph-list 69,2588
-(defvar unicode-tokens-token-prefix 73,2732
-(defvar unicode-tokens-token-suffix 76,2816
-(defvar unicode-tokens-control-token-match 79,2898
-(defvar unicode-tokens-token-match 82,2974
-(defvar unicode-tokens-hexcode-match 85,3057
-(defvar unicode-tokens-next-character-regexp 88,3165
-(defvar unicode-tokens-shortcut-alist91,3310
-(defface unicode-tokens-script-font-face107,3762
-(defface unicode-tokens-fraktur-font-face117,4027
-(defface unicode-tokens-serif-font-face127,4321
-(defvar unicode-tokens-max-token-length 142,4648
-(defvar unicode-tokens-codept-charname-alist 145,4747
-(defvar unicode-tokens-token-alist 148,4855
-(defvar unicode-tokens-ustring-alist 152,5016
-(defun unicode-tokens-insert-char 160,5119
-(defun unicode-tokens-insert-string 170,5540
-(defun unicode-tokens-character-insert 180,5917
-(defun unicode-tokens-token-insert 202,6825
-(defun unicode-tokens-replace-token-after 223,7722
-(defun unicode-tokens-looking-backward-at 245,8487
-(defun unicode-tokens-electric-suffix 259,9120
-(defvar unicode-tokens-rotate-glyph-last-char 306,10724
-(defun unicode-tokens-rotate-glyph-forward 308,10776
-(defun unicode-tokens-rotate-glyph-backward 337,11958
-(defun unicode-tokens-map-ordering 358,12565
-(defun unicode-tokens-propertise-after-quail 362,12715
-(defun unicode-tokens-quail-define-rules 367,12870
-(defvar unicode-tokens-format-entry431,15200
-(defconst unicode-tokens-ignored-properties441,15498
-(defconst unicode-tokens-annotation-translations449,15752
-(defun unicode-tokens-remove-properties 474,16731
-(defun unicode-tokens-tokens-to-unicode 482,17049
-(defvar unicode-tokens-next-control-token-seen-token 503,17898
-(defun unicode-tokens-next-control-token 506,18016
-(defconst unicode-tokens-annotation-control-token-alist 560,20100
-(defun unicode-tokens-make-token-annotation 575,20644
-(defun unicode-tokens-find-property 586,21082
-(defun unicode-tokens-annotate-region 600,21471
-(defun unicode-tokens-annotate-region-with 612,21879
-(defun unicode-tokens-annotate-string 617,22030
-(defun unicode-tokens-unicode-to-tokens 623,22198
-(defun unicode-tokens-replace-strings-propertise 643,22985
-(defun unicode-tokens-replace-strings-unpropertise 673,24235
-(defvar unicode-tokens-mode-map 702,24980
-(define-minor-mode unicode-tokens-mode705,25077
-(defun unicode-tokens-initialise 741,26455
-
-lib/xml-fixed.el,528
-(defsubst xml-node-name 82,2904
-(defsubst xml-node-attributes 87,3023
-(defsubst xml-node-children 92,3141
-(defun xml-get-children 97,3277
-(defun xml-get-attribute 107,3600
-(defun xml-parse-file 123,4064
-(defun xml-parse-region 144,4648
-(defun xml-parse-tag 179,5693
-(defun xml-parse-attlist 284,9162
-(defun xml-skip-dtd 321,10552
-(defun xml-parse-dtd 338,11188
-(defun xml-parse-elem-type 408,13266
-(defun xml-substitute-special 449,14421
-(defun xml-debug-print 470,15228
-(defun xml-debug-print-internal 474,15320
+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
 
 mmm/mmm-auto.el,343
 (defvar mmm-autoloaded-classes67,2675
@@ -2819,927 +2616,166 @@ mmm/mmm-vars.el,2667
 (defun mmm-mode-ext-applies 1023,38161
 (defun mmm-get-all-classes 1037,38645
 
-x-symbol/lisp/auto-autoloads.el,63
-(defalias 'x-symbol-map-autoload x-symbol-map-autoload
23,974
-
-x-symbol/lisp/x-symbol-autoloads.el,63
-(defalias 'x-symbol-map-autoload x-symbol-map-autoload
23,974
-
-x-symbol/lisp/x-symbol-bib.el,549
-(defcustom x-symbol-bib-auto-style 42,1544
-(defcustom x-symbol-bib-modeline-name 49,1800
-(defcustom x-symbol-bib-header-groups-alist 55,1979
-(defcustom x-symbol-bib-electric-ignore 62,2268
-(defcustom x-symbol-bib-class-alist 69,2558
-(defcustom x-symbol-bib-class-face-alist 76,2824
-(defvar x-symbol-bib-token-grammar89,3308
-(defvar x-symbol-bib-required-fonts 99,3784
-(defvar x-symbol-bib-user-table 103,3960
-(defvar x-symbol-bib-table106,4064
-(defvar x-symbol-bib-generated-data 113,4390
-(defun x-symbol-bib-default-token-list 117,4529
-
-x-symbol/lisp/x-symbol.el,9210
-(defvar x-symbol-trace-invisible 52,2014
-(defconst x-symbol-language-access-alist67,2529
-(defstruct (x-symbol-generated179,8410
-(defstruct (x-symbol-grammar190,8622
-(defvar x-symbol-map 213,9450
-(defvar x-symbol-unalias-alist 217,9577
-(defvar x-symbol-latin-decode-alists 221,9694
-(defvar x-symbol-context-atree 225,9879
-(defvar x-symbol-electric-atree 229,9994
-(defvar x-symbol-grid-alist 232,10088
-(defvar x-symbol-menu-alist 235,10171
-(defvar x-symbol-all-charsyms 238,10278
-(defvar x-symbol-fancy-value-cache 243,10486
-(defvar x-symbol-fchar-tables 247,10649
-(defvar x-symbol-bchar-tables 250,10778
-(defvar x-symbol-cstring-table 252,10814
-(defvar x-symbol-fontified-cstring-table 254,10851
-(defvar x-symbol-charsym-decode-obarray 256,10898
-(defun x-symbol-set-variable 263,11127
-(defun x-symbol-ensure-hashtable 277,11762
-(defun x-symbol-puthash 284,12064
-(defun x-symbol-call-function-or-regexp 292,12393
-(defun x-symbol-match-in-alist 301,12793
-(defun x-symbol-fancy-string 330,14017
-(defun x-symbol-fancy-value 352,14934
-(defun x-symbol-fancy-associations 371,15701
-(defun x-symbol-language-value 400,16853
-(defun x-symbol-charsym-face 414,17511
-(defun x-symbol-image-available-p 427,18138
-(defun x-symbol-default-context-info-ignore 432,18350
-(defun x-symbol-default-info-keys-keymaps 446,19117
-(defun x-symbol-alias-charsym 458,19592
-(defun x-symbol-default-valid-charsym 467,19961
-(defun x-symbol-next-valid-charsym 489,20998
-(defun x-symbol-valid-context-charsym 516,22005
-(defun x-symbol-next-valid-charsym-before 527,22604
-(defun x-symbol-prefix-arg-texts 551,23661
-(defun x-symbol-region-text 560,23956
-(defun x-symbol-language-text 569,24252
-(defun x-symbol-coding-text 577,24652
-(defun x-symbol-language-modeline-text 595,25347
-(defun x-symbol-coding-modeline-text 601,25583
-(defun x-symbol-translate-to-ascii 647,27488
-(defun x-symbol-package-web 681,28753
-(defun x-symbol-package-info 688,28974
-(defun x-symbol-package-bug 694,29135
-(defun x-symbol-package-reply-to-report 745,31108
-(defvar x-symbol-encode-rchars 765,31836
-(defun x-symbol-even-escapes-before-p 773,32118
-(defun x-symbol-decode-region 781,32297
-(defun x-symbol-decode-all 794,32770
-(defun x-symbol-decode-single-token 857,35838
-(defun x-symbol-decode-lisp 866,36145
-(defun x-symbol-encode-string 898,37612
-(defun x-symbol-encode-all 909,37931
-(defun x-symbol-encode-lisp 973,40966
-(defun x-symbol-decode-recode 1009,42371
-(defun x-symbol-decode 1039,43747
-(defun x-symbol-encode-recode 1052,44338
-(defun x-symbol-encode 1080,45614
-(defun x-symbol-unalias 1096,46373
-(defun x-symbol-copy-region-encoded 1161,49292
-(defun x-symbol-yank-decoded 1189,50542
-(defun x-symbol-update-modeline 1216,51642
-(defun x-symbol-auto-coding-alist 1240,52497
-(defun x-symbol-auto-8bit-search 1276,53658
-(defvar x-symbol-font-family-postfixes1301,54448
-(defvar x-symbol-font-lock-property-alist1304,54564
-(defvar x-symbol-font-lock-keywords1308,54745
-(defvar x-symbol-subscript-matcher 1335,55740
-(defvar x-symbol-subscript-type 1339,55843
-(defun x-symbol-subscripts-available-p 1342,55894
-(defun x-symbol-font-lock-start 1348,56135
-(defun x-symbol-match-subscript 1357,56521
-(defun x-symbol-init-font-lock 1363,56734
-(defun x-symbol-set-image 1395,58322
-(defun x-symbol-mode-internal 1413,59068
-(defun nuke-x-symbol 1487,62177
-(defun x-symbol-options-filter 1500,62630
-(defun x-symbol-extra-filter 1536,63786
-(defun x-symbol-menu-filter 1544,64034
-(defvar x-symbol-list-mode-map1574,65013
-(defvar x-symbol-list-buffer 1600,66163
-(defvar x-symbol-list-win-config 1602,66239
-(defvar x-symbol-invisible-spec 1604,66350
-(defvar x-symbol-itimer 1608,66500
-(defvar x-symbol-invisible-display-table1611,66583
-(defvar x-symbol-invisible-font 1620,66819
-(defvar x-symbol-charsym-info-cache 1645,68006
-(defvar x-symbol-language-info-caches 1647,68097
-(defvar x-symbol-coding-info-cache 1649,68191
-(defvar x-symbol-keys-info-cache 1651,68280
-(defun x-symbol-list-bury 1659,68585
-(defun x-symbol-list-restore 1665,68781
-(defun x-symbol-list-store 1695,69999
-(defun x-symbol-list-mode 1704,70416
-(defun x-symbol-list-scroll 1725,71218
-(defun x-symbol-init-language-interactive 1748,71860
-(defun x-symbol-list-menu 1765,72574
-(defun x-symbol-list-selected 1820,74482
-(defun x-symbol-list-menu-selected 1846,75691
-(defun x-symbol-list-mouse-selected 1857,76144
-(defun x-symbol-charsym-info 1874,76866
-(defun x-symbol-language-info 1888,77467
-(defun x-symbol-coding-info 1920,78667
-(defun x-symbol-keys-info 1940,79439
-(defun x-symbol-info 1964,80362
-(defun x-symbol-list-info 1977,80900
-(defun x-symbol-highlight-echo 1991,81443
-(defun x-symbol-point-info 2002,81992
-(defun x-symbol-hide-revealed-at-point 2048,83914
-(defun x-symbol-reveal-invisible 2085,85581
-(defun x-symbol-show-info-and-invisible 2133,87773
-(defun x-symbol-start-itimer-once 2169,89315
-(defun x-symbol-setup-minibuffer 2185,89941
-(defvar x-symbol-language-history 2203,90512
-(defvar x-symbol-token-history 2206,90636
-(defvar x-symbol-last-abbrev 2209,90712
-(defvar x-symbol-electric-pos 2211,90808
-(defvar x-symbol-command-keys 2214,90890
-(defvar x-symbol-help-keys 2218,91021
-(defvar x-symbol-help-language 2220,91116
-(defvar x-symbol-help-completions 2222,91215
-(defvar x-symbol-help-completions1 2224,91307
-(defun x-symbol-map-default-binding 2232,91583
-(defun x-symbol-read-charsym-token 2263,92661
-(defun x-symbol-insert-command 2289,93584
-(defun x-symbol-read-language 2340,95591
-(defun x-symbol-read-token 2355,96269
-(defun x-symbol-read-token-direct 2394,97778
-(defun x-symbol-grid 2406,98178
-(defun x-symbol-replace-from 2494,101794
-(defvar x-symbol-token-search-prelude-size 2530,103295
-(defun x-symbol-replace-token 2532,103343
-(defun x-symbol-match-token-before 2557,104434
-(defun x-symbol-token-input 2601,106237
-(defun x-symbol-modify-key 2622,107067
-(defun x-symbol-rotate-key 2655,108396
-(defun x-symbol-electric-input 2709,110606
-(defun x-symbol-help-mapper 2751,112307
-(defun x-symbol-help-output 2774,113146
-(defun x-symbol-help 2817,114742
-(defvar x-symbol-face-docstrings2870,116811
-(defvar x-symbol-all-key-prefixes 2876,116999
-(defvar x-symbol-all-key-chain-alist 2878,117110
-(defvar x-symbol-all-horizontal-chain-alist 2880,117209
-(defvar x-symbol-all-chain-subchains-alist 2882,117322
-(defvar x-symbol-all-exclusive-context-alist 2884,117436
-(defalias 'x-symbol-table-grouping x-symbol-table-grouping
2892,117732
-(defalias 'x-symbol-table-aspects x-symbol-table-aspects
2893,117773
-(defalias 'x-symbol-table-score x-symbol-table-score
2894,117814
-(defalias 'x-symbol-table-input x-symbol-table-input
2895,117854
-(defsubst x-symbol-table-prefixes 2896,117895
-(defsubst x-symbol-table-junk 2897,117946
-(defsubst x-symbol-charsym-defined-p 2899,117997
-(defun x-symbol-try-font-name-0 2907,118298
-(defun x-symbol-try-font-name 2925,118854
-(defun x-symbol-set-cstrings 2942,119370
-(defun x-symbol-init-charsym-command 2987,121348
-(defun x-symbol-init-charsym-input 2995,121714
-(defun x-symbol-init-charsym-aspects 3064,124432
-(defun x-symbol-init-cset 3094,125712
-(defun x-symbol-make-atree 3244,132535
-(defun x-symbol-atree-push 3248,132615
-(defun x-symbol-component-root-p 3268,133304
-(defun x-symbol-component-elements 3272,133443
-(defun x-symbol-component-merge 3279,133691
-(defun x-symbol-component-space 3293,134239
-(defun x-symbol-modify-less-than 3307,134823
-(defun x-symbol-inherit-aspects 3312,135046
-(defun x-symbol-compute-aspects 3321,135485
-(defun x-symbol-init-aspects 3337,136203
-(defun x-symbol-sort-modify-chain 3382,138252
-(defun x-symbol-init-horizontal/key-alist 3397,138824
-(defun x-symbol-init-exclusive-alist 3413,139570
-(defun x-symbol-init-horizontal-chain 3451,141174
-(defun x-symbol-init-exclusive-chain 3459,141506
-(defun x-symbol-init-rotate-chain 3466,141833
-(defun x-symbol-init-context-atree 3487,142707
-(defun x-symbol-init-key-bindings 3532,144990
-(defun x-symbol-rotate-modify-less-than 3555,145913
-(defun x-symbol-subgroup-less-than 3563,146308
-(defun x-symbol-header-charsyms 3568,146565
-(defun x-symbol-init-grid/menu 3594,147615
-(defun x-symbol-init-input 3666,150271
-(defun x-symbol-init-latin-decoding 3796,156747
-(defun x-symbol-get-prime-for 3837,158618
-(defun x-symbol-alist-to-obarray 3846,158942
-(defun x-symbol-alist-to-hash-table 3852,159150
-(defun x-symbol-init-language 3862,159483
-(defvar x-symbol-latin1-cset3986,164948
-(defvar x-symbol-latin2-cset3992,165121
-(defvar x-symbol-latin3-cset3998,165294
-(defvar x-symbol-latin5-cset4004,165467
-(defvar x-symbol-latin9-cset4010,165639
-(defvar x-symbol-xsymb0-cset4016,165845
-(defvar x-symbol-xsymb1-cset4022,166100
-(defvar x-symbol-latin1-table4028,166342
-(defvar x-symbol-latin2-table4129,170812
-(defvar x-symbol-latin3-table4228,174013
-(defvar x-symbol-latin5-table4334,177131
-(defvar x-symbol-latin9-table4433,179441
-(defvar x-symbol-xsymb0-table4532,181831
-(defvar x-symbol-xsymb1-table4682,189227
-(defvar x-symbol-no-of-charsyms 4890,199862
-(defun x-symbol-mac-setup1 4898,200228
-(defun x-symbol-mac-setup2 4919,201006
-(defun x-symbol-startup 4945,201872
-
-x-symbol/lisp/x-symbol-emacs.el,1126
-(defun emacs-version>=33,1289
-(defvar x-symbol-emacs-has-font-lock-with-props67,2953
-(defvar x-symbol-emacs-has-correct-find-safe-coding87,3682
-(defvar x-symbol-emacs-after-create-image-function102,4196
-(defvar image-types 128,5053
-(defvar init-file-loaded 164,6440
-(defvar message-stack 167,6513
-(defun region-active-p 250,9823
-(defvar x-symbol-data-directory 293,11359
-(defun x-symbol-directory-files 363,13636
-(defun x-symbol-event-in-current-buffer 377,14024
-(defun x-symbol-create-image 380,14073
-(defun x-symbol-make-glyph 383,14158
-(defun x-symbol-set-glyph-image 386,14229
-(defvar x-symbol-heading-strut-glyph 401,14726
-(defvar x-symbol-invisible-face 404,14813
-(defvar x-symbol-face 405,14871
-(defvar x-symbol-sub-face 406,14909
-(defvar x-symbol-sup-face 407,14955
-(defvar x-symbol-emacs-w32-font-directories409,15002
-(defvar x-symbol-invisible-display-table 422,15480
-(defalias 'x-symbol-window-width x-symbol-window-width
424,15527
-(defun x-symbol-set-face-font 429,15651
-(defun x-symbol-event-matches-key-specifier-p 453,16654
-(defun start-itimer 463,16926
-(defun itimer-live-p 465,17023
-
-x-symbol/lisp/x-symbol-hooks.el,3109
-(defvar x-symbol-warn-of-old-emacs 66,2522
-(defvar x-symbol-data-directory81,3030
-(defvar x-symbol-font-directory87,3246
-(defun x-symbol-define-user-options 98,3661
-(defun x-symbol-auto-mode-suffixes 126,5060
-(defcustom x-symbol-initialize 143,5652
-(defvar x-symbol-orig-comint-input-sender 177,7219
-(defun x-symbol-coding-system-from-locale 185,7531
-(defun x-symbol-buffer-coding 223,9137
-(defvar x-symbol-default-coding279,11196
-(defcustom x-symbol-compose-key 325,13040
-(defcustom x-symbol-auto-key-autoload 332,13308
-(defvar x-symbol-auto-conversion-method 340,13623
-(defvar x-symbol-language-alist 361,14586
-(defcustom x-symbol-charsym-name 370,14923
-(defcustom x-symbol-tex-name 378,15273
-(defcustom x-symbol-tex-modes384,15440
-(defcustom x-symbol-sgml-name 392,15708
-(defcustom x-symbol-sgml-modes398,15880
-(defcustom x-symbol-bib-name 407,16207
-(defcustom x-symbol-bib-modes 413,16377
-(defcustom x-symbol-texi-name 420,16603
-(defcustom x-symbol-texi-modes 426,16779
-(defvar x-symbol-mode 438,17188
-(defvar x-symbol-language 445,17415
-(defvar x-symbol-coding 460,18103
-(defvar x-symbol-8bits 487,19379
-(defvar x-symbol-unique 502,19965
-(defvar x-symbol-subscripts 517,20547
-(defvar x-symbol-image 530,21112
-(defcustom x-symbol-auto-mode-suffixes 547,21754
-(defcustom x-symbol-auto-8bit-search-limit 556,22179
-(defcustom x-symbol-auto-style-alist 563,22461
-(defvar x-symbol-mode-disable-alist 609,24419
-(defun x-symbol-image-set-colormap 617,24694
-(defcustom x-symbol-image-colormap-allocation 635,25402
-(defcustom x-symbol-image-convert-colormap646,25858
-(defalias 'x-symbol-cset-registry x-symbol-cset-registry
665,26545
-(defalias 'x-symbol-cset-coding x-symbol-cset-coding
666,26587
-(defalias 'x-symbol-cset-leading x-symbol-cset-leading
667,26627
-(defalias 'x-symbol-cset-score x-symbol-cset-score
668,26668
-(defalias 'x-symbol-cset-left x-symbol-cset-left
669,26708
-(defalias 'x-symbol-cset-right x-symbol-cset-right
670,26745
-(defvar x-symbol-input-initialized 672,26784
-(defun x-symbol-key-autoload 681,27080
-(defalias 'x-symbol-map-autoload x-symbol-map-autoload
703,28055
-(defun x-symbol-buffer-file-name 710,28304
-(defun x-symbol-auto-set-variable 723,28776
-(defun x-symbol-mode 729,28994
-(defun turn-on-x-symbol-conditionally 860,34373
-(defun x-symbol-fontify 868,34663
-(defun x-symbol-comint-output-filter 896,35787
-(defun x-symbol-comint-send 905,36149
-(defun x-symbol-format-decode 921,36806
-(defun x-symbol-format-encode 943,37724
-(defun x-symbol-after-insert-file 958,38250
-(defun x-symbol-write-region-annotate-function 995,40092
-(defun x-symbol-write-file-hook 1015,41096
-(defvar x-symbol-modeline-string 1076,43560
-(defvar x-symbol-mode-map1081,43775
-(defconst x-symbol-early-language-access-alist1090,44065
-(defun x-symbol-init-language-accesses 1095,44274
-(defun x-symbol-register-language 1126,45445
-(defun x-symbol-initialize 1146,46317
-(defun x-symbol-after-init 1248,51435
-(defun x-symbol-inherit-from-buffer 1306,54270
-(defun x-symbol-auctex-math-insert 1339,55750
-(defun x-symbol-turn-on-bib-cite 1348,56068
-
-x-symbol/lisp/x-symbol-image.el,1980
-(defvar x-symbol-image-process-buffer 48,1782
-(defvar x-symbol-image-process-name 51,1893
-(defvar x-symbol-image-highlight-map54,1992
-(defun x-symbol-image-try-special 73,2736
-(defvar x-symbol-image-broken-image82,3092
-(defvar x-symbol-image-create-image87,3298
-(defvar x-symbol-image-design-glyph92,3528
-(defvar x-symbol-image-locked-glyph98,3773
-(defvar x-symbol-image-remote-glyph104,4005
-(defvar x-symbol-image-junk-glyph110,4240
-(defvar x-symbol-image-buffer-extents 116,4471
-(defvar x-symbol-image-memory-cache 121,4705
-(defvar x-symbol-image-all-recursive-dirs 131,5181
-(defvar x-symbol-image-all-dirs 133,5289
-(defun x-symbol-image-parse-buffer 142,5583
-(defun x-symbol-image-after-change-function 184,7740
-(defun x-symbol-image-delete-extents 201,8322
-(defun x-symbol-image-parse-region 230,9501
-(defun x-symbol-image-default-file-name 313,12935
-(defun x-symbol-image-init-memory-cache 329,13656
-(defun x-symbol-image-init-memory-cache-1 359,14931
-(defun x-symbol-image-searchpath 371,15428
-(defun x-symbol-image-searchpath-1 399,16532
-(defun x-symbol-image-mouse-editor 425,17580
-(defun x-symbol-image-editor 433,17814
-(defun x-symbol-image-highlight-menu 462,18897
-(defun x-symbol-image-help-echo 471,19252
-(defun x-symbol-image-file-name 486,19870
-(defun x-symbol-image-event-file 502,20552
-(defun x-symbol-image-active-file 513,20947
-(defvar x-symbol-image-process-stack 569,22856
-(defvar x-symbol-image-process-elem 573,23024
-(defun x-symbol-image-create-glyph 587,23677
-(defun x-symbol-image-cache-name 645,25868
-(defun x-symbol-image-process-stack 670,26998
-(defun x-symbol-image-convert-file 683,27562
-(defun x-symbol-image-start-convert-mono 691,27895
-(defun x-symbol-image-start-convert-color 702,28375
-(defun x-symbol-image-start-convert-truecolor 713,28866
-(defun x-symbol-image-start-convert-mswindows 723,29317
-(defun x-symbol-image-start-convert-colormap 738,29917
-(defun x-symbol-image-process-sentinel 755,30778
-
-x-symbol/lisp/x-symbol-macs.el,569
-(defmacro x-symbol-ignore-property-changes 43,1617
-(defun x-symbol-set/push-assq/assoc 62,2278
-(defmacro x-symbol-set-assq 76,2819
-(defmacro x-symbol-set-assoc 82,3057
-(defmacro x-symbol-push-assq 88,3300
-(defmacro x-symbol-push-assoc 95,3618
-(defmacro x-symbol-dolist-delaying 107,4113
-(defmacro x-symbol-do-plist 148,5816
-(defmacro x-symbol-while-charsym 168,6560
-(defmacro x-symbol-encode-for-charsym 190,7309
-(defmacro x-symbol-decode-for-charsym 220,8473
-(defmacro x-symbol-decode-unique-test 245,9292
-(defmacro x-symbol-set-buffer-multibyte 251,9467
-
-x-symbol/lisp/x-symbol-mule.el,1507
-(defvar x-symbol-mule-default-charset48,2000
-(defalias 'x-symbol-make-cset x-symbol-make-cset
71,2912
-(defalias 'x-symbol-make-char x-symbol-make-char
72,2968
-(defalias 'x-symbol-init-charsym-syntax x-symbol-init-charsym-syntax
73,3024
-(defalias 'x-symbol-charsym-after x-symbol-charsym-after
74,3100
-(defalias 'x-symbol-string-to-charsyms x-symbol-string-to-charsyms
75,3164
-(defalias 'x-symbol-match-before x-symbol-match-before
76,3238
-(defalias 'x-symbol-encode-lisp x-symbol-encode-lisp
77,3300
-(defalias 'x-symbol-pre-command-hook x-symbol-pre-command-hook
78,3360
-(defalias 'x-symbol-post-command-hook x-symbol-post-command-hook
79,3430
-(defalias 'x-symbol-encode-charsym-after x-symbol-encode-charsym-after
80,3502
-(defalias 'x-symbol-init-quail-bindings x-symbol-init-quail-bindings
81,3580
-(defvar x-symbol-mule-char-table 83,3657
-(defvar x-symbol-mule-pre-command 85,3738
-(defun x-symbol-mule-make-charset 93,4009
-(defvar x-symbol-mule-default-font 107,4558
-(defun x-symbol-mule-default-font 109,4599
-(defun x-symbol-mule-make-cset 128,5509
-(defun x-symbol-mule-make-char 190,7903
-(defun x-symbol-mule-init-charsym-syntax 220,9039
-(defun x-symbol-mule-init-quail-bindings 236,9669
-(defun x-symbol-mule-encode-charsym-after 255,10393
-(defun x-symbol-mule-charsym-after 259,10498
-(defun x-symbol-mule-string-to-charsyms 268,10909
-(defun x-symbol-mule-match-before 281,11395
-(defun x-symbol-mule-pre-command-hook 305,12385
-(defun x-symbol-mule-post-command-hook 314,12788
-
-x-symbol/lisp/x-symbol-nomule.el,1954
-(defalias 'x-symbol-make-cset x-symbol-make-cset
46,1779
-(defalias 'x-symbol-make-char x-symbol-make-char
47,1837
-(defalias 'x-symbol-init-charsym-syntax x-symbol-init-charsym-syntax
48,1895
-(defalias 'x-symbol-charsym-after x-symbol-charsym-after
49,1944
-(defalias 'x-symbol-string-to-charsyms x-symbol-string-to-charsyms
50,2010
-(defalias 'x-symbol-match-before x-symbol-match-before
51,2086
-(defalias 'x-symbol-encode-lisp x-symbol-encode-lisp
52,2150
-(defalias 'x-symbol-pre-command-hook x-symbol-pre-command-hook
53,2212
-(defalias 'x-symbol-post-command-hook x-symbol-post-command-hook
54,2284
-(defalias 'x-symbol-encode-charsym-after x-symbol-encode-charsym-after
55,2358
-(defalias 'x-symbol-init-quail-bindings x-symbol-init-quail-bindings
56,2438
-(defvar x-symbol-nomule-mouse-yank-function 58,2488
-(defvar x-symbol-nomule-mouse-track-function61,2629
-(defvar x-symbol-nomule-cstring-regexp 66,2867
-(defvar x-symbol-nomule-char-table 71,3128
-(defvar x-symbol-nomule-pre-command 73,3211
-(defvar x-symbol-nomule-leading-faces-alist 76,3309
-(defvar x-symbol-nomule-font-lock-face 79,3482
-(defvar x-symbol-nomule-display-table82,3583
-(defvar x-symbol-nomule-character-quote-syntax 93,3945
-(defun x-symbol-nomule-init-faces 101,4248
-(defun x-symbol-nomule-make-cset 124,5108
-(defun x-symbol-nomule-make-char 150,6186
-(defun x-symbol-nomule-multibyte-char-p 180,7511
-(defun x-symbol-nomule-encode-charsym-after 185,7749
-(defun x-symbol-nomule-charsym-after 197,8147
-(defun x-symbol-nomule-string-to-charsyms 220,9090
-(defun x-symbol-nomule-match-before 236,9730
-(defun x-symbol-nomule-goto-leading-char 269,11142
-(defun x-symbol-nomule-mouse-yank-function 275,11371
-(defun x-symbol-nomule-mouse-track-function 282,11690
-(defun x-symbol-nomule-pre-command-hook 299,12476
-(defun x-symbol-nomule-post-command-hook 313,13109
-(defun x-symbol-nomule-match-cstring 351,14756
-(defun x-symbol-nomule-fontify-cstrings 369,15504
-
-x-symbol/lisp/x-symbol-sgml.el,1521
-(defcustom x-symbol-sgml-auto-style41,1525
-(defcustom x-symbol-sgml-auto-coding-alist52,1947
-(defface x-symbol-sgml-symbol-face71,2757
-(defface x-symbol-sgml-noname-face79,3038
-(defcustom x-symbol-sgml-modeline-name 87,3301
-(defcustom x-symbol-sgml-header-groups-alist93,3484
-(defcustom x-symbol-sgml-class-alist113,4257
-(defcustom x-symbol-sgml-class-face-alist124,4674
-(defcustom x-symbol-sgml-electric-ignore 134,5097
-(defvar x-symbol-sgml-token-list 141,5365
-(defvar x-symbol-sgml-token-grammar156,6077
-(defvar x-symbol-sgml-user-table 163,6317
-(defvar x-symbol-sgml-generated-data 166,6426
-(defcustom x-symbol-sgml-master-directory 175,6746
-(defcustom x-symbol-sgml-image-searchpath 182,6973
-(defcustom x-symbol-sgml-image-cached-dirs 189,7223
-(defcustom x-symbol-sgml-image-file-truename-alist196,7489
-(defcustom x-symbol-sgml-image-keywords226,8698
-(defun x-symbol-sgml-image-file-truename 236,9078
-(defcustom x-symbol-sgml-subscript-matcher 250,9639
-(defcustom x-symbol-sgml-font-lock-regexp 256,9875
-(defcustom x-symbol-sgml-font-lock-limit-regexp 262,10079
-(defcustom x-symbol-sgml-font-lock-contents-regexp 269,10350
-(defcustom x-symbol-sgml-font-lock-alist276,10605
-(defun x-symbol-sgml-default-token-list 292,11264
-(defvar x-symbol-sgml-latin1-table310,12052
-(defvar x-symbol-sgml-latinN-table409,15286
-(defvar x-symbol-sgml-xsymb0-table495,17715
-(defvar x-symbol-sgml-xsymb1-table601,21570
-(defvar x-symbol-sgml-table640,23549
-(defun x-symbol-sgml-subscript-matcher 657,24155
-
-x-symbol/lisp/x-symbol-tex.el,2359
-(defcustom x-symbol-tex-auto-style55,1896
-(defcustom x-symbol-tex-auto-coding-alist70,2510
-(defcustom x-symbol-tex-coding-master 87,3158
-(defcustom x-symbol-tex-modeline-name 99,3626
-(defcustom x-symbol-tex-header-groups-alist 105,3805
-(defcustom x-symbol-tex-electric-ignore 112,4065
-(defcustom x-symbol-tex-electric-ignore-regexp 119,4364
-(defcustom x-symbol-tex-token-suppress-space 126,4653
-(defvar x-symbol-tex-extra-menu-items135,5045
-(defvar x-symbol-tex-token-grammar145,5474
-(defvar x-symbol-tex-verb-delimiter-regexp 160,6263
-(defvar x-symbol-tex-env-verbatim-regexp 164,6456
-(defvar x-symbol-tex-env-tabbing-regexp 168,6637
-(defvar x-symbol-tex-user-table 172,6812
-(defvar x-symbol-tex-generated-data 175,6916
-(defcustom x-symbol-tex-master-directory 184,7234
-(defcustom x-symbol-tex-image-searchpath191,7518
-(defcustom x-symbol-tex-image-cached-dirs 209,8205
-(defcustom x-symbol-tex-image-keywords216,8458
-(defcustom x-symbol-tex-subscript-matcher 234,9311
-(defcustom x-symbol-tex-invisible-braces 240,9543
-(defcustom x-symbol-tex-font-lock-allowed-faces245,9639
-(defvar x-symbol-tex-font-lock-regexp256,10183
-(defvar x-symbol-tex-font-lock-limit-regexp 261,10425
-(defface x-symbol-tex-math-face270,10764
-(defface x-symbol-tex-text-face278,11034
-(defcustom x-symbol-tex-class-alist286,11306
-(defcustom x-symbol-tex-class-face-alist320,12867
-(defun x-symbol-tex-auto-coding-alist 336,13456
-(defun x-symbol-tex-default-master-directory 360,14702
-(defun x-symbol-tex-default-electric-ignore 368,15088
-(defun x-symbol-tex-default-token-list 390,16097
-(defun x-symbol-tex-after-init-language 400,16459
-(defvar x-symbol-tex-required-fonts 419,17293
-(defvar x-symbol-tex-latin1-table423,17445
-(defvar x-symbol-tex-latinN-table522,21630
-(defvar x-symbol-tex-xsymb0-table611,25318
-(defvar x-symbol-tex-xsymb1-table726,29931
-(defvar x-symbol-tex-table886,37347
-(defun x-symbol-tex-subscript-matcher 903,37904
-(defun x-symbol-tex-encode 951,39573
-(defun x-symbol-tex-decode 972,40387
-(defun x-symbol-tex-token-input 1047,43403
-(defun x-symbol-tex-translate-locations 1063,43971
-(defun x-symbol-tex-error-location 1119,45896
-(defun x-symbol-tex-preview-locations 1149,46926
-(defun x-symbol-tex-xdecode-old 1203,48666
-(defvar x-symbol-tex-xdecode-obarray 1245,50315
-(defun x-symbol-tex-xdecode-latex 1247,50358
-
-x-symbol/lisp/x-symbol-texi.el,597
-(defcustom x-symbol-texi-auto-style 41,1573
-(defcustom x-symbol-texi-modeline-name 48,1832
-(defcustom x-symbol-texi-header-groups-alist54,2015
-(defcustom x-symbol-texi-electric-ignore 69,2682
-(defcustom x-symbol-texi-class-alist76,2950
-(defcustom x-symbol-texi-class-face-alist 89,3508
-(defvar x-symbol-texi-token-grammar98,3801
-(defvar x-symbol-texi-user-table 107,4094
-(defvar x-symbol-texi-generated-data 110,4206
-(defvar x-symbol-texi-latin1-table119,4523
-(defvar x-symbol-texi-latinN-table218,7766
-(defvar x-symbol-texi-xsymbX-table303,10629
-(defvar x-symbol-texi-table327,11362
-
-x-symbol/lisp/x-symbol-unichars.el,99
-(defvar x-symbol-unicode-character-list5,115
-(defun x-symbol-list-unicode-characters 5044,235676
-
-x-symbol/lisp/x-symbol-unicode.el,169
-(defconst x-symbol-xsym-unicode-map	19,604
-(defconst x-symbol-old-tables267,10039
-(defconst x-symbol-unicode-table283,10470
-(defconst x-symbol-unicode-cset299,10973
-
-x-symbol/lisp/x-symbol-unicode-extras.el,40
-(defconst x-symol-unicode-extras13,263
-
-x-symbol/lisp/x-symbol-vars.el,8115
-(defconst x-symbol-version 40,1516
-(defgroup x-symbol 49,1858
-(defgroup x-symbol-mode 56,2069
-(defgroup x-symbol-input-init 61,2198
-(defgroup x-symbol-input-control 66,2334
-(defgroup x-symbol-info-general 71,2466
-(defgroup x-symbol-info-strings 76,2602
-(defgroup x-symbol-miscellaneous 81,2738
-(defgroup x-symbol-image-general 86,2864
-(defgroup x-symbol-image-language 91,3029
-(defgroup x-symbol-tex 101,3458
-(defgroup x-symbol-sgml 107,3589
-(defgroup x-symbol-bib 113,3725
-(defgroup x-symbol-texi 119,3859
-(define-widget 'x-symbol-key x-symbol-key
132,4246
-(define-widget 'x-symbol-auto-style x-symbol-auto-style
136,4336
-(define-widget 'x-symbol-command x-symbol-command
156,5203
-(define-widget 'x-symbol-charsym x-symbol-charsym
161,5311
-(define-widget 'x-symbol-group x-symbol-group
165,5402
-(define-widget 'x-symbol-coding x-symbol-coding
169,5494
-(define-widget 'x-symbol-function-or-regexp x-symbol-function-or-regexp
178,5712
-(define-widget 'x-symbol-fancy-spec x-symbol-fancy-spec
182,5881
-(define-widget 'x-symbol-fancy x-symbol-fancy
191,6229
-(define-widget 'x-symbol-auto-coding x-symbol-auto-coding
200,6582
-(define-widget 'x-symbol-headers x-symbol-headers
211,6889
-(define-widget 'x-symbol-class-info x-symbol-class-info
217,7045
-(define-widget 'x-symbol-class-faces x-symbol-class-faces
224,7288
-(define-widget 'x-symbol-image-keywords x-symbol-image-keywords
232,7568
-(defconst x-symbol-cache-variables 249,8155
-(defun x-symbol-set-cache-variable 258,8514
-(defconst x-symbol-LANG-name 270,8931
-(defconst x-symbol-LANG-modes 276,9186
-(defconst x-symbol-LANG-auto-style 282,9519
-(defcustom x-symbol-LANG-modeline-name 336,11613
-(defconst x-symbol-LANG-required-fonts 343,11898
-(defconst x-symbol-LANG-token-grammar348,12134
-(defconst x-symbol-LANG-generated-data 416,15400
-(defconst x-symbol-LANG-table 422,15652
-(defconst x-symbol-LANG-header-groups-alist 435,16207
-(defconst x-symbol-LANG-class-alist441,16510
-(defconst x-symbol-LANG-class-face-alist 455,17122
-(defconst x-symbol-LANG-electric-ignore 466,17574
-(defconst x-symbol-LANG-extra-menu-items 477,18088
-(defconst x-symbol-LANG-subscript-matcher 485,18533
-(defconst x-symbol-LANG-image-keywords 494,19001
-(defconst x-symbol-LANG-master-directory 509,19696
-(defconst x-symbol-LANG-image-searchpath 515,19987
-(defconst x-symbol-LANG-image-cached-dirs 523,20414
-(defvar x-symbol-package-url 534,20885
-(defconst x-symbol-maintainer-address 539,21129
-(defvar x-symbol-installer-address 542,21268
-(defcustom x-symbol-token-input 552,21708
-(defcustom x-symbol-electric-input 567,22362
-(defcustom x-symbol-local-menu 598,24006
-(defcustom x-symbol-local-grid 608,24350
-(defcustom x-symbol-temp-grid 620,24893
-(defcustom x-symbol-temp-help 630,25272
-(defvar x-symbol-use-refbuffer-once 640,25670
-(defcustom x-symbol-reveal-invisible 657,26459
-(defcustom x-symbol-character-info 676,27270
-(defcustom x-symbol-context-info 695,28145
-(defcustom x-symbol-charsym-modeline-name 710,28745
-(defcustom x-symbol-coding-name-alist716,28955
-(defcustom x-symbol-coding-modeline-alist742,29899
-(defcustom x-symbol-modeline-state-list757,30432
-(defcustom x-symbol-set-coding-system-if-undecided 794,31811
-(defcustom x-symbol-auto-coding-search-limit 807,32387
-(defcustom x-symbol-charsym-ascii-alist 819,32858
-(defcustom x-symbol-charsym-ascii-groups832,33446
-(defcustom x-symbol-valid-charsym-function 843,33930
-(defvar x-symbol-user-table 849,34181
-(defvar x-symbol-mule-change-default-face 861,34742
-(defcustom x-symbol-map-default-keys-alist872,35242
-(defcustom x-symbol-map-default-bindings902,36271
-(defvar x-symbol-after-init-input-hook 915,36725
-(defvar x-symbol-menu929,37366
-(defcustom x-symbol-menu-max-items 1005,40730
-(defcustom x-symbol-header-groups-alist1013,41090
-(defcustom x-symbol-completions-buffer 1042,42228
-(defcustom x-symbol-grid-buffer-format 1049,42470
-(defcustom x-symbol-grid-reuse 1058,42862
-(defcustom x-symbol-grid-header-echo1065,43142
-(defcustom x-symbol-grid-ignore-charsyms 1076,43585
-(defcustom x-symbol-grid-tab-width 1082,43812
-(defface x-symbol-heading-face1089,44115
-(defvar x-symbol-heading-strut-glyph1101,44565
-(defvar x-symbol-key-init-ignore 1115,45116
-(defvar x-symbol-quail-init-ignore 1119,45254
-(defvar x-symbol-context-init-ignore 1123,45394
-(defcustom x-symbol-context-ignore 1130,45685
-(defcustom x-symbol-electric-ignore 1138,46014
-(defcustom x-symbol-rotate-suffix-char 1149,46535
-(defcustom x-symbol-rotate-prefix-alist1158,46977
-(defvar x-symbol-list-mode-hook 1181,47657
-(defvar x-symbol-key-min-length 1186,47824
-(defvar x-symbol-quail-suffix-string 1191,48048
-(defvar x-symbol-define-input-method-quail 1194,48100
-(defcustom x-symbol-idle-delay 1201,48355
-(defface x-symbol-revealed-face1209,48703
-(defcustom x-symbol-context-info-ignore 1217,48995
-(defcustom x-symbol-context-info-threshold 1225,49388
-(defcustom x-symbol-context-info-ignore-regexp 1231,49594
-(defcustom x-symbol-context-info-ignore-groups1237,49821
-(defface x-symbol-info-face1251,50343
-(defface x-symbol-emph-info-face1262,50788
-(defcustom x-symbol-info-intro-after1270,51073
-(defcustom x-symbol-info-intro-before1279,51379
-(defcustom x-symbol-info-intro-highlight1288,51684
-(defcustom x-symbol-info-intro-list1297,52025
-(defcustom x-symbol-info-intro-yank1306,52413
-(defcustom x-symbol-info-alias-after1315,52795
-(defcustom x-symbol-info-alias-before1325,53227
-(defcustom x-symbol-info-context-pre1335,53644
-(defcustom x-symbol-info-context-post1344,54033
-(defcustom x-symbol-info-token-pre 1353,54349
-(defcustom x-symbol-info-token-charsym1360,54609
-(defcustom x-symbol-info-classes-pre 1369,54957
-(defcustom x-symbol-info-classes-sep 1376,55213
-(defcustom x-symbol-info-classes-post 1383,55468
-(defcustom x-symbol-info-classes-charsym 1390,55728
-(defcustom x-symbol-info-coding-pre 1397,56006
-(defcustom x-symbol-info-coding-sep 1404,56252
-(defcustom x-symbol-info-coding-post 1411,56499
-(defcustom x-symbol-info-coding-alist1418,56723
-(defcustom x-symbol-info-keys-keymaps 1434,57353
-(defcustom x-symbol-info-keys-pre1442,57729
-(defcustom x-symbol-info-keys-sep 1451,58097
-(defcustom x-symbol-info-keys-post 1458,58354
-(defconst x-symbol-fancy-cache-size 1465,58581
-(defvar x-symbol-cache-size 1468,58688
-(defvar x-symbol-modify-aspects-alist1477,59011
-(defvar x-symbol-rotate-aspects-alist1491,59696
-(defvar x-symbol-group-input-alist1507,60510
-(defvar x-symbol-group-syntax-alist1557,62097
-(defvar x-symbol-subgroup-string-alist1600,63344
-(defvar x-symbol-latin-force-use 1614,63859
-(defvar x-symbol-font-sizes1623,64369
-(defvar x-symbol-font-lock-with-extra-props1633,64777
-(defvar x-symbol-latin1-fonts1637,64928
-(defvar x-symbol-latin2-fonts1642,65128
-(defvar x-symbol-latin3-fonts1648,65391
-(defvar x-symbol-latin5-fonts1654,65654
-(defvar x-symbol-latin9-fonts1661,65961
-(defvar x-symbol-xsymb0-fonts1666,66159
-(defvar x-symbol-xsymb1-fonts1672,66448
-(defcustom x-symbol-image-max-width 1683,66909
-(defcustom x-symbol-image-max-height 1688,67031
-(defcustom x-symbol-image-update-cache 1693,67154
-(defcustom x-symbol-image-use-remote 1709,67925
-(defcustom x-symbol-image-current-marker 1734,69124
-(defcustom x-symbol-image-scale-method 1742,69471
-(defcustom x-symbol-image-explicitly-relative-regexp 1756,70201
-(defcustom x-symbol-image-searchpath-follow-symlink 1761,70383
-(defcustom x-symbol-image-cache-directories1776,71078
-(defvar x-symbol-image-temp-name1825,73060
-(defcustom x-symbol-image-convert-mono-regexp1834,73477
-(defcustom x-symbol-image-help-echo1848,74165
-(defcustom x-symbol-image-editor-alist1860,74669
-(defvar x-symbol-image-menu1893,76025
-(defvar x-symbol-image-data-directory 1914,77028
-(defvar x-symbol-image-special-glyphs1918,77195
-(defcustom x-symbol-image-convert-file-alist1951,78893
-(defcustom x-symbol-image-convert-program1961,79361
-(defcustom x-symbol-image-converter-required 1967,79588
-(defcustom x-symbol-image-converter1972,79767
-(defun x-symbol-variable-interactive 2080,84357
-(defcustom x-symbol-use-unicode 2099,85187
-
-x-symbol/lisp/x-symbol-xmacs.el,522
-(defun x-symbol-paren-reset-mode 102,4657
-(defvar x-symbol-xmacs-default-face-fonts 136,6073
-(defalias 'x-symbol-directory-files x-symbol-directory-files
138,6121
-(defun x-symbol-event-in-current-buffer 140,6176
-(defun x-symbol-create-image 144,6318
-(defalias 'x-symbol-make-glyph x-symbol-make-glyph
149,6483
-(defalias 'x-symbol-set-glyph-image x-symbol-set-glyph-image
151,6528
-(defun x-symbol-set-face-font 153,6583
-(defun x-symbol-event-matches-key-specifier-p 163,7016
-(defun x-symbol-window-width 173,7418
-
-doc/ProofGeneral.texi,5602
-@node Top167,5076
-@node Preface204,6204
-@node Latest news for version 3.7.1Latest news for version 3.7.1
227,6802
-@node Future272,8853
-@node Credits303,10152
-@node Introducing Proof GeneralIntroducing Proof General
409,13921
-@node Installing Proof GeneralInstalling Proof General
465,15963
-@node Quick start guideQuick start guide
479,16412
-@node Features of Proof GeneralFeatures of Proof General
523,18533
-@node Supported proof assistantsSupported proof assistants
612,22470
-@node Prerequisites for this manualPrerequisites for this manual
661,24390
-@node Organization of this manualOrganization of this manual
705,26016
-@node Basic Script ManagementBasic Script Management
731,26844
-@node Walkthrough example in IsabelleWalkthrough example in Isabelle
750,27444
-@node Proof scriptsProof scripts
1001,37097
-@node Script buffersScript buffers
1044,39217
-@node Locked queue and editing regionsLocked queue and editing regions
1066,39794
-@node Goal-save sequencesGoal-save sequences
1122,41941
-@node Active scripting bufferActive scripting buffer
1159,43427
-@node Summary of Proof General buffersSummary of Proof General buffers
1228,46847
-@node Script editing commandsScript editing commands
1290,49521
-@node Script processing commandsScript processing commands
1368,52380
-@node Proof assistant commandsProof assistant commands
1496,57681
-@node Toolbar commandsToolbar commands
1662,63460
-@node Interrupting during trace outputInterrupting during trace output
1686,64389
-@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
1725,66313
-@node Goals buffer commandsGoals buffer commands
1739,66813
-@node Advanced Script Management and EditingAdvanced Script Management and Editing
1828,70352
-@node Visibility of completed proofsVisibility of completed proofs
1860,71564
-@node Switching between proof scriptsSwitching between proof scripts
1915,73487
-@node View of processed files View of processed files 
1952,75459
-@node Retracting across filesRetracting across files
2012,78510
-@node Asserting across filesAsserting across files
2025,79141
-@node Automatic multiple file handlingAutomatic multiple file handling
2038,79707
-@node Escaping script managementEscaping script management
2063,80741
-@node Editing featuresEditing features
2121,82944
-@node Experimental featuresExperimental features
2185,85616
-@node Support for other PackagesSupport for other Packages
2219,86880
-@node Syntax highlightingSyntax highlighting
2252,87775
-@node X-Symbol supportX-Symbol support
2291,89396
-@node Unicode supportUnicode support
2349,91936
-@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)
2464,96733
-@node Support for outline modeSupport for outline mode
2523,98863
-@node Support for completionSupport for completion
2549,99993
-@node Support for tagsSupport for tags
2607,102169
-@node Customizing Proof GeneralCustomizing Proof General
2659,104498
-@node Basic optionsBasic options
2699,106168
-@node How to customizeHow to customize
2723,106926
-@node Display customizationDisplay customization
2774,109028
-@node User optionsUser options
2899,114266
-@node Changing facesChanging faces
3171,123965
-@node Tweaking configuration settingsTweaking configuration settings
3246,126634
-@node Hints and TipsHints and Tips
3303,129160
-@node Adding your own keybindingsAdding your own keybindings
3322,129761
-@node Using file variablesUsing file variables
3378,132294
-@node Using abbreviationsUsing abbreviations
3437,134480
-@node LEGO Proof GeneralLEGO Proof General
3476,135896
-@node LEGO specific commandsLEGO specific commands
3517,137265
-@node LEGO tagsLEGO tags
3537,137720
-@node LEGO customizationsLEGO customizations
3547,137967
-@node Coq Proof GeneralCoq Proof General
3579,138886
-@node Coq-specific commandsCoq-specific commands
3595,139295
-@node Coq-specific variablesCoq-specific variables
3617,139802
-@node Editing multiple proofsEditing multiple proofs
3639,140460
-@node User-loaded tacticsUser-loaded tactics
3663,141568
-@node Holes featureHoles feature
3727,144042
-@node Isabelle Proof GeneralIsabelle Proof General
3754,145329
-@node Choosing logic and starting isabelleChoosing logic and starting isabelle
3785,146498
-@node Isabelle commandsIsabelle commands
3860,149547
-@node Isabelle settingsIsabelle settings
4003,153702
-@node Isabelle customizationsIsabelle customizations
4017,154284
-@node HOL Proof GeneralHOL Proof General
4040,154771
-@node Shell Proof GeneralShell Proof General
4082,156593
-@node Obtaining and InstallingObtaining and Installing
4118,158052
-@node Obtaining Proof GeneralObtaining Proof General
4134,158465
-@node Installing Proof General from tarballInstalling Proof General from tarball
4165,159704
-@node Installing Proof General from RPM packageInstalling Proof General from RPM package
4190,160536
-@node Setting the names of binariesSetting the names of binaries
4205,160944
-@node Notes for syssiesNotes for syssies
4233,161884
-@node Bugs and EnhancementsBugs and Enhancements
4308,164920
-@node References4329,165735
-@node History of Proof GeneralHistory of Proof General
4369,166758
-@node Old News for 3.0Old News for 3.0
4460,170860
-@node Old News for 3.1Old News for 3.1
4530,174554
-@node Old News for 3.2Old News for 3.2
4556,175726
-@node Old News for 3.3Old News for 3.3
4617,178729
-@node Old News for 3.4Old News for 3.4
4636,179626
-@node Function IndexFunction Index
4659,180682
-@node Variable IndexVariable Index
4663,180758
-@node Keystroke IndexKeystroke Index
4667,180838
-@node Concept IndexConcept Index
4671,180904
-
-doc/PG-adapting.texi,3776
-@node Top157,4776
-@node Introduction195,5921
-@node Future236,7574
-@node Credits272,9170
-@node Beginning with a New ProverBeginning with a New Prover
282,9462
-@node Overview of adding a new proverOverview of adding a new prover
323,11411
-@node Demonstration instance and easy configurationDemonstration instance and easy configuration
401,14719
-@node Major modes used by Proof GeneralMajor modes used by Proof General
470,18110
-@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands
503,19461
-@node Settings for generic user-level commandsSettings for generic user-level commands
518,20007
-@node Menu configurationMenu configuration
563,21741
-@node Toolbar configurationToolbar configuration
587,22658
-@node Proof Script SettingsProof Script Settings
645,24900
-@node Recognizing commands and commentsRecognizing commands and comments
667,25480
-@node Recognizing proofsRecognizing proofs
788,30987
-@node Recognizing other elementsRecognizing other elements
900,35800
-@node Configuring undo behaviourConfiguring undo behaviour
1026,41311
-@node Nested proofsNested proofs
1163,46705
-@node Safe (state-preserving) commandsSafe (state-preserving) commands
1203,48331
-@node Activate scripting hookActivate scripting hook
1226,49277
-@node Automatic multiple filesAutomatic multiple files
1250,50140
-@node Completions1272,50987
-@node Proof Shell SettingsProof Shell Settings
1313,52476
-@node Proof shell commandsProof shell commands
1344,53758
-@node Script input to the shellScript input to the shell
1508,60697
-@node Settings for matching various output from proof processSettings for matching various output from proof process
1575,63744
-@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process
1706,69493
-@node Hooks and other settingsHooks and other settings
1921,79364
-@node Goals Buffer SettingsGoals Buffer Settings
2002,82733
-@node Splash Screen SettingsSplash Screen Settings
2079,85832
-@node Global ConstantsGlobal Constants
2105,86590
-@node Handling Multiple FilesHandling Multiple Files
2131,87431
-@node Configuring Editing SyntaxConfiguring Editing Syntax
2283,95214
-@node Configuring Font LockConfiguring Font Lock
2342,97335
-@node Configuring X-SymbolConfiguring X-Symbol
2429,101620
-@node Writing More Lisp CodeWriting More Lisp Code
2489,104140
-@node Default values for generic settingsDefault values for generic settings
2506,104785
-@node Adding prover-specific configurationsAdding prover-specific configurations
2536,105868
-@node Useful variablesUseful variables
2579,107150
-@node Useful functions and macrosUseful functions and macros
2594,107649
-@node Internals of Proof GeneralInternals of Proof General
2697,111604
-@node Spans2725,112512
-@node Proof General site configurationProof General site configuration
2738,112886
-@node Configuration variable mechanismsConfiguration variable mechanisms
2818,115932
-@node Global variablesGlobal variables
2939,121362
-@node Proof script modeProof script mode
3009,123910
-@node Proof shell modeProof shell mode
3268,135565
-@node Debugging3675,151647
-@node Plans and IdeasPlans and Ideas
3718,152523
-@node Proof by pointing and similar featuresProof by pointing and similar features
3739,153245
-@node Granularity of atomic command sequencesGranularity of atomic command sequences
3777,154903
-@node Browser mode for script files and theoriesBrowser mode for script files and theories
3822,157128
-@node Demonstration InstantiationsDemonstration Instantiations
3852,158159
-@node demoisa-easy.el3868,158590
-@node demoisa.el3931,160828
-@node Function IndexFunction Index
4086,165812
-@node Variable IndexVariable Index
4090,165888
-@node Concept IndexConcept Index
4099,166067
-
-x-symbol/lisp/_pkg.el,0
-
-x-symbol/lisp/custom-load.el,0
-
-lib/holes-load.el,0
+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
+
+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
 
 generic/proof.el,0
 
-generic/proof-autoloads.el,0
-
-twelf/x-symbol-twelf.el,0
-
 pgshell/pgshell.el,0
 
-lego/x-symbol-lego.el,0
-
 isar/isar-autotest.el,0
 
 isar/interface-setup.el,0
 
-hol98/x-symbol-hol98.el,0
-
 hol98/hol98.el,0
 
 demoisa/demoisa-easy.el,0
@@ -3750,6 +2786,4 @@ coq/coq-autotest.el,0
 
 ccc/ccc.el,0
 
-acl2/x-symbol-acl2.el,0
-
 acl2/acl2.el,0