tuned messages;
authorwenzelm
Mon Aug 10 11:23:49 2015 +0200 (2015-08-10)
changeset 608729f45c2f1cbfd
parent 60871 9b26f3118e40
child 60873 974d9acb2b87
tuned messages;
src/Pure/ML/ml_compiler_polyml.ML
     1.1 --- a/src/Pure/ML/ml_compiler_polyml.ML	Mon Aug 10 11:20:16 2015 +0200
     1.2 +++ b/src/Pure/ML/ml_compiler_polyml.ML	Mon Aug 10 11:23:49 2015 +0200
     1.3 @@ -153,8 +153,8 @@
     1.4  
     1.5      val error_buffer = Unsynchronized.ref Buffer.empty;
     1.6      fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n");
     1.7 -    fun flush_error () = #writeln flags (Buffer.content (! error_buffer));
     1.8 -    fun raise_error msg = error (Buffer.content (Buffer.add msg (! error_buffer)));
     1.9 +    fun flush_error () = #writeln flags (trim_line (Buffer.content (! error_buffer)));
    1.10 +    fun raise_error msg = error (trim_line (Buffer.content (Buffer.add msg (! error_buffer))));
    1.11  
    1.12      fun message {message = msg, hard, location = loc, context = _} =
    1.13        let