Add inline verbatim (<</>>), quotes (") and urls ({{url} name}) markup/typesetting to coqdoc.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15689 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 108 insertions, 23 deletions

diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 115bbe1cf..b96200091 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -77,8 +77,17 @@
   let in_proof = ref None
   let in_emph = ref false
 
-  let start_emph () = in_emph := true; Output.start_emph ()
-  let stop_emph () = if !in_emph then (Output.stop_emph (); in_emph := false)
+  let in_env start stop = 
+    let r = ref false in
+    let start_env () = r := true; start () in
+    let stop_env () = if !r then stop (); r := false in
+      (fun x -> !r), start_env, stop_env
+      
+  let in_emph, start_emph, stop_emph = in_env Output.start_emph Output.stop_emph
+  let in_quote, start_quote, stop_quote = in_env Output.start_quote Output.stop_quote
+
+  let url_buffer = Buffer.create 40
+  let url_name_buffer = Buffer.create 40
 
   let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos;
     lexbuf.lex_curr_p <- lexbuf.lex_start_p
@@ -702,7 +711,7 @@ and doc_bol = parse
   | space* nl+
       { Output.paragraph (); doc_bol lexbuf }
   | "<<" space*
-      { Output.start_verbatim (); verbatim lexbuf; doc_bol lexbuf }
+      { Output.start_verbatim false; verbatim false lexbuf; doc_bol lexbuf }
   | eof
       { true }
   | '_'
@@ -726,8 +735,8 @@ and doc_list_bol indents = parse
             backtrack lexbuf; doc_bol lexbuf
       }
   | "<<" space*
