aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-09-17 15:58:14 +0000
committerGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-09-17 15:58:14 +0000
commit61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch)
tree961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /tools
parent6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff)
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
-rw-r--r--tools/coq_makefile.ml486
-rw-r--r--tools/coq_tex.ml434
-rw-r--r--tools/coqdep.ml34
-rw-r--r--tools/coqdep_common.ml64
-rwxr-xr-xtools/coqdep_lexer.mll32
-rw-r--r--tools/coqdoc/alpha.ml4
-rw-r--r--tools/coqdoc/cdglobals.ml2
-rw-r--r--tools/coqdoc/cpretty.mll432
-rw-r--r--tools/coqdoc/index.mli8
-rw-r--r--tools/coqdoc/index.mll222
-rw-r--r--tools/coqdoc/main.ml148
-rw-r--r--tools/coqdoc/output.ml234
-rw-r--r--tools/coqwc.mll72
-rw-r--r--tools/gallina.ml22
-rw-r--r--tools/gallina_lexer.mll32
15 files changed, 713 insertions, 713 deletions
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index 8a39c383a..486c8804f 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -42,7 +42,7 @@ let rec print_list sep = function
let list_iter_i f =
let rec aux i = function [] -> () | a::l -> f i a; aux (i+1) l in aux 1
-let best_ocamlc =
+let best_ocamlc =
if Coq_config.best = "opt" then "ocamlc.opt" else "ocamlc"
let best_ocamlopt =
if Coq_config.best = "opt" then "ocamlopt.opt" else "ocamlopt"
@@ -85,7 +85,7 @@ coq_makefile [subdirectory] .... [file.v] ... [file.ml] ... [-custom
[-impredicative-set]: compile with option -impredicative-set of coq
[-no-install]: build a makefile with no install target
[-f file]: take the contents of file as arguments
-[-o file]: output should go in file file
+[-o file]: output should go in file file
[-h]: print this usage summary
[--help]: equivalent to [-h]\n";
exit 1
@@ -215,7 +215,7 @@ let clean sds sps =
print "\trm -f $(CMOFILES) $(MLFILES:.ml=.cmi) $(MLFILES:.ml=.ml.d) $(MLFILES:.ml=.cmx) $(MLFILES:.ml=.o)\n";
print "\t- rm -rf html\n";
List.iter
- (fun (file,_,_) ->
+ (fun (file,_,_) ->
if not (is_genrule file) then
(print "\t- rm -f "; print file; print "\n"))
sps;
@@ -233,8 +233,8 @@ let clean sds sps =
print "\t@echo CAMLP4LIB =\t$(CAMLP4LIB)\n\n"
let header_includes () = ()
-
-let footer_includes () =
+
+let footer_includes () =
if !some_vfile then print "-include $(VFILES:.v=.v.d)\n.SECONDARY: $(VFILES:.v=.v.d)\n\n";
if !some_mlfile then print "-include $(MLFILES:.ml=.ml.d)\n.SECONDARY: $(MLFILES:.ml=.ml.d)\n\n"
@@ -267,7 +267,7 @@ let variables defs =
let var_aux (v,def) = print v; print "="; print def; print "\n" in
section "Variables definitions.";
print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n";
- if !opt = "-byte" then
+ if !opt = "-byte" then
print "override OPT:=-byte\n"
else
print "OPT:=\n";
@@ -297,8 +297,8 @@ let parameters () =
print "# This Makefile may take 3 arguments passed as environment variables:\n";
print "# - COQBIN to specify the directory where Coq binaries resides;\n";
print "# - CAMLBIN and CAMLP4BIN to give the path for the OCaml and Camlp4/5 binaries.\n";
- print "COQLIB:=$(shell $(COQBIN)coqtop -where | sed -e 's/\\\\/\\\\\\\\/g')\n";
- print "CAMLP4:=\"$(shell $(COQBIN)coqtop -config | awk -F = '/CAMLP4=/{print $$2}')\"\n";
+ print "COQLIB:=$(shell $(COQBIN)coqtop -where | sed -e 's/\\\\/\\\\\\\\/g')\n";
+ print "CAMLP4:=\"$(shell $(COQBIN)coqtop -config | awk -F = '/CAMLP4=/{print $$2}')\"\n";
print "ifndef CAMLP4BIN\n CAMLP4BIN:=$(CAMLBIN)\nendif\n\n";
print "CAMLP4LIB:=$(shell $(CAMLP4BIN)$(CAMLP4) -where)\n\n"
@@ -329,7 +329,7 @@ let rec special = function
| [] -> []
| Special (file,deps,com) :: r -> (file,deps,com) :: (special r)
| _ :: r -> special r
-
+
let custom sps =
let pr_path (file,dependencies,com) =
print file; print ": "; print dependencies; print "\n";
@@ -347,7 +347,7 @@ let subdirs sds =
section "Special targets.";
print ".PHONY: ";
print_list " "
- ("all" :: "opt" :: "byte" :: "archclean" :: "clean" :: "install"
+ ("all" :: "opt" :: "byte" :: "archclean" :: "clean" :: "install"
:: "depend" :: "html" :: sds);
print "\n\n"
@@ -356,7 +356,7 @@ let rec split_arguments = function
let (v,m,o,s),i,d = split_arguments r in ((canonize n::v,m,o,s),i,d)
| ML n :: r ->
let (v,m,o,s),i,d = split_arguments r in ((v,canonize n::m,o,s),i,d)
- | Special (n,dep,c) :: r ->
+ | Special (n,dep,c) :: r ->
let (v,m,o,s),i,d = split_arguments r in ((v,m,(n,dep,c)::o,s),i,d)
| Subdir n :: r ->
let (v,m,o,s),i,d = split_arguments r in ((v,m,o,n::s),i,d)
@@ -364,7 +364,7 @@ let rec split_arguments = function
let t,(i,r),d = split_arguments r in (t,((p,absolute_dir p)::i,r),d)
| RInclude (p,l) :: r ->
let t,(i,r),d = split_arguments r in (t,(i,(p,l,absolute_dir p)::r),d)
- | Def (v,def) :: r ->
+ | Def (v,def) :: r ->
let t,i,d = split_arguments r in (t,i,(v,def)::d)
| [] -> ([],[],[],[]),([],[]),[]
@@ -397,15 +397,15 @@ let main_targets vfiles mlfiles other_targets inc =
if !some_mlfile then print "$(CMOFILES) ";
if Coq_config.has_natdynlink && !some_mlfile then print "$(CMXSFILES) ";
print_list "\\\n " other_targets; print "\n";
- if !some_vfile then
+ if !some_vfile then
begin
print "spec: $(VIFILES)\n\n";
print "gallina: $(GFILES)\n\n";
print "html: $(GLOBFILES) $(VFILES)\n";
- print "\t- mkdir html\n";
+ print "\t- mkdir html\n";
print "\t$(COQDOC) -toc -html $(COQDOCLIBS) -d html $(VFILES)\n\n";
print "gallinahtml: $(GLOBFILES) $(VFILES)\n";
- print "\t- mkdir html\n";
+ print "\t- mkdir html\n";
print "\t$(COQDOC) -toc -html -g $(COQDOCLIBS) -d html $(VFILES)\n\n";
print "all.ps: $(VFILES)\n";
print "\t$(COQDOC) -toc -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n";
@@ -425,20 +425,20 @@ let all_target (vfiles, mlfiles, sps, sds) inc =
main_targets vfiles mlfiles other_targets inc;
custom sps;
subdirs sds
-
+
let parse f =
- let rec string = parser
+ let rec string = parser
| [< '' ' | '\n' | '\t' >] -> ""
| [< 'c; s >] -> (String.make 1 c)^(string s)
| [< >] -> ""
- and string2 = parser
+ and string2 = parser
| [< ''"' >] -> ""
| [< 'c; s >] -> (String.make 1 c)^(string2 s)
- and skip_comment = parser
+ and skip_comment = parser
| [< ''\n'; s >] -> s
| [< 'c; s >] -> skip_comment s
| [< >] -> [< >]
- and args = parser
+ and args = parser
| [< '' ' | '\n' | '\t'; s >] -> args s
| [< ''#'; s >] -> args (skip_comment s)
| [< ''"'; str = string2; s >] -> ("" ^ str) :: args s
@@ -451,13 +451,13 @@ let parse f =
res
let rec process_cmd_line = function
- | [] ->
+ | [] ->
some_file := !some_file or !some_mlfile or !some_vfile; []
- | ("-h"|"--help") :: _ ->
+ | ("-h"|"--help") :: _ ->
usage ()
- | ("-no-opt"|"-byte") :: r ->
+ | ("-no-opt"|"-byte") :: r ->
opt := "-byte"; process_cmd_line r
- | ("-full"|"-opt") :: r ->
+ | ("-full"|"-opt") :: r ->
opt := "-opt"; process_cmd_line r
| "-impredicative-set" :: r ->
impredicative_set := true; process_cmd_line r
@@ -476,32 +476,32 @@ let rec process_cmd_line = function
Include d :: (process_cmd_line r)
| "-R" :: p :: l :: r ->
RInclude (p,l) :: (process_cmd_line r)
- | ("-I"|"-custom") :: _ ->
+ | ("-I"|"-custom") :: _ ->
usage ()
- | "-f" :: file :: r ->
+ | "-f" :: file :: r ->
make_name := file;
process_cmd_line ((parse file)@r)
- | ["-f"] ->
+ | ["-f"] ->
usage ()
- | "-o" :: file :: r ->
+ | "-o" :: file :: r ->
makefile_name := file;
output_channel := (open_out file);
(process_cmd_line r)
- | v :: "=" :: def :: r ->
+ | v :: "=" :: def :: r ->
Def (v,def) :: (process_cmd_line r)
| f :: r ->
if Filename.check_suffix f ".v" then begin
- some_vfile := true;
+ some_vfile := true;
V f :: (process_cmd_line r)
end else if (Filename.check_suffix f ".ml") || (Filename.check_suffix f ".ml4") then begin
- some_mlfile := true;
+ some_mlfile := true;
ML f :: (process_cmd_line r)
end else if (Filename.check_suffix f ".mli") then begin
Printf.eprintf "Warning: no need for .mli files, skipped %s\n" f;
process_cmd_line r
end else
Subdir f :: (process_cmd_line r)
-
+
let banner () =
print (Printf.sprintf
"##########################################################################
@@ -518,23 +518,23 @@ let warning () =
print "# This Makefile has been automagically generated\n";
print "# Edit at your own risks !\n";
print "#\n# END OF WARNING\n\n"
-
+
let print_list l = List.iter (fun x -> print x; print " ") l
-
+
let command_line args =
print "#\n# This Makefile was generated by the command line :\n";
print "# coq_makefile ";
print_list args;
print "\n#\n\n"
-
+
let directories_deps l =
- let print_dep f dep =
+ let print_dep f dep =
if dep <> [] then begin print f; print ": "; print_list dep; print "\n" end
in
let rec iter ((dirs,before) as acc) = function
- | [] ->
+ | [] ->
()
- | (Subdir d) :: l ->
+ | (Subdir d) :: l ->
print_dep d before; iter (d :: dirs, d :: before) l
| (ML f) :: l ->
print_dep f dirs; iter (dirs, f :: before) l
@@ -542,7 +542,7 @@ let directories_deps l =
print_dep f dirs; iter (dirs, f :: before) l
| (Special (f,_,_)) :: l ->
print_dep f dirs; iter (dirs, f :: before) l
- | _ :: l ->
+ | _ :: l ->
iter acc l
in
iter ([],[]) l
@@ -560,7 +560,7 @@ let warn_install_at_root_directory (vfiles,mlfiles,_,_) (inc_i,inc_r) =
if not !no_install &&
List.exists (fun f -> List.mem_assoc (Filename.dirname f) inc_top) files
then
- Printf.eprintf "Warning: install target will copy files at the first level of the coq contributions installation directory; option -R %sis recommended\n"
+ Printf.eprintf "Warning: install target will copy files at the first level of the coq contributions installation directory; option -R %sis recommended\n"
(if inc_r_top = [] then "" else "with non trivial logical root ")
let check_overlapping_include (inc_i,inc_r) =
@@ -575,7 +575,7 @@ let check_overlapping_include (inc_i,inc_r) =
Printf.eprintf "Warning: in options -R, %s and %s overlap\n" pdir pdir') l;
List.iter (fun (pdir',abspdir') ->
if is_prefix abspdir abspdir' or is_prefix abspdir' abspdir then
- Printf.eprintf "Warning: in option -I, %s overlap with %s in option -R\n" pdir' pdir) inc_i
+ Printf.eprintf "Warning: in option -I, %s overlap with %s in option -R\n" pdir' pdir) inc_i
in aux inc_r
let do_makefile args =
@@ -602,12 +602,12 @@ let do_makefile args =
warning ();
if not (!output_channel == stdout) then close_out !output_channel;
exit 0
-
+
let main () =
let args =
if Array.length Sys.argv = 1 then usage ();
List.tl (Array.to_list Sys.argv)
in
do_makefile args
-
+
let _ = Printexc.catch main ()
diff --git a/tools/coq_tex.ml4 b/tools/coq_tex.ml4
index 30f55468b..c46a187c5 100644
--- a/tools/coq_tex.ml4
+++ b/tools/coq_tex.ml4
@@ -12,7 +12,7 @@
* JCF, 16/1/98
* adapted from caml-tex (perl script written by Xavier Leroy)
*
- * Perl isn't as portable as it pretends to be, and is quite difficult
+ * Perl isn't as portable as it pretends to be, and is quite difficult
* to read and maintain... Let us rewrite the stuff in Caml! *)
let _ =
@@ -64,10 +64,10 @@ let extract texfile inputv =
outside ()
in
try
- output_string chan_out
+ output_string chan_out
("Set Printing Width " ^ (string_of_int !linelen) ^".\n");
outside ()
- with End_of_file ->
+ with End_of_file ->
begin close_in chan_in; close_out chan_out end
(* Second pass: insert the answers of Coq from [coq_output] into the
@@ -89,11 +89,11 @@ let expos = Str.regexp "^"
let tex_escaped s =
let rec trans = parser
- | [< s1 = (parser
- | [< ''_'|'$'|'{'|'}'|'&'|'%'|'#' as c >] ->
+ | [< s1 = (parser
+ | [< ''_'|'$'|'{'|'}'|'&'|'%'|'#' as c >] ->
"\\" ^ (String.make 1 c)
- | [< ''\\' >] -> "{\\char'134}"
- | [< ''^' >] -> "{\\char'136}"
+ | [< ''\\' >] -> "{\\char'134}"
+ | [< ''^' >] -> "{\\char'136}"
| [< ''~' >] -> "{\\char'176}"
| [< '' ' >] -> "~"
| [< ''<' >] -> "{<}"
@@ -101,7 +101,7 @@ let tex_escaped s =
| [< 'c >] -> String.make 1 c);
s2 = trans >] -> s1 ^ s2
| [< >] -> ""
- in
+ in
trans (Stream.of_string s)
let encapsule sl c_out s =
@@ -109,7 +109,7 @@ let encapsule sl c_out s =
Printf.fprintf c_out "\\texttt{\\textit{%s}}\\\\\n" (tex_escaped s)
else
Printf.fprintf c_out "\\texttt{%s}\\\\\n" (tex_escaped s)
-
+
let print_block c_out bl =
List.iter (fun s -> if s="" then () else encapsule !slanted c_out s) bl
@@ -138,7 +138,7 @@ let insert texfile coq_output result =
let first = !last_read in first :: (read_lines ())
in
(* we are just after \end{coq_...} block *)
- let rec just_after () =
+ let rec just_after () =
let s = input_line c_tex in
if Str.string_match begin_coq_example s 0 then begin
inside (Str.matched_group 1 s <> "example*")
@@ -149,11 +149,11 @@ let insert texfile coq_output result =
output_string c_out "\\end{flushleft}\n";
if !small then output_string c_out "\\end{small}\n";
if Str.string_match begin_coq_eval s 0 then
- eval 0
+ eval 0
else begin
output_string c_out (s ^ "\n");
outside ()
- end
+ end
end
(* we are outside of a \begin{coq_...} ... \end{coq_...} block *)
and outside () =
@@ -173,7 +173,7 @@ let insert texfile coq_output result =
(* we are inside a \begin{coq_example?} ... \end{coq_example?} block
* show_answers tells what kind of block it is
* k is the number of lines read until now *)
- and inside show_answers show_questions k first_block =
+ and inside show_answers show_questions k first_block =
let s = input_line c_tex in
if Str.string_match end_coq_example s 0 then begin
just_after ()
@@ -183,7 +183,7 @@ let insert texfile coq_output result =
if show_questions then encapsule false c_out ("Coq < " ^ s);
if has_match dot_end_line s then begin
let bl = next_block (succ k) in
- if !verbose then List.iter print_endline bl;
+ if !verbose then List.iter print_endline bl;
if show_answers then print_block c_out bl;
inside show_answers show_questions 0 false
end else
@@ -228,14 +228,14 @@ let one_file texfile =
else if Filename.check_suffix texfile ".tex" then
(Filename.chop_suffix texfile ".tex") ^ ".v.tex"
else
- texfile ^ ".v.tex"
+ texfile ^ ".v.tex"
in
try
(* 1. extract Coq phrases *)
extract texfile inputv;
(* 2. run Coq on input *)
let _ = Sys.command (Printf.sprintf "%s < %s > %s 2>&1" !image inputv
- coq_output)
+ coq_output)
in
(* 3. insert Coq output into original file *)
insert texfile coq_output result;
@@ -250,7 +250,7 @@ let one_file texfile =
* of all the files in the command line, one by one *)
let files = ref []
-
+
let parse_cl () =
Arg.parse
[ "-o", Arg.String (fun s -> output_specified := true; output := s),
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 5faedf682..9be50c62c 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -45,7 +45,7 @@ let add_coqlib_known phys_dir log_dir f =
Hashtbl.add coqlibKnown name ()
| _ -> ()
-let sort () =
+let sort () =
let seen = Hashtbl.create 97 in
let rec loop file =
let file = canonize file in
@@ -57,8 +57,8 @@ let sort () =
while true do
match coq_action lb with
| Require sl ->
- List.iter
- (fun s ->
+ List.iter
+ (fun s ->
try loop (Hashtbl.find vKnown s)
with Not_found -> ())
sl
@@ -73,16 +73,16 @@ let sort () =
List.iter (fun (name,_) -> loop name) !vAccu
let (dep_tab : (string,string list) Hashtbl.t) = Hashtbl.create 151
-
-let mL_dep_list b f =
- try
+
+let mL_dep_list b f =
+ try
Hashtbl.find dep_tab f
with Not_found ->
- let deja_vu = ref ([] : string list) in
- try
- let chan = open_in f in
- let buf = Lexing.from_channel chan in
- try
+ let deja_vu = ref ([] : string list) in
+ try
+ let chan = open_in f in
+ let buf = Lexing.from_channel chan in
+ try
while true do
let (Use_module str) = caml_action buf in
if str = b then begin
@@ -93,14 +93,14 @@ let mL_dep_list b f =
if not (List.mem str !deja_vu) then addQueue deja_vu str
done; []
with Fin_fichier -> begin
- close_in chan;
+ close_in chan;
let rl = List.rev !deja_vu in
Hashtbl.add dep_tab f rl;
rl
end
with Sys_error _ -> []
-let affiche_Declare f dcl =
+let affiche_Declare f dcl =
printf "\n*** In file %s: \n" f;
printf "Declare ML Module";
List.iter (fun str -> printf " \"%s\"" str) dcl;
@@ -115,7 +115,7 @@ let warning_Declare f dcl =
eprintf ".\n";
flush stderr
-let traite_Declare f =
+let traite_Declare f =
let decl_list = ref ([] : string list) in
let rec treat = function
| s :: ll ->
@@ -133,15 +133,15 @@ let traite_Declare f =
try
let chan = open_in f in
let buf = Lexing.from_channel chan in
- begin try
+ begin try
while true do
let tok = coq_action buf in
(match tok with
- | Declare sl ->
+ | Declare sl ->
decl_list := [];
treat sl;
decl_list := List.rev !decl_list;
- if !option_D then
+ if !option_D then
affiche_Declare f !decl_list
else if !decl_list <> sl then
warning_Declare f !decl_list
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 43395b0e9..21fc66fc6 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -78,7 +78,7 @@ let addQueue q v = q := v :: !q
let safe_hash_add clq q (k,v) =
try
let v2 = Hashtbl.find q k in
- if v<>v2 then
+ if v<>v2 then
let rec add_clash = function
(k1,l1)::cltl when k=k1 -> (k1,v::l1)::cltl
| cl::cltl -> cl::add_clash cltl
@@ -88,7 +88,7 @@ let safe_hash_add clq q (k,v) =
(** Files found in the loadpaths.
For the ML files, the string is the basename without extension.
- To allow ML source filename to be potentially capitalized,
+ To allow ML source filename to be potentially capitalized,
we perform a double search.
*)
@@ -177,16 +177,16 @@ let depend_ML str =
| None, None -> "", ""
let traite_fichier_ML md ext =
- try
- let chan = open_in (md ^ ext) in
- let buf = Lexing.from_channel chan in
+ try
+ let chan = open_in (md ^ ext) in
+ let buf = Lexing.from_channel chan in
let deja_vu = ref [md] in
let a_faire = ref "" in
let a_faire_opt = ref "" in
- begin try
+ begin try
while true do
let (Use_module str) = caml_action buf in
- if List.mem str !deja_vu then
+ if List.mem str !deja_vu then
()
else begin
addQueue deja_vu str;
@@ -223,13 +223,13 @@ let canonize f =
| (f,_) :: _ -> f
| _ -> f
-let traite_fichier_Coq verbose f =
- try
- let chan = open_in f in
- let buf = Lexing.from_channel chan in
+let traite_fichier_Coq verbose f =
+ try
+ let chan = open_in f in
+ let buf = Lexing.from_channel chan in
let deja_vu_v = ref ([]: string list list)
and deja_vu_ml = ref ([] : string list) in
- try
+ try
while true do
let tok = coq_action buf in
match tok with
@@ -240,18 +240,18 @@ let traite_fichier_Coq verbose f =
try
let file_str = safe_assoc verbose f str in
printf " %s%s" (canonize file_str) !suffixe
- with Not_found ->
+ with Not_found ->
if verbose && not (Hashtbl.mem coqlibKnown str) then
warning_module_notfound f str
end) strl
- | RequireString s ->
+ | RequireString s ->
let str = Filename.basename s in
if not (List.mem [str] !deja_vu_v) then begin
addQueue deja_vu_v [str];
try
let file_str = Hashtbl.find vKnown [str] in
printf " %s%s" (canonize file_str) !suffixe
- with Not_found ->
+ with Not_found ->
if not (Hashtbl.mem coqlibKnown [str]) then
warning_notfound f s
end
@@ -273,7 +273,7 @@ let traite_fichier_Coq verbose f =
| None -> warning_declare f str
end
in List.iter decl sl
- | Load str ->
+ | Load str ->
let str = Filename.basename str in
if not (List.mem [str] !deja_vu_v) then begin
addQueue deja_vu_v [str];
@@ -285,11 +285,11 @@ let traite_fichier_Coq verbose f =
done
with Fin_fichier -> ();
close_in chan
- with Sys_error _ -> ()
+ with Sys_error _ -> ()
let mL_dependencies () =
- List.iter
+ List.iter
(fun (name,ext,dirname) ->
let fullname = file_name name dirname in
let (dep,dep_opt) = traite_fichier_ML fullname ext in
@@ -344,10 +344,10 @@ let add_known phys_dir log_dir f =
| (basename,".mllib") -> add_mllib_known basename (Some phys_dir)
| _ -> ()
-(* Visits all the directories under [dir], including [dir],
+(* Visits all the directories under [dir], including [dir],
or just [dir] if [recur=false] *)
-let rec add_directory recur add_file phys_dir log_dir =
+let rec add_directory recur add_file phys_dir log_dir =
let dirh = opendir phys_dir in
try
while true do
@@ -366,32 +366,32 @@ let rec add_directory recur add_file phys_dir log_dir =
done
with End_of_file -> closedir dirh
-let add_dir add_file phys_dir log_dir =
+let add_dir add_file phys_dir log_dir =
try add_directory false add_file phys_dir log_dir with Unix_error _ -> ()
-let add_rec_dir add_file phys_dir log_dir =
+let add_rec_dir add_file phys_dir log_dir =
handle_unix_error (add_directory true add_file phys_dir) log_dir
let rec treat_file old_dirname old_name =
- let name = Filename.basename old_name
+ let name = Filename.basename old_name
and new_dirname = Filename.dirname old_name in
- let dirname =
- match (old_dirname,new_dirname) with
+ let dirname =
+ match (old_dirname,new_dirname) with
| (d, ".") -> d
| (None,d) -> Some d
- | (Some d1,d2) -> Some (d1//d2)
+ | (Some d1,d2) -> Some (d1//d2)
in
let complete_name = file_name name dirname in
- match try (stat complete_name).st_kind with _ -> S_BLK with
+ match try (stat complete_name).st_kind with _ -> S_BLK with
| S_DIR ->
- (if name.[0] <> '.' then
+ (if name.[0] <> '.' then
let dir=opendir complete_name in
- let newdirname =
- match dirname with
+ let newdirname =
+ match dirname with
| None -> name
- | Some d -> d//name
+ | Some d -> d//name
in
- try
+ try
while true do treat_file (Some newdirname) (readdir dir) done
with End_of_file -> closedir dir)
| S_REG ->
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index 3c7d09e1f..b13c16bad 100755
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -7,26 +7,26 @@
(************************************************************************)
(*i $Id$ i*)
-
+
{
- open Filename
+ open Filename
open Lexing
-
+
type mL_token = Use_module of string
type spec = bool
-
- type coq_token =
+
+ type coq_token =
| Require of string list list
| RequireString of string
| Declare of string list
| Load of string
let comment_depth = ref 0
-
+
exception Fin_fichier
-
+
let module_current_name = ref []
let module_names = ref []
let ml_module_name = ref ""
@@ -62,10 +62,10 @@ rule coq_action = parse
| "\""
{ string lexbuf; coq_action lexbuf}
| "(*" (* "*)" *)
- { comment_depth := 1; comment lexbuf; coq_action lexbuf }
- | eof
- { raise Fin_fichier}
- | _
+ { comment_depth := 1; comment lexbuf; coq_action lexbuf }
+ | eof
+ { raise Fin_fichier}
+ | _
{ coq_action lexbuf }
and caml_action = parse
@@ -132,7 +132,7 @@ and comment = parse
| "'" '\\' ['0'-'9'] ['0'-'9'] ['0'-'9'] "'"
{ comment lexbuf }
| eof
- { raise Fin_fichier }
+ { raise Fin_fichier }
| _ { comment lexbuf }
and string = parse
@@ -157,7 +157,7 @@ and load_file = parse
Load (if check_suffix f ".v" then chop_suffix f ".v" else f) }
| coq_ident
{ let s = lexeme lexbuf in skip_to_dot lexbuf; Load s }
- | eof
+ | eof
{ raise Fin_fichier }
| _
{ load_file lexbuf }
@@ -196,7 +196,7 @@ and opened_file_fields = parse
{ module_current_name :=
field_name (Lexing.lexeme lexbuf) :: !module_current_name;
opened_file_fields lexbuf }
- | coq_ident { module_names :=
+ | coq_ident { module_names :=
List.rev !module_current_name :: !module_names;
module_current_name := [Lexing.lexeme lexbuf];
opened_file_fields lexbuf }
@@ -211,10 +211,10 @@ and modules = parse
| "(*" (* "*)" *) { comment_depth := 1; comment lexbuf;
modules lexbuf }
| '"' [^'"']* '"'
- { let lex = (Lexing.lexeme lexbuf) in
+ { let lex = (Lexing.lexeme lexbuf) in
let str = String.sub lex 1 (String.length lex - 2) in
mllist := str :: !mllist; modules lexbuf}
- | _ { (Declare (List.rev !mllist)) }
+ | _ { (Declare (List.rev !mllist)) }
and qual_id = parse
| '.' [^ '.' '(' '['] {
diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml
index aef17031d..fe26e0086 100644
--- a/tools/coqdoc/alpha.ml
+++ b/tools/coqdoc/alpha.ml
@@ -32,10 +32,10 @@ let compare_char c1 c2 = match norm_char c1, norm_char c2 with
| _, 'A'..'Z' -> 1
| c1, c2 -> compare c1 c2
-let compare_string s1 s2 =
+let compare_string s1 s2 =
let n1 = String.length s1 in
let n2 = String.length s2 in
- let rec cmp i =
+ let rec cmp i =
if i == n1 || i == n2 then
n1 - n2
else
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index 2ee90820f..4994a1280 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -37,7 +37,7 @@ type glob_source_t =
| DotGlob
| GlobFile of string
-let glob_source = ref DotGlob
+let glob_source = ref DotGlob
let header_trailer = ref true
let header_file = ref ""
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index d9ed86297..22d81d6f5 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -16,7 +16,7 @@
open Lexing
(* A list function we need *)
- let rec take n ls =
+ let rec take n ls =
if n = 0 then [] else
match ls with
| [] -> []
@@ -25,7 +25,7 @@
(* count the number of spaces at the beginning of a string *)
let count_spaces s =
let n = String.length s in
- let rec count c i =
+ let rec count c i =
if i == n then c,i else match s.[i] with
| '\t' -> count (c + (8 - (c mod 8))) (i + 1)
| ' ' -> count (c + 1) (i + 1)
@@ -47,10 +47,10 @@
if l <= r then String.sub s l (r-l+1) else s
let sec_title s =
- let rec count lev i =
- if s.[i] = '*' then
- count (succ lev) (succ i)
- else
+ let rec count lev i =
+ if s.[i] = '*' then
+ count (succ lev) (succ i)
+ else
let t = String.sub s i (String.length s - i) in
lev, cut_head_tail_spaces t
in
@@ -88,14 +88,14 @@
let state_stack = Stack.create ()
- let save_state () =
+ let save_state () =
Stack.push { st_gallina = !Cdglobals.gallina; st_light = !Cdglobals.light } state_stack
let restore_state () =
let s = Stack.pop state_stack in
Cdglobals.gallina := s.st_gallina;
Cdglobals.light := s.st_light
-
+
let without_ref r f x = save_state (); r := false; f x; restore_state ()
let without_gallina = without_ref Cdglobals.gallina
@@ -127,16 +127,16 @@
if is_section s then begin
incr sections_to_close; true
end else if is_end s then begin
- if !sections_to_close > 0 then begin
- decr sections_to_close; true
- end else
+ if !sections_to_close > 0 then begin
+ decr sections_to_close; true
+ end else
false
end else
true
(* for item lists *)
- type list_compare =
- | Before
+ type list_compare =
+ | Before
| StartLevel of int
| InLevel of int * bool
@@ -147,16 +147,16 @@
let find_level levels cur_indent =
match levels with
| [] -> Before
- | (l::ls) ->
+ | (l::ls) ->
if cur_indent < l then Before
- else
+ else
(* cur_indent will never be less than the head of the list *)
- let rec findind ls n =
+ let rec findind ls n =
match ls with
| [] -> InLevel (n,true)
| (l :: []) -> if cur_indent = l then StartLevel n
else InLevel (n,true)
- | (l1 :: l2 :: ls) ->
+ | (l1 :: l2 :: ls) ->
if cur_indent = l1 then StartLevel n
else if cur_indent < l2 then InLevel (n,false)
else findind (l2 :: ls) (n+1)
@@ -171,16 +171,16 @@
let check_start_list str =
let n_dashes = count_dashes str in
let (n_spaces,_) = count_spaces str in
- if n_dashes >= 4 then
+ if n_dashes >= 4 then
Rule
- else
+ else
if n_dashes = 1 then
List n_spaces
else
Neither
(* examine a string for subtitleness *)
- let subtitle m s =
+ let subtitle m s =
match Str.split_delim (Str.regexp ":") s with
| [] -> false
| (name::_) ->
@@ -194,7 +194,7 @@
let token_buffer = Buffer.create 1024
- let token_re =
+ let token_re =
Str.regexp "[ \t]*(\\*\\*[ \t]+printing[ \t]+\\([^ \t]+\\)"
let printing_token_re =
Str.regexp
@@ -205,8 +205,8 @@
if Str.string_match token_re toks 0 then
let tok = Str.matched_group 1 toks in
if Str.string_match printing_token_re pps 0 then
- let pp =
- (try Some (Str.matched_group 3 pps) with _ ->
+ let pp =
+ (try Some (Str.matched_group 3 pps) with _ ->
try Some (Str.matched_group 4 pps) with _ -> None),
(try Some (Str.matched_group 6 pps) with _ -> None)
in
@@ -214,8 +214,8 @@
with _ ->
()
- let remove_token_re =
- Str.regexp
+ let remove_token_re =
+ Str.regexp
"[ \t]*(\\*\\*[ \t]+remove[ \t]+printing[ \t]+\\([^ \t]+\\)[ \t]*\\*)"
let remove_printing_token toks =
@@ -234,7 +234,7 @@
else
String.sub s 1 (String.length s - 3)
- let symbol lexbuf s = Output.symbol s
+ let symbol lexbuf s = Output.symbol s
}
@@ -244,41 +244,41 @@ let space = [' ' '\t']
let space_nl = [' ' '\t' '\n' '\r']
let nl = "\r\n" | '\n'
-let firstchar =
- ['A'-'Z' 'a'-'z' '_'
- (* iso 8859-1 accents *)
+let firstchar =
+ ['A'-'Z' 'a'-'z' '_'
+ (* iso 8859-1 accents *)
'\192'-'\214' '\216'-'\246' '\248'-'\255' ] |
(* *)
'\194' '\185' |
- (* utf-8 latin 1 supplement *)
+ (* utf-8 latin 1 supplement *)
'\195' ['\128'-'\191'] |
- (* utf-8 letterlike symbols *)
+ (* utf-8 letterlike symbols *)
'\206' ('\160' | [ '\177'-'\183'] | '\187') |
'\226' ('\130' [ '\128'-'\137' ] (* subscripts *)
| '\129' [ '\176'-'\187' ] (* superscripts *)
| '\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])
-let identchar =
+let identchar =
firstchar | ['\'' '0'-'9' '@' ]
let id = firstchar identchar*
let pfx_id = (id '.')*
-let identifier =
+let identifier =
id | pfx_id id
(* This misses unicode stuff, and it adds "[" and "]". It's only an
approximation of idents - used for detecting whether an underscore
is part of an identifier or meant to indicate emphasis *)
-let nonidentchar =
+let nonidentchar =
[^ 'A'-'Z' 'a'-'z' '_' '[' ']'
- (* iso 8859-1 accents *)
+ (* iso 8859-1 accents *)
'\192'-'\214' '\216'-'\246' '\248'-'\255'
'\'' '0'-'9' '@' ]
let symbolchar_symbol_no_brackets =
['!' '$' '%' '&' '*' '+' ',' '^' '#'
'\\' '/' '-' '<' '>' '|' ':' '?' '=' '~' ] |
- (* utf-8 symbols *)
+ (* utf-8 symbols *)
'\226' ['\134'-'\143' '\152'-'\155' '\164'-'\165' '\168'-'\171'] _
-let symbolchar_no_brackets = symbolchar_symbol_no_brackets |
+let symbolchar_no_brackets = symbolchar_symbol_no_brackets |
[ '@' '{' '}' '(' ')' 'A'-'Z' 'a'-'z' '_']
let symbolchar = symbolchar_no_brackets | '[' | ']'
let token_no_brackets = symbolchar_symbol_no_brackets symbolchar_no_brackets*
@@ -287,17 +287,17 @@ let printing_token = (token | id)+
(* tokens with balanced brackets *)
let token_brackets =
- ( token_no_brackets ('[' token_no_brackets? ']')*
+ ( token_no_brackets ('[' token_no_brackets? ']')*
| token_no_brackets? ('[' token_no_brackets? ']')+ )
token_no_brackets?
-let thm_token =
- "Theorem"
- | "Lemma"
- | "Fact"
- | "Remark"
- | "Corollary"
- | "Proposition"
+let thm_token =
+ "Theorem"
+ | "Lemma"
+ | "Fact"
+ | "Remark"
+ | "Corollary"
+ | "Proposition"
| "Property"
| "Goal"
@@ -305,18 +305,18 @@ let prf_token =
"Next" space+ "Obligation"
| "Proof" (space* "." | space+ "with")
-let def_token =
- "Definition"
- | "Let"
+let def_token =
+ "Definition"
+ | "Let"
| "Class"
| "SubClass"
| "Example"
- | "Local"
- | "Fixpoint"
- | "Boxed"
- | "CoFixpoint"
- | "Record"
- | "Structure"
+ | "Local"
+ | "Fixpoint"
+ | "Boxed"
+ | "CoFixpoint"
+ | "Record"
+ | "Structure"
| "Scheme"
| "Inductive"
| "CoInductive"
@@ -324,15 +324,15 @@ let def_token =
| "Instance"
| "Global" space+ "Instance"
-let decl_token =
- "Hypothesis"
- | "Hypotheses"
- | "Parameter"
- | "Axiom" 's'?
+let decl_token =
+ "Hypothesis"
+ | "Hypotheses"
+ | "Parameter"
+ | "Axiom" 's'?
| "Conjecture"
let gallina_ext =
- "Module"
+ "Module"
| "Include" space+ "Type"
| "Include"
| "Declare" space+ "Module"
@@ -352,7 +352,7 @@ let gallina_ext =
| ("Hypothesis" | "Hypotheses")
| "End"
-let commands =
+let commands =
"Pwd"
| "Cd"
| "Drop"
@@ -378,9 +378,9 @@ let commands =
let end_kw = "Qed" | "Defined" | "Save" | "Admitted" | "Abort"
-let extraction =
+let extraction =
"Extraction"
- | "Recursive" space+ "Extraction"
+ | "Recursive" space+ "Extraction"
| "Extract"
let gallina_kw = thm_token | def_token | decl_token | gallina_ext | commands | extraction
@@ -397,7 +397,7 @@ let gallina_kw_to_hide =
| "Require"
| "Import"
| "Export"
- | "Load"
+ | "Load"
| "Hint"
| "Open"
| "Close"
@@ -406,7 +406,7 @@ let gallina_kw_to_hide =
| "Opaque"
| ("Declare" space+ ("Morphism" | "Step") )
| ("Set" | "Unset") space+ "Printing" space+ "Coercions"
- | "Declare" space+ ("Left" | "Right") space+ "Step"
+ | "Declare" space+ ("Left" | "Right") space+ "Step"
let section = "*" | "**" | "***" | "****"
@@ -430,12 +430,12 @@ rule coq_bol = parse
| space* nl+
{ if not (!in_proof <> None && (!Cdglobals.gallina || !Cdglobals.light)) then Output.empty_line_of_code (); coq_bol lexbuf }
| space* "(**" space_nl
- { Output.end_coq (); Output.start_doc ();
+ { Output.end_coq (); Output.start_doc ();
let eol = doc_bol lexbuf in
- Output.end_doc (); Output.start_coq ();
+ Output.end_doc (); Output.start_coq ();
if eol then coq_bol lexbuf else coq lexbuf }
| space* "Comments" space_nl
- { Output.end_coq (); Output.start_doc (); comments lexbuf; Output.end_doc ();
+ { Output.end_coq (); Output.start_doc (); comments lexbuf; Output.end_doc ();
Output.start_coq (); coq lexbuf }
| space* begin_hide
{ skip_hide lexbuf; coq_bol lexbuf }
@@ -445,63 +445,63 @@ rule coq_bol = parse
{ end_show (); coq_bol lexbuf }
| space* gallina_kw_to_hide
{ let s = lexeme lexbuf in
- if !Cdglobals.light && section_or_end s then
+ if !Cdglobals.light && section_or_end s then
let eol = skip_to_dot lexbuf in
if eol then (coq_bol lexbuf) else coq lexbuf
- else
+ else
begin
let nbsp,isp = count_spaces s in
- Output.indentation nbsp;
+ Output.indentation nbsp;
let s = String.sub s isp (String.length s - isp) in
- Output.ident s (lexeme_start lexbuf + isp);
- let eol = body lexbuf in
+ Output.ident s (lexeme_start lexbuf + isp);
+ let eol = body lexbuf in
if eol then coq_bol lexbuf else coq lexbuf
end }
| space* thm_token
- { let s = lexeme lexbuf in
+ { let s = lexeme lexbuf in
let nbsp,isp = count_spaces s in
let s = String.sub s isp (String.length s - isp) in
Output.indentation nbsp;
- Output.ident s (lexeme_start lexbuf + isp);
+ Output.ident s (lexeme_start lexbuf + isp);
let eol = body lexbuf in
in_proof := Some eol;
if eol then coq_bol lexbuf else coq lexbuf }
| space* prf_token
{ in_proof := Some true;
- let eol =
- if not !Cdglobals.gallina then
- begin backtrack lexbuf; body_bol lexbuf end
- else
+ let eol =
+ if not !Cdglobals.gallina then
+ begin backtrack lexbuf; body_bol lexbuf end
+ else
let s = lexeme lexbuf in
if s.[String.length s - 1] = '.' then false
else skip_to_dot lexbuf
in if eol then coq_bol lexbuf else coq lexbuf }
- | space* end_kw {
- let eol =
- if not (!in_proof <> None && !Cdglobals.gallina) then
- begin backtrack lexbuf; body_bol lexbuf end
+ | space* end_kw {
+ let eol =
+ if not (!in_proof <> None && !Cdglobals.gallina) then
+ begin backtrack lexbuf; body_bol lexbuf end
else skip_to_dot lexbuf
in
in_proof := None;
if eol then coq_bol lexbuf else coq lexbuf }
| space* gallina_kw
- {
+ {
in_proof := None;
- let s = lexeme lexbuf in
+ let s = lexeme lexbuf in
let nbsp,isp = count_spaces s in
let s = String.sub s isp (String.length s - isp) in
Output.indentation nbsp;
- Output.ident s (lexeme_start lexbuf + isp);
+ Output.ident s (lexeme_start lexbuf + isp);
let eol= body lexbuf in
if eol then coq_bol lexbuf else coq lexbuf }
| space* prog_kw
- {
+ {
in_proof := None;
- let s = lexeme lexbuf in
+ let s = lexeme lexbuf in
let nbsp,isp = count_spaces s in
Output.indentation nbsp;
let s = String.sub s isp (String.length s - isp) in
- Output.ident s (lexeme_start lexbuf + isp);
+ Output.ident s (lexeme_start lexbuf + isp);
let eol= body lexbuf in
if eol then coq_bol lexbuf else coq lexbuf }
@@ -511,56 +511,56 @@ rule coq_bol = parse
add_printing_token tok s;
coq_bol lexbuf }
| space* "(**" space+ "printing" space+
- { eprintf "warning: bad 'printing' command at character %d\n"
+ { eprintf "warning: bad 'printing' command at character %d\n"
(lexeme_start lexbuf); flush stderr;
comment_level := 1;
ignore (comment lexbuf);
coq_bol lexbuf }
- | space* "(**" space+ "remove" space+ "printing" space+
+ | space* "(**" space+ "remove" space+ "printing" space+
(identifier | token) space* "*)"
{ remove_printing_token (lexeme lexbuf);
coq_bol lexbuf }
| space* "(**" space+ "remove" space+ "printing" space+
- { eprintf "warning: bad 'remove printing' command at character %d\n"
+ { eprintf "warning: bad 'remove printing' command at character %d\n"
(lexeme_start lexbuf); flush stderr;
comment_level := 1;
ignore (comment lexbuf);
coq_bol lexbuf }
| space* "(*"
- { comment_level := 1;
+ { comment_level := 1;
if !Cdglobals.parse_comments then begin
- let s = lexeme lexbuf in
+ let s = lexeme lexbuf in
let nbsp,isp = count_spaces s in
Output.indentation nbsp;
Output.start_comment ();
end;
let eol = comment lexbuf in
if eol then coq_bol lexbuf else coq lexbuf }
- | eof
+ | eof
{ () }
| _
- { let eol =
- if not !Cdglobals.gallina then
- begin backtrack lexbuf; body_bol lexbuf end
- else
- skip_to_dot lexbuf
+ { let eol =
+ if not !Cdglobals.gallina then
+ begin backtrack lexbuf; 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
- | nl
+ | nl
{ if not (!in_proof <> None && !Cdglobals.gallina) then Output.line_break(); coq_bol lexbuf }
| "(**" space_nl
- { Output.end_coq (); Output.start_doc ();
+ { Output.end_coq (); Output.start_doc ();
let eol = doc_bol lexbuf in
- Output.end_doc (); Output.start_coq ();
+ Output.end_doc (); Output.start_coq ();
if eol then coq_bol lexbuf else coq lexbuf }
| "(*"
{ comment_level := 1;
if !Cdglobals.parse_comments then begin
- let s = lexeme lexbuf in
+ let s = lexeme lexbuf in
let nbsp,isp = count_spaces s in
Output.indentation nbsp;
Output.start_comment ();
@@ -571,66 +571,66 @@ and coq = parse
}
| nl+ space* "]]"
{ if not !formatted then begin symbol lexbuf (lexeme lexbuf); coq lexbuf end }
- | eof
+ | eof
{ () }
| gallina_kw_to_hide
{ let s = lexeme lexbuf in
- if !Cdglobals.light && section_or_end s then
- begin
+ if !Cdglobals.light && section_or_end s then
+ begin
let eol = skip_to_dot lexbuf in
- if eol then coq_bol lexbuf else coq lexbuf
- end
- else
+ if eol then coq_bol lexbuf else coq lexbuf
+ end
+ else
begin
- Output.ident s (lexeme_start lexbuf);
- let eol=body lexbuf in
+ Output.ident s (lexeme_start lexbuf);
+ let eol=body lexbuf in
if eol then coq_bol lexbuf else coq lexbuf
end }
| prf_token
- { let eol =
- if not !Cdglobals.gallina then
- begin backtrack lexbuf; body_bol lexbuf end
- else
+ { let eol =
+ if not !Cdglobals.gallina then
+ begin backtrack lexbuf; body_bol lexbuf end
+ else
let s = lexeme lexbuf in
- let eol =
+ let eol =
if s.[String.length s - 1] = '.' then false
else skip_to_dot lexbuf
in
eol
in if eol then coq_bol lexbuf else coq lexbuf }
- | end_kw {
- let eol =
- if not !Cdglobals.gallina then
- begin backtrack lexbuf; body lexbuf end
- else
+ | end_kw {
+ let eol =
+ if not !Cdglobals.gallina then
+ begin backtrack lexbuf; body lexbuf end
+ else
let eol = skip_to_dot lexbuf in
- if !in_proof <> Some true && eol then
+ if !in_proof <> Some true && eol then
Output.line_break ();
eol
in
in_proof := None;
if eol then coq_bol lexbuf else coq lexbuf }
| gallina_kw
- { let s = lexeme lexbuf in
- Output.ident s (lexeme_start lexbuf);
+ { let s = lexeme lexbuf in
+ Output.ident s (lexeme_start lexbuf);
let eol = body lexbuf in
if eol then coq_bol lexbuf else coq lexbuf }
| prog_kw
- { let s = lexeme lexbuf in
- Output.ident s (lexeme_start lexbuf);
+ { let s = lexeme lexbuf in
+ Output.ident s (lexeme_start lexbuf);
let eol = body lexbuf in
if eol then coq_bol lexbuf else coq lexbuf }
| space+ { Output.char ' '; coq lexbuf }
- | eof
+ | eof
{ () }
- | _ { let eol =
- if not !Cdglobals.gallina then
- begin backtrack lexbuf; body lexbuf end
- else
+ | _ { let eol =
+ if not !Cdglobals.gallina then
+ begin backtrack lexbuf; body lexbuf end
+ else
skip_to_dot lexbuf
- in
+ in
if eol then coq_bol lexbuf else coq lexbuf}
-
+
(*s Scanning documentation, at beginning of line *)
and doc_bol = parse
@@ -650,7 +650,7 @@ and doc_bol = parse
production and the begin list production fire eliminates
extra vertical whitespace. *)
let buf' = lexeme lexbuf in
- let buf =
+ let buf =
let bufs = Str.split_delim (Str.regexp "['\n']") buf' in
match bufs with
| (_ :: s :: []) -> s
@@ -672,12 +672,12 @@ and doc_bol = parse
}
| "<<" space*
{ Output.start_verbatim (); verbatim lexbuf; doc_bol lexbuf }
- | eof
+ | eof
{ true }
| '_'
- { Output.start_emph ();
+ { Output.start_emph ();
doc None lexbuf }
- | _
+ | _
{ backtrack lexbuf; doc None lexbuf }
(*s Scanning lists - using whitespace *)
@@ -687,7 +687,7 @@ and doc_list_bol indents = parse
match find_level indents n_spaces with
| Before -> backtrack lexbuf; doc_bol lexbuf
| StartLevel n -> Output.item n; doc (Some (take n indents)) lexbuf
- | InLevel (n,true) ->
+ | InLevel (n,true) ->
let items = List.length indents in
Output.item (items+1);
doc (Some (List.append indents [n_spaces])) lexbuf
@@ -695,13 +695,13 @@ and doc_list_bol indents = parse
backtrack lexbuf; doc_bol lexbuf
}
| "<<" space*
- { Output.start_verbatim ();
- verbatim lexbuf;
+ { Output.start_verbatim ();
+ verbatim lexbuf;
doc_list_bol indents lexbuf }
| "[[" nl
{ formatted := true;
Output.paragraph ();
- Output.start_inline_coq ();
+ Output.start_inline_coq ();
ignore(body_bol lexbuf);
Output.end_inline_coq ();
formatted := false;
@@ -714,7 +714,7 @@ and doc_list_bol indents = parse
doc_list_bol indents lexbuf }
| space* nl space* _
{ let buf' = lexeme lexbuf in
- let buf =
+ let buf =
let bufs = Str.split_delim (Str.regexp "['\n']") buf' in
match bufs with
| (_ :: s :: []) -> s
@@ -723,7 +723,7 @@ and doc_list_bol indents = parse
exit 1
in
let (n_spaces,_) = count_spaces buf in
- match find_level indents n_spaces with
+ match find_level indents n_spaces with
| InLevel _ ->
Output.paragraph ();
backtrack_past_newline lexbuf;
@@ -741,15 +741,15 @@ and doc_list_bol indents = parse
backtrack_past_newline lexbuf;
doc_list_bol indents lexbuf
end
- | Before -> Output.stop_item ();
- backtrack_past_newline lexbuf;
+ | Before -> Output.stop_item ();
+ backtrack_past_newline lexbuf;
doc_bol lexbuf
}
- | space* _
+ | space* _
{ let (n_spaces,_) = count_spaces (lexeme lexbuf) in
- match find_level indents n_spaces with
- | Before -> Output.stop_item (); backtrack lexbuf;
+ match find_level indents n_spaces with
+ | Before -> Output.stop_item (); backtrack lexbuf;
doc_bol lexbuf
| StartLevel n ->
Output.reach_item_level (n-1);
@@ -764,20 +764,20 @@ and doc_list_bol indents = parse
(*s Scanning documentation elsewhere *)
and doc indents = parse
| nl
- { Output.char '\n';
- match indents with
- | Some ls -> doc_list_bol ls lexbuf
+ { Output.char '\n';
+ match indents with
+ | Some ls -> doc_list_bol ls lexbuf
| None -> doc_bol lexbuf }
| "[[" nl
{ if !Cdglobals.plain_comments
then (Output.char '['; Output.char '['; doc indents lexbuf)
- else (formatted := true;
+ else (formatted := true;
Output.line_break (); Output.start_inline_coq ();
- let eol = body_bol lexbuf in
+ let eol = body_bol lexbuf in
Output.end_inline_coq (); formatted := false;
if eol then
- match indents with
- | Some ls -> doc_list_bol ls lexbuf
+ match indents with
+ | Some ls -> doc_list_bol ls lexbuf
| None -> doc_bol lexbuf
else doc indents lexbuf)}
| "[]"
@@ -804,7 +804,7 @@ and doc indents = parse
else (Output.start_latex_math (); escaped_math_latex lexbuf);
doc indents lexbuf }
| "$$"
- { if !Cdglobals.plain_comments then Output.char '$';
+ { if !Cdglobals.plain_comments then Output.char '$';
Output.char '$'; doc indents lexbuf }
| "%"
{ if !Cdglobals.plain_comments then Output.char '%'
@@ -822,16 +822,16 @@ and doc indents = parse
{ List.iter (fun x -> Output.char (lexeme_char lexbuf x)) [0;1;2];
doc indents lexbuf}
| nonidentchar '_'
- { Output.char (lexeme_char lexbuf 0);
- Output.start_emph ();
+ { Output.char (lexeme_char lexbuf 0);
+ Output.start_emph ();
doc indents lexbuf }
| '_' nonidentchar
- { Output.stop_emph ();
+ { Output.stop_emph ();
Output.char (lexeme_char lexbuf 1);
doc indents lexbuf }
- | eof
+ | eof
{ false }
- | _
+ | _
{ Output.char (lexeme_char lexbuf 0); doc indents lexbuf }
(*s Various escapings *)
@@ -865,7 +865,7 @@ and verbatim = parse
and escaped_coq = parse
| "]"
- { decr brackets;
+ { decr brackets;
if !brackets > 0 then begin Output.char ']'; escaped_coq lexbuf end }
| "["
{ incr brackets; Output.char '['; escaped_coq lexbuf }
@@ -880,15 +880,15 @@ and escaped_coq = parse
symbol lexbuf s; escaped_coq lexbuf }
| (identifier '.')* identifier
{ Output.ident (lexeme lexbuf) (lexeme_start lexbuf); escaped_coq lexbuf }
- | _
+ | _
{ Output.char (lexeme_char lexbuf 0); escaped_coq lexbuf }
(*s Coq "Comments" command. *)
and comments = parse
- | space_nl+
+ | space_nl+
{ Output.char ' '; comments lexbuf }
- | '"' [^ '"']* '"'
+ | '"' [^ '"']* '"'
{ let s = lexeme lexbuf in
let s = String.sub s 1 (String.length s - 2) in
ignore (doc None (from_string s)); comments lexbuf }
@@ -896,9 +896,9 @@ and comments = parse
{ escaped_coq (from_string (lexeme lexbuf)); comments lexbuf }
| "." (space_nl | eof)
{ () }
- | eof
+ | eof
{ () }
- | _
+ | _
{ Output.char (lexeme_char lexbuf 0); comments lexbuf }
(*s Skip comments *)
@@ -908,10 +908,10 @@ and comment = parse
if !Cdglobals.parse_comments then Output.start_comment ();
comment lexbuf }
| "*)" space* nl {
- if !Cdglobals.parse_comments then
+ if !Cdglobals.parse_comments then
(Output.end_comment (); Output.line_break ());
decr comment_level; if !comment_level > 0 then comment lexbuf else true }
- | "*)" {
+ | "*)" {
if !Cdglobals.parse_comments then (Output.end_comment ());
decr comment_level; if !comment_level > 0 then comment lexbuf else false }
| "[" {
@@ -934,18 +934,18 @@ and comment = parse
else (Output.start_latex_math (); escaped_math_latex lexbuf);
comment lexbuf }
| "$$"
- { if !Cdglobals.parse_comments
- then
+ { if !Cdglobals.parse_comments
+ then
(if !Cdglobals.plain_comments then Output.char '$'; Output.char '$');
doc None lexbuf }
| "%"
{ if !Cdglobals.parse_comments
- then
+ then
if !Cdglobals.plain_comments then Output.char '%'
else escaped_latex lexbuf; comment lexbuf }
| "%%"
- { if !Cdglobals.parse_comments
- then
+ { if !Cdglobals.parse_comments
+ then
(if !Cdglobals.plain_comments then Output.char '%'; Output.char '%');
comment lexbuf }
| "#"
@@ -954,8 +954,8 @@ and comment = parse
if !Cdglobals.plain_comments then Output.char '$'
else escaped_html lexbuf; comment lexbuf }
| "##"
- { if !Cdglobals.parse_comments
- then
+ { if !Cdglobals.parse_comments
+ then
(if !Cdglobals.plain_comments then Output.char '#'; Output.char '#');
comment lexbuf }
| eof { false }
@@ -966,7 +966,7 @@ and comment = parse
then Output.line_break (); comment lexbuf }
| _ { if !Cdglobals.parse_comments then Output.char (lexeme_char lexbuf 0);
comment lexbuf }
-
+
and skip_to_dot = parse
| '.' space* nl { true }
| eof | '.' space+ { false }
@@ -981,68 +981,68 @@ and body_bol = parse
and body = parse
| nl {Output.line_break(); body_bol lexbuf}
| nl+ space* "]]" space* nl
- { if not !formatted then
- begin
- symbol lexbuf (lexeme lexbuf);
- body lexbuf
- end
- else
+ { if not !formatted then
+ begin
+ symbol lexbuf (lexeme lexbuf);
+ body lexbuf
+ end
+ else
begin
Output.paragraph ();
true
end }
| "]]" space* nl
- { if not !formatted then
- begin
- symbol lexbuf (lexeme lexbuf);
- body lexbuf
- end
- else
+ { if not !formatted then
+ begin
+ symbol lexbuf (lexeme lexbuf);
+ body lexbuf
+ end
+ else
begin
Output.paragraph ();
true
end }
| eof { false }
- | '.' space* nl | '.' space* eof
- { Output.char '.'; Output.line_break();
- if not !formatted then true else body_bol lexbuf }
+ | '.' space* nl | '.' space* eof
+ { Output.char '.'; Output.line_break();
+ if not !formatted then true else body_bol lexbuf }
| '.' space* nl "]]" space* nl
{ Output.char '.';
if not !formatted then
begin
- eprintf "Error: stray ]] at %d\n" (lexeme_start lexbuf);
+ eprintf "Error: stray ]] at %d\n" (lexeme_start lexbuf);
flush stderr;
exit 1
end
- else
+ else
begin
Output.paragraph ();
true
end
}
- | '.' space+ { Output.char '.'; Output.char ' ';
+ | '.' space+ { Output.char '.'; Output.char ' ';
if not !formatted then false else body lexbuf }
| '"' { Output.char '"'; ignore(notation lexbuf); body lexbuf }
| "(**" space_nl
- { Output.end_coq (); Output.start_doc ();
+ { Output.end_coq (); Output.start_doc ();
let eol = doc_bol lexbuf in
- Output.end_doc (); Output.start_coq ();
+ Output.end_doc (); Output.start_coq ();
if eol then body_bol lexbuf else body lexbuf }
- | "(*" { comment_level := 1;
+ | "(*" { comment_level := 1;
if !Cdglobals.parse_comments then Output.start_comment ();
- let eol = comment lexbuf in
- if eol
+ let eol = comment lexbuf in
+ if eol
then begin if not !Cdglobals.parse_comments then Output.line_break(); body_bol lexbuf end
else body lexbuf }
- | identifier
- { let s = lexeme lexbuf in
- Output.ident s (lexeme_start lexbuf);
+ | identifier
+ { let s = lexeme lexbuf in
+ Output.ident s (lexeme_start lexbuf);
body lexbuf }
| token_no_brackets
{ let s = lexeme lexbuf in
symbol lexbuf s; body lexbuf }
- | _ { let c = lexeme_char lexbuf 0 in
- Output.char c;
+ | _ { let c = lexeme_char lexbuf 0 in
+ Output.char c;
body lexbuf }
and notation_bol = parse
@@ -1056,8 +1056,8 @@ and notation = parse
| token
{ let s = lexeme lexbuf in
symbol lexbuf s; notation lexbuf }
- | _ { let c = lexeme_char lexbuf 0 in
- Output.char c;
+ | _ { let c = lexeme_char lexbuf 0 in
+ Output.char c;
notation lexbuf }
and skip_hide = parse
@@ -1067,18 +1067,18 @@ and skip_hide = parse
(*s Reading token pretty-print *)
and printing_token_body = parse
- | "*)" nl? | eof
- { let s = Buffer.contents token_buffer in
+ | "*)" nl? | eof
+ { let s = Buffer.contents token_buffer in
Buffer.clear token_buffer;
s }
- | _ { Buffer.add_string token_buffer (lexeme lexbuf);
+ | _ { Buffer.add_string token_buffer (lexeme lexbuf);
printing_token_body lexbuf }
(*s A small scanner to support the chapter subtitle feature *)
and st_start m = parse
| "(*" "*"+ space+ "*" space+
{ st_modname m lexbuf }
- | _
+ | _
{ None }
and st_modname m = parse
@@ -1088,20 +1088,20 @@ and st_modname m = parse
else
None
}
- | _
+ | _
{ None }
and st_subtitle = parse
| [^ '\n']* '\n'
{ let st = lexeme lexbuf in
- let i = try Str.search_forward (Str.regexp "\\**)") st 0 with
- Not_found ->
+ let i = try Str.search_forward (Str.regexp "\\**)") st 0 with
+ Not_found ->
(eprintf "unterminated comment at beginning of file\n";
exit 1)
in
Some (cut_head_tail_spaces (String.sub st 0 i))
}
- | _
+ | _
{ None }
(*s Applying the scanners to files *)
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index bfb57dad2..f8a8730d0 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -12,7 +12,7 @@ open Cdglobals
type loc = int
-type entry_type =
+type entry_type =
| Library
| Module
| Definition
@@ -33,7 +33,7 @@ type entry_type =
val type_name : entry_type -> string
-type index_entry =
+type index_entry =
| Def of string * entry_type
| Ref of coq_module * string * entry_type
| Mod of coq_module * string
@@ -58,14 +58,14 @@ val read_glob : string -> coq_module
(*s Indexes *)
-type 'a index = {
+type 'a index = {
idx_name : string;
idx_entries : (char * (string * 'a) list) list;
idx_size : int }
val current_library : string ref
-val all_entries : unit ->
+val all_entries : unit ->
(coq_module * entry_type) index *
(entry_type * coq_module index) list
diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
index 62ae42c1a..a39450986 100644
--- a/tools/coqdoc/index.mll
+++ b/tools/coqdoc/index.mll
@@ -12,14 +12,14 @@
{
open Filename
-open Lexing
+open Lexing
open Printf
open Cdglobals
type loc = int
-type entry_type =
+type entry_type =
| Library
| Module
| Definition
@@ -38,7 +38,7 @@ type entry_type =
| Notation
| Section
-type index_entry =
+type index_entry =
| Def of string * entry_type
| Ref of coq_module * string * entry_type
| Mod of coq_module * string
@@ -47,45 +47,45 @@ let current_type : entry_type ref = ref Library
let current_library = ref ""
(** refers to the file being parsed *)
-(** [deftable] stores only definitions and is used to interpolate idents
+(** [deftable] stores only definitions and is used to interpolate idents
inside comments, which are not globalized otherwise. *)
let deftable = Hashtbl.create 97
(** [reftable] stores references and definitions *)
let reftable = Hashtbl.create 97
-
+
let full_ident sp id =
- if sp <> "<>" then
- if id <> "<>" then
- sp ^ "." ^ id
- else sp
- else if id <> "<>"
- then id
+ if sp <> "<>" then
+ if id <> "<>" then
+ sp ^ "." ^ id
+ else sp
+ else if id <> "<>"
+ then id
else ""
-
-let add_def loc ty sp id =
+
+let add_def loc ty sp id =
Hashtbl.add reftable (!current_library, loc) (Def (full_ident sp id, ty));
Hashtbl.add deftable id (Ref (!current_library, full_ident sp id, ty))
-
-let add_ref m loc m' sp id ty =
+
+let add_ref m loc m' sp id ty =
if Hashtbl.mem reftable (m, loc) then ()
else Hashtbl.add reftable (m, loc) (Ref (m', full_ident sp id, ty));
let idx = if id = "<>" then m' else id in
if Hashtbl.mem deftable idx then ()
- else Hashtbl.add deftable idx (Ref (m', full_ident sp id, ty))
-
-let add_mod m loc m' id =
+ else Hashtbl.add deftable idx (Ref (m', full_ident sp id, ty))
+
+let add_mod m loc m' id =
Hashtbl.add reftable (m, loc) (Mod (m', id));
Hashtbl.add deftable m (Mod (m', id))
-
+
let find m l = Hashtbl.find reftable (m, l)
-
+
let find_string m s = Hashtbl.find deftable s
-
-(*s Manipulating path prefixes *)
-type stack = string list
+(*s Manipulating path prefixes *)
+
+type stack = string list
let rec string_of_stack st =
match st with
@@ -102,11 +102,11 @@ let init_stack () =
module_stack := empty_stack; section_stack := empty_stack
let push st p = st := p::!st
-let pop st =
- match !st with
+let pop st =
+ match !st with
| [] -> ()
| _::tl -> st := tl
-
+
let head st =
match st with
| [] -> ""
@@ -124,22 +124,22 @@ let end_block id =
else
()
-let make_fullid id =
+let make_fullid id =
(** prepends the current module path to an id *)
let path = string_of_stack !module_stack in
if String.length path > 0 then
path ^ "." ^ id
- else
+ else
id
(* Coq modules *)
-let split_sp s =
+let split_sp s =
try
let i = String.rindex s '.' in
String.sub s 0 i, String.sub s (i + 1) (String.length s - i - 1)
- with
+ with
Not_found -> "", s
let modules = Hashtbl.create 97
@@ -155,7 +155,7 @@ type module_kind = Local | Coqlib | Unknown
let coq_module m = String.length m >= 4 && String.sub m 0 4 = "Coq."
let find_module m =
- if Hashtbl.mem local_modules m then
+ if Hashtbl.mem local_modules m then
Local
else if coq_module m then
Coqlib
@@ -165,42 +165,42 @@ let find_module m =
(* Building indexes *)
-type 'a index = {
+type 'a index = {
idx_name : string;
idx_entries : (char * (string * 'a) list) list;
idx_size : int }
-
-let map f i =
- { i with idx_entries =
- List.map
- (fun (c,l) -> (c, List.map (fun (s,x) -> (s,f s x)) l))
+
+let map f i =
+ { i with idx_entries =
+ List.map
+ (fun (c,l) -> (c, List.map (fun (s,x) -> (s,f s x)) l))
i.idx_entries }
let compare_entries (s1,_) (s2,_) = Alpha.compare_string s1 s2
let sort_entries el =
let t = Hashtbl.create 97 in
- List.iter
+ List.iter
(fun c -> Hashtbl.add t c [])
- ['A'; 'B'; 'C'; 'D'; 'E'; 'F'; 'G'; 'H'; 'I'; 'J'; 'K'; 'L'; 'M'; 'N';
- 'O'; 'P'; 'Q'; 'R'; 'S'; 'T'; 'U'; 'V'; 'W'; 'X'; 'Y'; 'Z'; '_'];
- List.iter
- (fun ((s,_) as e) ->
- let c = Alpha.norm_char s.[0] in
+ ['A'; 'B'; 'C'; 'D'; 'E'; 'F'; 'G'; 'H'; 'I'; 'J'; 'K'; 'L'; 'M'; 'N';
+ 'O'; 'P'; 'Q'; 'R'; 'S'; 'T'; 'U'; 'V'; 'W'; 'X'; 'Y'; 'Z'; '_'];
+ List.iter
+ (fun ((s,_) as e) ->
+ let c = Alpha.norm_char s.[0] in
let l = try Hashtbl.find t c with Not_found -> [] in
- Hashtbl.replace t c (e :: l))
+ Hashtbl.replace t c (e :: l))
el;
let res = ref [] in
- Hashtbl.iter
+ Hashtbl.iter
(fun c l -> res := (c, List.sort compare_entries l) :: !res) t;
List.sort (fun (c1,_) (c2,_) -> Alpha.compare_char c1 c2) !res
-
+
let index_size = List.fold_left (fun s (_,l) -> s + List.length l) 0
-
+
let hashtbl_elements h = Hashtbl.fold (fun x y l -> (x,y)::l) h []
-
+
let type_name = function
- | Library ->
+ | Library ->
let ln = !lib_name in
if ln <> "" then String.lowercase ln else "library"
| Module -> "module"
@@ -228,31 +228,31 @@ let all_entries () =
let l = try Hashtbl.find bt t with Not_found -> [] in
Hashtbl.replace bt t ((s,m) :: l)
in
- let classify (m,_) e = match e with
+ let classify (m,_) e = match e with
| Def (s,t) -> add_g s m t; add_bt t s m
| Ref _ | Mod _ -> ()
in
Hashtbl.iter classify reftable;
Hashtbl.iter (fun id m -> add_g id m Library; add_bt Library id m) modules;
- { idx_name = "global";
- idx_entries = sort_entries !gl;
+ { idx_name = "global";
+ idx_entries = sort_entries !gl;
idx_size = List.length !gl },
- Hashtbl.fold (fun t e l -> (t, { idx_name = type_name t;
- idx_entries = sort_entries e;
+ Hashtbl.fold (fun t e l -> (t, { idx_name = type_name t;
+ idx_entries = sort_entries e;
idx_size = List.length e }) :: l) bt []
-
+
}
(*s Shortcuts for regular expressions. *)
let digit = ['0'-'9']
let num = digit+
-let space =
+let space =
[' ' '\010' '\013' '\009' '\012']
-let firstchar =
+let firstchar =
['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255']
-let identchar =
- ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255'
+let identchar =
+ ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255'
'\'' '0'-'9']
let id = firstchar identchar*
let pfx_id = (id '.')*
@@ -260,15 +260,15 @@ let ident = id | pfx_id id
let begin_hide = "(*" space* "begin" space+ "hide" space* "*)"
let end_hide = "(*" space* "end" space+ "hide" space* "*)"
-
+
(*s Indexing entry point. *)
-
+
rule traverse = parse
| ("Program" space+)? "Definition" space
{ current_type := Definition; index_ident lexbuf; traverse lexbuf }
| "Tactic" space+ "Definition" space
{ current_type := TacticDefinition; index_ident lexbuf; traverse lexbuf }
- | ("Axiom" | "Parameter") space
+ | ("Axiom" | "Parameter") space
{ current_type := Axiom; index_ident lexbuf; traverse lexbuf }
| ("Program" space+)? "Fixpoint" space
{ current_type := Definition; index_ident lexbuf; fixpoint lexbuf;
@@ -278,7 +278,7 @@ rule traverse = parse
| "Obligation" space num ("of" ident)?
{ current_type := Lemma; index_ident lexbuf; traverse lexbuf }
| "Inductive" space
- { current_type := Inductive;
+ { current_type := Inductive;
index_ident lexbuf; inductive lexbuf; traverse lexbuf }
| "Record" space
{ current_type := Inductive; index_ident lexbuf; traverse lexbuf }
@@ -288,40 +288,40 @@ rule traverse = parse
| "Variable" 's'? space
{ current_type := Variable; index_idents lexbuf; traverse lexbuf }
***i*)
- | "Require" (space+ ("Export"|"Import"))?
+ | "Require" (space+ ("Export"|"Import"))?
{ module_refs lexbuf; traverse lexbuf }
- | "End" space+
+ | "End" space+
{ end_ident lexbuf; traverse lexbuf }
- | begin_hide
+ | begin_hide
{ skip_hide lexbuf; traverse lexbuf }
- | "(*"
+ | "(*"
{ comment lexbuf; traverse lexbuf }
| '"'
{ string lexbuf; traverse lexbuf }
- | eof
+ | eof
{ () }
- | _
+ | _
{ traverse lexbuf }
(*s Index one identifier. *)
and index_ident = parse
- | space+
+ | space+
{ index_ident lexbuf }
- | ident
- { let fullid =
+ | ident
+ { let fullid =
let id = lexeme lexbuf in
match !current_type with
| Definition
| Inductive
- | Constructor
+ | Constructor
| Lemma -> make_fullid id
- | _ -> id
- in
+ | _ -> id
+ in
add_def (lexeme_start lexbuf) !current_type "" fullid }
- | eof
+ | eof
{ () }
- | _
+ | _
{ () }
(*s Index identifiers separated by blanks and/or commas. *)
@@ -329,42 +329,42 @@ and index_ident = parse
and index_idents = parse
| space+ | ','
{ index_idents lexbuf }
- | ident
+ | ident
{ add_def (lexeme_start lexbuf) !current_type "" (lexeme lexbuf);
index_idents lexbuf }
- | eof
+ | eof
{ () }
| _
{ skip_until_point lexbuf }
-
+
(*s Index identifiers in an inductive definition (types and constructors). *)
-
+
and inductive = parse
- | '|' | ":=" space* '|'?
+ | '|' | ":=" space* '|'?
{ current_type := Constructor; index_ident lexbuf; inductive lexbuf }
| "with" space
{ current_type := Inductive; index_ident lexbuf; inductive lexbuf }
- | '.'
+ | '.'
{ () }
- | eof
+ | eof
{ () }
- | _
+ | _
{ inductive lexbuf }
-
+
(*s Index identifiers in a Fixpoint declaration. *)
-
+
and fixpoint = parse
| "with" space
{ index_ident lexbuf; fixpoint lexbuf }
- | '.'
+ | '.'
{ () }
- | eof
+ | eof
{ () }
- | _
+ | _
{ fixpoint lexbuf }
-
+
(*s Skip a possibly nested comment. *)
-
+
and comment = parse
| "*)" { () }
| "(*" { comment lexbuf; comment lexbuf }
@@ -373,19 +373,19 @@ and comment = parse
| _ { comment lexbuf }
(*s Skip a constant string. *)
-
+
and string = parse
| '"' { () }
| eof { eprintf " *** Unterminated string while indexing" }
| _ { string lexbuf }
(*s Skip everything until the next dot. *)
-
+
and skip_until_point = parse
| '.' { () }
| eof { () }
| _ { skip_until_point lexbuf }
-
+
(*s Skip everything until [(* end hide *)] *)
and skip_hide = parse
@@ -393,13 +393,13 @@ and skip_hide = parse
| _ { skip_hide lexbuf }
and end_ident = parse
- | space+
+ | space+
{ end_ident lexbuf }
- | ident
+ | ident
{ let id = lexeme lexbuf in end_block id }
- | eof
+ | eof
{ () }
- | _
+ | _
{ () }
and module_ident = parse
@@ -419,19 +419,19 @@ and module_ident = parse
(*s parse module names *)
and module_refs = parse
- | space+
+ | space+
{ module_refs lexbuf }
- | ident
+ | ident
{ let id = lexeme lexbuf in
(try
add_mod !current_library (lexeme_start lexbuf) (Hashtbl.find modules id) id
with
Not_found -> ()
- );
+ );
module_refs lexbuf }
- | eof
+ | eof
{ () }
- | _
+ | _
{ () }
{
@@ -455,8 +455,8 @@ and module_refs = parse
| "tac" -> TacticDefinition
| "sec" -> Section
| s -> raise (Invalid_argument ("type_of_string:" ^ s))
-
- let read_glob f =
+
+ let read_glob f =
let c = open_in f in
let cur_mod = ref "" in
try
@@ -465,7 +465,7 @@ and module_refs = parse
let n = String.length s in
if n > 0 then begin
match s.[0] with
- | 'F' ->
+ | 'F' ->
cur_mod := String.sub s 1 (n - 1);
current_library := !cur_mod
| 'R' ->
@@ -474,16 +474,16 @@ and module_refs = parse
(fun loc lib_dp sp id ty ->
add_ref !cur_mod loc lib_dp sp id (type_of_string ty))
with _ -> ())
- | _ ->
+ | _ ->
try Scanf.sscanf s "%s %d %s %s"
(fun ty loc sp id -> add_def loc (type_of_string ty) sp id)
with Scanf.Scan_failure _ -> ()
end
done; assert false
- with End_of_file ->
+ with End_of_file ->
close_in c; !cur_mod
-
- let scan_file f m =
+
+ let scan_file f m =
init_stack (); current_library := m;
let c = open_in f in
let lb = from_channel c in
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 3c4c9a656..d2b66f993 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -54,7 +54,7 @@ let usage () =
prerr_endline " --files-from <file> read file names to process in <file>";
prerr_endline " --glob-from <file> read globalization information from <file>";
prerr_endline " --quiet quiet mode (default)";
- prerr_endline " --verbose verbose mode";
+ prerr_endline " --verbose verbose mode";
prerr_endline " --no-externals no links to Coq standard library";
prerr_endline " --coqlib <url> set URL for Coq standard library";
prerr_endline (" (default is " ^ Coq_config.wwwstdlib ^ ")");
@@ -80,20 +80,20 @@ let obsolete s =
(*s \textbf{Banner.} Always printed. Notice that it is printed on error
output, so that when the output of [coqdoc] is redirected this header
- is not (unless both standard and error outputs are redirected, of
+ is not (unless both standard and error outputs are redirected, of
course). *)
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 =
+
+let target_full_name f =
match !Cdglobals.target_language with
| HTML -> f ^ ".html"
| Raw -> f ^ ".txt"
| _ -> f ^ ".tex"
-
+
(*s \textbf{Separation of files.} Files given on the command line are
separated according to their type, which is determined by their
suffix. Coq files have suffixe \verb!.v! or \verb!.g! and \LaTeX\
@@ -106,7 +106,7 @@ let check_if_file_exists f =
end
-(*s Manipulations of paths and path aliases *)
+(*s Manipulations of paths and path aliases *)
let normalize_path p =
(* We use the Unix subsystem to normalize a physical path (relative
@@ -117,7 +117,7 @@ let normalize_path p =
let orig = Sys.getcwd () in
Sys.chdir p;
let res = Sys.getcwd () in
- Sys.chdir orig;
+ Sys.chdir orig;
res
let normalize_filename f =
@@ -127,22 +127,22 @@ let normalize_filename f =
(* [paths] maps a physical path to a name *)
let paths = ref []
-
-let add_path dir name =
+
+let add_path dir name =
(* if dir is relative we add both the relative and absolute name *)
let p = normalize_path dir in
paths := (p,name) :: !paths
-
+
(* turn A/B/C into A.B.C *)
let name_of_path = Str.global_replace (Str.regexp "/") ".";;
-let coq_module filename =
+let coq_module filename =
let bfname = Filename.chop_extension filename in
let nfname = normalize_filename bfname in
- let rec change_prefix map f =
+ let rec change_prefix map f =
match map with
- | [] ->
- (* There is no prefix alias;
+ | [] ->
+ (* There is no prefix alias;
we just cut the name wrt current working directory *)
let cwd = Sys.getcwd () in
let exp = Str.regexp (Str.quote (cwd ^ "/")) in
@@ -166,10 +166,10 @@ let what_file f =
Vernac_file (f, coq_module f)
else if Filename.check_suffix f ".tex" then
Latex_file f
- else
+ else
(eprintf "\ncoqdoc: don't know what to do with %s\n" f; exit 1)
-
-(*s \textbf{Reading file names from a file.}
+
+(*s \textbf{Reading file names from a file.}
* File names may be given
* in a file instead of being given on the command
* line. [(files_from_file f)] returns the list of file names contained
@@ -187,7 +187,7 @@ let files_from_file f =
| ' ' | '\t' | '\n' ->
if Buffer.length buf > 0 then l := (Buffer.contents buf) :: !l;
Buffer.clear buf
- | c ->
+ | c ->
Buffer.add_char buf c
done; []
with End_of_file ->
@@ -202,9 +202,9 @@ let files_from_file f =
eprintf "\ncoqdoc: cannot read from file %s (%s)\n" f s;
exit 1
end
-
+
(*s \textbf{Parsing of the command line.} *)
-
+
let dvi = ref false
let ps = ref false
let pdf = ref false
@@ -214,7 +214,7 @@ let parse () =
let add_file f = files := f :: !files in
let rec parse_rec = function
| [] -> ()
-
+
| ("-nopreamble" | "--nopreamble" | "--no-preamble"
| "-bodyonly" | "--bodyonly" | "--body-only") :: rem ->
header_trailer := false; parse_rec rem
@@ -244,11 +244,11 @@ let parse () =
out_to := StdOut; parse_rec rem
| ("-o" | "--output") :: f :: rem ->
out_to := File (Filename.basename f); output_dir := Filename.dirname f; parse_rec rem
- | ("-o" | "--output") :: [] ->
+ | ("-o" | "--output") :: [] ->
usage ()
| ("-d" | "--directory") :: dir :: rem ->
output_dir := dir; parse_rec rem
- | ("-d" | "--directory") :: [] ->
+ | ("-d" | "--directory") :: [] ->
usage ()
| ("-s" | "--short") :: rem ->
short := true; parse_rec rem
@@ -293,8 +293,8 @@ let parse () =
| ("-toc-depth" | "--toc-depth") :: [] ->
usage ()
| ("-toc-depth" | "--toc-depth") :: ds :: rem ->
- let d = try int_of_string ds with
- Failure _ ->
+ let d = try int_of_string ds with
+ Failure _ ->
(eprintf "--toc-depth must be followed by an integer";
exit 1)
in
@@ -314,32 +314,32 @@ let parse () =
Cdglobals.set_latin1 (); parse_rec rem
| ("-utf8" | "--utf8") :: rem ->
Cdglobals.set_utf8 (); parse_rec rem
-
+
| ("-q" | "-quiet" | "--quiet") :: rem ->
quiet := true; parse_rec rem
| ("-v" | "-verbose" | "--verbose") :: rem ->
quiet := false; parse_rec rem
-
+
| ("-h" | "-help" | "-?" | "--help") :: rem ->
banner (); usage ()
| ("-V" | "-version" | "--version") :: _ ->
banner (); exit 0
- | ("-vernac-file" | "--vernac-file") :: f :: rem ->
+ | ("-vernac-file" | "--vernac-file") :: f :: rem ->
check_if_file_exists f;
add_file (Vernac_file (f, coq_module f)); parse_rec rem
| ("-vernac-file" | "--vernac-file") :: [] ->
usage ()
- | ("-tex-file" | "--tex-file") :: f :: rem ->
+ | ("-tex-file" | "--tex-file") :: f :: rem ->
add_file (Latex_file f); parse_rec rem
| ("-tex-file" | "--tex-file") :: [] ->
usage ()
| ("-files" | "--files" | "--files-from") :: f :: rem ->
- List.iter (fun f -> add_file (what_file f)) (files_from_file f);
+ List.iter (fun f -> add_file (what_file f)) (files_from_file f);
parse_rec rem
| ("-files" | "--files") :: [] ->
usage ()
- | "-R" :: path :: log :: rem ->
+ | "-R" :: path :: log :: rem ->
add_path path log; parse_rec rem
| "-R" :: ([] | [_]) ->
usage ()
@@ -359,16 +359,16 @@ let parse () =
Cdglobals.coqlib_path := d; parse_rec rem
| ("--coqlib_path" | "-coqlib_path") :: [] ->
usage ()
- | f :: rem ->
+ | f :: rem ->
add_file (what_file f); parse_rec rem
- in
+ in
parse_rec (List.tl (Array.to_list Sys.argv));
Output.initialize ();
List.rev !files
-
+
(*s The following function produces the output. The default output is
- the \LaTeX\ document: in that case, we just call [Web.produce_document].
+ the \LaTeX\ document: in that case, we just call [Web.produce_document].
If option \verb!-dvi!, \verb!-ps! or \verb!-html! is invoked, then
we make calls to \verb!latex! or \verb!dvips! or \verb!pdflatex! accordingly. *)
@@ -390,9 +390,9 @@ let clean_temp_files basefile =
remove (basefile ^ ".pdf");
remove (basefile ^ ".haux");
remove (basefile ^ ".html")
-
+
let clean_and_exit file res = clean_temp_files file; exit res
-
+
let cat file =
let c = open_in file in
try
@@ -401,7 +401,7 @@ let cat file =
close_in c
let copy src dst =
- let cin = open_in src
+ let cin = open_in src
and cout = open_out dst in
try
while true do Pervasives.output_char cout (input_char cin) done
@@ -413,7 +413,7 @@ let copy src dst =
let gen_one_file l =
let file = function
- | Vernac_file (f,m) ->
+ | Vernac_file (f,m) ->
let sub = if !lib_subtitles then Cpretty.detect_subtitle f m else None in
Output.set_module m sub;
Cpretty.coq_file f m
@@ -424,57 +424,57 @@ let gen_one_file l =
List.iter file l;
if !index then Output.make_index();
if (!header_trailer) then Output.trailer ()
-
+
let gen_mult_files l =
let file = function
- | Vernac_file (f,m) ->
+ | Vernac_file (f,m) ->
let sub = if !lib_subtitles then Cpretty.detect_subtitle f m else None in
let hf = target_full_name m in
Output.set_module m sub;
open_out_file hf;
- if (!header_trailer) then Output.header ();
- Cpretty.coq_file f m;
+ if (!header_trailer) then Output.header ();
+ Cpretty.coq_file f m;
if (!header_trailer) then Output.trailer ();
close_out_file()
| Latex_file _ -> ()
in
List.iter file l;
if (!index && !target_language=HTML) then begin
- if (!multi_index) then Output.make_multi_index ();
- open_out_file (!index_name^".html");
+ if (!multi_index) then Output.make_multi_index ();
+ open_out_file (!index_name^".html");
page_title := (if !title <> "" then !title else "Index");
- if (!header_trailer) then Output.header ();
- Output.make_index ();
+ if (!header_trailer) then Output.header ();
+ Output.make_index ();
if (!header_trailer) then Output.trailer ();
close_out_file()
end;
if (!toc && !target_language=HTML) then begin
- open_out_file "toc.html";
+ open_out_file "toc.html";
page_title := (if !title <> "" then !title else "Table of contents");
if (!header_trailer) then Output.header ();
if !title <> "" then printf "<h1>%s</h1>\n" !title;
- Output.make_toc ();
+ Output.make_toc ();
if (!header_trailer) then Output.trailer ();
close_out_file()
- end
+ end
(* Rq: pour latex et texmacs, une toc ou un index séparé n'a pas de sens... *)
let read_glob x =
match x with
- | Vernac_file (f,m) ->
+ | Vernac_file (f,m) ->
let glob = (Filename.chop_extension f) ^ ".glob" in
(try
Vernac_file (f, Index.read_glob glob)
- with e ->
+ with e ->
eprintf "Warning: file %s cannot be used; links will not be available: %s\n" glob (Printexc.to_string e);
x)
| Latex_file _ -> x
let index_module = function
- | Vernac_file (f,m) ->
+ | Vernac_file (f,m) ->
Index.add_module m
| Latex_file _ -> ()
-
+
let produce_document l =
(if !target_language=HTML then
let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.css") in
@@ -482,8 +482,8 @@ let produce_document l =
if (Sys.file_exists src) then (copy src dst) else eprintf "Warning: file %s does not exist\n" src);
(if !target_language=LaTeX then
let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.sty") in
- let dst = if !output_dir <> "" then
- Filename.concat !output_dir "coqdoc.sty"
+ let dst = if !output_dir <> "" then
+ Filename.concat !output_dir "coqdoc.sty"
else "coqdoc.sty" in
if Sys.file_exists src then copy src dst else eprintf "Warning: file %s does not exist\n" src);
(match !Cdglobals.glob_source with
@@ -492,7 +492,7 @@ let produce_document l =
| GlobFile f -> ignore (Index.read_glob f));
List.iter index_module l;
match !out_to with
- | StdOut ->
+ | StdOut ->
Cdglobals.out_channel := stdout;
gen_one_file l
| File f ->
@@ -501,11 +501,11 @@ let produce_document l =
close_out_file()
| MultFiles ->
gen_mult_files l
-
+
let produce_output fl =
- if not (!dvi || !ps || !pdf) then
+ if not (!dvi || !ps || !pdf) then
produce_document fl
- else
+ else
begin
let texfile = Filename.temp_file "coqdoc" ".tex" in
let basefile = Filename.chop_suffix texfile ".tex" in
@@ -513,52 +513,52 @@ let produce_output fl =
out_to := File texfile;
output_dir := (Filename.dirname texfile);
produce_document fl;
-
+
let latexexe = if !pdf then "pdflatex" else "latex" in
- let latexcmd =
+ let latexcmd =
let file = Filename.basename texfile in
- let file =
- if !quiet then sprintf "'\\nonstopmode\\input{%s}'" file else file
+ let file =
+ if !quiet then sprintf "'\\nonstopmode\\input{%s}'" file else file
in
sprintf "%s %s && %s %s 1>&2 %s" latexexe file latexexe file (if !quiet then "> /dev/null" else "")
in
let res = locally (Filename.dirname texfile) Sys.command latexcmd in
if res <> 0 then begin
- eprintf "Couldn't run LaTeX successfully\n";
+ eprintf "Couldn't run LaTeX successfully\n";
clean_and_exit basefile res
end;
-
+
let dvifile = basefile ^ ".dvi" in
- if !dvi then
+ if !dvi then
begin
match final_out_to with
| MultFiles | StdOut -> cat dvifile
| File f -> copy dvifile f
end;
let pdffile = basefile ^ ".pdf" in
- if !pdf then
+ if !pdf then
begin
match final_out_to with
| MultFiles | StdOut -> cat pdffile
| File f -> copy pdffile f
end;
if !ps then begin
- let psfile = basefile ^ ".ps"
+ let psfile = basefile ^ ".ps"
in
- let command =
- sprintf "dvips %s -o %s %s" dvifile psfile
+ 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";
+ eprintf "Couldn't run dvips successfully\n";
clean_and_exit basefile res
end;
match final_out_to with
| MultFiles | StdOut -> cat psfile
| File f -> copy psfile f
end;
-
+
clean_temp_files basefile
end
@@ -570,5 +570,5 @@ let main () =
let files = parse () in
if not !quiet then banner ();
if files <> [] then produce_output files
-
+
let _ = Printexc.catch main ()
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 302cbffce..0c5e9ff29 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -25,26 +25,26 @@ let sprintf = Printf.sprintf
(*s Coq keywords *)
-let build_table l =
+let build_table l =
let h = Hashtbl.create 101 in
List.iter (fun key ->Hashtbl.add h key ()) l;
function s -> try Hashtbl.find h s; true with Not_found -> false
-let is_keyword =
+let is_keyword =
build_table
[ "AddPath"; "Axiom"; "Abort"; "Boxed"; "Chapter"; "Check"; "Coercion"; "CoFixpoint";
- "CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example";
+ "CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example";
"Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint";
- "Hypothesis"; "Hypotheses";
- "Resolve"; "Unfold"; "Immediate"; "Extern"; "Implicit"; "Import"; "Inductive";
- "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac";
+ "Hypothesis"; "Hypotheses";
+ "Resolve"; "Unfold"; "Immediate"; "Extern"; "Implicit"; "Import"; "Inductive";
+ "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac";
"Module"; "Module Type"; "Declare Module"; "Include";
"Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Proof with"; "Qed";
"Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme";
- "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem";
+ "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem";
"Set"; "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context";
"Notation"; "Reserved Notation"; "Tactic Notation";
- "Delimit"; "Bind"; "Open"; "Scope";
+ "Delimit"; "Bind"; "Open"; "Scope";
"Boxed"; "Unboxed"; "Inline";
"Implicit Arguments"; "Add"; "Strict";
"Typeclasses"; "Instance"; "Global Instance"; "Class"; "Instantiation";
@@ -54,13 +54,13 @@ let is_keyword =
"Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next";
"Program Instance"; "Equations"; "Equations_nocomp";
(*i (* coq terms *) *)
- "forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun";
+ "forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun";
"if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"; "struct"; "wf"; "measure";
(* Ltac *)
"before"; "after"
]
-let is_tactic =
+let is_tactic =
build_table
[ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection";
"elimtype"; "progress"; "setoid_rewrite";
@@ -81,14 +81,14 @@ let current_module : (string * string option) ref = ref ("",None)
let get_module withsub =
let (m,sub) = !current_module in
- if withsub then
- match sub with
+ if withsub then
+ match sub with
| None -> m
| Some sub -> m ^ ": " ^ sub
else
m
-let set_module m sub = current_module := (m,sub);
+let set_module m sub = current_module := (m,sub);
page_title := get_module true
(*s Common to both LaTeX and HTML *)
@@ -102,15 +102,15 @@ let token_pp = Hashtbl.create 97
let add_printing_token = Hashtbl.replace token_pp
-let find_printing_token tok =
+let find_printing_token tok =
try Hashtbl.find token_pp tok with Not_found -> None, None
let remove_printing_token = Hashtbl.remove token_pp
(* predefined pretty-prints *)
-let initialize () =
+let initialize () =
let if_utf8 = if !Cdglobals.utf8 then fun x -> Some x else fun _ -> None in
- List.iter
+ List.iter
(fun (s,l,l') -> Hashtbl.add token_pp s (Some l, l'))
[ "*" , "\\ensuremath{\\times}", if_utf8 "×";
"|", "\\ensuremath{|}", None;
@@ -136,7 +136,7 @@ let initialize () =
(*s Table of contents *)
-type toc_entry =
+type toc_entry =
| Toc_library of string * string option
| Toc_section of int * (unit -> unit) * string
@@ -172,7 +172,7 @@ module Latex = struct
Queue.iter (fun s -> printf "%s\n" s) preamble;
printf "\\begin{document}\n"
end;
- output_string
+ output_string
"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n";
output_string
"%% This file has been automatically generated with the command\n";
@@ -188,19 +188,19 @@ module Latex = struct
end
let char c = match c with
- | '\\' ->
+ | '\\' ->
printf "\\symbol{92}"
- | '$' | '#' | '%' | '&' | '{' | '}' | '_' ->
+ | '$' | '#' | '%' | '&' | '{' | '}' | '_' ->
output_char '\\'; output_char c
- | '^' | '~' ->
+ | '^' | '~' ->
output_char '\\'; output_char c; printf "{}"
- | _ ->
+ | _ ->
output_char c
let label_char c = match c with
| '\\' | '$' | '#' | '%' | '&' | '{' | '}' | '_'
| '^' | '~' -> ()
- | _ ->
+ | _ ->
output_char c
let latex_char = output_char
@@ -215,10 +215,10 @@ module Latex = struct
let label_ident s =
for i = 0 to String.length s - 1 do label_char s.[i] done
- let start_module () =
+ let start_module () =
let ln = !lib_name in
if not !short then begin
- printf "\\coqlibrary{";
+ printf "\\coqlibrary{";
label_ident (get_module false);
printf "}{";
if ln <> "" then printf "%s " ln;
@@ -235,22 +235,22 @@ module Latex = struct
let stop_verbatim () = printf "\\end{verbatim}\n"
- let indentation n =
- if n == 0 then
+ let indentation n =
+ if n == 0 then
printf "\\coqdocnoindent\n"
else
let space = 0.5 *. (float n) in
printf "\\coqdocindent{%2.2fem}\n" space
let with_latex_printing f tok =
- try
+ try
(match Hashtbl.find token_pp tok with
| Some s, _ -> output_string s
| _ -> f tok)
- with Not_found ->
+ with Not_found ->
f tok
- let module_ref m s =
+ let module_ref m s =
printf "\\moduleid{%s}{" m; raw_ident s; printf "}"
(*i
match find_module m with
@@ -278,16 +278,16 @@ module Latex = struct
printf "\\coq%s{" (type_name ty); label_ident (m ^ "." ^ id); printf "}{"; raw_ident s; printf "}"
let reference s = function
- | Def (fullid,typ) ->
+ | Def (fullid,typ) ->
defref (get_module false) fullid typ s
| Mod (m,s') when s = s' ->
module_ref m s
- | Ref (m,fullid,typ) ->
+ | Ref (m,fullid,typ) ->
ident_ref m fullid typ s
| Mod _ ->
printf "\\coqdocvar{"; raw_ident s; printf "}"
-
- let ident s loc =
+
+ let ident s loc =
if is_keyword s then begin
printf "\\coqdockw{"; raw_ident s; printf "}"
end else begin
@@ -298,7 +298,7 @@ module Latex = struct
if is_tactic s then begin
printf "\\coqdoctac{"; raw_ident s; printf "}"
end else begin
- if !Cdglobals.interpolate && !in_doc (* always a var otherwise *)
+ if !Cdglobals.interpolate && !in_doc (* always a var otherwise *)
then
try reference s (Index.find_string (get_module false) s)
with _ -> (printf "\\coqdocvar{"; raw_ident s; printf "}")
@@ -307,19 +307,19 @@ module Latex = struct
end
end
- let ident s l =
+ let ident s l =
if !in_title then (
printf "\\texorpdfstring{\\protect";
with_latex_printing (fun s -> ident s l) s;
printf "}{"; raw_ident s; printf "}")
else
with_latex_printing (fun s -> ident s l) s
-
+
let symbol s = with_latex_printing raw_ident s
let proofbox () = printf "\\ensuremath{\\Box}"
- let rec reach_item_level n =
+ let rec reach_item_level n =
if !item_level < n then begin
printf "\n\\begin{itemize}\n\\item "; incr item_level;
reach_item_level n
@@ -397,14 +397,14 @@ end
(*s HTML output *)
module Html = struct
-
+
let header () =
if !header_trailer then
if !header_file_spec then
let cin = Pervasives.open_in !header_file in
- try
- while true do
- let s = Pervasives.input_line cin in
+ try
+ while true do
+ let s = Pervasives.input_line cin in
printf "%s\n" s
done
with End_of_file -> Pervasives.close_in cin
@@ -421,14 +421,14 @@ module Html = struct
end
let trailer () =
- if !index && (get_module false) <> "Index" then
+ if !index && (get_module false) <> "Index" then
printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"%s.html\">Index</a>" !index_name;
- if !header_trailer then
+ if !header_trailer then
if !footer_file_spec then
let cin = Pervasives.open_in !footer_file in
- try
- while true do
- let s = Pervasives.input_line cin in
+ try
+ while true do
+ let s = Pervasives.input_line cin in
printf "%s\n" s
done
with End_of_file -> Pervasives.close_in cin
@@ -439,7 +439,7 @@ module Html = struct
printf "</div>\n\n</div>\n\n</body>\n</html>"
end
- let start_module () =
+ let start_module () =
let ln = !lib_name in
if not !short then begin
let (m,sub) = !current_module in
@@ -454,7 +454,7 @@ module Html = struct
let line_break () = printf "<br/>\n"
- let empty_line_of_code () =
+ let empty_line_of_code () =
printf "\n<br/>\n"
let char = function
@@ -477,7 +477,7 @@ module Html = struct
let start_verbatim () = printf "<pre>"
let stop_verbatim () = printf "</pre>\n"
- let module_ref m s =
+ let module_ref m s =
match find_module m with
| Local ->
printf "<a class=\"modref\" href=\"%s.html\">" m; raw_ident s; printf "</a>"
@@ -491,56 +491,56 @@ module Html = struct
match find_module m with
| Local ->
printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid;
- printf "<span class=\"id\" type=\"%s\">" typ;
+ printf "<span class=\"id\" type=\"%s\">" typ;
raw_ident s;
printf "</span></a>"
| Coqlib when !externals ->
let m = Filename.concat !coqlib m in
printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid;
- printf "<span class=\"id\" type=\"%s\">" typ;
+ printf "<span class=\"id\" type=\"%s\">" typ;
raw_ident s; printf "</span></a>"
| Coqlib | Unknown ->
printf "<span class=\"id\" type=\"%s\">" typ; raw_ident s; printf "</span>"
-
- let reference s r =
+
+ let reference s r =
match r with
- | Def (fullid,ty) ->
- printf "<a name=\"%s\">" fullid;
- printf "<span class=\"id\" type=\"%s\">" (type_name ty);
+ | Def (fullid,ty) ->
+ printf "<a name=\"%s\">" fullid;
+ printf "<span class=\"id\" type=\"%s\">" (type_name ty);
raw_ident s; printf "</span></a>"
| Mod (m,s') when s = s' ->
module_ref m s
- | Ref (m,fullid,ty) ->
+ | Ref (m,fullid,ty) ->
ident_ref m fullid (type_name ty) s
| Mod _ ->
printf "<span class=\"id\" type=\"mod\">"; raw_ident s ; printf "</span>"
- let ident s loc =
+ let ident s loc =
if is_keyword s then begin
- printf "<span class=\"id\" type=\"keyword\">";
- raw_ident s;
+ printf "<span class=\"id\" type=\"keyword\">";
+ raw_ident s;
printf "</span>"
- end else
+ end else
begin
try reference s (Index.find (get_module false) loc)
with Not_found ->
if is_tactic s then
(printf "<span class=\"id\" type=\"tactic\">"; raw_ident s; printf "</span>")
else
- if !Cdglobals.interpolate && !in_doc (* always a var otherwise *)
+ if !Cdglobals.interpolate && !in_doc (* always a var otherwise *)
then
try reference s (Index.find_string (get_module false) s)
with _ ->
(printf "<span class=\"id\" type=\"var\">"; raw_ident s ; printf "</span>")
else (printf "<span class=\"id\" type=\"var\">"; raw_ident s ; printf "</span>")
end
-
+
let with_html_printing f tok =
- try
+ try
(match Hashtbl.find token_pp tok with
| _, Some s -> output_string s
| _ -> f tok)
- with Not_found ->
+ with Not_found ->
f tok
let ident s l =
@@ -551,7 +551,7 @@ module Html = struct
let proofbox () = printf "<font size=-2>&#9744;</font>"
- let rec reach_item_level n =
+ let rec reach_item_level n =
if !item_level < n then begin
printf "<ul>\n<li>"; incr item_level;
reach_item_level n
@@ -576,11 +576,11 @@ module Html = struct
printf "\n<div class=\"doc\">\n"
let end_doc () = in_doc := false;
- stop_item ();
+ stop_item ();
if not !raw_comments then printf "\n</div>\n"
let start_emph () = printf "<i>"
-
+
let stop_emph () = printf "</i>"
let start_comment () = printf "<span class=\"comment\">(*"
@@ -620,19 +620,19 @@ module Html = struct
if l <> [] then begin
let cat = if category && idx <> "global" then "(" ^ idx ^ ")" else "" in
printf "<a name=\"%s_%c\"></a><h2>%c %s</h2>\n" idx c c cat;
- List.iter
- (fun (id,(text,link)) ->
+ List.iter
+ (fun (id,(text,link)) ->
printf "<a href=\"%s\">%s</a> %s<br/>\n" link id text) l;
printf "<br/><br/>"
end
-
+
let all_letters i = List.iter (letter_index false i.idx_name) i.idx_entries
(* Construction d'une liste des index (1 index global, puis 1
index par catégorie) *)
let format_global_index =
- Index.map
- (fun s (m,t) ->
+ Index.map
+ (fun s (m,t) ->
if t = Library then
let ln = !lib_name in
if ln <> "" then
@@ -647,16 +647,16 @@ module Html = struct
| Library, idx ->
Index.map (fun id m -> "", m ^ ".html") idx
| (t,idx) ->
- Index.map
- (fun s m ->
+ 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
(* 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) ->
+ List.iter
+ (fun (c,l) ->
if l <> [] then
printf "<td><a href=\"%s\">%c</a></td>\n" (index_ref i c) c
else
@@ -666,11 +666,11 @@ module Html = struct
printf "<td>(%d %s)</td>\n" n (if n > 1 then "entries" else "entry");
printf "</tr>\n"
- let print_index_table idxl =
+ let print_index_table idxl =
printf "<table>\n";
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
@@ -685,16 +685,16 @@ module Html = struct
in
List.iter one_letter i.idx_entries
- let make_multi_index () =
- let all_index =
+ 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 () =
- let all_index =
+ let all_index =
let glob,bt = Index.all_entries () in
(format_global_index glob) ::
(List.map format_bytype_index bt) in
@@ -708,16 +708,16 @@ module Html = struct
set_module "Index" None;
if !title <> "" then printf "<h1>%s</h1>\n" !title;
print_table ();
- if not (!multi_index) then
+ if not (!multi_index) then
begin
List.iter print_one_index all_index;
printf "<hr/>"; print_table ()
end
-
- let make_toc () =
+
+ let make_toc () =
let ln = !lib_name in
let make_toc_entry = function
- | Toc_library (m,sub) ->
+ | Toc_library (m,sub) ->
stop_item ();
let ms = match sub with | None -> m | Some s -> m ^ ": " ^ s in
if ln = "" then
@@ -725,14 +725,14 @@ module Html = struct
else
printf "<a href=\"%s.html\"><h2>%s %s</h2></a>\n" m ln ms
| Toc_section (n, f, r) ->
- item n;
+ item n;
printf "<a href=\"%s\">" r; f (); printf "</a>\n"
in
printf "<div id=\"toc\">\n";
Queue.iter make_toc_entry toc_q;
stop_item ();
printf "</div>\n"
-
+
end
@@ -742,15 +742,15 @@ module TeXmacs = struct
(*s Latex preamble *)
- let (preamble : string Queue.t) =
+ let (preamble : string Queue.t) =
in_doc := false; Queue.create ()
let push_in_preamble s = Queue.add s preamble
let header () =
- output_string
+ output_string
"(*i This file has been automatically generated with the command \n";
- output_string
+ output_string
" "; Array.iter (fun s -> printf "%s " s) Sys.argv; printf " *)\n"
let trailer () = ()
@@ -785,7 +785,7 @@ module TeXmacs = struct
let indentation n = ()
- let ident_true s =
+ let ident_true s =
if is_keyword s then begin
printf "<kw|"; raw_ident s; printf ">"
end else begin
@@ -793,8 +793,8 @@ module TeXmacs = struct
end
let ident s _ = if !in_doc then ident_true s else raw_ident s
-
- let symbol_true s =
+
+ let symbol_true s =
let ensuremath x = printf "<with|mode|math|\\<%s\\>>" x in
match s with
| "*" -> ensuremath "times"
@@ -815,7 +815,7 @@ module TeXmacs = struct
let proofbox () = printf "QED"
- let rec reach_item_level n =
+ let rec reach_item_level n =
if !item_level < n then begin
printf "\n<\\itemize>\n<item>"; incr item_level;
reach_item_level n
@@ -857,7 +857,7 @@ module TeXmacs = struct
let section lev f =
stop_item ();
- printf "<"; output_string (section_kind lev); printf "|";
+ printf "<"; output_string (section_kind lev); printf "|";
f (); printf ">\n\n"
let rule () =
@@ -897,7 +897,7 @@ module Raw = struct
let label_char c = match c with
| '\\' | '$' | '#' | '%' | '&' | '{' | '}' | '_'
| '^' | '~' -> ()
- | _ ->
+ | _ ->
output_char c
let latex_char = output_char
@@ -919,7 +919,7 @@ module Raw = struct
let stop_verbatim () = ()
- let indentation n =
+ let indentation n =
for i = 1 to n do printf " " done
let ident s loc = raw_ident s
@@ -947,15 +947,15 @@ module Raw = struct
let start_code () = end_doc (); start_coq ()
let end_code () = end_coq (); start_doc ()
- let section_kind =
+ let section_kind =
function
| 1 -> "* "
| 2 -> "** "
| 3 -> "*** "
| 4 -> "**** "
- | _ -> assert false
+ | _ -> assert false
- let section lev f =
+ let section lev f =
output_string (section_kind lev);
f ()
@@ -972,7 +972,7 @@ module Raw = struct
let make_multi_index () = ()
let make_index () = ()
- let make_toc () = ()
+ let make_toc () = ()
end
@@ -980,7 +980,7 @@ end
(*s Generic output *)
-let select f1 f2 f3 f4 x =
+let select f1 f2 f3 f4 x =
match !target_language with LaTeX -> f1 x | HTML -> f2 x | TeXmacs -> f3 x | Raw -> f4 x
let push_in_preamble = Latex.push_in_preamble
@@ -988,7 +988,7 @@ let push_in_preamble = Latex.push_in_preamble
let header = select Latex.header Html.header TeXmacs.header Raw.header
let trailer = select Latex.trailer Html.trailer TeXmacs.trailer Raw.trailer
-let start_module =
+let start_module =
select Latex.start_module Html.start_module TeXmacs.start_module Raw.start_module
let start_doc = select Latex.start_doc Html.start_doc TeXmacs.start_doc Raw.start_doc
@@ -1001,17 +1001,17 @@ let start_coq = select Latex.start_coq Html.start_coq TeXmacs.start_coq Raw.star
let end_coq = select Latex.end_coq Html.end_coq TeXmacs.end_coq Raw.end_coq
let start_code = select Latex.start_code Html.start_code TeXmacs.start_code Raw.start_code
-let end_code = select Latex.end_code Html.end_code TeXmacs.end_code Raw.end_code
+let end_code = select Latex.end_code Html.end_code TeXmacs.end_code Raw.end_code
-let start_inline_coq =
+let start_inline_coq =
select Latex.start_inline_coq Html.start_inline_coq TeXmacs.start_inline_coq Raw.start_inline_coq
-let end_inline_coq =
+let end_inline_coq =
select Latex.end_inline_coq Html.end_inline_coq TeXmacs.end_inline_coq Raw.end_inline_coq
let indentation = select Latex.indentation Html.indentation TeXmacs.indentation Raw.indentation
let paragraph = select Latex.paragraph Html.paragraph TeXmacs.paragraph Raw.paragraph
let line_break = select Latex.line_break Html.line_break TeXmacs.line_break Raw.line_break
-let empty_line_of_code = select
+let empty_line_of_code = select
Latex.empty_line_of_code Html.empty_line_of_code TeXmacs.empty_line_of_code Raw.empty_line_of_code
let section = select Latex.section Html.section TeXmacs.section Raw.section
@@ -1027,10 +1027,10 @@ let symbol = select Latex.symbol Html.symbol TeXmacs.symbol Raw.symbol
let proofbox = select Latex.proofbox Html.proofbox TeXmacs.proofbox Raw.proofbox
let latex_char = select Latex.latex_char Html.latex_char TeXmacs.latex_char Raw.latex_char
-let latex_string =
+let latex_string =
select Latex.latex_string Html.latex_string TeXmacs.latex_string Raw.latex_string
let html_char = select Latex.html_char Html.html_char TeXmacs.html_char Raw.html_char
-let html_string =
+let html_string =
select Latex.html_string Html.html_string TeXmacs.html_string Raw.html_string
let start_emph =
@@ -1038,16 +1038,16 @@ let start_emph =
let stop_emph =
select Latex.stop_emph Html.stop_emph TeXmacs.stop_emph Raw.stop_emph
-let start_latex_math =
+let start_latex_math =
select Latex.start_latex_math Html.start_latex_math TeXmacs.start_latex_math Raw.start_latex_math
-let stop_latex_math =
+let stop_latex_math =
select Latex.stop_latex_math Html.stop_latex_math TeXmacs.stop_latex_math Raw.stop_latex_math
-let start_verbatim =
+let start_verbatim =
select Latex.start_verbatim Html.start_verbatim TeXmacs.start_verbatim Raw.start_verbatim
-let stop_verbatim =
+let stop_verbatim =
select Latex.stop_verbatim Html.stop_verbatim TeXmacs.stop_verbatim Raw.stop_verbatim
-let verbatim_char =
+let verbatim_char =
select output_char Html.char TeXmacs.char Raw.char
let hard_verbatim_char = output_char
diff --git a/tools/coqwc.mll b/tools/coqwc.mll
index 9c0019342..f3646a8a1 100644
--- a/tools/coqwc.mll
+++ b/tools/coqwc.mll
@@ -11,10 +11,10 @@
(*i $Id$ i*)
-(*s {\bf coqwc.} Counts the lines of spec, proof and comments in a Coq source.
+(*s {\bf coqwc.} Counts the lines of spec, proof and comments in a Coq source.
It assumes the files to be lexically well-formed. *)
-(*i*){
+(*i*){
open Printf
open Lexing
open Filename
@@ -40,8 +40,8 @@ let tplines = ref 0
let tdlines = ref 0
let update_totals () =
- tslines := !tslines + !slines;
- tplines := !tplines + !plines;
+ tslines := !tslines + !slines;
+ tplines := !tplines + !plines;
tdlines := !tdlines + !dlines
(*s The following booleans indicate whether we have seen spec, proof or
@@ -53,12 +53,12 @@ let seen_proof = ref false
let seen_comment = ref false
let newline () =
- if !seen_spec then incr slines;
- if !seen_proof then incr plines;
- if !seen_comment then incr dlines;
+ if !seen_spec then incr slines;
+ if !seen_proof then incr plines;
+ if !seen_comment then incr dlines;
seen_spec := false; seen_proof := false; seen_comment := false
-let reset_counters () =
+let reset_counters () =
seen_spec := false; seen_proof := false; seen_comment := false;
slines := 0; plines := 0; dlines := 0
@@ -83,7 +83,7 @@ let print_totals () = print_line !tslines !tplines !tdlines (Some "total")
(*i*)}(*i*)
(*s Shortcuts for regular expressions. The [rcs] regular expression
- is used to skip the CVS infos possibly contained in some comments,
+ is used to skip the CVS infos possibly contained in some comments,
in order not to consider it as documentation. *)
let space = [' ' '\t' '\r']
@@ -96,7 +96,7 @@ let rcs_keyword =
let rcs = "\036" rcs_keyword [^ '$']* "\036"
let stars = "(*" '*'* "*)"
let dot = '.' (' ' | '\t' | '\n' | '\r' | eof)
-let proof_start =
+let proof_start =
"Theorem" | "Lemma" | "Fact" | "Remark" | "Goal" | "Correctness" | "Obligation" | "Next"
let proof_end =
("Save" | "Qed" | "Defined" | "Abort" | "Admitted") [^'.']* '.'
@@ -105,10 +105,10 @@ let proof_end =
rule spec = parse
| "(*" { comment lexbuf; spec lexbuf }
- | '"' { let n = string lexbuf in slines := !slines + n;
+ | '"' { let n = string lexbuf in slines := !slines + n;
seen_spec := true; spec lexbuf }
| '\n' { newline (); spec lexbuf }
- | space+ | stars
+ | space+ | stars
{ spec lexbuf }
| proof_start space
{ seen_spec := true; spec_to_dot lexbuf; proof lexbuf }
@@ -118,7 +118,7 @@ rule spec = parse
{ seen_spec := true; definition lexbuf }
| "Program"? "Fixpoint" space
{ seen_spec := true; definition lexbuf }
- | character | _
+ | character | _
{ seen_spec := true; spec lexbuf }
| eof { () }
@@ -126,29 +126,29 @@ rule spec = parse
and spec_to_dot = parse
| "(*" { comment lexbuf; spec_to_dot lexbuf }
- | '"' { let n = string lexbuf in slines := !slines + n;
+ | '"' { let n = string lexbuf in slines := !slines + n;
seen_spec := true; spec_to_dot lexbuf }
| '\n' { newline (); spec_to_dot lexbuf }
| dot { () }
- | space+ | stars
+ | space+ | stars
{ spec_to_dot lexbuf }
- | character | _
+ | character | _
{ seen_spec := true; spec_to_dot lexbuf }
| eof { () }
-(*s [definition] scans a definition; passes to [proof] is the body is
+(*s [definition] scans a definition; passes to [proof] is the body is
absent, and to [spec] otherwise *)
and definition = parse
| "(*" { comment lexbuf; definition lexbuf }
- | '"' { let n = string lexbuf in slines := !slines + n;
+ | '"' { let n = string lexbuf in slines := !slines + n;
seen_spec := true; definition lexbuf }
| '\n' { newline (); definition lexbuf }
| ":=" { seen_spec := true; spec lexbuf }
| dot { proof lexbuf }
- | space+ | stars
+ | space+ | stars
{ definition lexbuf }
- | character | _
+ | character | _
{ seen_spec := true; definition lexbuf }
| eof { () }
@@ -156,30 +156,30 @@ and definition = parse
and proof = parse
| "(*" { comment lexbuf; proof lexbuf }
- | '"' { let n = string lexbuf in plines := !plines + n;
+ | '"' { let n = string lexbuf in plines := !plines + n;
seen_proof := true; proof lexbuf }
- | space+ | stars
+ | space+ | stars
{ proof lexbuf }
| '\n' { newline (); proof lexbuf }
- | "Proof" space* '.'
+ | "Proof" space* '.'
{ seen_proof := true; proof lexbuf }
| "Proof" space
{ proof_term lexbuf }
| proof_end
{ seen_proof := true; spec lexbuf }
- | character | _
+ | character | _
{ seen_proof := true; proof lexbuf }
| eof { () }
and proof_term = parse
| "(*" { comment lexbuf; proof_term lexbuf }
- | '"' { let n = string lexbuf in plines := !plines + n;
+ | '"' { let n = string lexbuf in plines := !plines + n;
seen_proof := true; proof_term lexbuf }
- | space+ | stars
+ | space+ | stars
{ proof_term lexbuf }
| '\n' { newline (); proof_term lexbuf }
| dot { spec lexbuf }
- | character | _
+ | character | _
{ seen_proof := true; proof_term lexbuf }
| eof { () }
@@ -188,12 +188,12 @@ and proof_term = parse
and comment = parse
| "(*" { comment lexbuf; comment lexbuf }
| "*)" { () }
- | '"' { let n = string lexbuf in dlines := !dlines + n;
+ | '"' { let n = string lexbuf in dlines := !dlines + n;
seen_comment := true; comment lexbuf }
| '\n' { newline (); comment lexbuf }
| space+ | stars
{ comment lexbuf }
- | character | _
+ | character | _
{ seen_comment := true; comment lexbuf }
| eof { () }
@@ -212,9 +212,9 @@ and string = parse
It stops whenever it encounters an empty line or any character outside
a comment. In this last case, it correctly resets the lexer position
on that character (decreasing [lex_curr_pos] by 1). *)
-
+
and read_header = parse
- | "(*" { skip_comment lexbuf; skip_until_nl lexbuf;
+ | "(*" { skip_comment lexbuf; skip_until_nl lexbuf;
read_header lexbuf }
| "\n" { () }
| space+ { read_header lexbuf }
@@ -250,9 +250,9 @@ let process_file f =
print_file (Some f);
update_totals ()
with
- | Sys_error "Is a directory" ->
+ | Sys_error "Is a directory" ->
flush stdout; eprintf "coqwc: %s: Is a directory\n" f; flush stderr
- | Sys_error s ->
+ | Sys_error s ->
flush stdout; eprintf "coqwc: %s\n" s; flush stderr
(*s Parsing of the command line. *)
@@ -269,9 +269,9 @@ let usage () =
let rec parse = function
| [] -> []
| ("-h" | "-?" | "-help" | "--help") :: _ -> usage ()
- | ("-s" | "--spec-only") :: args ->
+ | ("-s" | "--spec-only") :: args ->
proof_only := false; spec_only := true; parse args
- | ("-r" | "--proof-only") :: args ->
+ | ("-r" | "--proof-only") :: args ->
spec_only := false; proof_only := true; parse args
| ("-p" | "--percentage") :: args -> percentage := true; parse args
| ("-e" | "--header") :: args -> skip_header := false; parse args
@@ -281,7 +281,7 @@ let rec parse = function
let main () =
let files = parse (List.tl (Array.to_list Sys.argv)) in
- if not (!spec_only || !proof_only) then
+ if not (!spec_only || !proof_only) then
printf " spec proof comments\n";
match files with
| [] -> process_channel stdin; print_file None
diff --git a/tools/gallina.ml b/tools/gallina.ml
index 8b3944207..8ba9ae104 100644
--- a/tools/gallina.ml
+++ b/tools/gallina.ml
@@ -16,29 +16,29 @@ let option_moins = ref false
let option_stdout = ref false
-let traite_fichier f =
- try
- let chan_in = open_in (f^".v") in
+let traite_fichier f =
+ try
+ let chan_in = open_in (f^".v") in
let buf = Lexing.from_channel chan_in in
if not !option_stdout then chan_out := open_out (f ^ ".g");
- try
+ try
while true do Gallina_lexer.action buf done
- with Fin_fichier -> begin
+ with Fin_fichier -> begin
flush !chan_out;
close_in chan_in;
if not !option_stdout then close_out !chan_out
end
- with Sys_error _ ->
- ()
+ with Sys_error _ ->
+ ()
let traite_stdin () =
try
let buf = Lexing.from_channel stdin in
- try
+ try
while true do Gallina_lexer.action buf done
- with Fin_fichier ->
+ with Fin_fichier ->
flush !chan_out
- with Sys_error _ ->
+ with Sys_error _ ->
()
let gallina () =
@@ -52,7 +52,7 @@ let gallina () =
| "-" -> option_moins := true
| "-stdout" -> option_stdout := true
| "-nocomments" -> comments := false
- | f ->
+ | f ->
if Filename.check_suffix f ".v" then
vfiles := (Filename.chop_suffix f ".v") :: !vfiles
in
diff --git a/tools/gallina_lexer.mll b/tools/gallina_lexer.mll
index b47a04b2c..6d35d8397 100644
--- a/tools/gallina_lexer.mll
+++ b/tools/gallina_lexer.mll
@@ -17,7 +17,7 @@
let cRcpt = ref 0
let comments = ref true
let print s = output_string !chan_out s
-
+
exception Fin_fichier
}
@@ -26,17 +26,17 @@ let space = [' ' '\t' '\n' '\r']
let enddot = '.' (' ' | '\t' | '\n' | '\r' | eof)
rule action = parse
- | "Theorem" space { print "Theorem "; body lexbuf;
+ | "Theorem" space { print "Theorem "; body lexbuf;
cRcpt := 1; action lexbuf }
- | "Lemma" space { print "Lemma "; body lexbuf;
+ | "Lemma" space { print "Lemma "; body lexbuf;
cRcpt := 1; action lexbuf }
- | "Fact" space { print "Fact "; body lexbuf;
+ | "Fact" space { print "Fact "; body lexbuf;
cRcpt := 1; action lexbuf }
- | "Remark" space { print "Remark "; body lexbuf;
+ | "Remark" space { print "Remark "; body lexbuf;
cRcpt := 1; action lexbuf }
- | "Goal" space { print "Goal "; body lexbuf;
+ | "Goal" space { print "Goal "; body lexbuf;
cRcpt := 1; action lexbuf }
- | "Correctness" space { print "Correctness "; body_pgm lexbuf;
+ | "Correctness" space { print "Correctness "; body_pgm lexbuf;
cRcpt := 1; action lexbuf }
| "Definition" space { print "Definition "; body_def lexbuf;
cRcpt := 1; action lexbuf }
@@ -55,7 +55,7 @@ rule action = parse
| _ { print (Lexing.lexeme lexbuf); cRcpt := 0; action lexbuf }
and comment = parse
- | "(*" { (if !comments then print "(*");
+ | "(*" { (if !comments then print "(*");
comment_depth := succ !comment_depth; comment lexbuf }
| "*)" { (if !comments then print "*)");
comment_depth := pred !comment_depth;
@@ -63,15 +63,15 @@ and comment = parse
| "*)" [' ''\t']*'\n' { (if !comments then print (Lexing.lexeme lexbuf));
comment_depth := pred !comment_depth;
if !comment_depth > 0 then comment lexbuf }
- | eof { raise Fin_fichier }
- | _ { (if !comments then print (Lexing.lexeme lexbuf));
+ | eof { raise Fin_fichier }
+ | _ { (if !comments then print (Lexing.lexeme lexbuf));
comment lexbuf }
and skip_comment = parse
| "(*" { comment_depth := succ !comment_depth; skip_comment lexbuf }
| "*)" { comment_depth := pred !comment_depth;
if !comment_depth > 0 then skip_comment lexbuf }
- | eof { raise Fin_fichier }
+ | eof { raise Fin_fichier }
| _ { skip_comment lexbuf }
and body_def = parse
@@ -83,14 +83,14 @@ and body = parse
| ":=" { print ".\n"; skip_proof lexbuf }
| "(*" { print "(*"; comment_depth := 1;
comment lexbuf; body lexbuf }
- | eof { raise Fin_fichier }
+ | eof { raise Fin_fichier }
| _ { print (Lexing.lexeme lexbuf); body lexbuf }
and body_pgm = parse
| enddot { print ".\n"; skip_proof lexbuf }
| "(*" { print "(*"; comment_depth := 1;
comment lexbuf; body_pgm lexbuf }
- | eof { raise Fin_fichier }
+ | eof { raise Fin_fichier }
| _ { print (Lexing.lexeme lexbuf); body_pgm lexbuf }
and skip_until_point = parse
@@ -98,13 +98,13 @@ and skip_until_point = parse
| enddot { end_of_line lexbuf }
| "(*" { comment_depth := 1;
skip_comment lexbuf; skip_until_point lexbuf }
- | eof { raise Fin_fichier }
+ | eof { raise Fin_fichier }
| _ { skip_until_point lexbuf }
and end_of_line = parse
| [' ' '\t' ]* { end_of_line lexbuf }
| '\n' { () }
- | eof { raise Fin_fichier }
+ | eof { raise Fin_fichier }
| _ { print (Lexing.lexeme lexbuf) }
and skip_proof = parse
@@ -124,5 +124,5 @@ and skip_proof = parse
| "Proof" [' ' '\t']* '.' { skip_proof lexbuf }
| "(*" { comment_depth := 1;
skip_comment lexbuf; skip_proof lexbuf }
- | eof { raise Fin_fichier }
+ | eof { raise Fin_fichier }
| _ { skip_proof lexbuf }
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 20:05:26 +0000