equal
deleted
inserted
replaced
505 |
505 |
506 (* markup commands *) |
506 (* markup commands *) |
507 |
507 |
508 fun check_text (txt, pos) state = |
508 fun check_text (txt, pos) state = |
509 (Position.report Markup.doc_source pos; |
509 (Position.report Markup.doc_source pos; |
510 ignore (ThyOutput.eval_antiquote (#1 (OuterKeyword.get_lexicons ())) state (txt, pos))); |
510 ignore (ThyOutput.eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos))); |
511 |
511 |
512 fun header_markup txt = Toplevel.keep (fn state => |
512 fun header_markup txt = Toplevel.keep (fn state => |
513 if Toplevel.is_toplevel state then check_text txt state |
513 if Toplevel.is_toplevel state then check_text txt state |
514 else raise Toplevel.UNDEF); |
514 else raise Toplevel.UNDEF); |
515 |
515 |