src/Pure/ML/ml_compiler.ML
author wenzelm
Mon Jun 01 23:28:06 2009 +0200 (2009-06-01)
changeset 31333 fcd010617e6c
child 31428 3b32a57b044b
permissions -rw-r--r--
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
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@31333
     9
  val eval: bool -> Position.T -> ML_Lex.token list -> unit
wenzelm@31333
    10
end
wenzelm@31333
    11
wenzelm@31333
    12
structure ML_Compiler: ML_COMPILER =
wenzelm@31333
    13
struct
wenzelm@31333
    14
wenzelm@31333
    15
fun eval verbose pos toks =
wenzelm@31333
    16
  let
wenzelm@31333
    17
    val line = the_default 1 (Position.line_of pos);
wenzelm@31333
    18
    val file = the_default "ML" (Position.file_of pos);
wenzelm@31333
    19
    val text = ML_Lex.flatten toks;
wenzelm@31333
    20
  in Secure.use_text ML_Env.local_context (line, file) verbose text end;
wenzelm@31333
    21
wenzelm@31333
    22
end;
wenzelm@31333
    23