src/Pure/ML/ml_compiler.ML
author wenzelm
Mon Apr 08 17:10:49 2013 +0200 (2013-04-08 ago)
changeset 51639 b7f908c99546
parent 51285 0859bd338c9b
child 53709 84522727f9d3
permissions -rw-r--r--
prefer pretty_exn where possible -- NB: low-level General.exnMessage may still be used elsewhere (e.g. by the ML compiler itself);
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@31333
    12
  val eval: bool -> Position.T -> ML_Lex.token list -> unit
wenzelm@31333
    13
end
wenzelm@31333
    14
wenzelm@31333
    15
structure ML_Compiler: ML_COMPILER =
wenzelm@31333
    16
struct
wenzelm@31333
    17
wenzelm@51639
    18
val exn_info =
wenzelm@51639
    19
 {exn_position = fn _: exn => Position.none,
wenzelm@51639
    20
  pretty_exn = Pretty.str o General.exnMessage};
wenzelm@51639
    21
wenzelm@51639
    22
val exn_messages_ids = Runtime.exn_messages_ids exn_info;
wenzelm@51639
    23
val exn_messages = Runtime.exn_messages exn_info;
wenzelm@51639
    24
val exn_message = Runtime.exn_message exn_info;
wenzelm@31428
    25
wenzelm@31333
    26
fun eval verbose pos toks =
wenzelm@31333
    27
  let
wenzelm@31333
    28
    val line = the_default 1 (Position.line_of pos);
wenzelm@31333
    29
    val file = the_default "ML" (Position.file_of pos);
wenzelm@31333
    30
    val text = ML_Lex.flatten toks;
wenzelm@31333
    31
  in Secure.use_text ML_Env.local_context (line, file) verbose text end;
wenzelm@31333
    32
wenzelm@31333
    33
end;
wenzelm@31333
    34