src/Pure/ML-Systems/system_shell.ML
author wenzelm
Sun, 31 May 2009 14:51:21 +0200
changeset 31312 1c00e4ff3c99
parent 29564 f8b933a62151
permissions -rw-r--r--
more modular setup of runtime compilation;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
26220
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML-Systems/system_shell.ML
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
     3
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
     4
Generic system shell processes (no provisions to propagate interrupts;
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
     5
might still work via the controlling tty).
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
     6
*)
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
     7
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
     8
local
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
     9
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
    10
fun read_file name =
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
    11
  let val is = TextIO.openIn name
26504
6e87c0a60104 before close: Exn.capture/release;
wenzelm
parents: 26220
diff changeset
    12
  in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
26220
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
    13
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
    14
fun write_file name txt =
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
    15
  let val os = TextIO.openOut name
26504
6e87c0a60104 before close: Exn.capture/release;
wenzelm
parents: 26220
diff changeset
    16
  in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
26220
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
    17
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
    18
in
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
    19
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
    20
fun system_out script =
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
    21
  let
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
    22
    val script_name = OS.FileSys.tmpName ();
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
    23
    val _ = write_file script_name script;
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
    24
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
    25
    val output_name = OS.FileSys.tmpName ();
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
    26
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
    27
    val status =
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
    28
      OS.Process.system ("perl -w \"$ISABELLE_HOME/lib/scripts/system.pl\" nogroup " ^
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
    29
        script_name ^ " /dev/null " ^ output_name);
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
    30
    val rc =
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
    31
      (case Posix.Process.fromStatus status of
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
    32
        Posix.Process.W_EXITED => 0
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
    33
      | Posix.Process.W_EXITSTATUS w => Word8.toInt w
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
    34
      | Posix.Process.W_SIGNALED s => 256 + LargeWord.toInt (Posix.Signal.toWord s)
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
    35
      | Posix.Process.W_STOPPED s => 512 + LargeWord.toInt (Posix.Signal.toWord s));
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
    36
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
    37
    val output = read_file output_name handle IO.Io _ => "";
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
    38
    val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
    39
    val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
    40
  in (output, rc) end;
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
    41
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
    42
end;
d34b68c21f9a common setup for system_out/system;
wenzelm
parents:
diff changeset
    43