system.ml

   1 (* ========================================================================= *)
   2 (* Some miscellaneous OCaml system hacking before we get started.            *)
   3 (*                                                                           *)
   4 (*              (c) Copyright, John Harrison 1998-2007                       *)
   5 (* ========================================================================= *)
   6
   7 Gc.set { (Gc.get()) with Gc.stack_limit = 16777216 };;
   8
   9 (* ------------------------------------------------------------------------- *)
  10 (* Make sure user interrupts generate an exception, not kill the process.    *)
  11 (* ------------------------------------------------------------------------- *)
  12
  13 Sys.catch_break true;;
  14
  15 (* ------------------------------------------------------------------------- *)
  16 (* Set up a quotation expander for the `...` quotes.                         *)
  17 (* This includes the case `;...` to support miz3, even if that isn't loaded. *)
  18 (* ------------------------------------------------------------------------- *)
  19
  20 let quotexpander s =
  21   if s = "" then failwith "Empty quotation" else
  22   let c = String.sub s 0 1 in
  23   if c = ":" then
  24     "parse_type \""^
  25     (String.escaped (String.sub s 1 (String.length s - 1)))^"\""
  26   else if c = ";" then "parse_qproof \""^(String.escaped s)^"\""
  27   else "parse_term \""^(String.escaped s)^"\"";;
  28
  29 Quotation.add "tot" (Quotation.ExStr (fun x -> quotexpander));;
  30
  31 (* ------------------------------------------------------------------------- *)
  32 (* Modify the lexical analysis of uppercase identifiers.                     *)
  33 (* ------------------------------------------------------------------------- *)
  34
  35 set_jrh_lexer;;
  36
  37 (* ------------------------------------------------------------------------- *)
  38 (* Load in the bignum library and set up printing in the toplevel.           *)
  39 (* ------------------------------------------------------------------------- *)
  40
  41 #load "nums.cma";;
  42
  43 include Num;;
  44
  45 let print_num n =
  46   Format.open_hbox();
  47   Format.print_string(string_of_num n);
  48   Format.close_box();;
  49
  50 #install_printer print_num;;