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,1224 +1,1226 @@
 /*  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 */
 
   sealed case class Blob(bytes: Bytes, source: String, chunk: Symbol.Text_Chunk, changed: Boolean) {
     def unchanged: Blob = copy(changed = false)
   }
 
   object Blobs {
     def apply(blobs: Map[Node.Name, Blob]): Blobs = new Blobs(blobs)
     val empty: Blobs = apply(Map.empty)
   }
 
   final class Blobs private(blobs: Map[Node.Name, Blob]) {
     def get(name: Node.Name): Option[Blob] = 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 {
       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, symmetric = true)(Ordering)
     }
 
     sealed case class Name(node: String, master_dir: String = "", 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 path: Path = Path.explode(File.standard_path(node))
       def master_dir_path: Path = Path.explode(File.standard_path(master_dir))
 
       def expand: Name =
         Name(path.expand.implode, master_dir_path.expand.implode, theory)
 
       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 map(f: String => String): Name = copy(f(node), f(master_dir), theory)
       def map_theory(f: String => String): Name = copy(node, master_dir, f(theory))
 
       def json: JSON.Object.T =
         JSON.Object("node_name" -> node, "theory_name" -> theory)
     }
 
     sealed case class Entry(name: Node.Name, header: Node.Header) {
       def map(f: String => String): Entry = copy(name = name.map(f))
 
       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: Document.Blob) 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 */
 
     type Perspective_Text = Perspective[Text.Edit, Text.Perspective]
     type Perspective_Command = Perspective[Command.Edit, Command.Perspective]
 
     val no_perspective_text: Perspective_Text =
       Perspective(false, Text.Perspective.empty, Overlays.empty)
 
     val no_perspective_command: Perspective_Command =
       Perspective(false, Command.Perspective.empty, Overlays.empty)
 
     def is_no_perspective_text(perspective: Perspective_Text): Boolean =
       !perspective.required &&
       perspective.visible.is_empty &&
       perspective.overlays.is_empty
 
     def is_no_perspective_command(perspective: Perspective_Command): 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],
         offset: Text.Offset = 0
       ) : Iterator[(Command, Text.Offset)] = {
         var i = offset
         for (command <- commands) yield {
           val start = i
           i += command.length
           (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 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()
   }
 
   final class Node private(
     val get_blob: Option[Document.Blob] = 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 = Node.no_perspective_command,
     _commands: Node.Commands = Node.Commands.empty
   ) {
     def is_empty: Boolean =
       get_blob.isEmpty &&
       header == Node.no_header &&
       text_perspective.is_empty &&
       Node.is_no_perspective_command(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 load_commands: List[Command] = _commands.load_commands
     def load_commands_changed(doc_blobs: Blobs): Boolean =
       load_commands.exists(_.blobs_changed(doc_blobs))
 
     def init_blob(blob: Blob): Node = new Node(get_blob = Some(blob.unchanged))
 
     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): 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): 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: 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 Snapshot {
     val init: Snapshot = State.init.snapshot()
   }
 
   class Snapshot private[Document](
     val state: State,
     val version: Version,
     val node_name: Node.Name,
     edits: List[Text.Edit],
     val snippet_command: Option[Command]
   ) {
     override def toString: String =
       "Snapshot(node = " + node_name.node + ", version = " + version.id +
         (if (is_outdated) ", outdated" else "") + ")"
 
 
     /* 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)
 
 
     /* source text */
 
     def source: String =
       snippet_command match {
         case Some(command) => command.source
         case None => node.source
       }
 
 
     /* edits */
 
     def is_outdated: Boolean = edits.nonEmpty
 
     private lazy val reverse_edits = edits.reverse
 
     def convert(offset: Text.Offset): Text.Offset =
       edits.foldLeft(offset) { case (i, edit) => edit.convert(i) }
     def revert(offset: Text.Offset): Text.Offset =
       reverse_edits.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): Snapshot = {
       val node_name = command.node_name
 
       val nodes0 = version.nodes
       val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command)))
       val version1 = Document.Version.make(nodes1)
 
       val edits: List[Edit_Text] =
         List(node_name -> Node.Edits(List(Text.Edit.insert(0, command.source))))
 
       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))
     }
 
 
     /* XML markup */
 
     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)
 
     def xml_markup_blobs(
       elements: Markup.Elements = Markup.Elements.full
     ) : List[(Command.Blob, XML.Body)] = {
       snippet_command match {
         case None => Nil
         case Some(command) =>
           for (Exn.Res(blob) <- command.blobs)
           yield {
             val bytes = blob.read_file
             val text = bytes.text
             val xml =
               if (Bytes(text) == bytes) {
                 val markup = command.init_markups(Command.Markup_Index.blob(blob))
                 markup.to_XML(Text.Range.length(text), text, elements)
               }
               else Nil
             blob -> xml
           }
       }
     }
 
 
     /* messages */
 
     lazy val messages: List[(XML.Elem, Position.T)] =
       (for {
         (command, start) <-
           Document.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 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 snapshot(): Snapshot
 
     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_required(document: Boolean): Boolean
+    def node_required: Boolean = get_required(false) || get_required(true)
+
     def get_blob: Option[Blob]
     def bibtex_entries: List[Text.Info[String]]
 
     def node_edits(
       node_header: Node.Header,
       text_edits: List[Text.Edit],
       perspective: Node.Perspective_Text
     ): 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): (Snapshot, State) =
       theories.get(id) match {
         case None => fail
         case Some(st) =>
           val command = st.command
           val node_name = command.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), 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))
             execs.get(exec_id).foreach(st => 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 {
         Text.Range.length(node.source).try_restrict(range) match {
           case None => Nil
           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)
         }
       }
     }
 
     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: List[Text.Edit] = Nil,
       snippet_command: Option[Command] = None
     ): Snapshot = {
       val stable = recent_stable
       val version = stable.version.get_finished
 
       val rev_pending_changes =
         for {
           change <- history.undo_list.takeWhile(_ != stable)
           (name, edits) <- change.rev_edits
           if name == node_name
         } yield edits
 
       val edits =
         rev_pending_changes.foldLeft(pending_edits) {
           case (edits, Node.Edits(es)) => es ::: edits
           case (edits, _) => edits
         }
 
       new Snapshot(this, version, node_name, edits, snippet_command)
     }
 
     def snippet(command: Command): Snapshot =
       snapshot().snippet(command)
   }
 }
