src/Pure/General/csv.scala
changeset 75393 87ebf5a50283
parent 73340 0ffcad1f6130
child 75606 0f7cb6cd08fe
--- a/src/Pure/General/csv.scala	Fri Apr 01 11:51:42 2022 +0200
+++ b/src/Pure/General/csv.scala	Fri Apr 01 17:06:10 2022 +0200
@@ -7,10 +7,8 @@
 package isabelle
 
 
-object CSV
-{
-  def print_field(field: Any): String =
-  {
+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("\"", "", "\"")
@@ -18,13 +16,11 @@
     else str
   }
 
-  sealed case class Record(fields: Any*)
-  {
+  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])
-  {
+  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"