author  wenzelm 
Fri, 18 Mar 2016 16:26:35 +0100  
changeset 62663  bea354f6ff21 
parent 61877  276ad4354069 
child 62819  d3ff367a16a0 
permissions  rwrr 
6118  1 
(* Title: Pure/General/path.ML 
5011  2 
Author: Markus Wenzel, TU Muenchen 
3 

43601  4 
Algebra of filesystem paths: basic POSIX notation, extended by named 
5 
roots (e.g. //foo) and variables (e.g. $BAR). 

5011  6 
*) 
7 

8 
signature PATH = 

9 
sig 

6183  10 
eqtype T 
6460  11 
val is_current: T > bool 
6183  12 
val current: T 
13 
val root: T 

36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

14 
val named_root: string > T 
6183  15 
val parent: T 
16 
val basic: string > T 

17 
val variable: string > T 

18 
val is_absolute: T > bool 

19 
val is_basic: T > bool 

56533
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56136
diff
changeset

20 
val starts_basic: T > bool 
6183  21 
val append: T > T > T 
6270  22 
val appends: T list > T 
6319  23 
val make: string list > T 
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
19482
diff
changeset

24 
val implode: T > string 
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
19482
diff
changeset

25 
val explode: string > T 
59363
4660b0409096
added Path.decode in ML, in correspondence to Path.encode in Scala;
wenzelm
parents:
56533
diff
changeset

26 
val decode: T XML.Decode.T 
53045  27 
val split: string > T list 
43593  28 
val pretty: T > Pretty.T 
29 
val print: T > string 

14912  30 
val dir: T > T 
6183  31 
val base: T > T 
32 
val ext: string > T > T 

14912  33 
val split_ext: T > T * string 
6183  34 
val expand: T > T 
56134  35 
val smart_implode: T > string 
26881  36 
val position: T > Position.T 
5011  37 
end; 
38 

6187  39 
structure Path: PATH = 
5011  40 
struct 
41 

6183  42 
(* path elements *) 
43 

36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

44 
datatype elem = 
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

45 
Root of string  
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

46 
Basic of string  
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

47 
Variable of string  
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

48 
Parent; 
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

49 

89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

50 
local 
6183  51 

52106  52 
fun err_elem msg s = error (msg ^ " path element specification " ^ quote s); 
6183  53 

52106  54 
fun check_elem s = 
55 
if s = "" orelse s = "~" orelse s = "~~" then err_elem "Illegal" s 

56 
else 

57 
let 

58 
fun check c = 

59 
if exists_string (fn c' => c = c') s then 

60 
err_elem ("Illegal character " ^ quote c ^ " in") s 

61 
else (); 

62 
val _ = List.app check ["/", "\\", "$", ":", "\"", "'"]; 

63 
in s end; 

6223  64 

36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

65 
in 
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

66 

52106  67 
val root_elem = Root o check_elem; 
68 
val basic_elem = Basic o check_elem; 

69 
val variable_elem = Variable o check_elem; 

6183  70 

36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

71 
end; 
6183  72 

73 

5011  74 
(* type path *) 
75 

36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

76 
datatype T = Path of elem list; (*reversed elements*) 
6183  77 

78 
fun rep (Path xs) = xs; 

5011  79 

6460  80 
fun is_current (Path []) = true 
81 
 is_current _ = false; 

82 

5011  83 
val current = Path []; 
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

84 
val root = Path [Root ""]; 
52106  85 
fun named_root s = Path [root_elem s]; 
86 
fun basic s = Path [basic_elem s]; 

87 
fun variable s = Path [variable_elem s]; 

36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

88 
val parent = Path [Parent]; 
5011  89 

36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

90 
fun is_absolute (Path xs) = 
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

91 
(case try List.last xs of 
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

92 
SOME (Root _) => true 
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

93 
 _ => false); 
5011  94 

6183  95 
fun is_basic (Path [Basic _]) = true 
96 
 is_basic _ = false; 

5011  97 

56533
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56136
diff
changeset

98 
fun starts_basic (Path xs) = 
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56136
diff
changeset

99 
(case try List.last xs of 
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56136
diff
changeset

100 
SOME (Basic _) => true 
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56136
diff
changeset

101 
 _ => false); 
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56136
diff
changeset

102 

5011  103 

104 
(* append and norm *) 

105 

36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

106 
fun apply (y as Root _) _ = [y] 
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

107 
 apply Parent (xs as (Root _ :: _)) = xs 
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

108 
 apply Parent (Basic _ :: rest) = rest 
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

109 
 apply y xs = y :: xs; 
5011  110 

36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

111 
fun append (Path xs) (Path ys) = Path (fold_rev apply ys xs); 
15570  112 
fun appends paths = Library.foldl (uncurry append) (current, paths); 
6319  113 
val make = appends o map basic; 
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

114 

89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

115 
fun norm elems = fold_rev apply elems []; 
5011  116 

6183  117 

21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
19482
diff
changeset

118 
(* implode *) 
5011  119 

36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

120 
local 
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

121 

89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

122 
fun implode_elem (Root "") = "" 
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

123 
 implode_elem (Root s) = "//" ^ s 
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
19482
diff
changeset

124 
 implode_elem (Basic s) = s 
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

125 
 implode_elem (Variable s) = "$" ^ s 
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

126 
 implode_elem Parent = ".."; 
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

127 

89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

128 
in 
5011  129 

21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
19482
diff
changeset

130 
fun implode_path (Path []) = "." 
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

131 
 implode_path (Path [Root ""]) = "/" 
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

132 
 implode_path (Path xs) = space_implode "/" (rev (map implode_elem xs)); 
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

133 

89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

134 
end; 
5011  135 

136 

21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
19482
diff
changeset

137 
(* explode *) 
6183  138 

52106  139 
fun explode_path str = 
140 
let 

141 
fun explode_elem s = 

142 
(if s = ".." then Parent 

143 
else if s = "~" then Variable "USER_HOME" 

144 
else if s = "~~" then Variable "ISABELLE_HOME" 

145 
else 

146 
(case try (unprefix "$") s of 

147 
SOME s' => variable_elem s' 

148 
 NONE => basic_elem s)) 

149 
handle ERROR msg => cat_error msg ("The error(s) above occurred in " ^ quote str); 

36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

150 

52106  151 
val (roots, raw_elems) = 
152 
(case take_prefix (equal "") (space_explode "/" str) >> length of 

153 
(0, es) => ([], es) 

154 
 (1, es) => ([Root ""], es) 

155 
 (_, []) => ([Root ""], []) 

156 
 (_, e :: es) => ([root_elem e], es)); 

157 
val elems = raw_elems > filter_out (fn c => c = "" orelse c = ".") > map explode_elem; 

6183  158 

52106  159 
in Path (norm (rev elems @ roots)) end; 
6183  160 

53045  161 
fun split str = 
162 
space_explode ":" str 

163 
> map_filter (fn s => if s = "" then NONE else SOME (explode_path s)); 

164 

59363
4660b0409096
added Path.decode in ML, in correspondence to Path.encode in Scala;
wenzelm
parents:
56533
diff
changeset

165 
val decode = XML.Decode.string #> explode_path; 
4660b0409096
added Path.decode in ML, in correspondence to Path.encode in Scala;
wenzelm
parents:
56533
diff
changeset

166 

5011  167 

43593  168 
(* print *) 
169 

170 
fun pretty path = 

171 
let val s = implode_path path 

50201
c26369c9eda6
Isabellespecific implementation of quasiabstract markup elements  back to module arrangement before d83797ef0d2d;
wenzelm
parents:
48866
diff
changeset

172 
in Pretty.mark (Markup.path s) (Pretty.str (quote s)) end; 
43593  173 

61877
276ad4354069
renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;
wenzelm
parents:
59363
diff
changeset

174 
val print = Pretty.unformatted_string_of o pretty; 
43593  175 

62663  176 
val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty); 
177 

