src/Pure/Thy/thy_info.ML
changeset 67173 e746db6db903
parent 67163 257bcd20eeec
child 67194 1c0a6a957114
equal deleted inserted replaced
67172:97d199699a6b 67173:e746db6db903
   267         val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results);
   267         val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results);
   268       in
   268       in
   269         if exists (Toplevel.is_skipped_proof o #2) res then ()
   269         if exists (Toplevel.is_skipped_proof o #2) res then ()
   270         else
   270         else
   271           let val tex_source = Thy_Output.present_thy thy res toks |> Buffer.content;
   271           let val tex_source = Thy_Output.present_thy thy res toks |> Buffer.content;
   272           in if document then Present.theory_output thy tex_source else () end
   272           in if document then Present.theory_output text_pos thy tex_source else () end
   273       end;
   273       end;
   274 
   274 
   275   in (thy, present, size text) end;
   275   in (thy, present, size text) end;
   276 
   276 
   277 
   277