summaryrefslogtreecommitdiff
path: root/lib/flags.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
commitcfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch)
treeb7832bd5d412a5a5d69cb36ae2ded62c71124c22 /lib/flags.ml
parent113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff)
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'lib/flags.ml')
-rw-r--r--lib/flags.ml67
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
+