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.ml6
-rw-r--r--tools/coqdoc/cdglobals.ml7
-rw-r--r--tools/coqdoc/main.ml10
-rw-r--r--tools/coqdoc/pretty.mll31
-rw-r--r--tools/gallina_lexer.mll4
6 files changed, 42 insertions, 24 deletions
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index 77dbcc47..d1d0d854 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 11136 2008-06-18 10:41:34Z herbelin $ *)
+(* $Id: coq_makefile.ml4 11255 2008-07-24 16:57:13Z notin $ *)
(* créer un Makefile pour un développement Coq automatiquement *)
@@ -156,7 +156,6 @@ let variables l =
| _ :: r -> var_aux r
in
section "Variables definitions.";
- print "CAMLP4LIB:=$(shell $(CAMLBIN)camlp5 -where 2> /dev/null || $(CAMLBIN)camlp4 -where)\n";
print "CAMLP4:=$(notdir $(CAMLP4LIB))\n";
if Coq_config.local then
(print "COQSRC:=$(COQTOP)\n";
@@ -175,7 +174,7 @@ let variables l =
-I $(COQTOP)/contrib/subtac -I $(COQTOP)/contrib/xml \\
-I $(CAMLP4LIB)\n")
else
- (print "COQSRC:=$(shell $(COQTOP)coqc -where)\n";
+ (print "COQSRC:=$(shell $(COQBIN)coqc -where)\n";
print "COQSRCLIBS:=-I $(COQSRC)\n");
print "ZFLAGS:=$(OCAMLLIBS) $(COQSRCLIBS)\n";
if !opt = "-byte" then
@@ -255,7 +254,8 @@ let include_dirs l =
let str_i' = parse_includes inc_i' in
let str_r = parse_includes inc_r in
section "Libraries definition.";
- print "OCAMLLIBS:="; print_list "\\\n " str_i; print "\n";
+ print "CAMLP4LIB:=$(shell $(CAMLBIN)camlp5 -where 2> /dev/null || $(CAMLBIN)camlp4 -where)\n";
+ print "OCAMLLIBS:=-I $(CAMLP4LIB) "; print_list "\\\n " str_i; print "\n";
print "COQLIBS:="; print_list "\\\n " str_i'; print " "; print_list "\\\n " str_r; print "\n";
print "COQDOCLIBS:="; print_list "\\\n " str_r; print "\n\n"
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index dc80476b..b4b161f5 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqdep.ml 10746 2008-04-03 15:45:25Z notin $ *)
+(* $Id: coqdep.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
open Printf
open Coqdep_lexer
@@ -442,8 +442,8 @@ let rec add_directory recur add_file phys_dir log_dir =
try
while true do
let f = readdir dirh in
- (* we avoid . .. and all hidden files and subdirs (e.g. .svn) *)
- if f.[0] <> '.' then
+ (* we avoid . .. and all hidden files and subdirs (e.g. .svn, _darcs) *)
+ if f.[0] <> '.' && f.[0] <> '_' then
let phys_f = phys_dir//f in
match try (stat phys_f).st_kind with _ -> S_BLK with
| S_DIR when recur -> add_directory recur add_file phys_f (log_dir@[f])
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index 44b9bd3c..3339b1db 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -32,6 +32,13 @@ let open_out_file f =
let close_out_file () = close_out !out_channel
+type glob_source_t =
+ | NoGlob
+ | DotGlob
+ | GlobFile of string
+
+let glob_source = ref DotGlob
+
let header_trailer = ref true
let header_file = ref ""
let header_file_spec = ref false
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 7111187f..81560259 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: main.ml 11024 2008-05-30 12:41:39Z msozeau $ i*)
+(*i $Id: main.ml 11236 2008-07-18 15:58:12Z notin $ i*)
(* Modified by Lionel Elie Mamane <lionel@mamane.lu> on 9 & 10 Mar 2004:
* - handling of absolute filenames (function coq_module)
@@ -50,6 +50,7 @@ let usage () =
prerr_endline " --tex <file> consider <file> as a .tex file";
prerr_endline " -p <string> insert <string> in LaTeX preamble";
prerr_endline " --files-from <file> read file names to process in <file>";
+ prerr_endline " --glob-from <file> read globalization information from <file>";
prerr_endline " --quiet quiet mode (default)";
prerr_endline " --verbose verbose mode";
prerr_endline " --no-externals no links to Coq standard library";
@@ -300,7 +301,7 @@ let parse () =
| "-R" :: ([] | [_]) ->
usage ()
| ("-glob-from" | "--glob-from") :: f :: rem ->
- obsolete "glob-from"; parse_rec rem
+ glob_source := GlobFile f; parse_rec rem
| ("-glob-from" | "--glob-from") :: [] ->
usage ()
| ("--no-externals" | "-no-externals" | "-noexternals") :: rem ->
@@ -436,7 +437,10 @@ let produce_document l =
Filename.concat !output_dir "coqdoc.sty"
else "coqdoc.sty" in
copy src dst);
- let l = List.map read_glob l in
+ (match !Cdglobals.glob_source with
+ | NoGlob -> ()
+ | DotGlob -> ignore (List.map read_glob l)
+ | GlobFile f -> ignore (Index.read_glob f));
List.iter index_module l;
match !out_to with
| StdOut ->
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index 8be3e0b0..baace5ba 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 11154 2008-06-19 18:42:19Z msozeau $ i*)
+(*i $Id: pretty.mll 11255 2008-07-24 16:57:13Z notin $ i*)
(*s Utility functions for the scanners *)
@@ -56,6 +56,7 @@
let formatted = ref false
let brackets = ref 0
+ let comment_level = ref 0
let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos
@@ -93,7 +94,8 @@
let reset () =
formatted := false;
- brackets := 0
+ brackets := 0;
+ comment_level := 0
(* erasing of Section/End *)
@@ -385,6 +387,7 @@ rule coq_bol = parse
| space* "(**" space+ "printing" space+
{ eprintf "warning: bad 'printing' command at character %d\n"
(lexeme_start lexbuf); flush stderr;
+ comment_level := 1;
ignore (comment lexbuf);
coq_bol lexbuf }
| space* "(**" space+ "remove" space+ "printing" space+
@@ -394,10 +397,12 @@ rule coq_bol = parse
| space* "(**" space+ "remove" space+ "printing" space+
{ eprintf "warning: bad 'remove printing' command at character %d\n"
(lexeme_start lexbuf); flush stderr;
+ comment_level := 1;
ignore (comment lexbuf);
coq_bol lexbuf }
| space* "(*"
- { let eol = comment lexbuf in
+ { comment_level := 1;
+ let eol = comment lexbuf in
if eol then coq_bol lexbuf else coq lexbuf }
| eof
{ () }
@@ -421,7 +426,8 @@ and coq = parse
Output.end_doc (); Output.start_coq ();
if eol then coq_bol lexbuf else coq lexbuf }
| "(*"
- { let eol = comment lexbuf in
+ { comment_level := 1;
+ let eol = comment lexbuf in
if eol then begin Output.line_break(); coq_bol lexbuf end
else coq lexbuf
}
@@ -556,7 +562,7 @@ and escaped_coq = parse
| "["
{ incr brackets; Output.char '['; escaped_coq lexbuf }
| "(*"
- { ignore (comment lexbuf); escaped_coq lexbuf }
+ { comment_level := 1; ignore (comment lexbuf); escaped_coq lexbuf }
| "*)"
{ (* likely to be a syntax error: we escape *) backtrack lexbuf }
| eof
@@ -591,16 +597,16 @@ and comments = parse
(*s Skip comments *)
and comment = parse
- | "(*" { comment lexbuf }
- | "*)" space* nl { true }
- | "*)" { false }
- | eof { false }
- | _ { comment lexbuf }
+ | "(*" { incr comment_level; comment lexbuf }
+ | "*)" space* nl { decr comment_level; if !comment_level > 0 then comment lexbuf else true }
+ | "*)" { decr comment_level; if !comment_level > 0 then comment lexbuf else false }
+ | eof { false }
+ | _ { comment lexbuf }
and skip_to_dot = parse
| '.' space* nl { true }
| eof | '.' space+ { false}
- | "(*" { ignore (comment lexbuf); skip_to_dot lexbuf }
+ | "(*" { comment_level := 1; ignore (comment lexbuf); skip_to_dot lexbuf }
| _ { skip_to_dot lexbuf }
and body_bol = parse
@@ -616,7 +622,8 @@ and body = parse
| '.' space* nl | '.' space* eof { Output.char '.'; Output.line_break(); true }
| '.' space+ { Output.char '.'; Output.char ' '; false }
| '"' { Output.char '"'; ignore(notation lexbuf); body lexbuf }
- | "(*" { let eol = comment lexbuf in
+ | "(*" { comment_level := 1;
+ let eol = comment lexbuf in
if eol
then begin Output.line_break(); body_bol lexbuf end
else body lexbuf }
diff --git a/tools/gallina_lexer.mll b/tools/gallina_lexer.mll
index 0b769dbd..7eaec2a8 100644
--- a/tools/gallina_lexer.mll
+++ b/tools/gallina_lexer.mll
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: gallina_lexer.mll 5920 2004-07-16 20:01:26Z herbelin $ *)
+(* $Id: gallina_lexer.mll 11301 2008-08-04 19:41:18Z herbelin $ *)
{
open Lexing
@@ -51,7 +51,7 @@ rule action = parse
cRcpt := 0; action lexbuf }
| [' ' '\t']* '\n' { if !cRcpt < 2 then print "\n";
cRcpt := !cRcpt+1; action lexbuf}
- | eof { raise Fin_fichier}
+ | eof { (raise Fin_fichier : unit)}
| _ { print (Lexing.lexeme lexbuf); cRcpt := 0; action lexbuf }
and comment = parse