src/Pure/sign.ML
changeset 901 77795af99315
parent 881 d7dcba167ed8
child 922 196ca0973a6d
equal deleted inserted replaced
900:8e22076cd3ca 901:77795af99315
   290               process_terms ts (Some n, infrd_t', tye') msg'' (n+1)
   290               process_terms ts (Some n, infrd_t', tye') msg'' (n+1)
   291          end
   291          end
   292       | process_terms [] (idx, infrd_t, tye) msg _ = 
   292       | process_terms [] (idx, infrd_t, tye) msg _ = 
   293           if msg = "" then (the idx, the infrd_t, the tye) 
   293           if msg = "" then (the idx, the infrd_t, the tye) 
   294           else
   294           else
   295             (if length ts <= !Syntax.ambiguity_level then
   295             (if length ts > 1 andalso length ts <= !Syntax.ambiguity_level then
   296                                                       (*no warning shown yet?*)
   296                                                       (*no warning shown yet?*)
   297                writeln "Warning: Currently parsed input \
   297                writeln "Warning: Currently parsed input \
   298                        \produces more than one parse tree.\n\
   298                        \produces more than one parse tree.\n\
   299                        \For more information lower Syntax.ambiguity_level."
   299                        \For more information lower Syntax.ambiguity_level."
   300              else ();
   300              else ();