# HG changeset patch
# User wenzelm
# Date 924705035 -7200
# Node ID cb8c85435228a320802d41e7b9361da98db07999
# Parent  1d13a86bfa6cc371233d36c2e8584145668caa7a
added is_current;

diff -r 1d13a86bfa6c -r cb8c85435228 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Tue Apr 20 15:23:43 1999 +0200
+++ b/src/Pure/General/path.ML	Wed Apr 21 16:30:35 1999 +0200
@@ -10,6 +10,7 @@
   datatype elem = Root | Parent | Basic of string | Variable of string
   eqtype T
   val rep: T -> elem list
+  val is_current: T -> bool
   val current: T
   val root: T
   val parent: T
@@ -59,6 +60,9 @@
 
 fun rep (Path xs) = xs;
 
+fun is_current (Path []) = true
+  | is_current _ = false;
+
 val current = Path [];
 val root = Path [Root];
 val parent = Path [Parent];