Better handling of emphasis.

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

1 files changed, 7 insertions, 3 deletions

diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 22d81d6f54..d92b34e25e 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -65,7 +65,11 @@
   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
   let backtrack_past_newline lexbuf =
     let buf = lexeme lexbuf in
@@ -675,7 +679,7 @@ and doc_bol = parse
   | eof
       { true }
   | '_'
-      { Output.start_emph ();
+      { start_emph ();
         doc None lexbuf }
   | _
       { backtrack lexbuf; doc None lexbuf }
@@ -823,10 +827,10 @@ and doc indents = parse
         doc indents lexbuf}
   | nonidentchar '_'
       { Output.char (lexeme_char lexbuf 0);
-        Output.start_emph ();
+        start_emph ();
         doc indents lexbuf }
   | '_' nonidentchar
-      { Output.stop_emph ();
+      { stop_emph ();
         Output.char (lexeme_char lexbuf 1);
         doc indents lexbuf }
   | eof