# HG changeset patch
# User wenzelm
# Date 939129970 -7200
# Node ID e6aa4fca983e1826db36e436ef1bd3c659a27a85
# Parent  f4fe9d620107cf04e0bacabb02b294a3d5a87545
added position;

diff -r f4fe9d620107 -r e6aa4fca983e 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;