From e0d682ec25282a348d35c5b169abafec48555690 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Mon, 20 Aug 2012 18:27:01 +0200
Subject: Imported Upstream version 8.4dfsg

---
 tools/coqdoc/cpretty.mll | 71 ++++++++++++++++++++++++++++++++++++++----------
 1 file changed, 57 insertions(+), 14 deletions(-)

(limited to 'tools/coqdoc/cpretty.mll')

diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 925f5258..d7b54fd0 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -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
@@ -254,7 +263,7 @@
     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)
+    Output.keyword s (lexeme_start lexbuf + isp)
 
 }
 
@@ -369,13 +378,17 @@ let commands =
   | "Drop"
   | "ProtectedLoop"
   | "Quit"
+  | "Restart"
   | "Load"
   | "Add"
   | "Remove" space+ "Loadpath"
   | "Print"
   | "Inspect"
   | "About"
+  | "SearchAbout"
+  | "SearchRewrite"
   | "Search"
+  | "Locate"
   | "Eval"
   | "Reset"
   | "Check"
@@ -403,6 +416,14 @@ let prog_kw =
   | "Obligations"
   | "Solve"
 
+let hint_kw = 
+  "Extern" | "Rewrite" | "Resolve" | "Immediate" | "Transparent" | "Opaque" | "Unfold" | "Constructors"
+
+let set_kw =
+    "Printing" space+ ("Coercions" | "Universes" | "All")
+  | "Implicit" space+ "Arguments"
+  
+
 let gallina_kw_to_hide =
     "Implicit" space+ "Arguments"
   | "Ltac"
@@ -410,15 +431,16 @@ let gallina_kw_to_hide =
   | "Import"
   | "Export"
   | "Load"
-  | "Hint"
+  | "Hint" space+ hint_kw
   | "Open"
   | "Close"
   | "Delimit"
   | "Transparent"
   | "Opaque"
   | ("Declare" space+ ("Morphism" | "Step") )
-  | ("Set" | "Unset") space+ "Printing" space+ "Coercions"
+  | ("Set" | "Unset") space+ set_kw
   | "Declare" space+ ("Left" | "Right") space+ "Step"
+  | "Debug" space+ ("On" | "Off")
 
 
 let section = "*" | "**" | "***" | "****"
@@ -689,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 }
   | '_'
@@ -713,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;
@@ -813,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;
@@ -872,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 }
   | _
@@ -898,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 inline '\n'; Output.stop_verbatim inline }
+  | nl ">>" { Output.verbatim_char inline '\n'; Output.stop_verbatim inline }
+  | ">>" { Output.stop_verbatim inline }
+  | eof { Output.stop_verbatim inline }
+  | _ { Output.verbatim_char inline (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 *)
 
-- 
cgit v1.2.3