more explicit treatment of return code vs. session phase;
authorwenzelm
Tue May 29 18:00:54 2012 +0200 (2012-05-29 ago)
changeset 48016edbc8e8accd9
parent 48015 878de88db080
child 48017 9f7b27635b57
more explicit treatment of return code vs. session phase;
src/Pure/PIDE/isabelle_markup.scala
src/Pure/System/isabelle_process.scala
src/Pure/System/session.scala
     1.1 --- a/src/Pure/PIDE/isabelle_markup.scala	Tue May 29 17:54:34 2012 +0200
     1.2 +++ b/src/Pure/PIDE/isabelle_markup.scala	Tue May 29 18:00:54 2012 +0200
     1.3 @@ -236,6 +236,8 @@
     1.4    val STDERR = "stderr"
     1.5    val EXIT = "exit"
     1.6  
     1.7 +  val Return_Code = new Properties.Int("return_code")
     1.8 +
     1.9    val LEGACY = "legacy"
    1.10  
    1.11    val NO_REPORT = "no_report"
     2.1 --- a/src/Pure/System/isabelle_process.scala	Tue May 29 17:54:34 2012 +0200
     2.2 +++ b/src/Pure/System/isabelle_process.scala	Tue May 29 18:00:54 2012 +0200
     2.3 @@ -104,9 +104,10 @@
     2.4      }
     2.5    }
     2.6  
     2.7 -  private def output_message(kind: String, text: String)
     2.8 +  private def exit_message(rc: Int)
     2.9    {
    2.10 -    output_message(kind, Nil, List(XML.Text(Symbol.decode(text))))
    2.11 +    output_message(Isabelle_Markup.EXIT, Isabelle_Markup.Return_Code(rc),
    2.12 +      List(XML.Text("Return code: " + rc.toString)))
    2.13    }
    2.14  
    2.15  
    2.16 @@ -172,7 +173,7 @@
    2.17      if (startup_errors != "") system_output(startup_errors)
    2.18  
    2.19      if (startup_failed) {
    2.20 -      output_message(Isabelle_Markup.EXIT, "Return code: 127")
    2.21 +      exit_message(127)
    2.22        process.stdin.close
    2.23        Thread.sleep(300)
    2.24        terminate_process()
    2.25 @@ -192,7 +193,7 @@
    2.26        for ((thread, _) <- List(standard_input, stdout, stderr, command_input, message))
    2.27          thread.join
    2.28        system_output("process_manager terminated")
    2.29 -      output_message(Isabelle_Markup.EXIT, "Return code: " + rc.toString)
    2.30 +      exit_message(rc)
    2.31      }
    2.32      system_channel.accepted()
    2.33    }
    2.34 @@ -263,7 +264,7 @@
    2.35              else done = true
    2.36            }
    2.37            if (result.length > 0) {
    2.38 -            output_message(markup, result.toString)
    2.39 +            output_message(markup, Nil, List(XML.Text(Symbol.decode(result.toString))))
    2.40              result.length = 0
    2.41            }
    2.42            else {
     3.1 --- a/src/Pure/System/session.scala	Tue May 29 17:54:34 2012 +0200
     3.2 +++ b/src/Pure/System/session.scala	Tue May 29 18:00:54 2012 +0200
     3.3 @@ -369,10 +369,12 @@
     3.4          case Isabelle_Markup.Keyword_Decl(name) if output.is_protocol =>
     3.5            prover_syntax += name
     3.6  
     3.7 +        case Isabelle_Markup.Return_Code(rc) if output.is_exit =>
     3.8 +          if (rc == 0) phase = Session.Inactive
     3.9 +          else phase = Session.Failed
    3.10 +
    3.11          case _ =>
    3.12 -          if (output.is_exit && phase == Session.Startup) phase = Session.Failed
    3.13 -          else if (output.is_exit) phase = Session.Inactive
    3.14 -          else if (output.is_init || output.is_stdout) { }
    3.15 +          if (output.is_init || output.is_stdout) { }
    3.16            else bad_output(output)
    3.17        }
    3.18      }