summaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
Diffstat (limited to 'tools')
-rw-r--r--tools/coq_makefile.ml48
-rw-r--r--tools/coqdep.ml44
-rw-r--r--tools/coqdoc/pretty.mll7
3 files changed, 50 insertions, 9 deletions
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index eb3a19fa..3ca1e7d3 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coq_makefile.ml4 12176 2009-06-09 09:44:40Z notin $ *)
+(* $Id: coq_makefile.ml4 12470 2009-11-05 15:50:20Z notin $ *)
(* créer un Makefile pour un développement Coq automatiquement *)
@@ -163,7 +163,7 @@ let install_include_by_root var files (_,inc_r) =
let ldir = List.assoc "." (List.map (fun (p,l,_) -> (p,l)) inc_r) in
let pdir = physical_dir_of_logical_dir ldir in
printf "\t(for i in $(%s); do \\\n" var;
- printf "\t install -D $$i $(COQLIB)/user-contrib/%s/$$i; \\\n" pdir;
+ printf "\t install -d `dirname $(COQLIB)/user-contrib/%s/$$i`; \\\n\t install $$i $(COQLIB)/user-contrib/%s/$$i; \\\n" pdir pdir;
printf "\t done)\n"
with Not_found ->
(* Files in the scope of a -R option (assuming they are disjoint) *)
@@ -172,12 +172,12 @@ let install_include_by_root var files (_,inc_r) =
begin
let pdir' = physical_dir_of_logical_dir ldir in
printf "\t(cd %s; for i in $(%s%d); do \\\n" pdir var i;
- printf "\t install -D $$i $(COQLIB)/user-contrib/%s/$$i; \\\n" pdir';
+ printf "\t install -d `dirname $(COQLIB)/user-contrib/%s/$$i`; \\\n\t install $$i $(COQLIB)/user-contrib/%s/$$i; \\\n" pdir' pdir';
printf "\t done)\n"
end) inc_r;
(* Files not in the scope of a -R option *)
printf "\t(for i in $(%s0); do \\\n" var;
- printf "\t install -D $$i $(COQLIB)/user-contrib/$(INSTALLDEFAULTROOT)/$$i; \\\n";
+ printf "\t install -d `dirname $(COQLIB)/user-contrib/$(INSTALLDEFAULTROOT)/$$i`; \\\n\t install $$i $(COQLIB)/user-contrib/$(INSTALLDEFAULTROOT)/$$i; \\\n";
printf "\t done)\n"
let install (vfiles,mlfiles,_,sds) inc =
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
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index c4a1a76f..b29e0734 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: pretty.mll 12187 2009-06-13 19:36:59Z msozeau $ i*)
+(*i $Id: pretty.mll 12908 2010-04-09 08:54:04Z herbelin $ i*)
(*s Utility functions for the scanners *)
@@ -126,7 +126,7 @@
Str.regexp "[ \t]*(\\*\\*[ \t]+printing[ \t]+\\([^ \t]+\\)"
let printing_token_re =
Str.regexp
- "[ \t]*\\(\\(%\\([^%]*\\)%\\)\\|\\(\\$[^$]*\\$\\)\\)?[ \t]*\\(#\\(\\([^#]\\|&#\\)*\\)#\\)?"
+ "[ \t]*\\(\\(%\\([^%]*\\)%\\)\\|\\(\\$[^$]*\\$\\)\\)?[ \t]*\\(#\\(\\(&#\\|[^#]\\)*\\)#\\)?"
let add_printing_token toks pps =
try
@@ -731,6 +731,9 @@ and body = parse
| token_no_brackets
{ let s = lexeme lexbuf in
symbol lexbuf s; body lexbuf }
+ | ".."
+ { Output.char '.'; Output.char '.';
+ body lexbuf }
| _ { let c = lexeme_char lexbuf 0 in
Output.char c;
body lexbuf }