more error information according to @<Print type of token list@> in pdfweb.tex;
authorwenzelm
Wed Dec 13 17:42:17 2017 +0100 (17 months ago)
changeset 67196eb29f4868d14
parent 67195 6be90977f882
child 67197 b335e255ebcc
more error information according to @<Print type of token list@> in pdfweb.tex;
src/Pure/Thy/latex.scala
     1.1 --- a/src/Pure/Thy/latex.scala	Wed Dec 13 16:42:02 2017 +0100
     1.2 +++ b/src/Pure/Thy/latex.scala	Wed Dec 13 17:42:17 2017 +0100
     1.3 @@ -116,15 +116,25 @@
     1.4          }
     1.5      }
     1.6  
     1.7 -    object Line_Error
     1.8 -    {
     1.9 -      val Pattern = """^l\.(\d+) (.*)$""".r
    1.10 -      def unapply(line: String): Option[(Int, String)] =
    1.11 -        line match {
    1.12 -          case Pattern(Value.Int(line), message) => Some((line, message))
    1.13 -          case _ => None
    1.14 -        }
    1.15 -    }
    1.16 +    val More_Error =
    1.17 +      List(
    1.18 +        """l\.\d+""",
    1.19 +        "<argument>",
    1.20 +        "<template>",
    1.21 +        "<recently read>",
    1.22 +        "<to be read again>",
    1.23 +        "<inserted text>",
    1.24 +        "<output>",
    1.25 +        "<everypar>",
    1.26 +        "<everymath>",
    1.27 +        "<everydisplay>",
    1.28 +        "<everyhbox>",
    1.29 +        "<everyvbox>",
    1.30 +        "<everyjob>",
    1.31 +        "<everycr>",
    1.32 +        "<mark>",
    1.33 +        "<everyeof>",
    1.34 +        "<write>").mkString("^(?:", "|", ") (.*)$").r
    1.35  
    1.36      @tailrec def filter(lines: List[String], result: List[(String, Position.T)])
    1.37        : List[(String, Position.T)] =
    1.38 @@ -133,7 +143,7 @@
    1.39          case File_Line_Error((file, line, msg1)) :: rest1 =>
    1.40            val pos = tex_file_position(file, line)
    1.41            rest1 match {
    1.42 -            case Line_Error((line2, msg2)) :: rest2 if line == line2 =>
    1.43 +            case More_Error(msg2) :: rest2 =>
    1.44                filter(rest2, (Exn.cat_message(msg1, msg2), pos) :: result)
    1.45              case _ =>
    1.46                filter(rest1, (msg1, pos) :: result)