src/Pure/ML/ml_compiler.ML
changeset 31333 fcd010617e6c
child 31428 3b32a57b044b
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/ML/ml_compiler.ML	Mon Jun 01 23:28:06 2009 +0200
     1.3 @@ -0,0 +1,23 @@
     1.4 +(*  Title:      Pure/ML/ml_compiler.ML
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Runtime compilation -- generic version.
     1.8 +*)
     1.9 +
    1.10 +signature ML_COMPILER =
    1.11 +sig
    1.12 +  val eval: bool -> Position.T -> ML_Lex.token list -> unit
    1.13 +end
    1.14 +
    1.15 +structure ML_Compiler: ML_COMPILER =
    1.16 +struct
    1.17 +
    1.18 +fun eval verbose pos toks =
    1.19 +  let
    1.20 +    val line = the_default 1 (Position.line_of pos);
    1.21 +    val file = the_default "ML" (Position.file_of pos);
    1.22 +    val text = ML_Lex.flatten toks;
    1.23 +  in Secure.use_text ML_Env.local_context (line, file) verbose text end;
    1.24 +
    1.25 +end;
    1.26 +