modernized data managed via Name_Space.table;
authorwenzelm
Mon Mar 10 17:09:40 2014 +0100 (2014-03-10)
changeset 56030ef2ffd622264
parent 56029 8bedca4bd5a3
child 56031 2e3329b89383
modernized data managed via Name_Space.table;
src/Pure/Thy/term_style.ML
     1.1 --- a/src/Pure/Thy/term_style.ML	Mon Mar 10 16:30:07 2014 +0100
     1.2 +++ b/src/Pure/Thy/term_style.ML	Mon Mar 10 17:09:40 2014 +0100
     1.3 @@ -6,46 +6,38 @@
     1.4  
     1.5  signature TERM_STYLE =
     1.6  sig
     1.7 -  val setup: string -> (Proof.context -> term -> term) parser -> theory -> theory
     1.8 +  val setup: binding -> (Proof.context -> term -> term) parser -> theory -> theory
     1.9    val parse: (term -> term) context_parser
    1.10  end;
    1.11  
    1.12  structure Term_Style: TERM_STYLE =
    1.13  struct
    1.14  
    1.15 -(* style data *)
    1.16 -
    1.17 -fun err_dup_style name =
    1.18 -  error ("Duplicate declaration of antiquote style: " ^ quote name);
    1.19 +(* theory data *)
    1.20  
    1.21 -structure Styles = Theory_Data
    1.22 +structure Data = Theory_Data
    1.23  (
    1.24 -  type T = ((Proof.context -> term -> term) parser * stamp) Symtab.table;
    1.25 -  val empty = Symtab.empty;
    1.26 +  type T = (Proof.context -> term -> term) parser Name_Space.table;
    1.27 +  val empty : T = Name_Space.empty_table "antiquotation_style";
    1.28    val extend = I;
    1.29 -  fun merge data : T = Symtab.merge (eq_snd (op =)) data
    1.30 -    handle Symtab.DUP dup => err_dup_style dup;
    1.31 +  fun merge data : T = Name_Space.merge_tables data;
    1.32  );
    1.33  
    1.34 -
    1.35 -(* accessors *)
    1.36 +val get_data = Data.get o Proof_Context.theory_of;
    1.37 +val get_style = Name_Space.get o get_data;
    1.38  
    1.39 -fun the_style thy name =
    1.40 -  (case Symtab.lookup (Styles.get thy) name of
    1.41 -    NONE => error ("Unknown antiquote style: " ^ quote name)
    1.42 -  | SOME (style, _) => style);
    1.43 -
    1.44 -fun setup name style thy =
    1.45 -  Styles.map (Symtab.update_new (name, (style, stamp ()))) thy
    1.46 -    handle Symtab.DUP _ => err_dup_style name;
    1.47 +fun setup binding style thy =
    1.48 +  Data.map (#2 o Name_Space.define (Context.Theory thy) true (binding, style)) thy;
    1.49  
    1.50  
    1.51  (* style parsing *)
    1.52  
    1.53 -fun parse_single ctxt = Parse.position Parse.xname -- Args.parse
    1.54 -  >> (fn ((name, pos), args) => fst (Args.context_syntax "style"
    1.55 -       (Scan.lift (the_style (Proof_Context.theory_of ctxt) name))
    1.56 -         (Args.src (name, pos) args) ctxt |>> (fn f => f ctxt)));
    1.57 +fun parse_single ctxt =
    1.58 +  Parse.position Parse.xname -- Args.parse >> (fn (name, args) =>
    1.59 +    let
    1.60 +      val (src, parse) = Args.check_src (Context.Proof ctxt) (get_data ctxt) (Args.src name args);
    1.61 +      val (f, _) = Args.context_syntax "antiquotation_style" (Scan.lift parse) src ctxt;
    1.62 +    in f ctxt end);
    1.63  
    1.64  val parse = Args.context :|-- (fn ctxt => Scan.lift
    1.65    (Args.parens (parse_single ctxt ::: Scan.repeat (Args.$$$ "," |-- parse_single ctxt))
    1.66 @@ -61,7 +53,7 @@
    1.67        Object_Logic.drop_judgment (Proof_Context.theory_of ctxt) (Logic.strip_imp_concl t)
    1.68    in
    1.69      (case concl of
    1.70 -      (_ $ l $ r) => proj (l, r)
    1.71 +      _ $ l $ r => proj (l, r)
    1.72      | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl))
    1.73    end);
    1.74  
    1.75 @@ -92,10 +84,10 @@
    1.76    | sub_term t = t;
    1.77  
    1.78  val _ = Theory.setup
    1.79 - (setup "lhs" (style_lhs_rhs fst) #>
    1.80 -  setup "rhs" (style_lhs_rhs snd) #>
    1.81 -  setup "prem" style_prem #>
    1.82 -  setup "concl" (Scan.succeed (K Logic.strip_imp_concl)) #>
    1.83 -  setup "sub" (Scan.succeed (K sub_term)));
    1.84 + (setup (Binding.name "lhs") (style_lhs_rhs fst) #>
    1.85 +  setup (Binding.name "rhs") (style_lhs_rhs snd) #>
    1.86 +  setup (Binding.name "prem") style_prem #>
    1.87 +  setup (Binding.name "concl") (Scan.succeed (K Logic.strip_imp_concl)) #>
    1.88 +  setup (Binding.name "sub") (Scan.succeed (K sub_term)));
    1.89  
    1.90  end;