# HG changeset patch
# User wenzelm
# Date 1689191234 -7200
# Node ID fcabbb45b2724a529bda1ea3328e7141ab4cea35
# Parent  be8aaaa4ac253349fa8833d06a8613ef9c16724c
tuned whitespace;

diff -r be8aaaa4ac25 -r fcabbb45b272 src/Pure/General/toml.scala
--- a/src/Pure/General/toml.scala	Wed Jul 12 21:07:21 2023 +0200
+++ b/src/Pure/General/toml.scala	Wed Jul 12 21:47:14 2023 +0200
@@ -1,8 +1,9 @@
 /*  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
 
 
@@ -229,10 +230,10 @@
 
   trait Parsers extends combinator.Parsers {
     type Elem = Token
-    
-    
+
+
     /* parse structure */
-    
+
     type Keys = List[Key]
 
     sealed trait V
@@ -243,14 +244,14 @@
     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] =
@@ -275,7 +276,7 @@
 
     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 ^^