author  wenzelm 
Fri, 03 Aug 2012 13:06:25 +0200  
changeset 48658  4c7932270d6d 
parent 48420  a8ed41b6280b 
child 48866  034df7b05759 
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 

20 
val append: T > T > T 

6270  21 
val appends: T list > T 
6319  22 
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

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

24 
val explode: string > T 
43593  25 
val pretty: T > Pretty.T 
26 
val print: T > string 

14912  27 
val dir: T > T 
6183  28 
val base: T > T 
29 
val ext: string > T > T 

14912  30 
val split_ext: T > T * string 
6183  31 
val expand: T > T 
26881  32 
val position: T > Position.T 
5011  33 
end; 
34 

6187  35 
structure Path: PATH = 
5011  36 
struct 
37 

6183  38 
(* path elements *) 
39 

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

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

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

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

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

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

45 

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

46 
local 
6183  47 

6223  48 
fun err_elem msg chs = error (msg ^ " path element specification: " ^ quote (implode chs)); 
6183  49 

6319  50 
fun check_elem (chs as []) = err_elem "Illegal" chs 
51 
 check_elem (chs as ["~"]) = err_elem "Illegal" chs 

6223  52 
 check_elem (chs as ["~", "~"]) = err_elem "Illegal" chs 
53 
 check_elem chs = 

48420
a8ed41b6280b
disallow quotes in path specifications  extra paranoia;
wenzelm
parents:
47661
diff
changeset

54 
(case inter (op =) ["/", "\\", "$", ":", "\"", "'"] chs of 
6223  55 
[] => chs 
56 
 bads => err_elem ("Illegal character(s) " ^ commas_quote bads ^ " in") chs); 

57 

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

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

59 

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

60 
val root_elem = Root o implode o check_elem; 
6223  61 
val basic_elem = Basic o implode o check_elem; 
62 
val variable_elem = Variable o implode o check_elem; 

6183  63 

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

64 
end; 
6183  65 

66 

5011  67 
(* type path *) 
68 

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

69 
datatype T = Path of elem list; (*reversed elements*) 
6183  70 

71 
fun rep (Path xs) = xs; 

5011  72 

6460  73 
fun is_current (Path []) = true 
74 
 is_current _ = false; 

75 

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

77 
val root = Path [Root ""]; 
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
36135
diff
changeset

78 
fun named_root s = Path [root_elem (raw_explode s)]; 
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
36135
diff
changeset

79 
fun basic s = Path [basic_elem (raw_explode s)]; 
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
36135
diff
changeset

80 
fun variable s = Path [variable_elem (raw_explode s)]; 
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

81 
val parent = Path [Parent]; 
5011  82 

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

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

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

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

86 
 _ => false); 
5011  87 

6183  88 
fun is_basic (Path [Basic _]) = true 
89 
 is_basic _ = false; 

5011  90 

91 

92 
(* append and norm *) 

93 

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

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

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

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

97 
 apply y xs = y :: xs; 
5011  98 

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

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

102 

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

103 
fun norm elems = fold_rev apply elems []; 
5011  104 

6183  105 

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

106 
(* implode *) 
5011  107 

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

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

109 

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

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

111 
 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

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

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

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

115 

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

116 
in 
5011  117 

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

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

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

120 
 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

121 

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

122 
end; 
5011  123 

124 

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

125 
(* explode *) 
6183  126 

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

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

128 

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

129 
fun explode_elem ".." = Parent 
47661
012a887997f3
USER_HOME settings variable points to crossplatform user home directory;
wenzelm
parents:
45666
diff
changeset

130 
 explode_elem "~" = Variable "USER_HOME" 
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
19482
diff
changeset

131 
 explode_elem "~~" = Variable "ISABELLE_HOME" 
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
19482
diff
changeset

132 
 explode_elem s = 
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
36135
diff
changeset

133 
(case raw_explode s of 
6183  134 
"$" :: cs => variable_elem cs 
135 
 cs => basic_elem cs); 

136 

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

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

138 
rev o map explode_elem o filter_out (fn c => c = "" orelse c = "."); 
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

139 

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

140 
in 
6183  141 

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

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

143 
let val (roots, raw_elems) = 
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

144 
(case take_prefix (equal "") (space_explode "/" str) >> length of 
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

145 
(0, es) => ([], es) 
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

146 
 (1, es) => ([Root ""], es) 
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

147 
 (_, []) => ([Root ""], []) 
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
36135
diff
changeset

148 
 (_, e :: es) => ([root_elem (raw_explode e)], es)) 
36135
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

149 
in Path (norm (explode_elems raw_elems @ roots)) end; 
89d1903fbd50
support named_root, which approximates UNC server prefix (for Cygwin);
wenzelm
parents:
33957
diff
changeset

150 

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

151 
end; 
6183  152 

5011  153 

43593  154 
(* print *) 
155 

156 
fun pretty path = 

157 
let val s = implode_path path 

45666  158 
in Pretty.mark (Isabelle_Markup.path s) (Pretty.str (quote s)) end; 
43593  159 

160 
val print = Pretty.str_of o pretty; 

161 

162 

6183  163 
(* base element *) 
164 

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

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

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

168 
val dir = split_path #1; 
7929  169 
val base = split_path (fn (_, s) => Path [Basic s]); 
6183  170 

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

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

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

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

174 
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

175 
(case take_suffix (fn c => c <> ".") (raw_explode s) of 
14912  176 
([], _) => (Path [Basic s], "") 
33957  177 
 (cs, e) => (Path [Basic (implode (take (length cs  1) cs))], implode e))); 
6319  178 

6183  179 

17827  180 
(* expand variables *) 
5011  181 

48658  182 
fun eval (Variable s) = 
183 
let val path = explode_path (getenv_strict s) in 

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

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

186 
else rep path 

187 
end 

17827  188 
 eval x = [x]; 
5011  189 

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

190 
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

191 

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

192 

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

193 
(* source position  with smart replacement ISABELLE_HOME *) 
49ea566cb3b4
more symbolic file positions via smart replacement of ISABELLE_HOME  allows Isabelle distribution to be moved later on;
wenzelm
parents:
44161
diff
changeset

194 

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

195 
val isabelle_home = explode_path "~~"; 
26881  196 

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

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

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

199 
val s = implode_path path; 
49ea566cb3b4
more symbolic file positions via smart replacement of ISABELLE_HOME  allows Isabelle distribution to be moved later on;
wenzelm
parents:
44161
diff
changeset

200 
val prfx = implode_path (expand isabelle_home) ^ "/"; 
49ea566cb3b4
more symbolic file positions via smart replacement of ISABELLE_HOME  allows Isabelle distribution to be moved later on;
wenzelm
parents:
44161
diff
changeset

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

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

203 
(case try (unprefix prfx) s of 
49ea566cb3b4
more symbolic file positions via smart replacement of ISABELLE_HOME  allows Isabelle distribution to be moved later on;
wenzelm
parents:
44161
diff
changeset

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

205 
 SOME s' => "~~/" ^ s') 
49ea566cb3b4
more symbolic file positions via smart replacement of ISABELLE_HOME  allows Isabelle distribution to be moved later on;
wenzelm
parents:
44161
diff
changeset

206 
end; 
26881  207 

208 

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

209 
(*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

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

211 
val explode = explode_path; 
5011  212 

213 
end; 

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

214 