clarified signature;
authorwenzelm
Wed Jan 16 17:12:48 2019 +0100 (10 months ago)
changeset 69670114ae60c4be7
parent 69666 d51e5e41fafe
child 69671 2486792eaf61
clarified signature;
src/Pure/General/path.ML
src/Pure/General/path.scala
     1.1 --- a/src/Pure/General/path.ML	Wed Jan 16 11:48:06 2019 +0100
     1.2 +++ b/src/Pure/General/path.ML	Wed Jan 16 17:12:48 2019 +0100
     1.3 @@ -14,6 +14,7 @@
     1.4    val root: T
     1.5    val named_root: string -> T
     1.6    val parent: T
     1.7 +  val make: string list -> T
     1.8    val basic: string -> T
     1.9    val variable: string -> T
    1.10    val has_parent: T -> bool
    1.11 @@ -22,7 +23,6 @@
    1.12    val starts_basic: T -> bool
    1.13    val append: T -> T -> T
    1.14    val appends: T list -> T
    1.15 -  val make: string list -> T
    1.16    val implode: T -> string
    1.17    val explode: string -> T
    1.18    val decode: T XML.Decode.T
    1.19 @@ -88,6 +88,7 @@
    1.20  val current = Path [];
    1.21  val root = Path [Root ""];
    1.22  fun named_root s = Path [root_elem s];
    1.23 +val make = Path o rev o map basic_elem;
    1.24  fun basic s = Path [basic_elem s];
    1.25  fun variable s = Path [variable_elem s];
    1.26  val parent = Path [Parent];
    1.27 @@ -117,7 +118,6 @@
    1.28  
    1.29  fun append (Path xs) (Path ys) = Path (fold_rev apply ys xs);
    1.30  fun appends paths = Library.foldl (uncurry append) (current, paths);
    1.31 -val make = appends o map basic;
    1.32  
    1.33  fun norm elems = fold_rev apply elems [];
    1.34  
     2.1 --- a/src/Pure/General/path.scala	Wed Jan 16 11:48:06 2019 +0100
     2.2 +++ b/src/Pure/General/path.scala	Wed Jan 16 17:12:48 2019 +0100
     2.3 @@ -73,6 +73,7 @@
     2.4    val current: Path = new Path(Nil)
     2.5    val root: Path = new Path(List(Root("")))
     2.6    def named_root(s: String): Path = new Path(List(root_elem(s)))
     2.7 +  def make(elems: List[String]): Path = new Path(elems.reverse.map(basic_elem(_)))
     2.8    def basic(s: String): Path = new Path(List(basic_elem(s)))
     2.9    def variable(s: String): Path = new Path(List(variable_elem(s)))
    2.10    val parent: Path = new Path(List(Parent))