src/Pure/Isar/toplevel.ML
changeset 51332 8707df0b0255
parent 51324 c17f5de0a915
child 51423 e5f9a6d9ca82
     1.1 --- a/src/Pure/Isar/toplevel.ML	Mon Mar 04 11:36:16 2013 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Mar 04 15:03:46 2013 +0100
     1.3 @@ -96,8 +96,9 @@
     1.4    val transition: bool -> transition -> state -> (state * (exn * string) option) option
     1.5    val command_errors: bool -> transition -> state -> Runtime.error list * state option
     1.6    val command_exception: bool -> transition -> state -> state
     1.7 -  val element_result: transition Thy_Syntax.element -> state ->
     1.8 -    (transition * state) list future * state
     1.9 +  type result
    1.10 +  val join_results: result -> (transition * state) list
    1.11 +  val element_result: transition Thy_Syntax.element -> state -> result * state
    1.12  end;
    1.13  
    1.14  structure Toplevel: TOPLEVEL =
    1.15 @@ -705,19 +706,26 @@
    1.16  
    1.17  (* scheduled proof result *)
    1.18  
    1.19 +datatype result =
    1.20 +  Result of transition * state |
    1.21 +  Result_List of result list |
    1.22 +  Result_Future of result future;
    1.23 +
    1.24 +fun join_results (Result x) = [x]
    1.25 +  | join_results (Result_List xs) = maps join_results xs
    1.26 +  | join_results (Result_Future x) = join_results (Future.join x);
    1.27 +
    1.28  local
    1.29  
    1.30  structure Result = Proof_Data
    1.31  (
    1.32 -  type T = (transition * state) list future;
    1.33 -  val empty: T = Future.value [];
    1.34 +  type T = result;
    1.35 +  val empty: T = Result_List [];
    1.36    fun init _ = empty;
    1.37  );
    1.38  
    1.39 -fun done_proof state =
    1.40 -  if can (Proof.assert_bottom true) state
    1.41 -  then Proof.global_done_proof state
    1.42 -  else Proof.context_of (Proof.local_done_proof state);
    1.43 +val get_result = Result.get o Proof.context_of;
    1.44 +val put_result = Proof.map_context o Result.put;
    1.45  
    1.46  fun proof_future_enabled st =
    1.47    (case try proof_of st of
    1.48 @@ -744,46 +752,52 @@
    1.49            (Goal.fork_name "Toplevel.diag" (priority (Thy_Syntax.atom tr))
    1.50              (fn () => command tr st); st)) ()
    1.51        else command tr st;
    1.52 -  in ((tr, st'), st') end;
    1.53 +  in (Result (tr, st'), st') end;
    1.54  
    1.55  in
    1.56  
    1.57 -fun element_result (Thy_Syntax.Element (tr, NONE)) st =
    1.58 -      let val (result, st') = atom_result tr st
    1.59 -      in (Future.value [result], st') end
    1.60 -  | element_result (Thy_Syntax.Element (head_tr, SOME proof)) st =
    1.61 +fun element_result (Thy_Syntax.Element (tr, NONE)) st = atom_result tr st
    1.62 +  | element_result (Thy_Syntax.Element (head_tr, SOME element_rest)) st =
    1.63        let
    1.64          val (head_result, st') = atom_result head_tr st;
    1.65 -        val (body_elems, end_tr) = proof;
    1.66 -        val body_trs = maps Thy_Syntax.flat_element body_elems;
    1.67 +        val (body_elems, end_tr) = element_rest;
    1.68        in
    1.69          if not (proof_future_enabled st')
    1.70          then
    1.71 -          let val (proof_results, st'') = fold_map atom_result (body_trs @ [end_tr]) st'
    1.72 -          in (Future.value (head_result :: proof_results), st'') end
    1.73 +          let
    1.74 +            val proof_trs = maps Thy_Syntax.flat_element body_elems @ [end_tr];
    1.75 +            val (proof_results, st'') = fold_map atom_result proof_trs st';
    1.76 +          in (Result_List (head_result :: proof_results), st'') end
    1.77          else
    1.78            let
    1.79              val finish = Context.Theory o Proof_Context.theory_of;
    1.80  
    1.81              val future_proof = Proof.future_proof
    1.82 -              (fn prf =>
    1.83 +              (fn state =>
    1.84                  setmp_thread_position head_tr (fn () =>
    1.85                    Goal.fork_name "Toplevel.future_proof"
    1.86 -                    (priority (Thy_Syntax.Element (empty, SOME proof)))
    1.87 +                    (priority (Thy_Syntax.Element (empty, SOME element_rest)))
    1.88                      (fn () =>
    1.89 -                      let val (result, result_state) =
    1.90 -                        (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
    1.91 -                          => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
    1.92 -                        |> fold_map atom_result body_trs ||> command end_tr;
    1.93 -                      in (result, presentation_context_of result_state) end)) ())
    1.94 -              #> (fn (result, state') => state' |> done_proof |> Result.put result);
    1.95 +                      let
    1.96 +                        val State (SOME (Proof (prf, (_, orig_gthy))), prev) = st';
    1.97 +                        val prf' = Proof_Node.apply (K state) prf;
    1.98 +                        val (result, result_state) =
    1.99 +                          State (SOME (Proof (prf', (finish, orig_gthy))), prev)
   1.100 +                          |> fold_map element_result body_elems ||> command end_tr;
   1.101 +                      in (Result_List result, presentation_context_of result_state) end)) ())
   1.102 +              #> (fn (res, state') => state' |> put_result (Result_Future res));
   1.103 +
   1.104 +            val forked_proof =
   1.105 +              proof (future_proof #>
   1.106 +                (fn state => state |> Proof.local_done_proof |> put_result (get_result state))) o
   1.107 +              end_proof (fn _ => future_proof #>
   1.108 +                (fn state => state |> Proof.global_done_proof |> Result.put (get_result state)));
   1.109  
   1.110              val st'' = st'
   1.111 -              |> command (head_tr |> set_print false |> reset_trans |> end_proof (K future_proof));
   1.112 +              |> command (head_tr |> set_print false |> reset_trans |> forked_proof);
   1.113 +            val end_result = Result (end_tr, st'');
   1.114              val result =
   1.115 -              Result.get (presentation_context_of st'')
   1.116 -              |> Future.map (fn body_results => head_result :: body_results @ [(end_tr, st'')]);
   1.117 -
   1.118 +              Result_List [head_result, Result.get (presentation_context_of st''), end_result];
   1.119            in (result, st'') end
   1.120        end;
   1.121