src/Pure/General/path.ML

 signature PATH =
 sig
   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
   val basic: string -> T
   val variable: string -> T

 (* type path *)
 
 datatype T = Path of elem list;
 
 fun rep (Path xs) = xs;
+
+fun is_current (Path []) = true
+  | is_current _ = false;
 
 val current = Path [];
 val root = Path [Root];
 val parent = Path [Parent];
 fun basic s = Path [basic_elem (explode s)];