126 (*call the compiler and pass resulting type string to the parser*) |
126 (*call the compiler and pass resulting type string to the parser*) |
127 fun determine_type ctxt s = |
127 fun determine_type ctxt s = |
128 let |
128 let |
129 val return = Unsynchronized.ref "return" |
129 val return = Unsynchronized.ref "return" |
130 val context : ML_Compiler0.context = |
130 val context : ML_Compiler0.context = |
131 {name_space = #name_space ML_Env.local_context, |
131 {name_space = #name_space ML_Env.context, |
132 here = #here ML_Env.local_context, |
132 here = #here ML_Env.context, |
133 print = fn r => return := r, |
133 print = fn r => return := r, |
134 error = #error ML_Env.local_context} |
134 error = #error ML_Env.context} |
135 val _ = |
135 val _ = |
136 Context.setmp_thread_data (SOME (Context.Proof ctxt)) |
136 Context.setmp_thread_data (SOME (Context.Proof ctxt)) |
137 (fn () => |
137 (fn () => |
138 ML_Compiler0.use_text context |
138 ML_Compiler0.use_text context |
139 {line = 0, file = "generated code", verbose = true, debug = false} s) () |
139 {line = 0, file = "generated code", verbose = true, debug = false} s) () |
143 |
143 |
144 (*call the compiler and run the test*) |
144 (*call the compiler and run the test*) |
145 fun run_test ctxt s = |
145 fun run_test ctxt s = |
146 Context.setmp_thread_data (SOME (Context.Proof ctxt)) |
146 Context.setmp_thread_data (SOME (Context.Proof ctxt)) |
147 (fn () => |
147 (fn () => |
148 ML_Compiler0.use_text ML_Env.local_context |
148 ML_Compiler0.use_text ML_Env.context |
149 {line = 0, file = "generated code", verbose = false, debug = false} s) (); |
149 {line = 0, file = "generated code", verbose = false, debug = false} s) (); |
150 |
150 |
151 (*split input into tokens*) |
151 (*split input into tokens*) |
152 fun input_split s = |
152 fun input_split s = |
153 let |
153 let |