From 94236aaad5f951ff5d47d9c1f63250081da4607a Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 19 Dec 2000 15:44:08 +0000
Subject: Amélioration affichage Print ALl
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1153 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/pretty.ml | 17 +++++++----------
 1 file 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" >]
-- 
cgit v1.2.3