# HG changeset patch # User wenzelm # Date 1330725477 -3600 # Node ID 4269ae06afc50d9f8f556f6ce49b84289f59a64b # Parent 07f9eda810b3b716c5ae64dc1343a013796ca0b3# Parent d52a4f2eeb7487c711accca93c2b01c211b572ec merged diff -r 07f9eda810b3 -r 4269ae06afc5 src/Pure/System/isabelle_process.scala --- 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) diff -r 07f9eda810b3 -r 4269ae06afc5 src/Tools/jEdit/src/plugin.scala --- 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)) + } + } } }