clarified module name;
authorwenzelm
Fri Jul 12 11:07:02 2013 +0200 (2013-07-12 ago)
changeset 52605a2a805549c74
parent 52604 ff2f0818aebc
child 52606 0d68d108d7e0
clarified module name;
src/Pure/PIDE/command.ML
src/Pure/PIDE/document.ML
src/Pure/PIDE/exec.ML
src/Pure/PIDE/execution.ML
src/Pure/PIDE/protocol.ML
src/Pure/ROOT
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/PIDE/command.ML	Thu Jul 11 23:24:40 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Fri Jul 12 11:07:02 2013 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4    type exec = eval * print list
     1.5    val no_exec: exec
     1.6    val exec_ids: exec option -> Document_ID.exec list
     1.7 -  val exec: Exec.context -> exec -> unit
     1.8 +  val exec: Execution.context -> exec -> unit
     1.9  end;
    1.10  
    1.11  structure Command: COMMAND =
    1.12 @@ -51,10 +51,10 @@
    1.13          (fn Result res => SOME (res, Result res)
    1.14            | expr as Expr (exec_id, e) =>
    1.15                uninterruptible (fn restore_attributes => fn () =>
    1.16 -                if Exec.running context exec_id then
    1.17 +                if Execution.running context exec_id then
    1.18                    let
    1.19                      val res = Exn.capture (restore_attributes e) ();
    1.20 -                    val _ = Exec.finished exec_id (not (Exn.is_interrupt_exn res));
    1.21 +                    val _ = Execution.finished exec_id (not (Exn.is_interrupt_exn res));
    1.22                    in SOME (res, Result res) end
    1.23                  else SOME (Exn.interrupt_exn, expr)) ())
    1.24        |> (fn NONE => error "Concurrent execution attempt" | SOME res => res))
    1.25 @@ -113,7 +113,7 @@
    1.26  val eval_result_state = #state o eval_result;
    1.27  
    1.28  fun eval_same (Eval {exec_id, ...}, Eval {exec_id = exec_id', ...}) =
    1.29 -  exec_id = exec_id' andalso Exec.is_stable exec_id;
    1.30 +  exec_id = exec_id' andalso Execution.is_stable exec_id;
    1.31  
    1.32  local
    1.33  
    1.34 @@ -198,7 +198,7 @@
    1.35      List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
    1.36  
    1.37  fun print_persistent (Print {persistent, ...}) = persistent;
    1.38 -fun print_stable (Print {exec_id, ...}) = Exec.is_stable exec_id;
    1.39 +fun print_stable (Print {exec_id, ...}) = Execution.is_stable exec_id;
    1.40  fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id';
    1.41  
    1.42  in
     2.1 --- a/src/Pure/PIDE/document.ML	Thu Jul 11 23:24:40 2013 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Fri Jul 12 11:07:02 2013 +0200
     2.3 @@ -205,10 +205,10 @@
     2.4  
     2.5  (** main state -- document structure and execution process **)
     2.6  
     2.7 -type execution = {version_id: Document_ID.version, context: Exec.context};
     2.8 +type execution = {version_id: Document_ID.version, context: Execution.context};
     2.9  
    2.10 -val no_execution = {version_id = Document_ID.none, context = Exec.no_context};
    2.11 -fun make_execution version_id = {version_id = version_id, context = Exec.fresh_context ()};
    2.12 +val no_execution = {version_id = Document_ID.none, context = Execution.no_context};
    2.13 +fun make_execution version_id = {version_id = version_id, context = Execution.fresh_context ()};
    2.14  
    2.15  abstype state = State of
    2.16   {versions: version Inttab.table,  (*version id -> document content*)
    2.17 @@ -297,16 +297,16 @@
    2.18  (* document execution *)
    2.19  
    2.20  fun discontinue_execution state =
    2.21 -  Exec.drop_context (#context (execution_of state));
    2.22 +  Execution.drop_context (#context (execution_of state));
    2.23  
    2.24  fun cancel_execution state =
    2.25 -  (Exec.drop_context (#context (execution_of state)); Exec.terminate_all ());
    2.26 +  (Execution.drop_context (#context (execution_of state)); Execution.terminate_all ());
    2.27  
    2.28  fun start_execution state =
    2.29    let
    2.30      val {version_id, context} = execution_of state;
    2.31      val _ =
    2.32 -      if Exec.is_running context then
    2.33 +      if Execution.is_running context then
    2.34          nodes_of (the_version state version_id) |> String_Graph.schedule
    2.35            (fn deps => fn (name, node) =>
    2.36              if not (visible_node node) andalso finished_theory node then
    2.37 @@ -319,7 +319,7 @@
    2.38                    iterate_entries (fn (_, opt_exec) => fn () =>
    2.39                      (case opt_exec of
    2.40                        SOME exec =>
    2.41 -                        if Exec.is_running context then SOME (Command.exec context exec)
    2.42 +                        if Execution.is_running context then SOME (Command.exec context exec)
    2.43                          else NONE
    2.44                      | NONE => NONE)) node ()))
    2.45        else [];
    2.46 @@ -452,7 +452,7 @@
    2.47  
    2.48  fun cancel_old_execs node0 (command_id, exec_ids) =
    2.49    subtract (op =) exec_ids (Command.exec_ids (lookup_entry node0 command_id))
    2.50 -  |> map_filter (Exec.peek_running #> Option.map (tap Future.cancel_group));
    2.51 +  |> map_filter (Execution.peek_running #> Option.map (tap Future.cancel_group));
    2.52  
    2.53  in
    2.54  
     3.1 --- a/src/Pure/PIDE/exec.ML	Thu Jul 11 23:24:40 2013 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,100 +0,0 @@
     3.4 -(*  Title:      Pure/PIDE/exec.ML
     3.5 -    Author:     Makarius
     3.6 -
     3.7 -Global management of command execution fragments.
     3.8 -*)
     3.9 -
    3.10 -signature EXEC =
    3.11 -sig
    3.12 -  type context
    3.13 -  val no_context: context
    3.14 -  val drop_context: context -> unit
    3.15 -  val fresh_context: unit -> context
    3.16 -  val is_running: context -> bool
    3.17 -  val running: context -> Document_ID.exec -> bool
    3.18 -  val finished: Document_ID.exec -> bool -> unit
    3.19 -  val is_stable: Document_ID.exec -> bool
    3.20 -  val peek_running: Document_ID.exec -> Future.group option
    3.21 -  val purge_canceled: unit -> unit
    3.22 -  val terminate_all: unit -> unit
    3.23 -end;
    3.24 -
    3.25 -structure Exec: EXEC =
    3.26 -struct
    3.27 -
    3.28 -(* global state *)
    3.29 -
    3.30 -datatype context = Context of Document_ID.generic;
    3.31 -val no_context = Context Document_ID.none;
    3.32 -
    3.33 -type status = Future.group option;  (*SOME group: running, NONE: canceled*)
    3.34 -val state = Synchronized.var "Exec.state" (no_context, Inttab.empty: status Inttab.table);
    3.35 -
    3.36 -
    3.37 -(* unique execution context *)
    3.38 -
    3.39 -fun drop_context context =
    3.40 -  Synchronized.change state
    3.41 -    (apfst (fn context' => if context = context' then no_context else context'));
    3.42 -
    3.43 -fun fresh_context () =
    3.44 -  let
    3.45 -    val context = Context (Document_ID.make ());
    3.46 -    val _ = Synchronized.change state (apfst (K context));
    3.47 -  in context end;
    3.48 -
    3.49 -fun is_running context = context = fst (Synchronized.value state);
    3.50 -
    3.51 -
    3.52 -(* registered execs *)
    3.53 -
    3.54 -fun running context exec_id =
    3.55 -  Synchronized.guarded_access state
    3.56 -    (fn (current_context, execs) =>
    3.57 -      let
    3.58 -        val cont = context = current_context;
    3.59 -        val execs' =
    3.60 -          if cont then
    3.61 -            Inttab.update_new (exec_id, SOME (Future.the_worker_group ())) execs
    3.62 -              handle Inttab.DUP dup => error ("Duplicate execution " ^ Document_ID.print dup)
    3.63 -          else execs;
    3.64 -      in SOME (cont, (current_context, execs')) end);
    3.65 -
    3.66 -fun finished exec_id stable =
    3.67 -  Synchronized.change state
    3.68 -    (apsnd (fn execs =>
    3.69 -      if not (Inttab.defined execs exec_id) then
    3.70 -        error ("Attempt to finish unknown execution: " ^ Document_ID.print exec_id)
    3.71 -      else if stable then Inttab.delete exec_id execs
    3.72 -      else Inttab.update (exec_id, NONE) execs));
    3.73 -
    3.74 -fun is_stable exec_id =
    3.75 -  not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))) andalso
    3.76 -  (case Inttab.lookup (snd (Synchronized.value state)) exec_id of
    3.77 -    NONE => true
    3.78 -  | SOME status => is_some status);
    3.79 -
    3.80 -fun peek_running exec_id =
    3.81 -  (case Inttab.lookup (snd (Synchronized.value state)) exec_id of
    3.82 -    SOME (SOME group) => SOME group
    3.83 -  | _ => NONE);
    3.84 -
    3.85 -fun purge_canceled () =
    3.86 -  Synchronized.guarded_access state
    3.87 -    (fn (context, execs) =>
    3.88 -      let
    3.89 -        val canceled = Inttab.fold (fn (exec_id, NONE) => cons exec_id | _ => I) execs [];
    3.90 -        val execs' = fold Inttab.delete canceled execs;
    3.91 -      in SOME ((), (context, execs')) end);
    3.92 -
    3.93 -fun terminate_all () =
    3.94 -  let
    3.95 -    val groups =
    3.96 -      Inttab.fold (fn (_, SOME group) => cons group | _ => I)
    3.97 -        (snd (Synchronized.value state)) [];
    3.98 -    val _ = List.app Future.cancel_group groups;
    3.99 -    val _ = List.app Future.terminate groups;
   3.100 -  in () end;
   3.101 -
   3.102 -end;
   3.103 -
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/PIDE/execution.ML	Fri Jul 12 11:07:02 2013 +0200
     4.3 @@ -0,0 +1,100 @@
     4.4 +(*  Title:      Pure/PIDE/execution.ML
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +Global management of command execution fragments.
     4.8 +*)
     4.9 +
    4.10 +signature EXECUTION =
    4.11 +sig
    4.12 +  type context
    4.13 +  val no_context: context
    4.14 +  val drop_context: context -> unit
    4.15 +  val fresh_context: unit -> context
    4.16 +  val is_running: context -> bool
    4.17 +  val running: context -> Document_ID.exec -> bool
    4.18 +  val finished: Document_ID.exec -> bool -> unit
    4.19 +  val is_stable: Document_ID.exec -> bool
    4.20 +  val peek_running: Document_ID.exec -> Future.group option
    4.21 +  val purge_canceled: unit -> unit
    4.22 +  val terminate_all: unit -> unit
    4.23 +end;
    4.24 +
    4.25 +structure Execution: EXECUTION =
    4.26 +struct
    4.27 +
    4.28 +(* global state *)
    4.29 +
    4.30 +datatype context = Context of Document_ID.generic;
    4.31 +val no_context = Context Document_ID.none;
    4.32 +
    4.33 +type status = Future.group option;  (*SOME group: running, NONE: canceled*)
    4.34 +val state = Synchronized.var "Execution.state" (no_context, Inttab.empty: status Inttab.table);
    4.35 +
    4.36 +
    4.37 +(* unique execution context *)
    4.38 +
    4.39 +fun drop_context context =
    4.40 +  Synchronized.change state
    4.41 +    (apfst (fn context' => if context = context' then no_context else context'));
    4.42 +
    4.43 +fun fresh_context () =
    4.44 +  let
    4.45 +    val context = Context (Document_ID.make ());
    4.46 +    val _ = Synchronized.change state (apfst (K context));
    4.47 +  in context end;
    4.48 +
    4.49 +fun is_running context = context = fst (Synchronized.value state);
    4.50 +
    4.51 +
    4.52 +(* registered execs *)
    4.53 +
    4.54 +fun running context exec_id =
    4.55 +  Synchronized.guarded_access state
    4.56 +    (fn (current_context, execs) =>
    4.57 +      let
    4.58 +        val cont = context = current_context;
    4.59 +        val execs' =
    4.60 +          if cont then
    4.61 +            Inttab.update_new (exec_id, SOME (Future.the_worker_group ())) execs
    4.62 +              handle Inttab.DUP dup => error ("Duplicate execution " ^ Document_ID.print dup)
    4.63 +          else execs;
    4.64 +      in SOME (cont, (current_context, execs')) end);
    4.65 +
    4.66 +fun finished exec_id stable =
    4.67 +  Synchronized.change state
    4.68 +    (apsnd (fn execs =>
    4.69 +      if not (Inttab.defined execs exec_id) then
    4.70 +        error ("Attempt to finish unknown execution: " ^ Document_ID.print exec_id)
    4.71 +      else if stable then Inttab.delete exec_id execs
    4.72 +      else Inttab.update (exec_id, NONE) execs));
    4.73 +
    4.74 +fun is_stable exec_id =
    4.75 +  not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))) andalso
    4.76 +  (case Inttab.lookup (snd (Synchronized.value state)) exec_id of
    4.77 +    NONE => true
    4.78 +  | SOME status => is_some status);
    4.79 +
    4.80 +fun peek_running exec_id =
    4.81 +  (case Inttab.lookup (snd (Synchronized.value state)) exec_id of
    4.82 +    SOME (SOME group) => SOME group
    4.83 +  | _ => NONE);
    4.84 +
    4.85 +fun purge_canceled () =
    4.86 +  Synchronized.guarded_access state
    4.87 +    (fn (context, execs) =>
    4.88 +      let
    4.89 +        val canceled = Inttab.fold (fn (exec_id, NONE) => cons exec_id | _ => I) execs [];
    4.90 +        val execs' = fold Inttab.delete canceled execs;
    4.91 +      in SOME ((), (context, execs')) end);
    4.92 +
    4.93 +fun terminate_all () =
    4.94 +  let
    4.95 +    val groups =
    4.96 +      Inttab.fold (fn (_, SOME group) => cons group | _ => I)
    4.97 +        (snd (Synchronized.value state)) [];
    4.98 +    val _ = List.app Future.cancel_group groups;
    4.99 +    val _ = List.app Future.terminate groups;
   4.100 +  in () end;
   4.101 +
   4.102 +end;
   4.103 +
     5.1 --- a/src/Pure/PIDE/protocol.ML	Thu Jul 11 23:24:40 2013 +0200
     5.2 +++ b/src/Pure/PIDE/protocol.ML	Fri Jul 12 11:07:02 2013 +0200
     5.3 @@ -54,7 +54,7 @@
     5.4          val (assign_update, state') = Document.update old_id new_id edits state;
     5.5  
     5.6          val _ = List.app Future.cancel_group (Goal.reset_futures ());
     5.7 -        val _ = Exec.purge_canceled ();
     5.8 +        val _ = Execution.purge_canceled ();
     5.9          val _ = Isabelle_Process.reset_tracing ();
    5.10  
    5.11          val _ =
     6.1 --- a/src/Pure/ROOT	Thu Jul 11 23:24:40 2013 +0200
     6.2 +++ b/src/Pure/ROOT	Fri Jul 12 11:07:02 2013 +0200
     6.3 @@ -150,10 +150,10 @@
     6.4      "ML/ml_syntax.ML"
     6.5      "ML/ml_thms.ML"
     6.6      "PIDE/active.ML"
     6.7 -    "PIDE/exec.ML"
     6.8      "PIDE/command.ML"
     6.9      "PIDE/document.ML"
    6.10      "PIDE/document_id.ML"
    6.11 +    "PIDE/execution.ML"
    6.12      "PIDE/markup.ML"
    6.13      "PIDE/protocol.ML"
    6.14      "PIDE/xml.ML"
     7.1 --- a/src/Pure/ROOT.ML	Thu Jul 11 23:24:40 2013 +0200
     7.2 +++ b/src/Pure/ROOT.ML	Fri Jul 12 11:07:02 2013 +0200
     7.3 @@ -267,7 +267,7 @@
     7.4  use "Isar/outer_syntax.ML";
     7.5  use "General/graph_display.ML";
     7.6  use "Thy/present.ML";
     7.7 -use "PIDE/exec.ML";
     7.8 +use "PIDE/execution.ML";
     7.9  use "PIDE/command.ML";
    7.10  use "Thy/thy_load.ML";
    7.11  use "Thy/thy_info.ML";