clarified ML compiler parameters: always provide PolyML.Compiler.CPDebug, ignore global default;
tuned;
(* Title: Pure/ML/ml_compiler_polyml.ML
Author: Makarius
Runtime compilation and evaluation -- Poly/ML version.
*)
structure ML_Compiler: ML_COMPILER =
struct
open ML_Compiler;
(* parse trees *)
fun report_parse_tree redirect depth space parse_tree =
let
val is_visible =
(case Context.thread_data () of
SOME context => Context_Position.is_visible_generic context
| NONE => true);
fun is_reported pos = is_visible andalso Position.is_reported pos;
(* syntax reports *)
fun reported_types loc types =
let val pos = Exn_Properties.position_of loc in
is_reported pos ?
let
val xml =
PolyML.NameSpace.displayTypeExpression (types, depth, space)
|> pretty_ml |> Pretty.from_ML |> Pretty.string_of
|> Output.output |> YXML.parse_body;
in cons (pos, fn () => Markup.ML_typing, fn () => YXML.string_of_body xml) end
end;
fun reported_entity kind loc decl =
let
val pos = Exn_Properties.position_of loc;
val def_pos = Exn_Properties.position_of decl;
in
(is_reported pos andalso pos <> def_pos) ?
let
fun markup () =
(Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of def_pos);
in cons (pos, markup, fn () => "") end
end;
fun reported_completions loc names =
let val pos = Exn_Properties.position_of loc in
if is_reported pos andalso not (null names) then
let
val completion = Completion.names pos (map (fn a => (a, ("ML", a))) names);
val xml = Completion.encode completion;
in cons (pos, fn () => Markup.completion, fn () => YXML.string_of_body xml) end
else I
end;
fun reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
| reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
| reported loc (PolyML.PTtype types) = reported_types loc types
| reported loc (PolyML.PTdeclaredAt decl) = reported_entity Markup.ML_defN loc decl
| reported loc (PolyML.PTopenedAt decl) = reported_entity Markup.ML_openN loc decl
| reported loc (PolyML.PTstructureAt decl) = reported_entity Markup.ML_structureN loc decl
| reported loc pt =
(case ML_Parse_Tree.completions pt of
SOME names => reported_completions loc names
| NONE => I)
and reported_tree (loc, props) = fold (reported loc) props;
val persistent_reports = reported_tree parse_tree [];
fun output () =
persistent_reports
|> map (fn (pos, markup, text) => Position.reported_text pos (markup ()) (text ()))
|> Output.report;
val _ =
if not (null persistent_reports) andalso redirect andalso Multithreading.enabled ()
then
Execution.print
{name = "ML_Compiler.report", pos = Position.thread_data (), pri = Task_Queue.urgent_pri}
output
else output ();
(* breakpoints *)
fun breakpoints _ (PolyML.PTnextSibling tree) = breakpoints_tree (tree ())
| breakpoints _ (PolyML.PTfirstChild tree) = breakpoints_tree (tree ())
| breakpoints loc pt =
(case ML_Parse_Tree.breakpoint pt of
SOME b =>
let val pos = Exn_Properties.position_of loc in
if is_reported pos then
let val id = serial ();
in cons ((pos, Markup.ML_breakpoint id), (id, b)) end
else I
end
| NONE => I)
and breakpoints_tree (loc, props) = fold (breakpoints loc) props;
val all_breakpoints = rev (breakpoints_tree parse_tree []);
val _ = Position.reports (map #1 all_breakpoints);
in map #2 all_breakpoints end;
(* eval ML source tokens *)
fun eval (flags: flags) pos toks =
let
val _ = Secure.secure_mltext ();
val space = ML_Env.name_space {SML = #SML flags, exchange = #exchange flags}
val opt_context = Context.thread_data ();
(* input *)
val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos)));
val input_explode =
if #SML flags then String.explode
else maps (String.explode o Symbol.esc) o Symbol.explode;
val input_buffer =
Unsynchronized.ref (toks |> map (`(input_explode o ML_Lex.check_content_of)));
fun get () =
(case ! input_buffer of
(c :: cs, tok) :: rest => (input_buffer := (cs, tok) :: rest; SOME c)
| ([], _) :: rest => (input_buffer := rest; SOME #" ")
| [] => NONE);
fun get_pos () =
(case ! input_buffer of
(_ :: _, tok) :: _ => ML_Lex.pos_of tok
| ([], tok) :: _ => ML_Lex.end_pos_of tok
| [] => Position.none);
(* output *)
val writeln_buffer = Unsynchronized.ref Buffer.empty;
fun write s = Unsynchronized.change writeln_buffer (Buffer.add s);
fun output_writeln () = writeln (trim_line (Buffer.content (! writeln_buffer)));
val warnings = Unsynchronized.ref ([]: string list);
fun warn msg = Unsynchronized.change warnings (cons msg);
fun output_warnings () = List.app warning (rev (! warnings));
val error_buffer = Unsynchronized.ref Buffer.empty;
fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n");
fun flush_error () = writeln (Buffer.content (! error_buffer));
fun raise_error msg = error (Buffer.content (Buffer.add msg (! error_buffer)));
fun message {message = msg, hard, location = loc, context = _} =
let
val pos = Exn_Properties.position_of loc;
val txt =
(if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^
Pretty.string_of (Pretty.from_ML (pretty_ml msg));
in if hard then err txt else warn txt end;
val breakpoints = Unsynchronized.ref ([]: (serial * bool Unsynchronized.ref) list);
(* results *)
val depth = ML_Options.get_print_depth ();
fun apply_result {fixes, types, signatures, structures, functors, values} =
let
fun display disp x =
if depth > 0 then
(disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> write; write "\n")
else ();
fun apply_fix (a, b) =
(#enterFix space (a, b); display PolyML.NameSpace.displayFix (a, b));
fun apply_type (a, b) =
(#enterType space (a, b); display PolyML.NameSpace.displayType (b, depth, space));
fun apply_sig (a, b) =
(#enterSig space (a, b); display PolyML.NameSpace.displaySig (b, depth, space));
fun apply_struct (a, b) =
(#enterStruct space (a, b); display PolyML.NameSpace.displayStruct (b, depth, space));
fun apply_funct (a, b) =
(#enterFunct space (a, b); display PolyML.NameSpace.displayFunct (b, depth, space));
fun apply_val (a, b) =
(#enterVal space (a, b); display PolyML.NameSpace.displayVal (b, depth, space));
in
List.app apply_fix fixes;
List.app apply_type types;
List.app apply_sig signatures;
List.app apply_struct structures;
List.app apply_funct functors;
List.app apply_val values
end;
exception STATIC_ERRORS of unit;
fun result_fun (phase1, phase2) () =
((case phase1 of
NONE => ()
| SOME parse_tree =>
breakpoints := report_parse_tree (#redirect flags) depth space parse_tree);
(case phase2 of
NONE => raise STATIC_ERRORS ()
| SOME code =>
apply_result
((code
|> Runtime.debugging opt_context
|> Runtime.toplevel_error (err o Runtime.exn_message)) ())));
(* compiler invocation *)
val parameters =
[PolyML.Compiler.CPOutStream write,
PolyML.Compiler.CPNameSpace space,
PolyML.Compiler.CPErrorMessageProc message,
PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos),
PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos),
PolyML.Compiler.CPFileName location_props,
PolyML.Compiler.CPPrintDepth ML_Options.get_print_depth,
PolyML.Compiler.CPCompilerResultFun result_fun,
PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
ML_Compiler_Parameters.debug (ML_Options.debugger_enabled opt_context);
val _ =
(while not (List.null (! input_buffer)) do
PolyML.compiler (get, parameters) ())
handle exn =>
if Exn.is_interrupt exn then reraise exn
else
let
val exn_msg =
(case exn of
STATIC_ERRORS () => ""
| Runtime.TOPLEVEL_ERROR => ""
| _ => "Exception- " ^ Pretty.string_of (Exn_Output.pretty exn) ^ " raised");
val _ = output_warnings ();
val _ = output_writeln ();
in raise_error exn_msg end;
in
if #verbose flags then (output_warnings (); flush_error (); output_writeln ())
else ()
end;
end;