src/Pure/General/path.scala

 import java.nio.file.{Path => JPath}
 
 import scala.util.matching.Regex
 
 
-object Path
-{
+object Path {
   /* path elements */
 
   sealed abstract class Elem
   private case class Root(name: String) extends Elem
   private case class Basic(name: String) extends Elem

   val ISABELLE_HOME: Path = variable("ISABELLE_HOME")
 
 
   /* explode */
 
-  def explode(str: String): Path =
-  {
+  def explode(str: String): Path = {
     def explode_elem(s: String): Elem =
       try {
         if (s == "..") Parent
         else if (s == "~") Variable("USER_HOME")
         else if (s == "~~") Variable("ISABELLE_HOME")

     Long_Name.explode(name).exists(a => reserved_windows.contains(Word.uppercase(a)))
 
 
   /* case-insensitive names */
 
-  def check_case_insensitive(paths: List[Path]): Unit =
-  {
+  def check_case_insensitive(paths: List[Path]): Unit = {
     val table =
       paths.foldLeft(Multi_Map.empty[String, String]) { case (tab, path) =>
         val name = path.expand.implode
         tab.insert(Word.lowercase(name), name)
       }

     }
   }
 }
 
 
-final class Path private(protected val elems: List[Path.Elem]) // reversed elements
-{
+final class Path private(
+  protected val elems: List[Path.Elem]  // reversed elements
+) {
   override def hashCode: Int = elems.hashCode
   override def equals(that: Any): Boolean =
     that match {
       case other: Path => elems == other.elems
       case _ => false

   def log: Path = ext("log")
   def orig: Path = ext("orig")
   def patch: Path = ext("patch")
   def shasum: Path = ext("shasum")
 
-  def backup: Path =
-  {
+  def backup: Path = {
     val (prfx, s) = split_path
     prfx + Path.basic(s + "~")
   }
 
-  def backup2: Path =
-  {
+  def backup2: Path = {
     val (prfx, s) = split_path
     prfx + Path.basic(s + "~~")
   }
 
   def exe: Path = ext("exe")
   def platform_exe: Path = if (Platform.is_windows) exe else this
 
   private val Ext = new Regex("(.*)\\.([^.]*)")
 
-  def split_ext: (Path, String) =
-  {
+  def split_ext: (Path, String) = {
     val (prefix, base) = split_path
     base match {
       case Ext(b, e) => (prefix + Path.basic(b), e)
       case _ => (prefix + Path.basic(base), "")
     }

   def squash: Path = new Path(elems.map(elem => Path.Basic(Path.squash_elem(elem))))
 
 
   /* expand */
 
-  def expand_env(env: JMap[String, String]): Path =
-  {
+  def expand_env(env: JMap[String, String]): Path = {
     def eval(elem: Path.Elem): List[Path.Elem] =
       elem match {
         case Path.Variable(s) =>
           val path = Path.explode(Isabelle_System.getenv_strict(s, env))
           if (path.elems.exists(_.isInstanceOf[Path.Variable]))

   def file_name: String = expand.base.implode
 
 
   /* implode wrt. given directories */
 
-  def implode_symbolic: String =
-  {
+  def implode_symbolic: String = {
     val directories =
       Library.space_explode(':', Isabelle_System.getenv("ISABELLE_DIRECTORIES")).reverse
     val full_name = expand.implode
     directories.view.flatMap(a =>
       try {