more permissive run_command: identity execution for empty toplevel, e.g. after malformed theory header;

--- a/src/Pure/PIDE/document.ML	Mon Apr 11 17:11:03 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Mon Apr 11 17:23:20 2011 +0200
@@ -242,7 +242,9 @@
         val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof);
 
         val start = Timing.start ();
-        val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
+        val (errs, result) =
+          if Toplevel.is_toplevel st andalso not is_init then ([], SOME st)
+          else run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
         val _ = timing tr (Timing.result start);
         val _ = List.app (Toplevel.error_msg tr) errs;
         val res =