1.1 --- a/src/Pure/Isar/toplevel.ML	Thu Jan 15 00:41:24 2009 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Jan 15 00:41:53 2009 +0100
     1.3 @@ -96,6 +96,7 @@
     1.4    val transition: bool -> transition -> state -> (state * (exn * string) option) option
     1.5    val commit_exit: Position.T -> transition
     1.6    val command: transition -> state -> state
     1.7 +  val run_command: transition -> state -> state option
     1.8    val excursion: (transition * transition list) list -> (transition * state) list lazy
     1.9  end;
    1.10  
    1.11 @@ -693,6 +694,16 @@
    1.12    | SOME (_, SOME exn_info) => raise EXCURSION_FAIL exn_info
    1.13    | NONE => raise EXCURSION_FAIL (TERMINATE, at_command tr));
    1.14  
    1.15 +fun command_result tr st =
    1.16 +  let val st' = command tr st
    1.17 +  in (st', st') end;
    1.18 +
    1.19 +fun run_command tr st =
    1.20 +  (case transition true tr st of
    1.21 +    SOME (st', NONE) => (status tr Markup.finished; SOME st')
    1.22 +  | SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE)
    1.23 +  | NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE));
    1.24 +
    1.25  
    1.26  (* excursion of units, consisting of commands with proof *)
    1.27  
    1.28 @@ -702,10 +713,6 @@
    1.29    fun init _ = NONE;
    1.30  );
    1.31  
    1.32 -fun command_result tr st =
    1.33 -  let val st' = command tr st
    1.34 -  in (st', st') end;
    1.35 -
    1.36  fun proof_result immediate (tr, proof_trs) st =
    1.37    let val st' = command tr st in
    1.38      if immediate orelse null proof_trs orelse