-      { Output.start_verbatim ();
-        verbatim lexbuf;
+      { Output.start_verbatim false;
+        verbatim false lexbuf;
         doc_list_bol indents lexbuf }
   | "[[" nl
       { formatted := true;
@@ -826,6 +835,7 @@ and doc indents = parse
       { inf_rules indents lexbuf }
   | "[]"
       { Output.proofbox (); doc indents lexbuf }
+  | "{{" { url lexbuf; doc indents lexbuf }
   | "["
       { if !Cdglobals.plain_comments then Output.char '['
         else (brackets := 1;  Output.start_inline_coq (); escaped_coq lexbuf;
@@ -885,6 +895,15 @@ and doc indents = parse
       { if !Cdglobals.plain_comments then Output.char '_' else stop_emph () ;
         Output.char (lexeme_char lexbuf 1);
         doc indents lexbuf }
+  | "<<" space*
+      { Output.start_verbatim true; verbatim true lexbuf; doc_bol lexbuf }
+  | '"'
+      { if !Cdglobals.plain_comments 
+	then Output.char '"' 
+	else if in_quote ()
+	then stop_quote () 
+	else start_quote ();
+        doc indents lexbuf }
   | eof
       { false }
   | _
@@ -911,11 +930,22 @@ and escaped_html = parse
   | eof { () }
   | _   { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf }
 
-and verbatim = parse
-  | nl ">>" space* nl { Output.verbatim_char '\n'; Output.stop_verbatim () }
-  | nl ">>" { Output.verbatim_char '\n'; Output.stop_verbatim () }
-  | eof { Output.stop_verbatim () }
-  | _ { Output.verbatim_char (lexeme_char lexbuf 0); verbatim lexbuf }
+and verbatim inline = parse
+  | nl ">>" space* nl { Output.verbatim_char '\n'; Output.stop_verbatim inline }
+  | nl ">>" { Output.verbatim_char '\n'; Output.stop_verbatim inline }
+  | ">>" { Output.stop_verbatim inline }
+  | eof { Output.stop_verbatim inline }
+  | _ { Output.verbatim_char (lexeme_char lexbuf 0); verbatim inline lexbuf }
+
+and url = parse
+  | "}}" { Output.url (Buffer.contents url_buffer) None; Buffer.clear url_buffer }
+  | "}" { url_name lexbuf }
+  | _ { Buffer.add_char url_buffer (lexeme_char lexbuf 0); url lexbuf }
+
+and url_name = parse
+  | "}" { Output.url (Buffer.contents url_buffer) (Some (Buffer.contents url_name_buffer));
+	  Buffer.clear url_buffer; Buffer.clear url_name_buffer }
+  | _ { Buffer.add_char url_name_buffer (lexeme_char lexbuf 0); url_name lexbuf }
 
 (*s Coq, inside quotations *)
 
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 2eec876cb..ab65474be 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -300,9 +300,23 @@ module Latex = struct
 
   let stop_latex_math () = output_char '$'
 
-  let start_verbatim () = printf "\\begin{verbatim}"
-
-  let stop_verbatim () = printf "\\end{verbatim}\n"
+  let start_quote () = output_char '`'; output_char '`'
+  let stop_quote () = output_char '\''; output_char '\''
+    
+  let start_verbatim inline = 
+    if inline then printf "\\texttt{"
+    else printf "\\begin{verbatim}"
+
+  let stop_verbatim inline =
+    if inline then printf "}"
+    else printf "\\end{verbatim}\n"
+
+  let url addr name = 
+    printf "%s\\footnote{\\url{%s}}"
+      (match name with
+       | None -> ""
+       | Some n -> n)
+      addr
 
   let indentation n =
     if n == 0 then
@@ -589,8 +603,22 @@ module Html = struct
   let start_latex_math () = ()
   let stop_latex_math () = ()
 
-  let start_verbatim () = printf "<pre>"
-  let stop_verbatim () = printf "</pre>\n"
+  let start_quote () = char '"'
+  let stop_quote () = start_quote ()
+
+  let start_verbatim inline = 
+    if inline then printf "<tt>"
+    else printf "<pre>"
+
+  let stop_verbatim inline = 
+    if inline then printf "</tt>" 
+    else printf "</pre>\n"
+
+  let url addr name = 
+    printf "<a href=\"%s\">%s</a>" addr 
+      (match name with
+       | Some n -> n
+       | None -> addr)
 
   let module_ref m s =
     match find_module m with
@@ -948,9 +976,17 @@ module TeXmacs = struct
 
   let stop_latex_math () = output_char '>'
 
-  let start_verbatim () = in_doc := true; printf "<\\verbatim>"
+  let start_verbatim inline = in_doc := true; printf "<\\verbatim>"
+  let stop_verbatim inline = in_doc := false; printf "</verbatim>"
 
-  let stop_verbatim () = in_doc := false; printf "</verbatim>"
+  let url addr name = 
+    printf "%s<\\footnote><\\url>%s</url></footnote>" addr
+      (match name with
+       | None -> ""
+       | Some n -> n)
+
+  let start_quote () = output_char '`'; output_char '`'
+  let stop_quote () = output_char '\''; output_char '\''
 
   let indentation n = ()
 
@@ -1076,9 +1112,16 @@ module Raw = struct
   let start_latex_math () = ()
   let stop_latex_math () = ()
 
-  let start_verbatim () = ()
+  let start_verbatim inline = ()
+  let stop_verbatim inline = ()
+
+  let url addr name = 
+    match name with
+    | Some n -> printf "%s (%s)" n addr
+    | None -> printf "%s" addr
 
-  let stop_verbatim () = ()
+  let start_quote () = printf "\""
+  let stop_quote () = printf "\""
 
   let indentation n =
       for i = 1 to n do printf " " done
@@ -1229,8 +1272,16 @@ let verbatim_char =
   select output_char Html.char TeXmacs.char Raw.char
 let hard_verbatim_char = output_char
 
+let url = 
+  select Latex.url Html.url TeXmacs.url Raw.url
+
+let start_quote =
+  select Latex.start_quote Html.start_quote TeXmacs.start_quote Raw.start_quote
+let stop_quote =
+  select Latex.stop_quote Html.stop_quote TeXmacs.stop_quote Raw.stop_quote
+
 let inf_rule_dumb assumptions (midsp,midln,midnm) conclusions = 
-  start_verbatim ();
+  start_verbatim false;
   let dumb_line = 
        function (sp,ln) -> (String.iter char ((String.make sp ' ') ^ ln);
                             char '\n')
@@ -1240,7 +1291,7 @@ let inf_rule_dumb assumptions (midsp,midln,midnm) conclusions =
                                 | Some s -> " " ^ s 
                                 | None -> ""));
      List.iter dumb_line conclusions);
-  stop_verbatim ()
+  stop_verbatim false
 
 let inf_rule = select inf_rule_dumb Html.inf_rule inf_rule_dumb inf_rule_dumb
 
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index b68857b27..2fcd58715 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -76,8 +76,12 @@ val hard_verbatim_char : char -> unit
 
 val start_latex_math : unit -> unit
 val stop_latex_math : unit -> unit
-val start_verbatim : unit -> unit
-val stop_verbatim : unit -> unit
+val start_verbatim : bool -> unit
+val stop_verbatim : bool -> unit
+val start_quote : unit -> unit
+val stop_quote : unit -> unit
+
+val url : string -> string option -> unit
 
 (* this outputs an inference rule in one go.  You pass it the list of
    assumptions, then the middle line info, then the conclusion (which