# HG changeset patch
# User wenzelm
# Date 1519931141 -3600
# Node ID 8af6fcdc869dbd8db8f339e3d2685db44ca5f0e6
# Parent  65016740d3e015fd0dae3d0ffcbe4dd535617f2a
support for CSV files;

diff -r 65016740d3e0 -r 8af6fcdc869d src/Pure/General/csv.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/csv.scala	Thu Mar 01 20:05:41 2018 +0100
@@ -0,0 +1,33 @@
+/*  Title:      Pure/General/csv.scala
+    Author:     Makarius
+
+Support for CSV: RFC 4180.
+*/
+
+package isabelle
+
+
+object CSV
+{
+  def print_field(field: Any): String =
+  {
+    val str = field.toString
+    if (str.exists("\",\r\n".contains(_))) {
+      (for (c <- str) yield { if (c == '"') "\"\"" else c.toString }).mkString("\"", "", "\"")
+    }
+    else str
+  }
+
+  sealed case class Record(fields: Any*)
+  {
+    override def toString: String = fields.iterator.map(print_field(_)).mkString(",")
+  }
+
+  sealed case class File(name: String, header: List[String], records: List[Record])
+  {
+    override def toString: String = (Record(header:_*) :: records).mkString("\r\n")
+
+    def file_name: String = name + ".csv"
+    def write(dir: Path) { isabelle.File.write(dir + Path.explode(file_name), toString) }
+  }
+}
diff -r 65016740d3e0 -r 8af6fcdc869d src/Pure/build-jars
--- a/src/Pure/build-jars	Thu Mar 01 15:02:45 2018 +0100
+++ b/src/Pure/build-jars	Thu Mar 01 20:05:41 2018 +0100
@@ -46,6 +46,7 @@
   General/codepoint.scala
   General/comment.scala
   General/completion.scala
+  General/csv.scala
   General/date.scala
   General/exn.scala
   General/file.scala