65 else { return slashes(backslashes); } |
65 else { return slashes(backslashes); } |
66 } |
66 } |
67 else { return platform_path; } |
67 else { return platform_path; } |
68 } |
68 } |
69 |
69 |
70 public static String platform_path(String cygwin_root, String standard_path) |
70 private static class Expand_Platform_Path |
71 { |
71 { |
72 if (is_windows()) { |
72 private String _cygwin_root; |
73 StringBuilder result_path = new StringBuilder(); |
73 private StringBuilder _result = new StringBuilder(); |
74 |
74 |
75 Pattern cygdrive_pattern = Pattern.compile("/cygdrive/([a-zA-Z])($|/.*)"); |
75 public Expand_Platform_Path(String cygwin_root) |
76 Matcher cygdrive_matcher = cygdrive_pattern.matcher(standard_path); |
76 { |
77 |
77 _cygwin_root = cygwin_root; |
78 Pattern named_root_pattern = Pattern.compile("//+([^/]*)(.*)"); |
78 } |
79 Matcher named_root_matcher = named_root_pattern.matcher(standard_path); |
79 |
80 |
80 public String result() { return _result.toString(); } |
81 String rest; |
81 |
82 if (cygdrive_matcher.matches()) { |
82 void clear() { _result.setLength(0); } |
83 String drive = cygdrive_matcher.group(1).toUpperCase(Locale.ROOT); |
83 void add(char c) { _result.append(c); } |
84 rest = cygdrive_matcher.group(2); |
84 void add(String s) { _result.append(s); } |
85 result_path.append(drive); |
85 void separator() |
86 result_path.append(':'); |
86 { |
87 result_path.append(File.separatorChar); |
87 int n = _result.length(); |
88 } |
88 if (n > 0 && _result.charAt(n - 1) != File.separatorChar) { |
89 else if (named_root_matcher.matches()) { |
89 add(File.separatorChar); |
90 String root = named_root_matcher.group(1); |
90 } |
91 rest = named_root_matcher.group(2); |
91 } |
92 result_path.append(File.separatorChar); |
92 |
93 result_path.append(File.separatorChar); |
93 public String check_root(String standard_path) |
94 result_path.append(root); |
94 { |
95 } |
95 String rest = standard_path; |
96 else { |
96 boolean is_root = standard_path.startsWith("/"); |
97 if (standard_path.startsWith("/")) { result_path.append(cygwin_root); } |
97 |
98 rest = standard_path; |
98 if (is_windows()) { |
99 } |
99 Pattern cygdrive_pattern = Pattern.compile("/cygdrive/([a-zA-Z])($|/.*)"); |
100 |
100 Matcher cygdrive_matcher = cygdrive_pattern.matcher(standard_path); |
101 for (String p : rest.split("/", -1)) { |
101 |
102 if (!p.isEmpty()) { |
102 Pattern named_root_pattern = Pattern.compile("//+([^/]*)(.*)"); |
103 int len = result_path.length(); |
103 Matcher named_root_matcher = named_root_pattern.matcher(standard_path); |
104 if (len > 0 && result_path.charAt(len - 1) != File.separatorChar) { |
104 |
105 result_path.append(File.separatorChar); |
105 if (cygdrive_matcher.matches()) { |
|
106 String drive = cygdrive_matcher.group(1).toUpperCase(Locale.ROOT); |
|
107 rest = cygdrive_matcher.group(2); |
|
108 clear(); |
|
109 add(drive); |
|
110 add(':'); |
|
111 add(File.separatorChar); |
|
112 } |
|
113 else if (named_root_matcher.matches()) { |
|
114 String root = named_root_matcher.group(1); |
|
115 rest = named_root_matcher.group(2); |
|
116 clear(); |
|
117 add(File.separatorChar); |
|
118 add(File.separatorChar); |
|
119 add(root); |
|
120 } |
|
121 else if (is_root) { |
|
122 clear(); |
|
123 add(_cygwin_root); |
|
124 } |
|
125 } |
|
126 else if (is_root) { |
|
127 clear(); |
|
128 add(File.separatorChar); |
|
129 } |
|
130 return rest; |
|
131 } |
|
132 |
|
133 public void check_rest(Map<String,String> env, String main) |
|
134 throws IOException, InterruptedException |
|
135 { |
|
136 for (String p : main.split("/", -1)) { |
|
137 if (env != null && p.startsWith("$")) { |
|
138 String var = p.substring(1); |
|
139 String res = env.getOrDefault(var, ""); |
|
140 if (res.isEmpty()) { |
|
141 throw new RuntimeException( |
|
142 "Bad Isabelle environment variable: " + quote(var)); |
106 } |
143 } |
107 result_path.append(p); |
144 else check(null, res); |
108 } |
145 } |
109 } |
146 else if (!p.isEmpty()) { |
110 |
147 separator(); |
111 return result_path.toString(); |
148 add(p); |
112 } |
149 } |
113 else { return standard_path; } |
150 } |
|
151 } |
|
152 |
|
153 public void check(Map<String,String> env, String path) |
|
154 throws IOException, InterruptedException |
|
155 { |
|
156 check_rest(env, check_root(path)); |
|
157 } |
|
158 } |
|
159 |
|
160 public static String expand_platform_path( |
|
161 Map<String,String> env, String cygwin_root, String standard_path) |
|
162 throws IOException, InterruptedException |
|
163 { |
|
164 Expand_Platform_Path expand = new Expand_Platform_Path(cygwin_root); |
|
165 expand.check(env, standard_path); |
|
166 return expand.result(); |
114 } |
167 } |
115 |
168 |
116 public static String join_paths(List<Path> paths) |
169 public static String join_paths(List<Path> paths) |
117 { |
170 { |
118 List<String> strs = new LinkedList<String>(); |
171 List<String> strs = new LinkedList<String>(); |
360 throws IOException, InterruptedException |
413 throws IOException, InterruptedException |
361 { |
414 { |
362 return standard_path(cygwin_root(), platform_path); |
415 return standard_path(cygwin_root(), platform_path); |
363 } |
416 } |
364 |
417 |
|
418 public static String expand_platform_path(String standard_path) |
|
419 throws IOException, InterruptedException |
|
420 { |
|
421 return expand_platform_path(settings(), cygwin_root(), standard_path); |
|
422 } |
|
423 |
365 public static String platform_path(String standard_path) |
424 public static String platform_path(String standard_path) |
366 throws IOException, InterruptedException |
425 throws IOException, InterruptedException |
367 { |
426 { |
368 return platform_path(cygwin_root(), standard_path); |
427 return expand_platform_path(null, cygwin_root(), standard_path); |
369 } |
428 } |
370 |
429 |
371 |
430 |
372 /* kill process (via bash) */ |
431 /* kill process (via bash) */ |
373 |
432 |