src/Tools/jEdit/src/plugin.scala
author wenzelm
Fri Apr 25 12:51:08 2014 +0200 (2014-04-25)
changeset 56715 52125652e82a
parent 56662 f373fb77e0a4
child 56770 e160ae47db94
permissions -rw-r--r--
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
eliminated old actors;
     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 = new Session(new JEdit_Resources(Set.empty, Outer_Syntax.empty))
    39 
    40   def options_changed() { plugin.options_changed() }
    41   def deps_changed() { 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_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
    67 
    68   def document_view(text_area: TextArea): Option[Document_View] = Document_View(text_area)
    69 
    70   def document_views(buffer: Buffer): List[Document_View] =
    71     for {
    72       text_area <- JEdit_Lib.jedit_text_areas(buffer).toList
    73       doc_view <- document_view(text_area)
    74     } yield doc_view
    75 
    76   def document_models(): List[Document_Model] =
    77     for {
    78       buffer <- JEdit_Lib.jedit_buffers().toList
    79       model <- document_model(buffer)
    80     } yield model
    81 
    82   def document_blobs(): Document.Blobs =
    83     Document.Blobs(
    84       (for {
    85         buffer <- JEdit_Lib.jedit_buffers()
    86         model <- document_model(buffer)
    87         blob <- model.get_blob()
    88       } yield (model.node_name -> blob)).toMap)
    89 
    90   def exit_models(buffers: List[Buffer])
    91   {
    92     Swing_Thread.now {
    93       PIDE.editor.flush()
    94       buffers.foreach(buffer =>
    95         JEdit_Lib.buffer_lock(buffer) {
    96           JEdit_Lib.jedit_text_areas(buffer).foreach(Document_View.exit)
    97           Document_Model.exit(buffer)
    98         })
    99       }
   100   }
   101 
   102   def init_models()
   103   {
   104     Swing_Thread.now {
   105       PIDE.editor.flush()
   106 
   107       for {
   108         buffer <- JEdit_Lib.jedit_buffers()
   109         if buffer != null && !buffer.isLoading && !buffer.getBooleanProperty(Buffer.GZIPPED)
   110       } {
   111         JEdit_Lib.buffer_lock(buffer) {
   112           val node_name = resources.node_name(buffer)
   113           val model =
   114             document_model(buffer) match {
   115               case Some(model) if model.node_name == node_name => model
   116               case _ => Document_Model.init(session, buffer, node_name)
   117             }
   118           for {
   119             text_area <- JEdit_Lib.jedit_text_areas(buffer)
   120             if document_view(text_area).map(_.model) != Some(model)
   121           } Document_View.init(model, text_area)
   122         }
   123       }
   124 
   125       PIDE.editor.invoke()
   126     }
   127   }
   128 
   129   def init_view(buffer: Buffer, text_area: JEditTextArea)
   130   {
   131     JEdit_Lib.swing_buffer_lock(buffer) {
   132       document_model(buffer) match {
   133         case Some(model) => Document_View.init(model, text_area)
   134         case None =>
   135       }
   136     }
   137   }
   138 
   139   def exit_view(buffer: Buffer, text_area: JEditTextArea)
   140   {
   141     JEdit_Lib.swing_buffer_lock(buffer) {
   142       Document_View.exit(text_area)
   143     }
   144   }
   145 
   146 
   147   /* current document content */
   148 
   149   def snapshot(view: View): Document.Snapshot =
   150   {
   151     val buffer = view.getBuffer
   152     document_model(buffer) match {
   153       case Some(model) => model.snapshot
   154       case None => error("No document model for current buffer")
   155     }
   156   }
   157 
   158   def rendering(view: View): Rendering =
   159   {
   160     val text_area = view.getTextArea
   161     document_view(text_area) match {
   162       case Some(doc_view) => doc_view.get_rendering()
   163       case None => error("No document view for current text area")
   164     }
   165   }
   166 }
   167 
   168 
   169 class Plugin extends EBPlugin
   170 {
   171   /* global changes */
   172 
   173   def options_changed()
   174   {
   175     PIDE.session.global_options.post(Session.Global_Options(PIDE.options.value))
   176     Swing_Thread.later { delay_load.invoke() }
   177   }
   178 
   179   def deps_changed()
   180   {
   181     Swing_Thread.later { delay_load.invoke() }
   182   }
   183 
   184 
   185   /* theory files */
   186 
   187   private lazy val delay_init =
   188     Swing_Thread.delay_last(PIDE.options.seconds("editor_load_delay"))
   189     {
   190       PIDE.init_models()
   191     }
   192 
   193   private lazy val delay_load =
   194     Swing_Thread.delay_last(PIDE.options.seconds("editor_load_delay"))
   195     {
   196       if (Isabelle.continuous_checking) {
   197         val view = jEdit.getActiveView()
   198 
   199         val buffers = JEdit_Lib.jedit_buffers().toList
   200         if (buffers.forall(_.isLoaded)) {
   201           def loaded_buffer(name: String): Boolean =
   202             buffers.exists(buffer => JEdit_Lib.buffer_name(buffer) == name)
   203 
   204           val thys =
   205             for {
   206               buffer <- buffers
   207               model <- PIDE.document_model(buffer)
   208               if model.is_theory
   209             } yield (model.node_name, Position.none)
   210 
   211           val thy_info = new Thy_Info(PIDE.resources)
   212           // FIXME avoid I/O in Swing thread!?!
   213           val files = thy_info.dependencies(thys).deps.map(_.name.node).
   214             filter(file => !loaded_buffer(file) && PIDE.resources.check_file(view, file))
   215 
   216           if (!files.isEmpty) {
   217             if (PIDE.options.bool("jedit_auto_load")) {
   218               files.foreach(file => jEdit.openFile(null: View, file))
   219             }
   220             else {
   221               val files_list = new ListView(files.sorted)
   222               for (i <- 0 until files.length)
   223                 files_list.selection.indices += i
   224 
   225               val answer =
   226                 GUI.confirm_dialog(view,
   227                   "Auto loading of required files",
   228                   JOptionPane.YES_NO_OPTION,
   229                   "The following files are required to resolve theory imports.",
   230                   "Reload selected files now?",
   231                   new ScrollPane(files_list),
   232                   new Isabelle.Continuous_Checking)
   233               if (answer == 0) {
   234                 files.foreach(file =>
   235                   if (files_list.selection.items.contains(file))
   236                     jEdit.openFile(null: View, file))
   237               }
   238             }
   239           }
   240         }
   241       }
   242     }
   243 
   244 
   245   /* session phase */
   246 
   247   private val session_phase =
   248     Session.Consumer[Session.Phase](getClass.getName) {
   249       case Session.Inactive | Session.Failed =>
   250         Swing_Thread.later {
   251           GUI.error_dialog(jEdit.getActiveView, "Prover process terminated",
   252               "Isabelle Syslog", GUI.scrollable_text(PIDE.session.current_syslog()))
   253         }
   254 
   255       case Session.Ready =>
   256         PIDE.session.update_options(PIDE.options.value)
   257         PIDE.init_models()
   258         Swing_Thread.later { delay_load.invoke() }
   259 
   260       case Session.Shutdown =>
   261         PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
   262         Swing_Thread.later { delay_load.revoke() }
   263 
   264       case _ =>
   265     }
   266 
   267 
   268   /* main plugin plumbing */
   269 
   270   override def handleMessage(message: EBMessage)
   271   {
   272     Swing_Thread.assert {}
   273 
   274     if (PIDE.startup_failure.isDefined && !PIDE.startup_notified) {
   275       message match {
   276         case msg: EditorStarted =>
   277           GUI.error_dialog(null, "Isabelle plugin startup failure",
   278             GUI.scrollable_text(Exn.message(PIDE.startup_failure.get)),
   279             "Prover IDE inactive!")
   280           PIDE.startup_notified = true
   281         case _ =>
   282       }
   283     }
   284 
   285     if (PIDE.startup_failure.isEmpty) {
   286       message match {
   287         case msg: EditorStarted =>
   288           PIDE.session.start("Isabelle", Isabelle_Logic.session_args())
   289 
   290         case msg: BufferUpdate
   291         if msg.getWhat == BufferUpdate.LOADED || msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
   292           if (PIDE.session.is_ready) {
   293             delay_init.invoke()
   294             delay_load.invoke()
   295           }
   296 
   297         case msg: EditPaneUpdate
   298         if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
   299             msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
   300             msg.getWhat == EditPaneUpdate.CREATED ||
   301             msg.getWhat == EditPaneUpdate.DESTROYED) =>
   302           val edit_pane = msg.getEditPane
   303           val buffer = edit_pane.getBuffer
   304           val text_area = edit_pane.getTextArea
   305 
   306           if (buffer != null && text_area != null) {
   307             if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
   308                 msg.getWhat == EditPaneUpdate.CREATED) {
   309               if (PIDE.session.is_ready)
   310                 PIDE.init_view(buffer, text_area)
   311             }
   312             else {
   313               PIDE.dismissed_popups(text_area.getView)
   314               PIDE.exit_view(buffer, text_area)
   315             }
   316 
   317             if (msg.getWhat == EditPaneUpdate.CREATED)
   318               Completion_Popup.Text_Area.init(text_area)
   319 
   320             if (msg.getWhat == EditPaneUpdate.DESTROYED)
   321               Completion_Popup.Text_Area.exit(text_area)
   322           }
   323 
   324         case msg: PropertiesChanged =>
   325           PIDE.spell_checker.update(PIDE.options.value)
   326           PIDE.session.update_options(PIDE.options.value)
   327 
   328         case _ =>
   329       }
   330     }
   331   }
   332 
   333   override def start()
   334   {
   335     try {
   336       Debug.DISABLE_SEARCH_DIALOG_POOL = true
   337 
   338       PIDE.plugin = this
   339       Isabelle_System.init()
   340       Isabelle_Font.install_fonts()
   341 
   342       PIDE.options.update(Options.init())
   343       PIDE.completion_history.load()
   344       PIDE.spell_checker.update(PIDE.options.value)
   345 
   346       SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
   347       if (ModeProvider.instance.isInstanceOf[ModeProvider])
   348         ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)
   349 
   350       JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)
   351 
   352       val content = Isabelle_Logic.session_content(false)
   353       val resources = new JEdit_Resources(content.loaded_theories, content.syntax)
   354 
   355       PIDE.session = new Session(resources) {
   356         override def output_delay = PIDE.options.seconds("editor_output_delay")
   357         override def reparse_limit = PIDE.options.int("editor_reparse_limit")
   358       }
   359 
   360       PIDE.session.phase_changed += session_phase
   361       PIDE.startup_failure = None
   362     }
   363     catch {
   364       case exn: Throwable =>
   365         PIDE.startup_failure = Some(exn)
   366         PIDE.startup_notified = false
   367     }
   368   }
   369 
   370   override def stop()
   371   {
   372     JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.exit _)
   373 
   374     if (PIDE.startup_failure.isEmpty) {
   375       PIDE.options.value.save_prefs()
   376       PIDE.completion_history.value.save()
   377     }
   378 
   379     PIDE.session.phase_changed -= session_phase
   380     PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
   381     PIDE.session.stop()
   382   }
   383 }