[isabelle-dev] NEWS: IDE support for the source-level debugger of Poly/ML

Makarius 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 mailing list