summaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /tools
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'tools')
-rw-r--r--tools/coq-tex.ml42
-rw-r--r--tools/coq_makefile.ml4439
-rw-r--r--tools/coqdep.ml396
-rwxr-xr-xtools/coqdep_lexer.mll4
-rw-r--r--tools/coqdoc/cdglobals.ml8
-rw-r--r--tools/coqdoc/coqdoc.sty126
-rw-r--r--tools/coqdoc/index.mli18
-rw-r--r--tools/coqdoc/index.mll145
-rw-r--r--tools/coqdoc/main.ml391
-rw-r--r--tools/coqdoc/output.ml193
-rw-r--r--tools/coqdoc/pretty.mll319
-rw-r--r--tools/coqwc.mll2
12 files changed, 1190 insertions, 853 deletions
diff --git a/tools/coq-tex.ml4 b/tools/coq-tex.ml4
index d55901b9..4c11725c 100644
--- a/tools/coq-tex.ml4
+++ b/tools/coq-tex.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coq-tex.ml4 9551 2007-01-29 15:13:35Z bgregoir $ *)
+(* $Id: coq-tex.ml4 9532 2007-01-24 16:04:29Z bgregoir $ *)
(* coq-tex
* JCF, 16/1/98
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index b6af3abc..77dbcc47 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 10185 2007-10-06 18:05:13Z herbelin $ *)
+(* $Id: coq_makefile.ml4 11136 2008-06-18 10:41:34Z herbelin $ *)
(* créer un Makefile pour un développement Coq automatiquement *)
@@ -81,21 +81,10 @@ coq_makefile [subdirectory] .... [file.v] ... [file.ml] ... [-custom
let standard sds sps =
print "byte:\n";
- print "\t$(MAKE) all \"OPT=\"\n\n";
+ print "\t$(MAKE) all \"OPT:=-byte\"\n\n";
print "opt:\n";
if !opt = "" then print "\t@echo \"WARNING: opt is disabled\"\n";
- print "\t$(MAKE) all \"OPT="; print !opt; print "\"\n\n";
- if !some_file then print "include .depend\n\n";
- print ".depend depend:\n";
- if !some_file then begin
- print "\trm -f .depend\n";
- print "\t$(COQDEP) -i $(COQLIBS) $(VFILES) *.ml *.mli >.depend\n";
- print "\t$(COQDEP) $(COQLIBS) -suffix .html $(VFILES) >>.depend\n";
- end;
- List.iter
- (fun x -> print "\t(cd "; print x; print " ; $(MAKE) depend)\n")
- sds;
- print "\n";
+ print "\t$(MAKE) all \"OPT:="; print !opt; print "\"\n\n";
print "install:\n";
print "\tmkdir -p `$(COQC) -where`/user-contrib\n";
if !some_vfile then print "\tcp -f $(VOFILES) `$(COQC) -where`/user-contrib\n";
@@ -116,7 +105,11 @@ let standard sds sps =
end;
print "clean:\n";
print "\trm -f *.cmo *.cmi *.cmx *.o $(VOFILES) $(VIFILES) $(GFILES) *~\n";
- print "\trm -f all.ps all-gal.ps $(HTMLFILES) $(GHTMLFILES)\n";
+ print "\trm -f all.ps all-gal.ps all.glob $(VFILES:.v=.glob) $(HTMLFILES) \
+ $(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) $(VFILES:.v=.v.d)\n";
+ if !some_mlfile then
+ print "\trm -f $(CMOFILES) $(MLFILES:.ml=.cmi) $(MLFILES:.ml=.ml.d)\n";
+ print "\t- rm -rf html\n";
List.iter
(fun (file,_,_) -> print "\t- rm -f "; print file; print "\n")
sps;
@@ -129,44 +122,32 @@ let standard sds sps =
List.iter
(fun x -> print "\t(cd "; print x; print " ; $(MAKE) archclean)\n")
sds;
- print "\n";
- print "html:\n";
- List.iter
- (fun x -> print "\t(cd "; print x; print " ; $(MAKE) html)\n")
- sds;
- print "\n"
+ print "\n\n"
+
+let includes () =
+ if !some_vfile then print "-include $(VFILES:.v=.v.d)\n.SECONDARY: $(VFILES:.v=.v.d)\n\n";
+ if !some_mlfile then print "-include $(MLFILES:.ml=.ml.d)\n.SECONDARY: $(MLFILES:.ml=.ml.d)\n\n"
let implicit () =
let ml_rules () =
- print ".mli.cmi:\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
- print ".ml.cmo:\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\n\n";
- print ".ml.cmx:\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\n\n";
+ print "%.cmi: %.mli\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
+ print "%.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\n\n";
+ print "%.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\n\n";
+ print "%.ml.d: %.ml\n";
+ print "\t$(CAMLBIN)ocamldep -slash $(ZFLAGS) $(PP) \"$<\" > \"$@\"\n\n"
and v_rule () =
- print ".v.vo:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n";
- print ".v.vi:\n\t$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*\n\n";
- print ".v.g:\n\t$(GALLINA) $<\n\n";
- print ".v.tex:\n\t$(COQDOC) -latex $< -o $@\n\n";
- print ".v.html:\n\t$(COQDOC) -html $< -o $@\n\n";
- print ".v.g.tex:\n\t$(COQDOC) -latex -g $< -o $@\n\n";
- print ".v.g.html:\n\t$(COQDOC) -html -g $< -o $@\n\n"
- and ml_suffixes =
- if !some_mlfile then
- [ ".mli"; ".ml"; ".cmo"; ".cmi"; ".cmx" ]
- else
- []
- and v_suffixes =
- if !some_vfile then
- [ ".v"; ".vo"; ".vi"; ".g"; ".html"; ".tex"; ".g.tex"; ".g.html" ]
- else
- []
+ print "%.vo %.glob: %.v\n\t$(COQC) -dump-glob $*.glob $(COQDEBUG) $(COQFLAGS) $*\n\n";
+ print "%.vi: %.v\n\t$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*\n\n";
+ print "%.g: %.v\n\t$(GALLINA) $<\n\n";
+ print "%.tex: %.v\n\t$(COQDOC) -latex $< -o $@\n\n";
+ print "%.html: %.v %.glob\n\t$(COQDOC) -glob-from $*.glob -html $< -o $@\n\n";
+ print "%.g.tex: %.v\n\t$(COQDOC) -latex -g $< -o $@\n\n";
+ print "%.g.html: %.v %.glob\n\t$(COQDOC) -glob-from $*.glob -html -g $< -o $@\n\n";
+ print "%.v.d: %.v\n";
+ print "\t$(COQDEP) -glob -slash $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"
in
- let suffixes = ml_suffixes @ v_suffixes in
- if suffixes <> [] then begin
- print ".SUFFIXES: "; print_list " " suffixes;
- print "\n\n"
- end;
- if !some_mlfile then ml_rules ();
- if !some_vfile then v_rule ()
+ if !some_mlfile then ml_rules ();
+ if !some_vfile then v_rule ()
let variables l =
let rec var_aux = function
@@ -174,71 +155,122 @@ let variables l =
| Def(v,def) :: r -> print v; print "="; print def; print "\n"; var_aux r
| _ :: r -> var_aux r
in
- section "Variables definitions.";
- print "CAMLP4LIB=`camlp5 -where 2> /dev/null || camlp4 -where`\n";
- print "CAMLP4=`basename $CAMLP4LIB`\n";
- print "COQSRC=-I $(COQTOP)/kernel -I $(COQTOP)/lib \\
+ 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";
+ print "COQSRCLIBS:=-I $(COQTOP)/kernel -I $(COQTOP)/lib \\
-I $(COQTOP)/library -I $(COQTOP)/parsing \\
-I $(COQTOP)/pretyping -I $(COQTOP)/interp \\
- -I $(COQTOP)/proofs -I $(COQTOP)/syntax -I $(COQTOP)/tactics \\
- -I $(COQTOP)/toplevel -I $(COQTOP)/contrib/correctness \\
- -I $(COQTOP)/contrib/extraction -I $(COQTOP)/contrib/field \\
- -I $(COQTOP)/contrib/fourier -I $(COQTOP)/contrib/graphs \\
+ -I $(COQTOP)/proofs -I $(COQTOP)/tactics \\
+ -I $(COQTOP)/toplevel -I $(COQTOP)/contrib/cc \\
+ -I $(COQTOP)/contrib/dp -I $(COQTOP)/contrib/extraction \\
+ -I $(COQTOP)/contrib/field -I $(COQTOP)/contrib/firstorder \\
+ -I $(COQTOP)/contrib/fourier -I $(COQTOP)/contrib/funind \\
-I $(COQTOP)/contrib/interface -I $(COQTOP)/contrib/jprover \\
- -I $(COQTOP)/contrib/omega -I $(COQTOP)/contrib/romega \\
- -I $(COQTOP)/contrib/ring -I $(COQTOP)/contrib/xml \\
- -I $(CAMLP4LIB)\n";
- print "ZFLAGS=$(OCAMLLIBS) $(COQSRC)\n";
- if !opt = "-byte" then
- print "override OPT=-byte\n"
- else
- print "OPT=\n";
- if !impredicative_set = true then print "OTHERFLAGS=-impredicative-set\n";
- print "COQFLAGS=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n";
- print "COQC=$(COQBIN)coqc\n";
- print "GALLINA=gallina\n";
- print "COQDOC=$(COQBIN)coqdoc\n";
- print "CAMLC=ocamlc -c\n";
- print "CAMLOPTC=ocamlopt -c\n";
- print "CAMLLINK=ocamlc\n";
- print "CAMLOPTLINK=ocamlopt\n";
- print "COQDEP=$(COQBIN)coqdep -c\n";
- print "GRAMMARS=grammar.cma\n";
- print "CAMLP4EXTEND=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n";
- print "PP=-pp \"$(CAMLP4)o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n";
- var_aux l;
- print "\n"
+ -I $(COQTOP)/contrib/micromega -I $(COQTOP)/contrib/omega \\
+ -I $(COQTOP)/contrib/ring -I $(COQTOP)/contrib/romega \\
+ -I $(COQTOP)/contrib/rtauto -I $(COQTOP)/contrib/setoid_ring \\
+ -I $(COQTOP)/contrib/subtac -I $(COQTOP)/contrib/xml \\
+ -I $(CAMLP4LIB)\n")
+ else
+ (print "COQSRC:=$(shell $(COQTOP)coqc -where)\n";
+ print "COQSRCLIBS:=-I $(COQSRC)\n");
+ print "ZFLAGS:=$(OCAMLLIBS) $(COQSRCLIBS)\n";
+ if !opt = "-byte" then
+ print "override OPT:=-byte\n"
+ else
+ print "OPT:=\n";
+ if !impredicative_set = true then print "OTHERFLAGS=-impredicative-set\n";
+ (* Coq executables and relative variables *)
+ print "COQFLAGS:=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n";
+ print "COQC:=$(COQBIN)coqc\n";
+ print "COQDEP:=$(COQBIN)coqdep -c\n";
+ print "GALLINA:=$(COQBIN)gallina\n";
+ print "COQDOC:=$(COQBIN)coqdoc\n";
+ (* Caml executables and relative variables *)
+ printf "CAMLC:=$(CAMLBIN)ocamlc -rectypes -c\n";
+ printf "CAMLOPTC:=$(CAMLBIN)ocamlopt -rectypes -c\n";
+ printf "CAMLLINK:=$(CAMLBIN)ocamlc -rectypes\n";
+ printf "CAMLOPTLINK:=$(CAMLBIN)ocamlopt -rectypes\n";
+ print "GRAMMARS:=grammar.cma\n";
+ print "CAMLP4EXTEND:=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n";
+
+ (if Coq_config.local then
+ print "PP:=-pp \"$(CAMLBIN)$(CAMLP4)o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n"
+ else
+ print "PP:=-pp \"$(CAMLBIN)$(CAMLP4)o -I . -I $(COQSRC) $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n");
+ var_aux l;
+ print "\n"
+
+let absolute_dir dir =
+ let current = Sys.getcwd () in
+ Sys.chdir dir;
+ let dir' = Sys.getcwd () in
+ Sys.chdir current;
+ dir'
+
+let is_prefix dir1 dir2 =
+ let l1 = String.length dir1 in
+ let l2 = String.length dir2 in
+ dir1 = dir2 or (l1 < l2 & String.sub dir2 0 l1 = dir1 & dir2.[l1] = '/')
+
+let is_included dir = function
+ | RInclude (dir',_) -> is_prefix (absolute_dir dir') (absolute_dir dir)
+ | Include dir' -> absolute_dir dir = absolute_dir dir'
+ | _ -> false
+
+let dir_of_target t =
+ match t with
+ | RInclude (dir,_) -> dir
+ | Include dir -> dir
+ | _ -> assert false
let include_dirs l =
- let include_aux' includeR =
- let rec include_aux = function
- | [] -> []
- | Include x :: r -> ("-I " ^ x) :: (include_aux r)
- | RInclude (p,l) :: r when includeR ->
- let l' = if l = "" then "\"\"" else l in
- ("-R " ^ p ^ " " ^ l') :: (include_aux r)
- | _ :: r -> include_aux r
- in
- include_aux
+ let rec split_includes l =
+ match l with
+ | [] -> [], []
+ | Include _ as i :: rem ->
+ let ri, rr = split_includes rem in
+ (i :: ri), rr
+ | RInclude _ as r :: rem ->
+ let ri, rr = split_includes rem in
+ ri, (r :: rr)
+ | _ :: rem -> split_includes rem
+ in
+ let rec parse_includes l =
+ match l with
+ | [] -> []
+ | Include x :: rem -> ("-I " ^ x) :: parse_includes rem
+ | RInclude (p,l) :: rem ->
+ let l' = if l = "" then "\"\"" else l in
+ ("-R " ^ p ^ " " ^ l') :: parse_includes rem
+ | _ :: rem -> parse_includes rem
in
- let i_ocaml = "-I ." :: (include_aux' false l) in
- let i_coq = "-I ." :: (include_aux' true l) in
- section "Libraries definition.";
- print "OCAMLLIBS="; print_list "\\\n " i_ocaml; print "\n";
- print "COQLIBS="; print_list "\\\n " i_coq; print "\n\n"
+ let l' = if List.exists (is_included ".") l then l else Include "." :: l in
+ let inc_i, inc_r = split_includes l' in
+ let inc_i' = List.filter (fun i -> not (List.exists (fun i' -> is_included (dir_of_target i) i') inc_r)) inc_i in
+ let str_i = parse_includes inc_i in
+ 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 "COQLIBS:="; print_list "\\\n " str_i'; print " "; print_list "\\\n " str_r; print "\n";
+ print "COQDOCLIBS:="; print_list "\\\n " str_r; print "\n\n"
let rec special = function
| [] -> []
| Special (file,deps,com) :: r -> (file,deps,com) :: (special r)
| _ :: r -> special r
-
+
let custom sps =
let pr_sp (file,dependencies,com) =
print file; print ": "; print dependencies; print "\n";
print "\t"; print com; print "\n\n"
in
- if sps <> [] then section "Custom targets.";
- List.iter pr_sp sps
+ if sps <> [] then section "Custom targets.";
+ List.iter pr_sp sps
let subdirs l =
let rec subdirs_aux = function
@@ -249,69 +281,69 @@ let subdirs l =
print s; print ":\n\tcd "; print s; print " ; $(MAKE) all\n\n"
in
let sds = subdirs_aux l in
- if sds <> [] then section "Subdirectories.";
- List.iter pr_subdir sds;
- section "Special targets.";
- print ".PHONY: ";
- print_list " "
- ("all" :: "opt" :: "byte" :: "archclean" :: "clean" :: "install"
- :: "depend" :: "html" :: sds);
- print "\n\n";
- sds
+ if sds <> [] then section "Subdirectories.";
+ List.iter pr_subdir sds;
+ section "Special targets.";
+ print ".PHONY: ";
+ print_list " "
+ ("all" :: "opt" :: "byte" :: "archclean" :: "clean" :: "install"
+ :: "depend" :: "html" :: sds);
+ print "\n\n";
+ sds
-(* Extract gallina/html filenames (foo.v) from the list of all targets *)
-
-let rec other_files suff = function
- | V n :: r ->
- let f = (Filename.chop_suffix n ".vo") ^ suff in
- f :: (other_files suff r)
- | _ :: r ->
- other_files suff r
- | [] ->
- []
-
-let vfiles = other_files ".v"
-let gfiles = other_files ".g"
-let hfiles = other_files ".html"
-let tfiles = other_files ".tex"
-let vifiles = other_files ".vi"
-let gtfiles l = List.map (fun f -> f ^ ".tex") (gfiles l)
-let ghfiles l = List.map (fun f -> f ^ ".html") (gfiles l)
-let vofiles = other_files ".vo"
let all_target l =
- let rec fnames = function
- | ML n :: r -> n :: (fnames r)
- | Subdir n :: r -> n :: (fnames r)
- | V n :: r -> n :: (fnames r)
- | Special (n,_,_) :: r -> n :: (fnames r)
- | Include _ :: r -> fnames r
- | RInclude _ :: r -> fnames r
- | Def _ :: r -> fnames r
- | [] -> []
+ let rec parse_arguments l =
+ match l with
+ | ML n :: r -> let v,m,o = parse_arguments r in (v,n::m,o)
+ | Subdir n :: r -> let v,m,o = parse_arguments r in (v,m,n::o)
+ | V n :: r -> let v,m,o = parse_arguments r in (n::v,m,o)
+ | Special (n,_,_) :: r -> let v,m,o = parse_arguments r in (v,m,n::o)
+ | Include _ :: r -> parse_arguments r
+ | RInclude _ :: r -> parse_arguments r
+ | Def _ :: r -> parse_arguments r
+ | [] -> [],[],[]
in
- section "Definition of the \"all\" target.";
- print "VFILES="; print_list "\\\n " (vfiles l); print "\n";
- print "VOFILES=$(VFILES:.v=.vo)\n";
- print "VIFILES=$(VFILES:.v=.vi)\n";
- print "GFILES=$(VFILES:.v=.g)\n";
- print "HTMLFILES=$(VFILES:.v=.html)\n";
- print "GHTMLFILES=$(VFILES:.v=.g.html)\n";
- print "\n";
- print "all: "; print_list "\\\n " (fnames l);
- print "\n\n";
- if !some_vfile then begin
- print "spec: $(VIFILES)\n\n";
- print "gallina: $(GFILES)\n\n";
- print "html: $(HTMLFILES)\n\n";
- print "gallinahtml: $(GHTMLFILES)\n\n";
- print "all.ps: $(VFILES)\n";
- print "\t$(COQDOC) -ps -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n";
- print "all-gal.ps: $(VFILES)\n";
- print "\t$(COQDOC) -ps -g -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n";
- print "\n\n"
- end
-
+ let
+ vfiles, mlfiles, other_targets = parse_arguments l
+ in
+ section "Definition of the \"all\" target.";
+ if !some_vfile then
+ begin
+ print "VFILES:="; print_list "\\\n " vfiles; print "\n";
+ print "VOFILES:=$(VFILES:.v=.vo)\n";
+ print "GLOBFILES:=$(VFILES:.v=.glob)\n";
+ print "VIFILES:=$(VFILES:.v=.vi)\n";
+ print "GFILES:=$(VFILES:.v=.g)\n";
+ print "HTMLFILES:=$(VFILES:.v=.html)\n";
+ print "GHTMLFILES:=$(VFILES:.v=.g.html)\n"
+ end;
+ if !some_mlfile then
+ begin
+ print "MLFILES:="; print_list "\\\n " mlfiles; print "\n";
+ print "CMOFILES:=$(MLFILES:.ml=.cmo)\n";
+ end;
+ print "\nall: ";
+ if !some_vfile then print "$(VOFILES) ";
+ if !some_mlfile then print "$(CMOFILES) ";
+ print_list "\\\n " other_targets; print "\n";
+ if !some_vfile then
+ begin
+ print "spec: $(VIFILES)\n\n";
+ print "gallina: $(GFILES)\n\n";
+ print "html: $(GLOBFILES) $(VFILES)\n";
+ print "\t- mkdir html\n";
+ print "\t$(COQDOC) -toc -html $(COQDOCLIBS) -d html $(VFILES)\n\n";
+ print "gallinahtml: $(GLOBFILES) $(VFILES)\n";
+ print "\t- mkdir html\n";
+ print "\t$(COQDOC) -toc -html -g $(COQDOCLIBS) -d html $(VFILES)\n\n";
+ print "all.ps: $(VFILES)\n";
+ print "\t$(COQDOC) -toc -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n";
+ print "all-gal.ps: $(VFILES)\n";
+ print "\t$(COQDOC) -toc -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n";
+ print "\n\n"
+ end
+
let parse f =
let rec string = parser
| [< '' ' | '\n' | '\t' >] -> ""
@@ -333,8 +365,8 @@ let parse f =
in
let c = open_in f in
let res = args (Stream.of_channel c) in
- close_in c;
- res
+ close_in c;
+ res
let rec process_cmd_line = function
| [] ->
@@ -348,8 +380,16 @@ let rec process_cmd_line = function
| "-impredicative-set" :: r ->
impredicative_set := true; process_cmd_line r
| "-custom" :: com :: dependencies :: file :: r ->
- some_file := true;
- Special (file,dependencies,com) :: (process_cmd_line r)
+ let check_dep f =
+ if Filename.check_suffix f ".v" then
+ some_vfile := true
+ else if Filename.check_suffix f ".ml" then
+ some_mlfile := true
+ else
+ ()
+ in
+ List.iter check_dep (Str.split (Str.regexp "[ \t]+") dependencies);
+ Special (file,dependencies,com) :: (process_cmd_line r)
| "-I" :: d :: r ->
Include d :: (process_cmd_line r)
| "-R" :: p :: l :: r ->
@@ -369,45 +409,39 @@ let rec process_cmd_line = function
Def (v,def) :: (process_cmd_line r)
| f :: r ->
if Filename.check_suffix f ".v" then begin
- some_vfile := true;
- V (f^"o") :: (process_cmd_line r)
- end else if Filename.check_suffix f ".ml" then begin
- some_mlfile := true;
- ML ((Filename.chop_suffix f "ml")^"cmo") :: (process_cmd_line r)
+ some_vfile := true;
+ V f :: (process_cmd_line r)
+ end else if Filename.check_suffix f ".ml" then begin
+ some_mlfile := true;
+ ML f :: (process_cmd_line r)
end else
- Subdir f :: (process_cmd_line r)
-
+ Subdir f :: (process_cmd_line r)
+
let banner () =
print
-"##############################################################################
-## The Calculus of Inductive Constructions ##
-## ##
-## Projet Coq ##
-## ##
-## INRIA ENS-CNRS ##
-## Rocquencourt Lyon ##
-## ##
-## Coq V7 ##
-## ##
-## ##
-##############################################################################
+"##########################################################################
+## v # The Coq Proof Assistant ##
+## <O___,, # CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud ##
+## \\VV/ # ##
+## // # Makefile automagically generated by coq_makefile V8.2 ##
+##########################################################################
"
let warning () =
print "# WARNING\n#\n";
- print "# This Makefile has been automagically generated by coq_makefile\n";
+ print "# This Makefile has been automagically generated\n";
print "# Edit at your own risks !\n";
print "#\n# END OF WARNING\n\n"
-
+
let print_list l = List.iter (fun x -> print x; print " ") l
-
+
let command_line args =
print "#\n# This Makefile was generated by the command line :\n";
print "# coq_makefile ";
print_list args;
print "\n#\n\n"
-
+
let directories_deps l =
let print_dep f dep =
if dep <> [] then begin print f; print ": "; print_list dep; print "\n" end
@@ -426,32 +460,33 @@ let directories_deps l =
| _ :: l ->
iter acc l
in
- iter ([],[]) l
+ iter ([],[]) l
let do_makefile args =
let l = process_cmd_line args in
- banner ();
- warning ();
- command_line args;
- variables l;
- include_dirs l;
- all_target l;
- let sps = special l in
- custom sps;
- let sds = subdirs l in
- implicit ();
- standard sds sps;
- (* TEST directories_deps l; *)
- warning ();
- if not (!output_channel == stdout) then close_out !output_channel;
- exit 0
-
+ banner ();
+ warning ();
+ command_line args;
+ include_dirs l;
+ variables l;
+ all_target l;
+ let sps = special l in
+ custom sps;
+ let sds = subdirs l in
+ implicit ();
+ standard sds sps;
+ (* TEST directories_deps l; *)
+ includes ();
+ warning ();
+ if not (!output_channel == stdout) then close_out !output_channel;
+ exit 0
+
let main () =
let args =
if Array.length Sys.argv = 1 then usage ();
List.tl (Array.to_list Sys.argv)
in
- do_makefile args
-
+ do_makefile args
+
let _ = Printexc.catch main ()
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index e787cdb3..dc80476b 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqdep.ml 10196 2007-10-08 13:50:39Z notin $ *)
+(* $Id: coqdep.ml 10746 2008-04-03 15:45:25Z notin $ *)
open Printf
open Coqdep_lexer
@@ -22,9 +22,9 @@ let option_D = ref false
let option_w = ref false
let option_i = ref false
let option_sort = ref false
+let option_glob = ref false
let option_slash = ref false
-
-let directories_added = ref false
+let option_boot = ref false
let suffixe = ref ".vo"
let suffixe_spec = ref ".vi"
@@ -41,6 +41,12 @@ let file_concat l =
if l=[] then "<empty>" else
List.fold_left (//) (List.hd l) (List.tl l)
+let make_ml_module_name filename =
+ (* Computes a ML Module name from its physical name *)
+ let fn = try Filename.chop_extension filename with _ -> filename in
+ let bn = Filename.basename fn in
+ String.capitalize bn
+
(* Files specified on the command line *)
let mlAccu = ref ([] : (string * string * dir) list)
and mliAccu = ref ([] : (string * string * dir) list)
@@ -49,28 +55,29 @@ and vAccu = ref ([] : (string * string) list)
(* Queue operations *)
let addQueue q v = q := v :: !q
-let safe_addQueue clq q (k,v) =
+let safe_hash_add clq q (k,v) =
try
- let v2 = List.assoc k !q in
+ let v2 = Hashtbl.find q k in
if v<>v2 then
let rec add_clash = function
(k1,l1)::cltl when k=k1 -> (k1,v::l1)::cltl
| cl::cltl -> cl::add_clash cltl
| [] -> [(k,[v;v2])] in
clq := add_clash !clq
- with Not_found -> addQueue q (k,v)
+ with Not_found -> Hashtbl.add q k v
(* Files found in the loadpaths *)
-let mlKnown = ref ([] : (string * dir) list)
-and mliKnown = ref ([] : (string * dir) list)
-and vKnown = ref ([] : (string list * string) list)
-and coqlibKnown = ref ([] : (string list * string) list)
+
+let mlKnown = (Hashtbl.create 19 : (string, dir) Hashtbl.t)
+let mliKnown = (Hashtbl.create 19 : (string, dir) Hashtbl.t)
+let vKnown = (Hashtbl.create 19 : (string list, string) Hashtbl.t)
+let coqlibKnown = (Hashtbl.create 19 : (string list, unit) Hashtbl.t)
let clash_v = ref ([]: (string list * string list) list)
let warning_module_notfound f s =
- eprintf "*** Warning : in file %s, module " f;
+ eprintf "*** Warning : in file %s, library " f;
eprintf "%s.v is required and has not been found in loadpath !\n"
(String.concat "." s);
flush stderr
@@ -88,7 +95,7 @@ let warning_clash file dir =
let d2 = Filename.dirname f2 in
let dl = List.map Filename.dirname (List.rev fl) in
eprintf
- "*** Warning : in file %s, \n required module %s is ambiguous!\n (found %s.v in "
+ "*** Warning : in file %s, \n required library %s is ambiguous!\n (found %s.v in "
file (String.concat "." dir) f;
List.iter (fun s -> eprintf "%s, " s) dl;
eprintf "%s and %s)\n" d2 d1
@@ -96,15 +103,14 @@ let warning_clash file dir =
let safe_assoc verbose file k =
if verbose && List.mem_assoc k !clash_v then warning_clash file k;
- List.assoc k !vKnown
-
+ Hashtbl.find vKnown k
let absolute_dir dir =
let current = Sys.getcwd () in
- Sys.chdir dir;
- let dir' = Sys.getcwd () in
- Sys.chdir current;
- dir'
+ Sys.chdir dir;
+ let dir' = Sys.getcwd () in
+ Sys.chdir current;
+ dir'
let absolute_file_name basename odir =
let dir = match odir with Some dir -> dir | None -> "." in
@@ -130,23 +136,23 @@ let traite_fichier_ML md ext =
else begin
addQueue deja_vu str;
begin try
- let mlidir = List.assoc str !mliKnown in
+ let mlidir = Hashtbl.find mliKnown str in
let filename = file_name ([str],mlidir) in
a_faire := !a_faire ^ " " ^ filename ^ ".cmi";
with Not_found ->
try
- let mldir = List.assoc str !mlKnown in
+ let mldir = Hashtbl.find mlKnown str in
let filename = file_name ([str],mldir) in
a_faire := !a_faire ^ " " ^ filename ^ ".cmo";
with Not_found -> ()
end;
begin try
- let mldir = List.assoc str !mlKnown in
+ let mldir = Hashtbl.find mlKnown str in
let filename = file_name ([str],mldir) in
a_faire_opt := !a_faire_opt ^ " " ^ filename ^ ".cmx"
with Not_found ->
try
- let mlidir = List.assoc str !mliKnown in
+ let mlidir = Hashtbl.find mliKnown str in
let filename = file_name ([str],mlidir) in
a_faire_opt := !a_faire_opt ^ " " ^ filename ^ ".cmi"
with Not_found -> ()
@@ -184,7 +190,7 @@ let sort () =
| Require (_, sl) ->
List.iter
(fun s ->
- try loop (List.assoc s !vKnown)
+ try loop (Hashtbl.find vKnown s)
with Not_found -> ())
sl
| RequireString (_, s) -> loop s
@@ -216,7 +222,7 @@ let traite_fichier_Coq verbose f =
printf " %s%s" (canonize file_str)
(if spec then !suffixe_spec else !suffixe)
with Not_found ->
- if verbose && not (List.mem_assoc str !coqlibKnown) then
+ if verbose && not (Hashtbl.mem coqlibKnown str) then
warning_module_notfound f str
end) strl
| RequireString (spec,s) ->
@@ -224,30 +230,31 @@ let traite_fichier_Coq verbose f =
if not (List.mem [str] !deja_vu_v) then begin
addQueue deja_vu_v [str];
try
- let file_str = List.assoc [str] !vKnown in
+ let file_str = Hashtbl.find vKnown [str] in
printf " %s%s" (canonize file_str)
(if spec then !suffixe_spec else !suffixe)
with Not_found ->
- begin try let _ = List.assoc [str] !coqlibKnown in ()
- with Not_found -> warning_notfound f s end
+ if not (Hashtbl.mem coqlibKnown [str]) then
+ warning_notfound f s
end
| Declare sl ->
List.iter
(fun str ->
- if not (List.mem str !deja_vu_ml) then begin
- addQueue deja_vu_ml str;
- try
- let mldir = List.assoc str !mlKnown in
- printf " %s.cmo" (file_name ([str],mldir))
- with Not_found -> ()
- end)
+ let s = make_ml_module_name str in
+ if not (List.mem s !deja_vu_ml) then begin
+ addQueue deja_vu_ml s;
+ try
+ let mldir = Hashtbl.find mlKnown s in
+ printf " %s.cmo" (file_name ([String.uncapitalize s],mldir))
+ with Not_found -> ()
+ end)
sl
| Load str ->
let str = Filename.basename str in
if not (List.mem [str] !deja_vu_v) then begin
addQueue deja_vu_v [str];
try
- let file_str = List.assoc [str] !vKnown in
+ let file_str = Hashtbl.find vKnown [str] in
printf " %s.v" (canonize file_str)
with Not_found -> ()
end
@@ -304,36 +311,37 @@ let traite_Declare f =
let decl_list = ref ([] : string list) in
let rec treat = function
| s :: ll ->
- if (List.mem_assoc s !mlKnown) & not (List.mem s !decl_list) then begin
- let mldir = List.assoc s !mlKnown in
- let fullname = file_name ([s],mldir) in
- let depl = mL_dep_list s (fullname ^ ".ml") in
- treat depl;
- decl_list := s :: !decl_list
- end;
- treat ll
+ let s' = make_ml_module_name s in
+ if (Hashtbl.mem mlKnown s') & not (List.mem s' !decl_list) then begin
+ let mldir = Hashtbl.find mlKnown s in
+ let fullname = file_name ([(String.uncapitalize s')],mldir) in
+ let depl = mL_dep_list s (fullname ^ ".ml") in
+ treat depl;
+ decl_list := s :: !decl_list
+ end;
+ treat ll
| [] -> ()
in
- try
- let chan = open_in f in
- let buf = Lexing.from_channel chan in
- begin try
- while true do
- let tok = coq_action buf in
- (match tok with
- | Declare sl ->
- decl_list := [];
- treat sl;
- decl_list := List.rev !decl_list;
- if !option_D then
- affiche_Declare f !decl_list
- else if !decl_list <> sl then
- warning_Declare f !decl_list
- | _ -> ())
- done
- with Fin_fichier -> () end;
- close_in chan
- with Sys_error _ -> ()
+ try
+ let chan = open_in f in
+ let buf = Lexing.from_channel chan in
+ begin try
+ while true do
+ let tok = coq_action buf in
+ (match tok with
+ | Declare sl ->
+ decl_list := [];
+ treat sl;
+ decl_list := List.rev !decl_list;
+ if !option_D then
+ affiche_Declare f !decl_list
+ else if !decl_list <> sl then
+ warning_Declare f !decl_list
+ | _ -> ())
+ done
+ with Fin_fichier -> () end;
+ close_in chan
+ with Sys_error _ -> ()
let file_mem (f,_,d) =
let rec loop = function
@@ -367,11 +375,12 @@ let mL_dependencies () =
let coq_dependencies () =
List.iter
(fun (name,_) ->
- printf "%s%s: %s.v" name !suffixe name;
+ let glob = if !option_glob then " "^name^".glob" else "" in
+ printf "%s%s%s: %s.v" name !suffixe glob name;
traite_fichier_Coq true (name ^ ".v");
printf "\n";
if !option_i then begin
- printf "%s%s: %s.v" name !suffixe_spec name;
+ printf "%s%s%s: %s.v" name !suffixe_spec glob name;
traite_fichier_Coq false (name ^ ".v");
printf "\n";
end;
@@ -387,8 +396,8 @@ let declare_dependencies () =
let rec warning_mult suf l =
let tab = Hashtbl.create 151 in
- List.iter
- (fun (f,d) ->
+ Hashtbl.iter
+ (fun f d ->
begin try
let d' = Hashtbl.find tab f in
if (Filename.dirname (file_name ([f],d)))
@@ -400,163 +409,128 @@ let rec warning_mult suf l =
Hashtbl.add tab f d)
l
-(* Gives the list of all the directories under [dir], including [dir] *)
-let all_subdirs root_dir log_dir =
- let l = ref [(root_dir,[log_dir])] in
- let add f = l := f :: !l in
- let rec traverse phys_dir dir =
- let dirh = handle_unix_error opendir phys_dir in
- try
- while true do
- let f = readdir dirh in
- if f <> "." && f <> ".." then
- let file = dir@[f] in
- let filename = phys_dir//f in
- if (stat filename).st_kind = S_DIR then begin
- add (filename,file);
- traverse filename file
- end
- done
- with End_of_file ->
- closedir dirh
- in
- traverse root_dir [log_dir]; List.rev !l
-
let usage () =
eprintf
"[ usage: coqdep [-w] [-I dir] [-R dir coqdir] [-coqlib dir] [-c] [-i] [-D] <filename>+ ]\n";
flush stderr;
exit 1
-let add_coqlib_known dir_name f =
- let complete_name = dir_name//f in
- let lib_name = Filename.basename dir_name in
+let add_coqlib_known phys_dir log_dir f =
+ if Filename.check_suffix f ".vo" then
+ let basename = Filename.chop_suffix f ".vo" in
+ let name = log_dir@[basename] in
+ Hashtbl.add coqlibKnown [basename] ();
+ Hashtbl.add coqlibKnown name ()
+
+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
+ Hashtbl.add mlKnown basename (Some phys_dir)
+ else if Filename.check_suffix f ".v" then
+ 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
+ List.iter
+ (fun n -> safe_hash_add clash_v vKnown (n,file)) paths
+
+(* Visits all the directories under [dir], including [dir],
+ or just [dir] if [recur=false] *)
+
+let rec add_directory recur add_file phys_dir log_dir =
+ let dirh = opendir phys_dir in
+ try
+ while true do
+ let f = readdir dirh in
+ (* we avoid . .. and all hidden files and subdirs (e.g. .svn) *)
+ if 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])
+ | S_REG -> add_file phys_dir log_dir f
+ | _ -> ()
+ done
+ with End_of_file -> closedir dirh
+
+let add_dir add_file phys_dir log_dir =
+ try add_directory false add_file phys_dir log_dir with Unix_error _ -> ()
+
+let add_rec_dir add_file phys_dir log_dir =
+ handle_unix_error (add_directory true add_file phys_dir) log_dir
+
+let rec treat_file old_dirname old_name =
+ let name = Filename.basename old_name
+ and new_dirname = Filename.dirname old_name in
+ let dirname =
+ match (old_dirname,new_dirname) with
+ | (d, ".") -> d
+ | (None,d) -> Some d
+ | (Some d1,d2) -> Some (d1//d2)
+ in
+ let complete_name = file_name ([name],dirname) in
match try (stat complete_name).st_kind with _ -> S_BLK with
+ | S_DIR ->
+ (if name.[0] <> '.' then
+ let dir=opendir complete_name in
+ let newdirname =
+ match dirname with
+ | None -> name
+ | Some d -> d//name
+ in
+ try
+ while true do treat_file (Some newdirname) (readdir dir) done
+ with End_of_file -> closedir dir)
| S_REG ->
- if Filename.check_suffix f ".vo" then
- let basename = Filename.chop_suffix f ".vo" in
- addQueue coqlibKnown ([basename],complete_name);
- addQueue coqlibKnown (["Coq";lib_name;basename],complete_name)
+ if Filename.check_suffix name ".ml" then
+ let basename = Filename.chop_suffix name ".ml" in
+ addQueue mlAccu (basename,".ml",dirname)
+ else if Filename.check_suffix name ".ml4" then
+ let basename = Filename.chop_suffix name ".ml4" in
+ addQueue mlAccu (basename,".ml4",dirname)
+ else if Filename.check_suffix name ".mli" then
+ let basename = Filename.chop_suffix name ".mli" in
+ addQueue mliAccu (basename,".mli",dirname)
+ else if Filename.check_suffix name ".v" then
+ let basename = Filename.chop_suffix name ".v" in
+ let name = file_name ([basename],dirname) in
+ addQueue vAccu (name, absolute_file_name basename dirname)
| _ -> ()
-let add_coqlib_directory dir_name =
- match try (stat dir_name).st_kind with _ -> S_BLK with
- | S_DIR ->
- (let dir = opendir dir_name in
- try
- while true do add_coqlib_known dir_name (readdir dir) done
- with End_of_file -> closedir dir)
- | _ -> ()
+let rec parse = function
+ | "-c" :: ll -> option_c := true; parse ll
+ | "-D" :: ll -> option_D := true; parse ll
+ | "-w" :: ll -> option_w := true; parse ll
+ | "-i" :: ll -> option_i := true; parse ll
+ | "-boot" :: ll -> option_boot := true; parse ll
+ | "-sort" :: ll -> option_sort := true; parse ll
+ | "-glob" :: ll -> option_glob := true; parse ll
+ | "-I" :: r :: ll -> add_dir add_known r []; parse ll
+ | "-I" :: [] -> usage ()
+ | "-R" :: r :: ln :: ll -> add_rec_dir add_known r [ln]; parse ll
+ | "-R" :: ([] | [_]) -> usage ()
+ | "-coqlib" :: (r :: ll) -> coqlib := r; parse ll
+ | "-coqlib" :: [] -> usage ()
+ | "-suffix" :: (s :: ll) -> suffixe := s ; suffixe_spec := s; parse ll
+ | "-suffix" :: [] -> usage ()
+ | "-slash" :: ll -> option_slash := true; parse ll
+ | f :: ll -> treat_file None f; parse ll
+ | [] -> ()
let coqdep () =
- let lg_command = Array.length Sys.argv in
- if lg_command < 2 then usage ();
- let rec treat old_dirname old_name =
- let name = Filename.basename old_name
- and new_dirname = Filename.dirname old_name in
- let dirname =
- match (old_dirname,new_dirname) with
- | (d, ".") -> d
- | (None,d) -> Some d
- | (Some d1,d2) -> Some (d1//d2)
- in
- let complete_name = file_name ([name],dirname) in
- match try (stat complete_name).st_kind with _ -> S_BLK with
- | S_DIR ->
- (if name <> "." & name <> ".." then
- let dir=opendir complete_name in
- let newdirname =
- match dirname with
- | None -> name
- | Some d -> d//name
- in
- try
- while true do treat (Some newdirname) (readdir dir) done
- with End_of_file -> closedir dir)
- | S_REG ->
- if Filename.check_suffix name ".ml" then
- let basename = Filename.chop_suffix name ".ml" in
- addQueue mlAccu (basename,".ml",dirname)
- else if Filename.check_suffix name ".ml4" then
- let basename = Filename.chop_suffix name ".ml4" in
- addQueue mlAccu (basename,".ml4",dirname)
- else if Filename.check_suffix name ".mli" then
- let basename = Filename.chop_suffix name ".mli" in
- addQueue mliAccu (basename,".mli",dirname)
- else if Filename.check_suffix name ".v" then
- let basename = Filename.chop_suffix name ".v" in
- let name = file_name ([basename],dirname) in
- addQueue vAccu (name, absolute_file_name basename dirname)
- | _ -> ()
- in
- let add_known phys_dir log_dir f =
- let complete_name = phys_dir//f in
- match try (stat complete_name).st_kind with _ -> S_BLK with
- | S_REG ->
- if Filename.check_suffix f ".ml" then
- let basename = Filename.chop_suffix f ".ml" in
- addQueue mlKnown (basename,Some phys_dir)
- else if Filename.check_suffix f ".ml4" then
- let basename = Filename.chop_suffix f ".ml4" in
- addQueue mlKnown (basename,Some phys_dir)
- else if Filename.check_suffix f ".mli" then
- let basename = Filename.chop_suffix f ".mli" in
- addQueue mliKnown (basename,Some phys_dir)
- else if Filename.check_suffix f ".v" then
- 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
- List.iter
- (fun n -> safe_addQueue clash_v vKnown (n,file)) paths
- | _ -> () in
- let add_directory (phys_dir, log_dir) =
- directories_added := true;
- match try (stat phys_dir).st_kind with _ -> S_BLK with
- | S_DIR ->
- (let dir = opendir phys_dir in
- try
- while true do
- add_known phys_dir log_dir (readdir dir) done
- with End_of_file -> closedir dir)
- | _ -> ()
- in
- let add_rec_directory dir_name log_name =
- List.iter add_directory (all_subdirs dir_name log_name)
- in
- let rec parse = function
- | "-c" :: ll -> option_c := true; parse ll
- | "-D" :: ll -> option_D := true; parse ll
- | "-w" :: ll -> option_w := true; parse ll
- | "-i" :: ll -> option_i := true; parse ll
- | "-sort" :: ll -> option_sort := true; parse ll
- | "-I" :: r :: ll -> add_directory (r, []); parse ll
- | "-I" :: [] -> usage ()
- | "-R" :: r :: ln :: ll -> add_rec_directory r ln; parse ll
- | "-R" :: ([] | [_]) -> usage ()
- | "-coqlib" :: (r :: ll) -> coqlib := r; parse ll
- | "-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
- if not !directories_added then add_directory (".", []);
+ if Array.length Sys.argv < 2 then usage ();
parse (List.tl (Array.to_list Sys.argv));
- List.iter
- (fun (s,_) -> add_coqlib_directory s)
- (all_subdirs (!coqlib//"theories") "Coq");
- List.iter
- (fun (s,_) -> add_coqlib_directory s)
- (all_subdirs (!coqlib//"contrib") "Coq");
- add_coqlib_directory (!coqlib//"user-contrib");
- mliKnown := !mliKnown @ (List.map (fun (f,_,d) -> (f,d)) !mliAccu);
- mlKnown := !mlKnown @ (List.map (fun (f,_,d) -> (f,d)) !mlAccu);
- warning_mult ".mli" !mliKnown;
- warning_mult ".ml" !mlKnown;
-(* warning_mult ".v" (List.map (fun (s,d) -> (file_concat s, d))
- !vKnown);*)
+ if !option_boot then begin
+ add_rec_dir add_known "theories" ["Coq"];
+ add_rec_dir add_known "contrib" ["Coq"]
+ end else begin
+ add_rec_dir add_coqlib_known (!coqlib//"theories") ["Coq"];
+ add_rec_dir add_coqlib_known (!coqlib//"contrib") ["Coq"];
+ add_dir add_coqlib_known (!coqlib//"user-contrib") []
+ end;
+ List.iter (fun (f,_,d) -> Hashtbl.add mliKnown f d) !mliAccu;
+ List.iter (fun (f,_,d) -> Hashtbl.add mlKnown f d) !mlAccu;
+ warning_mult ".mli" mliKnown;
+ warning_mult ".ml" mlKnown;
if !option_sort then begin sort (); exit 0 end;
if !option_c && not !option_D then mL_dependencies ();
if not !option_D then coq_dependencies ();
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index 8ecab3b4..cc9f2175 100755
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: coqdep_lexer.mll 8737 2006-04-26 21:55:21Z herbelin $ i*)
+(*i $Id: coqdep_lexer.mll 10721 2008-03-26 14:40:30Z notin $ i*)
{
@@ -215,7 +215,7 @@ and modules = parse
| '"' [^'"']* '"'
{ let lex = (Lexing.lexeme lexbuf) in
let str = String.sub lex 1 (String.length lex - 2) in
- mllist := str :: !mllist; modules lexbuf }
+ mllist := str :: !mllist; modules lexbuf}
| _ { (Declare (List.rev !mllist)) }
and qual_id = parse
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index 8a774876..44b9bd3c 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -26,14 +26,18 @@ let out_to = ref MultFiles
let out_channel = ref stdout
let open_out_file f =
- let f = if !output_dir <> "" then Filename.concat !output_dir f else f in
+ let f = if !output_dir <> "" && Filename.is_relative f then Filename.concat !output_dir f else f in
out_channel := open_out f
let close_out_file () = close_out !out_channel
let header_trailer = ref true
-let quiet = ref false
+let header_file = ref ""
+let header_file_spec = ref false
+let footer_file = ref ""
+let footer_file_spec = ref false
+let quiet = ref true
let light = ref false
let gallina = ref false
let short = ref false
diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty
index 2c07b9fc..d31314c5 100644
--- a/tools/coqdoc/coqdoc.sty
+++ b/tools/coqdoc/coqdoc.sty
@@ -8,20 +8,20 @@
\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{coqdoc}[2002/02/11]
-% Headings
-\usepackage{fancyhdr}
-\newcommand{\coqdocleftpageheader}{\thepage\ -- \today}
-\newcommand{\coqdocrightpageheader}{\today\ -- \thepage}
-\pagestyle{fancyplain}
+% % Headings
+% \usepackage{fancyhdr}
+% \newcommand{\coqdocleftpageheader}{\thepage\ -- \today}
+% \newcommand{\coqdocrightpageheader}{\today\ -- \thepage}
+% \pagestyle{fancyplain}
-%BEGIN LATEX
-\headsep 8mm
-\renewcommand{\plainheadrulewidth}{0.4pt}
-\renewcommand{\plainfootrulewidth}{0pt}
-\lhead[\coqdocleftpageheader]{\leftmark}
-\rhead[\leftmark]{\coqdocrightpageheader}
-\cfoot{}
-%END LATEX
+% %BEGIN LATEX
+% \headsep 8mm
+% \renewcommand{\plainheadrulewidth}{0.4pt}
+% \renewcommand{\plainfootrulewidth}{0pt}
+% \lhead[\coqdocleftpageheader]{\leftmark}
+% \rhead[\leftmark]{\coqdocrightpageheader}
+% \cfoot{}
+% %END LATEX
% Hevea puts to much space with \medskip and \bigskip
%HEVEA\renewcommand{\medskip}{}
@@ -36,11 +36,27 @@
%END LATEX
% macro for typesetting keywords
-\newcommand{\coqdockw}[1]{\textsf{#1}}
+\newcommand{\coqdockw}[1]{\texttt{#1}}
-% macro for typesetting identifiers
+% macro for typesetting variable identifiers
\newcommand{\coqdocid}[1]{\textit{#1}}
+% macro for typesetting constant identifiers
+\newcommand{\coqdoccst}[1]{\textsf{#1}}
+
+% macro for typesetting module identifiers
+\newcommand{\coqdocmod}[1]{\textsc{\textsf{#1}}}
+
+% macro for typesetting module constant identifiers (e.g. Parameters in
+% module types)
+\newcommand{\coqdocax}[1]{\textsl{\textsf{#1}}}
+
+% macro for typesetting inductive type identifiers
+\newcommand{\coqdocind}[1]{\textbf{\textsf{#1}}}
+
+% macro for typesetting constructor identifiers
+\newcommand{\coqdocconstr}[1]{\textsf{#1}}
+
% newline and indentation
%BEGIN LATEX
\newcommand{\coqdoceol}{\setlength\parskip{0pt}\par}
@@ -52,6 +68,86 @@
% macro for typesetting the title of a module implementation
\newcommand{\coqdocmodule}[1]{\chapter{Module #1}\markboth{Module #1}{}
}
+\usepackage{ifpdf}
+\ifpdf
+ \usepackage[pdftex]{hyperref}
+ \hypersetup{raiselinks=true,colorlinks=true,linkcolor=black}
+ \usepackage[all]{hypcap}
+
+ \newcommand{\coqdef}[3]{\phantomsection\hypertarget{coq:#1}{#3}}
+ \newcommand{\coqref}[2]{\hyperlink{coq:#1}{#2}}
+ \newcommand{\identref}[2]{\hyperlink{coq:#1}{\textsf {#2}}}
+ \newcommand{\coqlibrary}[2]{\cleardoublepage\phantomsection
+ \hypertarget{coq:#1}{\chapter{Library \coqdoccst{#2}}}}
+\else
+ \newcommand{\coqdef}[3]{#3}
+ \newcommand{\coqref}[2]{#2}
+ \newcommand{\identref}[2]{\textsf {#2}}
+ \newcommand{\coqlibrary}[2]{\cleardoublepage\chapter{Library \coqdoccst{#2}}}
+\fi
+\usepackage{xr}
+
+%\usepackage{color}
+%\usepackage{multind}
+%\newcommand{\coqdef}[3]{\hypertarget{coq:#1}{\index{coq}{#1@#2|hyperpage}#3}}
+
+
+
+\newcommand{\coqdocvar}[1]{{\textit{#1}}}
+\newcommand{\coqdoctac}[1]{{\texttt{#1}}}
+
+
+\newcommand{\coqdefinition}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
+\newcommand{\coqdefinitionref}[2]{\coqref{#1}{\coqdoccst{#2}}}
+
+%\newcommand{\coqvariable}[2]{\coqdef{#1}{#2}{\coqdocid{#2}}}
+%\newcommand{\coqaxiom}[2]{\coqdef{#1}{#2}{\coqdocid{#2}}}
+\newcommand{\coqvariable}[2]{\coqdocid{#2}}
+
+\newcommand{\coqinductive}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}}
+\newcommand{\coqinductiveref}[2]{\coqref{#1}{\coqdocind{#2}}}
+
+\newcommand{\coqconstructor}[2]{\coqdef{#1}{#2}{\coqdocconstr{#2}}}
+\newcommand{\coqconstructorref}[2]{\coqref{#1}{\coqdocconstr{#2}}}
+
+\newcommand{\coqlemma}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
+\newcommand{\coqlemmaref}[2]{\coqref{#1}{\coqdoccst{#2}}}
+
+\newcommand{\coqclass}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}}
+\newcommand{\coqclassref}[2]{\coqref{#1}{\coqdocind{#2}}}
+
+\newcommand{\coqinstance}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
+\newcommand{\coqinstanceref}[2]{\coqref{#1}{\coqdoccst{#2}}}
+
+\newcommand{\coqmethod}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
+\newcommand{\coqmethodref}[2]{\coqref{#1}{\coqdoccst{#2}}}
+
+\newcommand{\coqabbreviation}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
+\newcommand{\coqabbreviationref}[2]{\coqref{#1}{\coqdoccst{#2}}}
+
+\newcommand{\coqrecord}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}}
+\newcommand{\coqrecordref}[2]{\coqref{#1}{\coqdocind{#2}}}
+
+\newcommand{\coqprojection}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
+\newcommand{\coqprojectionref}[2]{\coqref{#1}{\coqdoccst{#2}}}
+
+\newcommand{\coqnotationref}[2]{\coqref{#1}{\coqdockw{#2}}}
+
+\newcommand{\coqsection}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
+\newcommand{\coqsectionref}[2]{\coqref{#1}{\coqdoccst{#2}}}
+
+%\newcommand{\coqlibrary}[2]{\chapter{Library \coqdoccst{#2}}\label{coq:#1}}
+
+%\newcommand{\coqlibraryref}[2]{\ref{coq:#1}}
+
+\newcommand{\coqlibraryref}[2]{\coqref{#1}{\coqdoccst{#2}}}
+
+\newcommand{\coqaxiom}[2]{\coqdef{#1}{#2}{\coqdocax{#2}}}
+\newcommand{\coqaxiomref}[2]{\coqref{#1}{\coqdocax{#2}}}
+
+\newcommand{\coqmodule}[2]{\coqdef{#1}{#2}{\coqdocmod{#2}}}
+\newcommand{\coqmoduleref}[2]{\coqref{#1}{\coqdocmod{#2}}}
+
%HEVEA\newcommand{\lnot}{\coqwkw{not}}
%HEVEA\newcommand{\lor}{\coqwkw{or}}
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index 4b53d6ff..1da8ebd7 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: index.mli 8617 2006-03-08 10:47:12Z notin $ i*)
+(*i $Id: index.mli 11065 2008-06-06 22:39:43Z msozeau $ i*)
open Cdglobals
@@ -19,13 +19,23 @@ type entry_type =
| Inductive
| Constructor
| Lemma
+ | Record
+ | Projection
+ | Instance
+ | Class
+ | Method
| Variable
| Axiom
| TacticDefinition
+ | Abbreviation
+ | Notation
+ | Section
+
+val type_name : entry_type -> string
type index_entry =
| Def of string * entry_type
- | Ref of coq_module * string
+ | Ref of coq_module * string * entry_type
| Mod of coq_module * string
val find : coq_module -> loc -> index_entry
@@ -42,7 +52,7 @@ val scan_file : string -> coq_module -> unit
(*s Read globalizations from a file (produced by coqc -dump-glob) *)
-val read_glob : string -> unit
+val read_glob : string -> coq_module
(*s Indexes *)
@@ -51,6 +61,8 @@ type 'a index = {
idx_entries : (char * (string * 'a) list) list;
idx_size : int }
+val current_library : string ref
+
val all_entries : unit ->
(coq_module * entry_type) index *
(entry_type * coq_module index) list
diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
index 5b281b8b..fc2090dc 100644
--- a/tools/coqdoc/index.mll
+++ b/tools/coqdoc/index.mll
@@ -1,3 +1,4 @@
+(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -6,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: index.mll 9204 2006-10-04 13:05:58Z notin $ i*)
+(*i $Id: index.mll 11065 2008-06-06 22:39:43Z msozeau $ i*)
{
@@ -25,31 +26,49 @@ type entry_type =
| Inductive
| Constructor
| Lemma
+ | Record
+ | Projection
+ | Instance
+ | Class
+ | Method
| Variable
| Axiom
| TacticDefinition
+ | Abbreviation
+ | Notation
+ | Section
type index_entry =
| Def of string * entry_type
- | Ref of coq_module * string
+ | Ref of coq_module * string * entry_type
| Mod of coq_module * string
let current_type = ref Library
let current_library = ref ""
- (** referes to the file being parsed *)
+ (** refers to the file being parsed *)
let table = Hashtbl.create 97
(** [table] is used to store references and definitions *)
-let add_def loc ty id = Hashtbl.add table (!current_library, loc) (Def (id, ty))
-
-let add_ref m loc m' id = Hashtbl.add table (m, loc) (Ref (m', id))
+let full_ident sp id =
+ if sp <> "<>" then
+ if id <> "<>" then
+ sp ^ "." ^ id
+ else sp
+ else if id <> "<>"
+ then id
+ else ""
+
+let add_def loc ty sp id =
+ Hashtbl.add table (!current_library, loc) (Def (full_ident sp id, ty))
+let add_ref m loc m' sp id ty =
+ Hashtbl.add table (m, loc) (Ref (m', full_ident sp id, ty))
+
let add_mod m loc m' id = Hashtbl.add table (m, loc) (Mod (m', id))
let find m l = Hashtbl.find table (m, l)
-
(*s Manipulating path prefixes *)
type stack = string list
@@ -99,14 +118,15 @@ let make_fullid id =
else
id
+
(* Coq modules *)
let split_sp s =
try
let i = String.rindex s '.' in
- String.sub s 0 i, String.sub s (i + 1) (String.length s - i - 1)
- with Not_found ->
- "", s
+ String.sub s 0 i, String.sub s (i + 1) (String.length s - i - 1)
+ with
+ Not_found -> "", s
let modules = Hashtbl.create 97
let local_modules = Hashtbl.create 97
@@ -118,8 +138,7 @@ let add_module m =
type module_kind = Local | Coqlib | Unknown
-let coq_module m =
- String.length m >= 4 && String.sub m 0 4 = "Coq."
+let coq_module m = String.length m >= 4 && String.sub m 0 4 = "Coq."
let find_module m =
if Hashtbl.mem local_modules m then
@@ -129,14 +148,6 @@ let find_module m =
else
Unknown
-let ref_module loc s =
- try
- let n = String.length s in
- let i = String.rindex s ' ' in
- let id = String.sub s (i+1) (n-i-1) in
- add_mod !current_library (loc+i+1) (Hashtbl.find modules id) id
- with Not_found ->
- ()
(* Building indexes *)
@@ -181,10 +192,18 @@ let type_name = function
| Inductive -> "inductive"
| Constructor -> "constructor"
| Lemma -> "lemma"
+ | Record -> "record"
+ | Projection -> "projection"
+ | Instance -> "instance"
+ | Class -> "class"
+ | Method -> "method"
| Variable -> "variable"
| Axiom -> "axiom"
| TacticDefinition -> "tactic"
-
+ | Abbreviation -> "abbreviation"
+ | Notation -> "notation"
+ | Section -> "section"
+
let all_entries () =
let gl = ref [] in
let add_g s m t = gl := (s,(m,t)) :: !gl in
@@ -209,6 +228,8 @@ let all_entries () =
}
(*s Shortcuts for regular expressions. *)
+let digit = ['0'-'9']
+let num = digit+
let space =
[' ' '\010' '\013' '\009' '\012']
@@ -225,16 +246,18 @@ let end_hide = "(*" space* "end" space+ "hide" space* "*)"
(*s Indexing entry point. *)
rule traverse = parse
- | "Definition" space
+ | ("Program" space+)? "Definition" space
{ current_type := Definition; index_ident lexbuf; traverse lexbuf }
| "Tactic" space+ "Definition" space
{ current_type := TacticDefinition; index_ident lexbuf; traverse lexbuf }
| ("Axiom" | "Parameter") space
{ current_type := Axiom; index_ident lexbuf; traverse lexbuf }
- | "Fixpoint" space
+ | ("Program" space+)? "Fixpoint" space
{ current_type := Definition; index_ident lexbuf; fixpoint lexbuf;
traverse lexbuf }
- | ("Lemma" | "Theorem") space
+ | ("Program" space+)? ("Lemma" | "Theorem") space
+ { current_type := Lemma; index_ident lexbuf; traverse lexbuf }
+ | "Obligation" space num ("of" ident)?
{ current_type := Lemma; index_ident lexbuf; traverse lexbuf }
| "Inductive" space
{ current_type := Inductive;
@@ -247,8 +270,8 @@ rule traverse = parse
| "Variable" 's'? space
{ current_type := Variable; index_idents lexbuf; traverse lexbuf }
***i*)
- | "Require" (space+ ("Export"|"Import"))? space+ ident
- { ref_module (lexeme_start lexbuf) (lexeme lexbuf); traverse lexbuf }
+ | "Require" (space+ ("Export"|"Import"))?
+ { module_refs lexbuf; traverse lexbuf }
| "End" space+
{ end_ident lexbuf; traverse lexbuf }
| begin_hide
@@ -277,7 +300,7 @@ and index_ident = parse
| Lemma -> make_fullid id
| _ -> id
in
- add_def (lexeme_start lexbuf) !current_type fullid }
+ add_def (lexeme_start lexbuf) !current_type "" fullid }
| eof
{ () }
| _
@@ -289,7 +312,7 @@ and index_idents = parse
| space+ | ','
{ index_idents lexbuf }
| ident
- { add_def (lexeme_start lexbuf) !current_type (lexeme lexbuf);
+ { add_def (lexeme_start lexbuf) !current_type "" (lexeme lexbuf);
index_idents lexbuf }
| eof
{ () }
@@ -369,14 +392,52 @@ and module_ident = parse
{ () }
| ident
{ let id = lexeme lexbuf in
- begin_module id; add_def (lexeme_start lexbuf) !current_type id }
+ begin_module id; add_def (lexeme_start lexbuf) !current_type "" id }
| eof
{ () }
| _
{ () }
+(*s parse module names *)
+
+and module_refs = parse
+ | space+
+ { module_refs lexbuf }
+ | ident
+ { let id = lexeme lexbuf in
+ (try
+ add_mod !current_library (lexeme_start lexbuf) (Hashtbl.find modules id) id
+ with
+ Not_found -> ()
+ );
+ module_refs lexbuf }
+ | eof
+ { () }
+ | _
+ { () }
+
{
-
+ let type_of_string = function
+ | "def" | "coe" | "subclass" | "canonstruc"
+ | "ex" | "scheme" -> Definition
+ | "prf" | "thm" -> Lemma
+ | "ind" | "coind" -> Inductive
+ | "constr" -> Constructor
+ | "rec" | "corec" -> Record
+ | "proj" -> Projection
+ | "class" -> Class
+ | "meth" -> Method
+ | "inst" -> Instance
+ | "var" -> Variable
+ | "defax" | "prfax" | "ax" -> Axiom
+ | "syndef" -> Abbreviation
+ | "not" -> Notation
+ | "lib" -> Library
+ | "mod" | "modtype" -> Module
+ | "tac" -> TacticDefinition
+ | "sec" -> Section
+ | s -> raise (Invalid_argument ("type_of_string:" ^ s))
+
let read_glob f =
let c = open_in f in
let cur_mod = ref "" in
@@ -387,22 +448,22 @@ and module_ident = parse
if n > 0 then begin
match s.[0] with
| 'F' ->
- cur_mod := String.sub s 1 (n - 1)
+ cur_mod := String.sub s 1 (n - 1);
+ current_library := !cur_mod
| 'R' ->
(try
- let i = String.index s ' ' in
- let j = String.index_from s (i+1) ' ' in
- let loc = int_of_string (String.sub s 1 (i - 1)) in
- let lib_dp = String.sub s (i + 1) (j - i - 1) in
- let full_id = String.sub s (j + 1) (n - j - 1) in
- add_ref !cur_mod loc lib_dp full_id
- with Not_found ->
- ())
- | _ -> ()
+ Scanf.sscanf s "R%d %s %s %s %s"
+ (fun loc lib_dp sp id ty ->
+ add_ref !cur_mod loc lib_dp sp id (type_of_string ty))
+ with _ -> ())
+ | _ ->
+ try Scanf.sscanf s "%s %d %s %s"
+ (fun ty loc sp id -> add_def loc (type_of_string ty) sp id)
+ with Scanf.Scan_failure _ -> ()
end
- done
+ done; assert false
with End_of_file ->
- close_in c
+ close_in c; !cur_mod
let scan_file f m =
init_stack (); current_library := m;
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 18a44a44..7111187f 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -1,3 +1,4 @@
+(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -6,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: main.ml 8777 2006-05-02 10:14:39Z notin $ i*)
+(*i $Id: main.ml 11024 2008-05-30 12:41:39Z msozeau $ i*)
(* Modified by Lionel Elie Mamane <lionel@mamane.lu> on 9 & 10 Mar 2004:
* - handling of absolute filenames (function coq_module)
@@ -19,50 +20,53 @@
*)
open Cdglobals
-open Filename
open Printf
-open Output
-open Pretty
(*s \textbf{Usage.} Printed on error output. *)
let usage () =
prerr_endline "";
prerr_endline "Usage: coqdoc <options and files>";
- prerr_endline " --html produce a HTML document (default)";
- prerr_endline " --latex produce a LaTeX document";
- prerr_endline " --texmacs produce a TeXmacs document";
- prerr_endline " --dvi output the DVI";
- prerr_endline " --ps output the PostScript";
- prerr_endline " --stdout write output to stdout";
- prerr_endline " -o <file> write output in file <file>";
- prerr_endline " -d <dir> output files into directory <dir>";
- prerr_endline " -g (gallina) skip proofs";
- prerr_endline " -s (short) no titles for files";
- prerr_endline " -l light mode (only defs and statements)";
- prerr_endline " -t <string> give a title to the document";
- prerr_endline " --body-only suppress LaTeX/HTML header and trailer";
- prerr_endline " --no-index do not output the index";
- prerr_endline " --multi-index index split in multiple files";
- prerr_endline " --toc output a table of contents";
- prerr_endline " --vernac <file> consider <file> as a .v file";
- 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 " --quiet quiet mode";
- prerr_endline " --glob-from <file> read Coq globalizations from file <file>";
- prerr_endline " --no-externals no links to Coq standard library";
- prerr_endline " --coqlib <url> set URL for Coq standard library";
- prerr_endline " (default is http://coq.inria.fr/library/)";
- prerr_endline " --coqlib_path <dir> set the path where Coq files are installed";
- prerr_endline " -R <dir> <coqdir> map physical dir to Coq dir";
- prerr_endline " --latin1 set ISO-8859-1 input language";
- prerr_endline " --utf8 set UTF-8 input language";
- prerr_endline " --charset <string> set HTML charset";
- prerr_endline " --inputenc <string> set LaTeX input encoding";
+ prerr_endline " --html produce a HTML document (default)";
+ prerr_endline " --latex produce a LaTeX document";
+ prerr_endline " --texmacs produce a TeXmacs document";
+ prerr_endline " --dvi output the DVI";
+ prerr_endline " --ps output the PostScript";
+ prerr_endline " --pdf output the Pdf";
+ prerr_endline " --stdout write output to stdout";
+ prerr_endline " -o <file> write output in file <file>";
+ prerr_endline " -d <dir> output files into directory <dir>";
+ prerr_endline " -g (gallina) skip proofs";
+ prerr_endline " -s (short) no titles for files";
+ prerr_endline " -l light mode (only defs and statements)";
+ prerr_endline " -t <string> give a title to the document";
+ prerr_endline " --body-only suppress LaTeX/HTML header and trailer";
+ prerr_endline " --with-header <file> prepend <file> as html reader";
+ prerr_endline " --with-footer <file> append <file> as html footer";
+ prerr_endline " --no-index do not output the index";
+ prerr_endline " --multi-index index split in multiple files";
+ prerr_endline " --toc output a table of contents";
+ prerr_endline " --vernac <file> consider <file> as a .v file";
+ 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 " --quiet quiet mode (default)";
+ prerr_endline " --verbose verbose mode";
+ prerr_endline " --no-externals no links to Coq standard library";
+ prerr_endline " --coqlib <url> set URL for Coq standard library";
+ prerr_endline " (default is http://coq.inria.fr/library/)";
+ prerr_endline " --coqlib_path <dir> set the path where Coq files are installed";
+ prerr_endline " -R <dir> <coqdir> map physical dir to Coq dir";
+ prerr_endline " --latin1 set ISO-8859-1 input language";
+ prerr_endline " --utf8 set UTF-8 input language";
+ prerr_endline " --charset <string> set HTML charset";
+ prerr_endline " --inputenc <string> set LaTeX input encoding";
prerr_endline "";
exit 1
+let obsolete s =
+ eprintf "Warning: option %s is now obsolete; please update your scripts\n" s
+
(*s \textbf{Banner.} Always printed. Notice that it is printed on error
output, so that when the output of [coqdoc] is redirected this header
is not (unless both standard and error outputs are redirected, of
@@ -74,7 +78,7 @@ let banner () =
flush stderr
let target_full_name f =
- match !target_language with
+ match !Cdglobals.target_language with
| HTML -> f ^ ".html"
| _ -> f ^ ".tex"
@@ -88,95 +92,70 @@ let check_if_file_exists f =
eprintf "\ncoqdoc: %s: no such file\n" f;
exit 1
end
-
+
+
+(*s Manipulations of paths and path aliases *)
+
+let normalize_path p =
+ (* We use the Unix subsystem to normalize a physical path (relative
+ or absolute) and get rid of symbolic links, relative links (like
+ ./ or ../ in the middle of the path; it's tricky but it
+ works... *)
+ (* Rq: Sys.getcwd () returns paths without '/' at the end *)
+ let orig = Sys.getcwd () in
+ Sys.chdir p;
+ let res = Sys.getcwd () in
+ Sys.chdir orig;
+ res
+
+let normalize_filename f =
+ let basename = Filename.basename f in
+ let dirname = Filename.dirname f in
+ Filename.concat (normalize_path dirname) basename
+
+(* [paths] maps a physical path to a name *)
let paths = ref []
-let add_path m l = paths := (m,l) :: !paths
+let add_path dir name =
+ (* if dir is relative we add both the relative and absolute name *)
+ let p = normalize_path dir in
+ paths := (p,name) :: !paths
-let exists_dir dir =
- try let _ = Unix.opendir dir in true with Unix.Unix_error _ -> false
-
-let add_rec_path f l =
- let rec traverse abs rel =
- add_path abs rel;
- let dirh = Unix.opendir abs in
- try
- while true do
- let f = Unix.readdir dirh in
- if f <> "" && f.[0] <> '.' && f <> "CVS" then
- let abs' = Filename.concat abs f in
- try
- if exists_dir abs' then traverse abs' (rel ^ "." ^ f)
- with Unix.Unix_error _ ->
- ()
- done
- with End_of_file ->
- Unix.closedir dirh
- in
- if exists_dir f then traverse f l
-
(* turn A/B/C into A.B.C *)
-let make_path = Str.global_replace (Str.regexp "/") ".";;
+let name_of_path = Str.global_replace (Str.regexp "/") ".";;
-let coq_module file =
- (* TODO
- * LEM:
- * We should also remove things like "/./" in the middle of the filename,
- * rewrite "/foo/../bar" to "/bar", recognise different paths that lead
- * to the same file / directory (via symlinks), etc. The best way to do
- * all this would be to use the libc function realpath() on _both_ p and
- * file / f before comparing them.
- *
- * The semantics of realpath() on file symlinks might not be what we
- * want... (But it is what we want on directory symlinks.) So, we would
- * have to cook up our own version of realpath()?
- *
- * Do all target platforms have realpath()?
- *)
- let f = chop_extension file in
- (* remove leading ./ and any number of slashes after *)
- let f = Str.replace_first (Str.regexp "^\\./+") "" f in
- if (Str.string_before f 1) = "/" then
- (* f is an absolute path. Prefixes must be matched with the beginning of f,
- * not prepended
- *)
- let rec trypath = function
- | [] -> make_path f
- | (p, lg) :: r ->
- (* make sure p ends with a single '/'
- * This guarantees that we don't match a file whose name is
- * of the form p ^ "foo". It means we may miss p itself,
- * but this does not matter: coqdoc doesn't do anything
- * of a directory anyway. *)
- let p = (Str.replace_first (Str.regexp "/*$") "/" p) in
- let p_quoted = (Str.quote p) in
- if (Str.string_match (Str.regexp p_quoted) f 0) then
- make_path (Filename.concat lg (Str.replace_first (Str.regexp (p_quoted ^ "/*")) "" f))
- else
- trypath r
- in trypath !paths
- else (* f is a relative path *)
- let rec trypath = function
- | [] ->
- make_path f
- | (p,lg) :: r ->
- let p_file = Filename.concat p file in
- if Sys.file_exists p_file then
- make_path (Filename.concat lg f)
- else
- trypath r
- in trypath !paths;;
+let coq_module filename =
+ let bfname = Filename.chop_extension filename in
+ let nfname = normalize_filename bfname in
+ let rec change_prefix map f =
+ match map with
+ | [] ->
+ (* There is no prefix alias;
+ we just cut the name wrt current working directory *)
+ let cwd = Sys.getcwd () in
+ let exp = Str.regexp (Str.quote (cwd ^ "/")) in
+ if (Str.string_match exp f 0) then
+ name_of_path (Str.replace_first exp "" f)
+ else
+ name_of_path f
+ | (p, name) :: rem ->
+ let expp = Str.regexp (Str.quote p) in
+ if (Str.string_match expp f 0) then
+ let newp = Str.replace_first expp name f in
+ name_of_path newp
+ else
+ change_prefix rem f
+ in
+ change_prefix !paths nfname
let what_file f =
check_if_file_exists f;
- if check_suffix f ".v" || check_suffix f ".g" then
+ if Filename.check_suffix f ".v" || Filename.check_suffix f ".g" then
Vernac_file (f, coq_module f)
- else if check_suffix f ".tex" then
+ else if Filename.check_suffix f ".tex" then
Latex_file f
- else begin
- eprintf "\ncoqdoc: don't know what to do with %s\n" f;
- exit 1
- end
+ else
+ (eprintf "\ncoqdoc: don't know what to do with %s\n" f; exit 1)
(*s \textbf{Reading file names from a file.}
* File names may be given
@@ -214,9 +193,9 @@ let files_from_file f =
(*s \textbf{Parsing of the command line.} *)
-let output_file = ref ""
let dvi = ref false
let ps = ref false
+let pdf = ref false
let parse () =
let files = ref [] in
@@ -227,8 +206,16 @@ let parse () =
| ("-nopreamble" | "--nopreamble" | "--no-preamble"
| "-bodyonly" | "--bodyonly" | "--body-only") :: rem ->
header_trailer := false; parse_rec rem
+ | ("-with-header" | "--with-header") :: f ::rem ->
+ header_trailer := true; header_file_spec := true; header_file := f; parse_rec rem
+ | ("-with-header" | "--with-header") :: [] ->
+ usage ()
+ | ("-with-footer" | "--with-footer") :: f ::rem ->
+ header_trailer := true; footer_file_spec := true; footer_file := f; parse_rec rem
+ | ("-with-footer" | "--with-footer") :: [] ->
+ usage ()
| ("-p" | "--preamble") :: s :: rem ->
- push_in_preamble s; parse_rec rem
+ Output.push_in_preamble s; parse_rec rem
| ("-p" | "--preamble") :: [] ->
usage ()
| ("-noindex" | "--noindex" | "--no-index") :: rem ->
@@ -259,6 +246,8 @@ let parse () =
usage ()
| ("-latex" | "--latex") :: rem ->
Cdglobals.target_language := LaTeX; parse_rec rem
+ | ("-pdf" | "--pdf") :: rem ->
+ Cdglobals.target_language := LaTeX; pdf := true; parse_rec rem
| ("-dvi" | "--dvi") :: rem ->
Cdglobals.target_language := LaTeX; dvi := true; parse_rec rem
| ("-ps" | "--ps") :: rem ->
@@ -284,10 +273,12 @@ let parse () =
| ("-q" | "-quiet" | "--quiet") :: rem ->
quiet := true; parse_rec rem
+ | ("-v" | "-verbose" | "--verbose") :: rem ->
+ quiet := false; parse_rec rem
| ("-h" | "-help" | "-?" | "--help") :: rem ->
banner (); usage ()
- | ("-v" | "-version" | "--version") :: _ ->
+ | ("-V" | "-version" | "--version") :: _ ->
banner (); exit 0
| ("-vernac-file" | "--vernac-file") :: f :: rem ->
@@ -309,7 +300,7 @@ let parse () =
| "-R" :: ([] | [_]) ->
usage ()
| ("-glob-from" | "--glob-from") :: f :: rem ->
- Index.read_glob f; parse_rec rem
+ obsolete "glob-from"; parse_rec rem
| ("-glob-from" | "--glob-from") :: [] ->
usage ()
| ("--no-externals" | "-no-externals" | "-noexternals") :: rem ->
@@ -332,7 +323,7 @@ let parse () =
(*s The following function produces the output. The default output is
the \LaTeX\ document: in that case, we just call [Web.produce_document].
If option \verb!-dvi!, \verb!-ps! or \verb!-html! is invoked, then
- we make calls to \verb!latex! or \verb!dvips! accordingly. *)
+ we make calls to \verb!latex! or \verb!dvips! or \verb!pdflatex! accordingly. *)
let locally dir f x =
let cwd = Sys.getcwd () in
@@ -346,8 +337,10 @@ let clean_temp_files basefile =
remove (basefile ^ ".tex");
remove (basefile ^ ".log");
remove (basefile ^ ".aux");
+ remove (basefile ^ ".toc");
remove (basefile ^ ".dvi");
remove (basefile ^ ".ps");
+ remove (basefile ^ ".pdf");
remove (basefile ^ ".haux");
remove (basefile ^ ".html")
@@ -370,70 +363,81 @@ let copy src dst =
(*s Functions for generating output files *)
-
+
let gen_one_file l =
let file = function
| Vernac_file (f,m) ->
- set_module m; coq_file f m
+ Output.set_module m; Pretty.coq_file f m
| Latex_file _ -> ()
in
- if (!header_trailer) then header ();
- if !toc then make_toc ();
+ if (!header_trailer) then Output.header ();
+ if !toc then Output.make_toc ();
List.iter file l;
- if !index then make_index();
- if (!header_trailer) then trailer ()
+ if !index then Output.make_index();
+ if (!header_trailer) then Output.trailer ()
let gen_mult_files l =
let file = function
| Vernac_file (f,m) ->
- set_module m;
+ Output.set_module m;
let hf = target_full_name m in
open_out_file hf;
- if (!header_trailer) then header ();
- if !toc then make_toc ();
- coq_file f m;
- if (!header_trailer) then trailer ();
+ if (!header_trailer) then Output.header ();
+ Pretty.coq_file f m;
+ if (!header_trailer) then Output.trailer ();
close_out_file()
| Latex_file _ -> ()
in
List.iter file l;
if (!index && !target_language=HTML) then begin
- if (!multi_index) then make_multi_index ();
+ if (!multi_index) then Output.make_multi_index ();
open_out_file "index.html";
page_title := (if !title <> "" then !title else "Index");
- if (!header_trailer) then header ();
- make_index ();
- if (!header_trailer) then trailer ();
+ if (!header_trailer) then Output.header ();
+ Output.make_index ();
+ if (!header_trailer) then Output.trailer ();
close_out_file()
end;
if (!toc && !target_language=HTML) then begin
open_out_file "toc.html";
page_title := (if !title <> "" then !title else "Table of contents");
- if (!header_trailer) then header ();
+ if (!header_trailer) then Output.header ();
if !title <> "" then printf "<h1>%s</h1>\n" !title;
- make_toc ();
- if (!header_trailer) then trailer ();
+ Output.make_toc ();
+ if (!header_trailer) then Output.trailer ();
close_out_file()
end
(* Rq: pour latex et texmacs, une toc ou un index séparé n'a pas de sens... *)
+let read_glob x =
+ match x with
+ | Vernac_file (f,m) ->
+ let glob = (Filename.chop_extension f) ^ ".glob" in
+ (try
+ Vernac_file (f, Index.read_glob glob)
+ with _ ->
+ eprintf "Warning: file %s cannot be opened; links will not be available\n" glob;
+ x)
+ | Latex_file _ -> x
let index_module = function
- | Vernac_file (_,m) -> Index.add_module m
+ | Vernac_file (f,m) ->
+ Index.add_module m
| Latex_file _ -> ()
let produce_document l =
- List.iter index_module l;
(if !target_language=HTML then
let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.css") in
let dst = if !output_dir <> "" then Filename.concat !output_dir "coqdoc.css" else "coqdoc.css" in
copy src dst);
(if !target_language=LaTeX then
- let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.sty") in
- let dst = if !output_dir <> "" then
- Filename.concat !output_dir "coqdoc.sty"
- else "coqdoc.sty" in
- copy src dst);
+ let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.sty") in
+ let dst = if !output_dir <> "" then
+ Filename.concat !output_dir "coqdoc.sty"
+ else "coqdoc.sty" in
+ copy src dst);
+ let l = List.map read_glob l in
+ List.iter index_module l;
match !out_to with
| StdOut ->
Cdglobals.out_channel := stdout;
@@ -446,51 +450,64 @@ let produce_document l =
gen_mult_files l
let produce_output fl =
- if not (!dvi || !ps) then begin
+ if not (!dvi || !ps || !pdf) then
produce_document fl
- end else begin
- let texfile = temp_file "coqdoc" ".tex" in
- let basefile = chop_suffix texfile ".tex" in
- open_out_file texfile;
- produce_document fl;
- let command =
- let file = basename texfile in
- let file =
- if !quiet then sprintf "'\\nonstopmode\\input{%s}'" file else file
+ else
+ begin
+ let texfile = Filename.temp_file "coqdoc" ".tex" in
+ let basefile = Filename.chop_suffix texfile ".tex" in
+ let final_out_to = !out_to in
+ out_to := File texfile;
+ output_dir := (Filename.dirname texfile);
+ produce_document fl;
+
+ let latexexe = if !pdf then "pdflatex" else "latex" in
+ let latexcmd =
+ let file = Filename.basename texfile in
+ let file =
+ if !quiet then sprintf "'\\nonstopmode\\input{%s}'" file else file
+ in
+ sprintf "%s %s && %s %s 1>&2 %s" latexexe file latexexe file (if !quiet then "> /dev/null" else "")
in
- sprintf "(latex %s && latex %s) 1>&2 %s" file file
- (if !quiet then "> /dev/null" else "")
- in
- let res = locally (dirname texfile) Sys.command command in
- if res <> 0 then begin
- eprintf "Couldn't run LaTeX successfully\n";
- clean_and_exit basefile res
- end;
- let dvifile = basefile ^ ".dvi" in
- if !dvi then begin
- if !output_file <> "" then
- (* we cannot use Sys.rename accross file systems *)
- copy dvifile !output_file
- else
- cat dvifile
- end;
- if !ps then begin
- let psfile =
- if !output_file <> "" then !output_file else basefile ^ ".ps"
- in
- let command =
- sprintf "dvips %s -o %s %s" dvifile psfile
- (if !quiet then "> /dev/null 2>&1" else "")
- in
- let res = Sys.command command in
- if res <> 0 then begin
- eprintf "Couldn't run dvips successfully\n";
- clean_and_exit basefile res
+ let res = locally (Filename.dirname texfile) Sys.command latexcmd in
+ if res <> 0 then begin
+ eprintf "Couldn't run LaTeX successfully\n";
+ clean_and_exit basefile res
+ end;
+
+ let dvifile = basefile ^ ".dvi" in
+ if !dvi then
+ begin
+ match final_out_to with
+ | MultFiles | StdOut -> cat dvifile
+ | File f -> copy dvifile f
end;
- if !output_file = "" then cat psfile
- end;
- clean_temp_files basefile
- end
+ let pdffile = basefile ^ ".pdf" in
+ if !pdf then
+ begin
+ match final_out_to with
+ | MultFiles | StdOut -> cat pdffile
+ | File f -> copy pdffile f
+ end;
+ if !ps then begin
+ let psfile = basefile ^ ".ps"
+ in
+ let command =
+ sprintf "dvips %s -o %s %s" dvifile psfile
+ (if !quiet then "> /dev/null 2>&1" else "")
+ in
+ let res = Sys.command command in
+ if res <> 0 then begin
+ eprintf "Couldn't run dvips successfully\n";
+ clean_and_exit basefile res
+ end;
+ match final_out_to with
+ | MultFiles | StdOut -> cat psfile
+ | File f -> copy psfile f
+ end;
+
+ clean_temp_files basefile
+ end
(*s \textbf{Main program.} Print the banner, parse the command line,
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 2d0bc6c2..93414f22 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -1,3 +1,4 @@
+(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -6,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: output.ml 10248 2007-10-23 13:02:56Z notin $ i*)
+(*i $Id: output.ml 11154 2008-06-19 18:42:19Z msozeau $ i*)
open Cdglobals
open Index
@@ -31,28 +32,44 @@ let build_table l =
let is_keyword =
build_table
- [ "AddPath"; "Axiom"; "Chapter"; "CoFixpoint";
- "CoInductive"; "Defined"; "Definition";
- "End"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint";
+ [ "AddPath"; "Axiom"; "Chapter"; "Check"; "CoFixpoint";
+ "CoInductive"; "Defined"; "Definition"; "End"; "Eval"; "Example";
+ "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint";
"Hypothesis"; "Hypotheses";
- "Immediate"; "Implicit"; "Import"; "Inductive";
+ "Resolve"; "Unfold"; "Immediate"; "Extern"; "Implicit"; "Import"; "Inductive";
"Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac";
- "Module"; "Module Type"; "Declare Module";
+ "Module"; "Module Type"; "Declare Module"; "Include";
"Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Qed";
"Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme";
- "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem";
- "Set"; "Unset"; "Variable"; "Variables";
+ "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem";
+ "Set"; "Unset"; "Variable"; "Variables"; "Context";
"Notation"; "Reserved Notation"; "Tactic Notation";
- "Delimit"; "Bind"; "Open"; "Scope";
- "Boxed"; "Unboxed";
- "Arguments";
+ "Delimit"; "Bind"; "Open"; "Scope";
+ "Boxed"; "Unboxed"; "Inline";
+ "Arguments"; "Add"; "Strict";
+ "Typeclasses"; "Instance"; "Class"; "Instantiation";
(* Program *)
- "Program Definition"; "Program Fixpoint"; "Program Lemma";
+ "Program Definition"; "Program Example"; "Program Fixpoint"; "Program Lemma";
"Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next";
+ "Program Instance";
(*i (* coq terms *) *)
- "match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun"; "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="
+ "match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun";
+ "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"
]
+let is_tactic =
+ build_table
+ [ "intro"; "intros"; "apply"; "rewrite"; "setoid_rewrite";
+ "destruct"; "induction"; "elim"; "dependent";
+ "generalize"; "clear"; "rename"; "move"; "set"; "assert";
+ "cut"; "assumption"; "exact"; "split"; "try"; "discriminate";
+ "simpl"; "unfold"; "red"; "compute"; "at"; "in"; "by";
+ "reflexivity"; "symmetry"; "transitivity";
+ "replace"; "setoid_replace"; "inversion"; "inversion_clear";
+ "pattern"; "intuition"; "congruence";
+ "trivial"; "exact"; "tauto"; "firstorder"; "ring";
+ "clapply"; "program_simpl"; "eapply"; "auto"; "eauto" ]
+
(*s Current Coq module *)
let current_module = ref ""
@@ -78,6 +95,7 @@ let remove_printing_token = Hashtbl.remove token_pp
let _ = List.iter
(fun (s,l) -> Hashtbl.add token_pp s (Some l, None))
[ "*" , "\\ensuremath{\\times}";
+ "|", "\\ensuremath{|}";
"->", "\\ensuremath{\\rightarrow}";
"->~", "\\ensuremath{\\rightarrow\\lnot}";
"->~~", "\\ensuremath{\\rightarrow\\lnot\\lnot}";
@@ -153,6 +171,12 @@ module Latex = struct
| _ ->
output_char c
+ let label_char c = match c with
+ | '\\' | '$' | '#' | '%' | '&' | '{' | '}' | '_'
+ | '^' | '~' -> ()
+ | _ ->
+ output_char c
+
let latex_char = output_char
let latex_string = output_string
@@ -162,9 +186,14 @@ module Latex = struct
let raw_ident s =
for i = 0 to String.length s - 1 do char s.[i] done
+ let label_ident s =
+ for i = 0 to String.length s - 1 do label_char s.[i] done
+
let start_module () =
if not !short then begin
- printf "\\coqdocmodule{";
+ printf "\\coqlibrary{";
+ label_ident !current_module;
+ printf "}{";
raw_ident !current_module;
printf "}\n\n"
end
@@ -192,11 +221,53 @@ module Latex = struct
with Not_found ->
f tok
- let ident s _ =
+ let module_ref m s =
+ printf "\\moduleid{%s}{" m; raw_ident s; printf "}"
+ (*i
+ match find_module m with
+ | Local ->
+ printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>"
+ | Coqlib when !externals ->
+ let m = Filename.concat !coqlib m in
+ printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>"
+ | Coqlib | Unknown ->
+ raw_ident s
+ i*)
+
+ let ident_ref m fid typ s =
+ let id = if fid <> "" then (m ^ "." ^ fid) else m in
+ match find_module m with
+ | Local ->
+ printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}"
+ | Coqlib when !externals ->
+ let _m = Filename.concat !coqlib m in
+ printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}"
+ | Coqlib | Unknown ->
+ raw_ident s
+
+ let defref m id ty s =
+ printf "\\coq%s{" (type_name ty); label_ident (m ^ "." ^ id); printf "}{"; raw_ident s; printf "}"
+
+ let ident s loc =
if is_keyword s then begin
printf "\\coqdockw{"; raw_ident s; printf "}"
end else begin
- printf "\\coqdocid{"; raw_ident s; printf "}"
+ begin
+ try
+ (match Index.find !current_module loc with
+ | Def (fullid,typ) ->
+ defref !current_module fullid typ s
+ | Mod (m,s') when s = s' ->
+ module_ref m s
+ | Ref (m,fullid,typ) ->
+ ident_ref m fullid typ s
+ | Mod _ ->
+ printf "\\coqdocid{"; raw_ident s; printf "}")
+ with Not_found ->
+ if is_tactic s then begin
+ printf "\\coqdoctac{"; raw_ident s; printf "}"
+ end else begin printf "\\coqdocvar{"; raw_ident s; printf "}" end
+ end
end
let ident s l = with_latex_printing (fun s -> ident s l) s
@@ -271,31 +342,51 @@ end
module Html = struct
let header () =
- if !header_trailer then begin
- printf "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"\n";
- printf "\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">\n";
- printf "<html xmlns=\"http://www.w3.org/1999/xhtml\">\n<head>\n";
- printf "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=%s\"/>\n" !charset;
- printf "<link href=\"coqdoc.css\" rel=\"stylesheet\" type=\"text/css\"/>\n";
- printf "<title>%s</title>\n</head>\n\n" !page_title;
- printf "<body>\n\n<div id=\"page\">\n\n<div id=\"header\">\n</div>\n\n";
- printf "<div id=\"main\">\n\n"
- end
+ if !header_trailer then
+ if !header_file_spec then
+ let cin = Pervasives.open_in !header_file in
+ try
+ while true do
+ let s = Pervasives.input_line cin in
+ printf "%s\n" s
+ done
+ with End_of_file -> Pervasives.close_in cin
+ else
+ begin
+ printf "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"\n";
+ printf "\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">\n";
+ printf "<html xmlns=\"http://www.w3.org/1999/xhtml\">\n<head>\n";
+ printf "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=%s\"/>\n" !charset;
+ printf "<link href=\"coqdoc.css\" rel=\"stylesheet\" type=\"text/css\"/>\n";
+ printf "<title>%s</title>\n</head>\n\n" !page_title;
+ printf "<body>\n\n<div id=\"page\">\n\n<div id=\"header\">\n</div>\n\n";
+ printf "<div id=\"main\">\n\n"
+ end
let self = "http://coq.inria.fr"
let trailer () =
if !index && !current_module <> "Index" then
printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"index.html\">Index</a>";
- if !header_trailer then begin
- printf "<hr/>This page has been generated by ";
- printf "<a href=\"%s\">coqdoc</a>\n" self;
- printf "</div>\n\n</div>\n\n</body>\n</html>"
- end
+ if !header_trailer then
+ if !footer_file_spec then
+ let cin = Pervasives.open_in !footer_file in
+ try
+ while true do
+ let s = Pervasives.input_line cin in
+ printf "%s\n" s
+ done
+ with End_of_file -> Pervasives.close_in cin
+ else
+ begin
+ printf "<hr/>This page has been generated by ";
+ printf "<a href=\"%s\">coqdoc</a>\n" self;
+ printf "</div>\n\n</div>\n\n</body>\n</html>"
+ end
let start_module () =
if not !short then begin
- (* add_toc_entry (Toc_library !current_module); *)
+ add_toc_entry (Toc_library !current_module);
printf "<h1 class=\"libtitle\">Library %s</h1>\n\n" !current_module
end
@@ -338,14 +429,15 @@ module Html = struct
raw_ident s
i*)
- let ident_ref m fid s = match find_module m with
- | Local ->
- printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; raw_ident s; printf "</a>"
- | Coqlib when !externals ->
- let m = Filename.concat !coqlib m in
- printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; raw_ident s; printf "</a>"
- | Coqlib | Unknown ->
- raw_ident s
+ let ident_ref m fid s =
+ match find_module m with
+ | Local ->
+ printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; raw_ident s; printf "</a>"
+ | Coqlib when !externals ->
+ let m = Filename.concat !coqlib m in
+ printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; raw_ident s; printf "</a>"
+ | Coqlib | Unknown ->
+ raw_ident s
let ident s loc =
if is_keyword s then begin
@@ -360,9 +452,9 @@ module Html = struct
printf "<a name=\"%s\"></a>" fullid; raw_ident s
| Mod (m,s') when s = s' ->
module_ref m s
- | Ref (m,fullid) ->
+ | Ref (m,fullid,ty) ->
ident_ref m fullid s
- | Mod _ | Ref _ ->
+ | Mod _ ->
raw_ident s)
with Not_found ->
raw_ident s
@@ -429,17 +521,6 @@ module Html = struct
let rule () = printf "<hr/>\n"
- let entry_type = function
- | Library -> "library"
- | Module -> "module"
- | Definition -> "definition"
- | Inductive -> "inductive"
- | Constructor -> "constructor"
- | Lemma -> "lemma"
- | Variable -> "variable"
- | Axiom -> "axiom"
- | TacticDefinition -> "tactic definition"
-
(* make a HTML index from a list of triples (name,text,link) *)
let index_ref i c =
let idxc = sprintf "%s_%c" i.idx_name c in
@@ -465,7 +546,7 @@ module Html = struct
if t = Library then
"[library]", m ^ ".html"
else
- sprintf "[%s, in <a href=\"%s.html\">%s</a>]" (entry_type t) m m ,
+ sprintf "[%s, in <a href=\"%s.html\">%s</a>]" (type_name t) m m ,
sprintf "%s.html#%s" m s)
let format_bytype_index = function
@@ -548,8 +629,8 @@ module Html = struct
item n;
printf "<a href=\"%s\">" r; f (); printf "</a>\n"
in
- Queue.iter make_toc_entry toc_q;
- stop_item ();
+ Queue.iter make_toc_entry toc_q;
+ stop_item ();
end
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index e16c7979..8be3e0b0 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -1,3 +1,4 @@
+(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -6,28 +7,24 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: pretty.mll 10248 2007-10-23 13:02:56Z notin $ i*)
+(*i $Id: pretty.mll 11154 2008-06-19 18:42:19Z msozeau $ i*)
(*s Utility functions for the scanners *)
{
-
- open Cdglobals
open Printf
- open Index
open Lexing
- open Output
(* count the number of spaces at the beginning of a string *)
let count_spaces s =
let n = String.length s in
let rec count c i =
- if i == n then c else match s.[i] with
+ if i == n then c,i else match s.[i] with
| '\t' -> count (c + (8 - (c mod 8))) (i + 1)
| ' ' -> count (c + 1) (i + 1)
- | _ -> c
+ | _ -> c,i
in
- count 0 0
+ count 0 0
let count_dashes s =
let c = ref 0 in
@@ -52,6 +49,11 @@
in
count 0 (String.index s '*')
+ let strip_eol s =
+ let eol = s.[String.length s - 1] = '\n' in
+ (eol, if eol then String.sub s 1 (String.length s - 1) else s)
+
+
let formatted = ref false
let brackets = ref 0
@@ -69,22 +71,22 @@
let state_stack = Stack.create ()
let save_state () =
- Stack.push { st_gallina = !gallina; st_light = !light } state_stack
+ Stack.push { st_gallina = !Cdglobals.gallina; st_light = !Cdglobals.light } state_stack
let restore_state () =
let s = Stack.pop state_stack in
- gallina := s.st_gallina;
- light := s.st_light
+ Cdglobals.gallina := s.st_gallina;
+ Cdglobals.light := s.st_light
let without_ref r f x = save_state (); r := false; f x; restore_state ()
- let without_gallina = without_ref gallina
+ let without_gallina = without_ref Cdglobals.gallina
- let without_light = without_ref light
+ let without_light = without_ref Cdglobals.light
let show_all f = without_gallina (without_light f)
- let begin_show () = save_state (); gallina := false; light := false
+ let begin_show () = save_state (); Cdglobals.gallina := false; Cdglobals.light := false
let end_show () = restore_state ()
(* Reset the globals *)
@@ -163,15 +165,20 @@
let space = [' ' '\t']
let space_nl = [' ' '\t' '\n' '\r']
+let nl = "\r\n" | '\n'
let firstchar =
['A'-'Z' 'a'-'z' '_'
(* iso 8859-1 accents *)
'\192'-'\214' '\216'-'\246' '\248'-'\255' ] |
+ '\194' '\185' |
(* utf-8 latin 1 supplement *)
'\195' ['\128'-'\191'] |
(* utf-8 letterlike symbols *)
- '\226' ('\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])
+ '\206' ['\177'-'\183'] |
+ '\226' ('\130' [ '\128'-'\137' ] (* subscripts *)
+ | '\129' [ '\176'-'\187' ] (* superscripts *)
+ | '\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])
let identchar =
firstchar | ['\'' '0'-'9' '@' ]
let id = firstchar identchar*
@@ -186,8 +193,9 @@ let symbolchar_no_brackets =
(* utf-8 symbols *)
'\226' ['\134'-'\143' '\152'-'\155' '\164'-'\165' '\168'-'\171'] _
let symbolchar = symbolchar_no_brackets | '[' | ']'
+let token_no_brackets = symbolchar_no_brackets+
let token = symbolchar+ | '[' [^ '[' ']' ':']* ']'
-
+let printing_token = (token | id)+
let thm_token =
"Theorem"
@@ -202,6 +210,7 @@ let thm_token =
let def_token =
"Definition"
| "Let"
+ | "Class"
| "SubClass"
| "Example"
| "Local"
@@ -209,11 +218,10 @@ let def_token =
| "CoFixpoint"
| "Record"
| "Structure"
+ | "Instance"
| "Scheme"
| "Inductive"
| "CoInductive"
- | "Program" space+ "Definition"
- | "Program" space+ "Fixpoint"
let decl_token =
"Hypothesis"
@@ -224,6 +232,8 @@ let decl_token =
let gallina_ext =
"Module"
+ | "Include" space+ "Type"
+ | "Include"
| "Declare" space+ "Module"
| "Transparent"
| "Opaque"
@@ -235,6 +245,11 @@ let gallina_ext =
| "Infix"
| "Tactic" space+ "Notation"
| "Reserved" space+ "Notation"
+ | "Section"
+ | "Context"
+ | "Variable" 's'?
+ | ("Hypothesis" | "Hypotheses")
+ | "End"
let commands =
"Pwd"
@@ -254,6 +269,12 @@ let commands =
| "Check"
| "Type"
+ | "Section"
+ | "Chapter"
+ | "Variable" 's'?
+ | ("Hypothesis" | "Hypotheses")
+ | "End"
+
let extraction =
"Extraction"
| "Recursive" space+ "Extraction"
@@ -261,6 +282,12 @@ let extraction =
let gallina_kw = thm_token | def_token | decl_token | gallina_ext | commands | extraction
+let prog_kw =
+ "Program" space+ gallina_kw
+ | "Obligation"
+ | "Obligations"
+ | "Solve"
+
let gallina_kw_to_hide =
"Implicit"
| "Ltac"
@@ -275,11 +302,6 @@ let gallina_kw_to_hide =
| "Transparent"
| "Opaque"
| ("Declare" space+ ("Morphism" | "Step") )
- | "Section"
- | "Chapter"
- | "Variable" 's'?
- | ("Hypothesis" | "Hypotheses")
- | "End"
| ("Set" | "Unset") space+ "Printing" space+ "Coercions"
| "Declare" space+ ("Left" | "Right") space+ "Step"
@@ -294,10 +316,10 @@ let section = "*" | "**" | "***" | "****"
let item_space = " "
-let begin_hide = "(*" space* "begin" space+ "hide" space* "*)" space* '\n'
-let end_hide = "(*" space* "end" space+ "hide" space* "*)" space* '\n'
-let begin_show = "(*" space* "begin" space+ "show" space* "*)" space* '\n'
-let end_show = "(*" space* "end" space+ "show" space* "*)" space* '\n'
+let begin_hide = "(*" space* "begin" space+ "hide" space* "*)" space* nl
+let end_hide = "(*" space* "end" space+ "hide" space* "*)" space* nl
+let begin_show = "(*" space* "begin" space+ "show" space* "*)" space* nl
+let end_show = "(*" space* "end" space+ "show" space* "*)" space* nl
(*
let begin_verb = "(*" space* "begin" space+ "verb" space* "*)"
let end_verb = "(*" space* "end" space+ "verb" space* "*)"
@@ -308,16 +330,16 @@ let end_verb = "(*" space* "end" space+ "verb" space* "*)"
(*s Scanning Coq, at beginning of line *)
rule coq_bol = parse
- | space* '\n'+
- { empty_line_of_code (); coq_bol lexbuf }
+ | space* nl+
+ { Output.empty_line_of_code (); coq_bol lexbuf }
| space* "(**" space_nl
- { end_coq (); start_doc ();
+ { Output.end_coq (); Output.start_doc ();
let eol = doc_bol lexbuf in
- end_doc (); start_coq ();
+ Output.end_doc (); Output.start_coq ();
if eol then coq_bol lexbuf else coq lexbuf }
| space* "Comments" space_nl
- { end_coq (); start_doc (); comments lexbuf; end_doc ();
- start_coq (); coq lexbuf }
+ { Output.end_coq (); Output.start_doc (); comments lexbuf; Output.end_doc ();
+ Output.start_coq (); coq lexbuf }
| space* begin_hide
{ skip_hide lexbuf; coq_bol lexbuf }
| space* begin_show
@@ -326,28 +348,38 @@ rule coq_bol = parse
{ end_show (); coq_bol lexbuf }
| space* gallina_kw_to_hide
{ let s = lexeme lexbuf in
- if !light && section_or_end s then begin
- skip_to_dot lexbuf;
- coq_bol lexbuf
- end else begin
- let nbsp = count_spaces s in
- indentation nbsp;
- let s = String.sub s nbsp (String.length s - nbsp) in
- ident s (lexeme_start lexbuf + nbsp);
- let eol= body lexbuf in
- if eol then coq_bol lexbuf else coq lexbuf
- end }
+ if !Cdglobals.light && section_or_end s then
+ let eol = skip_to_dot lexbuf in
+ if eol then (Output.line_break (); coq_bol lexbuf) else coq lexbuf
+ else
+ begin
+ let nbsp,isp = count_spaces s in
+ Output.indentation nbsp;
+ let s = String.sub s isp (String.length s - isp) in
+ Output.ident s (lexeme_start lexbuf + isp);
+ let eol = body lexbuf in
+ if eol then coq_bol lexbuf else coq lexbuf
+ end }
| space* gallina_kw
{ let s = lexeme lexbuf in
- let nbsp = count_spaces s in
- let s = String.sub s nbsp (String.length s - nbsp) in
- indentation nbsp;
- ident s (lexeme_start lexbuf + nbsp);
+ let nbsp,isp = count_spaces s in
+ let s = String.sub s isp (String.length s - isp) in
+ Output.indentation nbsp;
+ Output.ident s (lexeme_start lexbuf + isp);
let eol= body lexbuf in
if eol then coq_bol lexbuf else coq lexbuf }
- | space* "(**" space+ "printing" space+ (identifier | token) space+
+ | space* prog_kw
+ { let s = lexeme lexbuf in
+ let nbsp,isp = count_spaces s in
+ Output.indentation nbsp;
+ let s = String.sub s isp (String.length s - isp) in
+ Output.ident s (lexeme_start lexbuf + isp);
+ let eol= body lexbuf in
+ if eol then coq_bol lexbuf else coq lexbuf }
+
+ | space* "(**" space+ "printing" space+ printing_token space+
{ let tok = lexeme lexbuf in
- let s = printing_token lexbuf in
+ let s = printing_token_body lexbuf in
add_printing_token tok s;
coq_bol lexbuf }
| space* "(**" space+ "printing" space+
@@ -366,13 +398,13 @@ rule coq_bol = parse
coq_bol lexbuf }
| space* "(*"
{ let eol = comment lexbuf in
- if eol then begin line_break(); coq_bol lexbuf end else coq lexbuf }
+ if eol then coq_bol lexbuf else coq lexbuf }
| eof
{ () }
| _
{ let eol =
- if not !gallina then
- begin backtrack lexbuf; indentation 0; body_bol lexbuf end
+ if not !Cdglobals.gallina then
+ begin backtrack lexbuf; Output.indentation 0; body_bol lexbuf end
else
skip_to_dot lexbuf
in
@@ -381,141 +413,148 @@ rule coq_bol = parse
(*s Scanning Coq elsewhere *)
and coq = parse
- | "\n"
- { line_break(); coq_bol lexbuf }
+ | nl
+ { Output.line_break(); coq_bol lexbuf }
| "(**" space_nl
- { end_coq (); start_doc ();
+ { Output.end_coq (); Output.start_doc ();
let eol = doc_bol lexbuf in
- end_doc (); start_coq ();
+ Output.end_doc (); Output.start_coq ();
if eol then coq_bol lexbuf else coq lexbuf }
| "(*"
{ let eol = comment lexbuf in
- if eol then begin line_break(); coq_bol lexbuf end
+ if eol then begin Output.line_break(); coq_bol lexbuf end
else coq lexbuf
}
- | '\n'+ space* "]]"
- { if not !formatted then begin symbol (lexeme lexbuf); coq lexbuf end }
+ | nl+ space* "]]"
+ { if not !formatted then begin Output.symbol (lexeme lexbuf); coq lexbuf end }
| eof
{ () }
| gallina_kw_to_hide
{ let s = lexeme lexbuf in
- if !light && section_or_end s then
+ if !Cdglobals.light && section_or_end s then
begin
let eol = skip_to_dot lexbuf in
if eol then coq_bol lexbuf else coq lexbuf
end
else
begin
- ident s (lexeme_start lexbuf);
+ Output.ident s (lexeme_start lexbuf);
let eol=body lexbuf in
if eol then coq_bol lexbuf else coq lexbuf
end }
| gallina_kw
{ let s = lexeme lexbuf in
- ident s (lexeme_start lexbuf);
+ Output.ident s (lexeme_start lexbuf);
let eol = body lexbuf in
if eol then coq_bol lexbuf else coq lexbuf }
- | space+ { char ' '; coq lexbuf }
+ | prog_kw
+ { let s = lexeme lexbuf in
+ Output.ident s (lexeme_start lexbuf);
+ let eol = body lexbuf in
+ if eol then coq_bol lexbuf else coq lexbuf }
+ | space+ { Output.char ' '; coq lexbuf }
| eof
{ () }
- | _ { let eol =
- if not !gallina then
- begin backtrack lexbuf; indentation 0; body lexbuf end
+ | _ { let eol =
+ if not !Cdglobals.gallina then
+ begin backtrack lexbuf; Output.indentation 0; body lexbuf end
else
- skip_to_dot lexbuf
+ let eol = skip_to_dot lexbuf in
+ if eol then Output.line_break (); eol
in
if eol then coq_bol lexbuf else coq lexbuf}
(*s Scanning documentation, at beginning of line *)
-
+
and doc_bol = parse
- | space* "\n" '\n'*
- { paragraph (); doc_bol lexbuf }
- | space* section [^')'] ([^'\n' '*'] | '*' [^'\n'')'])*
-{ let lev, s = sec_title (lexeme lexbuf) in
- section lev (fun () -> ignore (doc (from_string s)));
- doc lexbuf }
-| space* '-'+
- { let n = count_dashes (lexeme lexbuf) in
- if n >= 4 then rule () else item n;
- doc lexbuf }
-| "<<" space*
- { start_verbatim (); verbatim lexbuf; doc_bol lexbuf }
+ | space* nl+
+ { Output.paragraph (); doc_bol lexbuf }
+ | space* section space+ ([^'\n' '*'] | '*'+ [^'\n' ')' '*'])* ('*'+ '\n')?
+ { let eol, lex = strip_eol (lexeme lexbuf) in
+ let lev, s = sec_title lex in
+ Output.section lev (fun () -> ignore (doc (from_string s)));
+ if eol then doc_bol lexbuf else doc lexbuf }
+ | space* '-'+
+ { let n = count_dashes (lexeme lexbuf) in
+ if n >= 4 then Output.rule () else Output.item n;
+ doc lexbuf }
+ | "<<" space*
+ { Output.start_verbatim (); verbatim lexbuf; doc_bol lexbuf }
| eof
- { false }
+ { true }
| _
{ backtrack lexbuf; doc lexbuf }
(*s Scanning documentation elsewhere *)
and doc = parse
- | "\n"
- { char '\n'; doc_bol lexbuf }
+ | nl
+ { Output.char '\n'; doc_bol lexbuf }
| "["
{ brackets := 1;
- start_inline_coq (); escaped_coq lexbuf; end_inline_coq ();
+ Output.start_inline_coq (); escaped_coq lexbuf; Output.end_inline_coq ();
doc lexbuf }
- | "[[" '\n' space*
- { formatted := true; line_break (); start_inline_coq ();
- indentation (count_spaces (lexeme lexbuf));
+ | "[[" nl space*
+ { formatted := true; Output.line_break (); Output.start_inline_coq ();
+ Output.indentation (fst (count_spaces (lexeme lexbuf)));
let eol = body_bol lexbuf in
- end_inline_coq (); formatted := false;
+ Output.end_inline_coq (); formatted := false;
if eol then doc_bol lexbuf else doc lexbuf}
- | '*'* "*)" space* '\n'
+ | '*'* "*)" space* nl
{ true }
| '*'* "*)"
{ false }
| "$"
- { start_latex_math (); escaped_math_latex lexbuf; doc lexbuf }
+ { Output.start_latex_math (); escaped_math_latex lexbuf; doc lexbuf }
| "$$"
- { char '$'; doc lexbuf }
+ { Output.char '$'; doc lexbuf }
| "%"
{ escaped_latex lexbuf; doc lexbuf }
| "%%"
- { char '%'; doc lexbuf }
+ { Output.char '%'; doc lexbuf }
| "#"
{ escaped_html lexbuf; doc lexbuf }
| "##"
- { char '#'; doc lexbuf }
+ { Output.char '#'; doc lexbuf }
| eof
{ false }
| _
- { char (lexeme_char lexbuf 0); doc lexbuf }
+ { Output.char (lexeme_char lexbuf 0); doc lexbuf }
(*s Various escapings *)
and escaped_math_latex = parse
- | "$" { stop_latex_math () }
- | eof { stop_latex_math () }
- | _ { latex_char (lexeme_char lexbuf 0); escaped_math_latex lexbuf }
+ | "$" { Output.stop_latex_math () }
+ | eof { Output.stop_latex_math () }
+ | _ { Output.latex_char (lexeme_char lexbuf 0); escaped_math_latex lexbuf }
and escaped_latex = parse
| "%" { () }
| eof { () }
- | _ { latex_char (lexeme_char lexbuf 0); escaped_latex lexbuf }
+ | _ { Output.latex_char (lexeme_char lexbuf 0); escaped_latex lexbuf }
and escaped_html = parse
| "#" { () }
| "&#"
- { html_char '&'; html_char '#'; escaped_html lexbuf }
+ { Output.html_char '&'; Output.html_char '#'; escaped_html lexbuf }
| "##"
- { html_char '#'; escaped_html lexbuf }
+ { Output.html_char '#'; escaped_html lexbuf }
| eof { () }
- | _ { html_char (lexeme_char lexbuf 0); escaped_html lexbuf }
+ | _ { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf }
and verbatim = parse
- | "\n>>" { verbatim_char '\n'; stop_verbatim () }
- | eof { stop_verbatim () }
- | _ { verbatim_char (lexeme_char lexbuf 0); verbatim lexbuf }
+ | nl ">>" { Output.verbatim_char '\n'; Output.stop_verbatim () }
+ | eof { Output.stop_verbatim () }
+ | _ { Output.verbatim_char (lexeme_char lexbuf 0); verbatim lexbuf }
(*s Coq, inside quotations *)
and escaped_coq = parse
| "]"
{ decr brackets;
- if !brackets > 0 then begin char ']'; escaped_coq lexbuf end }
+ if !brackets > 0 then begin Output.char ']'; escaped_coq lexbuf end }
| "["
- { incr brackets; char '['; escaped_coq lexbuf }
+ { incr brackets; Output.char '['; escaped_coq lexbuf }
| "(*"
{ ignore (comment lexbuf); escaped_coq lexbuf }
| "*)"
@@ -524,18 +563,18 @@ and escaped_coq = parse
{ () }
| token_brackets
{ let s = lexeme lexbuf in
- symbol s;
+ Output.symbol s;
escaped_coq lexbuf }
| (identifier '.')* identifier
- { ident (lexeme lexbuf) (lexeme_start lexbuf); escaped_coq lexbuf }
+ { Output.ident (lexeme lexbuf) (lexeme_start lexbuf); escaped_coq lexbuf }
| _
- { char (lexeme_char lexbuf 0); escaped_coq lexbuf }
+ { Output.char (lexeme_char lexbuf 0); escaped_coq lexbuf }
(*s Coq "Comments" command. *)
and comments = parse
| space_nl+
- { char ' '; comments lexbuf }
+ { Output.char ' '; comments lexbuf }
| '"' [^ '"']* '"'
{ let s = lexeme lexbuf in
let s = String.sub s 1 (String.length s - 2) in
@@ -547,61 +586,79 @@ and comments = parse
| eof
{ () }
| _
- { char (lexeme_char lexbuf 0); comments lexbuf }
+ { Output.char (lexeme_char lexbuf 0); comments lexbuf }
(*s Skip comments *)
and comment = parse
- | "(*" { ignore (comment lexbuf); comment lexbuf }
- | "*)" space* '\n'+ { true }
+ | "(*" { comment lexbuf }
+ | "*)" space* nl { true }
| "*)" { false }
| eof { false }
| _ { comment lexbuf }
and skip_to_dot = parse
- | '.' space* '\n' { true }
+ | '.' space* nl { true }
| eof | '.' space+ { false}
| "(*" { ignore (comment lexbuf); skip_to_dot lexbuf }
| _ { skip_to_dot lexbuf }
and body_bol = parse
| space+
- { indentation (count_spaces (lexeme lexbuf)); body lexbuf }
+ { Output.indentation (fst (count_spaces (lexeme lexbuf))); body lexbuf }
| _ { backtrack lexbuf; body lexbuf }
and body = parse
- | '\n' {line_break(); body_bol lexbuf}
- | '\n'+ space* "]]"
- { if not !formatted then begin symbol (lexeme lexbuf); body lexbuf end else true }
+ | nl {Output.line_break(); body_bol lexbuf}
+ | nl+ space* "]]"
+ { if not !formatted then begin Output.symbol (lexeme lexbuf); body lexbuf end else true }
| eof { false }
- | '.' space* '\n' | '.' space* eof { char '.'; line_break(); true }
- | '.' space+ { char '.'; char ' '; false }
+ | '.' 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
- if eol then begin line_break(); body_bol lexbuf end else body lexbuf }
+ if eol
+ then begin Output.line_break(); body_bol lexbuf end
+ else body lexbuf }
| identifier
{ let s = lexeme lexbuf in
- ident s (lexeme_start lexbuf);
+ Output.ident s (lexeme_start lexbuf);
body lexbuf }
- | token
+ | token_no_brackets
{ let s = lexeme lexbuf in
- symbol s; body lexbuf }
+ Output.symbol s; body lexbuf }
| _ { let c = lexeme_char lexbuf 0 in
- char c;
+ Output.char c;
body lexbuf }
+and notation_bol = parse
+ | space+
+ { Output.indentation (fst (count_spaces (lexeme lexbuf))); notation lexbuf }
+ | _ { backtrack lexbuf; notation lexbuf }
+
+and notation = parse
+ | nl { Output.line_break(); notation_bol lexbuf }
+ | '"' { Output.char '"'; false }
+ | token
+ { let s = lexeme lexbuf in
+ Output.symbol s; notation lexbuf }
+ | _ { let c = lexeme_char lexbuf 0 in
+ Output.char c;
+ notation lexbuf }
+
and skip_hide = parse
| eof | end_hide { () }
| _ { skip_hide lexbuf }
(*s Reading token pretty-print *)
-and printing_token = parse
+and printing_token_body = parse
| "*)" | eof
{ let s = Buffer.contents token_buffer in
Buffer.clear token_buffer;
s }
| _ { Buffer.add_string token_buffer (lexeme lexbuf);
- printing_token lexbuf }
+ printing_token_body lexbuf }
(*s Applying the scanners to files *)
@@ -609,11 +666,11 @@ and printing_token = parse
let coq_file f m =
reset ();
- Index.scan_file f m;
- start_module ();
+ Index.current_library := m;
+ Output.start_module ();
let c = open_in f in
let lb = from_channel c in
- start_coq (); coq_bol lb; end_coq ();
+ Output.start_coq (); coq_bol lb; Output.end_coq ();
close_in c
}
diff --git a/tools/coqwc.mll b/tools/coqwc.mll
index 0ce172ea..81fe06cd 100644
--- a/tools/coqwc.mll
+++ b/tools/coqwc.mll
@@ -9,7 +9,7 @@
(* coqwc - counts the lines of spec, proof and comments in Coq sources
* Copyright (C) 2003 Jean-Christophe Filliâtre *)
-(*i $Id: coqwc.mll 9976 2007-07-12 11:58:30Z msozeau $ i*)
+(*i $Id: coqwc.mll 9691 2007-03-08 15:29:27Z msozeau $ i*)
(*s {\bf coqwc.} Counts the lines of spec, proof and comments in a Coq source.
It assumes the files to be lexically well-formed. *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-28 14:45:37 +0000