another Latex error seen in the wild:
authorwenzelm
Sat, 13 Jan 2018 12:51:03 +0100
changeset 67417 34522db6b85a
parent 67416 efc9ec539224
child 67418 5a6ed2e679fb
another Latex error seen in the wild: Undefined control sequence. \isamarkupcancel #1->\xout
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)
           }