diff options
author | Paul Phillips <paulp@improving.org> | 2010-10-14 05:10:25 +0000 |
---|---|---|
committer | Paul Phillips <paulp@improving.org> | 2010-10-14 05:10:25 +0000 |
commit | 492f5f52141ecd71f2decdbf7eda7aed51dfb64c (patch) | |
tree | 9863f25a0f46261145c2f01b383ecc3350bb18ed /src/library | |
parent | 77c31e39ecd2d160cc27270fc8ef31eaa56e3444 (diff) | |
download | scala-492f5f52141ecd71f2decdbf7eda7aed51dfb64c.tar.gz scala-492f5f52141ecd71f2decdbf7eda7aed51dfb64c.tar.bz2 scala-492f5f52141ecd71f2decdbf7eda7aed51dfb64c.zip |
Fixing issue with XMLEventReader.stop failing t...
Fixing issue with XMLEventReader.stop failing to stop the parser thread.
Contributed by Jean-Laurent Huynh, reviewed by extempore. Closes #3881.
Diffstat (limited to 'src/library')
-rw-r--r--[-rwxr-xr-x] | src/library/scala/xml/pull/XMLEventReader.scala | 16 |
1 files changed, 15 insertions, 1 deletions
diff --git a/src/library/scala/xml/pull/XMLEventReader.scala b/src/library/scala/xml/pull/XMLEventReader.scala index d51202f2d8..100d4fec71 100755..100644 --- a/src/library/scala/xml/pull/XMLEventReader.scala +++ b/src/library/scala/xml/pull/XMLEventReader.scala @@ -52,6 +52,7 @@ class XMLEventReader(src: Source) extends ProducerConsumerIterator[XMLEvent] // or at least as much as it can fit in the queue.) def stop = { produce(POISON) + parser.pause() parserThread.interrupt() } @@ -87,8 +88,21 @@ class XMLEventReader(src: Source) extends ProducerConsumerIterator[XMLEvent] def entityRef(pos: Int, n: String) = setEvent(EvEntityRef(n)) def text(pos: Int, txt:String) = setEvent(EvText(txt)) + // use to make thread sleep on XMLEventReader.stop + @volatile private var pauseRequested = false + // requesting this thread to sleep so that it can be interrupted. + def pause() { pauseRequested = true } + override def run() { - curInput = input + curInput = new Source { + val iter = new Iterator[Char] { + def hasNext = input.hasNext + def next() = { + if (pauseRequested) Thread.sleep(1000) + input.next() + } + } + } interruptibly { this.initialize.document() } setEvent(POISON) } |