diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_makefile.ml4 | 8 | ||||
| -rw-r--r-- | tools/coqdep.ml | 6 | ||||
| -rw-r--r-- | tools/coqdoc/cdglobals.ml | 7 | ||||
| -rw-r--r-- | tools/coqdoc/main.ml | 10 | ||||
| -rw-r--r-- | tools/coqdoc/pretty.mll | 31 | ||||
| -rw-r--r-- | tools/gallina_lexer.mll | 4 |
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 |