src/Pure/General/path.ML
changeset 23863 8f3099589cfa
parent 23672 3fd7770f6795
child 26881 bb68f50644a9
equal deleted inserted replaced
23862:b1861768d8f4 23863:8f3099589cfa
     1 (*  Title:      Pure/General/path.ML
     1 (*  Title:      Pure/General/path.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     4 
     5 Abstract algebra of file paths (external encoding Unix-style).
     5 Abstract algebra of file paths (external encoding in Unix style).
     6 *)
     6 *)
     7 
     7 
     8 signature PATH =
     8 signature PATH =
     9 sig
     9 sig
    10   datatype elem = Root | Parent | Basic of string | Variable of string
       
    11   eqtype T
    10   eqtype T
    12   val rep: T -> elem list
       
    13   val is_current: T -> bool
    11   val is_current: T -> bool
    14   val current: T
    12   val current: T
    15   val root: T
    13   val root: T
    16   val parent: T
    14   val parent: T
    17   val basic: string -> T
    15   val basic: string -> T