equal
deleted
inserted
replaced
204 end; |
204 end; |
205 |
205 |
206 |
206 |
207 fun check_text (txt, pos) state = |
207 fun check_text (txt, pos) state = |
208 (Position.report pos Markup.doc_source; |
208 (Position.report pos Markup.doc_source; |
209 ignore (eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos))); |
209 if Toplevel.is_skipped_proof state then () |
|
210 else ignore (eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos))); |
210 |
211 |
211 |
212 |
212 |
213 |
213 (** present theory source **) |
214 (** present theory source **) |
214 |
215 |