diff options
author | Hendrik Tews <hendrik@askra.de> | 2012-01-03 09:37:13 +0000 |
---|---|---|
committer | Hendrik Tews <hendrik@askra.de> | 2012-01-03 09:37:13 +0000 |
commit | 413d5721b1dfb5f4d43c8e1676cd5def02f63423 (patch) | |
tree | e1e3a82f666433ebbc83f64d9f2df143c0a34b23 /TAGS | |
parent | 34c15424cc454cd59c5e094093acd6ddbdcc5186 (diff) |
update TAGS
Diffstat (limited to 'TAGS')
-rw-r--r-- | TAGS | 4946 |
1 files changed, 2528 insertions, 2418 deletions
@@ -38,207 +38,229 @@ coq/coq-db.el,678 (defconst coq-solve-tactics-face 266,9550 (defconst coq-cheat-face 270,9714 -coq/coq.el,8178 -(defcustom coq-prog-name58,1726 -(defcustom coq-translate-to-v8 77,2578 -(defun coq-build-prog-args 83,2758 -(defcustom coq-compiler93,3052 -(defcustom coq-dependency-analyzer99,3189 -(defcustom coq-use-makefile 105,3329 -(defcustom coq-default-undo-limit 111,3501 -(defconst coq-shell-init-cmd116,3629 -(defcustom coq-prog-env 125,3956 -(defconst coq-shell-restart-cmd 133,4205 -(defvar coq-shell-prompt-pattern135,4259 -(defvar coq-shell-cd 143,4562 -(defvar coq-shell-proof-completed-regexp 147,4722 -(defvar coq-goal-regexp150,4877 -(defun get-coq-library-directory 155,4973 -(defconst coq-library-directory 161,5155 -(defcustom coq-tags 164,5282 -(defconst coq-interrupt-regexp 169,5430 -(defcustom coq-www-home-page 172,5523 -(defvar coq-outline-regexp183,5698 -(defvar coq-outline-heading-end-regexp 190,5911 -(defvar coq-shell-outline-regexp 192,5965 -(defvar coq-shell-outline-heading-end-regexp 193,6015 -(defconst coq-state-preserving-tactics-regexp196,6079 -(defconst coq-state-changing-commands-regexp198,6181 -(defconst coq-state-preserving-commands-regexp200,6290 -(defconst coq-commands-regexp202,6403 -(defvar coq-retractable-instruct-regexp204,6482 -(defvar coq-non-retractable-instruct-regexp206,6574 -(defcustom coq-use-smie 238,7270 -(defconst coq-smie-grammar246,7499 -(defun coq-smie-search-token-forward 298,9919 -(defun coq-smie-search-token-backward 311,10426 -(defconst coq-smie-proof-end-tokens337,11638 -(defun coq-smie-forward-token 341,11768 -(defun coq-smie-backward-token 387,13521 -(defun coq-smie-rules 432,15226 -(defconst coq-script-command-end-regexp 503,18286 -(defun coq-script-parse-function 512,18715 -(defun coq-set-undo-limit 519,18941 -(defun build-list-id-from-string 523,19071 -(defun coq-last-prompt-info 535,19569 -(defun coq-last-prompt-info-safe 547,20101 -(defvar coq-last-but-one-statenum 553,20358 -(defvar coq-last-but-one-proofnum 560,20655 -(defvar coq-last-but-one-proofstack 563,20753 -(defsubst coq-get-span-statenum 566,20863 -(defsubst coq-get-span-proofnum 570,20978 -(defsubst coq-get-span-proofstack 574,21093 -(defsubst coq-set-span-statenum 578,21237 -(defsubst coq-get-span-goalcmd 582,21368 -(defsubst coq-set-span-goalcmd 586,21482 -(defsubst coq-set-span-proofnum 590,21612 -(defsubst coq-set-span-proofstack 594,21743 -(defsubst proof-last-locked-span 598,21903 -(defun proof-clone-buffer 602,22037 -(defun proof-store-buffer-win 616,22574 -(defun proof-store-response-win 627,23067 -(defun proof-store-goals-win 631,23194 -(defun coq-set-state-infos 643,23726 -(defun count-not-intersection 681,25812 -(defun coq-find-and-forget 711,27064 -(defvar coq-current-goal 738,28369 -(defun coq-goal-hyp 741,28434 -(defun coq-state-preserving-p 754,28908 -(defconst notation-print-kinds-table768,29229 -(defun coq-PrintScope 772,29396 -(defun coq-guess-or-ask-for-string 790,29945 -(defun coq-ask-do 804,30485 -(defsubst coq-put-into-brackets 813,30870 -(defsubst coq-put-into-quotes 816,30931 -(defun coq-SearchIsos 819,30990 -(defun coq-SearchConstant 827,31229 -(defun coq-Searchregexp 831,31322 -(defun coq-SearchRewrite 837,31463 -(defun coq-SearchAbout 841,31560 -(defun coq-Print 847,31703 -(defun coq-About 852,31827 -(defun coq-LocateConstant 857,31946 -(defun coq-LocateLibrary 862,32049 -(defun coq-LocateNotation 867,32166 -(defun coq-Pwd 875,32397 -(defun coq-Inspect 880,32521 -(defun coq-PrintSection(884,32621 -(defun coq-Print-implicit 888,32714 -(defun coq-Check 893,32865 -(defun coq-Show 898,32973 -(defun coq-Compile 912,33416 -(defun coq-guess-command-line 924,33734 -(defpacustom use-editing-holes 961,35291 -(defun coq-mode-config 970,35594 -(defun coq-shell-mode-config 1066,39074 -(defun coq-goals-mode-config 1111,40903 -(defun coq-response-config 1118,41147 -(defpacustom print-fully-explicit 1144,41988 -(defpacustom print-implicit 1149,42136 -(defpacustom print-coercions 1154,42302 -(defpacustom print-match-wildcards 1159,42446 -(defpacustom print-elim-types 1164,42626 -(defpacustom printing-depth 1169,42792 -(defpacustom undo-depth 1174,42953 -(defpacustom time-commands 1179,43119 -(defgroup coq-auto-compile 1190,43369 -(defpacustom compile-before-require 1195,43520 -(defcustom coq-compile-command 1207,44012 -(defconst coq-compile-substitution-list1237,45295 -(defcustom coq-load-path 1257,46216 -(defcustom coq-compile-auto-save 1308,48737 -(defcustom coq-lock-ancestors 1333,49795 -(defpacustom confirm-external-compilation 1342,50116 -(defcustom coq-load-path-include-current 1351,50423 -(defcustom coq-compile-ignored-directories 1360,50741 -(defcustom coq-compile-ignore-library-directory 1373,51374 -(defcustom coq-coqdep-error-regexp1385,51862 -(defconst coq-require-command-regexp1401,52580 -(defconst coq-require-id-regexp1408,52937 -(defvar coq-compile-history 1416,53371 -(defvar coq-compile-response-buffer 1419,53455 -(defvar coq-debug-auto-compilation 1423,53590 -(defun time-less-or-equal 1429,53698 -(defun coq-max-dep-mod-time 1437,54036 -(defun coq-prog-args 1460,54840 -(defun coq-lock-ancestor 1469,55099 -(defun coq-unlock-ancestor 1485,55874 -(defun coq-unlock-all-ancestors-of-span 1492,56169 -(defun coq-compile-ignore-file 1499,56465 -(defun coq-library-src-of-obj-file 1523,57348 -(defun coq-option-of-load-path-entry 1528,57580 -(defun coq-include-options 1544,58171 -(defun coq-init-compile-response-buffer 1564,58995 -(defun coq-display-compile-response-buffer 1587,60067 -(defun coq-get-library-dependencies 1601,60701 -(defun coq-compile-library 1648,62926 -(defun coq-compile-library-if-necessary 1675,64137 -(defun coq-make-lib-up-to-date 1721,66009 -(defun coq-auto-compile-externally 1777,68472 -(defun coq-map-module-id-to-obj-file 1820,70618 -(defun coq-check-module 1873,73220 -(defvar coq-process-require-current-buffer1901,74662 -(defun coq-compile-save-buffer-filter 1907,74927 -(defun coq-compile-save-some-buffers 1917,75341 -(defun coq-preprocess-require-commands 1939,76243 -(defun coq-switch-buffer-kill-proof-shell 1972,77812 -(defun coq-preprocessing 1993,78530 -(defun coq-fake-constant-markup 2007,78985 -(defun coq-create-span-menu 2023,79590 -(defconst module-kinds-table2041,80103 -(defconst modtype-kinds-table2045,80252 -(defun coq-insert-section-or-module 2049,80381 -(defconst reqkinds-kinds-table2070,81231 -(defun coq-insert-requires 2074,81375 -(defun coq-end-Section 2087,81854 -(defun coq-insert-intros 2105,82432 -(defun coq-insert-infoH-hook 2117,82963 -(defun coq-insert-as 2122,83171 -(defun coq-insert-match 2139,83864 -(defun coq-insert-solve-tactic 2168,85033 -(defun coq-insert-tactic 2174,85284 -(defun coq-insert-tactical 2180,85486 -(defun coq-insert-command 2186,85717 -(defun coq-insert-term 2191,85882 -(define-key coq-keymap 2196,86043 -(define-key coq-keymap 2197,86101 -(define-key coq-keymap 2198,86158 -(define-key coq-keymap 2199,86227 -(define-key coq-keymap 2200,86283 -(define-key coq-keymap 2201,86332 -(define-key coq-keymap 2202,86390 -(define-key coq-keymap 2203,86440 -(define-key coq-keymap 2204,86495 -(define-key coq-keymap 2206,86548 -(define-key coq-keymap 2208,86622 -(define-key coq-keymap 2209,86679 -(define-key coq-keymap 2212,86744 -(define-key coq-keymap 2213,86804 -(define-key coq-keymap 2215,86860 -(define-key coq-keymap 2216,86910 -(define-key coq-keymap 2217,86960 -(define-key coq-keymap 2218,87016 -(define-key coq-keymap 2219,87066 -(define-key coq-keymap 2220,87110 -(define-key coq-keymap 2221,87169 -(define-key coq-goals-mode-map 2224,87230 -(define-key coq-goals-mode-map 2225,87312 -(define-key coq-goals-mode-map 2226,87394 -(define-key coq-goals-mode-map 2227,87481 -(define-key coq-goals-mode-map 2228,87563 -(defvar last-coq-error-location 2237,87868 -(defun coq-get-last-error-location 2245,88252 -(defun coq-highlight-error 2295,90815 -(defun coq-highlight-error-hook 2323,91896 -(defun first-word-of-buffer 2333,92113 -(defun coq-show-first-goal 2341,92316 -(defvar coq-modeline-string2 2357,92981 -(defvar coq-modeline-string1 2358,93015 -(defvar coq-modeline-string0 2359,93049 -(defun coq-build-subgoals-string 2360,93090 -(defun coq-update-minor-mode-alist 2365,93256 -(defun is-not-split-vertic 2397,94649 -(defun optim-resp-windows 2406,95089 +coq/coq.el,9426 +(defcustom coq-prog-name61,1977 +(defcustom coq-translate-to-v8 80,2829 +(defun coq-build-prog-args 85,2944 +(defcustom coq-compiler95,3267 +(defcustom coq-dependency-analyzer101,3404 +(defcustom coq-use-makefile 107,3544 +(defcustom coq-default-undo-limit 113,3716 +(defconst coq-shell-init-cmd118,3844 +(defcustom coq-prog-env 127,4171 +(defconst coq-shell-restart-cmd 135,4420 +(defvar coq-shell-prompt-pattern137,4474 +(defvar coq-shell-cd 145,4777 +(defvar coq-shell-proof-completed-regexp 149,4937 +(defvar coq-goal-regexp152,5122 +(defun get-coq-library-directory 157,5218 +(defconst coq-library-directory 163,5400 +(defcustom coq-tags 166,5527 +(defconst coq-interrupt-regexp 171,5675 +(defcustom coq-www-home-page 174,5768 +(defcustom coq-end-goals-regexp-hide-subgoals 179,5875 +(defcustom coq-end-goals-regexp-show-subgoals 185,6112 +(defgroup coq-proof-tree 197,6413 +(defcustom coq-proof-tree-ignored-commands-regexp202,6553 +(defcustom coq-navigation-command-regexp208,6730 +(defcustom coq-proof-tree-cheating-regexp214,6902 +(defcustom coq-proof-tree-current-goal-regexp220,7042 +(defcustom coq-proof-tree-update-goal-regexp227,7296 +(defcustom coq-proof-tree-additional-subgoal-ID-regexp234,7530 +(defcustom coq-proof-tree-existential-regexp 240,7728 +(defcustom coq-proof-tree-instantiated-existential-regexp245,7882 +(defcustom coq-proof-tree-existentials-state-start-regexp251,8102 +(defcustom coq-proof-tree-existentials-state-end-regexp 257,8292 +(defcustom coq-proof-tree-proof-completed-regexp262,8461 +(defvar coq-outline-regexp274,8732 +(defvar coq-outline-heading-end-regexp 281,8945 +(defvar coq-shell-outline-regexp 283,8999 +(defvar coq-shell-outline-heading-end-regexp 284,9049 +(defconst coq-state-preserving-tactics-regexp287,9113 +(defconst coq-state-changing-commands-regexp289,9215 +(defconst coq-state-preserving-commands-regexp291,9324 +(defconst coq-commands-regexp293,9437 +(defvar coq-retractable-instruct-regexp295,9516 +(defvar coq-non-retractable-instruct-regexp297,9608 +(defcustom coq-use-smie 329,10304 +(defcustom coq-indent-box-style 335,10501 +(defconst coq-smie-grammar354,10795 +(defun coq-smie-search-token-forward 418,13720 +(defun coq-smie-search-token-backward 431,14227 +(defconst coq-smie-proof-end-tokens459,15562 +(defun coq-smie-forward-token 463,15692 +(defun coq-smie-backward-token 513,17645 +(defun coq-smie-rules 600,21089 +(defconst coq-script-command-end-regexp 682,24880 +(defun coq-script-parse-function 691,25309 +(defun coq-set-undo-limit 698,25535 +(defun build-list-id-from-string 702,25665 +(defun coq-last-prompt-info 711,26140 +(defun coq-last-prompt-info-safe 729,27034 +(defvar coq-last-but-one-statenum 737,27387 +(defvar coq-last-but-one-proofnum 744,27684 +(defvar coq-last-but-one-proofstack 747,27782 +(defsubst coq-get-span-statenum 750,27892 +(defsubst coq-get-span-proofnum 754,28007 +(defsubst coq-get-span-proofstack 758,28122 +(defsubst coq-set-span-statenum 762,28266 +(defsubst coq-get-span-goalcmd 766,28397 +(defsubst coq-set-span-goalcmd 770,28511 +(defsubst coq-set-span-proofnum 774,28641 +(defsubst coq-set-span-proofstack 778,28772 +(defsubst proof-last-locked-span 782,28932 +(defun proof-clone-buffer 786,29066 +(defun proof-store-buffer-win 800,29603 +(defun proof-store-response-win 811,30096 +(defun proof-store-goals-win 815,30223 +(defun coq-set-state-infos 827,30755 +(defun count-not-intersection 865,32845 +(defun coq-find-and-forget 895,34097 +(defvar coq-current-goal 922,35402 +(defun coq-goal-hyp 925,35467 +(defun coq-state-preserving-p 938,35941 +(defun coq-hide-additional-subgoals-switch 948,36235 +(defconst notation-print-kinds-table961,36600 +(defun coq-PrintScope 965,36767 +(defun coq-guess-or-ask-for-string 983,37316 +(defun coq-ask-do 997,37856 +(defsubst coq-put-into-brackets 1006,38241 +(defsubst coq-put-into-quotes 1009,38302 +(defun coq-SearchIsos 1012,38361 +(defun coq-SearchConstant 1020,38600 +(defun coq-Searchregexp 1024,38693 +(defun coq-SearchRewrite 1030,38834 +(defun coq-SearchAbout 1034,38931 +(defun coq-Print 1040,39074 +(defun coq-About 1045,39198 +(defun coq-LocateConstant 1050,39317 +(defun coq-LocateLibrary 1055,39420 +(defun coq-LocateNotation 1060,39537 +(defun coq-Pwd 1068,39768 +(defun coq-Inspect 1073,39892 +(defun coq-PrintSection(1077,39992 +(defun coq-Print-implicit 1081,40085 +(defun coq-Check 1086,40236 +(defun coq-Show 1091,40344 +(defun coq-Compile 1105,40787 +(defun coq-guess-command-line 1117,41105 +(defpacustom use-editing-holes 1154,42662 +(defun coq-mode-config 1163,42965 +(defun coq-shell-mode-config 1268,46776 +(defun coq-goals-mode-config 1341,49970 +(defun coq-response-config 1348,50214 +(defpacustom hide-additional-subgoals 1371,50931 +(defpacustom print-fully-explicit 1381,51241 +(defpacustom print-implicit 1386,51389 +(defpacustom print-coercions 1391,51555 +(defpacustom print-match-wildcards 1396,51699 +(defpacustom print-elim-types 1401,51879 +(defpacustom printing-depth 1406,52045 +(defpacustom undo-depth 1411,52206 +(defpacustom time-commands 1416,52372 +(defgroup coq-auto-compile 1427,52622 +(defpacustom compile-before-require 1432,52773 +(defcustom coq-compile-command 1444,53265 +(defconst coq-compile-substitution-list1474,54548 +(defcustom coq-load-path 1494,55469 +(defcustom coq-compile-auto-save 1545,57990 +(defcustom coq-lock-ancestors 1570,59048 +(defpacustom confirm-external-compilation 1579,59369 +(defcustom coq-load-path-include-current 1588,59676 +(defcustom coq-compile-ignored-directories 1597,59994 +(defcustom coq-compile-ignore-library-directory 1610,60627 +(defcustom coq-coqdep-error-regexp1622,61115 +(defconst coq-require-command-regexp1638,61833 +(defconst coq-require-id-regexp1645,62190 +(defvar coq-compile-history 1653,62624 +(defvar coq-compile-response-buffer 1656,62708 +(defvar coq-debug-auto-compilation 1660,62843 +(defun time-less-or-equal 1666,62951 +(defun coq-max-dep-mod-time 1674,63289 +(defun coq-prog-args 1697,64093 +(defun coq-lock-ancestor 1706,64352 +(defun coq-unlock-ancestor 1722,65127 +(defun coq-unlock-all-ancestors-of-span 1729,65422 +(defun coq-compile-ignore-file 1736,65718 +(defun coq-library-src-of-obj-file 1760,66605 +(defun coq-option-of-load-path-entry 1765,66837 +(defun coq-include-options 1781,67428 +(defun coq-init-compile-response-buffer 1801,68252 +(defun coq-display-compile-response-buffer 1824,69324 +(defun coq-get-library-dependencies 1838,69958 +(defun coq-compile-library 1885,72183 +(defun coq-compile-library-if-necessary 1912,73394 +(defun coq-make-lib-up-to-date 1958,75266 +(defun coq-auto-compile-externally 2014,77729 +(defun coq-map-module-id-to-obj-file 2057,79875 +(defun coq-check-module 2110,82477 +(defvar coq-process-require-current-buffer2138,83919 +(defun coq-compile-save-buffer-filter 2144,84184 +(defun coq-compile-save-some-buffers 2154,84598 +(defun coq-preprocess-require-commands 2176,85500 +(defun coq-switch-buffer-kill-proof-shell 2209,87069 +(defun coq-proof-tree-get-proof-info 2229,87702 +(defun coq-extract-instantiated-existentials 2239,88090 +(defun coq-show-sequent-command 2248,88482 +(defun coq-proof-tree-get-new-subgoals 2252,88636 +(defun coq-find-begin-of-unfinished-proof 2296,90761 +(defun coq-preprocessing 2321,91775 +(defun coq-fake-constant-markup 2335,92230 +(defun coq-create-span-menu 2351,92835 +(defconst module-kinds-table2369,93348 +(defconst modtype-kinds-table2373,93497 +(defun coq-insert-section-or-module 2377,93626 +(defconst reqkinds-kinds-table2398,94476 +(defun coq-insert-requires 2402,94620 +(defun coq-end-Section 2415,95099 +(defun coq-insert-intros 2433,95677 +(defun coq-insert-infoH-hook 2445,96208 +(defun coq-insert-as 2450,96416 +(defun coq-insert-match 2467,97109 +(defun coq-insert-solve-tactic 2496,98278 +(defun coq-insert-tactic 2502,98529 +(defun coq-insert-tactical 2508,98731 +(defun coq-insert-command 2514,98962 +(defun coq-insert-term 2519,99127 +(define-key coq-keymap 2524,99288 +(define-key coq-keymap 2525,99346 +(define-key coq-keymap 2526,99403 +(define-key coq-keymap 2527,99472 +(define-key coq-keymap 2528,99528 +(define-key coq-keymap 2529,99577 +(define-key coq-keymap 2530,99635 +(define-key coq-keymap 2531,99685 +(define-key coq-keymap 2532,99740 +(define-key coq-keymap 2534,99793 +(define-key coq-keymap 2536,99867 +(define-key coq-keymap 2537,99924 +(define-key coq-keymap 2540,99989 +(define-key coq-keymap 2541,100049 +(define-key coq-keymap 2543,100105 +(define-key coq-keymap 2544,100155 +(define-key coq-keymap 2545,100205 +(define-key coq-keymap 2546,100261 +(define-key coq-keymap 2547,100311 +(define-key coq-keymap 2548,100355 +(define-key coq-keymap 2549,100414 +(define-key coq-goals-mode-map 2552,100475 +(define-key coq-goals-mode-map 2553,100557 +(define-key coq-goals-mode-map 2554,100639 +(define-key coq-goals-mode-map 2555,100726 +(define-key coq-goals-mode-map 2556,100808 +(defvar last-coq-error-location 2565,101113 +(defun coq-get-last-error-location 2573,101497 +(defun coq-highlight-error 2623,104060 +(defun coq-highlight-error-hook 2651,105141 +(defun coq-first-word-before 2661,105358 +(defun coq-show-first-goal 2672,105690 +(defvar coq-modeline-string2 2688,106355 +(defvar coq-modeline-string1 2689,106389 +(defvar coq-modeline-string0 2690,106423 +(defun coq-build-subgoals-string 2691,106464 +(defun coq-update-minor-mode-alist 2696,106630 +(defun is-not-split-vertic 2728,108045 +(defun optim-resp-windows 2737,108485 coq/coq-indent.el,2565 (defconst coq-any-command-regexp20,368 @@ -258,127 +280,127 @@ coq/coq-indent.el,2565 (defconst coq-indent-pattern-regexp 68,2433 (defun coq-indent-goal-command-p 72,2536 (defconst coq-end-command-regexp94,3590 -(defun coq-search-comment-delimiter-forward 103,4054 -(defun coq-search-comment-delimiter-backward 112,4384 -(defun coq-skip-until-one-comment-backward 119,4658 -(defun coq-skip-until-one-comment-forward 134,5365 -(defun coq-looking-at-comment 145,5883 -(defun coq-find-comment-start 149,6024 -(defun coq-find-comment-end 160,6457 -(defun coq-looking-at-syntactic-context 172,6950 -(defconst coq-end-command-or-comment-regexp178,7172 -(defconst coq-end-command-or-comment-start-regexp181,7281 -(defun coq-find-not-in-comment-backward 184,7398 -(defun coq-find-not-in-comment-forward 204,8288 -(defun coq-is-on-ending-context 230,9480 -(defun coq-empty-command-p 239,9693 -(defun coq-script-parse-cmdend-forward 254,10412 -(defun coq-script-parse-cmdend-backward 303,12675 -(defun coq-find-current-start 341,14351 -(defun coq-find-real-start 350,14677 -(defun same-line 356,14895 -(defun coq-command-at-point 359,14982 -(defun coq-commands-at-line 374,15593 -(defun coq-indent-only-spaces-on-line 398,16559 -(defun coq-indent-find-reg 404,16836 -(defun coq-find-no-syntactic-on-line 418,17372 -(defun coq-back-to-indentation-prevline 431,17845 -(defun coq-find-unclosed 477,19912 -(defun coq-find-at-same-level-zero 507,21222 -(defun coq-find-unopened 536,22488 -(defun coq-find-last-unopened 579,23922 -(defun coq-end-offset 590,24319 -(defun coq-add-iter 615,25089 -(defun coq-goal-count 618,25195 -(defun coq-save-count 620,25267 -(defun coq-proof-count 625,25469 -(defun coq-goal-save-diff-maybe-proof 631,25757 -(defun coq-indent-command-offset 641,26051 -(defun coq-indent-expr-offset 707,29232 -(defun coq-indent-comment-offset 826,34114 -(defun coq-indent-offset 858,35566 -(defun coq-indent-calculate 877,36440 -(defun coq-indent-line 880,36528 -(defun coq-indent-line-not-comments 890,36894 -(defun coq-indent-region 900,37283 +(defun coq-search-comment-delimiter-forward 103,4095 +(defun coq-search-comment-delimiter-backward 112,4425 +(defun coq-skip-until-one-comment-backward 119,4699 +(defun coq-skip-until-one-comment-forward 134,5406 +(defun coq-looking-at-comment 145,5924 +(defun coq-find-comment-start 149,6065 +(defun coq-find-comment-end 160,6498 +(defun coq-looking-at-syntactic-context 172,6991 +(defconst coq-end-command-or-comment-regexp178,7213 +(defconst coq-end-command-or-comment-start-regexp181,7322 +(defun coq-find-not-in-comment-backward 184,7439 +(defun coq-find-not-in-comment-forward 204,8329 +(defun coq-is-on-ending-context 230,9521 +(defun coq-empty-command-p 239,9734 +(defun coq-script-parse-cmdend-forward 254,10475 +(defun coq-script-parse-cmdend-backward 306,12936 +(defun coq-find-current-start 347,14810 +(defun coq-find-real-start 356,15136 +(defun same-line 362,15354 +(defun coq-command-at-point 365,15441 +(defun coq-commands-at-line 380,16052 +(defun coq-indent-only-spaces-on-line 404,17018 +(defun coq-indent-find-reg 410,17295 +(defun coq-find-no-syntactic-on-line 424,17831 +(defun coq-back-to-indentation-prevline 437,18304 +(defun coq-find-unclosed 483,20371 +(defun coq-find-at-same-level-zero 513,21681 +(defun coq-find-unopened 542,22947 +(defun coq-find-last-unopened 585,24381 +(defun coq-end-offset 596,24778 +(defun coq-add-iter 621,25548 +(defun coq-goal-count 624,25654 +(defun coq-save-count 626,25726 +(defun coq-proof-count 631,25928 +(defun coq-goal-save-diff-maybe-proof 637,26216 +(defun coq-indent-command-offset 647,26510 +(defun coq-indent-expr-offset 713,29691 +(defun coq-indent-comment-offset 832,34573 +(defun coq-indent-offset 864,36025 +(defun coq-indent-calculate 883,36899 +(defun coq-indent-line 886,36987 +(defun coq-indent-line-not-comments 896,37353 +(defun coq-indent-region 906,37742 coq/coq-local-vars.el,229 -(defconst coq-local-vars-doc 21,445 -(defun coq-insert-coq-prog-name 84,2767 -(defun coq-read-directory 97,3318 -(defun coq-ask-load-path 114,4133 -(defun coq-ask-prog-name 132,4966 -(defun coq-ask-insert-coq-prog-name 149,5677 +(defconst coq-local-vars-doc 23,414 +(defun coq-insert-coq-prog-name 86,2736 +(defun coq-read-directory 99,3287 +(defun coq-ask-load-path 116,4102 +(defun coq-ask-prog-name 134,4935 +(defun coq-ask-insert-coq-prog-name 151,5646 coq/coq-syntax.el,2736 -(defcustom coq-user-tactics-db 21,583 -(defcustom coq-user-commands-db 38,1096 -(defcustom coq-user-tacticals-db 54,1615 -(defcustom coq-user-solve-tactics-db 70,2136 -(defcustom coq-user-cheat-tactics-db 86,2655 -(defcustom coq-user-reserved-db 105,3201 -(defvar coq-tactics-db123,3732 -(defvar coq-solve-tactics-db296,12866 -(defvar coq-solve-cheat-tactics-db323,13889 -(defvar coq-tacticals-db335,14064 -(defvar coq-decl-db359,14950 -(defvar coq-defn-db384,16406 -(defvar coq-goal-starters-db449,21128 -(defvar coq-other-commands-db479,22931 -(defvar coq-commands-db614,32916 -(defvar coq-terms-db621,33136 -(defun coq-count-match 683,35751 -(defun coq-module-opening-p 699,36480 -(defun coq-section-command-p 710,36891 -(defun coq-goal-command-str-p 714,36988 -(defun coq-goal-command-p 741,38090 -(defvar coq-keywords-save-strict751,38429 -(defvar coq-keywords-save758,38670 -(defun coq-save-command-p 763,38749 -(defvar coq-keywords-kill-goal774,39077 -(defvar coq-keywords-state-changing-misc-commands778,39167 -(defvar coq-keywords-goal781,39292 -(defvar coq-keywords-decl784,39375 -(defvar coq-keywords-defn787,39449 -(defvar coq-keywords-state-changing-commands791,39524 -(defvar coq-keywords-state-preserving-commands800,39784 -(defvar coq-keywords-commands805,40000 -(defvar coq-solve-tactics810,40148 -(defvar coq-solve-tactics-regexp814,40269 -(defvar coq-solve-cheat-tactics818,40403 -(defvar coq-solve-cheat-tactics-regexp822,40548 -(defvar coq-tacticals826,40706 -(defvar coq-reserved832,40845 -(defvar coq-reserved-regexp 842,41180 -(defvar coq-state-changing-tactics846,41291 -(defvar coq-state-preserving-tactics849,41400 -(defvar coq-tactics853,41514 -(defvar coq-tactics-regexp 856,41603 -(defvar coq-retractable-instruct859,41758 -(defvar coq-non-retractable-instruct862,41868 -(defvar coq-keywords866,41996 -(defun proof-regexp-alt-list-symb 872,42220 -(defvar coq-keywords-regexp 875,42325 -(defvar coq-symbols878,42398 -(defvar coq-error-regexp 900,42639 -(defvar coq-id 903,42867 -(defvar coq-id-shy 904,42892 -(defvar coq-ids 907,42994 -(defun coq-first-abstr-regexp 909,43060 -(defcustom coq-variable-highlight-enable 912,43155 -(defvar coq-font-lock-terms918,43282 -(defconst coq-save-command-regexp-strict940,44365 -(defconst coq-save-command-regexp946,44533 -(defconst coq-save-with-hole-regexp951,44686 -(defconst coq-goal-command-regexp955,44846 -(defconst coq-goal-with-hole-regexp958,44948 -(defconst coq-decl-with-hole-regexp962,45082 -(defconst coq-defn-with-hole-regexp969,45332 -(defconst coq-with-with-hole-regexp979,45622 -(defvar coq-font-lock-keywords-1994,46152 -(defvar coq-font-lock-keywords 1022,47487 -(defun coq-init-syntax-table 1024,47545 -(defconst coq-generic-expression1049,48272 +(defcustom coq-user-tactics-db 21,533 +(defcustom coq-user-commands-db 38,1046 +(defcustom coq-user-tacticals-db 54,1565 +(defcustom coq-user-solve-tactics-db 70,2086 +(defcustom coq-user-cheat-tactics-db 86,2605 +(defcustom coq-user-reserved-db 105,3151 +(defvar coq-tactics-db123,3682 +(defvar coq-solve-tactics-db296,12816 +(defvar coq-solve-cheat-tactics-db323,13839 +(defvar coq-tacticals-db335,14014 +(defvar coq-decl-db359,14900 +(defvar coq-defn-db384,16356 +(defvar coq-goal-starters-db449,21078 +(defvar coq-other-commands-db479,22881 +(defvar coq-commands-db614,32866 +(defvar coq-terms-db621,33086 +(defun coq-count-match 683,35701 +(defun coq-module-opening-p 699,36430 +(defun coq-section-command-p 710,36841 +(defun coq-goal-command-str-p 714,36938 +(defun coq-goal-command-p 741,38040 +(defvar coq-keywords-save-strict751,38379 +(defvar coq-keywords-save758,38620 +(defun coq-save-command-p 763,38699 +(defvar coq-keywords-kill-goal774,39027 +(defvar coq-keywords-state-changing-misc-commands778,39117 +(defvar coq-keywords-goal781,39242 +(defvar coq-keywords-decl784,39325 +(defvar coq-keywords-defn787,39399 +(defvar coq-keywords-state-changing-commands791,39474 +(defvar coq-keywords-state-preserving-commands800,39734 +(defvar coq-keywords-commands805,39950 +(defvar coq-solve-tactics810,40098 +(defvar coq-solve-tactics-regexp814,40219 +(defvar coq-solve-cheat-tactics818,40353 +(defvar coq-solve-cheat-tactics-regexp822,40498 +(defvar coq-tacticals826,40656 +(defvar coq-reserved832,40795 +(defvar coq-reserved-regexp 842,41130 +(defvar coq-state-changing-tactics846,41241 +(defvar coq-state-preserving-tactics849,41350 +(defvar coq-tactics853,41464 +(defvar coq-tactics-regexp 856,41553 +(defvar coq-retractable-instruct859,41708 +(defvar coq-non-retractable-instruct862,41818 +(defvar coq-keywords866,41946 +(defun proof-regexp-alt-list-symb 872,42170 +(defvar coq-keywords-regexp 875,42275 +(defvar coq-symbols878,42348 +(defvar coq-error-regexp 900,42589 +(defvar coq-id 903,42817 +(defvar coq-id-shy 904,42842 +(defvar coq-ids 907,42944 +(defun coq-first-abstr-regexp 909,43010 +(defcustom coq-variable-highlight-enable 912,43105 +(defvar coq-font-lock-terms918,43232 +(defconst coq-save-command-regexp-strict940,44315 +(defconst coq-save-command-regexp946,44483 +(defconst coq-save-with-hole-regexp951,44636 +(defconst coq-goal-command-regexp955,44796 +(defconst coq-goal-with-hole-regexp958,44898 +(defconst coq-decl-with-hole-regexp962,45032 +(defconst coq-defn-with-hole-regexp969,45282 +(defconst coq-with-with-hole-regexp979,45572 +(defvar coq-font-lock-keywords-1994,46102 +(defvar coq-font-lock-keywords 1022,47437 +(defun coq-init-syntax-table 1024,47495 +(defconst coq-generic-expression1049,48222 coq/coq-unicode-tokens.el,454 (defconst coq-token-format 39,1427 @@ -394,103 +416,103 @@ coq/coq-unicode-tokens.el,454 (defconst coq-control-regions266,7080 hol98/hol98.el,121 -(defvar hol98-keywords 17,419 -(defvar hol98-rules 18,447 -(defvar hol98-tactics 19,472 -(defvar hol98-tacticals 20,499 +(defvar hol98-keywords 17,374 +(defvar hol98-rules 18,402 +(defvar hol98-tactics 19,427 +(defvar hol98-tacticals 20,454 isar/isabelle-system.el,1254 -(defgroup isabelle 28,797 -(defcustom isabelle-web-page32,925 -(defcustom isa-isabelle-command41,1142 -(defvar isabelle-not-found 59,1824 -(defun isa-set-isabelle-command 62,1939 -(defun isa-shell-command-to-string 85,2957 -(defun isa-getenv 91,3181 -(defcustom isabelle-program-name-override 111,3880 -(defun isa-tool-list-logics 122,4226 -(defcustom isabelle-logics-available 129,4472 -(defcustom isabelle-chosen-logic 139,4809 -(defvar isabelle-chosen-logic-prev 155,5393 -(defun isabelle-hack-local-variables-function 158,5513 -(defun isabelle-set-prog-name 170,5952 -(defun isabelle-choose-logic 194,7072 -(defun isa-view-doc 213,7834 -(defun isa-tool-list-docs 220,8060 -(defconst isabelle-verbatim-regexp 238,8790 -(defun isabelle-verbatim 241,8932 -(defcustom isabelle-refresh-logics 248,9093 -(defvar isabelle-docs-menu256,9421 -(defvar isabelle-logics-menu-entries 263,9706 -(defun isabelle-logics-menu-calculate 266,9779 -(defvar isabelle-time-to-refresh-logics 287,10421 -(defun isabelle-logics-menu-refresh 291,10516 -(defun isabelle-menu-bar-update-logics 306,11149 -(defun isabelle-load-isar-keywords 322,11778 -(defun isabelle-create-span-menu 343,12506 -(defun isabelle-xml-sml-escapes 359,12937 -(defun isabelle-process-pgip 362,13038 +(defgroup isabelle 31,822 +(defcustom isabelle-web-page35,950 +(defcustom isa-isabelle-command44,1167 +(defvar isabelle-not-found 62,1849 +(defun isa-set-isabelle-command 65,1964 +(defun isa-shell-command-to-string 88,2982 +(defun isa-getenv 94,3206 +(defcustom isabelle-program-name-override 114,3905 +(defun isa-tool-list-logics 125,4251 +(defcustom isabelle-logics-available 132,4497 +(defcustom isabelle-chosen-logic 142,4834 +(defvar isabelle-chosen-logic-prev 158,5418 +(defun isabelle-hack-local-variables-function 161,5538 +(defun isabelle-set-prog-name 173,5977 +(defun isabelle-choose-logic 197,7097 +(defun isa-view-doc 216,7859 +(defun isa-tool-list-docs 223,8085 +(defconst isabelle-verbatim-regexp 241,8815 +(defun isabelle-verbatim 244,8957 +(defcustom isabelle-refresh-logics 251,9118 +(defvar isabelle-docs-menu259,9446 +(defvar isabelle-logics-menu-entries 266,9731 +(defun isabelle-logics-menu-calculate 269,9804 +(defvar isabelle-time-to-refresh-logics 290,10446 +(defun isabelle-logics-menu-refresh 294,10541 +(defun isabelle-menu-bar-update-logics 309,11188 +(defun isabelle-load-isar-keywords 325,11817 +(defun isabelle-create-span-menu 346,12545 +(defun isabelle-xml-sml-escapes 362,12976 +(defun isabelle-process-pgip 365,13077 isar/isar-autotest.el,31 -(defvar isar-long-tests 8,186 +(defvar isar-long-tests 8,133 isar/isar.el,1595 -(defcustom isar-keywords-name 39,915 -(defpgdefault completion-table 55,1426 -(defcustom isar-web-page57,1479 -(defun isar-strip-terminators 71,1829 -(defun isar-markup-ml 83,2185 -(defun isar-mode-config-set-variables 88,2320 -(defun isar-shell-mode-config-set-variables 153,5119 -(defun isar-set-proof-find-theorems-command 235,8309 -(defpacustom use-find-theorems-form 241,8493 -(defun isar-set-undo-commands 246,8659 -(defpacustom use-linear-undo 261,9292 -(defun isar-configure-from-settings 266,9450 -(defun isar-remove-file 274,9600 -(defun isar-shell-compute-new-files-list 286,9904 -(define-derived-mode isar-shell-mode 305,10474 -(define-derived-mode isar-response-mode 310,10601 -(define-derived-mode isar-goals-mode 315,10734 -(define-derived-mode isar-mode 320,10860 -(defpgdefault menu-entries372,12575 -(defun isar-set-command 403,13769 -(defpgdefault help-menu-entries 408,13899 -(defun isar-count-undos 411,13975 -(defun isar-find-and-forget 437,14941 -(defun isar-goal-command-p 473,16284 -(defun isar-global-save-command-p 478,16461 -(defvar isar-current-goal 499,17245 -(defun isar-state-preserving-p 502,17311 -(defvar isar-shell-current-line-width 527,18160 -(defun isar-shell-adjust-line-width 532,18352 -(defsubst isar-string-wrapping 555,19117 -(defsubst isar-positions-of 564,19311 -(defcustom isar-wrap-commands-singly 570,19516 -(defun isar-command-wrapping 576,19712 -(defun isar-preprocessing 584,20026 -(defun isar-mode-config 602,20577 -(defun isar-shell-mode-config 616,21230 -(defun isar-response-mode-config 626,21579 -(defun isar-goals-mode-config 636,21914 - -isar/isar-find-theorems.el,779 -(defvar isar-find-theorems-data 19,565 -(defun isar-find-theorems-minibuffer 35,1039 -(defun isar-find-theorems-form 49,1658 -(defvar isar-find-theorems-widget-number 92,3532 -(defvar isar-find-theorems-widget-pattern 95,3630 -(defvar isar-find-theorems-widget-intro 98,3722 -(defvar isar-find-theorems-widget-elim 101,3808 -(defvar isar-find-theorems-widget-dest 104,3892 -(defvar isar-find-theorems-widget-name 107,3976 -(defvar isar-find-theorems-widget-simp 110,4063 -(defun isar-find-theorems-create-searchform115,4209 -(defun isar-find-theorems-create-help 255,8752 -(defun isar-find-theorems-submit-searchform298,10924 -(defun isar-find-theorems-parse-criteria 376,13294 -(defun isar-find-theorems-parse-number 469,16275 -(defun isar-find-theorems-filter-empty 479,16552 +(defcustom isar-keywords-name 41,895 +(defpgdefault completion-table 57,1406 +(defcustom isar-web-page59,1459 +(defun isar-strip-terminators 73,1809 +(defun isar-markup-ml 85,2165 +(defun isar-mode-config-set-variables 90,2300 +(defun isar-shell-mode-config-set-variables 155,5099 +(defun isar-set-proof-find-theorems-command 237,8289 +(defpacustom use-find-theorems-form 243,8473 +(defun isar-set-undo-commands 248,8639 +(defpacustom use-linear-undo 263,9272 +(defun isar-configure-from-settings 268,9430 +(defun isar-remove-file 276,9580 +(defun isar-shell-compute-new-files-list 288,9884 +(define-derived-mode isar-shell-mode 307,10454 +(define-derived-mode isar-response-mode 312,10581 +(define-derived-mode isar-goals-mode 317,10714 +(define-derived-mode isar-mode 322,10840 +(defpgdefault menu-entries374,12555 +(defun isar-set-command 405,13749 +(defpgdefault help-menu-entries 410,13879 +(defun isar-count-undos 413,13955 +(defun isar-find-and-forget 439,14921 +(defun isar-goal-command-p 475,16264 +(defun isar-global-save-command-p 480,16441 +(defvar isar-current-goal 501,17225 +(defun isar-state-preserving-p 504,17291 +(defvar isar-shell-current-line-width 529,18140 +(defun isar-shell-adjust-line-width 534,18332 +(defsubst isar-string-wrapping 557,19097 +(defsubst isar-positions-of 566,19291 +(defcustom isar-wrap-commands-singly 572,19496 +(defun isar-command-wrapping 578,19692 +(defun isar-preprocessing 586,20006 +(defun isar-mode-config 604,20557 +(defun isar-shell-mode-config 618,21210 +(defun isar-response-mode-config 628,21559 +(defun isar-goals-mode-config 638,21894 + +isar/isar-find-theorems.el,778 +(defvar isar-find-theorems-data 19,507 +(defun isar-find-theorems-minibuffer 35,981 +(defun isar-find-theorems-form 49,1600 +(defvar isar-find-theorems-widget-number 92,3474 +(defvar isar-find-theorems-widget-pattern 95,3572 +(defvar isar-find-theorems-widget-intro 98,3664 +(defvar isar-find-theorems-widget-elim 101,3750 +(defvar isar-find-theorems-widget-dest 104,3834 +(defvar isar-find-theorems-widget-name 107,3918 +(defvar isar-find-theorems-widget-simp 110,4005 +(defun isar-find-theorems-create-searchform115,4151 +(defun isar-find-theorems-create-help 255,8694 +(defun isar-find-theorems-submit-searchform298,10866 +(defun isar-find-theorems-parse-criteria 376,13236 +(defun isar-find-theorems-parse-number 469,16217 +(defun isar-find-theorems-filter-empty 479,16494 isar/isar-keywords.el,1064 (defconst isar-keywords-major7,222 @@ -519,106 +541,106 @@ isar/isar-keywords.el,1064 (defconst isar-keywords-proof-script648,11005 isar/isar-mmm.el,81 -(defconst isar-start-latex-regexp24,744 -(defconst isar-start-sml-regexp36,1172 +(defconst isar-start-latex-regexp24,696 +(defconst isar-start-sml-regexp36,1124 isar/isar-syntax.el,4005 -(defconst isar-script-syntax-table-entries18,483 -(defconst isar-script-syntax-table-alist42,885 -(defun isar-init-syntax-table 51,1168 -(defun isar-init-output-syntax-table 59,1415 -(defconst isar-keyword-begin 74,1857 -(defconst isar-keyword-end 75,1895 -(defconst isar-keywords-theory-enclose77,1930 -(defconst isar-keywords-theory82,2068 -(defconst isar-keywords-save87,2199 -(defconst isar-keywords-proof-enclose92,2314 -(defconst isar-keywords-proof98,2475 -(defconst isar-keywords-proof-context105,2652 -(defconst isar-keywords-local-goal109,2759 -(defconst isar-keywords-proper113,2864 -(defconst isar-keywords-improper118,2983 -(defconst isar-keyword-level-alist123,3115 -(defconst isar-keywords-outline 138,3586 -(defconst isar-keywords-indent-open141,3662 -(defconst isar-keywords-indent-close148,3848 -(defconst isar-keywords-indent-enclose153,3981 -(defconst isar-ext-first 163,4210 -(defconst isar-ext-rest 164,4277 -(defconst isar-text 166,4349 -(defconst isar-long-id-stuff 167,4382 -(defconst isar-id 168,4456 -(defconst isar-idx 169,4526 -(defconst isar-string 171,4585 -(defun isar-ids-to-regexp 173,4645 -(defconst isar-any-command-regexp205,6437 -(defconst isar-name-regexp212,6810 -(defconst isar-improper-regexp218,7105 -(defconst isar-save-command-regexp222,7239 -(defconst isar-global-save-command-regexp225,7340 -(defconst isar-goal-command-regexp228,7454 -(defconst isar-local-goal-command-regexp231,7562 -(defconst isar-comment-start 234,7675 -(defconst isar-comment-end 235,7710 -(defconst isar-comment-start-regexp 236,7743 -(defconst isar-comment-end-regexp 237,7814 -(defconst isar-string-start-regexp 239,7882 -(defconst isar-string-end-regexp 240,7934 -(defun isar-syntactic-context 242,7985 -(defconst isar-antiq-regexp257,8380 -(defconst isar-nesting-regexp263,8531 -(defun isar-nesting 266,8629 -(defun isar-match-nesting 278,9022 -(defface isabelle-string-face 290,9356 -(defface isabelle-quote-face 298,9556 -(defface isabelle-class-name-face306,9752 -(defface isabelle-tfree-name-face314,9939 -(defface isabelle-tvar-name-face322,10132 -(defface isabelle-free-name-face330,10324 -(defface isabelle-bound-name-face338,10512 -(defface isabelle-var-name-face346,10703 -(defconst isabelle-string-face 354,10894 -(defconst isabelle-quote-face 355,10948 -(defconst isabelle-class-name-face 356,11001 -(defconst isabelle-tfree-name-face 357,11063 -(defconst isabelle-tvar-name-face 358,11125 -(defconst isabelle-free-name-face 359,11186 -(defconst isabelle-bound-name-face 360,11247 -(defconst isabelle-var-name-face 361,11309 -(defun isar-font-lock-fontify-syntactically-region 367,11458 -(defvar isar-font-lock-keywords-1402,12736 -(defun isar-output-flkprops 420,13744 -(defun isar-output-flk 426,13996 -(defvar isar-output-font-lock-keywords-1429,14105 -(defun isar-strip-output-markup 453,15104 -(defconst isar-shell-font-lock-keywords457,15240 -(defvar isar-goals-font-lock-keywords460,15324 -(defconst isar-linear-undo 494,16003 -(defconst isar-undo 496,16046 -(defconst isar-pr498,16089 -(defun isar-remove 505,16247 -(defun isar-undos 508,16322 -(defun isar-cannot-undo 518,16556 -(defconst isar-undo-commands521,16626 -(defconst isar-theory-start-regexp529,16763 -(defconst isar-end-regexp535,16921 -(defconst isar-undo-fail-regexp539,17022 -(defconst isar-undo-skip-regexp543,17126 -(defconst isar-undo-ignore-regexp546,17247 -(defconst isar-undo-remove-regexp549,17312 -(defconst isar-keywords-imenu557,17469 -(defconst isar-entity-regexp 564,17660 -(defconst isar-named-entity-regexp567,17756 -(defconst isar-named-entity-name-match-number572,17886 -(defconst isar-generic-expression575,17987 -(defconst isar-indent-any-regexp586,18221 -(defconst isar-indent-inner-regexp588,18314 -(defconst isar-indent-enclose-regexp590,18380 -(defconst isar-indent-open-regexp592,18496 -(defconst isar-indent-close-regexp594,18606 -(defconst isar-outline-regexp600,18743 -(defconst isar-outline-heading-end-regexp 604,18896 -(defconst isar-outline-heading-alist 606,18945 +(defconst isar-script-syntax-table-entries18,432 +(defconst isar-script-syntax-table-alist42,834 +(defun isar-init-syntax-table 51,1117 +(defun isar-init-output-syntax-table 59,1364 +(defconst isar-keyword-begin 74,1806 +(defconst isar-keyword-end 75,1844 +(defconst isar-keywords-theory-enclose77,1879 +(defconst isar-keywords-theory82,2017 +(defconst isar-keywords-save87,2148 +(defconst isar-keywords-proof-enclose92,2263 +(defconst isar-keywords-proof98,2424 +(defconst isar-keywords-proof-context105,2601 +(defconst isar-keywords-local-goal109,2708 +(defconst isar-keywords-proper113,2813 +(defconst isar-keywords-improper118,2932 +(defconst isar-keyword-level-alist123,3064 +(defconst isar-keywords-outline 138,3535 +(defconst isar-keywords-indent-open141,3611 +(defconst isar-keywords-indent-close148,3797 +(defconst isar-keywords-indent-enclose153,3930 +(defconst isar-ext-first 163,4159 +(defconst isar-ext-rest 164,4226 +(defconst isar-text 166,4298 +(defconst isar-long-id-stuff 167,4331 +(defconst isar-id 168,4405 +(defconst isar-idx 169,4475 +(defconst isar-string 171,4534 +(defun isar-ids-to-regexp 173,4594 +(defconst isar-any-command-regexp205,6386 +(defconst isar-name-regexp212,6759 +(defconst isar-improper-regexp218,7054 +(defconst isar-save-command-regexp222,7188 +(defconst isar-global-save-command-regexp225,7289 +(defconst isar-goal-command-regexp228,7403 +(defconst isar-local-goal-command-regexp231,7511 +(defconst isar-comment-start 234,7624 +(defconst isar-comment-end 235,7659 +(defconst isar-comment-start-regexp 236,7692 +(defconst isar-comment-end-regexp 237,7763 +(defconst isar-string-start-regexp 239,7831 +(defconst isar-string-end-regexp 240,7883 +(defun isar-syntactic-context 242,7934 +(defconst isar-antiq-regexp257,8329 +(defconst isar-nesting-regexp263,8480 +(defun isar-nesting 266,8578 +(defun isar-match-nesting 278,8971 +(defface isabelle-string-face 290,9305 +(defface isabelle-quote-face 298,9505 +(defface isabelle-class-name-face306,9701 +(defface isabelle-tfree-name-face314,9888 +(defface isabelle-tvar-name-face322,10081 +(defface isabelle-free-name-face330,10273 +(defface isabelle-bound-name-face338,10461 +(defface isabelle-var-name-face346,10652 +(defconst isabelle-string-face 354,10843 +(defconst isabelle-quote-face 355,10897 +(defconst isabelle-class-name-face 356,10950 +(defconst isabelle-tfree-name-face 357,11012 +(defconst isabelle-tvar-name-face 358,11074 +(defconst isabelle-free-name-face 359,11135 +(defconst isabelle-bound-name-face 360,11196 +(defconst isabelle-var-name-face 361,11258 +(defun isar-font-lock-fontify-syntactically-region 367,11407 +(defvar isar-font-lock-keywords-1402,12685 +(defun isar-output-flkprops 420,13693 +(defun isar-output-flk 426,13945 +(defvar isar-output-font-lock-keywords-1429,14054 +(defun isar-strip-output-markup 453,15053 +(defconst isar-shell-font-lock-keywords457,15189 +(defvar isar-goals-font-lock-keywords460,15273 +(defconst isar-linear-undo 494,15952 +(defconst isar-undo 496,15995 +(defconst isar-pr498,16038 +(defun isar-remove 505,16196 +(defun isar-undos 508,16271 +(defun isar-cannot-undo 518,16505 +(defconst isar-undo-commands521,16575 +(defconst isar-theory-start-regexp529,16712 +(defconst isar-end-regexp535,16870 +(defconst isar-undo-fail-regexp539,16971 +(defconst isar-undo-skip-regexp543,17075 +(defconst isar-undo-ignore-regexp546,17196 +(defconst isar-undo-remove-regexp549,17261 +(defconst isar-keywords-imenu557,17418 +(defconst isar-entity-regexp 564,17609 +(defconst isar-named-entity-regexp567,17705 +(defconst isar-named-entity-name-match-number572,17835 +(defconst isar-generic-expression575,17936 +(defconst isar-indent-any-regexp586,18170 +(defconst isar-indent-inner-regexp588,18263 +(defconst isar-indent-enclose-regexp590,18329 +(defconst isar-indent-open-regexp592,18445 +(defconst isar-indent-close-regexp594,18555 +(defconst isar-outline-regexp600,18692 +(defconst isar-outline-heading-end-regexp 604,18845 +(defconst isar-outline-heading-alist 606,18894 isar/isar-unicode-tokens.el,1363 (defgroup isabelle-tokens 25,672 @@ -653,93 +675,93 @@ isar/isar-unicode-tokens.el,1363 (defconst isar-tokens-customizable-variables661,17747 lego/lego.el,1636 -(defcustom lego-tags 21,534 -(defcustom lego-test-all-name 26,670 -(defpgdefault help-menu-entries32,828 -(defpgdefault menu-entries36,988 -(defvar lego-shell-handle-output47,1289 -(defconst lego-process-config55,1587 -(defconst lego-pretty-set-width 66,2018 -(defconst lego-interrupt-regexp 70,2160 -(defcustom lego-www-home-page 75,2277 -(defcustom lego-www-latest-release80,2401 -(defcustom lego-www-refcard86,2576 -(defcustom lego-library-www-page92,2725 -(defvar lego-prog-name 101,2941 -(defvar lego-shell-cd 104,3010 -(defvar lego-shell-proof-completed-regexp 107,3109 -(defvar lego-save-command-regexp110,3249 -(defvar lego-goal-command-regexp112,3339 -(defvar lego-kill-goal-command 115,3430 -(defvar lego-forget-id-command 116,3473 -(defvar lego-undoable-commands-regexp118,3519 -(defvar lego-goal-regexp 127,3893 -(defvar lego-outline-regexp129,3938 -(defvar lego-outline-heading-end-regexp 135,4113 -(defvar lego-shell-outline-regexp 137,4166 -(defvar lego-shell-outline-heading-end-regexp 138,4218 -(define-derived-mode lego-shell-mode 144,4497 -(define-derived-mode lego-mode 151,4658 -(define-derived-mode lego-goals-mode 162,4968 -(defun lego-count-undos 173,5394 -(defun lego-goal-command-p 192,6131 -(defun lego-find-and-forget 197,6302 -(defun lego-goal-hyp 239,8138 -(defun lego-state-preserving-p 248,8335 -(defvar lego-shell-current-line-width 264,9038 -(defun lego-shell-adjust-line-width 272,9345 -(defun lego-mode-config 289,10046 -(defun lego-equal-module-filename 357,12097 -(defun lego-shell-compute-new-files-list 363,12372 -(defun lego-shell-mode-config 373,12755 -(defun lego-goals-mode-config 420,14422 - -lego/lego-syntax.el,600 -(defconst lego-keywords-goal 15,358 -(defconst lego-keywords-save 17,401 -(defconst lego-commands19,472 -(defconst lego-keywords31,1030 -(defconst lego-tacticals 36,1207 -(defconst lego-error-regexp 39,1315 -(defvar lego-id 42,1473 -(defvar lego-ids 44,1500 -(defconst lego-arg-list-regexp 48,1696 -(defun lego-decl-defn-regexp 51,1812 -(defconst lego-definiendum-alternative-regexp59,2184 -(defvar lego-font-lock-terms63,2368 -(defconst lego-goal-with-hole-regexp89,3221 -(defconst lego-save-with-hole-regexp94,3443 -(defvar lego-font-lock-keywords-199,3660 -(defun lego-init-syntax-table 110,4122 - -phox/phox.el,555 -(defcustom phox-prog-name 32,916 -(defcustom phox-web-page37,1018 -(defcustom phox-doc-dir43,1168 -(defcustom phox-lib-dir49,1315 -(defcustom phox-tags-program55,1458 -(defcustom phox-tags-doc61,1637 -(defcustom phox-etags67,1774 -(defpgdefault menu-entries88,2224 -(defun phox-config 102,2417 -(defun phox-shell-config 146,4343 -(define-derived-mode phox-mode 170,5205 -(define-derived-mode phox-shell-mode 186,5668 -(define-derived-mode phox-response-mode 191,5796 -(define-derived-mode phox-goals-mode 201,6157 -(defpgdefault completion-table224,6943 +(defcustom lego-tags 21,490 +(defcustom lego-test-all-name 26,626 +(defpgdefault help-menu-entries32,784 +(defpgdefault menu-entries36,944 +(defvar lego-shell-handle-output47,1245 +(defconst lego-process-config55,1543 +(defconst lego-pretty-set-width 66,1974 +(defconst lego-interrupt-regexp 70,2116 +(defcustom lego-www-home-page 75,2233 +(defcustom lego-www-latest-release80,2357 +(defcustom lego-www-refcard86,2532 +(defcustom lego-library-www-page92,2681 +(defvar lego-prog-name 101,2897 +(defvar lego-shell-cd 104,2966 +(defvar lego-shell-proof-completed-regexp 107,3065 +(defvar lego-save-command-regexp110,3205 +(defvar lego-goal-command-regexp112,3295 +(defvar lego-kill-goal-command 115,3386 +(defvar lego-forget-id-command 116,3429 +(defvar lego-undoable-commands-regexp118,3475 +(defvar lego-goal-regexp 127,3849 +(defvar lego-outline-regexp129,3894 +(defvar lego-outline-heading-end-regexp 135,4069 +(defvar lego-shell-outline-regexp 137,4122 +(defvar lego-shell-outline-heading-end-regexp 138,4174 +(define-derived-mode lego-shell-mode 144,4453 +(define-derived-mode lego-mode 151,4614 +(define-derived-mode lego-goals-mode 162,4924 +(defun lego-count-undos 173,5350 +(defun lego-goal-command-p 192,6087 +(defun lego-find-and-forget 197,6258 +(defun lego-goal-hyp 239,8094 +(defun lego-state-preserving-p 248,8291 +(defvar lego-shell-current-line-width 264,8994 +(defun lego-shell-adjust-line-width 272,9301 +(defun lego-mode-config 289,10002 +(defun lego-equal-module-filename 357,12053 +(defun lego-shell-compute-new-files-list 363,12328 +(defun lego-shell-mode-config 373,12711 +(defun lego-goals-mode-config 420,14378 + +lego/lego-syntax.el,599 +(defconst lego-keywords-goal 15,307 +(defconst lego-keywords-save 17,350 +(defconst lego-commands19,421 +(defconst lego-keywords31,979 +(defconst lego-tacticals 36,1156 +(defconst lego-error-regexp 39,1264 +(defvar lego-id 42,1422 +(defvar lego-ids 44,1449 +(defconst lego-arg-list-regexp 48,1645 +(defun lego-decl-defn-regexp 51,1761 +(defconst lego-definiendum-alternative-regexp59,2133 +(defvar lego-font-lock-terms63,2317 +(defconst lego-goal-with-hole-regexp89,3170 +(defconst lego-save-with-hole-regexp94,3392 +(defvar lego-font-lock-keywords-199,3609 +(defun lego-init-syntax-table 110,4071 + +phox/phox.el,554 +(defcustom phox-prog-name 32,881 +(defcustom phox-web-page37,983 +(defcustom phox-doc-dir43,1133 +(defcustom phox-lib-dir49,1280 +(defcustom phox-tags-program55,1423 +(defcustom phox-tags-doc61,1602 +(defcustom phox-etags67,1739 +(defpgdefault menu-entries88,2189 +(defun phox-config 102,2382 +(defun phox-shell-config 146,4308 +(define-derived-mode phox-mode 170,5170 +(define-derived-mode phox-shell-mode 186,5633 +(define-derived-mode phox-response-mode 191,5761 +(define-derived-mode phox-goals-mode 201,6122 +(defpgdefault completion-table224,6908 phox/phox-extraction.el,383 -(defvar phox-prog-orig 19,619 -(defun phox-prog-flags-modify(21,687 -(defun phox-prog-flags-extract(50,1488 -(defun phox-prog-flags-erase(61,1778 -(defun phox-toggle-extraction(69,1974 -(defun phox-compile-theorem(81,2376 -(defun phox-compile-theorem-on-cursor(87,2601 -(defun phox-output 103,3079 -(defun phox-output-theorem 113,3291 -(defun phox-output-theorem-on-cursor(120,3590 +(defvar phox-prog-orig 19,584 +(defun phox-prog-flags-modify(21,652 +(defun phox-prog-flags-extract(50,1453 +(defun phox-prog-flags-erase(61,1743 +(defun phox-toggle-extraction(69,1939 +(defun phox-compile-theorem(81,2341 +(defun phox-compile-theorem-on-cursor(87,2566 +(defun phox-output 103,3044 +(defun phox-output-theorem 113,3256 +(defun phox-output-theorem-on-cursor(120,3555 phox/phox-font.el,231 (defvar phox-sym-lock-enabled 1,0 @@ -749,79 +771,79 @@ phox/phox-font.el,231 (defconst phox-sym-lock-keywords-table70,2628 (defun phox-sym-lock-start 93,3202 -phox/phox-fun.el,1659 -(defconst phox-forget-id-command 11,186 -(defconst phox-forget-proof-command 12,232 -(defconst phox-forget-new-elim-command 13,287 -(defconst phox-forget-new-intro-command 14,345 -(defconst phox-forget-new-equation-command 15,405 -(defconst phox-forget-close-def-command 16,471 -(defconst phox-comments-regexp 18,597 -(defconst phox-strict-comments-regexp 20,776 -(defconst phox-ident-regexp 21,941 -(defconst phox-inductive-option 22,1027 -(defconst phox-spaces-regexp 23,1079 -(defconst phox-sy-definition-regexp 24,1122 -(defconst phox-sy-inductive-regexp 28,1309 -(defconst phox-inductive-regexp 34,1522 -(defconst phox-data-regexp 40,1673 -(defconst phox-definition-regexp 46,1827 -(defconst phox-prove-claim-regexp 50,1971 -(defconst phox-new-elim-regexp 54,2077 -(defconst phox-new-intro-regexp 57,2196 -(defconst phox-new-rewrite-regexp 60,2317 -(defconst phox-new-equation-regexp 63,2442 -(defconst phox-close-def-regexp 66,2569 -(defun phox-init-syntax-table 71,2706 -(defvar phox-top-keywords87,3178 -(defvar phox-proof-keywords135,3633 -(defun phox-find-and-forget 176,3983 -(defalias 'phox-assert-next-command-interactive phox-assert-next-command-interactive255,6399 -(defun phox-depend-theorem(274,7365 -(defun phox-eshow-extlist(283,7654 -(defun phox-flag-name(297,8251 -(defun phox-path(308,8553 -(defun phox-print-expression(319,8789 -(defun phox-print-sort-expression(332,9245 -(defun phox-priority-symbols-list(343,9557 -(defun phox-search-string(355,9929 -(defun phox-constraints(370,10454 -(defun phox-goals(381,10710 -(defvar phox-state-menu393,10919 -(defun phox-delete-symbol(418,11909 -(defun phox-delete-symbol-on-cursor(424,12117 +phox/phox-fun.el,1658 +(defconst phox-forget-id-command 11,151 +(defconst phox-forget-proof-command 12,197 +(defconst phox-forget-new-elim-command 13,252 +(defconst phox-forget-new-intro-command 14,310 +(defconst phox-forget-new-equation-command 15,370 +(defconst phox-forget-close-def-command 16,436 +(defconst phox-comments-regexp 18,562 +(defconst phox-strict-comments-regexp 20,741 +(defconst phox-ident-regexp 21,906 +(defconst phox-inductive-option 22,992 +(defconst phox-spaces-regexp 23,1044 +(defconst phox-sy-definition-regexp 24,1087 +(defconst phox-sy-inductive-regexp 28,1274 +(defconst phox-inductive-regexp 34,1487 +(defconst phox-data-regexp 40,1638 +(defconst phox-definition-regexp 46,1792 +(defconst phox-prove-claim-regexp 50,1936 +(defconst phox-new-elim-regexp 54,2042 +(defconst phox-new-intro-regexp 57,2161 +(defconst phox-new-rewrite-regexp 60,2282 +(defconst phox-new-equation-regexp 63,2407 +(defconst phox-close-def-regexp 66,2534 +(defun phox-init-syntax-table 71,2671 +(defvar phox-top-keywords87,3143 +(defvar phox-proof-keywords135,3598 +(defun phox-find-and-forget 176,3948 +(defalias 'phox-assert-next-command-interactive phox-assert-next-command-interactive255,6364 +(defun phox-depend-theorem(274,7330 +(defun phox-eshow-extlist(283,7619 +(defun phox-flag-name(297,8216 +(defun phox-path(308,8518 +(defun phox-print-expression(319,8754 +(defun phox-print-sort-expression(332,9210 +(defun phox-priority-symbols-list(343,9522 +(defun phox-search-string(355,9894 +(defun phox-constraints(370,10419 +(defun phox-goals(381,10675 +(defvar phox-state-menu393,10884 +(defun phox-delete-symbol(418,11874 +(defun phox-delete-symbol-on-cursor(424,12082 phox/phox-lang.el,323 -(defvar phox-lang9,306 -(defun phox-lang-absurd 17,535 -(defun phox-lang-suppress 22,629 -(defun phox-lang-opendef 27,826 -(defun phox-lang-instance 32,944 -(defun phox-lang-open-instance 37,1073 -(defun phox-lang-lock 42,1222 -(defun phox-lang-unlock 47,1352 -(defun phox-lang-prove 52,1488 -(defun phox-lang-let 57,1622 +(defvar phox-lang9,271 +(defun phox-lang-absurd 17,500 +(defun phox-lang-suppress 22,594 +(defun phox-lang-opendef 27,791 +(defun phox-lang-instance 32,909 +(defun phox-lang-open-instance 37,1038 +(defun phox-lang-lock 42,1187 +(defun phox-lang-unlock 47,1317 +(defun phox-lang-prove 52,1453 +(defun phox-lang-let 57,1587 phox/phox-outline.el,254 -(defconst phox-outline-title-regexp 20,745 -(defconst phox-outline-section-regexp 21,810 -(defconst phox-outline-save-regexp 22,866 -(defconst phox-outline-heading-end-regexp 39,1409 -(defun phox-outline-level(45,1584 -(defun phox-setup-outline 59,2058 +(defconst phox-outline-title-regexp 19,723 +(defconst phox-outline-section-regexp 20,788 +(defconst phox-outline-save-regexp 21,844 +(defconst phox-outline-heading-end-regexp 38,1387 +(defun phox-outline-level(44,1562 +(defun phox-setup-outline 58,2036 phox/phox-pbrpm.el,513 -(defun phox-pbrpm-left-paren-p 39,1671 -(defun phox-pbrpm-right-paren-p 46,1874 -(defun phox-pbrpm-menu-from-string 54,2078 -(defun phox-pbrpm-rename-in-cmd 63,2410 -(defun phox-pbrpm-get-region-name 96,3658 -(defun phox-pbrpm-escape-string 99,3785 -(defun phox-pbrpm-generate-menu 103,3920 -(defalias 'proof-pbrpm-generate-menu proof-pbrpm-generate-menu310,11400 -(defalias 'proof-pbrpm-left-paren-p proof-pbrpm-left-paren-p311,11464 -(defalias 'proof-pbrpm-right-paren-p proof-pbrpm-right-paren-p312,11526 +(defun phox-pbrpm-left-paren-p 39,1636 +(defun phox-pbrpm-right-paren-p 46,1839 +(defun phox-pbrpm-menu-from-string 54,2043 +(defun phox-pbrpm-rename-in-cmd 63,2375 +(defun phox-pbrpm-get-region-name 96,3623 +(defun phox-pbrpm-escape-string 99,3750 +(defun phox-pbrpm-generate-menu 103,3885 +(defalias 'proof-pbrpm-generate-menu proof-pbrpm-generate-menu310,11365 +(defalias 'proof-pbrpm-left-paren-p proof-pbrpm-left-paren-p311,11429 +(defalias 'proof-pbrpm-right-paren-p proof-pbrpm-right-paren-p312,11491 phox/phox-sym-lock.el,1398 (defcustom phox-sym-lock-enabled 19,871 @@ -858,81 +880,81 @@ phox/phox-sym-lock.el,1398 (defun phox-sym-lock-patch-keywords 384,14798 phox/phox-tags.el,305 -(defun phox-tags-add-table(26,869 -(defun phox-tags-reset-table(35,1264 -(defun phox-tags-add-doc-table(40,1374 -(defun phox-tags-add-lib-table(46,1523 -(defun phox-tags-add-local-table(52,1658 -(defun phox-tags-create-local-table(58,1841 -(defun phox-complete-tag(69,2091 -(defvar phox-tags-menu76,2200 +(defun phox-tags-add-table(26,834 +(defun phox-tags-reset-table(35,1229 +(defun phox-tags-add-doc-table(40,1339 +(defun phox-tags-add-lib-table(46,1488 +(defun phox-tags-add-local-table(52,1623 +(defun phox-tags-create-local-table(58,1806 +(defun phox-complete-tag(69,2056 +(defvar phox-tags-menu76,2165 generic/pg-assoc.el,81 -(defun proof-associated-buffers 33,973 -(defun proof-associated-windows 43,1183 +(defun proof-associated-buffers 33,925 +(defun proof-associated-windows 43,1135 generic/pg-autotest.el,908 -(defvar pg-autotest-success 29,690 -(defvar pg-autotest-log 32,777 -(defun pg-autotest-find-file 37,871 -(defun pg-autotest-find-file-restart 44,1137 -(defmacro pg-autotest-apply 58,1611 -(defmacro pg-autotest 72,2026 -(defun pg-autotest-log 89,2463 -(defun pg-autotest-message 98,2726 -(defun pg-autotest-remark 107,3015 -(defun pg-autotest-timestart 110,3096 -(defun pg-autotest-timetaken 115,3279 -(defun pg-autotest-start 129,3667 -(defun pg-autotest-exit 140,4121 -(defun pg-autotest-test-process-wholefile 160,4904 -(defun pg-autotest-test-script-wholefile 168,5191 -(defun pg-autotest-test-script-randomjumps 193,6123 -(defun pg-autotest-test-retract-file 242,7680 -(defun pg-autotest-test-assert-processed 248,7821 -(defun pg-autotest-test-assert-full 254,8047 -(defun pg-autotest-test-assert-unprocessed 261,8288 -(defun pg-autotest-test-eval 268,8553 -(defun pg-autotest-test-quit-prover 272,8652 +(defvar pg-autotest-success 29,639 +(defvar pg-autotest-log 32,726 +(defun pg-autotest-find-file 37,820 +(defun pg-autotest-find-file-restart 44,1086 +(defmacro pg-autotest-apply 58,1560 +(defmacro pg-autotest 72,1975 +(defun pg-autotest-log 89,2412 +(defun pg-autotest-message 98,2675 +(defun pg-autotest-remark 107,2964 +(defun pg-autotest-timestart 110,3045 +(defun pg-autotest-timetaken 115,3228 +(defun pg-autotest-start 129,3616 +(defun pg-autotest-exit 140,4070 +(defun pg-autotest-test-process-wholefile 160,4853 +(defun pg-autotest-test-script-wholefile 168,5140 +(defun pg-autotest-test-script-randomjumps 193,6072 +(defun pg-autotest-test-retract-file 242,7629 +(defun pg-autotest-test-assert-processed 248,7770 +(defun pg-autotest-test-assert-full 254,7996 +(defun pg-autotest-test-assert-unprocessed 261,8237 +(defun pg-autotest-test-eval 268,8502 +(defun pg-autotest-test-quit-prover 272,8601 generic/pg-custom.el,635 -(defpgcustom script-indent 37,1199 -(defconst proof-toolbar-entries-default42,1336 -(defpgcustom toolbar-entries 70,3069 -(defpgcustom prog-args 89,3802 -(defpgcustom prog-env 101,4380 -(defpgcustom quit-timeout 110,4809 -(defpgcustom favourites 122,5236 -(defpgcustom menu-entries 127,5425 -(defpgcustom help-menu-entries 134,5661 -(defpgcustom keymap 141,5924 -(defpgcustom completion-table 146,6095 -(defpgcustom tags-program 157,6471 -(defpgcustom use-holes 166,6855 -(defpgcustom one-command-per-line173,7113 -(defpgcustom maths-menu-enable 184,7349 -(defpgcustom unicode-tokens-enable 190,7529 -(defpgcustom mmm-enable 196,7736 +(defpgcustom script-indent 37,1150 +(defconst proof-toolbar-entries-default42,1287 +(defpgcustom toolbar-entries 71,3122 +(defpgcustom prog-args 90,3855 +(defpgcustom prog-env 102,4433 +(defpgcustom quit-timeout 111,4862 +(defpgcustom favourites 123,5289 +(defpgcustom menu-entries 128,5478 +(defpgcustom help-menu-entries 135,5714 +(defpgcustom keymap 142,5977 +(defpgcustom completion-table 147,6148 +(defpgcustom tags-program 158,6524 +(defpgcustom use-holes 167,6908 +(defpgcustom one-command-per-line174,7166 +(defpgcustom maths-menu-enable 185,7402 +(defpgcustom unicode-tokens-enable 191,7582 +(defpgcustom mmm-enable 197,7789 generic/pg-goals.el,285 -(define-derived-mode proof-goals-mode 29,734 -(define-key proof-goals-mode-map 56,1592 -(define-key proof-goals-mode-map 58,1708 -(define-key proof-goals-mode-map 59,1776 -(defun proof-goals-config-done 68,1923 -(defun pg-goals-display 76,2189 -(defun pg-goals-button-action 117,3493 - -generic/pg-movie.el,334 -(defconst pg-movie-xml-header 33,944 -(defconst pg-movie-stylesheet35,1002 -(defun pg-movie-stylesheet-location 38,1101 -(defvar pg-movie-frame 42,1209 -(defun pg-movie-of-span 44,1263 -(defun pg-movie-of-region 80,2383 -(defun pg-movie-export 87,2571 -(defun pg-movie-export-from 109,3175 -(defun pg-movie-export-directory 120,3496 +(define-derived-mode proof-goals-mode 29,686 +(define-key proof-goals-mode-map 56,1544 +(define-key proof-goals-mode-map 58,1660 +(define-key proof-goals-mode-map 59,1728 +(defun proof-goals-config-done 68,1875 +(defun pg-goals-display 76,2141 +(defun pg-goals-button-action 117,3445 + +generic/pg-movie.el,333 +(defconst pg-movie-xml-header 32,875 +(defconst pg-movie-stylesheet34,933 +(defun pg-movie-stylesheet-location 37,1032 +(defvar pg-movie-frame 41,1140 +(defun pg-movie-of-span 43,1194 +(defun pg-movie-of-region 79,2314 +(defun pg-movie-export 86,2502 +(defun pg-movie-export-from 108,3106 +(defun pg-movie-export-directory 119,3427 generic/pg-pamacs.el,534 (defmacro deflocal 35,1138 @@ -952,1783 +974,1871 @@ generic/pg-pamacs.el,534 (defmacro proof-eval-when-ready-for-assistant 270,9510 generic/pg-pbrpm.el,1808 -(defvar pg-pbrpm-use-buffer-menu 45,1207 -(defvar pg-pbrpm-start-goal-regexp 48,1329 -(defvar pg-pbrpm-start-goal-regexp-par-num 52,1486 -(defvar pg-pbrpm-end-goal-regexp 55,1609 -(defvar pg-pbrpm-start-hyp-regexp 59,1761 -(defvar pg-pbrpm-start-hyp-regexp-par-num 63,1922 -(defvar pg-pbrpm-start-concl-regexp 67,2129 -(defvar pg-pbrpm-auto-select-regexp 71,2293 -(defvar pg-pbrpm-buffer-menu 78,2454 -(defvar pg-pbrpm-spans 79,2488 -(defvar pg-pbrpm-goal-description 80,2516 -(defvar pg-pbrpm-windows-dialog-bug 81,2555 -(defvar pbrpm-menu-desc 82,2596 -(defun pg-pbrpm-erase-buffer-menu 84,2626 -(defun pg-pbrpm-menu-change-hook 90,2798 -(defun pg-pbrpm-create-reset-buffer-menu 108,3373 -(defun pg-pbrpm-analyse-goal-buffer 127,4215 -(defun pg-pbrpm-button-action 187,6620 -(defun pg-pbrpm-exists 194,6846 -(defun pg-pbrpm-eliminate-id 198,6958 -(defun pg-pbrpm-build-menu 206,7204 -(defun pg-pbrpm-setup-span 269,9524 -(defun pg-pbrpm-run-command 329,11823 -(defun pg-pbrpm-get-pos-info 362,13348 -(defun pg-pbrpm-get-region-info 404,14647 -(defun pg-pbrpm-auto-select-around-point 415,15059 -(defun pg-pbrpm-translate-position 430,15583 -(defun pg-pbrpm-process-click 438,15837 -(defvar pg-pbrpm-remember-region-selected-region 458,16862 -(defvar pg-pbrpm-regions-list 459,16916 -(defun pg-pbrpm-erase-regions-list 461,16952 -(defun pg-pbrpm-filter-regions-list 470,17260 -(defface pg-pbrpm-multiple-selection-face477,17523 -(defface pg-pbrpm-menu-input-face485,17725 -(defun pg-pbrpm-do-remember-region 493,17915 -(defun pg-pbrpm-remember-region-drag-up-hook 514,18763 -(defun pg-pbrpm-remember-region-click-hook 518,18934 -(defun pg-pbrpm-remember-region 523,19119 -(defun pg-pbrpm-process-region 537,19833 -(defun pg-pbrpm-process-regions-list 555,20562 -(defun pg-pbrpm-region-expression 559,20745 +(defvar pg-pbrpm-use-buffer-menu 45,1159 +(defvar pg-pbrpm-start-goal-regexp 48,1281 +(defvar pg-pbrpm-start-goal-regexp-par-num 52,1438 +(defvar pg-pbrpm-end-goal-regexp 55,1561 +(defvar pg-pbrpm-start-hyp-regexp 59,1713 +(defvar pg-pbrpm-start-hyp-regexp-par-num 63,1874 +(defvar pg-pbrpm-start-concl-regexp 67,2081 +(defvar pg-pbrpm-auto-select-regexp 71,2245 +(defvar pg-pbrpm-buffer-menu 78,2406 +(defvar pg-pbrpm-spans 79,2440 +(defvar pg-pbrpm-goal-description 80,2468 +(defvar pg-pbrpm-windows-dialog-bug 81,2507 +(defvar pbrpm-menu-desc 82,2548 +(defun pg-pbrpm-erase-buffer-menu 84,2578 +(defun pg-pbrpm-menu-change-hook 90,2750 +(defun pg-pbrpm-create-reset-buffer-menu 108,3325 +(defun pg-pbrpm-analyse-goal-buffer 127,4167 +(defun pg-pbrpm-button-action 187,6572 +(defun pg-pbrpm-exists 194,6798 +(defun pg-pbrpm-eliminate-id 198,6910 +(defun pg-pbrpm-build-menu 206,7156 +(defun pg-pbrpm-setup-span 269,9476 +(defun pg-pbrpm-run-command 329,11775 +(defun pg-pbrpm-get-pos-info 362,13300 +(defun pg-pbrpm-get-region-info 404,14599 +(defun pg-pbrpm-auto-select-around-point 415,15011 +(defun pg-pbrpm-translate-position 430,15535 +(defun pg-pbrpm-process-click 438,15789 +(defvar pg-pbrpm-remember-region-selected-region 458,16814 +(defvar pg-pbrpm-regions-list 459,16868 +(defun pg-pbrpm-erase-regions-list 461,16904 +(defun pg-pbrpm-filter-regions-list 470,17212 +(defface pg-pbrpm-multiple-selection-face477,17475 +(defface pg-pbrpm-menu-input-face485,17677 +(defun pg-pbrpm-do-remember-region 493,17867 +(defun pg-pbrpm-remember-region-drag-up-hook 514,18715 +(defun pg-pbrpm-remember-region-click-hook 518,18886 +(defun pg-pbrpm-remember-region 523,19071 +(defun pg-pbrpm-process-region 537,19785 +(defun pg-pbrpm-process-regions-list 555,20514 +(defun pg-pbrpm-region-expression 559,20697 generic/pg-pgip.el,2931 -(defalias 'pg-pgip-debug pg-pgip-debug38,1032 -(defalias 'pg-pgip-error pg-pgip-error39,1073 -(defalias 'pg-pgip-warning pg-pgip-warning40,1108 -(defconst pg-pgip-version-supported 42,1158 -(defun pg-pgip-process-packet 46,1264 -(defvar pg-pgip-last-seen-id 56,1832 -(defvar pg-pgip-last-seen-seq 57,1866 -(defun pg-pgip-process-pgip 59,1902 -(defun pg-pgip-process-msg 78,2842 -(defvar pg-pgip-post-process-functions93,3433 -(defun pg-pgip-post-process 103,3908 -(defun pg-pgip-process-askpgip 120,4523 -(defun pg-pgip-process-usespgip 126,4727 -(defun pg-pgip-process-usespgml 130,4891 -(defun pg-pgip-process-pgmlconfig 134,5055 -(defun pg-pgip-process-proverinfo 150,5672 -(defun pg-pgip-process-hasprefs 167,6337 -(defun pg-pgip-haspref 181,6969 -(defun pg-pgip-process-prefval 199,7685 -(defun pg-pgip-process-guiconfig 226,8393 -(defvar proof-assistant-idtables 233,8510 -(defun pg-pgip-process-ids 236,8627 -(defun pg-complete-idtable-symbol 262,9699 -(defalias 'pg-pgip-process-setids pg-pgip-process-setids267,9791 -(defalias 'pg-pgip-process-addids pg-pgip-process-addids268,9847 -(defalias 'pg-pgip-process-delids pg-pgip-process-delids269,9903 -(defun pg-pgip-process-idvalue 272,9961 -(defun pg-pgip-process-menuadd 284,10307 -(defun pg-pgip-process-menudel 287,10350 -(defun pg-pgip-process-ready 296,10582 -(defun pg-pgip-process-cleardisplay 299,10623 -(defun pg-pgip-process-proofstate 313,11080 -(defun pg-pgip-process-normalresponse 317,11157 -(defun pg-pgip-process-errorresponse 321,11287 -(defun pg-pgip-process-scriptinsert 325,11416 -(defun pg-pgip-process-metainforesponse 330,11550 -(defun pg-pgip-file-of-url 339,11790 -(defun pg-pgip-process-informfileloaded 344,11925 -(defun pg-pgip-process-informfileretracted 350,12157 -(defun pg-pgip-process-brokerstatus 363,12604 -(defun pg-pgip-process-proveravailmsg 366,12652 -(defun pg-pgip-process-newprovermsg 369,12702 -(defun pg-pgip-process-proverstatusmsg 372,12750 -(defvar pg-pgip-srcids 381,12996 -(defun pg-pgip-process-newfile 385,13103 -(defun pg-pgip-process-filestatus 401,13685 -(defun pg-pgip-process-newobj 421,14339 -(defun pg-pgip-process-delobj 424,14381 -(defun pg-pgip-process-objectstatus 427,14423 -(defun pg-pgip-process-parsescript 441,14775 -(defun pg-pgip-get-pgiptype 464,15649 -(defun pg-pgip-default-for 485,16512 -(defun pg-pgip-subst-for 498,16907 -(defun pg-pgip-interpret-value 511,17277 -(defun pg-pgip-interpret-choice 530,18002 -(defun pg-pgip-string-of-command 561,19019 -(defconst pg-pgip-id578,19780 -(defvar pg-pgip-refseq 584,20060 -(defvar pg-pgip-refid 586,20157 -(defvar pg-pgip-seq 589,20249 -(defun pg-pgip-assemble-packet 591,20313 -(defun pg-pgip-issue 609,21124 -(defun pg-pgip-maybe-askpgip 626,21736 -(defun pg-pgip-askprefs 632,21927 -(defun pg-pgip-askids 636,22041 -(defun pg-pgip-reset 649,22329 -(defconst pg-pgip-start-element-regexp 680,23027 -(defconst pg-pgip-end-element-regexp 681,23079 - -generic/pg-response.el,1252 -(deflocal pg-response-eagerly-raise 32,788 -(define-derived-mode proof-response-mode 42,1013 -(define-key proof-response-mode-map 69,1950 -(define-key proof-response-mode-map 70,2021 -(define-key proof-response-mode-map 71,2075 -(defun proof-response-config-done 75,2161 -(defvar pg-response-special-display-regexp 86,2507 -(defconst proof-multiframe-parameters90,2674 -(defun proof-multiple-frames-enable 99,2964 -(defun proof-three-window-enable 109,3292 -(defun proof-select-three-b 112,3355 -(defun proof-display-three-b 127,3846 -(defvar pg-frame-configuration 138,4236 -(defun pg-cache-frame-configuration 142,4383 -(defun proof-layout-windows 146,4554 -(defun proof-delete-other-frames 186,6341 -(defvar pg-response-erase-flag 217,7429 -(defun pg-response-maybe-erase221,7558 -(defun pg-response-display 251,8662 -(defun pg-response-display-with-face 276,9445 -(defun pg-response-clear-displays 304,10291 -(defun pg-response-message 322,10997 -(defun pg-response-warning 328,11232 -(defun proof-next-error 343,11638 -(defun pg-response-has-error-location 421,14447 -(defcustom proof-trace-buffer-max-lines 436,14866 -(defun proof-trace-buffer-display 443,15101 -(defun proof-trace-buffer-finish 457,15508 -(defun pg-thms-buffer-clear 481,16161 +(defalias 'pg-pgip-debug pg-pgip-debug39,1044 +(defalias 'pg-pgip-error pg-pgip-error40,1085 +(defalias 'pg-pgip-warning pg-pgip-warning41,1120 +(defconst pg-pgip-version-supported 43,1170 +(defun pg-pgip-process-packet 47,1276 +(defvar pg-pgip-last-seen-id 57,1844 +(defvar pg-pgip-last-seen-seq 58,1878 +(defun pg-pgip-process-pgip 60,1914 +(defun pg-pgip-process-msg 79,2854 +(defvar pg-pgip-post-process-functions94,3445 +(defun pg-pgip-post-process 104,3920 +(defun pg-pgip-process-askpgip 121,4535 +(defun pg-pgip-process-usespgip 127,4739 +(defun pg-pgip-process-usespgml 131,4903 +(defun pg-pgip-process-pgmlconfig 135,5067 +(defun pg-pgip-process-proverinfo 151,5684 +(defun pg-pgip-process-hasprefs 168,6349 +(defun pg-pgip-haspref 182,6981 +(defun pg-pgip-process-prefval 200,7697 +(defun pg-pgip-process-guiconfig 227,8405 +(defvar proof-assistant-idtables 234,8522 +(defun pg-pgip-process-ids 237,8639 +(defun pg-complete-idtable-symbol 263,9711 +(defalias 'pg-pgip-process-setids pg-pgip-process-setids268,9803 +(defalias 'pg-pgip-process-addids pg-pgip-process-addids269,9859 +(defalias 'pg-pgip-process-delids pg-pgip-process-delids270,9915 +(defun pg-pgip-process-idvalue 273,9973 +(defun pg-pgip-process-menuadd 285,10319 +(defun pg-pgip-process-menudel 288,10362 +(defun pg-pgip-process-ready 297,10594 +(defun pg-pgip-process-cleardisplay 300,10635 +(defun pg-pgip-process-proofstate 314,11092 +(defun pg-pgip-process-normalresponse 318,11169 +(defun pg-pgip-process-errorresponse 322,11299 +(defun pg-pgip-process-scriptinsert 326,11428 +(defun pg-pgip-process-metainforesponse 331,11562 +(defun pg-pgip-file-of-url 340,11802 +(defun pg-pgip-process-informfileloaded 345,11937 +(defun pg-pgip-process-informfileretracted 351,12169 +(defun pg-pgip-process-brokerstatus 364,12616 +(defun pg-pgip-process-proveravailmsg 367,12664 +(defun pg-pgip-process-newprovermsg 370,12714 +(defun pg-pgip-process-proverstatusmsg 373,12762 +(defvar pg-pgip-srcids 382,13008 +(defun pg-pgip-process-newfile 386,13115 +(defun pg-pgip-process-filestatus 402,13697 +(defun pg-pgip-process-newobj 422,14351 +(defun pg-pgip-process-delobj 425,14393 +(defun pg-pgip-process-objectstatus 428,14435 +(defun pg-pgip-process-parsescript 442,14787 +(defun pg-pgip-get-pgiptype 465,15661 +(defun pg-pgip-default-for 486,16524 +(defun pg-pgip-subst-for 499,16919 +(defun pg-pgip-interpret-value 512,17289 +(defun pg-pgip-interpret-choice 531,18014 +(defun pg-pgip-string-of-command 562,19031 +(defconst pg-pgip-id579,19792 +(defvar pg-pgip-refseq 585,20072 +(defvar pg-pgip-refid 587,20169 +(defvar pg-pgip-seq 590,20261 +(defun pg-pgip-assemble-packet 592,20325 +(defun pg-pgip-issue 610,21136 +(defun pg-pgip-maybe-askpgip 627,21748 +(defun pg-pgip-askprefs 633,21939 +(defun pg-pgip-askids 637,22053 +(defun pg-pgip-reset 650,22341 +(defconst pg-pgip-start-element-regexp 681,23039 +(defconst pg-pgip-end-element-regexp 682,23091 + +generic/pg-response.el,1251 +(deflocal pg-response-eagerly-raise 32,737 +(define-derived-mode proof-response-mode 42,962 +(define-key proof-response-mode-map 69,1899 +(define-key proof-response-mode-map 70,1970 +(define-key proof-response-mode-map 71,2024 +(defun proof-response-config-done 75,2110 +(defvar pg-response-special-display-regexp 86,2456 +(defconst proof-multiframe-parameters90,2623 +(defun proof-multiple-frames-enable 99,2913 +(defun proof-three-window-enable 109,3241 +(defun proof-select-three-b 112,3304 +(defun proof-display-three-b 127,3795 +(defvar pg-frame-configuration 138,4185 +(defun pg-cache-frame-configuration 142,4332 +(defun proof-layout-windows 146,4503 +(defun proof-delete-other-frames 186,6290 +(defvar pg-response-erase-flag 217,7378 +(defun pg-response-maybe-erase221,7507 +(defun pg-response-display 251,8611 +(defun pg-response-display-with-face 276,9394 +(defun pg-response-clear-displays 304,10240 +(defun pg-response-message 322,10946 +(defun pg-response-warning 328,11181 +(defun proof-next-error 343,11587 +(defun pg-response-has-error-location 421,14396 +(defcustom proof-trace-buffer-max-lines 436,14815 +(defun proof-trace-buffer-display 443,15050 +(defun proof-trace-buffer-finish 457,15457 +(defun pg-thms-buffer-clear 481,16110 generic/pg-user.el,3635 -(defun proof-script-new-command-advance 43,1232 -(defun proof-maybe-follow-locked-end 67,2157 -(defun proof-goto-command-start 93,2993 -(defun proof-goto-command-end 116,3940 -(defun proof-forward-command 131,4362 -(defun proof-backward-command 152,5083 -(defun proof-goto-point 163,5297 -(defun proof-assert-next-command-interactive 177,5731 -(defun proof-assert-until-point-interactive 189,6217 -(defun proof-process-buffer 195,6447 -(defun proof-undo-last-successful-command 213,6959 -(defun proof-undo-and-delete-last-successful-command 218,7121 -(defun proof-undo-last-successful-command-1 230,7640 -(defun proof-retract-buffer 247,8304 -(defun proof-retract-current-goal 256,8588 -(defun proof-mouse-goto-point 275,9108 -(defvar proof-minibuffer-history 290,9384 -(defun proof-minibuffer-cmd 293,9479 -(defun proof-frob-locked-end 332,10886 -(defmacro proof-if-setting-configured 368,11987 -(defmacro proof-define-assistant-command 376,12256 -(defmacro proof-define-assistant-command-witharg 389,12711 -(defun proof-issue-new-command 409,13533 -(defun proof-cd-sync 449,14756 -(defun proof-electric-terminator-enable 500,16355 -(defun proof-electric-terminator 508,16659 -(defun proof-add-completions 536,17629 -(defun proof-script-complete 559,18452 -(defun pg-copy-span-contents 573,18761 -(defun pg-numth-span-higher-or-lower 587,19185 -(defun pg-control-span-of 613,19931 -(defun pg-move-span-contents 619,20135 -(defun pg-fixup-children-spans 670,22253 -(defun pg-move-region-down 680,22510 -(defun pg-move-region-up 689,22803 -(defun pg-pos-for-event 703,23077 -(defun pg-span-for-event 709,23298 -(defun pg-span-context-menu 713,23442 -(defun pg-toggle-visibility 729,23959 -(defun pg-create-in-span-context-menu 738,24266 -(defun pg-span-undo 763,25294 -(defun pg-goals-buffers-hint 776,25532 -(defun pg-slow-fontify-tracing-hint 780,25750 -(defun pg-response-buffers-hint 784,25939 -(defun pg-jump-to-end-hint 796,26354 -(defun pg-processing-complete-hint 800,26483 -(defun pg-next-error-hint 817,27203 -(defun pg-hint 822,27355 -(defun pg-identifier-under-mouse-query 833,27704 -(defun pg-identifier-near-point-query 844,28028 -(defvar proof-query-identifier-history 873,28951 -(defun proof-query-identifier 876,29038 -(defun pg-identifier-query 887,29394 -(defun proof-imenu-enable 920,30542 -(defvar pg-input-ring 956,31845 -(defvar pg-input-ring-index 959,31902 -(defvar pg-stored-incomplete-input 962,31974 -(defun pg-previous-input 965,32077 -(defun pg-next-input 979,32540 -(defun pg-delete-input 984,32662 -(defun pg-get-old-input 997,33000 -(defun pg-restore-input 1011,33391 -(defun pg-search-start 1022,33681 -(defun pg-regexp-arg 1034,34173 -(defun pg-search-arg 1046,34621 -(defun pg-previous-matching-input-string-position 1060,35038 -(defun pg-previous-matching-input 1087,36203 -(defun pg-next-matching-input 1106,37053 -(defvar pg-matching-input-from-input-string 1114,37436 -(defun pg-previous-matching-input-from-input 1118,37550 -(defun pg-next-matching-input-from-input 1136,38315 -(defun pg-add-to-input-history 1147,38694 -(defun pg-remove-from-input-history 1159,39147 -(defun pg-clear-input-ring 1170,39527 -(define-key proof-mode-map 1187,39997 -(define-key proof-mode-map 1188,40057 -(defun pg-protected-undo 1190,40129 -(defun pg-protected-undo-1 1220,41423 -(defun next-undo-elt 1251,42860 -(defvar proof-autosend-timer 1278,43816 -(deflocal proof-autosend-modified-tick 1280,43877 -(defun proof-autosend-enable 1284,43999 -(defun proof-autosend-delay 1298,44542 -(defun proof-autosend-loop 1302,44675 -(defun proof-autosend-loop-all 1316,45235 -(defun proof-autosend-loop-next 1340,46015 +(defun proof-script-new-command-advance 43,1185 +(defun proof-maybe-follow-locked-end 67,2110 +(defun proof-goto-command-start 93,2946 +(defun proof-goto-command-end 116,3893 +(defun proof-forward-command 131,4315 +(defun proof-backward-command 152,5036 +(defun proof-goto-point 163,5250 +(defun proof-assert-next-command-interactive 177,5684 +(defun proof-assert-until-point-interactive 189,6170 +(defun proof-process-buffer 196,6415 +(defun proof-undo-last-successful-command 214,6927 +(defun proof-undo-and-delete-last-successful-command 219,7089 +(defun proof-undo-last-successful-command-1 231,7608 +(defun proof-retract-buffer 248,8272 +(defun proof-retract-current-goal 257,8556 +(defun proof-mouse-goto-point 276,9076 +(defvar proof-minibuffer-history 291,9352 +(defun proof-minibuffer-cmd 294,9447 +(defun proof-frob-locked-end 333,10854 +(defmacro proof-if-setting-configured 369,11955 +(defmacro proof-define-assistant-command 377,12224 +(defmacro proof-define-assistant-command-witharg 390,12679 +(defun proof-issue-new-command 410,13501 +(defun proof-cd-sync 450,14724 +(defun proof-electric-terminator-enable 501,16323 +(defun proof-electric-terminator 509,16627 +(defun proof-add-completions 537,17597 +(defun proof-script-complete 560,18420 +(defun pg-copy-span-contents 574,18729 +(defun pg-numth-span-higher-or-lower 588,19153 +(defun pg-control-span-of 614,19899 +(defun pg-move-span-contents 620,20103 +(defun pg-fixup-children-spans 671,22221 +(defun pg-move-region-down 681,22478 +(defun pg-move-region-up 690,22771 +(defun pg-pos-for-event 704,23045 +(defun pg-span-for-event 710,23266 +(defun pg-span-context-menu 714,23410 +(defun pg-toggle-visibility 730,23927 +(defun pg-create-in-span-context-menu 739,24234 +(defun pg-span-undo 764,25262 +(defun pg-goals-buffers-hint 777,25500 +(defun pg-slow-fontify-tracing-hint 781,25718 +(defun pg-response-buffers-hint 785,25907 +(defun pg-jump-to-end-hint 797,26322 +(defun pg-processing-complete-hint 801,26451 +(defun pg-next-error-hint 818,27171 +(defun pg-hint 823,27323 +(defun pg-identifier-under-mouse-query 834,27672 +(defun pg-identifier-near-point-query 845,27996 +(defvar proof-query-identifier-history 874,28919 +(defun proof-query-identifier 877,29006 +(defun pg-identifier-query 888,29362 +(defun proof-imenu-enable 921,30510 +(defvar pg-input-ring 957,31813 +(defvar pg-input-ring-index 960,31870 +(defvar pg-stored-incomplete-input 963,31942 +(defun pg-previous-input 966,32045 +(defun pg-next-input 980,32508 +(defun pg-delete-input 985,32630 +(defun pg-get-old-input 998,32968 +(defun pg-restore-input 1012,33359 +(defun pg-search-start 1023,33649 +(defun pg-regexp-arg 1035,34141 +(defun pg-search-arg 1047,34589 +(defun pg-previous-matching-input-string-position 1061,35006 +(defun pg-previous-matching-input 1088,36171 +(defun pg-next-matching-input 1107,37021 +(defvar pg-matching-input-from-input-string 1115,37404 +(defun pg-previous-matching-input-from-input 1119,37518 +(defun pg-next-matching-input-from-input 1137,38283 +(defun pg-add-to-input-history 1148,38662 +(defun pg-remove-from-input-history 1160,39115 +(defun pg-clear-input-ring 1171,39495 +(define-key proof-mode-map 1188,39965 +(define-key proof-mode-map 1189,40025 +(defun pg-protected-undo 1191,40097 +(defun pg-protected-undo-1 1221,41391 +(defun next-undo-elt 1252,42828 +(defvar proof-autosend-timer 1279,43784 +(deflocal proof-autosend-modified-tick 1281,43845 +(defun proof-autosend-enable 1285,43967 +(defun proof-autosend-delay 1299,44510 +(defun proof-autosend-loop 1303,44643 +(defun proof-autosend-loop-all 1317,45203 +(defun proof-autosend-loop-next 1341,45983 generic/pg-vars.el,1500 -(defvar proof-assistant-cusgrp 22,388 -(defvar proof-assistant-internals-cusgrp 28,648 -(defvar proof-assistant 34,918 -(defvar proof-assistant-symbol 39,1141 -(defvar proof-mode-for-shell 52,1683 -(defvar proof-mode-for-response 57,1873 -(defvar proof-mode-for-goals 62,2099 -(defvar proof-mode-for-script 67,2288 -(defvar proof-ready-for-assistant-hook 72,2465 -(defvar proof-shell-busy 83,2753 -(defvar proof-shell-last-queuemode 101,3424 -(defvar proof-included-files-list 105,3579 -(defvar proof-script-buffer 127,4598 -(defvar proof-previous-script-buffer 130,4690 -(defvar proof-shell-buffer 134,4863 -(defvar proof-goals-buffer 137,4949 -(defvar proof-response-buffer 140,5004 -(defvar proof-trace-buffer 143,5065 -(defvar proof-thms-buffer 147,5219 -(defvar proof-shell-error-or-interrupt-seen 151,5374 -(defvar pg-response-next-error 156,5598 -(defvar proof-shell-proof-completed 159,5705 -(defvar proof-shell-silent 173,6090 -(defvar proof-shell-last-prompt 176,6178 -(defvar proof-shell-last-output 180,6348 -(defvar proof-shell-last-output-kind 184,6488 -(defvar proof-assistant-settings 204,7252 -(defvar pg-tracing-slow-mode 214,7766 -(defvar proof-nesting-depth 217,7855 -(defvar proof-last-theorem-dependencies 224,8090 -(defvar proof-autosend-running 228,8252 -(defvar proof-next-command-on-new-line 233,8451 -(defcustom proof-general-name 244,8685 -(defcustom proof-general-home-page249,8842 -(defcustom proof-unnamed-theorem-name255,9002 -(defcustom proof-universal-keys261,9186 - -generic/pg-xml.el,1177 -(defalias 'pg-xml-error pg-xml-error18,381 -(defun pg-xml-parse-string 41,1023 -(defun pg-xml-parse-buffer 51,1335 -(defun pg-xml-get-attr 70,1950 -(defun pg-xml-child-elts 78,2252 -(defun pg-xml-child-elt 83,2457 -(defun pg-xml-get-child 91,2739 -(defun pg-xml-get-text-content 101,3106 -(defmacro pg-xml-attr 112,3456 -(defmacro pg-xml-node 114,3518 -(defconst pg-xml-header117,3610 -(defun pg-xml-string-of 121,3686 -(defun pg-xml-output-internal 132,4053 -(defun pg-xml-cdata 166,5192 -(defsubst pg-pgip-get-area 174,5385 -(defun pg-pgip-get-icon 177,5502 -(defsubst pg-pgip-get-name 181,5650 -(defsubst pg-pgip-get-version 184,5767 -(defsubst pg-pgip-get-descr 187,5890 -(defsubst pg-pgip-get-thmname 190,6009 -(defsubst pg-pgip-get-thyname 193,6132 -(defsubst pg-pgip-get-url 196,6255 -(defsubst pg-pgip-get-srcid 199,6370 -(defsubst pg-pgip-get-proverid 202,6489 -(defsubst pg-pgip-get-symname 205,6614 -(defsubst pg-pgip-get-prefcat 208,6734 -(defsubst pg-pgip-get-default 211,6862 -(defsubst pg-pgip-get-objtype 214,6985 -(defsubst pg-pgip-get-value 217,7108 -(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext220,7178 -(defun pg-pgip-get-pgmltext 222,7237 +(defvar proof-assistant-cusgrp 22,341 +(defvar proof-assistant-internals-cusgrp 28,601 +(defvar proof-assistant 34,871 +(defvar proof-assistant-symbol 39,1094 +(defvar proof-mode-for-shell 52,1636 +(defvar proof-mode-for-response 57,1826 +(defvar proof-mode-for-goals 62,2052 +(defvar proof-mode-for-script 67,2241 +(defvar proof-ready-for-assistant-hook 72,2418 +(defvar proof-shell-busy 83,2706 +(defvar proof-shell-last-queuemode 101,3377 +(defvar proof-included-files-list 105,3532 +(defvar proof-script-buffer 127,4551 +(defvar proof-previous-script-buffer 130,4643 +(defvar proof-shell-buffer 134,4816 +(defvar proof-goals-buffer 137,4902 +(defvar proof-response-buffer 140,4957 +(defvar proof-trace-buffer 143,5018 +(defvar proof-thms-buffer 147,5172 +(defvar proof-shell-error-or-interrupt-seen 151,5327 +(defvar pg-response-next-error 156,5551 +(defvar proof-shell-proof-completed 159,5658 +(defvar proof-shell-silent 173,6043 +(defvar proof-shell-last-prompt 176,6131 +(defvar proof-shell-last-output 180,6301 +(defvar proof-shell-last-output-kind 184,6441 +(defvar proof-assistant-settings 204,7205 +(defvar pg-tracing-slow-mode 214,7719 +(defvar proof-nesting-depth 217,7808 +(defvar proof-last-theorem-dependencies 224,8043 +(defvar proof-autosend-running 228,8205 +(defvar proof-next-command-on-new-line 233,8404 +(defcustom proof-general-name 244,8638 +(defcustom proof-general-home-page249,8795 +(defcustom proof-unnamed-theorem-name255,8955 +(defcustom proof-universal-keys261,9139 + +generic/pg-xml.el,1176 +(defalias 'pg-xml-error pg-xml-error18,335 +(defun pg-xml-parse-string 41,977 +(defun pg-xml-parse-buffer 51,1289 +(defun pg-xml-get-attr 70,1904 +(defun pg-xml-child-elts 78,2206 +(defun pg-xml-child-elt 83,2411 +(defun pg-xml-get-child 91,2693 +(defun pg-xml-get-text-content 101,3060 +(defmacro pg-xml-attr 112,3410 +(defmacro pg-xml-node 114,3472 +(defconst pg-xml-header117,3564 +(defun pg-xml-string-of 121,3640 +(defun pg-xml-output-internal 132,4007 +(defun pg-xml-cdata 166,5146 +(defsubst pg-pgip-get-area 174,5339 +(defun pg-pgip-get-icon 177,5456 +(defsubst pg-pgip-get-name 181,5604 +(defsubst pg-pgip-get-version 184,5721 +(defsubst pg-pgip-get-descr 187,5844 +(defsubst pg-pgip-get-thmname 190,5963 +(defsubst pg-pgip-get-thyname 193,6086 +(defsubst pg-pgip-get-url 196,6209 +(defsubst pg-pgip-get-srcid 199,6324 +(defsubst pg-pgip-get-proverid 202,6443 +(defsubst pg-pgip-get-symname 205,6568 +(defsubst pg-pgip-get-prefcat 208,6688 +(defsubst pg-pgip-get-default 211,6816 +(defsubst pg-pgip-get-objtype 214,6939 +(defsubst pg-pgip-get-value 217,7062 +(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext220,7132 +(defun pg-pgip-get-pgmltext 222,7191 generic/proof-autoloads.el,97 -(defsubst proof-shell-live-buffer 722,23445 -(defsubst proof-replace-regexp-in-string 875,28925 +(defsubst proof-shell-live-buffer 727,23601 +(defsubst proof-replace-regexp-in-string 883,29162 generic/proof-auxmodes.el,149 (defun proof-mmm-support-available 20,495 (defun proof-maths-menu-support-available 44,1114 (defun proof-unicode-tokens-support-available 58,1531 -generic/proof-config.el,7741 -(defgroup prover-config 80,2632 -(defcustom proof-guess-command-line 98,3482 -(defcustom proof-assistant-home-page 113,3977 -(defcustom proof-context-command 119,4147 -(defcustom proof-info-command 124,4281 -(defcustom proof-showproof-command 131,4552 -(defcustom proof-goal-command 136,4688 -(defcustom proof-save-command 144,4985 -(defcustom proof-find-theorems-command 152,5294 -(defcustom proof-query-identifier-command 159,5602 -(defcustom proof-assistant-true-value 173,6291 -(defcustom proof-assistant-false-value 179,6481 -(defcustom proof-assistant-format-int-fn 185,6675 -(defcustom proof-assistant-format-float-fn 192,6924 -(defcustom proof-assistant-format-string-fn 199,7179 -(defcustom proof-assistant-setting-format 206,7446 -(defgroup proof-script 228,8141 -(defcustom proof-terminal-string 233,8271 -(defcustom proof-electric-terminator-noterminator 243,8659 -(defcustom proof-script-sexp-commands 248,8831 -(defcustom proof-script-command-end-regexp 259,9290 -(defcustom proof-script-command-start-regexp 277,10111 -(defcustom proof-script-integral-proofs 288,10574 -(defcustom proof-script-fly-past-comments 303,11230 -(defcustom proof-script-parse-function 308,11401 -(defcustom proof-script-comment-start 326,12046 -(defcustom proof-script-comment-start-regexp 337,12483 -(defcustom proof-script-comment-end 345,12802 -(defcustom proof-script-comment-end-regexp 357,13224 -(defcustom proof-string-start-regexp 365,13537 -(defcustom proof-string-end-regexp 370,13702 -(defcustom proof-case-fold-search 375,13863 -(defcustom proof-save-command-regexp 384,14275 -(defcustom proof-save-with-hole-regexp 389,14385 -(defcustom proof-save-with-hole-result 400,14760 -(defcustom proof-goal-command-regexp 410,15200 -(defcustom proof-goal-with-hole-regexp 418,15487 -(defcustom proof-goal-with-hole-result 430,15930 -(defcustom proof-non-undoables-regexp 439,16304 -(defcustom proof-nested-undo-regexp 450,16759 -(defcustom proof-ignore-for-undo-count 466,17471 -(defcustom proof-script-imenu-generic-expression 474,17774 -(defcustom proof-goal-command-p 482,18113 -(defcustom proof-really-save-command-p 493,18604 -(defcustom proof-completed-proof-behaviour 502,18911 -(defcustom proof-count-undos-fn 530,20260 -(defcustom proof-find-and-forget-fn 542,20811 -(defcustom proof-forget-id-command 559,21520 -(defcustom pg-topterm-goalhyplit-fn 569,21878 -(defcustom proof-kill-goal-command 581,22413 -(defcustom proof-undo-n-times-cmd 595,22917 -(defcustom proof-nested-goals-history-p 609,23454 -(defcustom proof-arbitrary-undo-positions 618,23791 -(defcustom proof-state-preserving-p 632,24372 -(defcustom proof-activate-scripting-hook 642,24844 -(defcustom proof-deactivate-scripting-hook 661,25625 -(defcustom proof-no-fully-processed-buffer 670,25955 -(defcustom proof-script-evaluate-elisp-comment-regexp 681,26453 -(defcustom proof-indent 699,27039 -(defcustom proof-indent-hang 704,27146 -(defcustom proof-indent-enclose-offset 709,27272 -(defcustom proof-indent-open-offset 714,27414 -(defcustom proof-indent-close-offset 719,27551 -(defcustom proof-indent-any-regexp 724,27689 -(defcustom proof-indent-inner-regexp 729,27849 -(defcustom proof-indent-enclose-regexp 734,28003 -(defcustom proof-indent-open-regexp 739,28157 -(defcustom proof-indent-close-regexp 744,28309 -(defcustom proof-script-font-lock-keywords 750,28463 -(defcustom proof-script-syntax-table-entries 758,28815 -(defcustom proof-script-span-context-menu-extensions 776,29211 -(defgroup proof-shell 802,29971 -(defcustom proof-prog-name 812,30141 -(defcustom proof-shell-auto-terminate-commands 824,30608 -(defcustom proof-shell-pre-sync-init-cmd 833,31013 -(defcustom proof-shell-init-cmd 847,31571 -(defcustom proof-shell-init-hook 859,32117 -(defcustom proof-shell-restart-cmd 864,32256 -(defcustom proof-shell-quit-cmd 869,32411 -(defcustom proof-shell-cd-cmd 874,32578 -(defcustom proof-shell-start-silent-cmd 891,33249 -(defcustom proof-shell-stop-silent-cmd 900,33625 -(defcustom proof-shell-silent-threshold 909,33960 -(defcustom proof-shell-inform-file-processed-cmd 917,34294 -(defcustom proof-shell-inform-file-retracted-cmd 938,35222 -(defcustom proof-auto-multiple-files 966,36494 -(defcustom proof-cannot-reopen-processed-files 981,37215 -(defcustom proof-shell-annotated-prompt-regexp 1001,38006 -(defcustom proof-shell-error-regexp 1016,38571 -(defcustom proof-shell-truncate-before-error 1036,39373 -(defcustom pg-next-error-regexp 1050,39912 -(defcustom pg-next-error-filename-regexp 1065,40521 -(defcustom pg-next-error-extract-filename 1089,41554 -(defcustom proof-shell-interrupt-regexp 1096,41797 -(defcustom proof-shell-proof-completed-regexp 1110,42392 -(defcustom proof-shell-clear-response-regexp 1123,42900 -(defcustom proof-shell-clear-goals-regexp 1135,43352 -(defcustom proof-shell-start-goals-regexp 1147,43798 -(defcustom proof-shell-end-goals-regexp 1156,44222 -(defcustom proof-shell-eager-annotation-start 1170,44795 -(defcustom proof-shell-eager-annotation-start-length 1193,45814 -(defcustom proof-shell-eager-annotation-end 1204,46240 -(defcustom proof-shell-strip-output-markup 1220,46915 -(defcustom proof-shell-assumption-regexp 1229,47300 -(defcustom proof-shell-process-file 1239,47704 -(defcustom proof-shell-retract-files-regexp 1265,48780 -(defcustom proof-shell-compute-new-files-list 1278,49268 -(defcustom pg-special-char-regexp 1293,49835 -(defcustom proof-shell-set-elisp-variable-regexp 1298,49979 -(defcustom proof-shell-match-pgip-cmd 1336,51645 -(defcustom proof-shell-issue-pgip-cmd 1350,52127 -(defcustom proof-use-pgip-askprefs 1355,52292 -(defcustom proof-shell-query-dependencies-cmd 1363,52639 -(defcustom proof-shell-theorem-dependency-list-regexp 1370,52899 -(defcustom proof-shell-theorem-dependency-list-split 1386,53559 -(defcustom proof-shell-show-dependency-cmd 1395,53982 -(defcustom proof-shell-trace-output-regexp 1417,54888 -(defcustom proof-shell-thms-output-regexp 1435,55482 -(defcustom proof-tokens-activate-command 1448,55865 -(defcustom proof-tokens-deactivate-command 1455,56105 -(defcustom proof-tokens-extra-modes 1462,56350 -(defcustom proof-shell-unicode 1477,56855 -(defcustom proof-shell-filename-escapes 1486,57245 -(defcustom proof-shell-process-connection-type 1503,57925 -(defcustom proof-shell-strip-crs-from-input 1509,58116 -(defcustom proof-shell-strip-crs-from-output 1521,58599 -(defcustom proof-shell-extend-queue-hook 1529,58967 -(defcustom proof-shell-insert-hook 1539,59397 -(defcustom proof-script-preprocess 1582,61495 -(defcustom proof-shell-handle-delayed-output-hook1588,61646 -(defcustom proof-shell-handle-error-or-interrupt-hook1594,61861 -(defcustom proof-shell-pre-interrupt-hook1612,62607 -(defcustom proof-shell-handle-output-system-specific 1620,62878 -(defcustom proof-state-change-hook 1643,63851 -(defcustom proof-shell-syntax-table-entries 1653,64244 -(defgroup proof-goals 1671,64615 -(defcustom pg-subterm-first-special-char 1676,64736 -(defcustom pg-subterm-anns-use-stack 1684,65048 -(defcustom pg-goals-change-goal 1693,65347 -(defcustom pbp-goal-command 1698,65463 -(defcustom pbp-hyp-command 1703,65619 -(defcustom pg-subterm-help-cmd 1708,65781 -(defcustom pg-goals-error-regexp 1715,66017 -(defcustom proof-shell-result-start 1720,66177 -(defcustom proof-shell-result-end 1726,66411 -(defcustom pg-subterm-start-char 1732,66624 -(defcustom pg-subterm-sep-char 1743,67098 -(defcustom pg-subterm-end-char 1749,67277 -(defcustom pg-topterm-regexp 1755,67434 -(defcustom proof-goals-font-lock-keywords 1770,68034 -(defcustom proof-response-font-lock-keywords 1778,68393 -(defcustom proof-shell-font-lock-keywords 1786,68755 -(defcustom pg-before-fontify-output-hook 1797,69269 -(defcustom pg-after-fontify-output-hook 1805,69630 +generic/proof-config.el,7845 +(defgroup prover-config 80,2580 +(defcustom proof-guess-command-line 98,3430 +(defcustom proof-assistant-home-page 113,3925 +(defcustom proof-context-command 119,4095 +(defcustom proof-info-command 124,4229 +(defcustom proof-showproof-command 131,4500 +(defcustom proof-goal-command 136,4636 +(defcustom proof-save-command 144,4933 +(defcustom proof-find-theorems-command 152,5242 +(defcustom proof-query-identifier-command 159,5550 +(defcustom proof-assistant-true-value 173,6239 +(defcustom proof-assistant-false-value 179,6429 +(defcustom proof-assistant-format-int-fn 185,6623 +(defcustom proof-assistant-format-float-fn 192,6872 +(defcustom proof-assistant-format-string-fn 199,7127 +(defcustom proof-assistant-setting-format 206,7394 +(defcustom proof-tree-configured 216,7877 +(defgroup proof-script 234,8343 +(defcustom proof-terminal-string 239,8473 +(defcustom proof-electric-terminator-noterminator 249,8861 +(defcustom proof-script-sexp-commands 254,9033 +(defcustom proof-script-command-end-regexp 265,9492 +(defcustom proof-script-command-start-regexp 283,10313 +(defcustom proof-script-integral-proofs 294,10776 +(defcustom proof-script-fly-past-comments 309,11432 +(defcustom proof-script-parse-function 314,11603 +(defcustom proof-script-comment-start 332,12248 +(defcustom proof-script-comment-start-regexp 343,12685 +(defcustom proof-script-comment-end 351,13004 +(defcustom proof-script-comment-end-regexp 363,13426 +(defcustom proof-string-start-regexp 371,13739 +(defcustom proof-string-end-regexp 376,13904 +(defcustom proof-case-fold-search 381,14065 +(defcustom proof-save-command-regexp 390,14477 +(defcustom proof-save-with-hole-regexp 395,14587 +(defcustom proof-save-with-hole-result 406,14962 +(defcustom proof-goal-command-regexp 416,15406 +(defcustom proof-goal-with-hole-regexp 424,15693 +(defcustom proof-goal-with-hole-result 436,16136 +(defcustom proof-non-undoables-regexp 445,16514 +(defcustom proof-nested-undo-regexp 456,16977 +(defcustom proof-ignore-for-undo-count 472,17697 +(defcustom proof-script-imenu-generic-expression 480,18008 +(defcustom proof-goal-command-p 488,18347 +(defcustom proof-really-save-command-p 499,18838 +(defcustom proof-completed-proof-behaviour 508,19145 +(defcustom proof-count-undos-fn 536,20494 +(defcustom proof-find-and-forget-fn 548,21045 +(defcustom proof-forget-id-command 565,21754 +(defcustom pg-topterm-goalhyplit-fn 575,22112 +(defcustom proof-kill-goal-command 587,22655 +(defcustom proof-undo-n-times-cmd 601,23159 +(defcustom proof-nested-goals-history-p 615,23696 +(defcustom proof-arbitrary-undo-positions 624,24033 +(defcustom proof-state-preserving-p 638,24614 +(defcustom proof-activate-scripting-hook 648,25086 +(defcustom proof-deactivate-scripting-hook 667,25867 +(defcustom proof-no-fully-processed-buffer 676,26197 +(defcustom proof-script-evaluate-elisp-comment-regexp 687,26695 +(defcustom proof-indent 705,27281 +(defcustom proof-indent-hang 710,27388 +(defcustom proof-indent-enclose-offset 715,27514 +(defcustom proof-indent-open-offset 720,27656 +(defcustom proof-indent-close-offset 725,27793 +(defcustom proof-indent-any-regexp 730,27931 +(defcustom proof-indent-inner-regexp 735,28091 +(defcustom proof-indent-enclose-regexp 740,28245 +(defcustom proof-indent-open-regexp 745,28399 +(defcustom proof-indent-close-regexp 750,28551 +(defcustom proof-script-font-lock-keywords 756,28705 +(defcustom proof-script-syntax-table-entries 764,29057 +(defcustom proof-script-span-context-menu-extensions 782,29453 +(defgroup proof-shell 808,30213 +(defcustom proof-prog-name 818,30383 +(defcustom proof-shell-auto-terminate-commands 830,30850 +(defcustom proof-shell-pre-sync-init-cmd 839,31255 +(defcustom proof-shell-init-cmd 853,31813 +(defcustom proof-shell-init-hook 865,32359 +(defcustom proof-shell-restart-cmd 870,32498 +(defcustom proof-shell-quit-cmd 875,32653 +(defcustom proof-shell-cd-cmd 880,32820 +(defcustom proof-shell-start-silent-cmd 897,33491 +(defcustom proof-shell-stop-silent-cmd 906,33867 +(defcustom proof-shell-silent-threshold 915,34202 +(defcustom proof-shell-inform-file-processed-cmd 923,34536 +(defcustom proof-shell-inform-file-retracted-cmd 944,35464 +(defcustom proof-auto-multiple-files 972,36736 +(defcustom proof-cannot-reopen-processed-files 987,37457 +(defcustom proof-shell-annotated-prompt-regexp 1007,38248 +(defcustom proof-shell-error-regexp 1022,38813 +(defcustom proof-shell-truncate-before-error 1042,39623 +(defcustom pg-next-error-regexp 1056,40162 +(defcustom pg-next-error-filename-regexp 1071,40771 +(defcustom pg-next-error-extract-filename 1095,41804 +(defcustom proof-shell-interrupt-regexp 1102,42047 +(defcustom proof-shell-proof-completed-regexp 1116,42650 +(defcustom proof-shell-clear-response-regexp 1129,43166 +(defcustom proof-shell-clear-goals-regexp 1141,43626 +(defcustom proof-shell-start-goals-regexp 1153,44080 +(defcustom proof-shell-end-goals-regexp 1162,44512 +(defcustom proof-shell-eager-annotation-start 1176,45093 +(defcustom proof-shell-eager-annotation-start-length 1199,46112 +(defcustom proof-shell-eager-annotation-end 1210,46538 +(defcustom proof-shell-strip-output-markup 1226,47213 +(defcustom proof-shell-assumption-regexp 1235,47598 +(defcustom proof-shell-process-file 1245,48002 +(defcustom proof-shell-retract-files-regexp 1271,49078 +(defcustom proof-shell-compute-new-files-list 1284,49566 +(defcustom pg-special-char-regexp 1299,50133 +(defcustom proof-shell-set-elisp-variable-regexp 1304,50277 +(defcustom proof-shell-match-pgip-cmd 1342,51951 +(defcustom proof-shell-issue-pgip-cmd 1356,52441 +(defcustom proof-use-pgip-askprefs 1361,52614 +(defcustom proof-shell-query-dependencies-cmd 1369,52961 +(defcustom proof-shell-theorem-dependency-list-regexp 1376,53221 +(defcustom proof-shell-theorem-dependency-list-split 1392,53889 +(defcustom proof-shell-show-dependency-cmd 1401,54320 +(defcustom proof-shell-trace-output-regexp 1423,55226 +(defcustom proof-shell-thms-output-regexp 1441,55828 +(defcustom proof-shell-interactive-prompt-regexp 1449,56162 +(defcustom proof-tokens-activate-command 1468,56815 +(defcustom proof-tokens-deactivate-command 1475,57055 +(defcustom proof-tokens-extra-modes 1482,57300 +(defcustom proof-shell-unicode 1497,57805 +(defcustom proof-shell-filename-escapes 1506,58195 +(defcustom proof-shell-process-connection-type 1523,58875 +(defcustom proof-shell-strip-crs-from-input 1529,59066 +(defcustom proof-shell-strip-crs-from-output 1541,59549 +(defcustom proof-shell-extend-queue-hook 1549,59917 +(defcustom proof-shell-insert-hook 1559,60347 +(defcustom proof-script-preprocess 1602,62445 +(defcustom proof-shell-handle-delayed-output-hook1608,62596 +(defcustom proof-shell-handle-error-or-interrupt-hook1614,62811 +(defcustom proof-shell-pre-interrupt-hook1632,63557 +(defcustom proof-shell-handle-output-system-specific 1640,63828 +(defcustom proof-state-change-hook 1663,64801 +(defcustom proof-shell-syntax-table-entries 1673,65194 +(defgroup proof-goals 1691,65565 +(defcustom pg-subterm-first-special-char 1696,65686 +(defcustom pg-subterm-anns-use-stack 1704,65998 +(defcustom pg-goals-change-goal 1713,66297 +(defcustom pbp-goal-command 1718,66413 +(defcustom pbp-hyp-command 1723,66577 +(defcustom pg-subterm-help-cmd 1728,66747 +(defcustom pg-goals-error-regexp 1735,66991 +(defcustom proof-shell-result-start 1740,67159 +(defcustom proof-shell-result-end 1746,67401 +(defcustom pg-subterm-start-char 1752,67614 +(defcustom pg-subterm-sep-char 1763,68088 +(defcustom pg-subterm-end-char 1769,68267 +(defcustom pg-topterm-regexp 1775,68424 +(defcustom proof-goals-font-lock-keywords 1790,69024 +(defcustom proof-response-font-lock-keywords 1798,69383 +(defcustom proof-shell-font-lock-keywords 1806,69745 +(defcustom pg-before-fontify-output-hook 1817,70259 +(defcustom pg-after-fontify-output-hook 1825,70620 generic/proof-depends.el,917 -(defvar proof-thm-names-of-files 25,639 -(defvar proof-def-names-of-files 31,923 -(defun proof-depends-module-name-for-buffer 42,1238 -(defun proof-depends-module-of 52,1679 -(defun proof-depends-names-in-same-file 60,1970 -(defun proof-depends-process-dependencies 79,2578 -(defun proof-dependency-in-span-context-menu 132,4313 -(defun proof-dep-alldeps-menu 155,5203 -(defun proof-dep-make-alldeps-menu 161,5429 -(defun proof-dep-split-deps 179,5924 -(defun proof-dep-make-submenu 198,6590 -(defun proof-make-highlight-depts-menu 209,7001 -(defun proof-goto-dependency 220,7309 -(defun proof-show-dependency 227,7561 -(defconst pg-dep-span-priority 234,7850 -(defconst pg-ordinary-span-priority 235,7886 -(defun proof-highlight-depcs 237,7928 -(defun proof-highlight-depts 248,8394 -(defun proof-depends-save-old-face 260,8904 -(defun proof-depends-restore-old-face 265,9081 -(defun proof-dep-unhighlight 271,9310 +(defvar proof-thm-names-of-files 25,586 +(defvar proof-def-names-of-files 31,870 +(defun proof-depends-module-name-for-buffer 42,1185 +(defun proof-depends-module-of 52,1626 +(defun proof-depends-names-in-same-file 60,1917 +(defun proof-depends-process-dependencies 79,2525 +(defun proof-dependency-in-span-context-menu 132,4260 +(defun proof-dep-alldeps-menu 155,5150 +(defun proof-dep-make-alldeps-menu 161,5376 +(defun proof-dep-split-deps 179,5871 +(defun proof-dep-make-submenu 198,6537 +(defun proof-make-highlight-depts-menu 209,6948 +(defun proof-goto-dependency 220,7256 +(defun proof-show-dependency 227,7508 +(defconst pg-dep-span-priority 234,7797 +(defconst pg-ordinary-span-priority 235,7833 +(defun proof-highlight-depcs 237,7875 +(defun proof-highlight-depts 248,8341 +(defun proof-depends-save-old-face 260,8851 +(defun proof-depends-restore-old-face 265,9028 +(defun proof-dep-unhighlight 271,9257 generic/proof-easy-config.el,192 -(defconst proof-easy-config-derived-modes-table16,544 -(defun proof-easy-config-define-derived-modes 23,950 -(defun proof-easy-config-check-setup 52,2135 -(defmacro proof-easy-config 84,3465 +(defconst proof-easy-config-derived-modes-table16,487 +(defun proof-easy-config-define-derived-modes 23,893 +(defun proof-easy-config-check-setup 52,2078 +(defmacro proof-easy-config 84,3408 generic/proof-faces.el,1809 -(defgroup proof-faces 29,809 -(defconst pg-defface-window-systems36,989 -(defmacro proof-face-specs 49,1551 -(defface proof-queue-face64,2003 -(defface proof-locked-face72,2281 -(defface proof-declaration-name-face82,2602 -(defface proof-tacticals-name-face91,2888 -(defface proof-tactics-name-face100,3150 -(defface proof-error-face109,3415 -(defface proof-warning-face117,3636 -(defface proof-eager-annotation-face126,3893 -(defface proof-debug-message-face134,4111 -(defface proof-boring-face142,4310 -(defface proof-mouse-highlight-face150,4502 -(defface proof-command-mouse-highlight-face158,4720 -(defface proof-region-mouse-highlight-face166,4959 -(defface proof-highlight-dependent-face174,5201 -(defface proof-highlight-dependency-face182,5408 -(defface proof-active-area-face190,5605 -(defface proof-script-sticky-error-face198,5917 -(defface proof-script-highlight-error-face206,6146 -(defconst proof-face-compat-doc 218,6491 -(defconst proof-queue-face 219,6571 -(defconst proof-locked-face 220,6639 -(defconst proof-declaration-name-face 221,6709 -(defconst proof-tacticals-name-face 222,6799 -(defconst proof-tactics-name-face 223,6885 -(defconst proof-error-face 224,6967 -(defconst proof-script-sticky-error-face 225,7035 -(defconst proof-script-highlight-error-face 226,7131 -(defconst proof-warning-face 227,7233 -(defconst proof-eager-annotation-face 228,7305 -(defconst proof-debug-message-face 229,7395 -(defconst proof-boring-face 230,7479 -(defconst proof-mouse-highlight-face 231,7549 -(defconst proof-command-mouse-highlight-face 232,7637 -(defconst proof-region-mouse-highlight-face 233,7741 -(defconst proof-highlight-dependent-face 234,7843 -(defconst proof-highlight-dependency-face 235,7939 -(defconst proof-active-area-face 236,8037 -(defconst proof-script-error-face 237,8117 +(defgroup proof-faces 29,758 +(defconst pg-defface-window-systems36,938 +(defmacro proof-face-specs 49,1500 +(defface proof-queue-face64,1952 +(defface proof-locked-face72,2230 +(defface proof-declaration-name-face82,2551 +(defface proof-tacticals-name-face91,2837 +(defface proof-tactics-name-face100,3099 +(defface proof-error-face109,3364 +(defface proof-warning-face117,3585 +(defface proof-eager-annotation-face126,3842 +(defface proof-debug-message-face134,4060 +(defface proof-boring-face142,4259 +(defface proof-mouse-highlight-face150,4451 +(defface proof-command-mouse-highlight-face158,4669 +(defface proof-region-mouse-highlight-face166,4908 +(defface proof-highlight-dependent-face174,5150 +(defface proof-highlight-dependency-face182,5357 +(defface proof-active-area-face190,5554 +(defface proof-script-sticky-error-face198,5866 +(defface proof-script-highlight-error-face206,6095 +(defconst proof-face-compat-doc 218,6440 +(defconst proof-queue-face 219,6520 +(defconst proof-locked-face 220,6588 +(defconst proof-declaration-name-face 221,6658 +(defconst proof-tacticals-name-face 222,6748 +(defconst proof-tactics-name-face 223,6834 +(defconst proof-error-face 224,6916 +(defconst proof-script-sticky-error-face 225,6984 +(defconst proof-script-highlight-error-face 226,7080 +(defconst proof-warning-face 227,7182 +(defconst proof-eager-annotation-face 228,7254 +(defconst proof-debug-message-face 229,7344 +(defconst proof-boring-face 230,7428 +(defconst proof-mouse-highlight-face 231,7498 +(defconst proof-command-mouse-highlight-face 232,7586 +(defconst proof-region-mouse-highlight-face 233,7690 +(defconst proof-highlight-dependent-face 234,7792 +(defconst proof-highlight-dependency-face 235,7888 +(defconst proof-active-area-face 236,7986 +(defconst proof-script-error-face 237,8066 generic/proof-indent.el,219 -(defun proof-indent-indent 19,449 -(defun proof-indent-offset 28,715 -(defun proof-indent-inner-p 45,1316 -(defun proof-indent-goto-prev 54,1616 -(defun proof-indent-calculate 61,1949 -(defun proof-indent-line 82,2708 +(defun proof-indent-indent 19,397 +(defun proof-indent-offset 28,663 +(defun proof-indent-inner-p 45,1264 +(defun proof-indent-goto-prev 54,1564 +(defun proof-indent-calculate 61,1897 +(defun proof-indent-line 82,2656 generic/proof-maths-menu.el,83 -(defun proof-maths-menu-set-global 32,906 -(defun proof-maths-menu-enable 46,1357 +(defun proof-maths-menu-set-global 32,850 +(defun proof-maths-menu-enable 46,1301 generic/proof-menu.el,2215 -(defvar proof-display-some-buffers-count 36,820 -(defun proof-display-some-buffers 38,865 -(defun proof-menu-define-keys 95,2992 -(defun proof-menu-define-main 153,5817 -(defvar proof-menu-favourites 162,6002 -(defvar proof-menu-settings 165,6109 -(defun proof-menu-define-specific 169,6198 -(defun proof-assistant-menu-update 212,7460 -(defvar proof-help-menu226,7893 -(defvar proof-show-hide-menu234,8157 -(defvar proof-buffer-menu245,8581 -(defun proof-keep-response-history 309,10937 -(defconst proof-quick-opts-menu317,11247 -(defun proof-quick-opts-vars 539,20314 -(defun proof-quick-opts-changed-from-defaults-p 571,21254 -(defun proof-quick-opts-changed-from-saved-p 575,21359 -(defun proof-set-document-centred 583,21515 -(defun proof-set-non-document-centred 596,21941 -(defun proof-quick-opts-save 615,22652 -(defun proof-quick-opts-reset 620,22820 -(defconst proof-config-menu632,23088 -(defconst proof-advanced-menu639,23267 -(defvar proof-menu657,23951 -(defun proof-main-menu 666,24233 -(defun proof-aux-menu 678,24572 -(defun proof-menu-define-favourites-menu 694,24918 -(defun proof-def-favourite 714,25567 -(defvar proof-make-favourite-cmd-history 741,26560 -(defvar proof-make-favourite-menu-history 744,26645 -(defun proof-save-favourites 747,26731 -(defun proof-del-favourite 752,26879 -(defun proof-read-favourite 769,27435 -(defun proof-add-favourite 793,28209 -(defun proof-menu-define-settings-menu 820,29254 -(defun proof-menu-entry-name 849,30246 -(defun proof-menu-entry-for-setting 859,30596 -(defun proof-settings-vars 882,31234 -(defun proof-settings-changed-from-defaults-p 887,31411 -(defun proof-settings-changed-from-saved-p 891,31517 -(defun proof-settings-save 895,31620 -(defun proof-settings-reset 900,31787 -(defun proof-assistant-invisible-command-ifposs 905,31950 -(defun proof-maybe-askprefs 927,32920 -(defun proof-assistant-settings-cmd 943,33537 -(defun proof-assistant-settings-cmds 951,33820 -(defvar proof-assistant-format-table966,34262 -(defun proof-assistant-format-bool 975,34688 -(defun proof-assistant-format-int 978,34801 -(defun proof-assistant-format-float 981,34893 -(defun proof-assistant-format-string 984,34989 -(defun proof-assistant-format 987,35087 +(defvar proof-display-some-buffers-count 36,770 +(defun proof-display-some-buffers 38,815 +(defun proof-menu-define-keys 95,2956 +(defun proof-menu-define-main 154,5862 +(defvar proof-menu-favourites 163,6047 +(defvar proof-menu-settings 166,6154 +(defun proof-menu-define-specific 170,6243 +(defun proof-assistant-menu-update 213,7505 +(defvar proof-help-menu227,7938 +(defvar proof-show-hide-menu235,8202 +(defvar proof-buffer-menu246,8626 +(defun proof-keep-response-history 310,10982 +(defconst proof-quick-opts-menu318,11292 +(defun proof-quick-opts-vars 540,20359 +(defun proof-quick-opts-changed-from-defaults-p 572,21299 +(defun proof-quick-opts-changed-from-saved-p 576,21404 +(defun proof-set-document-centred 584,21560 +(defun proof-set-non-document-centred 597,21986 +(defun proof-quick-opts-save 616,22697 +(defun proof-quick-opts-reset 621,22865 +(defconst proof-config-menu633,23133 +(defconst proof-advanced-menu640,23312 +(defvar proof-menu658,23996 +(defun proof-main-menu 667,24278 +(defun proof-aux-menu 679,24617 +(defun proof-menu-define-favourites-menu 695,24963 +(defun proof-def-favourite 715,25612 +(defvar proof-make-favourite-cmd-history 742,26605 +(defvar proof-make-favourite-menu-history 745,26690 +(defun proof-save-favourites 748,26776 +(defun proof-del-favourite 753,26924 +(defun proof-read-favourite 770,27480 +(defun proof-add-favourite 794,28254 +(defun proof-menu-define-settings-menu 821,29299 +(defun proof-menu-entry-name 850,30291 +(defun proof-menu-entry-for-setting 860,30641 +(defun proof-settings-vars 883,31279 +(defun proof-settings-changed-from-defaults-p 888,31456 +(defun proof-settings-changed-from-saved-p 892,31562 +(defun proof-settings-save 896,31665 +(defun proof-settings-reset 901,31832 +(defun proof-assistant-invisible-command-ifposs 906,31995 +(defun proof-maybe-askprefs 928,32965 +(defun proof-assistant-settings-cmd 944,33582 +(defun proof-assistant-settings-cmds 952,33865 +(defvar proof-assistant-format-table967,34307 +(defun proof-assistant-format-bool 976,34733 +(defun proof-assistant-format-int 979,34846 +(defun proof-assistant-format-float 982,34938 +(defun proof-assistant-format-string 985,35034 +(defun proof-assistant-format 988,35132 generic/proof-mmm.el,70 -(defun proof-mmm-set-global 43,1439 -(defun proof-mmm-enable 58,1978 +(defun proof-mmm-set-global 43,1390 +(defun proof-mmm-enable 58,1929 generic/proof-script.el,5813 -(deflocal proof-active-buffer-fake-minor-mode 46,1413 -(deflocal proof-script-buffer-file-name 49,1539 -(deflocal pg-script-portions 56,1949 -(defalias 'proof-active-buffer-fake-minor-modeproof-active-buffer-fake-minor-mode59,2055 -(defun proof-next-element-count 68,2250 -(defun proof-element-id 74,2492 -(defun proof-next-element-id 78,2661 -(deflocal proof-locked-span 114,3965 -(deflocal proof-queue-span 121,4231 -(deflocal proof-overlay-arrow 130,4717 -(defun proof-span-give-warning 136,4844 -(defun proof-span-read-only 142,5024 -(defun proof-strict-read-only 151,5397 -(defsubst proof-set-queue-endpoints 161,5775 -(defun proof-set-overlay-arrow 165,5916 -(defsubst proof-set-locked-endpoints 176,6254 -(defsubst proof-detach-queue 181,6430 -(defsubst proof-detach-locked 186,6569 -(defsubst proof-set-queue-start 193,6794 -(defsubst proof-set-locked-end 197,6920 -(defsubst proof-set-queue-end 209,7390 -(defun proof-init-segmentation 220,7687 -(defun proof-colour-locked 250,8938 -(defun proof-colour-locked-span 257,9211 -(defun proof-sticky-errors 263,9484 -(defun proof-restart-buffers 276,9900 -(defun proof-script-buffers-with-spans 300,10833 -(defun proof-script-remove-all-spans-and-deactivate 310,11189 -(defun proof-script-clear-queue-spans-on-error 314,11379 -(defun proof-script-delete-spans 340,12396 -(defun proof-script-delete-secondary-spans 345,12595 -(defun proof-unprocessed-begin 358,12884 -(defun proof-script-end 366,13138 -(defun proof-queue-or-locked-end 375,13448 -(defun proof-locked-region-full-p 394,14041 -(defun proof-locked-region-empty-p 403,14313 -(defun proof-only-whitespace-to-locked-region-p 407,14463 -(defun proof-in-locked-region-p 417,14812 -(defun proof-goto-end-of-locked 429,15069 -(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 446,15828 -(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 457,16309 -(defun proof-end-of-locked-visible-p 469,16849 -(defconst pg-idioms 488,17442 -(defconst pg-all-idioms 491,17538 -(defun pg-clear-script-portions 495,17659 -(defun pg-remove-element 501,17894 -(defun pg-get-element 509,18197 -(defun pg-add-element 519,18512 -(defun pg-invisible-prop 567,20474 -(defun pg-set-element-span-invisible 572,20675 -(defun pg-toggle-element-span-visibility 585,21241 -(defun pg-open-invisible-span 590,21402 -(defun pg-make-element-invisible 595,21573 -(defun pg-make-element-visible 600,21784 -(defun pg-toggle-element-visibility 605,21978 -(defun pg-show-all-portions 611,22241 -(defun pg-show-all-proofs 633,22985 -(defun pg-hide-all-proofs 638,23113 -(defun pg-add-proof-element 643,23244 -(defun pg-span-name 658,24031 -(defvar pg-span-context-menu-keymap691,25238 -(defun pg-last-output-displayform 698,25476 -(defun pg-set-span-helphighlights 721,26367 -(defun proof-complete-buffer-atomic 784,28514 -(defun proof-register-possibly-new-processed-file813,29784 -(defun proof-query-save-this-buffer-p 859,31658 -(defun proof-inform-prover-file-retracted 864,31883 -(defun proof-auto-retract-dependencies 884,32734 -(defun proof-unregister-buffer-file-name 938,35284 -(defsubst proof-action-completed 984,37109 -(defun proof-protected-process-or-retract 988,37279 -(defun proof-deactivate-scripting-auto 1016,38510 -(defun proof-deactivate-scripting-query-user-action 1025,38868 -(defun proof-deactivate-scripting-choose-action 1069,40377 -(defun proof-deactivate-scripting 1081,40762 -(defun proof-activate-scripting 1178,44885 -(defun proof-toggle-active-scripting 1278,49410 -(defun proof-done-advancing 1317,50655 -(defun proof-done-advancing-comment 1385,53152 -(defun proof-done-advancing-save 1419,54538 -(defun proof-make-goalsave1507,57902 -(defun proof-get-name-from-goal 1525,58767 -(defun proof-done-advancing-autosave 1545,59792 -(defun proof-done-advancing-other 1609,62288 -(defun proof-segment-up-to-parser 1638,63252 -(defun proof-script-generic-parse-find-comment-end 1708,65533 -(defun proof-script-generic-parse-cmdend 1717,65947 -(defun proof-script-generic-parse-cmdstart 1768,67843 -(defun proof-script-generic-parse-sexp 1807,69443 -(defun proof-semis-to-vanillas 1819,69909 -(defun proof-next-command-new-line 1872,71582 -(defun proof-script-next-command-advance 1877,71788 -(defun proof-assert-until-point 1896,72288 -(defun proof-assert-electric-terminator 1912,72959 -(defun proof-assert-semis 1956,74639 -(defun proof-retract-before-change 1970,75400 -(defun proof-insert-pbp-command 1993,76056 -(defun proof-insert-sendback-command 2008,76559 -(defun proof-done-retracting 2034,77462 -(defun proof-setup-retract-action 2069,78916 -(defun proof-last-goal-or-goalsave 2081,79521 -(defun proof-retract-target 2105,80433 -(defun proof-retract-until-point-interactive 2184,83686 -(defun proof-retract-until-point 2193,84093 -(define-derived-mode proof-mode 2248,86098 -(defun proof-script-set-visited-file-name 2284,87480 -(defun proof-script-set-buffer-hooks 2306,88493 -(defun proof-script-kill-buffer-fn 2314,88911 -(defun proof-config-done-related 2346,90228 -(defun proof-generic-goal-command-p 2411,92713 -(defun proof-generic-state-preserving-p 2416,92926 -(defun proof-generic-count-undos 2425,93443 -(defun proof-generic-find-and-forget 2456,94571 -(defconst proof-script-important-settings2507,96343 -(defun proof-config-done 2522,96889 -(defun proof-setup-parsing-mechanism 2589,99054 -(defun proof-setup-imenu 2613,100126 -(deflocal proof-segment-up-to-cache 2650,101408 -(deflocal proof-segment-up-to-cache-start 2654,101551 -(deflocal proof-segment-up-to-cache-end 2655,101596 -(deflocal proof-last-edited-low-watermark 2656,101639 -(defun proof-segment-up-to-using-cache 2658,101687 -(defun proof-segment-cache-contents-for 2686,102807 -(defun proof-script-after-change-function 2703,103389 -(defun proof-script-set-after-change-functions 2715,103896 - -generic/proof-shell.el,3700 -(defvar proof-marker 34,743 -(defvar proof-action-list 37,839 -(defsubst proof-shell-invoke-callback 77,2385 -(defvar proof-shell-last-goals-output 91,2877 -(defvar proof-shell-last-response-output 94,2957 -(defvar proof-shell-delayed-output-start 97,3044 -(defvar proof-shell-delayed-output-end 101,3226 -(defvar proof-shell-delayed-output-flags 105,3406 -(defvar proof-shell-interrupt-pending 108,3531 -(defvar proof-shell-exit-in-progress 113,3755 -(defcustom proof-shell-active-scripting-indicator125,4100 -(defun proof-shell-ready-prover 177,5684 -(defsubst proof-shell-live-buffer 191,6223 -(defun proof-shell-available-p 198,6443 -(defun proof-grab-lock 204,6665 -(defun proof-release-lock 214,7094 -(defcustom proof-shell-fiddle-frames 224,7268 -(defun proof-shell-set-text-representation 229,7426 -(defun proof-shell-start 237,7754 -(defvar proof-shell-kill-function-hooks 416,13848 -(defun proof-shell-kill-function 419,13946 -(defun proof-shell-clear-state 482,16148 -(defun proof-shell-exit 498,16623 -(defun proof-shell-bail-out 522,17557 -(defun proof-shell-restart 532,18079 -(defvar proof-shell-urgent-message-marker 573,19451 -(defvar proof-shell-urgent-message-scanner 576,19572 -(defun proof-shell-handle-error-output 580,19757 -(defun proof-shell-handle-error-or-interrupt 606,20619 -(defun proof-shell-error-or-interrupt-action 649,22368 -(defun proof-goals-pos 676,23465 -(defun proof-pbp-focus-on-first-goal 681,23676 -(defsubst proof-shell-string-match-safe 693,24092 -(defun proof-shell-handle-immediate-output 697,24253 -(defun proof-interrupt-process 764,26860 -(defun proof-shell-insert 798,28093 -(defun proof-shell-action-list-item 855,30075 -(defun proof-shell-set-silent 860,30317 -(defun proof-shell-start-silent-item 866,30536 -(defun proof-shell-clear-silent 872,30725 -(defun proof-shell-stop-silent-item 878,30947 -(defsubst proof-shell-should-be-silent 884,31136 -(defsubst proof-shell-insert-action-item 895,31646 -(defsubst proof-shell-slurp-comments 899,31821 -(defun proof-add-to-queue 910,32226 -(defun proof-start-queue 968,34250 -(defun proof-extend-queue 980,34645 -(defun proof-shell-exec-loop 999,35264 -(defun proof-shell-insert-loopback-cmd 1067,37567 -(defun proof-shell-process-urgent-message 1092,38731 -(defun proof-shell-process-urgent-message-default 1141,40451 -(defun proof-shell-process-urgent-message-trace 1157,41035 -(defun proof-shell-process-urgent-message-retract 1169,41558 -(defun proof-shell-process-urgent-message-elisp 1195,42688 -(defun proof-shell-process-urgent-message-thmdeps 1210,43183 -(defun proof-shell-strip-eager-annotations 1224,43562 -(defun proof-shell-filter 1240,44062 -(defun proof-shell-filter-first-command 1340,47434 -(defun proof-shell-process-urgent-messages 1355,47977 -(defun proof-shell-filter-manage-output 1405,49543 -(defsubst proof-shell-display-output-as-response 1437,50790 -(defun proof-shell-handle-delayed-output 1443,51085 -(defvar pg-last-tracing-output-time 1531,54258 -(defvar pg-last-trace-output-count 1534,54371 -(defconst pg-slow-mode-trigger-count 1537,54456 -(defconst pg-slow-mode-duration 1540,54561 -(defconst pg-fast-tracing-mode-threshold 1543,54643 -(defun pg-tracing-tight-loop 1546,54772 -(defun pg-finish-tracing-display 1570,55804 -(defun proof-shell-wait 1588,56185 -(defun proof-done-invisible 1618,57396 -(defun proof-shell-invisible-command 1624,57566 -(defun proof-shell-invisible-cmd-get-result 1671,59158 -(defun proof-shell-invisible-command-invisible-result 1683,59594 -(defun pg-insert-last-output-as-comment 1703,60095 -(define-derived-mode proof-shell-mode 1722,60567 -(defconst proof-shell-important-settings1759,61594 -(defun proof-shell-config-done 1765,61709 +(deflocal proof-active-buffer-fake-minor-mode 46,1361 +(deflocal proof-script-buffer-file-name 49,1487 +(deflocal pg-script-portions 56,1897 +(defalias 'proof-active-buffer-fake-minor-modeproof-active-buffer-fake-minor-mode59,2003 +(defun proof-next-element-count 68,2198 +(defun proof-element-id 74,2440 +(defun proof-next-element-id 78,2609 +(deflocal proof-locked-span 114,3913 +(deflocal proof-queue-span 121,4179 +(deflocal proof-overlay-arrow 130,4665 +(defun proof-span-give-warning 136,4792 +(defun proof-span-read-only 142,4972 +(defun proof-strict-read-only 151,5345 +(defsubst proof-set-queue-endpoints 161,5723 +(defun proof-set-overlay-arrow 165,5864 +(defsubst proof-set-locked-endpoints 176,6202 +(defsubst proof-detach-queue 181,6378 +(defsubst proof-detach-locked 186,6517 +(defsubst proof-set-queue-start 193,6742 +(defsubst proof-set-locked-end 197,6868 +(defsubst proof-set-queue-end 209,7338 +(defun proof-init-segmentation 220,7635 +(defun proof-colour-locked 250,8886 +(defun proof-colour-locked-span 257,9159 +(defun proof-sticky-errors 263,9432 +(defun proof-restart-buffers 276,9848 +(defun proof-script-buffers-with-spans 300,10781 +(defun proof-script-remove-all-spans-and-deactivate 310,11137 +(defun proof-script-clear-queue-spans-on-error 314,11327 +(defun proof-script-delete-spans 340,12344 +(defun proof-script-delete-secondary-spans 345,12543 +(defun proof-unprocessed-begin 358,12832 +(defun proof-script-end 366,13086 +(defun proof-queue-or-locked-end 375,13396 +(defun proof-locked-region-full-p 394,13989 +(defun proof-locked-region-empty-p 403,14261 +(defun proof-only-whitespace-to-locked-region-p 407,14411 +(defun proof-in-locked-region-p 417,14760 +(defun proof-goto-end-of-locked 429,15017 +(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 446,15804 +(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 457,16285 +(defun proof-end-of-locked-visible-p 469,16825 +(defconst pg-idioms 488,17418 +(defconst pg-all-idioms 491,17514 +(defun pg-clear-script-portions 495,17635 +(defun pg-remove-element 501,17870 +(defun pg-get-element 509,18173 +(defun pg-add-element 519,18488 +(defun pg-invisible-prop 567,20450 +(defun pg-set-element-span-invisible 572,20651 +(defun pg-toggle-element-span-visibility 585,21217 +(defun pg-open-invisible-span 590,21378 +(defun pg-make-element-invisible 595,21549 +(defun pg-make-element-visible 600,21760 +(defun pg-toggle-element-visibility 605,21954 +(defun pg-show-all-portions 611,22217 +(defun pg-show-all-proofs 633,22961 +(defun pg-hide-all-proofs 638,23089 +(defun pg-add-proof-element 643,23220 +(defun pg-span-name 658,24007 +(defvar pg-span-context-menu-keymap691,25214 +(defun pg-last-output-displayform 698,25452 +(defun pg-set-span-helphighlights 721,26343 +(defun proof-complete-buffer-atomic 784,28490 +(defun proof-register-possibly-new-processed-file813,29760 +(defun proof-query-save-this-buffer-p 859,31634 +(defun proof-inform-prover-file-retracted 864,31859 +(defun proof-auto-retract-dependencies 884,32710 +(defun proof-unregister-buffer-file-name 938,35260 +(defsubst proof-action-completed 984,37085 +(defun proof-protected-process-or-retract 988,37255 +(defun proof-deactivate-scripting-auto 1016,38486 +(defun proof-deactivate-scripting-query-user-action 1025,38844 +(defun proof-deactivate-scripting-choose-action 1069,40353 +(defun proof-deactivate-scripting 1081,40738 +(defun proof-activate-scripting 1178,44861 +(defun proof-toggle-active-scripting 1278,49400 +(defun proof-done-advancing 1317,50645 +(defun proof-done-advancing-comment 1385,53142 +(defun proof-done-advancing-save 1419,54528 +(defun proof-make-goalsave1507,57892 +(defun proof-get-name-from-goal 1525,58757 +(defun proof-done-advancing-autosave 1545,59782 +(defun proof-done-advancing-other 1609,62278 +(defun proof-segment-up-to-parser 1638,63242 +(defun proof-script-generic-parse-find-comment-end 1708,65523 +(defun proof-script-generic-parse-cmdend 1717,65937 +(defun proof-script-generic-parse-cmdstart 1768,67833 +(defun proof-script-generic-parse-sexp 1807,69433 +(defun proof-semis-to-vanillas 1819,69899 +(defun proof-next-command-new-line 1872,71572 +(defun proof-script-next-command-advance 1877,71778 +(defun proof-assert-until-point 1896,72278 +(defun proof-assert-electric-terminator 1912,72949 +(defun proof-assert-semis 1956,74629 +(defun proof-retract-before-change 1970,75390 +(defun proof-insert-pbp-command 1993,76046 +(defun proof-insert-sendback-command 2008,76549 +(defun proof-done-retracting 2034,77452 +(defun proof-setup-retract-action 2069,78906 +(defun proof-last-goal-or-goalsave 2081,79511 +(defun proof-retract-target 2105,80423 +(defun proof-retract-until-point-interactive 2184,83676 +(defun proof-retract-until-point 2193,84083 +(define-derived-mode proof-mode 2248,86088 +(defun proof-script-set-visited-file-name 2284,87470 +(defun proof-script-set-buffer-hooks 2306,88483 +(defun proof-script-kill-buffer-fn 2314,88901 +(defun proof-config-done-related 2346,90218 +(defun proof-generic-goal-command-p 2411,92703 +(defun proof-generic-state-preserving-p 2416,92916 +(defun proof-generic-count-undos 2425,93433 +(defun proof-generic-find-and-forget 2456,94561 +(defconst proof-script-important-settings2507,96333 +(defun proof-config-done 2522,96879 +(defun proof-setup-parsing-mechanism 2589,99044 +(defun proof-setup-imenu 2613,100116 +(deflocal proof-segment-up-to-cache 2650,101398 +(deflocal proof-segment-up-to-cache-start 2654,101541 +(deflocal proof-segment-up-to-cache-end 2655,101586 +(deflocal proof-last-edited-low-watermark 2656,101629 +(defun proof-segment-up-to-using-cache 2658,101677 +(defun proof-segment-cache-contents-for 2686,102797 +(defun proof-script-after-change-function 2703,103379 +(defun proof-script-set-after-change-functions 2715,103886 + +generic/proof-shell.el,3766 +(defvar proof-marker 35,721 +(defvar proof-action-list 38,817 +(defsubst proof-shell-invoke-callback 80,2530 +(defvar proof-shell-last-goals-output 94,3022 +(defvar proof-shell-last-response-output 97,3102 +(defvar proof-shell-delayed-output-start 100,3189 +(defvar proof-shell-delayed-output-end 104,3371 +(defvar proof-shell-delayed-output-flags 108,3551 +(defvar proof-shell-interrupt-pending 111,3676 +(defvar proof-shell-exit-in-progress 116,3900 +(defcustom proof-shell-active-scripting-indicator128,4245 +(defun proof-shell-ready-prover 180,5829 +(defsubst proof-shell-live-buffer 194,6368 +(defun proof-shell-available-p 201,6588 +(defun proof-grab-lock 207,6810 +(defun proof-release-lock 217,7239 +(defcustom proof-shell-fiddle-frames 227,7413 +(defun proof-shell-set-text-representation 232,7571 +(defun proof-shell-start 240,7899 +(defvar proof-shell-kill-function-hooks 419,13993 +(defun proof-shell-kill-function 422,14091 +(defun proof-shell-clear-state 485,16293 +(defun proof-shell-exit 501,16768 +(defun proof-shell-bail-out 525,17702 +(defun proof-shell-restart 535,18224 +(defvar proof-shell-urgent-message-marker 576,19596 +(defvar proof-shell-urgent-message-scanner 579,19717 +(defun proof-shell-handle-error-output 583,19902 +(defun proof-shell-handle-error-or-interrupt 609,20764 +(defun proof-shell-error-or-interrupt-action 652,22513 +(defun proof-goals-pos 679,23610 +(defun proof-pbp-focus-on-first-goal 684,23821 +(defsubst proof-shell-string-match-safe 696,24237 +(defun proof-shell-handle-immediate-output 700,24398 +(defun proof-interrupt-process 767,27005 +(defun proof-shell-insert 801,28238 +(defun proof-shell-action-list-item 858,30220 +(defun proof-shell-set-silent 863,30462 +(defun proof-shell-start-silent-item 869,30681 +(defun proof-shell-clear-silent 875,30870 +(defun proof-shell-stop-silent-item 881,31092 +(defsubst proof-shell-should-be-silent 887,31281 +(defsubst proof-shell-insert-action-item 899,31854 +(defsubst proof-shell-slurp-comments 903,32029 +(defun proof-add-to-queue 914,32434 +(defun proof-start-queue 966,34386 +(defun proof-extend-queue 978,34781 +(defun proof-shell-exec-loop 997,35400 +(defun proof-shell-insert-loopback-cmd 1079,38340 +(defun proof-shell-process-urgent-message 1104,39504 +(defun proof-shell-process-urgent-message-default 1160,41529 +(defun proof-shell-process-urgent-message-trace 1176,42113 +(defun proof-shell-process-urgent-message-retract 1188,42636 +(defun proof-shell-process-urgent-message-elisp 1214,43766 +(defun proof-shell-process-urgent-message-thmdeps 1229,44261 +(defun proof-shell-process-interactive-prompt-regexp 1239,44605 +(defun proof-shell-strip-eager-annotations 1251,44961 +(defun proof-shell-filter 1267,45461 +(defun proof-shell-filter-first-command 1367,48833 +(defun proof-shell-process-urgent-messages 1382,49376 +(defun proof-shell-filter-manage-output 1432,50942 +(defsubst proof-shell-display-output-as-response 1468,52365 +(defun proof-shell-handle-delayed-output 1474,52660 +(defvar pg-last-tracing-output-time 1562,55835 +(defvar pg-last-trace-output-count 1565,55948 +(defconst pg-slow-mode-trigger-count 1568,56033 +(defconst pg-slow-mode-duration 1571,56138 +(defconst pg-fast-tracing-mode-threshold 1574,56220 +(defun pg-tracing-tight-loop 1577,56349 +(defun pg-finish-tracing-display 1601,57381 +(defun proof-shell-wait 1619,57762 +(defun proof-done-invisible 1649,58973 +(defun proof-shell-invisible-command 1655,59143 +(defun proof-shell-invisible-cmd-get-result 1702,60735 +(defun proof-shell-invisible-command-invisible-result 1714,61171 +(defun pg-insert-last-output-as-comment 1734,61672 +(define-derived-mode proof-shell-mode 1753,62144 +(defconst proof-shell-important-settings1790,63171 +(defun proof-shell-config-done 1796,63286 generic/proof-site.el,666 -(defconst proof-assistant-table-default35,1207 -(defconst proof-general-short-version68,2229 -(defconst proof-general-version-year 74,2416 -(defgroup proof-general 81,2569 -(defgroup proof-general-internals 86,2677 -(defun proof-home-directory-fn 99,3065 -(defcustom proof-home-directory110,3437 -(defcustom proof-images-directory119,3803 -(defcustom proof-info-directory125,4005 -(defcustom proof-assistant-table154,4982 -(defcustom proof-assistants 195,6424 -(defun proof-ready-for-assistant 224,7578 -(defvar proof-general-configured-provers 276,9870 -(defun proof-chose-prover 349,12481 -(defun proofgeneral 354,12613 -(defun proof-visit-example-file 363,12931 - -generic/proof-splash.el,991 -(defcustom proof-splash-enable 34,1007 -(defcustom proof-splash-time 39,1159 -(defcustom proof-splash-contents47,1443 -(defconst proof-splash-startup-msg91,3008 -(defconst proof-splash-welcome 100,3386 -(define-derived-mode proof-splash-mode 103,3490 -(define-key proof-splash-mode-map 109,3664 -(define-key proof-splash-mode-map 110,3716 -(defsubst proof-emacs-imagep 115,3843 -(defun proof-get-image 120,3968 -(defvar proof-splash-timeout-conf 142,4768 -(defun proof-splash-centre-spaces 145,4881 -(defun proof-splash-remove-screen 172,6037 -(defun proof-splash-remove-buffer 189,6693 -(defvar proof-splash-seen 200,7081 -(defun proof-splash-insert-contents 203,7183 -(defun proof-splash-display-screen 243,8313 -(defalias 'pg-about pg-about279,9835 -(defun proof-splash-message 282,9901 -(defun proof-splash-timeout-waiter 295,10345 -(defvar proof-splash-old-frame-title-format 308,10903 -(defun proof-splash-set-frame-titles 310,10953 -(defun proof-splash-unset-frame-titles 319,11268 +(defconst proof-assistant-table-default35,1157 +(defconst proof-general-short-version68,2172 +(defconst proof-general-version-year 74,2359 +(defgroup proof-general 81,2512 +(defgroup proof-general-internals 86,2620 +(defun proof-home-directory-fn 99,3008 +(defcustom proof-home-directory110,3380 +(defcustom proof-images-directory119,3746 +(defcustom proof-info-directory125,3948 +(defcustom proof-assistant-table154,4925 +(defcustom proof-assistants 195,6367 +(defun proof-ready-for-assistant 224,7521 +(defvar proof-general-configured-provers 276,9813 +(defun proof-chose-prover 349,12424 +(defun proofgeneral 354,12556 +(defun proof-visit-example-file 363,12874 + +generic/proof-splash.el,990 +(defcustom proof-splash-enable 34,955 +(defcustom proof-splash-time 39,1107 +(defcustom proof-splash-contents47,1391 +(defconst proof-splash-startup-msg91,2956 +(defconst proof-splash-welcome 100,3334 +(define-derived-mode proof-splash-mode 103,3438 +(define-key proof-splash-mode-map 109,3612 +(define-key proof-splash-mode-map 110,3664 +(defsubst proof-emacs-imagep 115,3791 +(defun proof-get-image 120,3916 +(defvar proof-splash-timeout-conf 142,4716 +(defun proof-splash-centre-spaces 145,4829 +(defun proof-splash-remove-screen 172,5985 +(defun proof-splash-remove-buffer 189,6641 +(defvar proof-splash-seen 200,7029 +(defun proof-splash-insert-contents 203,7131 +(defun proof-splash-display-screen 243,8261 +(defalias 'pg-about pg-about279,9783 +(defun proof-splash-message 282,9849 +(defun proof-splash-timeout-waiter 295,10307 +(defvar proof-splash-old-frame-title-format 308,10865 +(defun proof-splash-set-frame-titles 310,10915 +(defun proof-splash-unset-frame-titles 319,11230 generic/proof-syntax.el,1278 -(defsubst proof-ids-to-regexp 22,516 -(defsubst proof-anchor-regexp 29,754 -(defconst proof-no-regexp 33,859 -(defsubst proof-regexp-alt 36,950 -(defsubst proof-regexp-alt-list 45,1262 -(defsubst proof-re-search-forward-region 49,1397 -(defsubst proof-search-forward 62,1895 -(defsubst proof-replace-regexp-in-string 69,2165 -(defsubst proof-re-search-forward 74,2416 -(defsubst proof-re-search-backward 79,2674 -(defsubst proof-re-search-forward-safe 84,2935 -(defsubst proof-string-match 90,3216 -(defsubst proof-string-match-safe 95,3445 -(defsubst proof-stringfn-match 99,3649 -(defsubst proof-looking-at 106,3912 -(defsubst proof-looking-at-safe 111,4099 -(defun proof-buffer-syntactic-context 120,4312 -(defsubst proof-looking-at-syntactic-context-default 141,5174 -(defun proof-looking-at-syntactic-context 150,5529 -(defun proof-inside-comment 159,5991 -(defun proof-inside-string 165,6164 -(defsubst proof-replace-string 175,6363 -(defsubst proof-replace-regexp 180,6567 -(defsubst proof-replace-regexp-nocasefold 185,6776 -(defvar proof-id 195,7064 -(defsubst proof-ids 201,7284 -(defun proof-zap-commas 208,7536 -(defadvice font-lock-fontify-keywords-region234,8422 -(defun proof-format 250,9018 -(defun proof-format-filename 269,9657 -(defun proof-insert 316,11059 - -generic/proof-toolbar.el,2332 -(defun proof-toolbar-function 33,812 -(defun proof-toolbar-icon 37,959 -(defun proof-toolbar-enabler 41,1106 -(defun proof-toolbar-make-icon 50,1308 -(defun proof-toolbar-make-toolbar-items 59,1616 -(defvar proof-toolbar-map 85,2477 -(defun proof-toolbar-available-p 88,2576 -(defun proof-toolbar-setup 98,2882 -(defun proof-toolbar-enable 119,3739 -(defalias 'proof-toolbar-undo proof-toolbar-undo152,4797 -(defun proof-toolbar-undo-enable-p 154,4865 -(defalias 'proof-toolbar-delete proof-toolbar-delete161,5023 -(defun proof-toolbar-delete-enable-p 163,5104 -(defalias 'proof-toolbar-home proof-toolbar-home171,5286 -(defalias 'proof-toolbar-next proof-toolbar-next175,5353 -(defun proof-toolbar-next-enable-p 177,5424 -(defalias 'proof-toolbar-goto proof-toolbar-goto183,5540 -(defun proof-toolbar-goto-enable-p 185,5590 -(defalias 'proof-toolbar-retract proof-toolbar-retract190,5675 -(defun proof-toolbar-retract-enable-p 192,5732 -(defalias 'proof-toolbar-use proof-toolbar-use198,5851 -(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p199,5903 -(defalias 'proof-toolbar-restart proof-toolbar-restart203,5984 -(defalias 'proof-toolbar-goal proof-toolbar-goal207,6049 -(defalias 'proof-toolbar-qed proof-toolbar-qed211,6107 -(defun proof-toolbar-qed-enable-p 213,6156 -(defalias 'proof-toolbar-state proof-toolbar-state221,6318 -(defalias 'proof-toolbar-state-enable-p proof-toolbar-state-enable-p222,6361 -(defalias 'proof-toolbar-context proof-toolbar-context226,6440 -(defalias 'proof-toolbar-context-enable-p proof-toolbar-context-enable-p227,6486 -(defalias 'proof-toolbar-command proof-toolbar-command231,6567 -(defalias 'proof-toolbar-command-enable-p proof-toolbar-command-enable-p232,6623 -(defun proof-toolbar-help 236,6728 -(defalias 'proof-toolbar-find proof-toolbar-find242,6808 -(defalias 'proof-toolbar-find-enable-p proof-toolbar-find-enable-p243,6860 -(defalias 'proof-toolbar-info proof-toolbar-info247,6935 -(defalias 'proof-toolbar-info-enable-p proof-toolbar-info-enable-p248,6990 -(defalias 'proof-toolbar-visibility proof-toolbar-visibility252,7088 -(defun proof-toolbar-visibility-enable-p 254,7148 -(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt259,7262 -(defun proof-toolbar-interrupt-enable-p 260,7323 -(defun proof-toolbar-scripting-menu 268,7476 +(defsubst proof-ids-to-regexp 22,464 +(defsubst proof-anchor-regexp 29,702 +(defconst proof-no-regexp 33,807 +(defsubst proof-regexp-alt 36,898 +(defsubst proof-regexp-alt-list 45,1210 +(defsubst proof-re-search-forward-region 49,1345 +(defsubst proof-search-forward 62,1843 +(defsubst proof-replace-regexp-in-string 69,2113 +(defsubst proof-re-search-forward 74,2364 +(defsubst proof-re-search-backward 79,2622 +(defsubst proof-re-search-forward-safe 84,2883 +(defsubst proof-string-match 90,3164 +(defsubst proof-string-match-safe 95,3393 +(defsubst proof-stringfn-match 99,3597 +(defsubst proof-looking-at 106,3860 +(defsubst proof-looking-at-safe 111,4047 +(defun proof-buffer-syntactic-context 120,4260 +(defsubst proof-looking-at-syntactic-context-default 141,5122 +(defun proof-looking-at-syntactic-context 150,5477 +(defun proof-inside-comment 159,5939 +(defun proof-inside-string 165,6112 +(defsubst proof-replace-string 175,6311 +(defsubst proof-replace-regexp 180,6515 +(defsubst proof-replace-regexp-nocasefold 185,6724 +(defvar proof-id 195,7012 +(defsubst proof-ids 201,7232 +(defun proof-zap-commas 208,7484 +(defadvice font-lock-fontify-keywords-region234,8370 +(defun proof-format 250,8966 +(defun proof-format-filename 269,9605 +(defun proof-insert 316,11007 + +generic/proof-toolbar.el,2401 +(defun proof-toolbar-function 33,759 +(defun proof-toolbar-icon 37,906 +(defun proof-toolbar-enabler 41,1053 +(defun proof-toolbar-make-icon 50,1255 +(defun proof-toolbar-make-toolbar-items 59,1563 +(defvar proof-toolbar-map 85,2424 +(defun proof-toolbar-available-p 88,2523 +(defun proof-toolbar-setup 98,2829 +(defun proof-toolbar-enable 119,3686 +(defalias 'proof-toolbar-undo proof-toolbar-undo152,4744 +(defun proof-toolbar-undo-enable-p 154,4812 +(defalias 'proof-toolbar-delete proof-toolbar-delete161,4970 +(defun proof-toolbar-delete-enable-p 163,5051 +(defalias 'proof-toolbar-home proof-toolbar-home171,5233 +(defalias 'proof-toolbar-next proof-toolbar-next175,5300 +(defun proof-toolbar-next-enable-p 177,5371 +(defalias 'proof-toolbar-goto proof-toolbar-goto183,5487 +(defun proof-toolbar-goto-enable-p 185,5537 +(defalias 'proof-toolbar-retract proof-toolbar-retract190,5622 +(defun proof-toolbar-retract-enable-p 192,5679 +(defalias 'proof-toolbar-use proof-toolbar-use198,5798 +(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p199,5850 +(defalias 'proof-toolbar-prooftree proof-toolbar-prooftree203,5933 +(defalias 'proof-toolbar-restart proof-toolbar-restart207,6018 +(defalias 'proof-toolbar-goal proof-toolbar-goal211,6083 +(defalias 'proof-toolbar-qed proof-toolbar-qed215,6141 +(defun proof-toolbar-qed-enable-p 217,6190 +(defalias 'proof-toolbar-state proof-toolbar-state225,6352 +(defalias 'proof-toolbar-state-enable-p proof-toolbar-state-enable-p226,6395 +(defalias 'proof-toolbar-context proof-toolbar-context230,6474 +(defalias 'proof-toolbar-context-enable-p proof-toolbar-context-enable-p231,6520 +(defalias 'proof-toolbar-command proof-toolbar-command235,6601 +(defalias 'proof-toolbar-command-enable-p proof-toolbar-command-enable-p236,6657 +(defun proof-toolbar-help 240,6762 +(defalias 'proof-toolbar-find proof-toolbar-find246,6842 +(defalias 'proof-toolbar-find-enable-p proof-toolbar-find-enable-p247,6894 +(defalias 'proof-toolbar-info proof-toolbar-info251,6969 +(defalias 'proof-toolbar-info-enable-p proof-toolbar-info-enable-p252,7024 +(defalias 'proof-toolbar-visibility proof-toolbar-visibility256,7122 +(defun proof-toolbar-visibility-enable-p 258,7182 +(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt263,7296 +(defun proof-toolbar-interrupt-enable-p 264,7357 +(defun proof-toolbar-scripting-menu 272,7510 + +generic/proof-tree.el,3278 +(defgroup proof-tree 90,3806 +(defcustom proof-tree-program 95,3947 +(defcustom proof-tree-arguments 100,4093 +(defgroup proof-tree-internals 110,4253 +(defcustom proof-tree-ignored-commands-regexp 118,4522 +(defcustom proof-tree-navigation-command-regexp 127,4921 +(defcustom proof-tree-cheating-regexp 135,5240 +(defcustom proof-tree-current-goal-regexp 144,5637 +(defcustom proof-tree-update-goal-regexp 154,6039 +(defcustom proof-tree-additional-subgoal-ID-regexp 166,6608 +(defcustom proof-tree-existential-regexp 174,6927 +(defcustom proof-tree-existentials-state-start-regexp 188,7547 +(defcustom proof-tree-existentials-state-end-regexp 199,8098 +(defcustom proof-tree-proof-completed-regexp 211,8741 +(defcustom proof-tree-get-proof-info 216,8890 +(defcustom proof-tree-extract-instantiated-existentials 240,9931 +(defcustom proof-tree-show-sequent-command 257,10649 +(defcustom proof-tree-find-begin-of-unfinished-proof 271,11271 +(defcustom proof-tree-urgent-action-hook 282,11833 +(defvar proof-tree-external-display 306,12688 +(defvar proof-tree-process 317,13193 +(defconst proof-tree-process-name 320,13282 +(defconst proof-tree-process-buffer323,13381 +(defconst proof-tree-emacs-exec-regexp327,13521 +(defvar proof-tree-last-state 331,13688 +(defvar proof-tree-current-proof 335,13792 +(defvar proof-tree-sequent-hash 340,13973 +(defvar proof-tree-existentials-alist 355,14680 +(defvar proof-tree-existentials-alist-history 366,15179 +(defun proof-tree-stop-external-display 375,15398 +(defun proof-tree-insert-output 383,15662 +(defun proof-tree-process-filter 394,16045 +(defun proof-tree-process-sentinel 420,16743 +(defun proof-tree-start-process 428,17069 +(defun proof-tree-is-running 457,18252 +(defun proof-tree-ensure-running 462,18413 +(defconst proof-tree-protocol-version 472,18617 +(defun proof-tree-send-message 477,18817 +(defun proof-tree-send-configure 491,19303 +(defun proof-tree-send-goal-state 499,19520 +(defun proof-tree-send-update-sequent 525,20569 +(defun proof-tree-send-switch-goal 538,21006 +(defun proof-tree-send-proof-completed 547,21332 +(defun proof-tree-send-undo 561,21773 +(defun proof-tree-send-quit-proof 566,21955 +(defun proof-tree-record-existentials-state 577,22290 +(defun proof-tree-undo-state-var 590,22840 +(defun proof-tree-undo-existentials 609,23621 +(defun proof-tree-delete-existential-assoc 617,23936 +(defun proof-tree-add-existential-assoc 623,24199 +(defun proof-tree-reset-existentials 636,24814 +(defun proof-tree-show-goal-callback 646,25090 +(defun proof-tree-make-show-goal-callback 667,26077 +(defun proof-tree-urgent-action 671,26238 +(defun proof-tree-quit-proof 736,28774 +(defun proof-tree-register-existentials 746,29210 +(defun proof-tree-extract-goals 759,29754 +(defun proof-tree-extract-list 781,30699 +(defun proof-tree-extract-existential-info 804,31669 +(defun proof-tree-handle-proof-progress 824,32540 +(defun proof-tree-handle-navigation 874,34611 +(defun proof-tree-handle-proof-command 892,35337 +(defun proof-tree-handle-undo 907,35999 +(defun proof-tree-update-sequent 939,37298 +(defun proof-tree-handle-delayed-output 980,39066 +(defun proof-tree-leave-buffer 1031,41089 +(defun proof-tree-display-current-proof 1043,41372 +(defun proof-tree-external-display-toggle 1075,42713 generic/proof-unicode-tokens.el,497 -(defvar proof-unicode-tokens-initialised 31,827 -(defun proof-unicode-tokens-init 34,934 -(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 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 +(defvar proof-unicode-tokens-initialised 31,767 +(defun proof-unicode-tokens-init 34,874 +(defun proof-unicode-tokens-configure 48,1376 +(defun proof-unicode-tokens-mode-if-enabled 60,1822 +(defun proof-unicode-tokens-set-global 66,2021 +(defun proof-unicode-tokens-enable 82,2591 +(defun proof-unicode-tokens-reconfigure 102,3444 +(defun proof-unicode-tokens-configure-prover 128,4332 +(defun proof-unicode-tokens-activate-prover 133,4513 +(defun proof-unicode-tokens-deactivate-prover 140,4759 generic/proof-useropts.el,1619 -(defgroup proof-user-options 21,564 -(defun proof-set-value 29,743 -(defcustom proof-electric-terminator-enable 62,1866 -(defcustom proof-toolbar-enable 74,2398 -(defcustom proof-imenu-enable 80,2571 -(defcustom pg-show-hints 86,2742 -(defcustom proof-shell-quiet-errors 91,2875 -(defcustom proof-trace-output-slow-catchup 98,3146 -(defcustom proof-strict-state-preserving 108,3643 -(defcustom proof-strict-read-only 121,4252 -(defcustom proof-three-window-enable 134,4831 -(defcustom proof-multiple-frames-enable 153,5581 -(defcustom proof-delete-empty-windows 162,5914 -(defcustom proof-shrink-windows-tofit 173,6445 -(defcustom proof-auto-raise-buffers 180,6717 -(defcustom proof-colour-locked 187,6952 -(defcustom proof-sticky-errors 195,7202 -(defcustom proof-query-file-save-when-activating-scripting202,7419 -(defcustom proof-prog-name-ask218,8139 -(defcustom proof-prog-name-guess224,8299 -(defcustom proof-tidy-response232,8564 -(defcustom proof-keep-response-history246,9027 -(defcustom pg-input-ring-size 256,9415 -(defcustom proof-general-debug 261,9567 -(defcustom proof-use-parser-cache 270,9938 -(defcustom proof-follow-mode 277,10192 -(defcustom proof-auto-action-when-deactivating-scripting 301,11369 -(defcustom proof-rsh-command 329,12551 -(defcustom proof-disappearing-proofs 345,13109 -(defcustom proof-full-annotation 350,13270 -(defcustom proof-output-tooltips 360,13733 -(defcustom proof-minibuffer-messages 371,14240 -(defcustom proof-autosend-enable 379,14549 -(defcustom proof-autosend-delay 385,14729 -(defcustom proof-autosend-all 391,14887 -(defcustom proof-fast-process-buffer 396,15056 +(defgroup proof-user-options 21,510 +(defun proof-set-value 29,689 +(defcustom proof-electric-terminator-enable 62,1812 +(defcustom proof-toolbar-enable 74,2344 +(defcustom proof-imenu-enable 80,2517 +(defcustom pg-show-hints 86,2688 +(defcustom proof-shell-quiet-errors 91,2821 +(defcustom proof-trace-output-slow-catchup 98,3092 +(defcustom proof-strict-state-preserving 108,3589 +(defcustom proof-strict-read-only 121,4198 +(defcustom proof-three-window-enable 134,4777 +(defcustom proof-multiple-frames-enable 153,5527 +(defcustom proof-delete-empty-windows 162,5860 +(defcustom proof-shrink-windows-tofit 173,6391 +(defcustom proof-auto-raise-buffers 180,6663 +(defcustom proof-colour-locked 187,6898 +(defcustom proof-sticky-errors 195,7148 +(defcustom proof-query-file-save-when-activating-scripting202,7365 +(defcustom proof-prog-name-ask218,8085 +(defcustom proof-prog-name-guess224,8245 +(defcustom proof-tidy-response232,8510 +(defcustom proof-keep-response-history246,8973 +(defcustom pg-input-ring-size 256,9361 +(defcustom proof-general-debug 261,9513 +(defcustom proof-use-parser-cache 270,9884 +(defcustom proof-follow-mode 277,10138 +(defcustom proof-auto-action-when-deactivating-scripting 301,11315 +(defcustom proof-rsh-command 329,12497 +(defcustom proof-disappearing-proofs 345,13055 +(defcustom proof-full-annotation 350,13216 +(defcustom proof-output-tooltips 360,13679 +(defcustom proof-minibuffer-messages 371,14186 +(defcustom proof-autosend-enable 379,14495 +(defcustom proof-autosend-delay 385,14675 +(defcustom proof-autosend-all 391,14833 +(defcustom proof-fast-process-buffer 396,15002 generic/proof-utils.el,1645 -(defmacro proof-with-current-buffer-if-exists 61,1735 -(defmacro proof-with-script-buffer 70,2112 -(defmacro proof-map-buffers 81,2493 -(defmacro proof-sym 86,2678 -(defsubst proof-try-require 91,2839 -(defun proof-save-some-buffers 104,3170 -(defun proof-save-this-buffer 124,3766 -(defun proof-file-truename 137,4130 -(defun proof-files-to-buffers 141,4312 -(defun proof-buffers-in-mode 149,4551 -(defun pg-save-from-death 163,5001 -(defun proof-define-keys 182,5617 -(defun pg-remove-specials 193,5902 -(defun pg-remove-specials-in-string 203,6238 -(defun proof-safe-split-window-vertically 213,6463 -(defun proof-warn-if-unset 218,6643 -(defun proof-get-window-for-buffer 223,6861 -(defun proof-display-and-keep-buffer 272,9171 -(defun proof-clean-buffer 314,10894 -(defun pg-internal-warning 330,11550 -(defun proof-debug 338,11832 -(defun proof-switch-to-buffer 353,12383 -(defun proof-resize-window-tofit 375,13507 -(defun proof-submit-bug-report 470,17355 -(defun proof-deftoggle-fn 505,18712 -(defmacro proof-deftoggle 520,19378 -(defun proof-defintset-fn 531,19891 -(defmacro proof-defintset 550,20715 -(defun proof-deffloatset-fn 557,21094 -(defmacro proof-deffloatset 573,21808 -(defun proof-defstringset-fn 580,22193 -(defmacro proof-defstringset 593,22819 -(defun proof-escape-keymap-doc 606,23275 -(defmacro proof-defshortcut 610,23429 -(defmacro proof-definvisible 625,24027 -(defun pg-custom-save-vars 652,24956 -(defun pg-custom-reset-vars 668,25600 -(defun proof-locate-executable 681,25937 -(defun pg-current-word-pos 696,26487 -(defsubst proof-shell-strip-output-markup 741,28142 -(defun proof-minibuffer-message 747,28406 +(defmacro proof-with-current-buffer-if-exists 61,1684 +(defmacro proof-with-script-buffer 70,2061 +(defmacro proof-map-buffers 81,2442 +(defmacro proof-sym 86,2627 +(defsubst proof-try-require 91,2788 +(defun proof-save-some-buffers 104,3119 +(defun proof-save-this-buffer 124,3715 +(defun proof-file-truename 137,4079 +(defun proof-files-to-buffers 141,4261 +(defun proof-buffers-in-mode 149,4500 +(defun pg-save-from-death 163,4950 +(defun proof-define-keys 182,5566 +(defun pg-remove-specials 193,5851 +(defun pg-remove-specials-in-string 203,6187 +(defun proof-safe-split-window-vertically 213,6412 +(defun proof-warn-if-unset 218,6592 +(defun proof-get-window-for-buffer 223,6810 +(defun proof-display-and-keep-buffer 272,9120 +(defun proof-clean-buffer 314,10843 +(defun pg-internal-warning 330,11499 +(defun proof-debug 338,11781 +(defun proof-switch-to-buffer 353,12332 +(defun proof-resize-window-tofit 375,13456 +(defun proof-submit-bug-report 470,17304 +(defun proof-deftoggle-fn 505,18661 +(defmacro proof-deftoggle 520,19327 +(defun proof-defintset-fn 531,19840 +(defmacro proof-defintset 550,20664 +(defun proof-deffloatset-fn 557,21043 +(defmacro proof-deffloatset 573,21757 +(defun proof-defstringset-fn 580,22142 +(defmacro proof-defstringset 593,22768 +(defun proof-escape-keymap-doc 606,23224 +(defmacro proof-defshortcut 610,23378 +(defmacro proof-definvisible 625,23976 +(defun pg-custom-save-vars 652,24905 +(defun pg-custom-reset-vars 668,25549 +(defun proof-locate-executable 681,25886 +(defun pg-current-word-pos 696,26436 +(defsubst proof-shell-strip-output-markup 741,28091 +(defun proof-minibuffer-message 747,28355 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 +(defun bufhist-ring-update 38,1344 +(defgroup bufhist 47,1666 +(defcustom bufhist-ring-size 51,1747 +(defvar bufhist-ring 56,1858 +(defvar bufhist-ring-pos 59,1932 +(defvar bufhist-lastswitch-modified-tick 62,2011 +(defvar bufhist-read-only-history 65,2117 +(defvar bufhist-saved-mode-line-format 68,2188 +(defvar bufhist-normal-read-only 71,2291 +(defvar bufhist-top-point 74,2385 +(defun bufhist-mode-line-format-entry 77,2475 +(defconst bufhist-minor-mode-map106,3549 +(define-minor-mode bufhist-mode119,4026 +(defun bufhist-get-buffer-contents 141,4907 +(defun bufhist-restore-buffer-contents 150,5249 +(defun bufhist-checkpoint 159,5563 +(defun bufhist-erase-buffer 167,5932 +(defun bufhist-checkpoint-and-erase 178,6303 +(defun bufhist-switch-to-index 184,6489 +(defun bufhist-first 223,8088 +(defun bufhist-last 228,8247 +(defun bufhist-prev 233,8391 +(defun bufhist-next 241,8614 +(defun bufhist-delete 246,8754 +(defun bufhist-clear 258,9295 +(defun bufhist-init 273,9690 +(defun bufhist-exit 301,10699 +(defun bufhist-set-readwrite 311,10963 +(defun bufhist-before-change-function 326,11583 +(define-button-type 'bufhist-nextbufhist-next340,12006 +(define-button-type 'bufhist-prevbufhist-prev344,12103 +(defun bufhist-insert-buttons 351,12315 lib/holes.el,2465 -(defvar holes-default-hole 44,1121 -(defvar holes-active-hole 50,1299 -(defgroup holes 60,1496 -(defcustom holes-empty-hole-string 65,1595 -(defcustom holes-empty-hole-regexp 70,1738 -(defface active-hole-face92,2440 -(defface inactive-hole-face102,2856 -(defvar hole-map116,3297 -(defvar holes-mode-map126,3688 -(defun holes-region-beginning-or-nil 172,5425 -(defun holes-region-end-or-nil 176,5561 -(defun holes-copy-active-region 180,5679 -(defun holes-is-hole-p 186,5889 -(defun holes-hole-start-position 190,5981 -(defun holes-hole-end-position 196,6164 -(defun holes-hole-buffer 201,6335 -(defun holes-hole-at 207,6509 -(defun holes-active-hole-exist-p 212,6679 -(defun holes-active-hole-start-position 219,6932 -(defun holes-active-hole-end-position 227,7300 -(defun holes-active-hole-buffer 236,7663 -(defun holes-goto-active-hole 244,7964 -(defun holes-highlight-hole-as-active 253,8223 -(defun holes-highlight-hole 261,8531 -(defun holes-disable-active-hole 269,8818 -(defun holes-set-active-hole 282,9350 -(defun holes-is-in-hole-p 292,9695 -(defun holes-make-hole 296,9833 -(defun holes-make-hole-at 314,10489 -(defun holes-clear-hole 328,10942 -(defun holes-clear-hole-at 337,11200 -(defun holes-map-holes 345,11456 -(defun holes-clear-all-buffer-holes 349,11610 -(defun holes-next 359,11911 -(defun holes-next-after-active-hole 366,12163 -(defun holes-set-active-hole-next 373,12379 -(defun holes-replace-segment 392,12916 -(defun holes-replace 401,13269 -(defun holes-replace-active-hole 429,14447 -(defun holes-replace-update-active-hole 436,14738 -(defun holes-delete-update-active-hole 454,15385 -(defun holes-set-make-active-hole 462,15612 -(defalias 'holes-track-mouse-selection holes-track-mouse-selection477,16167 -(defsubst holes-track-mouse-clicks 478,16225 -(defun holes-mouse-replace-active-hole 482,16335 -(defun holes-destroy-hole 496,16806 -(defsubst holes-hole-at-event 510,17188 -(defun holes-mouse-destroy-hole 514,17288 -(defun holes-mouse-forget-hole 521,17509 -(defun holes-mouse-set-make-active-hole 531,17801 -(defun holes-mouse-set-active-hole 547,18300 -(defun holes-set-point-next-hole-destroy 556,18551 -(defun holes-replace-string-by-holes-backward 582,19532 -(defun holes-skeleton-end-hook 600,20232 -(defconst holes-jump-doc609,20670 -(defun holes-replace-string-by-holes-backward-jump 616,20876 -(define-minor-mode holes-mode 633,21558 -(defun holes-abbrev-complete 728,25040 -(defun holes-insert-and-expand 738,25383 +(defvar holes-default-hole 44,1076 +(defvar holes-active-hole 50,1254 +(defgroup holes 60,1451 +(defcustom holes-empty-hole-string 65,1550 +(defcustom holes-empty-hole-regexp 70,1693 +(defface active-hole-face92,2395 +(defface inactive-hole-face102,2811 +(defvar hole-map116,3252 +(defvar holes-mode-map126,3643 +(defun holes-region-beginning-or-nil 172,5380 +(defun holes-region-end-or-nil 176,5516 +(defun holes-copy-active-region 180,5634 +(defun holes-is-hole-p 186,5844 +(defun holes-hole-start-position 190,5936 +(defun holes-hole-end-position 196,6119 +(defun holes-hole-buffer 201,6290 +(defun holes-hole-at 207,6464 +(defun holes-active-hole-exist-p 212,6634 +(defun holes-active-hole-start-position 219,6887 +(defun holes-active-hole-end-position 227,7255 +(defun holes-active-hole-buffer 236,7618 +(defun holes-goto-active-hole 244,7919 +(defun holes-highlight-hole-as-active 253,8178 +(defun holes-highlight-hole 261,8486 +(defun holes-disable-active-hole 269,8773 +(defun holes-set-active-hole 282,9305 +(defun holes-is-in-hole-p 292,9650 +(defun holes-make-hole 296,9788 +(defun holes-make-hole-at 314,10444 +(defun holes-clear-hole 328,10897 +(defun holes-clear-hole-at 337,11155 +(defun holes-map-holes 345,11411 +(defun holes-clear-all-buffer-holes 349,11565 +(defun holes-next 359,11866 +(defun holes-next-after-active-hole 366,12118 +(defun holes-set-active-hole-next 373,12334 +(defun holes-replace-segment 392,12871 +(defun holes-replace 401,13224 +(defun holes-replace-active-hole 429,14402 +(defun holes-replace-update-active-hole 436,14693 +(defun holes-delete-update-active-hole 454,15340 +(defun holes-set-make-active-hole 462,15567 +(defalias 'holes-track-mouse-selection holes-track-mouse-selection477,16122 +(defsubst holes-track-mouse-clicks 478,16180 +(defun holes-mouse-replace-active-hole 482,16290 +(defun holes-destroy-hole 496,16761 +(defsubst holes-hole-at-event 510,17143 +(defun holes-mouse-destroy-hole 514,17243 +(defun holes-mouse-forget-hole 521,17464 +(defun holes-mouse-set-make-active-hole 531,17756 +(defun holes-mouse-set-active-hole 547,18255 +(defun holes-set-point-next-hole-destroy 556,18506 +(defun holes-replace-string-by-holes-backward 582,19487 +(defun holes-skeleton-end-hook 600,20187 +(defconst holes-jump-doc609,20625 +(defun holes-replace-string-by-holes-backward-jump 616,20831 +(define-minor-mode holes-mode 633,21513 +(defun holes-abbrev-complete 728,24995 +(defun holes-insert-and-expand 738,25338 lib/local-vars-list.el,373 -(defconst local-vars-list-doc 28,825 -(defun local-vars-list-insert-empty-zone 44,1387 -(defun local-vars-list-find 82,2090 -(defun local-vars-list-goto-var 101,2861 -(defun local-vars-list-get-current 127,3908 -(defun local-vars-list-set-current 148,4758 -(defun local-vars-list-get 171,5473 -(defun local-vars-list-get-safe 188,6003 -(defun local-vars-list-set 193,6197 +(defconst local-vars-list-doc 28,770 +(defun local-vars-list-insert-empty-zone 44,1332 +(defun local-vars-list-find 82,2035 +(defun local-vars-list-goto-var 101,2806 +(defun local-vars-list-get-current 127,3853 +(defun local-vars-list-set-current 148,4703 +(defun local-vars-list-get 171,5418 +(defun local-vars-list-get-safe 188,5948 +(defun local-vars-list-set 193,6142 lib/maths-menu.el,242 -(defvar maths-menu-filter-predicate 56,2317 -(defvar maths-menu-tokenise-insert 59,2426 -(defun maths-menu-build-menu 62,2563 -(defvar maths-menu-menu84,3324 -(defvar maths-menu-mode-map344,12882 -(define-minor-mode maths-menu-mode352,13101 +(defvar maths-menu-filter-predicate 56,2267 +(defvar maths-menu-tokenise-insert 59,2376 +(defun maths-menu-build-menu 62,2513 +(defvar maths-menu-menu84,3274 +(defvar maths-menu-mode-map344,12832 +(define-minor-mode maths-menu-mode352,13051 lib/pg-dev.el,199 -(defconst pg-dev-lisp-font-lock-keywords52,1580 -(defun pg-loadpath 78,2279 -(defun unload-pg 88,2450 -(defun profile-pg 119,3344 -(defun elp-pack-number 149,4451 -(defun pg-bug-references 158,4651 +(defconst pg-dev-lisp-font-lock-keywords52,1534 +(defun pg-loadpath 78,2233 +(defun unload-pg 88,2404 +(defun profile-pg 119,3298 +(defun elp-pack-number 149,4405 +(defun pg-bug-references 158,4605 lib/pg-fontsets.el,209 -(defcustom pg-fontsets-default-fontset 24,722 -(defvar pg-fontsets-names 29,868 -(defun pg-fontsets-make-fontsetsizes 32,949 -(defconst pg-fontsets-base-fonts51,1710 -(defun pg-fontsets-make-fontsets 57,1840 +(defcustom pg-fontsets-default-fontset 24,671 +(defvar pg-fontsets-names 29,817 +(defun pg-fontsets-make-fontsetsizes 32,898 +(defconst pg-fontsets-base-fonts51,1659 +(defun pg-fontsets-make-fontsets 57,1789 lib/proof-compat.el,160 -(defvar proof-running-on-win32 32,975 -(defun pg-custom-undeclare-variable 53,1777 -(defmacro save-selected-frame 86,2602 -(defmacro declare-function 152,4610 - -lib/scomint.el,788 -(defvar scomint-buffer-maximum-size 19,493 -(defvar scomint-output-filter-functions 24,684 -(defvar scomint-mode-map27,794 -(defvar scomint-last-input-start 33,973 -(defvar scomint-last-input-end 34,1011 -(defvar scomint-last-output-start 35,1047 -(defvar scomint-exec-hook 37,1087 -(define-derived-mode scomint-mode 46,1430 -(defsubst scomint-check-proc 65,2345 -(defun scomint-make-in-buffer 73,2685 -(defun scomint-make 97,3952 -(defun scomint-exec 110,4663 -(defun scomint-exec-1 147,6256 -(defalias 'scomint-send-string scomint-send-string197,8386 -(defun scomint-send-eof 199,8440 -(defun scomint-send-input 208,8673 -(defun scomint-truncate-buffer 234,9569 -(defun scomint-strip-ctrl-m 247,9963 -(defun scomint-output-filter 261,10526 -(defun scomint-interrupt-process 284,11281 +(defvar proof-running-on-win32 32,923 +(defun pg-custom-undeclare-variable 53,1725 +(defmacro save-selected-frame 86,2550 +(defmacro declare-function 152,4558 + +lib/scomint.el,787 +(defvar scomint-buffer-maximum-size 19,446 +(defvar scomint-output-filter-functions 24,637 +(defvar scomint-mode-map27,747 +(defvar scomint-last-input-start 33,926 +(defvar scomint-last-input-end 34,964 +(defvar scomint-last-output-start 35,1000 +(defvar scomint-exec-hook 37,1040 +(define-derived-mode scomint-mode 46,1383 +(defsubst scomint-check-proc 65,2298 +(defun scomint-make-in-buffer 73,2638 +(defun scomint-make 97,3905 +(defun scomint-exec 110,4616 +(defun scomint-exec-1 147,6209 +(defalias 'scomint-send-string scomint-send-string197,8339 +(defun scomint-send-eof 199,8393 +(defun scomint-send-input 208,8626 +(defun scomint-truncate-buffer 234,9522 +(defun scomint-strip-ctrl-m 247,9916 +(defun scomint-output-filter 261,10493 +(defun scomint-interrupt-process 284,11248 lib/span.el,1553 -(defalias 'span-start span-start22,609 -(defalias 'span-end span-end23,647 -(defalias 'span-set-property span-set-property24,681 -(defalias 'span-property span-property25,724 -(defalias 'span-make span-make26,763 -(defalias 'span-detach span-detach27,799 -(defalias 'span-set-endpoints span-set-endpoints28,839 -(defalias 'span-buffer span-buffer29,884 -(defun span-read-only-hook 31,925 -(defsubst span-read-only 36,1115 -(defsubst span-read-write 43,1425 -(defsubst span-write-warning 48,1595 -(defsubst span-lt 59,2119 -(defsubst spans-at-point-prop 64,2263 -(defsubst spans-at-region-prop 73,2454 -(defsubst span-at 83,2720 -(defsubst span-delete 87,2846 -(defsubst span-add-delete-action 93,3042 -(defsubst span-mapcar-spans 99,3321 -(defsubst span-mapc-spans 103,3496 -(defsubst span-mapcar-spans-inorder 107,3667 -(defun span-at-before 113,3872 -(defsubst prev-span 130,4596 -(defsubst next-span 136,4749 -(defsubst span-live-p 142,4963 -(defsubst span-raise 148,5129 -(defsubst span-string 152,5262 -(defsubst set-span-properties 157,5422 -(defsubst span-find-span 163,5616 -(defsubst span-at-event 171,5928 -(defun fold-spans 177,6125 -(defsubst span-detached-p 191,6658 -(defsubst set-span-face 195,6774 -(defsubst set-span-keymap 199,6872 -(defsubst span-delete-spans 207,7041 -(defsubst span-property-safe 211,7203 -(defsubst span-set-start 215,7340 -(defsubst span-set-end 219,7472 -(defun span-make-self-removing-span 227,7632 -(defun span-delete-self-modification-hook 237,8000 -(defun span-make-modifying-removing-span 242,8174 +(defalias 'span-start span-start22,565 +(defalias 'span-end span-end23,603 +(defalias 'span-set-property span-set-property24,637 +(defalias 'span-property span-property25,680 +(defalias 'span-make span-make26,719 +(defalias 'span-detach span-detach27,755 +(defalias 'span-set-endpoints span-set-endpoints28,795 +(defalias 'span-buffer span-buffer29,840 +(defun span-read-only-hook 31,881 +(defsubst span-read-only 36,1071 +(defsubst span-read-write 43,1381 +(defsubst span-write-warning 48,1551 +(defsubst span-lt 59,2075 +(defsubst spans-at-point-prop 64,2219 +(defsubst spans-at-region-prop 73,2410 +(defsubst span-at 83,2676 +(defsubst span-delete 87,2802 +(defsubst span-add-delete-action 93,2998 +(defsubst span-mapcar-spans 99,3277 +(defsubst span-mapc-spans 103,3452 +(defsubst span-mapcar-spans-inorder 107,3623 +(defun span-at-before 113,3828 +(defsubst prev-span 130,4552 +(defsubst next-span 136,4705 +(defsubst span-live-p 142,4919 +(defsubst span-raise 148,5085 +(defsubst span-string 152,5218 +(defsubst set-span-properties 157,5378 +(defsubst span-find-span 163,5572 +(defsubst span-at-event 171,5884 +(defun fold-spans 177,6081 +(defsubst span-detached-p 191,6614 +(defsubst set-span-face 195,6730 +(defsubst set-span-keymap 199,6828 +(defsubst span-delete-spans 207,6997 +(defsubst span-property-safe 211,7159 +(defsubst span-set-start 215,7296 +(defsubst span-set-end 219,7428 +(defun span-make-self-removing-span 227,7588 +(defun span-delete-self-modification-hook 237,7956 +(defun span-make-modifying-removing-span 242,8130 lib/texi-docstring-magic.el,584 -(defun texi-docstring-magic-find-face 88,3027 -(defun texi-docstring-magic-splice-sep 93,3192 -(defconst texi-docstring-magic-munge-table103,3497 -(defun texi-docstring-magic-untabify 193,7260 -(defun texi-docstring-magic-munge-docstring 200,7458 -(defun texi-docstring-magic-texi 239,8739 -(defun texi-docstring-magic-format-default 252,9179 -(defun texi-docstring-magic-texi-for 268,9812 -(defconst texi-docstring-magic-comment326,11771 -(defun texi-docstring-magic 332,11925 -(defun texi-docstring-magic-face-at-point 366,13004 -(defun texi-docstring-magic-insert-magic 381,13527 +(defun texi-docstring-magic-find-face 88,2967 +(defun texi-docstring-magic-splice-sep 93,3132 +(defconst texi-docstring-magic-munge-table103,3437 +(defun texi-docstring-magic-untabify 193,7200 +(defun texi-docstring-magic-munge-docstring 200,7398 +(defun texi-docstring-magic-texi 239,8679 +(defun texi-docstring-magic-format-default 252,9119 +(defun texi-docstring-magic-texi-for 268,9752 +(defconst texi-docstring-magic-comment326,11711 +(defun texi-docstring-magic 332,11865 +(defun texi-docstring-magic-face-at-point 366,12944 +(defun texi-docstring-magic-insert-magic 381,13467 lib/unicode-chars.el,80 -(defvar unicode-chars-alist12,348 -(defun unicode-chars-list-chars 5051,245975 - -lib/unicode-tokens.el,5901 -(defgroup unicode-tokens-options 55,1711 -(defcustom unicode-tokens-add-help-echo 60,1836 -(defun unicode-tokens-toggle-add-help-echo 65,2003 -(defvar unicode-tokens-token-symbol-map 79,2409 -(defvar unicode-tokens-token-format 98,3068 -(defvar unicode-tokens-token-variant-format-regexp 104,3317 -(defvar unicode-tokens-shortcut-alist 118,3850 -(defvar unicode-tokens-shortcut-replacement-alist 124,4127 -(defvar unicode-tokens-control-region-format-regexp 132,4333 -(defvar unicode-tokens-control-char-format-regexp 139,4701 -(defvar unicode-tokens-control-regions 146,5062 -(defvar unicode-tokens-control-characters 149,5138 -(defvar unicode-tokens-control-char-format 152,5220 -(defvar unicode-tokens-control-region-format-start 155,5333 -(defvar unicode-tokens-control-region-format-end 158,5450 -(defvar unicode-tokens-tokens-customizable-variables 161,5563 -(defconst unicode-tokens-configuration-variables168,5731 -(defun unicode-tokens-config 183,6130 -(defun unicode-tokens-config-var 187,6275 -(defun unicode-tokens-copy-configuration-variables 199,6715 -(defvar unicode-tokens-token-list 227,7931 -(defvar unicode-tokens-hash-table 230,8051 -(defvar unicode-tokens-token-match-regexp 233,8167 -(defvar unicode-tokens-uchar-hash-table 239,8450 -(defvar unicode-tokens-uchar-regexp 243,8637 -(defgroup unicode-tokens-faces 251,8822 -(defconst unicode-tokens-font-family-alternatives261,9124 -(defface unicode-tokens-symbol-font-face276,9642 -(defface unicode-tokens-script-font-face286,10000 -(defface unicode-tokens-fraktur-font-face291,10144 -(defface unicode-tokens-serif-font-face296,10269 -(defface unicode-tokens-sans-font-face301,10406 -(defface unicode-tokens-highlight-face306,10528 -(defconst unicode-tokens-fonts315,10890 -(defconst unicode-tokens-fontsymb-properties324,11107 -(define-widget 'unicode-tokens-token-symbol-map unicode-tokens-token-symbol-map352,12728 -(define-widget 'unicode-tokens-shortcut-alist unicode-tokens-shortcut-alist370,13280 -(defconst unicode-tokens-font-lock-extra-managed-props383,13611 -(defun unicode-tokens-font-lock-keywords 387,13765 -(defun unicode-tokens-calculate-token-match 420,15136 -(defun unicode-tokens-usable-composition 450,16172 -(defun unicode-tokens-help-echo 463,16551 -(defvar unicode-tokens-show-symbols 468,16753 -(defun unicode-tokens-interpret-composition 471,16867 -(defun unicode-tokens-font-lock-compose-symbol 489,17379 -(defun unicode-tokens-prepend-text-properties-in-match 527,18911 -(defun unicode-tokens-prepend-text-property 541,19489 -(defun unicode-tokens-show-symbols 566,20634 -(defun unicode-tokens-symbs-to-props 574,20944 -(defvar unicode-tokens-show-controls 594,21643 -(defun unicode-tokens-show-controls 597,21734 -(defun unicode-tokens-control-char 609,22247 -(defun unicode-tokens-control-region 618,22686 -(defun unicode-tokens-control-font-lock-keywords 629,23233 -(defvar unicode-tokens-use-shortcuts 640,23557 -(defun unicode-tokens-use-shortcuts 643,23660 -(defun unicode-tokens-map-ordering 659,24256 -(defun unicode-tokens-quail-define-rules 668,24609 -(defun unicode-tokens-insert-token 691,25286 -(defun unicode-tokens-annotate-region 700,25590 -(defun unicode-tokens-insert-control 724,26428 -(defun unicode-tokens-insert-uchar-as-token 734,26877 -(defun unicode-tokens-delete-token-near-point 740,27098 -(defun unicode-tokens-delete-backward-char 752,27539 -(defun unicode-tokens-delete-char 763,27920 -(defun unicode-tokens-delete-backward-1 774,28274 -(defun unicode-tokens-delete-1 791,28870 -(defun unicode-tokens-prev-token 807,29414 -(defun unicode-tokens-rotate-token-forward 815,29711 -(defun unicode-tokens-rotate-token-backward 842,30601 -(defun unicode-tokens-replace-shortcut-match 847,30803 -(defun unicode-tokens-replace-shortcuts 856,31173 -(defun unicode-tokens-replace-unicode-match 870,31771 -(defun unicode-tokens-replace-unicode 877,32072 -(defun unicode-tokens-copy-token 894,32671 -(define-button-type 'unicode-tokens-listunicode-tokens-list901,32892 -(defun unicode-tokens-list-tokens 907,33096 -(defun unicode-tokens-list-shortcuts 946,34280 -(defalias 'unicode-tokens-list-unicode-chars unicode-tokens-list-unicode-chars964,34918 -(defun unicode-tokens-encode-in-temp-buffer 966,34991 -(defun unicode-tokens-encode 984,35647 -(defun unicode-tokens-encode-str 990,35883 -(defun unicode-tokens-copy 994,36045 -(defun unicode-tokens-paste 1003,36451 -(defvar unicode-tokens-highlight-unicode 1022,37172 -(defconst unicode-tokens-unicode-highlight-patterns1025,37264 -(defun unicode-tokens-highlight-unicode 1029,37433 -(defun unicode-tokens-highlight-unicode-setkeywords 1041,37896 -(defun unicode-tokens-initialise 1053,38265 -(defvar unicode-tokens-mode-map 1073,38936 -(defvar unicode-tokens-display-table1076,39033 -(define-minor-mode unicode-tokens-mode1083,39284 -(defun unicode-tokens-set-font-var 1219,43859 -(defun unicode-tokens-set-font-var-aux 1235,44348 -(defun unicode-tokens-mouse-set-font 1266,45509 -(defsubst unicode-tokens-face-font-sym 1279,46023 -(defun unicode-tokens-set-font-restart 1283,46203 -(defun unicode-tokens-save-fonts 1294,46513 -(defun unicode-tokens-custom-save-faces 1302,46769 -(define-key unicode-tokens-mode-map1319,47225 -(define-key unicode-tokens-mode-map1322,47332 -(defvar unicode-tokens-quail-translation-keymap1330,47591 -(define-key unicode-tokens-quail-translation-keymap1337,47781 -(defun unicode-tokens-quail-delete-last-char 1341,47915 -(define-key unicode-tokens-mode-map 1356,48342 -(define-key unicode-tokens-mode-map 1358,48434 -(define-key unicode-tokens-mode-map1360,48525 -(define-key unicode-tokens-mode-map1362,48631 -(define-key unicode-tokens-mode-map1365,48746 -(define-key unicode-tokens-mode-map1367,48855 -(define-key unicode-tokens-mode-map1369,48963 -(define-key unicode-tokens-mode-map1371,49069 -(defun unicode-tokens-customize-submenu 1379,49193 -(defun unicode-tokens-define-menu 1386,49416 +(defvar unicode-chars-alist12,295 +(defun unicode-chars-list-chars 5051,245922 + +lib/unicode-tokens.el,5900 +(defgroup unicode-tokens-options 55,1657 +(defcustom unicode-tokens-add-help-echo 60,1782 +(defun unicode-tokens-toggle-add-help-echo 65,1949 +(defvar unicode-tokens-token-symbol-map 79,2355 +(defvar unicode-tokens-token-format 98,3014 +(defvar unicode-tokens-token-variant-format-regexp 104,3263 +(defvar unicode-tokens-shortcut-alist 118,3796 +(defvar unicode-tokens-shortcut-replacement-alist 124,4073 +(defvar unicode-tokens-control-region-format-regexp 132,4279 +(defvar unicode-tokens-control-char-format-regexp 139,4647 +(defvar unicode-tokens-control-regions 146,5008 +(defvar unicode-tokens-control-characters 149,5084 +(defvar unicode-tokens-control-char-format 152,5166 +(defvar unicode-tokens-control-region-format-start 155,5279 +(defvar unicode-tokens-control-region-format-end 158,5396 +(defvar unicode-tokens-tokens-customizable-variables 161,5509 +(defconst unicode-tokens-configuration-variables168,5677 +(defun unicode-tokens-config 183,6076 +(defun unicode-tokens-config-var 187,6221 +(defun unicode-tokens-copy-configuration-variables 199,6661 +(defvar unicode-tokens-token-list 227,7877 +(defvar unicode-tokens-hash-table 230,7997 +(defvar unicode-tokens-token-match-regexp 233,8113 +(defvar unicode-tokens-uchar-hash-table 239,8396 +(defvar unicode-tokens-uchar-regexp 243,8583 +(defgroup unicode-tokens-faces 251,8768 +(defconst unicode-tokens-font-family-alternatives261,9070 +(defface unicode-tokens-symbol-font-face276,9588 +(defface unicode-tokens-script-font-face286,9946 +(defface unicode-tokens-fraktur-font-face291,10090 +(defface unicode-tokens-serif-font-face296,10215 +(defface unicode-tokens-sans-font-face301,10352 +(defface unicode-tokens-highlight-face306,10474 +(defconst unicode-tokens-fonts315,10836 +(defconst unicode-tokens-fontsymb-properties324,11053 +(define-widget 'unicode-tokens-token-symbol-map unicode-tokens-token-symbol-map352,12674 +(define-widget 'unicode-tokens-shortcut-alist unicode-tokens-shortcut-alist370,13226 +(defconst unicode-tokens-font-lock-extra-managed-props383,13557 +(defun unicode-tokens-font-lock-keywords 387,13711 +(defun unicode-tokens-calculate-token-match 420,15082 +(defun unicode-tokens-usable-composition 450,16118 +(defun unicode-tokens-help-echo 463,16497 +(defvar unicode-tokens-show-symbols 468,16699 +(defun unicode-tokens-interpret-composition 471,16813 +(defun unicode-tokens-font-lock-compose-symbol 489,17325 +(defun unicode-tokens-prepend-text-properties-in-match 527,18857 +(defun unicode-tokens-prepend-text-property 541,19435 +(defun unicode-tokens-show-symbols 566,20580 +(defun unicode-tokens-symbs-to-props 574,20890 +(defvar unicode-tokens-show-controls 594,21589 +(defun unicode-tokens-show-controls 597,21680 +(defun unicode-tokens-control-char 609,22193 +(defun unicode-tokens-control-region 618,22632 +(defun unicode-tokens-control-font-lock-keywords 629,23179 +(defvar unicode-tokens-use-shortcuts 640,23503 +(defun unicode-tokens-use-shortcuts 643,23606 +(defun unicode-tokens-map-ordering 659,24202 +(defun unicode-tokens-quail-define-rules 668,24555 +(defun unicode-tokens-insert-token 691,25232 +(defun unicode-tokens-annotate-region 700,25536 +(defun unicode-tokens-insert-control 724,26374 +(defun unicode-tokens-insert-uchar-as-token 734,26823 +(defun unicode-tokens-delete-token-near-point 740,27044 +(defun unicode-tokens-delete-backward-char 752,27485 +(defun unicode-tokens-delete-char 763,27866 +(defun unicode-tokens-delete-backward-1 774,28220 +(defun unicode-tokens-delete-1 791,28816 +(defun unicode-tokens-prev-token 807,29360 +(defun unicode-tokens-rotate-token-forward 815,29657 +(defun unicode-tokens-rotate-token-backward 842,30547 +(defun unicode-tokens-replace-shortcut-match 847,30749 +(defun unicode-tokens-replace-shortcuts 856,31119 +(defun unicode-tokens-replace-unicode-match 870,31717 +(defun unicode-tokens-replace-unicode 877,32018 +(defun unicode-tokens-copy-token 894,32617 +(define-button-type 'unicode-tokens-listunicode-tokens-list901,32838 +(defun unicode-tokens-list-tokens 907,33042 +(defun unicode-tokens-list-shortcuts 946,34226 +(defalias 'unicode-tokens-list-unicode-chars unicode-tokens-list-unicode-chars964,34864 +(defun unicode-tokens-encode-in-temp-buffer 966,34937 +(defun unicode-tokens-encode 984,35593 +(defun unicode-tokens-encode-str 990,35829 +(defun unicode-tokens-copy 994,35991 +(defun unicode-tokens-paste 1003,36397 +(defvar unicode-tokens-highlight-unicode 1022,37118 +(defconst unicode-tokens-unicode-highlight-patterns1025,37210 +(defun unicode-tokens-highlight-unicode 1029,37379 +(defun unicode-tokens-highlight-unicode-setkeywords 1041,37842 +(defun unicode-tokens-initialise 1053,38211 +(defvar unicode-tokens-mode-map 1073,38882 +(defvar unicode-tokens-display-table1076,38979 +(define-minor-mode unicode-tokens-mode1083,39230 +(defun unicode-tokens-set-font-var 1219,43805 +(defun unicode-tokens-set-font-var-aux 1235,44294 +(defun unicode-tokens-mouse-set-font 1266,45455 +(defsubst unicode-tokens-face-font-sym 1279,45969 +(defun unicode-tokens-set-font-restart 1283,46149 +(defun unicode-tokens-save-fonts 1294,46459 +(defun unicode-tokens-custom-save-faces 1302,46715 +(define-key unicode-tokens-mode-map1319,47171 +(define-key unicode-tokens-mode-map1322,47278 +(defvar unicode-tokens-quail-translation-keymap1330,47537 +(define-key unicode-tokens-quail-translation-keymap1337,47727 +(defun unicode-tokens-quail-delete-last-char 1341,47861 +(define-key unicode-tokens-mode-map 1356,48288 +(define-key unicode-tokens-mode-map 1358,48380 +(define-key unicode-tokens-mode-map1360,48471 +(define-key unicode-tokens-mode-map1362,48577 +(define-key unicode-tokens-mode-map1365,48692 +(define-key unicode-tokens-mode-map1367,48801 +(define-key unicode-tokens-mode-map1369,48909 +(define-key unicode-tokens-mode-map1371,49015 +(defun unicode-tokens-customize-submenu 1379,49139 +(defun unicode-tokens-define-menu 1386,49362 contrib/mmm/mmm-auto.el,343 -(defvar mmm-autoloaded-classes67,2676 -(defun mmm-autoload-class 89,3439 -(defvar mmm-changed-buffers-list 129,4992 -(defun mmm-major-mode-change 132,5099 -(defun mmm-check-changed-buffers 145,5620 -(defun mmm-mode-on-maybe 154,5970 -(defalias 'mmm-add-find-file-hooks mmm-add-find-file-hooks166,6374 -(defun mmm-add-find-file-hook 167,6434 +(defvar mmm-autoloaded-classes67,2628 +(defun mmm-autoload-class 89,3391 +(defvar mmm-changed-buffers-list 129,4944 +(defun mmm-major-mode-change 132,5051 +(defun mmm-check-changed-buffers 145,5572 +(defun mmm-mode-on-maybe 154,5922 +(defalias 'mmm-add-find-file-hooks mmm-add-find-file-hooks166,6326 +(defun mmm-add-find-file-hook 167,6386 contrib/mmm/mmm-class.el,415 -(defun mmm-get-class-spec 42,1296 -(defun mmm-get-class-parameter 59,1939 -(defun mmm-set-class-parameter 63,2105 -(defun* mmm-apply-class75,2455 -(defun* mmm-apply-classes90,3072 -(defun* mmm-apply-all 110,3803 -(defun* mmm-ify124,4250 -(defun* mmm-match-region206,7095 -(defun mmm-match->point 269,9480 -(defun mmm-match-and-verify 284,10050 -(defun mmm-get-form 310,11101 -(defun mmm-default-get-form 321,11576 +(defun mmm-get-class-spec 42,1247 +(defun mmm-get-class-parameter 59,1890 +(defun mmm-set-class-parameter 63,2056 +(defun* mmm-apply-class75,2406 +(defun* mmm-apply-classes90,3023 +(defun* mmm-apply-all 110,3754 +(defun* mmm-ify124,4201 +(defun* mmm-match-region206,7046 +(defun mmm-match->point 269,9431 +(defun mmm-match-and-verify 284,10001 +(defun mmm-get-form 310,11052 +(defun mmm-default-get-form 321,11527 contrib/mmm/mmm-cmds.el,712 -(defun mmm-ify-by-class 41,1210 -(defun mmm-ify-region 63,1822 -(defun mmm-ify-by-regexp75,2243 -(defun mmm-parse-buffer 97,2886 -(defun mmm-parse-region 106,3222 -(defun mmm-parse-block 115,3601 -(defun mmm-get-block 132,4352 -(defun mmm-reparse-current-region 146,4634 -(defun mmm-clear-current-region 167,5210 -(defun mmm-clear-regions 172,5374 -(defun mmm-clear-all-regions 177,5520 -(defun* mmm-end-current-region 185,5680 -(defun mmm-narrow-to-submode-region 220,6928 -(defun mmm-insert-region 239,7542 -(defun mmm-insert-by-key 258,8348 -(defun mmm-get-insertion-spec 342,11613 -(defun mmm-insertion-help 369,12573 -(defun mmm-display-insertion-key 379,12936 -(defun mmm-get-all-insertion-keys 401,13723 +(defun mmm-ify-by-class 41,1162 +(defun mmm-ify-region 63,1774 +(defun mmm-ify-by-regexp75,2195 +(defun mmm-parse-buffer 97,2838 +(defun mmm-parse-region 106,3174 +(defun mmm-parse-block 115,3553 +(defun mmm-get-block 132,4304 +(defun mmm-reparse-current-region 146,4586 +(defun mmm-clear-current-region 167,5162 +(defun mmm-clear-regions 172,5326 +(defun mmm-clear-all-regions 177,5472 +(defun* mmm-end-current-region 185,5632 +(defun mmm-narrow-to-submode-region 220,6880 +(defun mmm-insert-region 239,7494 +(defun mmm-insert-by-key 258,8300 +(defun mmm-get-insertion-spec 342,11565 +(defun mmm-insertion-help 369,12525 +(defun mmm-display-insertion-key 379,12888 +(defun mmm-get-all-insertion-keys 401,13675 contrib/mmm/mmm-compat.el,418 -(defvar mmm-xemacs 40,1313 -(defvar mmm-keywords-used49,1616 -(defmacro mmm-regexp-opt 91,2632 -(defvar mmm-evaporate-property110,3281 -(defmacro mmm-set-keymap-default 128,4047 -(defmacro mmm-event-key 137,4489 -(defvar skeleton-positions 146,4708 -(defun mmm-fixup-skeleton 147,4739 -(defmacro mmm-make-temp-buffer 159,5162 -(defvar mmm-font-lock-available-p 172,5558 -(defmacro mmm-set-font-lock-defaults 179,5772 +(defvar mmm-xemacs 40,1263 +(defvar mmm-keywords-used49,1566 +(defmacro mmm-regexp-opt 91,2582 +(defvar mmm-evaporate-property110,3231 +(defmacro mmm-set-keymap-default 128,3997 +(defmacro mmm-event-key 137,4439 +(defvar skeleton-positions 146,4658 +(defun mmm-fixup-skeleton 147,4689 +(defmacro mmm-make-temp-buffer 159,5112 +(defvar mmm-font-lock-available-p 172,5508 +(defmacro mmm-set-font-lock-defaults 179,5722 contrib/mmm/mmm-cweb.el,228 -(defvar mmm-cweb-section-tags38,1117 -(defvar mmm-cweb-section-regexp41,1164 -(defvar mmm-cweb-c-part-tags44,1254 -(defvar mmm-cweb-c-part-regexp47,1313 -(defun mmm-cweb-in-limbo 50,1397 -(defun mmm-cweb-verify-brief-c 57,1622 +(defvar mmm-cweb-section-tags38,1069 +(defvar mmm-cweb-section-regexp41,1116 +(defvar mmm-cweb-c-part-tags44,1206 +(defvar mmm-cweb-c-part-regexp47,1265 +(defun mmm-cweb-in-limbo 50,1349 +(defun mmm-cweb-verify-brief-c 57,1574 contrib/mmm/mmm-mason.el,410 -(defvar mmm-mason-perl-tags41,1236 -(defvar mmm-mason-pseudo-perl-tags45,1377 -(defvar mmm-mason-non-perl-tags48,1453 -(defvar mmm-mason-perl-tags-regexp51,1554 -(defvar mmm-mason-pseudo-perl-tags-regexp56,1749 -(defvar mmm-mason-tag-names-regexp61,1966 -(defun mmm-mason-verify-inline 66,2186 -(defun mmm-mason-start-line 156,4838 -(defun mmm-mason-end-line 161,4903 -(defun mmm-mason-set-mode-line 168,4997 - -contrib/mmm/mmm-mode.el,1025 -(defun mmm-mode 101,3867 -(defun mmm-mode-on 140,5372 -(defun mmm-mode-off 183,7156 -(defvar mmm-mode-map 209,7897 -(defvar mmm-mode-prefix-map 212,7972 -(defvar mmm-mode-menu-map 215,8082 -(defun mmm-define-key 218,8173 -(define-key mmm-mode-prefix-map 242,8928 -(define-key mmm-mode-prefix-map 249,9186 -(define-key mmm-mode-map 252,9297 -(define-key mmm-mode-menu-map 255,9399 -(define-key mmm-mode-menu-map 257,9471 -(define-key mmm-mode-menu-map 259,9530 -(define-key mmm-mode-menu-map 261,9611 -(define-key mmm-mode-menu-map 263,9692 -(define-key mmm-mode-menu-map 265,9779 -(define-key mmm-mode-menu-map 268,9873 -(define-key mmm-mode-menu-map 270,9933 -(define-key mmm-mode-menu-map 273,10024 -(define-key mmm-mode-menu-map 275,10084 -(define-key mmm-mode-menu-map 277,10191 -(define-key mmm-mode-menu-map 279,10276 -(define-key mmm-mode-menu-map 282,10362 -(define-key mmm-mode-menu-map 284,10422 -(define-key mmm-mode-menu-map 286,10535 -(define-key mmm-mode-menu-map 288,10620 -(define-key mmm-mode-map 291,10703 +(defvar mmm-mason-perl-tags41,1187 +(defvar mmm-mason-pseudo-perl-tags45,1328 +(defvar mmm-mason-non-perl-tags48,1404 +(defvar mmm-mason-perl-tags-regexp51,1505 +(defvar mmm-mason-pseudo-perl-tags-regexp56,1700 +(defvar mmm-mason-tag-names-regexp61,1917 +(defun mmm-mason-verify-inline 66,2137 +(defun mmm-mason-start-line 156,4789 +(defun mmm-mason-end-line 161,4854 +(defun mmm-mason-set-mode-line 168,4948 + +contrib/mmm/mmm-mode.el,1024 +(defun mmm-mode 101,3819 +(defun mmm-mode-on 140,5324 +(defun mmm-mode-off 183,7108 +(defvar mmm-mode-map 209,7849 +(defvar mmm-mode-prefix-map 212,7924 +(defvar mmm-mode-menu-map 215,8034 +(defun mmm-define-key 218,8125 +(define-key mmm-mode-prefix-map 242,8880 +(define-key mmm-mode-prefix-map 249,9138 +(define-key mmm-mode-map 252,9249 +(define-key mmm-mode-menu-map 255,9351 +(define-key mmm-mode-menu-map 257,9423 +(define-key mmm-mode-menu-map 259,9482 +(define-key mmm-mode-menu-map 261,9563 +(define-key mmm-mode-menu-map 263,9644 +(define-key mmm-mode-menu-map 265,9731 +(define-key mmm-mode-menu-map 268,9825 +(define-key mmm-mode-menu-map 270,9885 +(define-key mmm-mode-menu-map 273,9976 +(define-key mmm-mode-menu-map 275,10036 +(define-key mmm-mode-menu-map 277,10143 +(define-key mmm-mode-menu-map 279,10228 +(define-key mmm-mode-menu-map 282,10314 +(define-key mmm-mode-menu-map 284,10374 +(define-key mmm-mode-menu-map 286,10487 +(define-key mmm-mode-menu-map 288,10572 +(define-key mmm-mode-map 291,10655 contrib/mmm/mmm-region.el,1643 -(defsubst mmm-overlay-at 54,1749 -(defun mmm-overlays-at 59,1934 -(defun mmm-included-p 72,2387 -(defun mmm-overlays-containing 112,3876 -(defun mmm-overlays-contained-in 125,4314 -(defun mmm-overlays-overlapping 138,4754 -(defun mmm-sort-overlays 149,5117 -(defvar mmm-current-overlay 158,5359 -(defvar mmm-previous-overlay 163,5574 -(defvar mmm-current-submode 168,5762 -(defvar mmm-previous-submode 173,5962 -(defun mmm-update-current-submode 178,6135 -(defun mmm-set-current-submode 199,6930 -(defun mmm-submode-at 210,7373 -(defun mmm-match-front 219,7648 -(defun mmm-match-back 238,8409 -(defun mmm-front-start 257,9154 -(defun mmm-back-end 265,9458 -(defun mmm-valid-submode-region 278,9805 -(defun* mmm-make-region305,10961 -(defun mmm-make-overlay 431,16311 -(defun mmm-get-face 459,17444 -(defun mmm-clear-overlays 470,17736 -(defun mmm-update-mode-info 486,18201 -(defun mmm-update-submode-region 572,21874 -(defun mmm-add-hooks 589,22604 -(defun mmm-remove-hooks 592,22701 -(defun mmm-get-local-variables-list 598,22828 -(defun mmm-get-locals 618,23524 -(defun mmm-get-saved-local 631,24021 -(defun mmm-set-local-variables 635,24186 -(defun mmm-get-saved-local-variables 646,24564 -(defun mmm-save-changed-local-variables 654,24839 -(defun mmm-clear-local-variables 673,25543 -(defun mmm-enable-font-lock 684,25808 -(defun mmm-update-font-lock-buffer 692,26068 -(defun mmm-refontify-maybe 705,26479 -(defun mmm-submode-changes-in 720,26959 -(defun mmm-regions-in 731,27316 -(defun mmm-regions-alist 745,27794 -(defun mmm-fontify-region 762,28321 -(defun mmm-fontify-region-list 783,29343 -(defun mmm-beginning-of-syntax 805,30091 +(defsubst mmm-overlay-at 54,1699 +(defun mmm-overlays-at 59,1884 +(defun mmm-included-p 72,2337 +(defun mmm-overlays-containing 112,3826 +(defun mmm-overlays-contained-in 125,4264 +(defun mmm-overlays-overlapping 138,4704 +(defun mmm-sort-overlays 149,5067 +(defvar mmm-current-overlay 158,5309 +(defvar mmm-previous-overlay 163,5524 +(defvar mmm-current-submode 168,5712 +(defvar mmm-previous-submode 173,5912 +(defun mmm-update-current-submode 178,6085 +(defun mmm-set-current-submode 199,6880 +(defun mmm-submode-at 210,7323 +(defun mmm-match-front 219,7598 +(defun mmm-match-back 238,8359 +(defun mmm-front-start 257,9104 +(defun mmm-back-end 265,9408 +(defun mmm-valid-submode-region 278,9755 +(defun* mmm-make-region305,10911 +(defun mmm-make-overlay 431,16261 +(defun mmm-get-face 459,17394 +(defun mmm-clear-overlays 470,17686 +(defun mmm-update-mode-info 486,18151 +(defun mmm-update-submode-region 572,21824 +(defun mmm-add-hooks 589,22554 +(defun mmm-remove-hooks 592,22651 +(defun mmm-get-local-variables-list 598,22778 +(defun mmm-get-locals 618,23474 +(defun mmm-get-saved-local 631,23971 +(defun mmm-set-local-variables 635,24136 +(defun mmm-get-saved-local-variables 646,24514 +(defun mmm-save-changed-local-variables 654,24789 +(defun mmm-clear-local-variables 673,25493 +(defun mmm-enable-font-lock 684,25758 +(defun mmm-update-font-lock-buffer 692,26018 +(defun mmm-refontify-maybe 705,26429 +(defun mmm-submode-changes-in 720,26909 +(defun mmm-regions-in 731,27266 +(defun mmm-regions-alist 745,27744 +(defun mmm-fontify-region 762,28271 +(defun mmm-fontify-region-list 783,29293 +(defun mmm-beginning-of-syntax 805,30041 contrib/mmm/mmm-rpm.el,154 -(defconst mmm-rpm-sh-start-tags48,1618 -(defvar mmm-rpm-sh-end-tags53,1842 -(defvar mmm-rpm-sh-start-regexp57,2016 -(defvar mmm-rpm-sh-end-regexp61,2194 +(defconst mmm-rpm-sh-start-tags48,1571 +(defvar mmm-rpm-sh-end-tags53,1795 +(defvar mmm-rpm-sh-start-regexp57,1969 +(defvar mmm-rpm-sh-end-regexp61,2147 contrib/mmm/mmm-sample.el,168 -(defvar mmm-here-doc-mode-alist 84,2601 -(defun mmm-here-doc-get-mode 93,3086 -(defun mmm-file-variables-verify 208,6343 -(defun mmm-file-variables-find-back 232,7148 +(defvar mmm-here-doc-mode-alist 84,2551 +(defun mmm-here-doc-get-mode 93,3036 +(defun mmm-file-variables-verify 208,6293 +(defun mmm-file-variables-find-back 232,7098 contrib/mmm/mmm-univ.el,34 (defun mmm-univ-get-mode 38,1205 contrib/mmm/mmm-utils.el,282 -(defmacro mmm-valid-buffer 42,1332 -(defmacro mmm-save-all 61,1941 -(defun mmm-format-string 74,2223 -(defun mmm-format-matches 85,2661 -(defmacro mmm-save-keyword 108,3419 -(defmacro mmm-save-keywords 116,3746 -(defun mmm-looking-back-at 129,4244 -(defun mmm-make-marker 146,4784 +(defmacro mmm-valid-buffer 42,1283 +(defmacro mmm-save-all 61,1892 +(defun mmm-format-string 74,2174 +(defun mmm-format-matches 85,2612 +(defmacro mmm-save-keyword 108,3370 +(defmacro mmm-save-keywords 116,3697 +(defun mmm-looking-back-at 129,4195 +(defun mmm-make-marker 146,4735 contrib/mmm/mmm-vars.el,2668 -(defgroup mmm 104,3283 -(defvar mmm-c-derived-modes111,3393 -(defvar mmm-save-local-variables115,3512 -(defvar mmm-buffer-saved-locals 341,10293 -(defvar mmm-region-saved-locals-defaults 346,10493 -(defvar mmm-region-saved-locals-for-dominant 352,10753 -(defgroup mmm-faces 362,11130 -(defcustom mmm-submode-decoration-level 368,11301 -(defface mmm-init-submode-face 386,12145 -(defface mmm-cleanup-submode-face 390,12285 -(defface mmm-declaration-submode-face 394,12422 -(defface mmm-comment-submode-face 398,12568 -(defface mmm-output-submode-face 402,12721 -(defface mmm-special-submode-face 406,12870 -(defface mmm-code-submode-face 410,13034 -(defface mmm-default-submode-face 414,13173 -(defface mmm-delimiter-face 419,13381 -(defcustom mmm-mode-string 426,13507 -(defcustom mmm-submode-mode-line-format 431,13638 -(defvar mmm-primary-mode-display-name 448,14293 -(defvar mmm-buffer-mode-display-name 453,14507 -(defun mmm-set-mode-line 459,14806 -(defvar mmm-classes 483,15614 -(defvar mmm-global-classes 489,15859 -(defcustom mmm-mode-ext-classes-alist 496,16041 -(defun mmm-add-mode-ext-class 515,16831 -(defcustom mmm-major-mode-preferences524,17156 -(defun mmm-add-to-major-mode-preferences 542,17884 -(defun mmm-ensure-modename 558,18642 -(defun mmm-modename->function 567,18945 -(defcustom mmm-delimiter-mode 581,19394 -(defcustom mmm-mode-prefix-key 591,19663 -(defcustom mmm-command-modifiers 596,19790 -(defcustom mmm-insert-modifiers 610,20423 -(defcustom mmm-use-old-command-keys 625,21101 -(defun mmm-use-old-command-keys 635,21565 -(defcustom mmm-mode-hook 643,21757 -(defun mmm-run-constructed-hook 663,22564 -(defun mmm-run-major-hook 671,22908 -(defun mmm-run-submode-hook 674,22985 -(defvar mmm-class-hooks-run 677,23072 -(defun mmm-run-class-hook 682,23244 -(defvar mmm-primary-mode-entry-hook 687,23416 -(defcustom mmm-major-mode-hook 702,24063 -(defun mmm-run-major-mode-hook 716,24694 -(defcustom mmm-global-mode 729,25235 -(defcustom mmm-never-modes745,25902 -(defvar mmm-set-file-name-for-modes 763,26202 -(defvar mmm-mode 774,26561 -(defvar mmm-primary-mode 782,26769 -(defvar mmm-classes-alist 793,27135 -(defun mmm-add-classes 948,35342 -(defun mmm-add-group 953,35507 -(defun mmm-add-to-group 963,35880 -(defconst mmm-version 977,36307 -(defun mmm-version 980,36372 -(defvar mmm-temp-buffer-name 987,36515 -(defvar mmm-interactive-history 993,36645 -(defun mmm-add-to-history 999,36914 -(defun mmm-clear-history 1002,36997 -(defvar mmm-mode-ext-classes 1010,37182 -(defun mmm-get-mode-ext-classes 1015,37393 -(defun mmm-clear-mode-ext-classes 1024,37720 -(defun mmm-mode-ext-applies 1028,37845 -(defun mmm-get-all-classes 1042,38224 - -doc/ProofGeneral.texi,6650 -@node Top145,4231 -@node Preface183,5385 -@node News for Version 4.1News for Version 4.1207,5999 -@node News for Version 4.0News for Version 4.0218,6306 -@node Future239,7157 -@node Credits268,8492 -@node Introducing Proof GeneralIntroducing Proof General390,12601 -@node Installing Proof GeneralInstalling Proof General445,14575 -@node Quick start guideQuick start guide459,15024 -@node Features of Proof GeneralFeatures of Proof General503,17145 -@node Supported proof assistantsSupported proof assistants592,21082 -@node Prerequisites for this manualPrerequisites for this manual641,22963 -@node Organization of this manualOrganization of this manual685,24582 -@node Basic Script ManagementBasic Script Management711,25410 -@node Walkthrough example in IsabelleWalkthrough example in Isabelle730,26010 -@node Proof scriptsProof scripts1015,37405 -@node Script buffersScript buffers1058,39525 -@node Locked queue and editing regionsLocked queue and editing regions1080,40102 -@node Goal-save sequencesGoal-save sequences1136,42249 -@node Active scripting bufferActive scripting buffer1173,43733 -@node Summary of Proof General buffersSummary of Proof General buffers1246,47366 -@node Script editing commandsScript editing commands1295,49623 -@node Script processing commandsScript processing commands1375,52582 -@node Proof assistant commandsProof assistant commands1501,57827 -@node Toolbar commandsToolbar commands1694,64755 -@node Interrupting during trace outputInterrupting during trace output1719,65714 -@node Advanced Script Management and EditingAdvanced Script Management and Editing1759,67644 -@node Document centred workingDocument centred working1780,68265 -@node Automatic processingAutomatic processing1892,72943 -@node Visibility of completed proofsVisibility of completed proofs1947,74991 -@node Switching between proof scriptsSwitching between proof scripts2002,76931 -@node View of processed files View of processed files 2039,78903 -@node Retracting across filesRetracting across files2099,81954 -@node Asserting across filesAsserting across files2112,82585 -@node Automatic multiple file handlingAutomatic multiple file handling2125,83151 -@node Escaping script managementEscaping script management2150,84185 -@node Editing featuresEditing features2207,86297 -@node Unicode symbols and special layout supportUnicode symbols and special layout support2277,89076 -@node Maths menuMaths menu2319,90634 -@node Unicode Tokens modeUnicode Tokens mode2336,91325 -@node Configuring tokens symbols and shortcutsConfiguring tokens symbols and shortcuts2386,93748 -@node Special layout Special layout 2416,94709 -@node Moving between Unicode and tokensMoving between Unicode and tokens2526,98827 -@node Finding available tokens shortcuts and symbolsFinding available tokens shortcuts and symbols2581,100938 -@node Selecting suitable fontsSelecting suitable fonts2620,102112 -@node Support for other PackagesSupport for other Packages2685,105100 -@node Syntax highlightingSyntax highlighting2715,105936 -@node Imenu and SpeedbarImenu and Speedbar2743,106939 -@node Support for outline modeSupport for outline mode2789,108610 -@node Support for completionSupport for completion2814,109739 -@node Support for tagsSupport for tags2871,111901 -@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing2923,114249 -@node Goals buffer commandsGoals buffer commands2939,114844 -@node Customizing Proof GeneralCustomizing Proof General3038,118997 -@node Basic optionsBasic options3078,120667 -@node How to customizeHow to customize3102,121437 -@node Display customizationDisplay customization3149,123404 -@node User optionsUser options3317,130366 -@node Changing facesChanging faces3553,139034 -@node Script buffer facesScript buffer faces3575,139909 -@node Goals and response facesGoals and response faces3621,141509 -@node Tweaking configuration settingsTweaking configuration settings3666,143041 -@node Hints and TipsHints and Tips3723,145567 -@node Adding your own keybindingsAdding your own keybindings3742,146168 -@node Using file variablesUsing file variables3806,148782 -@node Using abbreviationsUsing abbreviations3882,151453 -@node LEGO Proof GeneralLEGO Proof General3921,152868 -@node LEGO specific commandsLEGO specific commands3962,154237 -@node LEGO tagsLEGO tags3982,154692 -@node LEGO customizationsLEGO customizations3992,154939 -@node Coq Proof GeneralCoq Proof General4024,155858 -@node Coq-specific commandsCoq-specific commands4039,156195 -@node Multiple File SupportMultiple File Support4062,156703 -@node Automatic Compilation in DetailAutomatic Compilation in Detail4132,159292 -@node Locking AncestorsLocking Ancestors4207,162643 -@node Customizing Coq Multiple File SupportCustomizing Coq Multiple File Support4240,164068 -@node Current LimitationsCurrent Limitations4472,173838 -@node Editing multiple proofsEditing multiple proofs4498,174690 -@node User-loaded tacticsUser-loaded tactics4522,175798 -@node Holes featureHoles feature4586,178272 -@node Isabelle Proof GeneralIsabelle Proof General4615,179602 -@node Choosing logic and starting isabelleChoosing logic and starting isabelle4641,180478 -@node Isabelle commandsIsabelle commands4710,183279 -@node Isabelle settingsIsabelle settings4853,187471 -@node Isabelle customizationsIsabelle customizations4867,188053 -@node HOL Proof GeneralHOL Proof General4890,188540 -@node Shell Proof GeneralShell Proof General4932,190362 -@node Obtaining and InstallingObtaining and Installing4968,191821 -@node Obtaining Proof GeneralObtaining Proof General4983,192186 -@node Installing Proof General from tarballInstalling Proof General from tarball5009,193068 -@node Setting the names of binariesSetting the names of binaries5033,193858 -@node Notes for syssiesNotes for syssies5061,194798 -@node Bugs and EnhancementsBugs and Enhancements5137,197795 -@node References5158,198610 -@node History of Proof GeneralHistory of Proof General5198,199633 -@node Old News for 3.0Old News for 3.05292,203798 -@node Old News for 3.1Old News for 3.15362,207492 -@node Old News for 3.2Old News for 3.25388,208664 -@node Old News for 3.3Old News for 3.35449,211667 -@node Old News for 3.4Old News for 3.45468,212564 -@node Old News for 3.5Old News for 3.55490,213619 -@node Old News for 3.6Old News for 3.65494,213676 -@node Old News for 3.7Old News for 3.75499,213776 -@node Function IndexFunction Index5529,215230 -@node Variable IndexVariable Index5533,215306 -@node Keystroke IndexKeystroke Index5537,215386 -@node Concept IndexConcept Index5541,215452 - -doc/PG-adapting.texi,3844 -@node Top137,3992 -@node Introduction174,5101 -@node Future215,6754 -@node Credits251,8350 -@node Beginning with a New ProverBeginning with a New Prover261,8642 -@node Overview of adding a new proverOverview of adding a new prover301,10584 -@node Demonstration instance and easy configurationDemonstration instance and easy configuration383,14133 -@node Major modes used by Proof GeneralMajor modes used by Proof General452,17524 -@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands495,19234 -@node Settings for generic user-level commandsSettings for generic user-level commands510,19780 -@node Menu configurationMenu configuration555,21512 -@node Toolbar configurationToolbar configuration579,22429 -@node Proof Script SettingsProof Script Settings638,24666 -@node Recognizing commands and commentsRecognizing commands and comments661,25278 -@node Recognizing proofsRecognizing proofs798,31731 -@node Recognizing other elementsRecognizing other elements902,36035 -@node Configuring undo behaviourConfiguring undo behaviour965,38514 -@node Nested proofsNested proofs1102,43901 -@node Safe (state-preserving) commandsSafe (state-preserving) commands1142,45527 -@node Activate scripting hookActivate scripting hook1165,46480 -@node Automatic multiple filesAutomatic multiple files1189,47350 -@node Completely asserted buffersCompletely asserted buffers1210,48196 -@node Completions1243,49661 -@node Proof Shell SettingsProof Shell Settings1284,51151 -@node Proof shell commandsProof shell commands1315,52433 -@node Script input to the shellScript input to the shell1492,60197 -@node Settings for matching various output from proof processSettings for matching various output from proof process1562,63401 -@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process1684,68755 -@node Hooks and other settingsHooks and other settings1911,78717 -@node Goals Buffer SettingsGoals Buffer Settings1990,81861 -@node Splash Screen SettingsSplash Screen Settings2064,84851 -@node Global ConstantsGlobal Constants2090,85606 -@node Handling Multiple FilesHandling Multiple Files2116,86435 -@node Configuring Editing SyntaxConfiguring Editing Syntax2285,95104 -@node Configuring Font LockConfiguring Font Lock2342,97221 -@node Configuring TokensConfiguring Tokens2418,100933 -@node Writing More Lisp CodeWriting More Lisp Code2468,103053 -@node Default values for generic settingsDefault values for generic settings2485,103698 -@node Adding prover-specific configurationsAdding prover-specific configurations2515,104781 -@node Useful variablesUseful variables2558,106063 -@node Useful functions and macrosUseful functions and macros2573,106562 -@node Internals of Proof GeneralInternals of Proof General2683,110874 -@node Spans2713,111804 -@node Proof General site configurationProof General site configuration2728,112177 -@node Configuration variable mechanismsConfiguration variable mechanisms2811,115258 -@node Global variablesGlobal variables2941,120974 -@node Proof script modeProof script mode3016,123598 -@node Proof shell modeProof shell mode3280,135555 -@node Debugging3824,157585 -@node Plans and IdeasPlans and Ideas3867,158461 -@node Proof by pointing and similar featuresProof by pointing and similar features3888,159183 -@node Granularity of atomic command sequencesGranularity of atomic command sequences3926,160841 -@node Browser mode for script files and theoriesBrowser mode for script files and theories3971,163066 -@node Demonstration InstantiationsDemonstration Instantiations4001,164097 -@node demoisa-easy.el4017,164528 -@node demoisa.el4079,166719 -@node Function IndexFunction Index4233,171638 -@node Variable IndexVariable Index4237,171714 -@node Concept IndexConcept Index4246,171893 - -generic/proofgeneral-pkg.el,0 +(defgroup mmm 104,3235 +(defvar mmm-c-derived-modes111,3345 +(defvar mmm-save-local-variables115,3464 +(defvar mmm-buffer-saved-locals 341,10245 +(defvar mmm-region-saved-locals-defaults 346,10445 +(defvar mmm-region-saved-locals-for-dominant 352,10705 +(defgroup mmm-faces 362,11082 +(defcustom mmm-submode-decoration-level 368,11253 +(defface mmm-init-submode-face 386,12097 +(defface mmm-cleanup-submode-face 390,12237 +(defface mmm-declaration-submode-face 394,12374 +(defface mmm-comment-submode-face 398,12520 +(defface mmm-output-submode-face 402,12673 +(defface mmm-special-submode-face 406,12822 +(defface mmm-code-submode-face 410,12986 +(defface mmm-default-submode-face 414,13125 +(defface mmm-delimiter-face 419,13333 +(defcustom mmm-mode-string 426,13459 +(defcustom mmm-submode-mode-line-format 431,13590 +(defvar mmm-primary-mode-display-name 448,14245 +(defvar mmm-buffer-mode-display-name 453,14459 +(defun mmm-set-mode-line 459,14758 +(defvar mmm-classes 483,15566 +(defvar mmm-global-classes 489,15811 +(defcustom mmm-mode-ext-classes-alist 496,15993 +(defun mmm-add-mode-ext-class 515,16783 +(defcustom mmm-major-mode-preferences524,17108 +(defun mmm-add-to-major-mode-preferences 542,17836 +(defun mmm-ensure-modename 558,18594 +(defun mmm-modename->function 567,18897 +(defcustom mmm-delimiter-mode 581,19346 +(defcustom mmm-mode-prefix-key 591,19615 +(defcustom mmm-command-modifiers 596,19742 +(defcustom mmm-insert-modifiers 610,20375 +(defcustom mmm-use-old-command-keys 625,21053 +(defun mmm-use-old-command-keys 635,21517 +(defcustom mmm-mode-hook 643,21709 +(defun mmm-run-constructed-hook 663,22516 +(defun mmm-run-major-hook 671,22860 +(defun mmm-run-submode-hook 674,22937 +(defvar mmm-class-hooks-run 677,23024 +(defun mmm-run-class-hook 682,23196 +(defvar mmm-primary-mode-entry-hook 687,23368 +(defcustom mmm-major-mode-hook 702,24015 +(defun mmm-run-major-mode-hook 716,24646 +(defcustom mmm-global-mode 729,25187 +(defcustom mmm-never-modes745,25854 +(defvar mmm-set-file-name-for-modes 763,26154 +(defvar mmm-mode 774,26513 +(defvar mmm-primary-mode 782,26721 +(defvar mmm-classes-alist 793,27087 +(defun mmm-add-classes 948,35294 +(defun mmm-add-group 953,35459 +(defun mmm-add-to-group 963,35832 +(defconst mmm-version 977,36259 +(defun mmm-version 980,36324 +(defvar mmm-temp-buffer-name 987,36467 +(defvar mmm-interactive-history 993,36597 +(defun mmm-add-to-history 999,36866 +(defun mmm-clear-history 1002,36949 +(defvar mmm-mode-ext-classes 1010,37134 +(defun mmm-get-mode-ext-classes 1015,37345 +(defun mmm-clear-mode-ext-classes 1024,37672 +(defun mmm-mode-ext-applies 1028,37797 +(defun mmm-get-all-classes 1042,38176 + +doc/ProofGeneral.texi,7046 +@node Top145,4126 +@node Preface184,5319 +@node News for Version 4.1News for Version 4.1208,5933 +@node News for Version 4.0News for Version 4.0219,6240 +@node Future240,7091 +@node Credits269,8426 +@node Introducing Proof GeneralIntroducing Proof General391,12535 +@node Installing Proof GeneralInstalling Proof General446,14509 +@node Quick start guideQuick start guide460,14958 +@node Features of Proof GeneralFeatures of Proof General504,17079 +@node Supported proof assistantsSupported proof assistants610,21623 +@node Prerequisites for this manualPrerequisites for this manual659,23504 +@node Organization of this manualOrganization of this manual703,25123 +@node Basic Script ManagementBasic Script Management729,25951 +@node Walkthrough example in IsabelleWalkthrough example in Isabelle748,26551 +@node Proof scriptsProof scripts1033,37946 +@node Script buffersScript buffers1076,40066 +@node Locked queue and editing regionsLocked queue and editing regions1098,40643 +@node Goal-save sequencesGoal-save sequences1154,42790 +@node Active scripting bufferActive scripting buffer1191,44274 +@node Summary of Proof General buffersSummary of Proof General buffers1264,47907 +@node Script editing commandsScript editing commands1313,50164 +@node Script processing commandsScript processing commands1393,53123 +@node Proof assistant commandsProof assistant commands1519,58368 +@node Toolbar commandsToolbar commands1712,65296 +@node Interrupting during trace outputInterrupting during trace output1737,66255 +@node Advanced Script Management and EditingAdvanced Script Management and Editing1777,68185 +@node Document centred workingDocument centred working1798,68806 +@node Automatic processingAutomatic processing1910,73484 +@node Visibility of completed proofsVisibility of completed proofs1965,75532 +@node Switching between proof scriptsSwitching between proof scripts2020,77472 +@node View of processed files View of processed files 2057,79444 +@node Retracting across filesRetracting across files2117,82495 +@node Asserting across filesAsserting across files2130,83126 +@node Automatic multiple file handlingAutomatic multiple file handling2143,83692 +@node Escaping script managementEscaping script management2168,84726 +@node Editing featuresEditing features2225,86838 +@node Unicode symbols and special layout supportUnicode symbols and special layout support2295,89617 +@node Maths menuMaths menu2337,91175 +@node Unicode Tokens modeUnicode Tokens mode2354,91866 +@node Configuring tokens symbols and shortcutsConfiguring tokens symbols and shortcuts2404,94289 +@node Special layout Special layout 2434,95250 +@node Moving between Unicode and tokensMoving between Unicode and tokens2544,99368 +@node Finding available tokens shortcuts and symbolsFinding available tokens shortcuts and symbols2599,101479 +@node Selecting suitable fontsSelecting suitable fonts2638,102653 +@node Support for other PackagesSupport for other Packages2703,105641 +@node Syntax highlightingSyntax highlighting2733,106477 +@node Imenu and SpeedbarImenu and Speedbar2761,107480 +@node Support for outline modeSupport for outline mode2807,109151 +@node Support for completionSupport for completion2832,110280 +@node Support for tagsSupport for tags2889,112442 +@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing2941,114790 +@node Goals buffer commandsGoals buffer commands2957,115385 +@node Graphical Proof-Tree VisualizationGraphical Proof-Tree Visualization3056,119538 +@node Starting and Stopping Proof-Tree VisualizationStarting and Stopping Proof-Tree Visualization3079,120430 +@node Features of ProoftreeFeatures of Prooftree3107,121587 +@node Prooftree CustomizationProoftree Customization3139,122799 +@node Customizing Proof GeneralCustomizing Proof General3163,123678 +@node Basic optionsBasic options3203,125348 +@node How to customizeHow to customize3227,126118 +@node Display customizationDisplay customization3274,128085 +@node User optionsUser options3442,135047 +@node Changing facesChanging faces3678,143715 +@node Script buffer facesScript buffer faces3700,144590 +@node Goals and response facesGoals and response faces3746,146190 +@node Tweaking configuration settingsTweaking configuration settings3791,147722 +@node Hints and TipsHints and Tips3848,150248 +@node Adding your own keybindingsAdding your own keybindings3867,150849 +@node Using file variablesUsing file variables3931,153463 +@node Using abbreviationsUsing abbreviations4007,156134 +@node LEGO Proof GeneralLEGO Proof General4046,157549 +@node LEGO specific commandsLEGO specific commands4087,158918 +@node LEGO tagsLEGO tags4107,159373 +@node LEGO customizationsLEGO customizations4117,159620 +@node Coq Proof GeneralCoq Proof General4149,160539 +@node Coq-specific commandsCoq-specific commands4165,160905 +@node Multiple File SupportMultiple File Support4188,161413 +@node Automatic Compilation in DetailAutomatic Compilation in Detail4258,164002 +@node Locking AncestorsLocking Ancestors4333,167353 +@node Customizing Coq Multiple File SupportCustomizing Coq Multiple File Support4366,168778 +@node Current LimitationsCurrent Limitations4598,178548 +@node Editing multiple proofsEditing multiple proofs4624,179400 +@node User-loaded tacticsUser-loaded tactics4648,180508 +@node Holes featureHoles feature4712,182982 +@node Proof-Tree VisualizationProof-Tree Visualization4737,184201 +@node Isabelle Proof GeneralIsabelle Proof General4749,184551 +@node Choosing logic and starting isabelleChoosing logic and starting isabelle4775,185427 +@node Isabelle commandsIsabelle commands4844,188228 +@node Isabelle settingsIsabelle settings4987,192420 +@node Isabelle customizationsIsabelle customizations5001,193002 +@node HOL Proof GeneralHOL Proof General5024,193489 +@node Shell Proof GeneralShell Proof General5066,195311 +@node Obtaining and InstallingObtaining and Installing5102,196770 +@node Obtaining Proof GeneralObtaining Proof General5117,197135 +@node Installing Proof General from tarballInstalling Proof General from tarball5143,198017 +@node Setting the names of binariesSetting the names of binaries5167,198807 +@node Notes for syssiesNotes for syssies5195,199747 +@node Bugs and EnhancementsBugs and Enhancements5271,202744 +@node References5292,203559 +@node History of Proof GeneralHistory of Proof General5332,204582 +@node Old News for 3.0Old News for 3.05426,208747 +@node Old News for 3.1Old News for 3.15496,212441 +@node Old News for 3.2Old News for 3.25522,213613 +@node Old News for 3.3Old News for 3.35583,216616 +@node Old News for 3.4Old News for 3.45602,217513 +@node Old News for 3.5Old News for 3.55624,218568 +@node Old News for 3.6Old News for 3.65628,218625 +@node Old News for 3.7Old News for 3.75633,218725 +@node Function IndexFunction Index5663,220179 +@node Variable IndexVariable Index5667,220255 +@node Keystroke IndexKeystroke Index5671,220335 +@node Concept IndexConcept Index5675,220401 + +doc/PG-adapting.texi,4541 +@node Top137,3889 +@node Introduction175,5039 +@node Future216,6692 +@node Credits252,8288 +@node Beginning with a New ProverBeginning with a New Prover262,8580 +@node Overview of adding a new proverOverview of adding a new prover302,10522 +@node Demonstration instance and easy configurationDemonstration instance and easy configuration384,14071 +@node Major modes used by Proof GeneralMajor modes used by Proof General453,17462 +@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands496,19172 +@node Settings for generic user-level commandsSettings for generic user-level commands511,19718 +@node Menu configurationMenu configuration556,21450 +@node Toolbar configurationToolbar configuration580,22367 +@node Proof Script SettingsProof Script Settings639,24604 +@node Recognizing commands and commentsRecognizing commands and comments662,25216 +@node Recognizing proofsRecognizing proofs799,31669 +@node Recognizing other elementsRecognizing other elements903,35973 +@node Configuring undo behaviourConfiguring undo behaviour966,38452 +@node Nested proofsNested proofs1103,43839 +@node Safe (state-preserving) commandsSafe (state-preserving) commands1143,45465 +@node Activate scripting hookActivate scripting hook1166,46418 +@node Automatic multiple filesAutomatic multiple files1190,47288 +@node Completely asserted buffersCompletely asserted buffers1211,48134 +@node Completions1244,49599 +@node Proof Shell SettingsProof Shell Settings1285,51089 +@node Proof shell commandsProof shell commands1316,52371 +@node Script input to the shellScript input to the shell1493,60135 +@node Settings for matching various output from proof processSettings for matching various output from proof process1563,63339 +@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process1686,68750 +@node Hooks and other settingsHooks and other settings1913,78712 +@node Goals Buffer SettingsGoals Buffer Settings1992,81856 +@node Splash Screen SettingsSplash Screen Settings2066,84846 +@node Global ConstantsGlobal Constants2092,85601 +@node Handling Multiple FilesHandling Multiple Files2118,86430 +@node Configuring Editing SyntaxConfiguring Editing Syntax2287,95099 +@node Configuring Font LockConfiguring Font Lock2344,97216 +@node Configuring TokensConfiguring Tokens2420,100928 +@node Configuring Proof-Tree VisualizationConfiguring Proof-Tree Visualization2470,103048 +@node Prerequisites2487,103588 +@node Proof-Tree Display InternalsProof-Tree Display Internals2550,106239 +@node Organization of the CodeOrganization of the Code2568,106729 +@node Communication2664,110992 +@node Guards2689,112104 +@node Urgent and Delayed ActionsUrgent and Delayed Actions2743,114249 +@node Full AnnotationFull Annotation2804,116757 +@node Configuring Prooftree for a New Proof AssistantConfiguring Prooftree for a New Proof Assistant2818,117331 +@node Proof Tree Elisp configurationProof Tree Elisp configuration2830,117663 +@node Prooftree AdaptionProoftree Adaption2851,118493 +@node Writing More Lisp CodeWriting More Lisp Code2871,119172 +@node Default values for generic settingsDefault values for generic settings2888,119817 +@node Adding prover-specific configurationsAdding prover-specific configurations2918,120900 +@node Useful variablesUseful variables2961,122182 +@node Useful functions and macrosUseful functions and macros2976,122681 +@node Internals of Proof GeneralInternals of Proof General3086,126993 +@node Spans3116,127923 +@node Proof General site configurationProof General site configuration3131,128296 +@node Configuration variable mechanismsConfiguration variable mechanisms3214,131377 +@node Global variablesGlobal variables3344,137093 +@node Proof script modeProof script mode3419,139717 +@node Proof shell modeProof shell mode3683,151674 +@node Debugging4234,174109 +@node Plans and IdeasPlans and Ideas4277,174985 +@node Proof by pointing and similar featuresProof by pointing and similar features4298,175707 +@node Granularity of atomic command sequencesGranularity of atomic command sequences4336,177365 +@node Browser mode for script files and theoriesBrowser mode for script files and theories4381,179590 +@node Demonstration InstantiationsDemonstration Instantiations4411,180621 +@node demoisa-easy.el4427,181052 +@node demoisa.el4489,183190 +@node Function IndexFunction Index4643,188056 +@node Variable IndexVariable Index4647,188132 +@node Concept IndexConcept Index4656,188311 generic/proof.el,0 |