1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
|
;; demoisa.el Example Proof General instance for Isabelle
;;
;; Copyright (C) 1999 LFCS Edinburgh.
;;
;; Author: David Aspinall <David.Aspinall@ed.ac.uk>
;;
;; demoisa.el,v 8.0 2004/04/17 23:39:58 da Exp
;;
;; =================================================================
;;
;; See README in this directory for an introduction.
;;
;; NEW INSTANCES: please use demoisa-easy.el as a basis instead.
;;
;; 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-script-comment-start "(*"
proof-script-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 "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)
|
