tuned whitespace;

--- a/src/Pure/General/symbol.scala	Thu Apr 20 10:35:00 2017 +0200
+++ b/src/Pure/General/symbol.scala	Thu Apr 20 11:33:36 2017 +0200
@@ -216,7 +216,6 @@
         { case (List(a), Nil) => File(a) }))
     }
 
-
     def apply(text: CharSequence): Text_Chunk =
       new Text_Chunk(Text.Range(0, text.length), Index(text))
   }