use_text/file: ignore str_of_pos argument;
authorwenzelm
Wed May 14 11:05:45 2008 +0200 (2008-05-14)
changeset 2688467c54c53da28
parent 26883 ae6ae88f9240
child 26885 cfd5eb167706
use_text/file: ignore str_of_pos argument;
src/Pure/ML-Systems/alice.ML
src/Pure/ML-Systems/mosml.ML
src/Pure/ML-Systems/polyml_old_compiler4.ML
src/Pure/ML-Systems/polyml_old_compiler5.ML
src/Pure/ML-Systems/poplogml.ML
src/Pure/ML-Systems/smlnj.ML
     1.1 --- a/src/Pure/ML-Systems/alice.ML	Wed May 14 11:05:11 2008 +0200
     1.2 +++ b/src/Pure/ML-Systems/alice.ML	Wed May 14 11:05:45 2008 +0200
     1.3 @@ -119,8 +119,8 @@
     1.4  
     1.5  (* ML command execution *)
     1.6  
     1.7 -fun use_text _ _ _ _ txt = (Compiler.eval txt; ());
     1.8 -fun use_file _ _ _ name = use name;
     1.9 +fun use_text _ _ _ _ _ txt = (Compiler.eval txt; ());
    1.10 +fun use_file _ _ _ _ name = use name;
    1.11  
    1.12  
    1.13  
     2.1 --- a/src/Pure/ML-Systems/mosml.ML	Wed May 14 11:05:11 2008 +0200
     2.2 +++ b/src/Pure/ML-Systems/mosml.ML	Wed May 14 11:05:45 2008 +0200
     2.3 @@ -152,7 +152,7 @@
     2.4  (* ML command execution *)
     2.5  
     2.6  (*Can one redirect 'use' directly to an instream?*)
     2.7 -fun use_text (tune: string -> string) _ _ _ txt =
     2.8 +fun use_text (tune: string -> string) _ _ _ _ txt =
     2.9    let
    2.10      val tmp_name = FileSys.tmpName ();
    2.11      val tmp_file = TextIO.openOut tmp_name;
    2.12 @@ -163,7 +163,7 @@
    2.13      FileSys.remove tmp_name
    2.14    end;
    2.15  
    2.16 -fun use_file _ _ _ name = use name;
    2.17 +fun use_file _ _ _ _ name = use name;
    2.18  
    2.19  
    2.20  
     3.1 --- a/src/Pure/ML-Systems/polyml_old_compiler4.ML	Wed May 14 11:05:11 2008 +0200
     3.2 +++ b/src/Pure/ML-Systems/polyml_old_compiler4.ML	Wed May 14 11:05:45 2008 +0200
     3.3 @@ -4,7 +4,7 @@
     3.4  Runtime compilation -- for old PolyML.compiler (version 4.x).
     3.5  *)
     3.6  
     3.7 -fun use_text (tune: string -> string) (line: int, name) (print, err) verbose txt =
     3.8 +fun use_text (tune: string -> string) _ (line: int, name) (print, err) verbose txt =
     3.9    let
    3.10      val in_buffer = ref (explode (tune txt));
    3.11      val out_buffer = ref ([]: string list);
    3.12 @@ -26,7 +26,7 @@
    3.13      if verbose then print (output ()) else ()
    3.14    end;
    3.15  
    3.16 -fun use_file tune output verbose name =
    3.17 +fun use_file tune _ output verbose name =
    3.18    let
    3.19      val instream = TextIO.openIn name;
    3.20      val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
     4.1 --- a/src/Pure/ML-Systems/polyml_old_compiler5.ML	Wed May 14 11:05:11 2008 +0200
     4.2 +++ b/src/Pure/ML-Systems/polyml_old_compiler5.ML	Wed May 14 11:05:45 2008 +0200
     4.3 @@ -4,7 +4,7 @@
     4.4  Runtime compilation -- for old PolyML.compilerEx (version 5.0, 5.1).
     4.5  *)
     4.6  
     4.7 -fun use_text (tune: string -> string) (line, name) (print, err) verbose txt =
     4.8 +fun use_text (tune: string -> string) _ (line, name) (print, err) verbose txt =
     4.9    let
    4.10      val in_buffer = ref (explode (tune txt));
    4.11      val out_buffer = ref ([]: string list);
    4.12 @@ -26,7 +26,7 @@
    4.13      if verbose then print (output ()) else ()
    4.14    end;
    4.15  
    4.16 -fun use_file tune output verbose name =
    4.17 +fun use_file tune _ output verbose name =
    4.18    let
    4.19      val instream = TextIO.openIn name;
    4.20      val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
     5.1 --- a/src/Pure/ML-Systems/poplogml.ML	Wed May 14 11:05:11 2008 +0200
     5.2 +++ b/src/Pure/ML-Systems/poplogml.ML	Wed May 14 11:05:45 2008 +0200
     5.3 @@ -374,5 +374,5 @@
     5.4  
     5.5  end;
     5.6  
     5.7 -fun use_text _ _ _ txt = use_string txt;
     5.8 -fun use_file _ _ name = use name;
     5.9 +fun use_text _ _ _ _ txt = use_string txt;
    5.10 +fun use_file _ _ _ name = use name;
     6.1 --- a/src/Pure/ML-Systems/smlnj.ML	Wed May 14 11:05:11 2008 +0200
     6.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Wed May 14 11:05:45 2008 +0200
     6.3 @@ -111,7 +111,7 @@
     6.4  
     6.5  (* ML command execution *)
     6.6  
     6.7 -fun use_text (tune: string -> string) (line: int, name) (print, err) verbose txt =
     6.8 +fun use_text (tune: string -> string) _ (line: int, name) (print, err) verbose txt =
     6.9    let
    6.10      val ref out_orig = Control.Print.out;
    6.11  
    6.12 @@ -129,7 +129,7 @@
    6.13      if verbose then print (output ()) else ()
    6.14    end;
    6.15  
    6.16 -fun use_file tune output verbose name =
    6.17 +fun use_file tune _ output verbose name =
    6.18    let
    6.19      val instream = TextIO.openIn name;
    6.20      val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);