src/Pure/System/isabelle_process.scala
changeset 38445 ba9ea6b9b75c
parent 38372 e753f71b6b34
child 38446 9d59dab38fef
     1.1 --- a/src/Pure/System/isabelle_process.scala	Mon Aug 16 16:24:22 2010 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.scala	Mon Aug 16 17:04:22 2010 +0200
     1.3 @@ -288,26 +288,14 @@
     1.4  
     1.5        do {
     1.6          try {
     1.7 -          //{{{
     1.8 -          c = stream.read
     1.9 -          var non_sync = 0
    1.10 -          while (c >= 0 && c != 2) {
    1.11 -            non_sync += 1
    1.12 -            c = stream.read
    1.13 +          val header = read_chunk()
    1.14 +          val body = read_chunk()
    1.15 +          header match {
    1.16 +            case List(XML.Elem(Markup(name, props), Nil))
    1.17 +                if name.size == 1 && Kind.markup.isDefinedAt(name(0)) =>
    1.18 +              put_result(Kind.markup(name(0)), props, body)
    1.19 +            case _ => throw new Protocol_Error("bad header: " + header.toString)
    1.20            }
    1.21 -          if (non_sync > 0)
    1.22 -            throw new Protocol_Error("lost synchronization -- skipping " + non_sync + " bytes")
    1.23 -          if (c == 2) {
    1.24 -            val header = read_chunk()
    1.25 -            val body = read_chunk()
    1.26 -            header match {
    1.27 -              case List(XML.Elem(Markup(name, props), Nil))
    1.28 -                  if name.size == 1 && Kind.markup.isDefinedAt(name(0)) =>
    1.29 -                put_result(Kind.markup(name(0)), props, body)
    1.30 -              case _ => throw new Protocol_Error("bad header: " + header.toString)
    1.31 -            }
    1.32 -          }
    1.33 -          //}}}
    1.34          }
    1.35          catch {
    1.36            case e: IOException =>