1.1 --- a/src/Pure/ML-Systems/polyml_old_compiler4.ML Mon Mar 24 18:44:21 2008 +0100
1.2 +++ b/src/Pure/ML-Systems/polyml_old_compiler4.ML Mon Mar 24 23:34:24 2008 +0100
1.3 @@ -1,10 +1,10 @@
1.4 (* Title: Pure/ML-Systems/polyml_old_compiler4.ML
1.5 ID: $Id$
1.6
1.7 -Runtime compilation -- for old version of PolyML.compiler (version 4.x).
1.8 +Runtime compilation -- for old PolyML.compiler (version 4.x).
1.9 *)
1.10
1.11 -fun use_text (tune: string -> string) name (print, err) verbose txt =
1.12 +fun use_text (tune: string -> string) (line: int, name) (print, err) verbose txt =
1.13 let
1.14 val in_buffer = ref (explode (tune txt));
1.15 val out_buffer = ref ([]: string list);
1.16 @@ -30,5 +30,5 @@
1.17 let
1.18 val instream = TextIO.openIn name;
1.19 val txt = TextIO.inputAll instream before TextIO.closeIn instream;
1.20 - in use_text tune name output verbose txt end;
1.21 + in use_text tune (1, name) output verbose txt end;
1.22