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,668
(defconst coq-syntax-db 23,544
(defvar coq-user-tactics-db59,1917
(defun coq-insert-from-db 69,2266
(defun coq-build-regexp-list-from-db 87,2998
(defun max-length-db 109,3981
(defun coq-build-menu-from-db-internal 121,4256
(defun coq-build-title-menu 156,5879
(defun coq-sort-menu-entries 165,6247
(defun coq-build-menu-from-db 171,6374
(defcustom coq-holes-minor-mode 193,7213
(defun coq-build-abbrev-table-from-db 199,7357
(defun filter-state-preserving 218,7995
(defun filter-state-changing 223,8149
(defface coq-solve-tactics-face230,8370
(defface coq-cheat-face239,8700
(defconst coq-solve-tactics-face 247,8948
(defconst coq-cheat-face 251,9112

coq/coq.el,5977
(defcustom coq-translate-to-v8 46,1310
(defun coq-build-prog-args 52,1490
(defcustom coq-compile-file-command 62,1786
(defcustom coq-use-makefile 70,2105
(defcustom coq-default-undo-limit 78,2328
(defconst coq-shell-init-cmd83,2456
(defcustom coq-prog-env 89,2583
(defconst coq-shell-restart-cmd 97,2833
(defvar coq-shell-prompt-pattern99,2887
(defvar coq-shell-cd 107,3191
(defvar coq-shell-proof-completed-regexp 111,3351
(defvar coq-goal-regexp114,3506
(defun coq-library-directory 121,3620
(defcustom coq-tags 128,3799
(defconst coq-interrupt-regexp 133,3949
(defcustom coq-www-home-page 138,4070
(defvar coq-outline-regexp145,4238
(defvar coq-outline-heading-end-regexp 152,4450
(defvar coq-shell-outline-regexp 154,4504
(defvar coq-shell-outline-heading-end-regexp 155,4554
(defconst coq-state-preserving-tactics-regexp161,4719
(defconst coq-state-changing-commands-regexp163,4819
(defconst coq-state-preserving-commands-regexp165,4926
(defconst coq-commands-regexp167,5037
(defvar coq-retractable-instruct-regexp169,5114
(defvar coq-non-retractable-instruct-regexp171,5204
(defun coq-set-undo-limit 205,6081
(defun build-list-id-from-string 209,6211
(defun coq-last-prompt-info 221,6709
(defun coq-last-prompt-info-safe 233,7241
(defvar coq-last-but-one-statenum 239,7498
(defvar coq-last-but-one-proofnum 245,7795
(defvar coq-last-but-one-proofstack 248,7893
(defun coq-get-span-statenum 251,8003
(defun coq-get-span-proofnum 256,8118
(defun coq-get-span-proofstack 261,8233
(defun coq-set-span-statenum 266,8377
(defun coq-get-span-goalcmd 271,8508
(defun coq-set-span-goalcmd 276,8622
(defun coq-set-span-proofnum 281,8752
(defun coq-set-span-proofstack 286,8883
(defun proof-last-locked-span 291,9043
(defun proof-clone-buffer 300,9341
(defun proof-store-buffer-win 314,9898
(defun proof-store-response-win 322,10123
(defun proof-store-goals-win 326,10252
(defun coq-set-state-infos 339,10787
(defun count-not-intersection 378,12782
(defun coq-find-and-forget 409,14032
(defvar coq-current-goal 429,14936
(defun coq-goal-hyp 432,15001
(defun coq-state-preserving-p 445,15433
(defconst notation-print-kinds-table459,15934
(defun coq-PrintScope 463,16101
(defun coq-guess-or-ask-for-string 481,16650
(defun coq-ask-do 495,17218
(defun coq-put-into-brackets 504,17603
(defun coq-put-into-quotes 508,17664
(defun coq-SearchIsos 510,17718
(defun coq-SearchConstant 516,17951
(defun coq-Searchregexp 522,18046
(defun coq-SearchRewrite 527,18182
(defun coq-SearchAbout 531,18280
(defun coq-Print 535,18418
(defun coq-About 539,18540
(defun coq-LocateConstant 543,18657
(defun coq-LocateLibrary 549,18792
(defun coq-LocateNotation 556,18943
(defun coq-Pwd 563,19147
(defun coq-Inspect 569,19279
(defun coq-PrintSection(573,19379
(defun coq-Print-implicit 577,19472
(defun coq-Check 582,19623
(defun coq-Show 587,19731
(defun coq-Compile 601,20174
(defun coq-guess-command-line 613,20492
(defpacustom use-editing-holes 652,22164
(defun coq-mode-config 662,22501
(defun coq-shell-mode-config 766,26385
(defun coq-goals-mode-config 809,28184
(defun coq-response-config 816,28428
(defpacustom print-fully-explicit 841,29253
(defpacustom print-implicit 846,29401
(defpacustom print-coercions 851,29567
(defpacustom print-match-wildcards 856,29711
(defpacustom print-elim-types 861,29891
(defpacustom printing-depth 866,30057
(defpacustom undo-depth 871,30218
(defpacustom time-commands 876,30365
(defpacustom undo-limit 880,30475
(defpacustom auto-compile-vos 885,30577
(defun coq-maybe-compile-buffer 914,31691
(defun coq-ancestors-of 950,33219
(defun coq-all-ancestors-of 973,34183
(defun coq-process-require-command 984,34530
(defun coq-included-children 989,34657
(defun coq-process-file 1010,35496
(defun coq-preprocessing 1025,36035
(defun coq-fake-constant-markup 1039,36470
(defun coq-create-span-menu 1055,37075
(defconst module-kinds-table1072,37559
(defconst modtype-kinds-table1076,37708
(defun coq-insert-section-or-module 1080,37837
(defconst reqkinds-kinds-table1103,38695
(defun coq-insert-requires 1108,38840
(defun coq-end-Section 1124,39343
(defun coq-insert-intros 1142,39921
(defun coq-insert-infoH-hook 1155,40455
(defun coq-insert-as 1160,40663
(defun coq-insert-match 1177,41366
(defun coq-insert-tactic 1209,42548
(defun coq-insert-tactical 1215,42787
(defun coq-insert-command 1221,43036
(defun coq-insert-term 1227,43280
(define-key coq-keymap 1233,43477
(define-key coq-keymap 1234,43535
(define-key coq-keymap 1235,43592
(define-key coq-keymap 1236,43661
(define-key coq-keymap 1237,43717
(define-key coq-keymap 1238,43766
(define-key coq-keymap 1239,43824
(define-key coq-keymap 1240,43884
(define-key coq-keymap 1241,43949
(define-key coq-keymap 1243,44012
(define-key coq-keymap 1244,44071
(define-key coq-keymap 1248,44196
(define-key coq-keymap 1250,44252
(define-key coq-keymap 1251,44302
(define-key coq-keymap 1252,44352
(define-key coq-keymap 1253,44408
(define-key coq-keymap 1254,44458
(define-key coq-keymap 1255,44512
(define-key coq-keymap 1256,44571
(define-key coq-goals-mode-map 1259,44632
(define-key coq-goals-mode-map 1260,44714
(define-key coq-goals-mode-map 1261,44796
(define-key coq-goals-mode-map 1262,44883
(define-key coq-goals-mode-map 1263,44965
(defvar last-coq-error-location 1272,45267
(defun coq-get-last-error-location 1281,45666
(defun coq-highlight-error 1331,48207
(defvar coq-allow-highlight-error 1362,49347
(defun coq-decide-highlight-error 1369,49673
(defun coq-highlight-error-hook 1374,49858
(defun first-word-of-buffer 1385,50251
(defun coq-show-first-goal 1393,50454
(defvar coq-modeline-string2 1410,51149
(defvar coq-modeline-string1 1411,51193
(defvar coq-modeline-string0 1412,51236
(defun coq-build-subgoals-string 1413,51281
(defun coq-update-minor-mode-alist 1418,51447
(defun is-not-split-vertic 1444,52518
(defun optim-resp-windows 1453,52958

coq/coq-indent.el,2223
(defconst coq-any-command-regexp20,368
(defconst coq-indent-inner-regexp23,459
(defconst coq-comment-start-regexp 33,813
(defconst coq-comment-end-regexp 34,856
(defconst coq-comment-start-or-end-regexp35,897
(defconst coq-indent-open-regexp37,1005
(defconst coq-indent-close-regexp42,1179
(defconst coq-indent-closepar-regexp 47,1360
(defconst coq-indent-closematch-regexp 48,1405
(defconst coq-indent-openpar-regexp 49,1476
(defconst coq-indent-openmatch-regexp 50,1520
(defconst coq-indent-any-regexp51,1600
(defconst coq-indent-kw56,1878
(defconst coq-indent-pattern-regexp 66,2332
(defun coq-indent-goal-command-p 70,2435
(defconst coq-end-command-regexp92,3486
(defun coq-search-comment-delimiter-forward 97,3638
(defun coq-search-comment-delimiter-backward 106,3968
(defun coq-skip-until-one-comment-backward 113,4242
(defun coq-skip-until-one-comment-forward 128,4949
(defun coq-looking-at-comment 139,5467
(defun coq-find-comment-start 143,5608
(defun coq-find-comment-end 154,6041
(defun coq-looking-at-syntactic-context 166,6534
(defconst coq-end-command-or-comment-regexp172,6756
(defconst coq-end-command-or-comment-start-regexp175,6865
(defun coq-find-not-in-comment-backward 179,6983
(defun coq-find-not-in-comment-forward 199,7884
(defun coq-find-command-end-backward 223,9023
(defun coq-find-command-end-forward 232,9414
(defun coq-find-command-end 241,9791
(defun coq-find-current-start 249,10123
(defun coq-find-real-start 258,10414
(defun coq-command-at-point 265,10633
(defun coq-indent-only-spaces-on-line 272,10910
(defun coq-indent-find-reg 278,11187
(defun coq-find-no-syntactic-on-line 292,11723
(defun coq-back-to-indentation-prevline 305,12196
(defun coq-find-unclosed 349,14104
(defun coq-find-at-same-level-zero 379,15400
(defun coq-find-unopened 407,16558
(defun coq-find-last-unopened 450,17992
(defun coq-end-offset 461,18389
(defun coq-indent-command-offset 486,19159
(defun coq-indent-expr-offset 533,20983
(defun coq-indent-comment-offset 649,25666
(defun coq-indent-offset 681,27115
(defun coq-indent-calculate 699,27977
(defun coq-indent-line 702,28065
(defun coq-indent-line-not-comments 712,28431
(defun coq-indent-region 722,28820

coq/coq-local-vars.el,280
(defconst coq-local-vars-doc 20,429
(defun coq-insert-coq-prog-name 78,2957
(defun coq-read-directory 89,3430
(defun coq-extract-directories-from-args 113,4533
(defun coq-ask-prog-args 128,5085
(defun coq-ask-prog-name 150,6149
(defun coq-ask-insert-coq-prog-name 168,6904

coq/coq-syntax.el,2563
(defcustom coq-prog-name 18,561
(defcustom coq-user-tactics-db 38,1343
(defcustom coq-user-commands-db 55,1856
(defcustom coq-user-tacticals-db 71,2375
(defcustom coq-user-solve-tactics-db 87,2896
(defcustom coq-user-cheat-tactics-db 103,3415
(defcustom coq-user-reserved-db 122,3961
(defvar coq-tactics-db140,4492
(defvar coq-solve-tactics-db298,12751
(defvar coq-solve-cheat-tactics-db321,13596
(defvar coq-tacticals-db333,13771
(defvar coq-decl-db357,14657
(defvar coq-defn-db380,15951
(defvar coq-goal-starters-db438,20313
(defvar coq-other-commands-db467,22070
(defvar coq-commands-db592,31283
(defvar coq-terms-db599,31503
(defun coq-count-match 663,34152
(defun coq-module-opening-p 679,34881
(defun coq-section-command-p 690,35292
(defun coq-goal-command-str-p 694,35389
(defun coq-goal-command-p 721,36491
(defvar coq-keywords-save-strict730,36774
(defvar coq-keywords-save739,36887
(defun coq-save-command-p 743,36965
(defvar coq-keywords-kill-goal752,37259
(defvar coq-keywords-state-changing-misc-commands756,37349
(defvar coq-keywords-goal759,37474
(defvar coq-keywords-decl762,37557
(defvar coq-keywords-defn765,37631
(defvar coq-keywords-state-changing-commands769,37706
(defvar coq-keywords-state-preserving-commands778,37966
(defvar coq-keywords-commands783,38182
(defvar coq-solve-tactics788,38330
(defvar coq-solve-cheat-tactics792,38451
(defvar coq-tacticals796,38596
(defvar coq-reserved802,38735
(defvar coq-state-changing-tactics813,39063
(defvar coq-state-preserving-tactics816,39172
(defvar coq-tactics820,39286
(defvar coq-retractable-instruct823,39375
(defvar coq-non-retractable-instruct826,39485
(defvar coq-keywords830,39613
(defvar coq-symbols837,39780
(defvar coq-error-regexp 856,39993
(defvar coq-id 859,40221
(defvar coq-id-shy 860,40246
(defvar coq-ids 862,40300
(defun coq-first-abstr-regexp 864,40341
(defcustom coq-variable-highlight-enable 867,40436
(defvar coq-font-lock-terms873,40563
(defconst coq-save-command-regexp-strict894,41562
(defconst coq-save-command-regexp898,41728
(defconst coq-save-with-hole-regexp903,41881
(defconst coq-goal-command-regexp907,42039
(defconst coq-goal-with-hole-regexp910,42139
(defconst coq-decl-with-hole-regexp914,42271
(defconst coq-defn-with-hole-regexp921,42519
(defconst coq-with-with-hole-regexp931,42807
(defconst coq-require-command-regexp938,43100
(defvar coq-font-lock-keywords-1946,43325
(defvar coq-font-lock-keywords 974,44727
(defun coq-init-syntax-table 976,44785
(defconst coq-generic-expression1005,45683

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-alist152,4361
(defconst coq-control-char-format-regexp241,6379
(defconst coq-control-char-format 245,6504
(defconst coq-control-characters247,6547
(defconst coq-control-region-format-regexp 251,6639
(defconst coq-control-regions253,6722

demoisa/demoisa.el,349
(defcustom isabelledemo-prog-name 56,1848
(defcustom isabelledemo-web-page61,1970
(defun demoisa-config 72,2200
(defun demoisa-shell-config 93,2992
(define-derived-mode demoisa-mode 118,3921
(define-derived-mode demoisa-shell-mode 123,4044
(define-derived-mode demoisa-response-mode 128,4187
(define-derived-mode demoisa-goals-mode 132,4314

hol98/hol98.el,121
(defvar hol98-keywords 17,419
(defvar hol98-rules 18,447
(defvar hol98-tactics 19,472
(defvar hol98-tacticals 20,499

isar/isabelle-system.el,1254
(defgroup isabelle 27,778
(defcustom isabelle-web-page31,906
(defcustom isa-isabelle-command40,1123
(defvar isabelle-not-found 58,1805
(defun isa-set-isabelle-command 61,1920
(defun isa-shell-command-to-string 84,2938
(defun isa-getenv 90,3162
(defcustom isabelle-program-name-override 110,3861
(defun isa-tool-list-logics 121,4207
(defcustom isabelle-logics-available 128,4453
(defcustom isabelle-chosen-logic 138,4790
(defvar isabelle-chosen-logic-prev 154,5374
(defun isabelle-hack-local-variables-function 157,5494
(defun isabelle-set-prog-name 169,5933
(defun isabelle-choose-logic 193,7053
(defun isa-view-doc 212,7815
(defun isa-tool-list-docs 219,8041
(defconst isabelle-verbatim-regexp 237,8771
(defun isabelle-verbatim 240,8913
(defcustom isabelle-refresh-logics 247,9074
(defvar isabelle-docs-menu255,9402
(defvar isabelle-logics-menu-entries 262,9687
(defun isabelle-logics-menu-calculate 265,9760
(defvar isabelle-time-to-refresh-logics 286,10402
(defun isabelle-logics-menu-refresh 290,10497
(defun isabelle-menu-bar-update-logics 305,11130
(defun isabelle-load-isar-keywords 321,11759
(defun isabelle-create-span-menu 342,12487
(defun isabelle-xml-sml-escapes 358,12918
(defun isabelle-process-pgip 361,13019

isar/isar.el,1595
(defcustom isar-keywords-name 40,925
(defpgdefault completion-table 56,1436
(defcustom isar-web-page58,1489
(defun isar-strip-terminators 72,1839
(defun isar-markup-ml 85,2216
(defun isar-mode-config-set-variables 90,2351
(defun isar-shell-mode-config-set-variables 155,5123
(defun isar-set-proof-find-theorems-command 236,8257
(defpacustom use-find-theorems-form 242,8441
(defun isar-set-undo-commands 247,8607
(defpacustom use-linear-undo 258,9058
(defun isar-configure-from-settings 263,9216
(defun isar-remove-file 271,9360
(defun isar-shell-compute-new-files-list 281,9715
(define-derived-mode isar-shell-mode 300,10295
(define-derived-mode isar-response-mode 305,10422
(define-derived-mode isar-goals-mode 310,10555
(define-derived-mode isar-mode 315,10681
(defpgdefault menu-entries372,12574
(defun isar-set-command 405,13874
(defpgdefault help-menu-entries 410,14004
(defun isar-count-undos 413,14080
(defun isar-find-and-forget 439,15062
(defun isar-goal-command-p 478,16519
(defun isar-global-save-command-p 483,16696
(defvar isar-current-goal 504,17480
(defun isar-state-preserving-p 507,17546
(defvar isar-shell-current-line-width 532,18395
(defun isar-shell-adjust-line-width 537,18587
(defsubst isar-string-wrapping 562,19385
(defsubst isar-positions-of 571,19579
(defcustom isar-wrap-commands-singly 577,19784
(defun isar-command-wrapping 583,19980
(defun isar-preprocessing 591,20294
(defun isar-mode-config 609,20845
(defun isar-shell-mode-config 623,21498
(defun isar-response-mode-config 633,21847
(defun isar-goals-mode-config 643,22182

isar/isar-find-theorems.el,779
(defvar isar-find-theorems-data 19,565
(defun isar-find-theorems-minibuffer 35,1039
(defun isar-find-theorems-form 49,1658
(defvar isar-find-theorems-widget-number 92,3532
(defvar isar-find-theorems-widget-pattern 95,3630
(defvar isar-find-theorems-widget-intro 98,3722
(defvar isar-find-theorems-widget-elim 101,3808
(defvar isar-find-theorems-widget-dest 104,3892
(defvar isar-find-theorems-widget-name 107,3976
(defvar isar-find-theorems-widget-simp 110,4063
(defun isar-find-theorems-create-searchform115,4209
(defun isar-find-theorems-create-help 255,8752
(defun isar-find-theorems-submit-searchform298,10924
(defun isar-find-theorems-parse-criteria 376,13294
(defun isar-find-theorems-parse-number 469,16275
(defun isar-find-theorems-filter-empty 479,16552

isar/isar-keywords.el,1052
(defconst isar-keywords-major13,481
(defconst isar-keywords-minor206,3641
(defconst isar-keywords-control262,4395
(defconst isar-keywords-diag282,4872
(defconst isar-keywords-theory-begin338,5831
(defconst isar-keywords-theory-switch341,5884
(defconst isar-keywords-theory-end344,5939
(defconst isar-keywords-theory-heading347,5987
(defconst isar-keywords-theory-decl353,6094
(defconst isar-keywords-theory-script412,7075
(defconst isar-keywords-theory-goal416,7152
(defconst isar-keywords-qed429,7369
(defconst isar-keywords-qed-block436,7455
(defconst isar-keywords-qed-global439,7502
(defconst isar-keywords-proof-heading442,7551
(defconst isar-keywords-proof-goal447,7634
(defconst isar-keywords-proof-block454,7733
(defconst isar-keywords-proof-open458,7795
(defconst isar-keywords-proof-close461,7841
(defconst isar-keywords-proof-chain464,7888
(defconst isar-keywords-proof-decl471,7991
(defconst isar-keywords-proof-asm480,8112
(defconst isar-keywords-proof-asm-goal487,8207
(defconst isar-keywords-proof-script490,8262

isar/isar-mmm.el,81
(defconst isar-start-latex-regexp24,744
(defconst isar-start-sml-regexp36,1172

isar/isar-syntax.el,3652
(defconst isar-script-syntax-table-entries18,478
(defconst isar-script-syntax-table-alist42,880
(defun isar-init-syntax-table 51,1163
(defun isar-init-output-syntax-table 59,1410
(defconst isar-keyword-begin 74,1852
(defconst isar-keyword-end 75,1890
(defconst isar-keywords-theory-enclose77,1925
(defconst isar-keywords-theory82,2063
(defconst isar-keywords-save87,2194
(defconst isar-keywords-proof-enclose92,2309
(defconst isar-keywords-proof98,2470
(defconst isar-keywords-proof-context105,2647
(defconst isar-keywords-local-goal109,2754
(defconst isar-keywords-proper113,2859
(defconst isar-keywords-improper118,2978
(defconst isar-keyword-level-alist123,3110
(defconst isar-keywords-outline 138,3581
(defconst isar-keywords-indent-open141,3657
(defconst isar-keywords-indent-close147,3820
(defconst isar-keywords-indent-enclose151,3918
(defconst isar-ext-first 160,4112
(defconst isar-ext-rest 161,4179
(defconst isar-long-id-stuff 163,4251
(defconst isar-id 164,4325
(defconst isar-idx 165,4395
(defconst isar-string 167,4454
(defun isar-ids-to-regexp 169,4514
(defconst isar-any-command-regexp201,6306
(defconst isar-name-regexp208,6679
(defconst isar-improper-regexp214,6974
(defconst isar-save-command-regexp218,7122
(defconst isar-global-save-command-regexp221,7223
(defconst isar-goal-command-regexp224,7337
(defconst isar-local-goal-command-regexp227,7445
(defconst isar-comment-start 230,7558
(defconst isar-comment-end 231,7593
(defconst isar-comment-start-regexp 232,7626
(defconst isar-comment-end-regexp 233,7697
(defconst isar-string-start-regexp 235,7765
(defconst isar-string-end-regexp 236,7817
(defun isar-syntactic-context 238,7868
(defconst isar-antiq-regexp253,8263
(defconst isar-nesting-regexp259,8414
(defun isar-nesting 262,8512
(defun isar-match-nesting 274,8905
(defface isabelle-class-name-face286,9236
(defface isabelle-tfree-name-face294,9419
(defface isabelle-tvar-name-face302,9608
(defface isabelle-free-name-face310,9796
(defface isabelle-bound-name-face318,9980
(defface isabelle-var-name-face326,10167
(defconst isabelle-class-name-face 334,10354
(defconst isabelle-tfree-name-face 335,10416
(defconst isabelle-tvar-name-face 336,10478
(defconst isabelle-free-name-face 337,10539
(defconst isabelle-bound-name-face 338,10600
(defconst isabelle-var-name-face 339,10662
(defvar isar-font-lock-keywords-1342,10724
(defun isar-output-flkprops 360,11732
(defun isar-output-flk 366,11984
(defvar isar-output-font-lock-keywords-1369,12093
(defun isar-strip-output-markup 405,13516
(defconst isar-shell-font-lock-keywords409,13652
(defvar isar-goals-font-lock-keywords412,13736
(defconst isar-linear-undo 446,14415
(defconst isar-undo 448,14458
(defconst isar-pr450,14501
(defun isar-remove 457,14659
(defun isar-undos 460,14734
(defun isar-cannot-undo 470,14968
(defconst isar-undo-commands473,15038
(defconst isar-theory-start-regexp481,15175
(defconst isar-end-regexp487,15333
(defconst isar-undo-fail-regexp491,15434
(defconst isar-undo-skip-regexp495,15538
(defconst isar-undo-ignore-regexp498,15659
(defconst isar-undo-remove-regexp501,15724
(defconst isar-keywords-imenu509,15881
(defconst isar-named-entity-regexp516,16072
(defconst isar-generic-expression521,16236
(defconst isar-indent-any-regexp532,16470
(defconst isar-indent-inner-regexp534,16563
(defconst isar-indent-enclose-regexp536,16629
(defconst isar-indent-open-regexp538,16745
(defconst isar-indent-close-regexp540,16855
(defconst isar-outline-regexp546,16992
(defconst isar-outline-heading-end-regexp 550,17145
(defconst isar-outline-heading-alist 552,17194

isar/isar-unicode-tokens.el,1363
(defgroup isabelle-tokens 25,672
(defun isar-set-and-restart-tokens 30,812
(defconst isar-control-region-format-regexp43,1165
(defconst isar-control-char-format-regexp46,1259
(defconst isar-control-char-format	52,1406
(defconst isar-control-region-format-start 53,1455
(defconst isar-control-region-format-end 54,1509
(defcustom isar-control-characters57,1565
(defcustom isar-control-regions71,1978
(defconst isar-token-format 97,2790
(defconst isar-token-variant-format-regexp101,2941
(defcustom isar-greek-letters-tokens104,3055
(defcustom isar-misc-letters-tokens144,3913
(defcustom isar-symbols-tokens156,4231
(defcustom isar-extended-symbols-tokens362,9042
(defun isar-try-char 431,10697
(defcustom isar-symbols-tokens-fallbacks435,10841
(defcustom isar-bold-nums-tokens462,11771
(defun isar-map-letters 478,12160
(defconst isar-script-letters-tokens 484,12308
(defconst isar-roman-letters-tokens 489,12462
(defconst isar-fraktur-uppercase-letters-tokens 494,12636
(defconst isar-fraktur-lowercase-letters-tokens 499,12805
(defcustom isar-token-symbol-map 504,12996
(defcustom isar-user-tokens 520,13465
(defun isar-init-token-symbol-map 527,13702
(defcustom isar-symbol-shortcuts552,14351
(defcustom isar-shortcut-alist 625,16578
(defun isar-init-shortcut-alists 633,16837
(defconst isar-tokens-customizable-variables654,17500

lclam/lclam.el,524
(defcustom lclam-prog-name 18,431
(defcustom lclam-web-page24,579
(defun lclam-config 35,809
(defun lclam-shell-config 57,1600
(define-derived-mode lclam-proofscript-mode 76,2215
(define-derived-mode lclam-shell-mode 81,2338
(define-derived-mode lclam-response-mode 86,2472
(define-derived-mode lclam-goals-mode 90,2595
(defun lclam-mode 98,2823
(define-derived-mode thy-mode 135,3669
(defvar thy-mode-map 138,3767
(defun thy-add-menus 140,3794
(defun process-thy-file 179,5275
(defun update-thy-only 185,5476

lego/lego.el,1636
(defcustom lego-tags 21,535
(defcustom lego-test-all-name 26,671
(defpgdefault help-menu-entries32,829
(defpgdefault menu-entries36,989
(defvar lego-shell-handle-output47,1290
(defconst lego-process-config55,1588
(defconst lego-pretty-set-width 66,2019
(defconst lego-interrupt-regexp 70,2161
(defcustom lego-www-home-page 75,2278
(defcustom lego-www-latest-release80,2402
(defcustom lego-www-refcard86,2577
(defcustom lego-library-www-page92,2726
(defvar lego-prog-name 101,2942
(defvar lego-shell-cd 104,3011
(defvar lego-shell-proof-completed-regexp 107,3110
(defvar lego-save-command-regexp110,3250
(defvar lego-goal-command-regexp112,3340
(defvar lego-kill-goal-command 115,3431
(defvar lego-forget-id-command 116,3474
(defvar lego-undoable-commands-regexp118,3520
(defvar lego-goal-regexp 127,3894
(defvar lego-outline-regexp129,3939
(defvar lego-outline-heading-end-regexp 135,4114
(defvar lego-shell-outline-regexp 137,4167
(defvar lego-shell-outline-heading-end-regexp 138,4219
(define-derived-mode lego-shell-mode 144,4498
(define-derived-mode lego-mode 151,4659
(define-derived-mode lego-goals-mode 162,4969
(defun lego-count-undos 173,5395
(defun lego-goal-command-p 192,6148
(defun lego-find-and-forget 197,6319
(defun lego-goal-hyp 239,8155
(defun lego-state-preserving-p 248,8352
(defvar lego-shell-current-line-width 264,9055
(defun lego-shell-adjust-line-width 272,9362
(defun lego-mode-config 291,10099
(defun lego-equal-module-filename 359,12148
(defun lego-shell-compute-new-files-list 365,12423
(defun lego-shell-mode-config 375,12806
(defun lego-goals-mode-config 422,14473

lego/lego-syntax.el,600
(defconst lego-keywords-goal 15,358
(defconst lego-keywords-save 17,401
(defconst lego-commands19,472
(defconst lego-keywords31,1030
(defconst lego-tacticals 36,1207
(defconst lego-error-regexp 39,1315
(defvar lego-id 42,1473
(defvar lego-ids 44,1500
(defconst lego-arg-list-regexp 48,1696
(defun lego-decl-defn-regexp 51,1812
(defconst lego-definiendum-alternative-regexp59,2184
(defvar lego-font-lock-terms63,2368
(defconst lego-goal-with-hole-regexp89,3221
(defconst lego-save-with-hole-regexp94,3443
(defvar lego-font-lock-keywords-199,3660
(defun lego-init-syntax-table 110,4122

phox/phox.el,555
(defcustom phox-prog-name 32,916
(defcustom phox-web-page37,1018
(defcustom phox-doc-dir43,1168
(defcustom phox-lib-dir49,1315
(defcustom phox-tags-program55,1458
(defcustom phox-tags-doc61,1637
(defcustom phox-etags67,1774
(defpgdefault menu-entries88,2224
(defun phox-config 102,2417
(defun phox-shell-config 146,4341
(define-derived-mode phox-mode 170,5203
(define-derived-mode phox-shell-mode 186,5666
(define-derived-mode phox-response-mode 191,5794
(define-derived-mode phox-goals-mode 201,6155
(defpgdefault completion-table224,6941

phox/phox-extraction.el,383
(defvar phox-prog-orig 19,619
(defun phox-prog-flags-modify(21,687
(defun phox-prog-flags-extract(50,1488
(defun phox-prog-flags-erase(61,1778
(defun phox-toggle-extraction(69,1974
(defun phox-compile-theorem(81,2376
(defun phox-compile-theorem-on-cursor(87,2601
(defun phox-output 103,3079
(defun phox-output-theorem 113,3291
(defun phox-output-theorem-on-cursor(120,3590

phox/phox-font.el,231
(defvar phox-sym-lock-enabled 1,0
(defvar phox-sym-lock-color 2,60
(defvar phox-sym-lock-keywords 3,118
(defconst phox-font-lock-keywords11,511
(defconst phox-sym-lock-keywords-table70,2628
(defun phox-sym-lock-start 93,3202

phox/phox-fun.el,1659
(defconst phox-forget-id-command 11,186
(defconst phox-forget-proof-command 12,232
(defconst phox-forget-new-elim-command 13,287
(defconst phox-forget-new-intro-command 14,345
(defconst phox-forget-new-equation-command 15,405
(defconst phox-forget-close-def-command 16,471
(defconst phox-comments-regexp 18,597
(defconst phox-strict-comments-regexp 20,776
(defconst phox-ident-regexp 21,941
(defconst phox-inductive-option 22,1027
(defconst phox-spaces-regexp 23,1079
(defconst phox-sy-definition-regexp 24,1122
(defconst phox-sy-inductive-regexp 28,1309
(defconst phox-inductive-regexp 34,1522
(defconst phox-data-regexp 40,1673
(defconst phox-definition-regexp 46,1827
(defconst phox-prove-claim-regexp 50,1971
(defconst phox-new-elim-regexp 54,2077
(defconst phox-new-intro-regexp 57,2196
(defconst phox-new-rewrite-regexp 60,2317
(defconst phox-new-equation-regexp 63,2442
(defconst phox-close-def-regexp 66,2569
(defun phox-init-syntax-table 71,2706
(defvar phox-top-keywords87,3178
(defvar phox-proof-keywords135,3633
(defun phox-find-and-forget 176,3983
(defalias 'phox-assert-next-command-interactive phox-assert-next-command-interactive
255,6399
(defun phox-depend-theorem(274,7365
(defun phox-eshow-extlist(283,7654
(defun phox-flag-name(297,8251
(defun phox-path(308,8553
(defun phox-print-expression(319,8789
(defun phox-print-sort-expression(332,9245
(defun phox-priority-symbols-list(343,9557
(defun phox-search-string(355,9929
(defun phox-constraints(370,10454
(defun phox-goals(381,10710
(defvar phox-state-menu393,10919
(defun phox-delete-symbol(418,11909
(defun phox-delete-symbol-on-cursor(424,12117

phox/phox-lang.el,323
(defvar phox-lang9,306
(defun phox-lang-absurd 17,535
(defun phox-lang-suppress 22,629
(defun phox-lang-opendef 27,826
(defun phox-lang-instance 32,944
(defun phox-lang-open-instance 37,1073
(defun phox-lang-lock 42,1222
(defun phox-lang-unlock 47,1352
(defun phox-lang-prove 52,1488
(defun phox-lang-let 57,1622

phox/phox-outline.el,254
(defconst phox-outline-title-regexp 20,745
(defconst phox-outline-section-regexp 21,810
(defconst phox-outline-save-regexp 22,866
(defconst phox-outline-heading-end-regexp 39,1409
(defun phox-outline-level(45,1584
(defun phox-setup-outline 59,2058

phox/phox-pbrpm.el,513
(defun phox-pbrpm-left-paren-p 39,1671
(defun phox-pbrpm-right-paren-p 46,1874
(defun phox-pbrpm-menu-from-string 54,2078
(defun phox-pbrpm-rename-in-cmd 63,2410
(defun phox-pbrpm-get-region-name 96,3658
(defun  phox-pbrpm-escape-string 99,3785
(defun phox-pbrpm-generate-menu 103,3920
(defalias 'proof-pbrpm-generate-menu proof-pbrpm-generate-menu
310,11400
(defalias 'proof-pbrpm-left-paren-p proof-pbrpm-left-paren-p
311,11464
(defalias 'proof-pbrpm-right-paren-p proof-pbrpm-right-paren-p
312,11526

phox/phox-sym-lock.el,1398
(defcustom phox-sym-lock-enabled 19,871
(defvar phox-sym-lock-sym-count 59,2452
(defvar phox-sym-lock-ext-start 62,2522
(defvar phox-sym-lock-ext-end 64,2644
(defvar phox-sym-lock-font-size 67,2763
(defvar phox-sym-lock-keywords 72,2953
(defvar phox-sym-lock-enabled 77,3129
(defvar phox-sym-lock-color 82,3291
(defvar phox-sym-lock-mouse-face 87,3509
(defvar phox-sym-lock-mouse-face-enabled 92,3699
(defconst phox-sym-lock-with-mule 97,3889
(defun phox-sym-lock-gen-symbol 100,3973
(defun phox-sym-lock-make-symbols-atomic 108,4275
(defun phox-sym-lock-compute-font-size 135,5216
(defvar phox-sym-lock-font-name173,6635
(defun phox-sym-lock-set-foreground 216,8233
(defun phox-sym-lock-translate-char 230,8842
(defun phox-sym-lock-translate-char-or-string 239,9159
(defun phox-sym-lock-remap-face 246,9387
(defvar phox-sym-lock-clear-face266,10375
(defun phox-sym-lock 278,10794
(defun phox-sym-lock-rec 287,11198
(defun phox-sym-lock-atom-face 293,11343
(defun phox-sym-lock-pre-idle-hook-first 298,11639
(defun phox-sym-lock-pre-idle-hook-last 308,12044
(defun phox-sym-lock-enable 317,12419
(defun phox-sym-lock-disable 330,12830
(defun phox-sym-lock-mouse-face-enable 343,13246
(defun phox-sym-lock-mouse-face-disable 350,13461
(defun phox-sym-lock-font-lock-hook 357,13680
(defun font-lock-set-defaults 372,14371
(defun phox-sym-lock-patch-keywords 384,14798

phox/phox-tags.el,305
(defun phox-tags-add-table(26,869
(defun phox-tags-reset-table(35,1264
(defun phox-tags-add-doc-table(40,1374
(defun phox-tags-add-lib-table(46,1523
(defun phox-tags-add-local-table(52,1658
(defun phox-tags-create-local-table(58,1841
(defun phox-complete-tag(69,2091
(defvar phox-tags-menu76,2200

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 234,7284
(defun plastic-find-and-forget 239,7476
(defun plastic-goal-hyp 278,8887
(defun plastic-state-preserving-p 289,9136
(defvar plastic-shell-current-line-width 312,10111
(defun plastic-shell-adjust-line-width 320,10427
(defun plastic-mode-config 347,11465
(defun plastic-show-shell-buffer 436,14724
(defun plastic-equal-module-filename 442,14827
(defun plastic-shell-compute-new-files-list 448,15105
(defun plastic-shell-mode-config 460,15499
(defun plastic-goals-mode-config 508,17302
(defun plastic-small-bar 520,17589
(defun plastic-large-bar 522,17678
(defun plastic-preprocessing 524,17816
(defun plastic-all-ctxt 576,19619
(defun plastic-send-one-undo 583,19788
(defun plastic-minibuf-cmd 593,20094
(defun plastic-minibuf 605,20566
(defun plastic-synchro 612,20772
(defun plastic-send-minibuf 617,20913
(defun plastic-had-error 625,21221
(defun plastic-reset-error 629,21396
(defun plastic-call-if-no-error 632,21535
(defun plastic-show-shell 637,21739
(define-key plastic-keymap 642,21867
(define-key plastic-keymap 643,21928
(define-key plastic-keymap 644,21989
(define-key plastic-keymap 645,22049
(define-key plastic-keymap 646,22108
(define-key plastic-keymap 647,22167
(defalias 'proof-toolbar-command proof-toolbar-command
657,22416
(defalias 'proof-minibuffer-cmd proof-minibuffer-cmd
658,22467

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,571
(defun pg-autotest-find-file 29,655
(defun pg-autotest-find-file-restart 36,935
(defmacro pg-autotest 49,1383
(defun pg-autotest-script-wholefile 63,1730
(defun pg-autotest-retract-file 80,2350
(defun pg-autotest-assert-processed 86,2486
(defun pg-autotest-assert-unprocessed 93,2740
(defun pg-autotest-message 100,3000
(defun pg-autotest-quit-prover 107,3193
(defun pg-autotest-finished 113,3374

generic/pg-custom.el,554
(defpgcustom maths-menu-enable 36,1134
(defpgcustom unicode-tokens-enable 42,1314
(defpgcustom mmm-enable 48,1491
(defpgcustom script-indent 57,1845
(defconst proof-toolbar-entries-default62,1982
(defpgcustom toolbar-entries 90,3754
(defpgcustom prog-args 109,4487
(defpgcustom prog-env 122,5062
(defpgcustom favourites 131,5488
(defpgcustom menu-entries 136,5677
(defpgcustom help-menu-entries 143,5913
(defpgcustom keymap 150,6176
(defpgcustom completion-table 155,6347
(defpgcustom tags-program 166,6721
(defpgcustom use-holes 175,7105

generic/pg-goals.el,285
(define-derived-mode proof-goals-mode 29,734
(define-key proof-goals-mode-map 57,1609
(define-key proof-goals-mode-map 59,1725
(define-key proof-goals-mode-map 60,1793
(defun proof-goals-config-done 69,1938
(defun pg-goals-display 77,2204
(defun pg-goals-button-action 118,3508

generic/pg-pbrpm.el,1808
(defvar pg-pbrpm-use-buffer-menu 41,1191
(defvar pg-pbrpm-start-goal-regexp 44,1313
(defvar pg-pbrpm-start-goal-regexp-par-num 48,1470
(defvar pg-pbrpm-end-goal-regexp 51,1593
(defvar pg-pbrpm-start-hyp-regexp 55,1745
(defvar pg-pbrpm-start-hyp-regexp-par-num 59,1906
(defvar pg-pbrpm-start-concl-regexp 63,2113
(defvar pg-pbrpm-auto-select-regexp 67,2277
(defvar pg-pbrpm-buffer-menu 74,2438
(defvar pg-pbrpm-spans 75,2472
(defvar pg-pbrpm-goal-description 76,2500
(defvar pg-pbrpm-windows-dialog-bug 77,2539
(defvar pbrpm-menu-desc 78,2580
(defun pg-pbrpm-erase-buffer-menu 80,2610
(defun pg-pbrpm-menu-change-hook 87,2794
(defun pg-pbrpm-create-reset-buffer-menu 105,3369
(defun pg-pbrpm-analyse-goal-buffer 124,4211
(defun pg-pbrpm-button-action 184,6609
(defun pg-pbrpm-exists 191,6835
(defun pg-pbrpm-eliminate-id 195,6947
(defun pg-pbrpm-build-menu 203,7193
(defun pg-pbrpm-setup-span 266,9513
(defun pg-pbrpm-run-command 326,11828
(defun pg-pbrpm-get-pos-info 359,13349
(defun pg-pbrpm-get-region-info 401,14648
(defun pg-pbrpm-auto-select-around-point 412,15060
(defun pg-pbrpm-translate-position 427,15584
(defun pg-pbrpm-process-click 435,15841
(defvar pg-pbrpm-remember-region-selected-region 455,16866
(defvar pg-pbrpm-regions-list 456,16920
(defun pg-pbrpm-erase-regions-list 458,16956
(defun pg-pbrpm-filter-regions-list 467,17264
(defface pg-pbrpm-multiple-selection-face474,17527
(defface pg-pbrpm-menu-input-face482,17729
(defun pg-pbrpm-do-remember-region 490,17919
(defun pg-pbrpm-remember-region-drag-up-hook 511,18767
(defun pg-pbrpm-remember-region-click-hook 515,18938
(defun pg-pbrpm-remember-region 520,19123
(defun pg-pbrpm-process-region 534,19837
(defun pg-pbrpm-process-regions-list 552,20566
(defun pg-pbrpm-region-expression 556,20749

generic/pg-pgip.el,2931
(defalias 'pg-pgip-debug pg-pgip-debug
38,1032
(defalias 'pg-pgip-error pg-pgip-error
39,1073
(defalias 'pg-pgip-warning pg-pgip-warning
40,1108
(defconst pg-pgip-version-supported 42,1158
(defun pg-pgip-process-packet 46,1264
(defvar pg-pgip-last-seen-id 56,1832
(defvar pg-pgip-last-seen-seq 57,1866
(defun pg-pgip-process-pgip 59,1902
(defun pg-pgip-process-msg 78,2833
(defvar pg-pgip-post-process-functions92,3403
(defun pg-pgip-post-process 102,3891
(defun pg-pgip-process-askpgip 118,4501
(defun pg-pgip-process-usespgip 124,4705
(defun pg-pgip-process-usespgml 128,4869
(defun pg-pgip-process-pgmlconfig 132,5033
(defun pg-pgip-process-proverinfo 148,5650
(defun pg-pgip-process-hasprefs 165,6315
(defun pg-pgip-haspref 179,6947
(defun pg-pgip-process-prefval 196,7649
(defun pg-pgip-process-guiconfig 223,8357
(defvar proof-assistant-idtables 230,8474
(defun pg-pgip-process-ids 233,8591
(defun pg-complete-idtable-symbol 259,9663
(defalias 'pg-pgip-process-setids pg-pgip-process-setids
264,9755
(defalias 'pg-pgip-process-addids pg-pgip-process-addids
265,9811
(defalias 'pg-pgip-process-delids pg-pgip-process-delids
266,9867
(defun pg-pgip-process-idvalue 269,9925
(defun pg-pgip-process-menuadd 281,10271
(defun pg-pgip-process-menudel 284,10314
(defun pg-pgip-process-ready 293,10546
(defun pg-pgip-process-cleardisplay 296,10587
(defun pg-pgip-process-proofstate 310,11044
(defun pg-pgip-process-normalresponse 314,11121
(defun pg-pgip-process-errorresponse 318,11251
(defun pg-pgip-process-scriptinsert 322,11380
(defun pg-pgip-process-metainforesponse 327,11514
(defun pg-pgip-file-of-url 336,11754
(defun pg-pgip-process-informfileloaded 341,11889
(defun pg-pgip-process-informfileretracted 347,12121
(defun pg-pgip-process-brokerstatus 360,12568
(defun pg-pgip-process-proveravailmsg 363,12616
(defun pg-pgip-process-newprovermsg 366,12666
(defun pg-pgip-process-proverstatusmsg 369,12714
(defvar pg-pgip-srcids 378,12960
(defun pg-pgip-process-newfile 382,13067
(defun pg-pgip-process-filestatus 398,13649
(defun pg-pgip-process-newobj 418,14303
(defun pg-pgip-process-delobj 421,14345
(defun pg-pgip-process-objectstatus 424,14387
(defun pg-pgip-process-parsescript 438,14739
(defun pg-pgip-get-pgiptype 461,15613
(defun pg-pgip-default-for 481,16405
(defun pg-pgip-subst-for 494,16800
(defun pg-pgip-interpret-value 506,17143
(defun pg-pgip-interpret-choice 524,17824
(defun pg-pgip-string-of-command 555,18841
(defconst pg-pgip-id572,19602
(defvar pg-pgip-refseq 578,19882
(defvar pg-pgip-refid 580,19979
(defvar pg-pgip-seq 583,20071
(defun pg-pgip-assemble-packet 585,20135
(defun pg-pgip-issue 603,20946
(defun pg-pgip-maybe-askpgip 620,21558
(defun pg-pgip-askprefs 626,21749
(defun pg-pgip-askids 630,21863
(defun pg-pgip-reset 643,22151
(defconst pg-pgip-start-element-regexp 674,22849
(defconst pg-pgip-end-element-regexp 675,22901

generic/pg-response.el,1292
(deflocal pg-response-eagerly-raise 32,788
(define-derived-mode proof-response-mode 42,1013
(define-key proof-response-mode-map 70,1967
(define-key proof-response-mode-map 71,2038
(define-key proof-response-mode-map 72,2092
(defun proof-response-config-done 76,2178
(defvar pg-response-special-display-regexp 87,2524
(defconst proof-multiframe-parameters91,2691
(defun proof-multiple-frames-enable 100,2990
(defun proof-three-window-enable 110,3318
(defun proof-select-three-b 113,3381
(defun proof-display-three-b 128,3850
(defvar pg-frame-configuration 139,4240
(defun pg-cache-frame-configuration 143,4387
(defun proof-layout-windows 147,4558
(defun proof-delete-other-frames 187,6345
(defvar pg-response-erase-flag 218,7433
(defun pg-response-maybe-erase222,7562
(defun pg-response-display 252,8658
(defun pg-response-display-with-face 277,9441
(defun pg-response-clear-displays 305,10287
(defun pg-response-message 318,10806
(defun pg-response-warning 324,11041
(defun proof-next-error 339,11445
(defun pg-response-has-error-location 421,14406
(defvar proof-trace-last-fontify-pos 444,15238
(defun proof-trace-fontify-pos 446,15281
(defun proof-trace-buffer-display 454,15594
(defun proof-trace-buffer-finish 465,15938
(defun pg-thms-buffer-clear 483,16281

generic/pg-thymodes.el,152
(defmacro pg-defthymode 23,499
(defmacro pg-do-unless-null 71,2310
(defun pg-symval 76,2393
(defun pg-modesym 82,2548
(defun pg-modesymval 86,2662

generic/pg-user.el,3332
(defun proof-script-new-command-advance 41,1156
(defun proof-maybe-follow-locked-end 84,2918
(defun proof-goto-command-start 111,3766
(defun proof-goto-command-end 134,4713
(defun proof-goto-point 157,5238
(defun proof-assert-next-command-interactive 171,5672
(defun proof-assert-until-point-interactive 183,6158
(defun proof-process-buffer 189,6388
(defun proof-undo-last-successful-command 204,6765
(defun proof-undo-and-delete-last-successful-command 209,6927
(defun proof-undo-last-successful-command-1 222,7481
(defun proof-retract-buffer 239,8100
(defun proof-retract-current-goal 248,8384
(defun proof-mouse-goto-point 267,8904
(defvar proof-minibuffer-history 282,9180
(defun proof-minibuffer-cmd 285,9275
(defun proof-frob-locked-end 329,10897
(defmacro proof-if-setting-configured 390,12835
(defmacro proof-define-assistant-command 398,13104
(defmacro proof-define-assistant-command-witharg 411,13559
(defun proof-issue-new-command 431,14381
(defun proof-cd-sync 477,15878
(defun proof-electric-terminator-enable 531,17598
(defun proof-electric-terminator 539,17888
(defun proof-add-completions 565,18710
(defun proof-script-complete 590,19617
(defun pg-copy-span-contents 604,19926
(defun pg-numth-span-higher-or-lower 621,20484
(defun pg-control-span-of 647,21230
(defun pg-move-span-contents 653,21434
(defun pg-fixup-children-spans 705,23610
(defun pg-move-region-down 715,23867
(defun pg-move-region-up 724,24160
(defun proof-forward-command 754,24988
(defun proof-backward-command 775,25709
(defun pg-pos-for-event 797,26053
(defun pg-span-for-event 803,26274
(defun pg-span-context-menu 807,26418
(defun pg-toggle-visibility 822,26866
(defun pg-create-in-span-context-menu 831,27173
(defun pg-span-undo 860,28387
(defun pg-goals-buffers-hint 906,29789
(defun pg-slow-fontify-tracing-hint 910,29971
(defun pg-response-buffers-hint 914,30142
(defun pg-jump-to-end-hint 926,30557
(defun pg-processing-complete-hint 930,30686
(defun pg-next-error-hint 947,31385
(defun pg-hint 952,31537
(defun pg-identifier-under-mouse-query 968,32127
(defun pg-identifier-near-point-query 977,32370
(defvar proof-query-identifier-collection 1004,33213
(defvar proof-query-identifier-history 1005,33260
(defun proof-query-identifier 1007,33305
(defun pg-identifier-query 1017,33574
(defun proof-imenu-enable 1048,34652
(defvar pg-input-ring 1084,35974
(defvar pg-input-ring-index 1087,36031
(defvar pg-stored-incomplete-input 1090,36103
(defun pg-previous-input 1093,36206
(defun pg-next-input 1107,36663
(defun pg-delete-input 1112,36785
(defun pg-get-old-input 1125,37123
(defun pg-restore-input 1139,37514
(defun pg-search-start 1150,37804
(defun pg-regexp-arg 1162,38296
(defun pg-search-arg 1174,38744
(defun pg-previous-matching-input-string-position 1188,39161
(defun pg-previous-matching-input 1215,40326
(defun pg-next-matching-input 1234,41176
(defvar pg-matching-input-from-input-string 1242,41559
(defun pg-previous-matching-input-from-input 1246,41673
(defun pg-next-matching-input-from-input 1264,42438
(defun pg-add-to-input-history 1275,42817
(defun pg-remove-from-input-history 1287,43270
(defun  pg-clear-input-ring 1298,43650
(define-key proof-mode-map 1312,44000
(define-key proof-mode-map 1313,44060
(defun pg-protected-undo 1315,44132

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 633,20742

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,7741
(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-integral-proofs 281,10313
(defcustom proof-script-fly-past-comments 296,10969
(defcustom proof-script-parse-function 301,11140
(defcustom proof-script-comment-start 319,11783
(defcustom proof-script-comment-start-regexp 330,12220
(defcustom proof-script-comment-end 338,12539
(defcustom proof-script-comment-end-regexp 350,12961
(defcustom proof-string-start-regexp 358,13272
(defcustom proof-string-end-regexp 363,13437
(defcustom proof-case-fold-search 368,13598
(defcustom proof-save-command-regexp 377,14010
(defcustom proof-save-with-hole-regexp 382,14120
(defcustom proof-save-with-hole-result 393,14495
(defcustom proof-goal-command-regexp 403,14945
(defcustom proof-goal-with-hole-regexp 411,15232
(defcustom proof-goal-with-hole-result 423,15675
(defcustom proof-non-undoables-regexp 432,16059
(defcustom proof-nested-undo-regexp 443,16514
(defcustom proof-ignore-for-undo-count 459,17226
(defcustom proof-script-imenu-generic-expression 467,17529
(defcustom proof-goal-command-p 475,17868
(defcustom proof-really-save-command-p 486,18359
(defcustom proof-completed-proof-behaviour 495,18666
(defcustom proof-count-undos-fn 523,20015
(defcustom proof-find-and-forget-fn 535,20566
(defcustom proof-forget-id-command 552,21275
(defcustom pg-topterm-goalhyplit-fn 562,21633
(defcustom proof-kill-goal-command 574,22168
(defcustom proof-undo-n-times-cmd 588,22672
(defcustom proof-nested-goals-history-p 602,23209
(defcustom proof-arbitrary-undo-positions 611,23546
(defcustom proof-state-preserving-p 625,24126
(defcustom proof-activate-scripting-hook 635,24598
(defcustom proof-deactivate-scripting-hook 654,25379
(defcustom proof-script-evaluate-elisp-comment-regexp 663,25709
(defcustom proof-indent 681,26295
(defcustom proof-indent-hang 686,26402
(defcustom proof-indent-enclose-offset 691,26528
(defcustom proof-indent-open-offset 696,26670
(defcustom proof-indent-close-offset 701,26807
(defcustom proof-indent-any-regexp 706,26945
(defcustom proof-indent-inner-regexp 711,27105
(defcustom proof-indent-enclose-regexp 716,27259
(defcustom proof-indent-open-regexp 721,27413
(defcustom proof-indent-close-regexp 726,27565
(defcustom proof-script-font-lock-keywords 732,27719
(defcustom proof-script-syntax-table-entries 740,28071
(defcustom proof-script-span-context-menu-extensions 758,28467
(defgroup proof-shell 784,29227
(defcustom proof-prog-name 794,29397
(defcustom proof-shell-auto-terminate-commands 805,29817
(defcustom proof-shell-pre-sync-init-cmd 814,30218
(defcustom proof-shell-init-cmd 828,30776
(defcustom proof-shell-init-hook 840,31305
(defcustom proof-shell-restart-cmd 845,31444
(defcustom proof-shell-quit-cmd 850,31599
(defcustom proof-shell-quit-timeout 855,31766
(defcustom proof-shell-cd-cmd 865,32217
(defcustom proof-shell-start-silent-cmd 882,32888
(defcustom proof-shell-stop-silent-cmd 891,33264
(defcustom proof-shell-silent-threshold 900,33599
(defcustom  proof-shell-inform-file-processed-cmd 908,33933
(defcustom  proof-shell-inform-file-retracted-cmd 929,34861
(defcustom proof-auto-multiple-files 957,36133
(defcustom proof-cannot-reopen-processed-files 972,36854
(defcustom proof-shell-require-command-regexp 986,37520
(defcustom proof-done-advancing-require-function 997,37982
(defcustom proof-shell-annotated-prompt-regexp 1009,38342
(defcustom proof-shell-error-regexp 1024,38907
(defcustom proof-shell-truncate-before-error 1044,39709
(defcustom pg-next-error-regexp 1058,40248
(defcustom pg-next-error-filename-regexp 1073,40857
(defcustom pg-next-error-extract-filename 1097,41890
(defcustom proof-shell-interrupt-regexp 1104,42133
(defcustom proof-shell-proof-completed-regexp 1118,42728
(defcustom proof-shell-clear-response-regexp 1131,43236
(defcustom proof-shell-clear-goals-regexp 1143,43688
(defcustom proof-shell-start-goals-regexp 1155,44134
(defcustom proof-shell-end-goals-regexp 1163,44501
(defcustom proof-shell-eager-annotation-start 1177,45076
(defcustom proof-shell-eager-annotation-start-length 1200,46095
(defcustom proof-shell-eager-annotation-end 1211,46521
(defcustom proof-shell-strip-output-markup 1227,47196
(defcustom proof-shell-assumption-regexp 1236,47581
(defcustom proof-shell-process-file 1246,47985
(defcustom proof-shell-retract-files-regexp 1272,49063
(defcustom proof-shell-compute-new-files-list 1285,49551
(defcustom pg-special-char-regexp 1300,50120
(defcustom proof-shell-set-elisp-variable-regexp 1305,50264
(defcustom proof-shell-match-pgip-cmd 1343,51930
(defcustom proof-shell-issue-pgip-cmd 1357,52412
(defcustom proof-use-pgip-askprefs 1362,52577
(defcustom proof-shell-query-dependencies-cmd 1370,52924
(defcustom proof-shell-theorem-dependency-list-regexp 1377,53184
(defcustom proof-shell-theorem-dependency-list-split 1393,53844
(defcustom proof-shell-show-dependency-cmd 1402,54267
(defcustom proof-shell-trace-output-regexp 1424,55173
(defcustom proof-shell-thms-output-regexp 1442,55768
(defcustom proof-tokens-activate-command 1455,56151
(defcustom proof-tokens-deactivate-command 1462,56391
(defcustom proof-tokens-extra-modes 1469,56636
(defcustom proof-shell-unicode 1484,57141
(defcustom proof-shell-filename-escapes 1493,57531
(defcustom proof-shell-process-connection-type1510,58211
(defcustom proof-shell-strip-crs-from-input 1533,59215
(defcustom proof-shell-strip-crs-from-output 1545,59698
(defcustom proof-shell-insert-hook 1553,60066
(defcustom proof-script-preprocess 1594,62026
(defcustom proof-shell-handle-delayed-output-hook1600,62177
(defcustom proof-shell-handle-error-or-interrupt-hook1606,62392
(defcustom proof-shell-pre-interrupt-hook1624,63138
(defcustom proof-shell-handle-output-system-specific 1632,63409
(defcustom proof-state-change-hook 1655,64385
(defcustom proof-shell-syntax-table-entries 1665,64778
(defgroup proof-goals 1683,65149
(defcustom pg-subterm-first-special-char 1688,65270
(defcustom pg-subterm-anns-use-stack 1696,65582
(defcustom pg-goals-change-goal 1705,65881
(defcustom pbp-goal-command 1710,65997
(defcustom pbp-hyp-command 1715,66153
(defcustom pg-subterm-help-cmd 1720,66315
(defcustom pg-goals-error-regexp 1727,66551
(defcustom proof-shell-result-start 1732,66711
(defcustom proof-shell-result-end 1738,66945
(defcustom pg-subterm-start-char 1744,67158
(defcustom pg-subterm-sep-char 1755,67632
(defcustom pg-subterm-end-char 1761,67811
(defcustom pg-topterm-regexp 1767,67968
(defcustom proof-goals-font-lock-keywords 1782,68568
(defcustom proof-response-font-lock-keywords 1790,68927
(defcustom proof-shell-font-lock-keywords 1798,69289
(defcustom pg-before-fontify-output-hook 1809,69804
(defcustom pg-after-fontify-output-hook 1817,70165

generic/proof-depends.el,917
(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 215,7235
(defun proof-show-dependency 221,7458
(defconst pg-dep-span-priority 228,7747
(defconst pg-ordinary-span-priority 229,7783
(defun proof-highlight-depcs 231,7825
(defun proof-highlight-depts 242,8291
(defun proof-depends-save-old-face 254,8801
(defun proof-depends-restore-old-face 259,8979
(defun proof-dep-unhighlight 265,9208

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,1595
(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,3638
(defface proof-eager-annotation-face126,3895
(defface proof-debug-message-face134,4113
(defface proof-boring-face142,4312
(defface proof-mouse-highlight-face150,4504
(defface proof-highlight-dependent-face158,4722
(defface proof-highlight-dependency-face166,4929
(defface proof-active-area-face174,5126
(defface proof-script-sticky-error-face182,5438
(defface proof-script-highlight-error-face190,5667
(defconst proof-face-compat-doc 202,6012
(defconst proof-queue-face 203,6092
(defconst proof-locked-face 204,6160
(defconst proof-declaration-name-face 205,6230
(defconst proof-tacticals-name-face 206,6320
(defconst proof-tactics-name-face 207,6406
(defconst proof-error-face 208,6488
(defconst proof-script-sticky-error-face 209,6556
(defconst proof-script-highlight-error-face 210,6652
(defconst proof-warning-face 211,6754
(defconst proof-eager-annotation-face 212,6826
(defconst proof-debug-message-face 213,6916
(defconst proof-boring-face 214,7000
(defconst proof-mouse-highlight-face 215,7070
(defconst proof-highlight-dependent-face 216,7158
(defconst proof-highlight-dependency-face 217,7254
(defconst proof-active-area-face 218,7352
(defconst proof-script-error-face 219,7432

generic/proof-indent.el,219
(defun proof-indent-indent 14,412
(defun proof-indent-offset 23,678
(defun proof-indent-inner-p 40,1278
(defun proof-indent-goto-prev 49,1578
(defun proof-indent-calculate 56,1911
(defun proof-indent-line 76,2611

generic/proof-maths-menu.el,83
(defun proof-maths-menu-set-global 30,942
(defun proof-maths-menu-enable 44,1393

generic/proof-menu.el,2026
(defvar proof-display-some-buffers-count 35,801
(defun proof-display-some-buffers 37,846
(defun proof-menu-define-keys 94,2976
(defun proof-menu-define-main 153,5842
(defvar proof-menu-favourites 162,6027
(defvar proof-menu-settings 165,6134
(defun proof-menu-define-specific 169,6223
(defun proof-assistant-menu-update 212,7485
(defvar proof-help-menu226,7918
(defvar proof-show-hide-menu234,8188
(defvar proof-buffer-menu245,8612
(defun proof-keep-response-history 306,10767
(defconst proof-quick-opts-menu314,11077
(defun proof-quick-opts-vars 504,18837
(defun proof-quick-opts-changed-from-defaults-p 534,19721
(defun proof-quick-opts-changed-from-saved-p 538,19826
(defun proof-quick-opts-save 549,20177
(defun proof-quick-opts-reset 554,20345
(defconst proof-config-menu566,20613
(defconst proof-advanced-menu573,20792
(defvar proof-menu586,21224
(defun proof-main-menu 595,21506
(defun proof-aux-menu 607,21845
(defun proof-menu-define-favourites-menu 623,22191
(defun proof-def-favourite 643,22840
(defvar proof-make-favourite-cmd-history 666,23811
(defvar proof-make-favourite-menu-history 669,23896
(defun proof-save-favourites 672,23982
(defun proof-del-favourite 677,24130
(defun proof-read-favourite 694,24686
(defun proof-add-favourite 718,25462
(defun proof-menu-define-settings-menu 745,26507
(defun proof-menu-entry-name 778,27638
(defun proof-menu-entry-for-setting 788,27988
(defun proof-settings-vars 807,28520
(defun proof-settings-changed-from-defaults-p 812,28697
(defun proof-settings-changed-from-saved-p 816,28803
(defun proof-settings-save 820,28906
(defun proof-settings-reset 825,29073
(defun proof-assistant-invisible-command-ifposs 830,29236
(defun proof-maybe-askprefs 852,30206
(defun proof-assistant-settings-cmd 858,30398
(defvar proof-assistant-format-table875,31053
(defun proof-assistant-format-bool 883,31421
(defun proof-assistant-format-int 886,31534
(defun proof-assistant-format-string 889,31626
(defun proof-assistant-format 892,31724

generic/proof-mmm.el,70
(defun proof-mmm-set-global 39,1466
(defun proof-mmm-enable 54,2005

generic/proof-script.el,5455
(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 110,3801
(deflocal proof-queue-span 117,4067
(deflocal proof-overlay-arrow 126,4553
(defun proof-span-give-warning 132,4680
(defun proof-span-read-only 138,4860
(defun proof-strict-read-only 147,5233
(defsubst proof-set-queue-endpoints 157,5611
(defun proof-set-overlay-arrow 161,5752
(defsubst proof-set-locked-endpoints 172,6090
(defsubst proof-detach-queue 177,6266
(defsubst proof-detach-locked 182,6405
(defsubst proof-set-queue-start 189,6630
(defsubst proof-set-locked-end 193,6756
(defsubst proof-set-queue-end 205,7226
(defun proof-init-segmentation 216,7523
(defun proof-colour-locked 248,8918
(defun proof-colour-locked-span 255,9191
(defun proof-sticky-errors 261,9464
(defun proof-restart-buffers 274,9880
(defun proof-script-buffers-with-spans 296,10699
(defun proof-script-remove-all-spans-and-deactivate 306,11055
(defun proof-script-clear-queue-spans-on-error 310,11245
(defun proof-script-delete-spans 332,12118
(defun proof-script-delete-secondary-spans 337,12317
(defun proof-unprocessed-begin 350,12606
(defun proof-script-end 358,12860
(defun proof-queue-or-locked-end 367,13170
(defun proof-locked-region-full-p 386,13764
(defun proof-locked-region-empty-p 395,14036
(defun proof-only-whitespace-to-locked-region-p 399,14186
(defun proof-in-locked-region-p 409,14513
(defun proof-goto-end-of-locked 421,14770
(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 438,15529
(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 449,16010
(defun proof-end-of-locked-visible-p 463,16623
(defvar pg-idioms 482,17216
(defun pg-clear-script-portions 485,17312
(defun pg-remove-element 491,17547
(defun pg-get-element 499,17850
(defun pg-add-element 509,18166
(defun pg-set-element-span-invisible 551,19961
(defun pg-open-invisible-span 555,20121
(defun pg-make-element-invisible 560,20292
(defun pg-make-element-visible 565,20503
(defun pg-toggle-element-span-visibility 570,20697
(defun pg-toggle-element-visibility 576,20861
(defun pg-show-all-portions 582,21124
(defun pg-show-all-proofs 601,21832
(defun pg-hide-all-proofs 606,21960
(defun pg-add-proof-element 611,22091
(defun pg-span-name 626,22862
(defvar pg-span-context-menu-keymap647,23562
(defun pg-last-output-displayform 654,23800
(defun pg-set-span-helphighlights 672,24496
(defun pg-delete-self-modification-hook 713,26196
(defun proof-complete-buffer-atomic 724,26469
(defun proof-register-possibly-new-processed-file766,28389
(defun proof-inform-prover-file-retracted 812,30226
(defun proof-auto-retract-dependencies 832,31077
(defun proof-unregister-buffer-file-name 886,33627
(defun proof-protected-process-or-retract 932,35452
(defun proof-deactivate-scripting-auto 959,36622
(defun proof-deactivate-scripting 968,36980
(defun proof-activate-scripting 1101,42236
(defun proof-toggle-active-scripting 1216,47350
(defun proof-done-advancing 1255,48595
(defun proof-done-advancing-comment 1334,51580
(defun proof-done-advancing-save 1368,52956
(defun proof-make-goalsave 1456,56321
(defun proof-get-name-from-goal 1474,57153
(defun proof-done-advancing-autosave 1494,58178
(defun proof-done-advancing-other 1559,60722
(defun proof-segment-up-to-parser 1588,61652
(defun proof-script-generic-parse-find-comment-end 1657,63922
(defun proof-script-generic-parse-cmdend 1666,64336
(defun proof-script-generic-parse-cmdstart 1717,66232
(defun proof-script-generic-parse-sexp 1756,67832
(defun proof-semis-to-vanillas 1768,68298
(defun proof-script-next-command-advance 1817,69820
(defun proof-assert-until-point 1836,70319
(defun proof-assert-electric-terminator 1851,70912
(defun proof-assert-semis 1886,72296
(defun proof-retract-before-change 1900,73002
(defun proof-inside-comment 1912,73403
(defun proof-inside-string 1918,73577
(defun proof-insert-pbp-command 1933,73858
(defun proof-insert-sendback-command 1948,74359
(defun proof-done-retracting 1974,75262
(defun proof-setup-retract-action 2009,76703
(defun proof-last-goal-or-goalsave 2019,77189
(defun proof-retract-target 2043,78101
(defun proof-retract-until-point-interactive 2124,81485
(defun proof-retract-until-point 2132,81870
(define-derived-mode proof-mode 2179,83705
(defun proof-script-set-visited-file-name 2213,84976
(defun proof-script-set-buffer-hooks 2235,85989
(defun proof-script-kill-buffer-fn 2243,86407
(defun proof-config-done-related 2275,87724
(defun proof-generic-goal-command-p 2343,90247
(defun proof-generic-state-preserving-p 2348,90460
(defun proof-generic-count-undos 2357,90977
(defun proof-generic-find-and-forget 2386,92030
(defconst proof-script-important-settings2437,93802
(defun proof-config-done 2452,94348
(defun proof-setup-parsing-mechanism 2510,96248
(defun proof-setup-imenu 2534,97327
(deflocal proof-segment-up-to-cache 2558,98101
(deflocal proof-segment-up-to-cache-start 2559,98142
(deflocal proof-last-edited-low-watermark 2560,98187
(defun proof-segment-up-to-using-cache 2570,98674
(defun proof-segment-cache-contents-for 2599,99822
(defun proof-script-after-change-function 2611,100191
(defun proof-script-set-after-change-functions 2623,100698

generic/proof-shell.el,3793
(defvar proof-marker 35,808
(defvar proof-action-list 38,904
(defvar proof-shell-last-goals-output 63,1832
(defvar proof-shell-last-response-output 66,1912
(defvar proof-shell-delayed-output-start 69,1999
(defvar proof-shell-delayed-output-end 73,2181
(defvar proof-shell-delayed-output-flags 77,2361
(defcustom proof-shell-active-scripting-indicator86,2557
(defun proof-shell-ready-prover 134,3909
(defsubst proof-shell-live-buffer 148,4448
(defun proof-shell-available-p 155,4687
(defun proof-grab-lock 161,4909
(defun proof-release-lock 172,5407
(defcustom proof-shell-fiddle-frames 184,5627
(defun proof-shell-set-text-representation 190,5849
(defun proof-shell-start 201,6310
(defvar proof-shell-kill-function-hooks 386,12588
(defun proof-shell-kill-function 389,12686
(defun proof-shell-clear-state 478,16490
(defun proof-shell-exit 493,16933
(defun proof-shell-bail-out 506,17437
(defun proof-shell-restart 515,17914
(defvar proof-shell-urgent-message-marker 557,19292
(defvar proof-shell-urgent-message-scanner 560,19413
(defun proof-shell-handle-error-output 564,19598
(defun proof-shell-handle-error-or-interrupt 590,20460
(defun proof-shell-error-or-interrupt-action 625,21881
(defun proof-goals-pos 639,22409
(defun proof-pbp-focus-on-first-goal 644,22620
(defsubst proof-shell-string-match-safe 656,23036
(defun proof-shell-handle-immediate-output 660,23197
(defvar proof-shell-expecting-output 727,25779
(defvar proof-shell-interrupt-pending 731,25938
(defun proof-interrupt-process 736,26162
(defun proof-shell-insert 774,27595
(defun proof-shell-action-list-item 827,29463
(defun proof-shell-set-silent 832,29714
(defun proof-shell-start-silent-item 838,29933
(defun proof-shell-clear-silent 844,30122
(defun proof-shell-stop-silent-item 850,30344
(defsubst proof-shell-should-be-silent 856,30533
(defsubst proof-shell-invoke-callback 867,31043
(defsubst proof-shell-insert-action-item 873,31253
(defsubst proof-shell-slurp-comments 877,31428
(defun proof-add-to-queue 888,31834
(defun proof-start-queue 946,33859
(defun proof-extend-queue 957,34223
(defun proof-shell-exec-loop 965,34604
(defun proof-shell-insert-loopback-cmd 1033,36908
(defun proof-shell-process-urgent-message 1058,38068
(defun proof-shell-process-urgent-message-default 1107,39789
(defun proof-shell-process-urgent-message-trace 1123,40376
(defun proof-shell-process-urgent-message-retract 1136,40936
(defun proof-shell-process-urgent-message-elisp 1157,41784
(defun proof-shell-process-urgent-message-thmdeps 1172,42279
(defun proof-shell-strip-eager-annotations 1186,42659
(defvar proof-shell-minibuffer-urgent-interactive-input-history 1201,43192
(defun proof-shell-minibuffer-urgent-interactive-input 1203,43262
(defun proof-shell-filter 1219,43736
(defun proof-shell-filter-first-command 1320,47145
(defun proof-shell-process-urgent-messages 1335,47688
(defun proof-shell-filter-manage-output 1385,49260
(defsubst proof-shell-display-output-as-response 1418,50563
(defun proof-shell-handle-delayed-output 1424,50855
(defvar pg-last-tracing-output-time 1519,54320
(defconst pg-slow-mode-duration 1522,54426
(defconst pg-fast-tracing-mode-threshold 1525,54508
(defvar pg-tracing-cleanup-timer 1528,54636
(defun pg-tracing-tight-loop 1530,54675
(defun pg-finish-tracing-display 1573,56387
(defun proof-shell-wait 1591,56751
(defun proof-done-invisible 1610,57659
(defun proof-shell-invisible-command 1616,57829
(defun proof-shell-invisible-cmd-get-result 1663,59373
(defun proof-shell-invisible-command-invisible-result 1675,59809
(defun pg-insert-last-output-as-comment 1695,60310
(define-derived-mode proof-shell-mode 1714,60782
(defconst proof-shell-important-settings1751,61813
(defun proof-shell-config-done 1757,61928

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,1006
(defsubst proof-ids-to-regexp 17,446
(defsubst proof-anchor-regexp 24,688
(defconst proof-no-regexp 28,793
(defsubst proof-regexp-alt 31,884
(defsubst proof-re-search-forward-region 40,1196
(defsubst proof-search-forward 53,1694
(defsubst proof-replace-regexp-in-string 59,1949
(defsubst proof-re-search-forward 64,2200
(defsubst proof-re-search-backward 69,2458
(defsubst proof-re-search-forward-safe 74,2719
(defsubst proof-string-match 80,3000
(defsubst proof-string-match-safe 85,3229
(defsubst proof-stringfn-match 89,3433
(defsubst proof-looking-at 96,3696
(defsubst proof-looking-at-safe 101,3883
(defsubst proof-looking-at-syntactic-context-default 105,4028
(defsubst proof-replace-string 116,4405
(defsubst proof-replace-regexp 121,4609
(defsubst proof-replace-regexp-nocasefold 126,4818
(defvar proof-id 134,5100
(defsubst proof-ids 140,5320
(defun proof-zap-commas 154,5812
(defun proof-format 170,6308
(defun proof-format-filename 189,6947
(defun proof-insert 236,8349

generic/proof-toolbar.el,2332
(defun proof-toolbar-function 33,809
(defun proof-toolbar-icon 36,906
(defun proof-toolbar-enabler 39,1007
(defun proof-toolbar-make-icon 46,1159
(defun proof-toolbar-make-toolbar-items 55,1467
(defvar proof-toolbar-map 80,2272
(defun proof-toolbar-available-p 83,2371
(defun proof-toolbar-setup 92,2647
(defun proof-toolbar-enable 113,3504
(defalias 'proof-toolbar-undo proof-toolbar-undo
146,4554
(defun proof-toolbar-undo-enable-p 148,4622
(defalias 'proof-toolbar-delete proof-toolbar-delete
155,4780
(defun proof-toolbar-delete-enable-p 157,4861
(defalias 'proof-toolbar-home proof-toolbar-home
165,5043
(defalias 'proof-toolbar-next proof-toolbar-next
169,5110
(defun proof-toolbar-next-enable-p 171,5181
(defalias 'proof-toolbar-goto proof-toolbar-goto
177,5297
(defun proof-toolbar-goto-enable-p 179,5347
(defalias 'proof-toolbar-retract proof-toolbar-retract
184,5432
(defun proof-toolbar-retract-enable-p 186,5489
(defalias 'proof-toolbar-use proof-toolbar-use
192,5608
(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p
193,5660
(defalias 'proof-toolbar-restart proof-toolbar-restart
197,5741
(defalias 'proof-toolbar-goal proof-toolbar-goal
201,5806
(defalias 'proof-toolbar-qed proof-toolbar-qed
205,5864
(defun proof-toolbar-qed-enable-p 207,5913
(defalias 'proof-toolbar-state proof-toolbar-state
215,6075
(defalias 'proof-toolbar-state-enable-p proof-toolbar-state-enable-p
216,6118
(defalias 'proof-toolbar-context proof-toolbar-context
220,6197
(defalias 'proof-toolbar-context-enable-p proof-toolbar-context-enable-p
221,6243
(defalias 'proof-toolbar-command proof-toolbar-command
225,6324
(defalias 'proof-toolbar-command-enable-p proof-toolbar-command-enable-p
226,6380
(defun proof-toolbar-help 230,6485
(defalias 'proof-toolbar-find proof-toolbar-find
236,6565
(defalias 'proof-toolbar-find-enable-p proof-toolbar-find-enable-p
237,6617
(defalias 'proof-toolbar-info proof-toolbar-info
241,6692
(defalias 'proof-toolbar-info-enable-p proof-toolbar-info-enable-p
242,6747
(defalias 'proof-toolbar-visibility proof-toolbar-visibility
246,6845
(defun proof-toolbar-visibility-enable-p 248,6905
(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt
253,7019
(defun proof-toolbar-interrupt-enable-p 254,7080
(defun proof-toolbar-scripting-menu 262,7233

generic/proof-unicode-tokens.el,497
(defvar proof-unicode-tokens-initialised 31,827
(defun proof-unicode-tokens-init 34,934
(defun proof-unicode-tokens-configure 48,1436
(defun proof-unicode-tokens-mode-if-enabled 60,1882
(defun proof-unicode-tokens-set-global 66,2081
(defun proof-unicode-tokens-enable 82,2651
(defun proof-unicode-tokens-reconfigure 102,3504
(defun proof-unicode-tokens-configure-prover 128,4392
(defun proof-unicode-tokens-activate-prover 133,4573
(defun proof-unicode-tokens-deactivate-prover 140,4819

generic/proof-useropts.el,1552
(defgroup proof-user-options 21,553
(defun proof-set-value 29,732
(defcustom proof-electric-terminator-enable 62,1855
(defcustom proof-toolbar-enable 74,2387
(defcustom proof-imenu-enable 80,2560
(defcustom pg-show-hints 86,2731
(defcustom proof-shell-quiet-errors 91,2864
(defcustom proof-trace-output-slow-catchup 98,3135
(defcustom proof-strict-state-preserving 108,3632
(defcustom proof-strict-read-only 121,4241
(defcustom proof-allow-undo-in-read-only 134,4820
(defcustom proof-three-window-enable 141,5102
(defcustom proof-multiple-frames-enable 160,5852
(defcustom proof-delete-empty-windows 169,6185
(defcustom proof-shrink-windows-tofit 180,6716
(defcustom proof-auto-raise-buffers 187,6988
(defcustom proof-colour-locked 194,7223
(defcustom proof-sticky-errors 202,7473
(defcustom proof-query-file-save-when-activating-scripting209,7690
(defcustom proof-one-command-per-line225,8410
(defcustom proof-prog-name-ask232,8634
(defcustom proof-prog-name-guess238,8794
(defcustom proof-tidy-response246,9059
(defcustom proof-keep-response-history260,9522
(defcustom pg-input-ring-size 270,9910
(defcustom proof-general-debug 275,10062
(defcustom proof-use-parser-cache 286,10471
(defcustom proof-follow-mode 296,10768
(defcustom proof-auto-action-when-deactivating-scripting 320,11945
(defcustom proof-script-command-separator 343,12894
(defcustom proof-rsh-command 351,13186
(defcustom proof-disappearing-proofs 367,13736
(defcustom proof-full-annotation 372,13897
(defcustom proof-minibuffer-messages 381,14269

generic/proof-utils.el,2073
(defmacro deflocal 61,1871
(defmacro proof-with-current-buffer-if-exists 68,2109
(deflocal proof-buffer-type 74,2319
(defmacro proof-with-script-buffer 80,2599
(defmacro proof-map-buffers 91,2980
(defmacro proof-sym 96,3165
(defsubst proof-try-require 101,3326
(defun proof-save-some-buffers 114,3657
(defun proof-save-this-buffer 134,4253
(defmacro proof-ass-sym 169,5575
(defmacro proof-ass-symv 175,5834
(defmacro proof-ass 181,6092
(defun proof-defpgcustom-fn 187,6344
(defun undefpgcustom 208,7214
(defmacro defpgcustom 214,7438
(defun proof-defpgdefault-fn 225,7849
(defmacro defpgdefault 239,8307
(defmacro defpgfun 250,8669
(defun proof-defpacustom-fn 264,9069
(defmacro defpacustom 330,11350
(defmacro proof-eval-when-ready-for-assistant 351,12297
(defun proof-file-truename 364,12688
(defun proof-files-to-buffers 368,12871
(defun proof-buffers-in-mode 376,13111
(defun pg-save-from-death 390,13561
(defun proof-define-keys 409,14178
(defun pg-remove-specials 420,14463
(defun pg-remove-specials-in-string 430,14799
(defun proof-warn-if-unset 441,15025
(defun proof-get-window-for-buffer 446,15243
(defun proof-display-and-keep-buffer 497,17551
(defun proof-clean-buffer 539,19274
(defun pg-internal-warning 555,19930
(defun proof-debug 562,20197
(defun proof-switch-to-buffer 572,20569
(defun proof-resize-window-tofit 594,21693
(defun proof-submit-bug-report 689,25541
(defun proof-deftoggle-fn 724,26898
(defmacro proof-deftoggle 739,27551
(defun proof-defintset-fn 746,27925
(defmacro proof-defintset 762,28629
(defun proof-defstringset-fn 769,29006
(defmacro proof-defstringset 782,29632
(defun proof-escape-keymap-doc 795,30088
(defmacro proof-defshortcut 799,30228
(defmacro proof-definvisible 814,30826
(defun pg-custom-save-vars 841,31753
(defun pg-custom-reset-vars 857,32397
(defun proof-locate-executable 870,32734
(defun pg-current-word-pos 885,33289
(defun proof-looking-at-syntactic-context 932,35005
(defsubst proof-shell-strip-output-markup 947,35574
(defun proof-minibuffer-message 953,35838

lib/bufhist.el,1257
(defun bufhist-ring-update 38,1391
(defgroup bufhist 47,1713
(defcustom bufhist-ring-size 51,1794
(defvar bufhist-ring 56,1905
(defvar bufhist-ring-pos 59,1979
(defvar bufhist-lastswitch-modified-tick 62,2058
(defvar bufhist-read-only-history 65,2164
(defvar bufhist-saved-mode-line-format 68,2235
(defvar bufhist-normal-read-only 71,2338
(defvar bufhist-top-point 74,2432
(defun bufhist-mode-line-format-entry 77,2522
(defconst bufhist-minor-mode-map106,3596
(define-minor-mode bufhist-mode119,4073
(defun bufhist-get-buffer-contents 141,4954
(defun bufhist-restore-buffer-contents 150,5296
(defun bufhist-checkpoint 159,5610
(defun bufhist-erase-buffer 167,5979
(defun bufhist-checkpoint-and-erase 178,6350
(defun bufhist-switch-to-index 184,6536
(defun bufhist-first 223,8135
(defun bufhist-last 228,8294
(defun bufhist-prev 233,8438
(defun bufhist-next 241,8661
(defun bufhist-delete 246,8801
(defun bufhist-clear 258,9342
(defun bufhist-init 273,9737
(defun bufhist-exit 301,10746
(defun bufhist-set-readwrite 311,11010
(defun bufhist-before-change-function 326,11630
(define-button-type 'bufhist-nextbufhist-next
340,12053
(define-button-type 'bufhist-prevbufhist-prev
344,12150
(defun bufhist-insert-buttons 351,12362

lib/holes.el,2465
(defvar holes-default-hole 44,1121
(defvar holes-active-hole 50,1299
(defgroup holes 60,1496
(defcustom holes-empty-hole-string 65,1595
(defcustom holes-empty-hole-regexp 70,1738
(defface active-hole-face92,2440
(defface inactive-hole-face102,2856
(defvar hole-map116,3297
(defvar holes-mode-map126,3688
(defun holes-region-beginning-or-nil 172,5425
(defun holes-region-end-or-nil 176,5561
(defun holes-copy-active-region 180,5679
(defun holes-is-hole-p 186,5889
(defun holes-hole-start-position 190,5981
(defun holes-hole-end-position 196,6164
(defun holes-hole-buffer 201,6335
(defun holes-hole-at 207,6509
(defun holes-active-hole-exist-p 212,6679
(defun holes-active-hole-start-position 219,6932
(defun holes-active-hole-end-position 227,7300
(defun holes-active-hole-buffer 236,7663
(defun holes-goto-active-hole 244,7964
(defun holes-highlight-hole-as-active 253,8223
(defun holes-highlight-hole 261,8531
(defun holes-disable-active-hole 269,8818
(defun holes-set-active-hole 282,9350
(defun holes-is-in-hole-p 292,9695
(defun holes-make-hole 296,9833
(defun holes-make-hole-at 314,10489
(defun holes-clear-hole 328,10942
(defun holes-clear-hole-at 337,11200
(defun holes-map-holes 345,11456
(defun holes-clear-all-buffer-holes 349,11610
(defun holes-next 359,11911
(defun holes-next-after-active-hole 366,12163
(defun holes-set-active-hole-next 373,12379
(defun holes-replace-segment 392,12916
(defun holes-replace 401,13269
(defun holes-replace-active-hole 429,14447
(defun holes-replace-update-active-hole 436,14738
(defun holes-delete-update-active-hole 454,15385
(defun holes-set-make-active-hole 462,15612
(defalias 'holes-track-mouse-selection holes-track-mouse-selection
477,16167
(defsubst holes-track-mouse-clicks 478,16225
(defun holes-mouse-replace-active-hole 482,16335
(defun holes-destroy-hole 496,16806
(defsubst holes-hole-at-event 510,17188
(defun holes-mouse-destroy-hole 514,17288
(defun holes-mouse-forget-hole 521,17509
(defun holes-mouse-set-make-active-hole 531,17801
(defun holes-mouse-set-active-hole 547,18300
(defun holes-set-point-next-hole-destroy 556,18551
(defun holes-replace-string-by-holes-backward 582,19532
(defun holes-skeleton-end-hook 600,20232
(defconst holes-jump-doc609,20670
(defun holes-replace-string-by-holes-backward-jump 616,20876
(define-minor-mode holes-mode 633,21558
(defun holes-abbrev-complete 728,25040
(defun holes-insert-and-expand 738,25383

lib/local-vars-list.el,373
(defconst local-vars-list-doc 28,825
(defun local-vars-list-insert-empty-zone 44,1387
(defun local-vars-list-find 82,2090
(defun local-vars-list-goto-var 101,2861
(defun local-vars-list-get-current 127,3908
(defun local-vars-list-set-current 148,4758
(defun local-vars-list-get 171,5473
(defun local-vars-list-get-safe 188,6003
(defun local-vars-list-set 193,6197

lib/maths-menu.el,242
(defvar maths-menu-filter-predicate 56,2317
(defvar maths-menu-tokenise-insert 59,2426
(defun maths-menu-build-menu 62,2563
(defvar maths-menu-menu84,3324
(defvar maths-menu-mode-map344,12882
(define-minor-mode maths-menu-mode352,13101

lib/pg-dev.el,166
(defconst pg-dev-lisp-font-lock-keywords52,1582
(defun pg-loadpath 80,2416
(defun unload-pg 90,2587
(defun profile-pg 118,3450
(defun pg-bug-references 139,4117

lib/pg-fontsets.el,209
(defcustom pg-fontsets-default-fontset 24,722
(defvar pg-fontsets-names 29,868
(defun pg-fontsets-make-fontsetsizes 32,949
(defconst pg-fontsets-base-fonts51,1710
(defun pg-fontsets-make-fontsets 57,1840

lib/proof-compat.el,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,2739
(defun scomint-make-in-buffer 86,3079
(defun scomint-make 110,4346
(defun scomint-exec 123,5057
(defun scomint-exec-1 160,6650
(defalias 'scomint-send-string scomint-send-string
210,8780
(defun scomint-send-eof 212,8834
(defun scomint-send-input 221,9067
(defun scomint-truncate-buffer 264,10568
(defun scomint-strip-ctrl-m 277,10962
(defun scomint-output-filter 291,11525
(defun scomint-interrupt-process 363,14257

lib/span.el,1315
(defalias 'span-start span-start
22,609
(defalias 'span-end span-end
23,647
(defalias 'span-set-property span-set-property
24,681
(defalias 'span-property span-property
25,724
(defalias 'span-make span-make
26,763
(defalias 'span-detach span-detach
27,799
(defalias 'span-set-endpoints span-set-endpoints
28,839
(defalias 'span-buffer span-buffer
29,884
(defun span-read-only-hook 31,925
(defsubst span-read-only 36,1115
(defsubst span-read-write 43,1425
(defsubst span-write-warning 48,1595
(defsubst span-lt 59,2119
(defsubst spans-at-point-prop 64,2263
(defsubst spans-at-region-prop 73,2454
(defsubst span-at 83,2720
(defsubst span-delete 87,2846
(defsubst span-mapcar-spans 94,3068
(defsubst span-mapc-spans 98,3243
(defun span-at-before 102,3414
(defsubst prev-span 119,4138
(defsubst next-span 125,4291
(defsubst span-live-p 131,4505
(defsubst span-raise 137,4671
(defsubst span-string 141,4804
(defsubst set-span-properties 146,4964
(defsubst span-find-span 152,5158
(defsubst span-at-event 160,5470
(defun fold-spans 166,5667
(defsubst span-detached-p 180,6200
(defsubst set-span-face 184,6316
(defsubst set-span-keymap 188,6414
(defsubst span-delete-spans 196,6583
(defsubst span-property-safe 200,6745
(defsubst span-set-start 204,6882
(defsubst span-set-end 208,7014

lib/texi-docstring-magic.el,584
(defun texi-docstring-magic-find-face 88,3027
(defun texi-docstring-magic-splice-sep 93,3192
(defconst texi-docstring-magic-munge-table103,3497
(defun texi-docstring-magic-untabify 193,7260
(defun texi-docstring-magic-munge-docstring 203,7575
(defun texi-docstring-magic-texi 242,8856
(defun texi-docstring-magic-format-default 255,9296
(defun texi-docstring-magic-texi-for 271,9929
(defconst texi-docstring-magic-comment329,11888
(defun texi-docstring-magic 335,12042
(defun texi-docstring-magic-face-at-point 369,13121
(defun texi-docstring-magic-insert-magic 384,13644

lib/unicode-chars.el,80
(defvar unicode-chars-alist12,348
(defun unicode-chars-list-chars 5051,245975

lib/unicode-tokens.el,5902
(defgroup unicode-tokens-options 55,1712
(defcustom unicode-tokens-add-help-echo 60,1837
(defun unicode-tokens-toggle-add-help-echo 65,2004
(defvar unicode-tokens-token-symbol-map 79,2410
(defvar unicode-tokens-token-format 98,3032
(defvar unicode-tokens-token-variant-format-regexp 104,3281
(defvar unicode-tokens-shortcut-alist 118,3814
(defvar unicode-tokens-shortcut-replacement-alist 124,4091
(defvar unicode-tokens-control-region-format-regexp 132,4297
(defvar unicode-tokens-control-char-format-regexp 139,4665
(defvar unicode-tokens-control-regions 146,5026
(defvar unicode-tokens-control-characters 149,5102
(defvar unicode-tokens-control-char-format 152,5184
(defvar unicode-tokens-control-region-format-start 155,5297
(defvar unicode-tokens-control-region-format-end 158,5414
(defvar unicode-tokens-tokens-customizable-variables 161,5527
(defconst unicode-tokens-configuration-variables168,5695
(defun unicode-tokens-config 183,6094
(defun unicode-tokens-config-var 187,6239
(defun unicode-tokens-copy-configuration-variables 199,6679
(defvar unicode-tokens-token-list 227,7895
(defvar unicode-tokens-hash-table 230,8015
(defvar unicode-tokens-token-match-regexp 233,8131
(defvar unicode-tokens-uchar-hash-table 239,8414
(defvar unicode-tokens-uchar-regexp 243,8601
(defgroup unicode-tokens-faces 251,8786
(defconst unicode-tokens-font-family-alternatives261,9083
(defface unicode-tokens-symbol-font-face276,9580
(defface unicode-tokens-script-font-face286,9918
(defface unicode-tokens-fraktur-font-face291,10062
(defface unicode-tokens-serif-font-face296,10187
(defface unicode-tokens-sans-font-face301,10324
(defface unicode-tokens-highlight-face306,10446
(defconst unicode-tokens-fonts315,10808
(defconst unicode-tokens-fontsymb-properties324,11025
(define-widget 'unicode-tokens-token-symbol-map unicode-tokens-token-symbol-map
352,12641
(define-widget 'unicode-tokens-shortcut-alist unicode-tokens-shortcut-alist
370,13193
(defconst unicode-tokens-font-lock-extra-managed-props383,13524
(defun unicode-tokens-font-lock-keywords 387,13678
(defun unicode-tokens-calculate-token-match 420,15049
(defun unicode-tokens-usable-composition 450,16087
(defun unicode-tokens-help-echo 463,16466
(defvar unicode-tokens-show-symbols 468,16668
(defun unicode-tokens-interpret-composition 471,16782
(defun unicode-tokens-font-lock-compose-symbol 489,17294
(defun unicode-tokens-prepend-text-properties-in-match 520,18576
(defun unicode-tokens-prepend-text-property 534,19154
(defun unicode-tokens-show-symbols 559,20299
(defun unicode-tokens-symbs-to-props 567,20609
(defvar unicode-tokens-show-controls 587,21308
(defun unicode-tokens-show-controls 590,21399
(defun unicode-tokens-control-char 603,21984
(defun unicode-tokens-control-region 612,22423
(defun unicode-tokens-control-font-lock-keywords 623,22970
(defvar unicode-tokens-use-shortcuts 634,23294
(defun unicode-tokens-use-shortcuts 637,23397
(defun unicode-tokens-map-ordering 653,23993
(defun unicode-tokens-quail-define-rules 662,24346
(defun unicode-tokens-insert-token 685,25023
(defun unicode-tokens-annotate-region 694,25327
(defun unicode-tokens-insert-control 718,26165
(defun unicode-tokens-insert-uchar-as-token 728,26614
(defun unicode-tokens-delete-token-near-point 734,26835
(defun unicode-tokens-delete-backward-char 746,27276
(defun unicode-tokens-delete-char 757,27657
(defun unicode-tokens-delete-backward-1 768,28011
(defun unicode-tokens-delete-1 785,28614
(defun unicode-tokens-prev-token 801,29158
(defun unicode-tokens-rotate-token-forward 809,29455
(defun unicode-tokens-rotate-token-backward 836,30345
(defun unicode-tokens-replace-shortcut-match 841,30547
(defun unicode-tokens-replace-shortcuts 850,30917
(defun unicode-tokens-replace-unicode-match 864,31515
(defun unicode-tokens-replace-unicode 871,31816
(defun unicode-tokens-copy-token 888,32415
(define-button-type 'unicode-tokens-listunicode-tokens-list
895,32636
(defun unicode-tokens-list-tokens 901,32840
(defun unicode-tokens-list-shortcuts 940,34024
(defalias 'unicode-tokens-list-unicode-chars unicode-tokens-list-unicode-chars
958,34662
(defun unicode-tokens-encode-in-temp-buffer 960,34735
(defun unicode-tokens-encode 978,35391
(defun unicode-tokens-encode-str 984,35627
(defun unicode-tokens-copy 988,35789
(defun unicode-tokens-paste 997,36195
(defvar unicode-tokens-highlight-unicode 1016,36916
(defconst unicode-tokens-unicode-highlight-patterns1019,37008
(defun unicode-tokens-highlight-unicode 1023,37177
(defun unicode-tokens-highlight-unicode-setkeywords 1035,37640
(defun unicode-tokens-initialise 1047,38009
(defvar unicode-tokens-mode-map 1067,38680
(defvar unicode-tokens-display-table 1070,38777
(define-minor-mode unicode-tokens-mode1077,39029
(defun unicode-tokens-set-font-var 1210,43512
(defun unicode-tokens-set-font-var-aux 1226,44001
(defun unicode-tokens-mouse-set-font 1258,45282
(defsubst unicode-tokens-face-font-sym 1271,45796
(defun unicode-tokens-set-font-restart 1275,45976
(defun unicode-tokens-save-fonts 1286,46286
(defun unicode-tokens-custom-save-faces 1294,46542
(define-key unicode-tokens-mode-map1311,46998
(define-key unicode-tokens-mode-map1314,47105
(defvar unicode-tokens-quail-translation-keymap 1318,47195
(define-key unicode-tokens-quail-translation-keymap 1324,47361
(defun unicode-tokens-quail-delete-last-char 1328,47496
(define-key unicode-tokens-mode-map 1344,47946
(define-key unicode-tokens-mode-map 1346,48038
(define-key unicode-tokens-mode-map1348,48129
(define-key unicode-tokens-mode-map1350,48235
(define-key unicode-tokens-mode-map1353,48350
(define-key unicode-tokens-mode-map1355,48459
(define-key unicode-tokens-mode-map1357,48567
(define-key unicode-tokens-mode-map1359,48673
(defun unicode-tokens-customize-submenu 1367,48797
(defun unicode-tokens-define-menu 1374,49020

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,6347
@node Top164,4936
@node Preface202,6090
@node News for Version 4.0News for Version 4.0
225,6679
@node Future246,7472
@node Credits275,8807
@node Introducing Proof GeneralIntroducing Proof General
387,12712
@node Installing Proof GeneralInstalling Proof General
442,14690
@node Quick start guideQuick start guide
456,15139
@node Features of Proof GeneralFeatures of Proof General
500,17260
@node Supported proof assistantsSupported proof assistants
589,21197
@node Prerequisites for this manualPrerequisites for this manual
638,23086
@node Organization of this manualOrganization of this manual
682,24705
@node Basic Script ManagementBasic Script Management
708,25533
@node Walkthrough example in IsabelleWalkthrough example in Isabelle
727,26133
@node Proof scriptsProof scripts
993,36384
@node Script buffersScript buffers
1036,38504
@node Locked queue and editing regionsLocked queue and editing regions
1058,39081
@node Goal-save sequencesGoal-save sequences
1114,41228
@node Active scripting bufferActive scripting buffer
1151,42694
@node Summary of Proof General buffersSummary of Proof General buffers
1220,46114
@node Script editing commandsScript editing commands
1283,48854
@node Script processing commandsScript processing commands
1363,51812
@node Proof assistant commandsProof assistant commands
1490,57105
@node Toolbar commandsToolbar commands
1665,63298
@node Interrupting during trace outputInterrupting during trace output
1689,64227
@node Advanced Script Management and EditingAdvanced Script Management and Editing
1729,66157
@node Document centred workingDocument centred working
1761,67372
@node Visibility of completed proofsVisibility of completed proofs
1838,69952
@node Switching between proof scriptsSwitching between proof scripts
1893,71881
@node View of processed files View of processed files 
1930,73853
@node Retracting across filesRetracting across files
1990,76904
@node Asserting across filesAsserting across files
2003,77535
@node Automatic multiple file handlingAutomatic multiple file handling
2016,78101
@node Escaping script managementEscaping script management
2041,79135
@node Editing featuresEditing features
2098,81247
@node Unicode symbols and special layout supportUnicode symbols and special layout support
2168,84026
@node Maths menuMaths menu
2210,85584
@node Unicode Tokens modeUnicode Tokens mode
2227,86275
@node Configuring tokens symbols and shortcutsConfiguring tokens symbols and shortcuts
2277,88698
@node Special layout Special layout 
2307,89659
@node Moving between Unicode and tokensMoving between Unicode and tokens
2415,93775
@node Finding available tokens shortcuts and symbolsFinding available tokens shortcuts and symbols
2470,95886
@node Selecting suitable fontsSelecting suitable fonts
2509,97060
@node Support for other PackagesSupport for other Packages
2574,100035
@node Syntax highlightingSyntax highlighting
2604,100871
@node Imenu and SpeedbarImenu and Speedbar
2632,101874
@node Support for outline modeSupport for outline mode
2678,103530
@node Support for completionSupport for completion
2703,104659
@node Support for tagsSupport for tags
2760,106821
@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
2812,109169
@node Goals buffer commandsGoals buffer commands
2827,109681
@node Customizing Proof GeneralCustomizing Proof General
2915,113216
@node Basic optionsBasic options
2955,114886
@node How to customizeHow to customize
2979,115656
@node Display customizationDisplay customization
3026,117623
@node User optionsUser options
3180,124028
@node Changing facesChanging faces
3420,132540
@node Script buffer facesScript buffer faces
3442,133415
@node Goals and response facesGoals and response faces
3488,135015
@node Tweaking configuration settingsTweaking configuration settings
3533,136547
@node Hints and TipsHints and Tips
3590,139073
@node Adding your own keybindingsAdding your own keybindings
3609,139674
@node Using file variablesUsing file variables
3673,142288
@node Using abbreviationsUsing abbreviations
3732,144474
@node LEGO Proof GeneralLEGO Proof General
3771,145889
@node LEGO specific commandsLEGO specific commands
3812,147258
@node LEGO tagsLEGO tags
3832,147713
@node LEGO customizationsLEGO customizations
3842,147960
@node Coq Proof GeneralCoq Proof General
3874,148879
@node Coq-specific commandsCoq-specific commands
3890,149288
@node Coq-specific variablesCoq-specific variables
3912,149795
@node Editing multiple proofsEditing multiple proofs
3934,150453
@node User-loaded tacticsUser-loaded tactics
3958,151561
@node Holes featureHoles feature
4022,154035
@node Isabelle Proof GeneralIsabelle Proof General
4049,155322
@node Choosing logic and starting isabelleChoosing logic and starting isabelle
4075,156198
@node Isabelle commandsIsabelle commands
4144,158999
@node Isabelle settingsIsabelle settings
4287,163191
@node Isabelle customizationsIsabelle customizations
4301,163773
@node HOL Proof GeneralHOL Proof General
4324,164260
@node Shell Proof GeneralShell Proof General
4366,166082
@node Obtaining and InstallingObtaining and Installing
4402,167541
@node Obtaining Proof GeneralObtaining Proof General
4418,167954
@node Installing Proof General from tarballInstalling Proof General from tarball
4449,169193
@node Installing Proof General from RPM packageInstalling Proof General from RPM package
4474,170025
@node Setting the names of binariesSetting the names of binaries
4489,170433
@node Notes for syssiesNotes for syssies
4517,171373
@node Bugs and EnhancementsBugs and Enhancements
4592,174409
@node References4613,175224
@node History of Proof GeneralHistory of Proof General
4653,176247
@node Old News for 3.0Old News for 3.0
4747,180412
@node Old News for 3.1Old News for 3.1
4817,184106
@node Old News for 3.2Old News for 3.2
4843,185278
@node Old News for 3.3Old News for 3.3
4904,188281
@node Old News for 3.4Old News for 3.4
4923,189178
@node Old News for 3.5Old News for 3.5
4945,190233
@node Old News for 3.6Old News for 3.6
4949,190290
@node Old News for 3.7Old News for 3.7
4954,190390
@node Function IndexFunction Index
4998,192301
@node Variable IndexVariable Index
5002,192377
@node Keystroke IndexKeystroke Index
5006,192457
@node Concept IndexConcept Index
5010,192523

doc/PG-adapting.texi,3770
@node Top155,4688
@node Introduction192,5797
@node Future233,7450
@node Credits269,9046
@node Beginning with a New ProverBeginning with a New Prover
279,9338
@node Overview of adding a new proverOverview of adding a new prover
319,11280
@node Demonstration instance and easy configurationDemonstration instance and easy configuration
396,14586
@node Major modes used by Proof GeneralMajor modes used by Proof General
465,17977
@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands
508,19687
@node Settings for generic user-level commandsSettings for generic user-level commands
523,20233
@node Menu configurationMenu configuration
568,21965
@node Toolbar configurationToolbar configuration
592,22882
@node Proof Script SettingsProof Script Settings
651,25119
@node Recognizing commands and commentsRecognizing commands and comments
673,25699
@node Recognizing proofsRecognizing proofs
810,32136
@node Recognizing other elementsRecognizing other elements
914,36450
@node Configuring undo behaviourConfiguring undo behaviour
977,38929
@node Nested proofsNested proofs
1114,44316
@node Safe (state-preserving) commandsSafe (state-preserving) commands
1154,45942
@node Activate scripting hookActivate scripting hook
1177,46895
@node Automatic multiple filesAutomatic multiple files
1201,47765
@node Completions1223,48612
@node Proof Shell SettingsProof Shell Settings
1264,50102
@node Proof shell commandsProof shell commands
1295,51384
@node Script input to the shellScript input to the shell
1459,58428
@node Settings for matching various output from proof processSettings for matching various output from proof process
1527,61498
@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process
1649,66854
@node Hooks and other settingsHooks and other settings
1889,77612
@node Goals Buffer SettingsGoals Buffer Settings
1974,81125
@node Splash Screen SettingsSplash Screen Settings
2048,84115
@node Global ConstantsGlobal Constants
2074,84870
@node Handling Multiple FilesHandling Multiple Files
2100,85699
@node Configuring Editing SyntaxConfiguring Editing Syntax
2252,93482
@node Configuring Font LockConfiguring Font Lock
2309,95599
@node Configuring TokensConfiguring Tokens
2381,99093
@node Writing More Lisp CodeWriting More Lisp Code
2431,101213
@node Default values for generic settingsDefault values for generic settings
2448,101858
@node Adding prover-specific configurationsAdding prover-specific configurations
2478,102941
@node Useful variablesUseful variables
2521,104223
@node Useful functions and macrosUseful functions and macros
2536,104722
@node Internals of Proof GeneralInternals of Proof General
2645,108945
@node Spans2673,109841
@node Proof General site configurationProof General site configuration
2685,110163
@node Configuration variable mechanismsConfiguration variable mechanisms
2765,113208
@node Global variablesGlobal variables
2886,118645
@node Proof script modeProof script mode
2956,121193
@node Proof shell modeProof shell mode
3185,131502
@node Debugging3682,151327
@node Plans and IdeasPlans and Ideas
3725,152203
@node Proof by pointing and similar featuresProof by pointing and similar features
3746,152925
@node Granularity of atomic command sequencesGranularity of atomic command sequences
3784,154583
@node Browser mode for script files and theoriesBrowser mode for script files and theories
3829,156808
@node Demonstration InstantiationsDemonstration Instantiations
3859,157839
@node demoisa-easy.el3875,158270
@node demoisa.el3937,160462
@node Function IndexFunction Index
4091,165402
@node Variable IndexVariable Index
4095,165478
@node Concept IndexConcept Index
4104,165657

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