update File_Model based on file-system events;
authorwenzelm
Mon Jan 09 22:54:48 2017 +0100 (2017-01-09)
changeset 64858e31cf6eaecb8
parent 64857 316d703f741d
child 64859 e600cfdc9e97
update File_Model based on file-system events;
src/Pure/General/file_watcher.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/jedit_resources.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/General/file_watcher.scala	Mon Jan 09 21:51:39 2017 +0100
     1.2 +++ b/src/Pure/General/file_watcher.scala	Mon Jan 09 22:54:48 2017 +0100
     1.3 @@ -25,9 +25,10 @@
     1.4  
     1.5  object File_Watcher
     1.6  {
     1.7 +  val none: File_Watcher = new File_Watcher
     1.8 +
     1.9    def apply(handle: Set[JFile] => Unit, delay: => Time = Time.seconds(0.5)): File_Watcher =
    1.10 -    if (Platform.is_windows) new File_Watcher
    1.11 -    else new Impl(handle, delay)
    1.12 +    if (Platform.is_windows) none else new Impl(handle, delay)
    1.13  
    1.14  
    1.15    /* proper implementation */
     2.1 --- a/src/Tools/jEdit/src/document_model.scala	Mon Jan 09 21:51:39 2017 +0100
     2.2 +++ b/src/Tools/jEdit/src/document_model.scala	Mon Jan 09 22:54:48 2017 +0100
     2.3 @@ -11,6 +11,8 @@
     2.4  
     2.5  import isabelle._
     2.6  
     2.7 +import java.io.{File => JFile}
     2.8 +
     2.9  import scala.collection.mutable
    2.10  
    2.11  import org.gjt.sp.jedit.{jEdit, View}
    2.12 @@ -70,6 +72,7 @@
    2.13        else {
    2.14          val edit = Text.Edit.insert(0, text)
    2.15          val model = File_Model(session, node_name, File_Content(text), pending_edits = List(edit))
    2.16 +        model.watch
    2.17          copy(models = models + (node_name -> model))
    2.18        }
    2.19    }
    2.20 @@ -87,6 +90,31 @@
    2.21      } yield Text.Info(range, (entry, model))
    2.22  
    2.23  
    2.24 +  /* sync external files */
    2.25 +
    2.26 +  def sync_files(changed_files: Set[JFile]): Boolean =
    2.27 +  {
    2.28 +    state.change_result(st =>
    2.29 +      {
    2.30 +        val changed_models =
    2.31 +          (for {
    2.32 +            model <- st.file_models_iterator
    2.33 +            node_name = model.node_name
    2.34 +            file <- PIDE.resources.node_name_file(node_name)
    2.35 +            if changed_files(file)
    2.36 +            text <- PIDE.resources.read_file_content(node_name)
    2.37 +            if model.content.text != text
    2.38 +          } yield {
    2.39 +            val content = Document_Model.File_Content(text)
    2.40 +            val edits = Text.Edit.replace(0, model.content.text, text)
    2.41 +            (node_name, model.copy(content = content, pending_edits = model.pending_edits ::: edits))
    2.42 +          }).toList
    2.43 +        if (changed_models.isEmpty) (false, st)
    2.44 +        else (true, st.copy(models = (st.models /: changed_models)(_ + _)))
    2.45 +      })
    2.46 +  }
    2.47 +
    2.48 +
    2.49    /* syntax */
    2.50  
    2.51    def syntax_changed(names: List[Document.Node.Name])
    2.52 @@ -313,6 +341,13 @@
    2.53  
    2.54    def is_stable: Boolean = pending_edits.isEmpty
    2.55    def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits)
    2.56 +
    2.57 +
    2.58 +  /* watch file-system content */
    2.59 +
    2.60 +  def watch: Unit =
    2.61 +    for (file <- PIDE.resources.node_name_file(node_name))
    2.62 +      PIDE.file_watcher.register_parent(file)
    2.63  }
    2.64  
    2.65  case class Buffer_Model(session: Session, node_name: Document.Node.Name, buffer: Buffer)
    2.66 @@ -522,7 +557,10 @@
    2.67      init_token_marker()
    2.68  
    2.69      val content = Document_Model.File_Content(JEdit_Lib.buffer_text(buffer))
    2.70 -    File_Model(session, node_name, content, node_required,
    2.71 -      pending_edits.get_last_perspective, pending_edits.get_edits)
    2.72 +    val model =
    2.73 +      File_Model(session, node_name, content, node_required,
    2.74 +        pending_edits.get_last_perspective, pending_edits.get_edits)
    2.75 +    model.watch
    2.76 +    model
    2.77    }
    2.78  }
     3.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Jan 09 21:51:39 2017 +0100
     3.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Mon Jan 09 22:54:48 2017 +0100
     3.3 @@ -47,6 +47,12 @@
     3.4      Document.Node.Name(node, master_dir, theory)
     3.5    }
     3.6  
     3.7 +  def node_name_file(name: Document.Node.Name): Option[JFile] =
     3.8 +  {
     3.9 +    val vfs = VFSManager.getVFSForPath(name.node)
    3.10 +    if (vfs.isInstanceOf[FileVFS]) Some(new JFile(name.node)) else None
    3.11 +  }
    3.12 +
    3.13    def theory_node_name(buffer: Buffer): Option[Document.Node.Name] =
    3.14    {
    3.15      val name = node_name(buffer)
     4.1 --- a/src/Tools/jEdit/src/plugin.scala	Mon Jan 09 21:51:39 2017 +0100
     4.2 +++ b/src/Tools/jEdit/src/plugin.scala	Mon Jan 09 22:54:48 2017 +0100
     4.3 @@ -11,6 +11,8 @@
     4.4  
     4.5  import javax.swing.JOptionPane
     4.6  
     4.7 +import java.io.{File => JFile}
     4.8 +
     4.9  import scala.swing.{ListView, ScrollPane}
    4.10  
    4.11  import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, Debug, PerspectiveManager}
    4.12 @@ -43,6 +45,9 @@
    4.13    def resources(): JEdit_Resources =
    4.14      session.resources.asInstanceOf[JEdit_Resources]
    4.15  
    4.16 +  def file_watcher(): File_Watcher =
    4.17 +    if (plugin == null) File_Watcher.none else plugin.file_watcher
    4.18 +
    4.19    lazy val editor = new JEdit_Editor
    4.20  
    4.21  
    4.22 @@ -233,6 +238,12 @@
    4.23    private lazy val delay_load =
    4.24      GUI_Thread.delay_last(PIDE.options.seconds("editor_load_delay")) { delay_load_action() }
    4.25  
    4.26 +  private def file_watcher_action(changed: Set[JFile]): Unit =
    4.27 +    if (Document_Model.sync_files(changed)) PIDE.editor.invoke_generated()
    4.28 +
    4.29 +  lazy val file_watcher: File_Watcher =
    4.30 +    File_Watcher(file_watcher_action _, PIDE.options.seconds("editor_load_delay"))
    4.31 +
    4.32  
    4.33    /* session phase */
    4.34  
    4.35 @@ -419,5 +430,6 @@
    4.36      PIDE.session.phase_changed -= session_phase
    4.37      PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
    4.38      PIDE.session.stop()
    4.39 +    PIDE.file_watcher.shutdown()
    4.40    }
    4.41  }