src/Tools/jEdit/src/plugin.scala
changeset 44963 4662dddc2fd8
parent 44955 9adaf5cd4f1c
child 45055 55274f7e306b
equal deleted inserted replaced
44962:5554ed48b13f 44963:4662dddc2fd8
   364   /* theory files */
   364   /* theory files */
   365 
   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 view = jEdit.getActiveView()
       
   370 
   369       val buffers = Isabelle.jedit_buffers().toList
   371       val buffers = Isabelle.jedit_buffers().toList
   370       def loaded_buffer(name: String): Boolean =
   372       def loaded_buffer(name: String): Boolean =
   371         buffers.exists(buffer => Isabelle.buffer_name(buffer) == name)
   373         buffers.exists(buffer => Isabelle.buffer_name(buffer) == name)
   372 
   374 
   373       val thys =
   375       val thys =
   374         for (buffer <- buffers; model <- Isabelle.document_model(buffer))
   376         for (buffer <- buffers; model <- Isabelle.document_model(buffer))
   375           yield model.name
   377           yield model.name
   376       val files = Isabelle.thy_info.dependencies(thys).map(_._1.node).filterNot(loaded_buffer _)
   378       val files = Isabelle.thy_info.dependencies(thys).map(_._1.node).
       
   379         filter(file => !loaded_buffer(file) && Isabelle.thy_load.check_file(view, file))
   377 
   380 
   378       if (!files.isEmpty) {
   381       if (!files.isEmpty) {
   379         val files_list = new ListView(Library.sort_strings(files))
   382         val files_list = new ListView(Library.sort_strings(files))
   380         for (i <- 0 until files.length)
   383         for (i <- 0 until files.length)
   381           files_list.selection.indices += i
   384           files_list.selection.indices += i
   382 
   385 
   383         val answer =
   386         val answer =
   384           Library.confirm_dialog(jEdit.getActiveView(),
   387           Library.confirm_dialog(view,
   385             "Auto loading of required files",
   388             "Auto loading of required files",
   386             JOptionPane.YES_NO_OPTION,
   389             JOptionPane.YES_NO_OPTION,
   387             "The following files are required to resolve theory imports.",
   390             "The following files are required to resolve theory imports.",
   388             "Reload selected files now?",
   391             "Reload selected files now?",
   389             new ScrollPane(files_list))
   392             new ScrollPane(files_list))
   390         if (answer == 0)
   393         if (answer == 0)
   391           for {
   394           for {
   392             file <- files
   395             file <- files
   393             if !loaded_buffer(file) && files_list.selection.items.contains(file)
   396             if files_list.selection.items.contains(file)
   394           } jEdit.openFile(null: View, file)
   397           } jEdit.openFile(null: View, file)
   395       }
   398       }
   396     }
   399     }
   397 
   400 
   398 
   401