src/Pure/ML-Systems/polyml_old_compiler4.ML
changeset 26385 ae7564661e76
parent 26382 16628f5c7e28
child 26504 6e87c0a60104
     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