equal
deleted
inserted
replaced
|
1 /* Title: Pure/General/csv.scala |
|
2 Author: Makarius |
|
3 |
|
4 Support for CSV: RFC 4180. |
|
5 */ |
|
6 |
|
7 package isabelle |
|
8 |
|
9 |
|
10 object CSV |
|
11 { |
|
12 def print_field(field: Any): String = |
|
13 { |
|
14 val str = field.toString |
|
15 if (str.exists("\",\r\n".contains(_))) { |
|
16 (for (c <- str) yield { if (c == '"') "\"\"" else c.toString }).mkString("\"", "", "\"") |
|
17 } |
|
18 else str |
|
19 } |
|
20 |
|
21 sealed case class Record(fields: Any*) |
|
22 { |
|
23 override def toString: String = fields.iterator.map(print_field(_)).mkString(",") |
|
24 } |
|
25 |
|
26 sealed case class File(name: String, header: List[String], records: List[Record]) |
|
27 { |
|
28 override def toString: String = (Record(header:_*) :: records).mkString("\r\n") |
|
29 |
|
30 def file_name: String = name + ".csv" |
|
31 def write(dir: Path) { isabelle.File.write(dir + Path.explode(file_name), toString) } |
|
32 } |
|
33 } |