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
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
|
;; twelf.el Proof General instance for Twelf
;;
;; Copyright (C) 2000 LFCS Edinburgh.
;;
;; Author: David Aspinall <da@dcs.ed.ac.uk>
;;
;; $Id$
;;
;;
;; FIXME: PG needs a bit of tuning to get this to work
;; properly, because of mixed syntax for comments.
;; We should introduce a proof-parse-to-next-command
;; configurable setting, perhaps, which should skip
;; comments automatically.
(require 'proof-easy-config) ; easy configure mechanism
(require 'twelf-font) ; font lock configuration
;; (require 'twelf-old) ; port of parts of old code
;; FIXME: put parts of old code into twelf-syntax or similar
(proof-easy-config
'twelf "Twelf"
proof-prog-name "twelf-server"
proof-assistant-home-page "http://www.cs.cmu.edu/~twelf/"
proof-terminal-char ?\.
proof-shell-auto-terminate-commands nil ; server commands don't end with .
;; FIXME: must also cope with single line comments beginning with %
proof-comment-start "%{\\|^%"
proof-comment-end "}%\\|^%.*\n"
proof-comment-start-regexp "%[%{\t\n\f]"
proof-comment-end ""
;; FIXME: these don't apply?
proof-goal-command-regexp "^%theorem"
proof-save-command-regexp "" ;; FIXME: empty?
proof-goal-with-hole-regexp "^%theorem\w-+\\(.*\\)\w-+:"
proof-save-with-hole-regexp "" ;; FIXME
;; proof-non-undoables-regexp "undo\\|back"
proof-goal-command "%theorem %s."
proof-save-command "%prove "
;; 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 "OS.chDir %s"
proof-shell-prompt-pattern "%% OK %%\n"
proof-shell-interrupt-regexp "interrupt"
;; proof-shell-start-goals-regexp "Level [0-9]"
;; proof-shell-end-goals-regexp "val it"
proof-shell-annotated-prompt-regexp "%% [OA][KB]O?R?T? %%\n"
proof-shell-error-regexp "Server error:"
proof-shell-quit-cmd "quit"
proof-shell-restart-cmd "reset"
;; unset
;; 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")
)
;;
;; Syntax table
;;
;; Taken from old Emacs mode, renamed fns to be convention compliant
(defun twelf-set-syntax (char entry)
(modify-syntax-entry char entry twelf-mode-syntax-table))
(defun twelf-set-word (char) (twelf-set-syntax char "w "))
(defun twelf-set-symbol (char) (twelf-set-syntax char "_ "))
(defun twelf-map-string (func string)
(if (string= "" string)
()
(funcall func (string-to-char string))
(twelf-map-string func (substring string 1))))
;; A-Z and a-z are already word constituents
;; For fontification, it would be better if _ and ' were word constituents
(twelf-map-string
'twelf-set-word "!&$^+/<=>?@~|#*`;,-0123456789\\") ; word constituents
(twelf-map-string 'twelf-set-symbol "_'") ; symbol constituents
;; Delimited comments are %{ }%, see 1234 below.
(twelf-set-syntax ?\ " ") ; whitespace
(twelf-set-syntax ?\t " ") ; whitespace
(twelf-set-syntax ?% "< 14") ; comment begin
(twelf-set-syntax ?\n "> ") ; comment end
(twelf-set-syntax ?: ". ") ; punctuation
(twelf-set-syntax ?. ". ") ; punctuation
(twelf-set-syntax ?\( "() ") ; open delimiter
(twelf-set-syntax ?\) ")( ") ; close delimiter
(twelf-set-syntax ?\[ "(] ") ; open delimiter
(twelf-set-syntax ?\] ")[ ") ; close delimiter
(twelf-set-syntax ?\{ "(}2 ") ; open delimiter
(twelf-set-syntax ?\} "){ 3") ; close delimiter
;; Actually, strings are illegal but we include:
(twelf-set-syntax ?\" "\" ") ; string quote
;; \ is not an escape, but a word constituent (see above)
;;(twelf-set-syntax ?\\ "/ ") ; escape
;;
;; Syntax highlighting (from twelf-old.el, needs work)
;;
;; Automatically highlight Twelf sources using font-lock
;; (FIXME: this is not so good, should work with font-lock properly!)
(require 'twelf-font)
(add-hook 'twelf-mode-hook 'twelf-font-fontify-buffer)
(defun twelf-current-decl ()
"Returns list (START END COMPLETE) for current Twelf declaration.
This should be the declaration or query under or just before
point within the nearest enclosing blank lines.
If declaration ends in `.' then COMPLETE is t, otherwise nil."
(let (par-start par-end complete)
(save-excursion
;; Skip backwards if between declarations
(if (or (eobp) (looking-at (concat "[" *whitespace* "]")))
(skip-chars-backward (concat *whitespace* ".")))
(setq par-end (point))
;; Move forward from beginning of decl until last
;; declaration before par-end is found.
(if (not (bobp)) (backward-paragraph 1))
(setq par-start (point))
(while (and (twelf-end-of-par par-end)
(< (point) par-end))
(setq par-start (point)))
;; Now par-start is at end of preceding declaration or query.
(goto-char par-start)
(skip-twelf-comments-and-whitespace)
(setq par-start (point))
;; Skip to period or consective blank lines
(setq complete (twelf-end-of-par))
(setq par-end (point)))
(list par-start par-end complete)))
(defun twelf-next-decl (filename error-buffer)
"Set point after the identifier of the next declaration.
Return the declared identifier or `nil' if none was found.
FILENAME and ERROR-BUFFER are used if something appears wrong."
(let ((id nil)
end-of-id
beg-of-id)
(skip-twelf-comments-and-whitespace)
(while (and (not id) (not (eobp)))
(setq beg-of-id (point))
(if (zerop (skip-chars-forward *twelf-id-chars*))
;; Not looking at id: skip ahead
(skip-ahead filename (current-line-absolute) "No identifier"
error-buffer)
(setq end-of-id (point))
(skip-twelf-comments-and-whitespace)
(if (not (looking-at ":"))
;; Not looking at valid decl: skip ahead
(skip-ahead filename (current-line-absolute end-of-id) "No colon"
error-buffer)
(goto-char end-of-id)
(setq id (buffer-substring beg-of-id end-of-id))))
(skip-twelf-comments-and-whitespace))
id))
(defconst twelf-syntax-menu
'("Syntax Highlighting"
["Highlight Declaration" twelf-font-fontify-decl t]
["Highlight Buffer" twelf-font-fontify-buffer t]
;;(, (toggle "Immediate Highlighting" 'toggle-twelf-font-immediate
;;'font-lock-mode))
)
"Menu for syntax highlighting in Twelf mode.")
(defpgdefault menu-entries
(cdr twelf-syntax-menu))
(provide 'twelf)
|
