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) }
+  }
+}