ccc/ccc.el,87
(defvar ccc-keywords 17,587
(defvar ccc-tactics 18,613
(defvar ccc-tacticals 19,638

coq/coq-abbrev.el,495
(defun holes-show-doc 12,313
(defun coq-local-vars-list-show-doc 16,390
(defconst coq-tactics-menu21,490
(defconst coq-tactics-abbrev-table26,667
(defconst coq-tacticals-menu29,784
(defconst coq-tacticals-abbrev-table33,893
(defconst coq-commands-menu36,984
(defconst coq-commands-abbrev-table43,1207
(defconst coq-terms-menu46,1296
(defconst coq-terms-abbrev-table51,1434
(defun coq-install-abbrevs 58,1628
(defpgdefault menu-entries78,2365
(defpgdefault help-menu-entries141,4384

coq/coq-db.el,668
(defconst coq-syntax-db 23,544
(defvar coq-user-tactics-db59,1917
(defun coq-insert-from-db 69,2266
(defun coq-build-regexp-list-from-db 87,2998
(defun max-length-db 109,3981
(defun coq-build-menu-from-db-internal 121,4256
(defun coq-build-title-menu 156,5879
(defun coq-sort-menu-entries 165,6247
(defun coq-build-menu-from-db 171,6374
(defcustom coq-holes-minor-mode 193,7213
(defun coq-build-abbrev-table-from-db 199,7357
(defun filter-state-preserving 218,7995
(defun filter-state-changing 223,8149
(defface coq-solve-tactics-face230,8370
(defface coq-cheat-face239,8700
(defconst coq-solve-tactics-face 247,8948
(defconst coq-cheat-face 251,9112

coq/coq.el,5448
(defcustom coq-translate-to-v8 46,1310
(defun coq-build-prog-args 52,1490
(defcustom coq-compile-file-command 62,1786
(defcustom coq-use-makefile 70,2105
(defcustom coq-default-undo-limit 78,2328
(defconst coq-shell-init-cmd83,2456
(defcustom coq-prog-env 89,2583
(defconst coq-shell-restart-cmd 97,2833
(defvar coq-shell-prompt-pattern99,2887
(defvar coq-shell-cd 107,3191
(defvar coq-shell-proof-completed-regexp 111,3351
(defvar coq-goal-regexp114,3503
(defun coq-library-directory 121,3617
(defcustom coq-tags 128,3796
(defconst coq-interrupt-regexp 133,3946
(defcustom coq-www-home-page 138,4067
(defvar coq-outline-regexp145,4235
(defvar coq-outline-heading-end-regexp 152,4447
(defvar coq-shell-outline-regexp 154,4501
(defvar coq-shell-outline-heading-end-regexp 155,4551
(defconst coq-state-preserving-tactics-regexp161,4716
(defconst coq-state-changing-commands-regexp163,4816
(defconst coq-state-preserving-commands-regexp165,4923
(defconst coq-commands-regexp167,5034
(defvar coq-retractable-instruct-regexp169,5111
(defvar coq-non-retractable-instruct-regexp171,5201
(defun coq-set-undo-limit 205,6078
(defun build-list-id-from-string 209,6208
(defun coq-last-prompt-info 221,6706
(defun coq-last-prompt-info-safe 233,7238
(defvar coq-last-but-one-statenum 239,7495
(defvar coq-last-but-one-proofnum 245,7792
(defvar coq-last-but-one-proofstack 248,7890
(defun coq-get-span-statenum 251,8000
(defun coq-get-span-proofnum 256,8115
(defun coq-get-span-proofstack 261,8230
(defun coq-set-span-statenum 266,8374
(defun coq-get-span-goalcmd 271,8505
(defun coq-set-span-goalcmd 276,8619
(defun coq-set-span-proofnum 281,8749
(defun coq-set-span-proofstack 286,8880
(defun proof-last-locked-span 291,9040
(defun coq-set-state-infos 306,9643
(defun count-not-intersection 345,11638
(defun coq-find-and-forget 376,12888
(defvar coq-current-goal 395,13775
(defun coq-goal-hyp 398,13840
(defun coq-state-preserving-p 411,14272
(defconst notation-print-kinds-table425,14773
(defun coq-PrintScope 429,14940
(defun coq-guess-or-ask-for-string 447,15489
(defun coq-ask-do 461,16057
(defun coq-SearchIsos 470,16442
(defun coq-SearchConstant 476,16675
(defun coq-SearchRewrite 480,16768
(defun coq-SearchAbout 484,16866
(defun coq-Print 488,16958
(defun coq-About 492,17080
(defun coq-LocateConstant 496,17197
(defun coq-LocateLibrary 502,17332
(defun coq-addquotes 508,17482
(defun coq-LocateNotation 510,17530
(defun coq-Pwd 517,17728
(defun coq-Inspect 523,17860
(defun coq-PrintSection(527,17960
(defun coq-Print-implicit 531,18053
(defun coq-Check 536,18204
(defun coq-Show 541,18312
(defun coq-Compile 555,18755
(defun coq-guess-command-line 567,19073
(defpacustom use-editing-holes 606,20745
(defun coq-mode-config 616,21082
(defun coq-shell-mode-config 720,24966
(defun coq-goals-mode-config 763,26765
(defun coq-response-config 770,27009
(defpacustom print-fully-explicit 795,27834
(defpacustom print-implicit 800,27982
(defpacustom print-coercions 805,28148
(defpacustom print-match-wildcards 810,28292
(defpacustom print-elim-types 815,28472
(defpacustom printing-depth 820,28638
(defpacustom undo-depth 825,28799
(defpacustom time-commands 830,28946
(defpacustom undo-limit 834,29056
(defpacustom auto-compile-vos 839,29158
(defun coq-maybe-compile-buffer 868,30272
(defun coq-ancestors-of 904,31800
(defun coq-all-ancestors-of 927,32764
(defun coq-process-require-command 938,33111
(defun coq-included-children 943,33238
(defun coq-process-file 964,34077
(defun coq-preprocessing 979,34616
(defun coq-fake-constant-markup 993,35051
(defun coq-create-span-menu 1009,35656
(defconst module-kinds-table1026,36151
(defconst modtype-kinds-table1030,36300
(defun coq-insert-section-or-module 1034,36429
(defconst reqkinds-kinds-table1057,37287
(defun coq-insert-requires 1062,37432
(defun coq-end-Section 1078,37935
(defun coq-insert-intros 1096,38513
(defun coq-insert-infoH-hook 1109,39045
(defun coq-insert-as 1114,39253
(defun coq-insert-match 1131,39956
(defun coq-insert-tactic 1163,41138
(defun coq-insert-tactical 1169,41377
(defun coq-insert-command 1175,41626
(defun coq-insert-term 1181,41870
(define-key coq-keymap 1187,42067
(define-key coq-keymap 1188,42125
(define-key coq-keymap 1189,42182
(define-key coq-keymap 1190,42251
(define-key coq-keymap 1191,42307
(define-key coq-keymap 1192,42356
(define-key coq-keymap 1193,42414
(define-key coq-keymap 1195,42475
(define-key coq-keymap 1196,42534
(define-key coq-keymap 1198,42598
(define-key coq-keymap 1199,42658
(define-key coq-keymap 1201,42714
(define-key coq-keymap 1202,42764
(define-key coq-keymap 1203,42814
(define-key coq-keymap 1204,42864
(define-key coq-keymap 1205,42918
(define-key coq-keymap 1206,42977
(defvar last-coq-error-location 1214,43108
(defun coq-get-last-error-location 1223,43507
(defun coq-highlight-error 1271,45887
(defvar coq-allow-highlight-error 1302,47020
(defun coq-decide-highlight-error 1309,47346
(defun coq-highlight-error-hook 1314,47531
(defun first-word-of-buffer 1325,47924
(defun coq-show-first-goal 1333,48127
(defvar coq-modeline-string2 1350,48822
(defvar coq-modeline-string1 1351,48866
(defvar coq-modeline-string0 1352,48909
(defun coq-build-subgoals-string 1353,48954
(defun coq-update-minor-mode-alist 1358,49120
(defun is-not-split-vertic 1384,50191
(defun optim-resp-windows 1393,50630

coq/coq-indent.el,2223
(defconst coq-any-command-regexp20,368
(defconst coq-indent-inner-regexp23,459
(defconst coq-comment-start-regexp 33,813
(defconst coq-comment-end-regexp 34,856
(defconst coq-comment-start-or-end-regexp35,897
(defconst coq-indent-open-regexp37,1005
(defconst coq-indent-close-regexp42,1179
(defconst coq-indent-closepar-regexp 47,1360
(defconst coq-indent-closematch-regexp 48,1405
(defconst coq-indent-openpar-regexp 49,1476
(defconst coq-indent-openmatch-regexp 50,1520
(defconst coq-indent-any-regexp51,1600
(defconst coq-indent-kw56,1878
(defconst coq-indent-pattern-regexp 66,2332
(defun coq-indent-goal-command-p 70,2435
(defconst coq-end-command-regexp92,3486
(defun coq-search-comment-delimiter-forward 97,3638
(defun coq-search-comment-delimiter-backward 106,3968
(defun coq-skip-until-one-comment-backward 113,4242
(defun coq-skip-until-one-comment-forward 128,4949
(defun coq-looking-at-comment 139,5467
(defun coq-find-comment-start 143,5608
(defun coq-find-comment-end 154,6041
(defun coq-looking-at-syntactic-context 166,6534
(defconst coq-end-command-or-comment-regexp172,6756
(defconst coq-end-command-or-comment-start-regexp175,6865
(defun coq-find-not-in-comment-backward 179,6983
(defun coq-find-not-in-comment-forward 199,7884
(defun coq-find-command-end-backward 223,9023
(defun coq-find-command-end-forward 232,9414
(defun coq-find-command-end 241,9791
(defun coq-find-current-start 249,10123
(defun coq-find-real-start 258,10414
(defun coq-command-at-point 265,10633
(defun coq-indent-only-spaces-on-line 272,10910
(defun coq-indent-find-reg 278,11187
(defun coq-find-no-syntactic-on-line 292,11723
(defun coq-back-to-indentation-prevline 305,12196
(defun coq-find-unclosed 349,14104
(defun coq-find-at-same-level-zero 379,15400
(defun coq-find-unopened 407,16558
(defun coq-find-last-unopened 450,17992
(defun coq-end-offset 461,18389
(defun coq-indent-command-offset 486,19159
(defun coq-indent-expr-offset 533,20983
(defun coq-indent-comment-offset 649,25666
(defun coq-indent-offset 681,27115
(defun coq-indent-calculate 699,27977
(defun coq-indent-line 702,28065
(defun coq-indent-line-not-comments 712,28431
(defun coq-indent-region 722,28820

coq/coq-local-vars.el,280
(defconst coq-local-vars-doc 20,429
(defun coq-insert-coq-prog-name 78,2957
(defun coq-read-directory 89,3430
(defun coq-extract-directories-from-args 113,4533
(defun coq-ask-prog-args 128,5085
(defun coq-ask-prog-name 150,6149
(defun coq-ask-insert-coq-prog-name 168,6904

coq/coq-syntax.el,2563
(defcustom coq-prog-name 18,561
(defcustom coq-user-tactics-db 38,1343
(defcustom coq-user-commands-db 55,1856
(defcustom coq-user-tacticals-db 71,2375
(defcustom coq-user-solve-tactics-db 87,2896
(defcustom coq-user-cheat-tactics-db 103,3415
(defcustom coq-user-reserved-db 122,3961
(defvar coq-tactics-db140,4492
(defvar coq-solve-tactics-db298,12751
(defvar coq-solve-cheat-tactics-db321,13596
(defvar coq-tacticals-db333,13771
(defvar coq-decl-db357,14657
(defvar coq-defn-db380,15951
(defvar coq-goal-starters-db438,20329
(defvar coq-other-commands-db467,22086
(defvar coq-commands-db593,31364
(defvar coq-terms-db600,31584
(defun coq-count-match 664,34233
(defun coq-module-opening-p 680,34962
(defun coq-section-command-p 691,35373
(defun coq-goal-command-str-p 695,35470
(defun coq-goal-command-p 722,36572
(defvar coq-keywords-save-strict731,36855
(defvar coq-keywords-save740,36968
(defun coq-save-command-p 744,37046
(defvar coq-keywords-kill-goal753,37340
(defvar coq-keywords-state-changing-misc-commands757,37430
(defvar coq-keywords-goal760,37555
(defvar coq-keywords-decl763,37638
(defvar coq-keywords-defn766,37712
(defvar coq-keywords-state-changing-commands770,37787
(defvar coq-keywords-state-preserving-commands779,38047
(defvar coq-keywords-commands784,38263
(defvar coq-solve-tactics789,38411
(defvar coq-solve-cheat-tactics793,38532
(defvar coq-tacticals797,38677
(defvar coq-reserved803,38816
(defvar coq-state-changing-tactics814,39144
(defvar coq-state-preserving-tactics817,39253
(defvar coq-tactics821,39367
(defvar coq-retractable-instruct824,39456
(defvar coq-non-retractable-instruct827,39566
(defvar coq-keywords831,39694
(defvar coq-symbols838,39861
(defvar coq-error-regexp 857,40074
(defvar coq-id 860,40302
(defvar coq-id-shy 861,40327
(defvar coq-ids 863,40381
(defun coq-first-abstr-regexp 865,40422
(defcustom coq-variable-highlight-enable 868,40517
(defvar coq-font-lock-terms874,40644
(defconst coq-save-command-regexp-strict895,41643
(defconst coq-save-command-regexp899,41809
(defconst coq-save-with-hole-regexp904,41962
(defconst coq-goal-command-regexp908,42120
(defconst coq-goal-with-hole-regexp911,42220
(defconst coq-decl-with-hole-regexp915,42352
(defconst coq-defn-with-hole-regexp922,42600
(defconst coq-with-with-hole-regexp932,42888
(defconst coq-require-command-regexp939,43181
(defvar coq-font-lock-keywords-1947,43406
(defvar coq-font-lock-keywords 975,44808
(defun coq-init-syntax-table 977,44866
(defconst coq-generic-expression1006,45764

coq/coq-unicode-tokens.el,454
(defconst coq-token-format 39,1427
(defconst coq-token-match 40,1475
(defconst coq-hexcode-match 41,1506
(defun coq-unicode-tokens-set 43,1540
(defcustom coq-token-symbol-map49,1768
(defcustom coq-shortcut-alist148,4192
(defconst coq-control-char-format-regexp237,6210
(defconst coq-control-char-format 241,6335
(defconst coq-control-characters243,6378
(defconst coq-control-region-format-regexp 247,6470
(defconst coq-control-regions249,6553

demoisa/demoisa.el,349
(defcustom isabelledemo-prog-name 56,1848
(defcustom isabelledemo-web-page61,1970
(defun demoisa-config 72,2200
(defun demoisa-shell-config 93,2992
(define-derived-mode demoisa-mode 118,3921
(define-derived-mode demoisa-shell-mode 123,4044
(define-derived-mode demoisa-response-mode 128,4187
(define-derived-mode demoisa-goals-mode 132,4314

hol98/hol98.el,121
(defvar hol98-keywords 17,419
(defvar hol98-rules 18,447
(defvar hol98-tactics 19,472
(defvar hol98-tacticals 20,499

isar/isabelle-system.el,1291
(defgroup isabelle 26,716
(defcustom isabelle-web-page30,844
(defcustom isa-isabelle-command39,1061
(defvar isabelle-not-found 57,1743
(defun isa-set-isabelle-command 60,1858
(defun isa-shell-command-to-string 83,2876
(defun isa-getenv 89,3100
(defcustom isabelle-program-name-override 109,3792
(defvar isabelle-prog-name 120,4138
(defun isa-tool-list-logics 123,4248
(defcustom isabelle-logics-available 130,4487
(defcustom isabelle-chosen-logic 140,4824
(defvar isabelle-chosen-logic-prev 156,5408
(defun isabelle-hack-local-variables-function 159,5528
(defun isabelle-set-prog-name 171,5967
(defun isabelle-choose-logic 196,7157
(defun isa-view-doc 215,7919
(defun isa-tool-list-docs 224,8184
(defconst isabelle-verbatim-regexp 242,8907
(defun isabelle-verbatim 245,9049
(defcustom isabelle-refresh-logics 252,9210
(defvar isabelle-docs-menu260,9538
(defvar isabelle-logics-menu-entries 267,9823
(defun isabelle-logics-menu-calculate 270,9896
(defvar isabelle-time-to-refresh-logics 291,10538
(defun isabelle-logics-menu-refresh 295,10633
(defun isabelle-menu-bar-update-logics 310,11266
(defun isabelle-load-isar-keywords 326,11895
(defun isabelle-create-span-menu 347,12623
(defun isabelle-xml-sml-escapes 363,13065
(defun isabelle-process-pgip 366,13166

isar/isar.el,1616
(defcustom isar-keywords-name 39,915
(defpgdefault completion-table 56,1433
(defcustom isar-web-page58,1486
(defun isar-strip-terminators 72,1836
(defun isar-markup-ml 85,2213
(defun isar-mode-config-set-variables 90,2348
(defun isar-shell-mode-config-set-variables 162,5389
(defun isar-set-proof-find-theorems-command 243,8523
(defpacustom use-find-theorems-form 249,8707
(defun isar-set-undo-commands 254,8873
(defpacustom use-linear-undo 265,9324
(defun isar-configure-from-settings 270,9482
(defun isar-remove-file 278,9629
(defun isar-shell-compute-new-files-list 288,9984
(define-derived-mode isar-shell-mode 307,10564
(define-derived-mode isar-response-mode 312,10691
(define-derived-mode isar-goals-mode 317,10824
(define-derived-mode isar-mode 322,10950
(defpgdefault menu-entries379,12965
(defalias 'isar-set-command isar-set-command
409,14122
(defpgdefault help-menu-entries 411,14178
(defun isar-count-undos 414,14254
(defun isar-find-and-forget 440,15229
(defun isar-goal-command-p 480,16756
(defun isar-global-save-command-p 485,16933
(defvar isar-current-goal 506,17717
(defun isar-state-preserving-p 509,17783
(defvar isar-shell-current-line-width 534,18980
(defun isar-shell-adjust-line-width 539,19172
(defsubst isar-string-wrapping 564,19970
(defsubst isar-positions-of 573,20164
(defcustom isar-wrap-commands-singly 579,20369
(defun isar-command-wrapping 585,20565
(defun isar-preprocessing 593,20879
(defun isar-mode-config 611,21430
(defun isar-shell-mode-config 625,22083
(defun isar-response-mode-config 635,22432
(defun isar-goals-mode-config 645,22767

isar/isar-find-theorems.el,779
(defvar isar-find-theorems-data 19,565
(defun isar-find-theorems-minibuffer 35,1039
(defun isar-find-theorems-form 49,1658
(defvar isar-find-theorems-widget-number 92,3532
(defvar isar-find-theorems-widget-pattern 95,3630
(defvar isar-find-theorems-widget-intro 98,3722
(defvar isar-find-theorems-widget-elim 101,3808
(defvar isar-find-theorems-widget-dest 104,3892
(defvar isar-find-theorems-widget-name 107,3976
(defvar isar-find-theorems-widget-simp 110,4063
(defun isar-find-theorems-create-searchform115,4209
(defun isar-find-theorems-create-help 255,8752
(defun isar-find-theorems-submit-searchform298,10924
(defun isar-find-theorems-parse-criteria 376,13294
(defun isar-find-theorems-parse-number 469,16275
(defun isar-find-theorems-filter-empty 479,16552

isar/isar-keywords.el,1052
(defconst isar-keywords-major13,481
(defconst isar-keywords-minor206,3641
(defconst isar-keywords-control262,4395
(defconst isar-keywords-diag282,4872
(defconst isar-keywords-theory-begin338,5831
(defconst isar-keywords-theory-switch341,5884
(defconst isar-keywords-theory-end344,5939
(defconst isar-keywords-theory-heading347,5987
(defconst isar-keywords-theory-decl353,6094
(defconst isar-keywords-theory-script412,7075
(defconst isar-keywords-theory-goal416,7152
(defconst isar-keywords-qed429,7369
(defconst isar-keywords-qed-block436,7455
(defconst isar-keywords-qed-global439,7502
(defconst isar-keywords-proof-heading442,7551
(defconst isar-keywords-proof-goal447,7634
(defconst isar-keywords-proof-block454,7733
(defconst isar-keywords-proof-open458,7795
(defconst isar-keywords-proof-close461,7841
(defconst isar-keywords-proof-chain464,7888
(defconst isar-keywords-proof-decl471,7991
(defconst isar-keywords-proof-asm480,8112
(defconst isar-keywords-proof-asm-goal487,8207
(defconst isar-keywords-proof-script490,8262

isar/isar-mmm.el,81
(defconst isar-start-latex-regexp24,744
(defconst isar-start-sml-regexp36,1172

isar/isar-syntax.el,3799
(defconst isar-script-syntax-table-entries18,424
(defconst isar-script-syntax-table-alist42,826
(defun isar-init-syntax-table 51,1109
(defun isar-init-output-syntax-table 59,1356
(defconst isar-keyword-begin 75,1803
(defconst isar-keyword-end 76,1841
(defconst isar-keywords-theory-enclose78,1876
(defconst isar-keywords-theory83,2014
(defconst isar-keywords-save88,2145
(defconst isar-keywords-proof-enclose93,2260
(defconst isar-keywords-proof99,2421
(defconst isar-keywords-proof-context106,2598
(defconst isar-keywords-local-goal110,2705
(defconst isar-keywords-proper114,2810
(defconst isar-keywords-improper119,2929
(defconst isar-keyword-level-alist124,3061
(defconst isar-keywords-outline 139,3532
(defconst isar-keywords-fume142,3608
(defconst isar-keywords-indent-open149,3798
(defconst isar-keywords-indent-close155,3961
(defconst isar-keywords-indent-enclose159,4059
(defun isar-regexp-simple-alt 168,4253
(defun isar-ids-to-regexp 188,5013
(defconst isar-ext-first 222,6398
(defconst isar-ext-rest 223,6465
(defconst isar-long-id-stuff 225,6537
(defconst isar-id 226,6611
(defconst isar-idx 227,6681
(defconst isar-string 229,6740
(defconst isar-any-command-regexp231,6800
(defconst isar-name-regexp235,6934
(defconst isar-improper-regexp241,7229
(defconst isar-save-command-regexp245,7377
(defconst isar-global-save-command-regexp248,7478
(defconst isar-goal-command-regexp251,7592
(defconst isar-local-goal-command-regexp254,7700
(defconst isar-comment-start 257,7813
(defconst isar-comment-end 258,7848
(defconst isar-comment-start-regexp 259,7881
(defconst isar-comment-end-regexp 260,7952
(defconst isar-string-start-regexp 262,8020
(defconst isar-string-end-regexp 263,8072
(defun isar-syntactic-context 265,8123
(defconst isar-antiq-regexp280,8518
(defconst isar-nesting-regexp286,8669
(defun isar-nesting 289,8767
(defun isar-match-nesting 301,9160
(defface isabelle-class-name-face313,9491
(defface isabelle-tfree-name-face321,9674
(defface isabelle-tvar-name-face329,9863
(defface isabelle-free-name-face337,10051
(defface isabelle-bound-name-face345,10235
(defface isabelle-var-name-face353,10422
(defconst isabelle-class-name-face 361,10609
(defconst isabelle-tfree-name-face 362,10671
(defconst isabelle-tvar-name-face 363,10733
(defconst isabelle-free-name-face 364,10794
(defconst isabelle-bound-name-face 365,10855
(defconst isabelle-var-name-face 366,10917
(defvar isar-font-lock-keywords-1369,10979
(defun isar-output-flkprops 387,11987
(defun isar-output-flk 393,12239
(defvar isar-output-font-lock-keywords-1396,12348
(defun isar-strip-output-markup 432,13771
(defconst isar-shell-font-lock-keywords436,13907
(defvar isar-goals-font-lock-keywords439,13991
(defconst isar-linear-undo 473,14670
(defconst isar-undo 475,14713
(defun isar-remove 477,14756
(defun isar-undos 480,14831
(defun isar-cannot-undo 485,14992
(defconst isar-undo-commands488,15062
(defconst isar-theory-start-regexp496,15199
(defconst isar-end-regexp502,15357
(defconst isar-undo-fail-regexp506,15458
(defconst isar-undo-skip-regexp510,15562
(defconst isar-undo-ignore-regexp513,15683
(defconst isar-undo-remove-regexp516,15748
(defconst isar-any-entity-regexp524,15923
(defconst isar-named-entity-regexp529,16096
(defconst isar-unnamed-entity-regexp534,16259
(defconst isar-next-entity-regexps537,16361
(defconst isar-generic-expression545,16665
(defconst isar-indent-any-regexp556,16898
(defconst isar-indent-inner-regexp558,16991
(defconst isar-indent-enclose-regexp560,17057
(defconst isar-indent-open-regexp562,17173
(defconst isar-indent-close-regexp564,17283
(defconst isar-outline-regexp570,17420
(defconst isar-outline-heading-end-regexp 574,17573
(defconst isar-outline-heading-alist 576,17622

isar/isar-unicode-tokens.el,1289
(defgroup isabelle-tokens 25,672
(defun isar-set-and-restart-tokens 30,812
(defconst isar-control-region-format-regexp43,1165
(defconst isar-control-char-format-regexp46,1259
(defconst isar-control-char-format	49,1354
(defconst isar-control-region-format-start 50,1403
(defconst isar-control-region-format-end 51,1457
(defcustom isar-control-characters54,1513
(defcustom isar-control-regions67,1885
(defconst isar-token-format 91,2601
(defconst isar-token-variant-format-regexp95,2752
(defcustom isar-greek-letters-tokens98,2866
(defcustom isar-misc-letters-tokens138,3724
(defcustom isar-symbols-tokens150,4042
(defcustom isar-extended-symbols-tokens356,8853
(defun isar-try-char 425,10508
(defcustom isar-symbols-tokens-fallbacks429,10652
(defcustom isar-bold-nums-tokens456,11582
(defun isar-map-letters 472,11971
(defconst isar-script-letters-tokens478,12119
(defconst isar-roman-letters-tokens483,12257
(defconst isar-fraktur-letters-tokens488,12393
(defcustom isar-token-symbol-map 493,12535
(defcustom isar-user-tokens 509,13004
(defun isar-init-token-symbol-map 516,13241
(defcustom isar-symbol-shortcuts539,13796
(defcustom isar-shortcut-alist 612,16023
(defun isar-init-shortcut-alists 620,16282
(defconst isar-tokens-customizable-variables641,16945

lclam/lclam.el,524
(defcustom lclam-prog-name 18,431
(defcustom lclam-web-page24,579
(defun lclam-config 35,809
(defun lclam-shell-config 57,1600
(define-derived-mode lclam-proofscript-mode 76,2215
(define-derived-mode lclam-shell-mode 81,2338
(define-derived-mode lclam-response-mode 86,2472
(define-derived-mode lclam-goals-mode 90,2595
(defun lclam-mode 98,2823
(define-derived-mode thy-mode 135,3669
(defvar thy-mode-map 138,3767
(defun thy-add-menus 140,3794
(defun process-thy-file 179,5275
(defun update-thy-only 185,5476

lego/lego.el,1636
(defcustom lego-tags 21,534
(defcustom lego-test-all-name 26,670
(defpgdefault help-menu-entries32,828
(defpgdefault menu-entries36,988
(defvar lego-shell-handle-output47,1289
(defconst lego-process-config55,1587
(defconst lego-pretty-set-width 66,2018
(defconst lego-interrupt-regexp 70,2160
(defcustom lego-www-home-page 75,2277
(defcustom lego-www-latest-release80,2401
(defcustom lego-www-refcard86,2576
(defcustom lego-library-www-page92,2725
(defvar lego-prog-name 101,2941
(defvar lego-shell-cd 104,3010
(defvar lego-shell-proof-completed-regexp 107,3109
(defvar lego-save-command-regexp110,3249
(defvar lego-goal-command-regexp112,3339
(defvar lego-kill-goal-command 115,3430
(defvar lego-forget-id-command 116,3473
(defvar lego-undoable-commands-regexp118,3519
(defvar lego-goal-regexp 127,3893
(defvar lego-outline-regexp129,3938
(defvar lego-outline-heading-end-regexp 135,4113
(defvar lego-shell-outline-regexp 137,4166
(defvar lego-shell-outline-heading-end-regexp 138,4218
(define-derived-mode lego-shell-mode 144,4497
(define-derived-mode lego-mode 151,4658
(define-derived-mode lego-goals-mode 162,4968
(defun lego-count-undos 173,5394
(defun lego-goal-command-p 193,6212
(defun lego-find-and-forget 198,6383
(defun lego-goal-hyp 240,8199
(defun lego-state-preserving-p 249,8396
(defvar lego-shell-current-line-width 265,9099
(defun lego-shell-adjust-line-width 273,9406
(defun lego-mode-config 292,10143
(defun lego-equal-module-filename 360,12192
(defun lego-shell-compute-new-files-list 366,12467
(defun lego-shell-mode-config 376,12850
(defun lego-goals-mode-config 423,14517

lego/lego-syntax.el,600
(defconst lego-keywords-goal 15,358
(defconst lego-keywords-save 17,401
(defconst lego-commands19,472
(defconst lego-keywords31,1030
(defconst lego-tacticals 36,1207
(defconst lego-error-regexp 39,1315
(defvar lego-id 42,1473
(defvar lego-ids 44,1500
(defconst lego-arg-list-regexp 48,1696
(defun lego-decl-defn-regexp 51,1812
(defconst lego-definiendum-alternative-regexp59,2184
(defvar lego-font-lock-terms63,2368
(defconst lego-goal-with-hole-regexp89,3221
(defconst lego-save-with-hole-regexp94,3443
(defvar lego-font-lock-keywords-199,3660
(defun lego-init-syntax-table 110,4122

phox/phox.el,555
(defcustom phox-prog-name 32,916
(defcustom phox-web-page37,1018
(defcustom phox-doc-dir43,1168
(defcustom phox-lib-dir49,1315
(defcustom phox-tags-program55,1458
(defcustom phox-tags-doc61,1637
(defcustom phox-etags67,1774
(defpgdefault menu-entries88,2224
(defun phox-config 102,2417
(defun phox-shell-config 146,4341
(define-derived-mode phox-mode 170,5203
(define-derived-mode phox-shell-mode 186,5666
(define-derived-mode phox-response-mode 191,5794
(define-derived-mode phox-goals-mode 201,6155
(defpgdefault completion-table224,6941

phox/phox-extraction.el,383
(defvar phox-prog-orig 19,619
(defun phox-prog-flags-modify(21,687
(defun phox-prog-flags-extract(50,1488
(defun phox-prog-flags-erase(61,1778
(defun phox-toggle-extraction(69,1974
(defun phox-compile-theorem(81,2376
(defun phox-compile-theorem-on-cursor(87,2601
(defun phox-output 103,3079
(defun phox-output-theorem 113,3291
(defun phox-output-theorem-on-cursor(120,3590

phox/phox-font.el,231
(defvar phox-sym-lock-enabled 1,0
(defvar phox-sym-lock-color 2,60
(defvar phox-sym-lock-keywords 3,118
(defconst phox-font-lock-keywords11,511
(defconst phox-sym-lock-keywords-table70,2628
(defun phox-sym-lock-start 93,3202

phox/phox-fun.el,1659
(defconst phox-forget-id-command 11,186
(defconst phox-forget-proof-command 12,232
(defconst phox-forget-new-elim-command 13,287
(defconst phox-forget-new-intro-command 14,345
(defconst phox-forget-new-equation-command 15,405
(defconst phox-forget-close-def-command 16,471
(defconst phox-comments-regexp 18,597
(defconst phox-strict-comments-regexp 20,776
(defconst phox-ident-regexp 21,941
(defconst phox-inductive-option 22,1027
(defconst phox-spaces-regexp 23,1079
(defconst phox-sy-definition-regexp 24,1122
(defconst phox-sy-inductive-regexp 28,1309
(defconst phox-inductive-regexp 34,1522
(defconst phox-data-regexp 40,1673
(defconst phox-definition-regexp 46,1827
(defconst phox-prove-claim-regexp 50,1971
(defconst phox-new-elim-regexp 54,2077
(defconst phox-new-intro-regexp 57,2196
(defconst phox-new-rewrite-regexp 60,2317
(defconst phox-new-equation-regexp 63,2442
(defconst phox-close-def-regexp 66,2569
(defun phox-init-syntax-table 71,2706
(defvar phox-top-keywords87,3178
(defvar phox-proof-keywords135,3633
(defun phox-find-and-forget 176,3983
(defalias 'phox-assert-next-command-interactive phox-assert-next-command-interactive
255,6381
(defun phox-depend-theorem(274,7347
(defun phox-eshow-extlist(283,7636
(defun phox-flag-name(297,8233
(defun phox-path(308,8535
(defun phox-print-expression(319,8771
(defun phox-print-sort-expression(332,9227
(defun phox-priority-symbols-list(343,9539
(defun phox-search-string(355,9911
(defun phox-constraints(370,10436
(defun phox-goals(381,10692
(defvar phox-state-menu393,10901
(defun phox-delete-symbol(418,11891
(defun phox-delete-symbol-on-cursor(424,12099

phox/phox-lang.el,323
(defvar phox-lang9,306
(defun phox-lang-absurd 17,535
(defun phox-lang-suppress 22,629
(defun phox-lang-opendef 27,826
(defun phox-lang-instance 32,944
(defun phox-lang-open-instance 37,1073
(defun phox-lang-lock 42,1222
(defun phox-lang-unlock 47,1352
(defun phox-lang-prove 52,1488
(defun phox-lang-let 57,1622

phox/phox-outline.el,254
(defconst phox-outline-title-regexp 20,745
(defconst phox-outline-section-regexp 21,810
(defconst phox-outline-save-regexp 22,866
(defconst phox-outline-heading-end-regexp 39,1409
(defun phox-outline-level(45,1584
(defun phox-setup-outline 59,2058

phox/phox-pbrpm.el,513
(defun phox-pbrpm-left-paren-p 39,1671
(defun phox-pbrpm-right-paren-p 46,1874
(defun phox-pbrpm-menu-from-string 54,2078
(defun phox-pbrpm-rename-in-cmd 63,2410
(defun phox-pbrpm-get-region-name 96,3658
(defun  phox-pbrpm-escape-string 99,3785
(defun phox-pbrpm-generate-menu 103,3920
(defalias 'proof-pbrpm-generate-menu proof-pbrpm-generate-menu
310,11400
(defalias 'proof-pbrpm-left-paren-p proof-pbrpm-left-paren-p
311,11464
(defalias 'proof-pbrpm-right-paren-p proof-pbrpm-right-paren-p
312,11526

phox/phox-sym-lock.el,1398
(defcustom phox-sym-lock-enabled 19,871
(defvar phox-sym-lock-sym-count 59,2452
(defvar phox-sym-lock-ext-start 62,2522
(defvar phox-sym-lock-ext-end 64,2644
(defvar phox-sym-lock-font-size 67,2763
(defvar phox-sym-lock-keywords 72,2953
(defvar phox-sym-lock-enabled 77,3129
(defvar phox-sym-lock-color 82,3291
(defvar phox-sym-lock-mouse-face 87,3509
(defvar phox-sym-lock-mouse-face-enabled 92,3699
(defconst phox-sym-lock-with-mule 97,3889
(defun phox-sym-lock-gen-symbol 100,3973
(defun phox-sym-lock-make-symbols-atomic 108,4275
(defun phox-sym-lock-compute-font-size 135,5216
(defvar phox-sym-lock-font-name173,6635
(defun phox-sym-lock-set-foreground 216,8233
(defun phox-sym-lock-translate-char 230,8842
(defun phox-sym-lock-translate-char-or-string 239,9159
(defun phox-sym-lock-remap-face 246,9387
(defvar phox-sym-lock-clear-face266,10375
(defun phox-sym-lock 278,10794
(defun phox-sym-lock-rec 287,11198
(defun phox-sym-lock-atom-face 293,11343
(defun phox-sym-lock-pre-idle-hook-first 298,11639
(defun phox-sym-lock-pre-idle-hook-last 308,12044
(defun phox-sym-lock-enable 317,12419
(defun phox-sym-lock-disable 330,12830
(defun phox-sym-lock-mouse-face-enable 343,13246
(defun phox-sym-lock-mouse-face-disable 350,13461
(defun phox-sym-lock-font-lock-hook 357,13680
(defun font-lock-set-defaults 372,14371
(defun phox-sym-lock-patch-keywords 384,14798

phox/phox-tags.el,305
(defun phox-tags-add-table(26,869
(defun phox-tags-reset-table(35,1264
(defun phox-tags-add-doc-table(40,1374
(defun phox-tags-add-lib-table(46,1523
(defun phox-tags-add-local-table(52,1658
(defun phox-tags-create-local-table(58,1841
(defun phox-complete-tag(69,2091
(defvar phox-tags-menu76,2200

plastic/plastic.el,2759
(defcustom plastic-tags 29,608
(defcustom plastic-test-all-name 34,740
(defvar plastic-lit-string41,931
(defcustom plastic-help-menu-list45,1043
(defvar plastic-shell-handle-output59,1536
(defconst plastic-process-config67,1837
(defconst plastic-pretty-set-width 74,2085
(defconst plastic-interrupt-regexp 78,2233
(defcustom plastic-www-home-page 84,2354
(defcustom plastic-www-latest-release89,2491
(defcustom plastic-www-refcard95,2661
(defcustom plastic-library-www-page101,2792
(defcustom plastic-base111,3007
(defvar plastic-prog-name119,3178
(defun plastic-set-default-env-vars 123,3285
(defvar plastic-shell-cd131,3522
(defvar plastic-shell-proof-completed-regexp 135,3662
(defvar plastic-save-command-regexp138,3805
(defvar plastic-goal-command-regexp140,3901
(defvar plastic-kill-goal-command143,3998
(defvar plastic-forget-id-command145,4098
(defvar plastic-undoable-commands-regexp148,4178
(defvar plastic-goal-regexp 160,4625
(defvar plastic-outline-regexp162,4673
(defvar plastic-outline-heading-end-regexp 168,4851
(defvar plastic-shell-outline-regexp 170,4907
(defvar plastic-shell-outline-heading-end-regexp 171,4965
(defvar plastic-error-occurred173,5036
(define-derived-mode plastic-shell-mode 182,5353
(define-derived-mode plastic-mode 188,5535
(define-derived-mode plastic-goals-mode 204,6052
(defun plastic-count-undos 213,6397
(defun plastic-goal-command-p 233,7272
(defun plastic-find-and-forget 238,7464
(defun plastic-goal-hyp 275,8859
(defun plastic-state-preserving-p 286,9108
(defvar plastic-shell-current-line-width 309,10083
(defun plastic-shell-adjust-line-width 317,10399
(defun plastic-mode-config 344,11437
(defun plastic-show-shell-buffer 433,14696
(defun plastic-equal-module-filename 439,14799
(defun plastic-shell-compute-new-files-list 445,15077
(defun plastic-shell-mode-config 457,15471
(defun plastic-goals-mode-config 505,17274
(defun plastic-small-bar 517,17561
(defun plastic-large-bar 519,17650
(defun plastic-preprocessing 521,17788
(defun plastic-all-ctxt 573,19591
(defun plastic-send-one-undo 580,19760
(defun plastic-minibuf-cmd 590,20066
(defun plastic-minibuf 602,20538
(defun plastic-synchro 609,20744
(defun plastic-send-minibuf 614,20885
(defun plastic-had-error 622,21193
(defun plastic-reset-error 626,21368
(defun plastic-call-if-no-error 629,21507
(defun plastic-show-shell 634,21711
(define-key plastic-keymap 639,21839
(define-key plastic-keymap 640,21900
(define-key plastic-keymap 641,21961
(define-key plastic-keymap 642,22021
(define-key plastic-keymap 643,22080
(define-key plastic-keymap 644,22139
(defalias 'proof-toolbar-command proof-toolbar-command
654,22388
(defalias 'proof-minibuffer-cmd proof-minibuffer-cmd
655,22439

plastic/plastic-syntax.el,648
(defconst plastic-keywords-goal 18,536
(defconst plastic-keywords-save 20,582
(defconst plastic-commands22,656
(defconst plastic-keywords35,1263
(defconst plastic-tacticals 40,1446
(defconst plastic-error-regexp 43,1557
(defvar plastic-id 46,1690
(defvar plastic-ids 48,1720
(defconst plastic-arg-list-regexp 52,1928
(defun plastic-decl-defn-regexp 55,2047
(defconst plastic-definiendum-alternative-regexp63,2428
(defvar plastic-font-lock-terms67,2621
(defconst plastic-goal-with-hole-regexp89,3331
(defconst plastic-save-with-hole-regexp94,3557
(defvar plastic-font-lock-keywords-199,3783
(defun plastic-init-syntax-table 108,4175

generic/pg-assoc.el,81
(defun proof-associated-buffers 32,950
(defun proof-associated-windows 42,1160

generic/pg-autotest.el,443
(defvar pg-autotest-success 25,565
(defun pg-autotest-find-file 29,649
(defun pg-autotest-find-file-restart 36,929
(defmacro pg-autotest 49,1377
(defun pg-autotest-script-wholefile 63,1724
(defun pg-autotest-retract-file 80,2337
(defun pg-autotest-assert-processed 86,2473
(defun pg-autotest-assert-unprocessed 93,2727
(defun pg-autotest-message 100,2987
(defun pg-autotest-quit-prover 107,3180
(defun pg-autotest-finished 113,3361

generic/pg-custom.el,554
(defpgcustom maths-menu-enable 36,1134
(defpgcustom unicode-tokens-enable 42,1314
(defpgcustom mmm-enable 48,1491
(defpgcustom script-indent 57,1845
(defconst proof-toolbar-entries-default62,1982
(defpgcustom toolbar-entries 90,3754
(defpgcustom prog-args 109,4487
(defpgcustom prog-env 122,5062
(defpgcustom favourites 131,5488
(defpgcustom menu-entries 136,5677
(defpgcustom help-menu-entries 143,5913
(defpgcustom keymap 150,6176
(defpgcustom completion-table 155,6347
(defpgcustom tags-program 166,6721
(defpgcustom use-holes 175,7105

generic/pg-goals.el,285
(define-derived-mode proof-goals-mode 29,734
(define-key proof-goals-mode-map 57,1609
(define-key proof-goals-mode-map 59,1725
(define-key proof-goals-mode-map 60,1793
(defun proof-goals-config-done 69,1938
(defun pg-goals-display 77,2204
(defun pg-goals-button-action 118,3508

generic/pg-pbrpm.el,1808
(defvar pg-pbrpm-use-buffer-menu 41,1185
(defvar pg-pbrpm-start-goal-regexp 44,1307
(defvar pg-pbrpm-start-goal-regexp-par-num 48,1464
(defvar pg-pbrpm-end-goal-regexp 51,1587
(defvar pg-pbrpm-start-hyp-regexp 55,1739
(defvar pg-pbrpm-start-hyp-regexp-par-num 59,1900
(defvar pg-pbrpm-start-concl-regexp 63,2107
(defvar pg-pbrpm-auto-select-regexp 67,2271
(defvar pg-pbrpm-buffer-menu 74,2432
(defvar pg-pbrpm-spans 75,2466
(defvar pg-pbrpm-goal-description 76,2494
(defvar pg-pbrpm-windows-dialog-bug 77,2533
(defvar pbrpm-menu-desc 78,2574
(defun pg-pbrpm-erase-buffer-menu 80,2604
(defun pg-pbrpm-menu-change-hook 87,2788
(defun pg-pbrpm-create-reset-buffer-menu 105,3363
(defun pg-pbrpm-analyse-goal-buffer 124,4205
(defun pg-pbrpm-button-action 184,6603
(defun pg-pbrpm-exists 191,6829
(defun pg-pbrpm-eliminate-id 195,6941
(defun pg-pbrpm-build-menu 203,7187
(defun pg-pbrpm-setup-span 266,9507
(defun pg-pbrpm-run-command 326,11822
(defun pg-pbrpm-get-pos-info 356,13149
(defun pg-pbrpm-get-region-info 398,14448
(defun pg-pbrpm-auto-select-around-point 409,14860
(defun pg-pbrpm-translate-position 424,15384
(defun pg-pbrpm-process-click 432,15641
(defvar pg-pbrpm-remember-region-selected-region 452,16666
(defvar pg-pbrpm-regions-list 453,16720
(defun pg-pbrpm-erase-regions-list 455,16756
(defun pg-pbrpm-filter-regions-list 464,17064
(defface pg-pbrpm-multiple-selection-face471,17327
(defface pg-pbrpm-menu-input-face479,17529
(defun pg-pbrpm-do-remember-region 487,17719
(defun pg-pbrpm-remember-region-drag-up-hook 508,18567
(defun pg-pbrpm-remember-region-click-hook 512,18738
(defun pg-pbrpm-remember-region 517,18923
(defun pg-pbrpm-process-region 531,19637
(defun pg-pbrpm-process-regions-list 549,20366
(defun pg-pbrpm-region-expression 553,20549

generic/pg-pgip.el,2931
(defalias 'pg-pgip-debug pg-pgip-debug
38,1032
(defalias 'pg-pgip-error pg-pgip-error
39,1073
(defalias 'pg-pgip-warning pg-pgip-warning
40,1108
(defconst pg-pgip-version-supported 42,1158
(defun pg-pgip-process-packet 46,1264
(defvar pg-pgip-last-seen-id 56,1832
(defvar pg-pgip-last-seen-seq 57,1866
(defun pg-pgip-process-pgip 59,1902
(defun pg-pgip-process-msg 78,2833
(defvar pg-pgip-post-process-functions92,3403
(defun pg-pgip-post-process 102,3891
(defun pg-pgip-process-askpgip 118,4501
(defun pg-pgip-process-usespgip 124,4705
(defun pg-pgip-process-usespgml 128,4869
(defun pg-pgip-process-pgmlconfig 132,5033
(defun pg-pgip-process-proverinfo 148,5650
(defun pg-pgip-process-hasprefs 165,6315
(defun pg-pgip-haspref 179,6947
(defun pg-pgip-process-prefval 196,7649
(defun pg-pgip-process-guiconfig 223,8357
(defvar proof-assistant-idtables 230,8474
(defun pg-pgip-process-ids 233,8591
(defun pg-complete-idtable-symbol 259,9663
(defalias 'pg-pgip-process-setids pg-pgip-process-setids
264,9755
(defalias 'pg-pgip-process-addids pg-pgip-process-addids
265,9811
(defalias 'pg-pgip-process-delids pg-pgip-process-delids
266,9867
(defun pg-pgip-process-idvalue 269,9925
(defun pg-pgip-process-menuadd 281,10271
(defun pg-pgip-process-menudel 284,10314
(defun pg-pgip-process-ready 293,10546
(defun pg-pgip-process-cleardisplay 296,10587
(defun pg-pgip-process-proofstate 310,11044
(defun pg-pgip-process-normalresponse 314,11121
(defun pg-pgip-process-errorresponse 318,11251
(defun pg-pgip-process-scriptinsert 322,11380
(defun pg-pgip-process-metainforesponse 327,11514
(defun pg-pgip-file-of-url 336,11754
(defun pg-pgip-process-informfileloaded 341,11889
(defun pg-pgip-process-informfileretracted 347,12121
(defun pg-pgip-process-brokerstatus 360,12568
(defun pg-pgip-process-proveravailmsg 363,12616
(defun pg-pgip-process-newprovermsg 366,12666
(defun pg-pgip-process-proverstatusmsg 369,12714
(defvar pg-pgip-srcids 378,12960
(defun pg-pgip-process-newfile 382,13067
(defun pg-pgip-process-filestatus 398,13649
(defun pg-pgip-process-newobj 418,14303
(defun pg-pgip-process-delobj 421,14345
(defun pg-pgip-process-objectstatus 424,14387
(defun pg-pgip-process-parsescript 438,14739
(defun pg-pgip-get-pgiptype 461,15613
(defun pg-pgip-default-for 481,16405
(defun pg-pgip-subst-for 494,16800
(defun pg-pgip-interpret-value 506,17143
(defun pg-pgip-interpret-choice 524,17824
(defun pg-pgip-string-of-command 555,18841
(defconst pg-pgip-id572,19602
(defvar pg-pgip-refseq 578,19882
(defvar pg-pgip-refid 580,19979
(defvar pg-pgip-seq 583,20071
(defun pg-pgip-assemble-packet 585,20135
(defun pg-pgip-issue 603,20946
(defun pg-pgip-maybe-askpgip 620,21558
(defun pg-pgip-askprefs 626,21749
(defun pg-pgip-askids 630,21863
(defun pg-pgip-reset 643,22151
(defconst pg-pgip-start-element-regexp 674,22849
(defconst pg-pgip-end-element-regexp 675,22901

generic/pg-response.el,1291
(deflocal pg-response-eagerly-raise 32,787
(define-derived-mode proof-response-mode 42,1012
(define-key proof-response-mode-map 69,1938
(define-key proof-response-mode-map 70,2009
(define-key proof-response-mode-map 71,2063
(defun proof-response-config-done 75,2149
(defvar pg-response-special-display-regexp 86,2495
(defconst proof-multiframe-parameters90,2662
(defun proof-multiple-frames-enable 99,2961
(defun proof-three-window-enable 109,3289
(defun proof-select-three-b 112,3352
(defun proof-display-three-b 127,3821
(defvar pg-frame-configuration 139,4227
(defun pg-cache-frame-configuration 143,4374
(defun proof-layout-windows 147,4545
(defun proof-delete-other-frames 187,6332
(defvar pg-response-erase-flag 218,7420
(defun pg-response-maybe-erase222,7549
(defun pg-response-display 252,8645
(defun pg-response-display-with-face 277,9428
(defun pg-response-clear-displays 305,10274
(defun pg-response-message 317,10761
(defun pg-response-warning 323,10996
(defun proof-next-error 338,11400
(defun pg-response-has-error-location 420,14361
(defvar proof-trace-last-fontify-pos 443,15193
(defun proof-trace-fontify-pos 445,15236
(defun proof-trace-buffer-display 453,15549
(defun proof-trace-buffer-finish 478,16489
(defun pg-thms-buffer-clear 500,17056

generic/pg-thymodes.el,152
(defmacro pg-defthymode 23,499
(defmacro pg-do-unless-null 71,2310
(defun pg-symval 76,2393
(defun pg-modesym 82,2548
(defun pg-modesymval 86,2662

generic/pg-user.el,3332
(defun proof-script-new-command-advance 41,1156
(defun proof-maybe-follow-locked-end 84,2897
(defun proof-goto-command-start 111,3745
(defun proof-goto-command-end 134,4685
(defun proof-goto-point 157,5210
(defun proof-assert-next-command-interactive 171,5644
(defun proof-assert-until-point-interactive 183,6130
(defun proof-process-buffer 189,6360
(defun proof-undo-last-successful-command 204,6737
(defun proof-undo-and-delete-last-successful-command 209,6899
(defun proof-undo-last-successful-command-1 222,7453
(defun proof-retract-buffer 239,8065
(defun proof-retract-current-goal 248,8349
(defun proof-mouse-goto-point 267,8869
(defvar proof-minibuffer-history 282,9145
(defun proof-minibuffer-cmd 285,9240
(defun proof-frob-locked-end 329,10862
(defmacro proof-if-setting-configured 390,12786
(defmacro proof-define-assistant-command 398,13055
(defmacro proof-define-assistant-command-witharg 411,13510
(defun proof-issue-new-command 431,14332
(defun proof-cd-sync 477,15829
(defun proof-electric-terminator-enable 531,17549
(defun proof-electric-terminator 539,17839
(defun proof-add-completions 561,18484
(defun proof-script-complete 586,19391
(defun pg-copy-span-contents 600,19700
(defun pg-numth-span-higher-or-lower 617,20258
(defun pg-control-span-of 643,21004
(defun pg-move-span-contents 649,21208
(defun pg-fixup-children-spans 701,23384
(defun pg-move-region-down 711,23641
(defun pg-move-region-up 720,23934
(defun proof-forward-command 750,24762
(defun proof-backward-command 771,25483
(defun pg-pos-for-event 793,25827
(defun pg-span-for-event 799,26048
(defun pg-span-context-menu 803,26192
(defun pg-toggle-visibility 818,26647
(defun pg-create-in-span-context-menu 828,26969
(defun pg-span-undo 858,28178
(defun pg-goals-buffers-hint 904,29580
(defun pg-slow-fontify-tracing-hint 908,29762
(defun pg-response-buffers-hint 912,29933
(defun pg-jump-to-end-hint 922,30295
(defun pg-processing-complete-hint 926,30424
(defun pg-next-error-hint 943,31123
(defun pg-hint 948,31275
(defun pg-identifier-under-mouse-query 964,31865
(defun pg-identifier-near-point-query 973,32108
(defvar proof-query-identifier-collection 1000,32951
(defvar proof-query-identifier-history 1001,32998
(defun proof-query-identifier 1003,33043
(defun pg-identifier-query 1013,33312
(defun proof-imenu-enable 1044,34390
(defvar pg-input-ring 1080,35712
(defvar pg-input-ring-index 1083,35769
(defvar pg-stored-incomplete-input 1086,35841
(defun pg-previous-input 1089,35944
(defun pg-next-input 1103,36401
(defun pg-delete-input 1108,36523
(defun pg-get-old-input 1121,36861
(defun pg-restore-input 1135,37252
(defun pg-search-start 1146,37542
(defun pg-regexp-arg 1158,38034
(defun pg-search-arg 1170,38482
(defun pg-previous-matching-input-string-position 1184,38899
(defun pg-previous-matching-input 1211,40064
(defun pg-next-matching-input 1230,40914
(defvar pg-matching-input-from-input-string 1238,41297
(defun pg-previous-matching-input-from-input 1242,41411
(defun pg-next-matching-input-from-input 1260,42176
(defun pg-add-to-input-history 1271,42555
(defun pg-remove-from-input-history 1283,43008
(defun  pg-clear-input-ring 1294,43388
(define-key proof-mode-map 1308,43738
(define-key proof-mode-map 1309,43798
(defun pg-protected-undo 1311,43870

generic/pg-vars.el,1452
(defvar proof-assistant-cusgrp 22,382
(defvar proof-assistant-internals-cusgrp 28,642
(defvar proof-assistant 34,912
(defvar proof-assistant-symbol 39,1133
(defvar proof-mode-for-shell 52,1675
(defvar proof-mode-for-response 57,1865
(defvar proof-mode-for-goals 62,2091
(defvar proof-mode-for-script 67,2280
(defvar proof-ready-for-assistant-hook 72,2457
(defvar proof-shell-busy 83,2745
(defvar proof-included-files-list 88,2901
(defvar proof-script-buffer 110,3914
(defvar proof-previous-script-buffer 113,4006
(defvar proof-shell-buffer 117,4177
(defvar proof-goals-buffer 120,4263
(defvar proof-response-buffer 123,4318
(defvar proof-trace-buffer 126,4379
(defvar proof-thms-buffer 130,4533
(defvar proof-shell-error-or-interrupt-seen 134,4688
(defvar proof-shell-interrupt-pending 139,4912
(defvar pg-response-next-error 143,5078
(defvar proof-shell-proof-completed 146,5185
(defvar proof-terminal-string 158,5729
(defvar proof-shell-silent 170,5987
(defvar proof-shell-last-prompt 173,6075
(defvar proof-shell-last-output 177,6245
(defvar proof-shell-last-output-kind 181,6385
(defvar proof-assistant-settings 201,7149
(defvar pg-tracing-slow-mode 209,7597
(defvar proof-nesting-depth 212,7686
(defvar proof-last-theorem-dependencies 219,7921
(defcustom proof-general-name 228,8157
(defcustom proof-general-home-page233,8314
(defcustom proof-unnamed-theorem-name239,8474
(defcustom proof-universal-keys245,8658

generic/pg-xml.el,1177
(defalias 'pg-xml-error pg-xml-error
18,381
(defun pg-xml-parse-string 41,1023
(defun pg-xml-parse-buffer 52,1349
(defun pg-xml-get-attr 71,1964
(defun pg-xml-child-elts 79,2266
(defun pg-xml-child-elt 84,2471
(defun pg-xml-get-child 92,2753
(defun pg-xml-get-text-content 102,3120
(defmacro pg-xml-attr 113,3470
(defmacro pg-xml-node 115,3532
(defconst pg-xml-header118,3624
(defun pg-xml-string-of 122,3700
(defun pg-xml-output-internal 133,4067
(defun pg-xml-cdata 167,5206
(defsubst pg-pgip-get-area 175,5399
(defun pg-pgip-get-icon 178,5516
(defsubst pg-pgip-get-name 182,5664
(defsubst pg-pgip-get-version 185,5781
(defsubst pg-pgip-get-descr 188,5904
(defsubst pg-pgip-get-thmname 191,6023
(defsubst pg-pgip-get-thyname 194,6146
(defsubst pg-pgip-get-url 197,6269
(defsubst pg-pgip-get-srcid 200,6384
(defsubst pg-pgip-get-proverid 203,6503
(defsubst pg-pgip-get-symname 206,6628
(defsubst pg-pgip-get-prefcat 209,6748
(defsubst pg-pgip-get-default 212,6876
(defsubst pg-pgip-get-objtype 215,6999
(defsubst pg-pgip-get-value 218,7122
(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext
221,7192
(defun pg-pgip-get-pgmltext 223,7251

generic/proof-autoloads.el,45
(defsubst proof-shell-live-buffer 639,21040

generic/proof-auxmodes.el,149
(defun proof-mmm-support-available 20,489
(defun proof-maths-menu-support-available 44,1100
(defun proof-unicode-tokens-support-available 58,1517

generic/proof-config.el,7905
(defgroup prover-config 80,2633
(defcustom proof-guess-command-line 98,3483
(defcustom proof-assistant-home-page 113,3978
(defcustom proof-context-command 119,4148
(defcustom proof-info-command 124,4282
(defcustom proof-showproof-command 131,4553
(defcustom proof-goal-command 136,4689
(defcustom proof-save-command 144,4986
(defcustom proof-find-theorems-command 152,5295
(defcustom proof-query-identifier-command 159,5603
(defcustom proof-assistant-true-value 173,6292
(defcustom proof-assistant-false-value 179,6482
(defcustom proof-assistant-format-int-fn 185,6676
(defcustom proof-assistant-format-string-fn 192,6925
(defcustom proof-assistant-setting-format 199,7192
(defgroup proof-script 221,7887
(defcustom proof-terminal-char 226,8017
(defcustom proof-electric-terminator-noterminator 236,8404
(defcustom proof-script-sexp-commands 241,8576
(defcustom proof-script-command-end-regexp 252,9033
(defcustom proof-script-command-start-regexp 270,9852
(defcustom proof-script-use-old-parser 281,10313
(defcustom proof-script-integral-proofs 293,10799
(defcustom proof-script-fly-past-comments 308,11455
(defcustom proof-script-parse-function 313,11626
(defcustom proof-script-comment-start 331,12269
(defcustom proof-script-comment-start-regexp 342,12706
(defcustom proof-script-comment-end 350,13025
(defcustom proof-script-comment-end-regexp 362,13447
(defcustom proof-string-start-regexp 370,13758
(defcustom proof-string-end-regexp 375,13923
(defcustom proof-case-fold-search 380,14084
(defcustom proof-save-command-regexp 389,14496
(defcustom proof-save-with-hole-regexp 394,14606
(defcustom proof-save-with-hole-result 406,15060
(defcustom proof-goal-command-regexp 416,15510
(defcustom proof-goal-with-hole-regexp 425,15898
(defcustom proof-goal-with-hole-result 437,16341
(defcustom proof-non-undoables-regexp 446,16725
(defcustom proof-nested-undo-regexp 457,17180
(defcustom proof-ignore-for-undo-count 473,17892
(defcustom proof-script-next-entity-regexps 481,18195
(defcustom proof-script-find-next-entity-fn525,19936
(defcustom proof-script-imenu-generic-expression 545,20776
(defcustom proof-goal-command-p 553,21115
(defcustom proof-really-save-command-p 564,21606
(defcustom proof-completed-proof-behaviour 573,21913
(defcustom proof-count-undos-fn 601,23262
(defcustom proof-find-and-forget-fn 613,23811
(defcustom proof-forget-id-command 630,24514
(defcustom pg-topterm-goalhyplit-fn 640,24872
(defcustom proof-kill-goal-command 652,25407
(defcustom proof-undo-n-times-cmd 666,25911
(defcustom proof-nested-goals-history-p 680,26448
(defcustom proof-arbitrary-undo-positions 689,26785
(defcustom proof-state-preserving-p 703,27365
(defcustom proof-activate-scripting-hook 713,27837
(defcustom proof-deactivate-scripting-hook 732,28618
(defcustom proof-script-evaluate-elisp-comment-regexp 741,28948
(defcustom proof-indent 759,29534
(defcustom proof-indent-hang 764,29641
(defcustom proof-indent-enclose-offset 769,29767
(defcustom proof-indent-open-offset 774,29909
(defcustom proof-indent-close-offset 779,30046
(defcustom proof-indent-any-regexp 784,30184
(defcustom proof-indent-inner-regexp 789,30344
(defcustom proof-indent-enclose-regexp 794,30498
(defcustom proof-indent-open-regexp 799,30652
(defcustom proof-indent-close-regexp 804,30804
(defcustom proof-script-font-lock-keywords 810,30958
(defcustom proof-script-syntax-table-entries 818,31310
(defcustom proof-script-span-context-menu-extensions 836,31706
(defgroup proof-shell 862,32464
(defcustom proof-prog-name 872,32634
(defcustom proof-shell-auto-terminate-commands 883,33054
(defcustom proof-shell-pre-sync-init-cmd 892,33455
(defcustom proof-shell-init-cmd 906,34013
(defcustom proof-shell-init-hook 918,34542
(defcustom proof-shell-restart-cmd 923,34681
(defcustom proof-shell-quit-cmd 928,34836
(defcustom proof-shell-quit-timeout 933,35003
(defcustom proof-shell-cd-cmd 943,35453
(defcustom proof-shell-start-silent-cmd 960,36124
(defcustom proof-shell-stop-silent-cmd 969,36500
(defcustom proof-shell-silent-threshold 978,36835
(defcustom  proof-shell-inform-file-processed-cmd 986,37169
(defcustom  proof-shell-inform-file-retracted-cmd 1007,38097
(defcustom proof-auto-multiple-files 1035,39369
(defcustom proof-cannot-reopen-processed-files 1050,40090
(defcustom proof-shell-require-command-regexp 1064,40756
(defcustom proof-done-advancing-require-function 1075,41218
(defcustom proof-shell-annotated-prompt-regexp 1087,41578
(defcustom proof-shell-error-regexp 1102,42143
(defcustom proof-shell-truncate-before-error 1122,42945
(defcustom pg-next-error-regexp 1136,43484
(defcustom pg-next-error-filename-regexp 1151,44093
(defcustom pg-next-error-extract-filename 1175,45126
(defcustom proof-shell-interrupt-regexp 1182,45369
(defcustom proof-shell-proof-completed-regexp 1196,45964
(defcustom proof-shell-clear-response-regexp 1209,46472
(defcustom proof-shell-clear-goals-regexp 1221,46924
(defcustom proof-shell-start-goals-regexp 1233,47370
(defcustom proof-shell-end-goals-regexp 1241,47737
(defcustom proof-shell-eager-annotation-start 1255,48312
(defcustom proof-shell-eager-annotation-start-length 1278,49331
(defcustom proof-shell-eager-annotation-end 1289,49757
(defcustom proof-shell-strip-output-markup 1305,50432
(defcustom proof-shell-assumption-regexp 1314,50817
(defcustom proof-shell-process-file 1324,51221
(defcustom proof-shell-retract-files-regexp 1350,52299
(defcustom proof-shell-compute-new-files-list 1363,52787
(defcustom pg-special-char-regexp 1378,53356
(defcustom proof-shell-set-elisp-variable-regexp 1383,53500
(defcustom proof-shell-match-pgip-cmd 1421,55166
(defcustom proof-shell-issue-pgip-cmd 1435,55648
(defcustom proof-use-pgip-askprefs 1440,55813
(defcustom proof-shell-query-dependencies-cmd 1448,56160
(defcustom proof-shell-theorem-dependency-list-regexp 1455,56420
(defcustom proof-shell-theorem-dependency-list-split 1471,57080
(defcustom proof-shell-show-dependency-cmd 1480,57503
(defcustom proof-shell-trace-output-regexp 1502,58409
(defcustom proof-shell-thms-output-regexp 1520,59004
(defcustom proof-tokens-activate-command 1533,59387
(defcustom proof-tokens-deactivate-command 1540,59627
(defcustom proof-tokens-extra-modes 1547,59872
(defcustom proof-shell-unicode 1562,60377
(defcustom proof-shell-filename-escapes 1571,60767
(defcustom proof-shell-process-connection-type1588,61447
(defcustom proof-shell-strip-crs-from-input 1611,62451
(defcustom proof-shell-strip-crs-from-output 1623,62934
(defcustom proof-shell-insert-hook 1631,63302
(defcustom proof-script-preprocess 1672,65262
(defcustom proof-shell-handle-delayed-output-hook1678,65413
(defcustom proof-shell-handle-error-or-interrupt-hook1684,65628
(defcustom proof-shell-pre-interrupt-hook1702,66374
(defcustom proof-shell-handle-output-system-specific 1710,66645
(defcustom proof-state-change-hook 1733,67621
(defcustom proof-shell-syntax-table-entries 1743,68014
(defgroup proof-goals 1761,68385
(defcustom pg-subterm-first-special-char 1766,68506
(defcustom pg-subterm-anns-use-stack 1774,68818
(defcustom pg-goals-change-goal 1783,69117
(defcustom pbp-goal-command 1788,69233
(defcustom pbp-hyp-command 1793,69389
(defcustom pg-subterm-help-cmd 1798,69551
(defcustom pg-goals-error-regexp 1805,69787
(defcustom proof-shell-result-start 1810,69947
(defcustom proof-shell-result-end 1816,70181
(defcustom pg-subterm-start-char 1822,70394
(defcustom pg-subterm-sep-char 1836,70979
(defcustom pg-subterm-end-char 1842,71158
(defcustom pg-topterm-regexp 1848,71315
(defcustom proof-goals-font-lock-keywords 1863,71915
(defcustom proof-response-font-lock-keywords 1871,72274
(defcustom proof-shell-font-lock-keywords 1879,72636
(defcustom pg-before-fontify-output-hook 1890,73151
(defcustom pg-after-fontify-output-hook 1898,73512

generic/proof-depends.el,824
(defvar proof-thm-names-of-files 23,622
(defvar proof-def-names-of-files 29,906
(defun proof-depends-module-name-for-buffer 38,1210
(defun proof-depends-module-of 48,1651
(defun proof-depends-names-in-same-file 56,1944
(defun proof-depends-process-dependencies 75,2552
(defun proof-dependency-in-span-context-menu 128,4287
(defun proof-dep-alldeps-menu 151,5189
(defun proof-dep-make-alldeps-menu 157,5415
(defun proof-dep-split-deps 175,5910
(defun proof-dep-make-submenu 194,6576
(defun proof-make-highlight-depts-menu 204,6926
(defun proof-goto-dependency 214,7229
(defun proof-show-dependency 220,7452
(defconst pg-dep-span-priority 227,7741
(defconst pg-ordinary-span-priority 228,7777
(defun proof-highlight-depcs 230,7819
(defun proof-highlight-depts 240,8249
(defun proof-dep-unhighlight 251,8723

generic/proof-easy-config.el,192
(defconst proof-easy-config-derived-modes-table16,544
(defun proof-easy-config-define-derived-modes 23,950
(defun proof-easy-config-check-setup 52,2135
(defmacro proof-easy-config 84,3465

generic/proof-faces.el,1431
(defgroup proof-faces 29,810
(defconst pg-defface-window-systems36,990
(defmacro proof-face-specs 49,1552
(defface proof-queue-face64,2004
(defface proof-locked-face72,2282
(defface proof-declaration-name-face82,2603
(defface proof-tacticals-name-face91,2889
(defface proof-tactics-name-face100,3151
(defface proof-error-face109,3416
(defface proof-warning-face117,3606
(defface proof-eager-annotation-face126,3863
(defface proof-debug-message-face134,4081
(defface proof-boring-face142,4280
(defface proof-mouse-highlight-face150,4472
(defface proof-highlight-dependent-face158,4668
(defface proof-highlight-dependency-face166,4875
(defface proof-active-area-face174,5072
(defface proof-script-error-face182,5384
(defconst proof-face-compat-doc 191,5653
(defconst proof-queue-face 192,5733
(defconst proof-locked-face 193,5801
(defconst proof-declaration-name-face 194,5871
(defconst proof-tacticals-name-face 195,5961
(defconst proof-tactics-name-face 196,6047
(defconst proof-error-face 197,6129
(defconst proof-warning-face 198,6197
(defconst proof-eager-annotation-face 199,6269
(defconst proof-debug-message-face 200,6359
(defconst proof-boring-face 201,6443
(defconst proof-mouse-highlight-face 202,6513
(defconst proof-highlight-dependent-face 203,6601
(defconst proof-highlight-dependency-face 204,6697
(defconst proof-active-area-face 205,6795
(defconst proof-script-error-face 206,6875

generic/proof-indent.el,219
(defun proof-indent-indent 14,412
(defun proof-indent-offset 23,678
(defun proof-indent-inner-p 40,1278
(defun proof-indent-goto-prev 49,1578
(defun proof-indent-calculate 56,1911
(defun proof-indent-line 76,2611

generic/proof-maths-menu.el,83
(defun proof-maths-menu-set-global 30,942
(defun proof-maths-menu-enable 44,1393

generic/proof-menu.el,2026
(defvar proof-display-some-buffers-count 35,801
(defun proof-display-some-buffers 37,846
(defun proof-menu-define-keys 94,2986
(defun proof-menu-define-main 153,5852
(defvar proof-menu-favourites 162,6037
(defvar proof-menu-settings 165,6144
(defun proof-menu-define-specific 169,6233
(defun proof-assistant-menu-update 212,7494
(defvar proof-help-menu226,7927
(defvar proof-show-hide-menu234,8197
(defvar proof-buffer-menu243,8510
(defun proof-keep-response-history 305,10779
(defconst proof-quick-opts-menu313,11089
(defun proof-quick-opts-vars 500,18727
(defun proof-quick-opts-changed-from-defaults-p 529,19587
(defun proof-quick-opts-changed-from-saved-p 533,19692
(defun proof-quick-opts-save 544,20043
(defun proof-quick-opts-reset 549,20211
(defconst proof-config-menu561,20479
(defconst proof-advanced-menu568,20658
(defvar proof-menu581,21090
(defun proof-main-menu 590,21372
(defun proof-aux-menu 602,21711
(defun proof-menu-define-favourites-menu 618,22057
(defun proof-def-favourite 638,22706
(defvar proof-make-favourite-cmd-history 661,23680
(defvar proof-make-favourite-menu-history 664,23765
(defun proof-save-favourites 667,23851
(defun proof-del-favourite 672,23999
(defun proof-read-favourite 689,24555
(defun proof-add-favourite 713,25331
(defun proof-menu-define-settings-menu 740,26376
(defun proof-menu-entry-name 773,27497
(defun proof-menu-entry-for-setting 783,27847
(defun proof-settings-vars 802,28379
(defun proof-settings-changed-from-defaults-p 807,28556
(defun proof-settings-changed-from-saved-p 811,28662
(defun proof-settings-save 815,28765
(defun proof-settings-reset 820,28932
(defun proof-assistant-invisible-command-ifposs 825,29095
(defun proof-maybe-askprefs 847,30065
(defun proof-assistant-settings-cmd 853,30257
(defvar proof-assistant-format-table870,30912
(defun proof-assistant-format-bool 878,31280
(defun proof-assistant-format-int 881,31393
(defun proof-assistant-format-string 884,31485
(defun proof-assistant-format 887,31583

generic/proof-mmm.el,70
(defun proof-mmm-set-global 39,1466
(defun proof-mmm-enable 54,2005

generic/proof-script.el,5559
(deflocal proof-active-buffer-fake-minor-mode 44,1308
(deflocal proof-script-buffer-file-name 47,1434
(deflocal pg-script-portions 54,1844
(defun proof-next-element-count 64,2064
(defun proof-element-id 70,2306
(defun proof-next-element-id 74,2475
(deflocal proof-locked-span 109,3729
(deflocal proof-queue-span 116,3995
(deflocal proof-overlay-arrow 125,4481
(defun proof-span-give-warning 131,4608
(defun proof-span-read-only 137,4788
(defun proof-strict-read-only 146,5161
(defsubst proof-set-queue-endpoints 156,5539
(defun proof-set-overlay-arrow 160,5680
(defsubst proof-set-locked-endpoints 171,6018
(defsubst proof-detach-queue 176,6194
(defsubst proof-detach-locked 181,6333
(defsubst proof-set-queue-start 188,6558
(defsubst proof-set-locked-end 192,6684
(defsubst proof-set-queue-end 204,7154
(defun proof-init-segmentation 215,7451
(defun proof-colour-locked 248,8913
(defun proof-restart-buffers 259,9345
(defun proof-script-buffers-with-spans 281,10164
(defun proof-script-remove-all-spans-and-deactivate 291,10520
(defun proof-script-clear-queue-spans-on-error 295,10710
(defun proof-script-delete-spans 316,11511
(defun proof-script-delete-secondary-spans 321,11710
(defun proof-unprocessed-begin 333,11998
(defun proof-script-end 341,12252
(defun proof-queue-or-locked-end 350,12555
(defun proof-locked-end 365,13233
(defun proof-locked-region-full-p 379,13514
(defun proof-locked-region-empty-p 388,13786
(defun proof-only-whitespace-to-locked-region-p 392,13936
(defun proof-in-locked-region-p 402,14263
(defun proof-goto-end-of-locked 414,14520
(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 431,15279
(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 442,15760
(defun proof-end-of-locked-visible-p 456,16373
(defvar pg-idioms 474,16991
(defvar pg-visibility-specs 477,17087
(defconst pg-default-invisibility-spec484,17345
(defun pg-clear-script-portions 487,17414
(defun pg-remove-script-element 494,17688
(defsubst pg-visname 499,17877
(defun pg-add-element 503,18022
(defun pg-open-invisible-span 539,19712
(defun pg-remove-element 550,20075
(defun pg-make-element-invisible 556,20315
(defun pg-make-element-visible 562,20559
(defun pg-toggle-element-visibility 568,20810
(defun pg-show-all-portions 574,21067
(defun pg-show-all-proofs 595,21843
(defun pg-hide-all-proofs 600,21971
(defun pg-add-proof-element 605,22102
(defun pg-span-name 620,22829
(defvar pg-span-context-menu-keymap641,23529
(defun pg-last-output-displayform 648,23767
(defun pg-set-span-helphighlights 666,24463
(defun pg-delete-self-modification-hook 707,26163
(defun proof-complete-buffer-atomic 718,26436
(defun proof-register-possibly-new-processed-file760,28356
(defun proof-inform-prover-file-retracted 806,30193
(defun proof-auto-retract-dependencies 826,31044
(defun proof-unregister-buffer-file-name 880,33594
(defun proof-protected-process-or-retract 926,35419
(defun proof-deactivate-scripting-auto 953,36589
(defun proof-deactivate-scripting 962,36947
(defun proof-activate-scripting 1095,42203
(defun proof-toggle-active-scripting 1210,47321
(defun proof-done-advancing 1249,48566
(defun proof-done-advancing-comment 1328,51551
(defun proof-done-advancing-save 1362,52927
(defun proof-make-goalsave 1450,56292
(defun proof-get-name-from-goal 1468,57124
(defun proof-done-advancing-autosave 1488,58149
(defun proof-done-advancing-other 1553,60693
(defun proof-segment-up-to-parser 1581,61646
(defun proof-script-generic-parse-find-comment-end 1651,63921
(defun proof-script-generic-parse-cmdend 1660,64335
(defun proof-script-generic-parse-cmdstart 1685,65222
(defun proof-script-generic-parse-sexp 1748,67915
(defun proof-cmdstart-add-segment-for-cmd 1772,68847
(defun proof-segment-up-to-cmdstart 1823,70905
(defun proof-segment-up-to-cmdend 1884,73265
(defun proof-semis-to-vanillas 1956,75944
(defun proof-script-next-command-advance 2005,77466
(defun proof-assert-until-point 2024,77965
(defun proof-assert-electric-terminator 2039,78558
(defun proof-assert-semis 2073,79900
(defun proof-retract-before-change 2086,80539
(defun proof-inside-comment 2095,80857
(defun proof-insert-pbp-command 2110,81140
(defun proof-insert-sendback-command 2125,81634
(defun proof-done-retracting 2151,82537
(defun proof-setup-retract-action 2186,83978
(defun proof-last-goal-or-goalsave 2196,84464
(defun proof-retract-target 2220,85369
(defun proof-retract-until-point-interactive 2303,88883
(defun proof-retract-until-point 2311,89268
(define-derived-mode proof-mode 2358,91103
(defun proof-script-set-visited-file-name 2395,92471
(defun proof-script-set-buffer-hooks 2417,93484
(defun proof-script-kill-buffer-fn 2425,93902
(defun proof-config-done-related 2457,95219
(defun proof-generic-goal-command-p 2525,97742
(defun proof-generic-state-preserving-p 2530,97955
(defun proof-generic-count-undos 2539,98472
(defun proof-generic-find-and-forget 2568,99510
(defconst proof-script-important-settings2621,101349
(defun proof-config-done 2636,101895
(defun proof-setup-parsing-mechanism 2704,104173
(defun proof-setup-imenu 2748,106026
(deflocal proof-segment-up-to-cache 2772,106800
(deflocal proof-segment-up-to-cache-start 2773,106841
(deflocal proof-last-edited-low-watermark 2774,106886
(defun proof-segment-up-to-using-cache 2784,107373
(defun proof-segment-cache-contents-for 2813,108521
(defun proof-script-after-change-function 2825,108890
(defun proof-script-set-after-change-functions 2837,109397

generic/proof-shell.el,3793
(defvar proof-marker 35,808
(defvar proof-action-list 38,904
(defvar proof-shell-last-goals-output 63,1832
(defvar proof-shell-last-response-output 66,1912
(defvar proof-shell-delayed-output-start 69,1999
(defvar proof-shell-delayed-output-end 73,2181
(defvar proof-shell-delayed-output-flags 77,2361
(defcustom proof-shell-active-scripting-indicator86,2557
(defun proof-shell-ready-prover 134,3909
(defsubst proof-shell-live-buffer 148,4448
(defun proof-shell-available-p 155,4687
(defun proof-grab-lock 161,4909
(defun proof-release-lock 172,5407
(defcustom proof-shell-fiddle-frames 184,5627
(defun proof-shell-set-text-representation 190,5849
(defun proof-shell-start 201,6310
(defvar proof-shell-kill-function-hooks 387,12598
(defun proof-shell-kill-function 390,12696
(defun proof-shell-clear-state 479,16500
(defun proof-shell-exit 494,16943
(defun proof-shell-bail-out 506,17388
(defun proof-shell-restart 515,17865
(defvar proof-shell-urgent-message-marker 557,19243
(defvar proof-shell-urgent-message-scanner 560,19364
(defun proof-shell-handle-error-output 563,19490
(defun proof-shell-handle-error-or-interrupt 589,20352
(defun proof-shell-error-or-interrupt-action 624,21773
(defun proof-goals-pos 638,22301
(defun proof-pbp-focus-on-first-goal 643,22512
(defsubst proof-shell-string-match-safe 655,22928
(defun proof-shell-handle-immediate-output 659,23089
(defvar proof-shell-expecting-output 726,25671
(defvar proof-shell-interrupt-pending 730,25830
(defun proof-interrupt-process 735,26054
(defun proof-shell-insert 773,27487
(defun proof-shell-action-list-item 826,29355
(defun proof-shell-set-silent 831,29606
(defun proof-shell-start-silent-item 837,29825
(defun proof-shell-clear-silent 843,30014
(defun proof-shell-stop-silent-item 849,30236
(defsubst proof-shell-should-be-silent 855,30425
(defsubst proof-shell-invoke-callback 866,30935
(defsubst proof-shell-insert-action-item 872,31145
(defsubst proof-shell-slurp-comments 876,31320
(defun proof-add-to-queue 887,31726
(defun proof-start-queue 945,33751
(defun proof-extend-queue 956,34115
(defun proof-shell-exec-loop 964,34496
(defun proof-shell-insert-loopback-cmd 1032,36800
(defun proof-shell-process-urgent-message 1057,37946
(defun proof-shell-process-urgent-message-default 1106,39667
(defun proof-shell-process-urgent-message-trace 1122,40254
(defun proof-shell-process-urgent-message-retract 1135,40814
(defun proof-shell-process-urgent-message-elisp 1156,41662
(defun proof-shell-process-urgent-message-thmdeps 1171,42157
(defun proof-shell-strip-eager-annotations 1185,42537
(defvar proof-shell-minibuffer-urgent-interactive-input-history 1200,43070
(defun proof-shell-minibuffer-urgent-interactive-input 1202,43140
(defun proof-shell-filter 1218,43614
(defun proof-shell-filter-first-command 1319,47023
(defun proof-shell-process-urgent-messages 1334,47566
(defun proof-shell-filter-manage-output 1398,49866
(defsubst proof-shell-display-output-as-response 1431,51169
(defun proof-shell-handle-delayed-output 1437,51461
(defvar pg-last-tracing-output-time 1532,54926
(defconst pg-slow-mode-duration 1535,55032
(defconst pg-fast-tracing-mode-threshold 1538,55114
(defvar pg-tracing-cleanup-timer 1541,55242
(defun pg-tracing-tight-loop 1543,55281
(defun pg-finish-tracing-display 1586,56993
(defun proof-shell-wait 1604,57357
(defun proof-done-invisible 1623,58265
(defun proof-shell-invisible-command 1629,58435
(defun proof-shell-invisible-cmd-get-result 1676,59979
(defun proof-shell-invisible-command-invisible-result 1688,60415
(defun pg-insert-last-output-as-comment 1708,60916
(define-derived-mode proof-shell-mode 1727,61388
(defconst proof-shell-important-settings1764,62419
(defun proof-shell-config-done 1770,62534

generic/proof-site.el,503
(defconst proof-assistant-table-default22,725
(defconst proof-general-short-version60,2122
(defconst proof-general-version-year 66,2309
(defgroup proof-general 73,2462
(defgroup proof-general-internals 78,2570
(defun proof-home-directory-fn 91,2958
(defcustom proof-home-directory102,3328
(defcustom proof-images-directory111,3694
(defcustom proof-info-directory117,3896
(defcustom proof-assistant-table144,4871
(defcustom proof-assistants 179,5984
(defun proof-ready-for-assistant 208,7140

generic/proof-splash.el,800
(defcustom proof-splash-enable 17,324
(defcustom proof-splash-time 22,476
(defcustom proof-splash-contents30,760
(defconst proof-splash-startup-msg70,2134
(defconst proof-splash-welcome 79,2512
(defsubst proof-emacs-imagep 86,2687
(defun proof-get-image 91,2812
(defvar proof-splash-timeout-conf 113,3612
(defun proof-splash-centre-spaces 116,3698
(defun proof-splash-remove-screen 131,4321
(defvar proof-splash-seen 147,4846
(defun proof-splash-insert-contents 150,4948
(defun proof-splash-display-screen 189,6142
(defalias 'pg-about pg-about
217,7225
(defun proof-splash-message 220,7291
(defun proof-splash-timeout-waiter 234,7732
(defvar proof-splash-old-frame-title-format 243,8116
(defun proof-splash-set-frame-titles 245,8166
(defun proof-splash-unset-frame-titles 254,8481

generic/proof-syntax.el,1045
(defsubst proof-ids-to-regexp 17,446
(defsubst proof-anchor-regexp 21,619
(defconst proof-no-regexp 25,724
(defsubst proof-regexp-alt 28,815
(defsubst proof-re-search-forward-region 37,1124
(defsubst proof-search-forward 50,1622
(defsubst proof-replace-regexp-in-string 56,1877
(defsubst proof-re-search-forward 61,2128
(defsubst proof-re-search-backward 66,2386
(defsubst proof-re-search-forward-safe 71,2647
(defsubst proof-string-match 77,2928
(defsubst proof-string-match-safe 82,3157
(defsubst proof-stringfn-match 86,3361
(defsubst proof-looking-at 93,3624
(defsubst proof-looking-at-safe 98,3811
(defsubst proof-looking-at-syntactic-context-default 102,3956
(defsubst proof-replace-string 113,4333
(defsubst proof-replace-regexp 118,4537
(defsubst proof-replace-regexp-nocasefold 123,4746
(defvar proof-id 131,5028
(defsubst proof-ids 137,5248
(defun proof-zap-commas 151,5740
(defun proof-format 167,6236
(defun proof-format-filename 186,6875
(defun proof-insert 233,8277
(defun proof-splice-separator 270,9294

generic/proof-toolbar.el,2332
(defun proof-toolbar-function 33,809
(defun proof-toolbar-icon 36,906
(defun proof-toolbar-enabler 39,1007
(defun proof-toolbar-make-icon 46,1159
(defun proof-toolbar-make-toolbar-items 55,1467
(defvar proof-toolbar-map 80,2272
(defun proof-toolbar-available-p 83,2371
(defun proof-toolbar-setup 92,2647
(defun proof-toolbar-enable 113,3504
(defalias 'proof-toolbar-undo proof-toolbar-undo
146,4554
(defun proof-toolbar-undo-enable-p 148,4622
(defalias 'proof-toolbar-delete proof-toolbar-delete
155,4780
(defun proof-toolbar-delete-enable-p 157,4861
(defalias 'proof-toolbar-home proof-toolbar-home
165,5043
(defalias 'proof-toolbar-next proof-toolbar-next
169,5110
(defun proof-toolbar-next-enable-p 171,5181
(defalias 'proof-toolbar-goto proof-toolbar-goto
177,5297
(defun proof-toolbar-goto-enable-p 179,5347
(defalias 'proof-toolbar-retract proof-toolbar-retract
184,5432
(defun proof-toolbar-retract-enable-p 186,5489
(defalias 'proof-toolbar-use proof-toolbar-use
192,5608
(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p
193,5660
(defalias 'proof-toolbar-restart proof-toolbar-restart
197,5741
(defalias 'proof-toolbar-goal proof-toolbar-goal
201,5806
(defalias 'proof-toolbar-qed proof-toolbar-qed
205,5864
(defun proof-toolbar-qed-enable-p 207,5913
(defalias 'proof-toolbar-state proof-toolbar-state
215,6075
(defalias 'proof-toolbar-state-enable-p proof-toolbar-state-enable-p
216,6118
(defalias 'proof-toolbar-context proof-toolbar-context
220,6197
(defalias 'proof-toolbar-context-enable-p proof-toolbar-context-enable-p
221,6243
(defalias 'proof-toolbar-command proof-toolbar-command
225,6324
(defalias 'proof-toolbar-command-enable-p proof-toolbar-command-enable-p
226,6380
(defun proof-toolbar-help 230,6485
(defalias 'proof-toolbar-find proof-toolbar-find
236,6565
(defalias 'proof-toolbar-find-enable-p proof-toolbar-find-enable-p
237,6617
(defalias 'proof-toolbar-info proof-toolbar-info
241,6692
(defalias 'proof-toolbar-info-enable-p proof-toolbar-info-enable-p
242,6747
(defalias 'proof-toolbar-visibility proof-toolbar-visibility
246,6845
(defun proof-toolbar-visibility-enable-p 248,6905
(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt
253,7019
(defun proof-toolbar-interrupt-enable-p 254,7080
(defun proof-toolbar-scripting-menu 262,7233

generic/proof-unicode-tokens.el,497
(defvar proof-unicode-tokens-initialised 31,827
(defun proof-unicode-tokens-init 34,934
(defun proof-unicode-tokens-configure 48,1436
(defun proof-unicode-tokens-mode-if-enabled 60,1882
(defun proof-unicode-tokens-set-global 66,2081
(defun proof-unicode-tokens-enable 82,2651
(defun proof-unicode-tokens-reconfigure 102,3504
(defun proof-unicode-tokens-configure-prover 128,4392
(defun proof-unicode-tokens-activate-prover 133,4573
(defun proof-unicode-tokens-deactivate-prover 140,4819

generic/proof-useropts.el,1510
(defgroup proof-user-options 21,553
(defun proof-set-value 29,732
(defcustom proof-electric-terminator-enable 62,1855
(defcustom proof-toolbar-enable 74,2387
(defcustom proof-imenu-enable 80,2560
(defcustom pg-show-hints 86,2731
(defcustom proof-shell-quiet-errors 91,2864
(defcustom proof-trace-output-slow-catchup 98,3135
(defcustom proof-strict-state-preserving 108,3632
(defcustom proof-strict-read-only 121,4241
(defcustom proof-allow-undo-in-read-only 134,4820
(defcustom proof-three-window-enable 141,5102
(defcustom proof-multiple-frames-enable 160,5852
(defcustom proof-delete-empty-windows 169,6185
(defcustom proof-shrink-windows-tofit 180,6716
(defcustom proof-auto-raise-buffers 187,6988
(defcustom proof-colour-locked 194,7223
(defcustom proof-query-file-save-when-activating-scripting202,7473
(defcustom proof-one-command-per-line218,8193
(defcustom proof-prog-name-ask225,8417
(defcustom proof-prog-name-guess231,8577
(defcustom proof-tidy-response239,8842
(defcustom proof-keep-response-history253,9305
(defcustom pg-input-ring-size 263,9693
(defcustom proof-general-debug 268,9845
(defcustom proof-use-parser-cache 279,10254
(defcustom proof-follow-mode 289,10551
(defcustom proof-auto-action-when-deactivating-scripting 313,11728
(defcustom proof-script-command-separator 336,12677
(defcustom proof-rsh-command 344,12969
(defcustom proof-disappearing-proofs 360,13519
(defcustom proof-full-annotation 365,13680
(defcustom proof-minibuffer-messages 374,14052

generic/proof-utils.el,2033
(defmacro deflocal 61,1871
(defmacro proof-with-current-buffer-if-exists 68,2109
(deflocal proof-buffer-type 74,2319
(defmacro proof-with-script-buffer 80,2599
(defmacro proof-map-buffers 91,2980
(defmacro proof-sym 96,3165
(defsubst proof-try-require 101,3326
(defun proof-save-some-buffers 114,3657
(defmacro proof-ass-sym 163,5258
(defmacro proof-ass-symv 169,5517
(defmacro proof-ass 175,5775
(defun proof-defpgcustom-fn 181,6027
(defun undefpgcustom 202,6897
(defmacro defpgcustom 208,7121
(defun proof-defpgdefault-fn 219,7532
(defmacro defpgdefault 233,7990
(defmacro defpgfun 244,8352
(defun proof-defpacustom-fn 258,8752
(defmacro defpacustom 324,11033
(defmacro proof-eval-when-ready-for-assistant 345,11980
(defun proof-file-truename 358,12371
(defun proof-files-to-buffers 362,12554
(defun proof-buffers-in-mode 370,12794
(defun pg-save-from-death 384,13244
(defun proof-define-keys 403,13861
(defun pg-remove-specials 414,14146
(defun pg-remove-specials-in-string 424,14482
(defun proof-warn-if-unset 435,14708
(defun proof-get-window-for-buffer 440,14926
(defun proof-display-and-keep-buffer 491,17234
(defun proof-clean-buffer 533,18957
(defun pg-internal-warning 549,19613
(defun proof-debug 556,19880
(defun proof-switch-to-buffer 566,20252
(defun proof-resize-window-tofit 588,21376
(defun proof-submit-bug-report 683,25224
(defun proof-deftoggle-fn 718,26581
(defmacro proof-deftoggle 733,27234
(defun proof-defintset-fn 740,27608
(defmacro proof-defintset 756,28312
(defun proof-defstringset-fn 763,28689
(defmacro proof-defstringset 776,29315
(defun proof-escape-keymap-doc 789,29771
(defmacro proof-defshortcut 793,29911
(defmacro proof-definvisible 808,30509
(defun pg-custom-save-vars 835,31436
(defun pg-custom-reset-vars 851,32080
(defun proof-locate-executable 864,32417
(defun pg-current-word-pos 879,32972
(defun proof-looking-at-syntactic-context 926,34688
(defsubst proof-shell-strip-output-markup 941,35257
(defun proof-minibuffer-message 947,35521

lib/bufhist.el,1257
(defun bufhist-ring-update 38,1391
(defgroup bufhist 47,1713
(defcustom bufhist-ring-size 51,1794
(defvar bufhist-ring 56,1905
(defvar bufhist-ring-pos 59,1979
(defvar bufhist-lastswitch-modified-tick 62,2058
(defvar bufhist-read-only-history 65,2164
(defvar bufhist-saved-mode-line-format 68,2235
(defvar bufhist-normal-read-only 71,2338
(defvar bufhist-top-point 74,2432
(defun bufhist-mode-line-format-entry 77,2522
(defconst bufhist-minor-mode-map106,3596
(define-minor-mode bufhist-mode119,4073
(defun bufhist-get-buffer-contents 141,4954
(defun bufhist-restore-buffer-contents 150,5296
(defun bufhist-checkpoint 159,5610
(defun bufhist-erase-buffer 167,5979
(defun bufhist-checkpoint-and-erase 178,6350
(defun bufhist-switch-to-index 184,6536
(defun bufhist-first 223,8135
(defun bufhist-last 228,8294
(defun bufhist-prev 233,8438
(defun bufhist-next 241,8661
(defun bufhist-delete 246,8801
(defun bufhist-clear 258,9342
(defun bufhist-init 273,9737
(defun bufhist-exit 301,10746
(defun bufhist-set-readwrite 311,11010
(defun bufhist-before-change-function 326,11630
(define-button-type 'bufhist-nextbufhist-next
340,12053
(define-button-type 'bufhist-prevbufhist-prev
344,12150
(defun bufhist-insert-buttons 351,12362

lib/holes.el,2465
(defvar holes-default-hole 44,1121
(defvar holes-active-hole 50,1299
(defgroup holes 60,1496
(defcustom holes-empty-hole-string 65,1595
(defcustom holes-empty-hole-regexp 70,1738
(defface active-hole-face92,2440
(defface inactive-hole-face102,2856
(defvar hole-map116,3297
(defvar holes-mode-map126,3688
(defun holes-region-beginning-or-nil 172,5425
(defun holes-region-end-or-nil 176,5561
(defun holes-copy-active-region 180,5679
(defun holes-is-hole-p 186,5889
(defun holes-hole-start-position 190,5981
(defun holes-hole-end-position 196,6164
(defun holes-hole-buffer 201,6335
(defun holes-hole-at 207,6509
(defun holes-active-hole-exist-p 212,6679
(defun holes-active-hole-start-position 219,6932
(defun holes-active-hole-end-position 227,7300
(defun holes-active-hole-buffer 236,7663
(defun holes-goto-active-hole 244,7964
(defun holes-highlight-hole-as-active 253,8223
(defun holes-highlight-hole 261,8531
(defun holes-disable-active-hole 269,8818
(defun holes-set-active-hole 282,9350
(defun holes-is-in-hole-p 292,9695
(defun holes-make-hole 296,9833
(defun holes-make-hole-at 314,10489
(defun holes-clear-hole 328,10942
(defun holes-clear-hole-at 337,11200
(defun holes-map-holes 345,11456
(defun holes-clear-all-buffer-holes 349,11610
(defun holes-next 359,11911
(defun holes-next-after-active-hole 366,12163
(defun holes-set-active-hole-next 373,12379
(defun holes-replace-segment 392,12916
(defun holes-replace 401,13269
(defun holes-replace-active-hole 429,14447
(defun holes-replace-update-active-hole 436,14738
(defun holes-delete-update-active-hole 454,15385
(defun holes-set-make-active-hole 462,15612
(defalias 'holes-track-mouse-selection holes-track-mouse-selection
477,16167
(defsubst holes-track-mouse-clicks 478,16225
(defun holes-mouse-replace-active-hole 482,16335
(defun holes-destroy-hole 496,16806
(defsubst holes-hole-at-event 510,17188
(defun holes-mouse-destroy-hole 514,17288
(defun holes-mouse-forget-hole 521,17509
(defun holes-mouse-set-make-active-hole 531,17801
(defun holes-mouse-set-active-hole 547,18300
(defun holes-set-point-next-hole-destroy 556,18551
(defun holes-replace-string-by-holes-backward 582,19532
(defun holes-skeleton-end-hook 600,20232
(defconst holes-jump-doc609,20670
(defun holes-replace-string-by-holes-backward-jump 616,20876
(define-minor-mode holes-mode 633,21558
(defun holes-abbrev-complete 728,25040
(defun holes-insert-and-expand 738,25383

lib/local-vars-list.el,373
(defconst local-vars-list-doc 28,825
(defun local-vars-list-insert-empty-zone 44,1387
(defun local-vars-list-find 82,2090
(defun local-vars-list-goto-var 101,2861
(defun local-vars-list-get-current 127,3908
(defun local-vars-list-set-current 148,4758
(defun local-vars-list-get 171,5473
(defun local-vars-list-get-safe 188,6003
(defun local-vars-list-set 193,6197

lib/maths-menu.el,242
(defvar maths-menu-filter-predicate 56,2317
(defvar maths-menu-tokenise-insert 59,2426
(defun maths-menu-build-menu 62,2563
(defvar maths-menu-menu84,3324
(defvar maths-menu-mode-map344,12882
(define-minor-mode maths-menu-mode352,13101

lib/pg-dev.el,166
(defconst pg-dev-lisp-font-lock-keywords52,1582
(defun pg-loadpath 80,2416
(defun unload-pg 90,2587
(defun profile-pg 118,3450
(defun pg-bug-references 139,4117

lib/pg-fontsets.el,210
(defcustom pg-fontsets-default-fontset 28,780
(defvar pg-fontsets-names 33,926
(defun pg-fontsets-make-fontsetsizes 36,1007
(defconst pg-fontsets-base-fonts55,1768
(defun pg-fontsets-make-fontsets 61,1898

lib/proof-compat.el,297
(defvar proof-running-on-win32 32,975
(defun pg-custom-undeclare-variable 53,1777
(defmacro save-selected-frame 85,2548
(defun proof-buffer-syntactic-context-emulate 95,2925
(defalias 'proof-buffer-syntactic-contextproof-buffer-syntactic-context
164,5213
(defmacro declare-function 179,5596

lib/ps-fix.el,72
(defun ps-face-attributes 5,191
(defun ps-face-attribute-list 37,1269

lib/scomint.el,876
(defface scomint-highlight-input 19,493
(defface scomint-highlight-prompt23,609
(defvar scomint-buffer-maximum-size 30,847
(defvar scomint-output-filter-functions 35,1038
(defvar scomint-mode-map39,1149
(defvar scomint-last-input-start 45,1328
(defvar scomint-last-input-end 46,1366
(defvar scomint-last-output-start 47,1402
(defvar scomint-exec-hook 49,1442
(define-derived-mode scomint-mode 59,1824
(defsubst scomint-check-proc 78,2739
(defun scomint-make-in-buffer 86,3079
(defun scomint-make 110,4346
(defun scomint-exec 123,5057
(defun scomint-exec-1 160,6650
(defalias 'scomint-send-string scomint-send-string
210,8780
(defun scomint-send-eof 212,8834
(defun scomint-send-input 221,9067
(defun scomint-truncate-buffer 264,10568
(defun scomint-strip-ctrl-m 277,10962
(defun scomint-output-filter 291,11525
(defun scomint-interrupt-process 363,14257

lib/span.el,1315
(defalias 'span-start span-start
22,609
(defalias 'span-end span-end
23,647
(defalias 'span-set-property span-set-property
24,681
(defalias 'span-property span-property
25,724
(defalias 'span-make span-make
26,763
(defalias 'span-detach span-detach
27,799
(defalias 'span-set-endpoints span-set-endpoints
28,839
(defalias 'span-buffer span-buffer
29,884
(defun span-read-only-hook 31,925
(defsubst span-read-only 36,1115
(defsubst span-read-write 43,1425
(defsubst span-write-warning 48,1595
(defsubst span-lt 59,2119
(defsubst spans-at-point-prop 64,2263
(defsubst spans-at-region-prop 73,2454
(defsubst span-at 83,2720
(defsubst span-delete 87,2846
(defsubst span-mapcar-spans 94,3068
(defsubst span-mapc-spans 98,3243
(defun span-at-before 102,3414
(defsubst prev-span 119,4138
(defsubst next-span 125,4291
(defsubst span-live-p 131,4505
(defsubst span-raise 137,4671
(defsubst span-string 141,4804
(defsubst set-span-properties 146,4964
(defsubst span-find-span 152,5158
(defsubst span-at-event 160,5470
(defun fold-spans 166,5667
(defsubst span-detached-p 180,6200
(defsubst set-span-face 184,6316
(defsubst set-span-keymap 188,6414
(defsubst span-delete-spans 196,6583
(defsubst span-property-safe 200,6745
(defsubst span-set-start 204,6882
(defsubst span-set-end 208,7014

lib/texi-docstring-magic.el,584
(defun texi-docstring-magic-find-face 88,3027
(defun texi-docstring-magic-splice-sep 93,3192
(defconst texi-docstring-magic-munge-table103,3497
(defun texi-docstring-magic-untabify 193,7260
(defun texi-docstring-magic-munge-docstring 203,7575
(defun texi-docstring-magic-texi 242,8856
(defun texi-docstring-magic-format-default 255,9296
(defun texi-docstring-magic-texi-for 271,9929
(defconst texi-docstring-magic-comment329,11888
(defun texi-docstring-magic 335,12042
(defun texi-docstring-magic-face-at-point 369,13121
(defun texi-docstring-magic-insert-magic 384,13644

lib/unicode-chars.el,80
(defvar unicode-chars-alist12,348
(defun unicode-chars-list-chars 5051,245975

lib/unicode-tokens.el,5431
(defgroup unicode-tokens-options 54,1695
(defcustom unicode-tokens-add-help-echo 58,1804
(defun unicode-tokens-toggle-add-help-echo 63,1971
(defvar unicode-tokens-token-symbol-map 77,2377
(defvar unicode-tokens-token-format 96,2999
(defvar unicode-tokens-token-variant-format-regexp 102,3248
(defvar unicode-tokens-shortcut-alist 116,3781
(defvar unicode-tokens-shortcut-replacement-alist 122,4058
(defvar unicode-tokens-control-region-format-regexp 130,4264
(defvar unicode-tokens-control-char-format-regexp 137,4632
(defvar unicode-tokens-control-regions 144,4993
(defvar unicode-tokens-control-characters 147,5069
(defvar unicode-tokens-control-char-format 150,5151
(defvar unicode-tokens-control-region-format-start 153,5264
(defvar unicode-tokens-control-region-format-end 156,5381
(defvar unicode-tokens-tokens-customizable-variables 159,5494
(defconst unicode-tokens-configuration-variables166,5662
(defun unicode-tokens-config 181,6061
(defun unicode-tokens-config-var 185,6206
(defun unicode-tokens-copy-configuration-variables 197,6646
(defvar unicode-tokens-token-list 225,7862
(defvar unicode-tokens-hash-table 228,7982
(defvar unicode-tokens-token-match-regexp 231,8098
(defvar unicode-tokens-uchar-hash-table 237,8381
(defvar unicode-tokens-uchar-regexp 241,8568
(defgroup unicode-tokens-faces 249,8753
(defconst unicode-tokens-font-family-alternatives259,9050
(defface unicode-tokens-symbol-font-face273,9498
(defface unicode-tokens-script-font-face291,10138
(defface unicode-tokens-fraktur-font-face296,10282
(defface unicode-tokens-serif-font-face301,10407
(defface unicode-tokens-sans-font-face306,10544
(defface unicode-tokens-highlight-face311,10666
(defconst unicode-tokens-fonts320,11028
(defconst unicode-tokens-fontsymb-properties329,11245
(define-widget 'unicode-tokens-token-symbol-map unicode-tokens-token-symbol-map
355,12691
(define-widget 'unicode-tokens-shortcut-alist unicode-tokens-shortcut-alist
373,13243
(defconst unicode-tokens-font-lock-extra-managed-props386,13574
(defun unicode-tokens-font-lock-keywords 390,13728
(defun unicode-tokens-calculate-token-match 423,15099
(defun unicode-tokens-usable-composition 453,16137
(defun unicode-tokens-help-echo 466,16516
(defvar unicode-tokens-show-symbols 471,16718
(defun unicode-tokens-interpret-composition 474,16832
(defun unicode-tokens-font-lock-compose-symbol 492,17344
(defun unicode-tokens-prepend-text-properties-in-match 522,18591
(defun unicode-tokens-prepend-text-property 536,19169
(defun unicode-tokens-show-symbols 561,20314
(defun unicode-tokens-symbs-to-props 569,20624
(defvar unicode-tokens-show-controls 589,21323
(defun unicode-tokens-show-controls 592,21414
(defun unicode-tokens-control-char 605,21999
(defun unicode-tokens-control-region 614,22438
(defun unicode-tokens-control-font-lock-keywords 625,22985
(defvar unicode-tokens-use-shortcuts 636,23309
(defun unicode-tokens-use-shortcuts 639,23412
(defun unicode-tokens-map-ordering 657,24018
(defun unicode-tokens-quail-define-rules 666,24371
(defun unicode-tokens-insert-token 689,25048
(defun unicode-tokens-annotate-region 698,25352
(defun unicode-tokens-insert-control 722,26190
(defun unicode-tokens-insert-uchar-as-token 732,26639
(defun unicode-tokens-delete-token-near-point 738,26860
(defun unicode-tokens-prev-token 752,27422
(defun unicode-tokens-rotate-token-forward 760,27719
(defun unicode-tokens-rotate-token-backward 787,28609
(defun unicode-tokens-replace-shortcut-match 792,28811
(defun unicode-tokens-replace-shortcuts 801,29181
(defun unicode-tokens-replace-unicode-match 815,29779
(defun unicode-tokens-replace-unicode 822,30080
(defun unicode-tokens-copy-token 839,30679
(define-button-type 'unicode-tokens-listunicode-tokens-list
846,30900
(defun unicode-tokens-list-tokens 852,31104
(defun unicode-tokens-list-shortcuts 891,32288
(defalias 'unicode-tokens-list-unicode-chars unicode-tokens-list-unicode-chars
909,32926
(defun unicode-tokens-encode-in-temp-buffer 911,32999
(defun unicode-tokens-encode 929,33655
(defun unicode-tokens-encode-str 935,33891
(defun unicode-tokens-copy 939,34053
(defun unicode-tokens-paste 948,34459
(defvar unicode-tokens-highlight-unicode 967,35180
(defconst unicode-tokens-unicode-highlight-patterns970,35272
(defun unicode-tokens-highlight-unicode 974,35441
(defun unicode-tokens-highlight-unicode-setkeywords 986,35904
(defun unicode-tokens-initialise 998,36273
(defvar unicode-tokens-mode-map 1018,36944
(defvar unicode-tokens-display-table 1021,37041
(define-minor-mode unicode-tokens-mode1028,37293
(defun unicode-tokens-set-font-var 1161,41776
(defun unicode-tokens-set-font-var-aux 1177,42267
(defun unicode-tokens-mouse-set-font 1206,43509
(defsubst unicode-tokens-face-font-sym 1219,44023
(defun unicode-tokens-set-font-restart 1223,44203
(defun unicode-tokens-save-fonts 1234,44513
(defun unicode-tokens-custom-save-faces 1242,44769
(define-key unicode-tokens-mode-map 1259,45225
(define-key unicode-tokens-mode-map 1261,45317
(define-key unicode-tokens-mode-map1263,45408
(define-key unicode-tokens-mode-map1265,45514
(define-key unicode-tokens-mode-map1268,45629
(define-key unicode-tokens-mode-map1270,45738
(define-key unicode-tokens-mode-map1272,45846
(define-key unicode-tokens-mode-map1274,45952
(defun unicode-tokens-customize-submenu 1282,46076
(defun unicode-tokens-define-menu 1289,46299

mmm/mmm-auto.el,343
(defvar mmm-autoloaded-classes67,2676
(defun mmm-autoload-class 89,3439
(defvar mmm-changed-buffers-list 129,4992
(defun mmm-major-mode-change 132,5099
(defun mmm-check-changed-buffers 145,5620
(defun mmm-mode-on-maybe 155,5979
(defalias 'mmm-add-find-file-hooks mmm-add-find-file-hooks
167,6383
(defun mmm-add-find-file-hook 168,6443

mmm/mmm-class.el,415
(defun mmm-get-class-spec 42,1296
(defun mmm-get-class-parameter 59,1939
(defun mmm-set-class-parameter 63,2105
(defun* mmm-apply-class75,2455
(defun* mmm-apply-classes90,3072
(defun* mmm-apply-all 110,3803
(defun* mmm-ify124,4250
(defun* mmm-match-region206,7095
(defun mmm-match->point 269,9480
(defun mmm-match-and-verify 284,10050
(defun mmm-get-form 310,11101
(defun mmm-default-get-form 321,11576

mmm/mmm-cmds.el,712
(defun mmm-ify-by-class 41,1210
(defun mmm-ify-region 63,1822
(defun mmm-ify-by-regexp75,2243
(defun mmm-parse-buffer 97,2886
(defun mmm-parse-region 106,3222
(defun mmm-parse-block 115,3601
(defun mmm-get-block 132,4352
(defun mmm-reparse-current-region 146,4634
(defun mmm-clear-current-region 167,5210
(defun mmm-clear-regions 172,5374
(defun mmm-clear-all-regions 177,5520
(defun* mmm-end-current-region 185,5680
(defun mmm-narrow-to-submode-region 220,6928
(defun mmm-insert-region 239,7542
(defun mmm-insert-by-key 258,8348
(defun mmm-get-insertion-spec 342,11613
(defun mmm-insertion-help 369,12573
(defun mmm-display-insertion-key 379,12936
(defun mmm-get-all-insertion-keys 401,13723

mmm/mmm-compat.el,418
(defvar mmm-xemacs 40,1313
(defvar mmm-keywords-used49,1616
(defmacro mmm-regexp-opt 91,2632
(defvar mmm-evaporate-property110,3281
(defmacro mmm-set-keymap-default 128,4047
(defmacro mmm-event-key 137,4489
(defvar skeleton-positions 146,4708
(defun mmm-fixup-skeleton 147,4739
(defmacro mmm-make-temp-buffer 159,5162
(defvar mmm-font-lock-available-p 172,5558
(defmacro mmm-set-font-lock-defaults 179,5772

mmm/mmm-cweb.el,228
(defvar mmm-cweb-section-tags38,1117
(defvar mmm-cweb-section-regexp41,1164
(defvar mmm-cweb-c-part-tags44,1254
(defvar mmm-cweb-c-part-regexp47,1313
(defun mmm-cweb-in-limbo 50,1397
(defun mmm-cweb-verify-brief-c 57,1622

mmm/mmm-mason.el,410
(defvar mmm-mason-perl-tags41,1236
(defvar mmm-mason-pseudo-perl-tags45,1377
(defvar mmm-mason-non-perl-tags48,1453
(defvar mmm-mason-perl-tags-regexp51,1554
(defvar mmm-mason-pseudo-perl-tags-regexp56,1749
(defvar mmm-mason-tag-names-regexp61,1966
(defun mmm-mason-verify-inline 66,2186
(defun mmm-mason-start-line 156,4838
(defun mmm-mason-end-line 161,4903
(defun mmm-mason-set-mode-line 168,4997

mmm/mmm-mode.el,1023
(defun mmm-mode 101,3867
(defun mmm-mode-on 140,5372
(defun mmm-mode-off 181,7048
(defvar mmm-mode-map 206,7760
(defvar mmm-mode-prefix-map 209,7835
(defvar mmm-mode-menu-map 212,7945
(defun mmm-define-key 215,8036
(define-key mmm-mode-prefix-map 239,8791
(define-key mmm-mode-prefix-map 246,9049
(define-key mmm-mode-map 249,9160
(define-key mmm-mode-menu-map 252,9262
(define-key mmm-mode-menu-map 254,9334
(define-key mmm-mode-menu-map 256,9393
(define-key mmm-mode-menu-map 258,9474
(define-key mmm-mode-menu-map 260,9555
(define-key mmm-mode-menu-map 262,9642
(define-key mmm-mode-menu-map 265,9736
(define-key mmm-mode-menu-map 267,9796
(define-key mmm-mode-menu-map 270,9887
(define-key mmm-mode-menu-map 272,9947
(define-key mmm-mode-menu-map 274,10054
(define-key mmm-mode-menu-map 276,10139
(define-key mmm-mode-menu-map 279,10225
(define-key mmm-mode-menu-map 281,10285
(define-key mmm-mode-menu-map 283,10398
(define-key mmm-mode-menu-map 285,10483
(define-key mmm-mode-map 288,10566

mmm/mmm-region.el,1643
(defsubst mmm-overlay-at 54,1749
(defun mmm-overlays-at 59,1934
(defun mmm-included-p 72,2387
(defun mmm-overlays-containing 112,3876
(defun mmm-overlays-contained-in 125,4314
(defun mmm-overlays-overlapping 138,4754
(defun mmm-sort-overlays 149,5117
(defvar mmm-current-overlay 158,5359
(defvar mmm-previous-overlay 163,5574
(defvar mmm-current-submode 168,5762
(defvar mmm-previous-submode 173,5962
(defun mmm-update-current-submode 178,6135
(defun mmm-set-current-submode 199,6930
(defun mmm-submode-at 210,7373
(defun mmm-match-front 219,7648
(defun mmm-match-back 238,8409
(defun mmm-front-start 257,9154
(defun mmm-back-end 265,9458
(defun mmm-valid-submode-region 278,9805
(defun* mmm-make-region305,10961
(defun mmm-make-overlay 431,16311
(defun mmm-get-face 459,17444
(defun mmm-clear-overlays 470,17736
(defun mmm-update-mode-info 486,18201
(defun mmm-update-submode-region 572,21856
(defun mmm-add-hooks 589,22586
(defun mmm-remove-hooks 592,22683
(defun mmm-get-local-variables-list 598,22810
(defun mmm-get-locals 618,23506
(defun mmm-get-saved-local 631,24003
(defun mmm-set-local-variables 635,24168
(defun mmm-get-saved-local-variables 646,24546
(defun mmm-save-changed-local-variables 654,24821
(defun mmm-clear-local-variables 673,25525
(defun mmm-enable-font-lock 684,25790
(defun mmm-update-font-lock-buffer 692,26050
(defun mmm-refontify-maybe 705,26461
(defun mmm-submode-changes-in 720,26941
(defun mmm-regions-in 731,27298
(defun mmm-regions-alist 745,27776
(defun mmm-fontify-region 762,28303
(defun mmm-fontify-region-list 782,29299
(defun mmm-beginning-of-syntax 804,30047

mmm/mmm-rpm.el,154
(defconst mmm-rpm-sh-start-tags48,1618
(defvar mmm-rpm-sh-end-tags53,1842
(defvar mmm-rpm-sh-start-regexp57,2016
(defvar mmm-rpm-sh-end-regexp61,2194

mmm/mmm-sample.el,168
(defvar mmm-here-doc-mode-alist 84,2601
(defun mmm-here-doc-get-mode 93,3086
(defun mmm-file-variables-verify 208,6343
(defun mmm-file-variables-find-back 232,7148

mmm/mmm-univ.el,34
(defun mmm-univ-get-mode 38,1205

mmm/mmm-utils.el,282
(defmacro mmm-valid-buffer 42,1332
(defmacro mmm-save-all 61,1941
(defun mmm-format-string 74,2223
(defun mmm-format-matches 85,2661
(defmacro mmm-save-keyword 108,3419
(defmacro mmm-save-keywords 116,3746
(defun mmm-looking-back-at 129,4244
(defun mmm-make-marker 146,4784

mmm/mmm-vars.el,2668
(defgroup mmm 104,3283
(defvar mmm-c-derived-modes111,3393
(defvar mmm-save-local-variables115,3512
(defvar mmm-buffer-saved-locals 341,10293
(defvar mmm-region-saved-locals-defaults 346,10493
(defvar mmm-region-saved-locals-for-dominant 352,10753
(defgroup mmm-faces 362,11130
(defcustom mmm-submode-decoration-level 368,11301
(defface mmm-init-submode-face 386,12145
(defface mmm-cleanup-submode-face 390,12285
(defface mmm-declaration-submode-face 394,12422
(defface mmm-comment-submode-face 398,12568
(defface mmm-output-submode-face 402,12721
(defface mmm-special-submode-face 406,12870
(defface mmm-code-submode-face 410,13034
(defface mmm-default-submode-face 414,13173
(defface mmm-delimiter-face 419,13381
(defcustom mmm-mode-string 426,13507
(defcustom mmm-submode-mode-line-format 431,13638
(defvar mmm-primary-mode-display-name 448,14293
(defvar mmm-buffer-mode-display-name 453,14507
(defun mmm-set-mode-line 459,14806
(defvar mmm-classes 483,15614
(defvar mmm-global-classes 489,15859
(defcustom mmm-mode-ext-classes-alist 496,16041
(defun mmm-add-mode-ext-class 515,16831
(defcustom mmm-major-mode-preferences524,17156
(defun mmm-add-to-major-mode-preferences 542,17884
(defun mmm-ensure-modename 558,18642
(defun mmm-modename->function 567,18945
(defcustom mmm-delimiter-mode 581,19394
(defcustom mmm-mode-prefix-key 591,19663
(defcustom mmm-command-modifiers 596,19790
(defcustom mmm-insert-modifiers 610,20423
(defcustom mmm-use-old-command-keys 625,21101
(defun mmm-use-old-command-keys 635,21565
(defcustom mmm-mode-hook 643,21757
(defun mmm-run-constructed-hook 663,22564
(defun mmm-run-major-hook 671,22908
(defun mmm-run-submode-hook 674,22985
(defvar mmm-class-hooks-run 677,23072
(defun mmm-run-class-hook 682,23244
(defvar mmm-primary-mode-entry-hook 687,23416
(defcustom mmm-major-mode-hook 702,24063
(defun mmm-run-major-mode-hook 716,24694
(defcustom mmm-global-mode 729,25235
(defcustom mmm-never-modes745,25902
(defvar mmm-set-file-name-for-modes 763,26202
(defvar mmm-mode 774,26561
(defvar mmm-primary-mode 782,26769
(defvar mmm-classes-alist 793,27135
(defun mmm-add-classes 948,35342
(defun mmm-add-group 953,35507
(defun mmm-add-to-group 963,35880
(defconst mmm-version 977,36307
(defun mmm-version 980,36372
(defvar mmm-temp-buffer-name 987,36515
(defvar mmm-interactive-history 993,36645
(defun mmm-add-to-history 999,36914
(defun mmm-clear-history 1002,36997
(defvar mmm-mode-ext-classes 1010,37182
(defun mmm-get-mode-ext-classes 1015,37393
(defun mmm-clear-mode-ext-classes 1024,37720
(defun mmm-mode-ext-applies 1028,37845
(defun mmm-get-all-classes 1042,38224

doc/ProofGeneral.texi,5693
@node Top164,4937
@node Preface201,6044
@node News for Version 4.0News for Version 4.0
224,6633
@node Future241,7193
@node Credits270,8528
@node Introducing Proof GeneralIntroducing Proof General
380,12340
@node Installing Proof GeneralInstalling Proof General
435,14318
@node Quick start guideQuick start guide
449,14767
@node Features of Proof GeneralFeatures of Proof General
493,16888
@node Supported proof assistantsSupported proof assistants
582,20825
@node Prerequisites for this manualPrerequisites for this manual
631,22714
@node Organization of this manualOrganization of this manual
675,24333
@node Basic Script ManagementBasic Script Management
701,25161
@node Walkthrough example in IsabelleWalkthrough example in Isabelle
720,25761
@node Proof scriptsProof scripts
986,35994
@node Script buffersScript buffers
1029,38114
@node Locked queue and editing regionsLocked queue and editing regions
1051,38691
@node Goal-save sequencesGoal-save sequences
1107,40838
@node Active scripting bufferActive scripting buffer
1144,42324
@node Summary of Proof General buffersSummary of Proof General buffers
1213,45744
@node Script editing commandsScript editing commands
1276,48484
@node Script processing commandsScript processing commands
1356,51442
@node Proof assistant commandsProof assistant commands
1483,56735
@node Toolbar commandsToolbar commands
1658,62928
@node Interrupting during trace outputInterrupting during trace output
1682,63857
@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
1721,65778
@node Goals buffer commandsGoals buffer commands
1736,66290
@node Advanced Script Management and EditingAdvanced Script Management and Editing
1825,69854
@node Document centred workingDocument centred working
1857,71069
@node Visibility of completed proofsVisibility of completed proofs
1923,73173
@node Switching between proof scriptsSwitching between proof scripts
1978,75096
@node View of processed files View of processed files 
2015,77068
@node Retracting across filesRetracting across files
2075,80119
@node Asserting across filesAsserting across files
2088,80750
@node Automatic multiple file handlingAutomatic multiple file handling
2101,81316
@node Escaping script managementEscaping script management
2126,82350
@node Editing featuresEditing features
2183,84462
@node Support for other PackagesSupport for other Packages
2254,87254
@node Syntax highlightingSyntax highlighting
2286,88128
@node Unicode supportUnicode support
2315,89132
@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)
2471,95367
@node Support for outline modeSupport for outline mode
2526,97411
@node Support for completionSupport for completion
2551,98540
@node Support for tagsSupport for tags
2608,100702
@node Customizing Proof GeneralCustomizing Proof General
2660,103030
@node Basic optionsBasic options
2700,104700
@node How to customizeHow to customize
2724,105458
@node Display customizationDisplay customization
2771,107425
@node User optionsUser options
2925,113824
@node Changing facesChanging faces
3167,122377
@node Tweaking configuration settingsTweaking configuration settings
3242,125046
@node Hints and TipsHints and Tips
3299,127572
@node Adding your own keybindingsAdding your own keybindings
3318,128173
@node Using file variablesUsing file variables
3382,130760
@node Using abbreviationsUsing abbreviations
3441,132946
@node LEGO Proof GeneralLEGO Proof General
3480,134361
@node LEGO specific commandsLEGO specific commands
3521,135730
@node LEGO tagsLEGO tags
3541,136185
@node LEGO customizationsLEGO customizations
3551,136432
@node Coq Proof GeneralCoq Proof General
3583,137351
@node Coq-specific commandsCoq-specific commands
3599,137760
@node Coq-specific variablesCoq-specific variables
3621,138267
@node Editing multiple proofsEditing multiple proofs
3643,138925
@node User-loaded tacticsUser-loaded tactics
3667,140033
@node Holes featureHoles feature
3731,142507
@node Isabelle Proof GeneralIsabelle Proof General
3758,143794
@node Choosing logic and starting isabelleChoosing logic and starting isabelle
3789,144963
@node Isabelle commandsIsabelle commands
3858,147771
@node Isabelle settingsIsabelle settings
4001,151924
@node Isabelle customizationsIsabelle customizations
4015,152506
@node HOL Proof GeneralHOL Proof General
4038,152993
@node Shell Proof GeneralShell Proof General
4080,154815
@node Obtaining and InstallingObtaining and Installing
4116,156274
@node Obtaining Proof GeneralObtaining Proof General
4132,156687
@node Installing Proof General from tarballInstalling Proof General from tarball
4163,157926
@node Installing Proof General from RPM packageInstalling Proof General from RPM package
4188,158758
@node Setting the names of binariesSetting the names of binaries
4203,159166
@node Notes for syssiesNotes for syssies
4231,160106
@node Bugs and EnhancementsBugs and Enhancements
4306,163142
@node References4327,163957
@node History of Proof GeneralHistory of Proof General
4367,164980
@node Old News for 3.0Old News for 3.0
4461,169145
@node Old News for 3.1Old News for 3.1
4531,172839
@node Old News for 3.2Old News for 3.2
4557,174011
@node Old News for 3.3Old News for 3.3
4618,177014
@node Old News for 3.4Old News for 3.4
4637,177911
@node Old News for 3.5Old News for 3.5
4659,178966
@node Old News for 3.6Old News for 3.6
4663,179023
@node Old News for 3.7Old News for 3.7
4668,179123
@node Function IndexFunction Index
4712,181021
@node Variable IndexVariable Index
4716,181097
@node Keystroke IndexKeystroke Index
4720,181177
@node Concept IndexConcept Index
4724,181243

doc/PG-adapting.texi,3772
@node Top155,4689
@node Introduction192,5798
@node Future233,7451
@node Credits269,9047
@node Beginning with a New ProverBeginning with a New Prover
279,9339
@node Overview of adding a new proverOverview of adding a new prover
319,11281
@node Demonstration instance and easy configurationDemonstration instance and easy configuration
396,14587
@node Major modes used by Proof GeneralMajor modes used by Proof General
465,17978
@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands
508,19688
@node Settings for generic user-level commandsSettings for generic user-level commands
523,20234
@node Menu configurationMenu configuration
568,21966
@node Toolbar configurationToolbar configuration
592,22883
@node Proof Script SettingsProof Script Settings
651,25120
@node Recognizing commands and commentsRecognizing commands and comments
673,25700
@node Recognizing proofsRecognizing proofs
810,32137
@node Recognizing other elementsRecognizing other elements
919,36811
@node Configuring undo behaviourConfiguring undo behaviour
1045,42343
@node Nested proofsNested proofs
1182,47721
@node Safe (state-preserving) commandsSafe (state-preserving) commands
1222,49347
@node Activate scripting hookActivate scripting hook
1245,50300
@node Automatic multiple filesAutomatic multiple files
1269,51170
@node Completions1291,52017
@node Proof Shell SettingsProof Shell Settings
1332,53507
@node Proof shell commandsProof shell commands
1363,54789
@node Script input to the shellScript input to the shell
1527,61833
@node Settings for matching various output from proof processSettings for matching various output from proof process
1595,64903
@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process
1717,70259
@node Hooks and other settingsHooks and other settings
1957,81017
@node Goals Buffer SettingsGoals Buffer Settings
2042,84530
@node Splash Screen SettingsSplash Screen Settings
2119,87636
@node Global ConstantsGlobal Constants
2145,88391
@node Handling Multiple FilesHandling Multiple Files
2171,89220
@node Configuring Editing SyntaxConfiguring Editing Syntax
2323,97003
@node Configuring Font LockConfiguring Font Lock
2380,99120
@node Configuring TokensConfiguring Tokens
2452,102614
@node Writing More Lisp CodeWriting More Lisp Code
2502,104734
@node Default values for generic settingsDefault values for generic settings
2519,105379
@node Adding prover-specific configurationsAdding prover-specific configurations
2549,106462
@node Useful variablesUseful variables
2592,107744
@node Useful functions and macrosUseful functions and macros
2607,108243
@node Internals of Proof GeneralInternals of Proof General
2716,112466
@node Spans2744,113362
@node Proof General site configurationProof General site configuration
2756,113684
@node Configuration variable mechanismsConfiguration variable mechanisms
2836,116729
@node Global variablesGlobal variables
2957,122166
@node Proof script modeProof script mode
3027,124714
@node Proof shell modeProof shell mode
3269,135436
@node Debugging3775,155603
@node Plans and IdeasPlans and Ideas
3818,156479
@node Proof by pointing and similar featuresProof by pointing and similar features
3839,157201
@node Granularity of atomic command sequencesGranularity of atomic command sequences
3877,158859
@node Browser mode for script files and theoriesBrowser mode for script files and theories
3922,161084
@node Demonstration InstantiationsDemonstration Instantiations
3952,162115
@node demoisa-easy.el3968,162546
@node demoisa.el4030,164738
@node Function IndexFunction Index
4184,169678
@node Variable IndexVariable Index
4188,169754
@node Concept IndexConcept Index
4197,169933

generic/proof.el,0

pgshell/pgshell.el,0

isar/isar-autotest.el,0

isar/interface-setup.el,0

demoisa/demoisa-easy.el,0

coq/coq-mmm.el,0

coq/coq-autotest.el,0

acl2/acl2.el,0