src/Pure/Isar/toplevel.ML
changeset 51284 59a03019f3bf
parent 51282 3d3c1ea0a401
child 51285 0859bd338c9b
     1.1 --- a/src/Pure/Isar/toplevel.ML	Tue Feb 26 13:38:34 2013 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Feb 26 19:44:26 2013 +0100
     1.3 @@ -94,8 +94,9 @@
     1.4    val get_timing: transition -> Time.time
     1.5    val put_timing: Time.time -> transition -> transition
     1.6    val transition: bool -> transition -> state -> (state * (exn * string) option) option
     1.7 -  val command: transition -> state -> state
     1.8 -  val atom_result: transition -> state -> (transition * state) * state
     1.9 +  val command_exception: bool -> transition -> state -> state
    1.10 +  val command_errors: bool -> transition -> state ->
    1.11 +    ((serial * string) * string option) list * state option
    1.12    val element_result: transition Thy_Syntax.element -> state ->
    1.13      (transition * state) list future * state
    1.14  end;
    1.15 @@ -685,15 +686,21 @@
    1.16  end;
    1.17  
    1.18  
    1.19 -(* nested commands *)
    1.20 +(* managed commands *)
    1.21  
    1.22 -fun command tr st =
    1.23 -  (case transition (! interact) tr st of
    1.24 +fun command_exception int tr st =
    1.25 +  (case transition int tr st of
    1.26      SOME (st', NONE) => st'
    1.27    | SOME (_, SOME (exn, info)) =>
    1.28        if Exn.is_interrupt exn then reraise exn else raise Runtime.EXCURSION_FAIL (exn, info)
    1.29    | NONE => raise Runtime.EXCURSION_FAIL (Runtime.TERMINATE, at_command tr));
    1.30  
    1.31 +fun command_errors int tr st =
    1.32 +  (case transition int tr st of
    1.33 +    SOME (st', NONE) => ([], SOME st')
    1.34 +  | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages_ids exn, NONE)
    1.35 +  | NONE => (ML_Compiler.exn_messages_ids Runtime.TERMINATE, NONE));
    1.36 +
    1.37  
    1.38  (* scheduled proof result *)
    1.39  
    1.40 @@ -710,12 +717,19 @@
    1.41      else Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1)
    1.42    end;
    1.43  
    1.44 -fun atom_result tr st =
    1.45 -  let val st' = command tr st
    1.46 -  in ((tr, st'), st') end;
    1.47 -
    1.48  fun element_result (Thy_Syntax.Element (head_tr, opt_proof)) st =
    1.49    let
    1.50 +    val command = command_exception (! interact);
    1.51 +
    1.52 +    fun atom_result tr st =
    1.53 +      let
    1.54 +        val st' =
    1.55 +          if Goal.future_enabled () andalso Keyword.is_diag (name_of tr) then
    1.56 +            setmp_thread_position tr (fn () =>
    1.57 +              (Goal.fork_name "Toplevel.diag" (priority [tr]) (fn () => command tr st); st)) ()
    1.58 +          else command tr st;
    1.59 +      in ((tr, st'), st') end;
    1.60 +
    1.61      val proof_trs =
    1.62        (case opt_proof of
    1.63          NONE => []
    1.64 @@ -735,13 +749,14 @@
    1.65  
    1.66          val future_proof = Proof.global_future_proof
    1.67            (fn prf =>
    1.68 -            Goal.fork_name "Toplevel.future_proof" (priority proof_trs)
    1.69 -              (fn () =>
    1.70 -                let val (result, result_state) =
    1.71 -                  (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
    1.72 -                    => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
    1.73 -                  |> fold_map atom_result body_trs ||> command end_tr;
    1.74 -                in (result, presentation_context_of result_state) end))
    1.75 +            setmp_thread_position head_tr (fn () =>
    1.76 +              Goal.fork_name "Toplevel.future_proof" (priority proof_trs)
    1.77 +                (fn () =>
    1.78 +                  let val (result, result_state) =
    1.79 +                    (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
    1.80 +                      => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
    1.81 +                    |> fold_map atom_result body_trs ||> command end_tr;
    1.82 +                  in (result, presentation_context_of result_state) end)) ())
    1.83            #-> Result.put;
    1.84  
    1.85          val st'' = st'