59 |
59 |
60 |
60 |
61 *** Prover IDE -- Isabelle/Scala/jEdit *** |
61 *** Prover IDE -- Isabelle/Scala/jEdit *** |
62 |
62 |
63 * IDE support for the source-level debugger of Poly/ML, to work with |
63 * IDE support for the source-level debugger of Poly/ML, to work with |
64 Isabelle/ML and official Standard ML. Configuration option "ML_debugger" |
64 Isabelle/ML and official Standard ML. Option "ML_debugger" and commands |
65 and commands 'ML_file_debug', 'ML_file_no_debug', 'SML_file_debug', |
65 'ML_file_debug', 'ML_file_no_debug', 'SML_file_debug', |
66 'SML_file_no_debug' control compilation of sources with debugging |
66 'SML_file_no_debug' control compilation of sources with or without |
67 information. The Debugger panel allows to set breakpoints (via context |
67 debugging information. The Debugger panel allows to set breakpoints (via |
68 menu), step through stopped threads, evaluate local ML expressions etc. |
68 context menu), step through stopped threads, evaluate local ML |
69 At least one Debugger view needs to be active to have any effect on the |
69 expressions etc. At least one Debugger view needs to be active to have |
70 running ML program. |
70 any effect on the running ML program. |
71 |
71 |
72 * The State panel manages explicit proof state output, with dynamic |
72 * The State panel manages explicit proof state output, with dynamic |
73 auto-update according to cursor movement. Alternatively, the jEdit |
73 auto-update according to cursor movement. Alternatively, the jEdit |
74 action "isabelle.update-state" (shortcut S+ENTER) triggers manual |
74 action "isabelle.update-state" (shortcut S+ENTER) triggers manual |
75 update. |
75 update. |