lib/flags.ml


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132

(************************************************************************)
(*  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        *)
(************************************************************************)

(*i $Id: flags.ml 11077 2008-06-09 11:26:32Z herbelin $ i*)

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

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

(* 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

let warn = ref true
let make_warn flag = warn := flag;  ()
let if_warn f x = if !warn then f x

(* 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

(* 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 =
  let buff = Buffer.create (String.length s + String.length t) in
  let i = ref 0 in
  while (!i < String.length s) do
    if s.[!i] = '%' & !i+1 < String.length s & s.[!i+1] = 's'
    then (Buffer.add_string buff t;incr i)
    else Buffer.add_char buff s.[!i];
    incr i
  done;
  Buffer.contents buff

let browser_cmd_fmt =
 try
  let coq_netscape_remote_var = "COQREMOTEBROWSER" in
  Sys.getenv coq_netscape_remote_var
 with
  Not_found ->
   if Sys.os_type = "Win32"
   then "C:\\PROGRA~1\\INTERN~1\\IEXPLORE %s"
   else "firefox -remote \"OpenURL(%s,new-tab)\" || firefox %s &"