[stm] More cleanup of "classification is not an interpreter"

We remove meta-information from the query classification and we don't
process `Stm.query` as a transaction anymore, as the right API is
available to it to execute the command directly.

This simplifies pure commands and removes some impossible cases.

Depends on #7138.

2 files changed, 8 insertions, 19 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index a0305efee..ba0a2017a 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2782,16 +2782,9 @@ let process_transaction ?(newtip=Stateid.fresh ())
       | VtMeta, _ ->
         let id, w = Backtrack.undo_vernac_classifier expr in
         process_back_meta_command ~newtip ~head id x w
+
       (* Query *)
-      | VtQuery (false,route), VtNow ->
-        let query_sid = VCS.cur_tip () in
-        (try
-           let st = Vernacstate.freeze_interp_state `No in
-           ignore(stm_vernac_interp ~route query_sid st x)
-         with e ->
-           let e = CErrors.push e in
-           Exninfo.iraise (State.exn_on ~valid:Stateid.dummy query_sid e)); `Ok
-      | VtQuery (true, route), w ->
+      | VtQuery, w ->
           let id = VCS.new_node ~id:newtip () in
           let queue =
             if !cur_opt.async_proofs_full then `QueryQueue (ref false)
@@ -2803,9 +2796,6 @@ let process_transaction ?(newtip=Stateid.fresh ())
           VCS.commit id (mkTransCmd x [] false queue);
           Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
 
-      | VtQuery (false,_), VtLater ->
-          anomaly(str"classifier: VtQuery + VtLater must imply part_of_script.")
-
       (* Proof *)
       | VtStartProof (mode, guarantee, names), w ->
           let id = VCS.new_node ~id:newtip () in
@@ -3048,8 +3038,9 @@ let query ~doc ~at ~route s =
         let { CAst.loc; v=ast } = parse_sentence ~doc at s in
         let indentation, strlen = compute_indentation ?loc at in
         CWarnings.set_current_loc loc;
+        let st = State.get_cached at in
         let aast = { verbose = true; indentation; strlen; loc; expr = ast } in
-        ignore(process_transaction aast (VtQuery (false,route), VtNow))
+        ignore(stm_vernac_interp ~route at st aast)
       done;
     with
     | End_of_input -> ()
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index a78323323..eff870715 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -16,8 +16,6 @@ open Vernacexpr
 
 let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"]
 
-let string_of_in_script b = if b then " (inside script)" else ""
-
 let string_of_parallel = function
   | `Yes (solve,abs) ->
        "par" ^ if solve then "solve" else "" ^ if abs then "abs" else ""
@@ -34,7 +32,7 @@ let string_of_vernac_type = function
       "ProofStep " ^ string_of_parallel parallel ^
         Option.default "" proof_block_detection
   | VtProofMode s -> "ProofMode " ^ s
-  | VtQuery (b, route) -> "Query " ^ string_of_in_script b ^ " route " ^ string_of_int route
+  | VtQuery -> "Query"
   | VtMeta -> "Meta "
 
 let string_of_vernac_when = function
@@ -70,7 +68,7 @@ let classify_vernac e =
     | VernacEndProof _ | VernacExactProof _ -> VtQed VtKeep, VtLater
     (* Query *)
     | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _
-    | VernacCheckMayEval _ -> VtQuery (true,Feedback.default_route), VtLater
+    | VernacCheckMayEval _ -> VtQuery, VtLater
     (* ProofStep *)
     | VernacProof _ 
     | VernacFocus _ | VernacUnfocus
@@ -205,7 +203,7 @@ let classify_vernac e =
        static_control_classifier ~poly e
     | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
         (match static_control_classifier ~poly e with
-        | ( VtQuery _ | VtProofStep _ | VtSideff _
+        | ( VtQuery | VtProofStep _ | VtSideff _
           | VtProofMode _ | VtMeta), _ as x -> x
         | VtQed _, _ ->
             VtProofStep { parallel = `No; proof_block_detection = None },
@@ -214,6 +212,6 @@ let classify_vernac e =
   in
   static_control_classifier ~poly:(Flags.is_universe_polymorphism ()) e
 
-let classify_as_query = VtQuery (true,Feedback.default_route), VtLater
+let classify_as_query = VtQuery, VtLater
 let classify_as_sideeff = VtSideff [], VtLater
 let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}, VtLater