Updated.

2 files changed, 569 insertions, 537 deletions

diff --git a/COMPATIBILITY b/COMPATIBILITY
index c07a928b..64af7b6c 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -6,9 +6,9 @@ on Linux:
 
  Emacs 22.1.1	       -- recommended and supported
 
- Emacs 21.4.1          -- tested; works except X-Symbol sub/superscripts
- XEmacs 21.4.XX	       -- tested
+ Emacs 21.4.1          -- tested; poorer X-Symbol sub/superscript support
  XEmacs 21.5 (beta28)  -- tested; PG has workarounds for several bugs
+ XEmacs 21.4.XX	       -- tested
 
 and prover versions:
 
diff --git a/TAGS b/TAGS
index 66f800da..ce9cce75 100644
--- a/TAGS
+++ b/TAGS
@@ -185,7 +185,7 @@ coq/coq.el,6066
 (defun is-not-split-vertic 1587,58739
 (defun optim-resp-windows 1596,59178
 
-coq/coq-indent.el,2247
+coq/coq-indent.el,2259
 (defconst coq-any-command-regexp17,315
 (defconst coq-indent-inner-regexp20,406
 (defconst coq-comment-start-regexp 31,794
@@ -214,30 +214,30 @@ coq/coq-indent.el,2247
 (defconst coq-end-command-or-comment-start-regexp173,6813
 (defun coq-find-not-in-comment-backward 177,6931
 (defun coq-find-not-in-comment-forward 197,7832
-(defun coq-find-command-end-backward 217,8753
-(defun coq-find-command-end-forward 226,9144
-(defun coq-find-command-end 235,9521
-(defun coq-parse-function 244,9904
-(defun coq-find-current-start 253,10106
-(defun coq-find-real-start 262,10397
-(defun coq-command-at-point 269,10616
-(defun only-spaces-on-line 276,10893
-(defun coq-indent-find-reg 285,11164
-(defun coq-find-no-syntactic-on-line 299,11700
-(defun coq-back-to-indentation-prevline 312,12173
-(defun coq-find-unclosed 356,14087
-(defun coq-find-at-same-level-zero 386,15267
-(defun coq-find-unopened 414,16345
-(defun coq-find-last-unopened 457,17795
-(defun coq-end-offset 468,18192
-(defun coq-indent-command-offset 493,18983
-(defun coq-indent-expr-offset 540,20807
-(defun coq-indent-comment-offset 656,25510
-(defun coq-indent-offset 688,26957
-(defun coq-indent-calculate 706,27820
-(defun coq-indent-line 709,27908
-(defun coq-indent-line-not-comments 719,28274
-(defun coq-indent-region 729,28663
+(defun coq-find-command-end-backward 221,8974
+(defun coq-find-command-end-forward 230,9365
+(defun coq-find-command-end 239,9742
+(defun coq-parse-function 248,10125
+(defun coq-find-current-start 257,10327
+(defun coq-find-real-start 266,10618
+(defun coq-command-at-point 273,10837
+(defun coq-indent-only-spaces-on-line 280,11114
+(defun coq-indent-find-reg 286,11391
+(defun coq-find-no-syntactic-on-line 300,11927
+(defun coq-back-to-indentation-prevline 313,12400
+(defun coq-find-unclosed 357,14314
+(defun coq-find-at-same-level-zero 387,15615
+(defun coq-find-unopened 415,16780
+(defun coq-find-last-unopened 458,18230
+(defun coq-end-offset 469,18627
+(defun coq-indent-command-offset 494,19418
+(defun coq-indent-expr-offset 541,21242
+(defun coq-indent-comment-offset 657,25945
+(defun coq-indent-offset 689,27403
+(defun coq-indent-calculate 707,28266
+(defun coq-indent-line 710,28354
+(defun coq-indent-line-not-comments 720,28720
+(defun coq-indent-region 730,29109
 
 coq/coq-local-vars.el,279
 (defconst coq-local-vars-doc 17,306
@@ -364,41 +364,50 @@ demoisa/demoisa.el,349
 (define-derived-mode demoisa-response-mode 127,4196
 (define-derived-mode demoisa-goals-mode 131,4323
 
-isar/isabelle-system.el,1399
-(defgroup isabelle 26,775
-(defcustom isabelle-web-page30,903
-(defcustom isa-isatool-command41,1198
-(defvar isatool-not-found 68,2141
-(defun isa-set-isatool-command 71,2254
-(defun isa-shell-command-to-string 91,3115
-(defun isa-getenv 97,3339
-(defcustom isabelle-program-name116,4000
-(defvar isabelle-prog-name 142,4930
-(defun isa-tool-list-logics 145,5057
-(defcustom isabelle-logics-available 152,5294
-(defcustom isabelle-chosen-logic 163,5658
-(defun isabelle-command-line 176,6126
-(defun isabelle-choose-logic 199,7083
-(defun isa-view-doc 221,8049
-(defun isa-tool-list-docs 229,8274
-(defconst isabelle-verbatim-regexp 256,9306
-(defun isabelle-verbatim 259,9448
-(defcustom isabelle-refresh-logics 266,9609
-(defvar isabelle-docs-menu 274,9936
-(defvar isabelle-logics-menu-entries 282,10223
-(defun isabelle-logics-menu-calculate 285,10296
-(defvar isabelle-time-to-refresh-logics 304,10859
-(defun isabelle-logics-menu-refresh 308,10954
-(defun isabelle-logics-menu-filter 325,11651
-(defun isabelle-menu-bar-update-logics 331,11861
-(defvar isabelle-logics-menu342,12200
-(defun isabelle-load-isar-keywords 355,12812
-(defpgdefault menu-entries376,13553
-(defpgdefault help-menu-entries 379,13605
-(defun isabelle-convert-idmarkup-to-subterm 407,14363
-(defun isabelle-create-span-menu 431,15374
-(defun isabelle-xml-sml-escapes 447,15816
-(defun isabelle-process-pgip 450,15917
+isar/isabelle-system.el,1401
+(defgroup isabelle 26,776
+(defcustom isabelle-web-page30,904
+(defcustom isa-isatool-command41,1199
+(defvar isatool-not-found 71,2261
+(defun isa-set-isatool-command 74,2374
+(defun isa-shell-command-to-string 96,3296
+(defun isa-getenv 102,3520
+(defcustom isabelle-program-name122,4207
+(defvar isabelle-prog-name 148,5137
+(defun isa-tool-list-logics 151,5264
+(defcustom isabelle-logics-available 158,5501
+(defcustom isabelle-chosen-logic 169,5865
+(defun isabelle-command-line 182,6333
+(defun isabelle-choose-logic 205,7290
+(defun isa-view-doc 227,8256
+(defun isa-tool-list-docs 236,8520
+(defconst isabelle-verbatim-regexp 263,9552
+(defun isabelle-verbatim 266,9694
+(defcustom isabelle-refresh-logics 273,9855
+(defvar isabelle-docs-menu 281,10182
+(defvar isabelle-logics-menu-entries 289,10469
+(defun isabelle-logics-menu-calculate 292,10542
+(defvar isabelle-time-to-refresh-logics 311,11105
+(defun isabelle-logics-menu-refresh 315,11200
+(defun isabelle-logics-menu-filter 332,11897
+(defun isabelle-menu-bar-update-logics 338,12107
+(defvar isabelle-logics-menu349,12446
+(defun isabelle-load-isar-keywords 362,13058
+(defpgdefault menu-entries383,13799
+(defpgdefault help-menu-entries 386,13851
+(defun isabelle-convert-idmarkup-to-subterm 414,14609
+(defun isabelle-create-span-menu 438,15620
+(defun isabelle-xml-sml-escapes 454,16062
+(defun isabelle-process-pgip 457,16163
+
+isar/isabelle-unicode-tokens.el,257
+(defconst isar-token-format 10,368
+(defconst isar-charref-format 11,406
+(defconst isar-token-prefix 12,448
+(defconst isar-token-suffix 13,483
+(defconst isar-token-match 14,516
+(defconst isar-hexcode-match 15,570
+(defconst isar-token-name-alist17,632
 
 isar/isar.el,1204
 (defcustom isar-keywords-name 31,721
@@ -1259,87 +1268,74 @@ generic/pg-pbrpm.el,1802
 (defun pg-pbrpm-process-regions-list 533,19781
 (defun pg-pbrpm-region-expression 537,19964
 
-generic/pg-pgip.el,2892
-(defalias 'pg-pgip-debug pg-pgip-debug
36,985
-(defalias 'pg-pgip-error pg-pgip-error
37,1026
-(defalias 'pg-pgip-warning pg-pgip-warning
38,1061
-(defconst pg-pgip-version-supported 40,1111
-(defun pg-pgip-process-packet 44,1217
-(defvar pg-pgip-last-seen-id 54,1789
-(defvar pg-pgip-last-seen-seq 55,1823
-(defun pg-pgip-process-pgip 57,1859
-(defun pg-pgip-process-msg 76,2790
-(defvar pg-pgip-post-process-functions90,3360
-(defun pg-pgip-post-process 100,3848
-(defun pg-pgip-process-askpgip 116,4459
-(defun pg-pgip-process-usespgip 122,4664
-(defun pg-pgip-process-usespgml 126,4828
-(defun pg-pgip-process-pgmlconfig 130,4992
-(defun pg-pgip-process-proverinfo 146,5609
-(defun pg-pgip-process-hasprefs 163,6274
-(defun pg-pgip-haspref 177,6906
-(defun pg-pgip-process-prefval 196,7682
-(defun pg-pgip-process-guiconfig 223,8391
-(defvar proof-assistant-idtables 230,8508
-(defun pg-pgip-process-ids 233,8625
-(defun pg-complete-idtable-symbol 259,9701
-(defalias 'pg-pgip-process-setids pg-pgip-process-setids
264,9793
-(defalias 'pg-pgip-process-addids pg-pgip-process-addids
265,9849
-(defalias 'pg-pgip-process-delids pg-pgip-process-delids
266,9905
-(defun pg-pgip-process-idvalue 269,9963
-(defun pg-pgip-process-menuadd 281,10299
-(defun pg-pgip-process-menudel 284,10342
-(defun pg-pgip-process-ready 293,10575
-(defun pg-pgip-process-cleardisplay 296,10616
-(defun pg-pgip-process-proofstate 310,11073
-(defun pg-pgip-process-normalresponse 314,11150
-(defun pg-pgip-process-errorresponse 318,11274
-(defun pg-pgip-process-scriptinsert 322,11397
-(defun pg-pgip-process-metainforesponse 327,11531
-(defun pg-pgip-process-informfileloaded 336,11772
-(defun pg-pgip-process-informfileretracted 342,12038
-(defun pg-pgip-process-brokerstatus 355,12515
-(defun pg-pgip-process-proveravailmsg 358,12563
-(defun pg-pgip-process-newprovermsg 361,12613
-(defun pg-pgip-process-proverstatusmsg 364,12661
-(defvar pg-pgip-srcids 373,12908
-(defun pg-pgip-process-newfile 377,13015
-(defun pg-pgip-process-filestatus 393,13603
-(defun pg-pgip-process-newobj 413,14258
-(defun pg-pgip-process-delobj 416,14300
-(defun pg-pgip-process-objectstatus 419,14342
-(defun pg-pgip-process-parsescript 433,14697
-(defun pg-pgip-get-pgiptype 456,15572
-(defun pg-pgip-default-for 476,16365
-(defun pg-pgip-subst-for 489,16760
-(defun pg-pgip-interpret-value 501,17103
-(defun pg-pgip-interpret-choice 519,17788
-(defun pg-pgip-string-of-command 550,18805
-(defconst pg-pgip-id567,19566
-(defvar pg-pgip-refseq 573,19846
-(defvar pg-pgip-refid 575,19943
-(defvar pg-pgip-seq 578,20035
-(defun pg-pgip-assemble-packet 580,20099
-(defun pg-pgip-issue 598,20911
-(defun pg-pgip-maybe-askpgip 615,21523
-(defun pg-pgip-askprefs 621,21714
-(defun pg-pgip-askids 625,21828
-(defun pg-pgip-reset 638,22116
-(defconst pg-pgip-start-element-regexp 669,22814
-(defconst pg-pgip-end-element-regexp 670,22866
-
-generic/pg-pgip-old.el,456
-(defun pg-pgip-process-oldhaspref 19,617
-(defun pg-pgip-process-haspref 22,714
-(defun pg-pgip-old-interpret-bool 58,2142
-(defun pg-pgip-old-interpret-int 67,2426
-(defun pg-pgip-old-interpret-string 72,2599
-(defun pg-pgip-old-interpret-choice 75,2653
-(defun pg-pgip-old-interpret-value 95,3372
-(defun pg-pgip-old-default-for 114,3918
-(defun pg-pgip-old-subst-for 125,4242
-(defun pg-pgip-old-get-type 132,4407
-(defun pg-pgip-old-pgiptype 139,4623
+generic/pg-pgip.el,2889
+(defalias 'pg-pgip-debug pg-pgip-debug
35,920
+(defalias 'pg-pgip-error pg-pgip-error
36,961
+(defalias 'pg-pgip-warning pg-pgip-warning
37,996
+(defconst pg-pgip-version-supported 39,1046
+(defun pg-pgip-process-packet 43,1152
+(defvar pg-pgip-last-seen-id 53,1724
+(defvar pg-pgip-last-seen-seq 54,1758
+(defun pg-pgip-process-pgip 56,1794
+(defun pg-pgip-process-msg 75,2725
+(defvar pg-pgip-post-process-functions89,3295
+(defun pg-pgip-post-process 99,3783
+(defun pg-pgip-process-askpgip 115,4394
+(defun pg-pgip-process-usespgip 121,4599
+(defun pg-pgip-process-usespgml 125,4763
+(defun pg-pgip-process-pgmlconfig 129,4927
+(defun pg-pgip-process-proverinfo 145,5544
+(defun pg-pgip-process-hasprefs 162,6209
+(defun pg-pgip-haspref 176,6841
+(defun pg-pgip-process-prefval 195,7617
+(defun pg-pgip-process-guiconfig 222,8326
+(defvar proof-assistant-idtables 229,8443
+(defun pg-pgip-process-ids 232,8560
+(defun pg-complete-idtable-symbol 258,9636
+(defalias 'pg-pgip-process-setids pg-pgip-process-setids
263,9728
+(defalias 'pg-pgip-process-addids pg-pgip-process-addids
264,9784
+(defalias 'pg-pgip-process-delids pg-pgip-process-delids
265,9840
+(defun pg-pgip-process-idvalue 268,9898
+(defun pg-pgip-process-menuadd 280,10234
+(defun pg-pgip-process-menudel 283,10277
+(defun pg-pgip-process-ready 292,10510
+(defun pg-pgip-process-cleardisplay 295,10551
+(defun pg-pgip-process-proofstate 309,11008
+(defun pg-pgip-process-normalresponse 313,11085
+(defun pg-pgip-process-errorresponse 317,11209
+(defun pg-pgip-process-scriptinsert 321,11332
+(defun pg-pgip-process-metainforesponse 326,11466
+(defun pg-pgip-process-informfileloaded 335,11707
+(defun pg-pgip-process-informfileretracted 341,11973
+(defun pg-pgip-process-brokerstatus 354,12450
+(defun pg-pgip-process-proveravailmsg 357,12498
+(defun pg-pgip-process-newprovermsg 360,12548
+(defun pg-pgip-process-proverstatusmsg 363,12596
+(defvar pg-pgip-srcids 372,12843
+(defun pg-pgip-process-newfile 376,12950
+(defun pg-pgip-process-filestatus 392,13538
+(defun pg-pgip-process-newobj 412,14193
+(defun pg-pgip-process-delobj 415,14235
+(defun pg-pgip-process-objectstatus 418,14277
+(defun pg-pgip-process-parsescript 432,14632
+(defun pg-pgip-get-pgiptype 455,15507
+(defun pg-pgip-default-for 475,16300
+(defun pg-pgip-subst-for 488,16695
+(defun pg-pgip-interpret-value 500,17038
+(defun pg-pgip-interpret-choice 518,17723
+(defun pg-pgip-string-of-command 549,18740
+(defconst pg-pgip-id566,19501
+(defvar pg-pgip-refseq 572,19781
+(defvar pg-pgip-refid 574,19878
+(defvar pg-pgip-seq 577,19970
+(defun pg-pgip-assemble-packet 579,20034
+(defun pg-pgip-issue 597,20846
+(defun pg-pgip-maybe-askpgip 614,21458
+(defun pg-pgip-askprefs 620,21649
+(defun pg-pgip-askids 624,21763
+(defun pg-pgip-reset 637,22051
+(defconst pg-pgip-start-element-regexp 668,22749
+(defconst pg-pgip-end-element-regexp 669,22801
 
 generic/pg-response.el,1182
 (deflocal pg-response-eagerly-raise 31,731
@@ -1804,50 +1800,50 @@ generic/proof-menu.el,2101
 (defvar proof-buffer-menu225,8231
 (defun proof-keep-response-history 287,10476
 (defconst proof-quick-opts-menu295,10786
-(defun proof-quick-opts-vars 449,16914
-(defun proof-quick-opts-changed-from-defaults-p 474,17665
-(defun proof-quick-opts-changed-from-saved-p 478,17770
-(defun proof-quick-opts-save 489,18122
-(defun proof-quick-opts-reset 494,18290
-(defconst proof-config-menu506,18558
-(defconst proof-advanced-menu513,18737
-(defvar proof-menu 526,19172
-(defun proof-main-menu 535,19456
-(defun proof-aux-menu 546,19722
-(defun proof-menu-define-favourites-menu 562,20069
-(defun proof-def-favourite 582,20725
-(defvar proof-make-favourite-cmd-history 605,21700
-(defvar proof-make-favourite-menu-history 608,21785
-(defun proof-save-favourites 611,21871
-(defun proof-del-favourite 616,22019
-(defun proof-read-favourite 633,22580
-(defun proof-add-favourite 658,23383
-(defvar proof-menu-settings 685,24434
-(defun proof-menu-define-settings-menu 688,24508
-(defun proof-menu-entry-name 708,25252
-(defun proof-menu-entry-for-setting 720,25724
-(defun proof-settings-vars 738,26214
-(defun proof-settings-changed-from-defaults-p 743,26391
-(defun proof-settings-changed-from-saved-p 747,26497
-(defun proof-settings-save 751,26600
-(defun proof-settings-reset 756,26767
-(defun proof-defpacustom-fn 763,27012
-(defmacro defpacustom 839,29896
-(defun proof-assistant-invisible-command-ifposs 854,30723
-(defun proof-maybe-askprefs 876,31698
-(defun proof-assistant-settings-cmd 883,31902
-(defvar proof-assistant-format-table 900,32562
-(defun proof-assistant-format-bool 908,32931
-(defun proof-assistant-format-int 911,33044
-(defun proof-assistant-format-string 914,33136
-(defun proof-assistant-format 917,33234
+(defun proof-quick-opts-vars 450,16937
+(defun proof-quick-opts-changed-from-defaults-p 475,17688
+(defun proof-quick-opts-changed-from-saved-p 479,17793
+(defun proof-quick-opts-save 490,18145
+(defun proof-quick-opts-reset 495,18313
+(defconst proof-config-menu507,18581
+(defconst proof-advanced-menu514,18760
+(defvar proof-menu 527,19195
+(defun proof-main-menu 536,19479
+(defun proof-aux-menu 547,19745
+(defun proof-menu-define-favourites-menu 563,20092
+(defun proof-def-favourite 583,20748
+(defvar proof-make-favourite-cmd-history 606,21723
+(defvar proof-make-favourite-menu-history 609,21808
+(defun proof-save-favourites 612,21894
+(defun proof-del-favourite 617,22042
+(defun proof-read-favourite 634,22603
+(defun proof-add-favourite 659,23406
+(defvar proof-menu-settings 686,24457
+(defun proof-menu-define-settings-menu 689,24531
+(defun proof-menu-entry-name 709,25275
+(defun proof-menu-entry-for-setting 721,25747
+(defun proof-settings-vars 739,26237
+(defun proof-settings-changed-from-defaults-p 744,26414
+(defun proof-settings-changed-from-saved-p 748,26520
+(defun proof-settings-save 752,26623
+(defun proof-settings-reset 757,26790
+(defun proof-defpacustom-fn 764,27035
+(defmacro defpacustom 840,29919
+(defun proof-assistant-invisible-command-ifposs 855,30746
+(defun proof-maybe-askprefs 877,31721
+(defun proof-assistant-settings-cmd 884,31925
+(defvar proof-assistant-format-table 901,32585
+(defun proof-assistant-format-bool 909,32954
+(defun proof-assistant-format-int 912,33067
+(defun proof-assistant-format-string 915,33159
+(defun proof-assistant-format 918,33257
 
 generic/proof-mmm.el,114
 (defun proof-mmm-support-available 34,1131
 (defun proof-mmm-set-global 58,1979
 (defun proof-mmm-enable 73,2520
 
-generic/proof-script.el,5058
+generic/proof-script.el,5108
 (defvar proof-element-counters 28,719
 (deflocal proof-active-buffer-fake-minor-mode 34,859
 (deflocal proof-script-buffer-file-name 37,985
@@ -1888,77 +1884,78 @@ generic/proof-script.el,5058
 (defun proof-goto-end-of-queue-or-locked-if-not-visible 475,17368
 (defvar pg-idioms 494,18018
 (defvar pg-visibility-specs 497,18114
-(defun pg-clear-script-portions 502,18321
-(defun pg-add-script-element 516,18850
-(defun pg-remove-script-element 519,18926
-(defsubst pg-visname 527,19204
-(defun pg-add-element 531,19349
-(defun pg-open-invisible-span 565,20978
-(defun pg-remove-element 576,21341
-(defun pg-make-element-invisible 583,21611
-(defun pg-make-element-visible 589,21868
-(defun pg-toggle-element-visibility 594,22047
-(defun pg-redisplay-for-gnuemacs 602,22377
-(defun pg-show-all-portions 609,22648
-(defun pg-show-all-proofs 627,23319
-(defun pg-hide-all-proofs 632,23447
-(defun pg-add-proof-element 637,23578
-(defun pg-span-name 651,24198
-(defvar pg-span-context-menu-keymap672,24905
-(defun pg-set-span-helphighlights 685,25276
-(defun proof-complete-buffer-atomic 713,26205
-(defun proof-register-possibly-new-processed-file 754,28120
-(defun proof-inform-prover-file-retracted 805,30248
-(defun proof-auto-retract-dependencies 824,31034
-(defun proof-unregister-buffer-file-name 878,33574
-(defun proof-protected-process-or-retract 924,35397
-(defun proof-deactivate-scripting-auto 951,36567
-(defun proof-deactivate-scripting 960,36925
-(defun proof-activate-scripting 1097,42330
-(defun proof-toggle-active-scripting 1219,47762
-(defun proof-done-advancing 1260,49123
-(defun proof-done-advancing-comment 1355,52771
-(defun proof-done-advancing-save 1374,53513
-(defun proof-make-goalsave 1467,57128
-(defun proof-get-name-from-goal 1482,57871
-(defun proof-done-advancing-autosave 1501,58897
-(defun proof-done-advancing-other 1566,61443
-(defun proof-segment-up-to-parser 1594,62402
-(defun proof-script-generic-parse-find-comment-end 1657,64478
-(defun proof-script-generic-parse-cmdend 1666,64894
-(defun proof-script-generic-parse-cmdstart 1691,65789
-(defun proof-script-generic-parse-sexp 1754,68497
-(defun proof-cmdstart-add-segment-for-cmd 1778,69433
-(defun proof-segment-up-to-cmdstart 1830,71632
-(defun proof-segment-up-to-cmdend 1891,73992
-(defun proof-semis-to-vanillas 1963,76657
-(defun proof-script-new-command-advance 2002,77983
-(defun proof-script-next-command-advance 2044,79724
-(defun proof-assert-until-point-interactive 2056,80165
-(defun proof-assert-until-point 2082,81287
-(defun proof-assert-next-command2135,83719
-(defun proof-goto-point 2183,85982
-(defun proof-insert-pbp-command 2201,86523
-(defun proof-done-retracting 2233,87623
-(defun proof-setup-retract-action 2269,89109
-(defun proof-last-goal-or-goalsave 2279,89592
-(defun proof-retract-target 2302,90432
-(defun proof-retract-until-point-interactive 2387,94073
-(defun proof-retract-until-point 2395,94458
-(define-derived-mode proof-mode 2438,96207
-(defun proof-script-set-visited-file-name 2488,98134
-(defun proof-script-set-buffer-hooks 2512,99136
-(defun proof-script-kill-buffer-fn 2520,99554
-(defun proof-config-done-related 2564,101376
-(defun proof-generic-goal-command-p 2634,103854
-(defun proof-generic-state-preserving-p 2639,104066
-(defun proof-generic-count-undos 2648,104583
-(defun proof-generic-find-and-forget 2677,105613
-(defconst proof-script-important-settings2728,107438
-(defun proof-config-done 2743,107991
-(defun proof-setup-parsing-mechanism 2831,111109
-(defun proof-setup-imenu 2875,112962
-(defun proof-setup-func-menu 2892,113567
+(defconst pg-default-invisibility-spec 502,18321
+(defun pg-clear-script-portions 506,18461
+(defun pg-add-script-element 520,18938
+(defun pg-remove-script-element 523,19014
+(defsubst pg-visname 531,19292
+(defun pg-add-element 535,19437
+(defun pg-open-invisible-span 569,21066
+(defun pg-remove-element 580,21429
+(defun pg-make-element-invisible 587,21699
+(defun pg-make-element-visible 593,21956
+(defun pg-toggle-element-visibility 598,22135
+(defun pg-redisplay-for-gnuemacs 606,22465
+(defun pg-show-all-portions 613,22736
+(defun pg-show-all-proofs 631,23407
+(defun pg-hide-all-proofs 636,23535
+(defun pg-add-proof-element 641,23666
+(defun pg-span-name 655,24286
+(defvar pg-span-context-menu-keymap676,24993
+(defun pg-set-span-helphighlights 689,25364
+(defun proof-complete-buffer-atomic 717,26293
+(defun proof-register-possibly-new-processed-file 758,28208
+(defun proof-inform-prover-file-retracted 809,30336
+(defun proof-auto-retract-dependencies 828,31122
+(defun proof-unregister-buffer-file-name 882,33662
+(defun proof-protected-process-or-retract 928,35485
+(defun proof-deactivate-scripting-auto 955,36655
+(defun proof-deactivate-scripting 964,37013
+(defun proof-activate-scripting 1101,42418
+(defun proof-toggle-active-scripting 1223,47850
+(defun proof-done-advancing 1264,49211
+(defun proof-done-advancing-comment 1359,52859
+(defun proof-done-advancing-save 1378,53601
+(defun proof-make-goalsave 1471,57216
+(defun proof-get-name-from-goal 1486,57959
+(defun proof-done-advancing-autosave 1505,58985
+(defun proof-done-advancing-other 1570,61531
+(defun proof-segment-up-to-parser 1598,62490
+(defun proof-script-generic-parse-find-comment-end 1661,64566
+(defun proof-script-generic-parse-cmdend 1670,64982
+(defun proof-script-generic-parse-cmdstart 1695,65877
+(defun proof-script-generic-parse-sexp 1758,68585
+(defun proof-cmdstart-add-segment-for-cmd 1782,69521
+(defun proof-segment-up-to-cmdstart 1834,71720
+(defun proof-segment-up-to-cmdend 1895,74080
+(defun proof-semis-to-vanillas 1967,76745
+(defun proof-script-new-command-advance 2006,78071
+(defun proof-script-next-command-advance 2048,79812
+(defun proof-assert-until-point-interactive 2060,80253
+(defun proof-assert-until-point 2086,81375
+(defun proof-assert-next-command2139,83807
+(defun proof-goto-point 2187,86070
+(defun proof-insert-pbp-command 2205,86611
+(defun proof-done-retracting 2237,87711
+(defun proof-setup-retract-action 2273,89197
+(defun proof-last-goal-or-goalsave 2283,89680
+(defun proof-retract-target 2306,90520
+(defun proof-retract-until-point-interactive 2391,94161
+(defun proof-retract-until-point 2399,94546
+(define-derived-mode proof-mode 2442,96295
+(defun proof-script-set-visited-file-name 2492,98222
+(defun proof-script-set-buffer-hooks 2516,99224
+(defun proof-script-kill-buffer-fn 2524,99642
+(defun proof-config-done-related 2568,101464
+(defun proof-generic-goal-command-p 2638,103942
+(defun proof-generic-state-preserving-p 2643,104154
+(defun proof-generic-count-undos 2652,104671
+(defun proof-generic-find-and-forget 2681,105701
+(defconst proof-script-important-settings2732,107526
+(defun proof-config-done 2747,108079
+(defun proof-setup-parsing-mechanism 2835,111197
+(defun proof-setup-imenu 2879,113050
+(defun proof-setup-func-menu 2896,113655
 
 generic/proof-shell.el,3315
 (defvar proof-marker 28,643
@@ -1977,62 +1974,62 @@ generic/proof-shell.el,3315
 (defcustom proof-shell-fiddle-frames 208,6507
 (defun proof-shell-set-text-representation 215,6748
 (defun proof-shell-start 228,7303
-(defvar proof-shell-kill-function-hooks 437,14828
-(defun proof-shell-kill-function 440,14926
-(defun proof-shell-clear-state 529,18729
-(defun proof-shell-exit 544,19172
-(defun proof-shell-bail-out 556,19617
-(defun proof-shell-restart 565,20094
-(defvar proof-shell-no-response-display 607,21478
-(defvar proof-shell-urgent-message-marker 610,21582
-(defvar proof-shell-urgent-message-scanner 613,21703
-(defun proof-shell-handle-output 617,21830
-(defun proof-shell-handle-delayed-output 677,24471
-(defvar proof-shell-no-error-display 705,25514
-(defun proof-shell-handle-error 711,25718
-(defun proof-shell-handle-interrupt 729,26554
-(defun proof-shell-error-or-interrupt-action 743,27167
-(defun proof-goals-pos 768,28312
-(defun proof-pbp-focus-on-first-goal 773,28517
-(defsubst proof-shell-string-match-safe 785,29047
-(defun proof-shell-process-output 790,29215
-(defvar proof-shell-insert-space-fudge 901,33855
-(defun proof-shell-insert 911,34174
-(defun proof-shell-command-queue-item 985,37085
-(defun proof-shell-set-silent 990,37242
-(defun proof-shell-start-silent-item 996,37461
-(defun proof-shell-clear-silent 1002,37653
-(defun proof-shell-stop-silent-item 1008,37875
-(defun proof-shell-should-be-silent 1015,38147
-(defun proof-append-alist 1028,38703
-(defun proof-start-queue 1087,40940
-(defun proof-extend-queue 1098,41289
-(defun proof-shell-exec-loop 1109,41670
-(defun proof-shell-insert-loopback-cmd 1174,44258
-(defun proof-shell-message 1202,45584
-(defun proof-shell-process-urgent-message 1208,45800
-(defun proof-shell-strip-eager-annotations 1340,51065
-(defvar proof-shell-minibuffer-urgent-interactive-input-history 1351,51401
-(defun proof-shell-minibuffer-urgent-interactive-input 1353,51471
-(defun proof-shell-process-urgent-messages 1363,51830
-(defun proof-shell-filter 1437,54929
-(defun proof-shell-filter-process-output 1596,61518
-(defvar pg-last-tracing-output-time 1649,63572
-(defconst pg-slow-mode-duration 1652,63678
-(defconst pg-fast-tracing-mode-threshold 1655,63760
-(defvar pg-tracing-cleanup-timer 1658,63888
-(defun pg-tracing-tight-loop 1660,63927
-(defun pg-finish-tracing-display 1703,65645
-(defun proof-shell-dont-show-annotations 1716,65951
-(defun proof-shell-show-annotations 1732,66472
-(defun proof-shell-wait 1754,66999
-(defun proof-done-invisible 1774,67909
-(defun proof-shell-invisible-command 1817,69632
-(defun proof-shell-invisible-cmd-get-result 1851,70897
-(defun proof-shell-invisible-command-invisible-result 1869,71593
-(define-derived-mode proof-shell-mode 1888,72023
-(defconst proof-shell-important-settings1958,74689
-(defun proof-shell-config-done 1964,74804
+(defvar proof-shell-kill-function-hooks 438,14850
+(defun proof-shell-kill-function 441,14948
+(defun proof-shell-clear-state 530,18751
+(defun proof-shell-exit 545,19194
+(defun proof-shell-bail-out 557,19639
+(defun proof-shell-restart 566,20116
+(defvar proof-shell-no-response-display 608,21500
+(defvar proof-shell-urgent-message-marker 611,21604
+(defvar proof-shell-urgent-message-scanner 614,21725
+(defun proof-shell-handle-output 618,21852
+(defun proof-shell-handle-delayed-output 678,24493
+(defvar proof-shell-no-error-display 706,25536
+(defun proof-shell-handle-error 712,25740
+(defun proof-shell-handle-interrupt 730,26576
+(defun proof-shell-error-or-interrupt-action 744,27189
+(defun proof-goals-pos 769,28334
+(defun proof-pbp-focus-on-first-goal 774,28539
+(defsubst proof-shell-string-match-safe 786,29069
+(defun proof-shell-process-output 791,29237
+(defvar proof-shell-insert-space-fudge 902,33877
+(defun proof-shell-insert 912,34196
+(defun proof-shell-command-queue-item 986,37107
+(defun proof-shell-set-silent 991,37264
+(defun proof-shell-start-silent-item 997,37483
+(defun proof-shell-clear-silent 1003,37675
+(defun proof-shell-stop-silent-item 1009,37897
+(defun proof-shell-should-be-silent 1016,38169
+(defun proof-append-alist 1029,38725
+(defun proof-start-queue 1088,40962
+(defun proof-extend-queue 1099,41311
+(defun proof-shell-exec-loop 1110,41692
+(defun proof-shell-insert-loopback-cmd 1175,44280
+(defun proof-shell-message 1203,45606
+(defun proof-shell-process-urgent-message 1209,45822
+(defun proof-shell-strip-eager-annotations 1341,51087
+(defvar proof-shell-minibuffer-urgent-interactive-input-history 1352,51423
+(defun proof-shell-minibuffer-urgent-interactive-input 1354,51493
+(defun proof-shell-process-urgent-messages 1364,51852
+(defun proof-shell-filter 1438,54951
+(defun proof-shell-filter-process-output 1597,61540
+(defvar pg-last-tracing-output-time 1650,63594
+(defconst pg-slow-mode-duration 1653,63700
+(defconst pg-fast-tracing-mode-threshold 1656,63782
+(defvar pg-tracing-cleanup-timer 1659,63910
+(defun pg-tracing-tight-loop 1661,63949
+(defun pg-finish-tracing-display 1704,65667
+(defun proof-shell-dont-show-annotations 1717,65973
+(defun proof-shell-show-annotations 1733,66494
+(defun proof-shell-wait 1755,67021
+(defun proof-done-invisible 1775,67931
+(defun proof-shell-invisible-command 1818,69654
+(defun proof-shell-invisible-cmd-get-result 1852,70919
+(defun proof-shell-invisible-command-invisible-result 1870,71615
+(define-derived-mode proof-shell-mode 1889,72045
+(defconst proof-shell-important-settings1959,74711
+(defun proof-shell-config-done 1965,74826
 
 generic/proof-site.el,505
 (defconst proof-assistant-table-default23,728
@@ -2189,31 +2186,31 @@ generic/proof-utils.el,2111
 (defun proof-font-lock-clear-font-lock-vars 372,13261
 (defun proof-font-lock-set-font-lock-vars 378,13473
 (defun proof-fontify-region 382,13629
-(defun pg-remove-specials 442,15930
-(defun pg-remove-specials-in-string 452,16268
-(defun proof-fontify-buffer 459,16455
-(defun proof-warn-if-unset 472,16696
-(defun proof-get-window-for-buffer 477,16914
-(defun proof-display-and-keep-buffer 528,19222
-(defun proof-clean-buffer 560,20529
-(defun proof-message 575,21150
-(defun proof-warning 580,21363
-(defun pg-internal-warning 586,21645
-(defun proof-debug 594,21964
-(defun proof-switch-to-buffer 609,22635
-(defun proof-resize-window-tofit 642,24324
-(defun proof-submit-bug-report 742,28336
-(defun proof-deftoggle-fn 778,29715
-(defmacro proof-deftoggle 793,30368
-(defun proof-defintset-fn 800,30742
-(defmacro proof-defintset 816,31446
-(defun proof-defstringset-fn 823,31823
-(defmacro proof-defstringset 836,32449
-(defmacro proof-defshortcut 850,32906
-(defmacro proof-definvisible 865,33545
-(defun pg-custom-save-vars 893,34522
-(defun pg-custom-reset-vars 911,35245
-(defun proof-locate-executable 924,35582
+(defun pg-remove-specials 439,15846
+(defun pg-remove-specials-in-string 449,16184
+(defun proof-fontify-buffer 456,16371
+(defun proof-warn-if-unset 469,16612
+(defun proof-get-window-for-buffer 474,16830
+(defun proof-display-and-keep-buffer 525,19138
+(defun proof-clean-buffer 557,20445
+(defun proof-message 572,21066
+(defun proof-warning 577,21279
+(defun pg-internal-warning 583,21561
+(defun proof-debug 591,21880
+(defun proof-switch-to-buffer 606,22551
+(defun proof-resize-window-tofit 639,24240
+(defun proof-submit-bug-report 739,28252
+(defun proof-deftoggle-fn 775,29631
+(defmacro proof-deftoggle 790,30284
+(defun proof-defintset-fn 797,30658
+(defmacro proof-defintset 813,31362
+(defun proof-defstringset-fn 820,31739
+(defmacro proof-defstringset 833,32365
+(defmacro proof-defshortcut 847,32822
+(defmacro proof-definvisible 862,33461
+(defun pg-custom-save-vars 890,34438
+(defun pg-custom-reset-vars 908,35161
+(defun proof-locate-executable 921,35498
 
 generic/proof-x-symbol.el,580
 (defvar proof-x-symbol-initialized 52,2006
@@ -2343,26 +2340,26 @@ lib/pg-dev.el,75
 (defconst pg-dev-lisp-font-lock-keywords35,1049
 (defun unload-pg 69,1986
 
-lib/proof-compat.el,748
+lib/proof-compat.el,751
 (defvar proof-running-on-win32 29,914
 (defun pg-custom-undeclare-variable 41,1371
-(defun subst-char-in-string 103,3016
-(defun replace-regexp-in-string 118,3605
-(defconst menuvisiblep 180,6318
-(defun set-window-text-height 197,6931
-(defmacro save-selected-frame 223,7881
-(defun warn 262,9178
-(defun redraw-modeline 269,9433
-(defun proof-buffer-syntactic-context-emulate 280,9871
-(defvar read-shell-command-map313,11178
-(defun read-shell-command 331,11866
-(defun remassq 343,12347
-(defun remassoc 355,12736
-(defun frames-of-buffer 368,13181
-(defmacro with-selected-window 407,14443
-(defun pg-pop-to-buffer 450,15821
-(defun process-live-p 501,17654
-(defalias 'proof-buffer-syntactic-context proof-buffer-syntactic-context
518,18157
+(defun subst-char-in-string 131,4159
+(defun replace-regexp-in-string 146,4748
+(defconst menuvisiblep 208,7461
+(defun set-window-text-height 225,8074
+(defmacro save-selected-frame 251,9024
+(defun warn 290,10321
+(defun redraw-modeline 297,10576
+(defun proof-buffer-syntactic-context-emulate 308,11014
+(defvar read-shell-command-map341,12321
+(defun read-shell-command 359,13009
+(defun remassq 371,13490
+(defun remassoc 383,13879
+(defun frames-of-buffer 396,14324
+(defmacro with-selected-window 435,15586
+(defun pg-pop-to-buffer 478,16964
+(defun process-live-p 529,18797
+(defalias 'proof-buffer-syntactic-context proof-buffer-syntactic-context
546,19300
 
 lib/span.el,137
 (defsubst span-delete-spans 22,479
@@ -2456,6 +2453,28 @@ lib/unicode-chars.el,80
 (defvar unicode-chars-alist12,348
 (defun unicode-chars-list-chars 5050,245960
 
+lib/unicode-tokens.el,938
+(defvar unicode-tokens-charref-format 50,1715
+(defvar unicode-tokens-token-format 53,1812
+(defvar unicode-tokens-token-name-alist 56,1903
+(defvar unicode-tokens-glyph-list 59,2004
+(defvar unicode-tokens-token-prefix 63,2148
+(defvar unicode-tokens-token-suffix 66,2232
+(defvar unicode-tokens-token-match 69,2314
+(defvar unicode-tokens-hexcode-match 72,2399
+(defvar unicode-tokens-token-codept-alist 80,2569
+(defvar unicode-tokens-max-token-length 83,2667
+(defun unicode-tokens-insert-char 91,2784
+(defun unicode-tokens-character-insert 101,3205
+(defun unicode-tokens-token-insert 123,4113
+(defun unicode-tokens-replace-token-after 146,5099
+(defun unicode-tokens-looking-backward-at 168,5827
+(defun unicode-tokens-electric-suffix 179,6289
+(defun unicode-tokens-quail-define-rules 261,8641
+(defvar unicode-tokens-mode-map 292,9671
+(define-minor-mode unicode-tokens-mode295,9768
+(defun unicode-tokens-initialise 316,10395
+
 lib/xml-fixed.el,528
 (defsubst xml-node-name 82,2904
 (defsubst xml-node-attributes 87,3023
@@ -2771,7 +2790,7 @@ x-symbol/lisp/x-symbol-bib.el,549
 (defvar x-symbol-bib-generated-data 113,4390
 (defun x-symbol-bib-default-token-list 117,4529
 
-x-symbol/lisp/x-symbol.el,9173
+x-symbol/lisp/x-symbol.el,9210
 (defvar x-symbol-trace-invisible 51,1979
 (defconst x-symbol-language-access-alist66,2494
 (defstruct (x-symbol-generated178,8375
@@ -2827,186 +2846,187 @@ x-symbol/lisp/x-symbol.el,9173
 (defun x-symbol-decode-lisp 865,36110
 (defun x-symbol-encode-string 897,37577
 (defun x-symbol-encode-all 908,37896
-(defun x-symbol-encode-lisp 970,40852
-(defun x-symbol-decode-recode 1006,42257
-(defun x-symbol-decode 1036,43633
-(defun x-symbol-encode-recode 1049,44224
-(defun x-symbol-encode 1077,45500
-(defun x-symbol-unalias 1093,46259
-(defun x-symbol-copy-region-encoded 1158,49178
-(defun x-symbol-yank-decoded 1186,50428
-(defun x-symbol-update-modeline 1213,51528
-(defun x-symbol-auto-coding-alist 1237,52383
-(defun x-symbol-auto-8bit-search 1273,53544
-(defvar x-symbol-font-family-postfixes1298,54334
-(defvar x-symbol-font-lock-property-alist1301,54450
-(defvar x-symbol-font-lock-keywords1305,54631
-(defvar x-symbol-subscript-matcher 1332,55626
-(defvar x-symbol-subscript-type 1336,55729
-(defun x-symbol-subscripts-available-p 1339,55780
-(defun x-symbol-font-lock-start 1345,56021
-(defun x-symbol-match-subscript 1354,56407
-(defun x-symbol-init-font-lock 1360,56620
-(defun x-symbol-set-image 1392,58208
-(defun x-symbol-mode-internal 1410,58954
-(defun nuke-x-symbol 1484,62057
-(defun x-symbol-options-filter 1497,62510
-(defun x-symbol-extra-filter 1533,63666
-(defun x-symbol-menu-filter 1541,63914
-(defvar x-symbol-list-mode-map1568,64751
-(defvar x-symbol-list-buffer 1594,65901
-(defvar x-symbol-list-win-config 1596,65977
-(defvar x-symbol-invisible-spec 1598,66088
-(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 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
+(defun x-symbol-encode-lisp 972,40931
+(defun x-symbol-decode-recode 1008,42336
+(defun x-symbol-decode 1038,43712
+(defun x-symbol-encode-recode 1051,44303
+(defun x-symbol-encode 1079,45579
+(defun x-symbol-unalias 1095,46338
+(defun x-symbol-copy-region-encoded 1160,49257
+(defun x-symbol-yank-decoded 1188,50507
+(defun x-symbol-update-modeline 1215,51607
+(defun x-symbol-auto-coding-alist 1239,52462
+(defun x-symbol-auto-8bit-search 1275,53623
+(defvar x-symbol-font-family-postfixes1300,54413
+(defvar x-symbol-font-lock-property-alist1303,54529
+(defvar x-symbol-font-lock-keywords1307,54710
+(defvar x-symbol-subscript-matcher 1334,55705
+(defvar x-symbol-subscript-type 1338,55808
+(defun x-symbol-subscripts-available-p 1341,55859
+(defun x-symbol-font-lock-start 1347,56100
+(defun x-symbol-match-subscript 1356,56486
+(defun x-symbol-init-font-lock 1362,56699
+(defun x-symbol-set-image 1394,58287
+(defun x-symbol-mode-internal 1412,59033
+(defun nuke-x-symbol 1486,62136
+(defun x-symbol-options-filter 1499,62589
+(defun x-symbol-extra-filter 1535,63745
+(defun x-symbol-menu-filter 1543,63993
+(defvar x-symbol-list-mode-map1573,64972
+(defvar x-symbol-list-buffer 1599,66122
+(defvar x-symbol-list-win-config 1601,66198
+(defvar x-symbol-invisible-spec 1603,66309
+(defvar x-symbol-itimer 1607,66459
+(defvar x-symbol-invisible-display-table1610,66542
+(defvar x-symbol-invisible-font 1619,66778
+(defvar x-symbol-charsym-info-cache 1644,67965
+(defvar x-symbol-language-info-caches 1646,68056
+(defvar x-symbol-coding-info-cache 1648,68150
+(defvar x-symbol-keys-info-cache 1650,68239
+(defun x-symbol-list-bury 1658,68544
+(defun x-symbol-list-restore 1664,68740
+(defun x-symbol-list-store 1694,69958
+(defun x-symbol-list-mode 1703,70375
+(defun x-symbol-list-scroll 1724,71177
+(defun x-symbol-init-language-interactive 1747,71819
+(defun x-symbol-list-menu 1764,72533
+(defun x-symbol-list-selected 1819,74441
+(defun x-symbol-list-menu-selected 1845,75650
+(defun x-symbol-list-mouse-selected 1856,76103
+(defun x-symbol-charsym-info 1873,76825
+(defun x-symbol-language-info 1887,77426
+(defun x-symbol-coding-info 1919,78626
+(defun x-symbol-keys-info 1939,79398
+(defun x-symbol-info 1963,80321
+(defun x-symbol-list-info 1976,80859
+(defun x-symbol-highlight-echo 1990,81402
+(defun x-symbol-point-info 2001,81951
+(defun x-symbol-hide-revealed-at-point 2047,83873
+(defun x-symbol-reveal-invisible 2084,85540
+(defun x-symbol-show-info-and-invisible 2132,87732
+(defun x-symbol-start-itimer-once 2168,89274
+(defun x-symbol-setup-minibuffer 2184,89900
+(defvar x-symbol-language-history 2202,90471
+(defvar x-symbol-token-history 2205,90595
+(defvar x-symbol-last-abbrev 2208,90671
+(defvar x-symbol-electric-pos 2210,90767
+(defvar x-symbol-command-keys 2213,90849
+(defvar x-symbol-help-keys 2217,90980
+(defvar x-symbol-help-language 2219,91075
+(defvar x-symbol-help-completions 2221,91174
+(defvar x-symbol-help-completions1 2223,91266
+(defun x-symbol-map-default-binding 2231,91542
+(defun x-symbol-read-charsym-token 2262,92620
+(defun x-symbol-insert-command 2288,93543
+(defun x-symbol-read-language 2339,95550
+(defun x-symbol-read-token 2354,96228
+(defun x-symbol-read-token-direct 2393,97737
+(defun x-symbol-grid 2405,98137
+(defun x-symbol-replace-from 2493,101753
+(defvar x-symbol-token-search-prelude-size 2529,103254
+(defun x-symbol-replace-token 2531,103302
+(defun x-symbol-match-token-before 2556,104393
+(defun x-symbol-token-input 2600,106196
+(defun x-symbol-modify-key 2621,107026
+(defun x-symbol-rotate-key 2654,108355
+(defun x-symbol-electric-input 2708,110565
+(defun x-symbol-help-mapper 2750,112266
+(defun x-symbol-help-output 2773,113105
+(defun x-symbol-help 2816,114701
+(defvar x-symbol-face-docstrings2869,116770
+(defvar x-symbol-all-key-prefixes 2875,116958
+(defvar x-symbol-all-key-chain-alist 2877,117069
+(defvar x-symbol-all-horizontal-chain-alist 2879,117168
+(defvar x-symbol-all-chain-subchains-alist 2881,117281
+(defvar x-symbol-all-exclusive-context-alist 2883,117395
+(defalias 'x-symbol-table-grouping x-symbol-table-grouping
2891,117691
+(defalias 'x-symbol-table-aspects x-symbol-table-aspects
2892,117732
+(defalias 'x-symbol-table-score x-symbol-table-score
2893,117773
+(defalias 'x-symbol-table-input x-symbol-table-input
2894,117813
+(defsubst x-symbol-table-prefixes 2895,117854
+(defsubst x-symbol-table-junk 2896,117905
+(defsubst x-symbol-charsym-defined-p 2898,117956
+(defun x-symbol-try-font-name-0 2906,118257
+(defun x-symbol-try-font-name 2924,118813
+(defun x-symbol-set-cstrings 2941,119329
+(defun x-symbol-init-charsym-command 2986,121307
+(defun x-symbol-init-charsym-input 2994,121673
+(defun x-symbol-init-charsym-aspects 3063,124391
+(defun x-symbol-init-cset 3093,125671
+(defun x-symbol-make-atree 3243,132494
+(defun x-symbol-atree-push 3247,132574
+(defun x-symbol-component-root-p 3267,133263
+(defun x-symbol-component-elements 3271,133402
+(defun x-symbol-component-merge 3278,133650
+(defun x-symbol-component-space 3292,134198
+(defun x-symbol-modify-less-than 3306,134782
+(defun x-symbol-inherit-aspects 3311,135005
+(defun x-symbol-compute-aspects 3320,135444
+(defun x-symbol-init-aspects 3336,136162
+(defun x-symbol-sort-modify-chain 3381,138211
+(defun x-symbol-init-horizontal/key-alist 3396,138783
+(defun x-symbol-init-exclusive-alist 3412,139529
+(defun x-symbol-init-horizontal-chain 3450,141133
+(defun x-symbol-init-exclusive-chain 3458,141465
+(defun x-symbol-init-rotate-chain 3465,141792
+(defun x-symbol-init-context-atree 3486,142666
+(defun x-symbol-init-key-bindings 3531,144949
+(defun x-symbol-rotate-modify-less-than 3554,145872
+(defun x-symbol-subgroup-less-than 3562,146267
+(defun x-symbol-header-charsyms 3567,146524
+(defun x-symbol-init-grid/menu 3593,147574
+(defun x-symbol-init-input 3665,150230
+(defun x-symbol-init-latin-decoding 3795,156706
+(defun x-symbol-get-prime-for 3836,158577
+(defun x-symbol-alist-to-obarray 3845,158901
+(defun x-symbol-alist-to-hash-table 3851,159109
+(defun x-symbol-init-language 3861,159442
+(defvar x-symbol-latin1-cset3985,164907
+(defvar x-symbol-latin2-cset3991,165080
+(defvar x-symbol-latin3-cset3997,165253
+(defvar x-symbol-latin5-cset4003,165426
+(defvar x-symbol-latin9-cset4009,165598
+(defvar x-symbol-xsymb0-cset4015,165804
+(defvar x-symbol-xsymb1-cset4021,166059
+(defvar x-symbol-latin1-table4027,166301
+(defvar x-symbol-latin2-table4128,170771
+(defvar x-symbol-latin3-table4227,173972
+(defvar x-symbol-latin5-table4326,176853
+(defvar x-symbol-latin9-table4425,179163
+(defvar x-symbol-xsymb0-table4524,181553
+(defvar x-symbol-xsymb1-table4674,188949
+(defvar x-symbol-no-of-charsyms 4882,199584
+(defun x-symbol-mac-setup1 4890,199950
+(defun x-symbol-mac-setup2 4916,200859
+(defun x-symbol-startup 4934,201525
 
 x-symbol/lisp/x-symbol-emacs.el,1126
-(defun emacs-version>=34,1341
-(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
+(defun emacs-version>=33,1289
+(defvar x-symbol-emacs-has-font-lock-with-props67,2953
+(defvar x-symbol-emacs-has-correct-find-safe-coding87,3682
+(defvar x-symbol-emacs-after-create-image-function102,4196
+(defvar image-types 128,5053
+(defvar init-file-loaded 164,6440
+(defvar message-stack 167,6513
+(defun region-active-p 250,9823
+(defvar x-symbol-data-directory 287,11188
+(defun x-symbol-directory-files 357,13465
+(defun x-symbol-event-in-current-buffer 371,13853
+(defun x-symbol-create-image 374,13902
+(defun x-symbol-make-glyph 377,13987
+(defun x-symbol-set-glyph-image 380,14058
+(defvar x-symbol-heading-strut-glyph 395,14555
+(defvar x-symbol-invisible-face 398,14642
+(defvar x-symbol-face 399,14700
+(defvar x-symbol-sub-face 400,14738
+(defvar x-symbol-sup-face 401,14784
+(defvar x-symbol-emacs-w32-font-directories403,14831
+(defvar x-symbol-invisible-display-table 416,15309
+(defalias 'x-symbol-window-width x-symbol-window-width
418,15356
+(defun x-symbol-set-face-font 429,15852
+(defun x-symbol-event-matches-key-specifier-p 440,16325
+(defun start-itimer 450,16597
+(defun itimer-live-p 452,16694
 
 x-symbol/lisp/x-symbol-hooks.el,3109
 (defvar x-symbol-warn-of-old-emacs 66,2522
@@ -3306,14 +3326,14 @@ x-symbol/lisp/x-symbol-unichars.el,99
 (defvar x-symbol-unicode-character-list5,115
 (defun x-symbol-list-unicode-characters 5044,235676
 
-x-symbol/lisp/x-symbol-unicode.el,170
-(defconst x-symbol-xsym-unicode-map	12,383
-(defconst x-symbol-old-tables 260,9819
-(defconst x-symbol-unicode-table 276,10252
-(defconst x-symbol-unicode-cset292,10757
+x-symbol/lisp/x-symbol-unicode.el,168
+(defconst x-symbol-xsym-unicode-map	18,546
+(defconst x-symbol-old-tables266,9981
+(defconst x-symbol-unicode-table282,10412
+(defconst x-symbol-unicode-cset298,10915
 
-x-symbol/lisp/x-symbol-unicode-extras.el,38
-(defconst x-symol-unicode-extras 2,1
+x-symbol/lisp/x-symbol-unicode-extras.el,40
+(defconst x-symol-unicode-extras13,263
 
 x-symbol/lisp/x-symbol-vars.el,8058
 (defconst x-symbol-version 40,1516
@@ -3652,20 +3672,32 @@ x-symbol/lisp/custom-load.el,0
 
 lib/holes-load.el,0
 
+generic/test.el,0
+
 generic/proof.el,0
 
 generic/proof-autoloads.el,0
 
+generic/pg-cmdhist.el,0
+
+generic/comptest.el,0
+
 twelf/x-symbol-twelf.el,0
 
 pgshell/pgshell.el,0
 
 lego/x-symbol-lego.el,0
 
+isar/test.el,0
+
+isar/isar-templates.el,0
+
 isar/isar-autotest.el,0
 
 isar/interface-setup.el,0
 
+isar/comptest.el,0
+
 hol98/x-symbol-hol98.el,0
 
 hol98/hol98.el,0