src/Pure/ML/ml_compiler.ML
author wenzelm
Tue Feb 26 19:58:27 2013 +0100 (2013-02-26 ago)
changeset 51285 0859bd338c9b
parent 50914 fe4714886d92
child 51639 b7f908c99546
permissions -rw-r--r--
tuned signature;
     1 (*  Title:      Pure/ML/ml_compiler.ML
     2     Author:     Makarius
     3 
     4 Runtime compilation -- generic version.
     5 *)
     6 
     7 signature ML_COMPILER =
     8 sig
     9   val exn_position: exn -> Position.T
    10   val exn_messages_ids: exn -> Runtime.error list
    11   val exn_messages: exn -> (serial * string) list
    12   val exn_message: exn -> string
    13   val eval: bool -> Position.T -> ML_Lex.token list -> unit
    14 end
    15 
    16 structure ML_Compiler: ML_COMPILER =
    17 struct
    18 
    19 fun exn_position _ = Position.none;
    20 val exn_messages_ids = Runtime.exn_messages_ids exn_position;
    21 val exn_messages = Runtime.exn_messages exn_position;
    22 val exn_message = Runtime.exn_message exn_position;
    23 
    24 fun eval verbose pos toks =
    25   let
    26     val line = the_default 1 (Position.line_of pos);
    27     val file = the_default "ML" (Position.file_of pos);
    28     val text = ML_Lex.flatten toks;
    29   in Secure.use_text ML_Env.local_context (line, file) verbose text end;
    30 
    31 end;
    32