diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-05-11 14:37:59 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-05-11 14:37:59 +0000 |
| commit | 9e5aacb5d93701aa7373cd7f34d78bf8925fbd6a (patch) | |
| tree | 16f073f4d6e54c1738915ef7b495ce15edef7447 /isar/isar.el | |
| parent | c68ca4aa6cf07f863ce133dcf69444f8e8196064 (diff) | |
Load isabelle-system file shared with Isabelle Proof General.
Add default settings to proof-shell-init-cmd.
Add Isabelle menu to menubar.
Diffstat (limited to 'isar/isar.el')
| -rw-r--r-- | isar/isar.el | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/isar/isar.el b/isar/isar.el index 4fd72083..ca37f6fd 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -22,10 +22,14 @@ (setq auto-mode-alist (cons '("\\.thy$" . isar-mode) auto-mode-alist)) - (require 'proof) (require 'isar-syntax) +;; Add generic code for Isabelle and Isabelle/Isar +(setq load-path (cons (concat proof-home-directory "isa/") load-path)) +(require 'isabelle-system) + + ;; To make byte compiler be quiet. ;; NASTY: these result in loads when evaluated ;; ordinarily (from non-byte compiled code). @@ -65,12 +69,6 @@ :type 'number :group 'isabelle-isar) -(defcustom isabelle-web-page - "http://isabelle.in.tum.de" - "URL of web page for Isabelle." - :type 'string - :group 'isabelle-isar) - ;;; ;;; ======== Configuration of generic modes ======== @@ -195,6 +193,7 @@ (setq proof-assistant-home-page isabelle-web-page proof-mode-for-script 'isar-proofscript-mode + proof-assistant-menu-entries isabelle-menu-entries ;; proof script syntax proof-terminal-char ?\; ; ends a proof proof-comment-start "(*" ; comment in a proof @@ -275,7 +274,9 @@ proof-shell-end-goals-regexp "\367" proof-shell-goal-char ?\370 ;; initial command configures Isabelle/Isar by modifying print functions etc. - proof-shell-init-cmd (isar-verbatim "ProofGeneral.init true;") + proof-shell-init-cmd (concat + (isar-verbatim "ProofGeneral.init true;") + (isabelle-set-default-cmd)) proof-shell-restart-cmd "ProofGeneral.restart;" proof-shell-quit-cmd (isar-verbatim "quit();") |