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;
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@51285
     9
  val exn_messages_ids: exn -> Runtime.error list
wenzelm@44270
    10
  val exn_messages: exn -> (serial * string) list
wenzelm@31477
    11
  val exn_message: exn -> string
wenzelm@54387
    12
  val exn_error_message: exn -> unit
wenzelm@53709
    13
  val exn_trace: (unit -> 'a) -> 'a
wenzelm@56275
    14
  type flags = {SML: bool, verbose: bool}
wenzelm@56275
    15
  val eval: flags -> Position.T -> ML_Lex.token list -> unit
wenzelm@31333
    16
end
wenzelm@31333
    17
wenzelm@31333
    18
structure ML_Compiler: ML_COMPILER =
wenzelm@31333
    19
struct
wenzelm@31333
    20
wenzelm@51639
    21
val exn_info =
wenzelm@51639
    22
 {exn_position = fn _: exn => Position.none,
wenzelm@51639
    23
  pretty_exn = Pretty.str o General.exnMessage};
wenzelm@51639
    24
wenzelm@51639
    25
val exn_messages_ids = Runtime.exn_messages_ids exn_info;
wenzelm@51639
    26
val exn_messages = Runtime.exn_messages exn_info;
wenzelm@51639
    27
val exn_message = Runtime.exn_message exn_info;
wenzelm@54387
    28
wenzelm@54387
    29
val exn_error_message = Output.error_message o exn_message;
wenzelm@53709
    30
fun exn_trace e = print_exception_trace exn_message e;
wenzelm@31428
    31
wenzelm@56275
    32
type flags = {SML: bool, verbose: bool};
wenzelm@56275
    33
wenzelm@56275
    34
fun eval {SML, verbose} pos toks =
wenzelm@31333
    35
  let
wenzelm@56275
    36
    val _ = if SML then error ("Standard ML is unsupported on " ^ ML_System.name) else ();
wenzelm@31333
    37
    val line = the_default 1 (Position.line_of pos);
wenzelm@31333
    38
    val file = the_default "ML" (Position.file_of pos);
wenzelm@31333
    39
    val text = ML_Lex.flatten toks;
wenzelm@31333
    40
  in Secure.use_text ML_Env.local_context (line, file) verbose text end;
wenzelm@31333
    41
wenzelm@31333
    42
end;
wenzelm@31333
    43