aboutsummaryrefslogtreecommitdiffhomepage
path: root/demoisa
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2001-09-03 12:11:59 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2001-09-03 12:11:59 +0000
commitb7209db785ccd5e68ecc144f628cf7593a215ede (patch)
treed74caf158d93370c57368f40cdf16965d5d6894f /demoisa
parent53a6404d7394d16783bfc7fb9652993b426938fb (diff)
Updating branch
Diffstat (limited to 'demoisa')
-rw-r--r--demoisa/demoisa.el205
1 files changed, 55 insertions, 150 deletions
diff --git a/demoisa/demoisa.el b/demoisa/demoisa.el
index 1740a100..8b1c76d8 100644
--- a/demoisa/demoisa.el
+++ b/demoisa/demoisa.el
@@ -1,4 +1,4 @@
-;; demoisa.el Example Proof General instance for Isabelle
+;; demoisa-easy.el Example Proof General instance for Isabelle
;;
;; Copyright (C) 1999 LFCS Edinburgh.
;;
@@ -6,152 +6,57 @@
;;
;; $Id$
;;
-;; =================================================================
-;;
-;; 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)
+;; 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