src/Pure/Thy/latex.scala
author wenzelm
Mon Dec 11 17:49:47 2017 +0100 (18 months ago)
changeset 67183 28227b13a2f1
parent 67182 bdc03e20fce3
child 67184 ecc786cb3b7b
permissions -rw-r--r--
proper file;
wenzelm@67172
     1
/*  Title:      Pure/Thy/latex.scala
wenzelm@67172
     2
    Author:     Makarius
wenzelm@67172
     3
wenzelm@67172
     4
Support for LaTeX.
wenzelm@67172
     5
*/
wenzelm@67172
     6
wenzelm@67172
     7
package isabelle
wenzelm@67172
     8
wenzelm@67172
     9
wenzelm@67173
    10
import java.io.{File => JFile}
wenzelm@67173
    11
wenzelm@67172
    12
import scala.annotation.tailrec
wenzelm@67172
    13
wenzelm@67172
    14
wenzelm@67172
    15
object Latex
wenzelm@67172
    16
{
wenzelm@67173
    17
  /** latex errors **/
wenzelm@67173
    18
wenzelm@67176
    19
  def latex_errors(dir: Path, root_name: String): List[String] =
wenzelm@67176
    20
  {
wenzelm@67176
    21
    val root_log_path = dir + Path.explode(root_name).ext("log")
wenzelm@67176
    22
    if (root_log_path.is_file) {
wenzelm@67176
    23
      for { (msg, pos) <- filter_errors(dir, File.read(root_log_path)) }
wenzelm@67176
    24
      yield "Latex error" + Position.here(pos) + ":\n" + cat_lines(split_lines(msg).map("  " + _))
wenzelm@67176
    25
    }
wenzelm@67176
    26
    else Nil
wenzelm@67176
    27
  }
wenzelm@67176
    28
wenzelm@67176
    29
wenzelm@67173
    30
  /* generated .tex file */
wenzelm@67173
    31
wenzelm@67173
    32
  private val File_Pattern = """^.*%:%file=(.+)%:%$""".r
wenzelm@67173
    33
  private val Range_Pattern2 = """^.*%:%range=(\d+):(\d+)%:%$""".r
wenzelm@67173
    34
  private val Range_Pattern1 = """^.*%:%range=(\d+)%:%$""".r
wenzelm@67173
    35
wenzelm@67173
    36
  def read_tex_file(tex_file: Path): Tex_File =
wenzelm@67174
    37
    new Tex_File(tex_file, Line.logical_lines(File.read(tex_file)).toArray)
wenzelm@67173
    38
wenzelm@67173
    39
  final class Tex_File private[Latex](val tex_file: Path, tex_lines: Array[String])
wenzelm@67173
    40
  {
wenzelm@67173
    41
    override def toString: String = tex_file.toString
wenzelm@67173
    42
wenzelm@67173
    43
    val source_file: Option[Path] =
wenzelm@67173
    44
      if (tex_lines.length > 0) {
wenzelm@67173
    45
        tex_lines(0) match {
wenzelm@67173
    46
          case File_Pattern(file) if Path.is_wellformed(file) && Path.explode(file).is_file =>
wenzelm@67173
    47
            Some(Path.explode(file))
wenzelm@67173
    48
          case _ => None
wenzelm@67173
    49
        }
wenzelm@67173
    50
      }
wenzelm@67173
    51
      else None
wenzelm@67173
    52
wenzelm@67173
    53
    val source_content: Line.Document =
wenzelm@67173
    54
      source_file match {
wenzelm@67173
    55
        case Some(file) => Line.Document(Symbol.decode(File.read(file)))
wenzelm@67173
    56
        case None => Line.Document.empty
wenzelm@67173
    57
      }
wenzelm@67173
    58
wenzelm@67173
    59
    lazy val source_chunk: Symbol.Text_Chunk =
wenzelm@67173
    60
      Symbol.Text_Chunk(source_content.text)
wenzelm@67172
    61
wenzelm@67173
    62
    def source_position(l: Int): Option[Position.T] =
wenzelm@67173
    63
      for {
wenzelm@67173
    64
        file <- source_file
wenzelm@67173
    65
        if 0 < l && l <= tex_lines.length
wenzelm@67173
    66
        line = tex_lines(l - 1)
wenzelm@67173
    67
        if line.endsWith("%:%")
wenzelm@67173
    68
        symbol_range <-
wenzelm@67173
    69
          (line match {
wenzelm@67173
    70
            case Range_Pattern2(Value.Int(i), Value.Int(j)) => Some(Text.Range(i, j))
wenzelm@67173
    71
            case Range_Pattern1(Value.Int(i)) => Some(Text.Range(i, i + 1))
wenzelm@67173
    72
            case _ => None
wenzelm@67173
    73
          })
wenzelm@67173
    74
        range <- source_chunk.incorporate(symbol_range)
wenzelm@67173
    75
      }
wenzelm@67173
    76
      yield {
wenzelm@67173
    77
        Position.Line_File(source_content.position(range.start).line1, file.implode) :::
wenzelm@67173
    78
        Position.Range(symbol_range)
wenzelm@67173
    79
      }
wenzelm@67173
    80
wenzelm@67173
    81
    def tex_position(line: Int): Position.T =
wenzelm@67182
    82
        Position.Line_File(line, tex_file.implode)
wenzelm@67173
    83
wenzelm@67173
    84
    def position(line: Int): Position.T =
wenzelm@67173
    85
      source_position(line) getOrElse tex_position(line)
wenzelm@67173
    86
  }
wenzelm@67173
    87
wenzelm@67173
    88
wenzelm@67173
    89
  /* latex log */
wenzelm@67173
    90
wenzelm@67173
    91
  def filter_errors(dir: Path, root_log: String): List[(String, Position.T)] =
wenzelm@67172
    92
  {
wenzelm@67173
    93
    val seen_files = Synchronized(Map.empty[JFile, Tex_File])
wenzelm@67173
    94
wenzelm@67173
    95
    def check_tex_file(path: Path): Option[Tex_File] =
wenzelm@67173
    96
      seen_files.change_result(seen =>
wenzelm@67173
    97
        seen.get(path.file) match {
wenzelm@67173
    98
          case None =>
wenzelm@67173
    99
            if (path.is_file) {
wenzelm@67173
   100
              val tex_file = read_tex_file(path)
wenzelm@67173
   101
              (Some(tex_file), seen + (path.file -> tex_file))
wenzelm@67173
   102
            }
wenzelm@67173
   103
            else (None, seen)
wenzelm@67173
   104
          case some => (some, seen)
wenzelm@67173
   105
        })
wenzelm@67173
   106
wenzelm@67173
   107
    def tex_file_position(path: Path, line: Int): Position.T =
wenzelm@67173
   108
      check_tex_file(path) match {
wenzelm@67173
   109
        case Some(tex_file) => tex_file.position(line)
wenzelm@67173
   110
        case None => Position.Line_File(line, path.implode)
wenzelm@67173
   111
      }
wenzelm@67173
   112
wenzelm@67172
   113
    object File_Line_Error
wenzelm@67172
   114
    {
wenzelm@67172
   115
      val Pattern = """^(.*):(\d+): (.*)$""".r
wenzelm@67173
   116
      def unapply(line: String): Option[(Path, Int, String)] =
wenzelm@67172
   117
        line match {
wenzelm@67172
   118
          case Pattern(file, Value.Int(line), message) =>
wenzelm@67172
   119
            val path = File.standard_path(file)
wenzelm@67172
   120
            if (Path.is_wellformed(path)) {
wenzelm@67183
   121
              val file = (dir + Path.explode(path)).canonical
wenzelm@67173
   122
              if (file.is_file) Some((file, line, message)) else None
wenzelm@67172
   123
            }
wenzelm@67172
   124
            else None
wenzelm@67172
   125
          case _ => None
wenzelm@67172
   126
        }
wenzelm@67172
   127
    }
wenzelm@67172
   128
wenzelm@67172
   129
    object Line_Error
wenzelm@67172
   130
    {
wenzelm@67172
   131
      val Pattern = """^l\.(\d+) (.*)$""".r
wenzelm@67173
   132
      def unapply(line: String): Option[(Int, String)] =
wenzelm@67172
   133
        line match {
wenzelm@67173
   134
          case Pattern(Value.Int(line), message) => Some((line, message))
wenzelm@67172
   135
          case _ => None
wenzelm@67172
   136
        }
wenzelm@67172
   137
    }
wenzelm@67172
   138
wenzelm@67173
   139
    @tailrec def filter(lines: List[String], result: List[(String, Position.T)])
wenzelm@67173
   140
      : List[(String, Position.T)] =
wenzelm@67173
   141
    {
wenzelm@67172
   142
      lines match {
wenzelm@67173
   143
        case File_Line_Error((file, line, msg1)) :: rest1 =>
wenzelm@67183
   144
          val pos = tex_file_position(file, line)
wenzelm@67172
   145
          rest1 match {
wenzelm@67173
   146
            case Line_Error((line2, msg2)) :: rest2 if line == line2 =>
wenzelm@67173
   147
              filter(rest2, (Exn.cat_message(msg1, msg2), pos) :: result)
wenzelm@67173
   148
            case _ =>
wenzelm@67173
   149
              filter(rest1, (msg1, pos) :: result)
wenzelm@67172
   150
          }
wenzelm@67172
   151
        case _ :: rest => filter(rest, result)
wenzelm@67172
   152
        case Nil => result.reverse
wenzelm@67172
   153
      }
wenzelm@67173
   154
    }
wenzelm@67172
   155
wenzelm@67174
   156
    filter(Line.logical_lines(root_log), Nil)
wenzelm@67173
   157
  }
wenzelm@67172
   158
}