src/Pure/PIDE/command.scala
changeset 59684 86a76300137e
parent 59203 5f0bd5afc16d
child 59689 7968c57ea240
     1.1 --- a/src/Pure/PIDE/command.scala	Thu Mar 12 16:47:47 2015 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Thu Mar 12 20:34:08 2015 +0100
     1.3 @@ -253,15 +253,17 @@
     1.4    def apply(
     1.5      id: Document_ID.Command,
     1.6      node_name: Document.Node.Name,
     1.7 -    blobs: List[Blob],
     1.8 +    blobs: Option[(List[Blob], Int)],
     1.9      span: Command_Span.Span): Command =
    1.10    {
    1.11      val (source, span1) = span.compact_source
    1.12 -    new Command(id, node_name, blobs, span1, source, Results.empty, Markup_Tree.empty)
    1.13 +    val (blobs_list, blobs_index) = blobs.getOrElse((Nil, -1))
    1.14 +    new Command(
    1.15 +      id, node_name, blobs_list, blobs_index, span1, source, Results.empty, Markup_Tree.empty)
    1.16    }
    1.17  
    1.18    val empty: Command =
    1.19 -    Command(Document_ID.none, Document.Node.Name.empty, Nil, Command_Span.empty)
    1.20 +    Command(Document_ID.none, Document.Node.Name.empty, None, Command_Span.empty)
    1.21  
    1.22    def unparsed(
    1.23      id: Document_ID.Command,
    1.24 @@ -270,7 +272,7 @@
    1.25      markup: Markup_Tree): Command =
    1.26    {
    1.27      val (source1, span1) = Command_Span.unparsed(source).compact_source
    1.28 -    new Command(id, Document.Node.Name.empty, Nil, span1, source1, results, markup)
    1.29 +    new Command(id, Document.Node.Name.empty, Nil, -1, span1, source1, results, markup)
    1.30    }
    1.31  
    1.32    def unparsed(source: String): Command =
    1.33 @@ -312,6 +314,7 @@
    1.34      val id: Document_ID.Command,
    1.35      val node_name: Document.Node.Name,
    1.36      val blobs: List[Command.Blob],
    1.37 +    val blobs_index: Int,
    1.38      val span: Command_Span.Span,
    1.39      val source: String,
    1.40      val init_results: Command.Results,