# 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];