5 LICENSE: BSD 3-clause (Isabelle) |
5 LICENSE: BSD 3-clause (Isabelle) |
6 |
6 |
7 Quasi-abstract markup elements. |
7 Quasi-abstract markup elements. |
8 -} |
8 -} |
9 |
9 |
10 module Isabelle.Markup (T, empty, is_empty, Output, no_output) |
10 module Isabelle.Markup ( |
|
11 T, empty, is_empty, properties, |
|
12 |
|
13 nameN, name, xnameN, xname, kindN, |
|
14 |
|
15 lineN, end_lineN, offsetN, end_offsetN, fileN, idN, positionN, position, |
|
16 |
|
17 wordsN, words, no_wordsN, no_words, |
|
18 |
|
19 tfreeN, tfree, tvarN, tvar, freeN, free, skolemN, skolem, boundN, bound, varN, var, |
|
20 numeralN, numeral, literalN, literal, delimiterN, delimiter, inner_stringN, inner_string, |
|
21 inner_cartoucheN, inner_cartouche, inner_commentN, inner_comment, |
|
22 token_rangeN, token_range, |
|
23 sortingN, sorting, typingN, typing, class_parameterN, class_parameter, |
|
24 |
|
25 antiquotedN, antiquoted, antiquoteN, antiquote, |
|
26 |
|
27 paragraphN, paragraph, text_foldN, text_fold, |
|
28 |
|
29 keyword1N, keyword1, keyword2N, keyword2, keyword3N, keyword3, quasi_keywordN, quasi_keyword, |
|
30 improperN, improper, operatorN, operator, stringN, string, alt_stringN, alt_string, |
|
31 verbatimN, verbatim, cartoucheN, cartouche, commentN, comment, |
|
32 |
|
33 writelnN, writeln, stateN, state, informationN, information, tracingN, tracing, |
|
34 warningN, warning, legacyN, legacy, errorN, error, reportN, report, no_reportN, no_report, |
|
35 |
|
36 intensifyN, intensify, |
|
37 Output, no_output) |
11 where |
38 where |
12 |
39 |
|
40 import Prelude hiding (words, error) |
|
41 |
|
42 import Isabelle.Library |
13 import qualified Isabelle.Properties as Properties |
43 import qualified Isabelle.Properties as Properties |
14 |
44 |
|
45 |
|
46 {- basic markup -} |
15 |
47 |
16 type T = (String, Properties.T) |
48 type T = (String, Properties.T) |
17 |
49 |
18 empty :: T |
50 empty :: T |
19 empty = ("", []) |
51 empty = ("", []) |
20 |
52 |
21 is_empty :: T -> Bool |
53 is_empty :: T -> Bool |
22 is_empty ("", _) = True |
54 is_empty ("", _) = True |
23 is_empty _ = False |
55 is_empty _ = False |
24 |
56 |
|
57 properties :: Properties.T -> T -> T |
|
58 properties more_props (elem, props) = |
|
59 (elem, fold_rev Properties.put more_props props) |
|
60 |
|
61 markup_elem name = (name, (name, []) :: T) |
|
62 |
|
63 |
|
64 {- misc properties -} |
|
65 |
|
66 nameN :: String |
|
67 nameN = "name" |
|
68 |
|
69 name :: String -> T -> T |
|
70 name a = properties [(nameN, a)] |
|
71 |
|
72 xnameN :: String |
|
73 xnameN = "xname" |
|
74 |
|
75 xname :: String -> T -> T |
|
76 xname a = properties [(xnameN, a)] |
|
77 |
|
78 kindN :: String |
|
79 kindN = "kind" |
|
80 |
|
81 |
|
82 {- position -} |
|
83 |
|
84 lineN, end_lineN :: String |
|
85 lineN = "line" |
|
86 end_lineN = "end_line" |
|
87 |
|
88 offsetN, end_offsetN :: String |
|
89 offsetN = "offset" |
|
90 end_offsetN = "end_offset" |
|
91 |
|
92 fileN, idN :: String |
|
93 fileN = "file" |
|
94 idN = "id" |
|
95 |
|
96 positionN :: String; position :: T |
|
97 (positionN, position) = markup_elem "position" |
|
98 |
|
99 |
|
100 {- text properties -} |
|
101 |
|
102 wordsN :: String; words :: T |
|
103 (wordsN, words) = markup_elem "words" |
|
104 |
|
105 no_wordsN :: String; no_words :: T |
|
106 (no_wordsN, no_words) = markup_elem "no_words" |
|
107 |
|
108 |
|
109 {- inner syntax -} |
|
110 |
|
111 tfreeN :: String; tfree :: T |
|
112 (tfreeN, tfree) = markup_elem "tfree" |
|
113 |
|
114 tvarN :: String; tvar :: T |
|
115 (tvarN, tvar) = markup_elem "tvar" |
|
116 |
|
117 freeN :: String; free :: T |
|
118 (freeN, free) = markup_elem "free" |
|
119 |
|
120 skolemN :: String; skolem :: T |
|
121 (skolemN, skolem) = markup_elem "skolem" |
|
122 |
|
123 boundN :: String; bound :: T |
|
124 (boundN, bound) = markup_elem "bound" |
|
125 |
|
126 varN :: String; var :: T |
|
127 (varN, var) = markup_elem "var" |
|
128 |
|
129 numeralN :: String; numeral :: T |
|
130 (numeralN, numeral) = markup_elem "numeral" |
|
131 |
|
132 literalN :: String; literal :: T |
|
133 (literalN, literal) = markup_elem "literal" |
|
134 |
|
135 delimiterN :: String; delimiter :: T |
|
136 (delimiterN, delimiter) = markup_elem "delimiter" |
|
137 |
|
138 inner_stringN :: String; inner_string :: T |
|
139 (inner_stringN, inner_string) = markup_elem "inner_string" |
|
140 |
|
141 inner_cartoucheN :: String; inner_cartouche :: T |
|
142 (inner_cartoucheN, inner_cartouche) = markup_elem "inner_cartouche" |
|
143 |
|
144 inner_commentN :: String; inner_comment :: T |
|
145 (inner_commentN, inner_comment) = markup_elem "inner_comment" |
|
146 |
|
147 |
|
148 token_rangeN :: String; token_range :: T |
|
149 (token_rangeN, token_range) = markup_elem "token_range" |
|
150 |
|
151 |
|
152 sortingN :: String; sorting :: T |
|
153 (sortingN, sorting) = markup_elem "sorting" |
|
154 |
|
155 typingN :: String; typing :: T |
|
156 (typingN, typing) = markup_elem "typing" |
|
157 |
|
158 class_parameterN :: String; class_parameter :: T |
|
159 (class_parameterN, class_parameter) = markup_elem "class_parameter" |
|
160 |
|
161 |
|
162 {- antiquotations -} |
|
163 |
|
164 antiquotedN :: String; antiquoted :: T |
|
165 (antiquotedN, antiquoted) = markup_elem "antiquoted" |
|
166 |
|
167 antiquoteN :: String; antiquote :: T |
|
168 (antiquoteN, antiquote) = markup_elem "antiquote" |
|
169 |
|
170 |
|
171 {- text structure -} |
|
172 |
|
173 paragraphN :: String; paragraph :: T |
|
174 (paragraphN, paragraph) = markup_elem "paragraph" |
|
175 |
|
176 text_foldN :: String; text_fold :: T |
|
177 (text_foldN, text_fold) = markup_elem "text_fold" |
|
178 |
|
179 |
|
180 {- outer syntax -} |
|
181 |
|
182 keyword1N :: String; keyword1 :: T |
|
183 (keyword1N, keyword1) = markup_elem "keyword1" |
|
184 |
|
185 keyword2N :: String; keyword2 :: T |
|
186 (keyword2N, keyword2) = markup_elem "keyword2" |
|
187 |
|
188 keyword3N :: String; keyword3 :: T |
|
189 (keyword3N, keyword3) = markup_elem "keyword3" |
|
190 |
|
191 quasi_keywordN :: String; quasi_keyword :: T |
|
192 (quasi_keywordN, quasi_keyword) = markup_elem "quasi_keyword" |
|
193 |
|
194 improperN :: String; improper :: T |
|
195 (improperN, improper) = markup_elem "improper" |
|
196 |
|
197 operatorN :: String; operator :: T |
|
198 (operatorN, operator) = markup_elem "operator" |
|
199 |
|
200 stringN :: String; string :: T |
|
201 (stringN, string) = markup_elem "string" |
|
202 |
|
203 alt_stringN :: String; alt_string :: T |
|
204 (alt_stringN, alt_string) = markup_elem "alt_string" |
|
205 |
|
206 verbatimN :: String; verbatim :: T |
|
207 (verbatimN, verbatim) = markup_elem "verbatim" |
|
208 |
|
209 cartoucheN :: String; cartouche :: T |
|
210 (cartoucheN, cartouche) = markup_elem "cartouche" |
|
211 |
|
212 commentN :: String; comment :: T |
|
213 (commentN, comment) = markup_elem "comment" |
|
214 |
|
215 |
|
216 {- messages -} |
|
217 |
|
218 writelnN :: String; writeln :: T |
|
219 (writelnN, writeln) = markup_elem "writeln" |
|
220 |
|
221 stateN :: String; state :: T |
|
222 (stateN, state) = markup_elem "state" |
|
223 |
|
224 informationN :: String; information :: T |
|
225 (informationN, information) = markup_elem "information" |
|
226 |
|
227 tracingN :: String; tracing :: T |
|
228 (tracingN, tracing) = markup_elem "tracing" |
|
229 |
|
230 warningN :: String; warning :: T |
|
231 (warningN, warning) = markup_elem "warning" |
|
232 |
|
233 legacyN :: String; legacy :: T |
|
234 (legacyN, legacy) = markup_elem "legacy" |
|
235 |
|
236 errorN :: String; error :: T |
|
237 (errorN, error) = markup_elem "error" |
|
238 |
|
239 reportN :: String; report :: T |
|
240 (reportN, report) = markup_elem "report" |
|
241 |
|
242 no_reportN :: String; no_report :: T |
|
243 (no_reportN, no_report) = markup_elem "no_report" |
|
244 |
|
245 intensifyN :: String; intensify :: T |
|
246 (intensifyN, intensify) = markup_elem "intensify" |
|
247 |
|
248 |
|
249 {- output -} |
25 |
250 |
26 type Output = (String, String) |
251 type Output = (String, String) |
27 |
252 |
28 no_output :: Output |
253 no_output :: Output |
29 no_output = ("", "") |
254 no_output = ("", "") |