Ajout du traducteur

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

3 files changed, 72 insertions, 19 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index e8268e038d..f4315529d8 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -102,10 +102,10 @@ GEXTEND Gram
       | IDENT "Remark" -> Remark ] ]
   ;
   def_token:
-    [ [ "Definition" -> (fun _ _ -> ()), Global
-      | IDENT "Local" -> (fun _ _ -> ()), Local
-      | IDENT "SubClass"  -> Class.add_subclass_hook, Global
-      | IDENT "Local"; IDENT "SubClass"  -> Class.add_subclass_hook, Local ] ] 
+    [ [ "Definition" -> (fun _ _ -> ()), Global, GDefinition
+      | IDENT "Local" -> (fun _ _ -> ()), Local, LDefinition
+      | IDENT "SubClass"  -> Class.add_subclass_hook, Global, GCoercion
+      | IDENT "Local"; IDENT "SubClass"  -> Class.add_subclass_hook, Local, LCoercion ] ] 
   ;
   assumption_token:
     [ [ "Hypothesis" -> (Local, Logical)
@@ -178,8 +178,8 @@ GEXTEND Gram
     (* Definition, Theorem, Variable, Axiom, ... *)
     [ [ thm = thm_token; id = base_ident; bl = binders_list; ":"; c = constr ->
          VernacStartTheoremProof (thm, id, (bl, c), false, (fun _ _ -> ()))
-      | (f,d) = def_token; id = base_ident; b = def_body -> 
-          VernacDefinition (d, id, b, f)
+      | (f,d,e) = def_token; id = base_ident; b = def_body -> 
+          VernacDefinition (d, id, b, f, e)
       | stre = assumption_token; bl = ne_params_list -> 
 	  VernacAssumption (stre, bl)
       | stre = assumptions_token; bl = ne_params_list ->
@@ -383,17 +383,17 @@ GEXTEND Gram
 	  VernacCanonical qid
       | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body ->
           let s = Ast.coerce_global_to_id qid in
-	  VernacDefinition (Global,s,d,Recordobj.add_object_hook)
+	  VernacDefinition (Global,s,d,Recordobj.add_object_hook,SCanonical)
       (* Rem: LOBJECT, OBJCOERCION, LOBJCOERCION have been removed
          (they were unused and undocumented) *)
 
 (* Coercions *)
       | IDENT "Coercion"; qid = global; d = def_body ->
           let s = Ast.coerce_global_to_id qid in
-	  VernacDefinition (Global,s,d,Class.add_coercion_hook)
+	  VernacDefinition (Global,s,d,Class.add_coercion_hook,GCoercion)
       | IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body ->
            let s = Ast.coerce_global_to_id qid in
-	  VernacDefinition (Local,s,d,Class.add_coercion_hook)
+	  VernacDefinition (Local,s,d,Class.add_coercion_hook,LCoercion)
       | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = base_ident;
          ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> 
 	   VernacIdentityCoercion (Local, f, s, t)
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index cb0f071111..2d84593bc2 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -8,6 +8,7 @@
 
 (*i $Id$ i*)
 
+open Pp
 open Token
 
 (* Dictionaries: trees annotated with string options, each node being a map
@@ -195,20 +196,54 @@ let rec string bp len = parser
   | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_string
   | [< 'c; s >] -> string bp (store len c) s 
 
+let comments = ref None
+
+type commentar =
+  | InVernac
+  | InVernacEsc of string
+  | BeVernac of string
+  | InComment of string
+
+let current = ref (BeVernac "")
+
+let add_comment () = let reinit () = match ! current with
+  | InVernac -> ()
+  | InVernacEsc s -> current := InVernacEsc ""
+  | BeVernac s -> current := BeVernac ""
+  | InComment s -> current := InComment "" in
+match (!comments,!current) with
+  | None , InVernac -> ()
+  | None , BeVernac s | None , InComment s | None , InVernacEsc s -> reinit (); comments := Some [str s]
+  | Some _ , InVernac -> ()
+  | Some l , BeVernac s | Some l , InComment s | Some l , InVernacEsc s -> reinit (); comments := Some (str s::l)
+
+let add_comment_pp s = match !comments with
+  | None -> comments := Some [s]
+  | Some l -> comments := Some (s::l) 
+
+let add_string s = match !current with
+  | InVernac -> ()
+  | InVernacEsc t -> current := InVernacEsc (t^s)
+  | BeVernac t -> current := BeVernac (t^s)
+  | InComment t -> current := InComment (t^s)
+	
 let rec comment bp = parser
   | [< ''(';
        _ = (parser
-              | [< ''*'; _ = comment bp >] -> ()
-              | [< >] -> ()); 
+              | [< ''*'; s >] -> add_string "(*"; comment bp s
+              | [< >] -> add_string "(" ); 
        s >] -> comment bp s
   | [< ''*';
        _ = parser
-         | [< '')' >] -> ()
-         | [< s >] -> comment bp s >] -> ()
+         | [< '')' >] -> add_string "*)"; add_comment ()
+         | [< s >] -> add_string "*"; comment bp s >] -> ()
   | [< ''"'; _ = (parser bp [< _ = string bp 0 >] -> ()); s >] ->
       comment bp s
   | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_comment
-  | [< '_; s >] -> comment bp s 
+  | [< '_ as z; s >] -> 
+	(match z with
+	| '\n' | '\t' -> add_comment (); add_comment_pp (fnl ())
+	| _ -> add_string (String.make 1 z)); comment bp s 
 
 (* Parse a special token, using the [token_tree] *)
 
@@ -235,21 +270,28 @@ let process_chars bp c cs =
 (* Parse a token in a char stream *)
 
 let rec next_token = parser bp
-  | [< '' ' | '\n' | '\r'| '\t'; s >] -> next_token s
+  | [< ''\n'; s >] -> (match !current with
+	| BeVernac s -> current := InComment s
+	| InComment _ -> add_comment_pp (fnl ())
+	| _ -> ()); next_token s
+  | [< '' ' | '\t'; s >] -> (match !current with
+	| BeVernac _ |  InComment _ -> add_comment_pp (spc ())
+	| _ -> ()); next_token s
+  | [< ''\r'; s >] -> next_token s
   | [< ''$'; len = ident (store 0 '$') >] ep -> 
       (("METAIDENT", get_buff len), (bp,ep))
   | [< ''.' as c; t = parser
 	 | [< ' ('_' | 'a'..'z' | 'A'..'Z' | '\192'..'\214' 
 		| '\216'..'\246' | '\248'..'\255' as c);
-	      len = ident (store 0 c) >] -> ("FIELD", get_buff len)
+	      len = ident (store 0 c) >] -> current:=BeVernac ""; ("FIELD", get_buff len)
 (*
 	 | [< >] -> ("", ".") >] ep -> (t, (bp,ep))
 *)
-	 | [< (t,_) = process_chars bp c >] -> t >] ep -> (t, (bp,ep))
+	 | [< (t,_) = process_chars bp c >] -> t >] ep -> current:=BeVernac ""; (t, (bp,ep))
   | [< ' ('_' | 'a'..'z' | 'A'..'Z' | '\192'..'\214' 
          | '\216'..'\246' | '\248'..'\255' as c);
        len = ident (store 0 c) >] ep ->
-      let id = get_buff len in
+      let id = get_buff len in current:=InVernac; 
       (try ("", find_keyword id) with Not_found -> ("IDENT", id)), (bp, ep)
   | [< ' ('0'..'9' as c); len = number (store 0 c) >] ep ->
       (("INT", get_buff len), (bp, ep))
@@ -257,7 +299,14 @@ let rec next_token = parser bp
       (("STRING", get_buff len), (bp, ep))
   | [< ' ('(' as c);
        t = parser
-         | [< ''*'; _ = comment bp; s >] -> next_token s
+         | [< ''*'; c; s >] -> (match !current with
+				| InVernac -> current := InVernacEsc "(*"
+				| _ -> current := InComment "(*"); 
+	comment bp c; 
+	(match !current with
+	| InVernacEsc _ -> add_comment_pp (fnl ()); current := InVernac
+	| _ -> ()); 
+	next_token s
          | [< t = process_chars bp c >] -> t >] -> t
   | [< 'c; t = process_chars bp c >] -> t
   | [< _ = Stream.empty >] -> (("EOI", ""), (bp, bp + 1))
diff --git a/parsing/lexer.mli b/parsing/lexer.mli
index 9b0e3bbd8b..b722e8b0c9 100644
--- a/parsing/lexer.mli
+++ b/parsing/lexer.mli
@@ -8,6 +8,8 @@
 
 (*i $Id$ i*)
 
+open Pp
+
 type error =
   | Illegal_character
   | Unterminated_comment
@@ -32,3 +34,5 @@ type frozen_t
 val freeze : unit -> frozen_t
 val unfreeze : frozen_t -> unit
 val init : unit -> unit
+
+val comments : (std_ppcmds list option) ref