src/Tools/jEdit/src/plugin.scala
changeset 44954 b536b1144eb3
parent 44864 e50557cb0eb6
child 44955 9adaf5cd4f1c
equal deleted inserted replaced
44953:cdfe42f1267c 44954:b536b1144eb3
   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).toList.map(_._1.node).filterNot(loaded_buffer _)
   376       val files = 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
   386             JOptionPane.YES_NO_OPTION,
   386             JOptionPane.YES_NO_OPTION,
   387             "The following files are required to resolve theory imports.",
   387             "The following files are required to resolve theory imports.",
   388             "Reload selected files now?",
   388             "Reload selected files now?",
   389             new ScrollPane(files_list))
   389             new ScrollPane(files_list))
   390         if (answer == 0)
   390         if (answer == 0)
   391           files_list.selection.items foreach (file =>
   391           for {
   392             if (!loaded_buffer(file)) jEdit.openFile(null: View, file))
   392             file <- files
       
   393             if !loaded_buffer(file) && files_list.selection.items.contains(file)
       
   394           } jEdit.openFile(null: View, file)
   393       }
   395       }
   394     }
   396     }
   395 
   397 
   396 
   398 
   397   /* session manager */
   399   /* session manager */