equal
deleted
inserted
replaced
114 struct |
114 struct |
115 |
115 |
116 (** auxiliary **) |
116 (** auxiliary **) |
117 |
117 |
118 val debug = ref false; |
118 val debug = ref false; |
119 fun debug_msg f x = (if !debug then Output.debug (f x) else (); x); |
119 fun debug_msg f x = (if !debug then Output.tracing (f x) else (); x); |
120 val soft_exc = ref true; |
120 val soft_exc = ref true; |
121 |
121 |
122 fun unfoldl dest x = |
122 fun unfoldl dest x = |
123 case dest x |
123 case dest x |
124 of NONE => (x, []) |
124 of NONE => (x, []) |