1 (* Title: Pure/ML/ml_compiler.ML |
1 (* Title: Pure/ML/ml_compiler.ML |
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 Runtime compilation -- generic version. |
4 Runtime compilation and evaluation -- generic version. |
5 *) |
5 *) |
6 |
6 |
7 signature ML_COMPILER = |
7 signature ML_COMPILER = |
8 sig |
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 val print_depth_raw: Config.raw |
|
15 val print_depth: int Config.T |
|
16 val get_print_depth: unit -> int |
|
17 type flags = {SML: bool, verbose: bool} |
9 type flags = {SML: bool, verbose: bool} |
18 val eval: flags -> Position.T -> ML_Lex.token list -> unit |
10 val eval: flags -> Position.T -> ML_Lex.token list -> unit |
19 end |
11 end |
20 |
12 |
21 structure ML_Compiler: ML_COMPILER = |
13 structure ML_Compiler: ML_COMPILER = |
22 struct |
14 struct |
23 |
|
24 (* exceptions *) |
|
25 |
|
26 val exn_info = |
|
27 {exn_position = fn _: exn => Position.none, |
|
28 pretty_exn = Pretty.str o General.exnMessage}; |
|
29 |
|
30 val exn_messages_ids = Runtime.exn_messages_ids exn_info; |
|
31 val exn_messages = Runtime.exn_messages exn_info; |
|
32 val exn_message = Runtime.exn_message exn_info; |
|
33 |
|
34 val exn_error_message = Output.error_message o exn_message; |
|
35 fun exn_trace e = print_exception_trace exn_message e; |
|
36 |
|
37 |
|
38 (* print depth *) |
|
39 |
|
40 val print_depth_raw = |
|
41 Config.declare "ML_print_depth" (fn _ => Config.Int (get_default_print_depth ())); |
|
42 val print_depth = Config.int print_depth_raw; |
|
43 |
|
44 fun get_print_depth () = |
|
45 (case Context.thread_data () of |
|
46 NONE => get_default_print_depth () |
|
47 | SOME context => Config.get_generic context print_depth); |
|
48 |
|
49 |
|
50 (* eval *) |
|
51 |
15 |
52 type flags = {SML: bool, verbose: bool}; |
16 type flags = {SML: bool, verbose: bool}; |
53 |
17 |
54 fun eval {SML, verbose} pos toks = |
18 fun eval {SML, verbose} pos toks = |
55 let |
19 let |