--- 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()
}