1(* ===================================================================== *)
2(* FILE          : Globals.sml                                           *)
3(* DESCRIPTION   : Contains global flags for hol98.                      *)
4(*                                                                       *)
5(* AUTHOR        : (c) Konrad Slind, University of Calgary               *)
6(* DATE          : August 26, 1991                                       *)
7(*               : July 17, 1998                                         *)
8(*                                                                       *)
9(* ===================================================================== *)
10
11structure Globals :> Globals =
12struct
13
14(*---------------------------------------------------------------------------*
15 * Installation-specific information.                                        *
16 *---------------------------------------------------------------------------*)
17
18val HOLDIR = Systeml.HOLDIR
19
20(*---------------------------------------------------------------------------*
21 * Version information                                                       *
22 *---------------------------------------------------------------------------*)
23
24val release = Systeml.release
25val version = Systeml.version
26
27(*---------------------------------------------------------------------------*
28 * For showing assumptions in theorems                                       *
29 *---------------------------------------------------------------------------*)
30
31val show_assums = ref false
32
33(*---------------------------------------------------------------------------*
34 * For showing oracles used to prove theorems.                               *
35 *---------------------------------------------------------------------------*)
36
37val show_tags = ref false
38
39(*---------------------------------------------------------------------------*
40 * For showing the axioms used in the proof of a theorem.                    *
41 *---------------------------------------------------------------------------*)
42
43val show_axioms = ref true
44
45(*---------------------------------------------------------------------------*
46 * For showing the time taken to "scrub" the current theory of out-of-date   *
47 * items. For developers.                                                    *
48 *---------------------------------------------------------------------------*)
49
50val show_scrub = ref true
51
52(*---------------------------------------------------------------------------*
53 * Assignable function for printing errors.                                  *
54 *---------------------------------------------------------------------------*)
55
56fun outHOL_ERR_default {message,origin_function,origin_structure} =
57   (TextIO.output (TextIO.stdOut,
58                   "\nException raised at " ^ origin_structure ^ "." ^
59                   origin_function ^ ":\n" ^ message ^ "\n")
60    ; TextIO.flushOut TextIO.stdOut)
61
62val output_HOL_ERR = ref outHOL_ERR_default
63
64(*---------------------------------------------------------------------------*
65 * Prettyprinting flags                                                      *
66 *---------------------------------------------------------------------------*)
67
68val type_pp_prefix = ref "`" and type_pp_suffix = ref "`"
69val term_pp_prefix = ref "`" and term_pp_suffix = ref "`"
70val thm_pp_prefix = ref "|- " and thm_pp_suffix = ref ""
71
72(*---------------------------------------------------------------------------*
73 * Tells the prettyprinters how wide the page is.                            *
74 *---------------------------------------------------------------------------*)
75
76val linewidth = CoreReplVARS.linewidth
77
78(*---------------------------------------------------------------------------*
79 * Controls depth of printing for terms. Since the pp recursively decrements *
80 * this value when traversing a term, and since printing stops when the      *
81 * value is 0, the negative value means "print everything". Warning:         *
82 * this will work to negmaxint, but no guarantees after that.                *
83 *---------------------------------------------------------------------------*)
84
85val max_print_depth = ref ~1
86
87val pp_flags = {show_types = ref false, show_numeral_types = ref false}
88
89(*---------------------------------------------------------------------------*
90 * For prettyprinting type information in a term.                            *
91 *---------------------------------------------------------------------------*)
92
93val show_types = #show_types pp_flags
94val show_types_verbosely = ref false
95
96(*---------------------------------------------------------------------------*
97 * To make the system print out character suffixes on numerals to identify   *
98 * them as belonging to particular types.                                    *
99 *---------------------------------------------------------------------------*)
100
101val show_numeral_types = #show_numeral_types pp_flags
102
103val goal_line = ref "------------------------------------"
104
105(*---------------------------------------------------------------------------*
106 * At the end of type inference, HOL now guesses names for unconstrained     *
107 * type variables, if this flag is set.                                      *
108 *---------------------------------------------------------------------------*)
109
110val guessing_tyvars = ref true
111
112(*---------------------------------------------------------------------------*
113 * At the end of type inference, HOL will guess which instance of an         *
114 * overloaded constant to pick if there there is more than one choice, if    *
115 * this flag is set.                                                         *
116 *---------------------------------------------------------------------------*)
117
118val guessing_overloads = ref true
119
120(*---------------------------------------------------------------------------*
121 * If this flag is set, then the system will print a message when such       *
122 * guesses are made.                                                         *
123 *---------------------------------------------------------------------------*)
124
125val notify_on_tyvar_guess = ref true
126
127(*---------------------------------------------------------------------------*
128 * Whether or not to be strict about what name a type or constant has.       *
129 * Checked in Theory.new_type and Theory.new_constant.                       *
130 *---------------------------------------------------------------------------*)
131
132val checking_type_names  = ref true
133val checking_const_names = ref true
134
135(* ----------------------------------------------------------------------
136    The syntax used to highlight out-of-date constants in the
137    prettyprinters for types and terms - must generate unique names
138    because this determines the name of out-of-date constants, which
139    might otherwise overlap, and be identified.
140   ---------------------------------------------------------------------- *)
141
142val old =
143   let
144      val c = ref 0
145   in
146      fn s => String.concat ["old", Int.toString (!c), "->", s, "<-old"] before
147              c := !c + 1
148   end
149
150val print_thy_loads = ref false
151
152(* ----------------------------------------------------------------------
153    Flag telling us whether or not we're interactive.
154    If this is set, this allows for certain pieces of code to be a bit more
155    verbose.  It's set by std.prelude, so theory scripts and the like that
156    Holmake runs won't cause the printing of messages.
157   ---------------------------------------------------------------------- *)
158
159val interactive = ref false
160
161val hol_clock = Timer.startCPUTimer ()
162
163(*---------------------------------------------------------------------------*)
164(* The default directory where ML extracted from theory files is written.    *)
165(*---------------------------------------------------------------------------*)
166
167val emitMLDir = ref (Path.concat(HOLDIR,"src/emit/ML/"))
168val emitCAMLDir = ref (Path.concat(HOLDIR,"src/emit/Caml/"))
169
170end (* Globals *)
171