src/Pure/PIDE/document.ML
changeset 42328 61879dc97e72
parent 42012 2c3fe3cbebae
child 43642 9ef5479da29f
     1.1 --- a/src/Pure/PIDE/document.ML	Mon Apr 11 17:11:03 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Mon Apr 11 17:23:20 2011 +0200
     1.3 @@ -242,7 +242,9 @@
     1.4          val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof);
     1.5  
     1.6          val start = Timing.start ();
     1.7 -        val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
     1.8 +        val (errs, result) =
     1.9 +          if Toplevel.is_toplevel st andalso not is_init then ([], SOME st)
    1.10 +          else run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
    1.11          val _ = timing tr (Timing.result start);
    1.12          val _ = List.app (Toplevel.error_msg tr) errs;
    1.13          val res =