abstract algebra of file paths in Scala (cf. path.ML);
authorwenzelm
Thu Jun 30 00:09:57 2011 +0200 (2011-06-30)
changeset 436004ac04bf9ff89
parent 43599 e0ee016fc4fd
child 43601 fd650d659275
abstract algebra of file paths in Scala (cf. path.ML);
src/Pure/General/path.scala
src/Pure/build-jars
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/General/path.scala	Thu Jun 30 00:09:57 2011 +0200
     1.3 @@ -0,0 +1,137 @@
     1.4 +/*  Title:      Pure/General/path.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Abstract algebra of file paths: basic POSIX notation, extended by
     1.8 +named roots (e.g. //foo) and variables (e.g. $BAR).
     1.9 +*/
    1.10 +
    1.11 +package isabelle
    1.12 +
    1.13 +
    1.14 +object Path
    1.15 +{
    1.16 +  /* path elements */
    1.17 +
    1.18 +  private sealed abstract class Elem
    1.19 +  private case class Root(val name: String) extends Elem
    1.20 +  private case class Basic(val name: String) extends Elem
    1.21 +  private case class Variable(val name: String) extends Elem
    1.22 +  private case object Parent extends Elem
    1.23 +
    1.24 +  private def err_elem(msg: String, s: String): Nothing =
    1.25 +    error (msg + " path element specification: " + Library.quote(s))
    1.26 +
    1.27 +  private def check_elem(s: String): String =
    1.28 +    if (s == "" || s == "~" || s == "~~") err_elem("Illegal", s)
    1.29 +    else
    1.30 +      s.iterator.filter(c => c == '/' || c == '\\' || c == '$' || c == ':').toList match {
    1.31 +        case Nil => s
    1.32 +        case bads =>
    1.33 +          err_elem ("Illegal character(s) " + Library.commas_quote(bads.map(_.toString)) + " in", s)
    1.34 +      }
    1.35 +
    1.36 +  private def root_elem(s: String): Elem = Root(check_elem(s))
    1.37 +  private def basic_elem(s: String): Elem = Basic(check_elem(s))
    1.38 +  private def variable_elem(s: String): Elem = Variable(check_elem(s))
    1.39 +
    1.40 +  private def apply_elem(y: Elem, xs: List[Elem]): List[Elem] =
    1.41 +    (y, xs) match {
    1.42 +      case (Root(_), _) => List(y)
    1.43 +      case (Parent, Root(_) :: _) => xs
    1.44 +      case (Parent, Basic(_) :: rest) => rest
    1.45 +      case _ => y :: xs
    1.46 +    }
    1.47 +
    1.48 +  private def norm_elems(elems: List[Elem]): List[Elem] =
    1.49 +    (elems :\ (Nil: List[Elem]))(apply_elem)
    1.50 +
    1.51 +  private def implode_elem(elem: Elem): String =
    1.52 +    elem match {
    1.53 +      case Root("") => ""
    1.54 +      case Root(s) => "//" + s
    1.55 +      case Basic(s) => s
    1.56 +      case Variable(s) => "$" + s
    1.57 +      case Parent => ".."
    1.58 +    }
    1.59 +
    1.60 +
    1.61 +  /* path constructors */
    1.62 +
    1.63 +  private def apply(xs: List[Elem]): Path =
    1.64 +    new Path { override val elems = xs }
    1.65 +
    1.66 +  val current: Path = Path(Nil)
    1.67 +  val root: Path = Path(List(Root("")))
    1.68 +  def named_root(s: String): Path = Path(List(root_elem(s)))
    1.69 +  def basic(s: String): Path = Path(List(basic_elem(s)))
    1.70 +  def variable(s: String): Path = Path(List(variable_elem(s)))
    1.71 +  val parent: Path = Path(List(Parent))
    1.72 +
    1.73 +
    1.74 +  /* explode */
    1.75 +
    1.76 +  private def explode_elem(s: String): Elem =
    1.77 +    if (s == "..") Parent
    1.78 +    else if (s == "~") Variable("HOME")
    1.79 +    else if (s == "~~") Variable("ISABELLE_HOME")
    1.80 +    else if (s.startsWith("$")) variable_elem(s.substring(1))
    1.81 +    else basic_elem(s)
    1.82 +
    1.83 +  private def explode_elems(ss: List[String]): List[Elem] =
    1.84 +    ss.filterNot(s => s.isEmpty || s == ".").map(explode_elem).reverse
    1.85 +
    1.86 +  def explode(str: String): Path =
    1.87 +  {
    1.88 +    val ss = Library.space_explode('/', str)
    1.89 +    val r = ss.takeWhile(_.isEmpty).length
    1.90 +    val es = ss.dropWhile(_.isEmpty)
    1.91 +    val (roots, raw_elems) =
    1.92 +      if (r == 0) (Nil, es)
    1.93 +      else if (r == 1) (List(Root("")), es)
    1.94 +      else if (es.isEmpty) (List(Root("")), Nil)
    1.95 +      else (List(root_elem(es.head)), es.tail)
    1.96 +    Path(norm_elems(explode_elems(raw_elems) ++ roots))
    1.97 +  }
    1.98 +}
    1.99 +
   1.100 +class Path
   1.101 +{
   1.102 +  protected val elems: List[Path.Elem] = Nil   // reversed elements
   1.103 +
   1.104 +  def is_current: Boolean = elems.isEmpty
   1.105 +  def is_absolute: Boolean = !elems.isEmpty && elems.last.isInstanceOf[Path.Root]
   1.106 +  def is_basic: Boolean = elems match { case List(Path.Basic(_)) => true case _ => false }
   1.107 +
   1.108 +  def append(other: Path): Path = Path((elems :\ other.elems)(Path.apply_elem))
   1.109 +
   1.110 +
   1.111 +  /* print */
   1.112 +
   1.113 +  override def toString: String =
   1.114 +    elems match {
   1.115 +      case Nil => "."
   1.116 +      case List(Path.Root("")) => "/"
   1.117 +      case _ => elems.reverse.map(Path.implode_elem).mkString("/")
   1.118 +    }
   1.119 +
   1.120 +  def print: String = Library.quote(toString)
   1.121 +
   1.122 +
   1.123 +  /* base element */
   1.124 +
   1.125 +  private def split_path: (Path, String) =
   1.126 +    elems match {
   1.127 +      case Path.Basic(s) :: xs => (Path(xs), s)
   1.128 +      case _ => error("Cannot split path into dir/base: " + print)
   1.129 +    }
   1.130 +
   1.131 +  def dir: Path = split_path._1
   1.132 +  def base: Path = Path(List(Path.Basic(split_path._2)))
   1.133 +
   1.134 +  def ext(e: String): Path =
   1.135 +    if (e == "") this
   1.136 +    else {
   1.137 +      val (prfx, s) = split_path
   1.138 +      prfx.append(Path.basic(s + "." + e))
   1.139 +    }
   1.140 +}
     2.1 --- a/src/Pure/build-jars	Thu Jun 30 00:01:00 2011 +0200
     2.2 +++ b/src/Pure/build-jars	Thu Jun 30 00:09:57 2011 +0200
     2.3 @@ -16,6 +16,7 @@
     2.4    General/timing.scala
     2.5    General/linear_set.scala
     2.6    General/markup.scala
     2.7 +  General/path.scala
     2.8    General/position.scala
     2.9    General/pretty.scala
    2.10    General/scan.scala