1 /* Title: Pure/General/path.scala
4 Algebra of file-system paths: basic POSIX notation, extended by named
5 roots (e.g. //foo) and variables (e.g. $BAR).
11 import java.io.{File => JFile}
13 import scala.util.matching.Regex
20 sealed abstract class Elem
21 private case class Root(val name: String) extends Elem
22 private case class Basic(val name: String) extends Elem
23 private case class Variable(val name: String) extends Elem
24 private case object Parent extends Elem
26 private def err_elem(msg: String, s: String): Nothing =
27 error (msg + " path element specification: " + quote(s))
29 private def check_elem(s: String): String =
30 if (s == "" || s == "~" || s == "~~") err_elem("Illegal", s)
32 s.iterator.filter(c => c == '/' || c == '\\' || c == '$' || c == ':').toList match {
35 err_elem ("Illegal character(s) " + commas_quote(bads.map(_.toString)) + " in", s)
38 private def root_elem(s: String): Elem = Root(check_elem(s))
39 private def basic_elem(s: String): Elem = Basic(check_elem(s))
40 private def variable_elem(s: String): Elem = Variable(check_elem(s))
42 private def apply_elem(y: Elem, xs: List[Elem]): List[Elem] =
44 case (Root(_), _) => List(y)
45 case (Parent, Root(_) :: _) => xs
46 case (Parent, Basic(_) :: rest) => rest
50 private def norm_elems(elems: List[Elem]): List[Elem] =
51 (elems :\ (Nil: List[Elem]))(apply_elem)
53 private def implode_elem(elem: Elem): String =
56 case Root(s) => "//" + s
58 case Variable(s) => "$" + s
63 /* path constructors */
65 val current: Path = new Path(Nil)
66 val root: Path = new Path(List(Root("")))
67 def named_root(s: String): Path = new Path(List(root_elem(s)))
68 def basic(s: String): Path = new Path(List(basic_elem(s)))
69 def variable(s: String): Path = new Path(List(variable_elem(s)))
70 val parent: Path = new Path(List(Parent))
75 private def explode_elem(s: String): Elem =
77 else if (s == "~") Variable("USER_HOME")
78 else if (s == "~~") Variable("ISABELLE_HOME")
79 else if (s.startsWith("$")) variable_elem(s.substring(1))
82 private def explode_elems(ss: List[String]): List[Elem] =
83 ss.filterNot(s => s.isEmpty || s == ".").map(explode_elem).reverse
85 def explode(str: String): Path =
87 val ss = space_explode('/', str)
88 val r = ss.takeWhile(_.isEmpty).length
89 val es = ss.dropWhile(_.isEmpty)
90 val (roots, raw_elems) =
92 else if (r == 1) (List(Root("")), es)
93 else if (es.isEmpty) (List(Root("")), Nil)
94 else (List(root_elem(es.head)), es.tail)
95 new Path(norm_elems(explode_elems(raw_elems) ++ roots))
98 def split(str: String): List[Path] =
99 space_explode(':', str).filterNot(_.isEmpty).map(explode)
103 final class Path private(private val elems: List[Path.Elem]) // reversed elements
105 def is_current: Boolean = elems.isEmpty
106 def is_absolute: Boolean = !elems.isEmpty && elems.last.isInstanceOf[Path.Root]
107 def is_basic: Boolean = elems match { case List(Path.Basic(_)) => true case _ => false }
109 def +(other: Path): Path = new Path((other.elems :\ elems)(Path.apply_elem))
114 def implode: String =
117 case List(Path.Root("")) => "/"
118 case _ => elems.map(Path.implode_elem).reverse.mkString("/")
121 override def toString: String = quote(implode)
126 private def split_path: (Path, String) =
128 case Path.Basic(s) :: xs => (new Path(xs), s)
129 case _ => error("Cannot split path into dir/base: " + toString)
132 def dir: Path = split_path._1
133 def base: Path = new Path(List(Path.Basic(split_path._2)))
135 def ext(e: String): Path =
138 val (prfx, s) = split_path
139 prfx + Path.basic(s + "." + e)
142 private val Ext = new Regex("(.*)\\.([^.]*)")
144 def split_ext: (Path, String) =
146 val (prefix, base) = split_path
148 case Ext(b, e) => (prefix + Path.basic(b), e)
149 case _ => (Path.basic(base), "")
158 def eval(elem: Path.Elem): List[Path.Elem] =
160 case Path.Variable(s) =>
161 Path.explode(Isabelle_System.getenv_strict(s)).elems
165 new Path(Path.norm_elems(elems.map(eval).flatten))
171 def file: JFile = Isabelle_System.platform_file(this)