# HG changeset patch # User wenzelm # Date 1484063585 -3600 # Node ID e7220f4de11feade81434e6f6ca77c46772756d3 # Parent 372c833c76606ecfd431bd92bfead28f8ec34d8e support "purge" operation on document model; diff -r 372c833c7660 -r e7220f4de11f NEWS --- 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 *** diff -r 372c833c7660 -r e7220f4de11f src/Pure/General/file_watcher.scala --- 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 */ diff -r 372c833c7660 -r e7220f4de11f src/Pure/PIDE/document.scala --- 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 { diff -r 372c833c7660 -r e7220f4de11f src/Pure/PIDE/editor.scala --- 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 diff -r 372c833c7660 -r e7220f4de11f src/Tools/VSCode/src/document_model.scala --- 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 diff -r 372c833c7660 -r e7220f4de11f src/Tools/jEdit/src/document_model.scala --- 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 } diff -r 372c833c7660 -r e7220f4de11f src/Tools/jEdit/src/jedit_editor.scala --- 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() } diff -r 372c833c7660 -r e7220f4de11f src/Tools/jEdit/src/theories_dockable.scala --- 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)