src/Tools/jEdit/src/plugin.scala
changeset 44955 9adaf5cd4f1c
parent 44954 b536b1144eb3
child 44963 4662dddc2fd8
equal deleted inserted replaced
44954:b536b1144eb3 44955:9adaf5cd4f1c
    34 {
    34 {
    35   /* plugin instance */
    35   /* plugin instance */
    36 
    36 
    37   var plugin: Plugin = null
    37   var plugin: Plugin = null
    38   var session: Session = null
    38   var session: Session = null
       
    39 
       
    40   val thy_load = new JEdit_Thy_Load
       
    41   val thy_info = new Thy_Info(thy_load)
    39 
    42 
    40 
    43 
    41   /* properties */
    44   /* properties */
    42 
    45 
    43   val OPTION_PREFIX = "options.isabelle."
    46   val OPTION_PREFIX = "options.isabelle."
   358 
   361 
   359 class Plugin extends EBPlugin
   362 class Plugin extends EBPlugin
   360 {
   363 {
   361   /* theory files */
   364   /* theory files */
   362 
   365 
   363   val thy_load = new JEdit_Thy_Load
       
   364   val thy_info = new Thy_Info(thy_load)
       
   365 
       
   366   private lazy val delay_load =
   366   private lazy val delay_load =
   367     Swing_Thread.delay_last(Isabelle.session.load_delay)
   367     Swing_Thread.delay_last(Isabelle.session.load_delay)
   368     {
   368     {
   369       val buffers = Isabelle.jedit_buffers().toList
   369       val buffers = Isabelle.jedit_buffers().toList
   370       def loaded_buffer(name: String): Boolean =
   370       def loaded_buffer(name: String): Boolean =
   371         buffers.exists(buffer => Isabelle.buffer_name(buffer) == name)
   371         buffers.exists(buffer => Isabelle.buffer_name(buffer) == name)
   372 
   372 
   373       val thys =
   373       val thys =
   374         for (buffer <- buffers; model <- Isabelle.document_model(buffer))
   374         for (buffer <- buffers; model <- Isabelle.document_model(buffer))
   375           yield model.name
   375           yield model.name
   376       val files = thy_info.dependencies(thys).map(_._1.node).filterNot(loaded_buffer _)
   376       val files = Isabelle.thy_info.dependencies(thys).map(_._1.node).filterNot(loaded_buffer _)
   377 
   377 
   378       if (!files.isEmpty) {
   378       if (!files.isEmpty) {
   379         val files_list = new ListView(Library.sort_strings(files))
   379         val files_list = new ListView(Library.sort_strings(files))
   380         for (i <- 0 until files.length)
   380         for (i <- 0 until files.length)
   381           files_list.selection.indices += i
   381           files_list.selection.indices += i
   472   {
   472   {
   473     Isabelle.plugin = this
   473     Isabelle.plugin = this
   474     Isabelle.setup_tooltips()
   474     Isabelle.setup_tooltips()
   475     Isabelle_System.init()
   475     Isabelle_System.init()
   476     Isabelle_System.install_fonts()
   476     Isabelle_System.install_fonts()
   477     Isabelle.session = new Session(thy_load)
   477     Isabelle.session = new Session(Isabelle.thy_load)
   478     SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
   478     SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
   479     if (ModeProvider.instance.isInstanceOf[ModeProvider])
   479     if (ModeProvider.instance.isInstanceOf[ModeProvider])
   480       ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)
   480       ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)
   481     Isabelle.session.phase_changed += session_manager
   481     Isabelle.session.phase_changed += session_manager
   482   }
   482   }