155 error is raised. For printing anything more serious and elaborate, the |
155 error is raised. For printing anything more serious and elaborate, the |
156 function @{ML_ind tracing in Output} is more appropriate. This function writes all |
156 function @{ML_ind tracing in Output} is more appropriate. This function writes all |
157 output into a separate tracing buffer. For example: |
157 output into a separate tracing buffer. For example: |
158 |
158 |
159 @{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""} |
159 @{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""} |
160 |
|
161 It is also possible to redirect the ``channel'' where the string @{text |
|
162 "foo"} is printed to a separate file, e.g., in order to prevent ProofGeneral from |
|
163 choking on massive amounts of trace output. This redirection can be achieved |
|
164 with the code: |
|
165 *} |
|
166 |
|
167 ML{*val strip_specials = |
|
168 let |
|
169 fun strip ("\^A" :: _ :: cs) = strip cs |
|
170 | strip (c :: cs) = c :: strip cs |
|
171 | strip [] = []; |
|
172 in |
|
173 implode o strip o explode |
|
174 end |
|
175 |
|
176 fun redirect_tracing stream = |
|
177 Output.Private_Hooks.tracing_fn := (fn s => |
|
178 (TextIO.output (stream, (strip_specials s)); |
|
179 TextIO.output (stream, "\n"); |
|
180 TextIO.flushOut stream)) *} |
|
181 |
|
182 text {* |
|
183 Calling now |
|
184 |
|
185 @{ML [display,gray] "redirect_tracing (TextIO.openOut \"foo.bar\")"} |
|
186 |
|
187 will cause that all tracing information is printed into the file @{text "foo.bar"}. |
|
188 |
160 |
189 You can print out error messages with the function @{ML_ind error in Library}; for |
161 You can print out error messages with the function @{ML_ind error in Library}; for |
190 example: |
162 example: |
191 |
163 |
192 @{ML_response_fake [display,gray] |
164 @{ML_response_fake [display,gray] |
898 simpset. |
870 simpset. |
899 *} |
871 *} |
900 |
872 |
901 ML{*fun get_thm_names_from_ss simpset = |
873 ML{*fun get_thm_names_from_ss simpset = |
902 let |
874 let |
903 val {simps,...} = MetaSimplifier.dest_ss simpset |
875 val {simps,...} = Raw_Simplifier.dest_ss simpset |
904 in |
876 in |
905 map #1 simps |
877 map #1 simps |
906 end*} |
878 end*} |
907 |
879 |
908 text {* |
880 text {* |
909 The function @{ML_ind dest_ss in MetaSimplifier} returns a record containing all |
881 The function @{ML_ind dest_ss in Raw_Simplifier} returns a record containing all |
910 information stored in the simpset, but here we are only interested in the names of the |
882 information stored in the simpset, but here we are only interested in the names of the |
911 simp-rules. Now you can feed in the current simpset into this function. |
883 simp-rules. Now you can feed in the current simpset into this function. |
912 The current simpset can be referred to using the antiquotation @{text "@{simpset}"}. |
884 The current simpset can be referred to using the antiquotation @{text "@{simpset}"}. |
913 |
885 |
914 @{ML_response_fake [display,gray] |
886 @{ML_response_fake [display,gray] |