author | wenzelm |
Tue, 05 Oct 1999 15:26:10 +0200 | |
changeset 7714 | e6aa4fca983e |
parent 7713 | f4fe9d620107 |
child 7715 | f90ec7937a7d |
--- 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;