some support for LaTeX;
authorwenzelm
Fri Dec 08 23:43:58 2017 +0100 (17 months ago)
changeset 6717297d199699a6b
parent 67164 39f57f0757f1
child 67173 e746db6db903
some support for LaTeX;
src/Pure/Thy/latex.scala
src/Pure/build-jars
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Thy/latex.scala	Fri Dec 08 23:43:58 2017 +0100
     1.3 @@ -0,0 +1,60 @@
     1.4 +/*  Title:      Pure/Thy/latex.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Support for LaTeX.
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +
    1.13 +import scala.annotation.tailrec
    1.14 +
    1.15 +
    1.16 +object Latex
    1.17 +{
    1.18 +  sealed case class Error(file: Option[Path], line: Int, message: String)
    1.19 +
    1.20 +  def filter_errors(dir: Path, text: String): List[Error] =
    1.21 +  {
    1.22 +    object File_Line_Error
    1.23 +    {
    1.24 +      val Pattern = """^(.*):(\d+): (.*)$""".r
    1.25 +      def unapply(line: String): Option[Error] =
    1.26 +        line match {
    1.27 +          case Pattern(file, Value.Int(line), message) =>
    1.28 +            val path = File.standard_path(file)
    1.29 +            if (Path.is_wellformed(path)) {
    1.30 +              val file = Path.explode(path)
    1.31 +              if ((dir + file).is_file) Some(Error(Some(file), line, message)) else None
    1.32 +            }
    1.33 +            else None
    1.34 +          case _ => None
    1.35 +        }
    1.36 +    }
    1.37 +
    1.38 +    object Line_Error
    1.39 +    {
    1.40 +      val Pattern = """^l\.(\d+) (.*)$""".r
    1.41 +      def unapply(line: String): Option[Error] =
    1.42 +        line match {
    1.43 +          case Pattern(Value.Int(line), message) => Some(Error(None, line, message))
    1.44 +          case _ => None
    1.45 +        }
    1.46 +    }
    1.47 +
    1.48 +    @tailrec def filter(lines: List[String], result: List[Error]): List[Error] =
    1.49 +      lines match {
    1.50 +        case File_Line_Error(err1) :: rest1 =>
    1.51 +          rest1 match {
    1.52 +            case Line_Error(err2) :: rest2 if err1.line == err2.line =>
    1.53 +              val err = err1.copy(message = Exn.cat_message(err1.message, err2.message))
    1.54 +              filter(rest2, err :: result)
    1.55 +            case _ => filter(rest1, err1 :: result)
    1.56 +          }
    1.57 +        case _ :: rest => filter(rest, result)
    1.58 +        case Nil => result.reverse
    1.59 +      }
    1.60 +
    1.61 +    filter(split_lines(text), Nil)
    1.62 +  }
    1.63 +}
     2.1 --- a/src/Pure/build-jars	Fri Dec 08 17:57:29 2017 +0100
     2.2 +++ b/src/Pure/build-jars	Fri Dec 08 23:43:58 2017 +0100
     2.3 @@ -126,6 +126,7 @@
     2.4    System/progress.scala
     2.5    System/system_channel.scala
     2.6    Thy/html.scala
     2.7 +  Thy/latex.scala
     2.8    Thy/present.scala
     2.9    Thy/sessions.scala
    2.10    Thy/thy_header.scala