system.ml.patch

7,14d6
< Gc.set { (Gc.get()) with Gc.stack_limit = 16777216 };;
< 
< (* ------------------------------------------------------------------------- *)
< (* Make sure user interrupts generate an exception, not kill the process.    *)
< (* ------------------------------------------------------------------------- *)
< 
< Sys.catch_break true;;
< 
24,55c16,24
<   let c = String.sub s 0 1 in
<   if c = ":" then
<     "parse_type \""^
<     (String.escaped (String.sub s 1 (String.length s - 1)))^"\""
<   else if c = ";" then "parse_qproof \""^(String.escaped s)^"\"" else
<   let n = String.length s - 1 in
<   if String.sub s n 1 = ":"
<   then "\""^(String.escaped (String.sub s 0 n))^"\""
<   else "parse_term \""^(String.escaped s)^"\"";;
< 
< Quotation.add "tot" (Quotation.ExStr (fun x -> quotexpander));;
< 
< (* ------------------------------------------------------------------------- *)
< (* Modify the lexical analysis of uppercase identifiers.                     *)
< (* ------------------------------------------------------------------------- *)
< 
< set_jrh_lexer;;
< 
< (* ------------------------------------------------------------------------- *)
< (* Load in the bignum library and set up printing in the toplevel.           *)
< (* ------------------------------------------------------------------------- *)
< 
< #load "nums.cma";;
< 
< include Num;;
< 
< let pp_print_num fmt n =
<   Format.pp_open_hbox fmt ();
<   Format.pp_print_string fmt (string_of_num n);
<   Format.pp_close_box fmt ();;
< 
< let print_num = pp_print_num Format.std_formatter;;
---
>   let c = String.sub s 0 in
>   if c = ':' then
>     "parse_type \"" ^
>     string_escaped (String.substring s 1 (String.size s - 1)) ^ "\""
>   else if c = ';' then "parse_qproof \"" ^ string_escaped s ^ "\"" else
>   let n = String.size s - 1 in
>   if String.substring s n 1 = ":"
>   then "\"" ^ string_escaped (String.substring s 0 n) ^ "\""
>   else "parse_term \"" ^ string_escaped s ^ "\"";;
57c26
< #install_printer pp_print_num;;
---
> let _ = Cakeml.unquote := quotexpander;;