# HG changeset patch # User wenzelm # Date 1210755945 -7200 # Node ID 67c54c53da283a7e74d4b7b8cce3377bc015d871 # Parent ae6ae88f924038007f29a23044c20134781f6ccf use_text/file: ignore str_of_pos argument; diff -r ae6ae88f9240 -r 67c54c53da28 src/Pure/ML-Systems/alice.ML --- a/src/Pure/ML-Systems/alice.ML Wed May 14 11:05:11 2008 +0200 +++ b/src/Pure/ML-Systems/alice.ML Wed May 14 11:05:45 2008 +0200 @@ -119,8 +119,8 @@ (* ML command execution *) -fun use_text _ _ _ _ txt = (Compiler.eval txt; ()); -fun use_file _ _ _ name = use name; +fun use_text _ _ _ _ _ txt = (Compiler.eval txt; ()); +fun use_file _ _ _ _ name = use name; diff -r ae6ae88f9240 -r 67c54c53da28 src/Pure/ML-Systems/mosml.ML --- a/src/Pure/ML-Systems/mosml.ML Wed May 14 11:05:11 2008 +0200 +++ b/src/Pure/ML-Systems/mosml.ML Wed May 14 11:05:45 2008 +0200 @@ -152,7 +152,7 @@ (* ML command execution *) (*Can one redirect 'use' directly to an instream?*) -fun use_text (tune: string -> string) _ _ _ txt = +fun use_text (tune: string -> string) _ _ _ _ txt = let val tmp_name = FileSys.tmpName (); val tmp_file = TextIO.openOut tmp_name; @@ -163,7 +163,7 @@ FileSys.remove tmp_name end; -fun use_file _ _ _ name = use name; +fun use_file _ _ _ _ name = use name; diff -r ae6ae88f9240 -r 67c54c53da28 src/Pure/ML-Systems/polyml_old_compiler4.ML --- a/src/Pure/ML-Systems/polyml_old_compiler4.ML Wed May 14 11:05:11 2008 +0200 +++ b/src/Pure/ML-Systems/polyml_old_compiler4.ML Wed May 14 11:05:45 2008 +0200 @@ -4,7 +4,7 @@ Runtime compilation -- for old PolyML.compiler (version 4.x). *) -fun use_text (tune: string -> string) (line: int, name) (print, err) verbose txt = +fun use_text (tune: string -> string) _ (line: int, name) (print, err) verbose txt = let val in_buffer = ref (explode (tune txt)); val out_buffer = ref ([]: string list); @@ -26,7 +26,7 @@ if verbose then print (output ()) else () end; -fun use_file tune output verbose name = +fun use_file tune _ output verbose name = let val instream = TextIO.openIn name; val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream); diff -r ae6ae88f9240 -r 67c54c53da28 src/Pure/ML-Systems/polyml_old_compiler5.ML --- a/src/Pure/ML-Systems/polyml_old_compiler5.ML Wed May 14 11:05:11 2008 +0200 +++ b/src/Pure/ML-Systems/polyml_old_compiler5.ML Wed May 14 11:05:45 2008 +0200 @@ -4,7 +4,7 @@ Runtime compilation -- for old PolyML.compilerEx (version 5.0, 5.1). *) -fun use_text (tune: string -> string) (line, name) (print, err) verbose txt = +fun use_text (tune: string -> string) _ (line, name) (print, err) verbose txt = let val in_buffer = ref (explode (tune txt)); val out_buffer = ref ([]: string list); @@ -26,7 +26,7 @@ if verbose then print (output ()) else () end; -fun use_file tune output verbose name = +fun use_file tune _ output verbose name = let val instream = TextIO.openIn name; val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream); diff -r ae6ae88f9240 -r 67c54c53da28 src/Pure/ML-Systems/poplogml.ML --- a/src/Pure/ML-Systems/poplogml.ML Wed May 14 11:05:11 2008 +0200 +++ b/src/Pure/ML-Systems/poplogml.ML Wed May 14 11:05:45 2008 +0200 @@ -374,5 +374,5 @@ end; -fun use_text _ _ _ txt = use_string txt; -fun use_file _ _ name = use name; +fun use_text _ _ _ _ txt = use_string txt; +fun use_file _ _ _ name = use name; diff -r ae6ae88f9240 -r 67c54c53da28 src/Pure/ML-Systems/smlnj.ML --- a/src/Pure/ML-Systems/smlnj.ML Wed May 14 11:05:11 2008 +0200 +++ b/src/Pure/ML-Systems/smlnj.ML Wed May 14 11:05:45 2008 +0200 @@ -111,7 +111,7 @@ (* ML command execution *) -fun use_text (tune: string -> string) (line: int, name) (print, err) verbose txt = +fun use_text (tune: string -> string) _ (line: int, name) (print, err) verbose txt = let val ref out_orig = Control.Print.out; @@ -129,7 +129,7 @@ if verbose then print (output ()) else () end; -fun use_file tune output verbose name = +fun use_file tune _ output verbose name = let val instream = TextIO.openIn name; val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);