1 (* Title: Pure/Thy/thy_syntax.ML |
1 (* Title: Pure/Thy/thy_syntax.ML |
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 Superficial theory syntax: tokens and spans. |
4 Theory syntax elements. |
5 *) |
5 *) |
6 |
6 |
7 signature THY_SYNTAX = |
7 signature THY_SYNTAX = |
8 sig |
8 sig |
9 val reports_of_tokens: Keyword.keywords -> Token.T list -> bool * Position.report_text list |
|
10 val present_token: Keyword.keywords -> Token.T -> Output.output |
|
11 val present_span: Keyword.keywords -> Command_Span.span -> Output.output |
|
12 datatype 'a element = Element of 'a * ('a element list * 'a) option |
9 datatype 'a element = Element of 'a * ('a element list * 'a) option |
13 val atom: 'a -> 'a element |
10 val atom: 'a -> 'a element |
14 val map_element: ('a -> 'b) -> 'a element -> 'b element |
11 val map_element: ('a -> 'b) -> 'a element -> 'b element |
15 val flat_element: 'a element -> 'a list |
12 val flat_element: 'a element -> 'a list |
16 val last_element: 'a element -> 'a |
13 val last_element: 'a element -> 'a |
18 end; |
15 end; |
19 |
16 |
20 structure Thy_Syntax: THY_SYNTAX = |
17 structure Thy_Syntax: THY_SYNTAX = |
21 struct |
18 struct |
22 |
19 |
23 (** presentation **) |
20 (* datatype element: command with optional proof *) |
24 |
|
25 local |
|
26 |
|
27 fun reports_of_token keywords tok = |
|
28 let |
|
29 val malformed_symbols = |
|
30 Input.source_explode (Token.input_of tok) |
|
31 |> map_filter (fn (sym, pos) => |
|
32 if Symbol.is_malformed sym |
|
33 then SOME ((pos, Markup.bad), "Malformed symbolic character") else NONE); |
|
34 val is_malformed = Token.is_error tok orelse not (null malformed_symbols); |
|
35 val reports = Token.reports keywords tok @ Token.completion_report tok @ malformed_symbols; |
|
36 in (is_malformed, reports) end; |
|
37 |
|
38 in |
|
39 |
|
40 fun reports_of_tokens keywords toks = |
|
41 let val results = map (reports_of_token keywords) toks |
|
42 in (exists fst results, maps snd results) end; |
|
43 |
|
44 end; |
|
45 |
|
46 fun present_token keywords tok = |
|
47 fold_rev Markup.enclose (Token.markups keywords tok) (Output.output (Token.unparse tok)); |
|
48 |
|
49 fun present_span keywords = implode o map (present_token keywords) o Command_Span.content; |
|
50 |
|
51 |
|
52 |
|
53 (** specification elements: commands with optional proof **) |
|
54 |
21 |
55 datatype 'a element = Element of 'a * ('a element list * 'a) option; |
22 datatype 'a element = Element of 'a * ('a element list * 'a) option; |
56 |
23 |
57 fun element (a, b) = Element (a, SOME b); |
24 fun element (a, b) = Element (a, SOME b); |
58 fun atom a = Element (a, NONE); |
25 fun atom a = Element (a, NONE); |