Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: timeout.ML Sprache: SML

Original von: Isabelle^©

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

Execution with (relative) timeout.
*)

signature TIMEOUT =
sig
  exception TIMEOUT of Time.time
  val apply: Time.time -> ('a -> 'b) -> 'a -> 'b
  val print: Time.time -> string
end;

structure Timeout: TIMEOUT =
struct

exception TIMEOUT of Time.time;

fun apply timeout f x =
  Thread_Attributes.with_attributes Thread_Attributes.no_interrupts (fn orig_atts =>
    let
      val self = Thread.self ();
      val start = Time.now ();

      val request =
        Event_Timer.request {physical = false} (start + timeout)
          (fn () => Isabelle_Thread.interrupt_unsynchronized self);
      val result =
        Exn.capture (fn () => Thread_Attributes.with_attributes orig_atts (fn _ => f x)) ();

      val stop = Time.now ();
      val was_timeout = not (Event_Timer.cancel request);
      val test = Exn.capture Thread_Attributes.expose_interrupt ();
    in
      if was_timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test)
      then raise TIMEOUT (stop - start)
      else (Exn.release test; Exn.release result)
    end);

fun print t = "Timeout after " ^ Value.print_time t ^ "s";

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.