# HG changeset patch
# User wenzelm
# Date 1407794912 -7200
# Node ID c0c5652e796e0d105a9c67aef6ce3e3b3e9f4402
# Parent  922273b7bf8af332ec727b3fadf01fd767f9c934
separate module Command_Span: mostly syntactic representation;
potentially prover-specific Output_Syntax.parse_spans;

diff -r 922273b7bf8a -r c0c5652e796e src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Mon Aug 11 22:59:38 2014 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Aug 12 00:08:32 2014 +0200
@@ -33,6 +33,8 @@
   val print_outer_syntax: unit -> unit
   val scan: Position.T -> string -> Token.T list
   val parse: Position.T -> string -> Toplevel.transition list
+  val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list
+  val parse_spans: Token.T list -> Command_Span.span list
   type isar
   val isar: TextIO.instream -> bool -> isar
   val side_comments: Token.T list -> Token.T list
@@ -269,6 +271,43 @@
   |> toplevel_source false NONE lookup_commands_dynamic
   |> Source.exhaust;
 
+fun parse_tokens lexs pos =
+  Source.of_string #>
+  Symbol.source #>
+  Token.source {do_recover = SOME false} (K lexs) pos #>
+  Source.exhaust;
+
+
+(* parse spans *)
+
+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.Command_Span (Token.content_of (hd span), Token.pos_of (hd span))
+      else if forall Token.is_improper span then Command_Span.Ignored_Span
+      else Command_Span.Malformed_Span;
+  in cons (Command_Span.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;
+
 
 (* interactive source of toplevel transformers *)
 
diff -r 922273b7bf8a -r c0c5652e796e src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Mon Aug 11 22:59:38 2014 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Tue Aug 12 00:08:32 2014 +0200
@@ -152,6 +152,41 @@
   }
 
 
+  /* parse_spans */
+
+  def parse_spans(toks: List[Token]): List[Command_Span.Span] =
+  {
+    val result = new mutable.ListBuffer[Command_Span.Span]
+    val content = new mutable.ListBuffer[Token]
+    val improper = new mutable.ListBuffer[Token]
+
+    def ship(span: List[Token])
+    {
+      val kind =
+        if (!span.isEmpty && span.head.is_command && !span.exists(_.is_error))
+          Command_Span.Command_Span(span.head.source)
+        else if (span.forall(_.is_improper)) Command_Span.Ignored_Span
+        else Command_Span.Malformed_Span
+      result += Command_Span.Span(kind, span)
+    }
+
+    def flush()
+    {
+      if (!content.isEmpty) { ship(content.toList); content.clear }
+      if (!improper.isEmpty) { ship(improper.toList); improper.clear }
+    }
+
+    for (tok <- toks) {
+      if (tok.is_command) { flush(); content += tok }
+      else if (tok.is_improper) improper += tok
+      else { content ++= improper; improper.clear; content += tok }
+    }
+    flush()
+
+    result.toList
+  }
+
+
   /* language context */
 
   def set_language_context(context: Completion.Language_Context): Outer_Syntax =
diff -r 922273b7bf8a -r c0c5652e796e src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Mon Aug 11 22:59:38 2014 +0200
+++ b/src/Pure/PIDE/command.ML	Tue Aug 12 00:08:32 2014 +0200
@@ -121,9 +121,9 @@
   in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end
 
 fun resolve_files master_dir blobs toks =
