# HG changeset patch
# User wenzelm
# Date 1672935269 -3600
# Node ID 1bc50ffad6d23fa1f66c70222b45d80e0d8d01f1
# Parent  a8eb5046b05f7e1f71ccf71cf3e15033e0915d0a
tuned signature;

diff -r a8eb5046b05f -r 1bc50ffad6d2 src/Pure/Isar/document_structure.scala
--- 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()
   }
diff -r a8eb5046b05f -r 1bc50ffad6d2 src/Pure/PIDE/command.scala
--- 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 = {
diff -r a8eb5046b05f -r 1bc50ffad6d2 src/Pure/PIDE/session.scala
--- 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