--- a/src/Pure/Isar/constdefs.ML Mon Nov 02 20:50:48 2009 +0100
+++ b/src/Pure/Isar/constdefs.ML Mon Nov 02 20:57:48 2009 +0100
@@ -60,7 +60,7 @@
val ctxt = ProofContext.init thy;
val (structs, _) = prep_vars (map (fn (x, T) => (x, T, Structure)) raw_structs) ctxt;
val (decls, thy') = fold_map (gen_constdef prep_vars prep_prop prep_att structs) specs thy;
- in Pretty.writeln (ProofDisplay.pretty_consts ctxt (K true) decls); thy' end;
+ in Pretty.writeln (Proof_Display.pretty_consts ctxt (K true) decls); thy' end;
val add_constdefs = gen_constdefs ProofContext.read_vars Syntax.read_prop Attrib.attribute;
val add_constdefs_i = gen_constdefs ProofContext.cert_vars ProofContext.cert_prop (K I);
--- a/src/Pure/Isar/element.ML Mon Nov 02 20:50:48 2009 +0100
+++ b/src/Pure/Isar/element.ML Mon Nov 02 20:57:48 2009 +0100
@@ -294,7 +294,7 @@
fun witness_local_proof after_qed cmd wit_propss goal_ctxt int =
gen_witness_proof (fn after_qed' => fn propss =>
Proof.map_context (K goal_ctxt)
- #> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
+ #> Proof.local_goal (Proof_Display.print_results int) (K I) ProofContext.bind_propp_i
cmd NONE after_qed' (map (pair Thm.empty_binding) propss))
(fn wits => fn _ => after_qed wits) wit_propss [];
--- a/src/Pure/Isar/isar_cmd.ML Mon Nov 02 20:50:48 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Mon Nov 02 20:57:48 2009 +0100
@@ -324,7 +324,7 @@
val print_context = Toplevel.keep Toplevel.print_state_context;
fun print_theory verbose = Toplevel.unknown_theory o
- Toplevel.keep (Pretty.writeln o ProofDisplay.pretty_full_theory verbose o Toplevel.theory_of);
+ Toplevel.keep (Pretty.writeln o Proof_Display.pretty_full_theory verbose o Toplevel.theory_of);
val print_syntax = Toplevel.unknown_context o
Toplevel.keep (ProofContext.print_syntax o Toplevel.context_of);
@@ -346,8 +346,8 @@
val print_theorems_theory = Toplevel.keep (fn state =>
Toplevel.theory_of state |>
(case Toplevel.previous_context_of state of
- SOME prev => ProofDisplay.print_theorems_diff (ProofContext.theory_of prev)
- | NONE => ProofDisplay.print_theorems));
+ SOME prev => Proof_Display.print_theorems_diff (ProofContext.theory_of prev)
+ | NONE => Proof_Display.print_theorems));
val print_theorems = Toplevel.unknown_context o print_theorems_theory o print_theorems_proof;
--- a/src/Pure/Isar/obtain.ML Mon Nov 02 20:50:48 2009 +0100
+++ b/src/Pure/Isar/obtain.ML Mon Nov 02 20:57:48 2009 +0100
@@ -298,7 +298,7 @@
val goal = Var (("guess", 0), propT);
fun print_result ctxt' (k, [(s, [_, th])]) =
- ProofDisplay.print_results int ctxt' (k, [(s, [th])]);
+ Proof_Display.print_results int ctxt' (k, [(s, [th])]);
val before_qed = SOME (Method.primitive_text (Goal.conclude #> MetaSimplifier.norm_hhf #>
(fn th => Goal.protect (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))));
fun after_qed [[_, res]] =
--- a/src/Pure/Isar/proof.ML Mon Nov 02 20:50:48 2009 +0100
+++ b/src/Pure/Isar/proof.ML Mon Nov 02 20:57:48 2009 +0100
@@ -941,7 +941,7 @@
local
fun gen_have prep_att prepp before_qed after_qed stmt int =
- local_goal (ProofDisplay.print_results int) prep_att prepp "have" before_qed after_qed stmt;
+ local_goal (Proof_Display.print_results int) prep_att prepp "have" before_qed after_qed stmt;
fun gen_show prep_att prepp before_qed after_qed stmt int state =
let
@@ -949,14 +949,14 @@
val rule = Unsynchronized.ref (NONE: thm option);
fun fail_msg ctxt =
"Local statement will fail to refine any pending goal" ::
- (case ! rule of NONE => [] | SOME th => [ProofDisplay.string_of_rule ctxt "Failed" th])
+ (case ! rule of NONE => [] | SOME th => [Proof_Display.string_of_rule ctxt "Failed" th])
|> cat_lines;
fun print_results ctxt res =
- if ! testing then () else ProofDisplay.print_results int ctxt res;
+ if ! testing then () else Proof_Display.print_results int ctxt res;
fun print_rule ctxt th =
if ! testing then rule := SOME th
- else if int then priority (ProofDisplay.string_of_rule ctxt "Successful" th)
+ else if int then priority (Proof_Display.string_of_rule ctxt "Successful" th)
else ();
val test_proof =
try (local_skip_proof true)
--- a/src/Pure/Isar/proof_display.ML Mon Nov 02 20:50:48 2009 +0100
+++ b/src/Pure/Isar/proof_display.ML Mon Nov 02 20:57:48 2009 +0100
@@ -21,7 +21,7 @@
val pretty_consts: Proof.context -> (string * typ -> bool) -> (string * typ) list -> Pretty.T
end
-structure ProofDisplay: PROOF_DISPLAY =
+structure Proof_Display: PROOF_DISPLAY =
struct
(* toplevel pretty printing *)
--- a/src/Pure/Isar/specification.ML Mon Nov 02 20:50:48 2009 +0100
+++ b/src/Pure/Isar/specification.ML Mon Nov 02 20:57:48 2009 +0100
@@ -67,7 +67,7 @@
(* diagnostics *)
fun print_consts _ _ [] = ()
- | print_consts ctxt pred cs = Pretty.writeln (ProofDisplay.pretty_consts ctxt pred cs);
+ | print_consts ctxt pred cs = Pretty.writeln (Proof_Display.pretty_consts ctxt pred cs);
(* prepare specification *)
@@ -267,7 +267,7 @@
((name, map attrib atts),
bs |> map (fn (b, more_atts) => (prep_fact lthy b, map attrib more_atts))));
val (res, lthy') = lthy |> LocalTheory.notes kind facts;
- val _ = ProofDisplay.print_results true lthy' ((kind, ""), res);
+ val _ = Proof_Display.print_results true lthy' ((kind, ""), res);
in (res, lthy') end;
val theorems = gen_theorems (K I) (K I);
@@ -357,12 +357,12 @@
|> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
|> (fn (res, lthy') =>
if Binding.is_empty name andalso null atts then
- (ProofDisplay.print_results true lthy' ((kind, ""), res); lthy')
+ (Proof_Display.print_results true lthy' ((kind, ""), res); lthy')
else
let
val ([(res_name, _)], lthy'') = lthy'
|> LocalTheory.notes kind [((name, atts), [(maps #2 res, [])])];
- val _ = ProofDisplay.print_results true lthy' ((kind, res_name), res);
+ val _ = Proof_Display.print_results true lthy' ((kind, res_name), res);
in lthy'' end)
|> after_qed results'
end;
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Nov 02 20:50:48 2009 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Nov 02 20:57:48 2009 +0100
@@ -658,7 +658,7 @@
fun strings_of_thm (thy, name) =
map (Display.string_of_thm_global thy) (PureThy.get_thms thy name)
- val string_of_thy = Pretty.string_of o ProofDisplay.pretty_full_theory false
+ val string_of_thy = Pretty.string_of o Proof_Display.pretty_full_theory false
in
case (thyname, objtype) of
(_, ObjTheory) => idvalue [string_of_thy (ThyInfo.get_theory name)]
--- a/src/Pure/pure_setup.ML Mon Nov 02 20:50:48 2009 +0100
+++ b/src/Pure/pure_setup.ML Mon Nov 02 20:57:48 2009 +0100
@@ -22,13 +22,13 @@
toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
toplevel_pp ["Position", "T"] "Pretty.position";
toplevel_pp ["Binding", "binding"] "Pretty.str o quote o Binding.str_of";
-toplevel_pp ["Thm", "thm"] "ProofDisplay.pp_thm";
-toplevel_pp ["Thm", "cterm"] "ProofDisplay.pp_cterm";
-toplevel_pp ["Thm", "ctyp"] "ProofDisplay.pp_ctyp";
-toplevel_pp ["typ"] "ProofDisplay.pp_typ Pure.thy";
+toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm";
+toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm";
+toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp";
+toplevel_pp ["typ"] "Proof_Display.pp_typ Pure.thy";
toplevel_pp ["Context", "theory"] "Context.pretty_thy";
toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref";
-toplevel_pp ["Context", "Proof", "context"] "ProofDisplay.pp_context";
+toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast";
toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode";
toplevel_pp ["File", "ident"] "Pretty.str o quote o File.rep_ident";