# HG changeset patch
# User wenzelm
# Date 1426188848 -3600
# Node ID 86a76300137e5c3bfc4d7e8d4e02ae5d7704d3aa
# Parent  d6824d8490bef4f6ab3c693e80663079eba9e86e
clarified command content;

diff -r d6824d8490be -r 86a76300137e src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Thu Mar 12 16:47:47 2015 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Thu Mar 12 20:34:08 2015 +0100
@@ -284,7 +284,7 @@
     /* result structure */
 
     val spans = parse_spans(text)
-    spans.foreach(span => add(Command(Document_ID.none, node_name, Nil, span)))
+    spans.foreach(span => add(Command(Document_ID.none, node_name, None, span)))
     result()
   }
 }
diff -r d6824d8490be -r 86a76300137e src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Thu Mar 12 16:47:47 2015 +0100
+++ b/src/Pure/PIDE/command.scala	Thu Mar 12 20:34:08 2015 +0100
@@ -253,15 +253,17 @@
   def apply(
     id: Document_ID.Command,
     node_name: Document.Node.Name,
-    blobs: List[Blob],
+    blobs: Option[(List[Blob], Int)],
     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 (blobs_list, blobs_index) = blobs.getOrElse((Nil, -1))
+    new Command(
+      id, node_name, blobs_list, blobs_index, span1, source, Results.empty, Markup_Tree.empty)
   }
 
   val empty: Command =
-    Command(Document_ID.none, Document.Node.Name.empty, Nil, Command_Span.empty)
+    Command(Document_ID.none, Document.Node.Name.empty, None, Command_Span.empty)
 
   def unparsed(
     id: Document_ID.Command,
@@ -270,7 +272,7 @@
     markup: Markup_Tree): Command =
   {
     val (source1, span1) = Command_Span.unparsed(source).compact_source
-    new Command(id, Document.Node.Name.empty, Nil, span1, source1, results, markup)
+    new Command(id, Document.Node.Name.empty, Nil, -1, span1, source1, results, markup)
   }
 
   def unparsed(source: String): Command =
@@ -312,6 +314,7 @@
     val id: Document_ID.Command,
     val node_name: Document.Node.Name,
     val blobs: List[Command.Blob],
+    val blobs_index: Int,
     val span: Command_Span.Span,
     val source: String,
     val init_results: Command.Results,
diff -r d6824d8490be -r 86a76300137e src/Pure/PIDE/command_span.scala
--- a/src/Pure/PIDE/command_span.scala	Thu Mar 12 16:47:47 2015 +0100
+++ b/src/Pure/PIDE/command_span.scala	Thu Mar 12 20:34:08 2015 +0100
@@ -99,14 +99,17 @@
       node_name: Document.Node.Name,
       span: Span,
       get_blob: Document.Node.Name => Option[Document.Blob])
-    : List[Command.Blob] =
+    : (List[Command.Blob], Int) =
   {
-    span_files(syntax, span)._1.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)
-      })
+    val (files, index) = span_files(syntax, span)
+    val blobs =
+      files.map(file =>
+        Exn.capture {
+          val name =
+            Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file)))
+          val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
+          (name, blob)
+        })
+    (blobs, index)
   }
 }
diff -r d6824d8490be -r 86a76300137e src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Thu Mar 12 16:47:47 2015 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Thu Mar 12 20:34:08 2015 +0100
@@ -143,8 +143,8 @@
 
   @tailrec private def chop_common(
       cmds: List[Command],
-      blobs_spans: List[(List[Command.Blob], Command_Span.Span)])
-    : (List[Command], List[(List[Command.Blob], Command_Span.Span)]) =
+      blobs_spans: List[((List[Command.Blob], Int), Command_Span.Span)])
+    : (List[Command], List[((List[Command.Blob], Int), Command_Span.Span)]) =
   {
     (cmds, blobs_spans) match {
       case (cmd :: cmds, (blobs, span) :: rest) if cmd.blobs == blobs && cmd.span == span =>
@@ -179,7 +179,8 @@
       case cmd :: _ =>
         val hook = commands.prev(cmd)
         val inserted =
-          blobs_spans2.map({ case (blobs, span) => Command(Document_ID.make(), name, blobs, span) })
+          blobs_spans2.map({ case (blobs, span) =>
+            Command(Document_ID.make(), name, Some(blobs), span) })
         (commands /: cmds2)(_ - _).append_after(hook, inserted)
     }
   }