diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-16 19:27:00 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-19 01:42:01 +0100 |
commit | 5c8fc9aebe072237a65fc9ed7acf8ae559a78243 (patch) | |
tree | f45c69234da230de8901112dd5936dce4ed1fe6e | |
parent | 5bce635ad876bde78a7ffabc3e781112e5418a65 (diff) |
Moving the parsing of the Ltac proof mode to G_ltac.
-rw-r--r-- | parsing/g_ltac.ml4 | 42 | ||||
-rw-r--r-- | parsing/g_vernac.ml4 | 44 | ||||
-rw-r--r-- | test-suite/bugs/opened/3410.v | 1 | ||||
-rw-r--r-- | test-suite/ide/undo013.fake | 2 | ||||
-rw-r--r-- | test-suite/ide/undo014.fake | 2 | ||||
-rw-r--r-- | test-suite/ide/undo015.fake | 2 | ||||
-rw-r--r-- | test-suite/ide/undo016.fake | 2 |
7 files changed, 47 insertions, 48 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index e4ca936a6..35a9fede1 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Util open Pp open Compat open Constrexpr @@ -36,11 +37,35 @@ let reference_to_id = function Errors.user_err_loc (loc, "", str "This expression should be a simple identifier.") +let tactic_mode = Gram.entry_create "vernac:tactic_command" +let selector = Gram.entry_create "vernac:selector" + +(* Registers the Classic Proof Mode (which uses [tactic_mode] as a parser for + proof editing and changes nothing else). Then sets it as the default proof mode. *) +let _ = + let mode = { + Proof_global.name = "Classic"; + set = (fun () -> set_command_entry tactic_mode); + reset = (fun () -> set_command_entry Pcoq.Vernac_.noedit_mode); + } in + Proof_global.register_proof_mode mode + +(* Hack to parse "[ id" without dropping [ *) +let test_bracket_ident = + Gram.Entry.of_parser "test_bracket_ident" + (fun strm -> + match get_tok (stream_nth 0 strm) with + | KEYWORD "[" -> + (match get_tok (stream_nth 1 strm) with + | IDENT _ -> () + | _ -> raise Stream.Failure) + | _ -> raise Stream.Failure) + (* Tactics grammar rules *) GEXTEND Gram GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg - constr_may_eval constr_eval; + tactic_mode constr_may_eval constr_eval selector; tactic_then_last: [ [ "|"; lta = LIST0 OPT tactic_expr SEP "|" -> @@ -262,4 +287,19 @@ GEXTEND Gram tactic: [ [ tac = tactic_expr -> tac ] ] ; + selector: + [ [ n=natural; ":" -> Vernacexpr.SelectNth n + | test_bracket_ident; "["; id = ident; "]"; ":" -> Vernacexpr.SelectId id + | IDENT "all" ; ":" -> Vernacexpr.SelectAll + | IDENT "par" ; ":" -> Vernacexpr.SelectAllParallel ] ] + ; + tactic_mode: + [ [ g = OPT selector; + tac = G_vernac.subgoal_command -> tac g + | g = OPT selector; info = OPT [IDENT "Info";n=natural -> n]; + tac = Tactic.tactic; use_dft_tac = [ "." -> false | "..." -> true ] -> + let g = Option.default (Proof_global.get_default_goal_selector ()) g in + Vernacexpr.VernacSolve (g, info, tac, use_dft_tac) + ] ] + ; END diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 2eb590132..c89238d29 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -34,7 +34,6 @@ let _ = List.iter Lexer.add_keyword vernac_kw let query_command = Gram.entry_create "vernac:query_command" -let tactic_mode = Gram.entry_create "vernac:tactic_command" let subprf = Gram.entry_create "vernac:subprf" let class_rawexpr = Gram.entry_create "vernac:class_rawexpr" @@ -47,16 +46,6 @@ let subgoal_command = Gram.entry_create "proof_mode:subgoal_command" let instance_name = Gram.entry_create "vernac:instance_name" let section_subset_expr = Gram.entry_create "vernac:section_subset_expr" -(* Registers the Classic Proof Mode (which uses [tactic_mode] as a parser for - proof editing and changes nothing else). Then sets it as the default proof mode. *) -let set_tactic_mode () = set_command_entry tactic_mode -let set_noedit_mode () = set_command_entry noedit_mode -let _ = Proof_global.register_proof_mode {Proof_global. - name = "Classic" ; - set = set_tactic_mode ; - reset = set_noedit_mode - } - let make_bullet s = let n = String.length s in match s.[0] with @@ -65,19 +54,8 @@ let make_bullet s = | '*' -> Star n | _ -> assert false -(* Hack to parse "[ id" without dropping [ *) -let test_bracket_ident = - Gram.Entry.of_parser "test_bracket_ident" - (fun strm -> - match get_tok (stream_nth 0 strm) with - | KEYWORD "[" -> - (match get_tok (stream_nth 1 strm) with - | IDENT _ -> () - | _ -> raise Stream.Failure) - | _ -> raise Stream.Failure) - GEXTEND Gram - GLOBAL: vernac gallina_ext tactic_mode noedit_mode subprf subgoal_command; + GLOBAL: vernac gallina_ext noedit_mode subprf subgoal_command; vernac: FIRST [ [ IDENT "Time"; c = located_vernac -> VernacTime c | IDENT "Redirect"; s = ne_string; c = located_vernac -> VernacRedirect (s, c) @@ -125,18 +103,6 @@ GEXTEND Gram [ [ c = subgoal_command -> c None] ] ; - selector: - [ [ n=natural; ":" -> SelectNth n - | test_bracket_ident; "["; id = ident; "]"; ":" -> SelectId id - | IDENT "all" ; ":" -> SelectAll - | IDENT "par" ; ":" -> SelectAllParallel ] ] - ; - - tactic_mode: - [ [ gln = OPT selector; - tac = subgoal_command -> tac gln ] ] - ; - subprf: [ [ s = BULLET -> VernacBullet (make_bullet s) | "{" -> VernacSubproof None @@ -151,13 +117,7 @@ GEXTEND Gram | None -> c None | _ -> VernacError (UserError ("",str"Typing and evaluation commands, cannot be used with the \"all:\" selector.")) - end - | info = OPT [IDENT "Info";n=natural -> n]; - tac = Tactic.tactic; - use_dft_tac = [ "." -> false | "..." -> true ] -> - (fun g -> - let g = Option.default (Proof_global.get_default_goal_selector ()) g in - VernacSolve(g,info,tac,use_dft_tac)) ] ] + end ] ] ; located_vernac: [ [ v = vernac -> !@loc, v ] ] diff --git a/test-suite/bugs/opened/3410.v b/test-suite/bugs/opened/3410.v deleted file mode 100644 index 0d259181a..000000000 --- a/test-suite/bugs/opened/3410.v +++ /dev/null @@ -1 +0,0 @@ -Fail repeat match goal with H:_ |- _ => setoid_rewrite X in H end. diff --git a/test-suite/ide/undo013.fake b/test-suite/ide/undo013.fake index f44156aa3..921a9d0f0 100644 --- a/test-suite/ide/undo013.fake +++ b/test-suite/ide/undo013.fake @@ -23,5 +23,5 @@ ADD { Qed. } ADD { apply H. } # </replay> ADD { Qed. } -QUERY { Fail idtac. } +QUERY { Fail Show. } QUERY { Check (aa,bb,cc). } diff --git a/test-suite/ide/undo014.fake b/test-suite/ide/undo014.fake index 6d58b061e..f5fe77470 100644 --- a/test-suite/ide/undo014.fake +++ b/test-suite/ide/undo014.fake @@ -22,5 +22,5 @@ ADD { destruct H. } ADD { Qed. } ADD { apply H. } ADD { Qed. } -QUERY { Fail idtac. } +QUERY { Fail Show. } QUERY { Check (aa,bb,cc). } diff --git a/test-suite/ide/undo015.fake b/test-suite/ide/undo015.fake index ac17985aa..a1e5c947b 100644 --- a/test-suite/ide/undo015.fake +++ b/test-suite/ide/undo015.fake @@ -25,5 +25,5 @@ ADD { destruct H. } ADD { Qed. } ADD { apply H. } ADD { Qed. } -QUERY { Fail idtac. } +QUERY { Fail Show. } QUERY { Check (aa,bb,cc). } diff --git a/test-suite/ide/undo016.fake b/test-suite/ide/undo016.fake index bdb81ecd9..f9414c1ea 100644 --- a/test-suite/ide/undo016.fake +++ b/test-suite/ide/undo016.fake @@ -27,5 +27,5 @@ ADD { destruct H. } ADD { Qed. } ADD { apply H. } ADD { Qed. } -QUERY { Fail idtac. } +QUERY { Fail Show. } QUERY { Check (aa,bb,cc). } |