diff options
| author |  Makarius Wenzel <makarius@sketis.net> | 2000-09-17 11:46:48 +0000 |
|---|---|---|
| committer | Makarius Wenzel <makarius@sketis.net> | 2000-09-17 11:46:48 +0000 |
| commit | b944e4466c922c9b2145a4513bc4b03b1ef205f5 (patch) | |
| tree | 26ae05da536c2074a73bda9205dac5d5289cc7ae /isar | |
| parent | 63738d9de55c0ba5f62ddcaec1fab5707981d7d9 (diff) | |
removed proof-shell-pre-sync-init-cmd (init now handled by -PI options
in isabelle-command-line);
tuned comments;
Diffstat (limited to 'isar')
| -rw-r--r-- | isar/isar.el | 18 |
1 files changed, 7 insertions, 11 deletions
diff --git a/isar/isar.el b/isar/isar.el index 5013e054..13822fd1 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -2,7 +2,7 @@ ;; Copyright (C) 1994-1998 LFCS Edinburgh. ;; ;; Author: David Aspinall <da@dcs.ed.ac.uk> -;; Author / maintainer: Markus Wenzel <wenzelm@in.tum.de> +;; Author / Maintainer: Markus Wenzel <wenzelm@in.tum.de> ;; ;; $Id$ ;; @@ -91,7 +91,7 @@ proof-assistant-home-page isabelle-web-page proof-mode-for-script 'isar-mode ;; proof script syntax - proof-terminal-char ?\; ; forcibly ends a proof command + proof-terminal-char ?\; ; forcibly ends a command proof-script-command-start-regexp (proof-regexp-alt isar-any-command-regexp (regexp-quote ";")) @@ -101,6 +101,7 @@ proof-comment-end-regexp isar-comment-end-regexp proof-string-start-regexp isar-string-start-regexp proof-string-end-regexp isar-string-end-regexp + ;; Next few used for func-menu and recognizing goal..save regions in ;; script buffer. proof-save-command-regexp isar-save-command-regexp @@ -181,10 +182,6 @@ proof-shell-end-goals-regexp "\367" proof-shell-goal-char ?\370 - ;; initial command configures Isabelle/Isar by modifying print - ;; functions, restoring settings saved by Proof General, etc. - proof-shell-pre-sync-init-cmd (isabelle-verbatim - "ProofGeneral.init true;") proof-assistant-setting-format 'isar-markup-ml proof-shell-init-cmd (proof-assistant-settings-cmd) proof-shell-restart-cmd "ProofGeneral.restart" @@ -251,7 +248,6 @@ proof-shell-retract-files-regexp." (defun isar-activate-scripting () "Make sure the Isabelle/Isar toplevel is in a sane state.") -;FIXME (proof-shell-invisible-command proof-shell-restart-cmd)) ;; @@ -517,12 +513,12 @@ proof-shell-retract-files-regexp." (setq font-lock-keywords isar-goals-font-lock-keywords) (proof-goals-config-done)) -;; ================================================================= + ;; -;; x-symbol support for Isabelle PG, provided by David von Oheimb. +;; x-symbol support ;; -;; The following settings configure the generic PG package. -;; The token language "Isabelle Symbols" is in file x-symbol-isabelle.el +;; The following settings configure the generic PG package; the main +;; part is in isa/x-symbol-isabelle.el ;; (setq |