diff options
-rw-r--r-- | tools/coqdoc/coqdoc.css | 26 | ||||
-rw-r--r-- | tools/coqdoc/index.mli | 2 | ||||
-rw-r--r-- | tools/coqdoc/index.mll | 30 | ||||
-rw-r--r-- | tools/coqdoc/main.ml | 5 | ||||
-rw-r--r-- | tools/coqdoc/output.ml | 130 | ||||
-rw-r--r-- | tools/coqdoc/output.mli | 2 | ||||
-rw-r--r-- | tools/coqdoc/pretty.mll | 38 |
7 files changed, 161 insertions, 72 deletions
diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css index 65c39b7a2..bb9d2886c 100644 --- a/tools/coqdoc/coqdoc.css +++ b/tools/coqdoc/coqdoc.css @@ -66,3 +66,29 @@ body { padding: 0px 0px; #footer a:link { text-decoration: none; color: #888888; } +.id { display: inline; } + +.id[type="constructor"] { + color: rgb(60%,0%,0%); +} + +.id[type="var"] { + color: rgb(40%,0%,40%); +} + +.id[type="definition"] { + color: rgb(0%,40%,0%); +} + +.id[type="lemma"] { + color: rgb(0%,40%,0%); +} + +.id[type="inductive"] { + color: rgb(0%,0%,80%); +} + +.id[type="keyword"] { + color : #cf1d1d; +/* color: black; */ +} diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli index 9831ca3cb..bfb57dad2 100644 --- a/tools/coqdoc/index.mli +++ b/tools/coqdoc/index.mli @@ -40,6 +40,8 @@ type index_entry = val find : coq_module -> loc -> index_entry +val find_string : coq_module -> string -> index_entry + val add_module : coq_module -> unit type module_kind = Local | Coqlib | Unknown diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll index 6a61571c6..5b5425590 100644 --- a/tools/coqdoc/index.mll +++ b/tools/coqdoc/index.mll @@ -47,9 +47,14 @@ let current_type = ref Library let current_library = ref "" (** refers to the file being parsed *) -let table = Hashtbl.create 97 - (** [table] is used to store references and definitions *) +(** [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 @@ -60,15 +65,20 @@ let full_ident sp id = else "" let add_def loc ty sp id = - Hashtbl.add table (!current_library, loc) (Def (full_ident sp id, ty)) - + Hashtbl.add reftable (!current_library, loc) (Def (full_ident sp id, ty)); + Hashtbl.add deftable (!current_library, id) (Def (full_ident sp id, ty)) + let add_ref m loc m' sp id ty = - Hashtbl.add table (m, loc) (Ref (m', full_ident sp id, ty)) + Hashtbl.add reftable (m, loc) (Ref (m', full_ident sp id, ty)) -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 add_mod m loc m' id = + Hashtbl.add reftable (m, loc) (Mod (m', id)); + Hashtbl.add deftable (m, id) (Mod (m', id)) + +let find m l = Hashtbl.find reftable (m, l) + +let find_string m s = Hashtbl.find deftable (m, s) + (*s Manipulating path prefixes *) type stack = string list @@ -216,7 +226,7 @@ let all_entries () = | Def (s,t) -> add_g s m t; add_bt t s m | Ref _ | Mod _ -> () in - Hashtbl.iter classify table; + 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; diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index d9384adc4..08707ba24 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -62,6 +62,7 @@ let usage () = prerr_endline " --utf8 set UTF-8 input language"; prerr_endline " --charset <string> set HTML charset"; prerr_endline " --inputenc <string> set LaTeX input encoding"; + prerr_endline " --interpolate try to typeset identifiers in comments using definitions in the same module"; prerr_endline ""; exit 1 @@ -267,6 +268,9 @@ let parse () = usage () | ("-raw-comments" | "--raw-comments") :: rem -> Cdglobals.raw_comments := true; parse_rec rem + | ("-interpolate" | "--interpolate") :: rem -> + Cdglobals.interpolate := true; parse_rec rem + | ("-latin1" | "--latin1") :: rem -> Cdglobals.set_latin1 (); parse_rec rem | ("-utf8" | "--utf8") :: rem -> @@ -318,6 +322,7 @@ let parse () = add_file (what_file f); parse_rec rem in parse_rec (List.tl (Array.to_list Sys.argv)); + Output.initialize (); List.rev !files diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index a5378e9df..a7ed7444a 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -32,8 +32,8 @@ let build_table l = let is_keyword = build_table - [ "AddPath"; "Axiom"; "Chapter"; "Check"; "CoFixpoint"; - "CoInductive"; "Defined"; "Definition"; "End"; "Eval"; "Example"; + [ "AddPath"; "Axiom"; "Chapter"; "Check"; "Coercion"; "CoFixpoint"; + "CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint"; "Hypothesis"; "Hypotheses"; "Resolve"; "Unfold"; "Immediate"; "Extern"; "Implicit"; "Import"; "Inductive"; @@ -42,7 +42,7 @@ let is_keyword = "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Qed"; "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; - "Set"; "Unset"; "Variable"; "Variables"; "Context"; + "Set"; "Types"; "Unset"; "Variable"; "Variables"; "Context"; "Notation"; "Reserved Notation"; "Tactic Notation"; "Delimit"; "Bind"; "Open"; "Scope"; "Boxed"; "Unboxed"; "Inline"; @@ -53,8 +53,8 @@ let is_keyword = "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next"; "Program Instance"; (*i (* coq terms *) *) - "match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun"; - "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where" + "forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun"; + "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where" ] let is_tactic = @@ -92,27 +92,29 @@ let find_printing_token tok = let remove_printing_token = Hashtbl.remove token_pp (* predefined pretty-prints *) -let _ = List.iter - (fun (s,l) -> Hashtbl.add token_pp s (Some l, None)) - [ "*" , "\\ensuremath{\\times}"; - "|", "\\ensuremath{|}"; - "->", "\\ensuremath{\\rightarrow}"; - "->~", "\\ensuremath{\\rightarrow\\lnot}"; - "->~~", "\\ensuremath{\\rightarrow\\lnot\\lnot}"; - "<-", "\\ensuremath{\\leftarrow}"; - "<->", "\\ensuremath{\\leftrightarrow}"; - "=>", "\\ensuremath{\\Rightarrow}"; - "<=", "\\ensuremath{\\le}"; - ">=", "\\ensuremath{\\ge}"; - "<>", "\\ensuremath{\\not=}"; - "~", "\\ensuremath{\\lnot}"; - "/\\", "\\ensuremath{\\land}"; - "\\/", "\\ensuremath{\\lor}"; - "|-", "\\ensuremath{\\vdash}"; - "forall", "\\ensuremath{\\forall}"; - "exists", "\\ensuremath{\\exists}"; - (* "fun", "\\ensuremath{\\lambda}" ? *) - ] +let initialize () = + let if_utf8 = if !Cdglobals.utf8 then fun x -> Some x else fun _ -> None in + List.iter + (fun (s,l,l') -> Hashtbl.add token_pp s (Some l, l')) + [ "*" , "\\ensuremath{\\times}", if_utf8 "×"; + "|", "\\ensuremath{|}", None; + "->", "\\ensuremath{\\rightarrow}", if_utf8 "→"; + "->~", "\\ensuremath{\\rightarrow\\lnot}", None; + "->~~", "\\ensuremath{\\rightarrow\\lnot\\lnot}", None; + "<-", "\\ensuremath{\\leftarrow}", None; + "<->", "\\ensuremath{\\leftrightarrow}", if_utf8 "↔"; + "=>", "\\ensuremath{\\Rightarrow}", if_utf8 "⇒"; + "<=", "\\ensuremath{\\le}", if_utf8 "≤"; + ">=", "\\ensuremath{\\ge}", if_utf8 "≥"; + "<>", "\\ensuremath{\\not=}", if_utf8 "≠"; + "~", "\\ensuremath{\\lnot}", if_utf8 "¬"; + "/\\", "\\ensuremath{\\land}", if_utf8 "∧"; + "\\/", "\\ensuremath{\\lor}", if_utf8 "∨"; + "|-", "\\ensuremath{\\vdash}", None; + "forall", "\\ensuremath{\\forall}", if_utf8 "∀"; + "exists", "\\ensuremath{\\exists}", if_utf8 "∃" + (* "fun", "\\ensuremath{\\lambda}" ? *) + ] (*s Table of contents *) @@ -243,30 +245,37 @@ module Latex = struct let _m = Filename.concat !coqlib m in printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}" | Coqlib | Unknown -> - raw_ident s + printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}" let defref m id ty s = printf "\\coq%s{" (type_name ty); label_ident (m ^ "." ^ id); printf "}{"; raw_ident s; printf "}" + let reference s = function + | Def (fullid,typ) -> + defref !current_module fullid typ s + | Mod (m,s') when s = s' -> + module_ref m s + | Ref (m,fullid,typ) -> + ident_ref m fullid typ s + | Mod _ -> + printf "\\coqdocid{"; raw_ident s; printf "}" + let ident s loc = if is_keyword s then begin printf "\\coqdockw{"; raw_ident s; printf "}" end else begin begin try - (match Index.find !current_module loc with - | Def (fullid,typ) -> - defref !current_module fullid typ s - | Mod (m,s') when s = s' -> - module_ref m s - | Ref (m,fullid,typ) -> - ident_ref m fullid typ s - | Mod _ -> - printf "\\coqdocid{"; raw_ident s; printf "}") + reference s (Index.find !current_module loc) with Not_found -> if is_tactic s then begin printf "\\coqdoctac{"; raw_ident s; printf "}" - end else begin printf "\\coqdocvar{"; raw_ident s; printf "}" end + end else begin + if !Cdglobals.interpolate then + try reference s (Index.find_string !current_module s) + with _ -> printf "\\coqdocvar{"; raw_ident s; printf "}" + else printf "\\coqdocvar{"; raw_ident s; printf "}" + end end end @@ -394,7 +403,8 @@ module Html = struct let line_break () = printf "<br/>\n" - let empty_line_of_code () = printf "\n<br/>\n" + let empty_line_of_code () = + printf "\n<br/>\n" let char = function | '<' -> printf "<" @@ -426,37 +436,43 @@ module Html = struct | Coqlib | Unknown -> raw_ident s - let ident_ref m fid s = + let ident_ref m fid typ s = match find_module m with - | Local -> - printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; raw_ident s; printf "</a>" - | Coqlib when !externals -> - let m = Filename.concat !coqlib m in - printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; raw_ident s; printf "</a>" - | Coqlib | Unknown -> - raw_ident s - + | Local -> + printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; + printf "<div class=\"id\" type=\"%s\">" typ; raw_ident s; printf "</div></a>" + | Coqlib when !externals -> + let m = Filename.concat !coqlib m in + printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; + printf "<div class=\"id\" type=\"%s\">" typ; raw_ident s; printf "</div></a>" + | Coqlib | Unknown -> + printf "<div class=\"id\" type=\"%s\">" typ; raw_ident s; printf "</div>" + let ident s loc = if is_keyword s then begin - printf "<span class=\"keyword\">"; + printf "<div class=\"id\" type=\"keyword\">"; raw_ident s; - printf "</span>" + printf "</div>" end else begin try (match Index.find !current_module loc with - | Def (fullid,_) -> - printf "<a name=\"%s\"></a>" fullid; raw_ident s + | Def (fullid,ty) -> + printf "<a name=\"%s\">" fullid; + printf "<div class=\"id\" type=\"%s\">" (type_name ty); raw_ident s; printf "</div></a>" | Mod (m,s') when s = s' -> module_ref m s | Ref (m,fullid,ty) -> - ident_ref m fullid s + ident_ref m fullid (type_name ty) s | Mod _ -> - raw_ident s) + printf "<div class=\"id\" type=\"mod\">"; raw_ident s ; printf "</div>") with Not_found -> - raw_ident s + if is_tactic s then + (printf "<div class=\"id\" type=\"tactic\">"; raw_ident s; printf "</div>") + else + (printf "<div class=\"id\" type=\"var\">"; raw_ident s ; printf "</div>") end - + let with_html_printing f tok = try (match Hashtbl.find token_pp tok with @@ -536,7 +552,7 @@ module Html = struct 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) *) + index par catégorie) *) let format_global_index = Index.map (fun s (m,t) -> @@ -575,7 +591,7 @@ module Html = struct printf "</table>\n" let make_one_multi_index prt_tbl i = - (* Attn: make_one_multi_index créé un nouveau fichier... *) + (* Attn: make_one_multi_index créé un nouveau fichier... *) let idx = i.idx_name in let one_letter ((c,l) as cl) = open_out_file (sprintf "index_%s_%c.html" idx c); diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli index 824e267e5..f8fbb0fa4 100644 --- a/tools/coqdoc/output.mli +++ b/tools/coqdoc/output.mli @@ -11,6 +11,8 @@ open Cdglobals open Index +val initialize : unit -> unit + val add_printing_token : string -> string option * string option -> unit val remove_printing_token : string -> unit diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll index b02133285..fc40a97c5 100644 --- a/tools/coqdoc/pretty.mll +++ b/tools/coqdoc/pretty.mll @@ -57,6 +57,7 @@ let formatted = ref false let brackets = ref 0 let comment_level = ref 0 + let in_proof = ref false let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos @@ -214,7 +215,7 @@ let def_token = "Definition" | "Let" | "Class" - | "SubClass" + | "SubClass" | "Example" | "Local" | "Fixpoint" @@ -278,6 +279,8 @@ let commands = | ("Hypothesis" | "Hypotheses") | "End" +let end_kw = "Proof" | "Qed" | "Defined" | "Save" | "Admitted" + let extraction = "Extraction" | "Recursive" space+ "Extraction" @@ -292,7 +295,7 @@ let prog_kw = | "Solve" let gallina_kw_to_hide = - "Implicit" + "Implicit" space+ "Arguments" | "Ltac" | "Require" | "Import" @@ -304,6 +307,7 @@ let gallina_kw_to_hide = | "Delimit" | "Transparent" | "Opaque" + | "Proof" space+ "with" | ("Declare" space+ ("Morphism" | "Step") ) | ("Set" | "Unset") space+ "Printing" space+ "Coercions" | "Declare" space+ ("Left" | "Right") space+ "Step" @@ -334,7 +338,7 @@ let end_verb = "(*" space* "end" space+ "verb" space* "*)" rule coq_bol = parse | space* nl+ - { Output.empty_line_of_code (); coq_bol lexbuf } + { if not (!in_proof && !Cdglobals.gallina) then Output.empty_line_of_code (); coq_bol lexbuf } | space* "(**" space_nl { Output.end_coq (); Output.start_doc (); let eol = doc_bol lexbuf in @@ -353,7 +357,7 @@ rule coq_bol = parse { let s = lexeme lexbuf in if !Cdglobals.light && section_or_end s then let eol = skip_to_dot lexbuf in - if eol then (Output.line_break (); coq_bol lexbuf) else coq lexbuf + if eol then (coq_bol lexbuf) else coq lexbuf else begin let nbsp,isp = count_spaces s in @@ -363,6 +367,30 @@ rule coq_bol = parse let eol = body lexbuf in if eol then coq_bol lexbuf else coq lexbuf end } + | space* thm_token + { 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); + let eol = body lexbuf in + in_proof := true; + if eol then coq_bol lexbuf else coq lexbuf } + | space* "Proof" (space* "." | space+ "with") + { let eol = + if not !Cdglobals.gallina then + begin backtrack lexbuf; Output.indentation 0; body_bol lexbuf end + else true + in if eol then coq_bol lexbuf else coq lexbuf } + | space* end_kw { + in_proof := false; + let eol = + if not !Cdglobals.gallina then + begin backtrack lexbuf; Output.indentation 0; body_bol lexbuf end + else + skip_to_dot lexbuf + in + if eol then coq_bol lexbuf else coq lexbuf } | space* gallina_kw { let s = lexeme lexbuf in let nbsp,isp = count_spaces s in @@ -420,7 +448,7 @@ rule coq_bol = parse and coq = parse | nl - { Output.line_break(); coq_bol lexbuf } + { if not (!in_proof && !Cdglobals.gallina) then Output.line_break(); coq_bol lexbuf } | "(**" space_nl { Output.end_coq (); Output.start_doc (); let eol = doc_bol lexbuf in |