258 |
258 |
259 (** print_state **) |
259 (** print_state **) |
260 |
260 |
261 val verbose = ProofContext.verbose; |
261 val verbose = ProofContext.verbose; |
262 |
262 |
|
263 fun print_facts _ None = () |
|
264 | print_facts s (Some ths) = |
|
265 Pretty.writeln (Pretty.big_list (s ^ " facts:") (map Display.pretty_thm ths)); |
|
266 |
263 fun print_state (state as State ({context, facts, mode, goal = _}, nodes)) = |
267 fun print_state (state as State ({context, facts, mode, goal = _}, nodes)) = |
264 let |
268 let |
265 val ref (_, _, begin_goal) = Goals.current_goals_markers; |
269 val ref (_, _, begin_goal) = Goals.current_goals_markers; |
266 |
|
267 fun print_facts None = () |
|
268 | print_facts (Some ths) = |
|
269 Pretty.writeln (Pretty.big_list "Current facts:" (map Display.pretty_thm ths)); |
|
270 |
270 |
271 fun levels_up 0 = "" |
271 fun levels_up 0 = "" |
272 | levels_up i = " (" ^ string_of_int i ^ " levels up)"; |
272 | levels_up i = " (" ^ string_of_int i ^ " levels up)"; |
273 |
273 |
274 fun print_goal (i, ((kind, name, _, _), (_, thm))) = |
274 fun print_goal (i, ((kind, name, _, _), (goal_facts, thm))) = |
275 (writeln (kind_name kind ^ " " ^ quote name ^ levels_up (i div 2) ^ ":"); |
275 (print_facts "Using" (if null goal_facts then None else Some goal_facts); |
|
276 writeln (kind_name kind ^ " " ^ quote name ^ levels_up (i div 2) ^ ":"); |
276 Locale.print_goals_marker begin_goal (! goals_limit) thm); |
277 Locale.print_goals_marker begin_goal (! goals_limit) thm); |
277 in |
278 in |
278 writeln ("Nesting level: " ^ string_of_int (length nodes div 2)); |
279 writeln ("Nesting level: " ^ string_of_int (length nodes div 2)); |
279 writeln ""; |
280 writeln ""; |
280 writeln (enclose "`" "'" (mode_name mode) ^ " mode"); |
281 writeln (enclose "`" "'" (mode_name mode) ^ " mode"); |
281 writeln ""; |
282 writeln ""; |
282 if ! verbose orelse mode = Forward then |
283 if ! verbose orelse mode = Forward then |
283 (ProofContext.print_context context; |
284 (ProofContext.print_context context; |
284 writeln ""; |
285 writeln ""; |
285 print_facts facts; |
286 print_facts "Current" facts; |
286 print_goal (find_goal 0 state)) |
287 print_goal (find_goal 0 state)) |
287 else if mode = ForwardChain then print_facts facts |
288 else if mode = ForwardChain then print_facts "Picking" facts |
288 else print_goal (find_goal 0 state) |
289 else print_goal (find_goal 0 state) |
289 end; |
290 end; |
290 |
291 |
291 |
292 |
292 |
293 |