Imported Upstream version 8.1.pl1+dfsgupstream/8.1.pl1+dfsg

2 files changed, 20 insertions, 15 deletions

diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 84e03d92..28a0cd6d 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: output.ml 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: output.ml 9976 2007-07-12 11:58:30Z msozeau $ i*)
 
 open Cdglobals
 open Index
@@ -40,15 +40,14 @@ let is_keyword =
       "Module"; "Module Type"; "Declare Module";
       "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Qed";
       "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme";
-      "Section"; "Show"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; 
+      "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; 
       "Unset"; "Variable"; "Variables"; 
       "Notation"; 
-      (*i (* correctness *)
-      "array"; "assert"; "begin"; "do"; "done"; "else"; "end"; "if";
-      "in"; "invariant"; "let"; "of"; "ref"; "state"; "then"; "variant";
-      "while"; i*)
-      (*i (* coq terms *)
-      "with"; "Case"; "Cases"; "Prop"; "Set"; "Type"; i*)
+      (* Program *)
+      "Program Definition"; "Program Fixpoint"; "Program Lemma";
+      "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next";
+      (*i (* coq terms *) *)
+	"match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun"; "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="
        ]
 
 (*s Current Coq module *)
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index bdb58f86..c63a6a9b 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pretty.mll 9204 2006-10-04 13:05:58Z notin $ i*)
+(*i $Id: pretty.mll 10017 2007-07-18 13:23:55Z notin $ i*)
 
 (*s Utility functions for the scanners *)
 
@@ -212,6 +212,8 @@ let def_token =
   | "Scheme"
   | "Inductive"
   | "CoInductive"
+  | "Program" space+ "Definition"
+  | "Program" space+ "Fixpoint"
 
 let decl_token = 
   "Hypothesis" 
@@ -455,11 +457,11 @@ and doc = parse
 	start_inline_coq (); escaped_coq lexbuf; end_inline_coq ();
 	doc lexbuf }
   | "[[" '\n' space*
-      { formatted := true; start_code ();
+      { formatted := true; line_break (); start_inline_coq ();
 	indentation (count_spaces (lexeme lexbuf)); 
-	without_gallina coq lexbuf; 
-	end_code (); formatted := false;
-	doc lexbuf }
+	let eol = body_bol lexbuf in 
+	  end_inline_coq (); formatted := false;
+	  if eol then doc_bol lexbuf else doc lexbuf}
   | '*'* "*)" space* '\n'
       { true }
   | '*'* "*)"
@@ -570,6 +572,8 @@ and body_bol = parse
 
 and body = parse
   | '\n' {line_break(); body_bol lexbuf}
+  | '\n'+ space* "]]"
+      { if not !formatted then begin symbol (lexeme lexbuf); body lexbuf end else true }
   | eof { false }
   | '.' space* '\n' | '.' space* eof { char '.'; line_break(); true }      
   | '.' space+ { char '.'; char ' '; false }
@@ -577,12 +581,14 @@ and body = parse
 	     if eol then body_bol lexbuf else body lexbuf }
   | identifier 
       { let s = lexeme lexbuf in 
-	  ident s (lexeme_start lexbuf); body lexbuf }
+	  ident s (lexeme_start lexbuf); 
+	  body lexbuf }
   | token
       { let s = lexeme lexbuf in
 	  symbol s; body lexbuf }
   | _ { let c = lexeme_char lexbuf 0 in 
-	  char c; body lexbuf }
+	  char c; 
+          body lexbuf }
 
 and skip_hide = parse
   | eof | end_hide { () }