tuned;
authorwenzelm
Sun Mar 15 12:42:30 2015 +0100 (2015-03-15 ago)
changeset 59701a6efad6acafd
parent 59698 d4ce901f20c5
child 59702 d887abcc7c24
tuned;
src/Pure/PIDE/command.scala
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Sat Mar 14 21:16:29 2015 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Sun Mar 15 12:42:30 2015 +0100
     1.3 @@ -349,12 +349,11 @@
     1.4      }
     1.5  
     1.6    def resolve_files(
     1.7 -      resources: Resources,
     1.8 -      syntax: Prover.Syntax,
     1.9 -      node_name: Document.Node.Name,
    1.10 -      span: Command_Span.Span,
    1.11 -      get_blob: Document.Node.Name => Option[Document.Blob])
    1.12 -    : (List[Command.Blob], Int) =
    1.13 +    resources: Resources,
    1.14 +    syntax: Prover.Syntax,
    1.15 +    get_blob: Document.Node.Name => Option[Document.Blob],
    1.16 +    node_name: Document.Node.Name,
    1.17 +    span: Command_Span.Span): (List[Command.Blob], Int) =
    1.18    {
    1.19      val (files, index) = span_files(syntax, span)
    1.20      val blobs =
     2.1 --- a/src/Pure/Thy/thy_syntax.scala	Sat Mar 14 21:16:29 2015 +0100
     2.2 +++ b/src/Pure/Thy/thy_syntax.scala	Sun Mar 15 12:42:30 2015 +0100
     2.3 @@ -63,7 +63,7 @@
     2.4  
     2.5  
     2.6  
     2.7 -  /** header edits: structure and outer syntax **/
     2.8 +  /** header edits: graph structure and outer syntax **/
     2.9  
    2.10    private def header_edits(
    2.11      resources: Resources,
    2.12 @@ -157,14 +157,14 @@
    2.13      resources: Resources,
    2.14      syntax: Prover.Syntax,
    2.15      get_blob: Document.Node.Name => Option[Document.Blob],
    2.16 -    name: Document.Node.Name,
    2.17 +    node_name: Document.Node.Name,
    2.18      commands: Linear_Set[Command],
    2.19      first: Command, last: Command): Linear_Set[Command] =
    2.20    {
    2.21      val cmds0 = commands.iterator(first, last).toList
    2.22      val blobs_spans0 =
    2.23        syntax.parse_spans(cmds0.iterator.map(_.source).mkString).
    2.24 -        map(span => (Command.resolve_files(resources, syntax, name, span, get_blob), span))
    2.25 +        map(span => (Command.resolve_files(resources, syntax, get_blob, node_name, span), span))
    2.26  
    2.27      val (cmds1, blobs_spans1) = chop_common(cmds0, blobs_spans0)
    2.28  
    2.29 @@ -180,7 +180,7 @@
    2.30          val hook = commands.prev(cmd)
    2.31          val inserted =
    2.32            blobs_spans2.map({ case (blobs, span) =>
    2.33 -            Command(Document_ID.make(), name, Some(blobs), span) })
    2.34 +            Command(Document_ID.make(), node_name, Some(blobs), span) })
    2.35          (commands /: cmds2)(_ - _).append_after(hook, inserted)
    2.36      }
    2.37    }