substantial tuning -- adapted to common conventions;
authorwenzelm
Tue May 17 18:10:43 2005 +0200 (2005-05-17 ago)
changeset 159904ef32dcbb44f
parent 15989 80dd2f5780df
child 15991 670f8e4b5a98
substantial tuning -- adapted to common conventions;
src/Pure/Isar/term_style.ML
     1.1 --- a/src/Pure/Isar/term_style.ML	Tue May 17 18:10:42 2005 +0200
     1.2 +++ b/src/Pure/Isar/term_style.ML	Tue May 17 18:10:43 2005 +0200
     1.3 @@ -2,56 +2,64 @@
     1.4      ID:         $Id$
     1.5      Author:     Florian Haftmann, TU Muenchen
     1.6  
     1.7 -Styles for terms, to use with the "term_style" and "thm_style" antiquotations
     1.8 +Styles for terms, to use with the "term_style" and "thm_style" antiquotations.
     1.9  *)
    1.10  
    1.11 -(* style data *)
    1.12  signature TERM_STYLE =
    1.13  sig
    1.14 -  val lookup_style: theory -> string -> (Proof.context -> term -> term)
    1.15 -  val update_style: string -> (Proof.context -> term -> term) -> theory -> theory
    1.16 +  val the_style: theory -> string -> (Proof.context -> term -> term)
    1.17 +  val add_style: string -> (Proof.context -> term -> term) -> theory -> theory
    1.18 +  val print_styles: theory -> unit
    1.19  end;
    1.20  
    1.21  structure TermStyle: TERM_STYLE =
    1.22  struct
    1.23  
    1.24 +(* style data *)
    1.25 +
    1.26 +fun err_dup_styles names =
    1.27 +  error ("Duplicate declaration of antiquote style(s): " ^ commas_quote names);
    1.28 +
    1.29  structure StyleArgs =
    1.30  struct
    1.31    val name = "Isar/style";
    1.32 -  type T = (Proof.context -> term -> term) Symtab.table;
    1.33 +  type T = ((Proof.context -> term -> term) * stamp) Symtab.table;
    1.34    val empty = Symtab.empty;
    1.35    val copy = I;
    1.36    val prep_ext = I;
    1.37 -  fun merge x = Symtab.merge (K true) x;
    1.38 -  fun print _ table =
    1.39 -    Pretty.strs ("defined styles:" :: (Symtab.keys table))
    1.40 -    |> Pretty.writeln;
    1.41 +  fun merge tabs = Symtab.merge eq_snd tabs
    1.42 +    handle Symtab.DUPS dups => err_dup_styles dups;
    1.43 +  fun print _ tab = Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys tab));
    1.44  end;
    1.45  
    1.46  structure StyleData = TheoryDataFun(StyleArgs);
    1.47 +val _ = Context.add_setup [StyleData.init];
    1.48 +val print_styles = StyleData.print;
    1.49 +
    1.50  
    1.51  (* accessors *)
    1.52 -fun lookup_style thy name =
    1.53 -  case Symtab.lookup ((StyleData.get thy), name)
    1.54 -    of NONE => raise (ERROR_MESSAGE ("no style named " ^ name))
    1.55 -     | SOME style => style
    1.56  
    1.57 -fun update_style name style thy =
    1.58 -  thy
    1.59 -  |> StyleData.put (Symtab.update ((name, style), StyleData.get thy));
    1.60 +fun the_style thy name =
    1.61 +  (case Symtab.lookup (StyleData.get thy, name) of
    1.62 +    NONE => error ("Unknown antiquote style: " ^ quote name)
    1.63 +  | SOME (style, _) => style);
    1.64 +
    1.65 +fun add_style name style thy =
    1.66 +  StyleData.map (curry Symtab.update_new (name, (style, stamp ()))) thy
    1.67 +    handle Symtab.DUP _ => err_dup_styles [name];
    1.68 +
    1.69  
    1.70  (* predefined styles *)
    1.71 +
    1.72  fun style_binargs ctxt t =
    1.73    let val concl = ObjectLogic.drop_judgment (ProofContext.sign_of ctxt) (Logic.strip_imp_concl t) in
    1.74      case concl of (_ $ l $ r) => (l, r)
    1.75 -        | _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl)
    1.76 +    | _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl)
    1.77    end;
    1.78  
    1.79 -(* initialization *)
    1.80 -val _ = Context.add_setup [StyleData.init,
    1.81 -  update_style "lhs" (fst oo style_binargs),
    1.82 -  update_style "rhs" (snd oo style_binargs),
    1.83 -  update_style "conclusion" (K Logic.strip_imp_concl)
    1.84 -];
    1.85 +val _ = Context.add_setup
    1.86 + [add_style "lhs" (fst oo style_binargs),
    1.87 +  add_style "rhs" (snd oo style_binargs),
    1.88 +  add_style "conclusion" (K Logic.strip_imp_concl)];
    1.89  
    1.90  end;