src/Pure/ML/ml_compiler.ML
changeset 62516 5732f1c31566
parent 62505 9e2a65912111
child 62663 bea354f6ff21
equal deleted inserted replaced
62515:e73644de5db8 62516:5732f1c31566
    36 
    36 
    37 
    37 
    38 (* parse trees *)
    38 (* parse trees *)
    39 
    39 
    40 fun breakpoint_position loc =
    40 fun breakpoint_position loc =
    41   let val pos = Position.reset_range (Exn_Properties.position_of loc) in
    41   let val pos = Position.reset_range (Exn_Properties.position_of_location loc) in
    42     (case Position.offset_of pos of
    42     (case Position.offset_of pos of
    43       NONE => pos
    43       NONE => pos
    44     | SOME 1 => pos
    44     | SOME 1 => pos
    45     | SOME j =>
    45     | SOME j =>
    46         Position.properties_of pos
    46         Position.properties_of pos
    58 
    58 
    59 
    59 
    60     (* syntax reports *)
    60     (* syntax reports *)
    61 
    61 
    62     fun reported_types loc types =
    62     fun reported_types loc types =
    63       let val pos = Exn_Properties.position_of loc in
    63       let val pos = Exn_Properties.position_of_location loc in
    64         is_reported pos ?
    64         is_reported pos ?
    65           let
    65           let
    66             val xml =
    66             val xml =
    67               ML_Name_Space.displayTypeExpression (types, depth, space)
    67               ML_Name_Space.displayTypeExpression (types, depth, space)
    68               |> ML_Pretty.from_polyml |> Pretty.from_ML |> Pretty.string_of
    68               |> ML_Pretty.from_polyml |> Pretty.from_ML |> Pretty.string_of
    70           in cons (pos, fn () => Markup.ML_typing, fn () => YXML.string_of_body xml) end
    70           in cons (pos, fn () => Markup.ML_typing, fn () => YXML.string_of_body xml) end
    71       end;
    71       end;
    72 
    72 
    73     fun reported_entity kind loc decl =
    73     fun reported_entity kind loc decl =
    74       let
    74       let
    75         val pos = Exn_Properties.position_of loc;
    75         val pos = Exn_Properties.position_of_location loc;
    76         val def_pos = Exn_Properties.position_of decl;
    76         val def_pos = Exn_Properties.position_of_location decl;
    77       in
    77       in
    78         (is_reported pos andalso pos <> def_pos) ?
    78         (is_reported pos andalso pos <> def_pos) ?
    79           let
    79           let
    80             fun markup () =
    80             fun markup () =
    81               (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of def_pos);
    81               (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of def_pos);
    82           in cons (pos, markup, fn () => "") end
    82           in cons (pos, markup, fn () => "") end
    83       end;
    83       end;
    84 
    84 
    85     fun reported_completions loc names =
    85     fun reported_completions loc names =
    86       let val pos = Exn_Properties.position_of loc in
    86       let val pos = Exn_Properties.position_of_location loc in
    87         if is_reported pos andalso not (null names) then
    87         if is_reported pos andalso not (null names) then
    88           let
    88           let
    89             val completion = Completion.names pos (map (fn a => (a, ("ML", a))) names);
    89             val completion = Completion.names pos (map (fn a => (a, ("ML", a))) names);
    90             val xml = Completion.encode completion;
    90             val xml = Completion.encode completion;
    91           in cons (pos, fn () => Markup.completion, fn () => YXML.string_of_body xml) end
    91           in cons (pos, fn () => Markup.completion, fn () => YXML.string_of_body xml) end
   188     fun flush_error () = #writeln flags (trim_line (Buffer.content (! error_buffer)));
   188     fun flush_error () = #writeln flags (trim_line (Buffer.content (! error_buffer)));
   189     fun raise_error msg = error (trim_line (Buffer.content (Buffer.add msg (! error_buffer))));
   189     fun raise_error msg = error (trim_line (Buffer.content (Buffer.add msg (! error_buffer))));
   190 
   190 
   191     fun message {message = msg, hard, location = loc, context = _} =
   191     fun message {message = msg, hard, location = loc, context = _} =
   192       let
   192       let
   193         val pos = Exn_Properties.position_of loc;
   193         val pos = Exn_Properties.position_of_location loc;
   194         val txt =
   194         val txt =
   195           (if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^
   195           (if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^
   196           Pretty.string_of (Pretty.from_ML (ML_Pretty.from_polyml msg));
   196           Pretty.string_of (Pretty.from_ML (ML_Pretty.from_polyml msg));
   197       in if hard then err txt else warn txt end;
   197       in if hard then err txt else warn txt end;
   198 
   198 
   273           let
   273           let
   274             val exn_msg =
   274             val exn_msg =
   275               (case exn of
   275               (case exn of
   276                 STATIC_ERRORS () => ""
   276                 STATIC_ERRORS () => ""
   277               | Runtime.TOPLEVEL_ERROR => ""
   277               | Runtime.TOPLEVEL_ERROR => ""
   278               | _ => "Exception- " ^ Pretty.string_of (Exn_Output.pretty exn) ^ " raised");
   278               | _ => "Exception- " ^ Pretty.string_of (Runtime.pretty_exn exn) ^ " raised");
   279             val _ = output_warnings ();
   279             val _ = output_warnings ();
   280             val _ = output_writeln ();
   280             val _ = output_writeln ();
   281           in raise_error exn_msg end;
   281           in raise_error exn_msg end;
   282   in
   282   in
   283     if #verbose flags then (output_warnings (); flush_error (); output_writeln ())
   283     if #verbose flags then (output_warnings (); flush_error (); output_writeln ())