--- a/src/Pure/ML-Systems/compiler_polyml.ML Mon Aug 17 15:19:25 2015 +0200
+++ b/src/Pure/ML-Systems/compiler_polyml.ML Mon Aug 17 15:29:30 2015 +0200
@@ -12,31 +12,32 @@
in
fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
- (start_line, name) verbose txt =
+ (line, file) verbose txt =
let
- val line = Unsynchronized.ref start_line;
+ val current_line = Unsynchronized.ref line;
val in_buffer =
- Unsynchronized.ref (String.explode (tune_source (ml_positions start_line name txt)));
+ Unsynchronized.ref (String.explode (tune_source (ml_positions line file txt)));
val out_buffer = Unsynchronized.ref ([]: string list);
fun output () = drop_newline (implode (rev (! out_buffer)));
fun get () =
(case ! in_buffer of
[] => NONE
- | c :: cs => (in_buffer := cs; if c = #"\n" then line := ! line + 1 else (); SOME c));
+ | c :: cs =>
+ (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
fun put s = out_buffer := s :: ! out_buffer;
- fun put_message {message = msg1, hard, location = {startLine = line, ...}, context} =
+ fun put_message {message = msg1, hard, location = {startLine = message_line, ...}, context} =
(put (if hard then "Error: " else "Warning: ");
PolyML.prettyPrint (put, 76) msg1;
(case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2);
- put ("At" ^ str_of_pos line name ^ "\n"));
+ put ("At" ^ str_of_pos message_line file ^ "\n"));
val parameters =
[PolyML.Compiler.CPOutStream put,
PolyML.Compiler.CPNameSpace name_space,
PolyML.Compiler.CPErrorMessageProc put_message,
- PolyML.Compiler.CPLineNo (fn () => ! line),
- PolyML.Compiler.CPFileName name,
+ PolyML.Compiler.CPLineNo (fn () => ! current_line),
+ PolyML.Compiler.CPFileName file,
PolyML.Compiler.CPPrintInAlphabeticalOrder false];
val _ =
(while not (List.null (! in_buffer)) do
@@ -48,11 +49,10 @@
error (output ()); reraise exn);
in if verbose then print (output ()) else () end;
-fun use_file context verbose name =
+fun use_file context verbose file =
let
- val instream = TextIO.openIn name;
+ val instream = TextIO.openIn file;
val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
- in use_text context (1, name) verbose txt end;
+ in use_text context (1, file) verbose txt end;
end;
-
--- a/src/Pure/ML-Systems/smlnj.ML Mon Aug 17 15:19:25 2015 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML Mon Aug 17 15:29:30 2015 +0200
@@ -82,7 +82,7 @@
(* ML command execution *)
-fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt =
+fun use_text ({tune_source, print, error, ...}: use_context) (line, file) verbose txt =
let
val ref out_orig = Control.Print.out;
@@ -93,19 +93,19 @@
in String.substring (str, 0, Int.max (0, size str - 1)) end;
in
Control.Print.out := out;
- Backend.Interact.useStream (TextIO.openString (tune_source (ml_positions line name txt)))
+ Backend.Interact.useStream (TextIO.openString (tune_source (ml_positions line file txt)))
handle exn =>
(Control.Print.out := out_orig;
- error ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
+ error ((if file = "" then "" else "Error in " ^ file ^ "\n") ^ output ()); raise exn);
Control.Print.out := out_orig;
if verbose then print (output ()) else ()
end;
-fun use_file context verbose name =
+fun use_file context verbose file =
let
- val instream = TextIO.openIn name;
+ val instream = TextIO.openIn file;
val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
- in use_text context (1, name) verbose txt end;
+ in use_text context (1, file) verbose txt end;
(* toplevel pretty printing *)