src/Pure/Syntax/syntax.ML
changeset 1580 e3fd931e6095
parent 1511 09354d37a5ab
child 1813 23bda45846a2
equal deleted inserted replaced
1579:688e18023915 1580:e3fd931e6095
   306     val pts = parse gram root' (tokenize lexicon xids str);
   306     val pts = parse gram root' (tokenize lexicon xids str);
   307 
   307 
   308     fun show_pt pt = writeln (str_of_ast (pt_to_ast (K None) pt));
   308     fun show_pt pt = writeln (str_of_ast (pt_to_ast (K None) pt));
   309   in
   309   in
   310     if length pts > ! ambiguity_level then
   310     if length pts > ! ambiguity_level then
   311       (writeln ("Warning: Ambiguous input " ^ quote str);
   311       (warning ("Ambiguous input " ^ quote str);
   312        writeln "produces the following parse trees:";
   312        writeln "produces the following parse trees:";
   313        seq show_pt pts)
   313        seq show_pt pts)
   314     else ();
   314     else ();
   315     map (pt_to_ast (lookup_trtab parse_ast_trtab)) pts
   315     map (pt_to_ast (lookup_trtab parse_ast_trtab)) pts
   316   end;
   316   end;