diff options
Diffstat (limited to 'TAGS')
| -rw-r--r-- | TAGS | 2508 |
1 files changed, 1267 insertions, 1241 deletions
@@ -17,79 +17,241 @@ coq/coq-abbrev.el,495 (defconst coq-terms-abbrev-table51,1434 (defun coq-install-abbrevs 58,1628 (defpgdefault menu-entries78,2365 -(defpgdefault help-menu-entries141,4384 - -coq/coq-db.el,668 -(defconst coq-syntax-db 23,544 -(defvar coq-user-tactics-db59,1917 -(defun coq-insert-from-db 69,2266 -(defun coq-build-regexp-list-from-db 87,2998 -(defun max-length-db 109,3981 -(defun coq-build-menu-from-db-internal 121,4256 -(defun coq-build-title-menu 156,5879 -(defun coq-sort-menu-entries 165,6247 -(defun coq-build-menu-from-db 171,6374 -(defcustom coq-holes-minor-mode 193,7213 -(defun coq-build-abbrev-table-from-db 199,7357 -(defun filter-state-preserving 218,7995 -(defun filter-state-changing 223,8149 -(defface coq-solve-tactics-face230,8370 -(defface coq-cheat-face239,8700 -(defconst coq-solve-tactics-face 247,8948 -(defconst coq-cheat-face 251,9112 - -coq/coq-indent.el,2223 +(defpgdefault help-menu-entries143,4479 + +coq/coq-db.el,678 +(defconst coq-syntax-db 24,596 +(defun coq-insert-from-db 70,2319 +(defun coq-build-regexp-list-from-db 88,3050 +(defun coq-build-opt-regexp-from-db 107,3856 +(defun max-length-db 126,4677 +(defun coq-build-menu-from-db-internal 138,4952 +(defun coq-build-title-menu 175,6493 +(defun coq-sort-menu-entries 184,6861 +(defun coq-build-menu-from-db 190,6988 +(defcustom coq-holes-minor-mode 212,7827 +(defun coq-build-abbrev-table-from-db 218,7971 +(defun filter-state-preserving 237,8609 +(defun filter-state-changing 242,8763 +(defface coq-solve-tactics-face249,8984 +(defface coq-cheat-face258,9314 +(defconst coq-solve-tactics-face 266,9562 +(defconst coq-cheat-face 270,9726 + +coq/coq.el,5959 +(defcustom coq-translate-to-v8 48,1381 +(defun coq-build-prog-args 54,1561 +(defcustom coq-compile-file-command 64,1857 +(defcustom coq-use-makefile 72,2176 +(defcustom coq-default-undo-limit 80,2399 +(defconst coq-shell-init-cmd85,2527 +(defcustom coq-prog-env 91,2654 +(defconst coq-shell-restart-cmd 99,2904 +(defvar coq-shell-prompt-pattern101,2958 +(defvar coq-shell-cd 109,3261 +(defvar coq-shell-proof-completed-regexp 113,3421 +(defvar coq-goal-regexp116,3576 +(defun coq-library-directory 121,3672 +(defcustom coq-tags 127,3850 +(defconst coq-interrupt-regexp 132,4000 +(defcustom coq-www-home-page 135,4093 +(defvar coq-outline-regexp146,4268 +(defvar coq-outline-heading-end-regexp 153,4480 +(defvar coq-shell-outline-regexp 155,4534 +(defvar coq-shell-outline-heading-end-regexp 156,4584 +(defconst coq-state-preserving-tactics-regexp159,4648 +(defconst coq-state-changing-commands-regexp161,4750 +(defconst coq-state-preserving-commands-regexp163,4859 +(defconst coq-commands-regexp165,4972 +(defvar coq-retractable-instruct-regexp167,5051 +(defvar coq-non-retractable-instruct-regexp169,5143 +(defun coq-set-undo-limit 204,5830 +(defun build-list-id-from-string 208,5960 +(defun coq-last-prompt-info 220,6458 +(defun coq-last-prompt-info-safe 232,6990 +(defvar coq-last-but-one-statenum 238,7247 +(defvar coq-last-but-one-proofnum 245,7545 +(defvar coq-last-but-one-proofstack 248,7643 +(defsubst coq-get-span-statenum 251,7753 +(defsubst coq-get-span-proofnum 255,7868 +(defsubst coq-get-span-proofstack 259,7983 +(defsubst coq-set-span-statenum 263,8127 +(defsubst coq-get-span-goalcmd 267,8258 +(defsubst coq-set-span-goalcmd 271,8372 +(defsubst coq-set-span-proofnum 275,8502 +(defsubst coq-set-span-proofstack 279,8633 +(defsubst proof-last-locked-span 283,8793 +(defun proof-clone-buffer 287,8927 +(defun proof-store-buffer-win 301,9462 +(defun proof-store-response-win 312,9955 +(defun proof-store-goals-win 316,10082 +(defun coq-set-state-infos 328,10614 +(defun count-not-intersection 366,12701 +(defun coq-find-and-forget 396,13950 +(defvar coq-current-goal 420,15044 +(defun coq-goal-hyp 423,15109 +(defun coq-state-preserving-p 436,15541 +(defconst notation-print-kinds-table450,15855 +(defun coq-PrintScope 454,16022 +(defun coq-guess-or-ask-for-string 472,16571 +(defun coq-ask-do 486,17139 +(defsubst coq-put-into-brackets 495,17524 +(defsubst coq-put-into-quotes 498,17585 +(defun coq-SearchIsos 501,17645 +(defun coq-SearchConstant 509,17886 +(defun coq-Searchregexp 513,17979 +(defun coq-SearchRewrite 519,18122 +(defun coq-SearchAbout 523,18219 +(defun coq-Print 529,18364 +(defun coq-About 534,18489 +(defun coq-LocateConstant 539,18609 +(defun coq-LocateLibrary 544,18712 +(defun coq-LocateNotation 549,18829 +(defun coq-Pwd 557,19061 +(defun coq-Inspect 562,19185 +(defun coq-PrintSection(566,19285 +(defun coq-Print-implicit 570,19378 +(defun coq-Check 575,19529 +(defun coq-Show 580,19637 +(defun coq-Compile 594,20080 +(defun coq-guess-command-line 606,20398 +(defpacustom use-editing-holes 643,21951 +(defun coq-mode-config 652,22254 +(defun coq-shell-mode-config 745,25597 +(defun coq-goals-mode-config 788,27387 +(defun coq-response-config 795,27631 +(defpacustom print-fully-explicit 820,28456 +(defpacustom print-implicit 825,28604 +(defpacustom print-coercions 830,28770 +(defpacustom print-match-wildcards 835,28914 +(defpacustom print-elim-types 840,29094 +(defpacustom printing-depth 845,29260 +(defpacustom undo-depth 850,29421 +(defpacustom time-commands 855,29587 +(defpacustom auto-compile-vos 859,29697 +(defun coq-maybe-compile-buffer 888,30811 +(defun coq-ancestors-of 924,32339 +(defun coq-all-ancestors-of 947,33303 +(defun coq-process-require-command 958,33650 +(defun coq-included-children 963,33777 +(defun coq-process-file 984,34616 +(defun coq-preprocessing 999,35145 +(defun coq-fake-constant-markup 1013,35600 +(defun coq-create-span-menu 1029,36205 +(defconst module-kinds-table1047,36718 +(defconst modtype-kinds-table1051,36867 +(defun coq-insert-section-or-module 1055,36996 +(defconst reqkinds-kinds-table1076,37846 +(defun coq-insert-requires 1080,37990 +(defun coq-end-Section 1093,38470 +(defun coq-insert-intros 1111,39048 +(defun coq-insert-infoH-hook 1123,39581 +(defun coq-insert-as 1128,39789 +(defun coq-insert-match 1145,40482 +(defun coq-insert-solve-tactic 1174,41652 +(defun coq-insert-tactic 1180,41903 +(defun coq-insert-tactical 1186,42105 +(defun coq-insert-command 1192,42336 +(defun coq-insert-term 1197,42501 +(define-key coq-keymap 1202,42662 +(define-key coq-keymap 1203,42720 +(define-key coq-keymap 1204,42777 +(define-key coq-keymap 1205,42846 +(define-key coq-keymap 1206,42902 +(define-key coq-keymap 1207,42951 +(define-key coq-keymap 1208,43009 +(define-key coq-keymap 1209,43069 +(define-key coq-keymap 1210,43134 +(define-key coq-keymap 1213,43262 +(define-key coq-keymap 1215,43336 +(define-key coq-keymap 1216,43393 +(define-key coq-keymap 1220,43518 +(define-key coq-keymap 1222,43574 +(define-key coq-keymap 1223,43624 +(define-key coq-keymap 1224,43674 +(define-key coq-keymap 1225,43730 +(define-key coq-keymap 1226,43780 +(define-key coq-keymap 1227,43834 +(define-key coq-keymap 1228,43893 +(define-key coq-goals-mode-map 1231,43954 +(define-key coq-goals-mode-map 1232,44036 +(define-key coq-goals-mode-map 1233,44118 +(define-key coq-goals-mode-map 1234,44205 +(define-key coq-goals-mode-map 1235,44287 +(defvar last-coq-error-location 1244,44589 +(defun coq-get-last-error-location 1252,44973 +(defun coq-highlight-error 1302,47530 +(defun coq-highlight-error-hook 1330,48611 +(defun first-word-of-buffer 1340,48828 +(defun coq-show-first-goal 1348,49031 +(defvar coq-modeline-string2 1365,49726 +(defvar coq-modeline-string1 1366,49760 +(defvar coq-modeline-string0 1367,49794 +(defun coq-build-subgoals-string 1368,49835 +(defun coq-update-minor-mode-alist 1373,50001 +(defun is-not-split-vertic 1405,51395 +(defun optim-resp-windows 1414,51835 + +coq/coq-indent.el,2515 (defconst coq-any-command-regexp20,368 -(defconst coq-indent-inner-regexp23,459 -(defconst coq-comment-start-regexp 33,813 -(defconst coq-comment-end-regexp 34,856 -(defconst coq-comment-start-or-end-regexp35,897 -(defconst coq-indent-open-regexp37,1005 -(defconst coq-indent-close-regexp42,1179 -(defconst coq-indent-closepar-regexp 47,1360 -(defconst coq-indent-closematch-regexp 48,1405 -(defconst coq-indent-openpar-regexp 49,1476 -(defconst coq-indent-openmatch-regexp 50,1520 -(defconst coq-indent-any-regexp51,1600 -(defconst coq-indent-kw56,1878 -(defconst coq-indent-pattern-regexp 66,2332 -(defun coq-indent-goal-command-p 70,2435 -(defconst coq-end-command-regexp92,3486 -(defun coq-search-comment-delimiter-forward 97,3638 -(defun coq-search-comment-delimiter-backward 106,3968 -(defun coq-skip-until-one-comment-backward 113,4242 -(defun coq-skip-until-one-comment-forward 128,4949 -(defun coq-looking-at-comment 139,5467 -(defun coq-find-comment-start 143,5608 -(defun coq-find-comment-end 154,6041 -(defun coq-looking-at-syntactic-context 166,6534 -(defconst coq-end-command-or-comment-regexp172,6756 -(defconst coq-end-command-or-comment-start-regexp175,6865 -(defun coq-find-not-in-comment-backward 179,6983 -(defun coq-find-not-in-comment-forward 199,7884 -(defun coq-find-command-end-backward 223,9023 -(defun coq-find-command-end-forward 232,9414 -(defun coq-find-command-end 241,9791 -(defun coq-find-current-start 249,10123 -(defun coq-find-real-start 258,10414 -(defun coq-command-at-point 265,10633 -(defun coq-indent-only-spaces-on-line 272,10918 -(defun coq-indent-find-reg 278,11195 -(defun coq-find-no-syntactic-on-line 292,11731 -(defun coq-back-to-indentation-prevline 305,12204 -(defun coq-find-unclosed 349,14112 -(defun coq-find-at-same-level-zero 379,15408 -(defun coq-find-unopened 407,16566 -(defun coq-find-last-unopened 450,18000 -(defun coq-end-offset 461,18397 -(defun coq-indent-command-offset 486,19167 -(defun coq-indent-expr-offset 533,20991 -(defun coq-indent-comment-offset 649,25674 -(defun coq-indent-offset 681,27123 -(defun coq-indent-calculate 699,27985 -(defun coq-indent-line 702,28073 -(defun coq-indent-line-not-comments 712,28439 -(defun coq-indent-region 722,28828 +(defconst coq-indent-inner-regexp23,442 +(defconst coq-comment-start-regexp 33,796 +(defconst coq-comment-end-regexp 34,839 +(defconst coq-comment-start-or-end-regexp35,880 +(defconst coq-indent-open-regexp37,988 +(defconst coq-indent-close-regexp42,1164 +(defconst coq-indent-closepar-regexp 45,1275 +(defconst coq-indent-closematch-regexp 46,1320 +(defconst coq-indent-openpar-regexp 47,1391 +(defconst coq-indent-openmatch-regexp 48,1435 +(defconst coq-tacticals-tactics-regex49,1515 +(defconst coq-indent-any-regexp51,1634 +(defconst coq-indent-kw55,1850 +(defconst coq-indent-pattern-regexp 65,2316 +(defun coq-indent-goal-command-p 69,2419 +(defconst coq-end-command-regexp91,3470 +(defun coq-search-comment-delimiter-forward 96,3622 +(defun coq-search-comment-delimiter-backward 105,3952 +(defun coq-skip-until-one-comment-backward 112,4226 +(defun coq-skip-until-one-comment-forward 127,4933 +(defun coq-looking-at-comment 138,5451 +(defun coq-find-comment-start 142,5592 +(defun coq-find-comment-end 153,6025 +(defun coq-looking-at-syntactic-context 165,6518 +(defconst coq-end-command-or-comment-regexp171,6740 +(defconst coq-end-command-or-comment-start-regexp174,6849 +(defun coq-find-not-in-comment-backward 178,6967 +(defun coq-find-not-in-comment-forward 198,7868 +(defun coq-find-command-end-backward 222,9007 +(defun coq-find-command-end-forward 231,9398 +(defun coq-find-command-end 240,9775 +(defun coq-find-current-start 248,10107 +(defun coq-find-real-start 257,10398 +(defun coq-command-at-point 264,10617 +(defun same-line 272,10903 +(defun coq-commands-at-line 275,10990 +(defun coq-indent-only-spaces-on-line 294,11613 +(defun coq-indent-find-reg 300,11890 +(defun coq-find-no-syntactic-on-line 314,12426 +(defun coq-back-to-indentation-prevline 327,12899 +(defun coq-find-unclosed 370,14785 +(defun coq-find-at-same-level-zero 400,16095 +(defun coq-find-unopened 429,17361 +(defun coq-find-last-unopened 472,18795 +(defun coq-end-offset 483,19192 +(defun coq-add-iter 508,19962 +(defun coq-goal-count 511,20068 +(defun coq-save-count 513,20140 +(defun coq-proof-count 515,20226 +(defun coq-goal-save-diff-maybe-proof 519,20401 +(defun coq-indent-command-offset 526,20622 +(defun coq-indent-expr-offset 558,22225 +(defun coq-indent-comment-offset 673,26909 +(defun coq-indent-offset 705,28358 +(defun coq-indent-calculate 724,29233 +(defun coq-indent-line 727,29321 +(defun coq-indent-line-not-comments 737,29687 +(defun coq-indent-region 747,30076 coq/coq-local-vars.el,280 (defconst coq-local-vars-doc 20,429 @@ -97,74 +259,80 @@ coq/coq-local-vars.el,280 (defun coq-read-directory 89,3430 (defun coq-extract-directories-from-args 113,4533 (defun coq-ask-prog-args 128,5085 -(defun coq-ask-prog-name 150,6149 -(defun coq-ask-insert-coq-prog-name 168,6904 - -coq/coq-syntax.el,2563 -(defcustom coq-prog-name 18,561 -(defcustom coq-user-tactics-db 38,1343 -(defcustom coq-user-commands-db 55,1856 -(defcustom coq-user-tacticals-db 71,2375 -(defcustom coq-user-solve-tactics-db 87,2896 -(defcustom coq-user-cheat-tactics-db 103,3415 -(defcustom coq-user-reserved-db 122,3961 -(defvar coq-tactics-db140,4492 -(defvar coq-solve-tactics-db298,12751 -(defvar coq-solve-cheat-tactics-db321,13596 -(defvar coq-tacticals-db333,13771 -(defvar coq-decl-db357,14657 -(defvar coq-defn-db380,15951 -(defvar coq-goal-starters-db438,20313 -(defvar coq-other-commands-db467,22070 -(defvar coq-commands-db592,31283 -(defvar coq-terms-db599,31503 -(defun coq-count-match 663,34152 -(defun coq-module-opening-p 679,34881 -(defun coq-section-command-p 690,35292 -(defun coq-goal-command-str-p 694,35389 -(defun coq-goal-command-p 721,36491 -(defvar coq-keywords-save-strict730,36774 -(defvar coq-keywords-save739,36887 -(defun coq-save-command-p 743,36965 -(defvar coq-keywords-kill-goal752,37259 -(defvar coq-keywords-state-changing-misc-commands756,37349 -(defvar coq-keywords-goal759,37474 -(defvar coq-keywords-decl762,37557 -(defvar coq-keywords-defn765,37631 -(defvar coq-keywords-state-changing-commands769,37706 -(defvar coq-keywords-state-preserving-commands778,37966 -(defvar coq-keywords-commands783,38182 -(defvar coq-solve-tactics788,38330 -(defvar coq-solve-cheat-tactics792,38451 -(defvar coq-tacticals796,38596 -(defvar coq-reserved802,38735 -(defvar coq-state-changing-tactics813,39063 -(defvar coq-state-preserving-tactics816,39172 -(defvar coq-tactics820,39286 -(defvar coq-retractable-instruct823,39375 -(defvar coq-non-retractable-instruct826,39485 -(defvar coq-keywords830,39613 -(defvar coq-symbols837,39780 -(defvar coq-error-regexp 856,39993 -(defvar coq-id 859,40221 -(defvar coq-id-shy 860,40246 -(defvar coq-ids 862,40300 -(defun coq-first-abstr-regexp 864,40341 -(defcustom coq-variable-highlight-enable 867,40436 -(defvar coq-font-lock-terms873,40563 -(defconst coq-save-command-regexp-strict894,41562 -(defconst coq-save-command-regexp898,41728 -(defconst coq-save-with-hole-regexp903,41881 -(defconst coq-goal-command-regexp907,42039 -(defconst coq-goal-with-hole-regexp910,42139 -(defconst coq-decl-with-hole-regexp914,42271 -(defconst coq-defn-with-hole-regexp921,42519 -(defconst coq-with-with-hole-regexp931,42807 -(defconst coq-require-command-regexp938,43100 -(defvar coq-font-lock-keywords-1946,43325 -(defvar coq-font-lock-keywords 974,44727 -(defun coq-init-syntax-table 976,44785 -(defconst coq-generic-expression1005,45683 +(defun coq-ask-prog-name 150,6153 +(defun coq-ask-insert-coq-prog-name 167,6864 + +coq/coq-syntax.el,2818 +(defcustom coq-prog-name 18,559 +(defcustom coq-user-tactics-db 38,1341 +(defcustom coq-user-commands-db 55,1854 +(defcustom coq-user-tacticals-db 71,2373 +(defcustom coq-user-solve-tactics-db 87,2894 +(defcustom coq-user-cheat-tactics-db 103,3413 +(defcustom coq-user-reserved-db 122,3959 +(defvar coq-tactics-db140,4490 +(defvar coq-solve-tactics-db298,12749 +(defvar coq-solve-cheat-tactics-db321,13594 +(defvar coq-tacticals-db333,13769 +(defvar coq-decl-db357,14655 +(defvar coq-defn-db382,16111 +(defvar coq-goal-starters-db440,20466 +(defvar coq-other-commands-db469,22223 +(defvar coq-commands-db598,31689 +(defvar coq-terms-db605,31909 +(defun coq-count-match 667,34524 +(defun coq-module-opening-p 683,35253 +(defun coq-section-command-p 694,35664 +(defun coq-goal-command-str-p 698,35761 +(defun coq-goal-command-p 725,36863 +(defvar coq-keywords-save-strict734,37146 +(defvar coq-keywords-save743,37259 +(defun coq-save-command-p 747,37337 +(defvar coq-keywords-kill-goal758,37665 +(defvar coq-keywords-state-changing-misc-commands762,37755 +(defvar coq-keywords-goal765,37880 +(defvar coq-keywords-decl768,37963 +(defvar coq-keywords-defn771,38037 +(defvar coq-keywords-state-changing-commands775,38112 +(defvar coq-keywords-state-preserving-commands784,38372 +(defvar coq-keywords-commands789,38588 +(defvar coq-solve-tactics794,38736 +(defvar coq-solve-tactics-regexp798,38857 +(defvar coq-solve-cheat-tactics802,38991 +(defvar coq-solve-cheat-tactics-regexp806,39136 +(defvar coq-tacticals810,39294 +(defvar coq-reserved816,39433 +(defvar coq-reserved-regexp 826,39760 +(defvar coq-state-changing-tactics828,39825 +(defvar coq-state-preserving-tactics831,39934 +(defvar coq-tactics835,40048 +(defvar coq-tactics-regexp 838,40137 +(defvar coq-retractable-instruct841,40292 +(defvar coq-non-retractable-instruct844,40402 +(defvar coq-keywords848,40530 +(defun proof-regexp-alt-list-symb 854,40754 +(defvar coq-keywords-regexp 857,40859 +(defvar coq-symbols860,40927 +(defvar coq-error-regexp 879,41140 +(defvar coq-id 882,41368 +(defvar coq-id-shy 883,41393 +(defvar coq-ids 886,41495 +(defun coq-first-abstr-regexp 888,41561 +(defcustom coq-variable-highlight-enable 891,41656 +(defvar coq-font-lock-terms897,41783 +(defconst coq-save-command-regexp-strict919,42866 +(defconst coq-save-command-regexp925,43036 +(defconst coq-save-with-hole-regexp930,43191 +(defconst coq-goal-command-regexp934,43351 +(defconst coq-goal-with-hole-regexp937,43453 +(defconst coq-decl-with-hole-regexp941,43587 +(defconst coq-defn-with-hole-regexp948,43837 +(defconst coq-with-with-hole-regexp958,44127 +(defconst coq-require-command-regexp965,44420 +(defvar coq-font-lock-keywords-1973,44645 +(defvar coq-font-lock-keywords 1001,45980 +(defun coq-init-syntax-table 1003,46038 +(defconst coq-generic-expression1028,46765 coq/coq-unicode-tokens.el,454 (defconst coq-token-format 39,1427 @@ -172,167 +340,12 @@ coq/coq-unicode-tokens.el,454 (defconst coq-hexcode-match 41,1506 (defun coq-unicode-tokens-set 43,1540 (defcustom coq-token-symbol-map49,1768 -(defcustom coq-shortcut-alist152,4361 -(defconst coq-control-char-format-regexp241,6379 -(defconst coq-control-char-format 245,6504 -(defconst coq-control-characters247,6547 -(defconst coq-control-region-format-regexp 251,6639 -(defconst coq-control-regions253,6722 - -coq/coq.el,6009 -(defcustom coq-translate-to-v8 48,1381 -(defun coq-build-prog-args 54,1561 -(defcustom coq-compile-file-command 64,1857 -(defcustom coq-use-makefile 72,2176 -(defcustom coq-default-undo-limit 80,2399 -(defconst coq-shell-init-cmd85,2527 -(defcustom coq-prog-env 91,2654 -(defconst coq-shell-restart-cmd 99,2904 -(defvar coq-shell-prompt-pattern101,2958 -(defvar coq-shell-cd 109,3261 -(defvar coq-shell-proof-completed-regexp 113,3421 -(defvar coq-goal-regexp116,3576 -(defun coq-library-directory 123,3690 -(defcustom coq-tags 130,3869 -(defconst coq-interrupt-regexp 135,4019 -(defcustom coq-www-home-page 140,4140 -(defvar coq-outline-regexp147,4308 -(defvar coq-outline-heading-end-regexp 154,4520 -(defvar coq-shell-outline-regexp 156,4574 -(defvar coq-shell-outline-heading-end-regexp 157,4624 -(defconst coq-state-preserving-tactics-regexp163,4789 -(defconst coq-state-changing-commands-regexp165,4889 -(defconst coq-state-preserving-commands-regexp167,4996 -(defconst coq-commands-regexp169,5107 -(defvar coq-retractable-instruct-regexp171,5184 -(defvar coq-non-retractable-instruct-regexp173,5274 -(defun coq-set-undo-limit 207,6151 -(defun build-list-id-from-string 211,6281 -(defun coq-last-prompt-info 223,6779 -(defun coq-last-prompt-info-safe 235,7311 -(defvar coq-last-but-one-statenum 241,7568 -(defvar coq-last-but-one-proofnum 248,7866 -(defvar coq-last-but-one-proofstack 251,7964 -(defsubst coq-get-span-statenum 254,8074 -(defsubst coq-get-span-proofnum 258,8189 -(defsubst coq-get-span-proofstack 262,8304 -(defsubst coq-set-span-statenum 266,8448 -(defsubst coq-get-span-goalcmd 270,8579 -(defsubst coq-set-span-goalcmd 274,8693 -(defsubst coq-set-span-proofnum 278,8823 -(defsubst coq-set-span-proofstack 282,8954 -(defsubst proof-last-locked-span 286,9114 -(defun proof-clone-buffer 292,9347 -(defun proof-store-buffer-win 306,9904 -(defun proof-store-response-win 313,10176 -(defun proof-store-goals-win 317,10303 -(defun coq-set-state-infos 329,10835 -(defun count-not-intersection 366,12921 -(defun coq-find-and-forget 397,14171 -(defvar coq-current-goal 417,15075 -(defun coq-goal-hyp 420,15140 -(defun coq-state-preserving-p 433,15572 -(defconst notation-print-kinds-table447,16073 -(defun coq-PrintScope 451,16240 -(defun coq-guess-or-ask-for-string 469,16789 -(defun coq-ask-do 483,17357 -(defsubst coq-put-into-brackets 492,17742 -(defsubst coq-put-into-quotes 495,17803 -(defun coq-SearchIsos 498,17863 -(defun coq-SearchConstant 506,18104 -(defun coq-Searchregexp 510,18197 -(defun coq-SearchRewrite 516,18340 -(defun coq-SearchAbout 520,18438 -(defun coq-Print 526,18584 -(defun coq-About 531,18709 -(defun coq-LocateConstant 536,18829 -(defun coq-LocateLibrary 541,18932 -(defun coq-LocateNotation 546,19050 -(defun coq-Pwd 554,19247 -(defun coq-Inspect 559,19347 -(defun coq-PrintSection(563,19447 -(defun coq-Print-implicit 567,19540 -(defun coq-Check 572,19691 -(defun coq-Show 577,19799 -(defun coq-Compile 591,20242 -(defun coq-guess-command-line 603,20560 -(defpacustom use-editing-holes 640,22113 -(defun coq-mode-config 649,22416 -(defun coq-shell-mode-config 741,25721 -(defun coq-goals-mode-config 783,27444 -(defun coq-response-config 790,27688 -(defpacustom print-fully-explicit 815,28513 -(defpacustom print-implicit 820,28661 -(defpacustom print-coercions 825,28827 -(defpacustom print-match-wildcards 830,28971 -(defpacustom print-elim-types 835,29151 -(defpacustom printing-depth 840,29317 -(defpacustom undo-depth 845,29478 -(defpacustom time-commands 850,29625 -(defpacustom undo-limit 854,29735 -(defpacustom auto-compile-vos 859,29837 -(defun coq-maybe-compile-buffer 888,30951 -(defun coq-ancestors-of 924,32479 -(defun coq-all-ancestors-of 947,33443 -(defun coq-process-require-command 958,33790 -(defun coq-included-children 963,33917 -(defun coq-process-file 984,34756 -(defun coq-preprocessing 999,35295 -(defun coq-fake-constant-markup 1013,35730 -(defun coq-create-span-menu 1029,36335 -(defconst module-kinds-table1047,36848 -(defconst modtype-kinds-table1051,36997 -(defun coq-insert-section-or-module 1055,37126 -(defconst reqkinds-kinds-table1076,37976 -(defun coq-insert-requires 1080,38120 -(defun coq-end-Section 1093,38600 -(defun coq-insert-intros 1111,39178 -(defun coq-insert-infoH-hook 1123,39711 -(defun coq-insert-as 1128,39919 -(defun coq-insert-match 1145,40612 -(defun coq-insert-tactic 1174,41782 -(defun coq-insert-tactical 1180,42021 -(defun coq-insert-command 1186,42270 -(defun coq-insert-term 1192,42514 -(define-key coq-keymap 1198,42711 -(define-key coq-keymap 1199,42769 -(define-key coq-keymap 1200,42826 -(define-key coq-keymap 1201,42895 -(define-key coq-keymap 1202,42951 -(define-key coq-keymap 1203,43000 -(define-key coq-keymap 1204,43058 -(define-key coq-keymap 1205,43118 -(define-key coq-keymap 1206,43183 -(define-key coq-keymap 1208,43246 -(define-key coq-keymap 1209,43305 -(define-key coq-keymap 1213,43430 -(define-key coq-keymap 1215,43486 -(define-key coq-keymap 1216,43536 -(define-key coq-keymap 1217,43586 -(define-key coq-keymap 1218,43642 -(define-key coq-keymap 1219,43692 -(define-key coq-keymap 1220,43746 -(define-key coq-keymap 1221,43805 -(define-key coq-goals-mode-map 1224,43866 -(define-key coq-goals-mode-map 1225,43948 -(define-key coq-goals-mode-map 1226,44030 -(define-key coq-goals-mode-map 1227,44117 -(define-key coq-goals-mode-map 1228,44199 -(defvar last-coq-error-location 1237,44501 -(defun coq-get-last-error-location 1245,44885 -(defun coq-highlight-error 1295,47442 -(defvar coq-allow-highlight-error 1326,48638 -(defun coq-decide-highlight-error 1333,48964 -(defun coq-highlight-error-hook 1338,49149 -(defun first-word-of-buffer 1349,49542 -(defun coq-show-first-goal 1357,49745 -(defvar coq-modeline-string2 1374,50440 -(defvar coq-modeline-string1 1375,50484 -(defvar coq-modeline-string0 1376,50527 -(defun coq-build-subgoals-string 1377,50572 -(defun coq-update-minor-mode-alist 1382,50738 -(defun is-not-split-vertic 1408,51809 -(defun optim-resp-windows 1417,52249 +(defcustom coq-shortcut-alist165,4719 +(defconst coq-control-char-format-regexp254,6737 +(defconst coq-control-char-format 258,6862 +(defconst coq-control-characters260,6905 +(defconst coq-control-region-format-regexp 264,6997 +(defconst coq-control-regions266,7080 hol98/hol98.el,121 (defvar hol98-keywords 17,419 @@ -375,6 +388,46 @@ isar/isabelle-system.el,1254 isar/isar-autotest.el,31 (defvar isar-long-tests 8,187 +isar/isar.el,1595 +(defcustom isar-keywords-name 39,916 +(defpgdefault completion-table 55,1427 +(defcustom isar-web-page57,1480 +(defun isar-strip-terminators 71,1830 +(defun isar-markup-ml 83,2186 +(defun isar-mode-config-set-variables 88,2321 +(defun isar-shell-mode-config-set-variables 153,5120 +(defun isar-set-proof-find-theorems-command 235,8306 +(defpacustom use-find-theorems-form 241,8490 +(defun isar-set-undo-commands 246,8656 +(defpacustom use-linear-undo 260,9248 +(defun isar-configure-from-settings 265,9406 +(defun isar-remove-file 273,9550 +(defun isar-shell-compute-new-files-list 285,9854 +(define-derived-mode isar-shell-mode 304,10424 +(define-derived-mode isar-response-mode 309,10551 +(define-derived-mode isar-goals-mode 314,10684 +(define-derived-mode isar-mode 319,10810 +(defpgdefault menu-entries371,12525 +(defun isar-set-command 402,13719 +(defpgdefault help-menu-entries 407,13849 +(defun isar-count-undos 410,13925 +(defun isar-find-and-forget 436,14891 +(defun isar-goal-command-p 472,16234 +(defun isar-global-save-command-p 477,16411 +(defvar isar-current-goal 498,17195 +(defun isar-state-preserving-p 501,17261 +(defvar isar-shell-current-line-width 526,18110 +(defun isar-shell-adjust-line-width 531,18302 +(defsubst isar-string-wrapping 554,19067 +(defsubst isar-positions-of 563,19261 +(defcustom isar-wrap-commands-singly 569,19466 +(defun isar-command-wrapping 575,19662 +(defun isar-preprocessing 583,19976 +(defun isar-mode-config 601,20527 +(defun isar-shell-mode-config 615,21180 +(defun isar-response-mode-config 625,21529 +(defun isar-goals-mode-config 635,21864 + isar/isar-find-theorems.el,779 (defvar isar-find-theorems-data 19,565 (defun isar-find-theorems-minibuffer 35,1039 @@ -545,70 +598,12 @@ isar/isar-unicode-tokens.el,1363 (defconst isar-fraktur-uppercase-letters-tokens 494,12636 (defconst isar-fraktur-lowercase-letters-tokens 499,12805 (defcustom isar-token-symbol-map 504,12996 -(defcustom isar-user-tokens 520,13465 -(defun isar-init-token-symbol-map 527,13702 -(defcustom isar-symbol-shortcuts552,14351 -(defcustom isar-shortcut-alist 624,16550 -(defun isar-init-shortcut-alists 632,16809 -(defconst isar-tokens-customizable-variables653,17472 - -isar/isar.el,1595 -(defcustom isar-keywords-name 39,916 -(defpgdefault completion-table 55,1427 -(defcustom isar-web-page57,1480 -(defun isar-strip-terminators 71,1830 -(defun isar-markup-ml 83,2186 -(defun isar-mode-config-set-variables 88,2321 -(defun isar-shell-mode-config-set-variables 153,5120 -(defun isar-set-proof-find-theorems-command 235,8306 -(defpacustom use-find-theorems-form 241,8490 -(defun isar-set-undo-commands 246,8656 -(defpacustom use-linear-undo 260,9248 -(defun isar-configure-from-settings 265,9408 -(defun isar-remove-file 273,9552 -(defun isar-shell-compute-new-files-list 285,9856 -(define-derived-mode isar-shell-mode 304,10426 -(define-derived-mode isar-response-mode 309,10553 -(define-derived-mode isar-goals-mode 314,10686 -(define-derived-mode isar-mode 319,10812 -(defpgdefault menu-entries371,12527 -(defun isar-set-command 402,13721 -(defpgdefault help-menu-entries 407,13851 -(defun isar-count-undos 410,13927 -(defun isar-find-and-forget 436,14893 -(defun isar-goal-command-p 472,16245 -(defun isar-global-save-command-p 477,16422 -(defvar isar-current-goal 498,17206 -(defun isar-state-preserving-p 501,17272 -(defvar isar-shell-current-line-width 526,18121 -(defun isar-shell-adjust-line-width 531,18313 -(defsubst isar-string-wrapping 554,19078 -(defsubst isar-positions-of 563,19272 -(defcustom isar-wrap-commands-singly 569,19477 -(defun isar-command-wrapping 575,19673 -(defun isar-preprocessing 583,19987 -(defun isar-mode-config 601,20538 -(defun isar-shell-mode-config 615,21191 -(defun isar-response-mode-config 625,21540 -(defun isar-goals-mode-config 635,21875 - -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 +(defcustom isar-user-tokens 521,13537 +(defun isar-init-token-symbol-map 535,13977 +(defcustom isar-symbol-shortcuts560,14626 +(defcustom isar-shortcut-alist 632,16825 +(defun isar-init-shortcut-alists 640,17084 +(defconst isar-tokens-customizable-variables661,17747 lego/lego.el,1636 (defcustom lego-tags 21,535 @@ -652,6 +647,41 @@ lego/lego.el,1636 (defun lego-shell-mode-config 373,12756 (defun lego-goals-mode-config 420,14423 +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 + phox/phox-extraction.el,383 (defvar phox-prog-orig 19,619 (defun phox-prog-flags-modify(21,687 @@ -790,75 +820,59 @@ phox/phox-tags.el,305 (defun phox-complete-tag(69,2091 (defvar phox-tags-menu76,2200 -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 - generic/pg-assoc.el,81 (defun proof-associated-buffers 33,973 (defun proof-associated-windows 43,1183 -generic/pg-autotest.el,868 +generic/pg-autotest.el,869 (defvar pg-autotest-success 30,692 (defvar pg-autotest-log 33,779 -(defadvice proof-debug 38,916 -(defun pg-autotest-find-file 44,1092 -(defun pg-autotest-find-file-restart 51,1358 -(defmacro pg-autotest 64,1811 -(defun pg-autotest-log 91,2532 -(defun pg-autotest-message 99,2756 -(defun pg-autotest-remark 108,3040 -(defun pg-autotest-timestart 111,3121 -(defun pg-autotest-timetaken 116,3304 -(defun pg-autotest-exit 127,3668 -(defun pg-autotest-test-process-wholefile 138,4019 -(defun pg-autotest-test-script-wholefile 146,4306 -(defun pg-autotest-test-script-randomjumps 171,5238 -(defun pg-autotest-test-retract-file 221,6847 -(defun pg-autotest-test-assert-processed 227,6988 -(defun pg-autotest-test-assert-full 233,7214 -(defun pg-autotest-test-assert-unprocessed 240,7455 -(defun pg-autotest-test-eval 247,7720 -(defun pg-autotest-test-quit-prover 251,7819 - -generic/pg-custom.el,556 -(defpgcustom script-indent 36,1140 -(defconst proof-toolbar-entries-default41,1277 -(defpgcustom toolbar-entries 69,3008 -(defpgcustom prog-args 88,3741 -(defpgcustom prog-env 101,4316 -(defpgcustom favourites 110,4743 -(defpgcustom menu-entries 115,4932 -(defpgcustom help-menu-entries 122,5168 -(defpgcustom keymap 129,5431 -(defpgcustom completion-table 134,5602 -(defpgcustom tags-program 145,5976 -(defpgcustom use-holes 154,6360 -(defpgcustom maths-menu-enable 164,6641 -(defpgcustom unicode-tokens-enable 170,6821 -(defpgcustom mmm-enable 176,6998 +(defadvice proof-debug 39,972 +(defun pg-autotest-find-file 47,1176 +(defun pg-autotest-find-file-restart 54,1442 +(defmacro pg-autotest 68,1916 +(defun pg-autotest-log 95,2637 +(defun pg-autotest-message 103,2861 +(defun pg-autotest-remark 112,3150 +(defun pg-autotest-timestart 115,3231 +(defun pg-autotest-timetaken 120,3414 +(defun pg-autotest-exit 131,3778 +(defun pg-autotest-test-process-wholefile 142,4129 +(defun pg-autotest-test-script-wholefile 150,4416 +(defun pg-autotest-test-script-randomjumps 175,5348 +(defun pg-autotest-test-retract-file 224,6905 +(defun pg-autotest-test-assert-processed 230,7046 +(defun pg-autotest-test-assert-full 236,7272 +(defun pg-autotest-test-assert-unprocessed 243,7513 +(defun pg-autotest-test-eval 250,7778 +(defun pg-autotest-test-quit-prover 254,7877 + +generic/pg-custom.el,599 +(defpgcustom script-indent 37,1199 +(defconst proof-toolbar-entries-default42,1336 +(defpgcustom toolbar-entries 70,3069 +(defpgcustom prog-args 89,3802 +(defpgcustom prog-env 102,4377 +(defpgcustom favourites 111,4804 +(defpgcustom menu-entries 116,4993 +(defpgcustom help-menu-entries 123,5229 +(defpgcustom keymap 130,5492 +(defpgcustom completion-table 135,5663 +(defpgcustom tags-program 146,6037 +(defpgcustom use-holes 155,6421 +(defpgcustom one-command-per-line162,6679 +(defpgcustom maths-menu-enable 173,6915 +(defpgcustom unicode-tokens-enable 179,7095 +(defpgcustom mmm-enable 185,7272 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,1921 -(defun pg-goals-display 76,2187 -(defun pg-goals-button-action 117,3491 +(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 @@ -872,20 +886,20 @@ generic/pg-movie.el,334 (defun pg-movie-export-directory 120,3496 generic/pg-pamacs.el,486 -(defmacro deflocal 37,1200 -(deflocal proof-buffer-type 44,1438 -(defmacro proof-ass-sym 52,1574 -(defmacro proof-ass-symv 58,1833 -(defmacro proof-ass 64,2091 -(defun proof-defpgcustom-fn 70,2343 -(defun undefpgcustom 91,3213 -(defmacro defpgcustom 97,3437 -(defun proof-defpgdefault-fn 108,3848 -(defmacro defpgdefault 122,4306 -(defmacro defpgfun 133,4668 -(defun proof-defpacustom-fn 147,5067 -(defmacro defpacustom 211,7251 -(defmacro proof-eval-when-ready-for-assistant 232,8198 +(defmacro deflocal 35,1132 +(deflocal proof-buffer-type 42,1370 +(defmacro proof-ass-sym 50,1506 +(defmacro proof-ass-symv 56,1765 +(defmacro proof-ass 62,2023 +(defun proof-defpgcustom-fn 68,2275 +(defun undefpgcustom 89,3145 +(defmacro defpgcustom 95,3369 +(defun proof-defpgdefault-fn 106,3780 +(defmacro defpgdefault 120,4238 +(defmacro defpgfun 131,4600 +(defun proof-defpacustom-fn 145,4999 +(defmacro defpacustom 209,7183 +(defmacro proof-eval-when-ready-for-assistant 230,8130 generic/pg-pbrpm.el,1808 (defvar pg-pbrpm-use-buffer-menu 45,1208 @@ -911,24 +925,24 @@ generic/pg-pbrpm.el,1808 (defun pg-pbrpm-build-menu 206,7205 (defun pg-pbrpm-setup-span 269,9525 (defun pg-pbrpm-run-command 329,11824 -(defun pg-pbrpm-get-pos-info 362,13345 -(defun pg-pbrpm-get-region-info 404,14644 -(defun pg-pbrpm-auto-select-around-point 415,15056 -(defun pg-pbrpm-translate-position 430,15580 -(defun pg-pbrpm-process-click 438,15834 -(defvar pg-pbrpm-remember-region-selected-region 458,16859 -(defvar pg-pbrpm-regions-list 459,16913 -(defun pg-pbrpm-erase-regions-list 461,16949 -(defun pg-pbrpm-filter-regions-list 470,17257 -(defface pg-pbrpm-multiple-selection-face477,17520 -(defface pg-pbrpm-menu-input-face485,17722 -(defun pg-pbrpm-do-remember-region 493,17912 -(defun pg-pbrpm-remember-region-drag-up-hook 514,18760 -(defun pg-pbrpm-remember-region-click-hook 518,18931 -(defun pg-pbrpm-remember-region 523,19116 -(defun pg-pbrpm-process-region 537,19830 -(defun pg-pbrpm-process-regions-list 555,20559 -(defun pg-pbrpm-region-expression 559,20742 +(defun pg-pbrpm-get-pos-info 362,13349 +(defun pg-pbrpm-get-region-info 404,14648 +(defun pg-pbrpm-auto-select-around-point 415,15060 +(defun pg-pbrpm-translate-position 430,15584 +(defun pg-pbrpm-process-click 438,15838 +(defvar pg-pbrpm-remember-region-selected-region 458,16863 +(defvar pg-pbrpm-regions-list 459,16917 +(defun pg-pbrpm-erase-regions-list 461,16953 +(defun pg-pbrpm-filter-regions-list 470,17261 +(defface pg-pbrpm-multiple-selection-face477,17524 +(defface pg-pbrpm-menu-input-face485,17726 +(defun pg-pbrpm-do-remember-region 493,17916 +(defun pg-pbrpm-remember-region-drag-up-hook 514,18764 +(defun pg-pbrpm-remember-region-click-hook 518,18935 +(defun pg-pbrpm-remember-region 523,19120 +(defun pg-pbrpm-process-region 537,19834 +(defun pg-pbrpm-process-regions-list 555,20563 +(defun pg-pbrpm-region-expression 559,20746 generic/pg-pgip.el,2931 (defalias 'pg-pgip-debug pg-pgip-debug38,1032 @@ -1032,96 +1046,95 @@ generic/pg-response.el,1291 (defun proof-trace-buffer-finish 459,15774 (defun pg-thms-buffer-clear 477,16117 -generic/pg-user.el,3700 +generic/pg-user.el,3635 (defun proof-script-new-command-advance 42,1232 -(defun proof-maybe-follow-locked-end 85,2994 -(defun proof-goto-command-start 112,3870 -(defun proof-goto-command-end 135,4817 -(defun proof-goto-point 158,5342 -(defun proof-assert-next-command-interactive 172,5776 -(defun proof-assert-until-point-interactive 184,6262 -(defun proof-process-buffer 190,6492 -(defun proof-undo-last-successful-command 208,7004 -(defun proof-undo-and-delete-last-successful-command 213,7166 -(defun proof-undo-last-successful-command-1 226,7720 -(defun proof-retract-buffer 243,8339 -(defun proof-retract-current-goal 252,8623 -(defun proof-mouse-goto-point 271,9143 -(defvar proof-minibuffer-history 286,9419 -(defun proof-minibuffer-cmd 289,9514 -(defun proof-frob-locked-end 328,10921 -(defmacro proof-if-setting-configured 389,12859 -(defmacro proof-define-assistant-command 397,13128 -(defmacro proof-define-assistant-command-witharg 410,13583 -(defun proof-issue-new-command 430,14405 -(defun proof-cd-sync 470,15628 -(defun proof-electric-terminator-enable 523,17298 -(defun proof-electric-terminator 530,17542 -(defun proof-add-completions 555,18346 -(defun proof-script-complete 580,19235 -(defun pg-copy-span-contents 594,19544 -(defun pg-numth-span-higher-or-lower 611,20102 -(defun pg-control-span-of 637,20848 -(defun pg-move-span-contents 643,21052 -(defun pg-fixup-children-spans 695,23228 -(defun pg-move-region-down 705,23485 -(defun pg-move-region-up 714,23778 -(defun proof-forward-command 744,24606 -(defun proof-backward-command 765,25327 -(defun pg-pos-for-event 787,25671 -(defun pg-span-for-event 793,25892 -(defun pg-span-context-menu 797,26036 -(defun pg-toggle-visibility 812,26484 -(defun pg-create-in-span-context-menu 821,26791 -(defun pg-span-undo 850,28005 -(defun pg-goals-buffers-hint 896,29388 -(defun pg-slow-fontify-tracing-hint 900,29570 -(defun pg-response-buffers-hint 904,29741 -(defun pg-jump-to-end-hint 916,30156 -(defun pg-processing-complete-hint 920,30285 -(defun pg-next-error-hint 937,31005 -(defun pg-hint 942,31157 -(defun pg-identifier-under-mouse-query 958,31747 -(defun pg-identifier-near-point-query 968,32056 -(defvar proof-query-identifier-collection 996,32953 -(defvar proof-query-identifier-history 997,33000 -(defun proof-query-identifier 999,33045 -(defun pg-identifier-query 1010,33364 -(defun proof-imenu-enable 1043,34512 -(defvar pg-input-ring 1079,35815 -(defvar pg-input-ring-index 1082,35872 -(defvar pg-stored-incomplete-input 1085,35944 -(defun pg-previous-input 1088,36047 -(defun pg-next-input 1102,36504 -(defun pg-delete-input 1107,36626 -(defun pg-get-old-input 1120,36964 -(defun pg-restore-input 1134,37355 -(defun pg-search-start 1145,37645 -(defun pg-regexp-arg 1157,38137 -(defun pg-search-arg 1169,38585 -(defun pg-previous-matching-input-string-position 1183,39002 -(defun pg-previous-matching-input 1210,40167 -(defun pg-next-matching-input 1229,41017 -(defvar pg-matching-input-from-input-string 1237,41400 -(defun pg-previous-matching-input-from-input 1241,41514 -(defun pg-next-matching-input-from-input 1259,42279 -(defun pg-add-to-input-history 1270,42658 -(defun pg-remove-from-input-history 1282,43111 -(defun pg-clear-input-ring 1293,43491 -(define-key proof-mode-map 1310,43961 -(define-key proof-mode-map 1311,44021 -(defun pg-protected-undo 1313,44093 -(defun pg-protected-undo-1 1348,45483 -(defun next-undo-elt 1379,46917 -(defvar proof-autosend-timer 1406,47873 -(deflocal proof-autosend-modified-tick 1408,47934 -(defun proof-autosend-enable 1412,48056 -(defun proof-autosend-delay 1426,48599 -(defun proof-autosend-loop 1430,48732 -(defun proof-autosend-loop-all 1442,49191 -(defun proof-autosend-loop-next 1468,50117 - -generic/pg-vars.el,1451 +(defun proof-maybe-follow-locked-end 66,2157 +(defun proof-goto-command-start 92,2993 +(defun proof-goto-command-end 115,3940 +(defun proof-forward-command 130,4362 +(defun proof-backward-command 151,5083 +(defun proof-goto-point 162,5297 +(defun proof-assert-next-command-interactive 176,5731 +(defun proof-assert-until-point-interactive 188,6217 +(defun proof-process-buffer 194,6447 +(defun proof-undo-last-successful-command 212,6959 +(defun proof-undo-and-delete-last-successful-command 217,7121 +(defun proof-undo-last-successful-command-1 229,7642 +(defun proof-retract-buffer 246,8306 +(defun proof-retract-current-goal 255,8590 +(defun proof-mouse-goto-point 274,9110 +(defvar proof-minibuffer-history 289,9386 +(defun proof-minibuffer-cmd 292,9481 +(defun proof-frob-locked-end 331,10888 +(defmacro proof-if-setting-configured 367,11989 +(defmacro proof-define-assistant-command 375,12258 +(defmacro proof-define-assistant-command-witharg 388,12713 +(defun proof-issue-new-command 408,13535 +(defun proof-cd-sync 448,14758 +(defun proof-electric-terminator-enable 499,16357 +(defun proof-electric-terminator 507,16661 +(defun proof-add-completions 531,17441 +(defun proof-script-complete 554,18264 +(defun pg-copy-span-contents 568,18573 +(defun pg-numth-span-higher-or-lower 582,18997 +(defun pg-control-span-of 608,19743 +(defun pg-move-span-contents 614,19947 +(defun pg-fixup-children-spans 665,22065 +(defun pg-move-region-down 675,22322 +(defun pg-move-region-up 684,22615 +(defun pg-pos-for-event 698,22889 +(defun pg-span-for-event 704,23110 +(defun pg-span-context-menu 708,23254 +(defun pg-toggle-visibility 724,23771 +(defun pg-create-in-span-context-menu 733,24078 +(defun pg-span-undo 757,25010 +(defun pg-goals-buffers-hint 770,25248 +(defun pg-slow-fontify-tracing-hint 774,25430 +(defun pg-response-buffers-hint 778,25601 +(defun pg-jump-to-end-hint 790,26016 +(defun pg-processing-complete-hint 794,26145 +(defun pg-next-error-hint 811,26865 +(defun pg-hint 816,27017 +(defun pg-identifier-under-mouse-query 827,27366 +(defun pg-identifier-near-point-query 838,27690 +(defvar proof-query-identifier-history 867,28613 +(defun proof-query-identifier 870,28700 +(defun pg-identifier-query 881,29056 +(defun proof-imenu-enable 914,30204 +(defvar pg-input-ring 950,31507 +(defvar pg-input-ring-index 953,31564 +(defvar pg-stored-incomplete-input 956,31636 +(defun pg-previous-input 959,31739 +(defun pg-next-input 973,32202 +(defun pg-delete-input 978,32324 +(defun pg-get-old-input 991,32662 +(defun pg-restore-input 1005,33053 +(defun pg-search-start 1016,33343 +(defun pg-regexp-arg 1028,33835 +(defun pg-search-arg 1040,34283 +(defun pg-previous-matching-input-string-position 1054,34700 +(defun pg-previous-matching-input 1081,35865 +(defun pg-next-matching-input 1100,36715 +(defvar pg-matching-input-from-input-string 1108,37098 +(defun pg-previous-matching-input-from-input 1112,37212 +(defun pg-next-matching-input-from-input 1130,37977 +(defun pg-add-to-input-history 1141,38356 +(defun pg-remove-from-input-history 1153,38809 +(defun pg-clear-input-ring 1164,39189 +(define-key proof-mode-map 1181,39659 +(define-key proof-mode-map 1182,39719 +(defun pg-protected-undo 1184,39791 +(defun pg-protected-undo-1 1214,41085 +(defun next-undo-elt 1245,42522 +(defvar proof-autosend-timer 1272,43478 +(deflocal proof-autosend-modified-tick 1274,43539 +(defun proof-autosend-enable 1278,43661 +(defun proof-autosend-delay 1292,44204 +(defun proof-autosend-loop 1296,44337 +(defun proof-autosend-loop-all 1310,44897 +(defun proof-autosend-loop-next 1334,45677 + +generic/pg-vars.el,1500 (defvar proof-assistant-cusgrp 22,389 (defvar proof-assistant-internals-cusgrp 28,649 (defvar proof-assistant 34,919 @@ -1153,10 +1166,11 @@ generic/pg-vars.el,1451 (defvar proof-nesting-depth 215,7790 (defvar proof-last-theorem-dependencies 222,8025 (defvar proof-autosend-running 226,8187 -(defcustom proof-general-name 236,8460 -(defcustom proof-general-home-page241,8617 -(defcustom proof-unnamed-theorem-name247,8777 -(defcustom proof-universal-keys253,8961 +(defvar proof-next-command-on-new-line 231,8386 +(defcustom proof-general-name 242,8620 +(defcustom proof-general-home-page247,8777 +(defcustom proof-unnamed-theorem-name253,8937 +(defcustom proof-universal-keys259,9121 generic/pg-xml.el,1177 (defalias 'pg-xml-error pg-xml-error18,381 @@ -1275,86 +1289,86 @@ generic/proof-config.el,7744 (defcustom proof-shell-auto-terminate-commands 805,29809 (defcustom proof-shell-pre-sync-init-cmd 814,30214 (defcustom proof-shell-init-cmd 828,30772 -(defcustom proof-shell-init-hook 840,31301 -(defcustom proof-shell-restart-cmd 845,31440 -(defcustom proof-shell-quit-cmd 850,31595 -(defcustom proof-shell-quit-timeout 855,31762 -(defcustom proof-shell-cd-cmd 864,32153 -(defcustom proof-shell-start-silent-cmd 881,32824 -(defcustom proof-shell-stop-silent-cmd 890,33200 -(defcustom proof-shell-silent-threshold 899,33535 -(defcustom proof-shell-inform-file-processed-cmd 907,33869 -(defcustom proof-shell-inform-file-retracted-cmd 928,34797 -(defcustom proof-auto-multiple-files 956,36069 -(defcustom proof-cannot-reopen-processed-files 971,36790 -(defcustom proof-shell-require-command-regexp 985,37456 -(defcustom proof-done-advancing-require-function 996,37918 -(defcustom proof-shell-annotated-prompt-regexp 1008,38278 -(defcustom proof-shell-error-regexp 1023,38843 -(defcustom proof-shell-truncate-before-error 1043,39645 -(defcustom pg-next-error-regexp 1057,40184 -(defcustom pg-next-error-filename-regexp 1072,40793 -(defcustom pg-next-error-extract-filename 1096,41826 -(defcustom proof-shell-interrupt-regexp 1103,42069 -(defcustom proof-shell-proof-completed-regexp 1117,42664 -(defcustom proof-shell-clear-response-regexp 1130,43172 -(defcustom proof-shell-clear-goals-regexp 1142,43624 -(defcustom proof-shell-start-goals-regexp 1154,44070 -(defcustom proof-shell-end-goals-regexp 1162,44437 -(defcustom proof-shell-eager-annotation-start 1176,45010 -(defcustom proof-shell-eager-annotation-start-length 1199,46029 -(defcustom proof-shell-eager-annotation-end 1210,46455 -(defcustom proof-shell-strip-output-markup 1226,47130 -(defcustom proof-shell-assumption-regexp 1235,47515 -(defcustom proof-shell-process-file 1245,47919 -(defcustom proof-shell-retract-files-regexp 1271,48995 -(defcustom proof-shell-compute-new-files-list 1284,49483 -(defcustom pg-special-char-regexp 1299,50050 -(defcustom proof-shell-set-elisp-variable-regexp 1304,50194 -(defcustom proof-shell-match-pgip-cmd 1342,51860 -(defcustom proof-shell-issue-pgip-cmd 1356,52342 -(defcustom proof-use-pgip-askprefs 1361,52507 -(defcustom proof-shell-query-dependencies-cmd 1369,52854 -(defcustom proof-shell-theorem-dependency-list-regexp 1376,53114 -(defcustom proof-shell-theorem-dependency-list-split 1392,53774 -(defcustom proof-shell-show-dependency-cmd 1401,54197 -(defcustom proof-shell-trace-output-regexp 1423,55103 -(defcustom proof-shell-thms-output-regexp 1441,55697 -(defcustom proof-tokens-activate-command 1454,56080 -(defcustom proof-tokens-deactivate-command 1461,56320 -(defcustom proof-tokens-extra-modes 1468,56565 -(defcustom proof-shell-unicode 1483,57070 -(defcustom proof-shell-filename-escapes 1492,57460 -(defcustom proof-shell-process-connection-type 1509,58140 -(defcustom proof-shell-strip-crs-from-input 1515,58331 -(defcustom proof-shell-strip-crs-from-output 1527,58814 -(defcustom proof-shell-insert-hook 1535,59182 -(defcustom proof-script-preprocess 1576,61142 -(defcustom proof-shell-handle-delayed-output-hook1582,61293 -(defcustom proof-shell-handle-error-or-interrupt-hook1588,61508 -(defcustom proof-shell-pre-interrupt-hook1606,62254 -(defcustom proof-shell-handle-output-system-specific 1614,62525 -(defcustom proof-state-change-hook 1637,63498 -(defcustom proof-shell-syntax-table-entries 1647,63891 -(defgroup proof-goals 1665,64262 -(defcustom pg-subterm-first-special-char 1670,64383 -(defcustom pg-subterm-anns-use-stack 1678,64695 -(defcustom pg-goals-change-goal 1687,64994 -(defcustom pbp-goal-command 1692,65110 -(defcustom pbp-hyp-command 1697,65266 -(defcustom pg-subterm-help-cmd 1702,65428 -(defcustom pg-goals-error-regexp 1709,65664 -(defcustom proof-shell-result-start 1714,65824 -(defcustom proof-shell-result-end 1720,66058 -(defcustom pg-subterm-start-char 1726,66271 -(defcustom pg-subterm-sep-char 1737,66745 -(defcustom pg-subterm-end-char 1743,66924 -(defcustom pg-topterm-regexp 1749,67081 -(defcustom proof-goals-font-lock-keywords 1764,67681 -(defcustom proof-response-font-lock-keywords 1772,68040 -(defcustom proof-shell-font-lock-keywords 1780,68402 -(defcustom pg-before-fontify-output-hook 1791,68916 -(defcustom pg-after-fontify-output-hook 1799,69277 +(defcustom proof-shell-init-hook 840,31318 +(defcustom proof-shell-restart-cmd 845,31457 +(defcustom proof-shell-quit-cmd 850,31612 +(defcustom proof-shell-quit-timeout 855,31779 +(defcustom proof-shell-cd-cmd 864,32170 +(defcustom proof-shell-start-silent-cmd 881,32841 +(defcustom proof-shell-stop-silent-cmd 890,33217 +(defcustom proof-shell-silent-threshold 899,33552 +(defcustom proof-shell-inform-file-processed-cmd 907,33886 +(defcustom proof-shell-inform-file-retracted-cmd 928,34814 +(defcustom proof-auto-multiple-files 956,36086 +(defcustom proof-cannot-reopen-processed-files 971,36807 +(defcustom proof-shell-require-command-regexp 985,37473 +(defcustom proof-done-advancing-require-function 996,37935 +(defcustom proof-shell-annotated-prompt-regexp 1008,38295 +(defcustom proof-shell-error-regexp 1023,38860 +(defcustom proof-shell-truncate-before-error 1043,39662 +(defcustom pg-next-error-regexp 1057,40201 +(defcustom pg-next-error-filename-regexp 1072,40810 +(defcustom pg-next-error-extract-filename 1096,41843 +(defcustom proof-shell-interrupt-regexp 1103,42086 +(defcustom proof-shell-proof-completed-regexp 1117,42681 +(defcustom proof-shell-clear-response-regexp 1130,43189 +(defcustom proof-shell-clear-goals-regexp 1142,43641 +(defcustom proof-shell-start-goals-regexp 1154,44087 +(defcustom proof-shell-end-goals-regexp 1162,44454 +(defcustom proof-shell-eager-annotation-start 1176,45027 +(defcustom proof-shell-eager-annotation-start-length 1199,46046 +(defcustom proof-shell-eager-annotation-end 1210,46472 +(defcustom proof-shell-strip-output-markup 1226,47147 +(defcustom proof-shell-assumption-regexp 1235,47532 +(defcustom proof-shell-process-file 1245,47936 +(defcustom proof-shell-retract-files-regexp 1271,49012 +(defcustom proof-shell-compute-new-files-list 1284,49500 +(defcustom pg-special-char-regexp 1299,50067 +(defcustom proof-shell-set-elisp-variable-regexp 1304,50211 +(defcustom proof-shell-match-pgip-cmd 1342,51877 +(defcustom proof-shell-issue-pgip-cmd 1356,52359 +(defcustom proof-use-pgip-askprefs 1361,52524 +(defcustom proof-shell-query-dependencies-cmd 1369,52871 +(defcustom proof-shell-theorem-dependency-list-regexp 1376,53131 +(defcustom proof-shell-theorem-dependency-list-split 1392,53791 +(defcustom proof-shell-show-dependency-cmd 1401,54214 +(defcustom proof-shell-trace-output-regexp 1423,55120 +(defcustom proof-shell-thms-output-regexp 1441,55714 +(defcustom proof-tokens-activate-command 1454,56097 +(defcustom proof-tokens-deactivate-command 1461,56337 +(defcustom proof-tokens-extra-modes 1468,56582 +(defcustom proof-shell-unicode 1483,57087 +(defcustom proof-shell-filename-escapes 1492,57477 +(defcustom proof-shell-process-connection-type 1509,58157 +(defcustom proof-shell-strip-crs-from-input 1515,58348 +(defcustom proof-shell-strip-crs-from-output 1527,58831 +(defcustom proof-shell-insert-hook 1535,59199 +(defcustom proof-script-preprocess 1576,61159 +(defcustom proof-shell-handle-delayed-output-hook1582,61310 +(defcustom proof-shell-handle-error-or-interrupt-hook1588,61525 +(defcustom proof-shell-pre-interrupt-hook1606,62271 +(defcustom proof-shell-handle-output-system-specific 1614,62542 +(defcustom proof-state-change-hook 1637,63515 +(defcustom proof-shell-syntax-table-entries 1647,63908 +(defgroup proof-goals 1665,64279 +(defcustom pg-subterm-first-special-char 1670,64400 +(defcustom pg-subterm-anns-use-stack 1678,64712 +(defcustom pg-goals-change-goal 1687,65011 +(defcustom pbp-goal-command 1692,65127 +(defcustom pbp-hyp-command 1697,65283 +(defcustom pg-subterm-help-cmd 1702,65445 +(defcustom pg-goals-error-regexp 1709,65681 +(defcustom proof-shell-result-start 1714,65841 +(defcustom proof-shell-result-end 1720,66075 +(defcustom pg-subterm-start-char 1726,66288 +(defcustom pg-subterm-sep-char 1737,66762 +(defcustom pg-subterm-end-char 1743,66941 +(defcustom pg-topterm-regexp 1749,67098 +(defcustom proof-goals-font-lock-keywords 1764,67698 +(defcustom proof-response-font-lock-keywords 1772,68057 +(defcustom proof-shell-font-lock-keywords 1780,68419 +(defcustom pg-before-fontify-output-hook 1791,68933 +(defcustom pg-after-fontify-output-hook 1799,69294 generic/proof-depends.el,917 (defvar proof-thm-names-of-files 25,639 @@ -1385,7 +1399,7 @@ generic/proof-easy-config.el,192 (defun proof-easy-config-check-setup 52,2135 (defmacro proof-easy-config 84,3465 -generic/proof-faces.el,1595 +generic/proof-faces.el,1809 (defgroup proof-faces 29,809 (defconst pg-defface-window-systems36,989 (defmacro proof-face-specs 49,1551 @@ -1400,29 +1414,33 @@ generic/proof-faces.el,1595 (defface proof-debug-message-face134,4111 (defface proof-boring-face142,4310 (defface proof-mouse-highlight-face150,4502 -(defface proof-highlight-dependent-face158,4720 -(defface proof-highlight-dependency-face166,4927 -(defface proof-active-area-face174,5124 -(defface proof-script-sticky-error-face182,5436 -(defface proof-script-highlight-error-face190,5665 -(defconst proof-face-compat-doc 202,6010 -(defconst proof-queue-face 203,6090 -(defconst proof-locked-face 204,6158 -(defconst proof-declaration-name-face 205,6228 -(defconst proof-tacticals-name-face 206,6318 -(defconst proof-tactics-name-face 207,6404 -(defconst proof-error-face 208,6486 -(defconst proof-script-sticky-error-face 209,6554 -(defconst proof-script-highlight-error-face 210,6650 -(defconst proof-warning-face 211,6752 -(defconst proof-eager-annotation-face 212,6824 -(defconst proof-debug-message-face 213,6914 -(defconst proof-boring-face 214,6998 -(defconst proof-mouse-highlight-face 215,7068 -(defconst proof-highlight-dependent-face 216,7156 -(defconst proof-highlight-dependency-face 217,7252 -(defconst proof-active-area-face 218,7350 -(defconst proof-script-error-face 219,7430 +(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 generic/proof-indent.el,219 (defun proof-indent-indent 19,449 @@ -1436,372 +1454,381 @@ generic/proof-maths-menu.el,83 (defun proof-maths-menu-set-global 32,906 (defun proof-maths-menu-enable 46,1357 -generic/proof-menu.el,2074 +generic/proof-menu.el,2168 (defvar proof-display-some-buffers-count 36,816 (defun proof-display-some-buffers 38,861 (defun proof-menu-define-keys 95,2988 -(defun proof-menu-define-main 153,5808 -(defvar proof-menu-favourites 162,5993 -(defvar proof-menu-settings 165,6100 -(defun proof-menu-define-specific 169,6189 -(defun proof-assistant-menu-update 212,7451 -(defvar proof-help-menu226,7884 -(defvar proof-show-hide-menu234,8154 -(defvar proof-buffer-menu245,8578 -(defun proof-keep-response-history 308,10894 -(defconst proof-quick-opts-menu316,11204 -(defun proof-quick-opts-vars 528,19836 -(defun proof-quick-opts-changed-from-defaults-p 560,20776 -(defun proof-quick-opts-changed-from-saved-p 564,20881 -(defun proof-quick-opts-save 575,21232 -(defun proof-quick-opts-reset 580,21400 -(defconst proof-config-menu592,21668 -(defconst proof-advanced-menu599,21847 -(defvar proof-menu617,22531 -(defun proof-main-menu 626,22813 -(defun proof-aux-menu 638,23152 -(defun proof-menu-define-favourites-menu 654,23498 -(defun proof-def-favourite 674,24147 -(defvar proof-make-favourite-cmd-history 701,25140 -(defvar proof-make-favourite-menu-history 704,25225 -(defun proof-save-favourites 707,25311 -(defun proof-del-favourite 712,25459 -(defun proof-read-favourite 729,26015 -(defun proof-add-favourite 753,26789 -(defun proof-menu-define-settings-menu 780,27834 -(defun proof-menu-entry-name 813,28965 -(defun proof-menu-entry-for-setting 823,29315 -(defun proof-settings-vars 842,29847 -(defun proof-settings-changed-from-defaults-p 847,30024 -(defun proof-settings-changed-from-saved-p 851,30130 -(defun proof-settings-save 855,30233 -(defun proof-settings-reset 860,30400 -(defun proof-assistant-invisible-command-ifposs 865,30563 -(defun proof-maybe-askprefs 887,31533 -(defun proof-assistant-settings-cmd 893,31726 -(defun proof-assistant-settings-cmds 901,32010 -(defvar proof-assistant-format-table911,32352 -(defun proof-assistant-format-bool 919,32722 -(defun proof-assistant-format-int 922,32835 -(defun proof-assistant-format-string 925,32927 -(defun proof-assistant-format 928,33025 +(defun proof-menu-define-main 153,5813 +(defvar proof-menu-favourites 162,5998 +(defvar proof-menu-settings 165,6105 +(defun proof-menu-define-specific 169,6194 +(defun proof-assistant-menu-update 212,7456 +(defvar proof-help-menu226,7889 +(defvar proof-show-hide-menu234,8159 +(defvar proof-buffer-menu245,8583 +(defun proof-keep-response-history 308,10899 +(defconst proof-quick-opts-menu316,11209 +(defun proof-quick-opts-vars 534,20115 +(defun proof-quick-opts-changed-from-defaults-p 566,21055 +(defun proof-quick-opts-changed-from-saved-p 570,21160 +(defun proof-set-document-centred 578,21316 +(defun proof-set-non-document-centred 591,21742 +(defun proof-quick-opts-save 610,22453 +(defun proof-quick-opts-reset 615,22621 +(defconst proof-config-menu627,22889 +(defconst proof-advanced-menu634,23068 +(defvar proof-menu652,23752 +(defun proof-main-menu 661,24034 +(defun proof-aux-menu 673,24373 +(defun proof-menu-define-favourites-menu 689,24719 +(defun proof-def-favourite 709,25368 +(defvar proof-make-favourite-cmd-history 736,26361 +(defvar proof-make-favourite-menu-history 739,26446 +(defun proof-save-favourites 742,26532 +(defun proof-del-favourite 747,26680 +(defun proof-read-favourite 764,27236 +(defun proof-add-favourite 788,28010 +(defun proof-menu-define-settings-menu 815,29055 +(defun proof-menu-entry-name 848,30186 +(defun proof-menu-entry-for-setting 858,30536 +(defun proof-settings-vars 877,31068 +(defun proof-settings-changed-from-defaults-p 882,31245 +(defun proof-settings-changed-from-saved-p 886,31351 +(defun proof-settings-save 890,31454 +(defun proof-settings-reset 895,31621 +(defun proof-assistant-invisible-command-ifposs 900,31784 +(defun proof-maybe-askprefs 922,32754 +(defun proof-assistant-settings-cmd 928,32947 +(defun proof-assistant-settings-cmds 936,33231 +(defvar proof-assistant-format-table946,33573 +(defun proof-assistant-format-bool 954,33943 +(defun proof-assistant-format-int 957,34056 +(defun proof-assistant-format-string 960,34148 +(defun proof-assistant-format 963,34246 generic/proof-mmm.el,70 (defun proof-mmm-set-global 43,1439 (defun proof-mmm-enable 58,1978 -generic/proof-script.el,5425 +generic/proof-script.el,5496 (deflocal proof-active-buffer-fake-minor-mode 46,1414 (deflocal proof-script-buffer-file-name 49,1540 (deflocal pg-script-portions 56,1950 (defun proof-next-element-count 66,2170 (defun proof-element-id 72,2412 (defun proof-next-element-id 76,2581 -(deflocal proof-locked-span 112,3907 -(deflocal proof-queue-span 119,4173 -(deflocal proof-overlay-arrow 128,4659 -(defun proof-span-give-warning 134,4786 -(defun proof-span-read-only 140,4966 -(defun proof-strict-read-only 149,5339 -(defsubst proof-set-queue-endpoints 159,5717 -(defun proof-set-overlay-arrow 163,5858 -(defsubst proof-set-locked-endpoints 174,6196 -(defsubst proof-detach-queue 179,6372 -(defsubst proof-detach-locked 184,6511 -(defsubst proof-set-queue-start 191,6736 -(defsubst proof-set-locked-end 195,6862 -(defsubst proof-set-queue-end 207,7332 -(defun proof-init-segmentation 218,7629 -(defun proof-colour-locked 250,9024 -(defun proof-colour-locked-span 257,9297 -(defun proof-sticky-errors 263,9570 -(defun proof-restart-buffers 276,9986 -(defun proof-script-buffers-with-spans 298,10805 -(defun proof-script-remove-all-spans-and-deactivate 308,11161 -(defun proof-script-clear-queue-spans-on-error 312,11351 -(defun proof-script-delete-spans 338,12368 -(defun proof-script-delete-secondary-spans 343,12567 -(defun proof-unprocessed-begin 356,12856 -(defun proof-script-end 364,13110 -(defun proof-queue-or-locked-end 373,13420 -(defun proof-locked-region-full-p 392,14013 -(defun proof-locked-region-empty-p 401,14285 -(defun proof-only-whitespace-to-locked-region-p 405,14435 -(defun proof-in-locked-region-p 415,14784 -(defun proof-goto-end-of-locked 427,15041 -(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 444,15800 -(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 456,16314 -(defun proof-end-of-locked-visible-p 469,16898 -(defvar pg-idioms 488,17491 -(defun pg-clear-script-portions 491,17587 -(defun pg-remove-element 497,17822 -(defun pg-get-element 505,18125 -(defun pg-add-element 515,18440 -(defun pg-set-element-span-invisible 563,20419 -(defun pg-open-invisible-span 567,20579 -(defun pg-make-element-invisible 572,20750 -(defun pg-make-element-visible 577,20961 -(defun pg-toggle-element-span-visibility 582,21155 -(defun pg-toggle-element-visibility 588,21318 -(defun pg-show-all-portions 594,21581 -(defun pg-show-all-proofs 613,22289 -(defun pg-hide-all-proofs 618,22417 -(defun pg-add-proof-element 623,22548 -(defun pg-span-name 638,23319 -(defvar pg-span-context-menu-keymap659,24019 -(defun pg-last-output-displayform 666,24257 -(defun pg-set-span-helphighlights 689,25148 -(defun pg-delete-self-modification-hook 738,26962 -(defun proof-complete-buffer-atomic 749,27235 -(defun proof-register-possibly-new-processed-file790,29147 -(defun proof-query-save-this-buffer-p 836,31021 -(defun proof-inform-prover-file-retracted 841,31246 -(defun proof-auto-retract-dependencies 861,32097 -(defun proof-unregister-buffer-file-name 915,34647 -(defun proof-protected-process-or-retract 961,36472 -(defun proof-deactivate-scripting-auto 988,37642 -(defun proof-deactivate-scripting 997,38000 -(defun proof-activate-scripting 1130,43232 -(defun proof-toggle-active-scripting 1230,47747 -(defun proof-done-advancing 1269,48992 -(defun proof-done-advancing-comment 1348,51977 -(defun proof-done-advancing-save 1382,53353 -(defun proof-make-goalsave1470,56717 -(defun proof-get-name-from-goal 1488,57548 -(defun proof-done-advancing-autosave 1508,58573 -(defun proof-done-advancing-other 1573,61117 -(defun proof-segment-up-to-parser 1602,62046 -(defun proof-script-generic-parse-find-comment-end 1671,64312 -(defun proof-script-generic-parse-cmdend 1680,64726 -(defun proof-script-generic-parse-cmdstart 1731,66622 -(defun proof-script-generic-parse-sexp 1770,68222 -(defun proof-semis-to-vanillas 1782,68688 -(defun proof-script-next-command-advance 1835,70361 -(defun proof-assert-until-point 1854,70860 -(defun proof-assert-electric-terminator 1869,71487 -(defun proof-assert-semis 1904,72872 -(defun proof-retract-before-change 1918,73613 -(defun proof-insert-pbp-command 1938,74209 -(defun proof-insert-sendback-command 1953,74709 -(defun proof-done-retracting 1979,75612 -(defun proof-setup-retract-action 2014,77064 -(defun proof-last-goal-or-goalsave 2025,77601 -(defun proof-retract-target 2049,78513 -(defun proof-retract-until-point-interactive 2133,81977 -(defun proof-retract-until-point 2142,82384 -(define-derived-mode proof-mode 2189,84254 -(defun proof-script-set-visited-file-name 2225,85636 -(defun proof-script-set-buffer-hooks 2247,86649 -(defun proof-script-kill-buffer-fn 2255,87067 -(defun proof-config-done-related 2287,88384 -(defun proof-generic-goal-command-p 2352,90869 -(defun proof-generic-state-preserving-p 2357,91082 -(defun proof-generic-count-undos 2366,91599 -(defun proof-generic-find-and-forget 2397,92727 -(defconst proof-script-important-settings2448,94499 -(defun proof-config-done 2463,95045 -(defun proof-setup-parsing-mechanism 2524,97059 -(defun proof-setup-imenu 2548,98131 -(deflocal proof-segment-up-to-cache 2575,98909 -(deflocal proof-segment-up-to-cache-start 2576,98950 -(deflocal proof-last-edited-low-watermark 2577,98995 -(defun proof-segment-up-to-using-cache 2587,99482 -(defun proof-segment-cache-contents-for 2616,100616 -(defun proof-script-after-change-function 2628,100985 -(defun proof-script-set-after-change-functions 2640,101492 - -generic/proof-shell.el,3597 +(deflocal proof-locked-span 112,3885 +(deflocal proof-queue-span 119,4151 +(deflocal proof-overlay-arrow 128,4637 +(defun proof-span-give-warning 134,4764 +(defun proof-span-read-only 140,4944 +(defun proof-strict-read-only 149,5317 +(defsubst proof-set-queue-endpoints 159,5695 +(defun proof-set-overlay-arrow 163,5836 +(defsubst proof-set-locked-endpoints 174,6174 +(defsubst proof-detach-queue 179,6350 +(defsubst proof-detach-locked 184,6489 +(defsubst proof-set-queue-start 191,6714 +(defsubst proof-set-locked-end 195,6840 +(defsubst proof-set-queue-end 207,7310 +(defun proof-init-segmentation 218,7607 +(defun proof-colour-locked 248,8858 +(defun proof-colour-locked-span 255,9131 +(defun proof-sticky-errors 261,9404 +(defun proof-restart-buffers 274,9820 +(defun proof-script-buffers-with-spans 296,10639 +(defun proof-script-remove-all-spans-and-deactivate 306,10995 +(defun proof-script-clear-queue-spans-on-error 310,11185 +(defun proof-script-delete-spans 336,12202 +(defun proof-script-delete-secondary-spans 341,12401 +(defun proof-unprocessed-begin 354,12690 +(defun proof-script-end 362,12944 +(defun proof-queue-or-locked-end 371,13254 +(defun proof-locked-region-full-p 390,13847 +(defun proof-locked-region-empty-p 399,14119 +(defun proof-only-whitespace-to-locked-region-p 403,14269 +(defun proof-in-locked-region-p 413,14618 +(defun proof-goto-end-of-locked 425,14875 +(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 442,15634 +(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 453,16115 +(defun proof-end-of-locked-visible-p 465,16655 +(defconst pg-idioms 484,17248 +(defconst pg-all-idioms 487,17344 +(defun pg-clear-script-portions 491,17465 +(defun pg-remove-element 497,17700 +(defun pg-get-element 505,18003 +(defun pg-add-element 515,18318 +(defun pg-invisible-prop 563,20297 +(defun pg-set-element-span-invisible 568,20498 +(defun pg-toggle-element-span-visibility 581,21064 +(defun pg-open-invisible-span 586,21225 +(defun pg-make-element-invisible 591,21396 +(defun pg-make-element-visible 596,21607 +(defun pg-toggle-element-visibility 601,21801 +(defun pg-show-all-portions 607,22064 +(defun pg-show-all-proofs 626,22772 +(defun pg-hide-all-proofs 631,22900 +(defun pg-add-proof-element 636,23031 +(defun pg-span-name 651,23818 +(defvar pg-span-context-menu-keymap684,25025 +(defun pg-last-output-displayform 691,25263 +(defun pg-set-span-helphighlights 714,26154 +(defun proof-complete-buffer-atomic 772,28131 +(defun proof-register-possibly-new-processed-file801,29401 +(defun proof-query-save-this-buffer-p 847,31275 +(defun proof-inform-prover-file-retracted 852,31500 +(defun proof-auto-retract-dependencies 872,32351 +(defun proof-unregister-buffer-file-name 926,34901 +(defun proof-protected-process-or-retract 972,36726 +(defun proof-deactivate-scripting-auto 999,37896 +(defun proof-deactivate-scripting 1008,38254 +(defun proof-activate-scripting 1138,43398 +(defun proof-toggle-active-scripting 1239,47918 +(defun proof-done-advancing 1278,49163 +(defun proof-done-advancing-comment 1357,52148 +(defun proof-done-advancing-save 1391,53534 +(defun proof-make-goalsave1479,56898 +(defun proof-get-name-from-goal 1497,57763 +(defun proof-done-advancing-autosave 1517,58788 +(defun proof-done-advancing-other 1581,61284 +(defun proof-segment-up-to-parser 1610,62248 +(defun proof-script-generic-parse-find-comment-end 1679,64514 +(defun proof-script-generic-parse-cmdend 1688,64928 +(defun proof-script-generic-parse-cmdstart 1739,66824 +(defun proof-script-generic-parse-sexp 1778,68424 +(defun proof-semis-to-vanillas 1790,68890 +(defun proof-next-command-new-line 1843,70563 +(defun proof-script-next-command-advance 1848,70769 +(defun proof-assert-until-point 1867,71269 +(defun proof-assert-electric-terminator 1882,71896 +(defun proof-assert-semis 1925,73528 +(defun proof-retract-before-change 1939,74269 +(defun proof-insert-pbp-command 1959,74865 +(defun proof-insert-sendback-command 1974,75368 +(defun proof-done-retracting 2000,76271 +(defun proof-setup-retract-action 2035,77725 +(defun proof-last-goal-or-goalsave 2047,78330 +(defun proof-retract-target 2071,79242 +(defun proof-retract-until-point-interactive 2150,82495 +(defun proof-retract-until-point 2159,82902 +(define-derived-mode proof-mode 2214,84910 +(defun proof-script-set-visited-file-name 2250,86292 +(defun proof-script-set-buffer-hooks 2272,87305 +(defun proof-script-kill-buffer-fn 2280,87723 +(defun proof-config-done-related 2312,89040 +(defun proof-generic-goal-command-p 2377,91525 +(defun proof-generic-state-preserving-p 2382,91738 +(defun proof-generic-count-undos 2391,92255 +(defun proof-generic-find-and-forget 2422,93383 +(defconst proof-script-important-settings2473,95155 +(defun proof-config-done 2488,95701 +(defun proof-setup-parsing-mechanism 2555,97866 +(defun proof-setup-imenu 2579,98938 +(deflocal proof-segment-up-to-cache 2606,99716 +(deflocal proof-segment-up-to-cache-start 2607,99757 +(deflocal proof-last-edited-low-watermark 2608,99802 +(defun proof-segment-up-to-using-cache 2618,100289 +(defun proof-segment-cache-contents-for 2650,101534 +(defun proof-script-after-change-function 2662,101903 +(defun proof-script-set-after-change-functions 2674,102410 + +generic/proof-shell.el,3598 (defvar proof-marker 34,744 (defvar proof-action-list 37,840 -(defsubst proof-shell-invoke-callback 56,1512 -(defvar proof-shell-last-goals-output 70,2004 -(defvar proof-shell-last-response-output 73,2084 -(defvar proof-shell-delayed-output-start 76,2171 -(defvar proof-shell-delayed-output-end 80,2353 -(defvar proof-shell-delayed-output-flags 84,2533 -(defvar proof-shell-interrupt-pending 87,2658 -(defcustom proof-shell-active-scripting-indicator98,2953 -(defun proof-shell-ready-prover 144,4312 -(defsubst proof-shell-live-buffer 158,4851 -(defun proof-shell-available-p 165,5090 -(defun proof-grab-lock 171,5312 -(defun proof-release-lock 181,5741 -(defcustom proof-shell-fiddle-frames 191,5915 -(defun proof-shell-set-text-representation 196,6073 -(defun proof-shell-start 204,6401 -(defvar proof-shell-kill-function-hooks 378,12211 -(defun proof-shell-kill-function 381,12309 -(defun proof-shell-clear-state 434,14204 -(defun proof-shell-exit 450,14679 -(defun proof-shell-bail-out 463,15183 -(defun proof-shell-restart 473,15705 -(defvar proof-shell-urgent-message-marker 514,17077 -(defvar proof-shell-urgent-message-scanner 517,17198 -(defun proof-shell-handle-error-output 521,17383 -(defun proof-shell-handle-error-or-interrupt 547,18245 -(defun proof-shell-error-or-interrupt-action 590,19994 -(defun proof-goals-pos 613,20873 -(defun proof-pbp-focus-on-first-goal 618,21084 -(defsubst proof-shell-string-match-safe 630,21500 -(defun proof-shell-handle-immediate-output 634,21661 -(defun proof-interrupt-process 701,24268 -(defun proof-shell-insert 735,25501 -(defun proof-shell-action-list-item 786,27327 -(defun proof-shell-set-silent 791,27569 -(defun proof-shell-start-silent-item 797,27788 -(defun proof-shell-clear-silent 803,27977 -(defun proof-shell-stop-silent-item 809,28199 -(defsubst proof-shell-should-be-silent 815,28388 -(defsubst proof-shell-insert-action-item 826,28898 -(defsubst proof-shell-slurp-comments 830,29073 -(defun proof-add-to-queue 841,29478 -(defun proof-start-queue 899,31502 -(defun proof-extend-queue 910,31896 -(defun proof-shell-exec-loop 924,32364 -(defun proof-shell-insert-loopback-cmd 992,34667 -(defun proof-shell-process-urgent-message 1017,35831 -(defun proof-shell-process-urgent-message-default 1066,37551 -(defun proof-shell-process-urgent-message-trace 1082,38135 -(defun proof-shell-process-urgent-message-retract 1095,38694 -(defun proof-shell-process-urgent-message-elisp 1116,39542 -(defun proof-shell-process-urgent-message-thmdeps 1131,40037 -(defun proof-shell-strip-eager-annotations 1145,40416 -(defun proof-shell-filter 1161,40916 -(defun proof-shell-filter-first-command 1261,44288 -(defun proof-shell-process-urgent-messages 1276,44831 -(defun proof-shell-filter-manage-output 1326,46397 -(defsubst proof-shell-display-output-as-response 1358,47644 -(defun proof-shell-handle-delayed-output 1364,47939 -(defvar pg-last-tracing-output-time 1459,51398 -(defconst pg-slow-mode-duration 1462,51504 -(defconst pg-fast-tracing-mode-threshold 1465,51586 -(defvar pg-tracing-cleanup-timer 1468,51714 -(defun pg-tracing-tight-loop 1470,51753 -(defun pg-finish-tracing-display 1513,53465 -(defun proof-shell-wait 1531,53829 -(defun proof-done-invisible 1561,55034 -(defun proof-shell-invisible-command 1567,55204 -(defun proof-shell-invisible-cmd-get-result 1613,56739 -(defun proof-shell-invisible-command-invisible-result 1625,57175 -(defun pg-insert-last-output-as-comment 1645,57676 -(define-derived-mode proof-shell-mode 1664,58148 -(defconst proof-shell-important-settings1701,59175 -(defun proof-shell-config-done 1707,59290 - -generic/proof-site.el,503 +(defsubst proof-shell-invoke-callback 57,1594 +(defvar proof-shell-last-goals-output 71,2086 +(defvar proof-shell-last-response-output 74,2166 +(defvar proof-shell-delayed-output-start 77,2253 +(defvar proof-shell-delayed-output-end 81,2435 +(defvar proof-shell-delayed-output-flags 85,2615 +(defvar proof-shell-interrupt-pending 88,2740 +(defcustom proof-shell-active-scripting-indicator99,3035 +(defun proof-shell-ready-prover 151,4619 +(defsubst proof-shell-live-buffer 165,5158 +(defun proof-shell-available-p 172,5397 +(defun proof-grab-lock 178,5619 +(defun proof-release-lock 188,6048 +(defcustom proof-shell-fiddle-frames 198,6222 +(defun proof-shell-set-text-representation 203,6380 +(defun proof-shell-start 211,6708 +(defvar proof-shell-kill-function-hooks 385,12533 +(defun proof-shell-kill-function 388,12631 +(defun proof-shell-clear-state 441,14526 +(defun proof-shell-exit 457,15001 +(defun proof-shell-bail-out 470,15505 +(defun proof-shell-restart 480,16027 +(defvar proof-shell-urgent-message-marker 521,17399 +(defvar proof-shell-urgent-message-scanner 524,17520 +(defun proof-shell-handle-error-output 528,17705 +(defun proof-shell-handle-error-or-interrupt 554,18567 +(defun proof-shell-error-or-interrupt-action 597,20316 +(defun proof-goals-pos 624,21413 +(defun proof-pbp-focus-on-first-goal 629,21624 +(defsubst proof-shell-string-match-safe 641,22040 +(defun proof-shell-handle-immediate-output 645,22201 +(defun proof-interrupt-process 712,24808 +(defun proof-shell-insert 746,26041 +(defun proof-shell-action-list-item 797,27867 +(defun proof-shell-set-silent 802,28109 +(defun proof-shell-start-silent-item 808,28328 +(defun proof-shell-clear-silent 814,28517 +(defun proof-shell-stop-silent-item 820,28739 +(defsubst proof-shell-should-be-silent 826,28928 +(defsubst proof-shell-insert-action-item 837,29438 +(defsubst proof-shell-slurp-comments 841,29613 +(defun proof-add-to-queue 852,30018 +(defun proof-start-queue 910,32042 +(defun proof-extend-queue 921,32436 +(defun proof-shell-exec-loop 935,32904 +(defun proof-shell-insert-loopback-cmd 1003,35207 +(defun proof-shell-process-urgent-message 1028,36371 +(defun proof-shell-process-urgent-message-default 1077,38091 +(defun proof-shell-process-urgent-message-trace 1093,38675 +(defun proof-shell-process-urgent-message-retract 1106,39234 +(defun proof-shell-process-urgent-message-elisp 1127,40082 +(defun proof-shell-process-urgent-message-thmdeps 1142,40577 +(defun proof-shell-strip-eager-annotations 1156,40956 +(defun proof-shell-filter 1172,41456 +(defun proof-shell-filter-first-command 1272,44828 +(defun proof-shell-process-urgent-messages 1287,45371 +(defun proof-shell-filter-manage-output 1337,46937 +(defsubst proof-shell-display-output-as-response 1369,48184 +(defun proof-shell-handle-delayed-output 1375,48479 +(defvar pg-last-tracing-output-time 1470,51938 +(defconst pg-slow-mode-duration 1473,52044 +(defconst pg-fast-tracing-mode-threshold 1476,52126 +(defvar pg-tracing-cleanup-timer 1479,52254 +(defun pg-tracing-tight-loop 1481,52293 +(defun pg-finish-tracing-display 1524,54005 +(defun proof-shell-wait 1542,54369 +(defun proof-done-invisible 1572,55574 +(defun proof-shell-invisible-command 1578,55744 +(defun proof-shell-invisible-cmd-get-result 1625,57336 +(defun proof-shell-invisible-command-invisible-result 1637,57772 +(defun pg-insert-last-output-as-comment 1657,58273 +(define-derived-mode proof-shell-mode 1676,58745 +(defconst proof-shell-important-settings1713,59772 +(defun proof-shell-config-done 1719,59887 + +generic/proof-site.el,665 (defconst proof-assistant-table-default26,771 -(defconst proof-general-short-version59,1824 -(defconst proof-general-version-year 65,2011 -(defgroup proof-general 72,2164 -(defgroup proof-general-internals 77,2272 -(defun proof-home-directory-fn 90,2660 -(defcustom proof-home-directory101,3032 -(defcustom proof-images-directory110,3398 -(defcustom proof-info-directory116,3600 -(defcustom proof-assistant-table145,4577 -(defcustom proof-assistants 180,5690 -(defun proof-ready-for-assistant 209,6846 +(defconst proof-general-short-version59,1766 +(defconst proof-general-version-year 65,1953 +(defgroup proof-general 72,2106 +(defgroup proof-general-internals 77,2214 +(defun proof-home-directory-fn 90,2602 +(defcustom proof-home-directory101,2974 +(defcustom proof-images-directory110,3340 +(defcustom proof-info-directory116,3542 +(defcustom proof-assistant-table145,4519 +(defcustom proof-assistants 182,5687 +(defun proof-ready-for-assistant 211,6841 +(defvar proof-general-configured-provers 263,9133 +(defun proof-chose-prover 333,11656 +(defun proofgeneral 338,11788 +(defun proof-visit-example-file 347,12106 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 170,5966 -(defun proof-splash-remove-buffer 187,6622 -(defvar proof-splash-seen 198,7010 -(defun proof-splash-insert-contents 201,7112 -(defun proof-splash-display-screen 241,8242 -(defalias 'pg-about pg-about277,9764 -(defun proof-splash-message 280,9830 -(defun proof-splash-timeout-waiter 293,10274 -(defvar proof-splash-old-frame-title-format 306,10832 -(defun proof-splash-set-frame-titles 308,10882 -(defun proof-splash-unset-frame-titles 317,11197 - -generic/proof-syntax.el,1237 +(defcustom proof-splash-enable 34,1008 +(defcustom proof-splash-time 39,1160 +(defcustom proof-splash-contents47,1444 +(defconst proof-splash-startup-msg91,3009 +(defconst proof-splash-welcome 100,3387 +(define-derived-mode proof-splash-mode 103,3491 +(define-key proof-splash-mode-map 109,3665 +(define-key proof-splash-mode-map 110,3717 +(defsubst proof-emacs-imagep 115,3844 +(defun proof-get-image 120,3969 +(defvar proof-splash-timeout-conf 142,4769 +(defun proof-splash-centre-spaces 145,4882 +(defun proof-splash-remove-screen 172,6038 +(defun proof-splash-remove-buffer 189,6694 +(defvar proof-splash-seen 200,7082 +(defun proof-splash-insert-contents 203,7184 +(defun proof-splash-display-screen 243,8314 +(defalias 'pg-about pg-about279,9836 +(defun proof-splash-message 282,9902 +(defun proof-splash-timeout-waiter 295,10346 +(defvar proof-splash-old-frame-title-format 308,10904 +(defun proof-splash-set-frame-titles 310,10954 +(defun proof-splash-unset-frame-titles 319,11269 + +generic/proof-syntax.el,1278 (defsubst proof-ids-to-regexp 22,517 (defsubst proof-anchor-regexp 29,755 (defconst proof-no-regexp 33,860 (defsubst proof-regexp-alt 36,951 -(defsubst proof-re-search-forward-region 45,1263 -(defsubst proof-search-forward 58,1761 -(defsubst proof-replace-regexp-in-string 65,2031 -(defsubst proof-re-search-forward 70,2282 -(defsubst proof-re-search-backward 75,2540 -(defsubst proof-re-search-forward-safe 80,2801 -(defsubst proof-string-match 86,3082 -(defsubst proof-string-match-safe 91,3311 -(defsubst proof-stringfn-match 95,3515 -(defsubst proof-looking-at 102,3778 -(defsubst proof-looking-at-safe 107,3965 -(defun proof-buffer-syntactic-context 116,4178 -(defsubst proof-looking-at-syntactic-context-default 137,5040 -(defun proof-looking-at-syntactic-context 146,5395 -(defun proof-inside-comment 155,5857 -(defun proof-inside-string 161,6030 -(defsubst proof-replace-string 171,6229 -(defsubst proof-replace-regexp 176,6433 -(defsubst proof-replace-regexp-nocasefold 181,6642 -(defvar proof-id 191,6930 -(defsubst proof-ids 197,7150 -(defun proof-zap-commas 204,7402 -(defadvice font-lock-fontify-keywords-region230,8288 -(defun proof-format 246,8884 -(defun proof-format-filename 265,9523 -(defun proof-insert 312,10925 +(defsubst proof-regexp-alt-list 45,1263 +(defsubst proof-re-search-forward-region 49,1398 +(defsubst proof-search-forward 62,1896 +(defsubst proof-replace-regexp-in-string 69,2166 +(defsubst proof-re-search-forward 74,2417 +(defsubst proof-re-search-backward 79,2675 +(defsubst proof-re-search-forward-safe 84,2936 +(defsubst proof-string-match 90,3217 +(defsubst proof-string-match-safe 95,3446 +(defsubst proof-stringfn-match 99,3650 +(defsubst proof-looking-at 106,3913 +(defsubst proof-looking-at-safe 111,4100 +(defun proof-buffer-syntactic-context 120,4313 +(defsubst proof-looking-at-syntactic-context-default 141,5175 +(defun proof-looking-at-syntactic-context 150,5530 +(defun proof-inside-comment 159,5992 +(defun proof-inside-string 165,6165 +(defsubst proof-replace-string 175,6364 +(defsubst proof-replace-regexp 180,6568 +(defsubst proof-replace-regexp-nocasefold 185,6777 +(defvar proof-id 195,7065 +(defsubst proof-ids 201,7285 +(defun proof-zap-commas 208,7537 +(defadvice font-lock-fontify-keywords-region234,8423 +(defun proof-format 250,9019 +(defun proof-format-filename 269,9658 +(defun proof-insert 316,11060 generic/proof-toolbar.el,2332 -(defun proof-toolbar-function 33,810 -(defun proof-toolbar-icon 37,957 -(defun proof-toolbar-enabler 41,1104 -(defun proof-toolbar-make-icon 50,1306 -(defun proof-toolbar-make-toolbar-items 59,1614 -(defvar proof-toolbar-map 84,2419 -(defun proof-toolbar-available-p 87,2518 -(defun proof-toolbar-setup 97,2824 -(defun proof-toolbar-enable 118,3681 -(defalias 'proof-toolbar-undo proof-toolbar-undo151,4739 -(defun proof-toolbar-undo-enable-p 153,4807 -(defalias 'proof-toolbar-delete proof-toolbar-delete160,4965 -(defun proof-toolbar-delete-enable-p 162,5046 -(defalias 'proof-toolbar-home proof-toolbar-home170,5228 -(defalias 'proof-toolbar-next proof-toolbar-next174,5295 -(defun proof-toolbar-next-enable-p 176,5366 -(defalias 'proof-toolbar-goto proof-toolbar-goto182,5482 -(defun proof-toolbar-goto-enable-p 184,5532 -(defalias 'proof-toolbar-retract proof-toolbar-retract189,5617 -(defun proof-toolbar-retract-enable-p 191,5674 -(defalias 'proof-toolbar-use proof-toolbar-use197,5793 -(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p198,5845 -(defalias 'proof-toolbar-restart proof-toolbar-restart202,5926 -(defalias 'proof-toolbar-goal proof-toolbar-goal206,5991 -(defalias 'proof-toolbar-qed proof-toolbar-qed210,6049 -(defun proof-toolbar-qed-enable-p 212,6098 -(defalias 'proof-toolbar-state proof-toolbar-state220,6260 -(defalias 'proof-toolbar-state-enable-p proof-toolbar-state-enable-p221,6303 -(defalias 'proof-toolbar-context proof-toolbar-context225,6382 -(defalias 'proof-toolbar-context-enable-p proof-toolbar-context-enable-p226,6428 -(defalias 'proof-toolbar-command proof-toolbar-command230,6509 -(defalias 'proof-toolbar-command-enable-p proof-toolbar-command-enable-p231,6565 -(defun proof-toolbar-help 235,6670 -(defalias 'proof-toolbar-find proof-toolbar-find241,6750 -(defalias 'proof-toolbar-find-enable-p proof-toolbar-find-enable-p242,6802 -(defalias 'proof-toolbar-info proof-toolbar-info246,6877 -(defalias 'proof-toolbar-info-enable-p proof-toolbar-info-enable-p247,6932 -(defalias 'proof-toolbar-visibility proof-toolbar-visibility251,7030 -(defun proof-toolbar-visibility-enable-p 253,7090 -(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt258,7204 -(defun proof-toolbar-interrupt-enable-p 259,7265 -(defun proof-toolbar-scripting-menu 267,7418 +(defun proof-toolbar-function 33,813 +(defun proof-toolbar-icon 37,960 +(defun proof-toolbar-enabler 41,1107 +(defun proof-toolbar-make-icon 50,1309 +(defun proof-toolbar-make-toolbar-items 59,1617 +(defvar proof-toolbar-map 85,2493 +(defun proof-toolbar-available-p 88,2592 +(defun proof-toolbar-setup 98,2898 +(defun proof-toolbar-enable 119,3755 +(defalias 'proof-toolbar-undo proof-toolbar-undo152,4813 +(defun proof-toolbar-undo-enable-p 154,4881 +(defalias 'proof-toolbar-delete proof-toolbar-delete161,5039 +(defun proof-toolbar-delete-enable-p 163,5120 +(defalias 'proof-toolbar-home proof-toolbar-home171,5302 +(defalias 'proof-toolbar-next proof-toolbar-next175,5369 +(defun proof-toolbar-next-enable-p 177,5440 +(defalias 'proof-toolbar-goto proof-toolbar-goto183,5556 +(defun proof-toolbar-goto-enable-p 185,5606 +(defalias 'proof-toolbar-retract proof-toolbar-retract190,5691 +(defun proof-toolbar-retract-enable-p 192,5748 +(defalias 'proof-toolbar-use proof-toolbar-use198,5867 +(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p199,5919 +(defalias 'proof-toolbar-restart proof-toolbar-restart203,6000 +(defalias 'proof-toolbar-goal proof-toolbar-goal207,6065 +(defalias 'proof-toolbar-qed proof-toolbar-qed211,6123 +(defun proof-toolbar-qed-enable-p 213,6172 +(defalias 'proof-toolbar-state proof-toolbar-state221,6334 +(defalias 'proof-toolbar-state-enable-p proof-toolbar-state-enable-p222,6377 +(defalias 'proof-toolbar-context proof-toolbar-context226,6456 +(defalias 'proof-toolbar-context-enable-p proof-toolbar-context-enable-p227,6502 +(defalias 'proof-toolbar-command proof-toolbar-command231,6583 +(defalias 'proof-toolbar-command-enable-p proof-toolbar-command-enable-p232,6639 +(defun proof-toolbar-help 236,6744 +(defalias 'proof-toolbar-find proof-toolbar-find242,6824 +(defalias 'proof-toolbar-find-enable-p proof-toolbar-find-enable-p243,6876 +(defalias 'proof-toolbar-info proof-toolbar-info247,6951 +(defalias 'proof-toolbar-info-enable-p proof-toolbar-info-enable-p248,7006 +(defalias 'proof-toolbar-visibility proof-toolbar-visibility252,7104 +(defun proof-toolbar-visibility-enable-p 254,7164 +(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt259,7278 +(defun proof-toolbar-interrupt-enable-p 260,7339 +(defun proof-toolbar-scripting-menu 268,7492 generic/proof-unicode-tokens.el,497 (defvar proof-unicode-tokens-initialised 31,827 @@ -1815,7 +1842,7 @@ generic/proof-unicode-tokens.el,497 (defun proof-unicode-tokens-activate-prover 133,4573 (defun proof-unicode-tokens-deactivate-prover 140,4819 -generic/proof-useropts.el,1676 +generic/proof-useropts.el,1575 (defgroup proof-user-options 21,559 (defun proof-set-value 29,738 (defcustom proof-electric-terminator-enable 62,1861 @@ -1834,66 +1861,64 @@ generic/proof-useropts.el,1676 (defcustom proof-colour-locked 187,6947 (defcustom proof-sticky-errors 195,7197 (defcustom proof-query-file-save-when-activating-scripting202,7414 -(defcustom proof-one-command-per-line218,8134 -(defcustom proof-prog-name-ask225,8358 -(defcustom proof-prog-name-guess231,8518 -(defcustom proof-tidy-response239,8783 -(defcustom proof-keep-response-history253,9246 -(defcustom pg-input-ring-size 263,9634 -(defcustom proof-general-debug 268,9786 -(defcustom proof-use-parser-cache 277,10157 -(defcustom proof-follow-mode 284,10413 -(defcustom proof-auto-action-when-deactivating-scripting 308,11590 -(defcustom proof-script-command-separator 331,12539 -(defcustom proof-rsh-command 339,12831 -(defcustom proof-disappearing-proofs 355,13381 -(defcustom proof-full-annotation 360,13542 -(defcustom proof-minibuffer-messages 369,13912 -(defcustom proof-autosend-enable 377,14221 -(defcustom proof-autosend-delay 383,14401 -(defcustom proof-autosend-all 389,14559 -(defcustom proof-fast-process-buffer 394,14728 +(defcustom proof-prog-name-ask218,8134 +(defcustom proof-prog-name-guess224,8294 +(defcustom proof-tidy-response232,8559 +(defcustom proof-keep-response-history246,9022 +(defcustom pg-input-ring-size 256,9410 +(defcustom proof-general-debug 261,9562 +(defcustom proof-use-parser-cache 270,9933 +(defcustom proof-follow-mode 277,10189 +(defcustom proof-auto-action-when-deactivating-scripting 301,11366 +(defcustom proof-rsh-command 324,12315 +(defcustom proof-disappearing-proofs 340,12865 +(defcustom proof-full-annotation 345,13026 +(defcustom proof-minibuffer-messages 354,13396 +(defcustom proof-autosend-enable 362,13705 +(defcustom proof-autosend-delay 368,13885 +(defcustom proof-autosend-all 374,14043 +(defcustom proof-fast-process-buffer 379,14212 generic/proof-utils.el,1567 -(defmacro proof-with-current-buffer-if-exists 61,1732 -(defmacro proof-with-script-buffer 70,2109 -(defmacro proof-map-buffers 81,2490 -(defmacro proof-sym 86,2675 -(defsubst proof-try-require 91,2836 -(defun proof-save-some-buffers 104,3167 -(defun proof-save-this-buffer 124,3763 -(defun proof-file-truename 137,4127 -(defun proof-files-to-buffers 141,4309 -(defun proof-buffers-in-mode 149,4548 -(defun pg-save-from-death 163,4998 -(defun proof-define-keys 182,5614 -(defun pg-remove-specials 193,5899 -(defun pg-remove-specials-in-string 203,6235 -(defun proof-safe-split-window-vertically 213,6460 -(defun proof-warn-if-unset 219,6658 -(defun proof-get-window-for-buffer 224,6876 -(defun proof-display-and-keep-buffer 275,9195 -(defun proof-clean-buffer 317,10918 -(defun pg-internal-warning 333,11574 -(defun proof-debug 341,11856 -(defun proof-switch-to-buffer 351,12227 -(defun proof-resize-window-tofit 373,13351 -(defun proof-submit-bug-report 468,17199 -(defun proof-deftoggle-fn 503,18556 -(defmacro proof-deftoggle 518,19219 -(defun proof-defintset-fn 525,19595 -(defmacro proof-defintset 541,20299 -(defun proof-defstringset-fn 548,20678 -(defmacro proof-defstringset 561,21304 -(defun proof-escape-keymap-doc 574,21760 -(defmacro proof-defshortcut 578,21914 -(defmacro proof-definvisible 593,22512 -(defun pg-custom-save-vars 620,23441 -(defun pg-custom-reset-vars 636,24085 -(defun proof-locate-executable 649,24422 -(defun pg-current-word-pos 664,24977 -(defsubst proof-shell-strip-output-markup 709,26632 -(defun proof-minibuffer-message 715,26896 +(defmacro proof-with-current-buffer-if-exists 61,1730 +(defmacro proof-with-script-buffer 70,2107 +(defmacro proof-map-buffers 81,2488 +(defmacro proof-sym 86,2673 +(defsubst proof-try-require 91,2834 +(defun proof-save-some-buffers 104,3165 +(defun proof-save-this-buffer 124,3761 +(defun proof-file-truename 137,4125 +(defun proof-files-to-buffers 141,4307 +(defun proof-buffers-in-mode 149,4546 +(defun pg-save-from-death 163,4996 +(defun proof-define-keys 182,5612 +(defun pg-remove-specials 193,5897 +(defun pg-remove-specials-in-string 203,6233 +(defun proof-safe-split-window-vertically 213,6458 +(defun proof-warn-if-unset 219,6656 +(defun proof-get-window-for-buffer 224,6874 +(defun proof-display-and-keep-buffer 273,9184 +(defun proof-clean-buffer 315,10907 +(defun pg-internal-warning 331,11563 +(defun proof-debug 339,11845 +(defun proof-switch-to-buffer 349,12216 +(defun proof-resize-window-tofit 371,13340 +(defun proof-submit-bug-report 466,17188 +(defun proof-deftoggle-fn 501,18545 +(defmacro proof-deftoggle 516,19211 +(defun proof-defintset-fn 527,19724 +(defmacro proof-defintset 543,20428 +(defun proof-defstringset-fn 550,20807 +(defmacro proof-defstringset 563,21433 +(defun proof-escape-keymap-doc 576,21889 +(defmacro proof-defshortcut 580,22043 +(defmacro proof-definvisible 595,22641 +(defun pg-custom-save-vars 622,23570 +(defun pg-custom-reset-vars 638,24214 +(defun proof-locate-executable 651,24551 +(defun pg-current-word-pos 666,25101 +(defsubst proof-shell-strip-output-markup 711,26756 +(defun proof-minibuffer-message 717,27020 lib/bufhist.el,1257 (defun bufhist-ring-update 38,1391 @@ -2011,11 +2036,11 @@ lib/maths-menu.el,242 lib/pg-dev.el,199 (defconst pg-dev-lisp-font-lock-keywords52,1588 -(defun pg-loadpath 80,2422 -(defun unload-pg 90,2593 -(defun profile-pg 121,3487 -(defun elp-pack-number 150,4514 -(defun pg-bug-references 159,4714 +(defun pg-loadpath 78,2287 +(defun unload-pg 88,2458 +(defun profile-pg 119,3352 +(defun elp-pack-number 148,4379 +(defun pg-bug-references 157,4579 lib/pg-fontsets.el,209 (defcustom pg-fontsets-default-fontset 24,722 @@ -2054,7 +2079,7 @@ lib/scomint.el,876 (defun scomint-output-filter 291,11525 (defun scomint-interrupt-process 363,14257 -lib/span.el,1406 +lib/span.el,1510 (defalias 'span-start span-start22,610 (defalias 'span-end span-end23,648 (defalias 'span-set-property span-set-property24,682 @@ -2092,7 +2117,9 @@ lib/span.el,1406 (defsubst span-property-safe 206,6951 (defsubst span-set-start 210,7088 (defsubst span-set-end 214,7220 -(defun span-add-self-removing-span 222,7380 +(defun span-make-self-removing-span 222,7380 +(defun span-delete-self-modification-hook 232,7748 +(defun span-make-modifying-removing-span 237,7922 lib/texi-docstring-magic.el,584 (defun texi-docstring-magic-find-face 88,3027 @@ -2205,28 +2232,28 @@ lib/unicode-tokens.el,5900 (defvar unicode-tokens-mode-map 1073,38906 (defvar unicode-tokens-display-table1076,39003 (define-minor-mode unicode-tokens-mode1083,39254 -(defun unicode-tokens-set-font-var 1216,43737 -(defun unicode-tokens-set-font-var-aux 1232,44226 -(defun unicode-tokens-mouse-set-font 1263,45387 -(defsubst unicode-tokens-face-font-sym 1276,45901 -(defun unicode-tokens-set-font-restart 1280,46081 -(defun unicode-tokens-save-fonts 1291,46391 -(defun unicode-tokens-custom-save-faces 1299,46647 -(define-key unicode-tokens-mode-map1316,47103 -(define-key unicode-tokens-mode-map1319,47210 -(defvar unicode-tokens-quail-translation-keymap1323,47300 -(define-key unicode-tokens-quail-translation-keymap1330,47490 -(defun unicode-tokens-quail-delete-last-char 1334,47624 -(define-key unicode-tokens-mode-map 1349,48051 -(define-key unicode-tokens-mode-map 1351,48143 -(define-key unicode-tokens-mode-map1353,48234 -(define-key unicode-tokens-mode-map1355,48340 -(define-key unicode-tokens-mode-map1358,48455 -(define-key unicode-tokens-mode-map1360,48564 -(define-key unicode-tokens-mode-map1362,48672 -(define-key unicode-tokens-mode-map1364,48778 -(defun unicode-tokens-customize-submenu 1372,48902 -(defun unicode-tokens-define-menu 1379,49125 +(defun unicode-tokens-set-font-var 1219,43807 +(defun unicode-tokens-set-font-var-aux 1235,44296 +(defun unicode-tokens-mouse-set-font 1266,45457 +(defsubst unicode-tokens-face-font-sym 1279,45971 +(defun unicode-tokens-set-font-restart 1283,46151 +(defun unicode-tokens-save-fonts 1294,46461 +(defun unicode-tokens-custom-save-faces 1302,46717 +(define-key unicode-tokens-mode-map1319,47173 +(define-key unicode-tokens-mode-map1322,47280 +(defvar unicode-tokens-quail-translation-keymap1326,47370 +(define-key unicode-tokens-quail-translation-keymap1333,47560 +(defun unicode-tokens-quail-delete-last-char 1337,47694 +(define-key unicode-tokens-mode-map 1352,48121 +(define-key unicode-tokens-mode-map 1354,48213 +(define-key unicode-tokens-mode-map1356,48304 +(define-key unicode-tokens-mode-map1358,48410 +(define-key unicode-tokens-mode-map1361,48525 +(define-key unicode-tokens-mode-map1363,48634 +(define-key unicode-tokens-mode-map1365,48742 +(define-key unicode-tokens-mode-map1367,48848 +(defun unicode-tokens-customize-submenu 1375,48972 +(defun unicode-tokens-define-menu 1382,49195 contrib/mmm/mmm-auto.el,343 (defvar mmm-autoloaded-classes67,2675 @@ -2472,169 +2499,168 @@ contrib/mmm/mmm-vars.el,2668 (defun mmm-mode-ext-applies 1028,37844 (defun mmm-get-all-classes 1042,38223 -doc/ProofGeneral.texi,6304 -@node Top161,4909 -@node Preface199,6063 -@node News for Version 4.0News for Version 4.0222,6652 -@node Future243,7447 -@node Credits272,8782 -@node Introducing Proof GeneralIntroducing Proof General391,12966 -@node Installing Proof GeneralInstalling Proof General446,14940 -@node Quick start guideQuick start guide460,15389 -@node Features of Proof GeneralFeatures of Proof General504,17510 -@node Supported proof assistantsSupported proof assistants593,21447 -@node Prerequisites for this manualPrerequisites for this manual642,23338 -@node Organization of this manualOrganization of this manual686,24957 -@node Basic Script ManagementBasic Script Management712,25785 -@node Walkthrough example in IsabelleWalkthrough example in Isabelle731,26385 -@node Proof scriptsProof scripts997,36637 -@node Script buffersScript buffers1040,38757 -@node Locked queue and editing regionsLocked queue and editing regions1062,39334 -@node Goal-save sequencesGoal-save sequences1118,41481 -@node Active scripting bufferActive scripting buffer1155,42947 -@node Summary of Proof General buffersSummary of Proof General buffers1224,46367 -@node Script editing commandsScript editing commands1273,48624 -@node Script processing commandsScript processing commands1353,51583 -@node Proof assistant commandsProof assistant commands1480,56886 -@node Toolbar commandsToolbar commands1655,63075 -@node Interrupting during trace outputInterrupting during trace output1679,64004 -@node Advanced Script Management and EditingAdvanced Script Management and Editing1719,65934 -@node Document centred workingDocument centred working1740,66555 -@node Automatic processingAutomatic processing1809,69148 -@node Visibility of completed proofsVisibility of completed proofs1838,70157 -@node Switching between proof scriptsSwitching between proof scripts1893,72086 -@node View of processed files View of processed files 1930,74058 -@node Retracting across filesRetracting across files1990,77109 -@node Asserting across filesAsserting across files2003,77740 -@node Automatic multiple file handlingAutomatic multiple file handling2016,78306 -@node Escaping script managementEscaping script management2041,79340 -@node Editing featuresEditing features2098,81452 -@node Unicode symbols and special layout supportUnicode symbols and special layout support2168,84231 -@node Maths menuMaths menu2210,85789 -@node Unicode Tokens modeUnicode Tokens mode2227,86480 -@node Configuring tokens symbols and shortcutsConfiguring tokens symbols and shortcuts2277,88903 -@node Special layout Special layout 2307,89864 -@node Moving between Unicode and tokensMoving between Unicode and tokens2415,93980 -@node Finding available tokens shortcuts and symbolsFinding available tokens shortcuts and symbols2470,96091 -@node Selecting suitable fontsSelecting suitable fonts2509,97265 -@node Support for other PackagesSupport for other Packages2574,100253 -@node Syntax highlightingSyntax highlighting2604,101089 -@node Imenu and SpeedbarImenu and Speedbar2632,102092 -@node Support for outline modeSupport for outline mode2678,103748 -@node Support for completionSupport for completion2703,104877 -@node Support for tagsSupport for tags2760,107039 -@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing2812,109387 -@node Goals buffer commandsGoals buffer commands2827,109899 -@node Customizing Proof GeneralCustomizing Proof General2915,113434 -@node Basic optionsBasic options2955,115104 -@node How to customizeHow to customize2979,115874 -@node Display customizationDisplay customization3026,117841 -@node User optionsUser options3180,124246 -@node Changing facesChanging faces3411,132432 -@node Script buffer facesScript buffer faces3433,133307 -@node Goals and response facesGoals and response faces3479,134907 -@node Tweaking configuration settingsTweaking configuration settings3524,136439 -@node Hints and TipsHints and Tips3581,138965 -@node Adding your own keybindingsAdding your own keybindings3600,139566 -@node Using file variablesUsing file variables3664,142180 -@node Using abbreviationsUsing abbreviations3723,144366 -@node LEGO Proof GeneralLEGO Proof General3762,145781 -@node LEGO specific commandsLEGO specific commands3803,147150 -@node LEGO tagsLEGO tags3823,147605 -@node LEGO customizationsLEGO customizations3833,147852 -@node Coq Proof GeneralCoq Proof General3865,148771 -@node Coq-specific commandsCoq-specific commands3881,149180 -@node Coq-specific variablesCoq-specific variables3903,149687 -@node Editing multiple proofsEditing multiple proofs3925,150345 -@node User-loaded tacticsUser-loaded tactics3949,151453 -@node Holes featureHoles feature4013,153927 -@node Isabelle Proof GeneralIsabelle Proof General4040,155214 -@node Choosing logic and starting isabelleChoosing logic and starting isabelle4066,156090 -@node Isabelle commandsIsabelle commands4135,158886 -@node Isabelle settingsIsabelle settings4278,163078 -@node Isabelle customizationsIsabelle customizations4292,163660 -@node HOL Proof GeneralHOL Proof General4315,164147 -@node Shell Proof GeneralShell Proof General4357,165969 -@node Obtaining and InstallingObtaining and Installing4393,167428 -@node Obtaining Proof GeneralObtaining Proof General4408,167793 -@node Installing Proof General from tarballInstalling Proof General from tarball4434,168675 -@node Setting the names of binariesSetting the names of binaries4458,169465 -@node Notes for syssiesNotes for syssies4486,170405 -@node Bugs and EnhancementsBugs and Enhancements4562,173402 -@node References4583,174217 -@node History of Proof GeneralHistory of Proof General4623,175240 -@node Old News for 3.0Old News for 3.04717,179405 -@node Old News for 3.1Old News for 3.14787,183099 -@node Old News for 3.2Old News for 3.24813,184271 -@node Old News for 3.3Old News for 3.34874,187274 -@node Old News for 3.4Old News for 3.44893,188171 -@node Old News for 3.5Old News for 3.54915,189226 -@node Old News for 3.6Old News for 3.64919,189283 -@node Old News for 3.7Old News for 3.74924,189383 -@node Function IndexFunction Index4968,191306 -@node Variable IndexVariable Index4972,191382 -@node Keystroke IndexKeystroke Index4976,191462 -@node Concept IndexConcept Index4980,191528 +doc/ProofGeneral.texi,6240 +@node Top161,4917 +@node Preface199,6071 +@node News for Version 4.0News for Version 4.0222,6660 +@node Future243,7504 +@node Credits272,8839 +@node Introducing Proof GeneralIntroducing Proof General392,13042 +@node Installing Proof GeneralInstalling Proof General447,15016 +@node Quick start guideQuick start guide461,15465 +@node Features of Proof GeneralFeatures of Proof General505,17586 +@node Supported proof assistantsSupported proof assistants594,21523 +@node Prerequisites for this manualPrerequisites for this manual643,23404 +@node Organization of this manualOrganization of this manual687,25023 +@node Basic Script ManagementBasic Script Management713,25851 +@node Walkthrough example in IsabelleWalkthrough example in Isabelle732,26451 +@node Proof scriptsProof scripts995,36579 +@node Script buffersScript buffers1038,38699 +@node Locked queue and editing regionsLocked queue and editing regions1060,39276 +@node Goal-save sequencesGoal-save sequences1116,41423 +@node Active scripting bufferActive scripting buffer1153,42889 +@node Summary of Proof General buffersSummary of Proof General buffers1222,46309 +@node Script editing commandsScript editing commands1271,48566 +@node Script processing commandsScript processing commands1351,51525 +@node Proof assistant commandsProof assistant commands1477,56770 +@node Toolbar commandsToolbar commands1660,63241 +@node Interrupting during trace outputInterrupting during trace output1685,64200 +@node Advanced Script Management and EditingAdvanced Script Management and Editing1725,66130 +@node Document centred workingDocument centred working1746,66751 +@node Automatic processingAutomatic processing1825,69809 +@node Visibility of completed proofsVisibility of completed proofs1880,71832 +@node Switching between proof scriptsSwitching between proof scripts1935,73772 +@node View of processed files View of processed files 1972,75744 +@node Retracting across filesRetracting across files2032,78795 +@node Asserting across filesAsserting across files2045,79426 +@node Automatic multiple file handlingAutomatic multiple file handling2058,79992 +@node Escaping script managementEscaping script management2083,81026 +@node Editing featuresEditing features2140,83138 +@node Unicode symbols and special layout supportUnicode symbols and special layout support2210,85917 +@node Maths menuMaths menu2252,87475 +@node Unicode Tokens modeUnicode Tokens mode2269,88166 +@node Configuring tokens symbols and shortcutsConfiguring tokens symbols and shortcuts2319,90589 +@node Special layout Special layout 2349,91550 +@node Moving between Unicode and tokensMoving between Unicode and tokens2457,95666 +@node Finding available tokens shortcuts and symbolsFinding available tokens shortcuts and symbols2512,97777 +@node Selecting suitable fontsSelecting suitable fonts2551,98951 +@node Support for other PackagesSupport for other Packages2616,101939 +@node Syntax highlightingSyntax highlighting2646,102775 +@node Imenu and SpeedbarImenu and Speedbar2674,103778 +@node Support for outline modeSupport for outline mode2720,105449 +@node Support for completionSupport for completion2745,106578 +@node Support for tagsSupport for tags2802,108740 +@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing2854,111088 +@node Goals buffer commandsGoals buffer commands2870,111683 +@node Customizing Proof GeneralCustomizing Proof General2969,115836 +@node Basic optionsBasic options3009,117506 +@node How to customizeHow to customize3033,118276 +@node Display customizationDisplay customization3080,120243 +@node User optionsUser options3234,126648 +@node Changing facesChanging faces3454,134430 +@node Script buffer facesScript buffer faces3476,135305 +@node Goals and response facesGoals and response faces3522,136905 +@node Tweaking configuration settingsTweaking configuration settings3567,138437 +@node Hints and TipsHints and Tips3624,140963 +@node Adding your own keybindingsAdding your own keybindings3643,141564 +@node Using file variablesUsing file variables3707,144178 +@node Using abbreviationsUsing abbreviations3766,146364 +@node LEGO Proof GeneralLEGO Proof General3805,147779 +@node LEGO specific commandsLEGO specific commands3846,149148 +@node LEGO tagsLEGO tags3866,149603 +@node LEGO customizationsLEGO customizations3876,149850 +@node Coq Proof GeneralCoq Proof General3908,150769 +@node Coq-specific commandsCoq-specific commands3922,151080 +@node Editing multiple proofsEditing multiple proofs3945,151588 +@node User-loaded tacticsUser-loaded tactics3969,152696 +@node Holes featureHoles feature4033,155170 +@node Isabelle Proof GeneralIsabelle Proof General4062,156500 +@node Choosing logic and starting isabelleChoosing logic and starting isabelle4088,157376 +@node Isabelle commandsIsabelle commands4157,160177 +@node Isabelle settingsIsabelle settings4300,164369 +@node Isabelle customizationsIsabelle customizations4314,164951 +@node HOL Proof GeneralHOL Proof General4337,165438 +@node Shell Proof GeneralShell Proof General4379,167260 +@node Obtaining and InstallingObtaining and Installing4415,168719 +@node Obtaining Proof GeneralObtaining Proof General4430,169084 +@node Installing Proof General from tarballInstalling Proof General from tarball4456,169966 +@node Setting the names of binariesSetting the names of binaries4480,170756 +@node Notes for syssiesNotes for syssies4508,171696 +@node Bugs and EnhancementsBugs and Enhancements4584,174693 +@node References4605,175508 +@node History of Proof GeneralHistory of Proof General4645,176531 +@node Old News for 3.0Old News for 3.04739,180696 +@node Old News for 3.1Old News for 3.14809,184390 +@node Old News for 3.2Old News for 3.24835,185562 +@node Old News for 3.3Old News for 3.34896,188565 +@node Old News for 3.4Old News for 3.44915,189462 +@node Old News for 3.5Old News for 3.54937,190517 +@node Old News for 3.6Old News for 3.64941,190574 +@node Old News for 3.7Old News for 3.74946,190674 +@node Function IndexFunction Index4976,192128 +@node Variable IndexVariable Index4980,192204 +@node Keystroke IndexKeystroke Index4984,192284 +@node Concept IndexConcept Index4988,192350 doc/PG-adapting.texi,3770 -@node Top153,4679 -@node Introduction190,5788 -@node Future231,7441 -@node Credits267,9037 -@node Beginning with a New ProverBeginning with a New Prover277,9329 -@node Overview of adding a new proverOverview of adding a new prover317,11271 -@node Demonstration instance and easy configurationDemonstration instance and easy configuration394,14580 -@node Major modes used by Proof GeneralMajor modes used by Proof General463,17971 -@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands506,19681 -@node Settings for generic user-level commandsSettings for generic user-level commands521,20227 -@node Menu configurationMenu configuration566,21959 -@node Toolbar configurationToolbar configuration590,22876 -@node Proof Script SettingsProof Script Settings649,25113 -@node Recognizing commands and commentsRecognizing commands and comments671,25693 -@node Recognizing proofsRecognizing proofs808,32146 -@node Recognizing other elementsRecognizing other elements912,36450 -@node Configuring undo behaviourConfiguring undo behaviour975,38929 -@node Nested proofsNested proofs1112,44316 -@node Safe (state-preserving) commandsSafe (state-preserving) commands1152,45942 -@node Activate scripting hookActivate scripting hook1175,46895 -@node Automatic multiple filesAutomatic multiple files1199,47765 -@node Completions1221,48612 -@node Proof Shell SettingsProof Shell Settings1262,50102 -@node Proof shell commandsProof shell commands1293,51384 -@node Script input to the shellScript input to the shell1457,58432 -@node Settings for matching various output from proof processSettings for matching various output from proof process1525,61502 -@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process1647,66856 -@node Hooks and other settingsHooks and other settings1887,77610 -@node Goals Buffer SettingsGoals Buffer Settings1966,80754 -@node Splash Screen SettingsSplash Screen Settings2040,83744 -@node Global ConstantsGlobal Constants2066,84499 -@node Handling Multiple FilesHandling Multiple Files2092,85328 -@node Configuring Editing SyntaxConfiguring Editing Syntax2244,93132 -@node Configuring Font LockConfiguring Font Lock2301,95249 -@node Configuring TokensConfiguring Tokens2377,98956 -@node Writing More Lisp CodeWriting More Lisp Code2427,101076 -@node Default values for generic settingsDefault values for generic settings2444,101721 -@node Adding prover-specific configurationsAdding prover-specific configurations2474,102804 -@node Useful variablesUseful variables2517,104086 -@node Useful functions and macrosUseful functions and macros2532,104585 -@node Internals of Proof GeneralInternals of Proof General2641,108820 -@node Spans2671,109750 -@node Proof General site configurationProof General site configuration2686,110123 -@node Configuration variable mechanismsConfiguration variable mechanisms2769,113222 -@node Global variablesGlobal variables2895,118670 -@node Proof script modeProof script mode2970,121294 -@node Proof shell modeProof shell mode3201,131734 -@node Debugging3714,152272 -@node Plans and IdeasPlans and Ideas3757,153148 -@node Proof by pointing and similar featuresProof by pointing and similar features3778,153870 -@node Granularity of atomic command sequencesGranularity of atomic command sequences3816,155528 -@node Browser mode for script files and theoriesBrowser mode for script files and theories3861,157753 -@node Demonstration InstantiationsDemonstration Instantiations3891,158784 -@node demoisa-easy.el3907,159215 -@node demoisa.el3969,161407 -@node Function IndexFunction Index4123,166327 -@node Variable IndexVariable Index4127,166403 -@node Concept IndexConcept Index4136,166582 +@node Top153,4678 +@node Introduction190,5787 +@node Future231,7440 +@node Credits267,9036 +@node Beginning with a New ProverBeginning with a New Prover277,9328 +@node Overview of adding a new proverOverview of adding a new prover317,11270 +@node Demonstration instance and easy configurationDemonstration instance and easy configuration396,14573 +@node Major modes used by Proof GeneralMajor modes used by Proof General465,17964 +@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands508,19674 +@node Settings for generic user-level commandsSettings for generic user-level commands523,20220 +@node Menu configurationMenu configuration568,21952 +@node Toolbar configurationToolbar configuration592,22869 +@node Proof Script SettingsProof Script Settings651,25106 +@node Recognizing commands and commentsRecognizing commands and comments673,25686 +@node Recognizing proofsRecognizing proofs810,32139 +@node Recognizing other elementsRecognizing other elements914,36443 +@node Configuring undo behaviourConfiguring undo behaviour977,38922 +@node Nested proofsNested proofs1114,44309 +@node Safe (state-preserving) commandsSafe (state-preserving) commands1154,45935 +@node Activate scripting hookActivate scripting hook1177,46888 +@node Automatic multiple filesAutomatic multiple files1201,47758 +@node Completions1223,48605 +@node Proof Shell SettingsProof Shell Settings1264,50095 +@node Proof shell commandsProof shell commands1295,51377 +@node Script input to the shellScript input to the shell1459,58428 +@node Settings for matching various output from proof processSettings for matching various output from proof process1527,61498 +@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process1649,66852 +@node Hooks and other settingsHooks and other settings1889,77606 +@node Goals Buffer SettingsGoals Buffer Settings1968,80750 +@node Splash Screen SettingsSplash Screen Settings2042,83740 +@node Global ConstantsGlobal Constants2068,84495 +@node Handling Multiple FilesHandling Multiple Files2094,85324 +@node Configuring Editing SyntaxConfiguring Editing Syntax2246,93128 +@node Configuring Font LockConfiguring Font Lock2303,95245 +@node Configuring TokensConfiguring Tokens2379,98957 +@node Writing More Lisp CodeWriting More Lisp Code2429,101077 +@node Default values for generic settingsDefault values for generic settings2446,101722 +@node Adding prover-specific configurationsAdding prover-specific configurations2476,102805 +@node Useful variablesUseful variables2519,104087 +@node Useful functions and macrosUseful functions and macros2534,104586 +@node Internals of Proof GeneralInternals of Proof General2644,108898 +@node Spans2674,109828 +@node Proof General site configurationProof General site configuration2689,110201 +@node Configuration variable mechanismsConfiguration variable mechanisms2772,113282 +@node Global variablesGlobal variables2898,118763 +@node Proof script modeProof script mode2973,121387 +@node Proof shell modeProof shell mode3223,132713 +@node Debugging3737,153362 +@node Plans and IdeasPlans and Ideas3780,154238 +@node Proof by pointing and similar featuresProof by pointing and similar features3801,154960 +@node Granularity of atomic command sequencesGranularity of atomic command sequences3839,156618 +@node Browser mode for script files and theoriesBrowser mode for script files and theories3884,158843 +@node Demonstration InstantiationsDemonstration Instantiations3914,159874 +@node demoisa-easy.el3930,160305 +@node demoisa.el3992,162497 +@node Function IndexFunction Index4146,167417 +@node Variable IndexVariable Index4150,167493 +@node Concept IndexConcept Index4159,167672 generic/proof.el,0 |