Re: [isabelle] Declaring global attributes



On Sun, 23 Oct 2011, John Munroe wrote:

Thanks. Can I try to imitate the setup_config_int function with:

ML {*
val (_,setup) = Attrib.config_int (@{binding "foo"} |> Binding.name_of) (K 2);
val _ = Context.>> (Context.map_theory setup)

val foo_raw = Config.declare_global "foo" (K (Config.Int 2));
val foo = Config.int foo_raw
*}
declare [[ foo = 3 ]]

But reading the attribute with

ML {*
val max_stuff_arty = Config.get_global @{theory} max_stuff_arity
*}

gives 2 rather than 3. Am I missing something here?

Yes, you have dropped the actual foo value representing the config option in ML, and defined a separate one that is not linked to the attribute name space at all. The name suffixes "_global" and "_raw" that you have seen in the Pure sources have been chosen to indicate that there is something unusual -- normal user-space code is neither global nor raw.

This is how it works:

ML {* val (foo, foo_setup) = Attrib.config_int "foo" (K 2) *}
setup foo_setup

declare [[ foo = 3 ]]
ML {* Config.get @{context } foo *}


See also section "1.1.5 Configuration options" of the fine Isabelle/Isar Implementation manual http://isabelle.in.tum.de/website-Isabelle2011/dist/Isabelle2011/doc/implementation.pdf
It even includes some examples of the above kind.


Anyway, are you really stuck with old Isabelle2011? Isabelle2011-1 has slightly better support for ML programming in the Isabelle/jEdit Prover IDE than Isabelle2011 from 8 months ago.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.