src/Pure/ML-Systems/compiler_polyml-5.2.ML
changeset 31480 05937d6aafb5
parent 31312 1c00e4ff3c99
child 32738 15bb09ca0378
equal deleted inserted replaced
31479:08e2a70d002a 31480:05937d6aafb5
    36     val _ =
    36     val _ =
    37       (while not (List.null (! in_buffer)) do
    37       (while not (List.null (! in_buffer)) do
    38         PolyML.compiler (get, parameters) ())
    38         PolyML.compiler (get, parameters) ())
    39       handle exn =>
    39       handle exn =>
    40        (put ("Exception- " ^ General.exnMessage exn ^ " raised");
    40        (put ("Exception- " ^ General.exnMessage exn ^ " raised");
    41         error (output ()); raise exn);
    41         error (output ()); reraise exn);
    42   in if verbose then print (output ()) else () end;
    42   in if verbose then print (output ()) else () end;
    43 
    43 
    44 fun use_file context verbose name =
    44 fun use_file context verbose name =
    45   let
    45   let
    46     val instream = TextIO.openIn name;
    46     val instream = TextIO.openIn name;