From 3a447d83226c4591e796e44933dad8278d97d683 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Fri, 5 Jan 2018 12:57:56 +0100 Subject: Brackets support single numbered goal selectors. This allows to focus on a sub-goal other than the first one without resorting to the `Focus` command. --- ide/coq_lex.mll | 4 +++- intf/vernacexpr.ml | 2 +- plugins/ltac/g_ltac.ml4 | 3 ++- printing/ppvernac.ml | 4 ++-- vernac/vernacentries.ml | 11 +++++------ 5 files changed, 13 insertions(+), 11 deletions(-) diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll index 8bfd937e3..a7e9003db 100644 --- a/ide/coq_lex.mll +++ b/ide/coq_lex.mll @@ -17,7 +17,9 @@ let space = [' ' '\n' '\r' '\t' '\012'] (* '\012' is form-feed *) -let undotted_sep = '{' | '}' | '-'+ | '+'+ | '*'+ +let number = [ '0'-'9' ]+ + +let undotted_sep = (number space* ':' space*)? '{' | '}' | '-'+ | '+'+ | '*'+ let dot_sep = '.' (space | eof) diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 5106e513b..bc7b0585d 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -451,7 +451,7 @@ type vernac_expr = | VernacUnfocus | VernacUnfocused | VernacBullet of bullet - | VernacSubproof of int option + | VernacSubproof of goal_selector option | VernacEndSubproof | VernacShow of showable | VernacCheckGuard diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index ebf6e450b..cc7ce339b 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -327,7 +327,8 @@ GEXTEND Gram | IDENT "all"; ":" -> SelectAll ] ] ; tactic_mode: - [ [ g = OPT toplevel_selector; tac = G_vernac.query_command -> tac g ] ] + [ [ g = OPT toplevel_selector; tac = G_vernac.query_command -> tac g + | g = OPT toplevel_selector; "{" -> Vernacexpr.VernacSubproof g ] ] ; command: [ [ IDENT "Proof"; "with"; ta = Pltac.tactic; diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index e88284fb1..27c46fe4e 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -91,7 +91,7 @@ open Decl_kinds let sep_end = function | VernacBullet _ - | VernacSubproof None + | VernacSubproof _ | VernacEndSubproof -> str"" | _ -> str"." @@ -1199,7 +1199,7 @@ open Decl_kinds | VernacSubproof None -> return (str "{") | VernacSubproof (Some i) -> - return (keyword "BeginSubproof" ++ spc () ++ int i) + return (Proof_bullet.pr_goal_selector i ++ str ":" ++ spc () ++ str "{") | VernacEndSubproof -> return (str "}") diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index ded0d97e6..bccde169f 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1846,11 +1846,8 @@ let vernac_unfocused () = user_err Pp.(str "The proof is not fully unfocused.") -(* BeginSubproof / EndSubproof. - BeginSubproof (vernac_subproof) focuses on the first goal, or the goal - given as argument. - EndSubproof (vernac_end_subproof) unfocuses from a BeginSubproof, provided - that the proof of the goal has been completed. +(* "{" focuses on the first goal, "n: {" focuses on the n-th goal + "}" unfocuses, provided that the proof of the goal has been completed. *) let subproof_kind = Proof.new_focus_kind () let subproof_cond = Proof.done_cond subproof_kind @@ -1859,7 +1856,9 @@ let vernac_subproof gln = Proof_global.simple_with_current_proof (fun _ p -> match gln with | None -> Proof.focus subproof_cond () 1 p - | Some n -> Proof.focus subproof_cond () n p) + | Some (SelectNth n) -> Proof.focus subproof_cond () n p + | _ -> user_err ~hdr:"bracket_selector" + (str "Brackets only support the single numbered goal selector.")) let vernac_end_subproof () = Proof_global.simple_with_current_proof (fun _ p -> -- cgit v1.2.3 From e10b7ebe0eb05c01096d022f6f09e6c1562d5562 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Fri, 5 Jan 2018 13:06:17 +0100 Subject: Documentation and CHANGES for bracket with goal selector. --- CHANGES | 6 ++++++ doc/refman/RefMan-pro.tex | 9 +++++++++ 2 files changed, 15 insertions(+) diff --git a/CHANGES b/CHANGES index cbaa2c5e2..14b1b3fac 100644 --- a/CHANGES +++ b/CHANGES @@ -38,6 +38,12 @@ Tactics - Added tactics restart_timer, finish_timing, and time_constr as an experimental way of timing Ltac's evaluation phase +Focusing + +- Focusing bracket `{` now supports single-numbered goal selector, + e.g. `2: {` will focus on the second sub-goal. As usual, unfocus + with `}` once the sub-goal is fully solved. + Vernacular Commands - The deprecated Coercion Local, Open Local Scope, Notation Local syntax diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 1d3311edc..2bd50daf3 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -320,10 +320,19 @@ Note that when a focused goal is proved a message is displayed together with a suggestion about the right bullet or {\tt \}} to unfocus it or focus the next one. +\begin{Variants} + +\item {\tt {\num}: \{}\\ +This focuses on the $\num^{th}$ subgoal to prove. + +\end{Variants} + \begin{ErrMsgs} \item \errindex{This proof is focused, but cannot be unfocused this way} You are trying to use {\tt \}} but the current subproof has not been fully solved. +\item \errindex{No such goal} +\item \errindex{Brackets only support the single numbered goal selector} \item see also error message about bullets below. \end{ErrMsgs} -- cgit v1.2.3 From 54083a2a8e6c4c2083717ac18c7b4dc351ab0f7d Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 15 Jan 2018 13:17:14 +0100 Subject: Add test-suite file for bracket with goal selector. --- test-suite/success/BracketsWithGoalSelector.v | 10 ++++++++++ 1 file changed, 10 insertions(+) create mode 100644 test-suite/success/BracketsWithGoalSelector.v diff --git a/test-suite/success/BracketsWithGoalSelector.v b/test-suite/success/BracketsWithGoalSelector.v new file mode 100644 index 000000000..dd032767c --- /dev/null +++ b/test-suite/success/BracketsWithGoalSelector.v @@ -0,0 +1,10 @@ +Goal forall A B, B \/ A -> A \/ B. +Proof. + intros * [HB | HA]. + 2: { + left. + exact HA. + } + right. + exact HB. +Qed. -- cgit v1.2.3 From 1856d60057ac9096c791d71d4282c0cdfef85913 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 15 Jan 2018 13:54:01 +0100 Subject: More tests on brackets with goal selectors (including failures). --- test-suite/success/BracketsWithGoalSelector.v | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/test-suite/success/BracketsWithGoalSelector.v b/test-suite/success/BracketsWithGoalSelector.v index dd032767c..ed035f521 100644 --- a/test-suite/success/BracketsWithGoalSelector.v +++ b/test-suite/success/BracketsWithGoalSelector.v @@ -4,7 +4,13 @@ Proof. 2: { left. exact HA. + Fail right. (* No such goal. Try unfocusing with "}". *) + } + Fail 2: { (* Non-existent goal. *) + idtac. (* The idtac is to get a dot, so that IDEs know to stop there. *) + 1:{ (* Syntactic test: no space before bracket. *) + right. + exact HB. +Fail Qed. } - right. - exact HB. Qed. -- cgit v1.2.3