Email Gateway (Aug 18 2022 at 17:43): Email Gateway (Aug 18 2022 at 17:43):From: Matthias Schmalz <Matthias.Schmalz@inf.ethz.ch>
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
Email Gateway (Aug 18 2022 at 17:44):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 18 2022 at 17:44):From: Matthias Schmalz <Matthias.Schmalz@inf.ethz.ch>
This is no problem -- I anyway wanted to provide my commands by a
precompiled image.
Thanks for your help,
Matthias
Last updated: Apr 19 2024 at 20:15 UTC