diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-04-20 23:24:02 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-04-24 16:44:41 +0200 |
| commit | f3515efc26a693f4c525ad91c37c982f4c96e6ec (patch) | |
| tree | 6e74da53a761857bf905b5f43c498b3a4aac0fc0 | |
| parent | 65578a55b81252e2c4b006728522839a9e37cd5c (diff) | |
Factorizing the declaration of ML notation printing in Tacentries.
| -rw-r--r-- | grammar/tacextend.ml4 | 13 | ||||
| -rw-r--r-- | ltac/tacentries.ml | 8 |
2 files changed, 8 insertions, 13 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 2ef30f299..e52770aa2 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -56,15 +56,6 @@ let make_prod_item = function let mlexpr_of_clause cl = mlexpr_of_list (fun (a,_,_) -> mlexpr_of_list make_prod_item a) cl -let make_one_printing_rule (pt,_,e) = - let level = mlexpr_of_int 0 in (* only level 0 supported here *) - let loc = MLast.loc_of_expr e in - let prods = mlexpr_of_list make_prod_item pt in - <:expr< { Pptactic.pptac_level = $level$; - pptac_prods = $prods$ } >> - -let make_printing_rule r = mlexpr_of_list make_one_printing_rule r - (** Special treatment of constr entries *) let is_constr_gram = function | ExtTerminal _ -> false @@ -118,15 +109,13 @@ let declare_tactic loc s c cl = match cl with TacML tactic. *) let entry = mlexpr_of_string s in let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in - let pp = make_printing_rule cl in let gl = mlexpr_of_clause cl in let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ $gl$ >> in declare_str_items loc [ <:str_item< do { try do { Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc s cl$); - Mltop.declare_cache_obj $obj$ $plugin_name$; - Pptactic.declare_ml_tactic_pprule $se$ (Array.of_list $pp$); } + Mltop.declare_cache_obj $obj$ $plugin_name$; } with [ e when Errors.noncritical e -> Pp.msg_warning (Pp.app diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index 46e48c695..a3e15866e 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -360,7 +360,13 @@ let extend_atomic_tactic name entries = List.iteri add_atomic entries let cache_ml_tactic_notation (_, obj) = - extend_ml_tactic_grammar obj.mltacobj_name obj.mltacobj_prod + extend_ml_tactic_grammar obj.mltacobj_name obj.mltacobj_prod; + let pp_rule prods = { + Pptactic.pptac_level = 0 (* only level 0 supported here *); + pptac_prods = prods; + } in + let pp_rules = Array.map_of_list pp_rule obj.mltacobj_prod in + Pptactic.declare_ml_tactic_pprule obj.mltacobj_name pp_rules let open_ml_tactic_notation i obj = if Int.equal i 1 then cache_ml_tactic_notation obj |