merged

--- a/src/HOL/ex/Sketch_and_Explore.thy	Fri Mar 15 18:54:15 2024 +0100
+++ b/src/HOL/ex/Sketch_and_Explore.thy	Fri Mar 15 20:23:50 2024 +0100
@@ -6,7 +6,7 @@
 
 theory Sketch_and_Explore
   imports Main \<comment> \<open>TODO: generalize existing sledgehammer functions to Pure\<close>
-  keywords "sketch" "nxsketch" "explore" :: diag
+  keywords "sketch" "explore" :: diag
 begin
 
 ML \<open>
@@ -26,26 +26,20 @@
   t
   |> singleton (Syntax.uncheck_terms ctxt)
   |> Sledgehammer_Isar_Annotate.annotate_types_in_term ctxt
-      \<comment> \<open>TODO pointless to annotate explicit fixes in term\<close>
   |> Print_Mode.setmp [] (Syntax.unparse_term ctxt #> Pretty.string_of)
   |> Sledgehammer_Util.simplify_spaces
   |> ATP_Util.maybe_quote ctxt;
 
-fun eigen_context_for_statement (fixes, assms, concl) ctxt =
+fun eigen_context_for_statement (params, assms, concl) ctxt =
   let
-    val (fixes', ctxt') = Variable.add_fixes (map fst fixes) ctxt;
-    val subst_free = AList.lookup (op =) (map fst fixes ~~ fixes')
-    val subst = map_aterms (fn Free (v, T) => Free (the_default v (subst_free v), T)
-      | t => t)
-    val assms' = map subst assms;
-    val concl' = subst concl;
-  in ((fixes, assms', concl'), ctxt') end;
+    val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params
+    val ctxt' = ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes |> snd
+  in ((params, assms, concl), ctxt') end;
 
 fun print_isar_skeleton ctxt indent keyword stmt =
   let
     val ((fixes, assms, concl), ctxt') = eigen_context_for_statement stmt ctxt;
     val prefix = replicate_string indent " ";
-      \<comment> \<open>TODO consider pre-existing indentation -- how?\<close>
     val prefix_sep = "\n" ^ prefix ^ "    and ";
     val show_s = prefix ^ keyword ^ " " ^ print_term ctxt' concl;
     val if_s = if null assms then NONE
@@ -60,17 +54,14 @@
     s
   end;
 
-fun print_nonext_sketch ctxt method_text clauses =
-  "proof" ^ method_text :: map (print_isar_skeleton ctxt 2 "show") clauses @ ["qed"];
-
-fun print_next_skeleton ctxt indent keyword stmt =
+fun print_skeleton ctxt indent keyword stmt =
   let
     val ((fixes, assms, concl), ctxt') = eigen_context_for_statement stmt ctxt;
     val prefix = replicate_string indent " ";
-    val prefix_sep = "\n" ^ prefix ^ "    and ";
+    val prefix_sep = "\n" ^ prefix ^ "  and ";
     val show_s = prefix ^ keyword ^ " " ^ print_term ctxt' concl;
     val assumes_s = if null assms then NONE
-      else SOME (prefix ^ "  assume " ^ space_implode prefix_sep
+      else SOME (prefix ^ "assume " ^ space_implode prefix_sep
         (map (print_term ctxt') assms));
     val fixes_s = if null fixes then NONE
       else SOME (prefix ^ "fix " ^ space_implode prefix_sep
@@ -80,11 +71,8 @@
     s
   end;
 
-fun print_next_sketch ctxt method_text clauses =
-  "proof" ^ method_text :: separate "next" (map (print_next_skeleton ctxt 2 "show") clauses) @ ["qed"];
-
-fun print_sketch ctxt method_text [cl] = print_next_sketch ctxt method_text [cl]
-  | print_sketch ctxt method_text clauses = print_nonext_sketch ctxt method_text clauses;
+fun print_sketch ctxt method_text clauses =
+  "proof" ^ method_text :: separate "next" (map (print_skeleton ctxt 2 "show") clauses) @ ["qed"];
 
 fun print_exploration ctxt method_text [clause] =
     ["proof -", print_isar_skeleton ctxt 2 "have" clause,
@@ -123,23 +111,18 @@
       if is_none some_method_ref then ["  .."]
       else ["  by" ^ method_text]
       else print ctxt_print method_text clauses;
-    val message = Active.sendback_markup_properties [] (cat_lines lines);
+    val message = Active.sendback_markup_command (cat_lines lines);
   in
     (state |> tap (fn _ => Output.information message))
   end
 
 val sketch = print_proof_text_from_state print_sketch;
 
-val next_sketch = print_proof_text_from_state print_next_sketch;
-
 fun explore method_ref = print_proof_text_from_state print_exploration (SOME method_ref);
 
 fun sketch_cmd some_method_text =
   Toplevel.keep_proof (K () o sketch some_method_text o Toplevel.proof_of)
 
-fun next_sketch_cmd some_method_text =
-  Toplevel.keep_proof (K () o next_sketch some_method_text o Toplevel.proof_of)
-
 fun explore_cmd method_text =
   Toplevel.keep_proof (K () o explore method_text o Toplevel.proof_of)
 
@@ -149,11 +132,6 @@
     (Scan.option (Scan.trace Method.parse) >> sketch_cmd);
 
 val _ =
-  Outer_Syntax.command \<^command_keyword>\<open>nxsketch\<close>
-    "print sketch of Isar proof text after method application"
-    (Scan.option (Scan.trace Method.parse) >> next_sketch_cmd);
-
-val _ =
   Outer_Syntax.command \<^command_keyword>\<open>explore\<close>
     "explore proof obligations after method application as Isar proof text"
     (Scan.trace Method.parse >> explore_cmd);

--- a/src/Pure/Build/build_process.scala	Fri Mar 15 18:54:15 2024 +0100
+++ b/src/Pure/Build/build_process.scala	Fri Mar 15 20:23:50 2024 +0100
@@ -911,7 +911,7 @@
 
     /* collective operations */
 
-    def pull_database(db: SQL.Database, build_id: Long, worker_uuid: String, state: State): State = {
+    def pull_state(db: SQL.Database, build_id: Long, worker_uuid: String, state: State): State = {
       val serial_db = read_serial(db)
       if (serial_db == state.serial) state
       else {
@@ -928,7 +928,7 @@
       }
     }
 
-    def update_database(
+    def push_state(
       db: SQL.Database,
       build_id: Long,
       worker_uuid: String,
@@ -1124,11 +1124,11 @@
         case Some(db) =>
           Build_Process.private_data.transaction_lock(db, label = label) {
             val old_state =
-              Build_Process.private_data.pull_database(db, build_id, worker_uuid, _state)
+              Build_Process.private_data.pull_state(db, build_id, worker_uuid, _state)
             _state = old_state
             val res = body
             _state =
-              Build_Process.private_data.update_database(
+              Build_Process.private_data.push_state(
                 db, build_id, worker_uuid, _state, old_state)
             res
           }

--- a/src/Pure/Build/build_schedule.scala	Fri Mar 15 18:54:15 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Fri Mar 15 20:23:50 2024 +0100
@@ -879,15 +879,15 @@
           case Some(db) =>
             db.transaction_lock(Build_Schedule.private_data.all_tables, label = label) {
               val old_state =
-                Build_Process.private_data.pull_database(db, build_id, worker_uuid, _state)
+                Build_Process.private_data.pull_state(db, build_id, worker_uuid, _state)
               val old_schedule = Build_Schedule.private_data.pull_schedule(db, _schedule)
               _state = old_state
               _schedule = old_schedule
               val res = body
               _state =
-                Build_Process.private_data.update_database(
+                Build_Process.private_data.push_state(
                   db, build_id, worker_uuid, _state, old_state)
-              _schedule = Build_Schedule.private_data.update_schedule(db, _schedule, old_schedule)
+              _schedule = Build_Schedule.private_data.pull_schedule(db, _schedule, old_schedule)
               res
             }
         }
@@ -1273,7 +1273,7 @@
       }
     }
 
-    def update_schedule(db: SQL.Database, schedule: Schedule, old_schedule: Schedule): Schedule = {
+    def pull_schedule(db: SQL.Database, schedule: Schedule, old_schedule: Schedule): Schedule = {
       val changed =
         schedule.generator != old_schedule.generator ||
         schedule.start != old_schedule.start ||