# HG changeset patch
# User wenzelm
# Date 1545320063 -3600
# Node ID 59ada9f63cc5bffccb509d28062f13a9e23ccbde
# Parent  b734ff28e40536321e7b9e9f4af0788fff064cc8
proper trim_line according to ML/Scala versions;

diff -r b734ff28e405 -r 59ada9f63cc5 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Thu Dec 20 12:55:45 2018 +0000
+++ b/src/Tools/Haskell/Haskell.thy	Thu Dec 20 16:34:23 2018 +0100
@@ -116,10 +116,13 @@
 
 trim_line :: String -> String
 trim_line line =
-  case reverse line of
-    '\n' : '\r' : rest -> reverse rest
-    '\n' : rest -> reverse rest
-    _ -> line
+  if not (null line) && (last line == '\r' || last line == '\n') then
+    case reverse line of
+      '\n' : '\r' : rest -> reverse rest
+      '\r' : rest -> reverse rest
+      '\n' : rest -> reverse rest
+      _ -> line
+  else line
 
 clean_name :: String -> String
 clean_name = reverse #> dropWhile (== '_') #> reverse