diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 11:24:27 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 11:24:27 +0100 |
| commit | c5432539927de8a94d5c549d288b95b7215390b9 (patch) | |
| tree | a894769d27c70c780f684ff63b5e547556186a91 /parsing | |
| parent | 76058420ec0ea037504adf0af213d0542bd7c1c3 (diff) | |
| parent | ba0a37d773c5d42f96b3b88714767ba2e7fb7a3b (diff) | |
Merge PR #6909: Deprecate Focus and Unfocus
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_proofs.ml4 | 30 |
1 files changed, 27 insertions, 3 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 430d18893..e393c2bbf 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -21,6 +21,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; @@ -51,9 +69,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)) |