src/Pure/Thy/thy_output.ML
changeset 32890 77df12652210
parent 32738 15bb09ca0378
child 32898 e871d897969c
     1.1 --- a/src/Pure/Thy/thy_output.ML	Wed Oct 07 14:01:26 2009 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Wed Oct 07 16:57:56 2009 +0200
     1.3 @@ -470,11 +470,11 @@
     1.4  
     1.5  fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
     1.6  
     1.7 -fun pretty_term_style ctxt (name, t) =
     1.8 -  pretty_term ctxt (TermStyle.the_style (ProofContext.theory_of ctxt) name ctxt t);
     1.9 +fun pretty_term_style ctxt (style, t) =
    1.10 +  pretty_term ctxt (style t);
    1.11  
    1.12 -fun pretty_thm_style ctxt (name, th) =
    1.13 -  pretty_term_style ctxt (name, Thm.full_prop_of th);
    1.14 +fun pretty_thm_style ctxt (style, th) =
    1.15 +  pretty_term_style ctxt (style, Thm.full_prop_of th);
    1.16  
    1.17  fun pretty_prf full ctxt = ProofSyntax.pretty_proof_of ctxt full;
    1.18  
    1.19 @@ -513,15 +513,19 @@
    1.20  fun basic_entities name scan pretty = antiquotation name scan
    1.21    (fn {source, context, ...} => output o maybe_pretty_source (pretty context) source);
    1.22  
    1.23 +fun basic_entities_style name scan pretty = antiquotation name scan
    1.24 +  (fn {source, context, ...} => fn (style, xs) =>
    1.25 +    output (maybe_pretty_source (fn x => pretty context (style, x)) source xs));
    1.26 +
    1.27  fun basic_entity name scan = basic_entities name (scan >> single);
    1.28  
    1.29  in
    1.30  
    1.31 -val _ = basic_entities "thm" Attrib.thms pretty_thm;
    1.32 -val _ = basic_entity "thm_style" (Scan.lift Args.liberal_name -- Attrib.thm) pretty_thm_style;
    1.33 -val _ = basic_entity "prop" Args.prop pretty_term;
    1.34 -val _ = basic_entity "term" Args.term pretty_term;
    1.35 -val _ = basic_entity "term_style" (Scan.lift Args.liberal_name -- Args.term) pretty_term_style;
    1.36 +val _ = basic_entities_style "thm" (Term_Style.parse -- Attrib.thms) pretty_thm_style;
    1.37 +val _ = basic_entities_style "thm_style" (Term_Style.parse_bare -- Attrib.thms) pretty_thm_style;
    1.38 +val _ = basic_entity "prop" (Term_Style.parse -- Args.prop) pretty_term_style;
    1.39 +val _ = basic_entity "term" (Term_Style.parse -- Args.term) pretty_term_style;
    1.40 +val _ = basic_entity "term_style" (Term_Style.parse_bare -- Args.term) pretty_term_style;
    1.41  val _ = basic_entity "term_type" Args.term pretty_term_typ;
    1.42  val _ = basic_entity "typeof" Args.term pretty_term_typeof;
    1.43  val _ = basic_entity "const" Args.const_proper pretty_const;