proper position for ML-like commands;

--- a/src/Pure/Isar/local_theory.ML	Thu May 11 14:17:24 2023 +0200
+++ b/src/Pure/Isar/local_theory.ML	Thu May 11 21:32:22 2023 +0200
@@ -43,6 +43,7 @@
   val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
   val target_morphism: local_theory -> morphism
   val propagate_ml_env: generic_theory -> generic_theory
+  val touch_ml_env: generic_theory -> generic_theory
   val operations_of: local_theory -> operations
   val define: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory
@@ -253,6 +254,13 @@
       end
   | propagate_ml_env context = context;
 
+fun touch_ml_env context =
+  if Context.enabled_tracing () then
+    (case context of
+      Context.Theory _ => ML_Env.touch context
+    | Context.Proof _ => context)
+  else context;
+
 
 
 (** operations **)

--- a/src/Pure/Isar/outer_syntax.ML	Thu May 11 14:17:24 2023 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Thu May 11 21:32:22 2023 +0200
@@ -325,7 +325,8 @@
   command ("ML", \<^here>) "ML text within theory or local theory"
     (Parse.ML_source >> (fn source =>
       Toplevel.generic_theory
-        (ML_Context.exec (fn () =>
+        (Local_Theory.touch_ml_env #>
+          ML_Context.exec (fn () =>
             ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source) #>
           Local_Theory.propagate_ml_env)));
 

--- a/src/Pure/ML/ml_context.ML	Thu May 11 14:17:24 2023 +0200
+++ b/src/Pure/ML/ml_context.ML	Thu May 11 21:32:22 2023 +0200
@@ -228,7 +228,9 @@
     SOME context' => context'
   | NONE => error "Missing context after execution");
 
-fun expression pos ants = exec (fn () => eval ML_Compiler.flags pos ants);
+fun expression pos ants =
+  Local_Theory.touch_ml_env #>
+  exec (fn () => eval ML_Compiler.flags pos ants);
 
 end;
 

--- a/src/Pure/ML/ml_env.ML	Thu May 11 14:17:24 2023 +0200
+++ b/src/Pure/ML/ml_env.ML	Thu May 11 21:32:22 2023 +0200
@@ -26,6 +26,7 @@
   val Isabelle_operations: operations
   val SML_operations: operations
   val operations: Context.generic option -> string -> operations
+  val touch: Context.generic -> Context.generic
   val forget_structure: string -> Context.generic -> Context.generic
   val bootstrap_name_space: Context.generic -> Context.generic
   val add_name_space: string -> ML_Name_Space.T -> Context.generic -> Context.generic
@@ -127,6 +128,8 @@
 val get_env = Name_Space.get o #1 o Data.get;
 val get_tables = #1 oo get_env;
 
+val touch = Data.map I;
+
 fun update_tables env_name f context = context |> (Data.map o apfst) (fn envs =>
   let val _ = Name_Space.get envs env_name;
   in Name_Space.map_table_entry env_name (apfst f) envs end);

--- a/src/Pure/ML/ml_file.ML	Thu May 11 14:17:24 2023 +0200
+++ b/src/Pure/ML/ml_file.ML	Thu May 11 21:32:22 2023 +0200
@@ -28,6 +28,7 @@
         debug = debug, writeln = writeln, warning = warning};
   in
     gthy
+    |> Local_Theory.touch_ml_env
     |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
     |> Local_Theory.propagate_ml_env
     |> Context.mapping provide (Local_Theory.background_theory provide)

--- a/src/Pure/context.ML	Thu May 11 14:17:24 2023 +0200
+++ b/src/Pure/context.ML	Thu May 11 21:32:22 2023 +0200
@@ -69,6 +69,7 @@
   datatype generic = Theory of theory | Proof of Proof.context
   val theory_tracing: bool Unsynchronized.ref
   val proof_tracing: bool Unsynchronized.ref
+  val enabled_tracing: unit -> bool
   val finish_tracing: unit ->
    {contexts: (generic * Position.T) list,
     active_contexts: int,
@@ -198,6 +199,8 @@
 val theory_tracing = Unsynchronized.ref false;
 val proof_tracing = Unsynchronized.ref false;
 
+fun enabled_tracing () = ! theory_tracing orelse ! proof_tracing;
+
 local
 
 fun cons_tokens var token =