Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: bash.ML Sprache: SML

Original von: Isabelle^©

(*  Title:      Pure/System/bash.ML
    Author:     Makarius

GNU bash processes, with propagation of interrupts -- POSIX version.
*)

signature BASH =
sig
  val string: string -> string
  val strings: string list -> string
  val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
end;

structure Bash: sig val terminate: int option -> unit end =
struct

fun terminate NONE = ()
  | terminate (SOME pid) =
      let
        val kill = Kill.kill_group pid;

        fun multi_kill count s =
          count = 0 orelse
            (kill s; kill Kill.SIGNONE) andalso
            (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
        val _ =
          multi_kill 7 Kill.SIGINT andalso
          multi_kill 3 Kill.SIGTERM andalso
          multi_kill 1 Kill.SIGKILL;
      in () end;

end;

if ML_System.platform_is_windows then ML
\<open>
structure Bash: BASH =
struct

open Bash;

val string = Bash_Syntax.string;
val strings = Bash_Syntax.strings;

val process = Thread_Attributes.uninterruptible (fn restore_attributes => fn script =>
  let
    datatype result = Wait | Signal | Result of int;
    val result = Synchronized.var "bash_result" Wait;

    val id = serial_string ();
    val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
    val out_path = File.tmp_path (Path.basic ("bash_out" ^ id));
    val err_path = File.tmp_path (Path.basic ("bash_err" ^ id));
    val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id));

    fun cleanup_files () =
     (try File.rm script_path;
      try File.rm out_path;
      try File.rm err_path;
      try File.rm pid_path);
    val _ = cleanup_files ();

    val system_thread =
      Isabelle_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
        Thread_Attributes.with_attributes Thread_Attributes.private_interrupts (fn _ =>
          let
            val _ = File.write script_path script;
            val bash_script =
              "bash " ^ File.bash_path script_path ^
                " > " ^ File.bash_path out_path ^
                " 2> " ^ File.bash_path err_path;
            val bash_process = getenv_strict "ISABELLE_BASH_PROCESS";
            val rc =
              Windows.simpleExecute ("",
                quote (ML_System.platform_path bash_process) ^ " " ^
                quote (File.platform_path pid_path) ^  " \"\" bash -c " ^ quote bash_script)
              |> Windows.fromStatus |> SysWord.toInt;
            val res = if rc = 130 orelse rc = 512 then Signal else Result rc;
          in Synchronized.change result (K res) end
          handle exn =>
            (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn)));

    fun read_pid 0 = NONE
      | read_pid count =
          (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of
            NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1))
          | some => some);

    fun cleanup () =
     (Isabelle_Thread.interrupt_unsynchronized system_thread;
      cleanup_files ());
  in
    let
      val _ =
        restore_attributes (fn () =>
          Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) ();

      val out = the_default "" (try File.read out_path);
      val err = the_default "" (try File.read err_path);
      val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
      val pid = read_pid 1;
      val _ = cleanup ();
    in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end
    handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn)
  end);

end;
\<close>
else ML
\<open>
structure Bash: BASH =
struct

open Bash;

val string = Bash_Syntax.string;
val strings = Bash_Syntax.strings;

val process_ml = Thread_Attributes.uninterruptible (fn restore_attributes => fn script =>
  let
    datatype result = Wait | Signal | Result of int;
    val result = Synchronized.var "bash_result" Wait;

    val id = serial_string ();
    val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
    val out_path = File.tmp_path (Path.basic ("bash_out" ^ id));
    val err_path = File.tmp_path (Path.basic ("bash_err" ^ id));
    val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id));

    fun cleanup_files () =
     (try File.rm script_path;
      try File.rm out_path;
      try File.rm err_path;
      try File.rm pid_path);
    val _ = cleanup_files ();

    val system_thread =
      Isabelle_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
        Thread_Attributes.with_attributes Thread_Attributes.private_interrupts (fn _ =>
          let
            val _ = File.write script_path script;
            val _ = getenv_strict "ISABELLE_BASH_PROCESS";
            val status =
              OS.Process.system
                ("exec \"$ISABELLE_BASH_PROCESS\" " ^ File.bash_path pid_path ^ " \"\"" ^
                  " bash " ^ File.bash_path script_path ^
                  " > " ^ File.bash_path out_path ^
                  " 2> " ^ File.bash_path err_path);
            val res =
              (case Posix.Process.fromStatus status of
                Posix.Process.W_EXITED => Result 0
              | Posix.Process.W_EXITSTATUS 0wx82 => Signal
              | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w)
              | Posix.Process.W_SIGNALED s =>
                  if s = Posix.Signal.int then Signal
                  else Result (256 + LargeWord.toInt (Posix.Signal.toWord s))
              | Posix.Process.W_STOPPED s =>
                  Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
          in Synchronized.change result (K res) end
          handle exn =>
            (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn)));

    fun read_pid 0 = NONE
      | read_pid count =
          (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of
            NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1))
          | some => some);

    fun cleanup () =
     (Isabelle_Thread.interrupt_unsynchronized system_thread;
      cleanup_files ());
  in
    let
      val _ =
        restore_attributes (fn () =>
          Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) ();

      val out = the_default "" (try File.read out_path);
      val err = the_default "" (try File.read err_path);
      val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
      val pid = read_pid 1;
      val _ = cleanup ();
    in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end
    handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn)
  end);

fun process_scala script =
  Scala.function_thread "bash_process"
    ("export ISABELLE_TMP=" ^ string (getenv "ISABELLE_TMP") ^ "\n" ^ script)
  |> YXML.parse_body
  |>
    let open XML.Decode in
      variant
       [fn ([], []) => raise Exn.Interrupt,
        fn ([], a) => error (YXML.string_of_body a),
        fn ([a, b], c) =>
          let
            val rc = int_atom a;
            val pid = int_atom b;
            val (out, err) = pair I I c |> apply2 YXML.string_of_body;
          in {out = out, err = err, rc = rc, terminate = fn () => terminate (SOME pid)} end]
    end;

fun process script =
  if ML_System.platform_is_rosetta () then process_scala script else process_ml script;

end;
\<close>

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.