62 |
66 |
63 text {* |
67 text {* |
64 then Isabelle's undo operation has no effect on the definition of |
68 then Isabelle's undo operation has no effect on the definition of |
65 @{ML "foo"}. |
69 @{ML "foo"}. |
66 |
70 |
67 (FIXME: add comment about including whole ML-files) |
71 Once a portion of code is relatively stable, one usually wants to |
|
72 export it to a separate ML-file. Such files can be included in a |
|
73 theory using @{ML_text "uses"} in the header of the theory. |
|
74 |
|
75 \begin{center} |
|
76 \begin{tabular}{@ {}l} |
|
77 \isacommand{theory} CookBook\\ |
|
78 \isacommand{imports} Main\\ |
|
79 \isacommand{uses} @{text "\"file_to_be_included.ML\""}\\ |
|
80 \isacommand{begin}\\ |
|
81 \ldots |
|
82 \end{tabular} |
|
83 \end{center} |
|
84 *} |
|
85 |
|
86 section {* Debugging and Printing *} |
|
87 |
|
88 text {* |
68 |
89 |
69 During developments you might find it necessary to quickly inspect some data |
90 During developments you might find it necessary to quickly inspect some data |
70 in your code. This can be done in a ``quick-and-dirty'' fashion using |
91 in your code. This can be done in a ``quick-and-dirty'' fashion using |
71 the function @{ML "warning"}. For example |
92 the function @{ML "warning"}. For example |
72 *} |
93 *} |
73 |
94 |
74 ML {* |
95 ML {* warning "any string" *} |
75 val _ = warning "any string" |
|
76 *} |
|
77 |
96 |
78 text {* |
97 text {* |
79 will print out @{ML "\"any string\""} inside the response buffer of Isabelle. |
98 will print out @{ML "\"any string\""} inside the response buffer of Isabelle. |
80 PolyML provides a convenient, though again ``quick-and-dirty'', method for |
99 PolyML provides a convenient, though again ``quick-and-dirty'', method for |
81 converting arbitrary values into strings, for example: |
100 converting arbitrary values into strings, for example: |
82 *} |
101 *} |
83 |
102 |
84 ML {* |
103 ML {* warning (makestring 1) *} |
85 val _ = warning (makestring 1) |
|
86 *} |
|
87 |
104 |
88 text {* |
105 text {* |
89 However this only works if the type of what is printed is monomorphic and not |
106 However this only works if the type of what is printed is monomorphic and not |
90 a function. |
107 a function. |
91 *} |
108 *} |
92 |
109 |
93 text {* (FIXME: add here or in the appendix a comment about tracing) *} |
110 text {* |
94 text {* (FIXME: maybe a comment about redirecting the trace information) *} |
111 The funtion warning should only be used for testing purposes, because |
|
112 the problem with this function is that any output will be |
|
113 overwritten if an error is raised. For anything more serious |
|
114 the function @{ML tracing}, which writes all output in a separate |
|
115 buffer, should be used. |
|
116 |
|
117 *} |
|
118 |
|
119 ML {* tracing "foo" *} |
|
120 |
|
121 text {* (FIXME: complete the comment about redirecting the trace information) |
|
122 |
|
123 In Isabelle it is possible to redirect the message channels to a |
|
124 separate file, e.g. to prevent Proof General from choking on massive |
|
125 amounts of trace output. |
|
126 |
|
127 *} |
|
128 |
|
129 ML {* |
|
130 val strip_specials = |
|
131 let |
|
132 fun strip ("\^A" :: _ :: cs) = strip cs |
|
133 | strip (c :: cs) = c :: strip cs |
|
134 | strip [] = []; |
|
135 in implode o strip o explode end; |
|
136 |
|
137 fun redirect_tracing stream = |
|
138 Output.tracing_fn := (fn s => |
|
139 (TextIO.output (stream, (strip_specials s)); |
|
140 TextIO.output (stream, "\n"); |
|
141 TextIO.flushOut stream)); |
|
142 *} |
|
143 |
95 |
144 |
96 section {* Antiquotations *} |
145 section {* Antiquotations *} |
97 |
146 |
98 text {* |
147 text {* |
99 The main advantage of embedding all code |
148 The main advantage of embedding all code |