# HG changeset patch
# User wenzelm
# Date 1712078335 -7200
# Node ID d67cacd09251bc76a53398f98ef2d69d0b50875d
# Parent  33a9b1d6a651cdd6708b726cccfcab371a0dd330# Parent  09e9819beef62f806defc72f995356092015fb06
merged

diff -r 33a9b1d6a651 -r d67cacd09251 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Tue Apr 02 18:02:43 2024 +0200
+++ b/Admin/components/components.sha1	Tue Apr 02 19:18:55 2024 +0200
@@ -511,6 +511,7 @@
 423df2c437f7cceac1d269da8e379507feb246ef stack-2.13.1.tar.gz
 fdfea3b1c6b02612b1d50decb20b1a27ae741629 stack-2.15.1.tar.gz
 6fd65aac9147ba93fa3356fa629f6911d82d767b stack-2.15.3.tar.gz
+937a061f638823805ebc561b22465198f0ff1670 stack-2.15.5.tar.gz
 ebd0221d038966aa8bde075f1b0189ff867b02ca stack-2.5.1.tar.gz
 fa2d882ec45cbc8c7d2f3838b705a8316696dc66 stack-2.7.3.tar.gz
 18437bc9abd5b95be31a96f7c15a85a3ebf466cf stack-2.9.3.tar.gz
diff -r 33a9b1d6a651 -r d67cacd09251 Admin/components/main
--- a/Admin/components/main	Tue Apr 02 18:02:43 2024 +0200
+++ b/Admin/components/main	Tue Apr 02 19:18:55 2024 +0200
@@ -34,7 +34,7 @@
 smbc-0.4.1
 spass-3.8ds-2
 sqlite-3.45.2.0
-stack-2.15.3
+stack-2.15.5
 vampire-4.8
 verit-2021.06.2-rmx-1
 vscode_extension-20230206
diff -r 33a9b1d6a651 -r d67cacd09251 etc/settings
--- a/etc/settings	Tue Apr 02 18:02:43 2024 +0200
+++ b/etc/settings	Tue Apr 02 19:18:55 2024 +0200
@@ -173,7 +173,7 @@
 
 ISABELLE_STACK_ROOT="$USER_HOME/.stack"
 
-ISABELLE_STACK_RESOLVER="lts-22.13"
+ISABELLE_STACK_RESOLVER="lts-22.15"
 
 ISABELLE_GHC_VERSION="ghc-9.6.4"
 
diff -r 33a9b1d6a651 -r d67cacd09251 src/Pure/Admin/component_stack.scala
--- a/src/Pure/Admin/component_stack.scala	Tue Apr 02 18:02:43 2024 +0200
+++ b/src/Pure/Admin/component_stack.scala	Tue Apr 02 19:18:55 2024 +0200
@@ -29,7 +29,7 @@
   /* build stack */
 
   val default_url = "https://github.com/commercialhaskell/stack/releases/download"
