From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 16 Jun 2006 14:41:51 +0000 Subject: Imported Upstream version 8.0pl3+8.1beta --- tools/check-translate | 23 ++++ tools/coq_makefile.ml4 | 4 +- tools/coqdep.ml | 35 +++--- tools/coqdep_lexer.mll | 40 +++---- tools/coqdoc/cdglobals.ml | 2 +- tools/coqdoc/coqdoc.css | 26 +++-- tools/coqdoc/index.mll | 197 ++++++++++++++++++++++++---------- tools/coqdoc/main.ml | 263 +++++++++++++++++++++++----------------------- tools/coqdoc/output.ml | 34 +++--- tools/coqdoc/pretty.mll | 9 +- 10 files changed, 384 insertions(+), 249 deletions(-) create mode 100755 tools/check-translate (limited to 'tools') diff --git a/tools/check-translate b/tools/check-translate new file mode 100755 index 00000000..3dd82405 --- /dev/null +++ b/tools/check-translate @@ -0,0 +1,23 @@ +#!/bin/sh + +echo -------------- Producing translated files --------------------- +rm */*/*.v8 >& /dev/null +make COQ_XML=-translate theories || { echo ---- Failed to translate; exit 1; } +if [ -e translated ]; then rm -r translated; fi +if [ -e successful-translation ]; then rm -r successful-translation; fi +if [ -e failed-translation ]; then rm -r failed-translation; fi +mv theories translated +mkdir theories +echo -------------------- Upgrading files -------------------------- +cd translated +for i in */*.v +do + mkdir ../theories/`dirname $i` >& /dev/null + mv "$i"8 ../theories/$i +done +cd .. +echo --------------- Recompiling translated files ------------------ +make theories || { echo ---- Failed to recompile; mv theories failed-translation; mv translated theories; exit 1; } +echo ----------------- Recompilation successful -------------------- +if [ -e successful-translation ]; then rm -r successful-translation; fi +mv theories successful-translation; mv translated theories diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index cc3e9515..cd9d3669 100644 --- a/tools/coq_makefile.ml4 +++ b/tools/coq_makefile.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coq_makefile.ml4 7994 2006-02-06 08:48:37Z herbelin $ *) +(* $Id: coq_makefile.ml4 8840 2006-05-22 13:51:14Z notin $ *) (* créer un Makefile pour un développement Coq automatiquement *) @@ -197,7 +197,7 @@ let variables l = print "COQFLAGS=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n"; print "COQC=$(COQBIN)coqc\n"; print "GALLINA=gallina\n"; - print "COQDOC=coqdoc\n"; + print "COQDOC=$(COQBIN)coqdoc\n"; print "CAMLC=ocamlc -c\n"; print "CAMLOPTC=ocamlopt -c\n"; print "CAMLLINK=ocamlc\n"; diff --git a/tools/coqdep.ml b/tools/coqdep.ml index eb740712..6597c3f6 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqdep.ml 8642 2006-03-17 10:09:02Z notin $ *) +(* $Id: coqdep.ml 8923 2006-06-08 16:39:58Z herbelin $ *) open Printf open Coqdep_lexer @@ -162,8 +162,12 @@ let sort () = try while true do match coq_action lb with - | Require (_, s) -> - (try loop (List.assoc s !vKnown) with Not_found -> ()) + | Require (_, sl) -> + List.iter + (fun s -> + try loop (List.assoc s !vKnown) + with Not_found -> ()) + sl | RequireString (_, s) -> loop s | _ -> () done @@ -184,17 +188,18 @@ let traite_fichier_Coq verbose f = while true do let tok = coq_action buf in match tok with - | Require (spec,str) -> - if not (List.mem str !deja_vu_v) then begin - addQueue deja_vu_v str; - try - let file_str = safe_assoc verbose f str in - printf " %s%s" (canonize file_str) - (if spec then !suffixe_spec else !suffixe) - with Not_found -> - if verbose && not (List.mem_assoc str !coqlibKnown) then - warning_module_notfound f str - end + | Require (spec,strl) -> + List.iter (fun str -> + if not (List.mem str !deja_vu_v) then begin + addQueue deja_vu_v str; + try + let file_str = safe_assoc verbose f str in + printf " %s%s" (canonize file_str) + (if spec then !suffixe_spec else !suffixe) + with Not_found -> + if verbose && not (List.mem_assoc str !coqlibKnown) then + warning_module_notfound f str + end) strl | RequireString (spec,s) -> let str = Filename.basename s in if not (List.mem [str] !deja_vu_v) then begin @@ -332,7 +337,7 @@ let mL_dependencies () = flush stdout) (List.rev !mlAccu); List.iter - (fun ((name,ext,dirname) as pairname) -> + (fun ((name,ext,dirname)) -> let fullname = file_name ([name],dirname) in let (dep,_) = traite_fichier_ML fullname ext in printf "%s.cmi: %s%s" fullname fullname ext; diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll index f7f37086..8ecab3b4 100755 --- a/tools/coqdep_lexer.mll +++ b/tools/coqdep_lexer.mll @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: coqdep_lexer.mll 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: coqdep_lexer.mll 8737 2006-04-26 21:55:21Z herbelin $ i*) { @@ -18,7 +18,7 @@ type spec = bool type coq_token = - | Require of spec * string list + | Require of spec * string list list | RequireString of spec * string | Declare of string list | Load of string @@ -27,7 +27,8 @@ exception Fin_fichier - let module_name = ref [] + let module_current_name = ref [] + let module_names = ref [] let ml_module_name = ref "" let specif = ref false @@ -48,13 +49,11 @@ let dot = '.' ( space+ | eof) rule coq_action = parse | "Require" space+ - { specif := false; opened_file lexbuf } + { specif := false; module_names := []; opened_file lexbuf } | "Require" space+ "Export" space+ - { specif := false; opened_file lexbuf} - | "Require" space+ "Syntax" space+ - { specif := false; opened_file lexbuf} + { specif := false; module_names := []; opened_file lexbuf} | "Require" space+ "Import" space+ - { specif := false; opened_file lexbuf} + { specif := false; module_names := []; opened_file lexbuf} | "Declare" space+ "ML" space+ "Module" space+ { mllist := []; modules lexbuf} | "Load" space+ @@ -175,7 +174,7 @@ and opened_file = parse | "Specification" { specif := true; opened_file lexbuf } | coq_ident - { module_name := [Lexing.lexeme lexbuf]; + { module_current_name := [Lexing.lexeme lexbuf]; opened_file_fields lexbuf } | '"' [^'"']* '"' { (*'"'*) @@ -186,23 +185,28 @@ and opened_file = parse Filename.chop_suffix str ".v" else str in RequireString (!specif, str) } - | eof { raise Fin_fichier } - | _ { opened_file lexbuf } + | eof { raise Fin_fichier } + | _ { opened_file lexbuf } and opened_file_fields = parse | "(*" (* "*)" *) { comment_depth := 1; comment lexbuf; opened_file_fields lexbuf } | space+ - { opened_file_fields lexbuf } + { opened_file_fields lexbuf } | coq_field - { module_name := - field_name (Lexing.lexeme lexbuf) :: !module_name; + { module_current_name := + field_name (Lexing.lexeme lexbuf) :: !module_current_name; opened_file_fields lexbuf } - | dot { Require (!specif, List.rev !module_name) } - | eof { raise Fin_fichier } - | _ { opened_file_fields lexbuf } - + | coq_ident { module_names := + List.rev !module_current_name :: !module_names; + module_current_name := [Lexing.lexeme lexbuf]; + opened_file_fields lexbuf } + | dot { module_names := + List.rev !module_current_name :: !module_names; + Require (!specif, List.rev !module_names) } + | eof { raise Fin_fichier } + | _ { opened_file_fields lexbuf } and modules = parse | space+ { modules lexbuf } diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml index b5a4cb22..8a774876 100644 --- a/tools/coqdoc/cdglobals.ml +++ b/tools/coqdoc/cdglobals.ml @@ -44,6 +44,7 @@ let page_title = ref "" let title = ref "" let externals = ref true let coqlib = ref "http://coq.inria.fr/library/" +let coqlib_path = ref Coq_config.coqlib let raw_comments = ref false let charset = ref "iso-8859-1" @@ -69,4 +70,3 @@ type file = | Vernac_file of string * coq_module | Latex_file of string - diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css index b59438e5..3900987e 100644 --- a/tools/coqdoc/coqdoc.css +++ b/tools/coqdoc/coqdoc.css @@ -28,16 +28,21 @@ body { padding: 0px 0px; #main a.idref:visited {color : #416DFF; text-decoration : none; } #main a.idref:link {color : #416DFF; text-decoration : none; } -#main a.idref:hover {color : Red; text-decoration : underline; } -#main a.idref:active {color : Red; text-decoration : underline; } +#main a.idref:hover {text-decoration : none; } +#main a.idref:active {text-decoration : none; } -#main .keyword { font-weight : bold; - color : Red } +#main a.modref:visited {color : #416DFF; text-decoration : none; } +#main a.modref:link {color : #416DFF; text-decoration : none; } +#main a.modref:hover {text-decoration : none; } +#main a.modref:active {text-decoration : none; } -#main .section { font-size : 20pt } +#main .keyword { color : #cf1d1d } +#main { color: black } + +#main .section { background-color:#899BD6; + font-size : 20pt } #main code { font-family: monospace; - font-size: 8pt; line-height: 50% } #main .doc { margin: 0px; @@ -45,10 +50,11 @@ body { padding: 0px 0px; font-family: sans-serif; font-size: 11pt; font-weight:bold; - background-color:#66ff66 } + color: black; + background-color: #90bdff; + border-style: plain} -#main .doc code { font-family: monospace; - font-size: 10pt} +#main .doc code { font-family: monospace} /* Pied de page */ @@ -56,4 +62,6 @@ body { padding: 0px 0px; font-family: sans-serif; } #footer a:visited { color: blue; } +#footer a:link { text-decoration: none; + color: #888888; } diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll index ec89da2f..9b5716ff 100644 --- a/tools/coqdoc/index.mll +++ b/tools/coqdoc/index.mll @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: index.mll 8617 2006-03-08 10:47:12Z notin $ i*) +(*i $Id: index.mll 8863 2006-05-26 10:33:21Z notin $ i*) { @@ -34,11 +34,14 @@ type index_entry = | Ref of coq_module * string | Mod of coq_module * string -let table = Hashtbl.create 97 +let current_type = ref Library +let current_library = ref "" + (** referes to the file being parsed *) -let current_module = ref "" +let table = Hashtbl.create 97 + (** [table] is used to store references and definitions *) -let add_def loc ty id = Hashtbl.add table (!current_module, loc) (Def (id, ty)) +let add_def loc ty id = Hashtbl.add table (!current_library, loc) (Def (id, ty)) let add_ref m loc m' id = Hashtbl.add table (m, loc) (Ref (m', id)) @@ -46,7 +49,55 @@ let add_mod m loc m' id = Hashtbl.add table (m, loc) (Mod (m', id)) let find m l = Hashtbl.find table (m, l) -let current_type = ref Library + +(*s Manipulating path prefixes *) + +type stack = string list + +let rec string_of_stack st = + match st with + | [] -> "" + | x::[] -> x + | x::tl -> (string_of_stack tl) ^ "." ^ x + +let empty_stack = [] + +let module_stack = ref empty_stack +let section_stack = ref empty_stack + +let init_stack () = + module_stack := empty_stack; section_stack := empty_stack + +let push st p = st := p::!st +let pop st = + match !st with + | [] -> () + | _::tl -> st := tl + +let head st = + match st with + | [] -> "" + | x::_ -> x + +let begin_module m = push module_stack m +let begin_section s = push section_stack s + +let end_block id = + (** determines if it ends a module or a section and pops the stack *) + if ((String.compare (head !module_stack) id ) == 0) then + pop module_stack + else if ((String.compare (head !section_stack) id) == 0) then + pop section_stack + else + () + +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 + id (* Coq modules *) @@ -83,7 +134,7 @@ let ref_module loc s = let n = String.length s in let i = String.rindex s ' ' in let id = String.sub s (i+1) (n-i-1) in - add_mod !current_module (loc+i+1) (Hashtbl.find modules id) id + add_mod !current_library (loc+i+1) (Hashtbl.find modules id) id with Not_found -> () @@ -104,25 +155,25 @@ let compare_entries (s1,_) (s2,_) = Alpha.compare_string s1 s2 let sort_entries el = let t = Hashtbl.create 97 in - 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 - let l = try Hashtbl.find t c with Not_found -> [] in - Hashtbl.replace t c (e :: l)) - el; - let res = ref [] in - 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 - + 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 + let l = try Hashtbl.find t c with Not_found -> [] in + Hashtbl.replace t c (e :: l)) + el; + let res = ref [] in + 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" | Module -> "module" @@ -133,28 +184,28 @@ let type_name = function | Variable -> "variable" | Axiom -> "axiom" | TacticDefinition -> "tactic" - + let all_entries () = let gl = ref [] in let add_g s m t = gl := (s,(m,t)) :: !gl in let bt = Hashtbl.create 11 in let add_bt t s m = let l = try Hashtbl.find bt t with Not_found -> [] in - Hashtbl.replace bt t ((s,m) :: l) + Hashtbl.replace bt t ((s,m) :: l) in 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 table; - 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_size = List.length !gl }, - Hashtbl.fold (fun t e l -> (t, { idx_name = type_name t; + Hashtbl.iter classify table; + 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_size = List.length !gl }, + 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. *) @@ -165,15 +216,14 @@ let firstchar = ['$' '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 ident = - firstchar identchar* + '\'' '0'-'9'] +let ident = firstchar identchar* let begin_hide = "(*" space* "begin" space+ "hide" space* "*)" let end_hide = "(*" space* "end" space+ "hide" space* "*)" - + (*s Indexing entry point. *) - + rule traverse = parse | "Definition" space { current_type := Definition; index_ident lexbuf; traverse lexbuf } @@ -192,13 +242,15 @@ rule traverse = parse | "Record" space { current_type := Inductive; index_ident lexbuf; traverse lexbuf } | "Module" (space+ "Type")? space - { current_type := Module; index_ident lexbuf; traverse lexbuf } + { current_type := Module; module_ident lexbuf; traverse lexbuf } (*i*** | "Variable" 's'? space { current_type := Variable; index_idents lexbuf; traverse lexbuf } ***i*) | "Require" (space+ ("Export"|"Import"))? space+ ident { ref_module (lexeme_start lexbuf) (lexeme lexbuf); traverse lexbuf } + | "End" space+ + { end_ident lexbuf; traverse lexbuf } | begin_hide { skip_hide lexbuf; traverse lexbuf } | "(*" @@ -216,7 +268,16 @@ and index_ident = parse | space+ { index_ident lexbuf } | ident - { add_def (lexeme_start lexbuf) !current_type (lexeme lexbuf) } + { let fullid = + let id = lexeme lexbuf in + match !current_type with + | Definition + | Inductive + | Constructor + | Lemma -> make_fullid id + | _ -> id + in + add_def (lexeme_start lexbuf) !current_type fullid } | eof { () } | _ @@ -234,12 +295,12 @@ and index_idents = parse { () } | _ { skip_until_point lexbuf } - + (*s Index identifiers in an inductive definition (types and constructors). *) - + and inductive = parse | '|' | ":=" space* '|'? - { current_type := Constructor; index_ident lexbuf; inductive lexbuf } + { current_type := Constructor; index_ident lexbuf; inductive lexbuf } | "with" space { current_type := Inductive; index_ident lexbuf; inductive lexbuf } | '.' @@ -248,9 +309,9 @@ and inductive = parse { () } | _ { inductive lexbuf } - + (*s Index identifiers in a Fixpoint declaration. *) - + and fixpoint = parse | "with" space { index_ident lexbuf; fixpoint lexbuf } @@ -260,9 +321,9 @@ and fixpoint = parse { () } | _ { fixpoint lexbuf } - + (*s Skip a possibly nested comment. *) - + and comment = parse | "*)" { () } | "(*" { comment lexbuf; comment lexbuf } @@ -271,25 +332,48 @@ 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 | eof | end_hide { () } | _ { skip_hide lexbuf } +and end_ident = parse + | space+ + { end_ident lexbuf } + | ident + { let id = lexeme lexbuf in end_block id } + | eof + { () } + | _ + { () } + +and module_ident = parse + | space+ + { module_ident lexbuf } + | ident space* ":=" + { () } + | ident + { let id = lexeme lexbuf in + begin_module id; add_def (lexeme_start lexbuf) !current_type id } + | eof + { () } + | _ + { () } + { let read_glob f = @@ -306,10 +390,11 @@ and skip_hide = parse | 'R' -> (try let i = String.index s ' ' in + let j = String.index_from s (i+1) ' ' in let loc = int_of_string (String.sub s 1 (i - 1)) in - let sp = String.sub s (i + 1) (n - i - 1) in - let m',id = split_sp sp in - add_ref !cur_mod loc m' id + let lib_dp = String.sub s (i + 1) (j - i - 1) in + let full_id = String.sub s (j + 1) (n - j - 1) in + add_ref !cur_mod loc lib_dp full_id with Not_found -> ()) | _ -> () @@ -317,11 +402,11 @@ and skip_hide = parse done with End_of_file -> close_in c - + let scan_file f m = - current_module := m; + init_stack (); current_library := m; let c = open_in f in let lb = from_channel c in - traverse lb; - close_in c + traverse lb; + close_in c } diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 177fc2bc..18a44a44 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: main.ml 8669 2006-03-28 17:34:15Z notin $ i*) +(*i $Id: main.ml 8777 2006-05-02 10:14:39Z notin $ i*) (* Modified by Lionel Elie Mamane on 9 & 10 Mar 2004: * - handling of absolute filenames (function coq_module) @@ -54,6 +54,7 @@ let usage () = prerr_endline " --no-externals no links to Coq standard library"; prerr_endline " --coqlib set URL for Coq standard library"; prerr_endline " (default is http://coq.inria.fr/library/)"; + prerr_endline " --coqlib_path set the path where Coq files are installed"; prerr_endline " -R map physical dir to Coq dir"; prerr_endline " --latin1 set ISO-8859-1 input language"; prerr_endline " --utf8 set UTF-8 input language"; @@ -71,12 +72,12 @@ let banner () = eprintf "This is coqdoc version %s, compiled on %s\n" Coq_config.version Coq_config.compile_date; flush stderr - + let target_full_name f = match !target_language with | HTML -> f ^ ".html" | _ -> f ^ ".tex" - + (*s \textbf{Separation of files.} Files given on the command line are separated according to their type, which is determined by their suffix. Coq files have suffixe \verb!.v! or \verb!.g! and \LaTeX\ @@ -87,11 +88,11 @@ let check_if_file_exists f = eprintf "\ncoqdoc: %s: no such file\n" f; exit 1 end - + let paths = ref [] - + let add_path m l = paths := (m,l) :: !paths - + let exists_dir dir = try let _ = Unix.opendir dir in true with Unix.Unix_error _ -> false @@ -99,72 +100,72 @@ let add_rec_path f l = let rec traverse abs rel = add_path abs rel; let dirh = Unix.opendir abs in - try - while true do - let f = Unix.readdir dirh in - if f <> "" && f.[0] <> '.' && f <> "CVS" then - let abs' = Filename.concat abs f in - try - if exists_dir abs' then traverse abs' (rel ^ "." ^ f) - with Unix.Unix_error _ -> - () - done - with End_of_file -> - Unix.closedir dirh + try + while true do + let f = Unix.readdir dirh in + if f <> "" && f.[0] <> '.' && f <> "CVS" then + let abs' = Filename.concat abs f in + try + if exists_dir abs' then traverse abs' (rel ^ "." ^ f) + with Unix.Unix_error _ -> + () + done + with End_of_file -> + Unix.closedir dirh in - if exists_dir f then traverse f l + if exists_dir f then traverse f l (* turn A/B/C into A.B.C *) let make_path = Str.global_replace (Str.regexp "/") ".";; let coq_module file = -(* TODO - * LEM: - * We should also remove things like "/./" in the middle of the filename, - * rewrite "/foo/../bar" to "/bar", recognise different paths that lead - * to the same file / directory (via symlinks), etc. The best way to do - * all this would be to use the libc function realpath() on _both_ p and - * file / f before comparing them. - * - * The semantics of realpath() on file symlinks might not be what we - * want... (But it is what we want on directory symlinks.) So, we would - * have to cook up our own version of realpath()? - * - * Do all target platforms have realpath()? - *) + (* TODO + * LEM: + * We should also remove things like "/./" in the middle of the filename, + * rewrite "/foo/../bar" to "/bar", recognise different paths that lead + * to the same file / directory (via symlinks), etc. The best way to do + * all this would be to use the libc function realpath() on _both_ p and + * file / f before comparing them. + * + * The semantics of realpath() on file symlinks might not be what we + * want... (But it is what we want on directory symlinks.) So, we would + * have to cook up our own version of realpath()? + * + * Do all target platforms have realpath()? + *) let f = chop_extension file in - (* remove leading ./ and any number of slashes after *) + (* remove leading ./ and any number of slashes after *) let f = Str.replace_first (Str.regexp "^\\./+") "" f in - if (Str.string_before f 1) = "/" then - (* f is an absolute path. Prefixes must be matched with the beginning of f, - * not prepended - *) - let rec trypath = function - | [] -> make_path f - | (p, lg) :: r -> - (* make sure p ends with a single '/' - * This guarantees that we don't match a file whose name is - * of the form p ^ "foo". It means we may miss p itself, - * but this does not matter: coqdoc doesn't do anything - * of a directory anyway. *) - let p = (Str.replace_first (Str.regexp "/*$") "/" p) in - let p_quoted = (Str.quote p) in - if (Str.string_match (Str.regexp p_quoted) f 0) then - make_path (Filename.concat lg (Str.replace_first (Str.regexp (p_quoted ^ "/*")) "" f)) - else - trypath r - in trypath !paths - else (* f is a relative path *) - let rec trypath = function - | [] -> - make_path f - | (p,lg) :: r -> - let p_file = Filename.concat p file in - if Sys.file_exists p_file then - make_path (Filename.concat lg f) - else - trypath r - in trypath !paths;; + if (Str.string_before f 1) = "/" then + (* f is an absolute path. Prefixes must be matched with the beginning of f, + * not prepended + *) + let rec trypath = function + | [] -> make_path f + | (p, lg) :: r -> + (* make sure p ends with a single '/' + * This guarantees that we don't match a file whose name is + * of the form p ^ "foo". It means we may miss p itself, + * but this does not matter: coqdoc doesn't do anything + * of a directory anyway. *) + let p = (Str.replace_first (Str.regexp "/*$") "/" p) in + let p_quoted = (Str.quote p) in + if (Str.string_match (Str.regexp p_quoted) f 0) then + make_path (Filename.concat lg (Str.replace_first (Str.regexp (p_quoted ^ "/*")) "" f)) + else + trypath r + in trypath !paths + else (* f is a relative path *) + let rec trypath = function + | [] -> + make_path f + | (p,lg) :: r -> + let p_file = Filename.concat p file in + if Sys.file_exists p_file then + make_path (Filename.concat lg f) + else + trypath r + in trypath !paths;; let what_file f = check_if_file_exists f; @@ -176,43 +177,43 @@ let what_file f = eprintf "\ncoqdoc: don't know what to do with %s\n" f; exit 1 end - + (*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 - in the file named [f]. These file names must be separated by spaces, - tabulations or newlines. + * 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 + * in the file named [f]. These file names must be separated by spaces, + * tabulations or newlines. *) let files_from_file f = let files_from_channel ch = let buf = Buffer.create 80 in let l = ref [] in - try - while true do - match input_char ch with - | ' ' | '\t' | '\n' -> - if Buffer.length buf > 0 then l := (Buffer.contents buf) :: !l; - Buffer.clear buf - | c -> - Buffer.add_char buf c - done; [] - with End_of_file -> - List.rev !l + try + while true do + match input_char ch with + | ' ' | '\t' | '\n' -> + if Buffer.length buf > 0 then l := (Buffer.contents buf) :: !l; + Buffer.clear buf + | c -> + Buffer.add_char buf c + done; [] + with End_of_file -> + List.rev !l in - try - check_if_file_exists f; - let ch = open_in f in - let l = files_from_channel ch in - close_in ch;l - with Sys_error s -> begin - eprintf "\ncoqdoc: cannot read from file %s (%s)\n" f s; - exit 1 - end - + try + check_if_file_exists f; + let ch = open_in f in + let l = files_from_channel ch in + close_in ch;l + with Sys_error s -> begin + eprintf "\ncoqdoc: cannot read from file %s (%s)\n" f s; + exit 1 + end + (*s \textbf{Parsing of the command line.} *) - + let output_file = ref "" let dvi = ref false let ps = ref false @@ -222,9 +223,9 @@ let parse () = let add_file f = files := f :: !files in let rec parse_rec = function | [] -> () - + | ("-nopreamble" | "--nopreamble" | "--no-preamble" - | "-bodyonly" | "--bodyonly" | "--body-only") :: rem -> + | "-bodyonly" | "--bodyonly" | "--body-only") :: rem -> header_trailer := false; parse_rec rem | ("-p" | "--preamble") :: s :: rem -> push_in_preamble s; parse_rec rem @@ -239,7 +240,7 @@ let parse () = | ("-stdout" | "--stdout") :: rem -> out_to := StdOut; parse_rec rem | ("-o" | "--output") :: f :: rem -> - out_to := File f; parse_rec rem + out_to := File (Filename.basename f); output_dir := Filename.dirname f; parse_rec rem | ("-o" | "--output") :: [] -> usage () | ("-d" | "--directory") :: dir :: rem -> @@ -280,10 +281,10 @@ 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 - + | ("-h" | "-help" | "-?" | "--help") :: rem -> banner (); usage () | ("-v" | "-version" | "--version") :: _ -> @@ -317,13 +318,17 @@ let parse () = Cdglobals.coqlib := u; parse_rec rem | ("--coqlib" | "-coqlib") :: [] -> usage () + | ("--coqlib_path" | "-coqlib_path") :: d :: rem -> + Cdglobals.coqlib_path := d; parse_rec rem + | ("--coqlib_path" | "-coqlib_path") :: [] -> + usage () | f :: rem -> add_file (what_file f); parse_rec rem in - parse_rec (List.tl (Array.to_list Sys.argv)); - List.rev !files - + parse_rec (List.tl (Array.to_list Sys.argv)); + 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]. If option \verb!-dvi!, \verb!-ps! or \verb!-html! is invoked, then @@ -331,41 +336,41 @@ let parse () = let locally dir f x = let cwd = Sys.getcwd () in - try - Sys.chdir dir; let y = f x in Sys.chdir cwd; y - with e -> - Sys.chdir cwd; raise e + try + Sys.chdir dir; let y = f x in Sys.chdir cwd; y + with e -> + Sys.chdir cwd; raise e let clean_temp_files basefile = let remove f = try Sys.remove f with _ -> () in - remove (basefile ^ ".tex"); - remove (basefile ^ ".log"); - remove (basefile ^ ".aux"); - remove (basefile ^ ".dvi"); - remove (basefile ^ ".ps"); - remove (basefile ^ ".haux"); - remove (basefile ^ ".html") - + remove (basefile ^ ".tex"); + remove (basefile ^ ".log"); + remove (basefile ^ ".aux"); + remove (basefile ^ ".dvi"); + remove (basefile ^ ".ps"); + 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 - while true do print_char (input_char c) done - with End_of_file -> - close_in c + try + while true do print_char (input_char c) done + with End_of_file -> + close_in c let copy src dst = let cin = open_in src and cout = open_out dst in - try - while true do Pervasives.output_char cout (input_char cin) done - with End_of_file -> - close_in cin; close_out cout + try + while true do Pervasives.output_char cout (input_char cin) done + with End_of_file -> + close_in cin; close_out cout (*s Functions for generating output files *) - + let gen_one_file l = let file = function | Vernac_file (f,m) -> @@ -416,15 +421,15 @@ let gen_mult_files l = let index_module = function | Vernac_file (_,m) -> Index.add_module m | Latex_file _ -> () - + let produce_document l = List.iter index_module l; (if !target_language=HTML then - let src = (Filename.concat Coq_config.coqlib "/tools/coqdoc/coqdoc.css") in + let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.css") in let dst = if !output_dir <> "" then Filename.concat !output_dir "coqdoc.css" else "coqdoc.css" in copy src dst); (if !target_language=LaTeX then - let src = (Filename.concat Coq_config.coqlib "/tools/coqdoc/coqdoc.sty") in + let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.sty") in let dst = if !output_dir <> "" then Filename.concat !output_dir "coqdoc.sty" else "coqdoc.sty" in @@ -439,7 +444,7 @@ let produce_document l = close_out_file() | MultFiles -> gen_mult_files l - + let produce_output fl = if not (!dvi || !ps) then begin produce_document fl @@ -493,7 +498,7 @@ let produce_output fl = let main () = let files = parse () in - if not !quiet then banner (); - if files <> [] then produce_output files - + 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 4c4cf5ec..e6a0a72b 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: output.ml 8669 2006-03-28 17:34:15Z notin $ i*) +(*i $Id: output.ml 8863 2006-05-26 10:33:21Z notin $ i*) open Cdglobals open Index @@ -336,12 +336,12 @@ module Html = struct raw_ident s i*) - let ident_ref m s = match find_module m with + let ident_ref m fid s = match find_module m with | Local -> - printf "" m s; raw_ident s; printf "" + printf "" m fid; raw_ident s; printf "" | Coqlib when !externals -> let m = Filename.concat !coqlib m in - printf "" m s; raw_ident s; printf "" + printf "" m fid; raw_ident s; printf "" | Coqlib | Unknown -> raw_ident s @@ -351,18 +351,20 @@ module Html = struct raw_ident s; printf "" end else - try - (match Index.find !current_module loc with - | Def _ -> - printf "" s; raw_ident s - | Mod (m,s') when s = s' -> - module_ref m s - | Ref (m,s') when s = s' -> - ident_ref m s - | Mod _ | Ref _ -> - raw_ident s) - with Not_found -> - raw_ident s + begin + try + (match Index.find !current_module loc with + | Def (fullid,_) -> + printf "" fullid; raw_ident s + | Mod (m,s') when s = s' -> + module_ref m s + | Ref (m,fullid) -> + ident_ref m fullid s + | Mod _ | Ref _ -> + raw_ident s) + with Not_found -> + raw_ident s + end let with_html_printing f tok = try diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll index ad9057ad..5c6c7952 100644 --- a/tools/coqdoc/pretty.mll +++ b/tools/coqdoc/pretty.mll @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pretty.mll 8666 2006-03-27 17:02:49Z notin $ i*) +(*i $Id: pretty.mll 8861 2006-05-24 15:52:15Z notin $ i*) (*s Utility functions for the scanners *) @@ -173,8 +173,11 @@ let firstchar = (* utf-8 letterlike symbols *) '\226' ('\132' ['\128'-'\191'] | '\133' ['\128'-'\143']) let identchar = - firstchar | ['\'' '0'-'9' '@'] -let identifier = firstchar identchar* + firstchar | ['\'' '0'-'9' '@' ] +let id = firstchar identchar* +let pfx_id = (id '.')* +let identifier = + id | pfx_id id let symbolchar_no_brackets = ['!' '$' '%' '&' '*' '+' ',' '@' '^' '#' -- cgit v1.2.3