# HG changeset patch
# User wenzelm
# Date 1362314637 -3600
# Node ID fd67b7f219e4a38ac3f3e5b564f4fce5dfd57485
# Parent  75682dfff630e75adfb4aa2a6af7c52eece643c0
clarified Toplevel.element_result wrt. Toplevel.is_ignored;

diff -r 75682dfff630 -r fd67b7f219e4 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sun Mar 03 13:23:06 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML	Sun Mar 03 13:43:57 2013 +0100
@@ -735,15 +735,15 @@
     val proof_trs =
       (case opt_proof of
         NONE => []
-      | SOME (a, b) => (maps Thy_Syntax.flat_element a @ [b]) |> filter_out is_ignored);
+      | SOME (a, b) => maps Thy_Syntax.flat_element a @ [b]);
 
     val (_, st') = atom_result head_tr st;
   in
-    if not (Goal.future_enabled ()) orelse is_ignored head_tr orelse
-      null proof_trs orelse not (can proof_of st') orelse Proof.is_relevant (proof_of st')
+    if not (Goal.future_enabled ()) orelse null proof_trs orelse
+      not (can proof_of st') orelse Proof.is_relevant (proof_of st')
     then
       let val (results, st'') = fold_map atom_result proof_trs st'
-      in (Future.value (if is_ignored head_tr then results else (head_tr, st') :: results), st'') end
+      in (Future.value ((head_tr, st') :: results), st'') end
     else
       let
         val (body_trs, end_tr) = split_last proof_trs;
diff -r 75682dfff630 -r fd67b7f219e4 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Sun Mar 03 13:23:06 2013 +0100
+++ b/src/Pure/Thy/thy_load.ML	Sun Mar 03 13:43:57 2013 +0100
@@ -265,7 +265,7 @@
         let val ((minor, _), outer_syntax) = Outer_Syntax.get_syntax () in
           Thy_Output.present_thy minor Keyword.command_tags
             (Outer_Syntax.is_markup outer_syntax)
-            (maps Future.join results) toks
+            (filter_out (Toplevel.is_ignored o #1) (maps Future.join results)) toks
           |> Buffer.content
           |> Present.theory_output name
         end);