# HG changeset patch
# User wenzelm
# Date 1546283312 -3600
# Node ID 66c8dff9639f580277fefe5333cb71d2c0303581
# Parent  101ee69cba49e053ca436a50406f31de9cad5d7d
tuned;

diff -r 101ee69cba49 -r 66c8dff9639f src/Pure/Thy/thy_syntax.scala
--- 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 =