more liberal handling of skipped proofs;

--- a/src/Pure/Thy/thy_load.ML	Wed Mar 27 17:53:29 2013 +0100
+++ b/src/Pure/Thy/thy_load.ML	Wed Mar 27 17:55:21 2013 +0100
@@ -263,10 +263,13 @@
         val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results);
         val ((minor, _), outer_syntax) = Outer_Syntax.get_syntax ();
       in
-        Thy_Output.present_thy minor Keyword.command_tags
-          (Outer_Syntax.is_markup outer_syntax) res toks
-        |> Buffer.content
-        |> Present.theory_output name
+        if exists (Toplevel.is_skipped_proof o #2) res then
+          warning ("Cannot present theory with skipped proofs: " ^ quote name)
+        else
+          Thy_Output.present_thy minor Keyword.command_tags
+            (Outer_Syntax.is_markup outer_syntax) res toks
+          |> Buffer.content
+          |> Present.theory_output name
       end;
 
   in (thy, present, size text) end;

--- a/src/Pure/Thy/thy_output.ML	Wed Mar 27 17:53:29 2013 +0100
+++ b/src/Pure/Thy/thy_output.ML	Wed Mar 27 17:55:21 2013 +0100
@@ -206,7 +206,8 @@
 
 fun check_text (txt, pos) state =
  (Position.report pos Markup.doc_source;
-  ignore (eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos)));
+  if Toplevel.is_skipped_proof state then ()
+  else ignore (eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos)));