src/Pure/Isar/term_style.ML
changeset 15960 9bd6550dc004
parent 15918 6d6d3fabef02
child 15961 24c6b96b4a2f
     1.1 --- a/src/Pure/Isar/term_style.ML	Fri May 13 20:21:41 2005 +0200
     1.2 +++ b/src/Pure/Isar/term_style.ML	Sat May 14 21:31:13 2005 +0200
     1.3 @@ -5,60 +5,53 @@
     1.4  Styles for terms, to use with the "term_style" and "thm_style" antiquotations
     1.5  *)
     1.6  
     1.7 -signature STYLE =
     1.8 +(* style data *)
     1.9 +signature TERM_STYLE =
    1.10  sig
    1.11 -  val get_style: theory -> string -> (Term.term -> Term.term)
    1.12 -  val put_style: string -> (Term.term -> Term.term) -> theory -> theory
    1.13 +  val lookup_style: theory -> string -> (Proof.context -> term -> term)
    1.14 +  val update_style: string -> (Proof.context -> term -> term) -> theory -> theory
    1.15  end;
    1.16  
    1.17 -structure Style: STYLE =
    1.18 +structure TermStyle: TERM_STYLE =
    1.19  struct
    1.20  
    1.21 -(* exception *)
    1.22 -exception STYLE of string;
    1.23 -
    1.24 -(* style data *)
    1.25  structure StyleArgs =
    1.26  struct
    1.27    val name = "Isar/style";
    1.28 -  type T = (string * (Term.term -> Term.term)) list;
    1.29 -  val empty = [];
    1.30 +  type T = (Proof.context -> term -> term) Symtab.table;
    1.31 +  val empty = Symtab.empty;
    1.32    val copy = I;
    1.33    val prep_ext = I;
    1.34 -  fun merge (a1, a2) = Library.foldl Library.overwrite (a1, a2);
    1.35 -    (* piecewise update of a1 by a2 *)
    1.36 -  fun print _ _ = raise (STYLE "cannot print style (not implemented)");
    1.37 +  val merge = Symtab.merge (K true);
    1.38 +  fun print _ table =
    1.39 +    Pretty.strs ("defined styles:" :: (Symtab.keys table))
    1.40 +    |> Pretty.writeln;
    1.41  end;
    1.42  
    1.43  structure StyleData = TheoryDataFun(StyleArgs);
    1.44  
    1.45  (* accessors *)
    1.46 -fun get_style thy name =
    1.47 -  case Library.assoc_string ((StyleData.get thy), name)
    1.48 -    of NONE => raise (STYLE ("no style named " ^ name))
    1.49 +fun lookup_style thy name =
    1.50 +  case Symtab.lookup ((StyleData.get thy), name)
    1.51 +    of NONE => raise (ERROR_MESSAGE ("no style named " ^ name))
    1.52       | SOME style => style
    1.53  
    1.54 -fun put_style name style thy =
    1.55 -  StyleData.put (Library.overwrite ((StyleData.get thy), (name, style))) thy;
    1.56 +fun update_style name style thy =
    1.57 +  thy
    1.58 +  |> StyleData.put (Symtab.update ((name, style), StyleData.get thy));
    1.59  
    1.60  (* predefined styles *)
    1.61 -fun style_lhs (Const ("==", _) $ t $ _) = t
    1.62 -  | style_lhs (Const ("Trueprop", _) $ t) = style_lhs t
    1.63 -  | style_lhs (Const ("==>", _) $ _ $ t) = style_lhs t
    1.64 -  | style_lhs (_ $ t $ _) = t
    1.65 -  | style_lhs _ = error ("Binary operator expected")
    1.66 -
    1.67 -fun style_rhs (Const ("==", _) $ _ $ t) = t
    1.68 -  | style_rhs (Const ("Trueprop", _) $ t) = style_rhs t
    1.69 -  | style_rhs (Const ("==>", _) $ _ $ t) = style_rhs t
    1.70 -  | style_rhs (_ $ _ $ t) = t
    1.71 -  | style_rhs _ = error ("Binary operator expected")
    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 +  end;
    1.77  
    1.78  (* initialization *)
    1.79  val _ = Context.add_setup [StyleData.init,
    1.80 -  put_style "lhs" style_lhs,
    1.81 -  put_style "rhs" style_rhs,
    1.82 -  put_style "conclusion" Logic.strip_imp_concl
    1.83 +  update_style "lhs" (fst oo style_binargs),
    1.84 +  update_style "rhs" (snd oo style_binargs),
    1.85 +  update_style "conclusion" (K Logic.strip_imp_concl)
    1.86  ];
    1.87  
    1.88  end;