From a9e3dbd470079b1088bd686344bc54b2d086e3eb Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 5 Nov 2020 12:36:19 +0100 Subject: Reorganizing the printing of warnings; fixing line count. The line count remains fragile though... Any idea to do it automatically? --- tools/coqdoc/cpretty.mll | 115 +++++++++++++++++++++++++++-------------------- 1 file changed, 67 insertions(+), 48 deletions(-) diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 5d210b2e60..d056887591 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -278,8 +278,16 @@ pos_lnum = lcp.pos_lnum + n; pos_bol = lcp.pos_cnum } - let print_position chan p = - Printf.fprintf chan "%s:%d:%d" p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol) + let print_position_p chan p = + Printf.fprintf chan "%s%d, character %d" + (if p.pos_fname = "" then "Line " else "File \"" ^ p.pos_fname ^ "\", line ") + p.pos_lnum (p.pos_cnum - p.pos_bol) + + let print_position chan {lex_start_p = p} = print_position_p chan p + + let warn msg lexbuf = + eprintf "%a, warning: %s\n" print_position lexbuf msg; + flush stderr exception MismatchPreformatted of position @@ -487,29 +495,29 @@ rule coq_bol = parse then Output.empty_line_of_code (); coq_bol lexbuf } | space* "(**" (space_nl as s) - { if is_nl s then Lexing.new_line lexbuf; + { if is_nl s then new_lines 1 lexbuf; 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 as s) - { if is_nl s then Lexing.new_line lexbuf; + { if is_nl s then new_lines 1 lexbuf; Output.end_coq (); Output.start_doc (); comments lexbuf; Output.end_doc (); Output.start_coq (); coq lexbuf } | space* begin_hide nl - { Lexing.new_line lexbuf; skip_hide lexbuf; coq_bol lexbuf } + { new_lines 1 lexbuf; skip_hide lexbuf; coq_bol lexbuf } | space* begin_show nl - { Lexing.new_line lexbuf; begin_show (); coq_bol lexbuf } + { new_lines 1 lexbuf; begin_show (); coq_bol lexbuf } | space* end_show nl - { Lexing.new_line lexbuf; end_show (); coq_bol lexbuf } + { new_lines 1 lexbuf; end_show (); coq_bol lexbuf } | space* begin_details (* At this point, the comment remains open, and will be closed by [details_body] *) { let s = details_body lexbuf in Output.end_coq (); begin_details s; Output.start_coq (); coq_bol lexbuf } | space* end_details nl - { Lexing.new_line lexbuf; + { new_lines 1 lexbuf; Output.end_coq (); end_details (); Output.start_coq (); coq_bol lexbuf } | space* (("Local"|"Global") space+)? gallina_kw_to_hide { let s = lexeme lexbuf in @@ -572,8 +580,7 @@ rule coq_bol = parse 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; + { warn "bad 'printing' command" lexbuf; comment_level := 1; ignore (comment lexbuf); coq_bol lexbuf } @@ -582,8 +589,7 @@ rule coq_bol = parse { 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; + { warn "bad 'remove printing' command" lexbuf; comment_level := 1; ignore (comment lexbuf); coq_bol lexbuf } @@ -616,9 +622,9 @@ rule coq_bol = parse and coq = parse | nl - { Lexing.new_line lexbuf; if not (only_gallina ()) then Output.line_break(); coq_bol lexbuf } + { new_lines 1 lexbuf; if not (only_gallina ()) then Output.line_break(); coq_bol lexbuf } | "(**" (space_nl as s) - { if is_nl s then Lexing.new_line lexbuf; + { if is_nl s then new_lines 1 lexbuf; Output.end_coq (); Output.start_doc (); let eol = doc_bol lexbuf in Output.end_doc (); Output.start_coq (); @@ -719,7 +725,7 @@ and coq = parse and doc_bol = parse | space* section space+ ([^'\n' '\r' '*'] | '*'+ [^'\n' '\r' ')' '*'])* ('*'+ (nl as s))? - { if not (is_none s) then Lexing.new_line lexbuf; + { if not (is_none s) then new_lines 1 lexbuf; let eol, lex = strip_eol (lexeme lexbuf) in let lev, s = sec_title lex in if (!Cdglobals.lib_subtitles) && @@ -731,7 +737,7 @@ and doc_bol = parse | ((space_nl* nl)? as s) (space* '-'+ as line) { let nl_count = count_newlines s in match check_start_list line with - | Neither -> backtrack_past_newline lexbuf; Lexing.new_line lexbuf; doc None lexbuf + | Neither -> backtrack_past_newline lexbuf; new_lines 1 lexbuf; doc None lexbuf | List n -> new_lines nl_count lexbuf; if nl_count > 0 then Output.paragraph (); @@ -770,22 +776,24 @@ and doc_list_bol indents = parse verbatim 0 false lexbuf; doc_list_bol indents lexbuf } | "[[" nl - { formatted := Some lexbuf.lex_start_p; + { new_lines 1 lexbuf; formatted := Some lexbuf.lex_start_p; Output.start_inline_coq_block (); ignore(body_bol lexbuf); Output.end_inline_coq_block (); formatted := None; doc_list_bol indents lexbuf } | "[[[" nl - { inf_rules (Some indents) lexbuf } + { new_lines 1 lexbuf; inf_rules (Some indents) lexbuf } | space* nl space* '-' { (* Like in the doc_bol production, these two productions exist only to deal properly with whitespace *) + new_lines 1 lexbuf; Output.paragraph (); backtrack_past_newline lexbuf; doc_list_bol indents lexbuf } | space* nl space* _ - { let buf' = lexeme lexbuf in + { new_lines 1 lexbuf; + let buf' = lexeme lexbuf in let buf = let bufs = Str.split_delim (Str.regexp "['\n']") buf' in match bufs with @@ -830,12 +838,14 @@ and doc_list_bol indents = parse (*s Scanning documentation elsewhere *) and doc indents = parse | nl - { Output.char '\n'; + { new_lines 1 lexbuf; + Output.char '\n'; match indents with | Some ls -> doc_list_bol ls lexbuf | None -> doc_bol lexbuf } | "[[" nl - { if !Cdglobals.plain_comments + { new_lines 1 lexbuf; + if !Cdglobals.plain_comments then (Output.char '['; Output.char '['; doc indents lexbuf) else (formatted := Some lexbuf.lex_start_p; Output.start_inline_coq_block (); @@ -847,7 +857,7 @@ and doc indents = parse | None -> doc_bol lexbuf else doc indents lexbuf)} | "[[[" nl - { inf_rules indents lexbuf } + { new_lines 1 lexbuf; inf_rules indents lexbuf } | "[]" { Output.proofbox (); doc indents lexbuf } | "{{" { url lexbuf; doc indents lexbuf } @@ -877,7 +887,7 @@ and doc indents = parse doc_bol lexbuf } | '*'* "*)" space* nl - { true } + { new_lines 1 lexbuf; true } | '*'* "*)" { false } | "$" @@ -952,8 +962,8 @@ and escaped_html = parse | _ { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf } and verbatim depth inline = parse - | nl ">>" space* nl { Output.verbatim_char inline '\n'; Output.stop_verbatim inline } - | nl ">>" { Output.verbatim_char inline '\n'; Output.stop_verbatim inline } + | nl ">>" space* nl { new_lines 2 lexbuf; Output.verbatim_char inline '\n'; Output.stop_verbatim inline } + | nl ">>" { new_lines 1 lexbuf; Output.verbatim_char inline '\n'; Output.stop_verbatim inline } | ">>" { Output.stop_verbatim inline } | "(*" { Output.verbatim_char inline '('; Output.verbatim_char inline '*'; @@ -993,7 +1003,8 @@ and escaped_coq = parse else skipped_comment lexbuf); escaped_coq lexbuf } | "*)" - { (* likely to be a syntax error: we escape *) backtrack lexbuf } + { (* likely to be a syntax error *) + warn "unterminated \"]\"" lexbuf; backtrack lexbuf } | eof { Tokens.flush_sublexer () } | identifier @@ -1036,7 +1047,8 @@ and skipped_comment = parse { incr comment_level; skipped_comment lexbuf } | "*)" space* nl - { decr comment_level; + { new_lines 1 lexbuf; + decr comment_level; if !comment_level > 0 then skipped_comment lexbuf else true } | "*)" { decr comment_level; @@ -1050,7 +1062,8 @@ and comment = parse Output.start_comment (); comment lexbuf } | "*)" space* nl - { Output.end_comment (); + { new_lines 1 lexbuf; + Output.end_comment (); Output.line_break (); decr comment_level; if !comment_level > 0 then comment lexbuf else true } @@ -1064,7 +1077,8 @@ and comment = parse escaped_coq lexbuf; Output.end_inline_coq ()); comment lexbuf } | "[[" nl - { if !Cdglobals.plain_comments then (Output.char '['; Output.char '[') + { new_lines 1 lexbuf; + if !Cdglobals.plain_comments then (Output.char '['; Output.char '[') else (formatted := Some lexbuf.lex_start_p; Output.start_inline_coq_block (); let _ = body_bol lexbuf in @@ -1099,13 +1113,14 @@ and comment = parse { Output.indentation (fst (count_spaces (lexeme lexbuf))); comment lexbuf } | nl - { Output.line_break (); + { new_lines 1 lexbuf; + Output.line_break (); comment lexbuf } | _ { Output.char (lexeme_char lexbuf 0); comment lexbuf } and skip_to_dot = parse - | '.' space* nl { true } + | '.' space* nl { new_lines 1 lexbuf; true } | eof | '.' space+ { false } | "(*" { comment_level := 1; @@ -1114,14 +1129,14 @@ and skip_to_dot = parse | _ { skip_to_dot lexbuf } and skip_to_dot_or_brace = parse - | '.' space* nl { true } + | '.' space* nl { new_lines 1 lexbuf; true } | eof | '.' space+ { false } | "(*" { comment_level := 1; ignore (skipped_comment lexbuf); skip_to_dot_or_brace lexbuf } | "}" space* nl - { true } + { new_lines 1 lexbuf; true } | "}" { false } | space* @@ -1134,7 +1149,7 @@ and body_bol = parse | "" { Output.indentation 0; body lexbuf } and body = parse - | nl {Tokens.flush_sublexer(); Output.line_break(); Lexing.new_line lexbuf; body_bol lexbuf} + | nl { Tokens.flush_sublexer(); Output.line_break(); new_lines 1 lexbuf; body_bol lexbuf} | (nl+ as s) space* "]]" space* nl { new_lines (count_newlines s + 1) lexbuf; Tokens.flush_sublexer(); @@ -1156,7 +1171,7 @@ and body = parse end } | "]]" space* nl { Tokens.flush_sublexer(); - Lexing.new_line lexbuf; + new_lines 1 lexbuf; if is_none !formatted then begin let loc = lexeme_start lexbuf in @@ -1265,31 +1280,31 @@ and string = parse | _ { let c = lexeme_char lexbuf 0 in Output.char c; string lexbuf } and skip_hide = parse - | eof | end_hide nl { Lexing.new_line lexbuf; () } + | eof | end_hide nl { new_lines 1 lexbuf; () } | _ { skip_hide lexbuf } (*s Reading token pretty-print *) and printing_token_body = parse | "*)" (nl as s)? | eof - { if not (is_none s) then Lexing.new_line lexbuf; + { if not (is_none s) then new_lines 1 lexbuf; let s = Buffer.contents token_buffer in Buffer.clear token_buffer; s } | (nl | _) as s - { if is_nl s then Lexing.new_line lexbuf; + { if is_nl s then new_lines 1 lexbuf; Buffer.add_string token_buffer (lexeme lexbuf); printing_token_body lexbuf } and details_body = parse | "*)" space* (nl as s)? | eof - { if not (is_none s) then Lexing.new_line lexbuf; + { if not (is_none s) then new_lines 1 lexbuf; None } | ":" space* { details_body_rec lexbuf } and details_body_rec = parse | "*)" space* (nl as s)? | eof - { if not (is_none s) then Lexing.new_line lexbuf; + { if not (is_none s) then new_lines 1 lexbuf; let s = Buffer.contents token_buffer in Buffer.clear token_buffer; Some s } @@ -1300,9 +1315,10 @@ and details_body_rec = parse enclosed in [[[ ]]] brackets *) and inf_rules indents = parse | space* nl (* blank line, before or between definitions *) - { inf_rules indents lexbuf } + { new_lines 1 lexbuf; inf_rules indents lexbuf } | "]]]" nl (* end of the inference rules block *) - { match indents with + { new_lines 1 lexbuf; + match indents with | Some ls -> doc_list_bol ls lexbuf | None -> doc_bol lexbuf } | _ @@ -1315,7 +1331,8 @@ and inf_rules indents = parse *) and inf_rules_assumptions indents assumptions = parse | space* "---" '-'* [^ '\n']* nl (* hit the horizontal line *) - { let line = lexeme lexbuf in + { new_lines 1 lexbuf; + let line = lexeme lexbuf in let (spaces,_) = count_spaces line in let dashes_and_name = cut_head_tail_spaces (String.sub line 0 (String.length line - 1)) @@ -1334,7 +1351,8 @@ and inf_rules_assumptions indents assumptions = parse inf_rules_conclusion indents (List.rev assumptions) (spaces, dashes, name) [] lexbuf } | [^ '\n']* nl (* if it's not the horizontal line, it's an assumption *) - { let line = lexeme lexbuf in + { new_lines 1 lexbuf; + let line = lexeme lexbuf in let (spaces,_) = count_spaces line in let assumption = cut_head_tail_spaces (String.sub line 0 (String.length line - 1)) @@ -1348,11 +1366,12 @@ and inf_rules_assumptions indents assumptions = parse blank line or a ']]]'. *) and inf_rules_conclusion indents assumptions middle conclusions = parse | space* nl | space* "]]]" nl (* end of conclusions. *) - { backtrack lexbuf; + { new_lines 2 lexbuf; backtrack lexbuf; Output.inf_rule assumptions middle (List.rev conclusions); inf_rules indents lexbuf } | space* [^ '\n']+ nl (* this is a line in the conclusion *) - { let line = lexeme lexbuf in + { new_lines 1 lexbuf; + let line = lexeme lexbuf in let (spaces,_) = count_spaces line in let conc = cut_head_tail_spaces (String.sub line 0 (String.length line - 1)) @@ -1395,16 +1414,16 @@ and st_subtitle = parse { (* coq_bol with error handling *) let coq_bol' f lb = - Lexing.new_line lb; (* Start numbering lines from 1 *) try coq_bol lb with | MismatchPreformatted p -> - Printf.eprintf "%a: mismatched \"[[\"\n" print_position { p with pos_fname = f }; + Printf.eprintf "%a: mismatched \"[[\"\n" print_position_p p; exit 1 let coq_file f m = reset (); let c = open_in f in let lb = from_channel c in + let lb = { lb with lex_start_p = { lb.lex_start_p with pos_fname = f } } in (Index.current_library := m; Output.initialize (); Output.start_module (); -- cgit v1.2.3 From b01fb0118f701f7aec83a04039a280238c866be0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 5 Nov 2020 16:16:31 +0100 Subject: Dead code in coqdoc. --- tools/coqdoc/output.ml | 17 ----------------- tools/coqdoc/output.mli | 3 --- 2 files changed, 20 deletions(-) diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 32cf05e1eb..a6165918f9 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -479,10 +479,6 @@ module Latex = struct let end_coq () = printf "\\end{coqdoccode}\n" - let start_code () = end_doc (); start_coq () - - let end_code () = end_coq (); start_doc () - let section_kind = function | 1 -> "\\section{" | 2 -> "\\subsection{" @@ -754,10 +750,6 @@ module Html = struct let end_comment () = printf "*)" - let start_code () = end_doc (); start_coq () - - let end_code () = end_coq (); start_doc () - let start_inline_coq () = if !inline_notmono then printf "" else printf "" @@ -1069,9 +1061,6 @@ module TeXmacs = struct let start_comment () = () let end_comment () = () - let start_code () = in_doc := true; printf "<\\code>\n" - let end_code () = in_doc := false; printf "\n" - let section_kind = function | 1 -> "section" | 2 -> "subsection" @@ -1181,9 +1170,6 @@ module Raw = struct let start_coq () = () let end_coq () = () - let start_code () = end_doc (); start_coq () - let end_code () = end_coq (); start_doc () - let section_kind = function | 1 -> "* " @@ -1240,9 +1226,6 @@ let end_comment = select Latex.end_comment Html.end_comment TeXmacs.end_comment let start_coq = select Latex.start_coq Html.start_coq TeXmacs.start_coq Raw.start_coq 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 start_inline_coq = select Latex.start_inline_coq Html.start_inline_coq TeXmacs.start_inline_coq Raw.start_inline_coq let end_inline_coq = diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli index b7a8d4d858..4088fdabf7 100644 --- a/tools/coqdoc/output.mli +++ b/tools/coqdoc/output.mli @@ -41,9 +41,6 @@ val end_comment : unit -> unit val start_coq : unit -> unit val end_coq : unit -> unit -val start_code : unit -> unit -val end_code : unit -> unit - val start_inline_coq : unit -> unit val end_inline_coq : unit -> unit -- cgit v1.2.3 From 7923bb570cd493aff31ac1c94f9e03ff4efd465f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 5 Nov 2020 13:08:14 +0100 Subject: Addressing #13304: how to verbatim an expression mentioning >>. We clarify that there are two kinds of verbatim: inline and block. We add a test testing verbatim and others. Co-authored-by: Xia Li-yao --- test-suite/coqdoc/bug5700.html.out | 6 +- test-suite/coqdoc/bug5700.tex.out | 6 +- test-suite/coqdoc/bug5700.v | 2 +- test-suite/coqdoc/verbatim.html.out | 114 ++++++++++++++++++++++++++++++++++++ test-suite/coqdoc/verbatim.tex.out | 84 ++++++++++++++++++++++++++ test-suite/coqdoc/verbatim.v | 40 +++++++++++++ tools/coqdoc/cpretty.mll | 51 +++++++++------- tools/coqdoc/output.ml | 8 +-- 8 files changed, 278 insertions(+), 33 deletions(-) create mode 100644 test-suite/coqdoc/verbatim.html.out create mode 100644 test-suite/coqdoc/verbatim.tex.out create mode 100644 test-suite/coqdoc/verbatim.v diff --git a/test-suite/coqdoc/bug5700.html.out b/test-suite/coqdoc/bug5700.html.out index 286e8bba4d..84214a73d3 100644 --- a/test-suite/coqdoc/bug5700.html.out +++ b/test-suite/coqdoc/bug5700.html.out @@ -22,8 +22,7 @@
-
foo (* bar *)
- + foo (* {bar_bar} *)
Definition const1 := 1.
@@ -32,8 +31,7 @@
-
more (* nested (* comments *) within verbatim *)
- + more (* nested (* comments *) within verbatim *)
Definition const2 := 2.
diff --git a/test-suite/coqdoc/bug5700.tex.out b/test-suite/coqdoc/bug5700.tex.out index 1a1af5dfdd..9dddb00450 100644 --- a/test-suite/coqdoc/bug5700.tex.out +++ b/test-suite/coqdoc/bug5700.tex.out @@ -20,14 +20,12 @@ \begin{coqdoccode} \end{coqdoccode} -\begin{verbatim}foo (* bar *) \end{verbatim} - \begin{coqdoccode} +\texttt{ foo (* \{bar\_bar\} *) } \begin{coqdoccode} \coqdocnoindent \coqdockw{Definition} \coqdef{Coqdoc.bug5700.const1}{const1}{\coqdocdefinition{const1}} := 1.\coqdoceol \coqdocemptyline \end{coqdoccode} -\begin{verbatim}more (* nested (* comments *) within verbatim *) \end{verbatim} - \begin{coqdoccode} +\texttt{ more (* nested (* comments *) within verbatim *) } \begin{coqdoccode} \coqdocnoindent \coqdockw{Definition} \coqdef{Coqdoc.bug5700.const2}{const2}{\coqdocdefinition{const2}} := 2.\coqdoceol \end{coqdoccode} diff --git a/test-suite/coqdoc/bug5700.v b/test-suite/coqdoc/bug5700.v index 839034a48f..fc985276af 100644 --- a/test-suite/coqdoc/bug5700.v +++ b/test-suite/coqdoc/bug5700.v @@ -1,4 +1,4 @@ -(** << foo (* bar *) >> *) +(** << foo (* {bar_bar} *) >> *) Definition const1 := 1. (** << more (* nested (* comments *) within verbatim *) >> *) diff --git a/test-suite/coqdoc/verbatim.html.out b/test-suite/coqdoc/verbatim.html.out new file mode 100644 index 0000000000..bf9f975ee8 --- /dev/null +++ b/test-suite/coqdoc/verbatim.html.out @@ -0,0 +1,114 @@ + + + + + +Coqdoc.verbatim + + + + +
+ + + +
+ +

Library Coqdoc.verbatim

+ +
+
+ +
+ +
+ +
+uint32_t shift_right( uint32_t a, uint32_t shift )
+{
+    return a >> shift;
+}
+
+ +
+ +This line and the following shows verbatim text: + +
+ + A stand-alone inline verbatim + +
+ + A non-ended inline verbatim to test line location + + +
+ +
    +
  • item 1 + +
    • +
  • item 2 is verbatim + +
    • +
  • item 3 is verbatim too +
    +A coq block : ∀ n, n = 0 +
    + +     +
    • +
  • verbatim again, and a formula True → False + +
    • +
  • +
    +multiline
+verbatim
+
    + +
    • +
  • last item + +
    • +
+ +
+ +
+ + + + + + + + + + +
Γ ⊢ A +   +
Γ ⊢ A ∨ B
+
+ +
+A non-ended block verbatim to test line location
+
+*)
+
+
+
+
+
+ + + +
+ + + \ No newline at end of file diff --git a/test-suite/coqdoc/verbatim.tex.out b/test-suite/coqdoc/verbatim.tex.out new file mode 100644 index 0000000000..b692f6ad6a --- /dev/null +++ b/test-suite/coqdoc/verbatim.tex.out @@ -0,0 +1,84 @@ +\documentclass[12pt]{report} +\usepackage[utf8x]{inputenc} + +%Warning: tipa declares many non-standard macros used by utf8x to +%interpret utf8 characters but extra packages might have to be added +%such as "textgreek" for Greek letters not already in tipa +%or "stmaryrd" for mathematical symbols. +%Utf8 codes missing a LaTeX interpretation can be defined by using +%\DeclareUnicodeCharacter{code}{interpretation}. +%Use coqdoc's option -p to add new packages or declarations. +\usepackage{tipa} + +\usepackage[T1]{fontenc} +\usepackage{fullpage} +\usepackage{coqdoc} +\usepackage{amsmath,amssymb} +\usepackage{url} +\begin{document} +\coqlibrary{Coqdoc.verbatim}{Library }{Coqdoc.verbatim} + +\begin{coqdoccode} +\end{coqdoccode} + + +\begin{verbatim} +uint32_t shift_right( uint32_t a, uint32_t shift ) +{ + return a >> shift; +} +\end{verbatim} + + +This line and the following shows \texttt{verbatim } text: + + +\texttt{ A stand-alone inline verbatim } + + +\texttt{ A non-ended inline verbatim to test line location +} + + + +\begin{itemize} +\item item 1 + +\item item 2 is \texttt{verbatim} + +\item item 3 is \texttt{verbatim} too +\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdocvar{A} \coqdocvar{coq} \coqdocvar{block} : \coqdockw{\ensuremath{\forall}} \coqdocvar{n}, \coqdocvar{n} = 0 + +\coqdocemptyline + +\item \texttt{verbatim} again, and a formula \coqdocvar{True} \ensuremath{\rightarrow} \coqdocvar{False} + +\item +\begin{verbatim} +multiline +verbatim +\end{verbatim} + +\item last item + +\end{itemize} + + +\begin{verbatim} +Γ ⊢ A +---- +Γ ⊢ A ∨ B +\end{verbatim} + + +\begin{verbatim} +A non-ended block verbatim to test line location + +*) +\end{verbatim} +\begin{coqdoccode} +\end{coqdoccode} +\end{document} diff --git a/test-suite/coqdoc/verbatim.v b/test-suite/coqdoc/verbatim.v new file mode 100644 index 0000000000..129a5117c9 --- /dev/null +++ b/test-suite/coqdoc/verbatim.v @@ -0,0 +1,40 @@ +(** + +<< +uint32_t shift_right( uint32_t a, uint32_t shift ) +{ + return a >> shift; +} +>> + +This line and the following shows << verbatim >> text: + +<< A stand-alone inline verbatim >> + +<< A non-ended inline verbatim to test line location + + +- item 1 +- item 2 is <> +- item 3 is <> too +[[ +A coq block : forall n, n = 0 +]] +- <> again, and a formula [ True -> False ] +- +<< +multiline +verbatim +>> +- last item + +[[[ +Γ ⊢ A +---- +Γ ⊢ A ∨ B +]]] + +<< +A non-ended block verbatim to test line location + +*) diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index d056887591..f2b6a3f38f 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -748,8 +748,10 @@ and doc_bol = parse } | (space_nl* nl) as s { new_lines (count_newlines s) lexbuf; Output.paragraph (); doc_bol lexbuf } - | "<<" space* - { Output.start_verbatim false; verbatim 0 false lexbuf; doc_bol lexbuf } + | "<<" space* nl + { new_lines 1 lexbuf; Output.start_verbatim false; verbatim_block lexbuf; doc_bol lexbuf } + | "<<" + { Output.start_verbatim true; verbatim_inline lexbuf; doc None lexbuf } | eof { true } | '_' @@ -771,10 +773,14 @@ and doc_list_bol indents = parse | InLevel (_,false) -> backtrack lexbuf; doc_bol lexbuf } - | "<<" space* - { Output.start_verbatim false; - verbatim 0 false lexbuf; + | "<<" space* nl + { new_lines 1 lexbuf; Output.start_verbatim false; + verbatim_block lexbuf; doc_list_bol indents lexbuf } + | "<<" space* + { Output.start_verbatim true; + verbatim_inline lexbuf; + doc (Some indents) lexbuf } | "[[" nl { new_lines 1 lexbuf; formatted := Some lexbuf.lex_start_p; Output.start_inline_coq_block (); @@ -921,7 +927,7 @@ and doc indents = parse Output.char (lexeme_char lexbuf 1); doc indents lexbuf } | "<<" space* - { Output.start_verbatim true; verbatim 0 true lexbuf; doc_bol lexbuf } + { Output.start_verbatim true; verbatim_inline lexbuf; doc indents lexbuf } | '"' { if !Cdglobals.plain_comments then Output.char '"' @@ -961,20 +967,25 @@ and escaped_html = parse { backtrack lexbuf } | _ { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf } -and verbatim depth inline = parse - | nl ">>" space* nl { new_lines 2 lexbuf; Output.verbatim_char inline '\n'; Output.stop_verbatim inline } - | nl ">>" { new_lines 1 lexbuf; Output.verbatim_char inline '\n'; Output.stop_verbatim inline } - | ">>" { Output.stop_verbatim inline } - | "(*" { Output.verbatim_char inline '('; - Output.verbatim_char inline '*'; - verbatim (depth+1) inline lexbuf } - | "*)" { if (depth == 0) - then (Output.stop_verbatim inline; backtrack lexbuf) - else (Output.verbatim_char inline '*'; - Output.verbatim_char inline ')'; - verbatim (depth-1) inline lexbuf) } - | eof { Output.stop_verbatim inline } - | _ { Output.verbatim_char inline (lexeme_char lexbuf 0); verbatim depth inline lexbuf } +and verbatim_block = parse + | nl ">>" space* nl { new_lines 2 lexbuf; Output.verbatim_char false '\n'; Output.stop_verbatim false } + | nl ">>" + { new_lines 1 lexbuf; + warn "missing newline after \">>\" block" lexbuf; + Output.verbatim_char false '\n'; + Output.stop_verbatim false } + | eof { warn "unterminated \">>\" block" lexbuf; Output.stop_verbatim false } + | nl { new_lines 1 lexbuf; Output.verbatim_char false (lexeme_char lexbuf 0); verbatim_block lexbuf } + | _ { Output.verbatim_char false (lexeme_char lexbuf 0); verbatim_block lexbuf } + +and verbatim_inline = parse + | nl { new_lines 1 lexbuf; + warn "unterminated inline \">>\"" lexbuf; + Output.char '\n'; + Output.stop_verbatim true } + | ">>" { Output.stop_verbatim true } + | eof { warn "unterminated inline \">>\"" lexbuf; Output.stop_verbatim true } + | _ { Output.verbatim_char true (lexeme_char lexbuf 0); verbatim_inline lexbuf } and url = parse | "}}" { Output.url (Buffer.contents url_buffer) None; Buffer.clear url_buffer } diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index a6165918f9..57b2b6e620 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -313,7 +313,7 @@ module Latex = struct let start_verbatim inline = if inline then printf "\\texttt{" - else printf "\\begin{verbatim}" + else printf "\\begin{verbatim}\n" let stop_verbatim inline = if inline then printf "}" @@ -628,11 +628,11 @@ module Html = struct let stop_quote () = start_quote () let start_verbatim inline = - if inline then printf "" - else printf "
"
+    if inline then printf ""
+    else printf "
\n"
 
   let stop_verbatim inline =
-    if inline then printf ""
+    if inline then printf ""
     else printf "
\n"
 
   let url addr name =
-- 
cgit v1.2.3


From 0b12bb8c03b0ac7cc8aa7578a8db8ca93ecd1fd0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 5 Nov 2020 13:17:38 +0100
Subject: Documenting one-line verbatim.

---
 doc/sphinx/using/tools/coqdoc.rst | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/doc/sphinx/using/tools/coqdoc.rst b/doc/sphinx/using/tools/coqdoc.rst
index 7ab8f9d763..b68b2ed2a7 100644
--- a/doc/sphinx/using/tools/coqdoc.rst
+++ b/doc/sphinx/using/tools/coqdoc.rst
@@ -200,6 +200,14 @@ at the beginning of a line.
           if n <= 1 then 1 else n * fact (n-1)
       >>
 
+Verbatim material on a single line is also possible (assuming that
+``>>`` is not part of the text to be presented as verbatim).
+
+.. example::
+
+  ::
+
+      Here is the corresponding caml expression: << fact (n-1) >>
 
 
 Hyperlinks
-- 
cgit v1.2.3


From 696df507b58800a7a6b52741fd4ed859aff7b1c3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 5 Nov 2020 16:17:37 +0100
Subject: Coqdoc: we move a newline at a better place.

This does not affect the rendering but gives better structured
html/tex files.
---
 test-suite/coqdoc/binder.tex.out   | 3 ++-
 test-suite/coqdoc/bug12742.tex.out | 1 +
 test-suite/coqdoc/bug5700.tex.out  | 6 ++++--
 test-suite/coqdoc/links.tex.out    | 4 +++-
 tools/coqdoc/cpretty.mll           | 2 +-
 tools/coqdoc/output.ml             | 2 +-
 6 files changed, 12 insertions(+), 6 deletions(-)

diff --git a/test-suite/coqdoc/binder.tex.out b/test-suite/coqdoc/binder.tex.out
index 2b5648aee6..aceccc25fd 100644
--- a/test-suite/coqdoc/binder.tex.out
+++ b/test-suite/coqdoc/binder.tex.out
@@ -20,7 +20,8 @@
 
 \begin{coqdoccode}
 \end{coqdoccode}
-Link binders \begin{coqdoccode}
+Link binders 
+\begin{coqdoccode}
 \coqdocemptyline
 \coqdocnoindent
 \coqdockw{Definition} \coqdef{Coqdoc.binder.foo}{foo}{\coqdocdefinition{foo}} \coqdef{Coqdoc.binder.alpha:1}{alpha}{\coqdocbinder{alpha}} \coqdef{Coqdoc.binder.beta:2}{beta}{\coqdocbinder{beta}} := \coqref{Coqdoc.binder.alpha:1}{\coqdocvariable{alpha}} \coqexternalref{::nat scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocnotation{+}} \coqref{Coqdoc.binder.beta:2}{\coqdocvariable{beta}}.\coqdoceol
diff --git a/test-suite/coqdoc/bug12742.tex.out b/test-suite/coqdoc/bug12742.tex.out
index d7eba096fc..a8f4c254cb 100644
--- a/test-suite/coqdoc/bug12742.tex.out
+++ b/test-suite/coqdoc/bug12742.tex.out
@@ -46,6 +46,7 @@ Xxx xxxx xx xxxxx xxxxxxx xxxxx xxx xxxxxxxx xxxxxxx xxx xxx xxxx
           xxxxx xxxx xxxxxx.
 
 \end{itemize}
+
 \begin{coqdoccode}
 \end{coqdoccode}
 \end{document}
diff --git a/test-suite/coqdoc/bug5700.tex.out b/test-suite/coqdoc/bug5700.tex.out
index 9dddb00450..f2b12f0079 100644
--- a/test-suite/coqdoc/bug5700.tex.out
+++ b/test-suite/coqdoc/bug5700.tex.out
@@ -20,12 +20,14 @@
 
 \begin{coqdoccode}
 \end{coqdoccode}
-\texttt{ foo (* \{bar\_bar\} *) } \begin{coqdoccode}
+\texttt{ foo (* \{bar\_bar\} *) } 
+\begin{coqdoccode}
 \coqdocnoindent
 \coqdockw{Definition} \coqdef{Coqdoc.bug5700.const1}{const1}{\coqdocdefinition{const1}} := 1.\coqdoceol
 \coqdocemptyline
 \end{coqdoccode}
-\texttt{ more (* nested (* comments *) within verbatim *) } \begin{coqdoccode}
+\texttt{ more (* nested (* comments *) within verbatim *) } 
+\begin{coqdoccode}
 \coqdocnoindent
 \coqdockw{Definition} \coqdef{Coqdoc.bug5700.const2}{const2}{\coqdocdefinition{const2}} := 2.\coqdoceol
 \end{coqdoccode}
diff --git a/test-suite/coqdoc/links.tex.out b/test-suite/coqdoc/links.tex.out
index 2304f5ecc1..412a9ca6ac 100644
--- a/test-suite/coqdoc/links.tex.out
+++ b/test-suite/coqdoc/links.tex.out
@@ -36,6 +36,7 @@ Various checks for coqdoc
 \item  ``..'' should be rendered correctly
 
 \end{itemize}
+
 \begin{coqdoccode}
 \coqdocemptyline
 \coqdocnoindent
@@ -166,7 +167,8 @@ skip
 
  skip 
 
- skip \begin{coqdoccode}
+ skip 
+\begin{coqdoccode}
 \coqdocemptyline
 \end{coqdoccode}
 \end{document}
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index f2b6a3f38f..e5beab5d33 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -893,7 +893,7 @@ and doc indents = parse
        doc_bol lexbuf
       }
   | '*'* "*)" space* nl
-      { new_lines 1 lexbuf; true }
+      { new_lines 1 lexbuf; Output.char '\n'; true }
   | '*'* "*)"
       { false }
   | "$"
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 57b2b6e620..a87dfb5b2e 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -734,7 +734,7 @@ module Html = struct
 
   let end_doc () = in_doc := false;
     stop_item ();
-    if not !raw_comments then printf "\n
\n" + if not !raw_comments then printf "\n" let start_emph () = printf "" -- cgit v1.2.3