# HG changeset patch
# User wenzelm
# Date 1515844263 -3600
# Node ID 34522db6b85a83138d699a1a27f191966f19cbec
# Parent  efc9ec53922455644df79b75c478bba63343f9d0
another Latex error seen in the wild:
Undefined control sequence.
\isamarkupcancel #1->\xout

diff -r efc9ec539224 -r 34522db6b85a src/Pure/Thy/latex.scala
--- 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)
           }