[isabelle-dev] NEWS: IDE support for the source-level debugger of Poly/ML
makarius at sketis.net
Thu Aug 27 11:44:38 CEST 2015
On Thu, 27 Aug 2015, Florian Haftmann wrote:
>> *** Prover IDE -- Isabelle/Scala/jEdit ***
>> * IDE support for the source-level debugger of Poly/ML, to work with
>> Isabelle/ML and official Standard ML.
> That's a promising announcement.
> However I struggle to get something run from the attached example. I
> suspect that after placing the focus in the ML block something should be
> displayed in the debug panel, but there is no sign of anything.
The situation of the screenshot looks OK so far. Now you should activate
the "fun*loop" breakpoint via the context menu of jEdit -- it requires
some practice to get the mouse position right. Then you can scroll
further down to run some ML_val snippets, or produce dummy edits to ensure
they are run again after setting the breakpoint.
Afterwards the debugger panel should show the state of stopped threads.
More information about the isabelle-dev