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