equal
deleted
inserted
replaced
277 (*Print goals of current level*) |
277 (*Print goals of current level*) |
278 val current_goals_markers = ref ("", "", ""); |
278 val current_goals_markers = ref ("", "", ""); |
279 |
279 |
280 fun print_current_goals_default n max th = |
280 fun print_current_goals_default n max th = |
281 let val ref (begin_state, end_state, begin_goal) = current_goals_markers in |
281 let val ref (begin_state, end_state, begin_goal) = current_goals_markers in |
282 writeln begin_state; |
282 if begin_state = "" then () else writeln begin_state; |
283 writeln ("Level " ^ string_of_int n); |
283 writeln ("Level " ^ string_of_int n); |
284 Locale.print_goals_marker begin_goal max th; |
284 Locale.print_goals_marker begin_goal max th; |
285 writeln end_state |
285 if end_state = "" then () else writeln end_state |
286 end; |
286 end; |
287 |
287 |
288 val print_current_goals_fn = ref print_current_goals_default; |
288 val print_current_goals_fn = ref print_current_goals_default; |
289 |
289 |
290 (*Print a level of the goal stack.*) |
290 (*Print a level of the goal stack.*) |