Updated

1 files changed, 356 insertions, 345 deletions

diff --git a/TAGS b/TAGS
index 2196eecb..5f1aed34 100644
--- a/TAGS
+++ b/TAGS
@@ -1093,85 +1093,85 @@ generic/pg-thymodes.el,152
 (defun pg-modesym 82,2548
 (defun pg-modesymval 86,2662
 
-generic/pg-user.el,3331
+generic/pg-user.el,3332
 (defun proof-script-new-command-advance 41,1156
 (defun proof-maybe-follow-locked-end 84,2897
-(defun proof-goto-command-start 111,3726
-(defun proof-goto-command-end 134,4666
-(defun proof-goto-point 157,5191
-(defun proof-assert-next-command-interactive 171,5625
-(defun proof-assert-until-point-interactive 184,6150
-(defun proof-process-buffer 190,6380
-(defun proof-undo-last-successful-command 205,6757
-(defun proof-undo-and-delete-last-successful-command 210,6919
-(defun proof-undo-last-successful-command-1 223,7473
-(defun proof-retract-buffer 240,8085
-(defun proof-retract-current-goal 249,8369
-(defun proof-mouse-goto-point 268,8889
-(defvar proof-minibuffer-history 283,9165
-(defun proof-minibuffer-cmd 286,9260
-(defun proof-frob-locked-end 330,10882
-(defmacro proof-if-setting-configured 391,12806
-(defmacro proof-define-assistant-command 399,13075
-(defmacro proof-define-assistant-command-witharg 412,13530
-(defun proof-issue-new-command 432,14352
-(defun proof-cd-sync 478,15849
-(defun proof-electric-terminator-enable 532,17569
-(defun proof-electric-terminator 540,17859
-(defun proof-add-completions 562,18504
-(defun proof-script-complete 587,19411
-(defun pg-copy-span-contents 601,19720
-(defun pg-numth-span-higher-or-lower 618,20278
-(defun pg-control-span-of 644,21024
-(defun pg-move-span-contents 650,21228
-(defun pg-fixup-children-spans 702,23404
-(defun pg-move-region-down 712,23661
-(defun pg-move-region-up 721,23954
-(defun proof-forward-command 751,24782
-(defun proof-backward-command 772,25503
-(defun pg-pos-for-event 794,25847
-(defun pg-span-for-event 800,26068
-(defun pg-span-context-menu 804,26212
-(defun pg-toggle-visibility 819,26667
-(defun pg-create-in-span-context-menu 829,26989
-(defun pg-span-undo 859,28198
-(defun pg-goals-buffers-hint 905,29600
-(defun pg-slow-fontify-tracing-hint 909,29782
-(defun pg-response-buffers-hint 913,29953
-(defun pg-jump-to-end-hint 923,30315
-(defun pg-processing-complete-hint 927,30444
-(defun pg-next-error-hint 944,31143
-(defun pg-hint 949,31295
-(defun pg-identifier-under-mouse-query 965,31885
-(defun pg-identifier-near-point-query 974,32128
-(defvar proof-query-identifier-collection 999,32844
-(defvar proof-query-identifier-history 1000,32891
-(defun proof-query-identifier 1002,32936
-(defun pg-identifier-query 1012,33205
-(defun proof-imenu-enable 1043,34283
-(defvar pg-input-ring 1079,35605
-(defvar pg-input-ring-index 1082,35662
-(defvar pg-stored-incomplete-input 1085,35734
-(defun pg-previous-input 1088,35837
-(defun pg-next-input 1102,36294
-(defun pg-delete-input 1107,36416
-(defun pg-get-old-input 1120,36754
-(defun pg-restore-input 1134,37145
-(defun pg-search-start 1145,37435
-(defun pg-regexp-arg 1157,37927
-(defun pg-search-arg 1169,38375
-(defun pg-previous-matching-input-string-position 1183,38792
-(defun pg-previous-matching-input 1210,39957
-(defun pg-next-matching-input 1229,40807
-(defvar pg-matching-input-from-input-string 1237,41190
-(defun pg-previous-matching-input-from-input 1241,41304
-(defun pg-next-matching-input-from-input 1259,42069
-(defun pg-add-to-input-history 1270,42448
-(defun pg-remove-from-input-history 1282,42901
-(defun  pg-clear-input-ring 1293,43281
-(define-key proof-mode-map 1307,43631
-(define-key proof-mode-map 1308,43691
-(defun pg-protected-undo 1310,43763
+(defun proof-goto-command-start 111,3745
+(defun proof-goto-command-end 134,4685
+(defun proof-goto-point 157,5210
+(defun proof-assert-next-command-interactive 171,5644
+(defun proof-assert-until-point-interactive 183,6130
+(defun proof-process-buffer 189,6360
+(defun proof-undo-last-successful-command 204,6737
+(defun proof-undo-and-delete-last-successful-command 209,6899
+(defun proof-undo-last-successful-command-1 222,7453
+(defun proof-retract-buffer 239,8065
+(defun proof-retract-current-goal 248,8349
+(defun proof-mouse-goto-point 267,8869
+(defvar proof-minibuffer-history 282,9145
+(defun proof-minibuffer-cmd 285,9240
+(defun proof-frob-locked-end 329,10862
+(defmacro proof-if-setting-configured 390,12786
+(defmacro proof-define-assistant-command 398,13055
+(defmacro proof-define-assistant-command-witharg 411,13510
+(defun proof-issue-new-command 431,14332
+(defun proof-cd-sync 477,15829
+(defun proof-electric-terminator-enable 531,17549
+(defun proof-electric-terminator 539,17839
+(defun proof-add-completions 561,18484
+(defun proof-script-complete 586,19391
+(defun pg-copy-span-contents 600,19700
+(defun pg-numth-span-higher-or-lower 617,20258
+(defun pg-control-span-of 643,21004
+(defun pg-move-span-contents 649,21208
+(defun pg-fixup-children-spans 701,23384
+(defun pg-move-region-down 711,23641
+(defun pg-move-region-up 720,23934
+(defun proof-forward-command 750,24762
+(defun proof-backward-command 771,25483
+(defun pg-pos-for-event 793,25827
+(defun pg-span-for-event 799,26048
+(defun pg-span-context-menu 803,26192
+(defun pg-toggle-visibility 818,26647
+(defun pg-create-in-span-context-menu 828,26969
+(defun pg-span-undo 858,28178
+(defun pg-goals-buffers-hint 904,29580
+(defun pg-slow-fontify-tracing-hint 908,29762
+(defun pg-response-buffers-hint 912,29933
+(defun pg-jump-to-end-hint 922,30295
+(defun pg-processing-complete-hint 926,30424
+(defun pg-next-error-hint 943,31123
+(defun pg-hint 948,31275
+(defun pg-identifier-under-mouse-query 964,31865
+(defun pg-identifier-near-point-query 973,32108
+(defvar proof-query-identifier-collection 1000,32951
+(defvar proof-query-identifier-history 1001,32998
+(defun proof-query-identifier 1003,33043
+(defun pg-identifier-query 1013,33312
+(defun proof-imenu-enable 1044,34390
+(defvar pg-input-ring 1080,35712
+(defvar pg-input-ring-index 1083,35769
+(defvar pg-stored-incomplete-input 1086,35841
+(defun pg-previous-input 1089,35944
+(defun pg-next-input 1103,36401
+(defun pg-delete-input 1108,36523
+(defun pg-get-old-input 1121,36861
+(defun pg-restore-input 1135,37252
+(defun pg-search-start 1146,37542
+(defun pg-regexp-arg 1158,38034
+(defun pg-search-arg 1170,38482
+(defun pg-previous-matching-input-string-position 1184,38899
+(defun pg-previous-matching-input 1211,40064
+(defun pg-next-matching-input 1230,40914
+(defvar pg-matching-input-from-input-string 1238,41297
+(defun pg-previous-matching-input-from-input 1242,41411
+(defun pg-next-matching-input-from-input 1260,42176
+(defun pg-add-to-input-history 1271,42555
+(defun pg-remove-from-input-history 1283,43008
+(defun  pg-clear-input-ring 1294,43388
+(define-key proof-mode-map 1308,43738
+(define-key proof-mode-map 1309,43798
+(defun pg-protected-undo 1311,43870
 
 generic/pg-vars.el,1452
 (defvar proof-assistant-cusgrp 22,382
@@ -1244,7 +1244,7 @@ generic/pg-xml.el,1177
 (defun pg-pgip-get-pgmltext 223,7251
 
 generic/proof-autoloads.el,45
-(defsubst proof-shell-live-buffer 639,20962
+(defsubst proof-shell-live-buffer 639,21040
 
 generic/proof-auxmodes.el,149
 (defun proof-mmm-support-available 20,489
@@ -1499,46 +1499,46 @@ generic/proof-menu.el,2026
 (defvar proof-buffer-menu243,8510
 (defun proof-keep-response-history 305,10779
 (defconst proof-quick-opts-menu313,11089
-(defun proof-quick-opts-vars 496,18562
-(defun proof-quick-opts-changed-from-defaults-p 525,19422
-(defun proof-quick-opts-changed-from-saved-p 529,19527
-(defun proof-quick-opts-save 540,19878
-(defun proof-quick-opts-reset 545,20046
-(defconst proof-config-menu557,20314
-(defconst proof-advanced-menu564,20493
-(defvar proof-menu577,20928
-(defun proof-main-menu 586,21210
-(defun proof-aux-menu 597,21476
-(defun proof-menu-define-favourites-menu 613,21822
-(defun proof-def-favourite 633,22471
-(defvar proof-make-favourite-cmd-history 656,23445
-(defvar proof-make-favourite-menu-history 659,23530
-(defun proof-save-favourites 662,23616
-(defun proof-del-favourite 667,23764
-(defun proof-read-favourite 684,24320
-(defun proof-add-favourite 708,25096
-(defun proof-menu-define-settings-menu 735,26141
-(defun proof-menu-entry-name 768,27262
-(defun proof-menu-entry-for-setting 778,27612
-(defun proof-settings-vars 797,28144
-(defun proof-settings-changed-from-defaults-p 802,28321
-(defun proof-settings-changed-from-saved-p 806,28427
-(defun proof-settings-save 810,28530
-(defun proof-settings-reset 815,28697
-(defun proof-assistant-invisible-command-ifposs 820,28860
-(defun proof-maybe-askprefs 842,29830
-(defun proof-assistant-settings-cmd 848,30022
-(defvar proof-assistant-format-table865,30677
-(defun proof-assistant-format-bool 873,31045
-(defun proof-assistant-format-int 876,31158
-(defun proof-assistant-format-string 879,31250
-(defun proof-assistant-format 882,31348
+(defun proof-quick-opts-vars 500,18727
+(defun proof-quick-opts-changed-from-defaults-p 529,19587
+(defun proof-quick-opts-changed-from-saved-p 533,19692
+(defun proof-quick-opts-save 544,20043
+(defun proof-quick-opts-reset 549,20211
+(defconst proof-config-menu561,20479
+(defconst proof-advanced-menu568,20658
+(defvar proof-menu581,21090
+(defun proof-main-menu 590,21372
+(defun proof-aux-menu 602,21711
+(defun proof-menu-define-favourites-menu 618,22057
+(defun proof-def-favourite 638,22706
+(defvar proof-make-favourite-cmd-history 661,23680
+(defvar proof-make-favourite-menu-history 664,23765
+(defun proof-save-favourites 667,23851
+(defun proof-del-favourite 672,23999
+(defun proof-read-favourite 689,24555
+(defun proof-add-favourite 713,25331
+(defun proof-menu-define-settings-menu 740,26376
+(defun proof-menu-entry-name 773,27497
+(defun proof-menu-entry-for-setting 783,27847
+(defun proof-settings-vars 802,28379
+(defun proof-settings-changed-from-defaults-p 807,28556
+(defun proof-settings-changed-from-saved-p 811,28662
+(defun proof-settings-save 815,28765
+(defun proof-settings-reset 820,28932
+(defun proof-assistant-invisible-command-ifposs 825,29095
+(defun proof-maybe-askprefs 847,30065
+(defun proof-assistant-settings-cmd 853,30257
+(defvar proof-assistant-format-table870,30912
+(defun proof-assistant-format-bool 878,31280
+(defun proof-assistant-format-int 881,31393
+(defun proof-assistant-format-string 884,31485
+(defun proof-assistant-format 887,31583
 
 generic/proof-mmm.el,70
 (defun proof-mmm-set-global 39,1466
 (defun proof-mmm-enable 54,2005
 
-generic/proof-script.el,5552
+generic/proof-script.el,5559
 (deflocal proof-active-buffer-fake-minor-mode 44,1308
 (deflocal proof-script-buffer-file-name 47,1434
 (deflocal pg-script-portions 54,1844
@@ -1565,101 +1565,101 @@ generic/proof-script.el,5552
 (defun proof-script-buffers-with-spans 281,10164
 (defun proof-script-remove-all-spans-and-deactivate 291,10520
 (defun proof-script-clear-queue-spans-on-error 295,10710
-(defun proof-script-delete-spans 311,11287
-(defun proof-script-delete-secondary-spans 316,11486
-(defun proof-unprocessed-begin 328,11774
-(defun proof-script-end 336,12028
-(defun proof-queue-or-locked-end 345,12331
-(defun proof-locked-end 360,13009
-(defun proof-locked-region-full-p 374,13290
-(defun proof-locked-region-empty-p 383,13562
-(defun proof-only-whitespace-to-locked-region-p 387,13712
-(defun proof-in-locked-region-p 397,14039
-(defun proof-goto-end-of-locked 409,14296
-(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 426,15055
-(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 437,15536
-(defun proof-end-of-locked-visible-p 451,16149
-(defvar pg-idioms 469,16767
-(defvar pg-visibility-specs 472,16863
-(defconst pg-default-invisibility-spec477,17070
-(defun pg-clear-script-portions 480,17139
-(defun pg-remove-script-element 487,17413
-(defsubst pg-visname 492,17602
-(defun pg-add-element 496,17747
-(defun pg-open-invisible-span 532,19440
-(defun pg-remove-element 543,19803
-(defun pg-make-element-invisible 550,20073
-(defun pg-make-element-visible 556,20317
-(defun pg-toggle-element-visibility 560,20460
-(defun pg-redisplay-for-gnuemacs 567,20747
-(defun pg-show-all-portions 571,20894
-(defun pg-show-all-proofs 591,21612
-(defun pg-hide-all-proofs 596,21740
-(defun pg-add-proof-element 601,21871
-(defun pg-span-name 616,22592
-(defvar pg-span-context-menu-keymap637,23292
-(defun pg-last-output-displayform 644,23530
-(defun pg-set-span-helphighlights 660,24156
-(defun proof-complete-buffer-atomic 707,25859
-(defun proof-register-possibly-new-processed-file749,27779
-(defun proof-inform-prover-file-retracted 795,29616
-(defun proof-auto-retract-dependencies 815,30467
-(defun proof-unregister-buffer-file-name 869,33017
-(defun proof-protected-process-or-retract 915,34842
-(defun proof-deactivate-scripting-auto 942,36012
-(defun proof-deactivate-scripting 951,36370
-(defun proof-activate-scripting 1084,41626
-(defun proof-toggle-active-scripting 1199,46744
-(defun proof-done-advancing 1238,47989
-(defun proof-done-advancing-comment 1317,50974
-(defun proof-done-advancing-save 1351,52350
-(defun proof-make-goalsave 1439,55715
-(defun proof-get-name-from-goal 1457,56547
-(defun proof-done-advancing-autosave 1477,57572
-(defun proof-done-advancing-other 1542,60116
-(defun proof-segment-up-to-parser 1570,61069
-(defun proof-script-generic-parse-find-comment-end 1640,63344
-(defun proof-script-generic-parse-cmdend 1649,63758
-(defun proof-script-generic-parse-cmdstart 1674,64645
-(defun proof-script-generic-parse-sexp 1737,67338
-(defun proof-cmdstart-add-segment-for-cmd 1761,68270
-(defun proof-segment-up-to-cmdstart 1812,70328
-(defun proof-segment-up-to-cmdend 1873,72688
-(defun proof-semis-to-vanillas 1945,75367
-(defun proof-script-next-command-advance 1994,76889
-(defun proof-assert-until-point 2013,77388
-(defun proof-assert-electric-terminator 2028,77981
-(defun proof-assert-semis 2062,79323
-(defun proof-retract-before-change 2075,79962
-(defun proof-inside-comment 2084,80280
-(defun proof-insert-pbp-command 2099,80563
-(defun proof-insert-sendback-command 2114,81057
-(defun proof-done-retracting 2140,81960
-(defun proof-setup-retract-action 2175,83401
-(defun proof-last-goal-or-goalsave 2185,83887
-(defun proof-retract-target 2209,84792
-(defun proof-retract-until-point-interactive 2292,88306
-(defun proof-retract-until-point 2300,88691
-(define-derived-mode proof-mode 2347,90526
-(defun proof-script-set-visited-file-name 2384,91894
-(defun proof-script-set-buffer-hooks 2406,92907
-(defun proof-script-kill-buffer-fn 2414,93325
-(defun proof-config-done-related 2446,94642
-(defun proof-generic-goal-command-p 2514,97165
-(defun proof-generic-state-preserving-p 2519,97378
-(defun proof-generic-count-undos 2528,97895
-(defun proof-generic-find-and-forget 2557,98933
-(defconst proof-script-important-settings2610,100772
-(defun proof-config-done 2625,101318
-(defun proof-setup-parsing-mechanism 2693,103596
-(defun proof-setup-imenu 2737,105449
-(deflocal proof-segment-up-to-cache 2761,106223
-(deflocal proof-segment-up-to-cache-start 2762,106264
-(deflocal proof-last-edited-low-watermark 2763,106309
-(defun proof-segment-up-to-using-cache 2773,106796
-(defun proof-segment-cache-contents-for 2802,107944
-(defun proof-script-after-change-function 2814,108313
-(defun proof-script-set-after-change-functions 2826,108820
+(defun proof-script-delete-spans 316,11511
+(defun proof-script-delete-secondary-spans 321,11710
+(defun proof-unprocessed-begin 333,11998
+(defun proof-script-end 341,12252
+(defun proof-queue-or-locked-end 350,12555
+(defun proof-locked-end 365,13233
+(defun proof-locked-region-full-p 379,13514
+(defun proof-locked-region-empty-p 388,13786
+(defun proof-only-whitespace-to-locked-region-p 392,13936
+(defun proof-in-locked-region-p 402,14263
+(defun proof-goto-end-of-locked 414,14520
+(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 431,15279
+(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 442,15760
+(defun proof-end-of-locked-visible-p 456,16373
+(defvar pg-idioms 474,16991
+(defvar pg-visibility-specs 477,17087
+(defconst pg-default-invisibility-spec484,17345
+(defun pg-clear-script-portions 487,17414
+(defun pg-remove-script-element 494,17688
+(defsubst pg-visname 499,17877
+(defun pg-add-element 503,18022
+(defun pg-open-invisible-span 539,19712
+(defun pg-remove-element 550,20075
+(defun pg-make-element-invisible 556,20315
+(defun pg-make-element-visible 562,20559
+(defun pg-toggle-element-visibility 568,20810
+(defun pg-show-all-portions 574,21067
+(defun pg-show-all-proofs 595,21843
+(defun pg-hide-all-proofs 600,21971
+(defun pg-add-proof-element 605,22102
+(defun pg-span-name 620,22829
+(defvar pg-span-context-menu-keymap641,23529
+(defun pg-last-output-displayform 648,23767
+(defun pg-set-span-helphighlights 666,24463
+(defun pg-delete-self-modification-hook 707,26163
+(defun proof-complete-buffer-atomic 718,26436
+(defun proof-register-possibly-new-processed-file760,28356
+(defun proof-inform-prover-file-retracted 806,30193
+(defun proof-auto-retract-dependencies 826,31044
+(defun proof-unregister-buffer-file-name 880,33594
+(defun proof-protected-process-or-retract 926,35419
+(defun proof-deactivate-scripting-auto 953,36589
+(defun proof-deactivate-scripting 962,36947
+(defun proof-activate-scripting 1095,42203
+(defun proof-toggle-active-scripting 1210,47321
+(defun proof-done-advancing 1249,48566
+(defun proof-done-advancing-comment 1328,51551
+(defun proof-done-advancing-save 1362,52927
+(defun proof-make-goalsave 1450,56292
+(defun proof-get-name-from-goal 1468,57124
+(defun proof-done-advancing-autosave 1488,58149
+(defun proof-done-advancing-other 1553,60693
+(defun proof-segment-up-to-parser 1581,61646
+(defun proof-script-generic-parse-find-comment-end 1651,63921
+(defun proof-script-generic-parse-cmdend 1660,64335
+(defun proof-script-generic-parse-cmdstart 1685,65222
+(defun proof-script-generic-parse-sexp 1748,67915
+(defun proof-cmdstart-add-segment-for-cmd 1772,68847
+(defun proof-segment-up-to-cmdstart 1823,70905
+(defun proof-segment-up-to-cmdend 1884,73265
+(defun proof-semis-to-vanillas 1956,75944
+(defun proof-script-next-command-advance 2005,77466
+(defun proof-assert-until-point 2024,77965
+(defun proof-assert-electric-terminator 2039,78558
+(defun proof-assert-semis 2073,79900
+(defun proof-retract-before-change 2086,80539
+(defun proof-inside-comment 2095,80857
+(defun proof-insert-pbp-command 2110,81140
+(defun proof-insert-sendback-command 2125,81634
+(defun proof-done-retracting 2151,82537
+(defun proof-setup-retract-action 2186,83978
+(defun proof-last-goal-or-goalsave 2196,84464
+(defun proof-retract-target 2220,85369
+(defun proof-retract-until-point-interactive 2303,88883
+(defun proof-retract-until-point 2311,89268
+(define-derived-mode proof-mode 2358,91103
+(defun proof-script-set-visited-file-name 2395,92471
+(defun proof-script-set-buffer-hooks 2417,93484
+(defun proof-script-kill-buffer-fn 2425,93902
+(defun proof-config-done-related 2457,95219
+(defun proof-generic-goal-command-p 2525,97742
+(defun proof-generic-state-preserving-p 2530,97955
+(defun proof-generic-count-undos 2539,98472
+(defun proof-generic-find-and-forget 2568,99510
+(defconst proof-script-important-settings2621,101349
+(defun proof-config-done 2636,101895
+(defun proof-setup-parsing-mechanism 2704,104173
+(defun proof-setup-imenu 2748,106026
+(deflocal proof-segment-up-to-cache 2772,106800
+(deflocal proof-segment-up-to-cache-start 2773,106841
+(deflocal proof-last-edited-low-watermark 2774,106886
+(defun proof-segment-up-to-using-cache 2784,107373
+(defun proof-segment-cache-contents-for 2813,108521
+(defun proof-script-after-change-function 2825,108890
+(defun proof-script-set-after-change-functions 2837,109397
 
 generic/proof-shell.el,3793
 (defvar proof-marker 35,808
@@ -1855,11 +1855,11 @@ generic/proof-unicode-tokens.el,497
 (defun proof-unicode-tokens-configure 48,1436
 (defun proof-unicode-tokens-mode-if-enabled 60,1882
 (defun proof-unicode-tokens-set-global 66,2081
-(defun proof-unicode-tokens-enable 80,2635
-(defun proof-unicode-tokens-reconfigure 100,3488
-(defun proof-unicode-tokens-configure-prover 126,4376
-(defun proof-unicode-tokens-activate-prover 131,4557
-(defun proof-unicode-tokens-deactivate-prover 138,4803
+(defun proof-unicode-tokens-enable 82,2651
+(defun proof-unicode-tokens-reconfigure 102,3504
+(defun proof-unicode-tokens-configure-prover 128,4392
+(defun proof-unicode-tokens-activate-prover 133,4573
+(defun proof-unicode-tokens-deactivate-prover 140,4819
 
 generic/proof-useropts.el,1510
 (defgroup proof-user-options 21,553
@@ -1950,36 +1950,39 @@ generic/proof-utils.el,2033
 (defsubst proof-shell-strip-output-markup 941,35257
 (defun proof-minibuffer-message 947,35521
 
-lib/bufhist.el,1106
-(defun bufhist-ring-update 36,1305
-(defgroup bufhist 45,1627
-(defcustom bufhist-ring-size 49,1708
-(defvar bufhist-ring 54,1819
-(defvar bufhist-ring-pos 57,1893
-(defvar bufhist-lastswitch-modified-tick 60,1972
-(defvar bufhist-read-only-history 63,2078
-(defvar bufhist-saved-mode-line-format 66,2149
-(defvar bufhist-normal-read-only 69,2252
-(defun bufhist-mode-line-format-entry 72,2346
-(defconst bufhist-minor-mode-map101,3420
-(define-minor-mode bufhist-mode114,3897
-(defun bufhist-get-buffer-contents 135,4730
-(defun bufhist-restore-buffer-contents 143,5028
-(defun bufhist-checkpoint 151,5315
-(defun bufhist-erase-buffer 159,5684
-(defun bufhist-checkpoint-and-erase 169,6028
-(defun bufhist-switch-to-index 175,6214
-(defun bufhist-first 214,7813
-(defun bufhist-last 219,7972
-(defun bufhist-prev 224,8116
-(defun bufhist-next 232,8339
-(defun bufhist-delete 237,8479
-(defun bufhist-clear 249,9020
-(defun bufhist-init 264,9415
-(defun bufhist-exit 289,10348
-(defun bufhist-set-readwrite 299,10612
-(defun bufhist-before-change-function 314,11232
-(defun bufhist-make-buttons 326,11647
+lib/bufhist.el,1257
+(defun bufhist-ring-update 38,1391
+(defgroup bufhist 47,1713
+(defcustom bufhist-ring-size 51,1794
+(defvar bufhist-ring 56,1905
+(defvar bufhist-ring-pos 59,1979
+(defvar bufhist-lastswitch-modified-tick 62,2058
+(defvar bufhist-read-only-history 65,2164
+(defvar bufhist-saved-mode-line-format 68,2235
+(defvar bufhist-normal-read-only 71,2338
+(defvar bufhist-top-point 74,2432
+(defun bufhist-mode-line-format-entry 77,2522
+(defconst bufhist-minor-mode-map106,3596
+(define-minor-mode bufhist-mode119,4073
+(defun bufhist-get-buffer-contents 141,4954
+(defun bufhist-restore-buffer-contents 150,5296
+(defun bufhist-checkpoint 159,5610
+(defun bufhist-erase-buffer 167,5979
+(defun bufhist-checkpoint-and-erase 178,6350
+(defun bufhist-switch-to-index 184,6536
+(defun bufhist-first 223,8135
+(defun bufhist-last 228,8294
+(defun bufhist-prev 233,8438
+(defun bufhist-next 241,8661
+(defun bufhist-delete 246,8801
+(defun bufhist-clear 258,9342
+(defun bufhist-init 273,9737
+(defun bufhist-exit 301,10746
+(defun bufhist-set-readwrite 311,11010
+(defun bufhist-before-change-function 326,11630
+(define-button-type 'bufhist-nextbufhist-next
340,12053
+(define-button-type 'bufhist-prevbufhist-prev
344,12150
+(defun bufhist-insert-buttons 351,12362
 
 lib/holes.el,2465
 (defvar holes-default-hole 44,1121
@@ -2083,6 +2086,10 @@ lib/proof-compat.el,297
 (defalias 'proof-buffer-syntactic-contextproof-buffer-syntactic-context
164,5213
 (defmacro declare-function 179,5596
 
+lib/ps-fix.el,72
+(defun ps-face-attributes 5,191
+(defun ps-face-attribute-list 37,1269
+
 lib/scomint.el,876
 (defface scomint-highlight-input 19,493
 (defface scomint-highlight-prompt23,609
@@ -2163,108 +2170,112 @@ lib/unicode-chars.el,80
 (defvar unicode-chars-alist12,348
 (defun unicode-chars-list-chars 5051,245975
 
-lib/unicode-tokens.el,5231
-(defvar unicode-tokens-token-symbol-map 56,1828
-(defvar unicode-tokens-token-format 75,2450
-(defvar unicode-tokens-token-variant-format-regexp 81,2699
-(defvar unicode-tokens-shortcut-alist 95,3232
-(defvar unicode-tokens-shortcut-replacement-alist 101,3509
-(defvar unicode-tokens-control-region-format-regexp 109,3715
-(defvar unicode-tokens-control-char-format-regexp 116,4083
-(defvar unicode-tokens-control-regions 123,4444
-(defvar unicode-tokens-control-characters 126,4520
-(defvar unicode-tokens-control-char-format 129,4602
-(defvar unicode-tokens-control-region-format-start 132,4715
-(defvar unicode-tokens-control-region-format-end 135,4832
-(defvar unicode-tokens-tokens-customizable-variables 138,4945
-(defconst unicode-tokens-configuration-variables145,5113
-(defun unicode-tokens-config 160,5512
-(defun unicode-tokens-config-var 164,5657
-(defun unicode-tokens-copy-configuration-variables 176,6097
-(defvar unicode-tokens-token-list 204,7313
-(defvar unicode-tokens-hash-table 207,7433
-(defvar unicode-tokens-token-match-regexp 210,7549
-(defvar unicode-tokens-uchar-hash-table 216,7832
-(defvar unicode-tokens-uchar-regexp 220,8019
-(defgroup unicode-tokens-faces 228,8204
-(defconst unicode-tokens-font-family-alternatives238,8501
-(defface unicode-tokens-symbol-font-face252,8949
-(defface unicode-tokens-script-font-face270,9589
-(defface unicode-tokens-fraktur-font-face275,9733
-(defface unicode-tokens-serif-font-face280,9858
-(defface unicode-tokens-sans-font-face285,9995
-(defface unicode-tokens-highlight-face290,10117
-(defconst unicode-tokens-fonts299,10479
-(defconst unicode-tokens-fontsymb-properties308,10696
-(define-widget 'unicode-tokens-token-symbol-map unicode-tokens-token-symbol-map
334,12142
-(define-widget 'unicode-tokens-shortcut-alist unicode-tokens-shortcut-alist
352,12694
-(defconst unicode-tokens-font-lock-extra-managed-props365,13025
-(defun unicode-tokens-font-lock-keywords 369,13179
-(defun unicode-tokens-calculate-token-match 402,14550
-(defun unicode-tokens-usable-composition 432,15588
-(defun unicode-tokens-help-echo 445,15967
-(defvar unicode-tokens-show-symbols 449,16131
-(defun unicode-tokens-interpret-composition 452,16245
-(defun unicode-tokens-font-lock-compose-symbol 470,16757
-(defun unicode-tokens-prepend-text-properties-in-match 500,18004
-(defun unicode-tokens-prepend-text-property 514,18582
-(defun unicode-tokens-show-symbols 539,19727
-(defun unicode-tokens-symbs-to-props 547,20037
-(defvar unicode-tokens-show-controls 567,20736
-(defun unicode-tokens-show-controls 570,20827
-(defun unicode-tokens-control-char 583,21412
-(defun unicode-tokens-control-region 592,21851
-(defun unicode-tokens-control-font-lock-keywords 603,22398
-(defvar unicode-tokens-use-shortcuts 614,22722
-(defun unicode-tokens-use-shortcuts 617,22825
-(defun unicode-tokens-map-ordering 635,23431
-(defun unicode-tokens-quail-define-rules 644,23784
-(defun unicode-tokens-insert-token 667,24461
-(defun unicode-tokens-annotate-region 676,24765
-(defun unicode-tokens-insert-control 700,25603
-(defun unicode-tokens-insert-uchar-as-token 710,26052
-(defun unicode-tokens-delete-token-near-point 716,26273
-(defun unicode-tokens-prev-token 730,26835
-(defun unicode-tokens-rotate-token-forward 738,27132
-(defun unicode-tokens-rotate-token-backward 765,28022
-(defun unicode-tokens-replace-shortcut-match 770,28224
-(defun unicode-tokens-replace-shortcuts 779,28594
-(defun unicode-tokens-replace-unicode-match 793,29192
-(defun unicode-tokens-replace-unicode 800,29493
-(defun unicode-tokens-copy-token 817,30092
-(define-button-type 'unicode-tokens-listunicode-tokens-list
824,30313
-(defun unicode-tokens-list-tokens 830,30517
-(defun unicode-tokens-list-shortcuts 869,31701
-(defalias 'unicode-tokens-list-unicode-chars unicode-tokens-list-unicode-chars
887,32339
-(defun unicode-tokens-encode-in-temp-buffer 889,32412
-(defun unicode-tokens-encode 907,33068
-(defun unicode-tokens-encode-str 913,33304
-(defun unicode-tokens-copy 917,33466
-(defun unicode-tokens-paste 926,33872
-(defvar unicode-tokens-highlight-unicode 945,34593
-(defconst unicode-tokens-unicode-highlight-patterns948,34685
-(defun unicode-tokens-highlight-unicode 952,34854
-(defun unicode-tokens-highlight-unicode-setkeywords 964,35317
-(defun unicode-tokens-initialise 976,35686
-(defvar unicode-tokens-mode-map 996,36357
-(define-minor-mode unicode-tokens-mode999,36454
-(defun unicode-tokens-set-font-var 1126,40698
-(defun unicode-tokens-set-font-var-aux 1142,41189
-(defun unicode-tokens-mouse-set-font 1171,42431
-(defsubst unicode-tokens-face-font-sym 1184,42945
-(defun unicode-tokens-set-font-restart 1188,43125
-(defun unicode-tokens-save-fonts 1199,43435
-(defun unicode-tokens-custom-save-faces 1207,43691
-(define-key unicode-tokens-mode-map 1224,44147
-(define-key unicode-tokens-mode-map 1226,44239
-(define-key unicode-tokens-mode-map1228,44330
-(define-key unicode-tokens-mode-map1230,44436
-(define-key unicode-tokens-mode-map1233,44551
-(define-key unicode-tokens-mode-map1235,44660
-(define-key unicode-tokens-mode-map1237,44768
-(define-key unicode-tokens-mode-map1239,44874
-(defun unicode-tokens-customize-submenu 1247,44998
-(defun unicode-tokens-define-menu 1254,45221
+lib/unicode-tokens.el,5431
+(defgroup unicode-tokens-options 54,1695
+(defcustom unicode-tokens-add-help-echo 58,1804
+(defun unicode-tokens-toggle-add-help-echo 63,1971
+(defvar unicode-tokens-token-symbol-map 77,2377
+(defvar unicode-tokens-token-format 96,2999
+(defvar unicode-tokens-token-variant-format-regexp 102,3248
+(defvar unicode-tokens-shortcut-alist 116,3781
+(defvar unicode-tokens-shortcut-replacement-alist 122,4058
+(defvar unicode-tokens-control-region-format-regexp 130,4264
+(defvar unicode-tokens-control-char-format-regexp 137,4632
+(defvar unicode-tokens-control-regions 144,4993
+(defvar unicode-tokens-control-characters 147,5069
+(defvar unicode-tokens-control-char-format 150,5151
+(defvar unicode-tokens-control-region-format-start 153,5264
+(defvar unicode-tokens-control-region-format-end 156,5381
+(defvar unicode-tokens-tokens-customizable-variables 159,5494
+(defconst unicode-tokens-configuration-variables166,5662
+(defun unicode-tokens-config 181,6061
+(defun unicode-tokens-config-var 185,6206
+(defun unicode-tokens-copy-configuration-variables 197,6646
+(defvar unicode-tokens-token-list 225,7862
+(defvar unicode-tokens-hash-table 228,7982
+(defvar unicode-tokens-token-match-regexp 231,8098
+(defvar unicode-tokens-uchar-hash-table 237,8381
+(defvar unicode-tokens-uchar-regexp 241,8568
+(defgroup unicode-tokens-faces 249,8753
+(defconst unicode-tokens-font-family-alternatives259,9050
+(defface unicode-tokens-symbol-font-face273,9498
+(defface unicode-tokens-script-font-face291,10138
+(defface unicode-tokens-fraktur-font-face296,10282
+(defface unicode-tokens-serif-font-face301,10407
+(defface unicode-tokens-sans-font-face306,10544
+(defface unicode-tokens-highlight-face311,10666
+(defconst unicode-tokens-fonts320,11028
+(defconst unicode-tokens-fontsymb-properties329,11245
+(define-widget 'unicode-tokens-token-symbol-map unicode-tokens-token-symbol-map
355,12691
+(define-widget 'unicode-tokens-shortcut-alist unicode-tokens-shortcut-alist
373,13243
+(defconst unicode-tokens-font-lock-extra-managed-props386,13574
+(defun unicode-tokens-font-lock-keywords 390,13728
+(defun unicode-tokens-calculate-token-match 423,15099
+(defun unicode-tokens-usable-composition 453,16137
+(defun unicode-tokens-help-echo 466,16516
+(defvar unicode-tokens-show-symbols 471,16718
+(defun unicode-tokens-interpret-composition 474,16832
+(defun unicode-tokens-font-lock-compose-symbol 492,17344
+(defun unicode-tokens-prepend-text-properties-in-match 522,18591
+(defun unicode-tokens-prepend-text-property 536,19169
+(defun unicode-tokens-show-symbols 561,20314
+(defun unicode-tokens-symbs-to-props 569,20624
+(defvar unicode-tokens-show-controls 589,21323
+(defun unicode-tokens-show-controls 592,21414
+(defun unicode-tokens-control-char 605,21999
+(defun unicode-tokens-control-region 614,22438
+(defun unicode-tokens-control-font-lock-keywords 625,22985
+(defvar unicode-tokens-use-shortcuts 636,23309
+(defun unicode-tokens-use-shortcuts 639,23412
+(defun unicode-tokens-map-ordering 657,24018
+(defun unicode-tokens-quail-define-rules 666,24371
+(defun unicode-tokens-insert-token 689,25048
+(defun unicode-tokens-annotate-region 698,25352
+(defun unicode-tokens-insert-control 722,26190
+(defun unicode-tokens-insert-uchar-as-token 732,26639
+(defun unicode-tokens-delete-token-near-point 738,26860
+(defun unicode-tokens-prev-token 752,27422
+(defun unicode-tokens-rotate-token-forward 760,27719
+(defun unicode-tokens-rotate-token-backward 787,28609
+(defun unicode-tokens-replace-shortcut-match 792,28811
+(defun unicode-tokens-replace-shortcuts 801,29181
+(defun unicode-tokens-replace-unicode-match 815,29779
+(defun unicode-tokens-replace-unicode 822,30080
+(defun unicode-tokens-copy-token 839,30679
+(define-button-type 'unicode-tokens-listunicode-tokens-list
846,30900
+(defun unicode-tokens-list-tokens 852,31104
+(defun unicode-tokens-list-shortcuts 891,32288
+(defalias 'unicode-tokens-list-unicode-chars unicode-tokens-list-unicode-chars
909,32926
+(defun unicode-tokens-encode-in-temp-buffer 911,32999
+(defun unicode-tokens-encode 929,33655
+(defun unicode-tokens-encode-str 935,33891
+(defun unicode-tokens-copy 939,34053
+(defun unicode-tokens-paste 948,34459
+(defvar unicode-tokens-highlight-unicode 967,35180
+(defconst unicode-tokens-unicode-highlight-patterns970,35272
+(defun unicode-tokens-highlight-unicode 974,35441
+(defun unicode-tokens-highlight-unicode-setkeywords 986,35904
+(defun unicode-tokens-initialise 998,36273
+(defvar unicode-tokens-mode-map 1018,36944
+(defvar unicode-tokens-display-table 1021,37041
+(define-minor-mode unicode-tokens-mode1028,37293
+(defun unicode-tokens-set-font-var 1161,41776
+(defun unicode-tokens-set-font-var-aux 1177,42267
+(defun unicode-tokens-mouse-set-font 1206,43509
+(defsubst unicode-tokens-face-font-sym 1219,44023
+(defun unicode-tokens-set-font-restart 1223,44203
+(defun unicode-tokens-save-fonts 1234,44513
+(defun unicode-tokens-custom-save-faces 1242,44769
+(define-key unicode-tokens-mode-map 1259,45225
+(define-key unicode-tokens-mode-map 1261,45317
+(define-key unicode-tokens-mode-map1263,45408
+(define-key unicode-tokens-mode-map1265,45514
+(define-key unicode-tokens-mode-map1268,45629
+(define-key unicode-tokens-mode-map1270,45738
+(define-key unicode-tokens-mode-map1272,45846
+(define-key unicode-tokens-mode-map1274,45952
+(defun unicode-tokens-customize-submenu 1282,46076
+(defun unicode-tokens-define-menu 1289,46299
 
 mmm/mmm-auto.el,343
 (defvar mmm-autoloaded-classes67,2676