Ant S. (Apr 29 2026 at 10:05): Ant S. (Apr 29 2026 at 10:05):I have sifting through implementation.pdf, section 1.15 and isar-ref.pdf to figure out how to write out the value of a configuration parameter (e.g. declare [[ smt_timeout = 0 ]] ) how do I print the value of smt_timeout?
Would it be something on the lines of ML <Config.get context smt_timeout>? That doesn't seem to be syntactically correct
Ant S. (Apr 29 2026 at 10:10):Is the only way to do this print_options?
Lukas Stevens (Apr 29 2026 at 12:23):This works ML ‹Config.get @{context} SMT_Config.timeout›
Ant S. (Apr 29 2026 at 12:23):Thank you! How should I have figured it out?
Ant S. (Apr 29 2026 at 12:23):from the manual
Lukas Stevens (Apr 29 2026 at 12:24):You can Ctrl-click on smt_timeout to find out the corresponding ML constant. @{context} is the usual way to get hold of the context at that position in ML.
Ant S. (Apr 29 2026 at 12:25):attribute "SMT.smt_timeout"
It doesn't say SMT_Config though
Ant S. (Apr 29 2026 at 12:57):Ant S. said:
attribute "SMT.smt_timeout"
to clarify this is what I get when CTRL-hovering/clicking
Ant S. (Apr 29 2026 at 12:58):is it based on the ML file name (SMT_Config.ml)
Lukas Stevens (Apr 29 2026 at 13:18):If you look at the file, you see that the result of the declaration of the config attribute is assigned to timeout. Since timeout is part of the module SMT_Config, you can refer to this config option as SMT_Config.timeout.
Ant S. (Apr 29 2026 at 13:24):structure SMT_Config: SMT_CONFIG
ah, so this line. Is there some way to get a "bird's eye view" of the file/module structure in jEdit? Sort of like what Ctrl-hovering does in Isar or just hovering over a variable does in VSCode for most languages. Ctrl-click/hover doesn't seem to do much in ML
Is there some jEdit plugin that does this? I found https://github.com/polyml/jedit-plugin but it seems outdated...
Mathias Fleury (Apr 29 2026 at 16:41):the sidekick works to get some idea of the structure
Mathias Fleury (Apr 29 2026 at 16:41):but there is no way to show documentation of a variable
Mathias Fleury (Apr 29 2026 at 16:41):because there is none
Mathias Fleury (Apr 29 2026 at 16:42):Some people have the opinion that no documentation is better than a misleading one
Jonathan Julian Huerta y Munive (Apr 29 2026 at 23:03):Ant S. said:
Is there some way to get a "bird's eye view" of the file/module structure in jEdit? Sort of like what Ctrl-hovering does in Isar or just hovering over a variable does in VSCode for most languages.
I am not sure I am understanding what you want, but, if you (1) open your ISABELLE_HOME/src/HOL/SMT.thy in jEdit, (2) load it to the end of the file, and then (3) open the smt_config.ML in jEdit, you will be able to ctrl-hover some things in that file and get, e.g. some typing information.
Last updated: May 05 2026 at 02:56 UTC