From 9e5aacb5d93701aa7373cd7f34d78bf8925fbd6a Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Thu, 11 May 2000 14:37:59 +0000
Subject: Load isabelle-system file shared with Isabelle Proof General. Add
 default settings to proof-shell-init-cmd. Add Isabelle menu to menubar.

---
 isar/isar.el | 17 +++++++++--------
 1 file 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();")
    
-- 
cgit v1.2.3