[isabelle] Behavior of configuration options in local theories



Dear all,

I was surprised by the fact that configuration options seem to be reset when closing a local target:

ML â
val foo = Attrib.setup_config_int @{binding foo} (K 6);
â

local_setup âfn lthy =>
  let
    val _ = Config.get lthy foo |> @{print}
    val _ = Config.get (Config.put foo 7 lthy) foo |> @{print}
    val _ = Config.get (Config.put foo 7 lthy |> Local_Theory.open_target |> snd) foo |> @{print}
    val _ = Config.get (Config.put foo 7 lthy |> Local_Theory.open_target |> snd |> Local_Theory.close_target) foo |> @{print}
  in
    lthy
  end
â

This prints
6
7
7
6.

I had expected the last one to be 7 as well. Is there a way to make the changes to configuration options persistent in this respect?

Thanks for any hints,
Dmitriy



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