# HG changeset patch
# User wenzelm
# Date 1343991985 -7200
# Node ID 4c7932270d6da90a480931c6cee593c77fbd632d
# Parent  63ef2f0cf8bb66074bc515c746b18cb9e24214c1
reject path variable nesting explicitly;

diff -r 63ef2f0cf8bb -r 4c7932270d6d src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Fri Aug 03 12:37:31 2012 +0200
+++ b/src/Pure/General/path.ML	Fri Aug 03 13:06:25 2012 +0200
@@ -179,7 +179,12 @@
 
 (* expand variables *)
 
-fun eval (Variable s) = rep (explode_path (getenv_strict s))
+fun eval (Variable s) =
+      let val path = explode_path (getenv_strict s) in
+        if exists (fn Variable _ => true | _ => false) (rep path) then
+          error ("Illegal path variable nesting: " ^ s ^ "=" ^ print path)
+        else rep path
+      end
   | eval x = [x];
 
 val expand = rep #> maps eval #> norm #> Path;
diff -r 63ef2f0cf8bb -r 4c7932270d6d src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Fri Aug 03 12:37:31 2012 +0200
+++ b/src/Pure/General/path.scala	Fri Aug 03 13:06:25 2012 +0200
@@ -167,7 +167,10 @@
     def eval(elem: Path.Elem): List[Path.Elem] =
       elem match {
         case Path.Variable(s) =>
-          Path.explode(Isabelle_System.getenv_strict(s)).elems
+          val path = Path.explode(Isabelle_System.getenv_strict(s))
+          if (path.elems.exists(_.isInstanceOf[Path.Variable]))
+            error ("Illegal path variable nesting: " + s + "=" + path.toString)
+          else path.elems
         case x => List(x)
       }