Accidental update; revert to previous

1 files changed, 150 insertions, 55 deletions

diff --git a/demoisa/demoisa.el b/demoisa/demoisa.el
index 8b1c76d8..1740a100 100644
--- a/demoisa/demoisa.el
+++ b/demoisa/demoisa.el
@@ -1,4 +1,4 @@
-;; demoisa-easy.el Example Proof General instance for Isabelle
+;; demoisa.el Example Proof General instance for Isabelle
 ;;
 ;; Copyright (C) 1999 LFCS Edinburgh. 
 ;;
@@ -6,57 +6,152 @@
 ;;
 ;; $Id$
 ;;
-;; This is an alternative version of demoisa.el which uses the
-;; proof-easy-config macro to do the work of declaring derived modes,
-;; etc.  
-;;
-;; This mechanism is in fact 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.
-;; It is easy to augment with additional elisp functions and
-;; other settings.
-;;
-;; See demoisa.el and the Adapting Proof General manual for more
-;; documentation.
-;;
-;; To test this file you must rename it demoisa.el.
-;;
-
-(require 'proof-easy-config)            ; easy configure mechanism
-
-(proof-easy-config 
- 'demoisa "Isabelle Demo" 
- proof-prog-name		 "isabelle"
- proof-terminal-char             ?\;
- proof-comment-start             "(*"
- proof-comment-end               "*)"
- proof-goal-command-regexp       "^Goal"
- proof-save-command-regexp       "^qed"
- proof-goal-with-hole-regexp     "qed_goal \"\\(\\(.*\\)\\)\""
- proof-save-with-hole-regexp     "qed \"\\(\\(.*\\)\\)\""
- proof-non-undoables-regexp      "undo\\|back"
- proof-goal-command              "Goal \"%s\";"
- proof-save-command              "qed \"%s\";"
- proof-kill-goal-command         "Goal \"PROP no_goal_set\";"
- proof-showproof-command         "pr()"
- proof-undo-n-times-cmd          "pg_repeat undo %s;"
- proof-auto-multiple-files       t
- proof-shell-cd-cmd              "cd \"%s\""
- proof-shell-prompt-pattern      "[ML-=#>]+>? "
- proof-shell-interrupt-regexp    "Interrupt"
- proof-shell-start-goals-regexp  "Level [0-9]"
- proof-shell-end-goals-regexp    "val it"
- proof-shell-quit-cmd            "quit();"
- proof-assistant-home-page    
- "http://www.cl.cam.ac.uk/Research/HVG/Isabelle/"
- proof-shell-annotated-prompt-regexp 
- "^\\(val it = () : unit\n\\)?ML>? "
- proof-shell-error-regexp             
- "\\*\\*\\*\\|^.*Error:\\|^uncaught exception \\|^Exception- "
- proof-shell-init-cmd  
- "fun pg_repeat f 0 = () | pg_repeat f n = (f(); pg_repeat f (n-1));"
- proof-shell-proof-completed-regexp "^No subgoals!"
- proof-shell-eager-annotation-start   
- "^\\[opening \\|^###\\|^Reading")
-
-(provide 'demoisa)
\ No newline at end of file
+;; =================================================================
+;;
+;; See README in this directory for an introduction.
+;;
+;; Basic configuration is controlled by one line in `proof-site.el'.
+;; It has this line in proof-assistant-table:
+;;
+;;     (demoisa "Isabelle Demo"	"\\.ML$")
+;;
+;; From this it loads this file "demoisa/demoisa.el" whenever
+;; a .ML file is visited, and sets the mode to `demoisa-mode'
+;; (defined below).  
+;; 
+;; I've called this instance "Isabelle Demo Proof General" just to
+;; avoid confusion with the real "Isabelle Proof General" in case the
+;; demo gets loaded by accident.
+;;
+;; To make the line above take precedence over the real Isabelle mode
+;; later in the table, set PROOFGENERAL_ASSISTANTS=demoisa in the
+;; shell before starting Emacs  (or customize proof-assistants).
+;;
+
+
+(require 'proof)			; load generic parts
+
+
+;; ======== User settings for Isabelle ========
+;;
+;; Defining variables using customize is pretty easy.
+;; You should do it at least for your prover-specific user options.
+;;
+;; proof-site provides us with two customization groups
+;; automatically:  (based on the name of the assistant)
+;;
+;; 'isabelledemo        -  User options for Isabelle Demo Proof General
+;; 'isabelledemo-config -  Configuration of Isabelle Proof General
+;;			   (constants, but may be nice to tweak)
+;;
+;; The first group appears in the menu
+;;   ProofGeneral -> Customize -> Isabelledemo 
+;; The second group appears in the menu:
+;;   ProofGeneral -> Internals -> Isabelledemo config
+;;
+
+(defcustom isabelledemo-prog-name "isabelle"
+  "*Name of program to run Isabelle."
+  :type 'file
+  :group 'isabelledemo)
+
+(defcustom isabelledemo-web-page
+  "http://www.cl.cam.ac.uk/Research/HVG/isabelle.html"
+  "URL of web page for Isabelle."
+  :type 'string
+  :group 'isabelledemo-config)
+
+
+;;
+;; ======== Configuration of generic modes ========
+;;
+
+(defun demoisa-config ()
+  "Configure Proof General scripting for Isabelle."
+  (setq
+   proof-terminal-char		?\;	; ends every command
+   proof-comment-start		"(*"
+   proof-comment-end		"*)"
+   proof-goal-command-regexp    "^Goal"
+   proof-save-command-regexp    "^qed"
+   proof-goal-with-hole-regexp  "qed_goal \"\\(\\(.*\\)\\)\""
+   proof-save-with-hole-regexp  "qed \"\\(\\(.*\\)\\)\""
+   proof-non-undoables-regexp   "undo\\|back"
+   proof-undo-n-times-cmd	"pg_repeat undo %s;"
+   proof-showproof-command	"pr()"
+   proof-goal-command		"Goal \"%s\";"
+   proof-save-command		"qed \"%s\";"
+   proof-kill-goal-command	"Goal \"PROP no_goal_set\";"
+   proof-assistant-home-page	isabelledemo-web-page
+   proof-auto-multiple-files    t))
+
+
+(defun demoisa-shell-config ()
+  "Configure Proof General shell for Isabelle."
+  (setq
+   proof-shell-annotated-prompt-regexp   "^\\(val it = () : unit\n\\)?ML>? "
+   proof-shell-cd-cmd			"cd \"%s\""
+   proof-shell-prompt-pattern		"[ML-=#>]+>? "
+   proof-shell-interrupt-regexp         "Interrupt"
+   proof-shell-error-regexp		"\\*\\*\\*\\|^.*Error:\\|^uncaught exception \\|^Exception- "
+   proof-shell-start-goals-regexp	"Level [0-9]"
+   proof-shell-end-goals-regexp		"val it"
+   proof-shell-proof-completed-regexp   "^No subgoals!"
+   proof-shell-eager-annotation-start   "^\\[opening \\|^###\\|^Reading"
+   proof-shell-init-cmd  ; define a utility function, in a lib somewhere?
+   "fun pg_repeat f 0 = () 
+      | pg_repeat f n = (f(); pg_repeat f (n-1));"
+   proof-shell-quit-cmd			"quit();"))
+
+
+
+;;
+;; ======== 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.
+
+(define-derived-mode demoisa-mode proof-mode
+    "Isabelle Demo script" nil
+    (demoisa-config)
+    (proof-config-done))
+
+(define-derived-mode demoisa-shell-mode proof-shell-mode
+   "Isabelle Demo shell" nil
+   (demoisa-shell-config)
+   (proof-shell-config-done))
+
+(define-derived-mode demoisa-response-mode proof-response-mode
+  "Isabelle Demo response" nil
+  (proof-response-config-done))
+
+(define-derived-mode demoisa-goals-mode proof-goals-mode
+  "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 "pbp-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)