equal
deleted
inserted
replaced
50 val current_goals_markers: (string * string * string) ref |
50 val current_goals_markers: (string * string * string) ref |
51 val print_current_goals_default: (int -> int -> thm -> unit) |
51 val print_current_goals_default: (int -> int -> thm -> unit) |
52 val print_current_goals_fn : (int -> int -> thm -> unit) ref |
52 val print_current_goals_fn : (int -> int -> thm -> unit) ref |
53 val pop_proof : unit -> thm list |
53 val pop_proof : unit -> thm list |
54 val pr : unit -> unit |
54 val pr : unit -> unit |
|
55 val disable_pr : unit -> unit |
|
56 val enable_pr : unit -> unit |
55 val prlev : int -> unit |
57 val prlev : int -> unit |
56 val prlim : int -> unit |
58 val prlim : int -> unit |
57 val premises : unit -> thm list |
59 val premises : unit -> thm list |
58 val prin : term -> unit |
60 val prin : term -> unit |
59 val printyp : typ -> unit |
61 val printyp : typ -> unit |
328 if end_state = "" then () else writeln end_state |
330 if end_state = "" then () else writeln end_state |
329 end; |
331 end; |
330 |
332 |
331 val print_current_goals_fn = ref print_current_goals_default; |
333 val print_current_goals_fn = ref print_current_goals_default; |
332 |
334 |
333 (*Print a level of the goal stack.*) |
335 (* Print a level of the goal stack -- subject to quiet mode *) |
|
336 |
|
337 val quiet = ref false; |
|
338 fun disable_pr () = quiet := true; |
|
339 fun enable_pr () = quiet := false; |
|
340 |
334 fun print_top ((th, _), pairs) = |
341 fun print_top ((th, _), pairs) = |
335 !print_current_goals_fn (length pairs) (!goals_limit) th; |
342 if ! quiet then () |
|
343 else ! print_current_goals_fn (length pairs) (! goals_limit) th; |
336 |
344 |
337 (*Printing can raise exceptions, so the assignment occurs last. |
345 (*Printing can raise exceptions, so the assignment occurs last. |
338 Can do setstate[(st,Seq.empty)] to set st as the state. *) |
346 Can do setstate[(st,Seq.empty)] to set st as the state. *) |
339 fun setstate newgoals = |
347 fun setstate newgoals = |
340 (print_top (pop newgoals); undo_list := newgoals :: !undo_list); |
348 (print_top (pop newgoals); undo_list := newgoals :: !undo_list); |
382 else error ("Level number must lie between 0 and " ^ |
390 else error ("Level number must lie between 0 and " ^ |
383 string_of_int level) |
391 string_of_int level) |
384 end; |
392 end; |
385 |
393 |
386 (*Print the given level of the proof; prlev ~1 prints previous level*) |
394 (*Print the given level of the proof; prlev ~1 prints previous level*) |
387 fun prlev n = apply_fun (print_top o pop o (chop_level n)); |
395 fun prlev n = (enable_pr (); apply_fun (print_top o pop o (chop_level n))); |
388 fun pr () = apply_fun print_top; |
396 fun pr () = (enable_pr (); apply_fun print_top); |
389 |
397 |
390 (*Set goals_limit and print again*) |
398 (*Set goals_limit and print again*) |
391 fun prlim n = (goals_limit:=n; pr()); |
399 fun prlim n = (goals_limit:=n; pr()); |
392 |
400 |
393 (** the goal.... commands |
401 (** the goal.... commands |