Many compatibility updates, bug fixes, rearrangements for compilation.

2 files changed, 14 insertions, 26 deletions

diff --git a/demoisa/demoisa-easy.el b/demoisa/demoisa-easy.el
index c9d1869f..f5957f2d 100644
--- a/demoisa/demoisa-easy.el
+++ b/demoisa/demoisa-easy.el
@@ -1,6 +1,6 @@
-;; demoisa-easy.el Example Proof General instance for Isabelle
+;; demoisa-easy.el --- Example Proof General instance for Isabelle
 ;;
-;; Copyright (C) 1999 LFCS Edinburgh. 
+;; Copyright (C) 1999 LFCS Edinburgh.
 ;;
 ;; Author: David Aspinall <David.Aspinall@ed.ac.uk>
 ;;
@@ -12,10 +12,10 @@
 ;; This mechanism is recommended for new instantiations of
 ;; Proof General since it follows a regular pattern, and we can more
 ;; easily adapt it in the future to new versions of Proof General
-;; using alternative architectures. It is still easy to augment 
+;; using alternative architectures. It is still easy to augment
 ;; with additional elisp functions and other settings.
 ;;
-;; The most important setting is `proof-shell-annotated-prompt-regexp' 
+;; The most important setting is `proof-shell-annotated-prompt-regexp'
 ;; used to recognize prompt texts from the prover.
 ;;
 ;; See demoisa.el and the Adapting Proof General manual for more
@@ -25,10 +25,15 @@
 ;; To test this file you must rename it demoisa.el.
 ;;
 
+(eval-when-compile
+  (require 'proof-site)			; compilation for demoisa
+  (proof-ready-for-assistant 'demoisa))
+
+(require 'proof)
 (require 'proof-easy-config)            ; easy configure mechanism
 
-(proof-easy-config 
- 'demoisa "Isabelle Demo" 
+(proof-easy-config
+ 'demoisa "Isabelle Demo"
  proof-prog-name		 "isabelle"
  proof-terminal-char             ?\;
  proof-script-comment-start             "(*"
@@ -58,3 +63,5 @@
  proof-shell-eager-annotation-start "^\\[opening \\|^###\\|^Reading")
 
 (provide 'demoisa)
+
+;;; demoisa-easy.el ends here
diff --git a/demoisa/demoisa.el b/demoisa/demoisa.el
index f9b75845..ed3aa8e1 100644
--- a/demoisa/demoisa.el
+++ b/demoisa/demoisa.el
@@ -84,6 +84,7 @@
    proof-save-command		"qed \"%s\";"
    proof-kill-goal-command	"Goal \"PROP no_goal_set\";"
    proof-assistant-home-page	isabelledemo-web-page
+   proof-prog-name		isabelledemo-prog-name
    proof-auto-multiple-files    t))
 
 
@@ -110,9 +111,6 @@
 ;; ======== Defining the derived modes ========
 ;;
 
-;; The name of the script mode is always <proofsym>-script,
-;; but the others can be whatever you like.
-;;
 ;; The derived modes set the variables, then call the
 ;; <mode>-config-done function to complete configuration.
 
@@ -134,25 +132,8 @@
   "Isabelle Demo goals" nil
   (proof-goals-config-done))
 
-;; The response buffer and goals buffer modes defined above are
-;; trivial.  In fact, we don't need to define them at all -- they
-;; would simply default to "proof-response-mode" and "pg-goals-mode".
-
 ;; A more sophisticated instantiation might set font-lock-keywords to
 ;; add highlighting, or some of the proof by pointing markup
 ;; configuration for the goals buffer.
 
-;; The final piece of magic here is a hook which configures settings
-;; to get the proof shell running.  Proof General needs to know the
-;; name of the program to run, and the modes for the shell, response,
-;; and goals buffers.
-
-(add-hook 'proof-pre-shell-start-hook 'demoisa-pre-shell-start)
-
-(defun demoisa-pre-shell-start ()
-  (setq proof-prog-name		isabelledemo-prog-name)
-  (setq proof-mode-for-shell    'demoisa-shell-mode)
-  (setq proof-mode-for-response 'demoisa-response-mode)
-  (setq proof-mode-for-goals	'demoisa-goals-mode))
-
 (provide 'demoisa)