# HG changeset patch
# User wenzelm
# Date 1515871852 -3600
# Node ID 8bec22c6b0fb5858e88f0c2e78c533ed031ccd0f
# Parent  eec44c98d8b327b2a6870d0f0b1bec5f4b833854
tuned messages;

diff -r eec44c98d8b3 -r 8bec22c6b0fb src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala	Sat Jan 13 20:02:19 2018 +0100
+++ b/src/Pure/Thy/latex.scala	Sat Jan 13 20:30:52 2018 +0100
@@ -109,7 +109,8 @@
             val path = File.standard_path(file)
             if (Path.is_wellformed(path)) {
               val file = (dir + Path.explode(path)).canonical
-              if (file.is_file) Some((file, line, message)) else None
+              val msg = Library.perhaps_unprefix("LaTeX Error: ", message)
+              if (file.is_file) Some((file, line, msg)) else None
             }
             else None
           case _ => None
@@ -136,11 +137,17 @@
         "<everyeof>",
         "<write>").mkString("^(?:", "|", ") (.*)$").r
 
+    val error_ignore =
+      Set(
+        "See the LaTeX manual or LaTeX Companion for explanation.",
+        "Type  H <return>  for immediate help.")
+
     def error_suffix1(lines: List[String]): Option[String] =
     {
       val lines1 = lines.take(20).takeWhile({ case File_Line_Error(_) => false case _ => true })
       lines1.zipWithIndex.collectFirst({
-        case (Line_Error(msg), i) => cat_lines(lines1.take(i) ::: List(msg)) })
+        case (Line_Error(msg), i) =>
+          cat_lines(lines1.take(i).filterNot(error_ignore) ::: List(msg)) })
     }
     def error_suffix2(lines: List[String]): Option[String] =
       lines match {