# HG changeset patch
# User wenzelm
# Date 1116346243 -7200
# Node ID 4ef32dcbb44f62a6e43e4679827e52252ff0f364
# Parent  80dd2f5780df8ccc9590d6b3819582184ec487d7
substantial tuning -- adapted to common conventions;

diff -r 80dd2f5780df -r 4ef32dcbb44f src/Pure/Isar/term_style.ML
--- a/src/Pure/Isar/term_style.ML	Tue May 17 18:10:42 2005 +0200
+++ b/src/Pure/Isar/term_style.ML	Tue May 17 18:10:43 2005 +0200
@@ -2,56 +2,64 @@
     ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 
-Styles for terms, to use with the "term_style" and "thm_style" antiquotations
+Styles for terms, to use with the "term_style" and "thm_style" antiquotations.
 *)
 
-(* style data *)
 signature TERM_STYLE =
 sig
-  val lookup_style: theory -> string -> (Proof.context -> term -> term)
-  val update_style: string -> (Proof.context -> term -> term) -> theory -> theory
+  val the_style: theory -> string -> (Proof.context -> term -> term)
+  val add_style: string -> (Proof.context -> term -> term) -> theory -> theory
+  val print_styles: theory -> unit
 end;
 
 structure TermStyle: TERM_STYLE =
 struct
 
+(* style data *)
+
+fun err_dup_styles names =
+  error ("Duplicate declaration of antiquote style(s): " ^ commas_quote names);
+
 structure StyleArgs =
 struct
   val name = "Isar/style";
-  type T = (Proof.context -> term -> term) Symtab.table;
+  type T = ((Proof.context -> term -> term) * stamp) Symtab.table;
   val empty = Symtab.empty;
   val copy = I;
   val prep_ext = I;
-  fun merge x = Symtab.merge (K true) x;
-  fun print _ table =
-    Pretty.strs ("defined styles:" :: (Symtab.keys table))
-    |> Pretty.writeln;
+  fun merge tabs = Symtab.merge eq_snd tabs
+    handle Symtab.DUPS dups => err_dup_styles dups;
+  fun print _ tab = Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys tab));
 end;
 
 structure StyleData = TheoryDataFun(StyleArgs);
+val _ = Context.add_setup [StyleData.init];
+val print_styles = StyleData.print;
+
 
 (* accessors *)
-fun lookup_style thy name =
-  case Symtab.lookup ((StyleData.get thy), name)
-    of NONE => raise (ERROR_MESSAGE ("no style named " ^ name))
-     | SOME style => style
 
-fun update_style name style thy =
-  thy
-  |> StyleData.put (Symtab.update ((name, style), StyleData.get thy));
+fun the_style thy name =
+  (case Symtab.lookup (StyleData.get thy, name) of
+    NONE => error ("Unknown antiquote style: " ^ quote name)
+  | SOME (style, _) => style);
+
+fun add_style name style thy =
+  StyleData.map (curry Symtab.update_new (name, (style, stamp ()))) thy
+    handle Symtab.DUP _ => err_dup_styles [name];
+
 
 (* predefined styles *)
+
 fun style_binargs ctxt t =
   let val concl = ObjectLogic.drop_judgment (ProofContext.sign_of ctxt) (Logic.strip_imp_concl t) in
     case concl of (_ $ l $ r) => (l, r)
-        | _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl)
+    | _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl)
   end;
 
-(* initialization *)
-val _ = Context.add_setup [StyleData.init,
-  update_style "lhs" (fst oo style_binargs),
-  update_style "rhs" (snd oo style_binargs),
-  update_style "conclusion" (K Logic.strip_imp_concl)
-];
+val _ = Context.add_setup
+ [add_style "lhs" (fst oo style_binargs),
+  add_style "rhs" (snd oo style_binargs),
+  add_style "conclusion" (K Logic.strip_imp_concl)];
 
 end;