# HG changeset patch
# User wenzelm
# Date 1748784635 -7200
# Node ID c603d41dc183b84edcb6b94180c6150cfd917dfa
# Parent  33dba4986b9ff5a91268a56eab8e209934bddce0
support for Thy_Info.get_theories_segments, depending on system option "record_theories";

diff -r 33dba4986b9f -r c603d41dc183 NEWS
--- a/NEWS	Sun Jun 01 13:12:43 2025 +0200
+++ b/NEWS	Sun Jun 01 15:30:35 2025 +0200
@@ -260,6 +260,11 @@
 
 *** System ***
 
+* 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.
+
 * 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
 on all platforms, but requires a reasonably new version of Windows
diff -r 33dba4986b9f -r c603d41dc183 etc/options
--- a/etc/options	Sun Jun 01 13:12:43 2025 +0200
+++ b/etc/options	Sun Jun 01 15:30:35 2025 +0200
@@ -121,7 +121,10 @@
   -- "tracing of persistent Proof.context values within ML heap"
 
 
-section "Detail of Proof Checking"
+section "Detail of Theory and Proof Processing"
+
+option record_theories : bool = false for content
+  -- "record intermediate theory commands and results"
 
 option record_proofs : int = -1 for content
   -- "set level of proofterm recording: 0, 1, 2, negative means unchanged"
diff -r 33dba4986b9f -r c603d41dc183 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sun Jun 01 13:12:43 2025 +0200
+++ b/src/Pure/Thy/thy_info.ML	Sun Jun 01 15:30:35 2025 +0200
@@ -17,6 +17,7 @@
   val lookup_theory: string -> theory option
   val defined_theory: string -> bool
   val get_theory: string -> theory
+  val get_theory_segments: string -> Document_Output.segment list
   val check_theory: Proof.context -> string * Position.T -> theory
   val master_directory: string -> Path.T
   val remove_thy: string -> unit
@@ -105,9 +106,8 @@
   the_default Path.current (Option.map (Path.dir o #1 o #master) d);
 
 local
-  val global_thys =
-    Synchronized.var "Thy_Info.thys"
-      (String_Graph.empty: (deps option * theory option) String_Graph.T);
+  type thy = deps option * (theory * Document_Output.segment list) option;
+  val global_thys = Synchronized.var "Thy_Info.thys" (String_Graph.empty: thy String_Graph.T);
 in
   fun get_thys () = Synchronized.value global_thys;
   fun change_thys f = Synchronized.change global_thys f;
@@ -140,7 +140,7 @@
 
 fun lookup_theory name =
   (case lookup_thy name of
-    SOME (_, SOME theory) => SOME theory
+    SOME (_, SOME (theory, _)) => SOME theory
   | _ => NONE);
 
 val defined_theory = is_some o lookup_theory;
@@ -150,6 +150,21 @@
     SOME theory => theory
   | _ => error ("Theory loader: undefined entry for theory " ^ quote name));
 
+fun get_theory_segments name =
+  let
+    val _ = get_theory name;
+    val segments =
+      (case lookup_thy name of
+        SOME (_, SOME (_, segments)) => segments
+      | _ => []);
+  in
+    if null segments then
+      error ("Theory loader: no theory segments for theory " ^ quote name ^
+        "\n Need to build with option " ^ quote \<^system_option>\<open>record_theories\<close>)
+    else segments
+  end;
+
+
 val get_imports = Resources.imports_of o get_theory;
 
 val check_theory = Theory.check_theory {get = get_theory, all = get_names};
@@ -175,16 +190,16 @@
 
 (* update *)
 
-fun update deps theory thys =
+fun update deps (res as (theory, _)) thys =
   let
     val name = Context.theory_long_name theory;
     val parents = map Context.theory_long_name (Theory.parents_of theory);
 
     val thys' = remove name thys;
     val _ = map (get thys') parents;
-  in new_entry name parents (SOME deps, SOME theory) thys' end;
+  in new_entry name parents (SOME deps, SOME res) thys' end;
 
-fun update_thy deps theory = change_thys (update deps theory);
+fun update_thy deps res = change_thys (update deps res);
 
 
 (* scheduling loader tasks *)
@@ -194,14 +209,14 @@
    {theory: theory,
     exec_id: Document_ID.exec,
     present: unit -> presentation_context option,
-    commit: unit -> unit};
+    commit: Document_Output.segment list -> unit};
 
 fun theory_result theory =
   Result
    {theory = theory,
     exec_id = Document_ID.none,
     present = K NONE,
-    commit = I};
+    commit = K ()};
 
 fun result_theory (Result {theory, ...}) = theory;
 fun result_commit (Result {commit, ...}) = commit;
@@ -220,12 +235,10 @@
         val exns = maps Task_Queue.group_status (Execution.peek exec_id);
       in result :: map Exn.Exn exns end;
 
-fun present_theory (Exn.Exn exn) = [Exn.Exn exn]
+fun present_theory (Exn.Exn exn) = SOME (Exn.Exn exn)
   | present_theory (Exn.Res (Result {theory, present, ...})) =
-      (case present () of
-        NONE => []
-      | SOME (context as {segments, ...}) =>
-          [Exn.capture_body (fn () => (apply_presentation context theory; (theory, segments)))]);
+      present () |> Option.map (fn context as {segments, ...} =>
+        Exn.capture_body (fn () => (apply_presentation context theory; (theory, segments))));
 
 in
 
@@ -252,11 +265,14 @@
 
     val results1 = futures |> maps (consolidate_theory o Future.join_result);
 
-    val present_results = futures |> maps (present_theory o Future.join_result);
+    val presented_results = futures |> map (present_theory o Future.join_result);
+    val present_results = map_filter I presented_results;
+
     val results2 = (map o Exn.map_res) (K ()) present_results;
 
-    val results3 = futures
-      |> map (fn future => Exn.capture_body (fn () => result_commit (Future.join future) ()));
+    val results3 = (futures, presented_results) |> ListPair.map (fn (future, presented) =>
+      let val segments = (case presented of SOME (Exn.Res (_, segments)) => segments | _ => []);
+      in Exn.capture_body (fn () => result_commit (Future.join future) segments) end);
 
     val results4 = map Exn.Exn (maps Task_Queue.group_status (Execution.reset ()));
 
@@ -357,7 +373,9 @@
     val timing_props = [Markup.theory_timing, (Markup.nameN, name)];
     val _ = Output.try_protocol_message (timing_props @ Markup.timing_properties timing_result) []
 
-    fun commit () = update_thy deps theory;
+    fun commit segments =
+      update_thy deps (theory,
+        if Options.bool options \<^system_option>\<open>record_theories\<close> then segments else []);
   in Result {theory = theory, exec_id = exec_id, present = SOME o present, commit = commit} end;
 
 fun check_thy_deps dir name =
@@ -456,7 +474,7 @@
       let
         val thys' = remove name thys;
         val _ = writeln ("Registering theory " ^ quote name);
-      in update (make_deps master imports) theory thys' end)
+      in update (make_deps master imports) (theory, []) thys' end)
   end;