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

[Makarius]

*** Prover IDE -- Isabelle/Scala/jEdit ***

* IDE support for the source-level debugger of Poly/ML, to work with 
Isabelle/ML and official Standard ML. Configuration option "ML_debugger" 
and commands 'ML_file_debug', 'ML_file_no_debug', 'SML_file_debug', 
'SML_file_no_debug' control compilation of sources with debugging 
information. The Debugger panel allows to set breakpoints (via context 
menu), step through stopped threads, evaluate local ML expressions etc. At 
least one Debugger view needs to be active to have any effect on the 
running ML program.

This refers to Isabelle/077f663b6c24. A small example is included as 
attachment.

The Poly/ML debugger interface is 
new, see also 
http://www.polyml.org/documentation/Reference/PolyMLDebuggerInterface.html

We have now the opportunity to test all that thoroughly, before David 
Matthews can roll out a proper release.


 	Makarius
-------------- next part --------------
theory Debugger_Example
imports Pure
begin

section \<open>Minimal example\<close>

text \<open>
  \<bullet> Ensure that the Debugger panel is open

  \<bullet> Right-click on the "fun\<bullet>loop" breakpoint and enable it via context menu item
    "Toggle Breakpoint".

  \<bullet> Edit some spaces in lemma statement to re-check ML_val invocations below,
    and run into the debugger.

  \<bullet> Step through the ML source, using Debugger controls, depending on thread
    context.
\<close>

declare [[ML_debugger = true]]

ML \<open>
  fun print n s = writeln (string_of_int n ^ " " ^ s);

  fun loop n =
    if n <= 0 then n
    else
      let
        val _ = print n "a";
        val m = loop (n - 1);
        val _ = print (m + 1) "b";
      in n end;
\<close>

ML_val \<open>loop 10\<close>
ML_val \<open>loop 10\<close>
ML_val \<open>loop 10\<close>

end