--- a/src/Pure/Isar/document_structure.scala Thu Jan 05 17:00:22 2023 +0100
+++ b/src/Pure/Isar/document_structure.scala Thu Jan 05 17:14:29 2023 +0100
@@ -99,7 +99,7 @@
/* result structure */
val spans = syntax.parse_spans(text)
- spans.foreach(span => add(Command(Document_ID.none, node_name, Command.Blobs_Info.none, span)))
+ spans.foreach(span => add(Command(Document_ID.none, node_name, Command.Blobs_Info.empty, span)))
result()
}
@@ -166,7 +166,7 @@
for { span <- syntax.parse_spans(text) } {
sections.add(
new Command_Item(syntax.keywords,
- Command(Document_ID.none, node_name, Command.Blobs_Info.none, span)))
+ Command(Document_ID.none, node_name, Command.Blobs_Info.empty, span)))
}
sections.result()
}
--- a/src/Pure/PIDE/command.scala Thu Jan 05 17:00:22 2023 +0100
+++ b/src/Pure/PIDE/command.scala Thu Jan 05 17:14:29 2023 +0100
@@ -24,10 +24,10 @@
}
object Blobs_Info {
- val none: Blobs_Info = Blobs_Info(Nil)
+ val empty: Blobs_Info = Blobs_Info(Nil)
def make(blobs: List[(Blob, Document.Blobs.Item)]): Blobs_Info =
- if (blobs.isEmpty) none else Blobs_Info(for ((a, _) <- blobs) yield Exn.Res(a))
+ if (blobs.isEmpty) empty else Blobs_Info(for ((a, _) <- blobs) yield Exn.Res(a))
def errors(msgs: List[String]): Blobs_Info =
Blobs_Info(msgs.map(msg => Exn.Exn[Blob](ERROR(msg))))
@@ -371,14 +371,14 @@
}
val empty: Command =
- Command(Document_ID.none, Document.Node.Name.empty, Blobs_Info.none, Command_Span.empty)
+ Command(Document_ID.none, Document.Node.Name.empty, Blobs_Info.empty, Command_Span.empty)
def unparsed(
source: String,
theory: Boolean = false,
id: Document_ID.Command = Document_ID.none,
node_name: Document.Node.Name = Document.Node.Name.empty,
- blobs_info: Blobs_Info = Blobs_Info.none,
+ blobs_info: Blobs_Info = Blobs_Info.empty,
results: Results = Results.empty,
markups: Markups = Markups.empty
): Command = {
--- a/src/Pure/PIDE/session.scala Thu Jan 05 17:00:22 2023 +0100
+++ b/src/Pure/PIDE/session.scala Thu Jan 05 17:14:29 2023 +0100
@@ -125,7 +125,7 @@
val cache: Term.Cache = Term.Cache.make()
- def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info = Command.Blobs_Info.none
+ def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info = Command.Blobs_Info.empty
def build_blobs(name: Document.Node.Name): Document.Blobs = Document.Blobs.empty