-  (case Thy_Syntax.parse_spans toks of
+  (case Outer_Syntax.parse_spans toks of
     [span] => span
-      |> Thy_Syntax.resolve_files (fn cmd => fn (path, pos) =>
+      |> Command_Span.resolve_files (fn cmd => fn (path, pos) =>
         let
           fun make_file src_path (Exn.Res (file_node, NONE)) =
                 Exn.interruptible_capture (fn () =>
@@ -140,7 +140,7 @@
             map2 make_file src_paths blobs
           else error ("Misalignment of inlined files" ^ Position.here pos)
         end)
-      |> Thy_Syntax.span_content
+      |> Command_Span.content
   | _ => toks);
 
 in
diff -r 922273b7bf8a -r c0c5652e796e src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Mon Aug 11 22:59:38 2014 +0200
+++ b/src/Pure/PIDE/command.scala	Tue Aug 12 00:08:32 2014 +0200
@@ -254,14 +254,14 @@
     id: Document_ID.Command,
     node_name: Document.Node.Name,
     blobs: List[Blob],
-    span: Thy_Syntax.Span): Command =
+    span: Command_Span.Span): Command =
   {
     val (source, span1) = span.compact_source
     new Command(id, node_name, blobs, span1, source, Results.empty, Markup_Tree.empty)
   }
 
   val empty: Command =
-    Command(Document_ID.none, Document.Node.Name.empty, Nil, Thy_Syntax.empty_span)
+    Command(Document_ID.none, Document.Node.Name.empty, Nil, Command_Span.empty)
 
   def unparsed(
     id: Document_ID.Command,
@@ -269,7 +269,7 @@
     results: Results,
     markup: Markup_Tree): Command =
   {
-    val (source1, span1) = Thy_Syntax.unparsed_span(source).compact_source
+    val (source1, span1) = Command_Span.unparsed(source).compact_source
     new Command(id, Document.Node.Name.empty, Nil, span1, source1, results, markup)
   }
 
@@ -312,7 +312,7 @@
     val id: Document_ID.Command,
     val node_name: Document.Node.Name,
     val blobs: List[Command.Blob],
-    val span: Thy_Syntax.Span,
+    val span: Command_Span.Span,
     val source: String,
     val init_results: Command.Results,
     val init_markup: Markup_Tree)
@@ -320,12 +320,12 @@
   /* name and classification */
 
   def name: String =
-    span.kind match { case Thy_Syntax.Command_Span(name) => name case _ => "" }
+    span.kind match { case Command_Span.Command_Span(name) => name case _ => "" }
 
   override def toString = id + "/" + span.kind.toString
 
-  def is_proper: Boolean = span.kind.isInstanceOf[Thy_Syntax.Command_Span]
-  def is_ignored: Boolean = span.kind == Thy_Syntax.Ignored_Span
+  def is_proper: Boolean = span.kind.isInstanceOf[Command_Span.Command_Span]
+  def is_ignored: Boolean = span.kind == Command_Span.Ignored_Span
 
   def is_undefined: Boolean = id == Document_ID.none
   val is_unparsed: Boolean = span.content.exists(_.is_unparsed)
