<commit_before>(*  Title:      Pure/Concurrent/time_limit.ML
    Author:     Makarius

Execution with time limit (relative timeout).
*)

signature TIME_LIMIT =
sig
  exception TimeOut
  val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b
end;

structure TimeLimit: TIME_LIMIT =
struct

exception TimeOut;

fun timeLimit timeout f x =
  Multithreading.with_attributes Multithreading.no_interrupts (fn orig_atts =>
    let
      val self = Thread.self ();

      val request =
        Event_Timer.request (Time.+ (Time.now (), timeout))
          (fn () => Simple_Thread.interrupt_unsynchronized self);

      val result =
        Exn.capture (fn () => Multithreading.with_attributes orig_atts (fn _ => f x)) ();

      val was_timeout = not (Event_Timer.cancel request);
    in
      if was_timeout andalso Exn.is_interrupt_exn result
      then raise TimeOut
      else Exn.release result
    end);

end;
<commit_msg>back to more paranoid interrupt test after request is cancelled -- avoid race condition;<commit_after>(*  Title:      Pure/Concurrent/time_limit.ML
    Author:     Makarius

Execution with time limit (relative timeout).
*)

signature TIME_LIMIT =
sig
  exception TimeOut
  val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b
end;

structure TimeLimit: TIME_LIMIT =
struct

exception TimeOut;

fun timeLimit timeout f x =
  Multithreading.with_attributes Multithreading.no_interrupts (fn orig_atts =>
    let
      val self = Thread.self ();

      val request =
        Event_Timer.request (Time.+ (Time.now (), timeout))
          (fn () => Simple_Thread.interrupt_unsynchronized self);

      val result =
        Exn.capture (fn () => Multithreading.with_attributes orig_atts (fn _ => f x)) ();

      val was_timeout = not (Event_Timer.cancel request);
      val test = Exn.capture Multithreading.interrupted ();
    in
      if was_timeout andalso (Exn.is_interrupt_exn result orelse Exn.is_interrupt_exn test)
      then raise TimeOut
      else if Exn.is_interrupt_exn test then Exn.interrupt ()
      else Exn.release result
    end);

end;

{'fraction_non_alphanumeric': 0.09777347531461762, 'fraction_numerical': 0.0, 'mean_word_length': 3.013592233009709, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 19, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4718852', 'n_tokens_mistral': 637, 'n_tokens_neox': 622, 'n_words': 185}