From 3a447d83226c4591e796e44933dad8278d97d683 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
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