diff --git a/src/Pure/PIDE/document.scala b/src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala
+++ b/src/Pure/PIDE/document.scala
@@ -1,1266 +1,1266 @@
 /*  Title:      Pure/PIDE/document.scala
     Author:     Makarius
 
 Document as collection of named nodes, each consisting of an editable
 list of commands, associated with asynchronous execution process.
 */
 
 package isabelle
 
 
 import scala.collection.mutable
 
 
 object Document {
   /** document structure **/
 
   /* overlays -- print functions with arguments */
 
   object Overlays {
     val empty = new Overlays(Map.empty)
   }
 
   final class Overlays private(rep: Map[Node.Name, Node.Overlays]) {
     def apply(name: Node.Name): Node.Overlays =
       rep.getOrElse(name, Node.Overlays.empty)
 
     private def update(name: Node.Name, f: Node.Overlays => Node.Overlays): Overlays = {
       val node_overlays = f(apply(name))
       new Overlays(if (node_overlays.is_empty) rep - name else rep + (name -> node_overlays))
     }
 
     def insert(command: Command, fn: String, args: List[String]): Overlays =
       update(command.node_name, _.insert(command, fn, args))
 
     def remove(command: Command, fn: String, args: List[String]): Overlays =
       update(command.node_name, _.remove(command, fn, args))
 
     override def toString: String = rep.mkString("Overlays(", ",", ")")
   }
 
 
   /* document blobs: auxiliary files */
 
   object Blobs {
     sealed case class Item(
       bytes: Bytes,
       source: String,
       chunk: Symbol.Text_Chunk,
       changed: Boolean
     ) {
       def source_wellformed: Boolean = bytes.wellformed_text.nonEmpty
       def unchanged: Item = copy(changed = false)
     }
 
     def apply(blobs: Map[Node.Name, Item]): Blobs = new Blobs(blobs)
     val empty: Blobs = apply(Map.empty)
 
     def make(blobs: List[(Command.Blob, Item)]): Blobs =
       if (blobs.isEmpty) empty
       else apply((for ((a, b) <- blobs.iterator) yield a.name -> b).toMap)
   }
 
   final class Blobs private(blobs: Map[Node.Name, Blobs.Item]) {
     def get(name: Node.Name): Option[Blobs.Item] = blobs.get(name)
 
     def changed(name: Node.Name): Boolean =
       get(name) match {
         case Some(blob) => blob.changed
         case None => false
       }
 
     override def toString: String = blobs.mkString("Blobs(", ",", ")")
   }
 
 
   /* document nodes: theories and auxiliary files */
 
   type Edit[A, B] = (Node.Name, Node.Edit[A, B])
   type Edit_Text = Edit[Text.Edit, Text.Perspective]
   type Edit_Command = Edit[Command.Edit, Command.Perspective]
 
   object Node {
     /* header and name */
 
     sealed case class Header(
       imports_pos: List[(Name, Position.T)] = Nil,
       keywords: Thy_Header.Keywords = Nil,
       abbrevs: Thy_Header.Abbrevs = Nil,
       errors: List[String] = Nil
     ) {
       def imports: List[Name] = imports_pos.map(_._1)
 
       def append_errors(msgs: List[String]): Header =
         copy(errors = errors ::: msgs)
 
       def cat_errors(msg2: String): Header =
         copy(errors = errors.map(msg1 => Exn.cat_message(msg1, msg2)))
     }
 
     val no_header: Header = Header()
     def bad_header(msg: String): Header = Header(errors = List(msg))
 
     object Name {
       def apply(node: String, theory: String = ""): Name = new Name(node, theory)
 
       def loaded_theory(theory: String): Name = Name(theory, theory = theory)
 
       val empty: Name = Name("")
 
       object Ordering extends scala.math.Ordering[Name] {
         def compare(name1: Name, name2: Name): Int = name1.node compare name2.node
       }
 
       type Graph[A] = isabelle.Graph[Node.Name, A]
 
       def make_graph[A](entries: List[((Name, A), List[Name])]): Graph[A] =
         Graph.make(entries, converse = true)(Ordering)
     }
 
     final class Name private(val node: String, val theory: String) {
       override def hashCode: Int = node.hashCode
       override def equals(that: Any): Boolean =
         that match {
           case other: Name => node == other.node
           case _ => false
         }
 
       def file_name: String = Url.get_base_name(node).getOrElse("")
 
       def path: Path = Path.explode(File.standard_path(node))
 
       def master_dir: String = Url.strip_base_name(node).getOrElse("")
 
       def is_theory: Boolean = theory.nonEmpty
 
       def theory_base_name: String = Long_Name.base_name(theory)
 
       override def toString: String = if (is_theory) theory else node
 
       def json: JSON.Object.T =
         JSON.Object("node_name" -> node, "theory_name" -> theory)
     }
 
     sealed case class Entry(name: Node.Name, header: Node.Header) {
       override def toString: String = name.toString
     }
 
 
     /* node overlays */
 
     object Overlays {
       val empty = new Overlays(Multi_Map.empty)
     }
 
     final class Overlays private(rep: Multi_Map[Command, (String, List[String])]) {
       def commands: Set[Command] = rep.keySet
       def is_empty: Boolean = rep.isEmpty
       def dest: List[(Command, (String, List[String]))] = rep.iterator.toList
       def insert(cmd: Command, fn: String, args: List[String]): Overlays =
         new Overlays(rep.insert(cmd, (fn, args)))
       def remove(cmd: Command, fn: String, args: List[String]): Overlays =
         new Overlays(rep.remove(cmd, (fn, args)))
 
       override def toString: String = rep.mkString("Node.Overlays(", ",", ")")
     }
 
 
     /* edits */
 
     sealed abstract class Edit[A, B] {
       def foreach(f: A => Unit): Unit = {
         this match {
           case Edits(es) => es.foreach(f)
           case _ =>
         }
       }
 
       def is_void: Boolean =
         this match {
           case Edits(Nil) => true
           case _ => false
         }
     }
     case class Blob[A, B](blob: Blobs.Item) extends Edit[A, B]
 
     case class Edits[A, B](edits: List[A]) extends Edit[A, B]
     case class Deps[A, B](header: Header) extends Edit[A, B]
     case class Perspective[A, B](required: Boolean, visible: B, overlays: Overlays) extends Edit[A, B]
 
 
     /* perspective */
 
     object Perspective_Text {
       type T = Perspective[Text.Edit, Text.Perspective]
       val empty: T = Perspective(false, Text.Perspective.empty, Overlays.empty)
       def is_empty(perspective: T): Boolean =
         !perspective.required &&
         perspective.visible.is_empty &&
         perspective.overlays.is_empty
     }
 
     object Perspective_Command {
       type T = Perspective[Command.Edit, Command.Perspective]
       val empty: T = Perspective(false, Command.Perspective.empty, Overlays.empty)
       def is_empty(perspective: T): Boolean =
         !perspective.required &&
         perspective.visible.is_empty &&
         perspective.overlays.is_empty
     }
 
 
     /* commands */
 
     object Commands {
       def apply(commands: Linear_Set[Command]): Commands = new Commands(commands)
       val empty: Commands = apply(Linear_Set.empty)
 
       def starts(
         commands: Iterator[Command],
         init: Int = 0,
         count: Command => Int = _.length
       ) : Iterator[(Command, Int)] = {
         var i = init
         for (command <- commands) yield {
           val start = i
           i += count(command)
           (command, start)
         }
       }
 
       def starts_pos(
         commands: Iterator[Command],
         pos: Token.Pos = Token.Pos.start
       ) : Iterator[(Command, Token.Pos)] = {
         var p = pos
         for (command <- commands) yield {
           val start = p
           p = command.span.content.foldLeft(p)(_.advance(_))
           (command, start)
         }
       }
 
       private val block_size = 256
     }
 
     final class Commands private(val commands: Linear_Set[Command]) {
       lazy val start_lines: Map[Document_ID.Command, Int] =
         (for {
           (command, line) <-
             Node.Commands.starts(commands.iterator, init = 1,
-              count = cmd => cmd.source.count(_ == '\n'))
+              count = cmd => Library.count_newlines(cmd.source))
         } yield command.id -> line).toMap
 
       lazy val load_commands: List[Command] =
         commands.iterator.filter(cmd => cmd.blobs.nonEmpty).toList
 
       private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) = {
         val blocks = new mutable.ListBuffer[(Command, Text.Offset)]
         var next_block = 0
         var last_stop = 0
         for ((command, start) <- Commands.starts(commands.iterator)) {
           last_stop = start + command.length
           while (last_stop + 1 > next_block) {
             blocks += (command -> start)
             next_block += Commands.block_size
           }
         }
         (blocks.toArray, Text.Range(0, last_stop))
       }
 
       private def full_range: Text.Range = full_index._2
 
       def iterator(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] = {
         if (commands.nonEmpty && full_range.contains(i)) {
           val (cmd0, start0) = full_index._1(i / Commands.block_size)
           Node.Commands.starts(commands.iterator(cmd0), start0) dropWhile {
             case (cmd, start) => start + cmd.length <= i }
         }
         else Iterator.empty
       }
     }
 
     val empty: Node = new Node()
 
     def init_blob(blob: Blobs.Item): Node =
       new Node(get_blob = Some(blob.unchanged))
   }
 
   final class Node private(
     val get_blob: Option[Blobs.Item] = None,
     val header: Node.Header = Node.no_header,
     val syntax: Option[Outer_Syntax] = None,
     val text_perspective: Text.Perspective = Text.Perspective.empty,
     val perspective: Node.Perspective_Command.T = Node.Perspective_Command.empty,
     _commands: Node.Commands = Node.Commands.empty
   ) {
     def is_empty: Boolean =
       get_blob.isEmpty &&
       header == Node.no_header &&
       text_perspective.is_empty &&
       Node.Perspective_Command.is_empty(perspective) &&
       commands.isEmpty
 
     def has_header: Boolean = header != Node.no_header
 
     override def toString: String =
       if (is_empty) "empty"
       else if (get_blob.isDefined) "blob"
       else "node"
 
     def commands: Linear_Set[Command] = _commands.commands
     def command_start_line(command: Command): Option[Int] =
       _commands.start_lines.get(command.id)
     def load_commands: List[Command] = _commands.load_commands
     def load_commands_changed(doc_blobs: Blobs): Boolean =
       load_commands.exists(_.blobs_changed(doc_blobs))
 
     def update_header(new_header: Node.Header): Node =
       new Node(get_blob, new_header, syntax, text_perspective, perspective, _commands)
 
     def update_syntax(new_syntax: Option[Outer_Syntax]): Node =
       new Node(get_blob, header, new_syntax, text_perspective, perspective, _commands)
 
     def update_perspective(
         new_text_perspective: Text.Perspective,
         new_perspective: Node.Perspective_Command.T): Node =
       new Node(get_blob, header, syntax, new_text_perspective, new_perspective, _commands)
 
     def edit_perspective: Node.Edit[Text.Edit, Text.Perspective] =
       Node.Perspective(perspective.required, text_perspective, perspective.overlays)
 
     def same_perspective(
         other_text_perspective: Text.Perspective,
         other_perspective: Node.Perspective_Command.T): Boolean =
       text_perspective == other_text_perspective &&
       perspective.required == other_perspective.required &&
       perspective.visible.same(other_perspective.visible) &&
       perspective.overlays == other_perspective.overlays
 
     def update_commands(new_commands: Linear_Set[Command]): Node =
       if (new_commands eq _commands.commands) this
       else {
         new Node(get_blob, header, syntax, text_perspective, perspective,
           Node.Commands(new_commands))
       }
 
     def command_iterator(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
       _commands.iterator(i)
 
     def command_iterator(range: Text.Range): Iterator[(Command, Text.Offset)] =
       command_iterator(range.start) takeWhile { case (_, start) => start < range.stop }
 
     def command_start(cmd: Command): Option[Text.Offset] =
       Node.Commands.starts(commands.iterator).find(_._1 == cmd).map(_._2)
 
     lazy val source_wellformed: Boolean =
       get_blob match {
         case Some(blob) => blob.source_wellformed
         case None => true
       }
 
     lazy val source: String =
       get_blob match {
         case Some(blob) => blob.source
         case None => command_iterator().map({ case (cmd, _) => cmd.source }).mkString
       }
   }
 
 
   /* development graph */
 
   object Nodes {
     val empty: Nodes = new Nodes(Graph.empty(Node.Name.Ordering))
   }
 
   final class Nodes private(graph: Graph[Node.Name, Node]) {
     def apply(name: Node.Name): Node =
       graph.default_node(name, Node.empty).get_node(name)
 
     def is_suppressed(name: Node.Name): Boolean = {
       val graph1 = graph.default_node(name, Node.empty)
       graph1.is_maximal(name) && graph1.get_node(name).is_empty
     }
 
     def purge_suppressed: Option[Nodes] =
       graph.keys_iterator.filter(is_suppressed).toList match {
         case Nil => None
         case del => Some(new Nodes(del.foldLeft(graph)(_.del_node(_))))
       }
 
     def + (entry: (Node.Name, Node)): Nodes = {
       val (name, node) = entry
       val imports = node.header.imports
       val graph1 =
         imports.foldLeft(graph.default_node(name, Node.empty)) {
           case (g, p) => g.default_node(p, Node.empty)
         }
       val graph2 =
         graph1.imm_preds(name).foldLeft(graph1) { case (g, dep) => g.del_edge(dep, name) }
       val graph3 = imports.foldLeft(graph2) { case (g, dep) => g.add_edge(dep, name) }
       new Nodes(graph3.map_node(name, _ => node))
     }
 
     def domain: Set[Node.Name] = graph.domain
 
     def iterator: Iterator[(Node.Name, Node)] =
       graph.iterator.map({ case (name, (node, _)) => (name, node) })
 
     def theory_name(theory: String): Option[Node.Name] =
       graph.keys_iterator.find(name => name.theory == theory)
 
     def commands_loading(file_name: Node.Name): List[Command] =
       (for {
         (_, node) <- iterator
         cmd <- node.load_commands.iterator
         name <- cmd.blobs_names.iterator
         if name == file_name
       } yield cmd).toList
 
     def descendants(names: List[Node.Name]): List[Node.Name] = graph.all_succs(names)
     def requirements(names: List[Node.Name]): List[Node.Name] = graph.all_preds_rev(names)
     def topological_order: List[Node.Name] = graph.topological_order
 
     override def toString: String = topological_order.mkString("Nodes(", ",", ")")
   }
 
 
 
   /** versioning **/
 
   /* particular document versions */
 
   object Version {
     val init: Version = new Version()
     def make(nodes: Nodes): Version = new Version(Document_ID.make(), nodes)
 
     def purge_future(
       versions: Map[Document_ID.Version, Version],
       future: Future[Version]
     ) : Future[Version] = {
       if (future.is_finished) {
         val version = future.join
         versions.get(version.id) match {
           case Some(version1) if !(version eq version1) => Future.value(version1)
           case _ => future
         }
       }
       else future
     }
 
     def purge_suppressed(
       versions: Map[Document_ID.Version, Version]
     ): Map[Document_ID.Version, Version] = {
       (for ((id, v) <- versions.iterator; v1 <- v.purge_suppressed) yield (id, v1)).
         foldLeft(versions)(_ + _)
     }
   }
 
   final class Version private(
     val id: Document_ID.Version = Document_ID.none,
     val nodes: Nodes = Nodes.empty
   ) {
     override def toString: String = "Version(" + id + ")"
 
     def purge_suppressed: Option[Version] =
       nodes.purge_suppressed.map(new Version(id, _))
   }
 
 
   /* changes of plain text, eventually resulting in document edits */
 
   object Change {
     val init: Change = new Change()
 
     def make(previous: Future[Version], edits: List[Edit_Text], version: Future[Version]): Change =
       new Change(Some(previous), edits.reverse, version)
   }
 
   final class Change private(
     val previous: Option[Future[Version]] = Some(Future.value(Version.init)),
     val rev_edits: List[Edit_Text] = Nil,
     val version: Future[Version] = Future.value(Version.init)
   ) {
     def is_finished: Boolean =
       (previous match { case None => true case Some(future) => future.is_finished }) &&
       version.is_finished
 
     def truncate: Change = new Change(None, Nil, version)
 
     def purge(versions: Map[Document_ID.Version, Version]): Option[Change] = {
       val previous1 = previous.map(Version.purge_future(versions, _))
       val version1 = Version.purge_future(versions, version)
       if ((previous eq previous1) && (version eq version1)) None
       else Some(new Change(previous1, rev_edits, version1))
     }
   }
 
 
   /* history navigation */
 
   object History {
     val init: History = new History()
   }
 
   final class History private(
     val undo_list: List[Change] = List(Change.init)  // non-empty list
   ) {
     override def toString: String = "History(" + undo_list.length + ")"
 
     def tip: Change = undo_list.head
     def + (change: Change): History = new History(change :: undo_list)
 
     def prune(check: Change => Boolean, retain: Int): Option[(List[Change], History)] = {
       val n = undo_list.iterator.zipWithIndex.find(p => check(p._1)).get._2 + 1
       val (retained, dropped) = undo_list.splitAt(n max retain)
 
       retained.splitAt(retained.length - 1) match {
         case (prefix, List(last)) => Some(dropped, new History(prefix ::: List(last.truncate)))
         case _ => None
       }
     }
 
     def purge(versions: Map[Document_ID.Version, Version]): History = {
       val undo_list1 = undo_list.map(_.purge(versions))
       if (undo_list1.forall(_.isEmpty)) this
       else new History(for ((a, b) <- undo_list1 zip undo_list) yield a.getOrElse(b))
     }
   }
 
 
   /* snapshot: persistent user-view of document state */
 
   object Pending_Edits {
     val empty: Pending_Edits = make(Nil)
 
     def make(models: Iterable[Model]): Pending_Edits =
       new Pending_Edits(
         (for {
           model <- models.iterator
           edits = model.pending_edits if edits.nonEmpty
         } yield model.node_name -> edits).toMap)
   }
 
   final class Pending_Edits(pending_edits: Map[Node.Name, List[Text.Edit]]) {
     def is_stable: Boolean = pending_edits.isEmpty
 
     def + (entry: (Node.Name, List[Text.Edit])): Pending_Edits = {
       val (name, es) = entry
       if (es.isEmpty) this
       else new Pending_Edits(pending_edits + (name -> (es ::: edits(name))))
     }
 
     def edits(name: Node.Name): List[Text.Edit] =
       pending_edits.getOrElse(name, Nil)
 
     def reverse_edits(name: Node.Name): List[Text.Edit] =
       reverse_pending_edits.getOrElse(name, Nil)
 
     private lazy val reverse_pending_edits =
       (for ((name, es) <- pending_edits.iterator) yield (name, es.reverse)).toMap
   }
 
   object Snapshot {
     val init: Snapshot = State.init.snapshot()
   }
 
   class Snapshot private[Document](
     val state: State,
     val version: Version,
     val node_name: Node.Name,
     pending_edits: Pending_Edits,
     val snippet_command: Option[Command]
   ) {
     override def toString: String =
       "Snapshot(node = " + node_name.node + ", version = " + version.id +
         (if (is_outdated) ", outdated" else "") + ")"
 
     def switch(name: Node.Name): Snapshot =
       if (name == node_name) this
       else new Snapshot(state, version, name, pending_edits, None)
 
 
     /* nodes */
 
     def get_node(name: Node.Name): Node = version.nodes(name)
 
     val node: Node = get_node(node_name)
 
     def node_files: List[Node.Name] =
       node_name :: node.load_commands.flatMap(_.blobs_names)
 
 
     /* pending edits */
 
     def is_outdated: Boolean = !pending_edits.is_stable
 
     def convert(offset: Text.Offset): Text.Offset =
       pending_edits.edits(node_name).foldLeft(offset) { case (i, edit) => edit.convert(i) }
     def revert(offset: Text.Offset): Text.Offset =
       pending_edits.reverse_edits(node_name).foldLeft(offset) { case (i, edit) => edit.revert(i) }
 
     def convert(range: Text.Range): Text.Range = range.map(convert)
     def revert(range: Text.Range): Text.Range = range.map(revert)
 
 
     /* theory load commands */
 
     val commands_loading: List[Command] =
       if (node_name.is_theory) Nil
       else version.nodes.commands_loading(node_name)
 
     def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range] =
       (for {
         cmd <- node.load_commands.iterator
         blob_name <- cmd.blobs_names.iterator
         if pred(blob_name)
         start <- node.command_start(cmd)
       } yield convert(cmd.core_range + start)).toList
 
 
     /* command as add-on snippet */
 
     def snippet(command: Command, doc_blobs: Blobs): Snapshot = {
       val node_name = command.node_name
 
       val blobs = for (a <- command.blobs_names; b <- doc_blobs.get(a)) yield a -> b
 
       val nodes0 = version.nodes
       val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command)))
       val nodes2 = blobs.foldLeft(nodes1) { case (ns, (a, b)) => ns + (a -> Node.init_blob(b)) }
       val version1 = Version.make(nodes2)
 
       val edits: List[Edit_Text] =
         List(node_name -> Node.Edits(List(Text.Edit.insert(0, command.source)))) :::
         blobs.map({ case (a, b) => a -> Node.Blob(b) })
 
       val state0 = state.define_command(command)
       val state1 =
         state0.continue_history(Future.value(version), edits, Future.value(version1))
           .define_version(version1, state0.the_assignment(version))
           .assign(version1.id, Nil, List(command.id -> List(Document_ID.make())))._2
 
       state1.snapshot(node_name = node_name, snippet_command = Some(command))
     }
 
 
     /* markup and messages */
 
     def xml_markup(
         range: Text.Range = Text.Range.full,
         elements: Markup.Elements = Markup.Elements.full): XML.Body =
       state.xml_markup(version, node_name, range = range, elements = elements)
 
     lazy val messages: List[(XML.Elem, Position.T)] =
       (for {
         (command, start) <-
           Node.Commands.starts_pos(node.commands.iterator, Token.Pos.file(node_name.node))
         pos = command.span.keyword_pos(start).position(command.span.name)
         (_, elem) <- state.command_results(version, command).iterator
        } yield (elem, pos)).toList
 
 
     /* exports */
 
     lazy val exports: List[Export.Entry] =
       state.node_exports(version, node_name).iterator.map(_._2).toList
 
     lazy val all_exports: Map[Export.Entry_Name, Export.Entry] =
       (for {
         (name, _) <- version.nodes.iterator
         (_, entry) <- state.node_exports(version, name).iterator
         if entry.entry_name.session == Sessions.DRAFT
       } yield entry.entry_name -> entry).toMap
 
 
     /* find command */
 
     def find_command(id: Document_ID.Generic): Option[(Node, Command)] =
       state.lookup_id(id) match {
         case None => None
         case Some(st) =>
           val command = st.command
           val command_node = get_node(command.node_name)
           if (command_node.commands.contains(command)) Some((command_node, command)) else None
       }
 
     def find_command_position(
       id: Document_ID.Generic,
       offset: Symbol.Offset
     ): Option[Line.Node_Position] = {
       for ((node, command) <- find_command(id))
       yield {
         val name = command.node_name.node
         val sources_iterator =
           node.commands.iterator.takeWhile(_ != command).map(_.source) ++
             (if (offset == 0) Iterator.empty
              else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
         val pos = sources_iterator.foldLeft(Line.Position.zero)(_.advance(_))
         Line.Node_Position(name, pos)
       }
     }
 
     def find_command_line(id: Document_ID.Generic, offset: Symbol.Offset): Option[Int] =
       for {
         (node, command) <- find_command(id)
         range = Text.Range(0, command.chunk.decode(offset))
         text <- range.try_substring(command.source)
         line <- node.command_start_line(command)
-      } yield line + text.count(_ == '\n')
+      } yield line + Library.count_newlines(text)
 
     def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command] =
       if (other_node_name.is_theory) {
         val other_node = get_node(other_node_name)
         val iterator = other_node.command_iterator(revert(offset) max 0)
         if (iterator.hasNext) {
           val (command0, _) = iterator.next()
           other_node.commands.reverse.iterator(command0).find(command => !command.is_ignored)
         }
         else other_node.commands.reverse.iterator.find(command => !command.is_ignored)
       }
       else version.nodes.commands_loading(other_node_name).headOption
 
 
     /* command results */
 
     def command_results(range: Text.Range): Command.Results =
       Command.State.merge_results(
         select[List[Command.State]](range, Markup.Elements.full,
           command_states => _ => Some(command_states)).flatMap(_.info))
 
     def command_results(command: Command): Command.Results =
       state.command_results(version, command)
 
 
     /* cumulate markup */
 
     def cumulate[A](
       range: Text.Range,
       info: A,
       elements: Markup.Elements,
       result: List[Command.State] => (A, Text.Markup) => Option[A],
       status: Boolean = false
     ): List[Text.Info[A]] = {
       val former_range = revert(range).inflate_singularity
       val (chunk_name, command_iterator) =
         commands_loading.headOption match {
           case None => (Symbol.Text_Chunk.Default, node.command_iterator(former_range))
           case Some(command) => (Symbol.Text_Chunk.File(node_name.node), Iterator((command, 0)))
         }
       val markup_index = Command.Markup_Index(status, chunk_name)
       (for {
         (command, command_start) <- command_iterator
         chunk <- command.chunks.get(chunk_name).iterator
         states = state.command_states(version, command)
         res = result(states)
         markup_range <- (former_range - command_start).try_restrict(chunk.range).iterator
         markup = Command.State.merge_markup(states, markup_index, markup_range, elements)
         Text.Info(r0, a) <- markup.cumulate[A](markup_range, info, elements,
           {
             case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b))
           }).iterator
         r1 <- convert(r0 + command_start).try_restrict(range).iterator
       } yield Text.Info(r1, a)).toList
     }
 
     def select[A](
       range: Text.Range,
       elements: Markup.Elements,
       result: List[Command.State] => Text.Markup => Option[A],
       status: Boolean = false
     ): List[Text.Info[A]] = {
       def result1(states: List[Command.State]): (Option[A], Text.Markup) => Option[Option[A]] = {
         val res = result(states)
         (_: Option[A], x: Text.Markup) =>
           res(x) match {
             case None => None
             case some => Some(some)
           }
       }
       for (Text.Info(r, Some(x)) <- cumulate(range, None, elements, result1, status))
         yield Text.Info(r, x)
     }
   }
 
 
   /* model */
 
   trait Session {
     def resources: Resources
   }
 
   trait Model {
     def session: Session
     def is_stable: Boolean
     def pending_edits: List[Text.Edit]
 
     def node_name: Node.Name
     def is_theory: Boolean = node_name.is_theory
     override def toString: String = node_name.toString
 
     def get_text(range: Text.Range): Option[String]
 
     def node_required: Boolean
 
     def get_blob: Option[Blobs.Item]
 
     def untyped_data: AnyRef
     def get_data[C](c: Class[C]): Option[C] = Library.as_subclass(c)(untyped_data)
 
     def node_edits(
       node_header: Node.Header,
       text_edits: List[Text.Edit],
       perspective: Node.Perspective_Text.T
     ): List[Edit_Text] = {
       val edits: List[Node.Edit[Text.Edit, Text.Perspective]] =
         get_blob match {
           case None =>
             List(
               Node.Deps(
                 if (session.resources.session_base.loaded_theory(node_name)) {
                   node_header.append_errors(
                     List("Cannot update finished theory " + quote(node_name.theory)))
                 }
                 else node_header),
               Node.Edits(text_edits), perspective)
           case Some(blob) => List(Node.Blob(blob), Node.Edits(text_edits))
         }
       edits.flatMap(edit => if (edit.is_void) None else Some(node_name -> edit))
     }
   }
 
 
   /** global state -- document structure, execution process, editing history **/
 
   type Assign_Update =
     List[(Document_ID.Command, List[Document_ID.Exec])]  // update of exec state assignment
 
   object State {
     class Fail(state: State) extends Exception
 
     object Assignment {
       val init: Assignment = new Assignment()
     }
 
     final class Assignment private(
       val command_execs: Map[Document_ID.Command, List[Document_ID.Exec]] = Map.empty,
       val is_finished: Boolean = false
     ) {
       override def toString: String = "Assignment(" + command_execs.size + "," + is_finished + ")"
 
       def check_finished: Assignment = { require(is_finished, "assignment not finished"); this }
       def unfinished: Assignment = new Assignment(command_execs, false)
 
       def assign(update: Assign_Update): Assignment = {
         require(!is_finished, "assignment already finished")
         val command_execs1 =
           update.foldLeft(command_execs) {
             case (res, (command_id, exec_ids)) =>
               if (exec_ids.isEmpty) res - command_id
               else res + (command_id -> exec_ids)
           }
         new Assignment(command_execs1, true)
       }
     }
 
     val init: State =
       State().define_version(Version.init, Assignment.init).assign(Version.init.id, Nil, Nil)._2
   }
 
   final case class State private(
     /*reachable versions*/
     versions: Map[Document_ID.Version, Version] = Map.empty,
     /*inlined auxiliary files*/
     blobs: Set[SHA1.Digest] = Set.empty,
     /*loaded theories in batch builds*/
     theories: Map[Document_ID.Exec, Command.State] = Map.empty,
     /*static markup from define_command*/
     commands: Map[Document_ID.Command, Command.State] = Map.empty,
     /*dynamic markup from execution*/
     execs: Map[Document_ID.Exec, Command.State] = Map.empty,
     /*command-exec assignment for each version*/
     assignments: Map[Document_ID.Version, State.Assignment] = Map.empty,
     /*commands with markup produced by other commands (imm_succs)*/
     commands_redirection: Graph[Document_ID.Command, Unit] = Graph.long,
     /*explicit (linear) history*/
     history: History = History.init,
     /*intermediate state between remove_versions/removed_versions*/
     removing_versions: Boolean = false
   ) {
     override def toString: String =
       "State(versions = " + versions.size +
       ", blobs = " + blobs.size +
       ", commands = " + commands.size +
       ", execs = " + execs.size +
       ", assignments = " + assignments.size +
       ", commands_redirection = " + commands_redirection.size +
       ", history = " + history.undo_list.size +
       ", removing_versions = " + removing_versions + ")"
 
     private def fail[A]: A = throw new State.Fail(this)
 
     def define_version(version: Version, assignment: State.Assignment): State = {
       val id = version.id
       copy(versions = versions + (id -> version),
         assignments = assignments + (id -> assignment.unfinished))
     }
 
     def define_blob(digest: SHA1.Digest): State = copy(blobs = blobs + digest)
     def defined_blob(digest: SHA1.Digest): Boolean = blobs.contains(digest)
 
     def define_command(command: Command): State = {
       val id = command.id
       if (commands.isDefinedAt(id)) fail
       else copy(commands = commands + (id -> command.init_state))
     }
 
     def defined_command(id: Document_ID.Command): Boolean = commands.isDefinedAt(id)
 
     def the_version(id: Document_ID.Version): Version = versions.getOrElse(id, fail)
     def the_static_state(id: Document_ID.Command): Command.State = commands.getOrElse(id, fail)
     def the_dynamic_state(id: Document_ID.Exec): Command.State = execs.getOrElse(id, fail)
     def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version.id, fail)
 
     def lookup_id(id: Document_ID.Generic): Option[Command.State] =
       theories.get(id) orElse commands.get(id) orElse execs.get(id)
 
     private def self_id(st: Command.State)(id: Document_ID.Generic): Boolean =
       id == st.command.id ||
       (execs.get(id) match { case Some(st1) => st1.command.id == st.command.id case None => false })
 
     private def other_id(
       node_name: Node.Name,
       id: Document_ID.Generic
     ) : Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)] = {
       for {
         st <- lookup_id(id)
         if st.command.node_name == node_name
       } yield (Symbol.Text_Chunk.Id(st.command.id), st.command.chunk)
     }
 
     private def redirection(st: Command.State): Graph[Document_ID.Command, Unit] =
       st.markups.redirection_iterator.foldLeft(commands_redirection) {
         case (graph, id) =>
           graph.default_node(id, ()).default_node(st.command.id, ()).add_edge(id, st.command.id)
       }
 
     def accumulate(
       id: Document_ID.Generic,
       message: XML.Elem,
       cache: XML.Cache
     ) : (Command.State, State) = {
       def update(st: Command.State): (Command.State, State) = {
         val st1 = st.accumulate(self_id(st), other_id, message, cache)
         (st1, copy(commands_redirection = redirection(st1)))
       }
       execs.get(id).map(update) match {
         case Some((st1, state1)) => (st1, state1.copy(execs = execs + (id -> st1)))
         case None =>
           commands.get(id).map(update) match {
             case Some((st1, state1)) => (st1, state1.copy(commands = commands + (id -> st1)))
             case None =>
               theories.get(id).map(update) match {
                 case Some((st1, state1)) => (st1, state1.copy(theories = theories + (id -> st1)))
                 case None => fail
               }
           }
       }
     }
 
     def add_export(
       id: Document_ID.Generic,
       entry: Command.Exports.Entry
     ): (Command.State, State) = {
       execs.get(id) match {
         case Some(st) =>
           st.add_export(entry) match {
             case Some(new_st) => (new_st, copy(execs = execs + (id -> new_st)))
             case None => fail
           }
         case None =>
           commands.get(id) match {
             case Some(st) =>
               st.add_export(entry) match {
                 case Some(new_st) => (new_st, copy(commands = commands + (id -> new_st)))
                 case None => fail
               }
             case None => fail
           }
       }
     }
 
     def node_exports(version: Version, node_name: Node.Name): Command.Exports =
       Command.Exports.merge(
         for {
           command <- version.nodes(node_name).commands.iterator
           st <- command_states(version, command).iterator
         } yield st.exports)
 
     def begin_theory(
       node_name: Node.Name,
       id: Document_ID.Exec,
       source: String,
       blobs_info: Command.Blobs_Info
     ): State = {
       if (theories.isDefinedAt(id)) fail
       else {
         val command =
           Command.unparsed(source, theory = true, id = id, node_name = node_name,
             blobs_info = blobs_info)
         copy(theories = theories + (id -> command.empty_state))
       }
     }
 
     def end_theory(id: Document_ID.Exec, document_blobs: Node.Name => Blobs): (Snapshot, State) =
       theories.get(id) match {
         case None => fail
         case Some(st) =>
           val command = st.command
           val node_name = command.node_name
           val doc_blobs = document_blobs(node_name)
           val command1 =
             Command.unparsed(command.source, theory = true, id = id, node_name = node_name,
               blobs_info = command.blobs_info, results = st.results, markups = st.markups)
           val state1 = copy(theories = theories - id)
           (state1.snippet(command1, doc_blobs), state1)
       }
 
     def assign(
       id: Document_ID.Version,
       edited: List[String],
       update: Assign_Update
     ) : ((List[Node.Name], List[Command]), State) = {
       val version = the_version(id)
 
       val edited_set = edited.toSet
       val edited_nodes =
         (for { (name, _) <- version.nodes.iterator if edited_set(name.node) } yield name).toList
 
       def upd(
         exec_id: Document_ID.Exec,
         st: Command.State
       ): Option[(Document_ID.Exec, Command.State)] = {
         if (execs.isDefinedAt(exec_id)) None else Some(exec_id -> st)
       }
 
       val (changed_commands, new_execs) =
         update.foldLeft((List.empty[Command], execs)) {
           case ((commands1, execs1), (command_id, exec)) =>
             val st = the_static_state(command_id)
             val command = st.command
             val commands2 = command :: commands1
             val execs2 =
               exec match {
                 case Nil => execs1
                 case eval_id :: print_ids =>
                   execs1 ++ upd(eval_id, st) ++
                     (for (id <- print_ids; up <- upd(id, command.empty_state)) yield up)
               }
             (commands2, execs2)
         }
       val new_assignment = the_assignment(version).assign(update)
       val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs)
 
       ((edited_nodes, changed_commands), new_state)
     }
 
     def is_assigned(version: Version): Boolean =
       assignments.get(version.id) match {
         case Some(assgn) => assgn.is_finished
         case None => false
       }
 
     def is_stable(change: Change): Boolean =
       change.is_finished && is_assigned(change.version.get_finished)
 
     def recent_finished: Change = history.undo_list.find(_.is_finished) getOrElse fail
     def recent_stable: Change = history.undo_list.find(is_stable) getOrElse fail
     def stable_tip_version: Option[Version] =
       if (is_stable(history.tip)) Some(history.tip.version.get_finished) else None
 
     def continue_history(
       previous: Future[Version],
       edits: List[Edit_Text],
       version: Future[Version]
     ): State = {
       val change = Change.make(previous, edits, version)
       copy(history = history + change)
     }
 
     def remove_versions(retain: Int = 0): (List[Version], State) = {
       history.prune(is_stable, retain) match {
         case Some((dropped, history1)) =>
           val old_versions = dropped.map(change => change.version.get_finished)
           val removing = old_versions.nonEmpty
           val state1 = copy(history = history1, removing_versions = removing)
           (old_versions, state1)
         case None => fail
       }
     }
 
     def removed_versions(removed: List[Document_ID.Version]): State = {
       val versions1 = Version.purge_suppressed(versions -- removed)
 
       val assignments1 = assignments -- removed
       var blobs1_names = Set.empty[Node.Name]
       var blobs1 = Set.empty[SHA1.Digest]
       var commands1 = Map.empty[Document_ID.Command, Command.State]
       var execs1 = Map.empty[Document_ID.Exec, Command.State]
       for {
         (version_id, version) <- versions1.iterator
         command_execs = assignments1(version_id).command_execs
         (_, node) <- version.nodes.iterator
         command <- node.commands.iterator
       } {
         for ((name, digest) <- command.blobs_defined) {
           blobs1_names += name
           blobs1 += digest
         }
 
         if (!commands1.isDefinedAt(command.id)) {
           commands.get(command.id).foreach(st => commands1 += (command.id -> st))
         }
 
         for {
           exec_id <- command_execs.getOrElse(command.id, Nil)
           if !execs1.isDefinedAt(exec_id)
           st <- execs.get(exec_id)
         } execs1 += (exec_id -> st)
       }
 
       copy(
         versions = versions1,
         blobs = blobs1,
         commands = commands1,
         execs = execs1,
         commands_redirection = commands_redirection.restrict(commands1.keySet),
         assignments = assignments1,
         history = history.purge(versions1),
         removing_versions = false)
     }
 
     def command_maybe_consolidated(version: Version, command: Command): Boolean = {
       require(is_assigned(version), "version not assigned (command_maybe_consolidated)")
       try {
         the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil) match {
           case eval_id :: print_ids =>
             the_dynamic_state(eval_id).maybe_consolidated &&
             !print_ids.exists(print_id => the_dynamic_state(print_id).consolidating)
           case Nil => false
         }
       }
       catch { case _: State.Fail => false }
     }
 
     private def command_states_self(
       version: Version,
       command: Command
     ) : List[(Document_ID.Generic, Command.State)] = {
       require(is_assigned(version), "version not assigned (command_states_self)")
       try {
         the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil)
           .map(id => id -> the_dynamic_state(id)) match {
             case Nil => fail
             case res => res
           }
       }
       catch {
         case _: State.Fail =>
           try { List(command.id -> the_static_state(command.id)) }
           catch { case _: State.Fail => List(command.id -> command.init_state) }
       }
     }
 
     def command_states(version: Version, command: Command): List[Command.State] = {
       val self = command_states_self(version, command)
       val others =
         if (commands_redirection.defined(command.id)) {
           (for {
             command_id <- commands_redirection.imm_succs(command.id).iterator
             (id, st) <- command_states_self(version, the_static_state(command_id).command)
             if !self.exists(_._1 == id)
           } yield (id, st)).toMap.valuesIterator.toList
         }
         else Nil
       self.map(_._2) ::: others.flatMap(_.redirect(command))
     }
 
     def command_results(version: Version, command: Command): Command.Results =
       Command.State.merge_results(command_states(version, command))
 
     def command_markup(version: Version, command: Command, index: Command.Markup_Index,
         range: Text.Range, elements: Markup.Elements): Markup_Tree =
       Command.State.merge_markup(command_states(version, command), index, range, elements)
 
     def xml_markup(
       version: Version,
       node_name: Node.Name,
       range: Text.Range = Text.Range.full,
       elements: Markup.Elements = Markup.Elements.full
     ): XML.Body = {
       val node = version.nodes(node_name)
       if (node_name.is_theory) {
         val markup_index = Command.Markup_Index.markup
         (for {
           command <- node.commands.iterator
           command_range <- command.range.try_restrict(range).iterator
           markup = command_markup(version, command, markup_index, command_range, elements)
           tree <- markup.to_XML(command_range, command.source, elements).iterator
         } yield tree).toList
       }
       else if (node.source_wellformed) {
         Text.Range.length(node.source).try_restrict(range) match {
           case Some(node_range) =>
             val markup =
               version.nodes.commands_loading(node_name).headOption match {
                 case None => Markup_Tree.empty
                 case Some(command) =>
                   val chunk_name = Symbol.Text_Chunk.File(node_name.node)
                   val markup_index = Command.Markup_Index(false, chunk_name)
                   command_markup(version, command, markup_index, node_range, elements)
               }
             markup.to_XML(node_range, node.source, elements)
           case None => Nil
         }
       }
       else Nil
     }
 
     def node_initialized(version: Version, name: Node.Name): Boolean =
       name.is_theory &&
       (version.nodes(name).commands.iterator.find(_.potentially_initialized) match {
         case None => false
         case Some(command) => command_states(version, command).headOption.exists(_.initialized)
       })
 
     def node_maybe_consolidated(version: Version, name: Node.Name): Boolean =
       name.is_theory &&
       version.nodes(name).commands.reverse.iterator.forall(command_maybe_consolidated(version, _))
 
     def node_consolidated(version: Version, name: Node.Name): Boolean =
       !name.is_theory || {
         val it = version.nodes(name).commands.reverse.iterator
         it.hasNext && command_states(version, it.next()).exists(_.consolidated)
       }
 
     def snapshot(
       node_name: Node.Name = Node.Name.empty,
       pending_edits: Pending_Edits = Pending_Edits.empty,
       snippet_command: Option[Command] = None
     ): Snapshot = {
       val stable = recent_stable
       val version = stable.version.get_finished
 
       val pending_edits1 =
         (for {
           change <- history.undo_list.takeWhile(_ != stable)
           (name, Node.Edits(es)) <- change.rev_edits
         } yield (name -> es)).foldLeft(pending_edits)(_ + _)
 
       new Snapshot(this, version, node_name, pending_edits1, snippet_command)
     }
 
     def snippet(command: Command, doc_blobs: Blobs): Snapshot =
       snapshot().snippet(command, doc_blobs)
   }
 }
