1/* Title: Pure/Thy/latex.scala 2 Author: Makarius 3 4Support for LaTeX. 5*/ 6 7package isabelle 8 9 10import java.io.{File => JFile} 11 12import scala.annotation.tailrec 13 14 15object Latex 16{ 17 /** latex errors **/ 18 19 def latex_errors(dir: Path, root_name: String): List[String] = 20 { 21 val root_log_path = dir + Path.explode(root_name).ext("log") 22 if (root_log_path.is_file) { 23 for { (msg, pos) <- filter_errors(dir, File.read(root_log_path)) } 24 yield "Latex error" + Position.here(pos) + ":\n" + cat_lines(split_lines(msg).map(" " + _)) 25 } 26 else Nil 27 } 28 29 30 /* generated .tex file */ 31 32 private val File_Pattern = """^%:%file=(.+)%:%$""".r 33 private val Line_Pattern = """^*%:%(\d+)=(\d+)%:%$""".r 34 35 def read_tex_file(tex_file: Path): Tex_File = 36 { 37 val positions = 38 Line.logical_lines(File.read(tex_file)).reverse. 39 takeWhile(_ != "\\endinput").reverse 40 41 val source_file = 42 positions match { 43 case File_Pattern(file) :: _ => Some(file) 44 case _ => None 45 } 46 47 val source_lines = 48 if (source_file.isEmpty) Nil 49 else 50 positions.flatMap(line => 51 line match { 52 case Line_Pattern(Value.Int(line), Value.Int(source_line)) => Some(line -> source_line) 53 case _ => None 54 }) 55 56 new Tex_File(tex_file, source_file, source_lines) 57 } 58 59 final class Tex_File private[Latex]( 60 tex_file: Path, source_file: Option[String], source_lines: List[(Int, Int)]) 61 { 62 override def toString: String = tex_file.toString 63 64 def source_position(l: Int): Option[Position.T] = 65 source_file match { 66 case None => None 67 case Some(file) => 68 val source_line = 69 (0 /: source_lines.iterator.takeWhile({ case (m, _) => m <= l }))( 70 { case (_, (_, n)) => n }) 71 if (source_line == 0) None else Some(Position.Line_File(source_line, file)) 72 } 73 74 def position(line: Int): Position.T = 75 source_position(line) getOrElse Position.Line_File(line, tex_file.implode) 76 } 77 78 79 /* latex log */ 80 81 def filter_errors(dir: Path, root_log: String): List[(String, Position.T)] = 82 { 83 val seen_files = Synchronized(Map.empty[JFile, Tex_File]) 84 85 def check_tex_file(path: Path): Option[Tex_File] = 86 seen_files.change_result(seen => 87 seen.get(path.file) match { 88 case None => 89 if (path.is_file) { 90 val tex_file = read_tex_file(path) 91 (Some(tex_file), seen + (path.file -> tex_file)) 92 } 93 else (None, seen) 94 case some => (some, seen) 95 }) 96 97 def tex_file_position(path: Path, line: Int): Position.T = 98 check_tex_file(path) match { 99 case Some(tex_file) => tex_file.position(line) 100 case None => Position.Line_File(line, path.implode) 101 } 102 103 object File_Line_Error 104 { 105 val Pattern = """^(.*?\.\w\w\w):(\d+): (.*)$""".r 106 def unapply(line: String): Option[(Path, Int, String)] = 107 line match { 108 case Pattern(file, Value.Int(line), message) => 109 val path = File.standard_path(file) 110 if (Path.is_wellformed(path)) { 111 val file = (dir + Path.explode(path)).canonical 112 val msg = Library.perhaps_unprefix("LaTeX Error: ", message) 113 if (file.is_file) Some((file, line, msg)) else None 114 } 115 else None 116 case _ => None 117 } 118 } 119 120 val Line_Error = """^l\.\d+ (.*)$""".r 121 val More_Error = 122 List( 123 "<argument>", 124 "<template>", 125 "<recently read>", 126 "<to be read again>", 127 "<inserted text>", 128 "<output>", 129 "<everypar>", 130 "<everymath>", 131 "<everydisplay>", 132 "<everyhbox>", 133 "<everyvbox>", 134 "<everyjob>", 135 "<everycr>", 136 "<mark>", 137 "<everyeof>", 138 "<write>").mkString("^(?:", "|", ") (.*)$").r 139 140 val Bad_File = """^! LaTeX Error: (File `.*' not found\.)$""".r 141 142 val error_ignore = 143 Set( 144 "See the LaTeX manual or LaTeX Companion for explanation.", 145 "Type H <return> for immediate help.") 146 147 def error_suffix1(lines: List[String]): Option[String] = 148 { 149 val lines1 = lines.take(20).takeWhile({ case File_Line_Error(_) => false case _ => true }) 150 lines1.zipWithIndex.collectFirst({ 151 case (Line_Error(msg), i) => 152 cat_lines(lines1.take(i).filterNot(error_ignore) ::: List(msg)) }) 153 } 154 def error_suffix2(lines: List[String]): Option[String] = 155 lines match { 156 case More_Error(msg) :: _ => Some(msg) 157 case _ => None 158 } 159 160 @tailrec def filter(lines: List[String], result: List[(String, Position.T)]) 161 : List[(String, Position.T)] = 162 { 163 lines match { 164 case File_Line_Error((file, line, msg1)) :: rest1 => 165 val pos = tex_file_position(file, line) 166 val msg2 = error_suffix1(rest1) orElse error_suffix2(rest1) getOrElse "" 167 filter(rest1, (Exn.cat_message(msg1, msg2), pos) :: result) 168 case Bad_File(msg) :: rest => 169 filter(rest, (msg, Position.none) :: result) 170 case _ :: rest => filter(rest, result) 171 case Nil => result.reverse 172 } 173 } 174 175 filter(Line.logical_lines(root_log), Nil) 176 } 177} 178