# HG changeset patch
# User wenzelm
# Date 1753626490 -7200
# Node ID a27841dcd7df44d38714ee40394f58d057ab8926
# Parent  c7e51784a3d553ce62eed7032960d8c5546d579c
more direct support for "command_span" markup property "is_begin";

diff -r c7e51784a3d5 -r a27841dcd7df src/Pure/General/properties.ML
--- a/src/Pure/General/properties.ML	Sun Jul 27 14:58:34 2025 +0200
+++ b/src/Pure/General/properties.ML	Sun Jul 27 16:28:10 2025 +0200
@@ -16,6 +16,7 @@
   val put: entry -> T -> T
   val remove: string -> T -> T
   val make_string: string -> string -> T
+  val make_bool: string -> bool -> T
   val make_int: string -> int -> T
   val get_string: T -> string -> string
   val get_bool: T -> string -> bool
@@ -41,6 +42,7 @@
 fun remove name (props: T) = AList.delete (op =) name props;
 
 fun make_string k s = if s = "" then [] else [(k, s)];
+fun make_bool k b = if not b then [] else [(k, Value.print_bool b)];
 fun make_int k i = if i = 0 then [] else [(k, Value.print_int i)];
 
 val get_string = the_default "" oo get;
diff -r c7e51784a3d5 -r a27841dcd7df src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Sun Jul 27 14:58:34 2025 +0200
+++ b/src/Pure/Isar/token.ML	Sun Jul 27 16:28:10 2025 +0200
@@ -54,6 +54,7 @@
   val is_formal_comment: T -> bool
   val is_document_marker: T -> bool
   val is_ignored: T -> bool
+  val is_begin: T -> bool
   val is_begin_ignore: T -> bool
   val is_end_ignore: T -> bool
   val is_error: T -> bool
@@ -276,6 +277,9 @@
 fun is_document_marker (Token (_, (Comment (SOME Comment.Marker), _), _)) = true
   | is_document_marker _ = false;
 
+fun is_begin (Token (_, (Keyword, "begin"), _)) = true
+  | is_begin _ = false;
+
 fun is_begin_ignore (Token (_, (Comment NONE, "<"), _)) = true
   | is_begin_ignore _ = false;
 
diff -r c7e51784a3d5 -r a27841dcd7df src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Sun Jul 27 14:58:34 2025 +0200
+++ b/src/Pure/PIDE/command.ML	Sun Jul 27 16:28:10 2025 +0200
@@ -127,7 +127,8 @@
         let
           val name = Toplevel.name_of tr;
           val kind = the_default "" (Keyword.command_kind (Thy_Header.get_keywords thy) name);
-          val markup = Markup.command_span {name = name, kind = kind};
+          val is_begin = exists Token.is_begin span;
+          val markup = Markup.command_span {name = name, kind = kind, is_begin = is_begin};
         in Position.report (#1 core_range) markup end;
   in tr end;
 
diff -r c7e51784a3d5 -r a27841dcd7df src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sun Jul 27 14:58:34 2025 +0200
+++ b/src/Pure/PIDE/document.scala	Sun Jul 27 16:28:10 2025 +0200
@@ -812,6 +812,17 @@
       for (case Text.Info(r, Some(x)) <- cumulate(range, None, elements, result1, status))
         yield Text.Info(r, x)
     }
+
+
+    /* command spans --- according to PIDE markup */
+
+    def command_spans(range: Text.Range): List[Text.Info[Markup.Command_Span.Arg]] =
+      select(range, Markup.Elements(Markup.COMMAND_SPAN), _ =>
+        {
+          case Text.Info(range, XML.Elem(Markup.Command_Span(arg), _)) =>
+            Some(Text.Info(range, arg))
+          case _ => None
+        }).map(_.info)
   }
 
 
diff -r c7e51784a3d5 -r a27841dcd7df src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Sun Jul 27 14:58:34 2025 +0200
+++ b/src/Pure/PIDE/markup.ML	Sun Jul 27 16:28:10 2025 +0200
@@ -182,7 +182,7 @@
   val descriptionN: string
   val inputN: string val input: bool -> Properties.T -> T
   val command_keywordN: string val command_keyword: T
-  val command_spanN: string val command_span: {name: string, kind: string} -> T
+  val command_spanN: string val command_span: {name: string, kind: string, is_begin: bool} -> T
   val commandN: string val command_properties: T -> T
   val keywordN: string val keyword_properties: T -> T
   val stringN: string val string: T
@@ -659,8 +659,10 @@
 
 val (command_keywordN, command_keyword) = markup_elem "command_keyword";
 
+val is_beginN = "is_begin";
 val command_spanN = "command_span";
-fun command_span {name, kind} : T = (command_spanN, name_proper name @ kind_proper kind);
+fun command_span {name, kind, is_begin} : T =
+  (command_spanN, name_proper name @ kind_proper kind @ Properties.make_bool is_beginN is_begin);
 
 val commandN = "command"; val command_properties = properties [(kindN, commandN)];
 val keywordN = "keyword"; val keyword_properties = properties [(kindN, keywordN)];
