diff options
author | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
commit | cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch) | |
tree | b7832bd5d412a5a5d69cb36ae2ded62c71124c22 /lib/flags.ml | |
parent | 113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff) |
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'lib/flags.ml')
-rw-r--r-- | lib/flags.ml | 67 |
1 files changed, 27 insertions, 40 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index 16ae0c64..928912e6 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -6,13 +6,18 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: flags.ml 11309 2008-08-06 10:30:35Z herbelin $ i*) +(*i $Id: flags.ml 11801 2009-01-18 20:11:41Z 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 +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 + let boot = ref false let batch_mode = ref false @@ -33,13 +38,10 @@ let raw_print = ref false let unicode_syntax = 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 +let beautify = ref false +let make_beautify f = beautify := f +let do_beautify () = !beautify +let beautify_file = ref false (* Silent / Verbose *) let silent = ref false @@ -47,16 +49,8 @@ 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 silently f x = with_option silent f x +let verbosely f x = without_option silent f x let if_silent f x = if !silent then f x let if_verbose f x = if not !silent then f x @@ -82,33 +76,13 @@ 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 - -(* Flags.for the virtual machine *) +(* 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 *) +(* Flags for external tools *) let subst_command_placeholder s t = let buff = Buffer.create (String.length s + String.length t) in @@ -127,3 +101,16 @@ let browser_cmd_fmt = Sys.getenv coq_netscape_remote_var with Not_found -> Coq_config.browser + +(* Options for changing coqlib *) +let coqlib_spec = ref false +let coqlib = ref Coq_config.coqlib + +(* Options for changing camlbin (used by coqmktop) *) +let camlbin_spec = ref false +let camlbin = ref Coq_config.camlbin + +(* Options for changing camlp4bin (used by coqmktop) *) +let camlp4bin_spec = ref false +let camlp4bin = ref Coq_config.camlp4bin + |