diff --git a/src/Pure/Thy/bibtex.scala b/src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala
+++ b/src/Pure/Thy/bibtex.scala
@@ -1,769 +1,769 @@
 /*  Title:      Pure/Thy/bibtex.scala
     Author:     Makarius
 
 BibTeX support.
 */
 
 package isabelle
 
 
 import java.io.{File => JFile}
 
 import scala.collection.mutable
 import scala.util.parsing.combinator.RegexParsers
 import scala.util.parsing.input.Reader
 import scala.util.matching.Regex
 
 
 object Bibtex {
   /** file format **/
 
   class File_Format extends isabelle.File_Format {
     val format_name: String = "bibtex"
     val file_ext: String = "bib"
 
     override def parse_data(name: String, text: String): Bibtex.Entries =
       Bibtex.Entries.parse(text, file_pos = name)
 
     override def theory_suffix: String = "bibtex_file"
     override def theory_content(name: String): String =
       """theory "bib" imports Pure begin bibtex_file "." end"""
     override def theory_excluded(name: String): Boolean = name == "bib"
 
     override def html_document(snapshot: Document.Snapshot): Option[Browser_Info.HTML_Document] = {
       val name = snapshot.node_name
       if (detect(name.node)) {
         val title = "Bibliography " + quote(snapshot.node_name.file_name)
         val content =
           Isabelle_System.with_tmp_file("bib", "bib") { bib =>
             File.write(bib, snapshot.node.source)
             Bibtex.html_output(List(bib), style = "unsort", title = title)
           }
         Some(Browser_Info.HTML_Document(title, content))
       }
       else None
     }
   }
 
 
 
   /** bibtex errors **/
 
   def bibtex_errors(dir: Path, root_name: String): List[String] = {
     val log_path = dir + Path.explode(root_name).ext("blg")
     if (log_path.is_file) {
       val Error1 = """^(I couldn't open database file .+)$""".r
       val Error2 = """^(I found no .+)$""".r
       val Error3 = """^(.+)---line (\d+) of file (.+)""".r
       Line.logical_lines(File.read(log_path)).flatMap(line =>
         line match {
           case Error1(msg) => Some("Bibtex error: " + msg)
           case Error2(msg) => Some("Bibtex error: " + msg)
           case Error3(msg, Value.Int(l), file) =>
             val path = File.standard_path(file)
             if (Path.is_wellformed(path)) {
               val pos = Position.Line_File(l, (dir + Path.explode(path)).canonical.implode)
               Some("Bibtex error" + Position.here(pos) + ":\n  " + msg)
             }
             else None
           case _ => None
         })
     }
     else Nil
   }
 
 
 
   /** check database **/
 
   def check_database(database: String): (List[(String, Position.T)], List[(String, Position.T)]) = {
     val chunks = parse(Line.normalize(database))
     var chunk_pos = Map.empty[String, Position.T]
     val tokens = new mutable.ListBuffer[(Token, Position.T)]
     var line = 1
     var offset = 1
 
     def make_pos(length: Int): Position.T =
       Position.Offset(offset) ::: Position.End_Offset(offset + length) ::: Position.Line(line)
 
     def advance_pos(tok: Token): Unit = {
       for (s <- Symbol.iterator(tok.source)) {
         if (Symbol.is_newline(s)) line += 1
         offset += 1
       }
     }
 
     def get_line_pos(l: Int): Position.T =
       if (0 < l && l <= tokens.length) tokens(l - 1)._2 else Position.none
 
     for (chunk <- chunks) {
       val name = chunk.name
       if (name != "" && !chunk_pos.isDefinedAt(name)) {
         chunk_pos += (name -> make_pos(chunk.heading_length))
       }
       for (tok <- chunk.tokens) {
         tokens += (tok.copy(source = tok.source.replace("\n", " ")) -> make_pos(tok.source.length))
         advance_pos(tok)
       }
     }
 
     Isabelle_System.with_tmp_dir("bibtex") { tmp_dir =>
       File.write(tmp_dir + Path.explode("root.bib"),
         tokens.iterator.map(p => p._1.source).mkString("", "\n", "\n"))
       File.write(tmp_dir + Path.explode("root.aux"),
         "\\bibstyle{plain}\n\\bibdata{root}\n\\citation{*}")
       Isabelle_System.bash("\"$ISABELLE_BIBTEX\" root", cwd = tmp_dir.file)
 
       val Error = """^(.*)---line (\d+) of file root.bib$""".r
       val Warning = """^Warning--(.+)$""".r
       val Warning_Line = """--line (\d+) of file root.bib$""".r
       val Warning_in_Chunk = """^Warning--(.+) in (.+)$""".r
 
       val log_file = tmp_dir + Path.explode("root.blg")
       val lines = if (log_file.is_file) Line.logical_lines(File.read(log_file)) else Nil
 
       val (errors, warnings) =
         if (lines.isEmpty) (Nil, Nil)
         else {
           lines.zip(lines.tail ::: List("")).flatMap(
             {
               case (Error(msg, Value.Int(l)), _) =>
                 Some((true, (msg, get_line_pos(l))))
               case (Warning_in_Chunk(msg, name), _) if chunk_pos.isDefinedAt(name) =>
                 Some((false, (Word.capitalize(msg + " in entry " + quote(name)), chunk_pos(name))))
               case (Warning(msg), Warning_Line(Value.Int(l))) =>
                 Some((false, (Word.capitalize(msg), get_line_pos(l))))
               case (Warning(msg), _) =>
                 Some((false, (Word.capitalize(msg), Position.none)))
               case _ => None
             }
           ).partition(_._1)
         }
       (errors.map(_._2), warnings.map(_._2))
     }
   }
 
   object Check_Database extends Scala.Fun_String("bibtex_check_database") {
     val here = Scala_Project.here
     def apply(database: String): String = {
       import XML.Encode._
       YXML.string_of_body(pair(list(pair(string, properties)), list(pair(string, properties)))(
         check_database(database)))
     }
   }
 
 
 
   /** document model **/
 
   /* entries */
 
   object Entries {
     val empty: Entries = apply(Nil)
 
     def apply(entries: List[Text.Info[String]], errors: List[String] = Nil): Entries =
       new Entries(entries, errors)
 
     def parse(text: String, file_pos: String = ""): Entries = {
       val entries = new mutable.ListBuffer[Text.Info[String]]
       var offset = 0
       var line = 1
       var err_line = 0
 
       try {
         for (chunk <- Bibtex.parse(text)) {
           val end_offset = offset + chunk.source.length
           if (chunk.name != "" && !chunk.is_command) {
             entries += Text.Info(Text.Range(offset, end_offset), chunk.name)
           }
           if (chunk.is_malformed && err_line == 0) { err_line = line }
           offset = end_offset
-          line += chunk.source.count(_ == '\n')
+          line += Library.count_newlines(chunk.source)
         }
 
         val err_pos =
           if (err_line == 0 || file_pos.isEmpty) Position.none
           else Position.Line_File(err_line, file_pos)
         val errors =
           if (err_line == 0) Nil
           else List("Malformed bibtex file" + Position.here(err_pos))
 
         apply(entries.toList, errors = errors)
       }
       catch { case ERROR(msg) => apply(Nil, errors = List(msg)) }
     }
 
     def iterator[A <: Document.Model](models: Iterable[A]): Iterator[Text.Info[(String, A)]] =
       for {
         model <- models.iterator
         bibtex_entries <- model.get_data(classOf[Entries]).iterator
         info <- bibtex_entries.entries.iterator
       } yield info.map((_, model))
   }
 
   final class Entries private(val entries: List[Text.Info[String]], val errors: List[String]) {
     override def toString: String = "Bibtex.Entries(" + entries.length + ")"
 
     def ::: (other: Entries): Entries =
       new Entries(entries ::: other.entries, errors ::: other.errors)
   }
 
 
   /* completion */
 
   def completion[A <: Document.Model](
     history: Completion.History,
     rendering: Rendering,
     caret: Text.Offset,
     models: Iterable[A]
   ): Option[Completion.Result] = {
     for {
       Text.Info(r, name) <- rendering.citations(rendering.before_caret_range(caret)).headOption
       name1 <- Completion.clean_name(name)
 
       original <- rendering.get_text(r)
       original1 <- Completion.clean_name(Library.perhaps_unquote(original))
 
       entries =
         (for {
           Text.Info(_, (entry, _)) <- Entries.iterator(models)
           if entry.toLowerCase.containsSlice(name1.toLowerCase) && entry != original1
         } yield entry).toList
       if entries.nonEmpty
 
       items =
         entries.sorted.map({
           case entry =>
             val full_name = Long_Name.qualify(Markup.CITATION, entry)
             val description = List(entry, "(BibTeX entry)")
             val replacement = quote(entry)
             Completion.Item(r, original, full_name, description, replacement, 0, false)
         }).sorted(history.ordering).take(rendering.options.int("completion_limit"))
     } yield Completion.Result(r, original, false, items)
   }
 
 
 
   /** content **/
 
   private val months = List(
     "jan",
     "feb",
     "mar",
     "apr",
     "may",
     "jun",
     "jul",
     "aug",
     "sep",
     "oct",
     "nov",
     "dec")
   def is_month(s: String): Boolean = months.contains(s.toLowerCase)
 
   private val commands = List("preamble", "string")
   def is_command(s: String): Boolean = commands.contains(s.toLowerCase)
 
   sealed case class Entry(
     kind: String,
     required: List[String],
     optional_crossref: List[String],
     optional_other: List[String]
   ) {
     val optional_standard: List[String] = List("url", "doi", "ee")
 
     def is_required(s: String): Boolean = required.contains(s.toLowerCase)
     def is_optional(s: String): Boolean =
       optional_crossref.contains(s.toLowerCase) ||
       optional_other.contains(s.toLowerCase) ||
       optional_standard.contains(s.toLowerCase)
 
     def fields: List[String] =
       required ::: optional_crossref ::: optional_other ::: optional_standard
 
     def template: String =
       "@" + kind + "{,\n" + fields.map(x => "  " + x + " = {},\n").mkString + "}\n"
   }
 
   val known_entries: List[Entry] =
     List(
       Entry("Article",
         List("author", "title"),
         List("journal", "year"),
         List("volume", "number", "pages", "month", "note")),
       Entry("InProceedings",
         List("author", "title"),
         List("booktitle", "year"),
         List("editor", "volume", "number", "series", "pages", "month", "address",
           "organization", "publisher", "note")),
       Entry("InCollection",
         List("author", "title", "booktitle"),
         List("publisher", "year"),
         List("editor", "volume", "number", "series", "type", "chapter", "pages",
           "edition", "month", "address", "note")),
       Entry("InBook",
         List("author", "editor", "title", "chapter"),
         List("publisher", "year"),
         List("volume", "number", "series", "type", "address", "edition", "month", "pages", "note")),
       Entry("Proceedings",
         List("title", "year"),
         List(),
         List("booktitle", "editor", "volume", "number", "series", "address", "month",
           "organization", "publisher", "note")),
       Entry("Book",
         List("author", "editor", "title"),
         List("publisher", "year"),
         List("volume", "number", "series", "address", "edition", "month", "note")),
       Entry("Booklet",
         List("title"),
         List(),
         List("author", "howpublished", "address", "month", "year", "note")),
       Entry("PhdThesis",
         List("author", "title", "school", "year"),
         List(),
         List("type", "address", "month", "note")),
       Entry("MastersThesis",
         List("author", "title", "school", "year"),
         List(),
         List("type", "address", "month", "note")),
       Entry("TechReport",
         List("author", "title", "institution", "year"),
         List(),
         List("type", "number", "address", "month", "note")),
       Entry("Manual",
         List("title"),
         List(),
         List("author", "organization", "address", "edition", "month", "year", "note")),
       Entry("Unpublished",
         List("author", "title", "note"),
         List(),
         List("month", "year")),
       Entry("Misc",
         List(),
         List(),
         List("author", "title", "howpublished", "month", "year", "note")))
 
   def get_entry(kind: String): Option[Entry] =
     known_entries.find(entry => entry.kind.toLowerCase == kind.toLowerCase)
 
   def is_entry(kind: String): Boolean = get_entry(kind).isDefined
 
 
 
   /** tokens and chunks **/
 
   object Token {
     object Kind extends Enumeration {
       val COMMAND = Value("command")
       val ENTRY = Value("entry")
       val KEYWORD = Value("keyword")
       val NAT = Value("natural number")
       val STRING = Value("string")
       val NAME = Value("name")
       val IDENT = Value("identifier")
       val SPACE = Value("white space")
       val COMMENT = Value("ignored text")
       val ERROR = Value("bad input")
     }
   }
 
   sealed case class Token(kind: Token.Kind.Value, source: String) {
     def is_kind: Boolean =
       kind == Token.Kind.COMMAND ||
       kind == Token.Kind.ENTRY ||
       kind == Token.Kind.IDENT
     def is_name: Boolean =
       kind == Token.Kind.NAME ||
       kind == Token.Kind.IDENT
     def is_ignored: Boolean =
       kind == Token.Kind.SPACE ||
       kind == Token.Kind.COMMENT
     def is_malformed: Boolean =
       kind == Token.Kind.ERROR
     def is_open: Boolean =
       kind == Token.Kind.KEYWORD && (source == "{" || source == "(")
   }
 
   case class Chunk(kind: String, tokens: List[Token]) {
     val source = tokens.map(_.source).mkString
 
     private val content: Option[List[Token]] =
       tokens match {
         case Token(Token.Kind.KEYWORD, "@") :: body if body.nonEmpty =>
           (body.init.filterNot(_.is_ignored), body.last) match {
             case (tok :: Token(Token.Kind.KEYWORD, "{") :: toks, Token(Token.Kind.KEYWORD, "}"))
             if tok.is_kind => Some(toks)
 
             case (tok :: Token(Token.Kind.KEYWORD, "(") :: toks, Token(Token.Kind.KEYWORD, ")"))
             if tok.is_kind => Some(toks)
 
             case _ => None
           }
         case _ => None
       }
 
     def name: String =
       content match {
         case Some(tok :: _) if tok.is_name => tok.source
         case _ => ""
       }
 
     def heading_length: Int =
       if (name == "") 1
       else {
         tokens.takeWhile(tok => !tok.is_open).foldLeft(0) { case (n, tok) => n + tok.source.length }
       }
 
     def is_ignored: Boolean = kind == "" && tokens.forall(_.is_ignored)
     def is_malformed: Boolean = tokens.exists(_.is_malformed)
     def is_command: Boolean = Bibtex.is_command(kind) && name != "" && content.isDefined
     def is_entry: Boolean = Bibtex.is_entry(kind) && name != "" && content.isDefined
   }
 
 
 
   /** parsing **/
 
   // context of partial line-oriented scans
   abstract class Line_Context
   case object Ignored extends Line_Context
   case object At extends Line_Context
   case class Item_Start(kind: String) extends Line_Context
   case class Item_Open(kind: String, end: String) extends Line_Context
   case class Item(kind: String, end: String, delim: Delimited) extends Line_Context
 
   case class Delimited(quoted: Boolean, depth: Int)
   val Closed = Delimited(false, 0)
 
   private def token(kind: Token.Kind.Value)(source: String): Token = Token(kind, source)
   private def keyword(source: String): Token = Token(Token.Kind.KEYWORD, source)
 
 
   // See also https://ctan.org/tex-archive/biblio/bibtex/base/bibtex.web
   // module @<Scan for and process a \.{.bib} command or database entry@>.
 
   object Parsers extends RegexParsers {
     /* white space and comments */
 
     override val whiteSpace = "".r
 
     private val space = """[ \t\n\r]+""".r ^^ token(Token.Kind.SPACE)
     private val spaces = rep(space)
 
 
     /* ignored text */
 
     private val ignored: Parser[Chunk] =
       rep1("""(?i)([^@]+|@[ \t]*comment)""".r) ^^ {
         case ss => Chunk("", List(Token(Token.Kind.COMMENT, ss.mkString))) }
 
     private def ignored_line: Parser[(Chunk, Line_Context)] =
       ignored ^^ { case a => (a, Ignored) }
 
 
     /* delimited string: outermost "..." or {...} and body with balanced {...} */
 
     // see also bibtex.web: scan_a_field_token_and_eat_white, scan_balanced_braces
     private def delimited_depth(delim: Delimited): Parser[(String, Delimited)] =
       new Parser[(String, Delimited)] {
         require(if (delim.quoted) delim.depth > 0 else delim.depth >= 0,
           "bad delimiter depth")
 
         def apply(in: Input) = {
           val start = in.offset
           val end = in.source.length
 
           var i = start
           var q = delim.quoted
           var d = delim.depth
           var finished = false
           while (!finished && i < end) {
             val c = in.source.charAt(i)
 
             if (c == '"' && d == 0) { i += 1; d = 1; q = true }
             else if (c == '"' && d == 1 && q) {
               i += 1; d = 0; q = false; finished = true
             }
             else if (c == '{') { i += 1; d += 1 }
             else if (c == '}') {
               if (d == 1 && !q || d > 1) { i += 1; d -= 1; if (d == 0) finished = true }
               else {i = start; finished = true }
             }
             else if (d > 0) i += 1
             else finished = true
           }
           if (i == start) Failure("bad input", in)
           else {
             val s = in.source.subSequence(start, i).toString
             Success((s, Delimited(q, d)), in.drop(i - start))
           }
         }
       }.named("delimited_depth")
 
     private def delimited: Parser[Token] =
       delimited_depth(Closed) ^?
         { case (s, delim) if delim == Closed => Token(Token.Kind.STRING, s) }
 
     private def recover_delimited: Parser[Token] =
       """["{][^@]*""".r ^^ token(Token.Kind.ERROR)
 
     def delimited_line(ctxt: Item): Parser[(Chunk, Line_Context)] =
       delimited_depth(ctxt.delim) ^^ { case (s, delim1) =>
         (Chunk(ctxt.kind, List(Token(Token.Kind.STRING, s))), ctxt.copy(delim = delim1)) } |
       recover_delimited ^^ { case a => (Chunk(ctxt.kind, List(a)), Ignored) }
 
 
     /* other tokens */
 
     private val at = "@" ^^ keyword
 
     private val nat = "[0-9]+".r ^^ token(Token.Kind.NAT)
 
     private val name = """[\x21-\x7f&&[^"#%'(),={}]]+""".r ^^ token(Token.Kind.NAME)
 
     private val identifier =
       """[\x21-\x7f&&[^"#%'(),={}0-9]][\x21-\x7f&&[^"#%'(),={}]]*""".r
 
     private val ident = identifier ^^ token(Token.Kind.IDENT)
 
     val other_token = "[=#,]".r ^^ keyword | (nat | (ident | space))
 
 
     /* body */
 
     private val body =
       delimited | (recover_delimited | other_token)
 
     private def body_line(ctxt: Item) =
       if (ctxt.delim.depth > 0)
         delimited_line(ctxt)
       else
         delimited_line(ctxt) |
         other_token ^^ { case a => (Chunk(ctxt.kind, List(a)), ctxt) } |
         ctxt.end ^^ { case a => (Chunk(ctxt.kind, List(keyword(a))), Ignored) }
 
 
     /* items: command or entry */
 
     private val item_kind =
       identifier ^^ { case a =>
         val kind =
           if (is_command(a)) Token.Kind.COMMAND
           else if (is_entry(a)) Token.Kind.ENTRY
           else Token.Kind.IDENT
         Token(kind, a)
       }
 
     private val item_begin =
       "{" ^^ { case a => ("}", keyword(a)) } |
       "(" ^^ { case a => (")", keyword(a)) }
 
     private def item_name(kind: String) =
       kind.toLowerCase match {
         case "preamble" => failure("")
         case "string" => identifier ^^ token(Token.Kind.NAME)
         case _ => name
       }
 
     private val item_start =
       at ~ spaces ~ item_kind ~ spaces ^^
         { case a ~ b ~ c ~ d => (c.source, List(a) ::: b ::: List(c) ::: d) }
 
     private val item: Parser[Chunk] =
       (item_start ~ item_begin ~ spaces) into
         { case (kind, a) ~ ((end, b)) ~ c =>
             opt(item_name(kind)) ~ rep(body) ~ opt(end ^^ keyword) ^^ {
               case d ~ e ~ f => Chunk(kind, a ::: List(b) ::: c ::: d.toList ::: e ::: f.toList) } }
 
     private val recover_item: Parser[Chunk] =
       at ~ "[^@]*".r ^^ { case a ~ b => Chunk("", List(a, Token(Token.Kind.ERROR, b))) }
 
 
     /* chunks */
 
     val chunk: Parser[Chunk] = ignored | (item | recover_item)
 
     def chunk_line(ctxt: Line_Context): Parser[(Chunk, Line_Context)] = {
       ctxt match {
         case Ignored =>
           ignored_line |
           at ^^ { case a => (Chunk("", List(a)), At) }
 
         case At =>
           space ^^ { case a => (Chunk("", List(a)), ctxt) } |
           item_kind ^^ { case a => (Chunk(a.source, List(a)), Item_Start(a.source)) } |
           recover_item ^^ { case a => (a, Ignored) } |
           ignored_line
 
         case Item_Start(kind) =>
           space ^^ { case a => (Chunk(kind, List(a)), ctxt) } |
           item_begin ^^ { case (end, a) => (Chunk(kind, List(a)), Item_Open(kind, end)) } |
           recover_item ^^ { case a => (a, Ignored) } |
           ignored_line
 
         case Item_Open(kind, end) =>
           space ^^ { case a => (Chunk(kind, List(a)), ctxt) } |
           item_name(kind) ^^ { case a => (Chunk(kind, List(a)), Item(kind, end, Closed)) } |
           body_line(Item(kind, end, Closed)) |
           ignored_line
 
         case item_ctxt: Item =>
           body_line(item_ctxt) |
           ignored_line
 
         case _ => failure("")
       }
     }
   }
 
 
   /* parse */
 
   def parse(input: CharSequence): List[Chunk] =
     Parsers.parseAll(Parsers.rep(Parsers.chunk), Scan.char_reader(input)) match {
       case Parsers.Success(result, _) => result
       case _ => error("Unexpected failure to parse input:\n" + input.toString)
     }
 
   def parse_line(input: CharSequence, context: Line_Context): (List[Chunk], Line_Context) = {
     var in: Reader[Char] = Scan.char_reader(input)
     val chunks = new mutable.ListBuffer[Chunk]
     var ctxt = context
     while (!in.atEnd) {
       val result = Parsers.parse(Parsers.chunk_line(ctxt), in)
       (result : @unchecked) match {
         case Parsers.Success((x, c), rest) => chunks += x; ctxt = c; in = rest
         case Parsers.NoSuccess(_, rest) =>
           error("Unepected failure to parse input:\n" + rest.source.toString)
       }
     }
     (chunks.toList, ctxt)
   }
 
 
 
   /** HTML output **/
 
   private val output_styles =
     List(
       "" -> "html-n",
       "plain" -> "html-n",
       "alpha" -> "html-a",
       "named" -> "html-n",
       "paragraph" -> "html-n",
       "unsort" -> "html-u",
       "unsortlist" -> "html-u")
 
   def html_output(bib: List[Path],
     title: String = "Bibliography",
     body: Boolean = false,
     citations: List[String] = List("*"),
     style: String = "",
     chronological: Boolean = false
   ): String = {
     Isabelle_System.with_tmp_dir("bibtex") { tmp_dir =>
       /* database files */
 
       val bib_files = bib.map(_.drop_ext)
       val bib_names = {
         val names0 = bib_files.map(_.file_name)
         if (Library.duplicates(names0).isEmpty) names0
         else names0.zipWithIndex.map({ case (name, i) => (i + 1).toString + "-" + name })
       }
 
       for ((a, b) <- bib_files zip bib_names) {
         Isabelle_System.copy_file(a.ext("bib"), tmp_dir + Path.basic(b).ext("bib"))
       }
 
 
       /* style file */
 
       val bst =
         output_styles.toMap.get(style) match {
           case Some(base) => base + (if (chronological) "c" else "") + ".bst"
           case None =>
             error("Bad style for bibtex HTML output: " + quote(style) +
               "\n(expected: " + commas_quote(output_styles.map(_._1)) + ")")
         }
       Isabelle_System.copy_file(Path.explode("$BIB2XHTML_HOME/bst") + Path.explode(bst), tmp_dir)
 
 
       /* result */
 
       val in_file = Path.explode("bib.aux")
       val out_file = Path.explode("bib.html")
 
       File.write(tmp_dir + in_file,
         bib_names.mkString("\\bibdata{", ",", "}\n") +
         citations.map(cite => "\\citation{" + cite + "}\n").mkString)
 
       Isabelle_System.bash(
         "\"$BIB2XHTML_HOME/main/bib2xhtml.pl\" -B \"$ISABELLE_BIBTEX\"" +
           " -u -s " + Bash.string(proper_string(style) getOrElse "empty") +
           (if (chronological) " -c" else "") +
           (if (title != "") " -h " + Bash.string(title) + " " else "") +
           " " + File.bash_path(in_file) + " " + File.bash_path(out_file),
         cwd = tmp_dir.file).check
 
       val html = File.read(tmp_dir + out_file)
 
       if (body) {
         cat_lines(
           split_lines(html).
             dropWhile(line => !line.startsWith("<!-- BEGIN BIBLIOGRAPHY")).reverse.
             dropWhile(line => !line.startsWith("<!-- END BIBLIOGRAPHY")).reverse)
       }
       else html
     }
   }
 
 
 
   /** cite commands and antiquotations **/
 
   def cite_antiquotation(name: String, body: String): String =
     """\<^""" + name + """>\<open>""" + body + """\<close>"""
 
   def cite_antiquotation(name: String, location: String, citations: List[String]): String = {
     val body =
       (if (location.isEmpty) "" else Symbol.cartouche(location) + " in ") +
       citations.map(quote).mkString(" and ")
     cite_antiquotation(name, body)
   }
 
   private val Cite_Command = """\\(cite|nocite|citet|citep)((?:\[[^\]]*\])?)\{([^}]*)\}""".r
   private val Cite_Macro = """\[\s*cite_macro\s*=\s*"?(\w+)"?\]\s*""".r
   private val CITE = "cite"
 
   def update_cite_commands(str: String): String =
     Cite_Command.replaceAllIn(str, { m =>
       val name = m.group(1)
       val loc = m.group(2)
       val location =
         if (loc.startsWith("[") && loc.endsWith("]")) loc.substring(1, loc.length - 1)
         else loc
       val citations = Library.space_explode(',', m.group(3)).map(_.trim)
       Regex.quoteReplacement(cite_antiquotation(name, location, citations))
     })
 
   def update_cite_antiquotation(cite_commands: List[String], str: String): String = {
     val opt_body =
       for {
         str1 <- Library.try_unprefix("@{cite", str)
         str2 <- Library.try_unsuffix("}", str1)
       } yield str2.trim
 
     opt_body match {
       case None => str
       case Some(body0) =>
         val (name, body1) =
           Cite_Macro.findFirstMatchIn(body0) match {
             case None => (CITE, body0)
             case Some(m) => (m.group(1), Cite_Macro.replaceAllIn(body0, ""))
           }
         val body2 = body1.replace("""\<close>""", """\<close> in""")
         if (cite_commands.contains(name)) cite_antiquotation(name, body2)
         else cite_antiquotation(CITE, body2 + " using " + quote(name))
     }
   }
 }
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,483 +1,483 @@
 /*  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.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))
 
   def append_position(path: Path, file_pos: String): Unit = {
     val pos = init_position(file_pos).mkString
     if (pos.nonEmpty) {
       val sep = if (File.read(path).endsWith("\n")) "" else "\n"
       File.append(path, sep + pos)
     }
   }
 
   def copy_file(src: Path, dst: Path): Unit = {
     Isabelle_System.copy_file(src, dst)
     if (src.is_latex) {
       val target = if (dst.is_dir) dst + src.base else dst
       val file_pos = File.symbolic_path(src)
       append_position(target, file_pos)
     }
   }
 
   def copy_file_base(base_dir: Path, src: Path, target_dir: Path): Unit = {
     Isabelle_System.copy_file_base(base_dir, src, target_dir)
     if (src.is_latex) {
       val file_pos = File.symbolic_path(base_dir + src)
       append_position(target_dir + src, 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 = "",
       line_pos: Properties.T => Option[Int] = Position.Line.unapply
     ): 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')
+            line += Library.count_newlines(s)
             result += s
           case elem @ XML.Elem(markup, body) =>
             val a = Markup.Optional_Argument.get(markup.properties)
             traverse {
               markup match {
                 case Markup.Document_Latex(props) =>
                   if (positions.nonEmpty) {
                     for (l <- line_pos(props)) {
                       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, source_file.getOrElse(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)
   }
 }
diff --git a/src/Pure/library.scala b/src/Pure/library.scala
--- a/src/Pure/library.scala
+++ b/src/Pure/library.scala
@@ -1,297 +1,299 @@
 /*  Title:      Pure/library.scala
     Author:     Makarius
 
 Basic library.
 */
 
 package isabelle
 
 
 import scala.annotation.tailrec
 import scala.collection.mutable
 import scala.util.matching.Regex
 
 
 object Library {
   /* resource management */
 
   def using[A <: AutoCloseable, B](a: A)(f: A => B): B = {
     try { f(a) }
     finally { if (a != null) a.close() }
   }
 
 
   /* integers */
 
   private val small_int = 10000
   private lazy val small_int_table = {
     val array = new Array[String](small_int)
     for (i <- 0 until small_int) array(i) = i.toString
     array
   }
 
   def is_small_int(s: String): Boolean = {
     val len = s.length
     1 <= len && len <= 4 &&
     s.forall(c => '0' <= c && c <= '9') &&
     (len == 1 || s(0) != '0')
   }
 
   def signed_string_of_long(i: Long): String =
     if (0 <= i && i < small_int) small_int_table(i.toInt)
     else i.toString
 
   def signed_string_of_int(i: Int): String =
     if (0 <= i && i < small_int) small_int_table(i)
     else i.toString
 
 
   /* separated chunks */
 
   def separate[A](s: A, list: List[A]): List[A] = {
     val result = new mutable.ListBuffer[A]
     var first = true
     for (x <- list) {
       if (first) {
         first = false
         result += x
       }
       else {
         result += s
         result += x
       }
     }
     result.toList
   }
 
   def separated_chunks(sep: Char => Boolean, source: CharSequence): Iterator[CharSequence] =
     new Iterator[CharSequence] {
       private val end = source.length
       private def next_chunk(i: Int): Option[(CharSequence, Int)] = {
         if (i < end) {
           var j = i
           while ({
             j += 1
             j < end && !sep(source.charAt(j))
           }) ()
           Some((source.subSequence(i + 1, j), j))
         }
         else None
       }
       private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1)
 
       def hasNext: Boolean = state.isDefined
       def next(): CharSequence =
         state match {
           case Some((s, i)) => state = next_chunk(i); s
           case None => Iterator.empty.next()
         }
     }
 
   def space_explode(sep: Char, str: String): List[String] =
     separated_chunks(_ == sep, str).map(_.toString).toList
 
 
   /* lines */
 
