removed pointer_eq from polyml_common.ML (structure Address no longer available after 5.1);
authorwenzelm
Mon Mar 24 18:35:46 2008 +0100 (2008-03-24 ago)
changeset 263805d368eb42c11
parent 26379 a01a05cdd3b8
child 26381 509a1ca9d35c
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;
src/Pure/ML-Systems/polyml_common.ML
     1.1 --- a/src/Pure/ML-Systems/polyml_common.ML	Mon Mar 24 18:35:43 2008 +0100
     1.2 +++ b/src/Pure/ML-Systems/polyml_common.ML	Mon Mar 24 18:35:46 2008 +0100
     1.3 @@ -23,12 +23,6 @@
     1.4  PolyML.Compiler.maxInlineSize := 80;
     1.5  
     1.6  
     1.7 -(* String compatibility *)
     1.8 -
     1.9 -(*low-level pointer equality*)
    1.10 -val pointer_eq = Address.wordEq;
    1.11 -
    1.12 -
    1.13  (* old Poly/ML emulation *)
    1.14  
    1.15  local
    1.16 @@ -91,50 +85,6 @@
    1.17  end;
    1.18  
    1.19  
    1.20 -(* ML command execution -- 'eval' *)
    1.21 -
    1.22 -fun use_text (tune: string -> string) name (print, err) verbose txt =
    1.23 -  let
    1.24 -    val in_buffer = ref (explode (tune txt));
    1.25 -    val out_buffer = ref ([]: string list);
    1.26 -    fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
    1.27 -
    1.28 -    fun get () =
    1.29 -      (case ! in_buffer of
    1.30 -        [] => ""
    1.31 -      | c :: cs => (in_buffer := cs; c));
    1.32 -    fun put s = out_buffer := s :: ! out_buffer;
    1.33 -
    1.34 -    fun exec () =
    1.35 -      (case ! in_buffer of
    1.36 -        [] => ()
    1.37 -      | _ => (PolyML.compiler (get, put) (); exec ()));
    1.38 -  in
    1.39 -    exec () handle exn =>
    1.40 -      (err ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
    1.41 -    if verbose then print (output ()) else ()
    1.42 -  end;
    1.43 -
    1.44 -fun use_file tune output verbose name =
    1.45 -  let
    1.46 -    val instream = TextIO.openIn name;
    1.47 -    val txt = TextIO.inputAll instream before TextIO.closeIn instream;
    1.48 -  in use_text tune name output verbose txt end;
    1.49 -
    1.50 -
    1.51 -(*eval command line arguments*)
    1.52 -local
    1.53 -  fun println s =
    1.54 -    (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut);
    1.55 -  fun eval "-q" = ()
    1.56 -    | eval txt = use_text (fn x => x) "" (println, println) false txt;
    1.57 -in
    1.58 -  val _ = PolyML.onEntry (fn () =>
    1.59 -   (Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ()));
    1.60 -    app eval (CommandLine.arguments ())));
    1.61 -end;
    1.62 -
    1.63 -
    1.64  
    1.65  (** interrupts **)
    1.66  
    1.67 @@ -146,6 +96,7 @@
    1.68  val default_handler = Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ());
    1.69  
    1.70  val _ = Signal.signal (sig_int, default_handler);
    1.71 +val _ = PolyML.onEntry (fn () => (Signal.signal (sig_int, default_handler); ()));
    1.72  
    1.73  fun change_signal new_handler f x =
    1.74    let