From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- tools/check-v8 | 24 --- tools/coq-tex.ml4 | 2 +- tools/coq_makefile.ml4 | 27 +-- tools/coqdep.ml | 3 +- tools/coqdep_lexer.mll | 2 +- tools/coqdoc/alpha.ml | 2 +- tools/coqdoc/alpha.mli | 2 +- tools/coqdoc/cdglobals.ml | 72 ++++++++ tools/coqdoc/coqdoc.css | 59 +++++++ tools/coqdoc/coqdoc.sty | 5 +- tools/coqdoc/index.mli | 4 +- tools/coqdoc/index.mll | 4 +- tools/coqdoc/main.ml | 197 +++++++++++++++------- tools/coqdoc/output.ml | 212 +++++++++-------------- tools/coqdoc/output.mli | 31 +--- tools/coqdoc/pretty.mli | 10 +- tools/coqdoc/pretty.mll | 371 ++++++++++++++++++++++------------------- tools/coqwc.mll | 4 +- tools/gallina.ml | 2 +- tools/gallina_lexer.mll | 2 +- tools/restore-v7 | 9 - tools/translate-v8 | 41 ----- tools/translate_V6-3-1_to_V7-0 | 27 --- tools/upgrade-v8 | 22 --- 24 files changed, 582 insertions(+), 552 deletions(-) delete mode 100755 tools/check-v8 mode change 100755 => 100644 tools/coqdep.ml create mode 100644 tools/coqdoc/cdglobals.ml create mode 100644 tools/coqdoc/coqdoc.css delete mode 100755 tools/restore-v7 delete mode 100755 tools/translate-v8 delete mode 100755 tools/translate_V6-3-1_to_V7-0 delete mode 100755 tools/upgrade-v8 (limited to 'tools') diff --git a/tools/check-v8 b/tools/check-v8 deleted file mode 100755 index 9dfa0be3..00000000 --- a/tools/check-v8 +++ /dev/null @@ -1,24 +0,0 @@ -#!/bin/sh - -echo ------------------ Producing v8 files ------------------------- -if [ -e v8 ]; then rm -r v8; fi -if [ -e /tmp/v8.$$ ]; then rm -r /tmp/v8.$$; fi -cp -pr . /tmp/v8.$$ -mv /tmp/v8.$$ v8 -cd v8 -rm description -make clean -make COQFLAGS='-translate -q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)' || \ - { echo ---- Failed to translate; exit 1; } -echo ------------------ Upgrading v8 files ------------------------- -v8files=`find . -name \*.v8` -for i in $v8files; do - j=`dirname $i`/`basename $i .v8`.v - echo Upgrading $i - mv -u -f $i $j -done -echo ------------------ Recompiling v8 files ----------------------- -make clean -make || { echo ---- Failed to recompile; exit 1; } -make clean # to save disk space -echo ------------------ Translation completed ---------------------- diff --git a/tools/coq-tex.ml4 b/tools/coq-tex.ml4 index 6987d78b..7565c22e 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,v 1.5.2.1 2004/07/16 19:31:45 herbelin Exp $ *) +(* $Id: coq-tex.ml4 5920 2004-07-16 20:01:26Z herbelin $ *) (* coq-tex * JCF, 16/1/98 diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index 02607f14..cc3e9515 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,v 1.16.2.4 2005/01/12 16:00:19 sacerdot Exp $ *) +(* $Id: coq_makefile.ml4 7994 2006-02-06 08:48:37Z herbelin $ *) (* créer un Makefile pour un développement Coq automatiquement *) @@ -79,9 +79,9 @@ coq_makefile [subdirectory] .... [file.v] ... [file.ml] ... [-custom [--help]: equivalent to [-h]\n"; exit 1 -let standard sds = +let standard sds sps = print "byte:\n"; - print "\t$(MAKE) all \"OPT=-byte\"\n\n"; + print "\t$(MAKE) all \"OPT=\"\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"; @@ -117,6 +117,9 @@ let standard sds = 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"; + List.iter + (fun (file,_,_) -> print "\t- rm -f "; print file; print "\n") + sps; List.iter (fun x -> print "\t(cd "; print x; print " ; $(MAKE) clean)\n") sds; @@ -224,17 +227,16 @@ let include_dirs l = print "OCAMLLIBS="; print_list "\\\n " i_ocaml; print "\n"; print "COQLIBS="; print_list "\\\n " i_coq; print "\n\n" -let special l = +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 - let rec sp_aux = function - | [] -> [] - | Special (file,deps,com) :: r -> (file,deps,com) :: (sp_aux r) - | _ :: r -> sp_aux r - in - let sps = sp_aux l in if sps <> [] then section "Custom targets."; List.iter pr_sp sps @@ -434,10 +436,11 @@ let do_makefile args = variables l; include_dirs l; all_target l; - special l; + let sps = special l in + custom sps; let sds = subdirs l in implicit (); - standard sds; + standard sds sps; (* TEST directories_deps l; *) warning (); if not (!output_channel == stdout) then close_out !output_channel; diff --git a/tools/coqdep.ml b/tools/coqdep.ml old mode 100755 new mode 100644 index ab7cef92..eb740712 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqdep.ml,v 1.15.2.1 2004/07/16 19:31:46 herbelin Exp $ *) +(* $Id: coqdep.ml 8642 2006-03-17 10:09:02Z notin $ *) open Printf open Coqdep_lexer @@ -523,6 +523,7 @@ let coqdep () = 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; diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll index 4f5f172f..f7f37086 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,v 1.6.6.1 2004/07/16 19:31:46 herbelin Exp $ i*) +(*i $Id: coqdep_lexer.mll 5920 2004-07-16 20:01:26Z herbelin $ i*) { diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml index 2418b6e1..b1a46bae 100644 --- a/tools/coqdoc/alpha.ml +++ b/tools/coqdoc/alpha.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: alpha.ml,v 1.1.2.1 2004/07/16 19:31:46 herbelin Exp $ i*) +(*i $Id: alpha.ml 5920 2004-07-16 20:01:26Z herbelin $ i*) let norm_char c = match Char.uppercase c with | '\192'..'\198' -> 'A' diff --git a/tools/coqdoc/alpha.mli b/tools/coqdoc/alpha.mli index 46409c9a..d3c26537 100644 --- a/tools/coqdoc/alpha.mli +++ b/tools/coqdoc/alpha.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: alpha.mli,v 1.1.2.1 2004/07/16 19:31:46 herbelin Exp $ i*) +(*i $Id: alpha.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) (* Alphabetic order. *) diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml new file mode 100644 index 00000000..b5a4cb22 --- /dev/null +++ b/tools/coqdoc/cdglobals.ml @@ -0,0 +1,72 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* "" 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 light = ref false +let gallina = ref false +let short = ref false +let index = ref true +let multi_index = ref false +let toc = ref false +let page_title = ref "" +let title = ref "" +let externals = ref true +let coqlib = ref "http://coq.inria.fr/library/" +let raw_comments = ref false + +let charset = ref "iso-8859-1" +let inputenc = ref "" +let latin1 = ref false +let utf8 = ref false + +let set_latin1 () = + charset := "iso-8859-1"; + inputenc := "latin1"; + latin1 := true + +let set_utf8 () = + charset := "utf-8"; + inputenc := "utf8"; + utf8 := true + +(* Parsing options *) + +type coq_module = string + +type file = + | Vernac_file of string * coq_module + | Latex_file of string + + diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css new file mode 100644 index 00000000..b59438e5 --- /dev/null +++ b/tools/coqdoc/coqdoc.css @@ -0,0 +1,59 @@ +body { padding: 0px 0px; + margin: 0px 0px; + background-color: white } + +#page { display: block; + padding: 0px; + margin: 0px; + padding-bottom: 10px; } + +#header { display: block; + position: relative; + padding: 0; + margin: 0; + vertical-align: middle; + border-bottom-style: solid; + border-width: thin } + +#header h1 { padding: 0; + margin: 0;} + + +/* Contenu */ + +#main{ display: block; + padding: 10px; + overflow: hidden; + font-size: 10pt } + +#main a.idref:visited {color : #416DFF; text-decoration : none; } +#main a.idref:link {color : #416DFF; text-decoration : none; } +#main a.idref:hover {color : Red; text-decoration : underline; } +#main a.idref:active {color : Red; text-decoration : underline; } + +#main .keyword { font-weight : bold; + color : Red } + +#main .section { font-size : 20pt } + +#main code { font-family: monospace; + font-size: 8pt; + line-height: 50% } + +#main .doc { margin: 0px; + padding: 10px; + font-family: sans-serif; + font-size: 11pt; + font-weight:bold; + background-color:#66ff66 } + +#main .doc code { font-family: monospace; + font-size: 10pt} + +/* Pied de page */ + +#footer { font-size: 8pt; + font-family: sans-serif; } + +#footer a:visited { color: blue; } + diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty index 68b9ab26..597152f5 100644 --- a/tools/coqdoc/coqdoc.sty +++ b/tools/coqdoc/coqdoc.sty @@ -9,13 +9,13 @@ \ProvidesPackage{coqdoc}[2002/02/11] % 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} @@ -50,7 +50,8 @@ %HEVEA\newcommand{\coqdocindent}[1]{\hspace{#1}\hspace{#1}} % macro for typesetting the title of a module implementation -\newcommand{\coqdocmodule}[1]{\section*{Module #1}\markboth{Module #1}{}} +\newcommand{\coqdocmodule}[1]{\section*{Module #1}\markboth{Module #1}{} +} %HEVEA\newcommand{\lnot}{\coqwkw{not}} %HEVEA\newcommand{\lor}{\coqwkw{or}} diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli index 60c21387..4b53d6ff 100644 --- a/tools/coqdoc/index.mli +++ b/tools/coqdoc/index.mli @@ -6,9 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: index.mli,v 1.1.2.1 2004/07/16 19:31:46 herbelin Exp $ i*) +(*i $Id: index.mli 8617 2006-03-08 10:47:12Z notin $ i*) -type coq_module = string +open Cdglobals type loc = int diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll index 875a2337..ec89da2f 100644 --- a/tools/coqdoc/index.mll +++ b/tools/coqdoc/index.mll @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: index.mll,v 1.2.2.2 2004/08/03 17:31:04 herbelin Exp $ i*) +(*i $Id: index.mll 8617 2006-03-08 10:47:12Z notin $ i*) { @@ -14,7 +14,7 @@ open Filename open Lexing open Printf -type coq_module = string +open Cdglobals type loc = int diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 66d2a993..177fc2bc 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: main.ml,v 1.4.2.1 2004/07/16 19:31:47 herbelin Exp $ i*) +(*i $Id: main.ml 8669 2006-03-28 17:34:15Z notin $ i*) (* Modified by Lionel Elie Mamane on 9 & 10 Mar 2004: * - handling of absolute filenames (function coq_module) @@ -18,6 +18,7 @@ * It may be removed or abbreviated as far as I am concerned. *) +open Cdglobals open Filename open Printf open Output @@ -33,6 +34,7 @@ let usage () = 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 write output in file "; prerr_endline " -d output files into directory "; prerr_endline " -g (gallina) skip proofs"; @@ -58,8 +60,6 @@ let usage () = prerr_endline " --charset set HTML charset"; prerr_endline " --inputenc set LaTeX input encoding"; prerr_endline ""; - prerr_endline - "On-line documentation at http://www.lri.fr/~filliatr/coqdoc/\n"; exit 1 (*s \textbf{Banner.} Always printed. Notice that it is printed on error @@ -71,7 +71,11 @@ let banner () = eprintf "This is coqdoc version %s, compiled on %s\n" Coq_config.version Coq_config.compile_date; flush stderr - + +let target_full_name f = + match !target_language with + | HTML -> f ^ ".html" + | _ -> f ^ ".tex" (*s \textbf{Separation of files.} Files given on the command line are separated according to their type, which is determined by their @@ -232,8 +236,10 @@ let parse () = multi_index := true; parse_rec rem | ("-toc" | "--toc" | "--table-of-contents") :: rem -> toc := true; parse_rec rem + | ("-stdout" | "--stdout") :: rem -> + out_to := StdOut; parse_rec rem | ("-o" | "--output") :: f :: rem -> - output_file := f; parse_rec rem + out_to := File f; parse_rec rem | ("-o" | "--output") :: [] -> usage () | ("-d" | "--directory") :: dir :: rem -> @@ -251,30 +257,29 @@ let parse () = | ("-t" | "-title" | "--title") :: [] -> usage () | ("-latex" | "--latex") :: rem -> - Output.target_language := LaTeX; parse_rec rem + Cdglobals.target_language := LaTeX; parse_rec rem | ("-dvi" | "--dvi") :: rem -> - Output.target_language := LaTeX; dvi := true; parse_rec rem + Cdglobals.target_language := LaTeX; dvi := true; parse_rec rem | ("-ps" | "--ps") :: rem -> - Output.target_language := LaTeX; ps := true; parse_rec rem + Cdglobals.target_language := LaTeX; ps := true; parse_rec rem | ("-html" | "--html") :: rem -> - Output.target_language := HTML; parse_rec rem + Cdglobals.target_language := HTML; parse_rec rem | ("-texmacs" | "--texmacs") :: rem -> - Output.target_language := TeXmacs; parse_rec rem - + Cdglobals.target_language := TeXmacs; parse_rec rem | ("-charset" | "--charset") :: s :: rem -> - Output.charset := s; parse_rec rem + Cdglobals.charset := s; parse_rec rem | ("-charset" | "--charset") :: [] -> usage () | ("-inputenc" | "--inputenc") :: s :: rem -> - Output.inputenc := s; parse_rec rem + Cdglobals.inputenc := s; parse_rec rem | ("-inputenc" | "--inputenc") :: [] -> usage () | ("-raw-comments" | "--raw-comments") :: rem -> - Output.raw_comments := true; parse_rec rem + Cdglobals.raw_comments := true; parse_rec rem | ("-latin1" | "--latin1") :: rem -> - Output.set_latin1 (); parse_rec rem + Cdglobals.set_latin1 (); parse_rec rem | ("-utf8" | "--utf8") :: rem -> - Output.set_utf8 (); parse_rec rem + Cdglobals.set_utf8 (); parse_rec rem | ("-q" | "-quiet" | "--quiet") :: rem -> quiet := true; parse_rec rem @@ -298,7 +303,6 @@ let parse () = parse_rec rem | ("-files" | "--files") :: [] -> usage () - | "-R" :: path :: log :: rem -> add_path path log; parse_rec rem | "-R" :: ([] | [_]) -> @@ -308,12 +312,11 @@ let parse () = | ("-glob-from" | "--glob-from") :: [] -> usage () | ("--no-externals" | "-no-externals" | "-noexternals") :: rem -> - Output.externals := false; parse_rec rem + Cdglobals.externals := false; parse_rec rem | ("--coqlib" | "-coqlib") :: u :: rem -> - Output.coqlib := u; parse_rec rem + Cdglobals.coqlib := u; parse_rec rem | ("--coqlib" | "-coqlib") :: [] -> usage () - | f :: rem -> add_file (what_file f); parse_rec rem in @@ -360,52 +363,128 @@ let copy src dst = with End_of_file -> close_in cin; close_out cout + +(*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 + | Latex_file _ -> () + in + if (!header_trailer) then header (); + if !toc then make_toc (); + List.iter file l; + if !index then make_index(); + if (!header_trailer) then trailer () + +let gen_mult_files l = + let file = function + | Vernac_file (f,m) -> + 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 (); + close_out_file() + | Latex_file _ -> () + in + List.iter file l; + if (!index && !target_language=HTML) then begin + if (!multi_index) then 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 (); + 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 !title <> "" then printf "

