1.1 --- a/src/Pure/ML-Systems/polyml-experimental.ML	Mon Mar 23 21:40:11 2009 +0100
     1.2 +++ b/src/Pure/ML-Systems/polyml-experimental.ML	Mon Mar 23 21:40:11 2009 +0100
     1.3 @@ -4,6 +4,14 @@
     1.4  *)
     1.5  
     1.6  open Thread;
     1.7 +
     1.8 +structure ML_Name_Space =
     1.9 +struct
    1.10 +  open PolyML.NameSpace;
    1.11 +  type T = PolyML.NameSpace.nameSpace;
    1.12 +  val global = PolyML.globalNameSpace;
    1.13 +end;
    1.14 +
    1.15  use "ML-Systems/polyml_common.ML";
    1.16  use "ML-Systems/multithreading_polyml.ML";
    1.17  
    1.18 @@ -14,12 +22,6 @@
    1.19  
    1.20  (* runtime compilation *)
    1.21  
    1.22 -structure ML_NameSpace =
    1.23 -struct
    1.24 -  open PolyML.NameSpace;
    1.25 -  val global = PolyML.globalNameSpace;
    1.26 -end;
    1.27 -
    1.28  local
    1.29  
    1.30  fun drop_newline s =
    1.31 @@ -28,11 +30,11 @@
    1.32  
    1.33  in
    1.34  
    1.35 -fun use_text (tune: string -> string) str_of_pos
    1.36 -    name_space (start_line, name) (print, err) verbose txt =
    1.37 +fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
    1.38 +    (start_line, name) verbose txt =
    1.39    let
    1.40      val current_line = ref start_line;
    1.41 -    val in_buffer = ref (String.explode (tune txt));
    1.42 +    val in_buffer = ref (String.explode (tune_source txt));
    1.43      val out_buffer = ref ([]: string list);
    1.44      fun output () = drop_newline (implode (rev (! out_buffer)));
    1.45  
    1.46 @@ -42,10 +44,11 @@
    1.47        | c :: cs =>
    1.48            (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
    1.49      fun put s = out_buffer := s :: ! out_buffer;
    1.50 -    fun put_message {message, hard, location = {startLine = line, ...}, context} =
    1.51 +    fun put_message {message = msg1, hard, location = {startLine = line, ...}, context} =
    1.52       (put (if hard then "Error: " else "Warning: ");
    1.53 -      PolyML.prettyPrint (put, 76) message;
    1.54 -      put (str_of_pos line name ^ "\n"));
    1.55 +      PolyML.prettyPrint (put, 76) msg1;
    1.56 +      (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2);
    1.57 +      put ("At" ^ str_of_pos line name ^ "\n"));
    1.58  
    1.59      val parameters =
    1.60       [PolyML.Compiler.CPOutStream put,
    1.61 @@ -58,14 +61,14 @@
    1.62          PolyML.compiler (get, parameters) ())
    1.63        handle exn =>
    1.64         (put ("Exception- " ^ General.exnMessage exn ^ " raised");
    1.65 -        err (output ()); raise exn);
    1.66 +        error (output ()); raise exn);
    1.67    in if verbose then print (output ()) else () end;
    1.68  
    1.69 -fun use_file tune str_of_pos name_space output verbose name =
    1.70 +fun use_file context verbose name =
    1.71    let
    1.72      val instream = TextIO.openIn name;
    1.73      val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
    1.74 -  in use_text tune str_of_pos name_space (1, name) output verbose txt end;
    1.75 +  in use_text context (1, name) verbose txt end;
    1.76  
    1.77  end;
    1.78  
    1.79 @@ -81,7 +84,7 @@
    1.80    | ml_pretty (ML_Pretty.Break (false, wd)) = PrettyBreak (wd, 0)
    1.81    | ml_pretty (ML_Pretty.Break (true, _)) = PrettyBreak (99999, 0);
    1.82  
    1.83 -fun toplevel_pp tune str_of_pos output (_: string list) pp =
    1.84 -  use_text tune str_of_pos ML_NameSpace.global (1, "pp") output false
    1.85 +fun toplevel_pp context (_: string list) pp =
    1.86 +  use_text context (1, "pp") false
    1.87      ("addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
    1.88