proper trim_line according to ML/Scala versions;
authorwenzelm
Thu, 20 Dec 2018 16:34:23 +0100
changeset 69498 59ada9f63cc5
parent 69497 b734ff28e405
child 69499 681760f50723
proper trim_line according to ML/Scala versions;
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