# HG changeset patch # User wenzelm # Date 1484065455 -3600 # Node ID a73ac955822086a274c10d9d35d2c135630d531e # Parent 2baa926a958d7952ca5a38cf6db30e390146a1f1# Parent 6212d3c396b01a7058b5d3acbe37529ab44b9b5f merged diff -r 2baa926a958d -r a73ac9558220 NEWS --- a/NEWS Tue Jan 10 14:29:40 2017 +0100 +++ b/NEWS Tue Jan 10 17:24:15 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 2baa926a958d -r a73ac9558220 src/Pure/General/file_watcher.scala --- a/src/Pure/General/file_watcher.scala Tue Jan 10 14:29:40 2017 +0100 +++ b/src/Pure/General/file_watcher.scala Tue Jan 10 17:24:15 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 2baa926a958d -r a73ac9558220 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Tue Jan 10 14:29:40 2017 +0100 +++ b/src/Pure/PIDE/document.scala Tue Jan 10 17:24:15 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 2baa926a958d -r a73ac9558220 src/Pure/PIDE/editor.scala --- a/src/Pure/PIDE/editor.scala Tue Jan 10 14:29:40 2017 +0100 +++ b/src/Pure/PIDE/editor.scala Tue Jan 10 17:24:15 2017 +0100 @@ -10,7 +10,7 @@ abstract class Editor[Context] { def session: Session - def flush(hidden: Boolean = true): Unit + def flush(hidden: Boolean = false, purge: Boolean = false): Unit def invoke(): Unit def invoke_generated(): Unit def current_context: Context diff -r 2baa926a958d -r a73ac9558220 src/Tools/VSCode/src/document_model.scala --- a/src/Tools/VSCode/src/document_model.scala Tue Jan 10 14:29:40 2017 +0100 +++ b/src/Tools/VSCode/src/document_model.scala Tue Jan 10 17:24:15 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 2baa926a958d -r a73ac9558220 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Tue Jan 10 14:29:40 2017 +0100 +++ b/src/Tools/jEdit/src/document_model.scala Tue Jan 10 17:24:15 2017 +0100 @@ -28,18 +28,11 @@ models: Map[Document.Node.Name, Document_Model] = Map.empty, buffer_models: Map[JEditBuffer, Buffer_Model] = Map.empty) { - def models_iterator: Iterator[Document_Model] = - for ((_, model) <- models.iterator) yield model - - def file_models_iterator: Iterator[File_Model] = + def file_models_iterator: Iterator[(Document.Node.Name, File_Model)] = for { - (_, model) <- models.iterator + (node_name, model) <- models.iterator if model.isInstanceOf[File_Model] - } yield model.asInstanceOf[File_Model] - - def buffer_models_iterator: Iterator[Buffer_Model] = - for ((_, model) <- buffer_models.iterator) yield model - + } yield (node_name, model.asInstanceOf[File_Model]) def open_buffer(session: Session, node_name: Document.Node.Name, buffer: Buffer) : (Buffer_Model, State) = @@ -71,8 +64,7 @@ if (models.isDefinedAt(node_name)) this else { val edit = Text.Edit.insert(0, text) - val model = File_Model(session, node_name, File_Content(text), pending_edits = List(edit)) - model.watch + val model = File_Model.init(session, node_name, text, pending_edits = List(edit)) copy(models = models + (node_name -> model)) } } @@ -85,7 +77,7 @@ def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] = for { - model <- state.value.models_iterator + (_, model) <- state.value.models.iterator Text.Info(range, entry) <- model.bibtex_entries.iterator } yield Text.Info(range, (entry, model)) @@ -98,10 +90,8 @@ { val changed_models = (for { - model <- st.file_models_iterator - node_name = model.node_name - file <- PIDE.resources.node_name_file(node_name) - if changed_files(file) + (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 { @@ -169,9 +159,9 @@ def required_nodes(): Set[Document.Node.Name] = (for { - model <- state.value.models_iterator + (node_name, model) <- state.value.models.iterator if model.node_required - } yield model.node_name).toSet + } yield node_name).toSet def node_required(name: Document.Node.Name, toggle: Boolean = false, set: Boolean = false) { @@ -204,7 +194,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 {} @@ -213,27 +203,53 @@ val doc_blobs = Document.Blobs( (for { - model <- st.models_iterator + (node_name, model) <- st.models.iterator blob <- model.get_blob - } yield (model.node_name -> blob)).toMap) + } yield (node_name -> blob)).toMap) val buffer_edits = (for { - model <- st.buffer_models_iterator + (_, model) <- st.buffer_models.iterator edit <- model.flush_edits(doc_blobs, hidden).iterator } yield edit).toList val file_edits = (for { - model <- st.file_models_iterator - change <- model.flush_edits(doc_blobs, hidden) - } yield change).toList + (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 edits = buffer_edits ::: file_edits.flatMap(_._1) + 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.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) }) } @@ -285,13 +301,31 @@ } } +object File_Model +{ + def init(session: Session, + node_name: Document.Node.Name, + text: String, + node_required: Boolean = false, + last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text, + pending_edits: List[Text.Edit] = Nil): File_Model = + { + val file = PIDE.resources.node_name_file(node_name) + file.foreach(PIDE.file_watcher.register_parent(_)) + + val content = Document_Model.File_Content(text) + File_Model(session, node_name, file, content, node_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 = false, - last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text, - pending_edits: List[Text.Edit] = Nil) extends Document_Model + node_required: Boolean, + last_perspective: Document.Node.Perspective_Text, + pending_edits: List[Text.Edit]) extends Document_Model { /* header */ @@ -330,24 +364,25 @@ { 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 */ def is_stable: Boolean = pending_edits.isEmpty def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits) - - - /* watch file-system content */ - - def watch: Unit = - for (file <- PIDE.resources.node_name_file(node_name)) - PIDE.file_watcher.register_parent(file) } case class Buffer_Model(session: Session, node_name: Document.Node.Name, buffer: Buffer) @@ -456,7 +491,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 } @@ -556,11 +591,7 @@ buffer.removeBufferListener(buffer_listener) init_token_marker() - val content = Document_Model.File_Content(JEdit_Lib.buffer_text(buffer)) - val model = - File_Model(session, node_name, content, node_required, - pending_edits.get_last_perspective, pending_edits.get_edits) - model.watch - model + File_Model.init(session, node_name, JEdit_Lib.buffer_text(buffer), node_required, + pending_edits.get_last_perspective, pending_edits.get_edits) } } diff -r 2baa926a958d -r a73ac9558220 src/Tools/jEdit/src/info_dockable.scala --- a/src/Tools/jEdit/src/info_dockable.scala Tue Jan 10 14:29:40 2017 +0100 +++ b/src/Tools/jEdit/src/info_dockable.scala Tue Jan 10 17:24:15 2017 +0100 @@ -9,9 +9,6 @@ import isabelle._ -import scala.swing.Button -import scala.swing.event.ButtonClicked - import java.awt.BorderLayout import java.awt.event.{ComponentEvent, ComponentAdapter, WindowFocusListener, WindowEvent} diff -r 2baa926a958d -r a73ac9558220 src/Tools/jEdit/src/jedit_editor.scala --- a/src/Tools/jEdit/src/jedit_editor.scala Tue Jan 10 14:29:40 2017 +0100 +++ b/src/Tools/jEdit/src/jedit_editor.scala Tue Jan 10 17:24:15 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 2baa926a958d -r a73ac9558220 src/Tools/jEdit/src/theories_dockable.scala --- a/src/Tools/jEdit/src/theories_dockable.scala Tue Jan 10 14:29:40 2017 +0100 +++ b/src/Tools/jEdit/src/theories_dockable.scala Tue Jan 10 17:24:15 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)