diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2000-09-13 15:47:09 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2000-09-13 15:47:09 +0000 |
commit | 8e39eeed71729920b48e061ebba6f9fc754b158e (patch) | |
tree | e9d249fb3c1e6504f632df76514a63059430ef37 /doc | |
parent | 1f71b01d4482c18f42118e85bd64b2ee8c89dd96 (diff) |
Remove keystroke index, add appendix with demoisa code (directly included)
Diffstat (limited to 'doc')
-rw-r--r-- | doc/PG-adapting.texi | 261 |
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 |