support "purge" operation on document model;

--- a/NEWS	Tue Jan 10 16:09:04 2017 +0100
+++ b/NEWS	Tue Jan 10 16:53:05 2017 +0100
@@ -20,6 +20,10 @@
 The system option "jedit_auto_load" has been discontinued: it is
 effectively always enabled.
 
+* The Theories dockable provides a "Purge" button, in order to restrict
+the document model to theories that are required for open editor
+buffers.
+
 
 *** HOL ***
 

--- a/src/Pure/General/file_watcher.scala	Tue Jan 10 16:09:04 2017 +0100
+++ b/src/Pure/General/file_watcher.scala	Tue Jan 10 16:53:05 2017 +0100
@@ -20,6 +20,7 @@
   def register(dir: JFile) { }
   def register_parent(file: JFile) { }
   def deregister(dir: JFile) { }
+  def purge(retain: Set[JFile]) { }
   def shutdown() { }
 }
 
@@ -75,6 +76,11 @@
             st.copy(dirs = st.dirs - dir)
         })
 
+    override def purge(retain: Set[JFile]): Unit =
+      state.change(st =>
+        st.copy(dirs = st.dirs --
+          (for ((dir, key) <- st.dirs.iterator if !retain(dir)) yield { key.cancel; dir })))
+
 
     /* changed directory entries */
 

--- a/src/Pure/PIDE/document.scala	Tue Jan 10 16:09:04 2017 +0100
+++ b/src/Pure/PIDE/document.scala	Tue Jan 10 16:53:05 2017 +0100
@@ -178,6 +178,11 @@
     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 &&
@@ -479,9 +484,10 @@
     def node_required: Boolean
     def get_blob: Option[Document.Blob]
 
-    def node_header: Node.Header
     def node_edits(
-      text_edits: List[Text.Edit], perspective: Node.Perspective_Text): List[Edit_Text] =
+      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 {

--- a/src/Pure/PIDE/editor.scala	Tue Jan 10 16:09:04 2017 +0100
+++ b/src/Pure/PIDE/editor.scala	Tue Jan 10 16:53:05 2017 +0100
@@ -10,7 +10,7 @@
 abstract class Editor[Context]
 {
   def session: Session
-  def flush(hidden: Boolean = false): Unit
+  def flush(hidden: Boolean = false, purge: Boolean = false): Unit
   def invoke(): Unit
   def invoke_generated(): Unit
   def current_context: Context

--- a/src/Tools/VSCode/src/document_model.scala	Tue Jan 10 16:09:04 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Tue Jan 10 16:53:05 2017 +0100
@@ -103,7 +103,7 @@
   {
     val (reparse, perspective) = node_perspective(doc_blobs)
     if (reparse || pending_edits.nonEmpty || last_perspective != perspective) {
-      val edits = node_edits(pending_edits, perspective)
+      val edits = node_edits(node_header, pending_edits, perspective)
       Some((edits, copy(pending_edits = Nil, last_perspective = perspective)))
     }
     else None

--- a/src/Tools/jEdit/src/document_model.scala	Tue Jan 10 16:09:04 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Tue Jan 10 16:53:05 2017 +0100
@@ -202,7 +202,7 @@
 
   /* flushed edits */
 
-  def flush_edits(hidden: Boolean): (Document.Blobs, List[Document.Edit_Text]) =
+  def flush_edits(hidden: Boolean, purge: Boolean): (Document.Blobs, List[Document.Edit_Text]) =
   {
     GUI_Thread.require {}
 
@@ -224,14 +224,39 @@
         val file_edits =
           (for {
             model <- st.file_models_iterator
-            change <- model.flush_edits(doc_blobs, hidden)
-          } yield change).toList
+            (edits, model1) <- model.flush_edits(doc_blobs, hidden)
+          } yield (edits, model.node_name -> model1)).toList
+
+        val model_edits = buffer_edits ::: file_edits.flatMap(_._1)
+
+        val purge_edits =
+          if (purge) {
+            val purged =
+              (for (model <- st.file_models_iterator)
+               yield (model.node_name -> model.purge_edits(doc_blobs))).toList
 
-        val edits = buffer_edits ::: file_edits.flatMap(_._1)
+            val imports =
+            {
+              val open_nodes = st.buffer_models_iterator.map(_.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.thy_info.dependencies("", imports).deps.map(_.name).toSet
 
-        ((doc_blobs, edits),
-          st.copy(
-            models = (st.models /: file_edits) { case (ms, (_, m)) => ms + (m.node_name -> m) }))
+            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.file_watcher.purge(
+          (for {
+            model <- st1.file_models_iterator
+            file <- model.file
+          } yield file.getParentFile).toSet)
+
+        ((doc_blobs, model_edits ::: purge_edits), st1)
       })
   }
 
@@ -346,12 +371,20 @@
   {
     val (reparse, perspective) = node_perspective(doc_blobs, hidden)
     if (reparse || pending_edits.nonEmpty || last_perspective != perspective) {
-      val edits = node_edits(pending_edits, 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 (node_required || !Document.Node.is_no_perspective_text(last_perspective) ||
+        pending_edits.nonEmpty) 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 */
 
@@ -465,7 +498,7 @@
         if (reparse || edits.nonEmpty || last_perspective != perspective) {
           pending.clear
           last_perspective = perspective
-          node_edits(edits, perspective)
+          node_edits(node_header, edits, perspective)
         }
         else Nil
       }

--- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Jan 10 16:09:04 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Jan 10 16:53:05 2017 +0100
@@ -22,12 +22,14 @@
 
   override def session: Session = PIDE.session
 
-  override def flush(hidden: Boolean = false): Unit =
+  override def flush(hidden: Boolean = false, purge: Boolean = false): Unit =
     GUI_Thread.require {
-      val (doc_blobs, edits) = Document_Model.flush_edits(hidden)
+      val (doc_blobs, edits) = Document_Model.flush_edits(hidden, purge)
       session.update(doc_blobs, edits)
     }
 
+  def purge() { flush(purge = true) }
+
   private val delay1_flush =
     GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
 

--- a/src/Tools/jEdit/src/theories_dockable.scala	Tue Jan 10 16:09:04 2017 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Tue Jan 10 16:53:05 2017 +0100
@@ -11,7 +11,7 @@
 
 import scala.swing.{Button, TextArea, Label, ListView, Alignment,
   ScrollPane, Component, CheckBox, BorderPanel}
-import scala.swing.event.{MouseClicked, MouseMoved}
+import scala.swing.event.{ButtonClicked, MouseClicked, MouseMoved}
 
 import java.awt.{BorderLayout, Graphics2D, Color, Point, Dimension}
 import javax.swing.{JList, BorderFactory, UIManager}
@@ -72,13 +72,18 @@
     session_phase.text = " " + phase_text(phase) + " "
   }
 
+  private val purge = new Button("Purge") {
+    tooltip = "Restrict document model to theories required for open editor buffers"
+    reactions += { case ButtonClicked(_) => PIDE.editor.purge() }
+  }
+
   private val continuous_checking = new Isabelle.Continuous_Checking
   continuous_checking.focusable = false
 
   private val logic = JEdit_Sessions.logic_selector(true)
 
   private val controls =
-    new Wrap_Panel(Wrap_Panel.Alignment.Right)(continuous_checking, session_phase, logic)
+    new Wrap_Panel(Wrap_Panel.Alignment.Right)(purge, continuous_checking, session_phase, logic)
   add(controls.peer, BorderLayout.NORTH)