--- 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), _)) =>
--- 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)
}