--- a/src/Pure/Thy/thy_syntax.ML Mon Aug 11 22:59:38 2014 +0200
+++ b/src/Pure/Thy/thy_syntax.ML Tue Aug 12 00:08:32 2014 +0200
@@ -6,39 +6,21 @@
signature THY_SYNTAX =
sig
- val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list
val reports_of_tokens: Token.T list -> bool * Position.report_text list
val present_token: Token.T -> Output.output
- datatype span_kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span
- datatype span = Span of span_kind * Token.T list
- val span_kind: span -> span_kind
- val span_content: span -> Token.T list
- val present_span: span -> Output.output
- val parse_spans: Token.T list -> span list
- val resolve_files: (string -> Path.T * Position.T -> Token.file Exn.result list) -> span -> span
+ val present_span: Command_Span.span -> Output.output
datatype 'a element = Element of 'a * ('a element list * 'a) option
val atom: 'a -> 'a element
val map_element: ('a -> 'b) -> 'a element -> 'b element
val flat_element: 'a element -> 'a list
val last_element: 'a element -> 'a
- val parse_elements: span list -> span element list
+ val parse_elements: Command_Span.span list -> Command_Span.span element list
end;
structure Thy_Syntax: THY_SYNTAX =
struct
-(** tokens **)
-
-(* parse *)
-
-fun parse_tokens lexs pos =
- Source.of_string #>
- Symbol.source #>
- Token.source {do_recover = SOME false} (K lexs) pos #>
- Source.exhaust;
-
-
-(* present *)
+(** presentation **)
local
@@ -60,97 +42,12 @@
let val results = map reports_of_token toks
in (exists fst results, maps snd results) end;
+end;
+
fun present_token tok =
Markup.enclose (Token.markup tok) (Output.output (Token.unparse tok));
-end;
-
-
-
-(** spans **)
-
-datatype span_kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span;
-datatype span = Span of span_kind * Token.T list;
-
-fun span_kind (Span (k, _)) = k;
-fun span_content (Span (_, toks)) = toks;
-
-val present_span = implode o map present_token o span_content;
-
-
-(* parse *)
-
-local
-
-fun ship span =
- let
- val kind =
- if not (null span) andalso Token.is_command (hd span) andalso not (exists Token.is_error span)
- then Command_Span (Token.content_of (hd span), Token.pos_of (hd span))
- else if forall Token.is_improper span then Ignored_Span
- else Malformed_Span;
- in cons (Span (kind, span)) end;
-
-fun flush (result, content, improper) =
- result
- |> not (null content) ? ship (rev content)
- |> not (null improper) ? ship (rev improper);
-
-fun parse tok (result, content, improper) =
- if Token.is_command tok then (flush (result, content, improper), [tok], [])
- else if Token.is_improper tok then (result, content, tok :: improper)
- else (result, tok :: (improper @ content), []);
-
-in
-
-fun parse_spans toks =
- fold parse toks ([], [], []) |> flush |> rev;
-
-end;
-
-
-(* inlined files *)
-
-local
-
-fun clean ((i1, t1) :: (i2, t2) :: toks) =
- if Token.keyword_with (fn s => s = "%" orelse s = "--") t1 then clean toks
- else (i1, t1) :: clean ((i2, t2) :: toks)
- | clean toks = toks;
-
-fun clean_tokens toks =
- ((0 upto length toks - 1) ~~ toks)
- |> filter (fn (_, tok) => Token.is_proper tok)
- |> clean;
-
-fun find_file ((_, tok) :: toks) =
- if Token.is_command tok then
- toks |> get_first (fn (i, tok) =>
- if Token.is_name tok then
- SOME (i, (Path.explode (Token.content_of tok), Token.pos_of tok))
- handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok))
- else NONE)
- else NONE
- | find_file [] = NONE;
-
-in
-
-fun resolve_files read_files span =
- (case span of
- Span (Command_Span (cmd, pos), toks) =>
- if Keyword.is_theory_load cmd then
- (case find_file (clean_tokens toks) of
- NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.here pos)
- | SOME (i, path) =>
- let
- val toks' = toks |> map_index (fn (j, tok) =>
- if i = j then Token.put_files (read_files cmd path) tok
- else tok);
- in Span (Command_Span (cmd, pos), toks') end)
- else span
- | _ => span);
-
-end;
+val present_span = implode o map present_token o Command_Span.content;
@@ -174,9 +71,9 @@
(* scanning spans *)
-val eof = Span (Command_Span ("", Position.none), []);
+val eof = Command_Span.Span (Command_Span.Command_Span ("", Position.none), []);
-fun is_eof (Span (Command_Span ("", _), _)) = true
+fun is_eof (Command_Span.Span (Command_Span.Command_Span ("", _), _)) = true
| is_eof _ = false;
val not_eof = not o is_eof;
@@ -189,10 +86,13 @@
local
fun command_with pred =
- Scan.one (fn (Span (Command_Span (name, _), _)) => pred name | _ => false);
+ Scan.one
+ (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) => pred name | _ => false);
val proof_atom =
- Scan.one (fn (Span (Command_Span (name, _), _)) => Keyword.is_proof_body name | _ => true) >> atom;
+ Scan.one
+ (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) => Keyword.is_proof_body name
+ | _ => true) >> atom;
fun proof_element x = (command_with Keyword.is_proof_goal -- proof_rest >> element || proof_atom) x
and proof_rest x = (Scan.repeat proof_element -- command_with Keyword.is_qed) x;