more basic Goal.reset_futures as snapshot of implicit state;
authorwenzelm
Thu Oct 18 19:58:30 2012 +0200 (2012-10-18)
changeset 4993185780e6f8fd2
parent 49930 defce6616890
child 49932 9d3bc26485eb
more basic Goal.reset_futures as snapshot of implicit state;
more robust Session.finish_futures: do not cancel here, to allow later Future.map of persistent futures (notably proof terms);
src/Pure/PIDE/protocol.ML
src/Pure/System/session.ML
src/Pure/goal.ML
     1.1 --- a/src/Pure/PIDE/protocol.ML	Thu Oct 18 19:12:58 2012 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.ML	Thu Oct 18 19:58:30 2012 +0200
     1.3 @@ -59,7 +59,7 @@
     1.4                in pair int (list (pair int (option int))) end
     1.5                |> YXML.string_of_body);
     1.6  
     1.7 -        val _ = Goal.cancel_futures ();
     1.8 +        val _ = List.app Future.cancel_group (Goal.reset_futures ());
     1.9          val _ = Isabelle_Process.reset_tracing_limits ();
    1.10          val _ = Document.start_execution state';
    1.11        in state' end));
     2.1 --- a/src/Pure/System/session.ML	Thu Oct 18 19:12:58 2012 +0200
     2.2 +++ b/src/Pure/System/session.ML	Thu Oct 18 19:58:30 2012 +0200
     2.3 @@ -66,15 +66,18 @@
     2.4  
     2.5  (* finish *)
     2.6  
     2.7 +fun finish_futures () =
     2.8 +  (case map_filter Task_Queue.group_status (Goal.reset_futures ()) of
     2.9 +    [] => ()
    2.10 +  | exns => raise Par_Exn.make exns);
    2.11 +
    2.12  fun finish () =
    2.13   (Future.shutdown ();
    2.14 -  Goal.finish_futures ();
    2.15 +  finish_futures ();
    2.16    Thy_Info.finish ();
    2.17    Present.finish ();
    2.18    Keyword.status ();
    2.19    Outer_Syntax.check_syntax ();
    2.20 -  Goal.cancel_futures ();
    2.21 -  Future.shutdown ();
    2.22    Options.reset_default ();
    2.23    session_finished := true);
    2.24  
     3.1 --- a/src/Pure/goal.ML	Thu Oct 18 19:12:58 2012 +0200
     3.2 +++ b/src/Pure/goal.ML	Thu Oct 18 19:58:30 2012 +0200
     3.3 @@ -27,8 +27,7 @@
     3.4    val fork_name: string -> (unit -> 'a) -> 'a future
     3.5    val fork: (unit -> 'a) -> 'a future
     3.6    val peek_futures: serial -> unit future list
     3.7 -  val finish_futures: unit -> unit
     3.8 -  val cancel_futures: unit -> unit
     3.9 +  val reset_futures: unit -> Future.group list
    3.10    val future_enabled_level: int -> bool
    3.11    val future_enabled: unit -> bool
    3.12    val future_enabled_nested: int -> bool
    3.13 @@ -174,14 +173,9 @@
    3.14  fun peek_futures id =
    3.15    Inttab.lookup_list (#3 (Synchronized.value forked_proofs)) id;
    3.16  
    3.17 -fun finish_futures () =
    3.18 -  (case map_filter Task_Queue.group_status (#2 (Synchronized.value forked_proofs)) of
    3.19 -    [] => ()
    3.20 -  | exns => raise Par_Exn.make exns);
    3.21 -
    3.22 -fun cancel_futures () =
    3.23 -  Synchronized.change forked_proofs (fn (m, groups, tab) =>
    3.24 -    (List.app Future.cancel_group groups; (0, [], Inttab.empty)));
    3.25 +fun reset_futures () =
    3.26 +  Synchronized.change_result forked_proofs (fn (m, groups, tab) =>
    3.27 +    (groups, (0, [], Inttab.empty)));
    3.28  
    3.29  end;
    3.30