merged

--- a/src/Pure/System/isabelle_process.scala	Fri Mar 02 18:26:54 2012 +0100
+++ b/src/Pure/System/isabelle_process.scala	Fri Mar 02 22:57:57 2012 +0100
@@ -234,7 +234,9 @@
           }
           //}}}
         }
-        catch { case e: IOException => system_result(name + ": " + e.getMessage) }
+        catch {
+          case e: IOException => finished = true; system_result(name + ": " + e.getMessage)
+        }
       }
       system_result(name + " terminated")
     }
@@ -273,7 +275,9 @@
           }
           //}}}
         }
-        catch { case e: IOException => system_result(name + ": " + e.getMessage) }
+        catch {
+          case e: IOException => finished; system_result(name + ": " + e.getMessage)
+        }
       }
       system_result(name + " terminated")
     }
@@ -304,7 +308,9 @@
           }
           //}}}
         }
-        catch { case e: IOException => system_result(name + ": " + e.getMessage) }
+        catch {
+          case e: IOException => finished; system_result(name + ": " + e.getMessage)
+        }
       }
       system_result(name + " terminated")
     }
@@ -371,8 +377,8 @@
           }
         }
         catch {
-          case e: IOException => system_result("Cannot read message:\n" + e.getMessage)
-          case e: Protocol_Error => system_result("Malformed message:\n" + e.getMessage)
+          case e: IOException => c = -1; system_result("Cannot read message:\n" + e.getMessage)
+          case e: Protocol_Error => c = -1; system_result("Malformed message:\n" + e.getMessage)
           case _: EOF =>
         }
       } while (c != -1)

--- a/src/Tools/jEdit/src/plugin.scala	Fri Mar 02 18:26:54 2012 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Fri Mar 02 22:57:57 2012 +0100
@@ -344,32 +344,36 @@
       val view = jEdit.getActiveView()
 
       val buffers = Isabelle.jedit_buffers().toList
-      def loaded_buffer(name: String): Boolean =
-        buffers.exists(buffer => Isabelle.buffer_name(buffer) == name)
+      if (buffers.forall(_.isLoaded)) {
+        def loaded_buffer(name: String): Boolean =
+          buffers.exists(buffer => Isabelle.buffer_name(buffer) == name)
 
-      val thys =
-        for (buffer <- buffers; model <- Isabelle.document_model(buffer))
-          yield model.name
-      val files = Isabelle.thy_info.dependencies(thys).map(_._1.node).
-        filter(file => !loaded_buffer(file) && Isabelle.thy_load.check_file(view, file))
+        val thys =
+          for (buffer <- buffers; model <- Isabelle.document_model(buffer))
+            yield model.name
+
+        // FIXME avoid I/O in Swing thread!?!
+        val files = Isabelle.thy_info.dependencies(thys).map(_._1.node).
+          filter(file => !loaded_buffer(file) && Isabelle.thy_load.check_file(view, file))
 
-      if (!files.isEmpty) {
-        val files_list = new ListView(files.sorted)
-        for (i <- 0 until files.length)
-          files_list.selection.indices += i
+        if (!files.isEmpty) {
+          val files_list = new ListView(files.sorted)
+          for (i <- 0 until files.length)
+            files_list.selection.indices += i
 
-        val answer =
-          Library.confirm_dialog(view,
-            "Auto loading of required files",
-            JOptionPane.YES_NO_OPTION,
-            "The following files are required to resolve theory imports.",
-            "Reload selected files now?",
-            new ScrollPane(files_list))
-        if (answer == 0)
-          for {
-            file <- files
-            if files_list.selection.items.contains(file)
-          } jEdit.openFile(null: View, file)
+          val answer =
+            Library.confirm_dialog(view,
+              "Auto loading of required files",
+              JOptionPane.YES_NO_OPTION,
+              "The following files are required to resolve theory imports.",
+              "Reload selected files now?",
+              new ScrollPane(files_list))
+          if (answer == 0) {
+            files.foreach(file =>
+              if (files_list.selection.items.contains(file))
+                jEdit.openFile(null: View, file))
+          }
+        }
       }
     }