# HG changeset patch
# User wenzelm
# Date 1309385397 -7200
# Node ID 4ac04bf9ff898ffd7081fdad05f6d029b3782ce1
# Parent  e0ee016fc4fdd62ef27189981736dc7165b35edf
abstract algebra of file paths in Scala (cf. path.ML);

diff -r e0ee016fc4fd -r 4ac04bf9ff89 src/Pure/General/path.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/path.scala	Thu Jun 30 00:09:57 2011 +0200
@@ -0,0 +1,137 @@
+/*  Title:      Pure/General/path.scala
+    Author:     Makarius
+
+Abstract algebra of file paths: basic POSIX notation, extended by
+named roots (e.g. //foo) and variables (e.g. $BAR).
+*/
+
+package isabelle
+
+
+object Path
+{
+  /* path elements */
+
+  private sealed abstract class Elem
+  private case class Root(val name: String) extends Elem
+  private case class Basic(val name: String) extends Elem
+  private case class Variable(val name: String) extends Elem
+  private case object Parent extends Elem
+
+  private def err_elem(msg: String, s: String): Nothing =
+    error (msg + " path element specification: " + Library.quote(s))
+
+  private def check_elem(s: String): String =
+    if (s == "" || s == "~" || s == "~~") err_elem("Illegal", s)
+    else
+      s.iterator.filter(c => c == '/' || c == '\\' || c == '$' || c == ':').toList match {
+        case Nil => s
+        case bads =>
+          err_elem ("Illegal character(s) " + Library.commas_quote(bads.map(_.toString)) + " in", s)
+      }
+
+  private def root_elem(s: String): Elem = Root(check_elem(s))
+  private def basic_elem(s: String): Elem = Basic(check_elem(s))
+  private def variable_elem(s: String): Elem = Variable(check_elem(s))
+
+  private def apply_elem(y: Elem, xs: List[Elem]): List[Elem] =
+    (y, xs) match {
+      case (Root(_), _) => List(y)
+      case (Parent, Root(_) :: _) => xs
+      case (Parent, Basic(_) :: rest) => rest
+      case _ => y :: xs
+    }
+
+  private def norm_elems(elems: List[Elem]): List[Elem] =
+    (elems :\ (Nil: List[Elem]))(apply_elem)
+
+  private def implode_elem(elem: Elem): String =
+    elem match {
+      case Root("") => ""
+      case Root(s) => "//" + s
+      case Basic(s) => s
+      case Variable(s) => "$" + s
+      case Parent => ".."
+    }
+
+
+  /* path constructors */
+
+  private def apply(xs: List[Elem]): Path =
+    new Path { override val elems = xs }
+
+  val current: Path = Path(Nil)
+  val root: Path = Path(List(Root("")))
+  def named_root(s: String): Path = Path(List(root_elem(s)))
+  def basic(s: String): Path = Path(List(basic_elem(s)))
+  def variable(s: String): Path = Path(List(variable_elem(s)))
+  val parent: Path = Path(List(Parent))
+
+
+  /* explode */
+
+  private def explode_elem(s: String): Elem =
+    if (s == "..") Parent
+    else if (s == "~") Variable("HOME")
+    else if (s == "~~") Variable("ISABELLE_HOME")
+    else if (s.startsWith("$")) variable_elem(s.substring(1))
+    else basic_elem(s)
+
+  private def explode_elems(ss: List[String]): List[Elem] =
+    ss.filterNot(s => s.isEmpty || s == ".").map(explode_elem).reverse
+
+  def explode(str: String): Path =
+  {
+    val ss = Library.space_explode('/', str)
+    val r = ss.takeWhile(_.isEmpty).length
+    val es = ss.dropWhile(_.isEmpty)
+    val (roots, raw_elems) =
+      if (r == 0) (Nil, es)
+      else if (r == 1) (List(Root("")), es)
+      else if (es.isEmpty) (List(Root("")), Nil)
+      else (List(root_elem(es.head)), es.tail)
+    Path(norm_elems(explode_elems(raw_elems) ++ roots))
+  }
+}
+
+class Path
+{
+  protected val elems: List[Path.Elem] = Nil   // reversed elements
+
+  def is_current: Boolean = elems.isEmpty
+  def is_absolute: Boolean = !elems.isEmpty && elems.last.isInstanceOf[Path.Root]
+  def is_basic: Boolean = elems match { case List(Path.Basic(_)) => true case _ => false }
+
+  def append(other: Path): Path = Path((elems :\ other.elems)(Path.apply_elem))
+
+
+  /* print */
+
+  override def toString: String =
+    elems match {
+      case Nil => "."
+      case List(Path.Root("")) => "/"
+      case _ => elems.reverse.map(Path.implode_elem).mkString("/")
+    }
+
+  def print: String = Library.quote(toString)
+
+
+  /* base element */
+
+  private def split_path: (Path, String) =
+    elems match {
+      case Path.Basic(s) :: xs => (Path(xs), s)
+      case _ => error("Cannot split path into dir/base: " + print)
+    }
+
+  def dir: Path = split_path._1
+  def base: Path = Path(List(Path.Basic(split_path._2)))
+
+  def ext(e: String): Path =
+    if (e == "") this
+    else {
+      val (prfx, s) = split_path
+      prfx.append(Path.basic(s + "." + e))
+    }
+}
diff -r e0ee016fc4fd -r 4ac04bf9ff89 src/Pure/build-jars
--- a/src/Pure/build-jars	Thu Jun 30 00:01:00 2011 +0200
+++ b/src/Pure/build-jars	Thu Jun 30 00:09:57 2011 +0200
@@ -16,6 +16,7 @@
   General/timing.scala
   General/linear_set.scala
   General/markup.scala
+  General/path.scala
   General/position.scala
   General/pretty.scala
   General/scan.scala