src/Pure/General/path.ML
changeset 7714 e6aa4fca983e
parent 6460 cb8c85435228
child 7929 2010ae0393ca
--- 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;