# HG changeset patch
# User wenzelm
# Date 1712071209 -7200
# Node ID 40f5ddeda2b4b9f8ec0fe204aebfe0337d459ffc
# Parent  876bb57e7376bb5fd0b519afeb4b408ddedc073a
further performance tuning (after f906f7f83dae): interactive mode is closer to earlier approach with Lazy.value, which could be relevant with rather complex grammars under tight memory situations;

diff -r 876bb57e7376 -r 40f5ddeda2b4 src/Pure/Concurrent/synchronized.ML
--- a/src/Pure/Concurrent/synchronized.ML	Tue Apr 02 16:33:53 2024 +0200
+++ b/src/Pure/Concurrent/synchronized.ML	Tue Apr 02 17:20:09 2024 +0200
@@ -17,7 +17,7 @@
   type 'a cache
   val cache: (unit -> 'a) -> 'a cache
   val cache_peek: 'a cache -> 'a option
-  val cache_eval: 'a cache -> 'a
+  val cache_eval: {persistent: bool} -> 'a cache -> 'a
 end;
 
 structure Synchronized: SYNCHRONIZED =
@@ -99,24 +99,46 @@
 
 (* cached evaluation via weak_ref *)
 
+local
+
+datatype 'a cache_state =
+    Undef
+  | Value of 'a
+  | Weak_Ref of 'a Unsynchronized.weak_ref;
+
+fun peek Undef = NONE
+  | peek (Value x) = SOME x
+  | peek (Weak_Ref r) = Unsynchronized.weak_peek r;
+
+fun weak_active (Weak_Ref r) = Unsynchronized.weak_active r
+  | weak_active _ = false;
+
+in
+
 abstype 'a cache =
-  Cache of {expr: unit -> 'a, var: 'a Unsynchronized.weak_ref option var}
+  Cache of {expr: unit -> 'a, var: 'a cache_state var}
 with
 
 fun cache expr =
-  Cache {expr = expr, var = var "Synchronized.cache" NONE};
+  Cache {expr = expr, var = var "Synchronized.cache" Undef};
 
-fun cache_peek (Cache {var, ...}) =
-  Option.mapPartial Unsynchronized.weak_peek (value var);
+fun cache_peek (Cache {var, ...}) = peek (value var);
 
-fun cache_eval (Cache {expr, var}) =
+fun cache_eval {persistent} (Cache {expr, var}) =
   change_result var (fn state =>
-    (case Option.mapPartial Unsynchronized.weak_peek state of
-      SOME result => (result, state)
-    | NONE =>
-        let val result = expr ()
-        in (result, SOME (Unsynchronized.weak_ref result)) end));
+    let
+      val result =
+        (case peek state of
+          SOME result => result
+        | NONE => expr ());
+      val state' =
+        if persistent then Value result
+        else if weak_active state then state
+        else Weak_Ref (Unsynchronized.weak_ref result);
+    in (result, state') end);
 
 end;
 
 end;
+
+end;
diff -r 876bb57e7376 -r 40f5ddeda2b4 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Tue Apr 02 16:33:53 2024 +0200
+++ b/src/Pure/Syntax/syntax.ML	Tue Apr 02 17:20:09 2024 +0200
@@ -72,6 +72,8 @@
   val string_of_sort_global: theory -> sort -> string
   val pretty_flexpair: Proof.context -> term * term -> Pretty.T list
   type syntax
+  val cache_persistent: bool Unsynchronized.ref
+  val cache_syntax: syntax -> unit
   val eq_syntax: syntax * syntax -> bool
   datatype approx = Prefix of string | Infix of {assoc: Printer.assoc, delim: string, pri: int}
   val get_approx: syntax -> string -> approx option
@@ -419,6 +421,13 @@
     print_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table,
     prtabs: Printer.prtabs} * stamp;
 
+val cache_persistent = Unsynchronized.ref false;
+
+fun cache_eval (gram: Parser.gram Synchronized.cache) =
+  Synchronized.cache_eval {persistent = ! cache_persistent} gram;
+
+fun cache_syntax (Syntax ({gram, ...}, _)) = ignore (cache_eval gram);
+
 fun eq_syntax (Syntax (_, s1), Syntax (_, s2)) = s1 = s2;
 
 datatype approx = Prefix of string | Infix of {assoc: Printer.assoc, delim: string, pri: int};
@@ -434,7 +443,7 @@
 fun lookup_const (Syntax ({consts, ...}, _)) = Symtab.lookup consts;
 fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode;
 fun tokenize (Syntax ({lexicon, ...}, _)) = Lexicon.tokenize lexicon;
-fun parse (Syntax ({gram, ...}, _)) = Parser.parse (Synchronized.cache_eval gram);
+fun parse (Syntax ({gram, ...}, _)) = Parser.parse (cache_eval gram);
 
 fun parse_ast_translation (Syntax ({parse_ast_trtab, ...}, _)) = lookup_tr parse_ast_trtab;
 fun parse_translation (Syntax ({parse_trtab, ...}, _)) = lookup_tr parse_trtab;
@@ -596,7 +605,7 @@
   in
     [Pretty.block (Pretty.breaks
       (Pretty.str "lexicon:" :: map (Pretty.quote o Pretty.keyword1) (Scan.dest_lexicon lexicon))),
-      Pretty.big_list "productions:" (Parser.pretty_gram (Synchronized.cache_eval gram)),
+      Pretty.big_list "productions:" (Parser.pretty_gram (cache_eval gram)),
       pretty_strs_qs "print modes:" prmodes']
   end;
 
diff -r 876bb57e7376 -r 40f5ddeda2b4 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Tue Apr 02 16:33:53 2024 +0200
+++ b/src/Pure/System/isabelle_process.ML	Tue Apr 02 17:20:09 2024 +0200
@@ -210,12 +210,14 @@
   Printer.show_markup_default := false;
   Context.theory_tracing := Options.default_bool "context_theory_tracing";
   Context.proof_tracing := Options.default_bool "context_proof_tracing";
-  Context.data_timing := Options.default_bool "context_data_timing");
+  Context.data_timing := Options.default_bool "context_data_timing";
+  Syntax.cache_persistent := false);
 
 fun init_options_interactive () =
  (init_options ();
   Multithreading.parallel_proofs := (if Options.default_int "parallel_proofs" > 0 then 3 else 0);
-  Printer.show_markup_default := true);
+  Printer.show_markup_default := true;
+  Syntax.cache_persistent := true);
 
 
 (* generic init *)
diff -r 876bb57e7376 -r 40f5ddeda2b4 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Tue Apr 02 16:33:53 2024 +0200
+++ b/src/Pure/theory.ML	Tue Apr 02 17:20:09 2024 +0200
@@ -201,6 +201,7 @@
       |> Sign.init_naming
       |> Sign.local_path
       |> apply_wrappers wrappers
+      |> tap (Syntax.cache_syntax o Sign.syn_of)
     end;
 
 fun end_theory thy =