src/HOL/Tools/async_manager.ML
author bulwahn
Fri, 03 Dec 2010 08:40:47 +0100
changeset 40905 647142607448
parent 40301 bf39a257b3d3
permissions -rw-r--r--
only handle TimeOut exception if used interactively
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
38990
7fba3ccc755a finish moving file
blanchet
parents: 38989
diff changeset
     1
(*  Title:      HOL/Tools/async_manager.ML
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
     2
    Author:     Fabian Immler, TU Muenchen
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
     3
    Author:     Makarius
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
     4
    Author:     Jasmin Blanchette, TU Muenchen
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
     5
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
     6
Central manager for asynchronous diagnosis tool threads.
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
     7
*)
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
     8
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
     9
signature ASYNC_MANAGER =
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    10
sig
39369
8e585c7d418a export function
blanchet
parents: 39006
diff changeset
    11
  val break_into_chunks : string list -> string list
37584
2e289dc13615 factor out thread creation
blanchet
parents: 37583
diff changeset
    12
  val launch :
39006
a02cb5717677 remove time information in output, since it's confusing anyway
blanchet
parents: 38990
diff changeset
    13
    string -> Time.time -> Time.time -> string -> (unit -> string) -> unit
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
    14
  val kill_threads : string -> string -> unit
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
    15
  val running_threads : string -> string -> unit
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
    16
  val thread_messages : string -> string -> int option -> unit
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    17
end;
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    18
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    19
structure Async_Manager : ASYNC_MANAGER =
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    20
struct
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    21
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    22
(** preferences **)
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    23
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    24
val message_store_limit = 20;
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    25
val message_display_limit = 5;
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    26
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    27
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    28
(** thread management **)
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    29
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    30
(* data structures over threads *)
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    31
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    32
structure Thread_Heap = Heap
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    33
(
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    34
  type elem = Time.time * Thread.thread;
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    35
  fun ord ((a, _), (b, _)) = Time.compare (a, b);
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    36
);
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    37
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    38
fun lookup_thread xs = AList.lookup Thread.equal xs;
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    39
fun delete_thread xs = AList.delete Thread.equal xs;
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    40
fun update_thread xs = AList.update Thread.equal xs;
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    41
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    42
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    43
(* state of thread manager *)
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    44
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    45
type state =
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
    46
  {manager: Thread.thread option,
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
    47
   timeout_heap: Thread_Heap.T,
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
    48
   active: (Thread.thread * (string * Time.time * Time.time * string)) list,
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
    49
   canceling: (Thread.thread * (string * Time.time * string)) list,
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
    50
   messages: (string * string) list,
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
    51
   store: (string * string) list}
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    52
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    53
fun make_state manager timeout_heap active canceling messages store : state =
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    54
  {manager = manager, timeout_heap = timeout_heap, active = active,
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    55
   canceling = canceling, messages = messages, store = store}
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    56
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    57
val global_state = Synchronized.var "async_manager"
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    58
  (make_state NONE Thread_Heap.empty [] [] [] []);
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    59
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    60
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    61
(* unregister thread *)
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    62
39006
a02cb5717677 remove time information in output, since it's confusing anyway
blanchet
parents: 38990
diff changeset
    63
fun unregister message thread =
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    64
  Synchronized.change global_state
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    65
  (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    66
    (case lookup_thread active thread of
39376
blanchet
parents: 39369
diff changeset
    67
      SOME (tool, _, _, desc) =>
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    68
        let
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    69
          val active' = delete_thread thread active;
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    70
          val now = Time.now ()
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
    71
          val canceling' = (thread, (tool, now, desc)) :: canceling
39006
a02cb5717677 remove time information in output, since it's confusing anyway
blanchet
parents: 38990
diff changeset
    72
          val message' = desc ^ "\n" ^ message
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
    73
          val messages' = (tool, message') :: messages;
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
    74
          val store' = (tool, message') ::
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    75
            (if length store <= message_store_limit then store
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    76
             else #1 (chop message_store_limit store));
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    77
        in make_state manager timeout_heap active' canceling' messages' store' end
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    78
    | NONE => state));
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    79
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    80
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    81
(* main manager thread -- only one may exist *)
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    82
40301
bf39a257b3d3 simplified some time constants;
wenzelm
parents: 40132
diff changeset
    83
val min_wait_time = seconds 0.3;
bf39a257b3d3 simplified some time constants;
wenzelm
parents: 40132
diff changeset
    84
