src/Pure/ML-Systems/polyml.ML

--- a/src/Pure/ML-Systems/polyml.ML	Mon Mar 24 18:44:21 2008 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Mon Mar 24 23:34:24 2008 +0100
@@ -22,24 +22,24 @@
 
 (* improved versions of use_text/file *)
 
-fun use_text (tune: string -> string) name (print, err) verbose txt =
+fun use_text (tune: string -> string) (line, name) (print, err) verbose txt =
   let
     val in_buffer = ref (String.explode (tune txt));
     val out_buffer = ref ([]: string list);
     fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
 
-    val line_no = ref 1;
-    fun line () = ! line_no;
+    val current_line = ref line;
     fun get () =
       (case ! in_buffer of
         [] => NONE
-      | c :: cs => (in_buffer := cs; if c = #"\n" then line_no := ! line_no + 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;
 
     val _ =
       (while not (List.null (! in_buffer)) do
         PolyML.compiler
-          {getChar = get, putString = put, lineNumber = line, fileName = name,
+          {getChar = get, putString = put, lineNumber = fn () => ! current_line, fileName = name,
             nameSpace = PolyML.globalNameSpace} ())
       handle exn => (err (output ()); raise exn);
   in
@@ -50,5 +50,5 @@
   let
     val instream = TextIO.openIn name;
     val txt = TextIO.inputAll instream before TextIO.closeIn instream;
-  in use_text tune name output verbose txt end;
+  in use_text tune (1, name) output verbose txt end;