src/Pure/General/path.scala
changeset 48484 70898d016538
parent 48457 fd9e28d5a143
child 48548 49afe0e92163
equal deleted inserted replaced
48483:9bfb6978eb80 48484:70898d016538
    94       else if (es.isEmpty) (List(Root("")), Nil)
    94       else if (es.isEmpty) (List(Root("")), Nil)
    95       else (List(root_elem(es.head)), es.tail)
    95       else (List(root_elem(es.head)), es.tail)
    96     new Path(norm_elems(explode_elems(raw_elems) ++ roots))
    96     new Path(norm_elems(explode_elems(raw_elems) ++ roots))
    97   }
    97   }
    98 
    98 
       
    99   def is_ok(str: String): Boolean =
       
   100     try { explode(str); true } catch { case ERROR(_) => false }
       
   101 
    99   def split(str: String): List[Path] =
   102   def split(str: String): List[Path] =
   100     space_explode(':', str).filterNot(_.isEmpty).map(explode)
   103     space_explode(':', str).filterNot(_.isEmpty).map(explode)
   101 
   104 
   102 
   105 
   103   /* encode */
   106   /* encode */