# HG changeset patch
# User wenzelm
# Date 1206380146 -3600
# Node ID 5d368eb42c119479b9db1931d37fee643a548300
# Parent  a01a05cdd3b8f708e165dc9de928238b7b2b6268
removed pointer_eq from polyml_common.ML (structure Address no longer available after 5.1);
moved use_text/file to polyml_old_compiler4.ML;
PolyML.onEntry: no longer evaluate command line;

diff -r a01a05cdd3b8 -r 5d368eb42c11 src/Pure/ML-Systems/polyml_common.ML
--- a/src/Pure/ML-Systems/polyml_common.ML	Mon Mar 24 18:35:43 2008 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML	Mon Mar 24 18:35:46 2008 +0100
@@ -23,12 +23,6 @@
 PolyML.Compiler.maxInlineSize := 80;
 
 
-(* String compatibility *)
-
-(*low-level pointer equality*)
-val pointer_eq = Address.wordEq;
-
-
 (* old Poly/ML emulation *)
 
 local
@@ -91,50 +85,6 @@
 end;
 
 
-(* ML command execution -- 'eval' *)
-
-fun use_text (tune: string -> string) name (print, err) verbose txt =
-  let
-    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));
-
-    fun get () =
-      (case ! in_buffer of
-        [] => ""
-      | c :: cs => (in_buffer := cs; c));
-    fun put s = out_buffer := s :: ! out_buffer;
-
-    fun exec () =
-      (case ! in_buffer of
-        [] => ()
-      | _ => (PolyML.compiler (get, put) (); exec ()));
-  in
-    exec () handle exn =>
-      (err ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
-    if verbose then print (output ()) else ()
-  end;
-
-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*)
-local
-  fun println s =
-    (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut);
-  fun eval "-q" = ()
-    | 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 ()));
-    app eval (CommandLine.arguments ())));
-end;
-
-
 
 (** interrupts **)
 
@@ -146,6 +96,7 @@
 val default_handler = Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ());
 
 val _ = Signal.signal (sig_int, default_handler);
+val _ = PolyML.onEntry (fn () => (Signal.signal (sig_int, default_handler); ()));
 
 fun change_signal new_handler f x =
   let