src/Pure/General/toml.scala

 /*  Title:      Pure/General/toml.scala
-    Author: Fabian Huch, TU Muenchen
+    Author:     Fabian Huch, TU Muenchen
 
 Support for TOML: https://toml.io/en/v1.0.0
- */
+*/
+
 package isabelle
 
 
 import TOML.Parsers.Keys
 import TOML.Parse_Context.Seen

 
   /* parser */
 
   trait Parsers extends combinator.Parsers {
     type Elem = Token
-    
-    
+
+
     /* parse structure */
-    
+
     type Keys = List[Key]
 
     sealed trait V
     case class Primitive(t: T) extends V
     case class Array(rep: List[V]) extends V
     case class Inline_Table(elems: List[(Keys, V)]) extends V
 
     sealed trait Def
     case class Table(key: Keys, elems: List[(Keys, V)]) extends Def
     case class Array_Of_Tables(key: Keys, elems: List[(Keys, V)]) extends Def
-    
+
     case class File(elems: List[(Keys, V)], defs: List[Def])
-    
+
 
     /* top-level syntax structure */
-    
+
     def key: Parser[Keys] = rep1sep(keys, $$$(".")) ^^ (_.flatten)
-    
+
     def string: Parser[String] =
       elem("string", e => e.is_string || e.is_multiline_string) ^^ (s => String(s.text))
     def integer: Parser[Integer] =
       (decimal_int | binary_int | octal_int | hexadecimal_int) ^^ Integer.apply
     def float: Parser[Float] = (symbol_float | number_float) ^^ Float.apply

       $$$("[") ~>! repsep(opt(line_sep) ~> toml_value, opt(line_sep) ~ $$$(",")) <~!
         opt(line_sep) ~! opt($$$(",")) ~! opt(line_sep) <~! $$$("]") ^^ Array.apply
 
     def inline_table: Parser[Inline_Table] =
       $$$("{") ~>! repsep(pair, $$$(",")) <~! $$$("}") ^^ Inline_Table.apply
-    
+
     def pair: Parser[(Keys, V)] = (key <~! $$$("=")) ~! toml_value ^^ { case ks ~ v => (ks, v) }
 
     def table: Parser[Table] = $$$("[") ~> (key <~! $$$("]") ~! line_sep) ~! content ^^
       { case key ~ content => Table(key, content) }