src/Tools/jEdit/src/plugin.scala
author wenzelm
Wed Apr 30 22:34:11 2014 +0200 (2014-04-30)
changeset 56801 8dd9df88f647
parent 56775 59f70b89e5fd
child 56834 a752f065f3d3
permissions -rw-r--r--
some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
     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     Swing_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     Swing_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     Swing_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     Swing_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 =
   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 =
   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     Swing_Thread.delay_last(PIDE.options.seconds("editor_load_delay"))
   190     {
   191       PIDE.init_models()
   192     }
   193 
   194   private lazy val delay_load =
   195     Swing_Thread.delay_last(PIDE.options.seconds("editor_load_delay"))
   196     {
   197       if (Isabelle.continuous_checking) {
   198         val view = jEdit.getActiveView()
   199 
   200         val buffers = JEdit_Lib.jedit_buffers().toList
   201         if (buffers.forall(_.isLoaded)) {
   202           def loaded_buffer(name: String): Boolean =
   203             buffers.exists(buffer => JEdit_Lib.buffer_name(buffer) == name)
   204 
   205           val thys =
   206             for {
   207               buffer <- buffers
   208               model <- PIDE.document_model(buffer)
   209               if model.is_theory
   210             } yield (model.node_name, Position.none)
   211 
   212           val thy_info = new Thy_Info(PIDE.resources)
   213           // FIXME avoid I/O in Swing thread!?!
   214           val files = thy_info.dependencies("", thys).deps.map(_.name.node).
   215             filter(file => !loaded_buffer(file) && PIDE.resources.check_file(view, file))
   216 
   217           if (!files.isEmpty) {
   218             if (PIDE.options.bool("jedit_auto_load")) {
   219               files.foreach(file => jEdit.openFile(null: View, file))
   220             }
   221             else {
   222               val files_list = new ListView(files.sorted)
   223               for (i <- 0 until files.length)
   224                 files_list.selection.indices += i
   225 
   226               val answer =
   227                 GUI.confirm_dialog(view,
   228                   "Auto loading of required files",
   229                   JOptionPane.YES_NO_OPTION,
   230                   "The following files are required to resolve theory imports.",
   231                   "Reload selected files now?",
   232                   new ScrollPane(files_list),
   233                   new Isabelle.Continuous_Checking)
   234               if (answer == 0) {
   235                 files.foreach(file =>
   236                   if (files_list.selection.items.contains(file))
   237                     jEdit.openFile(null: View, file))
   238               }
   239             }
   240           }
   241         }
   242       }
   243     }
   244 
   245 
   246   /* session phase */
   247 
   248   private val session_phase =
   249     Session.Consumer[Session.Phase](getClass.getName) {
   250       case Session.Inactive | Session.Failed =>
   251         Swing_Thread.later {
   252           GUI.error_dialog(jEdit.getActiveView, "Prover process terminated",
   253             "Isabelle Syslog", GUI.scrollable_text(PIDE.session.syslog_content()))
   254         }
   255 
   256       case Session.Ready =>
   257         PIDE.session.update_options(PIDE.options.value)
   258         PIDE.init_models()
   259         delay_load.invoke()
   260 
   261       case Session.Shutdown =>
   262         PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
   263         delay_load.revoke()
   264 
   265       case _ =>
   266     }
   267 
   268 
   269   /* main plugin plumbing */
   270 
   271   override def handleMessage(message: EBMessage)
   272   {
   273     Swing_Thread.assert {}
   274 
   275     if (PIDE.startup_failure.isDefined && !PIDE.startup_notified) {
   276       message match {
   277         case msg: EditorStarted =>
   278           GUI.error_dialog(null, "Isabelle plugin startup failure",
   279             GUI.scrollable_text(Exn.message(PIDE.startup_failure.get)),
   280             "Prover IDE inactive!")
   281           PIDE.startup_notified = true
   282         case _ =>
   283       }
   284     }
   285 
   286     if (PIDE.startup_failure.isEmpty) {
   287       message match {
   288         case msg: EditorStarted =>
   289           PIDE.session.start("Isabelle", Isabelle_Logic.session_args())
   290 
   291         case msg: BufferUpdate
   292         if msg.getWhat == BufferUpdate.LOADED || msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
   293           if (PIDE.session.is_ready) {
   294             delay_init.invoke()
   295             delay_load.invoke()
   296           }
   297 
   298         case msg: EditPaneUpdate
   299         if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
   300             msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
   301             msg.getWhat == EditPaneUpdate.CREATED ||
   302             msg.getWhat == EditPaneUpdate.DESTROYED) =>
   303           val edit_pane = msg.getEditPane
   304           val buffer = edit_pane.getBuffer
   305           val text_area = edit_pane.getTextArea
   306 
   307           if (buffer != null && text_area != null) {
   308             if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
   309                 msg.getWhat == EditPaneUpdate.CREATED) {
   310               if (PIDE.session.is_ready)
   311                 PIDE.init_view(buffer, text_area)
   312             }
   313             else {
   314               PIDE.dismissed_popups(text_area.getView)
   315               PIDE.exit_view(buffer, text_area)
   316             }
   317 
   318             if (msg.getWhat == EditPaneUpdate.CREATED)
   319               Completion_Popup.Text_Area.init(text_area)
   320 
   321             if (msg.getWhat == EditPaneUpdate.DESTROYED)
   322               Completion_Popup.Text_Area.exit(text_area)
   323           }
   324 
   325         case msg: PropertiesChanged =>
   326           PIDE.spell_checker.update(PIDE.options.value)
   327           PIDE.session.update_options(PIDE.options.value)
   328 
   329         case _ =>
   330       }
   331     }
   332   }
   333 
   334   override def start()
   335   {
   336     try {
   337       Debug.DISABLE_SEARCH_DIALOG_POOL = true
   338 
   339       PIDE.plugin = this
   340       Isabelle_System.init()
   341       Isabelle_Font.install_fonts()
   342 
   343       PIDE.options.update(Options.init())
   344       PIDE.completion_history.load()
   345       PIDE.spell_checker.update(PIDE.options.value)
   346 
   347       SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
   348       if (ModeProvider.instance.isInstanceOf[ModeProvider])
   349         ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)
   350 
   351       JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)
   352 
   353       val content = Isabelle_Logic.session_content(false)
   354       val resources =
   355         new JEdit_Resources(content.loaded_theories, content.known_theories, content.syntax)
   356 
   357       PIDE.session = new Session(resources) {
   358         override def output_delay = PIDE.options.seconds("editor_output_delay")
   359         override def reparse_limit = PIDE.options.int("editor_reparse_limit")
   360       }
   361 
   362       PIDE.session.phase_changed += session_phase
   363       PIDE.startup_failure = None
   364     }
   365     catch {
   366       case exn: Throwable =>
   367         PIDE.startup_failure = Some(exn)
   368         PIDE.startup_notified = false
   369     }
   370   }
   371 
   372   override def stop()
   373   {
   374     JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.exit _)
   375 
   376     if (PIDE.startup_failure.isEmpty) {
   377       PIDE.options.value.save_prefs()
   378       PIDE.completion_history.value.save()
   379     }
   380 
   381     PIDE.session.phase_changed -= session_phase
   382     PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
   383     PIDE.session.stop()
   384   }
   385 }