diff options
author | 2004-08-25 21:05:53 +0000 | |
---|---|---|
committer | 2004-08-25 21:05:53 +0000 | |
commit | 882e453a0921295e95201a57ed55517ad66e9342 (patch) | |
tree | e9678e5fe096024b8be35d0830a699c4e3ced7b7 /TAGS | |
parent | c0ba98b45ed0c886e5bbfbc76c79aeeaf388fd64 (diff) |
Updated.
Diffstat (limited to 'TAGS')
-rw-r--r-- | TAGS | 2413 |
1 files changed, 1257 insertions, 1156 deletions
@@ -11,97 +11,97 @@ coq/coq-abbrev-V7.el,49 (defpgdefault menu-entriesmenu-entries119,5878 coq/coq.el,5468 -(defcustom coq-prog-name coq-prog-name13,355 -(defcustom coq-compile-file-command coq-compile-file-command18,464 -(defcustom coq-default-undo-limit coq-default-undo-limit28,833 -(defconst coq-shell-init-cmd coq-shell-init-cmd33,961 -(defconst coq-shell-restart-cmd coq-shell-restart-cmd46,1384 -(defvar coq-shell-prompt-pattern coq-shell-prompt-pattern53,1642 -(defvar coq-shell-cd coq-shell-cd58,1850 -(defvar coq-shell-abort-goal-regexp coq-shell-abort-goal-regexp64,2051 -(defvar coq-shell-proof-completed-regexp coq-shell-proof-completed-regexp67,2177 -(defvar coq-goal-regexpcoq-goal-regexp70,2308 -(defun coq-library-directory coq-library-directory79,2497 -(defcustom coq-tags coq-tags86,2677 -(defconst coq-interrupt-regexp coq-interrupt-regexp91,2826 -(defcustom coq-www-home-page coq-www-home-page96,2946 -(defun coq-insert-section coq-insert-section112,3196 -(defconst module-kinds-table module-kinds-table121,3453 -(defconst modtype-kinds-tablemodtype-kinds-table125,3589 -(defun coq-insert-module coq-insert-module129,3718 -(defvar coq-outline-regexpcoq-outline-regexp150,4475 -(defvar coq-outline-heading-end-regexp coq-outline-heading-end-regexp155,4884 -(defvar coq-shell-outline-regexp coq-shell-outline-regexp157,4943 -(defvar coq-shell-outline-heading-end-regexp coq-shell-outline-heading-end-regexp158,4993 -(defconst coq-kill-goal-command coq-kill-goal-command160,5056 -(defconst coq-forget-id-command coq-forget-id-command161,5099 -(defconst coq-back-n-command coq-back-n-command162,5145 -(defconst coq-state-changing-tactics-regexp coq-state-changing-tactics-regexp166,5207 -(defconst coq-state-preserving-tactics-regexp coq-state-preserving-tactics-regexp168,5304 -(defconst coq-tactics-regexpcoq-tactics-regexp170,5405 -(defconst coq-state-changing-commands-regexpcoq-state-changing-commands-regexp172,5471 -(defconst coq-state-preserving-commands-regexp coq-state-preserving-commands-regexp174,5578 -(defvar coq-retractable-instruct-regexp coq-retractable-instruct-regexp176,5690 -(defvar coq-non-retractable-instruct-regexpcoq-non-retractable-instruct-regexp178,5781 -(defvar coq-keywords-sectioncoq-keywords-section181,5880 -(defvar coq-section-regexp coq-section-regexp186,6025 -(defun coq-set-undo-limit coq-set-undo-limit219,7092 -(defconst coq-keywords-decl-defn-regexpcoq-keywords-decl-defn-regexp230,7435 -(defun coq-proof-mode-p coq-proof-mode-p238,7823 -(defun coq-is-comment-or-proverprocp coq-is-comment-or-proverprocp253,8329 -(defun coq-is-goalsave-p coq-is-goalsave-p255,8433 -(defun coq-is-module-equal-p coq-is-module-equal-p256,8508 -(defun coq-is-def-p coq-is-def-p259,8704 -(defun coq-is-decl-defn-p coq-is-decl-defn-p261,8812 -(defun coq-state-preserving-command-p coq-state-preserving-command-p266,8979 -(defun coq-state-preserving-tactic-p coq-state-preserving-tactic-p269,9113 -(defun coq-state-changing-command-p coq-state-changing-command-p272,9245 -(defun coq-section-or-module-start-p coq-section-or-module-start-p278,9553 -(defun coq-find-and-forget coq-find-and-forget286,9806 -(defvar coq-current-goal coq-current-goal378,14373 -(defun coq-goal-hyp coq-goal-hyp381,14438 -(defun coq-state-preserving-p coq-state-preserving-p394,14868 -(defun coq-SearchIsos coq-SearchIsos401,15185 -(defun coq-guess-or-ask-for-string coq-guess-or-ask-for-string415,15619 -(defun coq-Print coq-Print425,15913 -(defun coq-Check coq-Check434,16171 -(defun coq-Show coq-Show443,16413 -(defun coq-PrintHint coq-PrintHint464,17099 -(defun coq-end-Section coq-end-Section470,17242 -(defun coq-Compile coq-Compile488,17826 -(defun coq-intros coq-intros495,18006 -(define-key coq-keymap coq-keymap512,18683 -(define-key coq-keymap coq-keymap513,18734 -(define-key coq-keymap coq-keymap514,18793 -(define-key coq-keymap coq-keymap515,18851 -(define-key coq-keymap coq-keymap516,18907 -(define-key coq-keymap coq-keymap517,18962 -(define-key coq-keymap coq-keymap518,19012 -(define-key coq-keymap coq-keymap519,19062 -(define-key global-map global-map528,19571 -(defun coq-guess-command-line coq-guess-command-line587,21565 -(defun coq-pre-shell-start coq-pre-shell-start609,22371 -(defun coq-mode-config coq-mode-config620,22892 -(defun coq-shell-mode-config coq-shell-mode-config726,26637 -(defun coq-goals-mode-config coq-goals-mode-config765,28272 -(defun coq-response-config coq-response-config772,28503 -(defun coq-maybe-compile-buffer coq-maybe-compile-buffer792,29219 -(defun coq-ancestors-of coq-ancestors-of829,30753 -(defun coq-all-ancestors-of coq-all-ancestors-of852,31720 -(defconst coq-require-command-regexp coq-require-command-regexp864,32113 -(defun coq-process-require-command coq-process-require-command869,32322 -(defun coq-included-children coq-included-children874,32449 -(defun coq-process-file coq-process-file895,33288 -(defpacustom print-only-first-subgoal print-only-first-subgoal909,33786 -(defpacustom print-fully-explicit print-fully-explicit914,33937 -(defpacustom print-coercions print-coercions919,34084 -(defpacustom print-match-wildcards print-match-wildcards924,34227 -(defpacustom time-commands time-commands930,34409 -(defpacustom auto-compile-vos auto-compile-vos934,34520 -(defpacustom translate-to-v8 translate-to-v8956,35475 -(defun coq-preprocessing coq-preprocessing965,35691 -(defun coq-fake-constant-markup coq-fake-constant-markup980,36110 -(defun coq-create-span-menu coq-create-span-menu1002,36917 +(defcustom coq-prog-name coq-prog-name13,353 +(defcustom coq-compile-file-command coq-compile-file-command18,462 +(defcustom coq-default-undo-limit coq-default-undo-limit28,831 +(defconst coq-shell-init-cmd coq-shell-init-cmd33,959 +(defconst coq-shell-restart-cmd coq-shell-restart-cmd46,1382 +(defvar coq-shell-prompt-pattern coq-shell-prompt-pattern53,1640 +(defvar coq-shell-cd coq-shell-cd58,1848 +(defvar coq-shell-abort-goal-regexp coq-shell-abort-goal-regexp64,2049 +(defvar coq-shell-proof-completed-regexp coq-shell-proof-completed-regexp67,2175 +(defvar coq-goal-regexpcoq-goal-regexp70,2306 +(defun coq-library-directory coq-library-directory79,2495 +(defcustom coq-tags coq-tags86,2675 +(defconst coq-interrupt-regexp coq-interrupt-regexp91,2824 +(defcustom coq-www-home-page coq-www-home-page96,2944 +(defun coq-insert-section coq-insert-section112,3194 +(defconst module-kinds-table module-kinds-table121,3451 +(defconst modtype-kinds-tablemodtype-kinds-table125,3587 +(defun coq-insert-module coq-insert-module129,3716 +(defvar coq-outline-regexpcoq-outline-regexp150,4473 +(defvar coq-outline-heading-end-regexp coq-outline-heading-end-regexp155,4882 +(defvar coq-shell-outline-regexp coq-shell-outline-regexp157,4941 +(defvar coq-shell-outline-heading-end-regexp coq-shell-outline-heading-end-regexp158,4991 +(defconst coq-kill-goal-command coq-kill-goal-command160,5054 +(defconst coq-forget-id-command coq-forget-id-command161,5097 +(defconst coq-back-n-command coq-back-n-command162,5143 +(defconst coq-state-changing-tactics-regexp coq-state-changing-tactics-regexp166,5205 +(defconst coq-state-preserving-tactics-regexp coq-state-preserving-tactics-regexp168,5302 +(defconst coq-tactics-regexpcoq-tactics-regexp170,5403 +(defconst coq-state-changing-commands-regexpcoq-state-changing-commands-regexp172,5469 +(defconst coq-state-preserving-commands-regexp coq-state-preserving-commands-regexp174,5576 +(defvar coq-retractable-instruct-regexp coq-retractable-instruct-regexp176,5688 +(defvar coq-non-retractable-instruct-regexpcoq-non-retractable-instruct-regexp178,5779 +(defvar coq-keywords-sectioncoq-keywords-section181,5878 +(defvar coq-section-regexp coq-section-regexp186,6023 +(defun coq-set-undo-limit coq-set-undo-limit219,7090 +(defconst coq-keywords-decl-defn-regexpcoq-keywords-decl-defn-regexp230,7433 +(defun coq-proof-mode-p coq-proof-mode-p238,7821 +(defun coq-is-comment-or-proverprocp coq-is-comment-or-proverprocp253,8327 +(defun coq-is-goalsave-p coq-is-goalsave-p255,8431 +(defun coq-is-module-equal-p coq-is-module-equal-p256,8506 +(defun coq-is-def-p coq-is-def-p259,8702 +(defun coq-is-decl-defn-p coq-is-decl-defn-p261,8810 +(defun coq-state-preserving-command-p coq-state-preserving-command-p266,8977 +(defun coq-state-preserving-tactic-p coq-state-preserving-tactic-p269,9111 +(defun coq-state-changing-command-p coq-state-changing-command-p272,9243 +(defun coq-section-or-module-start-p coq-section-or-module-start-p278,9551 +(defun coq-find-and-forget coq-find-and-forget286,9804 +(defvar coq-current-goal coq-current-goal378,14371 +(defun coq-goal-hyp coq-goal-hyp381,14436 +(defun coq-state-preserving-p coq-state-preserving-p394,14866 +(defun coq-SearchIsos coq-SearchIsos401,15183 +(defun coq-guess-or-ask-for-string coq-guess-or-ask-for-string415,15617 +(defun coq-Print coq-Print425,15911 +(defun coq-Check coq-Check434,16169 +(defun coq-Show coq-Show443,16411 +(defun coq-PrintHint coq-PrintHint464,17097 +(defun coq-end-Section coq-end-Section470,17240 +(defun coq-Compile coq-Compile488,17824 +(defun coq-intros coq-intros495,18004 +(define-key coq-keymap coq-keymap512,18681 +(define-key coq-keymap coq-keymap513,18732 +(define-key coq-keymap coq-keymap514,18791 +(define-key coq-keymap coq-keymap515,18849 +(define-key coq-keymap coq-keymap516,18905 +(define-key coq-keymap coq-keymap517,18960 +(define-key coq-keymap coq-keymap518,19010 +(define-key coq-keymap coq-keymap519,19060 +(define-key global-map global-map528,19569 +(defun coq-guess-command-line coq-guess-command-line587,21563 +(defun coq-pre-shell-start coq-pre-shell-start609,22369 +(defun coq-mode-config coq-mode-config620,22890 +(defun coq-shell-mode-config coq-shell-mode-config727,26705 +(defun coq-goals-mode-config coq-goals-mode-config766,28340 +(defun coq-response-config coq-response-config773,28571 +(defun coq-maybe-compile-buffer coq-maybe-compile-buffer793,29287 +(defun coq-ancestors-of coq-ancestors-of830,30821 +(defun coq-all-ancestors-of coq-all-ancestors-of853,31788 +(defconst coq-require-command-regexp coq-require-command-regexp865,32181 +(defun coq-process-require-command coq-process-require-command870,32390 +(defun coq-included-children coq-included-children875,32517 +(defun coq-process-file coq-process-file896,33356 +(defpacustom print-only-first-subgoal print-only-first-subgoal910,33854 +(defpacustom print-fully-explicit print-fully-explicit915,34005 +(defpacustom print-coercions print-coercions920,34152 +(defpacustom print-match-wildcards print-match-wildcards925,34295 +(defpacustom time-commands time-commands931,34477 +(defpacustom auto-compile-vos auto-compile-vos935,34588 +(defpacustom translate-to-v8 translate-to-v8957,35543 +(defun coq-preprocessing coq-preprocessing966,35759 +(defun coq-fake-constant-markup coq-fake-constant-markup981,36178 +(defun coq-create-span-menu coq-create-span-menu1003,36985 coq/coq-indent.el,1791 (defconst coq-any-command-regexpcoq-any-command-regexp11,262 @@ -141,51 +141,51 @@ coq/coq-syntax.el,3214 (defvar coq-version-is-V7 coq-version-is-V732,1119 (defvar coq-version-is-V74 coq-version-is-V7440,1529 (defvar coq-version-is-V8 coq-version-is-V849,1988 -(defvar coq-keywords-declcoq-keywords-decl124,4579 -(defvar coq-keywords-defncoq-keywords-defn139,4935 -(defun coq-count-match coq-count-match213,7291 -(defun coq-goal-command-p coq-goal-command-p225,7711 -(defvar coq-keywords-save-strictcoq-keywords-save-strict245,8295 -(defvar coq-keywords-savecoq-keywords-save253,8392 -(defun coq-save-command-p coq-save-command-p257,8468 -(defvar coq-keywords-kill-goal coq-keywords-kill-goal265,8747 -(defcustom coq-user-state-changing-commands coq-user-state-changing-commands271,8797 -(defcustom coq-user-state-preserving-commands coq-user-state-preserving-commands283,9194 -(defvar coq-keywords-state-preserving-commandscoq-keywords-state-preserving-commands296,9634 -(defvar coq-keywords-state-changing-misc-commandscoq-keywords-state-changing-misc-commands343,10745 -(defvar coq-keywords-state-changing-commandscoq-keywords-state-changing-commands417,12763 -(defvar coq-keywords-commandscoq-keywords-commands427,12960 -(defcustom coq-user-state-changing-tactics coq-user-state-changing-tactics433,13110 -(defvar coq-state-changing-tacticscoq-state-changing-tactics444,13536 -(defcustom coq-user-state-preserving-tactics coq-user-state-preserving-tactics645,16861 -(defvar coq-state-preserving-tacticscoq-state-preserving-tactics656,17275 -(defvar coq-tacticscoq-tactics660,17373 -(defvar coq-retractable-instructcoq-retractable-instruct663,17462 -(defvar coq-non-retractable-instructcoq-non-retractable-instruct666,17572 -(defvar coq-keywordscoq-keywords670,17694 -(defvar coq-tacticalscoq-tacticals675,17859 -(defvar coq-reserved-commoncoq-reserved-common697,18242 -(defvar coq-reserved-V8coq-reserved-V8713,18435 -(defvar coq-reserved-V7coq-reserved-V7724,18539 -(defvar coq-reserved coq-reserved729,18614 -(defvar coq-symbolscoq-symbols737,18770 -(defvar coq-error-regexp coq-error-regexp755,18974 -(defvar coq-id coq-id758,19190 -(defvar coq-ids coq-ids760,19216 -(defun coq-first-abstr-regexp coq-first-abstr-regexp762,19253 -(defun coq-next-abstr-regexp coq-next-abstr-regexp765,19341 -(defvar coq-font-lock-termscoq-font-lock-terms768,19419 -(defconst coq-save-command-regexp-strictcoq-save-command-regexp-strict783,20072 -(defconst coq-save-command-regexpcoq-save-command-regexp785,20185 -(defconst coq-save-with-hole-regexpcoq-save-with-hole-regexp787,20284 -(defconst coq-goal-command-regexpcoq-goal-command-regexp790,20422 -(defconst coq-goal-with-hole-regexpcoq-goal-with-hole-regexp792,20521 -(defconst coq-decl-with-hole-regexpcoq-decl-with-hole-regexp798,20810 -(defconst coq-defn-with-hole-regexpcoq-defn-with-hole-regexp801,20943 -(defvar coq-font-lock-keywords-1coq-font-lock-keywords-1804,21083 -(defvar coq-font-lock-keywords coq-font-lock-keywords825,22126 -(defun coq-init-syntax-table coq-init-syntax-table827,22184 -(defconst coq-generic-expressioncoq-generic-expression856,23082 +(defvar coq-keywords-declcoq-keywords-decl124,4542 +(defvar coq-keywords-defncoq-keywords-defn139,4898 +(defun coq-count-match coq-count-match213,7254 +(defun coq-goal-command-p coq-goal-command-p225,7674 +(defvar coq-keywords-save-strictcoq-keywords-save-strict245,8258 +(defvar coq-keywords-savecoq-keywords-save253,8355 +(defun coq-save-command-p coq-save-command-p257,8431 +(defvar coq-keywords-kill-goal coq-keywords-kill-goal265,8710 +(defcustom coq-user-state-changing-commands coq-user-state-changing-commands271,8760 +(defcustom coq-user-state-preserving-commands coq-user-state-preserving-commands283,9157 +(defvar coq-keywords-state-preserving-commandscoq-keywords-state-preserving-commands296,9597 +(defvar coq-keywords-state-changing-misc-commandscoq-keywords-state-changing-misc-commands344,10722 +(defvar coq-keywords-state-changing-commandscoq-keywords-state-changing-commands418,12740 +(defvar coq-keywords-commandscoq-keywords-commands428,12937 +(defcustom coq-user-state-changing-tactics coq-user-state-changing-tactics434,13087 +(defvar coq-state-changing-tacticscoq-state-changing-tactics445,13513 +(defcustom coq-user-state-preserving-tactics coq-user-state-preserving-tactics646,16838 +(defvar coq-state-preserving-tacticscoq-state-preserving-tactics657,17252 +(defvar coq-tacticscoq-tactics661,17350 +(defvar coq-retractable-instructcoq-retractable-instruct664,17439 +(defvar coq-non-retractable-instructcoq-non-retractable-instruct667,17549 +(defvar coq-keywordscoq-keywords671,17671 +(defvar coq-tacticalscoq-tacticals676,17836 +(defvar coq-reserved-commoncoq-reserved-common698,18219 +(defvar coq-reserved-V8coq-reserved-V8714,18412 +(defvar coq-reserved-V7coq-reserved-V7725,18516 +(defvar coq-reserved coq-reserved730,18591 +(defvar coq-symbolscoq-symbols738,18747 +(defvar coq-error-regexp coq-error-regexp756,18951 +(defvar coq-id coq-id759,19180 +(defvar coq-ids coq-ids761,19206 +(defun coq-first-abstr-regexp coq-first-abstr-regexp763,19243 +(defun coq-next-abstr-regexp coq-next-abstr-regexp766,19331 +(defvar coq-font-lock-termscoq-font-lock-terms769,19409 +(defconst coq-save-command-regexp-strictcoq-save-command-regexp-strict784,20062 +(defconst coq-save-command-regexpcoq-save-command-regexp786,20175 +(defconst coq-save-with-hole-regexpcoq-save-with-hole-regexp788,20274 +(defconst coq-goal-command-regexpcoq-goal-command-regexp791,20412 +(defconst coq-goal-with-hole-regexpcoq-goal-with-hole-regexp793,20511 +(defconst coq-decl-with-hole-regexpcoq-decl-with-hole-regexp799,20800 +(defconst coq-defn-with-hole-regexpcoq-defn-with-hole-regexp802,20933 +(defvar coq-font-lock-keywords-1coq-font-lock-keywords-1805,21073 +(defvar coq-font-lock-keywords coq-font-lock-keywords826,22116 +(defun coq-init-syntax-table coq-init-syntax-table828,22174 +(defconst coq-generic-expressioncoq-generic-expression857,23072 coq/x-symbol-coq.el,2822 (defvar x-symbol-coq-required-fonts x-symbol-coq-required-fonts16,384 @@ -239,69 +239,6 @@ demoisa/demoisa.el,568 (define-derived-mode demoisa-goals-mode demoisa-goals-mode133,4387 (defun demoisa-pre-shell-start demoisa-pre-shell-start152,5169 -generic/holes.el,3536 -(defun holes-short-doc holes-short-doc24,736 -(defcustom empty-hole-string empty-hole-string149,5370 -(defcustom empty-hole-regexp empty-hole-regexp152,5475 -(defcustom hole-search-limit hole-search-limit155,6075 -(defface active-hole-faceactive-hole-face168,6441 -(defface inactive-hole-faceinactive-hole-face178,6898 -(defun region-beginning-or-nil region-beginning-or-nil197,7434 -(defun region-end-or-nil region-end-or-nil201,7523 -(defun copy-active-region copy-active-region205,7602 -(defun is-hole-p is-hole-p211,7780 -(defun hole-start-position hole-start-position216,7840 -(defun hole-end-position hole-end-position221,7977 -(defun hole-buffer hole-buffer226,8107 -(defun hole-at hole-at231,8229 -(defun active-hole-exist-p active-hole-exist-p240,8417 -(defun active-hole-start-position active-hole-start-position250,8668 -(defun active-hole-end-position active-hole-end-position261,9018 -(defun active-hole-buffer active-hole-buffer273,9364 -(defun goto-active-hole goto-active-hole284,9644 -(defun highlight-hole-as-active highlight-hole-as-active296,9917 -(defun highlight-hole highlight-hole306,10224 -(defun disable-active-hole disable-active-hole317,10519 -(defun set-active-hole set-active-hole335,11028 -(defun is-in-hole-p is-in-hole-p347,11329 -(defun make-hole make-hole357,11474 -(defun make-hole-at make-hole-at382,12289 -(defun clear-hole clear-hole401,12731 -(defun clear-hole-at clear-hole-at411,12948 -(defun map-holes map-holes420,13177 -(defun mapcar-holes mapcar-holes426,13291 -(defun clear-all-buffer-holes clear-all-buffer-holes430,13390 -(defun next-hole next-hole442,13624 -(defun next-after-active-hole next-after-active-hole451,13888 -(defun set-active-hole-next set-active-hole-next458,14068 -(defun set-active-hole-next-after-active set-active-hole-next-after-active475,14425 -(defun replace-segment replace-segment486,14583 -(defun replace-hole replace-hole502,14899 -(defun replace-active-hole replace-active-hole536,16055 -(defun replace-update-active-hole replace-update-active-hole545,16338 -(defun delete-update-active-hole delete-update-active-hole568,16964 -(defun set-make-active-hole set-make-active-hole577,17161 -(defun mouse-replace-active-hole mouse-replace-active-hole624,18508 -(defun destroy-hole destroy-hole642,18984 -(defun hole-at-event hole-at-event657,19295 -(defun mouse-destroy-hole mouse-destroy-hole659,19354 -(defun mouse-forget-hole mouse-forget-hole667,19528 -(defun mouse-set-make-active-hole mouse-set-make-active-hole681,19769 -(defun mouse-set-active-hole mouse-set-active-hole701,20220 -(defun set-point-next-hole-destroy set-point-next-hole-destroy711,20414 -(defun count-char-in-string count-char-in-string775,22661 -(defun count-re-in-string count-re-in-string785,22866 -(defun count-chars-in-last-expand count-chars-in-last-expand795,23077 -(defun count-newlines-in-last-expand count-newlines-in-last-expand799,23166 -(defun indent-last-expand indent-last-expand803,23277 -(defun count-holes-in-last-expand count-holes-in-last-expand818,23603 -(defun replace-string-by-holes replace-string-by-holes822,23722 -(defun replace-string-by-holes-backward replace-string-by-holes-backward841,24148 -(defun replace-string-by-holes-move-point replace-string-by-holes-move-point872,24966 -(defun replace-string-by-holes-backward-move-point replace-string-by-holes-backward-move-point879,25120 -(defun holes-abbrev-complete holes-abbrev-complete889,25296 -(defun insert-and-expand insert-and-expand911,26098 - generic/pg-assoc.el,408 (define-derived-mode proof-universal-keys-only-mode proof-universal-keys-only-mode20,563 (defun proof-associated-buffers proof-associated-buffers32,987 @@ -328,63 +265,131 @@ generic/pg-goals.el,1074 (defun pg-goals-construct-command pg-goals-construct-command348,12775 (defun pg-goals-get-subterm-help pg-goals-get-subterm-help372,13627 -generic/pg-init.el,0 - generic/pg-metadata.el,204 (defcustom pg-metadata-default-directory pg-metadata-default-directory23,628 (defface proof-preparsed-span proof-preparsed-span28,802 (defun pg-metadata-filename-for pg-metadata-filename-for39,1065 -generic/pg-nxml.el,66 -(defun pg-nxml-support-available pg-nxml-support-available9,236 - -generic/pg-pgip.el,1154 -(defalias 'pg-pgip-error pg-pgip-error17,544 -(defun pg-pgip-process-packet pg-pgip-process-packet20,593 -(defun pg-pgip-process-cmds pg-pgip-process-cmds28,981 -(defun pg-pgip-post-process pg-pgip-post-process88,2599 -(defun pg-pgip-haspref pg-pgip-haspref125,3616 -(defun pg-pgip-default-for pg-pgip-default-for188,5899 -(defun pg-pgip-subst-for pg-pgip-subst-for199,6211 -(defun pg-pgip-get-type pg-pgip-get-type206,6372 -(defun pg-pgip-pgiptype pg-pgip-pgiptype213,6594 -(defun pg-pgip-interpret-bool pg-pgip-interpret-bool237,7458 -(defun pg-pgip-interpret-int pg-pgip-interpret-int246,7734 -(defun pg-pgip-interpret-string pg-pgip-interpret-string251,7897 -(defun pg-pgip-interpret-choice pg-pgip-interpret-choice254,7947 -(defun pg-pgip-interpret-value pg-pgip-interpret-value274,8642 -(defun pg-pgip-get-attr pg-pgip-get-attr297,9267 -(defun pg-pgip-get-version pg-pgip-get-version304,9480 -(defun pg-prover-interpret-pgip-command pg-prover-interpret-pgip-command312,9712 -(defun pg-issue-pgip pg-issue-pgip329,10134 -(defun pg-pgip-askprefs pg-pgip-askprefs337,10406 -(defun pg-pgip-parsescript pg-pgip-parsescript346,10618 - -generic/pg-response.el,1673 +generic/pg-pgip.el,4870 +(defalias 'pg-pgip-debug pg-pgip-debug22,725 +(defalias 'pg-pgip-error pg-pgip-error23,766 +(defalias 'pg-pgip-warning pg-pgip-warning24,801 +(defun pg-pgip-process-packet pg-pgip-process-packet27,866 +(defvar pg-pgip-last-seen-id pg-pgip-last-seen-id37,1439 +(defvar pg-pgip-last-seen-seq pg-pgip-last-seen-seq38,1473 +(defun pg-pgip-process-pgip pg-pgip-process-pgip40,1509 +(defun pg-pgip-process-msg pg-pgip-process-msg56,2224 +(defvar pg-pgip-post-process-functionspg-pgip-post-process-functions69,2770 +(defun pg-pgip-post-process pg-pgip-post-process78,3164 +(defun pg-pgip-process-usespgip pg-pgip-process-usespgip94,3775 +(defun pg-pgip-process-usespgml pg-pgip-process-usespgml98,3939 +(defun pg-pgip-process-pgmlconfig pg-pgip-process-pgmlconfig102,4103 +(defun pg-pgip-process-proverinfo pg-pgip-process-proverinfo118,4711 +(defun pg-pgip-process-hasprefs pg-pgip-process-hasprefs135,5365 +(defun pg-pgip-haspref pg-pgip-haspref149,5997 +(defun pg-pgip-process-prefval pg-pgip-process-prefval168,6776 +(defun pg-pgip-process-guiconfig pg-pgip-process-guiconfig195,7485 +(defun pg-pgip-process-ids pg-pgip-process-ids202,7602 +(defalias 'pg-pgip-process-setids pg-pgip-process-setids224,8508 +(defalias 'pg-pgip-process-addids pg-pgip-process-addids225,8564 +(defalias 'pg-pgip-process-delids pg-pgip-process-delids226,8620 +(defun pg-pgip-process-idvalue pg-pgip-process-idvalue229,8678 +(defun pg-pgip-process-menuadd pg-pgip-process-menuadd241,9015 +(defun pg-pgip-process-menudel pg-pgip-process-menudel244,9058 +(defun pg-pgip-process-ready pg-pgip-process-ready253,9291 +(defun pg-pgip-process-cleardisplay pg-pgip-process-cleardisplay256,9332 +(defun pg-pgip-process-proofstate pg-pgip-process-proofstate270,9809 +(defun pg-pgip-process-normalresponse pg-pgip-process-normalresponse274,9886 +(defun pg-pgip-process-errorresponse pg-pgip-process-errorresponse278,10010 +(defun pg-pgip-process-scriptinsert pg-pgip-process-scriptinsert282,10133 +(defun pg-pgip-process-metainforesponse pg-pgip-process-metainforesponse287,10267 +(defun pg-pgip-process-parseresult pg-pgip-process-parseresult290,10319 +(defun pg-pgip-process-informfileloaded pg-pgip-process-informfileloaded299,10555 +(defun pg-pgip-process-informfileretracted pg-pgip-process-informfileretracted305,10821 +(defun pg-pgip-process-brokerstatus pg-pgip-process-brokerstatus318,11295 +(defun pg-pgip-process-proveravailmsg pg-pgip-process-proveravailmsg321,11343 +(defun pg-pgip-process-newprovermsg pg-pgip-process-newprovermsg324,11393 +(defun pg-pgip-process-proverstatusmsg pg-pgip-process-proverstatusmsg327,11441 +(defvar pg-pgip-srcids pg-pgip-srcids336,11688 +(defun pg-pgip-process-newfile pg-pgip-process-newfile340,11795 +(defun pg-pgip-process-filestatus pg-pgip-process-filestatus356,12383 +(defun pg-pgip-process-newobj pg-pgip-process-newobj376,13038 +(defun pg-pgip-process-delobj pg-pgip-process-delobj379,13080 +(defun pg-pgip-process-objectstatus pg-pgip-process-objectstatus382,13122 +(defun pg-pgip-process-parsescript pg-pgip-process-parsescript396,13478 +(defun pg-pgip-get-pgiptype pg-pgip-get-pgiptype419,14354 +(defun pg-pgip-default-for pg-pgip-default-for439,15149 +(defun pg-pgip-subst-for pg-pgip-subst-for452,15544 +(defun pg-pgip-interpret-value pg-pgip-interpret-value464,15887 +(defun pg-pgip-interpret-choice pg-pgip-interpret-choice482,16570 +(defun pg-pgip-get-icon pg-pgip-get-icon513,17643 +(defsubst pg-pgip-get-name pg-pgip-get-name517,17791 +(defsubst pg-pgip-get-version pg-pgip-get-version520,17908 +(defsubst pg-pgip-get-descr pg-pgip-get-descr523,18031 +(defsubst pg-pgip-get-thmname pg-pgip-get-thmname526,18150 +(defsubst pg-pgip-get-thyname pg-pgip-get-thyname529,18273 +(defsubst pg-pgip-get-url pg-pgip-get-url532,18396 +(defsubst pg-pgip-get-srcid pg-pgip-get-srcid535,18511 +(defsubst pg-pgip-get-proverid pg-pgip-get-proverid538,18630 +(defsubst pg-pgip-get-symname pg-pgip-get-symname541,18755 +(defsubst pg-pgip-get-prefcat pg-pgip-get-prefcat544,18875 +(defsubst pg-pgip-get-default pg-pgip-get-default547,19003 +(defsubst pg-pgip-get-objtype pg-pgip-get-objtype550,19126 +(defsubst pg-pgip-get-value pg-pgip-get-value553,19249 +(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext556,19311 +(defun pg-pgip-get-pgmltext pg-pgip-get-pgmltext558,19370 +(defun pg-pgip-string-of-command pg-pgip-string-of-command567,19597 +(defconst pg-pgip-idpg-pgip-id584,20358 +(defvar pg-pgip-refseq pg-pgip-refseq590,20638 +(defvar pg-pgip-refid pg-pgip-refid592,20736 +(defvar pg-pgip-seq pg-pgip-seq595,20830 +(defun pg-pgip-assemble-packet pg-pgip-assemble-packet597,20894 +(defun pg-pgip-issue pg-pgip-issue615,21709 +(defun pg-pgip-askprefs pg-pgip-askprefs632,22322 +(defun pg-pgip-askids pg-pgip-askids636,22436 +(defun pg-pgip-reset pg-pgip-reset649,22727 + +generic/pg-pgip-old.el,734 +(defun pg-pgip-process-oldhaspref pg-pgip-process-oldhaspref18,633 +(defun pg-pgip-process-haspref pg-pgip-process-haspref21,730 +(defun pg-pgip-old-interpret-bool pg-pgip-old-interpret-bool58,2245 +(defun pg-pgip-old-interpret-int pg-pgip-old-interpret-int67,2529 +(defun pg-pgip-old-interpret-string pg-pgip-old-interpret-string72,2696 +(defun pg-pgip-old-interpret-choice pg-pgip-old-interpret-choice75,2750 +(defun pg-pgip-old-interpret-value pg-pgip-old-interpret-value95,3469 +(defun pg-pgip-old-default-for pg-pgip-old-default-for114,4015 +(defun pg-pgip-old-subst-for pg-pgip-old-subst-for125,4339 +(defun pg-pgip-old-get-type pg-pgip-old-get-type132,4504 +(defun pg-pgip-old-pgiptype pg-pgip-old-pgiptype139,4726 + +generic/pg-response.el,1890 (define-derived-mode proof-response-mode proof-response-mode24,597 (defun proof-response-config-done proof-response-config-done47,1490 (defvar proof-shell-special-display-regexp proof-shell-special-display-regexp68,2265 (defconst proof-multiframe-specifiers proof-multiframe-specifiers76,2670 (defun proof-map-multiple-frame-specifiers proof-map-multiple-frame-specifiers85,3034 (defconst proof-multiframe-parametersproof-multiframe-parameters95,3496 -(defun proof-multiple-frames-enable proof-multiple-frames-enable103,3730 -(defun proof-three-window-enable proof-three-window-enable125,4450 -(defun proof-select-three-b proof-select-three-b129,4514 -(defun proof-display-three-b proof-display-three-b144,4983 -(defvar pg-frame-configuration pg-frame-configuration158,5477 -(defun pg-cache-frame-configuration pg-cache-frame-configuration162,5624 -(defun proof-layout-windows proof-layout-windows166,5795 -(defun proof-delete-other-frames proof-delete-other-frames207,7608 -(defvar pg-response-erase-flag pg-response-erase-flag238,8703 -(defun proof-shell-maybe-erase-responseproof-shell-maybe-erase-response241,8818 -(defun pg-response-display pg-response-display271,9968 -(defun pg-response-display-with-face pg-response-display-with-face288,10790 -(defun pg-response-clear-displays pg-response-clear-displays323,12147 -(defvar pg-response-next-error pg-response-next-error340,12677 -(defun proof-next-error proof-next-error344,12799 -(defvar proof-trace-last-fontify-pos proof-trace-last-fontify-pos439,16212 -(defun proof-trace-buffer-display proof-trace-buffer-display442,16304 -(defun pg-thms-buffer-clear pg-thms-buffer-clear482,17517 +(defun proof-multiple-frames-enable proof-multiple-frames-enable104,3795 +(defun proof-three-window-enable proof-three-window-enable126,4515 +(defun proof-select-three-b proof-select-three-b130,4579 +(defun proof-display-three-b proof-display-three-b145,5048 +(defvar pg-frame-configuration pg-frame-configuration159,5542 +(defun pg-cache-frame-configuration pg-cache-frame-configuration163,5689 +(defun proof-layout-windows proof-layout-windows167,5860 +(defun proof-delete-other-frames proof-delete-other-frames208,7673 +(defvar pg-response-erase-flag pg-response-erase-flag239,8768 +(defun proof-shell-maybe-erase-responseproof-shell-maybe-erase-response242,8883 +(defun pg-response-display pg-response-display272,10033 +(defun pg-response-display-with-face pg-response-display-with-face289,10855 +(defun pg-response-clear-displays pg-response-clear-displays324,12212 +(defvar pg-response-next-error pg-response-next-error341,12742 +(defun proof-next-error proof-next-error345,12864 +(defun pg-response-has-error-location pg-response-has-error-location425,15798 +(defvar proof-trace-last-fontify-pos proof-trace-last-fontify-pos448,16631 +(defun proof-trace-fontify-pos proof-trace-fontify-pos450,16674 +(defun proof-trace-buffer-display proof-trace-buffer-display458,16988 +(defun proof-trace-buffer-finish proof-trace-buffer-finish482,17961 +(defun pg-thms-buffer-clear pg-thms-buffer-clear503,18486 generic/pg-thymodes.el,219 (defmacro pg-defthymode pg-defthymode19,466 @@ -393,7 +398,7 @@ generic/pg-thymodes.el,219 (defun pg-modesym pg-modesym78,2520 (defun pg-modesymval pg-modesymval82,2634 -generic/pg-user.el,3521 +generic/pg-user.el,3655 (defmacro proof-maybe-save-point proof-maybe-save-point21,410 (defun proof-maybe-follow-locked-end proof-maybe-follow-locked-end29,612 (defun proof-assert-next-command-interactive proof-assert-next-command-interactive43,977 @@ -439,12 +444,14 @@ generic/pg-user.el,3521 (defun pg-toggle-visibility pg-toggle-visibility938,31093 (defun pg-create-in-span-context-menu pg-create-in-span-context-menu948,31415 (defun pg-goals-buffers-hint pg-goals-buffers-hint1020,33968 -(defun pg-response-buffers-hint pg-response-buffers-hint1023,34135 -(defun pg-jump-to-end-hint pg-jump-to-end-hint1032,34484 -(defun pg-processing-complete-hint pg-processing-complete-hint1035,34600 -(defun pg-hint pg-hint1051,35286 -(defun pg-identifier-under-mouse-query pg-identifier-under-mouse-query1070,35962 -(defun proof-imenu-enable proof-imenu-enable1115,37589 +(defun pg-slow-fontify-tracing-hint pg-slow-fontify-tracing-hint1023,34135 +(defun pg-response-buffers-hint pg-response-buffers-hint1026,34291 +(defun pg-jump-to-end-hint pg-jump-to-end-hint1035,34640 +(defun pg-processing-complete-hint pg-processing-complete-hint1038,34756 +(defun pg-next-error-hint pg-next-error-hint1054,35442 +(defun pg-hint pg-hint1058,35579 +(defun pg-identifier-under-mouse-query pg-identifier-under-mouse-query1077,36255 +(defun proof-imenu-enable proof-imenu-enable1122,37882 generic/pg-xhtml.el,573 (defvar pg-xhtml-dir pg-xhtml-dir17,423 @@ -458,60 +465,25 @@ generic/pg-xhtml.el,573 (defun pg-xhtml-display-file-mozilla pg-xhtml-display-file-mozilla79,2229 (defalias 'pg-xhtml-display-file pg-xhtml-display-file84,2402 -generic/pg-xml.el,1487 -(defconst pg-xml-name pg-xml-name32,848 -(defconst pg-xml-space pg-xml-space33,901 -(defconst pg-xml-ref pg-xml-ref34,936 -(defconst pg-xml-start-open-elt-regexp pg-xml-start-open-elt-regexp36,1012 -(defconst pg-xml-end-open-elt-regexp pg-xml-end-open-elt-regexp38,1106 -(defconst pg-xml-close-elt-regexp pg-xml-close-elt-regexp40,1185 -(defconst pg-xml-attribute-regexp pg-xml-attribute-regexp42,1276 -(defconst pg-xml-attribute-val-regexp pg-xml-attribute-val-regexp44,1364 -(defconst pg-xml-comment-start-regexp pg-xml-comment-start-regexp47,1515 -(defconst pg-xml-comment-end-regexp pg-xml-comment-end-regexp48,1561 -(defconst pg-xml-anymarkup-regexp pg-xml-anymarkup-regexp49,1604 -(defconst pg-xml-special-eltspg-xml-special-elts50,1643 -(defvar xmlparse xmlparse54,1742 -(defun pg-xml-add-text pg-xml-add-text57,1797 -(defun pg-xml-parse-buffer pg-xml-parse-buffer64,2009 -(defun pg-xml-parse-string pg-xml-parse-string171,5979 -(defconst pg-xml-header pg-xml-header188,6468 -(defvar pg-xml-doc pg-xml-doc191,6544 -(defvar pg-xml-openelts pg-xml-openelts194,6634 -(defvar pg-xml-indentp pg-xml-indentp197,6690 -(defun pg-xml-encode-entities pg-xml-encode-entities200,6763 -(defun pg-xml-begin-write pg-xml-begin-write210,7252 -(defun pg-xml-indent pg-xml-indent215,7444 -(defun pg-xml-openelt pg-xml-openelt221,7583 -(defun pg-xml-closeelt pg-xml-closeelt240,8129 -(defun pg-xml-writetext pg-xml-writetext252,8399 -(defun pg-xml-doc pg-xml-doc255,8500 +generic/pg-xml.el,627 +(defun pg-xml-parse-string pg-xml-parse-string38,1118 +(defun pg-xml-parse-buffer pg-xml-parse-buffer49,1452 +(defun pg-xml-get-attr pg-xml-get-attr71,2185 +(defun pg-xml-child-elts pg-xml-child-elts79,2489 +(defun pg-xml-child-elt pg-xml-child-elt84,2694 +(defun pg-xml-get-child pg-xml-get-child92,2977 +(defun pg-xml-get-text-content pg-xml-get-text-content102,3349 +(defmacro pg-xml-attr pg-xml-attr113,3699 +(defmacro pg-xml-node pg-xml-node115,3761 +(defconst pg-xml-header pg-xml-header118,3854 +(defun pg-xml-string-of pg-xml-string-of122,3931 +(defun pg-xml-output-internal pg-xml-output-internal133,4303 generic/_pkg.el,0 generic/proof-autoloads.el,0 -generic/proof-compat.el,999 -(defun pg-custom-undeclare-variable pg-custom-undeclare-variable28,1002 -(defun subst-char-in-string subst-char-in-string99,3142 -(defun replace-regexp-in-string replace-regexp-in-string112,3633 -(defconst menuvisiblep menuvisiblep174,6346 -(defun set-window-text-height set-window-text-height191,6965 -(defmacro save-selected-frame save-selected-frame217,7915 -(defun warn warn256,9217 -(defun redraw-modeline redraw-modeline263,9472 -(defun replace-in-string replace-in-string278,10039 -(defun proof-buffer-syntactic-context-emulate proof-buffer-syntactic-context-emulate327,11557 -(defvar read-shell-command-mapread-shell-command-map360,12864 -(defun read-shell-command read-shell-command378,13566 -(defun remassq remassq390,14047 -(defun remassoc remassoc402,14436 -(defun frames-of-buffer frames-of-buffer415,14881 -(defmacro with-selected-window with-selected-window454,16144 -(defun pg-pop-to-buffer pg-pop-to-buffer490,17269 -(defun process-live-p process-live-p541,19121 - -generic/proof-config.el,16702 +generic/proof-config.el,16775 (defgroup proof-user-options proof-user-options84,3173 (defcustom proof-electric-terminator-enable proof-electric-terminator-enable89,3287 (defcustom proof-toolbar-enable proof-toolbar-enable101,3821 @@ -544,196 +516,197 @@ generic/proof-config.el,16702 (defgroup proof-faces proof-faces433,16394 (defmacro proof-face-specs proof-face-specs438,16500 (defface proof-queue-face proof-queue-face453,16946 -(defface proof-locked-faceproof-locked-face461,17219 -(defface proof-declaration-name-faceproof-declaration-name-face469,17477 -(defconst proof-declaration-name-face proof-declaration-name-face481,17870 -(defface proof-tacticals-name-faceproof-tacticals-name-face486,18106 -(defconst proof-tacticals-name-face proof-tacticals-name-face495,18368 -(defface proof-tactics-name-faceproof-tactics-name-face500,18598 -(defconst proof-tactics-name-face proof-tactics-name-face509,18863 -(defface proof-error-face proof-error-face514,19087 -(defface proof-warning-faceproof-warning-face522,19294 -(defface proof-eager-annotation-faceproof-eager-annotation-face531,19551 -(defface proof-debug-message-faceproof-debug-message-face539,19769 -(defface proof-boring-faceproof-boring-face547,19968 -(defface proof-mouse-highlight-faceproof-mouse-highlight-face555,20160 -(defface proof-highlight-dependent-faceproof-highlight-dependent-face563,20356 -(defface proof-highlight-dependency-faceproof-highlight-dependency-face571,20565 -(defgroup prover-config prover-config589,20824 -(defcustom proof-mode-for-shell proof-mode-for-shell623,21943 -(defcustom proof-mode-for-response proof-mode-for-response630,22190 -(defcustom proof-mode-for-goals proof-mode-for-goals637,22473 -(defcustom proof-mode-for-script proof-mode-for-script644,22728 -(defcustom proof-guess-command-line proof-guess-command-line655,23162 -(defcustom proof-assistant-home-page proof-assistant-home-page670,23659 -(defcustom proof-context-command proof-context-command676,23829 -(defcustom proof-info-command proof-info-command681,23963 -(defcustom proof-showproof-command proof-showproof-command688,24235 -(defcustom proof-goal-command proof-goal-command693,24371 -(defcustom proof-save-command proof-save-command701,24669 -(defcustom proof-find-theorems-command proof-find-theorems-command709,24979 -(defconst proof-toolbar-entries-defaultproof-toolbar-entries-default716,25288 -(defpgcustom toolbar-entries toolbar-entries747,27020 -(defcustom proof-assistant-true-value proof-assistant-true-value765,27741 -(defcustom proof-assistant-false-value proof-assistant-false-value771,27931 -(defcustom proof-assistant-format-int-fn proof-assistant-format-int-fn777,28125 -(defcustom proof-assistant-format-string-fn proof-assistant-format-string-fn784,28374 -(defcustom proof-assistant-setting-format proof-assistant-setting-format791,28641 -(defgroup proof-script proof-script813,29336 -(defcustom proof-terminal-char proof-terminal-char818,29466 -(defcustom proof-script-sexp-commands proof-script-sexp-commands828,29870 -(defcustom proof-script-command-end-regexp proof-script-command-end-regexp839,30340 -(defcustom proof-script-command-start-regexp proof-script-command-start-regexp857,31159 -(defcustom proof-script-use-old-parser proof-script-use-old-parser868,31621 -(defcustom proof-script-integral-proofs proof-script-integral-proofs880,32110 -(defcustom proof-script-fly-past-comments proof-script-fly-past-comments895,32766 -(defcustom proof-script-parse-function proof-script-parse-function902,33083 -(defcustom proof-script-comment-start proof-script-comment-start920,33729 -(defcustom proof-script-comment-start-regexp proof-script-comment-start-regexp931,34164 -(defcustom proof-script-comment-end proof-script-comment-end939,34481 -(defcustom proof-script-comment-end-regexp proof-script-comment-end-regexp951,34899 -(defcustom pg-insert-output-as-comment-fn pg-insert-output-as-comment-fn959,35210 -(defcustom proof-string-start-regexp proof-string-start-regexp965,35462 -(defcustom proof-string-end-regexp proof-string-end-regexp970,35627 -(defcustom proof-case-fold-search proof-case-fold-search975,35788 -(defcustom proof-save-command-regexp proof-save-command-regexp984,36204 -(defcustom proof-save-with-hole-regexp proof-save-with-hole-regexp989,36315 -(defcustom proof-save-with-hole-result proof-save-with-hole-result1001,36767 -(defcustom proof-goal-command-regexp proof-goal-command-regexp1012,37231 -(defcustom proof-goal-with-hole-regexp proof-goal-with-hole-regexp1021,37623 -(defcustom proof-goal-with-hole-result proof-goal-with-hole-result1033,38067 -(defcustom proof-non-undoables-regexp proof-non-undoables-regexp1043,38466 -(defcustom proof-nested-undo-regexp proof-nested-undo-regexp1054,38922 -(defcustom proof-ignore-for-undo-count proof-ignore-for-undo-count1070,39634 -(defcustom proof-script-next-entity-regexps proof-script-next-entity-regexps1078,39937 -(defcustom proof-script-find-next-entity-fnproof-script-find-next-entity-fn1122,41671 -(defcustom proof-script-imenu-generic-expression proof-script-imenu-generic-expression1142,42501 -(defcustom proof-goal-command-p proof-goal-command-p1157,43162 -(defcustom proof-really-save-command-p proof-really-save-command-p1184,44598 -(defcustom proof-completed-proof-behaviour proof-completed-proof-behaviour1196,45059 -(defcustom proof-count-undos-fn proof-count-undos-fn1224,46419 -(defconst proof-no-command proof-no-command1259,48020 -(defcustom proof-find-and-forget-fn proof-find-and-forget-fn1264,48224 -(defcustom proof-forget-id-command proof-forget-id-command1281,48935 -(defcustom pg-topterm-goalhyp-fn pg-topterm-goalhyp-fn1291,49293 -(defcustom proof-kill-goal-command proof-kill-goal-command1303,49774 -(defcustom proof-undo-n-times-cmd proof-undo-n-times-cmd1317,50284 -(defcustom proof-nested-goals-history-p proof-nested-goals-history-p1331,50833 -(defcustom proof-state-preserving-p proof-state-preserving-p1340,51171 -(defcustom proof-activate-scripting-hook proof-activate-scripting-hook1350,51641 -(defcustom proof-deactivate-scripting-hook proof-deactivate-scripting-hook1369,52419 -(defcustom proof-indent proof-indent1382,52784 -(defcustom proof-indent-pad-eol proof-indent-pad-eol1388,52958 -(defcustom proof-indent-hang proof-indent-hang1395,53198 -(defcustom proof-indent-enclose-offset proof-indent-enclose-offset1400,53324 -(defcustom proof-indent-open-offset proof-indent-open-offset1405,53466 -(defcustom proof-indent-close-offset proof-indent-close-offset1410,53603 -(defcustom proof-indent-any-regexp proof-indent-any-regexp1415,53741 -(defcustom proof-indent-inner-regexp proof-indent-inner-regexp1420,53901 -(defcustom proof-indent-enclose-regexp proof-indent-enclose-regexp1425,54055 -(defcustom proof-indent-open-regexp proof-indent-open-regexp1430,54209 -(defcustom proof-indent-close-regexp proof-indent-close-regexp1435,54361 -(defcustom proof-script-font-lock-keywords proof-script-font-lock-keywords1441,54515 -(defcustom proof-script-syntax-table-entries proof-script-syntax-table-entries1449,54838 -(defcustom proof-script-span-context-menu-extensions proof-script-span-context-menu-extensions1467,55235 -(defgroup proof-shell proof-shell1493,56024 -(defcustom proof-prog-name proof-prog-name1503,56195 -(defcustom proof-shell-auto-terminate-commands proof-shell-auto-terminate-commands1512,56550 -(defcustom proof-shell-pre-sync-init-cmd proof-shell-pre-sync-init-cmd1521,56947 -(defcustom proof-shell-init-cmd proof-shell-init-cmd1535,57506 -(defcustom proof-shell-restart-cmd proof-shell-restart-cmd1546,57976 -(defcustom proof-shell-quit-cmd proof-shell-quit-cmd1551,58131 -(defcustom proof-shell-quit-timeout proof-shell-quit-timeout1556,58298 -(defcustom proof-shell-cd-cmd proof-shell-cd-cmd1566,58746 -(defcustom proof-shell-start-silent-cmd proof-shell-start-silent-cmd1583,59413 -(defcustom proof-shell-stop-silent-cmd proof-shell-stop-silent-cmd1592,59789 -(defcustom proof-shell-silent-threshold proof-shell-silent-threshold1601,60126 -(defcustom proof-shell-inform-file-processed-cmd proof-shell-inform-file-processed-cmd1609,60460 -(defcustom proof-shell-inform-file-retracted-cmd proof-shell-inform-file-retracted-cmd1630,61383 -(defcustom proof-auto-multiple-files proof-auto-multiple-files1658,62654 -(defcustom proof-cannot-reopen-processed-files proof-cannot-reopen-processed-files1673,63375 -(defcustom proof-shell-require-command-regexp proof-shell-require-command-regexp1687,64042 -(defcustom proof-done-advancing-require-function proof-done-advancing-require-function1698,64504 -(defcustom proof-shell-prompt-pattern proof-shell-prompt-pattern1716,64877 -(defcustom proof-shell-wakeup-char proof-shell-wakeup-char1726,65299 -(defcustom proof-shell-annotated-prompt-regexp proof-shell-annotated-prompt-regexp1732,65530 -(defcustom proof-shell-abort-goal-regexp proof-shell-abort-goal-regexp1748,66170 -(defcustom proof-shell-error-regexp proof-shell-error-regexp1753,66305 -(defcustom proof-shell-truncate-before-error proof-shell-truncate-before-error1773,67099 -(defcustom pg-next-error-regexp pg-next-error-regexp1787,67642 -(defcustom pg-next-error-filename-regexp pg-next-error-filename-regexp1802,68252 -(defcustom pg-next-error-extract-filename pg-next-error-extract-filename1826,69290 -(defcustom proof-shell-interrupt-regexp proof-shell-interrupt-regexp1833,69533 -(defcustom proof-shell-proof-completed-regexp proof-shell-proof-completed-regexp1847,70125 -(defcustom proof-shell-clear-response-regexp proof-shell-clear-response-regexp1860,70633 -(defcustom proof-shell-clear-goals-regexp proof-shell-clear-goals-regexp1867,70932 -(defcustom proof-shell-start-goals-regexp proof-shell-start-goals-regexp1874,71225 -(defcustom proof-shell-end-goals-regexp proof-shell-end-goals-regexp1882,71592 -(defcustom proof-shell-eager-annotation-start proof-shell-eager-annotation-start1888,71834 -(defcustom proof-shell-eager-annotation-start-length proof-shell-eager-annotation-start-length1906,72572 -(defcustom proof-shell-eager-annotation-end proof-shell-eager-annotation-end1917,72999 -(defcustom proof-shell-assumption-regexp proof-shell-assumption-regexp1933,73675 -(defcustom proof-shell-process-file proof-shell-process-file1943,74087 -(defcustom proof-shell-retract-files-regexp proof-shell-retract-files-regexp1965,75039 -(defcustom proof-shell-compute-new-files-list proof-shell-compute-new-files-list1974,75375 -(defcustom pg-use-specials-for-fontify pg-use-specials-for-fontify1986,75920 -(defcustom proof-shell-set-elisp-variable-regexp proof-shell-set-elisp-variable-regexp1994,76244 -(defcustom proof-shell-match-pgip-cmd proof-shell-match-pgip-cmd2027,77716 -(defcustom proof-shell-issue-pgip-cmd proof-shell-issue-pgip-cmd2036,78046 -(defcustom proof-shell-query-dependencies-cmd proof-shell-query-dependencies-cmd2045,78402 -(defcustom proof-shell-theorem-dependency-list-regexp proof-shell-theorem-dependency-list-regexp2052,78662 -(defcustom proof-shell-theorem-dependency-list-split proof-shell-theorem-dependency-list-split2068,79322 -(defcustom proof-shell-show-dependency-cmd proof-shell-show-dependency-cmd2077,79747 -(defcustom proof-shell-identifier-under-mouse-cmd proof-shell-identifier-under-mouse-cmd2084,80016 -(defcustom proof-shell-trace-output-regexp proof-shell-trace-output-regexp2107,81097 -(defcustom proof-shell-thms-output-regexp proof-shell-thms-output-regexp2123,81641 -(defcustom proof-shell-filename-escapes proof-shell-filename-escapes2135,82026 -(defcustom proof-shell-process-connection-type proof-shell-process-connection-type2152,82706 -(defcustom proof-shell-strip-crs-from-input proof-shell-strip-crs-from-input2172,83584 -(defcustom proof-shell-strip-crs-from-output proof-shell-strip-crs-from-output2184,84073 -(defcustom proof-shell-insert-hook proof-shell-insert-hook2192,84441 -(defcustom proof-pre-shell-start-hook proof-pre-shell-start-hook2232,86405 -(defcustom proof-shell-handle-delayed-output-hookproof-shell-handle-delayed-output-hook2248,86877 -(defcustom proof-shell-handle-error-or-interrupt-hookproof-shell-handle-error-or-interrupt-hook2254,87092 -(defcustom proof-shell-pre-interrupt-hookproof-shell-pre-interrupt-hook2269,87706 -(defcustom proof-shell-process-output-system-specific proof-shell-process-output-system-specific2279,88076 -(defcustom proof-state-change-hook proof-state-change-hook2298,88941 -(defcustom proof-shell-font-lock-keywords proof-shell-font-lock-keywords2309,89323 -(defcustom proof-shell-syntax-table-entries proof-shell-syntax-table-entries2317,89651 -(defgroup proof-goals proof-goals2335,90023 -(defcustom pg-subterm-first-special-char pg-subterm-first-special-char2340,90144 -(defcustom pg-subterm-anns-use-stack pg-subterm-anns-use-stack2348,90456 -(defcustom pg-goals-change-goal pg-goals-change-goal2357,90760 -(defcustom pbp-goal-command pbp-goal-command2362,90875 -(defcustom pbp-hyp-command pbp-hyp-command2367,91031 -(defcustom pg-subterm-help-cmd pg-subterm-help-cmd2372,91193 -(defcustom pg-goals-error-regexp pg-goals-error-regexp2379,91429 -(defcustom proof-shell-result-start proof-shell-result-start2384,91589 -(defcustom proof-shell-result-end proof-shell-result-end2390,91823 -(defcustom pg-subterm-start-char pg-subterm-start-char2396,92036 -(defcustom pg-subterm-sep-char pg-subterm-sep-char2410,92618 -(defcustom pg-subterm-end-char pg-subterm-end-char2416,92797 -(defcustom pg-topterm-char pg-topterm-char2422,92954 -(defcustom proof-goals-font-lock-keywords proof-goals-font-lock-keywords2439,93560 -(defcustom proof-resp-font-lock-keywords proof-resp-font-lock-keywords2453,94239 -(defcustom pg-before-fontify-output-hook pg-before-fontify-output-hook2465,94817 -(defcustom pg-after-fontify-output-hook pg-after-fontify-output-hook2473,95177 -(defgroup proof-x-symbol proof-x-symbol2485,95431 -(defcustom proof-xsym-extra-modes proof-xsym-extra-modes2490,95559 -(defcustom proof-xsym-font-lock-keywords proof-xsym-font-lock-keywords2503,96188 -(defcustom proof-xsym-activate-command proof-xsym-activate-command2511,96565 -(defcustom proof-xsym-deactivate-command proof-xsym-deactivate-command2518,96801 -(defpgcustom x-symbol-language x-symbol-language2525,97043 -(defpgcustom favourites favourites2540,97490 -(defpgcustom menu-entries menu-entries2545,97680 -(defpgcustom help-menu-entries help-menu-entries2552,97917 -(defpgcustom keymap keymap2559,98180 -(defpgcustom completion-table completion-table2564,98351 -(defpgcustom tags-program tags-program2574,98716 -(defcustom proof-general-name proof-general-name2586,98889 -(defcustom proof-general-home-pageproof-general-home-page2591,99046 -(defcustom proof-unnamed-theorem-nameproof-unnamed-theorem-name2597,99205 -(defcustom proof-universal-keysproof-universal-keys2605,99481 +(defface proof-locked-faceproof-locked-face461,17226 +(defface proof-declaration-name-faceproof-declaration-name-face474,17729 +(defconst proof-declaration-name-face proof-declaration-name-face486,18122 +(defface proof-tacticals-name-faceproof-tacticals-name-face491,18358 +(defconst proof-tacticals-name-face proof-tacticals-name-face500,18620 +(defface proof-tactics-name-faceproof-tactics-name-face505,18850 +(defconst proof-tactics-name-face proof-tactics-name-face514,19115 +(defface proof-error-face proof-error-face519,19339 +(defface proof-warning-faceproof-warning-face527,19546 +(defface proof-eager-annotation-faceproof-eager-annotation-face536,19803 +(defface proof-debug-message-faceproof-debug-message-face544,20021 +(defface proof-boring-faceproof-boring-face552,20220 +(defface proof-mouse-highlight-faceproof-mouse-highlight-face560,20412 +(defface proof-highlight-dependent-faceproof-highlight-dependent-face568,20608 +(defface proof-highlight-dependency-faceproof-highlight-dependency-face576,20817 +(defgroup prover-config prover-config594,21076 +(defcustom proof-mode-for-shell proof-mode-for-shell628,22195 +(defcustom proof-mode-for-response proof-mode-for-response635,22442 +(defcustom proof-mode-for-goals proof-mode-for-goals642,22725 +(defcustom proof-mode-for-script proof-mode-for-script649,22980 +(defcustom proof-guess-command-line proof-guess-command-line660,23414 +(defcustom proof-assistant-home-page proof-assistant-home-page675,23911 +(defcustom proof-context-command proof-context-command681,24081 +(defcustom proof-info-command proof-info-command686,24215 +(defcustom proof-showproof-command proof-showproof-command693,24487 +(defcustom proof-goal-command proof-goal-command698,24623 +(defcustom proof-save-command proof-save-command706,24921 +(defcustom proof-find-theorems-command proof-find-theorems-command714,25231 +(defconst proof-toolbar-entries-defaultproof-toolbar-entries-default721,25540 +(defpgcustom toolbar-entries toolbar-entries752,27272 +(defcustom proof-assistant-true-value proof-assistant-true-value770,27993 +(defcustom proof-assistant-false-value proof-assistant-false-value776,28183 +(defcustom proof-assistant-format-int-fn proof-assistant-format-int-fn782,28377 +(defcustom proof-assistant-format-string-fn proof-assistant-format-string-fn789,28626 +(defcustom proof-assistant-setting-format proof-assistant-setting-format796,28893 +(defgroup proof-script proof-script818,29588 +(defcustom proof-terminal-char proof-terminal-char823,29718 +(defcustom proof-script-sexp-commands proof-script-sexp-commands833,30122 +(defcustom proof-script-command-end-regexp proof-script-command-end-regexp844,30592 +(defcustom proof-script-command-start-regexp proof-script-command-start-regexp862,31411 +(defcustom proof-script-use-old-parser proof-script-use-old-parser873,31873 +(defcustom proof-script-integral-proofs proof-script-integral-proofs885,32362 +(defcustom proof-script-fly-past-comments proof-script-fly-past-comments900,33018 +(defcustom proof-script-parse-function proof-script-parse-function907,33335 +(defcustom proof-script-comment-start proof-script-comment-start925,33981 +(defcustom proof-script-comment-start-regexp proof-script-comment-start-regexp936,34416 +(defcustom proof-script-comment-end proof-script-comment-end944,34733 +(defcustom proof-script-comment-end-regexp proof-script-comment-end-regexp956,35151 +(defcustom pg-insert-output-as-comment-fn pg-insert-output-as-comment-fn964,35462 +(defcustom proof-string-start-regexp proof-string-start-regexp970,35714 +(defcustom proof-string-end-regexp proof-string-end-regexp975,35879 +(defcustom proof-case-fold-search proof-case-fold-search980,36040 +(defcustom proof-save-command-regexp proof-save-command-regexp989,36456 +(defcustom proof-save-with-hole-regexp proof-save-with-hole-regexp994,36567 +(defcustom proof-save-with-hole-result proof-save-with-hole-result1006,37019 +(defcustom proof-goal-command-regexp proof-goal-command-regexp1017,37483 +(defcustom proof-goal-with-hole-regexp proof-goal-with-hole-regexp1026,37875 +(defcustom proof-goal-with-hole-result proof-goal-with-hole-result1038,38319 +(defcustom proof-non-undoables-regexp proof-non-undoables-regexp1048,38718 +(defcustom proof-nested-undo-regexp proof-nested-undo-regexp1059,39174 +(defcustom proof-ignore-for-undo-count proof-ignore-for-undo-count1075,39886 +(defcustom proof-script-next-entity-regexps proof-script-next-entity-regexps1083,40189 +(defcustom proof-script-find-next-entity-fnproof-script-find-next-entity-fn1127,41923 +(defcustom proof-script-imenu-generic-expression proof-script-imenu-generic-expression1147,42753 +(defcustom proof-goal-command-p proof-goal-command-p1162,43414 +(defcustom proof-really-save-command-p proof-really-save-command-p1189,44850 +(defcustom proof-completed-proof-behaviour proof-completed-proof-behaviour1201,45311 +(defcustom proof-count-undos-fn proof-count-undos-fn1229,46671 +(defconst proof-no-command proof-no-command1264,48272 +(defcustom proof-find-and-forget-fn proof-find-and-forget-fn1269,48476 +(defcustom proof-forget-id-command proof-forget-id-command1286,49187 +(defcustom pg-topterm-goalhyp-fn pg-topterm-goalhyp-fn1296,49545 +(defcustom proof-kill-goal-command proof-kill-goal-command1308,50026 +(defcustom proof-undo-n-times-cmd proof-undo-n-times-cmd1322,50536 +(defcustom proof-nested-goals-history-p proof-nested-goals-history-p1336,51085 +(defcustom proof-state-preserving-p proof-state-preserving-p1345,51423 +(defcustom proof-activate-scripting-hook proof-activate-scripting-hook1355,51893 +(defcustom proof-deactivate-scripting-hook proof-deactivate-scripting-hook1374,52671 +(defcustom proof-indent proof-indent1387,53036 +(defcustom proof-indent-pad-eol proof-indent-pad-eol1393,53210 +(defcustom proof-indent-hang proof-indent-hang1400,53450 +(defcustom proof-indent-enclose-offset proof-indent-enclose-offset1405,53576 +(defcustom proof-indent-open-offset proof-indent-open-offset1410,53718 +(defcustom proof-indent-close-offset proof-indent-close-offset1415,53855 +(defcustom proof-indent-any-regexp proof-indent-any-regexp1420,53993 +(defcustom proof-indent-inner-regexp proof-indent-inner-regexp1425,54153 +(defcustom proof-indent-enclose-regexp proof-indent-enclose-regexp1430,54307 +(defcustom proof-indent-open-regexp proof-indent-open-regexp1435,54461 +(defcustom proof-indent-close-regexp proof-indent-close-regexp1440,54613 +(defcustom proof-script-font-lock-keywords proof-script-font-lock-keywords1446,54767 +(defcustom proof-script-syntax-table-entries proof-script-syntax-table-entries1454,55090 +(defcustom proof-script-span-context-menu-extensions proof-script-span-context-menu-extensions1472,55487 +(defgroup proof-shell proof-shell1498,56276 +(defcustom proof-prog-name proof-prog-name1508,56447 +(defcustom proof-shell-auto-terminate-commands proof-shell-auto-terminate-commands1517,56802 +(defcustom proof-shell-pre-sync-init-cmd proof-shell-pre-sync-init-cmd1526,57199 +(defcustom proof-shell-init-cmd proof-shell-init-cmd1540,57758 +(defcustom proof-shell-restart-cmd proof-shell-restart-cmd1551,58228 +(defcustom proof-shell-quit-cmd proof-shell-quit-cmd1556,58383 +(defcustom proof-shell-quit-timeout proof-shell-quit-timeout1561,58550 +(defcustom proof-shell-cd-cmd proof-shell-cd-cmd1571,58998 +(defcustom proof-shell-start-silent-cmd proof-shell-start-silent-cmd1588,59665 +(defcustom proof-shell-stop-silent-cmd proof-shell-stop-silent-cmd1597,60041 +(defcustom proof-shell-silent-threshold proof-shell-silent-threshold1606,60378 +(defcustom proof-shell-inform-file-processed-cmd proof-shell-inform-file-processed-cmd1614,60712 +(defcustom proof-shell-inform-file-retracted-cmd proof-shell-inform-file-retracted-cmd1635,61635 +(defcustom proof-auto-multiple-files proof-auto-multiple-files1663,62906 +(defcustom proof-cannot-reopen-processed-files proof-cannot-reopen-processed-files1678,63627 +(defcustom proof-shell-require-command-regexp proof-shell-require-command-regexp1692,64294 +(defcustom proof-done-advancing-require-function proof-done-advancing-require-function1703,64756 +(defcustom proof-shell-quiet-errors proof-shell-quiet-errors1709,64996 +(defcustom proof-shell-prompt-pattern proof-shell-prompt-pattern1726,65334 +(defcustom proof-shell-wakeup-char proof-shell-wakeup-char1736,65756 +(defcustom proof-shell-annotated-prompt-regexp proof-shell-annotated-prompt-regexp1742,65987 +(defcustom proof-shell-abort-goal-regexp proof-shell-abort-goal-regexp1758,66627 +(defcustom proof-shell-error-regexp proof-shell-error-regexp1763,66762 +(defcustom proof-shell-truncate-before-error proof-shell-truncate-before-error1783,67556 +(defcustom pg-next-error-regexp pg-next-error-regexp1797,68099 +(defcustom pg-next-error-filename-regexp pg-next-error-filename-regexp1812,68709 +(defcustom pg-next-error-extract-filename pg-next-error-extract-filename1836,69747 +(defcustom proof-shell-interrupt-regexp proof-shell-interrupt-regexp1843,69990 +(defcustom proof-shell-proof-completed-regexp proof-shell-proof-completed-regexp1857,70582 +(defcustom proof-shell-clear-response-regexp proof-shell-clear-response-regexp1870,71090 +(defcustom proof-shell-clear-goals-regexp proof-shell-clear-goals-regexp1877,71389 +(defcustom proof-shell-start-goals-regexp proof-shell-start-goals-regexp1884,71682 +(defcustom proof-shell-end-goals-regexp proof-shell-end-goals-regexp1892,72049 +(defcustom proof-shell-eager-annotation-start proof-shell-eager-annotation-start1898,72291 +(defcustom proof-shell-eager-annotation-start-length proof-shell-eager-annotation-start-length1916,73029 +(defcustom proof-shell-eager-annotation-end proof-shell-eager-annotation-end1927,73456 +(defcustom proof-shell-assumption-regexp proof-shell-assumption-regexp1943,74132 +(defcustom proof-shell-process-file proof-shell-process-file1953,74544 +(defcustom proof-shell-retract-files-regexp proof-shell-retract-files-regexp1975,75496 +(defcustom proof-shell-compute-new-files-list proof-shell-compute-new-files-list1984,75832 +(defcustom pg-use-specials-for-fontify pg-use-specials-for-fontify1996,76377 +(defcustom proof-shell-set-elisp-variable-regexp proof-shell-set-elisp-variable-regexp2004,76701 +(defcustom proof-shell-match-pgip-cmd proof-shell-match-pgip-cmd2037,78173 +(defcustom proof-shell-issue-pgip-cmd proof-shell-issue-pgip-cmd2046,78503 +(defcustom proof-shell-query-dependencies-cmd proof-shell-query-dependencies-cmd2055,78859 +(defcustom proof-shell-theorem-dependency-list-regexp proof-shell-theorem-dependency-list-regexp2062,79119 +(defcustom proof-shell-theorem-dependency-list-split proof-shell-theorem-dependency-list-split2078,79779 +(defcustom proof-shell-show-dependency-cmd proof-shell-show-dependency-cmd2087,80204 +(defcustom proof-shell-identifier-under-mouse-cmd proof-shell-identifier-under-mouse-cmd2094,80473 +(defcustom proof-shell-trace-output-regexp proof-shell-trace-output-regexp2117,81554 +(defcustom proof-shell-thms-output-regexp proof-shell-thms-output-regexp2133,82098 +(defcustom proof-shell-filename-escapes proof-shell-filename-escapes2145,82483 +(defcustom proof-shell-process-connection-type proof-shell-process-connection-type2162,83163 +(defcustom proof-shell-strip-crs-from-input proof-shell-strip-crs-from-input2182,84041 +(defcustom proof-shell-strip-crs-from-output proof-shell-strip-crs-from-output2194,84530 +(defcustom proof-shell-insert-hook proof-shell-insert-hook2202,84898 +(defcustom proof-pre-shell-start-hook proof-pre-shell-start-hook2242,86862 +(defcustom proof-shell-handle-delayed-output-hookproof-shell-handle-delayed-output-hook2258,87334 +(defcustom proof-shell-handle-error-or-interrupt-hookproof-shell-handle-error-or-interrupt-hook2264,87549 +(defcustom proof-shell-pre-interrupt-hookproof-shell-pre-interrupt-hook2279,88163 +(defcustom proof-shell-process-output-system-specific proof-shell-process-output-system-specific2289,88533 +(defcustom proof-state-change-hook proof-state-change-hook2308,89398 +(defcustom proof-shell-font-lock-keywords proof-shell-font-lock-keywords2319,89780 +(defcustom proof-shell-syntax-table-entries proof-shell-syntax-table-entries2327,90108 +(defgroup proof-goals proof-goals2345,90480 +(defcustom pg-subterm-first-special-char pg-subterm-first-special-char2350,90601 +(defcustom pg-subterm-anns-use-stack pg-subterm-anns-use-stack2358,90913 +(defcustom pg-goals-change-goal pg-goals-change-goal2367,91217 +(defcustom pbp-goal-command pbp-goal-command2372,91332 +(defcustom pbp-hyp-command pbp-hyp-command2377,91488 +(defcustom pg-subterm-help-cmd pg-subterm-help-cmd2382,91650 +(defcustom pg-goals-error-regexp pg-goals-error-regexp2389,91886 +(defcustom proof-shell-result-start proof-shell-result-start2394,92046 +(defcustom proof-shell-result-end proof-shell-result-end2400,92280 +(defcustom pg-subterm-start-char pg-subterm-start-char2406,92493 +(defcustom pg-subterm-sep-char pg-subterm-sep-char2420,93075 +(defcustom pg-subterm-end-char pg-subterm-end-char2426,93254 +(defcustom pg-topterm-char pg-topterm-char2432,93411 +(defcustom proof-goals-font-lock-keywords proof-goals-font-lock-keywords2449,94017 +(defcustom proof-resp-font-lock-keywords proof-resp-font-lock-keywords2463,94696 +(defcustom pg-before-fontify-output-hook pg-before-fontify-output-hook2475,95274 +(defcustom pg-after-fontify-output-hook pg-after-fontify-output-hook2483,95634 +(defgroup proof-x-symbol proof-x-symbol2495,95888 +(defcustom proof-xsym-extra-modes proof-xsym-extra-modes2500,96016 +(defcustom proof-xsym-font-lock-keywords proof-xsym-font-lock-keywords2513,96645 +(defcustom proof-xsym-activate-command proof-xsym-activate-command2521,97022 +(defcustom proof-xsym-deactivate-command proof-xsym-deactivate-command2528,97258 +(defpgcustom x-symbol-language x-symbol-language2535,97500 +(defpgcustom favourites favourites2550,97947 +(defpgcustom menu-entries menu-entries2555,98137 +(defpgcustom help-menu-entries help-menu-entries2562,98374 +(defpgcustom keymap keymap2569,98637 +(defpgcustom completion-table completion-table2574,98808 +(defpgcustom tags-program tags-program2584,99173 +(defcustom proof-general-name proof-general-name2596,99346 +(defcustom proof-general-home-pageproof-general-home-page2601,99503 +(defcustom proof-unnamed-theorem-nameproof-unnamed-theorem-name2607,99662 +(defcustom proof-universal-keysproof-universal-keys2615,99938 generic/proof-depends.el,1325 (defvar proof-thm-names-of-files proof-thm-names-of-files19,540 @@ -837,33 +810,33 @@ generic/proof-menu.el,4166 (defun proof-menu-define-favourites-menu proof-menu-define-favourites-menu496,17589 (defmacro proof-defshortcut proof-defshortcut517,18260 (defmacro proof-definvisible proof-definvisible533,18915 -(defun proof-def-favourite proof-def-favourite548,19534 -(defvar proof-make-favourite-cmd-history proof-make-favourite-cmd-history571,20509 -(defvar proof-make-favourite-menu-history proof-make-favourite-menu-history574,20594 -(defun proof-save-favourites proof-save-favourites577,20680 -(defun proof-del-favourite proof-del-favourite582,20828 -(defun proof-read-favourite proof-read-favourite599,21389 -(defun proof-add-favourite proof-add-favourite624,22192 -(defvar proof-assistant-settings proof-assistant-settings651,23243 -(defvar proof-menu-settings proof-menu-settings658,23606 -(defun proof-menu-define-settings-menu proof-menu-define-settings-menu661,23680 -(defun proof-menu-entry-name proof-menu-entry-name679,24324 -(defun proof-menu-entry-for-setting proof-menu-entry-for-setting684,24483 -(defun proof-settings-vars proof-settings-vars702,24973 -(defun proof-settings-changed-from-defaults-p proof-settings-changed-from-defaults-p707,25150 -(defun proof-settings-changed-from-saved-p proof-settings-changed-from-saved-p711,25256 -(defun proof-settings-save proof-settings-save715,25359 -(defun proof-settings-reset proof-settings-reset720,25526 -(defun proof-defpacustom-fn proof-defpacustom-fn728,25772 -(defmacro defpacustom defpacustom793,28165 -(defun proof-assistant-invisible-command-ifposs proof-assistant-invisible-command-ifposs804,28805 -(defun proof-maybe-askprefs proof-maybe-askprefs826,29780 -(defun proof-assistant-settings-cmd proof-assistant-settings-cmd833,29984 -(defun proof-assistant-format proof-assistant-format850,30644 -(defvar proof-assistant-format-table proof-assistant-format-table867,31386 -(defun proof-assistant-format-bool proof-assistant-format-bool875,31755 -(defun proof-assistant-format-int proof-assistant-format-int878,31868 -(defun proof-assistant-format-string proof-assistant-format-string881,31960 +(defun proof-def-favourite proof-def-favourite554,19740 +(defvar proof-make-favourite-cmd-history proof-make-favourite-cmd-history577,20715 +(defvar proof-make-favourite-menu-history proof-make-favourite-menu-history580,20800 +(defun proof-save-favourites proof-save-favourites583,20886 +(defun proof-del-favourite proof-del-favourite588,21034 +(defun proof-read-favourite proof-read-favourite605,21595 +(defun proof-add-favourite proof-add-favourite630,22398 +(defvar proof-assistant-settings proof-assistant-settings657,23449 +(defvar proof-menu-settings proof-menu-settings664,23812 +(defun proof-menu-define-settings-menu proof-menu-define-settings-menu667,23886 +(defun proof-menu-entry-name proof-menu-entry-name687,24630 +(defun proof-menu-entry-for-setting proof-menu-entry-for-setting699,25102 +(defun proof-settings-vars proof-settings-vars717,25592 +(defun proof-settings-changed-from-defaults-p proof-settings-changed-from-defaults-p722,25769 +(defun proof-settings-changed-from-saved-p proof-settings-changed-from-saved-p726,25875 +(defun proof-settings-save proof-settings-save730,25978 +(defun proof-settings-reset proof-settings-reset735,26145 +(defun proof-defpacustom-fn proof-defpacustom-fn743,26391 +(defmacro defpacustom defpacustom819,29275 +(defun proof-assistant-invisible-command-ifposs proof-assistant-invisible-command-ifposs830,29916 +(defun proof-maybe-askprefs proof-maybe-askprefs852,30891 +(defun proof-assistant-settings-cmd proof-assistant-settings-cmd859,31095 +(defun proof-assistant-format proof-assistant-format876,31755 +(defvar proof-assistant-format-table proof-assistant-format-table900,32814 +(defun proof-assistant-format-bool proof-assistant-format-bool908,33183 +(defun proof-assistant-format-int proof-assistant-format-int911,33296 +(defun proof-assistant-format-string proof-assistant-format-string914,33388 generic/proof-mmm.el,179 (defun proof-mmm-support-available proof-mmm-support-available25,909 @@ -906,85 +879,85 @@ generic/proof-script.el,8107 (defun proof-only-whitespace-to-locked-region-p proof-only-whitespace-to-locked-region-p420,14842 (defun proof-in-locked-region-p proof-in-locked-region-p433,15478 (defun proof-goto-end-of-locked proof-goto-end-of-locked445,15741 -(defun proof-goto-end-of-locked-if-pos-not-visible-in-window proof-goto-end-of-locked-if-pos-not-visible-in-window459,16352 -(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window470,16833 -(defun proof-end-of-locked-visible-p proof-end-of-locked-visible-p484,17486 -(defun proof-goto-end-of-queue-or-locked-if-not-visible proof-goto-end-of-queue-or-locked-if-not-visible493,17937 -(defvar pg-idioms pg-idioms512,18587 -(defvar pg-visibility-specs pg-visibility-specs515,18683 -(deflocal pg-script-portions pg-script-portions520,18890 -(defun pg-clear-script-portions pg-clear-script-portions523,19012 -(defun pg-add-script-element pg-add-script-element541,19676 -(defun pg-remove-script-element pg-remove-script-element544,19752 -(defsubst pg-visname pg-visname552,20030 -(defun pg-add-element pg-add-element556,20175 -(defun pg-open-invisible-span pg-open-invisible-span590,21804 -(defun pg-remove-element pg-remove-element601,22167 -(defun pg-make-element-invisible pg-make-element-invisible608,22437 -(defun pg-make-element-visible pg-make-element-visible614,22694 -(defun pg-toggle-element-visibility pg-toggle-element-visibility619,22873 -(defun pg-redisplay-for-gnuemacs pg-redisplay-for-gnuemacs627,23203 -(defun pg-show-all-portions pg-show-all-portions634,23474 -(defun pg-show-all-proofs pg-show-all-proofs652,24145 -(defun pg-hide-all-proofs pg-hide-all-proofs657,24273 -(defun pg-add-proof-element pg-add-proof-element662,24404 -(defun pg-span-name pg-span-name676,25024 -(defun pg-set-span-helphighlights pg-set-span-helphighlights697,25731 -(defun proof-complete-buffer-atomic proof-complete-buffer-atomic722,26555 -(defun proof-register-possibly-new-processed-file proof-register-possibly-new-processed-file763,28470 -(defun proof-inform-prover-file-retracted proof-inform-prover-file-retracted814,30598 -(defun proof-auto-retract-dependencies proof-auto-retract-dependencies833,31384 -(defun proof-unregister-buffer-file-name proof-unregister-buffer-file-name887,33924 -(defun proof-protected-process-or-retract proof-protected-process-or-retract933,35747 -(defun proof-deactivate-scripting-auto proof-deactivate-scripting-auto960,36917 -(defun proof-deactivate-scripting proof-deactivate-scripting969,37275 -(defun proof-activate-scripting proof-activate-scripting1106,42680 -(defun proof-toggle-active-scripting proof-toggle-active-scripting1234,48434 -(defun proof-done-advancing proof-done-advancing1275,49795 -(defun proof-done-advancing-comment proof-done-advancing-comment1360,53200 -(defun proof-done-advancing-save proof-done-advancing-save1379,53942 -(defun proof-make-goalsave proof-make-goalsave1472,57555 -(defun proof-get-name-from-goal proof-get-name-from-goal1487,58298 -(defun proof-done-advancing-autosave proof-done-advancing-autosave1506,59324 -(defun proof-done-advancing-other proof-done-advancing-other1570,61841 -(defun proof-segment-up-to-parser proof-segment-up-to-parser1598,62821 -(defun proof-script-generic-parse-find-comment-end proof-script-generic-parse-find-comment-end1661,64897 -(defun proof-script-generic-parse-cmdend proof-script-generic-parse-cmdend1670,65313 -(defun proof-script-generic-parse-cmdstart proof-script-generic-parse-cmdstart1695,66208 -(defun proof-script-generic-parse-sexp proof-script-generic-parse-sexp1758,68916 -(defun proof-cmdstart-add-segment-for-cmd proof-cmdstart-add-segment-for-cmd1782,69852 -(defun proof-segment-up-to-cmdstart proof-segment-up-to-cmdstart1834,72051 -(defun proof-segment-up-to-cmdend proof-segment-up-to-cmdend1895,74411 -(defun proof-semis-to-vanillas proof-semis-to-vanillas1966,77056 -(defun proof-script-new-command-advance proof-script-new-command-advance2005,78382 -(defun proof-script-next-command-advance proof-script-next-command-advance2047,80123 -(defun proof-assert-until-point-interactive proof-assert-until-point-interactive2059,80564 -(defun proof-assert-until-point proof-assert-until-point2085,81686 -(defun proof-assert-next-commandproof-assert-next-command2138,84118 -(defun proof-goto-point proof-goto-point2186,86381 -(defun proof-insert-pbp-command proof-insert-pbp-command2203,86907 -(defun proof-done-retracting proof-done-retracting2235,87980 -(defun proof-setup-retract-action proof-setup-retract-action2262,89091 -(defun proof-last-goal-or-goalsave proof-last-goal-or-goalsave2272,89574 -(defun proof-retract-target proof-retract-target2296,90443 -(defun proof-retract-until-point-interactive proof-retract-until-point-interactive2381,94084 -(defun proof-retract-until-point proof-retract-until-point2389,94469 -(define-derived-mode proof-mode proof-mode2434,96330 -(defun proof-script-set-visited-file-name proof-script-set-visited-file-name2470,97816 -(defun proof-script-set-buffer-hooks proof-script-set-buffer-hooks2494,98818 -(defun proof-script-kill-buffer-fn proof-script-kill-buffer-fn2504,99314 -(defun proof-config-done-related proof-config-done-related2548,101136 -(defun proof-generic-goal-command-p proof-generic-goal-command-p2618,103702 -(defun proof-generic-state-preserving-p proof-generic-state-preserving-p2622,103877 -(defun proof-generic-count-undos proof-generic-count-undos2631,104394 -(defun proof-generic-find-and-forget proof-generic-find-and-forget2660,105424 -(defconst proof-script-important-settingsproof-script-important-settings2711,107249 -(defun proof-config-done proof-config-done2724,107786 -(defun proof-setup-parsing-mechanism proof-setup-parsing-mechanism2821,111334 -(defun proof-setup-imenu proof-setup-imenu2865,113187 -(defun proof-setup-func-menu proof-setup-func-menu2882,113792 - -generic/proof-shell.el,5288 +(defun proof-goto-end-of-locked-if-pos-not-visible-in-window proof-goto-end-of-locked-if-pos-not-visible-in-window462,16500 +(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window473,16981 +(defun proof-end-of-locked-visible-p proof-end-of-locked-visible-p487,17634 +(defun proof-goto-end-of-queue-or-locked-if-not-visible proof-goto-end-of-queue-or-locked-if-not-visible496,18085 +(defvar pg-idioms pg-idioms515,18735 +(defvar pg-visibility-specs pg-visibility-specs518,18831 +(deflocal pg-script-portions pg-script-portions523,19038 +(defun pg-clear-script-portions pg-clear-script-portions526,19160 +(defun pg-add-script-element pg-add-script-element544,19824 +(defun pg-remove-script-element pg-remove-script-element547,19900 +(defsubst pg-visname pg-visname555,20178 +(defun pg-add-element pg-add-element559,20323 +(defun pg-open-invisible-span pg-open-invisible-span593,21952 +(defun pg-remove-element pg-remove-element604,22315 +(defun pg-make-element-invisible pg-make-element-invisible611,22585 +(defun pg-make-element-visible pg-make-element-visible617,22842 +(defun pg-toggle-element-visibility pg-toggle-element-visibility622,23021 +(defun pg-redisplay-for-gnuemacs pg-redisplay-for-gnuemacs630,23351 +(defun pg-show-all-portions pg-show-all-portions637,23622 +(defun pg-show-all-proofs pg-show-all-proofs655,24293 +(defun pg-hide-all-proofs pg-hide-all-proofs660,24421 +(defun pg-add-proof-element pg-add-proof-element665,24552 +(defun pg-span-name pg-span-name679,25172 +(defun pg-set-span-helphighlights pg-set-span-helphighlights700,25879 +(defun proof-complete-buffer-atomic proof-complete-buffer-atomic725,26703 +(defun proof-register-possibly-new-processed-file proof-register-possibly-new-processed-file766,28618 +(defun proof-inform-prover-file-retracted proof-inform-prover-file-retracted817,30746 +(defun proof-auto-retract-dependencies proof-auto-retract-dependencies836,31532 +(defun proof-unregister-buffer-file-name proof-unregister-buffer-file-name890,34072 +(defun proof-protected-process-or-retract proof-protected-process-or-retract936,35895 +(defun proof-deactivate-scripting-auto proof-deactivate-scripting-auto963,37065 +(defun proof-deactivate-scripting proof-deactivate-scripting972,37423 +(defun proof-activate-scripting proof-activate-scripting1109,42828 +(defun proof-toggle-active-scripting proof-toggle-active-scripting1237,48582 +(defun proof-done-advancing proof-done-advancing1278,49943 +(defun proof-done-advancing-comment proof-done-advancing-comment1363,53348 +(defun proof-done-advancing-save proof-done-advancing-save1382,54090 +(defun proof-make-goalsave proof-make-goalsave1475,57703 +(defun proof-get-name-from-goal proof-get-name-from-goal1490,58446 +(defun proof-done-advancing-autosave proof-done-advancing-autosave1509,59472 +(defun proof-done-advancing-other proof-done-advancing-other1573,61989 +(defun proof-segment-up-to-parser proof-segment-up-to-parser1601,62969 +(defun proof-script-generic-parse-find-comment-end proof-script-generic-parse-find-comment-end1664,65045 +(defun proof-script-generic-parse-cmdend proof-script-generic-parse-cmdend1673,65461 +(defun proof-script-generic-parse-cmdstart proof-script-generic-parse-cmdstart1698,66356 +(defun proof-script-generic-parse-sexp proof-script-generic-parse-sexp1761,69064 +(defun proof-cmdstart-add-segment-for-cmd proof-cmdstart-add-segment-for-cmd1785,70000 +(defun proof-segment-up-to-cmdstart proof-segment-up-to-cmdstart1837,72199 +(defun proof-segment-up-to-cmdend proof-segment-up-to-cmdend1898,74559 +(defun proof-semis-to-vanillas proof-semis-to-vanillas1969,77204 +(defun proof-script-new-command-advance proof-script-new-command-advance2008,78530 +(defun proof-script-next-command-advance proof-script-next-command-advance2050,80271 +(defun proof-assert-until-point-interactive proof-assert-until-point-interactive2062,80712 +(defun proof-assert-until-point proof-assert-until-point2088,81834 +(defun proof-assert-next-commandproof-assert-next-command2141,84266 +(defun proof-goto-point proof-goto-point2189,86529 +(defun proof-insert-pbp-command proof-insert-pbp-command2206,87055 +(defun proof-done-retracting proof-done-retracting2238,88128 +(defun proof-setup-retract-action proof-setup-retract-action2265,89239 +(defun proof-last-goal-or-goalsave proof-last-goal-or-goalsave2275,89722 +(defun proof-retract-target proof-retract-target2299,90591 +(defun proof-retract-until-point-interactive proof-retract-until-point-interactive2384,94232 +(defun proof-retract-until-point proof-retract-until-point2392,94617 +(define-derived-mode proof-mode proof-mode2437,96478 +(defun proof-script-set-visited-file-name proof-script-set-visited-file-name2473,97964 +(defun proof-script-set-buffer-hooks proof-script-set-buffer-hooks2497,98966 +(defun proof-script-kill-buffer-fn proof-script-kill-buffer-fn2507,99462 +(defun proof-config-done-related proof-config-done-related2551,101284 +(defun proof-generic-goal-command-p proof-generic-goal-command-p2621,103850 +(defun proof-generic-state-preserving-p proof-generic-state-preserving-p2625,104025 +(defun proof-generic-count-undos proof-generic-count-undos2634,104542 +(defun proof-generic-find-and-forget proof-generic-find-and-forget2663,105572 +(defconst proof-script-important-settingsproof-script-important-settings2714,107397 +(defun proof-config-done proof-config-done2727,107934 +(defun proof-setup-parsing-mechanism proof-setup-parsing-mechanism2824,111482 +(defun proof-setup-imenu proof-setup-imenu2868,113335 +(defun proof-setup-func-menu proof-setup-func-menu2885,113940 + +generic/proof-shell.el,5296 (defvar proof-shell-last-output proof-shell-last-output19,458 (defvar proof-marker proof-marker63,1714 (defvar proof-action-list proof-action-list66,1811 @@ -1013,88 +986,86 @@ generic/proof-shell.el,5288 (defvar proof-shell-urgent-message-scanner proof-shell-urgent-message-scanner615,22050 (defun proof-shell-handle-output proof-shell-handle-output619,22177 (defun proof-shell-handle-delayed-output proof-shell-handle-delayed-output693,25514 -(defvar proof-shell-ignore-errors proof-shell-ignore-errors728,26936 -(defun proof-shell-handle-error proof-shell-handle-error734,27138 -(defun proof-shell-handle-interrupt proof-shell-handle-interrupt752,27982 -(defun proof-shell-error-or-interrupt-action proof-shell-error-or-interrupt-action766,28598 -(defun proof-goals-pos proof-goals-pos784,29424 -(defun proof-pbp-focus-on-first-goal proof-pbp-focus-on-first-goal789,29629 -(defsubst proof-shell-string-match-safe proof-shell-string-match-safe801,30164 -(defun proof-shell-process-output proof-shell-process-output806,30332 -(defvar proof-shell-insert-space-fudge proof-shell-insert-space-fudge917,34972 -(defun proof-shell-insert proof-shell-insert926,35281 -(defun proof-shell-command-queue-item proof-shell-command-queue-item994,37815 -(defun proof-shell-set-silent proof-shell-set-silent999,37972 -(defun proof-shell-start-silent-item proof-shell-start-silent-item1005,38191 -(defun proof-shell-clear-silent proof-shell-clear-silent1011,38383 -(defun proof-shell-stop-silent-item proof-shell-stop-silent-item1017,38605 -(defun proof-shell-should-be-silent proof-shell-should-be-silent1024,38877 -(defun proof-append-alist proof-append-alist1037,39433 -(defun proof-start-queue proof-start-queue1093,41560 -(defun proof-extend-queue proof-extend-queue1104,41909 -(defun proof-shell-exec-loop proof-shell-exec-loop1115,42290 -(defun proof-shell-insert-loopback-cmd proof-shell-insert-loopback-cmd1177,44757 -(defun proof-shell-message proof-shell-message1215,46480 -(defun proof-shell-process-urgent-message proof-shell-process-urgent-message1221,46696 -(defvar proof-shell-minibuffer-urgent-interactive-input-history proof-shell-minibuffer-urgent-interactive-input-history1432,55614 -(defun proof-shell-minibuffer-urgent-interactive-input proof-shell-minibuffer-urgent-interactive-input1434,55684 -(defun proof-shell-process-urgent-messages proof-shell-process-urgent-messages1446,56054 -(defun proof-shell-filter proof-shell-filter1515,59110 -(defun proof-shell-filter-process-output proof-shell-filter-process-output1668,65447 -(defvar pg-last-tracing-output-time pg-last-tracing-output-time1721,67501 -(defvar pg-tracing-slow-mode pg-tracing-slow-mode1724,67607 -(defconst pg-slow-mode-duration pg-slow-mode-duration1727,67696 -(defconst pg-fast-tracing-mode-threshold pg-fast-tracing-mode-threshold1730,67778 -(defvar pg-tracing-cleanup-timer pg-tracing-cleanup-timer1733,67906 -(defun pg-tracing-tight-loop pg-tracing-tight-loop1735,67945 -(defun pg-finish-tracing-display pg-finish-tracing-display1778,69698 -(defun proof-shell-dont-show-annotations proof-shell-dont-show-annotations1789,69968 -(defun proof-shell-show-annotations proof-shell-show-annotations1805,70503 -(defun proof-shell-wait proof-shell-wait1826,71000 -(defun proof-done-invisible proof-done-invisible1846,71910 -(defun proof-shell-invisible-command proof-shell-invisible-command1889,73633 -(defun proof-shell-invisible-cmd-get-result proof-shell-invisible-cmd-get-result1922,74883 -(defun proof-shell-invisible-command-invisible-result proof-shell-invisible-command-invisible-result1939,75564 -(define-derived-mode proof-shell-mode proof-shell-mode1959,76068 -(defconst proof-shell-important-settingsproof-shell-important-settings2029,78671 -(defun proof-shell-config-done proof-shell-config-done2034,78771 - -generic/proof-site.el,1154 -(defgroup proof-general proof-general20,593 -(defgroup proof-general-internals proof-general-internals33,1009 -(defun proof-home-directory-fn proof-home-directory-fn42,1202 -(defcustom proof-home-directoryproof-home-directory53,1572 -(defcustom proof-images-directoryproof-images-directory62,1938 -(defcustom proof-info-directoryproof-info-directory68,2139 -(defcustom proof-assistant-tableproof-assistant-table97,3388 -(defun proof-string-to-list proof-string-to-list156,5375 -(defcustom proof-assistants proof-assistants172,5866 -(defun proof-ready-for-assistant proof-ready-for-assistant220,7691 -(defconst proof-general-version proof-general-version335,11984 -(defcustom proof-assistant-cusgrp proof-assistant-cusgrp350,12549 -(defcustom proof-assistant-internals-cusgrp proof-assistant-internals-cusgrp358,12852 -(defcustom proof-assistant proof-assistant366,13164 -(defcustom proof-assistant-symbol proof-assistant-symbol374,13433 -(defvar proof-running-on-XEmacs proof-running-on-XEmacs391,13981 -(defvar proof-running-on-Emacs21 proof-running-on-Emacs21393,14103 -(defvar proof-running-on-win32 proof-running-on-win32397,14350 +(defvar proof-shell-no-error-display proof-shell-no-error-display728,26936 +(defun proof-shell-handle-error proof-shell-handle-error734,27142 +(defun proof-shell-handle-interrupt proof-shell-handle-interrupt752,27978 +(defun proof-shell-error-or-interrupt-action proof-shell-error-or-interrupt-action766,28600 +(defun proof-goals-pos proof-goals-pos793,29805 +(defun proof-pbp-focus-on-first-goal proof-pbp-focus-on-first-goal798,30010 +(defsubst proof-shell-string-match-safe proof-shell-string-match-safe810,30545 +(defun proof-shell-process-output proof-shell-process-output815,30713 +(defvar proof-shell-insert-space-fudge proof-shell-insert-space-fudge926,35353 +(defun proof-shell-insert proof-shell-insert935,35662 +(defun proof-shell-command-queue-item proof-shell-command-queue-item1003,38196 +(defun proof-shell-set-silent proof-shell-set-silent1008,38353 +(defun proof-shell-start-silent-item proof-shell-start-silent-item1014,38572 +(defun proof-shell-clear-silent proof-shell-clear-silent1020,38764 +(defun proof-shell-stop-silent-item proof-shell-stop-silent-item1026,38986 +(defun proof-shell-should-be-silent proof-shell-should-be-silent1033,39258 +(defun proof-append-alist proof-append-alist1046,39814 +(defun proof-start-queue proof-start-queue1102,41941 +(defun proof-extend-queue proof-extend-queue1113,42290 +(defun proof-shell-exec-loop proof-shell-exec-loop1124,42671 +(defun proof-shell-insert-loopback-cmd proof-shell-insert-loopback-cmd1189,45259 +(defun proof-shell-message proof-shell-message1227,46982 +(defun proof-shell-process-urgent-message proof-shell-process-urgent-message1233,47198 +(defvar proof-shell-minibuffer-urgent-interactive-input-history proof-shell-minibuffer-urgent-interactive-input-history1442,56063 +(defun proof-shell-minibuffer-urgent-interactive-input proof-shell-minibuffer-urgent-interactive-input1444,56133 +(defun proof-shell-process-urgent-messages proof-shell-process-urgent-messages1456,56503 +(defun proof-shell-filter proof-shell-filter1525,59559 +(defun proof-shell-filter-process-output proof-shell-filter-process-output1678,65896 +(defvar pg-last-tracing-output-time pg-last-tracing-output-time1731,67950 +(defvar pg-tracing-slow-mode pg-tracing-slow-mode1734,68056 +(defconst pg-slow-mode-duration pg-slow-mode-duration1737,68145 +(defconst pg-fast-tracing-mode-threshold pg-fast-tracing-mode-threshold1740,68227 +(defvar pg-tracing-cleanup-timer pg-tracing-cleanup-timer1743,68355 +(defun pg-tracing-tight-loop pg-tracing-tight-loop1745,68394 +(defun pg-finish-tracing-display pg-finish-tracing-display1788,70112 +(defun proof-shell-dont-show-annotations proof-shell-dont-show-annotations1801,70418 +(defun proof-shell-show-annotations proof-shell-show-annotations1817,70953 +(defun proof-shell-wait proof-shell-wait1838,71450 +(defun proof-done-invisible proof-done-invisible1858,72360 +(defun proof-shell-invisible-command proof-shell-invisible-command1901,74083 +(defun proof-shell-invisible-cmd-get-result proof-shell-invisible-cmd-get-result1934,75333 +(defun proof-shell-invisible-command-invisible-result proof-shell-invisible-command-invisible-result1951,76014 +(define-derived-mode proof-shell-mode proof-shell-mode1971,76518 +(defconst proof-shell-important-settingsproof-shell-important-settings2039,79071 +(defun proof-shell-config-done proof-shell-config-done2044,79171 + +generic/proof-site.el,1030 +(defgroup proof-general proof-general20,594 +(defgroup proof-general-internals proof-general-internals33,1010 +(defun proof-home-directory-fn proof-home-directory-fn42,1203 +(defcustom proof-home-directoryproof-home-directory53,1573 +(defcustom proof-images-directoryproof-images-directory62,1939 +(defcustom proof-info-directoryproof-info-directory68,2140 +(defcustom proof-assistant-tableproof-assistant-table97,3389 +(defun proof-string-to-list proof-string-to-list163,5568 +(defcustom proof-assistants proof-assistants179,6059 +(defun proof-ready-for-assistant proof-ready-for-assistant215,7472 +(defconst proof-general-version proof-general-version328,11681 +(defconst proof-general-short-version proof-general-short-version331,11824 +(defcustom proof-assistant-cusgrp proof-assistant-cusgrp348,12406 +(defcustom proof-assistant-internals-cusgrp proof-assistant-internals-cusgrp356,12709 +(defcustom proof-assistant proof-assistant364,13021 +(defcustom proof-assistant-symbol proof-assistant-symbol372,13290 generic/proof-splash.el,976 (defcustom proof-splash-enable proof-splash-enable14,379 (defcustom proof-splash-time proof-splash-time19,531 (defcustom proof-splash-contentsproof-splash-contents27,816 -(defconst proof-splash-startup-msg proof-splash-startup-msg59,1970 -(defconst proof-splash-welcome proof-splash-welcome68,2349 -(defun proof-get-image proof-get-image87,2913 -(defvar proof-splash-timeout-conf proof-splash-timeout-conf139,4737 -(defun proof-splash-centre-spaces proof-splash-centre-spaces142,4850 -(defun proof-splash-remove-screen proof-splash-remove-screen170,6019 -(defun proof-splash-remove-buffer proof-splash-remove-buffer191,6736 -(defvar proof-splash-seen proof-splash-seen207,7400 -(defun proof-splash-display-screen proof-splash-display-screen211,7517 -(defun proof-splash-message proof-splash-message286,10676 -(defun proof-splash-timeout-waiter proof-splash-timeout-waiter296,11039 -(defun proof-splash-set-frame-titles proof-splash-set-frame-titles313,11778 +(defconst proof-splash-startup-msg proof-splash-startup-msg56,1895 +(defconst proof-splash-welcome proof-splash-welcome65,2274 +(defun proof-get-image proof-get-image84,2838 +(defvar proof-splash-timeout-conf proof-splash-timeout-conf136,4662 +(defun proof-splash-centre-spaces proof-splash-centre-spaces139,4775 +(defun proof-splash-remove-screen proof-splash-remove-screen167,5944 +(defun proof-splash-remove-buffer proof-splash-remove-buffer188,6661 +(defvar proof-splash-seen proof-splash-seen204,7325 +(defun proof-splash-display-screen proof-splash-display-screen208,7442 +(defun proof-splash-message proof-splash-message283,10601 +(defun proof-splash-timeout-waiter proof-splash-timeout-waiter293,10964 +(defun proof-splash-set-frame-titles proof-splash-set-frame-titles310,11703 generic/proof-syntax.el,1296 (defun proof-ids-to-regexp proof-ids-to-regexp16,445 @@ -1181,7 +1152,7 @@ generic/proof-toolbar.el,3888 (defun proof-toolbar-make-menu-item proof-toolbar-make-menu-item558,16193 (defconst proof-toolbar-scripting-menuproof-toolbar-scripting-menu580,16881 -generic/proof-utils.el,3092 +generic/proof-utils.el,3150 (defmacro deflocal deflocal18,471 (defmacro proof-with-current-buffer-if-exists proof-with-current-buffer-if-exists25,709 (defmacro proof-with-script-buffer proof-with-script-buffer34,1086 @@ -1211,145 +1182,44 @@ generic/proof-utils.el,3092 (defun proof-font-lock-clear-font-lock-vars proof-font-lock-clear-font-lock-vars387,13915 (defun proof-font-lock-set-font-lock-vars proof-font-lock-set-font-lock-vars398,14288 (defun proof-fontify-region proof-fontify-region405,14501 -(defconst pg-special-char-regexp pg-special-char-regexp459,16467 -(defun pg-remove-specials pg-remove-specials463,16579 -(defun proof-fontify-buffer proof-fontify-buffer477,17004 -(defun proof-warn-if-unset proof-warn-if-unset490,17245 -(defun proof-get-window-for-buffer proof-get-window-for-buffer495,17463 -(defun proof-display-and-keep-buffer proof-display-and-keep-buffer532,19115 -(defun proof-clean-buffer proof-clean-buffer563,20391 -(defun proof-message proof-message575,20869 -(defun proof-warning proof-warning580,21082 -(defun proof-debug proof-debug587,21416 -(defun proof-switch-to-buffer proof-switch-to-buffer600,21907 -(defun proof-resize-window-tofit proof-resize-window-tofit633,23599 -(defun proof-submit-bug-report proof-submit-bug-report733,27627 -(defun proof-deftoggle-fn proof-deftoggle-fn756,28406 -(defmacro proof-deftoggle proof-deftoggle771,29061 -(defun proof-defintset-fn proof-defintset-fn778,29435 -(defmacro proof-defintset proof-defintset792,30090 -(defun proof-defstringset-fn proof-defstringset-fn799,30467 -(defmacro proof-defstringset proof-defstringset812,31094 -(defun pg-custom-save-vars pg-custom-save-vars826,31559 -(defun pg-custom-reset-vars pg-custom-reset-vars844,32285 -(defun proof-locate-executable proof-locate-executable857,32622 -(defconst proof-extra-flsproof-extra-fls889,34035 +(defconst pg-special-char-regexp pg-special-char-regexp464,16730 +(defun pg-remove-specials pg-remove-specials468,16842 +(defun proof-fontify-buffer proof-fontify-buffer482,17267 +(defun proof-warn-if-unset proof-warn-if-unset495,17508 +(defun proof-get-window-for-buffer proof-get-window-for-buffer500,17726 +(defun proof-display-and-keep-buffer proof-display-and-keep-buffer537,19378 +(defun proof-clean-buffer proof-clean-buffer568,20654 +(defun proof-message proof-message582,21191 +(defun proof-warning proof-warning587,21404 +(defun pg-internal-warning pg-internal-warning593,21686 +(defun proof-debug proof-debug601,22005 +(defun proof-switch-to-buffer proof-switch-to-buffer616,22678 +(defun proof-resize-window-tofit proof-resize-window-tofit649,24370 +(defun proof-submit-bug-report proof-submit-bug-report749,28398 +(defun proof-deftoggle-fn proof-deftoggle-fn773,29200 +(defmacro proof-deftoggle proof-deftoggle788,29855 +(defun proof-defintset-fn proof-defintset-fn795,30229 +(defmacro proof-defintset proof-defintset809,30884 +(defun proof-defstringset-fn proof-defstringset-fn816,31261 +(defmacro proof-defstringset proof-defstringset829,31888 +(defun pg-custom-save-vars pg-custom-save-vars843,32353 +(defun pg-custom-reset-vars pg-custom-reset-vars861,33079 +(defun proof-locate-executable proof-locate-executable874,33416 +(defconst proof-extra-flsproof-extra-fls906,34829 generic/proof-x-symbol.el,960 -(defvar proof-x-symbol-initialized proof-x-symbol-initialized53,2149 -(defun proof-x-symbol-tokenlang-file proof-x-symbol-tokenlang-file56,2244 -(defun proof-x-symbol-support-maybe-available proof-x-symbol-support-maybe-available62,2426 -(defun proof-x-symbol-initialize proof-x-symbol-initialize82,3171 -(defun proof-x-symbol-enable proof-x-symbol-enable177,7034 -(defun proof-x-symbol-refresh-output-buffers proof-x-symbol-refresh-output-buffers199,8003 -(defun proof-x-symbol-mode-associated-buffers proof-x-symbol-mode-associated-buffers214,8757 -(defalias 'proof-x-symbol-decode-region proof-x-symbol-decode-region236,9461 -(defun proof-x-symbol-encode-shell-input proof-x-symbol-encode-shell-input238,9527 -(defun proof-x-symbol-set-language proof-x-symbol-set-language255,10118 -(defun proof-x-symbol-shell-config proof-x-symbol-shell-config260,10289 -(defun proof-x-symbol-config-output-buffer proof-x-symbol-config-output-buffer308,12456 - -generic/span.el,192 -(defsubst delete-spans delete-spans22,471 -(defsubst span-property-safe span-property-safe26,625 -(defsubst set-span-start set-span-start30,764 -(defsubst set-span-end set-span-end34,896 - -generic/span-extent.el,1346 -(defsubst make-span make-span16,557 -(defsubst detach-span detach-span20,679 -(defsubst set-span-endpoints set-span-endpoints24,766 -(defsubst set-span-property set-span-property28,899 -(defsubst span-read-only span-read-only32,1026 -(defsubst span-read-write span-read-write36,1130 -(defun span-give-warning span-give-warning40,1237 -(defun span-write-warning span-write-warning44,1335 -(defsubst span-property span-property49,1535 -(defsubst delete-span delete-span53,1650 -(defsubst mapcar-spans mapcar-spans59,1821 -(defsubst span-at span-at63,2027 -(defsubst span-at-before span-at-before67,2144 -(defsubst span-start span-start72,2341 -(defsubst span-end span-end76,2470 -(defsubst prev-span prev-span80,2593 -(defsubst next-span next-span84,2739 -(defsubst span-live-p span-live-p88,2881 -(defun span-raise span-raise96,3153 -(defalias 'span-object span-object100,3252 -(defalias 'span-string span-string101,3291 -(defsubst make-detached-span make-detached-span104,3377 -(defsubst span-buffer span-buffer110,3474 -(defsubst span-detached-p span-detached-p115,3566 -(defsubst set-span-face set-span-face120,3678 -(defsubst fold-spans fold-spans125,3774 -(defsubst set-span-properties set-span-properties130,3972 -(defsubst set-span-keymap set-span-keymap135,4081 -(defsubst span-at-event span-at-event140,4196 - -generic/span-overlay.el,2198 -(defvar before-list before-list20,771 -(defun foldr foldr27,906 -(defun foldl foldl39,1239 -(defsubst span-start span-start51,1556 -(defsubst span-end span-end55,1648 -(defun set-span-property set-span-property59,1734 -(defsubst span-property span-property63,1850 -(defun span-read-only-hook span-read-only-hook67,1961 -(defun span-read-only span-read-only71,2093 -(defun span-read-write span-read-write86,2871 -(defun span-give-warning span-give-warning92,3090 -(defun span-write-warning span-write-warning96,3198 -(defun int-nil-lt int-nil-lt101,3421 -(defun span-lt span-lt110,3624 -(defun span-traverse span-traverse115,3783 -(defun add-span add-span131,4230 -(defun make-span make-span145,4632 -(defun remove-span remove-span149,4763 -(defun spans-at-point spans-at-point162,5216 -(defun append-unique append-unique176,5696 -(defun spans-at-region spans-at-region179,5783 -(defun spans-at-point-prop spans-at-point-prop186,6005 -(defun spans-at-region-prop spans-at-region-prop194,6255 -(defun span-at span-at206,6602 -(defsubst detach-span detach-span212,6816 -(defsubst delete-span delete-span218,6943 -(defsubst set-span-endpoints set-span-endpoints226,7186 -(defsubst mapcar-spans mapcar-spans233,7402 -(defun map-spans-aux map-spans-aux237,7606 -(defsubst map-spans map-spans241,7721 -(defun find-span-aux find-span-aux244,7779 -(defun find-span find-span249,7905 -(defun span-at-before span-at-before252,7970 -(defun prev-span prev-span265,8412 -(defun next-span next-span274,8694 -(defsubst span-live-p span-live-p299,9678 -(defun span-raise span-raise305,9844 -(defalias 'span-object span-object311,10075 -(defun span-string span-string313,10116 -(defun set-span-properties set-span-properties319,10298 -(defun span-find-span span-find-span331,10553 -(defsubst span-at-event span-at-event342,10912 -(defun make-detached-span make-detached-span347,11036 -(defun fold-spans-aux fold-spans-aux353,11170 -(defun fold-spans fold-spans361,11426 -(defsubst span-buffer span-buffer368,11634 -(defsubst span-detached-p span-detached-p373,11726 -(defsubst set-span-face set-span-face381,11922 -(defsubst set-span-keymap set-span-keymap386,12022 - -generic/texi-docstring-magic.el,958 -(defun texi-docstring-magic-find-face texi-docstring-magic-find-face85,2996 -(defun texi-docstring-magic-splice-sep texi-docstring-magic-splice-sep90,3161 -(defconst texi-docstring-magic-munge-tabletexi-docstring-magic-munge-table100,3466 -(defun texi-docstring-magic-untabify texi-docstring-magic-untabify190,7185 -(defun texi-docstring-magic-munge-docstring texi-docstring-magic-munge-docstring200,7500 -(defun texi-docstring-magic-texi texi-docstring-magic-texi239,8787 -(defun texi-docstring-magic-format-default texi-docstring-magic-format-default252,9227 -(defun texi-docstring-magic-texi-for texi-docstring-magic-texi-for268,9862 -(defconst texi-docstring-magic-commenttexi-docstring-magic-comment326,11822 -(defun texi-docstring-magic texi-docstring-magic332,11976 -(defun texi-docstring-magic-face-at-point texi-docstring-magic-face-at-point366,13056 -(defun texi-docstring-magic-insert-magic texi-docstring-magic-insert-magic381,13579 +(defvar proof-x-symbol-initialized proof-x-symbol-initialized54,2151 +(defun proof-x-symbol-tokenlang-file proof-x-symbol-tokenlang-file57,2246 +(defun proof-x-symbol-support-maybe-available proof-x-symbol-support-maybe-available63,2428 +(defun proof-x-symbol-initialize proof-x-symbol-initialize83,3173 +(defun proof-x-symbol-enable proof-x-symbol-enable178,7036 +(defun proof-x-symbol-refresh-output-buffers proof-x-symbol-refresh-output-buffers200,8005 +(defun proof-x-symbol-mode-associated-buffers proof-x-symbol-mode-associated-buffers215,8759 +(defalias 'proof-x-symbol-decode-region proof-x-symbol-decode-region237,9463 +(defun proof-x-symbol-encode-shell-input proof-x-symbol-encode-shell-input239,9529 +(defun proof-x-symbol-set-language proof-x-symbol-set-language256,10120 +(defun proof-x-symbol-shell-config proof-x-symbol-shell-config261,10291 +(defun proof-x-symbol-config-output-buffer proof-x-symbol-config-output-buffer309,12458 hol98/hol98.el,0 @@ -1447,11 +1317,11 @@ isa/isa.el,2283 (defun isa-state-preserving-p isa-state-preserving-p550,20655 (defun isa-pre-shell-start isa-pre-shell-start559,21023 (defun isa-mode-config isa-mode-config566,21300 -(defun isa-shell-mode-config isa-shell-mode-config593,22373 -(defun isa-response-mode-config isa-response-mode-config600,22622 -(defun isa-goals-mode-config isa-goals-mode-config605,22783 -(defun isa-preprocessing isa-preprocessing613,23107 -(defpgdefault completion-tablecompletion-table627,23611 +(defun isa-shell-mode-config isa-shell-mode-config594,22443 +(defun isa-response-mode-config isa-response-mode-config601,22692 +(defun isa-goals-mode-config isa-goals-mode-config606,22853 +(defun isa-preprocessing isa-preprocessing614,23177 +(defpgdefault completion-tablecompletion-table628,23681 isa/isa-syntax.el,3046 (defun isa-init-syntax-table isa-init-syntax-table14,312 @@ -1599,36 +1469,36 @@ isa/x-symbol-isabelle.el,3169 isa/x-symbol-isa.el,0 isar/isar.el,1883 -(defcustom isar-keywords-name isar-keywords-name28,631 -(defpgdefault completion-table completion-table45,1155 -(defcustom isar-web-pageisar-web-page47,1208 -(defun isar-detect-header isar-detect-header65,1572 -(defun isar-strip-terminators isar-strip-terminators100,2835 -(defun isar-markup-ml isar-markup-ml113,3206 -(defun isar-mode-config-set-variables isar-mode-config-set-variables118,3341 -(defun isar-shell-mode-config-set-variables isar-shell-mode-config-set-variables182,6172 -(defun isar-remove-file isar-remove-file296,10961 -(defun isar-shell-compute-new-files-list isar-shell-compute-new-files-list306,11324 -(defun isar-activate-scripting isar-activate-scripting317,11790 -(define-derived-mode isar-shell-mode isar-shell-mode326,11960 -(define-derived-mode isar-response-mode isar-response-mode331,12083 -(define-derived-mode isar-goals-mode isar-goals-mode336,12265 -(define-derived-mode isar-mode isar-mode341,12440 -(defpgdefault menu-entriesmenu-entries374,13796 -(defun isar-count-undos isar-count-undos398,14818 -(defun isar-find-and-forget isar-find-and-forget424,15919 -(defun isar-goal-command-p isar-goal-command-p471,17764 -(defun isar-global-save-command-p isar-global-save-command-p475,17896 -(defvar isar-current-goal isar-current-goal496,18733 -(defun isar-state-preserving-p isar-state-preserving-p499,18799 -(defvar isar-shell-current-line-width isar-shell-current-line-width522,19833 -(defun isar-shell-adjust-line-width isar-shell-adjust-line-width528,20051 -(defun isar-pre-shell-start isar-pre-shell-start548,20934 -(defun isar-preprocessing isar-preprocessing560,21270 -(defun isar-mode-config isar-mode-config583,22481 -(defun isar-shell-mode-config isar-shell-mode-config594,22984 -(defun isar-response-mode-config isar-response-mode-config605,23354 -(defun isar-goals-mode-config isar-goals-mode-config614,23611 +(defcustom isar-keywords-name isar-keywords-name28,630 +(defpgdefault completion-table completion-table45,1154 +(defcustom isar-web-pageisar-web-page47,1207 +(defun isar-detect-header isar-detect-header65,1571 +(defun isar-strip-terminators isar-strip-terminators100,2834 +(defun isar-markup-ml isar-markup-ml113,3205 +(defun isar-mode-config-set-variables isar-mode-config-set-variables118,3340 +(defun isar-shell-mode-config-set-variables isar-shell-mode-config-set-variables182,6171 +(defun isar-remove-file isar-remove-file296,10966 +(defun isar-shell-compute-new-files-list isar-shell-compute-new-files-list306,11329 +(defun isar-activate-scripting isar-activate-scripting317,11795 +(define-derived-mode isar-shell-mode isar-shell-mode326,11965 +(define-derived-mode isar-response-mode isar-response-mode331,12088 +(define-derived-mode isar-goals-mode isar-goals-mode336,12270 +(define-derived-mode isar-mode isar-mode341,12445 +(defpgdefault menu-entriesmenu-entries388,14264 +(defun isar-count-undos isar-count-undos419,15622 +(defun isar-find-and-forget isar-find-and-forget445,16723 +(defun isar-goal-command-p isar-goal-command-p492,18568 +(defun isar-global-save-command-p isar-global-save-command-p496,18700 +(defvar isar-current-goal isar-current-goal517,19537 +(defun isar-state-preserving-p isar-state-preserving-p520,19603 +(defvar isar-shell-current-line-width isar-shell-current-line-width543,20637 +(defun isar-shell-adjust-line-width isar-shell-adjust-line-width549,20855 +(defun isar-pre-shell-start isar-pre-shell-start569,21738 +(defun isar-preprocessing isar-preprocessing581,22074 +(defun isar-mode-config isar-mode-config604,23285 +(defun isar-shell-mode-config isar-shell-mode-config616,23855 +(defun isar-response-mode-config isar-response-mode-config627,24225 +(defun isar-goals-mode-config isar-goals-mode-config636,24482 isar/isar-keywords.el,1650 (defconst isar-keywords-majorisar-keywords-major14,378 @@ -1660,83 +1530,83 @@ isar/isar-mmm.el,129 (defconst isar-start-latex-regexp isar-start-latex-regexp23,697 (defconst isar-start-sml-regexp isar-start-sml-regexp35,1130 -isar/isar-syntax.el,4918 +isar/isar-syntax.el,4921 (defconst isar-script-syntax-table-entries isar-script-syntax-table-entries18,414 -(defconst isar-script-syntax-table-alistisar-script-syntax-table-alist57,1326 -(defun isar-init-syntax-table isar-init-syntax-table66,1609 -(defun isar-init-output-syntax-table isar-init-output-syntax-table74,1857 -(defconst isar-keywords-theory-encloseisar-keywords-theory-enclose89,2272 -(defconst isar-keywords-theoryisar-keywords-theory94,2424 -(defconst isar-keywords-saveisar-keywords-save99,2569 -(defconst isar-keywords-proof-encloseisar-keywords-proof-enclose104,2698 -(defconst isar-keywords-proofisar-keywords-proof110,2880 -(defconst isar-keywords-proof-contextisar-keywords-proof-context117,3078 -(defconst isar-keywords-local-goalisar-keywords-local-goal121,3192 -(defconst isar-keywords-improperisar-keywords-improper125,3304 -(defconst isar-keywords-outlineisar-keywords-outline130,3443 -(defconst isar-keywords-fumeisar-keywords-fume133,3508 -(defconst isar-keywords-indent-openisar-keywords-indent-open140,3726 -(defconst isar-keywords-indent-closeisar-keywords-indent-close146,3910 -(defconst isar-keywords-indent-encloseisar-keywords-indent-enclose150,4015 -(defun isar-regexp-simple-alt isar-regexp-simple-alt158,4194 -(defun isar-ids-to-regexp isar-ids-to-regexp178,4955 -(defconst isar-ext-first isar-ext-first212,6223 -(defconst isar-ext-rest isar-ext-rest213,6290 -(defconst isar-long-id-stuff isar-long-id-stuff215,6362 -(defconst isar-id isar-id216,6436 -(defconst isar-idx isar-idx217,6506 -(defconst isar-string isar-string219,6565 -(defconst isar-any-command-regexpisar-any-command-regexp221,6627 -(defconst isar-name-regexpisar-name-regexp225,6761 -(defconst isar-tac-regexpisar-tac-regexp229,6930 -(defconst isar-save-command-regexpisar-save-command-regexp233,7038 -(defconst isar-global-save-command-regexpisar-global-save-command-regexp236,7139 -(defconst isar-goal-command-regexpisar-goal-command-regexp239,7253 -(defconst isar-local-goal-command-regexpisar-local-goal-command-regexp242,7361 -(defconst isar-comment-start isar-comment-start245,7474 -(defconst isar-comment-end isar-comment-end246,7509 -(defconst isar-comment-start-regexp isar-comment-start-regexp247,7542 -(defconst isar-comment-end-regexp isar-comment-end-regexp248,7613 -(defconst isar-string-start-regexp isar-string-start-regexp250,7681 -(defconst isar-string-end-regexp isar-string-end-regexp251,7729 -(defconst isar-antiq-regexpisar-antiq-regexp260,7979 -(defface isabelle-class-name-faceisabelle-class-name-face267,8159 -(defface isabelle-tfree-name-faceisabelle-tfree-name-face277,8434 -(defface isabelle-tvar-name-faceisabelle-tvar-name-face287,8715 -(defface isabelle-free-name-faceisabelle-free-name-face297,8995 -(defface isabelle-bound-name-faceisabelle-bound-name-face307,9271 -(defface isabelle-var-name-faceisabelle-var-name-face317,9550 -(defconst isabelle-class-name-face isabelle-class-name-face327,9829 -(defconst isabelle-tfree-name-face isabelle-tfree-name-face328,9891 -(defconst isabelle-tvar-name-face isabelle-tvar-name-face329,9953 -(defconst isabelle-free-name-face isabelle-free-name-face330,10014 -(defconst isabelle-bound-name-face isabelle-bound-name-face331,10075 -(defconst isabelle-var-name-face isabelle-var-name-face332,10137 -(defvar isar-font-lock-keywords-1isar-font-lock-keywords-1334,10198 -(defvar isar-output-font-lock-keywords-1isar-output-font-lock-keywords-1348,11127 -(defvar isar-goals-font-lock-keywordsisar-goals-font-lock-keywords360,11783 -(defconst isar-undo isar-undo391,12417 -(defconst isar-kill isar-kill392,12479 -(defun isar-remove isar-remove394,12509 -(defun isar-undos isar-undos397,12588 -(defun isar-cannot-undo isar-cannot-undo401,12694 -(defconst isar-undo-fail-regexpisar-undo-fail-regexp405,12765 -(defconst isar-undo-skip-regexpisar-undo-skip-regexp409,12903 -(defconst isar-undo-ignore-regexpisar-undo-ignore-regexp412,13024 -(defconst isar-undo-remove-regexpisar-undo-remove-regexp415,13089 -(defconst isar-undo-kill-regexpisar-undo-kill-regexp420,13229 -(defconst isar-any-entity-regexpisar-any-entity-regexp426,13371 -(defconst isar-named-entity-regexpisar-named-entity-regexp431,13558 -(defconst isar-unnamed-entity-regexpisar-unnamed-entity-regexp436,13735 -(defconst isar-next-entity-regexpsisar-next-entity-regexps439,13837 -(defconst isar-generic-expressionisar-generic-expression447,14144 -(defconst isar-indent-any-regexpisar-indent-any-regexp458,14378 -(defconst isar-indent-inner-regexpisar-indent-inner-regexp460,14471 -(defconst isar-indent-enclose-regexpisar-indent-enclose-regexp462,14537 -(defconst isar-indent-open-regexpisar-indent-open-regexp464,14653 -(defconst isar-indent-close-regexpisar-indent-close-regexp466,14763 -(defconst isar-outline-regexpisar-outline-regexp472,14900 -(defconst isar-outline-heading-end-regexp isar-outline-heading-end-regexp476,15053 +(defconst isar-script-syntax-table-alistisar-script-syntax-table-alist58,1362 +(defun isar-init-syntax-table isar-init-syntax-table67,1645 +(defun isar-init-output-syntax-table isar-init-output-syntax-table75,1893 +(defconst isar-keywords-theory-encloseisar-keywords-theory-enclose90,2308 +(defconst isar-keywords-theoryisar-keywords-theory95,2460 +(defconst isar-keywords-saveisar-keywords-save100,2605 +(defconst isar-keywords-proof-encloseisar-keywords-proof-enclose105,2734 +(defconst isar-keywords-proofisar-keywords-proof111,2916 +(defconst isar-keywords-proof-contextisar-keywords-proof-context118,3114 +(defconst isar-keywords-local-goalisar-keywords-local-goal122,3228 +(defconst isar-keywords-improperisar-keywords-improper126,3340 +(defconst isar-keywords-outlineisar-keywords-outline131,3479 +(defconst isar-keywords-fumeisar-keywords-fume134,3544 +(defconst isar-keywords-indent-openisar-keywords-indent-open141,3762 +(defconst isar-keywords-indent-closeisar-keywords-indent-close147,3946 +(defconst isar-keywords-indent-encloseisar-keywords-indent-enclose151,4051 +(defun isar-regexp-simple-alt isar-regexp-simple-alt159,4230 +(defun isar-ids-to-regexp isar-ids-to-regexp179,4991 +(defconst isar-ext-first isar-ext-first213,6259 +(defconst isar-ext-rest isar-ext-rest214,6326 +(defconst isar-long-id-stuff isar-long-id-stuff216,6398 +(defconst isar-id isar-id217,6472 +(defconst isar-idx isar-idx218,6542 +(defconst isar-string isar-string220,6601 +(defconst isar-any-command-regexpisar-any-command-regexp222,6661 +(defconst isar-name-regexpisar-name-regexp226,6795 +(defconst isar-tac-regexpisar-tac-regexp232,7090 +(defconst isar-save-command-regexpisar-save-command-regexp236,7198 +(defconst isar-global-save-command-regexpisar-global-save-command-regexp239,7299 +(defconst isar-goal-command-regexpisar-goal-command-regexp242,7413 +(defconst isar-local-goal-command-regexpisar-local-goal-command-regexp245,7521 +(defconst isar-comment-start isar-comment-start248,7634 +(defconst isar-comment-end isar-comment-end249,7669 +(defconst isar-comment-start-regexp isar-comment-start-regexp250,7702 +(defconst isar-comment-end-regexp isar-comment-end-regexp251,7773 +(defconst isar-string-start-regexp isar-string-start-regexp253,7841 +(defconst isar-string-end-regexp isar-string-end-regexp254,7889 +(defconst isar-antiq-regexpisar-antiq-regexp263,8139 +(defface isabelle-class-name-faceisabelle-class-name-face270,8319 +(defface isabelle-tfree-name-faceisabelle-tfree-name-face280,8594 +(defface isabelle-tvar-name-faceisabelle-tvar-name-face290,8875 +(defface isabelle-free-name-faceisabelle-free-name-face300,9155 +(defface isabelle-bound-name-faceisabelle-bound-name-face310,9431 +(defface isabelle-var-name-faceisabelle-var-name-face320,9710 +(defconst isabelle-class-name-face isabelle-class-name-face330,9989 +(defconst isabelle-tfree-name-face isabelle-tfree-name-face331,10051 +(defconst isabelle-tvar-name-face isabelle-tvar-name-face332,10113 +(defconst isabelle-free-name-face isabelle-free-name-face333,10174 +(defconst isabelle-bound-name-face isabelle-bound-name-face334,10235 +(defconst isabelle-var-name-face isabelle-var-name-face335,10297 +(defvar isar-font-lock-keywords-1isar-font-lock-keywords-1337,10358 +(defvar isar-output-font-lock-keywords-1isar-output-font-lock-keywords-1351,11287 +(defvar isar-goals-font-lock-keywordsisar-goals-font-lock-keywords365,12077 +(defconst isar-undo isar-undo396,12711 +(defconst isar-kill isar-kill397,12773 +(defun isar-remove isar-remove399,12803 +(defun isar-undos isar-undos402,12878 +(defun isar-cannot-undo isar-cannot-undo406,12984 +(defconst isar-undo-fail-regexpisar-undo-fail-regexp410,13055 +(defconst isar-undo-skip-regexpisar-undo-skip-regexp414,13193 +(defconst isar-undo-ignore-regexpisar-undo-ignore-regexp417,13314 +(defconst isar-undo-remove-regexpisar-undo-remove-regexp420,13379 +(defconst isar-undo-kill-regexpisar-undo-kill-regexp425,13519 +(defconst isar-any-entity-regexpisar-any-entity-regexp431,13661 +(defconst isar-named-entity-regexpisar-named-entity-regexp436,13848 +(defconst isar-unnamed-entity-regexpisar-unnamed-entity-regexp441,14025 +(defconst isar-next-entity-regexpsisar-next-entity-regexps444,14127 +(defconst isar-generic-expressionisar-generic-expression452,14434 +(defconst isar-indent-any-regexpisar-indent-any-regexp463,14668 +(defconst isar-indent-inner-regexpisar-indent-inner-regexp465,14761 +(defconst isar-indent-enclose-regexpisar-indent-enclose-regexp467,14827 +(defconst isar-indent-open-regexpisar-indent-open-regexp469,14943 +(defconst isar-indent-close-regexpisar-indent-close-regexp471,15053 +(defconst isar-outline-regexpisar-outline-regexp477,15190 +(defconst isar-outline-heading-end-regexp isar-outline-heading-end-regexp481,15343 isar/x-symbol-isar.el,0 @@ -1822,6 +1692,233 @@ lego/lego-syntax.el,919 lego/x-symbol-lego.el,0 +lib/holes.el,3536 +(defun holes-short-doc holes-short-doc24,736 +(defcustom empty-hole-string empty-hole-string149,5370 +(defcustom empty-hole-regexp empty-hole-regexp152,5475 +(defcustom hole-search-limit hole-search-limit155,6075 +(defface active-hole-faceactive-hole-face168,6441 +(defface inactive-hole-faceinactive-hole-face178,6898 +(defun region-beginning-or-nil region-beginning-or-nil197,7434 +(defun region-end-or-nil region-end-or-nil201,7523 +(defun copy-active-region copy-active-region205,7602 +(defun is-hole-p is-hole-p211,7780 +(defun hole-start-position hole-start-position216,7840 +(defun hole-end-position hole-end-position221,7977 +(defun hole-buffer hole-buffer226,8107 +(defun hole-at hole-at231,8229 +(defun active-hole-exist-p active-hole-exist-p240,8417 +(defun active-hole-start-position active-hole-start-position250,8668 +(defun active-hole-end-position active-hole-end-position261,9018 +(defun active-hole-buffer active-hole-buffer273,9364 +(defun goto-active-hole goto-active-hole284,9644 +(defun highlight-hole-as-active highlight-hole-as-active296,9917 +(defun highlight-hole highlight-hole306,10224 +(defun disable-active-hole disable-active-hole317,10519 +(defun set-active-hole set-active-hole335,11028 +(defun is-in-hole-p is-in-hole-p347,11329 +(defun make-hole make-hole357,11474 +(defun make-hole-at make-hole-at382,12289 +(defun clear-hole clear-hole401,12731 +(defun clear-hole-at clear-hole-at411,12948 +(defun map-holes map-holes420,13177 +(defun mapcar-holes mapcar-holes426,13291 +(defun clear-all-buffer-holes clear-all-buffer-holes430,13390 +(defun next-hole next-hole442,13624 +(defun next-after-active-hole next-after-active-hole451,13888 +(defun set-active-hole-next set-active-hole-next458,14068 +(defun set-active-hole-next-after-active set-active-hole-next-after-active475,14425 +(defun replace-segment replace-segment486,14583 +(defun replace-hole replace-hole502,14899 +(defun replace-active-hole replace-active-hole536,16055 +(defun replace-update-active-hole replace-update-active-hole545,16338 +(defun delete-update-active-hole delete-update-active-hole568,16964 +(defun set-make-active-hole set-make-active-hole577,17161 +(defun mouse-replace-active-hole mouse-replace-active-hole624,18508 +(defun destroy-hole destroy-hole642,18984 +(defun hole-at-event hole-at-event657,19295 +(defun mouse-destroy-hole mouse-destroy-hole659,19354 +(defun mouse-forget-hole mouse-forget-hole667,19528 +(defun mouse-set-make-active-hole mouse-set-make-active-hole681,19769 +(defun mouse-set-active-hole mouse-set-active-hole701,20220 +(defun set-point-next-hole-destroy set-point-next-hole-destroy711,20414 +(defun count-char-in-string count-char-in-string775,22661 +(defun count-re-in-string count-re-in-string785,22866 +(defun count-chars-in-last-expand count-chars-in-last-expand795,23077 +(defun count-newlines-in-last-expand count-newlines-in-last-expand799,23166 +(defun indent-last-expand indent-last-expand803,23277 +(defun count-holes-in-last-expand count-holes-in-last-expand818,23603 +(defun replace-string-by-holes replace-string-by-holes822,23722 +(defun replace-string-by-holes-backward replace-string-by-holes-backward841,24148 +(defun replace-string-by-holes-move-point replace-string-by-holes-move-point872,24966 +(defun replace-string-by-holes-backward-move-point replace-string-by-holes-backward-move-point879,25120 +(defun holes-abbrev-complete holes-abbrev-complete889,25296 +(defun insert-and-expand insert-and-expand911,26098 + +lib/proof-compat.el,1194 +(defvar proof-running-on-XEmacs proof-running-on-XEmacs24,760 +(defvar proof-running-on-Emacs21 proof-running-on-Emacs2126,882 +(defvar proof-running-on-win32 proof-running-on-win3230,1129 +(defun pg-custom-undeclare-variable pg-custom-undeclare-variable41,1562 +(defun subst-char-in-string subst-char-in-string112,3702 +(defun replace-regexp-in-string replace-regexp-in-string126,4256 +(defconst menuvisiblep menuvisiblep188,6969 +(defun set-window-text-height set-window-text-height205,7588 +(defmacro save-selected-frame save-selected-frame231,8538 +(defun warn warn270,9840 +(defun redraw-modeline redraw-modeline277,10095 +(defun replace-in-string replace-in-string292,10662 +(defun proof-buffer-syntactic-context-emulate proof-buffer-syntactic-context-emulate341,12180 +(defvar read-shell-command-mapread-shell-command-map374,13487 +(defun read-shell-command read-shell-command392,14189 +(defun remassq remassq404,14670 +(defun remassoc remassoc416,15059 +(defun frames-of-buffer frames-of-buffer429,15504 +(defmacro with-selected-window with-selected-window468,16767 +(defun pg-pop-to-buffer pg-pop-to-buffer504,17892 +(defun process-live-p process-live-p555,19744 + +lib/span.el,192 +(defsubst delete-spans delete-spans22,471 +(defsubst span-property-safe span-property-safe26,625 +(defsubst set-span-start set-span-start30,764 +(defsubst set-span-end set-span-end34,896 + +lib/span-extent.el,1346 +(defsubst make-span make-span16,557 +(defsubst detach-span detach-span20,679 +(defsubst set-span-endpoints set-span-endpoints24,766 +(defsubst set-span-property set-span-property28,899 +(defsubst span-read-only span-read-only32,1026 +(defsubst span-read-write span-read-write36,1130 +(defun span-give-warning span-give-warning40,1237 +(defun span-write-warning span-write-warning44,1335 +(defsubst span-property span-property49,1535 +(defsubst delete-span delete-span53,1650 +(defsubst mapcar-spans mapcar-spans59,1821 +(defsubst span-at span-at63,2027 +(defsubst span-at-before span-at-before67,2144 +(defsubst span-start span-start72,2341 +(defsubst span-end span-end76,2470 +(defsubst prev-span prev-span80,2593 +(defsubst next-span next-span84,2739 +(defsubst span-live-p span-live-p88,2881 +(defun span-raise span-raise96,3153 +(defalias 'span-object span-object100,3252 +(defalias 'span-string span-string101,3291 +(defsubst make-detached-span make-detached-span104,3377 +(defsubst span-buffer span-buffer110,3474 +(defsubst span-detached-p span-detached-p115,3566 +(defsubst set-span-face set-span-face120,3678 +(defsubst fold-spans fold-spans125,3774 +(defsubst set-span-properties set-span-properties130,3972 +(defsubst set-span-keymap set-span-keymap135,4081 +(defsubst span-at-event span-at-event140,4196 + +lib/span-overlay.el,2198 +(defvar before-list before-list20,771 +(defun foldr foldr27,906 +(defun foldl foldl39,1239 +(defsubst span-start span-start51,1556 +(defsubst span-end span-end55,1648 +(defun set-span-property set-span-property59,1734 +(defsubst span-property span-property63,1850 +(defun span-read-only-hook span-read-only-hook67,1961 +(defun span-read-only span-read-only71,2093 +(defun span-read-write span-read-write86,2871 +(defun span-give-warning span-give-warning92,3090 +(defun span-write-warning span-write-warning96,3198 +(defun int-nil-lt int-nil-lt101,3421 +(defun span-lt span-lt110,3624 +(defun span-traverse span-traverse115,3783 +(defun add-span add-span131,4230 +(defun make-span make-span145,4632 +(defun remove-span remove-span149,4763 +(defun spans-at-point spans-at-point162,5216 +(defun append-unique append-unique176,5696 +(defun spans-at-region spans-at-region179,5783 +(defun spans-at-point-prop spans-at-point-prop186,6005 +(defun spans-at-region-prop spans-at-region-prop194,6255 +(defun span-at span-at206,6602 +(defsubst detach-span detach-span212,6816 +(defsubst delete-span delete-span218,6943 +(defsubst set-span-endpoints set-span-endpoints226,7186 +(defsubst mapcar-spans mapcar-spans233,7402 +(defun map-spans-aux map-spans-aux237,7606 +(defsubst map-spans map-spans241,7721 +(defun find-span-aux find-span-aux244,7779 +(defun find-span find-span249,7905 +(defun span-at-before span-at-before252,7970 +(defun prev-span prev-span265,8412 +(defun next-span next-span274,8694 +(defsubst span-live-p span-live-p299,9678 +(defun span-raise span-raise305,9844 +(defalias 'span-object span-object311,10075 +(defun span-string span-string313,10116 +(defun set-span-properties set-span-properties319,10298 +(defun span-find-span span-find-span331,10553 +(defsubst span-at-event span-at-event342,10912 +(defun make-detached-span make-detached-span347,11036 +(defun fold-spans-aux fold-spans-aux353,11170 +(defun fold-spans fold-spans361,11426 +(defsubst span-buffer span-buffer368,11634 +(defsubst span-detached-p span-detached-p373,11726 +(defsubst set-span-face set-span-face381,11922 +(defsubst set-span-keymap set-span-keymap386,12022 + +lib/texi-docstring-magic.el,958 +(defun texi-docstring-magic-find-face texi-docstring-magic-find-face85,2996 +(defun texi-docstring-magic-splice-sep texi-docstring-magic-splice-sep90,3161 +(defconst texi-docstring-magic-munge-tabletexi-docstring-magic-munge-table100,3466 +(defun texi-docstring-magic-untabify texi-docstring-magic-untabify190,7186 +(defun texi-docstring-magic-munge-docstring texi-docstring-magic-munge-docstring200,7501 +(defun texi-docstring-magic-texi texi-docstring-magic-texi239,8788 +(defun texi-docstring-magic-format-default texi-docstring-magic-format-default252,9228 +(defun texi-docstring-magic-texi-for texi-docstring-magic-texi-for268,9863 +(defconst texi-docstring-magic-commenttexi-docstring-magic-comment326,11823 +(defun texi-docstring-magic texi-docstring-magic332,11977 +(defun texi-docstring-magic-face-at-point texi-docstring-magic-face-at-point366,13057 +(defun texi-docstring-magic-insert-magic texi-docstring-magic-insert-magic381,13580 + +lib/url-parse.el,921 +(defmacro url-type url-type28,1226 +(defmacro url-user url-user31,1282 +(defmacro url-password url-password34,1338 +(defmacro url-host url-host37,1398 +(defmacro url-port url-port40,1454 +(defmacro url-filename url-filename45,1613 +(defmacro url-target url-target48,1673 +(defmacro url-attributes url-attributes51,1731 +(defmacro url-fullness url-fullness54,1793 +(defmacro url-set-type url-set-type57,1853 +(defmacro url-set-user url-set-user60,1927 +(defmacro url-set-password url-set-password63,2001 +(defmacro url-set-host url-set-host66,2079 +(defmacro url-set-port url-set-port69,2153 +(defmacro url-set-filename url-set-filename72,2227 +(defmacro url-set-target url-set-target75,2305 +(defmacro url-set-attributes url-set-attributes78,2381 +(defmacro url-set-full url-set-full81,2461 +(defun url-recreate-url url-recreate-url84,2535 +(defun url-generic-parse-url url-generic-parse-url109,3289 + +lib/xml.el,790 +(defsubst xml-node-name xml-node-name82,2907 +(defsubst xml-node-attributes xml-node-attributes87,3026 +(defsubst xml-node-children xml-node-children92,3144 +(defun xml-get-children xml-get-children97,3280 +(defun xml-get-attribute xml-get-attribute107,3603 +(defun xml-parse-file xml-parse-file123,4067 +(defun xml-parse-region xml-parse-region144,4651 +(defun xml-parse-tag xml-parse-tag179,5696 +(defun xml-parse-attlist xml-parse-attlist284,9165 +(defun xml-skip-dtd xml-skip-dtd321,10555 +(defun xml-parse-dtd xml-parse-dtd338,11191 +(defun xml-parse-elem-type xml-parse-elem-type408,13269 +(defun xml-substitute-special xml-substitute-special449,14424 +(defun xml-debug-print xml-debug-print470,15231 +(defun xml-debug-print-internal xml-debug-print-internal474,15323 + mmm/mmm-auto.el,499 (defvar mmm-autoloaded-classesmmm-autoloaded-classes67,2675 (defun mmm-autoload-class mmm-autoload-class85,3320 @@ -2045,24 +2142,26 @@ mmm/mmm-vars.el,3586 (defun mmm-mode-ext-applies mmm-mode-ext-applies737,28391 (defun mmm-get-all-classes mmm-get-all-classes751,28875 -phox/phox.el,886 +phox/phox.el,1008 (defcustom phox-prog-name phox-prog-name30,907 (defcustom phox-sym-lock phox-sym-lock35,1009 -(defcustom phox-web-pagephox-web-page40,1107 -(defcustom phox-doc-dir phox-doc-dir46,1257 -(defcustom phox-lib-dir phox-lib-dir52,1405 -(defcustom phox-tags-program phox-tags-program58,1549 -(defcustom phox-tags-doc phox-tags-doc64,1729 -(defcustom phox-etags phox-etags70,1867 -(defpgdefault menu-entriesmenu-entries90,2297 -(defun phox-config phox-config107,2626 -(defun phox-shell-config phox-shell-config149,4550 -(define-derived-mode phox-mode phox-mode189,6130 -(define-derived-mode phox-shell-mode phox-shell-mode204,6574 -(define-derived-mode phox-response-mode phox-response-mode209,6702 -(define-derived-mode phox-goals-mode phox-goals-mode221,7121 -(defun phox-pre-shell-start phox-pre-shell-start247,8180 -(defpgdefault completion-tablecompletion-table261,8694 +(defcustom phox-x-symbol-enable phox-x-symbol-enable40,1133 +(defcustom phox-web-pagephox-web-page45,1238 +(defcustom phox-doc-dir phox-doc-dir51,1388 +(defcustom phox-lib-dir phox-lib-dir57,1536 +(defcustom phox-tags-program phox-tags-program63,1680 +(defcustom phox-tags-doc phox-tags-doc69,1860 +(defcustom phox-etags phox-etags75,1998 +(defpgdefault menu-entriesmenu-entries95,2428 +(defun phox-config phox-config112,2757 +(defun phox-shell-config phox-shell-config154,4681 +(define-derived-mode phox-mode phox-mode194,6261 +(define-derived-mode phox-shell-mode phox-shell-mode209,6705 +(define-derived-mode phox-response-mode phox-response-mode214,6833 +(define-derived-mode phox-goals-mode phox-goals-mode226,7252 +(defun phox-pre-shell-start phox-pre-shell-start252,8311 +(defpgdefault completion-tablecompletion-table266,8825 +(defpgdefault x-symbol-language x-symbol-language286,9405 phox/phox-extraction.el,603 (defvar phox-prog-orig phox-prog-orig11,480 @@ -2148,42 +2247,43 @@ phox/phox-tags.el,483 (defun phox-complete-tag(phox-complete-tag77,2349 (defvar phox-tags-menuphox-tags-menu96,2904 -phox/x-symbol-phox.el,2672 -(defvar x-symbol-phox-required-fonts x-symbol-phox-required-fonts21,705 -(defvar x-symbol-phox-name x-symbol-phox-name31,1204 -(defvar x-symbol-phox-modeline-name x-symbol-phox-modeline-name32,1246 -(defcustom x-symbol-phox-header-groups-alist x-symbol-phox-header-groups-alist34,1291 -(defcustom x-symbol-phox-electric-ignore x-symbol-phox-electric-ignore41,1511 -(defvar x-symbol-phox-required-fonts x-symbol-phox-required-fonts48,1759 -(defvar x-symbol-phox-extra-menu-items x-symbol-phox-extra-menu-items51,1860 -(defvar x-symbol-phox-token-grammarx-symbol-phox-token-grammar55,1950 -(defvar x-symbol-phox-input-token-grammarx-symbol-phox-input-token-grammar66,2456 -(defun x-symbol-phox-default-token-list x-symbol-phox-default-token-list72,2711 -(defvar x-symbol-phox-user-table x-symbol-phox-user-table84,3000 -(defvar x-symbol-phox-generated-data x-symbol-phox-generated-data87,3109 -(defvar x-symbol-phox-master-directory x-symbol-phox-master-directory95,3348 -(defvar x-symbol-phox-image-searchpath x-symbol-phox-image-searchpath96,3397 -(defvar x-symbol-phox-image-cached-dirs x-symbol-phox-image-cached-dirs97,3445 -(defvar x-symbol-phox-image-file-truename-alist x-symbol-phox-image-file-truename-alist98,3511 -(defvar x-symbol-phox-image-keywords x-symbol-phox-image-keywords99,3564 -(defcustom x-symbol-phox-class-alistx-symbol-phox-class-alist105,3784 -(defcustom x-symbol-phox-class-face-alist x-symbol-phox-class-face-alist116,4166 -(defvar x-symbol-phox-font-lock-keywords x-symbol-phox-font-lock-keywords126,4479 -(defvar x-symbol-phox-font-lock-allowed-faces x-symbol-phox-font-lock-allowed-faces128,4526 -(defvar x-symbol-phox-case-insensitive x-symbol-phox-case-insensitive134,4751 -(defvar x-symbol-phox-token-shape x-symbol-phox-token-shape135,4795 -(defvar x-symbol-phox-input-token-ignore x-symbol-phox-input-token-ignore136,4834 -(defvar x-symbol-phox-token-list x-symbol-phox-token-list143,5073 -(defvar x-symbol-phox-xsymb0-table x-symbol-phox-xsymb0-table145,5118 -(defun x-symbol-phox-prepare-table x-symbol-phox-prepare-table166,5573 -(defvar x-symbol-phox-tablex-symbol-phox-table173,5744 -(defvar x-symbol-phox-menu-alist x-symbol-phox-menu-alist184,6116 -(defvar x-symbol-phox-grid-alist x-symbol-phox-grid-alist186,6206 -(defvar x-symbol-phox-decode-atree x-symbol-phox-decode-atree189,6297 -(defvar x-symbol-phox-decode-alist x-symbol-phox-decode-alist191,6390 -(defvar x-symbol-phox-encode-alist x-symbol-phox-encode-alist193,6487 -(defvar x-symbol-phox-nomule-decode-exec x-symbol-phox-nomule-decode-exec197,6644 -(defvar x-symbol-phox-nomule-encode-exec x-symbol-phox-nomule-encode-exec199,6744 +phox/x-symbol-phox.el,2739 +(defvar x-symbol-phox-required-fonts x-symbol-phox-required-fonts14,449 +(defvar x-symbol-phox-name x-symbol-phox-name24,946 +(defvar x-symbol-phox-modeline-name x-symbol-phox-modeline-name25,988 +(defcustom x-symbol-phox-header-groups-alist x-symbol-phox-header-groups-alist27,1033 +(defcustom x-symbol-phox-electric-ignore x-symbol-phox-electric-ignore34,1253 +(defvar x-symbol-phox-required-fonts x-symbol-phox-required-fonts41,1501 +(defvar x-symbol-phox-extra-menu-items x-symbol-phox-extra-menu-items44,1602 +(defvar x-symbol-phox-token-grammarx-symbol-phox-token-grammar47,1691 +(defvar x-symbol-phox-input-token-grammarx-symbol-phox-input-token-grammar59,2220 +(defun x-symbol-phox-default-token-list x-symbol-phox-default-token-list65,2475 +(defvar x-symbol-phox-user-table x-symbol-phox-user-table77,2764 +(defvar x-symbol-phox-generated-data x-symbol-phox-generated-data80,2873 +(defvar x-symbol-phox-master-directory x-symbol-phox-master-directory88,3112 +(defvar x-symbol-phox-image-searchpath x-symbol-phox-image-searchpath89,3161 +(defvar x-symbol-phox-image-cached-dirs x-symbol-phox-image-cached-dirs90,3209 +(defvar x-symbol-phox-image-file-truename-alist x-symbol-phox-image-file-truename-alist91,3275 +(defvar x-symbol-phox-image-keywords x-symbol-phox-image-keywords92,3328 +(defcustom x-symbol-phox-class-alistx-symbol-phox-class-alist99,3549 +(defcustom x-symbol-phox-class-face-alist x-symbol-phox-class-face-alist110,3931 +(defvar x-symbol-phox-font-lock-keywords x-symbol-phox-font-lock-keywords120,4244 +(defvar x-symbol-phox-font-lock-allowed-faces x-symbol-phox-font-lock-allowed-faces122,4291 +(defvar x-symbol-phox-case-insensitive x-symbol-phox-case-insensitive128,4516 +(defvar x-symbol-phox-token-shape x-symbol-phox-token-shape129,4560 +(defvar x-symbol-phox-input-token-ignore x-symbol-phox-input-token-ignore130,4599 +(defvar x-symbol-phox-token-list x-symbol-phox-token-list137,4838 +(defvar x-symbol-phox-xsymb0-table x-symbol-phox-xsymb0-table139,4883 +(defun x-symbol-phox-prepare-table x-symbol-phox-prepare-table160,5342 +(defvar x-symbol-phox-tablex-symbol-phox-table167,5513 +(defcustom x-symbol-phox-auto-stylex-symbol-phox-auto-style178,5831 +(defvar x-symbol-phox-menu-alist x-symbol-phox-menu-alist204,6781 +(defvar x-symbol-phox-grid-alist x-symbol-phox-grid-alist206,6871 +(defvar x-symbol-phox-decode-atree x-symbol-phox-decode-atree209,6962 +(defvar x-symbol-phox-decode-alist x-symbol-phox-decode-alist211,7055 +(defvar x-symbol-phox-encode-alist x-symbol-phox-encode-alist213,7152 +(defvar x-symbol-phox-nomule-decode-exec x-symbol-phox-nomule-decode-exec217,7309 +(defvar x-symbol-phox-nomule-encode-exec x-symbol-phox-nomule-encode-exec219,7409 plastic/plastic.el,4425 (defcustom plastic-tags plastic-tags28,805 @@ -2496,186 +2596,187 @@ twelf/twelf-old.el,10513 twelf/x-symbol-twelf.el,0 todo,1297 - function to to373,15257 + function to to383,15505 $Id: todo,2,21 This is an outline file. Use C-c C-n,4,67 -X 41,1156 -*** C Improved configurability of command settings,172,6638 - We should let command settings,173,6695 - We should let command settings, etc,173,6695 - - XEmacs pg forces on font-lock,323,12844 - Save foo;399,16380 -*** A Doc new bits: font lock keywords,469,19081 -*** A Doc new bits: font lock keywords, filename %e,469,19081 - Added proof-{script,470,19138 - Added proof-{script,shell,470,19138 - Added proof-{script,shell,goals,470,19138 - Presently used only in proof-easy-config,471,19198 - - Mention configuring function menus,482,19534 - - document mouse functions,484,19620 - - document mouse functions, proof-cd,484,19620 - - document mouse functions, proof-cd, process quit timeout,484,19620 - X-Symbol,485,19683 - X-Symbol, prog-name-guess,485,19683 -*** D Fix INFO-DIR-ENTRY in 499,20191 -*** C Fixing up errors caused by pbp-generated commands; currently,565,22668 - should mean generates an error. With LEGO pbp,568,22874 - tactic which always succeeds,569,22938 - decodes annotations eagerly. Lazily would be faster,577,23294 - the tech report claims --- djs: probably not much faster,578,23363 -*** 6. Update Emacs and prover versions in texi,667,26366 - -doc/ProofGeneral.texi,5815 -@node TopTop166,5018 -@node PrefacePreface203,6141 -@node Latest news for 3.5Latest news for 3.5226,6729 -@node FutureFuture264,8387 -@node CreditsCredits299,9937 -@node Introducing Proof GeneralIntroducing Proof General397,13352 -@node Quick start guideQuick start guide452,15344 -@node Features of Proof GeneralFeatures of Proof General506,17913 -@node Supported proof assistantsSupported proof assistants595,21838 -@node Prerequisites for this manualPrerequisites for this manual647,23834 -@node Organization of this manualOrganization of this manual691,25460 -@node Basic Script ManagementBasic Script Management717,26287 -@node Walkthrough example in Isabelle/IsarWalkthrough example in Isabelle/Isar736,26892 -@node Proof scriptsProof scripts963,35427 -@node Script buffersScript buffers1006,37547 -@node Locked queue and editing regionsLocked queue and editing regions1028,38124 -@node Goal-save sequencesGoal-save sequences1084,40271 -@node Active scripting bufferActive scripting buffer1121,41757 -@node Summary of Proof General buffersSummary of Proof General buffers1190,45177 -@node Script editing commandsScript editing commands1252,47851 -@node Script processing commandsScript processing commands1329,50614 -@node Proof assistant commandsProof assistant commands1457,55915 -@node Toolbar commandsToolbar commands1603,60802 -@node Interrupting during trace outputInterrupting during trace output1627,61731 -@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing1666,63654 -@node Goals buffer commandsGoals buffer commands1680,64154 -@node Advanced Script ManagementAdvanced Script Management1769,67686 -@node Visibility of completed proofsVisibility of completed proofs1800,68840 -@node Switching between proof scriptsSwitching between proof scripts1855,70763 -@node View of processed files View of processed files 1892,72735 -@node Retracting across filesRetracting across files1952,75786 -@node Asserting across filesAsserting across files1965,76417 -@node Automatic multiple file handlingAutomatic multiple file handling1978,76983 -@node Escaping script managementEscaping script management2003,78017 -@node Experimental featuresExperimental features2061,80220 -@node Support for other PackagesSupport for other Packages2095,81482 -@node Syntax highlightingSyntax highlighting2127,82357 -@node X-Symbol supportX-Symbol support2166,83966 -@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)2225,86512 -@node Support for outline modeSupport for outline mode2284,88642 -@node Support for completionSupport for completion2310,89772 -@node Support for tagsSupport for tags2367,91935 -@node Customizing Proof GeneralCustomizing Proof General2419,94263 -@node Basic optionsBasic options2459,95933 -@node How to customizeHow to customize2483,96691 -@node Display customizationDisplay customization2534,98781 -@node User optionsUser options2659,104015 -@node Changing facesChanging faces2913,113021 -@node Tweaking configuration settingsTweaking configuration settings2988,115690 -@node Hints and TipsHints and Tips3045,118215 -@node Adding your own keybindingsAdding your own keybindings3064,118816 -@node Using file variablesUsing file variables3120,121349 -@node Using abbreviationsUsing abbreviations3173,123172 -@node LEGO Proof GeneralLEGO Proof General3212,124587 -@node LEGO specific commandsLEGO specific commands3253,125956 -@node LEGO tagsLEGO tags3273,126411 -@node LEGO customizationsLEGO customizations3283,126658 -@node Coq Proof GeneralCoq Proof General3315,127576 -@node Coq-specific commandsCoq-specific commands3331,127985 -@node Coq-specific variablesCoq-specific variables3353,128492 -@node Editing multiple proofsEditing multiple proofs3391,129707 -@node User-loaded tacticsUser-loaded tactics3415,130815 -@node Holes featureHoles feature3480,133342 -@node Isabelle Proof GeneralIsabelle Proof General3507,134628 -@node Classic IsabelleClassic Isabelle3576,137951 -@node ML filesML files3592,138389 -@node Theory filesTheory files3663,140814 -@node General commands for IsabelleGeneral commands for Isabelle3717,143285 -@node Specific commands for IsabelleSpecific commands for Isabelle3729,143767 -@node Isabelle customizationsIsabelle customizations3758,144707 -@node Isabelle/IsarIsabelle/Isar3823,146805 -@node General commands for Isabelle/IsarGeneral commands for Isabelle/Isar3844,147568 -@node Specific commands for Isabelle/IsarSpecific commands for Isabelle/Isar3851,147822 -@node Logics and SettingsLogics and Settings3938,150350 -@node HOL Proof GeneralHOL Proof General3979,152038 -@node Shell Proof GeneralShell Proof General4020,153822 -@node Obtaining and InstallingObtaining and Installing4056,155280 -@node Obtaining Proof GeneralObtaining Proof General4072,155693 -@node Installing Proof General from tarballInstalling Proof General from tarball4103,156932 -@node Installing Proof General from RPM packageInstalling Proof General from RPM package4128,157764 -@node Setting the names of binariesSetting the names of binaries4143,158172 -@node Notes for syssiesNotes for syssies4171,159100 -@node Known bugs and workaroundsKnown bugs and workarounds4244,162049 -@node ReferencesReferences4257,162482 -@node History of Proof GeneralHistory of Proof General4297,163506 -@node Old News for 3.0Old News for 3.04388,167608 -@node Old News for 3.1Old News for 3.14458,171302 -@node Old News for 3.2Old News for 3.24484,172474 -@node Old News for 3.3Old News for 3.34545,175477 -@node Old News for 3.4Old News for 3.44564,176374 -@node Function IndexFunction Index4587,177430 -@node Variable IndexVariable Index4591,177506 -@node Keystroke IndexKeystroke Index4595,177586 -@node Concept IndexConcept Index4599,177652 - -doc/PG-adapting.texi,3791 -@node TopTop157,4774 -@node IntroductionIntroduction194,5888 -@node FutureFuture235,7541 -@node CreditsCredits271,9137 -@node Beginning with a new proverBeginning with a new prover281,9429 -@node Overview of adding a new proverOverview of adding a new prover322,11378 -@node Demonstration instance and easy configurationDemonstration instance and easy configuration396,14799 -@node Major modes used by Proof GeneralMajor modes used by Proof General465,18190 -@node Menus and toolbar and user-level commandsMenus and toolbar and user-level commands538,21273 -@node Settings for generic user-level commandsSettings for generic user-level commands553,21819 -@node Menu configurationMenu configuration598,23555 -@node Toolbar configurationToolbar configuration622,24473 -@node Proof script settingsProof script settings680,26718 -@node Recognizing commands and commentsRecognizing commands and comments702,27298 -@node Recognizing proofsRecognizing proofs823,32825 -@node Recognizing other elementsRecognizing other elements935,37639 -@node Configuring undo behaviourConfiguring undo behaviour1061,43117 -@node Nested proofsNested proofs1199,48458 -@node Safe (state-preserving) commandsSafe (state-preserving) commands1239,50085 -@node Activate scripting hookActivate scripting hook1262,51031 -@node Automatic multiple filesAutomatic multiple files1286,51895 -@node CompletionsCompletions1308,52742 -@node Proof shell settingsProof shell settings1348,54218 -@node Proof shell commandsProof shell commands1379,55500 -@node Script input to the shellScript input to the shell1542,62375 -@node Settings for matching various output from proof processSettings for matching various output from proof process1609,65418 -@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process1740,71182 -@node Hooks and other settingsHooks and other settings1950,80735 -@node Goals buffer settingsGoals buffer settings2046,84568 -@node Splash screen settingsSplash screen settings2123,87676 -@node Global constantsGlobal constants2149,88434 -@node Handling multiple filesHandling multiple files2175,89283 -@node Configuring Font LockConfiguring Font Lock2327,97067 -@node Configuring X-SymbolConfiguring X-Symbol2370,98960 -@node Writing more lisp codeWriting more lisp code2430,101483 -@node Default values for generic settingsDefault values for generic settings2447,102128 -@node Adding prover-specific configurationsAdding prover-specific configurations2477,103211 -@node Useful variablesUseful variables2520,104481 -@node Useful functions and macrosUseful functions and macros2546,105275 -@node Internals of Proof GeneralInternals of Proof General2648,109152 -@node SpansSpans2676,110060 -@node Proof General site configurationProof General site configuration2689,110434 -@node Configuration variable mechanismsConfiguration variable mechanisms2769,113578 -@node Global variablesGlobal variables2887,118814 -@node Proof script modeProof script mode2957,121364 -@node Proof shell modeProof shell mode3216,133019 -@node DebuggingDebugging3622,149066 -@node Plans and ideasPlans and ideas3665,149961 -@node Proof by pointing and similar featuresProof by pointing and similar features3686,150683 -@node Granularity of atomic command sequencesGranularity of atomic command sequences3724,152341 -@node Browser mode for script files and theoriesBrowser mode for script files and theories3769,154566 -@node Demonstration InstantiationsDemonstration Instantiations3799,155597 -@node demoisa-easy.eldemoisa-easy.el3815,156028 -@node demoisa.eldemoisa.el3878,158266 -@node Function IndexFunction Index4046,163782 -@node Variable IndexVariable Index4050,163858 -@node Concept IndexConcept Index4059,164037 +X 51,1404 +*** C Improved configurability of command settings,182,6886 + We should let command settings,183,6943 + We should let command settings, etc,183,6943 + - XEmacs pg forces on font-lock,333,13092 + Save foo;409,16628 +*** A Doc new bits: font lock keywords,479,19329 +*** A Doc new bits: font lock keywords, filename %e,479,19329 + Added proof-{script,480,19386 + Added proof-{script,shell,480,19386 + Added proof-{script,shell,goals,480,19386 + Presently used only in proof-easy-config,481,19446 + - Mention configuring function menus,492,19782 + - document mouse functions,494,19868 + - document mouse functions, proof-cd,494,19868 + - document mouse functions, proof-cd, process quit timeout,494,19868 + X-Symbol,495,19931 + X-Symbol, prog-name-guess,495,19931 +*** D Fix INFO-DIR-ENTRY in 509,20439 +*** C Fixing up errors caused by pbp-generated commands; currently,575,22916 + should mean generates an error. With LEGO pbp,578,23122 + tactic which always succeeds,579,23186 + decodes annotations eagerly. Lazily would be faster,587,23542 + the tech report claims --- djs: probably not much faster,588,23611 +*** 6. Update Emacs and prover versions in texi,677,26614 + +doc/ProofGeneral.texi,5783 +@node TopTop166,5019 +@node PrefacePreface203,6126 +@node Latest news for 3.5Latest news for 3.5226,6714 +@node FutureFuture264,8372 +@node CreditsCredits299,9922 +@node Introducing Proof GeneralIntroducing Proof General397,13337 +@node Quick start guideQuick start guide452,15329 +@node Features of Proof GeneralFeatures of Proof General506,17898 +@node Supported proof assistantsSupported proof assistants595,21823 +@node Prerequisites for this manualPrerequisites for this manual647,23819 +@node Organization of this manualOrganization of this manual691,25445 +@node Basic Script ManagementBasic Script Management717,26272 +@node Walkthrough example in Isabelle/IsarWalkthrough example in Isabelle/Isar736,26877 +@node Proof scriptsProof scripts963,35412 +@node Script buffersScript buffers1006,37532 +@node Locked queue and editing regionsLocked queue and editing regions1028,38109 +@node Goal-save sequencesGoal-save sequences1084,40256 +@node Active scripting bufferActive scripting buffer1121,41742 +@node Summary of Proof General buffersSummary of Proof General buffers1190,45162 +@node Script editing commandsScript editing commands1252,47836 +@node Script processing commandsScript processing commands1330,50694 +@node Proof assistant commandsProof assistant commands1458,55995 +@node Toolbar commandsToolbar commands1604,60882 +@node Interrupting during trace outputInterrupting during trace output1628,61811 +@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing1667,63734 +@node Goals buffer commandsGoals buffer commands1681,64234 +@node Advanced Script ManagementAdvanced Script Management1770,67766 +@node Visibility of completed proofsVisibility of completed proofs1801,68920 +@node Switching between proof scriptsSwitching between proof scripts1856,70843 +@node View of processed files View of processed files 1893,72815 +@node Retracting across filesRetracting across files1953,75866 +@node Asserting across filesAsserting across files1966,76497 +@node Automatic multiple file handlingAutomatic multiple file handling1979,77063 +@node Escaping script managementEscaping script management2004,78097 +@node Experimental featuresExperimental features2062,80300 +@node Support for other PackagesSupport for other Packages2096,81562 +@node Syntax highlightingSyntax highlighting2128,82437 +@node X-Symbol supportX-Symbol support2167,84046 +@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)2226,86592 +@node Support for outline modeSupport for outline mode2285,88722 +@node Support for completionSupport for completion2311,89852 +@node Support for tagsSupport for tags2368,92017 +@node Customizing Proof GeneralCustomizing Proof General2420,94345 +@node Basic optionsBasic options2460,96015 +@node How to customizeHow to customize2484,96773 +@node Display customizationDisplay customization2535,98863 +@node User optionsUser options2660,104097 +@node Changing facesChanging faces2914,113103 +@node Tweaking configuration settingsTweaking configuration settings2989,115772 +@node Hints and TipsHints and Tips3046,118297 +@node Adding your own keybindingsAdding your own keybindings3065,118898 +@node Using file variablesUsing file variables3121,121431 +@node Using abbreviationsUsing abbreviations3174,123254 +@node LEGO Proof GeneralLEGO Proof General3213,124669 +@node LEGO specific commandsLEGO specific commands3254,126038 +@node LEGO tagsLEGO tags3274,126493 +@node LEGO customizationsLEGO customizations3284,126740 +@node Coq Proof GeneralCoq Proof General3316,127658 +@node Coq-specific commandsCoq-specific commands3332,128067 +@node Coq-specific variablesCoq-specific variables3354,128574 +@node Editing multiple proofsEditing multiple proofs3392,129789 +@node User-loaded tacticsUser-loaded tactics3416,130897 +@node Holes featureHoles feature3481,133424 +@node Isabelle Proof GeneralIsabelle Proof General3508,134710 +@node Classic IsabelleClassic Isabelle3577,138033 +@node ML filesML files3593,138471 +@node Theory filesTheory files3664,140896 +@node General commands for IsabelleGeneral commands for Isabelle3718,143367 +@node Specific commands for IsabelleSpecific commands for Isabelle3730,143849 +@node Isabelle customizationsIsabelle customizations3759,144789 +@node Isabelle/IsarIsabelle/Isar3824,146887 +@node General commands for Isabelle/IsarGeneral commands for Isabelle/Isar3845,147650 +@node Specific commands for Isabelle/IsarSpecific commands for Isabelle/Isar3852,147904 +@node Logics and SettingsLogics and Settings3939,150432 +@node HOL Proof GeneralHOL Proof General3980,152120 +@node Shell Proof GeneralShell Proof General4021,153904 +@node Obtaining and InstallingObtaining and Installing4057,155362 +@node Obtaining Proof GeneralObtaining Proof General4073,155775 +@node Installing Proof General from tarballInstalling Proof General from tarball4104,157014 +@node Installing Proof General from RPM packageInstalling Proof General from RPM package4129,157846 +@node Setting the names of binariesSetting the names of binaries4144,158254 +@node Notes for syssiesNotes for syssies4172,159182 +@node Known BugsKnown Bugs4245,162115 +@node ReferencesReferences4258,162516 +@node History of Proof GeneralHistory of Proof General4298,163540 +@node Old News for 3.0Old News for 3.04389,167642 +@node Old News for 3.1Old News for 3.14459,171336 +@node Old News for 3.2Old News for 3.24485,172508 +@node Old News for 3.3Old News for 3.34546,175511 +@node Old News for 3.4Old News for 3.44565,176408 +@node Function IndexFunction Index4588,177464 +@node Variable IndexVariable Index4592,177540 +@node Keystroke IndexKeystroke Index4596,177620 +@node Concept IndexConcept Index4600,177686 + +doc/PG-adapting.texi,3863 +@node TopTop157,4775 +@node IntroductionIntroduction195,5920 +@node FutureFuture236,7573 +@node CreditsCredits272,9169 +@node Beginning with a New ProverBeginning with a New Prover282,9461 +@node Overview of adding a new proverOverview of adding a new prover323,11410 +@node Demonstration instance and easy configurationDemonstration instance and easy configuration397,14831 +@node Major modes used by Proof GeneralMajor modes used by Proof General466,18222 +@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands539,21305 +@node Settings for generic user-level commandsSettings for generic user-level commands554,21851 +@node Menu configurationMenu configuration599,23587 +@node Toolbar configurationToolbar configuration623,24505 +@node Proof Script SettingsProof Script Settings681,26750 +@node Recognizing commands and commentsRecognizing commands and comments703,27330 +@node Recognizing proofsRecognizing proofs824,32857 +@node Recognizing other elementsRecognizing other elements936,37671 +@node Configuring undo behaviourConfiguring undo behaviour1062,43149 +@node Nested proofsNested proofs1200,48490 +@node Safe (state-preserving) commandsSafe (state-preserving) commands1240,50117 +@node Activate scripting hookActivate scripting hook1263,51063 +@node Automatic multiple filesAutomatic multiple files1287,51927 +@node CompletionsCompletions1309,52774 +@node Proof Shell SettingsProof Shell Settings1349,54252 +@node Proof shell commandsProof shell commands1380,55534 +@node Script input to the shellScript input to the shell1543,62409 +@node Settings for matching various output from proof processSettings for matching various output from proof process1610,65452 +@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process1741,71216 +@node Hooks and other settingsHooks and other settings1951,80769 +@node Goals Buffer SettingsGoals Buffer Settings2047,84602 +@node Splash Screen SettingsSplash Screen Settings2124,87710 +@node Global ConstantsGlobal Constants2150,88468 +@node Handling Multiple FilesHandling Multiple Files2176,89317 +@node Configuring Editing SyntaxConfiguring Editing Syntax2328,97101 +@node Configuring Font LockConfiguring Font Lock2385,99218 +@node Configuring X-SymbolConfiguring X-Symbol2472,103461 +@node Writing More Lisp CodeWriting More Lisp Code2532,105984 +@node Default values for generic settingsDefault values for generic settings2549,106629 +@node Adding prover-specific configurationsAdding prover-specific configurations2579,107712 +@node Useful variablesUseful variables2622,108982 +@node Useful functions and macrosUseful functions and macros2648,109776 +@node Internals of Proof GeneralInternals of Proof General2750,113653 +@node SpansSpans2778,114561 +@node Proof General site configurationProof General site configuration2791,114935 +@node Configuration variable mechanismsConfiguration variable mechanisms2871,118079 +@node Global variablesGlobal variables2989,123315 +@node Proof script modeProof script mode3059,125865 +@node Proof shell modeProof shell mode3318,137520 +@node DebuggingDebugging3724,153567 +@node Plans and IdeasPlans and Ideas3767,154462 +@node Proof by pointing and similar featuresProof by pointing and similar features3788,155184 +@node Granularity of atomic command sequencesGranularity of atomic command sequences3826,156842 +@node Browser mode for script files and theoriesBrowser mode for script files and theories3871,159067 +@node Demonstration InstantiationsDemonstration Instantiations3901,160098 +@node demoisa-easy.eldemoisa-easy.el3917,160529 +@node demoisa.eldemoisa.el3980,162767 +@node Function IndexFunction Index4148,168283 +@node Variable IndexVariable Index4152,168359 +@node Concept IndexConcept Index4161,168538 |