ccc/ccc.el,87
(defvar ccc-keywords 17,587
(defvar ccc-tactics 18,613
(defvar ccc-tacticals 19,638

coq/coq-abbrev.el,495
(defun holes-show-doc 12,313
(defun coq-local-vars-list-show-doc 16,390
(defconst coq-tactics-menu21,490
(defconst coq-tactics-abbrev-table26,667
(defconst coq-tacticals-menu29,784
(defconst coq-tacticals-abbrev-table33,893
(defconst coq-commands-menu36,984
(defconst coq-commands-abbrev-table43,1207
(defconst coq-terms-menu46,1296
(defconst coq-terms-abbrev-table51,1434
(defun coq-install-abbrevs 58,1628
(defpgdefault menu-entries80,2533
(defpgdefault help-menu-entries145,4647

coq/coq-db.el,678
(defconst coq-syntax-db 24,596
(defun coq-insert-from-db 70,2319
(defun coq-build-regexp-list-from-db 88,3050
(defun coq-build-opt-regexp-from-db 107,3856
(defun max-length-db 126,4677
(defun coq-build-menu-from-db-internal 138,4952
(defun coq-build-title-menu 175,6493
(defun coq-sort-menu-entries 184,6861
(defun coq-build-menu-from-db 190,6988
(defcustom coq-holes-minor-mode 212,7827
(defun coq-build-abbrev-table-from-db 218,7971
(defun filter-state-preserving 237,8597
(defun filter-state-changing 242,8751
(defface coq-solve-tactics-face249,8972
(defface coq-cheat-face258,9302
(defconst coq-solve-tactics-face 266,9550
(defconst coq-cheat-face 270,9714

coq/coq.el,9426
(defcustom coq-prog-name61,1977
(defcustom coq-translate-to-v8 80,2829
(defun coq-build-prog-args 85,2944
(defcustom coq-compiler95,3267
(defcustom coq-dependency-analyzer101,3404
(defcustom coq-use-makefile 107,3544
(defcustom coq-default-undo-limit 113,3716
(defconst coq-shell-init-cmd118,3844
(defcustom coq-prog-env 127,4171
(defconst coq-shell-restart-cmd 135,4420
(defvar coq-shell-prompt-pattern137,4474
(defvar coq-shell-cd 145,4777
(defvar coq-shell-proof-completed-regexp 149,4937
(defvar coq-goal-regexp152,5122
(defun get-coq-library-directory 157,5218
(defconst coq-library-directory 163,5400
(defcustom coq-tags 166,5527
(defconst coq-interrupt-regexp 171,5675
(defcustom coq-www-home-page 174,5768
(defcustom coq-end-goals-regexp-hide-subgoals 179,5875
(defcustom coq-end-goals-regexp-show-subgoals 185,6112
(defgroup coq-proof-tree 197,6413
(defcustom coq-proof-tree-ignored-commands-regexp202,6553
(defcustom coq-navigation-command-regexp208,6730
(defcustom coq-proof-tree-cheating-regexp214,6902
(defcustom coq-proof-tree-current-goal-regexp220,7042
(defcustom coq-proof-tree-update-goal-regexp227,7296
(defcustom coq-proof-tree-additional-subgoal-ID-regexp234,7530
(defcustom coq-proof-tree-existential-regexp 240,7728
(defcustom coq-proof-tree-instantiated-existential-regexp245,7882
(defcustom coq-proof-tree-existentials-state-start-regexp251,8102
(defcustom coq-proof-tree-existentials-state-end-regexp 257,8292
(defcustom coq-proof-tree-proof-completed-regexp262,8461
(defvar coq-outline-regexp274,8732
(defvar coq-outline-heading-end-regexp 281,8945
(defvar coq-shell-outline-regexp 283,8999
(defvar coq-shell-outline-heading-end-regexp 284,9049
(defconst coq-state-preserving-tactics-regexp287,9113
(defconst coq-state-changing-commands-regexp289,9215
(defconst coq-state-preserving-commands-regexp291,9324
(defconst coq-commands-regexp293,9437
(defvar coq-retractable-instruct-regexp295,9516
(defvar coq-non-retractable-instruct-regexp297,9608
(defcustom coq-use-smie 329,10304
(defcustom coq-indent-box-style 335,10501
(defconst coq-smie-grammar354,10795
(defun coq-smie-search-token-forward 418,13720
(defun coq-smie-search-token-backward 431,14227
(defconst coq-smie-proof-end-tokens459,15562
(defun coq-smie-forward-token 463,15692
(defun coq-smie-backward-token 513,17645
(defun coq-smie-rules 600,21089
(defconst coq-script-command-end-regexp 682,24880
(defun coq-script-parse-function 691,25309
(defun coq-set-undo-limit 698,25535
(defun build-list-id-from-string 702,25665
(defun coq-last-prompt-info 711,26140
(defun coq-last-prompt-info-safe 729,27034
(defvar coq-last-but-one-statenum 737,27387
(defvar coq-last-but-one-proofnum 744,27684
(defvar coq-last-but-one-proofstack 747,27782
(defsubst coq-get-span-statenum 750,27892
(defsubst coq-get-span-proofnum 754,28007
(defsubst coq-get-span-proofstack 758,28122
(defsubst coq-set-span-statenum 762,28266
(defsubst coq-get-span-goalcmd 766,28397
(defsubst coq-set-span-goalcmd 770,28511
(defsubst coq-set-span-proofnum 774,28641
(defsubst coq-set-span-proofstack 778,28772
(defsubst proof-last-locked-span 782,28932
(defun proof-clone-buffer 786,29066
(defun proof-store-buffer-win 800,29603
(defun proof-store-response-win 811,30096
(defun proof-store-goals-win 815,30223
(defun coq-set-state-infos 827,30755
(defun count-not-intersection 865,32845
(defun coq-find-and-forget 895,34097
(defvar coq-current-goal 922,35402
(defun coq-goal-hyp 925,35467
(defun coq-state-preserving-p 938,35941
(defun coq-hide-additional-subgoals-switch 948,36235
(defconst notation-print-kinds-table961,36600
(defun coq-PrintScope 965,36767
(defun coq-guess-or-ask-for-string 983,37316
(defun coq-ask-do 997,37856
(defsubst coq-put-into-brackets 1006,38241
(defsubst coq-put-into-quotes 1009,38302
(defun coq-SearchIsos 1012,38361
(defun coq-SearchConstant 1020,38600
(defun coq-Searchregexp 1024,38693
(defun coq-SearchRewrite 1030,38834
(defun coq-SearchAbout 1034,38931
(defun coq-Print 1040,39074
(defun coq-About 1045,39198
(defun coq-LocateConstant 1050,39317
(defun coq-LocateLibrary 1055,39420
(defun coq-LocateNotation 1060,39537
(defun coq-Pwd 1068,39768
(defun coq-Inspect 1073,39892
(defun coq-PrintSection(1077,39992
(defun coq-Print-implicit 1081,40085
(defun coq-Check 1086,40236
(defun coq-Show 1091,40344
(defun coq-Compile 1105,40787
(defun coq-guess-command-line 1117,41105
(defpacustom use-editing-holes 1154,42662
(defun coq-mode-config 1163,42965
(defun coq-shell-mode-config 1268,46776
(defun coq-goals-mode-config 1341,49970
(defun coq-response-config 1348,50214
(defpacustom hide-additional-subgoals 1371,50931
(defpacustom print-fully-explicit 1381,51241
(defpacustom print-implicit 1386,51389
(defpacustom print-coercions 1391,51555
(defpacustom print-match-wildcards 1396,51699
(defpacustom print-elim-types 1401,51879
(defpacustom printing-depth 1406,52045
(defpacustom undo-depth 1411,52206
(defpacustom time-commands 1416,52372
(defgroup coq-auto-compile 1427,52622
(defpacustom compile-before-require 1432,52773
(defcustom coq-compile-command 1444,53265
(defconst coq-compile-substitution-list1474,54548
(defcustom coq-load-path 1494,55469
(defcustom coq-compile-auto-save 1545,57990
(defcustom coq-lock-ancestors 1570,59048
(defpacustom confirm-external-compilation 1579,59369
(defcustom coq-load-path-include-current 1588,59676
(defcustom coq-compile-ignored-directories 1597,59994
(defcustom coq-compile-ignore-library-directory 1610,60627
(defcustom coq-coqdep-error-regexp1622,61115
(defconst coq-require-command-regexp1638,61833
(defconst coq-require-id-regexp1645,62190
(defvar coq-compile-history 1653,62624
(defvar coq-compile-response-buffer 1656,62708
(defvar coq-debug-auto-compilation 1660,62843
(defun time-less-or-equal 1666,62951
(defun coq-max-dep-mod-time 1674,63289
(defun coq-prog-args 1697,64093
(defun coq-lock-ancestor 1706,64352
(defun coq-unlock-ancestor 1722,65127
(defun coq-unlock-all-ancestors-of-span 1729,65422
(defun coq-compile-ignore-file 1736,65718
(defun coq-library-src-of-obj-file 1760,66605
(defun coq-option-of-load-path-entry 1765,66837
(defun coq-include-options 1781,67428
(defun coq-init-compile-response-buffer 1801,68252
(defun coq-display-compile-response-buffer 1824,69324
(defun coq-get-library-dependencies 1838,69958
(defun coq-compile-library 1885,72183
(defun coq-compile-library-if-necessary 1912,73394
(defun coq-make-lib-up-to-date 1958,75266
(defun coq-auto-compile-externally 2014,77729
(defun coq-map-module-id-to-obj-file 2057,79875
(defun coq-check-module 2110,82477
(defvar coq-process-require-current-buffer2138,83919
(defun coq-compile-save-buffer-filter 2144,84184
(defun coq-compile-save-some-buffers 2154,84598
(defun coq-preprocess-require-commands 2176,85500
(defun coq-switch-buffer-kill-proof-shell 2209,87069
(defun coq-proof-tree-get-proof-info 2229,87702
(defun coq-extract-instantiated-existentials 2239,88090
(defun coq-show-sequent-command 2248,88482
(defun coq-proof-tree-get-new-subgoals 2252,88636
(defun coq-find-begin-of-unfinished-proof 2296,90761
(defun coq-preprocessing 2321,91775
(defun coq-fake-constant-markup 2335,92230
(defun coq-create-span-menu 2351,92835
(defconst module-kinds-table2369,93348
(defconst modtype-kinds-table2373,93497
(defun coq-insert-section-or-module 2377,93626
(defconst reqkinds-kinds-table2398,94476
(defun coq-insert-requires 2402,94620
(defun coq-end-Section 2415,95099
(defun coq-insert-intros 2433,95677
(defun coq-insert-infoH-hook 2445,96208
(defun coq-insert-as 2450,96416
(defun coq-insert-match 2467,97109
(defun coq-insert-solve-tactic 2496,98278
(defun coq-insert-tactic 2502,98529
(defun coq-insert-tactical 2508,98731
(defun coq-insert-command 2514,98962
(defun coq-insert-term 2519,99127
(define-key coq-keymap 2524,99288
(define-key coq-keymap 2525,99346
(define-key coq-keymap 2526,99403
(define-key coq-keymap 2527,99472
(define-key coq-keymap 2528,99528
(define-key coq-keymap 2529,99577
(define-key coq-keymap 2530,99635
(define-key coq-keymap 2531,99685
(define-key coq-keymap 2532,99740
(define-key coq-keymap 2534,99793
(define-key coq-keymap 2536,99867
(define-key coq-keymap 2537,99924
(define-key coq-keymap 2540,99989
(define-key coq-keymap 2541,100049
(define-key coq-keymap 2543,100105
(define-key coq-keymap 2544,100155
(define-key coq-keymap 2545,100205
(define-key coq-keymap 2546,100261
(define-key coq-keymap 2547,100311
(define-key coq-keymap 2548,100355
(define-key coq-keymap 2549,100414
(define-key coq-goals-mode-map 2552,100475
(define-key coq-goals-mode-map 2553,100557
(define-key coq-goals-mode-map 2554,100639
(define-key coq-goals-mode-map 2555,100726
(define-key coq-goals-mode-map 2556,100808
(defvar last-coq-error-location 2565,101113
(defun coq-get-last-error-location 2573,101497
(defun coq-highlight-error 2623,104060
(defun coq-highlight-error-hook 2651,105141
(defun coq-first-word-before 2661,105358
(defun coq-show-first-goal 2672,105690
(defvar coq-modeline-string2 2688,106355
(defvar coq-modeline-string1 2689,106389
(defvar coq-modeline-string0 2690,106423
(defun coq-build-subgoals-string 2691,106464
(defun coq-update-minor-mode-alist 2696,106630
(defun is-not-split-vertic 2728,108045
(defun optim-resp-windows 2737,108485

coq/coq-indent.el,2565
(defconst coq-any-command-regexp20,368
(defconst coq-indent-inner-regexp23,442
(defconst coq-comment-start-regexp 33,804
(defconst coq-comment-end-regexp 34,847
(defconst coq-comment-start-or-end-regexp35,888
(defconst coq-indent-open-regexp37,996
(defconst coq-indent-close-regexp42,1193
(defconst coq-indent-closepar-regexp 48,1392
(defconst coq-indent-closematch-regexp 49,1437
(defconst coq-indent-openpar-regexp 50,1508
(defconst coq-indent-openmatch-regexp 51,1552
(defconst coq-tacticals-tactics-regex52,1632
(defconst coq-indent-any-regexp54,1751
(defconst coq-indent-kw58,1967
(defconst coq-indent-pattern-regexp 68,2433
(defun coq-indent-goal-command-p 72,2536
(defconst coq-end-command-regexp94,3590
(defun coq-search-comment-delimiter-forward 103,4095
(defun coq-search-comment-delimiter-backward 112,4425
(defun coq-skip-until-one-comment-backward 119,4699
(defun coq-skip-until-one-comment-forward 134,5406
(defun coq-looking-at-comment 145,5924
(defun coq-find-comment-start 149,6065
(defun coq-find-comment-end 160,6498
(defun coq-looking-at-syntactic-context 172,6991
(defconst coq-end-command-or-comment-regexp178,7213
(defconst coq-end-command-or-comment-start-regexp181,7322
(defun coq-find-not-in-comment-backward 184,7439
(defun coq-find-not-in-comment-forward 204,8329
(defun coq-is-on-ending-context 230,9521
(defun coq-empty-command-p 239,9734
(defun coq-script-parse-cmdend-forward 254,10475
(defun coq-script-parse-cmdend-backward 306,12936
(defun coq-find-current-start 347,14810
(defun coq-find-real-start 356,15136
(defun same-line 362,15354
(defun coq-command-at-point 365,15441
(defun coq-commands-at-line 380,16052
(defun coq-indent-only-spaces-on-line 404,17018
(defun coq-indent-find-reg 410,17295
(defun coq-find-no-syntactic-on-line 424,17831
(defun coq-back-to-indentation-prevline 437,18304
(defun coq-find-unclosed 483,20371
(defun coq-find-at-same-level-zero 513,21681
(defun coq-find-unopened 542,22947
(defun coq-find-last-unopened 585,24381
(defun coq-end-offset 596,24778
(defun coq-add-iter 621,25548
(defun coq-goal-count 624,25654
(defun coq-save-count 626,25726
(defun coq-proof-count 631,25928
(defun coq-goal-save-diff-maybe-proof 637,26216
(defun coq-indent-command-offset 647,26510
(defun coq-indent-expr-offset 713,29691
(defun coq-indent-comment-offset 832,34573
(defun coq-indent-offset 864,36025
(defun coq-indent-calculate 883,36899
(defun coq-indent-line 886,36987
(defun coq-indent-line-not-comments 896,37353
(defun coq-indent-region 906,37742

coq/coq-local-vars.el,229
(defconst coq-local-vars-doc 23,414
(defun coq-insert-coq-prog-name 86,2736
(defun coq-read-directory 99,3287
(defun coq-ask-load-path 116,4102
(defun coq-ask-prog-name 134,4935
(defun coq-ask-insert-coq-prog-name 151,5646

coq/coq-syntax.el,2736
(defcustom coq-user-tactics-db 21,533
(defcustom coq-user-commands-db 38,1046
(defcustom coq-user-tacticals-db 54,1565
(defcustom coq-user-solve-tactics-db 70,2086
(defcustom coq-user-cheat-tactics-db 86,2605
(defcustom coq-user-reserved-db 105,3151
(defvar coq-tactics-db123,3682
(defvar coq-solve-tactics-db296,12816
(defvar coq-solve-cheat-tactics-db323,13839
(defvar coq-tacticals-db335,14014
(defvar coq-decl-db359,14900
(defvar coq-defn-db384,16356
(defvar coq-goal-starters-db449,21078
(defvar coq-other-commands-db479,22881
(defvar coq-commands-db614,32866
(defvar coq-terms-db621,33086
(defun coq-count-match 683,35701
(defun coq-module-opening-p 699,36430
(defun coq-section-command-p 710,36841
(defun coq-goal-command-str-p 714,36938
(defun coq-goal-command-p 741,38040
(defvar coq-keywords-save-strict751,38379
(defvar coq-keywords-save758,38620
(defun coq-save-command-p 763,38699
(defvar coq-keywords-kill-goal774,39027
(defvar coq-keywords-state-changing-misc-commands778,39117
(defvar coq-keywords-goal781,39242
(defvar coq-keywords-decl784,39325
(defvar coq-keywords-defn787,39399
(defvar coq-keywords-state-changing-commands791,39474
(defvar coq-keywords-state-preserving-commands800,39734
(defvar coq-keywords-commands805,39950
(defvar coq-solve-tactics810,40098
(defvar coq-solve-tactics-regexp814,40219
(defvar coq-solve-cheat-tactics818,40353
(defvar coq-solve-cheat-tactics-regexp822,40498
(defvar coq-tacticals826,40656
(defvar coq-reserved832,40795
(defvar coq-reserved-regexp 842,41130
(defvar coq-state-changing-tactics846,41241
(defvar coq-state-preserving-tactics849,41350
(defvar coq-tactics853,41464
(defvar coq-tactics-regexp 856,41553
(defvar coq-retractable-instruct859,41708
(defvar coq-non-retractable-instruct862,41818
(defvar coq-keywords866,41946
(defun proof-regexp-alt-list-symb 872,42170
(defvar coq-keywords-regexp 875,42275
(defvar coq-symbols878,42348
(defvar coq-error-regexp 900,42589
(defvar coq-id 903,42817
(defvar coq-id-shy 904,42842
(defvar coq-ids 907,42944
(defun coq-first-abstr-regexp 909,43010
(defcustom coq-variable-highlight-enable 912,43105
(defvar coq-font-lock-terms918,43232
(defconst coq-save-command-regexp-strict940,44315
(defconst coq-save-command-regexp946,44483
(defconst coq-save-with-hole-regexp951,44636
(defconst coq-goal-command-regexp955,44796
(defconst coq-goal-with-hole-regexp958,44898
(defconst coq-decl-with-hole-regexp962,45032
(defconst coq-defn-with-hole-regexp969,45282
(defconst coq-with-with-hole-regexp979,45572
(defvar coq-font-lock-keywords-1994,46102
(defvar coq-font-lock-keywords 1022,47437
(defun coq-init-syntax-table 1024,47495
(defconst coq-generic-expression1049,48222

coq/coq-unicode-tokens.el,454
(defconst coq-token-format 39,1427
(defconst coq-token-match 40,1475
(defconst coq-hexcode-match 41,1506
(defun coq-unicode-tokens-set 43,1540
(defcustom coq-token-symbol-map49,1768
(defcustom coq-shortcut-alist165,4719
(defconst coq-control-char-format-regexp254,6737
(defconst coq-control-char-format 258,6862
(defconst coq-control-characters260,6905
(defconst coq-control-region-format-regexp 264,6997
(defconst coq-control-regions266,7080

hol98/hol98.el,121
(defvar hol98-keywords 17,374
(defvar hol98-rules 18,402
(defvar hol98-tactics 19,427
(defvar hol98-tacticals 20,454

isar/isabelle-system.el,1254
(defgroup isabelle 31,822
(defcustom isabelle-web-page35,950
(defcustom isa-isabelle-command44,1167
(defvar isabelle-not-found 62,1849
(defun isa-set-isabelle-command 65,1964
(defun isa-shell-command-to-string 88,2982
(defun isa-getenv 94,3206
(defcustom isabelle-program-name-override 114,3905
(defun isa-tool-list-logics 125,4251
(defcustom isabelle-logics-available 132,4497
(defcustom isabelle-chosen-logic 142,4834
(defvar isabelle-chosen-logic-prev 158,5418
(defun isabelle-hack-local-variables-function 161,5538
(defun isabelle-set-prog-name 173,5977
(defun isabelle-choose-logic 197,7097
(defun isa-view-doc 216,7859
(defun isa-tool-list-docs 223,8085
(defconst isabelle-verbatim-regexp 241,8815
(defun isabelle-verbatim 244,8957
(defcustom isabelle-refresh-logics 251,9118
(defvar isabelle-docs-menu259,9446
(defvar isabelle-logics-menu-entries 266,9731
(defun isabelle-logics-menu-calculate 269,9804
(defvar isabelle-time-to-refresh-logics 290,10446
(defun isabelle-logics-menu-refresh 294,10541
(defun isabelle-menu-bar-update-logics 309,11188
(defun isabelle-load-isar-keywords 325,11817
(defun isabelle-create-span-menu 346,12545
(defun isabelle-xml-sml-escapes 362,12976
(defun isabelle-process-pgip 365,13077

isar/isar-autotest.el,31
(defvar isar-long-tests 8,133

isar/isar.el,1595
(defcustom isar-keywords-name 41,895
(defpgdefault completion-table 57,1406
(defcustom isar-web-page59,1459
(defun isar-strip-terminators 73,1809
(defun isar-markup-ml 85,2165
(defun isar-mode-config-set-variables 90,2300
(defun isar-shell-mode-config-set-variables 155,5099
(defun isar-set-proof-find-theorems-command 237,8289
(defpacustom use-find-theorems-form 243,8473
(defun isar-set-undo-commands 248,8639
(defpacustom use-linear-undo 263,9272
(defun isar-configure-from-settings 268,9430
(defun isar-remove-file 276,9580
(defun isar-shell-compute-new-files-list 288,9884
(define-derived-mode isar-shell-mode 307,10454
(define-derived-mode isar-response-mode 312,10581
(define-derived-mode isar-goals-mode 317,10714
(define-derived-mode isar-mode 322,10840
(defpgdefault menu-entries374,12555
(defun isar-set-command 405,13749
(defpgdefault help-menu-entries 410,13879
(defun isar-count-undos 413,13955
(defun isar-find-and-forget 439,14921
(defun isar-goal-command-p 475,16264
(defun isar-global-save-command-p 480,16441
(defvar isar-current-goal 501,17225
(defun isar-state-preserving-p 504,17291
(defvar isar-shell-current-line-width 529,18140
(defun isar-shell-adjust-line-width 534,18332
(defsubst isar-string-wrapping 557,19097
(defsubst isar-positions-of 566,19291
(defcustom isar-wrap-commands-singly 572,19496
(defun isar-command-wrapping 578,19692
(defun isar-preprocessing 586,20006
(defun isar-mode-config 604,20557
(defun isar-shell-mode-config 618,21210
(defun isar-response-mode-config 628,21559
(defun isar-goals-mode-config 638,21894

isar/isar-find-theorems.el,778
(defvar isar-find-theorems-data 19,507
(defun isar-find-theorems-minibuffer 35,981
(defun isar-find-theorems-form 49,1600
(defvar isar-find-theorems-widget-number 92,3474
(defvar isar-find-theorems-widget-pattern 95,3572
(defvar isar-find-theorems-widget-intro 98,3664
(defvar isar-find-theorems-widget-elim 101,3750
(defvar isar-find-theorems-widget-dest 104,3834
(defvar isar-find-theorems-widget-name 107,3918
(defvar isar-find-theorems-widget-simp 110,4005
(defun isar-find-theorems-create-searchform115,4151
(defun isar-find-theorems-create-help 255,8694
(defun isar-find-theorems-submit-searchform298,10866
(defun isar-find-theorems-parse-criteria 376,13236
(defun isar-find-theorems-parse-number 469,16217
(defun isar-find-theorems-filter-empty 479,16494

isar/isar-keywords.el,1064
(defconst isar-keywords-major7,222
(defconst isar-keywords-minor280,4856
(defconst isar-keywords-control339,5659
(defconst isar-keywords-diag360,6153
(defconst isar-keywords-theory-begin434,7438
(defconst isar-keywords-theory-switch437,7491
(defconst isar-keywords-theory-end440,7537
(defconst isar-keywords-theory-heading443,7585
(defconst isar-keywords-theory-decl449,7692
(defconst isar-keywords-theory-script552,9481
(defconst isar-keywords-theory-goal555,9544
(defconst isar-keywords-qed583,10059
(defconst isar-keywords-qed-block590,10145
(defconst isar-keywords-qed-global593,10192
(defconst isar-keywords-proof-heading596,10241
(defconst isar-keywords-proof-goal601,10324
(defconst isar-keywords-proof-block606,10401
(defconst isar-keywords-proof-open610,10463
(defconst isar-keywords-proof-close613,10509
(defconst isar-keywords-proof-chain616,10556
(defconst isar-keywords-proof-decl623,10659
(defconst isar-keywords-proof-asm635,10821
(defconst isar-keywords-proof-asm-goal642,10916
(defconst isar-keywords-proof-script648,11005

isar/isar-mmm.el,81
(defconst isar-start-latex-regexp24,696
(defconst isar-start-sml-regexp36,1124

isar/isar-syntax.el,4005
(defconst isar-script-syntax-table-entries18,432
(defconst isar-script-syntax-table-alist42,834
(defun isar-init-syntax-table 51,1117
(defun isar-init-output-syntax-table 59,1364
(defconst isar-keyword-begin 74,1806
(defconst isar-keyword-end 75,1844
(defconst isar-keywords-theory-enclose77,1879
(defconst isar-keywords-theory82,2017
(defconst isar-keywords-save87,2148
(defconst isar-keywords-proof-enclose92,2263
(defconst isar-keywords-proof98,2424
(defconst isar-keywords-proof-context105,2601
(defconst isar-keywords-local-goal109,2708
(defconst isar-keywords-proper113,2813
(defconst isar-keywords-improper118,2932
(defconst isar-keyword-level-alist123,3064
(defconst isar-keywords-outline 138,3535
(defconst isar-keywords-indent-open141,3611
(defconst isar-keywords-indent-close148,3797
(defconst isar-keywords-indent-enclose153,3930
(defconst isar-ext-first 163,4159
(defconst isar-ext-rest 164,4226
(defconst isar-text 166,4298
(defconst isar-long-id-stuff 167,4331
(defconst isar-id 168,4405
(defconst isar-idx 169,4475
(defconst isar-string 171,4534
(defun isar-ids-to-regexp 173,4594
(defconst isar-any-command-regexp205,6386
(defconst isar-name-regexp212,6759
(defconst isar-improper-regexp218,7054
(defconst isar-save-command-regexp222,7188
(defconst isar-global-save-command-regexp225,7289
(defconst isar-goal-command-regexp228,7403
(defconst isar-local-goal-command-regexp231,7511
(defconst isar-comment-start 234,7624
(defconst isar-comment-end 235,7659
(defconst isar-comment-start-regexp 236,7692
(defconst isar-comment-end-regexp 237,7763
(defconst isar-string-start-regexp 239,7831
(defconst isar-string-end-regexp 240,7883
(defun isar-syntactic-context 242,7934
(defconst isar-antiq-regexp257,8329
(defconst isar-nesting-regexp263,8480
(defun isar-nesting 266,8578
(defun isar-match-nesting 278,8971
(defface isabelle-string-face 290,9305
(defface isabelle-quote-face 298,9505
(defface isabelle-class-name-face306,9701
(defface isabelle-tfree-name-face314,9888
(defface isabelle-tvar-name-face322,10081
(defface isabelle-free-name-face330,10273
(defface isabelle-bound-name-face338,10461
(defface isabelle-var-name-face346,10652
(defconst isabelle-string-face 354,10843
(defconst isabelle-quote-face 355,10897
(defconst isabelle-class-name-face 356,10950
(defconst isabelle-tfree-name-face 357,11012
(defconst isabelle-tvar-name-face 358,11074
(defconst isabelle-free-name-face 359,11135
(defconst isabelle-bound-name-face 360,11196
(defconst isabelle-var-name-face 361,11258
(defun isar-font-lock-fontify-syntactically-region 367,11407
(defvar isar-font-lock-keywords-1402,12685
(defun isar-output-flkprops 420,13693
(defun isar-output-flk 426,13945
(defvar isar-output-font-lock-keywords-1429,14054
(defun isar-strip-output-markup 453,15053
(defconst isar-shell-font-lock-keywords457,15189
(defvar isar-goals-font-lock-keywords460,15273
(defconst isar-linear-undo 494,15952
(defconst isar-undo 496,15995
(defconst isar-pr498,16038
(defun isar-remove 505,16196
(defun isar-undos 508,16271
(defun isar-cannot-undo 518,16505
(defconst isar-undo-commands521,16575
(defconst isar-theory-start-regexp529,16712
(defconst isar-end-regexp535,16870
(defconst isar-undo-fail-regexp539,16971
(defconst isar-undo-skip-regexp543,17075
(defconst isar-undo-ignore-regexp546,17196
(defconst isar-undo-remove-regexp549,17261
(defconst isar-keywords-imenu557,17418
(defconst isar-entity-regexp 564,17609
(defconst isar-named-entity-regexp567,17705
(defconst isar-named-entity-name-match-number572,17835
(defconst isar-generic-expression575,17936
(defconst isar-indent-any-regexp586,18170
(defconst isar-indent-inner-regexp588,18263
(defconst isar-indent-enclose-regexp590,18329
(defconst isar-indent-open-regexp592,18445
(defconst isar-indent-close-regexp594,18555
(defconst isar-outline-regexp600,18692
(defconst isar-outline-heading-end-regexp 604,18845
(defconst isar-outline-heading-alist 606,18894

isar/isar-unicode-tokens.el,1363
(defgroup isabelle-tokens 25,672
(defun isar-set-and-restart-tokens 30,812
(defconst isar-control-region-format-regexp43,1165
(defconst isar-control-char-format-regexp46,1259
(defconst isar-control-char-format	52,1406
(defconst isar-control-region-format-start 53,1455
(defconst isar-control-region-format-end 54,1509
(defcustom isar-control-characters57,1565
(defcustom isar-control-regions71,1978
(defconst isar-token-format 97,2790
(defconst isar-token-variant-format-regexp101,2941
(defcustom isar-greek-letters-tokens104,3055
(defcustom isar-misc-letters-tokens144,3913
(defcustom isar-symbols-tokens156,4231
(defcustom isar-extended-symbols-tokens362,9042
(defun isar-try-char 431,10697
(defcustom isar-symbols-tokens-fallbacks435,10841
(defcustom isar-bold-nums-tokens462,11771
(defun isar-map-letters 478,12160
(defconst isar-script-letters-tokens 484,12308
(defconst isar-roman-letters-tokens 489,12462
(defconst isar-fraktur-uppercase-letters-tokens 494,12636
(defconst isar-fraktur-lowercase-letters-tokens 499,12805
(defcustom isar-token-symbol-map 504,12996
(defcustom isar-user-tokens 521,13537
(defun isar-init-token-symbol-map 535,13977
(defcustom isar-symbol-shortcuts560,14626
(defcustom isar-shortcut-alist 632,16825
(defun isar-init-shortcut-alists 640,17084
(defconst isar-tokens-customizable-variables661,17747

lego/lego.el,1636
(defcustom lego-tags 21,490
(defcustom lego-test-all-name 26,626
(defpgdefault help-menu-entries32,784
(defpgdefault menu-entries36,944
(defvar lego-shell-handle-output47,1245
(defconst lego-process-config55,1543
(defconst lego-pretty-set-width 66,1974
(defconst lego-interrupt-regexp 70,2116
(defcustom lego-www-home-page 75,2233
(defcustom lego-www-latest-release80,2357
(defcustom lego-www-refcard86,2532
(defcustom lego-library-www-page92,2681
(defvar lego-prog-name 101,2897
(defvar lego-shell-cd 104,2966
(defvar lego-shell-proof-completed-regexp 107,3065
(defvar lego-save-command-regexp110,3205
(defvar lego-goal-command-regexp112,3295
(defvar lego-kill-goal-command 115,3386
(defvar lego-forget-id-command 116,3429
(defvar lego-undoable-commands-regexp118,3475
(defvar lego-goal-regexp 127,3849
(defvar lego-outline-regexp129,3894
(defvar lego-outline-heading-end-regexp 135,4069
(defvar lego-shell-outline-regexp 137,4122
(defvar lego-shell-outline-heading-end-regexp 138,4174
(define-derived-mode lego-shell-mode 144,4453
(define-derived-mode lego-mode 151,4614
(define-derived-mode lego-goals-mode 162,4924
(defun lego-count-undos 173,5350
(defun lego-goal-command-p 192,6087
(defun lego-find-and-forget 197,6258
(defun lego-goal-hyp 239,8094
(defun lego-state-preserving-p 248,8291
(defvar lego-shell-current-line-width 264,8994
(defun lego-shell-adjust-line-width 272,9301
(defun lego-mode-config 289,10002
(defun lego-equal-module-filename 357,12053
(defun lego-shell-compute-new-files-list 363,12328
(defun lego-shell-mode-config 373,12711
(defun lego-goals-mode-config 420,14378

lego/lego-syntax.el,599
(defconst lego-keywords-goal 15,307
(defconst lego-keywords-save 17,350
(defconst lego-commands19,421
(defconst lego-keywords31,979
(defconst lego-tacticals 36,1156
(defconst lego-error-regexp 39,1264
(defvar lego-id 42,1422
(defvar lego-ids 44,1449
(defconst lego-arg-list-regexp 48,1645
(defun lego-decl-defn-regexp 51,1761
(defconst lego-definiendum-alternative-regexp59,2133
(defvar lego-font-lock-terms63,2317
(defconst lego-goal-with-hole-regexp89,3170
(defconst lego-save-with-hole-regexp94,3392
(defvar lego-font-lock-keywords-199,3609
(defun lego-init-syntax-table 110,4071

phox/phox.el,554
(defcustom phox-prog-name 32,881
(defcustom phox-web-page37,983
(defcustom phox-doc-dir43,1133
(defcustom phox-lib-dir49,1280
(defcustom phox-tags-program55,1423
(defcustom phox-tags-doc61,1602
(defcustom phox-etags67,1739
(defpgdefault menu-entries88,2189
(defun phox-config 102,2382
(defun phox-shell-config 146,4308
(define-derived-mode phox-mode 170,5170
(define-derived-mode phox-shell-mode 186,5633
(define-derived-mode phox-response-mode 191,5761
(define-derived-mode phox-goals-mode 201,6122
(defpgdefault completion-table224,6908

phox/phox-extraction.el,383
(defvar phox-prog-orig 19,584
(defun phox-prog-flags-modify(21,652
(defun phox-prog-flags-extract(50,1453
(defun phox-prog-flags-erase(61,1743
(defun phox-toggle-extraction(69,1939
(defun phox-compile-theorem(81,2341
(defun phox-compile-theorem-on-cursor(87,2566
(defun phox-output 103,3044
(defun phox-output-theorem 113,3256
(defun phox-output-theorem-on-cursor(120,3555

phox/phox-font.el,231
(defvar phox-sym-lock-enabled 1,0
(defvar phox-sym-lock-color 2,60
(defvar phox-sym-lock-keywords 3,118
(defconst phox-font-lock-keywords11,511
(defconst phox-sym-lock-keywords-table70,2628
(defun phox-sym-lock-start 93,3202

phox/phox-fun.el,1658
(defconst phox-forget-id-command 11,151
(defconst phox-forget-proof-command 12,197
(defconst phox-forget-new-elim-command 13,252
(defconst phox-forget-new-intro-command 14,310
(defconst phox-forget-new-equation-command 15,370
(defconst phox-forget-close-def-command 16,436
(defconst phox-comments-regexp 18,562
(defconst phox-strict-comments-regexp 20,741
(defconst phox-ident-regexp 21,906
(defconst phox-inductive-option 22,992
(defconst phox-spaces-regexp 23,1044
(defconst phox-sy-definition-regexp 24,1087
(defconst phox-sy-inductive-regexp 28,1274
(defconst phox-inductive-regexp 34,1487
(defconst phox-data-regexp 40,1638
(defconst phox-definition-regexp 46,1792
(defconst phox-prove-claim-regexp 50,1936
(defconst phox-new-elim-regexp 54,2042
(defconst phox-new-intro-regexp 57,2161
(defconst phox-new-rewrite-regexp 60,2282
(defconst phox-new-equation-regexp 63,2407
(defconst phox-close-def-regexp 66,2534
(defun phox-init-syntax-table 71,2671
(defvar phox-top-keywords87,3143
(defvar phox-proof-keywords135,3598
(defun phox-find-and-forget 176,3948
(defalias 'phox-assert-next-command-interactive phox-assert-next-command-interactive
255,6364
(defun phox-depend-theorem(274,7330
(defun phox-eshow-extlist(283,7619
(defun phox-flag-name(297,8216
(defun phox-path(308,8518
(defun phox-print-expression(319,8754
(defun phox-print-sort-expression(332,9210
(defun phox-priority-symbols-list(343,9522
(defun phox-search-string(355,9894
(defun phox-constraints(370,10419
(defun phox-goals(381,10675
(defvar phox-state-menu393,10884
(defun phox-delete-symbol(418,11874
(defun phox-delete-symbol-on-cursor(424,12082

phox/phox-lang.el,323
(defvar phox-lang9,271
(defun phox-lang-absurd 17,500
(defun phox-lang-suppress 22,594
(defun phox-lang-opendef 27,791
(defun phox-lang-instance 32,909
(defun phox-lang-open-instance 37,1038
(defun phox-lang-lock 42,1187
(defun phox-lang-unlock 47,1317
(defun phox-lang-prove 52,1453
(defun phox-lang-let 57,1587

phox/phox-outline.el,254
(defconst phox-outline-title-regexp 19,723
(defconst phox-outline-section-regexp 20,788
(defconst phox-outline-save-regexp 21,844
(defconst phox-outline-heading-end-regexp 38,1387
(defun phox-outline-level(44,1562
(defun phox-setup-outline 58,2036

phox/phox-pbrpm.el,513
(defun phox-pbrpm-left-paren-p 39,1636
(defun phox-pbrpm-right-paren-p 46,1839
(defun phox-pbrpm-menu-from-string 54,2043
(defun phox-pbrpm-rename-in-cmd 63,2375
(defun phox-pbrpm-get-region-name 96,3623
(defun  phox-pbrpm-escape-string 99,3750
(defun phox-pbrpm-generate-menu 103,3885
(defalias 'proof-pbrpm-generate-menu proof-pbrpm-generate-menu
310,11365
(defalias 'proof-pbrpm-left-paren-p proof-pbrpm-left-paren-p
311,11429
(defalias 'proof-pbrpm-right-paren-p proof-pbrpm-right-paren-p
312,11491

phox/phox-sym-lock.el,1398
(defcustom phox-sym-lock-enabled 19,871
(defvar phox-sym-lock-sym-count 59,2452
(defvar phox-sym-lock-ext-start 62,2522
(defvar phox-sym-lock-ext-end 64,2644
(defvar phox-sym-lock-font-size 67,2763
(defvar phox-sym-lock-keywords 72,2953
(defvar phox-sym-lock-enabled 77,3129
(defvar phox-sym-lock-color 82,3291
(defvar phox-sym-lock-mouse-face 87,3509
(defvar phox-sym-lock-mouse-face-enabled 92,3699
(defconst phox-sym-lock-with-mule 97,3889
(defun phox-sym-lock-gen-symbol 100,3973
(defun phox-sym-lock-make-symbols-atomic 108,4275
(defun phox-sym-lock-compute-font-size 135,5216
(defvar phox-sym-lock-font-name173,6635
(defun phox-sym-lock-set-foreground 216,8233
(defun phox-sym-lock-translate-char 230,8842
(defun phox-sym-lock-translate-char-or-string 239,9159
(defun phox-sym-lock-remap-face 246,9387
(defvar phox-sym-lock-clear-face266,10375
(defun phox-sym-lock 278,10794
(defun phox-sym-lock-rec 287,11198
(defun phox-sym-lock-atom-face 293,11343
(defun phox-sym-lock-pre-idle-hook-first 298,11639
(defun phox-sym-lock-pre-idle-hook-last 308,12044
(defun phox-sym-lock-enable 317,12419
(defun phox-sym-lock-disable 330,12830
(defun phox-sym-lock-mouse-face-enable 343,13246
(defun phox-sym-lock-mouse-face-disable 350,13461
(defun phox-sym-lock-font-lock-hook 357,13680
(defun font-lock-set-defaults 372,14371
(defun phox-sym-lock-patch-keywords 384,14798

phox/phox-tags.el,305
(defun phox-tags-add-table(26,834
(defun phox-tags-reset-table(35,1229
(defun phox-tags-add-doc-table(40,1339
(defun phox-tags-add-lib-table(46,1488
(defun phox-tags-add-local-table(52,1623
(defun phox-tags-create-local-table(58,1806
(defun phox-complete-tag(69,2056
(defvar phox-tags-menu76,2165

generic/pg-assoc.el,81
(defun proof-associated-buffers 33,925
(defun proof-associated-windows 43,1135

generic/pg-autotest.el,908
(defvar pg-autotest-success 29,639
(defvar pg-autotest-log 32,726
(defun pg-autotest-find-file 37,820
(defun pg-autotest-find-file-restart 44,1086
(defmacro pg-autotest-apply 58,1560
(defmacro pg-autotest 72,1975
(defun pg-autotest-log 89,2412
(defun pg-autotest-message 98,2675
(defun pg-autotest-remark 107,2964
(defun pg-autotest-timestart 110,3045
(defun pg-autotest-timetaken 115,3228
(defun pg-autotest-start 129,3616
(defun pg-autotest-exit 140,4070
(defun pg-autotest-test-process-wholefile 160,4853
(defun pg-autotest-test-script-wholefile 168,5140
(defun pg-autotest-test-script-randomjumps 193,6072
(defun pg-autotest-test-retract-file 242,7629
(defun pg-autotest-test-assert-processed 248,7770
(defun pg-autotest-test-assert-full 254,7996
(defun pg-autotest-test-assert-unprocessed 261,8237
(defun pg-autotest-test-eval 268,8502
(defun pg-autotest-test-quit-prover 272,8601

generic/pg-custom.el,635
(defpgcustom script-indent 37,1150
(defconst proof-toolbar-entries-default42,1287
(defpgcustom toolbar-entries 71,3122
(defpgcustom prog-args 90,3855
(defpgcustom prog-env 102,4433
(defpgcustom quit-timeout 111,4862
(defpgcustom favourites 123,5289
(defpgcustom menu-entries 128,5478
(defpgcustom help-menu-entries 135,5714
(defpgcustom keymap 142,5977
(defpgcustom completion-table 147,6148
(defpgcustom tags-program 158,6524
(defpgcustom use-holes 167,6908
(defpgcustom one-command-per-line174,7166
(defpgcustom maths-menu-enable 185,7402
(defpgcustom unicode-tokens-enable 191,7582
(defpgcustom mmm-enable 197,7789

generic/pg-goals.el,285
(define-derived-mode proof-goals-mode 29,686
(define-key proof-goals-mode-map 56,1544
(define-key proof-goals-mode-map 58,1660
(define-key proof-goals-mode-map 59,1728
(defun proof-goals-config-done 68,1875
(defun pg-goals-display 76,2141
(defun pg-goals-button-action 117,3445

generic/pg-movie.el,333
(defconst pg-movie-xml-header 32,875
(defconst pg-movie-stylesheet34,933
(defun pg-movie-stylesheet-location 37,1032
(defvar pg-movie-frame 41,1140
(defun pg-movie-of-span 43,1194
(defun pg-movie-of-region 79,2314
(defun pg-movie-export 86,2502
(defun pg-movie-export-from 108,3106
(defun pg-movie-export-directory 119,3427

generic/pg-pamacs.el,534
(defmacro deflocal 35,1138
(deflocal proof-buffer-type 42,1376
(defmacro proof-ass-sym 50,1512
(defmacro proof-ass-symv 56,1771
(defmacro proof-ass 62,2029
(defun proof-ass-differs-from-default 68,2281
(defun proof-defpgcustom-fn 74,2536
(defun undefpgcustom 98,3420
(defmacro defpgcustom 104,3644
(defun proof-defpgdefault-fn 117,4294
(defmacro defpgdefault 131,4752
(defmacro defpgfun 142,5114
(defun proof-defpacustom-fn 156,5513
(defmacro defpacustom 223,7701
(defmacro proof-eval-when-ready-for-assistant 270,9510

generic/pg-pbrpm.el,1808
(defvar pg-pbrpm-use-buffer-menu 45,1159
(defvar pg-pbrpm-start-goal-regexp 48,1281
(defvar pg-pbrpm-start-goal-regexp-par-num 52,1438
(defvar pg-pbrpm-end-goal-regexp 55,1561
(defvar pg-pbrpm-start-hyp-regexp 59,1713
(defvar pg-pbrpm-start-hyp-regexp-par-num 63,1874
(defvar pg-pbrpm-start-concl-regexp 67,2081
(defvar pg-pbrpm-auto-select-regexp 71,2245
(defvar pg-pbrpm-buffer-menu 78,2406
(defvar pg-pbrpm-spans 79,2440
(defvar pg-pbrpm-goal-description 80,2468
(defvar pg-pbrpm-windows-dialog-bug 81,2507
(defvar pbrpm-menu-desc 82,2548
(defun pg-pbrpm-erase-buffer-menu 84,2578
(defun pg-pbrpm-menu-change-hook 90,2750
(defun pg-pbrpm-create-reset-buffer-menu 108,3325
(defun pg-pbrpm-analyse-goal-buffer 127,4167
(defun pg-pbrpm-button-action 187,6572
(defun pg-pbrpm-exists 194,6798
(defun pg-pbrpm-eliminate-id 198,6910
(defun pg-pbrpm-build-menu 206,7156
(defun pg-pbrpm-setup-span 269,9476
(defun pg-pbrpm-run-command 329,11775
(defun pg-pbrpm-get-pos-info 362,13300
(defun pg-pbrpm-get-region-info 404,14599
(defun pg-pbrpm-auto-select-around-point 415,15011
(defun pg-pbrpm-translate-position 430,15535
(defun pg-pbrpm-process-click 438,15789
(defvar pg-pbrpm-remember-region-selected-region 458,16814
(defvar pg-pbrpm-regions-list 459,16868
(defun pg-pbrpm-erase-regions-list 461,16904
(defun pg-pbrpm-filter-regions-list 470,17212
(defface pg-pbrpm-multiple-selection-face477,17475
(defface pg-pbrpm-menu-input-face485,17677
(defun pg-pbrpm-do-remember-region 493,17867
(defun pg-pbrpm-remember-region-drag-up-hook 514,18715
(defun pg-pbrpm-remember-region-click-hook 518,18886
(defun pg-pbrpm-remember-region 523,19071
(defun pg-pbrpm-process-region 537,19785
(defun pg-pbrpm-process-regions-list 555,20514
(defun pg-pbrpm-region-expression 559,20697

generic/pg-pgip.el,2931
(defalias 'pg-pgip-debug pg-pgip-debug
39,1044
(defalias 'pg-pgip-error pg-pgip-error
40,1085
(defalias 'pg-pgip-warning pg-pgip-warning
41,1120
(defconst pg-pgip-version-supported 43,1170
(defun pg-pgip-process-packet 47,1276
(defvar pg-pgip-last-seen-id 57,1844
(defvar pg-pgip-last-seen-seq 58,1878
(defun pg-pgip-process-pgip 60,1914
(defun pg-pgip-process-msg 79,2854
(defvar pg-pgip-post-process-functions94,3445
(defun pg-pgip-post-process 104,3920
(defun pg-pgip-process-askpgip 121,4535
(defun pg-pgip-process-usespgip 127,4739
(defun pg-pgip-process-usespgml 131,4903
(defun pg-pgip-process-pgmlconfig 135,5067
(defun pg-pgip-process-proverinfo 151,5684
(defun pg-pgip-process-hasprefs 168,6349
(defun pg-pgip-haspref 182,6981
(defun pg-pgip-process-prefval 200,7697
(defun pg-pgip-process-guiconfig 227,8405
(defvar proof-assistant-idtables 234,8522
(defun pg-pgip-process-ids 237,8639
(defun pg-complete-idtable-symbol 263,9711
(defalias 'pg-pgip-process-setids pg-pgip-process-setids
268,9803
(defalias 'pg-pgip-process-addids pg-pgip-process-addids
269,9859
(defalias 'pg-pgip-process-delids pg-pgip-process-delids
270,9915
(defun pg-pgip-process-idvalue 273,9973
(defun pg-pgip-process-menuadd 285,10319
(defun pg-pgip-process-menudel 288,10362
(defun pg-pgip-process-ready 297,10594
(defun pg-pgip-process-cleardisplay 300,10635
(defun pg-pgip-process-proofstate 314,11092
(defun pg-pgip-process-normalresponse 318,11169
(defun pg-pgip-process-errorresponse 322,11299
(defun pg-pgip-process-scriptinsert 326,11428
(defun pg-pgip-process-metainforesponse 331,11562
(defun pg-pgip-file-of-url 340,11802
(defun pg-pgip-process-informfileloaded 345,11937
(defun pg-pgip-process-informfileretracted 351,12169
(defun pg-pgip-process-brokerstatus 364,12616
(defun pg-pgip-process-proveravailmsg 367,12664
(defun pg-pgip-process-newprovermsg 370,12714
(defun pg-pgip-process-proverstatusmsg 373,12762
(defvar pg-pgip-srcids 382,13008
(defun pg-pgip-process-newfile 386,13115
(defun pg-pgip-process-filestatus 402,13697
(defun pg-pgip-process-newobj 422,14351
(defun pg-pgip-process-delobj 425,14393
(defun pg-pgip-process-objectstatus 428,14435
(defun pg-pgip-process-parsescript 442,14787
(defun pg-pgip-get-pgiptype 465,15661
(defun pg-pgip-default-for 486,16524
(defun pg-pgip-subst-for 499,16919
(defun pg-pgip-interpret-value 512,17289
(defun pg-pgip-interpret-choice 531,18014
(defun pg-pgip-string-of-command 562,19031
(defconst pg-pgip-id579,19792
(defvar pg-pgip-refseq 585,20072
(defvar pg-pgip-refid 587,20169
(defvar pg-pgip-seq 590,20261
(defun pg-pgip-assemble-packet 592,20325
(defun pg-pgip-issue 610,21136
(defun pg-pgip-maybe-askpgip 627,21748
(defun pg-pgip-askprefs 633,21939
(defun pg-pgip-askids 637,22053
(defun pg-pgip-reset 650,22341
(defconst pg-pgip-start-element-regexp 681,23039
(defconst pg-pgip-end-element-regexp 682,23091

generic/pg-response.el,1251
(deflocal pg-response-eagerly-raise 32,737
(define-derived-mode proof-response-mode 42,962
(define-key proof-response-mode-map 69,1899
(define-key proof-response-mode-map 70,1970
(define-key proof-response-mode-map 71,2024
(defun proof-response-config-done 75,2110
(defvar pg-response-special-display-regexp 86,2456
(defconst proof-multiframe-parameters90,2623
(defun proof-multiple-frames-enable 99,2913
(defun proof-three-window-enable 109,3241
(defun proof-select-three-b 112,3304
(defun proof-display-three-b 127,3795
(defvar pg-frame-configuration 138,4185
(defun pg-cache-frame-configuration 142,4332
(defun proof-layout-windows 146,4503
(defun proof-delete-other-frames 186,6290
(defvar pg-response-erase-flag 217,7378
(defun pg-response-maybe-erase221,7507
(defun pg-response-display 251,8611
(defun pg-response-display-with-face 276,9394
(defun pg-response-clear-displays 304,10240
(defun pg-response-message 322,10946
(defun pg-response-warning 328,11181
(defun proof-next-error 343,11587
(defun pg-response-has-error-location 421,14396
(defcustom proof-trace-buffer-max-lines 436,14815
(defun proof-trace-buffer-display 443,15050
(defun proof-trace-buffer-finish 457,15457
(defun pg-thms-buffer-clear 481,16110

generic/pg-user.el,3635
(defun proof-script-new-command-advance 43,1185
(defun proof-maybe-follow-locked-end 67,2110
(defun proof-goto-command-start 93,2946
(defun proof-goto-command-end 116,3893
(defun proof-forward-command 131,4315
(defun proof-backward-command 152,5036
(defun proof-goto-point 163,5250
(defun proof-assert-next-command-interactive 177,5684
(defun proof-assert-until-point-interactive 189,6170
(defun proof-process-buffer 196,6415
(defun proof-undo-last-successful-command 214,6927
(defun proof-undo-and-delete-last-successful-command 219,7089
(defun proof-undo-last-successful-command-1 231,7608
(defun proof-retract-buffer 248,8272
(defun proof-retract-current-goal 257,8556
(defun proof-mouse-goto-point 276,9076
(defvar proof-minibuffer-history 291,9352
(defun proof-minibuffer-cmd 294,9447
(defun proof-frob-locked-end 333,10854
(defmacro proof-if-setting-configured 369,11955
(defmacro proof-define-assistant-command 377,12224
(defmacro proof-define-assistant-command-witharg 390,12679
(defun proof-issue-new-command 410,13501
(defun proof-cd-sync 450,14724
(defun proof-electric-terminator-enable 501,16323
(defun proof-electric-terminator 509,16627
(defun proof-add-completions 537,17597
(defun proof-script-complete 560,18420
(defun pg-copy-span-contents 574,18729
(defun pg-numth-span-higher-or-lower 588,19153
(defun pg-control-span-of 614,19899
(defun pg-move-span-contents 620,20103
(defun pg-fixup-children-spans 671,22221
(defun pg-move-region-down 681,22478
(defun pg-move-region-up 690,22771
(defun pg-pos-for-event 704,23045
(defun pg-span-for-event 710,23266
(defun pg-span-context-menu 714,23410
(defun pg-toggle-visibility 730,23927
(defun pg-create-in-span-context-menu 739,24234
(defun pg-span-undo 764,25262
(defun pg-goals-buffers-hint 777,25500
(defun pg-slow-fontify-tracing-hint 781,25718
(defun pg-response-buffers-hint 785,25907
(defun pg-jump-to-end-hint 797,26322
(defun pg-processing-complete-hint 801,26451
(defun pg-next-error-hint 818,27171
(defun pg-hint 823,27323
(defun pg-identifier-under-mouse-query 834,27672
(defun pg-identifier-near-point-query 845,27996
(defvar proof-query-identifier-history 874,28919
(defun proof-query-identifier 877,29006
(defun pg-identifier-query 888,29362
(defun proof-imenu-enable 921,30510
(defvar pg-input-ring 957,31813
(defvar pg-input-ring-index 960,31870
(defvar pg-stored-incomplete-input 963,31942
(defun pg-previous-input 966,32045
(defun pg-next-input 980,32508
(defun pg-delete-input 985,32630
(defun pg-get-old-input 998,32968
(defun pg-restore-input 1012,33359
(defun pg-search-start 1023,33649
(defun pg-regexp-arg 1035,34141
(defun pg-search-arg 1047,34589
(defun pg-previous-matching-input-string-position 1061,35006
(defun pg-previous-matching-input 1088,36171
(defun pg-next-matching-input 1107,37021
(defvar pg-matching-input-from-input-string 1115,37404
(defun pg-previous-matching-input-from-input 1119,37518
(defun pg-next-matching-input-from-input 1137,38283
(defun pg-add-to-input-history 1148,38662
(defun pg-remove-from-input-history 1160,39115
(defun  pg-clear-input-ring 1171,39495
(define-key proof-mode-map 1188,39965
(define-key proof-mode-map 1189,40025
(defun pg-protected-undo 1191,40097
(defun pg-protected-undo-1 1221,41391
(defun next-undo-elt 1252,42828
(defvar proof-autosend-timer 1279,43784
(deflocal proof-autosend-modified-tick 1281,43845
(defun proof-autosend-enable 1285,43967
(defun proof-autosend-delay 1299,44510
(defun proof-autosend-loop 1303,44643
(defun proof-autosend-loop-all 1317,45203
(defun proof-autosend-loop-next 1341,45983

generic/pg-vars.el,1500
(defvar proof-assistant-cusgrp 22,341
(defvar proof-assistant-internals-cusgrp 28,601
(defvar proof-assistant 34,871
(defvar proof-assistant-symbol 39,1094
(defvar proof-mode-for-shell 52,1636
(defvar proof-mode-for-response 57,1826
(defvar proof-mode-for-goals 62,2052
(defvar proof-mode-for-script 67,2241
(defvar proof-ready-for-assistant-hook 72,2418
(defvar proof-shell-busy 83,2706
(defvar proof-shell-last-queuemode 101,3377
(defvar proof-included-files-list 105,3532
(defvar proof-script-buffer 127,4551
(defvar proof-previous-script-buffer 130,4643
(defvar proof-shell-buffer 134,4816
(defvar proof-goals-buffer 137,4902
(defvar proof-response-buffer 140,4957
(defvar proof-trace-buffer 143,5018
(defvar proof-thms-buffer 147,5172
(defvar proof-shell-error-or-interrupt-seen 151,5327
(defvar pg-response-next-error 156,5551
(defvar proof-shell-proof-completed 159,5658
(defvar proof-shell-silent 173,6043
(defvar proof-shell-last-prompt 176,6131
(defvar proof-shell-last-output 180,6301
(defvar proof-shell-last-output-kind 184,6441
(defvar proof-assistant-settings 204,7205
(defvar pg-tracing-slow-mode 214,7719
(defvar proof-nesting-depth 217,7808
(defvar proof-last-theorem-dependencies 224,8043
(defvar proof-autosend-running 228,8205
(defvar proof-next-command-on-new-line 233,8404
(defcustom proof-general-name 244,8638
(defcustom proof-general-home-page249,8795
(defcustom proof-unnamed-theorem-name255,8955
(defcustom proof-universal-keys261,9139

generic/pg-xml.el,1176
(defalias 'pg-xml-error pg-xml-error
18,335
(defun pg-xml-parse-string 41,977
(defun pg-xml-parse-buffer 51,1289
(defun pg-xml-get-attr 70,1904
(defun pg-xml-child-elts 78,2206
(defun pg-xml-child-elt 83,2411
(defun pg-xml-get-child 91,2693
(defun pg-xml-get-text-content 101,3060
(defmacro pg-xml-attr 112,3410
(defmacro pg-xml-node 114,3472
(defconst pg-xml-header117,3564
(defun pg-xml-string-of 121,3640
(defun pg-xml-output-internal 132,4007
(defun pg-xml-cdata 166,5146
(defsubst pg-pgip-get-area 174,5339
(defun pg-pgip-get-icon 177,5456
(defsubst pg-pgip-get-name 181,5604
(defsubst pg-pgip-get-version 184,5721
(defsubst pg-pgip-get-descr 187,5844
(defsubst pg-pgip-get-thmname 190,5963
(defsubst pg-pgip-get-thyname 193,6086
(defsubst pg-pgip-get-url 196,6209
(defsubst pg-pgip-get-srcid 199,6324
(defsubst pg-pgip-get-proverid 202,6443
(defsubst pg-pgip-get-symname 205,6568
(defsubst pg-pgip-get-prefcat 208,6688
(defsubst pg-pgip-get-default 211,6816
(defsubst pg-pgip-get-objtype 214,6939
(defsubst pg-pgip-get-value 217,7062
(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext
220,7132
(defun pg-pgip-get-pgmltext 222,7191

generic/proof-autoloads.el,97
(defsubst proof-shell-live-buffer 727,23601
(defsubst proof-replace-regexp-in-string 883,29162

generic/proof-auxmodes.el,149
(defun proof-mmm-support-available 20,495
(defun proof-maths-menu-support-available 44,1114
(defun proof-unicode-tokens-support-available 58,1531

generic/proof-config.el,7845
(defgroup prover-config 80,2580
(defcustom proof-guess-command-line 98,3430
(defcustom proof-assistant-home-page 113,3925
(defcustom proof-context-command 119,4095
(defcustom proof-info-command 124,4229
(defcustom proof-showproof-command 131,4500
(defcustom proof-goal-command 136,4636
(defcustom proof-save-command 144,4933
(defcustom proof-find-theorems-command 152,5242
(defcustom proof-query-identifier-command 159,5550
(defcustom proof-assistant-true-value 173,6239
(defcustom proof-assistant-false-value 179,6429
(defcustom proof-assistant-format-int-fn 185,6623
(defcustom proof-assistant-format-float-fn 192,6872
(defcustom proof-assistant-format-string-fn 199,7127
(defcustom proof-assistant-setting-format 206,7394
(defcustom proof-tree-configured 216,7877
(defgroup proof-script 234,8343
(defcustom proof-terminal-string 239,8473
(defcustom proof-electric-terminator-noterminator 249,8861
(defcustom proof-script-sexp-commands 254,9033
(defcustom proof-script-command-end-regexp 265,9492
(defcustom proof-script-command-start-regexp 283,10313
(defcustom proof-script-integral-proofs 294,10776
(defcustom proof-script-fly-past-comments 309,11432
(defcustom proof-script-parse-function 314,11603
(defcustom proof-script-comment-start 332,12248
(defcustom proof-script-comment-start-regexp 343,12685
(defcustom proof-script-comment-end 351,13004
(defcustom proof-script-comment-end-regexp 363,13426
(defcustom proof-string-start-regexp 371,13739
(defcustom proof-string-end-regexp 376,13904
(defcustom proof-case-fold-search 381,14065
(defcustom proof-save-command-regexp 390,14477
(defcustom proof-save-with-hole-regexp 395,14587
(defcustom proof-save-with-hole-result 406,14962
(defcustom proof-goal-command-regexp 416,15406
(defcustom proof-goal-with-hole-regexp 424,15693
(defcustom proof-goal-with-hole-result 436,16136
(defcustom proof-non-undoables-regexp 445,16514
(defcustom proof-nested-undo-regexp 456,16977
(defcustom proof-ignore-for-undo-count 472,17697
(defcustom proof-script-imenu-generic-expression 480,18008
(defcustom proof-goal-command-p 488,18347
(defcustom proof-really-save-command-p 499,18838
(defcustom proof-completed-proof-behaviour 508,19145
(defcustom proof-count-undos-fn 536,20494
(defcustom proof-find-and-forget-fn 548,21045
(defcustom proof-forget-id-command 565,21754
(defcustom pg-topterm-goalhyplit-fn 575,22112
(defcustom proof-kill-goal-command 587,22655
(defcustom proof-undo-n-times-cmd 601,23159
(defcustom proof-nested-goals-history-p 615,23696
(defcustom proof-arbitrary-undo-positions 624,24033
(defcustom proof-state-preserving-p 638,24614
(defcustom proof-activate-scripting-hook 648,25086
(defcustom proof-deactivate-scripting-hook 667,25867
(defcustom proof-no-fully-processed-buffer 676,26197
(defcustom proof-script-evaluate-elisp-comment-regexp 687,26695
(defcustom proof-indent 705,27281
(defcustom proof-indent-hang 710,27388
(defcustom proof-indent-enclose-offset 715,27514
(defcustom proof-indent-open-offset 720,27656
(defcustom proof-indent-close-offset 725,27793
(defcustom proof-indent-any-regexp 730,27931
(defcustom proof-indent-inner-regexp 735,28091
(defcustom proof-indent-enclose-regexp 740,28245
(defcustom proof-indent-open-regexp 745,28399
(defcustom proof-indent-close-regexp 750,28551
(defcustom proof-script-font-lock-keywords 756,28705
(defcustom proof-script-syntax-table-entries 764,29057
(defcustom proof-script-span-context-menu-extensions 782,29453
(defgroup proof-shell 808,30213
(defcustom proof-prog-name 818,30383
(defcustom proof-shell-auto-terminate-commands 830,30850
(defcustom proof-shell-pre-sync-init-cmd 839,31255
(defcustom proof-shell-init-cmd 853,31813
(defcustom proof-shell-init-hook 865,32359
(defcustom proof-shell-restart-cmd 870,32498
(defcustom proof-shell-quit-cmd 875,32653
(defcustom proof-shell-cd-cmd 880,32820
(defcustom proof-shell-start-silent-cmd 897,33491
(defcustom proof-shell-stop-silent-cmd 906,33867
(defcustom proof-shell-silent-threshold 915,34202
(defcustom  proof-shell-inform-file-processed-cmd 923,34536
(defcustom  proof-shell-inform-file-retracted-cmd 944,35464
(defcustom proof-auto-multiple-files 972,36736
(defcustom proof-cannot-reopen-processed-files 987,37457
(defcustom proof-shell-annotated-prompt-regexp 1007,38248
(defcustom proof-shell-error-regexp 1022,38813
(defcustom proof-shell-truncate-before-error 1042,39623
(defcustom pg-next-error-regexp 1056,40162
(defcustom pg-next-error-filename-regexp 1071,40771
(defcustom pg-next-error-extract-filename 1095,41804
(defcustom proof-shell-interrupt-regexp 1102,42047
(defcustom proof-shell-proof-completed-regexp 1116,42650
(defcustom proof-shell-clear-response-regexp 1129,43166
(defcustom proof-shell-clear-goals-regexp 1141,43626
(defcustom proof-shell-start-goals-regexp 1153,44080
(defcustom proof-shell-end-goals-regexp 1162,44512
(defcustom proof-shell-eager-annotation-start 1176,45093
(defcustom proof-shell-eager-annotation-start-length 1199,46112
(defcustom proof-shell-eager-annotation-end 1210,46538
(defcustom proof-shell-strip-output-markup 1226,47213
(defcustom proof-shell-assumption-regexp 1235,47598
(defcustom proof-shell-process-file 1245,48002
(defcustom proof-shell-retract-files-regexp 1271,49078
(defcustom proof-shell-compute-new-files-list 1284,49566
(defcustom pg-special-char-regexp 1299,50133
(defcustom proof-shell-set-elisp-variable-regexp 1304,50277
(defcustom proof-shell-match-pgip-cmd 1342,51951
(defcustom proof-shell-issue-pgip-cmd 1356,52441
(defcustom proof-use-pgip-askprefs 1361,52614
(defcustom proof-shell-query-dependencies-cmd 1369,52961
(defcustom proof-shell-theorem-dependency-list-regexp 1376,53221
(defcustom proof-shell-theorem-dependency-list-split 1392,53889
(defcustom proof-shell-show-dependency-cmd 1401,54320
(defcustom proof-shell-trace-output-regexp 1423,55226
(defcustom proof-shell-thms-output-regexp 1441,55828
(defcustom proof-shell-interactive-prompt-regexp 1449,56162
(defcustom proof-tokens-activate-command 1468,56815
(defcustom proof-tokens-deactivate-command 1475,57055
(defcustom proof-tokens-extra-modes 1482,57300
(defcustom proof-shell-unicode 1497,57805
(defcustom proof-shell-filename-escapes 1506,58195
(defcustom proof-shell-process-connection-type 1523,58875
(defcustom proof-shell-strip-crs-from-input 1529,59066
(defcustom proof-shell-strip-crs-from-output 1541,59549
(defcustom proof-shell-extend-queue-hook 1549,59917
(defcustom proof-shell-insert-hook 1559,60347
(defcustom proof-script-preprocess 1602,62445
(defcustom proof-shell-handle-delayed-output-hook1608,62596
(defcustom proof-shell-handle-error-or-interrupt-hook1614,62811
(defcustom proof-shell-pre-interrupt-hook1632,63557
(defcustom proof-shell-handle-output-system-specific 1640,63828
(defcustom proof-state-change-hook 1663,64801
(defcustom proof-shell-syntax-table-entries 1673,65194
(defgroup proof-goals 1691,65565
(defcustom pg-subterm-first-special-char 1696,65686
(defcustom pg-subterm-anns-use-stack 1704,65998
(defcustom pg-goals-change-goal 1713,66297
(defcustom pbp-goal-command 1718,66413
(defcustom pbp-hyp-command 1723,66577
(defcustom pg-subterm-help-cmd 1728,66747
(defcustom pg-goals-error-regexp 1735,66991
(defcustom proof-shell-result-start 1740,67159
(defcustom proof-shell-result-end 1746,67401
(defcustom pg-subterm-start-char 1752,67614
(defcustom pg-subterm-sep-char 1763,68088
(defcustom pg-subterm-end-char 1769,68267
(defcustom pg-topterm-regexp 1775,68424
(defcustom proof-goals-font-lock-keywords 1790,69024
(defcustom proof-response-font-lock-keywords 1798,69383
(defcustom proof-shell-font-lock-keywords 1806,69745
(defcustom pg-before-fontify-output-hook 1817,70259
(defcustom pg-after-fontify-output-hook 1825,70620

generic/proof-depends.el,917
(defvar proof-thm-names-of-files 25,586
(defvar proof-def-names-of-files 31,870
(defun proof-depends-module-name-for-buffer 42,1185
(defun proof-depends-module-of 52,1626
(defun proof-depends-names-in-same-file 60,1917
(defun proof-depends-process-dependencies 79,2525
(defun proof-dependency-in-span-context-menu 132,4260
(defun proof-dep-alldeps-menu 155,5150
(defun proof-dep-make-alldeps-menu 161,5376
(defun proof-dep-split-deps 179,5871
(defun proof-dep-make-submenu 198,6537
(defun proof-make-highlight-depts-menu 209,6948
(defun proof-goto-dependency 220,7256
(defun proof-show-dependency 227,7508
(defconst pg-dep-span-priority 234,7797
(defconst pg-ordinary-span-priority 235,7833
(defun proof-highlight-depcs 237,7875
(defun proof-highlight-depts 248,8341
(defun proof-depends-save-old-face 260,8851
(defun proof-depends-restore-old-face 265,9028
(defun proof-dep-unhighlight 271,9257

generic/proof-easy-config.el,192
(defconst proof-easy-config-derived-modes-table16,487
(defun proof-easy-config-define-derived-modes 23,893
(defun proof-easy-config-check-setup 52,2078
(defmacro proof-easy-config 84,3408

generic/proof-faces.el,1809
(defgroup proof-faces 29,758
(defconst pg-defface-window-systems36,938
(defmacro proof-face-specs 49,1500
(defface proof-queue-face64,1952
(defface proof-locked-face72,2230
(defface proof-declaration-name-face82,2551
(defface proof-tacticals-name-face91,2837
(defface proof-tactics-name-face100,3099
(defface proof-error-face109,3364
(defface proof-warning-face117,3585
(defface proof-eager-annotation-face126,3842
(defface proof-debug-message-face134,4060
(defface proof-boring-face142,4259
(defface proof-mouse-highlight-face150,4451
(defface proof-command-mouse-highlight-face158,4669
(defface proof-region-mouse-highlight-face166,4908
(defface proof-highlight-dependent-face174,5150
(defface proof-highlight-dependency-face182,5357
(defface proof-active-area-face190,5554
(defface proof-script-sticky-error-face198,5866
(defface proof-script-highlight-error-face206,6095
(defconst proof-face-compat-doc 218,6440
(defconst proof-queue-face 219,6520
(defconst proof-locked-face 220,6588
(defconst proof-declaration-name-face 221,6658
(defconst proof-tacticals-name-face 222,6748
(defconst proof-tactics-name-face 223,6834
(defconst proof-error-face 224,6916
(defconst proof-script-sticky-error-face 225,6984
(defconst proof-script-highlight-error-face 226,7080
(defconst proof-warning-face 227,7182
(defconst proof-eager-annotation-face 228,7254
(defconst proof-debug-message-face 229,7344
(defconst proof-boring-face 230,7428
(defconst proof-mouse-highlight-face 231,7498
(defconst proof-command-mouse-highlight-face 232,7586
(defconst proof-region-mouse-highlight-face 233,7690
(defconst proof-highlight-dependent-face 234,7792
(defconst proof-highlight-dependency-face 235,7888
(defconst proof-active-area-face 236,7986
(defconst proof-script-error-face 237,8066

generic/proof-indent.el,219
(defun proof-indent-indent 19,397
(defun proof-indent-offset 28,663
(defun proof-indent-inner-p 45,1264
(defun proof-indent-goto-prev 54,1564
(defun proof-indent-calculate 61,1897
(defun proof-indent-line 82,2656

generic/proof-maths-menu.el,83
(defun proof-maths-menu-set-global 32,850
(defun proof-maths-menu-enable 46,1301

generic/proof-menu.el,2215
(defvar proof-display-some-buffers-count 36,770
(defun proof-display-some-buffers 38,815
(defun proof-menu-define-keys 95,2956
(defun proof-menu-define-main 154,5862
(defvar proof-menu-favourites 163,6047
(defvar proof-menu-settings 166,6154
(defun proof-menu-define-specific 170,6243
(defun proof-assistant-menu-update 213,7505
(defvar proof-help-menu227,7938
(defvar proof-show-hide-menu235,8202
(defvar proof-buffer-menu246,8626
(defun proof-keep-response-history 310,10982
(defconst proof-quick-opts-menu318,11292
(defun proof-quick-opts-vars 540,20359
(defun proof-quick-opts-changed-from-defaults-p 572,21299
(defun proof-quick-opts-changed-from-saved-p 576,21404
(defun proof-set-document-centred 584,21560
(defun proof-set-non-document-centred 597,21986
(defun proof-quick-opts-save 616,22697
(defun proof-quick-opts-reset 621,22865
(defconst proof-config-menu633,23133
(defconst proof-advanced-menu640,23312
(defvar proof-menu658,23996
(defun proof-main-menu 667,24278
(defun proof-aux-menu 679,24617
(defun proof-menu-define-favourites-menu 695,24963
(defun proof-def-favourite 715,25612
(defvar proof-make-favourite-cmd-history 742,26605
(defvar proof-make-favourite-menu-history 745,26690
(defun proof-save-favourites 748,26776
(defun proof-del-favourite 753,26924
(defun proof-read-favourite 770,27480
(defun proof-add-favourite 794,28254
(defun proof-menu-define-settings-menu 821,29299
(defun proof-menu-entry-name 850,30291
(defun proof-menu-entry-for-setting 860,30641
(defun proof-settings-vars 883,31279
(defun proof-settings-changed-from-defaults-p 888,31456
(defun proof-settings-changed-from-saved-p 892,31562
(defun proof-settings-save 896,31665
(defun proof-settings-reset 901,31832
(defun proof-assistant-invisible-command-ifposs 906,31995
(defun proof-maybe-askprefs 928,32965
(defun proof-assistant-settings-cmd 944,33582
(defun proof-assistant-settings-cmds 952,33865
(defvar proof-assistant-format-table967,34307
(defun proof-assistant-format-bool 976,34733
(defun proof-assistant-format-int 979,34846
(defun proof-assistant-format-float 982,34938
(defun proof-assistant-format-string 985,35034
(defun proof-assistant-format 988,35132

generic/proof-mmm.el,70
(defun proof-mmm-set-global 43,1390
(defun proof-mmm-enable 58,1929

generic/proof-script.el,5813
(deflocal proof-active-buffer-fake-minor-mode 46,1361
(deflocal proof-script-buffer-file-name 49,1487
(deflocal pg-script-portions 56,1897
(defalias 'proof-active-buffer-fake-minor-modeproof-active-buffer-fake-minor-mode
59,2003
(defun proof-next-element-count 68,2198
(defun proof-element-id 74,2440
(defun proof-next-element-id 78,2609
(deflocal proof-locked-span 114,3913
(deflocal proof-queue-span 121,4179
(deflocal proof-overlay-arrow 130,4665
(defun proof-span-give-warning 136,4792
(defun proof-span-read-only 142,4972
(defun proof-strict-read-only 151,5345
(defsubst proof-set-queue-endpoints 161,5723
(defun proof-set-overlay-arrow 165,5864
(defsubst proof-set-locked-endpoints 176,6202
(defsubst proof-detach-queue 181,6378
(defsubst proof-detach-locked 186,6517
(defsubst proof-set-queue-start 193,6742
(defsubst proof-set-locked-end 197,6868
(defsubst proof-set-queue-end 209,7338
(defun proof-init-segmentation 220,7635
(defun proof-colour-locked 250,8886
(defun proof-colour-locked-span 257,9159
(defun proof-sticky-errors 263,9432
(defun proof-restart-buffers 276,9848
(defun proof-script-buffers-with-spans 300,10781
(defun proof-script-remove-all-spans-and-deactivate 310,11137
(defun proof-script-clear-queue-spans-on-error 314,11327
(defun proof-script-delete-spans 340,12344
(defun proof-script-delete-secondary-spans 345,12543
(defun proof-unprocessed-begin 358,12832
(defun proof-script-end 366,13086
(defun proof-queue-or-locked-end 375,13396
(defun proof-locked-region-full-p 394,13989
(defun proof-locked-region-empty-p 403,14261
(defun proof-only-whitespace-to-locked-region-p 407,14411
(defun proof-in-locked-region-p 417,14760
(defun proof-goto-end-of-locked 429,15017
(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 446,15804
(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 457,16285
(defun proof-end-of-locked-visible-p 469,16825
(defconst pg-idioms 488,17418
(defconst pg-all-idioms 491,17514
(defun pg-clear-script-portions 495,17635
(defun pg-remove-element 501,17870
(defun pg-get-element 509,18173
(defun pg-add-element 519,18488
(defun pg-invisible-prop 567,20450
(defun pg-set-element-span-invisible 572,20651
(defun pg-toggle-element-span-visibility 585,21217
(defun pg-open-invisible-span 590,21378
(defun pg-make-element-invisible 595,21549
(defun pg-make-element-visible 600,21760
(defun pg-toggle-element-visibility 605,21954
(defun pg-show-all-portions 611,22217
(defun pg-show-all-proofs 633,22961
(defun pg-hide-all-proofs 638,23089
(defun pg-add-proof-element 643,23220
(defun pg-span-name 658,24007
(defvar pg-span-context-menu-keymap691,25214
(defun pg-last-output-displayform 698,25452
(defun pg-set-span-helphighlights 721,26343
(defun proof-complete-buffer-atomic 784,28490
(defun proof-register-possibly-new-processed-file813,29760
(defun proof-query-save-this-buffer-p 859,31634
(defun proof-inform-prover-file-retracted 864,31859
(defun proof-auto-retract-dependencies 884,32710
(defun proof-unregister-buffer-file-name 938,35260
(defsubst proof-action-completed 984,37085
(defun proof-protected-process-or-retract 988,37255
(defun proof-deactivate-scripting-auto 1016,38486
(defun proof-deactivate-scripting-query-user-action 1025,38844
(defun proof-deactivate-scripting-choose-action 1069,40353
(defun proof-deactivate-scripting 1081,40738
(defun proof-activate-scripting 1178,44861
(defun proof-toggle-active-scripting 1278,49400
(defun proof-done-advancing 1317,50645
(defun proof-done-advancing-comment 1385,53142
(defun proof-done-advancing-save 1419,54528
(defun proof-make-goalsave1507,57892
(defun proof-get-name-from-goal 1525,58757
(defun proof-done-advancing-autosave 1545,59782
(defun proof-done-advancing-other 1609,62278
(defun proof-segment-up-to-parser 1638,63242
(defun proof-script-generic-parse-find-comment-end 1708,65523
(defun proof-script-generic-parse-cmdend 1717,65937
(defun proof-script-generic-parse-cmdstart 1768,67833
(defun proof-script-generic-parse-sexp 1807,69433
(defun proof-semis-to-vanillas 1819,69899
(defun proof-next-command-new-line 1872,71572
(defun proof-script-next-command-advance 1877,71778
(defun proof-assert-until-point 1896,72278
(defun proof-assert-electric-terminator 1912,72949
(defun proof-assert-semis 1956,74629
(defun proof-retract-before-change 1970,75390
(defun proof-insert-pbp-command 1993,76046
(defun proof-insert-sendback-command 2008,76549
(defun proof-done-retracting 2034,77452
(defun proof-setup-retract-action 2069,78906
(defun proof-last-goal-or-goalsave 2081,79511
(defun proof-retract-target 2105,80423
(defun proof-retract-until-point-interactive 2184,83676
(defun proof-retract-until-point 2193,84083
(define-derived-mode proof-mode 2248,86088
(defun proof-script-set-visited-file-name 2284,87470
(defun proof-script-set-buffer-hooks 2306,88483
(defun proof-script-kill-buffer-fn 2314,88901
(defun proof-config-done-related 2346,90218
(defun proof-generic-goal-command-p 2411,92703
(defun proof-generic-state-preserving-p 2416,92916
(defun proof-generic-count-undos 2425,93433
(defun proof-generic-find-and-forget 2456,94561
(defconst proof-script-important-settings2507,96333
(defun proof-config-done 2522,96879
(defun proof-setup-parsing-mechanism 2589,99044
(defun proof-setup-imenu 2613,100116
(deflocal proof-segment-up-to-cache 2650,101398
(deflocal proof-segment-up-to-cache-start 2654,101541
(deflocal proof-segment-up-to-cache-end 2655,101586
(deflocal proof-last-edited-low-watermark 2656,101629
(defun proof-segment-up-to-using-cache 2658,101677
(defun proof-segment-cache-contents-for 2686,102797
(defun proof-script-after-change-function 2703,103379
(defun proof-script-set-after-change-functions 2715,103886

generic/proof-shell.el,3766
(defvar proof-marker 35,721
(defvar proof-action-list 38,817
(defsubst proof-shell-invoke-callback 80,2530
(defvar proof-shell-last-goals-output 94,3022
(defvar proof-shell-last-response-output 97,3102
(defvar proof-shell-delayed-output-start 100,3189
(defvar proof-shell-delayed-output-end 104,3371
(defvar proof-shell-delayed-output-flags 108,3551
(defvar proof-shell-interrupt-pending 111,3676
(defvar proof-shell-exit-in-progress 116,3900
(defcustom proof-shell-active-scripting-indicator128,4245
(defun proof-shell-ready-prover 180,5829
(defsubst proof-shell-live-buffer 194,6368
(defun proof-shell-available-p 201,6588
(defun proof-grab-lock 207,6810
(defun proof-release-lock 217,7239
(defcustom proof-shell-fiddle-frames 227,7413
(defun proof-shell-set-text-representation 232,7571
(defun proof-shell-start 240,7899
(defvar proof-shell-kill-function-hooks 419,13993
(defun proof-shell-kill-function 422,14091
(defun proof-shell-clear-state 485,16293
(defun proof-shell-exit 501,16768
(defun proof-shell-bail-out 525,17702
(defun proof-shell-restart 535,18224
(defvar proof-shell-urgent-message-marker 576,19596
(defvar proof-shell-urgent-message-scanner 579,19717
(defun proof-shell-handle-error-output 583,19902
(defun proof-shell-handle-error-or-interrupt 609,20764
(defun proof-shell-error-or-interrupt-action 652,22513
(defun proof-goals-pos 679,23610
(defun proof-pbp-focus-on-first-goal 684,23821
(defsubst proof-shell-string-match-safe 696,24237
(defun proof-shell-handle-immediate-output 700,24398
(defun proof-interrupt-process 767,27005
(defun proof-shell-insert 801,28238
(defun proof-shell-action-list-item 858,30220
(defun proof-shell-set-silent 863,30462
(defun proof-shell-start-silent-item 869,30681
(defun proof-shell-clear-silent 875,30870
(defun proof-shell-stop-silent-item 881,31092
(defsubst proof-shell-should-be-silent 887,31281
(defsubst proof-shell-insert-action-item 899,31854
(defsubst proof-shell-slurp-comments 903,32029
(defun proof-add-to-queue 914,32434
(defun proof-start-queue 966,34386
(defun proof-extend-queue 978,34781
(defun proof-shell-exec-loop 997,35400
(defun proof-shell-insert-loopback-cmd 1079,38340
(defun proof-shell-process-urgent-message 1104,39504
(defun proof-shell-process-urgent-message-default 1160,41529
(defun proof-shell-process-urgent-message-trace 1176,42113
(defun proof-shell-process-urgent-message-retract 1188,42636
(defun proof-shell-process-urgent-message-elisp 1214,43766
(defun proof-shell-process-urgent-message-thmdeps 1229,44261
(defun proof-shell-process-interactive-prompt-regexp 1239,44605
(defun proof-shell-strip-eager-annotations 1251,44961
(defun proof-shell-filter 1267,45461
(defun proof-shell-filter-first-command 1367,48833
(defun proof-shell-process-urgent-messages 1382,49376
(defun proof-shell-filter-manage-output 1432,50942
(defsubst proof-shell-display-output-as-response 1468,52365
(defun proof-shell-handle-delayed-output 1474,52660
(defvar pg-last-tracing-output-time 1562,55835
(defvar pg-last-trace-output-count 1565,55948
(defconst pg-slow-mode-trigger-count 1568,56033
(defconst pg-slow-mode-duration 1571,56138
(defconst pg-fast-tracing-mode-threshold 1574,56220
(defun pg-tracing-tight-loop 1577,56349
(defun pg-finish-tracing-display 1601,57381
(defun proof-shell-wait 1619,57762
(defun proof-done-invisible 1649,58973
(defun proof-shell-invisible-command 1655,59143
(defun proof-shell-invisible-cmd-get-result 1702,60735
(defun proof-shell-invisible-command-invisible-result 1714,61171
(defun pg-insert-last-output-as-comment 1734,61672
(define-derived-mode proof-shell-mode 1753,62144
(defconst proof-shell-important-settings1790,63171
(defun proof-shell-config-done 1796,63286

generic/proof-site.el,666
(defconst proof-assistant-table-default35,1157
(defconst proof-general-short-version68,2172
(defconst proof-general-version-year 74,2359
(defgroup proof-general 81,2512
(defgroup proof-general-internals 86,2620
(defun proof-home-directory-fn 99,3008
(defcustom proof-home-directory110,3380
(defcustom proof-images-directory119,3746
(defcustom proof-info-directory125,3948
(defcustom proof-assistant-table154,4925
(defcustom proof-assistants 195,6367
(defun proof-ready-for-assistant 224,7521
(defvar proof-general-configured-provers 276,9813
(defun proof-chose-prover 349,12424
(defun proofgeneral 354,12556
(defun proof-visit-example-file 363,12874

generic/proof-splash.el,990
(defcustom proof-splash-enable 34,955
(defcustom proof-splash-time 39,1107
(defcustom proof-splash-contents47,1391
(defconst proof-splash-startup-msg91,2956
(defconst proof-splash-welcome 100,3334
(define-derived-mode proof-splash-mode 103,3438
(define-key proof-splash-mode-map 109,3612
(define-key proof-splash-mode-map 110,3664
(defsubst proof-emacs-imagep 115,3791
(defun proof-get-image 120,3916
(defvar proof-splash-timeout-conf 142,4716
(defun proof-splash-centre-spaces 145,4829
(defun proof-splash-remove-screen 172,5985
(defun proof-splash-remove-buffer 189,6641
(defvar proof-splash-seen 200,7029
(defun proof-splash-insert-contents 203,7131
(defun proof-splash-display-screen 243,8261
(defalias 'pg-about pg-about
279,9783
(defun proof-splash-message 282,9849
(defun proof-splash-timeout-waiter 295,10307
(defvar proof-splash-old-frame-title-format 308,10865
(defun proof-splash-set-frame-titles 310,10915
(defun proof-splash-unset-frame-titles 319,11230

generic/proof-syntax.el,1278
(defsubst proof-ids-to-regexp 22,464
(defsubst proof-anchor-regexp 29,702
(defconst proof-no-regexp 33,807
(defsubst proof-regexp-alt 36,898
(defsubst proof-regexp-alt-list 45,1210
(defsubst proof-re-search-forward-region 49,1345
(defsubst proof-search-forward 62,1843
(defsubst proof-replace-regexp-in-string 69,2113
(defsubst proof-re-search-forward 74,2364
(defsubst proof-re-search-backward 79,2622
(defsubst proof-re-search-forward-safe 84,2883
(defsubst proof-string-match 90,3164
(defsubst proof-string-match-safe 95,3393
(defsubst proof-stringfn-match 99,3597
(defsubst proof-looking-at 106,3860
(defsubst proof-looking-at-safe 111,4047
(defun proof-buffer-syntactic-context 120,4260
(defsubst proof-looking-at-syntactic-context-default 141,5122
(defun proof-looking-at-syntactic-context 150,5477
(defun proof-inside-comment 159,5939
(defun proof-inside-string 165,6112
(defsubst proof-replace-string 175,6311
(defsubst proof-replace-regexp 180,6515
(defsubst proof-replace-regexp-nocasefold 185,6724
(defvar proof-id 195,7012
(defsubst proof-ids 201,7232
(defun proof-zap-commas 208,7484
(defadvice font-lock-fontify-keywords-region234,8370
(defun proof-format 250,8966
(defun proof-format-filename 269,9605
(defun proof-insert 316,11007

generic/proof-toolbar.el,2401
(defun proof-toolbar-function 33,759
(defun proof-toolbar-icon 37,906
(defun proof-toolbar-enabler 41,1053
(defun proof-toolbar-make-icon 50,1255
(defun proof-toolbar-make-toolbar-items 59,1563
(defvar proof-toolbar-map 85,2424
(defun proof-toolbar-available-p 88,2523
(defun proof-toolbar-setup 98,2829
(defun proof-toolbar-enable 119,3686
(defalias 'proof-toolbar-undo proof-toolbar-undo
152,4744
(defun proof-toolbar-undo-enable-p 154,4812
(defalias 'proof-toolbar-delete proof-toolbar-delete
161,4970
(defun proof-toolbar-delete-enable-p 163,5051
(defalias 'proof-toolbar-home proof-toolbar-home
171,5233
(defalias 'proof-toolbar-next proof-toolbar-next
175,5300
(defun proof-toolbar-next-enable-p 177,5371
(defalias 'proof-toolbar-goto proof-toolbar-goto
183,5487
(defun proof-toolbar-goto-enable-p 185,5537
(defalias 'proof-toolbar-retract proof-toolbar-retract
190,5622
(defun proof-toolbar-retract-enable-p 192,5679
(defalias 'proof-toolbar-use proof-toolbar-use
198,5798
(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p
199,5850
(defalias 'proof-toolbar-prooftree proof-toolbar-prooftree
203,5933
(defalias 'proof-toolbar-restart proof-toolbar-restart
207,6018
(defalias 'proof-toolbar-goal proof-toolbar-goal
211,6083
(defalias 'proof-toolbar-qed proof-toolbar-qed
215,6141
(defun proof-toolbar-qed-enable-p 217,6190
(defalias 'proof-toolbar-state proof-toolbar-state
225,6352
(defalias 'proof-toolbar-state-enable-p proof-toolbar-state-enable-p
226,6395
(defalias 'proof-toolbar-context proof-toolbar-context
230,6474
(defalias 'proof-toolbar-context-enable-p proof-toolbar-context-enable-p
231,6520
(defalias 'proof-toolbar-command proof-toolbar-command
235,6601
(defalias 'proof-toolbar-command-enable-p proof-toolbar-command-enable-p
236,6657
(defun proof-toolbar-help 240,6762
(defalias 'proof-toolbar-find proof-toolbar-find
246,6842
(defalias 'proof-toolbar-find-enable-p proof-toolbar-find-enable-p
247,6894
(defalias 'proof-toolbar-info proof-toolbar-info
251,6969
(defalias 'proof-toolbar-info-enable-p proof-toolbar-info-enable-p
252,7024
(defalias 'proof-toolbar-visibility proof-toolbar-visibility
256,7122
(defun proof-toolbar-visibility-enable-p 258,7182
(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt
263,7296
(defun proof-toolbar-interrupt-enable-p 264,7357
(defun proof-toolbar-scripting-menu 272,7510

generic/proof-tree.el,3278
(defgroup proof-tree 90,3806
(defcustom proof-tree-program 95,3947
(defcustom proof-tree-arguments 100,4093
(defgroup proof-tree-internals 110,4253
(defcustom proof-tree-ignored-commands-regexp 118,4522
(defcustom proof-tree-navigation-command-regexp 127,4921
(defcustom proof-tree-cheating-regexp 135,5240
(defcustom proof-tree-current-goal-regexp 144,5637
(defcustom proof-tree-update-goal-regexp 154,6039
(defcustom proof-tree-additional-subgoal-ID-regexp 166,6608
(defcustom proof-tree-existential-regexp 174,6927
(defcustom proof-tree-existentials-state-start-regexp 188,7547
(defcustom proof-tree-existentials-state-end-regexp 199,8098
(defcustom proof-tree-proof-completed-regexp 211,8741
(defcustom proof-tree-get-proof-info 216,8890
(defcustom proof-tree-extract-instantiated-existentials 240,9931
(defcustom proof-tree-show-sequent-command 257,10649
(defcustom proof-tree-find-begin-of-unfinished-proof 271,11271
(defcustom proof-tree-urgent-action-hook 282,11833
(defvar proof-tree-external-display 306,12688
(defvar proof-tree-process 317,13193
(defconst proof-tree-process-name 320,13282
(defconst proof-tree-process-buffer323,13381
(defconst proof-tree-emacs-exec-regexp327,13521
(defvar proof-tree-last-state 331,13688
(defvar proof-tree-current-proof 335,13792
(defvar proof-tree-sequent-hash 340,13973
(defvar proof-tree-existentials-alist 355,14680
(defvar proof-tree-existentials-alist-history 366,15179
(defun proof-tree-stop-external-display 375,15398
(defun proof-tree-insert-output 383,15662
(defun proof-tree-process-filter 394,16045
(defun proof-tree-process-sentinel 420,16743
(defun proof-tree-start-process 428,17069
(defun proof-tree-is-running 457,18252
(defun proof-tree-ensure-running 462,18413
(defconst proof-tree-protocol-version 472,18617
(defun proof-tree-send-message 477,18817
(defun proof-tree-send-configure 491,19303
(defun proof-tree-send-goal-state 499,19520
(defun proof-tree-send-update-sequent 525,20569
(defun proof-tree-send-switch-goal 538,21006
(defun proof-tree-send-proof-completed 547,21332
(defun proof-tree-send-undo 561,21773
(defun proof-tree-send-quit-proof 566,21955
(defun proof-tree-record-existentials-state 577,22290
(defun proof-tree-undo-state-var 590,22840
(defun proof-tree-undo-existentials 609,23621
(defun proof-tree-delete-existential-assoc 617,23936
(defun proof-tree-add-existential-assoc 623,24199
(defun proof-tree-reset-existentials 636,24814
(defun proof-tree-show-goal-callback 646,25090
(defun proof-tree-make-show-goal-callback 667,26077
(defun proof-tree-urgent-action 671,26238
(defun proof-tree-quit-proof 736,28774
(defun proof-tree-register-existentials 746,29210
(defun proof-tree-extract-goals 759,29754
(defun proof-tree-extract-list 781,30699
(defun proof-tree-extract-existential-info 804,31669
(defun proof-tree-handle-proof-progress 824,32540
(defun proof-tree-handle-navigation 874,34611
(defun proof-tree-handle-proof-command 892,35337
(defun proof-tree-handle-undo 907,35999
(defun proof-tree-update-sequent 939,37298
(defun proof-tree-handle-delayed-output 980,39066
(defun proof-tree-leave-buffer 1031,41089
(defun proof-tree-display-current-proof 1043,41372
(defun proof-tree-external-display-toggle 1075,42713

generic/proof-unicode-tokens.el,497
(defvar proof-unicode-tokens-initialised 31,767
(defun proof-unicode-tokens-init 34,874
(defun proof-unicode-tokens-configure 48,1376
(defun proof-unicode-tokens-mode-if-enabled 60,1822
(defun proof-unicode-tokens-set-global 66,2021
(defun proof-unicode-tokens-enable 82,2591
(defun proof-unicode-tokens-reconfigure 102,3444
(defun proof-unicode-tokens-configure-prover 128,4332
(defun proof-unicode-tokens-activate-prover 133,4513
(defun proof-unicode-tokens-deactivate-prover 140,4759

generic/proof-useropts.el,1619
(defgroup proof-user-options 21,510
(defun proof-set-value 29,689
(defcustom proof-electric-terminator-enable 62,1812
(defcustom proof-toolbar-enable 74,2344
(defcustom proof-imenu-enable 80,2517
(defcustom pg-show-hints 86,2688
(defcustom proof-shell-quiet-errors 91,2821
(defcustom proof-trace-output-slow-catchup 98,3092
(defcustom proof-strict-state-preserving 108,3589
(defcustom proof-strict-read-only 121,4198
(defcustom proof-three-window-enable 134,4777
(defcustom proof-multiple-frames-enable 153,5527
(defcustom proof-delete-empty-windows 162,5860
(defcustom proof-shrink-windows-tofit 173,6391
(defcustom proof-auto-raise-buffers 180,6663
(defcustom proof-colour-locked 187,6898
(defcustom proof-sticky-errors 195,7148
(defcustom proof-query-file-save-when-activating-scripting202,7365
(defcustom proof-prog-name-ask218,8085
(defcustom proof-prog-name-guess224,8245
(defcustom proof-tidy-response232,8510
(defcustom proof-keep-response-history246,8973
(defcustom pg-input-ring-size 256,9361
(defcustom proof-general-debug 261,9513
(defcustom proof-use-parser-cache 270,9884
(defcustom proof-follow-mode 277,10138
(defcustom proof-auto-action-when-deactivating-scripting 301,11315
(defcustom proof-rsh-command 329,12497
(defcustom proof-disappearing-proofs 345,13055
(defcustom proof-full-annotation 350,13216
(defcustom proof-output-tooltips 360,13679
(defcustom proof-minibuffer-messages 371,14186
(defcustom proof-autosend-enable 379,14495
(defcustom proof-autosend-delay 385,14675
(defcustom proof-autosend-all 391,14833
(defcustom proof-fast-process-buffer 396,15002

generic/proof-utils.el,1645
(defmacro proof-with-current-buffer-if-exists 61,1684
(defmacro proof-with-script-buffer 70,2061
(defmacro proof-map-buffers 81,2442
(defmacro proof-sym 86,2627
(defsubst proof-try-require 91,2788
(defun proof-save-some-buffers 104,3119
(defun proof-save-this-buffer 124,3715
(defun proof-file-truename 137,4079
(defun proof-files-to-buffers 141,4261
(defun proof-buffers-in-mode 149,4500
(defun pg-save-from-death 163,4950
(defun proof-define-keys 182,5566
(defun pg-remove-specials 193,5851
(defun pg-remove-specials-in-string 203,6187
(defun proof-safe-split-window-vertically 213,6412
(defun proof-warn-if-unset 218,6592
(defun proof-get-window-for-buffer 223,6810
(defun proof-display-and-keep-buffer 272,9120
(defun proof-clean-buffer 314,10843
(defun pg-internal-warning 330,11499
(defun proof-debug 338,11781
(defun proof-switch-to-buffer 353,12332
(defun proof-resize-window-tofit 375,13456
(defun proof-submit-bug-report 470,17304
(defun proof-deftoggle-fn 505,18661
(defmacro proof-deftoggle 520,19327
(defun proof-defintset-fn 531,19840
(defmacro proof-defintset 550,20664
(defun proof-deffloatset-fn 557,21043
(defmacro proof-deffloatset 573,21757
(defun proof-defstringset-fn 580,22142
(defmacro proof-defstringset 593,22768
(defun proof-escape-keymap-doc 606,23224
(defmacro proof-defshortcut 610,23378
(defmacro proof-definvisible 625,23976
(defun pg-custom-save-vars 652,24905
(defun pg-custom-reset-vars 668,25549
(defun proof-locate-executable 681,25886
(defun pg-current-word-pos 696,26436
(defsubst proof-shell-strip-output-markup 741,28091
(defun proof-minibuffer-message 747,28355

lib/bufhist.el,1257
(defun bufhist-ring-update 38,1344
(defgroup bufhist 47,1666
(defcustom bufhist-ring-size 51,1747
(defvar bufhist-ring 56,1858
(defvar bufhist-ring-pos 59,1932
(defvar bufhist-lastswitch-modified-tick 62,2011
(defvar bufhist-read-only-history 65,2117
(defvar bufhist-saved-mode-line-format 68,2188
(defvar bufhist-normal-read-only 71,2291
(defvar bufhist-top-point 74,2385
(defun bufhist-mode-line-format-entry 77,2475
(defconst bufhist-minor-mode-map106,3549
(define-minor-mode bufhist-mode119,4026
(defun bufhist-get-buffer-contents 141,4907
(defun bufhist-restore-buffer-contents 150,5249
(defun bufhist-checkpoint 159,5563
(defun bufhist-erase-buffer 167,5932
(defun bufhist-checkpoint-and-erase 178,6303
(defun bufhist-switch-to-index 184,6489
(defun bufhist-first 223,8088
(defun bufhist-last 228,8247
(defun bufhist-prev 233,8391
(defun bufhist-next 241,8614
(defun bufhist-delete 246,8754
(defun bufhist-clear 258,9295
(defun bufhist-init 273,9690
(defun bufhist-exit 301,10699
(defun bufhist-set-readwrite 311,10963
(defun bufhist-before-change-function 326,11583
(define-button-type 'bufhist-nextbufhist-next
340,12006
(define-button-type 'bufhist-prevbufhist-prev
344,12103
(defun bufhist-insert-buttons 351,12315

lib/holes.el,2465
(defvar holes-default-hole 44,1076
(defvar holes-active-hole 50,1254
(defgroup holes 60,1451
(defcustom holes-empty-hole-string 65,1550
(defcustom holes-empty-hole-regexp 70,1693
(defface active-hole-face92,2395
(defface inactive-hole-face102,2811
(defvar hole-map116,3252
(defvar holes-mode-map126,3643
(defun holes-region-beginning-or-nil 172,5380
(defun holes-region-end-or-nil 176,5516
(defun holes-copy-active-region 180,5634
(defun holes-is-hole-p 186,5844
(defun holes-hole-start-position 190,5936
(defun holes-hole-end-position 196,6119
(defun holes-hole-buffer 201,6290
(defun holes-hole-at 207,6464
(defun holes-active-hole-exist-p 212,6634
(defun holes-active-hole-start-position 219,6887
(defun holes-active-hole-end-position 227,7255
(defun holes-active-hole-buffer 236,7618
(defun holes-goto-active-hole 244,7919
(defun holes-highlight-hole-as-active 253,8178
(defun holes-highlight-hole 261,8486
(defun holes-disable-active-hole 269,8773
(defun holes-set-active-hole 282,9305
(defun holes-is-in-hole-p 292,9650
(defun holes-make-hole 296,9788
(defun holes-make-hole-at 314,10444
(defun holes-clear-hole 328,10897
(defun holes-clear-hole-at 337,11155
(defun holes-map-holes 345,11411
(defun holes-clear-all-buffer-holes 349,11565
(defun holes-next 359,11866
(defun holes-next-after-active-hole 366,12118
(defun holes-set-active-hole-next 373,12334
(defun holes-replace-segment 392,12871
(defun holes-replace 401,13224
(defun holes-replace-active-hole 429,14402
(defun holes-replace-update-active-hole 436,14693
(defun holes-delete-update-active-hole 454,15340
(defun holes-set-make-active-hole 462,15567
(defalias 'holes-track-mouse-selection holes-track-mouse-selection
477,16122
(defsubst holes-track-mouse-clicks 478,16180
(defun holes-mouse-replace-active-hole 482,16290
(defun holes-destroy-hole 496,16761
(defsubst holes-hole-at-event 510,17143
(defun holes-mouse-destroy-hole 514,17243
(defun holes-mouse-forget-hole 521,17464
(defun holes-mouse-set-make-active-hole 531,17756
(defun holes-mouse-set-active-hole 547,18255
(defun holes-set-point-next-hole-destroy 556,18506
(defun holes-replace-string-by-holes-backward 582,19487
(defun holes-skeleton-end-hook 600,20187
(defconst holes-jump-doc609,20625
(defun holes-replace-string-by-holes-backward-jump 616,20831
(define-minor-mode holes-mode 633,21513
(defun holes-abbrev-complete 728,24995
(defun holes-insert-and-expand 738,25338

lib/local-vars-list.el,373
(defconst local-vars-list-doc 28,770
(defun local-vars-list-insert-empty-zone 44,1332
(defun local-vars-list-find 82,2035
(defun local-vars-list-goto-var 101,2806
(defun local-vars-list-get-current 127,3853
(defun local-vars-list-set-current 148,4703
(defun local-vars-list-get 171,5418
(defun local-vars-list-get-safe 188,5948
(defun local-vars-list-set 193,6142

lib/maths-menu.el,242
(defvar maths-menu-filter-predicate 56,2267
(defvar maths-menu-tokenise-insert 59,2376
(defun maths-menu-build-menu 62,2513
(defvar maths-menu-menu84,3274
(defvar maths-menu-mode-map344,12832
(define-minor-mode maths-menu-mode352,13051

lib/pg-dev.el,199
(defconst pg-dev-lisp-font-lock-keywords52,1534
(defun pg-loadpath 78,2233
(defun unload-pg 88,2404
(defun profile-pg 119,3298
(defun elp-pack-number 149,4405
(defun pg-bug-references 158,4605

lib/pg-fontsets.el,209
(defcustom pg-fontsets-default-fontset 24,671
(defvar pg-fontsets-names 29,817
(defun pg-fontsets-make-fontsetsizes 32,898
(defconst pg-fontsets-base-fonts51,1659
(defun pg-fontsets-make-fontsets 57,1789

lib/proof-compat.el,160
(defvar proof-running-on-win32 32,923
(defun pg-custom-undeclare-variable 53,1725
(defmacro save-selected-frame 86,2550
(defmacro declare-function 152,4558

lib/scomint.el,787
(defvar scomint-buffer-maximum-size 19,446
(defvar scomint-output-filter-functions 24,637
(defvar scomint-mode-map27,747
(defvar scomint-last-input-start 33,926
(defvar scomint-last-input-end 34,964
(defvar scomint-last-output-start 35,1000
(defvar scomint-exec-hook 37,1040
(define-derived-mode scomint-mode 46,1383
(defsubst scomint-check-proc 65,2298
(defun scomint-make-in-buffer 73,2638
(defun scomint-make 97,3905
(defun scomint-exec 110,4616
(defun scomint-exec-1 147,6209
(defalias 'scomint-send-string scomint-send-string
197,8339
(defun scomint-send-eof 199,8393
(defun scomint-send-input 208,8626
(defun scomint-truncate-buffer 234,9522
(defun scomint-strip-ctrl-m 247,9916
(defun scomint-output-filter 261,10493
(defun scomint-interrupt-process 284,11248

lib/span.el,1553
(defalias 'span-start span-start
22,565
(defalias 'span-end span-end
23,603
(defalias 'span-set-property span-set-property
24,637
(defalias 'span-property span-property
25,680
(defalias 'span-make span-make
26,719
(defalias 'span-detach span-detach
27,755
(defalias 'span-set-endpoints span-set-endpoints
28,795
(defalias 'span-buffer span-buffer
29,840
(defun span-read-only-hook 31,881
(defsubst span-read-only 36,1071
(defsubst span-read-write 43,1381
(defsubst span-write-warning 48,1551
(defsubst span-lt 59,2075
(defsubst spans-at-point-prop 64,2219
(defsubst spans-at-region-prop 73,2410
(defsubst span-at 83,2676
(defsubst span-delete 87,2802
(defsubst span-add-delete-action 93,2998
(defsubst span-mapcar-spans 99,3277
(defsubst span-mapc-spans 103,3452
(defsubst span-mapcar-spans-inorder 107,3623
(defun span-at-before 113,3828
(defsubst prev-span 130,4552
(defsubst next-span 136,4705
(defsubst span-live-p 142,4919
(defsubst span-raise 148,5085
(defsubst span-string 152,5218
(defsubst set-span-properties 157,5378
(defsubst span-find-span 163,5572
(defsubst span-at-event 171,5884
(defun fold-spans 177,6081
(defsubst span-detached-p 191,6614
(defsubst set-span-face 195,6730
(defsubst set-span-keymap 199,6828
(defsubst span-delete-spans 207,6997
(defsubst span-property-safe 211,7159
(defsubst span-set-start 215,7296
(defsubst span-set-end 219,7428
(defun span-make-self-removing-span 227,7588
(defun span-delete-self-modification-hook 237,7956
(defun span-make-modifying-removing-span 242,8130

lib/texi-docstring-magic.el,584
(defun texi-docstring-magic-find-face 88,2967
(defun texi-docstring-magic-splice-sep 93,3132
(defconst texi-docstring-magic-munge-table103,3437
(defun texi-docstring-magic-untabify 193,7200
(defun texi-docstring-magic-munge-docstring 200,7398
(defun texi-docstring-magic-texi 239,8679
(defun texi-docstring-magic-format-default 252,9119
(defun texi-docstring-magic-texi-for 268,9752
(defconst texi-docstring-magic-comment326,11711
(defun texi-docstring-magic 332,11865
(defun texi-docstring-magic-face-at-point 366,12944
(defun texi-docstring-magic-insert-magic 381,13467

lib/unicode-chars.el,80
(defvar unicode-chars-alist12,295
(defun unicode-chars-list-chars 5051,245922

lib/unicode-tokens.el,5900
(defgroup unicode-tokens-options 55,1657
(defcustom unicode-tokens-add-help-echo 60,1782
(defun unicode-tokens-toggle-add-help-echo 65,1949
(defvar unicode-tokens-token-symbol-map 79,2355
(defvar unicode-tokens-token-format 98,3014
(defvar unicode-tokens-token-variant-format-regexp 104,3263
(defvar unicode-tokens-shortcut-alist 118,3796
(defvar unicode-tokens-shortcut-replacement-alist 124,4073
(defvar unicode-tokens-control-region-format-regexp 132,4279
(defvar unicode-tokens-control-char-format-regexp 139,4647
(defvar unicode-tokens-control-regions 146,5008
(defvar unicode-tokens-control-characters 149,5084
(defvar unicode-tokens-control-char-format 152,5166
(defvar unicode-tokens-control-region-format-start 155,5279
(defvar unicode-tokens-control-region-format-end 158,5396
(defvar unicode-tokens-tokens-customizable-variables 161,5509
(defconst unicode-tokens-configuration-variables168,5677
(defun unicode-tokens-config 183,6076
(defun unicode-tokens-config-var 187,6221
(defun unicode-tokens-copy-configuration-variables 199,6661
(defvar unicode-tokens-token-list 227,7877
(defvar unicode-tokens-hash-table 230,7997
(defvar unicode-tokens-token-match-regexp 233,8113
(defvar unicode-tokens-uchar-hash-table 239,8396
(defvar unicode-tokens-uchar-regexp 243,8583
(defgroup unicode-tokens-faces 251,8768
(defconst unicode-tokens-font-family-alternatives261,9070
(defface unicode-tokens-symbol-font-face276,9588
(defface unicode-tokens-script-font-face286,9946
(defface unicode-tokens-fraktur-font-face291,10090
(defface unicode-tokens-serif-font-face296,10215
(defface unicode-tokens-sans-font-face301,10352
(defface unicode-tokens-highlight-face306,10474
(defconst unicode-tokens-fonts315,10836
(defconst unicode-tokens-fontsymb-properties324,11053
(define-widget 'unicode-tokens-token-symbol-map unicode-tokens-token-symbol-map
352,12674
(define-widget 'unicode-tokens-shortcut-alist unicode-tokens-shortcut-alist
370,13226
(defconst unicode-tokens-font-lock-extra-managed-props383,13557
(defun unicode-tokens-font-lock-keywords 387,13711
(defun unicode-tokens-calculate-token-match 420,15082
(defun unicode-tokens-usable-composition 450,16118
(defun unicode-tokens-help-echo 463,16497
(defvar unicode-tokens-show-symbols 468,16699
(defun unicode-tokens-interpret-composition 471,16813
(defun unicode-tokens-font-lock-compose-symbol 489,17325
(defun unicode-tokens-prepend-text-properties-in-match 527,18857
(defun unicode-tokens-prepend-text-property 541,19435
(defun unicode-tokens-show-symbols 566,20580
(defun unicode-tokens-symbs-to-props 574,20890
(defvar unicode-tokens-show-controls 594,21589
(defun unicode-tokens-show-controls 597,21680
(defun unicode-tokens-control-char 609,22193
(defun unicode-tokens-control-region 618,22632
(defun unicode-tokens-control-font-lock-keywords 629,23179
(defvar unicode-tokens-use-shortcuts 640,23503
(defun unicode-tokens-use-shortcuts 643,23606
(defun unicode-tokens-map-ordering 659,24202
(defun unicode-tokens-quail-define-rules 668,24555
(defun unicode-tokens-insert-token 691,25232
(defun unicode-tokens-annotate-region 700,25536
(defun unicode-tokens-insert-control 724,26374
(defun unicode-tokens-insert-uchar-as-token 734,26823
(defun unicode-tokens-delete-token-near-point 740,27044
(defun unicode-tokens-delete-backward-char 752,27485
(defun unicode-tokens-delete-char 763,27866
(defun unicode-tokens-delete-backward-1 774,28220
(defun unicode-tokens-delete-1 791,28816
(defun unicode-tokens-prev-token 807,29360
(defun unicode-tokens-rotate-token-forward 815,29657
(defun unicode-tokens-rotate-token-backward 842,30547
(defun unicode-tokens-replace-shortcut-match 847,30749
(defun unicode-tokens-replace-shortcuts 856,31119
(defun unicode-tokens-replace-unicode-match 870,31717
(defun unicode-tokens-replace-unicode 877,32018
(defun unicode-tokens-copy-token 894,32617
(define-button-type 'unicode-tokens-listunicode-tokens-list
901,32838
(defun unicode-tokens-list-tokens 907,33042
(defun unicode-tokens-list-shortcuts 946,34226
(defalias 'unicode-tokens-list-unicode-chars unicode-tokens-list-unicode-chars
964,34864
(defun unicode-tokens-encode-in-temp-buffer 966,34937
(defun unicode-tokens-encode 984,35593
(defun unicode-tokens-encode-str 990,35829
(defun unicode-tokens-copy 994,35991
(defun unicode-tokens-paste 1003,36397
(defvar unicode-tokens-highlight-unicode 1022,37118
(defconst unicode-tokens-unicode-highlight-patterns1025,37210
(defun unicode-tokens-highlight-unicode 1029,37379
(defun unicode-tokens-highlight-unicode-setkeywords 1041,37842
(defun unicode-tokens-initialise 1053,38211
(defvar unicode-tokens-mode-map 1073,38882
(defvar unicode-tokens-display-table1076,38979
(define-minor-mode unicode-tokens-mode1083,39230
(defun unicode-tokens-set-font-var 1219,43805
(defun unicode-tokens-set-font-var-aux 1235,44294
(defun unicode-tokens-mouse-set-font 1266,45455
(defsubst unicode-tokens-face-font-sym 1279,45969
(defun unicode-tokens-set-font-restart 1283,46149
(defun unicode-tokens-save-fonts 1294,46459
(defun unicode-tokens-custom-save-faces 1302,46715
(define-key unicode-tokens-mode-map1319,47171
(define-key unicode-tokens-mode-map1322,47278
(defvar unicode-tokens-quail-translation-keymap1330,47537
(define-key unicode-tokens-quail-translation-keymap1337,47727
(defun unicode-tokens-quail-delete-last-char 1341,47861
(define-key unicode-tokens-mode-map 1356,48288
(define-key unicode-tokens-mode-map 1358,48380
(define-key unicode-tokens-mode-map1360,48471
(define-key unicode-tokens-mode-map1362,48577
(define-key unicode-tokens-mode-map1365,48692
(define-key unicode-tokens-mode-map1367,48801
(define-key unicode-tokens-mode-map1369,48909
(define-key unicode-tokens-mode-map1371,49015
(defun unicode-tokens-customize-submenu 1379,49139
(defun unicode-tokens-define-menu 1386,49362

contrib/mmm/mmm-auto.el,343
(defvar mmm-autoloaded-classes67,2628
(defun mmm-autoload-class 89,3391
(defvar mmm-changed-buffers-list 129,4944
(defun mmm-major-mode-change 132,5051
(defun mmm-check-changed-buffers 145,5572
(defun mmm-mode-on-maybe 154,5922
(defalias 'mmm-add-find-file-hooks mmm-add-find-file-hooks
166,6326
(defun mmm-add-find-file-hook 167,6386

contrib/mmm/mmm-class.el,415
(defun mmm-get-class-spec 42,1247
(defun mmm-get-class-parameter 59,1890
(defun mmm-set-class-parameter 63,2056
(defun* mmm-apply-class75,2406
(defun* mmm-apply-classes90,3023
(defun* mmm-apply-all 110,3754
(defun* mmm-ify124,4201
(defun* mmm-match-region206,7046
(defun mmm-match->point 269,9431
(defun mmm-match-and-verify 284,10001
(defun mmm-get-form 310,11052
(defun mmm-default-get-form 321,11527

contrib/mmm/mmm-cmds.el,712
(defun mmm-ify-by-class 41,1162
(defun mmm-ify-region 63,1774
(defun mmm-ify-by-regexp75,2195
(defun mmm-parse-buffer 97,2838
(defun mmm-parse-region 106,3174
(defun mmm-parse-block 115,3553
(defun mmm-get-block 132,4304
(defun mmm-reparse-current-region 146,4586
(defun mmm-clear-current-region 167,5162
(defun mmm-clear-regions 172,5326
(defun mmm-clear-all-regions 177,5472
(defun* mmm-end-current-region 185,5632
(defun mmm-narrow-to-submode-region 220,6880
(defun mmm-insert-region 239,7494
(defun mmm-insert-by-key 258,8300
(defun mmm-get-insertion-spec 342,11565
(defun mmm-insertion-help 369,12525
(defun mmm-display-insertion-key 379,12888
(defun mmm-get-all-insertion-keys 401,13675

contrib/mmm/mmm-compat.el,418
(defvar mmm-xemacs 40,1263
(defvar mmm-keywords-used49,1566
(defmacro mmm-regexp-opt 91,2582
(defvar mmm-evaporate-property110,3231
(defmacro mmm-set-keymap-default 128,3997
(defmacro mmm-event-key 137,4439
(defvar skeleton-positions 146,4658
(defun mmm-fixup-skeleton 147,4689
(defmacro mmm-make-temp-buffer 159,5112
(defvar mmm-font-lock-available-p 172,5508
(defmacro mmm-set-font-lock-defaults 179,5722

contrib/mmm/mmm-cweb.el,228
(defvar mmm-cweb-section-tags38,1069
(defvar mmm-cweb-section-regexp41,1116
(defvar mmm-cweb-c-part-tags44,1206
(defvar mmm-cweb-c-part-regexp47,1265
(defun mmm-cweb-in-limbo 50,1349
(defun mmm-cweb-verify-brief-c 57,1574

contrib/mmm/mmm-mason.el,410
(defvar mmm-mason-perl-tags41,1187
(defvar mmm-mason-pseudo-perl-tags45,1328
(defvar mmm-mason-non-perl-tags48,1404
(defvar mmm-mason-perl-tags-regexp51,1505
(defvar mmm-mason-pseudo-perl-tags-regexp56,1700
(defvar mmm-mason-tag-names-regexp61,1917
(defun mmm-mason-verify-inline 66,2137
(defun mmm-mason-start-line 156,4789
(defun mmm-mason-end-line 161,4854
(defun mmm-mason-set-mode-line 168,4948

contrib/mmm/mmm-mode.el,1024
(defun mmm-mode 101,3819
(defun mmm-mode-on 140,5324
(defun mmm-mode-off 183,7108
(defvar mmm-mode-map 209,7849
(defvar mmm-mode-prefix-map 212,7924
(defvar mmm-mode-menu-map 215,8034
(defun mmm-define-key 218,8125
(define-key mmm-mode-prefix-map 242,8880
(define-key mmm-mode-prefix-map 249,9138
(define-key mmm-mode-map 252,9249
(define-key mmm-mode-menu-map 255,9351
(define-key mmm-mode-menu-map 257,9423
(define-key mmm-mode-menu-map 259,9482
(define-key mmm-mode-menu-map 261,9563
(define-key mmm-mode-menu-map 263,9644
(define-key mmm-mode-menu-map 265,9731
(define-key mmm-mode-menu-map 268,9825
(define-key mmm-mode-menu-map 270,9885
(define-key mmm-mode-menu-map 273,9976
(define-key mmm-mode-menu-map 275,10036
(define-key mmm-mode-menu-map 277,10143
(define-key mmm-mode-menu-map 279,10228
(define-key mmm-mode-menu-map 282,10314
(define-key mmm-mode-menu-map 284,10374
(define-key mmm-mode-menu-map 286,10487
(define-key mmm-mode-menu-map 288,10572
(define-key mmm-mode-map 291,10655

contrib/mmm/mmm-region.el,1643
(defsubst mmm-overlay-at 54,1699
(defun mmm-overlays-at 59,1884
(defun mmm-included-p 72,2337
(defun mmm-overlays-containing 112,3826
(defun mmm-overlays-contained-in 125,4264
(defun mmm-overlays-overlapping 138,4704
(defun mmm-sort-overlays 149,5067
(defvar mmm-current-overlay 158,5309
(defvar mmm-previous-overlay 163,5524
(defvar mmm-current-submode 168,5712
(defvar mmm-previous-submode 173,5912
(defun mmm-update-current-submode 178,6085
(defun mmm-set-current-submode 199,6880
(defun mmm-submode-at 210,7323
(defun mmm-match-front 219,7598
(defun mmm-match-back 238,8359
(defun mmm-front-start 257,9104
(defun mmm-back-end 265,9408
(defun mmm-valid-submode-region 278,9755
(defun* mmm-make-region305,10911
(defun mmm-make-overlay 431,16261
(defun mmm-get-face 459,17394
(defun mmm-clear-overlays 470,17686
(defun mmm-update-mode-info 486,18151
(defun mmm-update-submode-region 572,21824
(defun mmm-add-hooks 589,22554
(defun mmm-remove-hooks 592,22651
(defun mmm-get-local-variables-list 598,22778
(defun mmm-get-locals 618,23474
(defun mmm-get-saved-local 631,23971
(defun mmm-set-local-variables 635,24136
(defun mmm-get-saved-local-variables 646,24514
(defun mmm-save-changed-local-variables 654,24789
(defun mmm-clear-local-variables 673,25493
(defun mmm-enable-font-lock 684,25758
(defun mmm-update-font-lock-buffer 692,26018
(defun mmm-refontify-maybe 705,26429
(defun mmm-submode-changes-in 720,26909
(defun mmm-regions-in 731,27266
(defun mmm-regions-alist 745,27744
(defun mmm-fontify-region 762,28271
(defun mmm-fontify-region-list 783,29293
(defun mmm-beginning-of-syntax 805,30041

contrib/mmm/mmm-rpm.el,154
(defconst mmm-rpm-sh-start-tags48,1571
(defvar mmm-rpm-sh-end-tags53,1795
(defvar mmm-rpm-sh-start-regexp57,1969
(defvar mmm-rpm-sh-end-regexp61,2147

contrib/mmm/mmm-sample.el,168
(defvar mmm-here-doc-mode-alist 84,2551
(defun mmm-here-doc-get-mode 93,3036
(defun mmm-file-variables-verify 208,6293
(defun mmm-file-variables-find-back 232,7098

contrib/mmm/mmm-univ.el,34
(defun mmm-univ-get-mode 38,1205

contrib/mmm/mmm-utils.el,282
(defmacro mmm-valid-buffer 42,1283
(defmacro mmm-save-all 61,1892
(defun mmm-format-string 74,2174
(defun mmm-format-matches 85,2612
(defmacro mmm-save-keyword 108,3370
(defmacro mmm-save-keywords 116,3697
(defun mmm-looking-back-at 129,4195
(defun mmm-make-marker 146,4735

contrib/mmm/mmm-vars.el,2668
(defgroup mmm 104,3235
(defvar mmm-c-derived-modes111,3345
(defvar mmm-save-local-variables115,3464
(defvar mmm-buffer-saved-locals 341,10245
(defvar mmm-region-saved-locals-defaults 346,10445
(defvar mmm-region-saved-locals-for-dominant 352,10705
(defgroup mmm-faces 362,11082
(defcustom mmm-submode-decoration-level 368,11253
(defface mmm-init-submode-face 386,12097
(defface mmm-cleanup-submode-face 390,12237
(defface mmm-declaration-submode-face 394,12374
(defface mmm-comment-submode-face 398,12520
(defface mmm-output-submode-face 402,12673
(defface mmm-special-submode-face 406,12822
(defface mmm-code-submode-face 410,12986
(defface mmm-default-submode-face 414,13125
(defface mmm-delimiter-face 419,13333
(defcustom mmm-mode-string 426,13459
(defcustom mmm-submode-mode-line-format 431,13590
(defvar mmm-primary-mode-display-name 448,14245
(defvar mmm-buffer-mode-display-name 453,14459
(defun mmm-set-mode-line 459,14758
(defvar mmm-classes 483,15566
(defvar mmm-global-classes 489,15811
(defcustom mmm-mode-ext-classes-alist 496,15993
(defun mmm-add-mode-ext-class 515,16783
(defcustom mmm-major-mode-preferences524,17108
(defun mmm-add-to-major-mode-preferences 542,17836
(defun mmm-ensure-modename 558,18594
(defun mmm-modename->function 567,18897
(defcustom mmm-delimiter-mode 581,19346
(defcustom mmm-mode-prefix-key 591,19615
(defcustom mmm-command-modifiers 596,19742
(defcustom mmm-insert-modifiers 610,20375
(defcustom mmm-use-old-command-keys 625,21053
(defun mmm-use-old-command-keys 635,21517
(defcustom mmm-mode-hook 643,21709
(defun mmm-run-constructed-hook 663,22516
(defun mmm-run-major-hook 671,22860
(defun mmm-run-submode-hook 674,22937
(defvar mmm-class-hooks-run 677,23024
(defun mmm-run-class-hook 682,23196
(defvar mmm-primary-mode-entry-hook 687,23368
(defcustom mmm-major-mode-hook 702,24015
(defun mmm-run-major-mode-hook 716,24646
(defcustom mmm-global-mode 729,25187
(defcustom mmm-never-modes745,25854
(defvar mmm-set-file-name-for-modes 763,26154
(defvar mmm-mode 774,26513
(defvar mmm-primary-mode 782,26721
(defvar mmm-classes-alist 793,27087
(defun mmm-add-classes 948,35294
(defun mmm-add-group 953,35459
(defun mmm-add-to-group 963,35832
(defconst mmm-version 977,36259
(defun mmm-version 980,36324
(defvar mmm-temp-buffer-name 987,36467
(defvar mmm-interactive-history 993,36597
(defun mmm-add-to-history 999,36866
(defun mmm-clear-history 1002,36949
(defvar mmm-mode-ext-classes 1010,37134
(defun mmm-get-mode-ext-classes 1015,37345
(defun mmm-clear-mode-ext-classes 1024,37672
(defun mmm-mode-ext-applies 1028,37797
(defun mmm-get-all-classes 1042,38176

doc/ProofGeneral.texi,7046
@node Top145,4126
@node Preface184,5319
@node News for Version 4.1News for Version 4.1
208,5933
@node News for Version 4.0News for Version 4.0
219,6240
@node Future240,7091
@node Credits269,8426
@node Introducing Proof GeneralIntroducing Proof General
391,12535
@node Installing Proof GeneralInstalling Proof General
446,14509
@node Quick start guideQuick start guide
460,14958
@node Features of Proof GeneralFeatures of Proof General
504,17079
@node Supported proof assistantsSupported proof assistants
610,21623
@node Prerequisites for this manualPrerequisites for this manual
659,23504
@node Organization of this manualOrganization of this manual
703,25123
@node Basic Script ManagementBasic Script Management
729,25951
@node Walkthrough example in IsabelleWalkthrough example in Isabelle
748,26551
@node Proof scriptsProof scripts
1033,37946
@node Script buffersScript buffers
1076,40066
@node Locked queue and editing regionsLocked queue and editing regions
1098,40643
@node Goal-save sequencesGoal-save sequences
1154,42790
@node Active scripting bufferActive scripting buffer
1191,44274
@node Summary of Proof General buffersSummary of Proof General buffers
1264,47907
@node Script editing commandsScript editing commands
1313,50164
@node Script processing commandsScript processing commands
1393,53123
@node Proof assistant commandsProof assistant commands
1519,58368
@node Toolbar commandsToolbar commands
1712,65296
@node Interrupting during trace outputInterrupting during trace output
1737,66255
@node Advanced Script Management and EditingAdvanced Script Management and Editing
1777,68185
@node Document centred workingDocument centred working
1798,68806
@node Automatic processingAutomatic processing
1910,73484
@node Visibility of completed proofsVisibility of completed proofs
1965,75532
@node Switching between proof scriptsSwitching between proof scripts
2020,77472
@node View of processed files View of processed files 
2057,79444
@node Retracting across filesRetracting across files
2117,82495
@node Asserting across filesAsserting across files
2130,83126
@node Automatic multiple file handlingAutomatic multiple file handling
2143,83692
@node Escaping script managementEscaping script management
2168,84726
@node Editing featuresEditing features
2225,86838
@node Unicode symbols and special layout supportUnicode symbols and special layout support
2295,89617
@node Maths menuMaths menu
2337,91175
@node Unicode Tokens modeUnicode Tokens mode
2354,91866
@node Configuring tokens symbols and shortcutsConfiguring tokens symbols and shortcuts
2404,94289
@node Special layout Special layout 
2434,95250
@node Moving between Unicode and tokensMoving between Unicode and tokens
2544,99368
@node Finding available tokens shortcuts and symbolsFinding available tokens shortcuts and symbols
2599,101479
@node Selecting suitable fontsSelecting suitable fonts
2638,102653
@node Support for other PackagesSupport for other Packages
2703,105641
@node Syntax highlightingSyntax highlighting
2733,106477
@node Imenu and SpeedbarImenu and Speedbar
2761,107480
@node Support for outline modeSupport for outline mode
2807,109151
@node Support for completionSupport for completion
2832,110280
@node Support for tagsSupport for tags
2889,112442
@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
2941,114790
@node Goals buffer commandsGoals buffer commands
2957,115385
@node Graphical Proof-Tree VisualizationGraphical Proof-Tree Visualization
3056,119538
@node Starting and Stopping Proof-Tree VisualizationStarting and Stopping Proof-Tree Visualization
3079,120430
@node Features of ProoftreeFeatures of Prooftree
3107,121587
@node Prooftree CustomizationProoftree Customization
3139,122799
@node Customizing Proof GeneralCustomizing Proof General
3163,123678
@node Basic optionsBasic options
3203,125348
@node How to customizeHow to customize
3227,126118
@node Display customizationDisplay customization
3274,128085
@node User optionsUser options
3442,135047
@node Changing facesChanging faces
3678,143715
@node Script buffer facesScript buffer faces
3700,144590
@node Goals and response facesGoals and response faces
3746,146190
@node Tweaking configuration settingsTweaking configuration settings
3791,147722
@node Hints and TipsHints and Tips
3848,150248
@node Adding your own keybindingsAdding your own keybindings
3867,150849
@node Using file variablesUsing file variables
3931,153463
@node Using abbreviationsUsing abbreviations
4007,156134
@node LEGO Proof GeneralLEGO Proof General
4046,157549
@node LEGO specific commandsLEGO specific commands
4087,158918
@node LEGO tagsLEGO tags
4107,159373
@node LEGO customizationsLEGO customizations
4117,159620
@node Coq Proof GeneralCoq Proof General
4149,160539
@node Coq-specific commandsCoq-specific commands
4165,160905
@node Multiple File SupportMultiple File Support
4188,161413
@node Automatic Compilation in DetailAutomatic Compilation in Detail
4258,164002
@node Locking AncestorsLocking Ancestors
4333,167353
@node Customizing Coq Multiple File SupportCustomizing Coq Multiple File Support
4366,168778
@node Current LimitationsCurrent Limitations
4598,178548
@node Editing multiple proofsEditing multiple proofs
4624,179400
@node User-loaded tacticsUser-loaded tactics
4648,180508
@node Holes featureHoles feature
4712,182982
@node Proof-Tree VisualizationProof-Tree Visualization
4737,184201
@node Isabelle Proof GeneralIsabelle Proof General
4749,184551
@node Choosing logic and starting isabelleChoosing logic and starting isabelle
4775,185427
@node Isabelle commandsIsabelle commands
4844,188228
@node Isabelle settingsIsabelle settings
4987,192420
@node Isabelle customizationsIsabelle customizations
5001,193002
@node HOL Proof GeneralHOL Proof General
5024,193489
@node Shell Proof GeneralShell Proof General
5066,195311
@node Obtaining and InstallingObtaining and Installing
5102,196770
@node Obtaining Proof GeneralObtaining Proof General
5117,197135
@node Installing Proof General from tarballInstalling Proof General from tarball
5143,198017
@node Setting the names of binariesSetting the names of binaries
5167,198807
@node Notes for syssiesNotes for syssies
5195,199747
@node Bugs and EnhancementsBugs and Enhancements
5271,202744
@node References5292,203559
@node History of Proof GeneralHistory of Proof General
5332,204582
@node Old News for 3.0Old News for 3.0
5426,208747
@node Old News for 3.1Old News for 3.1
5496,212441
@node Old News for 3.2Old News for 3.2
5522,213613
@node Old News for 3.3Old News for 3.3
5583,216616
@node Old News for 3.4Old News for 3.4
5602,217513
@node Old News for 3.5Old News for 3.5
5624,218568
@node Old News for 3.6Old News for 3.6
5628,218625
@node Old News for 3.7Old News for 3.7
5633,218725
@node Function IndexFunction Index
5663,220179
@node Variable IndexVariable Index
5667,220255
@node Keystroke IndexKeystroke Index
5671,220335
@node Concept IndexConcept Index
5675,220401

doc/PG-adapting.texi,4541
@node Top137,3889
@node Introduction175,5039
@node Future216,6692
@node Credits252,8288
@node Beginning with a New ProverBeginning with a New Prover
262,8580
@node Overview of adding a new proverOverview of adding a new prover
302,10522
@node Demonstration instance and easy configurationDemonstration instance and easy configuration
384,14071
@node Major modes used by Proof GeneralMajor modes used by Proof General
453,17462
@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands
496,19172
@node Settings for generic user-level commandsSettings for generic user-level commands
511,19718
@node Menu configurationMenu configuration
556,21450
@node Toolbar configurationToolbar configuration
580,22367
@node Proof Script SettingsProof Script Settings
639,24604
@node Recognizing commands and commentsRecognizing commands and comments
662,25216
@node Recognizing proofsRecognizing proofs
799,31669
@node Recognizing other elementsRecognizing other elements
903,35973
@node Configuring undo behaviourConfiguring undo behaviour
966,38452
@node Nested proofsNested proofs
1103,43839
@node Safe (state-preserving) commandsSafe (state-preserving) commands
1143,45465
@node Activate scripting hookActivate scripting hook
1166,46418
@node Automatic multiple filesAutomatic multiple files
1190,47288
@node Completely asserted buffersCompletely asserted buffers
1211,48134
@node Completions1244,49599
@node Proof Shell SettingsProof Shell Settings
1285,51089
@node Proof shell commandsProof shell commands
1316,52371
@node Script input to the shellScript input to the shell
1493,60135
@node Settings for matching various output from proof processSettings for matching various output from proof process
1563,63339
@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process
1686,68750
@node Hooks and other settingsHooks and other settings
1913,78712
@node Goals Buffer SettingsGoals Buffer Settings
1992,81856
@node Splash Screen SettingsSplash Screen Settings
2066,84846
@node Global ConstantsGlobal Constants
2092,85601
@node Handling Multiple FilesHandling Multiple Files
2118,86430
@node Configuring Editing SyntaxConfiguring Editing Syntax
2287,95099
@node Configuring Font LockConfiguring Font Lock
2344,97216
@node Configuring TokensConfiguring Tokens
2420,100928
@node Configuring Proof-Tree VisualizationConfiguring Proof-Tree Visualization
2470,103048
@node Prerequisites2487,103588
@node Proof-Tree Display InternalsProof-Tree Display Internals
2550,106239
@node Organization of the CodeOrganization of the Code
2568,106729
@node Communication2664,110992
@node Guards2689,112104
@node Urgent and Delayed ActionsUrgent and Delayed Actions
2743,114249
@node Full AnnotationFull Annotation
2804,116757
@node Configuring Prooftree for a New Proof AssistantConfiguring Prooftree for a New Proof Assistant
2818,117331
@node Proof Tree Elisp configurationProof Tree Elisp configuration
2830,117663
@node Prooftree AdaptionProoftree Adaption
2851,118493
@node Writing More Lisp CodeWriting More Lisp Code
2871,119172
@node Default values for generic settingsDefault values for generic settings
2888,119817
@node Adding prover-specific configurationsAdding prover-specific configurations
2918,120900
@node Useful variablesUseful variables
2961,122182
@node Useful functions and macrosUseful functions and macros
2976,122681
@node Internals of Proof GeneralInternals of Proof General
3086,126993
@node Spans3116,127923
@node Proof General site configurationProof General site configuration
3131,128296
@node Configuration variable mechanismsConfiguration variable mechanisms
3214,131377
@node Global variablesGlobal variables
3344,137093
@node Proof script modeProof script mode
3419,139717
@node Proof shell modeProof shell mode
3683,151674
@node Debugging4234,174109
@node Plans and IdeasPlans and Ideas
4277,174985
@node Proof by pointing and similar featuresProof by pointing and similar features
4298,175707
@node Granularity of atomic command sequencesGranularity of atomic command sequences
4336,177365
@node Browser mode for script files and theoriesBrowser mode for script files and theories
4381,179590
@node Demonstration InstantiationsDemonstration Instantiations
4411,180621
@node demoisa-easy.el4427,181052
@node demoisa.el4489,183190
@node Function IndexFunction Index
4643,188056
@node Variable IndexVariable Index
4647,188132
@node Concept IndexConcept Index
4656,188311

generic/proof.el,0

pgshell/pgshell.el,0

isar/isar-profiling.el,0

isar/interface-setup.el,0

coq/coq-mmm.el,0

coq/coq-autotest.el,0

acl2/acl2.el,0