tuned output;
authorwenzelm
Sun May 03 17:41:54 2015 +0200 (2015-05-03)
changeset 60244523ec7e4b022
parent 60243 5901cb4db0ae
child 60245 79ad597fe699
tuned output;
src/Pure/Isar/named_target.ML
     1.1 --- a/src/Pure/Isar/named_target.ML	Sun May 03 17:36:46 2015 +0200
     1.2 +++ b/src/Pure/Isar/named_target.ML	Sun May 03 17:41:54 2015 +0200
     1.3 @@ -116,28 +116,28 @@
     1.4  (* pretty *)
     1.5  
     1.6  fun pretty (target, is_class) ctxt =
     1.7 -  let
     1.8 -    val target_name =
     1.9 -      [Pretty.keyword1 (if is_class then "class" else "locale"), Pretty.brk 1,
    1.10 -        Locale.pretty_name ctxt target];
    1.11 -    val fixes =
    1.12 -      map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
    1.13 -        (#1 (Proof_Context.inferred_fixes ctxt));
    1.14 -    val assumes =
    1.15 -      map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
    1.16 -        (Assumption.all_assms_of ctxt);
    1.17 -    val elems =
    1.18 -      (if null fixes then [] else [Element.Fixes fixes]) @
    1.19 -      (if null assumes then [] else [Element.Assumes assumes]);
    1.20 -    val body_elems =
    1.21 -      if target = "" then []
    1.22 -      else if null elems then [Pretty.block target_name]
    1.23 +  if target = "" then
    1.24 +    [Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1,
    1.25 +      Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))]]
    1.26 +  else if is_class then Class.pretty_specification (Proof_Context.theory_of ctxt) target
    1.27 +  else
    1.28 +    (* FIXME pretty locale content *)
    1.29 +    let
    1.30 +      val target_name = [Pretty.keyword1 "locale", Pretty.brk 1, Locale.pretty_name ctxt target];
    1.31 +      val fixes =
    1.32 +        map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
    1.33 +          (#1 (Proof_Context.inferred_fixes ctxt));
    1.34 +      val assumes =
    1.35 +        map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
    1.36 +          (Assumption.all_assms_of ctxt);
    1.37 +      val elems =
    1.38 +        (if null fixes then [] else [Element.Fixes fixes]) @
    1.39 +        (if null assumes then [] else [Element.Assumes assumes]);
    1.40 +    in
    1.41 +      if null elems then [Pretty.block target_name]
    1.42        else [Pretty.block (Pretty.fbreaks (Pretty.block (target_name @ [Pretty.str " ="]) ::
    1.43 -        map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))];
    1.44 -  in
    1.45 -    Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1,
    1.46 -      Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))] :: body_elems
    1.47 -  end;
    1.48 +        map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))]
    1.49 +    end;
    1.50  
    1.51  
    1.52  (* init *)