src/Pure/General/path.scala
changeset 72572 e7e93c0f6d96
parent 72464 b32eea5823c8
child 72574 d892f6d66402
--- a/src/Pure/General/path.scala	Tue Nov 10 12:48:56 2020 +0100
+++ b/src/Pure/General/path.scala	Wed Nov 11 20:55:25 2020 +0100
@@ -156,6 +156,7 @@
   def is_absolute: Boolean = elems.nonEmpty && elems.last.isInstanceOf[Path.Root]
   def is_root: Boolean = elems match { case List(Path.Root(_)) => true case _ => false }
   def is_basic: Boolean = elems match { case List(Path.Basic(_)) => true case _ => false }
+  def starts_basic: Boolean = elems.nonEmpty && elems.last.isInstanceOf[Path.Basic]
 
   def +(other: Path): Path = new Path((other.elems :\ elems)(Path.apply_elem))