diff options
Diffstat (limited to 'toplevel/metasyntax.mli')
| -rw-r--r-- | toplevel/metasyntax.mli | 39 |
1 files changed, 22 insertions, 17 deletions
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index fefc0b27..a0680693 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -6,10 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: metasyntax.mli 11481 2008-10-20 19:23:51Z herbelin $ i*) +(*i $Id$ i*) (*i*) open Util +open Names open Libnames open Ppextend open Extend @@ -23,16 +24,16 @@ val add_token_obj : string -> unit (* Adding a tactic notation in the environment *) -val add_tactic_notation : - int * grammar_production list * raw_tactic_expr -> unit +val add_tactic_notation : + int * grammar_tactic_prod_item_expr list * raw_tactic_expr -> unit (* Adding a (constr) notation in the environment*) -val add_infix : locality_flag -> (string * syntax_modifier list) -> - reference -> scope_name option -> unit +val add_infix : locality_flag -> (lstring * syntax_modifier list) -> + constr_expr -> scope_name option -> unit val add_notation : locality_flag -> constr_expr -> - (string * syntax_modifier list) -> scope_name option -> unit + (lstring * syntax_modifier list) -> scope_name option -> unit (* Declaring delimiter keys and default scopes *) @@ -41,22 +42,26 @@ val add_class_scope : scope_name -> Classops.cl_typ -> 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 : + (lstring * constr_expr * scope_name option) -> unit -(* Add only the parsing/printing rule of a notation *) +(* Add a notation interpretation for supporting the "where" clause *) -val add_syntax_extension : - locality_flag -> (string * syntax_modifier list) -> unit +val set_notation_for_interpretation : Constrintern.full_internalization_env -> + (lstring * constr_expr * scope_name option) -> unit -(* Print the Camlp4 state of a grammar *) +(* Add only the parsing/printing rule of a notation *) -val print_grammar : string -> unit +val add_syntax_extension : + locality_flag -> (lstring * syntax_modifier list) -> unit + +(* Add a syntactic definition (as in "Notation f := ...") *) -(* Removes quotes in a notation *) +val add_syntactic_definition : identifier -> identifier list * constr_expr -> + bool -> bool -> unit -val standardize_locatable_notation : string -> string +(* Print the Camlp4 state of a grammar *) -(* Evaluate whether a notation is not printable *) +val print_grammar : string -> unit -val is_not_printable : aconstr -> bool +val check_infix_modifiers : syntax_modifier list -> unit |