Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: makefile.xml Sprache: SML

Original von: Isabelle^©

(*  Title:      Pure/Concurrent/isabelle_thread.ML
    Author:     Makarius

Isabelle-specific thread management.
*)

signature ISABELLE_THREAD =
sig
  val is_self: Thread.thread -> bool
  val get_name: unit -> string
  val stack_limit: unit -> int option
  type params = {name: string, stack_limit: int option, interrupts: bool}
  val attributes: params -> Thread.threadAttribute list
  val fork: params -> (unit -> unit) -> Thread.thread
  val join: Thread.thread -> unit
  val interrupt_unsynchronized: Thread.thread -> unit
end;

structure Isabelle_Thread: ISABELLE_THREAD =
struct

(* self *)

fun is_self thread = Thread.equal (Thread.self (), thread);

(* unique name *)

local
  val name_var = Thread_Data.var () : string Thread_Data.var;
  val count = Counter.make ();
in

fun get_name () =
  (case Thread_Data.get name_var of
    SOME name => name
  | NONE => raise Fail "Isabelle-specific thread required");

fun set_name base =
  Thread_Data.put name_var (SOME ("Isabelle." ^ base ^ "-" ^ string_of_int (count ())));

end;

(* fork *)

fun stack_limit () =
  let
    val threads_stack_limit =
      Real.floor (Options.default_real "threads_stack_limit" * 1024.0 * 1024.0 * 1024.0);
  in if threads_stack_limit <= 0 then NONE else SOME threads_stack_limit end;

type params = {name: string, stack_limit: int option, interrupts: bool};

fun attributes ({stack_limit, interrupts, ...}: params) =
  Thread.MaximumMLStack stack_limit ::
  Thread_Attributes.convert_attributes
    (if interrupts then Thread_Attributes.public_interrupts else Thread_Attributes.no_interrupts);

fun fork (params: params) body =
  Thread.fork (fn () =>
    Exn.trace General.exnMessage tracing (fn () =>
      (set_name (#name params); body ())
        handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn),
    attributes params);

(* join *)

fun join thread =
  while Thread.isActive thread
  do OS.Process.sleep (seconds 0.1);

(* interrupt *)

fun interrupt_unsynchronized thread =
  Thread.interrupt thread handle Thread _ => ();

end;

¤ Dauer der Verarbeitung: 0.1 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.