src/Pure/General/csv.scala
author wenzelm
Thu, 01 Mar 2018 20:05:41 +0100
changeset 67737 8af6fcdc869d
child 71601 97ccf48c2f0c
permissions -rw-r--r--
support for CSV files;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
67737
8af6fcdc869d support for CSV files;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/csv.scala
8af6fcdc869d support for CSV files;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
8af6fcdc869d support for CSV files;
wenzelm
parents:
diff changeset
     3
8af6fcdc869d support for CSV files;
wenzelm
parents:
diff changeset
     4
Support for CSV: RFC 4180.
8af6fcdc869d support for CSV files;
wenzelm
parents:
diff changeset
     5
*/
8af6fcdc869d support for CSV files;
wenzelm
parents:
diff changeset
     6
8af6fcdc869d support for CSV files;
wenzelm
parents:
diff changeset
     7
package isabelle
8af6fcdc869d support for CSV files;
wenzelm
parents:
diff changeset
     8
8af6fcdc869d support for CSV files;
wenzelm
parents:
diff changeset
     9
8af6fcdc869d support for CSV files;
wenzelm
parents:
diff changeset
    10
object CSV
8af6fcdc869d support for CSV files;
wenzelm
parents:
diff changeset
    11
{
8af6fcdc869d support for CSV files;
wenzelm
parents:
diff changeset
    12
  def print_field(field: Any): String =
8af6fcdc869d support for CSV files;
wenzelm
parents:
diff changeset
    13
  {
8af6fcdc869d support for CSV files;
wenzelm
parents:
diff changeset
    14
    val str = field.toString
8af6fcdc869d support for CSV files;
wenzelm
parents:
diff changeset
    15
    if (str.exists("\",\r\n".contains(_))) {
8af6fcdc869d support for CSV files;
wenzelm
parents:
diff changeset
    16
      (for (c <- str) yield { if (c == '"') "\"\"" else c.toString }).mkString("\"", "", "\"")
8af6fcdc869d support for CSV files;
wenzelm
parents:
diff changeset
    17
    }
8af6fcdc869d support for CSV files;
wenzelm
parents:
diff changeset
    18
    else str
8af6fcdc869d support for CSV files;
wenzelm
parents:
diff changeset
    19
  }
8af6fcdc869d support for CSV files;
wenzelm
parents:
diff changeset
    20
8af6fcdc869d support for CSV files;
wenzelm
parents:
diff changeset
    21
  sealed case class Record(fields: Any*)
8af6fcdc869d support for CSV files;
wenzelm
parents:
diff changeset
    22
  {
8af6fcdc869d support for CSV files;
wenzelm
parents:
diff changeset
    23
    override def toString: String = fields.iterator.map(print_field(_)).mkString(",")
8af6fcdc869d support for CSV files;
wenzelm
parents:
diff changeset
    24
  }
8af6fcdc869d support for CSV files;
wenzelm
parents:
diff changeset
    25
8af6fcdc869d support for CSV files;
wenzelm
parents:
diff changeset
    26
  sealed case class File(name: String, header: List[String], records: List[Record])
8af6fcdc869d support for CSV files;
wenzelm
parents:
diff changeset
    27
  {
8af6fcdc869d support for CSV files;
wenzelm
parents:
diff changeset
    28
    override def toString: String = (Record(header:_*) :: records).mkString("\r\n")
8af6fcdc869d support for CSV files;
wenzelm
parents:
diff changeset
    29
8af6fcdc869d support for CSV files;
wenzelm
parents:
diff changeset
    30
    def file_name: String = name + ".csv"
8af6fcdc869d support for CSV files;
wenzelm
parents:
diff changeset
    31
    def write(dir: Path) { isabelle.File.write(dir + Path.explode(file_name), toString) }
8af6fcdc869d support for CSV files;
wenzelm
parents:
diff changeset
    32
  }
8af6fcdc869d support for CSV files;
wenzelm
parents:
diff changeset
    33
}