# HG changeset patch
# User wenzelm
# Date 1302535400 -7200
# Node ID 61879dc97e72cbc5e1be79d8ea5c63abff0d6c50
# Parent  7c7cc7590eb38a1e27b86eda2037995b27c8d08c
more permissive run_command: identity execution for empty toplevel, e.g. after malformed theory header;

diff -r 7c7cc7590eb3 -r 61879dc97e72 src/Pure/PIDE/document.ML
--- 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 =