val max_wait_time = seconds 10.0;
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    85
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    86
fun replace_all bef aft =
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    87
  let
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    88
    fun aux seen "" = String.implode (rev seen)
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    89
      | aux seen s =
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    90
        if String.isPrefix bef s then
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    91
          aux seen "" ^ aft ^ aux [] (unprefix bef s)
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    92
        else
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    93
          aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    94
  in aux [] end
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    95
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    96
(* This is a workaround for Proof General's off-by-a-few sendback display bug,
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    97
   whereby "pr" in "proof" is not highlighted. *)
39369
8e585c7d418a export function
blanchet
parents: 39006
diff changeset
    98
val break_into_chunks = maps (space_explode "\000" o replace_all "\n\n" "\000")
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
    99
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   100
fun print_new_messages () =
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   101
  case Synchronized.change_result global_state
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   102
         (fn {manager, timeout_heap, active, canceling, messages, store} =>
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   103
             (messages, make_state manager timeout_heap active canceling []
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   104
                                   store)) of
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   105
    [] => ()
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   106
  | msgs as (tool, _) :: _ =>
39369
8e585c7d418a export function
blanchet
parents: 39006
diff changeset
   107
    let val ss = break_into_chunks (map snd msgs) in
40132
7ee65dbffa31 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents: 39376
diff changeset
   108
      List.app Output.urgent_message (tool ^ ": " ^ hd ss :: tl ss)
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   109
    end
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   110
39006
a02cb5717677 remove time information in output, since it's confusing anyway
blanchet
parents: 38990
diff changeset
   111
