# HG changeset patch
# User wenzelm
# Date 1753627594 -7200
# Node ID f7778350d1ac42dcd0da7a3b76571d066a81f36b
# Parent  f7db39778e549d09a798209bcc4fc5f31a9b0c24
clarified signature;

diff -r f7db39778e54 -r f7778350d1ac src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sun Jul 27 16:41:25 2025 +0200
+++ b/src/Pure/PIDE/document.scala	Sun Jul 27 16:46:34 2025 +0200
@@ -816,7 +816,7 @@
 
     /* command spans --- according to PIDE markup */
 
-    def command_spans(range: Text.Range): List[Text.Info[Markup.Command_Span.Args]] =
+    def command_spans(range: Text.Range = Text.Range.full): List[Text.Info[Markup.Command_Span.Args]] =
       select(range, Markup.Elements(Markup.COMMAND_SPAN), _ =>
         {
           case Text.Info(range, XML.Elem(Markup.Command_Span(args), _)) =>
diff -r f7db39778e54 -r f7778350d1ac src/Tools/Find_Facts/src/thy_blocks.scala
--- a/src/Tools/Find_Facts/src/thy_blocks.scala	Sun Jul 27 16:41:25 2025 +0200
+++ b/src/Tools/Find_Facts/src/thy_blocks.scala	Sun Jul 27 16:46:34 2025 +0200
@@ -112,7 +112,7 @@
 
   def read_blocks(snapshot: Document.Snapshot): List[Block] = {
     val spans =
-      for (Text.Info(range, arg) <- snapshot.command_spans(Text.Range.full))
+      for (Text.Info(range, arg) <- snapshot.command_spans())
         yield Span(range, arg.name, arg.kind, arg.is_begin)
     Parser.parse(spans)
   }