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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
