more explicit latex errors;
authorwenzelm
Sun Dec 10 14:29:14 2017 +0100 (17 months ago)
changeset 67173e746db6db903
parent 67172 97d199699a6b
child 67174 258e1394e76a
more explicit latex errors;
NEWS
etc/settings
lib/Tools/document
src/Pure/PIDE/markup.ML
src/Pure/System/isabelle_tool.scala
src/Pure/Thy/latex.ML
src/Pure/Thy/latex.scala
src/Pure/Thy/present.ML
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/NEWS	Fri Dec 08 23:43:58 2017 +0100
     1.2 +++ b/NEWS	Sun Dec 10 14:29:14 2017 +0100
     1.3 @@ -86,6 +86,8 @@
     1.4  * Document preparation with skip_proofs option now preserves the content
     1.5  more accurately: only terminal proof steps ('by' etc.) are skipped.
     1.6  
     1.7 +* More explicit errors from latex process.
     1.8 +
     1.9  
    1.10  *** HOL ***
    1.11  
     2.1 --- a/etc/settings	Fri Dec 08 23:43:58 2017 +0100
     2.2 +++ b/etc/settings	Sun Dec 10 14:29:14 2017 +0100
     2.3 @@ -46,12 +46,17 @@
     2.4  ### Document preparation (cf. isabelle latex/document)
     2.5  ###
     2.6  
     2.7 -ISABELLE_LATEX="latex"
     2.8 -ISABELLE_PDFLATEX="pdflatex"
     2.9 +ISABELLE_LATEX="latex -file-line-error"
    2.10 +ISABELLE_PDFLATEX="pdflatex -file-line-error"
    2.11  ISABELLE_BIBTEX="bibtex"
    2.12  ISABELLE_MAKEINDEX="makeindex"
    2.13  ISABELLE_EPSTOPDF="epstopdf"
    2.14  
    2.15 +if [ "$ISABELLE_PLATFORM_FAMILY" = "windows" ]; then
    2.16 +  ISABELLE_LATEX="latex -c-style-errors"
    2.17 +  ISABELLE_PDFLATEX="pdflatex -c-style-errors"
    2.18 +fi
    2.19 +
    2.20  
    2.21  ###
    2.22  ### Misc path settings
     3.1 --- a/lib/Tools/document	Fri Dec 08 23:43:58 2017 +0100
     3.2 +++ b/lib/Tools/document	Sun Dec 10 14:29:14 2017 +0100
     3.3 @@ -137,7 +137,9 @@
     3.4      RC="$?"
     3.5    fi
     3.6  
     3.7 -  if [ "$RC" -eq 0 -a -f "$ROOT_NAME.$OUTFORMAT" ]; then
     3.8 +  if [ "$RC" -ne 0 ]; then
     3.9 +    isabelle latex_errors -n "$ROOT_NAME"
    3.10 +  elif [ -f "$ROOT_NAME.$OUTFORMAT" ]; then
    3.11      cp -f "$ROOT_NAME.$OUTFORMAT" "../$NAME.$OUTFORMAT"
    3.12    fi
    3.13  
     4.1 --- a/src/Pure/PIDE/markup.ML	Fri Dec 08 23:43:58 2017 +0100
     4.2 +++ b/src/Pure/PIDE/markup.ML	Sun Dec 10 14:29:14 2017 +0100
     4.3 @@ -54,6 +54,7 @@
     4.4    val position_properties': string list
     4.5    val position_properties: string list
     4.6    val positionN: string val position: T
     4.7 +  val rangeN: string
     4.8    val expressionN: string val expression: string -> T
     4.9    val citationN: string val citation: string -> T
    4.10    val pathN: string val path: string -> T
    4.11 @@ -336,6 +337,8 @@
    4.12  
    4.13  val (positionN, position) = markup_elem "position";
    4.14  
    4.15 +val rangeN = "range";
    4.16 +
    4.17  
    4.18  (* expression *)
    4.19  
     5.1 --- a/src/Pure/System/isabelle_tool.scala	Fri Dec 08 23:43:58 2017 +0100
     5.2 +++ b/src/Pure/System/isabelle_tool.scala	Sun Dec 10 14:29:14 2017 +0100
     5.3 @@ -110,6 +110,7 @@
     5.4        Check_Sources.isabelle_tool,
     5.5        Doc.isabelle_tool,
     5.6        Imports.isabelle_tool,
     5.7 +      Latex.isabelle_tool,
     5.8        Mkroot.isabelle_tool,
     5.9        ML_Process.isabelle_tool,
    5.10        NEWS.isabelle_tool,
     6.1 --- a/src/Pure/Thy/latex.ML	Fri Dec 08 23:43:58 2017 +0100
     6.2 +++ b/src/Pure/Thy/latex.ML	Sun Dec 10 14:29:14 2017 +0100
     6.3 @@ -15,6 +15,9 @@
     6.4      Symbol.symbol list -> string
     6.5    val output_symbols: Symbol.symbol list -> string
     6.6    val output_syms: string -> string
     6.7 +  val output_file: Position.T -> string
     6.8 +  val output_range: Position.T -> string
     6.9 +  val range_output: Position.T -> string -> string
    6.10    val output_token: Token.T -> string
    6.11    val begin_delim: string -> string
    6.12    val end_delim: string -> string
    6.13 @@ -22,7 +25,7 @@
    6.14    val end_tag: string -> string
    6.15    val environment: string -> string -> string
    6.16    val tex_trailer: string
    6.17 -  val isabelle_theory: string -> string -> string
    6.18 +  val isabelle_theory: Position.T -> string -> string -> string
    6.19    val symbol_source: (string -> bool) * (string -> bool) ->
    6.20      string -> Symbol.symbol list -> string
    6.21    val theory_entry: string -> string
    6.22 @@ -170,28 +173,53 @@
    6.23  end;
    6.24  
    6.25  
    6.26 +(* output properties *)
    6.27 +
    6.28 +fun output_prop (a, b) = enclose "%:%" "%:%\n" (a ^ "=" ^ b);
    6.29 +
    6.30 +fun output_file pos =
    6.31 +  (case Position.file_of pos of
    6.32 +    NONE => ""
    6.33 +  | SOME file => output_prop (Markup.fileN, file));
    6.34 +
    6.35 +fun output_range pos =
    6.36 +  (case (Position.offset_of pos, Position.end_offset_of pos) of
    6.37 +    (NONE, _) => ""
    6.38 +  | (SOME i, NONE) => output_prop (Markup.rangeN, Value.print_int i)
    6.39 +  | (SOME i, SOME j) => output_prop (Markup.rangeN, Value.print_int i ^ ":" ^ Value.print_int j));
    6.40 +
    6.41 +fun range_output _ "" = ""
    6.42 +  | range_output pos output =
    6.43 +      (case output_range pos of
    6.44 +        "" => output
    6.45 +      | range => split_lines output |> map (fn "" => "%\n" | line => line ^ range) |> implode);
    6.46 +
    6.47 +
    6.48  (* output token *)
    6.49  
    6.50  fun output_token tok =
    6.51 -  let val s = Token.content_of tok in
    6.52 -    if Token.is_kind Token.Comment tok then ""
    6.53 -    else if Token.is_command tok then
    6.54 -      "\\isacommand{" ^ output_syms s ^ "}"
    6.55 -    else if Token.is_kind Token.Keyword tok andalso Symbol.is_ascii_identifier s then
    6.56 -      "\\isakeyword{" ^ output_syms s ^ "}"
    6.57 -    else if Token.is_kind Token.String tok then
    6.58 -      enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s)
    6.59 -    else if Token.is_kind Token.Alt_String tok then
    6.60 -      enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
    6.61 -    else if Token.is_kind Token.Verbatim tok then
    6.62 -      let
    6.63 -        val ants = Antiquote.read (Token.input_of tok);
    6.64 -        val out = implode (map output_syms_antiq ants);
    6.65 -      in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
    6.66 -    else if Token.is_kind Token.Cartouche tok then
    6.67 -      enclose "{\\isacartoucheopen}" "{\\isacartoucheclose}" (output_syms s)
    6.68 -    else output_syms s
    6.69 -  end handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok));
    6.70 +  let
    6.71 +    val s = Token.content_of tok;
    6.72 +    val output =
    6.73 +      if Token.is_kind Token.Comment tok then ""
    6.74 +      else if Token.is_command tok then
    6.75 +        "\\isacommand{" ^ output_syms s ^ "}"
    6.76 +      else if Token.is_kind Token.Keyword tok andalso Symbol.is_ascii_identifier s then
    6.77 +        "\\isakeyword{" ^ output_syms s ^ "}"
    6.78 +      else if Token.is_kind Token.String tok then
    6.79 +        enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s)
    6.80 +      else if Token.is_kind Token.Alt_String tok then
    6.81 +        enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
    6.82 +      else if Token.is_kind Token.Verbatim tok then
    6.83 +        let
    6.84 +          val ants = Antiquote.read (Token.input_of tok);
    6.85 +          val out = implode (map output_syms_antiq ants);
    6.86 +        in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
    6.87 +      else if Token.is_kind Token.Cartouche tok then
    6.88 +        enclose "{\\isacartoucheopen}" "{\\isacartoucheclose}" (output_syms s)
    6.89 +      else output_syms s;
    6.90 +  in range_output (Token.pos_of tok) output end
    6.91 +  handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok));
    6.92  
    6.93  
    6.94  (* tags *)
    6.95 @@ -213,13 +241,14 @@
    6.96    \%%% TeX-master: \"root\"\n\
    6.97    \%%% End:\n";
    6.98  
    6.99 -fun isabelle_theory name txt =
   6.100 -  "%\n\\begin{isabellebody}%\n\
   6.101 +fun isabelle_theory pos name txt =
   6.102 +  output_file pos ^
   6.103 +  "\\begin{isabellebody}%\n\
   6.104    \\\setisabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^
   6.105    "%\n\\end{isabellebody}%\n" ^ tex_trailer;
   6.106  
   6.107  fun symbol_source known name syms =
   6.108 -  isabelle_theory name
   6.109 +  isabelle_theory Position.none name
   6.110      ("\\isamarkupfile{" ^ output_known_symbols known (Symbol.explode name) ^ "}%\n" ^
   6.111        output_known_symbols known syms);
   6.112  
     7.1 --- a/src/Pure/Thy/latex.scala	Fri Dec 08 23:43:58 2017 +0100
     7.2 +++ b/src/Pure/Thy/latex.scala	Sun Dec 10 14:29:14 2017 +0100
     7.3 @@ -7,25 +7,108 @@
     7.4  package isabelle
     7.5  
     7.6  
     7.7 +import java.io.{File => JFile}
     7.8 +
     7.9  import scala.annotation.tailrec
    7.10  
    7.11  
    7.12  object Latex
    7.13  {
    7.14 -  sealed case class Error(file: Option[Path], line: Int, message: String)
    7.15 +  /** latex errors **/
    7.16 +
    7.17 +  /* generated .tex file */
    7.18 +
    7.19 +  private val File_Pattern = """^.*%:%file=(.+)%:%$""".r
    7.20 +  private val Range_Pattern2 = """^.*%:%range=(\d+):(\d+)%:%$""".r
    7.21 +  private val Range_Pattern1 = """^.*%:%range=(\d+)%:%$""".r
    7.22 +
    7.23 +  def read_tex_file(tex_file: Path): Tex_File =
    7.24 +    new Tex_File(tex_file, split_lines(File.read(tex_file)).toArray)
    7.25 +
    7.26 +  final class Tex_File private[Latex](val tex_file: Path, tex_lines: Array[String])
    7.27 +  {
    7.28 +    override def toString: String = tex_file.toString
    7.29 +
    7.30 +    val source_file: Option[Path] =
    7.31 +      if (tex_lines.length > 0) {
    7.32 +        tex_lines(0) match {
    7.33 +          case File_Pattern(file) if Path.is_wellformed(file) && Path.explode(file).is_file =>
    7.34 +            Some(Path.explode(file))
    7.35 +          case _ => None
    7.36 +        }
    7.37 +      }
    7.38 +      else None
    7.39 +
    7.40 +    val source_content: Line.Document =
    7.41 +      source_file match {
    7.42 +        case Some(file) => Line.Document(Symbol.decode(File.read(file)))
    7.43 +        case None => Line.Document.empty
    7.44 +      }
    7.45 +
    7.46 +    lazy val source_chunk: Symbol.Text_Chunk =
    7.47 +      Symbol.Text_Chunk(source_content.text)
    7.48  
    7.49 -  def filter_errors(dir: Path, text: String): List[Error] =
    7.50 +    def source_position(l: Int): Option[Position.T] =
    7.51 +      for {
    7.52 +        file <- source_file
    7.53 +        if 0 < l && l <= tex_lines.length
    7.54 +        line = tex_lines(l - 1)
    7.55 +        if line.endsWith("%:%")
    7.56 +        symbol_range <-
    7.57 +          (line match {
    7.58 +            case Range_Pattern2(Value.Int(i), Value.Int(j)) => Some(Text.Range(i, j))
    7.59 +            case Range_Pattern1(Value.Int(i)) => Some(Text.Range(i, i + 1))
    7.60 +            case _ => None
    7.61 +          })
    7.62 +        range <- source_chunk.incorporate(symbol_range)
    7.63 +      }
    7.64 +      yield {
    7.65 +        Position.Line_File(source_content.position(range.start).line1, file.implode) :::
    7.66 +        Position.Range(symbol_range)
    7.67 +      }
    7.68 +
    7.69 +    def tex_position(line: Int): Position.T =
    7.70 +      Position.File(tex_file.implode) ::: Position.Line(line)
    7.71 +
    7.72 +    def position(line: Int): Position.T =
    7.73 +      source_position(line) getOrElse tex_position(line)
    7.74 +  }
    7.75 +
    7.76 +
    7.77 +  /* latex log */
    7.78 +
    7.79 +  def filter_errors(dir: Path, root_log: String): List[(String, Position.T)] =
    7.80    {
    7.81 +    val seen_files = Synchronized(Map.empty[JFile, Tex_File])
    7.82 +
    7.83 +    def check_tex_file(path: Path): Option[Tex_File] =
    7.84 +      seen_files.change_result(seen =>
    7.85 +        seen.get(path.file) match {
    7.86 +          case None =>
    7.87 +            if (path.is_file) {
    7.88 +              val tex_file = read_tex_file(path)
    7.89 +              (Some(tex_file), seen + (path.file -> tex_file))
    7.90 +            }
    7.91 +            else (None, seen)
    7.92 +          case some => (some, seen)
    7.93 +        })
    7.94 +
    7.95 +    def tex_file_position(path: Path, line: Int): Position.T =
    7.96 +      check_tex_file(path) match {
    7.97 +        case Some(tex_file) => tex_file.position(line)
    7.98 +        case None => Position.Line_File(line, path.implode)
    7.99 +      }
   7.100 +
   7.101      object File_Line_Error
   7.102      {
   7.103        val Pattern = """^(.*):(\d+): (.*)$""".r
   7.104 -      def unapply(line: String): Option[Error] =
   7.105 +      def unapply(line: String): Option[(Path, Int, String)] =
   7.106          line match {
   7.107            case Pattern(file, Value.Int(line), message) =>
   7.108              val path = File.standard_path(file)
   7.109              if (Path.is_wellformed(path)) {
   7.110 -              val file = Path.explode(path)
   7.111 -              if ((dir + file).is_file) Some(Error(Some(file), line, message)) else None
   7.112 +              val file = dir + Path.explode(path)
   7.113 +              if (file.is_file) Some((file, line, message)) else None
   7.114              }
   7.115              else None
   7.116            case _ => None
   7.117 @@ -35,26 +118,75 @@
   7.118      object Line_Error
   7.119      {
   7.120        val Pattern = """^l\.(\d+) (.*)$""".r
   7.121 -      def unapply(line: String): Option[Error] =
   7.122 +      def unapply(line: String): Option[(Int, String)] =
   7.123          line match {
   7.124 -          case Pattern(Value.Int(line), message) => Some(Error(None, line, message))
   7.125 +          case Pattern(Value.Int(line), message) => Some((line, message))
   7.126            case _ => None
   7.127          }
   7.128      }
   7.129  
   7.130 -    @tailrec def filter(lines: List[String], result: List[Error]): List[Error] =
   7.131 +    @tailrec def filter(lines: List[String], result: List[(String, Position.T)])
   7.132 +      : List[(String, Position.T)] =
   7.133 +    {
   7.134        lines match {
   7.135 -        case File_Line_Error(err1) :: rest1 =>
   7.136 +        case File_Line_Error((file, line, msg1)) :: rest1 =>
   7.137 +          val pos = tex_file_position(file, line)
   7.138            rest1 match {
   7.139 -            case Line_Error(err2) :: rest2 if err1.line == err2.line =>
   7.140 -              val err = err1.copy(message = Exn.cat_message(err1.message, err2.message))
   7.141 -              filter(rest2, err :: result)
   7.142 -            case _ => filter(rest1, err1 :: result)
   7.143 +            case Line_Error((line2, msg2)) :: rest2 if line == line2 =>
   7.144 +              filter(rest2, (Exn.cat_message(msg1, msg2), pos) :: result)
   7.145 +            case _ =>
   7.146 +              filter(rest1, (msg1, pos) :: result)
   7.147            }
   7.148          case _ :: rest => filter(rest, result)
   7.149          case Nil => result.reverse
   7.150        }
   7.151 +    }
   7.152  
   7.153 -    filter(split_lines(text), Nil)
   7.154 +    filter(split_lines(root_log), Nil)
   7.155 +  }
   7.156 +
   7.157 +
   7.158 +  /* errors */
   7.159 +
   7.160 +  val default_root_name: String = "root"
   7.161 +
   7.162 +  def latex_errors(dir: Path = Path.current, root_name: String = default_root_name)
   7.163 +  {
   7.164 +    val root_log_path = dir + Path.explode(root_name).ext("log")
   7.165 +    val errors =
   7.166 +      if (root_log_path.is_file) {
   7.167 +        for { (msg, pos) <- filter_errors(dir, File.read(root_log_path)) }
   7.168 +        yield "Latex error" + Position.here(pos) + ":\n" + cat_lines(split_lines(msg).map("  " + _))
   7.169 +      }
   7.170 +      else Nil
   7.171 +    if (errors.nonEmpty) Output.writeln(cat_lines(errors))
   7.172    }
   7.173 +
   7.174 +
   7.175 +  /* Isabelle tool wrapper */
   7.176 +
   7.177 +  val isabelle_tool =
   7.178 +    Isabelle_Tool("latex_errors", "print latex errors for Isabelle document output", args =>
   7.179 +  {
   7.180 +    var dir = Path.current
   7.181 +    var root_name = default_root_name
   7.182 +
   7.183 +    val getopts = Getopts("""
   7.184 +Usage: isabelle latex_errors
   7.185 +
   7.186 +  Options are:
   7.187 +    -d DIR       alternative document directory (default: current)
   7.188 +    -n NAME      alternative root name (default: """ + quote(default_root_name) + """)
   7.189 +
   7.190 +  Print latex errors for Isabelle document output directory (with root.tex,
   7.191 +  root.log etc.).
   7.192 +""",
   7.193 +      "d:" -> (arg => dir = Path.explode(arg)),
   7.194 +      "n:" -> (arg => root_name = arg))
   7.195 +
   7.196 +    val more_args = getopts(args)
   7.197 +    if (more_args.nonEmpty) getopts.usage()
   7.198 +
   7.199 +    latex_errors(dir = dir, root_name = root_name)
   7.200 +  })
   7.201  }
     8.1 --- a/src/Pure/Thy/present.ML	Fri Dec 08 23:43:58 2017 +0100
     8.2 +++ b/src/Pure/Thy/present.ML	Sun Dec 10 14:29:14 2017 +0100
     8.3 @@ -12,7 +12,7 @@
     8.4    val init: HTML.symbols -> bool -> bool -> Path.T -> string -> string -> (string * string) list ->
     8.5      (Path.T * Path.T) list -> Path.T -> string * string -> bool -> unit
     8.6    val finish: unit -> unit
     8.7 -  val theory_output: theory -> string -> unit
     8.8 +  val theory_output: Position.T -> theory -> string -> unit
     8.9    val begin_theory: int -> (unit -> HTML.text) -> theory -> theory
    8.10    val display_drafts: Path.T list -> int
    8.11  end;
    8.12 @@ -191,14 +191,14 @@
    8.13  fun isabelle_document {verbose, purge} format name tags dir =
    8.14    let
    8.15      val s = "isabelle document -o '" ^ format ^ "' \
    8.16 -      \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.bash_path dir ^ " 2>&1";
    8.17 +      \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.bash_path dir;
    8.18      val doc_path = Path.appends [dir, Path.parent, Path.basic name |> Path.ext format];
    8.19      val _ = if verbose then writeln s else ();
    8.20 -    val (out, rc) = Isabelle_System.bash_output s;
    8.21 +    val {out, err, rc, ...} = Bash.process s;
    8.22 +    val _ = if verbose then writeln out else ();
    8.23      val _ =
    8.24        if not (File.exists doc_path) orelse rc <> 0 then
    8.25 -        cat_error out ("Failed to build document " ^ quote (show_path doc_path))
    8.26 -      else if verbose then writeln out
    8.27 +        cat_error err ("Failed to build document " ^ quote (show_path doc_path))
    8.28        else ();
    8.29      val _ = if purge andalso rc = 0 then Isabelle_System.rm_tree dir else ();
    8.30    in doc_path end;
    8.31 @@ -279,11 +279,11 @@
    8.32  
    8.33  (* theory elements *)
    8.34  
    8.35 -fun theory_output thy tex =
    8.36 +fun theory_output pos thy tex =
    8.37    with_session_info () (fn _ =>
    8.38      if is_session_theory thy then
    8.39        let val name = Context.theory_name thy;
    8.40 -      in change_theory_info name (fn (_, html) => (Latex.isabelle_theory name tex, html)) end
    8.41 +      in change_theory_info name (fn (_, html) => (Latex.isabelle_theory pos name tex, html)) end
    8.42      else ());
    8.43  
    8.44  fun theory_link (curr_chapter, curr_session) thy =
     9.1 --- a/src/Pure/Thy/thy_info.ML	Fri Dec 08 23:43:58 2017 +0100
     9.2 +++ b/src/Pure/Thy/thy_info.ML	Sun Dec 10 14:29:14 2017 +0100
     9.3 @@ -269,7 +269,7 @@
     9.4          if exists (Toplevel.is_skipped_proof o #2) res then ()
     9.5          else
     9.6            let val tex_source = Thy_Output.present_thy thy res toks |> Buffer.content;
     9.7 -          in if document then Present.theory_output thy tex_source else () end
     9.8 +          in if document then Present.theory_output text_pos thy tex_source else () end
     9.9        end;
    9.10  
    9.11    in (thy, present, size text) end;
    10.1 --- a/src/Pure/Thy/thy_output.ML	Fri Dec 08 23:43:58 2017 +0100
    10.2 +++ b/src/Pure/Thy/thy_output.ML	Sun Dec 10 14:29:14 2017 +0100
    10.3 @@ -218,23 +218,24 @@
    10.4      and output_block (Markdown.Par lines) = cat_lines (map output_line lines)
    10.5        | output_block (Markdown.List {kind, body, ...}) =
    10.6            Latex.environment (Markdown.print_kind kind) (output_blocks body);
    10.7 -  in
    10.8 -    if Toplevel.is_skipped_proof state then ""
    10.9 -    else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms
   10.10 -    then
   10.11 -      let
   10.12 -        val ants = Antiquote.parse pos syms;
   10.13 -        val reports = Antiquote.antiq_reports ants;
   10.14 -        val blocks = Markdown.read_antiquotes ants;
   10.15 -        val _ = if is_reported then Position.reports (reports @ Markdown.reports blocks) else ();
   10.16 -      in output_blocks blocks end
   10.17 -    else
   10.18 -      let
   10.19 -        val ants = Antiquote.parse pos (Symbol_Pos.trim_blanks syms);
   10.20 -        val reports = Antiquote.antiq_reports ants;
   10.21 -        val _ = if is_reported then Position.reports (reports @ Markdown.text_reports ants) else ();
   10.22 -      in output_antiquotes ants end
   10.23 -  end;
   10.24 +
   10.25 +    val output =
   10.26 +      if Toplevel.is_skipped_proof state then ""
   10.27 +      else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms
   10.28 +      then
   10.29 +        let
   10.30 +          val ants = Antiquote.parse pos syms;
   10.31 +          val reports = Antiquote.antiq_reports ants;
   10.32 +          val blocks = Markdown.read_antiquotes ants;
   10.33 +          val _ = if is_reported then Position.reports (reports @ Markdown.reports blocks) else ();
   10.34 +        in output_blocks blocks end
   10.35 +      else
   10.36 +        let
   10.37 +          val ants = Antiquote.parse pos (Symbol_Pos.trim_blanks syms);
   10.38 +          val reports = Antiquote.antiq_reports ants;
   10.39 +          val _ = if is_reported then Position.reports (reports @ Markdown.text_reports ants) else ();
   10.40 +        in output_antiquotes ants end;
   10.41 +  in Latex.range_output pos output end;
   10.42  
   10.43  
   10.44  
   10.45 @@ -271,7 +272,8 @@
   10.46    | Markup_Env_Token (cmd, source) =>
   10.47        Latex.environment ("isamarkup" ^ cmd) (output_text state {markdown = true} source)
   10.48    | Raw_Token source =>
   10.49 -      "%\n" ^ output_text state {markdown = true} source ^ "\n");
   10.50 +      let val output = "%\n" ^ output_text state {markdown = true} source
   10.51 +      in if String.isSuffix "\n" output then output else output ^ "\n" end);
   10.52  
   10.53  
   10.54  (* command spans *)