blob: 2cba6435b242f157794da72aa7e1e5d5f19c4a2a (
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
|
;; isa-syntax.el Syntax expressions for Isabelle
;;
(require 'proof-syntax)
;; ----- keywords for font-lock.
(defvar isa-keywords-decl
'(
))
(defvar isa-keywords-defn
'(
"bind_thm"
))
(defvar isa-keywords-goal
'(
"goal"
))
(defvar isa-keywords-save
'(
"qed"
))
(defvar isa-keywords-kill-goal '(
))
(defvar isa-keywords-commands
'(
"by"
"goal"
))
;; See isa-command-table in Isamode/isa-menus.el to get this list.
(defvar isa-tactics
'(
"resolve_tac" "assume_tac"
))
(defvar isa-keywords
(append isa-keywords-goal isa-keywords-save isa-keywords-decl
isa-keywords-defn isa-keywords-commands isa-tactics)
"All keywords in a Isa script")
(defvar isa-tacticals '(
"REPEAT" "THEN" "ORELSE" "TRY"
))
;; ----- regular expressions
;; this should come from isa-ml-compiler stuff.
(defvar isa-error-regexp
"^.*Error:"
"A regular expression indicating that the Isa process has identified
an error.")
(defvar isa-id proof-id)
(defvar 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 (isa-abstr-regexp "\\[" ":") 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.")
;; According to Isa, "Definition" is both a declaration and a goal.
;; It is understood here as being a goal. This is important for
;; recognizing global identifiers, see isa-global-p.
(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)
|
