diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2010-08-24 19:09:36 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2010-08-24 19:09:36 +0000 |
| commit | b0e087829c9089a3ba5a64a4fedaf756cf274178 (patch) | |
| tree | 2995ef668094f3023a3d20dee620310141258713 /isar | |
| parent | 582a46965f00ed0777c0a8d30c47cdca92fdddf8 (diff) | |
Tidy comments
Diffstat (limited to 'isar')
| -rw-r--r-- | isar/isar.el | 21 |
1 files changed, 10 insertions, 11 deletions
diff --git a/isar/isar.el b/isar/isar.el index bf922e57..91bc652d 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -11,7 +11,6 @@ ;; ;; Contributors: David von Oheimb, Sebastian Skalberg ;; -;; ;; $Id$ ;; @@ -209,12 +208,10 @@ See -k option for Isabelle interface script." "\^AIProof General, you can unlock the file \"\\(.*\\)\"\^AJ" proof-shell-process-file (cons - ;; Theory loader output "\^AIProof General, this file is loaded: \"\\(.*\\)\"\^AJ" (lambda () (match-string 1))) - proof-shell-match-pgip-cmd "\^AI<pgip" - ;; configuration for these + proof-shell-match-pgip-cmd "\^AI<pgip" proof-shell-issue-pgip-cmd 'isabelle-process-pgip proof-shell-theorem-dependency-list-split "\" \"" @@ -227,10 +224,13 @@ See -k option for Isabelle interface script." "ProofGeneral.inform_file_retracted \"%s\"")) -;;; -;;; Settings for the interface -;;; (Settings for Isabelle are configured automatically via PGIP message) -;;; +;; +;; Settings for the interface +;; +;; Note: settings for Isabelle are configured automatically via PGIP messages, +;; see `pg-pgip-process-hasprefs' in pg-pgip.el and +;; `proof-assistant-settings-cmds' in proof-menu.el. +;; (defun isar-set-proof-find-theorems-command () (setq proof-find-theorems-command @@ -293,7 +293,7 @@ This is called when Proof General spots output matching ;; -;; Define the derived modes +;; Define the derived modes ;; ;; use eval-and-compile to define vars for byte comp. @@ -325,8 +325,7 @@ This is called when Proof General spots output matching ;; ;; Help menu ;; - -;;; NB: definvisible must be after derived modes (uses isar-mode-map) +;; NB: definvisible must be after derived modes (uses isar-mode-map) (proof-definvisible isar-help-antiquotations "print_antiquotations" "hA") (proof-definvisible isar-help-attributes "print_attributes" "ha") |