wenzelm@6118: (* Title: Pure/General/path.ML wenzelm@5011: ID: $Id$ wenzelm@5011: Author: Markus Wenzel, TU Muenchen wenzelm@5011: wenzelm@6183: Abstract algebra of file paths (external encoding Unix-style). wenzelm@5011: *) wenzelm@5011: wenzelm@5011: signature PATH = wenzelm@5011: sig wenzelm@6183: datatype elem = Root | Parent | Basic of string | Variable of string wenzelm@6183: eqtype T wenzelm@6183: val rep: T -> elem list wenzelm@6460: val is_current: T -> bool wenzelm@6183: val current: T wenzelm@6183: val root: T wenzelm@6183: val parent: T wenzelm@6183: val basic: string -> T wenzelm@6183: val variable: string -> T wenzelm@6183: val is_absolute: T -> bool wenzelm@6183: val is_basic: T -> bool wenzelm@6183: val append: T -> T -> T wenzelm@6270: val appends: T list -> T wenzelm@6319: val make: string list -> T wenzelm@5011: val pack: T -> string wenzelm@5011: val unpack: string -> T wenzelm@14912: val dir: T -> T wenzelm@6183: val base: T -> T wenzelm@6183: val ext: string -> T -> T wenzelm@14912: val split_ext: T -> T * string wenzelm@6183: val expand: T -> T wenzelm@7714: val position: T -> Position.T wenzelm@5011: end; wenzelm@5011: wenzelm@6187: structure Path: PATH = wenzelm@5011: struct wenzelm@5011: wenzelm@6183: wenzelm@6183: (* path elements *) wenzelm@6183: wenzelm@6183: datatype elem = Root | Parent | Basic of string | Variable of string; wenzelm@6183: wenzelm@6223: fun err_elem msg chs = error (msg ^ " path element specification: " ^ quote (implode chs)); wenzelm@6183: wenzelm@6319: fun check_elem (chs as []) = err_elem "Illegal" chs wenzelm@6319: | check_elem (chs as ["~"]) = err_elem "Illegal" chs wenzelm@6223: | check_elem (chs as ["~", "~"]) = err_elem "Illegal" chs wenzelm@6223: | check_elem chs = wenzelm@6223: (case ["/", "\\", "$", ":"] inter_string chs of wenzelm@6223: [] => chs wenzelm@6223: | bads => err_elem ("Illegal character(s) " ^ commas_quote bads ^ " in") chs); wenzelm@6223: wenzelm@6223: val basic_elem = Basic o implode o check_elem; wenzelm@6223: val variable_elem = Variable o implode o check_elem; wenzelm@6183: wenzelm@6183: fun is_var (Variable _) = true wenzelm@6183: | is_var _ = false; wenzelm@6183: wenzelm@6183: wenzelm@5011: (* type path *) wenzelm@5011: wenzelm@6183: datatype T = Path of elem list; wenzelm@6183: wenzelm@6183: fun rep (Path xs) = xs; wenzelm@5011: wenzelm@6460: fun is_current (Path []) = true wenzelm@6460: | is_current _ = false; wenzelm@6460: wenzelm@5011: val current = Path []; wenzelm@6183: val root = Path [Root]; wenzelm@6183: val parent = Path [Parent]; wenzelm@6183: fun basic s = Path [basic_elem (explode s)]; wenzelm@6183: fun variable s = Path [variable_elem (explode s)]; wenzelm@5011: wenzelm@6183: fun is_absolute (Path (Root :: _)) = true wenzelm@6183: | is_absolute _ = false; wenzelm@5011: wenzelm@6183: fun is_basic (Path [Basic _]) = true wenzelm@6183: | is_basic _ = false; wenzelm@5011: wenzelm@5011: wenzelm@5011: (* append and norm *) wenzelm@5011: wenzelm@5011: (*append non-normal path (2n arg) to reversed normal one, result is normal*) wenzelm@5011: fun rev_app xs [] = rev xs wenzelm@6183: | rev_app _ (Root :: ys) = rev_app [Root] ys wenzelm@6183: | rev_app (x :: xs) (Parent :: ys) = wenzelm@6183: if x = Parent orelse is_var x then rev_app (Parent :: x :: xs) ys wenzelm@6183: else if x = Root then rev_app (x :: xs) ys wenzelm@5011: else rev_app xs ys wenzelm@5011: | rev_app xs (y :: ys) = rev_app (y :: xs) ys; wenzelm@5011: wenzelm@6183: fun append (Path xs) (Path ys) = Path (rev_app (rev xs) ys); skalberg@15570: fun appends paths = Library.foldl (uncurry append) (current, paths); wenzelm@6319: val make = appends o map basic; wenzelm@5011: fun norm path = rev_app [] path; wenzelm@5011: wenzelm@6183: wenzelm@6183: (* pack *) wenzelm@5011: wenzelm@6183: fun pack_elem Root = "" wenzelm@6183: | pack_elem Parent = ".." wenzelm@6183: | pack_elem (Basic s) = s wenzelm@6183: | pack_elem (Variable s) = "$" ^ s; wenzelm@5011: wenzelm@5011: fun pack (Path []) = "." wenzelm@6183: | pack (Path (Root :: xs)) = "/" ^ space_implode "/" (map pack_elem xs) wenzelm@6183: | pack (Path xs) = space_implode "/" (map pack_elem xs); wenzelm@5011: wenzelm@5011: wenzelm@6183: (* unpack *) wenzelm@6183: wenzelm@6183: fun unpack_elem "" = Root wenzelm@6183: | unpack_elem ".." = Parent wenzelm@6183: | unpack_elem "~" = Variable "HOME" wenzelm@6183: | unpack_elem "~~" = Variable "ISABELLE_HOME" wenzelm@6183: | unpack_elem s = wenzelm@6183: (case explode s of wenzelm@6183: "$" :: cs => variable_elem cs wenzelm@6183: | cs => basic_elem cs); wenzelm@6183: wenzelm@19305: val unpack_elems = map unpack_elem o filter_out (fn c => c = "" orelse c = "."); wenzelm@6183: wenzelm@6183: fun unpack str = Path (norm wenzelm@6183: (case space_explode "/" str of wenzelm@6183: "" :: ss => Root :: unpack_elems ss wenzelm@6183: | ss => unpack_elems ss)); wenzelm@6183: wenzelm@5011: wenzelm@6183: (* base element *) wenzelm@6183: wenzelm@7929: fun split_path f (path as Path xs) = wenzelm@7929: (case try split_last xs of skalberg@15531: SOME (prfx, Basic s) => f (prfx, s) wenzelm@7929: | _ => error ("Cannot split path into dir/base: " ^ quote (pack path))); wenzelm@6183: wenzelm@14912: val dir = split_path (fn (prfx, _) => Path prfx); wenzelm@7929: val base = split_path (fn (_, s) => Path [Basic s]); wenzelm@6183: wenzelm@7929: fun ext "" path = path wenzelm@7929: | ext e path = split_path (fn (prfx, s) => append (Path prfx) (basic (s ^ "." ^ e))) path; wenzelm@6183: wenzelm@14912: val split_ext = split_path (fn (prfx, s) => apfst (append (Path prfx)) wenzelm@19305: (case take_suffix (fn c => c <> ".") (explode s) of wenzelm@14912: ([], _) => (Path [Basic s], "") skalberg@15570: | (cs, e) => (Path [Basic (implode (Library.take (length cs - 1, cs)))], implode e))); wenzelm@6319: wenzelm@6183: wenzelm@17827: (* expand variables *) wenzelm@5011: wenzelm@17827: fun eval (Variable s) = wenzelm@17827: (case getenv s of wenzelm@17827: "" => error ("Undefined Isabelle environment variable: " ^ quote s) wenzelm@17827: | path => rep (unpack path)) wenzelm@17827: | eval x = [x]; wenzelm@5011: wenzelm@19482: val expand = rep #> maps eval #> norm #> Path; wenzelm@17827: val position = expand #> pack #> quote #> Position.line_name 1; wenzelm@5011: wenzelm@5011: end;