diff options
| -rw-r--r-- | intf/vernacexpr.mli | 1 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 1 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 1 | ||||
| -rw-r--r-- | proofs/pfedit.ml | 3 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 1 | ||||
| -rw-r--r-- | proofs/proofview.ml | 17 | ||||
| -rw-r--r-- | proofs/proofview.mli | 2 |
7 files changed, 25 insertions, 1 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index b784bc433..009ec543c 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -30,6 +30,7 @@ type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation similar, they do not seem to mean the same thing. *) type goal_selector = | SelectNth of int + | SelectId of Id.t | SelectAll | SelectAllParallel diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 9fb7c8926..955179ba0 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -127,6 +127,7 @@ GEXTEND Gram selector: [ [ n=natural; ":" -> SelectNth n + | "["; id = ident; "]"; ":" -> SelectId id | IDENT "all" ; ":" -> SelectAll | IDENT "par" ; ":" -> SelectAllParallel ] ] ; diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 930166524..b7ac274b7 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -769,6 +769,7 @@ let rec pr_vernac = function | VernacSolve (i,tac,deftac) -> let pr_goal_selector = function | SelectNth i -> int i ++ str":" + | SelectId id -> pr_id id ++ str":" | SelectAll -> str"all" ++ str":" | SelectAllParallel -> str"par" in diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 49195aecc..1b0b2f401 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -94,6 +94,7 @@ let solve ?with_end_tac gi tac pr = | Some etac -> Proofview.tclTHEN tac etac in let tac = match gi with | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i tac + | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id tac | Vernacexpr.SelectAll -> tac | Vernacexpr.SelectAllParallel -> Errors.anomaly(str"SelectAllParallel not handled by Stm") @@ -101,7 +102,7 @@ let solve ?with_end_tac gi tac pr = Proof.run_tactic (Global.env ()) tac pr with | Proof_global.NoCurrentProof -> Errors.error "No focused proof" - | Proofview.IndexOutOfRange -> + | Proofview.IndexOutOfRange -> match gi with | Vernacexpr.SelectNth i -> let msg = str "No such goal: " ++ int i ++ str "." in Errors.errorlabstrm "" msg diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 82e176f97..1994922a9 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -528,6 +528,7 @@ let get_default_goal_selector () = !default_goal_selector let print_goal_selector = function | Vernacexpr.SelectAll -> "all" | Vernacexpr.SelectNth i -> string_of_int i + | Vernacexpr.SelectId id -> Id.to_string id | Vernacexpr.SelectAllParallel -> "par" let parse_goal_selector = function diff --git a/proofs/proofview.ml b/proofs/proofview.ml index a5cb2edb8..bc6ce4fc6 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -330,6 +330,23 @@ let tclFOCUS_gen nosuchgoal i j t = let tclFOCUS i j t = tclFOCUS_gen (tclZERO (NoSuchGoals (j+1-i))) i j t let tclTRYFOCUS i j t = tclFOCUS_gen (tclUNIT ()) i j t +let tclFOCUSID id t = + let (>>=) = Proof.bind in + let (>>) = Proof.seq in + Proof.get >>= fun initial -> + let rec aux n = function + | [] -> tclZERO (NoSuchGoals 1) + | g::l -> + if Names.Id.equal (Goal.goal_ident initial.solution g) id then + let (focused,context) = focus n n initial in + Proof.set focused >> + t >>= fun result -> + Proof.modify (fun next -> unfocus context next) >> + Proof.ret result + else + aux (n+1) l in + aux 1 initial.comb + (* Dispatch tacticals are used to apply a different tactic to each goal under consideration. They come in two flavours: diff --git a/proofs/proofview.mli b/proofs/proofview.mli index b1ff30ee9..3b2dd7ccd 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -197,6 +197,8 @@ val tclEXACTLY_ONCE : exn -> 'a tactic -> 'a tactic exception NoSuchGoals of int val tclFOCUS : int -> int -> 'a tactic -> 'a tactic +val tclFOCUSID : Names.Id.t -> 'a tactic -> 'a tactic + (* Focuses a tactic at a range of subgoals, found by their indices. The other goals are restored to the focus when the tactic is done. |