summaryrefslogtreecommitdiff
path: root/tools/coqdoc
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coqdoc')
-rw-r--r--tools/coqdoc/alpha.ml19
-rw-r--r--tools/coqdoc/alpha.mli2
-rw-r--r--tools/coqdoc/cdglobals.ml22
-rw-r--r--tools/coqdoc/coqdoc.css129
-rw-r--r--tools/coqdoc/coqdoc.sty78
-rw-r--r--tools/coqdoc/cpretty.mli (renamed from tools/coqdoc/pretty.mli)3
-rw-r--r--tools/coqdoc/cpretty.mll1176
-rw-r--r--tools/coqdoc/index.ml335
-rw-r--r--tools/coqdoc/index.mli22
-rw-r--r--tools/coqdoc/index.mll490
-rw-r--r--tools/coqdoc/main.ml280
-rw-r--r--tools/coqdoc/output.ml759
-rw-r--r--tools/coqdoc/output.mli19
-rw-r--r--tools/coqdoc/pretty.mll784
-rw-r--r--tools/coqdoc/tokens.ml171
-rw-r--r--tools/coqdoc/tokens.mli78
16 files changed, 2578 insertions, 1789 deletions
diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml
index b1a46bae..d25034f2 100644
--- a/tools/coqdoc/alpha.ml
+++ b/tools/coqdoc/alpha.ml
@@ -6,9 +6,11 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: alpha.ml 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id$ i*)
-let norm_char c = match Char.uppercase c with
+open Cdglobals
+
+let norm_char_latin1 c = match Char.uppercase c with
| '\192'..'\198' -> 'A'
| '\199' -> 'C'
| '\200'..'\203' -> 'E'
@@ -19,6 +21,13 @@ let norm_char c = match Char.uppercase c with
| '\221' -> 'Y'
| c -> c
+let norm_char_utf8 c = Char.uppercase c
+
+let norm_char c =
+ if !utf8 then norm_char_utf8 c else
+ if !latin1 then norm_char_latin1 c else
+ Char.uppercase c
+
let norm_string s =
let u = String.copy s in
for i = 0 to String.length s - 1 do
@@ -30,12 +39,14 @@ let compare_char c1 c2 = match norm_char c1, norm_char c2 with
| ('A'..'Z' as c1), ('A'..'Z' as c2) -> compare c1 c2
| 'A'..'Z', _ -> -1
| _, 'A'..'Z' -> 1
+ | '_', _ -> -1
+ | _, '_' -> 1
| c1, c2 -> compare c1 c2
-let compare_string s1 s2 =
+let compare_string s1 s2 =
let n1 = String.length s1 in
let n2 = String.length s2 in
- let rec cmp i =
+ let rec cmp i =
if i == n1 || i == n2 then
n1 - n2
else
diff --git a/tools/coqdoc/alpha.mli b/tools/coqdoc/alpha.mli
index d3c26537..922a10d6 100644
--- a/tools/coqdoc/alpha.mli
+++ b/tools/coqdoc/alpha.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: alpha.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id$ i*)
(* Alphabetic order. *)
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index b3f0739d..b2e23657 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -25,9 +25,19 @@ let out_to = ref MultFiles
let out_channel = ref stdout
+let coqdoc_out f =
+ if !output_dir <> "" && Filename.is_relative f then
+ if not (Sys.file_exists !output_dir) then
+ (Printf.eprintf "No such directory: %s\n" !output_dir; exit 1)
+ else
+ Filename.concat !output_dir f
+ else
+ f
+
let open_out_file f =
- let f = if !output_dir <> "" && Filename.is_relative f then Filename.concat !output_dir f else f in
- out_channel := open_out f
+ out_channel :=
+ try open_out (coqdoc_out f)
+ with Sys_error s -> Printf.eprintf "%s\n" s; exit 1
let close_out_file () = close_out !out_channel
@@ -37,7 +47,7 @@ type glob_source_t =
| DotGlob
| GlobFile of string
-let glob_source = ref DotGlob
+let glob_source = ref DotGlob
let header_trailer = ref true
let header_file = ref ""
@@ -50,6 +60,7 @@ let gallina = ref false
let short = ref false
let index = ref true
let multi_index = ref false
+let index_name = ref "index"
let toc = ref false
let page_title = ref ""
let title = ref ""
@@ -58,6 +69,10 @@ let coqlib = ref Coq_config.wwwstdlib
let coqlib_path = ref Coq_config.coqlib
let raw_comments = ref false
let parse_comments = ref false
+let plain_comments = ref false
+let toc_depth = (ref None : int option ref)
+let lib_name = ref "Library"
+let lib_subtitles = ref false
let interpolate = ref false
let charset = ref "iso-8859-1"
@@ -82,4 +97,3 @@ type coq_module = string
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 762be5af..24b514b7 100644
--- a/tools/coqdoc/coqdoc.css
+++ b/tools/coqdoc/coqdoc.css
@@ -19,14 +19,16 @@ body { padding: 0px 0px;
margin: 0;}
-/* Contenu */
+/* Contents */
#main{ display: block;
padding: 10px;
- overflow: hidden;
+ font-family: sans-serif;
font-size: 100%;
line-height: 100% }
+#main h1 { line-height: 95% } /* allow for multi-line headers */
+
#main a.idref:visited {color : #416DFF; text-decoration : none; }
#main a.idref:link {color : #416DFF; text-decoration : none; }
#main a.idref:hover {text-decoration : none; }
@@ -40,41 +42,93 @@ body { padding: 0px 0px;
#main .keyword { color : #cf1d1d }
#main { color: black }
-#main .section { background-color:#90bdff;
- font-size : 175% }
+.section { background-color: rgb(60%,60%,100%);
+ padding-top: 13px;
+ padding-bottom: 13px;
+ padding-left: 3px;
+ margin-top: 5px;
+ margin-bottom: 5px;
+ font-size : 175% }
+
+h2.section { background-color: rgb(80%,80%,100%);
+ padding-left: 3px;
+ padding-top: 12px;
+ padding-bottom: 10px;
+ font-size : 130% }
+
+h3.section { background-color: rgb(90%,90%,100%);
+ padding-left: 3px;
+ padding-top: 7px;
+ padding-bottom: 7px;
+ font-size : 115% }
+
+h4.section {
+/*
+ background-color: rgb(80%,80%,80%);
+ max-width: 20em;
+ padding-left: 5px;
+ padding-top: 5px;
+ padding-bottom: 5px;
+*/
+ background-color: white;
+ padding-left: 0px;
+ padding-top: 0px;
+ padding-bottom: 0px;
+ font-size : 100%;
+ font-style : bold;
+ text-decoration : underline;
+ }
#main .doc { margin: 0px;
- padding: 10px;
font-family: sans-serif;
font-size: 100%;
- line-height: 100%;
- font-weight:bold;
+ line-height: 125%;
+ max-width: 40em;
color: black;
+ padding: 10px;
background-color: #90bdff;
border-style: plain}
.inlinecode {
display: inline;
+/* font-size: 125%; */
+ color: #666666;
+ font-family: monospace }
+
+.doc .inlinecode {
+ display: inline;
+ font-size: 120%;
+ color: rgb(30%,30%,70%);
+ font-family: monospace }
+
+.doc .inlinecode .id {
+ color: rgb(30%,30%,70%);
+}
+
+.doc .code {
+ display: inline;
+ font-size: 120%;
+ color: rgb(30%,30%,70%);
font-family: monospace }
.comment {
display: inline;
font-family: monospace;
- color: red; }
+ color: rgb(50%,50%,80%);
+}
.code {
display: block;
- font-family: monospace }
+/* padding-left: 15px; */
+ font-size: 110%;
+ font-family: monospace;
+ }
/* Pied de page */
#footer { font-size: 65%;
font-family: sans-serif; }
-#footer a:visited { color: blue; }
-#footer a:link { text-decoration: none;
- color: #888888; }
-
.id { display: inline; }
.id[type="constructor"] {
@@ -129,3 +183,52 @@ body { padding: 0px 0px;
color : #cf1d1d;
/* color: black; */
}
+
+.inlinecode .id {
+ color: rgb(0%,0%,0%);
+}
+
+
+/* TOC */
+
+#toc h2 {
+ padding: 10px;
+ background-color: rgb(60%,60%,100%);
+}
+
+#toc li {
+ padding-bottom: 8px;
+}
+
+/* Index */
+
+#index {
+ margin: 0;
+ padding: 0;
+ width: 100%;
+}
+
+#index #frontispiece {
+ margin: 1em auto;
+ padding: 1em;
+ width: 60%;
+}
+
+.booktitle { font-size : 140% }
+.authors { font-size : 90%;
+ line-height: 115%; }
+.moreauthors { font-size : 60% }
+
+#index #entrance {
+ text-align: center;
+}
+
+#index #entrance .spacer {
+ margin: 0 30px 0 30px;
+}
+
+#index #footer {
+ position: absolute;
+ bottom: 0;
+ text-align: bottom;
+} \ No newline at end of file
diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty
index fca9a1d7..4314d07d 100644
--- a/tools/coqdoc/coqdoc.sty
+++ b/tools/coqdoc/coqdoc.sty
@@ -65,6 +65,25 @@
% macro for typesetting tactic identifiers
\newcommand{\coqdoctac}[1]{\texttt{#1}}
+% These are the real macros used by coqdoc, their typesetting is
+% based on the above macros by default.
+
+\newcommand{\coqdoclibrary}[1]{\coqdoccst{#1}}
+\newcommand{\coqdocinductive}[1]{\coqdocind{#1}}
+\newcommand{\coqdocdefinition}[1]{\coqdoccst{#1}}
+\newcommand{\coqdocvariable}[1]{\coqdocvar{#1}}
+\newcommand{\coqdocconstructor}[1]{\coqdocconstr{#1}}
+\newcommand{\coqdoclemma}[1]{\coqdoccst{#1}}
+\newcommand{\coqdocclass}[1]{\coqdocind{#1}}
+\newcommand{\coqdocinstance}[1]{\coqdoccst{#1}}
+\newcommand{\coqdocmethod}[1]{\coqdoccst{#1}}
+\newcommand{\coqdocabbreviation}[1]{\coqdoccst{#1}}
+\newcommand{\coqdocrecord}[1]{\coqdocind{#1}}
+\newcommand{\coqdocprojection}[1]{\coqdoccst{#1}}
+\newcommand{\coqdocnotation}[1]{\coqdockw{#1}}
+\newcommand{\coqdocsection}[1]{\coqdoccst{#1}}
+\newcommand{\coqdocaxiom}[1]{\coqdocax{#1}}
+\newcommand{\coqdocmoduleid}[1]{\coqdocmod{#1}}
% Environment encompassing code fragments
% !!! CAUTION: This environment may have empty contents
@@ -102,15 +121,18 @@
\newcommand{\coqdef}[3]{\phantomsection\hypertarget{coq:#1}{#3}}
\newcommand{\coqref}[2]{\hyperlink{coq:#1}{#2}}
+ \newcommand{\coqexternalref}[3]{\href{#1.html\##2}{#3}}
+
\newcommand{\identref}[2]{\hyperlink{coq:#1}{\textsf {#2}}}
- \newcommand{\coqlibrary}[2]{\cleardoublepage\phantomsection
- \hypertarget{coq:#1}{\chapter{Library \texorpdfstring{\coqdoccst}{}{#2}}}}
+ \newcommand{\coqlibrary}[3]{\cleardoublepage\phantomsection
+ \hypertarget{coq:#1}{\chapter{#2\texorpdfstring{\coqdoccst}{}{#3}}}}
\else
\newcommand{\coqdef}[3]{#3}
\newcommand{\coqref}[2]{#2}
+ \newcommand{\coqexternalref}[3]{#3}
\newcommand{\texorpdfstring}[2]{#1}
\newcommand{\identref}[2]{\textsf{#2}}
- \newcommand{\coqlibrary}[2]{\cleardoublepage\chapter{Library \coqdoccst{#2}}}
+ \newcommand{\coqlibrary}[3]{\cleardoublepage\chapter{#2\coqdoccst{#3}}}
\fi
\usepackage{xr}
@@ -147,54 +169,4 @@
\def\coqdoctac#1{{\color{\coqdoctaccolor}{\texttt{#1}}}}
\fi
-\newcommand{\coqdefinition}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
-\newcommand{\coqdefinitionref}[2]{\coqref{#1}{\coqdoccst{#2}}}
-
-\newcommand{\coqvariable}[2]{\coqdocvar{#2}}
-\newcommand{\coqvariableref}[2]{\coqref{#1}{\coqdocvar{#2}}}
-
-\newcommand{\coqinductive}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}}
-\newcommand{\coqinductiveref}[2]{\coqref{#1}{\coqdocind{#2}}}
-
-\newcommand{\coqconstructor}[2]{\coqdef{#1}{#2}{\coqdocconstr{#2}}}
-\newcommand{\coqconstructorref}[2]{\coqref{#1}{\coqdocconstr{#2}}}
-
-\newcommand{\coqlemma}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
-\newcommand{\coqlemmaref}[2]{\coqref{#1}{\coqdoccst{#2}}}
-
-\newcommand{\coqclass}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}}
-\newcommand{\coqclassref}[2]{\coqref{#1}{\coqdocind{#2}}}
-
-\newcommand{\coqinstance}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
-\newcommand{\coqinstanceref}[2]{\coqref{#1}{\coqdoccst{#2}}}
-
-\newcommand{\coqmethod}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
-\newcommand{\coqmethodref}[2]{\coqref{#1}{\coqdoccst{#2}}}
-
-\newcommand{\coqabbreviation}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
-\newcommand{\coqabbreviationref}[2]{\coqref{#1}{\coqdoccst{#2}}}
-
-\newcommand{\coqrecord}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}}
-\newcommand{\coqrecordref}[2]{\coqref{#1}{\coqdocind{#2}}}
-
-\newcommand{\coqprojection}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
-\newcommand{\coqprojectionref}[2]{\coqref{#1}{\coqdoccst{#2}}}
-
-\newcommand{\coqnotationref}[2]{\coqref{#1}{\coqdockw{#2}}}
-
-\newcommand{\coqsection}[2]{\coqdef{sec:#1}{#2}{\coqdoccst{#2}}}
-\newcommand{\coqsectionref}[2]{\coqref{sec:#1}{\coqdoccst{#2}}}
-
-%\newcommand{\coqlibrary}[2]{\chapter{Library \coqdoccst{#2}}\label{coq:#1}}
-
-%\newcommand{\coqlibraryref}[2]{\ref{coq:#1}}
-
-\newcommand{\coqlibraryref}[2]{\coqref{#1}{\coqdoccst{#2}}}
-
-\newcommand{\coqaxiom}[2]{\coqdef{#1}{#2}{\coqdocax{#2}}}
-\newcommand{\coqaxiomref}[2]{\coqref{#1}{\coqdocax{#2}}}
-
-\newcommand{\coqmodule}[2]{\coqdef{mod:#1}{#2}{\coqdocmod{#2}}}
-\newcommand{\coqmoduleref}[2]{\coqref{mod:#1}{\coqdocmod{#2}}}
-
\endinput
diff --git a/tools/coqdoc/pretty.mli b/tools/coqdoc/cpretty.mli
index dda0439e..213c76aa 100644
--- a/tools/coqdoc/pretty.mli
+++ b/tools/coqdoc/cpretty.mli
@@ -6,8 +6,9 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: pretty.mli 8617 2006-03-08 10:47:12Z notin $ i*)
+(*i $Id$ i*)
open Index
val coq_file : string -> Cdglobals.coq_module -> unit
+val detect_subtitle : string -> Cdglobals.coq_module -> string option
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
new file mode 100644
index 00000000..be8bc85d
--- /dev/null
+++ b/tools/coqdoc/cpretty.mll
@@ -0,0 +1,1176 @@
+(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+(*s Utility functions for the scanners *)
+
+{
+ open Printf
+ open Lexing
+
+ (* A function that emulates Lexing.new_line (which does not exist in OCaml < 3.11.0) *)
+ let new_line lexbuf =
+ let pos = lexbuf.lex_curr_p in
+ lexbuf.lex_curr_p <- { pos with
+ pos_lnum = pos.pos_lnum + 1;
+ pos_bol = pos.pos_cnum }
+
+ (* A list function we need *)
+ let rec take n ls =
+ if n = 0 then [] else
+ match ls with
+ | [] -> []
+ | (l :: ls) -> l :: (take (n-1) ls)
+
+ (* count the number of spaces at the beginning of a string *)
+ let count_spaces s =
+ let n = String.length s in
+ let rec count c i =
+ if i == n then c,i else match s.[i] with
+ | '\t' -> count (c + (8 - (c mod 8))) (i + 1)
+ | ' ' -> count (c + 1) (i + 1)
+ | _ -> c,i
+ in
+ count 0 0
+
+ let remove_newline s =
+ let n = String.length s in
+ let rec count i = if i == n || s.[i] <> '\n' then i else count (i + 1) in
+ let i = count 0 in
+ i, String.sub s i (n - i)
+
+ let count_dashes s =
+ let c = ref 0 in
+ for i = 0 to String.length s - 1 do if s.[i] = '-' then incr c done;
+ !c
+
+ let cut_head_tail_spaces s =
+ let n = String.length s in
+ let rec look_up i = if i == n || s.[i] <> ' ' then i else look_up (i+1) in
+ let rec look_dn i = if i == -1 || s.[i] <> ' ' then i else look_dn (i-1) in
+ let l = look_up 0 in
+ let r = look_dn (n-1) in
+ if l <= r then String.sub s l (r-l+1) else s
+
+ let sec_title s =
+ let rec count lev i =
+ if s.[i] = '*' then
+ count (succ lev) (succ i)
+ else
+ let t = String.sub s i (String.length s - i) in
+ lev, cut_head_tail_spaces t
+ in
+ count 0 (String.index s '*')
+
+ let strip_eol s =
+ let eol = s.[String.length s - 1] = '\n' in
+ (eol, if eol then String.sub s 1 (String.length s - 1) else s)
+
+
+ let formatted = ref false
+ let brackets = ref 0
+ let comment_level = ref 0
+ 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 backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos;
+ lexbuf.lex_curr_p <- lexbuf.lex_start_p
+
+ let backtrack_past_newline lexbuf =
+ let buf = lexeme lexbuf in
+ let splits = Str.bounded_split_delim (Str.regexp "['\n']") buf 2 in
+ match splits with
+ | [] -> ()
+ | (_ :: []) -> ()
+ | (s1 :: rest :: _) ->
+ let length_skip = 1 + String.length s1 in
+ lexbuf.lex_curr_pos <- lexbuf.lex_start_pos + length_skip
+
+ let is_space = function ' ' | '\t' | '\n' | '\r' -> true | _ -> false
+
+ (* saving/restoring the PP state *)
+
+ type state = {
+ st_gallina : bool;
+ st_light : bool
+ }
+
+ let state_stack = Stack.create ()
+
+ let save_state () =
+ Stack.push { st_gallina = !Cdglobals.gallina; st_light = !Cdglobals.light } state_stack
+
+ let restore_state () =
+ let s = Stack.pop state_stack in
+ Cdglobals.gallina := s.st_gallina;
+ Cdglobals.light := s.st_light
+
+ let without_ref r f x = save_state (); r := false; f x; restore_state ()
+
+ let without_gallina = without_ref Cdglobals.gallina
+
+ let without_light = without_ref Cdglobals.light
+
+ let show_all f = without_gallina (without_light f)
+
+ let begin_show () = save_state (); Cdglobals.gallina := false; Cdglobals.light := false
+ let end_show () = restore_state ()
+
+ (* Reset the globals *)
+
+ let reset () =
+ formatted := false;
+ brackets := 0;
+ comment_level := 0
+
+ (* erasing of Section/End *)
+
+ let section_re = Str.regexp "[ \t]*Section"
+ let end_re = Str.regexp "[ \t]*End"
+ let is_section s = Str.string_match section_re s 0
+ let is_end s = Str.string_match end_re s 0
+
+ let sections_to_close = ref 0
+
+ let section_or_end s =
+ if is_section s then begin
+ incr sections_to_close; true
+ end else if is_end s then begin
+ if !sections_to_close > 0 then begin
+ decr sections_to_close; true
+ end else
+ false
+ end else
+ true
+
+ (* for item lists *)
+ type list_compare =
+ | Before
+ | StartLevel of int
+ | InLevel of int * bool
+
+ (* Before : we're before any levels
+ StartLevel : at the same column as the dash in a level
+ InLevel : after the dash of this level, but before any deeper dashes.
+ bool is true if this is the last level *)
+ let find_level levels cur_indent =
+ match levels with
+ | [] -> Before
+ | (l::ls) ->
+ if cur_indent < l then Before
+ else
+ (* cur_indent will never be less than the head of the list *)
+ let rec findind ls n =
+ match ls with
+ | [] -> InLevel (n,true)
+ | (l :: []) -> if cur_indent = l then StartLevel n
+ else InLevel (n,true)
+ | (l1 :: l2 :: ls) ->
+ if cur_indent = l1 then StartLevel n
+ else if cur_indent < l2 then InLevel (n,false)
+ else findind (l2 :: ls) (n+1)
+ in
+ findind (l::ls) 1
+
+ type is_start_list =
+ | Rule
+ | List of int
+ | Neither
+
+ let check_start_list str =
+ let n_dashes = count_dashes str in
+ let (n_spaces,_) = count_spaces str in
+ if n_dashes >= 4 && not !Cdglobals.plain_comments then
+ Rule
+ else
+ if n_dashes = 1 && not !Cdglobals.plain_comments then
+ List n_spaces
+ else
+ Neither
+
+ (* examine a string for subtitleness *)
+ let subtitle m s =
+ match Str.split_delim (Str.regexp ":") s with
+ | [] -> false
+ | (name::_) ->
+ if (cut_head_tail_spaces name) = m then
+ true
+ else
+ false
+
+
+ (* tokens pretty-print *)
+
+ let token_buffer = Buffer.create 1024
+
+ let token_re =
+ Str.regexp "[ \t]*(\\*\\*[ \t]+printing[ \t]+\\([^ \t]+\\)"
+ let printing_token_re =
+ Str.regexp
+ "[ \t]*\\(\\(%\\([^%]*\\)%\\)\\|\\(\\$[^$]*\\$\\)\\)?[ \t]*\\(#\\(\\(&#\\|[^#]\\)*\\)#\\)?"
+
+ let add_printing_token toks pps =
+ try
+ if Str.string_match token_re toks 0 then
+ let tok = Str.matched_group 1 toks in
+ if Str.string_match printing_token_re pps 0 then
+ let pp =
+ (try Some (Str.matched_group 3 pps) with _ ->
+ try Some (Str.matched_group 4 pps) with _ -> None),
+ (try Some (Str.matched_group 6 pps) with _ -> None)
+ in
+ Output.add_printing_token tok pp
+ with _ ->
+ ()
+
+ let remove_token_re =
+ Str.regexp
+ "[ \t]*(\\*\\*[ \t]+remove[ \t]+printing[ \t]+\\([^ \t]+\\)[ \t]*\\*)"
+
+ let remove_printing_token toks =
+ try
+ if Str.string_match remove_token_re toks 0 then
+ let tok = Str.matched_group 1 toks in
+ Output.remove_printing_token tok
+ with _ ->
+ ()
+
+ let extract_ident_re = Str.regexp "([ \t]*\\([^ \t]+\\)[ \t]*:="
+ let extract_ident s =
+ assert (String.length s >= 3);
+ if Str.string_match extract_ident_re s 0 then
+ Str.matched_group 1 s
+ else
+ String.sub s 1 (String.length s - 3)
+
+ let output_indented_keyword s lexbuf =
+ 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)
+
+}
+
+(*s Regular expressions *)
+
+let space = [' ' '\t']
+let space_nl = [' ' '\t' '\n' '\r']
+let nl = "\r\n" | '\n'
+
+let firstchar =
+ ['A'-'Z' 'a'-'z' '_'] |
+ (* superscript 1 *)
+ '\194' '\185' |
+ (* utf-8 latin 1 supplement *)
+ '\195' ['\128'-'\191'] |
+ (* utf-8 letterlike symbols *)
+ (* '\206' ([ '\145' - '\183'] | '\187') | *)
+ (* '\xCF' [ '\x00' - '\xCE' ] | *)
+ (* utf-8 letterlike symbols *)
+ '\206' ('\160' | [ '\177'-'\183'] | '\187') |
+ '\226' ('\130' [ '\128'-'\137' ] (* subscripts *)
+ | '\129' [ '\176'-'\187' ] (* superscripts *)
+ | '\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])
+let identchar =
+ firstchar | ['\'' '0'-'9' '@' ]
+let id = firstchar identchar*
+let pfx_id = (id '.')*
+let identifier =
+ id | pfx_id id
+
+(* This misses unicode stuff, and it adds "[" and "]". It's only an
+ approximation of idents - used for detecting whether an underscore
+ is part of an identifier or meant to indicate emphasis *)
+let nonidentchar = [^ 'A'-'Z' 'a'-'z' '_' '[' ']' '\'' '0'-'9' '@' ]
+
+let printing_token = [^ ' ' '\t']*
+
+let thm_token =
+ "Theorem"
+ | "Lemma"
+ | "Fact"
+ | "Remark"
+ | "Corollary"
+ | "Proposition"
+ | "Property"
+ | "Goal"
+
+let prf_token =
+ "Next" space+ "Obligation"
+ | "Proof" (space* "." | space+ "with")
+
+let def_token =
+ "Definition"
+ | "Let"
+ | "Class"
+ | "SubClass"
+ | "Example"
+ | "Local"
+ | "Fixpoint"
+ | "Boxed"
+ | "CoFixpoint"
+ | "Record"
+ | "Structure"
+ | "Scheme"
+ | "Inductive"
+ | "CoInductive"
+ | "Equations"
+ | "Instance"
+ | "Global" space+ "Instance"
+
+let decl_token =
+ "Hypothesis"
+ | "Hypotheses"
+ | "Parameter"
+ | "Axiom" 's'?
+ | "Conjecture"
+
+let gallina_ext =
+ "Module"
+ | "Include" space+ "Type"
+ | "Include"
+ | "Declare" space+ "Module"
+ | "Transparent"
+ | "Opaque"
+ | "Canonical"
+ | "Coercion"
+ | "Identity"
+ | "Implicit"
+ | "Tactic" space+ "Notation"
+ | "Section"
+ | "Context"
+ | "Variable" 's'?
+ | ("Hypothesis" | "Hypotheses")
+ | "End"
+
+let notation_kw =
+ "Notation"
+ | "Infix"
+ | "Reserved" space+ "Notation"
+
+let commands =
+ "Pwd"
+ | "Cd"
+ | "Drop"
+ | "ProtectedLoop"
+ | "Quit"
+ | "Load"
+ | "Add"
+ | "Remove" space+ "Loadpath"
+ | "Print"
+ | "Inspect"
+ | "About"
+ | "Search"
+ | "Eval"
+ | "Reset"
+ | "Check"
+ | "Type"
+
+ | "Section"
+ | "Chapter"
+ | "Variable" 's'?
+ | ("Hypothesis" | "Hypotheses")
+ | "End"
+
+let end_kw = "Qed" | "Defined" | "Save" | "Admitted" | "Abort"
+
+let extraction =
+ "Extraction"
+ | "Recursive" space+ "Extraction"
+ | "Extract"
+
+let gallina_kw = thm_token | def_token | decl_token | gallina_ext | commands | extraction
+
+let prog_kw =
+ "Program" space+ gallina_kw
+ | "Obligation"
+ | "Obligations"
+ | "Solve"
+
+let gallina_kw_to_hide =
+ "Implicit" space+ "Arguments"
+ | "Ltac"
+ | "Require"
+ | "Import"
+ | "Export"
+ | "Load"
+ | "Hint"
+ | "Open"
+ | "Close"
+ | "Delimit"
+ | "Transparent"
+ | "Opaque"
+ | ("Declare" space+ ("Morphism" | "Step") )
+ | ("Set" | "Unset") space+ "Printing" space+ "Coercions"
+ | "Declare" space+ ("Left" | "Right") space+ "Step"
+
+
+let section = "*" | "**" | "***" | "****"
+
+let item_space = " "
+
+let begin_hide = "(*" space* "begin" space+ "hide" space* "*)" space* nl
+let end_hide = "(*" space* "end" space+ "hide" space* "*)" space* nl
+let begin_show = "(*" space* "begin" space+ "show" space* "*)" space* nl
+let end_show = "(*" space* "end" space+ "show" space* "*)" space* nl
+(*
+let begin_verb = "(*" space* "begin" space+ "verb" space* "*)"
+let end_verb = "(*" space* "end" space+ "verb" space* "*)"
+*)
+
+(*s Scanning Coq, at beginning of line *)
+
+rule coq_bol = parse
+ | space* nl+
+ { if not (!in_proof <> None && (!Cdglobals.gallina || !Cdglobals.light))
+ then Output.empty_line_of_code ();
+ coq_bol lexbuf }
+ | space* "(**" space_nl
+ { Output.end_coq (); Output.start_doc ();
+ let eol = doc_bol lexbuf in
+ Output.end_doc (); Output.start_coq ();
+ if eol then coq_bol lexbuf else coq lexbuf }
+ | space* "Comments" space_nl
+ { Output.end_coq (); Output.start_doc (); comments lexbuf; Output.end_doc ();
+ Output.start_coq (); coq lexbuf }
+ | space* begin_hide
+ { skip_hide lexbuf; coq_bol lexbuf }
+ | space* begin_show
+ { begin_show (); coq_bol lexbuf }
+ | space* end_show
+ { end_show (); coq_bol lexbuf }
+ | space* gallina_kw_to_hide
+ { let s = lexeme lexbuf in
+ if !Cdglobals.light && section_or_end s then
+ let eol = skip_to_dot lexbuf in
+ if eol then (coq_bol lexbuf) else coq lexbuf
+ else
+ begin
+ output_indented_keyword s lexbuf;
+ let eol = body lexbuf in
+ if eol then coq_bol lexbuf else coq lexbuf
+ end }
+ | space* thm_token
+ { let s = lexeme lexbuf in
+ output_indented_keyword s lexbuf;
+ let eol = body lexbuf in
+ in_proof := Some eol;
+ if eol then coq_bol lexbuf else coq lexbuf }
+ | space* prf_token
+ { in_proof := Some true;
+ let eol =
+ if not !Cdglobals.gallina then
+ begin backtrack lexbuf; body_bol lexbuf end
+ else
+ let s = lexeme lexbuf in
+ if s.[String.length s - 1] = '.' then false
+ else skip_to_dot lexbuf
+ in if eol then coq_bol lexbuf else coq lexbuf }
+ | space* end_kw {
+ let eol =
+ if not (!in_proof <> None && !Cdglobals.gallina) then
+ begin backtrack lexbuf; body_bol lexbuf end
+ else skip_to_dot lexbuf
+ in
+ in_proof := None;
+ if eol then coq_bol lexbuf else coq lexbuf }
+ | space* gallina_kw
+ {
+ in_proof := None;
+ let s = lexeme lexbuf in
+ output_indented_keyword s lexbuf;
+ let eol= body lexbuf in
+ if eol then coq_bol lexbuf else coq lexbuf }
+ | space* prog_kw
+ {
+ in_proof := None;
+ let s = lexeme lexbuf in
+ output_indented_keyword s lexbuf;
+ let eol= body lexbuf in
+ if eol then coq_bol lexbuf else coq lexbuf }
+ | space* notation_kw space*
+ { let s = lexeme lexbuf in
+ output_indented_keyword s lexbuf;
+ let eol= start_notation_string lexbuf in
+ if eol then coq_bol lexbuf else coq lexbuf }
+
+ | space* "(**" space+ "printing" space+ printing_token space+
+ { let tok = lexeme lexbuf in
+ let s = printing_token_body lexbuf in
+ add_printing_token tok s;
+ coq_bol lexbuf }
+ | space* "(**" space+ "printing" space+
+ { eprintf "warning: bad 'printing' command at character %d\n"
+ (lexeme_start lexbuf); flush stderr;
+ comment_level := 1;
+ ignore (comment lexbuf);
+ coq_bol lexbuf }
+ | space* "(**" space+ "remove" space+ "printing" space+
+ printing_token space* "*)"
+ { remove_printing_token (lexeme lexbuf);
+ coq_bol lexbuf }
+ | space* "(**" space+ "remove" space+ "printing" space+
+ { eprintf "warning: bad 'remove printing' command at character %d\n"
+ (lexeme_start lexbuf); flush stderr;
+ comment_level := 1;
+ ignore (comment lexbuf);
+ coq_bol lexbuf }
+ | space* "(*"
+ { comment_level := 1;
+ if !Cdglobals.parse_comments then begin
+ let s = lexeme lexbuf in
+ let nbsp,isp = count_spaces s in
+ Output.indentation nbsp;
+ Output.start_comment ();
+ end;
+ let eol = comment lexbuf in
+ if eol then coq_bol lexbuf else coq lexbuf }
+ | eof
+ { () }
+ | _
+ { let eol =
+ if not !Cdglobals.gallina then
+ begin backtrack lexbuf; body_bol lexbuf end
+ else
+ skip_to_dot lexbuf
+ in
+ if eol then coq_bol lexbuf else coq lexbuf }
+
+(*s Scanning Coq elsewhere *)
+
+and coq = parse
+ | nl
+ { if not (!in_proof <> None && !Cdglobals.gallina) then Output.line_break(); coq_bol lexbuf }
+ | "(**" space_nl
+ { Output.end_coq (); Output.start_doc ();
+ let eol = doc_bol lexbuf in
+ Output.end_doc (); Output.start_coq ();
+ if eol then coq_bol lexbuf else coq lexbuf }
+ | "(*"
+ { comment_level := 1;
+ if !Cdglobals.parse_comments then begin
+ let s = lexeme lexbuf in
+ let nbsp,isp = count_spaces s in
+ Output.indentation nbsp;
+ Output.start_comment ();
+ end;
+ let eol = comment lexbuf in
+ if eol then coq_bol lexbuf
+ else coq lexbuf
+ }
+ | nl+ space* "]]"
+ { if not !formatted then
+ begin
+ (* Isn't this an anomaly *)
+ let s = lexeme lexbuf in
+ let nlsp,s = remove_newline s in
+ let nbsp,isp = count_spaces s in
+ Output.indentation nbsp;
+ let loc = lexeme_start lexbuf + isp + nlsp in
+ Output.sublexer ']' loc;
+ Output.sublexer ']' (loc+1);
+ coq lexbuf
+ end }
+ | eof
+ { () }
+ | gallina_kw_to_hide
+ { let s = lexeme lexbuf in
+ if !Cdglobals.light && section_or_end s then
+ begin
+ let eol = skip_to_dot lexbuf in
+ if eol then coq_bol lexbuf else coq lexbuf
+ end
+ else
+ begin
+ Output.ident s (lexeme_start lexbuf);
+ let eol=body lexbuf in
+ if eol then coq_bol lexbuf else coq lexbuf
+ end }
+ | prf_token
+ { let eol =
+ if not !Cdglobals.gallina then
+ begin backtrack lexbuf; body_bol lexbuf end
+ else
+ let s = lexeme lexbuf in
+ let eol =
+ if s.[String.length s - 1] = '.' then false
+ else skip_to_dot lexbuf
+ in
+ eol
+ in if eol then coq_bol lexbuf else coq lexbuf }
+ | end_kw {
+ let eol =
+ if not !Cdglobals.gallina then
+ begin backtrack lexbuf; body lexbuf end
+ else
+ let eol = skip_to_dot lexbuf in
+ if !in_proof <> Some true && eol then
+ Output.line_break ();
+ eol
+ in
+ in_proof := None;
+ if eol then coq_bol lexbuf else coq lexbuf }
+ | gallina_kw
+ { let s = lexeme lexbuf in
+ Output.ident s (lexeme_start lexbuf);
+ let eol = body lexbuf in
+ if eol then coq_bol lexbuf else coq lexbuf }
+ | notation_kw space*
+ { let s = lexeme lexbuf in
+ Output.ident s (lexeme_start lexbuf);
+ let eol= start_notation_string lexbuf in
+ if eol then coq_bol lexbuf else coq lexbuf }
+ | prog_kw
+ { let s = lexeme lexbuf in
+ Output.ident s (lexeme_start lexbuf);
+ let eol = body lexbuf in
+ if eol then coq_bol lexbuf else coq lexbuf }
+ | space+ { Output.char ' '; coq lexbuf }
+ | eof
+ { () }
+ | _ { let eol =
+ if not !Cdglobals.gallina then
+ begin backtrack lexbuf; body lexbuf end
+ else
+ skip_to_dot lexbuf
+ in
+ if eol then coq_bol lexbuf else coq lexbuf}
+
+(*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
+ if (!Cdglobals.lib_subtitles) &&
+ (subtitle (Output.get_module false) s) then
+ ()
+ 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
+ in
+ match check_start_list buf 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
+ | Rule -> Output.rule (); doc None lexbuf
+ }
+ | "<<" space*
+ { Output.start_verbatim (); verbatim lexbuf; doc_bol lexbuf }
+ | eof
+ { true }
+ | '_'
+ { if !Cdglobals.plain_comments then Output.char '_' else start_emph ();
+ doc None lexbuf }
+ | _
+ { backtrack lexbuf; doc None lexbuf }
+
+(*s Scanning lists - using whitespace *)
+and doc_list_bol indents = parse
+ | space* '-'
+ { let (n_spaces,_) = count_spaces (lexeme lexbuf) in
+ match find_level indents n_spaces with
+ | Before -> backtrack lexbuf; doc_bol lexbuf
+ | StartLevel n -> Output.item n; doc (Some (take n indents)) lexbuf
+ | InLevel (n,true) ->
+ let items = List.length indents in
+ Output.item (items+1);
+ doc (Some (List.append indents [n_spaces])) lexbuf
+ | InLevel (_,false) ->
+ backtrack lexbuf; doc_bol lexbuf
+ }
+ | "<<" space*
+ { Output.start_verbatim ();
+ verbatim lexbuf;
+ doc_list_bol indents lexbuf }
+ | "[[" nl
+ { formatted := true;
+ Output.start_inline_coq_block ();
+ ignore(body_bol lexbuf);
+ Output.end_inline_coq_block ();
+ formatted := false;
+ doc_list_bol indents lexbuf }
+ | space* nl space* '-'
+ { (* Like in the doc_bol production, these two productions
+ exist only to deal properly with whitespace *)
+ Output.paragraph ();
+ backtrack_past_newline lexbuf;
+ doc_list_bol indents lexbuf }
+ | space* nl space* _
+ { 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_split2 - please report\n";
+ exit 1
+ in
+ let (n_spaces,_) = count_spaces buf in
+ match find_level indents n_spaces with
+ | InLevel _ ->
+ Output.paragraph ();
+ backtrack_past_newline lexbuf;
+ doc_list_bol indents lexbuf
+ | StartLevel n ->
+ if n = 1 then
+ begin
+ Output.stop_item ();
+ backtrack_past_newline lexbuf;
+ doc_bol lexbuf
+ end
+ else
+ begin
+ Output.paragraph ();
+ backtrack_past_newline lexbuf;
+ doc_list_bol indents lexbuf
+ end
+ | Before -> Output.stop_item ();
+ backtrack_past_newline lexbuf;
+ doc_bol lexbuf
+
+ }
+ | space* _
+ { let (n_spaces,_) = count_spaces (lexeme lexbuf) in
+ match find_level indents n_spaces with
+ | Before -> Output.stop_item (); backtrack lexbuf;
+ doc_bol lexbuf
+ | StartLevel n ->
+ Output.reach_item_level (n-1);
+ backtrack lexbuf;
+ doc (Some (take (n-1) indents)) lexbuf
+ | InLevel (n,_) ->
+ Output.reach_item_level n;
+ backtrack lexbuf;
+ doc (Some (take n indents)) lexbuf
+ }
+
+(*s Scanning documentation elsewhere *)
+and doc indents = parse
+ | nl
+ { Output.char '\n';
+ match indents with
+ | Some ls -> doc_list_bol ls lexbuf
+ | None -> doc_bol lexbuf }
+ | "[[" nl
+ { if !Cdglobals.plain_comments
+ then (Output.char '['; Output.char '['; doc indents lexbuf)
+ else (formatted := true;
+ Output.start_inline_coq_block ();
+ let eol = body_bol lexbuf in
+ Output.end_inline_coq_block (); formatted := false;
+ if eol then
+ match indents with
+ | Some ls -> doc_list_bol ls lexbuf
+ | None -> doc_bol lexbuf
+ else doc indents lexbuf)}
+ | "[]"
+ { Output.proofbox (); doc indents lexbuf }
+ | "["
+ { if !Cdglobals.plain_comments then Output.char '['
+ else (brackets := 1; Output.start_inline_coq (); escaped_coq lexbuf;
+ Output.end_inline_coq ()); doc indents lexbuf }
+ | "(*"
+ { backtrack lexbuf ;
+ let bol_parse = match indents with
+ | Some is -> doc_list_bol is
+ | None -> doc_bol
+ in
+ let eol = comment lexbuf in
+ if eol then bol_parse lexbuf else doc indents lexbuf
+ }
+ | '*'* "*)" space* nl
+ { true }
+ | '*'* "*)"
+ { false }
+ | "$"
+ { if !Cdglobals.plain_comments then Output.char '$'
+ else (Output.start_latex_math (); escaped_math_latex lexbuf);
+ doc indents lexbuf }
+ | "$$"
+ { if !Cdglobals.plain_comments then Output.char '$';
+ Output.char '$'; doc indents lexbuf }
+ | "%"
+ { if !Cdglobals.plain_comments then Output.char '%'
+ else escaped_latex lexbuf; doc indents lexbuf }
+ | "%%"
+ { if !Cdglobals.plain_comments then Output.char '%';
+ Output.char '%'; doc indents lexbuf }
+ | "#"
+ { if !Cdglobals.plain_comments then Output.char '#'
+ else escaped_html lexbuf; doc indents lexbuf }
+ | "##"
+ { if !Cdglobals.plain_comments then Output.char '#';
+ Output.char '#'; doc indents lexbuf }
+ | nonidentchar '_' nonidentchar
+ { List.iter (fun x -> Output.char (lexeme_char lexbuf x)) [0;1;2];
+ doc indents lexbuf}
+ | nonidentchar '_'
+ { Output.char (lexeme_char lexbuf 0);
+ if !Cdglobals.plain_comments then Output.char '_' else start_emph () ;
+ doc indents lexbuf }
+ | '_' nonidentchar
+ { if !Cdglobals.plain_comments then Output.char '_' else stop_emph () ;
+ Output.char (lexeme_char lexbuf 1);
+ doc indents lexbuf }
+ | eof
+ { false }
+ | _
+ { Output.char (lexeme_char lexbuf 0); doc indents lexbuf }
+
+(*s Various escapings *)
+
+and escaped_math_latex = parse
+ | "$" { Output.stop_latex_math () }
+ | eof { Output.stop_latex_math () }
+ | _ { Output.latex_char (lexeme_char lexbuf 0); escaped_math_latex lexbuf }
+
+and escaped_latex = parse
+ | "%" { () }
+ | eof { () }
+ | _ { Output.latex_char (lexeme_char lexbuf 0); escaped_latex lexbuf }
+
+and escaped_html = parse
+ | "#" { () }
+ | "&#"
+ { Output.html_char '&'; Output.html_char '#'; escaped_html lexbuf }
+ | "##"
+ { Output.html_char '#'; escaped_html lexbuf }
+ | 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 }
+
+(*s Coq, inside quotations *)
+
+and escaped_coq = parse
+ | "]"
+ { decr brackets;
+ if !brackets > 0 then
+ (Output.sublexer ']' (lexeme_start lexbuf); escaped_coq lexbuf)
+ else Tokens.flush_sublexer () }
+ | "["
+ { incr brackets;
+ Output.sublexer '[' (lexeme_start lexbuf); escaped_coq lexbuf }
+ | "(*"
+ { Tokens.flush_sublexer (); comment_level := 1;
+ ignore (comment lexbuf); escaped_coq lexbuf }
+ | "*)"
+ { (* likely to be a syntax error: we escape *) backtrack lexbuf }
+ | eof
+ { Tokens.flush_sublexer () }
+ | (identifier '.')* identifier
+ { Output.ident (lexeme lexbuf) (lexeme_start lexbuf); escaped_coq lexbuf }
+ | space
+ { Tokens.flush_sublexer(); Output.char (lexeme_char lexbuf 0);
+ escaped_coq lexbuf }
+ | _
+ { Output.sublexer (lexeme_char lexbuf 0) (lexeme_start lexbuf);
+ escaped_coq lexbuf }
+
+(*s Coq "Comments" command. *)
+
+and comments = parse
+ | space_nl+
+ { Output.char ' '; comments lexbuf }
+ | '"' [^ '"']* '"'
+ { let s = lexeme lexbuf in
+ let s = String.sub s 1 (String.length s - 2) in
+ ignore (doc None (from_string s)); comments lexbuf }
+ | ([^ '.' '"'] | '.' [^ ' ' '\t' '\n'])+
+ { escaped_coq (from_string (lexeme lexbuf)); comments lexbuf }
+ | "." (space_nl | eof)
+ { () }
+ | eof
+ { () }
+ | _
+ { Output.char (lexeme_char lexbuf 0); comments lexbuf }
+
+(*s Skip comments *)
+
+and comment = parse
+ | "(*" { incr comment_level;
+ if !Cdglobals.parse_comments then Output.start_comment ();
+ comment lexbuf }
+ | "*)" space* nl {
+ if !Cdglobals.parse_comments then
+ (Output.end_comment (); Output.line_break ());
+ decr comment_level; if !comment_level > 0 then comment lexbuf else true }
+ | "*)" {
+ if !Cdglobals.parse_comments then (Output.end_comment ());
+ decr comment_level; if !comment_level > 0 then comment lexbuf else false }
+ | "[" {
+ if !Cdglobals.parse_comments then
+ if !Cdglobals.plain_comments then Output.char '['
+ else (brackets := 1; Output.start_inline_coq ();
+ escaped_coq lexbuf; Output.end_inline_coq ());
+ comment lexbuf }
+ | "[[" nl {
+ if !Cdglobals.parse_comments then
+ if !Cdglobals.plain_comments then (Output.char '['; Output.char '[')
+ else (formatted := true;
+ Output.start_inline_coq_block ();
+ let _ = body_bol lexbuf in
+ Output.end_inline_coq_block (); formatted := false);
+ comment lexbuf}
+ | "$"
+ { if !Cdglobals.parse_comments then
+ if !Cdglobals.plain_comments then Output.char '$'
+ else (Output.start_latex_math (); escaped_math_latex lexbuf);
+ comment lexbuf }
+ | "$$"
+ { if !Cdglobals.parse_comments
+ then
+ (if !Cdglobals.plain_comments then Output.char '$'; Output.char '$');
+ doc None lexbuf }
+ | "%"
+ { if !Cdglobals.parse_comments
+ then
+ if !Cdglobals.plain_comments then Output.char '%'
+ else escaped_latex lexbuf; comment lexbuf }
+ | "%%"
+ { if !Cdglobals.parse_comments
+ then
+ (if !Cdglobals.plain_comments then Output.char '%'; Output.char '%');
+ comment lexbuf }
+ | "#"
+ { if !Cdglobals.parse_comments
+ then
+ if !Cdglobals.plain_comments then Output.char '$'
+ else escaped_html lexbuf; comment lexbuf }
+ | "##"
+ { if !Cdglobals.parse_comments
+ then
+ (if !Cdglobals.plain_comments then Output.char '#'; Output.char '#');
+ comment lexbuf }
+ | eof { false }
+ | space+ { if !Cdglobals.parse_comments
+ then Output.indentation (fst (count_spaces (lexeme lexbuf)));
+ comment lexbuf }
+ | nl { if !Cdglobals.parse_comments
+ then Output.line_break (); comment lexbuf }
+ | _ { if !Cdglobals.parse_comments then Output.char (lexeme_char lexbuf 0);
+ comment lexbuf }
+
+and skip_to_dot = parse
+ | '.' space* nl { true }
+ | eof | '.' space+ { false }
+ | "(*" { comment_level := 1; ignore (comment lexbuf); skip_to_dot lexbuf }
+ | _ { skip_to_dot lexbuf }
+
+and body_bol = parse
+ | space+
+ { Output.indentation (fst (count_spaces (lexeme lexbuf))); body lexbuf }
+ | _ { backtrack lexbuf; Output.indentation 0; body lexbuf }
+
+and body = parse
+ | nl {Tokens.flush_sublexer(); Output.line_break(); new_line lexbuf; body_bol lexbuf}
+ | nl+ space* "]]" space* nl
+ { Tokens.flush_sublexer();
+ if not !formatted then
+ begin
+ let s = lexeme lexbuf in
+ let nlsp,s = remove_newline s in
+ let _,isp = count_spaces s in
+ let loc = lexeme_start lexbuf + nlsp + isp in
+ Output.sublexer ']' loc;
+ Output.sublexer ']' (loc+1);
+ Tokens.flush_sublexer();
+ body lexbuf
+ end
+ else
+ begin
+ Output.paragraph ();
+ true
+ end }
+ | "]]" space* nl
+ { Tokens.flush_sublexer();
+ if not !formatted then
+ begin
+ let loc = lexeme_start lexbuf in
+ Output.sublexer ']' loc;
+ Output.sublexer ']' (loc+1);
+ Tokens.flush_sublexer();
+ Output.line_break();
+ body lexbuf
+ end
+ else
+ begin
+ Output.paragraph ();
+ true
+ end }
+ | eof { Tokens.flush_sublexer(); false }
+ | '.' space* nl | '.' space* eof
+ { Tokens.flush_sublexer(); Output.char '.'; Output.line_break();
+ if not !formatted then true else body_bol lexbuf }
+ | '.' space* nl "]]" space* nl
+ { Tokens.flush_sublexer(); Output.char '.';
+ if not !formatted then
+ begin
+ eprintf "Error: stray ]] at %d\n" (lexeme_start lexbuf);
+ flush stderr;
+ exit 1
+ end
+ else
+ begin
+ Output.paragraph ();
+ true
+ end
+ }
+ | '.' space+
+ { Tokens.flush_sublexer(); Output.char '.'; Output.char ' ';
+ if not !formatted then false else body lexbuf }
+ | "(**" space_nl
+ { Tokens.flush_sublexer(); Output.end_coq (); Output.start_doc ();
+ let eol = doc_bol lexbuf in
+ Output.end_doc (); Output.start_coq ();
+ if eol then body_bol lexbuf else body lexbuf }
+ | "(*" { Tokens.flush_sublexer(); comment_level := 1;
+ if !Cdglobals.parse_comments then Output.start_comment ();
+ let eol = comment lexbuf in
+ if eol
+ then begin if not !Cdglobals.parse_comments then Output.line_break(); body_bol lexbuf end
+ else body lexbuf }
+ | "where" space*
+ { Tokens.flush_sublexer();
+ Output.ident (lexeme lexbuf) (lexeme_start lexbuf);
+ start_notation_string lexbuf }
+ | identifier
+ { Tokens.flush_sublexer();
+ Output.ident (lexeme lexbuf) (lexeme_start lexbuf);
+ body lexbuf }
+ | ".."
+ { Tokens.flush_sublexer(); Output.char '.'; Output.char '.';
+ body lexbuf }
+ | '"'
+ { Tokens.flush_sublexer(); Output.char '"';
+ string lexbuf;
+ body lexbuf }
+ | space
+ { Tokens.flush_sublexer(); Output.char (lexeme_char lexbuf 0);
+ body lexbuf }
+
+ | _ { let c = lexeme_char lexbuf 0 in
+ Output.sublexer c (lexeme_start lexbuf);
+ body lexbuf }
+
+and start_notation_string = parse
+ | '"' (* a true notation *)
+ { Output.sublexer '"' (lexeme_start lexbuf);
+ notation_string lexbuf;
+ body lexbuf }
+ | _ (* an abbreviation *)
+ { backtrack lexbuf; body lexbuf }
+
+and notation_string = parse
+ | "\"\""
+ { Output.char '"'; Output.char '"'; (* Unlikely! *)
+ notation_string lexbuf }
+ | '"'
+ { Tokens.flush_sublexer(); Output.char '"' }
+ | _ { let c = lexeme_char lexbuf 0 in
+ Output.sublexer c (lexeme_start lexbuf);
+ notation_string lexbuf }
+
+and string = parse
+ | "\"\"" { Output.char '"'; Output.char '"'; string lexbuf }
+ | '"' { Output.char '"' }
+ | _ { let c = lexeme_char lexbuf 0 in Output.char c; string lexbuf }
+
+and skip_hide = parse
+ | eof | end_hide { () }
+ | _ { skip_hide lexbuf }
+
+(*s Reading token pretty-print *)
+
+and printing_token_body = parse
+ | "*)" nl? | eof
+ { let s = Buffer.contents token_buffer in
+ Buffer.clear token_buffer;
+ s }
+ | _ { Buffer.add_string token_buffer (lexeme lexbuf);
+ printing_token_body lexbuf }
+
+(*s A small scanner to support the chapter subtitle feature *)
+and st_start m = parse
+ | "(*" "*"+ space+ "*" space+
+ { st_modname m lexbuf }
+ | _
+ { None }
+
+and st_modname m = parse
+ | identifier space* ":" space*
+ { if subtitle m (lexeme lexbuf) then
+ st_subtitle lexbuf
+ else
+ None
+ }
+ | _
+ { None }
+
+and st_subtitle = parse
+ | [^ '\n']* '\n'
+ { let st = lexeme lexbuf in
+ let i = try Str.search_forward (Str.regexp "\\**)") st 0 with
+ Not_found ->
+ (eprintf "unterminated comment at beginning of file\n";
+ exit 1)
+ in
+ Some (cut_head_tail_spaces (String.sub st 0 i))
+ }
+ | _
+ { None }
+(*s Applying the scanners to files *)
+
+{
+ let coq_file f m =
+ reset ();
+ let c = open_in f in
+ let lb = from_channel c in
+ (Index.current_library := m;
+ Output.initialize ();
+ Output.start_module ();
+ Output.start_coq (); coq_bol lb; Output.end_coq ();
+ close_in c)
+
+ let detect_subtitle f m =
+ let c = open_in f in
+ let lb = from_channel c in
+ let sub = st_start m lb in
+ close_in c;
+ sub
+}
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
new file mode 100644
index 00000000..889e5d6f
--- /dev/null
+++ b/tools/coqdoc/index.ml
@@ -0,0 +1,335 @@
+(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+open Filename
+open Lexing
+open Printf
+open Cdglobals
+
+type loc = int
+
+type entry_type =
+ | Library
+ | Module
+ | Definition
+ | Inductive
+ | Constructor
+ | Lemma
+ | Record
+ | Projection
+ | Instance
+ | Class
+ | Method
+ | Variable
+ | Axiom
+ | TacticDefinition
+ | Abbreviation
+ | Notation
+ | Section
+
+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. *)
+
+let deftable = Hashtbl.create 97
+
+(** [reftable] stores references and definitions *)
+let reftable = Hashtbl.create 97
+
+let full_ident sp id =
+ if sp <> "<>" then
+ if id <> "<>" then
+ sp ^ "." ^ id
+ else sp
+ else if id <> "<>"
+ then id
+ else ""
+
+let add_def loc ty sp id =
+ Hashtbl.add reftable (!current_library, loc) (Def (full_ident sp id, ty));
+ Hashtbl.add deftable id (Ref (!current_library, full_ident sp id, ty))
+
+let add_ref m loc m' sp id ty =
+ if Hashtbl.mem reftable (m, loc) then ()
+ else Hashtbl.add reftable (m, loc) (Ref (m', full_ident sp id, ty));
+ let idx = if id = "<>" then m' else id in
+ if Hashtbl.mem deftable idx then ()
+ else Hashtbl.add deftable idx (Ref (m', full_ident sp id, ty))
+
+let add_mod m loc m' id =
+ Hashtbl.add reftable (m, loc) (Mod (m', id));
+ Hashtbl.add deftable m (Mod (m', id))
+
+let find m l = Hashtbl.find reftable (m, l)
+
+let find_string m s = Hashtbl.find deftable s
+
+(*s Manipulating path prefixes *)
+
+type stack = string list
+
+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 *)
+
+let split_sp s =
+ try
+ let i = String.rindex s '.' in
+ String.sub s 0 i, String.sub s (i + 1) (String.length s - i - 1)
+ with
+ Not_found -> "", s
+
+let modules = Hashtbl.create 97
+let local_modules = Hashtbl.create 97
+
+let add_module m =
+ let _,id = split_sp m in
+ Hashtbl.add modules id m;
+ Hashtbl.add local_modules m ()
+
+type module_kind = Local | External of string | Unknown
+
+let external_libraries = ref []
+
+let add_external_library logicalpath url =
+ external_libraries := (logicalpath,url) :: !external_libraries
+
+let find_external_library logicalpath =
+ let rec aux = function
+ | [] -> raise Not_found
+ | (l,u)::rest ->
+ if String.length logicalpath > String.length l &
+ String.sub logicalpath 0 (String.length l + 1) = l ^"."
+ then u
+ else aux rest
+ in aux !external_libraries
+
+let init_coqlib_library () = add_external_library "Coq" !coqlib
+
+let find_module m =
+ if Hashtbl.mem local_modules m then
+ Local
+ else
+ try External (Filename.concat (find_external_library m) m)
+ with Not_found -> Unknown
+
+
+(* Building indexes *)
+
+type 'a index = {
+ idx_name : string;
+ idx_entries : (char * (string * 'a) list) list;
+ idx_size : int }
+
+let map f i =
+ { i with idx_entries =
+ List.map
+ (fun (c,l) -> (c, List.map (fun (s,x) -> (s,f s x)) l))
+ i.idx_entries }
+
+let compare_entries (s1,_) (s2,_) = Alpha.compare_string s1 s2
+
+let sort_entries el =
+ let t = Hashtbl.create 97 in
+ List.iter
+ (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 c,l =
+ try c,Hashtbl.find t c with Not_found -> '*',Hashtbl.find t '*' 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 display_letter c = if c = '*' then "other" else String.make 1 c
+
+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 ->
+ let ln = !lib_name in
+ if ln <> "" then String.lowercase ln else "library"
+ | Module -> "moduleid"
+ | Definition -> "definition"
+ | Inductive -> "inductive"
+ | Constructor -> "constructor"
+ | Lemma -> "lemma"
+ | Record -> "record"
+ | Projection -> "projection"
+ | Instance -> "instance"
+ | Class -> "class"
+ | Method -> "method"
+ | Variable -> "variable"
+ | Axiom -> "axiom"
+ | TacticDefinition -> "tactic"
+ | Abbreviation -> "abbreviation"
+ | Notation -> "notation"
+ | Section -> "section"
+
+let prepare_entry s = function
+ | Notation ->
+ (* Notations have conventially the form section.:sc: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
+ let sc = String.sub s (h+1) (i-h-1) in
+ let ntn = String.make (String.length s) ' ' in
+ let k = ref 0 in
+ let j = ref (i+1) in
+ let quoted = ref false in
+ while !j <> String.length s do
+ if s.[!j] = '_' && not !quoted then ntn.[!k] <- ' ' else
+ if s.[!j] = 'x' && not !quoted then ntn.[!k] <- '_' else
+ if s.[!j] = '\'' then
+ if s.[!j+1] = 'x' && s.[!j+1] = '\'' then (ntn.[!k] <- 'x'; j:=!j+2)
+ else (quoted := not !quoted; ntn.[!k] <- '\'')
+ else ntn.[!k] <- s.[!j];
+ incr j; incr k
+ done;
+ let ntn = String.sub ntn 0 !k in
+ if sc = "" then ntn else ntn ^ " (" ^ sc ^ ")"
+ | _ ->
+ s
+
+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)
+ 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;
+ 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 []
+
+let type_of_string = function
+ | "def" | "coe" | "subclass" | "canonstruc" | "fix" | "cofix"
+ | "ex" | "scheme" -> Definition
+ | "prf" | "thm" -> Lemma
+ | "ind" | "coind" -> Inductive
+ | "constr" -> Constructor
+ | "rec" | "corec" -> Record
+ | "proj" -> Projection
+ | "class" -> Class
+ | "meth" -> Method
+ | "inst" -> Instance
+ | "var" -> Variable
+ | "defax" | "prfax" | "ax" -> Axiom
+ | "syndef" -> Abbreviation
+ | "not" -> Notation
+ | "lib" -> Library
+ | "mod" | "modtype" -> Module
+ | "tac" -> TacticDefinition
+ | "sec" -> Section
+ | s -> raise (Invalid_argument ("type_of_string:" ^ s))
+
+let read_glob f =
+ let c = open_in f in
+ let cur_mod = ref "" in
+ try
+ while true do
+ let s = input_line c in
+ let n = String.length s in
+ if n > 0 then begin
+ match s.[0] with
+ | 'F' ->
+ cur_mod := String.sub s 1 (n - 1);
+ current_library := !cur_mod
+ | 'R' ->
+ (try
+ 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)
+ done)
+ with _ ->
+ try
+ Scanf.sscanf s "R%d %s %s %s %s"
+ (fun loc lib_dp sp id ty ->
+ add_ref !cur_mod loc lib_dp sp id (type_of_string ty))
+ with _ -> ())
+ | _ ->
+ try Scanf.sscanf s "%s %d %s %s"
+ (fun ty loc sp id -> add_def loc (type_of_string ty) sp id)
+ with Scanf.Scan_failure _ -> ()
+ end
+ done; assert false
+ with End_of_file ->
+ close_in c
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index 56a3cd11..517ec97a 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -6,13 +6,13 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: index.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
+(*i $Id$ i*)
open Cdglobals
type loc = int
-type entry_type =
+type entry_type =
| Library
| Module
| Definition
@@ -33,7 +33,7 @@ type entry_type =
val type_name : entry_type -> string
-type index_entry =
+type index_entry =
| Def of string * entry_type
| Ref of coq_module * string * entry_type
| Mod of coq_module * string
@@ -44,28 +44,32 @@ val find_string : coq_module -> string -> index_entry
val add_module : coq_module -> unit
-type module_kind = Local | Coqlib | Unknown
+type module_kind = Local | External of coq_module | Unknown
val find_module : coq_module -> module_kind
-(*s Scan identifiers introductions from a file *)
+val init_coqlib_library : unit -> unit
-val scan_file : string -> coq_module -> unit
+val add_external_library : string -> coq_module -> unit
(*s Read globalizations from a file (produced by coqc -dump-glob) *)
-val read_glob : string -> coq_module
+val read_glob : string -> unit
(*s Indexes *)
-type 'a index = {
+type 'a index = {
idx_name : string;
idx_entries : (char * (string * 'a) list) list;
idx_size : int }
val current_library : string ref
-val all_entries : unit ->
+val display_letter : char -> string
+
+val prepare_entry : string -> entry_type -> string
+
+val all_entries : unit ->
(coq_module * entry_type) index *
(entry_type * coq_module index) list
diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
deleted file mode 100644
index f8adb52b..00000000
--- a/tools/coqdoc/index.mll
+++ /dev/null
@@ -1,490 +0,0 @@
-(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(*i $Id: index.mll 11790 2009-01-15 20:19:58Z msozeau $ i*)
-
-{
-
-open Filename
-open Lexing
-open Printf
-
-open Cdglobals
-
-type loc = int
-
-type entry_type =
- | Library
- | Module
- | Definition
- | Inductive
- | Constructor
- | Lemma
- | Record
- | Projection
- | Instance
- | Class
- | Method
- | Variable
- | Axiom
- | TacticDefinition
- | Abbreviation
- | Notation
- | Section
-
-type index_entry =
- | Def of string * entry_type
- | Ref of coq_module * string * entry_type
- | Mod of coq_module * string
-
-let current_type = 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. *)
-
-let deftable = Hashtbl.create 97
-
-(** [reftable] stores references and definitions *)
-let reftable = Hashtbl.create 97
-
-let full_ident sp id =
- if sp <> "<>" then
- if id <> "<>" then
- sp ^ "." ^ id
- else sp
- else if id <> "<>"
- then id
- else ""
-
-let add_def loc ty sp id =
- Hashtbl.add reftable (!current_library, loc) (Def (full_ident sp id, ty));
- Hashtbl.add deftable id (Ref (!current_library, full_ident sp id, ty))
-
-let add_ref m loc m' sp id ty =
- if Hashtbl.mem reftable (m, loc) then ()
- else Hashtbl.add reftable (m, loc) (Ref (m', full_ident sp id, ty));
- let idx = if id = "<>" then m' else id in
- if Hashtbl.mem deftable idx then ()
- else Hashtbl.add deftable idx (Ref (m', full_ident sp id, ty))
-
-let add_mod m loc m' id =
- Hashtbl.add reftable (m, loc) (Mod (m', id));
- Hashtbl.add deftable m (Mod (m', id))
-
-let find m l = Hashtbl.find reftable (m, l)
-
-let find_string m s = Hashtbl.find deftable s
-
-(*s Manipulating path prefixes *)
-
-type stack = string list
-
-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 *)
-
-let split_sp s =
- try
- let i = String.rindex s '.' in
- String.sub s 0 i, String.sub s (i + 1) (String.length s - i - 1)
- with
- Not_found -> "", s
-
-let modules = Hashtbl.create 97
-let local_modules = Hashtbl.create 97
-
-let add_module m =
- let _,id = split_sp m in
- Hashtbl.add modules id m;
- Hashtbl.add local_modules m ()
-
-type module_kind = Local | Coqlib | Unknown
-
-let coq_module m = String.length m >= 4 && String.sub m 0 4 = "Coq."
-
-let find_module m =
- if Hashtbl.mem local_modules m then
- Local
- else if coq_module m then
- Coqlib
- else
- Unknown
-
-
-(* Building indexes *)
-
-type 'a index = {
- idx_name : string;
- idx_entries : (char * (string * 'a) list) list;
- idx_size : int }
-
-let map f i =
- { i with idx_entries =
- List.map
- (fun (c,l) -> (c, List.map (fun (s,x) -> (s,f s x)) l))
- i.idx_entries }
-
-let compare_entries (s1,_) (s2,_) = Alpha.compare_string s1 s2
-
-let sort_entries el =
- let t = Hashtbl.create 97 in
- List.iter
- (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"
- | Definition -> "definition"
- | Inductive -> "inductive"
- | Constructor -> "constructor"
- | Lemma -> "lemma"
- | Record -> "record"
- | Projection -> "projection"
- | Instance -> "instance"
- | Class -> "class"
- | Method -> "method"
- | Variable -> "variable"
- | Axiom -> "axiom"
- | TacticDefinition -> "tactic"
- | Abbreviation -> "abbreviation"
- | Notation -> "notation"
- | Section -> "section"
-
-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)
- 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;
- 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. *)
-let digit = ['0'-'9']
-let num = digit+
-
-let space =
- [' ' '\010' '\013' '\009' '\012']
-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 id = firstchar identchar*
-let pfx_id = (id '.')*
-let ident = id | pfx_id id
-
-let begin_hide = "(*" space* "begin" space+ "hide" space* "*)"
-let end_hide = "(*" space* "end" space+ "hide" space* "*)"
-
-(*s Indexing entry point. *)
-
-rule traverse = parse
- | ("Program" space+)? "Definition" space
- { current_type := Definition; index_ident lexbuf; traverse lexbuf }
- | "Tactic" space+ "Definition" space
- { current_type := TacticDefinition; index_ident lexbuf; traverse lexbuf }
- | ("Axiom" | "Parameter") space
- { current_type := Axiom; index_ident lexbuf; traverse lexbuf }
- | ("Program" space+)? "Fixpoint" space
- { current_type := Definition; index_ident lexbuf; fixpoint lexbuf;
- traverse lexbuf }
- | ("Program" space+)? ("Lemma" | "Theorem") space
- { current_type := Lemma; index_ident lexbuf; traverse lexbuf }
- | "Obligation" space num ("of" ident)?
- { current_type := Lemma; index_ident lexbuf; traverse lexbuf }
- | "Inductive" space
- { current_type := Inductive;
- index_ident lexbuf; inductive lexbuf; traverse lexbuf }
- | "Record" space
- { current_type := Inductive; index_ident lexbuf; traverse lexbuf }
- | "Module" (space+ "Type")? space
- { 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"))?
- { module_refs lexbuf; traverse lexbuf }
- | "End" space+
- { end_ident lexbuf; traverse lexbuf }
- | begin_hide
- { skip_hide lexbuf; traverse lexbuf }
- | "(*"
- { comment lexbuf; traverse lexbuf }
- | '"'
- { string lexbuf; traverse lexbuf }
- | eof
- { () }
- | _
- { traverse lexbuf }
-
-(*s Index one identifier. *)
-
-and index_ident = parse
- | space+
- { index_ident lexbuf }
- | ident
- { 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
- { () }
- | _
- { () }
-
-(*s Index identifiers separated by blanks and/or commas. *)
-
-and index_idents = parse
- | space+ | ','
- { index_idents lexbuf }
- | ident
- { add_def (lexeme_start lexbuf) !current_type "" (lexeme lexbuf);
- index_idents lexbuf }
- | eof
- { () }
- | _
- { 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 }
- | "with" space
- { current_type := Inductive; index_ident lexbuf; inductive lexbuf }
- | '.'
- { () }
- | eof
- { () }
- | _
- { inductive lexbuf }
-
-(*s Index identifiers in a Fixpoint declaration. *)
-
-and fixpoint = parse
- | "with" space
- { index_ident lexbuf; fixpoint lexbuf }
- | '.'
- { () }
- | eof
- { () }
- | _
- { fixpoint lexbuf }
-
-(*s Skip a possibly nested comment. *)
-
-and comment = parse
- | "*)" { () }
- | "(*" { comment lexbuf; comment lexbuf }
- | '"' { string lexbuf; comment lexbuf }
- | eof { eprintf " *** Unterminated comment while indexing" }
- | _ { 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 }
- | '"' { string lexbuf; module_ident lexbuf }
- | ident space* ":="
- { () }
- | ident
- { let id = lexeme lexbuf in
- begin_module id; add_def (lexeme_start lexbuf) !current_type "" id }
- | eof
- { () }
- | _
- { () }
-
-(*s parse module names *)
-
-and module_refs = parse
- | space+
- { module_refs lexbuf }
- | ident
- { let id = lexeme lexbuf in
- (try
- add_mod !current_library (lexeme_start lexbuf) (Hashtbl.find modules id) id
- with
- Not_found -> ()
- );
- module_refs lexbuf }
- | eof
- { () }
- | _
- { () }
-
-{
- let type_of_string = function
- | "def" | "coe" | "subclass" | "canonstruc" | "fix" | "cofix"
- | "ex" | "scheme" -> Definition
- | "prf" | "thm" -> Lemma
- | "ind" | "coind" -> Inductive
- | "constr" -> Constructor
- | "rec" | "corec" -> Record
- | "proj" -> Projection
- | "class" -> Class
- | "meth" -> Method
- | "inst" -> Instance
- | "var" -> Variable
- | "defax" | "prfax" | "ax" -> Axiom
- | "syndef" -> Abbreviation
- | "not" -> Notation
- | "lib" -> Library
- | "mod" | "modtype" -> Module
- | "tac" -> TacticDefinition
- | "sec" -> Section
- | s -> raise (Invalid_argument ("type_of_string:" ^ s))
-
- let read_glob f =
- let c = open_in f in
- let cur_mod = ref "" in
- try
- while true do
- let s = input_line c in
- let n = String.length s in
- if n > 0 then begin
- match s.[0] with
- | 'F' ->
- cur_mod := String.sub s 1 (n - 1);
- current_library := !cur_mod
- | 'R' ->
- (try
- Scanf.sscanf s "R%d %s %s %s %s"
- (fun loc lib_dp sp id ty ->
- add_ref !cur_mod loc lib_dp sp id (type_of_string ty))
- with _ -> ())
- | _ ->
- try Scanf.sscanf s "%s %d %s %s"
- (fun ty loc sp id -> add_def loc (type_of_string ty) sp id)
- with Scanf.Scan_failure _ -> ()
- end
- done; assert false
- with End_of_file ->
- close_in c; !cur_mod
-
- let scan_file f m =
- init_stack (); current_library := m;
- let c = open_in f in
- let lb = from_channel c in
- traverse lb;
- close_in c
-}
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 2ee9ac96..67c63865 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: main.ml 12187 2009-06-13 19:36:59Z msozeau $ i*)
+(*i $Id$ i*)
(* Modified by Lionel Elie Mamane <lionel@mamane.lu> on 9 & 10 Mar 2004:
* - handling of absolute filenames (function coq_module)
@@ -46,6 +46,7 @@ let usage () =
prerr_endline " --with-footer <file> append <file> as html footer";
prerr_endline " --no-index do not output the index";
prerr_endline " --multi-index index split in multiple files";
+ prerr_endline " --index <string> set index name (default is index)";
prerr_endline " --toc output a table of contents";
prerr_endline " --vernac <file> consider <file> as a .v file";
prerr_endline " --tex <file> consider <file> as a .tex file";
@@ -53,8 +54,9 @@ let usage () =
prerr_endline " --files-from <file> read file names to process in <file>";
prerr_endline " --glob-from <file> read globalization information from <file>";
prerr_endline " --quiet quiet mode (default)";
- prerr_endline " --verbose verbose mode";
+ prerr_endline " --verbose verbose mode";
prerr_endline " --no-externals no links to Coq standard library";
+ prerr_endline " --external <url> <d> set URL for external library d";
prerr_endline " --coqlib <url> set URL for Coq standard library";
prerr_endline (" (default is " ^ Coq_config.wwwstdlib ^ ")");
prerr_endline " --boot run in boot mode";
@@ -66,6 +68,11 @@ let usage () =
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 " --parse-comments parse regular comments";
+ prerr_endline " --plain-comments consider comments as non-literate text";
+ prerr_endline " --toc-depth <int> don't include TOC entries for sections below level <int>";
+ 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 "";
exit 1
@@ -74,20 +81,20 @@ let obsolete s =
(*s \textbf{Banner.} Always printed. Notice that it is printed on error
output, so that when the output of [coqdoc] is redirected this header
- is not (unless both standard and error outputs are redirected, of
+ is not (unless both standard and error outputs are redirected, of
course). *)
let banner () =
eprintf "This is coqdoc version %s, compiled on %s\n"
Coq_config.version Coq_config.compile_date;
flush stderr
-
-let target_full_name f =
+
+let target_full_name f =
match !Cdglobals.target_language with
| HTML -> f ^ ".html"
| Raw -> f ^ ".txt"
| _ -> f ^ ".tex"
-
+
(*s \textbf{Separation of files.} Files given on the command line are
separated according to their type, which is determined by their
suffix. Coq files have suffixe \verb!.v! or \verb!.g! and \LaTeX\
@@ -95,12 +102,12 @@ let target_full_name f =
let check_if_file_exists f =
if not (Sys.file_exists f) then begin
- eprintf "\ncoqdoc: %s: no such file\n" f;
+ eprintf "coqdoc: %s: no such file\n" f;
exit 1
end
-(*s Manipulations of paths and path aliases *)
+(*s Manipulations of paths and path aliases *)
let normalize_path p =
(* We use the Unix subsystem to normalize a physical path (relative
@@ -109,50 +116,43 @@ let normalize_path p =
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
+ 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
- Filename.concat (normalize_path dirname) basename
+ normalize_path dirname, basename
(* [paths] maps a physical path to a name *)
let paths = ref []
-
-let add_path dir name =
- (* if dir is relative we add both the relative and absolute name *)
+
+let add_path dir name =
let p = normalize_path dir in
- paths := (p,name) :: !paths
-
-(* turn A/B/C into A.B.C *)
-let name_of_path = Str.global_replace (Str.regexp "/") ".";;
+ paths := (p,name) :: !paths
-let coq_module filename =
+(* turn A/B/C into A.B.C *)
+let rec name_of_path p name dirname suffix =
+ if p = dirname then String.concat "." (name::suffix)
+ else
+ let subdir = Filename.dirname dirname in
+ if subdir = dirname then raise Not_found
+ else name_of_path p name subdir (Filename.basename dirname::suffix)
+
+let coq_module filename =
let bfname = Filename.chop_extension filename in
- let nfname = normalize_filename bfname in
- let rec change_prefix map f =
- match map with
- | [] ->
- (* There is no prefix alias;
- we just cut the name wrt current working directory *)
- let cwd = Sys.getcwd () in
- let exp = Str.regexp (Str.quote (cwd ^ "/")) in
- if (Str.string_match exp f 0) then
- name_of_path (Str.replace_first exp "" f)
- else
- name_of_path f
- | (p, name) :: rem ->
- let expp = Str.regexp (Str.quote p) in
- if (Str.string_match expp f 0) then
- let newp = Str.replace_first expp name f in
- name_of_path newp
- else
- change_prefix rem f
+ let dirname, fname = normalize_filename bfname in
+ let rec change_prefix = function
+ (* Follow coqc: if in scope of -R, substitute logical name *)
+ (* otherwise, keep only base name *)
+ | [] -> fname
+ | (p, name) :: rem ->
+ try name_of_path p name dirname [fname]
+ with Not_found -> change_prefix rem
in
- change_prefix !paths nfname
+ change_prefix !paths
let what_file f =
check_if_file_exists f;
@@ -160,10 +160,10 @@ let what_file f =
Vernac_file (f, coq_module f)
else if Filename.check_suffix f ".tex" then
Latex_file f
- else
+ else
(eprintf "\ncoqdoc: don't know what to do with %s\n" f; exit 1)
-
-(*s \textbf{Reading file names from a file.}
+
+(*s \textbf{Reading file names from a file.}
* File names may be given
* in a file instead of being given on the command
* line. [(files_from_file f)] returns the list of file names contained
@@ -181,7 +181,7 @@ let files_from_file f =
| ' ' | '\t' | '\n' ->
if Buffer.length buf > 0 then l := (Buffer.contents buf) :: !l;
Buffer.clear buf
- | c ->
+ | c ->
Buffer.add_char buf c
done; []
with End_of_file ->
@@ -193,12 +193,12 @@ let files_from_file f =
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;
+ eprintf "coqdoc: cannot read from file %s (%s)\n" f s;
exit 1
end
-
+
(*s \textbf{Parsing of the command line.} *)
-
+
let dvi = ref false
let ps = ref false
let pdf = ref false
@@ -208,7 +208,7 @@ let parse () =
let add_file f = files := f :: !files in
let rec parse_rec = function
| [] -> ()
-
+
| ("-nopreamble" | "--nopreamble" | "--no-preamble"
| "-bodyonly" | "--bodyonly" | "--body-only") :: rem ->
header_trailer := false; parse_rec rem
@@ -228,17 +228,21 @@ let parse () =
index := false; parse_rec rem
| ("-multi-index" | "--multi-index") :: rem ->
multi_index := true; parse_rec rem
+ | ("-index" | "--index") :: s :: rem ->
+ Cdglobals.index_name := s; parse_rec rem
+ | ("-index" | "--index") :: [] ->
+ usage ()
| ("-toc" | "--toc" | "--table-of-contents") :: rem ->
toc := true; parse_rec rem
| ("-stdout" | "--stdout") :: rem ->
out_to := StdOut; parse_rec rem
| ("-o" | "--output") :: f :: rem ->
out_to := File (Filename.basename f); output_dir := Filename.dirname f; parse_rec rem
- | ("-o" | "--output") :: [] ->
+ | ("-o" | "--output") :: [] ->
usage ()
| ("-d" | "--directory") :: dir :: rem ->
output_dir := dir; parse_rec rem
- | ("-d" | "--directory") :: [] ->
+ | ("-d" | "--directory") :: [] ->
usage ()
| ("-s" | "--short") :: rem ->
short := true; parse_rec rem
@@ -276,39 +280,60 @@ let parse () =
Cdglobals.raw_comments := true; parse_rec rem
| ("-parse-comments" | "--parse-comments") :: rem ->
Cdglobals.parse_comments := true; parse_rec rem
+ | ("-plain-comments" | "--plain-comments") :: rem ->
+ Cdglobals.plain_comments := true; parse_rec rem
| ("-interpolate" | "--interpolate") :: rem ->
Cdglobals.interpolate := true; parse_rec rem
+ | ("-toc-depth" | "--toc-depth") :: [] ->
+ usage ()
+ | ("-toc-depth" | "--toc-depth") :: ds :: rem ->
+ let d = try int_of_string ds with
+ Failure _ ->
+ (eprintf "--toc-depth must be followed by an integer\n";
+ exit 1)
+ in
+ Cdglobals.toc_depth := Some d;
+ parse_rec rem
+ | ("-no-lib-name" | "--no-lib-name") :: rem ->
+ Cdglobals.lib_name := "";
+ parse_rec rem
+ | ("-lib-name" | "--lib-name") :: ds :: rem ->
+ Cdglobals.lib_name := ds;
+ parse_rec rem
+ | ("-lib-subtitles" | "--lib-subtitles") :: rem ->
+ Cdglobals.lib_subtitles := true;
+ parse_rec rem
| ("-latin1" | "--latin1") :: rem ->
Cdglobals.set_latin1 (); parse_rec rem
| ("-utf8" | "--utf8") :: rem ->
Cdglobals.set_utf8 (); parse_rec rem
-
+
| ("-q" | "-quiet" | "--quiet") :: rem ->
quiet := true; parse_rec rem
| ("-v" | "-verbose" | "--verbose") :: rem ->
quiet := false; parse_rec rem
-
+
| ("-h" | "-help" | "-?" | "--help") :: rem ->
banner (); usage ()
| ("-V" | "-version" | "--version") :: _ ->
banner (); exit 0
- | ("-vernac-file" | "--vernac-file") :: f :: rem ->
+ | ("-vernac-file" | "--vernac-file") :: f :: rem ->
check_if_file_exists f;
add_file (Vernac_file (f, coq_module f)); parse_rec rem
| ("-vernac-file" | "--vernac-file") :: [] ->
usage ()
- | ("-tex-file" | "--tex-file") :: f :: rem ->
+ | ("-tex-file" | "--tex-file") :: f :: rem ->
add_file (Latex_file f); parse_rec rem
| ("-tex-file" | "--tex-file") :: [] ->
usage ()
| ("-files" | "--files" | "--files-from") :: f :: rem ->
- List.iter (fun f -> add_file (what_file f)) (files_from_file f);
+ List.iter (fun f -> add_file (what_file f)) (files_from_file f);
parse_rec rem
| ("-files" | "--files") :: [] ->
usage ()
- | "-R" :: path :: log :: rem ->
+ | "-R" :: path :: log :: rem ->
add_path path log; parse_rec rem
| "-R" :: ([] | [_]) ->
usage ()
@@ -318,6 +343,8 @@ let parse () =
usage ()
| ("--no-externals" | "-no-externals" | "-noexternals") :: rem ->
Cdglobals.externals := false; parse_rec rem
+ | ("--external" | "-external") :: u :: logicalpath :: rem ->
+ Index.add_external_library logicalpath u; parse_rec rem
| ("--coqlib" | "-coqlib") :: u :: rem ->
Cdglobals.coqlib := u; parse_rec rem
| ("--coqlib" | "-coqlib") :: [] ->
@@ -328,16 +355,15 @@ let parse () =
Cdglobals.coqlib_path := d; parse_rec rem
| ("--coqlib_path" | "-coqlib_path") :: [] ->
usage ()
- | f :: rem ->
+ | f :: rem ->
add_file (what_file f); parse_rec rem
- in
+ in
parse_rec (List.tl (Array.to_list Sys.argv));
- Output.initialize ();
List.rev !files
-
+
(*s The following function produces the output. The default output is
- the \LaTeX\ document: in that case, we just call [Web.produce_document].
+ the \LaTeX\ document: in that case, we just call [Web.produce_document].
If option \verb!-dvi!, \verb!-ps! or \verb!-html! is invoked, then
we make calls to \verb!latex! or \verb!dvips! or \verb!pdflatex! accordingly. *)
@@ -359,9 +385,9 @@ let clean_temp_files basefile =
remove (basefile ^ ".pdf");
remove (basefile ^ ".haux");
remove (basefile ^ ".html")
-
+
let clean_and_exit file res = clean_temp_files file; exit res
-
+
let cat file =
let c = open_in file in
try
@@ -370,20 +396,26 @@ let cat file =
close_in c
let copy src dst =
- let cin = open_in src
- and cout = open_out dst in
+ let cin = open_in src in
+ try
+ let 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
-
+ close_out cout;
+ close_in cin
+ with Sys_error e ->
+ eprintf "%s\n" e;
+ exit 1
(*s Functions for generating output files *)
let gen_one_file l =
let file = function
- | Vernac_file (f,m) ->
- Output.set_module m; Pretty.coq_file f m
+ | Vernac_file (f,m) ->
+ let sub = if !lib_subtitles then Cpretty.detect_subtitle f m else None in
+ Output.set_module m sub;
+ Cpretty.coq_file f m
| Latex_file _ -> ()
in
if (!header_trailer) then Output.header ();
@@ -391,74 +423,73 @@ let gen_one_file l =
List.iter file l;
if !index then Output.make_index();
if (!header_trailer) then Output.trailer ()
-
+
let gen_mult_files l =
let file = function
- | Vernac_file (f,m) ->
- Output.set_module m;
+ | Vernac_file (f,m) ->
+ let sub = if !lib_subtitles then Cpretty.detect_subtitle f m else None in
let hf = target_full_name m in
+ Output.set_module m sub;
open_out_file hf;
- if (!header_trailer) then Output.header ();
- Pretty.coq_file f m;
+ if (!header_trailer) then Output.header ();
+ Cpretty.coq_file f m;
if (!header_trailer) then Output.trailer ();
close_out_file()
| Latex_file _ -> ()
in
List.iter file l;
if (!index && !target_language=HTML) then begin
- if (!multi_index) then Output.make_multi_index ();
- open_out_file "index.html";
+ if (!multi_index) then Output.make_multi_index ();
+ open_out_file (!index_name^".html");
page_title := (if !title <> "" then !title else "Index");
- if (!header_trailer) then Output.header ();
- Output.make_index ();
+ if (!header_trailer) then Output.header ();
+ Output.make_index ();
if (!header_trailer) then Output.trailer ();
close_out_file()
end;
if (!toc && !target_language=HTML) then begin
- open_out_file "toc.html";
+ open_out_file "toc.html";
page_title := (if !title <> "" then !title else "Table of contents");
if (!header_trailer) then Output.header ();
if !title <> "" then printf "<h1>%s</h1>\n" !title;
- Output.make_toc ();
+ Output.make_toc ();
if (!header_trailer) then Output.trailer ();
close_out_file()
- end
+ end
(* Rq: pour latex et texmacs, une toc ou un index séparé n'a pas de sens... *)
-let read_glob x =
- match x with
- | Vernac_file (f,m) ->
- let glob = (Filename.chop_extension f) ^ ".glob" in
- (try
- Vernac_file (f, Index.read_glob glob)
- with e ->
- eprintf "Warning: file %s cannot be used; links will not be available: %s\n" glob (Printexc.to_string e);
- x)
- | Latex_file _ -> x
+let 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_of = function
+ | Vernac_file (f,_) -> read_glob_file (Filename.chop_extension f ^ ".glob")
+ | Latex_file _ -> ()
let index_module = function
- | Vernac_file (f,m) ->
+ | Vernac_file (f,m) ->
Index.add_module m
| Latex_file _ -> ()
-
+
+let copy_style_file file =
+ let src =
+ List.fold_left
+ Filename.concat !Cdglobals.coqlib_path ["tools";"coqdoc";file] in
+ let dst = coqdoc_out file in
+ if Sys.file_exists src then copy src dst
+ else eprintf "Warning: file %s does not exist\n" src
+
let produce_document l =
- (if !target_language=HTML then
- 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
- if (Sys.file_exists src) then (copy src dst) else eprintf "Warning: file %s does not exist\n" src);
- (if !target_language=LaTeX then
- let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.sty") in
- let dst = if !output_dir <> "" then
- Filename.concat !output_dir "coqdoc.sty"
- else "coqdoc.sty" in
- if Sys.file_exists src then copy src dst else eprintf "Warning: file %s does not exist\n" src);
+ if !target_language=HTML then copy_style_file "coqdoc.css";
+ if !target_language=LaTeX then copy_style_file "coqdoc.sty";
(match !Cdglobals.glob_source with
| NoGlob -> ()
- | DotGlob -> ignore (List.map read_glob l)
- | GlobFile f -> ignore (Index.read_glob f));
+ | DotGlob -> List.iter read_glob_file_of l
+ | GlobFile f -> read_glob_file f);
List.iter index_module l;
match !out_to with
- | StdOut ->
+ | StdOut ->
Cdglobals.out_channel := stdout;
gen_one_file l
| File f ->
@@ -467,11 +498,11 @@ let produce_document l =
close_out_file()
| MultFiles ->
gen_mult_files l
-
+
let produce_output fl =
- if not (!dvi || !ps || !pdf) then
+ if not (!dvi || !ps || !pdf) then
produce_document fl
- else
+ else
begin
let texfile = Filename.temp_file "coqdoc" ".tex" in
let basefile = Filename.chop_suffix texfile ".tex" in
@@ -479,52 +510,52 @@ let produce_output fl =
out_to := File texfile;
output_dir := (Filename.dirname texfile);
produce_document fl;
-
+
let latexexe = if !pdf then "pdflatex" else "latex" in
- let latexcmd =
+ let latexcmd =
let file = Filename.basename texfile in
- let file =
- if !quiet then sprintf "'\\nonstopmode\\input{%s}'" file else file
+ let file =
+ if !quiet then sprintf "'\\nonstopmode\\input{%s}'" file else file
in
sprintf "%s %s && %s %s 1>&2 %s" latexexe file latexexe file (if !quiet then "> /dev/null" else "")
in
let res = locally (Filename.dirname texfile) Sys.command latexcmd in
if res <> 0 then begin
- eprintf "Couldn't run LaTeX successfully\n";
+ eprintf "Couldn't run LaTeX successfully\n";
clean_and_exit basefile res
end;
-
+
let dvifile = basefile ^ ".dvi" in
- if !dvi then
+ if !dvi then
begin
match final_out_to with
| MultFiles | StdOut -> cat dvifile
| File f -> copy dvifile f
end;
let pdffile = basefile ^ ".pdf" in
- if !pdf then
+ if !pdf then
begin
match final_out_to with
| MultFiles | StdOut -> cat pdffile
| File f -> copy pdffile f
end;
if !ps then begin
- let psfile = basefile ^ ".ps"
+ let psfile = basefile ^ ".ps"
in
- let command =
- sprintf "dvips %s -o %s %s" dvifile psfile
+ let command =
+ sprintf "dvips %s -o %s %s" dvifile psfile
(if !quiet then "> /dev/null 2>&1" else "")
in
let res = Sys.command command in
if res <> 0 then begin
- eprintf "Couldn't run dvips successfully\n";
+ eprintf "Couldn't run dvips successfully\n";
clean_and_exit basefile res
end;
match final_out_to with
| MultFiles | StdOut -> cat psfile
| File f -> copy psfile f
end;
-
+
clean_temp_files basefile
end
@@ -534,7 +565,8 @@ let produce_output fl =
let main () =
let files = parse () in
+ Index.init_coqlib_library ();
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 1ad8b14f..93e1f843 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: output.ml 12187 2009-06-13 19:36:59Z msozeau $ i*)
+(*i $Id$ i*)
open Cdglobals
open Index
@@ -25,26 +25,26 @@ let sprintf = Printf.sprintf
(*s Coq keywords *)
-let build_table l =
+let build_table l =
let h = Hashtbl.create 101 in
List.iter (fun key ->Hashtbl.add h key ()) l;
function s -> try Hashtbl.find h s; true with Not_found -> false
-let is_keyword =
+let is_keyword =
build_table
[ "AddPath"; "Axiom"; "Abort"; "Boxed"; "Chapter"; "Check"; "Coercion"; "CoFixpoint";
- "CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example";
+ "CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example";
"Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint";
- "Hypothesis"; "Hypotheses";
- "Resolve"; "Unfold"; "Immediate"; "Extern"; "Implicit"; "Import"; "Inductive";
- "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac";
+ "Hypothesis"; "Hypotheses";
+ "Resolve"; "Unfold"; "Immediate"; "Extern"; "Implicit"; "Import"; "Inductive";
+ "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac";
"Module"; "Module Type"; "Declare Module"; "Include";
"Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Proof with"; "Qed";
"Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme";
- "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem";
+ "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem";
"Set"; "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context";
"Notation"; "Reserved Notation"; "Tactic Notation";
- "Delimit"; "Bind"; "Open"; "Scope";
+ "Delimit"; "Bind"; "Open"; "Scope";
"Boxed"; "Unboxed"; "Inline";
"Implicit Arguments"; "Add"; "Strict";
"Typeclasses"; "Instance"; "Global Instance"; "Class"; "Instantiation";
@@ -54,13 +54,13 @@ let is_keyword =
"Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next";
"Program Instance"; "Equations"; "Equations_nocomp";
(*i (* coq terms *) *)
- "forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun";
+ "forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let"; "fun";
"if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"; "struct"; "wf"; "measure";
(* Ltac *)
"before"; "after"
]
-let is_tactic =
+let is_tactic =
build_table
[ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection";
"elimtype"; "progress"; "setoid_rewrite";
@@ -77,30 +77,51 @@ let is_tactic =
(*s Current Coq module *)
-let current_module = ref ""
+let current_module : (string * string option) ref = ref ("",None)
-let set_module m = current_module := m; page_title := m
+let get_module withsub =
+ let (m,sub) = !current_module in
+ if withsub then
+ match sub with
+ | None -> m
+ | Some sub -> m ^ ": " ^ sub
+ else
+ m
+
+let set_module m sub = current_module := (m,sub);
+ page_title := get_module true
(*s Common to both LaTeX and HTML *)
let item_level = ref 0
-
-(*s Customized pretty-print *)
-
-let token_pp = Hashtbl.create 97
-
-let add_printing_token = Hashtbl.replace token_pp
-
-let find_printing_token tok =
- try Hashtbl.find token_pp tok with Not_found -> None, None
-
-let remove_printing_token = Hashtbl.remove token_pp
-
-(* predefined pretty-prints *)
-let initialize () =
+let in_doc = ref false
+
+(*s Customized and predefined pretty-print *)
+
+let initialize_texmacs () =
+ let ensuremath x = sprintf "<with|mode|math|\\<%s\\>>" x in
+ List.fold_right (fun (s,t) tt -> Tokens.ttree_add tt s t)
+ [ "*", ensuremath "times";
+ "->", ensuremath "rightarrow";
+ "<-", ensuremath "leftarrow";
+ "<->", ensuremath "leftrightarrow";
+ "=>", ensuremath "Rightarrow";
+ "<=", ensuremath "le";
+ ">=", ensuremath "ge";
+ "<>", ensuremath "noteq";
+ "~", ensuremath "lnot";
+ "/\\", ensuremath "land";
+ "\\/", ensuremath "lor";
+ "|-", ensuremath "vdash"
+ ] Tokens.empty_ttree
+
+let token_tree_texmacs = ref (initialize_texmacs ())
+
+let initialize_tex_html () =
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'))
+ 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 "×";
"|", "\\ensuremath{|}", None;
"->", "\\ensuremath{\\rightarrow}", if_utf8 "→";
@@ -119,14 +140,27 @@ let initialize () =
"forall", "\\ensuremath{\\forall}", if_utf8 "∀";
"exists", "\\ensuremath{\\exists}", if_utf8 "∃";
"Π", "\\ensuremath{\\Pi}", if_utf8 "Π";
- "λ", "\\ensuremath{\\lambda}", 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 ()))
+
+let add_printing_token s (t1,t2) =
+ (match t1 with None -> () | Some t1 ->
+ token_tree_latex := Tokens.ttree_add !token_tree_latex s t1);
+ (match t2 with None -> () | Some t2 ->
+ token_tree_html := Tokens.ttree_add !token_tree_html s t2)
+
+let remove_printing_token s =
+ token_tree_latex := Tokens.ttree_remove !token_tree_latex s;
+ token_tree_html := Tokens.ttree_remove !token_tree_html s
(*s Table of contents *)
-type toc_entry =
- | Toc_library of string
+type toc_entry =
+ | Toc_library of string * string option
| Toc_section of int * (unit -> unit) * string
let (toc_q : toc_entry Queue.t) = Queue.create ()
@@ -140,7 +174,6 @@ let new_label = let r = ref 0 in fun () -> incr r; "lab" ^ string_of_int !r
module Latex = struct
let in_title = ref false
- let in_doc = ref false
(*s Latex preamble *)
@@ -155,10 +188,14 @@ module Latex = struct
printf "\\usepackage[T1]{fontenc}\n";
printf "\\usepackage{fullpage}\n";
printf "\\usepackage{coqdoc}\n";
+ printf "\\usepackage{amsmath,amssymb}\n";
+ (match !toc_depth with
+ | None -> ()
+ | Some n -> printf "\\setcounter{tocdepth}{%i}\n" n);
Queue.iter (fun s -> printf "%s\n" s) preamble;
printf "\\begin{document}\n"
end;
- output_string
+ output_string
"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n";
output_string
"%% This file has been automatically generated with the command\n";
@@ -173,21 +210,28 @@ module Latex = struct
printf "\\end{document}\n"
end
+ (*s Latex low-level translation *)
+
+ let nbsp () = output_char '~'
+
let char c = match c with
- | '\\' ->
+ | '\\' ->
printf "\\symbol{92}"
- | '$' | '#' | '%' | '&' | '{' | '}' | '_' ->
+ | '$' | '#' | '%' | '&' | '{' | '}' | '_' ->
output_char '\\'; output_char c
- | '^' | '~' ->
+ | '^' | '~' ->
output_char '\\'; output_char c; printf "{}"
- | _ ->
+ | _ ->
output_char c
let label_char c = match c with
- | '\\' | '$' | '#' | '%' | '&' | '{' | '}' | '_'
- | '^' | '~' -> ()
- | _ ->
- output_char c
+ | '_' -> output_char ' '
+ | '\\' | '$' | '#' | '%' | '&' | '{' | '}'
+ | '^' | '~' -> printf "x%X" (Char.code c)
+ | _ -> if c >= '\x80' then printf "x%X" (Char.code c) else output_char c
+
+ let label_ident s =
+ for i = 0 to String.length s - 1 do label_char s.[i] done
let latex_char = output_char
let latex_string = output_string
@@ -195,19 +239,36 @@ module Latex = struct
let html_char _ = ()
let html_string _ = ()
- let raw_ident s =
- for i = 0 to String.length s - 1 do char s.[i] done
-
- let label_ident s =
- for i = 0 to String.length s - 1 do label_char s.[i] done
-
- let start_module () =
- if not !short then begin
- printf "\\coqlibrary{";
- label_ident !current_module;
- printf "}{";
- raw_ident !current_module;
- printf "}\n\n"
+ (*s Latex char escaping *)
+
+ let escaped =
+ let buff = Buffer.create 5 in
+ fun s ->
+ Buffer.clear buff;
+ for i = 0 to String.length s - 1 do
+ match s.[i] with
+ | '\\' ->
+ Buffer.add_string buff "\\symbol{92}"
+ | '$' | '#' | '%' | '&' | '{' | '}' | '_' as c ->
+ Buffer.add_char buff '\\'; Buffer.add_char buff c
+ | '^' | '~' as c ->
+ Buffer.add_char buff '\\'; Buffer.add_char buff c;
+ Buffer.add_string buff "{}"
+ | c ->
+ Buffer.add_char buff c
+ done;
+ Buffer.contents buff
+
+ (*s Latex reference and symbol translation *)
+
+ let start_module () =
+ let ln = !lib_name in
+ if not !short then begin
+ printf "\\coqlibrary{";
+ label_ident (get_module false);
+ printf "}{";
+ if ln <> "" then printf "%s " ln;
+ printf "}{%s}\n\n" (escaped (get_module true))
end
let start_latex_math () = output_char '$'
@@ -218,89 +279,101 @@ module Latex = struct
let stop_verbatim () = printf "\\end{verbatim}\n"
- let indentation n =
- if n == 0 then
+ let indentation n =
+ if n == 0 then
printf "\\coqdocnoindent\n"
else
let space = 0.5 *. (float n) in
printf "\\coqdocindent{%2.2fem}\n" space
- let with_latex_printing f tok =
- try
- (match Hashtbl.find token_pp tok with
- | Some s, _ -> output_string s
- | _ -> f tok)
- with Not_found ->
- f tok
-
- let module_ref m s =
- printf "\\moduleid{%s}{" m; raw_ident s; printf "}"
- (*i
- match find_module m with
- | Local ->
- printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>"
- | Coqlib when !externals ->
- let m = Filename.concat !coqlib m in
- printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>"
- | Coqlib | Unknown ->
- raw_ident s
- i*)
+ let module_ref m s =
+ printf "\\moduleid{%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
| Local ->
- printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}"
- | Coqlib when !externals ->
- let _m = Filename.concat !coqlib m in
- printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}"
- | Coqlib | Unknown ->
- printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}"
+ if typ = Variable then
+ printf "\\coqdoc%s{%s}" (type_name typ) s
+ else
+ (printf "\\coqref{"; label_ident id;
+ printf "}{\\coqdoc%s{%s}}" (type_name typ) s)
+ | External m when !externals ->
+ printf "\\coqexternalref{"; label_ident fid;
+ printf "}{%s}{\\coqdoc%s{%s}}" (escaped m) (type_name typ) s
+ | External _ | Unknown ->
+ printf "\\coqdoc%s{%s}" (type_name typ) s
let defref m id ty s =
- printf "\\coq%s{" (type_name ty); label_ident (m ^ "." ^ id); printf "}{"; raw_ident s; printf "}"
+ printf "\\coqdef{"; label_ident (m ^ "." ^ id);
+ printf "}{%s}{\\coqdoc%s{%s}}" s (type_name ty) s
let reference s = function
- | Def (fullid,typ) ->
- defref !current_module fullid typ s
+ | Def (fullid,typ) ->
+ defref (get_module false) fullid typ s
| Mod (m,s') when s = s' ->
module_ref m s
- | Ref (m,fullid,typ) ->
+ | Ref (m,fullid,typ) ->
ident_ref m fullid typ s
| Mod _ ->
- printf "\\coqdocvar{"; raw_ident s; printf "}"
-
- let ident s loc =
- if is_keyword s then begin
- printf "\\coqdockw{"; raw_ident s; printf "}"
- end else begin
- begin
+ printf "\\coqdocvar{%s}" (escaped s)
+
+ (*s The sublexer buffers symbol characters and attached
+ uninterpreted ident and try to apply special translation such as,
+ predefined, translation "->" to "\ensuremath{\rightarrow}" or,
+ virtually, a user-level translation from "=_h" to "\ensuremath{=_{h}}" *)
+
+ let output_sublexer_string doescape issymbchar tag s =
+ let s = if doescape then escaped s else s in
+ match tag with
+ | Some ref -> reference s ref
+ | None -> if issymbchar then output_string s else printf "\\coqdocvar{%s}" s
+
+ 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
+
+ let initialize () =
+ Tokens.token_tree := token_tree_latex;
+ Tokens.outfun := output_sublexer_string
+
+ (*s Interpreting ident with fallback on sublexer if unknown ident *)
+
+ let translate s =
+ match Tokens.translate s with Some s -> s | None -> escaped s
+
+ let ident s loc =
+ try
+ 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)
+ else if is_keyword s then
+ printf "\\coqdockw{%s}" (translate s)
+ else if !Cdglobals.interpolate && !in_doc (* always a var otherwise *)
+ then
try
- 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
- if !Cdglobals.interpolate && !in_doc (* always a var otherwise *)
- 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
+ let tag = Index.find_string (get_module false) s in
+ reference (translate s) tag
+ with _ -> Tokens.output_tagged_ident_string s
+ else Tokens.output_tagged_ident_string s
- let ident s l =
+ let ident s l =
if !in_title then (
printf "\\texorpdfstring{\\protect";
- with_latex_printing (fun s -> ident s l) s;
- printf "}{"; raw_ident s; printf "}")
+ ident s l;
+ printf "}{%s}" (translate s))
else
- with_latex_printing (fun s -> ident s l) s
-
- let symbol s = with_latex_printing raw_ident s
+ ident s l
+
+ (*s Translating structure *)
+
+ let proofbox () = printf "\\ensuremath{\\Box}"
- let rec reach_item_level n =
+ let rec reach_item_level n =
if !item_level < n then begin
printf "\n\\begin{itemize}\n\\item "; incr item_level;
reach_item_level n
@@ -320,7 +393,11 @@ module Latex = struct
let end_doc () = in_doc := false; stop_item ()
- let comment c = char c
+ (* This is broken if we are in math mode, but coqdoc currently isn't
+ tracking that *)
+ let start_emph () = printf "\\textit{"
+
+ let stop_emph () = printf "}"
let start_comment () = printf "\\begin{coqdoccomment}\n"
@@ -350,12 +427,16 @@ module Latex = struct
let rule () =
printf "\\par\n\\noindent\\hrulefill\\par\n\\noindent{}"
- let paragraph () = stop_item (); printf "\n\n"
+ let paragraph () = printf "\n\n"
let line_break () = printf "\\coqdoceol\n"
let empty_line_of_code () = printf "\\coqdocemptyline\n"
+ let start_inline_coq_block () = line_break (); empty_line_of_code ()
+
+ let end_inline_coq_block () = empty_line_of_code ()
+
let start_inline_coq () = ()
let end_inline_coq () = ()
@@ -377,9 +458,9 @@ module Html = struct
if !header_trailer then
if !header_file_spec then
let cin = Pervasives.open_in !header_file in
- try
- while true do
- let s = Pervasives.input_line cin in
+ try
+ while true do
+ let s = Pervasives.input_line cin in
printf "%s\n" s
done
with End_of_file -> Pervasives.close_in cin
@@ -396,14 +477,14 @@ module Html = struct
end
let trailer () =
- if !index && !current_module <> "Index" then
- printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"index.html\">Index</a>";
- if !header_trailer then
+ if !index && (get_module false) <> "Index" then
+ printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"%s.html\">Index</a>" !index_name;
+ if !header_trailer then
if !footer_file_spec then
let cin = Pervasives.open_in !footer_file in
- try
- while true do
- let s = Pervasives.input_line cin in
+ try
+ while true do
+ let s = Pervasives.input_line cin in
printf "%s\n" s
done
with End_of_file -> Pervasives.close_in cin
@@ -414,26 +495,47 @@ module Html = struct
printf "</div>\n\n</div>\n\n</body>\n</html>"
end
- let start_module () =
+ let start_module () =
+ let ln = !lib_name in
if not !short then begin
- add_toc_entry (Toc_library !current_module);
- printf "<h1 class=\"libtitle\">Library %s</h1>\n\n" !current_module
+ let (m,sub) = !current_module in
+ add_toc_entry (Toc_library (m,sub));
+ if ln = "" then
+ printf "<h1 class=\"libtitle\">%s</h1>\n\n" (get_module true)
+ else
+ printf "<h1 class=\"libtitle\">%s %s</h1>\n\n" ln (get_module true)
end
let indentation n = for i = 1 to n do printf "&nbsp;" done
let line_break () = printf "<br/>\n"
- let empty_line_of_code () =
+ let empty_line_of_code () =
printf "\n<br/>\n"
+ let nbsp () = printf "&nbsp;"
+
let char = function
| '<' -> printf "&lt;"
| '>' -> printf "&gt;"
| '&' -> printf "&amp;"
| c -> output_char c
- let raw_ident s = for i = 0 to String.length s - 1 do char s.[i] done
+ 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 ->
+ Buffer.clear buff;
+ for i = 0 to String.length s - 1 do
+ match s.[i] with
+ | '<' -> Buffer.add_string buff "&lt;"
+ | '>' -> Buffer.add_string buff "&gt;"
+ | '&' -> Buffer.add_string buff "&amp;"
+ | c -> Buffer.add_char buff c
+ done;
+ Buffer.contents buff
let latex_char _ = ()
let latex_string _ = ()
@@ -447,74 +549,81 @@ module Html = struct
let start_verbatim () = printf "<pre>"
let stop_verbatim () = printf "</pre>\n"
- let module_ref m s =
+ let module_ref m s =
match find_module m with
| Local ->
- printf "<a class=\"modref\" href=\"%s.html\">" m; raw_ident s; printf "</a>"
- | Coqlib when !externals ->
- let m = Filename.concat !coqlib m in
- printf "<a class=\"modref\" href=\"%s.html\">" m; raw_ident s; printf "</a>"
- | Coqlib | Unknown ->
- raw_ident s
+ 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 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\">" typ;
- raw_ident s;
- printf "</span></a>"
- | Coqlib when !externals ->
- let m = Filename.concat !coqlib m in
- printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid;
- printf "<span class=\"id\" type=\"%s\">" typ;
- raw_ident s; printf "</span></a>"
- | Coqlib | Unknown ->
- printf "<span class=\"id\" type=\"%s\">" typ; raw_ident s; printf "</span>"
-
- let ident s loc =
- if is_keyword s then begin
- printf "<span class=\"id\" type=\"keyword\">";
- raw_ident s;
- printf "</span>"
- end else
- begin
- try
- (match Index.find !current_module loc with
- | Def (fullid,ty) ->
- printf "<a name=\"%s\">" fullid;
- printf "<span class=\"id\" type=\"%s\">" (type_name ty);
- raw_ident s; printf "</span></a>"
- | Mod (m,s') when s = s' ->
- module_ref m s
- | Ref (m,fullid,ty) ->
- ident_ref m fullid (type_name ty) s
- | Mod _ ->
- printf "<span class=\"id\" type=\"mod\">"; raw_ident s ; printf "</span>")
- with Not_found ->
- if is_tactic s then
- (printf "<span class=\"id\" type=\"tactic\">"; raw_ident s; printf "</span>")
- else
- (printf "<span class=\"id\" type=\"var\">"; raw_ident s ; printf "</span>")
- end
+ printf "<span class=\"id\" type=\"%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
+ | External _ | Unknown ->
+ printf "<span class=\"id\" type=\"%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
+ | 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
+ match tag with
+ | Some ref -> reference s ref
+ | None ->
+ if issymbchar then output_string s
+ else printf "<span class=\"id\" type=\"var\">%s</span>" s
+
+ 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
- let with_html_printing f tok =
- try
- (match Hashtbl.find token_pp tok with
- | _, Some s -> output_string s
- | _ -> f tok)
- with Not_found ->
- f tok
+ let initialize () =
+ Tokens.token_tree := token_tree_html;
+ Tokens.outfun := output_sublexer_string
- let ident s l =
- with_html_printing (fun s -> ident s l) s
+ let translate s =
+ match Tokens.translate s with Some s -> s | None -> escaped s
- let symbol s =
- with_html_printing raw_ident s
+ let ident s loc =
+ if is_keyword s then begin
+ printf "<span class=\"id\" type=\"keyword\">%s</span>" (translate s)
+ end else begin
+ try 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)
+ else
+ if !Cdglobals.interpolate && !in_doc (* always a var otherwise *)
+ then
+ try reference (translate s) (Index.find_string (get_module false) s)
+ with _ -> Tokens.output_tagged_ident_string s
+ else
+ Tokens.output_tagged_ident_string s
+ end
- let rec reach_item_level n =
+ let proofbox () = printf "<font size=-2>&#9744;</font>"
+
+ let rec reach_item_level n =
if !item_level < n then begin
- printf "\n<ul>\n<li>"; incr item_level;
+ printf "<ul>\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;
@@ -532,14 +641,18 @@ module Html = struct
let end_coq () = if not !raw_comments then printf "</div>\n"
- let start_doc () =
+ let start_doc () = in_doc := true;
if not !raw_comments then
printf "\n<div class=\"doc\">\n"
- let end_doc () =
- stop_item ();
+ let end_doc () = in_doc := false;
+ stop_item ();
if not !raw_comments then printf "\n</div>\n"
+ let start_emph () = printf "<i>"
+
+ let stop_emph () = printf "</i>"
+
let start_comment () = printf "<span class=\"comment\">(*"
let end_comment () = printf "*)</span>"
@@ -552,16 +665,19 @@ module Html = struct
let end_inline_coq () = printf "</span>"
- let paragraph () =
- let i = !item_level in
- stop_item ();
- if i > 0 then printf "\n"
- else printf "\n<br/> <br/>\n"
+ let start_inline_coq_block () = line_break (); start_inline_coq ()
+
+ let end_inline_coq_block () = end_inline_coq ()
+
+ let paragraph () = printf "\n<br/> <br/>\n"
let section lev f =
let lab = new_label () in
- let r = sprintf "%s.html#%s" !current_module lab in
- add_toc_entry (Toc_section (lev, f, r));
+ let r = sprintf "%s.html#%s" (get_module false) lab in
+ (match !toc_depth with
+ | None -> add_toc_entry (Toc_section (lev, f, r))
+ | Some n -> if lev <= n then add_toc_entry (Toc_section (lev, f, r))
+ else ());
stop_item ();
printf "<a name=\"%s\"></a><h%d class=\"section\">" lab lev;
f ();
@@ -572,64 +688,70 @@ module Html = struct
(* make a HTML index from a list of triples (name,text,link) *)
let index_ref i c =
let idxc = sprintf "%s_%c" i.idx_name c in
- if !multi_index then "index_" ^ idxc ^ ".html" else "index.html#" ^ idxc
+ !index_name ^ (if !multi_index then "_" ^ idxc ^ ".html" else ".html#" ^ idxc)
let letter_index category idx (c,l) =
if l <> [] then begin
let cat = if category && idx <> "global" then "(" ^ idx ^ ")" else "" in
- printf "<a name=\"%s_%c\"></a><h2>%c %s</h2>\n" idx c c cat;
- List.iter
- (fun (id,(text,link)) ->
- printf "<a href=\"%s\">%s</a> %s<br/>\n" link id text) l;
+ printf "<a name=\"%s_%c\"></a><h2>%s %s</h2>\n" idx c (display_letter c) cat;
+ List.iter
+ (fun (id,(text,link,t)) ->
+ let id' = prepare_entry id t in
+ printf "<a href=\"%s\">%s</a> %s<br/>\n" link id' text) l;
printf "<br/><br/>"
end
-
+
let all_letters i = List.iter (letter_index false i.idx_name) i.idx_entries
(* Construction d'une liste des index (1 index global, puis 1
index par catégorie) *)
let format_global_index =
- Index.map
- (fun s (m,t) ->
- if t = Library then
- "[library]", m ^ ".html"
- else
- sprintf "[%s, in <a href=\"%s.html\">%s</a>]" (type_name t) m m ,
- sprintf "%s.html#%s" m s)
+ Index.map
+ (fun s (m,t) ->
+ if t = Library then
+ let ln = !lib_name in
+ if ln <> "" then
+ "[" ^ String.lowercase ln ^ "]", m ^ ".html", t
+ else
+ "[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)
let format_bytype_index = function
| Library, idx ->
- Index.map (fun id m -> "", m ^ ".html") idx
+ Index.map (fun id m -> "", m ^ ".html", Library) idx
| (t,idx) ->
- Index.map
- (fun s m ->
+ Index.map
+ (fun s m ->
let text = sprintf "[in <a href=\"%s.html\">%s</a>]" m m in
- (text, sprintf "%s.html#%s" m s)) idx
+ (text, sprintf "%s.html#%s" m s, t)) idx
(* Impression de la table d'index *)
let print_index_table_item i =
printf "<tr>\n<td>%s Index</td>\n" (String.capitalize i.idx_name);
- List.iter
- (fun (c,l) ->
+ List.iter
+ (fun (c,l) ->
if l <> [] then
- printf "<td><a href=\"%s\">%c</a></td>\n" (index_ref i c) c
+ printf "<td><a href=\"%s\">%s</a></td>\n" (index_ref i c)
+ (display_letter c)
else
- printf "<td>%c</td>\n" c)
+ printf "<td>%s</td>\n" (display_letter c))
i.idx_entries;
let n = i.idx_size in
printf "<td>(%d %s)</td>\n" n (if n > 1 then "entries" else "entry");
printf "</tr>\n"
- let print_index_table idxl =
+ let print_index_table idxl =
printf "<table>\n";
List.iter print_index_table_item idxl;
printf "</table>\n"
-
+
let make_one_multi_index prt_tbl i =
- (* Attn: make_one_multi_index créé un nouveau fichier... *)
+ (* Attn: make_one_multi_index crée 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);
+ open_out_file (sprintf "%s_%s_%c.html" !index_name idx c);
if (!header_trailer) then header ();
prt_tbl (); printf "<hr/>";
letter_index true idx cl;
@@ -639,16 +761,16 @@ module Html = struct
in
List.iter one_letter i.idx_entries
- let make_multi_index () =
- let all_index =
+ let make_multi_index () =
+ let all_index =
let glob,bt = Index.all_entries () in
(format_global_index glob) ::
(List.map format_bytype_index bt) in
let print_table () = print_index_table all_index in
List.iter (make_one_multi_index print_table) all_index
-
+
let make_index () =
- let all_index =
+ let all_index =
let glob,bt = Index.all_entries () in
(format_global_index glob) ::
(List.map format_bytype_index bt) in
@@ -659,26 +781,33 @@ module Html = struct
all_letters i
end
in
- current_module := "Index";
+ set_module "Index" None;
if !title <> "" then printf "<h1>%s</h1>\n" !title;
print_table ();
- if not (!multi_index) then
+ if not (!multi_index) then
begin
List.iter print_one_index all_index;
printf "<hr/>"; print_table ()
end
-
- let make_toc () =
- let make_toc_entry = function
- | Toc_library m ->
- stop_item ();
- printf "<a href=\"%s.html\"><h2>Library %s</h2></a>\n" m m
- | Toc_section (n, f, r) ->
- item n;
- printf "<a href=\"%s\">" r; f (); printf "</a>\n"
- in
- Queue.iter make_toc_entry toc_q;
- stop_item ();
+
+ let make_toc () =
+ let ln = !lib_name in
+ let make_toc_entry = function
+ | Toc_library (m,sub) ->
+ stop_item ();
+ let ms = match sub with | None -> m | Some s -> m ^ ": " ^ s in
+ if ln = "" then
+ printf "<a href=\"%s.html\"><h2>%s</h2></a>\n" m ms
+ else
+ printf "<a href=\"%s.html\"><h2>%s %s</h2></a>\n" m ln ms
+ | Toc_section (n, f, r) ->
+ item n;
+ printf "<a href=\"%s\">" r; f (); printf "</a>\n"
+ in
+ printf "<div id=\"toc\">\n";
+ Queue.iter make_toc_entry toc_q;
+ stop_item ();
+ printf "</div>\n"
end
@@ -689,21 +818,21 @@ module TeXmacs = struct
(*s Latex preamble *)
- let in_doc = ref false
-
- let (preamble : string Queue.t) =
+ let (preamble : string Queue.t) =
in_doc := false; Queue.create ()
let push_in_preamble s = Queue.add s preamble
let header () =
- output_string
+ output_string
"(*i This file has been automatically generated with the command \n";
- output_string
+ output_string
" "; Array.iter (fun s -> printf "%s " s) Sys.argv; printf " *)\n"
let trailer () = ()
+ let nbsp () = output_char ' '
+
let char_true c = match c with
| '\\' -> printf "\\\\"
| '<' -> printf "\\<"
@@ -734,7 +863,7 @@ module TeXmacs = struct
let indentation n = ()
- let ident_true s =
+ let ident_true s =
if is_keyword s then begin
printf "<kw|"; raw_ident s; printf ">"
end else begin
@@ -742,27 +871,20 @@ module TeXmacs = struct
end
let ident s _ = if !in_doc then ident_true s else raw_ident s
-
- let symbol_true s =
- let ensuremath x = printf "<with|mode|math|\\<%s\\>>" x in
- match s with
- | "*" -> ensuremath "times"
- | "->" -> ensuremath "rightarrow"
- | "<-" -> ensuremath "leftarrow"
- | "<->" ->ensuremath "leftrightarrow"
- | "=>" -> ensuremath "Rightarrow"
- | "<=" -> ensuremath "le"
- | ">=" -> ensuremath "ge"
- | "<>" -> ensuremath "noteq"
- | "~" -> ensuremath "lnot"
- | "/\\" -> ensuremath "land"
- | "\\/" -> ensuremath "lor"
- | "|-" -> ensuremath "vdash"
- | s -> raw_ident s
-
- let symbol s = if !in_doc then symbol_true s else raw_ident s
-
- let rec reach_item_level n =
+
+ let output_sublexer_string doescape issymbchar tag s =
+ if doescape then raw_ident s else output_string s
+
+ let sublexer c l =
+ if !in_doc then Tokens.output_tagged_symbol_char None c else char c
+
+ let initialize () =
+ Tokens.token_tree := token_tree_texmacs;
+ Tokens.outfun := output_sublexer_string
+
+ let proofbox () = printf "QED"
+
+ let rec reach_item_level n =
if !item_level < n then begin
printf "\n<\\itemize>\n<item>"; incr item_level;
reach_item_level n
@@ -786,6 +908,9 @@ module TeXmacs = struct
let end_coq () = ()
+ let start_emph () = printf "<with|font shape|italic|"
+ let stop_emph () = printf ">"
+
let start_comment () = ()
let end_comment () = ()
@@ -801,13 +926,13 @@ module TeXmacs = struct
let section lev f =
stop_item ();
- printf "<"; output_string (section_kind lev); printf "|";
+ printf "<"; output_string (section_kind lev); printf "|";
f (); printf ">\n\n"
let rule () =
printf "\n<hrule>\n"
- let paragraph () = stop_item (); printf "\n\n"
+ let paragraph () = printf "\n\n"
let line_break_true () = printf "<format|line break>"
@@ -819,6 +944,10 @@ module TeXmacs = struct
let end_inline_coq () = printf "]>"
+ let start_inline_coq_block () = line_break (); start_inline_coq ()
+
+ let end_inline_coq_block () = end_inline_coq ()
+
let make_multi_index () = ()
let make_index () = ()
@@ -828,7 +957,7 @@ module TeXmacs = struct
end
-(*s LaTeX output *)
+(*s Raw output *)
module Raw = struct
@@ -836,13 +965,9 @@ module Raw = struct
let trailer () = ()
- let char = output_char
+ let nbsp () = output_char ' '
- let label_char c = match c with
- | '\\' | '$' | '#' | '%' | '&' | '{' | '}' | '_'
- | '^' | '~' -> ()
- | _ ->
- output_char c
+ let char = output_char
let latex_char = output_char
let latex_string = output_string
@@ -863,22 +988,31 @@ module Raw = struct
let stop_verbatim () = ()
- let indentation n =
+ let indentation n =
for i = 1 to n do printf " " done
let ident s loc = raw_ident s
- let symbol s = raw_ident s
+ let sublexer c l = char c
- let item n = printf "- "
+ let initialize () =
+ Tokens.token_tree := ref Tokens.empty_ttree;
+ Tokens.outfun := (fun _ _ _ _ -> failwith "Useless")
+
+ let proofbox () = printf "[]"
+ let item n = printf "- "
let stop_item () = ()
+ let reach_item_level _ = ()
let start_doc () = printf "(** "
let end_doc () = printf " *)\n"
- let start_comment () = ()
- let end_comment () = ()
+ let start_emph () = printf "_"
+ let stop_emph () = printf "_"
+
+ let start_comment () = printf "(*"
+ let end_comment () = printf "*)"
let start_coq () = ()
let end_coq () = ()
@@ -886,15 +1020,15 @@ module Raw = struct
let start_code () = end_doc (); start_coq ()
let end_code () = end_coq (); start_doc ()
- let section_kind =
+ let section_kind =
function
- | 1 -> "*"
- | 2 -> "**"
- | 3 -> "***"
- | 4 -> "****"
- | _ -> assert false
+ | 1 -> "* "
+ | 2 -> "** "
+ | 3 -> "*** "
+ | 4 -> "**** "
+ | _ -> assert false
- let section lev f =
+ let section lev f =
output_string (section_kind lev);
f ()
@@ -909,9 +1043,12 @@ module Raw = struct
let start_inline_coq () = ()
let end_inline_coq () = ()
+ let start_inline_coq_block () = line_break (); start_inline_coq ()
+ let end_inline_coq_block () = end_inline_coq ()
+
let make_multi_index () = ()
let make_index () = ()
- let make_toc () = ()
+ let make_toc () = ()
end
@@ -919,7 +1056,7 @@ end
(*s Generic output *)
-let select f1 f2 f3 f4 x =
+let select f1 f2 f3 f4 x =
match !target_language with LaTeX -> f1 x | HTML -> f2 x | TeXmacs -> f3 x | Raw -> f4 x
let push_in_preamble = Latex.push_in_preamble
@@ -927,7 +1064,7 @@ let push_in_preamble = Latex.push_in_preamble
let header = select Latex.header Html.header TeXmacs.header Raw.header
let trailer = select Latex.trailer Html.trailer TeXmacs.trailer Raw.trailer
-let start_module =
+let start_module =
select Latex.start_module Html.start_module TeXmacs.start_module Raw.start_module
let start_doc = select Latex.start_doc Html.start_doc TeXmacs.start_doc Raw.start_doc
@@ -940,45 +1077,61 @@ let start_coq = select Latex.start_coq Html.start_coq TeXmacs.start_coq Raw.star
let end_coq = select Latex.end_coq Html.end_coq TeXmacs.end_coq Raw.end_coq
let start_code = select Latex.start_code Html.start_code TeXmacs.start_code Raw.start_code
-let end_code = select Latex.end_code Html.end_code TeXmacs.end_code Raw.end_code
+let end_code = select Latex.end_code Html.end_code TeXmacs.end_code Raw.end_code
-let start_inline_coq =
+let start_inline_coq =
select Latex.start_inline_coq Html.start_inline_coq TeXmacs.start_inline_coq Raw.start_inline_coq
-let end_inline_coq =
+let end_inline_coq =
select Latex.end_inline_coq Html.end_inline_coq TeXmacs.end_inline_coq Raw.end_inline_coq
+let start_inline_coq_block =
+ select Latex.start_inline_coq_block Html.start_inline_coq_block
+ TeXmacs.start_inline_coq_block Raw.start_inline_coq_block
+let end_inline_coq_block =
+ select Latex.end_inline_coq_block Html.end_inline_coq_block TeXmacs.end_inline_coq_block Raw.end_inline_coq_block
+
let indentation = select Latex.indentation Html.indentation TeXmacs.indentation Raw.indentation
let paragraph = select Latex.paragraph Html.paragraph TeXmacs.paragraph Raw.paragraph
let line_break = select Latex.line_break Html.line_break TeXmacs.line_break Raw.line_break
-let empty_line_of_code = select
+let empty_line_of_code = select
Latex.empty_line_of_code Html.empty_line_of_code TeXmacs.empty_line_of_code Raw.empty_line_of_code
let section = select Latex.section Html.section TeXmacs.section Raw.section
let item = select Latex.item Html.item TeXmacs.item Raw.item
let stop_item = select Latex.stop_item Html.stop_item TeXmacs.stop_item Raw.stop_item
+let reach_item_level = select Latex.reach_item_level Html.reach_item_level TeXmacs.reach_item_level Raw.reach_item_level
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 ident = select Latex.ident Html.ident TeXmacs.ident Raw.ident
-let symbol = select Latex.symbol Html.symbol TeXmacs.symbol Raw.symbol
+let sublexer = select Latex.sublexer Html.sublexer TeXmacs.sublexer Raw.sublexer
+let initialize = select Latex.initialize Html.initialize TeXmacs.initialize Raw.initialize
+
+let proofbox = select Latex.proofbox Html.proofbox TeXmacs.proofbox Raw.proofbox
let latex_char = select Latex.latex_char Html.latex_char TeXmacs.latex_char Raw.latex_char
-let latex_string =
+let latex_string =
select Latex.latex_string Html.latex_string TeXmacs.latex_string Raw.latex_string
let html_char = select Latex.html_char Html.html_char TeXmacs.html_char Raw.html_char
-let html_string =
+let html_string =
select Latex.html_string Html.html_string TeXmacs.html_string Raw.html_string
-let start_latex_math =
+let start_emph =
+ select Latex.start_emph Html.start_emph TeXmacs.start_emph Raw.start_emph
+let stop_emph =
+ select Latex.stop_emph Html.stop_emph TeXmacs.stop_emph Raw.stop_emph
+
+let start_latex_math =
select Latex.start_latex_math Html.start_latex_math TeXmacs.start_latex_math Raw.start_latex_math
-let stop_latex_math =
+let stop_latex_math =
select Latex.stop_latex_math Html.stop_latex_math TeXmacs.stop_latex_math Raw.stop_latex_math
-let start_verbatim =
+let start_verbatim =
select Latex.start_verbatim Html.start_verbatim TeXmacs.start_verbatim Raw.start_verbatim
-let stop_verbatim =
+let stop_verbatim =
select Latex.stop_verbatim Html.stop_verbatim TeXmacs.stop_verbatim Raw.stop_verbatim
-let verbatim_char =
+let verbatim_char =
select output_char Html.char TeXmacs.char Raw.char
let hard_verbatim_char = output_char
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index 75c7ccf8..d836f6b3 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: output.mli 12187 2009-06-13 19:36:59Z msozeau $ i*)
+(*i $Id$ i*)
open Cdglobals
open Index
@@ -16,7 +16,8 @@ val initialize : unit -> unit
val add_printing_token : string -> string option * string option -> unit
val remove_printing_token : string -> unit
-val set_module : coq_module -> unit
+val set_module : coq_module -> string option -> unit
+val get_module : bool -> string
val header : unit -> unit
val trailer : unit -> unit
@@ -28,6 +29,9 @@ val start_module : unit -> unit
val start_doc : unit -> unit
val end_doc : unit -> unit
+val start_emph : unit -> unit
+val stop_emph : unit -> unit
+
val start_comment : unit -> unit
val end_comment : unit -> unit
@@ -40,6 +44,9 @@ val end_code : unit -> unit
val start_inline_coq : unit -> unit
val end_inline_coq : unit -> unit
+val start_inline_coq_block : unit -> unit
+val end_inline_coq_block : unit -> unit
+
val indentation : int -> unit
val line_break : unit -> unit
val paragraph : unit -> unit
@@ -48,12 +55,18 @@ val empty_line_of_code : unit -> unit
val section : int -> (unit -> unit) -> unit
val item : int -> unit
+val stop_item : unit -> unit
+val reach_item_level : int -> unit
val rule : unit -> unit
+val nbsp : unit -> unit
val char : char -> unit
val ident : string -> loc -> unit
-val symbol : string -> unit
+val sublexer : char -> loc -> unit
+val initialize : unit -> unit
+
+val proofbox : unit -> unit
val latex_char : char -> unit
val latex_string : string -> unit
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
deleted file mode 100644
index b29e0734..00000000
--- a/tools/coqdoc/pretty.mll
+++ /dev/null
@@ -1,784 +0,0 @@
-(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(*i $Id: pretty.mll 12908 2010-04-09 08:54:04Z herbelin $ i*)
-
-(*s Utility functions for the scanners *)
-
-{
- open Printf
- open Lexing
-
- (* count the number of spaces at the beginning of a string *)
- let count_spaces s =
- let n = String.length s in
- let rec count c i =
- if i == n then c,i else match s.[i] with
- | '\t' -> count (c + (8 - (c mod 8))) (i + 1)
- | ' ' -> count (c + 1) (i + 1)
- | _ -> c,i
- in
- count 0 0
-
- let count_dashes s =
- let c = ref 0 in
- for i = 0 to String.length s - 1 do if s.[i] = '-' then incr c done;
- !c
-
- let cut_head_tail_spaces s =
- let n = String.length s in
- let rec look_up i = if i == n || s.[i] <> ' ' then i else look_up (i+1) in
- let rec look_dn i = if i == -1 || s.[i] <> ' ' then i else look_dn (i-1) in
- let l = look_up 0 in
- let r = look_dn (n-1) in
- if l <= r then String.sub s l (r-l+1) else s
-
- let sec_title s =
- let rec count lev i =
- if s.[i] = '*' then
- count (succ lev) (succ i)
- else
- let t = String.sub s i (String.length s - i) in
- lev, cut_head_tail_spaces t
- in
- count 0 (String.index s '*')
-
- let strip_eol s =
- let eol = s.[String.length s - 1] = '\n' in
- (eol, if eol then String.sub s 1 (String.length s - 1) else s)
-
-
- let formatted = ref false
- let brackets = ref 0
- let comment_level = ref 0
- let in_proof = ref None
-
- let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos
-
- let is_space = function ' ' | '\t' | '\n' | '\r' -> true | _ -> false
-
- (* saving/restoring the PP state *)
-
- type state = {
- st_gallina : bool;
- st_light : bool
- }
-
- let state_stack = Stack.create ()
-
- let save_state () =
- Stack.push { st_gallina = !Cdglobals.gallina; st_light = !Cdglobals.light } state_stack
-
- let restore_state () =
- let s = Stack.pop state_stack in
- Cdglobals.gallina := s.st_gallina;
- Cdglobals.light := s.st_light
-
- let without_ref r f x = save_state (); r := false; f x; restore_state ()
-
- let without_gallina = without_ref Cdglobals.gallina
-
- let without_light = without_ref Cdglobals.light
-
- let show_all f = without_gallina (without_light f)
-
- let begin_show () = save_state (); Cdglobals.gallina := false; Cdglobals.light := false
- let end_show () = restore_state ()
-
- (* Reset the globals *)
-
- let reset () =
- formatted := false;
- brackets := 0;
- comment_level := 0
-
- (* erasing of Section/End *)
-
- let section_re = Str.regexp "[ \t]*Section"
- let end_re = Str.regexp "[ \t]*End"
- let is_section s = Str.string_match section_re s 0
- let is_end s = Str.string_match end_re s 0
-
- let sections_to_close = ref 0
-
- let section_or_end s =
- if is_section s then begin
- incr sections_to_close; true
- end else if is_end s then begin
- if !sections_to_close > 0 then begin
- decr sections_to_close; true
- end else
- false
- end else
- true
-
- (* tokens pretty-print *)
-
- let token_buffer = Buffer.create 1024
-
- let token_re =
- Str.regexp "[ \t]*(\\*\\*[ \t]+printing[ \t]+\\([^ \t]+\\)"
- let printing_token_re =
- Str.regexp
- "[ \t]*\\(\\(%\\([^%]*\\)%\\)\\|\\(\\$[^$]*\\$\\)\\)?[ \t]*\\(#\\(\\(&#\\|[^#]\\)*\\)#\\)?"
-
- let add_printing_token toks pps =
- try
- if Str.string_match token_re toks 0 then
- let tok = Str.matched_group 1 toks in
- if Str.string_match printing_token_re pps 0 then
- let pp =
- (try Some (Str.matched_group 3 pps) with _ ->
- try Some (Str.matched_group 4 pps) with _ -> None),
- (try Some (Str.matched_group 6 pps) with _ -> None)
- in
- Output.add_printing_token tok pp
- with _ ->
- ()
-
- let remove_token_re =
- Str.regexp
- "[ \t]*(\\*\\*[ \t]+remove[ \t]+printing[ \t]+\\([^ \t]+\\)[ \t]*\\*)"
-
- let remove_printing_token toks =
- try
- if Str.string_match remove_token_re toks 0 then
- let tok = Str.matched_group 1 toks in
- Output.remove_printing_token tok
- with _ ->
- ()
-
- let extract_ident_re = Str.regexp "([ \t]*\\([^ \t]+\\)[ \t]*:="
- let extract_ident s =
- assert (String.length s >= 3);
- if Str.string_match extract_ident_re s 0 then
- Str.matched_group 1 s
- else
- String.sub s 1 (String.length s - 3)
-
- let symbol lexbuf s = Output.symbol s
-
-}
-
-(*s Regular expressions *)
-
-let space = [' ' '\t']
-let space_nl = [' ' '\t' '\n' '\r']
-let nl = "\r\n" | '\n'
-
-let firstchar =
- ['A'-'Z' 'a'-'z' '_'
- (* iso 8859-1 accents *)
- '\192'-'\214' '\216'-'\246' '\248'-'\255' ] |
- (* *)
- '\194' '\185' |
- (* utf-8 latin 1 supplement *)
- '\195' ['\128'-'\191'] |
- (* utf-8 letterlike symbols *)
- '\206' ('\160' | [ '\177'-'\183'] | '\187') |
- '\226' ('\130' [ '\128'-'\137' ] (* subscripts *)
- | '\129' [ '\176'-'\187' ] (* superscripts *)
- | '\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])
-let identchar =
- firstchar | ['\'' '0'-'9' '@' ]
-let id = firstchar identchar*
-let pfx_id = (id '.')*
-let identifier =
- id | pfx_id id
-
-let symbolchar_symbol_no_brackets =
- ['!' '$' '%' '&' '*' '+' ',' '^' '#'
- '\\' '/' '-' '<' '>' '|' ':' '?' '=' '~' ] |
- (* utf-8 symbols *)
- '\226' ['\134'-'\143' '\152'-'\155' '\164'-'\165' '\168'-'\171'] _
-let symbolchar_no_brackets = symbolchar_symbol_no_brackets |
- [ '@' '{' '}' '(' ')' 'A'-'Z' 'a'-'z' '_']
-let symbolchar = symbolchar_no_brackets | '[' | ']'
-let token_no_brackets = symbolchar_symbol_no_brackets symbolchar_no_brackets*
-let token = symbolchar_symbol_no_brackets symbolchar* | '[' [^ '[' ']' ':']* ']'
-let printing_token = (token | id)+
-
-(* tokens with balanced brackets *)
-let token_brackets =
- ( token_no_brackets ('[' token_no_brackets? ']')*
- | token_no_brackets? ('[' token_no_brackets? ']')+ )
- token_no_brackets?
-
-let thm_token =
- "Theorem"
- | "Lemma"
- | "Fact"
- | "Remark"
- | "Corollary"
- | "Proposition"
- | "Property"
- | "Goal"
-
-let prf_token =
- "Next" space+ "Obligation"
- | "Proof" (space* "." | space+ "with")
-
-let def_token =
- "Definition"
- | "Let"
- | "Class"
- | "SubClass"
- | "Example"
- | "Local"
- | "Fixpoint"
- | "Boxed"
- | "CoFixpoint"
- | "Record"
- | "Structure"
- | "Scheme"
- | "Inductive"
- | "CoInductive"
- | "Equations"
- | "Instance"
- | "Global" space+ "Instance"
-
-let decl_token =
- "Hypothesis"
- | "Hypotheses"
- | "Parameter"
- | "Axiom" 's'?
- | "Conjecture"
-
-let gallina_ext =
- "Module"
- | "Include" space+ "Type"
- | "Include"
- | "Declare" space+ "Module"
- | "Transparent"
- | "Opaque"
- | "Canonical"
- | "Coercion"
- | "Identity"
- | "Implicit"
- | "Notation"
- | "Infix"
- | "Tactic" space+ "Notation"
- | "Reserved" space+ "Notation"
- | "Section"
- | "Context"
- | "Variable" 's'?
- | ("Hypothesis" | "Hypotheses")
- | "End"
-
-let commands =
- "Pwd"
- | "Cd"
- | "Drop"
- | "ProtectedLoop"
- | "Quit"
- | "Load"
- | "Add"
- | "Remove" space+ "Loadpath"
- | "Print"
- | "Inspect"
- | "About"
- | "Search"
- | "Eval"
- | "Reset"
- | "Check"
- | "Type"
-
- | "Section"
- | "Chapter"
- | "Variable" 's'?
- | ("Hypothesis" | "Hypotheses")
- | "End"
-
-let end_kw = "Qed" | "Defined" | "Save" | "Admitted" | "Abort"
-
-let extraction =
- "Extraction"
- | "Recursive" space+ "Extraction"
- | "Extract"
-
-let gallina_kw = thm_token | def_token | decl_token | gallina_ext | commands | extraction
-
-let prog_kw =
- "Program" space+ gallina_kw
- | "Obligation"
- | "Obligations"
- | "Solve"
-
-let gallina_kw_to_hide =
- "Implicit" space+ "Arguments"
- | "Ltac"
- | "Require"
- | "Import"
- | "Export"
- | "Load"
- | "Hint"
- | "Open"
- | "Close"
- | "Delimit"
- | "Transparent"
- | "Opaque"
- | ("Declare" space+ ("Morphism" | "Step") )
- | ("Set" | "Unset") space+ "Printing" space+ "Coercions"
- | "Declare" space+ ("Left" | "Right") space+ "Step"
-
-
-let section = "*" | "**" | "***" | "****"
-
-let item_space = " "
-
-let begin_hide = "(*" space* "begin" space+ "hide" space* "*)" space* nl
-let end_hide = "(*" space* "end" space+ "hide" space* "*)" space* nl
-let begin_show = "(*" space* "begin" space+ "show" space* "*)" space* nl
-let end_show = "(*" space* "end" space+ "show" space* "*)" space* nl
-(*
-let begin_verb = "(*" space* "begin" space+ "verb" space* "*)"
-let end_verb = "(*" space* "end" space+ "verb" space* "*)"
-*)
-
-
-
-(*s Scanning Coq, at beginning of line *)
-
-rule coq_bol = parse
- | space* nl+
- { if not (!in_proof <> None && (!Cdglobals.gallina || !Cdglobals.light)) then Output.empty_line_of_code (); coq_bol lexbuf }
- | space* "(**" space_nl
- { Output.end_coq (); Output.start_doc ();
- let eol = doc_bol lexbuf in
- Output.end_doc (); Output.start_coq ();
- if eol then coq_bol lexbuf else coq lexbuf }
- | space* "Comments" space_nl
- { Output.end_coq (); Output.start_doc (); comments lexbuf; Output.end_doc ();
- Output.start_coq (); coq lexbuf }
- | space* begin_hide
- { skip_hide lexbuf; coq_bol lexbuf }
- | space* begin_show
- { begin_show (); coq_bol lexbuf }
- | space* end_show
- { end_show (); coq_bol lexbuf }
- | space* gallina_kw_to_hide
- { let s = lexeme lexbuf in
- if !Cdglobals.light && section_or_end s then
- let eol = skip_to_dot lexbuf in
- if eol then (coq_bol lexbuf) else coq lexbuf
- else
- begin
- 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);
- 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 := Some eol;
- if eol then coq_bol lexbuf else coq lexbuf }
- | space* prf_token
- { in_proof := Some true;
- let eol =
- if not !Cdglobals.gallina then
- begin backtrack lexbuf; body_bol lexbuf end
- else
- let s = lexeme lexbuf in
- if s.[String.length s - 1] = '.' then false
- else skip_to_dot lexbuf
- in if eol then coq_bol lexbuf else coq lexbuf }
- | space* end_kw {
- let eol =
- if not (!in_proof <> None && !Cdglobals.gallina) then
- begin backtrack lexbuf; body_bol lexbuf end
- else skip_to_dot lexbuf
- in
- in_proof := None;
- if eol then coq_bol lexbuf else coq lexbuf }
- | space* gallina_kw
- {
- in_proof := None;
- let s = lexeme lexbuf in
- let 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
- if eol then coq_bol lexbuf else coq lexbuf }
- | space* prog_kw
- {
- in_proof := None;
- let s = lexeme lexbuf in
- let nbsp,isp = count_spaces s in
- Output.indentation nbsp;
- let s = String.sub s isp (String.length s - isp) in
- Output.ident s (lexeme_start lexbuf + isp);
- let eol= body lexbuf in
- if eol then coq_bol lexbuf else coq lexbuf }
-
- | space* "(**" space+ "printing" space+ printing_token space+
- { let tok = lexeme lexbuf in
- let s = printing_token_body lexbuf in
- add_printing_token tok s;
- coq_bol lexbuf }
- | space* "(**" space+ "printing" space+
- { eprintf "warning: bad 'printing' command at character %d\n"
- (lexeme_start lexbuf); flush stderr;
- comment_level := 1;
- ignore (comment lexbuf);
- coq_bol lexbuf }
- | space* "(**" space+ "remove" space+ "printing" space+
- (identifier | token) space* "*)"
- { remove_printing_token (lexeme lexbuf);
- coq_bol lexbuf }
- | space* "(**" space+ "remove" space+ "printing" space+
- { eprintf "warning: bad 'remove printing' command at character %d\n"
- (lexeme_start lexbuf); flush stderr;
- comment_level := 1;
- ignore (comment lexbuf);
- coq_bol lexbuf }
- | space* "(*"
- { comment_level := 1;
- if !Cdglobals.parse_comments then begin
- let s = lexeme lexbuf in
- let nbsp,isp = count_spaces s in
- Output.indentation nbsp;
- Output.start_comment ();
- end;
- let eol = comment lexbuf in
- if eol then coq_bol lexbuf else coq lexbuf }
- | eof
- { () }
- | _
- { let eol =
- if not !Cdglobals.gallina then
- begin backtrack lexbuf; body_bol lexbuf end
- else
- skip_to_dot lexbuf
- in
- if eol then coq_bol lexbuf else coq lexbuf }
-
-(*s Scanning Coq elsewhere *)
-
-and coq = parse
- | nl
- { if not (!in_proof <> None && !Cdglobals.gallina) then Output.line_break(); coq_bol lexbuf }
- | "(**" space_nl
- { Output.end_coq (); Output.start_doc ();
- let eol = doc_bol lexbuf in
- Output.end_doc (); Output.start_coq ();
- if eol then coq_bol lexbuf else coq lexbuf }
- | "(*"
- { comment_level := 1;
- if !Cdglobals.parse_comments then begin
- let s = lexeme lexbuf in
- let nbsp,isp = count_spaces s in
- Output.indentation nbsp;
- Output.start_comment ();
- end;
- let eol = comment lexbuf in
- if eol then coq_bol lexbuf
- else coq lexbuf
- }
- | nl+ space* "]]"
- { if not !formatted then begin symbol lexbuf (lexeme lexbuf); coq lexbuf end }
- | eof
- { () }
- | gallina_kw_to_hide
- { let s = lexeme lexbuf in
- if !Cdglobals.light && section_or_end s then
- begin
- let eol = skip_to_dot lexbuf in
- if eol then coq_bol lexbuf else coq lexbuf
- end
- else
- begin
- Output.ident s (lexeme_start lexbuf);
- let eol=body lexbuf in
- if eol then coq_bol lexbuf else coq lexbuf
- end }
- | prf_token
- { let eol =
- if not !Cdglobals.gallina then
- begin backtrack lexbuf; body_bol lexbuf end
- else
- let s = lexeme lexbuf in
- let eol =
- if s.[String.length s - 1] = '.' then false
- else skip_to_dot lexbuf
- in
- eol
- in if eol then coq_bol lexbuf else coq lexbuf }
- | end_kw {
- let eol =
- if not !Cdglobals.gallina then
- begin backtrack lexbuf; body lexbuf end
- else
- let eol = skip_to_dot lexbuf in
- if !in_proof <> Some true && eol then
- Output.line_break ();
- eol
- in
- in_proof := None;
- if eol then coq_bol lexbuf else coq lexbuf }
- | gallina_kw
- { let s = lexeme lexbuf in
- Output.ident s (lexeme_start lexbuf);
- let eol = body lexbuf in
- if eol then coq_bol lexbuf else coq lexbuf }
- | prog_kw
- { let s = lexeme lexbuf in
- Output.ident s (lexeme_start lexbuf);
- let eol = body lexbuf in
- if eol then coq_bol lexbuf else coq lexbuf }
- | space+ { Output.char ' '; coq lexbuf }
- | eof
- { () }
- | _ { let eol =
- if not !Cdglobals.gallina then
- begin backtrack lexbuf; body lexbuf end
- else
- skip_to_dot lexbuf
- in
- if eol then coq_bol lexbuf else coq lexbuf}
-
-(*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
- Output.section lev (fun () -> ignore (doc (from_string s)));
- if eol then doc_bol lexbuf else doc lexbuf }
- | space* '-'+
- { let n = count_dashes (lexeme lexbuf) in
- if n >= 4 then Output.rule () else Output.item n;
- doc lexbuf }
- | "<<" space*
- { Output.start_verbatim (); verbatim lexbuf; doc_bol lexbuf }
- | eof
- { true }
- | _
- { backtrack lexbuf; doc lexbuf }
-
-(*s Scanning documentation elsewhere *)
-
-and doc = parse
- | nl
- { Output.char '\n'; doc_bol lexbuf }
- | "[[" nl
- { formatted := true; Output.line_break (); Output.start_inline_coq ();
- let eol = body_bol lexbuf in
- Output.end_inline_coq (); formatted := false;
- if eol then doc_bol lexbuf else doc lexbuf}
- | "["
- { brackets := 1;
- Output.start_inline_coq (); escaped_coq lexbuf; Output.end_inline_coq ();
- doc lexbuf }
- | '*'* "*)" space* nl
- { true }
- | '*'* "*)"
- { false }
- | "$"
- { Output.start_latex_math (); escaped_math_latex lexbuf; doc lexbuf }
- | "$$"
- { Output.char '$'; doc lexbuf }
- | "%"
- { escaped_latex lexbuf; doc lexbuf }
- | "%%"
- { Output.char '%'; doc lexbuf }
- | "#"
- { escaped_html lexbuf; doc lexbuf }
- | "##"
- { Output.char '#'; doc lexbuf }
- | eof
- { false }
- | _
- { Output.char (lexeme_char lexbuf 0); doc lexbuf }
-
-(*s Various escapings *)
-
-and escaped_math_latex = parse
- | "$" { Output.stop_latex_math () }
- | eof { Output.stop_latex_math () }
- | _ { Output.latex_char (lexeme_char lexbuf 0); escaped_math_latex lexbuf }
-
-and escaped_latex = parse
- | "%" { () }
- | eof { () }
- | _ { Output.latex_char (lexeme_char lexbuf 0); escaped_latex lexbuf }
-
-and escaped_html = parse
- | "#" { () }
- | "&#"
- { Output.html_char '&'; Output.html_char '#'; escaped_html lexbuf }
- | "##"
- { Output.html_char '#'; escaped_html lexbuf }
- | eof { () }
- | _ { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf }
-
-and verbatim = parse
- | nl ">>" { Output.verbatim_char '\n'; Output.stop_verbatim () }
- | eof { Output.stop_verbatim () }
- | _ { Output.verbatim_char (lexeme_char lexbuf 0); verbatim lexbuf }
-
-(*s Coq, inside quotations *)
-
-and escaped_coq = parse
- | "]"
- { decr brackets;
- if !brackets > 0 then begin Output.char ']'; escaped_coq lexbuf end }
- | "["
- { incr brackets; Output.char '['; escaped_coq lexbuf }
- | "(*"
- { comment_level := 1; ignore (comment lexbuf); escaped_coq lexbuf }
- | "*)"
- { (* likely to be a syntax error: we escape *) backtrack lexbuf }
- | eof
- { () }
- | token_brackets
- { let s = lexeme lexbuf in
- symbol lexbuf s; escaped_coq lexbuf }
- | (identifier '.')* identifier
- { Output.ident (lexeme lexbuf) (lexeme_start lexbuf); escaped_coq lexbuf }
- | _
- { Output.char (lexeme_char lexbuf 0); escaped_coq lexbuf }
-
-(*s Coq "Comments" command. *)
-
-and comments = parse
- | space_nl+
- { Output.char ' '; comments lexbuf }
- | '"' [^ '"']* '"'
- { let s = lexeme lexbuf in
- let s = String.sub s 1 (String.length s - 2) in
- ignore (doc (from_string s)); comments lexbuf }
- | ([^ '.' '"'] | '.' [^ ' ' '\t' '\n'])+
- { escaped_coq (from_string (lexeme lexbuf)); comments lexbuf }
- | "." (space_nl | eof)
- { () }
- | eof
- { () }
- | _
- { Output.char (lexeme_char lexbuf 0); comments lexbuf }
-
-(*s Skip comments *)
-
-and comment = parse
- | "(*" { incr comment_level;
- if !Cdglobals.parse_comments then Output.start_comment ();
- comment lexbuf }
- | "*)" space* nl {
- if !Cdglobals.parse_comments then (Output.end_comment (); Output.line_break ());
- decr comment_level; if !comment_level > 0 then comment lexbuf else true }
- | "*)" {
- if !Cdglobals.parse_comments then (Output.end_comment ());
- decr comment_level; if !comment_level > 0 then comment lexbuf else false }
- | "[" {
- if !Cdglobals.parse_comments then (
- brackets := 1;
- Output.start_inline_coq (); escaped_coq lexbuf; Output.end_inline_coq ());
- comment lexbuf }
- | eof { false }
- | space+ { if !Cdglobals.parse_comments then
- Output.indentation (fst (count_spaces (lexeme lexbuf))); comment lexbuf }
- | nl { if !Cdglobals.parse_comments then Output.line_break (); comment lexbuf }
- | _ { if !Cdglobals.parse_comments then Output.char (lexeme_char lexbuf 0);
- comment lexbuf }
-
-and skip_to_dot = parse
- | '.' space* nl { true }
- | eof | '.' space+ { false }
- | "(*" { comment_level := 1; ignore (comment lexbuf); skip_to_dot lexbuf }
- | _ { skip_to_dot lexbuf }
-
-and body_bol = parse
- | space+
- { Output.indentation (fst (count_spaces (lexeme lexbuf))); body lexbuf }
- | _ { backtrack lexbuf; Output.indentation 0; body lexbuf }
-
-and body = parse
- | nl {Output.line_break(); body_bol lexbuf}
- | nl+ space* "]]"
- { if not !formatted then begin symbol lexbuf (lexeme lexbuf); body lexbuf end else true }
- | eof { false }
- | '.' space* nl | '.' space* eof
- { Output.char '.'; Output.line_break();
- if not !formatted then true else body_bol lexbuf }
- | '.' space+ { Output.char '.'; Output.char ' ';
- if not !formatted then false else body lexbuf }
- | '"' { Output.char '"'; ignore(notation lexbuf); body lexbuf }
- | "(*" { comment_level := 1;
- if !Cdglobals.parse_comments then Output.start_comment ();
- let eol = comment lexbuf in
- if eol
- then begin if not !Cdglobals.parse_comments then Output.line_break(); body_bol lexbuf end
- else body lexbuf }
- | identifier
- { let s = lexeme lexbuf in
- Output.ident s (lexeme_start lexbuf);
- body lexbuf }
- | token_no_brackets
- { let s = lexeme lexbuf in
- symbol lexbuf s; body lexbuf }
- | ".."
- { Output.char '.'; Output.char '.';
- body lexbuf }
- | _ { let c = lexeme_char lexbuf 0 in
- Output.char c;
- body lexbuf }
-
-and notation_bol = parse
- | space+
- { Output.indentation (fst (count_spaces (lexeme lexbuf))); notation lexbuf }
- | _ { backtrack lexbuf; notation lexbuf }
-
-and notation = parse
- | nl { Output.line_break(); notation_bol lexbuf }
- | '"' { Output.char '"'}
- | token
- { let s = lexeme lexbuf in
- symbol lexbuf s; notation lexbuf }
- | _ { let c = lexeme_char lexbuf 0 in
- Output.char c;
- notation lexbuf }
-
-and skip_hide = parse
- | eof | end_hide { () }
- | _ { skip_hide lexbuf }
-
-(*s Reading token pretty-print *)
-
-and printing_token_body = parse
- | "*)" nl? | eof
- { let s = Buffer.contents token_buffer in
- Buffer.clear token_buffer;
- s }
- | _ { Buffer.add_string token_buffer (lexeme lexbuf);
- printing_token_body lexbuf }
-
-(*s Applying the scanners to files *)
-
-{
-
- let coq_file f m =
- reset ();
- Index.current_library := m;
- Output.start_module ();
- let c = open_in f in
- let lb = from_channel c in
- Output.start_coq (); coq_bol lb; Output.end_coq ();
- close_in c
-
-}
-
diff --git a/tools/coqdoc/tokens.ml b/tools/coqdoc/tokens.ml
new file mode 100644
index 00000000..c2a47308
--- /dev/null
+++ b/tools/coqdoc/tokens.ml
@@ -0,0 +1,171 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* Application of printing rules based on a dictionary specific to the
+ target language *)
+
+open Cdglobals
+
+(*s Dictionaries: trees annotated with string options, each node being a map
+ from chars to dictionaries (the subtrees). A trie, in other words.
+
+ (code copied from parsing/lexer.ml4 for the use of coqdoc, Apr 2010)
+*)
+
+module CharMap = Map.Make (struct type t = char let compare = compare end)
+
+type ttree = {
+ node : string option;
+ branch : ttree CharMap.t }
+
+let empty_ttree = { node = None; branch = CharMap.empty }
+
+let ttree_add ttree str translated =
+ let rec insert tt i =
+ if i == String.length str then
+ {node = Some translated; branch = tt.branch}
+ else
+ let c = str.[i] in
+ let br =
+ match try Some (CharMap.find c tt.branch) with Not_found -> None with
+ | Some tt' ->
+ CharMap.add c (insert tt' (i + 1)) (CharMap.remove c tt.branch)
+ | None ->
+ let tt' = {node = None; branch = CharMap.empty} in
+ CharMap.add c (insert tt' (i + 1)) tt.branch
+ in
+ { node = tt.node; branch = br }
+ in
+ insert ttree 0
+
+(* Removes a string from a dictionary: returns an equal dictionary
+ if the word not present. *)
+let ttree_remove ttree str =
+ let rec remove tt i =
+ if i == String.length str then
+ {node = None; branch = tt.branch}
+ else
+ let c = str.[i] in
+ let br =
+ match try Some (CharMap.find c tt.branch) with Not_found -> None with
+ | Some tt' ->
+ CharMap.add c (remove tt' (i + 1)) (CharMap.remove c tt.branch)
+ | None -> tt.branch
+ in
+ { node = tt.node; branch = br }
+ in
+ remove ttree 0
+
+let ttree_descend ttree c = CharMap.find c ttree.branch
+
+let ttree_find ttree str =
+ let rec proc_rec tt i =
+ if i == String.length str then tt
+ else proc_rec (CharMap.find str.[i] tt.branch) (i+1)
+ in
+ proc_rec ttree 0
+
+(*s Parameters of the translation automaton *)
+
+type out_function = bool -> bool -> Index.index_entry option -> string -> unit
+
+let token_tree = ref (ref empty_ttree)
+let outfun = ref (fun _ _ _ _ -> failwith "outfun not initialized")
+
+(*s Translation automaton *)
+
+let buff = Buffer.create 4
+
+let flush_buffer was_symbolchar tag tok =
+ let hastr = String.length tok <> 0 in
+ if hastr then !outfun false was_symbolchar tag tok;
+ if Buffer.length buff <> 0 then
+ !outfun true (if hastr then not was_symbolchar else was_symbolchar)
+ tag (Buffer.contents buff);
+ Buffer.clear buff
+
+type sublexer_state =
+ | Neutral
+ | Buffering of bool * Index.index_entry option * string * ttree
+
+let translation_state = ref Neutral
+
+let buffer_char is_symbolchar ctag c =
+ let rec aux = function
+ | Neutral ->
+ restart_buffering ()
+ | Buffering (was_symbolchar,tag,translated,tt) ->
+ if tag <> ctag then
+ (* A strong tag comes from Coq; if different Coq tags *)
+ (* hence, we don't try to see the chars as part of a single token *)
+ let translated =
+ match tt.node with
+ | Some tok -> Buffer.clear buff; tok
+ | None -> translated in
+ flush_buffer was_symbolchar tag translated;
+ restart_buffering ()
+ else
+ begin
+ (* If we change the category of characters (symbol vs ident) *)
+ (* we accept this as a possible token cut point and remember the *)
+ (* translated token up to that point *)
+ let translated =
+ if is_symbolchar <> was_symbolchar then
+ match tt.node with
+ | Some tok -> Buffer.clear buff; tok
+ | None -> translated
+ else translated in
+ (* We try to make a significant token from the current *)
+ (* buffer and the new character *)
+ try
+ let tt = ttree_descend tt c in
+ Buffer.add_char buff c;
+ Buffering (is_symbolchar,ctag,translated,tt)
+ with Not_found ->
+ (* No existing translation for the given set of chars *)
+ if is_symbolchar <> was_symbolchar then
+ (* If we changed the category of character read, we accept it *)
+ (* as a possible cut point and restart looking for a translation *)
+ (flush_buffer was_symbolchar tag translated;
+ restart_buffering ())
+ else
+ (* If we did not change the category of character read, we do *)
+ (* not want to cut arbitrarily in the middle of the sequence of *)
+ (* symbol characters or identifier characters *)
+ (Buffer.add_char buff c;
+ Buffering (is_symbolchar,tag,translated,empty_ttree))
+ end
+
+ and restart_buffering () =
+ let tt = try ttree_descend !(!token_tree) c with Not_found -> empty_ttree in
+ Buffer.add_char buff c;
+ Buffering (is_symbolchar,ctag,"",tt)
+
+ in
+ translation_state := aux !translation_state
+
+let output_tagged_ident_string s =
+ for i = 0 to String.length s - 1 do buffer_char false None s.[i] done
+
+let output_tagged_symbol_char tag c =
+ buffer_char true tag c
+
+let flush_sublexer () =
+ match !translation_state with
+ | Neutral -> ()
+ | Buffering (was_symbolchar,tag,translated,tt) ->
+ let translated =
+ match tt.node with
+ | Some tok -> Buffer.clear buff; tok
+ | None -> translated in
+ flush_buffer was_symbolchar tag translated;
+ translation_state := Neutral
+
+(* Translation not using the automaton *)
+let translate s =
+ try (ttree_find !(!token_tree) s).node with Not_found -> None
diff --git a/tools/coqdoc/tokens.mli b/tools/coqdoc/tokens.mli
new file mode 100644
index 00000000..a85e75c4
--- /dev/null
+++ b/tools/coqdoc/tokens.mli
@@ -0,0 +1,78 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* Type of dictionaries *)
+
+type ttree
+
+val empty_ttree : ttree
+
+(* Add a string with some translation in dictionary *)
+val ttree_add : ttree -> string -> string -> ttree
+
+(* Remove a translation from a dictionary: returns an equal dictionary
+ if the word not present *)
+val ttree_remove : ttree -> string -> ttree
+
+(* Translate a string *)
+val translate : string -> string option
+
+(* Sublexer automaton *)
+
+(* The sublexer buffers the chars it receives; if after some time, it
+ recognizes that a sequence of chars has a translation in the
+ current dictionary, it replaces the buffer by the translation *)
+
+(* Received chars can come with a "tag" (usually made from
+ informations from the globalization file). A sequence of chars can
+ be considered a word only, if all chars have the same "tag". Rules
+ for cutting words are the following:
+
+ - in a sequence like "**" where * is in the dictionary but not **,
+ "**" is not translated; otherwise said, to be translated, a sequence
+ must not be surrounded by other symbol-like chars
+
+ - in a sequence like "<>_h*", where <>_h is in the dictionary, the
+ translation is done because the switch from a letter to a symbol char
+ is an acceptable cutting point
+
+ - in a sequence like "<>_ha", where <>_h is in the dictionary, the
+ translation is not done because it is considered that h and a are
+ not separable (however, if h and a have different tags, and h has
+ the same tags as <, > and _, the translation happens)
+
+ - in a sequence like "<>_ha", where <> but not <>_h is in the
+ dictionary, the translation is done for <> and _ha is considered
+ independently because the switch from a symbol char to a letter
+ is considered to be an acceptable cutting point
+
+ - the longest-word rule applies: if both <> and <>_h are in the
+ dictionary, "<>_h" is one word and gets translated
+*)
+
+(* Warning: do not output anything on output channel inbetween a call
+ to [output_tagged_*] and [flush_sublexer]!! *)
+
+type out_function =
+ bool (* needs escape *) ->
+ bool (* it is a symbol, not a pure ident *) ->
+ Index.index_entry option (* the index type of the token if any *) ->
+ string -> unit
+
+(* This must be initialized before calling the sublexer *)
+val token_tree : ttree ref ref
+val outfun : out_function ref
+
+(* Process an ident part that might be a symbol part *)
+val output_tagged_ident_string : string -> unit
+
+(* Process a non-ident char (possibly equipped with a tag) *)
+val output_tagged_symbol_char : Index.index_entry option -> char -> unit
+
+(* Flush the buffered content of the lexer using [outfun] *)
+val flush_sublexer : unit -> unit
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-04 03:14:51 +0000