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

Makarius makarius at sketis.net
Thu Aug 20 17:43:36 CEST 2015

*** 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 

The Poly/ML debugger interface is 
new, see also 

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

-------------- next part --------------
theory Debugger_Example
imports Pure

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

declare [[ML_debugger = true]]

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

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

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


More information about the isabelle-dev mailing list