pretty_locale: backquote notes;
authorwenzelm
Sat Jan 07 12:26:31 2006 +0100 (2006-01-07)
changeset 1860646e7fc90fde3
parent 18605 b971e113dee7
child 18607 7b074c340aac
pretty_locale: backquote notes;
src/Pure/Isar/element.ML
     1.1 --- a/src/Pure/Isar/element.ML	Sat Jan 07 12:26:29 2006 +0100
     1.2 +++ b/src/Pure/Isar/element.ML	Sat Jan 07 12:26:31 2006 +0100
     1.3 @@ -77,7 +77,7 @@
     1.4    let
     1.5      val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt;
     1.6      val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
     1.7 -    val prt_thm = Pretty.quote o ProofContext.pretty_thm ctxt;
     1.8 +    val prt_thm = Pretty.backquote o ProofContext.pretty_thm ctxt;
     1.9      val prt_atts = Args.pretty_attribs ctxt;
    1.10  
    1.11      fun prt_syn syn =
    1.12 @@ -89,20 +89,20 @@
    1.13      fun prt_constrain (x, T) = prt_fix (x, SOME T, SOME (Syntax.NoSyn));
    1.14  
    1.15      fun prt_name name = Pretty.str (ProofContext.extern_thm ctxt name);
    1.16 -    fun prt_name_atts (name, atts) =
    1.17 +    fun prt_name_atts (name, atts) sep =
    1.18        if name = "" andalso null atts then []
    1.19 -      else [Pretty.block (Pretty.breaks (prt_name name :: prt_atts atts @ [Pretty.str ":"]))];
    1.20 +      else [Pretty.block (Pretty.breaks (prt_name name :: prt_atts atts @ [Pretty.str sep]))];
    1.21  
    1.22      fun prt_asm (a, ts) =
    1.23 -      Pretty.block (Pretty.breaks (prt_name_atts a @ map (prt_term o fst) ts));
    1.24 +      Pretty.block (Pretty.breaks (prt_name_atts a ":" @ map (prt_term o fst) ts));
    1.25      fun prt_def (a, (t, _)) =
    1.26 -      Pretty.block (Pretty.breaks (prt_name_atts a @ [prt_term t]));
    1.27 +      Pretty.block (Pretty.breaks (prt_name_atts a ":" @ [prt_term t]));
    1.28  
    1.29      fun prt_fact (ths, []) = map prt_thm ths
    1.30        | prt_fact (ths, atts) =
    1.31            Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths)) :: prt_atts atts;
    1.32      fun prt_note (a, ths) =
    1.33 -      Pretty.block (Pretty.breaks (List.concat (prt_name_atts a :: map prt_fact ths)));
    1.34 +      Pretty.block (Pretty.breaks (List.concat (prt_name_atts a "=" :: map prt_fact ths)));
    1.35  
    1.36      fun items _ [] = []
    1.37        | items prfx (x :: xs) =