diff options
Diffstat (limited to 'toplevel/metasyntax.mli')
| -rw-r--r-- | toplevel/metasyntax.mli | 55 |
1 files changed, 25 insertions, 30 deletions
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index be90cd7a..71522567 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: metasyntax.mli,v 1.26.2.1 2004/07/16 19:31:49 herbelin Exp $ i*) +(*i $Id: metasyntax.mli 7732 2005-12-26 13:51:24Z herbelin $ i*) (*i*) open Util @@ -15,49 +15,44 @@ open Ppextend open Extend open Tacexpr open Vernacexpr -open Symbols +open Notation open Topconstr (*i*) -(* Adding grammar and pretty-printing objects in the environment *) +val add_token_obj : string -> unit -val add_syntax_obj : string -> raw_syntax_entry list -> unit +(* Adding a tactic notation in the environment *) -val add_grammar_obj : string -> raw_grammar_entry list -> unit -val add_token_obj : string -> unit -val add_tactic_grammar : - (string * (string * grammar_production list) * raw_tactic_expr) list -> unit +val add_tactic_notation : + int * grammar_production list * raw_tactic_expr -> unit + +(* Adding a (constr) notation in the environment*) val add_infix : locality_flag -> (string * syntax_modifier list) -> - reference -> (string * syntax_modifier list) option -> - scope_name option -> unit -val add_distfix : locality_flag -> - grammar_associativity -> precedence -> string -> reference - -> scope_name option -> unit -val translate_distfix : grammar_associativity -> string -> reference -> - Gramext.g_assoc * string * constr_expr + reference -> scope_name option -> unit + +val add_notation : locality_flag -> constr_expr -> + (string * syntax_modifier list) -> scope_name option -> unit + +(* Declaring delimiter keys and default scopes *) val add_delimiters : scope_name -> string -> unit val add_class_scope : scope_name -> Classops.cl_typ -> unit -val add_notation : locality_flag -> constr_expr - -> (string * syntax_modifier list) option - -> (string * syntax_modifier list) option - -> scope_name option -> unit +(* Add only the interpretation of a notation that already has pa/pp rules *) -val add_notation_interpretation : string -> Constrintern.implicits_env - -> constr_expr -> scope_name option -> unit +val add_notation_interpretation : string -> Constrintern.implicits_env -> + constr_expr -> scope_name option -> unit -val add_syntax_extension : locality_flag - -> (string * syntax_modifier list) option - -> (string * syntax_modifier list) option -> unit +(* Add only the parsing/printing rule of a notation *) -val print_grammar : string -> string -> unit +val add_syntax_extension : + locality_flag -> (string * syntax_modifier list) -> unit -val merge_modifiers : Gramext.g_assoc option -> int option -> - syntax_modifier list -> syntax_modifier list +(* Print the Camlp4 state of a grammar *) + +val print_grammar : string -> string -> unit -val interp_infix_modifiers : syntax_modifier list -> - Gramext.g_assoc option * precedence option * bool * string located option +(* Removes quotes in a notation *) -val standardise_locatable_notation : string -> string +val standardize_locatable_notation : string -> string |