# HG changeset patch
# User wenzelm
# Date 1269900807 -7200
# Node ID 6111de7c916a157e2c4af7e8bd6af10cb22be458
# Parent  c51a077680e496f3697b0a9af8bbb62e9b97cc83
adapted to Scala 2.8.0 Beta 1;

diff -r c51a077680e4 -r 6111de7c916a src/Pure/System/standard_system.scala
--- 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 {
diff -r c51a077680e4 -r 6111de7c916a src/Tools/jEdit/src/jedit/document_model.scala
--- 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
 
diff -r c51a077680e4 -r 6111de7c916a src/Tools/jEdit/src/jedit/document_view.scala
--- 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}
diff -r c51a077680e4 -r 6111de7c916a src/Tools/jEdit/src/jedit/html_panel.scala
--- 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
diff -r c51a077680e4 -r 6111de7c916a src/Tools/jEdit/src/jedit/isabelle_encoding.scala
--- 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 =
diff -r c51a077680e4 -r 6111de7c916a src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
--- 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}
diff -r c51a077680e4 -r 6111de7c916a src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- 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
 
diff -r c51a077680e4 -r 6111de7c916a src/Tools/jEdit/src/jedit/output_dockable.scala
--- 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
diff -r c51a077680e4 -r 6111de7c916a src/Tools/jEdit/src/jedit/plugin.scala
--- 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
diff -r c51a077680e4 -r 6111de7c916a src/Tools/jEdit/src/jedit/protocol_dockable.scala
--- 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}
diff -r c51a077680e4 -r 6111de7c916a src/Tools/jEdit/src/jedit/scala_console.scala
--- 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)