diff options
| -rw-r--r-- | CHANGES | 1 | ||||
| -rw-r--r-- | doc/refman/RefMan-pro.tex | 6 | ||||
| -rw-r--r-- | parsing/g_proofs.ml4 | 30 |
3 files changed, 33 insertions, 4 deletions
@@ -60,6 +60,7 @@ 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. + The `Focus` and `Unfocus` commands are now deprecated. Vernacular Commands diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 0113c8df3..bd74a40d7 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -298,13 +298,17 @@ subgoals which clutter your screen. \begin{Variant} \item {\tt Focus {\num}.}\\ This focuses the attention on the $\num^{th}$ subgoal to prove. - \end{Variant} +\emph{This command is deprecated since 8.8: prefer the use of bullets or + focusing brackets instead, including {\tt {\num}: \{}}. + \subsection[\tt Unfocus.]{\tt Unfocus.\comindex{Unfocus}} This command restores to focus the goal that were suspended by the last {\tt Focus} command. +\emph{This command is deprecated since 8.8.} + \subsection[\tt Unfocused.]{\tt Unfocused.\comindex{Unfocused}} Succeeds in the proof if fully unfocused, fails if there are some goals out of focus. diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 482373150..44f46578c 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -19,6 +19,24 @@ let thm_token = G_vernac.thm_token let hint = Gram.entry_create "hint" +let warn_deprecated_focus = + CWarnings.create ~name:"deprecated-focus" ~category:"deprecated" + (fun () -> + Pp.strbrk + "The Focus command is deprecated; use bullets or focusing brackets instead" + ) + +let warn_deprecated_focus_n n = + CWarnings.create ~name:"deprecated-focus" ~category:"deprecated" + (fun () -> + Pp.(str "The Focus command is deprecated;" ++ spc () + ++ str "use '" ++ int n ++ str ": {' instead") + ) + +let warn_deprecated_unfocus = + CWarnings.create ~name:"deprecated-unfocus" ~category:"deprecated" + (fun () -> Pp.strbrk "The Unfocus command is deprecated") + (* Proof commands *) GEXTEND Gram GLOBAL: hint command; @@ -49,9 +67,15 @@ GEXTEND Gram | IDENT "Undo" -> VernacUndo 1 | IDENT "Undo"; n = natural -> VernacUndo n | IDENT "Undo"; IDENT "To"; n = natural -> VernacUndoTo n - | IDENT "Focus" -> VernacFocus None - | IDENT "Focus"; n = natural -> VernacFocus (Some n) - | IDENT "Unfocus" -> VernacUnfocus + | IDENT "Focus" -> + warn_deprecated_focus ~loc:!@loc (); + VernacFocus None + | IDENT "Focus"; n = natural -> + warn_deprecated_focus_n n ~loc:!@loc (); + VernacFocus (Some n) + | IDENT "Unfocus" -> + warn_deprecated_unfocus ~loc:!@loc (); + VernacUnfocus | IDENT "Unfocused" -> VernacUnfocused | IDENT "Show" -> VernacShow (ShowGoal OpenSubgoals) | IDENT "Show"; n = natural -> VernacShow (ShowGoal (NthGoal n)) |