# HG changeset patch # User wenzelm # Date 1512912554 -3600 # Node ID e746db6db903732d6425d17300fe402ac58db182 # Parent 97d199699a6bfbfe4867bcc6afead09d78e80704 more explicit latex errors; diff -r 97d199699a6b -r e746db6db903 NEWS --- a/NEWS Fri Dec 08 23:43:58 2017 +0100 +++ b/NEWS Sun Dec 10 14:29:14 2017 +0100 @@ -86,6 +86,8 @@ * Document preparation with skip_proofs option now preserves the content more accurately: only terminal proof steps ('by' etc.) are skipped. +* More explicit errors from latex process. + *** HOL *** diff -r 97d199699a6b -r e746db6db903 etc/settings --- a/etc/settings Fri Dec 08 23:43:58 2017 +0100 +++ b/etc/settings Sun Dec 10 14:29:14 2017 +0100 @@ -46,12 +46,17 @@ ### Document preparation (cf. isabelle latex/document) ### -ISABELLE_LATEX="latex" -ISABELLE_PDFLATEX="pdflatex" +ISABELLE_LATEX="latex -file-line-error" +ISABELLE_PDFLATEX="pdflatex -file-line-error" ISABELLE_BIBTEX="bibtex" ISABELLE_MAKEINDEX="makeindex" ISABELLE_EPSTOPDF="epstopdf" +if [ "$ISABELLE_PLATFORM_FAMILY" = "windows" ]; then + ISABELLE_LATEX="latex -c-style-errors" + ISABELLE_PDFLATEX="pdflatex -c-style-errors" +fi + ### ### Misc path settings diff -r 97d199699a6b -r e746db6db903 lib/Tools/document --- a/lib/Tools/document Fri Dec 08 23:43:58 2017 +0100 +++ b/lib/Tools/document Sun Dec 10 14:29:14 2017 +0100 @@ -137,7 +137,9 @@ RC="$?" fi - if [ "$RC" -eq 0 -a -f "$ROOT_NAME.$OUTFORMAT" ]; then + if [ "$RC" -ne 0 ]; then + isabelle latex_errors -n "$ROOT_NAME" + elif [ -f "$ROOT_NAME.$OUTFORMAT" ]; then cp -f "$ROOT_NAME.$OUTFORMAT" "../$NAME.$OUTFORMAT" fi diff -r 97d199699a6b -r e746db6db903 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Fri Dec 08 23:43:58 2017 +0100 +++ b/src/Pure/PIDE/markup.ML Sun Dec 10 14:29:14 2017 +0100 @@ -54,6 +54,7 @@ val position_properties': string list val position_properties: string list val positionN: string val position: T + val rangeN: string val expressionN: string val expression: string -> T val citationN: string val citation: string -> T val pathN: string val path: string -> T @@ -336,6 +337,8 @@ val (positionN, position) = markup_elem "position"; +val rangeN = "range"; + (* expression *) diff -r 97d199699a6b -r e746db6db903 src/Pure/System/isabelle_tool.scala --- a/src/Pure/System/isabelle_tool.scala Fri Dec 08 23:43:58 2017 +0100 +++ b/src/Pure/System/isabelle_tool.scala Sun Dec 10 14:29:14 2017 +0100 @@ -110,6 +110,7 @@ Check_Sources.isabelle_tool, Doc.isabelle_tool, Imports.isabelle_tool, + Latex.isabelle_tool, Mkroot.isabelle_tool, ML_Process.isabelle_tool, NEWS.isabelle_tool, diff -r 97d199699a6b -r e746db6db903 src/Pure/Thy/latex.ML --- a/src/Pure/Thy/latex.ML Fri Dec 08 23:43:58 2017 +0100 +++ b/src/Pure/Thy/latex.ML Sun Dec 10 14:29:14 2017 +0100 @@ -15,6 +15,9 @@ Symbol.symbol list -> string val output_symbols: Symbol.symbol list -> string val output_syms: string -> string + val output_file: Position.T -> string + val output_range: Position.T -> string + val range_output: Position.T -> string -> string val output_token: Token.T -> string val begin_delim: string -> string val end_delim: string -> string @@ -22,7 +25,7 @@ val end_tag: string -> string val environment: string -> string -> string val tex_trailer: string - val isabelle_theory: string -> string -> string + val isabelle_theory: Position.T -> string -> string -> string val symbol_source: (string -> bool) * (string -> bool) -> string -> Symbol.symbol list -> string val theory_entry: string -> string @@ -170,28 +173,53 @@ end; +(* output properties *) + +fun output_prop (a, b) = enclose "%:%" "%:%\n" (a ^ "=" ^ b); + +fun output_file pos = + (case Position.file_of pos of + NONE => "" + | SOME file => output_prop (Markup.fileN, file)); + +fun output_range pos = + (case (Position.offset_of pos, Position.end_offset_of pos) of + (NONE, _) => "" + | (SOME i, NONE) => output_prop (Markup.rangeN, Value.print_int i) + | (SOME i, SOME j) => output_prop (Markup.rangeN, Value.print_int i ^ ":" ^ Value.print_int j)); + +fun range_output _ "" = "" + | range_output pos output = + (case output_range pos of + "" => output + | range => split_lines output |> map (fn "" => "%\n" | line => line ^ range) |> implode); + + (* output token *) fun output_token tok = - let val s = Token.content_of tok in - if Token.is_kind Token.Comment tok then "" - else if Token.is_command tok then - "\\isacommand{" ^ output_syms s ^ "}" - else if Token.is_kind Token.Keyword tok andalso Symbol.is_ascii_identifier s then - "\\isakeyword{" ^ output_syms s ^ "}" - else if Token.is_kind Token.String tok then - enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s) - else if Token.is_kind Token.Alt_String tok then - enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s) - else if Token.is_kind Token.Verbatim tok then - let - val ants = Antiquote.read (Token.input_of tok); - val out = implode (map output_syms_antiq ants); - in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end - else if Token.is_kind Token.Cartouche tok then - enclose "{\\isacartoucheopen}" "{\\isacartoucheclose}" (output_syms s) - else output_syms s - end handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok)); + let + val s = Token.content_of tok; + val output = + if Token.is_kind Token.Comment tok then "" + else if Token.is_command tok then + "\\isacommand{" ^ output_syms s ^ "}" + else if Token.is_kind Token.Keyword tok andalso Symbol.is_ascii_identifier s then + "\\isakeyword{" ^ output_syms s ^ "}" + else if Token.is_kind Token.String tok then + enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s) + else if Token.is_kind Token.Alt_String tok then + enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s) + else if Token.is_kind Token.Verbatim tok then + let + val ants = Antiquote.read (Token.input_of tok); + val out = implode (map output_syms_antiq ants); + in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end + else if Token.is_kind Token.Cartouche tok then + enclose "{\\isacartoucheopen}" "{\\isacartoucheclose}" (output_syms s) + else output_syms s; + in range_output (Token.pos_of tok) output end + handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok)); (* tags *) @@ -213,13 +241,14 @@ \%%% TeX-master: \"root\"\n\ \%%% End:\n"; -fun isabelle_theory name txt = - "%\n\\begin{isabellebody}%\n\ +fun isabelle_theory pos name txt = + output_file pos ^ + "\\begin{isabellebody}%\n\ \\\setisabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^ "%\n\\end{isabellebody}%\n" ^ tex_trailer; fun symbol_source known name syms = - isabelle_theory name + isabelle_theory Position.none name ("\\isamarkupfile{" ^ output_known_symbols known (Symbol.explode name) ^ "}%\n" ^ output_known_symbols known syms); diff -r 97d199699a6b -r e746db6db903 src/Pure/Thy/latex.scala --- a/src/Pure/Thy/latex.scala Fri Dec 08 23:43:58 2017 +0100 +++ b/src/Pure/Thy/latex.scala Sun Dec 10 14:29:14 2017 +0100 @@ -7,25 +7,108 @@ package isabelle +import java.io.{File => JFile} + import scala.annotation.tailrec object Latex { - sealed case class Error(file: Option[Path], line: Int, message: String) + /** latex errors **/ + + /* generated .tex file */ + + private val File_Pattern = """^.*%:%file=(.+)%:%$""".r + private val Range_Pattern2 = """^.*%:%range=(\d+):(\d+)%:%$""".r + private val Range_Pattern1 = """^.*%:%range=(\d+)%:%$""".r + + def read_tex_file(tex_file: Path): Tex_File = + new Tex_File(tex_file, split_lines(File.read(tex_file)).toArray) + + final class Tex_File private[Latex](val tex_file: Path, tex_lines: Array[String]) + { + override def toString: String = tex_file.toString + + val source_file: Option[Path] = + if (tex_lines.length > 0) { + tex_lines(0) match { + case File_Pattern(file) if Path.is_wellformed(file) && Path.explode(file).is_file => + Some(Path.explode(file)) + case _ => None + } + } + else None + + val source_content: Line.Document = + source_file match { + case Some(file) => Line.Document(Symbol.decode(File.read(file))) + case None => Line.Document.empty + } + + lazy val source_chunk: Symbol.Text_Chunk = + Symbol.Text_Chunk(source_content.text) - def filter_errors(dir: Path, text: String): List[Error] = + def source_position(l: Int): Option[Position.T] = + for { + file <- source_file + if 0 < l && l <= tex_lines.length + line = tex_lines(l - 1) + if line.endsWith("%:%") + symbol_range <- + (line match { + case Range_Pattern2(Value.Int(i), Value.Int(j)) => Some(Text.Range(i, j)) + case Range_Pattern1(Value.Int(i)) => Some(Text.Range(i, i + 1)) + case _ => None + }) + range <- source_chunk.incorporate(symbol_range) + } + yield { + Position.Line_File(source_content.position(range.start).line1, file.implode) ::: + Position.Range(symbol_range) + } + + def tex_position(line: Int): Position.T = + Position.File(tex_file.implode) ::: Position.Line(line) + + def position(line: Int): Position.T = + source_position(line) getOrElse tex_position(line) + } + + + /* latex log */ + + def filter_errors(dir: Path, root_log: String): List[(String, Position.T)] = { + val seen_files = Synchronized(Map.empty[JFile, Tex_File]) + + def check_tex_file(path: Path): Option[Tex_File] = + seen_files.change_result(seen => + seen.get(path.file) match { + case None => + if (path.is_file) { + val tex_file = read_tex_file(path) + (Some(tex_file), seen + (path.file -> tex_file)) + } + else (None, seen) + case some => (some, seen) + }) + + def tex_file_position(path: Path, line: Int): Position.T = + check_tex_file(path) match { + case Some(tex_file) => tex_file.position(line) + case None => Position.Line_File(line, path.implode) + } + object File_Line_Error { val Pattern = """^(.*):(\d+): (.*)$""".r - def unapply(line: String): Option[Error] = + def unapply(line: String): Option[(Path, Int, String)] = line match { case Pattern(file, Value.Int(line), message) => val path = File.standard_path(file) if (Path.is_wellformed(path)) { - val file = Path.explode(path) - if ((dir + file).is_file) Some(Error(Some(file), line, message)) else None + val file = dir + Path.explode(path) + if (file.is_file) Some((file, line, message)) else None } else None case _ => None @@ -35,26 +118,75 @@ object Line_Error { val Pattern = """^l\.(\d+) (.*)$""".r - def unapply(line: String): Option[Error] = + def unapply(line: String): Option[(Int, String)] = line match { - case Pattern(Value.Int(line), message) => Some(Error(None, line, message)) + case Pattern(Value.Int(line), message) => Some((line, message)) case _ => None } } - @tailrec def filter(lines: List[String], result: List[Error]): List[Error] = + @tailrec def filter(lines: List[String], result: List[(String, Position.T)]) + : List[(String, Position.T)] = + { lines match { - case File_Line_Error(err1) :: rest1 => + case File_Line_Error((file, line, msg1)) :: rest1 => + val pos = tex_file_position(file, line) rest1 match { - case Line_Error(err2) :: rest2 if err1.line == err2.line => - val err = err1.copy(message = Exn.cat_message(err1.message, err2.message)) - filter(rest2, err :: result) - case _ => filter(rest1, err1 :: result) + case Line_Error((line2, msg2)) :: rest2 if line == line2 => + filter(rest2, (Exn.cat_message(msg1, msg2), pos) :: result) + case _ => + filter(rest1, (msg1, pos) :: result) } case _ :: rest => filter(rest, result) case Nil => result.reverse } + } - filter(split_lines(text), Nil) + filter(split_lines(root_log), Nil) + } + + + /* errors */ + + val default_root_name: String = "root" + + def latex_errors(dir: Path = Path.current, root_name: String = default_root_name) + { + val root_log_path = dir + Path.explode(root_name).ext("log") + val errors = + if (root_log_path.is_file) { + for { (msg, pos) <- filter_errors(dir, File.read(root_log_path)) } + yield "Latex error" + Position.here(pos) + ":\n" + cat_lines(split_lines(msg).map(" " + _)) + } + else Nil + if (errors.nonEmpty) Output.writeln(cat_lines(errors)) } + + + /* Isabelle tool wrapper */ + + val isabelle_tool = + Isabelle_Tool("latex_errors", "print latex errors for Isabelle document output", args => + { + var dir = Path.current + var root_name = default_root_name + + val getopts = Getopts(""" +Usage: isabelle latex_errors + + Options are: + -d DIR alternative document directory (default: current) + -n NAME alternative root name (default: """ + quote(default_root_name) + """) + + Print latex errors for Isabelle document output directory (with root.tex, + root.log etc.). +""", + "d:" -> (arg => dir = Path.explode(arg)), + "n:" -> (arg => root_name = arg)) + + val more_args = getopts(args) + if (more_args.nonEmpty) getopts.usage() + + latex_errors(dir = dir, root_name = root_name) + }) } diff -r 97d199699a6b -r e746db6db903 src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Fri Dec 08 23:43:58 2017 +0100 +++ b/src/Pure/Thy/present.ML Sun Dec 10 14:29:14 2017 +0100 @@ -12,7 +12,7 @@ val init: HTML.symbols -> bool -> bool -> Path.T -> string -> string -> (string * string) list -> (Path.T * Path.T) list -> Path.T -> string * string -> bool -> unit val finish: unit -> unit - val theory_output: theory -> string -> unit + val theory_output: Position.T -> theory -> string -> unit val begin_theory: int -> (unit -> HTML.text) -> theory -> theory val display_drafts: Path.T list -> int end; @@ -191,14 +191,14 @@ fun isabelle_document {verbose, purge} format name tags dir = let val s = "isabelle document -o '" ^ format ^ "' \ - \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.bash_path dir ^ " 2>&1"; + \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.bash_path dir; val doc_path = Path.appends [dir, Path.parent, Path.basic name |> Path.ext format]; val _ = if verbose then writeln s else (); - val (out, rc) = Isabelle_System.bash_output s; + val {out, err, rc, ...} = Bash.process s; + val _ = if verbose then writeln out else (); val _ = if not (File.exists doc_path) orelse rc <> 0 then - cat_error out ("Failed to build document " ^ quote (show_path doc_path)) - else if verbose then writeln out + cat_error err ("Failed to build document " ^ quote (show_path doc_path)) else (); val _ = if purge andalso rc = 0 then Isabelle_System.rm_tree dir else (); in doc_path end; @@ -279,11 +279,11 @@ (* theory elements *) -fun theory_output thy tex = +fun theory_output pos thy tex = with_session_info () (fn _ => if is_session_theory thy then let val name = Context.theory_name thy; - in change_theory_info name (fn (_, html) => (Latex.isabelle_theory name tex, html)) end + in change_theory_info name (fn (_, html) => (Latex.isabelle_theory pos name tex, html)) end else ()); fun theory_link (curr_chapter, curr_session) thy = diff -r 97d199699a6b -r e746db6db903 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Fri Dec 08 23:43:58 2017 +0100 +++ b/src/Pure/Thy/thy_info.ML Sun Dec 10 14:29:14 2017 +0100 @@ -269,7 +269,7 @@ if exists (Toplevel.is_skipped_proof o #2) res then () else let val tex_source = Thy_Output.present_thy thy res toks |> Buffer.content; - in if document then Present.theory_output thy tex_source else () end + in if document then Present.theory_output text_pos thy tex_source else () end end; in (thy, present, size text) end; diff -r 97d199699a6b -r e746db6db903 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Fri Dec 08 23:43:58 2017 +0100 +++ b/src/Pure/Thy/thy_output.ML Sun Dec 10 14:29:14 2017 +0100 @@ -218,23 +218,24 @@ and output_block (Markdown.Par lines) = cat_lines (map output_line lines) | output_block (Markdown.List {kind, body, ...}) = Latex.environment (Markdown.print_kind kind) (output_blocks body); - in - if Toplevel.is_skipped_proof state then "" - else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms - then - let - val ants = Antiquote.parse pos syms; - val reports = Antiquote.antiq_reports ants; - val blocks = Markdown.read_antiquotes ants; - val _ = if is_reported then Position.reports (reports @ Markdown.reports blocks) else (); - in output_blocks blocks end - else - let - val ants = Antiquote.parse pos (Symbol_Pos.trim_blanks syms); - val reports = Antiquote.antiq_reports ants; - val _ = if is_reported then Position.reports (reports @ Markdown.text_reports ants) else (); - in output_antiquotes ants end - end; + + val output = + if Toplevel.is_skipped_proof state then "" + else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms + then + let + val ants = Antiquote.parse pos syms; + val reports = Antiquote.antiq_reports ants; + val blocks = Markdown.read_antiquotes ants; + val _ = if is_reported then Position.reports (reports @ Markdown.reports blocks) else (); + in output_blocks blocks end + else + let + val ants = Antiquote.parse pos (Symbol_Pos.trim_blanks syms); + val reports = Antiquote.antiq_reports ants; + val _ = if is_reported then Position.reports (reports @ Markdown.text_reports ants) else (); + in output_antiquotes ants end; + in Latex.range_output pos output end; @@ -271,7 +272,8 @@ | Markup_Env_Token (cmd, source) => Latex.environment ("isamarkup" ^ cmd) (output_text state {markdown = true} source) | Raw_Token source => - "%\n" ^ output_text state {markdown = true} source ^ "\n"); + let val output = "%\n" ^ output_text state {markdown = true} source + in if String.isSuffix "\n" output then output else output ^ "\n" end); (* command spans *)