equal
deleted
inserted
replaced
332 val print_context = Toplevel.keep Toplevel.print_state_context; |
332 val print_context = Toplevel.keep Toplevel.print_state_context; |
333 |
333 |
334 fun print_theory verbose = Toplevel.unknown_theory o |
334 fun print_theory verbose = Toplevel.unknown_theory o |
335 Toplevel.keep (ProofDisplay.print_full_theory verbose o Toplevel.theory_of); |
335 Toplevel.keep (ProofDisplay.print_full_theory verbose o Toplevel.theory_of); |
336 |
336 |
337 val print_syntax = Toplevel.unknown_theory o |
337 val print_syntax = Toplevel.unknown_context o |
338 Toplevel.keep (Display.print_syntax o Toplevel.theory_of) o |
338 Toplevel.keep (ProofContext.print_syntax o Toplevel.context_of); |
339 Toplevel.keep (ProofContext.print_syntax o Proof.context_of o Toplevel.proof_of); |
|
340 |
339 |
341 val print_facts = Toplevel.unknown_context o Toplevel.keep (fn state => |
340 val print_facts = Toplevel.unknown_context o Toplevel.keep (fn state => |
342 ProofContext.setmp_verbose |
341 ProofContext.setmp_verbose |
343 ProofContext.print_lthms (Toplevel.context_of state)); |
342 ProofContext.print_lthms (Toplevel.context_of state)); |
344 |
343 |
350 Toplevel.theory_of state |> |
349 Toplevel.theory_of state |> |
351 (case Option.map Toplevel.theory_node (History.previous (Toplevel.node_history_of state)) of |
350 (case Option.map Toplevel.theory_node (History.previous (Toplevel.node_history_of state)) of |
352 SOME (SOME prev_thy) => ProofDisplay.print_theorems_diff (Context.theory_of prev_thy) |
351 SOME (SOME prev_thy) => ProofDisplay.print_theorems_diff (Context.theory_of prev_thy) |
353 | _ => ProofDisplay.print_theorems)); |
352 | _ => ProofDisplay.print_theorems)); |
354 |
353 |
355 val print_theorems = Toplevel.unknown_theory o print_theorems_theory o print_theorems_proof; |
354 val print_theorems = Toplevel.unknown_context o print_theorems_theory o print_theorems_proof; |
356 |
355 |
357 val print_locales = Toplevel.unknown_theory o |
356 val print_locales = Toplevel.unknown_theory o |
358 Toplevel.keep (Locale.print_locales o Toplevel.theory_of); |
357 Toplevel.keep (Locale.print_locales o Toplevel.theory_of); |
359 |
358 |
360 fun print_locale (show_facts, (import, body)) = Toplevel.unknown_theory o |
359 fun print_locale (show_facts, (import, body)) = Toplevel.unknown_theory o |
416 in FindTheorems.print_theorems ctxt opt_goal opt_lim spec end); |
415 in FindTheorems.print_theorems ctxt opt_goal opt_lim spec end); |
417 |
416 |
418 |
417 |
419 (* print proof context contents *) |
418 (* print proof context contents *) |
420 |
419 |
421 val print_binds = Toplevel.unknown_proof o Toplevel.keep (fn state => |
420 val print_binds = Toplevel.unknown_context o Toplevel.keep (fn state => |
422 ProofContext.setmp_verbose |
421 ProofContext.setmp_verbose ProofContext.print_binds (Toplevel.context_of state)); |
423 ProofContext.print_binds (Proof.context_of (Toplevel.proof_of state))); |
422 |
424 |
423 val print_cases = Toplevel.unknown_context o Toplevel.keep (fn state => |
425 val print_cases = Toplevel.unknown_proof o Toplevel.keep (fn state => |
424 ProofContext.setmp_verbose ProofContext.print_cases (Toplevel.context_of state)); |
426 ProofContext.setmp_verbose |
|
427 ProofContext.print_cases (Proof.context_of (Toplevel.proof_of state))); |
|
428 |
425 |
429 |
426 |
430 (* print theorems, terms, types etc. *) |
427 (* print theorems, terms, types etc. *) |
431 |
428 |
432 local |
429 local |