src/Pure/Isar/proof.ML
changeset 51662 3391a493f39a
parent 51606 2843cc095a57
child 52456 960202346d0c
     1.1 --- a/src/Pure/Isar/proof.ML	Tue Apr 09 15:59:02 2013 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Tue Apr 09 20:16:52 2013 +0200
     1.3 @@ -1154,16 +1154,20 @@
     1.4  end;
     1.5  
     1.6  
     1.7 -(* terminal proofs *)
     1.8 +(* terminal proofs *)  (* FIXME avoid toplevel imitation -- include in PIDE/document *)
     1.9  
    1.10  local
    1.11  
    1.12  fun future_terminal_proof proof1 proof2 done int state =
    1.13    if Goal.future_enabled_level 3 andalso not (is_relevant state) then
    1.14      state |> future_proof (fn state' =>
    1.15 -      Goal.fork_params
    1.16 -        {name = "Proof.future_terminal_proof", pos = Position.thread_data (), pri = ~1}
    1.17 -        (fn () => ((), Timing.status proof2 state'))) |> snd |> done
    1.18 +      let
    1.19 +        val pos = Position.thread_data ();
    1.20 +        val props = Markup.command_timing :: (Markup.nameN, "by") :: Position.properties_of pos;
    1.21 +      in
    1.22 +        Goal.fork_params {name = "Proof.future_terminal_proof", pos = pos, pri = ~1}
    1.23 +          (fn () => ((), Timing.protocol props proof2 state'))
    1.24 +      end) |> snd |> done
    1.25    else proof1 state;
    1.26  
    1.27  in