src/Tools/jEdit/src/plugin.scala
changeset 66019 69b5ef78fb07
parent 65571 923e32ad0976
child 66082 2d12a730a380
--- a/src/Tools/jEdit/src/plugin.scala	Mon Jun 05 23:13:08 2017 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Jun 05 23:55:58 2017 +0200
@@ -12,6 +12,7 @@
 import javax.swing.JOptionPane
 
 import java.io.{File => JFile}
+import java.util.UUID
 
 import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, Debug, PerspectiveManager}
 import org.gjt.sp.jedit.textarea.JEditTextArea
@@ -393,6 +394,13 @@
   }
 
 
+  /* HTTP server */
+
+  val http_root: String = "/" + UUID.randomUUID().toString
+
+  val http_server: HTTP.Server = HTTP.server(Document_Model.http_handlers(http_root))
+
+
   /* start and stop */
 
   override def start()
@@ -418,6 +426,8 @@
       init_mode_provider()
       JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)
 
+      http_server.start
+
       startup_failure = None
     }
     catch {
@@ -430,6 +440,8 @@
 
   override def stop()
   {
+    http_server.stop
+
     exit_mode_provider()
     JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.exit _)