src/Pure/Thy/latex.scala
changeset 67417 34522db6b85a
parent 67196 eb29f4868d14
child 67418 5a6ed2e679fb
--- a/src/Pure/Thy/latex.scala	Sat Jan 13 12:19:03 2018 +0100
+++ b/src/Pure/Thy/latex.scala	Sat Jan 13 12:51:03 2018 +0100
@@ -145,6 +145,10 @@
           rest1 match {
             case More_Error(msg2) :: rest2 =>
               filter(rest2, (Exn.cat_message(msg1, msg2), pos) :: result)
+            case msg2 :: rest2
+            if msg1.startsWith("Undefined control sequence") &&
+                msg2.startsWith("\\") && msg2.containsSlice("->") =>
+              filter(rest2, (Exn.cat_message(msg1, msg2), pos) :: result)
             case _ =>
               filter(rest1, (msg1, pos) :: result)
           }