Updated.

1 files changed, 783 insertions, 705 deletions

diff --git a/TAGS b/TAGS
index a7d7c3b8..0d1407de 100644
--- a/TAGS
+++ b/TAGS
@@ -11,8 +11,8 @@ coq/coq-abbrev.el,495
 (defconst coq-terms-menu43,1284
 (defconst coq-terms-abbrev-table48,1422
 (defun coq-install-abbrevs 55,1616
-(defpgdefault menu-entries74,2286
-(defpgdefault help-menu-entries155,5695
+(defpgdefault menu-entries75,2353
+(defpgdefault help-menu-entries156,5762
 
 coq/coq-db.el,559
 (defconst coq-syntax-db 22,534
@@ -31,168 +31,168 @@ coq/coq-db.el,559
 (defconst coq-solve-tactics-face 229,8518
 
 coq/coq.el,6441
-(defcustom coq-translate-to-v8 45,1303
-(defun coq-build-prog-args 51,1483
-(defcustom coq-compile-file-command 64,1863
-(defcustom coq-default-undo-limit 74,2232
-(defconst coq-shell-init-cmd 79,2360
-(defcustom coq-prog-env 96,2960
-(defconst coq-shell-restart-cmd 104,3212
-(defvar coq-shell-prompt-pattern 111,3472
-(defvar coq-shell-cd 119,3801
-(defvar coq-shell-abort-goal-regexp 123,3956
-(defvar coq-shell-proof-completed-regexp 126,4082
-(defvar coq-goal-regexp129,4234
-(defun coq-library-directory 138,4423
-(defcustom coq-tags 145,4603
-(defconst coq-interrupt-regexp 150,4753
-(defcustom coq-www-home-page 155,4874
-(defvar coq-outline-regexp165,5045
-(defvar coq-outline-heading-end-regexp 172,5259
-(defvar coq-shell-outline-regexp 174,5313
-(defvar coq-shell-outline-heading-end-regexp 175,5363
-(defconst coq-kill-goal-command 180,5473
-(defconst coq-forget-id-command 181,5516
-(defconst coq-back-n-command 182,5563
-(defconst coq-state-preserving-tactics-regexp 186,5707
-(defconst coq-state-changing-commands-regexp188,5808
-(defconst coq-state-preserving-commands-regexp 190,5915
-(defconst coq-commands-regexp 192,6027
-(defvar coq-retractable-instruct-regexp 194,6105
-(defvar coq-non-retractable-instruct-regexp 196,6196
-(defvar coq-keywords-section200,6336
-(defvar coq-section-regexp 203,6430
-(defun coq-set-undo-limit 240,7576
-(defconst coq-keywords-decl-defn-regexp251,8015
-(defun coq-proof-mode-p 255,8165
-(defun coq-is-comment-or-proverprocp 266,8573
-(defun coq-is-goalsave-p 268,8677
-(defun coq-is-module-equal-p 269,8752
-(defun coq-is-def-p 272,8948
-(defun coq-is-decl-defn-p 274,9056
-(defun coq-state-preserving-command-p 279,9223
-(defun coq-command-p 282,9357
-(defun coq-state-preserving-tactic-p 285,9457
-(defun coq-state-changing-tactic-p 290,9605
-(defun coq-state-changing-command-p 297,9839
-(defun coq-section-or-module-start-p 304,10185
-(defun build-list-id-from-string 313,10426
-(defun coq-last-prompt-info 326,10956
-(defun coq-last-prompt-info-safe 338,11497
-(defvar coq-last-but-one-statenum 344,11754
-(defvar coq-last-but-one-proofnum 350,12052
-(defvar coq-last-but-one-proofstack 353,12150
-(defun coq-get-span-statenum 356,12260
-(defun coq-get-span-proofnum 361,12375
-(defun coq-get-span-proofstack 366,12490
-(defun coq-set-span-statenum 371,12634
-(defun coq-get-span-goalcmd 376,12765
-(defun coq-set-span-goalcmd 381,12879
-(defun coq-set-span-proofnum 386,13009
-(defun coq-set-span-proofstack 391,13140
-(defun proof-last-locked-span 396,13300
-(defun coq-set-state-infos 411,13904
-(defun count-not-intersection 451,15983
-(defun  coq-find-and-forget-v81 482,17237
-(defun coq-find-and-forget-v80 510,18369
-(defun coq-find-and-forget 605,23068
-(defvar coq-current-goal 618,23608
-(defun coq-goal-hyp 621,23673
-(defun coq-state-preserving-p 634,24106
-(defconst notation-print-kinds-table 648,24611
-(defun coq-PrintScope 652,24779
-(defun coq-guess-or-ask-for-string 671,25335
-(defun coq-ask-do 682,25722
-(defun coq-SearchIsos 691,26110
-(defun coq-SearchConstant 697,26343
-(defun coq-SearchRewrite 701,26436
-(defun coq-SearchAbout 705,26534
-(defun coq-Print 709,26626
-(defun coq-About 713,26748
-(defun coq-LocateConstant 717,26865
-(defun coq-LocateLibrary 723,27000
-(defun coq-addquotes 729,27150
-(defun coq-LocateNotation 731,27198
-(defun coq-Pwd 738,27397
-(defun coq-Inspect 744,27529
-(defun coq-PrintSection(748,27629
-(defun coq-Print-implicit 752,27722
-(defun coq-Check 757,27873
-(defun coq-Show 762,27981
-(defun coq-Compile 776,28424
-(defun coq-guess-command-line 790,28744
-(defun coq-mode-config 820,30153
-(defvar coq-last-hybrid-pre-string 932,34259
-(defun coq-hybrid-ouput-goals-response-p 935,34438
-(defun coq-hybrid-ouput-goals-response 941,34696
-(defun coq-shell-mode-config 962,35656
-(defun coq-goals-mode-config 1006,37727
-(defun coq-response-config 1013,37959
-(defpacustom print-fully-explicit 1036,38668
-(defpacustom print-implicit 1041,38817
-(defpacustom print-coercions 1046,38984
-(defpacustom print-match-wildcards 1051,39129
-(defpacustom print-elim-types 1056,39310
-(defpacustom printing-depth 1061,39477
-(defpacustom undo-depth 1066,39639
-(defpacustom time-commands 1071,39787
-(defpacustom auto-compile-vos 1075,39898
-(defun coq-maybe-compile-buffer 1104,41014
-(defun coq-ancestors-of 1141,42548
-(defun coq-all-ancestors-of 1164,43515
-(defconst coq-require-command-regexp 1176,43908
-(defun coq-process-require-command 1181,44117
-(defun coq-included-children 1186,44244
-(defun coq-process-file 1207,45083
-(defun coq-preprocessing 1222,45622
-(defun coq-fake-constant-markup 1237,46041
-(defun coq-create-span-menu 1258,46847
-(defconst module-kinds-table 1275,47346
-(defconst modtype-kinds-table1279,47496
-(defun coq-insert-section-or-module 1283,47625
-(defconst reqkinds-kinds-table1306,48485
-(defun coq-insert-requires 1311,48630
-(defun coq-end-Section 1327,49136
-(defun coq-insert-intros 1345,49720
-(defun coq-insert-infoH-hook 1358,50245
-(defun coq-insert-as 1362,50323
-(defun coq-insert-match 1383,51072
-(defun coq-insert-tactic 1415,52250
-(defun coq-insert-tactical 1421,52489
-(defun coq-insert-command 1427,52738
-(defun coq-insert-term 1433,52982
-(define-key coq-keymap 1439,53179
-(define-key coq-keymap 1440,53237
-(define-key coq-keymap 1441,53294
-(define-key coq-keymap 1442,53363
-(define-key coq-keymap 1443,53419
-(define-key coq-keymap 1444,53468
-(define-key coq-keymap 1445,53526
-(define-key coq-keymap 1447,53587
-(define-key coq-keymap 1448,53646
-(define-key coq-keymap 1450,53710
-(define-key coq-keymap 1451,53770
-(define-key coq-keymap 1453,53826
-(define-key coq-keymap 1454,53876
-(define-key coq-keymap 1455,53926
-(define-key coq-keymap 1456,53976
-(define-key coq-keymap 1457,54030
-(define-key coq-keymap 1458,54089
-(defvar last-coq-error-location 1468,54272
-(defun coq-get-last-error-location 1477,54671
-(defun coq-highlight-error 1510,56068
-(defvar coq-allow-highlight-error 1575,58623
-(defun coq-decide-highlight-error 1581,58889
-(defun coq-highlight-error-hook 1586,59051
-(defun first-word-of-buffer 1597,59444
-(defun coq-show-first-goal 1607,59676
-(defvar coq-modeline-string2 1624,60371
-(defvar coq-modeline-string1 1625,60415
-(defvar coq-modeline-string0 1626,60458
-(defun coq-build-subgoals-string 1627,60503
-(defun coq-update-minor-mode-alist 1632,60671
-(defun is-not-split-vertic 1658,61739
-(defun optim-resp-windows 1667,62178
+(defcustom coq-translate-to-v8 45,1304
+(defun coq-build-prog-args 51,1484
+(defcustom coq-compile-file-command 64,1864
+(defcustom coq-default-undo-limit 74,2233
+(defconst coq-shell-init-cmd 79,2361
+(defcustom coq-prog-env 96,2961
+(defconst coq-shell-restart-cmd 104,3213
+(defvar coq-shell-prompt-pattern 111,3473
+(defvar coq-shell-cd 119,3802
+(defvar coq-shell-abort-goal-regexp 123,3957
+(defvar coq-shell-proof-completed-regexp 126,4083
+(defvar coq-goal-regexp129,4235
+(defun coq-library-directory 138,4424
+(defcustom coq-tags 145,4604
+(defconst coq-interrupt-regexp 150,4754
+(defcustom coq-www-home-page 155,4875
+(defvar coq-outline-regexp165,5046
+(defvar coq-outline-heading-end-regexp 172,5260
+(defvar coq-shell-outline-regexp 174,5314
+(defvar coq-shell-outline-heading-end-regexp 175,5364
+(defconst coq-kill-goal-command 180,5474
+(defconst coq-forget-id-command 181,5517
+(defconst coq-back-n-command 182,5564
+(defconst coq-state-preserving-tactics-regexp 186,5708
+(defconst coq-state-changing-commands-regexp188,5809
+(defconst coq-state-preserving-commands-regexp 190,5916
+(defconst coq-commands-regexp 192,6028
+(defvar coq-retractable-instruct-regexp 194,6106
+(defvar coq-non-retractable-instruct-regexp 196,6197
+(defvar coq-keywords-section200,6337
+(defvar coq-section-regexp 203,6431
+(defun coq-set-undo-limit 240,7577
+(defconst coq-keywords-decl-defn-regexp251,8016
+(defun coq-proof-mode-p 255,8166
+(defun coq-is-comment-or-proverprocp 266,8574
+(defun coq-is-goalsave-p 268,8678
+(defun coq-is-module-equal-p 269,8753
+(defun coq-is-def-p 272,8949
+(defun coq-is-decl-defn-p 274,9057
+(defun coq-state-preserving-command-p 279,9224
+(defun coq-command-p 282,9358
+(defun coq-state-preserving-tactic-p 285,9458
+(defun coq-state-changing-tactic-p 290,9606
+(defun coq-state-changing-command-p 297,9840
+(defun coq-section-or-module-start-p 304,10186
+(defun build-list-id-from-string 313,10427
+(defun coq-last-prompt-info 326,10957
+(defun coq-last-prompt-info-safe 338,11498
+(defvar coq-last-but-one-statenum 344,11755
+(defvar coq-last-but-one-proofnum 350,12053
+(defvar coq-last-but-one-proofstack 353,12151
+(defun coq-get-span-statenum 356,12261
+(defun coq-get-span-proofnum 361,12376
+(defun coq-get-span-proofstack 366,12491
+(defun coq-set-span-statenum 371,12635
+(defun coq-get-span-goalcmd 376,12766
+(defun coq-set-span-goalcmd 381,12880
+(defun coq-set-span-proofnum 386,13010
+(defun coq-set-span-proofstack 391,13141
+(defun proof-last-locked-span 396,13301
+(defun coq-set-state-infos 411,13905
+(defun count-not-intersection 451,15984
+(defun  coq-find-and-forget-v81 482,17238
+(defun coq-find-and-forget-v80 510,18370
+(defun coq-find-and-forget 605,23069
+(defvar coq-current-goal 618,23609
+(defun coq-goal-hyp 621,23674
+(defun coq-state-preserving-p 634,24107
+(defconst notation-print-kinds-table 648,24612
+(defun coq-PrintScope 652,24780
+(defun coq-guess-or-ask-for-string 671,25336
+(defun coq-ask-do 682,25723
+(defun coq-SearchIsos 691,26111
+(defun coq-SearchConstant 697,26344
+(defun coq-SearchRewrite 701,26437
+(defun coq-SearchAbout 705,26535
+(defun coq-Print 709,26627
+(defun coq-About 713,26749
+(defun coq-LocateConstant 717,26866
+(defun coq-LocateLibrary 723,27001
+(defun coq-addquotes 729,27151
+(defun coq-LocateNotation 731,27199
+(defun coq-Pwd 738,27398
+(defun coq-Inspect 744,27530
+(defun coq-PrintSection(748,27630
+(defun coq-Print-implicit 752,27723
+(defun coq-Check 757,27874
+(defun coq-Show 762,27982
+(defun coq-Compile 776,28425
+(defun coq-guess-command-line 790,28745
+(defun coq-mode-config 820,30155
+(defvar coq-last-hybrid-pre-string 932,34261
+(defun coq-hybrid-ouput-goals-response-p 935,34440
+(defun coq-hybrid-ouput-goals-response 941,34698
+(defun coq-shell-mode-config 962,35658
+(defun coq-goals-mode-config 1006,37729
+(defun coq-response-config 1013,37961
+(defpacustom print-fully-explicit 1036,38670
+(defpacustom print-implicit 1041,38819
+(defpacustom print-coercions 1046,38986
+(defpacustom print-match-wildcards 1051,39131
+(defpacustom print-elim-types 1056,39312
+(defpacustom printing-depth 1061,39479
+(defpacustom undo-depth 1066,39641
+(defpacustom time-commands 1071,39789
+(defpacustom auto-compile-vos 1075,39900
+(defun coq-maybe-compile-buffer 1104,41016
+(defun coq-ancestors-of 1141,42550
+(defun coq-all-ancestors-of 1164,43517
+(defconst coq-require-command-regexp 1176,43910
+(defun coq-process-require-command 1181,44119
+(defun coq-included-children 1186,44246
+(defun coq-process-file 1207,45085
+(defun coq-preprocessing 1222,45624
+(defun coq-fake-constant-markup 1237,46043
+(defun coq-create-span-menu 1258,46849
+(defconst module-kinds-table 1275,47348
+(defconst modtype-kinds-table1279,47498
+(defun coq-insert-section-or-module 1283,47627
+(defconst reqkinds-kinds-table1306,48487
+(defun coq-insert-requires 1311,48632
+(defun coq-end-Section 1327,49138
+(defun coq-insert-intros 1345,49722
+(defun coq-insert-infoH-hook 1358,50247
+(defun coq-insert-as 1362,50325
+(defun coq-insert-match 1383,51074
+(defun coq-insert-tactic 1415,52252
+(defun coq-insert-tactical 1421,52491
+(defun coq-insert-command 1427,52740
+(defun coq-insert-term 1433,52984
+(define-key coq-keymap 1439,53181
+(define-key coq-keymap 1440,53239
+(define-key coq-keymap 1441,53296
+(define-key coq-keymap 1442,53365
+(define-key coq-keymap 1443,53421
+(define-key coq-keymap 1444,53470
+(define-key coq-keymap 1445,53528
+(define-key coq-keymap 1447,53589
+(define-key coq-keymap 1448,53648
+(define-key coq-keymap 1450,53712
+(define-key coq-keymap 1451,53772
+(define-key coq-keymap 1453,53828
+(define-key coq-keymap 1454,53878
+(define-key coq-keymap 1455,53928
+(define-key coq-keymap 1456,53978
+(define-key coq-keymap 1457,54032
+(define-key coq-keymap 1458,54091
+(defvar last-coq-error-location 1468,54274
+(defun coq-get-last-error-location 1477,54673
+(defun coq-highlight-error 1510,56069
+(defvar coq-allow-highlight-error 1576,58749
+(defun coq-decide-highlight-error 1582,59015
+(defun coq-highlight-error-hook 1587,59177
+(defun first-word-of-buffer 1598,59570
+(defun coq-show-first-goal 1608,59802
+(defvar coq-modeline-string2 1625,60497
+(defvar coq-modeline-string1 1626,60541
+(defvar coq-modeline-string0 1627,60584
+(defun coq-build-subgoals-string 1628,60629
+(defun coq-update-minor-mode-alist 1633,60797
+(defun is-not-split-vertic 1659,61865
+(defun optim-resp-windows 1668,62304
 
 coq/coq-indent.el,2259
 (defconst coq-any-command-regexp17,315
@@ -385,41 +385,43 @@ demoisa/demoisa.el,349
 (define-derived-mode demoisa-response-mode 127,4196
 (define-derived-mode demoisa-goals-mode 131,4323
 
-isar/isabelle-system.el,1401
+isar/isabelle-system.el,1512
 (defgroup isabelle 26,775
 (defcustom isabelle-web-page30,903
 (defcustom isa-isatool-command41,1198
-(defvar isatool-not-found 71,2260
-(defun isa-set-isatool-command 74,2373
-(defun isa-shell-command-to-string 97,3317
-(defun isa-getenv 103,3541
-(defcustom isabelle-program-name123,4228
-(defvar isabelle-prog-name 149,5158
-(defun isa-tool-list-logics 152,5285
-(defcustom isabelle-logics-available 159,5522
-(defcustom isabelle-chosen-logic 170,5886
-(defun isabelle-command-line 183,6354
-(defun isabelle-choose-logic 206,7311
-(defun isa-view-doc 228,8277
-(defun isa-tool-list-docs 237,8541
-(defconst isabelle-verbatim-regexp 264,9573
-(defun isabelle-verbatim 267,9715
-(defcustom isabelle-refresh-logics 274,9876
-(defvar isabelle-docs-menu 282,10203
-(defvar isabelle-logics-menu-entries 290,10490
-(defun isabelle-logics-menu-calculate 293,10563
-(defvar isabelle-time-to-refresh-logics 312,11126
-(defun isabelle-logics-menu-refresh 316,11221
-(defun isabelle-logics-menu-filter 333,11918
-(defun isabelle-menu-bar-update-logics 339,12128
-(defvar isabelle-logics-menu350,12467
-(defun isabelle-load-isar-keywords 363,13079
-(defpgdefault menu-entries384,13820
-(defpgdefault help-menu-entries 387,13872
-(defun isabelle-convert-idmarkup-to-subterm 415,14630
-(defun isabelle-create-span-menu 439,15641
-(defun isabelle-xml-sml-escapes 455,16083
-(defun isabelle-process-pgip 458,16184
+(defvar isatool-not-found 59,1857
+(defun isa-set-isatool-command 62,1970
+(defun isa-shell-command-to-string 85,2914
+(defun isa-getenv 91,3138
+(defcustom isabelle-program-name-override 111,3825
+(defvar isabelle-prog-name 128,4409
+(defun isa-tool-list-logics 131,4519
+(defcustom isabelle-logics-available 138,4756
+(defcustom isabelle-chosen-logic 148,5092
+(defvar isabelle-chosen-logic-prev 163,5617
+(defun isabelle-hack-local-variables-function 166,5739
+(defun isabelle-set-prog-name 178,6180
+(defun isabelle-choose-logic 203,7339
+(defun isa-view-doc 222,8101
+(defun isa-tool-list-docs 231,8365
+(defconst isabelle-verbatim-regexp 258,9397
+(defun isabelle-verbatim 261,9539
+(defcustom isabelle-refresh-logics 268,9700
+(defvar isabelle-docs-menu 276,10027
+(defvar isabelle-logics-menu-entries 283,10313
+(defun isabelle-logics-menu-calculate 286,10386
+(defvar isabelle-time-to-refresh-logics 307,11028
+(defun isabelle-logics-menu-refresh 311,11123
+(defun isabelle-logics-menu-filter 328,11820
+(defun isabelle-menu-bar-update-logics 334,12030
+(defvar isabelle-logics-menu345,12369
+(defun isabelle-load-isar-keywords 358,12981
+(defpgdefault menu-entries379,13722
+(defpgdefault help-menu-entries 382,13774
+(defun isabelle-convert-idmarkup-to-subterm 410,14532
+(defun isabelle-create-span-menu 434,15543
+(defun isabelle-xml-sml-escapes 450,15985
+(defun isabelle-process-pgip 453,16086
 
 isar/isar.el,1162
 (defcustom isar-keywords-name 31,720
@@ -428,28 +430,28 @@ isar/isar.el,1162
 (defun isar-strip-terminators 64,1632
 (defun isar-markup-ml 77,2009
 (defun isar-mode-config-set-variables 82,2144
-(defun isar-shell-mode-config-set-variables 150,5325
-(defun isar-remove-file 246,9315
-(defun isar-shell-compute-new-files-list 256,9678
-(define-derived-mode isar-shell-mode 272,10199
-(define-derived-mode isar-response-mode 277,10322
-(define-derived-mode isar-goals-mode 282,10504
-(define-derived-mode isar-mode 287,10679
-(defpgdefault menu-entries344,12714
-(defun isar-count-undos 374,13953
-(defun isar-find-and-forget 401,15067
-(defun isar-goal-command-p 440,16647
-(defun isar-global-save-command-p 445,16824
-(defvar isar-current-goal 466,17685
-(defun isar-state-preserving-p 469,17751
-(defvar isar-shell-current-line-width 494,18948
-(defun isar-shell-adjust-line-width 499,19140
-(defun isar-preprocessing 522,20031
-(defun isar-mode-config 545,21298
-(defun isar-shell-mode-config 556,21799
-(defun isar-response-mode-config 567,22158
-(defun isar-goals-mode-config 576,22401
-(defun isar-goalhyplit-test 587,22733
+(defun isar-shell-mode-config-set-variables 152,5365
+(defun isar-remove-file 248,9355
+(defun isar-shell-compute-new-files-list 258,9718
+(define-derived-mode isar-shell-mode 274,10239
+(define-derived-mode isar-response-mode 279,10362
+(define-derived-mode isar-goals-mode 284,10544
+(define-derived-mode isar-mode 289,10719
+(defpgdefault menu-entries346,12754
+(defun isar-count-undos 376,13993
+(defun isar-find-and-forget 403,15107
+(defun isar-goal-command-p 442,16687
+(defun isar-global-save-command-p 447,16864
+(defvar isar-current-goal 468,17725
+(defun isar-state-preserving-p 471,17791
+(defvar isar-shell-current-line-width 496,18988
+(defun isar-shell-adjust-line-width 501,19180
+(defun isar-preprocessing 524,20071
+(defun isar-mode-config 547,21338
+(defun isar-shell-mode-config 558,21839
+(defun isar-response-mode-config 569,22198
+(defun isar-goals-mode-config 578,22441
+(defun isar-goalhyplit-test 589,22773
 
 isar/isar-find-theorems.el,778
 (defun isar-find-theorems-minibuffer 18,712
@@ -499,90 +501,103 @@ isar/isar-mmm.el,83
 (defconst isar-start-latex-regexp 23,697
 (defconst isar-start-sml-regexp 35,1130
 
-isar/isar-syntax.el,3471
-(defconst isar-script-syntax-table-entries20,471
-(defconst isar-script-syntax-table-alist61,1502
-(defun isar-init-syntax-table 70,1792
-(defun isar-init-output-syntax-table 78,2039
-(defconst isar-keyword-begin 94,2486
-(defconst isar-keyword-end 95,2524
-(defconst isar-keywords-theory-enclose97,2559
-(defconst isar-keywords-theory102,2704
-(defconst isar-keywords-save107,2849
-(defconst isar-keywords-proof-enclose112,2978
-(defconst isar-keywords-proof118,3160
-(defconst isar-keywords-proof-context125,3365
-(defconst isar-keywords-local-goal129,3479
-(defconst isar-keywords-proper133,3591
-(defconst isar-keywords-improper138,3724
-(defconst isar-keywords-outline143,3870
-(defconst isar-keywords-fume146,3935
-(defconst isar-keywords-indent-open153,4153
-(defconst isar-keywords-indent-close159,4337
-(defconst isar-keywords-indent-enclose163,4442
-(defun isar-regexp-simple-alt 172,4657
-(defun isar-ids-to-regexp 192,5417
-(defconst isar-ext-first 226,6823
-(defconst isar-ext-rest 227,6890
-(defconst isar-long-id-stuff 229,6962
-(defconst isar-id 230,7036
-(defconst isar-idx 231,7106
-(defconst isar-string 233,7165
-(defconst isar-any-command-regexp235,7225
-(defconst isar-name-regexp239,7359
-(defconst isar-improper-regexp245,7654
-(defconst isar-save-command-regexp249,7802
-(defconst isar-global-save-command-regexp252,7903
-(defconst isar-goal-command-regexp255,8017
-(defconst isar-local-goal-command-regexp258,8125
-(defconst isar-comment-start 261,8238
-(defconst isar-comment-end 262,8273
-(defconst isar-comment-start-regexp 263,8306
-(defconst isar-comment-end-regexp 264,8377
-(defconst isar-string-start-regexp 266,8445
-(defconst isar-string-end-regexp 267,8497
-(defconst isar-antiq-regexp276,8750
-(defconst isar-nesting-regexp283,8911
-(defun isar-nesting 286,9009
-(defun isar-match-nesting 298,9430
-(defface isabelle-class-name-face310,9761
-(defface isabelle-tfree-name-face320,10036
-(defface isabelle-tvar-name-face330,10317
-(defface isabelle-free-name-face340,10597
-(defface isabelle-bound-name-face350,10873
-(defface isabelle-var-name-face360,11152
-(defconst isabelle-class-name-face 370,11431
-(defconst isabelle-tfree-name-face 371,11493
-(defconst isabelle-tvar-name-face 372,11555
-(defconst isabelle-free-name-face 373,11616
-(defconst isabelle-bound-name-face 374,11677
-(defconst isabelle-var-name-face 375,11739
-(defconst isar-font-lock-local378,11801
-(defvar isar-font-lock-keywords-1383,11967
-(defvar isar-output-font-lock-keywords-1397,12833
-(defvar isar-goals-font-lock-keywords424,14457
-(defconst isar-undo 458,15136
-(defun isar-remove 460,15198
-(defun isar-undos 463,15273
-(defun isar-cannot-undo 467,15379
-(defconst isar-theory-start-regexp470,15449
-(defconst isar-end-regexp476,15614
-(defconst isar-undo-fail-regexp480,15715
-(defconst isar-undo-skip-regexp484,15819
-(defconst isar-undo-ignore-regexp487,15940
-(defconst isar-undo-remove-regexp490,16005
-(defconst isar-any-entity-regexp498,16180
-(defconst isar-named-entity-regexp503,16367
-(defconst isar-unnamed-entity-regexp508,16544
-(defconst isar-next-entity-regexps511,16646
-(defconst isar-generic-expression519,16957
-(defconst isar-indent-any-regexp530,17274
-(defconst isar-indent-inner-regexp532,17367
-(defconst isar-indent-enclose-regexp534,17433
-(defconst isar-indent-open-regexp536,17549
-(defconst isar-indent-close-regexp538,17659
-(defconst isar-outline-regexp544,17796
-(defconst isar-outline-heading-end-regexp 548,17949
+isar/isar-syntax.el,3470
+(defconst isar-script-syntax-table-entries20,477
+(defconst isar-script-syntax-table-alist61,1508
+(defun isar-init-syntax-table 70,1798
+(defun isar-init-output-syntax-table 78,2045
+(defconst isar-keyword-begin 94,2492
+(defconst isar-keyword-end 95,2530
+(defconst isar-keywords-theory-enclose97,2565
+(defconst isar-keywords-theory102,2710
+(defconst isar-keywords-save107,2855
+(defconst isar-keywords-proof-enclose112,2984
+(defconst isar-keywords-proof118,3166
+(defconst isar-keywords-proof-context125,3371
+(defconst isar-keywords-local-goal129,3485
+(defconst isar-keywords-proper133,3597
+(defconst isar-keywords-improper138,3730
+(defconst isar-keywords-outline143,3876
+(defconst isar-keywords-fume146,3941
+(defconst isar-keywords-indent-open153,4159
+(defconst isar-keywords-indent-close159,4343
+(defconst isar-keywords-indent-enclose163,4448
+(defun isar-regexp-simple-alt 172,4663
+(defun isar-ids-to-regexp 192,5423
+(defconst isar-ext-first 226,6829
+(defconst isar-ext-rest 227,6896
+(defconst isar-long-id-stuff 229,6968
+(defconst isar-id 230,7042
+(defconst isar-idx 231,7112
+(defconst isar-string 233,7171
+(defconst isar-any-command-regexp235,7231
+(defconst isar-name-regexp239,7365
+(defconst isar-improper-regexp245,7660
+(defconst isar-save-command-regexp249,7808
+(defconst isar-global-save-command-regexp252,7909
+(defconst isar-goal-command-regexp255,8023
+(defconst isar-local-goal-command-regexp258,8131
+(defconst isar-comment-start 261,8244
+(defconst isar-comment-end 262,8279
+(defconst isar-comment-start-regexp 263,8312
+(defconst isar-comment-end-regexp 264,8383
+(defconst isar-string-start-regexp 266,8451
+(defconst isar-string-end-regexp 267,8503
+(defconst isar-antiq-regexp276,8756
+(defconst isar-nesting-regexp283,8917
+(defun isar-nesting 286,9015
+(defun isar-match-nesting 298,9436
+(defface isabelle-class-name-face310,9767
+(defface isabelle-tfree-name-face318,9950
+(defface isabelle-tvar-name-face326,10139
+(defface isabelle-free-name-face334,10327
+(defface isabelle-bound-name-face342,10511
+(defface isabelle-var-name-face350,10698
+(defconst isabelle-class-name-face 358,10885
+(defconst isabelle-tfree-name-face 359,10947
+(defconst isabelle-tvar-name-face 360,11009
+(defconst isabelle-free-name-face 361,11070
+(defconst isabelle-bound-name-face 362,11131
+(defconst isabelle-var-name-face 363,11193
+(defconst isar-font-lock-local366,11255
+(defvar isar-font-lock-keywords-1371,11421
+(defvar isar-output-font-lock-keywords-1385,12287
+(defvar isar-goals-font-lock-keywords412,13911
+(defconst isar-undo 446,14590
+(defun isar-remove 448,14633
+(defun isar-undos 451,14708
+(defun isar-cannot-undo 455,14814
+(defconst isar-theory-start-regexp458,14884
+(defconst isar-end-regexp464,15049
+(defconst isar-undo-fail-regexp468,15150
+(defconst isar-undo-skip-regexp472,15254
+(defconst isar-undo-ignore-regexp475,15375
+(defconst isar-undo-remove-regexp478,15440
+(defconst isar-any-entity-regexp486,15615
+(defconst isar-named-entity-regexp491,15802
+(defconst isar-unnamed-entity-regexp496,15979
+(defconst isar-next-entity-regexps499,16081
+(defconst isar-generic-expression507,16392
+(defconst isar-indent-any-regexp518,16709
+(defconst isar-indent-inner-regexp520,16802
+(defconst isar-indent-enclose-regexp522,16868
+(defconst isar-indent-open-regexp524,16984
+(defconst isar-indent-close-regexp526,17094
+(defconst isar-outline-regexp532,17231
+(defconst isar-outline-heading-end-regexp 536,17384
+
+isar/isar-unicode-tokens2.el,431
+(defconst isar-token-format 14,437
+(defconst isar-charref-format 15,475
+(defconst isar-token-prefix 16,517
+(defconst isar-token-suffix 17,552
+(defconst isar-token-match 18,585
+(defconst isar-control-token-match 19,650
+(defconst isar-control-token-format 20,724
+(defconst isar-hexcode-match 21,771
+(defconst isar-next-character-regexp 22,832
+(defcustom isar-token-name-alist24,901
+(defcustom isar-shortcut-alist492,13147
 
 isar/isar-unicode-tokens.el,431
 (defconst isar-token-format 14,433
@@ -590,12 +605,12 @@ isar/isar-unicode-tokens.el,431
 (defconst isar-token-prefix 16,513
 (defconst isar-token-suffix 17,548
 (defconst isar-token-match 18,581
-(defconst isar-control-token-match 19,635
-(defconst isar-control-token-format 20,699
-(defconst isar-hexcode-match 21,746
-(defconst isar-next-character-regexp 22,807
-(defcustom isar-token-name-alist24,876
-(defcustom isar-shortcut-alist492,13119
+(defconst isar-control-token-match 19,646
+(defconst isar-control-token-format 20,720
+(defconst isar-hexcode-match 21,767
+(defconst isar-next-character-regexp 22,828
+(defcustom isar-token-name-alist24,897
+(defcustom isar-shortcut-alist492,13140
 
 isar/x-symbol-isar.el,1775
 (defvar x-symbol-isar-required-fonts 15,498
@@ -1207,34 +1222,36 @@ generic/pg-autotest.el,442
 (defun pg-autotest-quit-prover 106,3158
 (defun pg-autotest-finished 112,3339
 
-generic/pg-custom.el,600
+generic/pg-custom.el,678
 (defpgcustom x-symbol-enable 32,1065
 (defpgcustom x-symbol-language 42,1491
 (defpgcustom maths-menu-enable 47,1713
 (defpgcustom unicode-tokens-enable 53,1893
-(defpgcustom mmm-enable 59,2070
-(defpgcustom script-indent 68,2424
-(defconst proof-toolbar-entries-default73,2561
-(defpgcustom toolbar-entries 107,4474
-(defpgcustom prog-args 125,5194
-(defpgcustom prog-env 138,5769
-(defpgcustom favourites 147,6195
-(defpgcustom menu-entries 152,6384
-(defpgcustom help-menu-entries 159,6620
-(defpgcustom keymap 166,6883
-(defpgcustom completion-table 171,7055
-(defpgcustom tags-program 182,7429
+(defpgcustom unicode-tokens2-enable 59,2070
+(defpgcustom mmm-enable 65,2248
+(defpgcustom script-indent 74,2602
+(defconst proof-toolbar-entries-default79,2739
+(defpgcustom toolbar-entries 113,4652
+(defpgcustom prog-args 131,5372
+(defpgcustom prog-env 144,5947
+(defpgcustom favourites 153,6373
+(defpgcustom menu-entries 158,6562
+(defpgcustom help-menu-entries 165,6798
+(defpgcustom keymap 172,7061
+(defpgcustom completion-table 177,7233
+(defpgcustom tags-program 188,7607
+(defpgcustom use-holes 197,7991
 
 generic/pg-goals.el,363
 (define-derived-mode proof-goals-mode 30,632
-(define-key proof-goals-mode-map 61,1622
-(defun proof-goals-config-done 91,3090
-(defun pg-goals-display 101,3378
-(defun pg-goals-yank-subterm 167,5815
-(defun pg-goals-button-action 194,6715
-(defun proof-expand-path 215,7687
-(defun pg-goals-construct-command 224,7929
-(defun pg-goals-get-subterm-help 256,9117
+(define-key proof-goals-mode-map 61,1623
+(defun proof-goals-config-done 91,3091
+(defun pg-goals-display 101,3379
+(defun pg-goals-yank-subterm 167,5816
+(defun pg-goals-button-action 194,6716
+(defun proof-expand-path 215,7688
+(defun pg-goals-construct-command 224,7930
+(defun pg-goals-get-subterm-help 256,9118
 
 generic/pg-pbrpm.el,1803
 (defvar pg-pbrpm-use-buffer-menu 22,547
@@ -1351,31 +1368,31 @@ generic/pg-pgip.el,2889
 generic/pg-response.el,1182
 (deflocal pg-response-eagerly-raise 31,730
 (define-derived-mode proof-response-mode 41,955
-(defun proof-response-config-done 67,2079
-(defvar pg-response-special-display-regexp 88,2854
-(defconst proof-multiframe-specifiers96,3260
-(defun proof-map-multiple-frame-specifiers 105,3617
-(defconst proof-multiframe-parameters116,4139
-(defun proof-multiple-frames-enable 125,4438
-(defun proof-three-window-enable 143,5082
-(defun proof-select-three-b 147,5146
-(defun proof-display-three-b 162,5615
-(defvar pg-frame-configuration 176,6107
-(defun pg-cache-frame-configuration 180,6254
-(defun proof-layout-windows 184,6425
-(defun proof-delete-other-frames 225,8248
-(defvar pg-response-erase-flag 256,9338
-(defun pg-response-maybe-erase260,9467
-(defun pg-response-display 291,10652
-(defun pg-response-display-with-face 310,11500
-(defun pg-response-clear-displays 346,12730
-(defun proof-next-error 365,13317
-(defun pg-response-has-error-location 446,16233
-(defvar proof-trace-last-fontify-pos 469,17066
-(defun proof-trace-fontify-pos 471,17109
-(defun proof-trace-buffer-display 479,17422
-(defun proof-trace-buffer-finish 503,18394
-(defun pg-thms-buffer-clear 524,18974
+(defun proof-response-config-done 67,2080
+(defvar pg-response-special-display-regexp 88,2855
+(defconst proof-multiframe-specifiers96,3261
+(defun proof-map-multiple-frame-specifiers 105,3618
+(defconst proof-multiframe-parameters116,4140
+(defun proof-multiple-frames-enable 125,4439
+(defun proof-three-window-enable 143,5083
+(defun proof-select-three-b 147,5147
+(defun proof-display-three-b 162,5616
+(defvar pg-frame-configuration 176,6108
+(defun pg-cache-frame-configuration 180,6255
+(defun proof-layout-windows 184,6426
+(defun proof-delete-other-frames 225,8249
+(defvar pg-response-erase-flag 256,9339
+(defun pg-response-maybe-erase260,9468
+(defun pg-response-display 291,10653
+(defun pg-response-display-with-face 310,11501
+(defun pg-response-clear-displays 346,12731
+(defun proof-next-error 365,13318
+(defun pg-response-has-error-location 446,16234
+(defvar proof-trace-last-fontify-pos 469,17067
+(defun proof-trace-fontify-pos 471,17110
+(defun proof-trace-buffer-display 479,17423
+(defun proof-trace-buffer-finish 503,18395
+(defun pg-thms-buffer-clear 524,18975
 
 generic/pg-thymodes.el,152
 (defmacro pg-defthymode 23,499
@@ -1717,40 +1734,40 @@ generic/proof-config.el,11009
 (defcustom proof-shell-strip-crs-from-input 2134,81851
 (defcustom proof-shell-strip-crs-from-output 2146,82336
 (defcustom proof-shell-insert-hook 2154,82704
-(defcustom proof-shell-handle-delayed-output-hook2194,84661
-(defcustom proof-shell-handle-error-or-interrupt-hook2200,84876
-(defcustom proof-shell-pre-interrupt-hook2218,85625
-(defcustom proof-shell-process-output-system-specific 2226,85897
-(defcustom proof-state-change-hook 2245,86761
-(defcustom proof-shell-font-lock-keywords 2256,87143
-(defcustom proof-shell-syntax-table-entries 2264,87475
-(defgroup proof-goals 2282,87847
-(defcustom pg-subterm-first-special-char 2287,87968
-(defcustom pg-subterm-anns-use-stack 2295,88280
-(defcustom pg-goals-change-goal 2304,88579
-(defcustom pbp-goal-command 2309,88695
-(defcustom pbp-hyp-command 2314,88851
-(defcustom pg-subterm-help-cmd 2319,89013
-(defcustom pg-goals-error-regexp 2326,89249
-(defcustom proof-shell-result-start 2331,89409
-(defcustom proof-shell-result-end 2337,89643
-(defcustom pg-subterm-start-char 2343,89856
-(defcustom pg-subterm-sep-char 2357,90436
-(defcustom pg-subterm-end-char 2363,90615
-(defcustom pg-topterm-regexp 2369,90772
-(defcustom proof-goals-font-lock-keywords 2386,91374
-(defcustom proof-resp-font-lock-keywords 2400,92059
-(defcustom pg-before-fontify-output-hook 2412,92639
-(defcustom pg-after-fontify-output-hook 2420,92999
-(defgroup proof-x-symbol 2432,93279
-(defcustom proof-xsym-extra-modes 2437,93407
-(defcustom proof-xsym-font-lock-keywords 2450,94035
-(defcustom proof-xsym-activate-command 2458,94412
-(defcustom proof-xsym-deactivate-command 2465,94647
-(defcustom proof-general-name 2482,94932
-(defcustom proof-general-home-page2487,95089
-(defcustom proof-unnamed-theorem-name2493,95249
-(defcustom proof-universal-keys2499,95433
+(defcustom proof-shell-handle-delayed-output-hook2194,84663
+(defcustom proof-shell-handle-error-or-interrupt-hook2200,84878
+(defcustom proof-shell-pre-interrupt-hook2218,85627
+(defcustom proof-shell-process-output-system-specific 2226,85899
+(defcustom proof-state-change-hook 2245,86763
+(defcustom proof-shell-font-lock-keywords 2256,87145
+(defcustom proof-shell-syntax-table-entries 2264,87477
+(defgroup proof-goals 2282,87849
+(defcustom pg-subterm-first-special-char 2287,87970
+(defcustom pg-subterm-anns-use-stack 2295,88282
+(defcustom pg-goals-change-goal 2304,88581
+(defcustom pbp-goal-command 2309,88697
+(defcustom pbp-hyp-command 2314,88853
+(defcustom pg-subterm-help-cmd 2319,89015
+(defcustom pg-goals-error-regexp 2326,89251
+(defcustom proof-shell-result-start 2331,89411
+(defcustom proof-shell-result-end 2337,89645
+(defcustom pg-subterm-start-char 2343,89858
+(defcustom pg-subterm-sep-char 2357,90438
+(defcustom pg-subterm-end-char 2363,90617
+(defcustom pg-topterm-regexp 2369,90774
+(defcustom proof-goals-font-lock-keywords 2386,91376
+(defcustom proof-resp-font-lock-keywords 2400,92061
+(defcustom pg-before-fontify-output-hook 2412,92641
+(defcustom pg-after-fontify-output-hook 2420,93001
+(defgroup proof-x-symbol 2432,93281
+(defcustom proof-xsym-extra-modes 2437,93409
+(defcustom proof-xsym-font-lock-keywords 2450,94037
+(defcustom proof-xsym-activate-command 2458,94414
+(defcustom proof-xsym-deactivate-command 2465,94649
+(defcustom proof-general-name 2482,94934
+(defcustom proof-general-home-page2487,95091
+(defcustom proof-unnamed-theorem-name2493,95251
+(defcustom proof-universal-keys2499,95435
 
 generic/proof-depends.el,824
 (defvar proof-thm-names-of-files 23,624
@@ -1802,45 +1819,45 @@ generic/proof-menu.el,2101
 (defvar proof-help-menu208,7639
 (defvar proof-show-hide-menu216,7917
 (defvar proof-buffer-menu225,8230
-(defun proof-keep-response-history 286,10398
-(defconst proof-quick-opts-menu294,10708
-(defun proof-quick-opts-vars 437,16385
-(defun proof-quick-opts-changed-from-defaults-p 463,17177
-(defun proof-quick-opts-changed-from-saved-p 467,17282
-(defun proof-quick-opts-save 478,17634
-(defun proof-quick-opts-reset 483,17802
-(defconst proof-config-menu495,18070
-(defconst proof-advanced-menu502,18249
-(defvar proof-menu 515,18684
-(defun proof-main-menu 524,18968
-(defun proof-aux-menu 535,19234
-(defun proof-menu-define-favourites-menu 551,19581
-(defun proof-def-favourite 571,20237
-(defvar proof-make-favourite-cmd-history 594,21212
-(defvar proof-make-favourite-menu-history 597,21297
-(defun proof-save-favourites 600,21383
-(defun proof-del-favourite 605,21531
-(defun proof-read-favourite 622,22092
-(defun proof-add-favourite 647,22895
-(defvar proof-menu-settings 674,23946
-(defun proof-menu-define-settings-menu 677,24020
-(defun proof-menu-entry-name 697,24764
-(defun proof-menu-entry-for-setting 709,25236
-(defun proof-settings-vars 727,25726
-(defun proof-settings-changed-from-defaults-p 732,25903
-(defun proof-settings-changed-from-saved-p 736,26009
-(defun proof-settings-save 740,26112
-(defun proof-settings-reset 745,26279
-(defun proof-defpacustom-fn 752,26524
-(defmacro defpacustom 828,29408
-(defun proof-assistant-invisible-command-ifposs 843,30235
-(defun proof-maybe-askprefs 865,31210
-(defun proof-assistant-settings-cmd 872,31414
-(defvar proof-assistant-format-table 889,32074
-(defun proof-assistant-format-bool 897,32443
-(defun proof-assistant-format-int 900,32556
-(defun proof-assistant-format-string 903,32648
-(defun proof-assistant-format 906,32746
+(defun proof-keep-response-history 288,10496
+(defconst proof-quick-opts-menu296,10806
+(defun proof-quick-opts-vars 449,16899
+(defun proof-quick-opts-changed-from-defaults-p 475,17691
+(defun proof-quick-opts-changed-from-saved-p 479,17796
+(defun proof-quick-opts-save 490,18148
+(defun proof-quick-opts-reset 495,18316
+(defconst proof-config-menu507,18584
+(defconst proof-advanced-menu514,18763
+(defvar proof-menu 527,19198
+(defun proof-main-menu 536,19482
+(defun proof-aux-menu 547,19748
+(defun proof-menu-define-favourites-menu 563,20095
+(defun proof-def-favourite 583,20751
+(defvar proof-make-favourite-cmd-history 606,21726
+(defvar proof-make-favourite-menu-history 609,21811
+(defun proof-save-favourites 612,21897
+(defun proof-del-favourite 617,22045
+(defun proof-read-favourite 634,22606
+(defun proof-add-favourite 659,23409
+(defvar proof-menu-settings 686,24460
+(defun proof-menu-define-settings-menu 689,24534
+(defun proof-menu-entry-name 709,25278
+(defun proof-menu-entry-for-setting 721,25750
+(defun proof-settings-vars 739,26240
+(defun proof-settings-changed-from-defaults-p 744,26417
+(defun proof-settings-changed-from-saved-p 748,26523
+(defun proof-settings-save 752,26626
+(defun proof-settings-reset 757,26793
+(defun proof-defpacustom-fn 764,27038
+(defmacro defpacustom 840,29922
+(defun proof-assistant-invisible-command-ifposs 855,30749
+(defun proof-maybe-askprefs 877,31724
+(defun proof-assistant-settings-cmd 884,31928
+(defvar proof-assistant-format-table 901,32588
+(defun proof-assistant-format-bool 909,32957
+(defun proof-assistant-format-int 912,33070
+(defun proof-assistant-format-string 915,33162
+(defun proof-assistant-format 918,33260
 
 generic/proof-mmm.el,70
 (defun proof-mmm-set-global 41,1516
@@ -1923,42 +1940,42 @@ generic/proof-script.el,5112
 (defun proof-done-advancing-autosave 1515,59345
 (defun proof-done-advancing-other 1580,61891
 (defun proof-segment-up-to-parser 1608,62850
-(defun proof-script-generic-parse-find-comment-end 1671,64940
-(defun proof-script-generic-parse-cmdend 1680,65356
-(defun proof-script-generic-parse-cmdstart 1705,66251
-(defun proof-script-generic-parse-sexp 1768,68959
-(defun proof-cmdstart-add-segment-for-cmd 1792,69895
-(defun proof-segment-up-to-cmdstart 1844,72108
-(defun proof-segment-up-to-cmdend 1905,74468
-(defun proof-semis-to-vanillas 1977,77147
-(defun proof-script-new-command-advance 2016,78473
-(defun proof-script-next-command-advance 2058,80214
-(defun proof-assert-until-point-interactive 2070,80655
-(defun proof-assert-until-point 2096,81777
-(defun proof-assert-next-command2149,84209
-(defun proof-goto-point 2197,86472
-(defun proof-insert-pbp-command 2215,87013
-(defun proof-insert-sendback-command 2229,87482
-(defun proof-done-retracting 2255,88372
-(defun proof-setup-retract-action 2291,89858
-(defun proof-last-goal-or-goalsave 2301,90341
-(defun proof-retract-target 2324,91181
-(defun proof-retract-until-point-interactive 2409,94822
-(defun proof-retract-until-point 2417,95207
-(define-derived-mode proof-mode 2460,96956
-(defun proof-script-set-visited-file-name 2510,98883
-(defun proof-script-set-buffer-hooks 2534,99885
-(defun proof-script-kill-buffer-fn 2542,100303
-(defun proof-config-done-related 2586,102125
-(defun proof-generic-goal-command-p 2656,104603
-(defun proof-generic-state-preserving-p 2661,104815
-(defun proof-generic-count-undos 2670,105332
-(defun proof-generic-find-and-forget 2699,106362
-(defconst proof-script-important-settings2750,108187
-(defun proof-config-done 2765,108740
-(defun proof-setup-parsing-mechanism 2853,111858
-(defun proof-setup-imenu 2897,113711
-(defun proof-setup-func-menu 2914,114316
+(defun proof-script-generic-parse-find-comment-end 1671,64926
+(defun proof-script-generic-parse-cmdend 1680,65342
+(defun proof-script-generic-parse-cmdstart 1705,66237
+(defun proof-script-generic-parse-sexp 1768,68945
+(defun proof-cmdstart-add-segment-for-cmd 1792,69881
+(defun proof-segment-up-to-cmdstart 1844,72080
+(defun proof-segment-up-to-cmdend 1905,74440
+(defun proof-semis-to-vanillas 1977,77105
+(defun proof-script-new-command-advance 2016,78431
+(defun proof-script-next-command-advance 2058,80172
+(defun proof-assert-until-point-interactive 2070,80613
+(defun proof-assert-until-point 2096,81735
+(defun proof-assert-next-command2149,84167
+(defun proof-goto-point 2197,86430
+(defun proof-insert-pbp-command 2215,86971
+(defun proof-insert-sendback-command 2229,87440
+(defun proof-done-retracting 2255,88330
+(defun proof-setup-retract-action 2291,89816
+(defun proof-last-goal-or-goalsave 2301,90299
+(defun proof-retract-target 2324,91139
+(defun proof-retract-until-point-interactive 2409,94780
+(defun proof-retract-until-point 2417,95165
+(define-derived-mode proof-mode 2460,96914
+(defun proof-script-set-visited-file-name 2510,98841
+(defun proof-script-set-buffer-hooks 2534,99843
+(defun proof-script-kill-buffer-fn 2542,100261
+(defun proof-config-done-related 2586,102083
+(defun proof-generic-goal-command-p 2656,104561
+(defun proof-generic-state-preserving-p 2661,104773
+(defun proof-generic-count-undos 2670,105290
+(defun proof-generic-find-and-forget 2699,106320
+(defconst proof-script-important-settings2750,108145
+(defun proof-config-done 2765,108698
+(defun proof-setup-parsing-mechanism 2853,111816
+(defun proof-setup-imenu 2897,113669
+(defun proof-setup-func-menu 2914,114274
 
 generic/proof-shell.el,3314
 (defvar proof-marker 28,649
@@ -2015,38 +2032,38 @@ generic/proof-shell.el,3314
 (defvar proof-shell-minibuffer-urgent-interactive-input-history 1322,50188
 (defun proof-shell-minibuffer-urgent-interactive-input 1324,50258
 (defun proof-shell-process-urgent-messages 1334,50617
-(defun proof-shell-filter 1408,53716
-(defun proof-shell-filter-process-output 1569,60349
-(defvar pg-last-tracing-output-time 1622,62403
-(defconst pg-slow-mode-duration 1625,62509
-(defconst pg-fast-tracing-mode-threshold 1628,62591
-(defvar pg-tracing-cleanup-timer 1631,62719
-(defun pg-tracing-tight-loop 1633,62758
-(defun pg-finish-tracing-display 1676,64476
-(defun proof-shell-dont-show-annotations 1689,64782
-(defun proof-shell-show-annotations 1705,65303
-(defun proof-shell-wait 1727,65830
-(defun proof-done-invisible 1746,66739
-(defun proof-shell-invisible-command 1752,66911
-(defun proof-shell-invisible-cmd-get-result 1786,68176
-(defun proof-shell-invisible-command-invisible-result 1804,68872
-(define-derived-mode proof-shell-mode 1823,69302
-(defconst proof-shell-important-settings1893,71968
-(defun proof-shell-config-done 1899,72083
+(defun proof-shell-filter 1408,53721
+(defun proof-shell-filter-process-output 1569,60354
+(defvar pg-last-tracing-output-time 1622,62408
+(defconst pg-slow-mode-duration 1625,62514
+(defconst pg-fast-tracing-mode-threshold 1628,62596
+(defvar pg-tracing-cleanup-timer 1631,62724
+(defun pg-tracing-tight-loop 1633,62763
+(defun pg-finish-tracing-display 1676,64481
+(defun proof-shell-dont-show-annotations 1689,64787
+(defun proof-shell-show-annotations 1705,65308
+(defun proof-shell-wait 1727,65835
+(defun proof-done-invisible 1746,66744
+(defun proof-shell-invisible-command 1752,66916
+(defun proof-shell-invisible-cmd-get-result 1786,68181
+(defun proof-shell-invisible-command-invisible-result 1804,68877
+(define-derived-mode proof-shell-mode 1823,69307
+(defconst proof-shell-important-settings1893,71973
+(defun proof-shell-config-done 1899,72088
 
 generic/proof-site.el,504
-(defconst proof-assistant-table-default23,727
-(defconst proof-general-short-version 61,2145
-(defconst proof-general-version-year 67,2333
-(defgroup proof-general 74,2486
-(defgroup proof-general-internals 79,2594
-(defun proof-home-directory-fn 92,2982
-(defcustom proof-home-directory103,3353
-(defcustom proof-images-directory112,3720
-(defcustom proof-info-directory118,3922
-(defcustom proof-assistant-table145,5068
-(defcustom proof-assistants 180,6184
-(defun proof-ready-for-assistant 208,7329
+(defconst proof-assistant-table-default23,728
+(defconst proof-general-short-version 61,2146
+(defconst proof-general-version-year 67,2334
+(defgroup proof-general 74,2487
+(defgroup proof-general-internals 79,2595
+(defun proof-home-directory-fn 92,2983
+(defcustom proof-home-directory103,3354
+(defcustom proof-images-directory112,3721
+(defcustom proof-info-directory118,3923
+(defcustom proof-assistant-table145,5069
+(defcustom proof-assistants 180,6185
+(defun proof-ready-for-assistant 208,7330
 
 generic/proof-splash.el,726
 (defcustom proof-splash-enable 17,319
@@ -2106,52 +2123,64 @@ generic/proof-toolbar.el,2874
 (deflocal proof-toolbar-itimer 119,3909
 (defun proof-toolbar-setup 123,4019
 (defun proof-toolbar-build 166,5562
-(defalias 'proof-toolbar-enable proof-toolbar-enable
231,7760
-(defun proof-toolbar-setup-refresh 242,8064
-(defun proof-toolbar-disable-refresh 263,8885
-(deflocal proof-toolbar-refresh-flag 271,9275
-(defun proof-toolbar-refresh 277,9546
-(defvar proof-toolbar-enablers281,9691
-(defvar proof-toolbar-enablers-last-state287,9867
-(defun proof-toolbar-really-refresh 291,9958
-(defun proof-toolbar-undo-enable-p 346,11852
-(defalias 'proof-toolbar-undo proof-toolbar-undo
351,12000
-(defun proof-toolbar-delete-enable-p 357,12119
-(defalias 'proof-toolbar-delete proof-toolbar-delete
363,12293
-(defun proof-toolbar-lockedend-enable-p 370,12429
-(defalias 'proof-toolbar-lockedend proof-toolbar-lockedend
373,12479
-(defun proof-toolbar-next-enable-p 382,12567
-(defalias 'proof-toolbar-next proof-toolbar-next
386,12674
-(defun proof-toolbar-goto-enable-p 393,12768
-(defalias 'proof-toolbar-goto proof-toolbar-goto
396,12841
-(defun proof-toolbar-retract-enable-p 403,12917
-(defalias 'proof-toolbar-retract proof-toolbar-retract
407,13028
-(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p
414,13107
-(defalias 'proof-toolbar-use proof-toolbar-use
415,13175
-(defun proof-toolbar-restart-enable-p 421,13253
-(defalias 'proof-toolbar-restart proof-toolbar-restart
426,13414
-(defun proof-toolbar-goal-enable-p 432,13492
-(defalias 'proof-toolbar-goal proof-toolbar-goal
439,13725
-(defun proof-toolbar-qed-enable-p 446,13797
-(defalias 'proof-toolbar-qed proof-toolbar-qed
452,13949
-(defun proof-toolbar-state-enable-p 458,14021
-(defalias 'proof-toolbar-state proof-toolbar-state
461,14092
-(defun proof-toolbar-context-enable-p 467,14161
-(defalias 'proof-toolbar-context proof-toolbar-context
470,14234
-(defun proof-toolbar-info-enable-p 478,14394
-(defalias 'proof-toolbar-info proof-toolbar-info
481,14438
-(defun proof-toolbar-command-enable-p 487,14507
-(defalias 'proof-toolbar-command proof-toolbar-command
490,14578
-(defun proof-toolbar-help-enable-p 496,14658
-(defun proof-toolbar-help 499,14703
-(defun proof-toolbar-find-enable-p 507,14797
-(defalias 'proof-toolbar-find proof-toolbar-find
510,14866
-(defun proof-toolbar-visibility-enable-p 516,14964
-(defalias 'proof-toolbar-visibility proof-toolbar-visibility
519,15064
-(defun proof-toolbar-interrupt-enable-p 525,15152
-(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt
528,15216
-(defun proof-toolbar-make-menu-item 537,15405
-(defun proof-toolbar-scripting-menu 560,16105
+(defalias 'proof-toolbar-enable proof-toolbar-enable
230,7673
+(defun proof-toolbar-setup-refresh 241,7977
+(defun proof-toolbar-disable-refresh 262,8798
+(deflocal proof-toolbar-refresh-flag 270,9188
+(defun proof-toolbar-refresh 276,9459
+(defvar proof-toolbar-enablers280,9604
+(defvar proof-toolbar-enablers-last-state286,9780
+(defun proof-toolbar-really-refresh 290,9871
+(defun proof-toolbar-undo-enable-p 345,11765
+(defalias 'proof-toolbar-undo proof-toolbar-undo
350,11913
+(defun proof-toolbar-delete-enable-p 356,12032
+(defalias 'proof-toolbar-delete proof-toolbar-delete
362,12206
+(defun proof-toolbar-lockedend-enable-p 369,12342
+(defalias 'proof-toolbar-lockedend proof-toolbar-lockedend
372,12392
+(defun proof-toolbar-next-enable-p 381,12480
+(defalias 'proof-toolbar-next proof-toolbar-next
385,12587
+(defun proof-toolbar-goto-enable-p 392,12681
+(defalias 'proof-toolbar-goto proof-toolbar-goto
395,12754
+(defun proof-toolbar-retract-enable-p 402,12830
+(defalias 'proof-toolbar-retract proof-toolbar-retract
406,12941
+(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p
413,13020
+(defalias 'proof-toolbar-use proof-toolbar-use
414,13088
+(defun proof-toolbar-restart-enable-p 420,13166
+(defalias 'proof-toolbar-restart proof-toolbar-restart
425,13327
+(defun proof-toolbar-goal-enable-p 431,13405
+(defalias 'proof-toolbar-goal proof-toolbar-goal
438,13638
+(defun proof-toolbar-qed-enable-p 445,13710
+(defalias 'proof-toolbar-qed proof-toolbar-qed
451,13862
+(defun proof-toolbar-state-enable-p 457,13934
+(defalias 'proof-toolbar-state proof-toolbar-state
460,14005
+(defun proof-toolbar-context-enable-p 466,14074
+(defalias 'proof-toolbar-context proof-toolbar-context
469,14147
+(defun proof-toolbar-info-enable-p 477,14307
+(defalias 'proof-toolbar-info proof-toolbar-info
480,14351
+(defun proof-toolbar-command-enable-p 486,14420
+(defalias 'proof-toolbar-command proof-toolbar-command
489,14491
+(defun proof-toolbar-help-enable-p 495,14571
+(defun proof-toolbar-help 498,14616
+(defun proof-toolbar-find-enable-p 506,14710
+(defalias 'proof-toolbar-find proof-toolbar-find
509,14779
+(defun proof-toolbar-visibility-enable-p 515,14877
+(defalias 'proof-toolbar-visibility proof-toolbar-visibility
518,14977
+(defun proof-toolbar-interrupt-enable-p 524,15065
+(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt
527,15129
+(defun proof-toolbar-make-menu-item 536,15318
+(defun proof-toolbar-scripting-menu 559,16018
+
+generic/proof-unicode-tokens2.el,484
+(defvar proof-unicode-tokens2-initialised 17,499
+(defun proof-unicode-tokens2-init 20,607
+(defun proof-unicode-tokens2-enable 43,1239
+(defun proof-unicode-tokens2-set-global 57,1867
+(defun proof-token-name-alist 76,2535
+(defun proof-shortcut-alist 91,3194
+(defun proof-unicode-tokens2-activate-prover 103,3534
+(defun proof-unicode-tokens2-deactivate-prover 110,3778
+(defun proof-unicode-tokens2-shell-config 121,4211
+(defun proof-unicode-tokens2-encode-shell-input 131,4615
 
 generic/proof-unicode-tokens.el,476
 (defvar proof-unicode-tokens-initialised 17,496
@@ -2466,58 +2495,105 @@ lib/texi-docstring-magic.el,584
 
 lib/unicode-chars.el,80
 (defvar unicode-chars-alist12,348
-(defun unicode-chars-list-chars 5051,245961
-
-lib/unicode-tokens.el,2472
-(defvar unicode-tokens-charref-format 58,2190
-(defvar unicode-tokens-token-format 61,2287
-(defvar unicode-tokens-token-name-alist 64,2378
-(defvar unicode-tokens-glyph-list 67,2471
-(defvar unicode-tokens-token-prefix 71,2615
-(defvar unicode-tokens-token-suffix 74,2699
-(defvar unicode-tokens-control-token-match 77,2781
-(defvar unicode-tokens-token-match 80,2857
-(defvar unicode-tokens-hexcode-match 83,2940
-(defvar unicode-tokens-next-character-regexp 86,3048
-(defvar unicode-tokens-shortcut-alist89,3193
-(defface unicode-tokens-script-font-face105,3645
-(defface unicode-tokens-fraktur-font-face115,3910
-(defface unicode-tokens-serif-font-face125,4204
-(defvar unicode-tokens-max-token-length 140,4531
-(defvar unicode-tokens-codept-charname-alist 143,4630
-(defvar unicode-tokens-token-alist 146,4738
-(defvar unicode-tokens-ustring-alist 150,4899
-(defun unicode-tokens-insert-char 158,5002
-(defun unicode-tokens-insert-string 168,5423
-(defun unicode-tokens-character-insert 178,5800
-(defun unicode-tokens-token-insert 200,6708
-(defun unicode-tokens-replace-token-after 221,7605
-(defun unicode-tokens-looking-backward-at 243,8370
-(defun unicode-tokens-electric-suffix 257,9003
-(defvar unicode-tokens-rotate-glyph-last-char 304,10607
-(defun unicode-tokens-rotate-glyph-forward 306,10659
-(defun unicode-tokens-rotate-glyph-backward 335,11841
-(defun unicode-tokens-map-ordering 356,12448
-(defun unicode-tokens-propertise-after-quail 360,12598
-(defun unicode-tokens-quail-define-rules 365,12753
-(defvar unicode-tokens-format-entry429,15083
-(defconst unicode-tokens-ignored-properties439,15381
-(defconst unicode-tokens-annotation-translations445,15590
-(defun unicode-tokens-remove-properties 463,16134
-(defun unicode-tokens-tokens-to-unicode 471,16452
-(defvar unicode-tokens-next-control-token-seen-token 492,17301
-(defun unicode-tokens-next-control-token 495,17419
-(defconst unicode-tokens-annotation-control-token-alist 546,19379
-(defun unicode-tokens-make-token-annotation 559,19857
-(defun unicode-tokens-find-property 570,20295
-(defun unicode-tokens-annotate-region 584,20684
-(defun unicode-tokens-annotate-string 596,21092
-(defun unicode-tokens-unicode-to-tokens 602,21260
-(defun unicode-tokens-replace-strings-propertise 622,22047
-(defun unicode-tokens-replace-strings-unpropertise 652,23297
-(defvar unicode-tokens-mode-map 681,24042
-(define-minor-mode unicode-tokens-mode684,24139
-(defun unicode-tokens-initialise 720,25517
+(defun unicode-chars-list-chars 5050,245960
+
+lib/unicode-tokens2.el,2266
+(defvar unicode-tokens2-charref-format 62,2327
+(defvar unicode-tokens2-token-format 65,2425
+(defvar unicode-tokens2-token-name-alist 68,2517
+(defvar unicode-tokens2-glyph-list 71,2611
+(defvar unicode-tokens2-token-prefix 75,2756
+(defvar unicode-tokens2-token-suffix 78,2841
+(defvar unicode-tokens2-control-token-match 81,2924
+(defvar unicode-tokens2-token-match 84,3001
+(defvar unicode-tokens2-hexcode-match 87,3085
+(defvar unicode-tokens2-next-character-regexp 90,3194
+(defvar unicode-tokens2-shortcut-alist93,3340
+(defface unicode-tokens2-script-font-face109,3794
+(defface unicode-tokens2-fraktur-font-face119,4060
+(defface unicode-tokens2-serif-font-face129,4355
+(defvar unicode-tokens2-max-token-length 144,4684
+(defvar unicode-tokens2-codept-charname-alist 147,4784
+(defvar unicode-tokens2-token-alist 150,4893
+(defvar unicode-tokens2-ustring-alist 154,5056
+(defun unicode-tokens2-insert-char 162,5160
+(defun unicode-tokens2-insert-string 172,5584
+(defun unicode-tokens2-character-insert 182,5964
+(defun unicode-tokens2-token-insert 204,6875
+(defun unicode-tokens2-replace-token-after 225,7778
+(defun unicode-tokens2-looking-backward-at 247,8547
+(defun unicode-tokens2-electric-suffix 261,9181
+(defvar unicode-tokens2-rotate-glyph-last-char 308,10801
+(defun unicode-tokens2-rotate-glyph-forward 310,10854
+(defun unicode-tokens2-rotate-glyph-backward 339,12043
+(defconst unicode-tokens2-ignored-properties348,12388
+(defconst unicode-tokens2-annotation-translations354,12598
+(defun unicode-tokens2-font-lock-keywords 372,13146
+(defvar unicode-tokens2-next-control-token-seen-token 399,14033
+(defun unicode-tokens2-next-control-token 402,14152
+(defconst unicode-tokens2-annotation-control-token-alist 453,16123
+(defun unicode-tokens2-make-token-annotation 466,16602
+(defun unicode-tokens2-find-property 477,17044
+(defun unicode-tokens2-annotate-region 491,17435
+(defun unicode-tokens2-annotate-string 503,17847
+(defun unicode-tokens2-unicode-to-tokens 509,18017
+(defun unicode-tokens2-replace-strings-propertise 529,18810
+(defun unicode-tokens2-replace-strings-unpropertise 559,20061
+(defvar unicode-tokens2-mode-map 588,20808
+(define-minor-mode unicode-tokens2-mode591,20906
+(defun unicode-tokens2-initialise 627,22293
+
+lib/unicode-tokens.el,2526
+(defvar unicode-tokens-charref-format 60,2307
+(defvar unicode-tokens-token-format 63,2404
+(defvar unicode-tokens-token-name-alist 66,2495
+(defvar unicode-tokens-glyph-list 69,2588
+(defvar unicode-tokens-token-prefix 73,2732
+(defvar unicode-tokens-token-suffix 76,2816
+(defvar unicode-tokens-control-token-match 79,2898
+(defvar unicode-tokens-token-match 82,2974
+(defvar unicode-tokens-hexcode-match 85,3057
+(defvar unicode-tokens-next-character-regexp 88,3165
+(defvar unicode-tokens-shortcut-alist91,3310
+(defface unicode-tokens-script-font-face107,3762
+(defface unicode-tokens-fraktur-font-face117,4027
+(defface unicode-tokens-serif-font-face127,4321
+(defvar unicode-tokens-max-token-length 142,4648
+(defvar unicode-tokens-codept-charname-alist 145,4747
+(defvar unicode-tokens-token-alist 148,4855
+(defvar unicode-tokens-ustring-alist 152,5016
+(defun unicode-tokens-insert-char 160,5119
+(defun unicode-tokens-insert-string 170,5540
+(defun unicode-tokens-character-insert 180,5917
+(defun unicode-tokens-token-insert 202,6825
+(defun unicode-tokens-replace-token-after 223,7722
+(defun unicode-tokens-looking-backward-at 245,8487
+(defun unicode-tokens-electric-suffix 259,9120
+(defvar unicode-tokens-rotate-glyph-last-char 306,10724
+(defun unicode-tokens-rotate-glyph-forward 308,10776
+(defun unicode-tokens-rotate-glyph-backward 337,11958
+(defun unicode-tokens-map-ordering 358,12565
+(defun unicode-tokens-propertise-after-quail 362,12715
+(defun unicode-tokens-quail-define-rules 367,12870
+(defvar unicode-tokens-format-entry431,15200
+(defconst unicode-tokens-ignored-properties441,15498
+(defconst unicode-tokens-annotation-translations449,15752
+(defun unicode-tokens-remove-properties 474,16731
+(defun unicode-tokens-tokens-to-unicode 482,17049
+(defvar unicode-tokens-next-control-token-seen-token 503,17898
+(defun unicode-tokens-next-control-token 506,18016
+(defconst unicode-tokens-annotation-control-token-alist 560,20100
+(defun unicode-tokens-make-token-annotation 575,20644
+(defun unicode-tokens-find-property 586,21082
+(defun unicode-tokens-annotate-region 600,21471
+(defun unicode-tokens-annotate-region-with 612,21879
+(defun unicode-tokens-annotate-string 617,22030
+(defun unicode-tokens-unicode-to-tokens 623,22198
+(defun unicode-tokens-replace-strings-propertise 643,22985
+(defun unicode-tokens-replace-strings-unpropertise 673,24235
+(defvar unicode-tokens-mode-map 702,24980
+(define-minor-mode unicode-tokens-mode705,25077
+(defun unicode-tokens-initialise 741,26455
 
 lib/xml-fixed.el,528
 (defsubst xml-node-name 82,2904
@@ -3379,7 +3455,7 @@ x-symbol/lisp/x-symbol-unicode.el,169
 x-symbol/lisp/x-symbol-unicode-extras.el,40
 (defconst x-symol-unicode-extras13,263
 
-x-symbol/lisp/x-symbol-vars.el,8058
+x-symbol/lisp/x-symbol-vars.el,8115
 (defconst x-symbol-version 40,1516
 (defgroup x-symbol 49,1858
 (defgroup x-symbol-mode 56,2069
@@ -3524,28 +3600,29 @@ x-symbol/lisp/x-symbol-vars.el,8058
 (defvar x-symbol-latin5-fonts1654,65654
 (defvar x-symbol-latin9-fonts1661,65961
 (defvar x-symbol-xsymb0-fonts1666,66159
-(defvar x-symbol-xsymb1-fonts1672,66450
-(defcustom x-symbol-image-max-width 1683,66913
-(defcustom x-symbol-image-max-height 1688,67035
-(defcustom x-symbol-image-update-cache 1693,67158
-(defcustom x-symbol-image-use-remote 1709,67929
-(defcustom x-symbol-image-current-marker 1734,69128
-(defcustom x-symbol-image-scale-method 1742,69475
-(defcustom x-symbol-image-explicitly-relative-regexp 1756,70205
-(defcustom x-symbol-image-searchpath-follow-symlink 1761,70387
-(defcustom x-symbol-image-cache-directories1776,71082
-(defvar x-symbol-image-temp-name1825,73064
-(defcustom x-symbol-image-convert-mono-regexp1834,73481
-(defcustom x-symbol-image-help-echo1848,74169
-(defcustom x-symbol-image-editor-alist1860,74673
-(defvar x-symbol-image-menu1893,76029
-(defvar x-symbol-image-data-directory 1914,77032
-(defvar x-symbol-image-special-glyphs1918,77199
-(defcustom x-symbol-image-convert-file-alist1951,78897
-(defcustom x-symbol-image-convert-program1961,79365
-(defcustom x-symbol-image-converter1967,79592
-(defun x-symbol-variable-interactive 2074,84086
-(defcustom x-symbol-use-unicode 2093,84916
+(defvar x-symbol-xsymb1-fonts1672,66448
+(defcustom x-symbol-image-max-width 1683,66909
+(defcustom x-symbol-image-max-height 1688,67031
+(defcustom x-symbol-image-update-cache 1693,67154
+(defcustom x-symbol-image-use-remote 1709,67925
+(defcustom x-symbol-image-current-marker 1734,69124
+(defcustom x-symbol-image-scale-method 1742,69471
+(defcustom x-symbol-image-explicitly-relative-regexp 1756,70201
+(defcustom x-symbol-image-searchpath-follow-symlink 1761,70383
+(defcustom x-symbol-image-cache-directories1776,71078
+(defvar x-symbol-image-temp-name1825,73060
+(defcustom x-symbol-image-convert-mono-regexp1834,73477
+(defcustom x-symbol-image-help-echo1848,74165
+(defcustom x-symbol-image-editor-alist1860,74669
+(defvar x-symbol-image-menu1893,76025
+(defvar x-symbol-image-data-directory 1914,77028
+(defvar x-symbol-image-special-glyphs1918,77195
+(defcustom x-symbol-image-convert-file-alist1951,78893
+(defcustom x-symbol-image-convert-program1961,79361
+(defcustom x-symbol-image-converter-required 1967,79588
+(defcustom x-symbol-image-converter1972,79767
+(defun x-symbol-variable-interactive 2080,84357
+(defcustom x-symbol-use-unicode 2099,85187
 
 x-symbol/lisp/x-symbol-xmacs.el,522
 (defun x-symbol-paren-reset-mode 102,4657
@@ -3559,97 +3636,98 @@ x-symbol/lisp/x-symbol-xmacs.el,522
 (defun x-symbol-event-matches-key-specifier-p 163,7016
 (defun x-symbol-window-width 173,7418
 
-doc/ProofGeneral.texi,5509
-@node Top167,5089
-@node Preface204,6217
-@node Latest news for version 3.7Latest news for version 3.7
227,6813
-@node Future269,8735
-@node Credits300,10034
-@node Introducing Proof GeneralIntroducing Proof General
406,13803
-@node Installing Proof GeneralInstalling Proof General
462,15845
-@node Quick start guideQuick start guide
476,16294
-@node Features of Proof GeneralFeatures of Proof General
520,18415
-@node Supported proof assistantsSupported proof assistants
609,22352
-@node Prerequisites for this manualPrerequisites for this manual
658,24258
-@node Organization of this manualOrganization of this manual
702,25884
-@node Basic Script ManagementBasic Script Management
728,26712
-@node Walkthrough example in IsabelleWalkthrough example in Isabelle
747,27312
-@node Proof scriptsProof scripts
998,36965
-@node Script buffersScript buffers
1041,39085
-@node Locked queue and editing regionsLocked queue and editing regions
1063,39662
-@node Goal-save sequencesGoal-save sequences
1119,41809
-@node Active scripting bufferActive scripting buffer
1156,43295
-@node Summary of Proof General buffersSummary of Proof General buffers
1225,46715
-@node Script editing commandsScript editing commands
1287,49389
-@node Script processing commandsScript processing commands
1365,52248
-@node Proof assistant commandsProof assistant commands
1493,57549
-@node Toolbar commandsToolbar commands
1659,63328
-@node Interrupting during trace outputInterrupting during trace output
1683,64257
-@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
1722,66181
-@node Goals buffer commandsGoals buffer commands
1736,66681
-@node Advanced Script Management and EditingAdvanced Script Management and Editing
1825,70220
-@node Visibility of completed proofsVisibility of completed proofs
1857,71432
-@node Switching between proof scriptsSwitching between proof scripts
1912,73355
-@node View of processed files View of processed files 
1949,75327
-@node Retracting across filesRetracting across files
2009,78378
-@node Asserting across filesAsserting across files
2022,79009
-@node Automatic multiple file handlingAutomatic multiple file handling
2035,79575
-@node Escaping script managementEscaping script management
2060,80609
-@node Editing featuresEditing features
2118,82812
-@node Experimental featuresExperimental features
2182,85484
-@node Support for other PackagesSupport for other Packages
2216,86748
-@node Syntax highlightingSyntax highlighting
2249,87643
-@node X-Symbol supportX-Symbol support
2288,89264
-@node Unicode supportUnicode support
2346,91804
-@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)
2461,96601
-@node Support for outline modeSupport for outline mode
2520,98731
-@node Support for completionSupport for completion
2546,99861
-@node Support for tagsSupport for tags
2604,102037
-@node Customizing Proof GeneralCustomizing Proof General
2656,104366
-@node Basic optionsBasic options
2696,106036
-@node How to customizeHow to customize
2720,106794
-@node Display customizationDisplay customization
2771,108896
-@node User optionsUser options
2896,114134
-@node Changing facesChanging faces
3168,123833
-@node Tweaking configuration settingsTweaking configuration settings
3243,126502
-@node Hints and TipsHints and Tips
3300,129028
-@node Adding your own keybindingsAdding your own keybindings
3319,129629
-@node Using file variablesUsing file variables
3375,132162
-@node Using abbreviationsUsing abbreviations
3434,134348
-@node LEGO Proof GeneralLEGO Proof General
3473,135764
-@node LEGO specific commandsLEGO specific commands
3514,137133
-@node LEGO tagsLEGO tags
3534,137588
-@node LEGO customizationsLEGO customizations
3544,137835
-@node Coq Proof GeneralCoq Proof General
3576,138754
-@node Coq-specific commandsCoq-specific commands
3592,139163
-@node Coq-specific variablesCoq-specific variables
3614,139670
-@node Editing multiple proofsEditing multiple proofs
3636,140328
-@node User-loaded tacticsUser-loaded tactics
3660,141436
-@node Holes featureHoles feature
3724,143910
-@node Isabelle Proof GeneralIsabelle Proof General
3751,145197
-@node Isabelle commandsIsabelle commands
3781,146327
-@node Logics and SettingsLogics and Settings
3926,150484
-@node Isabelle customizationsIsabelle customizations
3960,152024
-@node HOL Proof GeneralHOL Proof General
3984,152506
-@node Shell Proof GeneralShell Proof General
4026,154328
-@node Obtaining and InstallingObtaining and Installing
4062,155787
-@node Obtaining Proof GeneralObtaining Proof General
4078,156200
-@node Installing Proof General from tarballInstalling Proof General from tarball
4109,157439
-@node Installing Proof General from RPM packageInstalling Proof General from RPM package
4134,158271
-@node Setting the names of binariesSetting the names of binaries
4149,158679
-@node Notes for syssiesNotes for syssies
4177,159619
-@node Bugs and EnhancementsBugs and Enhancements
4252,162655
-@node References4273,163470
-@node History of Proof GeneralHistory of Proof General
4313,164494
-@node Old News for 3.0Old News for 3.0
4404,168596
-@node Old News for 3.1Old News for 3.1
4474,172290
-@node Old News for 3.2Old News for 3.2
4500,173462
-@node Old News for 3.3Old News for 3.3
4561,176465
-@node Old News for 3.4Old News for 3.4
4580,177362
-@node Function IndexFunction Index
4603,178418
-@node Variable IndexVariable Index
4607,178494
-@node Keystroke IndexKeystroke Index
4611,178574
-@node Concept IndexConcept Index
4615,178640
+doc/ProofGeneral.texi,5597
+@node Top167,5079
+@node Preface204,6207
+@node Latest news for version 3.7Latest news for version 3.7
227,6803
+@node Future269,8725
+@node Credits300,10024
+@node Introducing Proof GeneralIntroducing Proof General
406,13793
+@node Installing Proof GeneralInstalling Proof General
462,15835
+@node Quick start guideQuick start guide
476,16284
+@node Features of Proof GeneralFeatures of Proof General
520,18405
+@node Supported proof assistantsSupported proof assistants
609,22342
+@node Prerequisites for this manualPrerequisites for this manual
658,24248
+@node Organization of this manualOrganization of this manual
702,25874
+@node Basic Script ManagementBasic Script Management
728,26702
+@node Walkthrough example in IsabelleWalkthrough example in Isabelle
747,27302
+@node Proof scriptsProof scripts
998,36955
+@node Script buffersScript buffers
1041,39075
+@node Locked queue and editing regionsLocked queue and editing regions
1063,39652
+@node Goal-save sequencesGoal-save sequences
1119,41799
+@node Active scripting bufferActive scripting buffer
1156,43285
+@node Summary of Proof General buffersSummary of Proof General buffers
1225,46705
+@node Script editing commandsScript editing commands
1287,49379
+@node Script processing commandsScript processing commands
1365,52238
+@node Proof assistant commandsProof assistant commands
1493,57539
+@node Toolbar commandsToolbar commands
1659,63318
+@node Interrupting during trace outputInterrupting during trace output
1683,64247
+@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
1722,66171
+@node Goals buffer commandsGoals buffer commands
1736,66671
+@node Advanced Script Management and EditingAdvanced Script Management and Editing
1825,70210
+@node Visibility of completed proofsVisibility of completed proofs
1857,71422
+@node Switching between proof scriptsSwitching between proof scripts
1912,73345
+@node View of processed files View of processed files 
1949,75317
+@node Retracting across filesRetracting across files
2009,78368
+@node Asserting across filesAsserting across files
2022,78999
+@node Automatic multiple file handlingAutomatic multiple file handling
2035,79565
+@node Escaping script managementEscaping script management
2060,80599
+@node Editing featuresEditing features
2118,82802
+@node Experimental featuresExperimental features
2182,85474
+@node Support for other PackagesSupport for other Packages
2216,86738
+@node Syntax highlightingSyntax highlighting
2249,87633
+@node X-Symbol supportX-Symbol support
2288,89254
+@node Unicode supportUnicode support
2346,91794
+@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)
2461,96591
+@node Support for outline modeSupport for outline mode
2520,98721
+@node Support for completionSupport for completion
2546,99851
+@node Support for tagsSupport for tags
2604,102027
+@node Customizing Proof GeneralCustomizing Proof General
2656,104356
+@node Basic optionsBasic options
2696,106026
+@node How to customizeHow to customize
2720,106784
+@node Display customizationDisplay customization
2771,108886
+@node User optionsUser options
2896,114124
+@node Changing facesChanging faces
3168,123823
+@node Tweaking configuration settingsTweaking configuration settings
3243,126492
+@node Hints and TipsHints and Tips
3300,129018
+@node Adding your own keybindingsAdding your own keybindings
3319,129619
+@node Using file variablesUsing file variables
3375,132152
+@node Using abbreviationsUsing abbreviations
3434,134338
+@node LEGO Proof GeneralLEGO Proof General
3473,135754
+@node LEGO specific commandsLEGO specific commands
3514,137123
+@node LEGO tagsLEGO tags
3534,137578
+@node LEGO customizationsLEGO customizations
3544,137825
+@node Coq Proof GeneralCoq Proof General
3576,138744
+@node Coq-specific commandsCoq-specific commands
3592,139153
+@node Coq-specific variablesCoq-specific variables
3614,139660
+@node Editing multiple proofsEditing multiple proofs
3636,140318
+@node User-loaded tacticsUser-loaded tactics
3660,141426
+@node Holes featureHoles feature
3724,143900
+@node Isabelle Proof GeneralIsabelle Proof General
3751,145187
+@node Choosing logic and starting isabelleChoosing logic and starting isabelle
3782,146356
+@node Isabelle commandsIsabelle commands
3831,148313
+@node Isabelle settingsIsabelle settings
3974,152468
+@node Isabelle customizationsIsabelle customizations
3988,153050
+@node HOL Proof GeneralHOL Proof General
4011,153537
+@node Shell Proof GeneralShell Proof General
4053,155359
+@node Obtaining and InstallingObtaining and Installing
4089,156818
+@node Obtaining Proof GeneralObtaining Proof General
4105,157231
+@node Installing Proof General from tarballInstalling Proof General from tarball
4136,158470
+@node Installing Proof General from RPM packageInstalling Proof General from RPM package
4161,159302
+@node Setting the names of binariesSetting the names of binaries
4176,159710
+@node Notes for syssiesNotes for syssies
4204,160650
+@node Bugs and EnhancementsBugs and Enhancements
4279,163686
+@node References4300,164501
+@node History of Proof GeneralHistory of Proof General
4340,165524
+@node Old News for 3.0Old News for 3.0
4431,169626
+@node Old News for 3.1Old News for 3.1
4501,173320
+@node Old News for 3.2Old News for 3.2
4527,174492
+@node Old News for 3.3Old News for 3.3
4588,177495
+@node Old News for 3.4Old News for 3.4
4607,178392
+@node Function IndexFunction Index
4630,179448
+@node Variable IndexVariable Index
4634,179524
+@node Keystroke IndexKeystroke Index
4638,179604
+@node Concept IndexConcept Index
4642,179670
 
 doc/PG-adapting.texi,3776
 @node Top157,4776