Amélioration affichage Print ALl

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

1 files changed, 7 insertions, 10 deletions

diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 097a88e5a..6e831dc28 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -209,14 +209,10 @@ let print_inductive sp =
     hOV 0 [< 'sTR"Fw inductive definition "; 
 	     print_basename sp; 'fNL >]
 
-let print_syntactic_def with_values sep sp =
+let print_syntactic_def sep sp =
   let id = basename sp in
-  [< 'sTR" Syntax Macro "; 
-     pr_id id ; 'sTR sep;  
-     if with_values then 
-       let c = Syntax_def.search_syntactic_definition sp in 
-       [< pr_rawterm c >]
-     else [<>]; 'fNL >]
+  let c = Syntax_def.search_syntactic_definition sp in 
+  [< 'sTR" Syntactif Definition "; pr_id id ; 'sTR sep; pr_rawterm c; 'fNL >]
 
 let print_leaf_entry with_values sep (sp,lobj) =
   let tag = object_tag lobj in
@@ -228,11 +224,11 @@ let print_leaf_entry with_values sep (sp,lobj) =
     | (_,"INDUCTIVE") ->
 	print_inductive sp
     | (_,"AUTOHINT") -> 
-	[< 'sTR" Add Auto Marker"; 'fNL >]
+	[< 'sTR" Hint Marker"; 'fNL >]
     | (_,"GRAMMAR") -> 
 	[< 'sTR" Grammar Marker"; 'fNL >]
     | (_,"SYNTAXCONSTANT") -> 
-	print_syntactic_def with_values sep sp
+	print_syntactic_def sep sp
     | (_,"PPSYNTAX") -> 
 	[< 'sTR" Syntax Marker"; 'fNL >]
     | (_,"TOKEN") -> 
@@ -243,6 +239,7 @@ let print_leaf_entry with_values sep (sp,lobj) =
 	[< 'sTR" Coercion Marker"; 'fNL >]
     | (_,"REQUIRE") -> 
 	[< 'sTR" Require Marker"; 'fNL >]
+    | (_,"END-SECTION") -> [< >]
     | (_,s) -> 
 	[< 'sTR(string_of_path sp); 'sTR" : ";
            'sTR"Unrecognized object "; 'sTR s; 'fNL >]
@@ -343,7 +340,7 @@ let print_name qid =
   with Not_found ->
   try
     let sp = Syntax_def.locate_syntactic_definition qid in
-    print_syntactic_def true " = " sp
+    print_syntactic_def " = " sp
   with Not_found ->
     errorlabstrm "print_name"
       [< pr_qualid qid; 'sPC; 'sTR "not a defined object" >]