src/Pure/ML/ml_compiler.ML
author wenzelm
Tue Mar 25 13:18:10 2014 +0100 (2014-03-25 ago)
changeset 56275 600f432ab556
parent 54387 890e983cb07b
child 56281 03c3d1a7c3b8
permissions -rw-r--r--
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
     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_messages_ids: exn -> Runtime.error list
    10   val exn_messages: exn -> (serial * string) list
    11   val exn_message: exn -> string
    12   val exn_error_message: exn -> unit
    13   val exn_trace: (unit -> 'a) -> 'a
    14   type flags = {SML: bool, verbose: bool}
    15   val eval: flags -> Position.T -> ML_Lex.token list -> unit
    16 end
    17 
    18 structure ML_Compiler: ML_COMPILER =
    19 struct
    20 
    21 val exn_info =
    22  {exn_position = fn _: exn => Position.none,
    23   pretty_exn = Pretty.str o General.exnMessage};
    24 
    25 val exn_messages_ids = Runtime.exn_messages_ids exn_info;
    26 val exn_messages = Runtime.exn_messages exn_info;
    27 val exn_message = Runtime.exn_message exn_info;
    28 
    29 val exn_error_message = Output.error_message o exn_message;
    30 fun exn_trace e = print_exception_trace exn_message e;
    31 
    32 type flags = {SML: bool, verbose: bool};
    33 
    34 fun eval {SML, verbose} pos toks =
    35   let
    36     val _ = if SML then error ("Standard ML is unsupported on " ^ ML_System.name) else ();
    37     val line = the_default 1 (Position.line_of pos);
    38     val file = the_default "ML" (Position.file_of pos);
    39     val text = ML_Lex.flatten toks;
    40   in Secure.use_text ML_Env.local_context (line, file) verbose text end;
    41 
    42 end;
    43