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

2015-08-27 Thread 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

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


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

2015-08-27 Thread Florian Haftmann
 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.

I see, this nice bullet appearing between »fun« and »loop«.  Awesome…

Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev