# HG changeset patch
# User haftmann
# Date 1114754581 -7200
# Node ID d6aa6c707acf81d2192cffde52695784ec3583f2
# Parent  a83b9dc6151aa2c0faed363a362aa8d7e2e8bc1d
added antiquotations typeof, const, term_style, thm_style, term_type (something still to be done)

diff -r a83b9dc6151a -r d6aa6c707acf etc/settings
--- a/etc/settings	Fri Apr 29 00:52:12 2005 +0200
+++ b/etc/settings	Fri Apr 29 08:03:01 2005 +0200
@@ -60,7 +60,7 @@
 
 
 ###
-### Compilation options for isatool usedir
+### Compilation options for isatool usedir[B
 ### (as on command line)
 ###
 
diff -r a83b9dc6151a -r d6aa6c707acf src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Fri Apr 29 00:52:12 2005 +0200
+++ b/src/Pure/Isar/isar_output.ML	Fri Apr 29 08:03:01 2005 +0200
@@ -29,6 +29,7 @@
       (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 =
@@ -310,6 +311,31 @@
   ("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 *)
 
@@ -346,8 +372,24 @@
 
 fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.extern_skolem ctxt;
 
+fun pretty_term_typ 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_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_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_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
@@ -385,10 +427,15 @@
 
 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)),
+  ("term_type", args Args.local_term (output_with pretty_term_typ)),
+  ("typeof", args Args.local_term (output_with pretty_term_typeof)),
+  ("const", args Args.local_term (output_with pretty_term_const)),
   ("typ", args Args.local_typ_raw (output_with ProofContext.pretty_typ)),
   ("text", args (Scan.lift Args.name) (output_with (K pretty_text))),
   ("goals", output_goals true),
@@ -396,4 +443,7 @@
   ("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;
+