diff -r 922273b7bf8a -r c0c5652e796e src/Pure/PIDE/command_span.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/command_span.ML	Tue Aug 12 00:08:32 2014 +0200
@@ -0,0 +1,70 @@
+(*  Title:      Pure/PIDE/command_span.ML
+    Author:     Makarius
+
+Syntactic representation of command spans.
+*)
+
+signature COMMAND_SPAN =
+sig
+  datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span
+  datatype span = Span of kind * Token.T list
+  val kind: span -> kind
+  val content: span -> Token.T list
+  val resolve_files: (string -> Path.T * Position.T -> Token.file Exn.result list) -> span -> span
+end;
+
+structure Command_Span: COMMAND_SPAN =
+struct
+
+datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span;
+datatype span = Span of kind * Token.T list;
+
+fun kind (Span (k, _)) = k;
+fun content (Span (_, toks)) = toks;
+
+
+(* resolve 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;
+
+end;
+
diff -r 922273b7bf8a -r c0c5652e796e src/Pure/PIDE/command_span.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/command_span.scala	Tue Aug 12 00:08:32 2014 +0200
@@ -0,0 +1,104 @@
+/*  Title:      Pure/PIDE/command_span.scala
+    Author:     Makarius
+
+Syntactic representation of command spans.
+*/
+
+package isabelle
+
+
+import scala.collection.mutable
+
+
+object Command_Span
+{
+  sealed abstract class Kind {
+    override def toString: String =
+      this match {
+        case Command_Span(name) => if (name != "") name else "<command>"
+        case Ignored_Span => "<ignored>"
+        case Malformed_Span => "<malformed>"
+      }
+  }
+  case class Command_Span(name: String) extends Kind
+  case object Ignored_Span extends Kind
+  case object Malformed_Span extends Kind
+
+  sealed case class Span(kind: Kind, content: List[Token])
+  {
+    def compact_source: (String, Span) =
+    {
+      val source: String =
+        content match {
+          case List(tok) => tok.source
+          case toks => toks.map(_.source).mkString
+        }
+
+      val content1 = new mutable.ListBuffer[Token]
+      var i = 0
+      for (Token(kind, s) <- content) {
+        val n = s.length
+        val s1 = source.substring(i, i + n)
+        content1 += Token(kind, s1)
+        i += n
+      }
+      (source, Span(kind, content1.toList))
+    }
+  }
+
+  val empty: Span = Span(Ignored_Span, Nil)
+
+  def unparsed(source: String): Span =
+    Span(Malformed_Span, List(Token(Token.Kind.UNPARSED, source)))
+
+
+  /* resolve inlined files */
+
+  private def find_file(tokens: List[Token]): Option[String] =
+  {
+    def clean(toks: List[Token]): List[Token] =
+      toks match {
+        case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts)
+        case t :: ts => t :: clean(ts)
+        case Nil => Nil
+      }
+    clean(tokens.filter(_.is_proper)) match {
+      case tok :: toks if tok.is_command => toks.find(_.is_name).map(_.content)
+      case _ => None
+    }
+  }
+
+  def span_files(syntax: Prover.Syntax, span: Span): List[String] =
+    span.kind match {
+      case Command_Span(name) =>
+        syntax.load_command(name) match {
+          case Some(exts) =>
+            find_file(span.content) match {
+              case Some(file) =>
+                if (exts.isEmpty) List(file)
+                else exts.map(ext => file + "." + ext)
+              case None => Nil
+            }
+          case None => Nil
+        }
+      case _ => Nil
+    }
+
+  def resolve_files(
+      resources: Resources,
+      syntax: Prover.Syntax,
+      node_name: Document.Node.Name,
+      span: Span,
+      get_blob: Document.Node.Name => Option[Document.Blob])
+    : List[Command.Blob] =
+  {
+    span_files(syntax, span).map(file_name =>
+      Exn.capture {
+        val name =
+          Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file_name)))
+        val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
+        (name, blob)
+      })
+  }
+}
+
diff -r 922273b7bf8a -r c0c5652e796e src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Mon Aug 11 22:59:38 2014 +0200
+++ b/src/Pure/PIDE/document.ML	Tue Aug 12 00:08:32 2014 +0200
@@ -318,7 +318,7 @@
       val span =
         Lazy.lazy (fn () =>
           Position.setmp_thread_data (Position.id_only id)
-            (fn () => Thy_Syntax.parse_tokens (Keyword.get_lexicons ()) (Position.id id) text) ());
+            (fn () => Outer_Syntax.parse_tokens (Keyword.get_lexicons ()) (Position.id id) text) ());
       val _ =
         Position.setmp_thread_data (Position.id_only id)
           (fn () => Output.status (Markup.markup_only Markup.accepted)) ();
diff -r 922273b7bf8a -r c0c5652e796e src/Pure/PIDE/prover.scala
--- a/src/Pure/PIDE/prover.scala	Mon Aug 11 22:59:38 2014 +0200
+++ b/src/Pure/PIDE/prover.scala	Tue Aug 12 00:08:32 2014 +0200
@@ -15,6 +15,7 @@
   {
     def add_keywords(keywords: Thy_Header.Keywords): Syntax
     def scan(input: CharSequence): List[Token]
+    def parse_spans(toks: List[Token]): List[Command_Span.Span]
     def load_command(name: String): Option[List[String]]
     def load_commands_in(text: String): Boolean
   }
diff -r 922273b7bf8a -r c0c5652e796e src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Mon Aug 11 22:59:38 2014 +0200
+++ b/src/Pure/PIDE/resources.ML	Tue Aug 12 00:08:32 2014 +0200
@@ -132,7 +132,7 @@
 fun excursion master_dir last_timing init elements =
   let
     fun prepare_span span =
-      Thy_Syntax.span_content span
+      Command_Span.content span
       |> Command.read init master_dir []
       |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
 
@@ -157,8 +157,8 @@
     val _ = Thy_Header.define_keywords header;
 
     val lexs = Keyword.get_lexicons ();
