Email Gateway (Aug 22 2022 at 21:04): Email Gateway (Aug 22 2022 at 21:04):From: Javier Castellano <javier.castellano.manzano@gmail.com>
Dear list,
I have two issues with related to ML programming in Isabelle.
In .thy files I can press ctrl and then click on the definition I'm
interested and the IDE brings me to the definition. I would like to do the
same for .ML files.
Currently, I do so by including the files that I need to browse with
command:
ML_file ‹...›
in some .thy file. Then the above procedure also works.
The second issue is about debugging. I found a reference to debugger
support on the IDE.
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2015-August/006238.html
However, I'm missing here a button called "Step into" that let me explore
the ML functions. In the link above, this functionality could be, "please
step into function writeln definition".
Let me know if there are way to do this.
Best,
Javier
Email Gateway (Aug 22 2022 at 21:04):From: Makarius <makarius@sketis.net>
On 02/12/2019 12:19, Javier Castellano wrote:
I have two issues with related to ML programming in Isabelle.
In .thy files I can press ctrl and then click on the definition I'm
interested and the IDE brings me to the definition. I would like to do the
same for .ML files.Currently, I do so by including the files that I need to browse with
command:ML_file ‹...›
in some .thy file. Then the above procedure also works.
Yes, everything needs to be formally included in a theory context. The
commands 'ML_file', 'ML' do that for you.
There are exceptions for ROOT.ML files: they get an implicit theory context by
other means.
The second issue is about debugging. I found a reference to debugger
support on the IDE.https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2015-August/006238.html
However, I'm missing here a button called "Step into" that let me explore
the ML functions. In the link above, this functionality could be, "please
step into function writeln definition".
The "jedit" manual chapter 5 (see Documentation panel) explains the debugger.
It works with some precautions, i.e. it requires some practice to avoid
conflicts of ongoing edits and running the program.
In practice, I often you use @{print} antiquotations in ML source to see what
happens at run time.
Makarius
Last updated: Apr 26 2024 at 20:16 UTC