--- /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;
--- 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;
--- /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;
--- 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;
-
--- /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;
--- 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;
--- 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"
--- 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";