diff options
Diffstat (limited to 'lib/flags.ml')
-rw-r--r-- | lib/flags.ml | 56 |
1 files changed, 38 insertions, 18 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index 6b68a8f2..32c68b25 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -1,22 +1,20 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: flags.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) - let with_option o f x = let old = !o in o:=true; try let r = f x in o := old; r - with e -> o := old; raise e + with reraise -> o := old; raise reraise let without_option o f x = let old = !o in o:=false; try let r = f x in o := old; r - with e -> o := old; raise e + with reraise -> o := old; raise reraise let boot = ref false @@ -25,24 +23,34 @@ let batch_mode = ref false let debug = ref false let print_emacs = ref false -let print_emacs_safechar = ref false let term_quality = ref false let xml_export = ref false -let dont_load_proofs = ref false +type load_proofs = Force | Lazy | Dont + +let load_proofs = ref Lazy let raw_print = ref false +let record_print = ref true + (* Compatibility mode *) -type compat_version = V8_2 -let compat_version = ref None -let version_strictly_greater v = - match !compat_version with None -> true | Some v' -> v'>v +(* Current means no particular compatibility consideration. + For correct comparisons, this constructor should remain the last one. *) + +type compat_version = V8_2 | V8_3 | Current +let compat_version = ref Current +let version_strictly_greater v = !compat_version > v let version_less_or_equal v = not (version_strictly_greater v) +let pr_version = function + | V8_2 -> "8.2" + | V8_3 -> "8.3" + | Current -> "current" + (* Translate *) let beautify = ref false let make_beautify f = beautify := f @@ -86,12 +94,6 @@ let unsafe_set = ref Stringset.empty let add_unsafe s = unsafe_set := Stringset.add s !unsafe_set let is_unsafe s = Stringset.mem s !unsafe_set -(* Flags for the virtual machine *) - -let boxed_definitions = ref true -let set_boxed_definitions b = boxed_definitions := b -let boxed_definitions _ = !boxed_definitions - (* Flags for external tools *) let subst_command_placeholder s t = @@ -120,9 +122,21 @@ let is_standard_doc_url url = url = Coq_config.wwwrefman || url = wwwcompatprefix ^ String.sub Coq_config.wwwrefman n (n'-n) +(* same as in System, but copied here because of dependencies *) +let canonical_path_name p = + let current = Sys.getcwd () in + Sys.chdir p; + let result = Sys.getcwd () in + Sys.chdir current; + result + (* Options for changing coqlib *) let coqlib_spec = ref false -let coqlib = ref Coq_config.coqlib +let coqlib = ref ( + (* same as Envars.coqroot, but copied here because of dependencies *) + Filename.dirname + (canonical_path_name (Filename.dirname Sys.executable_name)) +) (* Options for changing camlbin (used by coqmktop) *) let camlbin_spec = ref false @@ -132,3 +146,9 @@ let camlbin = ref Coq_config.camlbin let camlp4bin_spec = ref false let camlp4bin = ref Coq_config.camlp4bin +(* Level of inlining during a functor application *) + +let default_inline_level = 100 +let inline_level = ref default_inline_level +let set_inline_level = (:=) inline_level +let get_inline_level () = !inline_level |