src/Tools/jEdit/src/plugin.scala
author wenzelm
Wed Jul 31 19:59:14 2013 +0200 (2013-07-31)
changeset 52815 eaad5fe7bb1b
parent 52807 b859a180936b
child 52816 c608e0ade554
permissions -rw-r--r--
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
just one module for Isabelle/jEdit actions;
     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.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
    18 import org.gjt.sp.jedit.syntax.ModeProvider
    19 import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
    20 
    21 import org.gjt.sp.util.SyntaxUtilities
    22 
    23 import scala.actors.Actor._
    24 
    25 
    26 object PIDE
    27 {
    28   /* plugin instance */
    29 
    30   val options = new JEdit_Options
    31 
    32   @volatile var startup_failure: Option[Throwable] = None
    33   @volatile var startup_notified = false
    34 
    35   @volatile var plugin: Plugin = null
    36   @volatile var session: Session = new Session(new JEdit_Thy_Load(Set.empty, Outer_Syntax.empty))
    37 
    38   def options_changed() { session.global_options.event(Session.Global_Options(options.value)) }
    39 
    40   def thy_load(): JEdit_Thy_Load =
    41     session.thy_load.asInstanceOf[JEdit_Thy_Load]
    42 
    43   def get_recent_syntax(): Option[Outer_Syntax] =
    44   {
    45     val current_session = session
    46     if (current_session.recent_syntax == Outer_Syntax.empty) None
    47     else Some(current_session.recent_syntax)
    48   }
    49 
    50 
    51   /* document model and view */
    52 
    53   def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
    54   def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area)
    55 
    56   def document_views(buffer: Buffer): List[Document_View] =
    57     for {
    58       text_area <- JEdit_Lib.jedit_text_areas(buffer).toList
    59       doc_view = document_view(text_area)
    60       if doc_view.isDefined
    61     } yield doc_view.get
    62 
    63   def exit_models(buffers: List[Buffer])
    64   {
    65     Swing_Thread.now {
    66       buffers.foreach(buffer =>
    67         JEdit_Lib.buffer_lock(buffer) {
    68           JEdit_Lib.jedit_text_areas(buffer).foreach(Document_View.exit)
    69           Document_Model.exit(buffer)
    70         })
    71       }
    72   }
    73 
    74   def init_models(buffers: List[Buffer])
    75   {
    76     Swing_Thread.now {
    77       val init_edits =
    78         (List.empty[Document.Edit_Text] /: buffers) { case (edits, buffer) =>
    79           JEdit_Lib.buffer_lock(buffer) {
    80             val (model_edits, opt_model) =
    81               thy_load.buffer_node_name(buffer) match {
    82                 case Some(node_name) =>
    83                   document_model(buffer) match {
    84                     case Some(model) if model.name == node_name => (Nil, Some(model))
    85                     case _ =>
    86                       val model = Document_Model.init(session, buffer, node_name)
    87                       (model.init_edits(), Some(model))
    88                   }
    89                 case None => (Nil, None)
    90               }
    91             if (opt_model.isDefined) {
    92               for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) {
    93                 if (document_view(text_area).map(_.model) != opt_model)
    94                   Document_View.init(opt_model.get, text_area)
    95               }
    96             }
    97             model_edits ::: edits
    98           }
    99         }
   100       session.update(init_edits)
   101     }
   102   }
   103 
   104   def init_view(buffer: Buffer, text_area: JEditTextArea)
   105   {
   106     JEdit_Lib.swing_buffer_lock(buffer) {
   107       document_model(buffer) match {
   108         case Some(model) => Document_View.init(model, text_area)
   109         case None =>
   110       }
   111     }
   112   }
   113 
   114   def exit_view(buffer: Buffer, text_area: JEditTextArea)
   115   {
   116     JEdit_Lib.swing_buffer_lock(buffer) {
   117       Document_View.exit(text_area)
   118     }
   119   }
   120 }
   121 
   122 
   123 class Plugin extends EBPlugin
   124 {
   125   /* theory files */
   126 
   127   private lazy val delay_init =
   128     Swing_Thread.delay_last(PIDE.options.seconds("editor_load_delay"))
   129     {
   130       PIDE.init_models(JEdit_Lib.jedit_buffers().toList)
   131     }
   132 
   133   private lazy val delay_load =
   134     Swing_Thread.delay_last(PIDE.options.seconds("editor_load_delay"))
   135     {
   136       val view = jEdit.getActiveView()
   137 
   138       val buffers = JEdit_Lib.jedit_buffers().toList
   139       if (buffers.forall(_.isLoaded)) {
   140         def loaded_buffer(name: String): Boolean =
   141           buffers.exists(buffer => JEdit_Lib.buffer_name(buffer) == name)
   142 
   143         val thys =
   144           for (buffer <- buffers; model <- PIDE.document_model(buffer))
   145             yield model.name
   146 
   147         val thy_info = new Thy_Info(PIDE.thy_load)
   148         // FIXME avoid I/O in Swing thread!?!
   149         val files = thy_info.dependencies(thys).deps.map(_.name.node).
   150           filter(file => !loaded_buffer(file) && PIDE.thy_load.check_file(view, file))
   151 
   152         if (!files.isEmpty) {
   153           val files_list = new ListView(files.sorted)
   154           for (i <- 0 until files.length)
   155             files_list.selection.indices += i
   156 
   157           val answer =
   158             GUI.confirm_dialog(view,
   159               "Auto loading of required files",
   160               JOptionPane.YES_NO_OPTION,
   161               "The following files are required to resolve theory imports.",
   162               "Reload selected files now?",
   163               new ScrollPane(files_list))
   164           if (answer == 0) {
   165             files.foreach(file =>
   166               if (files_list.selection.items.contains(file))
   167                 jEdit.openFile(null: View, file))
   168           }
   169         }
   170       }
   171     }
   172 
   173 
   174   /* session manager */
   175 
   176   private val session_manager = actor {
   177     loop {
   178       react {
   179         case phase: Session.Phase =>
   180           phase match {
   181             case Session.Inactive | Session.Failed =>
   182               Swing_Thread.later {
   183                 GUI.error_dialog(jEdit.getActiveView, "Prover process terminated",
   184                     "Isabelle Syslog", GUI.scrollable_text(PIDE.session.current_syslog()))
   185               }
   186 
   187             case Session.Ready =>
   188               PIDE.session.update_options(PIDE.options.value)
   189               PIDE.init_models(JEdit_Lib.jedit_buffers().toList)
   190               Swing_Thread.later { delay_load.invoke() }
   191 
   192             case Session.Shutdown =>
   193               PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
   194               Swing_Thread.later { delay_load.revoke() }
   195 
   196             case _ =>
   197           }
   198         case bad => java.lang.System.err.println("session_manager: ignoring bad message " + bad)
   199       }
   200     }
   201   }
   202 
   203 
   204   /* Mac OS X application hooks */
   205 
   206   def handle_quit(): Boolean =
   207   {
   208     jEdit.exit(jEdit.getActiveView(), true)
   209     false
   210   }
   211 
   212 
   213   /* main plugin plumbing */
   214 
   215   override def handleMessage(message: EBMessage)
   216   {
   217     Swing_Thread.assert()
   218 
   219     if (PIDE.startup_failure.isDefined && !PIDE.startup_notified) {
   220       message match {
   221         case msg: EditorStarted =>
   222           GUI.error_dialog(null, "Isabelle plugin startup failure",
   223             GUI.scrollable_text(Exn.message(PIDE.startup_failure.get)),
   224             "Prover IDE inactive!")
   225           PIDE.startup_notified = true
   226         case _ =>
   227       }
   228     }
   229 
   230     if (PIDE.startup_failure.isEmpty) {
   231       message match {
   232         case msg: EditorStarted =>
   233           PIDE.session.start(Isabelle_Logic.session_args())
   234 
   235         case msg: BufferUpdate
   236         if msg.getWhat == BufferUpdate.LOADED || msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
   237           if (PIDE.session.is_ready) {
   238             val buffer = msg.getBuffer
   239             if (buffer != null && !buffer.isLoading) delay_init.invoke()
   240             Swing_Thread.later { delay_load.invoke() }
   241           }
   242 
   243         case msg: EditPaneUpdate
   244         if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
   245             msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
   246             msg.getWhat == EditPaneUpdate.CREATED ||
   247             msg.getWhat == EditPaneUpdate.DESTROYED) =>
   248           val edit_pane = msg.getEditPane
   249           val buffer = edit_pane.getBuffer
   250           val text_area = edit_pane.getTextArea
   251 
   252           if (buffer != null && text_area != null) {
   253             if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
   254                 msg.getWhat == EditPaneUpdate.CREATED) {
   255               if (PIDE.session.is_ready)
   256                 PIDE.init_view(buffer, text_area)
   257             }
   258             else PIDE.exit_view(buffer, text_area)
   259           }
   260 
   261         case msg: PropertiesChanged =>
   262           PIDE.session.update_options(PIDE.options.value)
   263 
   264         case _ =>
   265       }
   266     }
   267   }
   268 
   269   override def start()
   270   {
   271     try {
   272       Debug.DISABLE_SEARCH_DIALOG_POOL = true
   273 
   274       PIDE.plugin = this
   275       Isabelle_System.init()
   276       Isabelle_Font.install_fonts()
   277 
   278       val init_options = Options.init()
   279       Swing_Thread.now { PIDE.options.update(init_options)  }
   280 
   281       if (Platform.is_macos && PIDE.options.bool("jedit_mac_adapter"))
   282         OSX_Adapter.set_quit_handler(this, this.getClass.getDeclaredMethod("handle_quit"))
   283 
   284       SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
   285       if (ModeProvider.instance.isInstanceOf[ModeProvider])
   286         ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)
   287 
   288       val content = Isabelle_Logic.session_content(false)
   289       val thy_load = new JEdit_Thy_Load(content.loaded_theories, content.syntax)
   290 
   291       PIDE.session = new Session(thy_load) {
   292         override def output_delay = PIDE.options.seconds("editor_output_delay")
   293         override def reparse_limit = PIDE.options.int("editor_reparse_limit")
   294       }
   295 
   296       PIDE.session.phase_changed += session_manager
   297       PIDE.startup_failure = None
   298     }
   299     catch {
   300       case exn: Throwable =>
   301         PIDE.startup_failure = Some(exn)
   302         PIDE.startup_notified = false
   303     }
   304   }
   305 
   306   override def stop()
   307   {
   308     if (PIDE.startup_failure.isEmpty)
   309       PIDE.options.value.save_prefs()
   310 
   311     PIDE.session.phase_changed -= session_manager
   312     PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
   313     PIDE.session.stop()
   314   }
   315 }