src/Pure/ML/ml_compiler.ML
changeset 62663 bea354f6ff21
parent 62516 5732f1c31566
child 62668 360d3464919c
equal deleted inserted replaced
62662:291cc01f56f5 62663:bea354f6ff21
    63       let val pos = Exn_Properties.position_of_location 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               |> Pretty.from_polyml |> Pretty.string_of
    69               |> Output.output |> YXML.parse_body;
    69               |> Output.output |> YXML.parse_body;
    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 =
   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_location 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_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 
   199 
   199 
   200     (* results *)
   200     (* results *)
   201 
   201 
   203 
   203 
   204     fun apply_result {fixes, types, signatures, structures, functors, values} =
   204     fun apply_result {fixes, types, signatures, structures, functors, values} =
   205       let
   205       let
   206         fun display disp x =
   206         fun display disp x =
   207           if depth > 0 then
   207           if depth > 0 then
   208             (write (disp x |> ML_Pretty.from_polyml |> Pretty.from_ML |> Pretty.string_of);
   208             (write (disp x |> Pretty.from_polyml |> Pretty.string_of); write "\n")
   209               write "\n")
       
   210           else ();
   209           else ();
   211 
   210 
   212         fun apply_fix (a, b) =
   211         fun apply_fix (a, b) =
   213           (#enterFix space (a, b); display ML_Name_Space.displayFix (a, b));
   212           (#enterFix space (a, b); display ML_Name_Space.displayFix (a, b));
   214         fun apply_type (a, b) =
   213         fun apply_type (a, b) =