[isabelle-dev] "local_setup" and "Generic_Data"

[Jasmin Blanchette]

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