src/Pure/PIDE/execution.ML
author wenzelm
Wed, 26 Mar 2014 20:08:07 +0100
changeset 56296 5413b6379c0e
parent 56292 1a91a0da65ab
child 56297 3925634718fb
permissions -rw-r--r--
less markup by default -- this is stored persistently in Isabelle/Scala; removed dead code;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
52605
a2a805549c74 clarified module name;
wenzelm
parents: 52604
diff changeset
     1
(*  Title:      Pure/PIDE/execution.ML
52596
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
     3
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
     4
Global management of execution.  Unique running execution serves as
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
     5
barrier for further exploration of forked command execs.
52596
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
     6
*)
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
     7
52605
a2a805549c74 clarified module name;
wenzelm
parents: 52604
diff changeset
     8
signature EXECUTION =
52596
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
     9
sig
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    10
  val start: unit -> Document_ID.execution
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    11
  val discontinue: unit -> unit
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    12
  val is_running: Document_ID.execution -> bool
52784
4ba2e8b9972f de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
wenzelm
parents: 52775
diff changeset
    13
  val is_running_exec: Document_ID.exec -> bool
53375
78693e46a237 Execution.fork formally requires registered Execution.running;
wenzelm
parents: 53193
diff changeset
    14
  val running: Document_ID.execution -> Document_ID.exec -> Future.group list -> bool
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    15
  val peek: Document_ID.exec -> Future.group list
52655
3b2b1ef13979 more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents: 52608
diff changeset
    16
  val cancel: Document_ID.exec -> unit
3b2b1ef13979 more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents: 52608
diff changeset
    17
  val terminate: Document_ID.exec -> unit
56292
1a91a0da65ab more uniform Execution.fork vs. Execution.print;
wenzelm
parents: 56291
diff changeset
    18
  type params = {name: string, pos: Position.T, pri: int}
