# HG changeset patch
# User wenzelm
# Date 1547655168 -3600
# Node ID 114ae60c4be7b8902a57879d17aa30143e8a0992
# Parent  d51e5e41fafe5fbd5c60c03980f8dec9d549ec30
clarified signature;

diff -r d51e5e41fafe -r 114ae60c4be7 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Wed Jan 16 11:48:06 2019 +0100
+++ b/src/Pure/General/path.ML	Wed Jan 16 17:12:48 2019 +0100
@@ -14,6 +14,7 @@
   val root: T
   val named_root: string -> T
   val parent: T
+  val make: string list -> T
   val basic: string -> T
   val variable: string -> T
   val has_parent: T -> bool
@@ -22,7 +23,6 @@
   val starts_basic: T -> bool
   val append: T -> T -> T
   val appends: T list -> T
-  val make: string list -> T
   val implode: T -> string
   val explode: string -> T
   val decode: T XML.Decode.T
@@ -88,6 +88,7 @@
 val current = Path [];
 val root = Path [Root ""];
 fun named_root s = Path [root_elem s];
+val make = Path o rev o map basic_elem;
 fun basic s = Path [basic_elem s];
 fun variable s = Path [variable_elem s];
 val parent = Path [Parent];
@@ -117,7 +118,6 @@
 
 fun append (Path xs) (Path ys) = Path (fold_rev apply ys xs);
 fun appends paths = Library.foldl (uncurry append) (current, paths);
-val make = appends o map basic;
 
 fun norm elems = fold_rev apply elems [];
 
diff -r d51e5e41fafe -r 114ae60c4be7 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Wed Jan 16 11:48:06 2019 +0100
+++ b/src/Pure/General/path.scala	Wed Jan 16 17:12:48 2019 +0100
@@ -73,6 +73,7 @@
   val current: Path = new Path(Nil)
   val root: Path = new Path(List(Root("")))
   def named_root(s: String): Path = new Path(List(root_elem(s)))
+  def make(elems: List[String]): Path = new Path(elems.reverse.map(basic_elem(_)))
   def basic(s: String): Path = new Path(List(basic_elem(s)))
   def variable(s: String): Path = new Path(List(variable_elem(s)))
   val parent: Path = new Path(List(Parent))