coqdep -slash

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9276 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 35 insertions, 18 deletions

diff --git a/man/coqdep.1 b/man/coqdep.1
index 01d080fc2..6ae89f8bd 100644
--- a/man/coqdep.1
+++ b/man/coqdep.1
@@ -23,6 +23,9 @@ coqdep \- Compute inter-module dependencies for Coq and Caml programs
 [
 .BI \-D
 ]
+[
+.BI \-slash
+]
 .I filename ...
 .I directory ...
 
@@ -37,10 +40,11 @@ When a directory is given as argument, it is recursively looked at.
 Dependencies of Coq modules are computed by looking at
 .IR Require \&
 commands (Require, Require Export, Require Import, Require Implementation),
-and
 .IR Declare \& 
 .IR ML \& 
 .IR Module \&
+commands and
+.IR Load \&
 commands. Dependencies relative to modules from the Coq library are not
 printed.
 
@@ -54,8 +58,7 @@ directives and the dot notation
 .TP
 .BI \-c
 Prints the dependencies of Caml modules.
-(On Caml modules, the behaviour is exactly the same as cldepend,
-except that nested comments and strings are correctly handled).
+(On Caml modules, the behaviour is exactly the same as ocamldep).
 .TP
 .BI \-w
 Prints a warning if a Coq command
@@ -78,6 +81,10 @@ of each Coq file given as argument and complete (if needed)
 the list of Caml modules. The new command is printed on
 the standard output. No dependency is computed with this option.
 .TP 
+.BI \-slash
+Prints paths using a slash instead of the OS specific separator. This
+option is useful when developping under Cygwin.
+.TP
 .BI \-I \ directory
 The files .v .ml .mli of the directory
 .IR directory \&
@@ -87,7 +94,7 @@ but their own dependencies are not printed.
 .BI \-coqlib \ directory
 Indicates where is the Coq library. The default value has been
 determined at installation time, and therefore this option should not
-be used.
+be used under normal circumstances.
 
 
 .SH SEE ALSO
@@ -120,7 +127,7 @@ Consider the files (in the same directory):
 where
 .TP
 .BI \+ 
-D.ml contains the commands `#open "A"', `#open "B"' and `type t = C__t' ;
+D.ml contains the commands `open A', `open B' and `type t = C.t' ;
 .TP
 .BI \+
 Y.v contains the command `Require X' ;
@@ -135,7 +142,7 @@ example% coqdep -I . *.v
 .RS
 .sp .5
 .nf
-.B Z.vo: Z.v ./X.vo ./D.zo
+.B Z.vo: Z.v ./X.vo ./D.cmo
 .B Y.vo: Y.v ./X.vo
 .B X.vo: X.v
 .fi
@@ -150,7 +157,7 @@ example% coqdep -w -I . *.v
 .RS
 .sp .5
 .nf
-.B Z.vo: Z.v ./X.vo ./D.zo
+.B Z.vo: Z.v ./X.vo ./D.cmo
 .B Y.vo: Y.v ./X.vo
 .B X.vo: X.v
 ### Warning : In file Z.v, the ML modules declaration should be
@@ -167,10 +174,14 @@ example% coqdep -c -I . *.ml
 .RS
 .sp .5
 .nf
-.B D.zo: D.ml ./A.zo ./B.zo ./C.zo
-.B C.zo: C.ml
-.B B.zo: B.ml
-.B A.zo: A.ml
+.B D.cmo: D.ml ./A.cmo ./B.cmo ./C.cmo
+.B D.cmx: D.ml ./A.cmx ./B.cmx ./C.cmx
+.B C.cmo: C.ml
+.B C.cmx: C.ml
+.B B.cmo: B.ml
+.B B.cmx: B.ml
+.B A.cmo: A.ml
+.B A.cmx: A.ml
 .fi
 .RE
 .br
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index a3089f713..423035fab 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -12,12 +12,6 @@ open Printf
 open Coqdep_lexer
 open Unix
 
-let (/) = Filename.concat
-
-let file_concat l =
-  if l=[] then "<empty>" else
-    List.fold_left (/) (List.hd l) (List.tl l)
-
 let stderr = Pervasives.stderr
 let stdout = Pervasives.stdout
 
@@ -28,12 +22,23 @@ let option_D = ref false
 let option_w = ref false
 let option_i = ref false
 let option_sort = ref false
+let option_slash = ref false
 
 let suffixe = ref ".vo"
 let suffixe_spec = ref ".vi"
 
 type dir = string option
 
+(* filename for printing *)
+let (//) s1 s2 =
+  if !option_slash then s1^"/"^s2 else Filename.concat s1 s2
+
+let (/) = Filename.concat
+
+let file_concat l =
+  if l=[] then "<empty>" else
+    List.fold_left (//) (List.hd l) (List.tl l)
+
 (* Files specified on the command line *)
 let mlAccu  = ref ([] : (string * string * dir) list) 
 and mliAccu = ref ([] : (string * string * dir) list) 
@@ -148,7 +153,7 @@ let cut_prefix p s =
   if ls >= lp && String.sub s 0 lp = p then String.sub s lp (ls - lp) else s
 
 let canonize f = match Sys.os_type with
-  | "Win32" -> cut_prefix ".\\" f
+  | "Win32" when not !option_slash -> cut_prefix ".\\" f
   | _ -> cut_prefix "./" f
 
 let sort () = 
@@ -517,6 +522,7 @@ let coqdep () =
       | "-coqlib" :: [] -> usage ()
       | "-suffix" :: (s :: ll) -> suffixe := s ; suffixe_spec := s; parse ll
       | "-suffix" :: [] -> usage ()
+      | "-slash" :: ll -> option_slash := true; parse ll
       | f :: ll -> treat None f; parse ll
       | [] -> ()
   in