diff options
| -rw-r--r-- | TAGS | 701 | ||||
| -rw-r--r-- | generic/proof-autoloads.el | 64 |
2 files changed, 388 insertions, 377 deletions
@@ -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-next340,12053 +(define-button-type 'bufhist-prevbufhist-prev344,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-context164,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-map334,12142 -(define-widget 'unicode-tokens-shortcut-alist unicode-tokens-shortcut-alist352,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-list824,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-chars887,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-map355,12691 +(define-widget 'unicode-tokens-shortcut-alist unicode-tokens-shortcut-alist373,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-list846,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-chars909,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 diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el index 91361e36..449755ec 100644 --- a/generic/proof-autoloads.el +++ b/generic/proof-autoloads.el @@ -8,7 +8,7 @@ ;;;### (autoloads (bufhist-exit bufhist-init bufhist-mode) "bufhist" -;;;;;; "../lib/bufhist.el" (19109 19688)) +;;;;;; "../lib/bufhist.el" (19127 26600)) ;;; Generated autoloads from ../lib/bufhist.el (autoload (quote bufhist-mode) "bufhist" "\ @@ -306,76 +306,76 @@ All of these settings are optional. ;;;;;; pg-response-buffers-hint pg-slow-fontify-tracing-hint proof-electric-terminator-enable ;;;;;; proof-define-assistant-command-witharg proof-define-assistant-command ;;;;;; proof-goto-point proof-script-new-command-advance) "pg-user" -;;;;;; "pg-user.el" (19122 39720)) +;;;;;; "pg-user.el" (19127 24433)) ;;; Generated autoloads from pg-user.el -(autoload 'proof-script-new-command-advance "pg-user" "\ +(autoload (quote proof-script-new-command-advance) "pg-user" "\ Move point to a nice position for a new command. Assumes that point is at the end of a command. \(fn)" t nil) -(autoload 'proof-goto-point "pg-user" "\ +(autoload (quote proof-goto-point) "pg-user" "\ Assert or retract to the command at current position. Calls `proof-assert-until-point' or `proof-retract-until-point' as appropriate. \(fn)" t nil) -(autoload 'proof-define-assistant-command "pg-user" "\ +(autoload (quote proof-define-assistant-command) "pg-user" "\ Define FN (docstring DOC) to send BODY to prover, based on CMDVAR. BODY defaults to CMDVAR, a variable. \(fn FN DOC CMDVAR &optional BODY)" nil (quote macro)) -(autoload 'proof-define-assistant-command-witharg "pg-user" "\ +(autoload (quote proof-define-assistant-command-witharg) "pg-user" "\ Define command FN to prompt for string CMDVAR to proof assistant. CMDVAR is a variable holding a function or string. Automatically has history. \(fn FN DOC CMDVAR PROMPT &rest BODY)" nil (quote macro)) -(autoload 'proof-electric-terminator-enable "pg-user" "\ +(autoload (quote proof-electric-terminator-enable) "pg-user" "\ Make sure the modeline is updated to display new value for electric terminator. \(fn)" nil nil) -(autoload 'pg-slow-fontify-tracing-hint "pg-user" "\ +(autoload (quote pg-slow-fontify-tracing-hint) "pg-user" "\ Not documented \(fn)" nil nil) -(autoload 'pg-response-buffers-hint "pg-user" "\ +(autoload (quote pg-response-buffers-hint) "pg-user" "\ Not documented \(fn &optional NEXTBUF)" nil nil) -(autoload 'pg-jump-to-end-hint "pg-user" "\ +(autoload (quote pg-jump-to-end-hint) "pg-user" "\ Not documented \(fn)" nil nil) -(autoload 'pg-processing-complete-hint "pg-user" "\ +(autoload (quote pg-processing-complete-hint) "pg-user" "\ Display hint for showing end of locked region or processing complete. \(fn)" nil nil) -(autoload 'pg-next-error-hint "pg-user" "\ +(autoload (quote pg-next-error-hint) "pg-user" "\ Display hint for locating error. \(fn)" nil nil) -(autoload 'pg-hint "pg-user" "\ +(autoload (quote pg-hint) "pg-user" "\ Display a hint HINTMSG in the minibuffer, if `pg-show-hints' is non-nil. The function `substitute-command-keys' is called on the argument. \(fn HINTMSG)" nil nil) -(autoload 'proof-imenu-enable "pg-user" "\ +(autoload (quote proof-imenu-enable) "pg-user" "\ Add or remove index menu. \(fn)" nil nil) -(autoload 'pg-previous-matching-input-from-input "pg-user" "\ +(autoload (quote pg-previous-matching-input-from-input) "pg-user" "\ Search backwards through input history for match for current input. \(Previous history elements are earlier commands.) With prefix argument N, search for Nth previous match. @@ -383,7 +383,7 @@ If N is negative, search forwards for the -Nth following match. \(fn N)" t nil) -(autoload 'pg-next-matching-input-from-input "pg-user" "\ +(autoload (quote pg-next-matching-input-from-input) "pg-user" "\ Search forwards through input history for match for current input. \(Following history elements are more recent commands.) With prefix argument N, search for Nth following match. @@ -391,21 +391,21 @@ If N is negative, search backwards for the -Nth previous match. \(fn N)" t nil) -(autoload 'pg-add-to-input-history "pg-user" "\ +(autoload (quote pg-add-to-input-history) "pg-user" "\ Maybe add CMD to the input history. CMD is only added to the input history if it is not a duplicate of the last item added. \(fn CMD)" nil nil) -(autoload 'pg-remove-from-input-history "pg-user" "\ +(autoload (quote pg-remove-from-input-history) "pg-user" "\ Maybe remove CMD from the end of the input history. This is called when the command is undone. It's only removed if it matches the last item in the ring. \(fn CMD)" nil nil) -(autoload 'pg-clear-input-ring "pg-user" "\ +(autoload (quote pg-clear-input-ring) "pg-user" "\ Not documented \(fn)" nil nil) @@ -487,26 +487,26 @@ in future if we have just activated it for this buffer. ;;;*** ;;;### (autoloads (proof-aux-menu proof-menu-define-specific proof-menu-define-main -;;;;;; proof-menu-define-keys) "proof-menu" "proof-menu.el" (19121 -;;;;;; 59724)) +;;;;;; proof-menu-define-keys) "proof-menu" "proof-menu.el" (19127 +;;;;;; 27638)) ;;; Generated autoloads from proof-menu.el -(autoload 'proof-menu-define-keys "proof-menu" "\ +(autoload (quote proof-menu-define-keys) "proof-menu" "\ Prover specific keymap under C-c C-a. \(fn MAP)" nil nil) -(autoload 'proof-menu-define-main "proof-menu" "\ +(autoload (quote proof-menu-define-main) "proof-menu" "\ Not documented \(fn)" nil nil) -(autoload 'proof-menu-define-specific "proof-menu" "\ +(autoload (quote proof-menu-define-specific) "proof-menu" "\ Not documented \(fn)" nil nil) -(autoload 'proof-aux-menu "proof-menu" "\ +(autoload (quote proof-aux-menu) "proof-menu" "\ Construct and return PG auxiliary menu used in non-scripting buffers. \(fn)" nil nil) @@ -537,7 +537,7 @@ in future if we have just activated it for this buffer. ;;;;;; proof-insert-pbp-command proof-register-possibly-new-processed-file ;;;;;; pg-set-span-helphighlights proof-locked-region-empty-p proof-locked-region-full-p ;;;;;; proof-locked-end proof-unprocessed-begin proof-colour-locked) -;;;;;; "proof-script" "proof-script.el" (19126 40975)) +;;;;;; "proof-script" "proof-script.el" (19127 27615)) ;;; Generated autoloads from proof-script.el (autoload (quote proof-colour-locked) "proof-script" "\ @@ -812,7 +812,7 @@ Menu made from the Proof General toolbar commands. ;;;### (autoloads (proof-unicode-tokens-enable proof-unicode-tokens-set-global ;;;;;; proof-unicode-tokens-mode-if-enabled) "proof-unicode-tokens" -;;;;;; "proof-unicode-tokens.el" (19126 41343)) +;;;;;; "proof-unicode-tokens.el" (19126 41475)) ;;; Generated autoloads from proof-unicode-tokens.el (autoload (quote proof-unicode-tokens-mode-if-enabled) "proof-unicode-tokens" "\ @@ -921,7 +921,7 @@ in your emacs font. ;;;*** ;;;### (autoloads (unicode-tokens-encode-str) "unicode-tokens" "../lib/unicode-tokens.el" -;;;;;; (19126 40592)) +;;;;;; (19127 27485)) ;;; Generated autoloads from ../lib/unicode-tokens.el (autoload (quote unicode-tokens-encode-str) "unicode-tokens" "\ @@ -932,10 +932,10 @@ Return a unicode encoded version presentation of STR. ;;;*** ;;;### (autoloads nil nil ("../lib/local-vars-list.el" "../lib/pg-dev.el" -;;;;;; "../lib/pg-fontsets.el" "../lib/proof-compat.el" "../lib/span.el" -;;;;;; "pg-autotest.el" "pg-custom.el" "pg-pbrpm.el" "pg-vars.el" -;;;;;; "proof-auxmodes.el" "proof-config.el" "proof-faces.el" "proof-useropts.el" -;;;;;; "proof.el") (19126 41348 193007)) +;;;;;; "../lib/pg-fontsets.el" "../lib/proof-compat.el" "../lib/ps-fix.el" +;;;;;; "../lib/span.el" "pg-autotest.el" "pg-custom.el" "pg-pbrpm.el" +;;;;;; "pg-vars.el" "proof-auxmodes.el" "proof-config.el" "proof-faces.el" +;;;;;; "proof-useropts.el" "proof.el") (19127 27664 537600)) ;;;*** |