equal
deleted
inserted
replaced
46 Note that the parser @{ML "(Scan.lift Args.name)"} in line 9 parses a string, |
46 Note that the parser @{ML "(Scan.lift Args.name)"} in line 9 parses a string, |
47 in this case the code. This code is send to the ML-compiler in the line 4. |
47 in this case the code. This code is send to the ML-compiler in the line 4. |
48 If the code is ``approved'' by the compiler, then the output function @{ML |
48 If the code is ``approved'' by the compiler, then the output function @{ML |
49 "ThyOutput.output_list (fn _ => fn s => Pretty.str s)"} in the next line pretty prints the |
49 "ThyOutput.output_list (fn _ => fn s => Pretty.str s)"} in the next line pretty prints the |
50 code. This function expects that the code is a list of strings where each |
50 code. This function expects that the code is a list of strings where each |
51 string correspond to a line (therefore the @{ML_open "(space_explode \"\\n\" txt)" for txt} |
51 string correspond to a line (therefore the @{ML "(space_explode \"\\n\" txt)" for txt} |
52 which produces this list). There are a number of options for antiquotations |
52 which produces this list). There are a number of options for antiquotations |
53 that are observed by @{ML ThyOutput.output_list} when printing the code (for |
53 that are observed by @{ML ThyOutput.output_list} when printing the code (for |
54 example @{text "[display]"}, @{text "[quotes]"} and @{text "[source]"}). |
54 example @{text "[display]"}, @{text "[quotes]"} and @{text "[source]"}). |
55 |
55 |
56 \begin{readmore} |
56 \begin{readmore} |
144 |
144 |
145 @{ML_response [display] "let val i = 3 in (i * i,\"foo\") end" "(9,\<dots>)"} |
145 @{ML_response [display] "let val i = 3 in (i * i,\"foo\") end" "(9,\<dots>)"} |
146 |
146 |
147 In both cases, the check by the compiler ensures that code and result match. A limitation |
147 In both cases, the check by the compiler ensures that code and result match. A limitation |
148 of this antiquotation is that the hints can only be given for results that can actually |
148 of this antiquotation is that the hints can only be given for results that can actually |
149 be constructed as a pattern. This excludes values that are abstract types, like |
149 be constructed as a pattern. This excludes values that are abstract datatypes, like |
150 theorems or cterms. |
150 theorems or cterms. |
151 |
151 |
152 *} |
152 *} |
153 |
153 |
154 |
154 |