changeset 67173 | e746db6db903 |
parent 67163 | 257bcd20eeec |
child 67194 | 1c0a6a957114 |
--- a/src/Pure/Thy/thy_info.ML Fri Dec 08 23:43:58 2017 +0100 +++ b/src/Pure/Thy/thy_info.ML Sun Dec 10 14:29:14 2017 +0100 @@ -269,7 +269,7 @@ if exists (Toplevel.is_skipped_proof o #2) res then () else let val tex_source = Thy_Output.present_thy thy res toks |> Buffer.content; - in if document then Present.theory_output thy tex_source else () end + in if document then Present.theory_output text_pos thy tex_source else () end end; in (thy, present, size text) end;