src/Pure/PIDE/session.scala
changeset 56782 433cf57550fa
parent 56775 59f70b89e5fd
child 56793 d5ab6a8799ce
     1.1 --- a/src/Pure/PIDE/session.scala	Tue Apr 29 13:29:05 2014 +0200
     1.2 +++ b/src/Pure/PIDE/session.scala	Tue Apr 29 13:32:13 2014 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4            try { c.consume(a) }
     1.5            catch {
     1.6              case exn: Throwable =>
     1.7 -              System.err.println("Consumer failed: " + quote(c.name) + "\n" + Exn.message(exn))
     1.8 +              Output.error_message("Consumer failed: " + quote(c.name) + "\n" + Exn.message(exn))
     1.9            })
    1.10        }
    1.11      }
    1.12 @@ -115,7 +115,7 @@
    1.13        val (handlers1, functions1) =
    1.14          handlers.get(name) match {
    1.15            case Some(old_handler) =>
    1.16 -            System.err.println("Redefining protocol handler: " + name)
    1.17 +            Output.warning("Redefining protocol handler: " + name)
    1.18              old_handler.stop(prover)
    1.19              (handlers - name, functions -- old_handler.functions.keys)
    1.20            case None => (handlers, functions)
    1.21 @@ -135,8 +135,8 @@
    1.22          }
    1.23          catch {
    1.24            case exn: Throwable =>
    1.25 -            System.err.println(Exn.error_message(
    1.26 -              "Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn)))
    1.27 +            Output.error_message(
    1.28 +              "Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn))
    1.29              (handlers1, functions1)
    1.30          }
    1.31  
    1.32 @@ -149,8 +149,8 @@
    1.33            try { functions(a)(msg) }
    1.34            catch {
    1.35              case exn: Throwable =>
    1.36 -              System.err.println(Exn.error_message(
    1.37 -                "Failed invocation of protocol function: " + quote(a) + "\n" + Exn.message(exn)))
    1.38 +              Output.error_message(
    1.39 +                "Failed invocation of protocol function: " + quote(a) + "\n" + Exn.message(exn))
    1.40              false
    1.41            }
    1.42          case _ => false
    1.43 @@ -381,7 +381,7 @@
    1.44                global_state.change(_.define_blob(digest))
    1.45                prover.get.define_blob(digest, blob.bytes)
    1.46              case None =>
    1.47 -              System.err.println("Missing blob for SHA1 digest " + digest)
    1.48 +              Output.error_message("Missing blob for SHA1 digest " + digest)
    1.49            }
    1.50          }
    1.51  
    1.52 @@ -411,7 +411,7 @@
    1.53        def bad_output()
    1.54        {
    1.55          if (verbose)
    1.56 -          System.err.println("Ignoring bad prover output: " + output.message.toString)
    1.57 +          Output.warning("Ignoring bad prover output: " + output.message.toString)
    1.58        }
    1.59  
    1.60        def accumulate(state_id: Document_ID.Generic, message: XML.Elem)