src/Pure/ML/ml_compiler_polyml.ML

               |> Runtime.toplevel_error (err o Runtime.exn_message)) ())));
 
 
     (* compiler invocation *)
 
+    val debug =
+      (case #debug flags of
+        SOME debug => debug
+      | NONE => ML_Options.debugger_enabled opt_context);
+
     val parameters =
      [PolyML.Compiler.CPOutStream write,
       PolyML.Compiler.CPNameSpace space,
       PolyML.Compiler.CPErrorMessageProc message,
       PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos),
       PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos),
       PolyML.Compiler.CPFileName location_props,
       PolyML.Compiler.CPPrintDepth ML_Options.get_print_depth,
       PolyML.Compiler.CPCompilerResultFun result_fun,
       PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
-     ML_Compiler_Parameters.debug (ML_Options.debugger_enabled opt_context);
+     ML_Compiler_Parameters.debug debug;
+
     val _ =
       (while not (List.null (! input_buffer)) do
         PolyML.compiler (get, parameters) ())
       handle exn =>
         if Exn.is_interrupt exn then reraise exn

     if #verbose flags then (output_warnings (); flush_error (); output_writeln ())
     else ()
   end;
 
 end;
-