-    val toks = Thy_Syntax.parse_tokens lexs text_pos text;
-    val spans = Thy_Syntax.parse_spans toks;
+    val toks = Outer_Syntax.parse_tokens lexs text_pos text;
+    val spans = Outer_Syntax.parse_spans toks;
     val elements = Thy_Syntax.parse_elements spans;
 
     fun init () =
diff -r 922273b7bf8a -r c0c5652e796e src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Mon Aug 11 22:59:38 2014 +0200
+++ b/src/Pure/PIDE/resources.scala	Tue Aug 12 00:08:32 2014 +0200
@@ -56,8 +56,8 @@
 
   def loaded_files(syntax: Prover.Syntax, text: String): List[String] =
     if (syntax.load_commands_in(text)) {
-      val spans = Thy_Syntax.parse_spans(syntax.scan(text))
-      spans.iterator.map(Thy_Syntax.span_files(syntax, _)).flatten.toList
+      val spans = syntax.parse_spans(syntax.scan(text))
+      spans.iterator.map(Command_Span.span_files(syntax, _)).flatten.toList
     }
     else Nil
 
diff -r 922273b7bf8a -r c0c5652e796e src/Pure/ROOT
--- a/src/Pure/ROOT	Mon Aug 11 22:59:38 2014 +0200
+++ b/src/Pure/ROOT	Tue Aug 12 00:08:32 2014 +0200
@@ -160,6 +160,7 @@
     "ML/ml_syntax.ML"
     "PIDE/active.ML"
     "PIDE/command.ML"
+    "PIDE/command_span.ML"
     "PIDE/document.ML"
     "PIDE/document_id.ML"
     "PIDE/execution.ML"
diff -r 922273b7bf8a -r c0c5652e796e src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Aug 11 22:59:38 2014 +0200
+++ b/src/Pure/ROOT.ML	Tue Aug 12 00:08:32 2014 +0200
@@ -236,6 +236,7 @@
 
 (*theory sources*)
 use "Thy/thy_header.ML";
+use "PIDE/command_span.ML";
 use "Thy/thy_syntax.ML";
 use "Thy/html.ML";
 use "Thy/latex.ML";
diff -r 922273b7bf8a -r c0c5652e796e src/Pure/Thy/thy_structure.scala
--- a/src/Pure/Thy/thy_structure.scala	Mon Aug 11 22:59:38 2014 +0200
+++ b/src/Pure/Thy/thy_structure.scala	Tue Aug 12 00:08:32 2014 +0200
@@ -63,7 +63,7 @@
 
     /* result structure */
 
