# HG changeset patch
# User wenzelm
# Date 1338320885 -7200
# Node ID a4f9957878ab637729dcd2f52226e56717793f99
# Parent  226dee06ab6ec503d93d611f9c985406bd60b285
clarified prover startup: no timeout, read stderr more carefully;

diff -r 226dee06ab6e -r a4f9957878ab src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Tue May 29 21:03:11 2012 +0200
+++ b/src/Pure/System/isabelle_process.scala	Tue May 29 21:48:05 2012 +0200
@@ -77,7 +77,6 @@
 
 
 class Isabelle_Process(
-    timeout: Time = Time.seconds(25),
     receiver: Isabelle_Process.Message => Unit = Console.println(_),
     args: List[String] = Nil)
 {
@@ -155,18 +154,18 @@
   {
     val (startup_failed, startup_errors) =
     {
-      val expired = System.currentTimeMillis() + timeout.ms
+      var finished: Option[Boolean] = None
       val result = new StringBuilder(100)
-
-      var finished: Option[Boolean] = None
-      while (finished.isEmpty && System.currentTimeMillis() <= expired) {
+      while (finished.isEmpty && (process.stderr.ready || !process_result.is_finished)) {
         while (finished.isEmpty && process.stderr.ready) {
-          val c = process.stderr.read
-          if (c == 2) finished = Some(true)
-          else result += c.toChar
+          try {
+            val c = process.stderr.read
+            if (c == 2) finished = Some(true)
+            else result += c.toChar
+          }
+          catch { case _: IOException => finished = Some(false) }
         }
-        if (process_result.is_finished) finished = Some(false)
-        else Thread.sleep(10)
+        Thread.sleep(10)
       }
       (finished.isEmpty || !finished.get, result.toString.trim)
     }
diff -r 226dee06ab6e -r a4f9957878ab src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Tue May 29 21:03:11 2012 +0200
+++ b/src/Pure/System/session.scala	Tue May 29 21:48:05 2012 +0200
@@ -174,7 +174,7 @@
 
   /* actor messages */
 
-  private case class Start(timeout: Time, args: List[String])
+  private case class Start(args: List[String])
   private case object Cancel_Execution
   private case class Edit(edits: List[Document.Edit_Text])
   private case class Change(
@@ -389,10 +389,10 @@
       receiveWithin(delay_commands_changed.flush_timeout) {
         case TIMEOUT => delay_commands_changed.flush()
 
-        case Start(timeout, args) if prover.isEmpty =>
+        case Start(args) if prover.isEmpty =>
           if (phase == Session.Inactive || phase == Session.Failed) {
             phase = Session.Startup
-            prover = Some(new Isabelle_Process(timeout, receiver.invoke _, args) with Protocol)
+            prover = Some(new Isabelle_Process(receiver.invoke _, args) with Protocol)
           }
 
         case Stop =>
@@ -446,10 +446,7 @@
 
   /* actions */
 
-  def start(timeout: Time, args: List[String])
-  { session_actor ! Start(timeout, args) }
-
-  def start(args: List[String]) { start (Time.seconds(25), args) }
+  def start(args: List[String]) { session_actor ! Start(args) }
 
   def stop() { commands_changed_buffer !? Stop; change_parser !? Stop; session_actor !? Stop }
 
diff -r 226dee06ab6e -r a4f9957878ab src/Tools/jEdit/src/Isabelle.props
--- a/src/Tools/jEdit/src/Isabelle.props	Tue May 29 21:03:11 2012 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props	Tue May 29 21:48:05 2012 +0200
@@ -33,7 +33,6 @@
 options.isabelle.tooltip-margin=60
 options.isabelle.tooltip-dismiss-delay.title=Tooltip Dismiss Delay (global)
 options.isabelle.tooltip-dismiss-delay=8.0
-options.isabelle.startup-timeout=25.0
 options.isabelle.auto-start.title=Auto Start
 options.isabelle.auto-start=true
 
diff -r 226dee06ab6e -r a4f9957878ab src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Tue May 29 21:03:11 2012 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Tue May 29 21:48:05 2012 +0200
@@ -295,14 +295,13 @@
 
   def start_session()
   {
-    val timeout = Time_Property("startup-timeout", Time.seconds(25)) max Time.seconds(5)
     val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
     val logic = {
       val logic = Property("logic")
       if (logic != null && logic != "") logic
       else Isabelle.default_logic()
     }
-    session.start(timeout, modes ::: List(logic))
+    session.start(modes ::: List(logic))
   }