src/Pure/ML/ml_compiler.ML
changeset 62505 9e2a65912111
parent 62503 19afb533028e
child 62516 5732f1c31566
equal deleted inserted replaced
62504:f14f17e656a6 62505:9e2a65912111
   266 
   266 
   267     val _ =
   267     val _ =
   268       (while not (List.null (! input_buffer)) do
   268       (while not (List.null (! input_buffer)) do
   269         PolyML.compiler (get, parameters) ())
   269         PolyML.compiler (get, parameters) ())
   270       handle exn =>
   270       handle exn =>
   271         if Exn.is_interrupt exn then reraise exn
   271         if Exn.is_interrupt exn then Exn.reraise exn
   272         else
   272         else
   273           let
   273           let
   274             val exn_msg =
   274             val exn_msg =
   275               (case exn of
   275               (case exn of
   276                 STATIC_ERRORS () => ""
   276                 STATIC_ERRORS () => ""