1/* Title: Pure/General/path.scala 2 Author: Makarius 3 4Algebra of file-system paths: basic POSIX notation, extended by named 5roots (e.g. //foo) and variables (e.g. $BAR). 6*/ 7 8package isabelle 9 10 11import java.io.{File => JFile} 12 13import scala.util.matching.Regex 14 15 16object Path 17{ 18 /* path elements */ 19 20 sealed abstract class Elem 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 24 private case object Parent extends Elem 25 26 private def err_elem(msg: String, s: String): Nothing = 27 error(msg + " path element specification " + quote(s)) 28 29 private def check_elem(s: String): String = 30 if (s == "" || s == "~" || s == "~~") err_elem("Illegal", s) 31 else { 32 "/\\$:\"'".iterator.foreach(c => 33 if (s.iterator.contains(c)) 34 err_elem("Illegal character " + quote(c.toString) + " in", s)) 35 s 36 } 37 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)) 41 42 private def apply_elem(y: Elem, xs: List[Elem]): List[Elem] = 43 (y, xs) match { 44 case (Root(_), _) => List(y) 45 case (Parent, Root(_) :: _) => xs 46 case (Parent, Basic(_) :: rest) => rest 47 case _ => y :: xs 48 } 49 50 private def norm_elems(elems: List[Elem]): List[Elem] = 51 (elems :\ (Nil: List[Elem]))(apply_elem) 52 53 private def implode_elem(elem: Elem, short: Boolean): String = 54 elem match { 55 case Root("") => "" 56 case Root(s) => "//" + s 57 case Basic(s) => s 58 case Variable("USER_HOME") if short => "~" 59 case Variable("ISABELLE_HOME") if short => "~~" 60 case Variable(s) => "$" + s 61 case Parent => ".." 62 } 63 64 65 /* path constructors */ 66 67 val current: Path = new Path(Nil) 68 val root: Path = new Path(List(Root(""))) 69 def named_root(s: String): Path = new Path(List(root_elem(s))) 70 def basic(s: String): Path = new Path(List(basic_elem(s))) 71 def variable(s: String): Path = new Path(List(variable_elem(s))) 72 val parent: Path = new Path(List(Parent)) 73 74 75 /* explode */ 76 77 def explode(str: String): Path = 78 { 79 def explode_elem(s: String): Elem = 80 try { 81 if (s == "..") Parent 82 else if (s == "~") Variable("USER_HOME") 83 else if (s == "~~") Variable("ISABELLE_HOME") 84 else if (s.startsWith("$")) variable_elem(s.substring(1)) 85 else basic_elem(s) 86 } 87 catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred in " + quote(str)) } 88 89 val ss = space_explode('/', str) 90 val r = ss.takeWhile(_.isEmpty).length 91 val es = ss.dropWhile(_.isEmpty) 92 val (roots, raw_elems) = 93 if (r == 0) (Nil, es) 94 else if (r == 1) (List(Root("")), es) 95 else if (es.isEmpty) (List(Root("")), Nil) 96 else (List(root_elem(es.head)), es.tail) 97 val elems = raw_elems.filterNot(s => s.isEmpty || s == ".").map(explode_elem) 98 99 new Path(norm_elems(elems reverse_::: roots)) 100 } 101 102 def is_wellformed(str: String): Boolean = 103 try { explode(str); true } catch { case ERROR(_) => false } 104 105 def is_valid(str: String): Boolean = 106 try { explode(str).expand; true } catch { case ERROR(_) => false } 107 108 def split(str: String): List[Path] = 109 space_explode(':', str).filterNot(_.isEmpty).map(explode) 110 111 112 /* encode */ 113 114 val encode: XML.Encode.T[Path] = (path => XML.Encode.string(path.implode)) 115} 116 117 118final class Path private(private val elems: List[Path.Elem]) // reversed elements 119{ 120 def is_current: Boolean = elems.isEmpty 121 def is_absolute: Boolean = elems.nonEmpty && elems.last.isInstanceOf[Path.Root] 122 def is_root: Boolean = elems match { case List(Path.Root(_)) => true case _ => false } 123 def is_basic: Boolean = elems match { case List(Path.Basic(_)) => true case _ => false } 124 125 def +(other: Path): Path = new Path((other.elems :\ elems)(Path.apply_elem)) 126 127 128 /* implode */ 129 130 private def gen_implode(short: Boolean): String = 131 elems match { 132 case Nil => "." 133 case List(Path.Root("")) => "/" 134 case _ => elems.map(Path.implode_elem(_, short)).reverse.mkString("/") 135 } 136 def implode: String = gen_implode(false) 137 def implode_short: String = gen_implode(true) 138 139 override def toString: String = quote(implode) 140 141 142 /* base element */ 143 144 private def split_path: (Path, String) = 145 elems match { 146 case Path.Basic(s) :: xs => (new Path(xs), s) 147 case _ => error("Cannot split path into dir/base: " + toString) 148 } 149 150 def dir: Path = split_path._1 151 def base: Path = new Path(List(Path.Basic(split_path._2))) 152 def base_name: String = base.implode 153 154 def ext(e: String): Path = 155 if (e == "") this 156 else { 157 val (prfx, s) = split_path 158 prfx + Path.basic(s + "." + e) 159 } 160 161 def backup: Path = 162 { 163 val (prfx, s) = split_path 164 prfx + Path.basic(s + "~") 165 } 166 167 def backup2: Path = 168 { 169 val (prfx, s) = split_path 170 prfx + Path.basic(s + "~~") 171 } 172 173 private val Ext = new Regex("(.*)\\.([^.]*)") 174 175 def split_ext: (Path, String) = 176 { 177 val (prefix, base) = split_path 178 base match { 179 case Ext(b, e) => (prefix + Path.basic(b), e) 180 case _ => (prefix + Path.basic(base), "") 181 } 182 } 183 184 185 /* expand */ 186 187 def expand_env(env: Map[String, String]): Path = 188 { 189 def eval(elem: Path.Elem): List[Path.Elem] = 190 elem match { 191 case Path.Variable(s) => 192 val path = Path.explode(Isabelle_System.getenv_strict(s, env)) 193 if (path.elems.exists(_.isInstanceOf[Path.Variable])) 194 error("Illegal path variable nesting: " + s + "=" + path.toString) 195 else path.elems 196 case x => List(x) 197 } 198 199 new Path(Path.norm_elems(elems.map(eval).flatten)) 200 } 201 202 def expand: Path = expand_env(Isabelle_System.settings()) 203 204 205 /* source position */ 206 207 def position: Position.T = Position.File(implode) 208 209 210 /* platform files */ 211 212 def file: JFile = File.platform_file(this) 213 def is_file: Boolean = file.isFile 214 def is_dir: Boolean = file.isDirectory 215 216 def absolute_file: JFile = File.absolute(file) 217 def canonical_file: JFile = File.canonical(file) 218 219 def absolute: Path = File.path(absolute_file) 220 def canonical: Path = File.path(canonical_file) 221} 222