src/Tools/jEdit/src/plugin.scala
author wenzelm
Fri Nov 30 14:46:00 2018 +0100 (12 months ago)
changeset 69377 81ae5893c556
parent 69255 800b1ce96fce
child 69458 5655af3ea5bd
permissions -rw-r--r--
use Isabelle fonts for all GUI look-and-feels;
     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 
    16 import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, PerspectiveManager}
    17 import org.gjt.sp.jedit.textarea.JEditTextArea
    18 import org.gjt.sp.jedit.syntax.ModeProvider
    19 import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged,
    20   ViewUpdate}
    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   object editor extends JEdit_Editor
    60 }
    61 
    62 class Plugin extends EBPlugin
    63 {
    64   /* options */
    65 
    66   private var _options: JEdit_Options = null
    67   private def init_options(): Unit = _options = new JEdit_Options(Options.init())
    68   def options: JEdit_Options = _options
    69 
    70 
    71   /* resources */
    72 
    73   private var _resources: JEdit_Resources = null
    74   private def init_resources(): Unit = _resources = JEdit_Resources(options.value)
    75   def resources: JEdit_Resources = _resources
    76 
    77 
    78   /* session */
    79 
    80   private var _session: Session = null
    81   private def init_session(): Unit = _session = new Session(options.value, resources)
    82   def session: Session = _session
    83 
    84 
    85   /* misc support */
    86 
    87   val completion_history = new Completion.History_Variable
    88   val spell_checker = new Spell_Checker_Variable
    89 
    90 
    91   /* global changes */
    92 
    93   def options_changed()
    94   {
    95     session.global_options.post(Session.Global_Options(options.value))
    96     delay_load.invoke()
    97   }
    98 
    99   def deps_changed()
   100   {
   101     delay_load.invoke()
   102   }
   103 
   104 
   105   /* theory files */
   106 
   107   lazy val delay_init =
   108     GUI_Thread.delay_last(options.seconds("editor_load_delay"))
   109     {
   110       init_models()
   111     }
   112 
   113   private val delay_load_active = Synchronized(false)
   114   private def delay_load_activated(): Boolean =
   115     delay_load_active.guarded_access(a => Some((!a, true)))
   116   private def delay_load_action()
   117   {
   118     if (Isabelle.continuous_checking && delay_load_activated() &&
   119         PerspectiveManager.isPerspectiveEnabled)
   120     {
   121       if (JEdit_Lib.jedit_buffers().exists(_.isLoading)) delay_load.invoke()
   122       else {
   123         val required_files =
   124         {
   125           val models = Document_Model.get_models()
   126 
   127           val thys =
   128             (for ((node_name, model) <- models.iterator if model.is_theory)
   129               yield (node_name, Position.none)).toList
   130           val thy_files1 = resources.dependencies(thys).theories
   131 
   132           val thy_files2 =
   133             (for {
   134               (name, _) <- models.iterator
   135               thy_name <- resources.make_theory_name(name)
   136             } yield thy_name).toList
   137 
   138           val aux_files =
   139             if (options.bool("jedit_auto_resolve")) {
   140               val stable_tip_version =
   141                 if (models.forall(p => p._2.is_stable))
   142                   session.current_state().stable_tip_version
   143                 else None
   144               stable_tip_version match {
   145                 case Some(version) => resources.undefined_blobs(version.nodes)
   146                 case None => delay_load.invoke(); Nil
   147               }
   148             }
   149             else Nil
   150 
   151           (thy_files1 ::: thy_files2 ::: aux_files).filterNot(models.isDefinedAt(_))
   152         }
   153         if (required_files.nonEmpty) {
   154           try {
   155             Standard_Thread.fork("resolve_dependencies") {
   156               val loaded_files =
   157                 for {
   158                   name <- required_files
   159                   text <- resources.read_file_content(name)
   160                 } yield (name, text)
   161 
   162               GUI_Thread.later {
   163                 try {
   164                   Document_Model.provide_files(session, loaded_files)
   165                   delay_init.invoke()
   166                 }
   167                 finally { delay_load_active.change(_ => false) }
   168               }
   169             }
   170           }
   171           catch { case _: Throwable => delay_load_active.change(_ => false) }
   172         }
   173         else delay_load_active.change(_ => false)
   174       }
   175     }
   176   }
   177 
   178   private lazy val delay_load =
   179     GUI_Thread.delay_last(options.seconds("editor_load_delay")) { delay_load_action() }
   180 
   181   private def file_watcher_action(changed: Set[JFile]): Unit =
   182     if (Document_Model.sync_files(changed)) PIDE.editor.invoke_generated()
   183 
   184   lazy val file_watcher: File_Watcher =
   185     File_Watcher(file_watcher_action _, options.seconds("editor_load_delay"))
   186 
   187 
   188   /* session phase */
   189 
   190   val session_phase_changed: Session.Phase => Unit =
   191   {
   192     case Session.Terminated(result) if !result.ok =>
   193       GUI_Thread.later {
   194         GUI.error_dialog(jEdit.getActiveView, "Prover process terminated with error",
   195           "Isabelle Syslog", GUI.scrollable_text(session.syslog_content()))
   196       }
   197 
   198     case Session.Ready =>
   199       init_models()
   200 
   201       if (!Isabelle.continuous_checking) {
   202         GUI_Thread.later {
   203           val answer =
   204             GUI.confirm_dialog(jEdit.getActiveView,
   205               "Continuous checking of PIDE document",
   206               JOptionPane.YES_NO_OPTION,
   207               "Continuous checking is presently disabled:",
   208               "editor buffers will remain inactive!",
   209               "Enable continuous checking now?")
   210           if (answer == 0) Isabelle.continuous_checking = true
   211         }
   212       }
   213 
   214       delay_load.invoke()
   215 
   216     case Session.Shutdown =>
   217       GUI_Thread.later {
   218         delay_load.revoke()
   219         delay_init.revoke()
   220         PIDE.editor.shutdown()
   221         exit_models(JEdit_Lib.jedit_buffers().toList)
   222       }
   223 
   224     case _ =>
   225   }
   226 
   227 
   228   /* document model and view */
   229 
   230   def exit_models(buffers: List[Buffer])
   231   {
   232     GUI_Thread.now {
   233       buffers.foreach(buffer =>
   234         JEdit_Lib.buffer_lock(buffer) {
   235           JEdit_Lib.jedit_text_areas(buffer).foreach(Document_View.exit)
   236           Document_Model.exit(buffer)
   237         })
   238       }
   239   }
   240 
   241   def init_models()
   242   {
   243     GUI_Thread.now {
   244       PIDE.editor.flush()
   245 
   246       for {
   247         buffer <- JEdit_Lib.jedit_buffers()
   248         if buffer != null && !buffer.getBooleanProperty(Buffer.GZIPPED)
   249       } {
   250         if (buffer.isLoaded) {
   251           JEdit_Lib.buffer_lock(buffer) {
   252             val node_name = resources.node_name(buffer)
   253             val model = Document_Model.init(session, node_name, buffer)
   254             for {
   255               text_area <- JEdit_Lib.jedit_text_areas(buffer)
   256               if Document_View.get(text_area).map(_.model) != Some(model)
   257             } Document_View.init(model, text_area)
   258           }
   259         }
   260         else delay_init.invoke()
   261       }
   262 
   263       PIDE.editor.invoke_generated()
   264     }
   265   }
   266 
   267   def init_view(buffer: Buffer, text_area: JEditTextArea): Unit =
   268     GUI_Thread.now {
   269       JEdit_Lib.buffer_lock(buffer) {
   270         Document_Model.get(buffer) match {
   271           case Some(model) => Document_View.init(model, text_area)
   272           case None =>
   273         }
   274       }
   275     }
   276 
   277   def exit_view(buffer: Buffer, text_area: JEditTextArea): Unit =
   278     GUI_Thread.now {
   279       JEdit_Lib.buffer_lock(buffer) {
   280         Document_View.exit(text_area)
   281       }
   282     }
   283 
   284 
   285   /* main plugin plumbing */
   286 
   287   @volatile private var startup_failure: Option[Throwable] = None
   288   @volatile private var startup_notified = false
   289 
   290   private def init_view(view: View)
   291   {
   292     Session_Build.check_dialog(view)
   293     Keymap_Merge.check_dialog(view)
   294   }
   295 
   296   private def init_title(view: View)
   297   {
   298     val title =
   299       proper_string(Isabelle_System.getenv("ISABELLE_IDENTIFIER")).getOrElse("Isabelle") +
   300         "/" + PIDE.resources.session_name
   301     val marker = "\u200B"
   302 
   303     val old_title = view.getViewConfig.title
   304     if (old_title == null || old_title.startsWith(marker)) {
   305       view.setUserTitle(marker + title)
   306     }
   307   }
   308 
   309   override def handleMessage(message: EBMessage)
   310   {
   311     GUI_Thread.assert {}
   312 
   313     if (startup_failure.isDefined && !startup_notified) {
   314       message match {
   315         case msg: EditorStarted =>
   316           GUI.error_dialog(null, "Isabelle plugin startup failure",
   317             GUI.scrollable_text(Exn.message(startup_failure.get)),
   318             "Prover IDE inactive!")
   319           startup_notified = true
   320         case _ =>
   321       }
   322     }
   323 
   324     if (startup_failure.isEmpty) {
   325       message match {
   326         case msg: EditorStarted =>
   327           if (Distribution.is_identified && !Distribution.is_official) {
   328             GUI.warning_dialog(jEdit.getActiveView, "Isabelle version for testing",
   329               "This is " + Distribution.version + ".",
   330               "It is for testing only, not for production use.")
   331           }
   332 
   333           if (resources.session_errors.nonEmpty) {
   334             GUI.warning_dialog(jEdit.getActiveView,
   335               "Bad session structure: may cause problems with theory imports",
   336               GUI.scrollable_text(cat_lines(resources.session_errors)))
   337           }
   338 
   339           jEdit.propertiesChanged()
   340 
   341           val view = jEdit.getActiveView()
   342           init_view(view)
   343 
   344           PIDE.editor.hyperlink_position(true, Document.Snapshot.init,
   345             JEdit_Sessions.logic_root(options.value)).foreach(_.follow(view))
   346 
   347         case msg: ViewUpdate
   348         if msg.getWhat == ViewUpdate.CREATED && msg.getView != null =>
   349           init_title(msg.getView)
   350 
   351         case msg: BufferUpdate
   352         if msg.getWhat == BufferUpdate.LOAD_STARTED || msg.getWhat == BufferUpdate.CLOSING =>
   353           if (msg.getBuffer != null) {
   354             exit_models(List(msg.getBuffer))
   355             PIDE.editor.invoke_generated()
   356           }
   357 
   358         case msg: BufferUpdate
   359         if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED || msg.getWhat == BufferUpdate.LOADED =>
   360           if (session.is_ready) {
   361             delay_init.invoke()
   362             delay_load.invoke()
   363           }
   364 
   365         case msg: EditPaneUpdate
   366         if msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
   367             msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
   368             msg.getWhat == EditPaneUpdate.CREATED ||
   369             msg.getWhat == EditPaneUpdate.DESTROYED =>
   370           val edit_pane = msg.getEditPane
   371           val buffer = edit_pane.getBuffer
   372           val text_area = edit_pane.getTextArea
   373 
   374           if (buffer != null && text_area != null) {
   375             if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
   376                 msg.getWhat == EditPaneUpdate.CREATED) {
   377               if (session.is_ready)
   378                 init_view(buffer, text_area)
   379             }
   380             else {
   381               Isabelle.dismissed_popups(text_area.getView)
   382               exit_view(buffer, text_area)
   383             }
   384 
   385             if (msg.getWhat == EditPaneUpdate.CREATED)
   386               Completion_Popup.Text_Area.init(text_area)
   387 
   388             if (msg.getWhat == EditPaneUpdate.DESTROYED)
   389               Completion_Popup.Text_Area.exit(text_area)
   390           }
   391 
   392         case msg: PropertiesChanged =>
   393           for {
   394             view <- JEdit_Lib.jedit_views
   395             edit_pane <- JEdit_Lib.jedit_edit_panes(view)
   396           } {
   397             val buffer = edit_pane.getBuffer
   398             val text_area = edit_pane.getTextArea
   399             if (buffer != null && text_area != null) init_view(buffer, text_area)
   400           }
   401 
   402           GUI.use_isabelle_fonts()
   403 
   404           spell_checker.update(options.value)
   405           session.update_options(options.value)
   406 
   407         case _ =>
   408       }
   409     }
   410   }
   411 
   412 
   413   /* mode provider */
   414 
   415   private var orig_mode_provider: ModeProvider = null
   416   private var pide_mode_provider: ModeProvider = null
   417 
   418   def init_mode_provider()
   419   {
   420     orig_mode_provider = ModeProvider.instance
   421     if (orig_mode_provider.isInstanceOf[ModeProvider]) {
   422       pide_mode_provider = new Token_Markup.Mode_Provider(orig_mode_provider)
   423       ModeProvider.instance = pide_mode_provider
   424     }
   425   }
   426 
   427   def exit_mode_provider()
   428   {
   429     if (ModeProvider.instance == pide_mode_provider)
   430       ModeProvider.instance = orig_mode_provider
   431   }
   432 
   433 
   434   /* HTTP server */
   435 
   436   val http_root: String = "/" + UUID()
   437 
   438   val http_server: HTTP.Server = HTTP.server(Document_Model.http_handlers(http_root))
   439 
   440 
   441   /* start and stop */
   442 
   443   override def start()
   444   {
   445     /* strict initialization */
   446 
   447     init_options()
   448     init_resources()
   449     init_session()
   450     PIDE._plugin = this
   451 
   452 
   453     /* non-strict initialization */
   454 
   455     try {
   456       completion_history.load()
   457       spell_checker.update(options.value)
   458 
   459       JEdit_Lib.jedit_views.foreach(init_title(_))
   460 
   461       isabelle.jedit_base.Syntax_Style.set_style_extender(Syntax_Style.Extender)
   462       init_mode_provider()
   463       JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)
   464 
   465       http_server.start
   466 
   467       startup_failure = None
   468     }
   469     catch {
   470       case exn: Throwable =>
   471         startup_failure = Some(exn)
   472         startup_notified = false
   473         Log.log(Log.ERROR, this, exn)
   474     }
   475 
   476     val view = jEdit.getActiveView()
   477     if (view != null) init_view(view)
   478   }
   479 
   480   override def stop()
   481   {
   482     http_server.stop
   483 
   484     isabelle.jedit_base.Syntax_Style.dummy_style_extender()
   485     exit_mode_provider()
   486     JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.exit _)
   487 
   488     if (startup_failure.isEmpty) {
   489       options.value.save_prefs()
   490       completion_history.value.save()
   491     }
   492 
   493     exit_models(JEdit_Lib.jedit_buffers().toList)
   494     session.stop()
   495     file_watcher.shutdown()
   496     PIDE.editor.shutdown()
   497   }
   498 }