# HG changeset patch
# User wenzelm
# Date 1412611876 -7200
# Node ID 127f192b755c19004e91220c55d5cf2b00fe8610
# Parent  72e2f0e7e3449c04f4ccc140790708fb5629c0ea
more defensive error handling -- token marker must not crash;

diff -r 72e2f0e7e344 -r 127f192b755c src/Tools/jEdit/src/bibtex_jedit.scala
--- a/src/Tools/jEdit/src/bibtex_jedit.scala	Mon Oct 06 17:27:27 2014 +0200
+++ b/src/Tools/jEdit/src/bibtex_jedit.scala	Mon Oct 06 18:11:16 2014 +0200
@@ -171,19 +171,26 @@
         }
       val line = if (raw_line == null) new Segment else raw_line
 
+      def no_markup =
+      {
+        val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
+        (List(styled_token), new Line_Context(None))
+      }
+
       val context1 =
       {
         val (styled_tokens, context1) =
           line_ctxt match {
             case Some(ctxt) =>
-              val (chunks, ctxt1) = Bibtex.parse_line(line, ctxt)
-              val styled_tokens =
-                for { chunk <- chunks; tok <- chunk.tokens }
-                yield (token_style(chunk.kind, tok), tok.source)
-              (styled_tokens, new Line_Context(Some(ctxt1)))
-            case None =>
-              val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
-              (List(styled_token), new Line_Context(None))
+              try {
+                val (chunks, ctxt1) = Bibtex.parse_line(line, ctxt)
+                val styled_tokens =
+                  for { chunk <- chunks; tok <- chunk.tokens }
+                  yield (token_style(chunk.kind, tok), tok.source)
+                (styled_tokens, new Line_Context(Some(ctxt1)))
+              }
+              catch { case ERROR(msg) => Output.warning(msg); no_markup }
+            case None => no_markup
           }
 
         var offset = 0
@@ -244,7 +251,7 @@
         }
         data
       }
-      catch { case ERROR(_) => null }
+      catch { case ERROR(msg) => Output.warning(msg); null }
     }
   }
 }