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