src/Pure/ML-Systems/smlnj.ML
changeset 26385 ae7564661e76
parent 26220 d34b68c21f9a
child 26474 94735cff132c
     1.1 --- a/src/Pure/ML-Systems/smlnj.ML	Mon Mar 24 18:44:21 2008 +0100
     1.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Mon Mar 24 23:34:24 2008 +0100
     1.3 @@ -110,7 +110,7 @@
     1.4  
     1.5  (* ML command execution *)
     1.6  
     1.7 -fun use_text (tune: string -> string) name (print, err) verbose txt =
     1.8 +fun use_text (tune: string -> string) (line: int, name) (print, err) verbose txt =
     1.9    let
    1.10      val ref out_orig = Control.Print.out;
    1.11  
    1.12 @@ -132,7 +132,7 @@
    1.13    let
    1.14      val instream = TextIO.openIn name;
    1.15      val txt = TextIO.inputAll instream before TextIO.closeIn instream;
    1.16 -  in use_text tune name output verbose txt end;
    1.17 +  in use_text tune (1, name) output verbose txt end;
    1.18  
    1.19  
    1.20