src/Pure/Isar/proof_context.ML
changeset 28212 44831b583999
parent 28209 02f3222a392d
child 28396 72695dd4395d
     1.1 --- a/src/Pure/Isar/proof_context.ML	Fri Sep 12 12:04:19 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Sep 12 12:04:20 2008 +0200
     1.3 @@ -35,6 +35,7 @@
     1.4    val transfer: theory -> Proof.context -> Proof.context
     1.5    val theory: (theory -> theory) -> Proof.context -> Proof.context
     1.6    val theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
     1.7 +  val extern_fact: Proof.context -> string -> xstring
     1.8    val pretty_term_abbrev: Proof.context -> term -> Pretty.T
     1.9    val pretty_thm_legacy: thm -> Pretty.T
    1.10    val pretty_thm: Proof.context -> thm -> Pretty.T
    1.11 @@ -282,6 +283,21 @@
    1.12  
    1.13  (** pretty printing **)
    1.14  
    1.15 +(* extern *)
    1.16 +
    1.17 +fun extern_fact ctxt name =
    1.18 +  let
    1.19 +    val local_facts = facts_of ctxt;
    1.20 +    val global_facts = PureThy.facts_of (theory_of ctxt);
    1.21 +  in
    1.22 +    if is_some (Facts.lookup (Context.Proof ctxt) local_facts name)
    1.23 +    then Facts.extern local_facts name
    1.24 +    else Facts.extern global_facts name
    1.25 +  end;
    1.26 +
    1.27 +
    1.28 +(* pretty *)
    1.29 +
    1.30  fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt);
    1.31  
    1.32  fun pretty_thm_legacy th =
    1.33 @@ -295,13 +311,14 @@
    1.34  fun pretty_thms ctxt [th] = pretty_thm ctxt th
    1.35    | pretty_thms ctxt ths = Pretty.blk (0, Pretty.fbreaks (map (pretty_thm ctxt) ths));
    1.36  
    1.37 -val extern_fact = Facts.extern o facts_of;
    1.38 +fun pretty_fact_name ctxt a = Pretty.block
    1.39 +  [Pretty.markup (Markup.fact a) [Pretty.str (extern_fact ctxt a)], Pretty.str ":"];
    1.40  
    1.41  fun pretty_fact ctxt ("", ths) = pretty_thms ctxt ths
    1.42    | pretty_fact ctxt (a, [th]) = Pretty.block
    1.43 -      [Pretty.str (extern_fact ctxt a ^ ":"), Pretty.brk 1, pretty_thm ctxt th]
    1.44 +      [pretty_fact_name ctxt a, Pretty.brk 1, pretty_thm ctxt th]
    1.45    | pretty_fact ctxt (a, ths) = Pretty.block
    1.46 -      (Pretty.fbreaks (Pretty.str (extern_fact ctxt a ^ ":") :: map (pretty_thm ctxt) ths));
    1.47 +      (Pretty.fbreaks (pretty_fact_name ctxt a :: map (pretty_thm ctxt) ths));
    1.48  
    1.49  val string_of_thm = Pretty.string_of oo pretty_thm;
    1.50  
    1.51 @@ -1265,10 +1282,10 @@
    1.52      val props = Facts.props local_facts;
    1.53      val facts =
    1.54        (if null props then [] else [("unnamed", props)]) @
    1.55 -      Facts.extern_static [] local_facts;
    1.56 +      Facts.dest_static [] local_facts;
    1.57    in
    1.58      if null facts andalso not (! verbose) then []
    1.59 -    else [Pretty.big_list "facts:" (map (pretty_fact ctxt) facts)]
    1.60 +    else [Pretty.big_list "facts:" (map #1 (sort_wrt (#1 o #2) (map (`(pretty_fact ctxt)) facts)))]
    1.61    end;
    1.62  
    1.63  val print_lthms = Pretty.writeln o Pretty.chunks o pretty_lthms;