diff -r 0bcd598d2587 -r 620a24bf954a ProgTutorial/Intro.thy --- a/ProgTutorial/Intro.thy Wed Apr 07 11:32:00 2010 +0200 +++ b/ProgTutorial/Intro.thy Sat Apr 24 22:55:50 2010 +0200 @@ -145,6 +145,28 @@ to solve the exercises on your own, and then look at the solutions. *} +section {* How To Understand Code in Isabelle *} + +text {* + One of the more difficult aspects of programming is to understand somebody + else's code. This is aggravated in Isabelle by the fact that many parts of + the code contain only few comments. There is one strategy that might be + helpful to navigate your way: ML is an interactive programming environment, + which means you can evaluate code on the fly (for example inside an + \isacommand{ML}~@{text "\\\"} section). So you can copy + self-contained chunks of existing code into a separate theory file and then + study it alongside with examples. You can also install probes inside the + copied code without having to recompile the whole Isabelle distributions. Such + probes might be messages or printouts of variables (see chapter + \ref{chp:firststeps}). Although PolyML also contains a debugger, it seems + probing the code with explicit print statements is the most efficient method + for understanding what some code is doing. However do not expect quick + results with this! Depending on the size of the code you are looking at, + you will spend the better part of a quiet afternoon with it. But there + seems to be no better way around it. +*} + + section {* Aaaaargh! My Code Does not Work Anymore *} text {* @@ -248,7 +270,10 @@ Please let me know of any omissions. Responsibility for any remaining errors lies with me.\bigskip - \vspace{5cm} + \newpage + \mbox{}\\[5cm] + + {\Large\bf This tutorial is still in the process of being written! All of the text is still under construction. Sections and