final implementation of antiquotations styles

--- 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";
 

--- 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 "\\<Colon>") (* 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;
 

--- /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;