equal
deleted
inserted
replaced
646 |> (if Config.get context display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |
646 |> (if Config.get context display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |
647 else verb_text))); |
647 else verb_text))); |
648 |
648 |
649 fun ml_enclose bg en source = |
649 fun ml_enclose bg en source = |
650 ML_Lex.read Position.none bg @ |
650 ML_Lex.read Position.none bg @ |
651 ML_Lex.read_source source @ |
651 ML_Lex.read_source false source @ |
652 ML_Lex.read Position.none en; |
652 ML_Lex.read Position.none en; |
653 |
653 |
654 in |
654 in |
655 |
655 |
656 val _ = Theory.setup |
656 val _ = Theory.setup |