diff options
author | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
commit | db38bb4ad9aff74576d3b7f00028d48f0447d5bd (patch) | |
tree | 09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /tools/coqdoc | |
parent | 6e34b272d789455a9be589e27ad3a998cf25496b (diff) | |
parent | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff) |
Merge branch 'experimental/upstream' into upstream
Diffstat (limited to 'tools/coqdoc')
-rw-r--r-- | tools/coqdoc/alpha.ml | 4 | ||||
-rw-r--r-- | tools/coqdoc/alpha.mli | 4 | ||||
-rw-r--r-- | tools/coqdoc/cdglobals.ml | 46 | ||||
-rw-r--r-- | tools/coqdoc/coqdoc.css | 46 | ||||
-rw-r--r-- | tools/coqdoc/cpretty.mli | 4 | ||||
-rw-r--r-- | tools/coqdoc/cpretty.mll | 233 | ||||
-rw-r--r-- | tools/coqdoc/index.ml | 103 | ||||
-rw-r--r-- | tools/coqdoc/index.mli | 9 | ||||
-rw-r--r-- | tools/coqdoc/main.ml | 49 | ||||
-rw-r--r-- | tools/coqdoc/output.ml | 292 | ||||
-rw-r--r-- | tools/coqdoc/output.mli | 32 | ||||
-rw-r--r-- | tools/coqdoc/tokens.ml | 2 | ||||
-rw-r--r-- | tools/coqdoc/tokens.mli | 2 |
13 files changed, 593 insertions, 233 deletions
diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml index 83bfa5ed..8802c0ef 100644 --- a/tools/coqdoc/alpha.ml +++ b/tools/coqdoc/alpha.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: alpha.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) - open Cdglobals let norm_char_latin1 c = match Char.uppercase c with diff --git a/tools/coqdoc/alpha.mli b/tools/coqdoc/alpha.mli index ec5b084f..792b71fc 100644 --- a/tools/coqdoc/alpha.mli +++ b/tools/coqdoc/alpha.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: alpha.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - (* Alphabetic order. *) val compare_char : char -> char -> int diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml index 5cb670dc..f37db46b 100644 --- a/tools/coqdoc/cdglobals.ml +++ b/tools/coqdoc/cdglobals.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -49,21 +49,40 @@ type glob_source_t = let glob_source = ref DotGlob +(*s Manipulations of paths and path aliases *) + +let normalize_path p = + (* We use the Unix subsystem to normalize a physical path (relative + or absolute) and get rid of symbolic links, relative links (like + ./ or ../ in the middle of the path; it's tricky but it + works... *) + (* Rq: Sys.getcwd () returns paths without '/' at the end *) + let orig = Sys.getcwd () in + Sys.chdir p; + let res = Sys.getcwd () in + Sys.chdir orig; + res + +let normalize_filename f = + let basename = Filename.basename f in + let dirname = Filename.dirname f in + normalize_path dirname, basename + (** A weaker analog of the function in Envars *) let guess_coqlib () = let file = "states/initial.coq" in - if Sys.file_exists (Filename.concat Coq_config.coqlib file) - then Coq_config.coqlib - else - let coqbin = Filename.dirname Sys.executable_name in - let prefix = Filename.dirname coqbin in - let rpath = if Coq_config.local then [] else - (if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) in - let coqlib = List.fold_left Filename.concat prefix rpath in - if Sys.file_exists (Filename.concat coqlib file) then coqlib - else - Coq_config.coqlib + match Coq_config.coqlib with + | Some coqlib when Sys.file_exists (Filename.concat coqlib file) -> + coqlib + | Some _ | None -> + let coqbin = normalize_path (Filename.dirname Sys.executable_name) in + let prefix = Filename.dirname coqbin in + let rpath = if Coq_config.local then [] else + (if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) in + let coqlib = List.fold_left Filename.concat prefix rpath in + if Sys.file_exists (Filename.concat coqlib file) then coqlib + else prefix let header_trailer = ref true let header_file = ref "" @@ -90,6 +109,7 @@ let toc_depth = (ref None : int option ref) let lib_name = ref "Library" let lib_subtitles = ref false let interpolate = ref false +let inline_notmono = ref false let charset = ref "iso-8859-1" let inputenc = ref "" @@ -103,7 +123,7 @@ let set_latin1 () = let set_utf8 () = charset := "utf-8"; - inputenc := "utf8"; + inputenc := "utf8x"; utf8 := true (* Parsing options *) diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css index 24b514b7..ccd285f1 100644 --- a/tools/coqdoc/coqdoc.css +++ b/tools/coqdoc/coqdoc.css @@ -101,8 +101,13 @@ h4.section { color: rgb(30%,30%,70%); font-family: monospace } -.doc .inlinecode .id { - color: rgb(30%,30%,70%); +.doc .inlinecode .id { + color: rgb(30%,30%,70%); +} + +.inlinecodenm { + display: inline; + color: #444444; } .doc .code { @@ -124,6 +129,32 @@ h4.section { font-family: monospace; } +table.infrule { + border: 0px; + margin-left: 50px; + margin-top: 10px; + margin-bottom: 10px; +} + +td.infrule { + font-family: monospace; + text-align: center; +/* color: rgb(35%,35%,70%); */ + padding: 0px; + line-height: 100%; +} + +tr.infrulemiddle hr { + margin: 1px 0 1px 0; +} + +.infrulenamecol { + color: rgb(60%,60%,60%); + font-size: 80%; + padding-left: 1em; + padding-bottom: 0.1em +} + /* Pied de page */ #footer { font-size: 65%; @@ -231,4 +262,13 @@ h4.section { position: absolute; bottom: 0; text-align: bottom; -}
\ No newline at end of file +} + +.paragraph { + height: 0.75em; +} + +ul.doclist { + margin-top: 0em; + margin-bottom: 0em; +} diff --git a/tools/coqdoc/cpretty.mli b/tools/coqdoc/cpretty.mli index 085ae122..adc49ed4 100644 --- a/tools/coqdoc/cpretty.mli +++ b/tools/coqdoc/cpretty.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: cpretty.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - open Index val coq_file : string -> Cdglobals.coq_module -> unit diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index a2bcb987..d7b54fd0 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -1,14 +1,11 @@ -(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: cpretty.mll 14868 2011-12-26 17:07:24Z herbelin $ i*) - (*s Utility functions for the scanners *) { @@ -80,8 +77,17 @@ let in_proof = ref None let in_emph = ref false - let start_emph () = in_emph := true; Output.start_emph () - let stop_emph () = if !in_emph then (Output.stop_emph (); in_emph := false) + let in_env start stop = + let r = ref false in + let start_env () = r := true; start () in + let stop_env () = if !r then stop (); r := false in + (fun x -> !r), start_env, stop_env + + let in_emph, start_emph, stop_emph = in_env Output.start_emph Output.stop_emph + let in_quote, start_quote, stop_quote = in_env Output.start_quote Output.stop_quote + + let url_buffer = Buffer.create 40 + let url_name_buffer = Buffer.create 40 let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos; lexbuf.lex_curr_p <- lexbuf.lex_start_p @@ -257,7 +263,7 @@ 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.keyword s (lexeme_start lexbuf + isp) } @@ -323,6 +329,7 @@ let def_token = | "SubClass" | "Example" | "Fixpoint" + | "Function" | "Boxed" | "CoFixpoint" | "Record" @@ -371,13 +378,17 @@ let commands = | "Drop" | "ProtectedLoop" | "Quit" + | "Restart" | "Load" | "Add" | "Remove" space+ "Loadpath" | "Print" | "Inspect" | "About" + | "SearchAbout" + | "SearchRewrite" | "Search" + | "Locate" | "Eval" | "Reset" | "Check" @@ -405,6 +416,14 @@ let prog_kw = | "Obligations" | "Solve" +let hint_kw = + "Extern" | "Rewrite" | "Resolve" | "Immediate" | "Transparent" | "Opaque" | "Unfold" | "Constructors" + +let set_kw = + "Printing" space+ ("Coercions" | "Universes" | "All") + | "Implicit" space+ "Arguments" + + let gallina_kw_to_hide = "Implicit" space+ "Arguments" | "Ltac" @@ -412,15 +431,16 @@ let gallina_kw_to_hide = | "Import" | "Export" | "Load" - | "Hint" + | "Hint" space+ hint_kw | "Open" | "Close" | "Delimit" | "Transparent" | "Opaque" | ("Declare" space+ ("Morphism" | "Step") ) - | ("Set" | "Unset") space+ "Printing" space+ "Coercions" + | ("Set" | "Unset") space+ set_kw | "Declare" space+ ("Left" | "Right") space+ "Step" + | "Debug" space+ ("On" | "Off") let section = "*" | "**" | "***" | "****" @@ -512,7 +532,7 @@ rule coq_bol = parse output_indented_keyword s lexbuf; let eol= body lexbuf in if eol then coq_bol lexbuf else coq lexbuf } - | space* notation_kw space* + | space* notation_kw { let s = lexeme lexbuf in output_indented_keyword s lexbuf; let eol= start_notation_string lexbuf in @@ -639,7 +659,7 @@ and coq = parse Output.ident s (lexeme_start lexbuf); let eol = body lexbuf in if eol then coq_bol lexbuf else coq lexbuf } - | notation_kw space* + | notation_kw { let s = lexeme lexbuf in Output.ident s (lexeme_start lexbuf); let eol= start_notation_string lexbuf in @@ -663,8 +683,6 @@ and coq = parse (*s Scanning documentation, at beginning of line *) and doc_bol = parse - | space* nl+ - { Output.paragraph (); doc_bol lexbuf } | space* section space+ ([^'\n' '*'] | '*'+ [^'\n' ')' '*'])* ('*'+ '\n')? { let eol, lex = strip_eol (lexeme lexbuf) in let lev, s = sec_title lex in @@ -674,33 +692,26 @@ and doc_bol = parse else Output.section lev (fun () -> ignore (doc None (from_string s))); if eol then doc_bol lexbuf else doc None lexbuf } - | space* nl space* '-'+ - { (* adding this production instead of just letting the paragraph - production and the begin list production fire eliminates - extra vertical whitespace. *) - let buf' = lexeme lexbuf in - let buf = - let bufs = Str.split_delim (Str.regexp "['\n']") buf' in - match bufs with - | (_ :: s :: []) -> s - | (_ :: _ :: s :: _) -> s - | _ -> eprintf "Internal error bad_split1 - please report\n"; - exit 1 + | space_nl* '-'+ + { let buf' = lexeme lexbuf in + let bufs = Str.split_delim (Str.regexp "['\n']") buf' in + let lines = (List.length bufs) - 1 in + let line = + match bufs with + | [] -> eprintf "Internal error bad_split1 - please report\n"; + exit 1 + | _ -> List.nth bufs lines in - match check_start_list buf with + match check_start_list line with | Neither -> backtrack_past_newline lexbuf; doc None lexbuf - | List n -> Output.item 1; doc (Some [n]) lexbuf - | Rule -> Output.rule (); doc None lexbuf - } - | space* '-'+ - { let buf = lexeme lexbuf in - match check_start_list buf with - | Neither -> backtrack lexbuf; doc None lexbuf - | List n -> Output.item 1; doc (Some [n]) lexbuf + | List n -> Output.paragraph (); + Output.item 1; doc (Some [n]) lexbuf | Rule -> Output.rule (); doc None lexbuf } + | space* nl+ + { Output.paragraph (); doc_bol lexbuf } | "<<" space* - { Output.start_verbatim (); verbatim lexbuf; doc_bol lexbuf } + { Output.start_verbatim false; verbatim false lexbuf; doc_bol lexbuf } | eof { true } | '_' @@ -724,8 +735,8 @@ and doc_list_bol indents = parse backtrack lexbuf; doc_bol lexbuf } | "<<" space* - { Output.start_verbatim (); - verbatim lexbuf; + { Output.start_verbatim false; + verbatim false lexbuf; doc_list_bol indents lexbuf } | "[[" nl { formatted := true; @@ -734,6 +745,8 @@ and doc_list_bol indents = parse Output.end_inline_coq_block (); formatted := false; doc_list_bol indents lexbuf } + | "[[[" nl + { inf_rules (Some indents) lexbuf } | space* nl space* '-' { (* Like in the doc_bol production, these two productions exist only to deal properly with whitespace *) @@ -769,9 +782,16 @@ and doc_list_bol indents = parse backtrack_past_newline lexbuf; doc_list_bol indents lexbuf end - | Before -> Output.stop_item (); - backtrack_past_newline lexbuf; - doc_bol lexbuf + | Before -> + (* Here we were at the beginning of a line, and it was blank. + The next line started before any list items. So: insert + a paragraph for the empty line, rewind to whatever's just + after the newline, then toss over to doc_bol for whatever + comes next. *) + Output.stop_item (); + Output.paragraph (); + backtrack_past_newline lexbuf; + doc_bol lexbuf } | space* _ @@ -780,7 +800,10 @@ and doc_list_bol indents = parse | Before -> Output.stop_item (); backtrack lexbuf; doc_bol lexbuf | StartLevel n -> - Output.reach_item_level (n-1); + (if n = 1 then + Output.stop_item () + else + Output.reach_item_level (n-1)); backtrack lexbuf; doc (Some (take (n-1) indents)) lexbuf | InLevel (n,_) -> @@ -808,8 +831,11 @@ and doc indents = parse | Some ls -> doc_list_bol ls lexbuf | None -> doc_bol lexbuf else doc indents lexbuf)} + | "[[[" nl + { inf_rules indents lexbuf } | "[]" { Output.proofbox (); doc indents lexbuf } + | "{{" { url lexbuf; doc indents lexbuf } | "[" { if !Cdglobals.plain_comments then Output.char '[' else (brackets := 1; Output.start_inline_coq (); escaped_coq lexbuf; @@ -823,6 +849,18 @@ and doc indents = parse let eol = comment lexbuf in if eol then bol_parse lexbuf else doc indents lexbuf } + | '*'* "*)" space_nl* "(**" + {(match indents with + | Some _ -> Output.stop_item () + | None -> ()); + (* this says - if there is a blank line between the two comments, + insert one in the output too *) + let lines = List.length (Str.split_delim (Str.regexp "['\n']") + (lexeme lexbuf)) + in + if lines > 2 then Output.paragraph (); + doc_bol lexbuf + } | '*'* "*)" space* nl { true } | '*'* "*)" @@ -857,6 +895,15 @@ and doc indents = parse { if !Cdglobals.plain_comments then Output.char '_' else stop_emph () ; Output.char (lexeme_char lexbuf 1); doc indents lexbuf } + | "<<" space* + { Output.start_verbatim true; verbatim true lexbuf; doc_bol lexbuf } + | '"' + { if !Cdglobals.plain_comments + then Output.char '"' + else if in_quote () + then stop_quote () + else start_quote (); + doc indents lexbuf } | eof { false } | _ @@ -883,11 +930,22 @@ and escaped_html = parse | eof { () } | _ { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf } -and verbatim = parse - | nl ">>" space* nl { Output.verbatim_char '\n'; Output.stop_verbatim () } - | nl ">>" { Output.verbatim_char '\n'; Output.stop_verbatim () } - | eof { Output.stop_verbatim () } - | _ { Output.verbatim_char (lexeme_char lexbuf 0); verbatim lexbuf } +and verbatim inline = parse + | nl ">>" space* nl { Output.verbatim_char inline '\n'; Output.stop_verbatim inline } + | nl ">>" { Output.verbatim_char inline '\n'; Output.stop_verbatim inline } + | ">>" { Output.stop_verbatim inline } + | eof { Output.stop_verbatim inline } + | _ { Output.verbatim_char inline (lexeme_char lexbuf 0); verbatim inline lexbuf } + +and url = parse + | "}}" { Output.url (Buffer.contents url_buffer) None; Buffer.clear url_buffer } + | "}" { url_name lexbuf } + | _ { Buffer.add_char url_buffer (lexeme_char lexbuf 0); url lexbuf } + +and url_name = parse + | "}" { Output.url (Buffer.contents url_buffer) (Some (Buffer.contents url_name_buffer)); + Buffer.clear url_buffer; Buffer.clear url_name_buffer } + | _ { Buffer.add_char url_name_buffer (lexeme_char lexbuf 0); url_name lexbuf } (*s Coq, inside quotations *) @@ -911,10 +969,16 @@ and escaped_coq = parse { Tokens.flush_sublexer(); Output.ident (lexeme lexbuf) (lexeme_start lexbuf); escaped_coq lexbuf } - | space - { Tokens.flush_sublexer(); Output.char (lexeme_char lexbuf 0); - escaped_coq lexbuf } - | _ + | space_nl* + { let str = lexeme lexbuf in + Tokens.flush_sublexer(); + (if !Cdglobals.inline_notmono then () + else Output.end_inline_coq ()); + String.iter Output.char str; + (if !Cdglobals.inline_notmono then () + else Output.start_inline_coq ()); + escaped_coq lexbuf } + | _ { Output.sublexer (lexeme_char lexbuf 0) (lexeme_start lexbuf); escaped_coq lexbuf } @@ -1081,7 +1145,7 @@ and body = parse if eol then begin if not !Cdglobals.parse_comments then Output.line_break(); body_bol lexbuf end else body lexbuf } - | "where" space* + | "where" { Tokens.flush_sublexer(); Output.ident (lexeme lexbuf) (lexeme_start lexbuf); start_notation_string lexbuf } @@ -1105,6 +1169,8 @@ and body = parse body lexbuf } and start_notation_string = parse + | space { Tokens.flush_sublexer(); Output.char (lexeme_char lexbuf 0); + start_notation_string lexbuf } | '"' (* a true notation *) { Output.sublexer '"' (lexeme_start lexbuf); notation_string lexbuf; @@ -1141,6 +1207,71 @@ and printing_token_body = parse | _ { Buffer.add_string token_buffer (lexeme lexbuf); printing_token_body lexbuf } +(*s These handle inference rules, parsing the body segments of things + enclosed in [[[ ]]] brackets *) +and inf_rules indents = parse + | space* nl (* blank line, before or between definitions *) + { inf_rules indents lexbuf } + | "]]]" nl (* end of the inference rules block *) + { match indents with + | Some ls -> doc_list_bol ls lexbuf + | None -> doc_bol lexbuf } + | _ + { backtrack lexbuf; (* anything else must be the first line in a rule *) + inf_rules_assumptions indents [] lexbuf} + +(* The inference rule parsing just collects the inference rule and then + calls the output function once, instead of doing things incrementally + like the rest of the lexer. If only there were a real parsing phase... +*) +and inf_rules_assumptions indents assumptions = parse + | space* "---" '-'* [^ '\n']* nl (* hit the horizontal line *) + { let line = lexeme lexbuf in + let (spaces,_) = count_spaces line in + let dashes_and_name = + cut_head_tail_spaces (String.sub line 0 (String.length line - 1)) + in + let ldn = String.length dashes_and_name in + let (dashes,name) = + try (let i = String.index dashes_and_name ' ' in + let d = String.sub dashes_and_name 0 i in + let n = cut_head_tail_spaces + (String.sub dashes_and_name (i+1) (ldn-i-1)) + in + (d, Some n)) + with _ -> (dashes_and_name, None) + + in + inf_rules_conclusion indents (List.rev assumptions) + (spaces, dashes, name) [] lexbuf } + | [^ '\n']* nl (* if it's not the horizontal line, it's an assumption *) + { let line = lexeme lexbuf in + let (spaces,_) = count_spaces line in + let assumption = cut_head_tail_spaces + (String.sub line 0 (String.length line - 1)) + in + inf_rules_assumptions indents ((spaces,assumption)::assumptions) + lexbuf } + +(*s The conclusion is required to come immediately after the + horizontal bar. It is allowed to contain multiple lines of + text, like the assumptions. The conclusion ends when we spot a + blank line or a ']]]'. *) +and inf_rules_conclusion indents assumptions middle conclusions = parse + | space* nl | space* "]]]" nl (* end of conclusions. *) + { backtrack lexbuf; + Output.inf_rule assumptions middle (List.rev conclusions); + inf_rules indents lexbuf } + | space* [^ '\n']+ nl (* this is a line in the conclusion *) + { let line = lexeme lexbuf in + let (spaces,_) = count_spaces line in + let conc = cut_head_tail_spaces (String.sub line 0 + (String.length line - 1)) + in + inf_rules_conclusion indents assumptions middle + ((spaces,conc) :: conclusions) lexbuf + } + (*s A small scanner to support the chapter subtitle feature *) and st_start m = parse | "(*" "*"+ space+ "*" space+ diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml index a2cb995e..14447b06 100644 --- a/tools/coqdoc/index.ml +++ b/tools/coqdoc/index.ml @@ -1,14 +1,11 @@ -(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: index.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) - open Filename open Lexing open Printf @@ -38,17 +35,18 @@ type entry_type = type index_entry = | Def of string * entry_type | Ref of coq_module * string * entry_type - | Mod of coq_module * string 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 - inside comments, which are not globalized otherwise. *) - +(** [deftable] stores only definitions and is used to build the index *) let deftable = Hashtbl.create 97 +(** [byidtable] is used to interpolate idents inside comments, which are not + globalized otherwise. *) +let byidtable = Hashtbl.create 97 + (** [reftable] stores references and definitions *) let reftable = Hashtbl.create 97 @@ -62,25 +60,25 @@ let full_ident sp id = else "" let add_def loc1 loc2 ty sp id = + let fullid = full_ident sp id in + let def = Def (fullid, ty) in for loc = loc1 to loc2 do - Hashtbl.add reftable (!current_library, loc) (Def (full_ident sp id, ty)) + Hashtbl.add reftable (!current_library, loc) def done; - Hashtbl.add deftable id (Ref (!current_library, full_ident sp id, ty)) + Hashtbl.add deftable !current_library (fullid, ty); + Hashtbl.add byidtable id (!current_library, fullid, ty) let add_ref m loc m' sp id ty = + let fullid = full_ident sp id in if Hashtbl.mem reftable (m, loc) then () - else Hashtbl.add reftable (m, loc) (Ref (m', full_ident sp id, ty)); + else Hashtbl.add reftable (m, loc) (Ref (m', fullid, 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 = - Hashtbl.add reftable (m, loc) (Mod (m', id)); - Hashtbl.add deftable m (Mod (m', id)) + if Hashtbl.mem byidtable idx then () + else Hashtbl.add byidtable idx (m', fullid, ty) let find m l = Hashtbl.find reftable (m, l) -let find_string m s = Hashtbl.find deftable s +let find_string m s = let (m,s,t) = Hashtbl.find byidtable s in Ref (m,s,t) (*s Manipulating path prefixes *) @@ -238,18 +236,20 @@ let type_name = function let prepare_entry s = function | Notation -> (* We decode the encoding done in Dumpglob.cook_notation of coqtop *) - (* Encoded notations have the form section:sc:x_'++'_x where: *) - (* - the section, if any, ends with a "." *) - (* - the scope can be empty *) - (* - tokens are separated with "_" *) - (* - non-terminal symbols are conventionally represented by "x" *) - (* - terminals are enclosed within simple quotes *) - (* - existing simple quotes (that necessarily are parts of terminals) *) - (* are doubled *) + (* Encoded notations have the form section:sc:x_'++'_x where: *) + (* - the section, if any, ends with a "." *) + (* - the scope can be empty *) + (* - tokens are separated with "_" *) + (* - non-terminal symbols are conventionally represented by "x" *) + (* - terminals are enclosed within simple quotes *) + (* - existing simple quotes (that necessarily are parts of *) + (* terminals) are doubled *) (* (as a consequence, when a terminal contains "_" or "x", these *) (* necessarily appear enclosed within non-doubled simple quotes) *) - (* Example: "x ' %x _% y %'x %'_' z" is encoded as *) - (* "x_''''_'%x'_'_%'_x_'%''x'_'%''_'''_x" *) + (* - non-printable characters < 32 are left encoded so that they *) + (* are human-readable in index files *) + (* Example: "x ' %x _% y %'x %'_' z" is encoded as *) + (* "x_''''_'%x'_'_%'_x_'%''x'_'%''_'''_x" *) let err () = eprintf "Invalid notation in globalization file\n"; exit 1 in let h = try String.index_from s 0 ':' with _ -> err () in let i = try String.index_from s (h+1) ':' with _ -> err () in @@ -268,10 +268,10 @@ let prepare_entry s = function | _ -> assert false) end else - if s.[!j] = '\'' then begin - if (!j = l || s.[!j+1] <> '\'') then quoted := false - else (ntn.[!k] <- s.[!j]; incr k; incr j) - end else begin + if s.[!j] = '\'' then + if (!j = l || s.[!j+1] = '_') then quoted := false + else (incr j; ntn.[!k] <- s.[!j]; incr k) + else begin ntn.[!k] <- s.[!j]; incr k end; @@ -290,11 +290,8 @@ 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 - | Def (s,t) -> add_g s m t; add_bt t s m - | Ref _ | Mod _ -> () - in - Hashtbl.iter classify reftable; + let classify m (s,t) = (add_g s m t; add_bt t s m) in + Hashtbl.iter classify deftable; Hashtbl.iter (fun id m -> add_g id m Library; add_bt Library id m) modules; { idx_name = "global"; idx_entries = sort_entries !gl; @@ -324,8 +321,27 @@ let type_of_string = function | "sec" -> Section | s -> raise (Invalid_argument ("type_of_string:" ^ s)) -let read_glob f = +let ill_formed_glob_file f = + eprintf "Warning: ill-formed file %s (links will not be available)\n" f +let outdated_glob_file f = + eprintf "Warning: %s not consistent with corresponding .v file (links will not be available)\n" f + +let correct_file vfile f c = + let s = input_line c in + if String.length s < 7 || String.sub s 0 7 <> "DIGEST " then + (ill_formed_glob_file f; false) + else + let s = String.sub s 7 (String.length s - 7) in + match vfile, s with + | None, "NO" -> true + | Some _, "NO" -> ill_formed_glob_file f; false + | None, _ -> ill_formed_glob_file f; false + | Some vfile, s -> + s = Digest.to_hex (Digest.file vfile) || (outdated_glob_file f; false) + +let read_glob vfile f = let c = open_in f in + if correct_file vfile f c then let cur_mod = ref "" in try while true do @@ -341,7 +357,16 @@ let read_glob f = Scanf.sscanf s "R%d:%d %s %s %s %s" (fun loc1 loc2 lib_dp sp id ty -> for loc=loc1 to loc2 do - add_ref !cur_mod loc lib_dp sp id (type_of_string ty) + add_ref !cur_mod loc lib_dp sp id (type_of_string ty); + + (* Also add an entry for each module mentioned in [lib_dp], + * to use in interpolation. *) + ignore (List.fold_right (fun thisPiece priorPieces -> + let newPieces = match priorPieces with + | "" -> thisPiece + | _ -> thisPiece ^ "." ^ priorPieces in + add_ref !cur_mod loc "" "" newPieces Library; + newPieces) (Str.split (Str.regexp_string ".") lib_dp) "") done) with _ -> ()) | _ -> diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli index a009e9dc..0f62a086 100644 --- a/tools/coqdoc/index.mli +++ b/tools/coqdoc/index.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: index.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - open Cdglobals type loc = int @@ -36,10 +34,11 @@ val type_name : entry_type -> string type index_entry = | Def of string * entry_type | Ref of coq_module * string * entry_type - | Mod of coq_module * string +(* Find what symbol coqtop said is located at loc in the source file *) val find : coq_module -> loc -> index_entry +(* Find what data is referred to by some string in some coq module *) val find_string : coq_module -> string -> index_entry val add_module : coq_module -> unit @@ -54,7 +53,7 @@ val add_external_library : string -> coq_module -> unit (*s Read globalizations from a file (produced by coqc -dump-glob) *) -val read_glob : string -> unit +val read_glob : Digest.t option -> string -> unit (*s Indexes *) diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 23dadbc1..b33ec1f0 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -1,14 +1,11 @@ -(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: main.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) - (* Modified by Lionel Elie Mamane <lionel@mamane.lu> on 9 & 10 Mar 2004: * - handling of absolute filenames (function coq_module) * - coq_module: chop ./// (arbitrary amount of slashes), not only "./" @@ -53,6 +50,7 @@ let usage () = prerr_endline " -p <string> insert <string> in LaTeX preamble"; prerr_endline " --files-from <file> read file names to process in <file>"; prerr_endline " --glob-from <file> read globalization information from <file>"; + prerr_endline " --no-glob don't use any globalization information (no links will be inserted at identifiers)"; prerr_endline " --quiet quiet mode (default)"; prerr_endline " --verbose verbose mode"; prerr_endline " --no-externals no links to Coq standard library"; @@ -73,6 +71,7 @@ let usage () = prerr_endline " --no-lib-name don't display \"Library\" before library names in the toc"; prerr_endline " --lib-name <string> call top level toc entries <string> instead of \"Library\""; prerr_endline " --lib-subtitles first line comments of the form (** * ModuleName : text *) will be interpreted as subtitles"; + prerr_endline " --inline-notmono use a proportional width font for inline code (possibly with a different color)"; prerr_endline ""; exit 1 @@ -107,25 +106,6 @@ let check_if_file_exists f = end -(*s Manipulations of paths and path aliases *) - -let normalize_path p = - (* We use the Unix subsystem to normalize a physical path (relative - or absolute) and get rid of symbolic links, relative links (like - ./ or ../ in the middle of the path; it's tricky but it - works... *) - (* Rq: Sys.getcwd () returns paths without '/' at the end *) - let orig = Sys.getcwd () in - Sys.chdir p; - let res = Sys.getcwd () in - Sys.chdir orig; - res - -let normalize_filename f = - let basename = Filename.basename f in - let dirname = Filename.dirname f in - normalize_path dirname, basename - (* [paths] maps a physical path to a name *) let paths = ref [] @@ -303,6 +283,9 @@ let parse () = | ("-lib-subtitles" | "--lib-subtitles") :: rem -> Cdglobals.lib_subtitles := true; parse_rec rem + | ("-inline-notmono" | "--inline-notmono") :: rem -> + Cdglobals.inline_notmono := true; + parse_rec rem | ("-latin1" | "--latin1") :: rem -> Cdglobals.set_latin1 (); parse_rec rem @@ -341,6 +324,8 @@ let parse () = glob_source := GlobFile f; parse_rec rem | ("-glob-from" | "--glob-from") :: [] -> usage () + | ("-no-glob" | "--no-glob") :: rem -> + glob_source := NoGlob; parse_rec rem | ("--no-externals" | "-no-externals" | "-noexternals") :: rem -> Cdglobals.externals := false; parse_rec rem | ("--external" | "-external") :: u :: logicalpath :: rem -> @@ -350,7 +335,11 @@ let parse () = | ("--coqlib" | "-coqlib") :: [] -> usage () | ("--boot" | "-boot") :: rem -> - Cdglobals.coqlib_path := Coq_config.coqsrc; parse_rec rem + Cdglobals.coqlib_path := normalize_path ( + Filename.concat + (Filename.dirname Sys.executable_name) + Filename.parent_dir_name + ); parse_rec rem | ("--coqlib_path" | "-coqlib_path") :: d :: rem -> Cdglobals.coqlib_path := d; parse_rec rem | ("--coqlib_path" | "-coqlib_path") :: [] -> @@ -458,13 +447,13 @@ let gen_mult_files l = end (* Rq: pour latex et texmacs, une toc ou un index séparé n'a pas de sens... *) -let read_glob_file x = - try Index.read_glob x - with Sys_error s -> - eprintf "Warning: %s (links will not be available)\n" s +let read_glob_file vfile f = + try Index.read_glob vfile f + with Sys_error s -> eprintf "Warning: %s (links will not be available)\n" s let read_glob_file_of = function - | Vernac_file (f,_) -> read_glob_file (Filename.chop_extension f ^ ".glob") + | Vernac_file (f,_) -> + read_glob_file (Some f) (Filename.chop_extension f ^ ".glob") | Latex_file _ -> () let index_module = function @@ -486,7 +475,7 @@ let produce_document l = (match !Cdglobals.glob_source with | NoGlob -> () | DotGlob -> List.iter read_glob_file_of l - | GlobFile f -> read_glob_file f); + | GlobFile f -> read_glob_file None f); List.iter index_module l; match !out_to with | StdOut -> diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index eefcfd11..0dc86bc8 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -1,14 +1,11 @@ -(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: output.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) - open Cdglobals open Index @@ -32,24 +29,27 @@ let build_table l = let is_keyword = build_table - [ "AddPath"; "Axiom"; "Abort"; "Boxed"; "Chapter"; "Check"; "Coercion"; "CoFixpoint"; + [ "About"; "AddPath"; "Axiom"; "Abort"; "Chapter"; "Check"; "Coercion"; "Compute"; "CoFixpoint"; "CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example"; - "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint"; + "Export"; "Fact"; "Fix"; "Fixpoint"; "Function"; "Generalizable"; "Global"; "Grammar"; + "Guarded"; "Goal"; "Hint"; "Debug"; "On"; "Hypothesis"; "Hypotheses"; - "Resolve"; "Unfold"; "Immediate"; "Extern"; "Implicit"; "Import"; "Inductive"; + "Resolve"; "Unfold"; "Immediate"; "Extern"; "Constructors"; "Rewrite"; + "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"; + "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"; "Set"; "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context"; "Notation"; "Reserved Notation"; "Tactic Notation"; - "Delimit"; "Bind"; "Open"; "Scope"; - "Boxed"; "Unboxed"; "Inline"; + "Delimit"; "Bind"; "Open"; "Scope"; "Inline"; "Implicit Arguments"; "Add"; "Strict"; "Typeclasses"; "Instance"; "Global Instance"; "Class"; "Instantiation"; - "subgoal"; - "Opaque"; "Transparent"; + "subgoal"; "subgoals"; "vm_compute"; + "Opaque"; "Transparent"; "Time"; + "Extraction"; "Extract"; (* Program *) "Program Definition"; "Program Example"; "Program Fixpoint"; "Program Lemma"; "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next"; @@ -57,14 +57,20 @@ let is_keyword = (*i (* coq terms *) *) "forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let"; "fun"; "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"; "struct"; "wf"; "measure"; + "fix"; "cofix"; (* Ltac *) - "before"; "after" + "before"; "after"; "constr"; "ltac"; "goal"; "context"; "beta"; "delta"; "iota"; "zeta"; + (* Notations *) + "level"; "associativity"; "no" ] let is_tactic = build_table [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection"; - "elimtype"; "progress"; "setoid_rewrite"; + "elimtype"; "progress"; "setoid_rewrite"; "left"; "right"; "constructor"; + "econstructor"; "decide equality"; "abstract"; "exists"; "cbv"; "simple destruct"; + "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instanciate"; + "quote"; "eexact"; "autorewrite"; "destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality"; "f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega"; "set"; "assert"; "do"; "repeat"; @@ -73,8 +79,10 @@ let is_tactic = "reflexivity"; "symmetry"; "transitivity"; "replace"; "setoid_replace"; "inversion"; "inversion_clear"; "pattern"; "intuition"; "congruence"; "fail"; "fresh"; - "trivial"; "exact"; "tauto"; "firstorder"; "ring"; - "clapply"; "program_simpl"; "program_simplify"; "eapply"; "auto"; "eauto" ] + "trivial"; "tauto"; "firstorder"; "ring"; + "clapply"; "program_simpl"; "program_simplify"; "eapply"; "auto"; "eauto"; + "change"; "fold"; "hnf"; "lazy"; "simple"; "eexists"; "debug"; "idtac"; "first"; "type of"; "pose"; + "eval"; "instantiate"; "until" ] (*s Current Coq module *) @@ -118,9 +126,12 @@ let initialize_texmacs () = let token_tree_texmacs = ref (initialize_texmacs ()) +let token_tree_latex = ref Tokens.empty_ttree +let token_tree_html = ref Tokens.empty_ttree + let initialize_tex_html () = let if_utf8 = if !Cdglobals.utf8 then fun x -> Some x else fun _ -> None in - List.fold_right (fun (s,l,l') (tt,tt') -> + let (tree_latex, tree_html) = List.fold_right (fun (s,l,l') (tt,tt') -> (Tokens.ttree_add tt s l, match l' with None -> tt' | Some l' -> Tokens.ttree_add tt' s l')) [ "*" , "\\ensuremath{\\times}", if_utf8 "×"; @@ -143,10 +154,9 @@ let initialize_tex_html () = "Î ", "\\ensuremath{\\Pi}", if_utf8 "Î "; "λ", "\\ensuremath{\\lambda}", if_utf8 "λ"; (* "fun", "\\ensuremath{\\lambda}" ? *) - ] (Tokens.empty_ttree,Tokens.empty_ttree) - -let token_tree_latex = ref (fst (initialize_tex_html ())) -let token_tree_html = ref (snd (initialize_tex_html ())) + ] (Tokens.empty_ttree,Tokens.empty_ttree) in + token_tree_latex := tree_latex; + token_tree_html := tree_html let add_printing_token s (t1,t2) = (match t1 with None -> () | Some t1 -> @@ -182,10 +192,20 @@ module Latex = struct let push_in_preamble s = Queue.add s preamble + let utf8x_extra_support () = + printf "\n"; + printf "%%Warning: tipa declares many non-standard macros used by utf8x to\n"; + printf "%%interpret utf8 characters but extra packages might have to be added\n"; + printf "%%(e.g. \"textgreek\" for Greek letters not already in tipa).\n"; + printf "%%Use coqdoc's option -p to add new packages.\n"; + printf "\\usepackage{tipa}\n"; + printf "\n" + let header () = if !header_trailer then begin printf "\\documentclass[12pt]{report}\n"; if !inputenc != "" then printf "\\usepackage[%s]{inputenc}\n" !inputenc; + if !inputenc = "utf8x" then utf8x_extra_support (); printf "\\usepackage[T1]{fontenc}\n"; printf "\\usepackage{fullpage}\n"; printf "\\usepackage{coqdoc}\n"; @@ -255,6 +275,12 @@ module Latex = struct | '^' | '~' as c -> Buffer.add_char buff '\\'; Buffer.add_char buff c; Buffer.add_string buff "{}" + | '\'' -> + if i < String.length s - 1 && s.[i+1] = '\'' then begin + Buffer.add_char buff '\''; Buffer.add_char buff '{'; + Buffer.add_char buff '}' + end else + Buffer.add_char buff '\'' | c -> Buffer.add_char buff c done; @@ -276,9 +302,23 @@ module Latex = struct let stop_latex_math () = output_char '$' - let start_verbatim () = printf "\\begin{verbatim}" + let start_quote () = output_char '`'; output_char '`' + let stop_quote () = output_char '\''; output_char '\'' + + let start_verbatim inline = + if inline then printf "\\texttt{" + else printf "\\begin{verbatim}" - let stop_verbatim () = printf "\\end{verbatim}\n" + let stop_verbatim inline = + if inline then printf "}" + else printf "\\end{verbatim}\n" + + let url addr name = + printf "%s\\footnote{\\url{%s}}" + (match name with + | None -> "" + | Some n -> n) + addr let indentation n = if n == 0 then @@ -287,9 +327,6 @@ module Latex = struct let space = 0.5 *. (float n) in printf "\\coqdocindent{%2.2fem}\n" space - let module_ref m s = - printf "\\coqdocmodule{%s}{%s}" m (escaped s) - let ident_ref m fid typ s = let id = if fid <> "" then (m ^ "." ^ fid) else m in match find_module m with @@ -306,18 +343,20 @@ module Latex = struct printf "\\coqdoc%s{%s}" (type_name typ) s let defref m id ty s = - printf "\\coqdef{"; label_ident (m ^ "." ^ id); - printf "}{%s}{\\coqdoc%s{%s}}" s (type_name ty) s + if ty <> Notation then + (printf "\\coqdef{"; label_ident (m ^ "." ^ id); + printf "}{%s}{\\coqdoc%s{%s}}" s (type_name ty) s) + else + (* Glob file still not able to say the exact extent of the definition *) + (* so we currently renounce to highlight the notation location *) + (printf "\\coqdef{"; label_ident (m ^ "." ^ id); + printf "}{%s}{%s}" s s) let reference s = function | Def (fullid,typ) -> defref (get_module false) 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 "\\coqdocvar{%s}" (escaped s) (*s The sublexer buffers symbol characters and attached uninterpreted ident and try to apply special translation such as, @@ -330,13 +369,22 @@ module Latex = struct | Some ref -> reference s ref | None -> if issymbchar then output_string s else printf "\\coqdocvar{%s}" s + let last_was_in = ref false + let sublexer c loc = - let tag = - try Some (Index.find (get_module false) loc) with Not_found -> None - in - Tokens.output_tagged_symbol_char tag c + if c = '*' && !last_was_in then begin + Tokens.flush_sublexer (); + output_char '*' + end else begin + let tag = + try Some (Index.find (get_module false) loc) with Not_found -> None + in + Tokens.output_tagged_symbol_char tag c + end; + last_was_in := false let initialize () = + initialize_tex_html (); Tokens.token_tree := token_tree_latex; Tokens.outfun := output_sublexer_string @@ -345,7 +393,11 @@ module Latex = struct let translate s = match Tokens.translate s with Some s -> s | None -> escaped s + let keyword s loc = + printf "\\coqdockw{%s}" (translate s) + let ident s loc = + last_was_in := s = "in"; try let tag = Index.find (get_module false) loc in reference (translate s) tag @@ -478,8 +530,7 @@ module Html = struct end let trailer () = - if !header_trailer then - if !footer_file_spec then + if !header_trailer && !footer_file_spec then let cin = Pervasives.open_in !footer_file in try while true do @@ -487,14 +538,14 @@ module Html = struct printf "%s\n" s done with End_of_file -> Pervasives.close_in cin - else - begin - if !index && (get_module false) <> "Index" then - printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"%s.html\">Index</a>" !index_name; - printf "<hr/>This page has been generated by "; - printf "<a href=\"%s\">coqdoc</a>\n" Coq_config.wwwcoq; - printf "</div>\n\n</div>\n\n</body>\n</html>" - end + else + begin + if !index && (get_module false) <> "Index" then + printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"%s.html\">Index</a>" !index_name; + printf "<hr/>This page has been generated by "; + printf "<a href=\"%s\">coqdoc</a>\n" Coq_config.wwwcoq; + printf "</div>\n\n</div>\n\n</body>\n</html>" + end let start_module () = let ln = !lib_name in @@ -547,17 +598,22 @@ module Html = struct let start_latex_math () = () let stop_latex_math () = () - let start_verbatim () = printf "<pre>" - let stop_verbatim () = printf "</pre>\n" + let start_quote () = char '"' + let stop_quote () = start_quote () - let module_ref m s = - match find_module m with - | Local -> - printf "<a class=\"modref\" href=\"%s.html\">%s</a>" m s - | External m when !externals -> - printf "<a class=\"modref\" href=\"%s.html\">%s</a>" m s - | External _ | Unknown -> - output_string s + let start_verbatim inline = + if inline then printf "<tt>" + else printf "<pre>" + + let stop_verbatim inline = + if inline then printf "</tt>" + else printf "</pre>\n" + + let url addr name = + printf "<a href=\"%s\">%s</a>" addr + (match name with + | Some n -> n + | None -> addr) let ident_ref m fid typ s = match find_module m with @@ -575,12 +631,8 @@ module Html = struct | Def (fullid,ty) -> printf "<a name=\"%s\">" fullid; printf "<span class=\"id\" type=\"%s\">%s</span></a>" (type_name ty) s - | Mod (m,s') when s = s' -> - module_ref m s | Ref (m,fullid,ty) -> ident_ref m fullid (type_name ty) s - | Mod _ -> - printf "<span class=\"id\" type=\"mod\">%s</span>" s let output_sublexer_string doescape issymbchar tag s = let s = if doescape then escaped s else s in @@ -597,12 +649,16 @@ module Html = struct Tokens.output_tagged_symbol_char tag c let initialize () = + initialize_tex_html(); Tokens.token_tree := token_tree_html; Tokens.outfun := output_sublexer_string let translate s = 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) + let ident s loc = if is_keyword s then begin printf "<span class=\"id\" type=\"keyword\">%s</span>" (translate s) @@ -624,7 +680,7 @@ module Html = struct let rec reach_item_level n = if !item_level < n then begin - printf "<ul>\n<li>"; incr item_level; + printf "<ul class=\"doclist\">\n<li>"; incr item_level; reach_item_level n end else if !item_level > n then begin printf "\n</li>\n</ul>\n"; decr item_level; @@ -662,7 +718,9 @@ module Html = struct let end_code () = end_coq (); start_doc () - let start_inline_coq () = printf "<span class=\"inlinecode\">" + let start_inline_coq () = + if !inline_notmono then printf "<span class=\"inlinecodenm\">" + else printf "<span class=\"inlinecode\">" let end_inline_coq () = printf "</span>" @@ -670,7 +728,50 @@ module Html = struct let end_inline_coq_block () = end_inline_coq () - let paragraph () = printf "\n<br/> <br/>\n" + let paragraph () = printf "\n<div class=\"paragraph\"> </div>\n\n" + + (* inference rules *) + let inf_rule assumptions (_,_,midnm) conclusions = + (* this first function replaces any occurance of 3 or more spaces + in a row with " "s. We do this to the assumptions so that + people can put multiple rules on a line with nice formatting *) + let replace_spaces str = + let rec copy a n = match n with 0 -> [] | n -> (a :: copy a (n - 1)) in + let results = Str.full_split (Str.regexp "[' '][' '][' ']+") str in + let strs = List.map (fun r -> match r with + | Str.Text s -> [s] + | Str.Delim s -> + copy " " (String.length s)) + results + in + String.concat "" (List.concat strs) + in + let start_assumption line = + (printf "<tr class=\"infruleassumption\">\n"; + printf " <td class=\"infrule\">%s</td>\n" (replace_spaces line)) in + let end_assumption () = + (printf " <td></td>\n"; + printf "</td>\n") in + let rec print_assumptions hyps = + match hyps with + | [] -> start_assumption " " + | [(_,hyp)] -> start_assumption hyp + | ((_,hyp) :: hyps') -> (start_assumption hyp; + end_assumption (); + print_assumptions hyps') in + printf "<center><table class=\"infrule\">\n"; + print_assumptions assumptions; + printf " <td class=\"infrulenamecol\" rowspan=\"3\">\n"; + (match midnm with + | None -> printf " \n </td>" + | Some s -> printf " %s \n </td>" s); + printf "</tr>\n"; + printf "<tr class=\"infrulemiddle\">\n"; + printf " <td class=\"infrule\"><hr /></td>\n"; + printf "</tr>\n"; + print_assumptions conclusions; + end_assumption (); + printf "</table></center>" let section lev f = let lab = new_label () in @@ -858,19 +959,28 @@ module TeXmacs = struct let stop_latex_math () = output_char '>' - let start_verbatim () = in_doc := true; printf "<\\verbatim>" + let start_verbatim inline = in_doc := true; printf "<\\verbatim>" + let stop_verbatim inline = in_doc := false; printf "</verbatim>" + + let url addr name = + printf "%s<\\footnote><\\url>%s</url></footnote>" addr + (match name with + | None -> "" + | Some n -> n) - let stop_verbatim () = in_doc := false; printf "</verbatim>" + let start_quote () = output_char '`'; output_char '`' + let stop_quote () = output_char '\''; output_char '\'' let indentation n = () + let keyword s = + printf "<kw|"; raw_ident s; printf ">" + let ident_true s = - if is_keyword s then begin - printf "<kw|"; raw_ident s; printf ">" - end else begin - raw_ident s - end + if is_keyword s then keyword s + else raw_ident s + let keyword s loc = keyword s let ident s _ = if !in_doc then ident_true s else raw_ident s let output_sublexer_string doescape issymbchar tag s = @@ -985,13 +1095,21 @@ module Raw = struct let start_latex_math () = () let stop_latex_math () = () - let start_verbatim () = () + let start_verbatim inline = () + let stop_verbatim inline = () - let stop_verbatim () = () + let url addr name = + match name with + | Some n -> printf "%s (%s)" n addr + | None -> printf "%s" addr + + let start_quote () = printf "\"" + let stop_quote () = printf "\"" let indentation n = 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 @@ -1105,6 +1223,7 @@ let rule = select Latex.rule Html.rule TeXmacs.rule Raw.rule let nbsp = select Latex.nbsp Html.nbsp TeXmacs.nbsp Raw.nbsp 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 initialize = select Latex.initialize Html.initialize TeXmacs.initialize Raw.initialize @@ -1132,10 +1251,33 @@ let start_verbatim = select Latex.start_verbatim Html.start_verbatim TeXmacs.start_verbatim Raw.start_verbatim let stop_verbatim = select Latex.stop_verbatim Html.stop_verbatim TeXmacs.stop_verbatim Raw.stop_verbatim -let verbatim_char = - select output_char Html.char TeXmacs.char Raw.char +let verbatim_char inline = + select (if inline then Latex.char else output_char) Html.char TeXmacs.char Raw.char let hard_verbatim_char = output_char +let url = + select Latex.url Html.url TeXmacs.url Raw.url + +let start_quote = + select Latex.start_quote Html.start_quote TeXmacs.start_quote Raw.start_quote +let stop_quote = + select Latex.stop_quote Html.stop_quote TeXmacs.stop_quote Raw.stop_quote + +let inf_rule_dumb assumptions (midsp,midln,midnm) conclusions = + start_verbatim false; + let dumb_line = + function (sp,ln) -> (String.iter char ((String.make sp ' ') ^ ln); + char '\n') + in + (List.iter dumb_line assumptions; + dumb_line (midsp, midln ^ (match midnm with + | Some s -> " " ^ s + | None -> "")); + List.iter dumb_line conclusions); + stop_verbatim false + +let inf_rule = select inf_rule_dumb Html.inf_rule inf_rule_dumb inf_rule_dumb + let make_multi_index = select Latex.make_multi_index Html.make_multi_index TeXmacs.make_multi_index Raw.make_multi_index let make_index = select Latex.make_index Html.make_index TeXmacs.make_index Raw.make_index let make_toc = select Latex.make_toc Html.make_toc TeXmacs.make_toc Raw.make_toc diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli index dcd9072d..80f39011 100644 --- a/tools/coqdoc/output.mli +++ b/tools/coqdoc/output.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: output.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - open Cdglobals open Index @@ -62,6 +60,7 @@ val rule : unit -> unit val nbsp : unit -> unit val char : char -> unit +val keyword : string -> loc -> unit val ident : string -> loc -> unit val sublexer : char -> loc -> unit val initialize : unit -> unit @@ -72,13 +71,34 @@ val latex_char : char -> unit val latex_string : string -> unit val html_char : char -> unit val html_string : string -> unit -val verbatim_char : char -> unit +val verbatim_char : bool -> char -> unit val hard_verbatim_char : char -> unit val start_latex_math : unit -> unit val stop_latex_math : unit -> unit -val start_verbatim : unit -> unit -val stop_verbatim : unit -> unit +val start_verbatim : bool -> unit +val stop_verbatim : bool -> unit +val start_quote : unit -> unit +val stop_quote : unit -> unit + +val url : string -> string option -> unit + +(* this outputs an inference rule in one go. You pass it the list of + assumptions, then the middle line info, then the conclusion (which + is allowed to span multiple lines). + + In each case, the int is the number of spaces before the start of + the line's text and the string is the text of the line with the + leading trailing space trimmed. For the middle rule, you can + also optionally provide a name. + + We need the space info so that in modes where we aren't doing + something smart we can just format the rule verbatim like the user did +*) +val inf_rule : (int * string) list + -> (int * string * (string option)) + -> (int * string) list + -> unit val make_multi_index : unit -> unit val make_index : unit -> unit diff --git a/tools/coqdoc/tokens.ml b/tools/coqdoc/tokens.ml index 9de39083..10a105f9 100644 --- a/tools/coqdoc/tokens.ml +++ b/tools/coqdoc/tokens.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/tools/coqdoc/tokens.mli b/tools/coqdoc/tokens.mli index 3b756e18..e9c74307 100644 --- a/tools/coqdoc/tokens.mli +++ b/tools/coqdoc/tokens.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |