src/Pure/Thy/thy_syntax.scala
changeset 68381 2fd3a6d6ba2e
parent 68336 09ac56914b29
child 69559 66c8dff9639f
equal deleted inserted replaced
68380:f249e1f5623b 68381:2fd3a6d6ba2e
   295       resources: Resources,
   295       resources: Resources,
   296       reparse_limit: Int,
   296       reparse_limit: Int,
   297       previous: Document.Version,
   297       previous: Document.Version,
   298       doc_blobs: Document.Blobs,
   298       doc_blobs: Document.Blobs,
   299       edits: List[Document.Edit_Text],
   299       edits: List[Document.Edit_Text],
   300       consolidate: Boolean): Session.Change =
   300       consolidate: List[Document.Node.Name]): Session.Change =
   301   {
   301   {
   302     val (syntax_changed, nodes0, doc_edits0) = header_edits(resources, previous, edits)
   302     val (syntax_changed, nodes0, doc_edits0) = header_edits(resources, previous, edits)
   303 
   303 
   304     def get_blob(name: Document.Node.Name) =
   304     def get_blob(name: Document.Node.Name) =
   305       doc_blobs.get(name) orElse previous.nodes(name).get_blob
   305       doc_blobs.get(name) orElse previous.nodes(name).get_blob