# HG changeset patch
# User wenzelm
# Date 1407788988 -7200
# Node ID e1abca2527da3216fbe35dfe5869397bd0c257bf
# Parent  fd03765b06c0db67d9ec852843875b3abced974a
more explicit type Span in Scala, according to ML version;

diff -r fd03765b06c0 -r e1abca2527da src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Mon Aug 11 20:46:56 2014 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Mon Aug 11 22:29:48 2014 +0200
@@ -57,8 +57,8 @@
   def keyword_kind_files(name: String): Option[(String, List[String])] = keywords.get(name)
   def keyword_kind(name: String): Option[String] = keyword_kind_files(name).map(_._1)
 
-  def load(span: List[Token]): Option[List[String]] =
-    keywords.get(Command.name(span)) match {
+  def load_command(name: String): Option[List[String]] =
+    keywords.get(name) match {
       case Some((Keyword.THY_LOAD, exts)) => Some(exts)
       case _ => None
     }
diff -r fd03765b06c0 -r e1abca2527da src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Mon Aug 11 20:46:56 2014 +0200
+++ b/src/Pure/PIDE/command.scala	Mon Aug 11 22:29:48 2014 +0200
@@ -250,39 +250,18 @@
 
   /* make commands */
 
-  def name(span: List[Token]): String =
-    span.find(_.is_command) match { case Some(tok) => tok.source case _ => "" }
-
-  private def source_span(span: List[Token]): (String, List[Token]) =
-  {
-    val source: String =
-      span match {
-        case List(tok) => tok.source
-        case _ => span.map(_.source).mkString
-      }
-
-    val span1 = new mutable.ListBuffer[Token]
-    var i = 0
-    for (Token(kind, s) <- span) {
-      val n = s.length
-      val s1 = source.substring(i, i + n)
-      span1 += Token(kind, s1)
-      i += n
-    }
-    (source, span1.toList)
-  }
-
   def apply(
     id: Document_ID.Command,
     node_name: Document.Node.Name,
     blobs: List[Blob],
-    span: List[Token]): Command =
+    span: Thy_Syntax.Span): Command =
   {
-    val (source, span1) = source_span(span)
+    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, Nil)
+  val empty: Command =
+    Command(Document_ID.none, Document.Node.Name.empty, Nil, Thy_Syntax.empty_span)
 
   def unparsed(
     id: Document_ID.Command,
@@ -290,8 +269,8 @@
     results: Results,
     markup: Markup_Tree): Command =
   {
-    val (source1, span) = source_span(List(Token(Token.Kind.UNPARSED, source)))
-    new Command(id, Document.Node.Name.empty, Nil, span, source1, results, markup)
+    val (source1, span1) = Thy_Syntax.unparsed_span(source).compact_source
+    new Command(id, Document.Node.Name.empty, Nil, span1, source1, results, markup)
   }
 
   def unparsed(source: String): Command =
@@ -333,7 +312,7 @@
     val id: Document_ID.Command,
     val node_name: Document.Node.Name,
     val blobs: List[Command.Blob],
-    val span: List[Token],
+    val span: Thy_Syntax.Span,
     val source: String,
     val init_results: Command.Results,
     val init_markup: Markup_Tree)
@@ -341,14 +320,15 @@
   /* classification */
 
   def is_undefined: Boolean = id == Document_ID.none
-  val is_unparsed: Boolean = span.exists(_.is_unparsed)
-  val is_unfinished: Boolean = span.exists(_.is_unfinished)
+  val is_unparsed: Boolean = span.content.exists(_.is_unparsed)
+  val is_unfinished: Boolean = span.content.exists(_.is_unfinished)
 
-  val is_ignored: Boolean = !span.exists(_.is_proper)
-  val is_malformed: Boolean = !is_ignored && (!span.head.is_command || span.exists(_.is_error))
-  def is_command: Boolean = !is_ignored && !is_malformed
+  def is_command: Boolean = span.kind.isInstanceOf[Thy_Syntax.Command_Span]
+  def is_ignored: Boolean = span.kind == Thy_Syntax.Ignored_Span
+  def is_malformed: Boolean = span.kind == Thy_Syntax.Malformed_Span
 
-  def name: String = Command.name(span)
+  def name: String =
+    span.kind match { case Thy_Syntax.Command_Span(name) => name case _ => "" }
 
   override def toString =
     id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
@@ -379,7 +359,8 @@
   def range: Text.Range = chunk.range
 
   val proper_range: Text.Range =
-    Text.Range(0, (length /: span.reverse.iterator.takeWhile(_.is_improper))(_ - _.source.length))
+    Text.Range(0,
+      (length /: span.content.reverse.iterator.takeWhile(_.is_improper))(_ - _.source.length))
 
   def source(range: Text.Range): String = source.substring(range.start, range.stop)
 
diff -r fd03765b06c0 -r e1abca2527da src/Pure/PIDE/prover.scala
--- a/src/Pure/PIDE/prover.scala	Mon Aug 11 20:46:56 2014 +0200
+++ b/src/Pure/PIDE/prover.scala	Mon Aug 11 22:29:48 2014 +0200
@@ -15,7 +15,7 @@
   {
     def add_keywords(keywords: Thy_Header.Keywords): Syntax
     def scan(input: CharSequence): List[Token]
-    def load(span: List[Token]): Option[List[String]]
+    def load_command(name: String): Option[List[String]]
     def load_commands_in(text: String): Boolean
   }
 
