author | wenzelm |
Thu, 18 Aug 2011 17:53:32 +0200 | |
changeset 44270 | 3eaad39e520c |
parent 43697 | 77ce24aa1770 |
child 45244 | c149b61bc372 |
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 |
||
43697
77ce24aa1770
explicit Document.Node.Header, with master_dir and thy_name;
wenzelm
parents:
43670
diff
changeset
|
11 |
import scala.util.matching.Regex |
77ce24aa1770
explicit Document.Node.Header, with master_dir and thy_name;
wenzelm
parents:
43670
diff
changeset
|
12 |
|
77ce24aa1770
explicit Document.Node.Header, with master_dir and thy_name;
wenzelm
parents:
43670
diff
changeset
|
13 |
|
43600 | 14 |
object Path |
15 |
{ |
|
16 |
/* path elements */ |
|
17 |
||
18 |
private sealed abstract class Elem |
|
19 |
private case class Root(val name: String) extends Elem |
|
20 |
private case class Basic(val name: String) extends Elem |
|
21 |
private case class Variable(val name: String) extends Elem |
|
22 |
private case object Parent extends Elem |
|
23 |
||
24 |
private def err_elem(msg: String, s: String): Nothing = |
|
43652 | 25 |
error (msg + " path element specification: " + quote(s)) |
43600 | 26 |
|
27 |
private def check_elem(s: String): String = |
|
28 |
if (s == "" || s == "~" || s == "~~") err_elem("Illegal", s) |
|
29 |
else |
|
30 |
s.iterator.filter(c => c == '/' || c == '\\' || c == '$' || c == ':').toList match { |
|
31 |
case Nil => s |
|
32 |
case bads => |
|
43652 | 33 |
err_elem ("Illegal character(s) " + commas_quote(bads.map(_.toString)) + " in", s) |
43600 | 34 |
} |
35 |
||
36 |
private def root_elem(s: String): Elem = Root(check_elem(s)) |
|
37 |
private def basic_elem(s: String): Elem = Basic(check_elem(s)) |
|
38 |
private def variable_elem(s: String): Elem = Variable(check_elem(s)) |
|
39 |
||
40 |
private def apply_elem(y: Elem, xs: List[Elem]): List[Elem] = |
|
41 |
(y, xs) match { |
|
42 |
case (Root(_), _) => List(y) |
|
43 |
case (Parent, Root(_) :: _) => xs |
|
44 |
case (Parent, Basic(_) :: rest) => rest |
|
45 |
case _ => y :: xs |
|
46 |
} |
|
47 |
||
48 |
private def norm_elems(elems: List[Elem]): List[Elem] = |
|
49 |
(elems :\ (Nil: List[Elem]))(apply_elem) |
|
50 |
||
51 |
private def implode_elem(elem: Elem): String = |
|
52 |
elem match { |
|
53 |
case Root("") => "" |
|
54 |
case Root(s) => "//" + s |
|
55 |
case Basic(s) => s |
|
56 |
case Variable(s) => "$" + s |
|
57 |
case Parent => ".." |
|
58 |
} |
|
59 |
||
60 |
||
61 |
/* path constructors */ |
|
62 |
||
63 |
private def apply(xs: List[Elem]): Path = |
|
64 |
new Path { override val elems = xs } |
|
65 |
||
66 |
val current: Path = Path(Nil) |
|
67 |
val root: Path = Path(List(Root(""))) |
|
68 |
def named_root(s: String): Path = Path(List(root_elem(s))) |
|
69 |
def basic(s: String): Path = Path(List(basic_elem(s))) |
|
70 |
def variable(s: String): Path = Path(List(variable_elem(s))) |
|
71 |
val parent: Path = Path(List(Parent)) |
|
72 |
||
73 |
||
74 |
/* explode */ |
|
75 |
||
76 |
private def explode_elem(s: String): Elem = |
|
77 |
if (s == "..") Parent |
|
78 |
else if (s == "~") Variable("HOME") |
|
79 |
else if (s == "~~") Variable("ISABELLE_HOME") |
|
80 |
else if (s.startsWith("$")) variable_elem(s.substring(1)) |
|
81 |
else basic_elem(s) |
|
82 |
||
83 |
private def explode_elems(ss: List[String]): List[Elem] = |
|
84 |
ss.filterNot(s => s.isEmpty || s == ".").map(explode_elem).reverse |
|
85 |
||
86 |
def explode(str: String): Path = |
|
87 |
{ |
|
43670
7f933761764b
prefer space_explode/split_lines as in Isabelle/ML;
wenzelm
parents:
43669
diff
changeset
|
88 |
val ss = space_explode('/', str) |
43600 | 89 |
val r = ss.takeWhile(_.isEmpty).length |
90 |
val es = ss.dropWhile(_.isEmpty) |
|
91 |
val (roots, raw_elems) = |
|
92 |
if (r == 0) (Nil, es) |
|
93 |
else if (r == 1) (List(Root("")), es) |
|
94 |
else if (es.isEmpty) (List(Root("")), Nil) |
|
95 |
else (List(root_elem(es.head)), es.tail) |
|
96 |
Path(norm_elems(explode_elems(raw_elems) ++ roots)) |
|
97 |
} |
|
43669 | 98 |
|
99 |
def split(str: String): List[Path] = |
|
43670
7f933761764b
prefer space_explode/split_lines as in Isabelle/ML;
wenzelm
parents:
43669
diff
changeset
|
100 |
space_explode(':', str).filterNot(_.isEmpty).map(explode) |
43600 | 101 |
} |
102 |
||
43669 | 103 |
|
43600 | 104 |
class Path |
105 |
{ |
|
106 |
protected val elems: List[Path.Elem] = Nil // reversed elements |
|
107 |
||
108 |
def is_current: Boolean = elems.isEmpty |
|
109 |
def is_absolute: Boolean = !elems.isEmpty && elems.last.isInstanceOf[Path.Root] |
|
110 |
def is_basic: Boolean = elems match { case List(Path.Basic(_)) => true case _ => false } |
|
111 |
||
43605 | 112 |
def +(other: Path): Path = Path((other.elems :\ elems)(Path.apply_elem)) |
43600 | 113 |
|
114 |
||
43604 | 115 |
/* implode */ |
43600 | 116 |
|
43604 | 117 |
def implode: String = |
43600 | 118 |
elems match { |
119 |
case Nil => "." |
|
120 |
case List(Path.Root("")) => "/" |
|
43604 | 121 |
case _ => elems.map(Path.implode_elem).reverse.mkString("/") |
43600 | 122 |
} |
123 |
||
43652 | 124 |
override def toString: String = quote(implode) |
43600 | 125 |
|
126 |
||
127 |
/* base element */ |
|
128 |
||
129 |
private def split_path: (Path, String) = |
|
130 |
elems match { |
|
131 |
case Path.Basic(s) :: xs => (Path(xs), s) |
|
43604 | 132 |
case _ => error("Cannot split path into dir/base: " + toString) |
43600 | 133 |
} |
134 |
||
135 |
def dir: Path = split_path._1 |
|
136 |
def base: Path = Path(List(Path.Basic(split_path._2))) |
|
137 |
||
138 |
def ext(e: String): Path = |
|
139 |
if (e == "") this |
|
140 |
else { |
|
141 |
val (prfx, s) = split_path |
|
43604 | 142 |
prfx + Path.basic(s + "." + e) |
43600 | 143 |
} |
43604 | 144 |
|
43697
77ce24aa1770
explicit Document.Node.Header, with master_dir and thy_name;
wenzelm
parents:
43670
diff
changeset
|
145 |
private val Ext = new Regex("(.*)\\.([^.]*)") |
77ce24aa1770
explicit Document.Node.Header, with master_dir and thy_name;
wenzelm
parents:
43670
diff
changeset
|
146 |
|
77ce24aa1770
explicit Document.Node.Header, with master_dir and thy_name;
wenzelm
parents:
43670
diff
changeset
|
147 |
def split_ext: (Path, String) = |
77ce24aa1770
explicit Document.Node.Header, with master_dir and thy_name;
wenzelm
parents:
43670
diff
changeset
|
148 |
{ |
77ce24aa1770
explicit Document.Node.Header, with master_dir and thy_name;
wenzelm
parents:
43670
diff
changeset
|
149 |
val (prefix, base) = split_path |
77ce24aa1770
explicit Document.Node.Header, with master_dir and thy_name;
wenzelm
parents:
43670
diff
changeset
|
150 |
base match { |
77ce24aa1770
explicit Document.Node.Header, with master_dir and thy_name;
wenzelm
parents:
43670
diff
changeset
|
151 |
case Ext(b, e) => (prefix + Path.basic(b), e) |
77ce24aa1770
explicit Document.Node.Header, with master_dir and thy_name;
wenzelm
parents:
43670
diff
changeset
|
152 |
case _ => (Path.basic(base), "") |
77ce24aa1770
explicit Document.Node.Header, with master_dir and thy_name;
wenzelm
parents:
43670
diff
changeset
|
153 |
} |
77ce24aa1770
explicit Document.Node.Header, with master_dir and thy_name;
wenzelm
parents:
43670
diff
changeset
|
154 |
} |
77ce24aa1770
explicit Document.Node.Header, with master_dir and thy_name;
wenzelm
parents:
43670
diff
changeset
|
155 |
|
43604 | 156 |
|
157 |
/* expand */ |
|
158 |
||
43664 | 159 |
def expand: Path = |
43604 | 160 |
{ |
161 |
def eval(elem: Path.Elem): List[Path.Elem] = |
|
162 |
elem match { |
|
43664 | 163 |
case Path.Variable(s) => |
164 |
Path.explode(Isabelle_System.getenv_strict(s)).elems |
|
43604 | 165 |
case x => List(x) |
166 |
} |
|
167 |
||
168 |
Path(Path.norm_elems(elems.map(eval).flatten)) |
|
169 |
} |
|
43600 | 170 |
} |