diff options
Diffstat (limited to 'tools')
-rw-r--r-- | tools/coq_makefile.ml4 | 86 | ||||
-rw-r--r-- | tools/coq_tex.ml4 | 34 | ||||
-rw-r--r-- | tools/coqdep.ml | 34 | ||||
-rw-r--r-- | tools/coqdep_common.ml | 64 | ||||
-rwxr-xr-x | tools/coqdep_lexer.mll | 32 | ||||
-rw-r--r-- | tools/coqdoc/alpha.ml | 4 | ||||
-rw-r--r-- | tools/coqdoc/cdglobals.ml | 2 | ||||
-rw-r--r-- | tools/coqdoc/cpretty.mll | 432 | ||||
-rw-r--r-- | tools/coqdoc/index.mli | 8 | ||||
-rw-r--r-- | tools/coqdoc/index.mll | 222 | ||||
-rw-r--r-- | tools/coqdoc/main.ml | 148 | ||||
-rw-r--r-- | tools/coqdoc/output.ml | 234 | ||||
-rw-r--r-- | tools/coqwc.mll | 72 | ||||
-rw-r--r-- | tools/gallina.ml | 22 | ||||
-rw-r--r-- | tools/gallina_lexer.mll | 32 |
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>☐</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 } |