diff -r fd03765b06c0 -r e1abca2527da src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Mon Aug 11 20:46:56 2014 +0200
+++ b/src/Pure/Thy/thy_syntax.ML	Mon Aug 11 22:29:48 2014 +0200
@@ -9,7 +9,7 @@
   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 of string * Position.T | Ignored | Malformed
+  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
@@ -69,9 +69,7 @@
 
 (** spans **)
 
-(* type span *)
-
-datatype span_kind = Command of string * Position.T | Ignored | Malformed;
+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;
@@ -84,27 +82,29 @@
 
 local
 
-fun make_span toks =
-  if not (null toks) andalso Token.is_command (hd toks) then
-    Span (Command (Token.content_of (hd toks), Token.pos_of (hd toks)), toks)
-  else if forall Token.is_improper toks then Span (Ignored, toks)
-  else Span (Malformed, toks);
+fun ship span =
+  let
+    val kind =
+      if not (null span) andalso Token.is_command (hd 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, span, improper) =
+fun flush (result, content, improper) =
   result
-  |> not (null span) ? cons (rev span)
-  |> not (null improper) ? cons (rev improper);
+  |> not (null content) ? ship (rev content)
+  |> not (null improper) ? ship (rev improper);
 
-fun parse tok (result, span, improper) =
-  if Token.is_command tok then (flush (result, span, improper), [tok], [])
-  else if Token.is_improper tok then (result, span, tok :: improper)
-  else (result, tok :: (improper @ span), []);
+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 |> map make_span;
+  fold parse toks ([], [], []) |> flush |> rev;
 
 end;
 
@@ -137,7 +137,7 @@
 
 fun resolve_files read_files span =
   (case span of
-    Span (Command (cmd, pos), toks) =>
+    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)
@@ -146,7 +146,7 @@
               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 (cmd, pos), toks') end)
+            in Span (Command_Span (cmd, pos), toks') end)
       else span
   | _ => span);
 
@@ -174,9 +174,9 @@
 
 (* scanning spans *)
 
-val eof = Span (Command ("", Position.none), []);
+val eof = Span (Command_Span ("", Position.none), []);
 
-fun is_eof (Span (Command ("", _), _)) = true
+fun is_eof (Span (Command_Span ("", _), _)) = true
   | is_eof _ = false;
 
 val not_eof = not o is_eof;
@@ -189,10 +189,10 @@
 local
 
 fun command_with pred =
-  Scan.one (fn (Span (Command (name, _), _)) => pred name | _ => false);
+  Scan.one (fn (Span (Command_Span (name, _), _)) => pred name | _ => false);
 
 val proof_atom =
-  Scan.one (fn (Span (Command (name, _), _)) => Keyword.is_proof_body name | _ => true) >> atom;
+  Scan.one (fn (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 fd03765b06c0 -r e1abca2527da src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Mon Aug 11 20:46:56 2014 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Mon Aug 11 22:29:48 2014 +0200
@@ -13,23 +13,69 @@
 
 object Thy_Syntax
 {
-  /** parse spans **/
+  /** spans **/
 
-  def parse_spans(toks: List[Token]): List[List[Token]] =
+  sealed abstract class Span_Kind
+  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])
   {
-    val result = new mutable.ListBuffer[List[Token]]
-    val span = new mutable.ListBuffer[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 (!span.isEmpty) { result += span.toList; span.clear }
-      if (!improper.isEmpty) { result += improper.toList; improper.clear }
+      if (!content.isEmpty) { ship(content.toList); content.clear }
+      if (!improper.isEmpty) { ship(improper.toList); improper.clear }
     }
+
     for (tok <- toks) {
-      if (tok.is_command) { flush(); span += tok }
+      if (tok.is_command) { flush(); content += tok }
       else if (tok.is_improper) improper += tok
-      else { span ++= improper; improper.clear; span += tok }
+      else { content ++= improper; improper.clear; content += tok }
     }
     flush()
 
@@ -185,23 +231,27 @@
     }
   }
 
-  def span_files(syntax: Prover.Syntax, span: List[Token]): List[String] =
-    syntax.load(span) match {
-      case Some(exts) =>
-        find_file(span) match {
-          case Some(file) =>
-            if (exts.isEmpty) List(file)
-            else exts.map(ext => file + "." + ext)
+  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 None => Nil
+      case _ => Nil
     }
 
   def resolve_files(
       resources: Resources,
       syntax: Prover.Syntax,
       node_name: Document.Node.Name,
-      span: List[Token],
+      span: Span,
       get_blob: Document.Node.Name => Option[Document.Blob])
     : List[Command.Blob] =
   {
@@ -219,8 +269,8 @@
 
   @tailrec private def chop_common(
       cmds: List[Command],
-      blobs_spans: List[(List[Command.Blob], List[Token])])
-    : (List[Command], List[(List[Command.Blob], List[Token])]) =
+      blobs_spans: List[(List[Command.Blob], Span)])
+    : (List[Command], List[(List[Command.Blob], Span)]) =
   {
     (cmds, blobs_spans) match {
       case (cmd :: cmds, (blobs, span) :: rest) if cmd.blobs == blobs && cmd.span == span =>