diff options
Diffstat (limited to 'lib/options.ml')
| -rw-r--r-- | lib/options.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/lib/options.ml b/lib/options.ml index 80b4631233..afa419d679 100644 --- a/lib/options.ml +++ b/lib/options.ml @@ -10,6 +10,11 @@ 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 @@ -26,6 +31,8 @@ let xml_export = ref false let dont_load_proofs = ref false +let raw_print = ref false + let v7 = let transl = array_exists ((=) "-translate") Sys.argv in let v7 = array_exists ((=) "-v7") Sys.argv in @@ -66,11 +73,6 @@ let silently f x = let if_silent f x = if !silent then f x let if_verbose f x = if not !silent then f x -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 - (* The number of printed hypothesis in a goal *) let print_hyps_limit = ref (None : int option) |