diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2009-09-15 08:40:12 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2009-09-15 08:40:12 +0000 |
commit | 5286b54dcbbda5715a59a7fc50cdfb9872706950 (patch) | |
tree | a830ea13cbed19d7312748b43ce6f194354377ec | |
parent | 815cadebd99cd25dc78be6e2ba3af177c4140ebd (diff) |
Updated
-rw-r--r-- | TAGS | 2572 |
1 files changed, 1302 insertions, 1270 deletions
@@ -37,146 +37,146 @@ coq/coq-db.el,600 (defconst coq-solve-tactics-face 236,8599 coq/coq.el,5449 -(defcustom coq-translate-to-v8 48,1389 -(defun coq-build-prog-args 54,1569 -(defcustom coq-compile-file-command 64,1865 -(defcustom coq-use-makefile 72,2184 -(defcustom coq-default-undo-limit 80,2407 -(defconst coq-shell-init-cmd85,2535 -(defcustom coq-prog-env 91,2662 -(defconst coq-shell-restart-cmd 99,2912 -(defvar coq-shell-prompt-pattern101,2966 -(defvar coq-shell-cd 109,3270 -(defvar coq-shell-proof-completed-regexp 113,3430 -(defvar coq-goal-regexp116,3582 -(defun coq-library-directory 123,3696 -(defcustom coq-tags 130,3875 -(defconst coq-interrupt-regexp 135,4025 -(defcustom coq-www-home-page 140,4146 -(defvar coq-outline-regexp147,4314 -(defvar coq-outline-heading-end-regexp 154,4526 -(defvar coq-shell-outline-regexp 156,4580 -(defvar coq-shell-outline-heading-end-regexp 157,4630 -(defconst coq-state-preserving-tactics-regexp163,4795 -(defconst coq-state-changing-commands-regexp165,4895 -(defconst coq-state-preserving-commands-regexp167,5002 -(defconst coq-commands-regexp169,5113 -(defvar coq-retractable-instruct-regexp171,5190 -(defvar coq-non-retractable-instruct-regexp173,5280 -(defun coq-set-undo-limit 207,6151 -(defun build-list-id-from-string 211,6281 -(defun coq-last-prompt-info 223,6779 -(defun coq-last-prompt-info-safe 235,7311 -(defvar coq-last-but-one-statenum 241,7568 -(defvar coq-last-but-one-proofnum 247,7865 -(defvar coq-last-but-one-proofstack 250,7963 -(defun coq-get-span-statenum 253,8073 -(defun coq-get-span-proofnum 258,8188 -(defun coq-get-span-proofstack 263,8303 -(defun coq-set-span-statenum 268,8447 -(defun coq-get-span-goalcmd 273,8578 -(defun coq-set-span-goalcmd 278,8692 -(defun coq-set-span-proofnum 283,8822 -(defun coq-set-span-proofstack 288,8953 -(defun proof-last-locked-span 293,9113 -(defun coq-set-state-infos 308,9716 -(defun count-not-intersection 347,11711 -(defun coq-find-and-forget 378,12961 -(defvar coq-current-goal 397,13848 -(defun coq-goal-hyp 400,13913 -(defun coq-state-preserving-p 413,14345 -(defconst notation-print-kinds-table427,14846 -(defun coq-PrintScope 431,15013 -(defun coq-guess-or-ask-for-string 449,15562 -(defun coq-ask-do 463,16130 -(defun coq-SearchIsos 472,16515 -(defun coq-SearchConstant 478,16748 -(defun coq-SearchRewrite 482,16841 -(defun coq-SearchAbout 486,16939 -(defun coq-Print 490,17031 -(defun coq-About 494,17153 -(defun coq-LocateConstant 498,17270 -(defun coq-LocateLibrary 504,17405 -(defun coq-addquotes 510,17555 -(defun coq-LocateNotation 512,17603 -(defun coq-Pwd 519,17801 -(defun coq-Inspect 525,17933 -(defun coq-PrintSection(529,18033 -(defun coq-Print-implicit 533,18126 -(defun coq-Check 538,18277 -(defun coq-Show 543,18385 -(defun coq-Compile 557,18828 -(defun coq-guess-command-line 569,19146 -(defpacustom use-editing-holes 608,20818 -(defun coq-mode-config 618,21155 -(defun coq-shell-mode-config 722,25039 -(defun coq-goals-mode-config 765,26838 -(defun coq-response-config 772,27082 -(defpacustom print-fully-explicit 797,27907 -(defpacustom print-implicit 802,28055 -(defpacustom print-coercions 807,28221 -(defpacustom print-match-wildcards 812,28365 -(defpacustom print-elim-types 817,28545 -(defpacustom printing-depth 822,28711 -(defpacustom undo-depth 827,28872 -(defpacustom time-commands 832,29019 -(defpacustom undo-limit 836,29129 -(defpacustom auto-compile-vos 841,29231 -(defun coq-maybe-compile-buffer 870,30345 -(defun coq-ancestors-of 906,31873 -(defun coq-all-ancestors-of 929,32837 -(defun coq-process-require-command 940,33184 -(defun coq-included-children 945,33311 -(defun coq-process-file 966,34150 -(defun coq-preprocessing 981,34689 -(defun coq-fake-constant-markup 994,35096 -(defun coq-create-span-menu 1010,35701 -(defconst module-kinds-table1027,36196 -(defconst modtype-kinds-table1031,36345 -(defun coq-insert-section-or-module 1035,36474 -(defconst reqkinds-kinds-table1058,37332 -(defun coq-insert-requires 1063,37477 -(defun coq-end-Section 1079,37980 -(defun coq-insert-intros 1097,38558 -(defun coq-insert-infoH-hook 1110,39090 -(defun coq-insert-as 1115,39242 -(defun coq-insert-match 1133,39985 -(defun coq-insert-tactic 1165,41167 -(defun coq-insert-tactical 1171,41406 -(defun coq-insert-command 1177,41655 -(defun coq-insert-term 1183,41899 -(define-key coq-keymap 1189,42096 -(define-key coq-keymap 1190,42154 -(define-key coq-keymap 1191,42211 -(define-key coq-keymap 1192,42280 -(define-key coq-keymap 1193,42336 -(define-key coq-keymap 1194,42385 -(define-key coq-keymap 1195,42443 -(define-key coq-keymap 1197,42504 -(define-key coq-keymap 1198,42563 -(define-key coq-keymap 1200,42627 -(define-key coq-keymap 1201,42687 -(define-key coq-keymap 1203,42743 -(define-key coq-keymap 1204,42793 -(define-key coq-keymap 1205,42843 -(define-key coq-keymap 1206,42893 -(define-key coq-keymap 1207,42947 -(define-key coq-keymap 1208,43006 -(defvar last-coq-error-location 1216,43137 -(defun coq-get-last-error-location 1225,43536 -(defun coq-highlight-error 1272,45874 -(defvar coq-allow-highlight-error 1307,47161 -(defun coq-decide-highlight-error 1314,47488 -(defun coq-highlight-error-hook 1318,47610 -(defun first-word-of-buffer 1329,48003 -(defun coq-show-first-goal 1337,48206 -(defvar coq-modeline-string2 1354,48901 -(defvar coq-modeline-string1 1355,48945 -(defvar coq-modeline-string0 1356,48988 -(defun coq-build-subgoals-string 1357,49033 -(defun coq-update-minor-mode-alist 1362,49199 -(defun is-not-split-vertic 1388,50270 -(defun optim-resp-windows 1397,50709 +(defcustom coq-translate-to-v8 47,1330 +(defun coq-build-prog-args 53,1510 +(defcustom coq-compile-file-command 63,1806 +(defcustom coq-use-makefile 71,2125 +(defcustom coq-default-undo-limit 79,2348 +(defconst coq-shell-init-cmd84,2476 +(defcustom coq-prog-env 90,2603 +(defconst coq-shell-restart-cmd 98,2853 +(defvar coq-shell-prompt-pattern100,2907 +(defvar coq-shell-cd 108,3211 +(defvar coq-shell-proof-completed-regexp 112,3371 +(defvar coq-goal-regexp115,3523 +(defun coq-library-directory 122,3637 +(defcustom coq-tags 129,3816 +(defconst coq-interrupt-regexp 134,3966 +(defcustom coq-www-home-page 139,4087 +(defvar coq-outline-regexp146,4255 +(defvar coq-outline-heading-end-regexp 153,4467 +(defvar coq-shell-outline-regexp 155,4521 +(defvar coq-shell-outline-heading-end-regexp 156,4571 +(defconst coq-state-preserving-tactics-regexp162,4736 +(defconst coq-state-changing-commands-regexp164,4836 +(defconst coq-state-preserving-commands-regexp166,4943 +(defconst coq-commands-regexp168,5054 +(defvar coq-retractable-instruct-regexp170,5131 +(defvar coq-non-retractable-instruct-regexp172,5221 +(defun coq-set-undo-limit 206,6098 +(defun build-list-id-from-string 210,6228 +(defun coq-last-prompt-info 222,6726 +(defun coq-last-prompt-info-safe 234,7258 +(defvar coq-last-but-one-statenum 240,7515 +(defvar coq-last-but-one-proofnum 246,7812 +(defvar coq-last-but-one-proofstack 249,7910 +(defun coq-get-span-statenum 252,8020 +(defun coq-get-span-proofnum 257,8135 +(defun coq-get-span-proofstack 262,8250 +(defun coq-set-span-statenum 267,8394 +(defun coq-get-span-goalcmd 272,8525 +(defun coq-set-span-goalcmd 277,8639 +(defun coq-set-span-proofnum 282,8769 +(defun coq-set-span-proofstack 287,8900 +(defun proof-last-locked-span 292,9060 +(defun coq-set-state-infos 307,9663 +(defun count-not-intersection 346,11658 +(defun coq-find-and-forget 377,12908 +(defvar coq-current-goal 396,13795 +(defun coq-goal-hyp 399,13860 +(defun coq-state-preserving-p 412,14292 +(defconst notation-print-kinds-table426,14793 +(defun coq-PrintScope 430,14960 +(defun coq-guess-or-ask-for-string 448,15509 +(defun coq-ask-do 462,16077 +(defun coq-SearchIsos 471,16462 +(defun coq-SearchConstant 477,16695 +(defun coq-SearchRewrite 481,16788 +(defun coq-SearchAbout 485,16886 +(defun coq-Print 489,16978 +(defun coq-About 493,17100 +(defun coq-LocateConstant 497,17217 +(defun coq-LocateLibrary 503,17352 +(defun coq-addquotes 509,17502 +(defun coq-LocateNotation 511,17550 +(defun coq-Pwd 518,17748 +(defun coq-Inspect 524,17880 +(defun coq-PrintSection(528,17980 +(defun coq-Print-implicit 532,18073 +(defun coq-Check 537,18224 +(defun coq-Show 542,18332 +(defun coq-Compile 556,18775 +(defun coq-guess-command-line 568,19093 +(defpacustom use-editing-holes 607,20765 +(defun coq-mode-config 617,21102 +(defun coq-shell-mode-config 721,24986 +(defun coq-goals-mode-config 764,26785 +(defun coq-response-config 771,27029 +(defpacustom print-fully-explicit 796,27854 +(defpacustom print-implicit 801,28002 +(defpacustom print-coercions 806,28168 +(defpacustom print-match-wildcards 811,28312 +(defpacustom print-elim-types 816,28492 +(defpacustom printing-depth 821,28658 +(defpacustom undo-depth 826,28819 +(defpacustom time-commands 831,28966 +(defpacustom undo-limit 835,29076 +(defpacustom auto-compile-vos 840,29178 +(defun coq-maybe-compile-buffer 869,30292 +(defun coq-ancestors-of 905,31820 +(defun coq-all-ancestors-of 928,32784 +(defun coq-process-require-command 939,33131 +(defun coq-included-children 944,33258 +(defun coq-process-file 965,34097 +(defun coq-preprocessing 980,34636 +(defun coq-fake-constant-markup 994,35071 +(defun coq-create-span-menu 1010,35676 +(defconst module-kinds-table1027,36171 +(defconst modtype-kinds-table1031,36320 +(defun coq-insert-section-or-module 1035,36449 +(defconst reqkinds-kinds-table1058,37307 +(defun coq-insert-requires 1063,37452 +(defun coq-end-Section 1079,37955 +(defun coq-insert-intros 1097,38533 +(defun coq-insert-infoH-hook 1110,39065 +(defun coq-insert-as 1115,39273 +(defun coq-insert-match 1132,39976 +(defun coq-insert-tactic 1164,41158 +(defun coq-insert-tactical 1170,41397 +(defun coq-insert-command 1176,41646 +(defun coq-insert-term 1182,41890 +(define-key coq-keymap 1188,42087 +(define-key coq-keymap 1189,42145 +(define-key coq-keymap 1190,42202 +(define-key coq-keymap 1191,42271 +(define-key coq-keymap 1192,42327 +(define-key coq-keymap 1193,42376 +(define-key coq-keymap 1194,42434 +(define-key coq-keymap 1196,42495 +(define-key coq-keymap 1197,42554 +(define-key coq-keymap 1199,42618 +(define-key coq-keymap 1200,42678 +(define-key coq-keymap 1202,42734 +(define-key coq-keymap 1203,42784 +(define-key coq-keymap 1204,42834 +(define-key coq-keymap 1205,42884 +(define-key coq-keymap 1206,42938 +(define-key coq-keymap 1207,42997 +(defvar last-coq-error-location 1215,43128 +(defun coq-get-last-error-location 1224,43527 +(defun coq-highlight-error 1272,45907 +(defvar coq-allow-highlight-error 1306,47157 +(defun coq-decide-highlight-error 1313,47483 +(defun coq-highlight-error-hook 1318,47668 +(defun first-word-of-buffer 1329,48061 +(defun coq-show-first-goal 1337,48264 +(defvar coq-modeline-string2 1354,48959 +(defvar coq-modeline-string1 1355,49003 +(defvar coq-modeline-string0 1356,49046 +(defun coq-build-subgoals-string 1357,49091 +(defun coq-update-minor-mode-alist 1362,49257 +(defun is-not-split-vertic 1388,50328 +(defun optim-resp-windows 1397,50767 coq/coq-indent.el,2223 (defconst coq-any-command-regexp20,368 @@ -232,13 +232,13 @@ coq/coq-indent.el,2223 (defun coq-indent-region 722,28820 coq/coq-local-vars.el,280 -(defconst coq-local-vars-doc 18,369 -(defun coq-insert-coq-prog-name 76,2897 -(defun coq-read-directory 87,3370 -(defun coq-extract-directories-from-args 111,4473 -(defun coq-ask-prog-args 126,5025 -(defun coq-ask-prog-name 148,6089 -(defun coq-ask-insert-coq-prog-name 166,6844 +(defconst coq-local-vars-doc 20,429 +(defun coq-insert-coq-prog-name 78,2957 +(defun coq-read-directory 89,3430 +(defun coq-extract-directories-from-args 113,4533 +(defun coq-ask-prog-args 128,5085 +(defun coq-ask-prog-name 150,6149 +(defun coq-ask-insert-coq-prog-name 168,6904 coq/coq-syntax.el,2428 (defcustom coq-prog-name 18,558 @@ -317,14 +317,14 @@ coq/coq-unicode-tokens.el,454 (defconst coq-control-regions249,6553 demoisa/demoisa.el,349 -(defcustom isabelledemo-prog-name 54,1805 -(defcustom isabelledemo-web-page59,1927 -(defun demoisa-config 70,2157 -(defun demoisa-shell-config 91,2949 -(define-derived-mode demoisa-mode 116,3878 -(define-derived-mode demoisa-shell-mode 121,4001 -(define-derived-mode demoisa-response-mode 126,4144 -(define-derived-mode demoisa-goals-mode 130,4271 +(defcustom isabelledemo-prog-name 56,1848 +(defcustom isabelledemo-web-page61,1970 +(defun demoisa-config 72,2200 +(defun demoisa-shell-config 93,2992 +(define-derived-mode demoisa-mode 118,3921 +(define-derived-mode demoisa-shell-mode 123,4044 +(define-derived-mode demoisa-response-mode 128,4187 +(define-derived-mode demoisa-goals-mode 132,4314 hol98/hol98.el,121 (defvar hol98-keywords 17,419 @@ -333,95 +333,95 @@ hol98/hol98.el,121 (defvar hol98-tacticals 20,499 isar/isabelle-system.el,1291 -(defgroup isabelle 26,776 -(defcustom isabelle-web-page30,904 -(defcustom isa-isabelle-command39,1121 -(defvar isabelle-not-found 57,1803 -(defun isa-set-isabelle-command 60,1918 -(defun isa-shell-command-to-string 83,2936 -(defun isa-getenv 89,3160 -(defcustom isabelle-program-name-override 109,3852 -(defvar isabelle-prog-name 120,4198 -(defun isa-tool-list-logics 123,4308 -(defcustom isabelle-logics-available 130,4547 -(defcustom isabelle-chosen-logic 140,4884 -(defvar isabelle-chosen-logic-prev 156,5468 -(defun isabelle-hack-local-variables-function 159,5588 -(defun isabelle-set-prog-name 171,6027 -(defun isabelle-choose-logic 196,7217 -(defun isa-view-doc 215,7979 -(defun isa-tool-list-docs 224,8244 -(defconst isabelle-verbatim-regexp 242,8967 -(defun isabelle-verbatim 245,9109 -(defcustom isabelle-refresh-logics 252,9270 -(defvar isabelle-docs-menu260,9598 -(defvar isabelle-logics-menu-entries 267,9883 -(defun isabelle-logics-menu-calculate 270,9956 -(defvar isabelle-time-to-refresh-logics 291,10598 -(defun isabelle-logics-menu-refresh 295,10693 -(defun isabelle-menu-bar-update-logics 310,11326 -(defun isabelle-load-isar-keywords 326,11955 -(defun isabelle-create-span-menu 347,12683 -(defun isabelle-xml-sml-escapes 363,13125 -(defun isabelle-process-pgip 366,13226 - -isar/isar.el,1610 -(defcustom isar-keywords-name 37,884 -(defpgdefault completion-table 54,1402 -(defcustom isar-web-page56,1455 -(defun isar-strip-terminators 70,1805 -(defun isar-markup-ml 83,2182 -(defun isar-mode-config-set-variables 88,2317 -(defun isar-shell-mode-config-set-variables 159,5303 -(defpacustom use-find-theorems-form 240,8437 -(defun isar-set-proof-find-theorems-command 245,8603 -(defpacustom use-linear-undo 251,8787 -(defun isar-set-undo-commands 255,8912 -(defun isar-configure-from-settings 266,9355 -(defun isar-remove-file 274,9502 -(defun isar-shell-compute-new-files-list 284,9857 -(define-derived-mode isar-shell-mode 302,10429 -(define-derived-mode isar-response-mode 307,10552 -(define-derived-mode isar-goals-mode 312,10680 -(define-derived-mode isar-mode 317,10801 -(defpgdefault menu-entries374,12823 -(defalias 'isar-set-command isar-set-command404,13980 -(defpgdefault help-menu-entries 406,14036 -(defun isar-count-undos 409,14112 -(defun isar-find-and-forget 435,15087 -(defun isar-goal-command-p 475,16614 -(defun isar-global-save-command-p 480,16791 -(defvar isar-current-goal 501,17575 -(defun isar-state-preserving-p 504,17641 -(defvar isar-shell-current-line-width 529,18838 -(defun isar-shell-adjust-line-width 534,19030 -(defun isar-string-wrapping 558,19801 -(defun isar-positions-of 567,19998 -(defun isar-command-wrapping 591,20702 -(defcustom isar-wrap-commands-singly 600,21046 -(defun isar-preprocessing 606,21242 -(defun isar-mode-config 625,21869 -(defun isar-shell-mode-config 636,22427 -(defun isar-response-mode-config 646,22776 -(defun isar-goals-mode-config 656,23111 - -isar/isar-find-theorems.el,778 -(defun isar-find-theorems-minibuffer 18,713 -(defun isar-find-theorems-form 32,1332 -(defvar isar-find-theorems-data 74,3132 -(defvar isar-find-theorems-widget-number 88,3467 -(defvar isar-find-theorems-widget-pattern 91,3565 -(defvar isar-find-theorems-widget-intro 94,3657 -(defvar isar-find-theorems-widget-elim 97,3743 -(defvar isar-find-theorems-widget-dest 100,3827 -(defvar isar-find-theorems-widget-name 103,3911 -(defvar isar-find-theorems-widget-simp 106,3998 -(defun isar-find-theorems-create-searchform111,4144 -(defun isar-find-theorems-create-help 251,8687 -(defun isar-find-theorems-submit-searchform294,10859 -(defun isar-find-theorems-parse-criteria 372,13229 -(defun isar-find-theorems-parse-number 465,16210 -(defun isar-find-theorems-filter-empty 475,16487 +(defgroup isabelle 26,716 +(defcustom isabelle-web-page30,844 +(defcustom isa-isabelle-command39,1061 +(defvar isabelle-not-found 57,1743 +(defun isa-set-isabelle-command 60,1858 +(defun isa-shell-command-to-string 83,2876 +(defun isa-getenv 89,3100 +(defcustom isabelle-program-name-override 109,3792 +(defvar isabelle-prog-name 120,4138 +(defun isa-tool-list-logics 123,4248 +(defcustom isabelle-logics-available 130,4487 +(defcustom isabelle-chosen-logic 140,4824 +(defvar isabelle-chosen-logic-prev 156,5408 +(defun isabelle-hack-local-variables-function 159,5528 +(defun isabelle-set-prog-name 171,5967 +(defun isabelle-choose-logic 196,7157 +(defun isa-view-doc 215,7919 +(defun isa-tool-list-docs 224,8184 +(defconst isabelle-verbatim-regexp 242,8907 +(defun isabelle-verbatim 245,9049 +(defcustom isabelle-refresh-logics 252,9210 +(defvar isabelle-docs-menu260,9538 +(defvar isabelle-logics-menu-entries 267,9823 +(defun isabelle-logics-menu-calculate 270,9896 +(defvar isabelle-time-to-refresh-logics 291,10538 +(defun isabelle-logics-menu-refresh 295,10633 +(defun isabelle-menu-bar-update-logics 310,11266 +(defun isabelle-load-isar-keywords 326,11895 +(defun isabelle-create-span-menu 347,12623 +(defun isabelle-xml-sml-escapes 363,13065 +(defun isabelle-process-pgip 366,13166 + +isar/isar.el,1616 +(defcustom isar-keywords-name 39,915 +(defpgdefault completion-table 56,1433 +(defcustom isar-web-page58,1486 +(defun isar-strip-terminators 72,1836 +(defun isar-markup-ml 85,2213 +(defun isar-mode-config-set-variables 90,2348 +(defun isar-shell-mode-config-set-variables 162,5389 +(defun isar-set-proof-find-theorems-command 243,8523 +(defpacustom use-find-theorems-form 249,8707 +(defun isar-set-undo-commands 254,8873 +(defpacustom use-linear-undo 265,9324 +(defun isar-configure-from-settings 270,9482 +(defun isar-remove-file 278,9629 +(defun isar-shell-compute-new-files-list 288,9984 +(define-derived-mode isar-shell-mode 307,10564 +(define-derived-mode isar-response-mode 312,10691 +(define-derived-mode isar-goals-mode 317,10824 +(define-derived-mode isar-mode 322,10950 +(defpgdefault menu-entries379,12965 +(defalias 'isar-set-command isar-set-command409,14122 +(defpgdefault help-menu-entries 411,14178 +(defun isar-count-undos 414,14254 +(defun isar-find-and-forget 440,15229 +(defun isar-goal-command-p 480,16756 +(defun isar-global-save-command-p 485,16933 +(defvar isar-current-goal 506,17717 +(defun isar-state-preserving-p 509,17783 +(defvar isar-shell-current-line-width 534,18980 +(defun isar-shell-adjust-line-width 539,19172 +(defsubst isar-string-wrapping 564,19970 +(defsubst isar-positions-of 573,20164 +(defcustom isar-wrap-commands-singly 579,20369 +(defun isar-command-wrapping 585,20565 +(defun isar-preprocessing 593,20879 +(defun isar-mode-config 611,21430 +(defun isar-shell-mode-config 625,22083 +(defun isar-response-mode-config 635,22432 +(defun isar-goals-mode-config 645,22767 + +isar/isar-find-theorems.el,779 +(defvar isar-find-theorems-data 19,565 +(defun isar-find-theorems-minibuffer 35,1039 +(defun isar-find-theorems-form 49,1658 +(defvar isar-find-theorems-widget-number 92,3532 +(defvar isar-find-theorems-widget-pattern 95,3630 +(defvar isar-find-theorems-widget-intro 98,3722 +(defvar isar-find-theorems-widget-elim 101,3808 +(defvar isar-find-theorems-widget-dest 104,3892 +(defvar isar-find-theorems-widget-name 107,3976 +(defvar isar-find-theorems-widget-simp 110,4063 +(defun isar-find-theorems-create-searchform115,4209 +(defun isar-find-theorems-create-help 255,8752 +(defun isar-find-theorems-submit-searchform298,10924 +(defun isar-find-theorems-parse-criteria 376,13294 +(defun isar-find-theorems-parse-number 469,16275 +(defun isar-find-theorems-filter-empty 479,16552 isar/isar-keywords.el,1052 (defconst isar-keywords-major13,481 @@ -453,7 +453,7 @@ isar/isar-mmm.el,81 (defconst isar-start-latex-regexp24,744 (defconst isar-start-sml-regexp36,1172 -isar/isar-syntax.el,3703 +isar/isar-syntax.el,3799 (defconst isar-script-syntax-table-entries18,424 (defconst isar-script-syntax-table-alist42,826 (defun isar-init-syntax-table 51,1109 @@ -469,127 +469,129 @@ isar/isar-syntax.el,3703 (defconst isar-keywords-local-goal110,2705 (defconst isar-keywords-proper114,2810 (defconst isar-keywords-improper119,2929 -(defconst isar-keywords-outline124,3061 -(defconst isar-keywords-fume127,3126 -(defconst isar-keywords-indent-open134,3316 -(defconst isar-keywords-indent-close140,3479 -(defconst isar-keywords-indent-enclose144,3577 -(defun isar-regexp-simple-alt 153,3771 -(defun isar-ids-to-regexp 173,4531 -(defconst isar-ext-first 207,5916 -(defconst isar-ext-rest 208,5983 -(defconst isar-long-id-stuff 210,6055 -(defconst isar-id 211,6129 -(defconst isar-idx 212,6199 -(defconst isar-string 214,6258 -(defconst isar-any-command-regexp216,6318 -(defconst isar-name-regexp220,6452 -(defconst isar-improper-regexp226,6747 -(defconst isar-save-command-regexp230,6895 -(defconst isar-global-save-command-regexp233,6996 -(defconst isar-goal-command-regexp236,7110 -(defconst isar-local-goal-command-regexp239,7218 -(defconst isar-comment-start 242,7331 -(defconst isar-comment-end 243,7366 -(defconst isar-comment-start-regexp 244,7399 -(defconst isar-comment-end-regexp 245,7470 -(defconst isar-string-start-regexp 247,7538 -(defconst isar-string-end-regexp 248,7590 -(defun isar-syntactic-context 250,7641 -(defconst isar-antiq-regexp265,8036 -(defconst isar-nesting-regexp271,8187 -(defun isar-nesting 274,8285 -(defun isar-match-nesting 286,8678 -(defface isabelle-class-name-face298,9009 -(defface isabelle-tfree-name-face306,9192 -(defface isabelle-tvar-name-face314,9381 -(defface isabelle-free-name-face322,9569 -(defface isabelle-bound-name-face330,9753 -(defface isabelle-var-name-face338,9940 -(defconst isabelle-class-name-face 346,10127 -(defconst isabelle-tfree-name-face 347,10189 -(defconst isabelle-tvar-name-face 348,10251 -(defconst isabelle-free-name-face 349,10312 -(defconst isabelle-bound-name-face 350,10373 -(defconst isabelle-var-name-face 351,10435 -(defvar isar-font-lock-keywords-1354,10497 -(defun isar-output-flkprops 372,11505 -(defun isar-output-flk 378,11757 -(defvar isar-output-font-lock-keywords-1381,11866 -(defun isar-strip-output-markup 417,13289 -(defconst isar-shell-font-lock-keywords421,13425 -(defvar isar-goals-font-lock-keywords424,13509 -(defconst isar-linear-undo 458,14188 -(defconst isar-undo 460,14231 -(defun isar-remove 462,14274 -(defun isar-undos 465,14349 -(defun isar-cannot-undo 470,14510 -(defconst isar-undo-commands473,14580 -(defconst isar-theory-start-regexp481,14717 -(defconst isar-end-regexp487,14875 -(defconst isar-undo-fail-regexp491,14976 -(defconst isar-undo-skip-regexp495,15080 -(defconst isar-undo-ignore-regexp498,15201 -(defconst isar-undo-remove-regexp501,15266 -(defconst isar-any-entity-regexp509,15441 -(defconst isar-named-entity-regexp514,15614 -(defconst isar-unnamed-entity-regexp519,15777 -(defconst isar-next-entity-regexps522,15879 -(defconst isar-generic-expression530,16183 -(defconst isar-indent-any-regexp541,16416 -(defconst isar-indent-inner-regexp543,16509 -(defconst isar-indent-enclose-regexp545,16575 -(defconst isar-indent-open-regexp547,16691 -(defconst isar-indent-close-regexp549,16801 -(defconst isar-outline-regexp555,16938 -(defconst isar-outline-heading-end-regexp 559,17091 +(defconst isar-keyword-level-alist124,3061 +(defconst isar-keywords-outline 139,3532 +(defconst isar-keywords-fume142,3608 +(defconst isar-keywords-indent-open149,3798 +(defconst isar-keywords-indent-close155,3961 +(defconst isar-keywords-indent-enclose159,4059 +(defun isar-regexp-simple-alt 168,4253 +(defun isar-ids-to-regexp 188,5013 +(defconst isar-ext-first 222,6398 +(defconst isar-ext-rest 223,6465 +(defconst isar-long-id-stuff 225,6537 +(defconst isar-id 226,6611 +(defconst isar-idx 227,6681 +(defconst isar-string 229,6740 +(defconst isar-any-command-regexp231,6800 +(defconst isar-name-regexp235,6934 +(defconst isar-improper-regexp241,7229 +(defconst isar-save-command-regexp245,7377 +(defconst isar-global-save-command-regexp248,7478 +(defconst isar-goal-command-regexp251,7592 +(defconst isar-local-goal-command-regexp254,7700 +(defconst isar-comment-start 257,7813 +(defconst isar-comment-end 258,7848 +(defconst isar-comment-start-regexp 259,7881 +(defconst isar-comment-end-regexp 260,7952 +(defconst isar-string-start-regexp 262,8020 +(defconst isar-string-end-regexp 263,8072 +(defun isar-syntactic-context 265,8123 +(defconst isar-antiq-regexp280,8518 +(defconst isar-nesting-regexp286,8669 +(defun isar-nesting 289,8767 +(defun isar-match-nesting 301,9160 +(defface isabelle-class-name-face313,9491 +(defface isabelle-tfree-name-face321,9674 +(defface isabelle-tvar-name-face329,9863 +(defface isabelle-free-name-face337,10051 +(defface isabelle-bound-name-face345,10235 +(defface isabelle-var-name-face353,10422 +(defconst isabelle-class-name-face 361,10609 +(defconst isabelle-tfree-name-face 362,10671 +(defconst isabelle-tvar-name-face 363,10733 +(defconst isabelle-free-name-face 364,10794 +(defconst isabelle-bound-name-face 365,10855 +(defconst isabelle-var-name-face 366,10917 +(defvar isar-font-lock-keywords-1369,10979 +(defun isar-output-flkprops 387,11987 +(defun isar-output-flk 393,12239 +(defvar isar-output-font-lock-keywords-1396,12348 +(defun isar-strip-output-markup 432,13771 +(defconst isar-shell-font-lock-keywords436,13907 +(defvar isar-goals-font-lock-keywords439,13991 +(defconst isar-linear-undo 473,14670 +(defconst isar-undo 475,14713 +(defun isar-remove 477,14756 +(defun isar-undos 480,14831 +(defun isar-cannot-undo 485,14992 +(defconst isar-undo-commands488,15062 +(defconst isar-theory-start-regexp496,15199 +(defconst isar-end-regexp502,15357 +(defconst isar-undo-fail-regexp506,15458 +(defconst isar-undo-skip-regexp510,15562 +(defconst isar-undo-ignore-regexp513,15683 +(defconst isar-undo-remove-regexp516,15748 +(defconst isar-any-entity-regexp524,15923 +(defconst isar-named-entity-regexp529,16096 +(defconst isar-unnamed-entity-regexp534,16259 +(defconst isar-next-entity-regexps537,16361 +(defconst isar-generic-expression545,16665 +(defconst isar-indent-any-regexp556,16898 +(defconst isar-indent-inner-regexp558,16991 +(defconst isar-indent-enclose-regexp560,17057 +(defconst isar-indent-open-regexp562,17173 +(defconst isar-indent-close-regexp564,17283 +(defconst isar-outline-regexp570,17420 +(defconst isar-outline-heading-end-regexp 574,17573 +(defconst isar-outline-heading-alist 576,17622 isar/isar-unicode-tokens.el,1289 -(defgroup isabelle-tokens 26,636 -(defun isar-set-and-restart-tokens 31,776 -(defconst isar-control-region-format-regexp44,1129 -(defconst isar-control-char-format-regexp47,1223 -(defconst isar-control-char-format 50,1318 -(defconst isar-control-region-format-start 51,1367 -(defconst isar-control-region-format-end 52,1421 -(defcustom isar-control-characters55,1477 -(defcustom isar-control-regions68,1849 -(defconst isar-token-format 92,2565 -(defconst isar-token-variant-format-regexp96,2716 -(defcustom isar-greek-letters-tokens99,2830 -(defcustom isar-misc-letters-tokens139,3688 -(defcustom isar-symbols-tokens151,4006 -(defcustom isar-extended-symbols-tokens357,8817 -(defun isar-try-char 426,10472 -(defcustom isar-symbols-tokens-fallbacks430,10616 -(defcustom isar-bold-nums-tokens457,11546 -(defun isar-map-letters 473,11935 -(defconst isar-script-letters-tokens479,12083 -(defconst isar-roman-letters-tokens484,12221 -(defconst isar-fraktur-letters-tokens489,12357 -(defcustom isar-token-symbol-map 494,12499 -(defcustom isar-user-tokens 510,12968 -(defun isar-init-token-symbol-map 517,13205 -(defcustom isar-symbol-shortcuts540,13760 -(defcustom isar-shortcut-alist 613,15986 -(defun isar-init-shortcut-alists 621,16245 -(defconst isar-tokens-customizable-variables642,16908 +(defgroup isabelle-tokens 25,672 +(defun isar-set-and-restart-tokens 30,812 +(defconst isar-control-region-format-regexp43,1165 +(defconst isar-control-char-format-regexp46,1259 +(defconst isar-control-char-format 49,1354 +(defconst isar-control-region-format-start 50,1403 +(defconst isar-control-region-format-end 51,1457 +(defcustom isar-control-characters54,1513 +(defcustom isar-control-regions67,1885 +(defconst isar-token-format 91,2601 +(defconst isar-token-variant-format-regexp95,2752 +(defcustom isar-greek-letters-tokens98,2866 +(defcustom isar-misc-letters-tokens138,3724 +(defcustom isar-symbols-tokens150,4042 +(defcustom isar-extended-symbols-tokens356,8853 +(defun isar-try-char 425,10508 +(defcustom isar-symbols-tokens-fallbacks429,10652 +(defcustom isar-bold-nums-tokens456,11582 +(defun isar-map-letters 472,11971 +(defconst isar-script-letters-tokens478,12119 +(defconst isar-roman-letters-tokens483,12257 +(defconst isar-fraktur-letters-tokens488,12393 +(defcustom isar-token-symbol-map 493,12535 +(defcustom isar-user-tokens 509,13004 +(defun isar-init-token-symbol-map 516,13241 +(defcustom isar-symbol-shortcuts539,13796 +(defcustom isar-shortcut-alist 612,16023 +(defun isar-init-shortcut-alists 620,16282 +(defconst isar-tokens-customizable-variables641,16945 lclam/lclam.el,524 -(defcustom lclam-prog-name 15,373 -(defcustom lclam-web-page21,521 -(defun lclam-config 32,751 -(defun lclam-shell-config 54,1542 -(define-derived-mode lclam-proofscript-mode 73,2157 -(define-derived-mode lclam-shell-mode 78,2280 -(define-derived-mode lclam-response-mode 83,2414 -(define-derived-mode lclam-goals-mode 87,2537 -(defun lclam-mode 95,2765 -(define-derived-mode thy-mode 132,3611 -(defvar thy-mode-map 135,3709 -(defun thy-add-menus 137,3736 -(defun process-thy-file 176,5217 -(defun update-thy-only 182,5418 +(defcustom lclam-prog-name 18,431 +(defcustom lclam-web-page24,579 +(defun lclam-config 35,809 +(defun lclam-shell-config 57,1600 +(define-derived-mode lclam-proofscript-mode 76,2215 +(define-derived-mode lclam-shell-mode 81,2338 +(define-derived-mode lclam-response-mode 86,2472 +(define-derived-mode lclam-goals-mode 90,2595 +(defun lclam-mode 98,2823 +(define-derived-mode thy-mode 135,3669 +(defvar thy-mode-map 138,3767 +(defun thy-add-menus 140,3794 +(defun process-thy-file 179,5275 +(defun update-thy-only 185,5476 lego/lego.el,1636 (defcustom lego-tags 21,534 @@ -619,19 +621,19 @@ lego/lego.el,1636 (defvar lego-shell-outline-heading-end-regexp 138,4218 (define-derived-mode lego-shell-mode 144,4497 (define-derived-mode lego-mode 151,4658 -(define-derived-mode lego-goals-mode 162,4953 -(defun lego-count-undos 173,5379 -(defun lego-goal-command-p 193,6197 -(defun lego-find-and-forget 198,6368 -(defun lego-goal-hyp 240,8184 -(defun lego-state-preserving-p 249,8381 -(defvar lego-shell-current-line-width 265,9084 -(defun lego-shell-adjust-line-width 273,9391 -(defun lego-mode-config 292,10128 -(defun lego-equal-module-filename 360,12177 -(defun lego-shell-compute-new-files-list 366,12452 -(defun lego-shell-mode-config 376,12835 -(defun lego-goals-mode-config 422,14488 +(define-derived-mode lego-goals-mode 162,4968 +(defun lego-count-undos 173,5394 +(defun lego-goal-command-p 193,6212 +(defun lego-find-and-forget 198,6383 +(defun lego-goal-hyp 240,8199 +(defun lego-state-preserving-p 249,8396 +(defvar lego-shell-current-line-width 265,9099 +(defun lego-shell-adjust-line-width 273,9406 +(defun lego-mode-config 292,10143 +(defun lego-equal-module-filename 360,12192 +(defun lego-shell-compute-new-files-list 366,12467 +(defun lego-shell-mode-config 376,12850 +(defun lego-goals-mode-config 423,14517 lego/lego-syntax.el,600 (defconst lego-keywords-goal 15,358 @@ -651,60 +653,84 @@ lego/lego-syntax.el,600 (defvar lego-font-lock-keywords-199,3660 (defun lego-init-syntax-table 110,4122 -phox/phox.el,597 +phox/phox.el,555 (defcustom phox-prog-name 32,916 -(defcustom phox-sym-lock-enabled 37,1018 -(defcustom phox-web-page43,1127 -(defcustom phox-doc-dir49,1277 -(defcustom phox-lib-dir55,1424 -(defcustom phox-tags-program61,1567 -(defcustom phox-tags-doc67,1746 -(defcustom phox-etags73,1883 -(defpgdefault menu-entries94,2333 -(defun phox-config 108,2526 -(defun phox-shell-config 152,4450 -(define-derived-mode phox-mode 176,5312 -(define-derived-mode phox-shell-mode 192,5775 -(define-derived-mode phox-response-mode 197,5903 -(define-derived-mode phox-goals-mode 207,6264 -(defpgdefault completion-table230,7050 +(defcustom phox-web-page37,1018 +(defcustom phox-doc-dir43,1168 +(defcustom phox-lib-dir49,1315 +(defcustom phox-tags-program55,1458 +(defcustom phox-tags-doc61,1637 +(defcustom phox-etags67,1774 +(defpgdefault menu-entries88,2224 +(defun phox-config 102,2417 +(defun phox-shell-config 146,4341 +(define-derived-mode phox-mode 170,5203 +(define-derived-mode phox-shell-mode 186,5666 +(define-derived-mode phox-response-mode 191,5794 +(define-derived-mode phox-goals-mode 201,6155 +(defpgdefault completion-table224,6941 phox/phox-extraction.el,383 -(defvar phox-prog-orig 17,605 -(defun phox-prog-flags-modify(19,673 -(defun phox-prog-flags-extract(48,1474 -(defun phox-prog-flags-erase(59,1764 -(defun phox-toggle-extraction(67,1960 -(defun phox-compile-theorem(79,2362 -(defun phox-compile-theorem-on-cursor(85,2587 -(defun phox-output 101,3065 -(defun phox-output-theorem 111,3277 -(defun phox-output-theorem-on-cursor(118,3576 - -phox/phox-font.el,123 -(defconst phox-font-lock-keywords6,282 -(defconst phox-sym-lock-keywords-table65,2399 -(defun phox-sym-lock-start 88,2973 - -phox/phox-fun.el,678 -(defun phox-init-syntax-table 67,2384 -(defvar phox-top-keywords83,2856 -(defvar phox-proof-keywords131,3311 -(defun phox-find-and-forget 172,3661 -(defun phox-assert-next-command-interactive 251,6059 -(defun phox-depend-theorem(269,6863 -(defun phox-eshow-extlist(278,7152 -(defun phox-flag-name(292,7749 -(defun phox-path(303,8051 -(defun phox-print-expression(314,8287 -(defun phox-print-sort-expression(327,8743 -(defun phox-priority-symbols-list(338,9055 -(defun phox-search-string(350,9427 -(defun phox-constraints(365,9952 -(defun phox-goals(376,10208 -(defvar phox-state-menu388,10417 -(defun phox-delete-symbol(413,11407 -(defun phox-delete-symbol-on-cursor(419,11615 +(defvar phox-prog-orig 19,619 +(defun phox-prog-flags-modify(21,687 +(defun phox-prog-flags-extract(50,1488 +(defun phox-prog-flags-erase(61,1778 +(defun phox-toggle-extraction(69,1974 +(defun phox-compile-theorem(81,2376 +(defun phox-compile-theorem-on-cursor(87,2601 +(defun phox-output 103,3079 +(defun phox-output-theorem 113,3291 +(defun phox-output-theorem-on-cursor(120,3590 + +phox/phox-font.el,231 +(defvar phox-sym-lock-enabled 1,0 +(defvar phox-sym-lock-color 2,60 +(defvar phox-sym-lock-keywords 3,118 +(defconst phox-font-lock-keywords11,511 +(defconst phox-sym-lock-keywords-table70,2628 +(defun phox-sym-lock-start 93,3202 + +phox/phox-fun.el,1659 +(defconst phox-forget-id-command 11,186 +(defconst phox-forget-proof-command 12,232 +(defconst phox-forget-new-elim-command 13,287 +(defconst phox-forget-new-intro-command 14,345 +(defconst phox-forget-new-equation-command 15,405 +(defconst phox-forget-close-def-command 16,471 +(defconst phox-comments-regexp 18,597 +(defconst phox-strict-comments-regexp 20,776 +(defconst phox-ident-regexp 21,941 +(defconst phox-inductive-option 22,1027 +(defconst phox-spaces-regexp 23,1079 +(defconst phox-sy-definition-regexp 24,1122 +(defconst phox-sy-inductive-regexp 28,1309 +(defconst phox-inductive-regexp 34,1522 +(defconst phox-data-regexp 40,1673 +(defconst phox-definition-regexp 46,1827 +(defconst phox-prove-claim-regexp 50,1971 +(defconst phox-new-elim-regexp 54,2077 +(defconst phox-new-intro-regexp 57,2196 +(defconst phox-new-rewrite-regexp 60,2317 +(defconst phox-new-equation-regexp 63,2442 +(defconst phox-close-def-regexp 66,2569 +(defun phox-init-syntax-table 71,2706 +(defvar phox-top-keywords87,3178 +(defvar phox-proof-keywords135,3633 +(defun phox-find-and-forget 176,3983 +(defalias 'phox-assert-next-command-interactive phox-assert-next-command-interactive255,6381 +(defun phox-depend-theorem(274,7347 +(defun phox-eshow-extlist(283,7636 +(defun phox-flag-name(297,8233 +(defun phox-path(308,8535 +(defun phox-print-expression(319,8771 +(defun phox-print-sort-expression(332,9227 +(defun phox-priority-symbols-list(343,9539 +(defun phox-search-string(355,9911 +(defun phox-constraints(370,10436 +(defun phox-goals(381,10692 +(defvar phox-state-menu393,10901 +(defun phox-delete-symbol(418,11891 +(defun phox-delete-symbol-on-cursor(424,12099 phox/phox-lang.el,323 (defvar phox-lang9,306 @@ -718,64 +744,69 @@ phox/phox-lang.el,323 (defun phox-lang-prove 52,1488 (defun phox-lang-let 57,1622 -phox/phox-outline.el,70 -(defun phox-outline-level(34,1143 -(defun phox-setup-outline 48,1617 - -phox/phox-pbrpm.el,512 -(defun phox-pbrpm-left-paren-p 27,1188 -(defun phox-pbrpm-right-paren-p 34,1391 -(defun phox-pbrpm-menu-from-string 42,1595 -(defun phox-pbrpm-rename-in-cmd 51,1927 -(defun phox-pbrpm-get-region-name 84,3175 -(defun phox-pbrpm-escape-string 87,3302 -(defun phox-pbrpm-generate-menu 91,3437 -(defalias 'proof-pbrpm-generate-menu proof-pbrpm-generate-menu298,10917 -(defalias 'proof-pbrpm-left-paren-p proof-pbrpm-left-paren-p299,10981 -(defalias 'proof-pbrpm-right-paren-p proof-pbrpm-right-paren-p300,11043 - -phox/phox-sym-lock.el,1353 -(defvar phox-sym-lock-sym-count 36,1642 -(defvar phox-sym-lock-ext-start 39,1712 -(defvar phox-sym-lock-ext-end 41,1834 -(defvar phox-sym-lock-font-size 44,1953 -(defvar phox-sym-lock-keywords 49,2143 -(defvar phox-sym-lock-enabled 54,2319 -(defvar phox-sym-lock-color 59,2481 -(defvar phox-sym-lock-mouse-face 64,2699 -(defvar phox-sym-lock-mouse-face-enabled 69,2889 -(defconst phox-sym-lock-with-mule 74,3079 -(defun phox-sym-lock-gen-symbol 77,3163 -(defun phox-sym-lock-make-symbols-atomic 85,3465 -(defun phox-sym-lock-compute-font-size 112,4406 -(defvar phox-sym-lock-font-name150,5825 -(defun phox-sym-lock-set-foreground 192,7304 -(defun phox-sym-lock-translate-char 206,7913 -(defun phox-sym-lock-translate-char-or-string 214,8181 -(defun phox-sym-lock-remap-face 221,8408 -(defvar phox-sym-lock-clear-face241,9398 -(defun phox-sym-lock 253,9819 -(defun phox-sym-lock-rec 262,10223 -(defun phox-sym-lock-atom-face 268,10368 -(defun phox-sym-lock-pre-idle-hook-first 273,10664 -(defun phox-sym-lock-pre-idle-hook-last 281,11022 -(defun phox-sym-lock-enable 290,11397 -(defun phox-sym-lock-disable 303,11810 -(defun phox-sym-lock-mouse-face-enable 316,12228 -(defun phox-sym-lock-mouse-face-disable 323,12443 -(defun phox-sym-lock-font-lock-hook 330,12662 -(defun font-lock-set-defaults 345,13353 -(defun phox-sym-lock-patch-keywords 356,13717 +phox/phox-outline.el,254 +(defconst phox-outline-title-regexp 20,745 +(defconst phox-outline-section-regexp 21,810 +(defconst phox-outline-save-regexp 22,866 +(defconst phox-outline-heading-end-regexp 39,1409 +(defun phox-outline-level(45,1584 +(defun phox-setup-outline 59,2058 + +phox/phox-pbrpm.el,513 +(defun phox-pbrpm-left-paren-p 39,1671 +(defun phox-pbrpm-right-paren-p 46,1874 +(defun phox-pbrpm-menu-from-string 54,2078 +(defun phox-pbrpm-rename-in-cmd 63,2410 +(defun phox-pbrpm-get-region-name 96,3658 +(defun phox-pbrpm-escape-string 99,3785 +(defun phox-pbrpm-generate-menu 103,3920 +(defalias 'proof-pbrpm-generate-menu proof-pbrpm-generate-menu310,11400 +(defalias 'proof-pbrpm-left-paren-p proof-pbrpm-left-paren-p311,11464 +(defalias 'proof-pbrpm-right-paren-p proof-pbrpm-right-paren-p312,11526 + +phox/phox-sym-lock.el,1398 +(defcustom phox-sym-lock-enabled 19,871 +(defvar phox-sym-lock-sym-count 59,2452 +(defvar phox-sym-lock-ext-start 62,2522 +(defvar phox-sym-lock-ext-end 64,2644 +(defvar phox-sym-lock-font-size 67,2763 +(defvar phox-sym-lock-keywords 72,2953 +(defvar phox-sym-lock-enabled 77,3129 +(defvar phox-sym-lock-color 82,3291 +(defvar phox-sym-lock-mouse-face 87,3509 +(defvar phox-sym-lock-mouse-face-enabled 92,3699 +(defconst phox-sym-lock-with-mule 97,3889 +(defun phox-sym-lock-gen-symbol 100,3973 +(defun phox-sym-lock-make-symbols-atomic 108,4275 +(defun phox-sym-lock-compute-font-size 135,5216 +(defvar phox-sym-lock-font-name173,6635 +(defun phox-sym-lock-set-foreground 216,8233 +(defun phox-sym-lock-translate-char 230,8842 +(defun phox-sym-lock-translate-char-or-string 239,9159 +(defun phox-sym-lock-remap-face 246,9387 +(defvar phox-sym-lock-clear-face266,10375 +(defun phox-sym-lock 278,10794 +(defun phox-sym-lock-rec 287,11198 +(defun phox-sym-lock-atom-face 293,11343 +(defun phox-sym-lock-pre-idle-hook-first 298,11639 +(defun phox-sym-lock-pre-idle-hook-last 308,12044 +(defun phox-sym-lock-enable 317,12419 +(defun phox-sym-lock-disable 330,12830 +(defun phox-sym-lock-mouse-face-enable 343,13246 +(defun phox-sym-lock-mouse-face-disable 350,13461 +(defun phox-sym-lock-font-lock-hook 357,13680 +(defun font-lock-set-defaults 372,14371 +(defun phox-sym-lock-patch-keywords 384,14798 phox/phox-tags.el,305 -(defun phox-tags-add-table(21,766 -(defun phox-tags-reset-table(30,1161 -(defun phox-tags-add-doc-table(35,1271 -(defun phox-tags-add-lib-table(41,1420 -(defun phox-tags-add-local-table(47,1555 -(defun phox-tags-create-local-table(53,1738 -(defun phox-complete-tag(64,1988 -(defvar phox-tags-menu71,2097 +(defun phox-tags-add-table(26,869 +(defun phox-tags-reset-table(35,1264 +(defun phox-tags-add-doc-table(40,1374 +(defun phox-tags-add-lib-table(46,1523 +(defun phox-tags-add-local-table(52,1658 +(defun phox-tags-create-local-table(58,1841 +(defun phox-complete-tag(69,2091 +(defvar phox-tags-menu76,2200 plastic/plastic.el,2759 (defcustom plastic-tags 29,608 @@ -825,24 +856,24 @@ plastic/plastic.el,2759 (defun plastic-small-bar 517,17561 (defun plastic-large-bar 519,17650 (defun plastic-preprocessing 521,17788 -(defun plastic-all-ctxt 572,19569 -(defun plastic-send-one-undo 579,19738 -(defun plastic-minibuf-cmd 589,20044 -(defun plastic-minibuf 601,20516 -(defun plastic-synchro 608,20722 -(defun plastic-send-minibuf 613,20863 -(defun plastic-had-error 621,21171 -(defun plastic-reset-error 625,21346 -(defun plastic-call-if-no-error 628,21485 -(defun plastic-show-shell 633,21689 -(define-key plastic-keymap 638,21817 -(define-key plastic-keymap 639,21878 -(define-key plastic-keymap 640,21939 -(define-key plastic-keymap 641,21999 -(define-key plastic-keymap 642,22058 -(define-key plastic-keymap 643,22117 -(defalias 'proof-toolbar-command proof-toolbar-command653,22366 -(defalias 'proof-minibuffer-cmd proof-minibuffer-cmd654,22417 +(defun plastic-all-ctxt 573,19591 +(defun plastic-send-one-undo 580,19760 +(defun plastic-minibuf-cmd 590,20066 +(defun plastic-minibuf 602,20538 +(defun plastic-synchro 609,20744 +(defun plastic-send-minibuf 614,20885 +(defun plastic-had-error 622,21193 +(defun plastic-reset-error 626,21368 +(defun plastic-call-if-no-error 629,21507 +(defun plastic-show-shell 634,21711 +(define-key plastic-keymap 639,21839 +(define-key plastic-keymap 640,21900 +(define-key plastic-keymap 641,21961 +(define-key plastic-keymap 642,22021 +(define-key plastic-keymap 643,22080 +(define-key plastic-keymap 644,22139 +(defalias 'proof-toolbar-command proof-toolbar-command654,22388 +(defalias 'proof-minibuffer-cmd proof-minibuffer-cmd655,22439 plastic/plastic-syntax.el,648 (defconst plastic-keywords-goal 18,536 @@ -905,118 +936,118 @@ generic/pg-goals.el,285 (defun pg-goals-display 77,2204 (defun pg-goals-button-action 118,3508 -generic/pg-pbrpm.el,1805 -(defvar pg-pbrpm-use-buffer-menu 31,742 -(defvar pg-pbrpm-start-goal-regexp 34,864 -(defvar pg-pbrpm-start-goal-regexp-par-num 38,1021 -(defvar pg-pbrpm-end-goal-regexp 41,1144 -(defvar pg-pbrpm-start-hyp-regexp 45,1296 -(defvar pg-pbrpm-start-hyp-regexp-par-num 49,1457 -(defvar pg-pbrpm-start-concl-regexp 53,1664 -(defvar pg-pbrpm-auto-select-regexp 57,1828 -(defvar pg-pbrpm-buffer-menu 64,1989 -(defvar pg-pbrpm-spans 65,2023 -(defvar pg-pbrpm-goal-description 66,2051 -(defvar pg-pbrpm-windows-dialog-bug 67,2090 -(defvar pbrpm-menu-desc 68,2131 -(defun pg-pbrpm-erase-buffer-menu 70,2161 -(defun pg-pbrpm-menu-change-hook 77,2345 -(defun pg-pbrpm-create-reset-buffer-menu 95,2920 -(defun pg-pbrpm-analyse-goal-buffer 114,3762 -(defun pg-pbrpm-button-action 174,6160 -(defun pg-pbrpm-exists 181,6386 -(defun pg-pbrpm-eliminate-id 185,6498 -(defun pg-pbrpm-build-menu 193,6744 -(defun pg-pbrpm-setup-span 256,9064 -(defun pg-pbrpm-run-command 316,11379 -(defun pg-pbrpm-get-pos-info 345,12689 -(defun pg-pbrpm-get-region-info 387,13988 -(defun pg-pbrpm-auto-select-around-point 398,14400 -(defun pg-pbrpm-translate-position 413,14924 -(defun pg-pbrpm-process-click 421,15181 -(defvar pg-pbrpm-remember-region-selected-region 441,16206 -(defvar pg-pbrpm-regions-list 442,16260 -(defun pg-pbrpm-erase-regions-list 444,16296 -(defun pg-pbrpm-filter-regions-list 453,16604 -(defface pg-pbrpm-multiple-selection-face460,16867 -(defface pg-pbrpm-menu-input-face468,17069 -(defun pg-pbrpm-do-remember-region 476,17259 -(defun pg-pbrpm-remember-region-drag-up-hook 497,18107 -(defun pg-pbrpm-remember-region-click-hook 501,18278 -(defun pg-pbrpm-remember-region 506,18463 -(defun pg-pbrpm-process-region 520,19177 -(defun pg-pbrpm-process-regions-list 538,19906 -(defun pg-pbrpm-region-expression 542,20089 +generic/pg-pbrpm.el,1808 +(defvar pg-pbrpm-use-buffer-menu 41,1185 +(defvar pg-pbrpm-start-goal-regexp 44,1307 +(defvar pg-pbrpm-start-goal-regexp-par-num 48,1464 +(defvar pg-pbrpm-end-goal-regexp 51,1587 +(defvar pg-pbrpm-start-hyp-regexp 55,1739 +(defvar pg-pbrpm-start-hyp-regexp-par-num 59,1900 +(defvar pg-pbrpm-start-concl-regexp 63,2107 +(defvar pg-pbrpm-auto-select-regexp 67,2271 +(defvar pg-pbrpm-buffer-menu 74,2432 +(defvar pg-pbrpm-spans 75,2466 +(defvar pg-pbrpm-goal-description 76,2494 +(defvar pg-pbrpm-windows-dialog-bug 77,2533 +(defvar pbrpm-menu-desc 78,2574 +(defun pg-pbrpm-erase-buffer-menu 80,2604 +(defun pg-pbrpm-menu-change-hook 87,2788 +(defun pg-pbrpm-create-reset-buffer-menu 105,3363 +(defun pg-pbrpm-analyse-goal-buffer 124,4205 +(defun pg-pbrpm-button-action 184,6603 +(defun pg-pbrpm-exists 191,6829 +(defun pg-pbrpm-eliminate-id 195,6941 +(defun pg-pbrpm-build-menu 203,7187 +(defun pg-pbrpm-setup-span 266,9507 +(defun pg-pbrpm-run-command 326,11822 +(defun pg-pbrpm-get-pos-info 356,13149 +(defun pg-pbrpm-get-region-info 398,14448 +(defun pg-pbrpm-auto-select-around-point 409,14860 +(defun pg-pbrpm-translate-position 424,15384 +(defun pg-pbrpm-process-click 432,15641 +(defvar pg-pbrpm-remember-region-selected-region 452,16666 +(defvar pg-pbrpm-regions-list 453,16720 +(defun pg-pbrpm-erase-regions-list 455,16756 +(defun pg-pbrpm-filter-regions-list 464,17064 +(defface pg-pbrpm-multiple-selection-face471,17327 +(defface pg-pbrpm-menu-input-face479,17529 +(defun pg-pbrpm-do-remember-region 487,17719 +(defun pg-pbrpm-remember-region-drag-up-hook 508,18567 +(defun pg-pbrpm-remember-region-click-hook 512,18738 +(defun pg-pbrpm-remember-region 517,18923 +(defun pg-pbrpm-process-region 531,19637 +(defun pg-pbrpm-process-regions-list 549,20366 +(defun pg-pbrpm-region-expression 553,20549 generic/pg-pgip.el,2931 -(defalias 'pg-pgip-debug pg-pgip-debug39,1033 -(defalias 'pg-pgip-error pg-pgip-error40,1074 -(defalias 'pg-pgip-warning pg-pgip-warning41,1109 -(defconst pg-pgip-version-supported 43,1159 -(defun pg-pgip-process-packet 47,1265 -(defvar pg-pgip-last-seen-id 57,1833 -(defvar pg-pgip-last-seen-seq 58,1867 -(defun pg-pgip-process-pgip 60,1903 -(defun pg-pgip-process-msg 79,2834 -(defvar pg-pgip-post-process-functions93,3404 -(defun pg-pgip-post-process 103,3892 -(defun pg-pgip-process-askpgip 119,4502 -(defun pg-pgip-process-usespgip 125,4706 -(defun pg-pgip-process-usespgml 129,4870 -(defun pg-pgip-process-pgmlconfig 133,5034 -(defun pg-pgip-process-proverinfo 149,5651 -(defun pg-pgip-process-hasprefs 166,6316 -(defun pg-pgip-haspref 180,6948 -(defun pg-pgip-process-prefval 197,7650 -(defun pg-pgip-process-guiconfig 224,8358 -(defvar proof-assistant-idtables 231,8475 -(defun pg-pgip-process-ids 234,8592 -(defun pg-complete-idtable-symbol 260,9664 -(defalias 'pg-pgip-process-setids pg-pgip-process-setids265,9756 -(defalias 'pg-pgip-process-addids pg-pgip-process-addids266,9812 -(defalias 'pg-pgip-process-delids pg-pgip-process-delids267,9868 -(defun pg-pgip-process-idvalue 270,9926 -(defun pg-pgip-process-menuadd 282,10272 -(defun pg-pgip-process-menudel 285,10315 -(defun pg-pgip-process-ready 294,10547 -(defun pg-pgip-process-cleardisplay 297,10588 -(defun pg-pgip-process-proofstate 311,11045 -(defun pg-pgip-process-normalresponse 315,11122 -(defun pg-pgip-process-errorresponse 319,11252 -(defun pg-pgip-process-scriptinsert 323,11381 -(defun pg-pgip-process-metainforesponse 328,11515 -(defun pg-pgip-file-of-url 337,11755 -(defun pg-pgip-process-informfileloaded 342,11890 -(defun pg-pgip-process-informfileretracted 348,12122 -(defun pg-pgip-process-brokerstatus 361,12569 -(defun pg-pgip-process-proveravailmsg 364,12617 -(defun pg-pgip-process-newprovermsg 367,12667 -(defun pg-pgip-process-proverstatusmsg 370,12715 -(defvar pg-pgip-srcids 379,12961 -(defun pg-pgip-process-newfile 383,13068 -(defun pg-pgip-process-filestatus 399,13650 -(defun pg-pgip-process-newobj 419,14304 -(defun pg-pgip-process-delobj 422,14346 -(defun pg-pgip-process-objectstatus 425,14388 -(defun pg-pgip-process-parsescript 439,14740 -(defun pg-pgip-get-pgiptype 462,15614 -(defun pg-pgip-default-for 482,16406 -(defun pg-pgip-subst-for 495,16801 -(defun pg-pgip-interpret-value 507,17144 -(defun pg-pgip-interpret-choice 525,17825 -(defun pg-pgip-string-of-command 556,18842 -(defconst pg-pgip-id573,19603 -(defvar pg-pgip-refseq 579,19883 -(defvar pg-pgip-refid 581,19980 -(defvar pg-pgip-seq 584,20072 -(defun pg-pgip-assemble-packet 586,20136 -(defun pg-pgip-issue 604,20947 -(defun pg-pgip-maybe-askpgip 621,21559 -(defun pg-pgip-askprefs 627,21750 -(defun pg-pgip-askids 631,21864 -(defun pg-pgip-reset 644,22152 -(defconst pg-pgip-start-element-regexp 675,22850 -(defconst pg-pgip-end-element-regexp 676,22902 +(defalias 'pg-pgip-debug pg-pgip-debug38,1032 +(defalias 'pg-pgip-error pg-pgip-error39,1073 +(defalias 'pg-pgip-warning pg-pgip-warning40,1108 +(defconst pg-pgip-version-supported 42,1158 +(defun pg-pgip-process-packet 46,1264 +(defvar pg-pgip-last-seen-id 56,1832 +(defvar pg-pgip-last-seen-seq 57,1866 +(defun pg-pgip-process-pgip 59,1902 +(defun pg-pgip-process-msg 78,2833 +(defvar pg-pgip-post-process-functions92,3403 +(defun pg-pgip-post-process 102,3891 +(defun pg-pgip-process-askpgip 118,4501 +(defun pg-pgip-process-usespgip 124,4705 +(defun pg-pgip-process-usespgml 128,4869 +(defun pg-pgip-process-pgmlconfig 132,5033 +(defun pg-pgip-process-proverinfo 148,5650 +(defun pg-pgip-process-hasprefs 165,6315 +(defun pg-pgip-haspref 179,6947 +(defun pg-pgip-process-prefval 196,7649 +(defun pg-pgip-process-guiconfig 223,8357 +(defvar proof-assistant-idtables 230,8474 +(defun pg-pgip-process-ids 233,8591 +(defun pg-complete-idtable-symbol 259,9663 +(defalias 'pg-pgip-process-setids pg-pgip-process-setids264,9755 +(defalias 'pg-pgip-process-addids pg-pgip-process-addids265,9811 +(defalias 'pg-pgip-process-delids pg-pgip-process-delids266,9867 +(defun pg-pgip-process-idvalue 269,9925 +(defun pg-pgip-process-menuadd 281,10271 +(defun pg-pgip-process-menudel 284,10314 +(defun pg-pgip-process-ready 293,10546 +(defun pg-pgip-process-cleardisplay 296,10587 +(defun pg-pgip-process-proofstate 310,11044 +(defun pg-pgip-process-normalresponse 314,11121 +(defun pg-pgip-process-errorresponse 318,11251 +(defun pg-pgip-process-scriptinsert 322,11380 +(defun pg-pgip-process-metainforesponse 327,11514 +(defun pg-pgip-file-of-url 336,11754 +(defun pg-pgip-process-informfileloaded 341,11889 +(defun pg-pgip-process-informfileretracted 347,12121 +(defun pg-pgip-process-brokerstatus 360,12568 +(defun pg-pgip-process-proveravailmsg 363,12616 +(defun pg-pgip-process-newprovermsg 366,12666 +(defun pg-pgip-process-proverstatusmsg 369,12714 +(defvar pg-pgip-srcids 378,12960 +(defun pg-pgip-process-newfile 382,13067 +(defun pg-pgip-process-filestatus 398,13649 +(defun pg-pgip-process-newobj 418,14303 +(defun pg-pgip-process-delobj 421,14345 +(defun pg-pgip-process-objectstatus 424,14387 +(defun pg-pgip-process-parsescript 438,14739 +(defun pg-pgip-get-pgiptype 461,15613 +(defun pg-pgip-default-for 481,16405 +(defun pg-pgip-subst-for 494,16800 +(defun pg-pgip-interpret-value 506,17143 +(defun pg-pgip-interpret-choice 524,17824 +(defun pg-pgip-string-of-command 555,18841 +(defconst pg-pgip-id572,19602 +(defvar pg-pgip-refseq 578,19882 +(defvar pg-pgip-refid 580,19979 +(defvar pg-pgip-seq 583,20071 +(defun pg-pgip-assemble-packet 585,20135 +(defun pg-pgip-issue 603,20946 +(defun pg-pgip-maybe-askpgip 620,21558 +(defun pg-pgip-askprefs 626,21749 +(defun pg-pgip-askids 630,21863 +(defun pg-pgip-reset 643,22151 +(defconst pg-pgip-start-element-regexp 674,22849 +(defconst pg-pgip-end-element-regexp 675,22901 generic/pg-response.el,1291 (deflocal pg-response-eagerly-raise 32,787 @@ -1057,87 +1088,85 @@ generic/pg-thymodes.el,152 (defun pg-modesym 82,2548 (defun pg-modesymval 86,2662 -generic/pg-user.el,3435 -(defun proof-script-next-command-advance 35,887 -(defun proof-script-new-command-advance 48,1366 -(defun proof-maybe-follow-locked-end 91,3108 -(defun proof-goto-command-start 118,3937 -(defun proof-goto-command-end 141,4877 -(defun proof-goto-point 164,5402 -(defun proof-assert-next-command-interactive 178,5836 -(defun proof-assert-until-point-interactive 191,6361 -(defun proof-process-buffer 197,6591 -(defun proof-undo-last-successful-command 212,6968 -(defun proof-undo-and-delete-last-successful-command 217,7130 -(defun proof-undo-last-successful-command-1 230,7684 -(defun proof-retract-buffer 247,8296 -(defun proof-retract-current-goal 256,8580 -(defun proof-mouse-goto-point 275,9100 -(defvar proof-minibuffer-history 290,9376 -(defun proof-minibuffer-cmd 293,9471 -(defun proof-frob-locked-end 337,11093 -(defmacro proof-if-setting-configured 398,13017 -(defmacro proof-define-assistant-command 406,13286 -(defmacro proof-define-assistant-command-witharg 419,13741 -(defun proof-issue-new-command 439,14563 -(defun proof-cd-sync 485,16060 -(defun proof-electric-terminator-enable 539,17780 -(defun proof-process-electric-terminator 547,18070 -(defun proof-electric-terminator 582,19409 -(defun proof-add-completions 604,20055 -(defun proof-script-complete 629,20962 -(defun pg-copy-span-contents 643,21271 -(defun pg-numth-span-higher-or-lower 660,21829 -(defun pg-control-span-of 686,22575 -(defun pg-move-span-contents 692,22779 -(defun pg-fixup-children-spans 744,24955 -(defun pg-move-region-down 754,25212 -(defun pg-move-region-up 763,25505 -(defun proof-forward-command 793,26333 -(defun proof-backward-command 814,27054 -(defun pg-pos-for-event 836,27398 -(defun pg-span-for-event 842,27619 -(defun pg-span-context-menu 846,27763 -(defun pg-toggle-visibility 861,28218 -(defun pg-create-in-span-context-menu 871,28540 -(defun pg-span-undo 901,29749 -(defun pg-goals-buffers-hint 947,31151 -(defun pg-slow-fontify-tracing-hint 951,31333 -(defun pg-response-buffers-hint 955,31504 -(defun pg-jump-to-end-hint 965,31866 -(defun pg-processing-complete-hint 969,31995 -(defun pg-next-error-hint 986,32694 -(defun pg-hint 991,32846 -(defun pg-identifier-under-mouse-query 1007,33436 -(defun pg-identifier-near-point-query 1016,33679 -(defvar proof-query-identifier-collection 1041,34395 -(defvar proof-query-identifier-history 1042,34442 -(defun proof-query-identifier 1044,34487 -(defun pg-identifier-query 1054,34756 -(defun proof-imenu-enable 1085,35834 -(defvar pg-input-ring 1116,36895 -(defvar pg-input-ring-index 1119,36952 -(defvar pg-stored-incomplete-input 1122,37024 -(defun pg-previous-input 1125,37127 -(defun pg-next-input 1139,37584 -(defun pg-delete-input 1144,37706 -(defun pg-get-old-input 1157,38044 -(defun pg-restore-input 1171,38435 -(defun pg-search-start 1182,38725 -(defun pg-regexp-arg 1194,39217 -(defun pg-search-arg 1206,39665 -(defun pg-previous-matching-input-string-position 1220,40082 -(defun pg-previous-matching-input 1247,41247 -(defun pg-next-matching-input 1266,42097 -(defvar pg-matching-input-from-input-string 1274,42480 -(defun pg-previous-matching-input-from-input 1278,42594 -(defun pg-next-matching-input-from-input 1296,43359 -(defun pg-add-to-input-history 1307,43738 -(defun pg-remove-from-input-history 1319,44191 -(defun pg-clear-input-ring 1330,44571 -(define-key proof-mode-map 1344,44921 -(define-key proof-mode-map 1345,44981 -(defun pg-protected-undo 1347,45053 +generic/pg-user.el,3331 +(defun proof-script-new-command-advance 41,1156 +(defun proof-maybe-follow-locked-end 84,2897 +(defun proof-goto-command-start 111,3726 +(defun proof-goto-command-end 134,4666 +(defun proof-goto-point 157,5191 +(defun proof-assert-next-command-interactive 171,5625 +(defun proof-assert-until-point-interactive 184,6150 +(defun proof-process-buffer 190,6380 +(defun proof-undo-last-successful-command 205,6757 +(defun proof-undo-and-delete-last-successful-command 210,6919 +(defun proof-undo-last-successful-command-1 223,7473 +(defun proof-retract-buffer 240,8085 +(defun proof-retract-current-goal 249,8369 +(defun proof-mouse-goto-point 268,8889 +(defvar proof-minibuffer-history 283,9165 +(defun proof-minibuffer-cmd 286,9260 +(defun proof-frob-locked-end 330,10882 +(defmacro proof-if-setting-configured 391,12806 +(defmacro proof-define-assistant-command 399,13075 +(defmacro proof-define-assistant-command-witharg 412,13530 +(defun proof-issue-new-command 432,14352 +(defun proof-cd-sync 478,15849 +(defun proof-electric-terminator-enable 532,17569 +(defun proof-electric-terminator 540,17859 +(defun proof-add-completions 562,18504 +(defun proof-script-complete 587,19411 +(defun pg-copy-span-contents 601,19720 +(defun pg-numth-span-higher-or-lower 618,20278 +(defun pg-control-span-of 644,21024 +(defun pg-move-span-contents 650,21228 +(defun pg-fixup-children-spans 702,23404 +(defun pg-move-region-down 712,23661 +(defun pg-move-region-up 721,23954 +(defun proof-forward-command 751,24782 +(defun proof-backward-command 772,25503 +(defun pg-pos-for-event 794,25847 +(defun pg-span-for-event 800,26068 +(defun pg-span-context-menu 804,26212 +(defun pg-toggle-visibility 819,26667 +(defun pg-create-in-span-context-menu 829,26989 +(defun pg-span-undo 859,28198 +(defun pg-goals-buffers-hint 905,29600 +(defun pg-slow-fontify-tracing-hint 909,29782 +(defun pg-response-buffers-hint 913,29953 +(defun pg-jump-to-end-hint 923,30315 +(defun pg-processing-complete-hint 927,30444 +(defun pg-next-error-hint 944,31143 +(defun pg-hint 949,31295 +(defun pg-identifier-under-mouse-query 965,31885 +(defun pg-identifier-near-point-query 974,32128 +(defvar proof-query-identifier-collection 999,32844 +(defvar proof-query-identifier-history 1000,32891 +(defun proof-query-identifier 1002,32936 +(defun pg-identifier-query 1012,33205 +(defun proof-imenu-enable 1043,34283 +(defvar pg-input-ring 1079,35605 +(defvar pg-input-ring-index 1082,35662 +(defvar pg-stored-incomplete-input 1085,35734 +(defun pg-previous-input 1088,35837 +(defun pg-next-input 1102,36294 +(defun pg-delete-input 1107,36416 +(defun pg-get-old-input 1120,36754 +(defun pg-restore-input 1134,37145 +(defun pg-search-start 1145,37435 +(defun pg-regexp-arg 1157,37927 +(defun pg-search-arg 1169,38375 +(defun pg-previous-matching-input-string-position 1183,38792 +(defun pg-previous-matching-input 1210,39957 +(defun pg-next-matching-input 1229,40807 +(defvar pg-matching-input-from-input-string 1237,41190 +(defun pg-previous-matching-input-from-input 1241,41304 +(defun pg-next-matching-input-from-input 1259,42069 +(defun pg-add-to-input-history 1270,42448 +(defun pg-remove-from-input-history 1282,42901 +(defun pg-clear-input-ring 1293,43281 +(define-key proof-mode-map 1307,43631 +(define-key proof-mode-map 1308,43691 +(defun pg-protected-undo 1310,43763 generic/pg-vars.el,1452 (defvar proof-assistant-cusgrp 22,382 @@ -1210,14 +1239,14 @@ generic/pg-xml.el,1177 (defun pg-pgip-get-pgmltext 223,7251 generic/proof-autoloads.el,45 -(defsubst proof-shell-live-buffer 636,20899 +(defsubst proof-shell-live-buffer 636,21159 generic/proof-auxmodes.el,149 (defun proof-mmm-support-available 20,489 (defun proof-maths-menu-support-available 44,1100 (defun proof-unicode-tokens-support-available 58,1517 -generic/proof-config.el,7858 +generic/proof-config.el,7905 (defgroup prover-config 80,2633 (defcustom proof-guess-command-line 98,3483 (defcustom proof-assistant-home-page 113,3978 @@ -1271,109 +1300,110 @@ generic/proof-config.el,7858 (defcustom pg-topterm-goalhyplit-fn 640,24872 (defcustom proof-kill-goal-command 652,25407 (defcustom proof-undo-n-times-cmd 666,25911 -(defcustom proof-nested-goals-history-p 680,26459 -(defcustom proof-arbitrary-undo-positions 689,26796 -(defcustom proof-state-preserving-p 703,27376 -(defcustom proof-activate-scripting-hook 713,27848 -(defcustom proof-deactivate-scripting-hook 732,28629 -(defcustom proof-script-evaluate-elisp-comment-regexp 741,28959 -(defcustom proof-indent 759,29545 -(defcustom proof-indent-hang 764,29652 -(defcustom proof-indent-enclose-offset 769,29778 -(defcustom proof-indent-open-offset 774,29920 -(defcustom proof-indent-close-offset 779,30057 -(defcustom proof-indent-any-regexp 784,30195 -(defcustom proof-indent-inner-regexp 789,30355 -(defcustom proof-indent-enclose-regexp 794,30509 -(defcustom proof-indent-open-regexp 799,30663 -(defcustom proof-indent-close-regexp 804,30815 -(defcustom proof-script-font-lock-keywords 810,30969 -(defcustom proof-script-syntax-table-entries 818,31321 -(defcustom proof-script-span-context-menu-extensions 836,31717 -(defgroup proof-shell 862,32475 -(defcustom proof-prog-name 872,32645 -(defcustom proof-shell-auto-terminate-commands 883,33065 -(defcustom proof-shell-pre-sync-init-cmd 892,33466 -(defcustom proof-shell-init-cmd 906,34024 -(defcustom proof-shell-init-hook 918,34553 -(defcustom proof-shell-restart-cmd 923,34692 -(defcustom proof-shell-quit-cmd 928,34847 -(defcustom proof-shell-quit-timeout 933,35014 -(defcustom proof-shell-cd-cmd 943,35464 -(defcustom proof-shell-start-silent-cmd 960,36135 -(defcustom proof-shell-stop-silent-cmd 969,36511 -(defcustom proof-shell-silent-threshold 978,36846 -(defcustom proof-shell-inform-file-processed-cmd 986,37180 -(defcustom proof-shell-inform-file-retracted-cmd 1007,38108 -(defcustom proof-auto-multiple-files 1035,39380 -(defcustom proof-cannot-reopen-processed-files 1050,40101 -(defcustom proof-shell-require-command-regexp 1064,40767 -(defcustom proof-done-advancing-require-function 1075,41229 -(defcustom proof-shell-annotated-prompt-regexp 1087,41589 -(defcustom proof-shell-error-regexp 1102,42154 -(defcustom proof-shell-truncate-before-error 1122,42956 -(defcustom pg-next-error-regexp 1136,43495 -(defcustom pg-next-error-filename-regexp 1151,44104 -(defcustom pg-next-error-extract-filename 1175,45137 -(defcustom proof-shell-interrupt-regexp 1182,45380 -(defcustom proof-shell-proof-completed-regexp 1196,45975 -(defcustom proof-shell-clear-response-regexp 1209,46483 -(defcustom proof-shell-clear-goals-regexp 1221,46935 -(defcustom proof-shell-start-goals-regexp 1233,47381 -(defcustom proof-shell-end-goals-regexp 1241,47748 -(defcustom proof-shell-eager-annotation-start 1255,48323 -(defcustom proof-shell-eager-annotation-start-length 1278,49342 -(defcustom proof-shell-eager-annotation-end 1289,49768 -(defcustom proof-shell-strip-output-markup 1305,50443 -(defcustom proof-shell-assumption-regexp 1314,50828 -(defcustom proof-shell-process-file 1324,51232 -(defcustom proof-shell-retract-files-regexp 1350,52310 -(defcustom proof-shell-compute-new-files-list 1363,52798 -(defcustom pg-special-char-regexp 1378,53367 -(defcustom proof-shell-set-elisp-variable-regexp 1383,53511 -(defcustom proof-shell-match-pgip-cmd 1421,55177 -(defcustom proof-shell-issue-pgip-cmd 1435,55659 -(defcustom proof-use-pgip-askprefs 1440,55824 -(defcustom proof-shell-query-dependencies-cmd 1448,56171 -(defcustom proof-shell-theorem-dependency-list-regexp 1455,56431 -(defcustom proof-shell-theorem-dependency-list-split 1471,57091 -(defcustom proof-shell-show-dependency-cmd 1480,57514 -(defcustom proof-shell-trace-output-regexp 1502,58420 -(defcustom proof-shell-thms-output-regexp 1520,59015 -(defcustom proof-tokens-activate-command 1533,59398 -(defcustom proof-tokens-deactivate-command 1540,59638 -(defcustom proof-tokens-extra-modes 1547,59883 -(defcustom proof-shell-unicode 1562,60388 -(defcustom proof-shell-filename-escapes 1571,60778 -(defcustom proof-shell-process-connection-type1588,61458 -(defcustom proof-shell-strip-crs-from-input 1611,62462 -(defcustom proof-shell-strip-crs-from-output 1623,62945 -(defcustom proof-shell-insert-hook 1631,63313 -(defcustom proof-shell-handle-delayed-output-hook1669,65173 -(defcustom proof-shell-handle-error-or-interrupt-hook1675,65388 -(defcustom proof-shell-pre-interrupt-hook1693,66134 -(defcustom proof-shell-handle-output-system-specific 1701,66405 -(defcustom proof-state-change-hook 1724,67381 -(defcustom proof-shell-syntax-table-entries 1734,67774 -(defgroup proof-goals 1752,68145 -(defcustom pg-subterm-first-special-char 1757,68266 -(defcustom pg-subterm-anns-use-stack 1765,68578 -(defcustom pg-goals-change-goal 1774,68877 -(defcustom pbp-goal-command 1779,68993 -(defcustom pbp-hyp-command 1784,69149 -(defcustom pg-subterm-help-cmd 1789,69311 -(defcustom pg-goals-error-regexp 1796,69547 -(defcustom proof-shell-result-start 1801,69707 -(defcustom proof-shell-result-end 1807,69941 -(defcustom pg-subterm-start-char 1813,70154 -(defcustom pg-subterm-sep-char 1827,70739 -(defcustom pg-subterm-end-char 1833,70918 -(defcustom pg-topterm-regexp 1839,71075 -(defcustom proof-goals-font-lock-keywords 1854,71675 -(defcustom proof-response-font-lock-keywords 1862,72034 -(defcustom proof-shell-font-lock-keywords 1870,72396 -(defcustom pg-before-fontify-output-hook 1881,72911 -(defcustom pg-after-fontify-output-hook 1889,73272 +(defcustom proof-nested-goals-history-p 680,26448 +(defcustom proof-arbitrary-undo-positions 689,26785 +(defcustom proof-state-preserving-p 703,27365 +(defcustom proof-activate-scripting-hook 713,27837 +(defcustom proof-deactivate-scripting-hook 732,28618 +(defcustom proof-script-evaluate-elisp-comment-regexp 741,28948 +(defcustom proof-indent 759,29534 +(defcustom proof-indent-hang 764,29641 +(defcustom proof-indent-enclose-offset 769,29767 +(defcustom proof-indent-open-offset 774,29909 +(defcustom proof-indent-close-offset 779,30046 +(defcustom proof-indent-any-regexp 784,30184 +(defcustom proof-indent-inner-regexp 789,30344 +(defcustom proof-indent-enclose-regexp 794,30498 +(defcustom proof-indent-open-regexp 799,30652 +(defcustom proof-indent-close-regexp 804,30804 +(defcustom proof-script-font-lock-keywords 810,30958 +(defcustom proof-script-syntax-table-entries 818,31310 +(defcustom proof-script-span-context-menu-extensions 836,31706 +(defgroup proof-shell 862,32464 +(defcustom proof-prog-name 872,32634 +(defcustom proof-shell-auto-terminate-commands 883,33054 +(defcustom proof-shell-pre-sync-init-cmd 892,33455 +(defcustom proof-shell-init-cmd 906,34013 +(defcustom proof-shell-init-hook 918,34542 +(defcustom proof-shell-restart-cmd 923,34681 +(defcustom proof-shell-quit-cmd 928,34836 +(defcustom proof-shell-quit-timeout 933,35003 +(defcustom proof-shell-cd-cmd 943,35453 +(defcustom proof-shell-start-silent-cmd 960,36124 +(defcustom proof-shell-stop-silent-cmd 969,36500 +(defcustom proof-shell-silent-threshold 978,36835 +(defcustom proof-shell-inform-file-processed-cmd 986,37169 +(defcustom proof-shell-inform-file-retracted-cmd 1007,38097 +(defcustom proof-auto-multiple-files 1035,39369 +(defcustom proof-cannot-reopen-processed-files 1050,40090 +(defcustom proof-shell-require-command-regexp 1064,40756 +(defcustom proof-done-advancing-require-function 1075,41218 +(defcustom proof-shell-annotated-prompt-regexp 1087,41578 +(defcustom proof-shell-error-regexp 1102,42143 +(defcustom proof-shell-truncate-before-error 1122,42945 +(defcustom pg-next-error-regexp 1136,43484 +(defcustom pg-next-error-filename-regexp 1151,44093 +(defcustom pg-next-error-extract-filename 1175,45126 +(defcustom proof-shell-interrupt-regexp 1182,45369 +(defcustom proof-shell-proof-completed-regexp 1196,45964 +(defcustom proof-shell-clear-response-regexp 1209,46472 +(defcustom proof-shell-clear-goals-regexp 1221,46924 +(defcustom proof-shell-start-goals-regexp 1233,47370 +(defcustom proof-shell-end-goals-regexp 1241,47737 +(defcustom proof-shell-eager-annotation-start 1255,48312 +(defcustom proof-shell-eager-annotation-start-length 1278,49331 +(defcustom proof-shell-eager-annotation-end 1289,49757 +(defcustom proof-shell-strip-output-markup 1305,50432 +(defcustom proof-shell-assumption-regexp 1314,50817 +(defcustom proof-shell-process-file 1324,51221 +(defcustom proof-shell-retract-files-regexp 1350,52299 +(defcustom proof-shell-compute-new-files-list 1363,52787 +(defcustom pg-special-char-regexp 1378,53356 +(defcustom proof-shell-set-elisp-variable-regexp 1383,53500 +(defcustom proof-shell-match-pgip-cmd 1421,55166 +(defcustom proof-shell-issue-pgip-cmd 1435,55648 +(defcustom proof-use-pgip-askprefs 1440,55813 +(defcustom proof-shell-query-dependencies-cmd 1448,56160 +(defcustom proof-shell-theorem-dependency-list-regexp 1455,56420 +(defcustom proof-shell-theorem-dependency-list-split 1471,57080 +(defcustom proof-shell-show-dependency-cmd 1480,57503 +(defcustom proof-shell-trace-output-regexp 1502,58409 +(defcustom proof-shell-thms-output-regexp 1520,59004 +(defcustom proof-tokens-activate-command 1533,59387 +(defcustom proof-tokens-deactivate-command 1540,59627 +(defcustom proof-tokens-extra-modes 1547,59872 +(defcustom proof-shell-unicode 1562,60377 +(defcustom proof-shell-filename-escapes 1571,60767 +(defcustom proof-shell-process-connection-type1588,61447 +(defcustom proof-shell-strip-crs-from-input 1611,62451 +(defcustom proof-shell-strip-crs-from-output 1623,62934 +(defcustom proof-shell-insert-hook 1631,63302 +(defcustom proof-script-preprocess 1672,65262 +(defcustom proof-shell-handle-delayed-output-hook1678,65413 +(defcustom proof-shell-handle-error-or-interrupt-hook1684,65628 +(defcustom proof-shell-pre-interrupt-hook1702,66374 +(defcustom proof-shell-handle-output-system-specific 1710,66645 +(defcustom proof-state-change-hook 1733,67621 +(defcustom proof-shell-syntax-table-entries 1743,68014 +(defgroup proof-goals 1761,68385 +(defcustom pg-subterm-first-special-char 1766,68506 +(defcustom pg-subterm-anns-use-stack 1774,68818 +(defcustom pg-goals-change-goal 1783,69117 +(defcustom pbp-goal-command 1788,69233 +(defcustom pbp-hyp-command 1793,69389 +(defcustom pg-subterm-help-cmd 1798,69551 +(defcustom pg-goals-error-regexp 1805,69787 +(defcustom proof-shell-result-start 1810,69947 +(defcustom proof-shell-result-end 1816,70181 +(defcustom pg-subterm-start-char 1822,70394 +(defcustom pg-subterm-sep-char 1836,70979 +(defcustom pg-subterm-end-char 1842,71158 +(defcustom pg-topterm-regexp 1848,71315 +(defcustom proof-goals-font-lock-keywords 1863,71915 +(defcustom proof-response-font-lock-keywords 1871,72274 +(defcustom proof-shell-font-lock-keywords 1879,72636 +(defcustom pg-before-fontify-output-hook 1890,73151 +(defcustom pg-after-fontify-output-hook 1898,73512 generic/proof-depends.el,824 (defvar proof-thm-names-of-files 23,622 @@ -1447,64 +1477,63 @@ generic/proof-indent.el,219 (defun proof-indent-line 76,2611 generic/proof-maths-menu.el,83 -(defun proof-maths-menu-set-global 30,936 -(defun proof-maths-menu-enable 44,1387 - -generic/proof-menu.el,2073 -(defvar proof-display-some-buffers-count 29,665 -(defun proof-display-some-buffers 31,710 -(defun proof-menu-define-keys 90,2906 -(defun proof-menu-define-main 149,5772 -(defvar proof-menu-favourites 158,5957 -(defvar proof-menu-settings 161,6064 -(defun proof-menu-define-specific 165,6153 -(defun proof-assistant-menu-update 208,7414 -(defvar proof-help-menu222,7847 -(defvar proof-show-hide-menu230,8117 -(defvar proof-buffer-menu239,8430 -(defun proof-retract-on-edit-toggle 302,10740 -(defun proof-keep-response-history 309,10916 -(defconst proof-quick-opts-menu317,11226 -(defun proof-quick-opts-vars 486,18144 -(defun proof-quick-opts-changed-from-defaults-p 515,19004 -(defun proof-quick-opts-changed-from-saved-p 519,19109 -(defun proof-quick-opts-save 530,19460 -(defun proof-quick-opts-reset 535,19628 -(defconst proof-config-menu547,19896 -(defconst proof-advanced-menu554,20075 -(defvar proof-menu567,20510 -(defun proof-main-menu 576,20792 -(defun proof-aux-menu 587,21058 -(defun proof-menu-define-favourites-menu 603,21404 -(defun proof-def-favourite 623,22053 -(defvar proof-make-favourite-cmd-history 646,23027 -(defvar proof-make-favourite-menu-history 649,23112 -(defun proof-save-favourites 652,23198 -(defun proof-del-favourite 657,23346 -(defun proof-read-favourite 674,23902 -(defun proof-add-favourite 698,24678 -(defun proof-menu-define-settings-menu 725,25723 -(defun proof-menu-entry-name 758,26844 -(defun proof-menu-entry-for-setting 768,27194 -(defun proof-settings-vars 787,27726 -(defun proof-settings-changed-from-defaults-p 792,27903 -(defun proof-settings-changed-from-saved-p 796,28009 -(defun proof-settings-save 800,28112 -(defun proof-settings-reset 805,28279 -(defun proof-assistant-invisible-command-ifposs 810,28442 -(defun proof-maybe-askprefs 832,29412 -(defun proof-assistant-settings-cmd 838,29604 -(defvar proof-assistant-format-table855,30259 -(defun proof-assistant-format-bool 863,30627 -(defun proof-assistant-format-int 866,30740 -(defun proof-assistant-format-string 869,30832 -(defun proof-assistant-format 872,30930 +(defun proof-maths-menu-set-global 30,942 +(defun proof-maths-menu-enable 44,1393 + +generic/proof-menu.el,2026 +(defvar proof-display-some-buffers-count 35,801 +(defun proof-display-some-buffers 37,846 +(defun proof-menu-define-keys 94,2986 +(defun proof-menu-define-main 153,5852 +(defvar proof-menu-favourites 162,6037 +(defvar proof-menu-settings 165,6144 +(defun proof-menu-define-specific 169,6233 +(defun proof-assistant-menu-update 212,7494 +(defvar proof-help-menu226,7927 +(defvar proof-show-hide-menu234,8197 +(defvar proof-buffer-menu243,8510 +(defun proof-keep-response-history 305,10779 +(defconst proof-quick-opts-menu313,11089 +(defun proof-quick-opts-vars 496,18562 +(defun proof-quick-opts-changed-from-defaults-p 525,19422 +(defun proof-quick-opts-changed-from-saved-p 529,19527 +(defun proof-quick-opts-save 540,19878 +(defun proof-quick-opts-reset 545,20046 +(defconst proof-config-menu557,20314 +(defconst proof-advanced-menu564,20493 +(defvar proof-menu577,20928 +(defun proof-main-menu 586,21210 +(defun proof-aux-menu 597,21476 +(defun proof-menu-define-favourites-menu 613,21822 +(defun proof-def-favourite 633,22471 +(defvar proof-make-favourite-cmd-history 656,23445 +(defvar proof-make-favourite-menu-history 659,23530 +(defun proof-save-favourites 662,23616 +(defun proof-del-favourite 667,23764 +(defun proof-read-favourite 684,24320 +(defun proof-add-favourite 708,25096 +(defun proof-menu-define-settings-menu 735,26141 +(defun proof-menu-entry-name 768,27262 +(defun proof-menu-entry-for-setting 778,27612 +(defun proof-settings-vars 797,28144 +(defun proof-settings-changed-from-defaults-p 802,28321 +(defun proof-settings-changed-from-saved-p 806,28427 +(defun proof-settings-save 810,28530 +(defun proof-settings-reset 815,28697 +(defun proof-assistant-invisible-command-ifposs 820,28860 +(defun proof-maybe-askprefs 842,29830 +(defun proof-assistant-settings-cmd 848,30022 +(defvar proof-assistant-format-table865,30677 +(defun proof-assistant-format-bool 873,31045 +(defun proof-assistant-format-int 876,31158 +(defun proof-assistant-format-string 879,31250 +(defun proof-assistant-format 882,31348 generic/proof-mmm.el,70 (defun proof-mmm-set-global 39,1466 (defun proof-mmm-enable 54,2005 -generic/proof-script.el,5381 +generic/proof-script.el,5552 (deflocal proof-active-buffer-fake-minor-mode 44,1308 (deflocal proof-script-buffer-file-name 47,1434 (deflocal pg-script-portions 54,1844 @@ -1515,196 +1544,197 @@ generic/proof-script.el,5381 (deflocal proof-queue-span 116,3995 (deflocal proof-overlay-arrow 125,4481 (defun proof-span-give-warning 131,4608 -(defun proof-span-read-only 136,4757 -(defun proof-strict-read-only 145,5130 -(defsubst proof-set-queue-endpoints 155,5508 -(defun proof-set-overlay-arrow 159,5649 -(defsubst proof-set-locked-endpoints 170,5987 -(defsubst proof-detach-queue 175,6163 -(defsubst proof-detach-locked 180,6302 -(defsubst proof-set-queue-start 187,6527 -(defsubst proof-set-locked-end 191,6653 -(defsubst proof-set-queue-end 203,7123 -(defun proof-init-segmentation 214,7420 -(defun proof-colour-locked 247,8882 -(defun proof-restart-buffers 258,9314 -(defun proof-script-buffers-with-spans 279,10065 -(defun proof-script-remove-all-spans-and-deactivate 289,10421 -(defun proof-script-clear-queue-spans 293,10611 -(defun proof-script-delete-spans 304,11001 -(defun proof-unprocessed-begin 320,11453 -(defun proof-script-end 328,11707 -(defun proof-queue-or-locked-end 337,12010 -(defun proof-locked-end 352,12688 -(defun proof-locked-region-full-p 366,12969 -(defun proof-locked-region-empty-p 375,13241 -(defun proof-only-whitespace-to-locked-region-p 379,13391 -(defun proof-in-locked-region-p 389,13718 -(defun proof-goto-end-of-locked 401,13975 -(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 418,14734 -(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 429,15215 -(defun proof-end-of-locked-visible-p 443,15828 -(defvar pg-idioms 461,16446 -(defvar pg-visibility-specs 464,16542 -(defconst pg-default-invisibility-spec469,16749 -(defun pg-clear-script-portions 472,16818 -(defun pg-remove-script-element 479,17092 -(defsubst pg-visname 484,17281 -(defun pg-add-element 488,17426 -(defun pg-open-invisible-span 524,19119 -(defun pg-remove-element 535,19482 -(defun pg-make-element-invisible 542,19752 -(defun pg-make-element-visible 548,19996 -(defun pg-toggle-element-visibility 552,20139 -(defun pg-redisplay-for-gnuemacs 559,20426 -(defun pg-show-all-portions 563,20573 -(defun pg-show-all-proofs 583,21291 -(defun pg-hide-all-proofs 588,21419 -(defun pg-add-proof-element 593,21550 -(defun pg-span-name 607,22208 -(defvar pg-span-context-menu-keymap628,22908 -(defun pg-last-output-displayform 635,23146 -(defun pg-set-span-helphighlights 650,23709 -(defun proof-complete-buffer-atomic 690,25153 -(defun proof-register-possibly-new-processed-file732,27073 -(defun proof-inform-prover-file-retracted 778,28910 -(defun proof-auto-retract-dependencies 798,29761 -(defun proof-unregister-buffer-file-name 852,32311 -(defun proof-protected-process-or-retract 898,34136 -(defun proof-deactivate-scripting-auto 925,35306 -(defun proof-deactivate-scripting 934,35664 -(defun proof-activate-scripting 1067,40920 -(defun proof-toggle-active-scripting 1182,46038 -(defun proof-done-advancing 1221,47283 -(defun proof-done-advancing-comment 1300,50268 -(defun proof-done-advancing-save 1334,51644 -(defun proof-make-goalsave 1419,54856 -(defun proof-get-name-from-goal 1437,55688 -(defun proof-done-advancing-autosave 1457,56713 -(defun proof-done-advancing-other 1522,59257 -(defun proof-segment-up-to-parser 1550,60210 -(defun proof-script-generic-parse-find-comment-end 1614,62293 -(defun proof-script-generic-parse-cmdend 1623,62707 -(defun proof-script-generic-parse-cmdstart 1648,63594 -(defun proof-script-generic-parse-sexp 1711,66287 -(defun proof-cmdstart-add-segment-for-cmd 1735,67219 -(defun proof-segment-up-to-cmdstart 1787,69432 -(defun proof-segment-up-to-cmdend 1848,71792 -(defun proof-semis-to-vanillas 1920,74471 -(defun proof-assert-until-point 1952,75570 -(defun proof-assert-semis 1967,76163 -(defun proof-retract-before-change 1975,76508 -(defun proof-inside-comment 1984,76826 -(defun proof-insert-pbp-command 1998,77061 -(defun proof-insert-sendback-command 2012,77540 -(defun proof-done-retracting 2038,78443 -(defun proof-setup-retract-action 2073,79884 -(defun proof-last-goal-or-goalsave 2083,80367 -(defun proof-retract-target 2107,81272 -(defun proof-retract-until-point-interactive 2188,84642 -(defun proof-retract-until-point 2196,85027 -(define-derived-mode proof-mode 2243,86862 -(defun proof-script-set-visited-file-name 2280,88230 -(defun proof-script-set-buffer-hooks 2302,89243 -(defun proof-script-kill-buffer-fn 2310,89661 -(defun proof-config-done-related 2342,90978 -(defun proof-generic-goal-command-p 2410,93501 -(defun proof-generic-state-preserving-p 2415,93714 -(defun proof-generic-count-undos 2424,94231 -(defun proof-generic-find-and-forget 2453,95269 -(defconst proof-script-important-settings2506,97108 -(defun proof-config-done 2521,97654 -(defun proof-setup-parsing-mechanism 2589,99932 -(defun proof-setup-imenu 2633,101785 -(deflocal proof-segment-up-to-cache 2657,102559 -(deflocal proof-segment-up-to-cache-start 2658,102600 -(deflocal proof-last-edited-low-watermark 2659,102645 -(defun proof-segment-up-to-using-cache 2669,103132 -(defun proof-segment-cache-contents-for 2698,104280 -(defun proof-script-after-change-function 2710,104649 -(defun proof-script-set-after-change-functions 2722,105156 - -generic/proof-shell.el,3834 +(defun proof-span-read-only 137,4788 +(defun proof-strict-read-only 146,5161 +(defsubst proof-set-queue-endpoints 156,5539 +(defun proof-set-overlay-arrow 160,5680 +(defsubst proof-set-locked-endpoints 171,6018 +(defsubst proof-detach-queue 176,6194 +(defsubst proof-detach-locked 181,6333 +(defsubst proof-set-queue-start 188,6558 +(defsubst proof-set-locked-end 192,6684 +(defsubst proof-set-queue-end 204,7154 +(defun proof-init-segmentation 215,7451 +(defun proof-colour-locked 248,8913 +(defun proof-restart-buffers 259,9345 +(defun proof-script-buffers-with-spans 281,10164 +(defun proof-script-remove-all-spans-and-deactivate 291,10520 +(defun proof-script-clear-queue-spans-on-error 295,10710 +(defun proof-script-delete-spans 311,11287 +(defun proof-script-delete-secondary-spans 316,11486 +(defun proof-unprocessed-begin 328,11774 +(defun proof-script-end 336,12028 +(defun proof-queue-or-locked-end 345,12331 +(defun proof-locked-end 360,13009 +(defun proof-locked-region-full-p 374,13290 +(defun proof-locked-region-empty-p 383,13562 +(defun proof-only-whitespace-to-locked-region-p 387,13712 +(defun proof-in-locked-region-p 397,14039 +(defun proof-goto-end-of-locked 409,14296 +(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 426,15055 +(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 437,15536 +(defun proof-end-of-locked-visible-p 451,16149 +(defvar pg-idioms 469,16767 +(defvar pg-visibility-specs 472,16863 +(defconst pg-default-invisibility-spec477,17070 +(defun pg-clear-script-portions 480,17139 +(defun pg-remove-script-element 487,17413 +(defsubst pg-visname 492,17602 +(defun pg-add-element 496,17747 +(defun pg-open-invisible-span 532,19440 +(defun pg-remove-element 543,19803 +(defun pg-make-element-invisible 550,20073 +(defun pg-make-element-visible 556,20317 +(defun pg-toggle-element-visibility 560,20460 +(defun pg-redisplay-for-gnuemacs 567,20747 +(defun pg-show-all-portions 571,20894 +(defun pg-show-all-proofs 591,21612 +(defun pg-hide-all-proofs 596,21740 +(defun pg-add-proof-element 601,21871 +(defun pg-span-name 616,22592 +(defvar pg-span-context-menu-keymap637,23292 +(defun pg-last-output-displayform 644,23530 +(defun pg-set-span-helphighlights 659,24093 +(defun proof-complete-buffer-atomic 706,25796 +(defun proof-register-possibly-new-processed-file748,27716 +(defun proof-inform-prover-file-retracted 794,29553 +(defun proof-auto-retract-dependencies 814,30404 +(defun proof-unregister-buffer-file-name 868,32954 +(defun proof-protected-process-or-retract 914,34779 +(defun proof-deactivate-scripting-auto 941,35949 +(defun proof-deactivate-scripting 950,36307 +(defun proof-activate-scripting 1083,41563 +(defun proof-toggle-active-scripting 1198,46681 +(defun proof-done-advancing 1237,47926 +(defun proof-done-advancing-comment 1316,50911 +(defun proof-done-advancing-save 1350,52287 +(defun proof-make-goalsave 1438,55652 +(defun proof-get-name-from-goal 1456,56484 +(defun proof-done-advancing-autosave 1476,57509 +(defun proof-done-advancing-other 1541,60053 +(defun proof-segment-up-to-parser 1569,61006 +(defun proof-script-generic-parse-find-comment-end 1639,63281 +(defun proof-script-generic-parse-cmdend 1648,63695 +(defun proof-script-generic-parse-cmdstart 1673,64582 +(defun proof-script-generic-parse-sexp 1736,67275 +(defun proof-cmdstart-add-segment-for-cmd 1760,68207 +(defun proof-segment-up-to-cmdstart 1812,70420 +(defun proof-segment-up-to-cmdend 1873,72780 +(defun proof-semis-to-vanillas 1945,75459 +(defun proof-script-next-command-advance 1994,76981 +(defun proof-assert-until-point 2013,77480 +(defun proof-assert-electric-terminator 2028,78073 +(defun proof-assert-semis 2062,79415 +(defun proof-retract-before-change 2075,80054 +(defun proof-inside-comment 2084,80372 +(defun proof-insert-pbp-command 2099,80655 +(defun proof-insert-sendback-command 2114,81149 +(defun proof-done-retracting 2140,82052 +(defun proof-setup-retract-action 2175,83493 +(defun proof-last-goal-or-goalsave 2185,83979 +(defun proof-retract-target 2209,84884 +(defun proof-retract-until-point-interactive 2292,88398 +(defun proof-retract-until-point 2300,88783 +(define-derived-mode proof-mode 2347,90618 +(defun proof-script-set-visited-file-name 2384,91986 +(defun proof-script-set-buffer-hooks 2406,92999 +(defun proof-script-kill-buffer-fn 2414,93417 +(defun proof-config-done-related 2446,94734 +(defun proof-generic-goal-command-p 2514,97257 +(defun proof-generic-state-preserving-p 2519,97470 +(defun proof-generic-count-undos 2528,97987 +(defun proof-generic-find-and-forget 2557,99025 +(defconst proof-script-important-settings2610,100864 +(defun proof-config-done 2625,101410 +(defun proof-setup-parsing-mechanism 2693,103688 +(defun proof-setup-imenu 2737,105541 +(deflocal proof-segment-up-to-cache 2761,106315 +(deflocal proof-segment-up-to-cache-start 2762,106356 +(deflocal proof-last-edited-low-watermark 2763,106401 +(defun proof-segment-up-to-using-cache 2773,106888 +(defun proof-segment-cache-contents-for 2802,108036 +(defun proof-script-after-change-function 2814,108405 +(defun proof-script-set-after-change-functions 2826,108912 + +generic/proof-shell.el,3745 (defvar proof-marker 35,808 (defvar proof-action-list 38,904 -(defvar proof-shell-last-goals-output 63,1842 -(defvar proof-shell-last-response-output 66,1922 -(defvar proof-shell-delayed-output-start 69,2009 -(defvar proof-shell-delayed-output-end 73,2191 -(defvar proof-shell-delayed-output-flags 77,2371 -(defcustom proof-shell-active-scripting-indicator86,2567 -(defun proof-shell-ready-prover 134,3881 -(defsubst proof-shell-live-buffer 148,4420 -(defun proof-shell-available-p 155,4659 -(defun proof-grab-lock 161,4881 -(defun proof-release-lock 172,5379 -(defcustom proof-shell-fiddle-frames 184,5599 -(defun proof-shell-set-text-representation 190,5821 -(defun proof-shell-start 201,6282 -(defvar proof-shell-kill-function-hooks 386,12548 -(defun proof-shell-kill-function 389,12646 -(defun proof-shell-clear-state 478,16450 -(defun proof-shell-exit 493,16893 -(defun proof-shell-bail-out 505,17338 -(defun proof-shell-restart 514,17815 -(defvar proof-shell-urgent-message-marker 556,19193 -(defvar proof-shell-urgent-message-scanner 559,19314 -(defun proof-shell-handle-error-output 562,19440 -(defsubst proof-shell-strip-output-markup 583,20202 -(defun proof-shell-handle-error-or-interrupt 596,20568 -(defun proof-shell-error-or-interrupt-action 632,22037 -(defun proof-goals-pos 654,22816 -(defun proof-pbp-focus-on-first-goal 659,23027 -(defsubst proof-shell-string-match-safe 671,23443 -(defun proof-shell-handle-immediate-output 675,23604 -(defvar proof-shell-expecting-output 742,26168 -(defvar proof-shell-interrupt-pending 746,26327 -(defun proof-interrupt-process 751,26551 -(defun proof-shell-insert 789,27984 -(defun proof-shell-action-list-item 840,29727 -(defun proof-shell-set-silent 846,29972 -(defun proof-shell-start-silent-item 852,30191 -(defun proof-shell-clear-silent 858,30380 -(defun proof-shell-stop-silent-item 864,30602 -(defun proof-shell-should-be-silent 871,30871 -(defsubst proof-shell-invoke-callback 885,31458 -(defsubst proof-shell-insert-action-item 891,31668 -(defun proof-append-alist 895,31843 -(defun proof-start-queue 953,33968 -(defun proof-extend-queue 964,34317 -(defun proof-shell-exec-loop 973,34696 -(defun proof-shell-insert-loopback-cmd 1050,37302 -(defun proof-shell-process-urgent-message 1075,38448 -(defun proof-shell-process-urgent-message-default 1124,40169 -(defun proof-shell-process-urgent-message-trace 1141,40801 -(defun proof-shell-process-urgent-message-retract 1154,41361 -(defun proof-shell-process-urgent-message-elisp 1175,42209 -(defun proof-shell-process-urgent-message-thmdeps 1190,42704 -(defun proof-shell-message 1204,43084 -(defun proof-shell-strip-eager-annotations 1211,43336 -(defvar proof-shell-minibuffer-urgent-interactive-input-history 1226,43869 -(defun proof-shell-minibuffer-urgent-interactive-input 1228,43939 -(defun proof-shell-filter 1244,44406 -(defun proof-shell-filter-first-command 1345,47815 -(defun proof-shell-process-urgent-messages 1360,48358 -(defun proof-shell-filter-manage-output 1427,50823 -(defsubst proof-shell-display-output-as-response 1460,52126 -(defun proof-shell-handle-delayed-output 1466,52418 -(defvar pg-last-tracing-output-time 1563,55885 -(defconst pg-slow-mode-duration 1566,55991 -(defconst pg-fast-tracing-mode-threshold 1569,56073 -(defvar pg-tracing-cleanup-timer 1572,56201 -(defun pg-tracing-tight-loop 1574,56240 -(defun pg-finish-tracing-display 1617,57952 -(defun proof-shell-wait 1635,58316 -(defun proof-done-invisible 1654,59224 -(defun proof-shell-invisible-command 1660,59394 -(defun proof-shell-invisible-cmd-get-result 1707,60938 -(defun proof-shell-invisible-command-invisible-result 1719,61374 -(defun pg-insert-last-output-as-comment 1739,61875 -(define-derived-mode proof-shell-mode 1758,62347 -(defconst proof-shell-important-settings1800,63740 -(defun proof-shell-config-done 1806,63855 +(defvar proof-shell-last-goals-output 63,1832 +(defvar proof-shell-last-response-output 66,1912 +(defvar proof-shell-delayed-output-start 69,1999 +(defvar proof-shell-delayed-output-end 73,2181 +(defvar proof-shell-delayed-output-flags 77,2361 +(defcustom proof-shell-active-scripting-indicator86,2557 +(defun proof-shell-ready-prover 134,3909 +(defsubst proof-shell-live-buffer 148,4448 +(defun proof-shell-available-p 155,4687 +(defun proof-grab-lock 161,4909 +(defun proof-release-lock 172,5407 +(defcustom proof-shell-fiddle-frames 184,5627 +(defun proof-shell-set-text-representation 190,5849 +(defun proof-shell-start 201,6310 +(defvar proof-shell-kill-function-hooks 387,12598 +(defun proof-shell-kill-function 390,12696 +(defun proof-shell-clear-state 479,16500 +(defun proof-shell-exit 494,16943 +(defun proof-shell-bail-out 506,17388 +(defun proof-shell-restart 515,17865 +(defvar proof-shell-urgent-message-marker 557,19243 +(defvar proof-shell-urgent-message-scanner 560,19364 +(defun proof-shell-handle-error-output 563,19490 +(defun proof-shell-handle-error-or-interrupt 589,20352 +(defun proof-shell-error-or-interrupt-action 624,21773 +(defun proof-goals-pos 638,22301 +(defun proof-pbp-focus-on-first-goal 643,22512 +(defsubst proof-shell-string-match-safe 655,22928 +(defun proof-shell-handle-immediate-output 659,23089 +(defvar proof-shell-expecting-output 726,25671 +(defvar proof-shell-interrupt-pending 730,25830 +(defun proof-interrupt-process 735,26054 +(defun proof-shell-insert 773,27487 +(defun proof-shell-action-list-item 826,29355 +(defun proof-shell-set-silent 831,29606 +(defun proof-shell-start-silent-item 837,29825 +(defun proof-shell-clear-silent 843,30014 +(defun proof-shell-stop-silent-item 849,30236 +(defsubst proof-shell-should-be-silent 855,30425 +(defsubst proof-shell-invoke-callback 867,30928 +(defsubst proof-shell-insert-action-item 873,31138 +(defun proof-add-to-queue 877,31313 +(defun proof-start-queue 934,33535 +(defun proof-extend-queue 945,33899 +(defun proof-shell-exec-loop 954,34281 +(defun proof-shell-insert-loopback-cmd 1034,37057 +(defun proof-shell-process-urgent-message 1059,38203 +(defun proof-shell-process-urgent-message-default 1108,39924 +(defun proof-shell-process-urgent-message-trace 1124,40511 +(defun proof-shell-process-urgent-message-retract 1137,41071 +(defun proof-shell-process-urgent-message-elisp 1158,41919 +(defun proof-shell-process-urgent-message-thmdeps 1173,42414 +(defun proof-shell-strip-eager-annotations 1187,42794 +(defvar proof-shell-minibuffer-urgent-interactive-input-history 1202,43327 +(defun proof-shell-minibuffer-urgent-interactive-input 1204,43397 +(defun proof-shell-filter 1220,43871 +(defun proof-shell-filter-first-command 1321,47280 +(defun proof-shell-process-urgent-messages 1336,47823 +(defun proof-shell-filter-manage-output 1400,50123 +(defsubst proof-shell-display-output-as-response 1433,51426 +(defun proof-shell-handle-delayed-output 1439,51718 +(defvar pg-last-tracing-output-time 1534,55183 +(defconst pg-slow-mode-duration 1537,55289 +(defconst pg-fast-tracing-mode-threshold 1540,55371 +(defvar pg-tracing-cleanup-timer 1543,55499 +(defun pg-tracing-tight-loop 1545,55538 +(defun pg-finish-tracing-display 1588,57250 +(defun proof-shell-wait 1606,57614 +(defun proof-done-invisible 1625,58522 +(defun proof-shell-invisible-command 1631,58692 +(defun proof-shell-invisible-cmd-get-result 1678,60236 +(defun proof-shell-invisible-command-invisible-result 1690,60672 +(defun pg-insert-last-output-as-comment 1710,61173 +(define-derived-mode proof-shell-mode 1729,61645 +(defconst proof-shell-important-settings1766,62676 +(defun proof-shell-config-done 1772,62791 generic/proof-site.el,503 (defconst proof-assistant-table-default22,725 @@ -1826,91 +1856,93 @@ generic/proof-unicode-tokens.el,497 (defun proof-unicode-tokens-deactivate-prover 138,4803 generic/proof-useropts.el,1510 -(defgroup proof-user-options 21,552 -(defun proof-set-value 29,731 -(defcustom proof-electric-terminator-enable 62,1854 -(defcustom proof-toolbar-enable 74,2386 -(defcustom proof-imenu-enable 80,2559 -(defcustom pg-show-hints 86,2730 -(defcustom proof-shell-quiet-errors 91,2863 -(defcustom proof-trace-output-slow-catchup 98,3136 -(defcustom proof-strict-state-preserving 108,3633 -(defcustom proof-strict-read-only 121,4242 -(defcustom proof-allow-undo-in-read-only 133,4752 -(defcustom proof-three-window-enable 140,5034 -(defcustom proof-multiple-frames-enable 159,5784 -(defcustom proof-delete-empty-windows 168,6117 -(defcustom proof-shrink-windows-tofit 179,6648 -(defcustom proof-auto-raise-buffers 186,6920 -(defcustom proof-colour-locked 193,7155 -(defcustom proof-query-file-save-when-activating-scripting201,7405 -(defcustom proof-one-command-per-line217,8125 -(defcustom proof-prog-name-ask224,8349 -(defcustom proof-prog-name-guess230,8509 -(defcustom proof-tidy-response238,8774 -(defcustom proof-keep-response-history252,9237 -(defcustom pg-input-ring-size 262,9625 -(defcustom proof-general-debug 267,9777 -(defcustom proof-use-parser-cache 278,10186 -(defcustom proof-follow-mode 288,10483 -(defcustom proof-auto-action-when-deactivating-scripting 312,11660 -(defcustom proof-script-command-separator 335,12609 -(defcustom proof-rsh-command 343,12901 -(defcustom proof-disappearing-proofs 359,13451 -(defcustom proof-full-annotation 364,13612 -(defcustom proof-minibuffer-messages 373,13984 - -generic/proof-utils.el,1938 -(defmacro deflocal 65,1980 -(defmacro proof-with-current-buffer-if-exists 72,2218 -(deflocal proof-buffer-type 78,2428 -(defmacro proof-with-script-buffer 84,2708 -(defmacro proof-map-buffers 95,3089 -(defmacro proof-sym 100,3274 -(defsubst proof-try-require 105,3435 -(defun proof-save-some-buffers 118,3766 -(defmacro proof-ass-sym 167,5367 -(defmacro proof-ass-symv 173,5626 -(defmacro proof-ass 179,5884 -(defun proof-defpgcustom-fn 185,6136 -(defun undefpgcustom 206,7006 -(defmacro defpgcustom 212,7230 -(defun proof-defpgdefault-fn 223,7641 -(defmacro defpgdefault 237,8099 -(defmacro defpgfun 248,8461 -(defun proof-defpacustom-fn 262,8861 -(defmacro defpacustom 328,11142 -(defmacro proof-eval-when-ready-for-assistant 349,12089 -(defun proof-file-truename 362,12480 -(defun proof-files-to-buffers 366,12663 -(defun proof-buffers-in-mode 374,12903 -(defun pg-save-from-death 388,13353 -(defun proof-define-keys 407,13970 -(defun pg-remove-specials 418,14255 -(defun pg-remove-specials-in-string 428,14591 -(defun proof-warn-if-unset 439,14817 -(defun proof-get-window-for-buffer 444,15035 -(defun proof-display-and-keep-buffer 495,17343 -(defun proof-clean-buffer 537,19066 -(defun pg-internal-warning 553,19722 -(defun proof-debug 560,19989 -(defun proof-switch-to-buffer 568,20338 -(defun proof-resize-window-tofit 590,21462 -(defun proof-submit-bug-report 684,25308 -(defun proof-deftoggle-fn 719,26665 -(defmacro proof-deftoggle 734,27318 -(defun proof-defintset-fn 741,27692 -(defmacro proof-defintset 757,28396 -(defun proof-defstringset-fn 764,28773 -(defmacro proof-defstringset 777,29399 -(defun proof-escape-keymap-doc 790,29855 -(defmacro proof-defshortcut 794,29995 -(defmacro proof-definvisible 809,30593 -(defun pg-custom-save-vars 836,31520 -(defun pg-custom-reset-vars 852,32164 -(defun proof-locate-executable 865,32501 -(defun pg-current-word-pos 880,33056 -(defun proof-looking-at-syntactic-context 927,34772 +(defgroup proof-user-options 21,553 +(defun proof-set-value 29,732 +(defcustom proof-electric-terminator-enable 62,1855 +(defcustom proof-toolbar-enable 74,2387 +(defcustom proof-imenu-enable 80,2560 +(defcustom pg-show-hints 86,2731 +(defcustom proof-shell-quiet-errors 91,2864 +(defcustom proof-trace-output-slow-catchup 98,3135 +(defcustom proof-strict-state-preserving 108,3632 +(defcustom proof-strict-read-only 121,4241 +(defcustom proof-allow-undo-in-read-only 134,4820 +(defcustom proof-three-window-enable 141,5102 +(defcustom proof-multiple-frames-enable 160,5852 +(defcustom proof-delete-empty-windows 169,6185 +(defcustom proof-shrink-windows-tofit 180,6716 +(defcustom proof-auto-raise-buffers 187,6988 +(defcustom proof-colour-locked 194,7223 +(defcustom proof-query-file-save-when-activating-scripting202,7473 +(defcustom proof-one-command-per-line218,8193 +(defcustom proof-prog-name-ask225,8417 +(defcustom proof-prog-name-guess231,8577 +(defcustom proof-tidy-response239,8842 +(defcustom proof-keep-response-history253,9305 +(defcustom pg-input-ring-size 263,9693 +(defcustom proof-general-debug 268,9845 +(defcustom proof-use-parser-cache 279,10254 +(defcustom proof-follow-mode 289,10551 +(defcustom proof-auto-action-when-deactivating-scripting 313,11728 +(defcustom proof-script-command-separator 336,12677 +(defcustom proof-rsh-command 344,12969 +(defcustom proof-disappearing-proofs 360,13519 +(defcustom proof-full-annotation 365,13680 +(defcustom proof-minibuffer-messages 374,14052 + +generic/proof-utils.el,2033 +(defmacro deflocal 61,1871 +(defmacro proof-with-current-buffer-if-exists 68,2109 +(deflocal proof-buffer-type 74,2319 +(defmacro proof-with-script-buffer 80,2599 +(defmacro proof-map-buffers 91,2980 +(defmacro proof-sym 96,3165 +(defsubst proof-try-require 101,3326 +(defun proof-save-some-buffers 114,3657 +(defmacro proof-ass-sym 163,5258 +(defmacro proof-ass-symv 169,5517 +(defmacro proof-ass 175,5775 +(defun proof-defpgcustom-fn 181,6027 +(defun undefpgcustom 202,6897 +(defmacro defpgcustom 208,7121 +(defun proof-defpgdefault-fn 219,7532 +(defmacro defpgdefault 233,7990 +(defmacro defpgfun 244,8352 +(defun proof-defpacustom-fn 258,8752 +(defmacro defpacustom 324,11033 +(defmacro proof-eval-when-ready-for-assistant 345,11980 +(defun proof-file-truename 358,12371 +(defun proof-files-to-buffers 362,12554 +(defun proof-buffers-in-mode 370,12794 +(defun pg-save-from-death 384,13244 +(defun proof-define-keys 403,13861 +(defun pg-remove-specials 414,14146 +(defun pg-remove-specials-in-string 424,14482 +(defun proof-warn-if-unset 435,14708 +(defun proof-get-window-for-buffer 440,14926 +(defun proof-display-and-keep-buffer 491,17234 +(defun proof-clean-buffer 533,18957 +(defun pg-internal-warning 549,19613 +(defun proof-debug 556,19880 +(defun proof-switch-to-buffer 566,20252 +(defun proof-resize-window-tofit 588,21376 +(defun proof-submit-bug-report 683,25224 +(defun proof-deftoggle-fn 718,26581 +(defmacro proof-deftoggle 733,27234 +(defun proof-defintset-fn 740,27608 +(defmacro proof-defintset 756,28312 +(defun proof-defstringset-fn 763,28689 +(defmacro proof-defstringset 776,29315 +(defun proof-escape-keymap-doc 789,29771 +(defmacro proof-defshortcut 793,29911 +(defmacro proof-definvisible 808,30509 +(defun pg-custom-save-vars 835,31436 +(defun pg-custom-reset-vars 851,32080 +(defun proof-locate-executable 864,32417 +(defun pg-current-word-pos 879,32972 +(defun proof-looking-at-syntactic-context 926,34688 +(defsubst proof-shell-strip-output-markup 941,35257 +(defun proof-minibuffer-message 947,35521 lib/bufhist.el,1106 (defun bufhist-ring-update 36,1305 @@ -2023,11 +2055,12 @@ lib/maths-menu.el,242 (defvar maths-menu-mode-map344,12882 (define-minor-mode maths-menu-mode352,13101 -lib/pg-dev.el,138 -(defconst pg-dev-lisp-font-lock-keywords52,1591 -(defun unload-pg 79,2385 -(defun profile-pg 107,3248 -(defun pg-bug-references 124,3674 +lib/pg-dev.el,166 +(defconst pg-dev-lisp-font-lock-keywords52,1582 +(defun pg-loadpath 80,2416 +(defun unload-pg 90,2587 +(defun profile-pg 118,3450 +(defun pg-bug-references 139,4117 lib/pg-fontsets.el,210 (defcustom pg-fontsets-default-fontset 28,780 @@ -2068,7 +2101,7 @@ lib/scomint.el,876 (defun scomint-output-filter 288,11418 (defun scomint-interrupt-process 360,14150 -lib/span.el,1354 +lib/span.el,1315 (defalias 'span-start span-start22,609 (defalias 'span-end span-end23,647 (defalias 'span-set-property span-set-property24,681 @@ -2080,32 +2113,31 @@ lib/span.el,1354 (defun span-read-only-hook 31,925 (defsubst span-read-only 36,1115 (defsubst span-read-write 43,1425 -(defsubst span-give-warning 48,1595 -(defsubst span-write-warning 53,1741 -(defsubst span-lt 65,2307 -(defsubst spans-at-point-prop 70,2451 -(defsubst spans-at-region-prop 79,2642 -(defsubst span-at 89,2908 -(defsubst span-delete 93,3034 -(defsubst span-mapcar-spans 100,3256 -(defsubst span-mapc-spans 104,3431 -(defun span-at-before 108,3602 -(defsubst prev-span 125,4326 -(defsubst next-span 131,4479 -(defsubst span-live-p 137,4693 -(defsubst span-raise 143,4859 -(defsubst span-string 147,4992 -(defsubst set-span-properties 152,5152 -(defsubst span-find-span 158,5346 -(defsubst span-at-event 166,5658 -(defun fold-spans 172,5855 -(defsubst span-detached-p 186,6388 -(defsubst set-span-face 190,6504 -(defsubst set-span-keymap 194,6602 -(defsubst span-delete-spans 202,6771 -(defsubst span-property-safe 206,6933 -(defsubst span-set-start 210,7070 -(defsubst span-set-end 214,7202 +(defsubst span-write-warning 48,1595 +(defsubst span-lt 59,2119 +(defsubst spans-at-point-prop 64,2263 +(defsubst spans-at-region-prop 73,2454 +(defsubst span-at 83,2720 +(defsubst span-delete 87,2846 +(defsubst span-mapcar-spans 94,3068 +(defsubst span-mapc-spans 98,3243 +(defun span-at-before 102,3414 +(defsubst prev-span 119,4138 +(defsubst next-span 125,4291 +(defsubst span-live-p 131,4505 +(defsubst span-raise 137,4671 +(defsubst span-string 141,4804 +(defsubst set-span-properties 146,4964 +(defsubst span-find-span 152,5158 +(defsubst span-at-event 160,5470 +(defun fold-spans 166,5667 +(defsubst span-detached-p 180,6200 +(defsubst set-span-face 184,6316 +(defsubst set-span-keymap 188,6414 +(defsubst span-delete-spans 196,6583 +(defsubst span-property-safe 200,6745 +(defsubst span-set-start 204,6882 +(defsubst span-set-end 208,7014 lib/texi-docstring-magic.el,584 (defun texi-docstring-magic-find-face 88,3027 @@ -2154,79 +2186,79 @@ lib/unicode-tokens.el,5231 (defface unicode-tokens-script-font-face270,9589 (defface unicode-tokens-fraktur-font-face275,9733 (defface unicode-tokens-serif-font-face280,9858 -(defface unicode-tokens-sans-font-face285,9985 -(defface unicode-tokens-highlight-face290,10107 -(defconst unicode-tokens-fonts299,10469 -(defconst unicode-tokens-fontsymb-properties308,10686 -(define-widget 'unicode-tokens-token-symbol-map unicode-tokens-token-symbol-map334,12132 -(define-widget 'unicode-tokens-shortcut-alist unicode-tokens-shortcut-alist352,12684 -(defconst unicode-tokens-font-lock-extra-managed-props365,13015 -(defun unicode-tokens-font-lock-keywords 369,13169 -(defun unicode-tokens-calculate-token-match 402,14540 -(defun unicode-tokens-usable-composition 432,15578 -(defun unicode-tokens-help-echo 445,15957 -(defvar unicode-tokens-show-symbols 449,16121 -(defun unicode-tokens-interpret-composition 452,16235 -(defun unicode-tokens-font-lock-compose-symbol 470,16747 -(defun unicode-tokens-prepend-text-properties-in-match 500,17994 -(defun unicode-tokens-prepend-text-property 514,18572 -(defun unicode-tokens-show-symbols 539,19717 -(defun unicode-tokens-symbs-to-props 547,20027 -(defvar unicode-tokens-show-controls 567,20726 -(defun unicode-tokens-show-controls 570,20817 -(defun unicode-tokens-control-char 583,21402 -(defun unicode-tokens-control-region 592,21841 -(defun unicode-tokens-control-font-lock-keywords 603,22388 -(defvar unicode-tokens-use-shortcuts 614,22712 -(defun unicode-tokens-use-shortcuts 617,22815 -(defun unicode-tokens-map-ordering 635,23421 -(defun unicode-tokens-quail-define-rules 644,23774 -(defun unicode-tokens-insert-token 667,24451 -(defun unicode-tokens-annotate-region 676,24755 -(defun unicode-tokens-insert-control 700,25593 -(defun unicode-tokens-insert-uchar-as-token 710,26042 -(defun unicode-tokens-delete-token-near-point 716,26263 -(defun unicode-tokens-prev-token 730,26825 -(defun unicode-tokens-rotate-token-forward 738,27122 -(defun unicode-tokens-rotate-token-backward 765,28012 -(defun unicode-tokens-replace-shortcut-match 770,28214 -(defun unicode-tokens-replace-shortcuts 779,28584 -(defun unicode-tokens-replace-unicode-match 793,29182 -(defun unicode-tokens-replace-unicode 800,29483 -(defun unicode-tokens-copy-token 817,30082 -(define-button-type 'unicode-tokens-listunicode-tokens-list824,30303 -(defun unicode-tokens-list-tokens 830,30507 -(defun unicode-tokens-list-shortcuts 869,31691 -(defalias 'unicode-tokens-list-unicode-chars unicode-tokens-list-unicode-chars887,32329 -(defun unicode-tokens-encode-in-temp-buffer 889,32402 -(defun unicode-tokens-encode 907,33058 -(defun unicode-tokens-encode-str 913,33294 -(defun unicode-tokens-copy 917,33456 -(defun unicode-tokens-paste 926,33862 -(defvar unicode-tokens-highlight-unicode 945,34583 -(defconst unicode-tokens-unicode-highlight-patterns948,34675 -(defun unicode-tokens-highlight-unicode 952,34844 -(defun unicode-tokens-highlight-unicode-setkeywords 964,35307 -(defun unicode-tokens-initialise 976,35676 -(defvar unicode-tokens-mode-map 996,36347 -(define-minor-mode unicode-tokens-mode999,36444 -(defun unicode-tokens-set-font-var 1126,40688 -(defun unicode-tokens-set-font-var-aux 1142,41179 -(defun unicode-tokens-mouse-set-font 1167,42221 -(defsubst unicode-tokens-face-font-sym 1180,42735 -(defun unicode-tokens-set-font-restart 1184,42915 -(defun unicode-tokens-save-fonts 1195,43225 -(defun unicode-tokens-custom-save-faces 1203,43481 -(define-key unicode-tokens-mode-map 1220,43937 -(define-key unicode-tokens-mode-map 1222,44029 -(define-key unicode-tokens-mode-map1224,44120 -(define-key unicode-tokens-mode-map1226,44226 -(define-key unicode-tokens-mode-map1229,44341 -(define-key unicode-tokens-mode-map1231,44450 -(define-key unicode-tokens-mode-map1233,44558 -(define-key unicode-tokens-mode-map1235,44664 -(defun unicode-tokens-customize-submenu 1243,44788 -(defun unicode-tokens-define-menu 1250,45011 +(defface unicode-tokens-sans-font-face285,9995 +(defface unicode-tokens-highlight-face290,10117 +(defconst unicode-tokens-fonts299,10479 +(defconst unicode-tokens-fontsymb-properties308,10696 +(define-widget 'unicode-tokens-token-symbol-map unicode-tokens-token-symbol-map334,12142 +(define-widget 'unicode-tokens-shortcut-alist unicode-tokens-shortcut-alist352,12694 +(defconst unicode-tokens-font-lock-extra-managed-props365,13025 +(defun unicode-tokens-font-lock-keywords 369,13179 +(defun unicode-tokens-calculate-token-match 402,14550 +(defun unicode-tokens-usable-composition 432,15588 +(defun unicode-tokens-help-echo 445,15967 +(defvar unicode-tokens-show-symbols 449,16131 +(defun unicode-tokens-interpret-composition 452,16245 +(defun unicode-tokens-font-lock-compose-symbol 470,16757 +(defun unicode-tokens-prepend-text-properties-in-match 500,18004 +(defun unicode-tokens-prepend-text-property 514,18582 +(defun unicode-tokens-show-symbols 539,19727 +(defun unicode-tokens-symbs-to-props 547,20037 +(defvar unicode-tokens-show-controls 567,20736 +(defun unicode-tokens-show-controls 570,20827 +(defun unicode-tokens-control-char 583,21412 +(defun unicode-tokens-control-region 592,21851 +(defun unicode-tokens-control-font-lock-keywords 603,22398 +(defvar unicode-tokens-use-shortcuts 614,22722 +(defun unicode-tokens-use-shortcuts 617,22825 +(defun unicode-tokens-map-ordering 635,23431 +(defun unicode-tokens-quail-define-rules 644,23784 +(defun unicode-tokens-insert-token 667,24461 +(defun unicode-tokens-annotate-region 676,24765 +(defun unicode-tokens-insert-control 700,25603 +(defun unicode-tokens-insert-uchar-as-token 710,26052 +(defun unicode-tokens-delete-token-near-point 716,26273 +(defun unicode-tokens-prev-token 730,26835 +(defun unicode-tokens-rotate-token-forward 738,27132 +(defun unicode-tokens-rotate-token-backward 765,28022 +(defun unicode-tokens-replace-shortcut-match 770,28224 +(defun unicode-tokens-replace-shortcuts 779,28594 +(defun unicode-tokens-replace-unicode-match 793,29192 +(defun unicode-tokens-replace-unicode 800,29493 +(defun unicode-tokens-copy-token 817,30092 +(define-button-type 'unicode-tokens-listunicode-tokens-list824,30313 +(defun unicode-tokens-list-tokens 830,30517 +(defun unicode-tokens-list-shortcuts 869,31701 +(defalias 'unicode-tokens-list-unicode-chars unicode-tokens-list-unicode-chars887,32339 +(defun unicode-tokens-encode-in-temp-buffer 889,32412 +(defun unicode-tokens-encode 907,33068 +(defun unicode-tokens-encode-str 913,33304 +(defun unicode-tokens-copy 917,33466 +(defun unicode-tokens-paste 926,33872 +(defvar unicode-tokens-highlight-unicode 945,34593 +(defconst unicode-tokens-unicode-highlight-patterns948,34685 +(defun unicode-tokens-highlight-unicode 952,34854 +(defun unicode-tokens-highlight-unicode-setkeywords 964,35317 +(defun unicode-tokens-initialise 976,35686 +(defvar unicode-tokens-mode-map 996,36357 +(define-minor-mode unicode-tokens-mode999,36454 +(defun unicode-tokens-set-font-var 1126,40698 +(defun unicode-tokens-set-font-var-aux 1142,41189 +(defun unicode-tokens-mouse-set-font 1167,42231 +(defsubst unicode-tokens-face-font-sym 1180,42745 +(defun unicode-tokens-set-font-restart 1184,42925 +(defun unicode-tokens-save-fonts 1195,43235 +(defun unicode-tokens-custom-save-faces 1203,43491 +(define-key unicode-tokens-mode-map 1220,43947 +(define-key unicode-tokens-mode-map 1222,44039 +(define-key unicode-tokens-mode-map1224,44130 +(define-key unicode-tokens-mode-map1226,44236 +(define-key unicode-tokens-mode-map1229,44351 +(define-key unicode-tokens-mode-map1231,44460 +(define-key unicode-tokens-mode-map1233,44568 +(define-key unicode-tokens-mode-map1235,44674 +(defun unicode-tokens-customize-submenu 1243,44798 +(defun unicode-tokens-define-menu 1250,45021 mmm/mmm-auto.el,343 (defvar mmm-autoloaded-classes67,2676 @@ -2583,49 +2615,49 @@ doc/PG-adapting.texi,3772 @node Proof Script SettingsProof Script Settings651,25120 @node Recognizing commands and commentsRecognizing commands and comments673,25700 @node Recognizing proofsRecognizing proofs810,32137 -@node Recognizing other elementsRecognizing other elements919,36812 -@node Configuring undo behaviourConfiguring undo behaviour1045,42344 -@node Nested proofsNested proofs1182,47733 -@node Safe (state-preserving) commandsSafe (state-preserving) commands1222,49359 -@node Activate scripting hookActivate scripting hook1245,50312 -@node Automatic multiple filesAutomatic multiple files1269,51182 -@node Completions1291,52029 -@node Proof Shell SettingsProof Shell Settings1332,53519 -@node Proof shell commandsProof shell commands1363,54801 -@node Script input to the shellScript input to the shell1527,61845 -@node Settings for matching various output from proof processSettings for matching various output from proof process1592,64803 -@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process1706,69781 -@node Hooks and other settingsHooks and other settings1921,79658 -@node Goals Buffer SettingsGoals Buffer Settings2002,83045 -@node Splash Screen SettingsSplash Screen Settings2079,86151 -@node Global ConstantsGlobal Constants2105,86906 -@node Handling Multiple FilesHandling Multiple Files2131,87747 -@node Configuring Editing SyntaxConfiguring Editing Syntax2283,95530 -@node Configuring Font LockConfiguring Font Lock2340,97647 -@node Configuring TokensConfiguring Tokens2412,101141 -@node Writing More Lisp CodeWriting More Lisp Code2462,103261 -@node Default values for generic settingsDefault values for generic settings2479,103906 -@node Adding prover-specific configurationsAdding prover-specific configurations2509,104989 -@node Useful variablesUseful variables2552,106271 -@node Useful functions and macrosUseful functions and macros2567,106770 -@node Internals of Proof GeneralInternals of Proof General2676,110993 -@node Spans2704,111889 -@node Proof General site configurationProof General site configuration2716,112211 -@node Configuration variable mechanismsConfiguration variable mechanisms2796,115256 -@node Global variablesGlobal variables2917,120700 -@node Proof script modeProof script mode2987,123248 -@node Proof shell modeProof shell mode3225,133855 -@node Debugging3661,151085 -@node Plans and IdeasPlans and Ideas3704,151961 -@node Proof by pointing and similar featuresProof by pointing and similar features3725,152683 -@node Granularity of atomic command sequencesGranularity of atomic command sequences3763,154341 -@node Browser mode for script files and theoriesBrowser mode for script files and theories3808,156566 -@node Demonstration InstantiationsDemonstration Instantiations3838,157597 -@node demoisa-easy.el3854,158028 -@node demoisa.el3916,160220 -@node Function IndexFunction Index4070,165160 -@node Variable IndexVariable Index4074,165236 -@node Concept IndexConcept Index4083,165415 +@node Recognizing other elementsRecognizing other elements919,36811 +@node Configuring undo behaviourConfiguring undo behaviour1045,42343 +@node Nested proofsNested proofs1182,47732 +@node Safe (state-preserving) commandsSafe (state-preserving) commands1222,49358 +@node Activate scripting hookActivate scripting hook1245,50311 +@node Automatic multiple filesAutomatic multiple files1269,51181 +@node Completions1291,52028 +@node Proof Shell SettingsProof Shell Settings1332,53518 +@node Proof shell commandsProof shell commands1363,54800 +@node Script input to the shellScript input to the shell1527,61844 +@node Settings for matching various output from proof processSettings for matching various output from proof process1592,64802 +@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process1706,69780 +@node Hooks and other settingsHooks and other settings1921,79657 +@node Goals Buffer SettingsGoals Buffer Settings2002,83044 +@node Splash Screen SettingsSplash Screen Settings2079,86150 +@node Global ConstantsGlobal Constants2105,86905 +@node Handling Multiple FilesHandling Multiple Files2131,87746 +@node Configuring Editing SyntaxConfiguring Editing Syntax2283,95529 +@node Configuring Font LockConfiguring Font Lock2340,97646 +@node Configuring TokensConfiguring Tokens2412,101140 +@node Writing More Lisp CodeWriting More Lisp Code2462,103260 +@node Default values for generic settingsDefault values for generic settings2479,103905 +@node Adding prover-specific configurationsAdding prover-specific configurations2509,104988 +@node Useful variablesUseful variables2552,106270 +@node Useful functions and macrosUseful functions and macros2567,106769 +@node Internals of Proof GeneralInternals of Proof General2676,110992 +@node Spans2704,111888 +@node Proof General site configurationProof General site configuration2716,112210 +@node Configuration variable mechanismsConfiguration variable mechanisms2796,115255 +@node Global variablesGlobal variables2917,120699 +@node Proof script modeProof script mode2987,123247 +@node Proof shell modeProof shell mode3225,133854 +@node Debugging3661,151084 +@node Plans and IdeasPlans and Ideas3704,151960 +@node Proof by pointing and similar featuresProof by pointing and similar features3725,152682 +@node Granularity of atomic command sequencesGranularity of atomic command sequences3763,154340 +@node Browser mode for script files and theoriesBrowser mode for script files and theories3808,156565 +@node Demonstration InstantiationsDemonstration Instantiations3838,157596 +@node demoisa-easy.el3854,158027 +@node demoisa.el3916,160219 +@node Function IndexFunction Index4070,165159 +@node Variable IndexVariable Index4074,165235 +@node Concept IndexConcept Index4083,165414 generic/proof.el,0 |