| 
67737
 | 
     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  | 
  {
 | 
| 
71601
 | 
    23  | 
    override def toString: String = fields.iterator.map(print_field).mkString(",")
 | 
| 
67737
 | 
    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"
  | 
| 
73340
 | 
    31  | 
    def write(dir: Path): Unit = isabelle.File.write(dir + Path.explode(file_name), toString)
  | 
| 
67737
 | 
    32  | 
  }
  | 
| 
 | 
    33  | 
}
  |