summaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
Diffstat (limited to 'tools')
-rwxr-xr-xtools/check-v824
-rw-r--r--tools/coq-tex.ml42
-rw-r--r--tools/coq_makefile.ml427
-rw-r--r--[-rwxr-xr-x]tools/coqdep.ml3
-rwxr-xr-xtools/coqdep_lexer.mll2
-rw-r--r--tools/coqdoc/alpha.ml2
-rw-r--r--tools/coqdoc/alpha.mli2
-rw-r--r--tools/coqdoc/cdglobals.ml72
-rw-r--r--tools/coqdoc/coqdoc.css59
-rw-r--r--tools/coqdoc/coqdoc.sty5
-rw-r--r--tools/coqdoc/index.mli4
-rw-r--r--tools/coqdoc/index.mll4
-rw-r--r--tools/coqdoc/main.ml197
-rw-r--r--tools/coqdoc/output.ml212
-rw-r--r--tools/coqdoc/output.mli31
-rw-r--r--tools/coqdoc/pretty.mli10
-rw-r--r--tools/coqdoc/pretty.mll371
-rw-r--r--tools/coqwc.mll4
-rw-r--r--tools/gallina.ml2
-rw-r--r--tools/gallina_lexer.mll2
-rwxr-xr-xtools/restore-v79
-rwxr-xr-xtools/translate-v841
-rwxr-xr-xtools/translate_V6-3-1_to_V7-027
-rwxr-xr-xtools/upgrade-v822
24 files changed, 582 insertions, 552 deletions
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";
@@ -118,6 +118,9 @@ let standard sds =
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;
print "\n";
@@ -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
index ab7cef92..eb740712 100755..100644
--- 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 *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+
+
+(*s Output options *)
+
+type target_language = LaTeX | HTML | TeXmacs
+
+let target_language = ref HTML
+
+type output_t =
+ | StdOut
+ | MultFiles
+ | File of string
+
+let output_dir = ref ""
+
+let out_to = ref MultFiles
+
+let out_channel = ref stdout
+
+let open_out_file f =
+ let f = if !output_dir <> "" then Filename.concat !output_dir f else f in
+ 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 <lionel@mamane.lu> 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 <file> write output in file <file>";
prerr_endline " -d <dir> output files into directory <dir>";
prerr_endline " -g (gallina) skip proofs";
@@ -58,8 +60,6 @@ let usage () =
prerr_endline " --charset <string> set HTML charset";
prerr_endline " --inputenc <string> 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 "<h1>%s</h1>\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 "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"\n";
+ printf "\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">\n";
printf "<html xmlns=\"http://www.w3.org/1999/xhtml\">\n<head>\n";
- if !charset != "" then
- printf "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=%s\">" !charset;
- printf "<link rel=\"stylesheet\" href=\"style.css\" type=\"text/css\">";
+ printf "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=%s\"/>\n" !charset;
+ printf "<link href=\"coqdoc.css\" rel=\"stylesheet\" type=\"text/css\"/>\n";
printf "<title>%s</title>\n</head>\n\n" !page_title;
- printf "<body>\n\n"
+ printf "<body>\n\n<div id=\"page\">\n\n<div id=\"header\">\n</div>\n\n";
+ printf "<div id=\"main\">\n\n"
end
- let self = "http://www.lri.fr/~filliatr/coqdoc/"
+ let self = "http://coq.inria.fr"
let trailer () =
if !index && !current_module <> "Index" then
- printf "<hr/><a href=\"index.html\">Index</a>";
+ printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"index.html\">Index</a>";
if !header_trailer then begin
printf "<hr/><font size=\"-1\">This page has been generated by ";
printf "<a href=\"%s\">coqdoc</a></font>\n" self;
- printf "</body>\n</html>"
+ printf "</div>\n\n</div>\n\n</body>\n</html>"
end
let start_module () =
if not !short then begin
(* add_toc_entry (Toc_library !current_module); *)
- printf "<h1>Library %s</h1>\n\n" !current_module
+ printf "<h1 class=\"libtitle\">Library %s</h1>\n\n" !current_module
end
let indentation n = for i = 1 to n do printf "&nbsp;" done
@@ -373,7 +324,7 @@ module Html = struct
let stop_verbatim () = printf "</pre>\n"
let module_ref m s =
- printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>"
+ printf "<a class=\"modref\" href=\"%s.html\">" m; raw_ident s; printf "</a>"
(*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 "<a href=\"%s.html#%s\">" m s; raw_ident s; printf "</a>"
+ printf "<a class=\"idref\" href=\"%s.html#%s\">" m s; raw_ident s; printf "</a>"
| Coqlib when !externals ->
let m = Filename.concat !coqlib m in
- printf "<a href=\"%s.html#%s\">" m s; raw_ident s; printf "</a>"
+ printf "<a class=\"idref\" href=\"%s.html#%s\">" m s; raw_ident s; printf "</a>"
| Coqlib | Unknown ->
raw_ident s
let ident s loc =
if is_keyword s then begin
- printf "<code class=\"keyword\">";
+ printf "<span class=\"keyword\">";
raw_ident s;
- printf "</code>"
+ printf "</span>"
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<table width=\"100%%\"><tr class=\"doc\"><td>\n"
+ printf "\n<div class=\"doc\">\n"
let end_doc () =
stop_item ();
- if not !raw_comments then printf "\n</td></tr></table>\n"
+ if not !raw_comments then printf "\n</div>\n"
let start_code () = end_doc (); start_coq ()
@@ -470,7 +421,7 @@ module Html = struct
stop_item ();
printf "<a name=\"%s\"></a><h%d>" lab lev;
f ();
- printf "</h%d>\n" lev
+ printf "</h%d class=\"section\">\n" lev
let rule () = printf "<hr/>\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 "<hr/>";
- letter_index true idx cl;
- if List.length l > 30 then begin printf "<hr/>"; 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 <a href=\"%s.html\">%s</a>]" (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 <a href=\"%s.html\">%s</a>]" 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 "<tr>\n<td>%s Index</td>\n" (String.capitalize i.idx_name);
List.iter
(fun (c,l) ->
@@ -544,52 +484,58 @@ module Html = struct
printf "<td>%c</td>\n" c)
i.idx_entries;
let n = i.idx_size in
- printf "<td>(%d %s)</td>\n" n (if n > 1 then "entries" else "entry");
- printf "</tr>\n"
+ printf "<td>(%d %s)</td>\n" n (if n > 1 then "entries" else "entry");
+ printf "</tr>\n"
- let navig_index il =
+ let print_index_table idxl =
printf "<table>\n";
- List.iter navig_one_index il;
+ List.iter print_index_table_item idxl;
printf "</table>\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 "<hr/>";
+ letter_index true idx cl;
+ if List.length l > 30 then begin printf "<hr/>"; 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 "<hr/>\n<h1>%s Index</h1>\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 "<h1>%s</h1>\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 "<hr/>\n<h1>%s Index</h1>\n" (String.capitalize i.idx_name);
- all_letters i
- end
- in
- List.iter one_index idxl;
- printf "<hr/>";
- navig ();
- trailer ();
- close ()
- end;
- end
-
+ print_table ();
+ if not (!multi_index) then
+ begin
+ List.iter print_one_index all_index;
+ printf "<hr/>"; 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 "<h1>%s</h1>\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 "<a href=\"index.html\"><h2>Index</h2></a>";
- 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/~</~ </g" -e "s/|</| </g" \
- -e "s/AddPath/Add LoadPath/g" -e "s/DelPath/Remove LoadPath/g" \
- -e "s/AddRecPath/Add Rec LoadPath/g" \
- -e "s/Implicit *Arguments *On/Set Implicit Arguments/g" \
- -e "s/Implicit *Arguments *Off/Unset Implicit Arguments/g" \
- -e "s/Begin *Silent/Set Silent/g" -e "s/End *Silent/Unset Silent/g" \
- -e "s/Print *Path/Print Coercion Paths/g" \
- $i > $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