diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 28 | ||||
| -rw-r--r-- | stm/texmacspp.ml | 2 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 2 |
3 files changed, 17 insertions, 15 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 07262ef68f..92032e9bc3 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1140,9 +1140,10 @@ end = struct (* {{{ *) let perform_states query = if query = [] then [] else - let is_tac = function - | VernacSolve _ | VernacFocus _ | VernacUnfocus | VernacBullet _ -> true - | _ -> false in + let is_tac e = match classify_vernac e with + | VtProofStep _, _ -> true + | _ -> false + in let initial = let rec aux id = try match VCS.visit id with { next } -> aux next @@ -1413,7 +1414,7 @@ and TacTask : sig t_state : Stateid.t; t_state_fb : Stateid.t; t_assign : output Future.assignement -> unit; - t_ast : ast; + t_ast : int * ast; t_goal : Goal.goal; t_kill : unit -> unit; t_name : string } @@ -1430,7 +1431,7 @@ end = struct (* {{{ *) t_state : Stateid.t; t_state_fb : Stateid.t; t_assign : output Future.assignement -> unit; - t_ast : ast; + t_ast : int * ast; t_goal : Goal.goal; t_kill : unit -> unit; t_name : string } @@ -1439,7 +1440,7 @@ end = struct (* {{{ *) r_state : Stateid.t; r_state_fb : Stateid.t; r_document : VCS.vcs option; - r_ast : ast; + r_ast : int * ast; r_goal : Goal.goal; r_name : string } @@ -1483,6 +1484,9 @@ end = struct (* {{{ *) | Some { t_kill } -> t_kill () | _ -> () + let command_focus = Proof.new_focus_kind () + let focus_cond = Proof.no_cond command_focus + let perform { r_state = id; r_state_fb; r_document = vcs; r_ast; r_goal } = Option.iter VCS.restore vcs; try @@ -1498,7 +1502,9 @@ end = struct (* {{{ *) Errors.errorlabstrm "Stm" (strbrk("the par: goal selector supports ground "^ "goals only")) else begin - vernac_interp r_state_fb r_ast; + let (i, ast) = r_ast in + Proof_global.simple_with_current_proof (fun _ p -> Proof.focus focus_cond () i p); + vernac_interp r_state_fb ast; let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in match Evd.(evar_body (find sigma r_goal)) with | Evd.Evar_empty -> Errors.errorlabstrm "Stm" (str "no progress") @@ -1527,12 +1533,11 @@ end = struct (* {{{ *) module TaskQueue = AsyncTaskQueue.MakeQueue(TacTask) let vernac_interp cancel nworkers safe_id id { verbose; loc; expr = e } = - let e, etac, time, fail = + let e, time, fail = let rec find time fail = function - | VernacSolve(_,_,re,b) -> re, b, time, fail | VernacTime (_,e) | VernacRedirect (_,(_,e)) -> find true fail e | VernacFail e -> find time true e - | _ -> errorlabstrm "Stm" (str"unsupported") in find false false e in + | _ -> e, time, fail in find false false e in Hooks.call Hooks.with_fail fail (fun () -> (if time then System.with_time false else (fun x -> x)) (fun () -> ignore(TaskQueue.with_n_workers nworkers (fun queue -> @@ -1544,8 +1549,7 @@ end = struct (* {{{ *) Future.create_delegate ~name:(Printf.sprintf "subgoal %d" i) (State.exn_on id ~valid:safe_id) in - let t_ast = - { verbose;loc;expr = VernacSolve(SelectNth i,None,e,etac) } in + let t_ast = (i, { verbose; loc; expr = e }) in let t_name = Goal.uid g in TaskQueue.enqueue_task queue ({ t_state = safe_id; t_state_fb = id; diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index 3c4b8cb71e..a459cd65f8 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -671,7 +671,7 @@ let rec tmpp v loc = (* Solving *) - | (VernacSolve _ | VernacSolveExistential _) as x -> + | (VernacSolveExistential _) as x -> xmlLtac loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))] (* Auxiliary file and library management *) diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index f9f08f7afb..97d6e1fb71 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -102,12 +102,10 @@ let rec classify_vernac e = | VernacCheckMayEval _ -> VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater (* ProofStep *) - | VernacSolve (SelectAllParallel,_,_,_) -> VtProofStep true, VtLater | VernacProof _ | VernacBullet _ | VernacFocus _ | VernacUnfocus | VernacSubproof _ | VernacEndSubproof - | VernacSolve _ | VernacCheckGuard | VernacUnfocused | VernacSolveExistential _ -> VtProofStep false, VtLater |