src/Pure/ML-Systems/polyml_common.ML
changeset 36162 0bd034a80a9a
parent 35014 a725ff6ead26
child 36876 1abc27d6c362
equal deleted inserted replaced
36161:e30e51b7e4dc 36162:0bd034a80a9a
    53 (* prompts *)
    53 (* prompts *)
    54 
    54 
    55 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
    55 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
    56 
    56 
    57 
    57 
    58 (* print depth *)
    58 (* toplevel printing *)
    59 
    59 
    60 local
    60 local
    61   val depth = Unsynchronized.ref 10;
    61   val depth = Unsynchronized.ref 10;
    62 in
    62 in
    63   fun get_print_depth () = ! depth;
    63   fun get_print_depth () = ! depth;
    64   fun print_depth n = (depth := n; PolyML.print_depth n);
    64   fun print_depth n = (depth := n; PolyML.print_depth n);
    65 end;
    65 end;
    66 
    66 
    67 val error_depth = PolyML.error_depth;
    67 val error_depth = PolyML.error_depth;
       
    68 
       
    69 val ml_make_string = "PolyML.makestring";
    68 
    70 
    69 
    71 
    70 
    72 
    71 (** interrupts **)
    73 (** interrupts **)
    72 
    74