# HG changeset patch # User wenzelm # Date 1413212665 -7200 # Node ID 9002fe021e2f89b02254789cb97dfe655a07104c # Parent c917dc0251849bdebf6186ab3aeb5835480b8003 support for indirections (defined entries), e.g. relevant for quickcheck and its sub-plugins; diff -r c917dc025184 -r 9002fe021e2f src/Pure/Tools/plugin.ML --- a/src/Pure/Tools/plugin.ML Mon Oct 13 15:45:23 2014 +0200 +++ b/src/Pure/Tools/plugin.ML Mon Oct 13 17:04:25 2014 +0200 @@ -10,8 +10,10 @@ signature PLUGIN_NAME = sig val check: Proof.context -> xstring * Position.T -> string + val define: binding -> string list -> theory -> string * theory + val define_setup: binding -> string list -> string val declare: binding -> theory -> string * theory - val setup: binding -> string + val declare_setup: binding -> string type filter = string -> bool val parse_filter: (Proof.context -> filter) parser val make_filter: Proof.context -> (Proof.context -> filter) -> filter @@ -24,7 +26,7 @@ structure Data = Theory_Data ( - type T = unit Name_Space.table; + type T = string list Name_Space.table; val empty: T = Name_Space.empty_table "plugin"; val extend = I; val merge = Name_Space.merge_tables; @@ -42,16 +44,27 @@ >> (ML_Syntax.print_string o uncurry check))); -(* declare *) +(* indirections *) -fun declare binding thy = +fun resolve thy = maps (fn name => + (case Name_Space.get (Data.get thy) name of + [] => [name] + | names => resolve thy names)); + +fun define binding rhs thy = let val context = Context.Theory thy |> Name_Space.map_naming (K Name_Space.default_naming); - val (name, data') = Name_Space.define context true (binding, ()) (Data.get thy); + val (name, data') = Name_Space.define context true (binding, resolve thy rhs) (Data.get thy); val thy' = Data.put data' thy; in (name, thy') end; -fun setup binding = Context.>>> (Context.map_theory_result (declare binding)); +fun define_setup binding rhs = Context.>>> (Context.map_theory_result (define binding rhs)); + + +(* immediate entries *) + +fun declare binding thy = define binding [] thy; +fun declare_setup binding = Context.>>> (Context.map_theory_result (declare binding)); (* filter *) @@ -66,9 +79,10 @@ (@{keyword ":"} |-- Scan.repeat (Parse.position Parse.name)) >> (fn (((_, pos1), (modif, pos2)), args) => fn ctxt => let + val thy = Proof_Context.theory_of ctxt; val _ = Context_Position.reports ctxt (map (rpair Markup.quasi_keyword) [pos1, pos2]); - val names = map (check ctxt) args; - in modif o member (op =) names end); + val basic_names = resolve thy (map (check ctxt) args); + in modif o member (op =) basic_names end); end;