src/Tools/jEdit/src/plugin.scala
changeset 53274 1760c01f1c78
parent 53272 0dfd78ff7696
child 53277 6aa348237973
equal deleted inserted replaced
53273:473ea1ed7503 53274:1760c01f1c78
    57 
    57 
    58   def dismissed_popups(view: View): Boolean =
    58   def dismissed_popups(view: View): Boolean =
    59   {
    59   {
    60     var dismissed = false
    60     var dismissed = false
    61 
    61 
    62     for {
    62     JEdit_Lib.jedit_text_areas(view).foreach(text_area =>
    63       text_area <- JEdit_Lib.jedit_text_areas(view)
    63       if (Completion_Popup.Text_Area.dismissed(text_area)) dismissed = true)
    64       doc_view <- document_view(text_area)
       
    65     } { if (doc_view.dismissed_popups()) dismissed = true }
       
    66 
    64 
    67     if (Pretty_Tooltip.dismissed_all()) dismissed = true
    65     if (Pretty_Tooltip.dismissed_all()) dismissed = true
    68 
    66 
    69     dismissed
    67     dismissed
    70   }
    68   }
    71 
    69 
    72 
    70 
    73   /* document model and view */
    71   /* document model and view */
    74 
    72 
    75   def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
    73   def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
       
    74 
    76   def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area)
    75   def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area)
    77 
    76 
    78   def document_views(buffer: Buffer): List[Document_View] =
    77   def document_views(buffer: Buffer): List[Document_View] =
    79     for {
    78     for {
    80       text_area <- JEdit_Lib.jedit_text_areas(buffer).toList
    79       text_area <- JEdit_Lib.jedit_text_areas(buffer).toList
   283             }
   282             }
   284             else {
   283             else {
   285               PIDE.dismissed_popups(text_area.getView)
   284               PIDE.dismissed_popups(text_area.getView)
   286               PIDE.exit_view(buffer, text_area)
   285               PIDE.exit_view(buffer, text_area)
   287             }
   286             }
       
   287 
       
   288             if (msg.getWhat == EditPaneUpdate.CREATED)
       
   289               Completion_Popup.Text_Area.init(text_area)
       
   290 
       
   291             if (msg.getWhat == EditPaneUpdate.DESTROYED)
       
   292               Completion_Popup.Text_Area.exit(text_area)
   288           }
   293           }
   289 
   294 
   290         case msg: PropertiesChanged =>
   295         case msg: PropertiesChanged =>
   291           PIDE.session.update_options(PIDE.options.value)
   296           PIDE.session.update_options(PIDE.options.value)
   292 
   297 
   311         OSX_Adapter.set_quit_handler(this, this.getClass.getDeclaredMethod("handle_quit"))
   316         OSX_Adapter.set_quit_handler(this, this.getClass.getDeclaredMethod("handle_quit"))
   312 
   317 
   313       SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
   318       SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
   314       if (ModeProvider.instance.isInstanceOf[ModeProvider])
   319       if (ModeProvider.instance.isInstanceOf[ModeProvider])
   315         ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)
   320         ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)
       
   321 
       
   322       JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)
   316 
   323 
   317       val content = Isabelle_Logic.session_content(false)
   324       val content = Isabelle_Logic.session_content(false)
   318       val thy_load = new JEdit_Thy_Load(content.loaded_theories, content.syntax)
   325       val thy_load = new JEdit_Thy_Load(content.loaded_theories, content.syntax)
   319 
   326 
   320       PIDE.session = new Session(thy_load) {
   327       PIDE.session = new Session(thy_load) {
   332     }
   339     }
   333   }
   340   }
   334 
   341 
   335   override def stop()
   342   override def stop()
   336   {
   343   {
       
   344     JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.exit _)
       
   345 
   337     if (PIDE.startup_failure.isEmpty)
   346     if (PIDE.startup_failure.isEmpty)
   338       PIDE.options.value.save_prefs()
   347       PIDE.options.value.save_prefs()
   339 
   348 
   340     PIDE.session.phase_changed -= session_manager
   349     PIDE.session.phase_changed -= session_manager
   341     PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
   350     PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)