43593  178 

6183  179 
(* base element *) 
180 

36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

181 
fun split_path f (Path (Basic s :: xs)) = f (Path xs, s) 
43599  182 
 split_path _ path = error ("Cannot split path into dir/base: " ^ print path); 
6183  183 

36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

184 
val dir = split_path #1; 
7929  185 
val base = split_path (fn (_, s) => Path [Basic s]); 
6183  186 

36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

187 
fun ext "" = I 
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

188 
 ext e = split_path (fn (prfx, s) => append prfx (basic (s ^ "." ^ e))); 
6183  189 

36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

190 
val split_ext = split_path (fn (prfx, s) => apfst (append prfx) 
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
36135
diff
changeset

191 
(case take_suffix (fn c => c <> ".") (raw_explode s) of 
14912  192 
([], _) => (Path [Basic s], "") 
33957  193 
 (cs, e) => (Path [Basic (implode (take (length cs  1) cs))], implode e))); 
6319  194 

6183  195 

17827  196 
(* expand variables *) 
5011  197 

48658  198 
fun eval (Variable s) = 
199 
let val path = explode_path (getenv_strict s) in 

200 
if exists (fn Variable _ => true  _ => false) (rep path) then 

201 
error ("Illegal path variable nesting: " ^ s ^ "=" ^ print path) 

202 
else rep path 

203 
end 

17827  204 
 eval x = [x]; 
5011  205 

19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19305
diff
changeset

206 
val expand = rep #> maps eval #> norm #> Path; 
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
19482
diff
changeset

207 

05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
19482
diff
changeset

208 

56136  209 
(* smart implode *) 
44863
49ea566cb3b4
more symbolic file positions via smart replacement of ISABELLE_HOME  allows Isabelle distribution to be moved later on;
wenzelm
parents:
44161
diff
changeset

210 

56134  211 
fun smart_implode path = 
44863
49ea566cb3b4
more symbolic file positions via smart replacement of ISABELLE_HOME  allows Isabelle distribution to be moved later on;
wenzelm
parents:
44161
diff
changeset

212 
let 
56134  213 
val full_name = implode_path (expand path); 
56136  214 
fun fold_path a = 
215 
let val b = implode_path (expand (explode_path a)) in 

216 
if full_name = b then SOME a 

217 
else 

218 
(case try (unprefix (b ^ "/")) full_name of 

219 
SOME name => SOME (a ^ "/" ^ name) 

220 
 NONE => NONE) 

221 
end; 

44863
49ea566cb3b4
more symbolic file positions via smart replacement of ISABELLE_HOME  allows Isabelle distribution to be moved later on;
wenzelm
parents:
44161
diff
changeset

222 
in 
56136  223 
(case get_first fold_path ["~~", "$ISABELLE_HOME_USER", "~"] of 
224 
SOME name => name 

225 
 NONE => implode_path path) 

44863
49ea566cb3b4
more symbolic file positions via smart replacement of ISABELLE_HOME  allows Isabelle distribution to be moved later on;
wenzelm
parents:
44161
diff
changeset

226 
end; 
26881  227 

56134  228 
val position = Position.file o smart_implode; 
26881  229 

21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
19482
diff
changeset

230 
(*final declarations of this structure!*) 
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
19482
diff
changeset

231 
val implode = implode_path; 
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
19482
diff
changeset

232 
val explode = explode_path; 
5011  233 

234 
end; 

36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

235 