equal
deleted
inserted
replaced
314 val current_goals_markers = ref ("", "", ""); |
314 val current_goals_markers = ref ("", "", ""); |
315 |
315 |
316 fun print_current_goals_default n max th = |
316 fun print_current_goals_default n max th = |
317 let val ref (begin_state, end_state, begin_goal) = current_goals_markers; |
317 let val ref (begin_state, end_state, begin_goal) = current_goals_markers; |
318 val ngoals = nprems_of th in |
318 val ngoals = nprems_of th in |
319 writeln (begin_state ^ "Level " ^ string_of_int n ^ |
319 writeln (begin_state ^ "Level " ^ string_of_int n ^ |
320 " (" ^ string_of_int ngoals ^ " subgoal" ^ |
320 (if ngoals > 0 then " (" ^ string_of_int ngoals ^ " subgoal" ^ |
321 (if ngoals <> 1 then "s" else "") ^ ")"); |
321 (if ngoals <> 1 then "s" else "") ^ ")" |
|
322 else "")); |
322 Locale.print_goals_marker begin_goal max th; |
323 Locale.print_goals_marker begin_goal max th; |
323 if end_state = "" then () else writeln end_state |
324 if end_state = "" then () else writeln end_state |
324 end; |
325 end; |
325 |
326 |
326 val print_current_goals_fn = ref print_current_goals_default; |
327 val print_current_goals_fn = ref print_current_goals_default; |