src/Tools/jEdit/src/main_plugin.scala

   ViewUpdate}
 import org.gjt.sp.util.SyntaxUtilities
 import org.gjt.sp.util.Log
 
 
-object PIDE
-{
+object PIDE {
   /* semantic document content */
 
-  def maybe_snapshot(view: View = null): Option[Document.Snapshot] = GUI_Thread.now
-  {
+  def maybe_snapshot(view: View = null): Option[Document.Snapshot] = GUI_Thread.now {
     val buffer = JEdit_Lib.jedit_view(view).getBuffer
     Document_Model.get(buffer).map(_.snapshot())
   }
 
-  def maybe_rendering(view: View = null): Option[JEdit_Rendering] = GUI_Thread.now
-  {
+  def maybe_rendering(view: View = null): Option[JEdit_Rendering] = GUI_Thread.now {
     val text_area = JEdit_Lib.jedit_view(view).getTextArea
     Document_View.get(text_area).map(_.get_rendering())
   }
 
   def snapshot(view: View = null): Document.Snapshot =

   def session: Session = plugin.session
 
   object editor extends JEdit_Editor
 }
 
-class Main_Plugin extends EBPlugin
-{
+class Main_Plugin extends EBPlugin {
   /* options */
 
   private var _options: JEdit_Options = null
   private def init_options(): Unit =
     _options = new JEdit_Options(Options.init())

   val spell_checker = new Spell_Checker_Variable
 
 
   /* global changes */
 
-  def options_changed(): Unit =
-  {
+  def options_changed(): Unit = {
     session.global_options.post(Session.Global_Options(options.value))
     delay_load.invoke()
   }
 
-  def deps_changed(): Unit =
-  {
+  def deps_changed(): Unit = {
     delay_load.invoke()
   }
 
 
   /* theory files */
 
   lazy val delay_init: Delay =
-    Delay.last(options.seconds("editor_load_delay"), gui = true)
-    {
+    Delay.last(options.seconds("editor_load_delay"), gui = true) {
       init_models()
     }
 
   private val delay_load_active = Synchronized(false)
   private def delay_load_activated(): Boolean =
     delay_load_active.guarded_access(a => Some((!a, true)))
-  private def delay_load_action(): Unit =
-  {
+  private def delay_load_action(): Unit = {
     if (Isabelle.continuous_checking && delay_load_activated() &&
-        PerspectiveManager.isPerspectiveEnabled)
-    {
+        PerspectiveManager.isPerspectiveEnabled) {
       if (JEdit_Lib.jedit_buffers().exists(_.isLoading)) delay_load.invoke()
       else {
-        val required_files =
-        {
+        val required_files = {
           val models = Document_Model.get_models()
 
           val thys =
             (for ((node_name, model) <- models.iterator if model.is_theory)
               yield (node_name, Position.none)).toList

     File_Watcher(file_watcher_action, options.seconds("editor_load_delay"))
 
 
   /* session phase */
 
-  val session_phase_changed: Session.Consumer[Session.Phase] = Session.Consumer("Isabelle/jEdit")
-  {
+  val session_phase_changed: Session.Consumer[Session.Phase] = Session.Consumer("Isabelle/jEdit") {
     case Session.Terminated(result) if !result.ok =>
       GUI_Thread.later {
         GUI.error_dialog(jEdit.getActiveView, "Prover process terminated with error",
           "Isabelle Syslog", GUI.scrollable_text(session.syslog_content()))
       }

   }
 
 
   /* document model and view */
 
-  def exit_models(buffers: List[Buffer]): Unit =
-  {
+  def exit_models(buffers: List[Buffer]): Unit = {
     GUI_Thread.now {
       buffers.foreach(buffer =>
         JEdit_Lib.buffer_lock(buffer) {
           JEdit_Lib.jedit_text_areas(buffer).foreach(Document_View.exit)
           Document_Model.exit(buffer)
         })
       }
   }
 
-  def init_models(): Unit =
-  {
+  def init_models(): Unit = {
     GUI_Thread.now {
       PIDE.editor.flush()
 
       for {
         buffer <- JEdit_Lib.jedit_buffers()

   /* main plugin plumbing */
 
   @volatile private var startup_failure: Option[Throwable] = None
   @volatile private var startup_notified = false
 
-  private def init_editor(view: View): Unit =
-  {
+  private def init_editor(view: View): Unit = {
     Keymap_Merge.check_dialog(view)
     Session_Build.check_dialog(view)
   }
 
-  private def init_title(view: View): Unit =
-  {
+  private def init_title(view: View): Unit = {
     val title =
       proper_string(Isabelle_System.getenv("ISABELLE_IDENTIFIER")).getOrElse("Isabelle") +
         "/" + PIDE.resources.session_name
     val marker = "\u200B"
 

     if (old_title == null || old_title.startsWith(marker)) {
       view.setUserTitle(marker + title)
     }
   }
 
-  override def handleMessage(message: EBMessage): Unit =
-  {
+  override def handleMessage(message: EBMessage): Unit = {
     GUI_Thread.assert {}
 
     if (startup_failure.isDefined && !startup_notified) {
       message match {
         case msg: EditorStarted =>

   /* mode provider */
 
   private var orig_mode_provider: ModeProvider = null
   private var pide_mode_provider: ModeProvider = null
 
-  def init_mode_provider(): Unit =
-  {
+  def init_mode_provider(): Unit = {
     orig_mode_provider = ModeProvider.instance
     if (orig_mode_provider.isInstanceOf[ModeProvider]) {
       pide_mode_provider = new Token_Markup.Mode_Provider(orig_mode_provider)
       ModeProvider.instance = pide_mode_provider
     }
   }
 
-  def exit_mode_provider(): Unit =
-  {
+  def exit_mode_provider(): Unit = {
     if (ModeProvider.instance == pide_mode_provider)
       ModeProvider.instance = orig_mode_provider
   }
 
 

 
   /* start and stop */
 
   private val shutting_down = Synchronized(false)
 
-  override def start(): Unit =
-  {
+  override def start(): Unit = {
     /* strict initialization */
 
     init_options()
     init_resources()
     init_session()

 
     val view = jEdit.getActiveView()
     if (view != null) init_editor(view)
   }
 
-  override def stop(): Unit =
-  {
+  override def stop(): Unit = {
     http_server.stop()
 
     Syntax_Style.set_extender(Syntax_Style.Base_Extender)
 
     exit_mode_provider()