added position;
authorwenzelm
Tue, 05 Oct 1999 15:26:10 +0200
changeset 7714 e6aa4fca983e
parent 7713 f4fe9d620107
child 7715 f90ec7937a7d
added position;
src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Tue Oct 05 15:25:52 1999 +0200
+++ b/src/Pure/General/path.ML	Tue Oct 05 15:26:10 1999 +0200
@@ -27,6 +27,7 @@
   val ext: string -> T -> T
   val dir: T -> T
   val expand: T -> T
+  val position: T -> Position.T
 end;
 
 structure Path: PATH =
@@ -155,5 +156,7 @@
 
 val expand = evaluate (unpack o getenv);
 
+val position = Position.line_name 1 o quote o pack o expand;
+
 
 end;