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,8178
(defcustom coq-prog-name58,1726
(defcustom coq-translate-to-v8 77,2578
(defun coq-build-prog-args 83,2758
(defcustom coq-compiler93,3052
(defcustom coq-dependency-analyzer99,3189
(defcustom coq-use-makefile 105,3329
(defcustom coq-default-undo-limit 111,3501
(defconst coq-shell-init-cmd116,3629
(defcustom coq-prog-env 125,3956
(defconst coq-shell-restart-cmd 133,4205
(defvar coq-shell-prompt-pattern135,4259
(defvar coq-shell-cd 143,4562
(defvar coq-shell-proof-completed-regexp 147,4722
(defvar coq-goal-regexp150,4877
(defun get-coq-library-directory 155,4973
(defconst coq-library-directory 161,5155
(defcustom coq-tags 164,5282
(defconst coq-interrupt-regexp 169,5430
(defcustom coq-www-home-page 172,5523
(defvar coq-outline-regexp183,5698
(defvar coq-outline-heading-end-regexp 190,5911
(defvar coq-shell-outline-regexp 192,5965
(defvar coq-shell-outline-heading-end-regexp 193,6015
(defconst coq-state-preserving-tactics-regexp196,6079
(defconst coq-state-changing-commands-regexp198,6181
(defconst coq-state-preserving-commands-regexp200,6290
(defconst coq-commands-regexp202,6403
(defvar coq-retractable-instruct-regexp204,6482
(defvar coq-non-retractable-instruct-regexp206,6574
(defcustom coq-use-smie 238,7270
(defconst coq-smie-grammar246,7499
(defun coq-smie-search-token-forward 298,9919
(defun coq-smie-search-token-backward 311,10426
(defconst coq-smie-proof-end-tokens337,11638
(defun coq-smie-forward-token 341,11768
(defun coq-smie-backward-token 387,13521
(defun coq-smie-rules 432,15226
(defconst coq-script-command-end-regexp 503,18286
(defun coq-script-parse-function 512,18715
(defun coq-set-undo-limit 519,18941
(defun build-list-id-from-string 523,19071
(defun coq-last-prompt-info 535,19569
(defun coq-last-prompt-info-safe 547,20101
(defvar coq-last-but-one-statenum 553,20358
(defvar coq-last-but-one-proofnum 560,20655
(defvar coq-last-but-one-proofstack 563,20753
(defsubst coq-get-span-statenum 566,20863
(defsubst coq-get-span-proofnum 570,20978
(defsubst coq-get-span-proofstack 574,21093
(defsubst coq-set-span-statenum 578,21237
(defsubst coq-get-span-goalcmd 582,21368
(defsubst coq-set-span-goalcmd 586,21482
(defsubst coq-set-span-proofnum 590,21612
(defsubst coq-set-span-proofstack 594,21743
(defsubst proof-last-locked-span 598,21903
(defun proof-clone-buffer 602,22037
(defun proof-store-buffer-win 616,22574
(defun proof-store-response-win 627,23067
(defun proof-store-goals-win 631,23194
(defun coq-set-state-infos 643,23726
(defun count-not-intersection 681,25812
(defun coq-find-and-forget 711,27064
(defvar coq-current-goal 738,28369
(defun coq-goal-hyp 741,28434
(defun coq-state-preserving-p 754,28908
(defconst notation-print-kinds-table768,29229
(defun coq-PrintScope 772,29396
(defun coq-guess-or-ask-for-string 790,29945
(defun coq-ask-do 804,30485
(defsubst coq-put-into-brackets 813,30870
(defsubst coq-put-into-quotes 816,30931
(defun coq-SearchIsos 819,30990
(defun coq-SearchConstant 827,31229
(defun coq-Searchregexp 831,31322
(defun coq-SearchRewrite 837,31463
(defun coq-SearchAbout 841,31560
(defun coq-Print 847,31703
(defun coq-About 852,31827
(defun coq-LocateConstant 857,31946
(defun coq-LocateLibrary 862,32049
(defun coq-LocateNotation 867,32166
(defun coq-Pwd 875,32397
(defun coq-Inspect 880,32521
(defun coq-PrintSection(884,32621
(defun coq-Print-implicit 888,32714
(defun coq-Check 893,32865
(defun coq-Show 898,32973
(defun coq-Compile 912,33416
(defun coq-guess-command-line 924,33734
(defpacustom use-editing-holes 961,35291
(defun coq-mode-config 970,35594
(defun coq-shell-mode-config 1066,39074
(defun coq-goals-mode-config 1111,40903
(defun coq-response-config 1118,41147
(defpacustom print-fully-explicit 1144,41988
(defpacustom print-implicit 1149,42136
(defpacustom print-coercions 1154,42302
(defpacustom print-match-wildcards 1159,42446
(defpacustom print-elim-types 1164,42626
(defpacustom printing-depth 1169,42792
(defpacustom undo-depth 1174,42953
(defpacustom time-commands 1179,43119
(defgroup coq-auto-compile 1190,43369
(defpacustom compile-before-require 1195,43520
(defcustom coq-compile-command 1207,44012
(defconst coq-compile-substitution-list1237,45295
(defcustom coq-load-path 1257,46216
(defcustom coq-compile-auto-save 1308,48737
(defcustom coq-lock-ancestors 1333,49795
(defpacustom confirm-external-compilation 1342,50116
(defcustom coq-load-path-include-current 1351,50423
(defcustom coq-compile-ignored-directories 1360,50741
(defcustom coq-compile-ignore-library-directory 1373,51374
(defcustom coq-coqdep-error-regexp1385,51862
(defconst coq-require-command-regexp1401,52580
(defconst coq-require-id-regexp1408,52937
(defvar coq-compile-history 1416,53371
(defvar coq-compile-response-buffer 1419,53455
(defvar coq-debug-auto-compilation 1423,53590
(defun time-less-or-equal 1429,53698
(defun coq-max-dep-mod-time 1437,54036
(defun coq-prog-args 1460,54840
(defun coq-lock-ancestor 1469,55099
(defun coq-unlock-ancestor 1485,55874
(defun coq-unlock-all-ancestors-of-span 1492,56169
(defun coq-compile-ignore-file 1499,56465
(defun coq-library-src-of-obj-file 1523,57348
(defun coq-option-of-load-path-entry 1528,57580
(defun coq-include-options 1544,58171
(defun coq-init-compile-response-buffer 1564,58995
(defun coq-display-compile-response-buffer 1587,60067
(defun coq-get-library-dependencies 1601,60701
(defun coq-compile-library 1648,62926
(defun coq-compile-library-if-necessary 1675,64137
(defun coq-make-lib-up-to-date 1721,66009
(defun coq-auto-compile-externally 1777,68472
(defun coq-map-module-id-to-obj-file 1820,70618
(defun coq-check-module 1873,73220
(defvar coq-process-require-current-buffer1901,74662
(defun coq-compile-save-buffer-filter 1907,74927
(defun coq-compile-save-some-buffers 1917,75341
(defun coq-preprocess-require-commands 1939,76243
(defun coq-switch-buffer-kill-proof-shell 1972,77812
(defun coq-preprocessing 1993,78530
(defun coq-fake-constant-markup 2007,78985
(defun coq-create-span-menu 2023,79590
(defconst module-kinds-table2041,80103
(defconst modtype-kinds-table2045,80252
(defun coq-insert-section-or-module 2049,80381
(defconst reqkinds-kinds-table2070,81231
(defun coq-insert-requires 2074,81375
(defun coq-end-Section 2087,81854
(defun coq-insert-intros 2105,82432
(defun coq-insert-infoH-hook 2117,82963
(defun coq-insert-as 2122,83171
(defun coq-insert-match 2139,83864
(defun coq-insert-solve-tactic 2168,85033
(defun coq-insert-tactic 2174,85284
(defun coq-insert-tactical 2180,85486
(defun coq-insert-command 2186,85717
(defun coq-insert-term 2191,85882
(define-key coq-keymap 2196,86043
(define-key coq-keymap 2197,86101
(define-key coq-keymap 2198,86158
(define-key coq-keymap 2199,86227
(define-key coq-keymap 2200,86283
(define-key coq-keymap 2201,86332
(define-key coq-keymap 2202,86390
(define-key coq-keymap 2203,86440
(define-key coq-keymap 2204,86495
(define-key coq-keymap 2206,86548
(define-key coq-keymap 2208,86622
(define-key coq-keymap 2209,86679
(define-key coq-keymap 2212,86744
(define-key coq-keymap 2213,86804
(define-key coq-keymap 2215,86860
(define-key coq-keymap 2216,86910
(define-key coq-keymap 2217,86960
(define-key coq-keymap 2218,87016
(define-key coq-keymap 2219,87066
(define-key coq-keymap 2220,87110
(define-key coq-keymap 2221,87169
(define-key coq-goals-mode-map 2224,87230
(define-key coq-goals-mode-map 2225,87312
(define-key coq-goals-mode-map 2226,87394
(define-key coq-goals-mode-map 2227,87481
(define-key coq-goals-mode-map 2228,87563
(defvar last-coq-error-location 2237,87868
(defun coq-get-last-error-location 2245,88252
(defun coq-highlight-error 2295,90815
(defun coq-highlight-error-hook 2323,91896
(defun first-word-of-buffer 2333,92113
(defun coq-show-first-goal 2341,92316
(defvar coq-modeline-string2 2357,92981
(defvar coq-modeline-string1 2358,93015
(defvar coq-modeline-string0 2359,93049
(defun coq-build-subgoals-string 2360,93090
(defun coq-update-minor-mode-alist 2365,93256
(defun is-not-split-vertic 2397,94649
(defun optim-resp-windows 2406,95089

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,4054
(defun coq-search-comment-delimiter-backward 112,4384
(defun coq-skip-until-one-comment-backward 119,4658
(defun coq-skip-until-one-comment-forward 134,5365
(defun coq-looking-at-comment 145,5883
(defun coq-find-comment-start 149,6024
(defun coq-find-comment-end 160,6457
(defun coq-looking-at-syntactic-context 172,6950
(defconst coq-end-command-or-comment-regexp178,7172
(defconst coq-end-command-or-comment-start-regexp181,7281
(defun coq-find-not-in-comment-backward 184,7398
(defun coq-find-not-in-comment-forward 204,8288
(defun coq-is-on-ending-context 230,9480
(defun coq-empty-command-p 239,9693
(defun coq-script-parse-cmdend-forward 254,10412
(defun coq-script-parse-cmdend-backward 303,12675
(defun coq-find-current-start 341,14351
(defun coq-find-real-start 350,14677
(defun same-line 356,14895
(defun coq-command-at-point 359,14982
(defun coq-commands-at-line 374,15593
(defun coq-indent-only-spaces-on-line 398,16559
(defun coq-indent-find-reg 404,16836
(defun coq-find-no-syntactic-on-line 418,17372
(defun coq-back-to-indentation-prevline 431,17845
(defun coq-find-unclosed 477,19912
(defun coq-find-at-same-level-zero 507,21222
(defun coq-find-unopened 536,22488
(defun coq-find-last-unopened 579,23922
(defun coq-end-offset 590,24319
(defun coq-add-iter 615,25089
(defun coq-goal-count 618,25195
(defun coq-save-count 620,25267
(defun coq-proof-count 625,25469
(defun coq-goal-save-diff-maybe-proof 631,25757
(defun coq-indent-command-offset 641,26051
(defun coq-indent-expr-offset 707,29232
(defun coq-indent-comment-offset 826,34114
(defun coq-indent-offset 858,35566
(defun coq-indent-calculate 877,36440
(defun coq-indent-line 880,36528
(defun coq-indent-line-not-comments 890,36894
(defun coq-indent-region 900,37283

coq/coq-local-vars.el,229
(defconst coq-local-vars-doc 21,445
(defun coq-insert-coq-prog-name 84,2767
(defun coq-read-directory 97,3318
(defun coq-ask-load-path 114,4133
(defun coq-ask-prog-name 132,4966
(defun coq-ask-insert-coq-prog-name 149,5677

coq/coq-syntax.el,2736
(defcustom coq-user-tactics-db 21,583
(defcustom coq-user-commands-db 38,1096
(defcustom coq-user-tacticals-db 54,1615
(defcustom coq-user-solve-tactics-db 70,2136
(defcustom coq-user-cheat-tactics-db 86,2655
(defcustom coq-user-reserved-db 105,3201
(defvar coq-tactics-db123,3732
(defvar coq-solve-tactics-db296,12866
(defvar coq-solve-cheat-tactics-db323,13889
(defvar coq-tacticals-db335,14064
(defvar coq-decl-db359,14950
(defvar coq-defn-db384,16406
(defvar coq-goal-starters-db449,21128
(defvar coq-other-commands-db479,22931
(defvar coq-commands-db614,32916
(defvar coq-terms-db621,33136
(defun coq-count-match 683,35751
(defun coq-module-opening-p 699,36480
(defun coq-section-command-p 710,36891
(defun coq-goal-command-str-p 714,36988
(defun coq-goal-command-p 741,38090
(defvar coq-keywords-save-strict751,38429
(defvar coq-keywords-save758,38670
(defun coq-save-command-p 763,38749
(defvar coq-keywords-kill-goal774,39077
(defvar coq-keywords-state-changing-misc-commands778,39167
(defvar coq-keywords-goal781,39292
(defvar coq-keywords-decl784,39375
(defvar coq-keywords-defn787,39449
(defvar coq-keywords-state-changing-commands791,39524
(defvar coq-keywords-state-preserving-commands800,39784
(defvar coq-keywords-commands805,40000
(defvar coq-solve-tactics810,40148
(defvar coq-solve-tactics-regexp814,40269
(defvar coq-solve-cheat-tactics818,40403
(defvar coq-solve-cheat-tactics-regexp822,40548
(defvar coq-tacticals826,40706
(defvar coq-reserved832,40845
(defvar coq-reserved-regexp 842,41180
(defvar coq-state-changing-tactics846,41291
(defvar coq-state-preserving-tactics849,41400
(defvar coq-tactics853,41514
(defvar coq-tactics-regexp 856,41603
(defvar coq-retractable-instruct859,41758
(defvar coq-non-retractable-instruct862,41868
(defvar coq-keywords866,41996
(defun proof-regexp-alt-list-symb 872,42220
(defvar coq-keywords-regexp 875,42325
(defvar coq-symbols878,42398
(defvar coq-error-regexp 900,42639
(defvar coq-id 903,42867
(defvar coq-id-shy 904,42892
(defvar coq-ids 907,42994
(defun coq-first-abstr-regexp 909,43060
(defcustom coq-variable-highlight-enable 912,43155
(defvar coq-font-lock-terms918,43282
(defconst coq-save-command-regexp-strict940,44365
(defconst coq-save-command-regexp946,44533
(defconst coq-save-with-hole-regexp951,44686
(defconst coq-goal-command-regexp955,44846
(defconst coq-goal-with-hole-regexp958,44948
(defconst coq-decl-with-hole-regexp962,45082
(defconst coq-defn-with-hole-regexp969,45332
(defconst coq-with-with-hole-regexp979,45622
(defvar coq-font-lock-keywords-1994,46152
(defvar coq-font-lock-keywords 1022,47487
(defun coq-init-syntax-table 1024,47545
(defconst coq-generic-expression1049,48272

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,419
(defvar hol98-rules 18,447
(defvar hol98-tactics 19,472
(defvar hol98-tacticals 20,499

isar/isabelle-system.el,1254
(defgroup isabelle 28,797
(defcustom isabelle-web-page32,925
(defcustom isa-isabelle-command41,1142
(defvar isabelle-not-found 59,1824
(defun isa-set-isabelle-command 62,1939
(defun isa-shell-command-to-string 85,2957
(defun isa-getenv 91,3181
(defcustom isabelle-program-name-override 111,3880
(defun isa-tool-list-logics 122,4226
(defcustom isabelle-logics-available 129,4472
(defcustom isabelle-chosen-logic 139,4809
(defvar isabelle-chosen-logic-prev 155,5393
(defun isabelle-hack-local-variables-function 158,5513
(defun isabelle-set-prog-name 170,5952
(defun isabelle-choose-logic 194,7072
(defun isa-view-doc 213,7834
(defun isa-tool-list-docs 220,8060
(defconst isabelle-verbatim-regexp 238,8790
(defun isabelle-verbatim 241,8932
(defcustom isabelle-refresh-logics 248,9093
(defvar isabelle-docs-menu256,9421
(defvar isabelle-logics-menu-entries 263,9706
(defun isabelle-logics-menu-calculate 266,9779
(defvar isabelle-time-to-refresh-logics 287,10421
(defun isabelle-logics-menu-refresh 291,10516
(defun isabelle-menu-bar-update-logics 306,11149
(defun isabelle-load-isar-keywords 322,11778
(defun isabelle-create-span-menu 343,12506
(defun isabelle-xml-sml-escapes 359,12937
(defun isabelle-process-pgip 362,13038

isar/isar-autotest.el,31
(defvar isar-long-tests 8,186

isar/isar.el,1595
(defcustom isar-keywords-name 39,915
(defpgdefault completion-table 55,1426
(defcustom isar-web-page57,1479
(defun isar-strip-terminators 71,1829
(defun isar-markup-ml 83,2185
(defun isar-mode-config-set-variables 88,2320
(defun isar-shell-mode-config-set-variables 153,5119
(defun isar-set-proof-find-theorems-command 235,8309
(defpacustom use-find-theorems-form 241,8493
(defun isar-set-undo-commands 246,8659
(defpacustom use-linear-undo 261,9292
(defun isar-configure-from-settings 266,9450
(defun isar-remove-file 274,9600
(defun isar-shell-compute-new-files-list 286,9904
(define-derived-mode isar-shell-mode 305,10474
(define-derived-mode isar-response-mode 310,10601
(define-derived-mode isar-goals-mode 315,10734
(define-derived-mode isar-mode 320,10860
(defpgdefault menu-entries372,12575
(defun isar-set-command 403,13769
(defpgdefault help-menu-entries 408,13899
(defun isar-count-undos 411,13975
(defun isar-find-and-forget 437,14941
(defun isar-goal-command-p 473,16284
(defun isar-global-save-command-p 478,16461
(defvar isar-current-goal 499,17245
(defun isar-state-preserving-p 502,17311
(defvar isar-shell-current-line-width 527,18160
(defun isar-shell-adjust-line-width 532,18352
(defsubst isar-string-wrapping 555,19117
(defsubst isar-positions-of 564,19311
(defcustom isar-wrap-commands-singly 570,19516
(defun isar-command-wrapping 576,19712
(defun isar-preprocessing 584,20026
(defun isar-mode-config 602,20577
(defun isar-shell-mode-config 616,21230
(defun isar-response-mode-config 626,21579
(defun isar-goals-mode-config 636,21914

isar/isar-find-theorems.el,779
(defvar isar-find-theorems-data 19,565
(defun isar-find-theorems-minibuffer 35,1039
(defun isar-find-theorems-form 49,1658
(defvar isar-find-theorems-widget-number 92,3532
(defvar isar-find-theorems-widget-pattern 95,3630
(defvar isar-find-theorems-widget-intro 98,3722
(defvar isar-find-theorems-widget-elim 101,3808
(defvar isar-find-theorems-widget-dest 104,3892
(defvar isar-find-theorems-widget-name 107,3976
(defvar isar-find-theorems-widget-simp 110,4063
(defun isar-find-theorems-create-searchform115,4209
(defun isar-find-theorems-create-help 255,8752
(defun isar-find-theorems-submit-searchform298,10924
(defun isar-find-theorems-parse-criteria 376,13294
(defun isar-find-theorems-parse-number 469,16275
(defun isar-find-theorems-filter-empty 479,16552

isar/isar-keywords.el,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,744
(defconst isar-start-sml-regexp36,1172

isar/isar-syntax.el,4005
(defconst isar-script-syntax-table-entries18,483
(defconst isar-script-syntax-table-alist42,885
(defun isar-init-syntax-table 51,1168
(defun isar-init-output-syntax-table 59,1415
(defconst isar-keyword-begin 74,1857
(defconst isar-keyword-end 75,1895
(defconst isar-keywords-theory-enclose77,1930
(defconst isar-keywords-theory82,2068
(defconst isar-keywords-save87,2199
(defconst isar-keywords-proof-enclose92,2314
(defconst isar-keywords-proof98,2475
(defconst isar-keywords-proof-context105,2652
(defconst isar-keywords-local-goal109,2759
(defconst isar-keywords-proper113,2864
(defconst isar-keywords-improper118,2983
(defconst isar-keyword-level-alist123,3115
(defconst isar-keywords-outline 138,3586
(defconst isar-keywords-indent-open141,3662
(defconst isar-keywords-indent-close148,3848
(defconst isar-keywords-indent-enclose153,3981
(defconst isar-ext-first 163,4210
(defconst isar-ext-rest 164,4277
(defconst isar-text 166,4349
(defconst isar-long-id-stuff 167,4382
(defconst isar-id 168,4456
(defconst isar-idx 169,4526
(defconst isar-string 171,4585
(defun isar-ids-to-regexp 173,4645
(defconst isar-any-command-regexp205,6437
(defconst isar-name-regexp212,6810
(defconst isar-improper-regexp218,7105
(defconst isar-save-command-regexp222,7239
(defconst isar-global-save-command-regexp225,7340
(defconst isar-goal-command-regexp228,7454
(defconst isar-local-goal-command-regexp231,7562
(defconst isar-comment-start 234,7675
(defconst isar-comment-end 235,7710
(defconst isar-comment-start-regexp 236,7743
(defconst isar-comment-end-regexp 237,7814
(defconst isar-string-start-regexp 239,7882
(defconst isar-string-end-regexp 240,7934
(defun isar-syntactic-context 242,7985
(defconst isar-antiq-regexp257,8380
(defconst isar-nesting-regexp263,8531
(defun isar-nesting 266,8629
(defun isar-match-nesting 278,9022
(defface isabelle-string-face 290,9356
(defface isabelle-quote-face 298,9556
(defface isabelle-class-name-face306,9752
(defface isabelle-tfree-name-face314,9939
(defface isabelle-tvar-name-face322,10132
(defface isabelle-free-name-face330,10324
(defface isabelle-bound-name-face338,10512
(defface isabelle-var-name-face346,10703
(defconst isabelle-string-face 354,10894
(defconst isabelle-quote-face 355,10948
(defconst isabelle-class-name-face 356,11001
(defconst isabelle-tfree-name-face 357,11063
(defconst isabelle-tvar-name-face 358,11125
(defconst isabelle-free-name-face 359,11186
(defconst isabelle-bound-name-face 360,11247
(defconst isabelle-var-name-face 361,11309
(defun isar-font-lock-fontify-syntactically-region 367,11458
(defvar isar-font-lock-keywords-1402,12736
(defun isar-output-flkprops 420,13744
(defun isar-output-flk 426,13996
(defvar isar-output-font-lock-keywords-1429,14105
(defun isar-strip-output-markup 453,15104
(defconst isar-shell-font-lock-keywords457,15240
(defvar isar-goals-font-lock-keywords460,15324
(defconst isar-linear-undo 494,16003
(defconst isar-undo 496,16046
(defconst isar-pr498,16089
(defun isar-remove 505,16247
(defun isar-undos 508,16322
(defun isar-cannot-undo 518,16556
(defconst isar-undo-commands521,16626
(defconst isar-theory-start-regexp529,16763
(defconst isar-end-regexp535,16921
(defconst isar-undo-fail-regexp539,17022
(defconst isar-undo-skip-regexp543,17126
(defconst isar-undo-ignore-regexp546,17247
(defconst isar-undo-remove-regexp549,17312
(defconst isar-keywords-imenu557,17469
(defconst isar-entity-regexp 564,17660
(defconst isar-named-entity-regexp567,17756
(defconst isar-named-entity-name-match-number572,17886
(defconst isar-generic-expression575,17987
(defconst isar-indent-any-regexp586,18221
(defconst isar-indent-inner-regexp588,18314
(defconst isar-indent-enclose-regexp590,18380
(defconst isar-indent-open-regexp592,18496
(defconst isar-indent-close-regexp594,18606
(defconst isar-outline-regexp600,18743
(defconst isar-outline-heading-end-regexp 604,18896
(defconst isar-outline-heading-alist 606,18945

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,534
(defcustom lego-test-all-name 26,670
(defpgdefault help-menu-entries32,828
(defpgdefault menu-entries36,988
(defvar lego-shell-handle-output47,1289
(defconst lego-process-config55,1587
(defconst lego-pretty-set-width 66,2018
(defconst lego-interrupt-regexp 70,2160
(defcustom lego-www-home-page 75,2277
(defcustom lego-www-latest-release80,2401
(defcustom lego-www-refcard86,2576
(defcustom lego-library-www-page92,2725
(defvar lego-prog-name 101,2941
(defvar lego-shell-cd 104,3010
(defvar lego-shell-proof-completed-regexp 107,3109
(defvar lego-save-command-regexp110,3249
(defvar lego-goal-command-regexp112,3339
(defvar lego-kill-goal-command 115,3430
(defvar lego-forget-id-command 116,3473
(defvar lego-undoable-commands-regexp118,3519
(defvar lego-goal-regexp 127,3893
(defvar lego-outline-regexp129,3938
(defvar lego-outline-heading-end-regexp 135,4113
(defvar lego-shell-outline-regexp 137,4166
(defvar lego-shell-outline-heading-end-regexp 138,4218
(define-derived-mode lego-shell-mode 144,4497
(define-derived-mode lego-mode 151,4658
(define-derived-mode lego-goals-mode 162,4968
(defun lego-count-undos 173,5394
(defun lego-goal-command-p 192,6131
(defun lego-find-and-forget 197,6302
(defun lego-goal-hyp 239,8138
(defun lego-state-preserving-p 248,8335
(defvar lego-shell-current-line-width 264,9038
(defun lego-shell-adjust-line-width 272,9345
(defun lego-mode-config 289,10046
(defun lego-equal-module-filename 357,12097
(defun lego-shell-compute-new-files-list 363,12372
(defun lego-shell-mode-config 373,12755
(defun lego-goals-mode-config 420,14422

lego/lego-syntax.el,600
(defconst lego-keywords-goal 15,358
(defconst lego-keywords-save 17,401
(defconst lego-commands19,472
(defconst lego-keywords31,1030
(defconst lego-tacticals 36,1207
(defconst lego-error-regexp 39,1315
(defvar lego-id 42,1473
(defvar lego-ids 44,1500
(defconst lego-arg-list-regexp 48,1696
(defun lego-decl-defn-regexp 51,1812
(defconst lego-definiendum-alternative-regexp59,2184
(defvar lego-font-lock-terms63,2368
(defconst lego-goal-with-hole-regexp89,3221
(defconst lego-save-with-hole-regexp94,3443
(defvar lego-font-lock-keywords-199,3660
(defun lego-init-syntax-table 110,4122

phox/phox.el,555
(defcustom phox-prog-name 32,916
(defcustom phox-web-page37,1018
(defcustom phox-doc-dir43,1168
(defcustom phox-lib-dir49,1315
(defcustom phox-tags-program55,1458
(defcustom phox-tags-doc61,1637
(defcustom phox-etags67,1774
(defpgdefault menu-entries88,2224
(defun phox-config 102,2417
(defun phox-shell-config 146,4343
(define-derived-mode phox-mode 170,5205
(define-derived-mode phox-shell-mode 186,5668
(define-derived-mode phox-response-mode 191,5796
(define-derived-mode phox-goals-mode 201,6157
(defpgdefault completion-table224,6943

phox/phox-extraction.el,383
(defvar phox-prog-orig 19,619
(defun phox-prog-flags-modify(21,687
(defun phox-prog-flags-extract(50,1488
(defun phox-prog-flags-erase(61,1778
(defun phox-toggle-extraction(69,1974
(defun phox-compile-theorem(81,2376
(defun phox-compile-theorem-on-cursor(87,2601
(defun phox-output 103,3079
(defun phox-output-theorem 113,3291
(defun phox-output-theorem-on-cursor(120,3590

phox/phox-font.el,231
(defvar phox-sym-lock-enabled 1,0
(defvar phox-sym-lock-color 2,60
(defvar phox-sym-lock-keywords 3,118
(defconst phox-font-lock-keywords11,511
(defconst phox-sym-lock-keywords-table70,2628
(defun phox-sym-lock-start 93,3202

phox/phox-fun.el,1659
(defconst phox-forget-id-command 11,186
(defconst phox-forget-proof-command 12,232
(defconst phox-forget-new-elim-command 13,287
(defconst phox-forget-new-intro-command 14,345
(defconst phox-forget-new-equation-command 15,405
(defconst phox-forget-close-def-command 16,471
(defconst phox-comments-regexp 18,597
(defconst phox-strict-comments-regexp 20,776
(defconst phox-ident-regexp 21,941
(defconst phox-inductive-option 22,1027
(defconst phox-spaces-regexp 23,1079
(defconst phox-sy-definition-regexp 24,1122
(defconst phox-sy-inductive-regexp 28,1309
(defconst phox-inductive-regexp 34,1522
(defconst phox-data-regexp 40,1673
(defconst phox-definition-regexp 46,1827
(defconst phox-prove-claim-regexp 50,1971
(defconst phox-new-elim-regexp 54,2077
(defconst phox-new-intro-regexp 57,2196
(defconst phox-new-rewrite-regexp 60,2317
(defconst phox-new-equation-regexp 63,2442
(defconst phox-close-def-regexp 66,2569
(defun phox-init-syntax-table 71,2706
(defvar phox-top-keywords87,3178
(defvar phox-proof-keywords135,3633
(defun phox-find-and-forget 176,3983
(defalias 'phox-assert-next-command-interactive phox-assert-next-command-interactive
255,6399
(defun phox-depend-theorem(274,7365
(defun phox-eshow-extlist(283,7654
(defun phox-flag-name(297,8251
(defun phox-path(308,8553
(defun phox-print-expression(319,8789
(defun phox-print-sort-expression(332,9245
(defun phox-priority-symbols-list(343,9557
(defun phox-search-string(355,9929
(defun phox-constraints(370,10454
(defun phox-goals(381,10710
(defvar phox-state-menu393,10919
(defun phox-delete-symbol(418,11909
(defun phox-delete-symbol-on-cursor(424,12117

phox/phox-lang.el,323
(defvar phox-lang9,306
(defun phox-lang-absurd 17,535
(defun phox-lang-suppress 22,629
(defun phox-lang-opendef 27,826
(defun phox-lang-instance 32,944
(defun phox-lang-open-instance 37,1073
(defun phox-lang-lock 42,1222
(defun phox-lang-unlock 47,1352
(defun phox-lang-prove 52,1488
(defun phox-lang-let 57,1622

phox/phox-outline.el,254
(defconst phox-outline-title-regexp 20,745
(defconst phox-outline-section-regexp 21,810
(defconst phox-outline-save-regexp 22,866
(defconst phox-outline-heading-end-regexp 39,1409
(defun phox-outline-level(45,1584
(defun phox-setup-outline 59,2058

phox/phox-pbrpm.el,513
(defun phox-pbrpm-left-paren-p 39,1671
(defun phox-pbrpm-right-paren-p 46,1874
(defun phox-pbrpm-menu-from-string 54,2078
(defun phox-pbrpm-rename-in-cmd 63,2410
(defun phox-pbrpm-get-region-name 96,3658
(defun  phox-pbrpm-escape-string 99,3785
(defun phox-pbrpm-generate-menu 103,3920
(defalias 'proof-pbrpm-generate-menu proof-pbrpm-generate-menu
310,11400
(defalias 'proof-pbrpm-left-paren-p proof-pbrpm-left-paren-p
311,11464
(defalias 'proof-pbrpm-right-paren-p proof-pbrpm-right-paren-p
312,11526

phox/phox-sym-lock.el,1398
(defcustom phox-sym-lock-enabled 19,871
(defvar phox-sym-lock-sym-count 59,2452
(defvar phox-sym-lock-ext-start 62,2522
(defvar phox-sym-lock-ext-end 64,2644
(defvar phox-sym-lock-font-size 67,2763
(defvar phox-sym-lock-keywords 72,2953
(defvar phox-sym-lock-enabled 77,3129
(defvar phox-sym-lock-color 82,3291
(defvar phox-sym-lock-mouse-face 87,3509
(defvar phox-sym-lock-mouse-face-enabled 92,3699
(defconst phox-sym-lock-with-mule 97,3889
(defun phox-sym-lock-gen-symbol 100,3973
(defun phox-sym-lock-make-symbols-atomic 108,4275
(defun phox-sym-lock-compute-font-size 135,5216
(defvar phox-sym-lock-font-name173,6635
(defun phox-sym-lock-set-foreground 216,8233
(defun phox-sym-lock-translate-char 230,8842
(defun phox-sym-lock-translate-char-or-string 239,9159
(defun phox-sym-lock-remap-face 246,9387
(defvar phox-sym-lock-clear-face266,10375
(defun phox-sym-lock 278,10794
(defun phox-sym-lock-rec 287,11198
(defun phox-sym-lock-atom-face 293,11343
(defun phox-sym-lock-pre-idle-hook-first 298,11639
(defun phox-sym-lock-pre-idle-hook-last 308,12044
(defun phox-sym-lock-enable 317,12419
(defun phox-sym-lock-disable 330,12830
(defun phox-sym-lock-mouse-face-enable 343,13246
(defun phox-sym-lock-mouse-face-disable 350,13461
(defun phox-sym-lock-font-lock-hook 357,13680
(defun font-lock-set-defaults 372,14371
(defun phox-sym-lock-patch-keywords 384,14798

phox/phox-tags.el,305
(defun phox-tags-add-table(26,869
(defun phox-tags-reset-table(35,1264
(defun phox-tags-add-doc-table(40,1374
(defun phox-tags-add-lib-table(46,1523
(defun phox-tags-add-local-table(52,1658
(defun phox-tags-create-local-table(58,1841
(defun phox-complete-tag(69,2091
(defvar phox-tags-menu76,2200

generic/pg-assoc.el,81
(defun proof-associated-buffers 33,973
(defun proof-associated-windows 43,1183

generic/pg-autotest.el,908
(defvar pg-autotest-success 29,690
(defvar pg-autotest-log 32,777
(defun pg-autotest-find-file 37,871
(defun pg-autotest-find-file-restart 44,1137
(defmacro pg-autotest-apply 58,1611
(defmacro pg-autotest 72,2026
(defun pg-autotest-log 89,2463
(defun pg-autotest-message 98,2726
(defun pg-autotest-remark 107,3015
(defun pg-autotest-timestart 110,3096
(defun pg-autotest-timetaken 115,3279
(defun pg-autotest-start 129,3667
(defun pg-autotest-exit 140,4121
(defun pg-autotest-test-process-wholefile 160,4904
(defun pg-autotest-test-script-wholefile 168,5191
(defun pg-autotest-test-script-randomjumps 193,6123
(defun pg-autotest-test-retract-file 242,7680
(defun pg-autotest-test-assert-processed 248,7821
(defun pg-autotest-test-assert-full 254,8047
(defun pg-autotest-test-assert-unprocessed 261,8288
(defun pg-autotest-test-eval 268,8553
(defun pg-autotest-test-quit-prover 272,8652

generic/pg-custom.el,635
(defpgcustom script-indent 37,1199
(defconst proof-toolbar-entries-default42,1336
(defpgcustom toolbar-entries 70,3069
(defpgcustom prog-args 89,3802
(defpgcustom prog-env 101,4380
(defpgcustom quit-timeout 110,4809
(defpgcustom favourites 122,5236
(defpgcustom menu-entries 127,5425
(defpgcustom help-menu-entries 134,5661
(defpgcustom keymap 141,5924
(defpgcustom completion-table 146,6095
(defpgcustom tags-program 157,6471
(defpgcustom use-holes 166,6855
(defpgcustom one-command-per-line173,7113
(defpgcustom maths-menu-enable 184,7349
(defpgcustom unicode-tokens-enable 190,7529
(defpgcustom mmm-enable 196,7736

generic/pg-goals.el,285
(define-derived-mode proof-goals-mode 29,734
(define-key proof-goals-mode-map 56,1592
(define-key proof-goals-mode-map 58,1708
(define-key proof-goals-mode-map 59,1776
(defun proof-goals-config-done 68,1923
(defun pg-goals-display 76,2189
(defun pg-goals-button-action 117,3493

generic/pg-movie.el,334
(defconst pg-movie-xml-header 33,944
(defconst pg-movie-stylesheet35,1002
(defun pg-movie-stylesheet-location 38,1101
(defvar pg-movie-frame 42,1209
(defun pg-movie-of-span 44,1263
(defun pg-movie-of-region 80,2383
(defun pg-movie-export 87,2571
(defun pg-movie-export-from 109,3175
(defun pg-movie-export-directory 120,3496

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,1207
(defvar pg-pbrpm-start-goal-regexp 48,1329
(defvar pg-pbrpm-start-goal-regexp-par-num 52,1486
(defvar pg-pbrpm-end-goal-regexp 55,1609
(defvar pg-pbrpm-start-hyp-regexp 59,1761
(defvar pg-pbrpm-start-hyp-regexp-par-num 63,1922
(defvar pg-pbrpm-start-concl-regexp 67,2129
(defvar pg-pbrpm-auto-select-regexp 71,2293
(defvar pg-pbrpm-buffer-menu 78,2454
(defvar pg-pbrpm-spans 79,2488
(defvar pg-pbrpm-goal-description 80,2516
(defvar pg-pbrpm-windows-dialog-bug 81,2555
(defvar pbrpm-menu-desc 82,2596
(defun pg-pbrpm-erase-buffer-menu 84,2626
(defun pg-pbrpm-menu-change-hook 90,2798
(defun pg-pbrpm-create-reset-buffer-menu 108,3373
(defun pg-pbrpm-analyse-goal-buffer 127,4215
(defun pg-pbrpm-button-action 187,6620
(defun pg-pbrpm-exists 194,6846
(defun pg-pbrpm-eliminate-id 198,6958
(defun pg-pbrpm-build-menu 206,7204
(defun pg-pbrpm-setup-span 269,9524
(defun pg-pbrpm-run-command 329,11823
(defun pg-pbrpm-get-pos-info 362,13348
(defun pg-pbrpm-get-region-info 404,14647
(defun pg-pbrpm-auto-select-around-point 415,15059
(defun pg-pbrpm-translate-position 430,15583
(defun pg-pbrpm-process-click 438,15837
(defvar pg-pbrpm-remember-region-selected-region 458,16862
(defvar pg-pbrpm-regions-list 459,16916
(defun pg-pbrpm-erase-regions-list 461,16952
(defun pg-pbrpm-filter-regions-list 470,17260
(defface pg-pbrpm-multiple-selection-face477,17523
(defface pg-pbrpm-menu-input-face485,17725
(defun pg-pbrpm-do-remember-region 493,17915
(defun pg-pbrpm-remember-region-drag-up-hook 514,18763
(defun pg-pbrpm-remember-region-click-hook 518,18934
(defun pg-pbrpm-remember-region 523,19119
(defun pg-pbrpm-process-region 537,19833
(defun pg-pbrpm-process-regions-list 555,20562
(defun pg-pbrpm-region-expression 559,20745

generic/pg-pgip.el,2931
(defalias 'pg-pgip-debug pg-pgip-debug
38,1032
(defalias 'pg-pgip-error pg-pgip-error
39,1073
(defalias 'pg-pgip-warning pg-pgip-warning
40,1108
(defconst pg-pgip-version-supported 42,1158
(defun pg-pgip-process-packet 46,1264
(defvar pg-pgip-last-seen-id 56,1832
(defvar pg-pgip-last-seen-seq 57,1866
(defun pg-pgip-process-pgip 59,1902
(defun pg-pgip-process-msg 78,2842
(defvar pg-pgip-post-process-functions93,3433
(defun pg-pgip-post-process 103,3908
(defun pg-pgip-process-askpgip 120,4523
(defun pg-pgip-process-usespgip 126,4727
(defun pg-pgip-process-usespgml 130,4891
(defun pg-pgip-process-pgmlconfig 134,5055
(defun pg-pgip-process-proverinfo 150,5672
(defun pg-pgip-process-hasprefs 167,6337
(defun pg-pgip-haspref 181,6969
(defun pg-pgip-process-prefval 199,7685
(defun pg-pgip-process-guiconfig 226,8393
(defvar proof-assistant-idtables 233,8510
(defun pg-pgip-process-ids 236,8627
(defun pg-complete-idtable-symbol 262,9699
(defalias 'pg-pgip-process-setids pg-pgip-process-setids
267,9791
(defalias 'pg-pgip-process-addids pg-pgip-process-addids
268,9847
(defalias 'pg-pgip-process-delids pg-pgip-process-delids
269,9903
(defun pg-pgip-process-idvalue 272,9961
(defun pg-pgip-process-menuadd 284,10307
(defun pg-pgip-process-menudel 287,10350
(defun pg-pgip-process-ready 296,10582
(defun pg-pgip-process-cleardisplay 299,10623
(defun pg-pgip-process-proofstate 313,11080
(defun pg-pgip-process-normalresponse 317,11157
(defun pg-pgip-process-errorresponse 321,11287
(defun pg-pgip-process-scriptinsert 325,11416
(defun pg-pgip-process-metainforesponse 330,11550
(defun pg-pgip-file-of-url 339,11790
(defun pg-pgip-process-informfileloaded 344,11925
(defun pg-pgip-process-informfileretracted 350,12157
(defun pg-pgip-process-brokerstatus 363,12604
(defun pg-pgip-process-proveravailmsg 366,12652
(defun pg-pgip-process-newprovermsg 369,12702
(defun pg-pgip-process-proverstatusmsg 372,12750
(defvar pg-pgip-srcids 381,12996
(defun pg-pgip-process-newfile 385,13103
(defun pg-pgip-process-filestatus 401,13685
(defun pg-pgip-process-newobj 421,14339
(defun pg-pgip-process-delobj 424,14381
(defun pg-pgip-process-objectstatus 427,14423
(defun pg-pgip-process-parsescript 441,14775
(defun pg-pgip-get-pgiptype 464,15649
(defun pg-pgip-default-for 485,16512
(defun pg-pgip-subst-for 498,16907
(defun pg-pgip-interpret-value 511,17277
(defun pg-pgip-interpret-choice 530,18002
(defun pg-pgip-string-of-command 561,19019
(defconst pg-pgip-id578,19780
(defvar pg-pgip-refseq 584,20060
(defvar pg-pgip-refid 586,20157
(defvar pg-pgip-seq 589,20249
(defun pg-pgip-assemble-packet 591,20313
(defun pg-pgip-issue 609,21124
(defun pg-pgip-maybe-askpgip 626,21736
(defun pg-pgip-askprefs 632,21927
(defun pg-pgip-askids 636,22041
(defun pg-pgip-reset 649,22329
(defconst pg-pgip-start-element-regexp 680,23027
(defconst pg-pgip-end-element-regexp 681,23079

generic/pg-response.el,1252
(deflocal pg-response-eagerly-raise 32,788
(define-derived-mode proof-response-mode 42,1013
(define-key proof-response-mode-map 69,1950
(define-key proof-response-mode-map 70,2021
(define-key proof-response-mode-map 71,2075
(defun proof-response-config-done 75,2161
(defvar pg-response-special-display-regexp 86,2507
(defconst proof-multiframe-parameters90,2674
(defun proof-multiple-frames-enable 99,2964
(defun proof-three-window-enable 109,3292
(defun proof-select-three-b 112,3355
(defun proof-display-three-b 127,3846
(defvar pg-frame-configuration 138,4236
(defun pg-cache-frame-configuration 142,4383
(defun proof-layout-windows 146,4554
(defun proof-delete-other-frames 186,6341
(defvar pg-response-erase-flag 217,7429
(defun pg-response-maybe-erase221,7558
(defun pg-response-display 251,8662
(defun pg-response-display-with-face 276,9445
(defun pg-response-clear-displays 304,10291
(defun pg-response-message 322,10997
(defun pg-response-warning 328,11232
(defun proof-next-error 343,11638
(defun pg-response-has-error-location 421,14447
(defcustom proof-trace-buffer-max-lines 436,14866
(defun proof-trace-buffer-display 443,15101
(defun proof-trace-buffer-finish 457,15508
(defun pg-thms-buffer-clear 481,16161

generic/pg-user.el,3635
(defun proof-script-new-command-advance 43,1232
(defun proof-maybe-follow-locked-end 67,2157
(defun proof-goto-command-start 93,2993
(defun proof-goto-command-end 116,3940
(defun proof-forward-command 131,4362
(defun proof-backward-command 152,5083
(defun proof-goto-point 163,5297
(defun proof-assert-next-command-interactive 177,5731
(defun proof-assert-until-point-interactive 189,6217
(defun proof-process-buffer 195,6447
(defun proof-undo-last-successful-command 213,6959
(defun proof-undo-and-delete-last-successful-command 218,7121
(defun proof-undo-last-successful-command-1 230,7640
(defun proof-retract-buffer 247,8304
(defun proof-retract-current-goal 256,8588
(defun proof-mouse-goto-point 275,9108
(defvar proof-minibuffer-history 290,9384
(defun proof-minibuffer-cmd 293,9479
(defun proof-frob-locked-end 332,10886
(defmacro proof-if-setting-configured 368,11987
(defmacro proof-define-assistant-command 376,12256
(defmacro proof-define-assistant-command-witharg 389,12711
(defun proof-issue-new-command 409,13533
(defun proof-cd-sync 449,14756
(defun proof-electric-terminator-enable 500,16355
(defun proof-electric-terminator 508,16659
(defun proof-add-completions 536,17629
(defun proof-script-complete 559,18452
(defun pg-copy-span-contents 573,18761
(defun pg-numth-span-higher-or-lower 587,19185
(defun pg-control-span-of 613,19931
(defun pg-move-span-contents 619,20135
(defun pg-fixup-children-spans 670,22253
(defun pg-move-region-down 680,22510
(defun pg-move-region-up 689,22803
(defun pg-pos-for-event 703,23077
(defun pg-span-for-event 709,23298
(defun pg-span-context-menu 713,23442
(defun pg-toggle-visibility 729,23959
(defun pg-create-in-span-context-menu 738,24266
(defun pg-span-undo 763,25294
(defun pg-goals-buffers-hint 776,25532
(defun pg-slow-fontify-tracing-hint 780,25750
(defun pg-response-buffers-hint 784,25939
(defun pg-jump-to-end-hint 796,26354
(defun pg-processing-complete-hint 800,26483
(defun pg-next-error-hint 817,27203
(defun pg-hint 822,27355
(defun pg-identifier-under-mouse-query 833,27704
(defun pg-identifier-near-point-query 844,28028
(defvar proof-query-identifier-history 873,28951
(defun proof-query-identifier 876,29038
(defun pg-identifier-query 887,29394
(defun proof-imenu-enable 920,30542
(defvar pg-input-ring 956,31845
(defvar pg-input-ring-index 959,31902
(defvar pg-stored-incomplete-input 962,31974
(defun pg-previous-input 965,32077
(defun pg-next-input 979,32540
(defun pg-delete-input 984,32662
(defun pg-get-old-input 997,33000
(defun pg-restore-input 1011,33391
(defun pg-search-start 1022,33681
(defun pg-regexp-arg 1034,34173
(defun pg-search-arg 1046,34621
(defun pg-previous-matching-input-string-position 1060,35038
(defun pg-previous-matching-input 1087,36203
(defun pg-next-matching-input 1106,37053
(defvar pg-matching-input-from-input-string 1114,37436
(defun pg-previous-matching-input-from-input 1118,37550
(defun pg-next-matching-input-from-input 1136,38315
(defun pg-add-to-input-history 1147,38694
(defun pg-remove-from-input-history 1159,39147
(defun  pg-clear-input-ring 1170,39527
(define-key proof-mode-map 1187,39997
(define-key proof-mode-map 1188,40057
(defun pg-protected-undo 1190,40129
(defun pg-protected-undo-1 1220,41423
(defun next-undo-elt 1251,42860
(defvar proof-autosend-timer 1278,43816
(deflocal proof-autosend-modified-tick 1280,43877
(defun proof-autosend-enable 1284,43999
(defun proof-autosend-delay 1298,44542
(defun proof-autosend-loop 1302,44675
(defun proof-autosend-loop-all 1316,45235
(defun proof-autosend-loop-next 1340,46015

generic/pg-vars.el,1500
(defvar proof-assistant-cusgrp 22,388
(defvar proof-assistant-internals-cusgrp 28,648
(defvar proof-assistant 34,918
(defvar proof-assistant-symbol 39,1141
(defvar proof-mode-for-shell 52,1683
(defvar proof-mode-for-response 57,1873
(defvar proof-mode-for-goals 62,2099
(defvar proof-mode-for-script 67,2288
(defvar proof-ready-for-assistant-hook 72,2465
(defvar proof-shell-busy 83,2753
(defvar proof-shell-last-queuemode 101,3424
(defvar proof-included-files-list 105,3579
(defvar proof-script-buffer 127,4598
(defvar proof-previous-script-buffer 130,4690
(defvar proof-shell-buffer 134,4863
(defvar proof-goals-buffer 137,4949
(defvar proof-response-buffer 140,5004
(defvar proof-trace-buffer 143,5065
(defvar proof-thms-buffer 147,5219
(defvar proof-shell-error-or-interrupt-seen 151,5374
(defvar pg-response-next-error 156,5598
(defvar proof-shell-proof-completed 159,5705
(defvar proof-shell-silent 173,6090
(defvar proof-shell-last-prompt 176,6178
(defvar proof-shell-last-output 180,6348
(defvar proof-shell-last-output-kind 184,6488
(defvar proof-assistant-settings 204,7252
(defvar pg-tracing-slow-mode 214,7766
(defvar proof-nesting-depth 217,7855
(defvar proof-last-theorem-dependencies 224,8090
(defvar proof-autosend-running 228,8252
(defvar proof-next-command-on-new-line 233,8451
(defcustom proof-general-name 244,8685
(defcustom proof-general-home-page249,8842
(defcustom proof-unnamed-theorem-name255,9002
(defcustom proof-universal-keys261,9186

generic/pg-xml.el,1177
(defalias 'pg-xml-error pg-xml-error
18,381
(defun pg-xml-parse-string 41,1023
(defun pg-xml-parse-buffer 51,1335
(defun pg-xml-get-attr 70,1950
(defun pg-xml-child-elts 78,2252
(defun pg-xml-child-elt 83,2457
(defun pg-xml-get-child 91,2739
(defun pg-xml-get-text-content 101,3106
(defmacro pg-xml-attr 112,3456
(defmacro pg-xml-node 114,3518
(defconst pg-xml-header117,3610
(defun pg-xml-string-of 121,3686
(defun pg-xml-output-internal 132,4053
(defun pg-xml-cdata 166,5192
(defsubst pg-pgip-get-area 174,5385
(defun pg-pgip-get-icon 177,5502
(defsubst pg-pgip-get-name 181,5650
(defsubst pg-pgip-get-version 184,5767
(defsubst pg-pgip-get-descr 187,5890
(defsubst pg-pgip-get-thmname 190,6009
(defsubst pg-pgip-get-thyname 193,6132
(defsubst pg-pgip-get-url 196,6255
(defsubst pg-pgip-get-srcid 199,6370
(defsubst pg-pgip-get-proverid 202,6489
(defsubst pg-pgip-get-symname 205,6614
(defsubst pg-pgip-get-prefcat 208,6734
(defsubst pg-pgip-get-default 211,6862
(defsubst pg-pgip-get-objtype 214,6985
(defsubst pg-pgip-get-value 217,7108
(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext
220,7178
(defun pg-pgip-get-pgmltext 222,7237

generic/proof-autoloads.el,97
(defsubst proof-shell-live-buffer 722,23445
(defsubst proof-replace-regexp-in-string 875,28925

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,7741
(defgroup prover-config 80,2632
(defcustom proof-guess-command-line 98,3482
(defcustom proof-assistant-home-page 113,3977
(defcustom proof-context-command 119,4147
(defcustom proof-info-command 124,4281
(defcustom proof-showproof-command 131,4552
(defcustom proof-goal-command 136,4688
(defcustom proof-save-command 144,4985
(defcustom proof-find-theorems-command 152,5294
(defcustom proof-query-identifier-command 159,5602
(defcustom proof-assistant-true-value 173,6291
(defcustom proof-assistant-false-value 179,6481
(defcustom proof-assistant-format-int-fn 185,6675
(defcustom proof-assistant-format-float-fn 192,6924
(defcustom proof-assistant-format-string-fn 199,7179
(defcustom proof-assistant-setting-format 206,7446
(defgroup proof-script 228,8141
(defcustom proof-terminal-string 233,8271
(defcustom proof-electric-terminator-noterminator 243,8659
(defcustom proof-script-sexp-commands 248,8831
(defcustom proof-script-command-end-regexp 259,9290
(defcustom proof-script-command-start-regexp 277,10111
(defcustom proof-script-integral-proofs 288,10574
(defcustom proof-script-fly-past-comments 303,11230
(defcustom proof-script-parse-function 308,11401
(defcustom proof-script-comment-start 326,12046
(defcustom proof-script-comment-start-regexp 337,12483
(defcustom proof-script-comment-end 345,12802
(defcustom proof-script-comment-end-regexp 357,13224
(defcustom proof-string-start-regexp 365,13537
(defcustom proof-string-end-regexp 370,13702
(defcustom proof-case-fold-search 375,13863
(defcustom proof-save-command-regexp 384,14275
(defcustom proof-save-with-hole-regexp 389,14385
(defcustom proof-save-with-hole-result 400,14760
(defcustom proof-goal-command-regexp 410,15200
(defcustom proof-goal-with-hole-regexp 418,15487
(defcustom proof-goal-with-hole-result 430,15930
(defcustom proof-non-undoables-regexp 439,16304
(defcustom proof-nested-undo-regexp 450,16759
(defcustom proof-ignore-for-undo-count 466,17471
(defcustom proof-script-imenu-generic-expression 474,17774
(defcustom proof-goal-command-p 482,18113
(defcustom proof-really-save-command-p 493,18604
(defcustom proof-completed-proof-behaviour 502,18911
(defcustom proof-count-undos-fn 530,20260
(defcustom proof-find-and-forget-fn 542,20811
(defcustom proof-forget-id-command 559,21520
(defcustom pg-topterm-goalhyplit-fn 569,21878
(defcustom proof-kill-goal-command 581,22413
(defcustom proof-undo-n-times-cmd 595,22917
(defcustom proof-nested-goals-history-p 609,23454
(defcustom proof-arbitrary-undo-positions 618,23791
(defcustom proof-state-preserving-p 632,24372
(defcustom proof-activate-scripting-hook 642,24844
(defcustom proof-deactivate-scripting-hook 661,25625
(defcustom proof-no-fully-processed-buffer 670,25955
(defcustom proof-script-evaluate-elisp-comment-regexp 681,26453
(defcustom proof-indent 699,27039
(defcustom proof-indent-hang 704,27146
(defcustom proof-indent-enclose-offset 709,27272
(defcustom proof-indent-open-offset 714,27414
(defcustom proof-indent-close-offset 719,27551
(defcustom proof-indent-any-regexp 724,27689
(defcustom proof-indent-inner-regexp 729,27849
(defcustom proof-indent-enclose-regexp 734,28003
(defcustom proof-indent-open-regexp 739,28157
(defcustom proof-indent-close-regexp 744,28309
(defcustom proof-script-font-lock-keywords 750,28463
(defcustom proof-script-syntax-table-entries 758,28815
(defcustom proof-script-span-context-menu-extensions 776,29211
(defgroup proof-shell 802,29971
(defcustom proof-prog-name 812,30141
(defcustom proof-shell-auto-terminate-commands 824,30608
(defcustom proof-shell-pre-sync-init-cmd 833,31013
(defcustom proof-shell-init-cmd 847,31571
(defcustom proof-shell-init-hook 859,32117
(defcustom proof-shell-restart-cmd 864,32256
(defcustom proof-shell-quit-cmd 869,32411
(defcustom proof-shell-cd-cmd 874,32578
(defcustom proof-shell-start-silent-cmd 891,33249
(defcustom proof-shell-stop-silent-cmd 900,33625
(defcustom proof-shell-silent-threshold 909,33960
(defcustom  proof-shell-inform-file-processed-cmd 917,34294
(defcustom  proof-shell-inform-file-retracted-cmd 938,35222
(defcustom proof-auto-multiple-files 966,36494
(defcustom proof-cannot-reopen-processed-files 981,37215
(defcustom proof-shell-annotated-prompt-regexp 1001,38006
(defcustom proof-shell-error-regexp 1016,38571
(defcustom proof-shell-truncate-before-error 1036,39373
(defcustom pg-next-error-regexp 1050,39912
(defcustom pg-next-error-filename-regexp 1065,40521
(defcustom pg-next-error-extract-filename 1089,41554
(defcustom proof-shell-interrupt-regexp 1096,41797
(defcustom proof-shell-proof-completed-regexp 1110,42392
(defcustom proof-shell-clear-response-regexp 1123,42900
(defcustom proof-shell-clear-goals-regexp 1135,43352
(defcustom proof-shell-start-goals-regexp 1147,43798
(defcustom proof-shell-end-goals-regexp 1156,44222
(defcustom proof-shell-eager-annotation-start 1170,44795
(defcustom proof-shell-eager-annotation-start-length 1193,45814
(defcustom proof-shell-eager-annotation-end 1204,46240
(defcustom proof-shell-strip-output-markup 1220,46915
(defcustom proof-shell-assumption-regexp 1229,47300
(defcustom proof-shell-process-file 1239,47704
(defcustom proof-shell-retract-files-regexp 1265,48780
(defcustom proof-shell-compute-new-files-list 1278,49268
(defcustom pg-special-char-regexp 1293,49835
(defcustom proof-shell-set-elisp-variable-regexp 1298,49979
(defcustom proof-shell-match-pgip-cmd 1336,51645
(defcustom proof-shell-issue-pgip-cmd 1350,52127
(defcustom proof-use-pgip-askprefs 1355,52292
(defcustom proof-shell-query-dependencies-cmd 1363,52639
(defcustom proof-shell-theorem-dependency-list-regexp 1370,52899
(defcustom proof-shell-theorem-dependency-list-split 1386,53559
(defcustom proof-shell-show-dependency-cmd 1395,53982
(defcustom proof-shell-trace-output-regexp 1417,54888
(defcustom proof-shell-thms-output-regexp 1435,55482
(defcustom proof-tokens-activate-command 1448,55865
(defcustom proof-tokens-deactivate-command 1455,56105
(defcustom proof-tokens-extra-modes 1462,56350
(defcustom proof-shell-unicode 1477,56855
(defcustom proof-shell-filename-escapes 1486,57245
(defcustom proof-shell-process-connection-type 1503,57925
(defcustom proof-shell-strip-crs-from-input 1509,58116
(defcustom proof-shell-strip-crs-from-output 1521,58599
(defcustom proof-shell-extend-queue-hook 1529,58967
(defcustom proof-shell-insert-hook 1539,59397
(defcustom proof-script-preprocess 1582,61495
(defcustom proof-shell-handle-delayed-output-hook1588,61646
(defcustom proof-shell-handle-error-or-interrupt-hook1594,61861
(defcustom proof-shell-pre-interrupt-hook1612,62607
(defcustom proof-shell-handle-output-system-specific 1620,62878
(defcustom proof-state-change-hook 1643,63851
(defcustom proof-shell-syntax-table-entries 1653,64244
(defgroup proof-goals 1671,64615
(defcustom pg-subterm-first-special-char 1676,64736
(defcustom pg-subterm-anns-use-stack 1684,65048
(defcustom pg-goals-change-goal 1693,65347
(defcustom pbp-goal-command 1698,65463
(defcustom pbp-hyp-command 1703,65619
(defcustom pg-subterm-help-cmd 1708,65781
(defcustom pg-goals-error-regexp 1715,66017
(defcustom proof-shell-result-start 1720,66177
(defcustom proof-shell-result-end 1726,66411
(defcustom pg-subterm-start-char 1732,66624
(defcustom pg-subterm-sep-char 1743,67098
(defcustom pg-subterm-end-char 1749,67277
(defcustom pg-topterm-regexp 1755,67434
(defcustom proof-goals-font-lock-keywords 1770,68034
(defcustom proof-response-font-lock-keywords 1778,68393
(defcustom proof-shell-font-lock-keywords 1786,68755
(defcustom pg-before-fontify-output-hook 1797,69269
(defcustom pg-after-fontify-output-hook 1805,69630

generic/proof-depends.el,917
(defvar proof-thm-names-of-files 25,639
(defvar proof-def-names-of-files 31,923
(defun proof-depends-module-name-for-buffer 42,1238
(defun proof-depends-module-of 52,1679
(defun proof-depends-names-in-same-file 60,1970
(defun proof-depends-process-dependencies 79,2578
(defun proof-dependency-in-span-context-menu 132,4313
(defun proof-dep-alldeps-menu 155,5203
(defun proof-dep-make-alldeps-menu 161,5429
(defun proof-dep-split-deps 179,5924
(defun proof-dep-make-submenu 198,6590
(defun proof-make-highlight-depts-menu 209,7001
(defun proof-goto-dependency 220,7309
(defun proof-show-dependency 227,7561
(defconst pg-dep-span-priority 234,7850
(defconst pg-ordinary-span-priority 235,7886
(defun proof-highlight-depcs 237,7928
(defun proof-highlight-depts 248,8394
(defun proof-depends-save-old-face 260,8904
(defun proof-depends-restore-old-face 265,9081
(defun proof-dep-unhighlight 271,9310

generic/proof-easy-config.el,192
(defconst proof-easy-config-derived-modes-table16,544
(defun proof-easy-config-define-derived-modes 23,950
(defun proof-easy-config-check-setup 52,2135
(defmacro proof-easy-config 84,3465

generic/proof-faces.el,1809
(defgroup proof-faces 29,809
(defconst pg-defface-window-systems36,989
(defmacro proof-face-specs 49,1551
(defface proof-queue-face64,2003
(defface proof-locked-face72,2281
(defface proof-declaration-name-face82,2602
(defface proof-tacticals-name-face91,2888
(defface proof-tactics-name-face100,3150
(defface proof-error-face109,3415
(defface proof-warning-face117,3636
(defface proof-eager-annotation-face126,3893
(defface proof-debug-message-face134,4111
(defface proof-boring-face142,4310
(defface proof-mouse-highlight-face150,4502
(defface proof-command-mouse-highlight-face158,4720
(defface proof-region-mouse-highlight-face166,4959
(defface proof-highlight-dependent-face174,5201
(defface proof-highlight-dependency-face182,5408
(defface proof-active-area-face190,5605
(defface proof-script-sticky-error-face198,5917
(defface proof-script-highlight-error-face206,6146
(defconst proof-face-compat-doc 218,6491
(defconst proof-queue-face 219,6571
(defconst proof-locked-face 220,6639
(defconst proof-declaration-name-face 221,6709
(defconst proof-tacticals-name-face 222,6799
(defconst proof-tactics-name-face 223,6885
(defconst proof-error-face 224,6967
(defconst proof-script-sticky-error-face 225,7035
(defconst proof-script-highlight-error-face 226,7131
(defconst proof-warning-face 227,7233
(defconst proof-eager-annotation-face 228,7305
(defconst proof-debug-message-face 229,7395
(defconst proof-boring-face 230,7479
(defconst proof-mouse-highlight-face 231,7549
(defconst proof-command-mouse-highlight-face 232,7637
(defconst proof-region-mouse-highlight-face 233,7741
(defconst proof-highlight-dependent-face 234,7843
(defconst proof-highlight-dependency-face 235,7939
(defconst proof-active-area-face 236,8037
(defconst proof-script-error-face 237,8117

generic/proof-indent.el,219
(defun proof-indent-indent 19,449
(defun proof-indent-offset 28,715
(defun proof-indent-inner-p 45,1316
(defun proof-indent-goto-prev 54,1616
(defun proof-indent-calculate 61,1949
(defun proof-indent-line 82,2708

generic/proof-maths-menu.el,83
(defun proof-maths-menu-set-global 32,906
(defun proof-maths-menu-enable 46,1357

generic/proof-menu.el,2215
(defvar proof-display-some-buffers-count 36,820
(defun proof-display-some-buffers 38,865
(defun proof-menu-define-keys 95,2992
(defun proof-menu-define-main 153,5817
(defvar proof-menu-favourites 162,6002
(defvar proof-menu-settings 165,6109
(defun proof-menu-define-specific 169,6198
(defun proof-assistant-menu-update 212,7460
(defvar proof-help-menu226,7893
(defvar proof-show-hide-menu234,8157
(defvar proof-buffer-menu245,8581
(defun proof-keep-response-history 309,10937
(defconst proof-quick-opts-menu317,11247
(defun proof-quick-opts-vars 539,20314
(defun proof-quick-opts-changed-from-defaults-p 571,21254
(defun proof-quick-opts-changed-from-saved-p 575,21359
(defun proof-set-document-centred 583,21515
(defun proof-set-non-document-centred 596,21941
(defun proof-quick-opts-save 615,22652
(defun proof-quick-opts-reset 620,22820
(defconst proof-config-menu632,23088
(defconst proof-advanced-menu639,23267
(defvar proof-menu657,23951
(defun proof-main-menu 666,24233
(defun proof-aux-menu 678,24572
(defun proof-menu-define-favourites-menu 694,24918
(defun proof-def-favourite 714,25567
(defvar proof-make-favourite-cmd-history 741,26560
(defvar proof-make-favourite-menu-history 744,26645
(defun proof-save-favourites 747,26731
(defun proof-del-favourite 752,26879
(defun proof-read-favourite 769,27435
(defun proof-add-favourite 793,28209
(defun proof-menu-define-settings-menu 820,29254
(defun proof-menu-entry-name 849,30246
(defun proof-menu-entry-for-setting 859,30596
(defun proof-settings-vars 882,31234
(defun proof-settings-changed-from-defaults-p 887,31411
(defun proof-settings-changed-from-saved-p 891,31517
(defun proof-settings-save 895,31620
(defun proof-settings-reset 900,31787
(defun proof-assistant-invisible-command-ifposs 905,31950
(defun proof-maybe-askprefs 927,32920
(defun proof-assistant-settings-cmd 943,33537
(defun proof-assistant-settings-cmds 951,33820
(defvar proof-assistant-format-table966,34262
(defun proof-assistant-format-bool 975,34688
(defun proof-assistant-format-int 978,34801
(defun proof-assistant-format-float 981,34893
(defun proof-assistant-format-string 984,34989
(defun proof-assistant-format 987,35087

generic/proof-mmm.el,70
(defun proof-mmm-set-global 43,1439
(defun proof-mmm-enable 58,1978

generic/proof-script.el,5813
(deflocal proof-active-buffer-fake-minor-mode 46,1413
(deflocal proof-script-buffer-file-name 49,1539
(deflocal pg-script-portions 56,1949
(defalias 'proof-active-buffer-fake-minor-modeproof-active-buffer-fake-minor-mode
59,2055
(defun proof-next-element-count 68,2250
(defun proof-element-id 74,2492
(defun proof-next-element-id 78,2661
(deflocal proof-locked-span 114,3965
(deflocal proof-queue-span 121,4231
(deflocal proof-overlay-arrow 130,4717
(defun proof-span-give-warning 136,4844
(defun proof-span-read-only 142,5024
(defun proof-strict-read-only 151,5397
(defsubst proof-set-queue-endpoints 161,5775
(defun proof-set-overlay-arrow 165,5916
(defsubst proof-set-locked-endpoints 176,6254
(defsubst proof-detach-queue 181,6430
(defsubst proof-detach-locked 186,6569
(defsubst proof-set-queue-start 193,6794
(defsubst proof-set-locked-end 197,6920
(defsubst proof-set-queue-end 209,7390
(defun proof-init-segmentation 220,7687
(defun proof-colour-locked 250,8938
(defun proof-colour-locked-span 257,9211
(defun proof-sticky-errors 263,9484
(defun proof-restart-buffers 276,9900
(defun proof-script-buffers-with-spans 300,10833
(defun proof-script-remove-all-spans-and-deactivate 310,11189
(defun proof-script-clear-queue-spans-on-error 314,11379
(defun proof-script-delete-spans 340,12396
(defun proof-script-delete-secondary-spans 345,12595
(defun proof-unprocessed-begin 358,12884
(defun proof-script-end 366,13138
(defun proof-queue-or-locked-end 375,13448
(defun proof-locked-region-full-p 394,14041
(defun proof-locked-region-empty-p 403,14313
(defun proof-only-whitespace-to-locked-region-p 407,14463
(defun proof-in-locked-region-p 417,14812
(defun proof-goto-end-of-locked 429,15069
(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 446,15828
(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 457,16309
(defun proof-end-of-locked-visible-p 469,16849
(defconst pg-idioms 488,17442
(defconst pg-all-idioms 491,17538
(defun pg-clear-script-portions 495,17659
(defun pg-remove-element 501,17894
(defun pg-get-element 509,18197
(defun pg-add-element 519,18512
(defun pg-invisible-prop 567,20474
(defun pg-set-element-span-invisible 572,20675
(defun pg-toggle-element-span-visibility 585,21241
(defun pg-open-invisible-span 590,21402
(defun pg-make-element-invisible 595,21573
(defun pg-make-element-visible 600,21784
(defun pg-toggle-element-visibility 605,21978
(defun pg-show-all-portions 611,22241
(defun pg-show-all-proofs 633,22985
(defun pg-hide-all-proofs 638,23113
(defun pg-add-proof-element 643,23244
(defun pg-span-name 658,24031
(defvar pg-span-context-menu-keymap691,25238
(defun pg-last-output-displayform 698,25476
(defun pg-set-span-helphighlights 721,26367
(defun proof-complete-buffer-atomic 784,28514
(defun proof-register-possibly-new-processed-file813,29784
(defun proof-query-save-this-buffer-p 859,31658
(defun proof-inform-prover-file-retracted 864,31883
(defun proof-auto-retract-dependencies 884,32734
(defun proof-unregister-buffer-file-name 938,35284
(defsubst proof-action-completed 984,37109
(defun proof-protected-process-or-retract 988,37279
(defun proof-deactivate-scripting-auto 1016,38510
(defun proof-deactivate-scripting-query-user-action 1025,38868
(defun proof-deactivate-scripting-choose-action 1069,40377
(defun proof-deactivate-scripting 1081,40762
(defun proof-activate-scripting 1178,44885
(defun proof-toggle-active-scripting 1278,49410
(defun proof-done-advancing 1317,50655
(defun proof-done-advancing-comment 1385,53152
(defun proof-done-advancing-save 1419,54538
(defun proof-make-goalsave1507,57902
(defun proof-get-name-from-goal 1525,58767
(defun proof-done-advancing-autosave 1545,59792
(defun proof-done-advancing-other 1609,62288
(defun proof-segment-up-to-parser 1638,63252
(defun proof-script-generic-parse-find-comment-end 1708,65533
(defun proof-script-generic-parse-cmdend 1717,65947
(defun proof-script-generic-parse-cmdstart 1768,67843
(defun proof-script-generic-parse-sexp 1807,69443
(defun proof-semis-to-vanillas 1819,69909
(defun proof-next-command-new-line 1872,71582
(defun proof-script-next-command-advance 1877,71788
(defun proof-assert-until-point 1896,72288
(defun proof-assert-electric-terminator 1912,72959
(defun proof-assert-semis 1956,74639
(defun proof-retract-before-change 1970,75400
(defun proof-insert-pbp-command 1993,76056
(defun proof-insert-sendback-command 2008,76559
(defun proof-done-retracting 2034,77462
(defun proof-setup-retract-action 2069,78916
(defun proof-last-goal-or-goalsave 2081,79521
(defun proof-retract-target 2105,80433
(defun proof-retract-until-point-interactive 2184,83686
(defun proof-retract-until-point 2193,84093
(define-derived-mode proof-mode 2248,86098
(defun proof-script-set-visited-file-name 2284,87480
(defun proof-script-set-buffer-hooks 2306,88493
(defun proof-script-kill-buffer-fn 2314,88911
(defun proof-config-done-related 2346,90228
(defun proof-generic-goal-command-p 2411,92713
(defun proof-generic-state-preserving-p 2416,92926
(defun proof-generic-count-undos 2425,93443
(defun proof-generic-find-and-forget 2456,94571
(defconst proof-script-important-settings2507,96343
(defun proof-config-done 2522,96889
(defun proof-setup-parsing-mechanism 2589,99054
(defun proof-setup-imenu 2613,100126
(deflocal proof-segment-up-to-cache 2650,101408
(deflocal proof-segment-up-to-cache-start 2654,101551
(deflocal proof-segment-up-to-cache-end 2655,101596
(deflocal proof-last-edited-low-watermark 2656,101639
(defun proof-segment-up-to-using-cache 2658,101687
(defun proof-segment-cache-contents-for 2686,102807
(defun proof-script-after-change-function 2703,103389
(defun proof-script-set-after-change-functions 2715,103896

generic/proof-shell.el,3700
(defvar proof-marker 34,743
(defvar proof-action-list 37,839
(defsubst proof-shell-invoke-callback 77,2385
(defvar proof-shell-last-goals-output 91,2877
(defvar proof-shell-last-response-output 94,2957
(defvar proof-shell-delayed-output-start 97,3044
(defvar proof-shell-delayed-output-end 101,3226
(defvar proof-shell-delayed-output-flags 105,3406
(defvar proof-shell-interrupt-pending 108,3531
(defvar proof-shell-exit-in-progress 113,3755
(defcustom proof-shell-active-scripting-indicator125,4100
(defun proof-shell-ready-prover 177,5684
(defsubst proof-shell-live-buffer 191,6223
(defun proof-shell-available-p 198,6443
(defun proof-grab-lock 204,6665
(defun proof-release-lock 214,7094
(defcustom proof-shell-fiddle-frames 224,7268
(defun proof-shell-set-text-representation 229,7426
(defun proof-shell-start 237,7754
(defvar proof-shell-kill-function-hooks 416,13848
(defun proof-shell-kill-function 419,13946
(defun proof-shell-clear-state 482,16148
(defun proof-shell-exit 498,16623
(defun proof-shell-bail-out 522,17557
(defun proof-shell-restart 532,18079
(defvar proof-shell-urgent-message-marker 573,19451
(defvar proof-shell-urgent-message-scanner 576,19572
(defun proof-shell-handle-error-output 580,19757
(defun proof-shell-handle-error-or-interrupt 606,20619
(defun proof-shell-error-or-interrupt-action 649,22368
(defun proof-goals-pos 676,23465
(defun proof-pbp-focus-on-first-goal 681,23676
(defsubst proof-shell-string-match-safe 693,24092
(defun proof-shell-handle-immediate-output 697,24253
(defun proof-interrupt-process 764,26860
(defun proof-shell-insert 798,28093
(defun proof-shell-action-list-item 855,30075
(defun proof-shell-set-silent 860,30317
(defun proof-shell-start-silent-item 866,30536
(defun proof-shell-clear-silent 872,30725
(defun proof-shell-stop-silent-item 878,30947
(defsubst proof-shell-should-be-silent 884,31136
(defsubst proof-shell-insert-action-item 895,31646
(defsubst proof-shell-slurp-comments 899,31821
(defun proof-add-to-queue 910,32226
(defun proof-start-queue 968,34250
(defun proof-extend-queue 980,34645
(defun proof-shell-exec-loop 999,35264
(defun proof-shell-insert-loopback-cmd 1067,37567
(defun proof-shell-process-urgent-message 1092,38731
(defun proof-shell-process-urgent-message-default 1141,40451
(defun proof-shell-process-urgent-message-trace 1157,41035
(defun proof-shell-process-urgent-message-retract 1169,41558
(defun proof-shell-process-urgent-message-elisp 1195,42688
(defun proof-shell-process-urgent-message-thmdeps 1210,43183
(defun proof-shell-strip-eager-annotations 1224,43562
(defun proof-shell-filter 1240,44062
(defun proof-shell-filter-first-command 1340,47434
(defun proof-shell-process-urgent-messages 1355,47977
(defun proof-shell-filter-manage-output 1405,49543
(defsubst proof-shell-display-output-as-response 1437,50790
(defun proof-shell-handle-delayed-output 1443,51085
(defvar pg-last-tracing-output-time 1531,54258
(defvar pg-last-trace-output-count 1534,54371
(defconst pg-slow-mode-trigger-count 1537,54456
(defconst pg-slow-mode-duration 1540,54561
(defconst pg-fast-tracing-mode-threshold 1543,54643
(defun pg-tracing-tight-loop 1546,54772
(defun pg-finish-tracing-display 1570,55804
(defun proof-shell-wait 1588,56185
(defun proof-done-invisible 1618,57396
(defun proof-shell-invisible-command 1624,57566
(defun proof-shell-invisible-cmd-get-result 1671,59158
(defun proof-shell-invisible-command-invisible-result 1683,59594
(defun pg-insert-last-output-as-comment 1703,60095
(define-derived-mode proof-shell-mode 1722,60567
(defconst proof-shell-important-settings1759,61594
(defun proof-shell-config-done 1765,61709

generic/proof-site.el,666
(defconst proof-assistant-table-default35,1207
(defconst proof-general-short-version68,2229
(defconst proof-general-version-year 74,2416
(defgroup proof-general 81,2569
(defgroup proof-general-internals 86,2677
(defun proof-home-directory-fn 99,3065
(defcustom proof-home-directory110,3437
(defcustom proof-images-directory119,3803
(defcustom proof-info-directory125,4005
(defcustom proof-assistant-table154,4982
(defcustom proof-assistants 195,6424
(defun proof-ready-for-assistant 224,7578
(defvar proof-general-configured-provers 276,9870
(defun proof-chose-prover 349,12481
(defun proofgeneral 354,12613
(defun proof-visit-example-file 363,12931

generic/proof-splash.el,991
(defcustom proof-splash-enable 34,1007
(defcustom proof-splash-time 39,1159
(defcustom proof-splash-contents47,1443
(defconst proof-splash-startup-msg91,3008
(defconst proof-splash-welcome 100,3386
(define-derived-mode proof-splash-mode 103,3490
(define-key proof-splash-mode-map 109,3664
(define-key proof-splash-mode-map 110,3716
(defsubst proof-emacs-imagep 115,3843
(defun proof-get-image 120,3968
(defvar proof-splash-timeout-conf 142,4768
(defun proof-splash-centre-spaces 145,4881
(defun proof-splash-remove-screen 172,6037
(defun proof-splash-remove-buffer 189,6693
(defvar proof-splash-seen 200,7081
(defun proof-splash-insert-contents 203,7183
(defun proof-splash-display-screen 243,8313
(defalias 'pg-about pg-about
279,9835
(defun proof-splash-message 282,9901
(defun proof-splash-timeout-waiter 295,10345
(defvar proof-splash-old-frame-title-format 308,10903
(defun proof-splash-set-frame-titles 310,10953
(defun proof-splash-unset-frame-titles 319,11268

generic/proof-syntax.el,1278
(defsubst proof-ids-to-regexp 22,516
(defsubst proof-anchor-regexp 29,754
(defconst proof-no-regexp 33,859
(defsubst proof-regexp-alt 36,950
(defsubst proof-regexp-alt-list 45,1262
(defsubst proof-re-search-forward-region 49,1397
(defsubst proof-search-forward 62,1895
(defsubst proof-replace-regexp-in-string 69,2165
(defsubst proof-re-search-forward 74,2416
(defsubst proof-re-search-backward 79,2674
(defsubst proof-re-search-forward-safe 84,2935
(defsubst proof-string-match 90,3216
(defsubst proof-string-match-safe 95,3445
(defsubst proof-stringfn-match 99,3649
(defsubst proof-looking-at 106,3912
(defsubst proof-looking-at-safe 111,4099
(defun proof-buffer-syntactic-context 120,4312
(defsubst proof-looking-at-syntactic-context-default 141,5174
(defun proof-looking-at-syntactic-context 150,5529
(defun proof-inside-comment 159,5991
(defun proof-inside-string 165,6164
(defsubst proof-replace-string 175,6363
(defsubst proof-replace-regexp 180,6567
(defsubst proof-replace-regexp-nocasefold 185,6776
(defvar proof-id 195,7064
(defsubst proof-ids 201,7284
(defun proof-zap-commas 208,7536
(defadvice font-lock-fontify-keywords-region234,8422
(defun proof-format 250,9018
(defun proof-format-filename 269,9657
(defun proof-insert 316,11059

generic/proof-toolbar.el,2332
(defun proof-toolbar-function 33,812
(defun proof-toolbar-icon 37,959
(defun proof-toolbar-enabler 41,1106
(defun proof-toolbar-make-icon 50,1308
(defun proof-toolbar-make-toolbar-items 59,1616
(defvar proof-toolbar-map 85,2477
(defun proof-toolbar-available-p 88,2576
(defun proof-toolbar-setup 98,2882
(defun proof-toolbar-enable 119,3739
(defalias 'proof-toolbar-undo proof-toolbar-undo
152,4797
(defun proof-toolbar-undo-enable-p 154,4865
(defalias 'proof-toolbar-delete proof-toolbar-delete
161,5023
(defun proof-toolbar-delete-enable-p 163,5104
(defalias 'proof-toolbar-home proof-toolbar-home
171,5286
(defalias 'proof-toolbar-next proof-toolbar-next
175,5353
(defun proof-toolbar-next-enable-p 177,5424
(defalias 'proof-toolbar-goto proof-toolbar-goto
183,5540
(defun proof-toolbar-goto-enable-p 185,5590
(defalias 'proof-toolbar-retract proof-toolbar-retract
190,5675
(defun proof-toolbar-retract-enable-p 192,5732
(defalias 'proof-toolbar-use proof-toolbar-use
198,5851
(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p
199,5903
(defalias 'proof-toolbar-restart proof-toolbar-restart
203,5984
(defalias 'proof-toolbar-goal proof-toolbar-goal
207,6049
(defalias 'proof-toolbar-qed proof-toolbar-qed
211,6107
(defun proof-toolbar-qed-enable-p 213,6156
(defalias 'proof-toolbar-state proof-toolbar-state
221,6318
(defalias 'proof-toolbar-state-enable-p proof-toolbar-state-enable-p
222,6361
(defalias 'proof-toolbar-context proof-toolbar-context
226,6440
(defalias 'proof-toolbar-context-enable-p proof-toolbar-context-enable-p
227,6486
(defalias 'proof-toolbar-command proof-toolbar-command
231,6567
(defalias 'proof-toolbar-command-enable-p proof-toolbar-command-enable-p
232,6623
(defun proof-toolbar-help 236,6728
(defalias 'proof-toolbar-find proof-toolbar-find
242,6808
(defalias 'proof-toolbar-find-enable-p proof-toolbar-find-enable-p
243,6860
(defalias 'proof-toolbar-info proof-toolbar-info
247,6935
(defalias 'proof-toolbar-info-enable-p proof-toolbar-info-enable-p
248,6990
(defalias 'proof-toolbar-visibility proof-toolbar-visibility
252,7088
(defun proof-toolbar-visibility-enable-p 254,7148
(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt
259,7262
(defun proof-toolbar-interrupt-enable-p 260,7323
(defun proof-toolbar-scripting-menu 268,7476

generic/proof-unicode-tokens.el,497
(defvar proof-unicode-tokens-initialised 31,827
(defun proof-unicode-tokens-init 34,934
(defun proof-unicode-tokens-configure 48,1436
(defun proof-unicode-tokens-mode-if-enabled 60,1882
(defun proof-unicode-tokens-set-global 66,2081
(defun proof-unicode-tokens-enable 82,2651
(defun proof-unicode-tokens-reconfigure 102,3504
(defun proof-unicode-tokens-configure-prover 128,4392
(defun proof-unicode-tokens-activate-prover 133,4573
(defun proof-unicode-tokens-deactivate-prover 140,4819

generic/proof-useropts.el,1619
(defgroup proof-user-options 21,564
(defun proof-set-value 29,743
(defcustom proof-electric-terminator-enable 62,1866
(defcustom proof-toolbar-enable 74,2398
(defcustom proof-imenu-enable 80,2571
(defcustom pg-show-hints 86,2742
(defcustom proof-shell-quiet-errors 91,2875
(defcustom proof-trace-output-slow-catchup 98,3146
(defcustom proof-strict-state-preserving 108,3643
(defcustom proof-strict-read-only 121,4252
(defcustom proof-three-window-enable 134,4831
(defcustom proof-multiple-frames-enable 153,5581
(defcustom proof-delete-empty-windows 162,5914
(defcustom proof-shrink-windows-tofit 173,6445
(defcustom proof-auto-raise-buffers 180,6717
(defcustom proof-colour-locked 187,6952
(defcustom proof-sticky-errors 195,7202
(defcustom proof-query-file-save-when-activating-scripting202,7419
(defcustom proof-prog-name-ask218,8139
(defcustom proof-prog-name-guess224,8299
(defcustom proof-tidy-response232,8564
(defcustom proof-keep-response-history246,9027
(defcustom pg-input-ring-size 256,9415
(defcustom proof-general-debug 261,9567
(defcustom proof-use-parser-cache 270,9938
(defcustom proof-follow-mode 277,10192
(defcustom proof-auto-action-when-deactivating-scripting 301,11369
(defcustom proof-rsh-command 329,12551
(defcustom proof-disappearing-proofs 345,13109
(defcustom proof-full-annotation 350,13270
(defcustom proof-output-tooltips 360,13733
(defcustom proof-minibuffer-messages 371,14240
(defcustom proof-autosend-enable 379,14549
(defcustom proof-autosend-delay 385,14729
(defcustom proof-autosend-all 391,14887
(defcustom proof-fast-process-buffer 396,15056

generic/proof-utils.el,1645
(defmacro proof-with-current-buffer-if-exists 61,1735
(defmacro proof-with-script-buffer 70,2112
(defmacro proof-map-buffers 81,2493
(defmacro proof-sym 86,2678
(defsubst proof-try-require 91,2839
(defun proof-save-some-buffers 104,3170
(defun proof-save-this-buffer 124,3766
(defun proof-file-truename 137,4130
(defun proof-files-to-buffers 141,4312
(defun proof-buffers-in-mode 149,4551
(defun pg-save-from-death 163,5001
(defun proof-define-keys 182,5617
(defun pg-remove-specials 193,5902
(defun pg-remove-specials-in-string 203,6238
(defun proof-safe-split-window-vertically 213,6463
(defun proof-warn-if-unset 218,6643
(defun proof-get-window-for-buffer 223,6861
(defun proof-display-and-keep-buffer 272,9171
(defun proof-clean-buffer 314,10894
(defun pg-internal-warning 330,11550
(defun proof-debug 338,11832
(defun proof-switch-to-buffer 353,12383
(defun proof-resize-window-tofit 375,13507
(defun proof-submit-bug-report 470,17355
(defun proof-deftoggle-fn 505,18712
(defmacro proof-deftoggle 520,19378
(defun proof-defintset-fn 531,19891
(defmacro proof-defintset 550,20715
(defun proof-deffloatset-fn 557,21094
(defmacro proof-deffloatset 573,21808
(defun proof-defstringset-fn 580,22193
(defmacro proof-defstringset 593,22819
(defun proof-escape-keymap-doc 606,23275
(defmacro proof-defshortcut 610,23429
(defmacro proof-definvisible 625,24027
(defun pg-custom-save-vars 652,24956
(defun pg-custom-reset-vars 668,25600
(defun proof-locate-executable 681,25937
(defun pg-current-word-pos 696,26487
(defsubst proof-shell-strip-output-markup 741,28142
(defun proof-minibuffer-message 747,28406

lib/bufhist.el,1257
(defun bufhist-ring-update 38,1391
(defgroup bufhist 47,1713
(defcustom bufhist-ring-size 51,1794
(defvar bufhist-ring 56,1905
(defvar bufhist-ring-pos 59,1979
(defvar bufhist-lastswitch-modified-tick 62,2058
(defvar bufhist-read-only-history 65,2164
(defvar bufhist-saved-mode-line-format 68,2235
(defvar bufhist-normal-read-only 71,2338
(defvar bufhist-top-point 74,2432
(defun bufhist-mode-line-format-entry 77,2522
(defconst bufhist-minor-mode-map106,3596
(define-minor-mode bufhist-mode119,4073
(defun bufhist-get-buffer-contents 141,4954
(defun bufhist-restore-buffer-contents 150,5296
(defun bufhist-checkpoint 159,5610
(defun bufhist-erase-buffer 167,5979
(defun bufhist-checkpoint-and-erase 178,6350
(defun bufhist-switch-to-index 184,6536
(defun bufhist-first 223,8135
(defun bufhist-last 228,8294
(defun bufhist-prev 233,8438
(defun bufhist-next 241,8661
(defun bufhist-delete 246,8801
(defun bufhist-clear 258,9342
(defun bufhist-init 273,9737
(defun bufhist-exit 301,10746
(defun bufhist-set-readwrite 311,11010
(defun bufhist-before-change-function 326,11630
(define-button-type 'bufhist-nextbufhist-next
340,12053
(define-button-type 'bufhist-prevbufhist-prev
344,12150
(defun bufhist-insert-buttons 351,12362

lib/holes.el,2465
(defvar holes-default-hole 44,1121
(defvar holes-active-hole 50,1299
(defgroup holes 60,1496
(defcustom holes-empty-hole-string 65,1595
(defcustom holes-empty-hole-regexp 70,1738
(defface active-hole-face92,2440
(defface inactive-hole-face102,2856
(defvar hole-map116,3297
(defvar holes-mode-map126,3688
(defun holes-region-beginning-or-nil 172,5425
(defun holes-region-end-or-nil 176,5561
(defun holes-copy-active-region 180,5679
(defun holes-is-hole-p 186,5889
(defun holes-hole-start-position 190,5981
(defun holes-hole-end-position 196,6164
(defun holes-hole-buffer 201,6335
(defun holes-hole-at 207,6509
(defun holes-active-hole-exist-p 212,6679
(defun holes-active-hole-start-position 219,6932
(defun holes-active-hole-end-position 227,7300
(defun holes-active-hole-buffer 236,7663
(defun holes-goto-active-hole 244,7964
(defun holes-highlight-hole-as-active 253,8223
(defun holes-highlight-hole 261,8531
(defun holes-disable-active-hole 269,8818
(defun holes-set-active-hole 282,9350
(defun holes-is-in-hole-p 292,9695
(defun holes-make-hole 296,9833
(defun holes-make-hole-at 314,10489
(defun holes-clear-hole 328,10942
(defun holes-clear-hole-at 337,11200
(defun holes-map-holes 345,11456
(defun holes-clear-all-buffer-holes 349,11610
(defun holes-next 359,11911
(defun holes-next-after-active-hole 366,12163
(defun holes-set-active-hole-next 373,12379
(defun holes-replace-segment 392,12916
(defun holes-replace 401,13269
(defun holes-replace-active-hole 429,14447
(defun holes-replace-update-active-hole 436,14738
(defun holes-delete-update-active-hole 454,15385
(defun holes-set-make-active-hole 462,15612
(defalias 'holes-track-mouse-selection holes-track-mouse-selection
477,16167
(defsubst holes-track-mouse-clicks 478,16225
(defun holes-mouse-replace-active-hole 482,16335
(defun holes-destroy-hole 496,16806
(defsubst holes-hole-at-event 510,17188
(defun holes-mouse-destroy-hole 514,17288
(defun holes-mouse-forget-hole 521,17509
(defun holes-mouse-set-make-active-hole 531,17801
(defun holes-mouse-set-active-hole 547,18300
(defun holes-set-point-next-hole-destroy 556,18551
(defun holes-replace-string-by-holes-backward 582,19532
(defun holes-skeleton-end-hook 600,20232
(defconst holes-jump-doc609,20670
(defun holes-replace-string-by-holes-backward-jump 616,20876
(define-minor-mode holes-mode 633,21558
(defun holes-abbrev-complete 728,25040
(defun holes-insert-and-expand 738,25383

lib/local-vars-list.el,373
(defconst local-vars-list-doc 28,825
(defun local-vars-list-insert-empty-zone 44,1387
(defun local-vars-list-find 82,2090
(defun local-vars-list-goto-var 101,2861
(defun local-vars-list-get-current 127,3908
(defun local-vars-list-set-current 148,4758
(defun local-vars-list-get 171,5473
(defun local-vars-list-get-safe 188,6003
(defun local-vars-list-set 193,6197

lib/maths-menu.el,242
(defvar maths-menu-filter-predicate 56,2317
(defvar maths-menu-tokenise-insert 59,2426
(defun maths-menu-build-menu 62,2563
(defvar maths-menu-menu84,3324
(defvar maths-menu-mode-map344,12882
(define-minor-mode maths-menu-mode352,13101

lib/pg-dev.el,199
(defconst pg-dev-lisp-font-lock-keywords52,1580
(defun pg-loadpath 78,2279
(defun unload-pg 88,2450
(defun profile-pg 119,3344
(defun elp-pack-number 149,4451
(defun pg-bug-references 158,4651

lib/pg-fontsets.el,209
(defcustom pg-fontsets-default-fontset 24,722
(defvar pg-fontsets-names 29,868
(defun pg-fontsets-make-fontsetsizes 32,949
(defconst pg-fontsets-base-fonts51,1710
(defun pg-fontsets-make-fontsets 57,1840

lib/proof-compat.el,160
(defvar proof-running-on-win32 32,975
(defun pg-custom-undeclare-variable 53,1777
(defmacro save-selected-frame 86,2602
(defmacro declare-function 152,4610

lib/scomint.el,788
(defvar scomint-buffer-maximum-size 19,493
(defvar scomint-output-filter-functions 24,684
(defvar scomint-mode-map27,794
(defvar scomint-last-input-start 33,973
(defvar scomint-last-input-end 34,1011
(defvar scomint-last-output-start 35,1047
(defvar scomint-exec-hook 37,1087
(define-derived-mode scomint-mode 46,1430
(defsubst scomint-check-proc 65,2345
(defun scomint-make-in-buffer 73,2685
(defun scomint-make 97,3952
(defun scomint-exec 110,4663
(defun scomint-exec-1 147,6256
(defalias 'scomint-send-string scomint-send-string
197,8386
(defun scomint-send-eof 199,8440
(defun scomint-send-input 208,8673
(defun scomint-truncate-buffer 234,9569
(defun scomint-strip-ctrl-m 247,9963
(defun scomint-output-filter 261,10526
(defun scomint-interrupt-process 284,11281

lib/span.el,1553
(defalias 'span-start span-start
22,609
(defalias 'span-end span-end
23,647
(defalias 'span-set-property span-set-property
24,681
(defalias 'span-property span-property
25,724
(defalias 'span-make span-make
26,763
(defalias 'span-detach span-detach
27,799
(defalias 'span-set-endpoints span-set-endpoints
28,839
(defalias 'span-buffer span-buffer
29,884
(defun span-read-only-hook 31,925
(defsubst span-read-only 36,1115
(defsubst span-read-write 43,1425
(defsubst span-write-warning 48,1595
(defsubst span-lt 59,2119
(defsubst spans-at-point-prop 64,2263
(defsubst spans-at-region-prop 73,2454
(defsubst span-at 83,2720
(defsubst span-delete 87,2846
(defsubst span-add-delete-action 93,3042
(defsubst span-mapcar-spans 99,3321
(defsubst span-mapc-spans 103,3496
(defsubst span-mapcar-spans-inorder 107,3667
(defun span-at-before 113,3872
(defsubst prev-span 130,4596
(defsubst next-span 136,4749
(defsubst span-live-p 142,4963
(defsubst span-raise 148,5129
(defsubst span-string 152,5262
(defsubst set-span-properties 157,5422
(defsubst span-find-span 163,5616
(defsubst span-at-event 171,5928
(defun fold-spans 177,6125
(defsubst span-detached-p 191,6658
(defsubst set-span-face 195,6774
(defsubst set-span-keymap 199,6872
(defsubst span-delete-spans 207,7041
(defsubst span-property-safe 211,7203
(defsubst span-set-start 215,7340
(defsubst span-set-end 219,7472
(defun span-make-self-removing-span 227,7632
(defun span-delete-self-modification-hook 237,8000
(defun span-make-modifying-removing-span 242,8174

lib/texi-docstring-magic.el,584
(defun texi-docstring-magic-find-face 88,3027
(defun texi-docstring-magic-splice-sep 93,3192
(defconst texi-docstring-magic-munge-table103,3497
(defun texi-docstring-magic-untabify 193,7260
(defun texi-docstring-magic-munge-docstring 200,7458
(defun texi-docstring-magic-texi 239,8739
(defun texi-docstring-magic-format-default 252,9179
(defun texi-docstring-magic-texi-for 268,9812
(defconst texi-docstring-magic-comment326,11771
(defun texi-docstring-magic 332,11925
(defun texi-docstring-magic-face-at-point 366,13004
(defun texi-docstring-magic-insert-magic 381,13527

lib/unicode-chars.el,80
(defvar unicode-chars-alist12,348
(defun unicode-chars-list-chars 5051,245975

lib/unicode-tokens.el,5901
(defgroup unicode-tokens-options 55,1711
(defcustom unicode-tokens-add-help-echo 60,1836
(defun unicode-tokens-toggle-add-help-echo 65,2003
(defvar unicode-tokens-token-symbol-map 79,2409
(defvar unicode-tokens-token-format 98,3068
(defvar unicode-tokens-token-variant-format-regexp 104,3317
(defvar unicode-tokens-shortcut-alist 118,3850
(defvar unicode-tokens-shortcut-replacement-alist 124,4127
(defvar unicode-tokens-control-region-format-regexp 132,4333
(defvar unicode-tokens-control-char-format-regexp 139,4701
(defvar unicode-tokens-control-regions 146,5062
(defvar unicode-tokens-control-characters 149,5138
(defvar unicode-tokens-control-char-format 152,5220
(defvar unicode-tokens-control-region-format-start 155,5333
(defvar unicode-tokens-control-region-format-end 158,5450
(defvar unicode-tokens-tokens-customizable-variables 161,5563
(defconst unicode-tokens-configuration-variables168,5731
(defun unicode-tokens-config 183,6130
(defun unicode-tokens-config-var 187,6275
(defun unicode-tokens-copy-configuration-variables 199,6715
(defvar unicode-tokens-token-list 227,7931
(defvar unicode-tokens-hash-table 230,8051
(defvar unicode-tokens-token-match-regexp 233,8167
(defvar unicode-tokens-uchar-hash-table 239,8450
(defvar unicode-tokens-uchar-regexp 243,8637
(defgroup unicode-tokens-faces 251,8822
(defconst unicode-tokens-font-family-alternatives261,9124
(defface unicode-tokens-symbol-font-face276,9642
(defface unicode-tokens-script-font-face286,10000
(defface unicode-tokens-fraktur-font-face291,10144
(defface unicode-tokens-serif-font-face296,10269
(defface unicode-tokens-sans-font-face301,10406
(defface unicode-tokens-highlight-face306,10528
(defconst unicode-tokens-fonts315,10890
(defconst unicode-tokens-fontsymb-properties324,11107
(define-widget 'unicode-tokens-token-symbol-map unicode-tokens-token-symbol-map
352,12728
(define-widget 'unicode-tokens-shortcut-alist unicode-tokens-shortcut-alist
370,13280
(defconst unicode-tokens-font-lock-extra-managed-props383,13611
(defun unicode-tokens-font-lock-keywords 387,13765
(defun unicode-tokens-calculate-token-match 420,15136
(defun unicode-tokens-usable-composition 450,16172
(defun unicode-tokens-help-echo 463,16551
(defvar unicode-tokens-show-symbols 468,16753
(defun unicode-tokens-interpret-composition 471,16867
(defun unicode-tokens-font-lock-compose-symbol 489,17379
(defun unicode-tokens-prepend-text-properties-in-match 527,18911
(defun unicode-tokens-prepend-text-property 541,19489
(defun unicode-tokens-show-symbols 566,20634
(defun unicode-tokens-symbs-to-props 574,20944
(defvar unicode-tokens-show-controls 594,21643
(defun unicode-tokens-show-controls 597,21734
(defun unicode-tokens-control-char 609,22247
(defun unicode-tokens-control-region 618,22686
(defun unicode-tokens-control-font-lock-keywords 629,23233
(defvar unicode-tokens-use-shortcuts 640,23557
(defun unicode-tokens-use-shortcuts 643,23660
(defun unicode-tokens-map-ordering 659,24256
(defun unicode-tokens-quail-define-rules 668,24609
(defun unicode-tokens-insert-token 691,25286
(defun unicode-tokens-annotate-region 700,25590
(defun unicode-tokens-insert-control 724,26428
(defun unicode-tokens-insert-uchar-as-token 734,26877
(defun unicode-tokens-delete-token-near-point 740,27098
(defun unicode-tokens-delete-backward-char 752,27539
(defun unicode-tokens-delete-char 763,27920
(defun unicode-tokens-delete-backward-1 774,28274
(defun unicode-tokens-delete-1 791,28870
(defun unicode-tokens-prev-token 807,29414
(defun unicode-tokens-rotate-token-forward 815,29711
(defun unicode-tokens-rotate-token-backward 842,30601
(defun unicode-tokens-replace-shortcut-match 847,30803
(defun unicode-tokens-replace-shortcuts 856,31173
(defun unicode-tokens-replace-unicode-match 870,31771
(defun unicode-tokens-replace-unicode 877,32072
(defun unicode-tokens-copy-token 894,32671
(define-button-type 'unicode-tokens-listunicode-tokens-list
901,32892
(defun unicode-tokens-list-tokens 907,33096
(defun unicode-tokens-list-shortcuts 946,34280
(defalias 'unicode-tokens-list-unicode-chars unicode-tokens-list-unicode-chars
964,34918
(defun unicode-tokens-encode-in-temp-buffer 966,34991
(defun unicode-tokens-encode 984,35647
(defun unicode-tokens-encode-str 990,35883
(defun unicode-tokens-copy 994,36045
(defun unicode-tokens-paste 1003,36451
(defvar unicode-tokens-highlight-unicode 1022,37172
(defconst unicode-tokens-unicode-highlight-patterns1025,37264
(defun unicode-tokens-highlight-unicode 1029,37433
(defun unicode-tokens-highlight-unicode-setkeywords 1041,37896
(defun unicode-tokens-initialise 1053,38265
(defvar unicode-tokens-mode-map 1073,38936
(defvar unicode-tokens-display-table1076,39033
(define-minor-mode unicode-tokens-mode1083,39284
(defun unicode-tokens-set-font-var 1219,43859
(defun unicode-tokens-set-font-var-aux 1235,44348
(defun unicode-tokens-mouse-set-font 1266,45509
(defsubst unicode-tokens-face-font-sym 1279,46023
(defun unicode-tokens-set-font-restart 1283,46203
(defun unicode-tokens-save-fonts 1294,46513
(defun unicode-tokens-custom-save-faces 1302,46769
(define-key unicode-tokens-mode-map1319,47225
(define-key unicode-tokens-mode-map1322,47332
(defvar unicode-tokens-quail-translation-keymap1330,47591
(define-key unicode-tokens-quail-translation-keymap1337,47781
(defun unicode-tokens-quail-delete-last-char 1341,47915
(define-key unicode-tokens-mode-map 1356,48342
(define-key unicode-tokens-mode-map 1358,48434
(define-key unicode-tokens-mode-map1360,48525
(define-key unicode-tokens-mode-map1362,48631
(define-key unicode-tokens-mode-map1365,48746
(define-key unicode-tokens-mode-map1367,48855
(define-key unicode-tokens-mode-map1369,48963
(define-key unicode-tokens-mode-map1371,49069
(defun unicode-tokens-customize-submenu 1379,49193
(defun unicode-tokens-define-menu 1386,49416

contrib/mmm/mmm-auto.el,343
(defvar mmm-autoloaded-classes67,2676
(defun mmm-autoload-class 89,3439
(defvar mmm-changed-buffers-list 129,4992
(defun mmm-major-mode-change 132,5099
(defun mmm-check-changed-buffers 145,5620
(defun mmm-mode-on-maybe 154,5970
(defalias 'mmm-add-find-file-hooks mmm-add-find-file-hooks
166,6374
(defun mmm-add-find-file-hook 167,6434

contrib/mmm/mmm-class.el,415
(defun mmm-get-class-spec 42,1296
(defun mmm-get-class-parameter 59,1939
(defun mmm-set-class-parameter 63,2105
(defun* mmm-apply-class75,2455
(defun* mmm-apply-classes90,3072
(defun* mmm-apply-all 110,3803
(defun* mmm-ify124,4250
(defun* mmm-match-region206,7095
(defun mmm-match->point 269,9480
(defun mmm-match-and-verify 284,10050
(defun mmm-get-form 310,11101
(defun mmm-default-get-form 321,11576

contrib/mmm/mmm-cmds.el,712
(defun mmm-ify-by-class 41,1210
(defun mmm-ify-region 63,1822
(defun mmm-ify-by-regexp75,2243
(defun mmm-parse-buffer 97,2886
(defun mmm-parse-region 106,3222
(defun mmm-parse-block 115,3601
(defun mmm-get-block 132,4352
(defun mmm-reparse-current-region 146,4634
(defun mmm-clear-current-region 167,5210
(defun mmm-clear-regions 172,5374
(defun mmm-clear-all-regions 177,5520
(defun* mmm-end-current-region 185,5680
(defun mmm-narrow-to-submode-region 220,6928
(defun mmm-insert-region 239,7542
(defun mmm-insert-by-key 258,8348
(defun mmm-get-insertion-spec 342,11613
(defun mmm-insertion-help 369,12573
(defun mmm-display-insertion-key 379,12936
(defun mmm-get-all-insertion-keys 401,13723

contrib/mmm/mmm-compat.el,418
(defvar mmm-xemacs 40,1313
(defvar mmm-keywords-used49,1616
(defmacro mmm-regexp-opt 91,2632
(defvar mmm-evaporate-property110,3281
(defmacro mmm-set-keymap-default 128,4047
(defmacro mmm-event-key 137,4489
(defvar skeleton-positions 146,4708
(defun mmm-fixup-skeleton 147,4739
(defmacro mmm-make-temp-buffer 159,5162
(defvar mmm-font-lock-available-p 172,5558
(defmacro mmm-set-font-lock-defaults 179,5772

contrib/mmm/mmm-cweb.el,228
(defvar mmm-cweb-section-tags38,1117
(defvar mmm-cweb-section-regexp41,1164
(defvar mmm-cweb-c-part-tags44,1254
(defvar mmm-cweb-c-part-regexp47,1313
(defun mmm-cweb-in-limbo 50,1397
(defun mmm-cweb-verify-brief-c 57,1622

contrib/mmm/mmm-mason.el,410
(defvar mmm-mason-perl-tags41,1236
(defvar mmm-mason-pseudo-perl-tags45,1377
(defvar mmm-mason-non-perl-tags48,1453
(defvar mmm-mason-perl-tags-regexp51,1554
(defvar mmm-mason-pseudo-perl-tags-regexp56,1749
(defvar mmm-mason-tag-names-regexp61,1966
(defun mmm-mason-verify-inline 66,2186
(defun mmm-mason-start-line 156,4838
(defun mmm-mason-end-line 161,4903
(defun mmm-mason-set-mode-line 168,4997

contrib/mmm/mmm-mode.el,1025
(defun mmm-mode 101,3867
(defun mmm-mode-on 140,5372
(defun mmm-mode-off 183,7156
(defvar mmm-mode-map 209,7897
(defvar mmm-mode-prefix-map 212,7972
(defvar mmm-mode-menu-map 215,8082
(defun mmm-define-key 218,8173
(define-key mmm-mode-prefix-map 242,8928
(define-key mmm-mode-prefix-map 249,9186
(define-key mmm-mode-map 252,9297
(define-key mmm-mode-menu-map 255,9399
(define-key mmm-mode-menu-map 257,9471
(define-key mmm-mode-menu-map 259,9530
(define-key mmm-mode-menu-map 261,9611
(define-key mmm-mode-menu-map 263,9692
(define-key mmm-mode-menu-map 265,9779
(define-key mmm-mode-menu-map 268,9873
(define-key mmm-mode-menu-map 270,9933
(define-key mmm-mode-menu-map 273,10024
(define-key mmm-mode-menu-map 275,10084
(define-key mmm-mode-menu-map 277,10191
(define-key mmm-mode-menu-map 279,10276
(define-key mmm-mode-menu-map 282,10362
(define-key mmm-mode-menu-map 284,10422
(define-key mmm-mode-menu-map 286,10535
(define-key mmm-mode-menu-map 288,10620
(define-key mmm-mode-map 291,10703

contrib/mmm/mmm-region.el,1643
(defsubst mmm-overlay-at 54,1749
(defun mmm-overlays-at 59,1934
(defun mmm-included-p 72,2387
(defun mmm-overlays-containing 112,3876
(defun mmm-overlays-contained-in 125,4314
(defun mmm-overlays-overlapping 138,4754
(defun mmm-sort-overlays 149,5117
(defvar mmm-current-overlay 158,5359
(defvar mmm-previous-overlay 163,5574
(defvar mmm-current-submode 168,5762
(defvar mmm-previous-submode 173,5962
(defun mmm-update-current-submode 178,6135
(defun mmm-set-current-submode 199,6930
(defun mmm-submode-at 210,7373
(defun mmm-match-front 219,7648
(defun mmm-match-back 238,8409
(defun mmm-front-start 257,9154
(defun mmm-back-end 265,9458
(defun mmm-valid-submode-region 278,9805
(defun* mmm-make-region305,10961
(defun mmm-make-overlay 431,16311
(defun mmm-get-face 459,17444
(defun mmm-clear-overlays 470,17736
(defun mmm-update-mode-info 486,18201
(defun mmm-update-submode-region 572,21874
(defun mmm-add-hooks 589,22604
(defun mmm-remove-hooks 592,22701
(defun mmm-get-local-variables-list 598,22828
(defun mmm-get-locals 618,23524
(defun mmm-get-saved-local 631,24021
(defun mmm-set-local-variables 635,24186
(defun mmm-get-saved-local-variables 646,24564
(defun mmm-save-changed-local-variables 654,24839
(defun mmm-clear-local-variables 673,25543
(defun mmm-enable-font-lock 684,25808
(defun mmm-update-font-lock-buffer 692,26068
(defun mmm-refontify-maybe 705,26479
(defun mmm-submode-changes-in 720,26959
(defun mmm-regions-in 731,27316
(defun mmm-regions-alist 745,27794
(defun mmm-fontify-region 762,28321
(defun mmm-fontify-region-list 783,29343
(defun mmm-beginning-of-syntax 805,30091

contrib/mmm/mmm-rpm.el,154
(defconst mmm-rpm-sh-start-tags48,1618
(defvar mmm-rpm-sh-end-tags53,1842
(defvar mmm-rpm-sh-start-regexp57,2016
(defvar mmm-rpm-sh-end-regexp61,2194

contrib/mmm/mmm-sample.el,168
(defvar mmm-here-doc-mode-alist 84,2601
(defun mmm-here-doc-get-mode 93,3086
(defun mmm-file-variables-verify 208,6343
(defun mmm-file-variables-find-back 232,7148

contrib/mmm/mmm-univ.el,34
(defun mmm-univ-get-mode 38,1205

contrib/mmm/mmm-utils.el,282
(defmacro mmm-valid-buffer 42,1332
(defmacro mmm-save-all 61,1941
(defun mmm-format-string 74,2223
(defun mmm-format-matches 85,2661
(defmacro mmm-save-keyword 108,3419
(defmacro mmm-save-keywords 116,3746
(defun mmm-looking-back-at 129,4244
(defun mmm-make-marker 146,4784

contrib/mmm/mmm-vars.el,2668
(defgroup mmm 104,3283
(defvar mmm-c-derived-modes111,3393
(defvar mmm-save-local-variables115,3512
(defvar mmm-buffer-saved-locals 341,10293
(defvar mmm-region-saved-locals-defaults 346,10493
(defvar mmm-region-saved-locals-for-dominant 352,10753
(defgroup mmm-faces 362,11130
(defcustom mmm-submode-decoration-level 368,11301
(defface mmm-init-submode-face 386,12145
(defface mmm-cleanup-submode-face 390,12285
(defface mmm-declaration-submode-face 394,12422
(defface mmm-comment-submode-face 398,12568
(defface mmm-output-submode-face 402,12721
(defface mmm-special-submode-face 406,12870
(defface mmm-code-submode-face 410,13034
(defface mmm-default-submode-face 414,13173
(defface mmm-delimiter-face 419,13381
(defcustom mmm-mode-string 426,13507
(defcustom mmm-submode-mode-line-format 431,13638
(defvar mmm-primary-mode-display-name 448,14293
(defvar mmm-buffer-mode-display-name 453,14507
(defun mmm-set-mode-line 459,14806
(defvar mmm-classes 483,15614
(defvar mmm-global-classes 489,15859
(defcustom mmm-mode-ext-classes-alist 496,16041
(defun mmm-add-mode-ext-class 515,16831
(defcustom mmm-major-mode-preferences524,17156
(defun mmm-add-to-major-mode-preferences 542,17884
(defun mmm-ensure-modename 558,18642
(defun mmm-modename->function 567,18945
(defcustom mmm-delimiter-mode 581,19394
(defcustom mmm-mode-prefix-key 591,19663
(defcustom mmm-command-modifiers 596,19790
(defcustom mmm-insert-modifiers 610,20423
(defcustom mmm-use-old-command-keys 625,21101
(defun mmm-use-old-command-keys 635,21565
(defcustom mmm-mode-hook 643,21757
(defun mmm-run-constructed-hook 663,22564
(defun mmm-run-major-hook 671,22908
(defun mmm-run-submode-hook 674,22985
(defvar mmm-class-hooks-run 677,23072
(defun mmm-run-class-hook 682,23244
(defvar mmm-primary-mode-entry-hook 687,23416
(defcustom mmm-major-mode-hook 702,24063
(defun mmm-run-major-mode-hook 716,24694
(defcustom mmm-global-mode 729,25235
(defcustom mmm-never-modes745,25902
(defvar mmm-set-file-name-for-modes 763,26202
(defvar mmm-mode 774,26561
(defvar mmm-primary-mode 782,26769
(defvar mmm-classes-alist 793,27135
(defun mmm-add-classes 948,35342
(defun mmm-add-group 953,35507
(defun mmm-add-to-group 963,35880
(defconst mmm-version 977,36307
(defun mmm-version 980,36372
(defvar mmm-temp-buffer-name 987,36515
(defvar mmm-interactive-history 993,36645
(defun mmm-add-to-history 999,36914
(defun mmm-clear-history 1002,36997
(defvar mmm-mode-ext-classes 1010,37182
(defun mmm-get-mode-ext-classes 1015,37393
(defun mmm-clear-mode-ext-classes 1024,37720
(defun mmm-mode-ext-applies 1028,37845
(defun mmm-get-all-classes 1042,38224

doc/ProofGeneral.texi,6650
@node Top145,4231
@node Preface183,5385
@node News for Version 4.1News for Version 4.1
207,5999
@node News for Version 4.0News for Version 4.0
218,6306
@node Future239,7157
@node Credits268,8492
@node Introducing Proof GeneralIntroducing Proof General
390,12601
@node Installing Proof GeneralInstalling Proof General
445,14575
@node Quick start guideQuick start guide
459,15024
@node Features of Proof GeneralFeatures of Proof General
503,17145
@node Supported proof assistantsSupported proof assistants
592,21082
@node Prerequisites for this manualPrerequisites for this manual
641,22963
@node Organization of this manualOrganization of this manual
685,24582
@node Basic Script ManagementBasic Script Management
711,25410
@node Walkthrough example in IsabelleWalkthrough example in Isabelle
730,26010
@node Proof scriptsProof scripts
1015,37405
@node Script buffersScript buffers
1058,39525
@node Locked queue and editing regionsLocked queue and editing regions
1080,40102
@node Goal-save sequencesGoal-save sequences
1136,42249
@node Active scripting bufferActive scripting buffer
1173,43733
@node Summary of Proof General buffersSummary of Proof General buffers
1246,47366
@node Script editing commandsScript editing commands
1295,49623
@node Script processing commandsScript processing commands
1375,52582
@node Proof assistant commandsProof assistant commands
1501,57827
@node Toolbar commandsToolbar commands
1694,64755
@node Interrupting during trace outputInterrupting during trace output
1719,65714
@node Advanced Script Management and EditingAdvanced Script Management and Editing
1759,67644
@node Document centred workingDocument centred working
1780,68265
@node Automatic processingAutomatic processing
1892,72943
@node Visibility of completed proofsVisibility of completed proofs
1947,74991
@node Switching between proof scriptsSwitching between proof scripts
2002,76931
@node View of processed files View of processed files 
2039,78903
@node Retracting across filesRetracting across files
2099,81954
@node Asserting across filesAsserting across files
2112,82585
@node Automatic multiple file handlingAutomatic multiple file handling
2125,83151
@node Escaping script managementEscaping script management
2150,84185
@node Editing featuresEditing features
2207,86297
@node Unicode symbols and special layout supportUnicode symbols and special layout support
2277,89076
@node Maths menuMaths menu
2319,90634
@node Unicode Tokens modeUnicode Tokens mode
2336,91325
@node Configuring tokens symbols and shortcutsConfiguring tokens symbols and shortcuts
2386,93748
@node Special layout Special layout 
2416,94709
@node Moving between Unicode and tokensMoving between Unicode and tokens
2526,98827
@node Finding available tokens shortcuts and symbolsFinding available tokens shortcuts and symbols
2581,100938
@node Selecting suitable fontsSelecting suitable fonts
2620,102112
@node Support for other PackagesSupport for other Packages
2685,105100
@node Syntax highlightingSyntax highlighting
2715,105936
@node Imenu and SpeedbarImenu and Speedbar
2743,106939
@node Support for outline modeSupport for outline mode
2789,108610
@node Support for completionSupport for completion
2814,109739
@node Support for tagsSupport for tags
2871,111901
@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
2923,114249
@node Goals buffer commandsGoals buffer commands
2939,114844
@node Customizing Proof GeneralCustomizing Proof General
3038,118997
@node Basic optionsBasic options
3078,120667
@node How to customizeHow to customize
3102,121437
@node Display customizationDisplay customization
3149,123404
@node User optionsUser options
3317,130366
@node Changing facesChanging faces
3553,139034
@node Script buffer facesScript buffer faces
3575,139909
@node Goals and response facesGoals and response faces
3621,141509
@node Tweaking configuration settingsTweaking configuration settings
3666,143041
@node Hints and TipsHints and Tips
3723,145567
@node Adding your own keybindingsAdding your own keybindings
3742,146168
@node Using file variablesUsing file variables
3806,148782
@node Using abbreviationsUsing abbreviations
3882,151453
@node LEGO Proof GeneralLEGO Proof General
3921,152868
@node LEGO specific commandsLEGO specific commands
3962,154237
@node LEGO tagsLEGO tags
3982,154692
@node LEGO customizationsLEGO customizations
3992,154939
@node Coq Proof GeneralCoq Proof General
4024,155858
@node Coq-specific commandsCoq-specific commands
4039,156195
@node Multiple File SupportMultiple File Support
4062,156703
@node Automatic Compilation in DetailAutomatic Compilation in Detail
4132,159292
@node Locking AncestorsLocking Ancestors
4207,162643
@node Customizing Coq Multiple File SupportCustomizing Coq Multiple File Support
4240,164068
@node Current LimitationsCurrent Limitations
4472,173838
@node Editing multiple proofsEditing multiple proofs
4498,174690
@node User-loaded tacticsUser-loaded tactics
4522,175798
@node Holes featureHoles feature
4586,178272
@node Isabelle Proof GeneralIsabelle Proof General
4615,179602
@node Choosing logic and starting isabelleChoosing logic and starting isabelle
4641,180478
@node Isabelle commandsIsabelle commands
4710,183279
@node Isabelle settingsIsabelle settings
4853,187471
@node Isabelle customizationsIsabelle customizations
4867,188053
@node HOL Proof GeneralHOL Proof General
4890,188540
@node Shell Proof GeneralShell Proof General
4932,190362
@node Obtaining and InstallingObtaining and Installing
4968,191821
@node Obtaining Proof GeneralObtaining Proof General
4983,192186
@node Installing Proof General from tarballInstalling Proof General from tarball
5009,193068
@node Setting the names of binariesSetting the names of binaries
5033,193858
@node Notes for syssiesNotes for syssies
5061,194798
@node Bugs and EnhancementsBugs and Enhancements
5137,197795
@node References5158,198610
@node History of Proof GeneralHistory of Proof General
5198,199633
@node Old News for 3.0Old News for 3.0
5292,203798
@node Old News for 3.1Old News for 3.1
5362,207492
@node Old News for 3.2Old News for 3.2
5388,208664
@node Old News for 3.3Old News for 3.3
5449,211667
@node Old News for 3.4Old News for 3.4
5468,212564
@node Old News for 3.5Old News for 3.5
5490,213619
@node Old News for 3.6Old News for 3.6
5494,213676
@node Old News for 3.7Old News for 3.7
5499,213776
@node Function IndexFunction Index
5529,215230
@node Variable IndexVariable Index
5533,215306
@node Keystroke IndexKeystroke Index
5537,215386
@node Concept IndexConcept Index
5541,215452

doc/PG-adapting.texi,3844
@node Top137,3992
@node Introduction174,5101
@node Future215,6754
@node Credits251,8350
@node Beginning with a New ProverBeginning with a New Prover
261,8642
@node Overview of adding a new proverOverview of adding a new prover
301,10584
@node Demonstration instance and easy configurationDemonstration instance and easy configuration
383,14133
@node Major modes used by Proof GeneralMajor modes used by Proof General
452,17524
@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands
495,19234
@node Settings for generic user-level commandsSettings for generic user-level commands
510,19780
@node Menu configurationMenu configuration
555,21512
@node Toolbar configurationToolbar configuration
579,22429
@node Proof Script SettingsProof Script Settings
638,24666
@node Recognizing commands and commentsRecognizing commands and comments
661,25278
@node Recognizing proofsRecognizing proofs
798,31731
@node Recognizing other elementsRecognizing other elements
902,36035
@node Configuring undo behaviourConfiguring undo behaviour
965,38514
@node Nested proofsNested proofs
1102,43901
@node Safe (state-preserving) commandsSafe (state-preserving) commands
1142,45527
@node Activate scripting hookActivate scripting hook
1165,46480
@node Automatic multiple filesAutomatic multiple files
1189,47350
@node Completely asserted buffersCompletely asserted buffers
1210,48196
@node Completions1243,49661
@node Proof Shell SettingsProof Shell Settings
1284,51151
@node Proof shell commandsProof shell commands
1315,52433
@node Script input to the shellScript input to the shell
1492,60197
@node Settings for matching various output from proof processSettings for matching various output from proof process
1562,63401
@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process
1684,68755
@node Hooks and other settingsHooks and other settings
1911,78717
@node Goals Buffer SettingsGoals Buffer Settings
1990,81861
@node Splash Screen SettingsSplash Screen Settings
2064,84851
@node Global ConstantsGlobal Constants
2090,85606
@node Handling Multiple FilesHandling Multiple Files
2116,86435
@node Configuring Editing SyntaxConfiguring Editing Syntax
2285,95104
@node Configuring Font LockConfiguring Font Lock
2342,97221
@node Configuring TokensConfiguring Tokens
2418,100933
@node Writing More Lisp CodeWriting More Lisp Code
2468,103053
@node Default values for generic settingsDefault values for generic settings
2485,103698
@node Adding prover-specific configurationsAdding prover-specific configurations
2515,104781
@node Useful variablesUseful variables
2558,106063
@node Useful functions and macrosUseful functions and macros
2573,106562
@node Internals of Proof GeneralInternals of Proof General
2683,110874
@node Spans2713,111804
@node Proof General site configurationProof General site configuration
2728,112177
@node Configuration variable mechanismsConfiguration variable mechanisms
2811,115258
@node Global variablesGlobal variables
2941,120974
@node Proof script modeProof script mode
3016,123598
@node Proof shell modeProof shell mode
3280,135555
@node Debugging3824,157585
@node Plans and IdeasPlans and Ideas
3867,158461
@node Proof by pointing and similar featuresProof by pointing and similar features
3888,159183
@node Granularity of atomic command sequencesGranularity of atomic command sequences
3926,160841
@node Browser mode for script files and theoriesBrowser mode for script files and theories
3971,163066
@node Demonstration InstantiationsDemonstration Instantiations
4001,164097
@node demoisa-easy.el4017,164528
@node demoisa.el4079,166719
@node Function IndexFunction Index
4233,171638
@node Variable IndexVariable Index
4237,171714
@node Concept IndexConcept Index
4246,171893

generic/proofgeneral-pkg.el,0

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