src/Pure/General/path.scala
changeset 53046 cba2ddfb30c4
parent 52106 090a519982e9
child 53336 b3bf6d72fea5
--- a/src/Pure/General/path.scala	Fri Aug 16 22:57:16 2013 +0200
+++ b/src/Pure/General/path.scala	Fri Aug 16 23:11:51 2013 +0200
@@ -24,7 +24,7 @@
   private case object Parent extends Elem
 
   private def err_elem(msg: String, s: String): Nothing =
-    error (msg + " path element specification " + quote(s))
+    error(msg + " path element specification " + quote(s))
 
   private def check_elem(s: String): String =
     if (s == "" || s == "~" || s == "~~") err_elem("Illegal", s)
@@ -170,7 +170,7 @@
         case Path.Variable(s) =>
           val path = Path.explode(Isabelle_System.getenv_strict(s))
           if (path.elems.exists(_.isInstanceOf[Path.Variable]))
-            error ("Illegal path variable nesting: " + s + "=" + path.toString)
+            error("Illegal path variable nesting: " + s + "=" + path.toString)
           else path.elems
         case x => List(x)
       }