equal
deleted
inserted
replaced
111 |
111 |
112 fun message {message = msg, hard, location = loc, context = _} = |
112 fun message {message = msg, hard, location = loc, context = _} = |
113 let |
113 let |
114 val pos = position_of loc; |
114 val pos = position_of loc; |
115 val txt = |
115 val txt = |
116 (Position.is_reported pos ? Markup.markup Isabelle_Markup.no_report) |
116 (if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^ |
117 ((if hard then "Error" else "Warning") ^ Position.here pos ^ ":\n") ^ |
117 Pretty.string_of (Pretty.from_ML (pretty_ml msg)); |
118 Pretty.string_of (Pretty.from_ML (pretty_ml msg)) ^ |
|
119 Position.reported_text pos Isabelle_Markup.report ""; |
|
120 in if hard then err txt else warn txt end; |
118 in if hard then err txt else warn txt end; |
121 |
119 |
122 |
120 |
123 (* results *) |
121 (* results *) |
124 |
122 |