path: root/TAGS


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,600
(defconst coq-syntax-db 21,521
(defvar coq-user-tactics-db57,1894
(defun coq-insert-from-db 67,2243
(defun coq-build-regexp-list-from-db 85,2975
(defun max-length-db 107,3958
(defun coq-build-menu-from-db-internal 119,4233
(defun coq-build-title-menu 154,5856
(defun coq-sort-menu-entries 163,6224
(defun coq-build-menu-from-db 169,6351
(defcustom coq-holes-minor-mode 191,7186
(defun coq-build-abbrev-table-from-db 197,7330
(defun filter-state-preserving 216,7968
(defun filter-state-changing 221,8122
(defface coq-solve-tactics-face228,8343
(defconst coq-solve-tactics-face 236,8599

coq/coq.el,5449
(defcustom coq-translate-to-v8 48,1389
(defun coq-build-prog-args 54,1569
(defcustom coq-compile-file-command 64,1865
(defcustom coq-use-makefile 72,2184
(defcustom coq-default-undo-limit 80,2407
(defconst coq-shell-init-cmd85,2535
(defcustom coq-prog-env 91,2662
(defconst coq-shell-restart-cmd 99,2912
(defvar coq-shell-prompt-pattern101,2966
(defvar coq-shell-cd 109,3270
(defvar coq-shell-proof-completed-regexp 113,3430
(defvar coq-goal-regexp116,3582
(defun coq-library-directory 123,3696
(defcustom coq-tags 130,3875
(defconst coq-interrupt-regexp 135,4025
(defcustom coq-www-home-page 140,4146
(defvar coq-outline-regexp147,4314
(defvar coq-outline-heading-end-regexp 154,4526
(defvar coq-shell-outline-regexp 156,4580
(defvar coq-shell-outline-heading-end-regexp 157,4630
(defconst coq-state-preserving-tactics-regexp163,4795
(defconst coq-state-changing-commands-regexp165,4895
(defconst coq-state-preserving-commands-regexp167,5002
(defconst coq-commands-regexp169,5113
(defvar coq-retractable-instruct-regexp171,5190
(defvar coq-non-retractable-instruct-regexp173,5280
(defun coq-set-undo-limit 207,6151
(defun build-list-id-from-string 211,6281
(defun coq-last-prompt-info 223,6779
(defun coq-last-prompt-info-safe 235,7311
(defvar coq-last-but-one-statenum 241,7568
(defvar coq-last-but-one-proofnum 247,7865
(defvar coq-last-but-one-proofstack 250,7963
(defun coq-get-span-statenum 253,8073
(defun coq-get-span-proofnum 258,8188
(defun coq-get-span-proofstack 263,8303
(defun coq-set-span-statenum 268,8447
(defun coq-get-span-goalcmd 273,8578
(defun coq-set-span-goalcmd 278,8692
(defun coq-set-span-proofnum 283,8822
(defun coq-set-span-proofstack 288,8953
(defun proof-last-locked-span 293,9113
(defun coq-set-state-infos 308,9716
(defun count-not-intersection 347,11711
(defun coq-find-and-forget 378,12961
(defvar coq-current-goal 397,13848
(defun coq-goal-hyp 400,13913
(defun coq-state-preserving-p 413,14345
(defconst notation-print-kinds-table427,14846
(defun coq-PrintScope 431,15013
(defun coq-guess-or-ask-for-string 449,15562
(defun coq-ask-do 463,16130
(defun coq-SearchIsos 472,16515
(defun coq-SearchConstant 478,16748
(defun coq-SearchRewrite 482,16841
(defun coq-SearchAbout 486,16939
(defun coq-Print 490,17031
(defun coq-About 494,17153
(defun coq-LocateConstant 498,17270
(defun coq-LocateLibrary 504,17405
(defun coq-addquotes 510,17555
(defun coq-LocateNotation 512,17603
(defun coq-Pwd 519,17801
(defun coq-Inspect 525,17933
(defun coq-PrintSection(529,18033
(defun coq-Print-implicit 533,18126
(defun coq-Check 538,18277
(defun coq-Show 543,18385
(defun coq-Compile 557,18828
(defun coq-guess-command-line 569,19146
(defpacustom use-editing-holes 608,20818
(defun coq-mode-config 618,21155
(defun coq-shell-mode-config 722,25039
(defun coq-goals-mode-config 765,26838
(defun coq-response-config 772,27082
(defpacustom print-fully-explicit 797,27907
(defpacustom print-implicit 802,28055
(defpacustom print-coercions 807,28221
(defpacustom print-match-wildcards 812,28365
(defpacustom print-elim-types 817,28545
(defpacustom printing-depth 822,28711
(defpacustom undo-depth 827,28872
(defpacustom time-commands 832,29019
(defpacustom undo-limit 836,29129
(defpacustom auto-compile-vos 841,29231
(defun coq-maybe-compile-buffer 870,30345
(defun coq-ancestors-of 906,31873
(defun coq-all-ancestors-of 929,32837
(defun coq-process-require-command 940,33184
(defun coq-included-children 945,33311
(defun coq-process-file 966,34150
(defun coq-preprocessing 981,34689
(defun coq-fake-constant-markup 994,35096
(defun coq-create-span-menu 1010,35701
(defconst module-kinds-table1027,36196
(defconst modtype-kinds-table1031,36345
(defun coq-insert-section-or-module 1035,36474
(defconst reqkinds-kinds-table1058,37332
(defun coq-insert-requires 1063,37477
(defun coq-end-Section 1079,37980
(defun coq-insert-intros 1097,38558
(defun coq-insert-infoH-hook 1110,39090
(defun coq-insert-as 1115,39242
(defun coq-insert-match 1133,39985
(defun coq-insert-tactic 1165,41167
(defun coq-insert-tactical 1171,41406
(defun coq-insert-command 1177,41655
(defun coq-insert-term 1183,41899
(define-key coq-keymap 1189,42096
(define-key coq-keymap 1190,42154
(define-key coq-keymap 1191,42211
(define-key coq-keymap 1192,42280
(define-key coq-keymap 1193,42336
(define-key coq-keymap 1194,42385
(define-key coq-keymap 1195,42443
(define-key coq-keymap 1197,42504
(define-key coq-keymap 1198,42563
(define-key coq-keymap 1200,42627
(define-key coq-keymap 1201,42687
(define-key coq-keymap 1203,42743
(define-key coq-keymap 1204,42793
(define-key coq-keymap 1205,42843
(define-key coq-keymap 1206,42893
(define-key coq-keymap 1207,42947
(define-key coq-keymap 1208,43006
(defvar last-coq-error-location 1216,43137
(defun coq-get-last-error-location 1225,43536
(defun coq-highlight-error 1272,45874
(defvar coq-allow-highlight-error 1307,47161
(defun coq-decide-highlight-error 1314,47488
(defun coq-highlight-error-hook 1318,47610
(defun first-word-of-buffer 1329,48003
(defun coq-show-first-goal 1337,48206
(defvar coq-modeline-string2 1354,48901
(defvar coq-modeline-string1 1355,48945
(defvar coq-modeline-string0 1356,48988
(defun coq-build-subgoals-string 1357,49033
(defun coq-update-minor-mode-alist 1362,49199
(defun is-not-split-vertic 1388,50270
(defun optim-resp-windows 1397,50709

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 18,369
(defun coq-insert-coq-prog-name 76,2897
(defun coq-read-directory 87,3370
(defun coq-extract-directories-from-args 111,4473
(defun coq-ask-prog-args 126,5025
(defun coq-ask-prog-name 148,6089
(defun coq-ask-insert-coq-prog-name 166,6844

coq/coq-syntax.el,2428
(defcustom coq-prog-name 18,558
(defcustom coq-user-tactics-db 38,1340
(defcustom coq-user-commands-db 55,1853
(defcustom coq-user-tacticals-db 71,2372
(defcustom coq-user-solve-tactics-db 87,2893
(defcustom coq-user-reserved-db 105,3414
(defvar coq-tactics-db123,3945
(defvar coq-solve-tactics-db278,12012
(defvar coq-tacticals-db302,12858
(defvar coq-decl-db326,13744
(defvar coq-defn-db348,14961
(defvar coq-goal-starters-db401,18945
(defvar coq-other-commands-db428,20500
(defvar coq-commands-db552,29694
(defvar coq-terms-db559,29914
(defun coq-count-match 623,32563
(defun coq-module-opening-p 639,33292
(defun coq-section-command-p 650,33703
(defun coq-goal-command-str-p 654,33800
(defun coq-goal-command-p 681,34902
(defvar coq-keywords-save-strict690,35185
(defvar coq-keywords-save699,35298
(defun coq-save-command-p 703,35376
(defvar coq-keywords-kill-goal712,35670
(defvar coq-keywords-state-changing-misc-commands716,35760
(defvar coq-keywords-goal719,35885
(defvar coq-keywords-decl722,35968
(defvar coq-keywords-defn725,36042
(defvar coq-keywords-state-changing-commands729,36117
(defvar coq-keywords-state-preserving-commands738,36377
(defvar coq-keywords-commands743,36593
(defvar coq-solve-tactics748,36741
(defvar coq-tacticals752,36862
(defvar coq-reserved758,37001
(defvar coq-state-changing-tactics769,37329
(defvar coq-state-preserving-tactics772,37438
(defvar coq-tactics776,37552
(defvar coq-retractable-instruct779,37641
(defvar coq-non-retractable-instruct782,37751
(defvar coq-keywords786,37879
(defvar coq-symbols793,38046
(defvar coq-error-regexp 812,38259
(defvar coq-id 815,38487
(defvar coq-id-shy 816,38512
(defvar coq-ids 818,38566
(defun coq-first-abstr-regexp 820,38607
(defcustom coq-variable-highlight-enable 823,38702
(defvar coq-font-lock-terms829,38829
(defconst coq-save-command-regexp-strict850,39828
(defconst coq-save-command-regexp854,39994
(defconst coq-save-with-hole-regexp859,40147
(defconst coq-goal-command-regexp863,40305
(defconst coq-goal-with-hole-regexp866,40405
(defconst coq-decl-with-hole-regexp870,40537
(defconst coq-defn-with-hole-regexp877,40785
(defconst coq-with-with-hole-regexp887,41073
(defconst coq-require-command-regexp894,41366
(defvar coq-font-lock-keywords-1902,41591
(defvar coq-font-lock-keywords 929,42920
(defun coq-init-syntax-table 931,42978
(defconst coq-generic-expression960,43876

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 54,1805
(defcustom isabelledemo-web-page59,1927
(defun demoisa-config 70,2157
(defun demoisa-shell-config 91,2949
(define-derived-mode demoisa-mode 116,3878
(define-derived-mode demoisa-shell-mode 121,4001
(define-derived-mode demoisa-response-mode 126,4144
(define-derived-mode demoisa-goals-mode 130,4271

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,776
(defcustom isabelle-web-page30,904
(defcustom isa-isabelle-command39,1121
(defvar isabelle-not-found 57,1803
(defun isa-set-isabelle-command 60,1918
(defun isa-shell-command-to-string 83,2936
(defun isa-getenv 89,3160
(defcustom isabelle-program-name-override 109,3852
(defvar isabelle-prog-name 120,4198
(defun isa-tool-list-logics 123,4308
(defcustom isabelle-logics-available 130,4547
(defcustom isabelle-chosen-logic 140,4884
(defvar isabelle-chosen-logic-prev 156,5468
(defun isabelle-hack-local-variables-function 159,5588
(defun isabelle-set-prog-name 171,6027
(defun isabelle-choose-logic 196,7217
(defun isa-view-doc 215,7979
(defun isa-tool-list-docs 224,8244
(defconst isabelle-verbatim-regexp 242,8967
(defun isabelle-verbatim 245,9109
(defcustom isabelle-refresh-logics 252,9270
(defvar isabelle-docs-menu260,9598
(defvar isabelle-logics-menu-entries 267,9883
(defun isabelle-logics-menu-calculate 270,9956
(defvar isabelle-time-to-refresh-logics 291,10598
(defun isabelle-logics-menu-refresh 295,10693
(defun isabelle-menu-bar-update-logics 310,11326
(defun isabelle-load-isar-keywords 326,11955
(defun isabelle-create-span-menu 347,12683
(defun isabelle-xml-sml-escapes 363,13125
(defun isabelle-process-pgip 366,13226

isar/isar.el,1610
(defcustom isar-keywords-name 37,884
(defpgdefault completion-table 54,1402
(defcustom isar-web-page56,1455
(defun isar-strip-terminators 70,1805
(defun isar-markup-ml 83,2182
(defun isar-mode-config-set-variables 88,2317
(defun isar-shell-mode-config-set-variables 159,5303
(defpacustom use-find-theorems-form 240,8437
(defun isar-set-proof-find-theorems-command 245,8603
(defpacustom use-linear-undo 251,8787
(defun isar-set-undo-commands 255,8912
(defun isar-configure-from-settings 266,9355
(defun isar-remove-file 274,9502
(defun isar-shell-compute-new-files-list 284,9857
(define-derived-mode isar-shell-mode 302,10429
(define-derived-mode isar-response-mode 307,10552
(define-derived-mode isar-goals-mode 312,10680
(define-derived-mode isar-mode 317,10801
(defpgdefault menu-entries374,12823
(defalias 'isar-set-command isar-set-command
404,13980
(defpgdefault help-menu-entries 406,14036
(defun isar-count-undos 409,14112
(defun isar-find-and-forget 435,15087
(defun isar-goal-command-p 475,16614
(defun isar-global-save-command-p 480,16791
(defvar isar-current-goal 501,17575
(defun isar-state-preserving-p 504,17641
(defvar isar-shell-current-line-width 529,18838
(defun isar-shell-adjust-line-width 534,19030
(defun isar-string-wrapping 558,19801
(defun isar-positions-of 567,19998
(defun isar-command-wrapping 591,20702
(defcustom isar-wrap-commands-singly 600,21046
(defun isar-preprocessing 606,21242
(defun isar-mode-config 625,21869
(defun isar-shell-mode-config 636,22427
(defun isar-response-mode-config 646,22776
(defun isar-goals-mode-config 656,23111

isar/isar-find-theorems.el,778
(defun isar-find-theorems-minibuffer 18,713
(defun isar-find-theorems-form 32,1332
(defvar isar-find-theorems-data 74,3132
(defvar isar-find-theorems-widget-number 88,3467
(defvar isar-find-theorems-widget-pattern 91,3565
(defvar isar-find-theorems-widget-intro 94,3657
(defvar isar-find-theorems-widget-elim 97,3743
(defvar isar-find-theorems-widget-dest 100,3827
(defvar isar-find-theorems-widget-name 103,3911
(defvar isar-find-theorems-widget-simp 106,3998
(defun isar-find-theorems-create-searchform111,4144
(defun isar-find-theorems-create-help 251,8687
(defun isar-find-theorems-submit-searchform294,10859
(defun isar-find-theorems-parse-criteria 372,13229
(defun isar-find-theorems-parse-number 465,16210
(defun isar-find-theorems-filter-empty 475,16487

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,3703
(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-keywords-outline124,3061
(defconst isar-keywords-fume127,3126
(defconst isar-keywords-indent-open134,3316
(defconst isar-keywords-indent-close140,3479
(defconst isar-keywords-indent-enclose144,3577
(defun isar-regexp-simple-alt 153,3771
(defun isar-ids-to-regexp 173,4531
(defconst isar-ext-first 207,5916
(defconst isar-ext-rest 208,5983
(defconst isar-long-id-stuff 210,6055
(defconst isar-id 211,6129
(defconst isar-idx 212,6199
(defconst isar-string 214,6258
(defconst isar-any-command-regexp216,6318
(defconst isar-name-regexp220,6452
(defconst isar-improper-regexp226,6747
(defconst isar-save-command-regexp230,6895
(defconst isar-global-save-command-regexp233,6996
(defconst isar-goal-command-regexp236,7110
(defconst isar-local-goal-command-regexp239,7218
(defconst isar-comment-start 242,7331
(defconst isar-comment-end 243,7366
(defconst isar-comment-start-regexp 244,7399
(defconst isar-comment-end-regexp 245,7470
(defconst isar-string-start-regexp 247,7538
(defconst isar-string-end-regexp 248,7590
(defun isar-syntactic-context 250,7641
(defconst isar-antiq-regexp265,8036
(defconst isar-nesting-regexp271,8187
(defun isar-nesting 274,8285
(defun isar-match-nesting 286,8678
(defface isabelle-class-name-face298,9009
(defface isabelle-tfree-name-face306,9192
(defface isabelle-tvar-name-face314,9381
(defface isabelle-free-name-face322,9569
(defface isabelle-bound-name-face330,9753
(defface isabelle-var-name-face338,9940
(defconst isabelle-class-name-face 346,10127
(defconst isabelle-tfree-name-face 347,10189
(defconst isabelle-tvar-name-face 348,10251
(defconst isabelle-free-name-face 349,10312
(defconst isabelle-bound-name-face 350,10373
(defconst isabelle-var-name-face 351,10435
(defvar isar-font-lock-keywords-1354,10497
(defun isar-output-flkprops 372,11505
(defun isar-output-flk 378,11757
(defvar isar-output-font-lock-keywords-1381,11866
(defun isar-strip-output-markup 417,13289
(defconst isar-shell-font-lock-keywords421,13425
(defvar isar-goals-font-lock-keywords424,13509
(defconst isar-linear-undo 458,14188
(defconst isar-undo 460,14231
(defun isar-remove 462,14274
(defun isar-undos 465,14349
(defun isar-cannot-undo 470,14510
(defconst isar-undo-commands473,14580
(defconst isar-theory-start-regexp481,14717
(defconst isar-end-regexp487,14875
(defconst isar-undo-fail-regexp491,14976
(defconst isar-undo-skip-regexp495,15080
(defconst isar-undo-ignore-regexp498,15201
(defconst isar-undo-remove-regexp501,15266
(defconst isar-any-entity-regexp509,15441
(defconst isar-named-entity-regexp514,15614
(defconst isar-unnamed-entity-regexp519,15777
(defconst isar-next-entity-regexps522,15879
(defconst isar-generic-expression530,16183
(defconst isar-indent-any-regexp541,16416
(defconst isar-indent-inner-regexp543,16509
(defconst isar-indent-enclose-regexp545,16575
(defconst isar-indent-open-regexp547,16691
(defconst isar-indent-close-regexp549,16801
(defconst isar-outline-regexp555,16938
(defconst isar-outline-heading-end-regexp 559,17091

isar/isar-unicode-tokens.el,1289
(defgroup isabelle-tokens 26,636
(defun isar-set-and-restart-tokens 31,776
(defconst isar-control-region-format-regexp44,1129
(defconst isar-control-char-format-regexp47,1223
(defconst isar-control-char-format	50,1318
(defconst isar-control-region-format-start 51,1367
(defconst isar-control-region-format-end 52,1421
(defcustom isar-control-characters55,1477
(defcustom isar-control-regions68,1849
(defconst isar-token-format 92,2565
(defconst isar-token-variant-format-regexp96,2716
(defcustom isar-greek-letters-tokens99,2830
(defcustom isar-misc-letters-tokens139,3688
(defcustom isar-symbols-tokens151,4006
(defcustom isar-extended-symbols-tokens357,8817
(defun isar-try-char 426,10472
(defcustom isar-symbols-tokens-fallbacks430,10616
(defcustom isar-bold-nums-tokens457,11546
(defun isar-map-letters 473,11935
(defconst isar-script-letters-tokens479,12083
(defconst isar-roman-letters-tokens484,12221
(defconst isar-fraktur-letters-tokens489,12357
(defcustom isar-token-symbol-map 494,12499
(defcustom isar-user-tokens 510,12968
(defun isar-init-token-symbol-map 517,13205
(defcustom isar-symbol-shortcuts540,13760
(defcustom isar-shortcut-alist 613,15986
(defun isar-init-shortcut-alists 621,16245
(defconst isar-tokens-customizable-variables642,16908

lclam/lclam.el,524
(defcustom lclam-prog-name 15,373
(defcustom lclam-web-page21,521
(defun lclam-config 32,751
(defun lclam-shell-config 54,1542
(define-derived-mode lclam-proofscript-mode 73,2157
(define-derived-mode lclam-shell-mode 78,2280
(define-derived-mode lclam-response-mode 83,2414
(define-derived-mode lclam-goals-mode 87,2537
(defun lclam-mode 95,2765
(define-derived-mode thy-mode 132,3611
(defvar thy-mode-map 135,3709
(defun thy-add-menus 137,3736
(defun process-thy-file 176,5217
(defun update-thy-only 182,5418

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,4953
(defun lego-count-undos 173,5379
(defun lego-goal-command-p 193,6197
(defun lego-find-and-forget 198,6368
(defun lego-goal-hyp 240,8184
(defun lego-state-preserving-p 249,8381
(defvar lego-shell-current-line-width 265,9084
(defun lego-shell-adjust-line-width 273,9391
(defun lego-mode-config 292,10128
(defun lego-equal-module-filename 360,12177
(defun lego-shell-compute-new-files-list 366,12452
(defun lego-shell-mode-config 376,12835
(defun lego-goals-mode-config 422,14488

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,597
(defcustom phox-prog-name 32,916
(defcustom phox-sym-lock-enabled 37,1018
(defcustom phox-web-page43,1127
(defcustom phox-doc-dir49,1277
(defcustom phox-lib-dir55,1424
(defcustom phox-tags-program61,1567
(defcustom phox-tags-doc67,1746
(defcustom phox-etags73,1883
(defpgdefault menu-entries94,2333
(defun phox-config 108,2526
(defun phox-shell-config 152,4450
(define-derived-mode phox-mode 176,5312
(define-derived-mode phox-shell-mode 192,5775
(define-derived-mode phox-response-mode 197,5903
(define-derived-mode phox-goals-mode 207,6264
(defpgdefault completion-table230,7050

phox/phox-extraction.el,383
(defvar phox-prog-orig 17,605
(defun phox-prog-flags-modify(19,673
(defun phox-prog-flags-extract(48,1474
(defun phox-prog-flags-erase(59,1764
(defun phox-toggle-extraction(67,1960
(defun phox-compile-theorem(79,2362
(defun phox-compile-theorem-on-cursor(85,2587
(defun phox-output 101,3065
(defun phox-output-theorem 111,3277
(defun phox-output-theorem-on-cursor(118,3576

phox/phox-font.el,123
(defconst phox-font-lock-keywords6,282
(defconst phox-sym-lock-keywords-table65,2399
(defun phox-sym-lock-start 88,2973

phox/phox-fun.el,678
(defun phox-init-syntax-table 67,2384
(defvar phox-top-keywords83,2856
(defvar phox-proof-keywords131,3311
(defun phox-find-and-forget 172,3661
(defun phox-assert-next-command-interactive 251,6059
(defun phox-depend-theorem(269,6863
(defun phox-eshow-extlist(278,7152
(defun phox-flag-name(292,7749
(defun phox-path(303,8051
(defun phox-print-expression(314,8287
(defun phox-print-sort-expression(327,8743
(defun phox-priority-symbols-list(338,9055
(defun phox-search-string(350,9427
(defun phox-constraints(365,9952
(defun phox-goals(376,10208
(defvar phox-state-menu388,10417
(defun phox-delete-symbol(413,11407
(defun phox-delete-symbol-on-cursor(419,11615

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,70
(defun phox-outline-level(34,1143
(defun phox-setup-outline 48,1617

phox/phox-pbrpm.el,512
(defun phox-pbrpm-left-paren-p 27,1188
(defun phox-pbrpm-right-paren-p 34,1391
(defun phox-pbrpm-menu-from-string 42,1595
(defun phox-pbrpm-rename-in-cmd 51,1927
(defun phox-pbrpm-get-region-name 84,3175
(defun  phox-pbrpm-escape-string 87,3302
(defun phox-pbrpm-generate-menu 91,3437
(defalias 'proof-pbrpm-generate-menu proof-pbrpm-generate-menu
298,10917
(defalias 'proof-pbrpm-left-paren-p proof-pbrpm-left-paren-p
299,10981
(defalias 'proof-pbrpm-right-paren-p proof-pbrpm-right-paren-p
300,11043

phox/phox-sym-lock.el,1353
(defvar phox-sym-lock-sym-count 36,1642
(defvar phox-sym-lock-ext-start 39,1712
(defvar phox-sym-lock-ext-end 41,1834
(defvar phox-sym-lock-font-size 44,1953
(defvar phox-sym-lock-keywords 49,2143
(defvar phox-sym-lock-enabled 54,2319
(defvar phox-sym-lock-color 59,2481
(defvar phox-sym-lock-mouse-face 64,2699
(defvar phox-sym-lock-mouse-face-enabled 69,2889
(defconst phox-sym-lock-with-mule 74,3079
(defun phox-sym-lock-gen-symbol 77,3163
(defun phox-sym-lock-make-symbols-atomic 85,3465
(defun phox-sym-lock-compute-font-size 112,4406
(defvar phox-sym-lock-font-name150,5825
(defun phox-sym-lock-set-foreground 192,7304
(defun phox-sym-lock-translate-char 206,7913
(defun phox-sym-lock-translate-char-or-string 214,8181
(defun phox-sym-lock-remap-face 221,8408
(defvar phox-sym-lock-clear-face241,9398
(defun phox-sym-lock 253,9819
(defun phox-sym-lock-rec 262,10223
(defun phox-sym-lock-atom-face 268,10368
(defun phox-sym-lock-pre-idle-hook-first 273,10664
(defun phox-sym-lock-pre-idle-hook-last 281,11022
(defun phox-sym-lock-enable 290,11397
(defun phox-sym-lock-disable 303,11810
(defun phox-sym-lock-mouse-face-enable 316,12228
(defun phox-sym-lock-mouse-face-disable 323,12443
(defun phox-sym-lock-font-lock-hook 330,12662
(defun font-lock-set-defaults 345,13353
(defun phox-sym-lock-patch-keywords 356,13717

phox/phox-tags.el,305
(defun phox-tags-add-table(21,766
(defun phox-tags-reset-table(30,1161
(defun phox-tags-add-doc-table(35,1271
(defun phox-tags-add-lib-table(41,1420
(defun phox-tags-add-local-table(47,1555
(defun phox-tags-create-local-table(53,1738
(defun phox-complete-tag(64,1988
(defvar phox-tags-menu71,2097

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 572,19569
(defun plastic-send-one-undo 579,19738
(defun plastic-minibuf-cmd 589,20044
(defun plastic-minibuf 601,20516
(defun plastic-synchro 608,20722
(defun plastic-send-minibuf 613,20863
(defun plastic-had-error 621,21171
(defun plastic-reset-error 625,21346
(defun plastic-call-if-no-error 628,21485
(defun plastic-show-shell 633,21689
(define-key plastic-keymap 638,21817
(define-key plastic-keymap 639,21878
(define-key plastic-keymap 640,21939
(define-key plastic-keymap 641,21999
(define-key plastic-keymap 642,22058
(define-key plastic-keymap 643,22117
(defalias 'proof-toolbar-command proof-toolbar-command
653,22366
(defalias 'proof-minibuffer-cmd proof-minibuffer-cmd
654,22417

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,1805
(defvar pg-pbrpm-use-buffer-menu 31,742
(defvar pg-pbrpm-start-goal-regexp 34,864
(defvar pg-pbrpm-start-goal-regexp-par-num 38,1021
(defvar pg-pbrpm-end-goal-regexp 41,1144
(defvar pg-pbrpm-start-hyp-regexp 45,1296
(defvar pg-pbrpm-start-hyp-regexp-par-num 49,1457
(defvar pg-pbrpm-start-concl-regexp 53,1664
(defvar pg-pbrpm-auto-select-regexp 57,1828
(defvar pg-pbrpm-buffer-menu 64,1989
(defvar pg-pbrpm-spans 65,2023
(defvar pg-pbrpm-goal-description 66,2051
(defvar pg-pbrpm-windows-dialog-bug 67,2090
(defvar pbrpm-menu-desc 68,2131
(defun pg-pbrpm-erase-buffer-menu 70,2161
(defun pg-pbrpm-menu-change-hook 77,2345
(defun pg-pbrpm-create-reset-buffer-menu 95,2920
(defun pg-pbrpm-analyse-goal-buffer 114,3762
(defun pg-pbrpm-button-action 174,6160
(defun pg-pbrpm-exists 181,6386
(defun pg-pbrpm-eliminate-id 185,6498
(defun pg-pbrpm-build-menu 193,6744
(defun pg-pbrpm-setup-span 256,9064
(defun pg-pbrpm-run-command 316,11379
(defun pg-pbrpm-get-pos-info 345,12689
(defun pg-pbrpm-get-region-info 387,13988
(defun pg-pbrpm-auto-select-around-point 398,14400
(defun pg-pbrpm-translate-position 413,14924
(defun pg-pbrpm-process-click 421,15181
(defvar pg-pbrpm-remember-region-selected-region 441,16206
(defvar pg-pbrpm-regions-list 442,16260
(defun pg-pbrpm-erase-regions-list 444,16296
(defun pg-pbrpm-filter-regions-list 453,16604
(defface pg-pbrpm-multiple-selection-face460,16867
(defface pg-pbrpm-menu-input-face468,17069
(defun pg-pbrpm-do-remember-region 476,17259
(defun pg-pbrpm-remember-region-drag-up-hook 497,18107
(defun pg-pbrpm-remember-region-click-hook 501,18278
(defun pg-pbrpm-remember-region 506,18463
(defun pg-pbrpm-process-region 520,19177
(defun pg-pbrpm-process-regions-list 538,19906
(defun pg-pbrpm-region-expression 542,20089

generic/pg-pgip.el,2931
(defalias 'pg-pgip-debug pg-pgip-debug
39,1033
(defalias 'pg-pgip-error pg-pgip-error
40,1074
(defalias 'pg-pgip-warning pg-pgip-warning
41,1109
(defconst pg-pgip-version-supported 43,1159
(defun pg-pgip-process-packet 47,1265
(defvar pg-pgip-last-seen-id 57,1833
(defvar pg-pgip-last-seen-seq 58,1867
(defun pg-pgip-process-pgip 60,1903
(defun pg-pgip-process-msg 79,2834
(defvar pg-pgip-post-process-functions93,3404
(defun pg-pgip-post-process 103,3892
(defun pg-pgip-process-askpgip 119,4502
(defun pg-pgip-process-usespgip 125,4706
(defun pg-pgip-process-usespgml 129,4870
(defun pg-pgip-process-pgmlconfig 133,5034
(defun pg-pgip-process-proverinfo 149,5651
(defun pg-pgip-process-hasprefs 166,6316
(defun pg-pgip-haspref 180,6948
(defun pg-pgip-process-prefval 197,7650
(defun pg-pgip-process-guiconfig 224,8358
(defvar proof-assistant-idtables 231,8475
(defun pg-pgip-process-ids 234,8592
(defun pg-complete-idtable-symbol 260,9664
(defalias 'pg-pgip-process-setids pg-pgip-process-setids
265,9756
(defalias 'pg-pgip-process-addids pg-pgip-process-addids
266,9812
(defalias 'pg-pgip-process-delids pg-pgip-process-delids
267,9868
(defun pg-pgip-process-idvalue 270,9926
(defun pg-pgip-process-menuadd 282,10272
(defun pg-pgip-process-menudel 285,10315
(defun pg-pgip-process-ready 294,10547
(defun pg-pgip-process-cleardisplay 297,10588
(defun pg-pgip-process-proofstate 311,11045
(defun pg-pgip-process-normalresponse 315,11122
(defun pg-pgip-process-errorresponse 319,11252
(defun pg-pgip-process-scriptinsert 323,11381
(defun pg-pgip-process-metainforesponse 328,11515
(defun pg-pgip-file-of-url 337,11755
(defun pg-pgip-process-informfileloaded 342,11890
(defun pg-pgip-process-informfileretracted 348,12122
(defun pg-pgip-process-brokerstatus 361,12569
(defun pg-pgip-process-proveravailmsg 364,12617
(defun pg-pgip-process-newprovermsg 367,12667
(defun pg-pgip-process-proverstatusmsg 370,12715
(defvar pg-pgip-srcids 379,12961
(defun pg-pgip-process-newfile 383,13068
(defun pg-pgip-process-filestatus 399,13650
(defun pg-pgip-process-newobj 419,14304
(defun pg-pgip-process-delobj 422,14346
(defun pg-pgip-process-objectstatus 425,14388
(defun pg-pgip-process-parsescript 439,14740
(defun pg-pgip-get-pgiptype 462,15614
(defun pg-pgip-default-for 482,16406
(defun pg-pgip-subst-for 495,16801
(defun pg-pgip-interpret-value 507,17144
(defun pg-pgip-interpret-choice 525,17825
(defun pg-pgip-string-of-command 556,18842
(defconst pg-pgip-id573,19603
(defvar pg-pgip-refseq 579,19883
(defvar pg-pgip-refid 581,19980
(defvar pg-pgip-seq 584,20072
(defun pg-pgip-assemble-packet 586,20136
(defun pg-pgip-issue 604,20947
(defun pg-pgip-maybe-askpgip 621,21559
(defun pg-pgip-askprefs 627,21750
(defun pg-pgip-askids 631,21864
(defun pg-pgip-reset 644,22152
(defconst pg-pgip-start-element-regexp 675,22850
(defconst pg-pgip-end-element-regexp 676,22902

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,3435
(defun proof-script-next-command-advance 35,887
(defun proof-script-new-command-advance 48,1366
(defun proof-maybe-follow-locked-end 91,3108
(defun proof-goto-command-start 118,3937
(defun proof-goto-command-end 141,4877
(defun proof-goto-point 164,5402
(defun proof-assert-next-command-interactive 178,5836
(defun proof-assert-until-point-interactive 191,6361
(defun proof-process-buffer 197,6591
(defun proof-undo-last-successful-command 212,6968
(defun proof-undo-and-delete-last-successful-command 217,7130
(defun proof-undo-last-successful-command-1 230,7684
(defun proof-retract-buffer 247,8296
(defun proof-retract-current-goal 256,8580
(defun proof-mouse-goto-point 275,9100
(defvar proof-minibuffer-history 290,9376
(defun proof-minibuffer-cmd 293,9471
(defun proof-frob-locked-end 337,11093
(defmacro proof-if-setting-configured 398,13017
(defmacro proof-define-assistant-command 406,13286
(defmacro proof-define-assistant-command-witharg 419,13741
(defun proof-issue-new-command 439,14563
(defun proof-cd-sync 485,16060
(defun proof-electric-terminator-enable 539,17780
(defun proof-process-electric-terminator 547,18070
(defun proof-electric-terminator 582,19409
(defun proof-add-completions 604,20055
(defun proof-script-complete 629,20962
(defun pg-copy-span-contents 643,21271
(defun pg-numth-span-higher-or-lower 660,21829
(defun pg-control-span-of 686,22575
(defun pg-move-span-contents 692,22779
(defun pg-fixup-children-spans 744,24955
(defun pg-move-region-down 754,25212
(defun pg-move-region-up 763,25505
(defun proof-forward-command 793,26333
(defun proof-backward-command 814,27054
(defun pg-pos-for-event 836,27398
(defun pg-span-for-event 842,27619
(defun pg-span-context-menu 846,27763
(defun pg-toggle-visibility 861,28218
(defun pg-create-in-span-context-menu 871,28540
(defun pg-span-undo 901,29749
(defun pg-goals-buffers-hint 947,31151
(defun pg-slow-fontify-tracing-hint 951,31333
(defun pg-response-buffers-hint 955,31504
(defun pg-jump-to-end-hint 965,31866
(defun pg-processing-complete-hint 969,31995
(defun pg-next-error-hint 986,32694
(defun pg-hint 991,32846
(defun pg-identifier-under-mouse-query 1007,33436
(defun pg-identifier-near-point-query 1016,33679
(defvar proof-query-identifier-collection 1041,34395
(defvar proof-query-identifier-history 1042,34442
(defun proof-query-identifier 1044,34487
(defun pg-identifier-query 1054,34756
(defun proof-imenu-enable 1085,35834
(defvar pg-input-ring 1116,36895
(defvar pg-input-ring-index 1119,36952
(defvar pg-stored-incomplete-input 1122,37024
(defun pg-previous-input 1125,37127
(defun pg-next-input 1139,37584
(defun pg-delete-input 1144,37706
(defun pg-get-old-input 1157,38044
(defun pg-restore-input 1171,38435
(defun pg-search-start 1182,38725
(defun pg-regexp-arg 1194,39217
(defun pg-search-arg 1206,39665
(defun pg-previous-matching-input-string-position 1220,40082
(defun pg-previous-matching-input 1247,41247
(defun pg-next-matching-input 1266,42097
(defvar pg-matching-input-from-input-string 1274,42480
(defun pg-previous-matching-input-from-input 1278,42594
(defun pg-next-matching-input-from-input 1296,43359
(defun pg-add-to-input-history 1307,43738
(defun pg-remove-from-input-history 1319,44191
(defun  pg-clear-input-ring 1330,44571
(define-key proof-mode-map 1344,44921
(define-key proof-mode-map 1345,44981
(defun pg-protected-undo 1347,45053

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 636,20899

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,7858
(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,26459
(defcustom proof-arbitrary-undo-positions 689,26796
(defcustom proof-state-preserving-p 703,27376
(defcustom proof-activate-scripting-hook 713,27848
(defcustom proof-deactivate-scripting-hook 732,28629
(defcustom proof-script-evaluate-elisp-comment-regexp 741,28959
(defcustom proof-indent 759,29545
(defcustom proof-indent-hang 764,29652
(defcustom proof-indent-enclose-offset 769,29778
(defcustom proof-indent-open-offset 774,29920
(defcustom proof-indent-close-offset 779,30057
(defcustom proof-indent-any-regexp 784,30195
(defcustom proof-indent-inner-regexp 789,30355
(defcustom proof-indent-enclose-regexp 794,30509
(defcustom proof-indent-open-regexp 799,30663
(defcustom proof-indent-close-regexp 804,30815
(defcustom proof-script-font-lock-keywords 810,30969
(defcustom proof-script-syntax-table-entries 818,31321
(defcustom proof-script-span-context-menu-extensions 836,31717
(defgroup proof-shell 862,32475
(defcustom proof-prog-name 872,32645
(defcustom proof-shell-auto-terminate-commands 883,33065
(defcustom proof-shell-pre-sync-init-cmd 892,33466
(defcustom proof-shell-init-cmd 906,34024
(defcustom proof-shell-init-hook 918,34553
(defcustom proof-shell-restart-cmd 923,34692
(defcustom proof-shell-quit-cmd 928,34847
(defcustom proof-shell-quit-timeout 933,35014
(defcustom proof-shell-cd-cmd 943,35464
(defcustom proof-shell-start-silent-cmd 960,36135
(defcustom proof-shell-stop-silent-cmd 969,36511
(defcustom proof-shell-silent-threshold 978,36846
(defcustom  proof-shell-inform-file-processed-cmd 986,37180
(defcustom  proof-shell-inform-file-retracted-cmd 1007,38108
(defcustom proof-auto-multiple-files 1035,39380
(defcustom proof-cannot-reopen-processed-files 1050,40101
(defcustom proof-shell-require-command-regexp 1064,40767
(defcustom proof-done-advancing-require-function 1075,41229
(defcustom proof-shell-annotated-prompt-regexp 1087,41589
(defcustom proof-shell-error-regexp 1102,42154
(defcustom proof-shell-truncate-before-error 1122,42956
(defcustom pg-next-error-regexp 1136,43495
(defcustom pg-next-error-filename-regexp 1151,44104
(defcustom pg-next-error-extract-filename 1175,45137
(defcustom proof-shell-interrupt-regexp 1182,45380
(defcustom proof-shell-proof-completed-regexp 1196,45975
(defcustom proof-shell-clear-response-regexp 1209,46483
(defcustom proof-shell-clear-goals-regexp 1221,46935
(defcustom proof-shell-start-goals-regexp 1233,47381
(defcustom proof-shell-end-goals-regexp 1241,47748
(defcustom proof-shell-eager-annotation-start 1255,48323
(defcustom proof-shell-eager-annotation-start-length 1278,49342
(defcustom proof-shell-eager-annotation-end 1289,49768
(defcustom proof-shell-strip-output-markup 1305,50443
(defcustom proof-shell-assumption-regexp 1314,50828
(defcustom proof-shell-process-file 1324,51232
(defcustom proof-shell-retract-files-regexp 1350,52310
(defcustom proof-shell-compute-new-files-list 1363,52798
(defcustom pg-special-char-regexp 1378,53367
(defcustom proof-shell-set-elisp-variable-regexp 1383,53511
(defcustom proof-shell-match-pgip-cmd 1421,55177
(defcustom proof-shell-issue-pgip-cmd 1435,55659
(defcustom proof-use-pgip-askprefs 1440,55824
(defcustom proof-shell-query-dependencies-cmd 1448,56171
(defcustom proof-shell-theorem-dependency-list-regexp 1455,56431
(defcustom proof-shell-theorem-dependency-list-split 1471,57091
(defcustom proof-shell-show-dependency-cmd 1480,57514
(defcustom proof-shell-trace-output-regexp 1502,58420
(defcustom proof-shell-thms-output-regexp 1520,59015
(defcustom proof-tokens-activate-command 1533,59398
(defcustom proof-tokens-deactivate-command 1540,59638
(defcustom proof-tokens-extra-modes 1547,59883
(defcustom proof-shell-unicode 1562,60388
(defcustom proof-shell-filename-escapes 1571,60778
(defcustom proof-shell-process-connection-type1588,61458
(defcustom proof-shell-strip-crs-from-input 1611,62462
(defcustom proof-shell-strip-crs-from-output 1623,62945
(defcustom proof-shell-insert-hook 1631,63313
(defcustom proof-shell-handle-delayed-output-hook1669,65173
(defcustom proof-shell-handle-error-or-interrupt-hook1675,65388
(defcustom proof-shell-pre-interrupt-hook1693,66134
(defcustom proof-shell-handle-output-system-specific 1701,66405
(defcustom proof-state-change-hook 1724,67381
(defcustom proof-shell-syntax-table-entries 1734,67774
(defgroup proof-goals 1752,68145
(defcustom pg-subterm-first-special-char 1757,68266
(defcustom pg-subterm-anns-use-stack 1765,68578
(defcustom pg-goals-change-goal 1774,68877
(defcustom pbp-goal-command 1779,68993
(defcustom pbp-hyp-command 1784,69149
(defcustom pg-subterm-help-cmd 1789,69311
(defcustom pg-goals-error-regexp 1796,69547
(defcustom proof-shell-result-start 1801,69707
(defcustom proof-shell-result-end 1807,69941
(defcustom pg-subterm-start-char 1813,70154
(defcustom pg-subterm-sep-char 1827,70739
(defcustom pg-subterm-end-char 1833,70918
(defcustom pg-topterm-regexp 1839,71075
(defcustom proof-goals-font-lock-keywords 1854,71675
(defcustom proof-response-font-lock-keywords 1862,72034
(defcustom proof-shell-font-lock-keywords 1870,72396
(defcustom pg-before-fontify-output-hook 1881,72911
(defcustom pg-after-fontify-output-hook 1889,73272

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,936
(defun proof-maths-menu-enable 44,1387

generic/proof-menu.el,2073
(defvar proof-display-some-buffers-count 29,665
(defun proof-display-some-buffers 31,710
(defun proof-menu-define-keys 90,2906
(defun proof-menu-define-main 149,5772
(defvar proof-menu-favourites 158,5957
(defvar proof-menu-settings 161,6064
(defun proof-menu-define-specific 165,6153
(defun proof-assistant-menu-update 208,7414
(defvar proof-help-menu222,7847
(defvar proof-show-hide-menu230,8117
(defvar proof-buffer-menu239,8430
(defun proof-retract-on-edit-toggle 302,10740
(defun proof-keep-response-history 309,10916
(defconst proof-quick-opts-menu317,11226
(defun proof-quick-opts-vars 486,18144
(defun proof-quick-opts-changed-from-defaults-p 515,19004
(defun proof-quick-opts-changed-from-saved-p 519,19109
(defun proof-quick-opts-save 530,19460
(defun proof-quick-opts-reset 535,19628
(defconst proof-config-menu547,19896
(defconst proof-advanced-menu554,20075
(defvar proof-menu567,20510
(defun proof-main-menu 576,20792
(defun proof-aux-menu 587,21058
(defun proof-menu-define-favourites-menu 603,21404
(defun proof-def-favourite 623,22053
(defvar proof-make-favourite-cmd-history 646,23027
(defvar proof-make-favourite-menu-history 649,23112
(defun proof-save-favourites 652,23198
(defun proof-del-favourite 657,23346
(defun proof-read-favourite 674,23902
(defun proof-add-favourite 698,24678
(defun proof-menu-define-settings-menu 725,25723
(defun proof-menu-entry-name 758,26844
(defun proof-menu-entry-for-setting 768,27194
(defun proof-settings-vars 787,27726
(defun proof-settings-changed-from-defaults-p 792,27903
(defun proof-settings-changed-from-saved-p 796,28009
(defun proof-settings-save 800,28112
(defun proof-settings-reset 805,28279
(defun proof-assistant-invisible-command-ifposs 810,28442
(defun proof-maybe-askprefs 832,29412
(defun proof-assistant-settings-cmd 838,29604
(defvar proof-assistant-format-table855,30259
(defun proof-assistant-format-bool 863,30627
(defun proof-assistant-format-int 866,30740
(defun proof-assistant-format-string 869,30832
(defun proof-assistant-format 872,30930

generic/proof-mmm.el,70
(defun proof-mmm-set-global 39,1466
(defun proof-mmm-enable 54,2005

generic/proof-script.el,5381
(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 136,4757
(defun proof-strict-read-only 145,5130
(defsubst proof-set-queue-endpoints 155,5508
(defun proof-set-overlay-arrow 159,5649
(defsubst proof-set-locked-endpoints 170,5987
(defsubst proof-detach-queue 175,6163
(defsubst proof-detach-locked 180,6302
(defsubst proof-set-queue-start 187,6527
(defsubst proof-set-locked-end 191,6653
(defsubst proof-set-queue-end 203,7123
(defun proof-init-segmentation 214,7420
(defun proof-colour-locked 247,8882
(defun proof-restart-buffers 258,9314
(defun proof-script-buffers-with-spans 279,10065
(defun proof-script-remove-all-spans-and-deactivate 289,10421
(defun proof-script-clear-queue-spans 293,10611
(defun proof-script-delete-spans 304,11001
(defun proof-unprocessed-begin 320,11453
(defun proof-script-end 328,11707
(defun proof-queue-or-locked-end 337,12010
(defun proof-locked-end 352,12688
(defun proof-locked-region-full-p 366,12969
(defun proof-locked-region-empty-p 375,13241
(defun proof-only-whitespace-to-locked-region-p 379,13391
(defun proof-in-locked-region-p 389,13718
(defun proof-goto-end-of-locked 401,13975
(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 418,14734
(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 429,15215
(defun proof-end-of-locked-visible-p 443,15828
(defvar pg-idioms 461,16446
(defvar pg-visibility-specs 464,16542
(defconst pg-default-invisibility-spec469,16749
(defun pg-clear-script-portions 472,16818
(defun pg-remove-script-element 479,17092
(defsubst pg-visname 484,17281
(defun pg-add-element 488,17426
(defun pg-open-invisible-span 524,19119
(defun pg-remove-element 535,19482
(defun pg-make-element-invisible 542,19752
(defun pg-make-element-visible 548,19996
(defun pg-toggle-element-visibility 552,20139
(defun pg-redisplay-for-gnuemacs 559,20426
(defun pg-show-all-portions 563,20573
(defun pg-show-all-proofs 583,21291
(defun pg-hide-all-proofs 588,21419
(defun pg-add-proof-element 593,21550
(defun pg-span-name 607,22208
(defvar pg-span-context-menu-keymap628,22908
(defun pg-last-output-displayform 635,23146
(defun pg-set-span-helphighlights 650,23709
(defun proof-complete-buffer-atomic 690,25153
(defun proof-register-possibly-new-processed-file732,27073
(defun proof-inform-prover-file-retracted 778,28910
(defun proof-auto-retract-dependencies 798,29761
(defun proof-unregister-buffer-file-name 852,32311
(defun proof-protected-process-or-retract 898,34136
(defun proof-deactivate-scripting-auto 925,35306
(defun proof-deactivate-scripting 934,35664
(defun proof-activate-scripting 1067,40920
(defun proof-toggle-active-scripting 1182,46038
(defun proof-done-advancing 1221,47283
(defun proof-done-advancing-comment 1300,50268
(defun proof-done-advancing-save 1334,51644
(defun proof-make-goalsave 1419,54856
(defun proof-get-name-from-goal 1437,55688
(defun proof-done-advancing-autosave 1457,56713
(defun proof-done-advancing-other 1522,59257
(defun proof-segment-up-to-parser 1550,60210
(defun proof-script-generic-parse-find-comment-end 1614,62293
(defun proof-script-generic-parse-cmdend 1623,62707
(defun proof-script-generic-parse-cmdstart 1648,63594
(defun proof-script-generic-parse-sexp 1711,66287
(defun proof-cmdstart-add-segment-for-cmd 1735,67219
(defun proof-segment-up-to-cmdstart 1787,69432
(defun proof-segment-up-to-cmdend 1848,71792
(defun proof-semis-to-vanillas 1920,74471
(defun proof-assert-until-point 1952,75570
(defun proof-assert-semis 1967,76163
(defun proof-retract-before-change 1975,76508
(defun proof-inside-comment 1984,76826
(defun proof-insert-pbp-command 1998,77061
(defun proof-insert-sendback-command 2012,77540
(defun proof-done-retracting 2038,78443
(defun proof-setup-retract-action 2073,79884
(defun proof-last-goal-or-goalsave 2083,80367
(defun proof-retract-target 2107,81272
(defun proof-retract-until-point-interactive 2188,84642
(defun proof-retract-until-point 2196,85027
(define-derived-mode proof-mode 2243,86862
(defun proof-script-set-visited-file-name 2280,88230
(defun proof-script-set-buffer-hooks 2302,89243
(defun proof-script-kill-buffer-fn 2310,89661
(defun proof-config-done-related 2342,90978
(defun proof-generic-goal-command-p 2410,93501
(defun proof-generic-state-preserving-p 2415,93714
(defun proof-generic-count-undos 2424,94231
(defun proof-generic-find-and-forget 2453,95269
(defconst proof-script-important-settings2506,97108
(defun proof-config-done 2521,97654
(defun proof-setup-parsing-mechanism 2589,99932
(defun proof-setup-imenu 2633,101785
(deflocal proof-segment-up-to-cache 2657,102559
(deflocal proof-segment-up-to-cache-start 2658,102600
(deflocal proof-last-edited-low-watermark 2659,102645
(defun proof-segment-up-to-using-cache 2669,103132
(defun proof-segment-cache-contents-for 2698,104280
(defun proof-script-after-change-function 2710,104649
(defun proof-script-set-after-change-functions 2722,105156

generic/proof-shell.el,3834
(defvar proof-marker 35,808
(defvar proof-action-list 38,904
(defvar proof-shell-last-goals-output 63,1842
(defvar proof-shell-last-response-output 66,1922
(defvar proof-shell-delayed-output-start 69,2009
(defvar proof-shell-delayed-output-end 73,2191
(defvar proof-shell-delayed-output-flags 77,2371
(defcustom proof-shell-active-scripting-indicator86,2567
(defun proof-shell-ready-prover 134,3881
(defsubst proof-shell-live-buffer 148,4420
(defun proof-shell-available-p 155,4659
(defun proof-grab-lock 161,4881
(defun proof-release-lock 172,5379
(defcustom proof-shell-fiddle-frames 184,5599
(defun proof-shell-set-text-representation 190,5821
(defun proof-shell-start 201,6282
(defvar proof-shell-kill-function-hooks 386,12548
(defun proof-shell-kill-function 389,12646
(defun proof-shell-clear-state 478,16450
(defun proof-shell-exit 493,16893
(defun proof-shell-bail-out 505,17338
(defun proof-shell-restart 514,17815
(defvar proof-shell-urgent-message-marker 556,19193
(defvar proof-shell-urgent-message-scanner 559,19314
(defun proof-shell-handle-error-output 562,19440
(defsubst proof-shell-strip-output-markup 583,20202
(defun proof-shell-handle-error-or-interrupt 596,20568
(defun proof-shell-error-or-interrupt-action 632,22037
(defun proof-goals-pos 654,22816
(defun proof-pbp-focus-on-first-goal 659,23027
(defsubst proof-shell-string-match-safe 671,23443
(defun proof-shell-handle-immediate-output 675,23604
(defvar proof-shell-expecting-output 742,26168
(defvar proof-shell-interrupt-pending 746,26327
(defun proof-interrupt-process 751,26551
(defun proof-shell-insert 789,27984
(defun proof-shell-action-list-item 840,29727
(defun proof-shell-set-silent 846,29972
(defun proof-shell-start-silent-item 852,30191
(defun proof-shell-clear-silent 858,30380
(defun proof-shell-stop-silent-item 864,30602
(defun proof-shell-should-be-silent 871,30871
(defsubst proof-shell-invoke-callback 885,31458
(defsubst proof-shell-insert-action-item 891,31668
(defun proof-append-alist 895,31843
(defun proof-start-queue 953,33968
(defun proof-extend-queue 964,34317
(defun proof-shell-exec-loop 973,34696
(defun proof-shell-insert-loopback-cmd 1050,37302
(defun proof-shell-process-urgent-message 1075,38448
(defun proof-shell-process-urgent-message-default 1124,40169
(defun proof-shell-process-urgent-message-trace 1141,40801
(defun proof-shell-process-urgent-message-retract 1154,41361
(defun proof-shell-process-urgent-message-elisp 1175,42209
(defun proof-shell-process-urgent-message-thmdeps 1190,42704
(defun proof-shell-message 1204,43084
(defun proof-shell-strip-eager-annotations 1211,43336
(defvar proof-shell-minibuffer-urgent-interactive-input-history 1226,43869
(defun proof-shell-minibuffer-urgent-interactive-input 1228,43939
(defun proof-shell-filter 1244,44406
(defun proof-shell-filter-first-command 1345,47815
(defun proof-shell-process-urgent-messages 1360,48358
(defun proof-shell-filter-manage-output 1427,50823
(defsubst proof-shell-display-output-as-response 1460,52126
(defun proof-shell-handle-delayed-output 1466,52418
(defvar pg-last-tracing-output-time 1563,55885
(defconst pg-slow-mode-duration 1566,55991
(defconst pg-fast-tracing-mode-threshold 1569,56073
(defvar pg-tracing-cleanup-timer 1572,56201
(defun pg-tracing-tight-loop 1574,56240
(defun pg-finish-tracing-display 1617,57952
(defun proof-shell-wait 1635,58316
(defun proof-done-invisible 1654,59224
(defun proof-shell-invisible-command 1660,59394
(defun proof-shell-invisible-cmd-get-result 1707,60938
(defun proof-shell-invisible-command-invisible-result 1719,61374
(defun pg-insert-last-output-as-comment 1739,61875
(define-derived-mode proof-shell-mode 1758,62347
(defconst proof-shell-important-settings1800,63740
(defun proof-shell-config-done 1806,63855

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 80,2635
(defun proof-unicode-tokens-reconfigure 100,3488
(defun proof-unicode-tokens-configure-prover 126,4376
(defun proof-unicode-tokens-activate-prover 131,4557
(defun proof-unicode-tokens-deactivate-prover 138,4803

generic/proof-useropts.el,1510
(defgroup proof-user-options 21,552
(defun proof-set-value 29,731
(defcustom proof-electric-terminator-enable 62,1854
(defcustom proof-toolbar-enable 74,2386
(defcustom proof-imenu-enable 80,2559
(defcustom pg-show-hints 86,2730
(defcustom proof-shell-quiet-errors 91,2863
(defcustom proof-trace-output-slow-catchup 98,3136
(defcustom proof-strict-state-preserving 108,3633
(defcustom proof-strict-read-only 121,4242
(defcustom proof-allow-undo-in-read-only 133,4752
(defcustom proof-three-window-enable 140,5034
(defcustom proof-multiple-frames-enable 159,5784
(defcustom proof-delete-empty-windows 168,6117
(defcustom proof-shrink-windows-tofit 179,6648
(defcustom proof-auto-raise-buffers 186,6920
(defcustom proof-colour-locked 193,7155
(defcustom proof-query-file-save-when-activating-scripting201,7405
(defcustom proof-one-command-per-line217,8125
(defcustom proof-prog-name-ask224,8349
(defcustom proof-prog-name-guess230,8509
(defcustom proof-tidy-response238,8774
(defcustom proof-keep-response-history252,9237
(defcustom pg-input-ring-size 262,9625
(defcustom proof-general-debug 267,9777
(defcustom proof-use-parser-cache 278,10186
(defcustom proof-follow-mode 288,10483
(defcustom proof-auto-action-when-deactivating-scripting 312,11660
(defcustom proof-script-command-separator 335,12609
(defcustom proof-rsh-command 343,12901
(defcustom proof-disappearing-proofs 359,13451
(defcustom proof-full-annotation 364,13612
(defcustom proof-minibuffer-messages 373,13984

generic/proof-utils.el,1938
(defmacro deflocal 65,1980
(defmacro proof-with-current-buffer-if-exists 72,2218
(deflocal proof-buffer-type 78,2428
(defmacro proof-with-script-buffer 84,2708
(defmacro proof-map-buffers 95,3089
(defmacro proof-sym 100,3274
(defsubst proof-try-require 105,3435
(defun proof-save-some-buffers 118,3766
(defmacro proof-ass-sym 167,5367
(defmacro proof-ass-symv 173,5626
(defmacro proof-ass 179,5884
(defun proof-defpgcustom-fn 185,6136
(defun undefpgcustom 206,7006
(defmacro defpgcustom 212,7230
(defun proof-defpgdefault-fn 223,7641
(defmacro defpgdefault 237,8099
(defmacro defpgfun 248,8461
(defun proof-defpacustom-fn 262,8861
(defmacro defpacustom 328,11142
(defmacro proof-eval-when-ready-for-assistant 349,12089
(defun proof-file-truename 362,12480
(defun proof-files-to-buffers 366,12663
(defun proof-buffers-in-mode 374,12903
(defun pg-save-from-death 388,13353
(defun proof-define-keys 407,13970
(defun pg-remove-specials 418,14255
(defun pg-remove-specials-in-string 428,14591
(defun proof-warn-if-unset 439,14817
(defun proof-get-window-for-buffer 444,15035
(defun proof-display-and-keep-buffer 495,17343
(defun proof-clean-buffer 537,19066
(defun pg-internal-warning 553,19722
(defun proof-debug 560,19989
(defun proof-switch-to-buffer 568,20338
(defun proof-resize-window-tofit 590,21462
(defun proof-submit-bug-report 684,25308
(defun proof-deftoggle-fn 719,26665
(defmacro proof-deftoggle 734,27318
(defun proof-defintset-fn 741,27692
(defmacro proof-defintset 757,28396
(defun proof-defstringset-fn 764,28773
(defmacro proof-defstringset 777,29399
(defun proof-escape-keymap-doc 790,29855
(defmacro proof-defshortcut 794,29995
(defmacro proof-definvisible 809,30593
(defun pg-custom-save-vars 836,31520
(defun pg-custom-reset-vars 852,32164
(defun proof-locate-executable 865,32501
(defun pg-current-word-pos 880,33056
(defun proof-looking-at-syntactic-context 927,34772

lib/bufhist.el,1106
(defun bufhist-ring-update 36,1305
(defgroup bufhist 45,1627
(defcustom bufhist-ring-size 49,1708
(defvar bufhist-ring 54,1819
(defvar bufhist-ring-pos 57,1893
(defvar bufhist-lastswitch-modified-tick 60,1972
(defvar bufhist-read-only-history 63,2078
(defvar bufhist-saved-mode-line-format 66,2149
(defvar bufhist-normal-read-only 69,2252
(defun bufhist-mode-line-format-entry 72,2346
(defconst bufhist-minor-mode-map101,3420
(define-minor-mode bufhist-mode114,3897
(defun bufhist-get-buffer-contents 135,4730
(defun bufhist-restore-buffer-contents 143,5028
(defun bufhist-checkpoint 151,5315
(defun bufhist-erase-buffer 159,5684
(defun bufhist-checkpoint-and-erase 169,6028
(defun bufhist-switch-to-index 175,6214
(defun bufhist-first 214,7813
(defun bufhist-last 219,7972
(defun bufhist-prev 224,8116
(defun bufhist-next 232,8339
(defun bufhist-delete 237,8479
(defun bufhist-clear 249,9020
(defun bufhist-init 264,9415
(defun bufhist-exit 289,10348
(defun bufhist-set-readwrite 299,10612
(defun bufhist-before-change-function 314,11232
(defun bufhist-make-buttons 326,11647

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,138
(defconst pg-dev-lisp-font-lock-keywords52,1591
(defun unload-pg 79,2385
(defun profile-pg 107,3248
(defun pg-bug-references 124,3674

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/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,2723
(defun scomint-make-in-buffer 86,3063
(defun scomint-make 110,4330
(defun scomint-exec 123,5041
(defun scomint-exec-1 160,6634
(defalias 'scomint-send-string scomint-send-string
210,8764
(defun scomint-send-eof 212,8818
(defun scomint-send-input 218,8960
(defun scomint-truncate-buffer 261,10461
(defun scomint-strip-ctrl-m 274,10855
(defun scomint-output-filter 288,11418
(defun scomint-interrupt-process 360,14150

lib/span.el,1354
(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-give-warning 48,1595
(defsubst span-write-warning 53,1741
(defsubst span-lt 65,2307
(defsubst spans-at-point-prop 70,2451
(defsubst spans-at-region-prop 79,2642
(defsubst span-at 89,2908
(defsubst span-delete 93,3034
(defsubst span-mapcar-spans 100,3256
(defsubst span-mapc-spans 104,3431
(defun span-at-before 108,3602
(defsubst prev-span 125,4326
(defsubst next-span 131,4479
(defsubst span-live-p 137,4693
(defsubst span-raise 143,4859
(defsubst span-string 147,4992
(defsubst set-span-properties 152,5152
(defsubst span-find-span 158,5346
(defsubst span-at-event 166,5658
(defun fold-spans 172,5855
(defsubst span-detached-p 186,6388
(defsubst set-span-face 190,6504
(defsubst set-span-keymap 194,6602
(defsubst span-delete-spans 202,6771
(defsubst span-property-safe 206,6933
(defsubst span-set-start 210,7070
(defsubst span-set-end 214,7202

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,5231
(defvar unicode-tokens-token-symbol-map 56,1828
(defvar unicode-tokens-token-format 75,2450
(defvar unicode-tokens-token-variant-format-regexp 81,2699
(defvar unicode-tokens-shortcut-alist 95,3232
(defvar unicode-tokens-shortcut-replacement-alist 101,3509
(defvar unicode-tokens-control-region-format-regexp 109,3715
(defvar unicode-tokens-control-char-format-regexp 116,4083
(defvar unicode-tokens-control-regions 123,4444
(defvar unicode-tokens-control-characters 126,4520
(defvar unicode-tokens-control-char-format 129,4602
(defvar unicode-tokens-control-region-format-start 132,4715
(defvar unicode-tokens-control-region-format-end 135,4832
(defvar unicode-tokens-tokens-customizable-variables 138,4945
(defconst unicode-tokens-configuration-variables145,5113
(defun unicode-tokens-config 160,5512
(defun unicode-tokens-config-var 164,5657
(defun unicode-tokens-copy-configuration-variables 176,6097
(defvar unicode-tokens-token-list 204,7313
(defvar unicode-tokens-hash-table 207,7433
(defvar unicode-tokens-token-match-regexp 210,7549
(defvar unicode-tokens-uchar-hash-table 216,7832
(defvar unicode-tokens-uchar-regexp 220,8019
(defgroup unicode-tokens-faces 228,8204
(defconst unicode-tokens-font-family-alternatives238,8501
(defface unicode-tokens-symbol-font-face252,8949
(defface unicode-tokens-script-font-face270,9589
(defface unicode-tokens-fraktur-font-face275,9733
(defface unicode-tokens-serif-font-face280,9858
(defface unicode-tokens-sans-font-face285,9985
(defface unicode-tokens-highlight-face290,10107
(defconst unicode-tokens-fonts299,10469
(defconst unicode-tokens-fontsymb-properties308,10686
(define-widget 'unicode-tokens-token-symbol-map unicode-tokens-token-symbol-map
334,12132
(define-widget 'unicode-tokens-shortcut-alist unicode-tokens-shortcut-alist
352,12684
(defconst unicode-tokens-font-lock-extra-managed-props365,13015
(defun unicode-tokens-font-lock-keywords 369,13169
(defun unicode-tokens-calculate-token-match 402,14540
(defun unicode-tokens-usable-composition 432,15578
(defun unicode-tokens-help-echo 445,15957
(defvar unicode-tokens-show-symbols 449,16121
(defun unicode-tokens-interpret-composition 452,16235
(defun unicode-tokens-font-lock-compose-symbol 470,16747
(defun unicode-tokens-prepend-text-properties-in-match 500,17994
(defun unicode-tokens-prepend-text-property 514,18572
(defun unicode-tokens-show-symbols 539,19717
(defun unicode-tokens-symbs-to-props 547,20027
(defvar unicode-tokens-show-controls 567,20726
(defun unicode-tokens-show-controls 570,20817
(defun unicode-tokens-control-char 583,21402
(defun unicode-tokens-control-region 592,21841
(defun unicode-tokens-control-font-lock-keywords 603,22388
(defvar unicode-tokens-use-shortcuts 614,22712
(defun unicode-tokens-use-shortcuts 617,22815
(defun unicode-tokens-map-ordering 635,23421
(defun unicode-tokens-quail-define-rules 644,23774
(defun unicode-tokens-insert-token 667,24451
(defun unicode-tokens-annotate-region 676,24755
(defun unicode-tokens-insert-control 700,25593
(defun unicode-tokens-insert-uchar-as-token 710,26042
(defun unicode-tokens-delete-token-near-point 716,26263
(defun unicode-tokens-prev-token 730,26825
(defun unicode-tokens-rotate-token-forward 738,27122
(defun unicode-tokens-rotate-token-backward 765,28012
(defun unicode-tokens-replace-shortcut-match 770,28214
(defun unicode-tokens-replace-shortcuts 779,28584
(defun unicode-tokens-replace-unicode-match 793,29182
(defun unicode-tokens-replace-unicode 800,29483
(defun unicode-tokens-copy-token 817,30082
(define-button-type 'unicode-tokens-listunicode-tokens-list
824,30303
(defun unicode-tokens-list-tokens 830,30507
(defun unicode-tokens-list-shortcuts 869,31691
(defalias 'unicode-tokens-list-unicode-chars unicode-tokens-list-unicode-chars
887,32329
(defun unicode-tokens-encode-in-temp-buffer 889,32402
(defun unicode-tokens-encode 907,33058
(defun unicode-tokens-encode-str 913,33294
(defun unicode-tokens-copy 917,33456
(defun unicode-tokens-paste 926,33862
(defvar unicode-tokens-highlight-unicode 945,34583
(defconst unicode-tokens-unicode-highlight-patterns948,34675
(defun unicode-tokens-highlight-unicode 952,34844
(defun unicode-tokens-highlight-unicode-setkeywords 964,35307
(defun unicode-tokens-initialise 976,35676
(defvar unicode-tokens-mode-map 996,36347
(define-minor-mode unicode-tokens-mode999,36444
(defun unicode-tokens-set-font-var 1126,40688
(defun unicode-tokens-set-font-var-aux 1142,41179
(defun unicode-tokens-mouse-set-font 1167,42221
(defsubst unicode-tokens-face-font-sym 1180,42735
(defun unicode-tokens-set-font-restart 1184,42915
(defun unicode-tokens-save-fonts 1195,43225
(defun unicode-tokens-custom-save-faces 1203,43481
(define-key unicode-tokens-mode-map 1220,43937
(define-key unicode-tokens-mode-map 1222,44029
(define-key unicode-tokens-mode-map1224,44120
(define-key unicode-tokens-mode-map1226,44226
(define-key unicode-tokens-mode-map1229,44341
(define-key unicode-tokens-mode-map1231,44450
(define-key unicode-tokens-mode-map1233,44558
(define-key unicode-tokens-mode-map1235,44664
(defun unicode-tokens-customize-submenu 1243,44788
(defun unicode-tokens-define-menu 1250,45011

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
1655,62840
@node Interrupting during trace outputInterrupting during trace output
1679,63769
@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
1718,65690
@node Goals buffer commandsGoals buffer commands
1733,66202
@node Advanced Script Management and EditingAdvanced Script Management and Editing
1822,69766
@node Document centred workingDocument centred working
1854,70981
@node Visibility of completed proofsVisibility of completed proofs
1920,73085
@node Switching between proof scriptsSwitching between proof scripts
1975,75008
@node View of processed files View of processed files 
2012,76980
@node Retracting across filesRetracting across files
2072,80031
@node Asserting across filesAsserting across files
2085,80662
@node Automatic multiple file handlingAutomatic multiple file handling
2098,81228
@node Escaping script managementEscaping script management
2123,82262
@node Editing featuresEditing features
2180,84374
@node Support for other PackagesSupport for other Packages
2251,87166
@node Syntax highlightingSyntax highlighting
2283,88040
@node Unicode supportUnicode support
2312,89044
@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)
2468,95279
@node Support for outline modeSupport for outline mode
2523,97323
@node Support for completionSupport for completion
2548,98452
@node Support for tagsSupport for tags
2605,100614
@node Customizing Proof GeneralCustomizing Proof General
2657,102942
@node Basic optionsBasic options
2697,104612
@node How to customizeHow to customize
2721,105370
@node Display customizationDisplay customization
2768,107337
@node User optionsUser options
2922,113736
@node Changing facesChanging faces
3163,122214
@node Tweaking configuration settingsTweaking configuration settings
3238,124883
@node Hints and TipsHints and Tips
3295,127409
@node Adding your own keybindingsAdding your own keybindings
3314,128010
@node Using file variablesUsing file variables
3378,130597
@node Using abbreviationsUsing abbreviations
3437,132783
@node LEGO Proof GeneralLEGO Proof General
3476,134198
@node LEGO specific commandsLEGO specific commands
3517,135567
@node LEGO tagsLEGO tags
3537,136022
@node LEGO customizationsLEGO customizations
3547,136269
@node Coq Proof GeneralCoq Proof General
3579,137188
@node Coq-specific commandsCoq-specific commands
3595,137597
@node Coq-specific variablesCoq-specific variables
3617,138104
@node Editing multiple proofsEditing multiple proofs
3639,138762
@node User-loaded tacticsUser-loaded tactics
3663,139870
@node Holes featureHoles feature
3727,142344
@node Isabelle Proof GeneralIsabelle Proof General
3754,143631
@node Choosing logic and starting isabelleChoosing logic and starting isabelle
3785,144800
@node Isabelle commandsIsabelle commands
3854,147608
@node Isabelle settingsIsabelle settings
3997,151761
@node Isabelle customizationsIsabelle customizations
4011,152343
@node HOL Proof GeneralHOL Proof General
4034,152830
@node Shell Proof GeneralShell Proof General
4076,154652
@node Obtaining and InstallingObtaining and Installing
4112,156111
@node Obtaining Proof GeneralObtaining Proof General
4128,156524
@node Installing Proof General from tarballInstalling Proof General from tarball
4159,157763
@node Installing Proof General from RPM packageInstalling Proof General from RPM package
4184,158595
@node Setting the names of binariesSetting the names of binaries
4199,159003
@node Notes for syssiesNotes for syssies
4227,159943
@node Bugs and EnhancementsBugs and Enhancements
4302,162979
@node References4323,163794
@node History of Proof GeneralHistory of Proof General
4363,164817
@node Old News for 3.0Old News for 3.0
4457,168982
@node Old News for 3.1Old News for 3.1
4527,172676
@node Old News for 3.2Old News for 3.2
4553,173848
@node Old News for 3.3Old News for 3.3
4614,176851
@node Old News for 3.4Old News for 3.4
4633,177748
@node Old News for 3.5Old News for 3.5
4655,178803
@node Old News for 3.6Old News for 3.6
4659,178860
@node Old News for 3.7Old News for 3.7
4664,178960
@node Function IndexFunction Index
4708,180858
@node Variable IndexVariable Index
4712,180934
@node Keystroke IndexKeystroke Index
4716,181014
@node Concept IndexConcept Index
4720,181080

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,36812
@node Configuring undo behaviourConfiguring undo behaviour
1045,42344
@node Nested proofsNested proofs
1182,47733
@node Safe (state-preserving) commandsSafe (state-preserving) commands
1222,49359
@node Activate scripting hookActivate scripting hook
1245,50312
@node Automatic multiple filesAutomatic multiple files
1269,51182
@node Completions1291,52029
@node Proof Shell SettingsProof Shell Settings
1332,53519
@node Proof shell commandsProof shell commands
1363,54801
@node Script input to the shellScript input to the shell
1527,61845
@node Settings for matching various output from proof processSettings for matching various output from proof process
1592,64803
@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process
1706,69781
@node Hooks and other settingsHooks and other settings
1921,79658
@node Goals Buffer SettingsGoals Buffer Settings
2002,83045
@node Splash Screen SettingsSplash Screen Settings
2079,86151
@node Global ConstantsGlobal Constants
2105,86906
@node Handling Multiple FilesHandling Multiple Files
2131,87747
@node Configuring Editing SyntaxConfiguring Editing Syntax
2283,95530
@node Configuring Font LockConfiguring Font Lock
2340,97647
@node Configuring TokensConfiguring Tokens
2412,101141
@node Writing More Lisp CodeWriting More Lisp Code
2462,103261
@node Default values for generic settingsDefault values for generic settings
2479,103906
@node Adding prover-specific configurationsAdding prover-specific configurations
2509,104989
@node Useful variablesUseful variables
2552,106271
@node Useful functions and macrosUseful functions and macros
2567,106770
@node Internals of Proof GeneralInternals of Proof General
2676,110993
@node Spans2704,111889
@node Proof General site configurationProof General site configuration
2716,112211
@node Configuration variable mechanismsConfiguration variable mechanisms
2796,115256
@node Global variablesGlobal variables
2917,120700
@node Proof script modeProof script mode
2987,123248
@node Proof shell modeProof shell mode
3225,133855
@node Debugging3661,151085
@node Plans and IdeasPlans and Ideas
3704,151961
@node Proof by pointing and similar featuresProof by pointing and similar features
3725,152683
@node Granularity of atomic command sequencesGranularity of atomic command sequences
3763,154341
@node Browser mode for script files and theoriesBrowser mode for script files and theories
3808,156566
@node Demonstration InstantiationsDemonstration Instantiations
3838,157597
@node demoisa-easy.el3854,158028
@node demoisa.el3916,160220
@node Function IndexFunction Index
4070,165160
@node Variable IndexVariable Index
4074,165236
@node Concept IndexConcept Index
4083,165415

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