diff -r 7f927120b5a2 -r ab76bd43c14a src/Pure/ML/ml_compiler.ML --- a/src/Pure/ML/ml_compiler.ML Wed Feb 17 21:51:58 2016 +0100 +++ b/src/Pure/ML/ml_compiler.ML Wed Feb 17 23:29:35 2016 +0100 @@ -1,7 +1,7 @@ (* Title: Pure/ML/ml_compiler.ML Author: Makarius -Runtime compilation and evaluation -- generic version. +Runtime compilation and evaluation. *) signature ML_COMPILER = @@ -14,9 +14,12 @@ val eval: flags -> Position.T -> ML_Lex.token list -> unit end + structure ML_Compiler: ML_COMPILER = struct +(* flags *) + type flags = {SML: bool, exchange: bool, redirect: bool, verbose: bool, debug: bool option, writeln: string -> unit, warning: string -> unit}; @@ -29,16 +32,257 @@ {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags, verbose = b, debug = #debug flags, writeln = #writeln flags, warning = #warning flags}; + +(* parse trees *) + +fun breakpoint_position loc = + let val pos = Position.reset_range (Exn_Properties.position_of loc) in + (case Position.offset_of pos of + NONE => pos + | SOME 1 => pos + | SOME j => + Position.properties_of pos + |> Properties.put (Markup.offsetN, Markup.print_int (j - 1)) + |> Position.of_properties) + end; + +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 = + ML_Name_Space.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 = breakpoint_position loc in + if is_reported pos then + let val id = serial (); + in cons ((pos, Markup.ML_breakpoint id), (id, (b, pos))) 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); + val _ = + if is_some (Context.thread_data ()) then + Context.>> (fold (ML_Env.add_breakpoint o #2) all_breakpoints) + else (); + in () end; + + +(* eval ML source tokens *) + fun eval (flags: flags) pos toks = let - val _ = if #SML flags then error ("Standard ML is unsupported on " ^ ML_System.name) else (); - val line = the_default 1 (Position.line_of pos); - val file = the_default "ML" (Position.file_of pos); - val debug = the_default false (#debug flags); - val text = ML_Lex.flatten toks; + 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 flags (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 flags) (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 flags (trim_line (Buffer.content (! error_buffer))); + fun raise_error msg = error (trim_line (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; + + + (* 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 ML_Name_Space.displayFix (a, b)); + fun apply_type (a, b) = + (#enterType space (a, b); display ML_Name_Space.displayType (b, depth, space)); + fun apply_sig (a, b) = + (#enterSig space (a, b); display ML_Name_Space.displaySig (b, depth, space)); + fun apply_struct (a, b) = + (#enterStruct space (a, b); display ML_Name_Space.displayStruct (b, depth, space)); + fun apply_funct (a, b) = + (#enterFunct space (a, b); display ML_Name_Space.displayFunct (b, depth, space)); + fun apply_val (a, b) = + (#enterVal space (a, b); display ML_Name_Space.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 => 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 debug = + (case #debug flags of + SOME debug => debug + | NONE => ML_Options.debugger_enabled opt_context); + + 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 debug; + + 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 - Secure.use_text ML_Env.local_context - {line = line, file = file, verbose = #verbose flags, debug = debug} text + if #verbose flags then (output_warnings (); flush_error (); output_writeln ()) + else () end; end;