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

4 files changed, 52 insertions, 29 deletions

diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 3647152a..89f39b22 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqdep.ml 9276 2006-10-25 13:00:22Z barras $ *)
+(* $Id: coqdep.ml 9808 2007-04-29 07:15:18Z herbelin $ *)
 
 open Printf
 open Coqdep_lexer
@@ -24,6 +24,8 @@ let option_i = ref false
 let option_sort = ref false
 let option_slash = ref false
 
+let directories_added = ref false
+
 let suffixe = ref ".vo"
 let suffixe_spec = ref ".vi"
 
@@ -42,7 +44,7 @@ let file_concat l =
 (* Files specified on the command line *)
 let mlAccu  = ref ([] : (string * string * dir) list) 
 and mliAccu = ref ([] : (string * string * dir) list) 
-and vAccu   = ref ([] : string list)
+and vAccu   = ref ([] : (string * string) list)
 
 (* Queue operations *)
 let addQueue q v = q := v :: !q
@@ -97,6 +99,16 @@ let safe_assoc verbose file k =
   List.assoc k !vKnown
 
 
+let absolute_dir dir =
+  let current = Sys.getcwd () in
+  Sys.chdir dir;
+  let dir' = Sys.getcwd () in
+  Sys.chdir current;
+  dir'
+
+let absolute_file_name basename odir =
+  let dir = match odir with Some dir -> dir | None -> "." in
+  absolute_dir dir / basename
      
 let file_name = function
   | (s,None)     -> file_concat s 
@@ -152,9 +164,11 @@ let cut_prefix p s =
   let ls = String.length s in
   if ls >= lp && String.sub s 0 lp = p then String.sub s lp (ls - lp) else s
 
-let canonize f = match Sys.os_type with
-  | "Win32" when not !option_slash -> cut_prefix ".\\" f
-  | _ -> cut_prefix "./" f
+let canonize f =
+  let f' = absolute_dir (Filename.dirname f) / Filename.basename f in
+  match List.filter (fun (_,full) -> f' = full) !vAccu with
+    | (f,_) :: _ -> f
+    | _ -> f
 
 let sort () = 
   let seen = Hashtbl.create 97 in
@@ -181,7 +195,7 @@ let sort () =
 	printf "%s%s " file !suffixe
     end
   in
-  List.iter loop !vAccu
+  List.iter (fun (name,_) -> loop name) !vAccu
 
 let traite_fichier_Coq verbose f = 
   try 
@@ -352,7 +366,7 @@ let mL_dependencies () =
 
 let coq_dependencies () =
   List.iter
-    (fun name ->
+    (fun (name,_) ->
        printf "%s%s: %s.v" name !suffixe name;
        traite_fichier_Coq true (name ^ ".v");
        printf "\n";
@@ -366,7 +380,7 @@ let coq_dependencies () =
 
 let declare_dependencies () =
   List.iter
-    (fun name ->
+    (fun (name,_) ->
        traite_Declare (name^".v");      
        flush stdout)
     (List.rev !vAccu)
@@ -410,7 +424,7 @@ let all_subdirs root_dir log_dir =
 
 let usage () =
   eprintf
-  "[ usage: coqdep [-w] [-I dir] [-coqlib dir] [-c] [-i] [-D] <filename>+ ]\n";
+  "[ usage: coqdep [-w] [-I dir] [-R dir coqdir] [-coqlib dir] [-c] [-i] [-D] <filename>+ ]\n";
   flush stderr;
   exit 1
 
@@ -471,7 +485,8 @@ let coqdep () =
 	    addQueue mliAccu (basename,".mli",dirname)
 	  else if Filename.check_suffix name ".v" then
 	    let basename = Filename.chop_suffix name ".v" in
-	    addQueue vAccu (file_name ([basename], dirname))
+	    let name = file_name ([basename],dirname) in
+	    addQueue vAccu (name, absolute_file_name basename dirname)
       | _ -> ()
   in 
   let add_known phys_dir log_dir f =
@@ -496,6 +511,7 @@ let coqdep () =
                 (fun n -> safe_addQueue clash_v vKnown (n,file)) paths
         | _ -> () in
   let add_directory (phys_dir, log_dir) = 
+      directories_added := true;
       match try (stat phys_dir).st_kind with _ -> S_BLK with 
 	| S_DIR -> 
 	    (let dir = opendir phys_dir in
@@ -526,7 +542,7 @@ let coqdep () =
       | f :: ll -> treat None f; parse ll
       | [] -> ()
   in
-  add_directory (".", []);
+  if not !directories_added then add_directory (".", []);
   parse (List.tl (Array.to_list Sys.argv));
   List.iter
     (fun (s,_) -> add_coqlib_directory s)
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 { () }
diff --git a/tools/coqwc.mll b/tools/coqwc.mll
index 26b64095..0ce172ea 100644
--- a/tools/coqwc.mll
+++ b/tools/coqwc.mll
@@ -9,7 +9,7 @@
 (* coqwc - counts the lines of spec, proof and comments in Coq sources
  * Copyright (C) 2003 Jean-Christophe Filliātre *)
 
-(*i $Id: coqwc.mll 7095 2005-05-31 15:05:23Z filliatr $ i*)
+(*i $Id: coqwc.mll 9976 2007-07-12 11:58:30Z msozeau $ i*)
 
 (*s {\bf coqwc.} Counts the lines of spec, proof and comments in a Coq source. 
     It assumes the files to be lexically well-formed. *)
@@ -97,7 +97,7 @@ let rcs = "\036" rcs_keyword [^ '$']* "\036"
 let stars = "(*" '*'* "*)"
 let dot = '.' (' ' | '\t' | '\n' | '\r' | eof)
 let proof_start =   
-  "Theorem" | "Lemma" | "Fact" | "Remark" | "Goal" | "Correctness"
+  "Theorem" | "Lemma" | "Fact" | "Remark" | "Goal" | "Correctness" | "Obligation" | "Next"
 let proof_end =
   ("Save" | "Qed" | "Defined" | "Abort" | "Admitted") [^'.']* '.'
 
@@ -114,8 +114,10 @@ rule spec = parse
            { seen_spec := true; spec_to_dot lexbuf; proof lexbuf }
   | proof_start '\n'
            { seen_spec := true; newline (); spec_to_dot lexbuf; proof lexbuf }
-  | "Definition" space
+  | "Program"? "Definition" space
            { seen_spec := true; definition lexbuf }
+  | "Program"? "Fixpoint" space
+  	   { seen_spec := true; definition lexbuf }
   | character | _ 
 	   { seen_spec := true; spec lexbuf }
   | eof    { () }