summaryrefslogtreecommitdiff
path: root/tools/coqdep.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coqdep.ml')
-rw-r--r--tools/coqdep.ml44
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