154 helpful to navigate your way: ML is an interactive programming environment, |
154 helpful to navigate your way: ML is an interactive programming environment, |
155 which means you can evaluate code on the fly (for example inside an |
155 which means you can evaluate code on the fly (for example inside an |
156 \isacommand{ML}~@{text "\<verbopen>\<dots>\<verbclose>"} section). So you can copy |
156 \isacommand{ML}~@{text "\<verbopen>\<dots>\<verbclose>"} section). So you can copy |
157 (self-contained) chunks of existing code into a separate theory file and then |
157 (self-contained) chunks of existing code into a separate theory file and then |
158 study it alongside with examples. You can also install ``probes'' inside the |
158 study it alongside with examples. You can also install ``probes'' inside the |
159 copied code without having to recompile the whole Isabelle distributions. Such |
159 copied code without having to recompile the whole Isabelle distribution. Such |
160 probes might be messages or printouts of variables (see chapter |
160 probes might be messages or printouts of variables (see chapter |
161 \ref{chp:firststeps}). Although PolyML also contains a debugger, it seems |
161 \ref{chp:firststeps}). Although PolyML also contains a debugger, it seems |
162 probing the code with explicit print statements is the most effective method |
162 probing the code with explicit print statements is the most effective method |
163 for understanding what some piece of code is doing. However do not expect quick |
163 for understanding what some piece of code is doing. However do not expect quick |
164 results with this! Depending on the size of the code you are looking at, |
164 results with this! Depending on the size of the code you are looking at, |