src/Pure/Thy/term_style.ML
changeset 23655 d2d1138e0ddc
parent 23577 c5b93c69afd3
child 24920 2a45e400fdad
equal deleted inserted replaced
23654:a2ad1c166ac8 23655:d2d1138e0ddc
    16 structure TermStyle: TERM_STYLE =
    16 structure TermStyle: TERM_STYLE =
    17 struct
    17 struct
    18 
    18 
    19 (* style data *)
    19 (* style data *)
    20 
    20 
    21 fun err_dup_styles names =
    21 fun err_dup_style name =
    22   error ("Duplicate declaration of antiquote style(s): " ^ commas_quote names);
    22   error ("Duplicate declaration of antiquote style: " ^ quote name);
    23 
    23 
    24 structure StyleData = TheoryDataFun
    24 structure StyleData = TheoryDataFun
    25 (
    25 (
    26   type T = ((Proof.context -> term -> term) * stamp) Symtab.table;
    26   type T = ((Proof.context -> term -> term) * stamp) Symtab.table;
    27   val empty = Symtab.empty;
    27   val empty = Symtab.empty;
    28   val copy = I;
    28   val copy = I;
    29   val extend = I;
    29   val extend = I;
    30   fun merge _ tabs : T = Symtab.merge (eq_snd (op =)) tabs
    30   fun merge _ tabs : T = Symtab.merge (eq_snd (op =)) tabs
    31     handle Symtab.DUPS dups => err_dup_styles dups;
    31     handle Symtab.DUP dup => err_dup_style dup;
    32 );
    32 );
    33 
    33 
    34 fun print_styles thy =
    34 fun print_styles thy =
    35   Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys (StyleData.get thy)));
    35   Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys (StyleData.get thy)));
    36 
    36 
    42     NONE => error ("Unknown antiquote style: " ^ quote name)
    42     NONE => error ("Unknown antiquote style: " ^ quote name)
    43   | SOME (style, _) => style);
    43   | SOME (style, _) => style);
    44 
    44 
    45 fun add_style name style thy =
    45 fun add_style name style thy =
    46   StyleData.map (Symtab.update_new (name, (style, stamp ()))) thy
    46   StyleData.map (Symtab.update_new (name, (style, stamp ()))) thy
    47     handle Symtab.DUP _ => err_dup_styles [name];
    47     handle Symtab.DUP _ => err_dup_style name;
    48 
    48 
    49 
    49 
    50 (* predefined styles *)
    50 (* predefined styles *)
    51 
    51 
    52 fun style_binargs ctxt t =
    52 fun style_binargs ctxt t =