--- 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 ***
--- 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
--- 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
--- 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 *)
--- 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,
--- 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);
--- 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)
+ })
}
--- 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 =
--- 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;
--- 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 *)