src/Pure/ML/ml_compiler.ML
author wenzelm
Thu Aug 02 12:36:54 2012 +0200 (2012-08-02)
changeset 48646 91281e9472d8
parent 44270 3eaad39e520c
child 50914 fe4714886d92
permissions -rw-r--r--
more official command specifications, including source position;
     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: exn -> (serial * string) list
    11   val exn_message: exn -> string
    12   val eval: bool -> Position.T -> ML_Lex.token list -> unit
    13 end
    14 
    15 structure ML_Compiler: ML_COMPILER =
    16 struct
    17 
    18 fun exn_position _ = Position.none;
    19 val exn_messages = Runtime.exn_messages exn_position;
    20 val exn_message = Runtime.exn_message exn_position;
    21 
    22 fun eval verbose pos toks =
    23   let
    24     val line = the_default 1 (Position.line_of pos);
    25     val file = the_default "ML" (Position.file_of pos);
    26     val text = ML_Lex.flatten toks;
    27   in Secure.use_text ML_Env.local_context (line, file) verbose text end;
    28 
    29 end;
    30