# HG changeset patch
# User wenzelm
# Date 1289055829 -3600
# Node ID 5bc4336d97682f528b24edc7db9e729503decd7e
# Parent  511e5263f5c6c9169133dd0ebcd1a41d095d3e7f
tuned;

diff -r 511e5263f5c6 -r 5bc4336d9768 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Sat Nov 06 15:34:11 2010 +0100
+++ b/src/Pure/PIDE/document.ML	Sat Nov 06 16:03:49 2010 +0100
@@ -210,6 +210,15 @@
             (fn () => Toplevel.print_state false st) ()))
   else ();
 
+fun run int tr st =
+  (case Toplevel.transition int tr st of
+    SOME (st', NONE) => ([], SOME st')
+  | SOME (_, SOME exn_info) =>
+      (case ML_Compiler.exn_messages (Runtime.EXCURSION_FAIL exn_info) of
+        [] => Exn.interrupt ()
+      | errs => (errs, NONE))
+  | NONE => ([ML_Compiler.exn_message Runtime.TERMINATE], NONE));
+
 in
 
 fun run_command thy_name tr st =
@@ -220,14 +229,7 @@
     Exn.Result () =>
       let
         val int = is_some (Toplevel.init_of tr);
-        val (errs, result) =
-          (case Toplevel.transition int tr st of
-            SOME (st', NONE) => ([], SOME st')
-          | SOME (_, SOME exn_info) =>
-              (case ML_Compiler.exn_messages (Runtime.EXCURSION_FAIL exn_info) of
-                [] => Exn.interrupt ()
-              | errs => (errs, NONE))
-          | NONE => ([ML_Compiler.exn_message Runtime.TERMINATE], NONE));
+        val (errs, result) = run int tr st;
         val _ = List.app (Toplevel.error_msg tr) errs;
         val _ =
           (case result of