equal
deleted
inserted
replaced
108 case None => name |
108 case None => name |
109 } |
109 } |
110 } |
110 } |
111 |
111 |
112 def apply(name: String, lines: List[String]): Log_File = |
112 def apply(name: String, lines: List[String]): Log_File = |
113 new Log_File(plain_name(name), lines) |
113 new Log_File(plain_name(name), lines.map(Library.trim_line)) |
114 |
114 |
115 def apply(name: String, text: String): Log_File = |
115 def apply(name: String, text: String): Log_File = |
116 Log_File(name, Library.trim_split_lines(text)) |
116 new Log_File(plain_name(name), Library.trim_split_lines(text)) |
117 |
117 |
118 def apply(file: JFile): Log_File = |
118 def apply(file: JFile): Log_File = |
119 { |
119 { |
120 val name = file.getName |
120 val name = file.getName |
121 val text = |
121 val text = |