added position;
authorwenzelm
Tue Oct 05 15:26:10 1999 +0200 (1999-10-05)
changeset 7714e6aa4fca983e
parent 7713 f4fe9d620107
child 7715 f90ec7937a7d
added position;
src/Pure/General/path.ML
     1.1 --- a/src/Pure/General/path.ML	Tue Oct 05 15:25:52 1999 +0200
     1.2 +++ b/src/Pure/General/path.ML	Tue Oct 05 15:26:10 1999 +0200
     1.3 @@ -27,6 +27,7 @@
     1.4    val ext: string -> T -> T
     1.5    val dir: T -> T
     1.6    val expand: T -> T
     1.7 +  val position: T -> Position.T
     1.8  end;
     1.9  
    1.10  structure Path: PATH =
    1.11 @@ -155,5 +156,7 @@
    1.12  
    1.13  val expand = evaluate (unpack o getenv);
    1.14  
    1.15 +val position = Position.line_name 1 o quote o pack o expand;
    1.16 +
    1.17  
    1.18  end;