src/Tools/Haskell/Haskell.thy
changeset 69486 59ada9f63cc5
parent 69482 186b03abb764
child 69490 ce85542368b9
equal deleted inserted replaced
69485:b734ff28e405 69486:59ada9f63cc5
   114 split_lines :: String -> [String]
   114 split_lines :: String -> [String]
   115 split_lines = space_explode '\n'
   115 split_lines = space_explode '\n'
   116 
   116 
   117 trim_line :: String -> String
   117 trim_line :: String -> String
   118 trim_line line =
   118 trim_line line =
   119   case reverse line of
   119   if not (null line) && (last line == '\r' || last line == '\n') then
   120     '\n' : '\r' : rest -> reverse rest
   120     case reverse line of
   121     '\n' : rest -> reverse rest
   121       '\n' : '\r' : rest -> reverse rest
   122     _ -> line
   122       '\r' : rest -> reverse rest
       
   123       '\n' : rest -> reverse rest
       
   124       _ -> line
       
   125   else line
   123 
   126 
   124 clean_name :: String -> String
   127 clean_name :: String -> String
   125 clean_name = reverse #> dropWhile (== '_') #> reverse
   128 clean_name = reverse #> dropWhile (== '_') #> reverse
   126 \<close>
   129 \<close>
   127 
   130