Updated.

1 files changed, 1325 insertions, 1306 deletions

diff --git a/TAGS b/TAGS
index 75d63fce..5f27222b 100644
--- a/TAGS
+++ b/TAGS
@@ -13,7 +13,7 @@ coq/coq-abbrev.el,468
 (defpgdefault menu-entries 71,2121
 (defpgdefault help-menu-entries152,5542
 
-coq/coq-db.el,474
+coq/coq-db.el,559
 (defconst coq-syntax-db 18,455
 (defvar coq-user-tactics-db54,1828
 (defun coq-insert-from-db 64,2177
@@ -26,163 +26,165 @@ coq/coq-db.el,474
 (defun coq-build-abbrev-table-from-db 183,7169
 (defun filter-state-preserving 199,7723
 (defun filter-state-changing 204,7877
-
-coq/coq.el,6119
-(defcustom coq-prog-name 28,652
-(defcustom coq-prog-args 41,1182
-(defcustom coq-compile-file-command 44,1292
-(defcustom coq-default-undo-limit 54,1661
-(defconst coq-shell-init-cmd 59,1789
-(defcustom coq-utf-safe 68,2005
-(defconst coq-shell-restart-cmd 84,2637
-(defvar coq-shell-prompt-pattern 91,2897
-(defvar coq-shell-cd 98,3219
-(defvar coq-shell-abort-goal-regexp 102,3374
-(defvar coq-shell-proof-completed-regexp 105,3500
-(defvar coq-goal-regexp108,3631
-(defun coq-library-directory 117,3820
-(defcustom coq-tags 124,4000
-(defconst coq-interrupt-regexp 129,4150
-(defcustom coq-www-home-page 134,4271
-(defvar coq-outline-regexp144,4442
-(defvar coq-outline-heading-end-regexp 151,4656
-(defvar coq-shell-outline-regexp 153,4710
-(defvar coq-shell-outline-heading-end-regexp 154,4760
-(defconst coq-kill-goal-command 159,4870
-(defconst coq-forget-id-command 160,4913
-(defconst coq-back-n-command 161,4960
-(defconst coq-state-preserving-tactics-regexp 165,5104
-(defconst coq-state-changing-commands-regexp167,5205
-(defconst coq-state-preserving-commands-regexp 169,5312
-(defconst coq-commands-regexp 171,5424
-(defvar coq-retractable-instruct-regexp 173,5502
-(defvar coq-non-retractable-instruct-regexp 175,5593
-(defvar coq-keywords-section179,5733
-(defvar coq-section-regexp 182,5827
-(defun coq-set-undo-limit 216,6927
-(defconst coq-keywords-decl-defn-regexp227,7366
-(defun coq-proof-mode-p 231,7516
-(defun coq-is-comment-or-proverprocp 242,7926
-(defun coq-is-goalsave-p 244,8030
-(defun coq-is-module-equal-p 245,8105
-(defun coq-is-def-p 248,8301
-(defun coq-is-decl-defn-p 250,8409
-(defun coq-state-preserving-command-p 255,8576
-(defun coq-command-p 258,8710
-(defun coq-state-preserving-tactic-p 261,8810
-(defun coq-state-changing-tactic-p 266,8958
-(defun coq-state-changing-command-p 273,9192
-(defun coq-section-or-module-start-p 280,9538
-(defun build-list-id-from-string 289,9779
-(defun coq-last-prompt-info 302,10309
-(defun coq-last-prompt-info-safe 314,10850
-(defvar coq-last-but-one-statenum 324,11365
-(defvar coq-last-but-one-proofnum 326,11432
-(defvar coq-last-but-one-proofstack 328,11495
-(defun coq-get-span-statenum 330,11537
-(defun coq-get-span-proofnum 335,11652
-(defun coq-get-span-proofstack 340,11767
-(defun coq-set-span-statenum 345,11911
-(defun coq-get-span-goalcmd 350,12042
-(defun coq-set-span-goalcmd 355,12156
-(defun coq-set-span-proofnum 360,12286
-(defun coq-set-span-proofstack 365,12417
-(defun proof-last-locked-span 370,12577
-(defun coq-set-state-infos 385,13181
-(defun count-not-intersection 425,15260
-(defun  coq-find-and-forget-v81 456,16514
-(defun coq-find-and-forget-v80 484,17646
-(defun coq-find-and-forget 579,22345
-(defvar coq-current-goal 592,22885
-(defun coq-goal-hyp 595,22950
-(defun coq-state-preserving-p 608,23380
-(defconst notation-print-kinds-table 623,23886
-(defun coq-PrintScope 627,24054
-(defun coq-guess-or-ask-for-string 646,24610
-(defun coq-ask-do 657,24995
-(defun coq-SearchIsos 666,25383
-(defun coq-SearchConstant 672,25616
-(defun coq-SearchRewrite 676,25709
-(defun coq-SearchAbout 680,25807
-(defun coq-Print 684,25899
-(defun coq-About 688,26021
-(defun coq-LocateConstant 692,26138
-(defun coq-LocateLibrary 698,26273
-(defun coq-addquotes 704,26423
-(defun coq-LocateNotation 706,26471
-(defun coq-Pwd 713,26670
-(defun coq-Inspect 719,26802
-(defun coq-PrintSection(723,26902
-(defun coq-Print-implicit 727,26996
-(defun coq-Check 732,27148
-(defun coq-Show 737,27258
-(defun coq-PrintHint 752,27704
-(defun coq-Compile 760,27850
-(defun coq-guess-command-line 773,28169
-(defun coq-pre-shell-start 795,29017
-(defun coq-mode-config 807,29541
-(defun coq-hybrid-ouput-goals-response-p 923,33751
-(defun coq-hybrid-ouput-goals-response 929,34009
-(defun coq-shell-mode-config 951,34921
-(defun coq-goals-mode-config 992,36758
-(defun coq-response-config 999,36990
-(defun coq-maybe-compile-buffer 1019,37696
-(defun coq-ancestors-of 1056,39230
-(defun coq-all-ancestors-of 1079,40197
-(defconst coq-require-command-regexp 1091,40590
-(defun coq-process-require-command 1096,40799
-(defun coq-included-children 1101,40926
-(defun coq-process-file 1122,41765
-(defpacustom print-fully-explicit 1147,42680
-(defpacustom print-implicit 1152,42829
-(defpacustom print-coercions 1157,42996
-(defpacustom print-match-wildcards 1162,43141
-(defpacustom print-elim-types 1167,43322
-(defpacustom printing-depth 1172,43489
-(defpacustom time-commands 1177,43651
-(defpacustom auto-compile-vos 1181,43762
-(defpacustom translate-to-v8 1203,44717
-(defun coq-preprocessing 1212,44933
-(defun coq-fake-constant-markup 1227,45352
-(defun coq-create-span-menu 1249,46159
-(defconst module-kinds-table 1276,46961
-(defconst modtype-kinds-table1280,47111
-(defun coq-insert-section-or-module 1284,47240
-(defconst reqkinds-kinds-table1307,48100
-(defun coq-insert-requires 1312,48245
-(defun coq-end-Section 1328,48751
-(defun coq-insert-intros 1346,49335
-(defun coq-insert-match 1358,49859
-(defun coq-insert-tactic 1390,51037
-(defun coq-insert-tactical 1396,51276
-(defun coq-insert-command 1402,51525
-(defun coq-insert-term 1408,51769
-(define-key coq-keymap 1415,51967
-(define-key coq-keymap 1416,52025
-(define-key coq-keymap 1417,52082
-(define-key coq-keymap 1418,52151
-(define-key coq-keymap 1419,52207
-(define-key coq-keymap 1420,52256
-(define-key coq-keymap 1421,52314
-(define-key coq-keymap 1423,52375
-(define-key coq-keymap 1424,52434
-(define-key coq-keymap 1426,52498
-(define-key coq-keymap 1427,52558
-(define-key coq-keymap 1429,52614
-(define-key coq-keymap 1430,52664
-(define-key coq-keymap 1431,52714
-(define-key coq-keymap 1432,52764
-(define-key coq-keymap 1433,52818
-(define-key coq-keymap 1434,52877
-(defvar last-coq-error-location 1444,53060
-(defun coq-get-last-error-location 1453,53459
-(defun coq-highlight-error 1486,54856
-(defun coq-decide-highlight-error 1555,57541
-(defun coq-highlight-error-hook 1560,57703
-(defun first-word-of-buffer 1571,58096
-(defun coq-show-first-goal 1580,58327
-(defun is-not-split-vertic 1605,59216
-(defun optim-resp-windows 1614,59655
+(defface coq-solve-tactics-face 211,8098
+(defconst coq-solve-tactics-face 219,8358
+
+coq/coq.el,6118
+(defcustom coq-prog-name 28,654
+(defcustom coq-prog-args 41,1184
+(defcustom coq-compile-file-command 45,1308
+(defcustom coq-default-undo-limit 55,1677
+(defconst coq-shell-init-cmd 60,1805
+(defvar coq-utf-safe 69,2021
+(defcustom coq-prog-env 81,2461
+(defconst coq-shell-restart-cmd 89,2713
+(defvar coq-shell-prompt-pattern 96,2973
+(defvar coq-shell-cd 103,3295
+(defvar coq-shell-abort-goal-regexp 107,3450
+(defvar coq-shell-proof-completed-regexp 110,3576
+(defvar coq-goal-regexp113,3707
+(defun coq-library-directory 122,3896
+(defcustom coq-tags 129,4076
+(defconst coq-interrupt-regexp 134,4226
+(defcustom coq-www-home-page 139,4347
+(defvar coq-outline-regexp149,4518
+(defvar coq-outline-heading-end-regexp 156,4732
+(defvar coq-shell-outline-regexp 158,4786
+(defvar coq-shell-outline-heading-end-regexp 159,4836
+(defconst coq-kill-goal-command 164,4946
+(defconst coq-forget-id-command 165,4989
+(defconst coq-back-n-command 166,5036
+(defconst coq-state-preserving-tactics-regexp 170,5180
+(defconst coq-state-changing-commands-regexp172,5281
+(defconst coq-state-preserving-commands-regexp 174,5388
+(defconst coq-commands-regexp 176,5500
+(defvar coq-retractable-instruct-regexp 178,5578
+(defvar coq-non-retractable-instruct-regexp 180,5669
+(defvar coq-keywords-section184,5809
+(defvar coq-section-regexp 187,5903
+(defun coq-set-undo-limit 221,7003
+(defconst coq-keywords-decl-defn-regexp232,7442
+(defun coq-proof-mode-p 236,7592
+(defun coq-is-comment-or-proverprocp 247,8002
+(defun coq-is-goalsave-p 249,8106
+(defun coq-is-module-equal-p 250,8181
+(defun coq-is-def-p 253,8377
+(defun coq-is-decl-defn-p 255,8485
+(defun coq-state-preserving-command-p 260,8652
+(defun coq-command-p 263,8786
+(defun coq-state-preserving-tactic-p 266,8886
+(defun coq-state-changing-tactic-p 271,9034
+(defun coq-state-changing-command-p 278,9268
+(defun coq-section-or-module-start-p 285,9614
+(defun build-list-id-from-string 294,9855
+(defun coq-last-prompt-info 307,10385
+(defun coq-last-prompt-info-safe 319,10926
+(defvar coq-last-but-one-statenum 329,11441
+(defvar coq-last-but-one-proofnum 331,11508
+(defvar coq-last-but-one-proofstack 333,11571
+(defun coq-get-span-statenum 335,11613
+(defun coq-get-span-proofnum 340,11728
+(defun coq-get-span-proofstack 345,11843
+(defun coq-set-span-statenum 350,11987
+(defun coq-get-span-goalcmd 355,12118
+(defun coq-set-span-goalcmd 360,12232
+(defun coq-set-span-proofnum 365,12362
+(defun coq-set-span-proofstack 370,12493
+(defun proof-last-locked-span 375,12653
+(defun coq-set-state-infos 390,13257
+(defun count-not-intersection 430,15336
+(defun  coq-find-and-forget-v81 461,16590
+(defun coq-find-and-forget-v80 489,17722
+(defun coq-find-and-forget 584,22421
+(defvar coq-current-goal 597,22961
+(defun coq-goal-hyp 600,23026
+(defun coq-state-preserving-p 613,23459
+(defconst notation-print-kinds-table 628,23965
+(defun coq-PrintScope 632,24133
+(defun coq-guess-or-ask-for-string 651,24689
+(defun coq-ask-do 662,25074
+(defun coq-SearchIsos 671,25462
+(defun coq-SearchConstant 677,25695
+(defun coq-SearchRewrite 681,25788
+(defun coq-SearchAbout 685,25886
+(defun coq-Print 689,25978
+(defun coq-About 693,26100
+(defun coq-LocateConstant 697,26217
+(defun coq-LocateLibrary 703,26352
+(defun coq-addquotes 709,26502
+(defun coq-LocateNotation 711,26550
+(defun coq-Pwd 718,26749
+(defun coq-Inspect 724,26881
+(defun coq-PrintSection(728,26981
+(defun coq-Print-implicit 732,27075
+(defun coq-Check 737,27227
+(defun coq-Show 742,27337
+(defun coq-Compile 756,27782
+(defun coq-guess-command-line 769,28101
+(defun coq-pre-shell-start 791,28949
+(defun coq-mode-config 803,29473
+(defun coq-hybrid-ouput-goals-response-p 919,33683
+(defun coq-hybrid-ouput-goals-response 925,33941
+(defun coq-shell-mode-config 947,34853
+(defun coq-goals-mode-config 991,36924
+(defun coq-response-config 998,37156
+(defun coq-maybe-compile-buffer 1018,37862
+(defun coq-ancestors-of 1055,39396
+(defun coq-all-ancestors-of 1078,40363
+(defconst coq-require-command-regexp 1090,40756
+(defun coq-process-require-command 1095,40965
+(defun coq-included-children 1100,41092
+(defun coq-process-file 1121,41931
+(defpacustom print-fully-explicit 1146,42846
+(defpacustom print-implicit 1151,42995
+(defpacustom print-coercions 1156,43162
+(defpacustom print-match-wildcards 1161,43307
+(defpacustom print-elim-types 1166,43488
+(defpacustom printing-depth 1171,43655
+(defpacustom time-commands 1176,43817
+(defpacustom auto-compile-vos 1180,43928
+(defpacustom translate-to-v8 1202,44883
+(defun coq-preprocessing 1211,45099
+(defun coq-fake-constant-markup 1226,45518
+(defun coq-create-span-menu 1248,46325
+(defconst module-kinds-table 1275,47127
+(defconst modtype-kinds-table1279,47277
+(defun coq-insert-section-or-module 1283,47406
+(defconst reqkinds-kinds-table1306,48266
+(defun coq-insert-requires 1311,48411
+(defun coq-end-Section 1327,48917
+(defun coq-insert-intros 1345,49501
+(defun coq-insert-match 1357,50025
+(defun coq-insert-tactic 1389,51203
+(defun coq-insert-tactical 1395,51442
+(defun coq-insert-command 1401,51691
+(defun coq-insert-term 1407,51935
+(define-key coq-keymap 1414,52133
+(define-key coq-keymap 1415,52191
+(define-key coq-keymap 1416,52248
+(define-key coq-keymap 1417,52317
+(define-key coq-keymap 1418,52373
+(define-key coq-keymap 1419,52422
+(define-key coq-keymap 1420,52480
+(define-key coq-keymap 1422,52541
+(define-key coq-keymap 1423,52600
+(define-key coq-keymap 1425,52664
+(define-key coq-keymap 1426,52724
+(define-key coq-keymap 1428,52780
+(define-key coq-keymap 1429,52830
+(define-key coq-keymap 1430,52880
+(define-key coq-keymap 1431,52930
+(define-key coq-keymap 1432,52984
+(define-key coq-keymap 1433,53043
+(defvar last-coq-error-location 1443,53226
+(defun coq-get-last-error-location 1452,53625
+(defun coq-highlight-error 1485,55022
+(defun coq-decide-highlight-error 1554,57707
+(defun coq-highlight-error-hook 1559,57869
+(defun first-word-of-buffer 1570,58262
+(defun coq-show-first-goal 1579,58493
+(defun is-not-split-vertic 1604,59382
+(defun optim-resp-windows 1613,59821
 
 coq/coq-indent.el,2241
 (defconst coq-any-command-regexp11,262
@@ -247,66 +249,70 @@ coq/coq-local-vars.el,279
 (defun coq-ask-prog-name 133,5426
 (defun coq-ask-insert-coq-prog-name 148,6067
 
-coq/coq-syntax.el,2333
-(defvar coq-version-is-V8 21,729
-(defvar coq-version-is-V8-0 23,808
-(defvar coq-version-is-V8-1 30,1180
-(defcustom coq-user-tactics-db 80,3391
-(defcustom coq-user-commands-db 97,3897
-(defcustom coq-user-tacticals-db 113,4409
-(defvar coq-tactics-db131,4925
-(defvar coq-tacticals-db286,12908
-(defvar coq-decl-db310,13723
-(defvar coq-defn-db332,14941
-(defvar coq-goal-starters-db384,18849
-(defvar coq-commands-db409,20266
-(defvar coq-terms-db533,29360
-(defun coq-count-match 597,31994
-(defun coq-goal-command-str-v80-p 616,32848
-(defun coq-module-opening-p 639,33714
-(defun coq-section-command-p 650,34126
-(defun coq-goal-command-str-v81-p 654,34223
-(defun coq-goal-command-p-v81 669,34891
-(defun coq-goal-command-str-p 679,35227
-(defun coq-goal-command-p 689,35588
-(defvar coq-keywords-save-strict697,35896
-(defvar coq-keywords-save706,36007
-(defun coq-save-command-p 710,36083
-(defvar coq-keywords-kill-goal 719,36377
-(defvar coq-keywords-state-changing-misc-commands723,36468
-(defvar coq-keywords-goal726,36593
-(defvar coq-keywords-decl729,36676
-(defvar coq-keywords-defn732,36750
-(defvar coq-keywords-state-changing-commands736,36825
-(defvar coq-keywords-state-preserving-commands745,37023
-(defvar coq-keywords-commands750,37239
-(defvar coq-tacticals755,37387
-(defvar coq-reserved760,37523
-(defvar coq-state-changing-tactics769,37816
-(defvar coq-state-preserving-tactics772,37925
-(defvar coq-tactics776,38039
-(defvar coq-retractable-instruct779,38128
-(defvar coq-non-retractable-instruct782,38238
-(defvar coq-keywords786,38360
-(defvar coq-symbols793,38527
-(defvar coq-error-regexp 812,38740
-(defvar coq-id 815,38968
-(defvar coq-id-shy 816,38993
-(defvar coq-ids 818,39047
-(defun coq-first-abstr-regexp 820,39088
-(defvar coq-font-lock-terms823,39184
-(defconst coq-save-command-regexp-strict837,39796
-(defconst coq-save-command-regexp841,39963
-(defconst coq-save-with-hole-regexp845,40116
-(defconst coq-goal-command-regexp849,40274
-(defconst coq-goal-with-hole-regexp852,40374
-(defconst coq-decl-with-hole-regexp856,40506
-(defconst coq-defn-with-hole-regexp860,40638
-(defconst coq-with-with-hole-regexp871,40922
-(defvar coq-font-lock-keywords-1877,41212
-(defvar coq-font-lock-keywords 900,42408
-(defun coq-init-syntax-table 902,42466
-(defconst coq-generic-expression931,43364
+coq/coq-syntax.el,2498
+(defvar coq-version-is-V8 21,731
+(defvar coq-version-is-V8-0 23,810
+(defvar coq-version-is-V8-1 30,1182
+(defcustom coq-user-tactics-db 82,3395
+(defcustom coq-user-commands-db 99,3901
+(defcustom coq-user-tacticals-db 115,4413
+(defcustom coq-user-solve-tactics-db 131,4927
+(defcustom coq-user-reserved-db 149,5441
+(defvar coq-tactics-db167,5965
+(defvar coq-solve-tactics-db322,13974
+(defvar coq-tacticals-db345,14771
+(defvar coq-decl-db370,15587
+(defvar coq-defn-db392,16805
+(defvar coq-goal-starters-db445,20791
+(defvar coq-commands-db471,22282
+(defvar coq-terms-db597,31529
+(defun coq-count-match 661,34163
+(defun coq-goal-command-str-v80-p 680,35017
+(defun coq-module-opening-p 703,35883
+(defun coq-section-command-p 714,36295
+(defun coq-goal-command-str-v81-p 718,36392
+(defun coq-goal-command-p-v81 733,37060
+(defun coq-goal-command-str-p 743,37396
+(defun coq-goal-command-p 753,37757
+(defvar coq-keywords-save-strict761,38065
+(defvar coq-keywords-save770,38176
+(defun coq-save-command-p 774,38252
+(defvar coq-keywords-kill-goal 783,38546
+(defvar coq-keywords-state-changing-misc-commands787,38637
+(defvar coq-keywords-goal790,38762
+(defvar coq-keywords-decl793,38845
+(defvar coq-keywords-defn796,38919
+(defvar coq-keywords-state-changing-commands800,38994
+(defvar coq-keywords-state-preserving-commands809,39192
+(defvar coq-keywords-commands814,39408
+(defvar coq-solve-tactics819,39556
+(defvar coq-tacticals823,39677
+(defvar coq-reserved829,39816
+(defvar coq-state-changing-tactics840,40136
+(defvar coq-state-preserving-tactics843,40245
+(defvar coq-tactics847,40359
+(defvar coq-retractable-instruct850,40448
+(defvar coq-non-retractable-instruct853,40558
+(defvar coq-keywords857,40680
+(defvar coq-symbols864,40847
+(defvar coq-error-regexp 883,41060
+(defvar coq-id 886,41288
+(defvar coq-id-shy 887,41313
+(defvar coq-ids 889,41367
+(defun coq-first-abstr-regexp 891,41408
+(defvar coq-font-lock-terms894,41504
+(defconst coq-save-command-regexp-strict912,42305
+(defconst coq-save-command-regexp916,42472
+(defconst coq-save-with-hole-regexp920,42625
+(defconst coq-goal-command-regexp924,42783
+(defconst coq-goal-with-hole-regexp927,42883
+(defconst coq-decl-with-hole-regexp931,43015
+(defconst coq-defn-with-hole-regexp935,43147
+(defconst coq-with-with-hole-regexp945,43430
+(defvar coq-font-lock-keywords-1951,43720
+(defvar coq-font-lock-keywords 975,44992
+(defun coq-init-syntax-table 977,45050
+(defconst coq-generic-expression1006,45948
 
 coq/x-symbol-coq.el,1746
 (defvar x-symbol-coq-required-fonts 16,384
@@ -358,43 +364,42 @@ demoisa/demoisa.el,390
 (define-derived-mode demoisa-goals-mode 133,4387
 (defun demoisa-pre-shell-start 152,5169
 
-isar/isabelle-system.el,1471
-(defgroup isabelle 19,602
-(defcustom isabelle-web-page23,730
-(defcustom isa-isatool-command34,1025
-(defvar isatool-not-found 61,1970
-(defun isa-set-isatool-command 64,2083
-(defun isa-shell-command-to-string 84,2944
-(defun isa-getenv 90,3168
-(defcustom isabelle-program-name 109,3825
-(defvar isabelle-prog-name 135,4773
-(defun isabelle-command-line 138,4900
-(defun isabelle-choose-logic 162,5857
-(defun isa-tool-list-logics 184,6829
-(defun isa-view-doc 191,7067
-(defun isa-tool-list-docs 199,7292
-(defun isa-quit 217,8014
-(defconst isabelle-verbatim-regexp 224,8209
-(defun isabelle-verbatim 227,8350
-(defcustom isabelle-refresh-logics 234,8506
-(defcustom isabelle-logics-available 242,8833
-(defcustom isabelle-chosen-logic 250,9133
-(defconst isabelle-docs-menu 263,9601
-(defun isabelle-logics-menu-calculate 273,9994
-(defvar isabelle-time-to-refresh-logics 289,10503
-(defun isabelle-logics-menu-refresh 292,10596
-(defun isabelle-logics-menu-filter 309,11295
-(defun isabelle-menu-bar-update-logics 315,11505
-(defvar isabelle-logics-menu-entries 326,11861
-(defvar isabelle-logics-menu 328,11933
-(defun isabelle-load-isar-keywords 341,12551
-(defpgdefault menu-entries362,13292
-(defpgdefault help-menu-entries 365,13344
-(defpgdefault x-symbol-language 373,13538
-(defun isabelle-convert-idmarkup-to-subterm 396,14153
-(defun isabelle-create-span-menu 420,15165
-(defun isabelle-xml-sml-escapes 436,15610
-(defun isabelle-process-pgip 439,15711
+isar/isabelle-system.el,1446
+(defgroup isabelle 19,596
+(defcustom isabelle-web-page23,724
+(defcustom isa-isatool-command34,1019
+(defvar isatool-not-found 61,1964
+(defun isa-set-isatool-command 64,2077
+(defun isa-shell-command-to-string 84,2938
+(defun isa-getenv 90,3162
+(defcustom isabelle-program-name 109,3819
+(defvar isabelle-prog-name 135,4767
+(defun isabelle-command-line 138,4894
+(defun isabelle-choose-logic 162,5851
+(defun isa-tool-list-logics 184,6823
+(defun isa-view-doc 191,7061
+(defun isa-tool-list-docs 199,7286
+(defconst isabelle-verbatim-regexp 226,8319
+(defun isabelle-verbatim 229,8460
+(defcustom isabelle-refresh-logics 236,8616
+(defcustom isabelle-logics-available 244,8943
+(defcustom isabelle-chosen-logic 252,9243
+(defconst isabelle-docs-menu 265,9711
+(defun isabelle-logics-menu-calculate 275,10104
+(defvar isabelle-time-to-refresh-logics 291,10613
+(defun isabelle-logics-menu-refresh 294,10706
+(defun isabelle-logics-menu-filter 311,11405
+(defun isabelle-menu-bar-update-logics 317,11615
+(defvar isabelle-logics-menu-entries 328,11971
+(defvar isabelle-logics-menu 330,12043
+(defun isabelle-load-isar-keywords 343,12661
+(defpgdefault menu-entries364,13402
+(defpgdefault help-menu-entries 367,13454
+(defpgdefault x-symbol-language 375,13648
+(defun isabelle-convert-idmarkup-to-subterm 398,14263
+(defun isabelle-create-span-menu 422,15275
+(defun isabelle-xml-sml-escapes 438,15720
+(defun isabelle-process-pgip 441,15821
 
 isar/isar.el,1243
 (defcustom isar-keywords-name 28,586
@@ -764,7 +769,7 @@ phox/phox-pbrpm.el,512
 (defalias 'proof-pbrpm-left-paren-p proof-pbrpm-left-paren-p
288,10677
 (defalias 'proof-pbrpm-right-paren-p proof-pbrpm-right-paren-p
289,10739
 
-phox/phox-sym-lock.el,1352
+phox/phox-sym-lock.el,1353
 (defvar phox-sym-lock-sym-count 34,1617
 (defvar phox-sym-lock-ext-start 37,1687
 (defvar phox-sym-lock-ext-end 39,1809
@@ -778,24 +783,24 @@ phox/phox-sym-lock.el,1352
 (defun phox-sym-lock-gen-symbol 75,3138
 (defun phox-sym-lock-make-symbols-atomic 83,3441
 (defun phox-sym-lock-compute-font-size 110,4383
-(defvar phox-sym-lock-font-name147,5729
-(defun phox-sym-lock-set-foreground 185,7014
-(defun phox-sym-lock-translate-char 199,7623
-(defun phox-sym-lock-translate-char-or-string 207,7891
-(defun phox-sym-lock-remap-face 214,8118
-(defvar phox-sym-lock-clear-face234,9108
-(defun phox-sym-lock 246,9530
-(defun phox-sym-lock-rec 255,9934
-(defun phox-sym-lock-atom-face 261,10087
-(defun phox-sym-lock-pre-idle-hook-first 266,10383
-(defun phox-sym-lock-pre-idle-hook-last 274,10741
-(defun phox-sym-lock-enable 283,11116
-(defun phox-sym-lock-disable 296,11529
-(defun phox-sym-lock-mouse-face-enable 309,11947
-(defun phox-sym-lock-mouse-face-disable 316,12162
-(defun phox-sym-lock-font-lock-hook 323,12381
-(defun font-lock-set-defaults 338,13074
-(defun phox-sym-lock-patch-keywords 349,13452
+(defvar phox-sym-lock-font-name148,5803
+(defun phox-sym-lock-set-foreground 186,7088
+(defun phox-sym-lock-translate-char 200,7697
+(defun phox-sym-lock-translate-char-or-string 208,7965
+(defun phox-sym-lock-remap-face 215,8192
+(defvar phox-sym-lock-clear-face235,9182
+(defun phox-sym-lock 247,9604
+(defun phox-sym-lock-rec 256,10008
+(defun phox-sym-lock-atom-face 262,10161
+(defun phox-sym-lock-pre-idle-hook-first 267,10457
+(defun phox-sym-lock-pre-idle-hook-last 275,10815
+(defun phox-sym-lock-enable 284,11190
+(defun phox-sym-lock-disable 297,11603
+(defun phox-sym-lock-mouse-face-enable 310,12021
+(defun phox-sym-lock-mouse-face-disable 317,12236
+(defun phox-sym-lock-font-lock-hook 324,12455
+(defun font-lock-set-defaults 339,13148
+(defun phox-sym-lock-patch-keywords 350,13526
 
 phox/phox-tags.el,305
 (defun phox-tags-add-table(21,766
@@ -1039,117 +1044,117 @@ twelf/twelf-old.el,6958
 (defconst twelf-error-decl-regexp928,36662
 (defun looked-at-nth 932,36811
 (defun looked-at-nth-int 938,36993
-(defun twelf-error-parser 943,37108
-(defun twelf-error-decl 957,37711
-(defun twelf-mark-relative 963,37890
-(defun twelf-mark-absolute 979,38560
-(defun twelf-find-decl 1004,39446
-(defun twelf-next-error 1019,40002
-(defun twelf-goto-error 1087,42812
-(defun twelf-convert-standard-filename 1101,43350
-(defun string-member 1113,43845
-(defun twelf-config-proceed-p 1125,44337
-(defun twelf-save-if-config 1132,44599
-(defun twelf-config-save-some-buffers 1145,45071
-(defun twelf-save-check-config 1149,45236
-(defun twelf-check-config 1164,45792
-(defun twelf-save-check-file 1176,46232
-(defun twelf-buffer-substring 1192,46955
-(defun twelf-buffer-substring-dot 1198,47217
-(defun twelf-check-declaration 1204,47483
-(defun twelf-highlight-range-zmacs 1227,48543
-(defun twelf-focus 1233,48793
-(defun twelf-focus-noop 1239,49059
-(defun twelf-type-const 1322,52681
-(defvar twelf-server-mode-map 1439,57823
-(defconst twelf-server-cd-regexp 1451,58375
-(defun looked-at-string 1454,58515
-(defun twelf-server-directory-tracker 1458,58656
-(defun twelf-input-filter 1480,59830
-(defun twelf-server-mode 1486,60085
-(defun twelf-parse-config 1519,61302
-(defun twelf-server-read-config 1537,62194
-(defun twelf-server-sync-config 1546,62531
-(defun twelf-get-server-buffer 1576,64037
-(defun twelf-init-variables 1593,64711
-(defun twelf-server 1600,64924
-(defun twelf-server-process 1642,66838
-(defun twelf-server-display 1651,67244
-(defun display-server-buffer 1658,67518
-(defun twelf-server-send-command 1673,68250
-(defun twelf-accept-process-output 1694,69210
-(defun twelf-server-wait 1703,69649
-(defun twelf-server-quit 1745,71787
-(defun twelf-server-interrupt 1750,71908
-(defun twelf-reset 1755,72044
-(defun twelf-config-directory 1760,72188
-(defun twelf-server-configure 1771,72602
-(defun natp 1844,75894
-(defun twelf-read-nat 1848,75995
-(defun twelf-read-bool 1857,76262
-(defun twelf-read-limit 1863,76410
-(defun twelf-read-strategy 1873,76710
-(defun twelf-read-value 1879,76862
-(defun twelf-set 1883,77025
-(defun twelf-set-parm 1896,77502
-(defun track-parm 1905,77799
-(defun twelf-toggle-double-check 1910,77973
-(defun twelf-toggle-print-implicit 1916,78176
-(defun twelf-get 1922,78389
-(defun twelf-timers-reset 1936,79015
-(defun twelf-timers-show 1941,79135
-(defun twelf-timers-check 1947,79286
-(defun twelf-server-restart 1953,79451
-(defun twelf-config-mode 1969,80128
-(defun twelf-config-mode-check 1985,80727
-(defun twelf-tag 1994,81177
-(defun twelf-tag-files 2022,82441
-(default: *tags-errors*)2026,82744
-(defun twelf-tag-file 2047,83495
-(defun twelf-next-decl 2082,84717
-(defun skip-ahead 2107,85739
-(defun current-line-absolute 2119,86161
-(defun new-temp-buffer 2124,86371
-(defun rev-relativize 2135,86755
-(defvar twelf-sml-mode-map 2149,87215
-(defconst twelf-sml-prompt-regexp 2159,87593
-(defun expand-dir 2161,87648
-(defun twelf-sml-cd 2168,87909
-(defconst twelf-sml-cd-regexp 2180,88398
-(defun twelf-sml-directory-tracker 2183,88532
-(defun twelf-sml-mode 2199,89377
-(defun twelf-sml 2250,91311
-(defun switch-to-twelf-sml 2270,92271
-(defun display-twelf-sml-buffer 2281,92620
-(defun twelf-sml-send-string 2297,93336
-(defun twelf-sml-send-region 2302,93540
-(defun twelf-sml-send-query 2326,94746
-(defun twelf-sml-send-newline 2336,95143
-(defun twelf-sml-send-semicolon 2344,95471
-(defun twelf-sml-status 2352,95805
-(defvar twelf-sml-init 2374,96752
-(defun twelf-sml-set-mode 2377,96929
-(defun twelf-sml-quit 2403,98106
-(defun twelf-sml-process-buffer 2408,98218
-(defun twelf-sml-process 2412,98334
-(defvar twelf-to-twelf-sml-mode 2424,98850
-(defun install-twelf-to-twelf-sml-keybindings 2427,98935
-(defvar twelf-to-twelf-sml-mode-map 2437,99320
-(defun twelf-to-twelf-sml-mode 2448,99833
-(defconst twelf-at-point-menu2498,101700
-(defconst twelf-server-state-menu2508,102072
-(defconst twelf-error-menu2518,102389
-(defconst twelf-tags-menu2524,102533
-(defun twelf-toggle-server-display-commands 2534,102818
-(defconst twelf-options-menu2537,102942
-(defconst twelf-timers-menu2572,104680
-(defconst twelf-syntax-menu2585,105174
-(defun twelf-add-menu 2612,106040
-(defun twelf-remove-menu 2616,106142
-(defun twelf-reset-menu 2620,106240
-(defun twelf-server-add-menu 2647,107139
-(defun twelf-server-remove-menu 2651,107262
-(defun twelf-server-reset-menu 2655,107374
+(defun twelf-error-parser 943,37111
+(defun twelf-error-decl 957,37714
+(defun twelf-mark-relative 963,37893
+(defun twelf-mark-absolute 979,38563
+(defun twelf-find-decl 1004,39449
+(defun twelf-next-error 1019,40005
+(defun twelf-goto-error 1087,42815
+(defun twelf-convert-standard-filename 1101,43353
+(defun string-member 1113,43848
+(defun twelf-config-proceed-p 1125,44340
+(defun twelf-save-if-config 1132,44602
+(defun twelf-config-save-some-buffers 1145,45074
+(defun twelf-save-check-config 1149,45239
+(defun twelf-check-config 1164,45795
+(defun twelf-save-check-file 1176,46235
+(defun twelf-buffer-substring 1192,46958
+(defun twelf-buffer-substring-dot 1198,47220
+(defun twelf-check-declaration 1204,47486
+(defun twelf-highlight-range-zmacs 1227,48546
+(defun twelf-focus 1233,48796
+(defun twelf-focus-noop 1239,49062
+(defun twelf-type-const 1322,52684
+(defvar twelf-server-mode-map 1439,57826
+(defconst twelf-server-cd-regexp 1451,58378
+(defun looked-at-string 1454,58518
+(defun twelf-server-directory-tracker 1458,58659
+(defun twelf-input-filter 1480,59839
+(defun twelf-server-mode 1486,60094
+(defun twelf-parse-config 1519,61311
+(defun twelf-server-read-config 1537,62203
+(defun twelf-server-sync-config 1546,62540
+(defun twelf-get-server-buffer 1576,64046
+(defun twelf-init-variables 1593,64720
+(defun twelf-server 1600,64933
+(defun twelf-server-process 1642,66847
+(defun twelf-server-display 1651,67253
+(defun display-server-buffer 1658,67527
+(defun twelf-server-send-command 1673,68259
+(defun twelf-accept-process-output 1694,69219
+(defun twelf-server-wait 1703,69658
+(defun twelf-server-quit 1745,71796
+(defun twelf-server-interrupt 1750,71917
+(defun twelf-reset 1755,72053
+(defun twelf-config-directory 1760,72197
+(defun twelf-server-configure 1771,72611
+(defun natp 1844,75903
+(defun twelf-read-nat 1848,76004
+(defun twelf-read-bool 1857,76271
+(defun twelf-read-limit 1863,76419
+(defun twelf-read-strategy 1873,76722
+(defun twelf-read-value 1879,76874
+(defun twelf-set 1883,77037
+(defun twelf-set-parm 1896,77514
+(defun track-parm 1905,77811
+(defun twelf-toggle-double-check 1910,77985
+(defun twelf-toggle-print-implicit 1916,78188
+(defun twelf-get 1922,78401
+(defun twelf-timers-reset 1936,79027
+(defun twelf-timers-show 1941,79147
+(defun twelf-timers-check 1947,79298
+(defun twelf-server-restart 1953,79463
+(defun twelf-config-mode 1969,80140
+(defun twelf-config-mode-check 1985,80739
+(defun twelf-tag 1994,81189
+(defun twelf-tag-files 2022,82453
+(default: *tags-errors*)2026,82756
+(defun twelf-tag-file 2047,83507
+(defun twelf-next-decl 2082,84729
+(defun skip-ahead 2107,85751
+(defun current-line-absolute 2119,86173
+(defun new-temp-buffer 2124,86383
+(defun rev-relativize 2135,86767
+(defvar twelf-sml-mode-map 2149,87227
+(defconst twelf-sml-prompt-regexp 2159,87605
+(defun expand-dir 2161,87660
+(defun twelf-sml-cd 2168,87921
+(defconst twelf-sml-cd-regexp 2180,88410
+(defun twelf-sml-directory-tracker 2183,88544
+(defun twelf-sml-mode 2199,89389
+(defun twelf-sml 2250,91323
+(defun switch-to-twelf-sml 2270,92283
+(defun display-twelf-sml-buffer 2281,92632
+(defun twelf-sml-send-string 2297,93348
+(defun twelf-sml-send-region 2302,93552
+(defun twelf-sml-send-query 2326,94758
+(defun twelf-sml-send-newline 2336,95155
+(defun twelf-sml-send-semicolon 2344,95483
+(defun twelf-sml-status 2352,95817
+(defvar twelf-sml-init 2374,96764
+(defun twelf-sml-set-mode 2377,96941
+(defun twelf-sml-quit 2403,98118
+(defun twelf-sml-process-buffer 2408,98230
+(defun twelf-sml-process 2412,98346
+(defvar twelf-to-twelf-sml-mode 2424,98862
+(defun install-twelf-to-twelf-sml-keybindings 2427,98947
+(defvar twelf-to-twelf-sml-mode-map 2437,99332
+(defun twelf-to-twelf-sml-mode 2448,99845
+(defconst twelf-at-point-menu2498,101712
+(defconst twelf-server-state-menu2508,102084
+(defconst twelf-error-menu2518,102401
+(defconst twelf-tags-menu2524,102545
+(defun twelf-toggle-server-display-commands 2534,102830
+(defconst twelf-options-menu2537,102954
+(defconst twelf-timers-menu2572,104692
+(defconst twelf-syntax-menu2585,105186
+(defun twelf-add-menu 2612,106052
+(defun twelf-remove-menu 2616,106154
+(defun twelf-reset-menu 2620,106252
+(defun twelf-server-add-menu 2647,107151
+(defun twelf-server-remove-menu 2651,107274
+(defun twelf-server-reset-menu 2655,107386
 
 generic/pg-assoc.el,329
 (define-derived-mode proof-universal-keys-only-mode 20,563
@@ -1204,43 +1209,43 @@ generic/pg-pbrpm.el,1781
 (defvar pg-pbrpm-goal-description 15,440
 (defvar pg-pbrpm-windows-dialog-bug 16,479
 (defun pg-pbrpm-erase-buffer-menu 18,521
-(defun pg-pbrpm-menu-change-hook 25,726
-(defun pg-pbrpm-create-reset-buffer-menu 43,1303
-(defun pg-pbrpm-analyse-goal-buffer 57,1917
-(defun pg-pbrpm-button-action 118,4337
-(defun pg-pbrpm-exists 125,4563
-(defun pg-pbrpm-eliminate-id 129,4675
-(defun pg-pbrpm-build-menu 137,4923
-(defun pg-pbrpm-setup-span 197,7261
-(defun pg-pbrpm-run-command 257,9631
-(defun pg-pbrpm-get-pos-info 286,10942
-(defun pg-pbrpm-get-region-info 322,12084
-(defun auto-select-arround-pos 332,12409
-(defun pg-pbrpm-translate-position 344,12853
-(defun pg-pbrpm-process-click 350,13077
-(defvar pg-pbrpm-remember-region-selected-region 370,14081
-(defvar pg-pbrpm-regions-list 371,14135
-(defun pg-pbrpm-erase-regions-list 373,14171
-(defun pg-pbrpm-filter-regions-list 382,14480
-(defface pg-pbrpm-multiple-selection-face389,14743
-(defface pg-pbrpm-menu-input-face397,14948
-(defun pg-pbrpm-do-remember-region 405,15141
-(defun pg-pbrpm-remember-region-drag-up-hook 426,15992
-(defun pg-pbrpm-remember-region-click-hook 430,16163
-(defun pg-pbrpm-remember-region 435,16348
-(defun pg-pbrpm-process-region 449,17063
-(defun pg-pbrpm-process-regions-list 466,17786
-(defun pg-pbrpm-region-expression 470,17969
-(define-key proof-goals-mode-map 494,18905
-(define-key proof-goals-mode-map 495,18975
-(define-key proof-goals-mode-map 496,19052
-(define-key pg-span-context-menu-keymap 497,19132
-(define-key pg-span-context-menu-keymap 498,19209
-(define-key proof-mode-map 499,19292
-(define-key proof-mode-map 500,19356
-(define-key proof-mode-map 501,19427
-
-generic/pg-pgip.el,3554
+(defun pg-pbrpm-menu-change-hook 25,705
+(defun pg-pbrpm-create-reset-buffer-menu 43,1282
+(defun pg-pbrpm-analyse-goal-buffer 57,1896
+(defun pg-pbrpm-button-action 118,4316
+(defun pg-pbrpm-exists 125,4542
+(defun pg-pbrpm-eliminate-id 129,4654
+(defun pg-pbrpm-build-menu 137,4902
+(defun pg-pbrpm-setup-span 197,7219
+(defun pg-pbrpm-run-command 257,9550
+(defun pg-pbrpm-get-pos-info 286,10861
+(defun pg-pbrpm-get-region-info 322,12003
+(defun auto-select-arround-pos 332,12328
+(defun pg-pbrpm-translate-position 344,12772
+(defun pg-pbrpm-process-click 350,12996
+(defvar pg-pbrpm-remember-region-selected-region 370,14003
+(defvar pg-pbrpm-regions-list 371,14057
+(defun pg-pbrpm-erase-regions-list 373,14093
+(defun pg-pbrpm-filter-regions-list 382,14402
+(defface pg-pbrpm-multiple-selection-face389,14665
+(defface pg-pbrpm-menu-input-face397,14870
+(defun pg-pbrpm-do-remember-region 405,15063
+(defun pg-pbrpm-remember-region-drag-up-hook 426,15914
+(defun pg-pbrpm-remember-region-click-hook 430,16085
+(defun pg-pbrpm-remember-region 435,16270
+(defun pg-pbrpm-process-region 449,16985
+(defun pg-pbrpm-process-regions-list 466,17711
+(defun pg-pbrpm-region-expression 470,17894
+(define-key proof-goals-mode-map 495,18856
+(define-key proof-goals-mode-map 496,18926
+(define-key proof-goals-mode-map 497,19003
+(define-key pg-span-context-menu-keymap 498,19083
+(define-key pg-span-context-menu-keymap 499,19160
+(define-key proof-mode-map 500,19243
+(define-key proof-mode-map 501,19307
+(define-key proof-mode-map 502,19378
+
+generic/pg-pgip.el,2889
 (defalias 'pg-pgip-debug pg-pgip-debug
29,894
 (defalias 'pg-pgip-error pg-pgip-error
30,935
 (defalias 'pg-pgip-warning pg-pgip-warning
31,970
@@ -1256,87 +1261,71 @@ generic/pg-pgip.el,3554
 (defun pg-pgip-process-usespgip 114,4527
 (defun pg-pgip-process-usespgml 118,4691
 (defun pg-pgip-process-pgmlconfig 122,4855
-(defun pg-pgip-process-proverinfo 138,5463
-(defun pg-pgip-process-hasprefs 155,6128
-(defun pg-pgip-haspref 169,6760
-(defun pg-pgip-process-prefval 188,7539
-(defun pg-pgip-process-guiconfig 215,8248
-(defvar proof-assistant-idtables 222,8365
-(defun pg-pgip-process-ids 225,8482
-(defun pg-complete-idtable-symbol 251,9561
-(defalias 'pg-pgip-process-setids pg-pgip-process-setids
256,9653
-(defalias 'pg-pgip-process-addids pg-pgip-process-addids
257,9709
-(defalias 'pg-pgip-process-delids pg-pgip-process-delids
258,9765
-(defun pg-pgip-process-idvalue 261,9823
-(defun pg-pgip-process-menuadd 273,10160
-(defun pg-pgip-process-menudel 276,10203
-(defun pg-pgip-process-ready 285,10436
-(defun pg-pgip-process-cleardisplay 288,10477
-(defun pg-pgip-process-proofstate 302,10954
-(defun pg-pgip-process-normalresponse 306,11031
-(defun pg-pgip-process-errorresponse 310,11155
-(defun pg-pgip-process-scriptinsert 314,11278
-(defun pg-pgip-process-metainforesponse 319,11412
-(defun pg-pgip-process-informfileloaded 328,11653
-(defun pg-pgip-process-informfileretracted 334,11919
-(defun pg-pgip-process-brokerstatus 347,12393
-(defun pg-pgip-process-proveravailmsg 350,12441
-(defun pg-pgip-process-newprovermsg 353,12491
-(defun pg-pgip-process-proverstatusmsg 356,12539
-(defvar pg-pgip-srcids 365,12786
-(defun pg-pgip-process-newfile 369,12893
-(defun pg-pgip-process-filestatus 385,13481
-(defun pg-pgip-process-newobj 405,14136
-(defun pg-pgip-process-delobj 408,14178
-(defun pg-pgip-process-objectstatus 411,14220
-(defun pg-pgip-process-parsescript 425,14576
-(defun pg-pgip-get-pgiptype 448,15451
-(defun pg-pgip-default-for 468,16246
-(defun pg-pgip-subst-for 481,16641
-(defun pg-pgip-interpret-value 493,16984
-(defun pg-pgip-interpret-choice 511,17667
-(defun pg-pgip-get-icon 542,18740
-(defsubst pg-pgip-get-name 546,18888
-(defsubst pg-pgip-get-version 549,19005
-(defsubst pg-pgip-get-descr 552,19128
-(defsubst pg-pgip-get-thmname 555,19247
-(defsubst pg-pgip-get-thyname 558,19370
-(defsubst pg-pgip-get-url 561,19493
-(defsubst pg-pgip-get-srcid 564,19608
-(defsubst pg-pgip-get-proverid 567,19727
-(defsubst pg-pgip-get-symname 570,19852
-(defsubst pg-pgip-get-prefcat 573,19972
-(defsubst pg-pgip-get-default 576,20100
-(defsubst pg-pgip-get-objtype 579,20223
-(defsubst pg-pgip-get-value 582,20346
-(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext
585,20416
-(defun pg-pgip-get-pgmltext 587,20475
-(defun pg-pgip-string-of-command 596,20710
-(defconst pg-pgip-id613,21471
-(defvar pg-pgip-refseq 619,21751
-(defvar pg-pgip-refid 621,21849
-(defvar pg-pgip-seq 624,21943
-(defun pg-pgip-assemble-packet 626,22007
-(defun pg-pgip-issue 644,22822
-(defun pg-pgip-maybe-askpgip 661,23435
-(defun pg-pgip-askprefs 667,23626
-(defun pg-pgip-askids 671,23740
-(defun pg-pgip-reset 684,24031
-(defconst pg-pgip-start-element-regexp 715,24729
-(defconst pg-pgip-end-element-regexp 716,24781
+(defun pg-pgip-process-proverinfo 138,5474
+(defun pg-pgip-process-hasprefs 155,6139
+(defun pg-pgip-haspref 169,6771
+(defun pg-pgip-process-prefval 188,7550
+(defun pg-pgip-process-guiconfig 215,8259
+(defvar proof-assistant-idtables 222,8376
+(defun pg-pgip-process-ids 225,8493
+(defun pg-complete-idtable-symbol 251,9572
+(defalias 'pg-pgip-process-setids pg-pgip-process-setids
256,9664
+(defalias 'pg-pgip-process-addids pg-pgip-process-addids
257,9720
+(defalias 'pg-pgip-process-delids pg-pgip-process-delids
258,9776
+(defun pg-pgip-process-idvalue 261,9834
+(defun pg-pgip-process-menuadd 273,10171
+(defun pg-pgip-process-menudel 276,10214
+(defun pg-pgip-process-ready 285,10447
+(defun pg-pgip-process-cleardisplay 288,10488
+(defun pg-pgip-process-proofstate 302,10965
+(defun pg-pgip-process-normalresponse 306,11042
+(defun pg-pgip-process-errorresponse 310,11166
+(defun pg-pgip-process-scriptinsert 314,11289
+(defun pg-pgip-process-metainforesponse 319,11423
+(defun pg-pgip-process-informfileloaded 328,11664
+(defun pg-pgip-process-informfileretracted 334,11931
+(defun pg-pgip-process-brokerstatus 347,12408
+(defun pg-pgip-process-proveravailmsg 350,12456
+(defun pg-pgip-process-newprovermsg 353,12506
+(defun pg-pgip-process-proverstatusmsg 356,12554
+(defvar pg-pgip-srcids 365,12801
+(defun pg-pgip-process-newfile 369,12908
+(defun pg-pgip-process-filestatus 385,13496
+(defun pg-pgip-process-newobj 405,14151
+(defun pg-pgip-process-delobj 408,14193
+(defun pg-pgip-process-objectstatus 411,14235
+(defun pg-pgip-process-parsescript 425,14591
+(defun pg-pgip-get-pgiptype 448,15466
+(defun pg-pgip-default-for 468,16263
+(defun pg-pgip-subst-for 481,16658
+(defun pg-pgip-interpret-value 493,17001
+(defun pg-pgip-interpret-choice 511,17687
+(defun pg-pgip-string-of-command 542,18707
+(defconst pg-pgip-id559,19468
+(defvar pg-pgip-refseq 565,19748
+(defvar pg-pgip-refid 567,19846
+(defvar pg-pgip-seq 570,19940
+(defun pg-pgip-assemble-packet 572,20004
+(defun pg-pgip-issue 590,20819
+(defun pg-pgip-maybe-askpgip 607,21432
+(defun pg-pgip-askprefs 613,21623
+(defun pg-pgip-askids 617,21737
+(defun pg-pgip-reset 630,22028
+(defconst pg-pgip-start-element-regexp 661,22726
+(defconst pg-pgip-end-element-regexp 662,22778
 
 generic/pg-pgip-old.el,456
 (defun pg-pgip-process-oldhaspref 18,633
 (defun pg-pgip-process-haspref 21,730
 (defun pg-pgip-old-interpret-bool 57,2158
 (defun pg-pgip-old-interpret-int 66,2442
-(defun pg-pgip-old-interpret-string 71,2609
-(defun pg-pgip-old-interpret-choice 74,2663
-(defun pg-pgip-old-interpret-value 94,3382
-(defun pg-pgip-old-default-for 113,3928
-(defun pg-pgip-old-subst-for 124,4252
-(defun pg-pgip-old-get-type 131,4417
-(defun pg-pgip-old-pgiptype 138,4633
+(defun pg-pgip-old-interpret-string 71,2615
+(defun pg-pgip-old-interpret-choice 74,2669
+(defun pg-pgip-old-interpret-value 94,3388
+(defun pg-pgip-old-default-for 113,3934
+(defun pg-pgip-old-subst-for 124,4258
+(defun pg-pgip-old-get-type 131,4423
+(defun pg-pgip-old-pgiptype 138,4639
 
 generic/pg-response.el,1188
 (define-derived-mode proof-response-mode 25,617
@@ -1360,12 +1349,12 @@ generic/pg-response.el,1188
 (defun pg-response-clear-displays 331,12432
 (defvar pg-response-next-error 349,13011
 (defun proof-next-error 353,13133
-(defun pg-response-has-error-location 433,16067
-(defvar proof-trace-last-fontify-pos 456,16900
-(defun proof-trace-fontify-pos 458,16943
-(defun proof-trace-buffer-display 466,17257
-(defun proof-trace-buffer-finish 490,18230
-(defun pg-thms-buffer-clear 511,18809
+(defun pg-response-has-error-location 433,16073
+(defvar proof-trace-last-fontify-pos 456,16906
+(defun proof-trace-fontify-pos 458,16949
+(defun proof-trace-buffer-display 466,17263
+(defun proof-trace-buffer-finish 490,18236
+(defun pg-thms-buffer-clear 511,18815
 
 generic/pg-thymodes.el,152
 (defmacro pg-defthymode 19,466
@@ -1374,7 +1363,7 @@ generic/pg-thymodes.el,152
 (defun pg-modesym 78,2520
 (defun pg-modesymval 82,2634
 
-generic/pg-user.el,2304
+generic/pg-user.el,2335
 (defmacro proof-maybe-save-point 21,410
 (defun proof-maybe-follow-locked-end 29,612
 (defun proof-assert-next-command-interactive 43,977
@@ -1407,27 +1396,28 @@ generic/pg-user.el,2304
 (defun pg-insert-last-output-as-comment 681,22596
 (defun pg-copy-span-contents 712,23824
 (defun pg-numth-span-higher-or-lower 729,24384
-(defun pg-control-span-of 755,25135
-(defun pg-move-span-contents 761,25339
-(defun pg-fixup-children-span 815,27563
-(defun pg-move-region-down 822,27771
-(defun pg-move-region-up 831,28065
-(defun proof-forward-command 861,28905
-(defun proof-backward-command 882,29627
-(defvar pg-span-context-menu-keymap898,29871
-(defun pg-span-for-event 914,30298
-(defun pg-span-context-menu 925,30682
-(defun pg-toggle-visibility 940,31142
-(defun pg-create-in-span-context-menu 950,31464
-(defun pg-goals-buffers-hint 1022,34017
-(defun pg-slow-fontify-tracing-hint 1025,34184
-(defun pg-response-buffers-hint 1028,34340
-(defun pg-jump-to-end-hint 1037,34689
-(defun pg-processing-complete-hint 1040,34805
-(defun pg-next-error-hint 1056,35491
-(defun pg-hint 1060,35628
-(defun pg-identifier-under-mouse-query 1079,36304
-(defun proof-imenu-enable 1124,37931
+(defun pg-control-span-of 755,25131
+(defun pg-move-span-contents 761,25335
+(defun pg-fixup-children-span 815,27559
+(defun pg-move-region-down 822,27762
+(defun pg-move-region-up 831,28056
+(defun proof-forward-command 861,28896
+(defun proof-backward-command 882,29618
+(defvar pg-span-context-menu-keymap898,29862
+(defun pg-span-for-event 914,30289
+(defun pg-span-context-menu 925,30673
+(defun pg-toggle-visibility 940,31133
+(defun pg-create-in-span-context-menu 950,31455
+(defun pg-span-undo 983,32807
+(defun pg-goals-buffers-hint 1029,34217
+(defun pg-slow-fontify-tracing-hint 1032,34384
+(defun pg-response-buffers-hint 1035,34540
+(defun pg-jump-to-end-hint 1044,34889
+(defun pg-processing-complete-hint 1047,35005
+(defun pg-next-error-hint 1063,35691
+(defun pg-hint 1067,35828
+(defun pg-identifier-under-mouse-query 1086,36504
+(defun proof-imenu-enable 1131,38131
 
 generic/pg-xhtml.el,392
 (defvar pg-xhtml-dir 17,423
@@ -1436,12 +1426,12 @@ generic/pg-xhtml.el,392
 (defun pg-xhtml-next-file 35,928
 (defvar pg-xhtml-header 47,1159
 (defmacro pg-xhtml-write-tempfile 53,1400
-(defun pg-xhtml-cleanup-tempdir 71,1990
-(defvar pg-mozilla-prog-name 75,2121
-(defun pg-xhtml-display-file-mozilla 79,2229
-(defalias 'pg-xhtml-display-file pg-xhtml-display-file
84,2402
+(defun pg-xhtml-cleanup-tempdir 71,1996
+(defvar pg-mozilla-prog-name 75,2127
+(defun pg-xhtml-display-file-mozilla 79,2235
+(defalias 'pg-xhtml-display-file pg-xhtml-display-file
84,2408
 
-generic/pg-xml.el,447
+generic/pg-xml.el,1096
 (defun pg-xml-parse-string 40,1169
 (defun pg-xml-parse-buffer 51,1503
 (defun pg-xml-get-attr 73,2236
@@ -1455,9 +1445,25 @@ generic/pg-xml.el,447
 (defun pg-xml-string-of 124,3982
 (defun pg-xml-output-internal 135,4354
 (defun pg-xml-cdata 169,5504
-
-generic/proof-autoloads.el,80
-(defalias 'proof-x-symbol-decode-region proof-x-symbol-decode-region
250,10161
+(defun pg-pgip-get-icon 177,5697
+(defsubst pg-pgip-get-name 181,5845
+(defsubst pg-pgip-get-version 184,5962
+(defsubst pg-pgip-get-descr 187,6085
+(defsubst pg-pgip-get-thmname 190,6204
+(defsubst pg-pgip-get-thyname 193,6327
+(defsubst pg-pgip-get-url 196,6450
+(defsubst pg-pgip-get-srcid 199,6565
+(defsubst pg-pgip-get-proverid 202,6684
+(defsubst pg-pgip-get-symname 205,6809
+(defsubst pg-pgip-get-prefcat 208,6929
+(defsubst pg-pgip-get-default 211,7057
+(defsubst pg-pgip-get-objtype 214,7180
+(defsubst pg-pgip-get-value 217,7303
+(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext
220,7373
+(defun pg-pgip-get-pgmltext 222,7432
+
+generic/proof-autoloads.el,57
+(defalias (quote proof-x-symbol-decode-region)407,13794
 
 generic/proof-config.el,11148
 (defgroup proof-user-options 85,3232
@@ -1524,171 +1530,171 @@ generic/proof-config.el,11148
 (defcustom proof-save-command 726,25697
 (defcustom proof-find-theorems-command 734,26007
 (defconst proof-toolbar-entries-default741,26316
-(defpgcustom toolbar-entries 773,28138
-(defcustom proof-assistant-true-value 791,28859
-(defcustom proof-assistant-false-value 797,29049
-(defcustom proof-assistant-format-int-fn 803,29243
-(defcustom proof-assistant-format-string-fn 810,29492
-(defcustom proof-assistant-setting-format 817,29759
-(defgroup proof-script 839,30454
-(defcustom proof-terminal-char 844,30584
-(defcustom proof-script-sexp-commands 854,30988
-(defcustom proof-script-command-end-regexp 865,31458
-(defcustom proof-script-command-start-regexp 883,32277
-(defcustom proof-script-use-old-parser 894,32739
-(defcustom proof-script-integral-proofs 906,33228
-(defcustom proof-script-fly-past-comments 921,33884
-(defcustom proof-script-parse-function 928,34201
-(defcustom proof-script-comment-start 946,34847
-(defcustom proof-script-comment-start-regexp 957,35282
-(defcustom proof-script-comment-end 965,35599
-(defcustom proof-script-comment-end-regexp 977,36017
-(defcustom pg-insert-output-as-comment-fn 985,36328
-(defcustom proof-string-start-regexp 991,36580
-(defcustom proof-string-end-regexp 996,36745
-(defcustom proof-case-fold-search 1001,36906
-(defcustom proof-save-command-regexp 1010,37322
-(defcustom proof-save-with-hole-regexp 1015,37433
-(defcustom proof-save-with-hole-result 1027,37885
-(defcustom proof-goal-command-regexp 1038,38349
-(defcustom proof-goal-with-hole-regexp 1047,38741
-(defcustom proof-goal-with-hole-result 1059,39185
-(defcustom proof-non-undoables-regexp 1069,39584
-(defcustom proof-nested-undo-regexp 1080,40040
-(defcustom proof-ignore-for-undo-count 1096,40752
-(defcustom proof-script-next-entity-regexps 1104,41055
-(defcustom proof-script-find-next-entity-fn1148,42789
-(defcustom proof-script-imenu-generic-expression 1168,43619
-(defcustom proof-goal-command-p 1186,44474
-(defcustom proof-really-save-command-p 1213,45915
-(defcustom proof-completed-proof-behaviour 1225,46376
-(defcustom proof-count-undos-fn 1253,47736
-(defconst proof-no-command 1288,49337
-(defcustom proof-find-and-forget-fn 1293,49541
-(defcustom proof-forget-id-command 1310,50252
-(defcustom pg-topterm-goalhyplit-fn 1320,50610
-(defcustom proof-kill-goal-command 1332,51166
-(defcustom proof-undo-n-times-cmd 1346,51676
-(defcustom proof-nested-goals-history-p 1360,52225
-(defcustom proof-state-preserving-p 1369,52563
-(defcustom proof-activate-scripting-hook 1379,53033
-(defcustom proof-deactivate-scripting-hook 1398,53811
-(defcustom proof-indent 1411,54176
-(defcustom proof-indent-hang 1416,54283
-(defcustom proof-indent-enclose-offset 1421,54409
-(defcustom proof-indent-open-offset 1426,54551
-(defcustom proof-indent-close-offset 1431,54688
-(defcustom proof-indent-any-regexp 1436,54826
-(defcustom proof-indent-inner-regexp 1441,54986
-(defcustom proof-indent-enclose-regexp 1446,55140
-(defcustom proof-indent-open-regexp 1451,55294
-(defcustom proof-indent-close-regexp 1456,55446
-(defcustom proof-script-font-lock-keywords 1462,55600
-(defcustom proof-script-syntax-table-entries 1470,55923
-(defcustom proof-script-span-context-menu-extensions 1488,56320
-(defgroup proof-shell 1514,57109
-(defcustom proof-prog-name 1524,57280
-(defpgcustom prog-args 1537,57915
-(defpgcustom prog-env 1550,58490
-(defcustom proof-shell-auto-terminate-commands 1559,58916
-(defcustom proof-shell-pre-sync-init-cmd 1568,59313
-(defcustom proof-shell-init-cmd 1582,59872
-(defcustom proof-shell-restart-cmd 1593,60342
-(defcustom proof-shell-quit-cmd 1598,60497
-(defcustom proof-shell-quit-timeout 1603,60664
-(defcustom proof-shell-cd-cmd 1613,61112
-(defcustom proof-shell-start-silent-cmd 1630,61779
-(defcustom proof-shell-stop-silent-cmd 1639,62155
-(defcustom proof-shell-silent-threshold 1648,62492
-(defcustom  proof-shell-inform-file-processed-cmd 1656,62826
-(defcustom  proof-shell-inform-file-retracted-cmd 1677,63749
-(defcustom proof-auto-multiple-files 1705,65020
-(defcustom proof-cannot-reopen-processed-files 1720,65741
-(defcustom proof-shell-require-command-regexp 1734,66408
-(defcustom proof-done-advancing-require-function 1745,66870
-(defcustom proof-shell-quiet-errors 1751,67110
-(defcustom proof-shell-prompt-pattern 1764,67444
-(defcustom proof-shell-wakeup-char 1774,67866
-(defcustom proof-shell-annotated-prompt-regexp 1780,68097
-(defcustom proof-shell-abort-goal-regexp 1796,68737
-(defcustom proof-shell-error-regexp 1801,68872
-(defcustom proof-shell-truncate-before-error 1821,69666
-(defcustom pg-next-error-regexp 1835,70209
-(defcustom pg-next-error-filename-regexp 1850,70819
-(defcustom pg-next-error-extract-filename 1874,71857
-(defcustom proof-shell-interrupt-regexp 1881,72100
-(defcustom proof-shell-proof-completed-regexp 1895,72692
-(defcustom proof-shell-clear-response-regexp 1908,73200
-(defcustom proof-shell-clear-goals-regexp 1915,73499
-(defcustom proof-shell-start-goals-regexp 1922,73792
-(defcustom proof-shell-end-goals-regexp 1930,74159
-(defcustom proof-shell-eager-annotation-start 1936,74401
-(defcustom proof-shell-eager-annotation-start-length 1954,75139
-(defcustom proof-shell-eager-annotation-end 1965,75566
-(defcustom proof-shell-assumption-regexp 1981,76242
-(defcustom proof-shell-process-file 1991,76657
-(defcustom proof-shell-retract-files-regexp 2013,77609
-(defcustom proof-shell-compute-new-files-list 2022,77945
-(defcustom pg-use-specials-for-fontify 2034,78490
-(defcustom pg-special-char-regexp 2042,78838
-(defcustom proof-shell-set-elisp-variable-regexp 2047,78982
-(defcustom proof-shell-match-pgip-cmd 2080,80454
-(defcustom proof-shell-issue-pgip-cmd 2089,80784
-(defcustom proof-shell-query-dependencies-cmd 2098,81140
-(defcustom proof-shell-theorem-dependency-list-regexp 2105,81400
-(defcustom proof-shell-theorem-dependency-list-split 2121,82060
-(defcustom proof-shell-show-dependency-cmd 2130,82485
-(defcustom proof-shell-identifier-under-mouse-cmd 2137,82754
-(defcustom proof-shell-trace-output-regexp 2160,83835
-(defcustom proof-shell-thms-output-regexp 2176,84379
-(defcustom proof-shell-unicode 2189,84765
-(defcustom proof-shell-filename-escapes 2197,85093
-(defcustom proof-shell-process-connection-type 2214,85773
-(defcustom proof-shell-strip-crs-from-input 2237,86820
-(defcustom proof-shell-strip-crs-from-output 2249,87309
-(defcustom proof-shell-insert-hook 2257,87677
-(defcustom proof-pre-shell-start-hook 2297,89641
-(defcustom proof-shell-handle-delayed-output-hook2313,90113
-(defcustom proof-shell-handle-error-or-interrupt-hook2319,90328
-(defcustom proof-shell-pre-interrupt-hook2337,91077
-(defcustom proof-shell-process-output-system-specific 2345,91349
-(defcustom proof-state-change-hook 2364,92214
-(defcustom proof-shell-font-lock-keywords 2375,92596
-(defcustom proof-shell-syntax-table-entries 2383,92924
-(defgroup proof-goals 2401,93296
-(defcustom pg-subterm-first-special-char 2406,93417
-(defcustom pg-subterm-anns-use-stack 2414,93729
-(defcustom pg-goals-change-goal 2423,94033
-(defcustom pbp-goal-command 2428,94148
-(defcustom pbp-hyp-command 2433,94304
-(defcustom pg-subterm-help-cmd 2438,94466
-(defcustom pg-goals-error-regexp 2445,94702
-(defcustom proof-shell-result-start 2450,94862
-(defcustom proof-shell-result-end 2456,95096
-(defcustom pg-subterm-start-char 2462,95309
-(defcustom pg-subterm-sep-char 2476,95891
-(defcustom pg-subterm-end-char 2482,96070
-(defcustom pg-topterm-regexp 2488,96227
-(defcustom proof-goals-font-lock-keywords 2505,96830
-(defcustom proof-resp-font-lock-keywords 2519,97509
-(defcustom pg-before-fontify-output-hook 2531,98087
-(defcustom pg-after-fontify-output-hook 2539,98447
-(defgroup proof-x-symbol 2551,98701
-(defcustom proof-xsym-extra-modes 2556,98829
-(defcustom proof-xsym-font-lock-keywords 2569,99458
-(defcustom proof-xsym-activate-command 2577,99835
-(defcustom proof-xsym-deactivate-command 2584,100071
-(defpgcustom x-symbol-language 2591,100313
-(defpgcustom favourites 2606,100760
-(defpgcustom menu-entries 2611,100950
-(defpgcustom help-menu-entries 2618,101187
-(defpgcustom keymap 2625,101450
-(defpgcustom completion-table 2630,101621
-(defpgcustom tags-program 2640,101986
-(defcustom proof-general-name 2652,102159
-(defcustom proof-general-home-page2657,102316
-(defcustom proof-unnamed-theorem-name2663,102475
-(defcustom proof-universal-keys2671,102751
+(defpgcustom toolbar-entries 775,28234
+(defcustom proof-assistant-true-value 793,28955
+(defcustom proof-assistant-false-value 799,29145
+(defcustom proof-assistant-format-int-fn 805,29339
+(defcustom proof-assistant-format-string-fn 812,29588
+(defcustom proof-assistant-setting-format 819,29855
+(defgroup proof-script 841,30550
+(defcustom proof-terminal-char 846,30680
+(defcustom proof-script-sexp-commands 856,31084
+(defcustom proof-script-command-end-regexp 867,31554
+(defcustom proof-script-command-start-regexp 885,32373
+(defcustom proof-script-use-old-parser 896,32835
+(defcustom proof-script-integral-proofs 908,33324
+(defcustom proof-script-fly-past-comments 923,33980
+(defcustom proof-script-parse-function 930,34297
+(defcustom proof-script-comment-start 948,34943
+(defcustom proof-script-comment-start-regexp 959,35378
+(defcustom proof-script-comment-end 967,35695
+(defcustom proof-script-comment-end-regexp 979,36113
+(defcustom pg-insert-output-as-comment-fn 987,36424
+(defcustom proof-string-start-regexp 993,36676
+(defcustom proof-string-end-regexp 998,36841
+(defcustom proof-case-fold-search 1003,37002
+(defcustom proof-save-command-regexp 1012,37418
+(defcustom proof-save-with-hole-regexp 1017,37529
+(defcustom proof-save-with-hole-result 1029,37981
+(defcustom proof-goal-command-regexp 1040,38445
+(defcustom proof-goal-with-hole-regexp 1049,38837
+(defcustom proof-goal-with-hole-result 1061,39281
+(defcustom proof-non-undoables-regexp 1071,39680
+(defcustom proof-nested-undo-regexp 1082,40136
+(defcustom proof-ignore-for-undo-count 1098,40848
+(defcustom proof-script-next-entity-regexps 1106,41151
+(defcustom proof-script-find-next-entity-fn1150,42885
+(defcustom proof-script-imenu-generic-expression 1170,43715
+(defcustom proof-goal-command-p 1188,44570
+(defcustom proof-really-save-command-p 1215,46011
+(defcustom proof-completed-proof-behaviour 1227,46472
+(defcustom proof-count-undos-fn 1255,47832
+(defconst proof-no-command 1290,49433
+(defcustom proof-find-and-forget-fn 1295,49637
+(defcustom proof-forget-id-command 1312,50348
+(defcustom pg-topterm-goalhyplit-fn 1322,50706
+(defcustom proof-kill-goal-command 1334,51262
+(defcustom proof-undo-n-times-cmd 1348,51772
+(defcustom proof-nested-goals-history-p 1362,52321
+(defcustom proof-state-preserving-p 1371,52659
+(defcustom proof-activate-scripting-hook 1381,53129
+(defcustom proof-deactivate-scripting-hook 1400,53907
+(defcustom proof-indent 1413,54272
+(defcustom proof-indent-hang 1418,54379
+(defcustom proof-indent-enclose-offset 1423,54505
+(defcustom proof-indent-open-offset 1428,54647
+(defcustom proof-indent-close-offset 1433,54784
+(defcustom proof-indent-any-regexp 1438,54922
+(defcustom proof-indent-inner-regexp 1443,55082
+(defcustom proof-indent-enclose-regexp 1448,55236
+(defcustom proof-indent-open-regexp 1453,55390
+(defcustom proof-indent-close-regexp 1458,55542
+(defcustom proof-script-font-lock-keywords 1464,55696
+(defcustom proof-script-syntax-table-entries 1472,56019
+(defcustom proof-script-span-context-menu-extensions 1490,56416
+(defgroup proof-shell 1516,57205
+(defcustom proof-prog-name 1526,57376
+(defpgcustom prog-args 1539,58011
+(defpgcustom prog-env 1552,58586
+(defcustom proof-shell-auto-terminate-commands 1561,59012
+(defcustom proof-shell-pre-sync-init-cmd 1570,59409
+(defcustom proof-shell-init-cmd 1584,59968
+(defcustom proof-shell-restart-cmd 1595,60438
+(defcustom proof-shell-quit-cmd 1600,60593
+(defcustom proof-shell-quit-timeout 1605,60760
+(defcustom proof-shell-cd-cmd 1615,61208
+(defcustom proof-shell-start-silent-cmd 1632,61875
+(defcustom proof-shell-stop-silent-cmd 1641,62251
+(defcustom proof-shell-silent-threshold 1650,62588
+(defcustom  proof-shell-inform-file-processed-cmd 1658,62922
+(defcustom  proof-shell-inform-file-retracted-cmd 1679,63845
+(defcustom proof-auto-multiple-files 1707,65116
+(defcustom proof-cannot-reopen-processed-files 1722,65837
+(defcustom proof-shell-require-command-regexp 1736,66504
+(defcustom proof-done-advancing-require-function 1747,66966
+(defcustom proof-shell-quiet-errors 1753,67206
+(defcustom proof-shell-prompt-pattern 1766,67540
+(defcustom proof-shell-wakeup-char 1776,67962
+(defcustom proof-shell-annotated-prompt-regexp 1782,68193
+(defcustom proof-shell-abort-goal-regexp 1798,68833
+(defcustom proof-shell-error-regexp 1803,68968
+(defcustom proof-shell-truncate-before-error 1823,69762
+(defcustom pg-next-error-regexp 1837,70305
+(defcustom pg-next-error-filename-regexp 1852,70915
+(defcustom pg-next-error-extract-filename 1876,71953
+(defcustom proof-shell-interrupt-regexp 1883,72196
+(defcustom proof-shell-proof-completed-regexp 1897,72788
+(defcustom proof-shell-clear-response-regexp 1910,73296
+(defcustom proof-shell-clear-goals-regexp 1917,73595
+(defcustom proof-shell-start-goals-regexp 1924,73888
+(defcustom proof-shell-end-goals-regexp 1932,74255
+(defcustom proof-shell-eager-annotation-start 1938,74497
+(defcustom proof-shell-eager-annotation-start-length 1956,75235
+(defcustom proof-shell-eager-annotation-end 1967,75662
+(defcustom proof-shell-assumption-regexp 1983,76338
+(defcustom proof-shell-process-file 1993,76753
+(defcustom proof-shell-retract-files-regexp 2015,77705
+(defcustom proof-shell-compute-new-files-list 2024,78041
+(defcustom pg-use-specials-for-fontify 2036,78586
+(defcustom pg-special-char-regexp 2044,78934
+(defcustom proof-shell-set-elisp-variable-regexp 2049,79078
+(defcustom proof-shell-match-pgip-cmd 2082,80550
+(defcustom proof-shell-issue-pgip-cmd 2091,80880
+(defcustom proof-shell-query-dependencies-cmd 2100,81236
+(defcustom proof-shell-theorem-dependency-list-regexp 2107,81496
+(defcustom proof-shell-theorem-dependency-list-split 2123,82156
+(defcustom proof-shell-show-dependency-cmd 2132,82581
+(defcustom proof-shell-identifier-under-mouse-cmd 2139,82850
+(defcustom proof-shell-trace-output-regexp 2162,83931
+(defcustom proof-shell-thms-output-regexp 2178,84475
+(defcustom proof-shell-unicode 2191,84861
+(defcustom proof-shell-filename-escapes 2199,85189
+(defcustom proof-shell-process-connection-type 2216,85869
+(defcustom proof-shell-strip-crs-from-input 2239,86916
+(defcustom proof-shell-strip-crs-from-output 2251,87405
+(defcustom proof-shell-insert-hook 2259,87773
+(defcustom proof-pre-shell-start-hook 2299,89737
+(defcustom proof-shell-handle-delayed-output-hook2315,90209
+(defcustom proof-shell-handle-error-or-interrupt-hook2321,90424
+(defcustom proof-shell-pre-interrupt-hook2339,91173
+(defcustom proof-shell-process-output-system-specific 2347,91445
+(defcustom proof-state-change-hook 2366,92310
+(defcustom proof-shell-font-lock-keywords 2377,92692
+(defcustom proof-shell-syntax-table-entries 2385,93020
+(defgroup proof-goals 2403,93392
+(defcustom pg-subterm-first-special-char 2408,93513
+(defcustom pg-subterm-anns-use-stack 2416,93825
+(defcustom pg-goals-change-goal 2425,94129
+(defcustom pbp-goal-command 2430,94244
+(defcustom pbp-hyp-command 2435,94400
+(defcustom pg-subterm-help-cmd 2440,94562
+(defcustom pg-goals-error-regexp 2447,94798
+(defcustom proof-shell-result-start 2452,94958
+(defcustom proof-shell-result-end 2458,95192
+(defcustom pg-subterm-start-char 2464,95405
+(defcustom pg-subterm-sep-char 2478,95987
+(defcustom pg-subterm-end-char 2484,96166
+(defcustom pg-topterm-regexp 2490,96323
+(defcustom proof-goals-font-lock-keywords 2507,96926
+(defcustom proof-resp-font-lock-keywords 2521,97605
+(defcustom pg-before-fontify-output-hook 2533,98183
+(defcustom pg-after-fontify-output-hook 2541,98543
+(defgroup proof-x-symbol 2553,98797
+(defcustom proof-xsym-extra-modes 2558,98925
+(defcustom proof-xsym-font-lock-keywords 2571,99554
+(defcustom proof-xsym-activate-command 2579,99931
+(defcustom proof-xsym-deactivate-command 2586,100167
+(defpgcustom x-symbol-language 2593,100409
+(defpgcustom favourites 2608,100856
+(defpgcustom menu-entries 2613,101046
+(defpgcustom help-menu-entries 2620,101283
+(defpgcustom keymap 2627,101546
+(defpgcustom completion-table 2632,101717
+(defpgcustom tags-program 2642,102082
+(defcustom proof-general-name 2654,102255
+(defcustom proof-general-home-page2659,102412
+(defcustom proof-unnamed-theorem-name2665,102571
+(defcustom proof-universal-keys2671,102755
 
 generic/proof-depends.el,824
 (defvar proof-thm-names-of-files 19,540
@@ -1741,6 +1747,12 @@ generic/proof-indent.el,219
 (defun proof-indent-calculate 55,1859
 (defun proof-indent-line 74,2575
 
+generic/proof-maths-menu.el,173
+(defun proof-maths-menu-support-available 24,770
+(defvar maths-menu-modes-list 44,1601
+(defun proof-maths-menu-set-global 46,1637
+(defun proof-maths-menu-enable 56,2005
+
 generic/proof-menu.el,2739
 (defvar proof-display-some-buffers-count 19,468
 (defun proof-display-some-buffers 21,513
@@ -1769,57 +1781,57 @@ generic/proof-menu.el,2739
 (define-key map 121,5027
 (defun proof-menu-define-main 141,5617
 (defun proof-menu-define-specific 151,5818
-(defun proof-assistant-menu-update 186,6835
-(defvar proof-help-menu203,7443
-(defvar proof-show-hide-menu211,7721
-(defvar proof-buffer-menu220,8034
-(defconst proof-quick-opts-menu278,10124
-(defun proof-quick-opts-vars 391,14681
-(defun proof-quick-opts-changed-from-defaults-p 415,15395
-(defun proof-quick-opts-changed-from-saved-p 419,15500
-(defun proof-quick-opts-save 430,15852
-(defun proof-quick-opts-reset 435,16020
-(defconst proof-config-menu447,16288
-(defconst proof-advanced-menu454,16467
-(defvar proof-menu 470,17046
-(defvar proof-main-menu479,17330
-(defvar proof-aux-menu489,17556
-(defvar proof-menu-favourites 505,17878
-(defun proof-menu-define-favourites-menu 508,17985
-(defmacro proof-defshortcut 529,18656
-(defmacro proof-definvisible 545,19311
-(defun proof-def-favourite 566,20136
-(defvar proof-make-favourite-cmd-history 589,21111
-(defvar proof-make-favourite-menu-history 592,21196
-(defun proof-save-favourites 595,21282
-(defun proof-del-favourite 600,21430
-(defun proof-read-favourite 617,21991
-(defun proof-add-favourite 642,22794
-(defvar proof-assistant-settings 669,23845
-(defvar proof-menu-settings 676,24208
-(defun proof-menu-define-settings-menu 679,24282
-(defun proof-menu-entry-name 699,25026
-(defun proof-menu-entry-for-setting 711,25498
-(defun proof-settings-vars 729,25988
-(defun proof-settings-changed-from-defaults-p 734,26165
-(defun proof-settings-changed-from-saved-p 738,26271
-(defun proof-settings-save 742,26374
-(defun proof-settings-reset 747,26541
-(defun proof-defpacustom-fn 755,26787
-(defmacro defpacustom 831,29671
-(defun proof-assistant-invisible-command-ifposs 842,30312
-(defun proof-maybe-askprefs 864,31287
-(defun proof-assistant-settings-cmd 871,31491
-(defun proof-assistant-format 888,32151
-(defvar proof-assistant-format-table 912,33210
-(defun proof-assistant-format-bool 920,33579
-(defun proof-assistant-format-int 923,33692
-(defun proof-assistant-format-string 926,33784
+(defun proof-assistant-menu-update 186,6836
+(defvar proof-help-menu203,7444
+(defvar proof-show-hide-menu211,7722
+(defvar proof-buffer-menu220,8035
+(defconst proof-quick-opts-menu279,10205
+(defun proof-quick-opts-vars 398,14971
+(defun proof-quick-opts-changed-from-defaults-p 423,15722
+(defun proof-quick-opts-changed-from-saved-p 427,15827
+(defun proof-quick-opts-save 438,16179
+(defun proof-quick-opts-reset 443,16347
+(defconst proof-config-menu455,16615
+(defconst proof-advanced-menu462,16794
+(defvar proof-menu 478,17373
+(defvar proof-main-menu487,17657
+(defvar proof-aux-menu497,17883
+(defvar proof-menu-favourites 513,18205
+(defun proof-menu-define-favourites-menu 516,18312
+(defmacro proof-defshortcut 537,18983
+(defmacro proof-definvisible 553,19638
+(defun proof-def-favourite 574,20463
+(defvar proof-make-favourite-cmd-history 597,21438
+(defvar proof-make-favourite-menu-history 600,21523
+(defun proof-save-favourites 603,21609
+(defun proof-del-favourite 608,21757
+(defun proof-read-favourite 625,22318
+(defun proof-add-favourite 650,23121
+(defvar proof-assistant-settings 677,24172
+(defvar proof-menu-settings 684,24535
+(defun proof-menu-define-settings-menu 687,24609
+(defun proof-menu-entry-name 707,25353
+(defun proof-menu-entry-for-setting 719,25825
+(defun proof-settings-vars 737,26315
+(defun proof-settings-changed-from-defaults-p 742,26492
+(defun proof-settings-changed-from-saved-p 746,26598
+(defun proof-settings-save 750,26701
+(defun proof-settings-reset 755,26868
+(defun proof-defpacustom-fn 763,27114
+(defmacro defpacustom 839,29998
+(defun proof-assistant-invisible-command-ifposs 850,30639
+(defun proof-maybe-askprefs 872,31614
+(defun proof-assistant-settings-cmd 879,31818
+(defun proof-assistant-format 896,32478
+(defvar proof-assistant-format-table 920,33537
+(defun proof-assistant-format-bool 928,33906
+(defun proof-assistant-format-int 931,34019
+(defun proof-assistant-format-string 934,34111
 
 generic/proof-mmm.el,113
-(defun proof-mmm-support-available 25,909
-(defun proof-mmm-set-global 49,1757
-(defun proof-mmm-enable 64,2298
+(defun proof-mmm-support-available 27,933
+(defun proof-mmm-set-global 53,1833
+(defun proof-mmm-enable 68,2374
 
 generic/proof-script.el,5105
 (defvar proof-last-theorem-dependencies 41,1047
@@ -1865,75 +1877,75 @@ generic/proof-script.el,5105
 (defvar pg-visibility-specs 514,18647
 (deflocal pg-script-portions 519,18854
 (defun pg-clear-script-portions 522,18976
-(defun pg-add-script-element 540,19640
-(defun pg-remove-script-element 543,19716
-(defsubst pg-visname 551,19994
-(defun pg-add-element 555,20139
-(defun pg-open-invisible-span 589,21768
-(defun pg-remove-element 600,22131
-(defun pg-make-element-invisible 607,22401
-(defun pg-make-element-visible 613,22658
-(defun pg-toggle-element-visibility 618,22837
-(defun pg-redisplay-for-gnuemacs 626,23167
-(defun pg-show-all-portions 633,23438
-(defun pg-show-all-proofs 651,24109
-(defun pg-hide-all-proofs 656,24237
-(defun pg-add-proof-element 661,24368
-(defun pg-span-name 675,24988
-(defun pg-set-span-helphighlights 696,25695
-(defun proof-complete-buffer-atomic 721,26519
-(defun proof-register-possibly-new-processed-file 762,28434
-(defun proof-inform-prover-file-retracted 813,30562
-(defun proof-auto-retract-dependencies 832,31348
-(defun proof-unregister-buffer-file-name 886,33888
-(defun proof-protected-process-or-retract 932,35711
-(defun proof-deactivate-scripting-auto 959,36881
-(defun proof-deactivate-scripting 968,37239
-(defun proof-activate-scripting 1105,42644
-(defun proof-toggle-active-scripting 1233,48398
-(defun proof-done-advancing 1274,49759
-(defun proof-done-advancing-comment 1360,53126
-(defun proof-done-advancing-save 1379,53868
-(defun proof-make-goalsave 1472,57483
-(defun proof-get-name-from-goal 1487,58226
-(defun proof-done-advancing-autosave 1506,59252
-(defun proof-done-advancing-other 1571,61798
-(defun proof-segment-up-to-parser 1599,62757
-(defun proof-script-generic-parse-find-comment-end 1662,64833
-(defun proof-script-generic-parse-cmdend 1671,65249
-(defun proof-script-generic-parse-cmdstart 1696,66144
-(defun proof-script-generic-parse-sexp 1759,68852
-(defun proof-cmdstart-add-segment-for-cmd 1783,69788
-(defun proof-segment-up-to-cmdstart 1835,71987
-(defun proof-segment-up-to-cmdend 1896,74347
-(defun proof-semis-to-vanillas 1967,76994
-(defun proof-script-new-command-advance 2006,78320
-(defun proof-script-next-command-advance 2048,80061
-(defun proof-assert-until-point-interactive 2060,80502
-(defun proof-assert-until-point 2086,81624
-(defun proof-assert-next-command2139,84056
-(defun proof-goto-point 2187,86319
-(defun proof-insert-pbp-command 2204,86845
-(defun proof-done-retracting 2237,87958
-(defun proof-setup-retract-action 2264,89069
-(defun proof-last-goal-or-goalsave 2274,89552
-(defun proof-retract-target 2297,90392
-(defun proof-retract-until-point-interactive 2382,94033
-(defun proof-retract-until-point 2390,94418
-(define-derived-mode proof-mode 2435,96279
-(defun proof-script-set-visited-file-name 2469,97649
-(defun proof-script-set-buffer-hooks 2493,98651
-(defun proof-script-kill-buffer-fn 2503,99147
-(defun proof-config-done-related 2547,100969
-(defun proof-generic-goal-command-p 2619,103537
-(defun proof-generic-state-preserving-p 2624,103749
-(defun proof-generic-count-undos 2633,104266
-(defun proof-generic-find-and-forget 2662,105296
-(defconst proof-script-important-settings2713,107121
-(defun proof-config-done 2726,107658
-(defun proof-setup-parsing-mechanism 2823,111206
-(defun proof-setup-imenu 2867,113059
-(defun proof-setup-func-menu 2884,113664
+(defun pg-add-script-element 536,19505
+(defun pg-remove-script-element 539,19581
+(defsubst pg-visname 547,19859
+(defun pg-add-element 551,20004
+(defun pg-open-invisible-span 585,21633
+(defun pg-remove-element 596,21996
+(defun pg-make-element-invisible 603,22266
+(defun pg-make-element-visible 609,22523
+(defun pg-toggle-element-visibility 614,22702
+(defun pg-redisplay-for-gnuemacs 622,23032
+(defun pg-show-all-portions 629,23303
+(defun pg-show-all-proofs 647,23974
+(defun pg-hide-all-proofs 652,24102
+(defun pg-add-proof-element 657,24233
+(defun pg-span-name 671,24853
+(defun pg-set-span-helphighlights 692,25560
+(defun proof-complete-buffer-atomic 717,26384
+(defun proof-register-possibly-new-processed-file 758,28299
+(defun proof-inform-prover-file-retracted 809,30427
+(defun proof-auto-retract-dependencies 828,31213
+(defun proof-unregister-buffer-file-name 882,33753
+(defun proof-protected-process-or-retract 928,35576
+(defun proof-deactivate-scripting-auto 955,36746
+(defun proof-deactivate-scripting 964,37104
+(defun proof-activate-scripting 1101,42509
+(defun proof-toggle-active-scripting 1229,48263
+(defun proof-done-advancing 1270,49624
+(defun proof-done-advancing-comment 1356,52991
+(defun proof-done-advancing-save 1375,53733
+(defun proof-make-goalsave 1468,57348
+(defun proof-get-name-from-goal 1483,58091
+(defun proof-done-advancing-autosave 1502,59117
+(defun proof-done-advancing-other 1567,61663
+(defun proof-segment-up-to-parser 1595,62622
+(defun proof-script-generic-parse-find-comment-end 1658,64698
+(defun proof-script-generic-parse-cmdend 1667,65114
+(defun proof-script-generic-parse-cmdstart 1692,66009
+(defun proof-script-generic-parse-sexp 1755,68717
+(defun proof-cmdstart-add-segment-for-cmd 1779,69653
+(defun proof-segment-up-to-cmdstart 1831,71852
+(defun proof-segment-up-to-cmdend 1892,74212
+(defun proof-semis-to-vanillas 1963,76859
+(defun proof-script-new-command-advance 2002,78185
+(defun proof-script-next-command-advance 2044,79926
+(defun proof-assert-until-point-interactive 2056,80367
+(defun proof-assert-until-point 2082,81489
+(defun proof-assert-next-command2135,83921
+(defun proof-goto-point 2183,86184
+(defun proof-insert-pbp-command 2200,86710
+(defun proof-done-retracting 2233,87823
+(defun proof-setup-retract-action 2260,88934
+(defun proof-last-goal-or-goalsave 2270,89417
+(defun proof-retract-target 2293,90257
+(defun proof-retract-until-point-interactive 2378,93898
+(defun proof-retract-until-point 2386,94283
+(define-derived-mode proof-mode 2431,96144
+(defun proof-script-set-visited-file-name 2480,98111
+(defun proof-script-set-buffer-hooks 2504,99113
+(defun proof-script-kill-buffer-fn 2514,99609
+(defun proof-config-done-related 2558,101431
+(defun proof-generic-goal-command-p 2630,103999
+(defun proof-generic-state-preserving-p 2635,104211
+(defun proof-generic-count-undos 2644,104728
+(defun proof-generic-find-and-forget 2673,105758
+(defconst proof-script-important-settings2724,107583
+(defun proof-config-done 2737,108120
+(defun proof-setup-parsing-mechanism 2834,111668
+(defun proof-setup-imenu 2878,113521
+(defun proof-setup-func-menu 2895,114126
 
 generic/proof-shell.el,3337
 (defvar proof-shell-last-output 19,457
@@ -1953,100 +1965,100 @@ generic/proof-shell.el,3337
 (defcustom proof-shell-fiddle-frames 243,7592
 (deflocal proof-eagerly-raise 250,7833
 (defun proof-shell-start 253,7939
-(defvar proof-shell-kill-function-hooks 472,16418
-(defun proof-shell-kill-function 475,16516
-(defun proof-shell-clear-state 566,20376
-(defun proof-shell-exit 581,20819
-(defun proof-shell-bail-out 593,21264
-(defun proof-shell-restart 602,21741
-(defvar proof-shell-no-response-display 644,23125
-(defvar proof-shell-urgent-message-marker 647,23229
-(defvar proof-shell-urgent-message-scanner 650,23350
-(defun proof-shell-handle-output 654,23477
-(defun proof-shell-handle-delayed-output 727,26800
-(defvar proof-shell-no-error-display 762,28222
-(defun proof-shell-handle-error 768,28428
-(defun proof-shell-handle-interrupt 786,29264
-(defun proof-shell-error-or-interrupt-action 800,29886
-(defun proof-goals-pos 827,31091
-(defun proof-pbp-focus-on-first-goal 832,31296
-(defsubst proof-shell-string-match-safe 844,31831
-(defun proof-shell-process-output 849,31999
-(defvar proof-shell-insert-space-fudge 960,36639
-(defun proof-shell-insert 969,36948
-(defun proof-shell-command-queue-item 1043,39860
-(defun proof-shell-set-silent 1048,40017
-(defun proof-shell-start-silent-item 1054,40236
-(defun proof-shell-clear-silent 1060,40428
-(defun proof-shell-stop-silent-item 1066,40650
-(defun proof-shell-should-be-silent 1073,40922
-(defun proof-append-alist 1086,41478
-(defun proof-start-queue 1145,43715
-(defun proof-extend-queue 1156,44064
-(defun proof-shell-exec-loop 1167,44445
-(defun proof-shell-insert-loopback-cmd 1232,47033
-(defun proof-shell-message 1260,48359
-(defun proof-shell-process-urgent-message 1266,48575
-(defvar proof-shell-minibuffer-urgent-interactive-input-history 1475,57463
-(defun proof-shell-minibuffer-urgent-interactive-input 1477,57533
-(defun proof-shell-process-urgent-messages 1489,57903
-(defun proof-shell-filter 1561,61073
-(defun proof-shell-filter-process-output 1714,67410
-(defvar pg-last-tracing-output-time 1767,69464
-(defvar pg-tracing-slow-mode 1770,69570
-(defconst pg-slow-mode-duration 1773,69659
-(defconst pg-fast-tracing-mode-threshold 1776,69741
-(defvar pg-tracing-cleanup-timer 1779,69869
-(defun pg-tracing-tight-loop 1781,69908
-(defun pg-finish-tracing-display 1824,71626
-(defun proof-shell-dont-show-annotations 1837,71932
-(defun proof-shell-show-annotations 1853,72467
-(defun proof-shell-wait 1874,72964
-(defun proof-done-invisible 1894,73874
-(defun proof-shell-invisible-command 1937,75597
-(defun proof-shell-invisible-cmd-get-result 1970,76847
-(defun proof-shell-invisible-command-invisible-result 1987,77528
-(define-derived-mode proof-shell-mode 2007,78032
-(defconst proof-shell-important-settings2078,80703
-(defun proof-shell-config-done 2083,80803
-
-generic/proof-site.el,720
+(defvar proof-shell-kill-function-hooks 472,16420
+(defun proof-shell-kill-function 475,16518
+(defun proof-shell-clear-state 566,20378
+(defun proof-shell-exit 581,20821
+(defun proof-shell-bail-out 593,21266
+(defun proof-shell-restart 602,21743
+(defvar proof-shell-no-response-display 644,23127
+(defvar proof-shell-urgent-message-marker 647,23231
+(defvar proof-shell-urgent-message-scanner 650,23352
+(defun proof-shell-handle-output 654,23479
+(defun proof-shell-handle-delayed-output 727,26802
+(defvar proof-shell-no-error-display 762,28224
+(defun proof-shell-handle-error 768,28430
+(defun proof-shell-handle-interrupt 786,29266
+(defun proof-shell-error-or-interrupt-action 800,29888
+(defun proof-goals-pos 827,31093
+(defun proof-pbp-focus-on-first-goal 832,31298
+(defsubst proof-shell-string-match-safe 844,31833
+(defun proof-shell-process-output 849,32001
+(defvar proof-shell-insert-space-fudge 960,36641
+(defun proof-shell-insert 969,36950
+(defun proof-shell-command-queue-item 1043,39862
+(defun proof-shell-set-silent 1048,40019
+(defun proof-shell-start-silent-item 1054,40238
+(defun proof-shell-clear-silent 1060,40430
+(defun proof-shell-stop-silent-item 1066,40652
+(defun proof-shell-should-be-silent 1073,40924
+(defun proof-append-alist 1086,41480
+(defun proof-start-queue 1145,43717
+(defun proof-extend-queue 1156,44066
+(defun proof-shell-exec-loop 1167,44447
+(defun proof-shell-insert-loopback-cmd 1232,47035
+(defun proof-shell-message 1260,48361
+(defun proof-shell-process-urgent-message 1266,48577
+(defvar proof-shell-minibuffer-urgent-interactive-input-history 1475,57465
+(defun proof-shell-minibuffer-urgent-interactive-input 1477,57535
+(defun proof-shell-process-urgent-messages 1489,57905
+(defun proof-shell-filter 1561,61075
+(defun proof-shell-filter-process-output 1714,67412
+(defvar pg-last-tracing-output-time 1767,69466
+(defvar pg-tracing-slow-mode 1770,69572
+(defconst pg-slow-mode-duration 1773,69661
+(defconst pg-fast-tracing-mode-threshold 1776,69743
+(defvar pg-tracing-cleanup-timer 1779,69871
+(defun pg-tracing-tight-loop 1781,69910
+(defun pg-finish-tracing-display 1824,71628
+(defun proof-shell-dont-show-annotations 1837,71934
+(defun proof-shell-show-annotations 1853,72469
+(defun proof-shell-wait 1874,72966
+(defun proof-done-invisible 1894,73876
+(defun proof-shell-invisible-command 1937,75599
+(defun proof-shell-invisible-cmd-get-result 1970,76849
+(defun proof-shell-invisible-command-invisible-result 1987,77530
+(define-derived-mode proof-shell-mode 2007,78034
+(defconst proof-shell-important-settings2078,80705
+(defun proof-shell-config-done 2083,80805
+
+generic/proof-site.el,719
 (defgroup proof-general 20,594
-(defgroup proof-general-internals 33,1010
-(defun proof-home-directory-fn 42,1203
-(defcustom proof-home-directory53,1573
-(defcustom proof-images-directory62,1939
-(defcustom proof-info-directory68,2140
-(defcustom proof-assistant-table97,3389
-(defun proof-string-to-list 159,5386
-(defcustom proof-assistants 175,5877
-(defun proof-ready-for-assistant 211,7290
-(defconst proof-general-version 324,11505
-(defconst proof-general-short-version 327,11646
-(defconst proof-general-version-year 332,11806
-(defcustom proof-assistant-cusgrp 346,12274
-(defcustom proof-assistant-internals-cusgrp 354,12577
-(defcustom proof-assistant 362,12889
-(defcustom proof-assistant-symbol 370,13158
+(defgroup proof-general-internals 32,994
+(defun proof-home-directory-fn 43,1234
+(defcustom proof-home-directory54,1604
+(defcustom proof-images-directory63,1970
+(defcustom proof-info-directory69,2171
+(defcustom proof-assistant-table98,3420
+(defun proof-string-to-list 160,5417
+(defcustom proof-assistants 176,5908
+(defun proof-ready-for-assistant 212,7321
+(defconst proof-general-version 325,11540
+(defconst proof-general-short-version 328,11681
+(defconst proof-general-version-year 333,11841
+(defcustom proof-assistant-cusgrp 347,12309
+(defcustom proof-assistant-internals-cusgrp 355,12612
+(defcustom proof-assistant 363,12924
+(defcustom proof-assistant-symbol 371,13193
 
 generic/proof-splash.el,727
 (defcustom proof-splash-enable 16,433
 (defcustom proof-splash-time 21,585
 (defcustom proof-splash-contents29,870
-(defconst proof-splash-startup-msg 58,1986
-(defconst proof-splash-welcome 67,2365
-(defun proof-get-image 86,2929
-(defvar proof-splash-timeout-conf 141,4780
-(defun proof-splash-centre-spaces 144,4893
-(defun proof-splash-remove-screen 172,6062
-(defun proof-splash-remove-buffer 193,6811
-(defvar proof-splash-seen 209,7475
-(defun proof-splash-display-screen 213,7592
-(defun proof-splash-message 288,10751
-(defun proof-splash-timeout-waiter 298,11114
-(defvar proof-splash-old-frame-title-format 315,11853
-(defun proof-splash-set-frame-titles 317,11903
-(defun proof-splash-unset-frame-titles 326,12219
+(defconst proof-splash-startup-msg 58,1985
+(defconst proof-splash-welcome 67,2364
+(defun proof-get-image 85,2900
+(defvar proof-splash-timeout-conf 125,4263
+(defun proof-splash-centre-spaces 128,4376
+(defun proof-splash-remove-screen 156,5545
+(defun proof-splash-remove-buffer 176,6271
+(defvar proof-splash-seen 192,6935
+(defun proof-splash-display-screen 196,7052
+(defun proof-splash-message 271,10211
+(defun proof-splash-timeout-waiter 281,10574
+(defvar proof-splash-old-frame-title-format 298,11313
+(defun proof-splash-set-frame-titles 300,11363
+(defun proof-splash-unset-frame-titles 309,11679
 
 generic/proof-syntax.el,972
 (defun proof-ids-to-regexp 16,445
@@ -2076,7 +2088,7 @@ generic/proof-syntax.el,972
 (defun proof-insert 248,8676
 (defun proof-splice-separator 284,9685
 
-generic/proof-toolbar.el,2880
+generic/proof-toolbar.el,2877
 (defun proof-toolbar-function 49,1595
 (defun proof-toolbar-icon 52,1692
 (defun proof-toolbar-enabler 55,1793
@@ -2087,52 +2099,52 @@ generic/proof-toolbar.el,2880
 (deflocal proof-toolbar-itimer 126,4184
 (defun proof-toolbar-setup 130,4294
 (defun proof-toolbar-build 174,5861
-(defalias 'proof-toolbar-enable proof-toolbar-enable
248,8422
-(defun proof-toolbar-setup-refresh 257,8661
-(defun proof-toolbar-disable-refresh 278,9431
-(deflocal proof-toolbar-refresh-flag 285,9753
-(defun proof-toolbar-refresh 291,10024
-(defvar proof-toolbar-enablers295,10169
-(defvar proof-toolbar-enablers-last-state301,10345
-(defun proof-toolbar-really-refresh 305,10436
-(defun proof-toolbar-undo-enable-p 358,12266
-(defalias 'proof-toolbar-undo proof-toolbar-undo
363,12414
-(defun proof-toolbar-delete-enable-p 369,12533
-(defalias 'proof-toolbar-delete proof-toolbar-delete
375,12707
-(defun proof-toolbar-lockedend-enable-p 382,12843
-(defalias 'proof-toolbar-lockedend proof-toolbar-lockedend
385,12893
-(defun proof-toolbar-next-enable-p 394,12981
-(defalias 'proof-toolbar-next proof-toolbar-next
398,13088
-(defun proof-toolbar-goto-enable-p 405,13182
-(defalias 'proof-toolbar-goto proof-toolbar-goto
408,13255
-(defun proof-toolbar-retract-enable-p 415,13331
-(defalias 'proof-toolbar-retract proof-toolbar-retract
419,13442
-(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p
426,13521
-(defalias 'proof-toolbar-use proof-toolbar-use
427,13589
-(defun proof-toolbar-restart-enable-p 433,13667
-(defalias 'proof-toolbar-restart proof-toolbar-restart
438,13828
-(defun proof-toolbar-goal-enable-p 444,13906
-(defalias 'proof-toolbar-goal proof-toolbar-goal
451,14139
-(defun proof-toolbar-qed-enable-p 458,14211
-(defalias 'proof-toolbar-qed proof-toolbar-qed
464,14363
-(defun proof-toolbar-state-enable-p 470,14435
-(defalias 'proof-toolbar-state proof-toolbar-state
473,14506
-(defun proof-toolbar-context-enable-p 479,14575
-(defalias 'proof-toolbar-context proof-toolbar-context
482,14648
-(defun proof-toolbar-info-enable-p 490,14808
-(defalias 'proof-toolbar-info proof-toolbar-info
493,14852
-(defun proof-toolbar-command-enable-p 499,14921
-(defalias 'proof-toolbar-command proof-toolbar-command
502,14992
-(defun proof-toolbar-help-enable-p 508,15072
-(defun proof-toolbar-help 511,15117
-(defun proof-toolbar-find-enable-p 519,15211
-(defalias 'proof-toolbar-find proof-toolbar-find
522,15280
-(defun proof-toolbar-visibility-enable-p 528,15378
-(defalias 'proof-toolbar-visibility proof-toolbar-visibility
531,15478
-(defun proof-toolbar-interrupt-enable-p 537,15566
-(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt
540,15630
-(defun proof-toolbar-make-menu-item 549,15819
-(defconst proof-toolbar-scripting-menu571,16507
+(defalias 'proof-toolbar-enable proof-toolbar-enable
239,8074
+(defun proof-toolbar-setup-refresh 248,8313
+(defun proof-toolbar-disable-refresh 269,9083
+(deflocal proof-toolbar-refresh-flag 276,9405
+(defun proof-toolbar-refresh 282,9676
+(defvar proof-toolbar-enablers286,9821
+(defvar proof-toolbar-enablers-last-state292,9997
+(defun proof-toolbar-really-refresh 296,10088
+(defun proof-toolbar-undo-enable-p 349,11918
+(defalias 'proof-toolbar-undo proof-toolbar-undo
354,12066
+(defun proof-toolbar-delete-enable-p 360,12185
+(defalias 'proof-toolbar-delete proof-toolbar-delete
366,12359
+(defun proof-toolbar-lockedend-enable-p 373,12495
+(defalias 'proof-toolbar-lockedend proof-toolbar-lockedend
376,12545
+(defun proof-toolbar-next-enable-p 385,12633
+(defalias 'proof-toolbar-next proof-toolbar-next
389,12740
+(defun proof-toolbar-goto-enable-p 396,12834
+(defalias 'proof-toolbar-goto proof-toolbar-goto
399,12907
+(defun proof-toolbar-retract-enable-p 406,12983
+(defalias 'proof-toolbar-retract proof-toolbar-retract
410,13094
+(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p
417,13173
+(defalias 'proof-toolbar-use proof-toolbar-use
418,13241
+(defun proof-toolbar-restart-enable-p 424,13319
+(defalias 'proof-toolbar-restart proof-toolbar-restart
429,13480
+(defun proof-toolbar-goal-enable-p 435,13558
+(defalias 'proof-toolbar-goal proof-toolbar-goal
442,13791
+(defun proof-toolbar-qed-enable-p 449,13863
+(defalias 'proof-toolbar-qed proof-toolbar-qed
455,14015
+(defun proof-toolbar-state-enable-p 461,14087
+(defalias 'proof-toolbar-state proof-toolbar-state
464,14158
+(defun proof-toolbar-context-enable-p 470,14227
+(defalias 'proof-toolbar-context proof-toolbar-context
473,14300
+(defun proof-toolbar-info-enable-p 481,14460
+(defalias 'proof-toolbar-info proof-toolbar-info
484,14504
+(defun proof-toolbar-command-enable-p 490,14573
+(defalias 'proof-toolbar-command proof-toolbar-command
493,14644
+(defun proof-toolbar-help-enable-p 499,14724
+(defun proof-toolbar-help 502,14769
+(defun proof-toolbar-find-enable-p 510,14863
+(defalias 'proof-toolbar-find proof-toolbar-find
513,14932
+(defun proof-toolbar-visibility-enable-p 519,15030
+(defalias 'proof-toolbar-visibility proof-toolbar-visibility
522,15130
+(defun proof-toolbar-interrupt-enable-p 528,15218
+(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt
531,15282
+(defun proof-toolbar-make-menu-item 540,15471
+(defconst proof-toolbar-scripting-menu562,16159
 
 generic/proof-utils.el,2099
 (defmacro deflocal 18,472
@@ -2179,30 +2191,30 @@ generic/proof-utils.el,2099
 (defun proof-switch-to-buffer 640,23835
 (defun proof-resize-window-tofit 673,25527
 (defun proof-submit-bug-report 773,29539
-(defun proof-deftoggle-fn 809,30923
-(defmacro proof-deftoggle 824,31578
-(defun proof-defintset-fn 831,31952
-(defmacro proof-defintset 847,32660
-(defun proof-defstringset-fn 854,33037
-(defmacro proof-defstringset 867,33664
-(defun pg-custom-save-vars 881,34129
-(defun pg-custom-reset-vars 899,34855
-(defun proof-locate-executable 912,35192
-(defconst proof-extra-fls941,36373
+(defun proof-deftoggle-fn 809,30927
+(defmacro proof-deftoggle 824,31582
+(defun proof-defintset-fn 831,31956
+(defmacro proof-defintset 847,32664
+(defun proof-defstringset-fn 854,33041
+(defmacro proof-defstringset 867,33668
+(defun pg-custom-save-vars 881,34133
+(defun pg-custom-reset-vars 899,34859
+(defun proof-locate-executable 912,35196
+(defconst proof-extra-fls941,36377
 
 generic/proof-x-symbol.el,613
-(defvar proof-x-symbol-initialized 54,2151
-(defun proof-x-symbol-tokenlang-file 57,2246
-(defun proof-x-symbol-support-maybe-available 63,2428
-(defun proof-x-symbol-initialize 83,3178
-(defun proof-x-symbol-enable 178,7046
-(defun proof-x-symbol-refresh-output-buffers 208,8363
-(defun proof-x-symbol-mode-associated-buffers 223,9117
-(defalias 'proof-x-symbol-decode-region proof-x-symbol-decode-region
245,9821
-(defun proof-x-symbol-encode-shell-input 247,9887
-(defun proof-x-symbol-set-language 264,10478
-(defun proof-x-symbol-shell-config 269,10649
-(defun proof-x-symbol-config-output-buffer 317,12816
+(defvar proof-x-symbol-initialized 51,2010
+(defun proof-x-symbol-tokenlang-file 54,2105
+(defun proof-x-symbol-support-maybe-available 60,2287
+(defun proof-x-symbol-initialize 80,3037
+(defun proof-x-symbol-enable 171,6698
+(defun proof-x-symbol-refresh-output-buffers 201,8015
+(defun proof-x-symbol-mode-associated-buffers 216,8769
+(defalias 'proof-x-symbol-decode-region proof-x-symbol-decode-region
238,9473
+(defun proof-x-symbol-encode-shell-input 240,9539
+(defun proof-x-symbol-set-language 257,10130
+(defun proof-x-symbol-shell-config 262,10301
+(defun proof-x-symbol-config-output-buffer 310,12468
 
 lib/bufhist.el,1058
 (defun bufhist-ring-update 32,1226
@@ -2307,32 +2319,38 @@ lib/local-vars-list.el,372
 (defun local-vars-list-get-safe 185,5955
 (defun local-vars-list-set 190,6149
 
-lib/proof-compat.el,1002
-(defvar proof-running-on-XEmacs 24,760
-(defvar proof-running-on-Emacs21 26,882
-(defvar proof-running-on-win32 30,1129
-(defun pg-custom-undeclare-variable 42,1563
-(defun pg-window-system 117,4045
-(defconst pg-defface-window-systems 126,4416
-(defun subst-char-in-string 150,5133
-(defun replace-regexp-in-string 164,5687
-(defconst menuvisiblep 226,8400
-(defun set-window-text-height 243,9019
-(defmacro save-selected-frame 269,9969
-(defun warn 308,11271
-(defun redraw-modeline 315,11526
-(defun replace-in-string 330,12093
-(defun proof-buffer-syntactic-context-emulate 379,13611
-(defvar read-shell-command-map412,14918
-(defun read-shell-command 430,15620
-(defun remassq 442,16101
-(defun remassoc 454,16490
-(defun frames-of-buffer 467,16935
-(defmacro with-selected-window 506,18197
-(defun pg-pop-to-buffer 549,19586
-(defun process-live-p 600,21438
-(defalias 'proof-buffer-syntactic-context proof-buffer-syntactic-context
667,23835
-(defun select-buffers-tab-buffers-by-mode 711,25183
+lib/maths-menu.el,153
+(defun maths-menu-build-menu 48,2022
+(defvar maths-menu-menu67,2690
+(defvar maths-menu-mode-map312,11648
+(define-minor-mode maths-menu-mode337,12521
+
+lib/proof-compat.el,1003
+(defvar proof-running-on-XEmacs 25,817
+(defvar proof-running-on-Emacs21 27,939
+(defvar proof-running-on-win32 31,1186
+(defun pg-custom-undeclare-variable 43,1620
+(defun pg-window-system 118,4102
+(defconst pg-defface-window-systems 127,4473
+(defun subst-char-in-string 151,5190
+(defun replace-regexp-in-string 165,5744
+(defconst menuvisiblep 227,8457
+(defun set-window-text-height 244,9076
+(defmacro save-selected-frame 270,10026
+(defun warn 309,11328
+(defun redraw-modeline 316,11583
+(defun replace-in-string 331,12150
+(defun proof-buffer-syntactic-context-emulate 380,13668
+(defvar read-shell-command-map413,14975
+(defun read-shell-command 431,15677
+(defun remassq 443,16158
+(defun remassoc 455,16547
+(defun frames-of-buffer 468,16992
+(defmacro with-selected-window 507,18254
+(defun pg-pop-to-buffer 550,19643
+(defun process-live-p 601,21495
+(defalias 'proof-buffer-syntactic-context proof-buffer-syntactic-context
618,21998
+(defun select-buffers-tab-buffers-by-mode 662,23346
 
 lib/span.el,132
 (defsubst delete-spans 24,499
@@ -2340,72 +2358,72 @@ lib/span.el,132
 (defsubst set-span-start 32,792
 (defsubst set-span-end 36,924
 
-lib/span-extent.el,972
-(defsubst make-span 16,557
-(defsubst detach-span 20,679
-(defsubst set-span-endpoints 24,766
-(defsubst set-span-property 28,899
-(defsubst span-read-only 32,1026
-(defsubst span-read-write 36,1130
-(defun span-give-warning 40,1237
-(defun span-write-warning 44,1335
-(defsubst span-property 49,1535
-(defsubst delete-span 53,1650
-(defsubst mapcar-spans 59,1821
-(defsubst span-at 63,2027
-(defsubst span-at-before 67,2144
-(defsubst span-start 72,2341
-(defsubst span-end 76,2470
-(defsubst prev-span 80,2593
-(defsubst next-span 84,2739
-(defsubst span-live-p 88,2881
-(defun span-raise 96,3153
-(defalias 'span-object span-object
100,3252
-(defalias 'span-string span-string
101,3291
-(defsubst make-detached-span 104,3377
-(defsubst span-buffer 109,3439
-(defsubst span-detached-p 114,3531
-(defsubst set-span-face 119,3643
-(defsubst fold-spans 124,3739
-(defsubst set-span-properties 129,3937
-(defsubst set-span-keymap 134,4046
-(defsubst span-at-event 139,4161
+lib/span-extent.el,968
+(defsubst make-span 12,367
+(defsubst detach-span 16,489
+(defsubst set-span-endpoints 20,576
+(defsubst set-span-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 delete-span 49,1470
+(defsubst mapcar-spans 55,1641
+(defsubst span-at 59,1847
+(defsubst span-at-before 63,1964
+(defsubst span-start 68,2161
+(defsubst span-end 72,2290
+(defsubst prev-span 76,2413
+(defsubst next-span 80,2559
+(defsubst span-live-p 84,2701
+(defun span-raise 92,2973
+(defalias 'span-object span-object
96,3072
+(defalias 'span-string span-string
97,3111
+(defsubst make-detached-span 100,3197
+(defsubst span-buffer 105,3259
+(defsubst span-detached-p 110,3351
+(defsubst set-span-face 115,3463
+(defsubst fold-spans 119,3558
+(defsubst set-span-properties 123,3755
+(defsubst set-span-keymap 127,3863
+(defsubst span-at-event 132,4007
 
 lib/span-overlay.el,1201
-(defalias 'span-start span-start
16,543
-(defalias 'span-end span-end
17,581
-(defalias 'set-span-property set-span-property
18,615
-(defalias 'span-property span-property
19,658
-(defalias 'make-span make-span
20,697
-(defalias 'detach-span detach-span
21,733
-(defalias 'set-span-endpoints set-span-endpoints
22,773
-(defalias 'span-buffer span-buffer
23,818
-(defun span-read-only-hook 25,859
-(defun span-read-only 29,991
-(defun span-read-write 44,1767
-(defun span-give-warning 50,1986
-(defun span-write-warning 54,2094
-(defun span-lt 61,2420
-(defun spans-at-point-prop 66,2561
-(defun spans-at-region-prop 72,2726
-(defun span-at 80,2970
-(defsubst delete-span 86,3184
-(defsubst mapcar-spans 93,3406
-(defun span-at-before 97,3610
-(defun prev-span 114,4336
-(defun next-span 120,4487
-(defsubst span-live-p 149,5712
-(defun span-raise 155,5878
-(defalias 'span-object span-object
161,6121
-(defun span-string 163,6162
-(defun set-span-properties 169,6344
-(defun span-find-span 181,6599
-(defsubst span-at-event 188,6906
-(defun make-detached-span 193,7030
-(defun fold-spans 198,7126
-(defsubst span-detached-p 213,7660
-(defsubst set-span-face 217,7775
-(defun set-span-keymap 221,7872
+(defalias 'span-start span-start
12,370
+(defalias 'span-end span-end
13,408
+(defalias 'set-span-property set-span-property
14,442
+(defalias 'span-property span-property
15,485
+(defalias 'make-span make-span
16,524
+(defalias 'detach-span detach-span
17,560
+(defalias 'set-span-endpoints set-span-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 76,2797
+(defsubst delete-span 82,3011
+(defsubst mapcar-spans 89,3233
+(defun span-at-before 93,3437
+(defun prev-span 110,4163
+(defun next-span 116,4314
+(defsubst span-live-p 145,5539
+(defun span-raise 151,5705
+(defalias 'span-object span-object
157,5948
+(defun span-string 159,5989
+(defun set-span-properties 165,6171
+(defun span-find-span 177,6426
+(defsubst span-at-event 184,6733
+(defun make-detached-span 189,6857
+(defun fold-spans 194,6953
+(defsubst span-detached-p 209,7487
+(defsubst set-span-face 213,7602
+(defun set-span-keymap 217,7699
 
 lib/texi-docstring-magic.el,584
 (defun texi-docstring-magic-find-face 85,2997
@@ -2687,10 +2705,10 @@ mmm/mmm-utils.el,282
 (defmacro mmm-save-all 60,1953
 (defun mmm-format-string 73,2242
 (defun mmm-format-matches 84,2694
-(defmacro mmm-save-keyword 107,3484
-(defmacro mmm-save-keywords 115,3811
-(defun mmm-looking-back-at 128,4344
-(defun mmm-make-marker 145,4912
+(defmacro mmm-save-keyword 107,3487
+(defmacro mmm-save-keywords 115,3814
+(defun mmm-looking-back-at 128,4347
+(defun mmm-make-marker 145,4915
 
 mmm/mmm-vars.el,2667
 (defgroup mmm 99,3072
@@ -2865,153 +2883,153 @@ x-symbol/lisp/x-symbol.el,9173
 (defvar x-symbol-itimer 1602,66238
 (defvar x-symbol-invisible-display-table1605,66321
 (defvar x-symbol-invisible-font 1614,66557
-(defvar x-symbol-charsym-info-cache 1638,67675
-(defvar x-symbol-language-info-caches 1640,67766
-(defvar x-symbol-coding-info-cache 1642,67860
-(defvar x-symbol-keys-info-cache 1644,67949
-(defun x-symbol-list-bury 1652,68254
-(defun x-symbol-list-restore 1658,68450
-(defun x-symbol-list-store 1688,69668
-(defun x-symbol-list-mode 1697,70085
-(defun x-symbol-list-scroll 1718,70887
-(defun x-symbol-init-language-interactive 1741,71529
-(defun x-symbol-list-menu 1758,72243
-(defun x-symbol-list-selected 1813,74151
-(defun x-symbol-list-menu-selected 1839,75360
-(defun x-symbol-list-mouse-selected 1850,75813
-(defun x-symbol-charsym-info 1867,76535
-(defun x-symbol-language-info 1881,77136
-(defun x-symbol-coding-info 1913,78336
-(defun x-symbol-keys-info 1933,79108
-(defun x-symbol-info 1957,80031
-(defun x-symbol-list-info 1970,80569
-(defun x-symbol-highlight-echo 1984,81112
-(defun x-symbol-point-info 1995,81661
-(defun x-symbol-hide-revealed-at-point 2041,83583
-(defun x-symbol-reveal-invisible 2078,85250
-(defun x-symbol-show-info-and-invisible 2126,87442
-(defun x-symbol-start-itimer-once 2162,88984
-(defun x-symbol-setup-minibuffer 2178,89610
-(defvar x-symbol-language-history 2196,90181
-(defvar x-symbol-token-history 2199,90305
-(defvar x-symbol-last-abbrev 2202,90381
-(defvar x-symbol-electric-pos 2204,90477
-(defvar x-symbol-command-keys 2207,90559
-(defvar x-symbol-help-keys 2211,90690
-(defvar x-symbol-help-language 2213,90785
-(defvar x-symbol-help-completions 2215,90884
-(defvar x-symbol-help-completions1 2217,90976
-(defun x-symbol-map-default-binding 2225,91252
-(defun x-symbol-read-charsym-token 2256,92330
-(defun x-symbol-insert-command 2282,93253
-(defun x-symbol-read-language 2333,95260
-(defun x-symbol-read-token 2348,95938
-(defun x-symbol-read-token-direct 2387,97447
-(defun x-symbol-grid 2399,97847
-(defun x-symbol-replace-from 2487,101463
-(defvar x-symbol-token-search-prelude-size 2523,102964
-(defun x-symbol-replace-token 2525,103012
-(defun x-symbol-match-token-before 2550,104103
-(defun x-symbol-token-input 2594,105906
-(defun x-symbol-modify-key 2615,106736
-(defun x-symbol-rotate-key 2648,108065
-(defun x-symbol-electric-input 2702,110275
-(defun x-symbol-help-mapper 2744,111976
-(defun x-symbol-help-output 2767,112815
-(defun x-symbol-help 2810,114411
-(defvar x-symbol-face-docstrings2863,116480
-(defvar x-symbol-all-key-prefixes 2869,116668
-(defvar x-symbol-all-key-chain-alist 2871,116779
-(defvar x-symbol-all-horizontal-chain-alist 2873,116878
-(defvar x-symbol-all-chain-subchains-alist 2875,116991
-(defvar x-symbol-all-exclusive-context-alist 2877,117105
-(defalias 'x-symbol-table-grouping x-symbol-table-grouping
2885,117401
-(defalias 'x-symbol-table-aspects x-symbol-table-aspects
2886,117442
-(defalias 'x-symbol-table-score x-symbol-table-score
2887,117483
-(defalias 'x-symbol-table-input x-symbol-table-input
2888,117523
-(defsubst x-symbol-table-prefixes 2889,117564
-(defsubst x-symbol-table-junk 2890,117615
-(defsubst x-symbol-charsym-defined-p 2892,117666
-(defun x-symbol-try-font-name-0 2900,117967
-(defun x-symbol-try-font-name 2918,118523
-(defun x-symbol-set-cstrings 2935,119039
-(defun x-symbol-init-charsym-command 2980,121017
-(defun x-symbol-init-charsym-input 2988,121383
-(defun x-symbol-init-charsym-aspects 3057,124101
-(defun x-symbol-init-cset 3087,125381
-(defun x-symbol-make-atree 3237,132204
-(defun x-symbol-atree-push 3241,132284
-(defun x-symbol-component-root-p 3261,132973
-(defun x-symbol-component-elements 3265,133112
-(defun x-symbol-component-merge 3272,133360
-(defun x-symbol-component-space 3286,133908
-(defun x-symbol-modify-less-than 3300,134492
-(defun x-symbol-inherit-aspects 3305,134715
-(defun x-symbol-compute-aspects 3314,135154
-(defun x-symbol-init-aspects 3330,135872
-(defun x-symbol-sort-modify-chain 3375,137921
-(defun x-symbol-init-horizontal/key-alist 3390,138493
-(defun x-symbol-init-exclusive-alist 3406,139239
-(defun x-symbol-init-horizontal-chain 3444,140843
-(defun x-symbol-init-exclusive-chain 3452,141175
-(defun x-symbol-init-rotate-chain 3459,141502
-(defun x-symbol-init-context-atree 3480,142376
-(defun x-symbol-init-key-bindings 3525,144659
-(defun x-symbol-rotate-modify-less-than 3548,145582
-(defun x-symbol-subgroup-less-than 3556,145977
-(defun x-symbol-header-charsyms 3561,146234
-(defun x-symbol-init-grid/menu 3587,147284
-(defun x-symbol-init-input 3658,149884
-(defun x-symbol-init-latin-decoding 3788,156360
-(defun x-symbol-get-prime-for 3829,158231
-(defun x-symbol-alist-to-obarray 3838,158555
-(defun x-symbol-alist-to-hash-table 3844,158763
-(defun x-symbol-init-language 3854,159096
-(defvar x-symbol-latin1-cset3978,164561
-(defvar x-symbol-latin2-cset3984,164734
-(defvar x-symbol-latin3-cset3990,164907
-(defvar x-symbol-latin5-cset3996,165080
-(defvar x-symbol-latin9-cset4002,165252
-(defvar x-symbol-xsymb0-cset4008,165458
-(defvar x-symbol-xsymb1-cset4014,165713
-(defvar x-symbol-latin1-table4020,165955
-(defvar x-symbol-latin2-table4121,170425
-(defvar x-symbol-latin3-table4220,173626
-(defvar x-symbol-latin5-table4319,176507
-(defvar x-symbol-latin9-table4418,178817
-(defvar x-symbol-xsymb0-table4517,181207
-(defvar x-symbol-xsymb1-table4667,188603
-(defvar x-symbol-no-of-charsyms 4875,199238
-(defun x-symbol-mac-setup1 4883,199604
-(defun x-symbol-mac-setup2 4909,200513
-
-x-symbol/lisp/x-symbol-emacs.el,1125
+(defvar x-symbol-charsym-info-cache 1639,67744
+(defvar x-symbol-language-info-caches 1641,67835
+(defvar x-symbol-coding-info-cache 1643,67929
+(defvar x-symbol-keys-info-cache 1645,68018
+(defun x-symbol-list-bury 1653,68323
+(defun x-symbol-list-restore 1659,68519
+(defun x-symbol-list-store 1689,69737
+(defun x-symbol-list-mode 1698,70154
+(defun x-symbol-list-scroll 1719,70956
+(defun x-symbol-init-language-interactive 1742,71598
+(defun x-symbol-list-menu 1759,72312
+(defun x-symbol-list-selected 1814,74220
+(defun x-symbol-list-menu-selected 1840,75429
+(defun x-symbol-list-mouse-selected 1851,75882
+(defun x-symbol-charsym-info 1868,76604
+(defun x-symbol-language-info 1882,77205
+(defun x-symbol-coding-info 1914,78405
+(defun x-symbol-keys-info 1934,79177
+(defun x-symbol-info 1958,80100
+(defun x-symbol-list-info 1971,80638
+(defun x-symbol-highlight-echo 1985,81181
+(defun x-symbol-point-info 1996,81730
+(defun x-symbol-hide-revealed-at-point 2042,83652
+(defun x-symbol-reveal-invisible 2079,85319
+(defun x-symbol-show-info-and-invisible 2127,87511
+(defun x-symbol-start-itimer-once 2163,89053
+(defun x-symbol-setup-minibuffer 2179,89679
+(defvar x-symbol-language-history 2197,90250
+(defvar x-symbol-token-history 2200,90374
+(defvar x-symbol-last-abbrev 2203,90450
+(defvar x-symbol-electric-pos 2205,90546
+(defvar x-symbol-command-keys 2208,90628
+(defvar x-symbol-help-keys 2212,90759
+(defvar x-symbol-help-language 2214,90854
+(defvar x-symbol-help-completions 2216,90953
+(defvar x-symbol-help-completions1 2218,91045
+(defun x-symbol-map-default-binding 2226,91321
+(defun x-symbol-read-charsym-token 2257,92399
+(defun x-symbol-insert-command 2283,93322
+(defun x-symbol-read-language 2334,95329
+(defun x-symbol-read-token 2349,96007
+(defun x-symbol-read-token-direct 2388,97516
+(defun x-symbol-grid 2400,97916
+(defun x-symbol-replace-from 2488,101532
+(defvar x-symbol-token-search-prelude-size 2524,103033
+(defun x-symbol-replace-token 2526,103081
+(defun x-symbol-match-token-before 2551,104172
+(defun x-symbol-token-input 2595,105975
+(defun x-symbol-modify-key 2616,106805
+(defun x-symbol-rotate-key 2649,108134
+(defun x-symbol-electric-input 2703,110344
+(defun x-symbol-help-mapper 2745,112045
+(defun x-symbol-help-output 2768,112884
+(defun x-symbol-help 2811,114480
+(defvar x-symbol-face-docstrings2864,116549
+(defvar x-symbol-all-key-prefixes 2870,116737
+(defvar x-symbol-all-key-chain-alist 2872,116848
+(defvar x-symbol-all-horizontal-chain-alist 2874,116947
+(defvar x-symbol-all-chain-subchains-alist 2876,117060
+(defvar x-symbol-all-exclusive-context-alist 2878,117174
+(defalias 'x-symbol-table-grouping x-symbol-table-grouping
2886,117470
+(defalias 'x-symbol-table-aspects x-symbol-table-aspects
2887,117511
+(defalias 'x-symbol-table-score x-symbol-table-score
2888,117552
+(defalias 'x-symbol-table-input x-symbol-table-input
2889,117592
+(defsubst x-symbol-table-prefixes 2890,117633
+(defsubst x-symbol-table-junk 2891,117684
+(defsubst x-symbol-charsym-defined-p 2893,117735
+(defun x-symbol-try-font-name-0 2901,118036
+(defun x-symbol-try-font-name 2919,118592
+(defun x-symbol-set-cstrings 2936,119108
+(defun x-symbol-init-charsym-command 2981,121086
+(defun x-symbol-init-charsym-input 2989,121452
+(defun x-symbol-init-charsym-aspects 3058,124170
+(defun x-symbol-init-cset 3088,125450
+(defun x-symbol-make-atree 3238,132273
+(defun x-symbol-atree-push 3242,132353
+(defun x-symbol-component-root-p 3262,133042
+(defun x-symbol-component-elements 3266,133181
+(defun x-symbol-component-merge 3273,133429
+(defun x-symbol-component-space 3287,133977
+(defun x-symbol-modify-less-than 3301,134561
+(defun x-symbol-inherit-aspects 3306,134784
+(defun x-symbol-compute-aspects 3315,135223
+(defun x-symbol-init-aspects 3331,135941
+(defun x-symbol-sort-modify-chain 3376,137990
+(defun x-symbol-init-horizontal/key-alist 3391,138562
+(defun x-symbol-init-exclusive-alist 3407,139308
+(defun x-symbol-init-horizontal-chain 3445,140912
+(defun x-symbol-init-exclusive-chain 3453,141244
+(defun x-symbol-init-rotate-chain 3460,141571
+(defun x-symbol-init-context-atree 3481,142445
+(defun x-symbol-init-key-bindings 3526,144728
+(defun x-symbol-rotate-modify-less-than 3549,145651
+(defun x-symbol-subgroup-less-than 3557,146046
+(defun x-symbol-header-charsyms 3562,146303
+(defun x-symbol-init-grid/menu 3588,147353
+(defun x-symbol-init-input 3659,149953
+(defun x-symbol-init-latin-decoding 3789,156429
+(defun x-symbol-get-prime-for 3830,158300
+(defun x-symbol-alist-to-obarray 3839,158624
+(defun x-symbol-alist-to-hash-table 3845,158832
+(defun x-symbol-init-language 3855,159165
+(defvar x-symbol-latin1-cset3979,164630
+(defvar x-symbol-latin2-cset3985,164803
+(defvar x-symbol-latin3-cset3991,164976
+(defvar x-symbol-latin5-cset3997,165149
+(defvar x-symbol-latin9-cset4003,165321
+(defvar x-symbol-xsymb0-cset4009,165527
+(defvar x-symbol-xsymb1-cset4015,165782
+(defvar x-symbol-latin1-table4021,166024
+(defvar x-symbol-latin2-table4122,170494
+(defvar x-symbol-latin3-table4221,173695
+(defvar x-symbol-latin5-table4320,176576
+(defvar x-symbol-latin9-table4419,178886
+(defvar x-symbol-xsymb0-table4518,181276
+(defvar x-symbol-xsymb1-table4668,188672
+(defvar x-symbol-no-of-charsyms 4876,199307
+(defun x-symbol-mac-setup1 4884,199673
+(defun x-symbol-mac-setup2 4910,200582
+
+x-symbol/lisp/x-symbol-emacs.el,1126
 (defun emacs-version>=34,1341
-(defvar x-symbol-emacs-has-font-lock-with-props68,3002
-(defvar x-symbol-emacs-has-correct-find-safe-coding81,3494
-(defvar x-symbol-emacs-after-create-image-function96,4008
-(defvar image-types 122,4865
-(defvar init-file-loaded 158,6252
-(defvar message-stack 161,6325
-(defun region-active-p 244,9635
-(defvar x-symbol-data-directory 281,11000
-(defun x-symbol-directory-files 351,13277
-(defun x-symbol-event-in-current-buffer 365,13665
-(defun x-symbol-create-image 368,13714
-(defun x-symbol-make-glyph 371,13799
-(defun x-symbol-set-glyph-image 374,13870
-(defvar x-symbol-heading-strut-glyph 389,14367
-(defvar x-symbol-invisible-face 392,14454
-(defvar x-symbol-face 393,14512
-(defvar x-symbol-sub-face 394,14550
-(defvar x-symbol-sup-face 395,14596
-(defvar x-symbol-emacs-w32-font-directories397,14643
-(defvar x-symbol-invisible-display-table 410,15121
-(defalias 'x-symbol-window-width x-symbol-window-width
412,15168
-(defun x-symbol-set-face-font 414,15217
-(defun x-symbol-event-matches-key-specifier-p 425,15690
-(defun start-itimer 435,15962
-(defun itimer-live-p 437,16059
+(defvar x-symbol-emacs-has-font-lock-with-props68,3005
+(defvar x-symbol-emacs-has-correct-find-safe-coding86,3670
+(defvar x-symbol-emacs-after-create-image-function101,4184
+(defvar image-types 127,5041
+(defvar init-file-loaded 163,6428
+(defvar message-stack 166,6501
+(defun region-active-p 249,9811
+(defvar x-symbol-data-directory 286,11176
+(defun x-symbol-directory-files 356,13453
+(defun x-symbol-event-in-current-buffer 370,13841
+(defun x-symbol-create-image 373,13890
+(defun x-symbol-make-glyph 376,13975
+(defun x-symbol-set-glyph-image 379,14046
+(defvar x-symbol-heading-strut-glyph 394,14543
+(defvar x-symbol-invisible-face 397,14630
+(defvar x-symbol-face 398,14688
+(defvar x-symbol-sub-face 399,14726
+(defvar x-symbol-sup-face 400,14772
+(defvar x-symbol-emacs-w32-font-directories402,14819
+(defvar x-symbol-invisible-display-table 415,15297
+(defalias 'x-symbol-window-width x-symbol-window-width
417,15344
+(defun x-symbol-set-face-font 428,15796
+(defun x-symbol-event-matches-key-specifier-p 439,16269
+(defun start-itimer 449,16541
+(defun itimer-live-p 451,16638
 
 x-symbol/lisp/x-symbol-hooks.el,3109
 (defvar x-symbol-warn-of-old-emacs 66,2522
@@ -3161,15 +3179,15 @@ x-symbol/lisp/x-symbol-mule.el,1507
 (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 179,7564
-(defun x-symbol-mule-init-charsym-syntax 209,8700
-(defun x-symbol-mule-init-quail-bindings 225,9330
-(defun x-symbol-mule-encode-charsym-after 244,10054
-(defun x-symbol-mule-charsym-after 248,10159
-(defun x-symbol-mule-string-to-charsyms 257,10570
-(defun x-symbol-mule-match-before 270,11056
-(defun x-symbol-mule-pre-command-hook 294,12046
-(defun x-symbol-mule-post-command-hook 303,12449
+(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
@@ -3320,7 +3338,7 @@ x-symbol/lisp/x-symbol-unicode.el,170
 x-symbol/lisp/x-symbol-unicode-extras.el,38
 (defconst x-symol-unicode-extras 2,1
 
-x-symbol/lisp/x-symbol-vars.el,8055
+x-symbol/lisp/x-symbol-vars.el,8058
 (defconst x-symbol-version 40,1516
 (defgroup x-symbol 49,1858
 (defgroup x-symbol-mode 56,2069
@@ -3486,7 +3504,7 @@ x-symbol/lisp/x-symbol-vars.el,8055
 (defcustom x-symbol-image-convert-program1961,79365
 (defcustom x-symbol-image-converter1967,79592
 (defun x-symbol-variable-interactive 2074,84086
-(defvar x-symbol-use-unicode 2093,84916
+(defcustom x-symbol-use-unicode 2093,84916
 
 x-symbol/lisp/x-symbol-xmacs.el,522
 (defun x-symbol-paren-reset-mode 102,4657
@@ -3503,94 +3521,95 @@ x-symbol/lisp/x-symbol-xmacs.el,522
 TODO.developer,26
    function to 401,16137
 
-doc/ProofGeneral.texi,5313
+doc/ProofGeneral.texi,5379
 @node Top166,5052
 @node Preface203,6168
 @node Latest news for version 3.7Latest news for version 3.7
226,6764
 @node Future264,8432
 @node Credits295,9731
 @node Introducing Proof GeneralIntroducing Proof General
394,13165
-@node Quick start guideQuick start guide
449,15157
-@node Features of Proof GeneralFeatures of Proof General
502,17646
-@node Supported proof assistantsSupported proof assistants
591,21571
-@node Prerequisites for this manualPrerequisites for this manual
640,23477
-@node Organization of this manualOrganization of this manual
684,25103
-@node Basic Script ManagementBasic Script Management
710,25931
-@node Walkthrough example in IsabelleWalkthrough example in Isabelle
729,26531
-@node Proof scriptsProof scripts
978,36097
-@node Script buffersScript buffers
1021,38217
-@node Locked queue and editing regionsLocked queue and editing regions
1043,38794
-@node Goal-save sequencesGoal-save sequences
1099,40941
-@node Active scripting bufferActive scripting buffer
1136,42427
-@node Summary of Proof General buffersSummary of Proof General buffers
1205,45847
-@node Script editing commandsScript editing commands
1267,48521
-@node Script processing commandsScript processing commands
1345,51379
-@node Proof assistant commandsProof assistant commands
1473,56680
-@node Toolbar commandsToolbar commands
1623,61684
-@node Interrupting during trace outputInterrupting during trace output
1647,62613
-@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
1686,64537
-@node Goals buffer commandsGoals buffer commands
1700,65037
-@node Advanced Script ManagementAdvanced Script Management
1789,68570
-@node Visibility of completed proofsVisibility of completed proofs
1820,69724
-@node Switching between proof scriptsSwitching between proof scripts
1875,71647
-@node View of processed files View of processed files 
1912,73619
-@node Retracting across filesRetracting across files
1972,76670
-@node Asserting across filesAsserting across files
1985,77301
-@node Automatic multiple file handlingAutomatic multiple file handling
1998,77867
-@node Escaping script managementEscaping script management
2023,78901
-@node Experimental featuresExperimental features
2081,81104
-@node Support for other PackagesSupport for other Packages
2115,82367
-@node Syntax highlightingSyntax highlighting
2147,83242
-@node X-Symbol supportX-Symbol support
2186,84863
-@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)
2245,87409
-@node Support for outline modeSupport for outline mode
2304,89539
-@node Support for completionSupport for completion
2330,90669
-@node Support for tagsSupport for tags
2387,92837
-@node Customizing Proof GeneralCustomizing Proof General
2439,95166
-@node Basic optionsBasic options
2479,96836
-@node How to customizeHow to customize
2503,97594
-@node Display customizationDisplay customization
2554,99696
-@node User optionsUser options
2679,104930
-@node Changing facesChanging faces
2943,114341
-@node Tweaking configuration settingsTweaking configuration settings
3018,117010
-@node Hints and TipsHints and Tips
3075,119536
-@node Adding your own keybindingsAdding your own keybindings
3094,120137
-@node Using file variablesUsing file variables
3150,122670
-@node Using abbreviationsUsing abbreviations
3209,124856
-@node LEGO Proof GeneralLEGO Proof General
3248,126272
-@node LEGO specific commandsLEGO specific commands
3289,127641
-@node LEGO tagsLEGO tags
3309,128096
-@node LEGO customizationsLEGO customizations
3319,128343
-@node Coq Proof GeneralCoq Proof General
3351,129262
-@node Coq-specific commandsCoq-specific commands
3367,129671
-@node Coq-specific variablesCoq-specific variables
3389,130178
-@node Editing multiple proofsEditing multiple proofs
3411,130836
-@node User-loaded tacticsUser-loaded tactics
3435,131944
-@node Holes featureHoles feature
3499,134418
-@node Isabelle Proof GeneralIsabelle Proof General
3526,135705
-@node Isabelle commandsIsabelle commands
3556,136835
-@node Logics and SettingsLogics and Settings
3663,139883
-@node Isabelle customizationsIsabelle customizations
3697,141423
-@node HOL Proof GeneralHOL Proof General
3721,141905
-@node Shell Proof GeneralShell Proof General
3763,143727
-@node Obtaining and InstallingObtaining and Installing
3799,145186
-@node Obtaining Proof GeneralObtaining Proof General
3815,145599
-@node Installing Proof General from tarballInstalling Proof General from tarball
3846,146838
-@node Installing Proof General from RPM packageInstalling Proof General from RPM package
3871,147670
-@node Setting the names of binariesSetting the names of binaries
3886,148078
-@node Notes for syssiesNotes for syssies
3914,149018
-@node Bugs and EnhancementsBugs and Enhancements
3987,151956
-@node References4008,152771
-@node History of Proof GeneralHistory of Proof General
4048,153795
-@node Old News for 3.0Old News for 3.0
4139,157897
-@node Old News for 3.1Old News for 3.1
4209,161591
-@node Old News for 3.2Old News for 3.2
4235,162763
-@node Old News for 3.3Old News for 3.3
4296,165766
-@node Old News for 3.4Old News for 3.4
4315,166663
-@node Function IndexFunction Index
4338,167719
-@node Variable IndexVariable Index
4342,167795
-@node Keystroke IndexKeystroke Index
4346,167875
-@node Concept IndexConcept Index
4350,167941
+@node Installing Proof GeneralInstalling Proof General
450,15197
+@node Quick start guideQuick start guide
464,15645
+@node Features of Proof GeneralFeatures of Proof General
508,17753
+@node Supported proof assistantsSupported proof assistants
597,21678
+@node Prerequisites for this manualPrerequisites for this manual
646,23584
+@node Organization of this manualOrganization of this manual
690,25210
+@node Basic Script ManagementBasic Script Management
716,26038
+@node Walkthrough example in IsabelleWalkthrough example in Isabelle
735,26638
+@node Proof scriptsProof scripts
986,36291
+@node Script buffersScript buffers
1029,38411
+@node Locked queue and editing regionsLocked queue and editing regions
1051,38988
+@node Goal-save sequencesGoal-save sequences
1107,41135
+@node Active scripting bufferActive scripting buffer
1144,42621
+@node Summary of Proof General buffersSummary of Proof General buffers
1213,46041
+@node Script editing commandsScript editing commands
1275,48715
+@node Script processing commandsScript processing commands
1353,51573
+@node Proof assistant commandsProof assistant commands
1481,56874
+@node Toolbar commandsToolbar commands
1631,61878
+@node Interrupting during trace outputInterrupting during trace output
1655,62807
+@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
1694,64731
+@node Goals buffer commandsGoals buffer commands
1708,65231
+@node Advanced Script ManagementAdvanced Script Management
1797,68764
+@node Visibility of completed proofsVisibility of completed proofs
1828,69918
+@node Switching between proof scriptsSwitching between proof scripts
1883,71841
+@node View of processed files View of processed files 
1920,73813
+@node Retracting across filesRetracting across files
1980,76864
+@node Asserting across filesAsserting across files
1993,77495
+@node Automatic multiple file handlingAutomatic multiple file handling
2006,78061
+@node Escaping script managementEscaping script management
2031,79095
+@node Experimental featuresExperimental features
2089,81298
+@node Support for other PackagesSupport for other Packages
2123,82561
+@node Syntax highlightingSyntax highlighting
2155,83436
+@node X-Symbol supportX-Symbol support
2194,85057
+@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)
2253,87603
+@node Support for outline modeSupport for outline mode
2312,89733
+@node Support for completionSupport for completion
2338,90863
+@node Support for tagsSupport for tags
2395,93031
+@node Customizing Proof GeneralCustomizing Proof General
2447,95360
+@node Basic optionsBasic options
2487,97030
+@node How to customizeHow to customize
2511,97788
+@node Display customizationDisplay customization
2562,99890
+@node User optionsUser options
2687,105124
+@node Changing facesChanging faces
2951,114535
+@node Tweaking configuration settingsTweaking configuration settings
3026,117204
+@node Hints and TipsHints and Tips
3083,119730
+@node Adding your own keybindingsAdding your own keybindings
3102,120331
+@node Using file variablesUsing file variables
3158,122864
+@node Using abbreviationsUsing abbreviations
3217,125050
+@node LEGO Proof GeneralLEGO Proof General
3256,126466
+@node LEGO specific commandsLEGO specific commands
3297,127835
+@node LEGO tagsLEGO tags
3317,128290
+@node LEGO customizationsLEGO customizations
3327,128537
+@node Coq Proof GeneralCoq Proof General
3359,129456
+@node Coq-specific commandsCoq-specific commands
3375,129865
+@node Coq-specific variablesCoq-specific variables
3397,130372
+@node Editing multiple proofsEditing multiple proofs
3419,131030
+@node User-loaded tacticsUser-loaded tactics
3443,132138
+@node Holes featureHoles feature
3507,134612
+@node Isabelle Proof GeneralIsabelle Proof General
3534,135899
+@node Isabelle commandsIsabelle commands
3564,137029
+@node Logics and SettingsLogics and Settings
3671,140077
+@node Isabelle customizationsIsabelle customizations
3705,141617
+@node HOL Proof GeneralHOL Proof General
3729,142099
+@node Shell Proof GeneralShell Proof General
3771,143921
+@node Obtaining and InstallingObtaining and Installing
3807,145380
+@node Obtaining Proof GeneralObtaining Proof General
3823,145793
+@node Installing Proof General from tarballInstalling Proof General from tarball
3854,147032
+@node Installing Proof General from RPM packageInstalling Proof General from RPM package
3879,147864
+@node Setting the names of binariesSetting the names of binaries
3894,148272
+@node Notes for syssiesNotes for syssies
3922,149212
+@node Bugs and EnhancementsBugs and Enhancements
3995,152150
+@node References4016,152965
+@node History of Proof GeneralHistory of Proof General
4056,153989
+@node Old News for 3.0Old News for 3.0
4147,158091
+@node Old News for 3.1Old News for 3.1
4217,161785
+@node Old News for 3.2Old News for 3.2
4243,162957
+@node Old News for 3.3Old News for 3.3
4304,165960
+@node Old News for 3.4Old News for 3.4
4323,166857
+@node Function IndexFunction Index
4346,167913
+@node Variable IndexVariable Index
4350,167989
+@node Keystroke IndexKeystroke Index
4354,168069
+@node Concept IndexConcept Index
4358,168135
 
 doc/PG-adapting.texi,3776
 @node Top157,4775