src/Pure/Tools/plugin.ML
changeset 58658 9002fe021e2f
parent 58657 c917dc025184
child 58660 8d4aebb9e327
     1.1 --- a/src/Pure/Tools/plugin.ML	Mon Oct 13 15:45:23 2014 +0200
     1.2 +++ b/src/Pure/Tools/plugin.ML	Mon Oct 13 17:04:25 2014 +0200
     1.3 @@ -10,8 +10,10 @@
     1.4  signature PLUGIN_NAME =
     1.5  sig
     1.6    val check: Proof.context -> xstring * Position.T -> string
     1.7 +  val define: binding -> string list -> theory -> string * theory
     1.8 +  val define_setup: binding -> string list -> string
     1.9    val declare: binding -> theory -> string * theory
    1.10 -  val setup: binding -> string
    1.11 +  val declare_setup: binding -> string
    1.12    type filter = string -> bool
    1.13    val parse_filter: (Proof.context -> filter) parser
    1.14    val make_filter: Proof.context -> (Proof.context -> filter) -> filter
    1.15 @@ -24,7 +26,7 @@
    1.16  
    1.17  structure Data = Theory_Data
    1.18  (
    1.19 -  type T = unit Name_Space.table;
    1.20 +  type T = string list Name_Space.table;
    1.21    val empty: T = Name_Space.empty_table "plugin";
    1.22    val extend = I;
    1.23    val merge = Name_Space.merge_tables;
    1.24 @@ -42,16 +44,27 @@
    1.25        >> (ML_Syntax.print_string o uncurry check)));
    1.26  
    1.27  
    1.28 -(* declare *)
    1.29 +(* indirections *)
    1.30  
    1.31 -fun declare binding thy =
    1.32 +fun resolve thy = maps (fn name =>
    1.33 +  (case Name_Space.get (Data.get thy) name of
    1.34 +    [] => [name]
    1.35 +  | names => resolve thy names));
    1.36 +
    1.37 +fun define binding rhs thy =
    1.38    let
    1.39      val context = Context.Theory thy |> Name_Space.map_naming (K Name_Space.default_naming);
    1.40 -    val (name, data') = Name_Space.define context true (binding, ()) (Data.get thy);
    1.41 +    val (name, data') = Name_Space.define context true (binding, resolve thy rhs) (Data.get thy);
    1.42      val thy' = Data.put data' thy;
    1.43    in (name, thy') end;
    1.44  
    1.45 -fun setup binding = Context.>>> (Context.map_theory_result (declare binding));
    1.46 +fun define_setup binding rhs = Context.>>> (Context.map_theory_result (define binding rhs));
    1.47 +
    1.48 +
    1.49 +(* immediate entries *)
    1.50 +
    1.51 +fun declare binding thy = define binding [] thy;
    1.52 +fun declare_setup binding = Context.>>> (Context.map_theory_result (declare binding));
    1.53  
    1.54  
    1.55  (* filter *)
    1.56 @@ -66,9 +79,10 @@
    1.57      (@{keyword ":"} |-- Scan.repeat (Parse.position Parse.name)) >>
    1.58        (fn (((_, pos1), (modif, pos2)), args) => fn ctxt =>
    1.59          let
    1.60 +          val thy = Proof_Context.theory_of ctxt;
    1.61            val _ = Context_Position.reports ctxt (map (rpair Markup.quasi_keyword) [pos1, pos2]);
    1.62 -          val names = map (check ctxt) args;
    1.63 -        in modif o member (op =) names end);
    1.64 +          val basic_names = resolve thy (map (check ctxt) args);
    1.65 +        in modif o member (op =) basic_names end);
    1.66  
    1.67  end;
    1.68