diff --git a/src/Pure/Thy/latex.scala b/src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala
+++ b/src/Pure/Thy/latex.scala
@@ -1,451 +1,451 @@
 /*  Title:      Pure/Thy/latex.scala
     Author:     Makarius
 
 Support for LaTeX.
 */
 
 package isabelle
 
 
 import java.io.{File => JFile}
 
 import scala.annotation.tailrec
 import scala.collection.mutable
 import scala.collection.immutable.TreeMap
 import scala.util.matching.Regex
 
 
 object Latex {
   /* output name for LaTeX macros */
 
   private val output_name_map: Map[Char, String] =
     Map('_' -> "UNDERSCORE",
       '\'' -> "PRIME",
       '0' -> "ZERO",
       '1' -> "ONE",
       '2' -> "TWO",
       '3' -> "THREE",
       '4' -> "FOUR",
       '5' -> "FIVE",
       '6' -> "SIX",
       '7' -> "SEVEN",
       '8' -> "EIGHT",
       '9' -> "NINE")
 
   def output_name(name: String): String =
     if (name.exists(output_name_map.keySet)) {
       val res = new StringBuilder
       for (c <- name) {
         output_name_map.get(c) match {
           case None => res += c
           case Some(s) => res ++= s
         }
       }
       res.toString
     }
     else name
 
 
   /* cite: references to bibliography */
 
   object Cite {
     sealed case class Value(kind: String, citation: String, location: XML.Body)
     def unapply(tree: XML.Tree): Option[Value] =
       tree match {
         case XML.Elem(Markup(Markup.Latex_Cite.name, props), body) =>
           val kind = Markup.Kind.unapply(props).getOrElse("cite")
-          val citations = Markup.Citations.unapply(props).getOrElse("")
+          val citations = Markup.Citations.get(props)
           Some(Value(kind, citations, body))
         case _ => None
       }
   }
 
 
   /* index entries */
 
   def index_escape(str: String): String = {
     val special1 = "!\"@|"
     val special2 = "\\{}#"
     if (str.exists(c => special1.contains(c) || special2.contains(c))) {
       val res = new StringBuilder
       for (c <- str) {
         if (special1.contains(c)) {
           res ++= "\\char"
           res ++= Value.Int(c)
         }
         else {
           if (special2.contains(c)) { res += '"'}
           res += c
         }
       }
       res.toString
     }
     else str
   }
 
   object Index_Item {
     sealed case class Value(text: Text, like: String)
     def unapply(tree: XML.Tree): Option[Value] =
       tree match {
         case XML.Wrapped_Elem(Markup.Latex_Index_Item(_), text, like) =>
           Some(Value(text, XML.content(like)))
         case _ => None
       }
   }
 
   object Index_Entry {
     sealed case class Value(items: List[Index_Item.Value], kind: String)
     def unapply(tree: XML.Tree): Option[Value] =
       tree match {
         case XML.Elem(Markup.Latex_Index_Entry(kind), body) =>
           val items = body.map(Index_Item.unapply)
           if (items.forall(_.isDefined)) Some(Value(items.map(_.get), kind)) else None
         case _ => None
       }
   }
 
 
   /* tags */
 
   object Tags {
     object Op extends Enumeration {
       val fold, drop, keep = Value
     }
 
     val standard = "document,theory,proof,ML,visible,-invisible,important,unimportant"
 
     private def explode(spec: String): List[String] =
       Library.space_explode(',', spec)
 
     def apply(spec: String): Tags =
       new Tags(spec,
         (explode(standard) ::: explode(spec)).foldLeft(TreeMap.empty[String, Op.Value]) {
           case (m, tag) =>
             tag.toList match {
               case '/' :: cs => m + (cs.mkString -> Op.fold)
               case '-' :: cs => m + (cs.mkString -> Op.drop)
               case '+' :: cs => m + (cs.mkString -> Op.keep)
               case cs => m + (cs.mkString -> Op.keep)
             }
         })
 
     val empty: Tags = apply("")
   }
 
   class Tags private(spec: String, map: TreeMap[String, Tags.Op.Value]) {
     override def toString: String = spec
 
     def get(name: String): Option[Tags.Op.Value] = map.get(name)
 
     def sty(comment_latex: Boolean): File.Content = {
       val path = Path.explode("isabelletags.sty")
       val comment =
         if (comment_latex) """\usepackage{comment}"""
         else """%plain TeX version of comment package -- much faster!
 \let\isafmtname\fmtname\def\fmtname{plain}
 \usepackage{comment}
 \let\fmtname\isafmtname"""
       val tags =
         (for ((name, op) <- map.iterator)
           yield "\\isa" + op + "tag{" + name + "}").toList
       File.content(path, comment + """
 
 \newcommand{\isakeeptag}[1]%
 {\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
 \newcommand{\isadroptag}[1]%
 {\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}
 \newcommand{\isafoldtag}[1]%
 {\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
 
 """ + Library.terminate_lines(tags))
     }
   }
 
 
   /* output text and positions */
 
   type Text = XML.Body
 
   def position(a: String, b: String): String = "%:%" + a + "=" + b + "%:%\n"
 
   def init_position(file_pos: String): List[String] =
     if (file_pos.isEmpty) Nil
     else List("\\endinput\n", position(Markup.FILE, file_pos))
 
   class Output(val options: Options) {
     def latex_output(latex_text: Text): String = make(latex_text)
 
     def latex_macro0(name: String, optional_argument: String = ""): Text =
       XML.string("\\" + name + optional_argument)
 
     def latex_macro(name: String, body: Text, optional_argument: String = ""): Text =
       XML.enclose("\\" + name + optional_argument + "{", "}", body)
 
     def latex_environment(name: String, body: Text, optional_argument: String = ""): Text =
       XML.enclose(
         "%\n\\begin{" + name + "}" + optional_argument + "%\n",
         "%\n\\end{" + name + "}", body)
 
     def latex_heading(kind: String, body: Text, optional_argument: String = ""): Text =
       XML.enclose(
         "%\n\\" + options.string("document_heading_prefix") + kind + optional_argument + "{",
         "%\n}\n", body)
 
     def latex_body(kind: String, body: Text, optional_argument: String = ""): Text =
       latex_environment("isamarkup" + kind, body, optional_argument)
 
     def latex_tag(name: String, body: Text, delim: Boolean = false): Text = {
       val s = output_name(name)
       val kind = if (delim) "delim" else "tag"
       val end = if (delim) "" else "{\\isafold" + s + "}%\n"
       if (options.bool("document_comment_latex")) {
         XML.enclose(
           "%\n\\begin{isa" + kind + s + "}\n",
           "%\n\\end{isa" + kind + s + "}\n" + end, body)
       }
       else {
         XML.enclose(
           "%\n\\isa" + kind + s + "\n",
           "%\n\\endisa" + kind + s + "\n" + end, body)
       }
     }
 
     def cite(value: Cite.Value): Text = {
       latex_macro0(value.kind) :::
       (if (value.location.isEmpty) Nil
        else XML.string("[") ::: value.location ::: XML.string("]")) :::
       XML.string("{" + value.citation + "}")
     }
 
     def index_item(item: Index_Item.Value): String = {
       val like = if (item.like.isEmpty) "" else index_escape(item.like) + "@"
       val text = index_escape(latex_output(item.text))
       like + text
     }
 
     def index_entry(entry: Index_Entry.Value): Text = {
       val items = entry.items.map(index_item).mkString("!")
       val kind = if (entry.kind.isEmpty) "" else "|" + index_escape(entry.kind)
       latex_macro("index", XML.string(items + kind))
     }
 
 
     /* standard output of text with per-line positions */
 
     def unknown_elem(elem: XML.Elem, pos: Position.T): XML.Body =
       error("Unknown latex markup element " + quote(elem.name) + Position.here(pos) +
         ":\n" + XML.string_of_tree(elem))
 
     def make(latex_text: Text, file_pos: String = ""): String = {
       var line = 1
       val result = new mutable.ListBuffer[String]
       val positions = new mutable.ListBuffer[String] ++= init_position(file_pos)
 
       val file_position = if (file_pos.isEmpty) Position.none else Position.File(file_pos)
 
       def traverse(xml: XML.Body): Unit = {
         xml.foreach {
           case XML.Text(s) =>
             line += s.count(_ == '\n')
             result += s
           case elem @ XML.Elem(markup, body) =>
             val a = Markup.Optional_Argument.get(markup.properties)
             traverse {
               markup match {
                 case Markup.Document_Latex(props) =>
                   for (l <- Position.Line.unapply(props) if positions.nonEmpty) {
                     val s = position(Value.Int(line), Value.Int(l))
                     if (positions.last != s) positions += s
                   }
                   body
                 case Markup.Latex_Output(_) => XML.string(latex_output(body))
                 case Markup.Latex_Macro0(name) if body.isEmpty => latex_macro0(name, a)
                 case Markup.Latex_Macro(name) => latex_macro(name, body, a)
                 case Markup.Latex_Environment(name) => latex_environment(name, body, a)
                 case Markup.Latex_Heading(kind) => latex_heading(kind, body, a)
                 case Markup.Latex_Body(kind) => latex_body(kind, body, a)
                 case Markup.Latex_Delim(name) => latex_tag(name, body, delim = true)
                 case Markup.Latex_Tag(name) => latex_tag(name, body)
                 case Markup.Latex_Cite(_) =>
                   elem match {
                     case Cite(value) => cite(value)
                     case _ => unknown_elem(elem, file_position)
                   }
                 case Markup.Latex_Index_Entry(_) =>
                   elem match {
                     case Index_Entry(entry) => index_entry(entry)
                     case _ => unknown_elem(elem, file_position)
                   }
                 case _ => unknown_elem(elem, file_position)
               }
             }
         }
       }
       traverse(latex_text)
 
       result ++= positions
       result.mkString
     }
   }
 
 
   /* generated .tex file */
 
   private val File_Pattern = """^%:%file=(.+)%:%$""".r
   private val Line_Pattern = """^*%:%(\d+)=(\d+)%:%$""".r
 
   def read_tex_file(tex_file: Path): Tex_File = {
     val positions =
       Line.logical_lines(File.read(tex_file)).reverse.
         takeWhile(_ != "\\endinput").reverse
 
     val source_file =
       positions match {
         case File_Pattern(file) :: _ => Some(file)
         case _ => None
       }
 
     val source_lines =
       if (source_file.isEmpty) Nil
       else
         positions.flatMap(line =>
           line match {
             case Line_Pattern(Value.Int(line), Value.Int(source_line)) => Some(line -> source_line)
             case _ => None
           })
 
     new Tex_File(tex_file, source_file, source_lines)
   }
 
   final class Tex_File private[Latex](
     tex_file: Path,
     source_file: Option[String],
     source_lines: List[(Int, Int)]
   ) {
     override def toString: String = tex_file.toString
 
     def source_position(l: Int): Option[Position.T] =
       source_file match {
         case None => None
         case Some(file) =>
           val source_line =
             source_lines.iterator.takeWhile({ case (m, _) => m <= l }).
               foldLeft(0) { case (_, (_, n)) => n }
           if (source_line == 0) None else Some(Position.Line_File(source_line, file))
       }
 
     def position(line: Int): Position.T =
       source_position(line) getOrElse Position.Line_File(line, tex_file.implode)
   }
 
 
   /* latex log */
 
   def latex_errors(dir: Path, root_name: String): List[String] = {
     val root_log_path = dir + Path.explode(root_name).ext("log")
     if (root_log_path.is_file) {
       for { (msg, pos) <- filter_errors(dir, File.read(root_log_path)) }
         yield "Latex error" + Position.here(pos) + ":\n" + Library.indent_lines(2, msg)
     }
     else Nil
   }
 
   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: Regex = """^(.*?\.\w\w\w):(\d+): (.*)$""".r
       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 = (dir + Path.explode(path)).canonical
               val msg = Library.perhaps_unprefix("LaTeX Error: ", message)
               if (file.is_file) Some((file, line, msg)) else None
             }
             else None
           case _ => None
         }
     }
 
     val Line_Error = """^l\.\d+ (.*)$""".r
     val More_Error =
       List(
         "<argument>",
         "<template>",
         "<recently read>",
         "<to be read again>",
         "<inserted text>",
         "<output>",
         "<everypar>",
         "<everymath>",
         "<everydisplay>",
         "<everyhbox>",
         "<everyvbox>",
         "<everyjob>",
         "<everycr>",
         "<mark>",
         "<everyeof>",
         "<write>").mkString("^(?:", "|", ") (.*)$").r
 
     val Bad_Font = """^LaTeX Font Warning: (Font .*\btxmia\b.* undefined).*$""".r
     val Bad_File = """^! LaTeX Error: (File `.*' not found\.)$""".r
 
     val error_ignore =
       Set(
         "See the LaTeX manual or LaTeX Companion for explanation.",
         "Type  H <return>  for immediate help.")
 
     def error_suffix1(lines: List[String]): Option[String] = {
       val lines1 =
         lines.take(20).takeWhile({ case File_Line_Error((_, _, _)) => false case _ => true })
       lines1.zipWithIndex.collectFirst({
         case (Line_Error(msg), i) =>
           cat_lines(lines1.take(i).filterNot(error_ignore) ::: List(msg)) })
     }
     def error_suffix2(lines: List[String]): Option[String] =
       lines match {
         case More_Error(msg) :: _ => Some(msg)
         case _ => None
       }
 
     @tailrec def filter(
       lines: List[String],
       result: List[(String, Position.T)]
     ) : List[(String, Position.T)] = {
       lines match {
         case File_Line_Error((file, line, msg1)) :: rest1 =>
           val pos = tex_file_position(file, line)
           val msg2 = error_suffix1(rest1) orElse error_suffix2(rest1) getOrElse ""
           filter(rest1, (Exn.cat_message(msg1, msg2), pos) :: result)
         case Bad_Font(msg) :: rest =>
           filter(rest, (msg, Position.none) :: result)
         case Bad_File(msg) :: rest =>
           filter(rest, (msg, Position.none) :: result)
         case _ :: rest => filter(rest, result)
         case Nil => result.reverse
       }
     }
 
     filter(Line.logical_lines(root_log), Nil)
   }
 }