clarified command content;
authorwenzelm
Thu Mar 12 20:34:08 2015 +0100 (2015-03-12 ago)
changeset 5968486a76300137e
parent 59683 d6824d8490be
child 59685 c043306d2598
clarified command content;
src/Pure/Isar/outer_syntax.scala
src/Pure/PIDE/command.scala
src/Pure/PIDE/command_span.scala
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Thu Mar 12 16:47:47 2015 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Thu Mar 12 20:34:08 2015 +0100
     1.3 @@ -284,7 +284,7 @@
     1.4      /* result structure */
     1.5  
     1.6      val spans = parse_spans(text)
     1.7 -    spans.foreach(span => add(Command(Document_ID.none, node_name, Nil, span)))
     1.8 +    spans.foreach(span => add(Command(Document_ID.none, node_name, None, span)))
     1.9      result()
    1.10    }
    1.11  }
     2.1 --- a/src/Pure/PIDE/command.scala	Thu Mar 12 16:47:47 2015 +0100
     2.2 +++ b/src/Pure/PIDE/command.scala	Thu Mar 12 20:34:08 2015 +0100
     2.3 @@ -253,15 +253,17 @@
     2.4    def apply(
     2.5      id: Document_ID.Command,
     2.6      node_name: Document.Node.Name,
     2.7 -    blobs: List[Blob],
     2.8 +    blobs: Option[(List[Blob], Int)],
     2.9      span: Command_Span.Span): Command =
    2.10    {
    2.11      val (source, span1) = span.compact_source
    2.12 -    new Command(id, node_name, blobs, span1, source, Results.empty, Markup_Tree.empty)
    2.13 +    val (blobs_list, blobs_index) = blobs.getOrElse((Nil, -1))
    2.14 +    new Command(
    2.15 +      id, node_name, blobs_list, blobs_index, span1, source, Results.empty, Markup_Tree.empty)
    2.16    }
    2.17  
    2.18    val empty: Command =
    2.19 -    Command(Document_ID.none, Document.Node.Name.empty, Nil, Command_Span.empty)
    2.20 +    Command(Document_ID.none, Document.Node.Name.empty, None, Command_Span.empty)
    2.21  
    2.22    def unparsed(
    2.23      id: Document_ID.Command,
    2.24 @@ -270,7 +272,7 @@
    2.25      markup: Markup_Tree): Command =
    2.26    {
    2.27      val (source1, span1) = Command_Span.unparsed(source).compact_source
    2.28 -    new Command(id, Document.Node.Name.empty, Nil, span1, source1, results, markup)
    2.29 +    new Command(id, Document.Node.Name.empty, Nil, -1, span1, source1, results, markup)
    2.30    }
    2.31  
    2.32    def unparsed(source: String): Command =
    2.33 @@ -312,6 +314,7 @@
    2.34      val id: Document_ID.Command,
    2.35      val node_name: Document.Node.Name,
    2.36      val blobs: List[Command.Blob],
    2.37 +    val blobs_index: Int,
    2.38      val span: Command_Span.Span,
    2.39      val source: String,
    2.40      val init_results: Command.Results,
     3.1 --- a/src/Pure/PIDE/command_span.scala	Thu Mar 12 16:47:47 2015 +0100
     3.2 +++ b/src/Pure/PIDE/command_span.scala	Thu Mar 12 20:34:08 2015 +0100
     3.3 @@ -99,14 +99,17 @@
     3.4        node_name: Document.Node.Name,
     3.5        span: Span,
     3.6        get_blob: Document.Node.Name => Option[Document.Blob])
     3.7 -    : List[Command.Blob] =
     3.8 +    : (List[Command.Blob], Int) =
     3.9    {
    3.10 -    span_files(syntax, span)._1.map(file_name =>
    3.11 -      Exn.capture {
    3.12 -        val name =
    3.13 -          Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file_name)))
    3.14 -        val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
    3.15 -        (name, blob)
    3.16 -      })
    3.17 +    val (files, index) = span_files(syntax, span)
    3.18 +    val blobs =
    3.19 +      files.map(file =>
    3.20 +        Exn.capture {
    3.21 +          val name =
    3.22 +            Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file)))
    3.23 +          val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
    3.24 +          (name, blob)
    3.25 +        })
    3.26 +    (blobs, index)
    3.27    }
    3.28  }
     4.1 --- a/src/Pure/Thy/thy_syntax.scala	Thu Mar 12 16:47:47 2015 +0100
     4.2 +++ b/src/Pure/Thy/thy_syntax.scala	Thu Mar 12 20:34:08 2015 +0100
     4.3 @@ -143,8 +143,8 @@
     4.4  
     4.5    @tailrec private def chop_common(
     4.6        cmds: List[Command],
     4.7 -      blobs_spans: List[(List[Command.Blob], Command_Span.Span)])
     4.8 -    : (List[Command], List[(List[Command.Blob], Command_Span.Span)]) =
     4.9 +      blobs_spans: List[((List[Command.Blob], Int), Command_Span.Span)])
    4.10 +    : (List[Command], List[((List[Command.Blob], Int), Command_Span.Span)]) =
    4.11    {
    4.12      (cmds, blobs_spans) match {
    4.13        case (cmd :: cmds, (blobs, span) :: rest) if cmd.blobs == blobs && cmd.span == span =>
    4.14 @@ -179,7 +179,8 @@
    4.15        case cmd :: _ =>
    4.16          val hook = commands.prev(cmd)
    4.17          val inserted =
    4.18 -          blobs_spans2.map({ case (blobs, span) => Command(Document_ID.make(), name, blobs, span) })
    4.19 +          blobs_spans2.map({ case (blobs, span) =>
    4.20 +            Command(Document_ID.make(), name, Some(blobs), span) })
    4.21          (commands /: cmds2)(_ - _).append_after(hook, inserted)
    4.22      }
    4.23    }