-    val spans = Thy_Syntax.parse_spans(syntax.scan(text))
+    val spans = syntax.parse_spans(syntax.scan(text))
     spans.foreach(span => add(Command(Document_ID.none, node_name, Nil, span)))
     result()
   }
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;
diff -r 922273b7bf8a -r c0c5652e796e src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Mon Aug 11 22:59:38 2014 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Tue Aug 12 00:08:32 2014 +0200
@@ -13,84 +13,6 @@
 
 object Thy_Syntax
 {
-  /** spans **/
-
-  sealed abstract class Span_Kind {
-    override def toString: String =
-      this match {
-        case Command_Span(name) => if (name != "") name else "<command>"
-        case Ignored_Span => "<ignored>"
-        case Malformed_Span => "<malformed>"
-      }
-  }
-  case class Command_Span(name: String) extends Span_Kind
-  case object Ignored_Span extends Span_Kind
-  case object Malformed_Span extends Span_Kind
-
-  sealed case class Span(kind: Span_Kind, content: List[Token])
-  {
-    def compact_source: (String, Span) =
-    {
-      val source: String =
-        content match {
-          case List(tok) => tok.source
-          case toks => toks.map(_.source).mkString
-        }
-
-      val content1 = new mutable.ListBuffer[Token]
-      var i = 0
-      for (Token(kind, s) <- content) {
-        val n = s.length
-        val s1 = source.substring(i, i + n)
-        content1 += Token(kind, s1)
-        i += n
-      }
-      (source, Span(kind, content1.toList))
-    }
-  }
-
-  val empty_span: Span = Span(Ignored_Span, Nil)
-
-  def unparsed_span(source: String): Span =
-    Span(Malformed_Span, List(Token(Token.Kind.UNPARSED, source)))
-
-
-  /* parse */
-
-  def parse_spans(toks: List[Token]): List[Span] =
-  {
-    val result = new mutable.ListBuffer[Span]
-    val content = new mutable.ListBuffer[Token]
-    val improper = new mutable.ListBuffer[Token]
-
-    def ship(span: List[Token])
-    {
-      val kind =
-        if (!span.isEmpty && span.head.is_command && !span.exists(_.is_error))
-          Command_Span(span.head.source)
-        else if (span.forall(_.is_improper)) Ignored_Span
-        else Malformed_Span
-      result += Span(kind, span)
-    }
-
-    def flush()
-    {
-      if (!content.isEmpty) { ship(content.toList); content.clear }
-      if (!improper.isEmpty) { ship(improper.toList); improper.clear }
-    }
-
-    for (tok <- toks) {
-      if (tok.is_command) { flush(); content += tok }
-      else if (tok.is_improper) improper += tok
-      else { content ++= improper; improper.clear; content += tok }
-    }
-    flush()
-
-    result.toList
-  }
-
-
-
   /** perspective **/
 
   def command_perspective(
@@ -222,62 +144,12 @@
   }
 
 
-  /* inlined files */
-
-  private def find_file(tokens: List[Token]): Option[String] =
-  {
-    def clean(toks: List[Token]): List[Token] =
-      toks match {
-        case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts)
-        case t :: ts => t :: clean(ts)
-        case Nil => Nil
-      }
-    clean(tokens.filter(_.is_proper)) match {
-      case tok :: toks if tok.is_command => toks.find(_.is_name).map(_.content)
-      case _ => None
-    }
-  }
-
-  def span_files(syntax: Prover.Syntax, span: Span): List[String] =
-    span.kind match {
-      case Command_Span(name) =>
-        syntax.load_command(name) match {
-          case Some(exts) =>
-            find_file(span.content) match {
-              case Some(file) =>
-                if (exts.isEmpty) List(file)
-                else exts.map(ext => file + "." + ext)
-              case None => Nil
-            }
-          case None => Nil
-        }
-      case _ => Nil
-    }
-
-  def resolve_files(
-      resources: Resources,
-      syntax: Prover.Syntax,
-      node_name: Document.Node.Name,
-      span: Span,
-      get_blob: Document.Node.Name => Option[Document.Blob])
-    : List[Command.Blob] =
-  {
-    span_files(syntax, span).map(file_name =>
-      Exn.capture {
-        val name =
-          Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file_name)))
-        val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
-        (name, blob)
-      })
-  }
-
-
   /* reparse range of command spans */
 
   @tailrec private def chop_common(
       cmds: List[Command],
-      blobs_spans: List[(List[Command.Blob], Span)])
-    : (List[Command], List[(List[Command.Blob], Span)]) =
+      blobs_spans: List[(List[Command.Blob], Command_Span.Span)])
+    : (List[Command], List[(List[Command.Blob], Command_Span.Span)]) =
   {
     (cmds, blobs_spans) match {
       case (cmd :: cmds, (blobs, span) :: rest) if cmd.blobs == blobs && cmd.span == span =>
@@ -296,8 +168,8 @@
   {
     val cmds0 = commands.iterator(first, last).toList
     val blobs_spans0 =
-      parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)).
-        map(span => (resolve_files(resources, syntax, name, span, get_blob), span))
+      syntax.parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)).
+        map(span => (Command_Span.resolve_files(resources, syntax, name, span, get_blob), span))
 
     val (cmds1, blobs_spans1) = chop_common(cmds0, blobs_spans0)
 
diff -r 922273b7bf8a -r c0c5652e796e src/Pure/build-jars
--- a/src/Pure/build-jars	Mon Aug 11 22:59:38 2014 +0200
+++ b/src/Pure/build-jars	Tue Aug 12 00:08:32 2014 +0200
@@ -54,6 +54,7 @@
   Isar/token.scala
   ML/ml_lex.scala
   PIDE/command.scala
+  PIDE/command_span.scala
   PIDE/document.scala
   PIDE/document_id.scala
   PIDE/editor.scala