src/Pure/Isar/document_structure.scala
changeset 72814 51eec6d51882
parent 71165 03afc8252225
child 73340 0ffcad1f6130
--- a/src/Pure/Isar/document_structure.scala	Wed Dec 02 10:30:59 2020 +0100
+++ b/src/Pure/Isar/document_structure.scala	Wed Dec 02 15:01:37 2020 +0100
@@ -101,7 +101,7 @@
     /* result structure */
 
     val spans = syntax.parse_spans(text)
-    spans.foreach(span => add(Command(Document_ID.none, node_name, Command.no_blobs, span)))
+    spans.foreach(span => add(Command(Document_ID.none, node_name, Command.Blobs_Info.none, span)))
     result()
   }
 
@@ -174,7 +174,7 @@
     for { span <- syntax.parse_spans(text) } {
       sections.add(
         new Command_Item(syntax.keywords,
-          Command(Document_ID.none, node_name, Command.no_blobs, span)))
+          Command(Document_ID.none, node_name, Command.Blobs_Info.none, span)))
     }
     sections.result()
   }