added is_base;
authorwenzelm
Thu, 04 Dec 1997 13:50:43 +0100
changeset 4365 fbb275398eb7
parent 4364 ab73573067d6
child 4366 4d84cdb0df42
added is_base;
src/Pure/Thy/path.ML
--- a/src/Pure/Thy/path.ML	Thu Dec 04 13:50:18 1997 +0100
+++ b/src/Pure/Thy/path.ML	Thu Dec 04 13:50:43 1997 +0100
@@ -20,6 +20,7 @@
   val evaluate: (string -> T) -> T -> T
   val expand: (string -> string) -> string -> string
   val base_name: string -> string
+  val is_base: string -> bool
 end;
 
 structure Path: PATH =
@@ -96,5 +97,8 @@
 
 val base_name = base o unpack;
 
+fun is_base str =
+  not (exists (equal "/" orf equal "$") (explode str));
+
 
 end;