tuned;
authorwenzelm
Fri, 16 Aug 2013 23:11:51 +0200
changeset 53046 cba2ddfb30c4
parent 53045 4c297ee47c28
child 53047 8dceafa07c4f
tuned;
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)
       }