[isabelle] unexpected behaviour of user defined command in jedit



Hi,

I have defined a configuration option "opt" and a command "print_opt" that prints the value of "opt". In jedit print_opt sometimes prints an outdated value of "opt". I would like to know whether it is my fault, or rather a limitation of jedit, and how I can achieve the desired behaviour.

Thank you very much,

Matthias

theory config_option imports Main begin

ML {*
val (opt, opt_setup) =
  Attrib.config_string "opt" (K "initial")
val _ = (Context.>> o Context.map_theory) opt_setup
fun opt_of ctxt = Config.get ctxt opt

val _ = Outer_Syntax.command
  "print_opt"
  "print opt"
  Keyword.diag
  (Scan.succeed (Toplevel.keep (Toplevel.context_of #> opt_of #> writeln)))
*}

print_opt (* "initial", as expected *)

declare[[opt="updated"]]

print_configs (* opt="updated", as expected *)

print_opt (* "initial" after reloading file, "updated" after retyping "print_opt" *)

end





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