author | wenzelm |
Thu Aug 18 17:53:32 2011 +0200 (2011-08-18 ago) | |
changeset 44270 | 3eaad39e520c |
parent 38874 | 4a4d34d2f97b |
child 50914 | fe4714886d92 |
permissions | -rw-r--r-- |
wenzelm@31333 | 1 |
(* Title: Pure/ML/ml_compiler.ML |
wenzelm@31333 | 2 |
Author: Makarius |
wenzelm@31333 | 3 |
|
wenzelm@31333 | 4 |
Runtime compilation -- generic version. |
wenzelm@31333 | 5 |
*) |
wenzelm@31333 | 6 |
|
wenzelm@31333 | 7 |
signature ML_COMPILER = |
wenzelm@31333 | 8 |
sig |
wenzelm@31477 | 9 |
val exn_position: exn -> Position.T |
wenzelm@44270 | 10 |
val exn_messages: exn -> (serial * string) list |
wenzelm@31477 | 11 |
val exn_message: exn -> string |
wenzelm@31333 | 12 |
val eval: bool -> Position.T -> ML_Lex.token list -> unit |
wenzelm@31333 | 13 |
end |
wenzelm@31333 | 14 |
|
wenzelm@31333 | 15 |
structure ML_Compiler: ML_COMPILER = |
wenzelm@31333 | 16 |
struct |
wenzelm@31333 | 17 |
|
wenzelm@31477 | 18 |
fun exn_position _ = Position.none; |
wenzelm@38874 | 19 |
val exn_messages = Runtime.exn_messages exn_position; |
wenzelm@31477 | 20 |
val exn_message = Runtime.exn_message exn_position; |
wenzelm@31428 | 21 |
|
wenzelm@31333 | 22 |
fun eval verbose pos toks = |
wenzelm@31333 | 23 |
let |
wenzelm@31333 | 24 |
val line = the_default 1 (Position.line_of pos); |
wenzelm@31333 | 25 |
val file = the_default "ML" (Position.file_of pos); |
wenzelm@31333 | 26 |
val text = ML_Lex.flatten toks; |
wenzelm@31333 | 27 |
in Secure.use_text ML_Env.local_context (line, file) verbose text end; |
wenzelm@31333 | 28 |
|
wenzelm@31333 | 29 |
end; |
wenzelm@31333 | 30 |