diff options
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 34 |
1 files changed, 20 insertions, 14 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index 4d7289c2..f52e17cc 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: notation.mli 11445 2008-10-11 16:42:46Z herbelin $ i*) +(*i $Id$ i*) (*i*) open Util @@ -39,9 +39,14 @@ val declare_scope : scope_name -> unit val current_scopes : unit -> scopes +(* Check where a scope is opened or not in a scope list, or in + * the current opened scopes *) +val scope_is_open_in_scopes : scope_name -> scopes -> bool +val scope_is_open : scope_name -> bool + (* Open scope *) -val open_close_scope : +val open_close_scope : (* locality *) bool * (* open *) bool * scope_name -> unit (* Extend a list of scopes *) @@ -60,8 +65,8 @@ val find_delimiters_scope : loc -> delimiters -> scope_name negative numbers are not supported, the interpreter must fail with an appropriate error message *) -type notation_location = dir_path * string -type required_module = section_path * string list +type notation_location = (dir_path * dir_path) * string +type required_module = full_path * string list type cases_pattern_status = bool (* true = use prim token in patterns *) type 'a prim_token_interpreter = @@ -81,19 +86,19 @@ val declare_string_interpreter : scope_name -> required_module -> val interp_prim_token : loc -> prim_token -> local_scopes -> rawconstr * (notation_location * scope_name option) -val interp_prim_token_cases_pattern : loc -> prim_token -> name -> +val interp_prim_token_cases_pattern : loc -> prim_token -> name -> local_scopes -> cases_pattern * (notation_location * scope_name option) (* Return the primitive token associated to a [term]/[cases_pattern]; raise [No_match] if no such token *) -val uninterp_prim_token : +val uninterp_prim_token : rawconstr -> scope_name * prim_token -val uninterp_prim_token_cases_pattern : +val uninterp_prim_token_cases_pattern : cases_pattern -> name * scope_name * prim_token -val availability_of_prim_token : - scope_name -> local_scopes -> delimiters option option +val availability_of_prim_token : + prim_token -> scope_name -> local_scopes -> delimiters option option (*s Declare and interpret back and forth a notation *) @@ -120,7 +125,7 @@ val uninterp_cases_pattern_notations : cases_pattern -> (* Test if a notation is available in the scopes *) (* context [scopes]; if available, the result is not None; the first *) (* argument is itself not None if a delimiters is needed *) -val availability_of_notation : scope_name option * notation -> local_scopes -> +val availability_of_notation : scope_name option * notation -> local_scopes -> (scope_name option * delimiters option) option (*s Declare and test the level of a (possibly uninterpreted) notation *) @@ -130,7 +135,7 @@ val level_of_notation : notation -> level (* raise [Not_found] if no level *) (*s** Miscellaneous *) -val interp_notation_as_global_reference : loc -> (global_reference -> bool) -> +val interp_notation_as_global_reference : loc -> (global_reference -> bool) -> notation -> delimiters option -> global_reference (* Checks for already existing notations *) @@ -138,7 +143,7 @@ val exists_notation_in_scope : scope_name option -> notation -> interpretation -> bool (* Declares and looks for scopes associated to arguments of a global ref *) -val declare_arguments_scope : +val declare_arguments_scope : bool (* true=local *) -> global_reference -> scope_name option list -> unit val find_arguments_scope : global_reference -> scope_name option list @@ -159,10 +164,11 @@ type symbol = val make_notation_key : symbol list -> notation val decompose_notation_key : notation -> symbol list -(* Prints scopes (expect a pure aconstr printer *) +(* Prints scopes (expects a pure aconstr printer) *) val pr_scope : (rawconstr -> std_ppcmds) -> scope_name -> std_ppcmds val pr_scopes : (rawconstr -> std_ppcmds) -> std_ppcmds -val locate_notation : (rawconstr -> std_ppcmds) -> notation -> std_ppcmds +val locate_notation : (rawconstr -> std_ppcmds) -> notation -> + scope_name option -> std_ppcmds val pr_visibility: (rawconstr -> std_ppcmds) -> scope_name option -> std_ppcmds |