# HG changeset patch # User haftmann # Date 1115109211 -7200 # Node ID 6d6d3fabef02864dbd5872289041c9e9c8890f8c # Parent cd4983c76548b3728b07f7a6ceeccd8bf13e9329 final implementation of antiquotations styles diff -r cd4983c76548 -r 6d6d3fabef02 src/Pure/Isar/ROOT.ML --- a/src/Pure/Isar/ROOT.ML Tue May 03 10:32:32 2005 +0200 +++ b/src/Pure/Isar/ROOT.ML Tue May 03 10:33:31 2005 +0200 @@ -32,6 +32,7 @@ (*toplevel environment*) use "toplevel.ML"; +use "term_style.ML"; use "isar_output.ML"; use "session.ML"; diff -r cd4983c76548 -r 6d6d3fabef02 src/Pure/Isar/isar_output.ML --- a/src/Pure/Isar/isar_output.ML Tue May 03 10:32:32 2005 +0200 +++ b/src/Pure/Isar/isar_output.ML Tue May 03 10:33:31 2005 +0200 @@ -1,6 +1,6 @@ (* Title: Pure/Isar/isar_output.ML ID: $Id$ - Author: Markus Wenzel, TU Muenchen + Author: Florian Haftmann, TU Muenchen Isar theory output. *) @@ -29,7 +29,6 @@ (Toplevel.transition * (Toplevel.state -> Toplevel.state -> Buffer.T -> Buffer.T)) list * Buffer.T val output_with: (Proof.context -> 'a -> Pretty.T) -> Args.src -> Proof.context -> 'a -> string - val put_style: string -> (Term.term -> Term.term) -> theory -> theory end; structure IsarOutput: ISAR_OUTPUT = @@ -311,32 +310,6 @@ ("source", Library.setmp source o boolean), ("goals_limit", Library.setmp goals_limit o integer)]; -(* style data *) - -exception Style of string; - -structure StyleArgs = -struct - val name = "Isar/style"; - type T = (string * (Term.term -> Term.term)) list; - val empty = []; - val copy = I; - val prep_ext = I; - fun merge (a1, a2) = Library.foldl Library.overwrite (a1, a2); - (* piecewise update of a1 by a2 *) - fun print _ _ = raise (Style "cannot print style (not implemented)"); -end; - -structure Style = TheoryDataFun(StyleArgs); - -fun get_style thy name = - case Library.assoc_string ((Style.get thy), name) - of NONE => raise (Style ("no style named " ^ name)) - | SOME style => style - -fun put_style name style thy = - Style.put (Library.overwrite ((Style.get thy), (name, style))) thy; - (* commands *) fun cond_quote prt = @@ -372,40 +345,29 @@ fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.extern_skolem ctxt; -fun pretty_term_typ ctxt term = Pretty.block [ +fun pretty_term_typ_old ctxt term = Pretty.block [ ((ProofContext.pretty_term ctxt o ProofContext.extern_skolem ctxt) term), (Pretty.str "\\") (* q'n'd *), ((ProofContext.pretty_typ ctxt o Term.type_of o ProofContext.extern_skolem ctxt) term) ] -fun pretty_term_typeof ctxt = ProofContext.pretty_typ ctxt o Term.type_of o ProofContext.extern_skolem ctxt; +fun pretty_term_typ ctxt term = let val t = (ProofContext.extern_skolem ctxt term) in + ProofContext.pretty_term ctxt ( + Syntax.const Syntax.constrainC $ t $ Syntax.term_of_typ (!show_sorts) (fastype_of t) + ) +end; -fun pretty_term_const ctxt term = case Sign.const_type (ProofContext.sign_of ctxt) (Term.string_of_term term) of - NONE => raise (Output.ERROR_MESSAGE ("Not a defined constant: " ^ (Term.string_of_term term))) - | (SOME _) => (ProofContext.pretty_term ctxt o ProofContext.extern_skolem ctxt) term; +fun pretty_term_typeof ctxt = ProofContext.pretty_typ ctxt o Term.fastype_of o ProofContext.extern_skolem ctxt; + +fun pretty_term_const ctxt (Const c) = pretty_term ctxt (Const c) + | pretty_term_const ctxt term = raise (Output.ERROR_MESSAGE ("Not a defined constant: " ^ (Term.string_of_term term))) fun pretty_thm ctxt = pretty_term ctxt o Thm.prop_of; -fun pretty_term_style ctxt (name, term) = pretty_term ctxt ((get_style (ProofContext.theory_of ctxt) name) term); +fun pretty_term_style ctxt (name, term) = pretty_term ctxt ((Style.get_style (ProofContext.theory_of ctxt) name) term); fun pretty_thm_style ctxt (name, thm) = pretty_term_style ctxt (name, Thm.prop_of thm); -fun lhs_of (Const ("==",_) $ t $ _) = t - | lhs_of (Const ("Trueprop",_) $ t) = lhs_of t - | lhs_of (Const ("==>",_) $ _ $ t) = lhs_of t - | lhs_of (_ $ t $ _) = t - | lhs_of _ = error ("Binary operator expected") - -fun pretty_lhs ctxt = pretty_term ctxt o lhs_of o Thm.prop_of; - -fun rhs_of (Const ("==",_) $ _ $ t) = t - | rhs_of (Const ("Trueprop",_) $ t) = rhs_of t - | rhs_of (Const ("==>",_) $ _ $ t) = rhs_of t - | rhs_of (_ $ _ $ t) = t - | rhs_of _ = error ("Binary operator expected") - -fun pretty_rhs ctxt = pretty_term ctxt o rhs_of o Thm.prop_of; - fun pretty_prf full ctxt thms = (* FIXME context syntax!? *) Pretty.chunks (map (ProofSyntax.pretty_proof_of full) thms); @@ -428,8 +390,6 @@ val _ = add_commands [("thm", args Attrib.local_thmss (output_seq_with pretty_thm)), ("thm_style", args ((Scan.lift Args.name) -- Attrib.local_thm) (output_with pretty_thm_style)), - ("lhs", args Attrib.local_thmss (output_seq_with pretty_lhs)), - ("rhs", args Attrib.local_thmss (output_seq_with pretty_rhs)), ("prop", args Args.local_prop (output_with pretty_term)), ("term", args Args.local_term (output_with pretty_term)), ("term_style", args ((Scan.lift Args.name) -- Args.local_term) (output_with pretty_term_style)), @@ -443,7 +403,5 @@ ("prf", args Attrib.local_thmss (output_with (pretty_prf false))), ("full_prf", args Attrib.local_thmss (output_with (pretty_prf true)))]; -val _ = Context.add_setup [Style.init]; - end; diff -r cd4983c76548 -r 6d6d3fabef02 src/Pure/Isar/term_style.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Isar/term_style.ML Tue May 03 10:33:31 2005 +0200 @@ -0,0 +1,64 @@ +(* Title: Pure/Isar/term_style.ML + ID: $Id$ + Author: Florian Haftmann, TU Muenchen + +Styles for terms, to use with the "term_style" and "thm_style" antiquotations +*) + +signature STYLE = +sig + val get_style: theory -> string -> (Term.term -> Term.term) + val put_style: string -> (Term.term -> Term.term) -> theory -> theory +end; + +structure Style: STYLE = +struct + +(* exception *) +exception STYLE of string; + +(* style data *) +structure StyleArgs = +struct + val name = "Isar/style"; + type T = (string * (Term.term -> Term.term)) list; + val empty = []; + val copy = I; + val prep_ext = I; + fun merge (a1, a2) = Library.foldl Library.overwrite (a1, a2); + (* piecewise update of a1 by a2 *) + fun print _ _ = raise (STYLE "cannot print style (not implemented)"); +end; + +structure StyleData = TheoryDataFun(StyleArgs); + +(* accessors *) +fun get_style thy name = + case Library.assoc_string ((StyleData.get thy), name) + of NONE => raise (STYLE ("no style named " ^ name)) + | SOME style => style + +fun put_style name style thy = + StyleData.put (Library.overwrite ((StyleData.get thy), (name, style))) thy; + +(* predefined styles *) +fun style_lhs (Const ("==", _) $ t $ _) = t + | style_lhs (Const ("Trueprop", _) $ t) = style_lhs t + | style_lhs (Const ("==>", _) $ _ $ t) = style_lhs t + | style_lhs (_ $ t $ _) = t + | style_lhs _ = error ("Binary operator expected") + +fun style_rhs (Const ("==", _) $ _ $ t) = t + | style_rhs (Const ("Trueprop", _) $ t) = style_rhs t + | style_rhs (Const ("==>", _) $ _ $ t) = style_rhs t + | style_rhs (_ $ _ $ t) = t + | style_rhs _ = error ("Binary operator expected") + +(* initialization *) +val _ = Context.add_setup [StyleData.init, + put_style "lhs" style_lhs, + put_style "rhs" style_rhs, + put_style "conclusion" Logic.strip_imp_concl +]; + +end;