use_text/file: tune text (cf. ML_Parse.fix_ints);
authorwenzelm
Sun Sep 16 14:55:48 2007 +0200 (2007-09-16)
changeset 246005877b88f262c
parent 24599 7b0ecf9a9055
child 24601 4a6607412b40
use_text/file: tune text (cf. ML_Parse.fix_ints);
src/Pure/General/secure.ML
src/Pure/ML-Systems/polyml-5.0.ML
src/Pure/ML-Systems/polyml-5.1.ML
     1.1 --- a/src/Pure/General/secure.ML	Sun Sep 16 14:52:34 2007 +0200
     1.2 +++ b/src/Pure/General/secure.ML	Sun Sep 16 14:55:48 2007 +0200
     1.3 @@ -37,8 +37,8 @@
     1.4  
     1.5  fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode";
     1.6  
     1.7 -val orig_use_text = use_text;
     1.8 -val orig_use_file = use_file;
     1.9 +fun orig_use_text x = use_text ML_Parse.fix_ints x;
    1.10 +fun orig_use_file x = use_file ML_Parse.fix_ints x;
    1.11  
    1.12  fun use_text name pr verbose txt = NAMED_CRITICAL "ML" (fn () =>
    1.13    (secure_mltext (); orig_use_text name pr verbose txt));
     2.1 --- a/src/Pure/ML-Systems/polyml-5.0.ML	Sun Sep 16 14:52:34 2007 +0200
     2.2 +++ b/src/Pure/ML-Systems/polyml-5.0.ML	Sun Sep 16 14:55:48 2007 +0200
     2.3 @@ -11,9 +11,9 @@
     2.4  
     2.5  (* improved versions of use_text/file *)
     2.6  
     2.7 -fun use_text name (print, err) verbose txt =
     2.8 +fun use_text (tune: string -> string) name (print, err) verbose txt =
     2.9    let
    2.10 -    val in_buffer = ref (explode txt);
    2.11 +    val in_buffer = ref (explode (tune txt));
    2.12      val out_buffer = ref ([]: string list);
    2.13      fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
    2.14  
     3.1 --- a/src/Pure/ML-Systems/polyml-5.1.ML	Sun Sep 16 14:52:34 2007 +0200
     3.2 +++ b/src/Pure/ML-Systems/polyml-5.1.ML	Sun Sep 16 14:55:48 2007 +0200
     3.3 @@ -12,9 +12,9 @@
     3.4  
     3.5  (* improved versions of use_text/file *)
     3.6  
     3.7 -fun use_text name (print, err) verbose txt =
     3.8 +fun use_text (tune: string -> string) name (print, err) verbose txt =
     3.9    let
    3.10 -    val in_buffer = ref (explode txt);
    3.11 +    val in_buffer = ref (explode (tune txt));
    3.12      val out_buffer = ref ([]: string list);
    3.13      fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
    3.14  
    3.15 @@ -35,8 +35,8 @@
    3.16      if verbose then print (output ()) else ()
    3.17    end;
    3.18  
    3.19 -fun use_file output verbose name =
    3.20 +fun use_file tune output verbose name =
    3.21    let
    3.22      val instream = TextIO.openIn name;
    3.23      val txt = TextIO.inputAll instream before TextIO.closeIn instream;
    3.24 -  in use_text name output verbose txt end;
    3.25 +  in use_text tune name output verbose txt end;