# HG changeset patch
# User wenzelm
# Date 1257191868 -3600
# Node ID bb3a5fa94a91fe02f58569ea473a39e6aa8823e2
# Parent  d64545e6cba59a57fc46e6c9fd5633ea109175ce
modernized structure Proof_Display;

diff -r d64545e6cba5 -r bb3a5fa94a91 src/Pure/Isar/constdefs.ML
--- 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);
diff -r d64545e6cba5 -r bb3a5fa94a91 src/Pure/Isar/element.ML
--- 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 [];
 
diff -r d64545e6cba5 -r bb3a5fa94a91 src/Pure/Isar/isar_cmd.ML
--- 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;
 
diff -r d64545e6cba5 -r bb3a5fa94a91 src/Pure/Isar/obtain.ML
--- 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]] =
diff -r d64545e6cba5 -r bb3a5fa94a91 src/Pure/Isar/proof.ML
--- 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)
diff -r d64545e6cba5 -r bb3a5fa94a91 src/Pure/Isar/proof_display.ML
--- 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 *)
diff -r d64545e6cba5 -r bb3a5fa94a91 src/Pure/Isar/specification.ML
--- 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;
diff -r d64545e6cba5 -r bb3a5fa94a91 src/Pure/ProofGeneral/proof_general_pgip.ML
--- 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)]
diff -r d64545e6cba5 -r bb3a5fa94a91 src/Pure/pure_setup.ML
--- 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";