diff options
author | 2008-07-25 15:12:53 +0200 | |
---|---|---|
committer | 2008-07-25 15:12:53 +0200 | |
commit | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch) | |
tree | dabcac548e299fee1da464c93b3dba98484f45b1 /lib/options.ml | |
parent | 2281410e38ef99d025ea77194585a9bc019fdaa9 (diff) |
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'lib/options.ml')
-rw-r--r-- | lib/options.ml | 124 |
1 files changed, 0 insertions, 124 deletions
diff --git a/lib/options.ml b/lib/options.ml deleted file mode 100644 index 53a7e9cf..00000000 --- a/lib/options.ml +++ /dev/null @@ -1,124 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* $Id: options.ml 10105 2007-08-30 16:53:32Z herbelin $ *) - -open Util - -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 - -let boot = ref false - -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 - -let raw_print = ref false - -(* Translate *) -let translate = ref false -let make_translate f = translate := f -let do_translate () = !translate -let translate_file = ref false - -(* True only when interning from pp*new.ml *) -let translate_syntax = ref false - -(* Silent / Verbose *) -let silent = ref false -let make_silent flag = silent := flag; () -let is_silent () = !silent -let is_verbose () = not !silent - -let silently f x = - let oldsilent = !silent in - try - silent := true; - let rslt = f x in - silent := oldsilent; - rslt - with e -> begin - silent := oldsilent; raise e - end - -let if_silent f x = if !silent then f x -let if_verbose f x = if not !silent then f x - -let hash_cons_proofs = ref true - -(* The number of printed hypothesis in a goal *) - -let print_hyps_limit = ref (None : int option) -let set_print_hyps_limit n = print_hyps_limit := n -let print_hyps_limit () = !print_hyps_limit - -(* A list of the areas of the system where "unsafe" operation - * has been requested *) - -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 - -(* Dump of globalization (to be used by coqdoc) *) - -let dump = ref false -let dump_file = ref "" -let dump_into_file f = dump := true; dump_file := f - -let dump_buffer = Buffer.create 8192 - -let dump_string = Buffer.add_string dump_buffer - -let dump_it () = - if !dump then begin - let mode = [Open_wronly; Open_append; Open_creat] in - let c = open_out_gen mode 0o666 !dump_file in - output_string c (Buffer.contents dump_buffer); - close_out c - end - -let _ = at_exit dump_it - -(* Options for the virtual machine *) - -let boxed_definitions = ref true -let set_boxed_definitions b = boxed_definitions := b -let boxed_definitions _ = !boxed_definitions - -(* Options for external tools *) - -let browser_cmd_fmt = - try - let coq_netscape_remote_var = "COQREMOTEBROWSER" in - let coq_netscape_remote = Sys.getenv coq_netscape_remote_var in - let i = Util.string_index_from coq_netscape_remote 0 "%s" in - let pre = String.sub coq_netscape_remote 0 i in - let post = String.sub coq_netscape_remote (i + 2) - (String.length coq_netscape_remote - (i + 2)) in - if Util.string_string_contains ~where:post ~what:"%s" then - error ("The environment variable \"" ^ - coq_netscape_remote_var ^ - "\" must contain exactly one placeholder \"%s\".") - else pre,post - with - Not_found -> - if Sys.os_type = "Win32" - then "C:\\PROGRA~1\\INTERN~1\\IEXPLORE ", "" - else "firefox -remote \"OpenURL(", ")\"" |