src/Tools/jEdit/src/plugin.scala
author wenzelm
Sat Jan 07 14:34:53 2017 +0100 (2017-01-07)
changeset 64817 0bb6b582bb4f
parent 64813 7283f41d05ab
child 64818 67a0a563d2b3
permissions -rw-r--r--
separate Buffer_Model vs. File_Model;
misc tuning and clarification;
     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 scala.swing.{ListView, ScrollPane}
    15 
    16 import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, Debug, PerspectiveManager}
    17 import org.gjt.sp.jedit.gui.AboutDialog
    18 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
    19 import org.gjt.sp.jedit.buffer.JEditBuffer
    20 import org.gjt.sp.jedit.syntax.ModeProvider
    21 import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
    22 import org.gjt.sp.util.SyntaxUtilities
    23 import org.gjt.sp.util.Log
    24 
    25 
    26 object PIDE
    27 {
    28   /* plugin instance */
    29 
    30   val options = new JEdit_Options
    31   val completion_history = new Completion.History_Variable
    32   val spell_checker = new Spell_Checker_Variable
    33 
    34   @volatile var startup_failure: Option[Throwable] = None
    35   @volatile var startup_notified = false
    36 
    37   @volatile var plugin: Plugin = null
    38   @volatile var session: Session = new Session(JEdit_Resources.empty)
    39 
    40   def options_changed() { if (plugin != null) plugin.options_changed() }
    41   def deps_changed() { if (plugin != null) plugin.deps_changed() }
    42 
    43   def resources(): JEdit_Resources =
    44     session.resources.asInstanceOf[JEdit_Resources]
    45 
    46   lazy val editor = new JEdit_Editor
    47 
    48 
    49   /* popups */
    50 
    51   def dismissed_popups(view: View): Boolean =
    52   {
    53     var dismissed = false
    54 
    55     JEdit_Lib.jedit_text_areas(view).foreach(text_area =>
    56       if (Completion_Popup.Text_Area.dismissed(text_area)) dismissed = true)
    57 
    58     if (Pretty_Tooltip.dismissed_all()) dismissed = true
    59 
    60     dismissed
    61   }
    62 
    63 
    64   /* document model and view */
    65 
    66   def document_view(text_area: TextArea): Option[Document_View] = Document_View(text_area)
    67 
    68   def document_views(buffer: Buffer): List[Document_View] =
    69     for {
    70       text_area <- JEdit_Lib.jedit_text_areas(buffer).toList
    71       doc_view <- document_view(text_area)
    72     } yield doc_view
    73 
    74   def exit_models(buffers: List[Buffer])
    75   {
    76     GUI_Thread.now {
    77       PIDE.editor.flush()
    78       buffers.foreach(buffer =>
    79         JEdit_Lib.buffer_lock(buffer) {
    80           JEdit_Lib.jedit_text_areas(buffer).foreach(Document_View.exit)
    81           Document_Model.exit(buffer)
    82         })
    83       }
    84   }
    85 
    86   def init_models()
    87   {
    88     GUI_Thread.now {
    89       PIDE.editor.flush()
    90 
    91       for {
    92         buffer <- JEdit_Lib.jedit_buffers()
    93         if buffer != null && !buffer.getBooleanProperty(Buffer.GZIPPED)
    94       } {
    95         if (buffer.isLoaded) {
    96           JEdit_Lib.buffer_lock(buffer) {
    97             val node_name = resources.node_name(buffer)
    98             val model = Document_Model.init(session, node_name, buffer)
    99             for {
   100               text_area <- JEdit_Lib.jedit_text_areas(buffer)
   101               if document_view(text_area).map(_.model) != Some(model)
   102             } Document_View.init(model, text_area)
   103           }
   104         }
   105         else if (plugin != null) plugin.delay_init.invoke()
   106       }
   107 
   108       PIDE.editor.invoke_generated()
   109     }
   110   }
   111 
   112   def init_view(buffer: Buffer, text_area: JEditTextArea): Unit =
   113     GUI_Thread.now {
   114       JEdit_Lib.buffer_lock(buffer) {
   115         Document_Model.get(buffer) match {
   116           case Some(model) => Document_View.init(model, text_area)
   117           case None =>
   118         }
   119       }
   120     }
   121 
   122   def exit_view(buffer: Buffer, text_area: JEditTextArea): Unit =
   123     GUI_Thread.now {
   124       JEdit_Lib.buffer_lock(buffer) {
   125         Document_View.exit(text_area)
   126       }
   127     }
   128 
   129 
   130   /* current document content */
   131 
   132   def snapshot(view: View): Document.Snapshot = GUI_Thread.now
   133   {
   134     Document_Model.get(view.getBuffer) match {
   135       case Some(model) => model.snapshot
   136       case None => error("No document model for current buffer")
   137     }
   138   }
   139 
   140   def rendering(view: View): JEdit_Rendering = GUI_Thread.now
   141   {
   142     val text_area = view.getTextArea
   143     document_view(text_area) match {
   144       case Some(doc_view) => doc_view.get_rendering()
   145       case None => error("No document view for current text area")
   146     }
   147   }
   148 }
   149 
   150 
   151 class Plugin extends EBPlugin
   152 {
   153   /* global changes */
   154 
   155   def options_changed()
   156   {
   157     PIDE.session.global_options.post(Session.Global_Options(PIDE.options.value))
   158     delay_load.invoke()
   159   }
   160 
   161   def deps_changed()
   162   {
   163     delay_load.invoke()
   164   }
   165 
   166 
   167   /* theory files */
   168 
   169   lazy val delay_init =
   170     GUI_Thread.delay_last(PIDE.options.seconds("editor_load_delay"))
   171     {
   172       PIDE.init_models()
   173     }
   174 
   175   private val delay_load_active = Synchronized(false)
   176   private def delay_load_activated(): Boolean =
   177     delay_load_active.guarded_access(a => Some((!a, true)))
   178   private def delay_load_action()
   179   {
   180     if (Isabelle.continuous_checking && delay_load_activated() &&
   181         PerspectiveManager.isPerspectiveEnabled)
   182     {
   183       try {
   184         val view = jEdit.getActiveView()
   185 
   186         val buffers = JEdit_Lib.jedit_buffers().toList
   187         if (buffers.forall(_.isLoaded)) {
   188           def loaded_buffer(name: String): Boolean =
   189             buffers.exists(buffer => JEdit_Lib.buffer_name(buffer) == name)
   190 
   191           val thys =
   192             for {
   193               buffer <- buffers
   194               model <- Document_Model.get(buffer)
   195               if model.is_theory
   196             } yield (model.node_name, Position.none)
   197 
   198           val thy_info = new Thy_Info(PIDE.resources)
   199           val thy_files = thy_info.dependencies("", thys).deps.map(_.name.node)
   200 
   201           val aux_files =
   202             if (PIDE.options.bool("jedit_auto_resolve")) {
   203               PIDE.editor.stable_tip_version() match {
   204                 case Some(version) => PIDE.resources.undefined_blobs(version.nodes).map(_.node)
   205                 case None => delay_load.invoke(); Nil
   206               }
   207             }
   208             else Nil
   209 
   210           val files =
   211             (thy_files ::: aux_files).filter(file =>
   212               !loaded_buffer(file) && PIDE.resources.check_file(file))
   213 
   214           if (files.nonEmpty) {
   215             if (PIDE.options.bool("jedit_auto_load")) {
   216               files.foreach(file => jEdit.openFile(null: View, file))
   217             }
   218             else {
   219               val files_list = new ListView(files.sorted)
   220               for (i <- 0 until files.length)
   221                 files_list.selection.indices += i
   222 
   223               val answer =
   224                 GUI.confirm_dialog(view,
   225                   "Auto loading of required files",
   226                   JOptionPane.YES_NO_OPTION,
   227                   "The following files are required to resolve theory imports.",
   228                   "Reload selected files now?",
   229                   new ScrollPane(files_list),
   230                   new Isabelle.Continuous_Checking)
   231               if (answer == 0) {
   232                 files.foreach(file =>
   233                   if (files_list.selection.items.contains(file))
   234                     jEdit.openFile(null: View, file))
   235               }
   236             }
   237           }
   238         }
   239         else delay_load.invoke()
   240       }
   241       finally { delay_load_active.change(_ => false) }
   242     }
   243   }
   244 
   245   private lazy val delay_load =
   246     GUI_Thread.delay_last(PIDE.options.seconds("editor_load_delay")) { delay_load_action() }
   247 
   248 
   249   /* session phase */
   250 
   251   private val session_phase =
   252     Session.Consumer[Session.Phase](getClass.getName) {
   253       case Session.Inactive | Session.Failed =>
   254         GUI_Thread.later {
   255           GUI.error_dialog(jEdit.getActiveView, "Prover process terminated",
   256             "Isabelle Syslog", GUI.scrollable_text(PIDE.session.syslog_content()))
   257         }
   258 
   259       case Session.Ready =>
   260         Debugger.init_session(PIDE.session)
   261         PIDE.session.update_options(PIDE.options.value)
   262         PIDE.init_models()
   263 
   264         if (!Isabelle.continuous_checking) {
   265           GUI_Thread.later {
   266             val answer =
   267               GUI.confirm_dialog(jEdit.getActiveView,
   268                 "Continuous checking of PIDE document",
   269                 JOptionPane.YES_NO_OPTION,
   270                 "Continuous checking is presently disabled:",
   271                 "editor buffers will remain inactive!",
   272                 "Enable continuous checking now?")
   273             if (answer == 0) Isabelle.continuous_checking = true
   274           }
   275         }
   276 
   277         delay_load.invoke()
   278 
   279       case Session.Shutdown =>
   280         GUI_Thread.later {
   281           delay_load.revoke()
   282           PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
   283         }
   284 
   285       case _ =>
   286     }
   287 
   288 
   289   /* main plugin plumbing */
   290 
   291   override def handleMessage(message: EBMessage)
   292   {
   293     GUI_Thread.assert {}
   294 
   295     if (PIDE.startup_failure.isDefined && !PIDE.startup_notified) {
   296       message match {
   297         case msg: EditorStarted =>
   298           GUI.error_dialog(null, "Isabelle plugin startup failure",
   299             GUI.scrollable_text(Exn.message(PIDE.startup_failure.get)),
   300             "Prover IDE inactive!")
   301           PIDE.startup_notified = true
   302         case _ =>
   303       }
   304     }
   305 
   306     if (PIDE.startup_failure.isEmpty) {
   307       message match {
   308         case msg: EditorStarted =>
   309           if (Distribution.is_identified && !Distribution.is_official) {
   310             GUI.warning_dialog(jEdit.getActiveView, "Isabelle version for testing",
   311               "This is " + Distribution.version + ".",
   312               "It is for testing only, not for production use.")
   313           }
   314 
   315           val view = jEdit.getActiveView()
   316 
   317           Session_Build.session_build(view)
   318 
   319           Keymap_Merge.check_dialog(view)
   320 
   321           PIDE.editor.hyperlink_position(true, Document.Snapshot.init,
   322             JEdit_Sessions.session_info().open_root).foreach(_.follow(view))
   323 
   324         case msg: BufferUpdate
   325         if msg.getWhat == BufferUpdate.LOADED ||
   326           msg.getWhat == BufferUpdate.PROPERTIES_CHANGED ||
   327           msg.getWhat == BufferUpdate.CLOSING =>
   328 
   329           if (msg.getWhat == BufferUpdate.CLOSING && msg.getBuffer != null)
   330             PIDE.exit_models(List(msg.getBuffer))
   331 
   332           if (PIDE.session.is_ready) {
   333             delay_init.invoke()
   334             delay_load.invoke()
   335           }
   336 
   337         case msg: EditPaneUpdate
   338         if msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
   339             msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
   340             msg.getWhat == EditPaneUpdate.CREATED ||
   341             msg.getWhat == EditPaneUpdate.DESTROYED =>
   342           val edit_pane = msg.getEditPane
   343           val buffer = edit_pane.getBuffer
   344           val text_area = edit_pane.getTextArea
   345 
   346           if (buffer != null && text_area != null) {
   347             if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
   348                 msg.getWhat == EditPaneUpdate.CREATED) {
   349               if (PIDE.session.is_ready)
   350                 PIDE.init_view(buffer, text_area)
   351             }
   352             else {
   353               PIDE.dismissed_popups(text_area.getView)
   354               PIDE.exit_view(buffer, text_area)
   355             }
   356 
   357             if (msg.getWhat == EditPaneUpdate.CREATED)
   358               Completion_Popup.Text_Area.init(text_area)
   359 
   360             if (msg.getWhat == EditPaneUpdate.DESTROYED)
   361               Completion_Popup.Text_Area.exit(text_area)
   362           }
   363 
   364         case msg: PropertiesChanged =>
   365           for {
   366             view <- JEdit_Lib.jedit_views
   367             edit_pane <- JEdit_Lib.jedit_edit_panes(view)
   368           } {
   369             val buffer = edit_pane.getBuffer
   370             val text_area = edit_pane.getTextArea
   371             if (buffer != null && text_area != null) PIDE.init_view(buffer, text_area)
   372           }
   373 
   374           PIDE.spell_checker.update(PIDE.options.value)
   375           PIDE.session.update_options(PIDE.options.value)
   376 
   377         case _ =>
   378       }
   379     }
   380   }
   381 
   382   override def start()
   383   {
   384     try {
   385       Debug.DISABLE_SEARCH_DIALOG_POOL = true
   386 
   387       PIDE.plugin = this
   388       PIDE.options.store(Options.init())
   389       PIDE.completion_history.load()
   390       PIDE.spell_checker.update(PIDE.options.value)
   391 
   392       SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
   393       if (ModeProvider.instance.isInstanceOf[ModeProvider])
   394         ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)
   395 
   396       JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)
   397 
   398       val content = JEdit_Sessions.session_content(false)
   399       val resources =
   400         new JEdit_Resources(content.loaded_theories, content.known_theories, content.syntax)
   401 
   402       PIDE.session.stop()
   403       PIDE.session = new Session(resources) {
   404         override def output_delay = PIDE.options.seconds("editor_output_delay")
   405         override def prune_delay = PIDE.options.seconds("editor_prune_delay")
   406         override def syslog_limit = PIDE.options.int("editor_syslog_limit")
   407         override def reparse_limit = PIDE.options.int("editor_reparse_limit")
   408       }
   409 
   410       PIDE.session.phase_changed += session_phase
   411       PIDE.startup_failure = None
   412     }
   413     catch {
   414       case exn: Throwable =>
   415         PIDE.startup_failure = Some(exn)
   416         PIDE.startup_notified = false
   417         Log.log(Log.ERROR, this, exn)
   418     }
   419   }
   420 
   421   override def stop()
   422   {
   423     JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.exit _)
   424 
   425     if (PIDE.startup_failure.isEmpty) {
   426       PIDE.options.value.save_prefs()
   427       PIDE.completion_history.value.save()
   428     }
   429 
   430     PIDE.session.phase_changed -= session_phase
   431     PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
   432     PIDE.session.stop()
   433   }
   434 }