src/Tools/jEdit/src/plugin.scala
author wenzelm
Sun Nov 25 21:35:29 2012 +0100 (2012-11-25)
changeset 50208 1382ad6d4774
parent 50207 54be125d8cdc
child 50209 907373a080b9
permissions -rw-r--r--
tuned signature;
     1 /*  Title:      Tools/jEdit/src/plugin.scala
     2     Author:     Makarius
     3 
     4 Main Isabelle/jEdit plugin setup.
     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}
    17 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
    18 import org.gjt.sp.jedit.syntax.{Token => JEditToken, 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 thy_load(): JEdit_Thy_Load =
    39     session.thy_load.asInstanceOf[JEdit_Thy_Load]
    40 
    41   def get_recent_syntax(): Option[Outer_Syntax] =
    42   {
    43     val current_session = session
    44     if (current_session.recent_syntax == Outer_Syntax.empty) None
    45     else Some(current_session.recent_syntax)
    46   }
    47 
    48 
    49   /* document model and view */
    50 
    51   def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
    52   def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area)
    53 
    54   def document_views(buffer: Buffer): List[Document_View] =
    55     for {
    56       text_area <- JEdit_Lib.jedit_text_areas(buffer).toList
    57       doc_view = document_view(text_area)
    58       if doc_view.isDefined
    59     } yield doc_view.get
    60 
    61   def exit_model(buffer: Buffer)
    62   {
    63     JEdit_Lib.swing_buffer_lock(buffer) {
    64       JEdit_Lib.jedit_text_areas(buffer).foreach(Document_View.exit)
    65       Document_Model.exit(buffer)
    66     }
    67   }
    68 
    69   def init_model(buffer: Buffer)
    70   {
    71     JEdit_Lib.swing_buffer_lock(buffer) {
    72       val opt_model =
    73         JEdit_Lib.buffer_node_name(buffer) match {
    74           case Some(node_name) =>
    75             document_model(buffer) match {
    76               case Some(model) if model.name == node_name => Some(model)
    77               case _ => Some(Document_Model.init(session, buffer, node_name))
    78             }
    79           case None => None
    80         }
    81       if (opt_model.isDefined) {
    82         for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) {
    83           if (document_view(text_area).map(_.model) != opt_model)
    84             Document_View.init(opt_model.get, text_area)
    85         }
    86       }
    87     }
    88   }
    89 
    90   def init_view(buffer: Buffer, text_area: JEditTextArea)
    91   {
    92     JEdit_Lib.swing_buffer_lock(buffer) {
    93       document_model(buffer) match {
    94         case Some(model) => Document_View.init(model, text_area)
    95         case None =>
    96       }
    97     }
    98   }
    99 
   100   def exit_view(buffer: Buffer, text_area: JEditTextArea)
   101   {
   102     JEdit_Lib.swing_buffer_lock(buffer) {
   103       Document_View.exit(text_area)
   104     }
   105   }
   106 }
   107 
   108 
   109 class Plugin extends EBPlugin
   110 {
   111   /* theory files */
   112 
   113   private lazy val delay_load =
   114     Swing_Thread.delay_last(PIDE.options.seconds("editor_load_delay"))
   115     {
   116       val view = jEdit.getActiveView()
   117 
   118       val buffers = JEdit_Lib.jedit_buffers().toList
   119       if (buffers.forall(_.isLoaded)) {
   120         def loaded_buffer(name: String): Boolean =
   121           buffers.exists(buffer => JEdit_Lib.buffer_name(buffer) == name)
   122 
   123         val thys =
   124           for (buffer <- buffers; model <- PIDE.document_model(buffer))
   125             yield model.name
   126 
   127         val thy_info = new Thy_Info(PIDE.thy_load)
   128         // FIXME avoid I/O in Swing thread!?!
   129         val files = thy_info.dependencies(true, thys).deps.map(_._1.node).
   130           filter(file => !loaded_buffer(file) && PIDE.thy_load.check_file(view, file))
   131 
   132         if (!files.isEmpty) {
   133           val files_list = new ListView(files.sorted)
   134           for (i <- 0 until files.length)
   135             files_list.selection.indices += i
   136 
   137           val answer =
   138             Library.confirm_dialog(view,
   139               "Auto loading of required files",
   140               JOptionPane.YES_NO_OPTION,
   141               "The following files are required to resolve theory imports.",
   142               "Reload selected files now?",
   143               new ScrollPane(files_list))
   144           if (answer == 0) {
   145             files.foreach(file =>
   146               if (files_list.selection.items.contains(file))
   147                 jEdit.openFile(null: View, file))
   148           }
   149         }
   150       }
   151     }
   152 
   153 
   154   /* session manager */
   155 
   156   private val session_manager = actor {
   157     loop {
   158       react {
   159         case phase: Session.Phase =>
   160           phase match {
   161             case Session.Failed =>
   162               Swing_Thread.later {
   163                 Library.error_dialog(jEdit.getActiveView, "Prover process failure",
   164                     "Isabelle Syslog", Library.scrollable_text(PIDE.session.current_syslog()))
   165               }
   166 
   167             case Session.Ready =>
   168               PIDE.session.global_options.event(Session.Global_Options(PIDE.options.value))
   169               JEdit_Lib.jedit_buffers.foreach(PIDE.init_model)
   170               Swing_Thread.later { delay_load.invoke() }
   171 
   172             case Session.Shutdown =>
   173               JEdit_Lib.jedit_buffers.foreach(PIDE.exit_model)
   174               Swing_Thread.later { delay_load.revoke() }
   175 
   176             case _ =>
   177           }
   178         case bad => java.lang.System.err.println("session_manager: ignoring bad message " + bad)
   179       }
   180     }
   181   }
   182 
   183 
   184   /* main plugin plumbing */
   185 
   186   override def handleMessage(message: EBMessage)
   187   {
   188     Swing_Thread.assert()
   189 
   190     if (PIDE.startup_failure.isDefined && !PIDE.startup_notified) {
   191       message match {
   192         case msg: EditorStarted =>
   193           Library.error_dialog(null, "Isabelle plugin startup failure",
   194             Library.scrollable_text(Exn.message(PIDE.startup_failure.get)),
   195             "Prover IDE inactive!")
   196           PIDE.startup_notified = true
   197         case _ =>
   198       }
   199     }
   200 
   201     if (PIDE.startup_failure.isEmpty) {
   202       message match {
   203         case msg: EditorStarted =>
   204           if (PIDE.options.bool("jedit_auto_start"))
   205             PIDE.session.start(Isabelle_Logic.session_args())
   206 
   207         case msg: BufferUpdate
   208         if msg.getWhat == BufferUpdate.LOADED || msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
   209           if (PIDE.session.is_ready) {
   210             val buffer = msg.getBuffer
   211             if (buffer != null && !buffer.isLoading) PIDE.init_model(buffer)
   212             Swing_Thread.later { delay_load.invoke() }
   213           }
   214 
   215         case msg: EditPaneUpdate
   216         if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
   217             msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
   218             msg.getWhat == EditPaneUpdate.CREATED ||
   219             msg.getWhat == EditPaneUpdate.DESTROYED) =>
   220           val edit_pane = msg.getEditPane
   221           val buffer = edit_pane.getBuffer
   222           val text_area = edit_pane.getTextArea
   223 
   224           if (buffer != null && text_area != null) {
   225             if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
   226                 msg.getWhat == EditPaneUpdate.CREATED) {
   227               if (PIDE.session.is_ready)
   228                 PIDE.init_view(buffer, text_area)
   229             }
   230             else PIDE.exit_view(buffer, text_area)
   231           }
   232 
   233         case msg: PropertiesChanged =>
   234           PIDE.session.global_options.event(Session.Global_Options(PIDE.options.value))
   235 
   236         case _ =>
   237       }
   238     }
   239   }
   240 
   241   override def start()
   242   {
   243     try {
   244       PIDE.plugin = this
   245       Isabelle_System.init()
   246       Isabelle_System.install_fonts()
   247 
   248       val init_options = Options.init()
   249       Swing_Thread.now { PIDE.options.update(init_options)  }
   250 
   251       SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
   252       if (ModeProvider.instance.isInstanceOf[ModeProvider])
   253         ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)
   254 
   255       val content = Isabelle_Logic.session_content(false)
   256       val thy_load = new JEdit_Thy_Load(content.loaded_theories, content.syntax)
   257 
   258       PIDE.session = new Session(thy_load) {
   259         override def output_delay = PIDE.options.seconds("editor_output_delay")
   260         override def reparse_limit = PIDE.options.int("editor_reparse_limit")
   261       }
   262 
   263       PIDE.session.phase_changed += session_manager
   264       PIDE.startup_failure = None
   265     }
   266     catch {
   267       case exn: Throwable =>
   268         PIDE.startup_failure = Some(exn)
   269         PIDE.startup_notified = false
   270     }
   271   }
   272 
   273   override def stop()
   274   {
   275     if (PIDE.startup_failure.isEmpty)
   276       PIDE.options.value.save_prefs()
   277 
   278     PIDE.session.phase_changed -= session_manager
   279     JEdit_Lib.jedit_buffers.foreach(PIDE.exit_model)
   280     PIDE.session.stop()
   281   }
   282 }