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