path: root/TAGS


coq/coq-abbrev.el,495
(defun holes-show-doc 10,309
(defun coq-local-vars-list-show-doc 14,386
(defconst coq-tactics-menu19,486
(defconst coq-tactics-abbrev-table24,663
(defconst coq-tacticals-menu27,780
(defconst coq-tacticals-abbrev-table31,889
(defconst coq-commands-menu34,980
(defconst coq-commands-abbrev-table41,1203
(defconst coq-terms-menu44,1292
(defconst coq-terms-abbrev-table49,1430
(defun coq-install-abbrevs 56,1624
(defpgdefault menu-entries76,2361
(defpgdefault help-menu-entries149,4975

coq/coq-db.el,600
(defconst coq-syntax-db 22,533
(defvar coq-user-tactics-db58,1906
(defun coq-insert-from-db 68,2255
(defun coq-build-regexp-list-from-db 86,2987
(defun max-length-db 108,3970
(defun coq-build-menu-from-db-internal 120,4245
(defun coq-build-title-menu 155,5868
(defun coq-sort-menu-entries 164,6236
(defun coq-build-menu-from-db 170,6363
(defcustom coq-holes-minor-mode 192,7198
(defun coq-build-abbrev-table-from-db 198,7342
(defun filter-state-preserving 217,7980
(defun filter-state-changing 222,8134
(defface coq-solve-tactics-face229,8355
(defconst coq-solve-tactics-face 237,8611

coq/coq.el,6544
(defcustom coq-translate-to-v8 45,1299
(defun coq-build-prog-args 51,1479
(defcustom coq-compile-file-command 64,1857
(defcustom coq-use-makefile 72,2176
(defcustom coq-default-undo-limit 80,2399
(defconst coq-shell-init-cmd85,2527
(defcustom coq-prog-env 97,2803
(defconst coq-shell-restart-cmd 105,3053
(defvar coq-shell-prompt-pattern112,3311
(defvar coq-shell-cd 122,3702
(defvar coq-shell-abort-goal-regexp 126,3862
(defvar coq-shell-proof-completed-regexp 129,3988
(defvar coq-goal-regexp132,4140
(defun coq-library-directory 139,4254
(defcustom coq-tags 146,4433
(defconst coq-interrupt-regexp 151,4583
(defcustom coq-www-home-page 156,4704
(defvar coq-outline-regexp166,4875
(defvar coq-outline-heading-end-regexp 173,5087
(defvar coq-shell-outline-regexp 175,5141
(defvar coq-shell-outline-heading-end-regexp 176,5191
(defconst coq-kill-goal-command 181,5301
(defconst coq-forget-id-command 182,5344
(defconst coq-back-n-command 183,5391
(defconst coq-state-preserving-tactics-regexp187,5535
(defconst coq-state-changing-commands-regexp189,5635
(defconst coq-state-preserving-commands-regexp191,5742
(defconst coq-commands-regexp193,5853
(defvar coq-retractable-instruct-regexp195,5930
(defvar coq-non-retractable-instruct-regexp197,6020
(defvar coq-keywords-section201,6159
(defvar coq-section-regexp204,6253
(defun coq-set-undo-limit 241,7394
(defconst coq-keywords-decl-defn-regexp252,7832
(defun coq-proof-mode-p 256,7982
(defun coq-is-comment-or-proverprocp 267,8389
(defun coq-is-goalsave-p 269,8492
(defun coq-is-module-equal-p 270,8567
(defun coq-is-def-p 273,8763
(defun coq-is-decl-defn-p 275,8870
(defun coq-state-preserving-command-p 280,9035
(defun coq-command-p 283,9169
(defun coq-state-preserving-tactic-p 286,9269
(defun coq-state-changing-tactic-p 291,9415
(defun coq-state-changing-command-p 298,9648
(defun coq-section-or-module-start-p 305,9993
(defun build-list-id-from-string 314,10231
(defun coq-last-prompt-info 327,10761
(defun coq-last-prompt-info-safe 339,11301
(defvar coq-last-but-one-statenum 345,11558
(defvar coq-last-but-one-proofnum 351,11855
(defvar coq-last-but-one-proofstack 354,11953
(defun coq-get-span-statenum 357,12063
(defun coq-get-span-proofnum 362,12178
(defun coq-get-span-proofstack 367,12293
(defun coq-set-span-statenum 372,12437
(defun coq-get-span-goalcmd 377,12568
(defun coq-set-span-goalcmd 382,12682
(defun coq-set-span-proofnum 387,12812
(defun coq-set-span-proofstack 392,12943
(defun proof-last-locked-span 397,13103
(defun coq-set-state-infos 412,13706
(defun count-not-intersection 452,15780
(defun  coq-find-and-forget-v81 483,17030
(defun coq-find-and-forget-v80 510,18182
(defun coq-find-and-forget 605,22885
(defvar coq-current-goal 618,23422
(defun coq-goal-hyp 621,23487
(defun coq-state-preserving-p 634,23919
(defconst notation-print-kinds-table648,24420
(defun coq-PrintScope 652,24587
(defun coq-guess-or-ask-for-string 670,25136
(defun coq-ask-do 684,25704
(defun coq-SearchIsos 693,26089
(defun coq-SearchConstant 699,26322
(defun coq-SearchRewrite 703,26415
(defun coq-SearchAbout 707,26513
(defun coq-Print 711,26605
(defun coq-About 715,26727
(defun coq-LocateConstant 719,26844
(defun coq-LocateLibrary 725,26979
(defun coq-addquotes 731,27129
(defun coq-LocateNotation 733,27177
(defun coq-Pwd 740,27375
(defun coq-Inspect 746,27507
(defun coq-PrintSection(750,27607
(defun coq-Print-implicit 754,27700
(defun coq-Check 759,27851
(defun coq-Show 764,27959
(defun coq-Compile 778,28402
(defun coq-guess-command-line 792,28722
(defpacustom use-editing-holes 831,30428
(defun coq-mode-config 841,30765
(defvar coq-last-hybrid-pre-string 949,34712
(defun coq-hybrid-ouput-goals-response-p 952,34891
(defun coq-hybrid-ouput-goals-response 958,35141
(defun coq-shell-mode-config 979,36100
(defun coq-goals-mode-config 1026,38065
(defun coq-response-config 1033,38309
(defpacustom print-fully-explicit 1058,39134
(defpacustom print-implicit 1063,39282
(defpacustom print-coercions 1068,39448
(defpacustom print-match-wildcards 1073,39592
(defpacustom print-elim-types 1078,39772
(defpacustom printing-depth 1083,39938
(defpacustom undo-depth 1088,40099
(defpacustom time-commands 1093,40246
(defpacustom undo-limit 1097,40356
(defpacustom auto-compile-vos 1102,40458
(defun coq-maybe-compile-buffer 1131,41572
(defun coq-ancestors-of 1168,43101
(defun coq-all-ancestors-of 1191,44065
(defconst coq-require-command-regexp1203,44458
(defun coq-process-require-command 1208,44664
(defun coq-included-children 1213,44791
(defun coq-process-file 1234,45630
(defun coq-preprocessing 1249,46169
(defun coq-fake-constant-markup 1264,46582
(defun coq-create-span-menu 1285,47386
(defconst module-kinds-table1302,47883
(defconst modtype-kinds-table1306,48032
(defun coq-insert-section-or-module 1310,48161
(defconst reqkinds-kinds-table1333,49019
(defun coq-insert-requires 1338,49164
(defun coq-end-Section 1354,49667
(defun coq-insert-intros 1372,50245
(defun coq-insert-infoH-hook 1385,50777
(defun coq-insert-as 1389,50855
(defun coq-insert-match 1410,51602
(defun coq-insert-tactic 1442,52784
(defun coq-insert-tactical 1448,53023
(defun coq-insert-command 1454,53272
(defun coq-insert-term 1460,53516
(define-key coq-keymap 1466,53713
(define-key coq-keymap 1467,53771
(define-key coq-keymap 1468,53828
(define-key coq-keymap 1469,53897
(define-key coq-keymap 1470,53953
(define-key coq-keymap 1471,54002
(define-key coq-keymap 1472,54060
(define-key coq-keymap 1474,54121
(define-key coq-keymap 1475,54180
(define-key coq-keymap 1477,54244
(define-key coq-keymap 1478,54304
(define-key coq-keymap 1480,54360
(define-key coq-keymap 1481,54410
(define-key coq-keymap 1482,54460
(define-key coq-keymap 1483,54510
(define-key coq-keymap 1484,54564
(define-key coq-keymap 1485,54623
(defvar last-coq-error-location 1493,54754
(defun coq-get-last-error-location 1502,55153
(defun coq-highlight-error 1549,57491
(defvar coq-allow-highlight-error 1584,58710
(defun coq-decide-highlight-error 1591,59037
(defun coq-highlight-error-hook 1595,59159
(defun first-word-of-buffer 1606,59552
(defun coq-show-first-goal 1614,59755
(defvar coq-modeline-string2 1631,60450
(defvar coq-modeline-string1 1632,60494
(defvar coq-modeline-string0 1633,60537
(defun coq-build-subgoals-string 1634,60582
(defun coq-update-minor-mode-alist 1639,60748
(defun is-not-split-vertic 1665,61819
(defun optim-resp-windows 1674,62258

coq/coq-indent.el,2222
(defconst coq-any-command-regexp17,314
(defconst coq-indent-inner-regexp20,405
(defconst coq-comment-start-regexp 30,759
(defconst coq-comment-end-regexp 31,802
(defconst coq-comment-start-or-end-regexp32,843
(defconst coq-indent-open-regexp34,951
(defconst coq-indent-close-regexp39,1125
(defconst coq-indent-closepar-regexp 44,1306
(defconst coq-indent-closematch-regexp 45,1351
(defconst coq-indent-openpar-regexp 46,1422
(defconst coq-indent-openmatch-regexp 47,1466
(defconst coq-indent-any-regexp48,1546
(defconst coq-indent-kw53,1824
(defconst coq-indent-pattern-regexp 63,2278
(defun coq-indent-goal-command-p 67,2381
(defconst coq-end-command-regexp89,3432
(defun coq-search-comment-delimiter-forward 94,3584
(defun coq-search-comment-delimiter-backward 103,3914
(defun coq-skip-until-one-comment-backward 110,4188
(defun coq-skip-until-one-comment-forward 125,4895
(defun coq-looking-at-comment 136,5413
(defun coq-find-comment-start 140,5554
(defun coq-find-comment-end 151,5987
(defun coq-looking-at-syntactic-context 163,6480
(defconst coq-end-command-or-comment-regexp169,6702
(defconst coq-end-command-or-comment-start-regexp172,6811
(defun coq-find-not-in-comment-backward 176,6929
(defun coq-find-not-in-comment-forward 196,7830
(defun coq-find-command-end-backward 220,8969
(defun coq-find-command-end-forward 229,9360
(defun coq-find-command-end 238,9737
(defun coq-find-current-start 246,10069
(defun coq-find-real-start 255,10360
(defun coq-command-at-point 262,10579
(defun coq-indent-only-spaces-on-line 269,10856
(defun coq-indent-find-reg 275,11133
(defun coq-find-no-syntactic-on-line 289,11669
(defun coq-back-to-indentation-prevline 302,12142
(defun coq-find-unclosed 346,14050
(defun coq-find-at-same-level-zero 376,15346
(defun coq-find-unopened 404,16504
(defun coq-find-last-unopened 447,17938
(defun coq-end-offset 458,18335
(defun coq-indent-command-offset 483,19105
(defun coq-indent-expr-offset 530,20929
(defun coq-indent-comment-offset 646,25612
(defun coq-indent-offset 678,27061
(defun coq-indent-calculate 696,27923
(defun coq-indent-line 699,28011
(defun coq-indent-line-not-comments 709,28377
(defun coq-indent-region 719,28766

coq/coq-local-vars.el,280
(defconst coq-local-vars-doc 17,303
(defun coq-insert-coq-prog-name 75,2831
(defun coq-read-directory 86,3304
(defun coq-extract-directories-from-args 110,4407
(defun coq-ask-prog-args 125,4959
(defun coq-ask-prog-name 147,6063
(defun coq-ask-insert-coq-prog-name 165,6818

coq/coq-syntax.el,2665
(defcustom coq-prog-name 13,428
(defvar coq-version-is-V8 34,1427
(defvar coq-version-is-V8-0 36,1506
(defvar coq-version-is-V8-1 43,1883
(defun coq-determine-version 52,2315
(defcustom coq-user-tactics-db 97,4172
(defcustom coq-user-commands-db 114,4685
(defcustom coq-user-tacticals-db 130,5204
(defcustom coq-user-solve-tactics-db 146,5725
(defcustom coq-user-reserved-db 164,6246
(defvar coq-tactics-db182,6777
(defvar coq-solve-tactics-db337,14844
(defvar coq-tacticals-db361,15690
(defvar coq-decl-db385,16576
(defvar coq-defn-db407,17793
(defvar coq-goal-starters-db460,21777
(defvar coq-other-commands-db487,23332
(defvar coq-commands-db611,32526
(defvar coq-terms-db618,32746
(defun coq-count-match 682,35395
(defun coq-goal-command-str-v80-p 701,36257
(defun coq-module-opening-p 724,37122
(defun coq-section-command-p 735,37533
(defun coq-goal-command-str-v81-p 739,37630
(defun coq-goal-command-p-v81 754,38299
(defun coq-goal-command-str-p 764,38637
(defun coq-goal-command-p 774,39002
(defvar coq-keywords-save-strict782,39313
(defvar coq-keywords-save791,39426
(defun coq-save-command-p 795,39504
(defvar coq-keywords-kill-goal804,39798
(defvar coq-keywords-state-changing-misc-commands808,39888
(defvar coq-keywords-goal811,40013
(defvar coq-keywords-decl814,40096
(defvar coq-keywords-defn817,40170
(defvar coq-keywords-state-changing-commands821,40245
(defvar coq-keywords-state-preserving-commands830,40505
(defvar coq-keywords-commands835,40721
(defvar coq-solve-tactics840,40869
(defvar coq-tacticals844,40990
(defvar coq-reserved850,41129
(defvar coq-state-changing-tactics861,41457
(defvar coq-state-preserving-tactics864,41566
(defvar coq-tactics868,41680
(defvar coq-retractable-instruct871,41769
(defvar coq-non-retractable-instruct874,41879
(defvar coq-keywords878,42007
(defvar coq-symbols885,42174
(defvar coq-error-regexp 904,42387
(defvar coq-id 907,42615
(defvar coq-id-shy 908,42640
(defvar coq-ids 910,42694
(defun coq-first-abstr-regexp 912,42735
(defcustom coq-variable-highlight-enable 915,42830
(defvar coq-font-lock-terms921,42957
(defconst coq-save-command-regexp-strict942,43956
(defconst coq-save-command-regexp946,44122
(defconst coq-save-with-hole-regexp950,44274
(defconst coq-goal-command-regexp954,44432
(defconst coq-goal-with-hole-regexp957,44532
(defconst coq-decl-with-hole-regexp961,44664
(defconst coq-defn-with-hole-regexp968,44912
(defconst coq-with-with-hole-regexp978,45200
(defvar coq-font-lock-keywords-1984,45492
(defvar coq-font-lock-keywords 1011,46821
(defun coq-init-syntax-table 1013,46879
(defconst coq-generic-expression1042,47777

coq/coq-unicode-tokens.el,410
(defconst coq-token-format 18,631
(defconst coq-token-match 19,664
(defconst coq-hexcode-match 20,695
(defcustom coq-token-symbol-map22,729
(defcustom coq-shortcut-alist88,2382
(defconst coq-control-char-format-regexp177,4388
(defconst coq-control-char-format 181,4513
(defconst coq-control-characters183,4556
(defconst coq-control-region-format-regexp 187,4648
(defconst coq-control-regions189,4731

demoisa/demoisa.el,349
(defcustom isabelledemo-prog-name 54,1805
(defcustom isabelledemo-web-page59,1927
(defun demoisa-config 70,2157
(defun demoisa-shell-config 91,2949
(define-derived-mode demoisa-mode 116,3878
(define-derived-mode demoisa-shell-mode 121,4001
(define-derived-mode demoisa-response-mode 126,4144
(define-derived-mode demoisa-goals-mode 130,4271

isar/isabelle-system.el,1291
(defgroup isabelle 26,776
(defcustom isabelle-web-page30,904
(defcustom isa-isabelle-command39,1121
(defvar isabelle-not-found 57,1803
(defun isa-set-isabelle-command 60,1918
(defun isa-shell-command-to-string 83,2936
(defun isa-getenv 89,3160
(defcustom isabelle-program-name-override 109,3852
(defvar isabelle-prog-name 120,4198
(defun isa-tool-list-logics 123,4308
(defcustom isabelle-logics-available 130,4547
(defcustom isabelle-chosen-logic 140,4884
(defvar isabelle-chosen-logic-prev 156,5468
(defun isabelle-hack-local-variables-function 159,5588
(defun isabelle-set-prog-name 171,6027
(defun isabelle-choose-logic 196,7217
(defun isa-view-doc 215,7979
(defun isa-tool-list-docs 224,8244
(defconst isabelle-verbatim-regexp 242,8967
(defun isabelle-verbatim 245,9109
(defcustom isabelle-refresh-logics 252,9270
(defvar isabelle-docs-menu260,9598
(defvar isabelle-logics-menu-entries 267,9883
(defun isabelle-logics-menu-calculate 270,9956
(defvar isabelle-time-to-refresh-logics 291,10598
(defun isabelle-logics-menu-refresh 295,10693
(defun isabelle-menu-bar-update-logics 310,11326
(defun isabelle-load-isar-keywords 326,11955
(defun isabelle-create-span-menu 347,12683
(defun isabelle-xml-sml-escapes 363,13125
(defun isabelle-process-pgip 366,13226

isar/isar.el,1530
(defcustom isar-keywords-name 33,762
(defpgdefault completion-table 50,1285
(defcustom isar-web-page52,1338
(defun isar-strip-terminators 66,1688
(defun isar-markup-ml 79,2065
(defun isar-mode-config-set-variables 84,2200
(defun isar-shell-mode-config-set-variables 157,5304
(defun isar-configure-from-settings 239,8493
(defpacustom use-find-theorems-form 242,8575
(defun isar-set-proof-find-theorems-command 247,8741
(defun isar-remove-file 257,8963
(defun isar-shell-compute-new-files-list 267,9318
(define-derived-mode isar-shell-mode 285,9890
(define-derived-mode isar-response-mode 290,10013
(define-derived-mode isar-goals-mode 295,10141
(define-derived-mode isar-mode 300,10262
(defpgdefault menu-entries357,12284
(defalias 'isar-set-command isar-set-command
387,13441
(defpgdefault help-menu-entries 389,13497
(defun isar-count-undos 392,13573
(defun isar-find-and-forget 418,14508
(defun isar-goal-command-p 458,16035
(defun isar-global-save-command-p 463,16212
(defvar isar-current-goal 484,16996
(defun isar-state-preserving-p 487,17062
(defvar isar-shell-current-line-width 512,18259
(defun isar-shell-adjust-line-width 517,18451
(defun isar-string-wrapping 542,19250
(defun isar-positions-of 551,19447
(defun isar-command-wrapping 575,20151
(defcustom isar-wrap-commands-singly 584,20495
(defun isar-preprocessing 590,20691
(defun isar-mode-config 610,21345
(defun isar-shell-mode-config 621,21903
(defun isar-response-mode-config 627,22100
(defun isar-goals-mode-config 637,22435

isar/isar-find-theorems.el,778
(defun isar-find-theorems-minibuffer 18,713
(defun isar-find-theorems-form 32,1332
(defvar isar-find-theorems-data 74,3132
(defvar isar-find-theorems-widget-number 88,3467
(defvar isar-find-theorems-widget-pattern 91,3565
(defvar isar-find-theorems-widget-intro 94,3657
(defvar isar-find-theorems-widget-elim 97,3743
(defvar isar-find-theorems-widget-dest 100,3827
(defvar isar-find-theorems-widget-name 103,3911
(defvar isar-find-theorems-widget-simp 106,3998
(defun isar-find-theorems-create-searchform111,4144
(defun isar-find-theorems-create-help 251,8687
(defun isar-find-theorems-submit-searchform294,10859
(defun isar-find-theorems-parse-criteria 372,13229
(defun isar-find-theorems-parse-number 465,16210
(defun isar-find-theorems-filter-empty 475,16487

isar/isar-keywords.el,1052
(defconst isar-keywords-major13,481
(defconst isar-keywords-minor206,3641
(defconst isar-keywords-control262,4395
(defconst isar-keywords-diag282,4872
(defconst isar-keywords-theory-begin338,5831
(defconst isar-keywords-theory-switch341,5884
(defconst isar-keywords-theory-end344,5939
(defconst isar-keywords-theory-heading347,5987
(defconst isar-keywords-theory-decl353,6094
(defconst isar-keywords-theory-script412,7075
(defconst isar-keywords-theory-goal416,7152
(defconst isar-keywords-qed429,7369
(defconst isar-keywords-qed-block436,7455
(defconst isar-keywords-qed-global439,7502
(defconst isar-keywords-proof-heading442,7551
(defconst isar-keywords-proof-goal447,7634
(defconst isar-keywords-proof-block454,7733
(defconst isar-keywords-proof-open458,7795
(defconst isar-keywords-proof-close461,7841
(defconst isar-keywords-proof-chain464,7888
(defconst isar-keywords-proof-decl471,7991
(defconst isar-keywords-proof-asm480,8112
(defconst isar-keywords-proof-asm-goal487,8207
(defconst isar-keywords-proof-script490,8262

isar/isar-mmm.el,81
(defconst isar-start-latex-regexp24,744
(defconst isar-start-sml-regexp36,1172

isar/isar-syntax.el,3653
(defconst isar-script-syntax-table-entries18,424
(defconst isar-script-syntax-table-alist42,826
(defun isar-init-syntax-table 51,1109
(defun isar-init-output-syntax-table 59,1356
(defconst isar-keyword-begin 75,1803
(defconst isar-keyword-end 76,1841
(defconst isar-keywords-theory-enclose78,1876
(defconst isar-keywords-theory83,2014
(defconst isar-keywords-save88,2145
(defconst isar-keywords-proof-enclose93,2260
(defconst isar-keywords-proof99,2421
(defconst isar-keywords-proof-context106,2598
(defconst isar-keywords-local-goal110,2705
(defconst isar-keywords-proper114,2810
(defconst isar-keywords-improper119,2929
(defconst isar-keywords-outline124,3061
(defconst isar-keywords-fume127,3126
(defconst isar-keywords-indent-open134,3316
(defconst isar-keywords-indent-close140,3479
(defconst isar-keywords-indent-enclose144,3577
(defun isar-regexp-simple-alt 153,3771
(defun isar-ids-to-regexp 173,4531
(defconst isar-ext-first 207,5916
(defconst isar-ext-rest 208,5983
(defconst isar-long-id-stuff 210,6055
(defconst isar-id 211,6129
(defconst isar-idx 212,6199
(defconst isar-string 214,6258
(defconst isar-any-command-regexp216,6318
(defconst isar-name-regexp220,6452
(defconst isar-improper-regexp226,6747
(defconst isar-save-command-regexp230,6895
(defconst isar-global-save-command-regexp233,6996
(defconst isar-goal-command-regexp236,7110
(defconst isar-local-goal-command-regexp239,7218
(defconst isar-comment-start 242,7331
(defconst isar-comment-end 243,7366
(defconst isar-comment-start-regexp 244,7399
(defconst isar-comment-end-regexp 245,7470
(defconst isar-string-start-regexp 247,7538
(defconst isar-string-end-regexp 248,7590
(defun isar-syntactic-context 250,7641
(defconst isar-antiq-regexp265,8036
(defconst isar-nesting-regexp271,8187
(defun isar-nesting 274,8285
(defun isar-match-nesting 286,8678
(defface isabelle-class-name-face298,9009
(defface isabelle-tfree-name-face306,9192
(defface isabelle-tvar-name-face314,9381
(defface isabelle-free-name-face322,9569
(defface isabelle-bound-name-face330,9753
(defface isabelle-var-name-face338,9940
(defconst isabelle-class-name-face 346,10127
(defconst isabelle-tfree-name-face 347,10189
(defconst isabelle-tvar-name-face 348,10251
(defconst isabelle-free-name-face 349,10312
(defconst isabelle-bound-name-face 350,10373
(defconst isabelle-var-name-face 351,10435
(defvar isar-font-lock-keywords-1354,10497
(defun isar-output-flkprops 372,11505
(defun isar-output-flk 378,11757
(defvar isar-output-font-lock-keywords-1381,11866
(defun isar-strip-output-markup 417,13289
(defvar isar-goals-font-lock-keywords421,13425
(defconst isar-linear-undo 455,14104
(defconst isar-undo 457,14147
(defun isar-remove 459,14190
(defun isar-undos 462,14265
(defun isar-cannot-undo 466,14382
(defconst isar-undo-commands469,14452
(defconst isar-theory-start-regexp477,14589
(defconst isar-end-regexp483,14747
(defconst isar-undo-fail-regexp487,14848
(defconst isar-undo-skip-regexp491,14952
(defconst isar-undo-ignore-regexp494,15073
(defconst isar-undo-remove-regexp497,15138
(defconst isar-any-entity-regexp505,15313
(defconst isar-named-entity-regexp510,15486
(defconst isar-unnamed-entity-regexp515,15649
(defconst isar-next-entity-regexps518,15751
(defconst isar-generic-expression526,16055
(defconst isar-indent-any-regexp537,16288
(defconst isar-indent-inner-regexp539,16381
(defconst isar-indent-enclose-regexp541,16447
(defconst isar-indent-open-regexp543,16563
(defconst isar-indent-close-regexp545,16673
(defconst isar-outline-regexp551,16810
(defconst isar-outline-heading-end-regexp 555,16963

isar/isar-unicode-tokens.el,1289
(defgroup isabelle-tokens 20,510
(defun isar-set-and-restart-tokens 25,650
(defconst isar-control-region-format-regexp38,1003
(defconst isar-control-char-format-regexp41,1097
(defconst isar-control-char-format	44,1192
(defconst isar-control-region-format-start 45,1241
(defconst isar-control-region-format-end 46,1295
(defcustom isar-control-characters49,1351
(defcustom isar-control-regions62,1723
(defconst isar-token-format 86,2439
(defconst isar-token-variant-format-regexp90,2590
(defcustom isar-greek-letters-tokens93,2704
(defcustom isar-misc-letters-tokens133,3562
(defcustom isar-symbols-tokens145,3880
(defcustom isar-extended-symbols-tokens351,8702
(defun isar-try-char 420,10357
(defcustom isar-symbols-tokens-fallbacks424,10501
(defcustom isar-bold-nums-tokens451,11431
(defun isar-map-letters 467,11820
(defconst isar-script-letters-tokens473,11968
(defconst isar-roman-letters-tokens478,12106
(defconst isar-fraktur-letters-tokens483,12242
(defcustom isar-token-symbol-map 488,12384
(defcustom isar-user-tokens 504,12853
(defun isar-init-token-symbol-map 511,13090
(defcustom isar-symbol-shortcuts534,13645
(defcustom isar-shortcut-alist 607,15871
(defun isar-init-shortcut-alists 615,16130
(defconst isar-tokens-customizable-variables636,16760

lclam/lclam.el,524
(defcustom lclam-prog-name 15,373
(defcustom lclam-web-page21,521
(defun lclam-config 32,751
(defun lclam-shell-config 54,1542
(define-derived-mode lclam-proofscript-mode 73,2157
(define-derived-mode lclam-shell-mode 78,2280
(define-derived-mode lclam-response-mode 83,2414
(define-derived-mode lclam-goals-mode 87,2537
(defun lclam-mode 95,2765
(define-derived-mode thy-mode 132,3611
(defvar thy-mode-map 135,3709
(defun thy-add-menus 137,3736
(defun process-thy-file 176,5217
(defun update-thy-only 182,5418

lego/lego.el,1683
(defcustom lego-tags 21,534
(defcustom lego-test-all-name 26,670
(defpgdefault help-menu-entries32,828
(defpgdefault menu-entries36,988
(defvar lego-shell-process-output47,1289
(defconst lego-process-config55,1612
(defconst lego-pretty-set-width 66,2043
(defconst lego-interrupt-regexp 70,2185
(defcustom lego-www-home-page 75,2302
(defcustom lego-www-latest-release80,2426
(defcustom lego-www-refcard86,2601
(defcustom lego-library-www-page92,2750
(defvar lego-prog-name 101,2966
(defvar lego-shell-cd 104,3035
(defvar lego-shell-abort-goal-regexp107,3134
(defvar lego-shell-proof-completed-regexp 112,3325
(defvar lego-save-command-regexp115,3465
(defvar lego-goal-command-regexp117,3555
(defvar lego-kill-goal-command 120,3646
(defvar lego-forget-id-command 121,3689
(defvar lego-undoable-commands-regexp123,3735
(defvar lego-goal-regexp 132,4109
(defvar lego-outline-regexp134,4154
(defvar lego-outline-heading-end-regexp 140,4329
(defvar lego-shell-outline-regexp 142,4382
(defvar lego-shell-outline-heading-end-regexp 143,4434
(define-derived-mode lego-shell-mode 149,4713
(define-derived-mode lego-mode 156,4874
(define-derived-mode lego-goals-mode 167,5169
(defun lego-count-undos 178,5595
(defun lego-goal-command-p 198,6413
(defun lego-find-and-forget 203,6584
(defun lego-goal-hyp 245,8400
(defun lego-state-preserving-p 254,8597
(defvar lego-shell-current-line-width 270,9300
(defun lego-shell-adjust-line-width 278,9607
(defun lego-mode-config 297,10344
(defun lego-equal-module-filename 365,12393
(defun lego-shell-compute-new-files-list 371,12668
(defun lego-shell-mode-config 381,13051
(defun lego-goals-mode-config 428,14766

lego/lego-syntax.el,600
(defconst lego-keywords-goal 15,358
(defconst lego-keywords-save 17,401
(defconst lego-commands19,472
(defconst lego-keywords31,1030
(defconst lego-tacticals 36,1207
(defconst lego-error-regexp 39,1315
(defvar lego-id 42,1473
(defvar lego-ids 44,1500
(defconst lego-arg-list-regexp 48,1696
(defun lego-decl-defn-regexp 51,1812
(defconst lego-definiendum-alternative-regexp59,2184
(defvar lego-font-lock-terms63,2368
(defconst lego-goal-with-hole-regexp89,3221
(defconst lego-save-with-hole-regexp94,3443
(defvar lego-font-lock-keywords-199,3660
(defun lego-init-syntax-table 110,4122

phox/phox.el,597
(defcustom phox-prog-name 31,915
(defcustom phox-sym-lock-enabled 36,1017
(defcustom phox-web-page42,1126
(defcustom phox-doc-dir48,1276
(defcustom phox-lib-dir54,1423
(defcustom phox-tags-program60,1566
(defcustom phox-tags-doc66,1745
(defcustom phox-etags72,1882
(defpgdefault menu-entries93,2332
(defun phox-config 107,2525
(defun phox-shell-config 151,4449
(define-derived-mode phox-mode 175,5311
(define-derived-mode phox-shell-mode 191,5774
(define-derived-mode phox-response-mode 196,5902
(define-derived-mode phox-goals-mode 206,6263
(defpgdefault completion-table229,7049

phox/phox-extraction.el,382
(defvar phox-prog-orig 11,480
(defun phox-prog-flags-modify(13,548
(defun phox-prog-flags-extract(42,1349
(defun phox-prog-flags-erase(53,1639
(defun phox-toggle-extraction(61,1835
(defun phox-compile-theorem(73,2237
(defun phox-compile-theorem-on-cursor(79,2462
(defun phox-output 95,2940
(defun phox-output-theorem 105,3152
(defun phox-output-theorem-on-cursor(112,3451

phox/phox-font.el,123
(defconst phox-font-lock-keywords6,282
(defconst phox-sym-lock-keywords-table65,2399
(defun phox-sym-lock-start 88,2973

phox/phox-fun.el,678
(defun phox-init-syntax-table 67,2384
(defvar phox-top-keywords83,2856
(defvar phox-proof-keywords131,3311
(defun phox-find-and-forget 172,3661
(defun phox-assert-next-command-interactive 251,6059
(defun phox-depend-theorem(269,6863
(defun phox-eshow-extlist(278,7152
(defun phox-flag-name(292,7749
(defun phox-path(303,8051
(defun phox-print-expression(314,8287
(defun phox-print-sort-expression(327,8743
(defun phox-priority-symbols-list(338,9055
(defun phox-search-string(350,9427
(defun phox-constraints(365,9952
(defun phox-goals(376,10208
(defvar phox-state-menu388,10417
(defun phox-delete-symbol(413,11407
(defun phox-delete-symbol-on-cursor(419,11615

phox/phox-lang.el,323
(defvar phox-lang9,306
(defun phox-lang-absurd 17,535
(defun phox-lang-suppress 22,629
(defun phox-lang-opendef 27,826
(defun phox-lang-instance 32,944
(defun phox-lang-open-instance 37,1073
(defun phox-lang-lock 42,1222
(defun phox-lang-unlock 47,1352
(defun phox-lang-prove 52,1488
(defun phox-lang-let 57,1622

phox/phox-outline.el,70
(defun phox-outline-level(32,1102
(defun phox-setup-outline 46,1576

phox/phox-pbrpm.el,512
(defun phox-pbrpm-left-paren-p 27,1188
(defun phox-pbrpm-right-paren-p 34,1391
(defun phox-pbrpm-menu-from-string 42,1595
(defun phox-pbrpm-rename-in-cmd 51,1927
(defun phox-pbrpm-get-region-name 84,3175
(defun  phox-pbrpm-escape-string 87,3302
(defun phox-pbrpm-generate-menu 91,3437
(defalias 'proof-pbrpm-generate-menu proof-pbrpm-generate-menu
298,10917
(defalias 'proof-pbrpm-left-paren-p proof-pbrpm-left-paren-p
299,10981
(defalias 'proof-pbrpm-right-paren-p proof-pbrpm-right-paren-p
300,11043

phox/phox-sym-lock.el,1353
(defvar phox-sym-lock-sym-count 34,1596
(defvar phox-sym-lock-ext-start 37,1666
(defvar phox-sym-lock-ext-end 39,1788
(defvar phox-sym-lock-font-size 42,1907
(defvar phox-sym-lock-keywords 47,2097
(defvar phox-sym-lock-enabled 52,2273
(defvar phox-sym-lock-color 57,2435
(defvar phox-sym-lock-mouse-face 62,2653
(defvar phox-sym-lock-mouse-face-enabled 67,2843
(defconst phox-sym-lock-with-mule 72,3033
(defun phox-sym-lock-gen-symbol 75,3117
(defun phox-sym-lock-make-symbols-atomic 83,3419
(defun phox-sym-lock-compute-font-size 110,4360
(defvar phox-sym-lock-font-name148,5779
(defun phox-sym-lock-set-foreground 190,7258
(defun phox-sym-lock-translate-char 204,7867
(defun phox-sym-lock-translate-char-or-string 212,8135
(defun phox-sym-lock-remap-face 219,8362
(defvar phox-sym-lock-clear-face239,9352
(defun phox-sym-lock 251,9773
(defun phox-sym-lock-rec 260,10177
(defun phox-sym-lock-atom-face 266,10322
(defun phox-sym-lock-pre-idle-hook-first 271,10618
(defun phox-sym-lock-pre-idle-hook-last 279,10976
(defun phox-sym-lock-enable 288,11351
(defun phox-sym-lock-disable 301,11764
(defun phox-sym-lock-mouse-face-enable 314,12182
(defun phox-sym-lock-mouse-face-disable 321,12397
(defun phox-sym-lock-font-lock-hook 328,12616
(defun font-lock-set-defaults 343,13307
(defun phox-sym-lock-patch-keywords 354,13671

phox/phox-tags.el,305
(defun phox-tags-add-table(21,766
(defun phox-tags-reset-table(30,1161
(defun phox-tags-add-doc-table(35,1271
(defun phox-tags-add-lib-table(41,1420
(defun phox-tags-add-local-table(47,1555
(defun phox-tags-create-local-table(53,1738
(defun phox-complete-tag(64,1988
(defvar phox-tags-menu71,2097

plastic/plastic.el,2808
(defcustom plastic-tags 22,490
(defcustom plastic-test-all-name 27,622
(defvar plastic-lit-string34,813
(defcustom plastic-help-menu-list38,925
(defvar plastic-shell-process-output52,1418
(defconst plastic-process-config60,1744
(defconst plastic-pretty-set-width 67,1992
(defconst plastic-interrupt-regexp 71,2140
(defcustom plastic-www-home-page 77,2261
(defcustom plastic-www-latest-release82,2398
(defcustom plastic-www-refcard88,2568
(defcustom plastic-library-www-page94,2699
(defcustom plastic-base104,2914
(defvar plastic-prog-name112,3085
(defun plastic-set-default-env-vars 116,3192
(defvar plastic-shell-cd124,3429
(defvar plastic-shell-abort-goal-regexp 128,3569
(defvar plastic-shell-proof-completed-regexp 132,3737
(defvar plastic-save-command-regexp135,3880
(defvar plastic-goal-command-regexp137,3976
(defvar plastic-kill-goal-command140,4073
(defvar plastic-forget-id-command142,4173
(defvar plastic-undoable-commands-regexp145,4253
(defvar plastic-goal-regexp 157,4700
(defvar plastic-outline-regexp159,4748
(defvar plastic-outline-heading-end-regexp 165,4926
(defvar plastic-shell-outline-regexp 167,4982
(defvar plastic-shell-outline-heading-end-regexp 168,5040
(defvar plastic-error-occurred170,5111
(define-derived-mode plastic-shell-mode 179,5428
(define-derived-mode plastic-mode 185,5610
(define-derived-mode plastic-goals-mode 201,6127
(defun plastic-count-undos 210,6472
(defun plastic-goal-command-p 230,7347
(defun plastic-find-and-forget 235,7539
(defun plastic-goal-hyp 270,8814
(defun plastic-state-preserving-p 281,9063
(defvar plastic-shell-current-line-width 304,10038
(defun plastic-shell-adjust-line-width 312,10354
(defun plastic-mode-config 339,11392
(defun plastic-show-shell-buffer 428,14651
(defun plastic-equal-module-filename 434,14754
(defun plastic-shell-compute-new-files-list 440,15032
(defun plastic-shell-mode-config 452,15426
(defun plastic-goals-mode-config 501,17279
(defun plastic-small-bar 513,17566
(defun plastic-large-bar 515,17655
(defun plastic-preprocessing 517,17793
(defun plastic-all-ctxt 568,19574
(defun plastic-send-one-undo 575,19743
(defun plastic-minibuf-cmd 585,20049
(defun plastic-minibuf 597,20521
(defun plastic-synchro 604,20727
(defun plastic-send-minibuf 609,20868
(defun plastic-had-error 617,21176
(defun plastic-reset-error 621,21351
(defun plastic-call-if-no-error 624,21490
(defun plastic-show-shell 629,21694
(define-key plastic-keymap 638,21956
(define-key plastic-keymap 639,22017
(define-key plastic-keymap 640,22078
(define-key plastic-keymap 641,22138
(define-key plastic-keymap 642,22197
(define-key plastic-keymap 643,22256
(defalias 'proof-toolbar-command proof-toolbar-command
653,22505
(defalias 'proof-minibuffer-cmd proof-minibuffer-cmd
654,22556

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

twelf/twelf.el,462
(defcustom twelf-root-dir25,589
(defcustom twelf-info-dir31,747
(defun twelf-add-read-declaration 99,3198
(defun twelf-set-syntax 112,3533
(defun twelf-set-word 114,3630
(defun twelf-set-symbol 115,3692
(defun twelf-map-string 117,3756
(defun twelf-mode-extra-config 164,5816
(defconst twelf-syntax-menu170,6021
(defpacustom chatter 184,6388
(defpacustom double-check 189,6481
(defpacustom print-implicit 193,6618
(defpgdefault menu-entries205,6762

twelf/twelf-font.el,917
(defun twelf-font-create-face 31,836
(defvar twelf-font-dark-background 38,1094
(defvar twelf-font-patterns64,2451
(defun twelf-font-fontify-decl 105,4300
(defun twelf-font-fontify-buffer 115,4597
(defun twelf-font-unfontify 122,4856
(defvar font-lock-message-threshold 127,5030
(defun twelf-font-fontify-region 129,5108
(defun twelf-font-highlight 195,7607
(defun twelf-font-find-delimited-comment 204,8064
(defun twelf-font-find-decl 223,8744
(defun twelf-font-find-binder 239,9234
(defun twelf-font-find-parm 301,11091
(defun twelf-font-find-evar 308,11414
(defun twelf-current-decl 330,12155
(defun twelf-next-decl 357,13283
(defconst *whitespace* 382,14200
(defconst *twelf-comment-start* 385,14298
(defconst *twelf-id-chars* 388,14427
(defun skip-twelf-comments-and-whitespace 391,14545
(defun twelf-end-of-par 403,15005
(defun skip-ahead 426,15737
(defun current-line-absolute 438,16159

twelf/twelf-old.el,6952
(defvar twelf-indent 212,8762
(defvar twelf-infix-regexp 215,8822
(defvar twelf-server-program 219,9017
(defvar twelf-info-file 222,9098
(defvar twelf-server-display-commands 225,9171
(defvar twelf-highlight-range-function 230,9419
(defvar twelf-focus-function 235,9702
(defvar twelf-server-echo-commands 241,9982
(defvar twelf-save-silently 244,10103
(defvar twelf-server-timeout 248,10275
(defvar twelf-sml-program 252,10422
(defvar twelf-sml-args 255,10494
(defvar twelf-sml-display-queries 258,10560
(defvar twelf-mode-hook 261,10668
(defvar twelf-server-mode-hook 264,10762
(defvar twelf-config-mode-hook 267,10870
(defvar twelf-sml-mode-hook 270,10984
(defvar twelf-to-twelf-sml-mode 273,11065
(defvar twelf-config-mode 276,11157
(defvar *twelf-server-buffer-name* 283,11421
(defvar *twelf-server-buffer* 286,11525
(defvar *twelf-server-process-name* 289,11613
(defvar *twelf-config-buffer* 292,11704
(defvar *twelf-config-time* 295,11798
(defvar *twelf-config-list* 298,11911
(defvar *twelf-server-last-process-mark* 301,12023
(defvar *twelf-last-region-sent* 304,12141
(defvar *twelf-last-input-buffer* 311,12465
(defvar *twelf-error-pos* 315,12588
(defconst *twelf-read-functions*318,12664
(defconst *twelf-parm-table*325,12902
(defvar twelf-chatter 338,13278
(defvar twelf-double-check 346,13495
(defvar twelf-print-implicit 349,13582
(defconst *twelf-track-parms*352,13674
(defun install-basic-twelf-keybindings 363,14098
(defun install-twelf-keybindings 388,15067
(defvar twelf-mode-map 404,15832
(defvar twelf-mode-syntax-table 416,16268
(defun set-twelf-syntax 419,16347
(defun set-word 421,16444
(defun set-symbol 422,16499
(defun map-string 424,16557
(defconst *whitespace* 456,18034
(defconst *twelf-comment-start* 459,18132
(defconst *twelf-id-chars* 462,18261
(defun skip-twelf-comments-and-whitespace 465,18379
(defun twelf-end-of-par 477,18839
(defun twelf-current-decl 500,19571
(defun twelf-mark-decl 527,20699
(defun twelf-indent-decl 536,20951
(defun twelf-indent-region 545,21223
(defun twelf-indent-lines 556,21505
(defun twelf-comment-indent 564,21678
(defun looked-at 575,21992
(defun twelf-indent-line 580,22164
(defun twelf-indent-line-to 613,23746
(defun twelf-calculate-indent 626,24180
(defun twelf-dsb 641,24734
(defun twelf-mode-variables 667,25985
(defun twelf-mode 689,26798
(defun twelf-info 904,35180
(defconst twelf-error-regexp918,35720
(defconst twelf-error-fields-regexp922,35831
(defconst twelf-error-decl-regexp928,36044
(defun looked-at-nth 932,36191
(defun looked-at-nth-int 938,36366
(defun twelf-error-parser 943,36484
(defun twelf-error-decl 957,37052
(defun twelf-mark-relative 963,37231
(defun twelf-mark-absolute 979,37845
(defun twelf-find-decl 1004,38731
(defun twelf-next-error 1019,39287
(defun twelf-goto-error 1087,42062
(defun twelf-convert-standard-filename 1101,42586
(defun string-member 1113,43081
(defun twelf-config-proceed-p 1125,43573
(defun twelf-save-if-config 1132,43835
(defun twelf-config-save-some-buffers 1145,44307
(defun twelf-save-check-config 1149,44472
(defun twelf-check-config 1164,45028
(defun twelf-save-check-file 1176,45468
(defun twelf-buffer-substring 1192,46191
(defun twelf-buffer-substring-dot 1198,46453
(defun twelf-check-declaration 1204,46719
(defun twelf-highlight-range-zmacs 1227,47758
(defun twelf-focus 1233,48008
(defun twelf-focus-noop 1239,48274
(defun twelf-type-const 1322,51896
(defvar twelf-server-mode-map 1439,56960
(defconst twelf-server-cd-regexp 1451,57512
(defun looked-at-string 1454,57652
(defun twelf-server-directory-tracker 1458,57793
(defun twelf-input-filter 1480,58952
(defun twelf-server-mode 1486,59207
(defun twelf-parse-config 1519,60424
(defun twelf-server-read-config 1537,61190
(defun twelf-server-sync-config 1546,61520
(defun twelf-get-server-buffer 1576,62892
(defun twelf-init-variables 1593,63510
(defun twelf-server 1600,63723
(defun twelf-server-process 1642,65357
(defun twelf-server-display 1651,65721
(defun display-server-buffer 1658,65995
(defun twelf-server-send-command 1673,66650
(defun twelf-accept-process-output 1694,67526
(defun twelf-server-wait 1703,67965
(defun twelf-server-quit 1745,69718
(defun twelf-server-interrupt 1750,69839
(defun twelf-reset 1755,69975
(defun twelf-config-directory 1760,70119
(defun twelf-server-configure 1771,70533
(defun natp 1844,73650
(defun twelf-read-nat 1848,73751
(defun twelf-read-bool 1857,74018
(defun twelf-read-limit 1863,74166
(defun twelf-read-strategy 1873,74469
(defun twelf-read-value 1879,74621
(defun twelf-set 1883,74784
(defun twelf-set-parm 1896,75260
(defun track-parm 1905,75557
(defun twelf-toggle-double-check 1910,75731
(defun twelf-toggle-print-implicit 1916,75934
(defun twelf-get 1922,76147
(defun twelf-timers-reset 1936,76773
(defun twelf-timers-show 1941,76893
(defun twelf-timers-check 1947,77044
(defun twelf-server-restart 1953,77209
(defun twelf-config-mode 1969,77823
(defun twelf-config-mode-check 1985,78422
(defun twelf-tag 1994,78872
(defun twelf-tag-files 2022,80059
(default: *tags-errors*)2026,80362
(defun twelf-tag-file 2047,81057
(defun twelf-next-decl 2082,82265
(defun skip-ahead 2107,83182
(defun current-line-absolute 2119,83604
(defun new-temp-buffer 2124,83814
(defun rev-relativize 2135,84177
(defvar twelf-sml-mode-map 2149,84630
(defconst twelf-sml-prompt-regexp 2159,85008
(defun expand-dir 2161,85063
(defun twelf-sml-cd 2168,85317
(defconst twelf-sml-cd-regexp 2180,85806
(defun twelf-sml-directory-tracker 2183,85940
(defun twelf-sml-mode 2199,86680
(defun twelf-sml 2250,88605
(defun switch-to-twelf-sml 2270,89565
(defun display-twelf-sml-buffer 2281,89900
(defun twelf-sml-send-string 2297,90546
(defun twelf-sml-send-region 2302,90750
(defun twelf-sml-send-query 2326,91942
(defun twelf-sml-send-newline 2336,92325
(defun twelf-sml-send-semicolon 2344,92653
(defun twelf-sml-status 2352,92987
(defvar twelf-sml-init 2374,93822
(defun twelf-sml-set-mode 2377,93999
(defun twelf-sml-quit 2403,95092
(defun twelf-sml-process-buffer 2408,95204
(defun twelf-sml-process 2412,95320
(defvar twelf-to-twelf-sml-mode 2424,95829
(defun install-twelf-to-twelf-sml-keybindings 2427,95914
(defvar twelf-to-twelf-sml-mode-map 2437,96299
(defun twelf-to-twelf-sml-mode 2448,96812
(defconst twelf-at-point-menu2498,98609
(defconst twelf-server-state-menu2508,98981
(defconst twelf-error-menu2518,99298
(defconst twelf-tags-menu2524,99442
(defun twelf-toggle-server-display-commands 2534,99727
(defconst twelf-options-menu2537,99851
(defconst twelf-timers-menu2572,101589
(defconst twelf-syntax-menu2585,102083
(defun twelf-add-menu 2612,102949
(defun twelf-remove-menu 2616,103051
(defun twelf-reset-menu 2620,103149
(defun twelf-server-add-menu 2647,104048
(defun twelf-server-remove-menu 2651,104171
(defun twelf-server-reset-menu 2655,104283

generic/pg-assoc.el,82
(defun proof-associated-buffers 36,1063
(defun proof-associated-windows 46,1273

generic/pg-autotest.el,442
(defvar pg-autotest-success 24,542
(defun pg-autotest-find-file 28,626
(defun pg-autotest-find-file-restart 35,906
(defmacro pg-autotest 48,1354
(defun pg-autotest-script-wholefile 62,1701
(defun pg-autotest-retract-file 79,2314
(defun pg-autotest-assert-processed 85,2450
(defun pg-autotest-assert-unprocessed 92,2704
(defun pg-autotest-message 99,2964
(defun pg-autotest-quit-prover 106,3157
(defun pg-autotest-finished 112,3338

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 30,654
(define-key proof-goals-mode-map 58,1529
(define-key proof-goals-mode-map 60,1645
(define-key proof-goals-mode-map 61,1713
(defun proof-goals-config-done 70,1858
(defun pg-goals-display 78,2124
(defun pg-goals-button-action 119,3428

generic/pg-pbrpm.el,1804
(defvar pg-pbrpm-use-buffer-menu 29,720
(defvar pg-pbrpm-start-goal-regexp 32,842
(defvar pg-pbrpm-start-goal-regexp-par-num 36,999
(defvar pg-pbrpm-end-goal-regexp 39,1122
(defvar pg-pbrpm-start-hyp-regexp 43,1274
(defvar pg-pbrpm-start-hyp-regexp-par-num 47,1435
(defvar pg-pbrpm-start-concl-regexp 51,1642
(defvar pg-pbrpm-auto-select-regexp 55,1806
(defvar pg-pbrpm-buffer-menu 62,1967
(defvar pg-pbrpm-spans 63,2001
(defvar pg-pbrpm-goal-description 64,2029
(defvar pg-pbrpm-windows-dialog-bug 65,2068
(defvar pbrpm-menu-desc 66,2109
(defun pg-pbrpm-erase-buffer-menu 68,2139
(defun pg-pbrpm-menu-change-hook 75,2323
(defun pg-pbrpm-create-reset-buffer-menu 93,2898
(defun pg-pbrpm-analyse-goal-buffer 110,3643
(defun pg-pbrpm-button-action 170,6041
(defun pg-pbrpm-exists 177,6267
(defun pg-pbrpm-eliminate-id 181,6379
(defun pg-pbrpm-build-menu 189,6625
(defun pg-pbrpm-setup-span 252,8945
(defun pg-pbrpm-run-command 312,11260
(defun pg-pbrpm-get-pos-info 341,12570
(defun pg-pbrpm-get-region-info 383,13869
(defun pg-pbrpm-auto-select-around-point 394,14281
(defun pg-pbrpm-translate-position 409,14805
(defun pg-pbrpm-process-click 417,15062
(defvar pg-pbrpm-remember-region-selected-region 437,16087
(defvar pg-pbrpm-regions-list 438,16141
(defun pg-pbrpm-erase-regions-list 440,16177
(defun pg-pbrpm-filter-regions-list 449,16485
(defface pg-pbrpm-multiple-selection-face456,16748
(defface pg-pbrpm-menu-input-face464,16950
(defun pg-pbrpm-do-remember-region 472,17140
(defun pg-pbrpm-remember-region-drag-up-hook 493,17988
(defun pg-pbrpm-remember-region-click-hook 497,18159
(defun pg-pbrpm-remember-region 502,18344
(defun pg-pbrpm-process-region 516,19058
(defun pg-pbrpm-process-regions-list 534,19787
(defun pg-pbrpm-region-expression 538,19970

generic/pg-pgip.el,2927
(defalias 'pg-pgip-debug pg-pgip-debug
35,913
(defalias 'pg-pgip-error pg-pgip-error
36,954
(defalias 'pg-pgip-warning pg-pgip-warning
37,989
(defconst pg-pgip-version-supported 39,1039
(defun pg-pgip-process-packet 43,1145
(defvar pg-pgip-last-seen-id 53,1713
(defvar pg-pgip-last-seen-seq 54,1747
(defun pg-pgip-process-pgip 56,1783
(defun pg-pgip-process-msg 75,2714
(defvar pg-pgip-post-process-functions89,3284
(defun pg-pgip-post-process 99,3772
(defun pg-pgip-process-askpgip 115,4382
(defun pg-pgip-process-usespgip 121,4586
(defun pg-pgip-process-usespgml 125,4750
(defun pg-pgip-process-pgmlconfig 129,4914
(defun pg-pgip-process-proverinfo 145,5531
(defun pg-pgip-process-hasprefs 162,6196
(defun pg-pgip-haspref 176,6828
(defun pg-pgip-process-prefval 193,7530
(defun pg-pgip-process-guiconfig 220,8238
(defvar proof-assistant-idtables 227,8355
(defun pg-pgip-process-ids 230,8472
(defun pg-complete-idtable-symbol 256,9544
(defalias 'pg-pgip-process-setids pg-pgip-process-setids
261,9636
(defalias 'pg-pgip-process-addids pg-pgip-process-addids
262,9692
(defalias 'pg-pgip-process-delids pg-pgip-process-delids
263,9748
(defun pg-pgip-process-idvalue 266,9806
(defun pg-pgip-process-menuadd 278,10142
(defun pg-pgip-process-menudel 281,10185
(defun pg-pgip-process-ready 290,10417
(defun pg-pgip-process-cleardisplay 293,10458
(defun pg-pgip-process-proofstate 307,10915
(defun pg-pgip-process-normalresponse 311,10992
(defun pg-pgip-process-errorresponse 315,11116
(defun pg-pgip-process-scriptinsert 319,11239
(defun pg-pgip-process-metainforesponse 324,11373
(defun pg-pgip-file-of-url 333,11613
(defun pg-pgip-process-informfileloaded 338,11748
(defun pg-pgip-process-informfileretracted 344,11980
(defun pg-pgip-process-brokerstatus 357,12431
(defun pg-pgip-process-proveravailmsg 360,12479
(defun pg-pgip-process-newprovermsg 363,12529
(defun pg-pgip-process-proverstatusmsg 366,12577
(defvar pg-pgip-srcids 375,12823
(defun pg-pgip-process-newfile 379,12930
(defun pg-pgip-process-filestatus 395,13512
(defun pg-pgip-process-newobj 415,14166
(defun pg-pgip-process-delobj 418,14208
(defun pg-pgip-process-objectstatus 421,14250
(defun pg-pgip-process-parsescript 435,14602
(defun pg-pgip-get-pgiptype 458,15476
(defun pg-pgip-default-for 478,16268
(defun pg-pgip-subst-for 491,16663
(defun pg-pgip-interpret-value 503,17006
(defun pg-pgip-interpret-choice 521,17687
(defun pg-pgip-string-of-command 552,18704
(defconst pg-pgip-id569,19465
(defvar pg-pgip-refseq 575,19745
(defvar pg-pgip-refid 577,19842
(defvar pg-pgip-seq 580,19934
(defun pg-pgip-assemble-packet 582,19998
(defun pg-pgip-issue 600,20809
(defun pg-pgip-maybe-askpgip 617,21421
(defun pg-pgip-askprefs 623,21612
(defun pg-pgip-askids 627,21726
(defun pg-pgip-reset 640,22014
(defconst pg-pgip-start-element-regexp 671,22712
(defconst pg-pgip-end-element-regexp 672,22764

generic/pg-response.el,1214
(deflocal pg-response-eagerly-raise 31,729
(define-derived-mode proof-response-mode 41,954
(define-key proof-response-mode-map 68,1880
(define-key proof-response-mode-map 69,1951
(define-key proof-response-mode-map 70,2005
(defun proof-response-config-done 74,2091
(defvar pg-response-special-display-regexp 85,2437
(defconst proof-multiframe-parameters89,2604
(defun proof-multiple-frames-enable 98,2903
(defun proof-three-window-enable 108,3231
(defun proof-select-three-b 111,3294
(defun proof-display-three-b 126,3763
(defvar pg-frame-configuration 138,4169
(defun pg-cache-frame-configuration 142,4316
(defun proof-layout-windows 146,4487
(defun proof-delete-other-frames 186,6274
(defvar pg-response-erase-flag 217,7362
(defun pg-response-maybe-erase221,7491
(defun pg-response-display 251,8587
(defun pg-response-display-with-face 276,9370
(defun pg-response-clear-displays 306,10292
(defun proof-next-error 325,10879
(defun pg-response-has-error-location 406,13795
(defvar proof-trace-last-fontify-pos 429,14627
(defun proof-trace-fontify-pos 431,14670
(defun proof-trace-buffer-display 439,14983
(defun proof-trace-buffer-finish 464,15923
(defun pg-thms-buffer-clear 486,16490

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,3486
(defun proof-script-next-command-advance 31,762
(defun proof-script-new-command-advance 43,1226
(defun proof-maybe-follow-locked-end 86,2968
(defun proof-goto-point 110,3737
(defun proof-assert-next-command-interactive 124,4171
(defun proof-assert-until-point-interactive 137,4696
(defun proof-process-buffer 143,4926
(defun proof-undo-last-successful-command 158,5303
(defun proof-undo-and-delete-last-successful-command 163,5465
(defun proof-undo-last-successful-command-1 176,6019
(defun proof-retract-buffer 193,6631
(defun proof-retract-current-goal 202,6915
(defun proof-goto-command-start 221,7476
(defun proof-goto-command-end 244,8416
(defun proof-mouse-goto-point 264,8865
(defvar proof-minibuffer-history 279,9141
(defun proof-minibuffer-cmd 282,9236
(defun proof-frob-locked-end 326,10858
(defmacro proof-if-setting-configured 387,12782
(defmacro proof-define-assistant-command 395,13051
(defmacro proof-define-assistant-command-witharg 408,13506
(defun proof-issue-new-command 428,14328
(defun proof-cd-sync 474,15825
(defun proof-electric-terminator-enable 528,17545
(defun proof-process-electric-terminator 536,17835
(defun proof-electric-terminator 571,19174
(defun proof-add-completions 593,19820
(defun proof-script-complete 617,20680
(defun pg-insert-last-output-as-comment 631,21066
(defun pg-copy-span-contents 645,21464
(defun pg-numth-span-higher-or-lower 662,22022
(defun pg-control-span-of 688,22768
(defun pg-move-span-contents 694,22972
(defun pg-fixup-children-spans 746,25148
(defun pg-move-region-down 756,25405
(defun pg-move-region-up 765,25698
(defun proof-forward-command 795,26526
(defun proof-backward-command 816,27247
(defun pg-pos-for-event 838,27591
(defun pg-span-for-event 844,27812
(defun pg-span-context-menu 848,27956
(defun pg-toggle-visibility 863,28411
(defun pg-create-in-span-context-menu 873,28733
(defun pg-span-undo 903,29942
(defun pg-goals-buffers-hint 949,31344
(defun pg-slow-fontify-tracing-hint 953,31526
(defun pg-response-buffers-hint 957,31697
(defun pg-jump-to-end-hint 967,32059
(defun pg-processing-complete-hint 971,32188
(defun pg-next-error-hint 988,32887
(defun pg-hint 993,33039
(defun pg-identifier-under-mouse-query 1009,33629
(defun pg-identifier-near-point-query 1018,33872
(defvar proof-query-identifier-collection 1043,34588
(defvar proof-query-identifier-history 1044,34635
(defun proof-query-identifier 1046,34680
(defun pg-identifier-query 1056,34949
(defun proof-imenu-enable 1087,36027
(defvar pg-input-ring 1118,37088
(defvar pg-input-ring-index 1121,37145
(defvar pg-stored-incomplete-input 1124,37217
(defun pg-previous-input 1127,37320
(defun pg-next-input 1141,37777
(defun pg-delete-input 1146,37899
(defun pg-get-old-input 1159,38237
(defun pg-restore-input 1173,38628
(defun pg-search-start 1184,38918
(defun pg-regexp-arg 1196,39410
(defun pg-search-arg 1208,39858
(defun pg-previous-matching-input-string-position 1222,40275
(defun pg-previous-matching-input 1249,41440
(defun pg-next-matching-input 1268,42290
(defvar pg-matching-input-from-input-string 1276,42673
(defun pg-previous-matching-input-from-input 1280,42787
(defun pg-next-matching-input-from-input 1298,43552
(defun pg-add-to-input-history 1309,43931
(defun pg-remove-from-input-history 1321,44384
(defun  pg-clear-input-ring 1332,44764
(define-key proof-mode-map 1346,45114
(define-key proof-mode-map 1347,45174
(defun pg-protected-undo 1349,45246

generic/pg-vars.el,1326
(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-last-output 169,5920
(defvar proof-assistant-settings 173,6060
(defvar pg-tracing-slow-mode 181,6508
(defvar proof-nesting-depth 184,6597
(defvar proof-last-theorem-dependencies 191,6832
(defcustom proof-general-name 200,7068
(defcustom proof-general-home-page205,7225
(defcustom proof-unnamed-theorem-name211,7385
(defcustom proof-universal-keys217,7569

generic/pg-xml.el,1177
(defalias 'pg-xml-error pg-xml-error
16,366
(defun pg-xml-parse-string 39,1008
(defun pg-xml-parse-buffer 50,1334
(defun pg-xml-get-attr 69,1949
(defun pg-xml-child-elts 77,2251
(defun pg-xml-child-elt 82,2456
(defun pg-xml-get-child 90,2738
(defun pg-xml-get-text-content 100,3105
(defmacro pg-xml-attr 111,3455
(defmacro pg-xml-node 113,3517
(defconst pg-xml-header116,3609
(defun pg-xml-string-of 120,3685
(defun pg-xml-output-internal 131,4052
(defun pg-xml-cdata 165,5191
(defsubst pg-pgip-get-area 173,5384
(defun pg-pgip-get-icon 176,5501
(defsubst pg-pgip-get-name 180,5649
(defsubst pg-pgip-get-version 183,5766
(defsubst pg-pgip-get-descr 186,5889
(defsubst pg-pgip-get-thmname 189,6008
(defsubst pg-pgip-get-thyname 192,6131
(defsubst pg-pgip-get-url 195,6254
(defsubst pg-pgip-get-srcid 198,6369
(defsubst pg-pgip-get-proverid 201,6488
(defsubst pg-pgip-get-symname 204,6613
(defsubst pg-pgip-get-prefcat 207,6733
(defsubst pg-pgip-get-default 210,6861
(defsubst pg-pgip-get-objtype 213,6984
(defsubst pg-pgip-get-value 216,7107
(defalias 'pg-pgip-get-displaytext pg-pgip-get-displaytext
219,7177
(defun pg-pgip-get-pgmltext 221,7236

generic/proof-autoloads.el,45
(defsubst proof-shell-live-buffer 618,20501

generic/proof-auxmodes.el,149
(defun proof-mmm-support-available 21,549
(defun proof-maths-menu-support-available 45,1160
(defun proof-unicode-tokens-support-available 59,1577

generic/proof-config.el,7853
(defgroup prover-config 79,2594
(defcustom proof-guess-command-line 97,3444
(defcustom proof-assistant-home-page 112,3939
(defcustom proof-context-command 118,4109
(defcustom proof-info-command 123,4243
(defcustom proof-showproof-command 130,4514
(defcustom proof-goal-command 135,4650
(defcustom proof-save-command 143,4947
(defcustom proof-find-theorems-command 151,5256
(defcustom proof-query-identifier-command 158,5564
(defcustom proof-assistant-true-value 172,6253
(defcustom proof-assistant-false-value 178,6443
(defcustom proof-assistant-format-int-fn 184,6637
(defcustom proof-assistant-format-string-fn 191,6886
(defcustom proof-assistant-setting-format 198,7153
(defgroup proof-script 220,7848
(defcustom proof-terminal-char 225,7978
(defcustom proof-electric-terminator-noterminator 235,8365
(defcustom proof-script-sexp-commands 240,8537
(defcustom proof-script-command-end-regexp 251,8994
(defcustom proof-script-command-start-regexp 269,9813
(defcustom proof-script-use-old-parser 280,10274
(defcustom proof-script-integral-proofs 292,10760
(defcustom proof-script-fly-past-comments 307,11416
(defcustom proof-script-parse-function 312,11587
(defcustom proof-script-comment-start 330,12230
(defcustom proof-script-comment-start-regexp 341,12667
(defcustom proof-script-comment-end 349,12986
(defcustom proof-script-comment-end-regexp 361,13408
(defcustom proof-string-start-regexp 369,13719
(defcustom proof-string-end-regexp 374,13884
(defcustom proof-case-fold-search 379,14045
(defcustom proof-save-command-regexp 388,14457
(defcustom proof-save-with-hole-regexp 393,14567
(defcustom proof-save-with-hole-result 405,15022
(defcustom proof-goal-command-regexp 415,15470
(defcustom proof-goal-with-hole-regexp 424,15858
(defcustom proof-goal-with-hole-result 436,16301
(defcustom proof-non-undoables-regexp 445,16685
(defcustom proof-nested-undo-regexp 456,17140
(defcustom proof-ignore-for-undo-count 472,17852
(defcustom proof-script-next-entity-regexps 480,18155
(defcustom proof-script-find-next-entity-fn524,19896
(defcustom proof-script-imenu-generic-expression 544,20736
(defcustom proof-goal-command-p 552,21075
(defcustom proof-really-save-command-p 563,21566
(defcustom proof-completed-proof-behaviour 572,21873
(defcustom proof-count-undos-fn 600,23222
(defcustom proof-find-and-forget-fn 612,23771
(defcustom proof-forget-id-command 629,24474
(defcustom pg-topterm-goalhyplit-fn 639,24832
(defcustom proof-kill-goal-command 651,25367
(defcustom proof-undo-n-times-cmd 665,25870
(defcustom proof-nested-goals-history-p 679,26418
(defcustom proof-state-preserving-p 688,26755
(defcustom proof-activate-scripting-hook 698,27227
(defcustom proof-deactivate-scripting-hook 717,28008
(defcustom proof-script-evaluate-elisp-comment-regexp 726,28338
(defcustom proof-indent 744,28924
(defcustom proof-indent-hang 749,29031
(defcustom proof-indent-enclose-offset 754,29157
(defcustom proof-indent-open-offset 759,29299
(defcustom proof-indent-close-offset 764,29436
(defcustom proof-indent-any-regexp 769,29574
(defcustom proof-indent-inner-regexp 774,29734
(defcustom proof-indent-enclose-regexp 779,29888
(defcustom proof-indent-open-regexp 784,30042
(defcustom proof-indent-close-regexp 789,30194
(defcustom proof-script-font-lock-keywords 795,30348
(defcustom proof-script-syntax-table-entries 803,30700
(defcustom proof-script-span-context-menu-extensions 821,31096
(defgroup proof-shell 847,31854
(defcustom proof-prog-name 857,32024
(defcustom proof-shell-auto-terminate-commands 868,32444
(defcustom proof-shell-pre-sync-init-cmd 877,32845
(defcustom proof-shell-init-cmd 891,33403
(defcustom proof-shell-init-hook 903,33932
(defcustom proof-shell-restart-cmd 908,34071
(defcustom proof-shell-quit-cmd 913,34226
(defcustom proof-shell-quit-timeout 918,34393
(defcustom proof-shell-cd-cmd 928,34843
(defcustom proof-shell-start-silent-cmd 945,35514
(defcustom proof-shell-stop-silent-cmd 954,35890
(defcustom proof-shell-silent-threshold 963,36225
(defcustom  proof-shell-inform-file-processed-cmd 971,36559
(defcustom  proof-shell-inform-file-retracted-cmd 992,37487
(defcustom proof-auto-multiple-files 1020,38759
(defcustom proof-cannot-reopen-processed-files 1035,39480
(defcustom proof-shell-require-command-regexp 1049,40146
(defcustom proof-done-advancing-require-function 1060,40608
(defcustom proof-shell-quiet-errors 1066,40843
(defcustom proof-shell-annotated-prompt-regexp 1079,41177
(defcustom proof-shell-abort-goal-regexp 1094,41742
(defcustom proof-shell-error-regexp 1099,41877
(defcustom proof-shell-truncate-before-error 1119,42679
(defcustom pg-next-error-regexp 1133,43218
(defcustom pg-next-error-filename-regexp 1148,43827
(defcustom pg-next-error-extract-filename 1172,44860
(defcustom proof-shell-interrupt-regexp 1179,45103
(defcustom proof-shell-proof-completed-regexp 1193,45698
(defcustom proof-shell-clear-response-regexp 1206,46206
(defcustom proof-shell-clear-goals-regexp 1218,46658
(defcustom proof-shell-start-goals-regexp 1230,47104
(defcustom proof-shell-end-goals-regexp 1238,47471
(defcustom proof-shell-eager-annotation-start 1252,48046
(defcustom proof-shell-eager-annotation-start-length 1275,49065
(defcustom proof-shell-eager-annotation-end 1286,49491
(defcustom proof-shell-strip-output-markup 1302,50166
(defcustom proof-shell-assumption-regexp 1311,50551
(defcustom proof-shell-process-file 1321,50955
(defcustom proof-shell-retract-files-regexp 1347,52033
(defcustom proof-shell-compute-new-files-list 1360,52521
(defcustom pg-special-char-regexp 1375,53090
(defcustom proof-shell-set-elisp-variable-regexp 1380,53234
(defcustom proof-shell-match-pgip-cmd 1418,54900
(defcustom proof-shell-issue-pgip-cmd 1432,55382
(defcustom proof-use-pgip-askprefs 1437,55547
(defcustom proof-shell-query-dependencies-cmd 1445,55894
(defcustom proof-shell-theorem-dependency-list-regexp 1452,56154
(defcustom proof-shell-theorem-dependency-list-split 1468,56814
(defcustom proof-shell-show-dependency-cmd 1477,57237
(defcustom proof-shell-trace-output-regexp 1499,58143
(defcustom proof-shell-thms-output-regexp 1517,58738
(defcustom proof-tokens-activate-command 1530,59121
(defcustom proof-tokens-deactivate-command 1537,59361
(defcustom proof-tokens-extra-modes 1544,59606
(defcustom proof-shell-unicode 1559,60111
(defcustom proof-shell-filename-escapes 1568,60501
(defcustom proof-shell-process-connection-type1585,61181
(defcustom proof-shell-strip-crs-from-input 1608,62185
(defcustom proof-shell-strip-crs-from-output 1620,62668
(defcustom proof-shell-insert-hook 1628,63036
(defcustom proof-shell-handle-delayed-output-hook1666,64896
(defcustom proof-shell-handle-error-or-interrupt-hook1672,65111
(defcustom proof-shell-pre-interrupt-hook1690,65864
(defcustom proof-shell-classify-output-system-specific 1698,66135
(defcustom proof-state-change-hook 1717,67003
(defcustom proof-shell-syntax-table-entries 1727,67396
(defgroup proof-goals 1745,67767
(defcustom pg-subterm-first-special-char 1750,67888
(defcustom pg-subterm-anns-use-stack 1758,68200
(defcustom pg-goals-change-goal 1767,68499
(defcustom pbp-goal-command 1772,68615
(defcustom pbp-hyp-command 1777,68771
(defcustom pg-subterm-help-cmd 1782,68933
(defcustom pg-goals-error-regexp 1789,69169
(defcustom proof-shell-result-start 1794,69329
(defcustom proof-shell-result-end 1800,69563
(defcustom pg-subterm-start-char 1806,69776
(defcustom pg-subterm-sep-char 1820,70361
(defcustom pg-subterm-end-char 1826,70540
(defcustom pg-topterm-regexp 1832,70697
(defcustom proof-goals-font-lock-keywords 1847,71297
(defcustom proof-response-font-lock-keywords 1855,71656
(defcustom pg-before-fontify-output-hook 1863,72018
(defcustom pg-after-fontify-output-hook 1871,72379

generic/proof-depends.el,824
(defvar proof-thm-names-of-files 23,622
(defvar proof-def-names-of-files 29,906
(defun proof-depends-module-name-for-buffer 38,1210
(defun proof-depends-module-of 48,1651
(defun proof-depends-names-in-same-file 56,1944
(defun proof-depends-process-dependencies 75,2552
(defun proof-dependency-in-span-context-menu 128,4287
(defun proof-dep-alldeps-menu 151,5189
(defun proof-dep-make-alldeps-menu 157,5415
(defun proof-dep-split-deps 175,5910
(defun proof-dep-make-submenu 196,6606
(defun proof-make-highlight-depts-menu 206,6956
(defun proof-goto-dependency 216,7259
(defun proof-show-dependency 222,7482
(defconst pg-dep-span-priority 229,7771
(defconst pg-ordinary-span-priority 230,7807
(defun proof-highlight-depcs 232,7849
(defun proof-highlight-depts 242,8279
(defun proof-dep-unhighlight 253,8753

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,2131
(defmacro proof-easy-config 84,3461

generic/proof-faces.el,1344
(defgroup proof-faces 28,747
(defconst pg-defface-window-systems35,927
(defmacro proof-face-specs 48,1489
(defface proof-queue-face63,1941
(defface proof-locked-face71,2219
(defface proof-declaration-name-face81,2540
(defface proof-tacticals-name-face90,2826
(defface proof-tactics-name-face99,3088
(defface proof-error-face108,3353
(defface proof-warning-face116,3543
(defface proof-eager-annotation-face125,3800
(defface proof-debug-message-face133,4018
(defface proof-boring-face141,4217
(defface proof-mouse-highlight-face149,4409
(defface proof-highlight-dependent-face157,4605
(defface proof-highlight-dependency-face165,4812
(defface proof-active-area-face173,5009
(defconst proof-face-compat-doc 184,5401
(defconst proof-queue-face 185,5481
(defconst proof-locked-face 186,5549
(defconst proof-declaration-name-face 187,5619
(defconst proof-tacticals-name-face 188,5709
(defconst proof-tactics-name-face 189,5795
(defconst proof-error-face 190,5877
(defconst proof-warning-face 191,5945
(defconst proof-eager-annotation-face 192,6017
(defconst proof-debug-message-face 193,6107
(defconst proof-boring-face 194,6191
(defconst proof-mouse-highlight-face 195,6261
(defconst proof-highlight-dependent-face 196,6349
(defconst proof-highlight-dependency-face 197,6445
(defconst proof-active-area-face 198,6543

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,959
(defun proof-maths-menu-enable 44,1410

generic/proof-menu.el,2146
(defvar proof-display-some-buffers-count 19,452
(defun proof-display-some-buffers 21,497
(defun proof-menu-define-keys 80,2693
(defun proof-menu-define-main 137,5498
(defvar proof-menu-favourites 146,5683
(defun proof-menu-define-specific 150,5805
(defun proof-assistant-menu-update 193,7073
(defvar proof-help-menu207,7506
(defvar proof-show-hide-menu215,7776
(defvar proof-buffer-menu224,8089
(defun proof-retract-on-edit-toggle 285,10312
(defun proof-keep-response-history 292,10488
(defconst proof-quick-opts-menu300,10798
(defun proof-quick-opts-vars 467,17723
(defun proof-quick-opts-changed-from-defaults-p 494,18524
(defun proof-quick-opts-changed-from-saved-p 498,18629
(defun proof-quick-opts-save 509,18980
(defun proof-quick-opts-reset 514,19148
(defconst proof-config-menu526,19416
(defconst proof-advanced-menu533,19595
(defvar proof-menu546,20030
(defun proof-main-menu 555,20312
(defun proof-aux-menu 566,20578
(defun proof-menu-define-favourites-menu 582,20924
(defun proof-def-favourite 602,21573
(defvar proof-make-favourite-cmd-history 625,22547
(defvar proof-make-favourite-menu-history 628,22632
(defun proof-save-favourites 631,22718
(defun proof-del-favourite 636,22866
(defun proof-read-favourite 653,23422
(defun proof-add-favourite 677,24198
(defvar proof-menu-settings 704,25243
(defun proof-menu-define-settings-menu 707,25317
(defun proof-menu-entry-name 740,26438
(defun proof-menu-entry-for-setting 750,26788
(defun proof-settings-vars 769,27320
(defun proof-settings-changed-from-defaults-p 774,27497
(defun proof-settings-changed-from-saved-p 778,27603
(defun proof-settings-save 782,27706
(defun proof-settings-reset 787,27873
(defun proof-defpacustom-fn 794,28118
(defmacro defpacustom 860,30399
(defun proof-assistant-invisible-command-ifposs 875,31226
(defun proof-maybe-askprefs 897,32196
(defun proof-assistant-settings-cmd 903,32388
(defvar proof-assistant-format-table920,33043
(defun proof-assistant-format-bool 928,33411
(defun proof-assistant-format-int 931,33524
(defun proof-assistant-format-string 934,33616
(defun proof-assistant-format 937,33714

generic/proof-mmm.el,70
(defun proof-mmm-set-global 41,1517
(defun proof-mmm-enable 56,2056

generic/proof-script.el,5377
(deflocal proof-active-buffer-fake-minor-mode 32,852
(deflocal proof-script-buffer-file-name 35,978
(deflocal pg-script-portions 42,1388
(defun proof-next-element-count 52,1608
(defun proof-element-id 58,1850
(defun proof-next-element-id 62,2019
(deflocal proof-locked-span 97,3273
(deflocal proof-queue-span 104,3539
(deflocal proof-overlay-arrow 113,4025
(defun proof-span-give-warning 119,4152
(defun proof-span-read-only 124,4301
(defun proof-strict-read-only 133,4674
(defsubst proof-set-queue-endpoints 143,5052
(defun proof-set-overlay-arrow 147,5193
(defsubst proof-set-locked-endpoints 158,5531
(defsubst proof-detach-queue 163,5707
(defsubst proof-detach-locked 168,5846
(defsubst proof-set-queue-start 175,6071
(defsubst proof-set-locked-end 179,6197
(defsubst proof-set-queue-end 191,6667
(defun proof-init-segmentation 202,6964
(defun proof-colour-locked 236,8462
(defun proof-restart-buffers 247,8894
(defun proof-script-buffers-with-spans 268,9645
(defun proof-script-remove-all-spans-and-deactivate 278,10001
(defun proof-script-clear-queue-spans 282,10191
(defun proof-script-delete-spans 292,10633
(defun proof-unprocessed-begin 307,10948
(defun proof-script-end 315,11202
(defun proof-queue-or-locked-end 324,11505
(defun proof-locked-end 339,12183
(defun proof-locked-region-full-p 353,12464
(defun proof-locked-region-empty-p 362,12736
(defun proof-only-whitespace-to-locked-region-p 366,12886
(defun proof-in-locked-region-p 376,13213
(defun proof-goto-end-of-locked 388,13470
(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 405,14229
(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 416,14710
(defun proof-end-of-locked-visible-p 430,15330
(defvar pg-idioms 448,15948
(defvar pg-visibility-specs 451,16044
(defconst pg-default-invisibility-spec456,16251
(defun pg-clear-script-portions 459,16320
(defun pg-remove-script-element 466,16594
(defsubst pg-visname 471,16783
(defun pg-add-element 475,16928
(defun pg-open-invisible-span 511,18621
(defun pg-remove-element 522,18984
(defun pg-make-element-invisible 529,19254
(defun pg-make-element-visible 535,19498
(defun pg-toggle-element-visibility 539,19641
(defun pg-redisplay-for-gnuemacs 546,19928
(defun pg-show-all-portions 550,20075
(defun pg-show-all-proofs 570,20793
(defun pg-hide-all-proofs 575,20921
(defun pg-add-proof-element 580,21052
(defun pg-span-name 594,21710
(defvar pg-span-context-menu-keymap615,22410
(defun pg-last-output-displayform 622,22648
(defun pg-set-span-helphighlights 635,23125
(defun proof-complete-buffer-atomic 672,24467
(defun proof-register-possibly-new-processed-file713,26372
(defun proof-inform-prover-file-retracted 759,28203
(defun proof-auto-retract-dependencies 779,29054
(defun proof-unregister-buffer-file-name 833,31598
(defun proof-protected-process-or-retract 879,33423
(defun proof-deactivate-scripting-auto 906,34593
(defun proof-deactivate-scripting 915,34951
(defun proof-activate-scripting 1048,40207
(defun proof-toggle-active-scripting 1163,45312
(defun proof-done-advancing 1202,46557
(defun proof-done-advancing-comment 1281,49542
(defun proof-done-advancing-save 1315,50918
(defun proof-make-goalsave 1403,54309
(defun proof-get-name-from-goal 1419,55092
(defun proof-done-advancing-autosave 1439,56117
(defun proof-done-advancing-other 1504,58661
(defun proof-segment-up-to-parser 1532,59614
(defun proof-script-generic-parse-find-comment-end 1596,61697
(defun proof-script-generic-parse-cmdend 1605,62111
(defun proof-script-generic-parse-cmdstart 1630,62998
(defun proof-script-generic-parse-sexp 1693,65691
(defun proof-cmdstart-add-segment-for-cmd 1717,66623
(defun proof-segment-up-to-cmdstart 1769,68836
(defun proof-segment-up-to-cmdend 1830,71196
(defun proof-semis-to-vanillas 1902,73875
(defun proof-assert-until-point 1934,74974
(defun proof-assert-semis 1949,75567
(defun proof-retract-before-change 1957,75912
(defun proof-inside-comment 1966,76230
(defun proof-insert-pbp-command 1980,76465
(defun proof-insert-sendback-command 1994,76944
(defun proof-done-retracting 2020,77847
(defun proof-setup-retract-action 2055,79288
(defun proof-last-goal-or-goalsave 2065,79771
(defun proof-retract-target 2089,80676
(defun proof-retract-until-point-interactive 2174,84318
(defun proof-retract-until-point 2182,84703
(define-derived-mode proof-mode 2225,86429
(defun proof-script-set-visited-file-name 2262,87797
(defun proof-script-set-buffer-hooks 2286,88806
(defun proof-script-kill-buffer-fn 2294,89224
(defun proof-config-done-related 2326,90541
(defun proof-generic-goal-command-p 2394,93064
(defun proof-generic-state-preserving-p 2399,93277
(defun proof-generic-count-undos 2408,93794
(defun proof-generic-find-and-forget 2437,94832
(defconst proof-script-important-settings2490,96671
(defun proof-config-done 2505,97217
(defun proof-setup-parsing-mechanism 2573,99495
(defun proof-setup-imenu 2617,101348
(deflocal proof-segment-up-to-cache 2641,102122
(deflocal proof-segment-up-to-cache-start 2642,102163
(deflocal proof-last-edited-low-watermark 2643,102208
(defun proof-segment-up-to-using-cache 2653,102695
(defun proof-segment-cache-contents-for 2682,103843
(defun proof-script-after-change-function 2694,104212
(defun proof-script-set-after-change-functions 2706,104719

generic/proof-shell.el,3801
(defvar proof-marker 36,824
(defvar proof-action-list 39,920
(defvar proof-shell-silent 57,1570
(defvar proof-shell-last-prompt 64,1861
(defvar proof-shell-last-output-kind 68,2031
(defvar proof-shell-delayed-output 89,2829
(defvar proof-shell-delayed-output-kind 92,2951
(defvar proof-shell-delayed-output-flags 95,3084
(defcustom proof-shell-active-scripting-indicator104,3280
(defun proof-shell-ready-prover 154,4664
(defsubst proof-shell-live-buffer 168,5203
(defun proof-shell-available-p 175,5442
(defun proof-grab-lock 181,5664
(defun proof-release-lock 194,6266
(defcustom proof-shell-fiddle-frames 209,6663
(defun proof-shell-set-text-representation 215,6885
(defun proof-shell-start 226,7346
(defvar proof-shell-kill-function-hooks 411,13611
(defun proof-shell-kill-function 414,13709
(defun proof-shell-clear-state 503,17513
(defun proof-shell-exit 518,17953
(defun proof-shell-bail-out 530,18398
(defun proof-shell-restart 539,18875
(defvar proof-shell-urgent-message-marker 579,20162
(defvar proof-shell-urgent-message-scanner 582,20283
(defun proof-shell-handle-output 586,20410
(defsubst proof-shell-strip-output-markup 623,21724
(defvar proof-shell-no-error-display 635,22089
(defun proof-shell-handle-error 641,22292
(defun proof-shell-handle-interrupt 658,23100
(defun proof-shell-error-or-interrupt-action 673,23766
(defun proof-goals-pos 703,24962
(defun proof-pbp-focus-on-first-goal 708,25173
(defsubst proof-shell-string-match-safe 720,25589
(defun proof-shell-classify-output 725,25751
(defvar proof-shell-expecting-output 831,29860
(defvar proof-shell-interrupt-pending 835,30019
(defun proof-interrupt-process 841,30244
(defun proof-shell-insert 879,31677
(defun proof-shell-action-list-item 927,33311
(defun proof-shell-set-silent 933,33556
(defun proof-shell-start-silent-item 939,33775
(defun proof-shell-clear-silent 945,33964
(defun proof-shell-stop-silent-item 951,34186
(defun proof-shell-should-be-silent 958,34455
(defsubst proof-shell-invoke-callback 972,35042
(defun proof-append-alist 978,35252
(defun proof-start-queue 1036,37460
(defun proof-extend-queue 1047,37809
(defun proof-shell-exec-loop 1056,38188
(defun proof-shell-insert-loopback-cmd 1135,40845
(defun proof-shell-process-urgent-message 1163,42167
(defun proof-shell-process-urgent-message-default 1221,44390
(defun proof-shell-process-urgent-message-trace 1239,45080
(defun proof-shell-process-urgent-message-retract 1252,45640
(defun proof-shell-process-urgent-message-elisp 1273,46488
(defun proof-shell-process-urgent-message-thmdeps 1288,46983
(defun proof-shell-message 1302,47363
(defun proof-shell-strip-eager-annotations 1309,47615
(defvar proof-shell-minibuffer-urgent-interactive-input-history 1324,48148
(defun proof-shell-minibuffer-urgent-interactive-input 1326,48218
(defun proof-shell-filter 1342,48685
(defun proof-shell-filter-first-command 1437,51779
(defun proof-shell-cleanup 1452,52322
(defun proof-shell-process-urgent-messages 1457,52470
(defun proof-shell-filter-manage-output 1524,54933
(defun proof-shell-handle-delayed-output 1561,56397
(defvar pg-last-tracing-output-time 1602,57946
(defconst pg-slow-mode-duration 1605,58052
(defconst pg-fast-tracing-mode-threshold 1608,58134
(defvar pg-tracing-cleanup-timer 1611,58262
(defun pg-tracing-tight-loop 1613,58301
(defun pg-finish-tracing-display 1656,60013
(defun proof-shell-wait 1674,60377
(defun proof-done-invisible 1693,61285
(defun proof-shell-invisible-command 1699,61455
(defun proof-shell-invisible-cmd-get-result 1746,62999
(defun proof-shell-invisible-command-invisible-result 1758,63435
(define-derived-mode proof-shell-mode 1777,63872
(defconst proof-shell-important-settings1819,65265
(defun proof-shell-config-done 1825,65380

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-table141,4817
(defcustom proof-assistants 176,5930
(defun proof-ready-for-assistant 205,7086

generic/proof-splash.el,800
(defcustom proof-splash-enable 17,318
(defcustom proof-splash-time 22,470
(defcustom proof-splash-contents30,754
(defconst proof-splash-startup-msg70,2128
(defconst proof-splash-welcome 79,2506
(defsubst proof-emacs-imagep 86,2681
(defun proof-get-image 91,2806
(defvar proof-splash-timeout-conf 113,3606
(defun proof-splash-centre-spaces 116,3692
(defun proof-splash-remove-screen 131,4315
(defvar proof-splash-seen 145,4774
(defun proof-splash-insert-contents 148,4876
(defun proof-splash-display-screen 187,6070
(defalias 'pg-about pg-about
204,6729
(defun proof-splash-message 207,6795
(defun proof-splash-timeout-waiter 220,7239
(defvar proof-splash-old-frame-title-format 229,7625
(defun proof-splash-set-frame-titles 231,7675
(defun proof-splash-unset-frame-titles 240,7990

generic/proof-syntax.el,996
(defsubst proof-ids-to-regexp 17,445
(defsubst proof-anchor-regexp 21,618
(defconst proof-no-regexp 25,723
(defsubst proof-regexp-alt 28,814
(defsubst proof-re-search-forward-region 37,1123
(defsubst proof-search-forward 50,1621
(defsubst proof-replace-regexp-in-string 56,1876
(defsubst proof-re-search-forward 61,2127
(defsubst proof-re-search-backward 66,2385
(defsubst proof-string-match 71,2646
(defsubst proof-string-match-safe 76,2875
(defsubst proof-stringfn-match 80,3079
(defsubst proof-looking-at 87,3342
(defsubst proof-looking-at-safe 92,3529
(defsubst proof-looking-at-syntactic-context-default 96,3674
(defsubst proof-replace-string 107,4051
(defsubst proof-replace-regexp 112,4255
(defsubst proof-replace-regexp-nocasefold 117,4464
(defvar proof-id 125,4746
(defsubst proof-ids 131,4966
(defun proof-zap-commas 145,5458
(defun proof-format 161,5954
(defun proof-format-filename 180,6593
(defun proof-insert 227,7995
(defun proof-splice-separator 264,9012

generic/proof-toolbar.el,2357
(defun proof-toolbar-function 33,837
(defun proof-toolbar-icon 36,934
(defun proof-toolbar-enabler 39,1035
(defun proof-toolbar-make-icon 46,1187
(defun proof-toolbar-make-toolbar-items 55,1495
(defvar proof-toolbar-map 80,2300
(defun proof-toolbar-available-p 83,2399
(defun proof-toolbar-setup 92,2675
(defalias 'proof-toolbar-enable proof-toolbar-enable
110,3471
(defalias 'proof-toolbar-undo proof-toolbar-undo
140,4451
(defun proof-toolbar-undo-enable-p 142,4519
(defalias 'proof-toolbar-delete proof-toolbar-delete
149,4677
(defun proof-toolbar-delete-enable-p 151,4758
(defalias 'proof-toolbar-home proof-toolbar-home
159,4940
(defalias 'proof-toolbar-next proof-toolbar-next
163,5007
(defun proof-toolbar-next-enable-p 165,5078
(defalias 'proof-toolbar-goto proof-toolbar-goto
171,5194
(defun proof-toolbar-goto-enable-p 173,5244
(defalias 'proof-toolbar-retract proof-toolbar-retract
178,5329
(defun proof-toolbar-retract-enable-p 180,5386
(defalias 'proof-toolbar-use proof-toolbar-use
186,5505
(defalias 'proof-toolbar-use-enable-p proof-toolbar-use-enable-p
187,5557
(defalias 'proof-toolbar-restart proof-toolbar-restart
191,5638
(defalias 'proof-toolbar-goal proof-toolbar-goal
195,5703
(defalias 'proof-toolbar-qed proof-toolbar-qed
199,5761
(defun proof-toolbar-qed-enable-p 201,5810
(defalias 'proof-toolbar-state proof-toolbar-state
209,5972
(defalias 'proof-toolbar-state-enable-p proof-toolbar-state-enable-p
210,6015
(defalias 'proof-toolbar-context proof-toolbar-context
214,6094
(defalias 'proof-toolbar-context-enable-p proof-toolbar-context-enable-p
215,6140
(defalias 'proof-toolbar-command proof-toolbar-command
219,6221
(defalias 'proof-toolbar-command-enable-p proof-toolbar-command-enable-p
220,6277
(defun proof-toolbar-help 224,6382
(defalias 'proof-toolbar-find proof-toolbar-find
230,6462
(defalias 'proof-toolbar-find-enable-p proof-toolbar-find-enable-p
231,6514
(defalias 'proof-toolbar-info proof-toolbar-info
235,6589
(defalias 'proof-toolbar-info-enable-p proof-toolbar-info-enable-p
236,6644
(defalias 'proof-toolbar-visibility proof-toolbar-visibility
240,6742
(defun proof-toolbar-visibility-enable-p 242,6802
(defalias 'proof-toolbar-interrupt proof-toolbar-interrupt
247,6916
(defun proof-toolbar-interrupt-enable-p 248,6977
(defun proof-toolbar-scripting-menu 256,7130

generic/proof-unicode-tokens.el,496
(defvar proof-unicode-tokens-initialised 28,760
(defun proof-unicode-tokens-init 31,867
(defun proof-unicode-tokens-configure 45,1369
(defun proof-unicode-tokens-enable 57,1815
(defun proof-unicode-tokens-mode-if-enabled 71,2502
(defun proof-unicode-tokens-set-global 77,2701
(defun proof-unicode-tokens-reconfigure 95,3339
(defun proof-unicode-tokens-configure-prover 121,4227
(defun proof-unicode-tokens-activate-prover 126,4408
(defun proof-unicode-tokens-deactivate-prover 133,4654

generic/proof-useropts.el,1416
(defgroup proof-user-options 21,552
(defun proof-set-value 29,731
(defcustom proof-electric-terminator-enable 62,1854
(defcustom proof-toolbar-enable 74,2386
(defcustom proof-imenu-enable 80,2559
(defcustom pg-show-hints 86,2730
(defcustom proof-trace-output-slow-catchup 92,2923
(defcustom proof-strict-state-preserving 102,3420
(defcustom proof-strict-read-only 115,4029
(defcustom proof-allow-undo-in-read-only 127,4539
(defcustom proof-three-window-enable 134,4821
(defcustom proof-multiple-frames-enable 153,5571
(defcustom proof-delete-empty-windows 162,5904
(defcustom proof-shrink-windows-tofit 173,6435
(defcustom proof-auto-raise-buffers 180,6707
(defcustom proof-colour-locked 187,6942
(defcustom proof-query-file-save-when-activating-scripting195,7192
(defcustom proof-one-command-per-line211,7912
(defcustom proof-prog-name-ask218,8136
(defcustom proof-prog-name-guess224,8296
(defcustom proof-tidy-response232,8561
(defcustom proof-keep-response-history246,9024
(defcustom pg-input-ring-size 256,9412
(defcustom proof-general-debug 261,9564
(defcustom proof-use-parser-cache 272,9973
(defcustom proof-follow-mode 282,10270
(defcustom proof-auto-action-when-deactivating-scripting 306,11447
(defcustom proof-script-command-separator 329,12396
(defcustom proof-rsh-command 337,12688
(defcustom proof-disappearing-proofs 353,13238
(defcustom proof-full-annotation 358,13399

generic/proof-utils.el,1925
(defmacro deflocal 62,1802
(defmacro proof-with-current-buffer-if-exists 69,2040
(deflocal proof-buffer-type 75,2250
(defmacro proof-with-script-buffer 81,2530
(defmacro proof-map-buffers 92,2911
(defmacro proof-sym 97,3096
(defsubst proof-try-require 102,3257
(defun proof-save-some-buffers 115,3588
(defmacro proof-ass-sym 164,5189
(defmacro proof-ass-symv 170,5448
(defmacro proof-ass 176,5706
(defun proof-defpgcustom-fn 182,5958
(defun undefpgcustom 203,6828
(defmacro defpgcustom 209,7052
(defun proof-defpgdefault-fn 220,7470
(defmacro defpgdefault 234,7928
(defmacro defpgfun 245,8290
(defmacro proof-eval-when-ready-for-assistant 255,8554
(defun proof-file-truename 268,8945
(defun proof-files-to-buffers 272,9128
(defun proof-buffers-in-mode 280,9368
(defun pg-save-from-death 294,9818
(defun proof-define-keys 313,10435
(defun pg-remove-specials 324,10720
(defun pg-remove-specials-in-string 334,11056
(defun proof-warn-if-unset 345,11282
(defun proof-get-window-for-buffer 350,11500
(defun proof-display-and-keep-buffer 401,13808
(defun proof-clean-buffer 443,15531
(defun proof-message 459,16187
(defun proof-warning 464,16400
(defun pg-internal-warning 470,16682
(defun proof-debug 477,16949
(defun proof-switch-to-buffer 485,17298
(defun proof-resize-window-tofit 507,18422
(defun proof-submit-bug-report 601,22268
(defun proof-deftoggle-fn 636,23625
(defmacro proof-deftoggle 651,24278
(defun proof-defintset-fn 658,24652
(defmacro proof-defintset 674,25356
(defun proof-defstringset-fn 681,25733
(defmacro proof-defstringset 694,26359
(defun proof-escape-keymap-doc 707,26815
(defmacro proof-defshortcut 711,26955
(defmacro proof-definvisible 726,27553
(defun pg-custom-save-vars 753,28480
(defun pg-custom-reset-vars 769,29124
(defun proof-locate-executable 782,29461
(defun pg-current-word-pos 797,30016
(defun proof-looking-at-syntactic-context 844,31732

lib/bufhist.el,1099
(defun bufhist-ring-update 34,1239
(defgroup bufhist 43,1561
(defcustom bufhist-ring-size 47,1642
(defvar bufhist-ring 52,1753
(defvar bufhist-ring-pos 55,1827
(defvar bufhist-lastswitch-modified-tick 58,1906
(defvar bufhist-read-only-history 61,2012
(defvar bufhist-saved-mode-line-format 64,2083
(defun bufhist-mode-line-format-entry 67,2184
(defun bufhist-get-buffer-contents 99,3452
(defun bufhist-restore-buffer-contents 111,3935
(defun bufhist-checkpoint 119,4222
(defun bufhist-erase-buffer 127,4591
(defun bufhist-checkpoint-and-erase 137,4935
(defun bufhist-switch-to-index 143,5121
(defun bufhist-first 182,6720
(defun bufhist-last 187,6879
(defun bufhist-prev 192,7023
(defun bufhist-next 200,7246
(defun bufhist-delete 205,7386
(defun bufhist-clear 217,7927
(defun bufhist-init 232,8322
(defun bufhist-exit 257,9255
(defun bufhist-set-readwrite 267,9519
(defun bufhist-before-change-function 282,10139
(defun bufhist-make-buttons 294,10554
(defconst bufhist-minor-mode-map308,10813
(define-minor-mode bufhist-mode321,11290
(defun bufhist-toggle-fn 341,12070

lib/holes.el,2465
(defvar holes-default-hole 44,1121
(defvar holes-active-hole 50,1299
(defgroup holes 60,1496
(defcustom holes-empty-hole-string 65,1595
(defcustom holes-empty-hole-regexp 70,1738
(defface active-hole-face92,2440
(defface inactive-hole-face102,2856
(defvar hole-map116,3297
(defvar holes-mode-map126,3688
(defun holes-region-beginning-or-nil 172,5425
(defun holes-region-end-or-nil 176,5561
(defun holes-copy-active-region 180,5679
(defun holes-is-hole-p 186,5889
(defun holes-hole-start-position 190,5981
(defun holes-hole-end-position 196,6164
(defun holes-hole-buffer 201,6335
(defun holes-hole-at 207,6509
(defun holes-active-hole-exist-p 212,6679
(defun holes-active-hole-start-position 219,6932
(defun holes-active-hole-end-position 227,7300
(defun holes-active-hole-buffer 236,7663
(defun holes-goto-active-hole 244,7964
(defun holes-highlight-hole-as-active 253,8223
(defun holes-highlight-hole 261,8531
(defun holes-disable-active-hole 269,8818
(defun holes-set-active-hole 282,9350
(defun holes-is-in-hole-p 292,9695
(defun holes-make-hole 296,9833
(defun holes-make-hole-at 314,10489
(defun holes-clear-hole 328,10942
(defun holes-clear-hole-at 337,11200
(defun holes-map-holes 345,11456
(defun holes-clear-all-buffer-holes 349,11610
(defun holes-next 359,11911
(defun holes-next-after-active-hole 366,12163
(defun holes-set-active-hole-next 373,12379
(defun holes-replace-segment 392,12916
(defun holes-replace 401,13269
(defun holes-replace-active-hole 429,14447
(defun holes-replace-update-active-hole 436,14738
(defun holes-delete-update-active-hole 454,15385
(defun holes-set-make-active-hole 462,15612
(defalias 'holes-track-mouse-selection holes-track-mouse-selection
477,16167
(defsubst holes-track-mouse-clicks 478,16225
(defun holes-mouse-replace-active-hole 482,16335
(defun holes-destroy-hole 496,16806
(defsubst holes-hole-at-event 510,17188
(defun holes-mouse-destroy-hole 514,17288
(defun holes-mouse-forget-hole 521,17509
(defun holes-mouse-set-make-active-hole 531,17801
(defun holes-mouse-set-active-hole 547,18300
(defun holes-set-point-next-hole-destroy 556,18551
(defun holes-replace-string-by-holes-backward 582,19532
(defun holes-skeleton-end-hook 600,20232
(defconst holes-jump-doc609,20670
(defun holes-replace-string-by-holes-backward-jump 616,20876
(define-minor-mode holes-mode 633,21558
(defun holes-abbrev-complete 728,25040
(defun holes-insert-and-expand 738,25383

lib/local-vars-list.el,373
(defconst local-vars-list-doc 28,825
(defun local-vars-list-insert-empty-zone 44,1387
(defun local-vars-list-find 82,2090
(defun local-vars-list-goto-var 101,2861
(defun local-vars-list-get-current 127,3908
(defun local-vars-list-set-current 148,4758
(defun local-vars-list-get 171,5473
(defun local-vars-list-get-safe 188,6003
(defun local-vars-list-set 193,6197

lib/maths-menu.el,242
(defvar maths-menu-filter-predicate 56,2317
(defvar maths-menu-tokenise-insert 59,2426
(defun maths-menu-build-menu 62,2563
(defvar maths-menu-menu84,3324
(defvar maths-menu-mode-map344,12882
(define-minor-mode maths-menu-mode352,13101

lib/pg-dev.el,138
(defconst pg-dev-lisp-font-lock-keywords48,1477
(defun unload-pg 75,2271
(defun profile-pg 103,3134
(defun pg-bug-references 120,3560

lib/pg-fontsets.el,210
(defcustom pg-fontsets-default-fontset 28,780
(defvar pg-fontsets-names 33,926
(defun pg-fontsets-make-fontsetsizes 36,1007
(defconst pg-fontsets-base-fonts55,1768
(defun pg-fontsets-make-fontsets 61,1898

lib/proof-compat.el,260
(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
163,5191

lib/scomint.el,873
(defface scomint-highlight-input 19,492
(defface scomint-highlight-prompt23,608
(defvar scomint-buffer-maximum-size 30,846
(defvar scomint-output-filter-functions 35,1037
(defvar scomint-mode-map39,1148
(defvar scomint-last-input-start 45,1327
(defvar scomint-last-input-end 46,1365
(defvar scomint-last-output-start 47,1401
(defvar scomint-exec-hook 49,1441
(define-derived-mode scomint-mode 59,1823
(defun scomint-check-proc 78,2722
(defun scomint-make-in-buffer 86,3059
(defun scomint-make 110,4326
(defun scomint-exec 123,5037
(defun scomint-exec-1 160,6630
(defalias 'scomint-send-string scomint-send-string
210,8760
(defun scomint-send-eof 212,8814
(defun scomint-send-input 218,8956
(defun scomint-truncate-buffer 261,10457
(defun scomint-strip-ctrl-m 274,10851
(defun scomint-output-filter 288,11414
(defun scomint-interrupt-process 360,14146

lib/span.el,1354
(defalias 'span-start span-start
22,609
(defalias 'span-end span-end
23,647
(defalias 'span-set-property span-set-property
24,681
(defalias 'span-property span-property
25,724
(defalias 'span-make span-make
26,763
(defalias 'span-detach span-detach
27,799
(defalias 'span-set-endpoints span-set-endpoints
28,839
(defalias 'span-buffer span-buffer
29,884
(defun span-read-only-hook 31,925
(defsubst span-read-only 36,1115
(defsubst span-read-write 43,1425
(defsubst span-give-warning 48,1595
(defsubst span-write-warning 53,1741
(defsubst span-lt 65,2307
(defsubst spans-at-point-prop 70,2451
(defsubst spans-at-region-prop 79,2642
(defsubst span-at 89,2908
(defsubst span-delete 93,3034
(defsubst span-mapcar-spans 100,3256
(defsubst span-mapc-spans 104,3431
(defun span-at-before 108,3602
(defsubst prev-span 125,4326
(defsubst next-span 131,4479
(defsubst span-live-p 137,4693
(defsubst span-raise 143,4859
(defsubst span-string 147,4992
(defsubst set-span-properties 152,5152
(defsubst span-find-span 158,5346
(defsubst span-at-event 166,5658
(defun fold-spans 172,5855
(defsubst span-detached-p 186,6388
(defsubst set-span-face 190,6504
(defsubst set-span-keymap 194,6602
(defsubst span-delete-spans 202,6771
(defsubst span-property-safe 206,6933
(defsubst span-set-start 210,7070
(defsubst span-set-end 214,7202

lib/texi-docstring-magic.el,584
(defun texi-docstring-magic-find-face 88,3027
(defun texi-docstring-magic-splice-sep 93,3192
(defconst texi-docstring-magic-munge-table103,3497
(defun texi-docstring-magic-untabify 193,7260
(defun texi-docstring-magic-munge-docstring 203,7575
(defun texi-docstring-magic-texi 242,8856
(defun texi-docstring-magic-format-default 255,9296
(defun texi-docstring-magic-texi-for 271,9929
(defconst texi-docstring-magic-comment329,11888
(defun texi-docstring-magic 335,12042
(defun texi-docstring-magic-face-at-point 369,13121
(defun texi-docstring-magic-insert-magic 384,13644

lib/unicode-chars.el,80
(defvar unicode-chars-alist12,348
(defun unicode-chars-list-chars 5051,245975

lib/unicode-tokens.el,5174
(defvar unicode-tokens-token-symbol-map 56,1828
(defvar unicode-tokens-token-format 75,2450
(defvar unicode-tokens-token-variant-format-regexp 81,2699
(defvar unicode-tokens-shortcut-alist 92,3081
(defvar unicode-tokens-shortcut-replacement-alist 98,3358
(defvar unicode-tokens-control-region-format-regexp 106,3564
(defvar unicode-tokens-control-char-format-regexp 113,3932
(defvar unicode-tokens-control-regions 120,4293
(defvar unicode-tokens-control-characters 123,4369
(defvar unicode-tokens-control-char-format 126,4451
(defvar unicode-tokens-control-region-format-start 129,4564
(defvar unicode-tokens-control-region-format-end 132,4681
(defvar unicode-tokens-tokens-customizable-variables 135,4794
(defconst unicode-tokens-configuration-variables142,4962
(defun unicode-tokens-config 157,5361
(defun unicode-tokens-config-var 161,5506
(defun unicode-tokens-copy-configuration-variables 173,5946
(defvar unicode-tokens-token-list 201,7162
(defvar unicode-tokens-hash-table 204,7282
(defvar unicode-tokens-token-match-regexp 207,7398
(defvar unicode-tokens-uchar-hash-table 210,7510
(defvar unicode-tokens-uchar-regexp 214,7697
(defgroup unicode-tokens-faces 222,7882
(defconst unicode-tokens-font-family-alternatives232,8179
(defface unicode-tokens-symbol-font-face246,8627
(defface unicode-tokens-script-font-face264,9267
(defface unicode-tokens-fraktur-font-face269,9411
(defface unicode-tokens-serif-font-face274,9536
(defface unicode-tokens-sans-font-face279,9663
(defface unicode-tokens-highlight-face284,9785
(defconst unicode-tokens-fonts293,10147
(defconst unicode-tokens-fontsymb-properties302,10364
(define-widget 'unicode-tokens-token-symbol-map unicode-tokens-token-symbol-map
328,11809
(define-widget 'unicode-tokens-shortcut-alist unicode-tokens-shortcut-alist
346,12361
(defconst unicode-tokens-font-lock-extra-managed-props359,12692
(defun unicode-tokens-font-lock-keywords 363,12846
(defun unicode-tokens-usable-composition 403,14499
(defun unicode-tokens-help-echo 416,14876
(defvar unicode-tokens-show-symbols 420,15040
(defun unicode-tokens-interpret-composition 423,15154
(defun unicode-tokens-font-lock-compose-symbol 441,15667
(defun unicode-tokens-prepend-text-properties-in-match 471,16898
(defun unicode-tokens-prepend-text-property 485,17476
(defun unicode-tokens-show-symbols 510,18621
(defun unicode-tokens-symbs-to-props 518,18931
(defvar unicode-tokens-show-controls 538,19630
(defun unicode-tokens-show-controls 541,19721
(defun unicode-tokens-control-char 554,20306
(defun unicode-tokens-control-region 563,20745
(defun unicode-tokens-control-font-lock-keywords 574,21292
(defvar unicode-tokens-use-shortcuts 585,21616
(defun unicode-tokens-use-shortcuts 588,21719
(defun unicode-tokens-map-ordering 606,22325
(defun unicode-tokens-quail-define-rules 615,22678
(defun unicode-tokens-insert-token 638,23355
(defun unicode-tokens-annotate-region 647,23659
(defun unicode-tokens-insert-control 671,24497
(defun unicode-tokens-insert-uchar-as-token 681,24946
(defun unicode-tokens-delete-token-near-point 687,25167
(defun unicode-tokens-prev-token 701,25729
(defun unicode-tokens-rotate-token-forward 710,26079
(defun unicode-tokens-rotate-token-backward 737,26969
(defun unicode-tokens-replace-shortcut-match 742,27171
(defun unicode-tokens-replace-shortcuts 751,27541
(defun unicode-tokens-replace-unicode-match 764,28120
(defun unicode-tokens-replace-unicode 771,28421
(defun unicode-tokens-copy-token 787,29001
(define-button-type 'unicode-tokens-listunicode-tokens-list
794,29222
(defun unicode-tokens-list-tokens 800,29426
(defun unicode-tokens-list-shortcuts 839,30610
(defalias 'unicode-tokens-list-unicode-chars unicode-tokens-list-unicode-chars
857,31248
(defun unicode-tokens-encode-in-temp-buffer 859,31321
(defun unicode-tokens-encode 879,32083
(defun unicode-tokens-encode-str 884,32304
(defun unicode-tokens-copy 888,32466
(defun unicode-tokens-paste 897,32872
(defvar unicode-tokens-highlight-unicode 916,33593
(defconst unicode-tokens-unicode-highlight-patterns919,33685
(defun unicode-tokens-highlight-unicode 923,33854
(defun unicode-tokens-highlight-unicode-setkeywords 935,34317
(defun unicode-tokens-initialise 947,34686
(defvar unicode-tokens-mode-map 959,35138
(define-minor-mode unicode-tokens-mode962,35235
(defun unicode-tokens-set-font-var 1089,39479
(defun unicode-tokens-set-font-var-aux 1105,39970
(defun unicode-tokens-mouse-set-font 1130,41012
(defsubst unicode-tokens-face-font-sym 1143,41526
(defun unicode-tokens-set-font-restart 1147,41706
(defun unicode-tokens-save-fonts 1158,42016
(defun unicode-tokens-custom-save-faces 1166,42272
(define-key unicode-tokens-mode-map 1183,42728
(define-key unicode-tokens-mode-map 1185,42820
(define-key unicode-tokens-mode-map1187,42911
(define-key unicode-tokens-mode-map1189,43017
(define-key unicode-tokens-mode-map1192,43132
(define-key unicode-tokens-mode-map1194,43241
(define-key unicode-tokens-mode-map1196,43349
(define-key unicode-tokens-mode-map1198,43455
(defun unicode-tokens-customize-submenu 1206,43579
(defun unicode-tokens-define-menu 1213,43802

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,414
(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 267,9384
(defun mmm-match-and-verify 281,9892
(defun mmm-get-form 307,10943
(defun mmm-default-get-form 318,11418

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 102,3169
(defvar mmm-c-derived-modes109,3279
(defvar mmm-save-local-variables113,3398
(defvar mmm-buffer-saved-locals 339,10179
(defvar mmm-region-saved-locals-defaults 344,10379
(defvar mmm-region-saved-locals-for-dominant 350,10639
(defgroup mmm-faces 360,11016
(defcustom mmm-submode-decoration-level 366,11187
(defface mmm-init-submode-face 384,12031
(defface mmm-cleanup-submode-face 388,12171
(defface mmm-declaration-submode-face 392,12308
(defface mmm-comment-submode-face 396,12454
(defface mmm-output-submode-face 400,12607
(defface mmm-special-submode-face 404,12756
(defface mmm-code-submode-face 408,12920
(defface mmm-default-submode-face 412,13059
(defface mmm-delimiter-face 417,13267
(defcustom mmm-mode-string 424,13393
(defcustom mmm-submode-mode-line-format 429,13524
(defvar mmm-primary-mode-display-name 446,14179
(defvar mmm-buffer-mode-display-name 451,14393
(defun mmm-set-mode-line 457,14692
(defvar mmm-classes 481,15500
(defvar mmm-global-classes 487,15745
(defcustom mmm-mode-ext-classes-alist 494,15927
(defun mmm-add-mode-ext-class 513,16717
(defcustom mmm-major-mode-preferences522,17042
(defun mmm-add-to-major-mode-preferences 540,17770
(defun mmm-ensure-modename 556,18528
(defun mmm-modename->function 565,18831
(defcustom mmm-delimiter-mode 579,19280
(defcustom mmm-mode-prefix-key 589,19549
(defcustom mmm-command-modifiers 594,19676
(defcustom mmm-insert-modifiers 608,20309
(defcustom mmm-use-old-command-keys 623,20987
(defun mmm-use-old-command-keys 633,21451
(defcustom mmm-mode-hook 641,21643
(defun mmm-run-constructed-hook 661,22450
(defun mmm-run-major-hook 669,22794
(defun mmm-run-submode-hook 672,22871
(defvar mmm-class-hooks-run 675,22958
(defun mmm-run-class-hook 680,23130
(defvar mmm-primary-mode-entry-hook 685,23302
(defcustom mmm-major-mode-hook 700,23949
(defun mmm-run-major-mode-hook 714,24580
(defcustom mmm-global-mode 727,25121
(defcustom mmm-never-modes743,25788
(defvar mmm-set-file-name-for-modes 761,26088
(defvar mmm-mode 772,26447
(defvar mmm-primary-mode 780,26655
(defvar mmm-classes-alist 791,27021
(defun mmm-add-classes 946,35228
(defun mmm-add-group 951,35393
(defun mmm-add-to-group 961,35766
(defconst mmm-version 975,36193
(defun mmm-version 978,36258
(defvar mmm-temp-buffer-name 985,36401
(defvar mmm-interactive-history 991,36531
(defun mmm-add-to-history 997,36800
(defun mmm-clear-history 1000,36883
(defvar mmm-mode-ext-classes 1008,37068
(defun mmm-get-mode-ext-classes 1013,37279
(defun mmm-clear-mode-ext-classes 1022,37606
(defun mmm-mode-ext-applies 1026,37731
(defun mmm-get-all-classes 1040,38110

doc/ProofGeneral.texi,5693
@node Top164,4937
@node Preface201,6044
@node News for Version 4.0News for Version 4.0
224,6633
@node Future241,7193
@node Credits270,8528
@node Introducing Proof GeneralIntroducing Proof General
380,12340
@node Installing Proof GeneralInstalling Proof General
435,14318
@node Quick start guideQuick start guide
449,14767
@node Features of Proof GeneralFeatures of Proof General
493,16888
@node Supported proof assistantsSupported proof assistants
582,20825
@node Prerequisites for this manualPrerequisites for this manual
631,22714
@node Organization of this manualOrganization of this manual
675,24333
@node Basic Script ManagementBasic Script Management
701,25161
@node Walkthrough example in IsabelleWalkthrough example in Isabelle
720,25761
@node Proof scriptsProof scripts
986,35994
@node Script buffersScript buffers
1029,38114
@node Locked queue and editing regionsLocked queue and editing regions
1051,38691
@node Goal-save sequencesGoal-save sequences
1107,40838
@node Active scripting bufferActive scripting buffer
1144,42324
@node Summary of Proof General buffersSummary of Proof General buffers
1213,45744
@node Script editing commandsScript editing commands
1276,48484
@node Script processing commandsScript processing commands
1356,51442
@node Proof assistant commandsProof assistant commands
1483,56735
@node Toolbar commandsToolbar commands
1655,62840
@node Interrupting during trace outputInterrupting during trace output
1679,63769
@node Subterm Activation and Proof by PointingSubterm Activation and Proof by Pointing
1718,65690
@node Goals buffer commandsGoals buffer commands
1733,66202
@node Advanced Script Management and EditingAdvanced Script Management and Editing
1822,69766
@node Document centred workingDocument centred working
1854,70981
@node Visibility of completed proofsVisibility of completed proofs
1920,73085
@node Switching between proof scriptsSwitching between proof scripts
1975,75008
@node View of processed files View of processed files 
2012,76980
@node Retracting across filesRetracting across files
2072,80031
@node Asserting across filesAsserting across files
2085,80662
@node Automatic multiple file handlingAutomatic multiple file handling
2098,81228
@node Escaping script managementEscaping script management
2123,82262
@node Editing featuresEditing features
2180,84374
@node Support for other PackagesSupport for other Packages
2251,87166
@node Syntax highlightingSyntax highlighting
2283,88040
@node Unicode supportUnicode support
2312,89044
@node Imenu and Speedbar (and Function Menu)Imenu and Speedbar (and Function Menu)
2468,95279
@node Support for outline modeSupport for outline mode
2523,97323
@node Support for completionSupport for completion
2548,98452
@node Support for tagsSupport for tags
2605,100614
@node Customizing Proof GeneralCustomizing Proof General
2657,102942
@node Basic optionsBasic options
2697,104612
@node How to customizeHow to customize
2721,105370
@node Display customizationDisplay customization
2768,107337
@node User optionsUser options
2922,113736
@node Changing facesChanging faces
3163,122214
@node Tweaking configuration settingsTweaking configuration settings
3238,124883
@node Hints and TipsHints and Tips
3295,127409
@node Adding your own keybindingsAdding your own keybindings
3314,128010
@node Using file variablesUsing file variables
3378,130597
@node Using abbreviationsUsing abbreviations
3437,132783
@node LEGO Proof GeneralLEGO Proof General
3476,134198
@node LEGO specific commandsLEGO specific commands
3517,135567
@node LEGO tagsLEGO tags
3537,136022
@node LEGO customizationsLEGO customizations
3547,136269
@node Coq Proof GeneralCoq Proof General
3579,137188
@node Coq-specific commandsCoq-specific commands
3595,137597
@node Coq-specific variablesCoq-specific variables
3617,138104
@node Editing multiple proofsEditing multiple proofs
3639,138762
@node User-loaded tacticsUser-loaded tactics
3663,139870
@node Holes featureHoles feature
3727,142344
@node Isabelle Proof GeneralIsabelle Proof General
3754,143631
@node Choosing logic and starting isabelleChoosing logic and starting isabelle
3785,144800
@node Isabelle commandsIsabelle commands
3854,147608
@node Isabelle settingsIsabelle settings
3997,151761
@node Isabelle customizationsIsabelle customizations
4011,152343
@node HOL Proof GeneralHOL Proof General
4034,152830
@node Shell Proof GeneralShell Proof General
4076,154652
@node Obtaining and InstallingObtaining and Installing
4112,156111
@node Obtaining Proof GeneralObtaining Proof General
4128,156524
@node Installing Proof General from tarballInstalling Proof General from tarball
4159,157763
@node Installing Proof General from RPM packageInstalling Proof General from RPM package
4184,158595
@node Setting the names of binariesSetting the names of binaries
4199,159003
@node Notes for syssiesNotes for syssies
4227,159943
@node Bugs and EnhancementsBugs and Enhancements
4302,162979
@node References4323,163794
@node History of Proof GeneralHistory of Proof General
4363,164817
@node Old News for 3.0Old News for 3.0
4457,168982
@node Old News for 3.1Old News for 3.1
4527,172676
@node Old News for 3.2Old News for 3.2
4553,173848
@node Old News for 3.3Old News for 3.3
4614,176851
@node Old News for 3.4Old News for 3.4
4633,177748
@node Old News for 3.5Old News for 3.5
4655,178803
@node Old News for 3.6Old News for 3.6
4659,178860
@node Old News for 3.7Old News for 3.7
4664,178960
@node Function IndexFunction Index
4708,180858
@node Variable IndexVariable Index
4712,180934
@node Keystroke IndexKeystroke Index
4716,181014
@node Concept IndexConcept Index
4720,181080

doc/PG-adapting.texi,3772
@node Top155,4689
@node Introduction192,5798
@node Future233,7451
@node Credits269,9047
@node Beginning with a New ProverBeginning with a New Prover
279,9339
@node Overview of adding a new proverOverview of adding a new prover
319,11281
@node Demonstration instance and easy configurationDemonstration instance and easy configuration
396,14587
@node Major modes used by Proof GeneralMajor modes used by Proof General
465,17978
@node Menus and Toolbar and User-level CommandsMenus and Toolbar and User-level Commands
508,19688
@node Settings for generic user-level commandsSettings for generic user-level commands
523,20234
@node Menu configurationMenu configuration
568,21966
@node Toolbar configurationToolbar configuration
592,22883
@node Proof Script SettingsProof Script Settings
651,25120
@node Recognizing commands and commentsRecognizing commands and comments
673,25700
@node Recognizing proofsRecognizing proofs
810,32137
@node Recognizing other elementsRecognizing other elements
919,36812
@node Configuring undo behaviourConfiguring undo behaviour
1045,42344
@node Nested proofsNested proofs
1182,47733
@node Safe (state-preserving) commandsSafe (state-preserving) commands
1222,49359
@node Activate scripting hookActivate scripting hook
1245,50312
@node Automatic multiple filesAutomatic multiple files
1269,51182
@node Completions1291,52029
@node Proof Shell SettingsProof Shell Settings
1332,53519
@node Proof shell commandsProof shell commands
1363,54801
@node Script input to the shellScript input to the shell
1527,61845
@node Settings for matching various output from proof processSettings for matching various output from proof process
1592,64803
@node Settings for matching urgent messages from proof processSettings for matching urgent messages from proof process
1709,69932
@node Hooks and other settingsHooks and other settings
1924,79809
@node Goals Buffer SettingsGoals Buffer Settings
2005,83196
@node Splash Screen SettingsSplash Screen Settings
2082,86302
@node Global ConstantsGlobal Constants
2108,87057
@node Handling Multiple FilesHandling Multiple Files
2134,87898
@node Configuring Editing SyntaxConfiguring Editing Syntax
2286,95681
@node Configuring Font LockConfiguring Font Lock
2343,97798
@node Configuring TokensConfiguring Tokens
2415,101292
@node Writing More Lisp CodeWriting More Lisp Code
2453,102793
@node Default values for generic settingsDefault values for generic settings
2470,103438
@node Adding prover-specific configurationsAdding prover-specific configurations
2500,104521
@node Useful variablesUseful variables
2543,105803
@node Useful functions and macrosUseful functions and macros
2558,106302
@node Internals of Proof GeneralInternals of Proof General
2667,110525
@node Spans2695,111421
@node Proof General site configurationProof General site configuration
2707,111743
@node Configuration variable mechanismsConfiguration variable mechanisms
2787,114788
@node Global variablesGlobal variables
2908,120232
@node Proof script modeProof script mode
2978,122780
@node Proof shell modeProof shell mode
3216,133387
@node Debugging3653,150663
@node Plans and IdeasPlans and Ideas
3696,151539
@node Proof by pointing and similar featuresProof by pointing and similar features
3717,152261
@node Granularity of atomic command sequencesGranularity of atomic command sequences
3755,153919
@node Browser mode for script files and theoriesBrowser mode for script files and theories
3800,156144
@node Demonstration InstantiationsDemonstration Instantiations
3830,157175
@node demoisa-easy.el3846,157606
@node demoisa.el3908,159798
@node Function IndexFunction Index
4062,164738
@node Variable IndexVariable Index
4066,164814
@node Concept IndexConcept Index
4075,164993

generic/proof.el,0

pgshell/pgshell.el,0

isar/isar-autotest.el,0

isar/interface-setup.el,0

hol98/hol98.el,0

demoisa/demoisa-easy.el,0

coq/coq-mmm.el,0

coq/coq-autotest.el,0

ccc/ccc.el,0

acl2/acl2.el,0