diff --git a/src/Tools/VSCode/src/vscode_model.scala b/src/Tools/VSCode/src/vscode_model.scala
--- a/src/Tools/VSCode/src/vscode_model.scala
+++ b/src/Tools/VSCode/src/vscode_model.scala
@@ -1,244 +1,250 @@
 /*  Title:      Tools/VSCode/src/vscode_model.scala
     Author:     Makarius
 
 VSCode document model for line-oriented text.
 */
 
 package isabelle.vscode
 
 
 import isabelle._
 
 import java.io.{File => JFile}
 
 
 object VSCode_Model {
   /* decorations */
 
   object Decoration {
     def empty(typ: String): Decoration = Decoration(typ, Nil)
 
     def ranges(typ: String, ranges: List[Text.Range]): Decoration =
       Decoration(typ, ranges.map(Text.Info(_, List.empty[XML.Body])))
   }
   sealed case class Decoration(typ: String, content: List[Text.Info[List[XML.Body]]])
 
 
   /* content */
 
   object Content {
     val empty: Content = Content(Line.Document.empty)
   }
 
   sealed case class Content(doc: Line.Document) {
     override def toString: String = doc.toString
     def text_length: Text.Offset = doc.text_length
     def text_range: Text.Range = doc.text_range
     def text: String = doc.text
 
     lazy val bytes: Bytes = Bytes(Symbol.encode(text))
     lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
     lazy val bibtex_entries: List[Text.Info[String]] =
       try { Bibtex.entries(text) }
       catch { case ERROR(_) => Nil }
 
     def recode_symbols: List[LSP.TextEdit] =
       (for {
         (line, l) <- doc.lines.iterator.zipWithIndex
         text1 = Symbol.encode(line.text)
         if (line.text != text1)
       } yield {
         val range = Line.Range(Line.Position(l), Line.Position(l, line.text.length))
         LSP.TextEdit(range, text1)
       }).toList
   }
 
   def init(
     session: Session,
     editor: Language_Server.Editor,
     node_name: Document.Node.Name
   ): VSCode_Model = {
     VSCode_Model(session, editor, node_name, Content.empty,
-      node_required = File_Format.registry.is_theory(node_name))
+      theory_required = File_Format.registry.is_theory(node_name))
   }
 }
 
 sealed case class VSCode_Model(
   session: Session,
   editor: Language_Server.Editor,
   node_name: Document.Node.Name,
   content: VSCode_Model.Content,
   version: Option[Long] = None,
   external_file: Boolean = false,
-  node_required: Boolean = false,
+  theory_required: Boolean = false,
+  document_required: Boolean = false,
   last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
   pending_edits: List[Text.Edit] = Nil,
   published_diagnostics: List[Text.Info[Command.Results]] = Nil,
   published_decorations: List[VSCode_Model.Decoration] = Nil
 ) extends Document.Model {
   model =>
 
+  /* required */
+
+  def get_required(document: Boolean): Boolean =
+    if (document) document_required else theory_required
+
 
   /* content */
 
   def get_text(range: Text.Range): Option[String] = content.doc.get_text(range)
 
   def set_version(new_version: Long): VSCode_Model = copy(version = Some(new_version))
 
 
   /* external file */
 
   def external(b: Boolean): VSCode_Model = copy(external_file = b)
 
   def node_visible: Boolean = !external_file
 
 
   /* header */
 
   def node_header: Document.Node.Header =
     resources.special_header(node_name) getOrElse
       resources.check_thy(node_name, Scan.char_reader(content.text))
 
 
   /* perspective */
 
   def node_perspective(
     doc_blobs: Document.Blobs,
     caret: Option[Line.Position]
   ): (Boolean, Document.Node.Perspective_Text) = {
     if (is_theory) {
       val snapshot = model.snapshot()
 
       val caret_perspective = resources.options.int("vscode_caret_perspective") max 0
       val caret_range =
         if (caret_perspective != 0) {
           caret match {
             case Some(pos) =>
               val doc = content.doc
               val pos1 = Line.Position((pos.line - caret_perspective) max 0)
               val pos2 = Line.Position((pos.line + caret_perspective + 1) min doc.lines.length)
               Text.Range(doc.offset(pos1).get, doc.offset(pos2).get)
             case None => Text.Range.offside
           }
         }
         else if (node_visible) content.text_range
         else Text.Range.offside
 
       val text_perspective =
         if (snapshot.commands_loading_ranges(resources.visible_node(_)).nonEmpty)
           Text.Perspective.full
         else
           content.text_range.try_restrict(caret_range) match {
             case Some(range) => Text.Perspective(List(range))
             case None => Text.Perspective.empty
           }
 
       val overlays = editor.node_overlays(node_name)
 
       (snapshot.node.load_commands_changed(doc_blobs),
         Document.Node.Perspective(node_required, text_perspective, overlays))
     }
     else (false, Document.Node.no_perspective_text)
   }
 
 
   /* blob */
 
   def get_blob: Option[Document.Blob] =
     if (is_theory) None
     else Some(Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty))
 
 
   /* bibtex entries */
 
   def bibtex_entries: List[Text.Info[String]] =
     model.content.bibtex_entries
 
 
   /* edits */
 
   def change_text(text: String, range: Option[Line.Range] = None): Option[VSCode_Model] = {
     val insert = Line.normalize(text)
     range match {
       case None =>
         Text.Edit.replace(0, content.text, insert) match {
           case Nil => None
           case edits =>
             val content1 = VSCode_Model.Content(Line.Document(insert))
             Some(copy(content = content1, pending_edits = pending_edits ::: edits))
         }
       case Some(remove) =>
         content.doc.change(remove, insert) match {
           case None => error("Failed to apply document change: " + remove)
           case Some((Nil, _)) => None
           case Some((edits, doc1)) =>
             val content1 = VSCode_Model.Content(doc1)
             Some(copy(content = content1, pending_edits = pending_edits ::: edits))
         }
     }
   }
 
   def flush_edits(
       unicode_symbols: Boolean,
       doc_blobs: Document.Blobs,
       file: JFile,
       caret: Option[Line.Position]
   ): Option[((List[LSP.TextDocumentEdit], List[Document.Edit_Text]), VSCode_Model)] = {
     val workspace_edits =
       if (unicode_symbols && version.isDefined) {
         val edits = content.recode_symbols
         if (edits.nonEmpty) List(LSP.TextDocumentEdit(file, version.get, edits))
         else Nil
       }
       else Nil
 
     val (reparse, perspective) = node_perspective(doc_blobs, caret)
     if (reparse || pending_edits.nonEmpty || last_perspective != perspective ||
         workspace_edits.nonEmpty) {
       val prover_edits = node_edits(node_header, pending_edits, perspective)
       val edits = (workspace_edits, prover_edits)
       Some((edits, copy(pending_edits = Nil, last_perspective = perspective)))
     }
     else None
   }
 
 
   /* publish annotations */
 
   def publish(
     rendering: VSCode_Rendering
   ): (Option[List[Text.Info[Command.Results]]], Option[List[VSCode_Model.Decoration]], VSCode_Model) = {
     val diagnostics = rendering.diagnostics
     val decorations =
       if (node_visible) rendering.decorations
       else { for (deco <- published_decorations) yield VSCode_Model.Decoration.empty(deco.typ) }
 
     val changed_diagnostics =
       if (diagnostics == published_diagnostics) None else Some(diagnostics)
     val changed_decorations =
       if (decorations == published_decorations) None
       else if (published_decorations.isEmpty) Some(decorations)
       else Some(for { (a, b) <- decorations zip published_decorations if a != b } yield a)
 
     (changed_diagnostics, changed_decorations,
       copy(published_diagnostics = diagnostics, published_decorations = decorations))
   }
 
 
   /* prover session */
 
   def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources]
 
   def is_stable: Boolean = pending_edits.isEmpty
   def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits)
 
   def rendering(snapshot: Document.Snapshot): VSCode_Rendering =
     new VSCode_Rendering(snapshot, model)
   def rendering(): VSCode_Rendering = rendering(snapshot())
 
 
   /* syntax */
 
   def syntax(): Outer_Syntax =
     if (is_theory) session.recent_syntax(node_name) else Outer_Syntax.empty
 }
