author | wenzelm |
Wed, 18 Mar 2009 21:55:38 +0100 | |
changeset 30573 | 49899f26fbd1 |
parent 29319 | 592503fd6dad |
child 36950 | 75b8f26f2f07 |
permissions | -rw-r--r-- |
29315
b074c05f00ad
renamed ThyEdit (in thy_edit.ML) to ThySyntax (in thy_syntax.ML);
wenzelm
parents:
28454
diff
changeset
|
1 |
(* Title: Pure/Thy/thy_syntax.ML |
23726 | 2 |
Author: Makarius |
3 |
||
29315
b074c05f00ad
renamed ThyEdit (in thy_edit.ML) to ThySyntax (in thy_syntax.ML);
wenzelm
parents:
28454
diff
changeset
|
4 |
Superficial theory syntax: tokens and spans. |
23726 | 5 |
*) |
6 |
||
29315
b074c05f00ad
renamed ThyEdit (in thy_edit.ML) to ThySyntax (in thy_syntax.ML);
wenzelm
parents:
28454
diff
changeset
|
7 |
signature THY_SYNTAX = |
23726 | 8 |
sig |
27842 | 9 |
val token_source: Scan.lexicon * Scan.lexicon -> Position.T -> (string, 'a) Source.source -> |
30573 | 10 |
(OuterLex.token, (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, 'a) |
27770 | 11 |
Source.source) Source.source) Source.source) Source.source |
27842 | 12 |
val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> OuterLex.token list |
23803 | 13 |
val present_token: OuterLex.token -> output |
27842 | 14 |
val report_token: OuterLex.token -> unit |
15 |
datatype span_kind = Command of string | Ignored | Malformed |
|
16 |
type span |
|
17 |
val span_kind: span -> span_kind |
|
18 |
val span_content: span -> OuterLex.token list |
|
27665 | 19 |
val span_range: span -> Position.range |
27842 | 20 |
val span_source: (OuterLex.token, 'a) Source.source -> |
21 |
(span, (OuterLex.token, 'a) Source.source) Source.source |
|
22 |
val parse_spans: Scan.lexicon * Scan.lexicon -> Position.T -> string -> span list |
|
27665 | 23 |
val present_span: span -> output |
27842 | 24 |
val report_span: span -> unit |
28434 | 25 |
val unit_source: (span, 'a) Source.source -> |
28438
32bb6b4eb390
unit_source: explicit treatment of 'oops' proofs;
wenzelm
parents:
28434
diff
changeset
|
26 |
(span * span list * bool, (span, 'a) Source.source) Source.source |
23726 | 27 |
end; |
28 |
||
29315
b074c05f00ad
renamed ThyEdit (in thy_edit.ML) to ThySyntax (in thy_syntax.ML);
wenzelm
parents:
28454
diff
changeset
|
29 |
structure ThySyntax: THY_SYNTAX = |
23726 | 30 |
struct |
31 |
||
28434 | 32 |
structure K = OuterKeyword; |
23726 | 33 |
structure T = OuterLex; |
34 |
structure P = OuterParse; |
|
35 |
||
36 |
||
23803 | 37 |
(** tokens **) |
38 |
||
39 |
(* parse *) |
|
23726 | 40 |
|
27842 | 41 |
fun token_source lexs pos src = |
42 |
Symbol.source {do_recover = true} src |
|
43 |
|> T.source {do_recover = SOME false} (K lexs) pos; |
|
23726 | 44 |
|
27842 | 45 |
fun parse_tokens lexs pos str = |
46 |
Source.of_string str |
|
47 |
|> token_source lexs pos |
|
48 |
|> Source.exhaust; |
|
23726 | 49 |
|
50 |
||
23803 | 51 |
(* present *) |
23726 | 52 |
|
53 |
local |
|
54 |
||
55 |
val token_kind_markup = |
|
27846 | 56 |
fn T.Command => (Markup.commandN, []) |
57 |
| T.Keyword => (Markup.keywordN, []) |
|
58 |
| T.Ident => Markup.ident |
|
59 |
| T.LongIdent => Markup.ident |
|
60 |
| T.SymIdent => Markup.ident |
|
29319 | 61 |
| T.Var => Markup.var |
62 |
| T.TypeIdent => Markup.tfree |
|
63 |
| T.TypeVar => Markup.tvar |
|
27846 | 64 |
| T.Nat => Markup.ident |
65 |
| T.String => Markup.string |
|
66 |
| T.AltString => Markup.altstring |
|
67 |
| T.Verbatim => Markup.verbatim |
|
68 |
| T.Space => Markup.none |
|
69 |
| T.Comment => Markup.comment |
|
70 |
| T.InternalValue => Markup.none |
|
71 |
| T.Malformed => Markup.malformed |
|
72 |
| T.Error _ => Markup.malformed |
|
73 |
| T.Sync => Markup.control |
|
74 |
| T.EOF => Markup.control; |
|
23726 | 75 |
|
23803 | 76 |
in |
77 |
||
23726 | 78 |
fun present_token tok = |
79 |
Markup.enclose (token_kind_markup (T.kind_of tok)) (Output.output (T.unparse tok)); |
|
80 |
||
27842 | 81 |
fun report_token tok = |
82 |
Position.report (token_kind_markup (T.kind_of tok)) (T.position_of tok); |
|
83 |
||
23803 | 84 |
end; |
85 |
||
86 |
||
87 |
||
27665 | 88 |
(** spans **) |
89 |
||
27842 | 90 |
(* type span *) |
91 |
||
92 |
datatype span_kind = Command of string | Ignored | Malformed; |
|
93 |
datatype span = Span of span_kind * OuterLex.token list; |
|
23803 | 94 |
|
27842 | 95 |
fun span_kind (Span (k, _)) = k; |
96 |
fun span_content (Span (_, toks)) = toks; |
|
97 |
||
98 |
fun span_range span = |
|
99 |
(case span_content span of |
|
100 |
[] => (Position.none, Position.none) |
|
101 |
| toks => |
|
27665 | 102 |
let |
103 |
val start_pos = T.position_of (hd toks); |
|
27756 | 104 |
val end_pos = T.end_position_of (List.last toks); |
27842 | 105 |
in (start_pos, end_pos) end); |
23803 | 106 |
|
107 |
||
108 |
(* parse *) |
|
23726 | 109 |
|
23803 | 110 |
local |
111 |
||
27665 | 112 |
val is_whitespace = T.is_kind T.Space orf T.is_kind T.Comment; |
113 |
||
114 |
val body = Scan.unless (Scan.many is_whitespace -- Scan.ahead (P.command || P.eof)) P.not_eof; |
|
23726 | 115 |
|
27665 | 116 |
val span = |
117 |
Scan.ahead P.command -- P.not_eof -- Scan.repeat body |
|
27842 | 118 |
>> (fn ((name, c), bs) => Span (Command name, c :: bs)) || |
119 |
Scan.many1 is_whitespace >> (fn toks => Span (Ignored, toks)) || |
|
120 |
Scan.repeat1 body >> (fn toks => Span (Malformed, toks)); |
|
23726 | 121 |
|
122 |
in |
|
123 |
||
27842 | 124 |
fun span_source src = Source.source T.stopper (Scan.bulk span) NONE src; |
23803 | 125 |
|
126 |
end; |
|
127 |
||
27842 | 128 |
fun parse_spans lexs pos str = |
129 |
Source.of_string str |
|
130 |
|> token_source lexs pos |
|
131 |
|> span_source |
|
132 |
|> Source.exhaust; |
|
23803 | 133 |
|
134 |
||
135 |
(* present *) |
|
136 |
||
137 |
local |
|
138 |
||
27665 | 139 |
fun kind_markup (Command name) = Markup.command_span name |
140 |
| kind_markup Ignored = Markup.ignored_span |
|
27842 | 141 |
| kind_markup Malformed = Markup.malformed_span; |
23803 | 142 |
|
143 |
in |
|
144 |
||
27842 | 145 |
fun present_span span = |
146 |
Markup.enclose (kind_markup (span_kind span)) (implode (map present_token (span_content span))); |
|
147 |
||
148 |
fun report_span span = |
|
149 |
Position.report (kind_markup (span_kind span)) (Position.encode_range (span_range span)); |
|
23803 | 150 |
|
151 |
end; |
|
152 |
||
28434 | 153 |
|
154 |
||
155 |
(** units: commands with proof **) |
|
156 |
||
157 |
(* scanning spans *) |
|
158 |
||
159 |
val eof = Span (Command "", []); |
|
160 |
||
161 |
fun is_eof (Span (Command "", _)) = true |
|
162 |
| is_eof _ = false; |
|
163 |
||
164 |
val not_eof = not o is_eof; |
|
165 |
||
166 |
val stopper = Scan.stopper (K eof) is_eof; |
|
167 |
||
168 |
||
169 |
(* unit_source *) |
|
170 |
||
171 |
local |
|
172 |
||
173 |
fun command_with pred = Scan.one (fn (Span (Command name, _)) => pred name | _ => false); |
|
174 |
||
175 |
val proof = Scan.pass 1 (Scan.repeat (Scan.depend (fn d => |
|
28454
c63168db774c
unit_source: more rigid parsing, stop after final qed;
wenzelm
parents:
28438
diff
changeset
|
176 |
if d <= 0 then Scan.fail |
28434 | 177 |
else |
28454
c63168db774c
unit_source: more rigid parsing, stop after final qed;
wenzelm
parents:
28438
diff
changeset
|
178 |
command_with K.is_qed_global >> pair ~1 || |
28434 | 179 |
command_with K.is_proof_goal >> pair (d + 1) || |
28454
c63168db774c
unit_source: more rigid parsing, stop after final qed;
wenzelm
parents:
28438
diff
changeset
|
180 |
(if d = 0 then Scan.fail else command_with K.is_qed >> pair (d - 1)) || |
28438
32bb6b4eb390
unit_source: explicit treatment of 'oops' proofs;
wenzelm
parents:
28434
diff
changeset
|
181 |
Scan.unless (command_with K.is_theory) (Scan.one not_eof) >> pair d)) -- Scan.state); |
28434 | 182 |
|
28438
32bb6b4eb390
unit_source: explicit treatment of 'oops' proofs;
wenzelm
parents:
28434
diff
changeset
|
183 |
val unit = |
28454
c63168db774c
unit_source: more rigid parsing, stop after final qed;
wenzelm
parents:
28438
diff
changeset
|
184 |
command_with K.is_theory_goal -- proof >> (fn (a, (bs, d)) => (a, bs, d >= 0)) || |
28438
32bb6b4eb390
unit_source: explicit treatment of 'oops' proofs;
wenzelm
parents:
28434
diff
changeset
|
185 |
Scan.one not_eof >> (fn a => (a, [], true)); |
28434 | 186 |
|
187 |
in |
|
188 |
||
189 |
fun unit_source src = Source.source stopper (Scan.bulk unit) NONE src; |
|
190 |
||
23726 | 191 |
end; |
28434 | 192 |
|
193 |
end; |