equal
deleted
inserted
replaced
129 val one_day = seconds (24.0 * 60.0 * 60.0) |
129 val one_day = seconds (24.0 * 60.0 * 60.0) |
130 val one_year = seconds (365.0 * 24.0 * 60.0 * 60.0) |
130 val one_year = seconds (365.0 * 24.0 * 60.0 * 60.0) |
131 |
131 |
132 fun hackish_string_of_term ctxt = |
132 fun hackish_string_of_term ctxt = |
133 (* FIXME: map_aterms (fn Free (s, T) => Free (if Name.is_internal s then "_" else s, T) | t => t) |
133 (* FIXME: map_aterms (fn Free (s, T) => Free (if Name.is_internal s then "_" else s, T) | t => t) |
134 #> *) Print_Mode.setmp [] (Syntax.string_of_term ctxt) |
134 #> *) Syntax.pretty_term ctxt |
|
135 #> Pretty.pure_string_of |
135 #> Protocol_Message.clean_output |
136 #> Protocol_Message.clean_output |
136 #> simplify_spaces |
137 #> simplify_spaces |
137 |
138 |
138 val spying_version = "d" |
139 val spying_version = "d" |
139 |
140 |