aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2000-09-13 15:47:09 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2000-09-13 15:47:09 +0000
commit8e39eeed71729920b48e061ebba6f9fc754b158e (patch)
treee9d249fb3c1e6504f632df76514a63059430ef37 /doc
parent1f71b01d4482c18f42118e85bd64b2ee8c89dd96 (diff)
Remove keystroke index, add appendix with demoisa code (directly included)
Diffstat (limited to 'doc')
-rw-r--r--doc/PG-adapting.texi261
1 files changed, 258 insertions, 3 deletions
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index 82dfa3b3..34605081 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -173,6 +173,7 @@ Proof General.
* Writing more lisp code::
* Internals of Proof General::
* Plans and ideas::
+* Demonstration Instantiations::
* Function Index::
* Variable Index::
* Keystroke Index::
@@ -3064,6 +3065,259 @@ particular constants, etc.
+
+@c
+@c
+@c APPENDIX: Demonstration instantiation for Isabelle
+@c
+@c
+@node Demonstration Instantiations
+@appendix Demonstration Instantiations
+
+This appendix contains the code for the two demonstration
+instantiations of Proof General, for Isabelle.
+
+These instantiations make an almost-bare minimum of settings to get
+things working. To add embellishments, you should refer to
+the instantiations for other systems distributed with
+Proof General.
+
+@menu
+* demoisa-easy.el::
+* demoisa.el::
+@end menu
+
+@node demoisa-easy.el
+@section demoisa-easy.el
+
+@lisp
+@c FIXME: MAGIC NEEDED TO INCLUDE FILE VERBATIM
+@c @includeverbatim ../demoisa/demoisa-easy.el
+;; demoisa-easy.el Example Proof General instance for Isabelle
+;;
+;; Copyright (C) 1999 LFCS Edinburgh.
+;;
+;; Author: David Aspinall <da@@dcs.ed.ac.uk>
+;;
+;; $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.
+;;
+;; See demoisa.el and the 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)
+@end lisp
+
+@node demoisa.el
+@section demoisa.el
+
+@lisp
+@c FIXME: MAGIC NEEDED TO INCLUDE FILE VERBATIM
+@c @includeverbatim ../demoisa/demoisa-easy.el
+;; demoisa.el Example Proof General instance for Isabelle
+;;
+;; Copyright (C) 1999 LFCS Edinburgh.
+;;
+;; Author: David Aspinall <da@@dcs.ed.ac.uk>
+;;
+;; $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)
+@end lisp
+
+
+
+
@node Function Index
@unnumbered Function and Command Index
@printindex fn
@@ -3072,9 +3326,10 @@ particular constants, etc.
@unnumbered Variable and User Option Index
@printindex vr
-@node Keystroke Index
-@unnumbered Keystroke Index
-@printindex ky
+@c Nothing in this one!
+@c @node Keystroke Index
+@c @unnumbered Keystroke Index
+@c @printindex ky
@node Concept Index
@unnumbered Concept Index