wenzelm@44473
|
1 |
/* Title: Pure/General/path.scala
|
wenzelm@44473
|
2 |
Author: Makarius
|
wenzelm@44473
|
3 |
|
wenzelm@44474
|
4 |
Algebra of file-system paths: basic POSIX notation, extended by named
|
wenzelm@44474
|
5 |
roots (e.g. //foo) and variables (e.g. $BAR).
|
wenzelm@44473
|
6 |
*/
|
wenzelm@44473
|
7 |
|
wenzelm@44473
|
8 |
package isabelle
|
wenzelm@44473
|
9 |
|
wenzelm@44473
|
10 |
|
wenzelm@49424
|
11 |
import java.io.{File => JFile}
|
wenzelm@49388
|
12 |
|
wenzelm@44571
|
13 |
import scala.util.matching.Regex
|
wenzelm@44571
|
14 |
|
wenzelm@44571
|
15 |
|
wenzelm@44473
|
16 |
object Path
|
wenzelm@44473
|
17 |
{
|
wenzelm@44473
|
18 |
/* path elements */
|
wenzelm@44473
|
19 |
|
wenzelm@46115
|
20 |
sealed abstract class Elem
|
wenzelm@44473
|
21 |
private case class Root(val name: String) extends Elem
|
wenzelm@44473
|
22 |
private case class Basic(val name: String) extends Elem
|
wenzelm@44473
|
23 |
private case class Variable(val name: String) extends Elem
|
wenzelm@44473
|
24 |
private case object Parent extends Elem
|
wenzelm@44473
|
25 |
|
wenzelm@44473
|
26 |
private def err_elem(msg: String, s: String): Nothing =
|
wenzelm@44529
|
27 |
error (msg + " path element specification: " + quote(s))
|
wenzelm@44473
|
28 |
|
wenzelm@44473
|
29 |
private def check_elem(s: String): String =
|
wenzelm@44473
|
30 |
if (s == "" || s == "~" || s == "~~") err_elem("Illegal", s)
|
wenzelm@44473
|
31 |
else
|
wenzelm@44473
|
32 |
s.iterator.filter(c => c == '/' || c == '\\' || c == '$' || c == ':').toList match {
|
wenzelm@44473
|
33 |
case Nil => s
|
wenzelm@44473
|
34 |
case bads =>
|
wenzelm@44529
|
35 |
err_elem ("Illegal character(s) " + commas_quote(bads.map(_.toString)) + " in", s)
|
wenzelm@44473
|
36 |
}
|
wenzelm@44473
|
37 |
|
wenzelm@44473
|
38 |
private def root_elem(s: String): Elem = Root(check_elem(s))
|
wenzelm@44473
|
39 |
private def basic_elem(s: String): Elem = Basic(check_elem(s))
|
wenzelm@44473
|
40 |
private def variable_elem(s: String): Elem = Variable(check_elem(s))
|
wenzelm@44473
|
41 |
|
wenzelm@44473
|
42 |
private def apply_elem(y: Elem, xs: List[Elem]): List[Elem] =
|
wenzelm@44473
|
43 |
(y, xs) match {
|
wenzelm@44473
|
44 |
case (Root(_), _) => List(y)
|
wenzelm@44473
|
45 |
case (Parent, Root(_) :: _) => xs
|
wenzelm@44473
|
46 |
case (Parent, Basic(_) :: rest) => rest
|
wenzelm@44473
|
47 |
case _ => y :: xs
|
wenzelm@44473
|
48 |
}
|
wenzelm@44473
|
49 |
|
wenzelm@44473
|
50 |
private def norm_elems(elems: List[Elem]): List[Elem] =
|
wenzelm@44473
|
51 |
(elems :\ (Nil: List[Elem]))(apply_elem)
|
wenzelm@44473
|
52 |
|
wenzelm@44473
|
53 |
private def implode_elem(elem: Elem): String =
|
wenzelm@44473
|
54 |
elem match {
|
wenzelm@44473
|
55 |
case Root("") => ""
|
wenzelm@44473
|
56 |
case Root(s) => "//" + s
|
wenzelm@44473
|
57 |
case Basic(s) => s
|
wenzelm@44473
|
58 |
case Variable(s) => "$" + s
|
wenzelm@44473
|
59 |
case Parent => ".."
|
wenzelm@44473
|
60 |
}
|
wenzelm@44473
|
61 |
|
wenzelm@44473
|
62 |
|
wenzelm@44473
|
63 |
/* path constructors */
|
wenzelm@44473
|
64 |
|
wenzelm@46115
|
65 |
val current: Path = new Path(Nil)
|
wenzelm@46115
|
66 |
val root: Path = new Path(List(Root("")))
|
wenzelm@46115
|
67 |
def named_root(s: String): Path = new Path(List(root_elem(s)))
|
wenzelm@46115
|
68 |
def basic(s: String): Path = new Path(List(basic_elem(s)))
|
wenzelm@46115
|
69 |
def variable(s: String): Path = new Path(List(variable_elem(s)))
|
wenzelm@46115
|
70 |
val parent: Path = new Path(List(Parent))
|
wenzelm@44473
|
71 |
|
wenzelm@44473
|
72 |
|
wenzelm@44473
|
73 |
/* explode */
|
wenzelm@44473
|
74 |
|
wenzelm@44473
|
75 |
private def explode_elem(s: String): Elem =
|
wenzelm@44473
|
76 |
if (s == "..") Parent
|
wenzelm@48538
|
77 |
else if (s == "~") Variable("USER_HOME")
|
wenzelm@44473
|
78 |
else if (s == "~~") Variable("ISABELLE_HOME")
|
wenzelm@44473
|
79 |
else if (s.startsWith("$")) variable_elem(s.substring(1))
|
wenzelm@44473
|
80 |
else basic_elem(s)
|
wenzelm@44473
|
81 |
|
wenzelm@44473
|
82 |
private def explode_elems(ss: List[String]): List[Elem] =
|
wenzelm@44473
|
83 |
ss.filterNot(s => s.isEmpty || s == ".").map(explode_elem).reverse
|
wenzelm@44473
|
84 |
|
wenzelm@44473
|
85 |
def explode(str: String): Path =
|
wenzelm@44473
|
86 |
{
|
wenzelm@44545
|
87 |
val ss = space_explode('/', str)
|
wenzelm@44473
|
88 |
val r = ss.takeWhile(_.isEmpty).length
|
wenzelm@44473
|
89 |
val es = ss.dropWhile(_.isEmpty)
|
wenzelm@44473
|
90 |
val (roots, raw_elems) =
|
wenzelm@44473
|
91 |
if (r == 0) (Nil, es)
|
wenzelm@44473
|
92 |
else if (r == 1) (List(Root("")), es)
|
wenzelm@44473
|
93 |
else if (es.isEmpty) (List(Root("")), Nil)
|
wenzelm@44473
|
94 |
else (List(root_elem(es.head)), es.tail)
|
wenzelm@46115
|
95 |
new Path(norm_elems(explode_elems(raw_elems) ++ roots))
|
wenzelm@44473
|
96 |
}
|
wenzelm@44544
|
97 |
|
wenzelm@44544
|
98 |
def split(str: String): List[Path] =
|
wenzelm@44545
|
99 |
space_explode(':', str).filterNot(_.isEmpty).map(explode)
|
wenzelm@44473
|
100 |
}
|
wenzelm@44473
|
101 |
|
wenzelm@44544
|
102 |
|
wenzelm@47583
|
103 |
final class Path private(private val elems: List[Path.Elem]) // reversed elements
|
wenzelm@44473
|
104 |
{
|
wenzelm@44473
|
105 |
def is_current: Boolean = elems.isEmpty
|
wenzelm@44473
|
106 |
def is_absolute: Boolean = !elems.isEmpty && elems.last.isInstanceOf[Path.Root]
|
wenzelm@44473
|
107 |
def is_basic: Boolean = elems match { case List(Path.Basic(_)) => true case _ => false }
|
wenzelm@44473
|
108 |
|
wenzelm@46115
|
109 |
def +(other: Path): Path = new Path((other.elems :\ elems)(Path.apply_elem))
|
wenzelm@44473
|
110 |
|
wenzelm@44473
|
111 |
|
wenzelm@44477
|
112 |
/* implode */
|
wenzelm@44473
|
113 |
|
wenzelm@44477
|
114 |
def implode: String =
|
wenzelm@44473
|
115 |
elems match {
|
wenzelm@44473
|
116 |
case Nil => "."
|
wenzelm@44473
|
117 |
case List(Path.Root("")) => "/"
|
wenzelm@44477
|
118 |
case _ => elems.map(Path.implode_elem).reverse.mkString("/")
|
wenzelm@44473
|
119 |
}
|
wenzelm@44473
|
120 |
|
wenzelm@44529
|
121 |
override def toString: String = quote(implode)
|
wenzelm@44473
|
122 |
|
wenzelm@44473
|
123 |
|
wenzelm@44473
|
124 |
/* base element */
|
wenzelm@44473
|
125 |
|
wenzelm@44473
|
126 |
private def split_path: (Path, String) =
|
wenzelm@44473
|
127 |
elems match {
|
wenzelm@46115
|
128 |
case Path.Basic(s) :: xs => (new Path(xs), s)
|
wenzelm@44477
|
129 |
case _ => error("Cannot split path into dir/base: " + toString)
|
wenzelm@44473
|
130 |
}
|
wenzelm@44473
|
131 |
|
wenzelm@44473
|
132 |
def dir: Path = split_path._1
|
wenzelm@46115
|
133 |
def base: Path = new Path(List(Path.Basic(split_path._2)))
|
wenzelm@44473
|
134 |
|
wenzelm@44473
|
135 |
def ext(e: String): Path =
|
wenzelm@44473
|
136 |
if (e == "") this
|
wenzelm@44473
|
137 |
else {
|
wenzelm@44473
|
138 |
val (prfx, s) = split_path
|
wenzelm@44477
|
139 |
prfx + Path.basic(s + "." + e)
|
wenzelm@44473
|
140 |
}
|
wenzelm@44477
|
141 |
|
wenzelm@44571
|
142 |
private val Ext = new Regex("(.*)\\.([^.]*)")
|
wenzelm@44571
|
143 |
|
wenzelm@44571
|
144 |
def split_ext: (Path, String) =
|
wenzelm@44571
|
145 |
{
|
wenzelm@44571
|
146 |
val (prefix, base) = split_path
|
wenzelm@44571
|
147 |
base match {
|
wenzelm@44571
|
148 |
case Ext(b, e) => (prefix + Path.basic(b), e)
|
wenzelm@44571
|
149 |
case _ => (Path.basic(base), "")
|
wenzelm@44571
|
150 |
}
|
wenzelm@44571
|
151 |
}
|
wenzelm@44571
|
152 |
|
wenzelm@44477
|
153 |
|
wenzelm@44477
|
154 |
/* expand */
|
wenzelm@44477
|
155 |
|
wenzelm@44539
|
156 |
def expand: Path =
|
wenzelm@44477
|
157 |
{
|
wenzelm@44477
|
158 |
def eval(elem: Path.Elem): List[Path.Elem] =
|
wenzelm@44477
|
159 |
elem match {
|
wenzelm@44539
|
160 |
case Path.Variable(s) =>
|
wenzelm@44539
|
161 |
Path.explode(Isabelle_System.getenv_strict(s)).elems
|
wenzelm@44477
|
162 |
case x => List(x)
|
wenzelm@44477
|
163 |
}
|
wenzelm@44477
|
164 |
|
wenzelm@46115
|
165 |
new Path(Path.norm_elems(elems.map(eval).flatten))
|
wenzelm@44477
|
166 |
}
|
wenzelm@49388
|
167 |
|
wenzelm@49388
|
168 |
|
wenzelm@49388
|
169 |
/* platform file */
|
wenzelm@49388
|
170 |
|
wenzelm@49424
|
171 |
def file: JFile = Isabelle_System.platform_file(this)
|
wenzelm@44473
|
172 |
}
|