added run_command (from isar_document.ML);
authorwenzelm
Thu, 15 Jan 2009 00:41:53 +0100
changeset 29483 e959ae4a0bca
parent 29482 fe044b49e34f
child 29484 15863d782ae3
added run_command (from isar_document.ML); tuned;
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