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