# HG changeset patch
# User wenzelm
# Date 1376687511 -7200
# Node ID cba2ddfb30c47192ecfbb531494a423125a1bb8b
# Parent  4c297ee47c28ca475ed612d62ab2b26d107c089f
tuned;

diff -r 4c297ee47c28 -r cba2ddfb30c4 src/Pure/General/path.scala
--- 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)
       }