equal
deleted
inserted
replaced
70 |
70 |
71 |
71 |
72 (* use ML text *) |
72 (* use ML text *) |
73 |
73 |
74 val ml_output = (writeln, error_msg: string -> unit); |
74 val ml_output = (writeln, error_msg: string -> unit); |
75 fun use_output verb txt = use_text ml_output verb (Symbol.plain_output txt); |
75 |
|
76 fun use_output verb txt = use_text ml_output verb (Symbol.escape txt); |
76 |
77 |
77 fun use_mltext txt verb opt_thy = setmp opt_thy (fn () => use_output verb txt) (); |
78 fun use_mltext txt verb opt_thy = setmp opt_thy (fn () => use_output verb txt) (); |
78 fun use_mltext_theory txt verb thy = #2 (pass_theory thy (use_output verb) txt); |
79 fun use_mltext_theory txt verb thy = #2 (pass_theory thy (use_output verb) txt); |
79 |
80 |
80 fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");") false; |
81 fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");") false; |