# HG changeset patch
# User wenzelm
# Date 1303040842 -7200
# Node ID b9a6b465da25850aecf547693f3eab3d89728bec
# Parent  fb539d6d1ac25901dad56596dc37d37a8660ee3d
clarified pretty_parsetree: suppress literal tokens;

diff -r fb539d6d1ac2 -r b9a6b465da25 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Sat Apr 16 23:41:58 2011 +0200
+++ b/src/Pure/Syntax/parser.ML	Sun Apr 17 13:47:22 2011 +0200
@@ -14,6 +14,7 @@
   datatype parsetree =
     Node of string * parsetree list |
     Tip of Lexicon.token
+  exception PARSETREE of parsetree
   val pretty_parsetree: parsetree -> Pretty.T
   val parse: Proof.context -> gram -> string -> Lexicon.token list -> parsetree list
   val guess_infix_lr: gram -> string -> (string * bool * bool * int) option
@@ -627,16 +628,26 @@
 
 
 
-(** Parser **)
+(** parser **)
+
+(* parsetree *)
 
 datatype parsetree =
   Node of string * parsetree list |
   Tip of Lexicon.token;
 
-fun pretty_parsetree (Node (c, pts)) =
-      Pretty.enclose "(" ")" (Pretty.breaks
-        (Pretty.quote (Pretty.str c) :: map pretty_parsetree pts))
-  | pretty_parsetree (Tip tok) = Pretty.str (Lexicon.str_of_token tok);
+exception PARSETREE of parsetree;
+
+fun pretty_parsetree parsetree =
+  let
+    fun pretty (Node (c, pts)) =
+          [Pretty.enclose "(" ")" (Pretty.breaks (Pretty.quote (Pretty.str c) :: maps pretty pts))]
+      | pretty (Tip tok) =
+          if Lexicon.valued_token tok then [Pretty.str (Lexicon.str_of_token tok)] else [];
+  in (case pretty parsetree of [prt] => prt | _ => raise PARSETREE parsetree) end;
+
+
+(* parser state *)
 
 type state =
   nt_tag * int *    (*identification and production precedence*)