diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqinit.ml | 8 | ||||
| -rw-r--r-- | toplevel/coqinit.mli | 2 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 19 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 18 | ||||
| -rw-r--r-- | toplevel/metasyntax.mli | 2 | ||||
| -rw-r--r-- | toplevel/usage.ml | 2 |
6 files changed, 37 insertions, 14 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 08cbe0640..652d0f7c6 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -136,3 +136,11 @@ let init_ocaml_path () = [ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ]; [ "tactics" ]; [ "toplevel" ]; [ "printing" ]; [ "intf" ]; [ "grammar" ]; [ "ide" ] ] + +let get_compat_version = function + | "8.3" -> Flags.V8_3 + | "8.2" -> Flags.V8_2 + | ("8.1" | "8.0") as s -> + msg_warning (strbrk ("Compatibility with version "^s^" not supported.")); + Flags.V8_2 + | s -> Errors.error ("Unknown compatibility version \""^s^"\".") diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index 43b1556d5..4461f721d 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -22,3 +22,5 @@ val init_load_path : unit -> unit val init_library_roots : unit -> unit val init_ocaml_path : unit -> unit + +val get_compat_version : string -> Flags.compat_version diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 6e5019adb..1a6867a51 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -125,13 +125,6 @@ let compile_files () = Vernac.compile v f) (List.rev !compile_list) -let set_compat_version = function - | "8.3" -> compat_version := Some V8_3 - | "8.2" -> compat_version := Some V8_2 - | "8.1" -> msg_warning (strbrk "Compatibility with version 8.1 not supported.") - | "8.0" -> msg_warning (strbrk "Compatibility with version 8.0 not supported.") - | s -> error ("Unknown compatibility version \""^s^"\".") - (*s options for the virtual machine *) let boxed_val = ref false @@ -158,6 +151,9 @@ let warning s = msg_warning (strbrk s) let ide_slave = ref false let filter_opts = ref false +let verb_compat_ntn = ref false +let no_compat_ntn = ref false + let parse_args arglist = let glob_opt = ref false in let rec parse = function @@ -249,9 +245,13 @@ let parse_args arglist = | "-debug" :: rem -> set_debug (); parse rem - | "-compat" :: v :: rem -> set_compat_version v; parse rem + | "-compat" :: v :: rem -> + Flags.compat_version := get_compat_version v; parse rem | "-compat" :: [] -> usage () + | "-verb-compat-notations" :: rem -> verb_compat_ntn := true; parse rem + | "-no-compat-notations" :: rem -> no_compat_ntn := true; parse rem + | "-vm" :: rem -> use_vm := true; parse rem | "-emacs" :: rem -> Flags.print_emacs := true; Pp.make_pp_emacs(); @@ -342,6 +342,9 @@ let init arglist = Mltop.init_known_plugins (); set_vm_opt (); engage (); + (* Be careful to set these variables after the inputstate *) + Syntax_def.set_verbose_compat_notations !verb_compat_ntn; + Syntax_def.set_compat_notations (not !no_compat_ntn); if (not !batch_mode|| !compile_list=[]) && Global.env_is_empty() then Option.iter Declaremods.start_library !toplevel_name; init_library_roots (); diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index fee4fef18..52722c9f5 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -770,7 +770,7 @@ let interp_modifiers modl = | SetAssoc a :: l -> if assoc <> None then error"An associativity is given more than once."; interp (Some a) level etyps format l - | SetOnlyParsing :: l -> + | SetOnlyParsing _ :: l -> onlyparsing := true; interp assoc level etyps format l | SetFormat s :: l -> @@ -783,8 +783,13 @@ let check_infix_modifiers modifiers = if t <> [] then error "Explicit entry level or type unexpected in infix notation." -let no_syntax_modifiers modifiers = - modifiers = [] or modifiers = [SetOnlyParsing] +let no_syntax_modifiers = function + | [] | [SetOnlyParsing _] -> true + | _ -> false + +let is_only_parsing = function + | [SetOnlyParsing _] -> true + | _ -> false (* Compute precedences from modifiers (or find default ones) *) @@ -1131,7 +1136,7 @@ let add_notation local c ((loc,df),modifiers) sc = let df' = if no_syntax_modifiers modifiers then (* No syntax data: try to rely on a previously declared rule *) - let onlyparse = modifiers=[SetOnlyParsing] in + let onlyparse = is_only_parsing modifiers in try add_notation_interpretation_core local df c sc onlyparse with NoSyntaxRule -> (* Try to determine a default syntax rule *) @@ -1209,6 +1214,9 @@ let add_syntactic_definition ident (vars,c) local onlyparse = let vars,pat = interp_notation_constr i_vars [] c in List.map (fun (id,(sc,kind)) -> (id,sc)) vars, pat in - let onlyparse = onlyparse or is_not_printable pat in + let onlyparse = match onlyparse with + | None when (is_not_printable pat) -> Some Flags.Current + | p -> p + in Syntax_def.declare_syntactic_definition local ident onlyparse (vars,pat) diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index f34b0ccae..22b16be23 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -52,7 +52,7 @@ val add_syntax_extension : (** Add a syntactic definition (as in "Notation f := ...") *) val add_syntactic_definition : identifier -> identifier list * constr_expr -> - bool -> bool -> unit + bool -> Flags.compat_version option -> unit (** Print the Camlp4 state of a grammar *) diff --git a/toplevel/usage.ml b/toplevel/usage.ml index dcf11354b..e1b70b52e 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -32,6 +32,8 @@ let print_usage_channel co command = \n -nois start with an empty state\ \n -outputstate f write state in file f.coq\ \n -compat X.Y provides compatibility support for Coq version X.Y\ +\n -verb-compat-notations be warned when using compatibility notations\ +\n -no-compat-notations get an error when using compatibility notations\ \n\ \n -load-ml-object f load ML object file f\ \n -load-ml-source f load ML file f\ |