+  def count_newlines(str: String): Int = str.count(_ == '\n')
+
   def terminate_lines(lines: IterableOnce[String]): String = {
     val it = lines.iterator
     if (it.isEmpty) "" else it.mkString("", "\n", "\n")
   }
 
   def cat_lines(lines: IterableOnce[String]): String =
     lines.iterator.mkString("\n")
 
   def split_lines(str: String): List[String] = space_explode('\n', str)
 
   def prefix_lines(prfx: String, str: String): String =
     isabelle.setup.Library.prefix_lines(prfx, str)
 
   def indent_lines(n: Int, str: String): String =
     prefix_lines(Symbol.spaces(n), str)
 
   def first_line(source: CharSequence): String = {
     val lines = separated_chunks(_ == '\n', source)
     if (lines.hasNext) lines.next().toString
     else ""
   }
 
   def trim_line(s: String): String =
     isabelle.setup.Library.trim_line(s)
 
   def trim_split_lines(s: String): List[String] =
     split_lines(trim_line(s)).map(trim_line)
 
   def encode_lines(s: String): String = s.replace('\n', '\u000b')
   def decode_lines(s: String): String = s.replace('\u000b', '\n')
 
 
   /* strings */
 
   def make_string(f: StringBuilder => Unit, capacity: Int = 16): String = {
     val s = new StringBuilder(capacity)
     f(s)
     s.toString
   }
 
   def try_unprefix(prfx: String, s: String): Option[String] =
     if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None
 
   def try_unsuffix(sffx: String, s: String): Option[String] =
     if (s.endsWith(sffx)) Some(s.substring(0, s.length - sffx.length)) else None
 
   def perhaps_unprefix(prfx: String, s: String): String = try_unprefix(prfx, s) getOrElse s
   def perhaps_unsuffix(sffx: String, s: String): String = try_unsuffix(sffx, s) getOrElse s
 
   def isolate_substring(s: String): String = new String(s.toCharArray)
 
   def strip_ansi_color(s: String): String =
     s.replaceAll("\u001b\\[\\d+m", "")
 
 
   /* quote */
 
   def single_quote(s: String): String = "'" + s + "'"
 
   def quote(s: String): String = "\"" + s + "\""
 
   def try_unquote(s: String): Option[String] =
     if (s.startsWith("\"") && s.endsWith("\"")) Some(s.substring(1, s.length - 1))
     else None
 
   def perhaps_unquote(s: String): String = try_unquote(s) getOrElse s
 
   def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ")
   def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ")
 
 
   /* CharSequence */
 
   class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence {
     require(0 <= start && start <= end && end <= text.length, "bad reverse range")
 
     def this(text: CharSequence) = this(text, 0, text.length)
 
     def length: Int = end - start
     def charAt(i: Int): Char = text.charAt(end - i - 1)
 
     def subSequence(i: Int, j: Int): CharSequence =
       if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
       else throw new IndexOutOfBoundsException
 
     override def toString: String = {
       val buf = new StringBuilder(length)
       for (i <- 0 until length)
         buf.append(charAt(i))
       buf.toString
     }
   }
 
   class Line_Termination(text: CharSequence) extends CharSequence {
     def length: Int = text.length + 1
     def charAt(i: Int): Char = if (i == text.length) '\n' else text.charAt(i)
     def subSequence(i: Int, j: Int): CharSequence =
       if (j == text.length + 1) new Line_Termination(text.subSequence(i, j - 1))
       else text.subSequence(i, j)
     override def toString: String = text.toString + "\n"
   }
 
 
   /* regular expressions */
 
   def make_regex(s: String): Option[Regex] =
     try { Some(new Regex(s)) } catch { case ERROR(_) => None }
 
   def is_regex_meta(c: Char): Boolean = """()[]{}\^$|?*+.<>-=!""".contains(c)
 
   def escape_regex(s: String): String =
     if (s.exists(is_regex_meta)) {
       (for (c <- s.iterator)
        yield { if (is_regex_meta(c)) "\\" + c.toString else c.toString }).mkString
     }
     else s
 
 
   /* lists */
 
   def take_prefix[A](pred: A => Boolean, xs: List[A]): (List[A], List[A]) =
     (xs.takeWhile(pred), xs.dropWhile(pred))
 
   def take_suffix[A](pred: A => Boolean, xs: List[A]): (List[A], List[A]) = {
     val rev_xs = xs.reverse
     (rev_xs.dropWhile(pred).reverse, rev_xs.takeWhile(pred).reverse)
   }
 
   def trim[A](pred: A => Boolean, xs: List[A]): List[A] =
     take_suffix(pred, take_prefix(pred, xs)._2)._1
 
   def member[A, B](xs: List[A])(x: B): Boolean = xs.contains(x)
   def insert[A](x: A)(xs: List[A]): List[A] = if (xs.contains(x)) xs else x :: xs
   def remove[A, B](x: B)(xs: List[A]): List[A] = if (member(xs)(x)) xs.filterNot(_ == x) else xs
   def update[A](x: A)(xs: List[A]): List[A] = x :: remove(x)(xs)
 
   def merge[A](xs: List[A], ys: List[A]): List[A] =
     if (xs.eq(ys)) xs
     else if (xs.isEmpty) ys
     else ys.foldRight(xs)(Library.insert(_)(_))
 
   def distinct[A](xs: List[A], eq: (A, A) => Boolean = (x: A, y: A) => x == y): List[A] = {
     val result = new mutable.ListBuffer[A]
     xs.foreach(x => if (!result.exists(y => eq(x, y))) result += x)
     result.toList
   }
 
   def duplicates[A](lst: List[A], eq: (A, A) => Boolean = (x: A, y: A) => x == y): List[A] = {
     val result = new mutable.ListBuffer[A]
     @tailrec def dups(rest: List[A]): Unit =
       rest match {
         case Nil =>
         case x :: xs =>
           if (!result.exists(y => eq(x, y)) && xs.exists(y => eq(x, y))) result += x
           dups(xs)
       }
     dups(lst)
     result.toList
   }
 
   def replicate[A](n: Int, a: A): List[A] =
     if (n < 0) throw new IllegalArgumentException
     else if (n == 0) Nil
     else {
       val res = new mutable.ListBuffer[A]
       (1 to n).foreach(_ => res += a)
       res.toList
     }
 
   def the_single[A](xs: List[A]): A =
     xs match {
       case List(x) => x
       case _ => error("Single argument expected")
     }
 
 
   /* proper values */
 
   def proper_bool(b: Boolean): Option[Boolean] =
     if (!b) None else Some(b)
 
   def proper_string(s: String): Option[String] =
     if (s == null || s == "") None else Some(s)
 
   def proper_list[A](list: List[A]): Option[List[A]] =
     if (list == null || list.isEmpty) None else Some(list)
 
 
   /* reflection */
 
   def is_subclass[A, B](a: Class[A], b: Class[B]): Boolean = {
     import scala.language.existentials
     @tailrec def subclass(c: Class[_]): Boolean = {
       c == b || { val d = c.getSuperclass; d != null && subclass(d) }
     }
     subclass(a)
   }
 
   def as_subclass[C](c: Class[C])(x: AnyRef): Option[C] =
     if (x == null || is_subclass(x.getClass, c)) Some(x.asInstanceOf[C]) else None
 }
