more generic parsing of command spans;
support for Thy_Info.get_theories_elements;

--- a/NEWS	Sun Jun 01 15:35:28 2025 +0200
+++ b/NEWS	Sun Jun 01 16:43:09 2025 +0200
@@ -263,7 +263,8 @@
 * System option "record_theories" tells "isabelle build" to record
 intermediate theory commands and results, at the cost of approx. 5 times
 larger ML heap images. This allows to retrieve fine-grained semantic
-information later on, using Thy_Info.get_theory_segments in Isabelle/ML.
+information later on, using Thy_Info.get_theory_segments or
+Thy_Info.get_theory_elements in Isabelle/ML.
 
 * The Z Garbage Collector (ZGC) of Java 21 is now used by default (see
 also https://wiki.openjdk.org/display/zgc). This should work uniformly

--- a/src/Pure/PIDE/command_span.ML	Sun Jun 01 15:35:28 2025 +0200
+++ b/src/Pure/PIDE/command_span.ML	Sun Jun 01 16:43:09 2025 +0200
@@ -12,6 +12,9 @@
   val kind: span -> kind
   val content: span -> Token.T list
   val symbol_length: span -> int option
+  val eof: span
+  val is_eof: span -> bool
+  val stopper: span Scan.stopper
   val adjust_offsets_kind: (int -> int option) -> kind -> kind
   val adjust_offsets: (int -> int option) -> span -> span
 end;
@@ -34,6 +37,16 @@
 val symbol_length = Position.distance_of o Token.range_of o content;
 
 
+(* stopper *)
+
+val eof = Span (Command_Span ("", Position.none), []);
+
+fun is_eof (Span (Command_Span ("", _), _)) = true
+  | is_eof _ = false;
+
+val stopper = Scan.stopper (K eof) is_eof;
+
+
 (* presentation positions *)
 
 fun adjust_offsets_kind adjust k =

--- a/src/Pure/Thy/document_output.ML	Sun Jun 01 15:35:28 2025 +0200
+++ b/src/Pure/Thy/document_output.ML	Sun Jun 01 16:43:09 2025 +0200
@@ -16,6 +16,8 @@
   type segment =
     {span: Command_Span.span, command: Toplevel.transition,
      prev_state: Toplevel.state, state: Toplevel.state}
+  val segment_eof: segment
+  val segment_stopper: segment Scan.stopper
   val present_thy: Options.T -> Keyword.keywords -> string -> segment list -> Latex.text
   val pretty_term: Proof.context -> term -> Pretty.T
   val pretty_thm: Proof.context -> thm -> Pretty.T
@@ -371,6 +373,14 @@
   {span: Command_Span.span, command: Toplevel.transition,
    prev_state: Toplevel.state, state: Toplevel.state};
 
+val segment_eof: segment =
+  {span = Command_Span.eof, command = Toplevel.empty,
+   prev_state = Toplevel.make_state NONE, state = Toplevel.make_state NONE};
+
+val segment_stopper =
+  Scan.stopper (K segment_eof) (Command_Span.is_eof o #span);
+
+
 local
 
 val markup_true = "\\isamarkuptrue%\n";

--- a/src/Pure/Thy/thy_element.ML	Sun Jun 01 15:35:28 2025 +0200
+++ b/src/Pure/Thy/thy_element.ML	Sun Jun 01 16:43:09 2025 +0200
@@ -11,6 +11,8 @@
   val map_element: ('a -> 'b) -> 'a element -> 'b element
   val flat_element: 'a element -> 'a list
   val last_element: 'a element -> 'a
+  val parse_elements_generic: Keyword.keywords -> ('a -> Command_Span.span) -> 'a Scan.stopper ->
+    'a list -> 'a element list
   val parse_elements: Keyword.keywords -> Command_Span.span list -> Command_Span.span element list
 end;
 
@@ -35,29 +37,18 @@
   | last_element (Element (_, SOME (_, b))) = b;
 
 
-(* scanning spans *)
-
-val eof = Command_Span.Span (Command_Span.Command_Span ("", Position.none), []);
-
-fun is_eof (Command_Span.Span (Command_Span.Command_Span ("", _), _)) = true
-  | is_eof _ = false;
-
-val not_eof = not o is_eof;
-
-val stopper = Scan.stopper (K eof) is_eof;
-
 
 (* parse *)
 
-local
+fun parse_elements_generic keywords get_span stopper =
+  let
+    val not_eof = not o Scan.is_stopper stopper;
 
-fun parse_element keywords =
-  let
     fun category pred other =
-      Scan.one
-        (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) =>
-            pred keywords name
-          | _ => other);
+      Scan.one (fn x =>
+        (case get_span x of
+          Command_Span.Span (Command_Span.Command_Span (name, _), _) => pred keywords name
+        | _ => other));
 
     fun theory_element x =
       (category Keyword.is_theory_goal false -- proof >> element) x
@@ -67,15 +58,15 @@
     and proof x = (Scan.repeat proof_element -- category Keyword.is_qed false) x;
 
     val default_element = Scan.one not_eof >> atom;
-  in theory_element || default_element end;
 
-in
+    val parse_element = theory_element || default_element
+  in
+    Source.of_list #>
+    Source.source stopper (Scan.bulk parse_element) #>
+    Source.exhaust
+  end;
 
 fun parse_elements keywords =
-  Source.of_list #>
-  Source.source stopper (Scan.bulk (parse_element keywords)) #>
-  Source.exhaust;
+  parse_elements_generic keywords I Command_Span.stopper;
 
 end;
-
-end;

--- a/src/Pure/Thy/thy_info.ML	Sun Jun 01 15:35:28 2025 +0200
+++ b/src/Pure/Thy/thy_info.ML	Sun Jun 01 16:43:09 2025 +0200
@@ -18,6 +18,7 @@
   val defined_theory: string -> bool
   val get_theory: string -> theory
   val get_theory_segments: string -> Document_Output.segment list
+  val get_theory_elements: string -> Document_Output.segment Thy_Element.element list
   val check_theory: Proof.context -> string * Position.T -> theory
   val master_directory: string -> Path.T
   val remove_thy: string -> unit
@@ -164,6 +165,14 @@
     else segments
   end;
 
+fun get_theory_elements name =
+  let
+    val theory = get_theory name;
+    val keywords = Thy_Header.get_keywords theory;
+    val stopper = Document_Output.segment_stopper;
+    val segments = get_theory_segments name;
+  in Thy_Element.parse_elements_generic keywords #span stopper segments end;
+
 
 val get_imports = Resources.imports_of o get_theory;