coq/coq-abbrev.el,495 (defun holes-show-doc 10,310 (defun coq-local-vars-list-show-doc 14,386 (defconst coq-tactics-menu19,486 (defconst coq-tactics-abbrev-table24,663 (defconst coq-tacticals-menu27,780 (defconst coq-tacticals-abbrev-table31,889 (defconst coq-commands-menu34,980 (defconst coq-commands-abbrev-table41,1203 (defconst coq-terms-menu44,1292 (defconst coq-terms-abbrev-table49,1430 (defun coq-install-abbrevs 56,1624 (defpgdefault menu-entries76,2361 (defpgdefault help-menu-entries169,5947 coq/coq-db.el,559 (defconst coq-syntax-db 22,534 (defvar coq-user-tactics-db58,1907 (defun coq-insert-from-db 68,2256 (defun coq-build-regexp-list-from-db 86,3037 (defun max-length-db 108,4090 (defun coq-build-menu-from-db-internal 120,4365 (defun coq-build-title-menu 155,5988 (defun coq-sort-menu-entries 164,6356 (defun coq-build-menu-from-db 170,6486 (defun coq-build-abbrev-table-from-db 192,7323 (defun filter-state-preserving 209,7881 (defun filter-state-changing 214,8035 (defface coq-solve-tactics-face 221,8256 (defconst coq-solve-tactics-face 229,8518 coq/coq.el,6441 (defcustom coq-translate-to-v8 45,1301 (defun coq-build-prog-args 51,1481 (defcustom coq-compile-file-command 64,1861 (defcustom coq-default-undo-limit 74,2230 (defconst coq-shell-init-cmd 79,2358 (defcustom coq-prog-env 96,2958 (defconst coq-shell-restart-cmd 104,3210 (defvar coq-shell-prompt-pattern 111,3470 (defvar coq-shell-cd 119,3799 (defvar coq-shell-abort-goal-regexp 123,3954 (defvar coq-shell-proof-completed-regexp 126,4080 (defvar coq-goal-regexp129,4232 (defun coq-library-directory 138,4421 (defcustom coq-tags 145,4601 (defconst coq-interrupt-regexp 150,4751 (defcustom coq-www-home-page 155,4872 (defvar coq-outline-regexp165,5043 (defvar coq-outline-heading-end-regexp 172,5257 (defvar coq-shell-outline-regexp 174,5311 (defvar coq-shell-outline-heading-end-regexp 175,5361 (defconst coq-kill-goal-command 180,5471 (defconst coq-forget-id-command 181,5514 (defconst coq-back-n-command 182,5561 (defconst coq-state-preserving-tactics-regexp 186,5705 (defconst coq-state-changing-commands-regexp188,5806 (defconst coq-state-preserving-commands-regexp 190,5913 (defconst coq-commands-regexp 192,6025 (defvar coq-retractable-instruct-regexp 194,6103 (defvar coq-non-retractable-instruct-regexp 196,6194 (defvar coq-keywords-section200,6334 (defvar coq-section-regexp 203,6428 (defun coq-set-undo-limit 240,7574 (defconst coq-keywords-decl-defn-regexp251,8013 (defun coq-proof-mode-p 255,8163 (defun coq-is-comment-or-proverprocp 266,8571 (defun coq-is-goalsave-p 268,8675 (defun coq-is-module-equal-p 269,8750 (defun coq-is-def-p 272,8946 (defun coq-is-decl-defn-p 274,9054 (defun coq-state-preserving-command-p 279,9221 (defun coq-command-p 282,9355 (defun coq-state-preserving-tactic-p 285,9455 (defun coq-state-changing-tactic-p 290,9603 (defun coq-state-changing-command-p 297,9837 (defun coq-section-or-module-start-p 304,10183 (defun build-list-id-from-string 313,10424 (defun coq-last-prompt-info 326,10954 (defun coq-last-prompt-info-safe 338,11495 (defvar coq-last-but-one-statenum 344,11752 (defvar coq-last-but-one-proofnum 350,12050 (defvar coq-last-but-one-proofstack 353,12148 (defun coq-get-span-statenum 356,12258 (defun coq-get-span-proofnum 361,12373 (defun coq-get-span-proofstack 366,12488 (defun coq-set-span-statenum 371,12632 (defun coq-get-span-goalcmd 376,12763 (defun coq-set-span-goalcmd 381,12877 (defun coq-set-span-proofnum 386,13007 (defun coq-set-span-proofstack 391,13138 (defun proof-last-locked-span 396,13298 (defun coq-set-state-infos 411,13902 (defun count-not-intersection 451,15981 (defun coq-find-and-forget-v81 482,17235 (defun coq-find-and-forget-v80 510,18367 (defun coq-find-and-forget 605,23066 (defvar coq-current-goal 618,23606 (defun coq-goal-hyp 621,23671 (defun coq-state-preserving-p 634,24104 (defconst notation-print-kinds-table 648,24609 (defun coq-PrintScope 652,24777 (defun coq-guess-or-ask-for-string 671,25333 (defun coq-ask-do 682,25720 (defun coq-SearchIsos 691,26108 (defun coq-SearchConstant 697,26341 (defun coq-SearchRewrite 701,26434 (defun coq-SearchAbout 705,26532 (defun coq-Print 709,26624 (defun coq-About 713,26746 (defun coq-LocateConstant 717,26863 (defun coq-LocateLibrary 723,26998 (defun coq-addquotes 729,27148 (defun coq-LocateNotation 731,27196 (defun coq-Pwd 738,27395 (defun coq-Inspect 744,27527 (defun coq-PrintSection(748,27627 (defun coq-Print-implicit 752,27720 (defun coq-Check 757,27871 (defun coq-Show 762,27979 (defun coq-Compile 776,28422 (defun coq-guess-command-line 790,28742 (defun coq-mode-config 820,30152 (defvar coq-last-hybrid-pre-string 932,34258 (defun coq-hybrid-ouput-goals-response-p 935,34437 (defun coq-hybrid-ouput-goals-response 941,34695 (defun coq-shell-mode-config 962,35655 (defun coq-goals-mode-config 1006,37726 (defun coq-response-config 1013,37958 (defpacustom print-fully-explicit 1036,38667 (defpacustom print-implicit 1041,38816 (defpacustom print-coercions 1046,38983 (defpacustom print-match-wildcards 1051,39128 (defpacustom print-elim-types 1056,39309 (defpacustom printing-depth 1061,39476 (defpacustom undo-depth 1066,39638 (defpacustom time-commands 1071,39786 (defpacustom auto-compile-vos 1075,39897 (defun coq-maybe-compile-buffer 1104,41013 (defun coq-ancestors-of 1141,42547 (defun coq-all-ancestors-of 1164,43514 (defconst coq-require-command-regexp 1176,43907 (defun coq-process-require-command 1181,44116 (defun coq-included-children 1186,44243 (defun coq-process-file 1207,45082 (defun coq-preprocessing 1222,45621 (defun coq-fake-constant-markup 1237,46040 (defun coq-create-span-menu 1258,46846 (defconst module-kinds-table 1275,47345 (defconst modtype-kinds-table1279,47495 (defun coq-insert-section-or-module 1283,47624 (defconst reqkinds-kinds-table1306,48484 (defun coq-insert-requires 1311,48629 (defun coq-end-Section 1327,49135 (defun coq-insert-intros 1345,49719 (defun coq-insert-infoH-hook 1358,50244 (defun coq-insert-as 1362,50322 (defun coq-insert-match 1383,51071 (defun coq-insert-tactic 1415,52249 (defun coq-insert-tactical 1421,52488 (defun coq-insert-command 1427,52737 (defun coq-insert-term 1433,52981 (define-key coq-keymap 1439,53178 (define-key coq-keymap 1440,53236 (define-key coq-keymap 1441,53293 (define-key coq-keymap 1442,53362 (define-key coq-keymap 1443,53418 (define-key coq-keymap 1444,53467 (define-key coq-keymap 1445,53525 (define-key coq-keymap 1447,53586 (define-key coq-keymap 1448,53645 (define-key coq-keymap 1450,53709 (define-key coq-keymap 1451,53769 (define-key coq-keymap 1453,53825 (define-key coq-keymap 1454,53875 (define-key coq-keymap 1455,53925 (define-key coq-keymap 1456,53975 (define-key coq-keymap 1457,54029 (define-key coq-keymap 1458,54088 (defvar last-coq-error-location 1466,54219 (defun coq-get-last-error-location 1475,54618 (defun coq-highlight-error 1508,56014 (defvar coq-allow-highlight-error 1574,58694 (defun coq-decide-highlight-error 1580,58960 (defun coq-highlight-error-hook 1585,59122 (defun first-word-of-buffer 1596,59515 (defun coq-show-first-goal 1606,59747 (defvar coq-modeline-string2 1623,60442 (defvar coq-modeline-string1 1624,60486 (defvar coq-modeline-string0 1625,60529 (defun coq-build-subgoals-string 1626,60574 (defun coq-update-minor-mode-alist 1631,60742 (defun is-not-split-vertic 1657,61810 (defun optim-resp-windows 1666,62249 coq/coq-indent.el,2259 (defconst coq-any-command-regexp17,315 (defconst coq-indent-inner-regexp20,406 (defconst coq-comment-start-regexp 31,794 (defconst coq-comment-end-regexp 32,837 (defconst coq-comment-start-or-end-regexp33,878 (defconst coq-indent-open-regexp35,986 (defconst coq-indent-close-regexp40,1160 (defconst coq-indent-closepar-regexp 45,1341 (defconst coq-indent-closematch-regexp 46,1386 (defconst coq-indent-openpar-regexp 47,1457 (defconst coq-indent-openmatch-regexp 48,1501 (defconst coq-indent-any-regexp49,1581 (defconst coq-indent-kw54,1859 (defconst coq-indent-pattern-regexp 64,2313 (defun coq-indent-goal-command-p 68,2416 (defconst coq-end-command-regexp90,3471 (defun coq-search-comment-delimiter-forward 95,3623 (defun coq-search-comment-delimiter-backward 104,3953 (defun coq-skip-until-one-comment-backward 111,4227 (defun coq-skip-until-one-comment-forward 126,4934 (defun coq-looking-at-comment 137,5452 (defun coq-find-comment-start 141,5593 (defun coq-find-comment-end 152,6026 (defun coq-looking-at-syntactic-context 165,6572 (defconst coq-end-command-or-comment-regexp171,6794 (defconst coq-end-command-or-comment-start-regexp174,6903 (defun coq-find-not-in-comment-backward 178,7021 (defun coq-find-not-in-comment-forward 198,7922 (defun coq-find-command-end-backward 222,9064 (defun coq-find-command-end-forward 231,9455 (defun coq-find-command-end 240,9832 (defun coq-parse-function 249,10215 (defun coq-find-current-start 258,10417 (defun coq-find-real-start 267,10708 (defun coq-command-at-point 274,10927 (defun coq-indent-only-spaces-on-line 281,11204 (defun coq-indent-find-reg 287,11481 (defun coq-find-no-syntactic-on-line 301,12017 (defun coq-back-to-indentation-prevline 314,12490 (defun coq-find-unclosed 358,14404 (defun coq-find-at-same-level-zero 388,15705 (defun coq-find-unopened 416,16870 (defun coq-find-last-unopened 459,18320 (defun coq-end-offset 470,18717 (defun coq-indent-command-offset 495,19508 (defun coq-indent-expr-offset 542,21332 (defun coq-indent-comment-offset 658,26035 (defun coq-indent-offset 690,27493 (defun coq-indent-calculate 708,28356 (defun coq-indent-line 711,28444 (defun coq-indent-line-not-comments 721,28810 (defun coq-indent-region 731,29199 coq/coq-local-vars.el,280 (defconst coq-local-vars-doc 17,306 (defun coq-insert-coq-prog-name 75,2832 (defun coq-read-directory 86,3305 (defun coq-extract-directories-from-args 110,4408 (defun coq-ask-prog-args 125,4960 (defun coq-ask-prog-name 147,6064 (defun coq-ask-insert-coq-prog-name 165,6819 coq/coq-syntax.el,2666 (defcustom coq-prog-name 13,422 (defvar coq-version-is-V8 34,1421 (defvar coq-version-is-V8-0 36,1500 (defvar coq-version-is-V8-1 43,1878 (defun coq-determine-version 52,2311 (defcustom coq-user-tactics-db 97,4169 (defcustom coq-user-commands-db 114,4682 (defcustom coq-user-tacticals-db 130,5201 (defcustom coq-user-solve-tactics-db 146,5722 (defcustom coq-user-reserved-db 164,6243 (defvar coq-tactics-db182,6774 (defvar coq-solve-tactics-db337,14842 (defvar coq-tacticals-db361,15689 (defvar coq-decl-db385,16576 (defvar coq-defn-db407,17794 (defvar coq-goal-starters-db460,21780 (defvar coq-other-commands-db487,23335 (defvar coq-commands-db611,32532 (defvar coq-terms-db618,32758 (defun coq-count-match 682,35410 (defun coq-goal-command-str-v80-p 701,36273 (defun coq-module-opening-p 724,37146 (defun coq-section-command-p 735,37562 (defun coq-goal-command-str-v81-p 739,37659 (defun coq-goal-command-p-v81 754,38328 (defun coq-goal-command-str-p 764,38668 (defun coq-goal-command-p 774,39034 (defvar coq-keywords-save-strict782,39346 (defvar coq-keywords-save791,39459 (defun coq-save-command-p 795,39537 (defvar coq-keywords-kill-goal 804,39831 (defvar coq-keywords-state-changing-misc-commands808,39922 (defvar coq-keywords-goal811,40047 (defvar coq-keywords-decl814,40130 (defvar coq-keywords-defn817,40204 (defvar coq-keywords-state-changing-commands821,40279 (defvar coq-keywords-state-preserving-commands830,40540 (defvar coq-keywords-commands835,40756 (defvar coq-solve-tactics840,40905 (defvar coq-tacticals844,41026 (defvar coq-reserved850,41165 (defvar coq-state-changing-tactics861,41494 (defvar coq-state-preserving-tactics864,41603 (defvar coq-tactics868,41717 (defvar coq-retractable-instruct871,41806 (defvar coq-non-retractable-instruct874,41916 (defvar coq-keywords878,42044 (defvar coq-symbols885,42212 (defvar coq-error-regexp 904,42425 (defvar coq-id 907,42653 (defvar coq-id-shy 908,42678 (defvar coq-ids 910,42732 (defun coq-first-abstr-regexp 912,42773 (defcustom coq-variable-highlight-enable 915,42868 (defvar coq-font-lock-terms921,42995 (defconst coq-save-command-regexp-strict942,43995 (defconst coq-save-command-regexp946,44162 (defconst coq-save-with-hole-regexp950,44315 (defconst coq-goal-command-regexp954,44474 (defconst coq-goal-with-hole-regexp957,44574 (defconst coq-decl-with-hole-regexp961,44707 (defconst coq-defn-with-hole-regexp968,44956 (defconst coq-with-with-hole-regexp978,45245 (defvar coq-font-lock-keywords-1984,45538 (defvar coq-font-lock-keywords 1010,46859 (defun coq-init-syntax-table 1012,46917 (defconst coq-generic-expression1041,47816 coq/coq-unicode-tokens.el,290 (defconst coq-token-format 18,631 (defconst coq-charref-format 19,664 (defconst coq-token-prefix 20,698 (defconst coq-token-suffix 21,730 (defconst coq-token-match 22,762 (defconst coq-hexcode-match 23,793 (defcustom coq-token-name-alist 25,827 (defcustom coq-shortcut-alist44,1557 coq/x-symbol-coq.el,1748 (defvar x-symbol-coq-required-fonts 19,510 (defvar x-symbol-coq-name 27,911 (defvar x-symbol-coq-modeline-name 28,951 (defcustom x-symbol-coq-header-groups-alist 30,994 (defcustom x-symbol-coq-electric-ignore 37,1212 (defvar x-symbol-coq-required-fonts 44,1457 (defvar x-symbol-coq-extra-menu-items 47,1556 (defvar x-symbol-coq-token-grammar51,1644 (defun x-symbol-coq-default-token-list 67,2310 (defvar x-symbol-coq-user-table 79,2598 (defvar x-symbol-coq-generated-data 82,2704 (defvar x-symbol-coq-master-directory 90,2942 (defvar x-symbol-coq-image-searchpath 91,2990 (defvar x-symbol-coq-image-cached-dirs 92,3037 (defvar x-symbol-coq-image-file-truename-alist 93,3102 (defvar x-symbol-coq-image-keywords 94,3154 (defcustom x-symbol-coq-subscript-matcher 101,3382 (defcustom x-symbol-coq-font-lock-regexp 107,3614 (defcustom x-symbol-coq-font-lock-limit-regexp 112,3786 (defcustom x-symbol-coq-font-lock-contents-regexp 118,3974 (defcustom x-symbol-coq-single-char-regexp 125,4228 (defun x-symbol-coq-subscript-matcher 130,4376 (defun coq-match-subscript 165,6065 (defvar x-symbol-coq-font-lock-allowed-faces 172,6231 (defcustom x-symbol-coq-class-alist177,6456 (defcustom x-symbol-coq-class-face-alist 188,6834 (defvar x-symbol-coq-font-lock-keywords 198,7144 (defvar x-symbol-coq-font-lock-allowed-faces 200,7190 (defvar x-symbol-coq-case-insensitive 206,7414 (defvar x-symbol-coq-token-shape 207,7457 (defvar x-symbol-coq-input-token-ignore 208,7495 (defvar x-symbol-coq-token-list 209,7540 (defvar x-symbol-coq-symbol-table 211,7584 (defvar x-symbol-coq-xsymbol-table 315,10006 (defun x-symbol-coq-prepare-table 462,13874 (defvar x-symbol-coq-table471,14141 (defcustom x-symbol-coq-auto-style478,14302 demoisa/demoisa.el,349 (defcustom isabelledemo-prog-name 54,1809 (defcustom isabelledemo-web-page59,1931 (defun demoisa-config 70,2161 (defun demoisa-shell-config 91,2953 (define-derived-mode demoisa-mode 117,3930 (define-derived-mode demoisa-shell-mode 122,4053 (define-derived-mode demoisa-response-mode 127,4196 (define-derived-mode demoisa-goals-mode 131,4323 isar/isabelle-system.el,1512 (defgroup isabelle 26,775 (defcustom isabelle-web-page30,903 (defcustom isa-isatool-command41,1198 (defvar isatool-not-found 59,1857 (defun isa-set-isatool-command 62,1970 (defun isa-shell-command-to-string 85,2914 (defun isa-getenv 91,3138 (defcustom isabelle-program-name-override 111,3825 (defvar isabelle-prog-name 128,4409 (defun isa-tool-list-logics 131,4519 (defcustom isabelle-logics-available 138,4756 (defcustom isabelle-chosen-logic 148,5092 (defvar isabelle-chosen-logic-prev 163,5617 (defun isabelle-hack-local-variables-function 166,5739 (defun isabelle-set-prog-name 178,6180 (defun isabelle-choose-logic 203,7339 (defun isa-view-doc 222,8101 (defun isa-tool-list-docs 231,8365 (defconst isabelle-verbatim-regexp 258,9397 (defun isabelle-verbatim 261,9539 (defcustom isabelle-refresh-logics 268,9700 (defvar isabelle-docs-menu 276,10027 (defvar isabelle-logics-menu-entries 283,10313 (defun isabelle-logics-menu-calculate 286,10386 (defvar isabelle-time-to-refresh-logics 305,10949 (defun isabelle-logics-menu-refresh 309,11044 (defun isabelle-logics-menu-filter 326,11741 (defun isabelle-menu-bar-update-logics 332,11951 (defvar isabelle-logics-menu343,12290 (defun isabelle-load-isar-keywords 356,12902 (defpgdefault menu-entries377,13643 (defpgdefault help-menu-entries 380,13695 (defun isabelle-convert-idmarkup-to-subterm 408,14453 (defun isabelle-create-span-menu 432,15464 (defun isabelle-xml-sml-escapes 448,15906 (defun isabelle-process-pgip 451,16007 isar/isar.el,1162 (defcustom isar-keywords-name 31,720 (defpgdefault completion-table 48,1243 (defcustom isar-web-page50,1296 (defun isar-strip-terminators 64,1632 (defun isar-markup-ml 77,2009 (defun isar-mode-config-set-variables 82,2144 (defun isar-shell-mode-config-set-variables 152,5365 (defun isar-remove-file 248,9355 (defun isar-shell-compute-new-files-list 258,9718 (define-derived-mode isar-shell-mode 274,10239 (define-derived-mode isar-response-mode 279,10362 (define-derived-mode isar-goals-mode 284,10544 (define-derived-mode isar-mode 289,10719 (defpgdefault menu-entries346,12754 (defun isar-count-undos 376,13993 (defun isar-find-and-forget 403,15107 (defun isar-goal-command-p 442,16687 (defun isar-global-save-command-p 447,16864 (defvar isar-current-goal 468,17725 (defun isar-state-preserving-p 471,17791 (defvar isar-shell-current-line-width 496,18988 (defun isar-shell-adjust-line-width 501,19180 (defun isar-preprocessing 524,20071 (defun isar-mode-config 547,21338 (defun isar-shell-mode-config 558,21839 (defun isar-response-mode-config 569,22198 (defun isar-goals-mode-config 578,22441 (defun isar-goalhyplit-test 589,22773 isar/isar-find-theorems.el,778 (defun isar-find-theorems-minibuffer 18,712 (defun isar-find-theorems-form 32,1331 (defvar isar-find-theorems-data 74,3131 (defvar isar-find-theorems-widget-number 88,3466 (defvar isar-find-theorems-widget-pattern 91,3564 (defvar isar-find-theorems-widget-intro 94,3656 (defvar isar-find-theorems-widget-elim 97,3742 (defvar isar-find-theorems-widget-dest 100,3826 (defvar isar-find-theorems-widget-name 103,3910 (defvar isar-find-theorems-widget-simp 106,3997 (defun isar-find-theorems-create-searchform111,4143 (defun isar-find-theorems-create-help 251,8758 (defun isar-find-theorems-submit-searchform294,10930 (defun isar-find-theorems-parse-criteria 372,13307 (defun isar-find-theorems-parse-number 465,16407 (defun isar-find-theorems-filter-empty 475,16684 isar/isar-keywords.el,1052 (defconst isar-keywords-major13,481 (defconst isar-keywords-minor206,3641 (defconst isar-keywords-control262,4395 (defconst isar-keywords-diag282,4872 (defconst isar-keywords-theory-begin338,5831 (defconst isar-keywords-theory-switch341,5884 (defconst isar-keywords-theory-end344,5939 (defconst isar-keywords-theory-heading347,5987 (defconst isar-keywords-theory-decl353,6094 (defconst isar-keywords-theory-script412,7075 (defconst isar-keywords-theory-goal416,7152 (defconst isar-keywords-qed429,7369 (defconst isar-keywords-qed-block436,7455 (defconst isar-keywords-qed-global439,7502 (defconst isar-keywords-proof-heading442,7551 (defconst isar-keywords-proof-goal447,7634 (defconst isar-keywords-proof-block454,7733 (defconst isar-keywords-proof-open458,7795 (defconst isar-keywords-proof-close461,7841 (defconst isar-keywords-proof-chain464,7888 (defconst isar-keywords-proof-decl471,7991 (defconst isar-keywords-proof-asm480,8112 (defconst isar-keywords-proof-asm-goal487,8207 (defconst isar-keywords-proof-script490,8262 isar/isar-mmm.el,83 (defconst isar-start-latex-regexp 23,697 (defconst isar-start-sml-regexp 35,1130 isar/isar-syntax.el,3470 (defconst isar-script-syntax-table-entries20,477 (defconst isar-script-syntax-table-alist61,1508 (defun isar-init-syntax-table 70,1798 (defun isar-init-output-syntax-table 78,2045 (defconst isar-keyword-begin 94,2492 (defconst isar-keyword-end 95,2530 (defconst isar-keywords-theory-enclose97,2565 (defconst isar-keywords-theory102,2710 (defconst isar-keywords-save107,2855 (defconst isar-keywords-proof-enclose112,2984 (defconst isar-keywords-proof118,3166 (defconst isar-keywords-proof-context125,3371 (defconst isar-keywords-local-goal129,3485 (defconst isar-keywords-proper133,3597 (defconst isar-keywords-improper138,3730 (defconst isar-keywords-outline143,3876 (defconst isar-keywords-fume146,3941 (defconst isar-keywords-indent-open153,4159 (defconst isar-keywords-indent-close159,4343 (defconst isar-keywords-indent-enclose163,4448 (defun isar-regexp-simple-alt 172,4663 (defun isar-ids-to-regexp 192,5423 (defconst isar-ext-first 226,6829 (defconst isar-ext-rest 227,6896 (defconst isar-long-id-stuff 229,6968 (defconst isar-id 230,7042 (defconst isar-idx 231,7112 (defconst isar-string 233,7171 (defconst isar-any-command-regexp235,7231 (defconst isar-name-regexp239,7365 (defconst isar-improper-regexp245,7660 (defconst isar-save-command-regexp249,7808 (defconst isar-global-save-command-regexp252,7909 (defconst isar-goal-command-regexp255,8023 (defconst isar-local-goal-command-regexp258,8131 (defconst isar-comment-start 261,8244 (defconst isar-comment-end 262,8279 (defconst isar-comment-start-regexp 263,8312 (defconst isar-comment-end-regexp 264,8383 (defconst isar-string-start-regexp 266,8451 (defconst isar-string-end-regexp 267,8503 (defconst isar-antiq-regexp276,8756 (defconst isar-nesting-regexp283,8917 (defun isar-nesting 286,9015 (defun isar-match-nesting 298,9436 (defface isabelle-class-name-face310,9767 (defface isabelle-tfree-name-face318,9950 (defface isabelle-tvar-name-face326,10139 (defface isabelle-free-name-face334,10327 (defface isabelle-bound-name-face342,10511 (defface isabelle-var-name-face350,10698 (defconst isabelle-class-name-face 358,10885 (defconst isabelle-tfree-name-face 359,10947 (defconst isabelle-tvar-name-face 360,11009 (defconst isabelle-free-name-face 361,11070 (defconst isabelle-bound-name-face 362,11131 (defconst isabelle-var-name-face 363,11193 (defconst isar-font-lock-local366,11255 (defvar isar-font-lock-keywords-1371,11421 (defvar isar-output-font-lock-keywords-1385,12287 (defvar isar-goals-font-lock-keywords412,13911 (defconst isar-undo 446,14590 (defun isar-remove 448,14633 (defun isar-undos 451,14708 (defun isar-cannot-undo 455,14814 (defconst isar-theory-start-regexp458,14884 (defconst isar-end-regexp464,15049 (defconst isar-undo-fail-regexp468,15150 (defconst isar-undo-skip-regexp472,15254 (defconst isar-undo-ignore-regexp475,15375 (defconst isar-undo-remove-regexp478,15440 (defconst isar-any-entity-regexp486,15615 (defconst isar-named-entity-regexp491,15802 (defconst isar-unnamed-entity-regexp496,15979 (defconst isar-next-entity-regexps499,16081 (defconst isar-generic-expression507,16392 (defconst isar-indent-any-regexp518,16709 (defconst isar-indent-inner-regexp520,16802 (defconst isar-indent-enclose-regexp522,16868 (defconst isar-indent-open-regexp524,16984 (defconst isar-indent-close-regexp526,17094 (defconst isar-outline-regexp532,17231 (defconst isar-outline-heading-end-regexp 536,17384 isar/isar-unicode-tokens.el,431 (defconst isar-token-format 14,433 (defconst isar-charref-format 15,471 (defconst isar-token-prefix 16,513 (defconst isar-token-suffix 17,548 (defconst isar-token-match 18,581 (defconst isar-control-token-match 19,646 (defconst isar-control-token-format 20,720 (defconst isar-hexcode-match 21,767 (defconst isar-next-character-regexp 22,828 (defcustom isar-token-name-alist24,897 (defcustom isar-shortcut-alist496,13694 isar/x-symbol-isar.el,1775 (defvar x-symbol-isar-required-fonts 15,498 (defvar x-symbol-isar-name 23,898 (defvar x-symbol-isar-modeline-name 24,944 (defcustom x-symbol-isar-header-groups-alist 26,988 (defcustom x-symbol-isar-electric-ignore 33,1208 (defvar x-symbol-isar-required-fonts 41,1456 (defvar x-symbol-isar-extra-menu-items 44,1561 (defvar x-symbol-isar-token-grammar48,1655 (defun x-symbol-isar-token-list 55,1853 (defvar x-symbol-isar-user-table 58,1938 (defvar x-symbol-isar-generated-data 61,2051 (defvar x-symbol-isar-master-directory 69,2290 (defvar x-symbol-isar-image-searchpath 70,2339 (defvar x-symbol-isar-image-cached-dirs 71,2387 (defvar x-symbol-isar-image-file-truename-alist 72,2453 (defvar x-symbol-isar-image-keywords 73,2506 (defcustom x-symbol-isar-subscript-matcher 83,2846 (defcustom x-symbol-isar-font-lock-regexp 89,3081 (defcustom x-symbol-isar-font-lock-limit-regexp 94,3257 (defcustom x-symbol-isar-font-lock-contents-regexp 100,3481 (defcustom x-symbol-isar-single-char-regexp 110,3865 (defun x-symbol-isar-subscript-matcher 116,4135 (defun isabelle-match-subscript 158,5787 (defvar x-symbol-isar-font-lock-keywords167,6163 (defvar x-symbol-isar-font-lock-allowed-faces 174,6423 (defcustom x-symbol-isar-class-alist181,6651 (defcustom x-symbol-isar-class-face-alist 192,7072 (defvar x-symbol-isar-case-insensitive 207,7592 (defvar x-symbol-isar-token-shape 208,7636 (defvar x-symbol-isar-input-token-ignore 209,7675 (defvar x-symbol-isar-token-list 210,7721 (defvar x-symbol-isar-symbol-table 212,7766 (defvar x-symbol-isar-xsymbol-table 312,10498 (defun x-symbol-isar-prepare-table 458,14928 (defvar x-symbol-isar-table466,15124 (defcustom x-symbol-isar-auto-style480,15457 (defcustom x-symbol-isar-auto-coding-alist 494,15954 lclam/lclam.el,524 (defcustom lclam-prog-name 15,385 (defcustom lclam-web-page21,533 (defun lclam-config 32,763 (defun lclam-shell-config 54,1557 (define-derived-mode lclam-proofscript-mode 74,2216 (define-derived-mode lclam-shell-mode 79,2339 (define-derived-mode lclam-response-mode 84,2473 (define-derived-mode lclam-goals-mode 88,2596 (defun lclam-mode 96,2824 (define-derived-mode thy-mode 133,3635 (defvar thy-mode-map 136,3733 (defun thy-add-menus 138,3760 (defun process-thy-file 178,5674 (defun update-thy-only 184,5875 lego/lego.el,1727 (defcustom lego-tags 19,493 (defcustom lego-test-all-name 24,629 (defpgdefault help-menu-entries30,787 (defpgdefault menu-entries34,947 (defvar lego-shell-process-output45,1249 (defconst lego-process-config53,1572 (defconst lego-pretty-set-width 64,2003 (defconst lego-interrupt-regexp 68,2146 (defcustom lego-www-home-page 73,2263 (defcustom lego-www-latest-release78,2387 (defcustom lego-www-refcard84,2565 (defcustom lego-library-www-page90,2714 (defvar lego-prog-name 99,2930 (defvar lego-shell-prompt-pattern 102,2999 (defvar lego-shell-cd 105,3120 (defvar lego-shell-abort-goal-regexp 108,3220 (defvar lego-shell-proof-completed-regexp 113,3412 (defvar lego-save-command-regexp116,3552 (defvar lego-goal-command-regexp118,3642 (defvar lego-kill-goal-command 121,3733 (defvar lego-forget-id-command 122,3776 (defvar lego-undoable-commands-regexp124,3822 (defvar lego-goal-regexp 133,4196 (defvar lego-outline-regexp135,4241 (defvar lego-outline-heading-end-regexp 141,4417 (defvar lego-shell-outline-regexp 143,4470 (defvar lego-shell-outline-heading-end-regexp 144,4522 (define-derived-mode lego-shell-mode 150,4801 (define-derived-mode lego-mode 157,4962 (define-derived-mode lego-goals-mode 168,5259 (defun lego-count-undos 179,5685 (defun lego-goal-command-p 199,6504 (defun lego-find-and-forget 204,6675 (defun lego-goal-hyp 246,8511 (defun lego-state-preserving-p 255,8709 (defvar lego-shell-current-line-width 271,9412 (defun lego-shell-adjust-line-width 279,9719 (defun lego-mode-config 298,10458 (defun lego-equal-module-filename 366,12485 (defun lego-shell-compute-new-files-list 372,12760 (defun lego-shell-mode-config 386,13286 (defun lego-goals-mode-config 435,15222 lego/lego-syntax.el,600 (defconst lego-keywords-goal 15,358 (defconst lego-keywords-save 17,401 (defconst lego-commands19,472 (defconst lego-keywords31,1032 (defconst lego-tacticals 36,1209 (defconst lego-error-regexp 39,1317 (defvar lego-id 42,1476 (defvar lego-ids 44,1503 (defconst lego-arg-list-regexp 48,1699 (defun lego-decl-defn-regexp 51,1815 (defconst lego-definiendum-alternative-regexp59,2187 (defvar lego-font-lock-terms63,2371 (defconst lego-goal-with-hole-regexp89,3227 (defconst lego-save-with-hole-regexp94,3450 (defvar lego-font-lock-keywords-199,3667 (defun lego-init-syntax-table 110,4134 phox/phox.el,644 (defcustom phox-prog-name 31,909 (defcustom phox-sym-lock-enabled 36,1011 (defcustom phox-web-page42,1118 (defcustom phox-doc-dir 48,1268 (defcustom phox-lib-dir 54,1416 (defcustom phox-tags-program 60,1560 (defcustom phox-tags-doc 66,1740 (defcustom phox-etags 72,1878 (defpgdefault menu-entries93,2330 (defun phox-config 107,2523 (defun phox-shell-config 153,4560 (define-derived-mode phox-mode 178,5489 (define-derived-mode phox-shell-mode 201,6152 (define-derived-mode phox-response-mode 206,6280 (define-derived-mode phox-goals-mode 218,6707 (defpgdefault completion-table243,7575 (defpgdefault x-symbol-language 251,7680 phox/phox-extraction.el,382 (defvar phox-prog-orig 11,480 (defun phox-prog-flags-modify(13,548 (defun phox-prog-flags-extract(42,1352 (defun phox-prog-flags-erase(53,1643 (defun phox-toggle-extraction(61,1839 (defun phox-compile-theorem(73,2241 (defun phox-compile-theorem-on-cursor(79,2467 (defun phox-output 95,2946 (defun phox-output-theorem 105,3160 (defun phox-output-theorem-on-cursor(112,3460 phox/phox-font.el,123 (defconst phox-font-lock-keywords6,282 (defconst phox-sym-lock-keywords-table65,2401 (defun phox-sym-lock-start 88,2975 phox/phox-fun.el,679 (defun phox-init-syntax-table 67,2392 (defvar phox-top-keywords83,2865 (defvar phox-proof-keywords131,3320 (defun phox-find-and-forget 172,3670 (defun phox-assert-next-command-interactive 251,6095 (defun phox-depend-theorem(270,6926 (defun phox-eshow-extlist(279,7216 (defun phox-flag-name(293,7815 (defun phox-path(304,8118 (defun phox-print-expression(315,8355 (defun phox-print-sort-expression(328,8813 (defun phox-priority-symbols-list(339,9126 (defun phox-search-string(351,9499 (defun phox-constraints(366,10027 (defun phox-goals(377,10284 (defvar phox-state-menu389,10494 (defun phox-delete-symbol(414,11484 (defun phox-delete-symbol-on-cursor(420,11693 phox/phox-lang.el,283 (defvar phox-lang8,278 (defun phox-lang-absurd 17,495 (defun phox-lang-suppress 22,590 (defun phox-lang-opendef 27,789 (defun phox-lang-instance 32,908 (defun phox-lang-lock 37,1037 (defun phox-lang-unlock 42,1174 (defun phox-lang-prove 47,1317 (defun phox-lang-let 52,1454 phox/phox-outline.el,70 (defun phox-outline-level(32,1113 (defun phox-setup-outline 46,1587 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,1929 (defun phox-pbrpm-get-region-name 84,3183 (defun phox-pbrpm-escape-string 87,3310 (defun phox-pbrpm-generate-menu 91,3445 (defalias 'proof-pbrpm-generate-menu proof-pbrpm-generate-menu289,10634 (defalias 'proof-pbrpm-left-paren-p proof-pbrpm-left-paren-p290,10698 (defalias 'proof-pbrpm-right-paren-p proof-pbrpm-right-paren-p291,10760 phox/phox-sym-lock.el,1353 (defvar phox-sym-lock-sym-count 34,1598 (defvar phox-sym-lock-ext-start 37,1668 (defvar phox-sym-lock-ext-end 39,1790 (defvar phox-sym-lock-font-size 42,1909 (defvar phox-sym-lock-keywords 47,2099 (defvar phox-sym-lock-enabled 52,2275 (defvar phox-sym-lock-color 57,2437 (defvar phox-sym-lock-mouse-face 62,2655 (defvar phox-sym-lock-mouse-face-enabled 67,2845 (defconst phox-sym-lock-with-mule 72,3035 (defun phox-sym-lock-gen-symbol 75,3119 (defun phox-sym-lock-make-symbols-atomic 83,3422 (defun phox-sym-lock-compute-font-size 110,4364 (defvar phox-sym-lock-font-name148,5784 (defun phox-sym-lock-set-foreground 190,7270 (defun phox-sym-lock-translate-char 204,7879 (defun phox-sym-lock-translate-char-or-string 212,8147 (defun phox-sym-lock-remap-face 219,8374 (defvar phox-sym-lock-clear-face239,9364 (defun phox-sym-lock 251,9786 (defun phox-sym-lock-rec 260,10190 (defun phox-sym-lock-atom-face 266,10343 (defun phox-sym-lock-pre-idle-hook-first 271,10639 (defun phox-sym-lock-pre-idle-hook-last 279,10997 (defun phox-sym-lock-enable 288,11372 (defun phox-sym-lock-disable 301,11785 (defun phox-sym-lock-mouse-face-enable 314,12203 (defun phox-sym-lock-mouse-face-disable 321,12418 (defun phox-sym-lock-font-lock-hook 328,12637 (defun font-lock-set-defaults 343,13330 (defun phox-sym-lock-patch-keywords 354,13708 phox/phox-tags.el,305 (defun phox-tags-add-table(21,766 (defun phox-tags-reset-table(38,1354 (defun phox-tags-add-doc-table(48,1619 (defun phox-tags-add-lib-table(54,1768 (defun phox-tags-add-local-table(60,1904 (defun phox-tags-create-local-table(66,2087 (defun phox-complete-tag(77,2339 (defvar phox-tags-menu96,2889 phox/x-symbol-phox.el,1609 (defvar x-symbol-phox-required-fonts 16,472 (defcustom x-symbol-phox-header-groups-alist 31,1079 (defcustom x-symbol-phox-electric-ignore 38,1299 (defvar x-symbol-phox-required-fonts 45,1515 (defvar x-symbol-phox-extra-menu-items 48,1616 (defvar x-symbol-phox-token-grammar51,1705 (defvar x-symbol-phox-input-token-grammar65,2496 (defun x-symbol-phox-default-token-list 71,2751 (defvar x-symbol-phox-user-table 83,3069 (defvar x-symbol-phox-generated-data 86,3178 (defvar x-symbol-phox-master-directory 94,3417 (defvar x-symbol-phox-image-searchpath 95,3466 (defvar x-symbol-phox-image-cached-dirs 96,3514 (defvar x-symbol-phox-image-file-truename-alist 97,3580 (defvar x-symbol-phox-image-keywords 98,3633 (defcustom x-symbol-phox-class-alist105,3854 (defcustom x-symbol-phox-class-face-alist 116,4236 (defvar x-symbol-phox-font-lock-keywords 126,4549 (defvar x-symbol-phox-font-lock-allowed-faces 128,4596 (defvar x-symbol-phox-case-insensitive 134,4821 (defvar x-symbol-phox-token-shape 135,4865 (defvar x-symbol-phox-input-token-ignore 136,4904 (defvar x-symbol-phox-token-list 143,5143 (defvar x-symbol-phox-xsymb0-table 145,5188 (defun x-symbol-phox-prepare-table 166,5647 (defvar x-symbol-phox-table174,5823 (defcustom x-symbol-phox-auto-style185,6141 (defvar x-symbol-phox-menu-alist 211,7084 (defvar x-symbol-phox-grid-alist 213,7174 (defvar x-symbol-phox-decode-atree 216,7265 (defvar x-symbol-phox-decode-alist 218,7358 (defvar x-symbol-phox-encode-alist 220,7455 (defvar x-symbol-phox-nomule-decode-exec 224,7612 (defvar x-symbol-phox-nomule-encode-exec 226,7712 plastic/plastic.el,2866 (defcustom plastic-tags 29,821 (defcustom plastic-test-all-name 34,953 (defvar plastic-lit-string 41,1144 (defcustom plastic-help-menu-list45,1258 (defvar plastic-shell-process-output59,1752 (defconst plastic-process-config 67,2078 (defconst plastic-pretty-set-width 74,2328 (defconst plastic-interrupt-regexp 78,2477 (defcustom plastic-www-home-page 84,2598 (defcustom plastic-www-latest-release89,2735 (defcustom plastic-www-refcard95,2908 (defcustom plastic-library-www-page101,3039 (defcustom plastic-base 111,3254 (defvar plastic-prog-name 119,3426 (defun plastic-set-default-env-vars 123,3534 (defvar plastic-shell-prompt-pattern 131,3772 (defvar plastic-shell-cd 134,3897 (defvar plastic-shell-abort-goal-regexp 138,4039 (defvar plastic-shell-proof-completed-regexp 142,4207 (defvar plastic-save-command-regexp145,4350 (defvar plastic-goal-command-regexp147,4446 (defvar plastic-kill-goal-command 150,4543 (defvar plastic-forget-id-command 152,4644 (defvar plastic-undoable-commands-regexp155,4725 (defvar plastic-goal-regexp 167,5172 (defvar plastic-outline-regexp169,5220 (defvar plastic-outline-heading-end-regexp 175,5399 (defvar plastic-shell-outline-regexp 177,5455 (defvar plastic-shell-outline-heading-end-regexp 178,5513 (defvar plastic-error-occurred 180,5584 (define-derived-mode plastic-shell-mode 189,5916 (define-derived-mode plastic-mode 195,6098 (define-derived-mode plastic-goals-mode 211,6618 (defun plastic-count-undos 220,6963 (defun plastic-goal-command-p 240,7839 (defun plastic-find-and-forget 245,8032 (defun plastic-goal-hyp 280,9380 (defun plastic-state-preserving-p 291,9630 (defvar plastic-shell-current-line-width 314,10606 (defun plastic-shell-adjust-line-width 322,10922 (defun plastic-mode-config 349,12017 (defun plastic-show-shell-buffer 438,15258 (defun plastic-equal-module-filename 444,15361 (defun plastic-shell-compute-new-files-list 450,15639 (defun plastic-shell-mode-config 466,16176 (defun plastic-goals-mode-config 517,18369 (defun plastic-small-bar 529,18651 (defun plastic-large-bar 531,18740 (defun plastic-preprocessing 533,18878 (defun plastic-all-ctxt 584,20706 (defun plastic-send-one-undo 591,20884 (defun plastic-minibuf-cmd 601,21212 (defun plastic-minibuf 613,21691 (defun plastic-synchro 620,21897 (defun plastic-send-minibuf 625,22038 (defun plastic-had-error 633,22367 (defun plastic-reset-error 637,22542 (defun plastic-call-if-no-error 640,22681 (defun plastic-show-shell 645,22885 (define-key plastic-keymap 654,23147 (define-key plastic-keymap 655,23208 (define-key plastic-keymap 656,23269 (define-key plastic-keymap 657,23329 (define-key plastic-keymap 658,23388 (define-key plastic-keymap 659,23447 (defalias 'proof-toolbar-command proof-toolbar-command669,23697 (defalias 'proof-minibuffer-cmd proof-minibuffer-cmd670,23748 plastic/plastic-syntax.el,648 (defconst plastic-keywords-goal 18,537 (defconst plastic-keywords-save 20,583 (defconst plastic-commands22,657 (defconst plastic-keywords35,1267 (defconst plastic-tacticals 40,1450 (defconst plastic-error-regexp 43,1561 (defvar plastic-id 46,1695 (defvar plastic-ids 48,1725 (defconst plastic-arg-list-regexp 52,1933 (defun plastic-decl-defn-regexp 55,2052 (defconst plastic-definiendum-alternative-regexp63,2433 (defvar plastic-font-lock-terms67,2626 (defconst plastic-goal-with-hole-regexp89,3339 (defconst plastic-save-with-hole-regexp94,3566 (defvar plastic-font-lock-keywords-199,3792 (defun plastic-init-syntax-table 108,4184 twelf/twelf.el,463 (defcustom twelf-root-dir25,591 (defcustom twelf-info-dir31,749 (defun twelf-add-read-declaration 100,3259 (defun twelf-set-syntax 113,3594 (defun twelf-set-word 115,3691 (defun twelf-set-symbol 116,3753 (defun twelf-map-string 118,3817 (defun twelf-mode-extra-config 165,5879 (defconst twelf-syntax-menu171,6085 (defpacustom chatter 185,6452 (defpacustom double-check 190,6545 (defpacustom print-implicit 194,6682 (defpgdefault menu-entries206,6826 twelf/twelf-font.el,917 (defun twelf-font-create-face 31,836 (defvar twelf-font-dark-background 38,1094 (defvar twelf-font-patterns64,2452 (defun twelf-font-fontify-decl 105,4302 (defun twelf-font-fontify-buffer 115,4599 (defun twelf-font-unfontify 122,4858 (defvar font-lock-message-threshold 127,5032 (defun twelf-font-fontify-region 129,5110 (defun twelf-font-highlight 195,7610 (defun twelf-font-find-delimited-comment 204,8067 (defun twelf-font-find-decl 223,8747 (defun twelf-font-find-binder 239,9237 (defun twelf-font-find-parm 301,11094 (defun twelf-font-find-evar 308,11417 (defun twelf-current-decl 330,12159 (defun twelf-next-decl 357,13315 (defconst *whitespace* 382,14337 (defconst *twelf-comment-start* 385,14435 (defconst *twelf-id-chars* 388,14564 (defun skip-twelf-comments-and-whitespace 391,14682 (defun twelf-end-of-par 403,15156 (defun skip-ahead 426,15930 (defun current-line-absolute 438,16352 twelf/twelf-old.el,6958 (defvar twelf-indent 212,8771 (defvar twelf-infix-regexp 215,8831 (defvar twelf-server-program 219,9026 (defvar twelf-info-file 222,9107 (defvar twelf-server-display-commands 225,9180 (defvar twelf-highlight-range-function 230,9428 (defvar twelf-focus-function 235,9711 (defvar twelf-server-echo-commands 241,9991 (defvar twelf-save-silently 244,10112 (defvar twelf-server-timeout 248,10284 (defvar twelf-sml-program 252,10431 (defvar twelf-sml-args 255,10503 (defvar twelf-sml-display-queries 258,10569 (defvar twelf-mode-hook 261,10677 (defvar twelf-server-mode-hook 264,10771 (defvar twelf-config-mode-hook 267,10879 (defvar twelf-sml-mode-hook 270,10993 (defvar twelf-to-twelf-sml-mode 273,11074 (defvar twelf-config-mode 276,11166 (defvar *twelf-server-buffer-name* 283,11430 (defvar *twelf-server-buffer* 286,11534 (defvar *twelf-server-process-name* 289,11622 (defvar *twelf-config-buffer* 292,11713 (defvar *twelf-config-time* 295,11807 (defvar *twelf-config-list* 298,11920 (defvar *twelf-server-last-process-mark* 301,12032 (defvar *twelf-last-region-sent* 304,12150 (defvar *twelf-last-input-buffer* 311,12474 (defvar *twelf-error-pos* 315,12597 (defconst *twelf-read-functions*318,12673 (defconst *twelf-parm-table*325,12911 (defvar twelf-chatter 338,13287 (defvar twelf-double-check 346,13504 (defvar twelf-print-implicit 349,13591 (defconst *twelf-track-parms*352,13683 (defun install-basic-twelf-keybindings 363,14107 (defun install-twelf-keybindings 388,15076 (defvar twelf-mode-map 404,15841 (defvar twelf-mode-syntax-table 416,16277 (defun set-twelf-syntax 419,16356 (defun set-word 421,16453 (defun set-symbol 422,16508 (defun map-string 424,16566 (defconst *whitespace* 456,18043 (defconst *twelf-comment-start* 459,18141 (defconst *twelf-id-chars* 462,18270 (defun skip-twelf-comments-and-whitespace 465,18388 (defun twelf-end-of-par 477,18862 (defun twelf-current-decl 500,19636 (defun twelf-mark-decl 527,20792 (defun twelf-indent-decl 536,21058 (defun twelf-indent-region 545,21344 (defun twelf-indent-lines 556,21668 (defun twelf-comment-indent 564,21841 (defun looked-at 575,22197 (defun twelf-indent-line 580,22369 (defun twelf-indent-line-to 613,24112 (defun twelf-calculate-indent 626,24567 (defun twelf-dsb 641,25191 (defun twelf-mode-variables 667,26603 (defun twelf-mode 689,27416 (defun twelf-info 904,35798 (defconst twelf-error-regexp918,36338 (defconst twelf-error-fields-regexp922,36449 (defconst twelf-error-decl-regexp928,36662 (defun looked-at-nth 932,36811 (defun looked-at-nth-int 938,36993 (defun twelf-error-parser 943,37111 (defun twelf-error-decl 957,37714 (defun twelf-mark-relative 963,37893 (defun twelf-mark-absolute 979,38563 (defun twelf-find-decl 1004,39449 (defun twelf-next-error 1019,40005 (defun twelf-goto-error 1087,42815 (defun twelf-convert-standard-filename 1101,43353 (defun string-member 1113,43848 (defun twelf-config-proceed-p 1125,44340 (defun twelf-save-if-config 1132,44602 (defun twelf-config-save-some-buffers 1145,45074 (defun twelf-save-check-config 1149,45239 (defun twelf-check-config 1164,45795 (defun twelf-save-check-file 1176,46235 (defun twelf-buffer-substring 1192,46958 (defun twelf-buffer-substring-dot 1198,47220 (defun twelf-check-declaration 1204,47486 (defun twelf-highlight-range-zmacs 1227,48546 (defun twelf-focus 1233,48796 (defun twelf-focus-noop 1239,49062 (defun twelf-type-const 1322,52684 (defvar twelf-server-mode-map 1439,57826 (defconst twelf-server-cd-regexp 1451,58378 (defun looked-at-string 1454,58518 (defun twelf-server-directory-tracker 1458,58659 (defun twelf-input-filter 1480,59839 (defun twelf-server-mode 1486,60094 (defun twelf-parse-config 1519,61311 (defun twelf-server-read-config 1537,62203 (defun twelf-server-sync-config 1546,62540 (defun twelf-get-server-buffer 1576,64046 (defun twelf-init-variables 1593,64720 (defun twelf-server 1600,64933 (defun twelf-server-process 1642,66847 (defun twelf-server-display 1651,67253 (defun display-server-buffer 1658,67527 (defun twelf-server-send-command 1673,68259 (defun twelf-accept-process-output 1694,69219 (defun twelf-server-wait 1703,69658 (defun twelf-server-quit 1745,71796 (defun twelf-server-interrupt 1750,71917 (defun twelf-reset 1755,72053 (defun twelf-config-directory 1760,72197 (defun twelf-server-configure 1771,72611 (defun natp 1844,75903 (defun twelf-read-nat 1848,76004 (defun twelf-read-bool 1857,76271 (defun twelf-read-limit 1863,76419 (defun twelf-read-strategy 1873,76722 (defun twelf-read-value 1879,76874 (defun twelf-set 1883,77037 (defun twelf-set-parm 1896,77514 (defun track-parm 1905,77811 (defun twelf-toggle-double-check 1910,77985 (defun twelf-toggle-print-implicit 1916,78188 (defun twelf-get 1922,78401 (defun twelf-timers-reset 1936,79027 (defun twelf-timers-show 1941,79147 (defun twelf-timers-check 1947,79298 (defun twelf-server-restart 1953,79463 (defun twelf-config-mode 1969,80140 (defun twelf-config-mode-check 1985,80739 (defun twelf-tag 1994,81189 (defun twelf-tag-files 2022,82453 (default: *tags-errors*)2026,82756 (defun twelf-tag-file 2047,83507 (defun twelf-next-decl 2082,84729 (defun skip-ahead 2107,85751 (defun current-line-absolute 2119,86173 (defun new-temp-buffer 2124,86383 (defun rev-relativize 2135,86767 (defvar twelf-sml-mode-map 2149,87227 (defconst twelf-sml-prompt-regexp 2159,87605 (defun expand-dir 2161,87660 (defun twelf-sml-cd 2168,87921 (defconst twelf-sml-cd-regexp 2180,88410 (defun twelf-sml-directory-tracker 2183,88544 (defun twelf-sml-mode 2199,89389 (defun twelf-sml 2250,91323 (defun switch-to-twelf-sml 2270,92283 (defun display-twelf-sml-buffer 2281,92632 (defun twelf-sml-send-string 2297,93348 (defun twelf-sml-send-region 2302,93552 (defun twelf-sml-send-query 2326,94758 (defun twelf-sml-send-newline 2336,95155 (defun twelf-sml-send-semicolon 2344,95483 (defun twelf-sml-status 2352,95817 (defvar twelf-sml-init 2374,96764 (defun twelf-sml-set-mode 2377,96941 (defun twelf-sml-quit 2403,98118 (defun twelf-sml-process-buffer 2408,98230 (defun twelf-sml-process 2412,98346 (defvar twelf-to-twelf-sml-mode 2424,98862 (defun install-twelf-to-twelf-sml-keybindings 2427,98947 (defvar twelf-to-twelf-sml-mode-map 2437,99332 (defun twelf-to-twelf-sml-mode 2448,99845 (defconst twelf-at-point-menu2498,101712 (defconst twelf-server-state-menu2508,102084 (defconst twelf-error-menu2518,102401 (defconst twelf-tags-menu2524,102545 (defun twelf-toggle-server-display-commands 2534,102830 (defconst twelf-options-menu2537,102954 (defconst twelf-timers-menu2572,104692 (defconst twelf-syntax-menu2585,105186 (defun twelf-add-menu 2612,106052 (defun twelf-remove-menu 2616,106154 (defun twelf-reset-menu 2620,106252 (defun twelf-server-add-menu 2647,107151 (defun twelf-server-remove-menu 2651,107274 (defun twelf-server-reset-menu 2655,107386 generic/pg-assoc.el,402 (defun proof-associated-buffers 38,1096 (defun proof-associated-windows 48,1308 (defun pg-assoc-strip-subterm-markup 65,1789 (defvar pg-assoc-ann-regexp 91,2722 (defun pg-assoc-strip-subterm-markup-buf 94,2817 (defun pg-assoc-strip-subterm-markup-buf-old 117,3536 (defconst pg-assoc-active-area-keymap 146,4391 (defun pg-assoc-make-top-span 153,4616 (defun pg-assoc-analyse-structure 190,6081 generic/pg-autotest.el,442 (defvar pg-autotest-success 24,543 (defun pg-autotest-find-file 28,627 (defun pg-autotest-find-file-restart 35,907 (defmacro pg-autotest 48,1355 (defun pg-autotest-script-wholefile 62,1702 (defun pg-autotest-retract-file 79,2315 (defun pg-autotest-assert-processed 85,2451 (defun pg-autotest-assert-unprocessed 92,2705 (defun pg-autotest-message 99,2965 (defun pg-autotest-quit-prover 106,3158 (defun pg-autotest-finished 112,3339 generic/pg-custom.el,678 (defpgcustom x-symbol-enable 32,1065 (defpgcustom x-symbol-language 42,1491 (defpgcustom maths-menu-enable 47,1713 (defpgcustom unicode-tokens-enable 53,1893 (defpgcustom unicode-tokens2-enable 59,2070 (defpgcustom mmm-enable 65,2248 (defpgcustom script-indent 74,2602 (defconst proof-toolbar-entries-default79,2739 (defpgcustom toolbar-entries 113,4652 (defpgcustom prog-args 131,5372 (defpgcustom prog-env 144,5947 (defpgcustom favourites 153,6373 (defpgcustom menu-entries 158,6562 (defpgcustom help-menu-entries 165,6798 (defpgcustom keymap 172,7061 (defpgcustom completion-table 177,7233 (defpgcustom tags-program 188,7607 (defpgcustom use-holes 197,7991 generic/pg-goals.el,363 (define-derived-mode proof-goals-mode 30,632 (define-key proof-goals-mode-map 61,1623 (defun proof-goals-config-done 91,3091 (defun pg-goals-display 101,3379 (defun pg-goals-yank-subterm 167,5816 (defun pg-goals-button-action 194,6716 (defun proof-expand-path 215,7688 (defun pg-goals-construct-command 224,7930 (defun pg-goals-get-subterm-help 256,9118 generic/pg-pbrpm.el,1803 (defvar pg-pbrpm-use-buffer-menu 22,547 (defvar pg-pbrpm-start-goal-regexp 25,669 (defvar pg-pbrpm-start-goal-regexp-par-num 29,826 (defvar pg-pbrpm-end-goal-regexp 32,949 (defvar pg-pbrpm-start-hyp-regexp 36,1101 (defvar pg-pbrpm-start-hyp-regexp-par-num 40,1262 (defvar pg-pbrpm-start-concl-regexp 44,1469 (defvar pg-pbrpm-auto-select-regexp 48,1633 (defvar pg-pbrpm-buffer-menu 55,1794 (defvar pg-pbrpm-spans 56,1828 (defvar pg-pbrpm-goal-description 57,1856 (defvar pg-pbrpm-windows-dialog-bug 58,1895 (defvar pbrpm-menu-desc 59,1936 (defun pg-pbrpm-erase-buffer-menu 61,1966 (defun pg-pbrpm-menu-change-hook 68,2150 (defun pg-pbrpm-create-reset-buffer-menu 86,2726 (defun pg-pbrpm-analyse-goal-buffer 101,3355 (defun pg-pbrpm-button-action 161,5765 (defun pg-pbrpm-exists 168,5991 (defun pg-pbrpm-eliminate-id 172,6103 (defun pg-pbrpm-build-menu 180,6349 (defun pg-pbrpm-setup-span 253,8976 (defun pg-pbrpm-run-command 313,11294 (defun pg-pbrpm-get-pos-info 342,12604 (defun pg-pbrpm-get-region-info 384,13911 (defun pg-pbrpm-auto-select-around-point 395,14325 (defun pg-pbrpm-translate-position 410,14855 (defun pg-pbrpm-process-click 418,15113 (defvar pg-pbrpm-remember-region-selected-region 438,16138 (defvar pg-pbrpm-regions-list 439,16192 (defun pg-pbrpm-erase-regions-list 441,16228 (defun pg-pbrpm-filter-regions-list 450,16536 (defface pg-pbrpm-multiple-selection-face457,16799 (defface pg-pbrpm-menu-input-face465,17001 (defun pg-pbrpm-do-remember-region 473,17191 (defun pg-pbrpm-remember-region-drag-up-hook 494,18039 (defun pg-pbrpm-remember-region-click-hook 498,18210 (defun pg-pbrpm-remember-region 503,18395 (defun pg-pbrpm-process-region 517,19110 (defun pg-pbrpm-process-regions-list 535,19839 (defun pg-pbrpm-region-expression 539,20022 generic/pg-pgip.el,2889 (defalias 'pg-pgip-debug pg-pgip-debug35,919 (defalias 'pg-pgip-error pg-pgip-error36,960 (defalias 'pg-pgip-warning pg-pgip-warning37,995 (defconst pg-pgip-version-supported 39,1045 (defun pg-pgip-process-packet 43,1151 (defvar pg-pgip-last-seen-id 53,1723 (defvar pg-pgip-last-seen-seq 54,1757 (defun pg-pgip-process-pgip 56,1793 (defun pg-pgip-process-msg 75,2724 (defvar pg-pgip-post-process-functions89,3294 (defun pg-pgip-post-process 99,3782 (defun pg-pgip-process-askpgip 115,4393 (defun pg-pgip-process-usespgip 121,4598 (defun pg-pgip-process-usespgml 125,4762 (defun pg-pgip-process-pgmlconfig 129,4926 (defun pg-pgip-process-proverinfo 145,5543 (defun pg-pgip-process-hasprefs 162,6208 (defun pg-pgip-haspref 176,6840 (defun pg-pgip-process-prefval 195,7616 (defun pg-pgip-process-guiconfig 222,8325 (defvar proof-assistant-idtables 229,8442 (defun pg-pgip-process-ids 232,8559 (defun pg-complete-idtable-symbol 258,9635 (defalias 'pg-pgip-process-setids pg-pgip-process-setids263,9727 (defalias 'pg-pgip-process-addids pg-pgip-process-addids264,9783 (defalias 'pg-pgip-process-delids pg-pgip-process-delids265,9839 (defun pg-pgip-process-idvalue 268,9897 (defun pg-pgip-process-menuadd 280,10233 (defun pg-pgip-process-menudel 283,10276 (defun pg-pgip-process-ready 292,10509 (defun pg-pgip-process-cleardisplay 295,10550 (defun pg-pgip-process-proofstate 309,11007 (defun pg-pgip-process-normalresponse 313,11084 (defun pg-pgip-process-errorresponse 317,11208 (defun pg-pgip-process-scriptinsert 321,11331 (defun pg-pgip-process-metainforesponse 326,11465 (defun pg-pgip-process-informfileloaded 335,11706 (defun pg-pgip-process-informfileretracted 341,11972 (defun pg-pgip-process-brokerstatus 354,12449 (defun pg-pgip-process-proveravailmsg 357,12497 (defun pg-pgip-process-newprovermsg 360,12547 (defun pg-pgip-process-proverstatusmsg 363,12595 (defvar pg-pgip-srcids 372,12842 (defun pg-pgip-process-newfile 376,12949 (defun pg-pgip-process-filestatus 392,13537 (defun pg-pgip-process-newobj 412,14192 (defun pg-pgip-process-delobj 415,14234 (defun pg-pgip-process-objectstatus 418,14276 (defun pg-pgip-process-parsescript 432,14631 (defun pg-pgip-get-pgiptype 455,15506 (defun pg-pgip-default-for 475,16299 (defun pg-pgip-subst-for 488,16694 (defun pg-pgip-interpret-value 500,17037 (defun pg-pgip-interpret-choice 518,17722 (defun pg-pgip-string-of-command 549,18739 (defconst pg-pgip-id566,19500 (defvar pg-pgip-refseq 572,19780 (defvar pg-pgip-refid 574,19877 (defvar pg-pgip-seq 577,19969 (defun pg-pgip-assemble-packet 579,20033 (defun pg-pgip-issue 597,20845 (defun pg-pgip-maybe-askpgip 614,21457 (defun pg-pgip-askprefs 620,21648 (defun pg-pgip-askids 624,21762 (defun pg-pgip-reset 637,22050 (defconst pg-pgip-start-element-regexp 668,22748 (defconst pg-pgip-end-element-regexp 669,22800 generic/pg-response.el,1182 (deflocal pg-response-eagerly-raise 31,730 (define-derived-mode proof-response-mode 41,955 (defun proof-response-config-done 67,2080 (defvar pg-response-special-display-regexp 88,2855 (defconst proof-multiframe-specifiers96,3261 (defun proof-map-multiple-frame-specifiers 105,3618 (defconst proof-multiframe-parameters116,4140 (defun proof-multiple-frames-enable 125,4439 (defun proof-three-window-enable 143,5083 (defun proof-select-three-b 147,5147 (defun proof-display-three-b 162,5616 (defvar pg-frame-configuration 176,6108 (defun pg-cache-frame-configuration 180,6255 (defun proof-layout-windows 184,6426 (defun proof-delete-other-frames 225,8249 (defvar pg-response-erase-flag 256,9339 (defun pg-response-maybe-erase260,9468 (defun pg-response-display 291,10653 (defun pg-response-display-with-face 310,11501 (defun pg-response-clear-displays 346,12731 (defun proof-next-error 365,13318 (defun pg-response-has-error-location 446,16234 (defvar proof-trace-last-fontify-pos 469,17067 (defun proof-trace-fontify-pos 471,17110 (defun proof-trace-buffer-display 479,17423 (defun proof-trace-buffer-finish 503,18395 (defun pg-thms-buffer-clear 524,18975 generic/pg-thymodes.el,152 (defmacro pg-defthymode 23,499 (defmacro pg-do-unless-null 71,2307 (defun pg-symval 76,2394 (defun pg-modesym 82,2549 (defun pg-modesymval 86,2663 generic/pg-user.el,3127 (defmacro proof-maybe-save-point 31,805 (defun proof-maybe-follow-locked-end 39,1007 (defun proof-assert-next-command-interactive 53,1372 (defun proof-process-buffer 63,1743 (defun proof-undo-last-successful-command 77,2060 (defun proof-undo-and-delete-last-successful-command 82,2222 (defun proof-undo-last-successful-command-1 104,3193 (defun proof-retract-buffer 120,3758 (defun proof-retract-current-goal 129,4038 (defun proof-interrupt-process 148,4544 (defun proof-goto-command-start 175,5533 (defun proof-goto-command-end 198,6473 (defun proof-mouse-goto-point 223,7251 (defun proof-mouse-track-insert 239,7883 (defvar proof-minibuffer-history 275,9020 (defun proof-minibuffer-cmd 278,9115 (defun proof-frob-locked-end 326,10909 (defmacro proof-if-setting-configured 387,12839 (defmacro proof-define-assistant-command 395,13108 (defmacro proof-define-assistant-command-witharg 408,13563 (defun proof-issue-new-command 428,14386 (defun proof-cd-sync 472,15829 (defun proof-electric-terminator-enable 531,17588 (defun proof-electric-term-incomment-fn 539,17883 (defun proof-process-electric-terminator 559,18634 (defun proof-electric-terminator 586,19782 (defun proof-add-completions 608,20419 (defun proof-script-complete 628,21173 (defun pg-insert-last-output-as-comment 656,21764 (defun pg-copy-span-contents 687,22998 (defun pg-numth-span-higher-or-lower 704,23556 (defun pg-control-span-of 730,24302 (defun pg-move-span-contents 736,24506 (defun pg-fixup-children-spans 788,26686 (defun pg-move-region-down 798,26949 (defun pg-move-region-up 807,27242 (defun proof-forward-command 837,28080 (defun proof-backward-command 858,28801 (defun pg-pos-for-event 880,29152 (defun pg-span-for-event 892,29513 (defun pg-span-context-menu 896,29657 (defun pg-toggle-visibility 911,30112 (defun pg-create-in-span-context-menu 921,30434 (defun pg-span-undo 954,31778 (defun pg-goals-buffers-hint 1000,33188 (defun pg-slow-fontify-tracing-hint 1004,33370 (defun pg-response-buffers-hint 1008,33541 (defun pg-jump-to-end-hint 1018,33903 (defun pg-processing-complete-hint 1022,34034 (defun pg-next-error-hint 1039,34733 (defun pg-hint 1044,34885 (defun pg-identifier-under-mouse-query 1063,35554 (defun proof-imenu-enable 1109,37209 (defvar pg-input-ring 1142,38349 (defvar pg-input-ring-index 1145,38405 (defvar pg-stored-incomplete-input 1148,38476 (defun pg-previous-input 1151,38578 (defun pg-next-input 1165,39035 (defun pg-delete-input 1170,39157 (defun pg-get-old-input 1183,39495 (defun pg-restore-input 1197,39886 (defun pg-search-start 1208,40176 (defun pg-regexp-arg 1220,40668 (defun pg-search-arg 1232,41116 (defun pg-previous-matching-input-string-position 1246,41533 (defun pg-previous-matching-input 1273,42698 (defun pg-next-matching-input 1292,43534 (defvar pg-matching-input-from-input-string 1300,43917 (defun pg-previous-matching-input-from-input 1304,44031 (defun pg-next-matching-input-from-input 1322,44796 (defun pg-add-to-input-history 1333,45175 (defun pg-remove-from-input-history 1345,45628 (defun pg-clear-input-ring 1356,46011 generic/pg-vars.el,1106 (defvar proof-assistant-cusgrp 20,379 (defvar proof-assistant-internals-cusgrp 26,641 (defvar proof-assistant 32,912 (defvar proof-assistant-symbol 37,1134 (defvar proof-mode-for-shell 50,1678 (defvar proof-mode-for-response 55,1870 (defvar proof-mode-for-goals 60,2097 (defvar proof-mode-for-script 65,2287 (defvar proof-ready-for-assistant-hook 70,2465 (defvar proof-shell-busy 80,2752 (defvar proof-included-files-list 85,2908 (defvar proof-script-buffer 107,3921 (defvar proof-previous-script-buffer 110,4013 (defvar proof-shell-buffer 114,4184 (defvar proof-goals-buffer 117,4270 (defvar proof-response-buffer 120,4325 (defvar proof-trace-buffer 123,4386 (defvar proof-thms-buffer 127,4540 (defvar proof-shell-error-or-interrupt-seen 131,4695 (defvar pg-response-next-error 136,4919 (defvar proof-shell-proof-completed 139,5026 (defvar proof-terminal-string 151,5570 (defvar proof-shell-last-output 161,5760 (defvar proof-assistant-settings 165,5901 (defvar pg-tracing-slow-mode 172,6264 (defvar proof-nesting-depth 175,6353 (defvar proof-last-theorem-dependencies 182,6588 generic/pg-xml.el,1141 (defalias 'pg-xml-error pg-xml-error24,625 (defun pg-xml-parse-string 47,1267 (defun pg-xml-parse-buffer 58,1593 (defun pg-xml-get-attr 80,2326 (defun pg-xml-child-elts 88,2628 (defun pg-xml-child-elt 93,2833 (defun pg-xml-get-child 101,3115 (defun pg-xml-get-text-content 111,3487 (defmacro pg-xml-attr 122,3837 (defmacro pg-xml-node 124,3899 (defconst pg-xml-header127,3991 (defun pg-xml-string-of 131,4067 (defun pg-xml-output-internal 142,4434 (defun pg-xml-cdata 176,5584 (defun pg-pgip-get-icon 184,5777 (defsubst pg-pgip-get-name 188,5925 (defsubst pg-pgip-get-version 191,6042 (defsubst pg-pgip-get-descr 194,6165 (defsubst pg-pgip-get-thmname 197,6284 (defsubst pg-pgip-get-thyname 200,6407 (defsubst pg-pgip-get-url 203,6530 (defsubst pg-pgip-get-srcid 206,6645 (defsubst pg-pgip-get-proverid 209,6764 (defsubst pg-pgip-get-symname 212,6889 (defsubst pg-pgip-get-prefcat 215,7009 (defsubst pg-pgip-get-default 218,7137 (defsubst pg-pgip-get-objtype 221,7260 (defsubst pg-pgip-get-value 224,7383 (defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext227,7453 (defun pg-pgip-get-pgmltext 229,7512 generic/proof-auxmodes.el,149 (defun proof-mmm-support-available 23,575 (defun proof-maths-menu-support-available 47,1193 (defun proof-unicode-tokens-support-available 66,1807 generic/proof-config.el,11009 (defgroup proof-user-options 85,3024 (defun proof-set-value 94,3221 (defcustom proof-electric-terminator-enable 127,4340 (defcustom proof-toolbar-enable 139,4872 (defcustom proof-imenu-enable 145,5045 (defcustom pg-show-hints 151,5216 (defcustom proof-output-fontify-enable 156,5351 (defcustom proof-trace-output-slow-catchup 166,5734 (defcustom proof-strict-state-preserving 176,6231 (defcustom proof-strict-read-only 189,6840 (defcustom proof-allow-undo-in-read-only 198,7189 (defcustom proof-three-window-enable 206,7522 (defcustom proof-multiple-frames-enable 225,8272 (defcustom proof-delete-empty-windows 234,8605 (defcustom proof-shrink-windows-tofit 245,9136 (defcustom proof-toolbar-use-button-enablers 252,9408 (defcustom proof-query-file-save-when-activating-scripting260,9743 (defcustom proof-one-command-per-line276,10463 (defcustom proof-prog-name-ask283,10690 (defcustom proof-prog-name-guess289,10850 (defcustom proof-tidy-response297,11109 (defcustom proof-keep-response-history311,11572 (defcustom pg-input-ring-size 321,11960 (defcustom proof-general-debug 326,12112 (defcustom proof-experimental-features 336,12484 (defcustom proof-follow-mode 350,13019 (defcustom proof-auto-action-when-deactivating-scripting 374,14199 (defcustom proof-script-command-separator 397,15148 (defcustom proof-rsh-command 405,15440 (defcustom proof-disappearing-proofs 421,15990 (defgroup proof-faces 448,16636 (defconst pg-defface-window-systems 455,16818 (defmacro proof-face-specs 468,17363 (defface proof-queue-face483,17815 (defface proof-locked-face491,18093 (defface proof-declaration-name-face504,18596 (defface proof-tacticals-name-face513,18882 (defface proof-tactics-name-face522,19144 (defface proof-error-face531,19409 (defface proof-warning-face539,19615 (defface proof-eager-annotation-face548,19872 (defface proof-debug-message-face556,20090 (defface proof-boring-face564,20289 (defface proof-mouse-highlight-face572,20481 (defface proof-highlight-dependent-face580,20677 (defface proof-highlight-dependency-face588,20886 (defface proof-active-area-face596,21083 (defconst proof-face-compat-doc 605,21479 (defconst proof-queue-face 606,21559 (defconst proof-locked-face 607,21627 (defconst proof-declaration-name-face 608,21697 (defconst proof-tacticals-name-face 609,21787 (defconst proof-tactics-name-face 610,21873 (defconst proof-error-face 611,21955 (defconst proof-warning-face 612,22023 (defconst proof-eager-annotation-face 613,22095 (defconst proof-debug-message-face 614,22185 (defconst proof-boring-face 615,22269 (defconst proof-mouse-highlight-face 616,22339 (defconst proof-highlight-dependent-face 617,22427 (defconst proof-highlight-dependency-face 618,22523 (defconst proof-active-area-face 619,22621 (defgroup prover-config 632,22765 (defcustom proof-guess-command-line 674,24076 (defcustom proof-assistant-home-page 689,24571 (defcustom proof-context-command 695,24741 (defcustom proof-info-command 700,24875 (defcustom proof-showproof-command 707,25146 (defcustom proof-goal-command 712,25282 (defcustom proof-save-command 720,25579 (defcustom proof-find-theorems-command 728,25888 (defcustom proof-assistant-true-value 735,26198 (defcustom proof-assistant-false-value 741,26388 (defcustom proof-assistant-format-int-fn 747,26582 (defcustom proof-assistant-format-string-fn 754,26831 (defcustom proof-assistant-setting-format 761,27098 (defgroup proof-script 783,27793 (defcustom proof-terminal-char 788,27923 (defcustom proof-script-sexp-commands 798,28310 (defcustom proof-script-command-end-regexp 809,28767 (defcustom proof-script-command-start-regexp 827,29586 (defcustom proof-script-use-old-parser 838,30047 (defcustom proof-script-integral-proofs 850,30533 (defcustom proof-script-fly-past-comments 865,31189 (defcustom proof-script-parse-function 870,31360 (defcustom proof-script-comment-start 888,32003 (defcustom proof-script-comment-start-regexp 899,32440 (defcustom proof-script-comment-end 907,32757 (defcustom proof-script-comment-end-regexp 919,33179 (defcustom pg-insert-output-as-comment-fn 927,33490 (defcustom proof-string-start-regexp 933,33742 (defcustom proof-string-end-regexp 938,33907 (defcustom proof-case-fold-search 943,34068 (defcustom proof-save-command-regexp 952,34478 (defcustom proof-save-with-hole-regexp 957,34588 (defcustom proof-save-with-hole-result 969,35042 (defcustom proof-goal-command-regexp 979,35493 (defcustom proof-goal-with-hole-regexp 988,35881 (defcustom proof-goal-with-hole-result 1000,36322 (defcustom proof-non-undoables-regexp 1009,36709 (defcustom proof-nested-undo-regexp 1020,37164 (defcustom proof-ignore-for-undo-count 1036,37876 (defcustom proof-script-next-entity-regexps 1044,38179 (defcustom proof-script-find-next-entity-fn1088,39914 (defcustom proof-script-imenu-generic-expression 1108,40752 (defcustom proof-goal-command-p 1126,41605 (defcustom proof-really-save-command-p 1153,43042 (defcustom proof-completed-proof-behaviour 1165,43504 (defcustom proof-count-undos-fn 1193,44860 (defconst proof-no-command 1205,45409 (defcustom proof-find-and-forget-fn 1210,45614 (defcustom proof-forget-id-command 1227,46326 (defcustom pg-topterm-goalhyplit-fn 1237,46684 (defcustom proof-kill-goal-command 1249,47219 (defcustom proof-undo-n-times-cmd 1263,47720 (defcustom proof-nested-goals-history-p 1277,48268 (defcustom proof-state-preserving-p 1286,48605 (defcustom proof-activate-scripting-hook 1296,49075 (defcustom proof-deactivate-scripting-hook 1315,49854 (defcustom proof-indent 1328,50219 (defcustom proof-indent-hang 1333,50326 (defcustom proof-indent-enclose-offset 1338,50452 (defcustom proof-indent-open-offset 1343,50594 (defcustom proof-indent-close-offset 1348,50731 (defcustom proof-indent-any-regexp 1353,50869 (defcustom proof-indent-inner-regexp 1358,51029 (defcustom proof-indent-enclose-regexp 1363,51183 (defcustom proof-indent-open-regexp 1368,51337 (defcustom proof-indent-close-regexp 1373,51489 (defcustom proof-script-font-lock-keywords 1379,51643 (defcustom proof-script-syntax-table-entries 1387,51972 (defcustom proof-script-span-context-menu-extensions 1405,52369 (defgroup proof-shell 1431,53129 (defcustom proof-prog-name 1441,53300 (defcustom proof-shell-auto-terminate-commands 1452,53718 (defcustom proof-shell-pre-sync-init-cmd 1461,54115 (defcustom proof-shell-init-cmd 1475,54673 (defcustom proof-shell-restart-cmd 1486,55142 (defcustom proof-shell-quit-cmd 1491,55297 (defcustom proof-shell-quit-timeout 1496,55464 (defcustom proof-shell-cd-cmd 1506,55912 (defcustom proof-shell-start-silent-cmd 1523,56577 (defcustom proof-shell-stop-silent-cmd 1532,56951 (defcustom proof-shell-silent-threshold 1541,57284 (defcustom proof-shell-inform-file-processed-cmd 1549,57618 (defcustom proof-shell-inform-file-retracted-cmd 1570,58540 (defcustom proof-auto-multiple-files 1598,59806 (defcustom proof-cannot-reopen-processed-files 1613,60527 (defcustom proof-shell-require-command-regexp 1627,61193 (defcustom proof-done-advancing-require-function 1638,61655 (defcustom proof-shell-quiet-errors 1644,61890 (defcustom proof-shell-prompt-pattern 1657,62224 (defcustom proof-shell-wakeup-char 1667,62645 (defcustom proof-shell-annotated-prompt-regexp 1673,62876 (defcustom proof-shell-abort-goal-regexp 1689,63510 (defcustom proof-shell-error-regexp 1694,63645 (defcustom proof-shell-truncate-before-error 1714,64439 (defcustom pg-next-error-regexp 1728,64982 (defcustom pg-next-error-filename-regexp 1743,65591 (defcustom pg-next-error-extract-filename 1767,66624 (defcustom proof-shell-interrupt-regexp 1774,66867 (defcustom proof-shell-proof-completed-regexp 1788,67458 (defcustom proof-shell-clear-response-regexp 1801,67966 (defcustom proof-shell-clear-goals-regexp 1808,68265 (defcustom proof-shell-start-goals-regexp 1815,68558 (defcustom proof-shell-end-goals-regexp 1823,68925 (defcustom proof-shell-eager-annotation-start 1829,69167 (defcustom proof-shell-eager-annotation-start-length 1852,70187 (defcustom proof-shell-eager-annotation-end 1863,70613 (defcustom proof-shell-assumption-regexp 1879,71288 (defcustom proof-shell-process-file 1889,71691 (defcustom proof-shell-retract-files-regexp 1911,72647 (defcustom proof-shell-compute-new-files-list 1920,72983 (defcustom pg-use-specials-for-fontify 1932,73531 (defcustom pg-special-char-regexp 1940,73879 (defcustom proof-shell-set-elisp-variable-regexp 1946,74024 (defcustom proof-shell-match-pgip-cmd 1979,75535 (defcustom proof-shell-issue-pgip-cmd 1988,75864 (defcustom proof-shell-query-dependencies-cmd 1997,76220 (defcustom proof-shell-theorem-dependency-list-regexp 2004,76480 (defcustom proof-shell-theorem-dependency-list-split 2020,77140 (defcustom proof-shell-show-dependency-cmd 2029,77563 (defcustom proof-shell-identifier-under-mouse-cmd 2036,77832 (defcustom proof-shell-trace-output-regexp 2059,78913 (defcustom proof-shell-thms-output-regexp 2073,79371 (defcustom proof-shell-unicode 2086,79757 (defcustom proof-shell-filename-escapes 2094,80077 (defcustom proof-shell-process-connection-type2111,80757 (defcustom proof-shell-strip-crs-from-input 2134,81803 (defcustom proof-shell-strip-crs-from-output 2146,82288 (defcustom proof-shell-insert-hook 2154,82656 (defcustom proof-shell-handle-delayed-output-hook2194,84615 (defcustom proof-shell-handle-error-or-interrupt-hook2200,84830 (defcustom proof-shell-pre-interrupt-hook2218,85579 (defcustom proof-shell-process-output-system-specific 2226,85851 (defcustom proof-state-change-hook 2245,86715 (defcustom proof-shell-font-lock-keywords 2256,87097 (defcustom proof-shell-syntax-table-entries 2264,87429 (defgroup proof-goals 2282,87801 (defcustom pg-subterm-first-special-char 2287,87922 (defcustom pg-subterm-anns-use-stack 2295,88234 (defcustom pg-goals-change-goal 2304,88533 (defcustom pbp-goal-command 2309,88649 (defcustom pbp-hyp-command 2314,88805 (defcustom pg-subterm-help-cmd 2319,88967 (defcustom pg-goals-error-regexp 2326,89203 (defcustom proof-shell-result-start 2331,89363 (defcustom proof-shell-result-end 2337,89597 (defcustom pg-subterm-start-char 2343,89810 (defcustom pg-subterm-sep-char 2357,90390 (defcustom pg-subterm-end-char 2363,90569 (defcustom pg-topterm-regexp 2369,90726 (defcustom proof-goals-font-lock-keywords 2386,91328 (defcustom proof-resp-font-lock-keywords 2400,92013 (defcustom pg-before-fontify-output-hook 2412,92593 (defcustom pg-after-fontify-output-hook 2420,92953 (defgroup proof-x-symbol 2432,93233 (defcustom proof-xsym-extra-modes 2437,93361 (defcustom proof-xsym-font-lock-keywords 2450,93989 (defcustom proof-xsym-activate-command 2458,94366 (defcustom proof-xsym-deactivate-command 2465,94601 (defcustom proof-general-name 2482,94886 (defcustom proof-general-home-page2487,95043 (defcustom proof-unnamed-theorem-name2493,95203 (defcustom proof-universal-keys2499,95387 generic/proof-depends.el,824 (defvar proof-thm-names-of-files 23,624 (defvar proof-def-names-of-files 29,908 (defun proof-depends-module-name-for-buffer 38,1212 (defun proof-depends-module-of 48,1654 (defun proof-depends-names-in-same-file 56,1948 (defun proof-depends-process-dependencies 75,2568 (defun proof-dependency-in-span-context-menu 128,4317 (defun proof-dep-alldeps-menu 151,5220 (defun proof-dep-make-alldeps-menu 157,5447 (defun proof-dep-split-deps 175,5943 (defun proof-dep-make-submenu 196,6642 (defun proof-make-highlight-depts-menu 206,6995 (defun proof-goto-dependency 216,7299 (defun proof-show-dependency 222,7522 (defconst pg-dep-span-priority 229,7812 (defconst pg-ordinary-span-priority 230,7848 (defun proof-highlight-depcs 232,7890 (defun proof-highlight-depts 242,8320 (defun proof-dep-unhighlight 253,8794 generic/proof-easy-config.el,192 (defconst proof-easy-config-derived-modes-table16,543 (defun proof-easy-config-define-derived-modes 23,949 (defun proof-easy-config-check-setup 56,2359 (defmacro proof-easy-config 88,3694 generic/proof-indent.el,219 (defun proof-indent-indent 14,411 (defun proof-indent-offset 23,677 (defun proof-indent-inner-p 40,1277 (defun proof-indent-goto-prev 49,1584 (defun proof-indent-calculate 56,1917 (defun proof-indent-line 76,2639 generic/proof-maths-menu.el,83 (defun proof-maths-menu-set-global 31,994 (defun proof-maths-menu-enable 45,1450 generic/proof-menu.el,2101 (defvar proof-display-some-buffers-count 17,437 (defun proof-display-some-buffers 19,482 (defun proof-menu-define-keys 78,2684 (defun proof-menu-define-main 141,5720 (defvar proof-menu-favourites 150,5908 (defun proof-menu-define-specific 154,6030 (defun proof-assistant-menu-update 192,7056 (defvar proof-help-menu208,7639 (defvar proof-show-hide-menu216,7917 (defvar proof-buffer-menu225,8230 (defun proof-keep-response-history 288,10496 (defconst proof-quick-opts-menu296,10806 (defun proof-quick-opts-vars 449,16899 (defun proof-quick-opts-changed-from-defaults-p 475,17691 (defun proof-quick-opts-changed-from-saved-p 479,17796 (defun proof-quick-opts-save 490,18148 (defun proof-quick-opts-reset 495,18316 (defconst proof-config-menu507,18584 (defconst proof-advanced-menu514,18763 (defvar proof-menu 527,19198 (defun proof-main-menu 536,19482 (defun proof-aux-menu 547,19748 (defun proof-menu-define-favourites-menu 563,20095 (defun proof-def-favourite 583,20751 (defvar proof-make-favourite-cmd-history 606,21726 (defvar proof-make-favourite-menu-history 609,21811 (defun proof-save-favourites 612,21897 (defun proof-del-favourite 617,22045 (defun proof-read-favourite 634,22606 (defun proof-add-favourite 659,23409 (defvar proof-menu-settings 686,24460 (defun proof-menu-define-settings-menu 689,24534 (defun proof-menu-entry-name 709,25278 (defun proof-menu-entry-for-setting 721,25750 (defun proof-settings-vars 739,26240 (defun proof-settings-changed-from-defaults-p 744,26417 (defun proof-settings-changed-from-saved-p 748,26523 (defun proof-settings-save 752,26626 (defun proof-settings-reset 757,26793 (defun proof-defpacustom-fn 764,27038 (defmacro defpacustom 840,29922 (defun proof-assistant-invisible-command-ifposs 855,30749 (defun proof-maybe-askprefs 877,31724 (defun proof-assistant-settings-cmd 884,31928 (defvar proof-assistant-format-table 901,32588 (defun proof-assistant-format-bool 909,32957 (defun proof-assistant-format-int 912,33070 (defun proof-assistant-format-string 915,33162 (defun proof-assistant-format 918,33260 generic/proof-mmm.el,70 (defun proof-mmm-set-global 41,1516 (defun proof-mmm-enable 56,2057 generic/proof-script.el,5112 (defvar proof-element-counters 28,718 (deflocal proof-active-buffer-fake-minor-mode 34,858 (deflocal proof-script-buffer-file-name 37,984 (deflocal pg-script-portions 44,1394 (defun proof-next-element-count 54,1630 (defun proof-element-id 63,1957 (defun proof-next-element-id 67,2126 (deflocal proof-script-last-entity 81,2443 (defun proof-script-find-next-entity 88,2723 (deflocal proof-locked-span 164,5465 (deflocal proof-queue-span 171,5731 (defun proof-span-read-only 183,6245 (defun proof-strict-read-only 190,6502 (defsubst proof-set-locked-endpoints 219,7693 (defsubst proof-detach-queue 223,7837 (defsubst proof-detach-locked 227,7969 (defsubst proof-set-queue-start 231,8105 (defsubst proof-set-locked-end 235,8231 (defsubst proof-set-queue-end 248,8716 (defun proof-init-segmentation 259,9013 (defun proof-restart-buffers 292,10408 (defun proof-script-buffers-with-spans 314,11340 (defun proof-script-remove-all-spans-and-deactivate 324,11696 (defun proof-script-clear-queue-spans 328,11884 (defun proof-unprocessed-begin 347,12445 (defun proof-script-end 355,12699 (defun proof-queue-or-locked-end 364,13000 (defun proof-locked-end 379,13678 (defun proof-locked-region-full-p 396,14063 (defun proof-locked-region-empty-p 405,14335 (defun proof-only-whitespace-to-locked-region-p 409,14485 (defun proof-in-locked-region-p 422,15121 (defun proof-goto-end-of-locked 434,15384 (defun proof-goto-end-of-locked-if-pos-not-visible-in-window 451,16143 (defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 462,16624 (defun proof-end-of-locked-visible-p 476,17277 (defun proof-goto-end-of-queue-or-locked-if-not-visible 485,17728 (defvar pg-idioms 504,18378 (defvar pg-visibility-specs 507,18474 (defconst pg-default-invisibility-spec 512,18681 (defun pg-clear-script-portions 516,18821 (defun pg-add-script-element 530,19298 (defun pg-remove-script-element 533,19374 (defsubst pg-visname 541,19652 (defun pg-add-element 545,19797 (defun pg-open-invisible-span 579,21426 (defun pg-remove-element 590,21789 (defun pg-make-element-invisible 597,22059 (defun pg-make-element-visible 603,22316 (defun pg-toggle-element-visibility 608,22495 (defun pg-redisplay-for-gnuemacs 616,22825 (defun pg-show-all-portions 623,23096 (defun pg-show-all-proofs 641,23767 (defun pg-hide-all-proofs 646,23895 (defun pg-add-proof-element 651,24026 (defun pg-span-name 665,24646 (defvar pg-span-context-menu-keymap686,25353 (defun pg-set-span-helphighlights 699,25724 (defun proof-complete-buffer-atomic 727,26653 (defun proof-register-possibly-new-processed-file 768,28568 (defun proof-inform-prover-file-retracted 819,30696 (defun proof-auto-retract-dependencies 838,31482 (defun proof-unregister-buffer-file-name 892,34022 (defun proof-protected-process-or-retract 938,35845 (defun proof-deactivate-scripting-auto 965,37015 (defun proof-deactivate-scripting 974,37373 (defun proof-activate-scripting 1111,42778 (defun proof-toggle-active-scripting 1233,48210 (defun proof-done-advancing 1274,49571 (defun proof-done-advancing-comment 1369,53219 (defun proof-done-advancing-save 1388,53961 (defun proof-make-goalsave 1481,57576 (defun proof-get-name-from-goal 1496,58319 (defun proof-done-advancing-autosave 1515,59345 (defun proof-done-advancing-other 1580,61891 (defun proof-segment-up-to-parser 1608,62850 (defun proof-script-generic-parse-find-comment-end 1671,64926 (defun proof-script-generic-parse-cmdend 1680,65342 (defun proof-script-generic-parse-cmdstart 1705,66237 (defun proof-script-generic-parse-sexp 1768,68945 (defun proof-cmdstart-add-segment-for-cmd 1792,69881 (defun proof-segment-up-to-cmdstart 1844,72080 (defun proof-segment-up-to-cmdend 1905,74440 (defun proof-semis-to-vanillas 1977,77105 (defun proof-script-new-command-advance 2016,78431 (defun proof-script-next-command-advance 2058,80172 (defun proof-assert-until-point-interactive 2070,80613 (defun proof-assert-until-point 2096,81735 (defun proof-assert-next-command2149,84167 (defun proof-goto-point 2197,86430 (defun proof-insert-pbp-command 2215,86971 (defun proof-insert-sendback-command 2229,87440 (defun proof-done-retracting 2255,88330 (defun proof-setup-retract-action 2291,89816 (defun proof-last-goal-or-goalsave 2301,90299 (defun proof-retract-target 2324,91139 (defun proof-retract-until-point-interactive 2409,94780 (defun proof-retract-until-point 2417,95165 (define-derived-mode proof-mode 2460,96914 (defun proof-script-set-visited-file-name 2510,98841 (defun proof-script-set-buffer-hooks 2534,99843 (defun proof-script-kill-buffer-fn 2542,100261 (defun proof-config-done-related 2586,102083 (defun proof-generic-goal-command-p 2656,104561 (defun proof-generic-state-preserving-p 2661,104773 (defun proof-generic-count-undos 2670,105290 (defun proof-generic-find-and-forget 2699,106320 (defconst proof-script-important-settings2750,108145 (defun proof-config-done 2765,108698 (defun proof-setup-parsing-mechanism 2853,111816 (defun proof-setup-imenu 2897,113669 (defun proof-setup-func-menu 2914,114274 generic/proof-shell.el,3314 (defvar proof-marker 28,649 (defvar proof-action-list 31,746 (defvar proof-shell-silent 39,922 (defvar proof-shell-last-prompt 46,1213 (defvar proof-shell-last-output-kind 50,1384 (defvar proof-shell-delayed-output 71,2206 (defvar proof-shell-delayed-output-kind 74,2327 (defcustom proof-shell-active-scripting-indicator83,2530 (defun proof-shell-ready-prover 135,3998 (defun proof-shell-live-buffer 149,4538 (defun proof-shell-available-p 156,4773 (defun proof-grab-lock 162,4996 (defun proof-release-lock 179,5708 (defcustom proof-shell-fiddle-frames 199,6259 (defun proof-shell-set-text-representation 205,6482 (defun proof-shell-start 216,6944 (defvar proof-shell-kill-function-hooks 426,14491 (defun proof-shell-kill-function 429,14589 (defun proof-shell-clear-state 518,18392 (defun proof-shell-exit 533,18835 (defun proof-shell-bail-out 545,19280 (defun proof-shell-restart 554,19757 (defvar proof-shell-no-response-display 596,21141 (defvar proof-shell-urgent-message-marker 599,21245 (defvar proof-shell-urgent-message-scanner 602,21366 (defun proof-shell-handle-output 606,21493 (defun proof-shell-handle-delayed-output 649,23186 (defvar proof-shell-no-error-display 677,24229 (defun proof-shell-handle-error 683,24433 (defun proof-shell-handle-interrupt 701,25269 (defun proof-shell-error-or-interrupt-action 715,25882 (defun proof-goals-pos 740,27027 (defun proof-pbp-focus-on-first-goal 745,27232 (defsubst proof-shell-string-match-safe 757,27762 (defun proof-shell-process-output 762,27930 (defconst proof-shell-insert-space-fudge 873,32570 (defun proof-shell-insert 885,32922 (defun proof-shell-command-queue-item 958,35874 (defun proof-shell-set-silent 963,36031 (defun proof-shell-start-silent-item 969,36250 (defun proof-shell-clear-silent 975,36442 (defun proof-shell-stop-silent-item 981,36664 (defun proof-shell-should-be-silent 988,36936 (defun proof-append-alist 1001,37492 (defun proof-start-queue 1060,39729 (defun proof-extend-queue 1071,40078 (defun proof-shell-exec-loop 1080,40457 (defun proof-shell-insert-loopback-cmd 1145,43045 (defun proof-shell-message 1173,44371 (defun proof-shell-process-urgent-message 1179,44587 (defun proof-shell-strip-eager-annotations 1311,49852 (defvar proof-shell-minibuffer-urgent-interactive-input-history 1322,50188 (defun proof-shell-minibuffer-urgent-interactive-input 1324,50258 (defun proof-shell-process-urgent-messages 1334,50617 (defun proof-shell-filter 1408,53721 (defun proof-shell-filter-process-output 1569,60354 (defvar pg-last-tracing-output-time 1622,62408 (defconst pg-slow-mode-duration 1625,62514 (defconst pg-fast-tracing-mode-threshold 1628,62596 (defvar pg-tracing-cleanup-timer 1631,62724 (defun pg-tracing-tight-loop 1633,62763 (defun pg-finish-tracing-display 1676,64481 (defun proof-shell-dont-show-annotations 1689,64787 (defun proof-shell-show-annotations 1705,65308 (defun proof-shell-wait 1727,65835 (defun proof-done-invisible 1746,66744 (defun proof-shell-invisible-command 1752,66916 (defun proof-shell-invisible-cmd-get-result 1786,68181 (defun proof-shell-invisible-command-invisible-result 1804,68877 (define-derived-mode proof-shell-mode 1823,69307 (defconst proof-shell-important-settings1893,71973 (defun proof-shell-config-done 1899,72088 generic/proof-site.el,504 (defconst proof-assistant-table-default23,728 (defconst proof-general-short-version 61,2156 (defconst proof-general-version-year 67,2344 (defgroup proof-general 74,2497 (defgroup proof-general-internals 79,2605 (defun proof-home-directory-fn 92,2993 (defcustom proof-home-directory103,3364 (defcustom proof-images-directory112,3731 (defcustom proof-info-directory118,3933 (defcustom proof-assistant-table145,5079 (defcustom proof-assistants 180,6195 (defun proof-ready-for-assistant 208,7340 generic/proof-splash.el,726 (defcustom proof-splash-enable 17,319 (defcustom proof-splash-time 22,471 (defcustom proof-splash-contents30,756 (defconst proof-splash-startup-msg 58,1775 (defconst proof-splash-welcome 67,2154 (defun proof-get-image 86,2701 (defvar proof-splash-timeout-conf 125,4052 (defun proof-splash-centre-spaces 128,4165 (defun proof-splash-remove-screen 156,5335 (defun proof-splash-remove-buffer 176,6056 (defvar proof-splash-seen 192,6720 (defun proof-splash-display-screen 196,6837 (defun proof-splash-message 271,9991 (defun proof-splash-timeout-waiter 284,10435 (defvar proof-splash-old-frame-title-format 300,11131 (defun proof-splash-set-frame-titles 302,11181 (defun proof-splash-unset-frame-titles 311,11497 generic/proof-syntax.el,981 (defun proof-ids-to-regexp 15,435 (defun proof-anchor-regexp 21,711 (defconst proof-no-regexp25,813 (defun proof-regexp-alt 30,906 (defun proof-regexp-region 39,1192 (defun proof-re-search-forward-region 48,1615 (defun proof-search-forward 61,2110 (defun proof-replace-regexp-in-string 67,2362 (defun proof-re-search-forward 73,2616 (defun proof-re-search-backward 79,2877 (defun proof-string-match 85,3141 (defun proof-string-match-safe 91,3373 (defun proof-stringfn-match 95,3578 (defun proof-looking-at 102,3838 (defun proof-looking-at-safe 108,4028 (defun proof-looking-at-syntactic-context 112,4168 (defsubst proof-replace-string 124,4531 (defsubst proof-replace-regexp 129,4735 (defsubst proof-replace-regexp-nocasefold 134,4944 (defvar proof-id 142,5226 (defun proof-ids 148,5446 (defun proof-zap-commas 161,6002 (defun proof-format 179,6571 (defun proof-format-filename 198,7210 (defun proof-insert 247,8681 (defun proof-splice-separator 284,9697 generic/proof-toolbar.el,2874 (defun proof-toolbar-function 42,1325 (defun proof-toolbar-icon 45,1422 (defun proof-toolbar-enabler 48,1523 (defun proof-toolbar-function-with-enabler 51,1631 (defun proof-toolbar-make-icon 58,1804 (defun proof-toolbar-make-toolbar-item 76,2404 (defvar proof-toolbar 115,3780 (deflocal proof-toolbar-itimer 119,3909 (defun proof-toolbar-setup 123,4019 (defun proof-toolbar-build 166,5562 (defalias 'proof-toolbar-enable proof-toolbar-enable230,7673 (defun proof-toolbar-setup-refresh 241,7977 (defun proof-toolbar-disable-refresh 262,8798 (deflocal proof-toolbar-refresh-flag 270,9188 (defun proof-toolbar-refresh 276,9459 (defvar proof-toolbar-enablers280,9604 (defvar proof-toolbar-enablers-last-state286,9780 (defun proof-toolbar-really-refresh 290,9871 (defun proof-toolbar-undo-enable-p 345,11765 (defalias 'proof-toolbar-undo proof-toolbar-undo350,11913 (defun proof-toolbar-delete-enable-p 356,12032 (defalias 'proof-toolbar-delete proof-toolbar-delete362,12206 (defun proof-toolbar-lockedend-enable-p 369,12342 (defalias 'proof-toolbar-lockedend proof-toolbar-lockedend372,12392 (defun proof-toolbar-next-enable-p 381,12480 (defalias 'proof-toolbar-next proof-toolbar-next385,12587 (defun proof-toolbar-goto-enable-p 392,12681 (defalias 'proof-toolbar-goto proof-toolbar-goto395,12754 (defun proof-toolbar-retract-enable-p 402,12830 (defalias 'proof-toolbar-retract proof-toolbar-retract406,12941 (defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p413,13020 (defalias 'proof-toolbar-use proof-toolbar-use414,13088 (defun proof-toolbar-restart-enable-p 420,13166 (defalias 'proof-toolbar-restart proof-toolbar-restart425,13327 (defun proof-toolbar-goal-enable-p 431,13405 (defalias 'proof-toolbar-goal proof-toolbar-goal438,13638 (defun proof-toolbar-qed-enable-p 445,13710 (defalias 'proof-toolbar-qed proof-toolbar-qed451,13862 (defun proof-toolbar-state-enable-p 457,13934 (defalias 'proof-toolbar-state proof-toolbar-state460,14005 (defun proof-toolbar-context-enable-p 466,14074 (defalias 'proof-toolbar-context proof-toolbar-context469,14147 (defun proof-toolbar-info-enable-p 477,14307 (defalias 'proof-toolbar-info proof-toolbar-info480,14351 (defun proof-toolbar-command-enable-p 486,14420 (defalias 'proof-toolbar-command proof-toolbar-command489,14491 (defun proof-toolbar-help-enable-p 495,14571 (defun proof-toolbar-help 498,14616 (defun proof-toolbar-find-enable-p 506,14710 (defalias 'proof-toolbar-find proof-toolbar-find509,14779 (defun proof-toolbar-visibility-enable-p 515,14877 (defalias 'proof-toolbar-visibility proof-toolbar-visibility518,14977 (defun proof-toolbar-interrupt-enable-p 524,15065 (defalias 'proof-toolbar-interrupt proof-toolbar-interrupt527,15129 (defun proof-toolbar-make-menu-item 536,15318 (defun proof-toolbar-scripting-menu 559,16018 generic/proof-unicode-tokens.el,476 (defvar proof-unicode-tokens-initialised 17,496 (defun proof-unicode-tokens-init 20,603 (defun proof-unicode-tokens-enable 43,1231 (defun proof-unicode-tokens-set-global 57,1851 (defun proof-token-name-alist 76,2512 (defun proof-shortcut-alist 91,3164 (defun proof-unicode-tokens-activate-prover 103,3501 (defun proof-unicode-tokens-deactivate-prover 110,3744 (defun proof-unicode-tokens-shell-config 121,4176 (defun proof-unicode-tokens-encode-shell-input 131,4573 generic/proof-utils.el,2116 (defmacro deflocal 63,1874 (defmacro proof-with-current-buffer-if-exists 70,2112 (deflocal proof-buffer-type 76,2322 (defmacro proof-with-script-buffer 82,2602 (defmacro proof-map-buffers 93,2989 (defmacro proof-sym 98,3174 (defsubst proof-try-require 103,3335 (defun proof-save-some-buffers 116,3666 (defmacro proof-ass-sym 165,5267 (defmacro proof-ass-symv 171,5526 (defmacro proof-ass 177,5784 (defun proof-defpgcustom-fn 183,6036 (defun undefpgcustom 204,6907 (defmacro defpgcustom 210,7131 (defun proof-defpgdefault-fn 221,7549 (defmacro defpgdefault 235,8007 (defmacro defpgfun 246,8369 (defmacro proof-eval-when-ready-for-assistant 256,8634 (defun proof-file-truename 269,9029 (defun proof-file-to-buffer 273,9212 (defun proof-files-to-buffers 284,9541 (defun proof-buffers-in-mode 291,9824 (defun pg-save-from-death 305,10274 (defun proof-define-keys 324,10891 (deflocal proof-font-lock-keywords 353,11890 (defun proof-font-lock-configure-defaults 359,12147 (defun proof-font-lock-clear-font-lock-vars 405,14298 (defun proof-font-lock-set-font-lock-vars 411,14510 (defun proof-fontify-region 415,14666 (defun pg-remove-specials 477,17068 (defun pg-remove-specials-in-string 487,17406 (defun proof-fontify-buffer 494,17593 (defun proof-warn-if-unset 507,17834 (defun proof-get-window-for-buffer 512,18052 (defun proof-display-and-keep-buffer 563,20360 (defun proof-clean-buffer 595,21667 (defun proof-message 610,22288 (defun proof-warning 615,22501 (defun pg-internal-warning 621,22783 (defun proof-debug 629,23102 (defun proof-switch-to-buffer 644,23773 (defun proof-resize-window-tofit 677,25462 (defun proof-submit-bug-report 777,29474 (defun proof-deftoggle-fn 813,30853 (defmacro proof-deftoggle 828,31506 (defun proof-defintset-fn 835,31880 (defmacro proof-defintset 851,32584 (defun proof-defstringset-fn 858,32961 (defmacro proof-defstringset 871,33587 (defmacro proof-defshortcut 885,34044 (defmacro proof-definvisible 900,34683 (defun pg-custom-save-vars 928,35660 (defun pg-custom-reset-vars 946,36383 (defun proof-locate-executable 959,36720 generic/proof-x-symbol.el,580 (defvar proof-x-symbol-initialized 52,2005 (defun proof-x-symbol-tokenlang-file 55,2100 (defun proof-x-symbol-support-maybe-available 61,2282 (defun proof-x-symbol-initialize 81,3011 (defun proof-x-symbol-enable 164,6277 (defun proof-x-symbol-refresh-output-buffers 186,7158 (defun proof-x-symbol-mode-associated-buffers 201,7900 (defun proof-x-symbol-decode-region 219,8438 (defun proof-x-symbol-encode-shell-input 240,9435 (defun proof-x-symbol-set-language 257,10026 (defun proof-x-symbol-shell-config 262,10197 (defun proof-x-symbol-config-output-buffer 311,12443 lib/bufhist.el,1100 (defun bufhist-ring-update 32,1226 (defgroup bufhist 41,1548 (defcustom bufhist-ring-size 45,1629 (defvar bufhist-ring 50,1740 (defvar bufhist-ring-pos 53,1814 (defvar bufhist-lastswitch-modified-tick 56,1893 (defvar bufhist-read-only-history 59,1999 (defvar bufhist-saved-mode-line-format 62,2070 (defun bufhist-mode-line-format-entry 65,2171 (defun bufhist-get-buffer-contents 101,3514 (defun bufhist-restore-buffer-contents 113,3998 (defun bufhist-checkpoint 121,4285 (defun bufhist-erase-buffer 129,4654 (defun bufhist-checkpoint-and-erase 139,4999 (defun bufhist-switch-to-index 145,5185 (defun bufhist-first 184,6789 (defun bufhist-last 189,6948 (defun bufhist-prev 194,7094 (defun bufhist-next 202,7317 (defun bufhist-delete 207,7457 (defun bufhist-clear 219,8000 (defun bufhist-init 234,8396 (defun bufhist-exit 259,9333 (defun bufhist-set-readwrite 269,9597 (defun bufhist-before-change-function 284,10217 (defun bufhist-make-buttons 296,10633 (defconst bufhist-minor-mode-map314,11072 (define-minor-mode bufhist-mode326,11534 (defun bufhist-toggle-fn 346,12319 lib/holes.el,2448 (defvar holes-doc 37,1050 (defvar holes-default-hole 145,5033 (defvar holes-active-hole 149,5202 (defcustom holes-empty-hole-string 156,5411 (defcustom holes-empty-hole-regexp 159,5522 (defcustom holes-search-limit 166,5813 (defface active-hole-face178,6189 (defface inactive-hole-face190,6637 (defun holes-region-beginning-or-nil 205,7113 (defun holes-region-end-or-nil 210,7223 (defun holes-copy-active-region 215,7321 (defun holes-is-hole-p 222,7520 (defun holes-hole-start-position 228,7627 (defun holes-hole-end-position 235,7816 (defun holes-hole-buffer 242,8000 (defun holes-hole-at 249,8175 (defun holes-active-hole-exist-p 256,8350 (defun holes-active-hole-start-position 266,8608 (defun holes-active-hole-end-position 276,8980 (defun holes-active-hole-buffer 287,9349 (defun holes-goto-active-hole 298,9655 (defun holes-highlight-hole-as-active 310,9923 (defun holes-highlight-hole 320,10235 (defun holes-disable-active-hole 331,10527 (defun holes-set-active-hole 349,11070 (defun holes-is-in-hole-p 362,11416 (defun holes-make-hole 369,11559 (defun holes-make-hole-at 395,12305 (defun holes-clear-hole 415,12781 (defun holes-clear-hole-at 427,13070 (defun holes-map-holes 436,13329 (defun holes-mapcar-holes 444,13512 (defun holes-clear-all-buffer-holes 450,13684 (defun holes-next 461,13984 (defun holes-next-after-active-hole 468,14235 (defun holes-set-active-hole-next 476,14454 (defun holes-replace-segment 498,15007 (defun holes-replace 508,15361 (defun holes-replace-active-hole 539,16556 (defun holes-replace-update-active-hole 548,16857 (defun holes-delete-update-active-hole 569,17547 (defun holes-set-make-active-hole 576,17761 (defun holes-mouse-replace-active-hole 623,19486 (defun holes-destroy-hole 643,20025 (defun holes-hole-at-event 660,20436 (defun holes-mouse-destroy-hole 665,20549 (defun holes-mouse-forget-hole 675,20789 (defun holes-mouse-set-make-active-hole 691,21099 (defun holes-mouse-set-active-hole 713,21660 (defun holes-set-point-next-hole-destroy 725,21924 (defvar hole-map741,22374 (defvar holes-mode-map757,22994 (defun holes-replace-string-by-holes-backward 794,24469 (defun holes-skeleton-end-hook 812,25170 (defconst holes-jump-doc 821,25608 (defun holes-replace-string-by-holes-backward-jump 828,25815 (defun holes-abbrev-complete 845,26446 (defun holes-insert-and-expand 854,26753 (defvar holes-mode 865,27185 (defun holes-mode 871,27381 lib/local-vars-list.el,373 (defconst local-vars-list-doc 28,829 (defun local-vars-list-insert-empty-zone 44,1393 (defun local-vars-list-find 82,2101 (defun local-vars-list-goto-var 101,2876 (defun local-vars-list-get-current 127,3926 (defun local-vars-list-set-current 148,4776 (defun local-vars-list-get 171,5493 (defun local-vars-list-get-safe 188,6025 (defun local-vars-list-set 193,6219 lib/maths-menu.el,153 (defun maths-menu-build-menu 51,2136 (defvar maths-menu-menu70,2804 (defvar maths-menu-mode-map315,11762 (define-minor-mode maths-menu-mode323,11981 lib/pg-dev.el,75 (defconst pg-dev-lisp-font-lock-keywords36,1102 (defun unload-pg 70,2039 lib/pg-fontsets.el,176 (defcustom pg-fontsets-default-fontset 23,682 (defun pg-fontsets-make-fontsetsizes 28,828 (defconst pg-fontsets-base-fonts 47,1612 (defun pg-fontsets-make-fontsets 52,1717 lib/proof-compat.el,751 (defvar proof-running-on-win32 29,913 (defun pg-custom-undeclare-variable 49,1708 (defun subst-char-in-string 139,4496 (defun replace-regexp-in-string 154,5085 (defconst menuvisiblep 216,7798 (defun set-window-text-height 233,8411 (defmacro save-selected-frame 259,9361 (defun warn 298,10658 (defun redraw-modeline 305,10913 (defun proof-buffer-syntactic-context-emulate 316,11351 (defvar read-shell-command-map349,12658 (defun read-shell-command 367,13346 (defun remassq 379,13827 (defun remassoc 391,14216 (defun frames-of-buffer 404,14661 (defmacro with-selected-window 443,15923 (defun pg-pop-to-buffer 486,17301 (defun process-live-p 537,19163 (defalias 'proof-buffer-syntactic-context proof-buffer-syntactic-context556,19778 lib/span.el,137 (defsubst span-delete-spans 22,479 (defsubst span-property-safe 26,643 (defsubst span-set-start 30,782 (defsubst span-set-end 34,914 lib/span-extent.el,1015 (defsubst span-make 12,367 (defsubst span-detach 16,489 (defsubst span-set-endpoints 20,576 (defsubst span-set-property 24,709 (defsubst span-read-only 28,836 (defsubst span-read-write 32,940 (defun span-give-warning 36,1047 (defun span-write-warning 40,1155 (defsubst span-property 45,1355 (defsubst span-delete 49,1470 (defsubst span-mapcar-spans 55,1641 (defsubst spans-at-region-prop 59,1852 (defsubst span-at 63,2040 (defsubst span-at-before 67,2157 (defsubst span-start 72,2354 (defsubst span-end 76,2483 (defsubst prev-span 80,2606 (defsubst next-span 84,2752 (defsubst span-live-p 88,2894 (defun span-raise 96,3166 (defalias 'span-object span-object100,3265 (defalias 'span-string span-string101,3304 (defsubst make-detached-span 104,3390 (defsubst span-buffer 109,3452 (defsubst span-detached-p 114,3544 (defsubst set-span-face 119,3656 (defsubst fold-spans 123,3751 (defsubst set-span-properties 127,3948 (defsubst set-span-keymap 131,4056 (defsubst span-at-event 136,4200 lib/span-overlay.el,1206 (defalias 'span-start span-start12,370 (defalias 'span-end span-end13,408 (defalias 'span-set-property span-set-property14,442 (defalias 'span-property span-property15,485 (defalias 'span-make span-make16,524 (defalias 'span-detach span-detach17,560 (defalias 'span-set-endpoints span-set-endpoints18,600 (defalias 'span-buffer span-buffer19,645 (defun span-read-only-hook 21,686 (defun span-read-only 25,818 (defun span-read-write 40,1594 (defun span-give-warning 46,1813 (defun span-write-warning 50,1921 (defun span-lt 57,2247 (defun spans-at-point-prop 62,2388 (defun spans-at-region-prop 68,2553 (defun span-at 77,2865 (defsubst span-delete 83,3079 (defsubst span-mapcar-spans 90,3301 (defun span-at-before 94,3510 (defun prev-span 111,4236 (defun next-span 117,4387 (defsubst span-live-p 146,5612 (defun span-raise 152,5778 (defalias 'span-object span-object158,6021 (defun span-string 160,6062 (defun set-span-properties 166,6244 (defun span-find-span 178,6499 (defsubst span-at-event 185,6806 (defun make-detached-span 189,6927 (defun fold-spans 194,7023 (defsubst span-detached-p 209,7557 (defsubst set-span-face 213,7672 (defun set-span-keymap 217,7769 lib/texi-docstring-magic.el,584 (defun texi-docstring-magic-find-face 88,3034 (defun texi-docstring-magic-splice-sep 93,3199 (defconst texi-docstring-magic-munge-table103,3504 (defun texi-docstring-magic-untabify 193,7271 (defun texi-docstring-magic-munge-docstring 203,7586 (defun texi-docstring-magic-texi 242,8873 (defun texi-docstring-magic-format-default 255,9313 (defun texi-docstring-magic-texi-for 271,9948 (defconst texi-docstring-magic-comment329,11908 (defun texi-docstring-magic 335,12062 (defun texi-docstring-magic-face-at-point 369,13142 (defun texi-docstring-magic-insert-magic 384,13665 lib/unicode-chars.el,80 (defvar unicode-chars-alist12,348 (defun unicode-chars-list-chars 5050,245960 lib/unicode-tokens.el,2526 (defvar unicode-tokens-charref-format 60,2307 (defvar unicode-tokens-token-format 63,2404 (defvar unicode-tokens-token-name-alist 66,2495 (defvar unicode-tokens-glyph-list 69,2588 (defvar unicode-tokens-token-prefix 73,2732 (defvar unicode-tokens-token-suffix 76,2816 (defvar unicode-tokens-control-token-match 79,2898 (defvar unicode-tokens-token-match 82,2974 (defvar unicode-tokens-hexcode-match 85,3057 (defvar unicode-tokens-next-character-regexp 88,3165 (defvar unicode-tokens-shortcut-alist91,3310 (defface unicode-tokens-script-font-face107,3762 (defface unicode-tokens-fraktur-font-face117,4027 (defface unicode-tokens-serif-font-face127,4321 (defvar unicode-tokens-max-token-length 142,4648 (defvar unicode-tokens-codept-charname-alist 145,4747 (defvar unicode-tokens-token-alist 148,4855 (defvar unicode-tokens-ustring-alist 152,5016 (defun unicode-tokens-insert-char 160,5119 (defun unicode-tokens-insert-string 170,5540 (defun unicode-tokens-character-insert 180,5917 (defun unicode-tokens-token-insert 202,6825 (defun unicode-tokens-replace-token-after 223,7722 (defun unicode-tokens-looking-backward-at 245,8487 (defun unicode-tokens-electric-suffix 259,9120 (defvar unicode-tokens-rotate-glyph-last-char 306,10724 (defun unicode-tokens-rotate-glyph-forward 308,10776 (defun unicode-tokens-rotate-glyph-backward 337,11958 (defun unicode-tokens-map-ordering 358,12565 (defun unicode-tokens-propertise-after-quail 362,12715 (defun unicode-tokens-quail-define-rules 367,12870 (defvar unicode-tokens-format-entry431,15200 (defconst unicode-tokens-ignored-properties441,15498 (defconst unicode-tokens-annotation-translations449,15752 (defun unicode-tokens-remove-properties 474,16731 (defun unicode-tokens-tokens-to-unicode 482,17049 (defvar unicode-tokens-next-control-token-seen-token 503,17898 (defun unicode-tokens-next-control-token 506,18016 (defconst unicode-tokens-annotation-control-token-alist 560,20100 (defun unicode-tokens-make-token-annotation 575,20644 (defun unicode-tokens-find-property 586,21082 (defun unicode-tokens-annotate-region 600,21471 (defun unicode-tokens-annotate-region-with 612,21879 (defun unicode-tokens-annotate-string 617,22030 (defun unicode-tokens-unicode-to-tokens 623,22198 (defun unicode-tokens-replace-strings-propertise 643,22985 (defun unicode-tokens-replace-strings-unpropertise 673,24235 (defvar unicode-tokens-mode-map 702,24980 (define-minor-mode unicode-tokens-mode705,25077 (defun unicode-tokens-initialise 741,26455 lib/xml-fixed.el,528 (defsubst xml-node-name 82,2904 (defsubst xml-node-attributes 87,3023 (defsubst xml-node-children 92,3141 (defun xml-get-children 97,3277 (defun xml-get-attribute 107,3600 (defun xml-parse-file 123,4064 (defun xml-parse-region 144,4648 (defun xml-parse-tag 179,5693 (defun xml-parse-attlist 284,9162 (defun xml-skip-dtd 321,10552 (defun xml-parse-dtd 338,11188 (defun xml-parse-elem-type 408,13266 (defun xml-substitute-special 449,14421 (defun xml-debug-print 470,15228 (defun xml-debug-print-internal 474,15320 mmm/mmm-auto.el,343 (defvar mmm-autoloaded-classes67,2675 (defun mmm-autoload-class 89,3438 (defvar mmm-changed-buffers-list 129,5005 (defun mmm-major-mode-change 132,5112 (defun mmm-check-changed-buffers 145,5633 (defun mmm-mode-on-maybe 155,6006 (defalias 'mmm-add-find-file-hooks mmm-add-find-file-hooks167,6424 (defun mmm-add-find-file-hook 168,6484 mmm/mmm-class.el,416 (defun mmm-get-class-spec 42,1295 (defun mmm-get-class-parameter 59,2008 (defun mmm-set-class-parameter 63,2174 (defun* mmm-apply-class75,2538 (defun* mmm-apply-classes90,3176 (defun* mmm-apply-all 110,3942 (defun* mmm-ify124,4389 (defun* mmm-match-region206,7472 (defun mmm-match->point 267,10161 (defun mmm-match-and-verify 281,10683 (defun mmm-get-form 307,11741 (defun mmm-default-get-form 318,12237 mmm/mmm-cmds.el,712 (defun mmm-ify-by-class 41,1209 (defun mmm-ify-region 63,1933 (defun mmm-ify-by-regexp75,2361 (defun mmm-parse-buffer 97,3037 (defun mmm-parse-region 106,3373 (defun mmm-parse-block 115,3752 (defun mmm-get-block 132,4503 (defun mmm-reparse-current-region 146,4834 (defun mmm-clear-current-region 167,5508 (defun mmm-clear-regions 172,5672 (defun mmm-clear-all-regions 177,5818 (defun* mmm-end-current-region 185,5978 (defun mmm-narrow-to-submode-region 220,7401 (defun mmm-insert-region 239,8015 (defun mmm-insert-by-key 258,8877 (defun mmm-get-insertion-spec 342,12437 (defun mmm-insertion-help 369,13516 (defun mmm-display-insertion-key 379,13886 (defun mmm-get-all-insertion-keys 401,14708 mmm/mmm-compat.el,418 (defvar mmm-xemacs 40,1312 (defvar mmm-keywords-used49,1615 (defmacro mmm-regexp-opt 91,2661 (defvar mmm-evaporate-property110,3310 (defmacro mmm-set-keymap-default 128,4076 (defmacro mmm-event-key 137,4518 (defvar skeleton-positions 146,4737 (defun mmm-fixup-skeleton 147,4768 (defmacro mmm-make-temp-buffer 159,5205 (defvar mmm-font-lock-available-p 172,5601 (defmacro mmm-set-font-lock-defaults 179,5815 mmm/mmm-cweb.el,228 (defvar mmm-cweb-section-tags38,1116 (defvar mmm-cweb-section-regexp41,1163 (defvar mmm-cweb-c-part-tags44,1253 (defvar mmm-cweb-c-part-regexp47,1312 (defun mmm-cweb-in-limbo 50,1396 (defun mmm-cweb-verify-brief-c 57,1621 mmm/mmm-mason.el,410 (defvar mmm-mason-perl-tags41,1235 (defvar mmm-mason-pseudo-perl-tags45,1376 (defvar mmm-mason-non-perl-tags48,1452 (defvar mmm-mason-perl-tags-regexp51,1553 (defvar mmm-mason-pseudo-perl-tags-regexp56,1748 (defvar mmm-mason-tag-names-regexp61,1965 (defun mmm-mason-verify-inline 66,2185 (defun mmm-mason-start-line 156,5089 (defun mmm-mason-end-line 161,5154 (defun mmm-mason-set-mode-line 168,5248 mmm/mmm-mode.el,1024 (defun mmm-mode 101,3866 (defun mmm-mode-on 140,5371 (defun mmm-mode-off 181,7131 (defvar mmm-mode-map 206,7864 (defvar mmm-mode-prefix-map 209,7939 (defvar mmm-mode-menu-map 212,8049 (defun mmm-define-key 215,8140 (define-key mmm-mode-prefix-map 239,8895 (define-key mmm-mode-prefix-map 246,9153 (define-key mmm-mode-map 249,9264 (define-key mmm-mode-menu-map 252,9366 (define-key mmm-mode-menu-map 254,9438 (define-key mmm-mode-menu-map 256,9497 (define-key mmm-mode-menu-map 258,9578 (define-key mmm-mode-menu-map 260,9659 (define-key mmm-mode-menu-map 262,9746 (define-key mmm-mode-menu-map 265,9840 (define-key mmm-mode-menu-map 267,9900 (define-key mmm-mode-menu-map 270,9991 (define-key mmm-mode-menu-map 272,10051 (define-key mmm-mode-menu-map 274,10158 (define-key mmm-mode-menu-map 276,10243 (define-key mmm-mode-menu-map 279,10329 (define-key mmm-mode-menu-map 281,10389 (define-key mmm-mode-menu-map 283,10502 (define-key mmm-mode-menu-map 285,10587 (define-key mmm-mode-map 288,10670 mmm/mmm-noweb.el,1291 (defvar mmm-noweb-code-mode 44,1352 (defvar mmm-noweb-quote-mode 50,1649 (defvar mmm-noweb-quote-string 54,1806 (defvar mmm-noweb-quote-number 58,1929 (defvar mmm-noweb-narrowing 62,2045 (defun mmm-noweb-chunk 68,2176 (defun mmm-noweb-quote 84,2876 (defun mmm-noweb-quote-name 89,3042 (defun mmm-noweb-chunk-name 95,3302 (defun mmm-noweb-regions 140,4748 (defun mmm-noweb-narrow-to-doc-chunk 166,5616 (defun mmm-noweb-fill-chunk 189,6386 (defun mmm-noweb-fill-paragraph-chunk 208,7070 (defun mmm-noweb-fill-named-chunk 222,7487 (defun mmm-noweb-auto-fill-doc-chunk 238,8064 (defun mmm-noweb-auto-fill-doc-mode 246,8283 (defun mmm-noweb-auto-fill-code-mode 251,8473 (defun mmm-noweb-complete-chunk 259,8685 (defvar mmm-noweb-chunk-history 292,9689 (defun mmm-noweb-goto-chunk 295,9767 (defun mmm-noweb-goto-next 307,10091 (defun mmm-noweb-goto-previous 319,10448 (defvar mmm-noweb-map 336,10852 (defvar mmm-noweb-prefix-map 337,10896 (define-key mmm-noweb-map 338,10947 (define-key mmm-noweb-prefix-map 347,11390 (defun mmm-noweb-bind-keys 352,11656 (defun mmm-syntax-region-list 368,12070 (defun mmm-syntax-other-regions 377,12426 (defun mmm-word-other-regions 389,12897 (defun mmm-space-other-regions 395,13066 (defun mmm-undo-syntax-other-regions 401,13237 mmm/mmm-region.el,1643 (defsubst mmm-overlay-at 54,1748 (defun mmm-overlays-at 59,1933 (defun mmm-included-p 72,2386 (defun mmm-overlays-containing 112,3875 (defun mmm-overlays-contained-in 125,4313 (defun mmm-overlays-overlapping 138,4753 (defun mmm-sort-overlays 149,5116 (defvar mmm-current-overlay 158,5386 (defvar mmm-previous-overlay 163,5601 (defvar mmm-current-submode 168,5789 (defvar mmm-previous-submode 173,5989 (defun mmm-update-current-submode 178,6162 (defun mmm-set-current-submode 199,6978 (defun mmm-submode-at 210,7470 (defun mmm-match-front 219,7745 (defun mmm-match-back 238,8506 (defun mmm-front-start 257,9251 (defun mmm-back-end 265,9555 (defun mmm-valid-submode-region 278,9902 (defun* mmm-make-region305,11058 (defun mmm-make-overlay 431,16429 (defun mmm-get-face 459,17562 (defun mmm-clear-overlays 470,17854 (defun mmm-update-mode-info 486,18321 (defun mmm-update-submode-region 571,22606 (defun mmm-add-hooks 588,23364 (defun mmm-remove-hooks 592,23499 (defun mmm-get-local-variables-list 598,23626 (defun mmm-get-locals 618,24546 (defun mmm-get-saved-local 631,25127 (defun mmm-set-local-variables 635,25292 (defun mmm-get-saved-local-variables 646,25733 (defun mmm-save-changed-local-variables 654,26050 (defun mmm-clear-local-variables 673,26908 (defun mmm-enable-font-lock 684,27187 (defun mmm-update-font-lock-buffer 692,27447 (defun mmm-refontify-maybe 705,27879 (defun mmm-submode-changes-in 720,28401 (defun mmm-regions-in 731,28849 (defun mmm-regions-alist 745,29419 (defun mmm-fontify-region 762,30065 (defun mmm-fontify-region-list 782,31096 (defun mmm-beginning-of-syntax 804,32012 mmm/mmm-rpm.el,154 (defconst mmm-rpm-sh-start-tags48,1617 (defvar mmm-rpm-sh-end-tags53,1841 (defvar mmm-rpm-sh-start-regexp57,2015 (defvar mmm-rpm-sh-end-regexp61,2193 mmm/mmm-sample.el,168 (defvar mmm-here-doc-mode-alist 84,2614 (defun mmm-here-doc-get-mode 93,3099 (defun mmm-file-variables-verify 208,6817 (defun mmm-file-variables-find-back 232,7853 mmm/mmm-univ.el,34 (defun mmm-univ-get-mode 38,1205 mmm/mmm-utils.el,282 (defmacro mmm-valid-buffer 41,1309 (defmacro mmm-save-all 60,1953 (defun mmm-format-string 73,2242 (defun mmm-format-matches 84,2694 (defmacro mmm-save-keyword 107,3487 (defmacro mmm-save-keywords 115,3814 (defun mmm-looking-back-at 128,4347 (defun mmm-make-marker 145,4915 mmm/mmm-vars.el,2667 (defgroup mmm 99,3072 (defvar mmm-c-derived-modes106,3182 (defvar mmm-save-local-variables 110,3301 (defvar mmm-buffer-saved-locals 336,10161 (defvar mmm-region-saved-locals-defaults 341,10361 (defvar mmm-region-saved-locals-for-dominant 347,10621 (defgroup mmm-faces 357,10998 (defcustom mmm-submode-decoration-level 363,11169 (defface mmm-init-submode-face 381,12041 (defface mmm-cleanup-submode-face 385,12181 (defface mmm-declaration-submode-face 389,12318 (defface mmm-comment-submode-face 393,12464 (defface mmm-output-submode-face 397,12617 (defface mmm-special-submode-face 401,12766 (defface mmm-code-submode-face 405,12930 (defface mmm-default-submode-face 409,13069 (defface mmm-delimiter-face 414,13277 (defcustom mmm-mode-string 421,13403 (defcustom mmm-submode-mode-line-format 426,13534 (defvar mmm-primary-mode-display-name 443,14189 (defvar mmm-buffer-mode-display-name 448,14403 (defun mmm-set-mode-line 454,14702 (defvar mmm-classes 478,15510 (defvar mmm-global-classes 484,15755 (defcustom mmm-mode-ext-classes-alist 491,15937 (defun mmm-add-mode-ext-class 510,16755 (defcustom mmm-major-mode-preferences519,17080 (defun mmm-add-to-major-mode-preferences 537,17878 (defun mmm-ensure-modename 553,18664 (defun mmm-modename->function 562,18974 (defcustom mmm-delimiter-mode 576,19437 (defcustom mmm-mode-prefix-key 586,19706 (defcustom mmm-command-modifiers 591,19833 (defcustom mmm-insert-modifiers 605,20466 (defcustom mmm-use-old-command-keys 620,21144 (defun mmm-use-old-command-keys 630,21608 (defcustom mmm-mode-hook 638,21807 (defun mmm-run-constructed-hook 658,22614 (defun mmm-run-major-hook 666,23000 (defun mmm-run-submode-hook 669,23077 (defvar mmm-class-hooks-run 672,23164 (defun mmm-run-class-hook 677,23336 (defvar mmm-primary-mode-entry-hook 682,23508 (defcustom mmm-major-mode-hook 697,24155 (defun mmm-run-major-mode-hook 711,24786 (defcustom mmm-global-mode 724,25327 (defcustom mmm-never-modes740,26022 (defvar mmm-set-file-name-for-modes 758,26322 (defvar mmm-mode 769,26681 (defvar mmm-primary-mode 777,26889 (defvar mmm-classes-alist 788,27255 (defun mmm-add-classes 943,35462 (defun mmm-add-group 948,35627 (defun mmm-add-to-group 958,36077 (defconst mmm-version 972,36574 (defun mmm-version 975,36639 (defvar mmm-temp-buffer-name 982,36782 (defvar mmm-interactive-history 988,36912 (defun mmm-add-to-history 994,37181 (defun mmm-clear-history 997,37264 (defvar mmm-mode-ext-classes 1005,37449 (defun mmm-get-mode-ext-classes 1010,37660 (defun mmm-clear-mode-ext-classes 1019,38036 (defun mmm-mode-ext-applies 1023,38161 (defun mmm-get-all-classes 1037,38645 x-symbol/lisp/auto-autoloads.el,63 (defalias 'x-symbol-map-autoload x-symbol-map-autoload23,974 x-symbol/lisp/x-symbol-autoloads.el,63 (defalias 'x-symbol-map-autoload x-symbol-map-autoload23,974 x-symbol/lisp/x-symbol-bib.el,549 (defcustom x-symbol-bib-auto-style 42,1544 (defcustom x-symbol-bib-modeline-name 49,1800 (defcustom x-symbol-bib-header-groups-alist 55,1979 (defcustom x-symbol-bib-electric-ignore 62,2268 (defcustom x-symbol-bib-class-alist 69,2558 (defcustom x-symbol-bib-class-face-alist 76,2824 (defvar x-symbol-bib-token-grammar89,3308 (defvar x-symbol-bib-required-fonts 99,3784 (defvar x-symbol-bib-user-table 103,3960 (defvar x-symbol-bib-table106,4064 (defvar x-symbol-bib-generated-data 113,4390 (defun x-symbol-bib-default-token-list 117,4529 x-symbol/lisp/x-symbol.el,9210 (defvar x-symbol-trace-invisible 52,2014 (defconst x-symbol-language-access-alist67,2529 (defstruct (x-symbol-generated179,8410 (defstruct (x-symbol-grammar190,8622 (defvar x-symbol-map 213,9450 (defvar x-symbol-unalias-alist 217,9577 (defvar x-symbol-latin-decode-alists 221,9694 (defvar x-symbol-context-atree 225,9879 (defvar x-symbol-electric-atree 229,9994 (defvar x-symbol-grid-alist 232,10088 (defvar x-symbol-menu-alist 235,10171 (defvar x-symbol-all-charsyms 238,10278 (defvar x-symbol-fancy-value-cache 243,10486 (defvar x-symbol-fchar-tables 247,10649 (defvar x-symbol-bchar-tables 250,10778 (defvar x-symbol-cstring-table 252,10814 (defvar x-symbol-fontified-cstring-table 254,10851 (defvar x-symbol-charsym-decode-obarray 256,10898 (defun x-symbol-set-variable 263,11127 (defun x-symbol-ensure-hashtable 277,11762 (defun x-symbol-puthash 284,12064 (defun x-symbol-call-function-or-regexp 292,12393 (defun x-symbol-match-in-alist 301,12793 (defun x-symbol-fancy-string 330,14017 (defun x-symbol-fancy-value 352,14934 (defun x-symbol-fancy-associations 371,15701 (defun x-symbol-language-value 400,16853 (defun x-symbol-charsym-face 414,17511 (defun x-symbol-image-available-p 427,18138 (defun x-symbol-default-context-info-ignore 432,18350 (defun x-symbol-default-info-keys-keymaps 446,19117 (defun x-symbol-alias-charsym 458,19592 (defun x-symbol-default-valid-charsym 467,19961 (defun x-symbol-next-valid-charsym 489,20998 (defun x-symbol-valid-context-charsym 516,22005 (defun x-symbol-next-valid-charsym-before 527,22604 (defun x-symbol-prefix-arg-texts 551,23661 (defun x-symbol-region-text 560,23956 (defun x-symbol-language-text 569,24252 (defun x-symbol-coding-text 577,24652 (defun x-symbol-language-modeline-text 595,25347 (defun x-symbol-coding-modeline-text 601,25583 (defun x-symbol-translate-to-ascii 647,27488 (defun x-symbol-package-web 681,28753 (defun x-symbol-package-info 688,28974 (defun x-symbol-package-bug 694,29135 (defun x-symbol-package-reply-to-report 745,31108 (defvar x-symbol-encode-rchars 765,31836 (defun x-symbol-even-escapes-before-p 773,32118 (defun x-symbol-decode-region 781,32297 (defun x-symbol-decode-all 794,32770 (defun x-symbol-decode-single-token 857,35838 (defun x-symbol-decode-lisp 866,36145 (defun x-symbol-encode-string 898,37612 (defun x-symbol-encode-all 909,37931 (defun x-symbol-encode-lisp 973,40966 (defun x-symbol-decode-recode 1009,42371 (defun x-symbol-decode 1039,43747 (defun x-symbol-encode-recode 1052,44338 (defun x-symbol-encode 1080,45614 (defun x-symbol-unalias 1096,46373 (defun x-symbol-copy-region-encoded 1161,49292 (defun x-symbol-yank-decoded 1189,50542 (defun x-symbol-update-modeline 1216,51642 (defun x-symbol-auto-coding-alist 1240,52497 (defun x-symbol-auto-8bit-search 1276,53658 (defvar x-symbol-font-family-postfixes1301,54448 (defvar x-symbol-font-lock-property-alist1304,54564 (defvar x-symbol-font-lock-keywords1308,54745 (defvar x-symbol-subscript-matcher 1335,55740 (defvar x-symbol-subscript-type 1339,55843 (defun x-symbol-subscripts-available-p 1342,55894 (defun x-symbol-font-lock-start 1348,56135 (defun x-symbol-match-subscript 1357,56521 (defun x-symbol-init-font-lock 1363,56734 (defun x-symbol-set-image 1395,58322 (defun x-symbol-mode-internal 1413,59068 (defun nuke-x-symbol 1487,62177 (defun x-symbol-options-filter 1500,62630 (defun x-symbol-extra-filter 1536,63786 (defun x-symbol-menu-filter 1544,64034 (defvar x-symbol-list-mode-map1574,65013 (defvar x-symbol-list-buffer 1600,66163 (defvar x-symbol-list-win-config 1602,66239 (defvar x-symbol-invisible-spec 1604,66350 (defvar x-symbol-itimer 1608,66500 (defvar x-symbol-invisible-display-table1611,66583 (defvar x-symbol-invisible-font 1620,66819 (defvar x-symbol-charsym-info-cache 1645,68006 (defvar x-symbol-language-info-caches 1647,68097 (defvar x-symbol-coding-info-cache 1649,68191 (defvar x-symbol-keys-info-cache 1651,68280 (defun x-symbol-list-bury 1659,68585 (defun x-symbol-list-restore 1665,68781 (defun x-symbol-list-store 1695,69999 (defun x-symbol-list-mode 1704,70416 (defun x-symbol-list-scroll 1725,71218 (defun x-symbol-init-language-interactive 1748,71860 (defun x-symbol-list-menu 1765,72574 (defun x-symbol-list-selected 1820,74482 (defun x-symbol-list-menu-selected 1846,75691 (defun x-symbol-list-mouse-selected 1857,76144 (defun x-symbol-charsym-info 1874,76866 (defun x-symbol-language-info 1888,77467 (defun x-symbol-coding-info 1920,78667 (defun x-symbol-keys-info 1940,79439 (defun x-symbol-info 1964,80362 (defun x-symbol-list-info 1977,80900 (defun x-symbol-highlight-echo 1991,81443 (defun x-symbol-point-info 2002,81992 (defun x-symbol-hide-revealed-at-point 2048,83914 (defun x-symbol-reveal-invisible 2085,85581 (defun x-symbol-show-info-and-invisible 2133,87773 (defun x-symbol-start-itimer-once 2169,89315 (defun x-symbol-setup-minibuffer 2185,89941 (defvar x-symbol-language-history 2203,90512 (defvar x-symbol-token-history 2206,90636 (defvar x-symbol-last-abbrev 2209,90712 (defvar x-symbol-electric-pos 2211,90808 (defvar x-symbol-command-keys 2214,90890 (defvar x-symbol-help-keys 2218,91021 (defvar x-symbol-help-language 2220,91116 (defvar x-symbol-help-completions 2222,91215 (defvar x-symbol-help-completions1 2224,91307 (defun x-symbol-map-default-binding 2232,91583 (defun x-symbol-read-charsym-token 2263,92661 (defun x-symbol-insert-command 2289,93584 (defun x-symbol-read-language 2340,95591 (defun x-symbol-read-token 2355,96269 (defun x-symbol-read-token-direct 2394,97778 (defun x-symbol-grid 2406,98178 (defun x-symbol-replace-from 2494,101794 (defvar x-symbol-token-search-prelude-size 2530,103295 (defun x-symbol-replace-token 2532,103343 (defun x-symbol-match-token-before 2557,104434 (defun x-symbol-token-input 2601,106237 (defun x-symbol-modify-key 2622,107067 (defun x-symbol-rotate-key 2655,108396 (defun x-symbol-electric-input 2709,110606 (defun x-symbol-help-mapper 2751,112307 (defun x-symbol-help-output 2774,113146 (defun x-symbol-help 2817,114742 (defvar x-symbol-face-docstrings2870,116811 (defvar x-symbol-all-key-prefixes 2876,116999 (defvar x-symbol-all-key-chain-alist 2878,117110 (defvar x-symbol-all-horizontal-chain-alist 2880,117209 (defvar x-symbol-all-chain-subchains-alist 2882,117322 (defvar x-symbol-all-exclusive-context-alist 2884,117436 (defalias 'x-symbol-table-grouping x-symbol-table-grouping2892,117732 (defalias 'x-symbol-table-aspects x-symbol-table-aspects2893,117773 (defalias 'x-symbol-table-score x-symbol-table-score2894,117814 (defalias 'x-symbol-table-input x-symbol-table-input2895,117854 (defsubst x-symbol-table-prefixes 2896,117895 (defsubst x-symbol-table-junk 2897,117946 (defsubst x-symbol-charsym-defined-p 2899,117997 (defun x-symbol-try-font-name-0 2907,118298 (defun x-symbol-try-font-name 2925,118854 (defun x-symbol-set-cstrings 2942,119370 (defun x-symbol-init-charsym-command 2987,121348 (defun x-symbol-init-charsym-input 2995,121714 (defun x-symbol-init-charsym-aspects 3064,124432 (defun x-symbol-init-cset 3094,125712 (defun x-symbol-make-atree 3244,132535 (defun x-symbol-atree-push 3248,132615 (defun x-symbol-component-root-p 3268,133304 (defun x-symbol-component-elements 3272,133443 (defun x-symbol-component-merge 3279,133691 (defun x-symbol-component-space 3293,134239 (defun x-symbol-modify-less-than 3307,134823 (defun x-symbol-inherit-aspects 3312,135046 (defun x-symbol-compute-aspects 3321,135485 (defun x-symbol-init-aspects 3337,136203 (defun x-symbol-sort-modify-chain 3382,138252 (defun x-symbol-init-horizontal/key-alist 3397,138824 (defun x-symbol-init-exclusive-alist 3413,139570 (defun x-symbol-init-horizontal-chain 3451,141174 (defun x-symbol-init-exclusive-chain 3459,141506 (defun x-symbol-init-rotate-chain 3466,141833 (defun x-symbol-init-context-atree 3487,142707 (defun x-symbol-init-key-bindings 3532,144990 (defun x-symbol-rotate-modify-less-than 3555,145913 (defun x-symbol-subgroup-less-than 3563,146308 (defun x-symbol-header-charsyms 3568,146565 (defun x-symbol-init-grid/menu 3594,147615 (defun x-symbol-init-input 3666,150271 (defun x-symbol-init-latin-decoding 3796,156747 (defun x-symbol-get-prime-for 3837,158618 (defun x-symbol-alist-to-obarray 3846,158942 (defun x-symbol-alist-to-hash-table 3852,159150 (defun x-symbol-init-language 3862,159483 (defvar x-symbol-latin1-cset3986,164948 (defvar x-symbol-latin2-cset3992,165121 (defvar x-symbol-latin3-cset3998,165294 (defvar x-symbol-latin5-cset4004,165467 (defvar x-symbol-latin9-cset4010,165639 (defvar x-symbol-xsymb0-cset4016,165845 (defvar x-symbol-xsymb1-cset4022,166100 (defvar x-symbol-latin1-table4028,166342 (defvar x-symbol-latin2-table4129,170812 (defvar x-symbol-latin3-table4228,174013 (defvar x-symbol-latin5-table4334,177131 (defvar x-symbol-latin9-table4433,179441 (defvar x-symbol-xsymb0-table4532,181831 (defvar x-symbol-xsymb1-table4682,189227 (defvar x-symbol-no-of-charsyms 4890,199862 (defun x-symbol-mac-setup1 4898,200228 (defun x-symbol-mac-setup2 4919,201006 (defun x-symbol-startup 4945,201872 x-symbol/lisp/x-symbol-emacs.el,1126 (defun emacs-version>=33,1289 (defvar x-symbol-emacs-has-font-lock-with-props67,2953 (defvar x-symbol-emacs-has-correct-find-safe-coding87,3682 (defvar x-symbol-emacs-after-create-image-function102,4196 (defvar image-types 128,5053 (defvar init-file-loaded 164,6440 (defvar message-stack 167,6513 (defun region-active-p 250,9823 (defvar x-symbol-data-directory 293,11359 (defun x-symbol-directory-files 363,13636 (defun x-symbol-event-in-current-buffer 377,14024 (defun x-symbol-create-image 380,14073 (defun x-symbol-make-glyph 383,14158 (defun x-symbol-set-glyph-image 386,14229 (defvar x-symbol-heading-strut-glyph 401,14726 (defvar x-symbol-invisible-face 404,14813 (defvar x-symbol-face 405,14871 (defvar x-symbol-sub-face 406,14909 (defvar x-symbol-sup-face 407,14955 (defvar x-symbol-emacs-w32-font-directories409,15002 (defvar x-symbol-invisible-display-table 422,15480 (defalias 'x-symbol-window-width x-symbol-window-width424,15527 (defun x-symbol-set-face-font 429,15651 (defun x-symbol-event-matches-key-specifier-p 453,16654 (defun start-itimer 463,16926 (defun itimer-live-p 465,17023 x-symbol/lisp/x-symbol-hooks.el,3109 (defvar x-symbol-warn-of-old-emacs 66,2522 (defvar x-symbol-data-directory81,3030 (defvar x-symbol-font-directory87,3246 (defun x-symbol-define-user-options 98,3661 (defun x-symbol-auto-mode-suffixes 126,5060 (defcustom x-symbol-initialize 143,5652 (defvar x-symbol-orig-comint-input-sender 177,7219 (defun x-symbol-coding-system-from-locale 185,7531 (defun x-symbol-buffer-coding 223,9137 (defvar x-symbol-default-coding279,11196 (defcustom x-symbol-compose-key 325,13040 (defcustom x-symbol-auto-key-autoload 332,13308 (defvar x-symbol-auto-conversion-method 340,13623 (defvar x-symbol-language-alist 361,14586 (defcustom x-symbol-charsym-name 370,14923 (defcustom x-symbol-tex-name 378,15273 (defcustom x-symbol-tex-modes384,15440 (defcustom x-symbol-sgml-name 392,15708 (defcustom x-symbol-sgml-modes398,15880 (defcustom x-symbol-bib-name 407,16207 (defcustom x-symbol-bib-modes 413,16377 (defcustom x-symbol-texi-name 420,16603 (defcustom x-symbol-texi-modes 426,16779 (defvar x-symbol-mode 438,17188 (defvar x-symbol-language 445,17415 (defvar x-symbol-coding 460,18103 (defvar x-symbol-8bits 487,19379 (defvar x-symbol-unique 502,19965 (defvar x-symbol-subscripts 517,20547 (defvar x-symbol-image 530,21112 (defcustom x-symbol-auto-mode-suffixes 547,21754 (defcustom x-symbol-auto-8bit-search-limit 556,22179 (defcustom x-symbol-auto-style-alist 563,22461 (defvar x-symbol-mode-disable-alist 609,24419 (defun x-symbol-image-set-colormap 617,24694 (defcustom x-symbol-image-colormap-allocation 635,25402 (defcustom x-symbol-image-convert-colormap646,25858 (defalias 'x-symbol-cset-registry x-symbol-cset-registry665,26545 (defalias 'x-symbol-cset-coding x-symbol-cset-coding666,26587 (defalias 'x-symbol-cset-leading x-symbol-cset-leading667,26627 (defalias 'x-symbol-cset-score x-symbol-cset-score668,26668 (defalias 'x-symbol-cset-left x-symbol-cset-left669,26708 (defalias 'x-symbol-cset-right x-symbol-cset-right670,26745 (defvar x-symbol-input-initialized 672,26784 (defun x-symbol-key-autoload 681,27080 (defalias 'x-symbol-map-autoload x-symbol-map-autoload703,28055 (defun x-symbol-buffer-file-name 710,28304 (defun x-symbol-auto-set-variable 723,28776 (defun x-symbol-mode 729,28994 (defun turn-on-x-symbol-conditionally 860,34373 (defun x-symbol-fontify 868,34663 (defun x-symbol-comint-output-filter 896,35787 (defun x-symbol-comint-send 905,36149 (defun x-symbol-format-decode 921,36806 (defun x-symbol-format-encode 943,37724 (defun x-symbol-after-insert-file 958,38250 (defun x-symbol-write-region-annotate-function 995,40092 (defun x-symbol-write-file-hook 1015,41096 (defvar x-symbol-modeline-string 1076,43560 (defvar x-symbol-mode-map1081,43775 (defconst x-symbol-early-language-access-alist1090,44065 (defun x-symbol-init-language-accesses 1095,44274 (defun x-symbol-register-language 1126,45445 (defun x-symbol-initialize 1146,46317 (defun x-symbol-after-init 1248,51435 (defun x-symbol-inherit-from-buffer 1306,54270 (defun x-symbol-auctex-math-insert 1339,55750 (defun x-symbol-turn-on-bib-cite 1348,56068 x-symbol/lisp/x-symbol-image.el,1980 (defvar x-symbol-image-process-buffer 48,1782 (defvar x-symbol-image-process-name 51,1893 (defvar x-symbol-image-highlight-map54,1992 (defun x-symbol-image-try-special 73,2736 (defvar x-symbol-image-broken-image82,3092 (defvar x-symbol-image-create-image87,3298 (defvar x-symbol-image-design-glyph92,3528 (defvar x-symbol-image-locked-glyph98,3773 (defvar x-symbol-image-remote-glyph104,4005 (defvar x-symbol-image-junk-glyph110,4240 (defvar x-symbol-image-buffer-extents 116,4471 (defvar x-symbol-image-memory-cache 121,4705 (defvar x-symbol-image-all-recursive-dirs 131,5181 (defvar x-symbol-image-all-dirs 133,5289 (defun x-symbol-image-parse-buffer 142,5583 (defun x-symbol-image-after-change-function 184,7740 (defun x-symbol-image-delete-extents 201,8322 (defun x-symbol-image-parse-region 230,9501 (defun x-symbol-image-default-file-name 313,12935 (defun x-symbol-image-init-memory-cache 329,13656 (defun x-symbol-image-init-memory-cache-1 359,14931 (defun x-symbol-image-searchpath 371,15428 (defun x-symbol-image-searchpath-1 399,16532 (defun x-symbol-image-mouse-editor 425,17580 (defun x-symbol-image-editor 433,17814 (defun x-symbol-image-highlight-menu 462,18897 (defun x-symbol-image-help-echo 471,19252 (defun x-symbol-image-file-name 486,19870 (defun x-symbol-image-event-file 502,20552 (defun x-symbol-image-active-file 513,20947 (defvar x-symbol-image-process-stack 569,22856 (defvar x-symbol-image-process-elem 573,23024 (defun x-symbol-image-create-glyph 587,23677 (defun x-symbol-image-cache-name 645,25868 (defun x-symbol-image-process-stack 670,26998 (defun x-symbol-image-convert-file 683,27562 (defun x-symbol-image-start-convert-mono 691,27895 (defun x-symbol-image-start-convert-color 702,28375 (defun x-symbol-image-start-convert-truecolor 713,28866 (defun x-symbol-image-start-convert-mswindows 723,29317 (defun x-symbol-image-start-convert-colormap 738,29917 (defun x-symbol-image-process-sentinel 755,30778 x-symbol/lisp/x-symbol-macs.el,569 (defmacro x-symbol-ignore-property-changes 43,1617 (defun x-symbol-set/push-assq/assoc 62,2278 (defmacro x-symbol-set-assq 76,2819 (defmacro x-symbol-set-assoc 82,3057 (defmacro x-symbol-push-assq 88,3300 (defmacro x-symbol-push-assoc 95,3618 (defmacro x-symbol-dolist-delaying 107,4113 (defmacro x-symbol-do-plist 148,5816 (defmacro x-symbol-while-charsym 168,6560 (defmacro x-symbol-encode-for-charsym 190,7309 (defmacro x-symbol-decode-for-charsym 220,8473 (defmacro x-symbol-decode-unique-test 245,9292 (defmacro x-symbol-set-buffer-multibyte 251,9467 x-symbol/lisp/x-symbol-mule.el,1507 (defvar x-symbol-mule-default-charset48,2000 (defalias 'x-symbol-make-cset x-symbol-make-cset71,2912 (defalias 'x-symbol-make-char x-symbol-make-char72,2968 (defalias 'x-symbol-init-charsym-syntax x-symbol-init-charsym-syntax73,3024 (defalias 'x-symbol-charsym-after x-symbol-charsym-after74,3100 (defalias 'x-symbol-string-to-charsyms x-symbol-string-to-charsyms75,3164 (defalias 'x-symbol-match-before x-symbol-match-before76,3238 (defalias 'x-symbol-encode-lisp x-symbol-encode-lisp77,3300 (defalias 'x-symbol-pre-command-hook x-symbol-pre-command-hook78,3360 (defalias 'x-symbol-post-command-hook x-symbol-post-command-hook79,3430 (defalias 'x-symbol-encode-charsym-after x-symbol-encode-charsym-after80,3502 (defalias 'x-symbol-init-quail-bindings x-symbol-init-quail-bindings81,3580 (defvar x-symbol-mule-char-table 83,3657 (defvar x-symbol-mule-pre-command 85,3738 (defun x-symbol-mule-make-charset 93,4009 (defvar x-symbol-mule-default-font 107,4558 (defun x-symbol-mule-default-font 109,4599 (defun x-symbol-mule-make-cset 128,5509 (defun x-symbol-mule-make-char 190,7903 (defun x-symbol-mule-init-charsym-syntax 220,9039 (defun x-symbol-mule-init-quail-bindings 236,9669 (defun x-symbol-mule-encode-charsym-after 255,10393 (defun x-symbol-mule-charsym-after 259,10498 (defun x-symbol-mule-string-to-charsyms 268,10909 (defun x-symbol-mule-match-before 281,11395 (defun x-symbol-mule-pre-command-hook 305,12385 (defun x-symbol-mule-post-command-hook 314,12788 x-symbol/lisp/x-symbol-nomule.el,1954 (defalias 'x-symbol-make-cset x-symbol-make-cset46,1779 (defalias 'x-symbol-make-char x-symbol-make-char47,1837 (defalias 'x-symbol-init-charsym-syntax x-symbol-init-charsym-syntax48,1895 (defalias 'x-symbol-charsym-after x-symbol-charsym-after49,1944 (defalias 'x-symbol-string-to-charsyms x-symbol-string-to-charsyms50,2010 (defalias 'x-symbol-match-before x-symbol-match-before51,2086 (defalias 'x-symbol-encode-lisp x-symbol-encode-lisp52,2150 (defalias 'x-symbol-pre-command-hook x-symbol-pre-command-hook53,2212 (defalias 'x-symbol-post-command-hook x-symbol-post-command-hook54,2284 (defalias 'x-symbol-encode-charsym-after x-symbol-encode-charsym-after55,2358 (defalias 'x-symbol-init-quail-bindings x-symbol-init-quail-bindings56,2438 (defvar x-symbol-nomule-mouse-yank-function 58,2488 (defvar x-symbol-nomule-mouse-track-function61,2629 (defvar x-symbol-nomule-cstring-regexp 66,2867 (defvar x-symbol-nomule-char-table 71,3128 (defvar x-symbol-nomule-pre-command 73,3211 (defvar x-symbol-nomule-leading-faces-alist 76,3309 (defvar x-symbol-nomule-font-lock-face 79,3482 (defvar x-symbol-nomule-display-table82,3583 (defvar x-symbol-nomule-character-quote-syntax 93,3945 (defun x-symbol-nomule-init-faces 101,4248 (defun x-symbol-nomule-make-cset 124,5108 (defun x-symbol-nomule-make-char 150,6186 (defun x-symbol-nomule-multibyte-char-p 180,7511 (defun x-symbol-nomule-encode-charsym-after 185,7749 (defun x-symbol-nomule-charsym-after 197,8147 (defun x-symbol-nomule-string-to-charsyms 220,9090 (defun x-symbol-nomule-match-before 236,9730 (defun x-symbol-nomule-goto-leading-char 269,11142 (defun x-symbol-nomule-mouse-yank-function 275,11371 (defun x-symbol-nomule-mouse-track-function 282,11690 (defun x-symbol-nomule-pre-command-hook 299,12476 (defun x-symbol-nomule-post-command-hook 313,13109 (defun x-symbol-nomule-match-cstring 351,14756 (defun x-symbol-nomule-fontify-cstrings 369,15504 x-symbol/lisp/x-symbol-sgml.el,1521 (defcustom x-symbol-sgml-auto-style41,1525 (defcustom x-symbol-sgml-auto-coding-alist52,1947 (defface x-symbol-sgml-symbol-face71,2757 (defface x-symbol-sgml-noname-face79,3038 (defcustom x-symbol-sgml-modeline-name 87,3301 (defcustom x-symbol-sgml-header-groups-alist93,3484 (defcustom x-symbol-sgml-class-alist113,4257 (defcustom x-symbol-sgml-class-face-alist124,4674 (defcustom x-symbol-sgml-electric-ignore 134,5097 (defvar x-symbol-sgml-token-list 141,5365 (defvar x-symbol-sgml-token-grammar156,6077 (defvar x-symbol-sgml-user-table 163,6317 (defvar x-symbol-sgml-generated-data 166,6426 (defcustom x-symbol-sgml-master-directory 175,6746 (defcustom x-symbol-sgml-image-searchpath 182,6973 (defcustom x-symbol-sgml-image-cached-dirs 189,7223 (defcustom x-symbol-sgml-image-file-truename-alist196,7489 (defcustom x-symbol-sgml-image-keywords226,8698 (defun x-symbol-sgml-image-file-truename 236,9078 (defcustom x-symbol-sgml-subscript-matcher 250,9639 (defcustom x-symbol-sgml-font-lock-regexp 256,9875 (defcustom x-symbol-sgml-font-lock-limit-regexp 262,10079 (defcustom x-symbol-sgml-font-lock-contents-regexp 269,10350 (defcustom x-symbol-sgml-font-lock-alist276,10605 (defun x-symbol-sgml-default-token-list 292,11264 (defvar x-symbol-sgml-latin1-table310,12052 (defvar x-symbol-sgml-latinN-table409,15286 (defvar x-symbol-sgml-xsymb0-table495,17715 (defvar x-symbol-sgml-xsymb1-table601,21570 (defvar x-symbol-sgml-table640,23549 (defun x-symbol-sgml-subscript-matcher 657,24155 x-symbol/lisp/x-symbol-tex.el,2359 (defcustom x-symbol-tex-auto-style55,1896 (defcustom x-symbol-tex-auto-coding-alist70,2510 (defcustom x-symbol-tex-coding-master 87,3158 (defcustom x-symbol-tex-modeline-name 99,3626 (defcustom x-symbol-tex-header-groups-alist 105,3805 (defcustom x-symbol-tex-electric-ignore 112,4065 (defcustom x-symbol-tex-electric-ignore-regexp 119,4364 (defcustom x-symbol-tex-token-suppress-space 126,4653 (defvar x-symbol-tex-extra-menu-items135,5045 (defvar x-symbol-tex-token-grammar145,5474 (defvar x-symbol-tex-verb-delimiter-regexp 160,6263 (defvar x-symbol-tex-env-verbatim-regexp 164,6456 (defvar x-symbol-tex-env-tabbing-regexp 168,6637 (defvar x-symbol-tex-user-table 172,6812 (defvar x-symbol-tex-generated-data 175,6916 (defcustom x-symbol-tex-master-directory 184,7234 (defcustom x-symbol-tex-image-searchpath191,7518 (defcustom x-symbol-tex-image-cached-dirs 209,8205 (defcustom x-symbol-tex-image-keywords216,8458 (defcustom x-symbol-tex-subscript-matcher 234,9311 (defcustom x-symbol-tex-invisible-braces 240,9543 (defcustom x-symbol-tex-font-lock-allowed-faces245,9639 (defvar x-symbol-tex-font-lock-regexp256,10183 (defvar x-symbol-tex-font-lock-limit-regexp 261,10425 (defface x-symbol-tex-math-face270,10764 (defface x-symbol-tex-text-face278,11034 (defcustom x-symbol-tex-class-alist286,11306 (defcustom x-symbol-tex-class-face-alist320,12867 (defun x-symbol-tex-auto-coding-alist 336,13456 (defun x-symbol-tex-default-master-directory 360,14702 (defun x-symbol-tex-default-electric-ignore 368,15088 (defun x-symbol-tex-default-token-list 390,16097 (defun x-symbol-tex-after-init-language 400,16459 (defvar x-symbol-tex-required-fonts 419,17293 (defvar x-symbol-tex-latin1-table423,17445 (defvar x-symbol-tex-latinN-table522,21630 (defvar x-symbol-tex-xsymb0-table611,25318 (defvar x-symbol-tex-xsymb1-table726,29931 (defvar x-symbol-tex-table886,37347 (defun x-symbol-tex-subscript-matcher 903,37904 (defun x-symbol-tex-encode 951,39573 (defun x-symbol-tex-decode 972,40387 (defun x-symbol-tex-token-input 1047,43403 (defun x-symbol-tex-translate-locations 1063,43971 (defun x-symbol-tex-error-location 1119,45896 (defun x-symbol-tex-preview-locations 1149,46926 (defun x-symbol-tex-xdecode-old 1203,48666 (defvar x-symbol-tex-xdecode-obarray 1245,50315 (defun x-symbol-tex-xdecode-latex 1247,50358 x-symbol/lisp/x-symbol-texi.el,597 (defcustom x-symbol-texi-auto-style 41,1573 (defcustom x-symbol-texi-modeline-name 48,1832 (defcustom x-symbol-texi-header-groups-alist54,2015 (defcustom x-symbol-texi-electric-ignore 69,2682 (defcustom x-symbol-texi-class-alist76,2950 (defcustom x-symbol-texi-class-face-alist 89,3508 (defvar x-symbol-texi-token-grammar98,3801 (defvar x-symbol-texi-user-table 107,4094 (defvar x-symbol-texi-generated-data 110,4206 (defvar x-symbol-texi-latin1-table119,4523 (defvar x-symbol-texi-latinN-table218,7766 (defvar x-symbol-texi-xsymbX-table303,10629 (defvar x-symbol-texi-table327,11362 x-symbol/lisp/x-symbol-unichars.el,99 (defvar x-symbol-unicode-character-list5,115 (defun x-symbol-list-unicode-characters 5044,235676 x-symbol/lisp/x-symbol-unicode.el,169 (defconst x-symbol-xsym-unicode-map 19,604 (defconst x-symbol-old-tables267,10039 (defconst x-symbol-unicode-table283,10470 (defconst x-symbol-unicode-cset299,10973 x-symbol/lisp/x-symbol-unicode-extras.el,40 (defconst x-symol-unicode-extras13,263 x-symbol/lisp/x-symbol-vars.el,8115 (defconst x-symbol-version 40,1516 (defgroup x-symbol 49,1858 (defgroup x-symbol-mode 56,2069 (defgroup x-symbol-input-init 61,2198 (defgroup x-symbol-input-control 66,2334 (defgroup x-symbol-info-general 71,2466 (defgroup x-symbol-info-strings 76,2602 (defgroup x-symbol-miscellaneous 81,2738 (defgroup x-symbol-image-general 86,2864 (defgroup x-symbol-image-language 91,3029 (defgroup x-symbol-tex 101,3458 (defgroup x-symbol-sgml 107,3589 (defgroup x-symbol-bib 113,3725 (defgroup x-symbol-texi 119,3859 (define-widget 'x-symbol-key x-symbol-key132,4246 (define-widget 'x-symbol-auto-style x-symbol-auto-style136,4336 (define-widget 'x-symbol-command x-symbol-command156,5203 (define-widget 'x-symbol-charsym x-symbol-charsym161,5311 (define-widget 'x-symbol-group x-symbol-group165,5402 (define-widget 'x-symbol-coding x-symbol-coding169,5494 (define-widget 'x-symbol-function-or-regexp x-symbol-function-or-regexp178,5712 (define-widget 'x-symbol-fancy-spec x-symbol-fancy-spec182,5881 (define-widget 'x-symbol-fancy x-symbol-fancy191,6229 (define-widget 'x-symbol-auto-coding x-symbol-auto-coding200,6582 (define-widget 'x-symbol-headers x-symbol-headers211,6889 (define-widget 'x-symbol-class-info x-symbol-class-info217,7045 (define-widget 'x-symbol-class-faces x-symbol-class-faces224,7288 (define-widget 'x-symbol-image-keywords x-symbol-image-keywords232,7568 (defconst x-symbol-cache-variables 249,8155 (defun x-symbol-set-cache-variable 258,8514 (defconst x-symbol-LANG-name 270,8931 (defconst x-symbol-LANG-modes 276,9186 (defconst x-symbol-LANG-auto-style 282,9519 (defcustom x-symbol-LANG-modeline-name 336,11613 (defconst x-symbol-LANG-required-fonts 343,11898 (defconst x-symbol-LANG-token-grammar348,12134 (defconst x-symbol-LANG-generated-data 416,15400 (defconst x-symbol-LANG-table 422,15652 (defconst x-symbol-LANG-header-groups-alist 435,16207 (defconst x-symbol-LANG-class-alist441,16510 (defconst x-symbol-LANG-class-face-alist 455,17122 (defconst x-symbol-LANG-electric-ignore 466,17574 (defconst x-symbol-LANG-extra-menu-items 477,18088 (defconst x-symbol-LANG-subscript-matcher 485,18533 (defconst x-symbol-LANG-image-keywords 494,19001 (defconst x-symbol-LANG-master-directory 509,19696 (defconst x-symbol-LANG-image-searchpath 515,19987 (defconst x-symbol-LANG-image-cached-dirs 523,20414 (defvar x-symbol-package-url 534,20885 (defconst x-symbol-maintainer-address 539,21129 (defvar x-symbol-installer-address 542,21268 (defcustom x-symbol-token-input 552,21708 (defcustom x-symbol-electric-input 567,22362 (defcustom x-symbol-local-menu 598,24006 (defcustom x-symbol-local-grid 608,24350 (defcustom x-symbol-temp-grid 620,24893 (defcustom x-symbol-temp-help 630,25272 (defvar x-symbol-use-refbuffer-once 640,25670 (defcustom x-symbol-reveal-invisible 657,26459 (defcustom x-symbol-character-info 676,27270 (defcustom x-symbol-context-info 695,28145 (defcustom x-symbol-charsym-modeline-name 710,28745 (defcustom x-symbol-coding-name-alist716,28955 (defcustom x-symbol-coding-modeline-alist742,29899 (defcustom x-symbol-modeline-state-list757,30432 (defcustom x-symbol-set-coding-system-if-undecided 794,31811 (defcustom x-symbol-auto-coding-search-limit 807,32387 (defcustom x-symbol-charsym-ascii-alist 819,32858 (defcustom x-symbol-charsym-ascii-groups832,33446 (defcustom x-symbol-valid-charsym-function 843,33930 (defvar x-symbol-user-table 849,34181 (defvar x-symbol-mule-change-default-face 861,34742 (defcustom x-symbol-map-default-keys-alist872,35242 (defcustom x-symbol-map-default-bindings902,36271 (defvar x-symbol-after-init-input-hook 915,36725 (defvar x-symbol-menu929,37366 (defcustom x-symbol-menu-max-items 1005,40730 (defcustom x-symbol-header-groups-alist1013,41090 (defcustom x-symbol-completions-buffer 1042,42228 (defcustom x-symbol-grid-buffer-format 1049,42470 (defcustom x-symbol-grid-reuse 1058,42862 (defcustom x-symbol-grid-header-echo1065,43142 (defcustom x-symbol-grid-ignore-charsyms 1076,43585 (defcustom x-symbol-grid-tab-width 1082,43812 (defface x-symbol-heading-face1089,44115 (defvar x-symbol-heading-strut-glyph1101,44565 (defvar x-symbol-key-init-ignore 1115,45116 (defvar x-symbol-quail-init-ignore 1119,45254 (defvar x-symbol-context-init-ignore 1123,45394 (defcustom x-symbol-context-ignore 1130,45685 (defcustom x-symbol-electric-ignore 1138,46014 (defcustom x-symbol-rotate-suffix-char 1149,46535 (defcustom x-symbol-rotate-prefix-alist1158,46977 (defvar x-symbol-list-mode-hook 1181,47657 (defvar x-symbol-key-min-length 1186,47824 (defvar x-symbol-quail-suffix-string 1191,48048 (defvar x-symbol-define-input-method-quail 1194,48100 (defcustom x-symbol-idle-delay 1201,48355 (defface x-symbol-revealed-face1209,48703 (defcustom x-symbol-context-info-ignore 1217,48995 (defcustom x-symbol-context-info-threshold 1225,49388 (defcustom x-symbol-context-info-ignore-regexp 1231,49594 (defcustom x-symbol-context-info-ignore-groups1237,49821 (defface x-symbol-info-face1251,50343 (defface x-symbol-emph-info-face1262,50788 (defcustom x-symbol-info-intro-after1270,51073 (defcustom x-symbol-info-intro-before1279,51379 (defcustom x-symbol-info-intro-highlight1288,51684 (defcustom x-symbol-info-intro-list1297,52025 (defcustom x-symbol-info-intro-yank1306,52413 (defcustom x-symbol-info-alias-after1315,52795 (defcustom x-symbol-info-alias-before1325,53227 (defcustom x-symbol-info-context-pre1335,53644 (defcustom x-symbol-info-context-post1344,54033 (defcustom x-symbol-info-token-pre 1353,54349 (defcustom x-symbol-info-token-charsym1360,54609 (defcustom x-symbol-info-classes-pre 1369,54957 (defcustom x-symbol-info-classes-sep 1376,55213 (defcustom x-symbol-info-classes-post 1383,55468 (defcustom x-symbol-info-classes-charsym 1390,55728 (defcustom x-symbol-info-coding-pre 1397,56006 (defcustom x-symbol-info-coding-sep 1404,56252 (defcustom x-symbol-info-coding-post 1411,56499 (defcustom x-symbol-info-coding-alist1418,56723 (defcustom x-symbol-info-keys-keymaps 1434,57353 (defcustom x-symbol-info-keys-pre1442,57729 (defcustom x-symbol-info-keys-sep 1451,58097 (defcustom x-symbol-info-keys-post 1458,58354 (defconst x-symbol-fancy-cache-size 1465,58581 (defvar x-symbol-cache-size 1468,58688 (defvar x-symbol-modify-aspects-alist1477,59011 (defvar x-symbol-rotate-aspects-alist1491,59696 (defvar x-symbol-group-input-alist1507,60510 (defvar x-symbol-group-syntax-alist1557,62097 (defvar x-symbol-subgroup-string-alist1600,63344 (defvar x-symbol-latin-force-use 1614,63859 (defvar x-symbol-font-sizes1623,64369 (defvar x-symbol-font-lock-with-extra-props1633,64777 (defvar x-symbol-latin1-fonts1637,64928 (defvar x-symbol-latin2-fonts1642,65128 (defvar x-symbol-latin3-fonts1648,65391 (defvar x-symbol-latin5-fonts1654,65654 (defvar x-symbol-latin9-fonts1661,65961 (defvar x-symbol-xsymb0-fonts1666,66159 (defvar x-symbol-xsymb1-fonts1672,66448 (defcustom x-symbol-image-max-width 1683,66909 (defcustom x-symbol-image-max-height 1688,67031 (defcustom x-symbol-image-update-cache 1693,67154 (defcustom x-symbol-image-use-remote 1709,67925 (defcustom x-symbol-image-current-marker 1734,69124 (defcustom x-symbol-image-scale-method 1742,69471 (defcustom x-symbol-image-explicitly-relative-regexp 1756,70201 (defcustom x-symbol-image-searchpath-follow-symlink 1761,70383 (defcustom x-symbol-image-cache-directories1776,71078 (defvar x-symbol-image-temp-name1825,73060 (defcustom x-symbol-image-convert-mono-regexp1834,73477 (defcustom x-symbol-image-help-echo1848,74165 (defcustom x-symbol-image-editor-alist1860,74669 (defvar x-symbol-image-menu1893,76025 (defvar x-symbol-image-data-directory 1914,77028 (defvar x-symbol-image-special-glyphs1918,77195 (defcustom x-symbol-image-convert-file-alist1951,78893 (defcustom x-symbol-image-convert-program1961,79361 (defcustom x-symbol-image-converter-required 1967,79588 (defcustom x-symbol-image-converter1972,79767 (defun x-symbol-variable-interactive 2080,84357 (defcustom x-symbol-use-unicode 2099,85187 x-symbol/lisp/x-symbol-xmacs.el,522 (defun x-symbol-paren-reset-mode 102,4657 (defvar x-symbol-xmacs-default-face-fonts 136,6073 (defalias 'x-symbol-directory-files x-symbol-directory-files138,6121 (defun x-symbol-event-in-current-buffer 140,6176 (defun x-symbol-create-image 144,6318 (defalias 'x-symbol-make-glyph x-symbol-make-glyph149,6483 (defalias 'x-symbol-set-glyph-image x-symbol-set-glyph-image151,6528 (defun x-symbol-set-face-font 153,6583 (defun x-symbol-event-matches-key-specifier-p 163,7016 (defun x-symbol-window-width 173,7418 doc/ProofGeneral.texi,5602 @node Top167,5076 @node Preface204,6204 @node Latest news for version 3.7.1Latest news for version 3.7.1227,6802 @node Future272,8853 @node Credits303,10152 @node Introducing Proof GeneralIntroducing Proof General409,13921 @node Installing Proof GeneralInstalling Proof General465,15963 @node Quick start guideQuick start guide479,16412 @node Features of Proof GeneralFeatures of Proof General523,18533 @node Supported proof assistantsSupported proof assistants612,22470 @node Prerequisites for this manualPrerequisites for this manual661,24390 @node Organization of this manualOrganization of this manual705,26016 @node Basic Script ManagementBasic Script Management731,26844 @node Walkthrough example in IsabelleWalkthrough example in Isabelle750,27444 @node Proof scriptsProof scripts1001,37097 @node Script buffersScript buffers1044,39217 @node Locked queue and editing regionsLocked queue and editing regions1066,39794 @node Goal-save sequencesGoal-save sequences1122,41941 @node Active scripting bufferActive scripting buffer1159,43427 @node Summary of Proof General buffersSummary of Proof General buffers1228,46847 @node Script editing commandsScript editing commands1290,49521 @node Script processing commandsScript processing commands1368,52380 @node Proof assistant commandsProof assistant commands1496,57681 @node Toolbar commandsToolbar commands1662,63460 @node Interrupting during trace outputInterrupting during trace output1686,64389 @node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing1725,66313 @node Goals buffer commandsGoals buffer commands1739,66813 @node Advanced Script Management and EditingAdvanced Script Management and Editing1828,70352 @node Visibility of completed proofsVisibility of completed proofs1860,71564 @node Switching between proof scriptsSwitching between proof scripts1915,73487 @node View of processed files View of processed files 1952,75459 @node Retracting across filesRetracting across files2012,78510 @node Asserting across filesAsserting across files2025,79141 @node Automatic multiple file handlingAutomatic multiple file handling2038,79707 @node Escaping script managementEscaping script management2063,80741 @node Editing featuresEditing features2121,82944 @node Experimental featuresExperimental features2185,85616 @node Support for other PackagesSupport for other Packages2219,86880 @node Syntax highlightingSyntax highlighting2252,87775 @node X-Symbol supportX-Symbol support2291,89396 @node Unicode supportUnicode support2349,91936 @node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)2464,96733 @node Support for outline modeSupport for outline mode2523,98863 @node Support for completionSupport for completion2549,99993 @node Support for tagsSupport for tags2607,102169 @node Customizing Proof GeneralCustomizing Proof General2659,104498 @node Basic optionsBasic options2699,106168 @node How to customizeHow to customize2723,106926 @node Display customizationDisplay customization2774,109028 @node User optionsUser options2899,114266 @node Changing facesChanging faces3171,123965 @node Tweaking configuration settingsTweaking configuration settings3246,126634 @node Hints and TipsHints and Tips3303,129160 @node Adding your own keybindingsAdding your own keybindings3322,129761 @node Using file variablesUsing file variables3378,132294 @node Using abbreviationsUsing abbreviations3437,134480 @node LEGO Proof GeneralLEGO Proof General3476,135896 @node LEGO specific commandsLEGO specific commands3517,137265 @node LEGO tagsLEGO tags3537,137720 @node LEGO customizationsLEGO customizations3547,137967 @node Coq Proof GeneralCoq Proof General3579,138886 @node Coq-specific commandsCoq-specific commands3595,139295 @node Coq-specific variablesCoq-specific variables3617,139802 @node Editing multiple proofsEditing multiple proofs3639,140460 @node User-loaded tacticsUser-loaded tactics3663,141568 @node Holes featureHoles feature3727,144042 @node Isabelle Proof GeneralIsabelle Proof General3754,145329 @node Choosing logic and starting isabelleChoosing logic and starting isabelle3785,146498 @node Isabelle commandsIsabelle commands3860,149547 @node Isabelle settingsIsabelle settings4003,153702 @node Isabelle customizationsIsabelle customizations4017,154284 @node HOL Proof GeneralHOL Proof General4040,154771 @node Shell Proof GeneralShell Proof General4082,156593 @node Obtaining and InstallingObtaining and Installing4118,158052 @node Obtaining Proof GeneralObtaining Proof General4134,158465 @node Installing Proof General from tarballInstalling Proof General from tarball4165,159704 @node Installing Proof General from RPM packageInstalling Proof General from RPM package4190,160536 @node Setting the names of binariesSetting the names of binaries4205,160944 @node Notes for syssiesNotes for syssies4233,161884 @node Bugs and EnhancementsBugs and Enhancements4308,164920 @node References4329,165735 @node History of Proof GeneralHistory of Proof General4369,166758 @node Old News for 3.0Old News for 3.04460,170860 @node Old News for 3.1Old News for 3.14530,174554 @node Old News for 3.2Old News for 3.24556,175726 @node Old News for 3.3Old News for 3.34617,178729 @node Old News for 3.4Old News for 3.44636,179626 @node Function IndexFunction Index4659,180682 @node Variable IndexVariable Index4663,180758 @node Keystroke IndexKeystroke Index4667,180838 @node Concept IndexConcept Index4671,180904 doc/PG-adapting.texi,3776 @node Top157,4776 @node Introduction195,5921 @node Future236,7574 @node Credits272,9170 @node Beginning with a New ProverBeginning with a New Prover282,9462 @node Overview of adding a new proverOverview of adding a new prover323,11411 @node Demonstration instance and easy configurationDemonstration instance and easy configuration401,14719 @node Major modes used by Proof GeneralMajor modes used by Proof General470,18110 @node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands503,19461 @node Settings for generic user-level commandsSettings for generic user-level commands518,20007 @node Menu configurationMenu configuration563,21741 @node Toolbar configurationToolbar configuration587,22658 @node Proof Script SettingsProof Script Settings645,24900 @node Recognizing commands and commentsRecognizing commands and comments667,25480 @node Recognizing proofsRecognizing proofs788,30987 @node Recognizing other elementsRecognizing other elements900,35800 @node Configuring undo behaviourConfiguring undo behaviour1026,41311 @node Nested proofsNested proofs1163,46705 @node Safe (state-preserving) commandsSafe (state-preserving) commands1203,48331 @node Activate scripting hookActivate scripting hook1226,49277 @node Automatic multiple filesAutomatic multiple files1250,50140 @node Completions1272,50987 @node Proof Shell SettingsProof Shell Settings1313,52476 @node Proof shell commandsProof shell commands1344,53758 @node Script input to the shellScript input to the shell1508,60697 @node Settings for matching various output from proof processSettings for matching various output from proof process1575,63744 @node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process1706,69493 @node Hooks and other settingsHooks and other settings1921,79364 @node Goals Buffer SettingsGoals Buffer Settings2002,82733 @node Splash Screen SettingsSplash Screen Settings2079,85832 @node Global ConstantsGlobal Constants2105,86590 @node Handling Multiple FilesHandling Multiple Files2131,87431 @node Configuring Editing SyntaxConfiguring Editing Syntax2283,95214 @node Configuring Font LockConfiguring Font Lock2342,97335 @node Configuring X-SymbolConfiguring X-Symbol2429,101620 @node Writing More Lisp CodeWriting More Lisp Code2489,104140 @node Default values for generic settingsDefault values for generic settings2506,104785 @node Adding prover-specific configurationsAdding prover-specific configurations2536,105868 @node Useful variablesUseful variables2579,107150 @node Useful functions and macrosUseful functions and macros2594,107649 @node Internals of Proof GeneralInternals of Proof General2697,111604 @node Spans2725,112512 @node Proof General site configurationProof General site configuration2738,112886 @node Configuration variable mechanismsConfiguration variable mechanisms2818,115932 @node Global variablesGlobal variables2939,121362 @node Proof script modeProof script mode3009,123910 @node Proof shell modeProof shell mode3268,135565 @node Debugging3675,151647 @node Plans and IdeasPlans and Ideas3718,152523 @node Proof by pointing and similar featuresProof by pointing and similar features3739,153245 @node Granularity of atomic command sequencesGranularity of atomic command sequences3777,154903 @node Browser mode for script files and theoriesBrowser mode for script files and theories3822,157128 @node Demonstration InstantiationsDemonstration Instantiations3852,158159 @node demoisa-easy.el3868,158590 @node demoisa.el3931,160828 @node Function IndexFunction Index4086,165812 @node Variable IndexVariable Index4090,165888 @node Concept IndexConcept Index4099,166067 x-symbol/lisp/_pkg.el,0 x-symbol/lisp/custom-load.el,0 lib/holes-load.el,0 generic/proof.el,0 generic/proof-autoloads.el,0 twelf/x-symbol-twelf.el,0 pgshell/pgshell.el,0 lego/x-symbol-lego.el,0 isar/isar-autotest.el,0 isar/interface-setup.el,0 hol98/x-symbol-hol98.el,0 hol98/hol98.el,0 demoisa/demoisa-easy.el,0 coq/coq-mmm.el,0 coq/coq-autotest.el,0 ccc/ccc.el,0 acl2/x-symbol-acl2.el,0 acl2/acl2.el,0