diff -r c7e51784a3d5 -r a27841dcd7df src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Sun Jul 27 14:58:34 2025 +0200
+++ b/src/Pure/PIDE/markup.scala	Sun Jul 27 16:28:10 2025 +0200
@@ -443,18 +443,23 @@
 
   val COMMAND_SPAN = "command_span"
   object Command_Span {
-    sealed case class Arg(name: String, kind: String) {
+    val Is_Begin = new Properties.Boolean("is_begin")
+
+    sealed case class Arg(name: String, kind: String, is_begin: Boolean) {
       def properties: Properties.T =
         (if (name.isEmpty) Nil else Name(name)) :::
-        (if (kind.isEmpty) Nil else Kind(kind))
+        (if (kind.isEmpty) Nil else Kind(kind)) :::
+        (if (!is_begin) Nil else Is_Begin(is_begin))
     }
 
     def apply(arg: Arg): Markup = Markup(COMMAND_SPAN, arg.properties)
-    def apply(name: String, kind: String): Markup = apply(Arg(name, kind))
+    def apply(name: String, kind: String, is_begin: Boolean): Markup =
+      apply(Arg(name, kind, is_begin))
 
     def unapply(markup: Markup): Option[Arg] =
       if (markup.name == COMMAND_SPAN) {
-        Some(Arg(Name.get(markup.properties), Kind.get(markup.properties)))
+        val props = markup.properties
+        Some(Arg(Name.get(props), Kind.get(props), Is_Begin.get(props)))
       }
       else None
   }
diff -r c7e51784a3d5 -r a27841dcd7df src/Tools/Find_Facts/src/thy_blocks.scala
--- a/src/Tools/Find_Facts/src/thy_blocks.scala	Sun Jul 27 14:58:34 2025 +0200
+++ b/src/Tools/Find_Facts/src/thy_blocks.scala	Sun Jul 27 16:28:10 2025 +0200
@@ -13,36 +13,11 @@
 object Thy_Blocks {
   /** spans **/
 
-  val keyword_elements =
-    Markup.Elements(Markup.KEYWORD, Markup.KEYWORD1, Markup.KEYWORD2, Markup.KEYWORD3)
-
-  object Span {
-    def read_build(snapshot: Document.Snapshot): List[Span] = {
-      def is_begin(markup: Text.Markup): Boolean = markup.info match {
-        case XML.Elem(Markup(_, Markup.Kind(Markup.KEYWORD)), Nil) =>
-          XML.content(snapshot.xml_markup(markup.range)) == "begin"
-        case _ => false
-      }
-
-      def has_begin(range: Text.Range): Boolean =
-        snapshot
-          .select(range, keyword_elements, _ => markup => Some(is_begin(markup)))
-          .exists(_.info)
-
-      snapshot.select(Text.Range.full, Markup.Elements(Markup.COMMAND_SPAN), _ =>
-        {
-          case Text.Info(range, XML.Elem(Markup.Command_Span(arg), _)) =>
-            Some(Span(range, arg.name, arg.kind, has_begin(range)))
-          case _ => None
-        }).map(_.info)
-    }
-  }
-
   case class Span(
     override val range: Text.Range,
     override val command: String,
     kind: String,
-    has_begin: Boolean
+    is_begin: Boolean
   ) extends Block {
     def spans: List[Span] = List(this)
 
@@ -114,7 +89,7 @@
           case Some(_) if span.is_of_kind(Keyword.diag) => blocks.add(span)
           case Some(Thy(_)) if span.is_of_kind(Keyword.theory_goal) => blocks.push(Prf(List(span)))
           case Some(Thy(_)) if span.is_of_kind(Keyword.theory_block) =>
-            (if (span.has_begin) blocks.push else blocks.add)(Decl(List(span)))
+            (if (span.is_begin) blocks.push else blocks.add)(Decl(List(span)))
           case Some(Thy(_)) if span.is_of_kind(Keyword.theory_end) => blocks.add(span).pop
           case Some(Thy(_)) if span.is_of_kind(Keyword.theory_body) => blocks.add(span)
           case Some(Prf(_)) if span.is_of_kind(Keyword.proof_open) => blocks.push(Prf(List(span)))
@@ -125,7 +100,7 @@
           case Some(Decl(_)) if span.is_of_kind(Keyword.proof_body) => blocks.add(span)
           case Some(Decl(_)) if span.is_of_kind(Keyword.theory_goal) => blocks.push(Prf(List(span)))
           case Some(Decl(_)) if span.is_of_kind(Keyword.theory_block) =>
-            (if (span.has_begin) blocks.push else blocks.add)(Decl(List(span)))
+            (if (span.is_begin) blocks.push else blocks.add)(Decl(List(span)))
           case Some(Decl(_)) if span.is_of_kind(Keyword.theory_end) => blocks.add(span).pop
           case Some(Decl(_)) if span.is_of_kind(Keyword.theory_body) => blocks.add(span)
           case e => error("Unexpected span " + span + " at " + e)
@@ -135,6 +110,10 @@
     }
   }
 
-  def read_blocks(snapshot: Document.Snapshot): List[Block] =
-    Parser.parse(Span.read_build(snapshot))
+  def read_blocks(snapshot: Document.Snapshot): List[Block] = {
+    val spans =
+      for (Text.Info(range, arg) <- snapshot.command_spans(Text.Range.full))
+        yield Span(range, arg.name, arg.kind, arg.is_begin)
+    Parser.parse(spans)
+  }
 }