# HG changeset patch
# User wenzelm
# Date 1406214700 -7200
# Node ID 10df45dd14da62833df926b93f65df563eab6bd5
# Parent  17d7f5d963289c3beb99ddf0d2b1121aa749f362
less warnings -- ignore potential prover startup/shutdown races;

diff -r 17d7f5d96328 -r 10df45dd14da src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Thu Jul 24 16:21:50 2014 +0200
+++ b/src/Pure/PIDE/session.scala	Thu Jul 24 17:11:40 2014 +0200
@@ -562,6 +562,9 @@
             if (global_state.value.is_assigned(change.previous))
               handle_change(change)
             else postponed_changes.store(change)
+
+          case bad =>
+            if (verbose) Output.warning("Ignoring bad message: " + bad.toString)
         }
         true
         //}}}