src/Pure/PIDE/document.ML

         (fn () =>
           Toplevel.setmp_thread_position tr
             (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 =
   (case
       (case Toplevel.init_of tr of
         SOME name => Exn.capture (fn () => Thy_Header.consistent_name thy_name name) ()
       | NONE => Exn.Result ()) of
     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
             NONE => Toplevel.status tr Markup.failed
           | SOME st' =>