# HG changeset patch
# User wenzelm
# Date 1231976513 -3600
# Node ID e959ae4a0bca78eb9add33237b806e35bbef024b
# Parent  fe044b49e34fe09076043b6c44d781fc84441a50
added run_command (from isar_document.ML);
tuned;

diff -r fe044b49e34f -r e959ae4a0bca src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Jan 15 00:41:24 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML	Thu Jan 15 00:41:53 2009 +0100
@@ -96,6 +96,7 @@
   val transition: bool -> transition -> state -> (state * (exn * string) option) option
   val commit_exit: Position.T -> transition
   val command: transition -> state -> state
+  val run_command: transition -> state -> state option
   val excursion: (transition * transition list) list -> (transition * state) list lazy
 end;
 
@@ -693,6 +694,16 @@
   | SOME (_, SOME exn_info) => raise EXCURSION_FAIL exn_info
   | NONE => raise EXCURSION_FAIL (TERMINATE, at_command tr));
 
+fun command_result tr st =
+  let val st' = command tr st
+  in (st', st') end;
+
+fun run_command tr st =
+  (case transition true tr st of
+    SOME (st', NONE) => (status tr Markup.finished; SOME st')
+  | SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE)
+  | NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE));
+
 
 (* excursion of units, consisting of commands with proof *)
 
@@ -702,10 +713,6 @@
   fun init _ = NONE;
 );
 
-fun command_result tr st =
-  let val st' = command tr st
-  in (st', st') end;
-
 fun proof_result immediate (tr, proof_trs) st =
   let val st' = command tr st in
     if immediate orelse null proof_trs orelse