diff options
Diffstat (limited to 'stm/stm.ml')
| -rw-r--r-- | stm/stm.ml | 191 |
1 files changed, 125 insertions, 66 deletions
@@ -51,7 +51,7 @@ let execution_error, execution_error_hook = Hook.make feedback ~state_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg))) () let unreachable_state, unreachable_state_hook = Hook.make - ~default:(fun _ -> ()) () + ~default:(fun _ _ -> ()) () include Hook @@ -86,7 +86,7 @@ let vernac_interp ?proof id ?route { verbose; loc; expr } = | VernacResetName _ | VernacResetInitial | VernacBack _ | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _ | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true - | VernacTime el -> List.for_all (fun (_,e) -> internal_command e) el + | VernacTime el | VernacRedirect (_,el) -> List.for_all (fun (_,e) -> internal_command e) el | _ -> false in if internal_command expr then begin prerr_endline ("ignoring " ^ string_of_ppcmds(pr_vernac expr)) @@ -123,6 +123,10 @@ let pr_open_cur_subgoals () = try Printer.pr_open_subgoals () with Proof_global.NoCurrentProof -> str"" +let update_global_env () = + if Proof_global.there_are_pending_proofs () then + Proof_global.update_global_env () + module Vcs_ = Vcs.Make(Stateid) type future_proof = Proof_global.closed_proof_output Future.computation type proof_mode = string @@ -131,9 +135,11 @@ type cancel_switch = bool ref type branch_type = [ `Master | `Proof of proof_mode * depth - | `Edit of proof_mode * Stateid.t * Stateid.t * vernac_qed_type ] + | `Edit of + proof_mode * Stateid.t * Stateid.t * vernac_qed_type * Vcs_.Branch.t ] type cmd_t = { ctac : bool; (* is a tactic, needed by the 8.4 semantics of Undo *) + ceff : bool; (* is a side-effecting command *) cast : ast; cids : Id.t list; cqueue : [ `MainQueue | `TacQueue of cancel_switch | `QueryQueue of cancel_switch ] } @@ -371,7 +377,7 @@ end = struct (* {{{ *) (try let n = Hashtbl.find clus c in from::n with Not_found -> [from]); true in let oc = open_out fname_dot in - output_string oc "digraph states {\nsplines=ortho\n"; + output_string oc "digraph states {\n"; Dag.iter graph (fun from cf _ l -> let c1 = add_to_clus_or_ids from cf in List.iter (fun (dest, trans) -> @@ -423,8 +429,8 @@ end = struct (* {{{ *) let reachable id = reachable !vcs id let mk_branch_name { expr = x } = Branch.make (match x with - | VernacDefinition (_,(_,i),_) -> string_of_id i - | VernacStartTheoremProof (_,[Some (_,i),_],_) -> string_of_id i + | VernacDefinition (_,((_,i),_),_) -> string_of_id i + | VernacStartTheoremProof (_,[Some ((_,i),_),_],_) -> string_of_id i | _ -> "branch") let edit_branch = Branch.make "edit" let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind @@ -449,7 +455,7 @@ end = struct (* {{{ *) if List.mem edit_branch (Vcs_.branches !vcs) then begin checkout edit_branch; match get_branch edit_branch with - | { kind = `Edit (mode, _,_,_) } -> Proof_global.activate_proof_mode mode + | { kind = `Edit (mode, _,_,_,_) } -> Proof_global.activate_proof_mode mode | _ -> assert false end else let pl = proof_nesting () in @@ -590,6 +596,7 @@ module State : sig ?safe_id:Stateid.t -> ?redefine:bool -> ?cache:Summary.marshallable -> ?feedback_processed:bool -> (unit -> unit) -> Stateid.t -> unit + val fix_exn_ref : (iexn -> iexn) ref val install_cached : Stateid.t -> unit val is_cached : ?cache:Summary.marshallable -> Stateid.t -> bool @@ -613,6 +620,7 @@ end = struct (* {{{ *) (* cur_id holds Stateid.dummy in case the last attempt to define a state * failed, so the global state may contain garbage *) let cur_id = ref Stateid.dummy + let fix_exn_ref = ref (fun x -> x) (* helpers *) let freeze_global_state marshallable = @@ -638,7 +646,7 @@ end = struct (* {{{ *) proof, Summary.project_summary (States.summary_of_state system) summary_pstate - let freeze marhallable id = VCS.set_state id (freeze_global_state marhallable) + let freeze marshallable id = VCS.set_state id (freeze_global_state marshallable) let is_cached ?(cache=`No) id = if Stateid.equal id !cur_id then @@ -670,11 +678,22 @@ end = struct (* {{{ *) let assign id what = if VCS.get_state id <> None then () else try match what with - | `Full s -> VCS.set_state id s + | `Full s -> + let s = + try + let prev = (VCS.visit id).next in + if is_cached prev + then { s with proof = + Proof_global.copy_terminators + ~src:(get_cached prev).proof ~tgt:s.proof } + else s + with VCS.Expired -> s in + VCS.set_state id s | `Proof(ontop,(pstate,counters)) -> if is_cached ontop then let s = get_cached ontop in - let s = { s with proof = pstate } in + let s = { s with proof = + Proof_global.copy_terminators ~src:s.proof ~tgt:pstate } in let s = { s with system = States.replace_summary s.system (Summary.surgery_summary @@ -709,7 +728,10 @@ end = struct (* {{{ *) try prerr_endline("defining "^str_id^" (cache="^ if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)"); + let good_id = match safe_id with None -> !cur_id | Some id -> id in + fix_exn_ref := exn_on id ~valid:good_id; f (); + fix_exn_ref := (fun x -> x); if cache = `Yes then freeze `No id else if cache = `Shallow then freeze `Shallow id; prerr_endline ("setting cur id to "^str_id); @@ -718,13 +740,13 @@ end = struct (* {{{ *) Hooks.(call state_computed id ~in_cache:false); VCS.reached id true; if Proof_global.there_are_pending_proofs () then - VCS.goals id (Proof_global.get_open_goals ()); + VCS.goals id (Proof_global.get_open_goals ()) with e -> let (e, info) = Errors.push e in let good_id = !cur_id in cur_id := Stateid.dummy; VCS.reached id false; - Hooks.(call unreachable_state id); + Hooks.(call unreachable_state id (e, info)); match Stateid.get info, safe_id with | None, None -> iraise (exn_on id ~valid:good_id (e, info)) | None, Some good_id -> iraise (exn_on id ~valid:good_id (e, info)) @@ -846,7 +868,8 @@ end = struct (* {{{ *) | None, _ -> anomaly(str"Backtrack: tip with no vcs_backup") | Some vcs, _ -> vcs in let cb, _ = - Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs) in + try Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs) + with Failure _ -> raise Proof_global.NoCurrentProof in let n = fold_until (fun n (_,vcs,_,_,_) -> if List.mem cb (Vcs_.branches vcs) then `Cont (n+1) else `Stop n) 0 id in @@ -875,9 +898,16 @@ let set_compilation_hints file = hints := Aux_file.load_aux_file_for file let get_hint_ctx loc = let s = Aux_file.get !hints loc "context_used" in - let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") s) in - let ids = List.map (fun id -> Loc.ghost, id) ids in - SsExpr (SsSet ids) + match Str.split (Str.regexp ";") s with + | ids :: _ -> + let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") ids) in + let ids = List.map (fun id -> Loc.ghost, id) ids in + begin match ids with + | [] -> SsEmpty + | x :: xs -> + List.fold_left (fun a x -> SsUnion (SsSingl x,a)) (SsSingl x) xs + end + | _ -> raise Not_found let get_hint_bp_time proof_name = try float_of_string (Aux_file.get !hints Loc.ghost proof_name) @@ -1117,7 +1147,7 @@ end = struct (* {{{ *) when is_tac expr && State.same_env o n -> (* A pure tactic *) Some (id, `Proof (prev, State.proof_part_of_frozen n)) | Some _, Some s -> - msg_warning (str "Sending back a fat state"); + msg_warning (str "STM: sending back a fat state"); Some (id, `Full s) | _, Some s -> Some (id, `Full s) in let rec aux seen = function @@ -1207,7 +1237,7 @@ end = struct (* {{{ *) (Lemmas.standard_proof_terminator [] (Lemmas.mk_hook (fun _ _ -> ()))); let proof = - Proof_global.close_proof ~keep_body_ucst_sepatate:true (fun x -> x) in + Proof_global.close_proof ~keep_body_ucst_separate:true (fun x -> x) in (* We jump at the beginning since the kernel handles side effects by also * looking at the ones that happen to be present in the current env *) Reach.known_state ~cache:`No start; @@ -1472,7 +1502,7 @@ end = struct (* {{{ *) let e, etac, time, fail = let rec find time fail = function | VernacSolve(_,_,re,b) -> re, b, time, fail - | VernacTime [_,e] -> find true fail e + | VernacTime [_,e] | VernacRedirect (_,[_,e]) -> find true fail e | VernacFail e -> find time true e | _ -> errorlabstrm "Stm" (str"unsupported") in find false false e in Hooks.call Hooks.with_fail fail (fun () -> @@ -1564,7 +1594,8 @@ end = struct (* {{{ *) vernac_interp r_for { r_what with verbose = true }; feedback ~state_id:r_for Feedback.Processed with e when Errors.noncritical e -> - let msg = string_of_ppcmds (print e) in + let e = Errors.push e in + let msg = string_of_ppcmds (iprint e) in feedback ~state_id:r_for (Feedback.ErrorMsg (Loc.ghost, msg)) let name_of_task { t_what } = string_of_ppcmds (pr_ast t_what) @@ -1675,7 +1706,10 @@ let collect_proof keep cur hd brkind id = assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch); let name = name ids in `MaybeASync (parent last, None, accn, name, delegate name) - | `Sideff _ -> `Sync (no_name,None,`NestedProof) + | `Sideff _ -> + Pp.(msg_warning (strbrk ("Nested proofs are deprecated and will "^ + "stop working in the next Coq version"))); + `Sync (no_name,None,`NestedProof) | _ -> `Sync (no_name,None,`Unknown) in let make_sync why = function | `Sync(name,pua,_) -> `Sync (name,pua,why) @@ -1729,8 +1763,9 @@ let known_state ?(redefine_qed=false) ~cache id = let cherry_pick_non_pstate () = Summary.freeze_summary ~marshallable:`No ~complement:true pstate, Lib.freeze ~marshallable:`No in - let inject_non_pstate (s,l) = Summary.unfreeze_summary s; Lib.unfreeze l in - + let inject_non_pstate (s,l) = + Summary.unfreeze_summary s; Lib.unfreeze l; update_global_env () + in let rec pure_cherry_pick_non_pstate id = Future.purify (fun id -> prerr_endline ("cherry-pick non pstate " ^ Stateid.to_string id); reach id; @@ -1757,12 +1792,12 @@ let known_state ?(redefine_qed=false) ~cache id = ), cache, true | `Cmd { cast = x; cqueue = `QueryQueue cancel } when Flags.async_proofs_is_master () -> (fun () -> - reach ~cache:`Shallow view.next; + reach view.next; Query.vernac_interp cancel view.next id x ), cache, false - | `Cmd { cast = x } -> (fun () -> - reach view.next; vernac_interp id x - ), cache, true + | `Cmd { cast = x; ceff = eff } -> (fun () -> + reach view.next; vernac_interp id x; + if eff then update_global_env ()), cache, true | `Fork ((x,_,_,_), None) -> (fun () -> reach view.next; vernac_interp id x; wall_clock_last_fork := Unix.gettimeofday () @@ -1787,7 +1822,7 @@ let known_state ?(redefine_qed=false) ~cache id = VCS.create_cluster nodes ~qed:id ~start; begin match brinfo, qed.fproof with | { VCS.kind = `Edit _ }, None -> assert false - | { VCS.kind = `Edit (_,_,_, okeep) }, Some (ofp, cancel) -> + | { VCS.kind = `Edit (_,_,_, okeep, _) }, Some (ofp, cancel) -> assert(redefine_qed = true); if okeep != keep then msg_error(strbrk("The command closing the proof changed. " @@ -1824,7 +1859,6 @@ let known_state ?(redefine_qed=false) ~cache id = Proof_global.discard_all () ), (if redefine_qed then `No else `Yes), true | `Sync (name, _, `Immediate) -> (fun () -> - assert (Stateid.equal view.next eop); reach eop; vernac_interp id x; Proof_global.discard_all () ), `Yes, true | `Sync (name, pua, reason) -> (fun () -> @@ -1841,11 +1875,10 @@ let known_state ?(redefine_qed=false) ~cache id = qed.fproof <- Some (fp, ref false); None | VtKeep -> Some(Proof_global.close_proof - ~keep_body_ucst_sepatate:false + ~keep_body_ucst_separate:false (State.exn_on id ~valid:eop)) in - reach view.next; - if keep == VtKeepAsAxiom then - Option.iter (vernac_interp id) pua; + if keep != VtKeepAsAxiom then + reach view.next; let wall_clock2 = Unix.gettimeofday () in vernac_interp id ?proof x; let wall_clock3 = Unix.gettimeofday () in @@ -1863,7 +1896,7 @@ let known_state ?(redefine_qed=false) ~cache id = in aux (collect_proof keep (view.next, x) brname brinfo eop) | `Sideff (`Ast (x,_)) -> (fun () -> - reach view.next; vernac_interp id x; + reach view.next; vernac_interp id x; update_global_env () ), cache, true | `Sideff (`Id origin) -> (fun () -> reach view.next; @@ -1890,7 +1923,7 @@ let init () = Backtrack.record (); Slaves.init (); if Flags.async_proofs_is_master () then begin - prerr_endline "Initialising workers"; + prerr_endline "Initializing workers"; Query.init (); let opts = match !Flags.async_proofs_private_flags with | None -> [] @@ -1921,7 +1954,7 @@ let finish ?(print_goals=false) () = VCS.print (); (* Some commands may by side effect change the proof mode *) match VCS.get_branch head with - | { VCS.kind = `Edit (mode, _,_,_) } -> Proof_global.activate_proof_mode mode + | { VCS.kind = `Edit (mode,_,_,_,_) } -> Proof_global.activate_proof_mode mode | { VCS.kind = `Proof (mode, _) } -> Proof_global.activate_proof_mode mode | _ -> () @@ -1989,7 +2022,7 @@ let merge_proof_branch ?valid ?id qast keep brname = VCS.delete_branch brname; if keep <> VtDrop then VCS.propagate_sideff None; `Ok - | { VCS.kind = `Edit (mode, qed_id, master_id, _) } -> + | { VCS.kind = `Edit (mode, qed_id, master_id, _,_) } -> let ofp = match VCS.visit qed_id with | { step = `Qed ({ fproof }, _) } -> fproof @@ -2018,7 +2051,7 @@ let handle_failure (e, info) vcs tty = end; VCS.print (); anomaly(str"error with no safe_id attached:" ++ spc() ++ - Errors.print_no_report e) + Errors.iprint_no_report (e, info)) | Some (safe_id, id) -> prerr_endline ("Failed at state " ^ Stateid.to_string id); VCS.restore vcs; @@ -2104,7 +2137,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = iraise (State.exn_on report_id e)); `Ok | VtQuery (false,(report_id,route)), VtNow -> (try vernac_interp report_id ~route x - with e when Errors.noncritical e -> + with e -> let e = Errors.push e in iraise (State.exn_on report_id e)); `Ok | VtQuery (true,(report_id,_)), w -> @@ -2113,7 +2146,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = let queue = if !Flags.async_proofs_full then `QueryQueue (ref false) else `MainQueue in - VCS.commit id (Cmd {ctac=false;cast = x; cids = []; cqueue = queue }); + VCS.commit id (Cmd {ctac=false;ceff=false;cast = x; cids = []; cqueue = queue }); Backtrack.record (); if w == VtNow then finish (); `Ok | VtQuery (false,_), VtLater -> anomaly(str"classifier: VtQuery + VtLater must imply part_of_script") @@ -2136,16 +2169,16 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = anomaly(str"VtProofMode must be executed VtNow") | VtProofMode mode, VtNow -> let id = VCS.new_node ~id:newtip () in - VCS.commit id (Cmd {ctac=false;cast = x;cids=[];cqueue = `MainQueue}); + VCS.commit id (Cmd {ctac=false;ceff=false;cast = x;cids=[];cqueue = `MainQueue}); List.iter (fun bn -> match VCS.get_branch bn with | { VCS.root; kind = `Master; pos } -> () | { VCS.root; kind = `Proof(_,d); pos } -> VCS.delete_branch bn; VCS.branch ~root ~pos bn (`Proof(mode,d)) - | { VCS.root; kind = `Edit(_,f,q,k); pos } -> + | { VCS.root; kind = `Edit(_,f,q,k,ob); pos } -> VCS.delete_branch bn; - VCS.branch ~root ~pos bn (`Edit(mode,f,q,k))) + VCS.branch ~root ~pos bn (`Edit(mode,f,q,k,ob))) (VCS.branches ()); VCS.checkout_shallowest_proof_branch (); Backtrack.record (); @@ -2154,7 +2187,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = | VtProofStep paral, w -> let id = VCS.new_node ~id:newtip () in let queue = if paral then `TacQueue (ref false) else `MainQueue in - VCS.commit id (Cmd {ctac = true;cast = x;cids = [];cqueue = queue }); + VCS.commit id (Cmd {ctac = true;ceff = false;cast = x;cids = [];cqueue = queue }); Backtrack.record (); if w == VtNow then finish (); `Ok | VtQed keep, w -> let valid = if tty then Some(VCS.get_branch_pos head) else None in @@ -2170,7 +2203,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = | VtSideff l, w -> let id = VCS.new_node ~id:newtip () in VCS.checkout VCS.Branch.master; - VCS.commit id (Cmd {ctac=false;cast=x;cids=l;cqueue=`MainQueue}); + VCS.commit id (Cmd {ctac=false;ceff=true;cast=x;cids=l;cqueue=`MainQueue}); VCS.propagate_sideff (Some x); VCS.checkout_shallowest_proof_branch (); Backtrack.record (); if w == VtNow then finish (); `Ok @@ -2194,7 +2227,8 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = VCS.branch bname (`Proof ("Classic", VCS.proof_nesting () + 1)); Proof_global.activate_proof_mode "Classic"; end else begin - VCS.commit id (Cmd {ctac=false; cast = x; cids = []; cqueue = `MainQueue}); + VCS.commit id (Cmd {ctac = false; ceff = true; + cast = x; cids = []; cqueue = `MainQueue}); VCS.propagate_sideff (Some x); VCS.checkout_shallowest_proof_branch (); end in @@ -2283,6 +2317,17 @@ let edit_at id = | { step = `Fork _ } -> false | { next } -> aux next in aux (VCS.get_branch_pos (VCS.current_branch ())) in + let rec is_pure_aux id = + let view = VCS.visit id in + match view.step with + | `Cmd _ -> is_pure_aux view.next + | `Fork _ -> true + | _ -> false in + let is_pure id = + match (VCS.visit id).step with + | `Qed (_,last_step) -> is_pure_aux last_step + | _ -> assert false + in let is_ancestor_of_cur_branch id = Vcs_.NodeSet.mem id (VCS.reachable (VCS.get_branch_pos (VCS.current_branch ()))) in @@ -2293,24 +2338,27 @@ let edit_at id = let rec master_for_br root tip = if Stateid.equal tip Stateid.initial then tip else match VCS.visit tip with - | { next } when next = root -> root - | { step = `Fork _ } -> tip - | { step = `Sideff (`Ast(_,id)|`Id id) } -> id + | { step = (`Fork _ | `Qed _) } -> tip + | { step = `Sideff (`Ast(_,id)) } -> id + | { step = `Sideff _ } -> tip | { next } -> master_for_br root next in - let reopen_branch start at_id mode qed_id tip = + let reopen_branch start at_id mode qed_id tip old_branch = let master_id, cancel_switch, keep = (* Hum, this should be the real start_id in the clusted and not next *) match VCS.visit qed_id with | { step = `Qed ({ fproof = Some (_,cs); keep },_) } -> start, cs, keep | _ -> anomaly (str "Cluster not ending with Qed") in VCS.branch ~root:master_id ~pos:id - VCS.edit_branch (`Edit (mode, qed_id, master_id, keep)); + VCS.edit_branch (`Edit (mode, qed_id, master_id, keep, old_branch)); VCS.delete_cluster_of id; cancel_switch := true; Reach.known_state ~cache:(interactive ()) id; VCS.checkout_shallowest_proof_branch (); `Focus { stop = qed_id; start = master_id; tip } in - let backto id = + let no_edit = function + | `Edit (pm, _,_,_,_) -> `Proof(pm,1) + | x -> x in + let backto id bn = List.iter VCS.delete_branch (VCS.branches ()); let ancestors = VCS.reachable id in let { mine = brname, brinfo; others } = Backtrack.branches_of id in @@ -2320,10 +2368,14 @@ let edit_at id = VCS.branch ~root ~pos name k) others; VCS.reset_branch VCS.Branch.master (master_for_br brinfo.VCS.root id); - VCS.branch ~root:brinfo.VCS.root ~pos:brinfo.VCS.pos brname brinfo.VCS.kind; + VCS.branch ~root:brinfo.VCS.root ~pos:brinfo.VCS.pos + (Option.default brname bn) + (no_edit brinfo.VCS.kind); VCS.delete_cluster_of id; VCS.gc (); - Reach.known_state ~cache:(interactive ()) id; + VCS.print (); + if not !Flags.async_proofs_full then + Reach.known_state ~cache:(interactive ()) id; VCS.checkout_shallowest_proof_branch (); `NewTip in try @@ -2331,20 +2383,21 @@ let edit_at id = let focused = List.exists ((=) VCS.edit_branch) (VCS.branches ()) in let branch_info = match snd (VCS.get_info id).vcs_backup with - | Some{ mine = _, { VCS.kind = (`Proof(m,_)|`Edit(m,_,_,_)) }} -> Some m + | Some{ mine = bn, { VCS.kind = `Proof(m,_) }} -> Some(m,bn) + | Some{ mine = _, { VCS.kind = `Edit(m,_,_,_,bn) }} -> Some (m,bn) | _ -> None in match focused, VCS.cluster_of id, branch_info with | _, Some _, None -> assert false - | false, Some (qed_id,start), Some mode -> + | false, Some (qed_id,start), Some(mode,bn) -> let tip = VCS.cur_tip () in - if has_failed qed_id && not !Flags.async_proofs_never_reopen_branch - then reopen_branch start id mode qed_id tip - else backto id - | true, Some (qed_id,_), Some mode -> + if has_failed qed_id && is_pure qed_id && not !Flags.async_proofs_never_reopen_branch + then reopen_branch start id mode qed_id tip bn + else backto id (Some bn) + | true, Some (qed_id,_), Some(mode,bn) -> if on_cur_branch id then begin assert false end else if is_ancestor_of_cur_branch id then begin - backto id + backto id (Some bn) end else begin anomaly(str"Cannot leave an `Edit branch open") end @@ -2355,11 +2408,12 @@ let edit_at id = VCS.checkout_shallowest_proof_branch (); `NewTip end else if is_ancestor_of_cur_branch id then begin - backto id + backto id None end else begin anomaly(str"Cannot leave an `Edit branch open") end - | false, None, _ -> backto id + | false, None, Some(_,bn) -> backto id (Some bn) + | false, None, None -> backto id None in VCS.print (); rc @@ -2376,6 +2430,9 @@ let edit_at id = VCS.print (); iraise (e, info) +let backup () = VCS.backup () +let restore d = VCS.restore d + (*********************** TTY API (PG, coqtop, coqc) ***************************) (******************************************************************************) @@ -2430,7 +2487,7 @@ let get_script prf = let branch, test = match prf with | None -> VCS.Branch.master, fun _ -> true - | Some name -> VCS.current_branch (), List.mem name in + | Some name -> VCS.current_branch (),fun nl -> nl=[] || List.mem name nl in let rec find acc id = if Stateid.equal id Stateid.initial || Stateid.equal id Stateid.dummy then acc else @@ -2441,7 +2498,9 @@ let get_script prf = | `Sideff (`Ast (x,_)) -> find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next | `Sideff (`Id id) -> find acc id - | `Cmd {cast = x} -> find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next + | `Cmd {cast = x; ctac} when ctac -> (* skip non-tactics *) + find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next + | `Cmd _ -> find acc view.next | `Alias (id,_) -> find acc id | `Fork _ -> find acc view.next in @@ -2517,5 +2576,5 @@ let process_error_hook = Hooks.process_error_hook let interp_hook = Hooks.interp_hook let with_fail_hook = Hooks.with_fail_hook let unreachable_state_hook = Hooks.unreachable_state_hook - +let get_fix_exn () = !State.fix_exn_ref (* vim:set foldmethod=marker: *) |