134 print = fn r => return := r, |
134 print = fn r => return := r, |
135 error = #error ML_Env.context} |
135 error = #error ML_Env.context} |
136 val _ = |
136 val _ = |
137 Context.setmp_generic_context (SOME (Context.Proof ctxt)) |
137 Context.setmp_generic_context (SOME (Context.Proof ctxt)) |
138 (fn () => |
138 (fn () => |
139 ML_Compiler0.use_text context |
139 ML_Compiler0.ML context |
140 {line = 0, file = "generated code", verbose = true, debug = false} s) () |
140 {line = 0, file = "generated code", verbose = true, debug = false} s) () |
141 in |
141 in |
142 Gen_Construction.parse_pred (! return) |
142 Gen_Construction.parse_pred (! return) |
143 end; |
143 end; |
144 |
144 |
145 (*call the compiler and run the test*) |
145 (*call the compiler and run the test*) |
146 fun run_test ctxt s = |
146 fun run_test ctxt s = |
147 Context.setmp_generic_context (SOME (Context.Proof ctxt)) |
147 Context.setmp_generic_context (SOME (Context.Proof ctxt)) |
148 (fn () => |
148 (fn () => |
149 ML_Compiler0.use_text ML_Env.context |
149 ML_Compiler0.ML ML_Env.context |
150 {line = 0, file = "generated code", verbose = false, debug = false} s) (); |
150 {line = 0, file = "generated code", verbose = false, debug = false} s) (); |
151 |
151 |
152 (*split input into tokens*) |
152 (*split input into tokens*) |
153 fun input_split s = |
153 fun input_split s = |
154 let |
154 let |