1a91a0da65ab more uniform Execution.fork vs. Execution.print;
wenzelm
parents: 56291
diff changeset
    19
  val fork: params -> (unit -> 'a) -> 'a future
1a91a0da65ab more uniform Execution.fork vs. Execution.print;
wenzelm
parents: 56291
diff changeset
    20
  val print: params -> (serial -> unit) -> unit
1a91a0da65ab more uniform Execution.fork vs. Execution.print;
wenzelm
parents: 56291
diff changeset
    21
  val fork_prints: Document_ID.exec -> unit
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    22
  val purge: Document_ID.exec list -> unit
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    23
  val reset: unit -> Future.group list
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    24
  val shutdown: unit -> unit
52596
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    25
end;
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    26
52605
a2a805549c74 clarified module name;
wenzelm
parents: 52604
diff changeset
    27
structure Execution: EXECUTION =
52596
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    28
struct
40298d383463 global management of command execution fragments;
wenzelm
parents:
diff changeset
    29
52787
c143ad7811fc pro-forma Execution.reset, despite lack of final join/commit;
wenzelm
parents: 52784
diff changeset
    30
(* global state *)
c143ad7811fc pro-forma Execution.reset, despite lack of final join/commit;
wenzelm
parents: 52784
diff changeset
    31
56292
1a91a0da65ab more uniform Execution.fork vs. Execution.print;
wenzelm
parents: 56291
diff changeset
    32
type print = {name: string, pri: int, body: unit -> unit};
1a91a0da65ab more uniform Execution.fork vs. Execution.print;
wenzelm
parents: 56291
diff changeset
    33
type exec_state = Future.group list * print list;  (*active forks, prints*)
56291
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
    34
type state =
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
    35
  Document_ID.execution * (*overall document execution*)
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
    36
  exec_state Inttab.table;  (*running command execs*)
52787
c143ad7811fc pro-forma Execution.reset, despite lack of final join/commit;
wenzelm
parents: 52784
diff changeset
    37
56291
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
    38
val init_state: state = (Document_ID.none, Inttab.make [(Document_ID.none, ([], []))]);
52787
c143ad7811fc pro-forma Execution.reset, despite lack of final join/commit;
wenzelm
parents: 52784
diff changeset
    39
val state = Synchronized.var "Execution.state" init_state;
52602
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    40
56291
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
    41
fun get_state () = Synchronized.value state;
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
    42
fun change_state_result f = Synchronized.change_result state f;
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
    43
fun change_state f = Synchronized.change state f;
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
    44
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
    45
fun unregistered exec_id = "Unregistered execution: " ^ Document_ID.print exec_id;
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    46
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    47
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    48
(* unique running execution *)
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    49
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    50
fun start () =
52602
00170ef1dc39 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
wenzelm
parents: 52596
diff changeset
    51
  let
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    52
    val execution_id = Document_ID.make ();
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    53
    val _ = change_state (apfst (K execution_id));
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    54
  in execution_id end;
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    55
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    56
fun discontinue () = change_state (apfst (K Document_ID.none));
52606
0d68d108d7e0 tuned signature;
wenzelm
parents: 52605
diff changeset
    57
56291
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
    58
fun is_running execution_id = execution_id = #1 (get_state ());
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    59
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    60
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    61
(* execs *)
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
    62
52784
4ba2e8b9972f de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
wenzelm
parents: 52775
diff changeset
    63
fun is_running_exec exec_id =
56291
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
    64
  Inttab.defined (#2 (get_state ())) exec_id;
52784
4ba2e8b9972f de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
wenzelm
parents: 52775
diff changeset
    65
53375
78693e46a237 Execution.fork formally requires registered Execution.running;
wenzelm
parents: 53193
diff changeset
    66
fun running execution_id exec_id groups =
56291
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
    67
  change_state_result (fn (execution_id', execs) =>
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
    68
    let
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
    69
      val continue = execution_id = execution_id';
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
    70
      val execs' =
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
    71
        if continue then
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
    72
          Inttab.update_new (exec_id, (groups, [])) execs
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
    73
            handle Inttab.DUP dup =>
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
    74
              raise Fail ("Execution already registered: " ^ Document_ID.print dup)
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
    75
        else execs;
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
    76
    in (continue, (execution_id', execs')) end);
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    77
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    78
fun peek exec_id =
56291
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
    79
  (case Inttab.lookup (#2 (get_state ())) exec_id of
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
    80
    SOME (groups, _) => groups
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
    81
  | NONE => []);
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    82
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    83
fun cancel exec_id = List.app Future.cancel_group (peek exec_id);
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    84
fun terminate exec_id = List.app Future.terminate (peek exec_id);
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    85
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    86
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    87
(* fork *)
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    88
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    89
fun status task markups =
56296
5413b6379c0e less markup by default -- this is stored persistently in Isabelle/Scala;
wenzelm
parents: 56292
diff changeset
    90
  let
5413b6379c0e less markup by default -- this is stored persistently in Isabelle/Scala;
wenzelm
parents: 56292
diff changeset
    91
    val props =
5413b6379c0e less markup by default -- this is stored persistently in Isabelle/Scala;
wenzelm
parents: 56292
diff changeset
    92
      if ! Multithreading.trace >= 2
5413b6379c0e less markup by default -- this is stored persistently in Isabelle/Scala;
wenzelm
parents: 56292
diff changeset
    93
      then [(Markup.taskN, Task_Queue.str_of_task task)] else [];
5413b6379c0e less markup by default -- this is stored persistently in Isabelle/Scala;
wenzelm
parents: 56292
diff changeset
    94
  in Output.status (implode (map (Markup.markup_only o Markup.properties props) markups)) end;
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    95
56292
1a91a0da65ab more uniform Execution.fork vs. Execution.print;
wenzelm
parents: 56291
diff changeset
    96
type params = {name: string, pos: Position.T, pri: int};
1a91a0da65ab more uniform Execution.fork vs. Execution.print;
wenzelm
parents: 56291
diff changeset
    97
1a91a0da65ab more uniform Execution.fork vs. Execution.print;
wenzelm
parents: 56291
diff changeset
    98
fun fork ({name, pos, pri}: params) e =
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
    99
  uninterruptible (fn _ => Position.setmp_thread_data pos (fn () =>
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   100
    let
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   101
      val exec_id = the_default 0 (Position.parse_id pos);
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   102
      val group = Future.worker_subgroup ();
53375
78693e46a237 Execution.fork formally requires registered Execution.running;
wenzelm
parents: 53193
diff changeset
   103
      val _ = change_state (apsnd (fn execs =>
56291
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
   104
        (case Inttab.lookup execs exec_id of
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
   105
          SOME (groups, prints) =>
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
   106
            Inttab.update (exec_id, (group :: groups, prints)) execs
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
   107
        | NONE => raise Fail (unregistered exec_id))));
52655
3b2b1ef13979 more careful termination of removed execs, leaving running execs undisturbed;
wenzelm
parents: 52608
diff changeset
   108
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   109
      val future =
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   110
        (singleton o Future.forks)
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   111
          {name = name, group = SOME group, deps = [], pri = pri, interrupts = false}
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   112
          (fn () =>
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   113
            let
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   114
              val task = the (Future.worker_task ());
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   115
              val _ = status task [Markup.running];
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   116
              val result =
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   117
                Exn.capture (Future.interruptible_task e) ()
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   118
                |> Future.identify_result pos;
54646
2b38549374ba more robust status reports: avoid loosing information about physical events (see also 28d207ba9340, 2bc5924b117f, 9edfd36a0355) -- NB: TTY and Proof General ignore Output.status and Output.report;
wenzelm
parents: 53375
diff changeset
   119
              val _ = status task [Markup.joined];
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   120
              val _ =
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   121
                (case result of
54678
87910da843d5 more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
wenzelm
parents: 54646
diff changeset
   122
                  Exn.Exn exn =>
54646
2b38549374ba more robust status reports: avoid loosing information about physical events (see also 28d207ba9340, 2bc5924b117f, 9edfd36a0355) -- NB: TTY and Proof General ignore Output.status and Output.report;
wenzelm
parents: 53375
diff changeset
   123
                   (status task [Markup.failed];
54678
87910da843d5 more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
wenzelm
parents: 54646
diff changeset
   124
                    status task [Markup.finished];
54646
2b38549374ba more robust status reports: avoid loosing information about physical events (see also 28d207ba9340, 2bc5924b117f, 9edfd36a0355) -- NB: TTY and Proof General ignore Output.status and Output.report;
wenzelm
parents: 53375
diff changeset
   125
                    Output.report (Markup.markup_only Markup.bad);
2b38549374ba more robust status reports: avoid loosing information about physical events (see also 28d207ba9340, 2bc5924b117f, 9edfd36a0355) -- NB: TTY and Proof General ignore Output.status and Output.report;
wenzelm
parents: 53375
diff changeset
   126
                    if exec_id = 0 then ()
54678
87910da843d5 more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
wenzelm
parents: 54646
diff changeset
   127
                    else List.app (Future.error_msg pos) (ML_Compiler.exn_messages_ids exn))
87910da843d5 more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
wenzelm
parents: 54646
diff changeset
   128
                | Exn.Res _ =>
87910da843d5 more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
wenzelm
parents: 54646
diff changeset
   129
                    status task [Markup.finished])
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   130
            in Exn.release result end);
54646
2b38549374ba more robust status reports: avoid loosing information about physical events (see also 28d207ba9340, 2bc5924b117f, 9edfd36a0355) -- NB: TTY and Proof General ignore Output.status and Output.report;
wenzelm
parents: 53375
diff changeset
   131
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   132
      val _ = status (Future.task_of future) [Markup.forked];
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   133
    in future end)) ();
52604
ff2f0818aebc more explicit type Exec.context;
wenzelm
parents: 52602
diff changeset
   134
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   135
56291
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
   136
(* print *)
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
   137
56292
1a91a0da65ab more uniform Execution.fork vs. Execution.print;
wenzelm
parents: 56291
diff changeset
   138
fun print ({name, pos, pri}: params) pr =
56291
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
   139
  change_state (apsnd (fn execs =>
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
   140
    let
56292
1a91a0da65ab more uniform Execution.fork vs. Execution.print;
wenzelm
parents: 56291
diff changeset
   141
      val exec_id = the_default 0 (Position.parse_id pos);
56291
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
   142
      val i = serial ();
56292
1a91a0da65ab more uniform Execution.fork vs. Execution.print;
wenzelm
parents: 56291
diff changeset
   143
      val print = {name = name, pri = pri, body = fn () => pr i};
56291
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
   144
    in
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
   145
      (case Inttab.lookup execs exec_id of
56292
1a91a0da65ab more uniform Execution.fork vs. Execution.print;
wenzelm
parents: 56291
diff changeset
   146
        SOME (groups, prints) => Inttab.update (exec_id, (groups, print :: prints)) execs
56291
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
   147
      | NONE => raise Fail (unregistered exec_id))
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
   148
    end));
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
   149
56292
1a91a0da65ab more uniform Execution.fork vs. Execution.print;
wenzelm
parents: 56291
diff changeset
   150
fun fork_prints exec_id =
56291
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
   151
  (case Inttab.lookup (#2 (get_state ())) exec_id of
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
   152
    SOME (_, prints) =>
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
   153
      if null prints orelse null (tl prints) orelse not (Multithreading.enabled ())
56292
1a91a0da65ab more uniform Execution.fork vs. Execution.print;
wenzelm
parents: 56291
diff changeset
   154
      then List.app (fn {body, ...} => body ()) (rev prints)
56291
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
   155
      else
56296
5413b6379c0e less markup by default -- this is stored persistently in Isabelle/Scala;
wenzelm
parents: 56292
diff changeset
   156
        let val pos = Position.thread_data () in
56292
1a91a0da65ab more uniform Execution.fork vs. Execution.print;
wenzelm
parents: 56291
diff changeset
   157
          List.app (fn {name, pri, body} =>
1a91a0da65ab more uniform Execution.fork vs. Execution.print;
wenzelm
parents: 56291
diff changeset
   158
            ignore (fork {name = name, pos = pos, pri = pri} body)) (rev prints)
1a91a0da65ab more uniform Execution.fork vs. Execution.print;
wenzelm
parents: 56291
diff changeset
   159
        end
56291
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
   160
  | NONE => raise Fail (unregistered exec_id));
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
   161
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
   162
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   163
(* cleanup *)
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   164
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   165
fun purge exec_ids =
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   166
  (change_state o apsnd) (fn execs =>
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   167
    let
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   168
      val execs' = fold Inttab.delete_safe exec_ids execs;
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   169
      val () =
56291
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
   170
        (execs', ()) |-> Inttab.fold (fn (exec_id, (groups, _)) => fn () =>
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   171
          if Inttab.defined execs' exec_id then ()
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   172
          else groups |> List.app (fn group =>
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   173
            if Task_Queue.is_canceled group then ()
53375
78693e46a237 Execution.fork formally requires registered Execution.running;
wenzelm
parents: 53193
diff changeset
   174
            else raise Fail ("Attempt to purge valid execution: " ^ Document_ID.print exec_id)));
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   175
    in execs' end);
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   176
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   177
fun reset () =
56291
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
   178
  change_state_result (fn (_, execs) =>
e79f76a48449 added Execution.print: accumulate print operations for some command execution, which are applied later and print time;
wenzelm
parents: 54678
diff changeset
   179
    let val groups = Inttab.fold (append o #1 o #2) execs []
53192
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   180
    in (groups, init_state) end);
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   181
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   182
fun shutdown () =
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   183
  (Future.shutdown ();
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   184
    (case maps Task_Queue.group_status (reset ()) of
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   185
      [] => ()
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   186
    | exns => raise Par_Exn.make exns));
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   187
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   188
end;
04df1d236e1c maintain goal forks as part of global execution;
wenzelm
parents: 52787
diff changeset
   189