Hi all,
I was trying to make Nitpick more context-friendly and thought that
"local_setup" and "Generic_Data" would be my friends. However, "local_setup"
seems to do nothing -- the changes I perform to the data are coldly ignored.
The little theory below shows illustrates what I mean:
theory Scratch
imports Main
begin
ML {*
structure Data = Generic_Data(
type T = int
val empty = 0
val extend = I
val merge = Int.max)
*}
setup {* Context.theory_map (Data.map (Integer.add 1)) *}
ML {* Data.get (Context.Theory @{theory}) *} (* OK: returns 1 *)
locale x =
fixes R :: 'a
begin
local_setup {* Context.proof_map (Data.map (Integer.add 3)) *}
ML {* Data.get (Context.Theory @{theory}) *} (* OK: returns 1 *)
ML {* Data.get (Context.Proof @{context}) *} (* Not OK: returns 1, expected 4
*)
end
end
I reproduced this behavior with both Isabelle2009-1 (where "local_setup" was
introduced) and a recent repository version.
Does anybody knows what's going on?
Thanks,
Jasmin
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
