diff options
Diffstat (limited to 'tools/coqdep.ml')
| -rw-r--r-- | tools/coqdep.ml | 44 |
1 files changed, 41 insertions, 3 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 4febe9d1..91a7e6d0 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqdep.ml 11749 2009-01-05 14:01:04Z notin $ *) +(* $Id: coqdep.ml 12916 2010-04-10 15:18:17Z herbelin $ *) open Printf open Coqdep_lexer @@ -60,7 +60,9 @@ let safe_hash_add clq q (k,v) = (k1,l1)::cltl when k=k1 -> (k1,v::l1)::cltl | cl::cltl -> cl::add_clash cltl | [] -> [(k,[v;v2])] in - clq := add_clash !clq + clq := add_clash !clq; + (* overwrite previous bindings, as coqc does *) + Hashtbl.add q k v with Not_found -> Hashtbl.add q k v (* Files found in the loadpaths *) @@ -167,6 +169,37 @@ let cut_prefix p s = let ls = String.length s in if ls >= lp && String.sub s 0 lp = p then String.sub s lp (ls - lp) else s +(* Makefile's escaping rules are awful: $ is escaped by doubling and + other special characters are escaped by backslash prefixing while + backslashes themselves must be escaped only if part of a sequence + followed by a special character (i.e. in case of ambiguity with a + use of it as escaping character). Moreover (even if not crucial) + it is apparently not possible to directly escape ';' and leading '\t'. *) + +let escape = + let s' = Buffer.create 10 in + fun s -> + Buffer.clear s'; + for i = 0 to String.length s - 1 do + let c = s.[i] in + if c = ' ' or c = '#' or c = ':' (* separators and comments *) + or c = '%' (* pattern *) + or c = '?' or c = '[' or c = ']' or c = '*' (* expansion in filenames *) + or i=0 && c = '~' && (String.length s = 1 || s.[1] = '/' || + 'A' <= s.[1] && s.[1] <= 'Z' || + 'a' <= s.[1] && s.[1] <= 'z') (* homedir expansion *) + then begin + let j = ref (i-1) in + while !j >= 0 && s.[!j] = '\\' do + Buffer.add_char s' '\\'; decr j (* escape all preceding '\' *) + done; + Buffer.add_char s' '\\'; + end; + if c = '$' then Buffer.add_char s' '$'; + Buffer.add_char s' c + done; + Buffer.contents s' + let canonize f = let f' = absolute_dir (Filename.dirname f) // Filename.basename f in match List.filter (fun (_,full) -> f' = full) !vAccu with @@ -423,6 +456,11 @@ let add_coqlib_known phys_dir log_dir f = Hashtbl.add coqlibKnown [basename] (); Hashtbl.add coqlibKnown name () +let rec suffixes = function + | [] -> assert false + | [name] -> [[name]] + | dir::suffix as l -> l::suffixes suffix + let add_known phys_dir log_dir f = if (Filename.check_suffix f ".ml" || Filename.check_suffix f ".mli" || Filename.check_suffix f ".ml4") then let basename = make_ml_module_name f in @@ -431,7 +469,7 @@ let add_known phys_dir log_dir f = let basename = Filename.chop_suffix f ".v" in let name = log_dir@[basename] in let file = phys_dir//basename in - let paths = [name;[basename]] in + let paths = suffixes name in List.iter (fun n -> safe_hash_add clash_v vKnown (n,file)) paths |