direct pretty printing of parsetrees -- prevent diagnostic output from crashing due to undeclared entities;

--- a/src/Pure/Syntax/parser.ML	Sun Apr 03 21:59:33 2011 +0200
+++ b/src/Pure/Syntax/parser.ML	Mon Apr 04 15:51:45 2011 +0200
@@ -15,6 +15,7 @@
   datatype parsetree =
     Node of string * parsetree list |
     Tip of Lexicon.token
+  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
   val branching_level: int Config.T
@@ -632,6 +633,11 @@
   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);
+
 type state =
   nt_tag * int *    (*identification and production precedence*)
   parsetree list *  (*already parsed nonterminals on rhs*)

--- a/src/Pure/Syntax/syntax.ML	Sun Apr 03 21:59:33 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML	Mon Apr 04 15:51:45 2011 +0200
@@ -725,9 +725,6 @@
     val len = length pts;
 
     val limit = Config.get ctxt ambiguity_limit;
-    fun show_pt pt =
-      Pretty.string_of
-        (Ast.pretty_ast (#2 (Syn_Trans.parsetree_to_ast ctxt type_ctxt false (K NONE) pt)));
     val _ =
       if len <= Config.get ctxt ambiguity_level then ()
       else if not (Config.get ctxt ambiguity_enabled) then error (ambiguity_msg pos)
@@ -736,7 +733,7 @@
           (("Ambiguous input" ^ Position.str_of pos ^
             "\nproduces " ^ string_of_int len ^ " parse trees" ^
             (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
-            map show_pt (take limit pts))));
+            map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))));
 
     val constrain_pos = not raw andalso Config.get ctxt positions;
   in