src/Tools/jEdit/src/plugin.scala
changeset 64858 e31cf6eaecb8
parent 64856 5e9bf964510a
child 64882 c3b42ac0cf81
     1.1 --- a/src/Tools/jEdit/src/plugin.scala	Mon Jan 09 21:51:39 2017 +0100
     1.2 +++ b/src/Tools/jEdit/src/plugin.scala	Mon Jan 09 22:54:48 2017 +0100
     1.3 @@ -11,6 +11,8 @@
     1.4  
     1.5  import javax.swing.JOptionPane
     1.6  
     1.7 +import java.io.{File => JFile}
     1.8 +
     1.9  import scala.swing.{ListView, ScrollPane}
    1.10  
    1.11  import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, Debug, PerspectiveManager}
    1.12 @@ -43,6 +45,9 @@
    1.13    def resources(): JEdit_Resources =
    1.14      session.resources.asInstanceOf[JEdit_Resources]
    1.15  
    1.16 +  def file_watcher(): File_Watcher =
    1.17 +    if (plugin == null) File_Watcher.none else plugin.file_watcher
    1.18 +
    1.19    lazy val editor = new JEdit_Editor
    1.20  
    1.21  
    1.22 @@ -233,6 +238,12 @@
    1.23    private lazy val delay_load =
    1.24      GUI_Thread.delay_last(PIDE.options.seconds("editor_load_delay")) { delay_load_action() }
    1.25  
    1.26 +  private def file_watcher_action(changed: Set[JFile]): Unit =
    1.27 +    if (Document_Model.sync_files(changed)) PIDE.editor.invoke_generated()
    1.28 +
    1.29 +  lazy val file_watcher: File_Watcher =
    1.30 +    File_Watcher(file_watcher_action _, PIDE.options.seconds("editor_load_delay"))
    1.31 +
    1.32  
    1.33    /* session phase */
    1.34  
    1.35 @@ -419,5 +430,6 @@
    1.36      PIDE.session.phase_changed -= session_phase
    1.37      PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
    1.38      PIDE.session.stop()
    1.39 +    PIDE.file_watcher.shutdown()
    1.40    }
    1.41  }