tuned messages;
authorwenzelm
Mon, 10 Aug 2015 11:23:49 +0200
changeset 60872 9f45c2f1cbfd
parent 60871 9b26f3118e40
child 60873 974d9acb2b87
tuned messages;
src/Pure/ML/ml_compiler_polyml.ML
--- a/src/Pure/ML/ml_compiler_polyml.ML	Mon Aug 10 11:20:16 2015 +0200
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Mon Aug 10 11:23:49 2015 +0200
@@ -153,8 +153,8 @@
 
     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 (Buffer.content (! error_buffer));
-    fun raise_error msg = error (Buffer.content (Buffer.add msg (! error_buffer)));
+    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