blob: 11d75de926122929542c1c023c32416ecd72ccb1 (
plain)
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
|
;; isa-syntax.el Syntax expressions for Isabelle
;;
;; David Aspinall <da@dcs.ed.ac.uk>
;;
;; $Id$
;;
(require 'proof-syntax)
;;; Proof mode customization: how should it work?
;;; Presently we have a bunch of variables in proof.el which are
;;; set from a bunch of similarly named variables in <engine>-syntax.el.
;;;
;;; Seems a bit daft: why not just have the customization in
;;; one place, and settings hardwired in <engine>-syntax.el.
;;;
;;; That way we can see which settings are part of instantiation of
;;; proof.el, and which are part of cusomization for <engine>.
;; ------ customize groups
;(defgroup isa-scripting nil
; "Customization of Isabelle script management"
; :group 'external
; :group 'languages)
;(defgroup isa-syntax nil
; "Customization of Isabelle's syntax recognition"
; :group 'isa-scripting)
;; ----- syntax for font-lock and other features
;; FIXME: this command-keyword orientation isn't good
;; enough for Isabelle, since we can have arbitrary
;; ML code around. One solution is to define a
;; restricted language consisting of the interactive
;; commands. We'd still need regexps below, though.
;; Alternatively: customize this for Marcus Wenzel's
;; proof language.
(defgroup isa-syntax nil
"Customization of Isabelle syntax for proof mode"
:group 'isa-settings)
(defcustom isa-keywords-decl
'("val" "fun" "datatype"
"signature" "structure")
"Isabelle keywords for declarations. Includes ML keywords to fontify ML files."
:group 'isa-syntax
:type '(repeat string))
(defcustom isa-keywords-defn
'("bind_thm")
"Isabelle keywords for definitions"
:group 'isa-syntax
:type '(repeat string))
;; isa-keywords-goal is used to manage undo actions
(defcustom isa-keywords-goal
'("Goal" "Goalw" "goal" "goalw" "goalw_cterm")
"Isabelle commands to begin an interactive proof"
:group 'isa-syntax
:type '(repeat string))
(defcustom isa-keywords-save
'("qed" "result" "uresult" "bind_thm" "store_thm")
"Isabelle commands to extract the proved theorem"
:group 'isa-syntax
:type '(repeat string))
(defcustom isa-keywords-commands
'("by" "byev"
"ba" "br" "be" "bd" "brs" "bes" "bds"
"chop" "choplev" "back" "undo"
"fa" "fr" "fe" "fd" "frs" "fes" "fds"
"bw" "bws" "ren"
;; batch proofs
"prove_goal" "qed_goal" "prove_goalw" "qed_goalw" "prove_goalw_cterm")
"Isabelle command keywords"
:group 'isa-syntax
:type '(repeat string))
;; See isa-command-table in Isamode/isa-menus.el to get this list.
;; BUT: tactics are not commands, so appear inside some expression.
(defconst isa-tactics
'("resolve_tac" "assume_tac"))
;; NB: this means that any adjustments above by customize will
;; only have effect in next session.
(defconst isa-keywords
(append isa-keywords-goal isa-keywords-save isa-keywords-decl
isa-keywords-defn isa-keywords-commands isa-tactics)
"All keywords in a Isabelle script")
(defconst isa-tacticals '("REPEAT" "THEN" "ORELSE" "TRY"))
;; ----- regular expressions
;; this should come from isa-ml-compiler stuff.
(defcustom isa-error-regexp
"^.*Error:\\|^\\*\\*\\*\\|^\\#\\#\\#"
"A regexp indicating that Isabelle has identified an error."
:type 'string
:group 'isa-syntax)
(defconst isa-id proof-id)
(defconst isa-ids (proof-ids isa-id))
(defun isa-abstr-regexp (paren char)
(concat paren "\\s-*\\(" isa-ids "\\)\\s-*" char))
(defvar isa-font-lock-terms
(list
;; lambda binders
(list (concat "\%\\s-*\\(" isa-ids "\\)\\.") 1
'font-lock-declaration-name-face)
;; Pi binders
(list (isa-abstr-regexp "(" ":") 1 'font-lock-declaration-name-face)
;; Kinds
(cons (concat "\\<Prop\\>\\|\\<Set\\>\\|\\<Type\\s-*\\(("
isa-id ")\\)?") 'font-lock-type-face))
"*Font-lock table for Isa terms.")
(defconst isa-save-command-regexp
(concat "^" (ids-to-regexp isa-keywords-save)))
(defconst isa-save-with-hole-regexp
(concat "\\(" (ids-to-regexp isa-keywords-save)
"\\)\\s-+\\(" isa-id "\\)\\s-*\."))
(defconst isa-goal-command-regexp
(concat "^" (ids-to-regexp isa-keywords-goal)))
(defconst isa-goal-with-hole-regexp
(concat "\\(" (ids-to-regexp isa-keywords-goal)
"\\)\\s-+\\(" isa-id "\\)\\s-*:"))
(defconst isa-decl-with-hole-regexp
(concat "\\(" (ids-to-regexp isa-keywords-decl)
"\\)\\s-+\\(" isa-ids "\\)\\s-*:"))
(defconst isa-defn-with-hole-regexp
(concat "\\(" (ids-to-regexp isa-keywords-defn)
"\\)\\s-+\\(" isa-id "\\)\\s-*[:[]"))
(defvar isa-font-lock-keywords-1
(append
isa-font-lock-terms
(list
(cons (ids-to-regexp isa-keywords) 'font-lock-keyword-face)
(cons (ids-to-regexp isa-tacticals) 'font-lock-tacticals-name-face)
(list isa-goal-with-hole-regexp 2 'font-lock-function-name-face)
(list isa-decl-with-hole-regexp 2 'font-lock-declaration-name-face)
(list isa-defn-with-hole-regexp 2 'font-lock-function-name-face)
(list isa-save-with-hole-regexp 2 'font-lock-function-name-face))))
(provide 'isa-syntax)
|
