equal
deleted
inserted
replaced
44 |
44 |
45 val method_of_file_name = |
45 val method_of_file_name = |
46 perhaps (try (unsuffix "_suggestions")) o List.last o space_explode "/" |
46 perhaps (try (unsuffix "_suggestions")) o List.last o space_explode "/" |
47 |
47 |
48 val methods = "isar" :: map method_of_file_name file_names |
48 val methods = "isar" :: map method_of_file_name file_names |
49 val lines_of = Path.explode #> try File.read_lines #> these |
49 val lines_of = Path.explode #> try (Bytes.read #> Bytes.trim_split_lines) #> these |
50 val liness0 = map lines_of file_names |
50 val liness0 = map lines_of file_names |
51 val num_lines = fold (Integer.max o length) liness0 0 |
51 val num_lines = fold (Integer.max o length) liness0 0 |
52 |
52 |
53 fun pad lines = lines @ replicate (num_lines - length lines) "" |
53 fun pad lines = lines @ replicate (num_lines - length lines) "" |
54 |
54 |