# HG changeset patch # User wenzelm # Date 1189947153 -7200 # Node ID 44a1c0c68e219b2156e97b7c5c698f58d309efa9 # Parent cbf2c5cf335ef9ca09521f213808ce5c789eb3cb added ml_system_fix_ints; use_text/file: tune text (cf. ML_Parse.fix_ints); diff -r cbf2c5cf335e -r 44a1c0c68e21 src/Pure/ML-Systems/polyml.ML --- a/src/Pure/ML-Systems/polyml.ML Sun Sep 16 14:52:32 2007 +0200 +++ b/src/Pure/ML-Systems/polyml.ML Sun Sep 16 14:52:33 2007 +0200 @@ -7,6 +7,8 @@ use "ML-Systems/exn.ML"; use "ML-Systems/multithreading_dummy.ML"; +val ml_system_fix_ints = false; + (** ML system and platform related **) @@ -87,9 +89,9 @@ (* ML command execution -- 'eval' *) -fun use_text name (print, err) verbose txt = +fun use_text (tune: string -> string) name (print, err) verbose txt = let - val in_buffer = ref (explode txt); + val in_buffer = ref (explode (tune txt)); val out_buffer = ref ([]: string list); fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs)); @@ -109,7 +111,11 @@ if verbose then print (output ()) else () end; -fun use_file _ _ name = use name; +fun use_file tune output verbose name = + let + val instream = TextIO.openIn name; + val txt = TextIO.inputAll instream before TextIO.closeIn instream; + in use_text tune name output verbose txt end; (*eval command line arguments*) @@ -117,7 +123,7 @@ fun println s = (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut); fun eval "-q" = () - | eval txt = use_text "" (println, println) false txt; + | eval txt = use_text (fn x => x) "" (println, println) false txt; in val _ = PolyML.onEntry (fn () => (Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ()));