modernized structure Proof_Display;
authorwenzelm
Mon Nov 02 20:57:48 2009 +0100 (2009-11-02)
changeset 33389bb3a5fa94a91
parent 33388 d64545e6cba5
child 33390 5b499f36dd25
modernized structure Proof_Display;
src/Pure/Isar/constdefs.ML
src/Pure/Isar/element.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_display.ML
src/Pure/Isar/specification.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/pure_setup.ML
     1.1 --- a/src/Pure/Isar/constdefs.ML	Mon Nov 02 20:50:48 2009 +0100
     1.2 +++ b/src/Pure/Isar/constdefs.ML	Mon Nov 02 20:57:48 2009 +0100
     1.3 @@ -60,7 +60,7 @@
     1.4      val ctxt = ProofContext.init thy;
     1.5      val (structs, _) = prep_vars (map (fn (x, T) => (x, T, Structure)) raw_structs) ctxt;
     1.6      val (decls, thy') = fold_map (gen_constdef prep_vars prep_prop prep_att structs) specs thy;
     1.7 -  in Pretty.writeln (ProofDisplay.pretty_consts ctxt (K true) decls); thy' end;
     1.8 +  in Pretty.writeln (Proof_Display.pretty_consts ctxt (K true) decls); thy' end;
     1.9  
    1.10  val add_constdefs = gen_constdefs ProofContext.read_vars Syntax.read_prop Attrib.attribute;
    1.11  val add_constdefs_i = gen_constdefs ProofContext.cert_vars ProofContext.cert_prop (K I);
     2.1 --- a/src/Pure/Isar/element.ML	Mon Nov 02 20:50:48 2009 +0100
     2.2 +++ b/src/Pure/Isar/element.ML	Mon Nov 02 20:57:48 2009 +0100
     2.3 @@ -294,7 +294,7 @@
     2.4  fun witness_local_proof after_qed cmd wit_propss goal_ctxt int =
     2.5    gen_witness_proof (fn after_qed' => fn propss =>
     2.6      Proof.map_context (K goal_ctxt)
     2.7 -    #> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
     2.8 +    #> Proof.local_goal (Proof_Display.print_results int) (K I) ProofContext.bind_propp_i
     2.9        cmd NONE after_qed' (map (pair Thm.empty_binding) propss))
    2.10      (fn wits => fn _ => after_qed wits) wit_propss [];
    2.11  
     3.1 --- a/src/Pure/Isar/isar_cmd.ML	Mon Nov 02 20:50:48 2009 +0100
     3.2 +++ b/src/Pure/Isar/isar_cmd.ML	Mon Nov 02 20:57:48 2009 +0100
     3.3 @@ -324,7 +324,7 @@
     3.4  val print_context = Toplevel.keep Toplevel.print_state_context;
     3.5  
     3.6  fun print_theory verbose = Toplevel.unknown_theory o
     3.7 -  Toplevel.keep (Pretty.writeln o ProofDisplay.pretty_full_theory verbose o Toplevel.theory_of);
     3.8 +  Toplevel.keep (Pretty.writeln o Proof_Display.pretty_full_theory verbose o Toplevel.theory_of);
     3.9  
    3.10  val print_syntax = Toplevel.unknown_context o
    3.11    Toplevel.keep (ProofContext.print_syntax o Toplevel.context_of);
    3.12 @@ -346,8 +346,8 @@
    3.13  val print_theorems_theory = Toplevel.keep (fn state =>
    3.14    Toplevel.theory_of state |>
    3.15    (case Toplevel.previous_context_of state of
    3.16 -    SOME prev => ProofDisplay.print_theorems_diff (ProofContext.theory_of prev)
    3.17 -  | NONE => ProofDisplay.print_theorems));
    3.18 +    SOME prev => Proof_Display.print_theorems_diff (ProofContext.theory_of prev)
    3.19 +  | NONE => Proof_Display.print_theorems));
    3.20  
    3.21  val print_theorems = Toplevel.unknown_context o print_theorems_theory o print_theorems_proof;
    3.22  
     4.1 --- a/src/Pure/Isar/obtain.ML	Mon Nov 02 20:50:48 2009 +0100
     4.2 +++ b/src/Pure/Isar/obtain.ML	Mon Nov 02 20:57:48 2009 +0100
     4.3 @@ -298,7 +298,7 @@
     4.4  
     4.5      val goal = Var (("guess", 0), propT);
     4.6      fun print_result ctxt' (k, [(s, [_, th])]) =
     4.7 -      ProofDisplay.print_results int ctxt' (k, [(s, [th])]);
     4.8 +      Proof_Display.print_results int ctxt' (k, [(s, [th])]);
     4.9      val before_qed = SOME (Method.primitive_text (Goal.conclude #> MetaSimplifier.norm_hhf #>
    4.10          (fn th => Goal.protect (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))));
    4.11      fun after_qed [[_, res]] =
     5.1 --- a/src/Pure/Isar/proof.ML	Mon Nov 02 20:50:48 2009 +0100
     5.2 +++ b/src/Pure/Isar/proof.ML	Mon Nov 02 20:57:48 2009 +0100
     5.3 @@ -941,7 +941,7 @@
     5.4  local
     5.5  
     5.6  fun gen_have prep_att prepp before_qed after_qed stmt int =
     5.7 -  local_goal (ProofDisplay.print_results int) prep_att prepp "have" before_qed after_qed stmt;
     5.8 +  local_goal (Proof_Display.print_results int) prep_att prepp "have" before_qed after_qed stmt;
     5.9  
    5.10  fun gen_show prep_att prepp before_qed after_qed stmt int state =
    5.11    let
    5.12 @@ -949,14 +949,14 @@
    5.13      val rule = Unsynchronized.ref (NONE: thm option);
    5.14      fun fail_msg ctxt =
    5.15        "Local statement will fail to refine any pending goal" ::
    5.16 -      (case ! rule of NONE => [] | SOME th => [ProofDisplay.string_of_rule ctxt "Failed" th])
    5.17 +      (case ! rule of NONE => [] | SOME th => [Proof_Display.string_of_rule ctxt "Failed" th])
    5.18        |> cat_lines;
    5.19  
    5.20      fun print_results ctxt res =
    5.21 -      if ! testing then () else ProofDisplay.print_results int ctxt res;
    5.22 +      if ! testing then () else Proof_Display.print_results int ctxt res;
    5.23      fun print_rule ctxt th =
    5.24        if ! testing then rule := SOME th
    5.25 -      else if int then priority (ProofDisplay.string_of_rule ctxt "Successful" th)
    5.26 +      else if int then priority (Proof_Display.string_of_rule ctxt "Successful" th)
    5.27        else ();
    5.28      val test_proof =
    5.29        try (local_skip_proof true)
     6.1 --- a/src/Pure/Isar/proof_display.ML	Mon Nov 02 20:50:48 2009 +0100
     6.2 +++ b/src/Pure/Isar/proof_display.ML	Mon Nov 02 20:57:48 2009 +0100
     6.3 @@ -21,7 +21,7 @@
     6.4    val pretty_consts: Proof.context -> (string * typ -> bool) -> (string * typ) list -> Pretty.T
     6.5  end
     6.6  
     6.7 -structure ProofDisplay: PROOF_DISPLAY =
     6.8 +structure Proof_Display: PROOF_DISPLAY =
     6.9  struct
    6.10  
    6.11  (* toplevel pretty printing *)
     7.1 --- a/src/Pure/Isar/specification.ML	Mon Nov 02 20:50:48 2009 +0100
     7.2 +++ b/src/Pure/Isar/specification.ML	Mon Nov 02 20:57:48 2009 +0100
     7.3 @@ -67,7 +67,7 @@
     7.4  (* diagnostics *)
     7.5  
     7.6  fun print_consts _ _ [] = ()
     7.7 -  | print_consts ctxt pred cs = Pretty.writeln (ProofDisplay.pretty_consts ctxt pred cs);
     7.8 +  | print_consts ctxt pred cs = Pretty.writeln (Proof_Display.pretty_consts ctxt pred cs);
     7.9  
    7.10  
    7.11  (* prepare specification *)
    7.12 @@ -267,7 +267,7 @@
    7.13        ((name, map attrib atts),
    7.14          bs |> map (fn (b, more_atts) => (prep_fact lthy b, map attrib more_atts))));
    7.15      val (res, lthy') = lthy |> LocalTheory.notes kind facts;
    7.16 -    val _ = ProofDisplay.print_results true lthy' ((kind, ""), res);
    7.17 +    val _ = Proof_Display.print_results true lthy' ((kind, ""), res);
    7.18    in (res, lthy') end;
    7.19  
    7.20  val theorems = gen_theorems (K I) (K I);
    7.21 @@ -357,12 +357,12 @@
    7.22          |> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
    7.23          |> (fn (res, lthy') =>
    7.24            if Binding.is_empty name andalso null atts then
    7.25 -            (ProofDisplay.print_results true lthy' ((kind, ""), res); lthy')
    7.26 +            (Proof_Display.print_results true lthy' ((kind, ""), res); lthy')
    7.27            else
    7.28              let
    7.29                val ([(res_name, _)], lthy'') = lthy'
    7.30                  |> LocalTheory.notes kind [((name, atts), [(maps #2 res, [])])];
    7.31 -              val _ = ProofDisplay.print_results true lthy' ((kind, res_name), res);
    7.32 +              val _ = Proof_Display.print_results true lthy' ((kind, res_name), res);
    7.33              in lthy'' end)
    7.34          |> after_qed results'
    7.35        end;
     8.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Nov 02 20:50:48 2009 +0100
     8.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Nov 02 20:57:48 2009 +0100
     8.3 @@ -658,7 +658,7 @@
     8.4          fun strings_of_thm (thy, name) =
     8.5            map (Display.string_of_thm_global thy) (PureThy.get_thms thy name)
     8.6  
     8.7 -        val string_of_thy = Pretty.string_of o ProofDisplay.pretty_full_theory false
     8.8 +        val string_of_thy = Pretty.string_of o Proof_Display.pretty_full_theory false
     8.9      in
    8.10          case (thyname, objtype) of
    8.11              (_, ObjTheory) => idvalue [string_of_thy (ThyInfo.get_theory name)]
     9.1 --- a/src/Pure/pure_setup.ML	Mon Nov 02 20:50:48 2009 +0100
     9.2 +++ b/src/Pure/pure_setup.ML	Mon Nov 02 20:57:48 2009 +0100
     9.3 @@ -22,13 +22,13 @@
     9.4  toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
     9.5  toplevel_pp ["Position", "T"] "Pretty.position";
     9.6  toplevel_pp ["Binding", "binding"] "Pretty.str o quote o Binding.str_of";
     9.7 -toplevel_pp ["Thm", "thm"] "ProofDisplay.pp_thm";
     9.8 -toplevel_pp ["Thm", "cterm"] "ProofDisplay.pp_cterm";
     9.9 -toplevel_pp ["Thm", "ctyp"] "ProofDisplay.pp_ctyp";
    9.10 -toplevel_pp ["typ"] "ProofDisplay.pp_typ Pure.thy";
    9.11 +toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm";
    9.12 +toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm";
    9.13 +toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp";
    9.14 +toplevel_pp ["typ"] "Proof_Display.pp_typ Pure.thy";
    9.15  toplevel_pp ["Context", "theory"] "Context.pretty_thy";
    9.16  toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref";
    9.17 -toplevel_pp ["Context", "Proof", "context"] "ProofDisplay.pp_context";
    9.18 +toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
    9.19  toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast";
    9.20  toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode";
    9.21  toplevel_pp ["File", "ident"] "Pretty.str o quote o File.rep_ident";