tuned;
authorwenzelm
Sun Mar 03 13:57:03 2013 +0100 (2013-03-03 ago)
changeset 513231b37556a3644
parent 51322 fd67b7f219e4
child 51324 c17f5de0a915
tuned;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sun Mar 03 13:43:57 2013 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sun Mar 03 13:57:03 2013 +0100
     1.3 @@ -94,8 +94,8 @@
     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_errors: bool -> transition -> state -> Runtime.error list * state option
     1.8    val command_exception: bool -> transition -> state -> state
     1.9 -  val command_errors: bool -> transition -> state -> Runtime.error list * state option
    1.10    val element_result: transition Thy_Syntax.element -> state ->
    1.11      (transition * state) list future * state
    1.12  end;
    1.13 @@ -687,6 +687,12 @@
    1.14  
    1.15  (* managed commands *)
    1.16  
    1.17 +fun command_errors int tr st =
    1.18 +  (case transition int tr st of
    1.19 +    SOME (st', NONE) => ([], SOME st')
    1.20 +  | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages_ids exn, NONE)
    1.21 +  | NONE => (ML_Compiler.exn_messages_ids Runtime.TERMINATE, NONE));
    1.22 +
    1.23  fun command_exception int tr st =
    1.24    (case transition int tr st of
    1.25      SOME (st', NONE) => st'
    1.26 @@ -694,15 +700,13 @@
    1.27        if Exn.is_interrupt exn then reraise exn else raise Runtime.EXCURSION_FAIL (exn, info)
    1.28    | NONE => raise Runtime.EXCURSION_FAIL (Runtime.TERMINATE, at_command tr));
    1.29  
    1.30 -fun command_errors int tr st =
    1.31 -  (case transition int tr st of
    1.32 -    SOME (st', NONE) => ([], SOME st')
    1.33 -  | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages_ids exn, NONE)
    1.34 -  | NONE => (ML_Compiler.exn_messages_ids Runtime.TERMINATE, NONE));
    1.35 +fun command tr = command_exception (! interact) tr;
    1.36  
    1.37  
    1.38  (* scheduled proof result *)
    1.39  
    1.40 +local
    1.41 +
    1.42  structure Result = Proof_Data
    1.43  (
    1.44    type T = (transition * state) list future;
    1.45 @@ -718,20 +722,20 @@
    1.46      else Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1)
    1.47    end;
    1.48  
    1.49 +fun atom_result tr st =
    1.50 +  let
    1.51 +    val st' =
    1.52 +      if Goal.future_enabled () andalso Keyword.is_diag (name_of tr) then
    1.53 +        setmp_thread_position tr (fn () =>
    1.54 +          (Goal.fork_name "Toplevel.diag" (priority (Thy_Syntax.atom tr))
    1.55 +            (fn () => command tr st); st)) ()
    1.56 +      else command tr st;
    1.57 +  in ((tr, st'), st') end;
    1.58 +
    1.59 +in
    1.60 +
    1.61  fun element_result (Thy_Syntax.Element (head_tr, opt_proof)) st =
    1.62    let
    1.63 -    val command = command_exception (! interact);
    1.64 -
    1.65 -    fun atom_result tr st =
    1.66 -      let
    1.67 -        val st' =
    1.68 -          if Goal.future_enabled () andalso Keyword.is_diag (name_of tr) then
    1.69 -            setmp_thread_position tr (fn () =>
    1.70 -              (Goal.fork_name "Toplevel.diag" (priority (Thy_Syntax.atom tr))
    1.71 -                (fn () => command tr st); st)) ()
    1.72 -          else command tr st;
    1.73 -      in ((tr, st'), st') end;
    1.74 -
    1.75      val proof_trs =
    1.76        (case opt_proof of
    1.77          NONE => []
    1.78 @@ -772,3 +776,5 @@
    1.79    end;
    1.80  
    1.81  end;
    1.82 +
    1.83 +end;