equal
deleted
inserted
replaced
109 fun error_msg s = ! error_fn (output s); |
109 fun error_msg s = ! error_fn (output s); |
110 fun prompt s = ! prompt_fn (output s); |
110 fun prompt s = ! prompt_fn (output s); |
111 |
111 |
112 val tolerate_legacy_features = ref true; |
112 val tolerate_legacy_features = ref true; |
113 fun legacy_feature s = |
113 fun legacy_feature s = |
114 (if ! tolerate_legacy_features then warning else error) ("Legacy feature: " ^ s); |
114 (if ! tolerate_legacy_features then warning else error) ("Legacy feature! " ^ s); |
115 |
115 |
116 fun no_warnings f = setmp warning_fn (K ()) f; |
116 fun no_warnings f = setmp warning_fn (K ()) f; |
117 |
117 |
118 val debugging = ref false; |
118 val debugging = ref false; |
119 fun debug s = if ! debugging then ! debug_fn (output (s ())) else () |
119 fun debug s = if ! debugging then ! debug_fn (output (s ())) else () |