src/Tools/jEdit/src/plugin.scala
author wenzelm
Mon Jun 05 23:55:58 2017 +0200 (2017-06-05)
changeset 66019 69b5ef78fb07
parent 65571 923e32ad0976
child 66082 2d12a730a380
permissions -rw-r--r--
HTML preview via builtin HTTP server;
     1 /*  Title:      Tools/jEdit/src/plugin.scala
     2     Author:     Makarius
     3 
     4 Main plumbing for PIDE infrastructure as jEdit plugin.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import javax.swing.JOptionPane
    13 
    14 import java.io.{File => JFile}
    15 import java.util.UUID
    16 
    17 import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, Debug, PerspectiveManager}
    18 import org.gjt.sp.jedit.textarea.JEditTextArea
    19 import org.gjt.sp.jedit.syntax.ModeProvider
    20 import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
    21 import org.gjt.sp.util.SyntaxUtilities
    22 import org.gjt.sp.util.Log
    23 
    24 
    25 object PIDE
    26 {
    27   /* semantic document content */
    28 
    29   def snapshot(view: View): Document.Snapshot = GUI_Thread.now
    30   {
    31     Document_Model.get(view.getBuffer) match {
    32       case Some(model) => model.snapshot
    33       case None => error("No document model for current buffer")
    34     }
    35   }
    36 
    37   def rendering(view: View): JEdit_Rendering = GUI_Thread.now
    38   {
    39     val text_area = view.getTextArea
    40     Document_View.get(text_area) match {
    41       case Some(doc_view) => doc_view.get_rendering()
    42       case None => error("No document view for current text area")
    43     }
    44   }
    45 
    46 
    47   /* plugin instance */
    48 
    49   @volatile var _plugin: Plugin = null
    50 
    51   def plugin: Plugin =
    52     if (_plugin == null) error("Uninitialized Isabelle/jEdit plugin")
    53     else _plugin
    54 
    55   def options: JEdit_Options = plugin.options
    56   def resources: JEdit_Resources = plugin.resources
    57   def session: Session = plugin.session
    58 }
    59 
    60 class Plugin extends EBPlugin
    61 {
    62   /* options */
    63 
    64   private var _options: JEdit_Options = null
    65   private def init_options(): Unit = _options = new JEdit_Options(Options.init())
    66   def options: JEdit_Options = _options
    67 
    68 
    69   /* resources */
    70 
    71   private var _resources: JEdit_Resources = null
    72   private def init_resources(): Unit =
    73     _resources = new JEdit_Resources(JEdit_Sessions.session_base(options.value))
    74   def resources: JEdit_Resources = _resources
    75 
    76 
    77   /* session */
    78 
    79   private var _session: Session = null
    80   private def init_session(): Unit = _session = new Session(options.value, resources)
    81   def session: Session = _session
    82 
    83 
    84   /* misc support */
    85 
    86   val completion_history = new Completion.History_Variable
    87   val spell_checker = new Spell_Checker_Variable
    88 
    89 
    90   /* global changes */
    91 
    92   def options_changed()
    93   {
    94     session.global_options.post(Session.Global_Options(options.value))
    95     delay_load.invoke()
    96   }
    97 
    98   def deps_changed()
    99   {
   100     delay_load.invoke()
   101   }
   102 
   103 
   104   /* theory files */
   105 
   106   lazy val delay_init =
   107     GUI_Thread.delay_last(options.seconds("editor_load_delay"))
   108     {
   109       init_models()
   110     }
   111 
   112   private val delay_load_active = Synchronized(false)
   113   private def delay_load_activated(): Boolean =
   114     delay_load_active.guarded_access(a => Some((!a, true)))
   115   private def delay_load_action()
   116   {
   117     if (Isabelle.continuous_checking && delay_load_activated() &&
   118         PerspectiveManager.isPerspectiveEnabled)
   119     {
   120       if (JEdit_Lib.jedit_buffers().exists(_.isLoading)) delay_load.invoke()
   121       else {
   122         val required_files =
   123         {
   124           val models = Document_Model.get_models()
   125 
   126           val thys =
   127             (for ((node_name, model) <- models.iterator if model.is_theory)
   128               yield (node_name, Position.none)).toList
   129           val thy_files = resources.thy_info.dependencies(thys).deps.map(_.name)
   130 
   131           val aux_files =
   132             if (options.bool("jedit_auto_resolve")) {
   133               val stable_tip_version =
   134                 if (models.forall(p => p._2.is_stable))
   135                   session.current_state().stable_tip_version
   136                 else None
   137               stable_tip_version match {
   138                 case Some(version) => resources.undefined_blobs(version.nodes)
   139                 case None => delay_load.invoke(); Nil
   140               }
   141             }
   142             else Nil
   143 
   144           (thy_files ::: aux_files).filterNot(models.isDefinedAt(_))
   145         }
   146         if (required_files.nonEmpty) {
   147           try {
   148             Standard_Thread.fork("resolve_dependencies") {
   149               val loaded_files =
   150                 for {
   151                   name <- required_files
   152                   text <- resources.read_file_content(name)
   153                 } yield (name, text)
   154 
   155               GUI_Thread.later {
   156                 try {
   157                   Document_Model.provide_files(session, loaded_files)
   158                   delay_init.invoke()
   159                 }
   160                 finally { delay_load_active.change(_ => false) }
   161               }
   162             }
   163           }
   164           catch { case _: Throwable => delay_load_active.change(_ => false) }
   165         }
   166         else delay_load_active.change(_ => false)
   167       }
   168     }
   169   }
   170 
   171   private lazy val delay_load =
   172     GUI_Thread.delay_last(options.seconds("editor_load_delay")) { delay_load_action() }
   173 
   174   private def file_watcher_action(changed: Set[JFile]): Unit =
   175     if (Document_Model.sync_files(changed)) JEdit_Editor.invoke_generated()
   176 
   177   lazy val file_watcher: File_Watcher =
   178     File_Watcher(file_watcher_action _, options.seconds("editor_load_delay"))
   179 
   180 
   181   /* session phase */
   182 
   183   val session_phase_changed: Session.Phase => Unit =
   184   {
   185     case Session.Terminated(result) if !result.ok =>
   186       GUI_Thread.later {
   187         GUI.error_dialog(jEdit.getActiveView, "Prover process terminated with error",
   188           "Isabelle Syslog", GUI.scrollable_text(session.syslog_content()))
   189       }
   190 
   191     case Session.Ready =>
   192       init_models()
   193 
   194       if (!Isabelle.continuous_checking) {
   195         GUI_Thread.later {
   196           val answer =
   197             GUI.confirm_dialog(jEdit.getActiveView,
   198               "Continuous checking of PIDE document",
   199               JOptionPane.YES_NO_OPTION,
   200               "Continuous checking is presently disabled:",
   201               "editor buffers will remain inactive!",
   202               "Enable continuous checking now?")
   203           if (answer == 0) Isabelle.continuous_checking = true
   204         }
   205       }
   206 
   207       delay_load.invoke()
   208 
   209     case Session.Shutdown =>
   210       GUI_Thread.later {
   211         delay_load.revoke()
   212         delay_init.revoke()
   213         JEdit_Editor.flush()
   214         exit_models(JEdit_Lib.jedit_buffers().toList)
   215       }
   216 
   217     case _ =>
   218   }
   219 
   220 
   221   /* document model and view */
   222 
   223   def exit_models(buffers: List[Buffer])
   224   {
   225     GUI_Thread.now {
   226       buffers.foreach(buffer =>
   227         JEdit_Lib.buffer_lock(buffer) {
   228           JEdit_Lib.jedit_text_areas(buffer).foreach(Document_View.exit)
   229           Document_Model.exit(buffer)
   230         })
   231       }
   232   }
   233 
   234   def init_models()
   235   {
   236     GUI_Thread.now {
   237       JEdit_Editor.flush()
   238 
   239       for {
   240         buffer <- JEdit_Lib.jedit_buffers()
   241         if buffer != null && !buffer.getBooleanProperty(Buffer.GZIPPED)
   242       } {
   243         if (buffer.isLoaded) {
   244           JEdit_Lib.buffer_lock(buffer) {
   245             val node_name = resources.node_name(buffer)
   246             val model = Document_Model.init(session, node_name, buffer)
   247             for {
   248               text_area <- JEdit_Lib.jedit_text_areas(buffer)
   249               if Document_View.get(text_area).map(_.model) != Some(model)
   250             } Document_View.init(model, text_area)
   251           }
   252         }
   253         else delay_init.invoke()
   254       }
   255 
   256       JEdit_Editor.invoke_generated()
   257     }
   258   }
   259 
   260   def init_view(buffer: Buffer, text_area: JEditTextArea): Unit =
   261     GUI_Thread.now {
   262       JEdit_Lib.buffer_lock(buffer) {
   263         Document_Model.get(buffer) match {
   264           case Some(model) => Document_View.init(model, text_area)
   265           case None =>
   266         }
   267       }
   268     }
   269 
   270   def exit_view(buffer: Buffer, text_area: JEditTextArea): Unit =
   271     GUI_Thread.now {
   272       JEdit_Lib.buffer_lock(buffer) {
   273         Document_View.exit(text_area)
   274       }
   275     }
   276 
   277 
   278   /* main plugin plumbing */
   279 
   280   @volatile private var startup_failure: Option[Throwable] = None
   281   @volatile private var startup_notified = false
   282 
   283   override def handleMessage(message: EBMessage)
   284   {
   285     GUI_Thread.assert {}
   286 
   287     if (startup_failure.isDefined && !startup_notified) {
   288       message match {
   289         case msg: EditorStarted =>
   290           GUI.error_dialog(null, "Isabelle plugin startup failure",
   291             GUI.scrollable_text(Exn.message(startup_failure.get)),
   292             "Prover IDE inactive!")
   293           startup_notified = true
   294         case _ =>
   295       }
   296     }
   297 
   298     if (startup_failure.isEmpty) {
   299       message match {
   300         case msg: EditorStarted =>
   301           if (Distribution.is_identified && !Distribution.is_official) {
   302             GUI.warning_dialog(jEdit.getActiveView, "Isabelle version for testing",
   303               "This is " + Distribution.version + ".",
   304               "It is for testing only, not for production use.")
   305           }
   306 
   307           val view = jEdit.getActiveView()
   308 
   309           Session_Build.check_dialog(view)
   310 
   311           Keymap_Merge.check_dialog(view)
   312 
   313           JEdit_Editor.hyperlink_position(true, Document.Snapshot.init,
   314             JEdit_Sessions.session_info(options.value).open_root).foreach(_.follow(view))
   315 
   316         case msg: BufferUpdate
   317         if msg.getWhat == BufferUpdate.LOAD_STARTED || msg.getWhat == BufferUpdate.CLOSING =>
   318           if (msg.getBuffer != null) {
   319             exit_models(List(msg.getBuffer))
   320             JEdit_Editor.invoke_generated()
   321           }
   322 
   323         case msg: BufferUpdate
   324         if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED || msg.getWhat == BufferUpdate.LOADED =>
   325           if (session.is_ready) {
   326             delay_init.invoke()
   327             delay_load.invoke()
   328           }
   329 
   330         case msg: EditPaneUpdate
   331         if msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
   332             msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
   333             msg.getWhat == EditPaneUpdate.CREATED ||
   334             msg.getWhat == EditPaneUpdate.DESTROYED =>
   335           val edit_pane = msg.getEditPane
   336           val buffer = edit_pane.getBuffer
   337           val text_area = edit_pane.getTextArea
   338 
   339           if (buffer != null && text_area != null) {
   340             if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
   341                 msg.getWhat == EditPaneUpdate.CREATED) {
   342               if (session.is_ready)
   343                 init_view(buffer, text_area)
   344             }
   345             else {
   346               Isabelle.dismissed_popups(text_area.getView)
   347               exit_view(buffer, text_area)
   348             }
   349 
   350             if (msg.getWhat == EditPaneUpdate.CREATED)
   351               Completion_Popup.Text_Area.init(text_area)
   352 
   353             if (msg.getWhat == EditPaneUpdate.DESTROYED)
   354               Completion_Popup.Text_Area.exit(text_area)
   355           }
   356 
   357         case msg: PropertiesChanged =>
   358           for {
   359             view <- JEdit_Lib.jedit_views
   360             edit_pane <- JEdit_Lib.jedit_edit_panes(view)
   361           } {
   362             val buffer = edit_pane.getBuffer
   363             val text_area = edit_pane.getTextArea
   364             if (buffer != null && text_area != null) init_view(buffer, text_area)
   365           }
   366 
   367           spell_checker.update(options.value)
   368           session.update_options(options.value)
   369 
   370         case _ =>
   371       }
   372     }
   373   }
   374 
   375 
   376   /* mode provider */
   377 
   378   private var orig_mode_provider: ModeProvider = null
   379   private var pide_mode_provider: ModeProvider = null
   380 
   381   def init_mode_provider()
   382   {
   383     orig_mode_provider = ModeProvider.instance
   384     if (orig_mode_provider.isInstanceOf[ModeProvider]) {
   385       pide_mode_provider = new Token_Markup.Mode_Provider(orig_mode_provider)
   386       ModeProvider.instance = pide_mode_provider
   387     }
   388   }
   389 
   390   def exit_mode_provider()
   391   {
   392     if (ModeProvider.instance == pide_mode_provider)
   393       ModeProvider.instance = orig_mode_provider
   394   }
   395 
   396 
   397   /* HTTP server */
   398 
   399   val http_root: String = "/" + UUID.randomUUID().toString
   400 
   401   val http_server: HTTP.Server = HTTP.server(Document_Model.http_handlers(http_root))
   402 
   403 
   404   /* start and stop */
   405 
   406   override def start()
   407   {
   408     Debug.DISABLE_SEARCH_DIALOG_POOL = true
   409 
   410 
   411     /* strict initialization */
   412 
   413     init_options()
   414     init_resources()
   415     init_session()
   416     PIDE._plugin = this
   417 
   418 
   419     /* non-strict initialization */
   420 
   421     try {
   422       completion_history.load()
   423       spell_checker.update(options.value)
   424 
   425       SyntaxUtilities.setStyleExtender(Syntax_Style.Extender)
   426       init_mode_provider()
   427       JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)
   428 
   429       http_server.start
   430 
   431       startup_failure = None
   432     }
   433     catch {
   434       case exn: Throwable =>
   435         startup_failure = Some(exn)
   436         startup_notified = false
   437         Log.log(Log.ERROR, this, exn)
   438     }
   439   }
   440 
   441   override def stop()
   442   {
   443     http_server.stop
   444 
   445     exit_mode_provider()
   446     JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.exit _)
   447 
   448     if (startup_failure.isEmpty) {
   449       options.value.save_prefs()
   450       completion_history.value.save()
   451     }
   452 
   453     exit_models(JEdit_Lib.jedit_buffers().toList)
   454     session.stop()
   455     file_watcher.shutdown()
   456   }
   457 }