diff --git a/src/Tools/jEdit/src/pretty_tooltip.scala b/src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala
@@ -1,280 +1,280 @@
 /*  Title:      Tools/jEdit/src/pretty_tooltip.scala
     Author:     Makarius
 
 Tooltip based on Pretty_Text_Area.
 */
 
 package isabelle.jedit
 
 
 import isabelle._
 
 import java.awt.{Color, Point, BorderLayout, Dimension}
 import java.awt.event.{FocusAdapter, FocusEvent}
 import javax.swing.{JPanel, JComponent, SwingUtilities, JLayeredPane}
 import javax.swing.border.LineBorder
 
 import scala.swing.{FlowPanel, Label}
 import scala.swing.event.MouseClicked
 
 import org.gjt.sp.jedit.View
 import org.gjt.sp.jedit.textarea.TextArea
 
 
 object Pretty_Tooltip {
   /* tooltip hierarchy */
 
   // owned by GUI thread
   private var stack: List[Pretty_Tooltip] = Nil
 
   private def hierarchy(
     tip: Pretty_Tooltip
   ): Option[(List[Pretty_Tooltip], List[Pretty_Tooltip])] = {
     GUI_Thread.require {}
 
     if (stack.contains(tip)) Some(stack.span(_ != tip))
     else None
   }
 
   private def descendant(parent: JComponent): Option[Pretty_Tooltip] =
     GUI_Thread.require { stack.find(tip => tip.original_parent == parent) }
 
   def apply(
     view: View,
     parent: JComponent,
     location: Point,
     rendering: JEdit_Rendering,
     results: Command.Results,
     info: Text.Info[XML.Body]
   ): Unit = {
     GUI_Thread.require {}
 
     stack match {
       case top :: _ if top.results == results && top.info == info =>
       case _ =>
         GUI.layered_pane(parent) match {
           case None =>
           case Some(layered) =>
             val (old, rest) =
               GUI.ancestors(parent).collectFirst({ case x: Pretty_Tooltip => x }) match {
                 case Some(tip) => hierarchy(tip).getOrElse((stack, Nil))
                 case None => (stack, Nil)
               }
             old.foreach(_.hide_popup())
 
             val loc = SwingUtilities.convertPoint(parent, location, layered)
             val tip = new Pretty_Tooltip(view, layered, parent, loc, rendering, results, info)
             stack = tip :: rest
             tip.show_popup()
         }
     }
   }
 
 
   /* pending event and active state */  // owned by GUI thread
 
   private var pending: Option[() => Unit] = None
   private var active = true
 
   private val pending_delay =
     Delay.last(PIDE.options.seconds("jedit_tooltip_delay"), gui = true) {
       pending match {
         case Some(body) => pending = None; body()
         case None =>
       }
     }
 
   def invoke(body: () => Unit): Unit =
     GUI_Thread.require {
       if (active) {
         pending = Some(body)
         pending_delay.invoke()
       }
     }
 
   def revoke(): Unit =
     GUI_Thread.require {
       pending = None
       pending_delay.revoke()
     }
 
   private lazy val reactivate_delay =
     Delay.last(PIDE.options.seconds("jedit_tooltip_delay"), gui = true) {
       active = true
     }
 
   private def deactivate(): Unit =
     GUI_Thread.require {
       revoke()
       active = false
       reactivate_delay.invoke()
     }
 
 
   /* dismiss */
 
   private lazy val focus_delay =
     Delay.last(PIDE.session.input_delay, gui = true) { dismiss_unfocused() }
 
   def dismiss_unfocused(): Unit = {
     stack.span(tip => !tip.pretty_text_area.isFocusOwner) match {
       case (Nil, _) =>
       case (unfocused, rest) =>
         deactivate()
         unfocused.foreach(_.hide_popup())
         stack = rest
     }
   }
 
   def dismiss(tip: Pretty_Tooltip): Unit = {
     deactivate()
     hierarchy(tip) match {
       case Some((old, _ :: rest)) =>
         rest match {
           case top :: _ => top.request_focus()
           case Nil => JEdit_Lib.request_focus_view()
         }
         old.foreach(_.hide_popup())
         tip.hide_popup()
         stack = rest
       case _ =>
     }
   }
 
   def dismiss_descendant(parent: JComponent): Unit =
     descendant(parent).foreach(dismiss)
 
   def dismissed_all(): Boolean = {
     deactivate()
     if (stack.isEmpty) false
     else {
       JEdit_Lib.request_focus_view()
       stack.foreach(_.hide_popup())
       stack = Nil
       true
     }
   }
 }
 
 
 class Pretty_Tooltip private(
   view: View,
   layered: JLayeredPane,
   val original_parent: JComponent,
   location: Point,
   rendering: JEdit_Rendering,
   private val results: Command.Results,
   private val info: Text.Info[XML.Body]
 ) extends JPanel(new BorderLayout) {
   tip =>
 
   GUI_Thread.require {}
 
 
   /* controls */
 
   private val close = new Label {
     icon = rendering.tooltip_close_icon
     tooltip = "Close tooltip window"
     listenTo(mouse.clicks)
     reactions += { case _: MouseClicked => Pretty_Tooltip.dismiss(tip) }
   }
 
   private val detach = new Label {
     icon = rendering.tooltip_detach_icon
     tooltip = "Detach tooltip window"
     listenTo(mouse.clicks)
     reactions += {
       case _: MouseClicked =>
         Info_Dockable(view, rendering.snapshot, results, info.info)
         Pretty_Tooltip.dismiss(tip)
     }
   }
 
   private val controls = new FlowPanel(FlowPanel.Alignment.Left)(close, detach) {
     background = rendering.tooltip_color
   }
 
 
   /* text area */
 
   val pretty_text_area: Pretty_Text_Area =
     new Pretty_Text_Area(view, () => Pretty_Tooltip.dismiss(tip), true) {
       override def get_background(): Option[Color] = Some(rendering.tooltip_color)
     }
 
   pretty_text_area.addFocusListener(new FocusAdapter {
     override def focusGained(e: FocusEvent): Unit = {
       tip_border(true)
       Pretty_Tooltip.focus_delay.invoke()
     }
     override def focusLost(e: FocusEvent): Unit = {
       tip_border(false)
       Pretty_Tooltip.focus_delay.invoke()
     }
   })
 
   pretty_text_area.resize(Font_Info.main(PIDE.options.real("jedit_popup_font_scale")))
 
 
   /* main content */
 
   def tip_border(has_focus: Boolean): Unit = {
     tip.setBorder(new LineBorder(if (has_focus) Color.BLACK else Color.GRAY))
     tip.repaint()
   }
   tip_border(true)
 
   override def getFocusTraversalKeysEnabled = false
   tip.setBackground(rendering.tooltip_color)
   tip.add(controls.peer, BorderLayout.NORTH)
   tip.add(pretty_text_area)
 
 
   /* popup */
 
   private val popup = {
     val screen = GUI.screen_location(layered, location)
     val size = {
       val bounds = JEdit_Rendering.popup_bounds
 
       val w_max = layered.getWidth min (screen.bounds.width * bounds).toInt
       val h_max = layered.getHeight min (screen.bounds.height * bounds).toInt
 
       val painter = pretty_text_area.getPainter
       val geometry = JEdit_Lib.window_geometry(tip, painter)
       val metric = JEdit_Lib.pretty_metric(painter)
 
       val margin =
         ((rendering.tooltip_margin * metric.average) min
           ((w_max - geometry.deco_width) / metric.unit).toInt) max 20
 
       val formatted = Pretty.formatted(info.info, margin = margin, metric = metric)
       val lines =
         XML.traverse_text(formatted)(if (XML.text_length(formatted) == 0) 0 else 1)(
-          (n: Int, s: String) => n + s.iterator.count(_ == '\n'))
+          (n: Int, s: String) => n + Library.count_newlines(s))
 
       val h = painter.getLineHeight * lines + geometry.deco_height
       val margin1 =
         if (h <= h_max) {
           split_lines(XML.content(formatted)).foldLeft(0.0) { case (m, line) => m max metric(line) }
         }
         else margin
       val w = (metric.unit * (margin1 + metric.average)).round.toInt + geometry.deco_width
 
       new Dimension(w min w_max, h min h_max)
     }
     new Popup(layered, tip, screen.relative(layered, size), size)
   }
 
   private def show_popup(): Unit = {
     popup.show
     pretty_text_area.requestFocus()
     pretty_text_area.update(rendering.snapshot, results, info.info)
   }
 
   private def hide_popup(): Unit = popup.hide
 
   private def request_focus(): Unit = pretty_text_area.requestFocus()
 }