Misc fixes.

- Correct backtracking function of coqdoc to handle the _p fields of lexers
- Try a better typesetting of [[ ]] inline code considering it as
blocks and not purely inline code like [ ] escapings.
- Rework latex macros for better factorization and support external
references in pdf output.
- Better criterion for generalization of variables in dependent
elimination tactic and better error message in [specialize_hypothesis].
- In autounfold, don't put the core unfolds by default.


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

4 files changed, 83 insertions, 93 deletions

diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty
index b50b755f6..4314d07d6 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,12 +121,15 @@
 
   \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}[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}[3]{\cleardoublepage\chapter{#2\coqdoccst{#3}}}
@@ -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/cpretty.mll b/tools/coqdoc/cpretty.mll
index 2820b9a88..c20449bcd 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -70,7 +70,9 @@
   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
+  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
@@ -435,7 +437,9 @@ let end_verb = "(*" space* "end" space+ "verb" space* "*)"
 
 rule coq_bol = parse
   | space* nl+
-      { if not (!in_proof <> None && (!Cdglobals.gallina || !Cdglobals.light)) then Output.empty_line_of_code (); coq_bol lexbuf }
+      { 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
@@ -707,10 +711,9 @@ and doc_list_bol indents = parse
         doc_list_bol indents lexbuf }
   | "[[" nl
       { formatted := true;
-        Output.paragraph ();
-        Output.start_inline_coq ();
+        Output.start_inline_coq_block ();
         ignore(body_bol lexbuf);
-        Output.end_inline_coq ();
+        Output.end_inline_coq_block ();
         formatted := false;
         doc_list_bol indents lexbuf }
   | space* nl space* '-'
@@ -779,9 +782,9 @@ and doc indents = parse
       { if !Cdglobals.plain_comments
         then (Output.char '['; Output.char '['; doc indents lexbuf)
         else (formatted := true;
-              Output.line_break (); Output.start_inline_coq ();
+              Output.start_inline_coq_block ();
 	      let eol = body_bol lexbuf in
-	        Output.end_inline_coq (); formatted := false;
+	        Output.end_inline_coq_block (); formatted := false;
 	        if eol then
 		  match indents with
 		  | Some ls -> doc_list_bol ls lexbuf
@@ -931,9 +934,9 @@ and comment = parse
       if !Cdglobals.parse_comments then
         if !Cdglobals.plain_comments then (Output.char '['; Output.char '[')
         else (formatted := true;
-              Output.line_break (); Output.start_inline_coq ();
+              Output.start_inline_coq_block ();
               let _ = body_bol lexbuf in
-                Output.end_inline_coq (); formatted := false);
+                Output.end_inline_coq_block (); formatted := false);
       comment lexbuf}
   | "$"
       { if !Cdglobals.parse_comments then
@@ -986,7 +989,7 @@ and body_bol = parse
   | _ { backtrack lexbuf; Output.indentation 0; body lexbuf }
 
 and body = parse
-  | nl {Output.line_break(); body_bol lexbuf}
+  | nl {Output.line_break(); Lexing.new_line lexbuf; body_bol lexbuf}
   | nl+ space* "]]" space* nl
       { if not !formatted then
           begin
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index ae35f7445..90d0d0e00 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -252,28 +252,25 @@ module Latex = struct
 
   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>"
-    | External m when !externals ->
-	printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>"
-    | External _ | Unknown ->
-	raw_ident s
-    i*)
 
   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 "}"
-      | External _ when !externals ->
-	  printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}"
+      | Local -> 
+	  if typ = Variable then (printf "\\coqdoc%s{" (type_name typ); raw_ident s; printf "}")
+	  else
+	    (printf "\\coqref{"; label_ident id; printf "}{\\coqdoc%s{" (type_name typ);
+	     raw_ident s; printf "}}")
+      | External m when !externals ->
+	  printf "\\coqexternalref{"; label_ident m; printf "}{";
+	  label_ident fid; printf "}{\\coqdoc%s{" (type_name typ); raw_ident s; printf "}}"
       | External _ | Unknown ->
-	  printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}"
+	  (* printf "\\coqref{"; label_ident id; printf "}{" *)
+	  printf "\\coqdoc%s{" (type_name typ); raw_ident s; printf "}"
 
   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 "}{"; raw_ident s; printf "}{";
+    printf "\\coqdoc%s{" (type_name ty); raw_ident s; printf "}}"
 
   let reference s = function
     | Def (fullid,typ) ->
@@ -286,24 +283,18 @@ module Latex = struct
 	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
-	try
-	  reference s (Index.find (get_module false) 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 (get_module false) s)
-	      with _ -> (printf "\\coqdocvar{"; raw_ident s; printf "}")
-	    else (printf "\\coqdocvar{"; raw_ident s; printf "}")
-	  end
-      end
-    end
+    try
+      reference s (Index.find (get_module false) loc)
+    with Not_found ->
+      if is_tactic s then
+	(printf "\\coqdoctac{"; raw_ident s; printf "}")
+      else if is_keyword s then
+	(printf "\\coqdockw{"; raw_ident s; printf "}")
+      else if !Cdglobals.interpolate && !in_doc (* always a var otherwise *)
+      then
+	try reference s (Index.find_string (get_module false) s)
+	with _ -> (printf "\\coqdocvar{"; raw_ident s; printf "}")
+      else (printf "\\coqdocvar{"; raw_ident s; printf "}")
 
   let ident s l =
     if !in_title then (
@@ -379,6 +370,10 @@ module Latex = struct
 
   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 () = ()
@@ -591,6 +586,10 @@ module Html = struct
 
   let end_inline_coq () = printf "</span>"
 
+  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 =
@@ -871,6 +870,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 () = ()
@@ -966,6 +969,9 @@ 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 () = ()
@@ -1004,6 +1010,12 @@ let start_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
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index 35f056d94..f8a25285c 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -44,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