From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 1 Feb 2009 00:54:40 +0100 Subject: Imported Upstream version 8.2~rc2+dfsg --- tools/beautify-archive | 52 ++++++ tools/coq_makefile.ml4 | 441 +++++++++++++++++++++++++++++----------------- tools/coqdep.ml | 26 +-- tools/coqdoc/cdglobals.ml | 3 +- tools/coqdoc/coqdoc.css | 38 +++- tools/coqdoc/coqdoc.sty | 104 +++++++---- tools/coqdoc/index.mli | 4 +- tools/coqdoc/index.mll | 48 +++-- tools/coqdoc/main.ml | 24 ++- tools/coqdoc/output.ml | 365 +++++++++++++++++++++++++------------- tools/coqdoc/output.mli | 4 +- tools/coqdoc/pretty.mll | 113 ++++++++---- 12 files changed, 837 insertions(+), 385 deletions(-) create mode 100755 tools/beautify-archive (limited to 'tools') diff --git a/tools/beautify-archive b/tools/beautify-archive new file mode 100755 index 00000000..aac6f3e0 --- /dev/null +++ b/tools/beautify-archive @@ -0,0 +1,52 @@ +#!/bin/sh + +#This script compiles and beautifies an archive, check the correctness +#of beautified files, then replace the original files by the +#beautified ones, keeping a copy of original files in $OLDARCHIVE. +#The script assumes: +#- that the archive provides a Makefile built by coq_makefile, +#- that coqc is in the path or that variables COQTOP and COQBIN are set. + +OLDARCHIVE=old_files +NEWARCHIVE=beautify_files +BEAUTIFYSUFFIX=.beautified + +if [ -e $OLDARCHIVE ]; then + echo "Warning: $OLDARCHIVE directory found, the files are maybe already beautified"; + sleep 5; +fi +echo ---- Producing beautified files in the beautification directory ------- +if [ -e $NEWARCHIVE ]; then rm -r $NEWARCHIVE; fi +if [ -e /tmp/$OLDARCHIVE.$$ ]; then rm -r /tmp/$OLDARCHIVE.$$; fi +cp -pr . /tmp/$OLDARCHIVE.$$ +cp -pr /tmp/$OLDARCHIVE.$$ $NEWARCHIVE +cd $NEWARCHIVE +rm description || true +make clean +make COQFLAGS='-beautify -q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)' || \ + { echo ---- Failed to beautify; exit 1; } +echo -------- Upgrading files in the beautification directory -------------- +beaufiles=`find . -name \*.v$BEAUTIFYSUFFIX` +for i in $beaufiles; do + j=`dirname $i`/`basename $i .v$BEAUTIFYSUFFIX`.v + echo Upgrading $j in the beautification directory + mv -u -f $i $j +done +echo ---- Recompiling beautified files in the beautification directory ----- +make clean +make || { echo ---- Failed to recompile; exit 1; } +echo ----- Saving old files in directory $OLDARCHIVE ------------------------- +/bin/rm -r ../$OLDARCHIVE +mv /tmp/$OLDARCHIVE.$$ ../$OLDARCHIVE +echo Saving $OLDARCHIVE files done +echo --------- Upgrading files in current directory ------------------------ +vfiles=`find . -name \*.v` +cd .. +for i in $vfiles; do + echo Upgrading $i in current directory + mv -u -f $NEWARCHIVE/$i $i +done +echo -------- Beautification completed ------------------------------------- +echo Old files are in directory '"$OLDARCHIVE"' +echo New files are in current directory +echo You can now remove the beautification directory '"$NEWARCHIVE"' diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index d1d0d854..3fbf71dd 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 11255 2008-07-24 16:57:13Z notin $ *) +(* $Id: coq_makefile.ml4 11771 2009-01-09 18:00:56Z notin $ *) (* créer un Makefile pour un développement Coq automatiquement *) @@ -29,6 +29,7 @@ let some_mlfile = ref false let opt = ref "-opt" let impredicative_set = ref false +let no_install = ref false let print x = output_string !output_channel x let printf x = Printf.fprintf !output_channel x @@ -38,6 +39,14 @@ let rec print_list sep = function | x :: l -> print x; print sep; print_list sep l | [] -> () +let list_iter_i f = + let rec aux i = function [] -> () | a::l -> f i a; aux (i+1) l in aux 1 + +let best_ocamlc = + if Coq_config.best = "opt" then "ocamlc.opt" else "ocamlc" +let best_ocamlopt = + if Coq_config.best = "opt" then "ocamlopt.opt" else "ocamlopt" + let section s = let l = String.length s in let sep = String.make (l+5) '#' @@ -58,10 +67,11 @@ let usage () = coq_makefile [subdirectory] .... [file.v] ... [file.ml] ... [-custom command dependencies file] ... [-I dir] ... [-R physicalpath logicalpath] - ... [VARIABLE = value] ... [-opt|-byte] [-f file] [-o file] [-h] [--help] + ... [VARIABLE = value] ... [-opt|-byte] [-impredicative-set] [-no-install] + [-f file] [-o file] [-h] [--help] [file.v]: Coq file to be compiled -[file.ml]: ML file to be compiled +[file.ml]: Objective Caml file to be compiled [subdirectory] : subdirectory that should be \"made\" [-custom command dependencies file]: add target \"file\" with command \"command\" and dependencies \"dependencies\" @@ -73,26 +83,118 @@ coq_makefile [subdirectory] .... [file.v] ... [file.ml] ... [-custom [-byte]: compile with byte-code version of coq [-opt]: compile with native-code version of coq [-impredicative-set]: compile with option -impredicative-set of coq +[-no-install]: build a makefile with no install target [-f file]: take the contents of file as arguments [-o file]: output should go in file file [-h]: print this usage summary [--help]: equivalent to [-h]\n"; exit 1 -let standard sds sps = +let is_genrule r = + let genrule = Str.regexp("%") in + Str.string_match genrule r 0 + +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 canonize f = + let l = String.length f in + if l > 2 && f.[0] = '.' && f.[1] = '/' then + let n = let i = ref 2 in while !i < l && f.[!i] = '/' do incr i done; !i in + String.sub f n (l-n) + else f + +let is_absolute_prefix dir dir' = + is_prefix (absolute_dir dir) (absolute_dir dir') + +let is_included dir = function + | RInclude (dir',_) -> is_absolute_prefix dir' dir + | Include dir' -> absolute_dir dir = absolute_dir dir' + | _ -> false + +let has_top_file = function + | ML s | V s -> s = Filename.basename s + | _ -> false + +let physical_dir_of_logical_dir ldir = + let pdir = String.copy ldir in + for i = 0 to String.length ldir - 1 do + if pdir.[i] = '.' then pdir.[i] <- '/'; + done; + pdir + +let standard ()= print "byte:\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"; + print "\t$(MAKE) all \"OPT:="; print !opt; print "\"\n\n" + +let is_prefix_of_file dir f = + is_prefix dir (absolute_dir (Filename.dirname f)) + +let classify_files_by_root var files (inc_i,inc_r) = + if not (List.exists (fun (pdir,_,_) -> pdir = ".") inc_r) then + begin + (* Files in the scope of a -R option (assuming they are disjoint) *) + list_iter_i (fun i (pdir,ldir,abspdir) -> + if List.exists (is_prefix_of_file abspdir) files then + printf "%s%d:=$(patsubst %s/%%,%%,$(filter %s/%%,$(%s)))\n" + var i pdir pdir var) + inc_r; + (* Files not in the scope of a -R option *) + let pat_of_dir (pdir,_,_) = pdir^"/%" in + let pdir_patterns = String.concat " " (List.map pat_of_dir inc_r) in + printf "%s0:=$(filter-out %s,$(%s))\n" var pdir_patterns var + end + +let install_include_by_root var files (_,inc_r) = + try + (* All files caught by a -R . option (assuming it is the only one) *) + let ldir = List.assoc "." (List.map (fun (p,l,_) -> (p,l)) inc_r) in + let pdir = physical_dir_of_logical_dir ldir in + printf "\t(for i in $(%s); do \\\n" var; + printf "\t install -D $$i $(COQLIB)/user-contrib/%s/$$i; \\\n" pdir; + printf "\t done)\n" + with Not_found -> + (* Files in the scope of a -R option (assuming they are disjoint) *) + list_iter_i (fun i (pdir,ldir,abspdir) -> + if List.exists (is_prefix_of_file abspdir) files then + begin + let pdir' = physical_dir_of_logical_dir ldir in + printf "\t(cd %s; for i in $(%s%d); do \\\n" pdir var i; + printf "\t install -D $$i $(COQLIB)/user-contrib/%s/$$i; \\\n" pdir'; + printf "\t done)\n" + end) inc_r; + (* Files not in the scope of a -R option *) + printf "\t(for i in $(%s0); do \\\n" var; + printf "\t install -D $$i $(COQLIB)/user-contrib/$(INSTALLDEFAULTROOT)/$$i; \\\n"; + printf "\t done)\n" + +let install (vfiles,mlfiles,_,sds) inc = print "install:\n"; - print "\tmkdir -p `$(COQC) -where`/user-contrib\n"; - if !some_vfile then print "\tcp -f $(VOFILES) `$(COQC) -where`/user-contrib\n"; - if !some_mlfile then print "\tcp -f *.cmo `$(COQC) -where`/user-contrib\n"; + print "\tmkdir -p $(COQLIB)/user-contrib\n"; + if !some_vfile then install_include_by_root "VOFILES" vfiles inc; + if !some_mlfile then install_include_by_root "CMOFILES" mlfiles inc; + if !some_mlfile then install_include_by_root "CMIFILES" mlfiles inc; + if Coq_config.has_natdynlink && !some_mlfile then + install_include_by_root "CMXSFILES" mlfiles inc; List.iter - (fun x -> print "\t(cd "; print x; print " ; $(MAKE) install)\n") + (fun x -> + printf "\t(cd %s; $(MAKE) INSTALLDEFAULTROOT=$(INSTALLDEFAULTROOT)/%s install)\n" x x) sds; - print "\n"; + print "\n" + +let make_makefile sds = if !make_name <> "" then begin printf "%s: %s\n" !makefile_name !make_name; printf "\tmv -f %s %s.bak\n" !makefile_name !makefile_name; @@ -102,16 +204,22 @@ let standard sds sps = (fun x -> print "\t(cd "; print x; print " ; $(MAKE) Makefile)\n") sds; print "\n"; - end; + end + +let clean sds sps = print "clean:\n"; - print "\trm -f *.cmo *.cmi *.cmx *.o $(VOFILES) $(VIFILES) $(GFILES) *~\n"; - print "\trm -f all.ps all-gal.ps all.glob $(VFILES:.v=.glob) $(HTMLFILES) \ + print "\trm -f $(VOFILES) $(VIFILES) $(GFILES) *~\n"; + print "\trm -f all.ps all-gal.ps all.pdf all-gal.pdf 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"; + if Coq_config.has_natdynlink && !some_mlfile then + print "\trm -f $(CMXSFILES) $(CMXSFILES:.cmxs=.o)\n"; print "\t- rm -rf html\n"; List.iter - (fun (file,_,_) -> print "\t- rm -f "; print file; print "\n") + (fun (file,_,_) -> + if not (is_genrule file) then + (print "\t- rm -f "; print file; print "\n")) sps; List.iter (fun x -> print "\t(cd "; print x; print " ; $(MAKE) clean)\n") @@ -122,19 +230,26 @@ let standard sds sps = List.iter (fun x -> print "\t(cd "; print x; print " ; $(MAKE) archclean)\n") sds; - print "\n\n" + print "\n\n"; + print "printenv: \n\t@echo CAMLC =\t$(CAMLC)\n\t@echo CAMLOPTC =\t$(CAMLOPTC)\n"; + print "\t@echo CAMLP4LIB =\t$(CAMLP4LIB)\n\n" -let includes () = +let header_includes () = () + +let footer_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 "%.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 "%.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) -c $(PP) $<\n\n"; + print "%.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -c $(PP) $<\n\n"; + print "%.cmxs: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) $<\n\n"; + print "%.cmo: %.ml4\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; + print "%.cmx: %.ml4\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; print "%.ml.d: %.ml\n"; - print "\t$(CAMLBIN)ocamldep -slash $(ZFLAGS) $(PP) \"$<\" > \"$@\"\n\n" + print "\t$(CAMLBIN)ocamldep -slash $(COQSRCLIBS) $(PP) \"$<\" > \"$@\"\n\n" and v_rule () = 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"; @@ -149,34 +264,10 @@ let implicit () = if !some_mlfile then ml_rules (); if !some_vfile then v_rule () -let variables l = - let rec var_aux = function - | [] -> () - | Def(v,def) :: r -> print v; print "="; print def; print "\n"; var_aux r - | _ :: r -> var_aux r - in +let variables defs = + let var_aux (v,def) = print v; print "="; print def; print "\n" in section "Variables definitions."; - 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)/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/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 $(COQBIN)coqc -where)\n"; - print "COQSRCLIBS:=-I $(COQSRC)\n"); - print "ZFLAGS:=$(OCAMLLIBS) $(COQSRCLIBS)\n"; + print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n"; if !opt = "-byte" then print "override OPT:=-byte\n" else @@ -184,81 +275,62 @@ let variables l = 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 "ifdef CAMLBIN\n COQMKTOPFLAGS:=-camlbin $(CAMLBIN) -camlp4bin $(CAMLP4BIN)\nendif\n"; print "COQC:=$(COQBIN)coqc\n"; print "COQDEP:=$(COQBIN)coqdep -c\n"; print "GALLINA:=$(COQBIN)gallina\n"; print "COQDOC:=$(COQBIN)coqdoc\n"; + print "COQMKTOP:=$(COQBIN)coqmktop\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"; + printf "CAMLC:=$(CAMLBIN)%s -rectypes\n" best_ocamlc; + printf "CAMLOPTC:=$(CAMLBIN)%s -rectypes\n" best_ocamlopt; + printf "CAMLLINK:=$(CAMLBIN)%s -rectypes\n" best_ocamlc; + printf "CAMLOPTLINK:=$(CAMLBIN)%s -rectypes\n" best_ocamlopt; 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 "CAMLP4OPTIONS:=\n"; + List.iter var_aux defs; + print "PP:=-pp \"$(CAMLP4BIN)$(CAMLP4)o -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl\"\n"; 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 parameters () = + print "# \n"; + print "# This Makefile may take 3 arguments passed as environment variables:\n"; + print "# - COQBIN to specify the directory where Coq binaries resides;\n"; + print "# - CAMLBIN and CAMLP4BIN to give the path for the OCaml and Camlp4/5 binaries.\n"; + print "COQLIB:=$(shell $(COQBIN)coqtop -where | sed -e 's/\\\\/\\\\\\\\/g')\n"; + print "CAMLP4:=\"$(shell $(COQBIN)coqtop -config | awk -F = '/CAMLP4=/{print $$2}')\"\n"; + print "ifndef CAMLP4BIN\n CAMLP4BIN:=$(CAMLBIN)\nendif\n\n"; + print "CAMLP4LIB:=$(shell $(CAMLP4BIN)$(CAMLP4) -where)\n\n" -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 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 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 include_dirs (inc_i,inc_r) = + let parse_includes l = List.map (fun (x,_) -> "-I " ^ x) l in + let parse_rec_includes l = + List.map (fun (p,l,_) -> + let l' = if l = "" then "\"\"" else l in "-R " ^ p ^ " " ^ l') + l in + let inc_i' = List.filter (fun (i,_) -> not (List.exists (fun (i',_,_) -> is_absolute_prefix 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 "CAMLP4LIB:=$(shell $(CAMLBIN)camlp5 -where 2> /dev/null || $(CAMLBIN)camlp4 -where)\n"; + let str_r = parse_rec_includes inc_r in + section "Libraries definitions."; print "OCAMLLIBS:=-I $(CAMLP4LIB) "; print_list "\\\n " str_i; print "\n"; + print "COQSRCLIBS:=-I $(COQLIB)/kernel -I $(COQLIB)/lib \\ + -I $(COQLIB)/library -I $(COQLIB)/parsing \\ + -I $(COQLIB)/pretyping -I $(COQLIB)/interp \\ + -I $(COQLIB)/proofs -I $(COQLIB)/tactics \\ + -I $(COQLIB)/toplevel -I $(COQLIB)/contrib/cc -I $(COQLIB)/contrib/dp \\ + -I $(COQLIB)/contrib/extraction -I $(COQLIB)/contrib/field \\ + -I $(COQLIB)/contrib/firstorder -I $(COQLIB)/contrib/fourier \\ + -I $(COQLIB)/contrib/funind -I $(COQLIB)/contrib/interface \\ + -I $(COQLIB)/contrib/micromega -I $(COQLIB)/contrib/omega \\ + -I $(COQLIB)/contrib/ring -I $(COQLIB)/contrib/romega \\ + -I $(COQLIB)/contrib/rtauto -I $(COQLIB)/contrib/setoid_ring \\ + -I $(COQLIB)/contrib/subtac -I $(COQLIB)/contrib/xml\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) @@ -272,15 +344,10 @@ let custom sps = if sps <> [] then section "Custom targets."; List.iter pr_sp sps -let subdirs l = - let rec subdirs_aux = function - | [] -> [] - | Subdir x :: r -> x :: (subdirs_aux r) - | _ :: r -> subdirs_aux r - and pr_subdir s = +let subdirs sds = + let pr_subdir s = 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."; @@ -288,30 +355,31 @@ let subdirs l = print_list " " ("all" :: "opt" :: "byte" :: "archclean" :: "clean" :: "install" :: "depend" :: "html" :: sds); - print "\n\n"; - sds - - -let all_target l = - 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 - let - vfiles, mlfiles, other_targets = parse_arguments l - in - section "Definition of the \"all\" target."; + print "\n\n" + +let rec split_arguments = function + | V n :: r -> + let (v,m,o,s),i,d = split_arguments r in ((canonize n::v,m,o,s),i,d) + | ML n :: r -> + let (v,m,o,s),i,d = split_arguments r in ((v,canonize n::m,o,s),i,d) + | Special (n,dep,c) :: r -> + let (v,m,o,s),i,d = split_arguments r in ((v,m,(n,dep,c)::o,s),i,d) + | Subdir n :: r -> + let (v,m,o,s),i,d = split_arguments r in ((v,m,o,n::s),i,d) + | Include p :: r -> + let t,(i,r),d = split_arguments r in (t,((p,absolute_dir p)::i,r),d) + | RInclude (p,l) :: r -> + let t,(i,r),d = split_arguments r in (t,(i,(p,l,absolute_dir p)::r),d) + | Def (v,def) :: r -> + let t,i,d = split_arguments r in (t,i,(v,def)::d) + | [] -> ([],[],[],[]),([],[]),[] + +let main_targets vfiles mlfiles other_targets inc = if !some_vfile then begin print "VFILES:="; print_list "\\\n " vfiles; print "\n"; print "VOFILES:=$(VFILES:.v=.vo)\n"; + classify_files_by_root "VOFILES" vfiles inc; print "GLOBFILES:=$(VFILES:.v=.glob)\n"; print "VIFILES:=$(VFILES:.v=.vi)\n"; print "GFILES:=$(VFILES:.v=.g)\n"; @@ -322,10 +390,18 @@ let all_target l = begin print "MLFILES:="; print_list "\\\n " mlfiles; print "\n"; print "CMOFILES:=$(MLFILES:.ml=.cmo)\n"; + classify_files_by_root "CMOFILES" mlfiles inc; + print "CMIFILES:=$(MLFILES:.ml=.cmi)\n"; + classify_files_by_root "CMIFILES" mlfiles inc; + print "CMXFILES:=$(MLFILES:.ml=.cmx)\n"; + print "CMXSFILES:=$(MLFILES:.ml=.cmxs)\n"; + classify_files_by_root "CMXSFILES" mlfiles inc; + print "OFILES:=$(MLFILES:.ml=.o)\n"; end; print "\nall: "; if !some_vfile then print "$(VOFILES) "; if !some_mlfile then print "$(CMOFILES) "; + if Coq_config.has_natdynlink && !some_mlfile then print "$(CMXSFILES) "; print_list "\\\n " other_targets; print "\n"; if !some_vfile then begin @@ -341,8 +417,20 @@ let all_target l = 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 "all.pdf: $(VFILES)\n"; + print "\t$(COQDOC) -toc -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n"; + print "all-gal.pdf: $(VFILES)\n"; + print "\t$(COQDOC) -toc -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n"; print "\n\n" end + +let all_target (vfiles, mlfiles, sps, sds) inc = + let special_targets = List.filter (fun (n,_,_) -> not (is_genrule n)) sps in + let other_targets = List.map (fun x,_,_ -> x) special_targets @ sds in + section "Definition of the \"all\" target."; + main_targets vfiles mlfiles other_targets inc; + custom sps; + subdirs sds let parse f = let rec string = parser @@ -379,14 +467,14 @@ let rec process_cmd_line = function opt := "-opt"; process_cmd_line r | "-impredicative-set" :: r -> impredicative_set := true; process_cmd_line r + | "-no-install" :: r -> + no_install := true; process_cmd_line r | "-custom" :: com :: dependencies :: file :: r -> let check_dep f = if Filename.check_suffix f ".v" then some_vfile := true - else if Filename.check_suffix f ".ml" then + else if (Filename.check_suffix f ".ml") || (Filename.check_suffix f ".ml4") then some_mlfile := true - else - () in List.iter check_dep (Str.split (Str.regexp "[ \t]+") dependencies); Special (file,dependencies,com) :: (process_cmd_line r) @@ -411,11 +499,14 @@ let rec process_cmd_line = function if Filename.check_suffix f ".v" then begin 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) + end else if (Filename.check_suffix f ".ml") || (Filename.check_suffix f ".ml4") then begin + some_mlfile := true; + ML f :: (process_cmd_line r) + end else if (Filename.check_suffix f ".mli") then begin + Printf.eprintf "Warning: no need for .mli files, skipped %s\n" f; + process_cmd_line r + end else + Subdir f :: (process_cmd_line r) let banner () = print @@ -462,24 +553,61 @@ let directories_deps l = in iter ([],[]) l +let ensure_root_dir l = + if List.exists (is_included ".") l or not (List.exists has_top_file l) then + l + else + Include "." :: l + +let warn_install_at_root_directory (vfiles,mlfiles,_,_) (inc_i,inc_r) = + let inc_r_top = List.filter (fun (_,ldir,_) -> ldir = "") inc_r in + let inc_top = List.map (fun (p,_,a) -> (p,a)) inc_r_top @ inc_i in + let files = vfiles @ mlfiles in + if not !no_install && + List.exists (fun f -> List.mem_assoc (Filename.dirname f) inc_top) files + then + Printf.eprintf "Warning: install target will copy files at the first level of the coq contributions installation directory; option -R %sis recommended\n" + (if inc_r_top = [] then "" else "with non trivial logical root ") + +let check_overlapping_include (inc_i,inc_r) = + let pwd = Sys.getcwd () in + let rec aux = function + | [] -> () + | (pdir,_,abspdir)::l -> + if not (is_prefix pwd abspdir) then + Printf.eprintf "Warning: in option -R, %s is not a subdirectoty of the current directory\n" pdir; + List.iter (fun (pdir',_,abspdir') -> + if is_prefix abspdir abspdir' or is_prefix abspdir' abspdir then + Printf.eprintf "Warning: in options -R, %s and %s overlap\n" pdir pdir') l; + List.iter (fun (pdir',abspdir') -> + if is_prefix abspdir abspdir' or is_prefix abspdir' abspdir then + Printf.eprintf "Warning: in option -I, %s overlap with %s in option -R\n" pdir' pdir) inc_i + in aux inc_r + let do_makefile args = let l = process_cmd_line args in - 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 l = ensure_root_dir l in + let (_,_,sps,sds as targets), inc, defs = split_arguments l in + warn_install_at_root_directory targets inc; + check_overlapping_include inc; + banner (); + header_includes (); + warning (); + command_line args; + parameters (); + include_dirs inc; + variables defs; + all_target targets inc; + implicit (); + standard (); + if not !no_install then install targets inc; + clean sds sps; + make_makefile sds; + (* TEST directories_deps l; *) + footer_includes (); + warning (); + if not (!output_channel == stdout) then close_out !output_channel; + exit 0 let main () = let args = @@ -489,4 +617,3 @@ let main () = do_makefile args let _ = Printexc.catch main () - diff --git a/tools/coqdep.ml b/tools/coqdep.ml index b4b161f5..4febe9d1 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqdep.ml 11282 2008-07-28 11:51:53Z msozeau $ *) +(* $Id: coqdep.ml 11749 2009-01-05 14:01:04Z notin $ *) open Printf open Coqdep_lexer @@ -15,8 +15,6 @@ open Unix let stderr = Pervasives.stderr let stdout = Pervasives.stdout -let coqlib = ref Coq_config.coqlib - let option_c = ref false let option_D = ref false let option_w = ref false @@ -24,7 +22,6 @@ let option_i = ref false let option_sort = ref false let option_glob = ref false let option_slash = ref false -let option_boot = ref false let suffixe = ref ".vo" let suffixe_spec = ref ".vi" @@ -245,7 +242,11 @@ let traite_fichier_Coq verbose f = addQueue deja_vu_ml s; try let mldir = Hashtbl.find mlKnown s in - printf " %s.cmo" (file_name ([String.uncapitalize s],mldir)) + let filename = file_name ([String.uncapitalize s],mldir) in + if Coq_config.has_natdynlink then + printf " %s.cmo %s.cmxs" filename filename + else + printf " %s.cmo" filename with Not_found -> () end) sl @@ -501,14 +502,14 @@ let rec parse = function | "-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 + | "-boot" :: ll -> Flags.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" :: (r :: ll) -> Flags.coqlib_spec := true; Flags.coqlib := r; parse ll | "-coqlib" :: [] -> usage () | "-suffix" :: (s :: ll) -> suffixe := s ; suffixe_spec := s; parse ll | "-suffix" :: [] -> usage () @@ -519,13 +520,14 @@ let rec parse = function let coqdep () = if Array.length Sys.argv < 2 then usage (); parse (List.tl (Array.to_list Sys.argv)); - if !option_boot then begin + if !Flags.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 else begin + let coqlib = Envars.coqlib () in + 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; diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml index 3339b1db..5bcbed64 100644 --- a/tools/coqdoc/cdglobals.ml +++ b/tools/coqdoc/cdglobals.ml @@ -10,7 +10,7 @@ (*s Output options *) -type target_language = LaTeX | HTML | TeXmacs +type target_language = LaTeX | HTML | TeXmacs | Raw let target_language = ref HTML @@ -57,6 +57,7 @@ let externals = ref true let coqlib = ref "http://coq.inria.fr/library/" let coqlib_path = ref Coq_config.coqlib let raw_comments = ref false +let interpolate = ref false let charset = ref "iso-8859-1" let inputenc = ref "" diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css index 65c39b7a..a9a99706 100644 --- a/tools/coqdoc/coqdoc.css +++ b/tools/coqdoc/coqdoc.css @@ -25,7 +25,7 @@ body { padding: 0px 0px; padding: 10px; overflow: hidden; font-size: 100%; - line-height: 80% } + line-height: 100% } #main a.idref:visited {color : #416DFF; text-decoration : none; } #main a.idref:link {color : #416DFF; text-decoration : none; } @@ -43,8 +43,6 @@ body { padding: 0px 0px; #main .section { background-color:#90bdff; font-size : 175% } -#main code { font-family: monospace } - #main .doc { margin: 0px; padding: 10px; font-family: sans-serif; @@ -55,7 +53,13 @@ body { padding: 0px 0px; background-color: #90bdff; border-style: plain} -#main .doc code { font-family: monospace} +.inlinecode { + display: inline; + font-family: monospace } + +.code { + display: block; + font-family: monospace } /* Pied de page */ @@ -66,3 +70,29 @@ body { padding: 0px 0px; #footer a:link { text-decoration: none; color: #888888; } +.id { display: inline; } + +.id[type="constructor"] { + color: rgb(60%,0%,0%); +} + +.id[type="var"] { + color: rgb(40%,0%,40%); +} + +.id[type="definition"] { + color: rgb(0%,40%,0%); +} + +.id[type="lemma"] { + color: rgb(0%,40%,0%); +} + +.id[type="inductive"] { + color: rgb(0%,0%,80%); +} + +.id[type="keyword"] { + color : #cf1d1d; +/* color: black; */ +} diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty index d31314c5..ef4f4119 100644 --- a/tools/coqdoc/coqdoc.sty +++ b/tools/coqdoc/coqdoc.sty @@ -27,6 +27,11 @@ %HEVEA\renewcommand{\medskip}{} %HEVEA\renewcommand{\bigskip}{} + +%HEVEA\newcommand{\lnot}{\coqwkw{not}} +%HEVEA\newcommand{\lor}{\coqwkw{or}} +%HEVEA\newcommand{\land}{\&} + % own name \newcommand{\coqdoc}{\textsf{coqdoc}} @@ -39,7 +44,7 @@ \newcommand{\coqdockw}[1]{\texttt{#1}} % macro for typesetting variable identifiers -\newcommand{\coqdocid}[1]{\textit{#1}} +\newcommand{\coqdocvar}[1]{\textit{#1}} % macro for typesetting constant identifiers \newcommand{\coqdoccst}[1]{\textsf{#1}} @@ -57,52 +62,93 @@ % macro for typesetting constructor identifiers \newcommand{\coqdocconstr}[1]{\textsf{#1}} +% macro for typesetting tactic identifiers +\newcommand{\coqdoctac}[1]{\texttt{#1}} + + +% Environment encompassing code fragments +% !!! CAUTION: This environment may have empty contents +\newenvironment{coqdoccode}{}{} + % newline and indentation %BEGIN LATEX -\newcommand{\coqdoceol}{\setlength\parskip{0pt}\par} -\newcommand{\coqdocindent}[1]{\noindent\kern#1} -%END LATEX -%HEVEA\newcommand{\coqdoceol}{\begin{rawhtml}
\end{rawhtml}} -%HEVEA\newcommand{\coqdocindent}[1]{\hspace{#1}\hspace{#1}} +% Base indentation length +\newlength{\coqdocbaseindent} +\setlength{\coqdocbaseindent}{0em} + +% Beginning of a line without any Coq indentation +\newcommand{\coqdocnoindent}{\noindent\kern\coqdocbaseindent} +% Beginning of a line with a given Coq indentation +\newcommand{\coqdocindent}[1]{\noindent\kern\coqdocbaseindent\noindent\kern#1} +% End-of-the-line +\newcommand{\coqdoceol}{\hspace*{\fill}\setlength\parskip{0pt}\par} +% Empty lines (in code only) +\newcommand{\coqdocemptyline}{\vskip 0.4em plus 0.1em minus 0.1em} % macro for typesetting the title of a module implementation \newcommand{\coqdocmodule}[1]{\chapter{Module #1}\markboth{Module #1}{} } \usepackage{ifpdf} \ifpdf - \usepackage[pdftex]{hyperref} + \RequirePackage{hyperref} \hypersetup{raiselinks=true,colorlinks=true,linkcolor=black} - \usepackage[all]{hypcap} + + % To do indexing, use something like: + % \usepackage{multind} + % \newcommand{\coqdef}[3]{\hypertarget{coq:#1}{\index{coq}{#1@#2|hyperpage}#3}} \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}}}} + \hypertarget{coq:#1}{\chapter{Library \texorpdfstring{\coqdoccst}{}{#2}}}} \else \newcommand{\coqdef}[3]{#3} \newcommand{\coqref}[2]{#2} - \newcommand{\identref}[2]{\textsf {#2}} + \newcommand{\texorpdfstring}[2]{#1} + \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}}} - +\newif\if@coqdoccolors + \@coqdoccolorsfalse + +\DeclareOption{color}{\@coqdoccolorstrue} +\ProcessOptions + +\if@coqdoccolors +\RequirePackage{xcolor} +\definecolor{varpurple}{rgb}{0.4,0,0.4} +\definecolor{constrmaroon}{rgb}{0.6,0,0} +\definecolor{defgreen}{rgb}{0,0.4,0} +\definecolor{indblue}{rgb}{0,0,0.8} +\definecolor{kwred}{rgb}{0.8,0.1,0.1} + +\def\coqdocvarcolor{varpurple} +\def\coqdockwcolor{kwred} +\def\coqdoccstcolor{defgreen} +\def\coqdocindcolor{indblue} +\def\coqdocconstrcolor{constrmaroon} +\def\coqdocmodcolor{defgreen} +\def\coqdocaxcolor{varpurple} +\def\coqdoctaccolor{black} + +\def\coqdockw#1{{\color{\coqdockwcolor}{\texttt{#1}}}} +\def\coqdocvar#1{{\color{\coqdocvarcolor}{\textit{#1}}}} +\def\coqdoccst#1{{\color{\coqdoccstcolor}{\textrm{#1}}}} +\def\coqdocind#1{{\color{\coqdocindcolor}{\textsf{#1}}}} +\def\coqdocconstr#1{{\color{\coqdocconstrcolor}{\textsf{#1}}}} +\def\coqdocmod#1{{{\color{\coqdocmodcolor}{\textsc{\textsf{#1}}}}}} +\def\coqdocax#1{{{\color{\coqdocaxcolor}{\textsl{\textrm{#1}}}}}} +\def\coqdoctac#1{{\color{\coqdoctaccolor}{\texttt{#1}}}} +\fi \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{\coqvariable}[2]{\coqdocvar{#2}} +\newcommand{\coqvariableref}[2]{\coqref{#1}{\coqdocvar{#2}}} \newcommand{\coqinductive}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}} \newcommand{\coqinductiveref}[2]{\coqref{#1}{\coqdocind{#2}}} @@ -133,8 +179,8 @@ \newcommand{\coqnotationref}[2]{\coqref{#1}{\coqdockw{#2}}} -\newcommand{\coqsection}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}} -\newcommand{\coqsectionref}[2]{\coqref{#1}{\coqdoccst{#2}}} +\newcommand{\coqsection}[2]{\coqdef{sec:#1}{#2}{\coqdoccst{#2}}} +\newcommand{\coqsectionref}[2]{\coqref{sec:#1}{\coqdoccst{#2}}} %\newcommand{\coqlibrary}[2]{\chapter{Library \coqdoccst{#2}}\label{coq:#1}} @@ -145,11 +191,7 @@ \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}} -%HEVEA\newcommand{\land}{\&} +\newcommand{\coqmodule}[2]{\coqdef{mod:#1}{#2}{\coqdocmod{#2}}} +\newcommand{\coqmoduleref}[2]{\coqref{mod:#1}{\coqdocmod{#2}}} +\endinput diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli index 1da8ebd7..56a3cd11 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 11065 2008-06-06 22:39:43Z msozeau $ i*) +(*i $Id: index.mli 11576 2008-11-10 19:13:15Z msozeau $ i*) open Cdglobals @@ -40,6 +40,8 @@ type index_entry = val find : coq_module -> loc -> index_entry +val find_string : coq_module -> string -> index_entry + val add_module : coq_module -> unit type module_kind = Local | Coqlib | Unknown diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll index fc2090dc..f8adb52b 100644 --- a/tools/coqdoc/index.mll +++ b/tools/coqdoc/index.mll @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: index.mll 11065 2008-06-06 22:39:43Z msozeau $ i*) +(*i $Id: index.mll 11790 2009-01-15 20:19:58Z msozeau $ i*) { @@ -47,9 +47,14 @@ let current_type = ref Library let current_library = ref "" (** refers to the file being parsed *) -let table = Hashtbl.create 97 - (** [table] is used to store references and definitions *) +(** [deftable] stores only definitions and is used to interpolate idents + inside comments, which are not globalized otherwise. *) +let deftable = Hashtbl.create 97 + +(** [reftable] stores references and definitions *) +let reftable = Hashtbl.create 97 + let full_ident sp id = if sp <> "<>" then if id <> "<>" then @@ -60,15 +65,24 @@ let full_ident sp id = else "" let add_def loc ty sp id = - Hashtbl.add table (!current_library, loc) (Def (full_ident sp id, ty)) - + Hashtbl.add reftable (!current_library, loc) (Def (full_ident sp id, ty)); + Hashtbl.add deftable id (Ref (!current_library, 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)) + if Hashtbl.mem reftable (m, loc) then () + else Hashtbl.add reftable (m, loc) (Ref (m', full_ident sp id, ty)); + let idx = if id = "<>" then m' else id in + if Hashtbl.mem deftable idx then () + else Hashtbl.add deftable idx (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) - +let add_mod m loc m' id = + Hashtbl.add reftable (m, loc) (Mod (m', id)); + Hashtbl.add deftable m (Mod (m', id)) + +let find m l = Hashtbl.find reftable (m, l) + +let find_string m s = Hashtbl.find deftable s + (*s Manipulating path prefixes *) type stack = string list @@ -216,7 +230,7 @@ let all_entries () = | Def (s,t) -> add_g s m t; add_bt t s m | Ref _ | Mod _ -> () in - Hashtbl.iter classify table; + Hashtbl.iter classify reftable; Hashtbl.iter (fun id m -> add_g id m Library; add_bt Library id m) modules; { idx_name = "global"; idx_entries = sort_entries !gl; @@ -238,7 +252,9 @@ let firstchar = let identchar = ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9'] -let ident = firstchar identchar* +let id = firstchar identchar* +let pfx_id = (id '.')* +let ident = id | pfx_id id let begin_hide = "(*" space* "begin" space+ "hide" space* "*)" let end_hide = "(*" space* "end" space+ "hide" space* "*)" @@ -406,9 +422,9 @@ and module_refs = parse | ident { let id = lexeme lexbuf in (try - add_mod !current_library (lexeme_start lexbuf) (Hashtbl.find modules id) id - with - Not_found -> () + add_mod !current_library (lexeme_start lexbuf) (Hashtbl.find modules id) id + with + Not_found -> () ); module_refs lexbuf } | eof @@ -418,7 +434,7 @@ and module_refs = parse { let type_of_string = function - | "def" | "coe" | "subclass" | "canonstruc" + | "def" | "coe" | "subclass" | "canonstruc" | "fix" | "cofix" | "ex" | "scheme" -> Definition | "prf" | "thm" -> Lemma | "ind" | "coind" -> Inductive diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 81560259..2e97618b 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: main.ml 11236 2008-07-18 15:58:12Z notin $ i*) +(*i $Id: main.ml 11828 2009-01-22 06:44:11Z notin $ i*) (* Modified by Lionel Elie Mamane on 9 & 10 Mar 2004: * - handling of absolute filenames (function coq_module) @@ -30,6 +30,7 @@ let usage () = prerr_endline " --html produce a HTML document (default)"; prerr_endline " --latex produce a LaTeX document"; prerr_endline " --texmacs produce a TeXmacs document"; + prerr_endline " --raw produce a text document"; prerr_endline " --dvi output the DVI"; prerr_endline " --ps output the PostScript"; prerr_endline " --pdf output the Pdf"; @@ -56,12 +57,14 @@ let usage () = prerr_endline " --no-externals no links to Coq standard library"; prerr_endline " --coqlib set URL for Coq standard library"; prerr_endline " (default is http://coq.inria.fr/library/)"; + prerr_endline " --boot run in boot mode"; prerr_endline " --coqlib_path set the path where Coq files are installed"; prerr_endline " -R 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 set HTML charset"; prerr_endline " --inputenc set LaTeX input encoding"; + prerr_endline " --interpolate try to typeset identifiers in comments using definitions in the same module"; prerr_endline ""; exit 1 @@ -81,6 +84,7 @@ let banner () = let target_full_name f = match !Cdglobals.target_language with | HTML -> f ^ ".html" + | Raw -> f ^ ".txt" | _ -> f ^ ".tex" (*s \textbf{Separation of files.} Files given on the command line are @@ -257,6 +261,8 @@ let parse () = Cdglobals.target_language := HTML; parse_rec rem | ("-texmacs" | "--texmacs") :: rem -> Cdglobals.target_language := TeXmacs; parse_rec rem + | ("-raw" | "--raw") :: rem -> + Cdglobals.target_language := Raw; parse_rec rem | ("-charset" | "--charset") :: s :: rem -> Cdglobals.charset := s; parse_rec rem | ("-charset" | "--charset") :: [] -> @@ -267,6 +273,9 @@ let parse () = usage () | ("-raw-comments" | "--raw-comments") :: rem -> Cdglobals.raw_comments := true; parse_rec rem + | ("-interpolate" | "--interpolate") :: rem -> + Cdglobals.interpolate := true; parse_rec rem + | ("-latin1" | "--latin1") :: rem -> Cdglobals.set_latin1 (); parse_rec rem | ("-utf8" | "--utf8") :: rem -> @@ -310,6 +319,8 @@ let parse () = Cdglobals.coqlib := u; parse_rec rem | ("--coqlib" | "-coqlib") :: [] -> usage () + | ("--boot" | "-boot") :: rem -> + Cdglobals.coqlib_path := Coq_config.coqsrc; parse_rec rem | ("--coqlib_path" | "-coqlib_path") :: d :: rem -> Cdglobals.coqlib_path := d; parse_rec rem | ("--coqlib_path" | "-coqlib_path") :: [] -> @@ -318,6 +329,7 @@ let parse () = add_file (what_file f); parse_rec rem in parse_rec (List.tl (Array.to_list Sys.argv)); + Output.initialize (); List.rev !files @@ -414,10 +426,10 @@ let read_glob x = match x with | Vernac_file (f,m) -> let glob = (Filename.chop_extension f) ^ ".glob" in - (try + (try Vernac_file (f, Index.read_glob glob) - with _ -> - eprintf "Warning: file %s cannot be opened; links will not be available\n" glob; + with e -> + eprintf "Warning: file %s cannot be used; links will not be available: %s\n" glob (Printexc.to_string e); x) | Latex_file _ -> x @@ -430,13 +442,13 @@ let produce_document 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 (Sys.file_exists src) then (copy src dst) else eprintf "Warning: file %s does not exist\n" src); (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); + if Sys.file_exists src then copy src dst else eprintf "Warning: file %s does not exist\n" src); (match !Cdglobals.glob_source with | NoGlob -> () | DotGlob -> ignore (List.map read_glob l) diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 93414f22..c146150c 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: output.ml 11154 2008-06-19 18:42:19Z msozeau $ i*) +(*i $Id: output.ml 11823 2009-01-21 15:32:37Z msozeau $ i*) open Cdglobals open Index @@ -32,43 +32,48 @@ let build_table l = let is_keyword = build_table - [ "AddPath"; "Axiom"; "Chapter"; "Check"; "CoFixpoint"; - "CoInductive"; "Defined"; "Definition"; "End"; "Eval"; "Example"; + [ "AddPath"; "Axiom"; "Abort"; "Boxed"; "Chapter"; "Check"; "Coercion"; "CoFixpoint"; + "CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint"; "Hypothesis"; "Hypotheses"; "Resolve"; "Unfold"; "Immediate"; "Extern"; "Implicit"; "Import"; "Inductive"; "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac"; "Module"; "Module Type"; "Declare Module"; "Include"; - "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Qed"; + "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Proof with"; "Qed"; "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; - "Set"; "Unset"; "Variable"; "Variables"; "Context"; + "Set"; "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context"; "Notation"; "Reserved Notation"; "Tactic Notation"; "Delimit"; "Bind"; "Open"; "Scope"; "Boxed"; "Unboxed"; "Inline"; - "Arguments"; "Add"; "Strict"; - "Typeclasses"; "Instance"; "Class"; "Instantiation"; + "Implicit Arguments"; "Add"; "Strict"; + "Typeclasses"; "Instance"; "Global Instance"; "Class"; "Instantiation"; + "subgoal"; (* Program *) "Program Definition"; "Program Example"; "Program Fixpoint"; "Program Lemma"; "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next"; - "Program Instance"; + "Program Instance"; "Equations"; "Equations_nocomp"; (*i (* coq terms *) *) - "match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun"; - "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where" + "forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun"; + "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"; "struct"; "wf"; "measure"; + (* Ltac *) + "before"; "after" ] 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"; + [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection"; + "elimtype"; "progress"; "setoid_rewrite"; + "destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality"; + "f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega"; + "set"; "assert"; "do"; "repeat"; + "cut"; "assumption"; "exact"; "split"; "subst"; "try"; "discriminate"; "simpl"; "unfold"; "red"; "compute"; "at"; "in"; "by"; "reflexivity"; "symmetry"; "transitivity"; "replace"; "setoid_replace"; "inversion"; "inversion_clear"; - "pattern"; "intuition"; "congruence"; + "pattern"; "intuition"; "congruence"; "fail"; "fresh"; "trivial"; "exact"; "tauto"; "firstorder"; "ring"; - "clapply"; "program_simpl"; "eapply"; "auto"; "eauto" ] + "clapply"; "program_simpl"; "program_simplify"; "eapply"; "auto"; "eauto" ] (*s Current Coq module *) @@ -92,27 +97,31 @@ let find_printing_token tok = let remove_printing_token = Hashtbl.remove token_pp (* predefined pretty-prints *) -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}"; - "<-", "\\ensuremath{\\leftarrow}"; - "<->", "\\ensuremath{\\leftrightarrow}"; - "=>", "\\ensuremath{\\Rightarrow}"; - "<=", "\\ensuremath{\\le}"; - ">=", "\\ensuremath{\\ge}"; - "<>", "\\ensuremath{\\not=}"; - "~", "\\ensuremath{\\lnot}"; - "/\\", "\\ensuremath{\\land}"; - "\\/", "\\ensuremath{\\lor}"; - "|-", "\\ensuremath{\\vdash}"; - "forall", "\\ensuremath{\\forall}"; - "exists", "\\ensuremath{\\exists}"; - (* "fun", "\\ensuremath{\\lambda}" ? *) - ] +let initialize () = + let if_utf8 = if !Cdglobals.utf8 then fun x -> Some x else fun _ -> None in + List.iter + (fun (s,l,l') -> Hashtbl.add token_pp s (Some l, l')) + [ "*" , "\\ensuremath{\\times}", if_utf8 "×"; + "|", "\\ensuremath{|}", None; + "->", "\\ensuremath{\\rightarrow}", if_utf8 "→"; + "->~", "\\ensuremath{\\rightarrow\\lnot}", None; + "->~~", "\\ensuremath{\\rightarrow\\lnot\\lnot}", None; + "<-", "\\ensuremath{\\leftarrow}", None; + "<->", "\\ensuremath{\\leftrightarrow}", if_utf8 "↔"; + "=>", "\\ensuremath{\\Rightarrow}", if_utf8 "⇒"; + "<=", "\\ensuremath{\\le}", if_utf8 "≤"; + ">=", "\\ensuremath{\\ge}", if_utf8 "≥"; + "<>", "\\ensuremath{\\not=}", if_utf8 "≠"; + "~", "\\ensuremath{\\lnot}", if_utf8 "¬"; + "/\\", "\\ensuremath{\\land}", if_utf8 "∧"; + "\\/", "\\ensuremath{\\lor}", if_utf8 "∨"; + "|-", "\\ensuremath{\\vdash}", None; + "forall", "\\ensuremath{\\forall}", if_utf8 "∀"; + "exists", "\\ensuremath{\\exists}", if_utf8 "∃"; + "Π", "\\ensuremath{\\Pi}", if_utf8 "Π"; + "λ", "\\ensuremath{\\lambda}", if_utf8 "λ" + (* "fun", "\\ensuremath{\\lambda}" ? *) + ] (*s Table of contents *) @@ -130,6 +139,9 @@ let new_label = let r = ref 0 in fun () -> incr r; "lab" ^ string_of_int !r module Latex = struct + let in_title = ref false + let in_doc = ref false + (*s Latex preamble *) let (preamble : string Queue.t) = Queue.create () @@ -208,7 +220,7 @@ module Latex = struct let indentation n = if n == 0 then - printf "\\noindent\n" + printf "\\coqdocnoindent\n" else let space = 0.5 *. (float n) in printf "\\coqdocindent{%2.2fem}\n" space @@ -243,35 +255,49 @@ module Latex = struct 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 + printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}" let defref m id ty s = printf "\\coq%s{" (type_name ty); label_ident (m ^ "." ^ id); printf "}{"; raw_ident s; printf "}" + let reference s = function + | 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 "\\coqdocvar{"; raw_ident s; printf "}" + let ident s loc = if is_keyword s then begin printf "\\coqdockw{"; raw_ident s; printf "}" end else begin 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 "}") + reference s (Index.find !current_module loc) 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 else begin + if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) + then + try reference s (Index.find_string !current_module s) + with _ -> (printf "\\coqdocvar{"; raw_ident s; printf "}") + else (printf "\\coqdocvar{"; raw_ident s; printf "}") + end end end - let ident s l = with_latex_printing (fun s -> ident s l) s - + let ident s l = + if !in_title then ( + printf "\\texorpdfstring{"; + with_latex_printing (fun s -> ident s l) s; + printf "}{"; raw_ident s; printf "}") + else + with_latex_printing (fun s -> ident s l) s + let symbol = with_latex_printing raw_ident let rec reach_item_level n = @@ -290,13 +316,13 @@ module Latex = struct let stop_item () = reach_item_level 0 - let start_doc () = printf "\n\n\n\\noindent\n" + let start_doc () = in_doc := true - let end_doc () = stop_item (); printf "\n\n\n" + let end_doc () = in_doc := false; stop_item () - let start_coq () = () + let start_coq () = printf "\\begin{coqdoccode}\n" - let end_coq () = () + let end_coq () = printf "\\end{coqdoccode}\n" let start_code () = end_doc (); start_coq () @@ -312,17 +338,17 @@ module Latex = struct let section lev f = stop_item (); output_string (section_kind lev); - f (); + in_title := true; f (); in_title := false; printf "}\n\n" let rule () = printf "\\par\n\\noindent\\hrulefill\\par\n\\noindent{}" - let paragraph () = stop_item (); printf "\n\n\\medskip\n" + let paragraph () = stop_item (); printf "\n\n" let line_break () = printf "\\coqdoceol\n" - let empty_line_of_code () = printf "\n\n\\medskip\n" + let empty_line_of_code () = printf "\\coqdocemptyline\n" let start_inline_coq () = () @@ -394,7 +420,8 @@ module Html = struct let line_break () = printf "
\n" - let empty_line_of_code () = printf "\n
\n" + let empty_line_of_code () = + printf "\n
\n" let char = function | '<' -> printf "<" @@ -417,49 +444,54 @@ module Html = struct let stop_verbatim () = printf "\n" let module_ref m s = - printf "" m; raw_ident s; printf "" - (*i - match find_module m with - | Local -> - printf "" m; raw_ident s; printf "" - | Coqlib when !externals -> - let m = Filename.concat !coqlib m in - printf "" m; raw_ident s; printf "" - | Coqlib | Unknown -> - raw_ident s - i*) - - let ident_ref m fid s = match find_module m with | Local -> - printf "" m fid; raw_ident s; printf "" + printf "" m; raw_ident s; printf "" | Coqlib when !externals -> let m = Filename.concat !coqlib m in - printf "" m fid; raw_ident s; printf "" + printf "" m; raw_ident s; printf "" | Coqlib | Unknown -> raw_ident s + let ident_ref m fid typ s = + match find_module m with + | Local -> + printf "" typ; + printf "" m fid; raw_ident s; + printf "" + | Coqlib when !externals -> + let m = Filename.concat !coqlib m in + printf "" typ; + printf "" m fid; + raw_ident s; printf "" + | Coqlib | Unknown -> + printf "" typ; raw_ident s; printf "" + let ident s loc = if is_keyword s then begin - printf ""; + printf ""; raw_ident s; printf "" end else begin try (match Index.find !current_module loc with - | Def (fullid,_) -> - printf "" fullid; raw_ident s + | Def (fullid,ty) -> + printf "" (type_name ty); + printf "" fullid; raw_ident s; printf "" | Mod (m,s') when s = s' -> module_ref m s | Ref (m,fullid,ty) -> - ident_ref m fullid s + ident_ref m fullid (type_name ty) s | Mod _ -> - raw_ident s) + printf ""; raw_ident s ; printf "") with Not_found -> - raw_ident s + if is_tactic s then + (printf ""; raw_ident s; printf "") + else + (printf ""; raw_ident s ; printf "") end - + let with_html_printing f tok = try (match Hashtbl.find token_pp tok with @@ -488,9 +520,9 @@ module Html = struct let stop_item () = reach_item_level 0 - let start_coq () = if not !raw_comments then printf "\n" + let start_coq () = if not !raw_comments then printf "
\n" - let end_coq () = if not !raw_comments then printf "\n" + let end_coq () = if not !raw_comments then printf "
\n" let start_doc () = if not !raw_comments then @@ -504,9 +536,9 @@ module Html = struct let end_code () = end_coq (); start_doc () - let start_inline_coq () = printf "" + let start_inline_coq () = printf "" - let end_inline_coq () = printf "" + let end_inline_coq () = printf "" let paragraph () = stop_item (); printf "\n

\n" @@ -539,7 +571,7 @@ module Html = struct let all_letters i = List.iter (letter_index false i.idx_name) i.idx_entries (* Construction d'une liste des index (1 index global, puis 1 - index par catégorie) *) + index par catégorie) *) let format_global_index = Index.map (fun s (m,t) -> @@ -578,7 +610,7 @@ module Html = struct printf "\n" let make_one_multi_index prt_tbl i = - (* Attn: make_one_multi_index créé un nouveau fichier... *) + (* Attn: make_one_multi_index créé un nouveau fichier... *) let idx = i.idx_name in let one_letter ((c,l) as cl) = open_out_file (sprintf "index_%s_%c.html" idx c); @@ -776,68 +808,155 @@ module TeXmacs = struct end + +(*s LaTeX output *) + +module Raw = struct + + let header () = () + + let trailer () = () + + let char = output_char + + let label_char c = match c with + | '\\' | '$' | '#' | '%' | '&' | '{' | '}' | '_' + | '^' | '~' -> () + | _ -> + output_char c + + let latex_char = output_char + let latex_string = output_string + + let html_char _ = () + let html_string _ = () + + let raw_ident s = + for i = 0 to String.length s - 1 do char s.[i] done + + let start_module () = () + let end_module () = () + + let start_latex_math () = () + let stop_latex_math () = () + + let start_verbatim () = () + + let stop_verbatim () = () + + let indentation n = + for i = 1 to n do printf " " done + + let ident s loc = raw_ident s + + let symbol = raw_ident + + let item n = printf "- " + + let stop_item () = () + + let start_doc () = printf "(** " + let end_doc () = printf " *)\n" + + let start_coq () = () + let end_coq () = () + + let start_code () = end_doc (); start_coq () + let end_code () = end_coq (); start_doc () + + let section_kind = + function + | 1 -> "*" + | 2 -> "**" + | 3 -> "***" + | 4 -> "****" + | _ -> assert false + + let section lev f = + output_string (section_kind lev); + f () + + let rule () = () + + let paragraph () = printf "\n\n" + + let line_break () = printf "\n" + + let empty_line_of_code () = printf "\n" + + let start_inline_coq () = () + let end_inline_coq () = () + + let make_multi_index () = () + let make_index () = () + let make_toc () = () + +end + + + (*s Generic output *) -let select f1 f2 f3 x = - match !target_language with LaTeX -> f1 x | HTML -> f2 x | TeXmacs -> f3 x +let select f1 f2 f3 f4 x = + match !target_language with LaTeX -> f1 x | HTML -> f2 x | TeXmacs -> f3 x | Raw -> f4 x let push_in_preamble = Latex.push_in_preamble -let header = select Latex.header Html.header TeXmacs.header -let trailer = select Latex.trailer Html.trailer TeXmacs.trailer +let header = select Latex.header Html.header TeXmacs.header Raw.header +let trailer = select Latex.trailer Html.trailer TeXmacs.trailer Raw.trailer let start_module = - select Latex.start_module Html.start_module TeXmacs.start_module + select Latex.start_module Html.start_module TeXmacs.start_module Raw.start_module -let start_doc = select Latex.start_doc Html.start_doc TeXmacs.start_doc -let end_doc = select Latex.end_doc Html.end_doc TeXmacs.end_doc +let start_doc = select Latex.start_doc Html.start_doc TeXmacs.start_doc Raw.start_doc +let end_doc = select Latex.end_doc Html.end_doc TeXmacs.end_doc Raw.end_doc -let start_coq = select Latex.start_coq Html.start_coq TeXmacs.start_coq -let end_coq = select Latex.end_coq Html.end_coq TeXmacs.end_coq +let start_coq = select Latex.start_coq Html.start_coq TeXmacs.start_coq Raw.start_coq +let end_coq = select Latex.end_coq Html.end_coq TeXmacs.end_coq Raw.end_coq -let start_code = select Latex.start_code Html.start_code TeXmacs.start_code -let end_code = select Latex.end_code Html.end_code TeXmacs.end_code +let start_code = select Latex.start_code Html.start_code TeXmacs.start_code Raw.start_code +let end_code = select Latex.end_code Html.end_code TeXmacs.end_code Raw.end_code let start_inline_coq = - select Latex.start_inline_coq Html.start_inline_coq TeXmacs.start_inline_coq + select Latex.start_inline_coq Html.start_inline_coq TeXmacs.start_inline_coq Raw.start_inline_coq let end_inline_coq = - select Latex.end_inline_coq Html.end_inline_coq TeXmacs.end_inline_coq + select Latex.end_inline_coq Html.end_inline_coq TeXmacs.end_inline_coq Raw.end_inline_coq -let indentation = select Latex.indentation Html.indentation TeXmacs.indentation -let paragraph = select Latex.paragraph Html.paragraph TeXmacs.paragraph -let line_break = select Latex.line_break Html.line_break TeXmacs.line_break +let indentation = select Latex.indentation Html.indentation TeXmacs.indentation Raw.indentation +let paragraph = select Latex.paragraph Html.paragraph TeXmacs.paragraph Raw.paragraph +let line_break = select Latex.line_break Html.line_break TeXmacs.line_break Raw.line_break let empty_line_of_code = select - Latex.empty_line_of_code Html.empty_line_of_code TeXmacs.empty_line_of_code + Latex.empty_line_of_code Html.empty_line_of_code TeXmacs.empty_line_of_code Raw.empty_line_of_code -let section = select Latex.section Html.section TeXmacs.section -let item = select Latex.item Html.item TeXmacs.item -let stop_item = select Latex.stop_item Html.stop_item TeXmacs.stop_item -let rule = select Latex.rule Html.rule TeXmacs.rule +let section = select Latex.section Html.section TeXmacs.section Raw.section +let item = select Latex.item Html.item TeXmacs.item Raw.item +let stop_item = select Latex.stop_item Html.stop_item TeXmacs.stop_item Raw.stop_item +let rule = select Latex.rule Html.rule TeXmacs.rule Raw.rule -let char = select Latex.char Html.char TeXmacs.char -let ident = select Latex.ident Html.ident TeXmacs.ident -let symbol = select Latex.symbol Html.symbol TeXmacs.symbol +let char = select Latex.char Html.char TeXmacs.char Raw.char +let ident = select Latex.ident Html.ident TeXmacs.ident Raw.ident +let symbol = select Latex.symbol Html.symbol TeXmacs.symbol Raw.symbol -let latex_char = select Latex.latex_char Html.latex_char TeXmacs.latex_char +let latex_char = select Latex.latex_char Html.latex_char TeXmacs.latex_char Raw.latex_char let latex_string = - select Latex.latex_string Html.latex_string TeXmacs.latex_string -let html_char = select Latex.html_char Html.html_char TeXmacs.html_char + select Latex.latex_string Html.latex_string TeXmacs.latex_string Raw.latex_string +let html_char = select Latex.html_char Html.html_char TeXmacs.html_char Raw.html_char let html_string = - select Latex.html_string Html.html_string TeXmacs.html_string + select Latex.html_string Html.html_string TeXmacs.html_string Raw.html_string let start_latex_math = - select Latex.start_latex_math Html.start_latex_math TeXmacs.start_latex_math + select Latex.start_latex_math Html.start_latex_math TeXmacs.start_latex_math Raw.start_latex_math let stop_latex_math = - select Latex.stop_latex_math Html.stop_latex_math TeXmacs.stop_latex_math + select Latex.stop_latex_math Html.stop_latex_math TeXmacs.stop_latex_math Raw.stop_latex_math let start_verbatim = - select Latex.start_verbatim Html.start_verbatim TeXmacs.start_verbatim + select Latex.start_verbatim Html.start_verbatim TeXmacs.start_verbatim Raw.start_verbatim let stop_verbatim = - select Latex.stop_verbatim Html.stop_verbatim TeXmacs.stop_verbatim + select Latex.stop_verbatim Html.stop_verbatim TeXmacs.stop_verbatim Raw.stop_verbatim let verbatim_char = - select output_char Html.char TeXmacs.char + select output_char Html.char TeXmacs.char Raw.char let hard_verbatim_char = output_char -let make_multi_index = select Latex.make_multi_index Html.make_multi_index TeXmacs.make_multi_index -let make_index = select Latex.make_index Html.make_index TeXmacs.make_index -let make_toc = select Latex.make_toc Html.make_toc TeXmacs.make_toc +let make_multi_index = select Latex.make_multi_index Html.make_multi_index TeXmacs.make_multi_index Raw.make_multi_index +let make_index = select Latex.make_index Html.make_index TeXmacs.make_index Raw.make_index +let make_toc = select Latex.make_toc Html.make_toc TeXmacs.make_toc Raw.make_toc diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli index 87b311f3..3da80335 100644 --- a/tools/coqdoc/output.mli +++ b/tools/coqdoc/output.mli @@ -6,11 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: output.mli 8669 2006-03-28 17:34:15Z notin $ i*) +(*i $Id: output.mli 11576 2008-11-10 19:13:15Z msozeau $ i*) open Cdglobals open Index +val initialize : unit -> unit + val add_printing_token : string -> string option * string option -> unit val remove_printing_token : string -> unit diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll index baace5ba..3ae5cbed 100644 --- a/tools/coqdoc/pretty.mll +++ b/tools/coqdoc/pretty.mll @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pretty.mll 11255 2008-07-24 16:57:13Z notin $ i*) +(*i $Id: pretty.mll 11823 2009-01-21 15:32:37Z msozeau $ i*) (*s Utility functions for the scanners *) @@ -57,6 +57,7 @@ let formatted = ref false let brackets = ref 0 let comment_level = ref 0 + let in_proof = ref false let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos @@ -173,11 +174,12 @@ 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 *) - '\206' ['\177'-'\183'] | + '\206' ('\160' | [ '\177'-'\183'] | '\187') | '\226' ('\130' [ '\128'-'\137' ] (* subscripts *) | '\129' [ '\176'-'\187' ] (* superscripts *) | '\132' ['\128'-'\191'] | '\133' ['\128'-'\143']) @@ -188,17 +190,24 @@ let pfx_id = (id '.')* let identifier = id | pfx_id id -let symbolchar_no_brackets = - ['!' '$' '%' '&' '*' '+' ',' '@' '^' '#' - '\\' '/' '-' '<' '>' '|' ':' '?' '=' '~' - '{' '}' '(' ')'] | +let symbolchar_symbol_no_brackets = + ['!' '$' '%' '&' '*' '+' ',' '^' '#' + '\\' '/' '-' '<' '>' '|' ':' '?' '=' '~' ] | (* utf-8 symbols *) '\226' ['\134'-'\143' '\152'-'\155' '\164'-'\165' '\168'-'\171'] _ +let symbolchar_no_brackets = symbolchar_symbol_no_brackets | + [ '@' '{' '}' '(' ')' 'A'-'Z' 'a'-'z' '_'] let symbolchar = symbolchar_no_brackets | '[' | ']' -let token_no_brackets = symbolchar_no_brackets+ -let token = symbolchar+ | '[' [^ '[' ']' ':']* ']' +let token_no_brackets = symbolchar_symbol_no_brackets symbolchar_no_brackets* +let token = symbolchar_symbol_no_brackets symbolchar* | '[' [^ '[' ']' ':']* ']' let printing_token = (token | id)+ +(* tokens with balanced brackets *) +let token_brackets = + ( token_no_brackets ('[' token_no_brackets? ']')* + | token_no_brackets? ('[' token_no_brackets? ']')+ ) + token_no_brackets? + let thm_token = "Theorem" | "Lemma" @@ -208,22 +217,26 @@ let thm_token = | "Proposition" | "Property" | "Goal" + | "Next" space+ "Obligation" let def_token = "Definition" | "Let" | "Class" - | "SubClass" + | "SubClass" | "Example" | "Local" | "Fixpoint" + | "Boxed" | "CoFixpoint" | "Record" | "Structure" - | "Instance" | "Scheme" | "Inductive" | "CoInductive" + | "Equations" + | "Instance" + | "Global" space+ "Instance" let decl_token = "Hypothesis" @@ -277,6 +290,8 @@ let commands = | ("Hypothesis" | "Hypotheses") | "End" +let end_kw = "Proof" | "Qed" | "Defined" | "Save" | "Admitted" | "Abort" + let extraction = "Extraction" | "Recursive" space+ "Extraction" @@ -291,7 +306,8 @@ let prog_kw = | "Solve" let gallina_kw_to_hide = - "Implicit" + "Implicit" space+ "Arguments" + | "Next" "Obligation" | "Ltac" | "Require" | "Import" @@ -308,12 +324,6 @@ let gallina_kw_to_hide = | "Declare" space+ ("Left" | "Right") space+ "Step" -(* tokens with balanced brackets *) -let token_brackets = - ( symbolchar_no_brackets+ ('[' symbolchar_no_brackets* ']')* - | symbolchar_no_brackets* ('[' symbolchar_no_brackets* ']')+ ) - symbolchar_no_brackets* - let section = "*" | "**" | "***" | "****" let item_space = " " @@ -333,7 +343,7 @@ let end_verb = "(*" space* "end" space+ "verb" space* "*)" rule coq_bol = parse | space* nl+ - { Output.empty_line_of_code (); coq_bol lexbuf } + { if not (!in_proof && !Cdglobals.gallina) then Output.empty_line_of_code (); coq_bol lexbuf } | space* "(**" space_nl { Output.end_coq (); Output.start_doc (); let eol = doc_bol lexbuf in @@ -352,7 +362,7 @@ rule coq_bol = parse { let s = lexeme lexbuf in 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 + if eol then (coq_bol lexbuf) else coq lexbuf else begin let nbsp,isp = count_spaces s in @@ -362,8 +372,35 @@ rule coq_bol = parse let eol = body lexbuf in if eol then coq_bol lexbuf else coq lexbuf end } - | space* gallina_kw + | space* thm_token { let s = lexeme lexbuf in + 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 + in_proof := true; + if eol then coq_bol lexbuf else coq lexbuf } + | space* "Proof" (space* "." | space+ "with") + { in_proof := true; + let eol = + if not !Cdglobals.gallina then + begin backtrack lexbuf; body_bol lexbuf end + else true + in if eol then coq_bol lexbuf else coq lexbuf } + | space* end_kw { + let eol = + if not (!in_proof && !Cdglobals.gallina) then + begin backtrack lexbuf; body_bol lexbuf end + else + skip_to_dot lexbuf + in + in_proof := false; + if eol then coq_bol lexbuf else coq lexbuf } + | space* gallina_kw + { + in_proof := false; + let s = lexeme lexbuf in let nbsp,isp = count_spaces s in let s = String.sub s isp (String.length s - isp) in Output.indentation nbsp; @@ -371,7 +408,9 @@ rule coq_bol = parse let eol= body lexbuf in if eol then coq_bol lexbuf else coq lexbuf } | space* prog_kw - { let s = lexeme lexbuf in + { + in_proof := false; + 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 @@ -409,7 +448,7 @@ rule coq_bol = parse | _ { let eol = if not !Cdglobals.gallina then - begin backtrack lexbuf; Output.indentation 0; body_bol lexbuf end + begin backtrack lexbuf; body_bol lexbuf end else skip_to_dot lexbuf in @@ -419,7 +458,7 @@ rule coq_bol = parse and coq = parse | nl - { Output.line_break(); coq_bol lexbuf } + { if not (!in_proof && !Cdglobals.gallina) then Output.line_break(); coq_bol lexbuf } | "(**" space_nl { Output.end_coq (); Output.start_doc (); let eol = doc_bol lexbuf in @@ -448,6 +487,15 @@ and coq = parse let eol=body lexbuf in if eol then coq_bol lexbuf else coq lexbuf end } + | end_kw { + let eol = + if not (!in_proof && !Cdglobals.gallina) then + begin backtrack lexbuf; body lexbuf end + else + skip_to_dot lexbuf + in + in_proof := false; + if eol then coq_bol lexbuf else coq lexbuf } | gallina_kw { let s = lexeme lexbuf in Output.ident s (lexeme_start lexbuf); @@ -463,7 +511,7 @@ and coq = parse { () } | _ { let eol = if not !Cdglobals.gallina then - begin backtrack lexbuf; Output.indentation 0; body lexbuf end + begin backtrack lexbuf; body lexbuf end else let eol = skip_to_dot lexbuf in if eol then Output.line_break (); eol @@ -496,16 +544,15 @@ and doc_bol = parse and doc = parse | nl { Output.char '\n'; doc_bol lexbuf } - | "[" - { brackets := 1; - Output.start_inline_coq (); escaped_coq lexbuf; Output.end_inline_coq (); - doc lexbuf } - | "[[" nl space* + | "[[" nl { formatted := true; Output.line_break (); Output.start_inline_coq (); - Output.indentation (fst (count_spaces (lexeme lexbuf))); let eol = body_bol lexbuf in Output.end_inline_coq (); formatted := false; if eol then doc_bol lexbuf else doc lexbuf} + | "[" + { brackets := 1; + Output.start_inline_coq (); escaped_coq lexbuf; Output.end_inline_coq (); + doc lexbuf } | '*'* "*)" space* nl { true } | '*'* "*)" @@ -612,7 +659,7 @@ and skip_to_dot = parse and body_bol = parse | space+ { Output.indentation (fst (count_spaces (lexeme lexbuf))); body lexbuf } - | _ { backtrack lexbuf; body lexbuf } + | _ { backtrack lexbuf; Output.indentation 0; body lexbuf } and body = parse | nl {Output.line_break(); body_bol lexbuf} @@ -645,7 +692,7 @@ and notation_bol = parse and notation = parse | nl { Output.line_break(); notation_bol lexbuf } - | '"' { Output.char '"'; false } + | '"' { Output.char '"'} | token { let s = lexeme lexbuf in Output.symbol s; notation lexbuf } @@ -660,7 +707,7 @@ and skip_hide = parse (*s Reading token pretty-print *) and printing_token_body = parse - | "*)" | eof + | "*)" nl? | eof { let s = Buffer.contents token_buffer in Buffer.clear token_buffer; s } -- cgit v1.2.3