diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_makefile.ml4 | 8 | ||||
| -rw-r--r-- | tools/coqdep.ml | 44 | ||||
| -rw-r--r-- | tools/coqdoc/pretty.mll | 7 |
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 } |