diff options
Diffstat (limited to 'tools/coqdoc/output.ml')
| -rw-r--r-- | tools/coqdoc/output.ml | 92 |
1 files changed, 62 insertions, 30 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 2d29c447..ae6e6388 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -41,7 +41,7 @@ let is_keyword = "Mutual"; "Parameter"; "Parameters"; "Print"; "Printing"; "All"; "Proof"; "Proof with"; "Qed"; "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; "Assumptions"; "Axioms"; "Universes"; "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; - "Search"; "SearchAbout"; "SearchRewrite"; + "Search"; "SearchAbout"; "SearchHead"; "SearchPattern"; "SearchRewrite"; "Set"; "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context"; "Notation"; "Reserved Notation"; "Tactic Notation"; "Delimit"; "Bind"; "Open"; "Scope"; "Inline"; @@ -50,6 +50,7 @@ let is_keyword = "subgoal"; "subgoals"; "vm_compute"; "Opaque"; "Transparent"; "Time"; "Extraction"; "Extract"; + "Variant"; (* Program *) "Program Definition"; "Program Example"; "Program Fixpoint"; "Program Lemma"; "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next"; @@ -59,7 +60,7 @@ let is_keyword = "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"; "struct"; "wf"; "measure"; "fix"; "cofix"; (* Ltac *) - "before"; "after"; "constr"; "ltac"; "goal"; "context"; "beta"; "delta"; "iota"; "zeta"; + "before"; "after"; "constr"; "ltac"; "goal"; "context"; "beta"; "delta"; "iota"; "zeta"; "lazymatch"; (* Notations *) "level"; "associativity"; "no" ] @@ -210,6 +211,7 @@ module Latex = struct printf "\\usepackage{fullpage}\n"; printf "\\usepackage{coqdoc}\n"; printf "\\usepackage{amsmath,amssymb}\n"; + printf "\\usepackage{url}\n"; (match !toc_depth with | None -> () | Some n -> printf "\\setcounter{tocdepth}{%i}\n" n); @@ -383,6 +385,14 @@ module Latex = struct end; last_was_in := false + let sublexer_in_doc c = + if c = '*' && !last_was_in then begin + Tokens.flush_sublexer (); + output_char '*' + end else + Tokens.output_tagged_symbol_char None c; + last_was_in := false + let initialize () = initialize_tex_html (); Tokens.token_tree := token_tree_latex; @@ -399,8 +409,11 @@ module Latex = struct let ident s loc = last_was_in := s = "in"; try - let tag = Index.find (get_module false) loc in - reference (translate s) tag + match loc with + | None -> raise Not_found + | Some loc -> + let tag = Index.find (get_module false) loc in + reference (translate s) tag with Not_found -> if is_tactic s then printf "\\coqdoctac{%s}" (translate s) @@ -522,8 +535,8 @@ module Html = struct printf "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"\n"; printf "\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">\n"; printf "<html xmlns=\"http://www.w3.org/1999/xhtml\">\n<head>\n"; - printf "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=%s\"/>\n" !charset; - printf "<link href=\"coqdoc.css\" rel=\"stylesheet\" type=\"text/css\"/>\n"; + printf "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=%s\" />\n" !charset; + printf "<link href=\"coqdoc.css\" rel=\"stylesheet\" type=\"text/css\" />\n"; printf "<title>%s</title>\n</head>\n\n" !page_title; printf "<body>\n\n<div id=\"page\">\n\n<div id=\"header\">\n</div>\n\n"; printf "<div id=\"main\">\n\n" @@ -558,7 +571,7 @@ module Html = struct printf "<h1 class=\"libtitle\">%s %s</h1>\n\n" ln (get_module true) end - let indentation n = for i = 1 to n do printf " " done + let indentation n = for _i = 1 to n do printf " " done let line_break () = printf "<br/>\n" @@ -573,9 +586,6 @@ module Html = struct | '&' -> printf "&" | c -> output_char c - let raw_string s = - for i = 0 to String.length s - 1 do char s.[i] done - let escaped = let buff = Buffer.create 5 in fun s -> @@ -585,10 +595,24 @@ module Html = struct | '<' -> Buffer.add_string buff "<" | '>' -> Buffer.add_string buff ">" | '&' -> Buffer.add_string buff "&" + | '\'' -> Buffer.add_string buff "´" + | '\"' -> Buffer.add_string buff """ | c -> Buffer.add_char buff c done; Buffer.contents buff + let sanitize_name s = + let rec loop esc i = + if i < 0 then if esc then escaped s else s + else match s.[i] with + | 'a'..'z' | 'A'..'Z' | '0'..'9' | '.' | '_' -> loop esc (i-1) + | '<' | '>' | '&' | '\'' | '\"' -> loop true (i-1) + | _ -> + (* This name contains complex characters: + this is probably a notation string, we simply hash it. *) + Digest.to_hex (Digest.string s) + in loop false (String.length s - 1) + let latex_char _ = () let latex_string _ = () @@ -618,19 +642,19 @@ module Html = struct let ident_ref m fid typ s = match find_module m with | Local -> - printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; - printf "<span class=\"id\" type=\"%s\">%s</span></a>" typ s + printf "<a class=\"idref\" href=\"%s.html#%s\">" m (sanitize_name fid); + printf "<span class=\"id\" title=\"%s\">%s</span></a>" typ s | External m when !externals -> - printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; - printf "<span class=\"id\" type=\"%s\">%s</span></a>" typ s + printf "<a class=\"idref\" href=\"%s.html#%s\">" m (sanitize_name fid); + printf "<span class=\"id\" title=\"%s\">%s</span></a>" typ s | External _ | Unknown -> - printf "<span class=\"id\" type=\"%s\">%s</span>" typ s + printf "<span class=\"id\" title=\"%s\">%s</span>" typ s let reference s r = match r with | Def (fullid,ty) -> - printf "<a name=\"%s\">" fullid; - printf "<span class=\"id\" type=\"%s\">%s</span></a>" (type_name ty) s + printf "<a name=\"%s\">" (sanitize_name fullid); + printf "<span class=\"id\" title=\"%s\">%s</span></a>" (type_name ty) s | Ref (m,fullid,ty) -> ident_ref m fullid (type_name ty) s @@ -640,7 +664,7 @@ module Html = struct | Some ref -> reference s ref | None -> if issymbchar then output_string s - else printf "<span class=\"id\" type=\"var\">%s</span>" s + else printf "<span class=\"id\" title=\"var\">%s</span>" s let sublexer c loc = let tag = @@ -648,6 +672,9 @@ module Html = struct in Tokens.output_tagged_symbol_char tag c + let sublexer_in_doc c = + Tokens.output_tagged_symbol_char None c + let initialize () = initialize_tex_html(); Tokens.token_tree := token_tree_html; @@ -657,16 +684,20 @@ module Html = struct match Tokens.translate s with Some s -> s | None -> escaped s let keyword s loc = - printf "<span class=\"id\" type=\"keyword\">%s</span>" (translate s) + printf "<span class=\"id\" title=\"keyword\">%s</span>" (translate s) let ident s loc = if is_keyword s then begin - printf "<span class=\"id\" type=\"keyword\">%s</span>" (translate s) + printf "<span class=\"id\" title=\"keyword\">%s</span>" (translate s) end else begin - try reference (translate s) (Index.find (get_module false) loc) + try + match loc with + | None -> raise Not_found + | Some loc -> + reference (translate s) (Index.find (get_module false) loc) with Not_found -> if is_tactic s then - printf "<span class=\"id\" type=\"tactic\">%s</span>" (translate s) + printf "<span class=\"id\" title=\"tactic\">%s</span>" (translate s) else if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) then @@ -818,7 +849,7 @@ module Html = struct "[library]", m ^ ".html", t else sprintf "[%s, in <a href=\"%s.html\">%s</a>]" (type_name t) m m , - sprintf "%s.html#%s" m s, t) + sprintf "%s.html#%s" m (sanitize_name s), t) let format_bytype_index = function | Library, idx -> @@ -827,7 +858,7 @@ module Html = struct Index.map (fun s m -> let text = sprintf "[in <a href=\"%s.html\">%s</a>]" m m in - (text, sprintf "%s.html#%s" m s, t)) idx + (text, sprintf "%s.html#%s" m (sanitize_name s), t)) idx (* Impression de la table d'index *) let print_index_table_item i = @@ -923,8 +954,6 @@ module TeXmacs = struct let (preamble : string Queue.t) = in_doc := false; Queue.create () - let push_in_preamble s = Queue.add s preamble - let header () = output_string "(*i This file has been automatically generated with the command \n"; @@ -989,6 +1018,9 @@ module TeXmacs = struct let sublexer c l = if !in_doc then Tokens.output_tagged_symbol_char None c else char c + let sublexer_in_doc c = + char c + let initialize () = Tokens.token_tree := token_tree_texmacs; Tokens.outfun := output_sublexer_string @@ -1045,8 +1077,6 @@ module TeXmacs = struct let paragraph () = printf "\n\n" - let line_break_true () = printf "<format|line break>" - let line_break () = printf "\n" let empty_line_of_code () = printf "\n" @@ -1107,12 +1137,13 @@ module Raw = struct let stop_quote () = printf "\"" let indentation n = - for i = 1 to n do printf " " done + for _i = 1 to n do printf " " done let keyword s loc = raw_ident s let ident s loc = raw_ident s let sublexer c l = char c + let sublexer_in_doc c = char c let initialize () = Tokens.token_tree := ref Tokens.empty_ttree; @@ -1226,6 +1257,7 @@ let char = select Latex.char Html.char TeXmacs.char Raw.char let keyword = select Latex.keyword Html.keyword TeXmacs.keyword Raw.keyword let ident = select Latex.ident Html.ident TeXmacs.ident Raw.ident let sublexer = select Latex.sublexer Html.sublexer TeXmacs.sublexer Raw.sublexer +let sublexer_in_doc = select Latex.sublexer_in_doc Html.sublexer_in_doc TeXmacs.sublexer_in_doc Raw.sublexer_in_doc let initialize = select Latex.initialize Html.initialize TeXmacs.initialize Raw.initialize let proofbox = select Latex.proofbox Html.proofbox TeXmacs.proofbox Raw.proofbox |