-  val default_version = "2.15.3"
+  val default_version = "2.15.5"
 
   def build_stack(
     base_url: String = default_url,
diff -r 33a9b1d6a651 -r d67cacd09251 src/Pure/Build/export_theory.ML
--- a/src/Pure/Build/export_theory.ML	Tue Apr 02 18:02:43 2024 +0200
+++ b/src/Pure/Build/export_theory.ML	Tue Apr 02 19:18:55 2024 +0200
@@ -38,7 +38,7 @@
 
 (* approximative syntax *)
 
-val get_syntax = Syntax.get_approx o Proof_Context.syn_of;
+val get_syntax = Syntax.get_approx o Proof_Context.syntax_of;
 fun get_syntax_type ctxt = get_syntax ctxt o Lexicon.mark_type;
 fun get_syntax_const ctxt = get_syntax ctxt o Lexicon.mark_const;
 fun get_syntax_fixed ctxt = get_syntax ctxt o Lexicon.mark_fixed;
diff -r 33a9b1d6a651 -r d67cacd09251 src/Pure/Concurrent/synchronized.ML
--- a/src/Pure/Concurrent/synchronized.ML	Tue Apr 02 18:02:43 2024 +0200
+++ b/src/Pure/Concurrent/synchronized.ML	Tue Apr 02 19:18:55 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 33a9b1d6a651 -r d67cacd09251 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Apr 02 18:02:43 2024 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Apr 02 19:18:55 2024 +0200
@@ -20,7 +20,7 @@
   val get_mode: Proof.context -> mode
   val restore_mode: Proof.context -> Proof.context -> Proof.context
   val abbrev_mode: Proof.context -> bool
-  val syn_of: Proof.context -> Syntax.syntax
+  val syntax_of: Proof.context -> Syntax.syntax
   val tsig_of: Proof.context -> Type.tsig
   val set_defsort: sort -> Proof.context -> Proof.context
   val default_sort: Proof.context -> indexname -> sort
@@ -312,10 +312,9 @@
 val restore_mode = set_mode o get_mode;
 val abbrev_mode = get_mode #> (fn Mode {abbrev, ...} => abbrev);
 
-val syntax_of = #syntax o rep_data;
-val syn_of = Local_Syntax.syn_of o syntax_of;
+val syntax_of = Local_Syntax.syntax_of o #syntax o rep_data;
 val set_syntax_mode = map_syntax o Local_Syntax.set_mode;
-val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o syntax_of;
+val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o #syntax o rep_data;
 
 val tsig_of = #1 o #tsig o rep_data;
 val set_defsort = map_tsig o apfst o Type.set_defsort;
@@ -1124,7 +1123,7 @@
 (* syntax *)
 
 fun check_syntax_const ctxt (c, pos) =
-  if is_some (Syntax.lookup_const (syn_of ctxt) c) then c
+  if is_some (Syntax.lookup_const (syntax_of ctxt) c) then c
   else error ("Unknown syntax const: " ^ quote c ^ Position.here pos);
 
 fun syntax add mode args ctxt =
@@ -1438,7 +1437,7 @@
 
 (* local syntax *)
 
-val print_syntax = Syntax.print_syntax o syn_of;
+val print_syntax = Syntax.print_syntax o syntax_of;
 
 
 (* abbreviations *)
diff -r 33a9b1d6a651 -r d67cacd09251 src/Pure/Syntax/local_syntax.ML
--- a/src/Pure/Syntax/local_syntax.ML	Tue Apr 02 18:02:43 2024 +0200
+++ b/src/Pure/Syntax/local_syntax.ML	Tue Apr 02 19:18:55 2024 +0200
@@ -8,7 +8,7 @@
 signature LOCAL_SYNTAX =
 sig
   type T
-  val syn_of: T -> Syntax.syntax
+  val syntax_of: T -> Syntax.syntax
   val init: theory -> T
   val rebuild: theory -> T -> T
   datatype kind = Type | Const | Fixed
@@ -43,16 +43,16 @@
   make_syntax (f (thy_syntax, local_syntax, mode, mixfixes));
 
 fun is_consistent thy (Syntax {thy_syntax, ...}) =
-  Syntax.eq_syntax (Sign.syn_of thy, thy_syntax);
+  Syntax.eq_syntax (Sign.syntax_of thy, thy_syntax);
 
-fun syn_of (Syntax {local_syntax, ...}) = local_syntax;
+fun syntax_of (Syntax {local_syntax, ...}) = local_syntax;
 
 
 (* build syntax *)
 
 fun build_syntax thy mode mixfixes =
   let
-    val thy_syntax = Sign.syn_of thy;
+    val thy_syntax = Sign.syntax_of thy;
     fun update_gram ((true, add, m), decls) = Syntax.update_type_gram add m decls
       | update_gram ((false, add, m), decls) =
           Syntax.update_const_gram add (Sign.logical_types thy) m decls;
@@ -62,7 +62,7 @@
   in make_syntax (thy_syntax, local_syntax, mode, mixfixes) end;
 
 fun init thy =
-  let val thy_syntax = Sign.syn_of thy
+  let val thy_syntax = Sign.syntax_of thy
   in make_syntax (thy_syntax, thy_syntax, Syntax.mode_default, []) end;
 
 fun rebuild thy (syntax as Syntax {mode, mixfixes, ...}) =
diff -r 33a9b1d6a651 -r d67cacd09251 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Tue Apr 02 18:02:43 2024 +0200
+++ b/src/Pure/Syntax/syntax.ML	Tue Apr 02 19:18:55 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 33a9b1d6a651 -r d67cacd09251 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Tue Apr 02 18:02:43 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Tue Apr 02 19:18:55 2024 +0200
@@ -64,7 +64,7 @@
   Markup.bound :: map (fn pos => Position.make_entity_markup def id Markup.boundN (name, pos)) ps;
 
 fun markup_entity ctxt c =
-  (case Syntax.lookup_const (Proof_Context.syn_of ctxt) c of
+  (case Syntax.lookup_const (Proof_Context.syntax_of ctxt) c of
     SOME "" => []
   | SOME b => markup_entity ctxt b
   | NONE => c |> Lexicon.unmark
@@ -338,7 +338,7 @@
 
 fun parse_asts ctxt raw root (syms, pos) =
   let
-    val syn = Proof_Context.syn_of ctxt;
+    val syn = Proof_Context.syntax_of ctxt;
     val ast_tr = Syntax.parse_ast_translation syn;
 
     val toks = Syntax.tokenize syn raw syms;
@@ -364,7 +364,7 @@
 
 fun parse_tree ctxt root input =
   let
-    val syn = Proof_Context.syn_of ctxt;
+    val syn = Proof_Context.syntax_of ctxt;
     val tr = Syntax.parse_translation syn;
     val parse_rules = Syntax.parse_rules syn;
     val (ambig_msgs, asts) = parse_asts ctxt false root input;
@@ -458,7 +458,7 @@
 
 fun parse_ast_pattern ctxt (root, str) =
   let
-    val syn = Proof_Context.syn_of ctxt;
+    val syn = Proof_Context.syntax_of ctxt;
 
     val reports = Unsynchronized.ref ([]: Position.report_text list);
     fun report ps = Position.store_reports reports ps;
@@ -731,7 +731,7 @@
     val show_sorts = Config.get ctxt show_sorts;
     val show_types = Config.get ctxt show_types orelse show_sorts;
 
-    val syn = Proof_Context.syn_of ctxt;
+    val syn = Proof_Context.syntax_of ctxt;
     val prtabs = Syntax.prtabs syn;
     val trf = Syntax.print_ast_translation syn;
 
@@ -801,7 +801,7 @@
 fun unparse_term ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val syn = Proof_Context.syn_of ctxt;
+    val syn = Proof_Context.syntax_of ctxt;
   in
     unparse_t (term_to_ast (is_some o Syntax.lookup_const syn))
       (Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy)))
diff -r 33a9b1d6a651 -r d67cacd09251 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Tue Apr 02 18:02:43 2024 +0200
+++ b/src/Pure/System/isabelle_process.ML	Tue Apr 02 19:18:55 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 33a9b1d6a651 -r d67cacd09251 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Apr 02 18:02:43 2024 +0200
+++ b/src/Pure/sign.ML	Tue Apr 02 19:18:55 2024 +0200
@@ -11,7 +11,7 @@
   val change_end: theory -> theory
   val change_end_local: Proof.context -> Proof.context
   val change_check: theory -> theory
-  val syn_of: theory -> Syntax.syntax
+  val syntax_of: theory -> Syntax.syntax
   val tsig_of: theory -> Type.tsig
   val classes_of: theory -> Sorts.algebra
   val all_classes: theory -> class list
@@ -176,7 +176,7 @@
 
 (* syntax *)
 
-val syn_of = #syn o rep_sg;
+val syntax_of = #syn o rep_sg;
 
 
 (* type signature *)
diff -r 33a9b1d6a651 -r d67cacd09251 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Tue Apr 02 18:02:43 2024 +0200
+++ b/src/Pure/theory.ML	Tue Apr 02 19:18:55 2024 +0200
@@ -201,6 +201,7 @@
       |> Sign.init_naming
       |> Sign.local_path
       |> apply_wrappers wrappers
+      |> tap (Syntax.cache_syntax o Sign.syntax_of)
     end;
 
 fun end_theory thy =