src/Pure/Thy/thy_syntax.scala
changeset 59699 a6efad6acafd
parent 59695 a03e0561bdbf
child 59702 58dfaa369c11
     1.1 --- a/src/Pure/Thy/thy_syntax.scala	Sat Mar 14 21:16:29 2015 +0100
     1.2 +++ b/src/Pure/Thy/thy_syntax.scala	Sun Mar 15 12:42:30 2015 +0100
     1.3 @@ -63,7 +63,7 @@
     1.4  
     1.5  
     1.6  
     1.7 -  /** header edits: structure and outer syntax **/
     1.8 +  /** header edits: graph structure and outer syntax **/
     1.9  
    1.10    private def header_edits(
    1.11      resources: Resources,
    1.12 @@ -157,14 +157,14 @@
    1.13      resources: Resources,
    1.14      syntax: Prover.Syntax,
    1.15      get_blob: Document.Node.Name => Option[Document.Blob],
    1.16 -    name: Document.Node.Name,
    1.17 +    node_name: Document.Node.Name,
    1.18      commands: Linear_Set[Command],
    1.19      first: Command, last: Command): Linear_Set[Command] =
    1.20    {
    1.21      val cmds0 = commands.iterator(first, last).toList
    1.22      val blobs_spans0 =
    1.23        syntax.parse_spans(cmds0.iterator.map(_.source).mkString).
    1.24 -        map(span => (Command.resolve_files(resources, syntax, name, span, get_blob), span))
    1.25 +        map(span => (Command.resolve_files(resources, syntax, get_blob, node_name, span), span))
    1.26  
    1.27      val (cmds1, blobs_spans1) = chop_common(cmds0, blobs_spans0)
    1.28  
    1.29 @@ -180,7 +180,7 @@
    1.30          val hook = commands.prev(cmd)
    1.31          val inserted =
    1.32            blobs_spans2.map({ case (blobs, span) =>
    1.33 -            Command(Document_ID.make(), name, Some(blobs), span) })
    1.34 +            Command(Document_ID.make(), node_name, Some(blobs), span) })
    1.35          (commands /: cmds2)(_ - _).append_after(hook, inserted)
    1.36      }
    1.37    }