Execution.fork formally requires registered Execution.running;
authorwenzelm
Tue Sep 03 11:29:01 2013 +0200 (2013-09-03 ago)
changeset 5337578693e46a237
parent 53374 a14d2a854c02
child 53376 1d4a46f1fced
Execution.fork formally requires registered Execution.running;
Thy_Info.load_thy: more official exec_id registration (batch mode);
dummy exec Document_ID.none is always registered (TTY mode);
clarified exceptions for module Execution (NB: fork is used in user space, unlike protocol operations of Command and Document);
src/Pure/PIDE/command.ML
src/Pure/PIDE/execution.ML
src/Pure/Thy/thy_info.ML
     1.1 --- a/src/Pure/PIDE/command.ML	Tue Sep 03 01:12:40 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Tue Sep 03 11:29:01 2013 +0200
     1.3 @@ -57,7 +57,7 @@
     1.4        (case expr of
     1.5          Expr (exec_id, body) =>
     1.6            uninterruptible (fn restore_attributes => fn () =>
     1.7 -            if Execution.running execution_id exec_id then
     1.8 +            if Execution.running execution_id exec_id [Future.the_worker_group ()] then
     1.9                let
    1.10                  val res =
    1.11                    (body
     2.1 --- a/src/Pure/PIDE/execution.ML	Tue Sep 03 01:12:40 2013 +0200
     2.2 +++ b/src/Pure/PIDE/execution.ML	Tue Sep 03 11:29:01 2013 +0200
     2.3 @@ -11,7 +11,7 @@
     2.4    val discontinue: unit -> unit
     2.5    val is_running: Document_ID.execution -> bool
     2.6    val is_running_exec: Document_ID.exec -> bool
     2.7 -  val running: Document_ID.execution -> Document_ID.exec -> bool
     2.8 +  val running: Document_ID.execution -> Document_ID.exec -> Future.group list -> bool
     2.9    val peek: Document_ID.exec -> Future.group list
    2.10    val cancel: Document_ID.exec -> unit
    2.11    val terminate: Document_ID.exec -> unit
    2.12 @@ -33,7 +33,7 @@
    2.13  fun make_state (execution, execs) = State {execution = execution, execs = execs};
    2.14  fun map_state f (State {execution, execs}) = make_state (f (execution, execs));
    2.15  
    2.16 -val init_state = make_state (Document_ID.none, Inttab.empty);
    2.17 +val init_state = make_state (Document_ID.none, Inttab.make [(Document_ID.none, [])]);
    2.18  val state = Synchronized.var "Execution.state" init_state;
    2.19  
    2.20  fun get_state () = let val State args = Synchronized.value state in args end;
    2.21 @@ -58,18 +58,18 @@
    2.22  fun is_running_exec exec_id =
    2.23    Inttab.defined (#execs (get_state ())) exec_id;
    2.24  
    2.25 -fun running execution_id exec_id =
    2.26 -  Synchronized.guarded_access state
    2.27 +fun running execution_id exec_id groups =
    2.28 +  Synchronized.change_result state
    2.29      (fn State {execution = execution_id', execs} =>
    2.30        let
    2.31          val continue = execution_id = execution_id';
    2.32          val execs' =
    2.33            if continue then
    2.34 -            Inttab.update_new (exec_id, [Future.the_worker_group ()]) execs
    2.35 +            Inttab.update_new (exec_id, groups) execs
    2.36                handle Inttab.DUP dup =>
    2.37 -                error ("Execution already registered: " ^ Document_ID.print dup)
    2.38 +                raise Fail ("Execution already registered: " ^ Document_ID.print dup)
    2.39            else execs;
    2.40 -      in SOME (continue, make_state (execution_id', execs')) end);
    2.41 +      in (continue, make_state (execution_id', execs')) end);
    2.42  
    2.43  fun peek exec_id =
    2.44    Inttab.lookup_list (#execs (get_state ())) exec_id;
    2.45 @@ -89,7 +89,10 @@
    2.46      let
    2.47        val exec_id = the_default 0 (Position.parse_id pos);
    2.48        val group = Future.worker_subgroup ();
    2.49 -      val _ = change_state (apsnd (Inttab.cons_list (exec_id, group)));
    2.50 +      val _ = change_state (apsnd (fn execs =>
    2.51 +        if Inttab.defined execs exec_id
    2.52 +        then Inttab.cons_list (exec_id, group) execs
    2.53 +        else raise Fail ("Cannot fork from unregistered execution: " ^ Document_ID.print exec_id)));
    2.54  
    2.55        val future =
    2.56          (singleton o Future.forks)
    2.57 @@ -127,7 +130,7 @@
    2.58            if Inttab.defined execs' exec_id then ()
    2.59            else groups |> List.app (fn group =>
    2.60              if Task_Queue.is_canceled group then ()
    2.61 -            else error ("Attempt to purge valid execution: " ^ Document_ID.print exec_id)));
    2.62 +            else raise Fail ("Attempt to purge valid execution: " ^ Document_ID.print exec_id)));
    2.63      in execs' end);
    2.64  
    2.65  fun reset () =
     3.1 --- a/src/Pure/Thy/thy_info.ML	Tue Sep 03 01:12:40 2013 +0200
     3.2 +++ b/src/Pure/Thy/thy_info.ML	Tue Sep 03 11:29:01 2013 +0200
     3.3 @@ -165,18 +165,20 @@
     3.4  (* scheduling loader tasks *)
     3.5  
     3.6  datatype result =
     3.7 -  Result of {theory: theory, id: serial, present: unit -> unit, commit: unit -> unit, weight: int};
     3.8 +  Result of {theory: theory, exec_id: Document_ID.exec,
     3.9 +    present: unit -> unit, commit: unit -> unit, weight: int};
    3.10  
    3.11 -fun theory_result theory = Result {theory = theory, id = 0, present = I, commit = I, weight = 0};
    3.12 +fun theory_result theory =
    3.13 +  Result {theory = theory, exec_id = Document_ID.none, present = I, commit = I, weight = 0};
    3.14  
    3.15  fun result_theory (Result {theory, ...}) = theory;
    3.16  fun result_present (Result {present, ...}) = present;
    3.17  fun result_commit (Result {commit, ...}) = commit;
    3.18  fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i);
    3.19  
    3.20 -fun join_theory (Result {theory, id, ...}) =
    3.21 +fun join_theory (Result {theory, exec_id, ...}) =
    3.22    Exn.capture Thm.join_theory_proofs theory ::
    3.23 -  map Exn.Exn (maps Task_Queue.group_status (Execution.peek id));
    3.24 +  map Exn.Exn (maps Task_Queue.group_status (Execution.peek exec_id));
    3.25  
    3.26  
    3.27  datatype task =
    3.28 @@ -271,13 +273,19 @@
    3.29  
    3.30      val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
    3.31  
    3.32 -    val id = serial ();
    3.33 -    val text_pos = Position.put_id (Markup.print_int id) (Path.position thy_path);
    3.34 +    val exec_id = Document_ID.make ();
    3.35 +    val _ =
    3.36 +      Execution.running Document_ID.none exec_id [] orelse
    3.37 +        raise Fail ("Failed to register execution: " ^ Document_ID.print exec_id);
    3.38 +
    3.39 +    val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path);
    3.40      val (theory, present, weight) =
    3.41        Thy_Load.load_thy last_timing update_time dir header text_pos text
    3.42          (if name = Context.PureN then [ML_Context.the_global_context ()] else parents);
    3.43      fun commit () = update_thy deps theory;
    3.44 -  in Result {theory = theory, id = id, present = present, commit = commit, weight = weight} end;
    3.45 +  in
    3.46 +    Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight}
    3.47 +  end;
    3.48  
    3.49  fun check_deps dir name =
    3.50    (case lookup_deps name of