diff -r 922273b7bf8a -r c0c5652e796e src/Pure/Thy/thy_syntax.ML
--- 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;