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