%s

\n" !title; + make_toc (); + if (!header_trailer) then trailer (); + close_out_file() + end + (* Rq: pour latex et texmacs, une toc ou un index séparé n'a pas de sens... *) + + +let index_module = function + | Vernac_file (_,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 Coq_config.coqlib "/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 Coq_config.coqlib "/tools/coqdoc/coqdoc.sty") in + let dst = if !output_dir <> "" then + Filename.concat !output_dir "coqdoc.sty" + else "coqdoc.sty" in + copy src dst); + match !out_to with + | StdOut -> + Cdglobals.out_channel := stdout; + gen_one_file l + | File f -> + open_out_file f; + gen_one_file l; + close_out_file() + | MultFiles -> + gen_mult_files l + let produce_output fl = if not (!dvi || !ps) then begin - if !output_file <> "" then set_out_file !output_file; produce_document fl end else begin let texfile = temp_file "coqdoc" ".tex" in let basefile = chop_suffix texfile ".tex" in - set_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 - 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 + open_out_file texfile; + produce_document fl; let command = - sprintf "dvips %s -o %s %s" dvifile psfile - (if !quiet then "> /dev/null 2>&1" else "") + let file = basename texfile in + let file = + if !quiet then sprintf "'\\nonstopmode\\input{%s}'" file else file + in + sprintf "(latex %s && latex %s) 1>&2 %s" file file + (if !quiet then "> /dev/null" 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; - if !output_file = "" then cat psfile - end; - clean_temp_files basefile + 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 + end; + if !output_file = "" then cat psfile + end; + clean_temp_files basefile end @@ -415,6 +494,6 @@ let produce_output fl = let main () = let files = parse () in if not !quiet then banner (); - if List.length files > 0 then produce_output files + if files <> [] then produce_output files let _ = Printexc.catch main () diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index c10f3683..4c4cf5ec 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -6,30 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: output.ml,v 1.7.2.1 2004/07/16 19:31:47 herbelin Exp $ i*) +(*i $Id: output.ml 8669 2006-03-28 17:34:15Z notin $ i*) +open Cdglobals open Index -(*s Target language *) - -type target_language = LaTeX | HTML | TeXmacs - -let target_language = ref HTML - (*s Low level output *) -let out_channel = ref stdout -let output_is_file = ref false -let output_dir = ref "" - -let set_out_file f = - let f = if !output_dir <> "" then Filename.concat !output_dir f else f in - out_channel := open_out f; - output_is_file := true - -let close () = - if !output_is_file then close_out !out_channel - let output_char c = Pervasives.output_char !out_channel c let output_string s = Pervasives.output_string !out_channel s @@ -38,43 +21,6 @@ let printf s = Printf.fprintf !out_channel s let sprintf = Printf.sprintf -let dump_file f = - let ch = open_in f in - try - while true do - Pervasives.output_char !out_channel (input_char ch) - done - with End_of_file -> close_in ch - -(*s Options *) - -let header_trailer = ref true -let quiet = ref false -let light = ref false -let short = ref false -let index = ref true -let multi_index = ref false -let toc = ref false -let page_title = ref "" -let title = ref "" -let externals = ref true -let coqlib = ref "http://coq.inria.fr/library/" -let raw_comments = ref false - -let charset = ref "" -let inputenc = ref "" -let latin1 = ref false -let utf8 = ref false - -let set_latin1 () = - charset := "iso-8859-1"; - inputenc := "latin1"; - latin1 := true - -let set_utf8 () = - charset := "utf-8"; - inputenc := "utf8"; - utf8 := true (*s Coq keywords *) @@ -85,9 +31,9 @@ let build_table l = let is_keyword = build_table - [ "Add"; "AddPath"; "Axiom"; "Chapter"; "CoFixpoint"; + [ "AddPath"; "Axiom"; "Chapter"; "CoFixpoint"; "CoInductive"; "Defined"; "Definition"; - "End"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Hint"; + "End"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint"; "Hypothesis"; "Hypotheses"; "Immediate"; "Implicit"; "Import"; "Inductive"; "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac"; @@ -145,6 +91,7 @@ let _ = List.iter "|-", "\\ensuremath{\\vdash}"; "forall", "\\ensuremath{\\forall}"; "exists", "\\ensuremath{\\exists}"; + (* "fun", "\\ensuremath{\\lambda}" ? *) ] (*s Table of contents *) @@ -308,6 +255,8 @@ module Latex = struct let end_inline_coq () = () + let make_multi_index () = () + let make_index () = () let make_toc () = printf "\\tableofcontents\n" @@ -321,29 +270,31 @@ module Html = struct let header () = if !header_trailer then begin + printf "\n"; printf "\n\n"; - if !charset != "" then - printf "" !charset; - printf ""; + printf "\n" !charset; + printf "\n"; printf "%s\n\n\n" !page_title; - printf "\n\n" + printf "\n\n
\n\n
\n
\n\n"; + printf "
\n\n" end - let self = "http://www.lri.fr/~filliatr/coqdoc/" + let self = "http://coq.inria.fr" let trailer () = if !index && !current_module <> "Index" then - printf "
Index"; + printf "
\n\n
\n
Index"; if !header_trailer then begin printf "
This page has been generated by "; printf "coqdoc\n" self; - printf "\n" + printf "
\n\n
\n\n\n" end let start_module () = if not !short then begin (* add_toc_entry (Toc_library !current_module); *) - printf "

Library %s

\n\n" !current_module + printf "

Library %s

\n\n" !current_module end let indentation n = for i = 1 to n do printf " " done @@ -373,7 +324,7 @@ module Html = struct let stop_verbatim () = printf "\n" let module_ref m s = - printf "" m; raw_ident s; printf "" + printf "" m; raw_ident s; printf "" (*i match find_module m with | Local -> @@ -387,18 +338,18 @@ module Html = struct let ident_ref m s = match find_module m with | Local -> - printf "" m s; raw_ident s; printf "" + printf "" m s; raw_ident s; printf "" | Coqlib when !externals -> let m = Filename.concat !coqlib m in - printf "" m s; raw_ident s; printf "" + printf "" m s; raw_ident s; printf "" | Coqlib | Unknown -> raw_ident s let ident s loc = if is_keyword s then begin - printf ""; + printf ""; raw_ident s; - printf "" + printf "" end else try (match Index.find !current_module loc with @@ -447,11 +398,11 @@ module Html = struct let start_doc () = if not !raw_comments then - printf "\n
\n" + printf "\n
\n" let end_doc () = stop_item (); - if not !raw_comments then printf "\n
\n" + if not !raw_comments then printf "\n\n" let start_code () = end_doc (); start_coq () @@ -470,7 +421,7 @@ module Html = struct stop_item (); printf "" lab lev; f (); - printf "\n" lev + printf "\n" lev let rule () = printf "
\n" @@ -502,20 +453,8 @@ module Html = struct let all_letters i = List.iter (letter_index false i.idx_name) i.idx_entries - let separate_index navig i = - let idx = i.idx_name in - let one_letter ((c,l) as cl) = - set_out_file (sprintf "index_%s_%c.html" idx c); - header (); - navig (); - printf "
"; - letter_index true idx cl; - if List.length l > 30 then begin printf "
"; navig () end; - trailer (); - close () - in - List.iter one_letter i.idx_entries - + (* Construction d'une liste des index (1 index global, puis 1 + index par catégorie) *) let format_global_index = Index.map (fun s (m,t) -> @@ -523,7 +462,7 @@ module Html = struct "[library]", m ^ ".html" else sprintf "[%s, in %s]" (entry_type t) m m , - sprintf "%s.html#%s" m s) + sprintf "%s.html#%s" m s) let format_bytype_index = function | Library, idx -> @@ -532,9 +471,10 @@ module Html = struct Index.map (fun s m -> let text = sprintf "[in %s]" m m in - (text, sprintf "%s.html#%s" m s)) idx + (text, sprintf "%s.html#%s" m s)) idx - let navig_one_index i = + (* Impression de la table d'index *) + let print_index_table_item i = printf "\n%s Index\n" (String.capitalize i.idx_name); List.iter (fun (c,l) -> @@ -544,52 +484,58 @@ module Html = struct printf "%c\n" c) i.idx_entries; let n = i.idx_size in - printf "(%d %s)\n" n (if n > 1 then "entries" else "entry"); - printf "\n" + printf "(%d %s)\n" n (if n > 1 then "entries" else "entry"); + printf "\n" - let navig_index il = + let print_index_table idxl = printf "\n"; - List.iter navig_one_index il; + List.iter print_index_table_item idxl; printf "
\n" - + + let make_one_multi_index prt_tbl i = + (* 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); + if (!header_trailer) then header (); + prt_tbl (); printf "
"; + letter_index true idx cl; + if List.length l > 30 then begin printf "
"; prt_tbl () end; + if (!header_trailer) then trailer (); + close_out_file () + in + List.iter one_letter i.idx_entries + + let make_multi_index () = + let all_index = + let glob,bt = Index.all_entries () in + (format_global_index glob) :: + (List.map format_bytype_index bt) in + let print_table () = print_index_table all_index in + List.iter (make_one_multi_index print_table) all_index + let make_index () = - if !index then begin - let idxl = - let glob,bt = Index.all_entries () in - format_global_index glob :: - List.map format_bytype_index bt - in - let navig () = navig_index idxl in - set_out_file "index.html"; + let all_index = + let glob,bt = Index.all_entries () in + (format_global_index glob) :: + (List.map format_bytype_index bt) in + let print_table () = print_index_table all_index in + let print_one_index i = + if i.idx_size > 0 then begin + printf "
\n

%s Index

\n" (String.capitalize i.idx_name); + all_letters i + end + in current_module := "Index"; - page_title := (if !title <> "" then !title else "Index"); - header (); if !title <> "" then printf "

%s

\n" !title; - navig (); - if !multi_index then begin - trailer (); - close (); - List.iter (separate_index navig) idxl; - end else begin - let one_index i = - if i.idx_size > 0 then begin - printf "
\n

%s Index

\n" (String.capitalize i.idx_name); - all_letters i - end - in - List.iter one_index idxl; - printf "
"; - navig (); - trailer (); - close () - end; - end - + print_table (); + if not (!multi_index) then + begin + List.iter print_one_index all_index; + printf "
"; print_table () + end + let make_toc () = - set_out_file "toc.html"; - page_title := (if !title <> "" then !title else "Table of contents"); - header (); - if !title <> "" then printf "

%s

\n" !title; let make_toc_entry = function | Toc_library m -> stop_item (); @@ -600,9 +546,6 @@ module Html = struct in Queue.iter make_toc_entry toc_q; stop_item (); - if !index then printf "

Index

"; - trailer (); - close () end @@ -740,6 +683,8 @@ module TeXmacs = struct let end_inline_coq () = printf "]>" + let make_multi_index () = () + let make_index () = () let make_toc () = () @@ -808,5 +753,6 @@ let verbatim_char = select output_char Html.char TeXmacs.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 diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli index 2195fa53..87b311f3 100644 --- a/tools/coqdoc/output.mli +++ b/tools/coqdoc/output.mli @@ -6,35 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: output.mli,v 1.3.2.1 2004/07/16 19:31:47 herbelin Exp $ i*) +(*i $Id: output.mli 8669 2006-03-28 17:34:15Z notin $ i*) +open Cdglobals open Index -type target_language = LaTeX | HTML | TeXmacs - -val target_language : target_language ref - -val set_out_file : string -> unit -val output_dir : string ref -val close : unit -> unit - -val quiet : bool ref -val short : bool ref -val light : bool ref -val header_trailer : bool ref -val index : bool ref -val multi_index : bool ref -val toc : bool ref -val title : string ref -val externals : bool ref -val coqlib : string ref -val raw_comments : bool ref - -val charset : string ref -val inputenc : string ref -val set_latin1 : unit -> unit -val set_utf8 : unit -> unit - val add_printing_token : string -> string option * string option -> unit val remove_printing_token : string -> unit @@ -45,8 +21,6 @@ val trailer : unit -> unit val push_in_preamble : string -> unit -val dump_file : string -> unit - val start_module : unit -> unit val start_doc : unit -> unit @@ -88,5 +62,6 @@ val stop_latex_math : unit -> unit val start_verbatim : unit -> unit val stop_verbatim : unit -> unit +val make_multi_index : unit -> unit val make_index : unit -> unit val make_toc : unit -> unit diff --git a/tools/coqdoc/pretty.mli b/tools/coqdoc/pretty.mli index 07808fe9..dda0439e 100644 --- a/tools/coqdoc/pretty.mli +++ b/tools/coqdoc/pretty.mli @@ -6,14 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pretty.mli,v 1.1.2.1 2004/07/16 19:31:47 herbelin Exp $ i*) +(*i $Id: pretty.mli 8617 2006-03-08 10:47:12Z notin $ i*) open Index -type file = - | Vernac_file of string * coq_module - | Latex_file of string - -val gallina : bool ref - -val produce_document : file list -> unit +val coq_file : string -> Cdglobals.coq_module -> unit diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll index 541939b5..ad9057ad 100644 --- a/tools/coqdoc/pretty.mll +++ b/tools/coqdoc/pretty.mll @@ -6,12 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pretty.mll,v 1.7.2.1 2004/07/16 19:31:47 herbelin Exp $ i*) +(*i $Id: pretty.mll 8666 2006-03-27 17:02:49Z notin $ i*) (*s Utility functions for the scanners *) { + open Cdglobals open Printf open Index open Lexing @@ -56,39 +57,8 @@ let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos - (* Gallina (skipping proofs). This is a three states automaton. *) - - let gallina = ref false - - type gallina_state = Nothing | AfterDot | Proof - - let gstate = ref AfterDot - - let is_proof = - let t = Hashtbl.create 13 in - List.iter (fun s -> Hashtbl.add t s true) - [ "Theorem"; "Lemma"; "Fact"; "Remark"; "Goal"; "Let"; - "Correctness"; "Definition"; "Morphism" ]; - fun s -> try Hashtbl.find t s with Not_found -> false - - let gallina_id id = - if !gstate = AfterDot then - if is_proof id then gstate := Proof else - if id <> "Add" then gstate := Nothing - - let gallina_symbol s = - if !gstate = AfterDot || (!gstate = Proof && s = ":=") then - gstate := Nothing - let is_space = function ' ' | '\t' | '\n' | '\r' -> true | _ -> false - let gallina_char c = - if c = '.' then - (let skip = !gstate = Proof in gstate := AfterDot; skip) - else - (if !gstate = AfterDot && not (is_space c) then gstate := Nothing; - false) - (* saving/restoring the PP state *) type state = { @@ -121,8 +91,7 @@ let reset () = formatted := false; - brackets := 0; - gstate := AfterDot + brackets := 0 (* erasing of Section/End *) @@ -216,6 +185,100 @@ let symbolchar_no_brackets = let symbolchar = symbolchar_no_brackets | '[' | ']' let token = symbolchar+ | '[' [^ '[' ']' ':']* ']' + +let thm_token = + "Theorem" + | "Lemma" + | "Fact" + | "Remark" + | "Corollary" + | "Proposition" + | "Property" + | "Goal" + +let def_token = + "Definition" + | "Let" + | "SubClass" + | "Example" + | "Local" + | "Fixpoint" + | "CoFixpoint" + | "Record" + | "Structure" + | "Scheme" + | "Inductive" + | "CoInductive" + +let decl_token = + "Hypothesis" + | "Hypotheses" + | "Parameter" + | "Axiom" 's'? + | "Conjecture" + +let gallina_ext = + "Module" + | "Declare" + | "Transparent" + | "Opaque" + | "Canonical" + | "Coercion" + | "Identity" + | "Implicit" + | "Notation" + | "Infix" + | "Tactic" space+ "Notation" + | "Reserved" space+ "Notation" + +let commands = + "Pwd" + | "Cd" + | "Drop" + | "ProtectedLoop" + | "Quit" + | "Load" + | "Add" + | "Remove" space+ "Loadpath" + | "Print" + | "Inspect" + | "About" + | "Search" + | "Eval" + | "Reset" + | "Check" + | "Type" + +let extraction = + "Extraction" + | "Recursive" space+ "Extraction" + | "Extract" + +let gallina_kw = thm_token | def_token | decl_token | gallina_ext | commands | extraction + +let gallina_kw_to_hide = + "Implicit" + | "Ltac" + | "Require" + | "Import" + | "Export" + | "Load" + | "Hint" + | "Open" + | "Close" + | "Delimit" + | "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" + + (* tokens with balanced brackets *) let token_brackets = ( symbolchar_no_brackets+ ('[' symbolchar_no_brackets* ']')* @@ -235,32 +298,18 @@ let begin_verb = "(*" space* "begin" space+ "verb" space* "*)" let end_verb = "(*" space* "end" space+ "verb" space* "*)" *) -let coq_command_to_hide = - "Implicit" space | - "Ltac" space | - "Require" space | - "Load" space | - "Hint" space | - "Transparent" space | - "Opaque" space | - ("Declare" space+ ("Morphism" | "Step") space) | - "Section" space | - "Variable" 's'? space | - ("Hypothesis" | "Hypotheses") space | - "End" space | - ("Set" | "Unset") space+ "Printing" space+ "Coercions" space | - "Declare" space+ ("Left" | "Right") space+ "Step" space + (*s Scanning Coq, at beginning of line *) rule coq_bol = parse - | '\n'+ + | space* '\n'+ { empty_line_of_code (); coq_bol lexbuf } | space* "(**" space_nl { end_coq (); start_doc (); let eol = doc_bol lexbuf in - end_doc (); start_coq (); - if eol then coq_bol lexbuf else coq lexbuf } + end_doc (); 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 } @@ -270,28 +319,40 @@ rule coq_bol = parse { begin_show (); coq_bol lexbuf } | space* end_show { end_show (); coq_bol lexbuf } - | space* coq_command_to_hide + | 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 - indentation (count_spaces s); - backtrack lexbuf; - coq lexbuf - end } + if !light && section_or_end s then begin + skip_to_dot lexbuf; + coq_bol lexbuf + end else begin + let s = lexeme lexbuf in + 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 } + | space* gallina_kw + { let s = lexeme lexbuf in + 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 } | space* "(**" space+ "printing" space+ (identifier | token) space+ { let tok = lexeme lexbuf in let s = printing_token lexbuf in - add_printing_token tok s; - coq_bol lexbuf } + add_printing_token tok s; + coq_bol lexbuf } | space* "(**" space+ "printing" space+ { eprintf "warning: bad 'printing' command at character %d\n" (lexeme_start lexbuf); flush stderr; ignore (comment lexbuf); coq_bol lexbuf } | space* "(**" space+ "remove" space+ "printing" space+ - (identifier | token) space* "*)" + (identifier | token) space* "*)" { remove_printing_token (lexeme lexbuf); coq_bol lexbuf } | space* "(**" space+ "remove" space+ "printing" space+ @@ -301,68 +362,77 @@ rule coq_bol = parse coq_bol lexbuf } | space* "(*" { let eol = comment lexbuf in - if eol then coq_bol lexbuf else coq lexbuf } - | space+ - { indentation (count_spaces (lexeme lexbuf)); coq lexbuf } + if eol then coq_bol lexbuf else coq lexbuf } | eof { () } - | _ - { backtrack lexbuf; indentation 0; coq lexbuf } + | _ + { let eol = + if not !gallina then + begin backtrack lexbuf; indentation 0; body_bol lexbuf end + else + skip_to_dot lexbuf + in + if eol then coq_bol lexbuf else coq lexbuf } (*s Scanning Coq elsewhere *) and coq = parse | "\n" - { line_break (); coq_bol lexbuf } + { line_break(); coq_bol lexbuf } | "(**" space_nl { end_coq (); start_doc (); let eol = doc_bol lexbuf in - end_doc (); start_coq (); - if eol then coq_bol lexbuf else coq lexbuf } + end_doc (); start_coq (); + if eol then coq_bol lexbuf else coq lexbuf } | "(*" { let eol = comment lexbuf in - if eol then coq_bol lexbuf else coq lexbuf } + if eol then begin line_break(); coq_bol lexbuf end + else coq lexbuf + } | '\n'+ space* "]]" { if not !formatted then begin symbol (lexeme lexbuf); coq lexbuf end } | eof { () } - | token + | gallina_kw_to_hide { let s = lexeme lexbuf in - if !gallina then gallina_symbol s; - symbol s; - coq lexbuf } - | "with" space+ "Module" | "Module" space+ "Type" | "Declare" space+ "Module" - (* hack to avoid making Type a keyword *) - { let s = lexeme lexbuf in - if !gallina then gallina_id s; - ident s (lexeme_start lexbuf); coq lexbuf } - | "(" space* identifier space* ":=" - { let id = extract_ident (lexeme lexbuf) in - symbol "("; ident id (lexeme_start lexbuf); symbol ":="; coq lexbuf } - | (identifier '.')* identifier - { let id = lexeme lexbuf in - if !gallina then gallina_id id; - ident id (lexeme_start lexbuf); coq lexbuf } - | _ - { let c = lexeme_char lexbuf 0 in - char c; - if !gallina && gallina_char c then skip_proof lexbuf; - coq lexbuf } - + if !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); + 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); + let eol = body lexbuf in + if eol then coq_bol lexbuf else coq lexbuf } + | space+ { char ' '; coq lexbuf } + | eof + { () } + | _ { let eol = + if not !gallina then + begin backtrack lexbuf; indentation 0; body lexbuf end + else + skip_to_dot lexbuf + 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* +{ 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 } | eof { false } @@ -481,22 +551,33 @@ and comment = parse | eof { false } | _ { comment lexbuf } -(*s Skip proofs *) - -and skip_proof = parse - | "(*" { ignore (comment lexbuf); skip_proof lexbuf } - | "Save" | "Qed" | "Defined" - | "Abort" | "Proof" | "Admitted" { skip_to_dot lexbuf } - | "Proof" space* '.' { skip_proof lexbuf } - | identifier { skip_proof lexbuf } (* to avoid keywords within idents *) - | eof { () } - | _ { skip_proof lexbuf } - and skip_to_dot = parse - | eof | '.' { if !gallina then gstate := AfterDot } + | '.' space* '\n' { 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 } + | _ { backtrack lexbuf; body lexbuf } + +and body = parse + | '\n' {line_break(); body_bol lexbuf} + | eof { false } + | '.' space* '\n' | '.' space* eof { char '.'; line_break(); true } + | '.' space+ { char '.'; char ' '; false } + | "(*" { let eol = comment lexbuf in + if eol then body_bol lexbuf else body lexbuf } + | identifier + { let s = lexeme lexbuf in + ident s (lexeme_start lexbuf); body lexbuf } + | token + { let s = lexeme lexbuf in + symbol s; body lexbuf } + | _ { let c = lexeme_char lexbuf 0 in + char c; body lexbuf } + and skip_hide = parse | eof | end_hide { () } | _ { skip_hide lexbuf } @@ -515,10 +596,6 @@ and printing_token = parse { - type file = - | Vernac_file of string * coq_module - | Latex_file of string - let coq_file f m = reset (); Index.scan_file f m; @@ -528,59 +605,5 @@ and printing_token = parse start_coq (); coq_bol lb; end_coq (); close_in c - (* LaTeX document *) - - let latex_document l = - let file = function - | Vernac_file (f,m) -> set_module m; coq_file f m - | Latex_file f -> dump_file f - in - header (); - if !toc then make_toc (); - List.iter file l; - trailer (); - close () - - (* HTML document *) - - let html_document l = - let file = function - | Vernac_file (f,m) -> - set_module m; - let hf = m ^ ".html" in - set_out_file hf; - header (); - coq_file f m; - trailer (); - close () - | Latex_file _ -> () - in - List.iter file l; - make_index (); - if !toc then make_toc () - - (* TeXmacs document *) - - let texmacs_document l = - let file = function - | Vernac_file (f,m) -> set_module m; coq_file f m - | Latex_file f -> dump_file f - in - header (); - List.iter file l; - trailer (); - close () - - let index_module = function - | Vernac_file (_,m) -> Index.add_module m - | Latex_file _ -> () - - let produce_document l = - List.iter index_module l; - (match !target_language with - | LaTeX -> latex_document - | HTML -> html_document - | TeXmacs -> texmacs_document) l - } diff --git a/tools/coqwc.mll b/tools/coqwc.mll index 08bf2bcc..26b64095 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,v 1.2.2.1 2004/07/16 19:31:46 herbelin Exp $ i*) +(*i $Id: coqwc.mll 7095 2005-05-31 15:05:23Z filliatr $ 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. *) @@ -99,7 +99,7 @@ let dot = '.' (' ' | '\t' | '\n' | '\r' | eof) let proof_start = "Theorem" | "Lemma" | "Fact" | "Remark" | "Goal" | "Correctness" let proof_end = - ("Save" | "Qed" | "Defined" | "Abort") [^'.']* '.' + ("Save" | "Qed" | "Defined" | "Abort" | "Admitted") [^'.']* '.' (*s [spec] scans the specification. *) diff --git a/tools/gallina.ml b/tools/gallina.ml index c997820c..a2c05c6d 100644 --- a/tools/gallina.ml +++ b/tools/gallina.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: gallina.ml,v 1.2.16.1 2004/07/16 19:31:46 herbelin Exp $ *) +(* $Id: gallina.ml 5920 2004-07-16 20:01:26Z herbelin $ *) open Gallina_lexer diff --git a/tools/gallina_lexer.mll b/tools/gallina_lexer.mll index ce9fb950..0b769dbd 100644 --- a/tools/gallina_lexer.mll +++ b/tools/gallina_lexer.mll @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: gallina_lexer.mll,v 1.5.6.1 2004/07/16 19:31:46 herbelin Exp $ *) +(* $Id: gallina_lexer.mll 5920 2004-07-16 20:01:26Z herbelin $ *) { open Lexing diff --git a/tools/restore-v7 b/tools/restore-v7 deleted file mode 100755 index ab884587..00000000 --- a/tools/restore-v7 +++ /dev/null @@ -1,9 +0,0 @@ -#!/bin/sh - -echo Restoring v7 files from directory v7 -v7files=`find v7 -name \*.v` -for i in $v7files; do - j=`echo $i | sed -e "s@^v7/@@"` - echo Restoring $i from v7 - cp -f $i $j -done diff --git a/tools/translate-v8 b/tools/translate-v8 deleted file mode 100755 index 7d71bea9..00000000 --- a/tools/translate-v8 +++ /dev/null @@ -1,41 +0,0 @@ -#!/bin/sh - -if [ -e v7 ]; then - echo "Warning: v7 directory found, the files are maybe already translated"; - sleep 5; -fi -echo --------- Producing v8 files in the translation directory ------------- -if [ -e v8 ]; then rm -r v8; fi -if [ -e /tmp/v7.$$ ]; then rm -r /tmp/v7.$$; fi -cp -pr . /tmp/v7.$$ -cp -pr /tmp/v7.$$ v8 -cd v8 -rm description toto -make clean -make COQFLAGS='-translate -q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)' || \ - { echo ---- Failed to translate; exit 1; } -echo --------- Upgrading files in the translation directory ---------------- -v8files=`find . -name \*.v8` -for i in $v8files; do - j=`dirname $i`/`basename $i .v8`.v - echo Upgrading $j in the translation directory - mv -u -f $i $j -done -echo --------- Recompiling v8 files in the translation directory ----------- -make clean -make || { echo ---- Failed to recompile; exit 1; } -echo --------- Saving v7 files in directory v7 ----------------------------- -/bin/rm -r ../v7 -mv /tmp/v7.$$ ../v7 -echo Saving v7 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 v8/$i $i -done -echo --------- Translation completed --------------------------------------- -echo Old files are in directory '"v7"' -echo New files are in current directory -echo You can now remove the translation directory '"v8"' diff --git a/tools/translate_V6-3-1_to_V7-0 b/tools/translate_V6-3-1_to_V7-0 deleted file mode 100755 index 10e7f140..00000000 --- a/tools/translate_V6-3-1_to_V7-0 +++ /dev/null @@ -1,27 +0,0 @@ -#! /bin/sh - -echo "This shell script performs the following transformations:" -echo "- Insertion of a space after a dot not followed by a separator" -echo "- Insertion of a space between consecutive ~ and < and between" -echo " consecutive | and < assumed to be part of distinct tokens" -echo "- Various renamings of commands as described in document Changes.ps" - -for i in $* - do sed -e "s/\.\([A-Z]\)/\. \1/g" -e "s/AddPath/Add LoadPath/g" \ - -e "s/~ $i.tmp$$ - if diff $i.tmp$$ $i > /dev/null - then - rm $i.tmp$$ - else - echo Le fichier $i a été modifié - mv $i.tmp$$ $i - fi - done -echo diff --git a/tools/upgrade-v8 b/tools/upgrade-v8 deleted file mode 100755 index 36d0bf8c..00000000 --- a/tools/upgrade-v8 +++ /dev/null @@ -1,22 +0,0 @@ -#!/bin/sh - -mv v7 v7.bak - -echo ---------------- Saving v7 files into directory v7 ------------------ -vfiles=`find . -name \*.v` -for i in $vfiles; do - if expr $i : 'v7\.bak/.*\.v' > /dev/null ; then continue ; fi - if expr $i : 'v7/.*\.v' > /dev/null ; then continue ; fi - echo Saving $i into v7/$i - j=v7/$i - mkdir -p `dirname $j` - mv -u -f $i $j -done - -echo ---------------- Upgrading files with v8 syntax --------------------- -v8files=`find . -name \*.v8` -for i in $v8files; do - j=`dirname $i`/`basename $i .v8`.v - echo Upgrading $i - mv -u -f $i $j -done -- cgit v1.2.3