src/Tools/jEdit/src/plugin.scala
changeset 66019 69b5ef78fb07
parent 65571 923e32ad0976
child 66082 2d12a730a380
     1.1 --- a/src/Tools/jEdit/src/plugin.scala	Mon Jun 05 23:13:08 2017 +0200
     1.2 +++ b/src/Tools/jEdit/src/plugin.scala	Mon Jun 05 23:55:58 2017 +0200
     1.3 @@ -12,6 +12,7 @@
     1.4  import javax.swing.JOptionPane
     1.5  
     1.6  import java.io.{File => JFile}
     1.7 +import java.util.UUID
     1.8  
     1.9  import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, Debug, PerspectiveManager}
    1.10  import org.gjt.sp.jedit.textarea.JEditTextArea
    1.11 @@ -393,6 +394,13 @@
    1.12    }
    1.13  
    1.14  
    1.15 +  /* HTTP server */
    1.16 +
    1.17 +  val http_root: String = "/" + UUID.randomUUID().toString
    1.18 +
    1.19 +  val http_server: HTTP.Server = HTTP.server(Document_Model.http_handlers(http_root))
    1.20 +
    1.21 +
    1.22    /* start and stop */
    1.23  
    1.24    override def start()
    1.25 @@ -418,6 +426,8 @@
    1.26        init_mode_provider()
    1.27        JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)
    1.28  
    1.29 +      http_server.start
    1.30 +
    1.31        startup_failure = None
    1.32      }
    1.33      catch {
    1.34 @@ -430,6 +440,8 @@
    1.35  
    1.36    override def stop()
    1.37    {
    1.38 +    http_server.stop
    1.39 +
    1.40      exit_mode_provider()
    1.41      JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.exit _)
    1.42