src/Pure/ML-Systems/polyml_common.ML
changeset 39616 8052101883c3
parent 39585 00be8711082f
child 40393 2bb7ec08574a
equal deleted inserted replaced
39615:b926f8ec9cac 39616:8052101883c3
    27 val _ = PolyML.Compiler.forgetValue "getOpt";
    27 val _ = PolyML.Compiler.forgetValue "getOpt";
    28 val _ = PolyML.Compiler.forgetValue "valOf";
    28 val _ = PolyML.Compiler.forgetValue "valOf";
    29 val _ = PolyML.Compiler.forgetValue "foldl";
    29 val _ = PolyML.Compiler.forgetValue "foldl";
    30 val _ = PolyML.Compiler.forgetValue "foldr";
    30 val _ = PolyML.Compiler.forgetValue "foldr";
    31 val _ = PolyML.Compiler.forgetValue "print";
    31 val _ = PolyML.Compiler.forgetValue "print";
    32 val _ = PolyML.Compiler.forgetValue "ref";
       
    33 val _ = PolyML.Compiler.forgetType "ref";
       
    34 
    32 
    35 
    33 
    36 (* Compiler options *)
    34 (* Compiler options *)
    37 
    35 
    38 val ml_system_fix_ints = false;
    36 val ml_system_fix_ints = false;
    60 
    58 
    61 
    59 
    62 (* toplevel printing *)
    60 (* toplevel printing *)
    63 
    61 
    64 local
    62 local
    65   val depth = Unsynchronized.ref 10;
    63   val depth = ref 10;
    66 in
    64 in
    67   fun get_print_depth () = ! depth;
    65   fun get_print_depth () = ! depth;
    68   fun print_depth n = (depth := n; PolyML.print_depth n);
    66   fun print_depth n = (depth := n; PolyML.print_depth n);
    69 end;
    67 end;
    70 
    68