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

[Makarius]

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.


 	Makarius