equal
deleted
inserted
replaced
162 You can print out error messages with the function @{ML [index] error}; for example: |
162 You can print out error messages with the function @{ML [index] error}; for example: |
163 |
163 |
164 @{ML_response_fake [display,gray] "if 0=1 then true else (error \"foo\")" |
164 @{ML_response_fake [display,gray] "if 0=1 then true else (error \"foo\")" |
165 "Exception- ERROR \"foo\" raised |
165 "Exception- ERROR \"foo\" raised |
166 At command \"ML\"."} |
166 At command \"ML\"."} |
|
167 |
|
168 This function raises the exception @{text ERROR} which will then |
|
169 be displayed by the infrastructure. |
|
170 |
167 |
171 |
168 (FIXME Mention how to work with @{ML [index] debug in Toplevel} and |
172 (FIXME Mention how to work with @{ML [index] debug in Toplevel} and |
169 @{ML [index] profiling in Toplevel}.) |
173 @{ML [index] profiling in Toplevel}.) |
170 *} |
174 *} |
171 |
175 |
2255 |
2259 |
2256 section {* Misc (TBD) *} |
2260 section {* Misc (TBD) *} |
2257 |
2261 |
2258 ML {*Datatype.get_info @{theory} "List.list"*} |
2262 ML {*Datatype.get_info @{theory} "List.list"*} |
2259 |
2263 |
2260 section {* Name Space(TBD) *} |
2264 section {* Name Space Issues (TBD) *} |
2261 |
2265 |
2262 |
2266 |
2263 end |
2267 end |