direct pretty printing of parsetrees -- prevent diagnostic output from crashing due to undeclared entities;
authorwenzelm
Mon Apr 04 15:51:45 2011 +0200 (2011-04-04)
changeset 4220522f5cc06c419
parent 42204 b3277168c1e7
child 42216 183ea7f77b72
direct pretty printing of parsetrees -- prevent diagnostic output from crashing due to undeclared entities;
src/Pure/Syntax/parser.ML
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Syntax/parser.ML	Sun Apr 03 21:59:33 2011 +0200
     1.2 +++ b/src/Pure/Syntax/parser.ML	Mon Apr 04 15:51:45 2011 +0200
     1.3 @@ -15,6 +15,7 @@
     1.4    datatype parsetree =
     1.5      Node of string * parsetree list |
     1.6      Tip of Lexicon.token
     1.7 +  val pretty_parsetree: parsetree -> Pretty.T
     1.8    val parse: Proof.context -> gram -> string -> Lexicon.token list -> parsetree list
     1.9    val guess_infix_lr: gram -> string -> (string * bool * bool * int) option
    1.10    val branching_level: int Config.T
    1.11 @@ -632,6 +633,11 @@
    1.12    Node of string * parsetree list |
    1.13    Tip of Lexicon.token;
    1.14  
    1.15 +fun pretty_parsetree (Node (c, pts)) =
    1.16 +      Pretty.enclose "(" ")" (Pretty.breaks
    1.17 +        (Pretty.quote (Pretty.str c) :: map pretty_parsetree pts))
    1.18 +  | pretty_parsetree (Tip tok) = Pretty.str (Lexicon.str_of_token tok);
    1.19 +
    1.20  type state =
    1.21    nt_tag * int *    (*identification and production precedence*)
    1.22    parsetree list *  (*already parsed nonterminals on rhs*)
     2.1 --- a/src/Pure/Syntax/syntax.ML	Sun Apr 03 21:59:33 2011 +0200
     2.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Apr 04 15:51:45 2011 +0200
     2.3 @@ -725,9 +725,6 @@
     2.4      val len = length pts;
     2.5  
     2.6      val limit = Config.get ctxt ambiguity_limit;
     2.7 -    fun show_pt pt =
     2.8 -      Pretty.string_of
     2.9 -        (Ast.pretty_ast (#2 (Syn_Trans.parsetree_to_ast ctxt type_ctxt false (K NONE) pt)));
    2.10      val _ =
    2.11        if len <= Config.get ctxt ambiguity_level then ()
    2.12        else if not (Config.get ctxt ambiguity_enabled) then error (ambiguity_msg pos)
    2.13 @@ -736,7 +733,7 @@
    2.14            (("Ambiguous input" ^ Position.str_of pos ^
    2.15              "\nproduces " ^ string_of_int len ^ " parse trees" ^
    2.16              (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
    2.17 -            map show_pt (take limit pts))));
    2.18 +            map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))));
    2.19  
    2.20      val constrain_pos = not raw andalso Config.get ctxt positions;
    2.21    in