coq/coq-abbrev.el,468
(defun holes-show-doc 10,310
(defun coq-local-vars-list-show-doc 14,387
(defconst coq-tactics-menu 19,487
(defconst coq-tactics-abbrev-table 24,636
(defconst coq-tacticals-menu 27,724
(defconst coq-tacticals-abbrev-table 32,879
(defconst coq-commands-menu 36,972
(defconst coq-commands-abbrev-table 42,1189
(defconst coq-terms-menu 45,1279
(defconst coq-terms-abbrev-table 50,1419
(defpgdefault menu-entries 71,2121
(defpgdefault help-menu-entries152,5550

coq/coq-db.el,434
(defconst coq-syntax-db 18,455
(defvar coq-user-tactics-db48,1608
(defun coq-insert-from-db 58,1957
(defun coq-build-regexp-list-from-db 76,2738
(defun max-length-db 98,3790
(defun coq-build-menu-from-db-internal 110,4065
(defun coq-build-title-menu 145,5689
(defun coq-build-menu-from-db 155,6058
(defun coq-build-abbrev-table-from-db 175,6805
(defun filter-state-preserving 191,7359
(defun filter-state-changing 196,7513

coq/coq.el,5744
(defcustom coq-prog-name 29,695
(defcustom coq-compile-file-command 49,1446
(defcustom coq-default-undo-limit 59,1815
(defconst coq-shell-init-cmd 64,1943
(defconst coq-shell-restart-cmd 74,2203
(defvar coq-shell-prompt-pattern 82,2504
(defvar coq-shell-cd 89,2780
(defvar coq-shell-abort-goal-regexp 93,2935
(defvar coq-shell-proof-completed-regexp 96,3061
(defvar coq-goal-regexp99,3192
(defun coq-library-directory 108,3381
(defcustom coq-tags 115,3561
(defconst coq-interrupt-regexp 120,3711
(defcustom coq-www-home-page 125,3832
(defvar coq-outline-regexp135,3960
(defvar coq-outline-heading-end-regexp 140,4369
(defvar coq-shell-outline-regexp 142,4428
(defvar coq-shell-outline-heading-end-regexp 143,4478
(defconst coq-kill-goal-command 148,4588
(defconst coq-forget-id-command 149,4631
(defconst coq-back-n-command 150,4678
(defconst coq-state-preserving-tactics-regexp 154,4822
(defconst coq-state-changing-commands-regexp156,4923
(defconst coq-state-preserving-commands-regexp 158,5030
(defconst coq-commands-regexp 160,5142
(defvar coq-retractable-instruct-regexp 162,5220
(defvar coq-non-retractable-instruct-regexp 164,5311
(defvar coq-keywords-section168,5451
(defvar coq-section-regexp 171,5545
(defun coq-set-undo-limit 205,6645
(defconst coq-keywords-decl-defn-regexp216,7084
(defun coq-proof-mode-p 220,7234
(defun coq-is-comment-or-proverprocp 231,7644
(defun coq-is-goalsave-p 233,7748
(defun coq-is-module-equal-p 234,7823
(defun coq-is-def-p 237,8019
(defun coq-is-decl-defn-p 239,8127
(defun coq-state-preserving-command-p 244,8294
(defun coq-command-p 247,8428
(defun coq-state-preserving-tactic-p 250,8528
(defun coq-state-changing-tactic-p 255,8676
(defun coq-state-changing-command-p 262,8910
(defun coq-section-or-module-start-p 269,9256
(defun build-list-id-from-string 278,9497
(defun coq-last-prompt-info 291,10027
(defun coq-last-prompt-info-safe 307,10625
(defvar coq-last-but-one-statenum 317,11140
(defvar coq-last-but-one-proofnum 319,11207
(defvar coq-last-but-one-proofstack 321,11270
(defun coq-get-span-statenum 323,11312
(defun coq-get-span-proofnum 328,11427
(defun coq-get-span-proofstack 333,11542
(defun coq-set-span-statenum 338,11686
(defun coq-get-span-goalcmd 343,11817
(defun coq-set-span-goalcmd 348,11931
(defun coq-set-span-proofnum 353,12061
(defun coq-set-span-proofstack 358,12192
(defun proof-last-locked-span 363,12352
(defun coq-set-state-infos 378,12956
(defun count-not-intersection 418,15035
(defun  coq-find-and-forget-v81 449,16289
(defun coq-find-and-forget-v80 477,17421
(defun coq-find-and-forget 572,22120
(defvar coq-current-goal 585,22660
(defun coq-goal-hyp 588,22725
(defun coq-state-preserving-p 601,23155
(defconst notation-print-kinds-table 616,23661
(defun coq-PrintScope 620,23829
(defun coq-guess-or-ask-for-string 639,24385
(defun coq-ask-do 650,24762
(defun coq-SearchIsos 659,25150
(defun coq-SearchConstant 665,25383
(defun coq-SearchRewrite 669,25476
(defun coq-SearchAbout 673,25577
(defun coq-Print 677,25672
(defun coq-About 681,25795
(defun coq-LocateConstant 685,25913
(defun coq-LocateLibrary 691,26050
(defun coq-addquotes 697,26200
(defun coq-LocateNotation 699,26248
(defun coq-Pwd 706,26436
(defun coq-Inspect 712,26568
(defun coq-PrintSection(716,26668
(defun coq-Print-implicit 720,26762
(defun coq-Check 725,26915
(defun coq-Show 730,27025
(defun coq-PrintHint 745,27469
(defun coq-Compile 753,27615
(defun coq-guess-command-line 766,27934
(defun coq-pre-shell-start 788,28741
(defun coq-mode-config 800,29265
(defun coq-shell-mode-config 914,33332
(defun coq-goals-mode-config 953,34983
(defun coq-response-config 961,35232
(defun coq-maybe-compile-buffer 982,35959
(defun coq-ancestors-of 1019,37493
(defun coq-all-ancestors-of 1042,38460
(defconst coq-require-command-regexp 1054,38853
(defun coq-process-require-command 1059,39062
(defun coq-included-children 1064,39189
(defun coq-process-file 1085,40028
(defpacustom print-fully-explicit 1110,40943
(defpacustom print-implicit 1115,41092
(defpacustom print-coercions 1120,41259
(defpacustom print-match-wildcards 1125,41404
(defpacustom print-elim-types 1130,41585
(defpacustom printing-depth 1135,41752
(defpacustom time-commands 1140,41914
(defpacustom auto-compile-vos 1144,42025
(defpacustom translate-to-v8 1166,42980
(defun coq-preprocessing 1175,43196
(defun coq-fake-constant-markup 1190,43615
(defun coq-create-span-menu 1212,44422
(defconst module-kinds-table 1239,45224
(defconst modtype-kinds-table1243,45374
(defun coq-insert-section-or-module 1247,45503
(defconst reqkinds-kinds-table1270,46363
(defun coq-insert-requires 1275,46508
(defun coq-end-Section 1291,47014
(defun coq-insert-intros 1309,47598
(defun coq-insert-match 1321,48122
(defun coq-insert-tactic 1353,49300
(defun coq-insert-tactical 1359,49539
(defun coq-insert-command 1365,49788
(defun coq-insert-term 1371,50032
(define-key coq-keymap 1378,50230
(define-key coq-keymap 1379,50288
(define-key coq-keymap 1380,50357
(define-key coq-keymap 1381,50415
(define-key coq-keymap 1382,50475
(define-key coq-keymap 1383,50534
(define-key coq-keymap 1384,50597
(define-key coq-keymap 1385,50657
(define-key coq-keymap 1386,50714
(define-key coq-keymap 1387,50770
(define-key coq-keymap 1388,50825
(define-key coq-keymap 1389,50875
(define-key coq-keymap 1390,50925
(define-key coq-keymap 1391,50975
(define-key coq-keymap 1392,51029
(define-key coq-keymap 1393,51088
(define-key coq-keymap 1394,51147
(defvar last-coq-error-location 1404,51320
(defun coq-get-last-error-location 1413,51719
(defun coq-highlight-error 1446,53118
(defun coq-highlight-error-hook 1478,54296

coq/coq-indent.el,2241
(defconst coq-any-command-regexp11,262
(defconst coq-indent-inner-regexp14,353
(defconst coq-comment-start-regexp 24,814
(defconst coq-comment-end-regexp 25,857
(defconst coq-comment-start-or-end-regexp 26,898
(defconst coq-indent-open-regexp28,1007
(defconst coq-indent-close-regexp33,1181
(defconst coq-indent-closepar-regexp 38,1364
(defconst coq-indent-closematch-regexp 39,1409
(defconst coq-indent-openpar-regexp 40,1480
(defconst coq-indent-openmatch-regexp 41,1524
(defconst coq-indent-any-regexp42,1604
(defconst coq-indent-kw 47,1882
(defconst coq-indent-pattern-regexp 57,2337
(defun coq-indent-goal-command-p 61,2440
(defconst coq-end-command-regexp 82,3498
(defun coq-search-comment-delimiter-forward 87,3651
(defun coq-search-comment-delimiter-backward 96,3983
(defun coq-skip-until-one-comment-backward 103,4257
(defun coq-skip-until-one-comment-forward 115,4873
(defun coq-looking-at-comment 126,5391
(defun coq-find-comment-start 130,5532
(defun coq-find-comment-end 140,5965
(defun coq-looking-at-syntactic-context 152,6511
(defconst coq-end-command-or-comment-regexp158,6733
(defconst coq-end-command-or-comment-start-regexp161,6842
(defun coq-find-not-in-comment-backward 165,6960
(defun coq-find-not-in-comment-forward 184,7863
(defun coq-find-command-end-backward 203,8782
(defun coq-find-command-end-forward 211,9180
(defun coq-find-command-end 219,9559
(defun coq-parse-function 227,9944
(defun coq-find-current-start 236,10147
(defun coq-find-real-start 245,10438
(defun coq-command-at-point 252,10657
(defun only-spaces-on-line 259,10934
(defun find-reg 268,11208
(defun coq-find-no-syntactic-on-line 283,11757
(defun coq-back-to-indentation-prevline 296,12230
(defun coq-find-unclosed 338,14126
(defun coq-find-at-same-level-zero 368,15310
(defun coq-find-unopened 396,16394
(defun coq-find-last-unopened 443,17748
(defun coq-end-offset 456,18152
(defun coq-indent-command-offset 484,18971
(defun coq-indent-expr-offset 531,20797
(defun coq-indent-comment-offset 650,25143
(defun coq-indent-offset 682,26591
(defun coq-indent-calculate 699,27398
(defun proof-indent-line 703,27488
(defun coq-indent-line-not-comments 714,27915
(defun coq-indent-region 725,28365

coq/coq-local-vars.el,279
(defconst coq-local-vars-doc 17,306
(defun coq-insert-coq-prog-name 75,2832
(defun coq-read-directory 84,3186
(defun coq-extract-directories-from-args 98,3755
(defun coq-ask-prog-args 113,4265
(defun coq-ask-prog-name 133,5262
(defun coq-ask-insert-coq-prog-name 147,5833

coq/coq-syntax.el,2331
(defvar coq-version-is-V8 21,718
(defvar coq-version-is-V8-0 23,797
(defvar coq-version-is-V8-1 30,1169
(defcustom coq-user-tactics-db 74,3092
(defcustom coq-user-commands-db 91,3600
(defvar coq-tactics-db108,4115
(defvar coq-tacticals-db263,12098
(defvar coq-decl-db285,12849
(defvar coq-defn-db307,14067
(defvar coq-goal-starters-db344,16672
(defvar coq-commands-db365,17760
(defvar coq-terms-db465,24615
(defun coq-count-match 529,27249
(defun coq-goal-command-str-v80-p 548,28103
(defun coq-module-opening-p 571,28969
(defun coq-section-command-p 582,29381
(defun coq-goal-command-str-v81-p 586,29478
(defun coq-goal-command-p-v81 601,30146
(defun coq-goal-command-str-p 611,30482
(defun coq-goal-command-p 621,30843
(defvar coq-keywords-save-strict629,31151
(defvar coq-keywords-save637,31250
(defun coq-save-command-p 641,31326
(defvar coq-keywords-kill-goal 650,31620
(defvar coq-keywords-state-changing-misc-commands654,31711
(defvar coq-keywords-goal657,31836
(defvar coq-keywords-decl660,31919
(defvar coq-keywords-defn663,31993
(defvar coq-keywords-state-changing-commands667,32068
(defvar coq-keywords-state-preserving-commands676,32266
(defvar coq-keywords-commands681,32482
(defvar coq-tacticals686,32630
(defvar coq-reserved691,32766
(defvar coq-state-changing-tactics700,33052
(defvar coq-state-preserving-tactics703,33161
(defvar coq-tactics707,33275
(defvar coq-retractable-instruct710,33364
(defvar coq-non-retractable-instruct713,33474
(defvar coq-keywords717,33596
(defvar coq-symbols724,33763
(defvar coq-error-regexp 743,33976
(defvar coq-id 746,34214
(defvar coq-id-shy 747,34239
(defvar coq-ids 749,34293
(defun coq-first-abstr-regexp 751,34334
(defun coq-first-abstr-regexp 754,34458
(defvar coq-font-lock-terms762,34650
(defconst coq-save-command-regexp-strict781,35444
(defconst coq-save-command-regexp783,35557
(defconst coq-save-with-hole-regexp785,35656
(defconst coq-goal-command-regexp789,35795
(defconst coq-goal-with-hole-regexp792,35895
(defconst coq-decl-with-hole-regexp798,36184
(defconst coq-defn-with-hole-regexp802,36318
(defconst coq-with-with-hole-regexp836,37166
(defvar coq-font-lock-keywords-1842,37418
(defvar coq-font-lock-keywords 864,38532
(defun coq-init-syntax-table 866,38590
(defconst coq-generic-expression895,39488

coq/x-symbol-coq.el,1746
(defvar x-symbol-coq-required-fonts 16,384
(defvar x-symbol-coq-name 24,785
(defvar x-symbol-coq-modeline-name 25,825
(defcustom x-symbol-coq-header-groups-alist 27,868
(defcustom x-symbol-coq-electric-ignore 34,1086
(defvar x-symbol-coq-required-fonts 41,1331
(defvar x-symbol-coq-extra-menu-items 44,1430
(defvar x-symbol-coq-token-grammar48,1518
(defun x-symbol-coq-default-token-list 64,2184
(defvar x-symbol-coq-user-table 76,2472
(defvar x-symbol-coq-generated-data 79,2578
(defvar x-symbol-coq-master-directory 87,2816
(defvar x-symbol-coq-image-searchpath 88,2864
(defvar x-symbol-coq-image-cached-dirs 89,2911
(defvar x-symbol-coq-image-file-truename-alist 90,2976
(defvar x-symbol-coq-image-keywords 91,3028
(defcustom x-symbol-coq-subscript-matcher 98,3256
(defcustom x-symbol-coq-font-lock-regexp 104,3488
(defcustom x-symbol-coq-font-lock-limit-regexp 109,3660
(defcustom x-symbol-coq-font-lock-contents-regexp 115,3848
(defcustom x-symbol-coq-single-char-regexp 122,4102
(defun x-symbol-coq-subscript-matcher 127,4250
(defun coq-match-subscript 162,5939
(defvar x-symbol-coq-font-lock-allowed-faces 169,6113
(defcustom x-symbol-coq-class-alist174,6338
(defcustom x-symbol-coq-class-face-alist 185,6716
(defvar x-symbol-coq-font-lock-keywords 195,7026
(defvar x-symbol-coq-font-lock-allowed-faces 197,7072
(defvar x-symbol-coq-case-insensitive 203,7296
(defvar x-symbol-coq-token-shape 204,7339
(defvar x-symbol-coq-input-token-ignore 205,7377
(defvar x-symbol-coq-token-list 206,7422
(defvar x-symbol-coq-symbol-table 208,7466
(defvar x-symbol-coq-xsymbol-table 312,9885
(defun x-symbol-coq-prepare-table 459,13753
(defvar x-symbol-coq-table468,14020
(defcustom x-symbol-coq-auto-style475,14181

demoisa/demoisa.el,390
(defcustom isabelledemo-prog-name 54,1809
(defcustom isabelledemo-web-page59,1931
(defun demoisa-config 70,2161
(defun demoisa-shell-config 90,2910
(define-derived-mode demoisa-mode 119,3994
(define-derived-mode demoisa-shell-mode 124,4117
(define-derived-mode demoisa-response-mode 129,4260
(define-derived-mode demoisa-goals-mode 133,4387
(defun demoisa-pre-shell-start 152,5169

isa/isabelle-system.el,2186
(defconst isa-running-isar 17,544
(defgroup isabelle 23,726
(defcustom isabelle-web-page27,855
(defcustom isa-isatool-command38,1150
(defvar isatool-not-found 65,2095
(defun isa-set-isatool-command 68,2208
(defun isa-shell-command-to-string 88,3069
(defun isa-getenv 94,3293
(defcustom isabelle-program-name 113,3950
(defvar isabelle-prog-name 139,4898
(defun isabelle-command-line 142,5025
(defun isabelle-choose-logic 166,6005
(defun isa-tool-list-logics 188,6977
(defun isa-view-doc 195,7215
(defvar isabelle-version-string 202,7439
(defun isa-version 204,7480
(defconst isa-supports-pgip 217,7963
(defun isa-tool-list-docs 225,8193
(defun isa-quit 243,8915
(defconst isabelle-verbatim-regexp 250,9110
(defun isabelle-verbatim 253,9251
(defcustom isabelle-refresh-logics 269,9842
(defcustom isabelle-logics-available 277,10169
(defcustom isabelle-chosen-logic 285,10469
(defconst isabelle-docs-menu 298,10937
(defun isabelle-logics-menu-calculate 308,11330
(defvar isabelle-time-to-refresh-logics 324,11839
(defun isabelle-logics-menu-refresh 327,11932
(defun isabelle-logics-menu-filter 344,12631
(defun isabelle-menu-bar-update-logics 350,12841
(defvar isabelle-logics-menu-entries 361,13197
(defvar isabelle-logics-menu 363,13269
(defun isabelle-load-isar-keywords 376,13887
(defpacustom show-types 403,14842
(defpacustom show-sorts 408,14958
(defpacustom show-consts 413,15074
(defpacustom long-names 418,15208
(defpacustom eta-contract 423,15340
(defpacustom trace-simplifier 428,15481
(defpacustom trace-rules 433,15613
(defpacustom quick-and-dirty 438,15745
(defpacustom full-proofs 443,15881
(defpacustom global-timing 448,16025
(defpacustom theorem-dependencies 454,16183
(defpacustom goals-limit 460,16425
(defpacustom prems-limit 465,16564
(defpacustom print-depth 470,16724
(defpgdefault menu-entries482,17013
(defpgdefault help-menu-entries 489,17175
(defpgdefault x-symbol-language 497,17369
(defun isabelle-convert-idmarkup-to-subterm 520,17984
(defun isabelle-create-span-menu 544,18996
(defun isabelle-xml-sml-escapes 561,19490
(defun isabelle-process-pgip 564,19591
(defun isabelle-parse-syntax-dump 581,20177

isa/isa.el,1517
(defcustom isa-outline-regexp43,1356
(defcustom isa-outline-heading-end-regexp 50,1593
(defvar isa-shell-outline-regexp 55,1745
(defvar isa-shell-outline-heading-end-regexp 56,1807
(defun isa-mode-config-set-variables 59,1859
(defun isa-shell-mode-config-set-variables 141,5268
(defun isa-update-thy-only 283,11160
(defun isa-shell-update-thy 295,11668
(defun isa-remove-file 320,12871
(defun isa-shell-compute-new-files-list 330,13189
(define-derived-mode isa-shell-mode 346,13701
(define-derived-mode isa-response-mode 351,13826
(define-derived-mode isa-goals-mode 356,13995
(define-derived-mode isa-proofscript-mode 361,14152
(defun isa-mode 370,14333
(define-key map 414,15873
(define-key map 415,15923
(defun isa-process-thy-file 419,16080
(defcustom isa-retract-thy-file-command 425,16289
(defun isa-retract-thy-file 431,16526
(defgroup thy 447,17155
(defun isa-splice-separator 459,17485
(defun isa-file-name-cons-extension 468,17737
(defun isa-format 475,18003
(define-key isa-proofscript-mode-map 487,18378
(defcustom isa-not-undoable-commands-regexp497,18511
(defun isa-count-undos 504,18764
(defun isa-goal-command-p 533,19901
(defun isa-find-and-forget 547,20587
(defun isa-state-preserving-p 550,20642
(defun isa-pre-shell-start 559,21010
(defun isa-mode-config 566,21287
(defun isa-shell-mode-config 594,22430
(defun isa-response-mode-config 601,22679
(defun isa-goals-mode-config 606,22840
(defun isa-preprocessing 614,23164
(defpgdefault completion-table628,23668

isa/isa-syntax.el,1982
(defun isa-init-syntax-table 14,312
(defun isa-init-output-syntax-table 34,960
(defgroup isa-syntax 71,2172
(defcustom isa-keywords-defn75,2274
(defcustom isa-keywords-goal82,2469
(defcustom isa-keywords-save88,2676
(defcustom isa-keywords-commands97,2968
(defcustom isa-keywords-sml109,3357
(defcustom isa-keyword-symbols119,3826
(defcustom isa-sml-names-keywords125,4021
(defcustom isa-sml-typenames-keywords131,4194
(defconst isa-keywords140,4490
(defconst isa-keywords-proof-commands146,4671
(defconst isa-tacticals151,4865
(defconst isa-id 159,5132
(defconst isa-idx 160,5181
(defconst isa-ids 162,5236
(defconst isa-string 165,5347
(defcustom isa-save-command-regexp167,5406
(defconst isa-save-with-hole-regexp181,5810
(defcustom isa-goal-command-regexp185,5945
(defconst isa-string-regexp197,6329
(defconst isa-goal-with-hole-regexp201,6460
(defconst isa-proof-command-regexp209,6702
(defface isabelle-class-name-face216,6913
(defface isabelle-tfree-name-face226,7198
(defface isabelle-tvar-name-face236,7485
(defface isabelle-free-name-face246,7775
(defface isabelle-bound-name-face256,8061
(defface isabelle-var-name-face266,8350
(defface isabelle-sml-symbol-face277,8687
(defconst isabelle-class-name-face 287,9063
(defconst isabelle-tfree-name-face 288,9125
(defconst isabelle-tvar-name-face 289,9187
(defconst isabelle-free-name-face 290,9247
(defconst isabelle-bound-name-face 291,9307
(defconst isabelle-var-name-face 292,9369
(defconst isabelle-sml-symbol-face 293,9427
(defconst isa-sml-function-var-names-regexp 296,9555
(defconst isa-sml-type-names-regexp 301,9815
(defvar isa-font-lock-keywords-1305,9983
(defvar isa-output-font-lock-keywords-1315,10540
(defvar isa-goals-font-lock-keywords 327,11111
(defconst isa-indent-any-regexp341,11386
(defconst isa-indent-inner-regexp343,11489
(defconst isa-indent-enclose-regexp345,11559
(defconst isa-indent-open-regexp347,11638
(defconst isa-indent-close-regexp349,11740

isa/thy-mode.el,1923
(defcustom thy-heading-indent 27,816
(defcustom thy-indent-level 32,920
(defcustom thy-indent-strings 37,1047
(defcustom thy-use-sml-mode 44,1272
(defcustom thy-sections55,1680
(defcustom thy-id-header108,3357
(defcustom thy-template120,3657
(defvar thy-mode-map 145,4085
(defvar thy-mode-syntax-table 147,4112
(defun thy-add-menus 182,5672
(defun thy-mode 220,7068
(defun thy-mode-quiet 275,8827
(defun thy-proofgeneral-send-string 355,11587
(defun isa-sml-hook 434,14194
(defun isa-sml-mode 448,14789
(defcustom isa-ml-file-extension 453,14921
(defun thy-find-other-file 458,15043
(defvar thy-minor-sml-mode-map 481,15925
(defun thy-install-sml-mode 483,15962
(defun thy-minor-sml-mode 492,16348
(defun thy-do-sml-indent 510,16998
(defun thy-insert-name 520,17395
(defun thy-insert-class 526,17593
(defun thy-insert-default-sort 536,17865
(defun thy-insert-type 544,18037
(defun thy-insert-arity 567,18607
(defun thy-insert-const 580,18982
(defun thy-insert-rule 592,19371
(defun thy-insert-template 601,19553
(defun isa-read-idlist 633,20432
(defun isa-read-id 642,20719
(defun isa-read-string 650,20948
(defun isa-read-num 658,21185
(defun thy-read-thy-name 669,21477
(defun thy-read-logic-image 678,21779
(defun thy-insert-header 688,22043
(defun thy-insert-id-header 706,22608
(defun thy-check-mode 718,22967
(defconst thy-headings-regexp723,23072
(defvar thy-mode-font-lock-keywords733,23331
(defun thy-goto-next-section 755,24091
(defun thy-goto-prev-section 783,25068
(defun thy-goto-top-of-section 790,25381
(defun thy-current-section 797,25578
(defun thy-kill-line 815,26041
(defun thy-indent-line 877,28125
(defun thy-calculate-indentation 904,29159
(defun thy-long-comment-string-indentation 924,29818
(defun thy-string-indentation 959,30802
(defun thy-indentation-for 978,31452
(defun thy-string-start 984,31611
(defun thy-comment-or-string-start 998,32148

isa/x-symbol-isabelle.el,1922
(defvar x-symbol-isabelle-required-fonts 20,630
(defvar x-symbol-isabelle-name 28,1034
(defvar x-symbol-isabelle-modeline-name 29,1084
(defcustom x-symbol-isabelle-header-groups-alist 31,1132
(defcustom x-symbol-isabelle-electric-ignore 38,1360
(defvar x-symbol-isabelle-required-fonts 46,1616
(defvar x-symbol-isabelle-extra-menu-items 49,1725
(defvar x-symbol-isabelle-token-grammar53,1823
(defun x-symbol-isabelle-token-list 60,2029
(defvar x-symbol-isabelle-user-table 63,2118
(defvar x-symbol-isabelle-generated-data 66,2239
(defvar x-symbol-isabelle-master-directory 74,2482
(defvar x-symbol-isabelle-image-searchpath 75,2535
(defvar x-symbol-isabelle-image-cached-dirs 76,2587
(defvar x-symbol-isabelle-image-file-truename-alist 77,2657
(defvar x-symbol-isabelle-image-keywords 78,2714
(defcustom x-symbol-isabelle-subscript-matcher 88,3058
(defcustom x-symbol-isabelle-font-lock-regexp 94,3305
(defcustom x-symbol-isabelle-font-lock-limit-regexp 99,3489
(defcustom x-symbol-isabelle-font-lock-contents-regexp 105,3721
(defcustom x-symbol-isabelle-single-char-regexp 115,4113
(defun x-symbol-isabelle-subscript-matcher 121,4339
(defun isabelle-match-subscript 163,6454
(defvar x-symbol-isabelle-font-lock-keywords172,6849
(defvar x-symbol-isabelle-font-lock-allowed-faces 179,7117
(defcustom x-symbol-isabelle-class-alist186,7349
(defcustom x-symbol-isabelle-class-face-alist 197,7774
(defvar x-symbol-isabelle-case-insensitive 212,8302
(defvar x-symbol-isabelle-token-shape 213,8350
(defvar x-symbol-isabelle-input-token-ignore 214,8393
(defvar x-symbol-isabelle-token-list 215,8443
(defvar x-symbol-isabelle-symbol-table 217,8492
(defvar x-symbol-isabelle-xsymbol-table 317,11228
(defun x-symbol-isabelle-prepare-table 463,15662
(defvar x-symbol-isabelle-table475,16073
(defcustom x-symbol-isabelle-auto-style489,16426
(defcustom x-symbol-isabelle-auto-coding-alist 503,16936

isar/isar.el,1244
(defcustom isar-keywords-name 28,633
(defpgdefault completion-table 45,1157
(defcustom isar-web-page47,1210
(defun isar-detect-header 65,1574
(defun isar-strip-terminators 100,2837
(defun isar-markup-ml 113,3208
(defun isar-mode-config-set-variables 118,3343
(defun isar-shell-mode-config-set-variables 182,6172
(defun isar-remove-file 282,10373
(defun isar-shell-compute-new-files-list 292,10736
(defun isar-activate-scripting 303,11202
(define-derived-mode isar-shell-mode 312,11372
(define-derived-mode isar-response-mode 317,11495
(define-derived-mode isar-goals-mode 322,11677
(define-derived-mode isar-mode 327,11852
(defpgdefault menu-entries380,13757
(defun isar-count-undos 409,14936
(defun isar-find-and-forget 435,16037
(defun isar-goal-command-p 482,17882
(defun isar-global-save-command-p 487,18054
(defvar isar-current-goal 508,18891
(defun isar-state-preserving-p 511,18957
(defvar isar-shell-current-line-width 536,20116
(defun isar-shell-adjust-line-width 542,20334
(defun isar-pre-shell-start 562,21219
(defun isar-preprocessing 574,21562
(defun isar-mode-config 597,22828
(defun isar-shell-mode-config 609,23398
(defun isar-response-mode-config 620,23768
(defun isar-goals-mode-config 629,24025

isar/isar-keywords.el,1052
(defconst isar-keywords-major13,487
(defconst isar-keywords-minor206,3647
(defconst isar-keywords-control262,4401
(defconst isar-keywords-diag282,4878
(defconst isar-keywords-theory-begin338,5837
(defconst isar-keywords-theory-switch341,5890
(defconst isar-keywords-theory-end344,5945
(defconst isar-keywords-theory-heading347,5993
(defconst isar-keywords-theory-decl353,6100
(defconst isar-keywords-theory-script412,7081
(defconst isar-keywords-theory-goal416,7158
(defconst isar-keywords-qed429,7375
(defconst isar-keywords-qed-block436,7461
(defconst isar-keywords-qed-global439,7508
(defconst isar-keywords-proof-heading442,7557
(defconst isar-keywords-proof-goal447,7640
(defconst isar-keywords-proof-block454,7739
(defconst isar-keywords-proof-open458,7801
(defconst isar-keywords-proof-close461,7847
(defconst isar-keywords-proof-chain464,7894
(defconst isar-keywords-proof-decl471,7997
(defconst isar-keywords-proof-asm480,8118
(defconst isar-keywords-proof-asm-goal487,8213
(defconst isar-keywords-proof-script490,8268

isar/isar-mmm.el,83
(defconst isar-start-latex-regexp 23,697
(defconst isar-start-sml-regexp 35,1130

isar/isar-syntax.el,3239
(defconst isar-script-syntax-table-entries 18,421
(defconst isar-script-syntax-table-alist59,1347
(defun isar-init-syntax-table 68,1630
(defun isar-init-output-syntax-table 76,1878
(defconst isar-keywords-theory-enclose92,2325
(defconst isar-keywords-theory97,2477
(defconst isar-keywords-save102,2622
(defconst isar-keywords-proof-enclose107,2751
(defconst isar-keywords-proof113,2933
(defconst isar-keywords-proof-context120,3131
(defconst isar-keywords-local-goal124,3245
(defconst isar-keywords-improper128,3357
(defconst isar-keywords-outline133,3496
(defconst isar-keywords-fume136,3561
(defconst isar-keywords-indent-open143,3779
(defconst isar-keywords-indent-close149,3963
(defconst isar-keywords-indent-enclose153,4068
(defun isar-regexp-simple-alt 161,4247
(defun isar-ids-to-regexp 181,5008
(defconst isar-ext-first 215,6276
(defconst isar-ext-rest 216,6343
(defconst isar-long-id-stuff 218,6415
(defconst isar-id 219,6489
(defconst isar-idx 220,6559
(defconst isar-string 222,6618
(defconst isar-any-command-regexp224,6678
(defconst isar-name-regexp228,6812
(defconst isar-improper-regexp234,7107
(defconst isar-save-command-regexp238,7245
(defconst isar-global-save-command-regexp241,7346
(defconst isar-goal-command-regexp244,7460
(defconst isar-local-goal-command-regexp247,7568
(defconst isar-comment-start 250,7681
(defconst isar-comment-end 251,7716
(defconst isar-comment-start-regexp 252,7749
(defconst isar-comment-end-regexp 253,7820
(defconst isar-string-start-regexp 255,7888
(defconst isar-string-end-regexp 256,7940
(defconst isar-antiq-regexp265,8194
(defface isabelle-class-name-face272,8374
(defface isabelle-tfree-name-face282,8649
(defface isabelle-tvar-name-face292,8930
(defface isabelle-free-name-face302,9210
(defface isabelle-bound-name-face312,9486
(defface isabelle-var-name-face322,9765
(defconst isabelle-class-name-face 332,10044
(defconst isabelle-tfree-name-face 333,10106
(defconst isabelle-tvar-name-face 334,10168
(defconst isabelle-free-name-face 335,10229
(defconst isabelle-bound-name-face 336,10290
(defconst isabelle-var-name-face 337,10352
(defconst isar-font-lock-local339,10413
(defvar isar-font-lock-keywords-1344,10576
(defvar isar-output-font-lock-keywords-1359,11526
(defvar isar-goals-font-lock-keywords384,13037
(defconst isar-undo 418,13716
(defconst isar-kill 419,13778
(defun isar-remove 421,13808
(defun isar-undos 424,13883
(defun isar-cannot-undo 428,13989
(defconst isar-undo-fail-regexp432,14060
(defconst isar-undo-skip-regexp436,14198
(defconst isar-undo-ignore-regexp439,14319
(defconst isar-undo-remove-regexp442,14384
(defconst isar-undo-kill-regexp447,14524
(defconst isar-any-entity-regexp453,14666
(defconst isar-named-entity-regexp458,14853
(defconst isar-unnamed-entity-regexp463,15030
(defconst isar-next-entity-regexps466,15132
(defconst isar-generic-expression474,15439
(defconst isar-indent-any-regexp485,15673
(defconst isar-indent-inner-regexp487,15766
(defconst isar-indent-enclose-regexp489,15832
(defconst isar-indent-open-regexp491,15948
(defconst isar-indent-close-regexp493,16058
(defconst isar-outline-regexp499,16195
(defconst isar-outline-heading-end-regexp 503,16348

lclam/lclam.el,563
(defcustom lclam-prog-name 15,385
(defcustom lclam-web-page21,533
(defun lclam-config 32,763
(defun lclam-shell-config 52,1477
(define-derived-mode lclam-proofscript-mode 72,2136
(define-derived-mode lclam-shell-mode 77,2259
(define-derived-mode lclam-response-mode 82,2393
(define-derived-mode lclam-goals-mode 86,2516
(defun lclam-mode 94,2744
(defun lclam-pre-shell-start 107,3027
(define-derived-mode thy-mode 141,3970
(defvar thy-mode-map 144,4068
(defun thy-add-menus 146,4095
(defun process-thy-file 186,6009
(defun update-thy-only 192,6210

lego/lego.el,1766
(defcustom lego-tags 19,495
(defcustom lego-test-all-name 24,631
(defpgdefault help-menu-entries30,789
(defpgdefault menu-entries34,949
(defvar lego-shell-process-output45,1251
(defconst lego-process-config53,1574
(defconst lego-pretty-set-width 64,2005
(defconst lego-interrupt-regexp 68,2148
(defcustom lego-www-home-page 73,2265
(defcustom lego-www-latest-release78,2389
(defcustom lego-www-refcard84,2567
(defcustom lego-library-www-page90,2716
(defvar lego-prog-name 99,2932
(defvar lego-shell-prompt-pattern 102,3001
(defvar lego-shell-cd 105,3122
(defvar lego-shell-abort-goal-regexp 108,3222
(defvar lego-shell-proof-completed-regexp 113,3414
(defvar lego-save-command-regexp116,3554
(defvar lego-goal-command-regexp118,3644
(defvar lego-kill-goal-command 121,3735
(defvar lego-forget-id-command 122,3778
(defvar lego-undoable-commands-regexp124,3824
(defvar lego-goal-regexp 133,4198
(defvar lego-outline-regexp135,4243
(defvar lego-outline-heading-end-regexp 141,4419
(defvar lego-shell-outline-regexp 143,4472
(defvar lego-shell-outline-heading-end-regexp 144,4524
(define-derived-mode lego-shell-mode 150,4803
(define-derived-mode lego-mode 156,4976
(define-derived-mode lego-goals-mode 167,5273
(defun lego-count-undos 178,5699
(defun lego-goal-command-p 198,6518
(defun lego-find-and-forget 203,6688
(defun lego-goal-hyp 245,8524
(defun lego-state-preserving-p 254,8722
(defvar lego-shell-current-line-width 270,9425
(defun lego-shell-adjust-line-width 278,9732
(defun lego-pre-shell-start 297,10471
(defun lego-mode-config 304,10668
(defun lego-equal-module-filename 373,12763
(defun lego-shell-compute-new-files-list 379,13038
(defun lego-shell-mode-config 393,13564
(defun lego-goals-mode-config 439,15407

lego/lego-syntax.el,600
(defconst lego-keywords-goal 15,358
(defconst lego-keywords-save 17,401
(defconst lego-commands19,472
(defconst lego-keywords31,1032
(defconst lego-tacticals 36,1209
(defconst lego-error-regexp 39,1317
(defvar lego-id 42,1476
(defvar lego-ids 44,1503
(defconst lego-arg-list-regexp 48,1699
(defun lego-decl-defn-regexp 51,1815
(defconst lego-definiendum-alternative-regexp59,2187
(defvar lego-font-lock-terms63,2371
(defconst lego-goal-with-hole-regexp89,3227
(defconst lego-save-with-hole-regexp94,3450
(defvar lego-font-lock-keywords-199,3667
(defun lego-init-syntax-table 110,4134

phox/phox.el,682
(defcustom phox-prog-name 31,931
(defcustom phox-sym-lock-enabled 36,1033
(defcustom phox-web-page42,1140
(defcustom phox-doc-dir 48,1290
(defcustom phox-lib-dir 54,1438
(defcustom phox-tags-program 60,1582
(defcustom phox-tags-doc 66,1762
(defcustom phox-etags 72,1900
(defpgdefault menu-entries93,2352
(defun phox-config 107,2545
(defun phox-shell-config 153,4582
(define-derived-mode phox-mode 178,5511
(define-derived-mode phox-shell-mode 198,6123
(define-derived-mode phox-response-mode 203,6251
(define-derived-mode phox-goals-mode 215,6678
(defun phox-pre-shell-start 243,7750
(defpgdefault completion-table257,8264
(defpgdefault x-symbol-language 265,8369

phox/phox-extraction.el,382
(defvar phox-prog-orig 11,480
(defun phox-prog-flags-modify(13,548
(defun phox-prog-flags-extract(42,1352
(defun phox-prog-flags-erase(53,1643
(defun phox-toggle-extraction(61,1839
(defun phox-compile-theorem(73,2241
(defun phox-compile-theorem-on-cursor(79,2467
(defun phox-output 95,2946
(defun phox-output-theorem 105,3160
(defun phox-output-theorem-on-cursor(112,3460

phox/phox-font.el,123
(defconst phox-font-lock-keywords6,282
(defconst phox-sym-lock-keywords-table65,2406
(defun phox-sym-lock-start 88,2980

phox/phox-fun.el,679
(defun phox-init-syntax-table 67,2392
(defvar phox-top-keywords83,2865
(defvar phox-proof-keywords131,3320
(defun phox-find-and-forget 172,3670
(defun phox-assert-next-command-interactive 251,6095
(defun phox-depend-theorem(270,6926
(defun phox-eshow-extlist(279,7216
(defun phox-flag-name(293,7815
(defun phox-path(304,8118
(defun phox-print-expression(315,8355
(defun phox-print-sort-expression(328,8813
(defun phox-priority-symbols-list(339,9126
(defun phox-search-string(351,9499
(defun phox-constraints(366,10027
(defun phox-goals(377,10284
(defvar phox-state-menu389,10494
(defun phox-delete-symbol(414,11484
(defun phox-delete-symbol-on-cursor(420,11693

phox/phox-lang.el,283
(defvar phox-lang8,278
(defun phox-lang-absurd 17,495
(defun phox-lang-suppress 22,590
(defun phox-lang-opendef 27,789
(defun phox-lang-instance 32,908
(defun phox-lang-lock 37,1037
(defun phox-lang-unlock 42,1174
(defun phox-lang-prove 47,1317
(defun phox-lang-let 52,1454

phox/phox-outline.el,70
(defun phox-outline-level(32,1113
(defun phox-setup-outline 46,1587

phox/phox-pbrpm.el,512
(defun phox-pbrpm-left-paren-p 25,1167
(defun phox-pbrpm-right-paren-p 32,1370
(defun phox-pbrpm-menu-from-string 40,1574
(defun phox-pbrpm-rename-in-cmd 49,1908
(defun phox-pbrpm-get-region-name 82,3162
(defun  phox-pbrpm-escape-string 85,3289
(defun phox-pbrpm-generate-menu 89,3424
(defalias 'proof-pbrpm-generate-menu proof-pbrpm-generate-menu
287,10613
(defalias 'proof-pbrpm-left-paren-p proof-pbrpm-left-paren-p
288,10677
(defalias 'proof-pbrpm-right-paren-p proof-pbrpm-right-paren-p
289,10739

phox/phox-sym-lock.el,1352
(defvar phox-sym-lock-sym-count 34,1617
(defvar phox-sym-lock-ext-start 37,1687
(defvar phox-sym-lock-ext-end 39,1809
(defvar phox-sym-lock-font-size 42,1928
(defvar phox-sym-lock-keywords 47,2118
(defvar phox-sym-lock-enabled 52,2294
(defvar phox-sym-lock-color 57,2456
(defvar phox-sym-lock-mouse-face 62,2674
(defvar phox-sym-lock-mouse-face-enabled 67,2864
(defconst phox-sym-lock-with-mule 72,3054
(defun phox-sym-lock-gen-symbol 75,3138
(defun phox-sym-lock-make-symbols-atomic 83,3441
(defun phox-sym-lock-compute-font-size 110,4383
(defvar phox-sym-lock-font-name147,5729
(defun phox-sym-lock-set-foreground 185,7014
(defun phox-sym-lock-translate-char 199,7623
(defun phox-sym-lock-translate-char-or-string 207,7891
(defun phox-sym-lock-remap-face 214,8118
(defvar phox-sym-lock-clear-face234,9108
(defun phox-sym-lock 246,9530
(defun phox-sym-lock-rec 255,9934
(defun phox-sym-lock-atom-face 261,10087
(defun phox-sym-lock-pre-idle-hook-first 266,10383
(defun phox-sym-lock-pre-idle-hook-last 274,10741
(defun phox-sym-lock-enable 283,11116
(defun phox-sym-lock-disable 296,11529
(defun phox-sym-lock-mouse-face-enable 309,11947
(defun phox-sym-lock-mouse-face-disable 316,12162
(defun phox-sym-lock-font-lock-hook 323,12381
(defun font-lock-set-defaults 338,13074
(defun phox-sym-lock-patch-keywords 349,13452

phox/phox-tags.el,305
(defun phox-tags-add-table(21,766
(defun phox-tags-reset-table(38,1359
(defun phox-tags-add-doc-table(48,1629
(defun phox-tags-add-lib-table(54,1778
(defun phox-tags-add-local-table(60,1914
(defun phox-tags-create-local-table(66,2097
(defun phox-complete-tag(77,2349
(defvar phox-tags-menu96,2904

phox/x-symbol-phox.el,1609
(defvar x-symbol-phox-required-fonts 14,449
(defcustom x-symbol-phox-header-groups-alist 29,1056
(defcustom x-symbol-phox-electric-ignore 36,1276
(defvar x-symbol-phox-required-fonts 43,1492
(defvar x-symbol-phox-extra-menu-items 46,1593
(defvar x-symbol-phox-token-grammar49,1682
(defvar x-symbol-phox-input-token-grammar63,2473
(defun x-symbol-phox-default-token-list 69,2728
(defvar x-symbol-phox-user-table 81,3046
(defvar x-symbol-phox-generated-data 84,3155
(defvar x-symbol-phox-master-directory 92,3394
(defvar x-symbol-phox-image-searchpath 93,3443
(defvar x-symbol-phox-image-cached-dirs 94,3491
(defvar x-symbol-phox-image-file-truename-alist 95,3557
(defvar x-symbol-phox-image-keywords 96,3610
(defcustom x-symbol-phox-class-alist103,3831
(defcustom x-symbol-phox-class-face-alist 114,4213
(defvar x-symbol-phox-font-lock-keywords 124,4526
(defvar x-symbol-phox-font-lock-allowed-faces 126,4573
(defvar x-symbol-phox-case-insensitive 132,4798
(defvar x-symbol-phox-token-shape 133,4842
(defvar x-symbol-phox-input-token-ignore 134,4881
(defvar x-symbol-phox-token-list 141,5120
(defvar x-symbol-phox-xsymb0-table 143,5165
(defun x-symbol-phox-prepare-table 164,5624
(defvar x-symbol-phox-table172,5800
(defcustom x-symbol-phox-auto-style183,6118
(defvar x-symbol-phox-menu-alist 209,7068
(defvar x-symbol-phox-grid-alist 211,7158
(defvar x-symbol-phox-decode-atree 214,7249
(defvar x-symbol-phox-decode-alist 216,7342
(defvar x-symbol-phox-encode-alist 218,7439
(defvar x-symbol-phox-nomule-decode-exec 222,7596
(defvar x-symbol-phox-nomule-encode-exec 224,7696

plastic/plastic.el,2907
(defcustom plastic-tags 28,805
(defcustom plastic-test-all-name 33,937
(defvar plastic-lit-string 39,1110
(defcustom plastic-help-menu-list43,1223
(defvar plastic-shell-process-output57,1717
(defconst plastic-process-config 65,2043
(defconst plastic-pretty-set-width 72,2293
(defconst plastic-interrupt-regexp 76,2442
(defcustom plastic-www-home-page 82,2563
(defcustom plastic-www-latest-release87,2700
(defcustom plastic-www-refcard93,2873
(defcustom plastic-library-www-page99,3004
(defcustom plastic-base 109,3219
(defvar plastic-prog-name 117,3391
(defun plastic-set-default-env-vars 121,3499
(defvar plastic-shell-prompt-pattern 129,3737
(defvar plastic-shell-cd 132,3862
(defvar plastic-shell-abort-goal-regexp 136,4004
(defvar plastic-shell-proof-completed-regexp 140,4172
(defvar plastic-save-command-regexp143,4315
(defvar plastic-goal-command-regexp145,4411
(defvar plastic-kill-goal-command 148,4508
(defvar plastic-forget-id-command 150,4609
(defvar plastic-undoable-commands-regexp153,4690
(defvar plastic-goal-regexp 165,5137
(defvar plastic-outline-regexp167,5185
(defvar plastic-outline-heading-end-regexp 173,5364
(defvar plastic-shell-outline-regexp 175,5420
(defvar plastic-shell-outline-heading-end-regexp 176,5478
(defvar plastic-error-occurred 178,5549
(define-derived-mode plastic-shell-mode 187,5881
(define-derived-mode plastic-mode 193,6063
(define-derived-mode plastic-goals-mode 207,6516
(defun plastic-count-undos 216,6861
(defun plastic-goal-command-p 236,7737
(defun plastic-find-and-forget 241,7930
(defun plastic-goal-hyp 276,9278
(defun plastic-state-preserving-p 287,9528
(defvar plastic-shell-current-line-width 309,10456
(defun plastic-shell-adjust-line-width 317,10772
(defun plastic-pre-shell-start 338,11653
(defun plastic-mode-config 353,12219
(defun plastic-show-shell-buffer 450,15861
(defun plastic-equal-module-filename 456,15964
(defun plastic-shell-compute-new-files-list 462,16242
(defun plastic-shell-mode-config 478,16779
(defun plastic-goals-mode-config 529,18969
(defun plastic-small-bar 541,19251
(defun plastic-large-bar 543,19340
(defun plastic-preprocessing 545,19478
(defun plastic-all-ctxt 596,21306
(defun plastic-send-one-undo 603,21484
(defun plastic-minibuf-cmd 613,21812
(defun plastic-minibuf 625,22291
(defun plastic-synchro 632,22497
(defun plastic-send-minibuf 637,22638
(defun plastic-had-error 645,22967
(defun plastic-reset-error 649,23142
(defun plastic-call-if-no-error 652,23281
(defun plastic-show-shell 657,23485
(define-key plastic-keymap 666,23747
(define-key plastic-keymap 667,23808
(define-key plastic-keymap 668,23869
(define-key plastic-keymap 669,23929
(define-key plastic-keymap 670,23988
(define-key plastic-keymap 671,24047
(defalias 'proof-toolbar-command proof-toolbar-command
681,24297
(defalias 'proof-minibuffer-cmd proof-minibuffer-cmd
682,24348

plastic/plastic-syntax.el,648
(defconst plastic-keywords-goal 18,537
(defconst plastic-keywords-save 20,583
(defconst plastic-commands22,657
(defconst plastic-keywords35,1267
(defconst plastic-tacticals 40,1450
(defconst plastic-error-regexp 43,1561
(defvar plastic-id 46,1695
(defvar plastic-ids 48,1725
(defconst plastic-arg-list-regexp 52,1933
(defun plastic-decl-defn-regexp 55,2052
(defconst plastic-definiendum-alternative-regexp63,2433
(defvar plastic-font-lock-terms67,2626
(defconst plastic-goal-with-hole-regexp89,3339
(defconst plastic-save-with-hole-regexp94,3566
(defvar plastic-font-lock-keywords-199,3792
(defun plastic-init-syntax-table 108,4184

twelf/twelf.el,463
(defcustom twelf-root-dir25,591
(defcustom twelf-info-dir31,749
(defun twelf-add-read-declaration 100,3259
(defun twelf-set-syntax 113,3594
(defun twelf-set-word 115,3691
(defun twelf-set-symbol 116,3753
(defun twelf-map-string 118,3817
(defun twelf-mode-extra-config 165,5879
(defconst twelf-syntax-menu171,6085
(defpacustom chatter 185,6452
(defpacustom double-check 190,6545
(defpacustom print-implicit 194,6682
(defpgdefault menu-entries206,6826

twelf/twelf-font.el,917
(defun twelf-font-create-face 31,836
(defvar twelf-font-dark-background 38,1094
(defvar twelf-font-patterns64,2452
(defun twelf-font-fontify-decl 105,4302
(defun twelf-font-fontify-buffer 115,4599
(defun twelf-font-unfontify 122,4858
(defvar font-lock-message-threshold 127,5032
(defun twelf-font-fontify-region 129,5110
(defun twelf-font-highlight 195,7610
(defun twelf-font-find-delimited-comment 204,8067
(defun twelf-font-find-decl 223,8747
(defun twelf-font-find-binder 239,9237
(defun twelf-font-find-parm 301,11094
(defun twelf-font-find-evar 308,11417
(defun twelf-current-decl 330,12159
(defun twelf-next-decl 357,13315
(defconst *whitespace* 382,14337
(defconst *twelf-comment-start* 385,14435
(defconst *twelf-id-chars* 388,14564
(defun skip-twelf-comments-and-whitespace 391,14682
(defun twelf-end-of-par 403,15156
(defun skip-ahead 426,15930
(defun current-line-absolute 438,16352

twelf/twelf-old.el,6958
(defvar twelf-indent 212,8771
(defvar twelf-infix-regexp 215,8831
(defvar twelf-server-program 219,9026
(defvar twelf-info-file 222,9107
(defvar twelf-server-display-commands 225,9180
(defvar twelf-highlight-range-function 230,9428
(defvar twelf-focus-function 235,9711
(defvar twelf-server-echo-commands 241,9991
(defvar twelf-save-silently 244,10112
(defvar twelf-server-timeout 248,10284
(defvar twelf-sml-program 252,10431
(defvar twelf-sml-args 255,10503
(defvar twelf-sml-display-queries 258,10569
(defvar twelf-mode-hook 261,10677
(defvar twelf-server-mode-hook 264,10771
(defvar twelf-config-mode-hook 267,10879
(defvar twelf-sml-mode-hook 270,10993
(defvar twelf-to-twelf-sml-mode 273,11074
(defvar twelf-config-mode 276,11166
(defvar *twelf-server-buffer-name* 283,11430
(defvar *twelf-server-buffer* 286,11534
(defvar *twelf-server-process-name* 289,11622
(defvar *twelf-config-buffer* 292,11713
(defvar *twelf-config-time* 295,11807
(defvar *twelf-config-list* 298,11920
(defvar *twelf-server-last-process-mark* 301,12032
(defvar *twelf-last-region-sent* 304,12150
(defvar *twelf-last-input-buffer* 311,12474
(defvar *twelf-error-pos* 315,12597
(defconst *twelf-read-functions*318,12673
(defconst *twelf-parm-table*325,12911
(defvar twelf-chatter 338,13287
(defvar twelf-double-check 346,13504
(defvar twelf-print-implicit 349,13591
(defconst *twelf-track-parms*352,13683
(defun install-basic-twelf-keybindings 363,14107
(defun install-twelf-keybindings 388,15076
(defvar twelf-mode-map 404,15841
(defvar twelf-mode-syntax-table 416,16277
(defun set-twelf-syntax 419,16356
(defun set-word 421,16453
(defun set-symbol 422,16508
(defun map-string 424,16566
(defconst *whitespace* 456,18043
(defconst *twelf-comment-start* 459,18141
(defconst *twelf-id-chars* 462,18270
(defun skip-twelf-comments-and-whitespace 465,18388
(defun twelf-end-of-par 477,18862
(defun twelf-current-decl 500,19636
(defun twelf-mark-decl 527,20792
(defun twelf-indent-decl 536,21058
(defun twelf-indent-region 545,21344
(defun twelf-indent-lines 556,21668
(defun twelf-comment-indent 564,21841
(defun looked-at 575,22197
(defun twelf-indent-line 580,22369
(defun twelf-indent-line-to 613,24112
(defun twelf-calculate-indent 626,24567
(defun twelf-dsb 641,25191
(defun twelf-mode-variables 667,26603
(defun twelf-mode 689,27416
(defun twelf-info 904,35798
(defconst twelf-error-regexp918,36338
(defconst twelf-error-fields-regexp922,36449
(defconst twelf-error-decl-regexp928,36662
(defun looked-at-nth 932,36811
(defun looked-at-nth-int 938,36993
(defun twelf-error-parser 943,37108
(defun twelf-error-decl 957,37711
(defun twelf-mark-relative 963,37890
(defun twelf-mark-absolute 979,38560
(defun twelf-find-decl 1004,39446
(defun twelf-next-error 1019,40002
(defun twelf-goto-error 1087,42812
(defun twelf-convert-standard-filename 1101,43350
(defun string-member 1113,43845
(defun twelf-config-proceed-p 1125,44337
(defun twelf-save-if-config 1132,44599
(defun twelf-config-save-some-buffers 1145,45071
(defun twelf-save-check-config 1149,45236
(defun twelf-check-config 1164,45792
(defun twelf-save-check-file 1176,46232
(defun twelf-buffer-substring 1192,46955
(defun twelf-buffer-substring-dot 1198,47217
(defun twelf-check-declaration 1204,47483
(defun twelf-highlight-range-zmacs 1227,48543
(defun twelf-focus 1233,48793
(defun twelf-focus-noop 1239,49059
(defun twelf-type-const 1322,52681
(defvar twelf-server-mode-map 1439,57823
(defconst twelf-server-cd-regexp 1451,58375
(defun looked-at-string 1454,58515
(defun twelf-server-directory-tracker 1458,58656
(defun twelf-input-filter 1480,59830
(defun twelf-server-mode 1486,60085
(defun twelf-parse-config 1519,61302
(defun twelf-server-read-config 1537,62194
(defun twelf-server-sync-config 1546,62531
(defun twelf-get-server-buffer 1576,64037
(defun twelf-init-variables 1593,64711
(defun twelf-server 1600,64924
(defun twelf-server-process 1642,66838
(defun twelf-server-display 1651,67244
(defun display-server-buffer 1658,67518
(defun twelf-server-send-command 1673,68250
(defun twelf-accept-process-output 1694,69210
(defun twelf-server-wait 1703,69649
(defun twelf-server-quit 1745,71787
(defun twelf-server-interrupt 1750,71908
(defun twelf-reset 1755,72044
(defun twelf-config-directory 1760,72188
(defun twelf-server-configure 1771,72602
(defun natp 1844,75894
(defun twelf-read-nat 1848,75995
(defun twelf-read-bool 1857,76262
(defun twelf-read-limit 1863,76410
(defun twelf-read-strategy 1873,76710
(defun twelf-read-value 1879,76862
(defun twelf-set 1883,77025
(defun twelf-set-parm 1896,77502
(defun track-parm 1905,77799
(defun twelf-toggle-double-check 1910,77973
(defun twelf-toggle-print-implicit 1916,78176
(defun twelf-get 1922,78389
(defun twelf-timers-reset 1936,79015
(defun twelf-timers-show 1941,79135
(defun twelf-timers-check 1947,79286
(defun twelf-server-restart 1953,79451
(defun twelf-config-mode 1969,80128
(defun twelf-config-mode-check 1985,80727
(defun twelf-tag 1994,81177
(defun twelf-tag-files 2022,82441
(default: *tags-errors*)2026,82744
(defun twelf-tag-file 2047,83495
(defun twelf-next-decl 2082,84717
(defun skip-ahead 2107,85739
(defun current-line-absolute 2119,86161
(defun new-temp-buffer 2124,86371
(defun rev-relativize 2135,86755
(defvar twelf-sml-mode-map 2149,87215
(defconst twelf-sml-prompt-regexp 2159,87593
(defun expand-dir 2161,87648
(defun twelf-sml-cd 2168,87909
(defconst twelf-sml-cd-regexp 2180,88398
(defun twelf-sml-directory-tracker 2183,88532
(defun twelf-sml-mode 2199,89377
(defun twelf-sml 2250,91311
(defun switch-to-twelf-sml 2270,92271
(defun display-twelf-sml-buffer 2281,92620
(defun twelf-sml-send-string 2297,93336
(defun twelf-sml-send-region 2302,93540
(defun twelf-sml-send-query 2326,94746
(defun twelf-sml-send-newline 2336,95143
(defun twelf-sml-send-semicolon 2344,95471
(defun twelf-sml-status 2352,95805
(defvar twelf-sml-init 2374,96752
(defun twelf-sml-set-mode 2377,96929
(defun twelf-sml-quit 2403,98106
(defun twelf-sml-process-buffer 2408,98218
(defun twelf-sml-process 2412,98334
(defvar twelf-to-twelf-sml-mode 2424,98850
(defun install-twelf-to-twelf-sml-keybindings 2427,98935
(defvar twelf-to-twelf-sml-mode-map 2437,99320
(defun twelf-to-twelf-sml-mode 2448,99833
(defconst twelf-at-point-menu2498,101700
(defconst twelf-server-state-menu2508,102072
(defconst twelf-error-menu2518,102389
(defconst twelf-tags-menu2524,102533
(defun twelf-toggle-server-display-commands 2534,102818
(defconst twelf-options-menu2537,102942
(defconst twelf-timers-menu2572,104680
(defconst twelf-syntax-menu2585,105174
(defun twelf-add-menu 2612,106040
(defun twelf-remove-menu 2616,106142
(defun twelf-reset-menu 2620,106240
(defun twelf-server-add-menu 2647,107139
(defun twelf-server-remove-menu 2651,107262
(defun twelf-server-reset-menu 2655,107374

generic/pg-assoc.el,250
(define-derived-mode proof-universal-keys-only-mode 20,563
(defun proof-associated-buffers 32,987
(defun pg-assoc-strip-subterm-markup 46,1287
(defun pg-assoc-strip-subterm-markup-buf 72,2220
(defun pg-assoc-strip-subterm-markup-buf-old 94,2969

generic/pg-autotest.el,442
(defvar pg-autotest-success 20,514
(defun pg-autotest-find-file 24,598
(defun pg-autotest-find-file-restart 31,869
(defmacro pg-autotest 44,1317
(defun pg-autotest-script-wholefile 58,1665
(defun pg-autotest-retract-file 75,2278
(defun pg-autotest-assert-processed 81,2414
(defun pg-autotest-assert-unprocessed 88,2660
(defun pg-autotest-message 95,2907
(defun pg-autotest-quit-prover 102,3100
(defun pg-autotest-finished 108,3282

generic/pg-goals.el,704
(define-derived-mode proof-goals-mode 29,669
(define-key proof-goals-mode-map 50,1432
(define-key proof-goals-mode-map 53,1515
(define-key proof-goals-mode-map 54,1585
(define-key proof-goals-mode-map 62,2175
(define-key proof-goals-mode-map 64,2248
(define-key proof-goals-mode-map 65,2316
(define-key proof-goals-mode-map 71,2750
(defun proof-goals-config-done 86,3014
(defun pg-goals-display 96,3302
(defun pg-goals-analyse-structure 147,5298
(defun pg-goals-make-top-span 271,10144
(defun pg-goals-yank-subterm 301,11151
(defun pg-goals-button-action 328,12051
(defun proof-expand-path 349,13024
(defun pg-goals-construct-command 358,13268
(defun pg-goals-get-subterm-help 382,14120

generic/pg-metadata.el,128
(defcustom pg-metadata-default-directory 23,628
(defface proof-preparsed-span 28,802
(defun pg-metadata-filename-for 39,1065

generic/pg-pbrpm.el,1781
(defvar pg-pbrpm-use-buffer-menu 11,259
(defvar pg-pbrpm-buffer-menu 13,378
(defvar pg-pbrpm-spans 14,412
(defvar pg-pbrpm-goal-description 15,440
(defvar pg-pbrpm-windows-dialog-bug 16,479
(defun pg-pbrpm-erase-buffer-menu 18,521
(defun pg-pbrpm-menu-change-hook 25,726
(defun pg-pbrpm-create-reset-buffer-menu 43,1303
(defun pg-pbrpm-analyse-goal-buffer 57,1917
(defun pg-pbrpm-button-action 118,4337
(defun pg-pbrpm-exists 125,4563
(defun pg-pbrpm-eliminate-id 129,4675
(defun pg-pbrpm-build-menu 137,4923
(defun pg-pbrpm-setup-span 197,7261
(defun pg-pbrpm-run-command 257,9631
(defun pg-pbrpm-get-pos-info 286,10942
(defun pg-pbrpm-get-region-info 322,12084
(defun auto-select-arround-pos 332,12409
(defun pg-pbrpm-translate-position 344,12853
(defun pg-pbrpm-process-click 350,13077
(defvar pg-pbrpm-remember-region-selected-region 370,14081
(defvar pg-pbrpm-regions-list 371,14135
(defun pg-pbrpm-erase-regions-list 373,14171
(defun pg-pbrpm-filter-regions-list 382,14480
(defface pg-pbrpm-multiple-selection-face389,14743
(defface pg-pbrpm-menu-input-face397,14948
(defun pg-pbrpm-do-remember-region 405,15141
(defun pg-pbrpm-remember-region-drag-up-hook 426,15992
(defun pg-pbrpm-remember-region-click-hook 430,16163
(defun pg-pbrpm-remember-region 435,16348
(defun pg-pbrpm-process-region 449,17063
(defun pg-pbrpm-process-regions-list 466,17786
(defun pg-pbrpm-region-expression 470,17969
(define-key proof-goals-mode-map 494,18905
(define-key proof-goals-mode-map 495,18975
(define-key proof-goals-mode-map 496,19052
(define-key pg-span-context-menu-keymap 497,19132
(define-key pg-span-context-menu-keymap 498,19209
(define-key proof-mode-map 499,19292
(define-key proof-mode-map 500,19356
(define-key proof-mode-map 501,19427

generic/pg-pgip.el,3554
(defalias 'pg-pgip-debug pg-pgip-debug
29,894
(defalias 'pg-pgip-error pg-pgip-error
30,935
(defalias 'pg-pgip-warning pg-pgip-warning
31,970
(defconst pg-pgip-version-supported 33,1020
(defun pg-pgip-process-packet 37,1126
(defvar pg-pgip-last-seen-id 47,1699
(defvar pg-pgip-last-seen-seq 48,1733
(defun pg-pgip-process-pgip 50,1769
(defun pg-pgip-process-msg 69,2700
(defvar pg-pgip-post-process-functions83,3270
(defun pg-pgip-post-process 93,3757
(defun pg-pgip-process-askpgip 109,4368
(defun pg-pgip-process-usespgip 114,4527
(defun pg-pgip-process-usespgml 118,4691
(defun pg-pgip-process-pgmlconfig 122,4855
(defun pg-pgip-process-proverinfo 138,5463
(defun pg-pgip-process-hasprefs 155,6128
(defun pg-pgip-haspref 169,6760
(defun pg-pgip-process-prefval 188,7539
(defun pg-pgip-process-guiconfig 215,8248
(defvar proof-assistant-idtables 222,8365
(defun pg-pgip-process-ids 225,8482
(defun pg-complete-idtable-symbol 251,9561
(defalias 'pg-pgip-process-setids pg-pgip-process-setids
256,9653
(defalias 'pg-pgip-process-addids pg-pgip-process-addids
257,9709
(defalias 'pg-pgip-process-delids pg-pgip-process-delids
258,9765
(defun pg-pgip-process-idvalue 261,9823
(defun pg-pgip-process-menuadd 273,10160
(defun pg-pgip-process-menudel 276,10203
(defun pg-pgip-process-ready 285,10436
(defun pg-pgip-process-cleardisplay 288,10477
(defun pg-pgip-process-proofstate 302,10954
(defun pg-pgip-process-normalresponse 306,11031
(defun pg-pgip-process-errorresponse 310,11155
(defun pg-pgip-process-scriptinsert 314,11278
(defun pg-pgip-process-metainforesponse 319,11412
(defun pg-pgip-process-informfileloaded 328,11653
(defun pg-pgip-process-informfileretracted 334,11919
(defun pg-pgip-process-brokerstatus 347,12393
(defun pg-pgip-process-proveravailmsg 350,12441
(defun pg-pgip-process-newprovermsg 353,12491
(defun pg-pgip-process-proverstatusmsg 356,12539
(defvar pg-pgip-srcids 365,12786
(defun pg-pgip-process-newfile 369,12893
(defun pg-pgip-process-filestatus 385,13481
(defun pg-pgip-process-newobj 405,14136
(defun pg-pgip-process-delobj 408,14178
(defun pg-pgip-process-objectstatus 411,14220
(defun pg-pgip-process-parsescript 425,14576
(defun pg-pgip-get-pgiptype 448,15451
(defun pg-pgip-default-for 468,16246
(defun pg-pgip-subst-for 481,16641
(defun pg-pgip-interpret-value 493,16984
(defun pg-pgip-interpret-choice 511,17667
(defun pg-pgip-get-icon 542,18740
(defsubst pg-pgip-get-name 546,18888
(defsubst pg-pgip-get-version 549,19005
(defsubst pg-pgip-get-descr 552,19128
(defsubst pg-pgip-get-thmname 555,19247
(defsubst pg-pgip-get-thyname 558,19370
(defsubst pg-pgip-get-url 561,19493
(defsubst pg-pgip-get-srcid 564,19608
(defsubst pg-pgip-get-proverid 567,19727
(defsubst pg-pgip-get-symname 570,19852
(defsubst pg-pgip-get-prefcat 573,19972
(defsubst pg-pgip-get-default 576,20100
(defsubst pg-pgip-get-objtype 579,20223
(defsubst pg-pgip-get-value 582,20346
(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext
585,20416
(defun pg-pgip-get-pgmltext 587,20475
(defun pg-pgip-string-of-command 596,20710
(defconst pg-pgip-id613,21471
(defvar pg-pgip-refseq 619,21751
(defvar pg-pgip-refid 621,21849
(defvar pg-pgip-seq 624,21943
(defun pg-pgip-assemble-packet 626,22007
(defun pg-pgip-issue 644,22822
(defun pg-pgip-maybe-askpgip 661,23435
(defun pg-pgip-askprefs 667,23626
(defun pg-pgip-askids 671,23740
(defun pg-pgip-reset 684,24031
(defconst pg-pgip-start-element-regexp 715,24729
(defconst pg-pgip-end-element-regexp 716,24781

generic/pg-pgip-old.el,456
(defun pg-pgip-process-oldhaspref 18,633
(defun pg-pgip-process-haspref 21,730
(defun pg-pgip-old-interpret-bool 57,2158
(defun pg-pgip-old-interpret-int 66,2442
(defun pg-pgip-old-interpret-string 71,2609
(defun pg-pgip-old-interpret-choice 74,2663
(defun pg-pgip-old-interpret-value 94,3382
(defun pg-pgip-old-default-for 113,3928
(defun pg-pgip-old-subst-for 124,4252
(defun pg-pgip-old-get-type 131,4417
(defun pg-pgip-old-pgiptype 138,4633

generic/pg-response.el,1188
(define-derived-mode proof-response-mode 25,617
(defun proof-response-config-done 49,1583
(defvar proof-shell-special-display-regexp 70,2358
(defconst proof-multiframe-specifiers 78,2763
(defun proof-map-multiple-frame-specifiers 87,3127
(defconst proof-multiframe-parameters97,3589
(defun proof-multiple-frames-enable 106,3888
(defun proof-three-window-enable 128,4608
(defun proof-select-three-b 132,4672
(defun proof-display-three-b 147,5141
(defvar pg-frame-configuration 161,5635
(defun pg-cache-frame-configuration 165,5782
(defun proof-layout-windows 169,5953
(defun proof-delete-other-frames 210,7766
(defvar pg-response-erase-flag 241,8861
(defun proof-shell-maybe-erase-response244,8976
(defun pg-response-display 275,10178
(defun pg-response-display-with-face 292,11000
(defun pg-response-clear-displays 327,12357
(defvar pg-response-next-error 345,12936
(defun proof-next-error 349,13058
(defun pg-response-has-error-location 429,15992
(defvar proof-trace-last-fontify-pos 452,16825
(defun proof-trace-fontify-pos 454,16868
(defun proof-trace-buffer-display 462,17182
(defun proof-trace-buffer-finish 486,18155
(defun pg-thms-buffer-clear 507,18734

generic/pg-thymodes.el,152
(defmacro pg-defthymode 19,466
(defmacro pg-do-unless-null 67,2277
(defun pg-symval 72,2364
(defun pg-modesym 78,2520
(defun pg-modesymval 82,2634

generic/pg-user.el,2304
(defmacro proof-maybe-save-point 21,410
(defun proof-maybe-follow-locked-end 29,612
(defun proof-assert-next-command-interactive 43,977
(defun proof-process-buffer 53,1348
(defun proof-undo-last-successful-command 67,1665
(defun proof-undo-and-delete-last-successful-command 72,1827
(defun proof-undo-last-successful-command-1 94,2799
(defun proof-retract-buffer 110,3364
(defun proof-retract-current-goal 119,3644
(defun proof-interrupt-process 137,4135
(defun proof-goto-command-start 164,5120
(defun proof-goto-command-end 187,6062
(defun proof-mouse-goto-point 212,6842
(defun proof-mouse-track-insert 227,7416
(defvar proof-minibuffer-history 262,8526
(defun proof-minibuffer-cmd 265,8620
(defun proof-frob-locked-end 313,10426
(defmacro proof-if-setting-configured 406,13340
(defmacro proof-define-assistant-command 414,13610
(defmacro proof-define-assistant-command-witharg 427,14076
(defun proof-issue-new-command 447,14901
(defun proof-cd-sync 492,16400
(deflocal proof-electric-terminator 543,17869
(defun proof-electric-terminator-enable 553,18216
(defun proof-electric-term-incomment-fn 564,18703
(defun proof-process-electric-terminator 584,19459
(defun proof-electric-terminator 611,20610
(defun proof-add-completions 633,21248
(defun proof-script-complete 653,22005
(defun pg-insert-last-output-as-comment 681,22596
(defun pg-copy-span-contents 712,23824
(defun pg-numth-span-higher-or-lower 729,24384
(defun pg-control-span-of 755,25135
(defun pg-move-span-contents 761,25339
(defun pg-fixup-children-span 815,27563
(defun pg-move-region-down 822,27771
(defun pg-move-region-up 831,28065
(defun proof-forward-command 861,28905
(defun proof-backward-command 882,29627
(defvar pg-span-context-menu-keymap898,29871
(defun pg-span-for-event 914,30298
(defun pg-span-context-menu 925,30682
(defun pg-toggle-visibility 940,31142
(defun pg-create-in-span-context-menu 950,31464
(defun pg-goals-buffers-hint 1022,34017
(defun pg-slow-fontify-tracing-hint 1025,34184
(defun pg-response-buffers-hint 1028,34340
(defun pg-jump-to-end-hint 1037,34689
(defun pg-processing-complete-hint 1040,34805
(defun pg-next-error-hint 1056,35491
(defun pg-hint 1060,35628
(defun pg-identifier-under-mouse-query 1079,36304
(defun proof-imenu-enable 1124,37931

generic/pg-xhtml.el,392
(defvar pg-xhtml-dir 17,423
(defun pg-xhtml-dir 20,489
(defvar pg-xhtml-file-count 32,856
(defun pg-xhtml-next-file 35,928
(defvar pg-xhtml-header 47,1159
(defmacro pg-xhtml-write-tempfile 53,1400
(defun pg-xhtml-cleanup-tempdir 71,1990
(defvar pg-mozilla-prog-name 75,2121
(defun pg-xhtml-display-file-mozilla 79,2229
(defalias 'pg-xhtml-display-file pg-xhtml-display-file
84,2402

generic/pg-xml.el,447
(defun pg-xml-parse-string 40,1169
(defun pg-xml-parse-buffer 51,1503
(defun pg-xml-get-attr 73,2236
(defun pg-xml-child-elts 81,2540
(defun pg-xml-child-elt 86,2745
(defun pg-xml-get-child 94,3028
(defun pg-xml-get-text-content 104,3400
(defmacro pg-xml-attr 115,3750
(defmacro pg-xml-node 117,3812
(defconst pg-xml-header 120,3905
(defun pg-xml-string-of 124,3982
(defun pg-xml-output-internal 135,4354
(defun pg-xml-cdata 169,5504

generic/proof-autoloads.el,80
(defalias 'proof-x-symbol-decode-region proof-x-symbol-decode-region
250,10161

generic/proof-config.el,11101
(defgroup proof-user-options 84,3173
(defcustom proof-electric-terminator-enable 89,3287
(defcustom proof-toolbar-enable 101,3821
(defcustom proof-imenu-enable 107,3994
(defpgcustom x-symbol-enable 113,4165
(defpgcustom mmm-enable 122,4515
(defcustom pg-show-hints 131,4869
(defcustom proof-output-fontify-enable 136,5004
(defcustom proof-trace-output-slow-catchup 146,5386
(defcustom proof-strict-state-preserving 156,5884
(defcustom proof-strict-read-only 169,6493
(defcustom proof-three-window-enable 179,6843
(defcustom proof-multiple-frames-enable 198,7598
(defcustom proof-delete-empty-windows 207,7934
(defcustom proof-shrink-windows-tofit 218,8465
(defcustom proof-toolbar-use-button-enablers 225,8737
(defcustom proof-query-file-save-when-activating-scripting 248,9609
(defpgcustom script-indent 264,10332
(defcustom proof-one-command-per-line 270,10520
(defcustom proof-prog-name-ask 278,10740
(defcustom proof-prog-name-guess 284,10901
(defcustom proof-tidy-response292,11161
(defcustom proof-keep-response-history306,11628
(defcustom proof-show-debug-messages 315,11991
(defcustom proof-experimental-features 324,12369
(defcustom proof-follow-mode 342,13131
(defcustom proof-auto-action-when-deactivating-scripting 368,14326
(defcustom proof-script-command-separator 391,15277
(defcustom proof-rsh-command 399,15570
(defcustom proof-disappearing-proofs 415,16121
(defgroup proof-faces 442,16771
(defmacro proof-face-specs 447,16877
(defface proof-queue-face 462,17327
(defface proof-locked-face470,17607
(defface proof-declaration-name-face483,18110
(defconst proof-declaration-name-face 495,18503
(defface proof-tacticals-name-face500,18739
(defconst proof-tacticals-name-face 509,19001
(defface proof-tactics-name-face514,19231
(defconst proof-tactics-name-face 523,19496
(defface proof-error-face 528,19720
(defface proof-warning-face536,19927
(defface proof-eager-annotation-face545,20184
(defface proof-debug-message-face553,20402
(defface proof-boring-face561,20601
(defface proof-mouse-highlight-face569,20793
(defface proof-highlight-dependent-face577,20989
(defface proof-highlight-dependency-face585,21198
(defgroup prover-config 603,21457
(defcustom proof-mode-for-shell 637,22576
(defcustom proof-mode-for-response 644,22823
(defcustom proof-mode-for-goals 651,23106
(defcustom proof-mode-for-script 658,23361
(defcustom proof-guess-command-line 669,23795
(defcustom proof-assistant-home-page 684,24292
(defcustom proof-context-command 690,24462
(defcustom proof-info-command 695,24596
(defcustom proof-showproof-command 702,24868
(defcustom proof-goal-command 707,25004
(defcustom proof-save-command 715,25302
(defcustom proof-find-theorems-command 723,25612
(defconst proof-toolbar-entries-default730,25921
(defpgcustom toolbar-entries 762,27743
(defcustom proof-assistant-true-value 780,28464
(defcustom proof-assistant-false-value 786,28654
(defcustom proof-assistant-format-int-fn 792,28848
(defcustom proof-assistant-format-string-fn 799,29097
(defcustom proof-assistant-setting-format 806,29364
(defgroup proof-script 828,30059
(defcustom proof-terminal-char 833,30189
(defcustom proof-script-sexp-commands 843,30593
(defcustom proof-script-command-end-regexp 854,31063
(defcustom proof-script-command-start-regexp 872,31882
(defcustom proof-script-use-old-parser 883,32344
(defcustom proof-script-integral-proofs 895,32833
(defcustom proof-script-fly-past-comments 910,33489
(defcustom proof-script-parse-function 917,33806
(defcustom proof-script-comment-start 935,34452
(defcustom proof-script-comment-start-regexp 946,34887
(defcustom proof-script-comment-end 954,35204
(defcustom proof-script-comment-end-regexp 966,35622
(defcustom pg-insert-output-as-comment-fn 974,35933
(defcustom proof-string-start-regexp 980,36185
(defcustom proof-string-end-regexp 985,36350
(defcustom proof-case-fold-search 990,36511
(defcustom proof-save-command-regexp 999,36927
(defcustom proof-save-with-hole-regexp 1004,37038
(defcustom proof-save-with-hole-result 1016,37490
(defcustom proof-goal-command-regexp 1027,37954
(defcustom proof-goal-with-hole-regexp 1036,38346
(defcustom proof-goal-with-hole-result 1048,38790
(defcustom proof-non-undoables-regexp 1058,39189
(defcustom proof-nested-undo-regexp 1069,39645
(defcustom proof-ignore-for-undo-count 1085,40357
(defcustom proof-script-next-entity-regexps 1093,40660
(defcustom proof-script-find-next-entity-fn1137,42394
(defcustom proof-script-imenu-generic-expression 1157,43224
(defcustom proof-goal-command-p 1175,44079
(defcustom proof-really-save-command-p 1202,45520
(defcustom proof-completed-proof-behaviour 1214,45981
(defcustom proof-count-undos-fn 1242,47341
(defconst proof-no-command 1277,48942
(defcustom proof-find-and-forget-fn 1282,49146
(defcustom proof-forget-id-command 1299,49857
(defcustom pg-topterm-goalhyp-fn 1309,50215
(defcustom proof-kill-goal-command 1321,50696
(defcustom proof-undo-n-times-cmd 1335,51206
(defcustom proof-nested-goals-history-p 1349,51755
(defcustom proof-state-preserving-p 1358,52093
(defcustom proof-activate-scripting-hook 1368,52563
(defcustom proof-deactivate-scripting-hook 1387,53341
(defcustom proof-indent 1400,53706
(defcustom proof-indent-pad-eol 1406,53880
(defcustom proof-indent-hang 1413,54120
(defcustom proof-indent-enclose-offset 1418,54246
(defcustom proof-indent-open-offset 1423,54388
(defcustom proof-indent-close-offset 1428,54525
(defcustom proof-indent-any-regexp 1433,54663
(defcustom proof-indent-inner-regexp 1438,54823
(defcustom proof-indent-enclose-regexp 1443,54977
(defcustom proof-indent-open-regexp 1448,55131
(defcustom proof-indent-close-regexp 1453,55283
(defcustom proof-script-font-lock-keywords 1459,55437
(defcustom proof-script-syntax-table-entries 1467,55760
(defcustom proof-script-span-context-menu-extensions 1485,56157
(defgroup proof-shell 1511,56946
(defcustom proof-prog-name 1521,57117
(defpgcustom prog-args 1534,57752
(defpgcustom prog-env 1547,58327
(defcustom proof-shell-auto-terminate-commands 1556,58753
(defcustom proof-shell-pre-sync-init-cmd 1565,59150
(defcustom proof-shell-init-cmd 1579,59709
(defcustom proof-shell-restart-cmd 1590,60179
(defcustom proof-shell-quit-cmd 1595,60334
(defcustom proof-shell-quit-timeout 1600,60501
(defcustom proof-shell-cd-cmd 1610,60949
(defcustom proof-shell-start-silent-cmd 1627,61616
(defcustom proof-shell-stop-silent-cmd 1636,61992
(defcustom proof-shell-silent-threshold 1645,62329
(defcustom  proof-shell-inform-file-processed-cmd 1653,62663
(defcustom  proof-shell-inform-file-retracted-cmd 1674,63586
(defcustom proof-auto-multiple-files 1702,64857
(defcustom proof-cannot-reopen-processed-files 1717,65578
(defcustom proof-shell-require-command-regexp 1731,66245
(defcustom proof-done-advancing-require-function 1742,66707
(defcustom proof-shell-quiet-errors 1748,66947
(defcustom proof-shell-prompt-pattern 1761,67281
(defcustom proof-shell-wakeup-char 1771,67703
(defcustom proof-shell-annotated-prompt-regexp 1777,67934
(defcustom proof-shell-abort-goal-regexp 1793,68574
(defcustom proof-shell-error-regexp 1798,68709
(defcustom proof-shell-truncate-before-error 1818,69503
(defcustom pg-next-error-regexp 1832,70046
(defcustom pg-next-error-filename-regexp 1847,70656
(defcustom pg-next-error-extract-filename 1871,71694
(defcustom proof-shell-interrupt-regexp 1878,71937
(defcustom proof-shell-proof-completed-regexp 1892,72529
(defcustom proof-shell-clear-response-regexp 1905,73037
(defcustom proof-shell-clear-goals-regexp 1912,73336
(defcustom proof-shell-start-goals-regexp 1919,73629
(defcustom proof-shell-end-goals-regexp 1927,73996
(defcustom proof-shell-eager-annotation-start 1933,74238
(defcustom proof-shell-eager-annotation-start-length 1951,74976
(defcustom proof-shell-eager-annotation-end 1962,75403
(defcustom proof-shell-assumption-regexp 1978,76079
(defcustom proof-shell-process-file 1988,76491
(defcustom proof-shell-retract-files-regexp 2010,77443
(defcustom proof-shell-compute-new-files-list 2019,77779
(defcustom pg-use-specials-for-fontify 2031,78324
(defcustom pg-special-char-regexp 2039,78672
(defcustom proof-shell-set-elisp-variable-regexp 2044,78816
(defcustom proof-shell-match-pgip-cmd 2077,80288
(defcustom proof-shell-issue-pgip-cmd 2086,80618
(defcustom proof-shell-query-dependencies-cmd 2095,80974
(defcustom proof-shell-theorem-dependency-list-regexp 2102,81234
(defcustom proof-shell-theorem-dependency-list-split 2118,81894
(defcustom proof-shell-show-dependency-cmd 2127,82319
(defcustom proof-shell-identifier-under-mouse-cmd 2134,82588
(defcustom proof-shell-trace-output-regexp 2157,83669
(defcustom proof-shell-thms-output-regexp 2173,84213
(defcustom proof-shell-unicode 2186,84599
(defcustom proof-shell-filename-escapes 2193,84869
(defcustom proof-shell-process-connection-type 2210,85549
(defcustom proof-shell-strip-crs-from-input 2233,86596
(defcustom proof-shell-strip-crs-from-output 2245,87085
(defcustom proof-shell-insert-hook 2253,87453
(defcustom proof-pre-shell-start-hook 2293,89417
(defcustom proof-shell-handle-delayed-output-hook2309,89889
(defcustom proof-shell-handle-error-or-interrupt-hook2315,90104
(defcustom proof-shell-pre-interrupt-hook2333,90853
(defcustom proof-shell-process-output-system-specific 2343,91223
(defcustom proof-state-change-hook 2362,92088
(defcustom proof-shell-font-lock-keywords 2373,92470
(defcustom proof-shell-syntax-table-entries 2381,92798
(defgroup proof-goals 2399,93170
(defcustom pg-subterm-first-special-char 2404,93291
(defcustom pg-subterm-anns-use-stack 2412,93603
(defcustom pg-goals-change-goal 2421,93907
(defcustom pbp-goal-command 2426,94022
(defcustom pbp-hyp-command 2431,94178
(defcustom pg-subterm-help-cmd 2436,94340
(defcustom pg-goals-error-regexp 2443,94576
(defcustom proof-shell-result-start 2448,94736
(defcustom proof-shell-result-end 2454,94970
(defcustom pg-subterm-start-char 2460,95183
(defcustom pg-subterm-sep-char 2474,95765
(defcustom pg-subterm-end-char 2480,95944
(defcustom pg-topterm-char 2486,96101
(defcustom proof-goals-font-lock-keywords 2503,96707
(defcustom proof-resp-font-lock-keywords 2517,97386
(defcustom pg-before-fontify-output-hook 2529,97964
(defcustom pg-after-fontify-output-hook 2537,98324
(defgroup proof-x-symbol 2549,98578
(defcustom proof-xsym-extra-modes 2554,98706
(defcustom proof-xsym-font-lock-keywords 2567,99335
(defcustom proof-xsym-activate-command 2575,99712
(defcustom proof-xsym-deactivate-command 2582,99948
(defpgcustom x-symbol-language 2589,100190
(defpgcustom favourites 2604,100637
(defpgcustom menu-entries 2609,100827
(defpgcustom help-menu-entries 2616,101064
(defpgcustom keymap 2623,101327
(defpgcustom completion-table 2628,101498
(defpgcustom tags-program 2638,101863
(defcustom proof-general-name 2650,102036
(defcustom proof-general-home-page2655,102193
(defcustom proof-unnamed-theorem-name2661,102352
(defcustom proof-universal-keys2669,102628

generic/proof-depends.el,824
(defvar proof-thm-names-of-files 19,540
(defvar proof-def-names-of-files 25,824
(defun proof-depends-module-name-for-buffer 34,1128
(defun proof-depends-module-of 44,1570
(defun proof-depends-names-in-same-file 52,1864
(defun proof-depends-process-dependencies 71,2484
(defun proof-dependency-in-span-context-menu 124,4226
(defun proof-dep-alldeps-menu 147,5129
(defun proof-dep-make-alldeps-menu 153,5356
(defun proof-dep-split-deps 171,5852
(defun proof-dep-make-submenu 192,6551
(defun proof-make-highlight-depts-menu 202,6904
(defun proof-goto-dependency 212,7208
(defun proof-show-dependency 218,7431
(defconst pg-dep-span-priority 225,7721
(defconst pg-ordinary-span-priority 226,7757
(defun proof-highlight-depcs 228,7799
(defun proof-highlight-depts 238,8229
(defun proof-dep-unhighlight 249,8703

generic/proof-easy-config.el,192
(defconst proof-easy-config-derived-modes-table15,492
(defun proof-easy-config-define-derived-modes 22,898
(defun proof-easy-config-check-setup 59,2510
(defmacro proof-easy-config 91,3835

generic/proof.el,516
(deflocal proof-buffer-type 35,900
(defvar proof-shell-busy 38,1013
(defvar proof-included-files-list 43,1169
(defvar proof-script-buffer 66,2185
(defvar proof-previous-script-buffer 70,2325
(defvar proof-shell-buffer 75,2579
(defvar proof-goals-buffer 78,2665
(defvar proof-response-buffer 81,2720
(defvar proof-trace-buffer 84,2781
(defvar proof-thms-buffer 88,2935
(defvar proof-shell-error-or-interrupt-seen 92,3090
(defvar proof-shell-proof-completed 97,3315
(defvar proof-terminal-string 109,3860

generic/proof-indent.el,301
(defun proof-indent-indent 13,353
(defun proof-indent-offset 22,619
(defun proof-indent-inner-p 39,1219
(defun proof-indent-goto-prev 48,1526
(defun proof-indent-calculate 55,1859
(defun proof-indent-line 74,2575
(defun proof-indent-pad-eol 98,3376
(defun proof-indent-pad-eol-region 116,3970

generic/proof-menu.el,2739
(defvar proof-display-some-buffers-count 19,467
(defun proof-display-some-buffers 21,512
(defun proof-menu-define-keys 80,2714
(define-key map 83,2862
(define-key map 84,2914
(define-key map 85,2965
(define-key map 86,3018
(define-key map 87,3072
(define-key map 88,3134
(define-key map 89,3194
(define-key map 90,3256
(define-key map 93,3429
(define-key map 97,3666
(define-key map 98,3720
(define-key map 99,3785
(define-key map 100,3859
(define-key map 103,4040
(define-key map 104,4106
(define-key map 107,4312
(define-key map 108,4378
(define-key map 110,4493
(define-key map 111,4556
(define-key map 113,4641
(define-key map 120,4967
(define-key map 121,5026
(defun proof-menu-define-main 141,5616
(defun proof-menu-define-specific 151,5817
(defun proof-assistant-menu-update 186,6834
(defvar proof-help-menu203,7442
(defvar proof-show-hide-menu211,7720
(defvar proof-buffer-menu220,8033
(defconst proof-quick-opts-menu278,10123
(defun proof-quick-opts-vars 391,14681
(defun proof-quick-opts-changed-from-defaults-p 415,15395
(defun proof-quick-opts-changed-from-saved-p 419,15500
(defun proof-quick-opts-save 430,15852
(defun proof-quick-opts-reset 435,16020
(defconst proof-config-menu447,16288
(defconst proof-advanced-menu454,16467
(defvar proof-menu 470,17046
(defvar proof-main-menu479,17330
(defvar proof-aux-menu489,17556
(defvar proof-menu-favourites 505,17878
(defun proof-menu-define-favourites-menu 508,17985
(defmacro proof-defshortcut 529,18656
(defmacro proof-definvisible 545,19311
(defun proof-def-favourite 566,20136
(defvar proof-make-favourite-cmd-history 589,21111
(defvar proof-make-favourite-menu-history 592,21196
(defun proof-save-favourites 595,21282
(defun proof-del-favourite 600,21430
(defun proof-read-favourite 617,21991
(defun proof-add-favourite 642,22794
(defvar proof-assistant-settings 669,23845
(defvar proof-menu-settings 676,24208
(defun proof-menu-define-settings-menu 679,24282
(defun proof-menu-entry-name 699,25026
(defun proof-menu-entry-for-setting 711,25498
(defun proof-settings-vars 729,25988
(defun proof-settings-changed-from-defaults-p 734,26165
(defun proof-settings-changed-from-saved-p 738,26271
(defun proof-settings-save 742,26374
(defun proof-settings-reset 747,26541
(defun proof-defpacustom-fn 755,26787
(defmacro defpacustom 831,29671
(defun proof-assistant-invisible-command-ifposs 842,30312
(defun proof-maybe-askprefs 864,31287
(defun proof-assistant-settings-cmd 871,31491
(defun proof-assistant-format 888,32151
(defvar proof-assistant-format-table 912,33210
(defun proof-assistant-format-bool 920,33579
(defun proof-assistant-format-int 923,33692
(defun proof-assistant-format-string 926,33784

generic/proof-mmm.el,113
(defun proof-mmm-support-available 25,909
(defun proof-mmm-set-global 49,1757
(defun proof-mmm-enable 64,2298

generic/proof-script.el,5105
(defvar proof-last-theorem-dependencies 41,1048
(defvar proof-nesting-depth 45,1210
(defvar proof-element-counters 52,1441
(deflocal proof-active-buffer-fake-minor-mode 58,1581
(deflocal proof-script-buffer-file-name 61,1707
(defun proof-next-element-count 75,2231
(defun proof-element-id 84,2558
(defun proof-next-element-id 88,2727
(deflocal proof-script-last-entity 102,3043
(defun proof-script-find-next-entity 109,3323
(deflocal proof-locked-span 185,6065
(deflocal proof-queue-span 192,6331
(defun proof-span-read-only 204,6845
(defun proof-strict-read-only 211,7102
(defsubst proof-set-queue-endpoints 230,7989
(defsubst proof-set-locked-endpoints 234,8130
(defsubst proof-detach-queue 238,8274
(defsubst proof-detach-locked 242,8406
(defsubst proof-set-queue-start 246,8542
(defsubst proof-set-locked-end 250,8668
(defsubst proof-set-queue-end 265,9215
(defun proof-init-segmentation 275,9471
(defun proof-restart-buffers 307,10842
(defun proof-script-buffers-with-spans 329,11764
(defun proof-script-remove-all-spans-and-deactivate 339,12120
(defun proof-script-clear-queue-spans 343,12308
(defun proof-unprocessed-begin 361,12849
(defun proof-script-end 369,13103
(defun proof-queue-or-locked-end 378,13404
(defun proof-locked-end 392,14067
(defun proof-locked-region-full-p 408,14437
(defun proof-locked-region-empty-p 416,14694
(defun proof-only-whitespace-to-locked-region-p 420,14844
(defun proof-in-locked-region-p 433,15480
(defun proof-goto-end-of-locked 445,15743
(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 462,16502
(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 473,16983
(defun proof-end-of-locked-visible-p 487,17636
(defun proof-goto-end-of-queue-or-locked-if-not-visible 496,18087
(defvar pg-idioms 515,18737
(defvar pg-visibility-specs 518,18833
(deflocal pg-script-portions 523,19040
(defun pg-clear-script-portions 526,19162
(defun pg-add-script-element 544,19826
(defun pg-remove-script-element 547,19902
(defsubst pg-visname 555,20180
(defun pg-add-element 559,20325
(defun pg-open-invisible-span 593,21954
(defun pg-remove-element 604,22317
(defun pg-make-element-invisible 611,22587
(defun pg-make-element-visible 617,22844
(defun pg-toggle-element-visibility 622,23023
(defun pg-redisplay-for-gnuemacs 630,23353
(defun pg-show-all-portions 637,23624
(defun pg-show-all-proofs 655,24295
(defun pg-hide-all-proofs 660,24423
(defun pg-add-proof-element 665,24554
(defun pg-span-name 679,25174
(defun pg-set-span-helphighlights 700,25881
(defun proof-complete-buffer-atomic 725,26705
(defun proof-register-possibly-new-processed-file 766,28620
(defun proof-inform-prover-file-retracted 817,30748
(defun proof-auto-retract-dependencies 836,31534
(defun proof-unregister-buffer-file-name 890,34074
(defun proof-protected-process-or-retract 936,35897
(defun proof-deactivate-scripting-auto 963,37067
(defun proof-deactivate-scripting 972,37425
(defun proof-activate-scripting 1109,42830
(defun proof-toggle-active-scripting 1237,48584
(defun proof-done-advancing 1278,49945
(defun proof-done-advancing-comment 1363,53351
(defun proof-done-advancing-save 1382,54093
(defun proof-make-goalsave 1475,57708
(defun proof-get-name-from-goal 1490,58451
(defun proof-done-advancing-autosave 1509,59477
(defun proof-done-advancing-other 1574,62023
(defun proof-segment-up-to-parser 1602,62982
(defun proof-script-generic-parse-find-comment-end 1665,65058
(defun proof-script-generic-parse-cmdend 1674,65474
(defun proof-script-generic-parse-cmdstart 1699,66369
(defun proof-script-generic-parse-sexp 1762,69077
(defun proof-cmdstart-add-segment-for-cmd 1786,70013
(defun proof-segment-up-to-cmdstart 1838,72212
(defun proof-segment-up-to-cmdend 1899,74572
(defun proof-semis-to-vanillas 1970,77219
(defun proof-script-new-command-advance 2009,78545
(defun proof-script-next-command-advance 2051,80286
(defun proof-assert-until-point-interactive 2063,80727
(defun proof-assert-until-point 2089,81849
(defun proof-assert-next-command2142,84281
(defun proof-goto-point 2190,86544
(defun proof-insert-pbp-command 2207,87070
(defun proof-done-retracting 2239,88143
(defun proof-setup-retract-action 2266,89254
(defun proof-last-goal-or-goalsave 2276,89737
(defun proof-retract-target 2299,90577
(defun proof-retract-until-point-interactive 2384,94218
(defun proof-retract-until-point 2392,94603
(define-derived-mode proof-mode 2437,96464
(defun proof-script-set-visited-file-name 2473,97950
(defun proof-script-set-buffer-hooks 2497,98952
(defun proof-script-kill-buffer-fn 2507,99448
(defun proof-config-done-related 2551,101270
(defun proof-generic-goal-command-p 2623,103838
(defun proof-generic-state-preserving-p 2628,104050
(defun proof-generic-count-undos 2637,104567
(defun proof-generic-find-and-forget 2666,105597
(defconst proof-script-important-settings2717,107422
(defun proof-config-done 2730,107959
(defun proof-setup-parsing-mechanism 2827,111507
(defun proof-setup-imenu 2871,113360
(defun proof-setup-func-menu 2888,113965

generic/proof-shell.el,3337
(defvar proof-shell-last-output 19,457
(defvar proof-marker 63,1713
(defvar proof-action-list 66,1810
(defvar proof-shell-silent 74,1986
(defvar proof-shell-last-prompt 88,2469
(defvar proof-shell-last-output-kind 93,2699
(defvar proof-shell-delayed-output 114,3521
(defvar proof-shell-delayed-output-kind 117,3642
(defcustom proof-shell-active-scripting-indicator126,3845
(defun proof-shell-ready-prover 179,5321
(defun proof-shell-live-buffer 193,5861
(defun proof-shell-available-p 200,6096
(defun proof-grab-lock 206,6319
(defun proof-release-lock 223,7036
(defcustom proof-shell-fiddle-frames 243,7592
(deflocal proof-eagerly-raise 250,7833
(defun proof-shell-start 253,7939
(defvar proof-shell-kill-function-hooks 469,16250
(defun proof-shell-kill-function 472,16348
(defun proof-shell-clear-state 563,20208
(defun proof-shell-exit 578,20651
(defun proof-shell-bail-out 590,21096
(defun proof-shell-restart 599,21573
(defvar proof-shell-no-response-display 641,22957
(defvar proof-shell-urgent-message-marker 644,23061
(defvar proof-shell-urgent-message-scanner 647,23182
(defun proof-shell-handle-output 651,23309
(defun proof-shell-handle-delayed-output 724,26632
(defvar proof-shell-no-error-display 759,28054
(defun proof-shell-handle-error 765,28260
(defun proof-shell-handle-interrupt 783,29096
(defun proof-shell-error-or-interrupt-action 797,29718
(defun proof-goals-pos 824,30923
(defun proof-pbp-focus-on-first-goal 829,31128
(defsubst proof-shell-string-match-safe 841,31663
(defun proof-shell-process-output 846,31831
(defvar proof-shell-insert-space-fudge 957,36471
(defun proof-shell-insert 966,36780
(defun proof-shell-command-queue-item 1040,39692
(defun proof-shell-set-silent 1045,39849
(defun proof-shell-start-silent-item 1051,40068
(defun proof-shell-clear-silent 1057,40260
(defun proof-shell-stop-silent-item 1063,40482
(defun proof-shell-should-be-silent 1070,40754
(defun proof-append-alist 1083,41310
(defun proof-start-queue 1139,43437
(defun proof-extend-queue 1150,43786
(defun proof-shell-exec-loop 1161,44167
(defun proof-shell-insert-loopback-cmd 1226,46755
(defun proof-shell-message 1263,48463
(defun proof-shell-process-urgent-message 1269,48679
(defvar proof-shell-minibuffer-urgent-interactive-input-history 1478,57567
(defun proof-shell-minibuffer-urgent-interactive-input 1480,57637
(defun proof-shell-process-urgent-messages 1492,58007
(defun proof-shell-filter 1564,61177
(defun proof-shell-filter-process-output 1717,67514
(defvar pg-last-tracing-output-time 1770,69568
(defvar pg-tracing-slow-mode 1773,69674
(defconst pg-slow-mode-duration 1776,69763
(defconst pg-fast-tracing-mode-threshold 1779,69845
(defvar pg-tracing-cleanup-timer 1782,69973
(defun pg-tracing-tight-loop 1784,70012
(defun pg-finish-tracing-display 1827,71730
(defun proof-shell-dont-show-annotations 1840,72036
(defun proof-shell-show-annotations 1856,72571
(defun proof-shell-wait 1877,73068
(defun proof-done-invisible 1897,73978
(defun proof-shell-invisible-command 1940,75701
(defun proof-shell-invisible-cmd-get-result 1973,76951
(defun proof-shell-invisible-command-invisible-result 1990,77632
(define-derived-mode proof-shell-mode 2010,78136
(defconst proof-shell-important-settings2081,80807
(defun proof-shell-config-done 2086,80907

generic/proof-site.el,720
(defgroup proof-general 20,594
(defgroup proof-general-internals 33,1010
(defun proof-home-directory-fn 42,1203
(defcustom proof-home-directory53,1573
(defcustom proof-images-directory62,1939
(defcustom proof-info-directory68,2140
(defcustom proof-assistant-table97,3389
(defun proof-string-to-list 163,5571
(defcustom proof-assistants 179,6062
(defun proof-ready-for-assistant 215,7475
(defconst proof-general-version 328,11690
(defconst proof-general-short-version 331,11831
(defconst proof-general-version-year 336,11991
(defcustom proof-assistant-cusgrp 350,12459
(defcustom proof-assistant-internals-cusgrp 358,12762
(defcustom proof-assistant 366,13074
(defcustom proof-assistant-symbol 374,13343

generic/proof-splash.el,727
(defcustom proof-splash-enable 16,433
(defcustom proof-splash-time 21,585
(defcustom proof-splash-contents29,870
(defconst proof-splash-startup-msg 58,1979
(defconst proof-splash-welcome 67,2358
(defun proof-get-image 86,2922
(defvar proof-splash-timeout-conf 138,4746
(defun proof-splash-centre-spaces 141,4859
(defun proof-splash-remove-screen 169,6028
(defun proof-splash-remove-buffer 190,6777
(defvar proof-splash-seen 206,7441
(defun proof-splash-display-screen 210,7558
(defun proof-splash-message 285,10717
(defun proof-splash-timeout-waiter 295,11080
(defvar proof-splash-old-frame-title-format 312,11819
(defun proof-splash-set-frame-titles 314,11869
(defun proof-splash-unset-frame-titles 323,12185

generic/proof-syntax.el,923
(defun proof-ids-to-regexp 16,447
(defun proof-anchor-regexp 22,703
(defconst proof-no-regexp26,805
(defun proof-regexp-alt 31,900
(defun proof-regexp-region 40,1186
(defun proof-re-search-forward-region 49,1609
(defun proof-search-forward 62,2104
(defun proof-replace-regexp-in-string 68,2356
(defun proof-re-search-forward 74,2610
(defun proof-re-search-backward 80,2871
(defun proof-string-match 86,3135
(defun proof-string-match-safe 92,3367
(defun proof-stringfn-match 96,3572
(defun proof-looking-at 103,3832
(defun proof-looking-at-safe 109,4022
(defun proof-looking-at-syntactic-context 113,4162
(defun proof-replace-string 125,4525
(defun proof-replace-regexp 130,4716
(defvar proof-id 138,4935
(defun proof-ids 144,5155
(defun proof-zap-commas 157,5716
(defun proof-format 175,6285
(defun proof-format-filename 194,6924
(defun proof-insert 243,8402
(defun proof-splice-separator 279,9411

generic/proof-toolbar.el,2880
(defun proof-toolbar-function 49,1595
(defun proof-toolbar-icon 52,1692
(defun proof-toolbar-enabler 55,1793
(defun proof-toolbar-function-with-enabler 58,1901
(defun proof-toolbar-make-icon 65,2074
(defun proof-toolbar-make-toolbar-item 83,2674
(defvar proof-toolbar 122,4055
(deflocal proof-toolbar-itimer 126,4184
(defun proof-toolbar-setup 130,4294
(defun proof-toolbar-build 175,5914
(defalias 'proof-toolbar-enable proof-toolbar-enable
249,8475
(defun proof-toolbar-setup-refresh 258,8714
(defun proof-toolbar-disable-refresh 279,9484
(deflocal proof-toolbar-refresh-flag 286,9806
(defun proof-toolbar-refresh 292,10077
(defvar proof-toolbar-enablers296,10222
(defvar proof-toolbar-enablers-last-state302,10398
(defun proof-toolbar-really-refresh 306,10489
(defun proof-toolbar-undo-enable-p 359,12319
(defalias 'proof-toolbar-undo proof-toolbar-undo
364,12467
(defun proof-toolbar-delete-enable-p 370,12586
(defalias 'proof-toolbar-delete proof-toolbar-delete
376,12760
(defun proof-toolbar-lockedend-enable-p 383,12896
(defalias 'proof-toolbar-lockedend proof-toolbar-lockedend
386,12946
(defun proof-toolbar-next-enable-p 395,13034
(defalias 'proof-toolbar-next proof-toolbar-next
399,13141
(defun proof-toolbar-goto-enable-p 406,13235
(defalias 'proof-toolbar-goto proof-toolbar-goto
409,13308
(defun proof-toolbar-retract-enable-p 416,13384
(defalias 'proof-toolbar-retract proof-toolbar-retract
420,13495
(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p
427,13574
(defalias 'proof-toolbar-use proof-toolbar-use
428,13642
(defun proof-toolbar-restart-enable-p 434,13720
(defalias 'proof-toolbar-restart proof-toolbar-restart
439,13881
(defun proof-toolbar-goal-enable-p 445,13959
(defalias 'proof-toolbar-goal proof-toolbar-goal
452,14192
(defun proof-toolbar-qed-enable-p 459,14264
(defalias 'proof-toolbar-qed proof-toolbar-qed
465,14416
(defun proof-toolbar-state-enable-p 471,14488
(defalias 'proof-toolbar-state proof-toolbar-state
474,14559
(defun proof-toolbar-context-enable-p 480,14628
(defalias 'proof-toolbar-context proof-toolbar-context
483,14701
(defun proof-toolbar-info-enable-p 491,14861
(defalias 'proof-toolbar-info proof-toolbar-info
494,14905
(defun proof-toolbar-command-enable-p 500,14974
(defalias 'proof-toolbar-command proof-toolbar-command
503,15045
(defun proof-toolbar-help-enable-p 509,15125
(defun proof-toolbar-help 512,15170
(defun proof-toolbar-find-enable-p 520,15264
(defalias 'proof-toolbar-find proof-toolbar-find
523,15333
(defun proof-toolbar-visibility-enable-p 529,15431
(defalias 'proof-toolbar-visibility proof-toolbar-visibility
532,15531
(defun proof-toolbar-interrupt-enable-p 538,15619
(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt
541,15683
(defun proof-toolbar-make-menu-item 550,15872
(defconst proof-toolbar-scripting-menu572,16560

generic/proof-utils.el,2064
(defmacro deflocal 18,472
(defmacro proof-with-current-buffer-if-exists 25,710
(defmacro proof-with-script-buffer 34,1087
(defmacro proof-map-buffers 45,1474
(defmacro proof-sym 50,1659
(defun proof-try-require 55,1820
(defun proof-save-some-buffers 68,2148
(defun proof-set-value 92,2839
(defun proof-ass-symv 152,5016
(defmacro proof-ass-sym 157,5203
(defun proof-defpgcustom-fn 161,5342
(defun undefpgcustom 186,6426
(defmacro defpgcustom 192,6650
(defmacro proof-ass 201,7067
(defun proof-defpgdefault-fn 206,7243
(defmacro defpgdefault 220,7702
(defmacro defpgfun 231,8064
(defun proof-file-truename 246,8358
(defun proof-file-to-buffer 250,8541
(defun proof-files-to-buffers 261,8870
(defun proof-buffers-in-mode 268,9153
(defun pg-save-from-death 282,9604
(defun proof-define-keys 301,10222
(deflocal proof-font-lock-keywords 330,11223
(deflocal proof-font-lock-keywords-case-fold-search 336,11488
(defun proof-font-lock-configure-defaults 339,11611
(defun proof-font-lock-clear-font-lock-vars 387,13924
(defun proof-font-lock-set-font-lock-vars 398,14297
(defun proof-fontify-region 405,14510
(defun pg-remove-specials 463,16738
(defun pg-remove-specials-in-string 473,17072
(defun proof-fontify-buffer 480,17259
(defun proof-warn-if-unset 493,17500
(defun proof-get-window-for-buffer 498,17718
(defun proof-display-and-keep-buffer 535,19356
(defun proof-clean-buffer 567,20665
(defun proof-message 582,21286
(defun proof-warning 587,21499
(defun pg-internal-warning 593,21781
(defun proof-debug 601,22100
(defun proof-switch-to-buffer 616,22783
(defun proof-resize-window-tofit 649,24475
(defun proof-submit-bug-report 749,28487
(defun proof-deftoggle-fn 774,29353
(defmacro proof-deftoggle 789,30008
(defun proof-defintset-fn 796,30382
(defmacro proof-defintset 810,31037
(defun proof-defstringset-fn 817,31414
(defmacro proof-defstringset 830,32041
(defun pg-custom-save-vars 844,32506
(defun pg-custom-reset-vars 862,33232
(defun proof-locate-executable 875,33569
(defconst proof-extra-fls904,34750

generic/proof-x-symbol.el,613
(defvar proof-x-symbol-initialized 54,2151
(defun proof-x-symbol-tokenlang-file 57,2246
(defun proof-x-symbol-support-maybe-available 63,2428
(defun proof-x-symbol-initialize 83,3173
(defun proof-x-symbol-enable 178,7036
(defun proof-x-symbol-refresh-output-buffers 208,8353
(defun proof-x-symbol-mode-associated-buffers 223,9107
(defalias 'proof-x-symbol-decode-region proof-x-symbol-decode-region
245,9811
(defun proof-x-symbol-encode-shell-input 247,9877
(defun proof-x-symbol-set-language 264,10468
(defun proof-x-symbol-shell-config 269,10639
(defun proof-x-symbol-config-output-buffer 317,12806

lib/bufhist.el,1021
(defun bufhist-ring-update 31,1132
(defgroup bufhist 40,1454
(defcustom bufhist-ring-size 44,1535
(defvar bufhist-ring 49,1646
(defvar bufhist-ring-pos 52,1720
(defvar bufhist-lastswitch-modified-tick 55,1799
(defvar bufhist-read-only-history 58,1905
(defvar bufhist-saved-mode-line-format 61,1976
(defconst bufhist-mode-line-format-entry64,2077
(defun bufhist-get-buffer-contents 75,2494
(defun bufhist-restore-buffer-contents 87,2978
(defun bufhist-checkpoint 95,3265
(defun bufhist-erase-buffer 103,3632
(defun bufhist-checkpoint-and-erase 113,3977
(defun bufhist-switch-to-index 119,4163
(defun bufhist-first 158,5767
(defun bufhist-last 163,5926
(defun bufhist-prev 168,6072
(defun bufhist-next 176,6295
(defun bufhist-delete 181,6435
(defun bufhist-clear 190,6798
(defun bufhist-init 204,7179
(defun bufhist-exit 227,8100
(defun bufhist-set-readwrite 238,8336
(defun bufhist-before-change-function 253,8956
(defconst bufhist-minor-mode-map270,9497
(define-minor-mode bufhist-mode282,9959

lib/bufregring.el,935
(defun bufhist-ring-update 25,793
(defgroup bufhist 34,1115
(defcustom bufhist-ring-size 38,1196
(defvar bufhist-ring 43,1306
(defvar bufhist-ring-pos 46,1380
(defvar bufhist-lastswitch-modified-tick 49,1459
(defvar bufhist-read-only-history 52,1565
(defvar bufhist-saved-mode-line-format 55,1636
(defconst bufhist-mode-line-format-entry58,1737
(defun bufhist-get-buffer-contents 69,2154
(defun bufhist-restore-buffer-contents 77,2506
(defun bufhist-checkpoint 83,2670
(defun bufhist-switch-to-index 89,2867
(defun bufhist-first 111,3836
(defun bufhist-last 116,3981
(defun bufhist-prev 121,4115
(defun bufhist-next 128,4321
(defun bufhist-delete 133,4461
(defun bufhist-clear 140,4698
(defun bufhist-init 149,4911
(defun bufhist-exit 172,5832
(defun bufhist-set-readwrite 183,6068
(defun bufhist-before-change-function 196,6536
(defconst bufhist-minor-mode-map208,6813
(define-minor-mode bufhist-mode218,7178

lib/bufregs.el,961
(defun bufregs-ring-update 27,936
(defgroup bufregs 36,1258
(defcustom bufregs-ring-size 40,1345
(defvar bufregs-ring 45,1455
(defvar bufregs-ring-pos 48,1529
(defvar bufregs-lastswitch-modified-tick 51,1608
(defvar bufregs-read-only-history 54,1714
(defvar bufregs-saved-mode-line-format 57,1785
(defconst bufregs-mode-line-format-entry60,1886
(defun bufregs-restore-buffer-contents 71,2303
(defun bufregs-makereg 76,2461
(defun bufregs-newregion 83,2663
(defun bufregs-delete-region 96,3065
(defun bufregs-switch-to-index 106,3361
(defun bufregs-first 116,3716
(defun bufregs-last 121,3861
(defun bufregs-prev 126,3995
(defun bufregs-next 133,4201
(defun bufregs-delete 138,4341
(defun bufregs-clear 145,4584
(defun bufregs-init 154,4796
(defun bufregs-exit 177,5716
(defun bufregs-set-readwrite 188,5952
(defun bufregs-before-change-function 201,6420
(defconst bufregs-minor-mode-map213,6697
(define-minor-mode bufregs-mode223,7062

lib/holes.el,2447
(defvar holes-doc 35,993
(defvar holes-default-hole 143,4976
(defvar holes-active-hole 147,5145
(defcustom holes-empty-hole-string 154,5354
(defcustom holes-empty-hole-regexp 157,5465
(defcustom holes-search-limit 164,5756
(defface active-hole-face176,6132
(defface inactive-hole-face188,6580
(defun holes-region-beginning-or-nil 203,7056
(defun holes-region-end-or-nil 208,7166
(defun holes-copy-active-region 213,7264
(defun holes-is-hole-p 220,7463
(defun holes-hole-start-position 226,7570
(defun holes-hole-end-position 233,7759
(defun holes-hole-buffer 240,7943
(defun holes-hole-at 247,8118
(defun holes-active-hole-exist-p 254,8293
(defun holes-active-hole-start-position 264,8551
(defun holes-active-hole-end-position 274,8923
(defun holes-active-hole-buffer 285,9292
(defun holes-goto-active-hole 296,9598
(defun holes-highlight-hole-as-active 308,9866
(defun holes-highlight-hole 318,10178
(defun holes-disable-active-hole 329,10470
(defun holes-set-active-hole 347,11013
(defun holes-is-in-hole-p 360,11359
(defun holes-make-hole 367,11502
(defun holes-make-hole-at 393,12248
(defun holes-clear-hole 413,12724
(defun holes-clear-hole-at 425,13013
(defun holes-map-holes 434,13272
(defun holes-mapcar-holes 442,13455
(defun holes-clear-all-buffer-holes 448,13622
(defun holes-next 459,13922
(defun holes-next-after-active-hole 466,14173
(defun holes-set-active-hole-next 474,14392
(defun holes-replace-segment 496,14945
(defun holes-replace 506,15299
(defun holes-replace-active-hole 537,16494
(defun holes-replace-update-active-hole 546,16795
(defun holes-delete-update-active-hole 567,17485
(defun holes-set-make-active-hole 574,17699
(defun holes-mouse-replace-active-hole 621,19327
(defun holes-destroy-hole 641,19866
(defun holes-hole-at-event 658,20277
(defun holes-mouse-destroy-hole 663,20390
(defun holes-mouse-forget-hole 673,20630
(defun holes-mouse-set-make-active-hole 689,20940
(defun holes-mouse-set-active-hole 711,21501
(defun holes-set-point-next-hole-destroy 723,21765
(defvar hole-map739,22215
(defvar holes-mode-map755,22835
(defun holes-replace-string-by-holes-backward 792,24300
(defun holes-skeleton-end-hook 810,25001
(defconst holes-jump-doc 818,25365
(defun holes-replace-string-by-holes-backward-jump 825,25572
(defun holes-abbrev-complete 842,26203
(defun holes-insert-and-expand 851,26510
(defvar holes-mode 862,26942
(defun holes-mode 868,27138

lib/local-vars-list.el,410
(defconst local-vars-list-doc 25,759
(defun local-vars-list-help 38,1213
(defun local-vars-list-insert-empty-zone 43,1399
(defun local-vars-list-find 81,2107
(defun local-vars-list-goto-var 100,2882
(defun local-vars-list-get-current 126,3932
(defun local-vars-list-set-current 147,4782
(defun local-vars-list-get 170,5499
(defun local-vars-list-get-safe 187,6031
(defun local-vars-list-set 192,6225

lib/proof-compat.el,921
(defvar proof-running-on-XEmacs 24,760
(defvar proof-running-on-Emacs21 26,882
(defvar proof-running-on-win32 30,1129
(defun pg-custom-undeclare-variable 41,1562
(defun subst-char-in-string 112,3702
(defun replace-regexp-in-string 126,4256
(defconst menuvisiblep 188,6969
(defun set-window-text-height 205,7588
(defmacro save-selected-frame 231,8538
(defun warn 270,9840
(defun redraw-modeline 277,10095
(defun replace-in-string 292,10662
(defun proof-buffer-syntactic-context-emulate 341,12180
(defvar read-shell-command-map374,13487
(defun read-shell-command 392,14189
(defun remassq 404,14670
(defun remassoc 416,15059
(defun frames-of-buffer 429,15504
(defmacro with-selected-window 468,16767
(defun pg-pop-to-buffer 504,17892
(defun process-live-p 555,19744
(defalias 'proof-buffer-syntactic-context proof-buffer-syntactic-context
622,22141
(defun select-buffers-tab-buffers-by-mode 666,23489

lib/span.el,132
(defsubst delete-spans 24,499
(defsubst span-property-safe 28,653
(defsubst set-span-start 32,792
(defsubst set-span-end 36,924

lib/span-extent.el,972
(defsubst make-span 16,557
(defsubst detach-span 20,679
(defsubst set-span-endpoints 24,766
(defsubst set-span-property 28,899
(defsubst span-read-only 32,1026
(defsubst span-read-write 36,1130
(defun span-give-warning 40,1237
(defun span-write-warning 44,1335
(defsubst span-property 49,1535
(defsubst delete-span 53,1650
(defsubst mapcar-spans 59,1821
(defsubst span-at 63,2027
(defsubst span-at-before 67,2144
(defsubst span-start 72,2341
(defsubst span-end 76,2470
(defsubst prev-span 80,2593
(defsubst next-span 84,2739
(defsubst span-live-p 88,2881
(defun span-raise 96,3153
(defalias 'span-object span-object
100,3252
(defalias 'span-string span-string
101,3291
(defsubst make-detached-span 104,3377
(defsubst span-buffer 109,3439
(defsubst span-detached-p 114,3531
(defsubst set-span-face 119,3643
(defsubst fold-spans 124,3739
(defsubst set-span-properties 129,3937
(defsubst set-span-keymap 134,4046
(defsubst span-at-event 139,4161

lib/span-overlay.el,1201
(defalias 'span-start span-start
16,543
(defalias 'span-end span-end
17,581
(defalias 'set-span-property set-span-property
18,615
(defalias 'span-property span-property
19,658
(defalias 'make-span make-span
20,697
(defalias 'detach-span detach-span
21,733
(defalias 'set-span-endpoints set-span-endpoints
22,773
(defalias 'span-buffer span-buffer
23,818
(defun span-read-only-hook 25,859
(defun span-read-only 29,991
(defun span-read-write 44,1767
(defun span-give-warning 50,1986
(defun span-write-warning 54,2094
(defun span-lt 61,2420
(defun spans-at-point-prop 66,2561
(defun spans-at-region-prop 72,2726
(defun span-at 80,2970
(defsubst delete-span 86,3184
(defsubst mapcar-spans 93,3406
(defun span-at-before 97,3610
(defun prev-span 114,4336
(defun next-span 120,4487
(defsubst span-live-p 149,5712
(defun span-raise 155,5878
(defalias 'span-object span-object
161,6121
(defun span-string 163,6162
(defun set-span-properties 169,6344
(defun span-find-span 181,6599
(defsubst span-at-event 188,6906
(defun make-detached-span 193,7030
(defun fold-spans 198,7126
(defsubst span-detached-p 213,7660
(defsubst set-span-face 217,7775
(defun set-span-keymap 221,7872

lib/texi-docstring-magic.el,584
(defun texi-docstring-magic-find-face 85,2997
(defun texi-docstring-magic-splice-sep 90,3162
(defconst texi-docstring-magic-munge-table100,3467
(defun texi-docstring-magic-untabify 190,7187
(defun texi-docstring-magic-munge-docstring 200,7502
(defun texi-docstring-magic-texi 239,8789
(defun texi-docstring-magic-format-default 252,9229
(defun texi-docstring-magic-texi-for 268,9864
(defconst texi-docstring-magic-comment326,11824
(defun texi-docstring-magic 332,11978
(defun texi-docstring-magic-face-at-point 366,13058
(defun texi-docstring-magic-insert-magic 381,13581

lib/xml-fixed.el,528
(defsubst xml-node-name 82,2904
(defsubst xml-node-attributes 87,3023
(defsubst xml-node-children 92,3141
(defun xml-get-children 97,3277
(defun xml-get-attribute 107,3600
(defun xml-parse-file 123,4064
(defun xml-parse-region 144,4648
(defun xml-parse-tag 179,5693
(defun xml-parse-attlist 284,9162
(defun xml-skip-dtd 321,10552
(defun xml-parse-dtd 338,11188
(defun xml-parse-elem-type 408,13266
(defun xml-substitute-special 449,14421
(defun xml-debug-print 470,15228
(defun xml-debug-print-internal 474,15320

mmm/mmm-auto.el,343
(defvar mmm-autoloaded-classes67,2675
(defun mmm-autoload-class 89,3438
(defvar mmm-changed-buffers-list 129,5005
(defun mmm-major-mode-change 132,5112
(defun mmm-check-changed-buffers 145,5633
(defun mmm-mode-on-maybe 155,6006
(defalias 'mmm-add-find-file-hooks mmm-add-find-file-hooks
167,6424
(defun mmm-add-find-file-hook 168,6484

mmm/mmm-class.el,416
(defun mmm-get-class-spec 42,1295
(defun mmm-get-class-parameter 59,2008
(defun mmm-set-class-parameter 63,2174
(defun* mmm-apply-class75,2538
(defun* mmm-apply-classes90,3176
(defun* mmm-apply-all 110,3942
(defun* mmm-ify124,4389
(defun* mmm-match-region206,7472
(defun mmm-match->point 267,10161
(defun mmm-match-and-verify 281,10683
(defun mmm-get-form 307,11741
(defun mmm-default-get-form 318,12237

mmm/mmm-cmds.el,712
(defun mmm-ify-by-class 41,1209
(defun mmm-ify-region 63,1933
(defun mmm-ify-by-regexp75,2361
(defun mmm-parse-buffer 97,3037
(defun mmm-parse-region 106,3373
(defun mmm-parse-block 115,3752
(defun mmm-get-block 132,4503
(defun mmm-reparse-current-region 146,4834
(defun mmm-clear-current-region 167,5508
(defun mmm-clear-regions 172,5672
(defun mmm-clear-all-regions 177,5818
(defun* mmm-end-current-region 185,5978
(defun mmm-narrow-to-submode-region 220,7401
(defun mmm-insert-region 239,8015
(defun mmm-insert-by-key 258,8877
(defun mmm-get-insertion-spec 339,12282
(defun mmm-insertion-help 366,13361
(defun mmm-display-insertion-key 376,13731
(defun mmm-get-all-insertion-keys 398,14553

mmm/mmm-compat.el,418
(defvar mmm-xemacs 40,1312
(defvar mmm-keywords-used49,1615
(defmacro mmm-regexp-opt 90,2612
(defvar mmm-evaporate-property109,3261
(defmacro mmm-set-keymap-default 127,4027
(defmacro mmm-event-key 136,4469
(defvar skeleton-positions 145,4688
(defun mmm-fixup-skeleton 146,4719
(defmacro mmm-make-temp-buffer 158,5156
(defvar mmm-font-lock-available-p 171,5552
(defmacro mmm-set-font-lock-defaults 178,5766

mmm/mmm-cweb.el,228
(defvar mmm-cweb-section-tags38,1116
(defvar mmm-cweb-section-regexp41,1163
(defvar mmm-cweb-c-part-tags44,1253
(defvar mmm-cweb-c-part-regexp47,1312
(defun mmm-cweb-in-limbo 50,1396
(defun mmm-cweb-verify-brief-c 57,1621

mmm/mmm-mason.el,410
(defvar mmm-mason-perl-tags41,1235
(defvar mmm-mason-pseudo-perl-tags45,1376
(defvar mmm-mason-non-perl-tags48,1452
(defvar mmm-mason-perl-tags-regexp51,1553
(defvar mmm-mason-pseudo-perl-tags-regexp56,1748
(defvar mmm-mason-tag-names-regexp61,1965
(defun mmm-mason-verify-inline 66,2185
(defun mmm-mason-start-line 156,5089
(defun mmm-mason-end-line 161,5154
(defun mmm-mason-set-mode-line 168,5248

mmm/mmm-mode.el,1024
(defun mmm-mode 101,3866
(defun mmm-mode-on 140,5371
(defun mmm-mode-off 181,7131
(defvar mmm-mode-map 206,7864
(defvar mmm-mode-prefix-map 209,7939
(defvar mmm-mode-menu-map 212,8049
(defun mmm-define-key 215,8140
(define-key mmm-mode-prefix-map 239,8895
(define-key mmm-mode-prefix-map 246,9153
(define-key mmm-mode-map 249,9264
(define-key mmm-mode-menu-map 252,9366
(define-key mmm-mode-menu-map 254,9438
(define-key mmm-mode-menu-map 256,9497
(define-key mmm-mode-menu-map 258,9578
(define-key mmm-mode-menu-map 260,9659
(define-key mmm-mode-menu-map 262,9746
(define-key mmm-mode-menu-map 265,9840
(define-key mmm-mode-menu-map 267,9900
(define-key mmm-mode-menu-map 270,9991
(define-key mmm-mode-menu-map 272,10051
(define-key mmm-mode-menu-map 274,10158
(define-key mmm-mode-menu-map 276,10243
(define-key mmm-mode-menu-map 279,10329
(define-key mmm-mode-menu-map 281,10389
(define-key mmm-mode-menu-map 283,10502
(define-key mmm-mode-menu-map 285,10587
(define-key mmm-mode-map 288,10670

mmm/mmm-noweb.el,1291
(defvar mmm-noweb-code-mode 44,1352
(defvar mmm-noweb-quote-mode 50,1649
(defvar mmm-noweb-quote-string 54,1806
(defvar mmm-noweb-quote-number 58,1929
(defvar mmm-noweb-narrowing 62,2045
(defun mmm-noweb-chunk 68,2176
(defun mmm-noweb-quote 84,2876
(defun mmm-noweb-quote-name 89,3042
(defun mmm-noweb-chunk-name 95,3302
(defun mmm-noweb-regions 140,4748
(defun mmm-noweb-narrow-to-doc-chunk 166,5616
(defun mmm-noweb-fill-chunk 189,6386
(defun mmm-noweb-fill-paragraph-chunk 208,7070
(defun mmm-noweb-fill-named-chunk 222,7487
(defun mmm-noweb-auto-fill-doc-chunk 238,8064
(defun mmm-noweb-auto-fill-doc-mode 246,8283
(defun mmm-noweb-auto-fill-code-mode 251,8473
(defun mmm-noweb-complete-chunk 259,8685
(defvar mmm-noweb-chunk-history 292,9689
(defun mmm-noweb-goto-chunk 295,9767
(defun mmm-noweb-goto-next 307,10091
(defun mmm-noweb-goto-previous 319,10448
(defvar mmm-noweb-map 336,10852
(defvar mmm-noweb-prefix-map 337,10896
(define-key mmm-noweb-map 338,10947
(define-key mmm-noweb-prefix-map 347,11390
(defun mmm-noweb-bind-keys 352,11656
(defun mmm-syntax-region-list 368,12070
(defun mmm-syntax-other-regions 377,12426
(defun mmm-word-other-regions 389,12897
(defun mmm-space-other-regions 395,13066
(defun mmm-undo-syntax-other-regions 401,13237

mmm/mmm-region.el,1643
(defsubst mmm-overlay-at 54,1748
(defun mmm-overlays-at 59,1933
(defun mmm-included-p 72,2386
(defun mmm-overlays-containing 112,3875
(defun mmm-overlays-contained-in 125,4313
(defun mmm-overlays-overlapping 138,4753
(defun mmm-sort-overlays 149,5116
(defvar mmm-current-overlay 158,5386
(defvar mmm-previous-overlay 163,5601
(defvar mmm-current-submode 168,5789
(defvar mmm-previous-submode 173,5989
(defun mmm-update-current-submode 178,6162
(defun mmm-set-current-submode 199,6978
(defun mmm-submode-at 210,7470
(defun mmm-match-front 219,7745
(defun mmm-match-back 238,8506
(defun mmm-front-start 257,9251
(defun mmm-back-end 265,9555
(defun mmm-valid-submode-region 278,9902
(defun* mmm-make-region305,11058
(defun mmm-make-overlay 431,16429
(defun mmm-get-face 459,17562
(defun mmm-clear-overlays 470,17854
(defun mmm-update-mode-info 486,18321
(defun mmm-update-submode-region 571,22606
(defun mmm-add-hooks 588,23364
(defun mmm-remove-hooks 592,23499
(defun mmm-get-local-variables-list 598,23626
(defun mmm-get-locals 618,24546
(defun mmm-get-saved-local 631,25127
(defun mmm-set-local-variables 635,25292
(defun mmm-get-saved-local-variables 646,25733
(defun mmm-save-changed-local-variables 654,26050
(defun mmm-clear-local-variables 673,26908
(defun mmm-enable-font-lock 684,27187
(defun mmm-update-font-lock-buffer 692,27447
(defun mmm-refontify-maybe 705,27879
(defun mmm-submode-changes-in 720,28401
(defun mmm-regions-in 731,28849
(defun mmm-regions-alist 745,29419
(defun mmm-fontify-region 762,30065
(defun mmm-fontify-region-list 782,31096
(defun mmm-beginning-of-syntax 804,32012

mmm/mmm-rpm.el,154
(defconst mmm-rpm-sh-start-tags48,1617
(defvar mmm-rpm-sh-end-tags53,1841
(defvar mmm-rpm-sh-start-regexp57,2015
(defvar mmm-rpm-sh-end-regexp61,2193

mmm/mmm-sample.el,168
(defvar mmm-here-doc-mode-alist 84,2614
(defun mmm-here-doc-get-mode 93,3099
(defun mmm-file-variables-verify 208,6817
(defun mmm-file-variables-find-back 232,7853

mmm/mmm-univ.el,34
(defun mmm-univ-get-mode 38,1205

mmm/mmm-utils.el,282
(defmacro mmm-valid-buffer 41,1309
(defmacro mmm-save-all 60,1953
(defun mmm-format-string 73,2242
(defun mmm-format-matches 84,2694
(defmacro mmm-save-keyword 107,3484
(defmacro mmm-save-keywords 115,3811
(defun mmm-looking-back-at 128,4344
(defun mmm-make-marker 145,4912

mmm/mmm-vars.el,2667
(defgroup mmm 99,3072
(defvar mmm-c-derived-modes106,3182
(defvar mmm-save-local-variables 110,3301
(defvar mmm-buffer-saved-locals 336,10161
(defvar mmm-region-saved-locals-defaults 341,10361
(defvar mmm-region-saved-locals-for-dominant 347,10621
(defgroup mmm-faces 357,10998
(defcustom mmm-submode-decoration-level 363,11169
(defface mmm-init-submode-face 381,12041
(defface mmm-cleanup-submode-face 385,12181
(defface mmm-declaration-submode-face 389,12318
(defface mmm-comment-submode-face 393,12464
(defface mmm-output-submode-face 397,12617
(defface mmm-special-submode-face 401,12766
(defface mmm-code-submode-face 405,12930
(defface mmm-default-submode-face 409,13069
(defface mmm-delimiter-face 414,13277
(defcustom mmm-mode-string 421,13403
(defcustom mmm-submode-mode-line-format 426,13534
(defvar mmm-primary-mode-display-name 443,14189
(defvar mmm-buffer-mode-display-name 448,14403
(defun mmm-set-mode-line 454,14702
(defvar mmm-classes 478,15510
(defvar mmm-global-classes 484,15755
(defcustom mmm-mode-ext-classes-alist 491,15937
(defun mmm-add-mode-ext-class 510,16755
(defcustom mmm-major-mode-preferences519,17080
(defun mmm-add-to-major-mode-preferences 537,17878
(defun mmm-ensure-modename 553,18664
(defun mmm-modename->function 562,18974
(defcustom mmm-delimiter-mode 576,19437
(defcustom mmm-mode-prefix-key 586,19706
(defcustom mmm-command-modifiers 591,19833
(defcustom mmm-insert-modifiers 605,20466
(defcustom mmm-use-old-command-keys 620,21144
(defun mmm-use-old-command-keys 630,21608
(defcustom mmm-mode-hook 638,21807
(defun mmm-run-constructed-hook 658,22614
(defun mmm-run-major-hook 666,23000
(defun mmm-run-submode-hook 669,23077
(defvar mmm-class-hooks-run 672,23164
(defun mmm-run-class-hook 677,23336
(defvar mmm-primary-mode-entry-hook 682,23508
(defcustom mmm-major-mode-hook 697,24155
(defun mmm-run-major-mode-hook 711,24786
(defcustom mmm-global-mode 724,25327
(defcustom mmm-never-modes740,26022
(defvar mmm-set-file-name-for-modes 758,26322
(defvar mmm-mode 769,26681
(defvar mmm-primary-mode 777,26889
(defvar mmm-classes-alist 788,27255
(defun mmm-add-classes 943,35462
(defun mmm-add-group 948,35627
(defun mmm-add-to-group 958,36077
(defconst mmm-version 972,36574
(defun mmm-version 975,36639
(defvar mmm-temp-buffer-name 982,36782
(defvar mmm-interactive-history 988,36912
(defun mmm-add-to-history 994,37181
(defun mmm-clear-history 997,37264
(defvar mmm-mode-ext-classes 1005,37449
(defun mmm-get-mode-ext-classes 1010,37660
(defun mmm-clear-mode-ext-classes 1019,38036
(defun mmm-mode-ext-applies 1023,38161
(defun mmm-get-all-classes 1037,38645

TODO.developer,26
   function to 400,16075

doc/ProofGeneral.texi,5747
@node Top166,5019
@node Preface203,6126
@node Latest news for 3.5 and 3.6Latest news for 3.5 and 3.6
226,6722
@node Future265,8410
@node Credits300,9960
@node Introducing Proof GeneralIntroducing Proof General
398,13376
@node Quick start guideQuick start guide
453,15368
@node Features of Proof GeneralFeatures of Proof General
507,17937
@node Supported proof assistantsSupported proof assistants
596,21862
@node Prerequisites for this manualPrerequisites for this manual
648,23858
@node Organization of this manualOrganization of this manual
692,25484
@node Basic Script ManagementBasic Script Management
718,26312
@node Walkthrough example in Isabelle/IsarWalkthrough example in Isabelle/Isar
737,26917
@node Proof scriptsProof scripts
964,35452
@node Script buffersScript buffers
1007,37572
@node Locked queue and editing regionsLocked queue and editing regions
1029,38149
@node Goal-save sequencesGoal-save sequences
1085,40296
@node Active scripting bufferActive scripting buffer
1122,41782
@node Summary of Proof General buffersSummary of Proof General buffers
1191,45202
@node Script editing commandsScript editing commands
1253,47876
@node Script processing commandsScript processing commands
1331,50734
@node Proof assistant commandsProof assistant commands
1459,56035
@node Toolbar commandsToolbar commands
1609,61039
@node Interrupting during trace outputInterrupting during trace output
1633,61968
@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
1672,63892
@node Goals buffer commandsGoals buffer commands
1686,64392
@node Advanced Script ManagementAdvanced Script Management
1775,67925
@node Visibility of completed proofsVisibility of completed proofs
1806,69079
@node Switching between proof scriptsSwitching between proof scripts
1861,71002
@node View of processed files View of processed files 
1898,72974
@node Retracting across filesRetracting across files
1958,76025
@node Asserting across filesAsserting across files
1971,76656
@node Automatic multiple file handlingAutomatic multiple file handling
1984,77222
@node Escaping script managementEscaping script management
2009,78256
@node Experimental featuresExperimental features
2067,80459
@node Support for other PackagesSupport for other Packages
2101,81722
@node Syntax highlightingSyntax highlighting
2133,82597
@node X-Symbol supportX-Symbol support
2172,84218
@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)
2231,86764
@node Support for outline modeSupport for outline mode
2290,88894
@node Support for completionSupport for completion
2316,90024
@node Support for tagsSupport for tags
2373,92189
@node Customizing Proof GeneralCustomizing Proof General
2425,94518
@node Basic optionsBasic options
2465,96188
@node How to customizeHow to customize
2489,96946
@node Display customizationDisplay customization
2540,99048
@node User optionsUser options
2665,104282
@node Changing facesChanging faces
2929,113692
@node Tweaking configuration settingsTweaking configuration settings
3004,116361
@node Hints and TipsHints and Tips
3061,118887
@node Adding your own keybindingsAdding your own keybindings
3080,119488
@node Using file variablesUsing file variables
3136,122021
@node Using abbreviationsUsing abbreviations
3195,124207
@node LEGO Proof GeneralLEGO Proof General
3234,125623
@node LEGO specific commandsLEGO specific commands
3275,126992
@node LEGO tagsLEGO tags
3295,127447
@node LEGO customizationsLEGO customizations
3305,127694
@node Coq Proof GeneralCoq Proof General
3337,128613
@node Coq-specific commandsCoq-specific commands
3353,129022
@node Coq-specific variablesCoq-specific variables
3375,129529
@node Editing multiple proofsEditing multiple proofs
3397,130187
@node User-loaded tacticsUser-loaded tactics
3421,131295
@node Holes featureHoles feature
3485,133769
@node Isabelle Proof GeneralIsabelle Proof General
3512,135056
@node Classic IsabelleClassic Isabelle
3581,138379
@node ML filesML files
3597,138817
@node Theory filesTheory files
3668,141242
@node General commands for IsabelleGeneral commands for Isabelle
3722,143713
@node Specific commands for IsabelleSpecific commands for Isabelle
3734,144195
@node Isabelle customizationsIsabelle customizations
3763,145135
@node Isabelle/Isar3828,147233
@node General commands for Isabelle/IsarGeneral commands for Isabelle/Isar
3849,147996
@node Specific commands for Isabelle/IsarSpecific commands for Isabelle/Isar
3856,148250
@node Logics and SettingsLogics and Settings
3956,151159
@node HOL Proof GeneralHOL Proof General
3997,152848
@node Shell Proof GeneralShell Proof General
4038,154633
@node Obtaining and InstallingObtaining and Installing
4074,156092
@node Obtaining Proof GeneralObtaining Proof General
4090,156505
@node Installing Proof General from tarballInstalling Proof General from tarball
4121,157744
@node Installing Proof General from RPM packageInstalling Proof General from RPM package
4146,158576
@node Setting the names of binariesSetting the names of binaries
4161,158984
@node Notes for syssiesNotes for syssies
4189,159924
@node Known BugsKnown Bugs
4262,162858
@node References4275,163259
@node History of Proof GeneralHistory of Proof General
4315,164283
@node Old News for 3.0Old News for 3.0
4406,168385
@node Old News for 3.1Old News for 3.1
4476,172079
@node Old News for 3.2Old News for 3.2
4502,173251
@node Old News for 3.3Old News for 3.3
4563,176254
@node Old News for 3.4Old News for 3.4
4582,177151
@node Function IndexFunction Index
4605,178207
@node Variable IndexVariable Index
4609,178283
@node Keystroke IndexKeystroke Index
4613,178363
@node Concept IndexConcept Index
4617,178429

doc/PG-adapting.texi,3776
@node Top157,4773
@node Introduction195,5918
@node Future236,7571
@node Credits272,9167
@node Beginning with a New ProverBeginning with a New Prover
282,9459
@node Overview of adding a new proverOverview of adding a new prover
323,11408
@node Demonstration instance and easy configurationDemonstration instance and easy configuration
397,14829
@node Major modes used by Proof GeneralMajor modes used by Proof General
466,18220
@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands
539,21303
@node Settings for generic user-level commandsSettings for generic user-level commands
554,21849
@node Menu configurationMenu configuration
599,23585
@node Toolbar configurationToolbar configuration
623,24503
@node Proof Script SettingsProof Script Settings
681,26748
@node Recognizing commands and commentsRecognizing commands and comments
703,27328
@node Recognizing proofsRecognizing proofs
824,32855
@node Recognizing other elementsRecognizing other elements
936,37669
@node Configuring undo behaviourConfiguring undo behaviour
1062,43147
@node Nested proofsNested proofs
1200,48488
@node Safe (state-preserving) commandsSafe (state-preserving) commands
1240,50115
@node Activate scripting hookActivate scripting hook
1263,51061
@node Automatic multiple filesAutomatic multiple files
1287,51925
@node Completions1309,52772
@node Proof Shell SettingsProof Shell Settings
1349,54250
@node Proof shell commandsProof shell commands
1380,55532
@node Script input to the shellScript input to the shell
1543,62407
@node Settings for matching various output from proof processSettings for matching various output from proof process
1610,65450
@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process
1741,71214
@node Hooks and other settingsHooks and other settings
1951,80767
@node Goals Buffer SettingsGoals Buffer Settings
2047,84600
@node Splash Screen SettingsSplash Screen Settings
2124,87708
@node Global ConstantsGlobal Constants
2150,88466
@node Handling Multiple FilesHandling Multiple Files
2176,89315
@node Configuring Editing SyntaxConfiguring Editing Syntax
2328,97099
@node Configuring Font LockConfiguring Font Lock
2385,99216
@node Configuring X-SymbolConfiguring X-Symbol
2472,103459
@node Writing More Lisp CodeWriting More Lisp Code
2532,105982
@node Default values for generic settingsDefault values for generic settings
2549,106627
@node Adding prover-specific configurationsAdding prover-specific configurations
2579,107710
@node Useful variablesUseful variables
2622,108992
@node Useful functions and macrosUseful functions and macros
2648,109786
@node Internals of Proof GeneralInternals of Proof General
2750,113663
@node Spans2778,114571
@node Proof General site configurationProof General site configuration
2791,114945
@node Configuration variable mechanismsConfiguration variable mechanisms
2871,118089
@node Global variablesGlobal variables
2989,123325
@node Proof script modeProof script mode
3059,125875
@node Proof shell modeProof shell mode
3318,137530
@node Debugging3724,153577
@node Plans and IdeasPlans and Ideas
3767,154472
@node Proof by pointing and similar featuresProof by pointing and similar features
3788,155194
@node Granularity of atomic command sequencesGranularity of atomic command sequences
3826,156852
@node Browser mode for script files and theoriesBrowser mode for script files and theories
3871,159077
@node Demonstration InstantiationsDemonstration Instantiations
3901,160108
@node demoisa-easy.el3917,160539
@node demoisa.el3980,162777
@node Function IndexFunction Index
4148,168305
@node Variable IndexVariable Index
4152,168381
@node Concept IndexConcept Index
4161,168560

lib/holes-load.el,0

generic/proof-system.el,0

generic/_pkg.el,0

twelf/x-symbol-twelf.el,0

pgshell/pgshell.el,0

lego/x-symbol-lego.el,0

isar/x-symbol-isar.el,0

isar/isar-autotest.el,0

isa/x-symbol-isa.el,0

isa/interface-setup.el,0

hol98/x-symbol-hol98.el,0

hol98/hol98.el,0

demoisa/demoisa-easy.el,0

coq/coq-autotest.el,0

ccc/ccc.el,0

acl2/x-symbol-acl2.el,0

acl2/acl2.el,0