equal
deleted
inserted
replaced
138 |
138 |
139 fun with_vanilla_print_mode f x = |
139 fun with_vanilla_print_mode f x = |
140 Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ())) f x |
140 Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ())) f x |
141 |
141 |
142 fun hackish_string_of_term ctxt = |
142 fun hackish_string_of_term ctxt = |
143 with_vanilla_print_mode (Syntax.string_of_term ctxt) #> unyxml #> simplify_spaces |
143 with_vanilla_print_mode (Syntax.string_of_term ctxt) #> YXML.content_of #> simplify_spaces |
144 |
144 |
145 val spying_version = "d" |
145 val spying_version = "d" |
146 |
146 |
147 fun spying false _ = () |
147 fun spying false _ = () |
148 | spying true f = |
148 | spying true f = |