# HG changeset patch # User wenzelm # Date 1455747347 -3600 # Node ID 00f7618a9f2b2c272517aa66cc986d2621dd35f9 # Parent fdd6989cc8a09c0bed7136c0fa60ed3dcc30bb29 clarified file names; diff -r fdd6989cc8a0 -r 00f7618a9f2b src/Pure/ML/exn_output.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML/exn_output.ML Wed Feb 17 23:15:47 2016 +0100 @@ -0,0 +1,24 @@ +(* Title: Pure/ML/exn_output.ML + Author: Makarius + +Auxiliary operations for exception output. +*) + +signature EXN_OUTPUT = +sig + val position: exn -> Position.T + val pretty: exn -> Pretty.T +end; + +structure Exn_Output: EXN_OUTPUT = +struct + +fun position exn = + (case PolyML.exceptionLocation exn of + NONE => Position.none + | SOME loc => Exn_Properties.position_of loc); + +fun pretty (exn: exn) = + Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (exn, ML_Options.get_print_depth ()))); + +end; diff -r fdd6989cc8a0 -r 00f7618a9f2b src/Pure/ML/exn_output_polyml.ML --- a/src/Pure/ML/exn_output_polyml.ML Wed Feb 17 23:06:24 2016 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,24 +0,0 @@ -(* Title: Pure/ML/exn_output_polyml.ML - Author: Makarius - -Auxiliary operations for exception output -- Poly/ML version. -*) - -signature EXN_OUTPUT = -sig - val position: exn -> Position.T - val pretty: exn -> Pretty.T -end; - -structure Exn_Output: EXN_OUTPUT = -struct - -fun position exn = - (case PolyML.exceptionLocation exn of - NONE => Position.none - | SOME loc => Exn_Properties.position_of loc); - -fun pretty (exn: exn) = - Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (exn, ML_Options.get_print_depth ()))); - -end; diff -r fdd6989cc8a0 -r 00f7618a9f2b src/Pure/ML/exn_properties.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML/exn_properties.ML Wed Feb 17 23:15:47 2016 +0100 @@ -0,0 +1,63 @@ +(* Title: Pure/ML/exn_properties.ML + Author: Makarius + +Exception properties. +*) + +signature EXN_PROPERTIES = +sig + val position_of: PolyML.location -> Position.T + val get: exn -> Properties.T + val update: Properties.entry list -> exn -> exn +end; + +structure Exn_Properties: EXN_PROPERTIES = +struct + +(* source locations *) + +fun props_of (loc: PolyML.location) = + (case YXML.parse_body (#file loc) of + [] => [] + | [XML.Text file] => + if file = "Standard Basis" then [] + else [(Markup.fileN, ml_standard_path file)] + | body => XML.Decode.properties body); + +fun position_of loc = + Position.make + {line = #startLine loc, + offset = #startPosition loc, + end_offset = #endPosition loc, + props = props_of loc}; + + +(* exception properties *) + +fun get exn = + (case PolyML.exceptionLocation exn of + NONE => [] + | SOME loc => props_of loc); + +fun update entries exn = + let + val loc = + the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0} + (PolyML.exceptionLocation exn); + val props = props_of loc; + val props' = fold Properties.put entries props; + in + if props = props' then exn + else + let + val loc' = + {file = YXML.string_of_body (XML.Encode.properties props'), + startLine = #startLine loc, endLine = #endLine loc, + startPosition = #startPosition loc, endPosition = #endPosition loc}; + in + uninterruptible (fn _ => fn () => PolyML.raiseWithLocation (exn, loc')) () + handle exn' => exn' + end + end; + +end; diff -r fdd6989cc8a0 -r 00f7618a9f2b src/Pure/ML/exn_properties_polyml.ML --- a/src/Pure/ML/exn_properties_polyml.ML Wed Feb 17 23:06:24 2016 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,64 +0,0 @@ -(* Title: Pure/ML/exn_properties_polyml.ML - Author: Makarius - -Exception properties for Poly/ML. -*) - -signature EXN_PROPERTIES = -sig - val position_of: PolyML.location -> Position.T - val get: exn -> Properties.T - val update: Properties.entry list -> exn -> exn -end; - -structure Exn_Properties: EXN_PROPERTIES = -struct - -(* source locations *) - -fun props_of (loc: PolyML.location) = - (case YXML.parse_body (#file loc) of - [] => [] - | [XML.Text file] => - if file = "Standard Basis" then [] - else [(Markup.fileN, ml_standard_path file)] - | body => XML.Decode.properties body); - -fun position_of loc = - Position.make - {line = #startLine loc, - offset = #startPosition loc, - end_offset = #endPosition loc, - props = props_of loc}; - - -(* exception properties *) - -fun get exn = - (case PolyML.exceptionLocation exn of - NONE => [] - | SOME loc => props_of loc); - -fun update entries exn = - let - val loc = - the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0} - (PolyML.exceptionLocation exn); - val props = props_of loc; - val props' = fold Properties.put entries props; - in - if props = props' then exn - else - let - val loc' = - {file = YXML.string_of_body (XML.Encode.properties props'), - startLine = #startLine loc, endLine = #endLine loc, - startPosition = #startPosition loc, endPosition = #endPosition loc}; - in - uninterruptible (fn _ => fn () => PolyML.raiseWithLocation (exn, loc')) () - handle exn' => exn' - end - end; - -end; - diff -r fdd6989cc8a0 -r 00f7618a9f2b src/Pure/ML/ml_compiler.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML/ml_compiler.ML Wed Feb 17 23:15:47 2016 +0100 @@ -0,0 +1,288 @@ +(* Title: Pure/ML/ml_compiler.ML + Author: Makarius + +Runtime compilation and evaluation. +*) + +signature ML_COMPILER = +sig + type flags = + {SML: bool, exchange: bool, redirect: bool, verbose: bool, + debug: bool option, writeln: string -> unit, warning: string -> unit} + val flags: flags + val verbose: bool -> flags -> flags + 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}; + +val flags: flags = + {SML = false, exchange = false, redirect = false, verbose = false, + debug = NONE, writeln = writeln, warning = warning}; + +fun verbose b (flags: flags) = + {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 _ = 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 + if #verbose flags then (output_warnings (); flush_error (); output_writeln ()) + else () + end; + +end; diff -r fdd6989cc8a0 -r 00f7618a9f2b src/Pure/ML/ml_compiler_polyml.ML --- a/src/Pure/ML/ml_compiler_polyml.ML Wed Feb 17 23:06:24 2016 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,288 +0,0 @@ -(* Title: Pure/ML/ml_compiler_polyml.ML - Author: Makarius - -Runtime compilation and evaluation -- Poly/ML version. -*) - -signature ML_COMPILER = -sig - type flags = - {SML: bool, exchange: bool, redirect: bool, verbose: bool, - debug: bool option, writeln: string -> unit, warning: string -> unit} - val flags: flags - val verbose: bool -> flags -> flags - 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}; - -val flags: flags = - {SML = false, exchange = false, redirect = false, verbose = false, - debug = NONE, writeln = writeln, warning = warning}; - -fun verbose b (flags: flags) = - {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 _ = 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 - if #verbose flags then (output_warnings (); flush_error (); output_writeln ()) - else () - end; - -end; diff -r fdd6989cc8a0 -r 00f7618a9f2b src/Pure/ROOT --- a/src/Pure/ROOT Wed Feb 17 23:06:24 2016 +0100 +++ b/src/Pure/ROOT Wed Feb 17 23:15:47 2016 +0100 @@ -163,11 +163,11 @@ "Isar/token.ML" "Isar/toplevel.ML" "Isar/typedecl.ML" - "ML/exn_output_polyml.ML" - "ML/exn_properties_polyml.ML" + "ML/exn_output.ML" + "ML/exn_properties.ML" "ML/install_pp_polyml.ML" "ML/ml_antiquotation.ML" - "ML/ml_compiler_polyml.ML" + "ML/ml_compiler.ML" "ML/ml_context.ML" "ML/ml_env.ML" "ML/ml_file.ML" diff -r fdd6989cc8a0 -r 00f7618a9f2b src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Wed Feb 17 23:06:24 2016 +0100 +++ b/src/Pure/ROOT.ML Wed Feb 17 23:15:47 2016 +0100 @@ -98,7 +98,7 @@ (* concurrency within the ML runtime *) -use "ML/exn_properties_polyml.ML"; +use "ML/exn_properties.ML"; if ML_System.name = "polyml-5.5.0" orelse ML_System.name = "polyml-5.5.1" @@ -200,11 +200,11 @@ use "ML/ml_syntax.ML"; use "ML/ml_env.ML"; use "ML/ml_options.ML"; -use "ML/exn_output_polyml.ML"; +use "ML/exn_output.ML"; use "ML/ml_options.ML"; use "Isar/runtime.ML"; use "PIDE/execution.ML"; -use "ML/ml_compiler_polyml.ML"; +use "ML/ml_compiler.ML"; use "skip_proof.ML"; use "goal.ML";