# HG changeset patch
# User wenzelm
# Date 1314794381 -7200
# Node ID b625650aa2dbff6a9f5ae14f381025cd1ac65b2c
# Parent  4877c4e184e56eacdd9fd92001bb4bd86d41b450
improved auto loading: selectable file list;

diff -r 4877c4e184e5 -r b625650aa2db src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Tue Aug 30 18:12:48 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Aug 31 14:39:41 2011 +0200
@@ -14,7 +14,7 @@
 import javax.swing.JOptionPane
 
 import scala.collection.mutable
-import scala.swing.ComboBox
+import scala.swing.{ComboBox, ListView, ScrollPane}
 import scala.util.Sorting
 
 import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
@@ -367,20 +367,23 @@
           yield (model.master_dir, model.thy_name)
       val files = thy_info.dependencies(thys).map(_._1).filterNot(loaded_buffer _)
 
-      val do_load = !files.isEmpty &&
-        {
-          val files_sorted = { val a = files.toArray; Sorting.quickSort(a); a.toList }
-          val files_text = new scala.swing.TextArea(files_sorted.mkString("\n"))
-          files_text.editable = false
+      if (!files.isEmpty) {
+        val files_sorted = { val a = files.toArray; Sorting.quickSort(a); a.toList }
+        val files_list = new ListView(files_sorted)
+        for (i <- 0 until files_sorted.length)
+          files_list.selection.indices += i
+
+        val answer =
           Library.confirm_dialog(jEdit.getActiveView(),
             "Auto loading of required files",
             JOptionPane.YES_NO_OPTION,
-            "The following files are required to resolve theory imports.  Reload now?",
-            files_text) == 0
-        }
-      if (do_load)
-        for (file <- files if !loaded_buffer(file))
-          jEdit.openFile(null: View, file)
+            "The following files are required to resolve theory imports.",
+            "Reload selected files now?",
+            new ScrollPane(files_list))
+        if (answer == 0)
+          files_list.selection.items foreach (file =>
+            if (!loaded_buffer(file)) jEdit.openFile(null: View, file))
+      }
     }