src/Pure/General/toml.scala
changeset 78326 1cdc65476c2e
parent 78317 fcabbb45b272
child 78327 a235fc426523
equal deleted inserted replaced
78325:19c617950a8e 78326:1cdc65476c2e
   499 
   499 
   500 
   500 
   501   /* Format TOML */
   501   /* Format TOML */
   502 
   502 
   503   object Format {
   503   object Format {
       
   504     private def basic_string(s: Str): Str =
       
   505       "\"" + s.iterator.map {
       
   506         case '\b' => "\\b" case '\t' => "\\t" case '\n' => "\\n" case '\f' => "\\f"
       
   507         case '\r' => "\\r" case '"' => "\\\"" case '\\' => "\\\\" case c =>
       
   508         if (c <= '\u001f' || c == '\u007f') "\\u%04x".format(c.toInt) else c
       
   509       }.mkString + "\""
       
   510 
       
   511     private def multiline_basic_string(s: Str): Str =
       
   512       "\"\"\"\n" + s.iterator.map {
       
   513         case '\b' => "\\b" case '\t' => "\t" case '\n' => "\n" case '\f' => "\\f"
       
   514         case '\r' => "\r" case '"' => "\\\"" case '\\' => "\\\\" case c =>
       
   515           if (c <= '\u001f' || c == '\u007f') "\\u%04x".format(c.toInt) else c
       
   516       }.mkString.replace("\"\"\"", "\"\"\\\"") + "\"\"\""
       
   517 
       
   518     def key(k: Key): Str = {
       
   519       val Bare_Key = """[A-Za-z0-9_-]+""".r
       
   520       k match {
       
   521         case Bare_Key() => k
       
   522         case _ => basic_string(k)
       
   523       }
       
   524     }
       
   525 
       
   526     def keys(ks: Keys): Str = ks.mkString(".")
       
   527 
       
   528     def inline(t: T, indent: Int = 0): Str = {
       
   529       val result = new StringBuilder
       
   530       def indentation(i: Int): Unit = for (_ <- Range(0, i)) result ++= "  "
       
   531 
       
   532       indentation(indent)
       
   533       t match {
       
   534         case s: String =>
       
   535           if (s.rep.contains("\n") && s.rep.length > 20) result ++= multiline_basic_string(s.rep)
       
   536           else result ++= basic_string(s.rep)
       
   537         case i: Integer => result ++= i.rep.toString
       
   538         case f: Float => result ++= f.rep.toString
       
   539         case b: Boolean => result ++= b.rep.toString
       
   540         case o: Offset_Date_Time => result ++= o.rep.toString
       
   541         case l: Local_Date_Time => result ++= l.rep.toString
       
   542         case l: Local_Date => result ++= l.rep.toString
       
   543         case l: Local_Time => result ++= l.rep.toString
       
   544         case a: Array =>
       
   545           if (a.is_empty) result ++= "[]"
       
   546           else {
       
   547             result ++= "[\n"
       
   548             a.any.values.foreach { elem =>
       
   549               result ++= inline(elem, indent + 1)
       
   550               result ++= ",\n"
       
   551             }
       
   552             indentation(indent)
       
   553             result += ']'
       
   554           }
       
   555         case table: Table =>
       
   556           if (table.is_empty) result ++= "{}"
       
   557           else {
       
   558             result ++= "{ "
       
   559             Library.separate(None, table.any.values.map(Some(_))).foreach {
       
   560               case None => result ++= ", "
       
   561               case Some((k, v)) =>
       
   562                 result ++= key(k)
       
   563                 result ++= " = "
       
   564                 result ++= inline(v)
       
   565             }
       
   566             result ++= " }"
       
   567           }
       
   568       }
       
   569       result.toString()
       
   570     }
       
   571 
   504     def apply(toml: Table): Str = {
   572     def apply(toml: Table): Str = {
   505       val result = new StringBuilder
   573       val result = new StringBuilder
   506 
       
   507       /* keys */
       
   508 
       
   509       def key(k: Key): Unit = {
       
   510         val Bare_Key = """[A-Za-z0-9_-]+""".r
       
   511         k match {
       
   512           case Bare_Key() => result ++= k
       
   513           case _ => result ++= basic_string(k)
       
   514         }
       
   515       }
       
   516 
       
   517       def keys(ks: List[Key]): Unit =
       
   518         Library.separate(None, ks.reverse.map(Some(_))).foreach {
       
   519           case None => result += '.'
       
   520           case Some(k) => key(k)
       
   521         }
       
   522 
       
   523       /* string */
       
   524 
       
   525       def basic_string(s: Str): Str =
       
   526         "\"" + s.iterator.map {
       
   527             case '\b' => "\\b" case '\t' => "\\t" case '\n' => "\\n" case '\f' => "\\f"
       
   528             case '\r' => "\\r" case '"' => "\\\"" case '\\' => "\\\\" case c =>
       
   529               if (c <= '\u001f' || c == '\u007f') "\\u%04x".format(c.toInt) else c
       
   530           }.mkString + "\""
       
   531 
       
   532       def multiline_basic_string(s: Str): Str =
       
   533         "\"\"\"\n" + s.iterator.map {
       
   534           case '\b' => "\\b" case '\t' => "\t" case '\n' => "\n" case '\f' => "\\f"
       
   535           case '\r' => "\r" case '"' => "\\\"" case '\\' => "\\\\" case c =>
       
   536             if (c <= '\u001f' || c == '\u007f') "\\u%04x".format(c.toInt) else c
       
   537         }.mkString.replace("\"\"\"", "\"\"\\\"") + "\"\"\""
       
   538 
       
   539 
       
   540       def `inline`(t: T, indent: Int = 0): Unit = {
       
   541         def indentation(i: Int): Unit = for (_ <- Range(0, i)) result ++= "  "
       
   542 
       
   543         indentation(indent)
       
   544         t match {
       
   545           case s: String =>
       
   546             if (s.rep.contains("\n") && s.rep.length > 20) result ++= multiline_basic_string(s.rep)
       
   547             else result ++= basic_string(s.rep)
       
   548           case i: Integer => result ++= i.rep.toString
       
   549           case f: Float => result ++= f.rep.toString
       
   550           case b: Boolean => result ++= b.rep.toString
       
   551           case o: Offset_Date_Time => result ++= o.rep.toString
       
   552           case l: Local_Date_Time => result ++= l.rep.toString
       
   553           case l: Local_Date => result ++= l.rep.toString
       
   554           case l: Local_Time => result ++= l.rep.toString
       
   555           case a: Array =>
       
   556             if (a.is_empty) result ++= "[]"
       
   557             else {
       
   558               result ++= "[\n"
       
   559               a.any.values.foreach { elem =>
       
   560                 `inline`(elem, indent + 1)
       
   561                 result ++= ",\n"
       
   562               }
       
   563               indentation(indent)
       
   564               result += ']'
       
   565             }
       
   566           case table: Table =>
       
   567             if (table.is_empty) result ++= "{}"
       
   568             else {
       
   569               result += '{'
       
   570               table.any.values.foreach { case (k, v) =>
       
   571                 key(k)
       
   572                 result ++= " = "
       
   573                 `inline`(v)
       
   574               }
       
   575               result += '}'
       
   576             }
       
   577         }
       
   578       }
       
   579 
       
   580       /* array */
       
   581 
   574 
   582       def inline_values(path: List[Key], t: T): Unit =
   575       def inline_values(path: List[Key], t: T): Unit =
   583         t match {
   576         t match {
   584           case t: Table => t.any.values.foreach { case (k, v1) => inline_values(k :: path, v1) }
   577           case t: Table => t.any.values.foreach { case (k, v1) => inline_values(k :: path, v1) }
   585           case _ =>
   578           case _ =>
   586             keys(path)
   579             result ++= keys(path.reverse)
   587             result ++= " = "
   580             result ++= " = "
   588             `inline`(t)
   581             result ++= inline(t)
   589             result += '\n'
   582             result += '\n'
   590         }
   583         }
   591 
   584 
   592       def is_inline(elem: T): Bool =
   585       def is_inline(elem: T): Bool =
   593         elem match {
   586         elem match {
   601       def array(path: List[Key], a: Array): Unit =
   594       def array(path: List[Key], a: Array): Unit =
   602         if (a.any.values.forall(is_inline) || !a.any.values.forall(is_table))
   595         if (a.any.values.forall(is_inline) || !a.any.values.forall(is_table))
   603           inline_values(path.take(1), a)
   596           inline_values(path.take(1), a)
   604         else a.table.values.foreach { t =>
   597         else a.table.values.foreach { t =>
   605           result ++= "\n[["
   598           result ++= "\n[["
   606           keys(path)
   599           result ++= keys(path.reverse)
   607           result ++= "]]\n"
   600           result ++= "]]\n"
   608           table(path, t, is_table_entry = true)
   601           table(path, t, is_table_entry = true)
   609         }
   602         }
   610 
   603 
   611       /* table */
       
   612 
       
   613       def table(path: List[Key], t: Table, is_table_entry: Bool = false): Unit = {
   604       def table(path: List[Key], t: Table, is_table_entry: Bool = false): Unit = {
   614         val (values, nodes) = t.any.values.partition(kv => is_inline(kv._2))
   605         val (values, nodes) = t.any.values.partition(kv => is_inline(kv._2))
   615 
   606 
   616         if (!is_table_entry && path.nonEmpty) {
   607         if (!is_table_entry && path.nonEmpty) {
   617           result ++= "\n["
   608           result ++= "\n["
   618           keys(path)
   609           result ++= keys(path.reverse)
   619           result ++= "]\n"
   610           result ++= "]\n"
   620         }
   611         }
   621 
   612 
   622         values.foreach { case (k, v) => inline_values(List(k), v) }
   613         values.foreach { case (k, v) => inline_values(List(k), v) }
   623         nodes.foreach {
   614         nodes.foreach {