author | wenzelm |
Sun, 30 Dec 2018 16:56:31 +0100 | |
changeset 69551 | adb52af5ba55 |
parent 69550 | 57ff523d9008 |
child 69670 | 114ae60c4be7 |
permissions | -rw-r--r-- |
43600 | 1 |
/* Title: Pure/General/path.scala |
2 |
Author: Makarius |
|
3 |
||
43601 | 4 |
Algebra of file-system paths: basic POSIX notation, extended by named |
5 |
roots (e.g. //foo) and variables (e.g. $BAR). |
|
43600 | 6 |
*/ |
7 |
||
8 |
package isabelle |
|
9 |
||
10 |
||
48409 | 11 |
import java.io.{File => JFile} |
48373 | 12 |
|
43697
77ce24aa1770
explicit Document.Node.Header, with master_dir and thy_name;
wenzelm
parents:
43670
diff
changeset
|
13 |
import scala.util.matching.Regex |
77ce24aa1770
explicit Document.Node.Header, with master_dir and thy_name;
wenzelm
parents:
43670
diff
changeset
|
14 |
|
77ce24aa1770
explicit Document.Node.Header, with master_dir and thy_name;
wenzelm
parents:
43670
diff
changeset
|
15 |
|
43600 | 16 |
object Path |
17 |
{ |
|
18 |
/* path elements */ |
|
19 |
||
45244 | 20 |
sealed abstract class Elem |
60215 | 21 |
private case class Root(name: String) extends Elem |
22 |
private case class Basic(name: String) extends Elem |
|
23 |
private case class Variable(name: String) extends Elem |
|
43600 | 24 |
private case object Parent extends Elem |
25 |
||
26 |
private def err_elem(msg: String, s: String): Nothing = |
|
69547 | 27 |
error(msg + " path element " + quote(s)) |
28 |
||
69548
415dc92050a6
more strict check: avoid confusion of Path.basic with Path.current / Path.parent;
wenzelm
parents:
69547
diff
changeset
|
29 |
private val illegal_elem = Set("", "~", "~~", ".", "..") |
69550
57ff523d9008
reject further illegal chars according to https://docs.microsoft.com/en-us/windows/desktop/fileio/naming-a-file
wenzelm
parents:
69549
diff
changeset
|
30 |
private val illegal_char = "/\\$:\"'<>|?*" |
43600 | 31 |
|
32 |
private def check_elem(s: String): String = |
|
69547 | 33 |
if (illegal_elem.contains(s)) err_elem("Illegal", s) |
52106 | 34 |
else { |
69550
57ff523d9008
reject further illegal chars according to https://docs.microsoft.com/en-us/windows/desktop/fileio/naming-a-file
wenzelm
parents:
69549
diff
changeset
|
35 |
for (c <- s) { |
57ff523d9008
reject further illegal chars according to https://docs.microsoft.com/en-us/windows/desktop/fileio/naming-a-file
wenzelm
parents:
69549
diff
changeset
|
36 |
if (c.toInt < 32) |
57ff523d9008
reject further illegal chars according to https://docs.microsoft.com/en-us/windows/desktop/fileio/naming-a-file
wenzelm
parents:
69549
diff
changeset
|
37 |
err_elem("Illegal control character " + c.toInt + " in", s) |
57ff523d9008
reject further illegal chars according to https://docs.microsoft.com/en-us/windows/desktop/fileio/naming-a-file
wenzelm
parents:
69549
diff
changeset
|
38 |
if (illegal_char.contains(c)) |
57ff523d9008
reject further illegal chars according to https://docs.microsoft.com/en-us/windows/desktop/fileio/naming-a-file
wenzelm
parents:
69549
diff
changeset
|
39 |
err_elem("Illegal character " + quote(c.toString) + " in", s) |
69547 | 40 |
} |
52106 | 41 |
s |
42 |
} |
|
43600 | 43 |
|
44 |
private def root_elem(s: String): Elem = Root(check_elem(s)) |
|
45 |
private def basic_elem(s: String): Elem = Basic(check_elem(s)) |
|
46 |
private def variable_elem(s: String): Elem = Variable(check_elem(s)) |
|
47 |
||
48 |
private def apply_elem(y: Elem, xs: List[Elem]): List[Elem] = |
|
49 |
(y, xs) match { |
|
50 |
case (Root(_), _) => List(y) |
|
51 |
case (Parent, Root(_) :: _) => xs |
|
52 |
case (Parent, Basic(_) :: rest) => rest |
|
53 |
case _ => y :: xs |
|
54 |
} |
|
55 |
||
56 |
private def norm_elems(elems: List[Elem]): List[Elem] = |
|
57 |
(elems :\ (Nil: List[Elem]))(apply_elem) |
|
58 |
||
56844 | 59 |
private def implode_elem(elem: Elem, short: Boolean): String = |
43600 | 60 |
elem match { |
61 |
case Root("") => "" |
|
62 |
case Root(s) => "//" + s |
|
63 |
case Basic(s) => s |
|
56844 | 64 |
case Variable("USER_HOME") if short => "~" |
65 |
case Variable("ISABELLE_HOME") if short => "~~" |
|
43600 | 66 |
case Variable(s) => "$" + s |
67 |
case Parent => ".." |
|
68 |
} |
|
69 |
||
70 |
||
71 |
/* path constructors */ |
|
72 |
||
45244 | 73 |
val current: Path = new Path(Nil) |
74 |
val root: Path = new Path(List(Root(""))) |
|
75 |
def named_root(s: String): Path = new Path(List(root_elem(s))) |
|
76 |
def basic(s: String): Path = new Path(List(basic_elem(s))) |
|
77 |
def variable(s: String): Path = new Path(List(variable_elem(s))) |
|
78 |
val parent: Path = new Path(List(Parent)) |
|
43600 | 79 |
|
80 |
||
81 |
/* explode */ |
|
82 |
||
83 |
def explode(str: String): Path = |
|
84 |
{ |
|
52106 | 85 |
def explode_elem(s: String): Elem = |
86 |
try { |
|
87 |
if (s == "..") Parent |
|
88 |
else if (s == "~") Variable("USER_HOME") |
|
89 |
else if (s == "~~") Variable("ISABELLE_HOME") |
|
90 |
else if (s.startsWith("$")) variable_elem(s.substring(1)) |
|
91 |
else basic_elem(s) |
|
92 |
} |
|
93 |
catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred in " + quote(str)) } |
|
94 |
||
43670
7f933761764b
prefer space_explode/split_lines as in Isabelle/ML;
wenzelm
parents:
43669
diff
changeset
|
95 |
val ss = space_explode('/', str) |
43600 | 96 |
val r = ss.takeWhile(_.isEmpty).length |
97 |
val es = ss.dropWhile(_.isEmpty) |
|
98 |
val (roots, raw_elems) = |
|
99 |
if (r == 0) (Nil, es) |
|
100 |
else if (r == 1) (List(Root("")), es) |
|
101 |
else if (es.isEmpty) (List(Root("")), Nil) |
|
102 |
else (List(root_elem(es.head)), es.tail) |
|
52106 | 103 |
val elems = raw_elems.filterNot(s => s.isEmpty || s == ".").map(explode_elem) |
104 |
||
63866 | 105 |
new Path(norm_elems(elems reverse_::: roots)) |
43600 | 106 |
} |
43669 | 107 |
|
55879
ac979f750c1a
clarified path checks: avoid crash of rendering due to spurious errors;
wenzelm
parents:
55555
diff
changeset
|
108 |
def is_wellformed(str: String): Boolean = |
48484 | 109 |
try { explode(str); true } catch { case ERROR(_) => false } |
110 |
||
55879
ac979f750c1a
clarified path checks: avoid crash of rendering due to spurious errors;
wenzelm
parents:
55555
diff
changeset
|
111 |
def is_valid(str: String): Boolean = |
ac979f750c1a
clarified path checks: avoid crash of rendering due to spurious errors;
wenzelm
parents:
55555
diff
changeset
|
112 |
try { explode(str).expand; true } catch { case ERROR(_) => false } |
ac979f750c1a
clarified path checks: avoid crash of rendering due to spurious errors;
wenzelm
parents:
55555
diff
changeset
|
113 |
|
43669 | 114 |
def split(str: String): List[Path] = |
43670
7f933761764b
prefer space_explode/split_lines as in Isabelle/ML;
wenzelm
parents:
43669
diff
changeset
|
115 |
space_explode(':', str).filterNot(_.isEmpty).map(explode) |
48457 | 116 |
|
117 |
||
118 |
/* encode */ |
|
119 |
||
120 |
val encode: XML.Encode.T[Path] = (path => XML.Encode.string(path.implode)) |
|
69551
adb52af5ba55
exclude file name components that are special on Windows;
wenzelm
parents:
69550
diff
changeset
|
121 |
|
adb52af5ba55
exclude file name components that are special on Windows;
wenzelm
parents:
69550
diff
changeset
|
122 |
|
adb52af5ba55
exclude file name components that are special on Windows;
wenzelm
parents:
69550
diff
changeset
|
123 |
/* reserved names */ |
adb52af5ba55
exclude file name components that are special on Windows;
wenzelm
parents:
69550
diff
changeset
|
124 |
|
adb52af5ba55
exclude file name components that are special on Windows;
wenzelm
parents:
69550
diff
changeset
|
125 |
private val reserved_windows: Set[String] = |
adb52af5ba55
exclude file name components that are special on Windows;
wenzelm
parents:
69550
diff
changeset
|
126 |
Set("CON", "PRN", "AUX", "NUL", |
adb52af5ba55
exclude file name components that are special on Windows;
wenzelm
parents:
69550
diff
changeset
|
127 |
"COM1", "COM2", "COM3", "COM4", "COM5", "COM6", "COM7", "COM8", "COM9", |
adb52af5ba55
exclude file name components that are special on Windows;
wenzelm
parents:
69550
diff
changeset
|
128 |
"LPT1", "LPT2", "LPT3", "LPT4", "LPT5", "LPT6", "LPT7", "LPT8", "LPT9") |
adb52af5ba55
exclude file name components that are special on Windows;
wenzelm
parents:
69550
diff
changeset
|
129 |
|
adb52af5ba55
exclude file name components that are special on Windows;
wenzelm
parents:
69550
diff
changeset
|
130 |
def is_reserved(name: String): Boolean = |
adb52af5ba55
exclude file name components that are special on Windows;
wenzelm
parents:
69550
diff
changeset
|
131 |
Long_Name.explode(name).exists(a => reserved_windows.contains(Word.uppercase(a))) |
43600 | 132 |
} |
133 |
||
43669 | 134 |
|
46712 | 135 |
final class Path private(private val elems: List[Path.Elem]) // reversed elements |
43600 | 136 |
{ |
137 |
def is_current: Boolean = elems.isEmpty |
|
59319 | 138 |
def is_absolute: Boolean = elems.nonEmpty && elems.last.isInstanceOf[Path.Root] |
65559 | 139 |
def is_root: Boolean = elems match { case List(Path.Root(_)) => true case _ => false } |
43600 | 140 |
def is_basic: Boolean = elems match { case List(Path.Basic(_)) => true case _ => false } |
141 |
||
45244 | 142 |
def +(other: Path): Path = new Path((other.elems :\ elems)(Path.apply_elem)) |
43600 | 143 |
|
144 |
||
43604 | 145 |
/* implode */ |
43600 | 146 |
|
56844 | 147 |
private def gen_implode(short: Boolean): String = |
43600 | 148 |
elems match { |
149 |
case Nil => "." |
|
150 |
case List(Path.Root("")) => "/" |
|
56844 | 151 |
case _ => elems.map(Path.implode_elem(_, short)).reverse.mkString("/") |
43600 | 152 |
} |
56844 | 153 |
def implode: String = gen_implode(false) |
154 |
def implode_short: String = gen_implode(true) |
|
43600 | 155 |
|
43652 | 156 |
override def toString: String = quote(implode) |
43600 | 157 |
|
158 |
||
159 |
/* base element */ |
|
160 |
||
161 |
private def split_path: (Path, String) = |
|
162 |
elems match { |
|
45244 | 163 |
case Path.Basic(s) :: xs => (new Path(xs), s) |
43604 | 164 |
case _ => error("Cannot split path into dir/base: " + toString) |
43600 | 165 |
} |
166 |
||
167 |
def dir: Path = split_path._1 |
|
45244 | 168 |
def base: Path = new Path(List(Path.Basic(split_path._2))) |
43600 | 169 |
|
170 |
def ext(e: String): Path = |
|
171 |
if (e == "") this |
|
172 |
else { |
|
173 |
val (prfx, s) = split_path |
|
43604 | 174 |
prfx + Path.basic(s + "." + e) |
43600 | 175 |
} |
43604 | 176 |
|
53336 | 177 |
def backup: Path = |
178 |
{ |
|
179 |
val (prfx, s) = split_path |
|
180 |
prfx + Path.basic(s + "~") |
|
181 |
} |
|
182 |
||
58610 | 183 |
def backup2: Path = |
184 |
{ |
|
185 |
val (prfx, s) = split_path |
|
186 |
prfx + Path.basic(s + "~~") |
|
187 |
} |
|
188 |
||
43697
77ce24aa1770
explicit Document.Node.Header, with master_dir and thy_name;
wenzelm
parents:
43670
diff
changeset
|
189 |
private val Ext = new Regex("(.*)\\.([^.]*)") |
77ce24aa1770
explicit Document.Node.Header, with master_dir and thy_name;
wenzelm
parents:
43670
diff
changeset
|
190 |
|
77ce24aa1770
explicit Document.Node.Header, with master_dir and thy_name;
wenzelm
parents:
43670
diff
changeset
|
191 |
def split_ext: (Path, String) = |
77ce24aa1770
explicit Document.Node.Header, with master_dir and thy_name;
wenzelm
parents:
43670
diff
changeset
|
192 |
{ |
77ce24aa1770
explicit Document.Node.Header, with master_dir and thy_name;
wenzelm
parents:
43670
diff
changeset
|
193 |
val (prefix, base) = split_path |
77ce24aa1770
explicit Document.Node.Header, with master_dir and thy_name;
wenzelm
parents:
43670
diff
changeset
|
194 |
base match { |
77ce24aa1770
explicit Document.Node.Header, with master_dir and thy_name;
wenzelm
parents:
43670
diff
changeset
|
195 |
case Ext(b, e) => (prefix + Path.basic(b), e) |
56556 | 196 |
case _ => (prefix + Path.basic(base), "") |
43697
77ce24aa1770
explicit Document.Node.Header, with master_dir and thy_name;
wenzelm
parents:
43670
diff
changeset
|
197 |
} |
77ce24aa1770
explicit Document.Node.Header, with master_dir and thy_name;
wenzelm
parents:
43670
diff
changeset
|
198 |
} |
77ce24aa1770
explicit Document.Node.Header, with master_dir and thy_name;
wenzelm
parents:
43670
diff
changeset
|
199 |
|
69367 | 200 |
def drop_ext: Path = split_ext._1 |
201 |
def get_ext: String = split_ext._2 |
|
202 |
||
43604 | 203 |
|
204 |
/* expand */ |
|
205 |
||
64228
b46969a851a9
expand relatively to given environment, notably remote HOME;
wenzelm
parents:
63866
diff
changeset
|
206 |
def expand_env(env: Map[String, String]): Path = |
43604 | 207 |
{ |
208 |
def eval(elem: Path.Elem): List[Path.Elem] = |
|
209 |
elem match { |
|
43664 | 210 |
case Path.Variable(s) => |
64228
b46969a851a9
expand relatively to given environment, notably remote HOME;
wenzelm
parents:
63866
diff
changeset
|
211 |
val path = Path.explode(Isabelle_System.getenv_strict(s, env)) |
48658 | 212 |
if (path.elems.exists(_.isInstanceOf[Path.Variable])) |
53046 | 213 |
error("Illegal path variable nesting: " + s + "=" + path.toString) |
48658 | 214 |
else path.elems |
43604 | 215 |
case x => List(x) |
216 |
} |
|
217 |
||
45244 | 218 |
new Path(Path.norm_elems(elems.map(eval).flatten)) |
43604 | 219 |
} |
48373 | 220 |
|
64228
b46969a851a9
expand relatively to given environment, notably remote HOME;
wenzelm
parents:
63866
diff
changeset
|
221 |
def expand: Path = expand_env(Isabelle_System.settings()) |
b46969a851a9
expand relatively to given environment, notably remote HOME;
wenzelm
parents:
63866
diff
changeset
|
222 |
|
69366 | 223 |
def file_name: String = expand.base.implode |
224 |
||
48373 | 225 |
|
48548 | 226 |
/* source position */ |
227 |
||
228 |
def position: Position.T = Position.File(implode) |
|
229 |
||
230 |
||
66232 | 231 |
/* platform files */ |
48373 | 232 |
|
60988 | 233 |
def file: JFile = File.platform_file(this) |
48548 | 234 |
def is_file: Boolean = file.isFile |
235 |
def is_dir: Boolean = file.isDirectory |
|
65833 | 236 |
|
66232 | 237 |
def absolute_file: JFile = File.absolute(file) |
238 |
def canonical_file: JFile = File.canonical(file) |
|
67181 | 239 |
|
240 |
def absolute: Path = File.path(absolute_file) |
|
241 |
def canonical: Path = File.path(canonical_file) |
|
43600 | 242 |
} |