src/Pure/ML-Systems/polyml_common.ML
changeset 26380 5d368eb42c11
parent 26220 d34b68c21f9a
child 26474 94735cff132c
equal deleted inserted replaced
26379:a01a05cdd3b8 26380:5d368eb42c11
    19 
    19 
    20 val ml_system_fix_ints = false;
    20 val ml_system_fix_ints = false;
    21 
    21 
    22 PolyML.Compiler.printInAlphabeticalOrder := false;
    22 PolyML.Compiler.printInAlphabeticalOrder := false;
    23 PolyML.Compiler.maxInlineSize := 80;
    23 PolyML.Compiler.maxInlineSize := 80;
    24 
       
    25 
       
    26 (* String compatibility *)
       
    27 
       
    28 (*low-level pointer equality*)
       
    29 val pointer_eq = Address.wordEq;
       
    30 
    24 
    31 
    25 
    32 (* old Poly/ML emulation *)
    26 (* old Poly/ML emulation *)
    33 
    27 
    34 local
    28 local
    89   fun get_print_depth () = ! depth;
    83   fun get_print_depth () = ! depth;
    90   fun print_depth n = (depth := n; PolyML.print_depth n);
    84   fun print_depth n = (depth := n; PolyML.print_depth n);
    91 end;
    85 end;
    92 
    86 
    93 
    87 
    94 (* ML command execution -- 'eval' *)
       
    95 
       
    96 fun use_text (tune: string -> string) name (print, err) verbose txt =
       
    97   let
       
    98     val in_buffer = ref (explode (tune txt));
       
    99     val out_buffer = ref ([]: string list);
       
   100     fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
       
   101 
       
   102     fun get () =
       
   103       (case ! in_buffer of
       
   104         [] => ""
       
   105       | c :: cs => (in_buffer := cs; c));
       
   106     fun put s = out_buffer := s :: ! out_buffer;
       
   107 
       
   108     fun exec () =
       
   109       (case ! in_buffer of
       
   110         [] => ()
       
   111       | _ => (PolyML.compiler (get, put) (); exec ()));
       
   112   in
       
   113     exec () handle exn =>
       
   114       (err ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
       
   115     if verbose then print (output ()) else ()
       
   116   end;
       
   117 
       
   118 fun use_file tune output verbose name =
       
   119   let
       
   120     val instream = TextIO.openIn name;
       
   121     val txt = TextIO.inputAll instream before TextIO.closeIn instream;
       
   122   in use_text tune name output verbose txt end;
       
   123 
       
   124 
       
   125 (*eval command line arguments*)
       
   126 local
       
   127   fun println s =
       
   128     (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut);
       
   129   fun eval "-q" = ()
       
   130     | eval txt = use_text (fn x => x) "" (println, println) false txt;
       
   131 in
       
   132   val _ = PolyML.onEntry (fn () =>
       
   133    (Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ()));
       
   134     app eval (CommandLine.arguments ())));
       
   135 end;
       
   136 
       
   137 
       
   138 
    88 
   139 (** interrupts **)
    89 (** interrupts **)
   140 
    90 
   141 exception Interrupt = SML90.Interrupt;
    91 exception Interrupt = SML90.Interrupt;
   142 
    92 
   144 
    94 
   145 val sig_int = 2;
    95 val sig_int = 2;
   146 val default_handler = Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ());
    96 val default_handler = Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ());
   147 
    97 
   148 val _ = Signal.signal (sig_int, default_handler);
    98 val _ = Signal.signal (sig_int, default_handler);
       
    99 val _ = PolyML.onEntry (fn () => (Signal.signal (sig_int, default_handler); ()));
   149 
   100 
   150 fun change_signal new_handler f x =
   101 fun change_signal new_handler f x =
   151   let
   102   let
   152     (*RACE wrt. other signals!*)
   103     (*RACE wrt. other signals!*)
   153     val old_handler = Signal.signal (sig_int, new_handler);
   104     val old_handler = Signal.signal (sig_int, new_handler);