pro-forma Execution.reset, despite lack of final join/commit;
authorwenzelm
Tue Jul 30 12:07:14 2013 +0200 (2013-07-30 ago)
changeset 52787c143ad7811fc
parent 52786 9795ea654905
child 52788 da1fdbfebd39
pro-forma Execution.reset, despite lack of final join/commit;
src/Pure/PIDE/execution.ML
src/Pure/System/isabelle_process.ML
     1.1 --- a/src/Pure/PIDE/execution.ML	Tue Jul 30 11:54:57 2013 +0200
     1.2 +++ b/src/Pure/PIDE/execution.ML	Tue Jul 30 12:07:14 2013 +0200
     1.3 @@ -7,6 +7,7 @@
     1.4  
     1.5  signature EXECUTION =
     1.6  sig
     1.7 +  val reset: unit -> unit
     1.8    val start: unit -> Document_ID.execution
     1.9    val discontinue: unit -> unit
    1.10    val is_running: Document_ID.execution -> bool
    1.11 @@ -19,13 +20,18 @@
    1.12  structure Execution: EXECUTION =
    1.13  struct
    1.14  
    1.15 -val state =
    1.16 -  Synchronized.var "Execution.state"
    1.17 -    (Document_ID.none, Inttab.empty: Future.group Inttab.table);
    1.18 +(* global state *)
    1.19 +
    1.20 +type state = Document_ID.execution * Future.group Inttab.table;
    1.21 +
    1.22 +val init_state: state = (Document_ID.none, Inttab.empty);
    1.23 +val state = Synchronized.var "Execution.state" init_state;
    1.24  
    1.25  
    1.26  (* unique running execution *)
    1.27  
    1.28 +fun reset () = Synchronized.change state (K init_state);
    1.29 +
    1.30  fun start () =
    1.31    let
    1.32      val execution_id = Document_ID.make ();
     2.1 --- a/src/Pure/System/isabelle_process.ML	Tue Jul 30 11:54:57 2013 +0200
     2.2 +++ b/src/Pure/System/isabelle_process.ML	Tue Jul 30 12:07:14 2013 +0200
     2.3 @@ -182,7 +182,7 @@
     2.4        | exn => (Output.error_msg (ML_Compiler.exn_message exn) handle crash => recover crash; true);
     2.5    in
     2.6      if continue then loop channel
     2.7 -    else (Future.shutdown (); Goal.reset_futures (); ())
     2.8 +    else (Future.shutdown (); Goal.reset_futures (); Execution.reset ())
     2.9    end;
    2.10  
    2.11  end;