src/Pure/ML-Systems/smlnj-0.93.ML
changeset 5090 75ac9b451ae0
parent 5038 301c37df931d
child 5816 6f3cb53502fa
equal deleted inserted replaced
5089:f95e0a6eb775 5090:75ac9b451ae0
    79 fun install_pp (path, pp) = System.PrettyPrint.install_pp path pp;
    79 fun install_pp (path, pp) = System.PrettyPrint.install_pp path pp;
    80 
    80 
    81 
    81 
    82 (* ML command execution *)
    82 (* ML command execution *)
    83 
    83 
    84 val use_text = System.Compile.use_stream o open_string;
    84 fun use_text _ = System.Compile.use_stream o open_string;
    85 
    85 
    86 
    86 
    87 
    87 
    88 (** OS related **)
    88 (** OS related **)
    89 
    89