ccc/ccc.el,87
(defvar ccc-keywords 17,587
(defvar ccc-tactics 18,613
(defvar ccc-tacticals 19,638

coq/coq-abbrev.el,590
(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,746
(defconst coq-tacticals-menu29,863
(defconst coq-tacticals-abbrev-table33,972
(defconst coq-commands-menu36,1063
(defconst coq-commands-abbrev-table43,1286
(defconst coq-terms-menu46,1375
(defconst coq-terms-abbrev-table51,1513
(defun coq-install-abbrevs 58,1707
(defconst coq-menu-common-entries81,2663
(defpgdefault menu-entries179,7146
(defpgdefault help-menu-entries213,8253
(defpgdefault other-buffers-menu-entries 217,8383

coq/coq-compile-common.el,1880
(defun get-coq-library-directory 31,820
(defconst coq-library-directory 37,1007
(defcustom coq-dependency-analyzer40,1134
(defcustom coq-compiler46,1274
(defun coq-par-enable 60,1799
(defun coq-par-disable 68,2071
(defun coq-seq-enable 76,2356
(defun coq-seq-disable 82,2562
(defun coq-load-path-safep 91,2813
(defun coq-switch-compilation-method 111,3409
(defgroup coq-auto-compile 123,3677
(defpacustom compile-before-require 128,3828
(defpacustom compile-parallel-in-background 140,4320
(defcustom coq-compile-command 161,5210
(defconst coq-compile-substitution-list191,6489
(defcustom coq-load-path 211,7410
(defcustom coq-compile-auto-save 248,9155
(defcustom coq-lock-ancestors 273,10212
(defpacustom confirm-external-compilation 282,10533
(defcustom coq-load-path-include-current 291,10840
(defcustom coq-compile-ignored-directories 300,11158
(defcustom coq-compile-ignore-library-directory 313,11790
(defcustom coq-coqdep-error-regexp325,12278
(defconst coq-require-command-regexp342,13057
(defconst coq-require-id-regexp349,13414
(defvar coq-compile-history 357,13848
(defvar coq-compile-response-buffer 360,13932
(defvar coq-debug-auto-compilation 364,14067
(defun time-less-or-equal 370,14176
(defun coq-max-dep-mod-time 378,14514
(defun coq-option-of-load-path-entry 401,15319
(defun coq-include-options 415,15834
(defun coq-prog-args 439,16853
(defun coq-compile-ignore-file 448,17126
(defun coq-library-src-of-obj-file 474,18048
(defun coq-unlock-ancestor 483,18372
(defun coq-unlock-all-ancestors-of-span 490,18667
(defun coq-init-compile-response-buffer 498,18952
(defun coq-display-compile-response-buffer 521,20024
(defvar coq-compile-buffer-with-current-require534,20543
(defun coq-compile-save-buffer-filter 540,20779
(defun coq-compile-save-some-buffers 551,21205
(defun coq-switch-buffer-kill-proof-shell 576,22159

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,6991
(defcustom coq-holes-minor-mode 212,7830
(defun coq-build-abbrev-table-from-db 218,7974
(defun filter-state-preserving 237,8600
(defun filter-state-changing 242,8754
(defface coq-solve-tactics-face249,8975
(defface coq-cheat-face258,9266
(defconst coq-solve-tactics-face 266,9515
(defconst coq-cheat-face 270,9679

coq/coq.el,8821
(defcustom coq-prog-name61,2049
(defcustom coq-translate-to-v8 80,2900
(defun coq-build-prog-args 85,3015
(defcustom coq-use-makefile 95,3338
(defcustom coq-default-undo-limit 101,3510
(defconst coq-shell-init-cmd106,3638
(defcustom coq-prog-env 115,3965
(defconst coq-shell-restart-cmd 123,4214
(defvar coq-shell-prompt-pattern125,4268
(defvar coq-shell-cd 133,4571
(defvar coq-shell-proof-completed-regexp 137,4731
(defvar coq-goal-regexp140,4946
(defcustom coq-tags 144,5037
(defconst coq-interrupt-regexp 149,5185
(defcustom coq-www-home-page 152,5278
(defcustom coq-end-goals-regexp-show-subgoals 157,5385
(defcustom coq-end-goals-regexp-hide-subgoals164,5669
(defgroup coq-proof-tree 175,6001
(defcustom coq-proof-tree-ignored-commands-regexp183,6364
(defcustom coq-navigation-command-regexp192,6758
(defcustom coq-proof-tree-cheating-regexp198,6930
(defcustom coq-proof-tree-current-goal-regexp204,7070
(defcustom coq-proof-tree-update-goal-regexp212,7404
(defcustom coq-proof-tree-additional-subgoal-ID-regexp219,7638
(defcustom coq-proof-tree-existential-regexp 225,7836
(defcustom coq-proof-tree-instantiated-existential-regexp230,7990
(defcustom coq-proof-tree-existentials-state-start-regexp236,8210
(defcustom coq-proof-tree-existentials-state-end-regexp 242,8400
(defcustom coq-proof-tree-proof-finished-regexp247,8569
(defvar coq-outline-regexp259,8838
(defvar coq-outline-heading-end-regexp 268,9112
(defvar coq-shell-outline-regexp 270,9166
(defvar coq-shell-outline-heading-end-regexp 271,9216
(defconst coq-state-preserving-tactics-regexp274,9280
(defconst coq-state-changing-commands-regexp276,9382
(defconst coq-state-preserving-commands-regexp278,9491
(defconst coq-commands-regexp280,9604
(defvar coq-retractable-instruct-regexp282,9683
(defvar coq-non-retractable-instruct-regexp284,9775
(defcustom coq-use-smie 316,10471
(defconst coq-script-command-end-regexp 341,11309
(defun coq-script-parse-function 350,11738
(defun coq-set-undo-limit 357,11964
(defun build-list-id-from-string 363,12096
(defun coq-last-prompt-info 372,12571
(defun coq-last-prompt-info-safe 390,13465
(defvar coq-last-but-one-statenum 398,13818
(defvar coq-last-but-one-proofnum 405,14115
(defvar coq-last-but-one-proofstack 408,14213
(defsubst coq-get-span-statenum 411,14323
(defsubst coq-get-span-proofnum 415,14438
(defsubst coq-get-span-proofstack 419,14553
(defsubst coq-set-span-statenum 423,14697
(defsubst coq-get-span-goalcmd 427,14828
(defsubst coq-set-span-goalcmd 431,14942
(defsubst coq-set-span-proofnum 435,15072
(defsubst coq-set-span-proofstack 439,15203
(defsubst proof-last-locked-span 443,15363
(defun proof-clone-buffer 447,15497
(defun proof-store-buffer-win 461,16034
(defun proof-store-response-win 472,16527
(defun proof-store-goals-win 476,16654
(defun coq-set-state-infos 488,17186
(defun count-not-intersection 526,19276
(defun coq-find-and-forget 556,20528
(defvar coq-current-goal 583,21833
(defun coq-goal-hyp 586,21898
(defun coq-state-preserving-p 599,22378
(defun coq-hide-additional-subgoals-switch 609,22672
(defconst notation-print-kinds-table621,23013
(defun coq-PrintScope 625,23180
(defun coq-remove-trailing-dot 643,23729
(defun coq-id-at-point 651,23966
(defun coq-guess-or-ask-for-string 665,24529
(defun coq-ask-do 684,25144
(defun coq-flag-is-on-p 693,25527
(defun coq-command-with-set-unset 699,25734
(defun coq-ask-do-set-unset 710,26384
(defun coq-ask-do-show-implicits 720,26914
(defun coq-ask-do-show-all 728,27274
(defsubst coq-put-into-brackets 749,27955
(defsubst coq-put-into-quotes 752,28016
(defun coq-SearchIsos 755,28075
(defun coq-SearchConstant 763,28314
(defun coq-Searchregexp 767,28407
(defun coq-SearchRewrite 773,28548
(defun coq-SearchAbout 777,28645
(defun coq-Print 783,28788
(defun coq-Print-with-implicits 791,29058
(defun coq-Print-with-all 796,29212
(defun coq-About 801,29354
(defun coq-About-with-implicits 808,29561
(defun coq-About-with-all 813,29710
(defun coq-LocateConstant 819,29848
(defun coq-LocateLibrary 824,29951
(defun coq-LocateNotation 829,30068
(defun coq-Pwd 837,30299
(defun coq-Inspect 842,30423
(defun coq-PrintSection(846,30523
(defun coq-Print-implicit 850,30616
(defun coq-Check 855,30767
(defun coq-Check-show-implicits 863,31021
(defun coq-Check-show-all 868,31159
(defun coq-get-response-string-at 873,31285
(defun coq-Show 887,31875
(defun coq-Show-with-implicits 917,33283
(defun coq-Show-with-all 922,33439
(defun coq-Compile 949,34816
(defun coq-guess-command-line 961,35141
(defun coq-mode-config 1019,37493
(defun coq-shell-mode-config 1130,41604
(defun coq-goals-mode-config 1221,45402
(defun coq-response-config 1228,45646
(defpacustom hide-additional-subgoals 1251,46363
(defpacustom printing-depth 1272,47026
(defpacustom undo-depth 1277,47187
(defpacustom time-commands 1282,47353
(defun coq-proof-tree-get-proof-info 1292,47558
(defun coq-extract-instantiated-existentials 1302,47946
(defun coq-show-sequent-command 1311,48338
(defun coq-proof-tree-get-new-subgoals 1315,48492
(defun coq-find-begin-of-unfinished-proof 1359,50617
(defun coq-preprocessing 1384,51631
(defun coq-fake-constant-markup 1398,52086
(defun coq-create-span-menu 1414,52691
(defconst module-kinds-table1432,53204
(defconst modtype-kinds-table1436,53353
(defun coq-postfix-.v-p 1440,53482
(defun coq-directories-files 1443,53543
(defun coq-remove-dot-v-extension 1449,53771
(defun coq-load-path-to-paths 1452,53832
(defun coq-build-accessible-modules-list 1455,53911
(defun coq-insert-section-or-module 1462,54228
(defconst reqkinds-kinds-table1484,55108
(defun coq-insert-requires 1488,55265
(defun coq-end-Section 1502,55818
(defun coq-insert-intros 1520,56396
(defvar coq-commands-accepting-as 1533,56928
(defvar coq-last-input-action 1535,57027
(defun coq-insert-infoH 1541,57243
(defun coq-auto-insert-as 1555,57908
(defpacustom auto-insert-as 1565,58322
(defun coq-tactic-already-has-an-as-close(1572,58557
(defun coq-insert-as 1587,59322
(defun coq-insert-as-in-region 1626,61418
(defun coq-insert-match 1638,61691
(defun coq-insert-solve-tactic 1667,62860
(defun coq-insert-tactic 1673,63111
(defun coq-insert-tactical 1679,63313
(defun coq-insert-command 1685,63544
(defun coq-insert-term 1690,63709
(define-key coq-keymap 1696,63892
(define-key coq-keymap 1697,63950
(define-key coq-keymap 1698,64007
(define-key coq-keymap 1699,64076
(define-key coq-keymap 1700,64132
(define-key coq-keymap 1701,64190
(define-key coq-keymap 1702,64240
(define-key coq-keymap 1703,64313
(define-key coq-keymap 1704,64370
(define-key coq-keymap 1705,64433
(define-key coq-keymap 1708,64511
(define-key coq-keymap 1709,64560
(define-key coq-keymap 1710,64615
(define-key coq-keymap 1711,64667
(define-key coq-keymap 1712,64722
(define-key coq-keymap 1713,64772
(define-key coq-keymap 1714,64822
(define-key coq-keymap 1715,64878
(define-key coq-keymap 1716,64928
(define-key coq-keymap 1717,64972
(define-key coq-keymap 1718,65031
(define-key coq-goals-mode-map 1726,65299
(define-key coq-goals-mode-map 1727,65381
(define-key coq-goals-mode-map 1728,65463
(define-key coq-goals-mode-map 1729,65550
(define-key coq-goals-mode-map 1730,65632
(define-key coq-goals-mode-map 1731,65720
(define-key coq-goals-mode-map 1732,65801
(define-key coq-goals-mode-map 1733,65888
(define-key coq-goals-mode-map 1734,65972
(define-key coq-response-mode-map 1737,66050
(define-key coq-response-mode-map 1738,66135
(define-key coq-response-mode-map 1739,66220
(define-key coq-response-mode-map 1740,66310
(define-key coq-response-mode-map 1741,66395
(define-key coq-response-mode-map 1742,66486
(define-key coq-response-mode-map 1743,66570
(define-key coq-response-mode-map 1744,66670
(define-key coq-response-mode-map 1745,66767
(defvar last-coq-error-location 1752,66917
(defun coq-get-last-error-location 1760,67301
(defun coq-highlight-error 1810,69864
(defun coq-highlight-error-hook 1838,70945
(defun coq-first-word-before 1848,71162
(defun coq-get-from-to-paren 1858,71493
(defun coq-show-first-goal 1871,71899
(defvar coq-modeline-string2 1887,72564
(defvar coq-modeline-string1 1888,72598
(defvar coq-modeline-string0 1889,72632
(defun coq-build-subgoals-string 1890,72673
(defun coq-update-minor-mode-alist 1896,72857
(defun is-not-split-vertic 1930,74426
(defun coq-optimise-resp-windows 1944,75219
(defcustom coq-double-hit-enable 1984,77041
(defadvice proof-electric-terminator-enable 2003,77827
(defvar coq-double-hit-delay 2011,78205
(defvar coq-double-hit-timer 2014,78320
(defvar coq-double-hit-hot 2017,78400
(defun coq-unset-double-hit-hot 2021,78496
(defun coq-colon-self-insert 2029,78827
(defun coq-terminator-insert 2043,79383

coq/coq-indent.el,2698
(defconst coq-any-command-regexp20,368
(defconst coq-indent-inner-regexp23,442
(defconst coq-comment-start-regexp 33,799
(defconst coq-comment-end-regexp 34,842
(defconst coq-comment-start-or-end-regexp35,883
(defconst coq-indent-open-regexp37,991
(defconst coq-indent-close-regexp42,1188
(defconst coq-indent-closepar-regexp 48,1387
(defconst coq-indent-closematch-regexp 49,1432
(defconst coq-indent-openpar-regexp 50,1503
(defconst coq-indent-openmatch-regexp 51,1547
(defconst coq-tacticals-tactics-regex52,1627
(defconst coq-indent-any-regexp54,1746
(defconst coq-indent-kw58,1962
(defconst coq-indent-pattern-regexp 68,2428
(defun coq-indent-goal-command-p 72,2531
(defconst coq-period-end-command93,3549
(defconst coq-curlybracket-end-command99,3831
(defconst coq-bullet-end-command104,4060
(defconst coq-end-command-regexp117,4515
(defun coq-search-comment-delimiter-forward 133,5240
(defun coq-search-comment-delimiter-backward 142,5570
(defun coq-skip-until-one-comment-backward 149,5844
(defun coq-skip-until-one-comment-forward 164,6551
(defun coq-looking-at-comment 175,7069
(defun coq-find-comment-start 180,7234
(defun coq-find-comment-end 192,7711
(defun coq-looking-at-syntactic-context 204,8204
(defconst coq-end-command-or-comment-regexp210,8426
(defconst coq-end-command-or-comment-start-regexp213,8535
(defun coq-find-not-in-comment-backward 216,8652
(defun coq-find-not-in-comment-forward 235,9531
(defun coq-is-on-ending-context 261,10723
(defun coq-empty-command-p 270,10936
(defun coq-script-parse-cmdend-forward 285,11677
(defun coq-script-parse-cmdend-backward 337,14178
(defun coq-find-current-start 378,16099
(defun coq-find-real-start 387,16425
(defun same-line 393,16643
(defun coq-command-at-point 396,16730
(defun coq-commands-at-line 411,17341
(defun coq-indent-only-spaces-on-line 435,18307
(defun coq-indent-find-reg 441,18584
(defun coq-find-no-syntactic-on-line 455,19120
(defun coq-back-to-indentation-prevline 468,19593
(defun coq-find-unclosed 514,21660
(defun coq-find-at-same-level-zero 544,22970
(defun coq-find-unopened 573,24236
(defun coq-find-last-unopened 616,25670
(defun coq-end-offset 627,26067
(defun coq-add-iter 652,26837
(defun coq-goal-count 655,26943
(defun coq-save-count 657,27015
(defun coq-proof-count 662,27214
(defun coq-goal-save-diff-maybe-proof 668,27500
(defun coq-indent-command-offset 678,27794
(defun coq-indent-expr-offset 744,30975
(defun coq-indent-comment-offset 863,35857
(defun coq-indent-offset 895,37309
(defun coq-indent-calculate 914,38183
(defun coq-indent-line 917,38271
(defun coq-indent-line-not-comments 927,38637
(defun coq-indent-region 937,39026

coq/coq-local-vars.el,229
(defconst coq-local-vars-doc 23,470
(defun coq-insert-coq-prog-name 86,2815
(defun coq-read-directory 99,3383
(defun coq-ask-load-path 116,4198
(defun coq-ask-prog-name 135,5165
(defun coq-ask-insert-coq-prog-name 152,5876

coq/coq-par-compile.el,2021
(defcustom coq-max-background-compilation-jobs 224,10071
(defvar coq-par-ancestor-files 230,10265
(defvar coq-current-background-jobs 246,10914
(defvar coq-compilation-object-hash 249,11003
(defvar coq-last-compilation-job 257,11376
(defvar coq-par-next-id 261,11519
(defun split-list-at-predicate 268,11676
(defun coq-par-time-less 292,12528
(defun coq-par-init-compilation-hash 302,12876
(defun coq-par-init-ancestor-hash 306,13037
(defconst coq-par-empty-compilation-queue 317,13322
(defvar coq-par-compilation-queue320,13431
(defun coq-par-enqueue 325,13617
(defun coq-par-dequeue 331,13851
(defun coq-par-coq-arguments 366,14905
(defun coq-par-analyse-coq-dep-exit 374,15274
(defun coq-par-get-library-dependencies 393,16057
(defun coq-par-map-module-id-to-obj-file 437,18027
(defun coq-par-kill-all-processes 496,20856
(defun coq-par-unlock-ancestors-on-error 506,21188
(defun coq-par-emergency-cleanup 516,21531
(defun coq-par-process-filter 532,22152
(defun coq-par-start-process 537,22361
(defun coq-par-process-sentinel 563,23623
(defun coq-par-job-is-ready 598,24927
(defun coq-par-dependencies-ready 602,25033
(defun coq-par-add-coqc-dependency 606,25177
(defun coq-par-add-queue-dependency 615,25590
(defun coq-par-get-obj-mod-time 625,26056
(defun coq-par-job-needs-compilation 639,26586
(defun coq-par-kickoff-queue-maybe 668,27817
(defun coq-par-compile-job-maybe 733,30617
(defun coq-par-decrease-coqc-dependency 747,31288
(defun coq-par-kickoff-coqc-dependants 782,33058
(defun coq-par-start-coqdep 824,34988
(defun coq-par-start-task 840,35644
(defun coq-par-start-jobs-until-full 856,36205
(defun coq-par-start-or-enqueue 866,36521
(defun coq-par-create-library-job 875,36922
(defun coq-par-process-coqdep-result 947,40080
(defun coq-par-coqc-continuation 1004,42525
(defun coq-par-handle-module 1027,43371
(defun coq-par-handle-require-list 1055,44571
(defun coq-par-item-require-predicate 1101,46629
(defun coq-par-preprocess-require-commands 1110,46952

coq/coq-seq-compile.el,422
(defun coq-seq-lock-ancestor 38,1174
(defun coq-seq-get-library-dependencies 56,2005
(defun coq-seq-compile-library 109,4420
(defun coq-seq-compile-library-if-necessary 136,5649
(defun coq-seq-make-lib-up-to-date 182,7533
(defun coq-seq-auto-compile-externally 240,10027
(defun coq-seq-map-module-id-to-obj-file 284,12191
(defun coq-seq-check-module 337,14809
(defun coq-seq-preprocess-require-commands 365,16275

coq/coq-smie-lexer.el,862
(defconst coq-smie-dot-friends 21,987
(defun coq-time-indent 26,1163
(defun coq-time-indent-region 32,1304
(defun coq-smie-is-tactic 41,1475
(defun coq-smie-.-deambiguate 51,1708
(defun coq-smie-complete-qualid-backward 80,2425
(defun coq-smie-find-unclosed-match-backward 88,2645
(defun coq-smie-with-deambiguate(98,2973
(defun coq-smie-search-token-forward 116,3538
(defun coq-smie-search-token-backward 161,5463
(defun coq-lonely-:=205,7371
(defun coq-smie-detect-goal-command 222,8132
(defun coq-smie-module-deambiguate 236,8795
(defconst coq-smie-proof-end-tokens255,9691
(defun coq-smie-forward-token 259,9842
(defun coq-is-at-command-real-start(334,12771
(defun coq-smie-:=339,12871
(defun coq-smie-backward-token 375,14320
(defcustom coq-indent-box-style 565,20606
(defconst coq-smie-grammar583,21035
(defun coq-smie-rules 705,26030

coq/coq-syntax.el,2786
(defcustom coq-user-tactics-db 21,586
(defcustom coq-user-commands-db 38,1099
(defcustom coq-user-tacticals-db 54,1618
(defcustom coq-user-solve-tactics-db 70,2139
(defcustom coq-user-cheat-tactics-db 86,2658
(defcustom coq-user-reserved-db 105,3204
(defvar coq-tactics-db123,3735
(defvar coq-solve-tactics-db296,12869
(defvar coq-solve-cheat-tactics-db323,13892
(defvar develock-coq-font-lock-keywords331,14098
(defvar coq-tacticals-db342,14405
(defvar coq-decl-db366,15291
(defvar coq-defn-db391,16747
(defvar coq-goal-starters-db456,21469
(defvar coq-other-commands-db486,23272
(defvar coq-commands-db621,33257
(defvar coq-terms-db628,33477
(defun coq-count-match 690,36092
(defun coq-module-opening-p 706,36821
(defun coq-section-command-p 716,37255
(defun coq-goal-command-str-p 720,37352
(defun coq-goal-command-p 746,38677
(defvar coq-keywords-save-strict755,39021
(defvar coq-keywords-save762,39262
(defun coq-save-command-p 767,39341
(defvar coq-keywords-kill-goal778,39669
(defvar coq-keywords-state-changing-misc-commands782,39759
(defvar coq-keywords-goal785,39884
(defvar coq-keywords-decl788,39967
(defvar coq-keywords-defn791,40041
(defvar coq-keywords-state-changing-commands795,40116
(defvar coq-keywords-state-preserving-commands804,40376
(defvar coq-keywords-commands809,40592
(defvar coq-solve-tactics814,40740
(defvar coq-solve-tactics-regexp818,40861
(defvar coq-solve-cheat-tactics822,40995
(defvar coq-solve-cheat-tactics-regexp826,41140
(defvar coq-tacticals830,41298
(defvar coq-reserved836,41437
(defvar coq-reserved-regexp 846,41772
(defvar coq-state-changing-tactics850,41883
(defvar coq-state-preserving-tactics853,41992
(defvar coq-tactics857,42106
(defvar coq-tactics-regexp 860,42195
(defvar coq-retractable-instruct863,42350
(defvar coq-non-retractable-instruct866,42460
(defvar coq-keywords870,42588
(defun proof-regexp-alt-list-symb 876,42812
(defvar coq-keywords-regexp 879,42917
(defvar coq-symbols882,42990
(defvar coq-error-regexp 904,43231
(defvar coq-id 907,43459
(defvar coq-id-shy 908,43484
(defvar coq-ids 911,43577
(defun coq-first-abstr-regexp 913,43643
(defcustom coq-variable-highlight-enable 916,43738
(defvar coq-font-lock-terms922,43865
(defconst coq-save-command-regexp-strict944,44948
(defconst coq-save-command-regexp950,45116
(defconst coq-save-with-hole-regexp955,45269
(defconst coq-goal-command-regexp959,45429
(defconst coq-goal-with-hole-regexp962,45531
(defconst coq-decl-with-hole-regexp966,45665
(defconst coq-defn-with-hole-regexp973,45915
(defconst coq-with-with-hole-regexp983,46205
(defvar coq-font-lock-keywords-1998,46735
(defvar coq-font-lock-keywords 1026,48070
(defun coq-init-syntax-table 1028,48128
(defconst coq-generic-expression1053,48855

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,6808
(defconst coq-control-char-format 258,6933
(defconst coq-control-characters260,6976
(defconst coq-control-region-format-regexp 264,7068
(defconst coq-control-regions266,7151

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,1255
(defgroup isabelle 31,882
(defcustom isabelle-web-page35,1010
(defcustom isa-isabelle-command44,1227
(defvar isabelle-not-found 62,1909
(defun isa-set-isabelle-command 65,2024
(defun isa-shell-command-to-string 88,3042
(defun isa-getenv 94,3266
(defcustom isabelle-program-name-override 114,3965
(defun isa-tool-list-logics 125,4311
(defcustom isabelle-logics-available 132,4557
(defcustom isabelle-chosen-logic 142,4894
(defvar isabelle-chosen-logic-prev 158,5478
(defun isabelle-hack-local-variables-function 161,5598
(defun isabelle-set-prog-name 173,6037
(defun isabelle-choose-logic 197,7157
(defun isa-view-doc 216,7919
(defun isa-tool-list-docs 223,8145
(defconst isabelle-verbatim-regexp 241,8875
(defun isabelle-verbatim 244,9017
(defcustom isabelle-refresh-logics 251,9178
(defvar isabelle-docs-menu259,9506
(defvar isabelle-logics-menu-entries 266,9809
(defun isabelle-logics-menu-calculate 269,9882
(defvar isabelle-time-to-refresh-logics 290,10524
(defun isabelle-logics-menu-refresh 294,10619
(defun isabelle-menu-bar-update-logics 309,11266
(defun isabelle-load-isar-keywords 325,11895
(defun isabelle-create-span-menu 346,12623
(defun isabelle-xml-sml-escapes 362,13054
(defun isabelle-process-pgip 365,13155

isar/isar-autotest.el,31
(defvar isar-long-tests 8,186

isar/isar.el,1595
(defcustom isar-keywords-name 41,939
(defpgdefault completion-table 57,1450
(defcustom isar-web-page59,1503
(defun isar-strip-terminators 73,1853
(defun isar-markup-ml 85,2209
(defun isar-mode-config-set-variables 90,2344
(defun isar-shell-mode-config-set-variables 155,5143
(defun isar-set-proof-find-theorems-command 237,8333
(defpacustom use-find-theorems-form 243,8517
(defun isar-set-undo-commands 248,8683
(defpacustom use-linear-undo 263,9316
(defun isar-configure-from-settings 268,9474
(defun isar-remove-file 276,9624
(defun isar-shell-compute-new-files-list 288,9928
(define-derived-mode isar-shell-mode 307,10498
(define-derived-mode isar-response-mode 312,10625
(define-derived-mode isar-goals-mode 317,10758
(define-derived-mode isar-mode 322,10884
(defpgdefault menu-entries374,12599
(defun isar-set-command 405,13793
(defpgdefault help-menu-entries 410,13923
(defun isar-count-undos 413,13999
(defun isar-find-and-forget 439,14965
(defun isar-goal-command-p 475,16308
(defun isar-global-save-command-p 480,16485
(defvar isar-current-goal 501,17269
(defun isar-state-preserving-p 504,17335
(defvar isar-shell-current-line-width 529,18184
(defun isar-shell-adjust-line-width 534,18376
(defsubst isar-string-wrapping 557,19141
(defsubst isar-positions-of 566,19335
(defcustom isar-wrap-commands-singly 572,19540
(defun isar-command-wrapping 578,19736
(defun isar-preprocessing 586,20050
(defun isar-mode-config 604,20601
(defun isar-shell-mode-config 618,21254
(defun isar-response-mode-config 628,21603
(defun isar-goals-mode-config 638,21938

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,539
(defcustom lego-test-all-name 26,675
(defpgdefault help-menu-entries32,833
(defpgdefault menu-entries36,993
(defvar lego-shell-handle-output47,1294
(defconst lego-process-config55,1604
(defconst lego-pretty-set-width 66,2035
(defconst lego-interrupt-regexp 70,2177
(defcustom lego-www-home-page 75,2294
(defcustom lego-www-latest-release80,2418
(defcustom lego-www-refcard86,2593
(defcustom lego-library-www-page92,2742
(defvar lego-prog-name 101,2958
(defvar lego-shell-cd 104,3027
(defvar lego-shell-proof-completed-regexp 107,3126
(defvar lego-save-command-regexp110,3266
(defvar lego-goal-command-regexp112,3356
(defvar lego-kill-goal-command 115,3447
(defvar lego-forget-id-command 116,3490
(defvar lego-undoable-commands-regexp118,3536
(defvar lego-goal-regexp 127,3910
(defvar lego-outline-regexp129,3955
(defvar lego-outline-heading-end-regexp 135,4130
(defvar lego-shell-outline-regexp 137,4183
(defvar lego-shell-outline-heading-end-regexp 138,4235
(define-derived-mode lego-shell-mode 144,4514
(define-derived-mode lego-mode 151,4675
(define-derived-mode lego-goals-mode 162,4985
(defun lego-count-undos 173,5411
(defun lego-goal-command-p 192,6148
(defun lego-find-and-forget 197,6319
(defun lego-goal-hyp 239,8155
(defun lego-state-preserving-p 248,8352
(defvar lego-shell-current-line-width 264,9055
(defun lego-shell-adjust-line-width 272,9362
(defun lego-mode-config 289,10063
(defun lego-equal-module-filename 357,12114
(defun lego-shell-compute-new-files-list 363,12389
(defun lego-shell-mode-config 373,12772
(defun lego-goals-mode-config 420,14439

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

hol-light/hol-light.el,1930
(defcustom hol-light-home 23,676
(defcustom hol-light-prog-name 30,877
(defcustom hol-light-use-custom-toplevel 38,1073
(defconst hol-light-pre-sync-cmd52,1569
(defcustom hol-light-init-cmd 56,1743
(defconst hol-light-plain-start-goals-regexp78,2474
(defconst hol-light-annotated-start-goals-regexp 85,2720
(defconst hol-light-plain-interrupt-regexp89,2879
(defconst hol-light-annotated-interrupt-regexp93,3010
(defconst hol-light-plain-prompt-regexp97,3172
(defconst hol-light-annotated-prompt-regexp101,3326
(defconst hol-light-plain-error-regexp105,3498
(defconst hol-light-annotated-error-regexp 116,3823
(defconst hol-light-plain-proof-completed-regexp121,4044
(defconst hol-light-annotated-proof-completed-regexp125,4197
(defconst hol-light-plain-message-start 129,4378
(defconst hol-light-annotated-message-start133,4522
(defconst hol-light-plain-message-end137,4676
(defconst hol-light-annotated-message-end141,4807
(defvar hol-light-keywords 150,4963
(defvar hol-light-rules 151,4995
(defvar hol-light-tactics 152,5024
(defvar hol-light-tacticals 153,5055
(defvar hol-light-update-goal-regexp 365,13124
(defconst hol-light-current-goal-regexp369,13250
(defconst hol-light-additional-subgoal-regexp 375,13444
(defconst hol-light-statenumber-regexp 379,13600
(defconst hol-light-existential-regexp 386,13904
(defconst hol-light-existentials-state-start-regexp 389,14011
(defconst hol-light-existentials-state-end-regexp 392,14158
(defvar proof-shell-delayed-output-start 424,15449
(defvar proof-shell-delayed-output-end 425,15495
(defvar proof-info 426,15539
(defvar proof-action-list 427,15563
(defun proof-shell-action-list-item 428,15594
(defconst hol-light-show-sequent-command 430,15645
(defun hol-light-get-proof-info 432,15713
(defun hol-light-find-begin-of-unfinished-proof 448,16214
(defun hol-light-proof-tree-get-new-subgoals 459,16662
(defpgdefault menu-entries509,18884

hol-light/hol-light-unicode-tokens.el,516
(defconst hol-light-token-format 23,746
(defconst hol-light-token-match 24,800
(defconst hol-light-hexcode-match 25,837
(defun hol-light-unicode-tokens-set 27,877
(defcustom hol-light-token-symbol-map33,1117
(defcustom hol-light-shortcut-alist128,3379
(defconst hol-light-control-char-format-regexp217,5409
(defconst hol-light-control-char-format 221,5540
(defconst hol-light-control-characters223,5589
(defconst hol-light-control-region-format-regexp 227,5687
(defconst hol-light-control-regions229,5776

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 21,583
(defun phox-lang-suppress 26,677
(defun phox-lang-opendef 31,874
(defun phox-lang-instance 36,992
(defun phox-lang-open-instance 41,1121
(defun phox-lang-lock 46,1270
(defun phox-lang-unlock 51,1400
(defun phox-lang-prove 56,1536
(defun phox-lang-let 61,1670

phox/phox-outline.el,254
(defconst phox-outline-title-regexp 19,723
(defconst phox-outline-section-regexp 20,788
(defconst phox-outline-save-regexp 21,844
(defconst phox-outline-heading-end-regexp 38,1387
(defun phox-outline-level(44,1566
(defun phox-setup-outline 58,2040

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,1201
(defconst proof-toolbar-entries-default42,1338
(defpgcustom toolbar-entries 71,3173
(defpgcustom prog-args 90,3906
(defpgcustom prog-env 102,4484
(defpgcustom quit-timeout 111,4913
(defpgcustom favourites 123,5340
(defpgcustom menu-entries 128,5529
(defpgcustom help-menu-entries 135,5765
(defpgcustom keymap 142,6028
(defpgcustom completion-table 147,6199
(defpgcustom tags-program 158,6575
(defpgcustom use-holes 167,6959
(defpgcustom one-command-per-line174,7217
(defpgcustom maths-menu-enable 185,7453
(defpgcustom unicode-tokens-enable 191,7633
(defpgcustom mmm-enable 197,7840

generic/pg-goals.el,285
(define-derived-mode proof-goals-mode 29,736
(define-key proof-goals-mode-map 56,1612
(define-key proof-goals-mode-map 58,1728
(define-key proof-goals-mode-map 59,1796
(defun proof-goals-config-done 68,1943
(defun pg-goals-display 76,2209
(defun pg-goals-button-action 119,3668

generic/pg-movie.el,333
(defconst pg-movie-xml-header 32,923
(defconst pg-movie-stylesheet34,981
(defun pg-movie-stylesheet-location 37,1080
(defvar pg-movie-frame 41,1188
(defun pg-movie-of-span 43,1242
(defun pg-movie-of-region 79,2362
(defun pg-movie-export 86,2550
(defun pg-movie-export-from 108,3154
(defun pg-movie-export-directory 119,3475

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,2932
(defalias 'pg-pgip-debug pg-pgip-debug
39,1091
(defalias 'pg-pgip-error pg-pgip-error
40,1132
(defalias 'pg-pgip-warning pg-pgip-warning
41,1167
(defconst pg-pgip-version-supported 43,1217
(defun pg-pgip-process-packet 47,1323
(defvar pg-pgip-last-seen-id 57,1891
(defvar pg-pgip-last-seen-seq 58,1925
(defun pg-pgip-process-pgip 60,1961
(defun pg-pgip-process-msg 79,2901
(defvar pg-pgip-post-process-functions94,3492
(defun pg-pgip-post-process 104,3967
(defun pg-pgip-process-askpgip 121,4582
(defun pg-pgip-process-usespgip 127,4786
(defun pg-pgip-process-usespgml 131,4950
(defun pg-pgip-process-pgmlconfig 135,5114
(defun pg-pgip-process-proverinfo 151,5731
(defun pg-pgip-process-hasprefs 168,6396
(defun pg-pgip-haspref 182,7028
(defun pg-pgip-process-prefval 200,7744
(defun pg-pgip-process-guiconfig 227,8452
(defvar proof-assistant-idtables 234,8569
(defun pg-pgip-process-ids 237,8686
(defun pg-complete-idtable-symbol 263,9758
(defalias 'pg-pgip-process-setids pg-pgip-process-setids
268,9850
(defalias 'pg-pgip-process-addids pg-pgip-process-addids
269,9906
(defalias 'pg-pgip-process-delids pg-pgip-process-delids
270,9962
(defun pg-pgip-process-idvalue 273,10020
(defun pg-pgip-process-menuadd 285,10366
(defun pg-pgip-process-menudel 288,10409
(defun pg-pgip-process-ready 297,10641
(defun pg-pgip-process-cleardisplay 300,10682
(defun pg-pgip-process-proofstate 314,11139
(defun pg-pgip-process-normalresponse 318,11216
(defun pg-pgip-process-errorresponse 322,11346
(defun pg-pgip-process-scriptinsert 326,11475
(defun pg-pgip-process-metainforesponse 331,11609
(defun pg-pgip-file-of-url 340,11849
(defun pg-pgip-process-informfileloaded 345,11984
(defun pg-pgip-process-informfileretracted 351,12216
(defun pg-pgip-process-brokerstatus 364,12663
(defun pg-pgip-process-proveravailmsg 367,12711
(defun pg-pgip-process-newprovermsg 370,12761
(defun pg-pgip-process-proverstatusmsg 373,12809
(defvar pg-pgip-srcids 382,13055
(defun pg-pgip-process-newfile 386,13162
(defun pg-pgip-process-filestatus 402,13744
(defun pg-pgip-process-newobj 422,14398
(defun pg-pgip-process-delobj 425,14440
(defun pg-pgip-process-objectstatus 428,14482
(defun pg-pgip-process-parsescript 442,14834
(defun pg-pgip-get-pgiptype 465,15708
(defun pg-pgip-default-for 486,16571
(defun pg-pgip-subst-for 499,16966
(defun pg-pgip-interpret-value 512,17336
(defun pg-pgip-interpret-choice 531,18061
(defun pg-pgip-string-of-command 562,19078
(defconst pg-pgip-id579,19839
(defvar pg-pgip-refseq 585,20119
(defvar pg-pgip-refid 587,20216
(defvar pg-pgip-seq 590,20308
(defun pg-pgip-assemble-packet 592,20372
(defun pg-pgip-issue 610,21183
(defun pg-pgip-maybe-askpgip 627,21795
(defun pg-pgip-askprefs 633,21986
(defun pg-pgip-askids 637,22100
(defun pg-pgip-reset 650,22388
(defconst pg-pgip-start-element-regexp 681,23086
(defconst pg-pgip-end-element-regexp 682,23138

generic/pg-response.el,1254
(deflocal pg-response-eagerly-raise 32,791
(define-derived-mode proof-response-mode 42,1016
(define-key proof-response-mode-map 69,1971
(define-key proof-response-mode-map 70,2042
(define-key proof-response-mode-map 71,2096
(defun proof-response-config-done 75,2182
(defvar pg-response-special-display-regexp 86,2528
(defconst proof-multiframe-parameters90,2695
(defun proof-multiple-frames-enable 99,2985
(defun proof-three-window-enable 109,3313
(defun proof-select-three-b 112,3376
(defun proof-display-three-b 157,4806
(defvar pg-frame-configuration 167,5174
(defun pg-cache-frame-configuration 171,5321
(defun proof-layout-windows 175,5492
(defun proof-delete-other-frames 241,8163
(defvar pg-response-erase-flag 272,9251
(defun pg-response-maybe-erase276,9380
(defun pg-response-display 320,10843
(defun pg-response-display-with-face 345,11626
(defun pg-response-clear-displays 373,12472
(defun pg-response-message 391,13178
(defun pg-response-warning 397,13413
(defun proof-next-error 412,13819
(defun pg-response-has-error-location 490,16628
(defcustom proof-trace-buffer-max-lines 505,17047
(defun proof-trace-buffer-display 512,17282
(defun proof-trace-buffer-finish 526,17689
(defun pg-thms-buffer-clear 550,18342

generic/pg-user.el,3669
(defvar which-func-modes)28,748
(defun proof-script-new-command-advance 43,1241
(defun proof-maybe-follow-locked-end 69,2268
(defun proof-goto-command-start 95,3104
(defun proof-goto-command-end 118,4051
(defun proof-forward-command 133,4473
(defun proof-backward-command 154,5194
(defun proof-goto-point 165,5408
(defun proof-assert-next-command-interactive 179,5842
(defun proof-assert-until-point-interactive 191,6328
(defun proof-process-buffer 198,6573
(defun proof-undo-last-successful-command 216,7085
(defun proof-undo-and-delete-last-successful-command 221,7247
(defun proof-undo-last-successful-command-1 233,7766
(defun proof-retract-buffer 250,8430
(defun proof-retract-current-goal 265,9038
(defun proof-mouse-goto-point 284,9558
(defvar proof-minibuffer-history 299,9834
(defun proof-minibuffer-cmd 302,9929
(defun proof-frob-locked-end 341,11336
(defmacro proof-if-setting-configured 377,12437
(defmacro proof-define-assistant-command 385,12706
(defmacro proof-define-assistant-command-witharg 398,13161
(defun proof-issue-new-command 418,13983
(defun proof-cd-sync 458,15206
(defun proof-electric-terminator-enable 509,16805
(defun proof-electric-terminator 517,17109
(defun proof-add-completions 545,18079
(defun proof-script-complete 568,18902
(defun pg-copy-span-contents 582,19211
(defun pg-numth-span-higher-or-lower 596,19635
(defun pg-control-span-of 622,20381
(defun pg-move-span-contents 628,20585
(defun pg-fixup-children-spans 679,22703
(defun pg-move-region-down 689,22960
(defun pg-move-region-up 698,23253
(defun pg-pos-for-event 712,23527
(defun pg-span-for-event 718,23748
(defun pg-span-context-menu 722,23892
(defun pg-toggle-visibility 738,24409
(defun pg-create-in-span-context-menu 747,24716
(defun pg-span-undo 772,25744
(defun pg-goals-buffers-hint 785,25982
(defun pg-slow-fontify-tracing-hint 789,26200
(defun pg-response-buffers-hint 793,26389
(defun pg-jump-to-end-hint 805,26804
(defun pg-processing-complete-hint 809,26933
(defun pg-next-error-hint 826,27653
(defun pg-hint 831,27805
(defun pg-identifier-under-mouse-query 842,28154
(defun pg-identifier-near-point-query 853,28478
(defvar proof-query-identifier-history 882,29401
(defun proof-query-identifier 885,29488
(defun pg-identifier-query 896,29844
(defun proof-imenu-enable 929,30992
(defvar pg-input-ring 969,32470
(defvar pg-input-ring-index 972,32527
(defvar pg-stored-incomplete-input 975,32599
(defun pg-previous-input 978,32702
(defun pg-next-input 992,33165
(defun pg-delete-input 997,33287
(defun pg-get-old-input 1010,33625
(defun pg-restore-input 1024,34016
(defun pg-search-start 1035,34306
(defun pg-regexp-arg 1047,34798
(defun pg-search-arg 1059,35246
(defun pg-previous-matching-input-string-position 1073,35663
(defun pg-previous-matching-input 1100,36828
(defun pg-next-matching-input 1119,37678
(defvar pg-matching-input-from-input-string 1127,38061
(defun pg-previous-matching-input-from-input 1131,38175
(defun pg-next-matching-input-from-input 1149,38940
(defun pg-add-to-input-history 1160,39319
(defun pg-remove-from-input-history 1172,39772
(defun  pg-clear-input-ring 1183,40152
(define-key proof-mode-map 1200,40622
(define-key proof-mode-map 1201,40682
(defun pg-protected-undo 1203,40754
(defun pg-protected-undo-1 1233,42048
(defun next-undo-elt 1264,43485
(defvar proof-autosend-timer 1291,44441
(deflocal proof-autosend-modified-tick 1293,44502
(defun proof-autosend-enable 1297,44624
(defun proof-autosend-delay 1311,45167
(defun proof-autosend-loop 1315,45300
(defun proof-autosend-loop-all 1329,45860
(defun proof-autosend-loop-next 1353,46640

generic/pg-vars.el,1500
(defvar proof-assistant-cusgrp 22,386
(defvar proof-assistant-internals-cusgrp 28,646
(defvar proof-assistant 34,916
(defvar proof-assistant-symbol 39,1139
(defvar proof-mode-for-shell 52,1681
(defvar proof-mode-for-response 57,1871
(defvar proof-mode-for-goals 62,2097
(defvar proof-mode-for-script 67,2286
(defvar proof-ready-for-assistant-hook 72,2463
(defvar proof-shell-busy 83,2751
(defvar proof-shell-last-queuemode 101,3422
(defvar proof-included-files-list 105,3577
(defvar proof-script-buffer 127,4596
(defvar proof-previous-script-buffer 130,4688
(defvar proof-shell-buffer 134,4861
(defvar proof-goals-buffer 137,4947
(defvar proof-response-buffer 140,5002
(defvar proof-trace-buffer 143,5063
(defvar proof-thms-buffer 147,5217
(defvar proof-shell-error-or-interrupt-seen 151,5372
(defvar pg-response-next-error 156,5596
(defvar proof-shell-proof-completed 159,5703
(defvar proof-shell-silent 173,6088
(defvar proof-shell-last-prompt 176,6176
(defvar proof-shell-last-output 180,6346
(defvar proof-shell-last-output-kind 184,6486
(defvar proof-assistant-settings 204,7250
(defvar pg-tracing-slow-mode 214,7764
(defvar proof-nesting-depth 217,7853
(defvar proof-last-theorem-dependencies 224,8088
(defvar proof-autosend-running 228,8250
(defvar proof-next-command-on-new-line 233,8449
(defcustom proof-general-name 244,8683
(defcustom proof-general-home-page249,8840
(defcustom proof-unnamed-theorem-name255,9000
(defcustom proof-universal-keys261,9184

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 736,23730
(defsubst proof-replace-regexp-in-string 892,29291

generic/proof-auxmodes.el,149
(defun proof-mmm-support-available 20,495
(defun proof-maths-menu-support-available 42,1096
(defun proof-unicode-tokens-support-available 56,1513

generic/proof-config.el,7902
(defgroup prover-config 80,2634
(defcustom proof-guess-command-line 98,3484
(defcustom proof-assistant-home-page 113,3979
(defcustom proof-context-command 119,4149
(defcustom proof-info-command 124,4283
(defcustom proof-showproof-command 131,4554
(defcustom proof-goal-command 136,4690
(defcustom proof-save-command 144,4987
(defcustom proof-find-theorems-command 152,5296
(defcustom proof-query-identifier-command 159,5604
(defcustom proof-assistant-true-value 173,6293
(defcustom proof-assistant-false-value 179,6483
(defcustom proof-assistant-format-int-fn 185,6677
(defcustom proof-assistant-format-float-fn 192,6926
(defcustom proof-assistant-format-string-fn 199,7181
(defcustom proof-assistant-setting-format 206,7448
(defcustom proof-tree-configured 216,7931
(defgroup proof-script 234,8397
(defcustom proof-terminal-string 239,8527
(defcustom proof-electric-terminator-noterminator 249,8915
(defcustom proof-script-sexp-commands 254,9087
(defcustom proof-script-command-end-regexp 265,9546
(defcustom proof-script-command-start-regexp 283,10367
(defcustom proof-script-integral-proofs 294,10830
(defcustom proof-script-fly-past-comments 309,11486
(defcustom proof-script-parse-function 314,11657
(defcustom proof-script-comment-start 332,12302
(defcustom proof-script-comment-start-regexp 343,12739
(defcustom proof-script-comment-end 351,13058
(defcustom proof-script-comment-end-regexp 363,13480
(defcustom proof-string-start-regexp 371,13793
(defcustom proof-string-end-regexp 376,13958
(defcustom proof-case-fold-search 381,14119
(defcustom proof-save-command-regexp 390,14531
(defcustom proof-save-with-hole-regexp 395,14641
(defcustom proof-save-with-hole-result 406,15016
(defcustom proof-goal-command-regexp 416,15460
(defcustom proof-goal-with-hole-regexp 424,15747
(defcustom proof-goal-with-hole-result 436,16190
(defcustom proof-non-undoables-regexp 445,16568
(defcustom proof-nested-undo-regexp 456,17031
(defcustom proof-ignore-for-undo-count 472,17751
(defcustom proof-script-imenu-generic-expression 480,18062
(defcustom proof-goal-command-p 488,18401
(defcustom proof-really-save-command-p 499,18892
(defcustom proof-completed-proof-behaviour 508,19199
(defcustom proof-count-undos-fn 536,20548
(defcustom proof-find-and-forget-fn 548,21099
(defcustom proof-forget-id-command 565,21808
(defcustom pg-topterm-goalhyplit-fn 575,22166
(defcustom proof-kill-goal-command 587,22709
(defcustom proof-undo-n-times-cmd 601,23213
(defcustom proof-nested-goals-history-p 615,23750
(defcustom proof-arbitrary-undo-positions 624,24087
(defcustom proof-state-preserving-p 638,24668
(defcustom proof-activate-scripting-hook 648,25140
(defcustom proof-deactivate-scripting-hook 667,25921
(defcustom proof-no-fully-processed-buffer 676,26251
(defcustom proof-script-evaluate-elisp-comment-regexp 687,26749
(defcustom proof-indent 705,27335
(defcustom proof-indent-hang 710,27442
(defcustom proof-indent-enclose-offset 715,27568
(defcustom proof-indent-open-offset 720,27710
(defcustom proof-indent-close-offset 725,27847
(defcustom proof-indent-any-regexp 730,27985
(defcustom proof-indent-inner-regexp 735,28145
(defcustom proof-indent-enclose-regexp 740,28299
(defcustom proof-indent-open-regexp 745,28453
(defcustom proof-indent-close-regexp 750,28605
(defcustom proof-script-font-lock-keywords 756,28759
(defcustom proof-script-syntax-table-entries 764,29111
(defcustom proof-script-span-context-menu-extensions 782,29507
(defgroup proof-shell 808,30267
(defcustom proof-prog-name 818,30437
(defcustom proof-shell-auto-terminate-commands 830,30904
(defcustom proof-shell-pre-sync-init-cmd 839,31309
(defcustom proof-shell-init-cmd 853,31867
(defcustom proof-shell-init-hook 865,32413
(defcustom proof-shell-restart-cmd 870,32552
(defcustom proof-shell-quit-cmd 875,32707
(defcustom proof-shell-cd-cmd 880,32874
(defcustom proof-shell-start-silent-cmd 897,33545
(defcustom proof-shell-stop-silent-cmd 906,33921
(defcustom proof-shell-silent-threshold 915,34256
(defcustom  proof-shell-inform-file-processed-cmd 923,34590
(defcustom  proof-shell-inform-file-retracted-cmd 944,35518
(defcustom proof-auto-multiple-files 972,36790
(defcustom proof-cannot-reopen-processed-files 987,37511
(defcustom proof-shell-annotated-prompt-regexp 1007,38302
(defcustom proof-shell-error-regexp 1022,38867
(defcustom proof-shell-truncate-before-error 1042,39677
(defcustom pg-next-error-regexp 1056,40216
(defcustom pg-next-error-filename-regexp 1071,40825
(defcustom pg-next-error-extract-filename 1095,41858
(defcustom proof-shell-interrupt-regexp 1102,42101
(defcustom proof-shell-proof-completed-regexp 1116,42704
(defcustom proof-shell-clear-response-regexp 1129,43220
(defcustom proof-shell-clear-goals-regexp 1141,43680
(defcustom proof-shell-start-goals-regexp 1153,44134
(defcustom proof-shell-end-goals-regexp 1166,44709
(defcustom proof-shell-eager-annotation-start 1180,45299
(defcustom proof-shell-eager-annotation-start-length 1203,46318
(defcustom proof-shell-eager-annotation-end 1214,46744
(defcustom proof-shell-strip-output-markup 1230,47419
(defcustom proof-shell-assumption-regexp 1239,47804
(defcustom proof-shell-process-file 1249,48208
(defcustom proof-shell-retract-files-regexp 1275,49284
(defcustom proof-shell-compute-new-files-list 1288,49772
(defcustom pg-special-char-regexp 1303,50339
(defcustom proof-shell-set-elisp-variable-regexp 1308,50483
(defcustom proof-shell-match-pgip-cmd 1346,52157
(defcustom proof-shell-issue-pgip-cmd 1360,52647
(defcustom proof-use-pgip-askprefs 1365,52820
(defcustom proof-shell-query-dependencies-cmd 1373,53167
(defcustom proof-shell-theorem-dependency-list-regexp 1380,53427
(defcustom proof-shell-theorem-dependency-list-split 1396,54095
(defcustom proof-shell-show-dependency-cmd 1405,54526
(defcustom proof-shell-trace-output-regexp 1427,55432
(defcustom proof-shell-thms-output-regexp 1445,56034
(defcustom proof-shell-interactive-prompt-regexp 1453,56368
(defcustom proof-tokens-activate-command 1472,57021
(defcustom proof-tokens-deactivate-command 1479,57261
(defcustom proof-tokens-extra-modes 1486,57506
(defcustom proof-shell-unicode 1501,58011
(defcustom proof-shell-filename-escapes 1510,58401
(defcustom proof-shell-process-connection-type 1527,59081
(defcustom proof-shell-strip-crs-from-input 1533,59308
(defcustom proof-shell-strip-crs-from-output 1545,59791
(defcustom proof-shell-extend-queue-hook 1553,60159
(defcustom proof-shell-insert-hook 1563,60589
(defcustom proof-script-preprocess 1606,62687
(defcustom proof-shell-handle-delayed-output-hook1612,62838
(defcustom proof-shell-handle-error-or-interrupt-hook1618,63053
(defcustom proof-shell-signal-interrupt-hook 1636,63799
(defcustom proof-shell-pre-interrupt-hook1647,64268
(defcustom proof-shell-handle-output-system-specific 1655,64539
(defcustom proof-state-change-hook 1678,65512
(defcustom proof-shell-syntax-table-entries 1688,65905
(defgroup proof-goals 1706,66276
(defcustom pg-subterm-first-special-char 1711,66397
(defcustom pg-subterm-anns-use-stack 1719,66709
(defcustom pg-goals-change-goal 1728,67008
(defcustom pbp-goal-command 1733,67124
(defcustom pbp-hyp-command 1738,67288
(defcustom pg-subterm-help-cmd 1743,67458
(defcustom pg-goals-error-regexp 1750,67702
(defcustom proof-shell-result-start 1755,67870
(defcustom proof-shell-result-end 1761,68112
(defcustom pg-subterm-start-char 1767,68325
(defcustom pg-subterm-sep-char 1778,68799
(defcustom pg-subterm-end-char 1784,68978
(defcustom pg-topterm-regexp 1790,69135
(defcustom proof-goals-font-lock-keywords 1805,69735
(defcustom proof-response-font-lock-keywords 1813,70094
(defcustom proof-shell-font-lock-keywords 1821,70456
(defcustom pg-before-fontify-output-hook 1832,70970
(defcustom pg-after-fontify-output-hook 1840,71331

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,193
(defconst proof-easy-config-derived-modes-table17,605
(defun proof-easy-config-define-derived-modes 24,1011
(defun proof-easy-config-check-setup 53,2196
(defmacro proof-easy-config 85,3526

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,2278
(defface proof-declaration-name-face82,2604
(defface proof-tacticals-name-face91,2890
(defface proof-tactics-name-face100,3152
(defface proof-error-face109,3417
(defface proof-warning-face117,3638
(defface proof-eager-annotation-face126,3895
(defface proof-debug-message-face134,4113
(defface proof-boring-face142,4312
(defface proof-mouse-highlight-face150,4504
(defface proof-command-mouse-highlight-face158,4722
(defface proof-region-mouse-highlight-face166,4961
(defface proof-highlight-dependent-face174,5203
(defface proof-highlight-dependency-face182,5410
(defface proof-active-area-face190,5607
(defface proof-script-sticky-error-face198,5919
(defface proof-script-highlight-error-face206,6148
(defconst proof-face-compat-doc 218,6493
(defconst proof-queue-face 219,6573
(defconst proof-locked-face 220,6641
(defconst proof-declaration-name-face 221,6711
(defconst proof-tacticals-name-face 222,6801
(defconst proof-tactics-name-face 223,6887
(defconst proof-error-face 224,6969
(defconst proof-script-sticky-error-face 225,7037
(defconst proof-script-highlight-error-face 226,7133
(defconst proof-warning-face 227,7235
(defconst proof-eager-annotation-face 228,7307
(defconst proof-debug-message-face 229,7397
(defconst proof-boring-face 230,7481
(defconst proof-mouse-highlight-face 231,7551
(defconst proof-command-mouse-highlight-face 232,7639
(defconst proof-region-mouse-highlight-face 233,7743
(defconst proof-highlight-dependent-face 234,7845
(defconst proof-highlight-dependency-face 235,7941
(defconst proof-active-area-face 236,8039
(defconst proof-script-error-face 237,8119

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,3006
(defun proof-menu-define-main 154,5912
(defvar proof-menu-favourites 163,6097
(defvar proof-menu-settings 166,6204
(defun proof-menu-define-specific 170,6293
(defun proof-assistant-menu-update 213,7555
(defvar proof-help-menu227,7988
(defvar proof-show-hide-menu235,8252
(defvar proof-buffer-menu246,8676
(defun proof-keep-response-history 312,11125
(defconst proof-quick-opts-menu320,11435
(defun proof-quick-opts-vars 546,20709
(defun proof-quick-opts-changed-from-defaults-p 578,21649
(defun proof-quick-opts-changed-from-saved-p 582,21754
(defun proof-set-document-centred 590,21910
(defun proof-set-non-document-centred 603,22336
(defun proof-quick-opts-save 622,23047
(defun proof-quick-opts-reset 627,23215
(defconst proof-config-menu639,23483
(defconst proof-advanced-menu646,23662
(defvar proof-menu664,24346
(defun proof-main-menu 673,24628
(defun proof-aux-menu 685,24967
(defun proof-menu-define-favourites-menu 701,25313
(defun proof-def-favourite 721,25962
(defvar proof-make-favourite-cmd-history 748,26955
(defvar proof-make-favourite-menu-history 751,27040
(defun proof-save-favourites 754,27126
(defun proof-del-favourite 759,27274
(defun proof-read-favourite 776,27830
(defun proof-add-favourite 800,28604
(defun proof-menu-define-settings-menu 827,29649
(defun proof-menu-entry-name 856,30641
(defun proof-menu-entry-for-setting 866,30991
(defun proof-settings-vars 889,31629
(defun proof-settings-changed-from-defaults-p 894,31806
(defun proof-settings-changed-from-saved-p 898,31912
(defun proof-settings-save 902,32015
(defun proof-settings-reset 907,32182
(defun proof-assistant-invisible-command-ifposs 912,32345
(defun proof-maybe-askprefs 934,33315
(defun proof-assistant-settings-cmd 950,33932
(defun proof-assistant-settings-cmds 958,34215
(defvar proof-assistant-format-table973,34657
(defun proof-assistant-format-bool 982,35083
(defun proof-assistant-format-int 985,35196
(defun proof-assistant-format-float 988,35288
(defun proof-assistant-format-string 991,35384
(defun proof-assistant-format 994,35482

generic/proof-mmm.el,70
(defun proof-mmm-set-global 43,1439
(defun proof-mmm-enable 58,1978

generic/proof-script.el,5814
(deflocal proof-active-buffer-fake-minor-mode 48,1552
(deflocal proof-script-buffer-file-name 51,1678
(deflocal pg-script-portions 58,2088
(defalias 'proof-active-buffer-fake-minor-modeproof-active-buffer-fake-minor-mode
61,2194
(defun proof-next-element-count 70,2389
(defun proof-element-id 76,2631
(defun proof-next-element-id 80,2800
(deflocal proof-locked-span 116,4104
(deflocal proof-queue-span 123,4370
(deflocal proof-overlay-arrow 132,4856
(defun proof-span-give-warning 138,4983
(defun proof-span-read-only 144,5163
(defun proof-strict-read-only 153,5536
(defsubst proof-set-queue-endpoints 163,5914
(defun proof-set-overlay-arrow 167,6055
(defsubst proof-set-locked-endpoints 178,6393
(defsubst proof-detach-queue 183,6569
(defsubst proof-detach-locked 188,6708
(defsubst proof-set-queue-start 195,6933
(defsubst proof-set-locked-end 199,7059
(defsubst proof-set-queue-end 211,7529
(defun proof-init-segmentation 222,7826
(defun proof-colour-locked 252,9077
(defun proof-colour-locked-span 259,9350
(defun proof-sticky-errors 265,9623
(defun proof-restart-buffers 278,10039
(defun proof-script-buffers-with-spans 302,10972
(defun proof-script-remove-all-spans-and-deactivate 312,11328
(defun proof-script-clear-queue-spans-on-error 316,11518
(defun proof-script-delete-spans 342,12535
(defun proof-script-delete-secondary-spans 347,12734
(defun proof-unprocessed-begin 360,13023
(defun proof-script-end 368,13277
(defun proof-queue-or-locked-end 377,13587
(defun proof-locked-region-full-p 396,14180
(defun proof-locked-region-empty-p 405,14452
(defun proof-only-whitespace-to-locked-region-p 409,14602
(defun proof-in-locked-region-p 419,14951
(defun proof-goto-end-of-locked 431,15208
(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 448,15995
(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 459,16476
(defun proof-end-of-locked-visible-p 471,17016
(defconst pg-idioms 490,17609
(defconst pg-all-idioms 493,17705
(defun pg-clear-script-portions 497,17826
(defun pg-remove-element 503,18061
(defun pg-get-element 511,18364
(defun pg-add-element 521,18679
(defun pg-invisible-prop 569,20641
(defun pg-set-element-span-invisible 574,20842
(defun pg-toggle-element-span-visibility 587,21408
(defun pg-open-invisible-span 592,21569
(defun pg-make-element-invisible 597,21740
(defun pg-make-element-visible 602,21951
(defun pg-toggle-element-visibility 607,22145
(defun pg-show-all-portions 613,22408
(defun pg-show-all-proofs 635,23152
(defun pg-hide-all-proofs 640,23280
(defun pg-add-proof-element 645,23411
(defun pg-span-name 660,24198
(defvar pg-span-context-menu-keymap693,25405
(defun pg-last-output-displayform 700,25643
(defun pg-set-span-helphighlights 723,26534
(defun proof-complete-buffer-atomic 786,28681
(defun proof-register-possibly-new-processed-file815,29951
(defun proof-query-save-this-buffer-p 861,31825
(defun proof-inform-prover-file-retracted 866,32050
(defun proof-auto-retract-dependencies 886,32901
(defun proof-unregister-buffer-file-name 940,35451
(defsubst proof-action-completed 986,37276
(defun proof-protected-process-or-retract 990,37446
(defun proof-deactivate-scripting-auto 1018,38677
(defun proof-deactivate-scripting-query-user-action 1027,39035
(defun proof-deactivate-scripting-choose-action 1071,40544
(defun proof-deactivate-scripting 1083,40929
(defun proof-activate-scripting 1180,45052
(defun proof-toggle-active-scripting 1280,49591
(defun proof-done-advancing 1319,50836
(defun proof-done-advancing-comment 1387,53333
(defun proof-done-advancing-save 1421,54719
(defun proof-make-goalsave1509,58083
(defun proof-get-name-from-goal 1527,58948
(defun proof-done-advancing-autosave 1547,59973
(defun proof-done-advancing-other 1611,62469
(defun proof-segment-up-to-parser 1640,63433
(defun proof-script-generic-parse-find-comment-end 1710,65714
(defun proof-script-generic-parse-cmdend 1719,66128
(defun proof-script-generic-parse-cmdstart 1770,68024
(defun proof-script-generic-parse-sexp 1809,69624
(defun proof-semis-to-vanillas 1821,70090
(defun proof-next-command-new-line 1874,71763
(defun proof-script-next-command-advance 1879,71969
(defun proof-assert-until-point 1898,72469
(defun proof-assert-electric-terminator 1914,73140
(defun proof-assert-semis 1958,74820
(defun proof-retract-before-change 1972,75581
(defun proof-insert-pbp-command 1995,76237
(defun proof-insert-sendback-command 2010,76740
(defun proof-done-retracting 2036,77643
(defun proof-setup-retract-action 2071,79097
(defun proof-last-goal-or-goalsave 2083,79702
(defun proof-retract-target 2107,80614
(defun proof-retract-until-point-interactive 2186,83867
(defun proof-retract-until-point 2195,84274
(define-derived-mode proof-mode 2253,86415
(defun proof-script-set-visited-file-name 2289,87797
(defun proof-script-set-buffer-hooks 2311,88810
(defun proof-script-kill-buffer-fn 2319,89228
(defun proof-config-done-related 2351,90545
(defun proof-generic-goal-command-p 2422,93402
(defun proof-generic-state-preserving-p 2427,93615
(defun proof-generic-count-undos 2436,94132
(defun proof-generic-find-and-forget 2467,95260
(defconst proof-script-important-settings2518,97032
(defun proof-config-done 2533,97578
(defun proof-setup-parsing-mechanism 2605,99856
(defun proof-setup-imenu 2629,100928
(deflocal proof-segment-up-to-cache 2666,102210
(deflocal proof-segment-up-to-cache-start 2670,102353
(deflocal proof-segment-up-to-cache-end 2671,102398
(deflocal proof-last-edited-low-watermark 2672,102441
(defun proof-segment-up-to-using-cache 2674,102489
(defun proof-segment-cache-contents-for 2702,103609
(defun proof-script-after-change-function 2719,104191
(defun proof-script-set-after-change-functions 2731,104698

generic/proof-shell.el,3871
(defvar proof-marker 35,775
(defvar proof-action-list 38,871
(defsubst proof-shell-invoke-callback 80,2584
(defvar proof-second-action-list-active 86,2794
(defvar proof-shell-last-goals-output 108,3747
(defvar proof-shell-last-response-output 111,3827
(defvar proof-shell-delayed-output-start 114,3914
(defvar proof-shell-delayed-output-end 118,4096
(defvar proof-shell-delayed-output-flags 122,4276
(defvar proof-shell-interrupt-pending 125,4401
(defvar proof-shell-exit-in-progress 130,4625
(defcustom proof-shell-active-scripting-indicator142,4970
(defun proof-shell-ready-prover 194,6554
(defsubst proof-shell-live-buffer 208,7093
(defun proof-shell-available-p 215,7313
(defun proof-grab-lock 221,7535
(defun proof-release-lock 231,7964
(defcustom proof-shell-fiddle-frames 241,8138
(defun proof-shell-set-text-representation 246,8296
(defun proof-shell-make-associated-buffers 253,8623
(defun proof-shell-start 269,9289
(defvar proof-shell-kill-function-hooks 431,14814
(defun proof-shell-kill-function 434,14912
(defun proof-shell-clear-state 499,17211
(defun proof-shell-exit 515,17686
(defun proof-shell-bail-out 539,18620
(defun proof-shell-restart 549,19142
(defvar proof-shell-urgent-message-marker 590,20514
(defvar proof-shell-urgent-message-scanner 593,20635
(defun proof-shell-handle-error-output 597,20820
(defun proof-shell-handle-error-or-interrupt 623,21682
(defun proof-shell-error-or-interrupt-action 666,23431
(defun proof-goals-pos 693,24528
(defun proof-pbp-focus-on-first-goal 698,24739
(defsubst proof-shell-string-match-safe 710,25155
(defun proof-shell-handle-immediate-output 714,25316
(defun proof-interrupt-process 781,27923
(defun proof-shell-insert 816,29205
(defun proof-shell-action-list-item 873,31187
(defun proof-shell-set-silent 878,31429
(defun proof-shell-start-silent-item 884,31648
(defun proof-shell-clear-silent 890,31837
(defun proof-shell-stop-silent-item 896,32059
(defsubst proof-shell-should-be-silent 902,32248
(defsubst proof-shell-insert-action-item 914,32821
(defsubst proof-shell-slurp-comments 918,32996
(defun proof-add-to-queue 929,33401
(defun proof-start-queue 985,35507
(defun proof-extend-queue 997,35902
(defun proof-shell-exec-loop 1016,36521
(defun proof-shell-insert-loopback-cmd 1100,39547
(defun proof-shell-process-urgent-message 1125,40711
(defun proof-shell-process-urgent-message-default 1181,42736
(defun proof-shell-process-urgent-message-trace 1197,43320
(defun proof-shell-process-urgent-message-retract 1209,43843
(defun proof-shell-process-urgent-message-elisp 1235,44973
(defun proof-shell-process-urgent-message-thmdeps 1250,45468
(defun proof-shell-process-interactive-prompt-regexp 1260,45812
(defun proof-shell-strip-eager-annotations 1272,46168
(defun proof-shell-filter 1288,46668
(defun proof-shell-filter-first-command 1388,50040
(defun proof-shell-process-urgent-messages 1403,50583
(defun proof-shell-filter-manage-output 1453,52149
(defsubst proof-shell-display-output-as-response 1489,53572
(defun proof-shell-handle-delayed-output 1495,53867
(defvar pg-last-tracing-output-time 1599,57439
(defvar pg-last-trace-output-count 1602,57552
(defconst pg-slow-mode-trigger-count 1605,57637
(defconst pg-slow-mode-duration 1608,57742
(defconst pg-fast-tracing-mode-threshold 1611,57824
(defun pg-tracing-tight-loop 1614,57953
(defun pg-finish-tracing-display 1638,58985
(defun proof-shell-wait 1658,59481
(defun proof-done-invisible 1688,60692
(defun proof-shell-invisible-command 1694,60862
(defun proof-shell-invisible-cmd-get-result 1741,62454
(defun proof-shell-invisible-command-invisible-result 1753,62890
(defun pg-insert-last-output-as-comment 1773,63391
(define-derived-mode proof-shell-mode 1792,63863
(defconst proof-shell-important-settings1829,64890
(defun proof-shell-config-done 1835,65005

generic/proof-site.el,708
(defconst proof-assistant-table-default36,1211
(defconst proof-general-short-version78,2415
(defconst proof-general-version-year 84,2602
(defgroup proof-general 91,2755
(defgroup proof-general-internals 96,2863
(defun proof-home-directory-fn 109,3251
(defcustom proof-home-directory120,3623
(defcustom proof-images-directory129,3989
(defcustom proof-info-directory135,4191
(defun proof-add-to-load-path 150,4667
(defcustom proof-assistant-table177,5517
(defcustom proof-assistants 218,6959
(defun proof-ready-for-assistant 247,8113
(defvar proof-general-configured-provers 298,10348
(defun proof-chose-prover 371,12961
(defun proofgeneral 376,13093
(defun proof-visit-example-file 385,13411

generic/proof-splash.el,991
(defcustom proof-splash-enable 34,1009
(defcustom proof-splash-time 39,1161
(defcustom proof-splash-contents47,1445
(defconst proof-splash-startup-msg91,3010
(defconst proof-splash-welcome 100,3388
(define-derived-mode proof-splash-mode 103,3492
(define-key proof-splash-mode-map 109,3666
(define-key proof-splash-mode-map 110,3718
(defsubst proof-emacs-imagep 115,3845
(defun proof-get-image 120,3970
(defvar proof-splash-timeout-conf 142,4770
(defun proof-splash-centre-spaces 145,4883
(defun proof-splash-remove-screen 172,6039
(defun proof-splash-remove-buffer 189,6695
(defvar proof-splash-seen 200,7083
(defun proof-splash-insert-contents 203,7185
(defun proof-splash-display-screen 243,8315
(defalias 'pg-about pg-about
279,9837
(defun proof-splash-message 282,9903
(defun proof-splash-timeout-waiter 295,10361
(defvar proof-splash-old-frame-title-format 308,10921
(defun proof-splash-set-frame-titles 310,10971
(defun proof-splash-unset-frame-titles 319,11286

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,2402
(defun proof-toolbar-function 34,872
(defun proof-toolbar-icon 38,1019
(defun proof-toolbar-enabler 42,1166
(defun proof-toolbar-make-icon 51,1368
(defun proof-toolbar-make-toolbar-items 60,1676
(defvar proof-toolbar-map 86,2537
(defun proof-toolbar-available-p 89,2636
(defun proof-toolbar-setup 99,2942
(defun proof-toolbar-enable 121,3833
(defalias 'proof-toolbar-undo proof-toolbar-undo
154,4891
(defun proof-toolbar-undo-enable-p 156,4959
(defalias 'proof-toolbar-delete proof-toolbar-delete
163,5117
(defun proof-toolbar-delete-enable-p 165,5198
(defalias 'proof-toolbar-home proof-toolbar-home
173,5380
(defalias 'proof-toolbar-next proof-toolbar-next
177,5447
(defun proof-toolbar-next-enable-p 179,5518
(defalias 'proof-toolbar-goto proof-toolbar-goto
185,5634
(defun proof-toolbar-goto-enable-p 187,5684
(defalias 'proof-toolbar-retract proof-toolbar-retract
192,5769
(defun proof-toolbar-retract-enable-p 194,5826
(defalias 'proof-toolbar-use proof-toolbar-use
200,5945
(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p
201,5997
(defalias 'proof-toolbar-prooftree proof-toolbar-prooftree
205,6080
(defalias 'proof-toolbar-restart proof-toolbar-restart
209,6165
(defalias 'proof-toolbar-goal proof-toolbar-goal
213,6230
(defalias 'proof-toolbar-qed proof-toolbar-qed
217,6288
(defun proof-toolbar-qed-enable-p 219,6337
(defalias 'proof-toolbar-state proof-toolbar-state
227,6499
(defalias 'proof-toolbar-state-enable-p proof-toolbar-state-enable-p
228,6542
(defalias 'proof-toolbar-context proof-toolbar-context
232,6621
(defalias 'proof-toolbar-context-enable-p proof-toolbar-context-enable-p
233,6667
(defalias 'proof-toolbar-command proof-toolbar-command
237,6748
(defalias 'proof-toolbar-command-enable-p proof-toolbar-command-enable-p
238,6804
(defun proof-toolbar-help 242,6909
(defalias 'proof-toolbar-find proof-toolbar-find
248,6989
(defalias 'proof-toolbar-find-enable-p proof-toolbar-find-enable-p
249,7041
(defalias 'proof-toolbar-info proof-toolbar-info
253,7116
(defalias 'proof-toolbar-info-enable-p proof-toolbar-info-enable-p
254,7171
(defalias 'proof-toolbar-visibility proof-toolbar-visibility
258,7269
(defun proof-toolbar-visibility-enable-p 260,7329
(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt
265,7443
(defun proof-toolbar-interrupt-enable-p 266,7504
(defun proof-toolbar-scripting-menu 274,7657

generic/proof-tree.el,3326
(defgroup proof-tree 90,3806
(defcustom proof-tree-program 95,3947
(defcustom proof-tree-arguments 100,4093
(defgroup proof-tree-internals 110,4253
(defcustom proof-tree-ignored-commands-regexp 118,4522
(defcustom proof-tree-navigation-command-regexp 130,5021
(defcustom proof-tree-cheating-regexp 138,5340
(defcustom proof-tree-current-goal-regexp 147,5737
(defcustom proof-tree-update-goal-regexp 157,6139
(defcustom proof-tree-additional-subgoal-ID-regexp 169,6708
(defcustom proof-tree-existential-regexp 177,7027
(defcustom proof-tree-existentials-state-start-regexp 191,7647
(defcustom proof-tree-existentials-state-end-regexp 202,8198
(defcustom proof-tree-proof-finished-regexp 214,8841
(defcustom proof-tree-get-proof-info 219,8988
(defcustom proof-tree-extract-instantiated-existentials 243,10029
(defcustom proof-tree-show-sequent-command 260,10747
(defcustom proof-tree-find-begin-of-unfinished-proof 274,11369
(defcustom proof-tree-urgent-action-hook 285,11932
(defvar proof-tree-external-display 309,12787
(defvar proof-tree-process 320,13292
(defconst proof-tree-process-name 323,13381
(defconst proof-tree-process-buffer326,13480
(defconst proof-tree-emacs-exec-regexp330,13620
(defvar proof-tree-last-state 334,13787
(defvar proof-tree-current-proof 338,13891
(defvar proof-tree-sequent-hash 343,14072
(defvar proof-tree-existentials-alist 358,14779
(defvar proof-tree-existentials-alist-history 369,15278
(defun proof-tree-stop-external-display 378,15497
(defun proof-tree-insert-output 386,15761
(defun proof-tree-process-filter 397,16144
(defun proof-tree-process-sentinel 423,16842
(defun proof-tree-start-process 431,17168
(defun proof-tree-is-running 460,18351
(defun proof-tree-ensure-running 465,18512
(defconst proof-tree-protocol-version 475,18716
(defun proof-tree-send-message 480,18916
(defun proof-tree-send-configure 494,19402
(defun proof-tree-send-goal-state 502,19619
(defun proof-tree-send-update-sequent 528,20668
(defun proof-tree-send-switch-goal 541,21105
(defun proof-tree-send-proof-finished 550,21431
(defun proof-tree-send-proof-complete 564,21943
(defun proof-tree-send-undo 572,22192
(defun proof-tree-send-quit-proof 577,22374
(defun proof-tree-record-existentials-state 588,22709
(defun proof-tree-undo-state-var 601,23259
(defun proof-tree-undo-existentials 620,24040
(defun proof-tree-delete-existential-assoc 628,24355
(defun proof-tree-add-existential-assoc 634,24618
(defun proof-tree-clear-existentials 647,25233
(defun proof-tree-show-goal-callback 657,25501
(defun proof-tree-make-show-goal-callback 678,26488
(defun proof-tree-urgent-action 682,26649
(defun proof-tree-quit-proof 747,29185
(defun proof-tree-register-existentials 757,29604
(defun proof-tree-extract-goals 770,30148
(defun proof-tree-extract-list 792,31093
(defun proof-tree-extract-existential-info 815,32063
(defun proof-tree-handle-proof-progress 835,32934
(defun proof-tree-handle-navigation 886,34970
(defun proof-tree-handle-proof-command 904,35696
(defun proof-tree-handle-undo 919,36358
(defun proof-tree-update-sequent 951,37657
(defun proof-tree-handle-delayed-output 992,39425
(defun proof-tree-leave-buffer 1045,41537
(defun proof-tree-display-current-proof 1057,41820
(defun proof-tree-external-display-toggle 1089,43161

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,1785
(defgroup proof-user-options 21,566
(defun proof-set-value 29,745
(defcustom proof-electric-terminator-enable 62,1868
(defcustom proof-next-command-insert-space 74,2400
(defcustom proof-toolbar-enable 82,2730
(defcustom proof-imenu-enable 88,2903
(defcustom pg-show-hints 94,3074
(defcustom proof-shell-quiet-errors 99,3207
(defcustom proof-trace-output-slow-catchup 106,3478
(defcustom proof-strict-state-preserving 116,3975
(defcustom proof-strict-read-only 129,4584
(defcustom proof-three-window-enable 142,5163
(defcustom proof-multiple-frames-enable 161,5911
(defcustom proof-layout-windows-on-visit-file 171,6306
(defcustom proof-three-window-mode-policy 180,6690
(defcustom proof-delete-empty-windows 199,7405
(defcustom proof-shrink-windows-tofit 210,7936
(defcustom proof-auto-raise-buffers 217,8208
(defcustom proof-colour-locked 224,8443
(defcustom proof-sticky-errors 232,8693
(defcustom proof-query-file-save-when-activating-scripting239,8910
(defcustom proof-prog-name-ask255,9630
(defcustom proof-prog-name-guess261,9790
(defcustom proof-tidy-response269,10055
(defcustom proof-keep-response-history283,10518
(defcustom pg-input-ring-size 293,10906
(defcustom proof-general-debug 298,11058
(defcustom proof-use-parser-cache 307,11429
(defcustom proof-follow-mode 314,11683
(defcustom proof-auto-action-when-deactivating-scripting 338,12860
(defcustom proof-rsh-command 366,14042
(defcustom proof-disappearing-proofs 382,14600
(defcustom proof-full-annotation 387,14761
(defcustom proof-output-tooltips 397,15224
(defcustom proof-minibuffer-messages 408,15731
(defcustom proof-autosend-enable 416,16040
(defcustom proof-autosend-delay 422,16220
(defcustom proof-autosend-all 428,16378
(defcustom proof-fast-process-buffer 433,16547

generic/proof-utils.el,1645
(defmacro proof-with-current-buffer-if-exists 61,1737
(defmacro proof-with-script-buffer 70,2114
(defmacro proof-map-buffers 81,2495
(defmacro proof-sym 86,2680
(defsubst proof-try-require 91,2841
(defun proof-save-some-buffers 104,3172
(defun proof-save-this-buffer 124,3768
(defun proof-file-truename 137,4132
(defun proof-files-to-buffers 141,4314
(defun proof-buffers-in-mode 149,4553
(defun pg-save-from-death 163,5003
(defun proof-define-keys 182,5619
(defun pg-remove-specials 193,5904
(defun pg-remove-specials-in-string 203,6240
(defun proof-safe-split-window-vertically 213,6465
(defun proof-warn-if-unset 218,6645
(defun proof-get-window-for-buffer 223,6863
(defun proof-display-and-keep-buffer 260,8497
(defun proof-clean-buffer 302,10220
(defun pg-internal-warning 318,10876
(defun proof-debug 326,11158
(defun proof-switch-to-buffer 341,11709
(defun proof-resize-window-tofit 363,12833
(defun proof-submit-bug-report 458,16681
(defun proof-deftoggle-fn 493,18038
(defmacro proof-deftoggle 508,18704
(defun proof-defintset-fn 519,19217
(defmacro proof-defintset 538,20041
(defun proof-deffloatset-fn 545,20420
(defmacro proof-deffloatset 561,21134
(defun proof-defstringset-fn 568,21519
(defmacro proof-defstringset 581,22145
(defun proof-escape-keymap-doc 594,22601
(defmacro proof-defshortcut 598,22755
(defmacro proof-definvisible 613,23353
(defun pg-custom-save-vars 640,24282
(defun pg-custom-reset-vars 656,24926
(defun proof-locate-executable 669,25263
(defun pg-current-word-pos 684,25813
(defsubst proof-shell-strip-output-markup 729,27468
(defun proof-minibuffer-message 735,27732

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,1123
(defvar holes-active-hole 50,1301
(defgroup holes 60,1498
(defcustom holes-empty-hole-string 65,1597
(defcustom holes-empty-hole-regexp 70,1740
(defface active-hole-face92,2442
(defface inactive-hole-face102,2858
(defvar hole-map116,3299
(defvar holes-mode-map126,3690
(defun holes-region-beginning-or-nil 172,5427
(defun holes-region-end-or-nil 176,5563
(defun holes-copy-active-region 180,5681
(defun holes-is-hole-p 186,5891
(defun holes-hole-start-position 190,5983
(defun holes-hole-end-position 196,6166
(defun holes-hole-buffer 201,6337
(defun holes-hole-at 207,6511
(defun holes-active-hole-exist-p 212,6681
(defun holes-active-hole-start-position 219,6934
(defun holes-active-hole-end-position 227,7302
(defun holes-active-hole-buffer 236,7665
(defun holes-goto-active-hole 244,7966
(defun holes-highlight-hole-as-active 253,8225
(defun holes-highlight-hole 261,8533
(defun holes-disable-active-hole 269,8820
(defun holes-set-active-hole 282,9352
(defun holes-is-in-hole-p 292,9697
(defun holes-make-hole 296,9835
(defun holes-make-hole-at 314,10491
(defun holes-clear-hole 328,10944
(defun holes-clear-hole-at 337,11202
(defun holes-map-holes 345,11458
(defun holes-clear-all-buffer-holes 349,11612
(defun holes-next 359,11912
(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,16166
(defsubst holes-track-mouse-clicks 478,16224
(defun holes-mouse-replace-active-hole 482,16334
(defun holes-destroy-hole 496,16805
(defsubst holes-hole-at-event 510,17187
(defun holes-mouse-destroy-hole 514,17287
(defun holes-mouse-forget-hole 521,17508
(defun holes-mouse-set-make-active-hole 531,17800
(defun holes-mouse-set-active-hole 547,18299
(defun holes-set-point-next-hole-destroy 556,18550
(defun holes-replace-string-by-holes-backward 582,19531
(defun holes-skeleton-end-hook 600,20231
(defconst holes-jump-doc609,20669
(defun holes-replace-string-by-holes-backward-jump 616,20875
(define-minor-mode holes-mode 634,21632
(defun holes-abbrev-complete 729,25114
(defun holes-insert-and-expand 739,25457

lib/local-vars-list.el,276
(defconst local-vars-list-doc 28,827
(defun local-vars-list-find 43,1276
(defun local-vars-list-goto-var 62,2047
(defun local-vars-list-get-current 88,3094
(defun local-vars-list-get 109,3944
(defun local-vars-list-get-safe 130,4653
(defun local-vars-list-set 135,4847

lib/maths-menu.el,242
(defvar maths-menu-filter-predicate 56,2328
(defvar maths-menu-tokenise-insert 59,2436
(defun maths-menu-build-menu 62,2551
(defvar maths-menu-menu84,3312
(defvar maths-menu-mode-map344,12870
(define-minor-mode maths-menu-mode352,13089

lib/pg-dev.el,199
(defconst pg-dev-lisp-font-lock-keywords58,1742
(defun pg-loadpath 84,2444
(defun unload-pg 94,2615
(defun profile-pg 125,3509
(defun elp-pack-number 155,4616
(defun pg-bug-references 164,4816

lib/pg-fontsets.el,210
(defcustom pg-fontsets-default-fontset 27,803
(defvar pg-fontsets-names 32,949
(defun pg-fontsets-make-fontsetsizes 35,1030
(defconst pg-fontsets-base-fonts54,1791
(defun pg-fontsets-make-fontsets 60,1921

lib/proof-compat.el,123
(defvar proof-running-on-win32 32,975
(defun pg-custom-undeclare-variable 53,1777
(defmacro save-selected-frame 86,2602

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,10540
(defun scomint-interrupt-process 284,11295

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,3032
(defun texi-docstring-magic-splice-sep 93,3197
(defconst texi-docstring-magic-munge-table103,3502
(defun texi-docstring-magic-untabify 193,7265
(defun texi-docstring-magic-munge-docstring 200,7463
(defun texi-docstring-magic-texi 239,8744
(defun texi-docstring-magic-format-default 252,9184
(defun texi-docstring-magic-texi-for 268,9817
(defconst texi-docstring-magic-comment326,11776
(defun texi-docstring-magic 332,11930
(defun texi-docstring-magic-face-at-point 366,13009
(defun texi-docstring-magic-insert-magic 381,13532

lib/unicode-chars.el,80
(defvar unicode-chars-alist12,348
(defun unicode-chars-list-chars 5051,245975

lib/unicode-tokens.el,5902
(defgroup unicode-tokens-options 58,1844
(defcustom unicode-tokens-add-help-echo 63,1969
(defun unicode-tokens-toggle-add-help-echo 68,2136
(defvar unicode-tokens-token-symbol-map 82,2542
(defvar unicode-tokens-token-format 101,3201
(defvar unicode-tokens-token-variant-format-regexp 107,3450
(defvar unicode-tokens-shortcut-alist 121,3983
(defvar unicode-tokens-shortcut-replacement-alist 127,4260
(defvar unicode-tokens-control-region-format-regexp 135,4466
(defvar unicode-tokens-control-char-format-regexp 142,4834
(defvar unicode-tokens-control-regions 149,5195
(defvar unicode-tokens-control-characters 152,5271
(defvar unicode-tokens-control-char-format 155,5353
(defvar unicode-tokens-control-region-format-start 158,5466
(defvar unicode-tokens-control-region-format-end 161,5583
(defvar unicode-tokens-tokens-customizable-variables 164,5696
(defconst unicode-tokens-configuration-variables171,5864
(defun unicode-tokens-config 186,6263
(defun unicode-tokens-config-var 190,6408
(defun unicode-tokens-copy-configuration-variables 202,6848
(defvar unicode-tokens-token-list 230,8064
(defvar unicode-tokens-hash-table 233,8184
(defvar unicode-tokens-token-match-regexp 236,8300
(defvar unicode-tokens-uchar-hash-table 242,8583
(defvar unicode-tokens-uchar-regexp 246,8770
(defgroup unicode-tokens-faces 254,8955
(defconst unicode-tokens-font-family-alternatives264,9257
(defface unicode-tokens-symbol-font-face279,9776
(defface unicode-tokens-script-font-face290,10249
(defface unicode-tokens-fraktur-font-face295,10393
(defface unicode-tokens-serif-font-face300,10518
(defface unicode-tokens-sans-font-face305,10655
(defface unicode-tokens-highlight-face310,10777
(defconst unicode-tokens-fonts319,11139
(defconst unicode-tokens-fontsymb-properties328,11356
(define-widget 'unicode-tokens-token-symbol-map unicode-tokens-token-symbol-map
356,12977
(define-widget 'unicode-tokens-shortcut-alist unicode-tokens-shortcut-alist
374,13529
(defconst unicode-tokens-font-lock-extra-managed-props387,13860
(defun unicode-tokens-font-lock-keywords 391,14014
(defun unicode-tokens-calculate-token-match 424,15385
(defun unicode-tokens-usable-composition 454,16421
(defun unicode-tokens-help-echo 467,16800
(defvar unicode-tokens-show-symbols 472,17002
(defun unicode-tokens-interpret-composition 475,17116
(defun unicode-tokens-font-lock-compose-symbol 493,17628
(defun unicode-tokens-prepend-text-properties-in-match 531,19160
(defun unicode-tokens-prepend-text-property 545,19738
(defun unicode-tokens-show-symbols 570,20883
(defun unicode-tokens-symbs-to-props 578,21193
(defvar unicode-tokens-show-controls 598,21892
(defun unicode-tokens-show-controls 601,21983
(defun unicode-tokens-control-char 613,22496
(defun unicode-tokens-control-region 622,22935
(defun unicode-tokens-control-font-lock-keywords 633,23482
(defvar unicode-tokens-use-shortcuts 644,23806
(defun unicode-tokens-use-shortcuts 647,23909
(defun unicode-tokens-map-ordering 663,24505
(defun unicode-tokens-quail-define-rules 672,24858
(defun unicode-tokens-insert-token 695,25535
(defun unicode-tokens-annotate-region 704,25839
(defun unicode-tokens-insert-control 728,26677
(defun unicode-tokens-insert-uchar-as-token 738,27126
(defun unicode-tokens-delete-token-near-point 744,27347
(defun unicode-tokens-delete-backward-char 756,27788
(defun unicode-tokens-delete-char 767,28169
(defun unicode-tokens-delete-backward-1 778,28523
(defun unicode-tokens-delete-1 795,29119
(defun unicode-tokens-prev-token 811,29663
(defun unicode-tokens-rotate-token-forward 819,29960
(defun unicode-tokens-rotate-token-backward 846,30850
(defun unicode-tokens-replace-shortcut-match 851,31052
(defun unicode-tokens-replace-shortcuts 860,31422
(defun unicode-tokens-replace-unicode-match 874,32021
(defun unicode-tokens-replace-unicode 881,32322
(defun unicode-tokens-copy-token 898,32924
(define-button-type 'unicode-tokens-listunicode-tokens-list
905,33145
(defun unicode-tokens-list-tokens 911,33349
(defun unicode-tokens-list-shortcuts 950,34533
(defalias 'unicode-tokens-list-unicode-chars unicode-tokens-list-unicode-chars
968,35171
(defun unicode-tokens-encode-in-temp-buffer 970,35244
(defun unicode-tokens-encode 988,35900
(defun unicode-tokens-encode-str 994,36136
(defun unicode-tokens-copy 998,36298
(defun unicode-tokens-paste 1007,36704
(defvar unicode-tokens-highlight-unicode 1026,37425
(defconst unicode-tokens-unicode-highlight-patterns1029,37517
(defun unicode-tokens-highlight-unicode 1033,37686
(defun unicode-tokens-highlight-unicode-setkeywords 1045,38149
(defun unicode-tokens-initialise 1057,38518
(defvar unicode-tokens-mode-map 1077,39189
(defvar unicode-tokens-display-table1080,39286
(define-minor-mode unicode-tokens-mode1087,39537
(defun unicode-tokens-set-font-var 1223,44112
(defun unicode-tokens-set-font-var-aux 1239,44601
(defun unicode-tokens-mouse-set-font 1270,45762
(defsubst unicode-tokens-face-font-sym 1283,46276
(defun unicode-tokens-set-font-restart 1287,46456
(defun unicode-tokens-save-fonts 1298,46766
(defun unicode-tokens-custom-save-faces 1306,47022
(define-key unicode-tokens-mode-map1323,47478
(define-key unicode-tokens-mode-map1326,47585
(defvar unicode-tokens-quail-translation-keymap1334,47844
(define-key unicode-tokens-quail-translation-keymap1341,48034
(defun unicode-tokens-quail-delete-last-char 1345,48168
(define-key unicode-tokens-mode-map 1360,48595
(define-key unicode-tokens-mode-map 1362,48687
(define-key unicode-tokens-mode-map1364,48778
(define-key unicode-tokens-mode-map1366,48884
(define-key unicode-tokens-mode-map1369,48999
(define-key unicode-tokens-mode-map1371,49108
(define-key unicode-tokens-mode-map1373,49216
(define-key unicode-tokens-mode-map1375,49322
(defun unicode-tokens-customize-submenu 1383,49446
(defun unicode-tokens-define-menu 1390,49669

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,7116
@node Top145,4240
@node Preface184,5439
@node News for Version 4.2News for Version 4.2
209,6078
@node News for Version 4.1News for Version 4.1
222,6534
@node News for Version 4.0News for Version 4.0
233,6841
@node Future254,7692
@node Credits283,9027
@node Introducing Proof GeneralIntroducing Proof General
405,13136
@node Installing Proof GeneralInstalling Proof General
460,15110
@node Quick start guideQuick start guide
474,15559
@node Features of Proof GeneralFeatures of Proof General
519,17753
@node Supported proof assistantsSupported proof assistants
625,22297
@node Prerequisites for this manualPrerequisites for this manual
677,24287
@node Organization of this manualOrganization of this manual
721,25906
@node Basic Script ManagementBasic Script Management
747,26734
@node Walkthrough example in IsabelleWalkthrough example in Isabelle
766,27334
@node Proof scriptsProof scripts
1051,38729
@node Script buffersScript buffers
1094,40849
@node Locked queue and editing regionsLocked queue and editing regions
1116,41426
@node Goal-save sequencesGoal-save sequences
1172,43573
@node Active scripting bufferActive scripting buffer
1209,45057
@node Summary of Proof General buffersSummary of Proof General buffers
1282,48690
@node Script editing commandsScript editing commands
1331,50947
@node Script processing commandsScript processing commands
1411,53906
@node Proof assistant commandsProof assistant commands
1540,59336
@node Toolbar commandsToolbar commands
1733,66264
@node Interrupting during trace outputInterrupting during trace output
1758,67223
@node Advanced Script Management and EditingAdvanced Script Management and Editing
1798,69153
@node Document centred workingDocument centred working
1819,69774
@node Automatic processingAutomatic processing
1931,74452
@node Visibility of completed proofsVisibility of completed proofs
1986,76500
@node Switching between proof scriptsSwitching between proof scripts
2041,78440
@node View of processed files View of processed files 
2078,80412
@node Retracting across filesRetracting across files
2138,83463
@node Asserting across filesAsserting across files
2151,84094
@node Automatic multiple file handlingAutomatic multiple file handling
2164,84660
@node Escaping script managementEscaping script management
2189,85694
@node Editing featuresEditing features
2246,87806
@node Unicode symbols and special layout supportUnicode symbols and special layout support
2316,90585
@node Maths menuMaths menu
2358,92143
@node Unicode Tokens modeUnicode Tokens mode
2375,92834
@node Configuring tokens symbols and shortcutsConfiguring tokens symbols and shortcuts
2425,95257
@node Special layout Special layout 
2455,96218
@node Moving between Unicode and tokensMoving between Unicode and tokens
2565,100336
@node Finding available tokens shortcuts and symbolsFinding available tokens shortcuts and symbols
2620,102447
@node Selecting suitable fontsSelecting suitable fonts
2659,103621
@node Support for other PackagesSupport for other Packages
2724,106609
@node Syntax highlightingSyntax highlighting
2754,107445
@node Imenu and SpeedbarImenu and Speedbar
2782,108448
@node Support for outline modeSupport for outline mode
2828,110119
@node Support for completionSupport for completion
2853,111248
@node Support for tagsSupport for tags
2910,113410
@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
2962,115758
@node Goals buffer commandsGoals buffer commands
2978,116353
@node Graphical Proof-Tree VisualizationGraphical Proof-Tree Visualization
3077,120506
@node Starting and Stopping Proof-Tree VisualizationStarting and Stopping Proof-Tree Visualization
3100,121398
@node Features of ProoftreeFeatures of Prooftree
3128,122555
@node Prooftree CustomizationProoftree Customization
3160,123766
@node Customizing Proof GeneralCustomizing Proof General
3184,124645
@node Basic optionsBasic options
3224,126315
@node How to customizeHow to customize
3248,127085
@node Display customizationDisplay customization
3295,129052
@node User optionsUser options
3466,136017
@node Changing facesChanging faces
3711,145032
@node Script buffer facesScript buffer faces
3733,145907
@node Goals and response facesGoals and response faces
3779,147507
@node Tweaking configuration settingsTweaking configuration settings
3824,149039
@node Hints and TipsHints and Tips
3881,151565
@node Adding your own keybindingsAdding your own keybindings
3900,152166
@node Using file variablesUsing file variables
3964,154780
@node Using abbreviationsUsing abbreviations
4041,157508
@node LEGO Proof GeneralLEGO Proof General
4080,158923
@node LEGO specific commandsLEGO specific commands
4121,160292
@node LEGO tagsLEGO tags
4141,160747
@node LEGO customizationsLEGO customizations
4151,160994
@node Coq Proof GeneralCoq Proof General
4181,161834
@node Coq-specific commandsCoq-specific commands
4197,162200
@node Multiple File SupportMultiple File Support
4220,162708
@node Automatic Compilation in DetailAutomatic Compilation in Detail
4290,165297
@node Locking AncestorsLocking Ancestors
4365,168648
@node Customizing Coq Multiple File SupportCustomizing Coq Multiple File Support
4398,170073
@node Current LimitationsCurrent Limitations
4627,179680
@node Editing multiple proofsEditing multiple proofs
4653,180532
@node User-loaded tacticsUser-loaded tactics
4677,181640
@node Holes featureHoles feature
4741,184114
@node Proof-Tree VisualizationProof-Tree Visualization
4766,185333
@node Isabelle Proof GeneralIsabelle Proof General
4784,185944
@node Choosing logic and starting isabelleChoosing logic and starting isabelle
4810,186820
@node Isabelle commandsIsabelle commands
4879,189621
@node Isabelle settingsIsabelle settings
5022,193813
@node Isabelle customizationsIsabelle customizations
5036,194395
@node HOL Light Proof GeneralHOL Light Proof General
5059,194888
@node Shell Proof GeneralShell Proof General
5106,196867
@node Obtaining and InstallingObtaining and Installing
5142,198326
@node Obtaining Proof GeneralObtaining Proof General
5157,198691
@node Installing Proof General from tarballInstalling Proof General from tarball
5183,199573
@node Setting the names of binariesSetting the names of binaries
5207,200363
@node Notes for syssiesNotes for syssies
5235,201303
@node Bugs and EnhancementsBugs and Enhancements
5311,204300
@node References5332,205115
@node History of Proof GeneralHistory of Proof General
5372,206138
@node Old News for 3.0Old News for 3.0
5466,210303
@node Old News for 3.1Old News for 3.1
5536,213997
@node Old News for 3.2Old News for 3.2
5562,215169
@node Old News for 3.3Old News for 3.3
5623,218172
@node Old News for 3.4Old News for 3.4
5642,219069
@node Old News for 3.5Old News for 3.5
5664,220124
@node Old News for 3.6Old News for 3.6
5668,220181
@node Old News for 3.7Old News for 3.7
5673,220281
@node Function IndexFunction Index
5703,221735
@node Variable IndexVariable Index
5707,221811
@node Keystroke IndexKeystroke Index
5711,221891
@node Concept IndexConcept Index
5715,221957

doc/PG-adapting.texi,4541
@node Top137,3999
@node Introduction175,5149
@node Future216,6802
@node Credits252,8398
@node Beginning with a New ProverBeginning with a New Prover
262,8690
@node Overview of adding a new proverOverview of adding a new prover
302,10632
@node Demonstration instance and easy configurationDemonstration instance and easy configuration
384,14281
@node Major modes used by Proof GeneralMajor modes used by Proof General
453,17672
@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands
496,19382
@node Settings for generic user-level commandsSettings for generic user-level commands
511,19928
@node Menu configurationMenu configuration
556,21660
@node Toolbar configurationToolbar configuration
580,22577
@node Proof Script SettingsProof Script Settings
639,24814
@node Recognizing commands and commentsRecognizing commands and comments
662,25426
@node Recognizing proofsRecognizing proofs
799,31879
@node Recognizing other elementsRecognizing other elements
903,36183
@node Configuring undo behaviourConfiguring undo behaviour
966,38662
@node Nested proofsNested proofs
1103,44049
@node Safe (state-preserving) commandsSafe (state-preserving) commands
1143,45675
@node Activate scripting hookActivate scripting hook
1166,46628
@node Automatic multiple filesAutomatic multiple files
1190,47498
@node Completely asserted buffersCompletely asserted buffers
1211,48344
@node Completions1244,49809
@node Proof Shell SettingsProof Shell Settings
1285,51299
@node Proof shell commandsProof shell commands
1316,52581
@node Script input to the shellScript input to the shell
1493,60345
@node Settings for matching various output from proof processSettings for matching various output from proof process
1563,63549
@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process
1690,69105
@node Hooks and other settingsHooks and other settings
1950,80395
@node Goals Buffer SettingsGoals Buffer Settings
2029,83539
@node Splash Screen SettingsSplash Screen Settings
2103,86529
@node Global ConstantsGlobal Constants
2129,87284
@node Handling Multiple FilesHandling Multiple Files
2155,88113
@node Configuring Editing SyntaxConfiguring Editing Syntax
2324,96782
@node Configuring Font LockConfiguring Font Lock
2381,98899
@node Configuring TokensConfiguring Tokens
2457,102611
@node Configuring Proof-Tree VisualizationConfiguring Proof-Tree Visualization
2507,104731
@node Prerequisites2524,105271
@node Proof-Tree Display InternalsProof-Tree Display Internals
2587,107922
@node Organization of the CodeOrganization of the Code
2605,108412
@node Communication2701,112675
@node Guards2726,113787
@node Urgent and Delayed ActionsUrgent and Delayed Actions
2780,115932
@node Full AnnotationFull Annotation
2841,118440
@node Configuring Prooftree for a New Proof AssistantConfiguring Prooftree for a New Proof Assistant
2855,119014
@node Proof Tree Elisp configurationProof Tree Elisp configuration
2867,119346
@node Prooftree AdaptionProoftree Adaption
2888,120176
@node Writing More Lisp CodeWriting More Lisp Code
2908,120855
@node Default values for generic settingsDefault values for generic settings
2925,121500
@node Adding prover-specific configurationsAdding prover-specific configurations
2955,122583
@node Useful variablesUseful variables
2998,123865
@node Useful functions and macrosUseful functions and macros
3013,124364
@node Internals of Proof GeneralInternals of Proof General
3123,128676
@node Spans3153,129606
@node Proof General site configurationProof General site configuration
3168,129979
@node Configuration variable mechanismsConfiguration variable mechanisms
3251,133115
@node Global variablesGlobal variables
3381,138831
@node Proof script modeProof script mode
3456,141455
@node Proof shell modeProof shell mode
3720,153412
@node Debugging4277,176003
@node Plans and IdeasPlans and Ideas
4320,176879
@node Proof by pointing and similar featuresProof by pointing and similar features
4341,177601
@node Granularity of atomic command sequencesGranularity of atomic command sequences
4379,179259
@node Browser mode for script files and theoriesBrowser mode for script files and theories
4424,181484
@node Demonstration InstantiationsDemonstration Instantiations
4454,182515
@node demoisa-easy.el4470,182946
@node demoisa.el4532,185139
@node Function IndexFunction Index
4686,190060
@node Variable IndexVariable Index
4690,190136
@node Concept IndexConcept Index
4699,190315

generic/proof.el,0

pghaskell/pghaskell.el,0

pghaskell/pghashell.el,0

pgocaml/pgocaml.el,0

pgshell/pgshell.el,0

hol-light/hol-light-autotest.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