diff --git a/src/Tools/jEdit/src/document_model.scala b/src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala
+++ b/src/Tools/jEdit/src/document_model.scala
@@ -1,688 +1,715 @@
 /*  Title:      Tools/jEdit/src/document_model.scala
     Author:     Fabian Immler, TU Munich
     Author:     Makarius
 
 Document model connected to jEdit buffer or external file: content of theory
 node or auxiliary file (blob).
 */
 
 package isabelle.jedit
 
 
 import isabelle._
 
 import java.io.{File => JFile}
 
 import scala.collection.mutable
 import scala.annotation.tailrec
 
 import org.gjt.sp.jedit.View
 import org.gjt.sp.jedit.Buffer
 import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
 
 
 object Document_Model {
   /* document models */
 
   sealed case class State(
     models: Map[Document.Node.Name, Document_Model] = Map.empty,
     buffer_models: Map[JEditBuffer, Buffer_Model] = Map.empty,
     overlays: Document.Overlays = Document.Overlays.empty
   ) {
     def file_models_iterator: Iterator[(Document.Node.Name, File_Model)] =
       for {
         (node_name, model) <- models.iterator
         if model.isInstanceOf[File_Model]
       } yield (node_name, model.asInstanceOf[File_Model])
 
     def document_blobs: Document.Blobs =
       Document.Blobs(
         (for {
           (node_name, model) <- models.iterator
           blob <- model.get_blob
         } yield (node_name -> blob)).toMap)
 
     def open_buffer(
       session: Session,
       node_name: Document.Node.Name,
       buffer: Buffer
     ) : (Buffer_Model, State) = {
       val old_model =
         models.get(node_name) match {
           case Some(file_model: File_Model) => Some(file_model)
           case Some(buffer_model: Buffer_Model) => Some(buffer_model.exit())
           case _ => None
         }
       val buffer_model = Buffer_Model(session, node_name, buffer).init(old_model)
       (buffer_model,
         copy(models = models + (node_name -> buffer_model),
           buffer_models = buffer_models + (buffer -> buffer_model)))
     }
 
     def close_buffer(buffer: JEditBuffer): State = {
       buffer_models.get(buffer) match {
         case None => this
         case Some(buffer_model) =>
           val file_model = buffer_model.exit()
           copy(models = models + (file_model.node_name -> file_model),
             buffer_models = buffer_models - buffer)
       }
     }
 
     def provide_file(session: Session, node_name: Document.Node.Name, text: String): State =
       if (models.isDefinedAt(node_name)) this
       else {
         val edit = Text.Edit.insert(0, text)
         val model = File_Model.init(session, node_name, text, pending_edits = List(edit))
         copy(models = models + (node_name -> model))
       }
   }
 
   private val state = Synchronized(State())  // owned by GUI thread
 
   def reset(): Unit = state.change(_ => State())
 
   def get_models(): Map[Document.Node.Name, Document_Model] = state.value.models
   def get(name: Document.Node.Name): Option[Document_Model] = get_models().get(name)
   def get(buffer: JEditBuffer): Option[Buffer_Model] = state.value.buffer_models.get(buffer)
 
   def document_blobs(): Document.Blobs = state.value.document_blobs
 
 
   /* bibtex */
 
   def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
     Bibtex.entries_iterator(state.value.models)
 
   def bibtex_completion(history: Completion.History, rendering: Rendering, caret: Text.Offset)
       : Option[Completion.Result] =
     Bibtex.completion(history, rendering, caret, state.value.models)
 
 
   /* overlays */
 
   def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
     state.value.overlays(name)
 
   def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
     state.change(st => st.copy(overlays = st.overlays.insert(command, fn, args)))
 
   def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
     state.change(st => st.copy(overlays = st.overlays.remove(command, fn, args)))
 
 
   /* sync external files */
 
   def sync_files(changed_files: Set[JFile]): Boolean = {
     state.change_result { st =>
       val changed_models =
         (for {
           (node_name, model) <- st.file_models_iterator
           file <- model.file if changed_files(file)
           text <- PIDE.resources.read_file_content(node_name)
           if model.content.text != text
         } yield {
           val content = Document_Model.File_Content(text)
           val edits = Text.Edit.replace(0, model.content.text, text)
           (node_name, model.copy(content = content, pending_edits = model.pending_edits ::: edits))
         }).toList
       if (changed_models.isEmpty) (false, st)
       else (true, st.copy(models = changed_models.foldLeft(st.models)(_ + _)))
     }
   }
 
 
   /* syntax */
 
   def syntax_changed(names: List[Document.Node.Name]): Unit = {
     GUI_Thread.require {}
 
     val models = state.value.models
     for (name <- names.iterator; model <- models.get(name)) {
       model match { case buffer_model: Buffer_Model => buffer_model.syntax_changed() case _ => }
     }
   }
 
 
   /* init and exit */
 
   def init(session: Session, node_name: Document.Node.Name, buffer: Buffer): Buffer_Model = {
     GUI_Thread.require {}
     state.change_result(st =>
       st.buffer_models.get(buffer) match {
         case Some(buffer_model) if buffer_model.node_name == node_name =>
           buffer_model.init_token_marker()
           (buffer_model, st)
         case _ =>
           val res = st.close_buffer(buffer).open_buffer(session, node_name, buffer)
           buffer.propertiesChanged()
           res
       })
   }
 
   def exit(buffer: Buffer): Unit = {
     GUI_Thread.require {}
     state.change(st =>
       if (st.buffer_models.isDefinedAt(buffer)) {
         val res = st.close_buffer(buffer)
         buffer.propertiesChanged()
         res
       }
       else st)
   }
 
   def provide_files(session: Session, files: List[(Document.Node.Name, String)]): Unit = {
     GUI_Thread.require {}
     state.change(st =>
       files.foldLeft(st) {
         case (st1, (node_name, text)) => st1.provide_file(session, node_name, text)
       })
   }
 
 
   /* required nodes */
 
-  def required_nodes(): Set[Document.Node.Name] =
+  def required_nodes(document: Boolean): Set[Document.Node.Name] =
     (for {
       (node_name, model) <- state.value.models.iterator
-      if model.node_required
+      if model.get_required(document)
     } yield node_name).toSet
 
   def node_required(
     name: Document.Node.Name,
+    document: Boolean = false,
     toggle: Boolean = false,
     set: Boolean = false
   ) : Unit = {
     GUI_Thread.require {}
 
     val changed =
       state.change_result(st =>
         st.models.get(name) match {
           case None => (false, st)
           case Some(model) =>
-            val required = if (toggle) !model.node_required else set
+            val a = model.get_required(document)
+            val b = if (toggle) !a else set
             model match {
-              case model1: File_Model if required != model1.node_required =>
-                (true, st.copy(models = st.models + (name -> model1.copy(node_required = required))))
-              case model1: Buffer_Model if required != model1.node_required =>
-                model1.set_node_required(required); (true, st)
+              case m: File_Model if a != b =>
+                (true, st.copy(models = st.models + (name -> m.set_required(document, b))))
+              case m: Buffer_Model if a != b =>
+                m.set_required(document, b); (true, st)
               case _ => (false, st)
             }
         })
     if (changed) {
       PIDE.plugin.options_changed()
       PIDE.editor.flush()
     }
   }
 
-  def view_node_required(view: View, toggle: Boolean = false, set: Boolean = false): Unit =
+  def view_node_required(
+    view: View,
+    document: Boolean = false,
+    toggle: Boolean = false,
+    set: Boolean = false
+  ): Unit =
     Document_Model.get(view.getBuffer).foreach(model =>
-      node_required(model.node_name, toggle = toggle, set = set))
+      node_required(model.node_name, document = document, toggle = toggle, set = set))
 
 
   /* flushed edits */
 
   def flush_edits(hidden: Boolean, purge: Boolean): (Document.Blobs, List[Document.Edit_Text]) = {
     GUI_Thread.require {}
 
     state.change_result { st =>
       val doc_blobs = st.document_blobs
 
       val buffer_edits =
         (for {
           (_, model) <- st.buffer_models.iterator
           edit <- model.flush_edits(doc_blobs, hidden).iterator
         } yield edit).toList
 
       val file_edits =
         (for {
           (node_name, model) <- st.file_models_iterator
           (edits, model1) <- model.flush_edits(doc_blobs, hidden)
         } yield (edits, node_name -> model1)).toList
 
       val model_edits = buffer_edits ::: file_edits.flatMap(_._1)
 
       val purge_edits =
         if (purge) {
           val purged =
             (for ((node_name, model) <- st.file_models_iterator)
              yield (node_name -> model.purge_edits(doc_blobs))).toList
 
           val imports = {
             val open_nodes =
               (for ((_, model) <- st.buffer_models.iterator) yield model.node_name).toList
             val touched_nodes = model_edits.map(_._1)
             val pending_nodes = for ((node_name, None) <- purged) yield node_name
             (open_nodes ::: touched_nodes ::: pending_nodes).map((_, Position.none))
           }
           val retain = PIDE.resources.dependencies(imports).theories.toSet
 
           for ((node_name, Some(edits)) <- purged if !retain(node_name); edit <- edits)
             yield edit
         }
         else Nil
 
       val st1 = st.copy(models = st.models ++ file_edits.map(_._2) -- purge_edits.map(_._1))
       PIDE.plugin.file_watcher.purge(
         (for {
           (_, model) <- st1.file_models_iterator
           file <- model.file
         } yield file.getParentFile).toSet)
 
       ((doc_blobs, model_edits ::: purge_edits), st1)
     }
   }
 
 
   /* file content */
 
   sealed case class File_Content(text: String) {
     lazy val bytes: Bytes = Bytes(Symbol.encode(text))
     lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
     lazy val bibtex_entries: List[Text.Info[String]] =
       try { Bibtex.entries(text) }
       catch { case ERROR(_) => Nil }
   }
 
 
   /* HTTP preview */
 
   def open_preview(view: View, plain_text: Boolean): Unit = {
     Document_Model.get(view.getBuffer) match {
       case Some(model) =>
         val url = Preview_Service.server_url(plain_text, model.node_name)
         PIDE.editor.hyperlink_url(url).follow(view)
       case _ =>
     }
   }
 
   object Preview_Service extends HTTP.Service("preview") {
     service =>
 
     private val plain_text_prefix = "plain_text="
 
     def server_url(plain_text: Boolean, node_name: Document.Node.Name): String =
       PIDE.plugin.http_server.url + "/" + service.name + "?" +
         (if (plain_text) plain_text_prefix else "") + Url.encode(node_name.node)
 
     def apply(request: HTTP.Request): Option[HTTP.Response] =
       for {
         query <- request.decode_query
         name = Library.perhaps_unprefix(plain_text_prefix, query)
         model <- get(PIDE.resources.node_name(name))
       }
       yield {
         val snapshot = model.await_stable_snapshot()
         val context =
           Browser_Info.context(PIDE.resources.sessions_structure,
             elements = Browser_Info.extra_elements)
         val document =
           context.preview_document(snapshot,
             plain_text = query.startsWith(plain_text_prefix),
             fonts_css = HTML.fonts_css_dir(HTTP.url_path(request.server_name)))
         HTTP.Response.html(document.content)
       }
   }
 }
 
 sealed abstract class Document_Model extends Document.Model {
   /* perspective */
 
   def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] = Nil
 
   def node_perspective(
     doc_blobs: Document.Blobs,
     hidden: Boolean
   ): (Boolean, Document.Node.Perspective_Text) = {
     GUI_Thread.require {}
 
     if (JEdit_Options.continuous_checking() && is_theory) {
       val snapshot = this.snapshot()
 
       val reparse = snapshot.node.load_commands_changed(doc_blobs)
       val perspective =
         if (hidden) Text.Perspective.empty
         else {
           val view_ranges = document_view_ranges(snapshot)
           val load_ranges = snapshot.commands_loading_ranges(PIDE.editor.visible_node)
           Text.Perspective(view_ranges ::: load_ranges)
         }
       val overlays = PIDE.editor.node_overlays(node_name)
 
       (reparse, Document.Node.Perspective(node_required, perspective, overlays))
     }
     else (false, Document.Node.no_perspective_text)
   }
 
 
   /* snapshot */
 
   @tailrec final def await_stable_snapshot(): Document.Snapshot = {
     val snapshot = this.snapshot()
     if (snapshot.is_outdated) {
       PIDE.options.seconds("editor_output_delay").sleep()
       await_stable_snapshot()
     }
     else snapshot
   }
 }
 
 object File_Model {
   def empty(session: Session): File_Model =
     File_Model(session, Document.Node.Name.empty, None, Document_Model.File_Content(""),
-      false, Document.Node.no_perspective_text, Nil)
+      false, false, Document.Node.no_perspective_text, Nil)
 
   def init(session: Session,
     node_name: Document.Node.Name,
     text: String,
-    node_required: Boolean = false,
+    theory_required: Boolean = false,
+    document_required: Boolean = false,
     last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
     pending_edits: List[Text.Edit] = Nil
   ): File_Model = {
     val file = JEdit_Lib.check_file(node_name.node)
     file.foreach(PIDE.plugin.file_watcher.register_parent(_))
 
     val content = Document_Model.File_Content(text)
-    val node_required1 = node_required || File_Format.registry.is_theory(node_name)
-    File_Model(session, node_name, file, content, node_required1, last_perspective, pending_edits)
+    val theory_required1 = theory_required || File_Format.registry.is_theory(node_name)
+    File_Model(session, node_name, file, content, theory_required1, document_required,
+      last_perspective, pending_edits)
   }
 }
 
 case class File_Model(
   session: Session,
   node_name: Document.Node.Name,
   file: Option[JFile],
   content: Document_Model.File_Content,
-  node_required: Boolean,
+  theory_required: Boolean,
+  document_required: Boolean,
   last_perspective: Document.Node.Perspective_Text,
   pending_edits: List[Text.Edit]
 ) extends Document_Model {
+  /* required */
+
+  def get_required(document: Boolean): Boolean =
+    if (document) document_required else theory_required
+
+  def set_required(document: Boolean, b: Boolean): File_Model =
+    if (document) copy(document_required = b) else copy(theory_required = b)
+
+
   /* text */
 
   def get_text(range: Text.Range): Option[String] =
     range.try_substring(content.text)
 
 
   /* header */
 
   def node_header: Document.Node.Header =
     PIDE.resources.special_header(node_name) getOrElse
       PIDE.resources.check_thy(node_name, Scan.char_reader(content.text), strict = false)
 
 
   /* content */
 
   def node_position(offset: Text.Offset): Line.Node_Position =
     Line.Node_Position(node_name.node,
       Line.Position.zero.advance(content.text.substring(0, offset)))
 
   def get_blob: Option[Document.Blob] =
     if (is_theory) None
     else Some(Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty))
 
   def bibtex_entries: List[Text.Info[String]] =
     if (File.is_bib(node_name.node)) content.bibtex_entries else Nil
 
 
   /* edits */
 
   def update_text(text: String): Option[File_Model] =
     Text.Edit.replace(0, content.text, text) match {
       case Nil => None
       case edits =>
         val content1 = Document_Model.File_Content(text)
         val pending_edits1 = pending_edits ::: edits
         Some(copy(content = content1, pending_edits = pending_edits1))
     }
 
   def flush_edits(
     doc_blobs: Document.Blobs,
     hidden: Boolean
   ) : Option[(List[Document.Edit_Text], File_Model)] = {
     val (reparse, perspective) = node_perspective(doc_blobs, hidden)
     if (reparse || pending_edits.nonEmpty || last_perspective != perspective) {
       val edits = node_edits(node_header, pending_edits, perspective)
       Some((edits, copy(last_perspective = perspective, pending_edits = Nil)))
     }
     else None
   }
 
   def purge_edits(doc_blobs: Document.Blobs): Option[List[Document.Edit_Text]] =
     if (pending_edits.nonEmpty ||
         !File_Format.registry.is_theory(node_name) &&
           (node_required || !Document.Node.is_no_perspective_text(last_perspective))) None
     else {
       val text_edits = List(Text.Edit.remove(0, content.text))
       Some(node_edits(Document.Node.no_header, text_edits, Document.Node.no_perspective_text))
     }
 
 
   /* snapshot */
 
   def is_stable: Boolean = pending_edits.isEmpty
   def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits)
 }
 
 case class Buffer_Model(session: Session, node_name: Document.Node.Name, buffer: Buffer)
 extends Document_Model {
   /* text */
 
   def get_text(range: Text.Range): Option[String] =
     JEdit_Lib.get_text(buffer, range)
 
 
   /* header */
 
   def node_header(): Document.Node.Header = {
     GUI_Thread.require {}
 
     PIDE.resources.special_header(node_name) getOrElse
       JEdit_Lib.buffer_lock(buffer) {
         PIDE.resources.check_thy(node_name, JEdit_Lib.buffer_reader(buffer), strict = false)
       }
   }
 
 
   /* perspective */
 
   // owned by GUI thread
-  private var _node_required = false
-  def node_required: Boolean = _node_required
-  def set_node_required(b: Boolean): Unit = GUI_Thread.require { _node_required = b }
+  private var _theory_required = false
+  private var _document_required = false
+
+  def get_required(document: Boolean): Boolean =
+    if (document) _document_required else _theory_required
+  def set_required(document: Boolean, b: Boolean): Unit =
+    GUI_Thread.require { if (document) _document_required = b else _theory_required = b }
 
   def document_view_iterator: Iterator[Document_View] =
     for {
       text_area <- JEdit_Lib.jedit_text_areas(buffer)
       doc_view <- Document_View.get(text_area)
     } yield doc_view
 
   override def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] = {
     GUI_Thread.require {}
 
     (for {
       doc_view <- document_view_iterator
       range <- doc_view.perspective(snapshot).ranges.iterator
     } yield range).toList
   }
 
 
   /* blob */
 
   // owned by GUI thread
   private var _blob: Option[(Bytes, String, Symbol.Text_Chunk)] = None
 
   private def reset_blob(): Unit = GUI_Thread.require { _blob = None }
 
   def get_blob: Option[Document.Blob] =
     GUI_Thread.require {
       if (is_theory) None
       else {
         val (bytes, text, chunk) =
           _blob match {
             case Some(x) => x
             case None =>
               val bytes = PIDE.resources.make_file_content(buffer)
               val text = buffer.getText(0, buffer.getLength)
               val chunk = Symbol.Text_Chunk(text)
               val x = (bytes, text, chunk)
               _blob = Some(x)
               x
           }
         val changed = pending_edits.nonEmpty
         Some(Document.Blob(bytes, text, chunk, changed))
       }
     }
 
 
   /* bibtex entries */
 
   // owned by GUI thread
   private var _bibtex_entries: Option[List[Text.Info[String]]] = None
 
   private def reset_bibtex_entries(): Unit = GUI_Thread.require { _bibtex_entries = None }
 
   def bibtex_entries: List[Text.Info[String]] =
     GUI_Thread.require {
       if (File.is_bib(node_name.node)) {
         _bibtex_entries match {
           case Some(entries) => entries
           case None =>
             val text = JEdit_Lib.buffer_text(buffer)
             val entries =
               try { Bibtex.entries(text) }
               catch { case ERROR(msg) => Output.warning(msg); Nil }
             _bibtex_entries = Some(entries)
             entries
         }
       }
       else Nil
     }
 
 
   /* pending edits */
 
   private object pending_edits {
     private val pending = new mutable.ListBuffer[Text.Edit]
     private var last_perspective = Document.Node.no_perspective_text
 
     def nonEmpty: Boolean = synchronized { pending.nonEmpty }
     def get_edits: List[Text.Edit] = synchronized { pending.toList }
     def get_last_perspective: Document.Node.Perspective_Text = synchronized { last_perspective }
     def set_last_perspective(perspective: Document.Node.Perspective_Text): Unit =
       synchronized { last_perspective = perspective }
 
     def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
       synchronized {
         GUI_Thread.require {}
 
         val edits = get_edits
         val (reparse, perspective) = node_perspective(doc_blobs, hidden)
         if (reparse || edits.nonEmpty || last_perspective != perspective) {
           pending.clear()
           last_perspective = perspective
           node_edits(node_header(), edits, perspective)
         }
         else Nil
       }
 
     def edit(edits: List[Text.Edit]): Unit = synchronized {
       GUI_Thread.require {}
 
       reset_blob()
       reset_bibtex_entries()
 
       for (doc_view <- document_view_iterator)
         doc_view.rich_text_area.active_reset()
 
       pending ++= edits
       PIDE.editor.invoke()
     }
   }
 
   def is_stable: Boolean = !pending_edits.nonEmpty
   def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits.get_edits)
 
   def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
     pending_edits.flush_edits(doc_blobs, hidden)
 
 
   /* buffer listener */
 
   private val buffer_listener: BufferListener = new BufferAdapter {
     override def contentInserted(
       buffer: JEditBuffer,
       start_line: Int,
       offset: Int,
       num_lines: Int,
       length: Int
     ): Unit = {
       pending_edits.edit(List(Text.Edit.insert(offset, buffer.getText(offset, length))))
     }
 
     override def preContentRemoved(
       buffer: JEditBuffer,
       start_line: Int,
       offset: Int,
       num_lines: Int,
       removed_length: Int
     ): Unit = {
       pending_edits.edit(List(Text.Edit.remove(offset, buffer.getText(offset, removed_length))))
     }
   }
 
 
   /* syntax */
 
   def syntax_changed(): Unit = {
     JEdit_Lib.buffer_line_manager(buffer).setFirstInvalidLineContext(0)
     for (text_area <- JEdit_Lib.jedit_text_areas(buffer))
       Untyped.method(Class.forName("org.gjt.sp.jedit.textarea.TextArea"), "foldStructureChanged").
         invoke(text_area)
     buffer.invalidateCachedFoldLevels()
   }
 
   def init_token_marker(): Unit = {
     Isabelle.buffer_token_marker(buffer) match {
       case Some(marker) if marker != buffer.getTokenMarker =>
         buffer.setTokenMarker(marker)
         syntax_changed()
       case _ =>
     }
   }
 
 
   /* init */
 
   def init(old_model: Option[File_Model]): Buffer_Model = {
     GUI_Thread.require {}
 
     old_model match {
       case None =>
         pending_edits.edit(List(Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer))))
       case Some(file_model) =>
