added is_current;
authorwenzelm
Wed Apr 21 16:30:35 1999 +0200 (1999-04-21)
changeset 6460cb8c85435228
parent 6459 1d13a86bfa6c
child 6461 99c34e50a2c6
added is_current;
src/Pure/General/path.ML
     1.1 --- a/src/Pure/General/path.ML	Tue Apr 20 15:23:43 1999 +0200
     1.2 +++ b/src/Pure/General/path.ML	Wed Apr 21 16:30:35 1999 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4    datatype elem = Root | Parent | Basic of string | Variable of string
     1.5    eqtype T
     1.6    val rep: T -> elem list
     1.7 +  val is_current: T -> bool
     1.8    val current: T
     1.9    val root: T
    1.10    val parent: T
    1.11 @@ -59,6 +60,9 @@
    1.12  
    1.13  fun rep (Path xs) = xs;
    1.14  
    1.15 +fun is_current (Path []) = true
    1.16 +  | is_current _ = false;
    1.17 +
    1.18  val current = Path [];
    1.19  val root = Path [Root];
    1.20  val parent = Path [Parent];