Re: [isabelle] unexpected behaviour of user defined command in jedit



On Fri, 20 May 2011, Matthias Schmalz wrote:

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.

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

It looks more like the confusion is caused by an outdated version of the 'print_opt' command that inspects a different data slot. The parsing of commands is done "declaratively" in a way that makes it hard to foresee the exact operational behaviour. (The deeper problem is that old stateful concepts like the global command table are getting in the way.)

Anyway, definining and using a command within the same theory file was never supported in the history of Isabelle so far. Only last week, I've got an idea to solve this problem in the near future.

In classic Proof General there are certain ways to cope with this situation. In Isabelle/jEdit it is a bit more difficult, because the user has little control over the scheduling of command execution. One workaround is to define your commands beforehand and build an image in batch mode that is then used as starting point for the editor session.


	Makarius





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