-        set_node_required(file_model.node_required)
+        set_required(false, file_model.theory_required)
+        set_required(true, file_model.document_required)
         pending_edits.set_last_perspective(file_model.last_perspective)
         pending_edits.edit(
           file_model.pending_edits :::
             Text.Edit.replace(0, file_model.content.text, JEdit_Lib.buffer_text(buffer)))
     }
 
     buffer.addBufferListener(buffer_listener)
     init_token_marker()
 
     this
   }
 
 
   /* exit */
 
   def exit(): File_Model = {
     GUI_Thread.require {}
 
     buffer.removeBufferListener(buffer_listener)
     init_token_marker()
 
-    File_Model.init(session, node_name, JEdit_Lib.buffer_text(buffer), node_required,
-      pending_edits.get_last_perspective, pending_edits.get_edits)
+    File_Model.init(session, node_name, JEdit_Lib.buffer_text(buffer),
+      theory_required = _theory_required,
+      document_required = _document_required,
+      last_perspective = pending_edits.get_last_perspective,
+      pending_edits = pending_edits.get_edits)
   }
 }
diff --git a/src/Tools/jEdit/src/theories_dockable.scala b/src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala
+++ b/src/Tools/jEdit/src/theories_dockable.scala
@@ -1,276 +1,298 @@
 /*  Title:      Tools/jEdit/src/theories_dockable.scala
     Author:     Makarius
 
 Dockable window for theories managed by prover.
 */
 
 package isabelle.jedit
 
 
 import isabelle._
 
 import scala.swing.{Button, TextArea, Label, ListView, Alignment,
   ScrollPane, Component, CheckBox, BorderPanel}
 import scala.swing.event.{MouseClicked, MouseMoved}
 
 import java.awt.{BorderLayout, Graphics2D, Color, Point, Dimension}
 import javax.swing.{JList, BorderFactory, UIManager}
 import javax.swing.border.{BevelBorder, SoftBevelBorder}
 
 import org.gjt.sp.jedit.{View, jEdit}
 
 
 class Theories_Dockable(view: View, position: String) extends Dockable(view, position) {
   /* status */
 
   private val status = new ListView(List.empty[Document.Node.Name]) {
     background = {
       // enforce default value
       val c = UIManager.getDefaults.getColor("Panel.background")
       new Color(c.getRed, c.getGreen, c.getBlue, c.getAlpha)
     }
     listenTo(mouse.clicks)
     listenTo(mouse.moves)
     reactions += {
       case MouseClicked(_, point, _, clicks, _) =>
         val index = peer.locationToIndex(point)
         if (index >= 0) {
-          if (in_checkbox(peer.indexToLocation(index), point)) {
-            if (clicks == 1) Document_Model.node_required(listData(index), toggle = true)
+          val index_location = peer.indexToLocation(index)
+          val a = in_required(index_location, point)
+          val b = in_required(index_location, point, document = true)
+          if (a || b) {
+            if (clicks == 1) {
+              Document_Model.node_required(listData(index), toggle = true, document = b)
+            }
           }
           else if (clicks == 2) PIDE.editor.goto_file(true, view, listData(index).node)
         }
       case MouseMoved(_, point, _) =>
         val index = peer.locationToIndex(point)
         val index_location = peer.indexToLocation(index)
-        if (index >= 0 && in_checkbox(index_location, point)) {
+        if (index >= 0 && in_required(index_location, point)) {
           tooltip = "Mark as required for continuous checking"
-        } else if (index >= 0 && in_label(index_location, point)) {
+        }
+        else if (index >= 0 && in_required(index_location, point, document = true)) {
+          tooltip = "Mark as required for continuous checking, with inclusion in document"
+        }
+        else if (index >= 0 && in_label(index_location, point)) {
           val name = listData(index)
           val st = nodes_status.overall_node_status(name)
           tooltip =
             "theory " + quote(name.theory) +
               (if (st == Document_Status.Overall_Node_Status.ok) "" else " (" + st + ")")
         }
         else tooltip = null
     }
   }
   status.peer.setLayoutOrientation(JList.HORIZONTAL_WRAP)
   status.peer.setVisibleRowCount(0)
   status.selection.intervalMode = ListView.IntervalMode.Single
 
   set_content(new ScrollPane(status))
 
 
   /* controls */
 
   def phase_text(phase: Session.Phase): String = "Prover: " + phase.print
 
   private val session_phase = new Label(phase_text(PIDE.session.phase))
   session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
   session_phase.tooltip = "Status of prover session"
 
   private def handle_phase(phase: Session.Phase): Unit = {
     GUI_Thread.require {}
     session_phase.text = " " + phase_text(phase) + " "
   }
 
   private val purge = new GUI.Button("Purge") {
     tooltip = "Restrict document model to theories required for open editor buffers"
     override def clicked(): Unit = PIDE.editor.purge()
   }
 
   private val continuous_checking = new JEdit_Options.continuous_checking.GUI
   continuous_checking.focusable = false
 
   private val logic = JEdit_Sessions.logic_selector(PIDE.options, autosave = true)
 
   private val controls =
     Wrap_Panel(List(purge, continuous_checking, session_phase, logic))
 
   add(controls.peer, BorderLayout.NORTH)
 
 
   /* component state -- owned by GUI thread */
 
   private var nodes_status = Document_Status.Nodes_Status.empty
-  private var nodes_required: Set[Document.Node.Name] = Document_Model.required_nodes()
+  private var theory_required: Set[Document.Node.Name] = Document_Model.required_nodes(false)
+  private var document_required: Set[Document.Node.Name] = Document_Model.required_nodes(true)
 
   private class Geometry {
     private var location: Point = null
     private var size: Dimension = null
 
-    def in(location0: Point, p: Point): Boolean = {
-      location != null && size != null &&
-        location0.x + location.x <= p.x && p.x < location0.x + size.width &&
-        location0.y + location.y <= p.y && p.y < location0.y + size.height
-    }
+    def in(location0: Point, p: Point): Boolean =
+      location != null && size != null && location0 != null && p != null && {
+        val x = location0.x + location.x
+        val y = location0.y + location.y
+        x <= p.x && p.x < x + size.width &&
+        y <= p.y && p.y < y + size.height
+      }
 
     def update(new_location: Point, new_size: Dimension): Unit = {
       if (new_location != null && new_size != null) {
         location = new_location
         size = new_size
       }
     }
   }
 
-  private def in_checkbox(location0: Point, p: Point): Boolean =
-    Node_Renderer_Component != null && Node_Renderer_Component.checkbox_geometry.in(location0, p)
+  private def in_required(location0: Point, p: Point, document: Boolean = false): Boolean =
+    Node_Renderer_Component != null && {
+      val required =
+        if (document) Node_Renderer_Component.document_required
+        else Node_Renderer_Component.theory_required
+      required.geometry.in(location0, p)
+    }
 
   private def in_label(location0: Point, p: Point): Boolean =
     Node_Renderer_Component != null && Node_Renderer_Component.label_geometry.in(location0, p)
 
+  private class Required extends CheckBox {
+    val geometry = new Geometry
+    opaque = false
+    override def paintComponent(gfx: Graphics2D): Unit = {
+      super.paintComponent(gfx)
+      geometry.update(location, size)
+    }
+  }
 
   private object Node_Renderer_Component extends BorderPanel {
     opaque = true
     border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
 
     var node_name: Document.Node.Name = Document.Node.Name.empty
 
-    val checkbox_geometry = new Geometry
-    val checkbox: CheckBox = new CheckBox {
-      opaque = false
-      override def paintComponent(gfx: Graphics2D): Unit = {
-        super.paintComponent(gfx)
-        checkbox_geometry.update(location, size)
-      }
-    }
+    val theory_required = new Required
+    val document_required = new Required
 
     val label_geometry = new Geometry
     val label: Label = new Label {
       background = view.getTextArea.getPainter.getBackground
       foreground = view.getTextArea.getPainter.getForeground
       opaque = false
       xAlignment = Alignment.Leading
 
       override def paintComponent(gfx: Graphics2D): Unit = {
         def paint_segment(x: Int, w: Int, color: Color): Unit = {
           gfx.setColor(color)
           gfx.fillRect(x, 0, w, size.height)
         }
 
         paint_segment(0, size.width, background)
         nodes_status.get(node_name) match {
           case Some(node_status) =>
             val segments =
               List(
                 (node_status.unprocessed, PIDE.options.color_value("unprocessed1_color")),
                 (node_status.running, PIDE.options.color_value("running_color")),
                 (node_status.warned, PIDE.options.color_value("warning_color")),
                 (node_status.failed, PIDE.options.color_value("error_color"))
               ).filter(_._1 > 0)
 
             segments.foldLeft(size.width - 2) {
               case (last, (n, color)) =>
                 val w = (n * ((size.width - 4) - segments.length) / node_status.total) max 4
                 paint_segment(last - w, w, color)
                 last - w - 1
               }
 
           case None =>
             paint_segment(0, size.width, PIDE.options.color_value("unprocessed1_color"))
         }
         super.paintComponent(gfx)
 
         label_geometry.update(location, size)
       }
     }
 
     def label_border(name: Document.Node.Name): Unit = {
       val st = nodes_status.overall_node_status(name)
       val color =
         st match {
           case Document_Status.Overall_Node_Status.ok =>
             PIDE.options.color_value("ok_color")
           case Document_Status.Overall_Node_Status.failed =>
             PIDE.options.color_value("failed_color")
           case _ => label.foreground
         }
       val thickness1 = if (st == Document_Status.Overall_Node_Status.pending) 1 else 3
       val thickness2 = 4 - thickness1
 
       label.border =
         BorderFactory.createCompoundBorder(
           BorderFactory.createLineBorder(color, thickness1),
           BorderFactory.createEmptyBorder(thickness2, thickness2, thickness2, thickness2))
     }
 
-    layout(checkbox) = BorderPanel.Position.West
+    layout(theory_required) = BorderPanel.Position.West
     layout(label) = BorderPanel.Position.Center
+    layout(document_required) = BorderPanel.Position.East
   }
 
   private class Node_Renderer extends ListView.Renderer[Document.Node.Name] {
     def componentFor(
       list: ListView[_ <: isabelle.Document.Node.Name],
       isSelected: Boolean,
       focused: Boolean,
       name: Document.Node.Name,
       index: Int
     ): Component = {
       val component = Node_Renderer_Component
       component.node_name = name
-      component.checkbox.selected = nodes_required.contains(name)
+      component.theory_required.selected = theory_required.contains(name)
+      component.document_required.selected = document_required.contains(name)
       component.label_border(name)
       component.label.text = name.theory_base_name
       component
     }
   }
   status.renderer = new Node_Renderer
 
   private def handle_update(
     domain: Option[Set[Document.Node.Name]] = None,
     trim: Boolean = false
   ): Unit = {
     GUI_Thread.require {}
 
     val snapshot = PIDE.session.snapshot()
 
     val (nodes_status_changed, nodes_status1) =
       nodes_status.update(
         PIDE.resources, snapshot.state, snapshot.version, domain = domain, trim = trim)
 
     nodes_status = nodes_status1
     if (nodes_status_changed) {
       status.listData =
         (for {
           (name, node_status) <- nodes_status1.present.iterator
           if !node_status.is_suppressed && node_status.total > 0
         } yield name).toList
     }
   }
 
 
   /* main */
 
   private val main =
     Session.Consumer[Any](getClass.getName) {
       case phase: Session.Phase =>
         GUI_Thread.later { handle_phase(phase) }
 
       case _: Session.Global_Options =>
         GUI_Thread.later {
           continuous_checking.load()
           logic.load ()
-          nodes_required = Document_Model.required_nodes()
+          theory_required = Document_Model.required_nodes(false)
+          document_required = Document_Model.required_nodes(true)
           status.repaint()
         }
 
       case changed: Session.Commands_Changed =>
         GUI_Thread.later { handle_update(domain = Some(changed.nodes), trim = changed.assignment) }
     }
 
   override def init(): Unit = {
     PIDE.session.phase_changed += main
     PIDE.session.global_options += main
     PIDE.session.commands_changed += main
 
     handle_phase(PIDE.session.phase)
     handle_update()
   }
 
   override def exit(): Unit = {
     PIDE.session.phase_changed -= main
     PIDE.session.global_options -= main
     PIDE.session.commands_changed -= main
   }
 }