changeset 69559 | 66c8dff9639f |
parent 68381 | 2fd3a6d6ba2e |
child 70625 | 1ae987cc052f |
--- a/src/Pure/Thy/thy_syntax.scala Mon Dec 31 13:30:57 2018 +0100 +++ b/src/Pure/Thy/thy_syntax.scala Mon Dec 31 20:08:32 2018 +0100 @@ -301,7 +301,7 @@ { val (syntax_changed, nodes0, doc_edits0) = header_edits(resources, previous, edits) - def get_blob(name: Document.Node.Name) = + def get_blob(name: Document.Node.Name): Option[Document.Blob] = doc_blobs.get(name) orElse previous.nodes(name).get_blob def can_import(name: Document.Node.Name): Boolean =