avoid spurious noise: Prover IDE is meant to check for errors;
authorwenzelm
Thu, 28 Dec 2017 12:44:42 +0100
changeset 67288 aa9d28034945
parent 67287 7ef1c5dada12
child 67289 bef14fa789ef
avoid spurious noise: Prover IDE is meant to check for errors;
src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Thu Dec 28 12:36:11 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Dec 28 12:44:42 2017 +0100
@@ -280,7 +280,7 @@
     lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
     lazy val bibtex_entries: List[Text.Info[String]] =
       try { Bibtex.entries(text) }
-      catch { case ERROR(msg) => Output.warning(msg); Nil }
+      catch { case ERROR(_) => Nil }
   }