summaryrefslogtreecommitdiff
path: root/toplevel/metasyntax.mli
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
commit3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch)
treead89c6bb57ceee608fcba2bb3435b74e0f57919e /toplevel/metasyntax.mli
parent018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff)
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'toplevel/metasyntax.mli')
-rw-r--r--toplevel/metasyntax.mli55
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