--- a/src/Pure/System/standard_system.scala Tue Mar 30 00:12:42 2010 +0200
+++ b/src/Pure/System/standard_system.scala Tue Mar 30 00:13:27 2010 +0200
@@ -20,7 +20,7 @@
object Standard_System
{
val charset = "UTF-8"
- val codec = Codec(charset)
+ def codec(): Codec = Codec(charset)
/* permissive UTF-8 decoding */
@@ -136,7 +136,7 @@
def process_output(proc: Process): (String, Int) =
{
proc.getOutputStream.close
- val output = Source.fromInputStream(proc.getInputStream)(codec).mkString // FIXME
+ val output = Source.fromInputStream(proc.getInputStream)(codec()).mkString // FIXME
val rc =
try { proc.waitFor }
finally {
--- a/src/Tools/jEdit/src/jedit/document_model.scala Tue Mar 30 00:12:42 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala Tue Mar 30 00:13:27 2010 +0200
@@ -8,6 +8,8 @@
package isabelle.jedit
+import isabelle._
+
import scala.actors.Actor, Actor._
import scala.collection.mutable
--- a/src/Tools/jEdit/src/jedit/document_view.scala Tue Mar 30 00:12:42 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Tue Mar 30 00:13:27 2010 +0200
@@ -8,6 +8,8 @@
package isabelle.jedit
+import isabelle._
+
import scala.actors.Actor._
import java.awt.event.{MouseAdapter, MouseEvent}
--- a/src/Tools/jEdit/src/jedit/html_panel.scala Tue Mar 30 00:12:42 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/html_panel.scala Tue Mar 30 00:13:27 2010 +0200
@@ -7,6 +7,8 @@
package isabelle.jedit
+import isabelle._
+
import java.io.StringReader
import java.awt.{BorderLayout, Dimension}
import java.awt.event.MouseEvent
--- a/src/Tools/jEdit/src/jedit/isabelle_encoding.scala Tue Mar 30 00:12:42 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_encoding.scala Tue Mar 30 00:13:27 2010 +0200
@@ -7,14 +7,16 @@
package isabelle.jedit
+import isabelle._
+
import org.gjt.sp.jedit.io.Encoding
import org.gjt.sp.jedit.buffer.JEditBuffer
-import java.nio.charset.{Charset, CharsetDecoder, CodingErrorAction}
+import java.nio.charset.{Charset, CodingErrorAction}
import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter,
CharArrayReader, ByteArrayOutputStream}
-import scala.io.{Source, BufferedSource}
+import scala.io.{Codec, Source, BufferedSource}
object Isabelle_Encoding
@@ -28,24 +30,23 @@
class Isabelle_Encoding extends Encoding
{
private val charset = Charset.forName(Standard_System.charset)
- private val BUFSIZE = 32768
+ val BUFSIZE = 32768
- private def text_reader(in: InputStream, decoder: CharsetDecoder): Reader =
+ private def text_reader(in: InputStream, codec: Codec): Reader =
{
- def source(): Source =
- BufferedSource.fromInputStream(in, decoder, BUFSIZE, { () => source() })
+ val source = new BufferedSource(in)(codec)
new CharArrayReader(Isabelle.system.symbols.decode(source.mkString).toArray)
}
override def getTextReader(in: InputStream): Reader =
- text_reader(in, charset.newDecoder())
+ text_reader(in, Standard_System.codec())
override def getPermissiveTextReader(in: InputStream): Reader =
{
- val decoder = charset.newDecoder()
- decoder.onMalformedInput(CodingErrorAction.REPLACE)
- decoder.onUnmappableCharacter(CodingErrorAction.REPLACE)
- text_reader(in, decoder)
+ val codec = Standard_System.codec()
+ codec.onMalformedInput(CodingErrorAction.REPLACE)
+ codec.onUnmappableCharacter(CodingErrorAction.REPLACE)
+ text_reader(in, codec)
}
override def getTextWriter(out: OutputStream): Writer =
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Tue Mar 30 00:12:42 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Tue Mar 30 00:13:27 2010 +0200
@@ -7,6 +7,8 @@
package isabelle.jedit
+import isabelle._
+
import java.io.File
import gatchan.jedit.hyperlinks.{Hyperlink, HyperlinkSource, AbstractHyperlink}
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Tue Mar 30 00:12:42 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Tue Mar 30 00:13:27 2010 +0200
@@ -8,6 +8,8 @@
package isabelle.jedit
+import isabelle._
+
import scala.collection.Set
import scala.collection.immutable.TreeSet
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala Tue Mar 30 00:12:42 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Tue Mar 30 00:13:27 2010 +0200
@@ -7,6 +7,8 @@
package isabelle.jedit
+import isabelle._
+
import scala.actors.Actor._
import javax.swing.JPanel
--- a/src/Tools/jEdit/src/jedit/plugin.scala Tue Mar 30 00:12:42 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala Tue Mar 30 00:13:27 2010 +0200
@@ -9,6 +9,8 @@
package isabelle.jedit
+import isabelle._
+
import java.io.{FileInputStream, IOException}
import java.awt.Font
import javax.swing.JTextArea
--- a/src/Tools/jEdit/src/jedit/protocol_dockable.scala Tue Mar 30 00:12:42 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/protocol_dockable.scala Tue Mar 30 00:13:27 2010 +0200
@@ -7,6 +7,8 @@
package isabelle.jedit
+import isabelle._
+
import scala.actors.Actor._
import java.awt.{Dimension, Graphics, BorderLayout}
--- a/src/Tools/jEdit/src/jedit/scala_console.scala Tue Mar 30 00:12:42 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/scala_console.scala Tue Mar 30 00:13:27 2010 +0200
@@ -7,6 +7,8 @@
package isabelle.jedit
+import isabelle._
+
import console.{Console, ConsolePane, Shell, Output}
import org.gjt.sp.jedit.{jEdit, JARClassLoader}
@@ -63,7 +65,7 @@
def write(cbuf: Array[Char], off: Int, len: Int)
{
- if (len > 0) write(new String(cbuf.subArray(off, off + len)))
+ if (len > 0) write(new String(cbuf.slice(off, off + len)))
}
override def write(str: String)