fun check_thread_manager () = Synchronized.change global_state
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   112
  (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   113
    if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   114
    else let val manager = SOME (Toplevel.thread false (fn () =>
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   115
      let
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   116
        fun time_limit timeout_heap =
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   117
          (case try Thread_Heap.min timeout_heap of
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   118
            NONE => Time.+ (Time.now (), max_wait_time)
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   119
          | SOME (time, _) => time);
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   120
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   121
        (*action: find threads whose timeout is reached, and interrupt canceling threads*)
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   122
        fun action {manager, timeout_heap, active, canceling, messages, store} =
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   123
          let val (timeout_threads, timeout_heap') =
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   124
            Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap;
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   125
          in
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   126
            if null timeout_threads andalso null canceling then
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   127
              NONE
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   128
            else
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   129
              let
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   130
                val _ = List.app (Simple_Thread.interrupt o #1) canceling
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   131
                val canceling' = filter (Thread.isActive o #1) canceling
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   132
                val state' = make_state manager timeout_heap' active canceling' messages store;
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   133
              in SOME (map #2 timeout_threads, state') end
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   134
          end;
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   135
      in
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   136
        while Synchronized.change_result global_state
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   137
          (fn state as {timeout_heap, active, canceling, messages, store, ...} =>
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   138
            if null active andalso null canceling andalso null messages
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   139
            then (false, make_state NONE timeout_heap active canceling messages store)
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   140
            else (true, state))
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   141
        do
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   142
          (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   143
            |> these
39006
a02cb5717677 remove time information in output, since it's confusing anyway
blanchet
parents: 38990
diff changeset
   144
            |> List.app (unregister "Timed out.\n");
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   145
            print_new_messages ();
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   146
            (*give threads some time to respond to interrupt*)
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   147
            OS.Process.sleep min_wait_time)
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   148
      end))
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   149
    in make_state manager timeout_heap active canceling messages store end)
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   150
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   151
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   152
(* register thread *)
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   153
39006
a02cb5717677 remove time information in output, since it's confusing anyway
blanchet
parents: 38990
diff changeset
   154
fun register tool birth_time death_time desc thread =
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   155
 (Synchronized.change global_state
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   156
    (fn {manager, timeout_heap, active, canceling, messages, store} =>
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   157
      let
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   158
        val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap;
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   159
        val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active;
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   160
        val state' = make_state manager timeout_heap' active' canceling messages store;
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   161
      in state' end);
39006
a02cb5717677 remove time information in output, since it's confusing anyway
blanchet
parents: 38990
diff changeset
   162
  check_thread_manager ())
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   163
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   164
39006
a02cb5717677 remove time information in output, since it's confusing anyway
blanchet
parents: 38990
diff changeset
   165
fun launch tool birth_time death_time desc f =
37584
2e289dc13615 factor out thread creation
blanchet
parents: 37583
diff changeset
   166
  (Toplevel.thread true
2e289dc13615 factor out thread creation
blanchet
parents: 37583
diff changeset
   167
       (fn () =>
2e289dc13615 factor out thread creation
blanchet
parents: 37583
diff changeset
   168
           let
2e289dc13615 factor out thread creation
blanchet
parents: 37583
diff changeset
   169
             val self = Thread.self ()
39006
a02cb5717677 remove time information in output, since it's confusing anyway
blanchet
parents: 38990
diff changeset
   170
             val _ = register tool birth_time death_time desc self
37584
2e289dc13615 factor out thread creation
blanchet
parents: 37583
diff changeset
   171
             val message = f ()
39006
a02cb5717677 remove time information in output, since it's confusing anyway
blanchet
parents: 38990
diff changeset
   172
           in unregister message self end);
37584
2e289dc13615 factor out thread creation
blanchet
parents: 37583
diff changeset
   173
   ())
2e289dc13615 factor out thread creation
blanchet
parents: 37583
diff changeset
   174
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   175
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   176
(** user commands **)
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   177
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   178
(* kill threads *)
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   179
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   180
fun kill_threads tool workers = Synchronized.change global_state
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   181
  (fn {manager, timeout_heap, active, canceling, messages, store} =>
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   182
    let
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   183
      val killing =
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   184
        map_filter (fn (th, (tool', _, _, desc)) =>
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   185
                       if tool' = tool then SOME (th, (tool', Time.now (), desc))
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   186
                       else NONE) active
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   187
      val state' = make_state manager timeout_heap [] (killing @ canceling) messages store;
40132
7ee65dbffa31 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents: 39376
diff changeset
   188
      val _ = if null killing then () else Output.urgent_message ("Killed active " ^ workers ^ ".")
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   189
    in state' end);
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   190
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   191
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   192
(* running threads *)
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   193
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   194
fun seconds time = string_of_int (Time.toSeconds time) ^ " s"
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   195
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   196
fun running_threads tool workers =
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   197
  let
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   198
    val {active, canceling, ...} = Synchronized.value global_state;
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   199
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   200
    val now = Time.now ();
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   201
    fun running_info (_, (tool', birth_time, death_time, desc)) =
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   202
      if tool' = tool then
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   203
        SOME ("Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   204
              seconds (Time.- (death_time, now)) ^ " to live:\n" ^ desc)
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   205
      else
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   206
        NONE
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   207
    fun canceling_info (_, (tool', death_time, desc)) =
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   208
      if tool' = tool then
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   209
        SOME ("Trying to interrupt thread since " ^
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   210
              seconds (Time.- (now, death_time)) ^ ":\n" ^ desc)
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   211
      else
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   212
        NONE
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   213
    val running =
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   214
      case map_filter running_info active of
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   215
        [] => ["No " ^ workers ^ " running."]
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   216
      | ss => "Running " ^ workers ^ ":" :: ss
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   217
    val interrupting =
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   218
      case map_filter canceling_info canceling of
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   219
        [] => []
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   220
      | ss => "Trying to interrupt the following " ^ workers ^ ":" :: ss
40132
7ee65dbffa31 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents: 39376
diff changeset
   221
  in Output.urgent_message (space_implode "\n\n" (running @ interrupting)) end
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   222
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   223
fun thread_messages tool worker opt_limit =
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   224
  let
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   225
    val limit = the_default message_display_limit opt_limit;
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   226
    val tool_store = Synchronized.value global_state
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   227
                     |> #store |> filter (curry (op =) tool o fst)
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   228
    val header =
37585
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   229
      "Recent " ^ worker ^ " messages" ^
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   230
        (if length tool_store <= limit then ":"
c2ed8112ce57 multiplexing
blanchet
parents: 37584
diff changeset
   231
         else " (" ^ string_of_int limit ^ " displayed):");
39369
8e585c7d418a export function
blanchet
parents: 39006
diff changeset
   232
  in
40132
7ee65dbffa31 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents: 39376
diff changeset
   233
    List.app Output.urgent_message (header :: break_into_chunks
39369
8e585c7d418a export function
blanchet
parents: 39006
diff changeset
   234
                                     (map snd (#1 (chop limit tool_store))))
8e585c7d418a export function
blanchet
parents: 39006
diff changeset
   235
  end
37583
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   236
9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration
blanchet
parents:
diff changeset
   237
end;