# HG changeset patch
# User huffman
# Date 1308848915 25200
# Node ID d6791dc3534d204979c883d3b14b35d7c6f50ff8
# Parent  15df7bc8e93fa8b76328e783b08c7f971a7d8ab2# Parent  50d1d8fba81169114e2fb762b2ca2199c24628b3
merged

diff -r 15df7bc8e93f -r d6791dc3534d Admin/build
--- a/Admin/build	Thu Jun 23 10:07:16 2011 -0700
+++ b/Admin/build	Thu Jun 23 10:08:35 2011 -0700
@@ -84,6 +84,7 @@
 
 function build_jars ()
 {
+  "$ISABELLE_HOME/lib/scripts/java_ext_dirs" >/dev/null
   pushd "$ISABELLE_HOME/src/Pure" >/dev/null
   "$ISABELLE_TOOL" env ./build-jars "$@" || exit $?
   popd >/dev/null
diff -r 15df7bc8e93f -r d6791dc3534d Isabelle
--- a/Isabelle	Thu Jun 23 10:07:16 2011 -0700
+++ b/Isabelle	Thu Jun 23 10:08:35 2011 -0700
@@ -26,4 +26,4 @@
 CLASSPATH="$(jvmpath "$CLASSPATH")"
 exec "$ISABELLE_TOOL" java \
   "-Disabelle.home=$(jvmpath "$ISABELLE_HOME")" \
-  -jar "$(jvmpath "$ISABELLE_HOME/lib/classes/isabelle-scala.jar")" "$@"
+  isabelle.GUI_Setup "$@"
diff -r 15df7bc8e93f -r d6791dc3534d etc/settings
--- a/etc/settings	Thu Jun 23 10:07:16 2011 -0700
+++ b/etc/settings	Thu Jun 23 10:08:35 2011 -0700
@@ -62,8 +62,6 @@
   ISABELLE_JAVA="java"
 fi
 
-classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
-
 
 ###
 ### Interactive sessions (cf. isabelle tty)
diff -r 15df7bc8e93f -r d6791dc3534d lib/Tools/java
--- a/lib/Tools/java	Thu Jun 23 10:07:16 2011 -0700
+++ b/lib/Tools/java	Thu Jun 23 10:08:35 2011 -0700
@@ -7,10 +7,13 @@
 CLASSPATH="$(jvmpath "$CLASSPATH")"
 
 JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}"
-if "$JAVA_EXE" -server >/dev/null 2>/dev/null
-then
-  exec "$JAVA_EXE" -Dfile.encoding=UTF-8 -server "$@"
+
+if "$JAVA_EXE" -server >/dev/null 2>/dev/null; then
+  SERVER="-server"
 else
-  exec "$JAVA_EXE" -Dfile.encoding=UTF-8 "$@"
+  SERVER=""
 fi
 
+exec "$JAVA_EXE" -Dfile.encoding=UTF-8 $SERVER \
+  "-Djava.ext.dirs=$("$ISABELLE_HOME/lib/scripts/java_ext_dirs")" "$@"
+
diff -r 15df7bc8e93f -r d6791dc3534d lib/Tools/scala
--- a/lib/Tools/scala	Thu Jun 23 10:07:16 2011 -0700
+++ b/lib/Tools/scala	Thu Jun 23 10:08:35 2011 -0700
@@ -9,4 +9,5 @@
 [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
 
 CLASSPATH="$(jvmpath "$CLASSPATH")"
-exec "$SCALA_HOME/bin/scala" -Dfile.encoding=UTF-8 "$@"
+exec "$SCALA_HOME/bin/scala" -Dfile.encoding=UTF-8 \
+  "-Djava.ext.dirs=$("$ISABELLE_HOME/lib/scripts/java_ext_dirs")" "$@"
diff -r 15df7bc8e93f -r d6791dc3534d lib/scripts/getsettings
--- a/lib/scripts/getsettings	Thu Jun 23 10:07:16 2011 -0700
+++ b/lib/scripts/getsettings	Thu Jun 23 10:08:35 2011 -0700
@@ -60,6 +60,7 @@
   THIS_CYGWIN="$(jvmpath "/")"
 else
   function jvmpath() { echo "$@"; }
+  CLASSPATH="$CLASSPATH"
 fi
 HOME_JVM="$HOME"
 
diff -r 15df7bc8e93f -r d6791dc3534d lib/scripts/java_ext_dirs
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/java_ext_dirs	Thu Jun 23 10:08:35 2011 -0700
@@ -0,0 +1,41 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# Augment Java extension directories.
+
+## diagnostics
+
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+
+## dependencies
+
+SOURCE="$ISABELLE_HOME/src/Pure/System/Java_Ext_Dirs.java"
+
+TARGET_DIR="$ISABELLE_HOME/lib/classes"
+TARGET="$TARGET_DIR/java_ext_dirs.jar"
+
+if [ ! -e "$TARGET" -o "$SOURCE" -nt "$TARGET" ]; then
+  mkdir -p "$TARGET_DIR" || fail "Bad directory: \"$TARGET_DIR\""
+  pushd "$TARGET_DIR" >/dev/null
+
+  rm -rf classes && mkdir classes
+  javac -d classes -source 1.5 "$(jvmpath "$SOURCE")" || fail "Failed to compile sources"
+  jar cf "$(jvmpath "$TARGET")" -C classes . || fail "Failed to produce $TARGET"
+  rm -rf classes
+
+  popd >/dev/null
+fi
+
+
+## main
+
+JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}"
+exec "$JAVA_EXE" -classpath "$(jvmpath "$TARGET")" isabelle.Java_Ext_Dirs \
+  "$(jvmpath "$ISABELLE_HOME/lib/classes/ext")"
+
diff -r 15df7bc8e93f -r d6791dc3534d src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Pure/General/xml.scala	Thu Jun 23 10:08:35 2011 -0700
@@ -6,6 +6,7 @@
 
 package isabelle
 
+import java.lang.System
 import java.util.WeakHashMap
 import java.lang.ref.WeakReference
 import javax.xml.parsers.DocumentBuilderFactory
diff -r 15df7bc8e93f -r d6791dc3534d src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Pure/PIDE/command.scala	Thu Jun 23 10:08:35 2011 -0700
@@ -7,6 +7,7 @@
 
 package isabelle
 
+import java.lang.System
 
 import scala.collection.immutable.SortedMap
 
diff -r 15df7bc8e93f -r d6791dc3534d src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Pure/PIDE/markup_tree.scala	Thu Jun 23 10:08:35 2011 -0700
@@ -7,7 +7,7 @@
 
 package isabelle
 
-
+import java.lang.System
 import javax.swing.tree.DefaultMutableTreeNode
 
 import scala.collection.immutable.SortedMap
diff -r 15df7bc8e93f -r d6791dc3534d src/Pure/System/Java_Ext_Dirs.java
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/Java_Ext_Dirs.java	Thu Jun 23 10:08:35 2011 -0700
@@ -0,0 +1,22 @@
+/*  Title:      Pure/System/Java_Ext_Dirs.java
+    Author:     Makarius
+
+Augment Java extension directories.
+*/
+
+package isabelle;
+
+public class Java_Ext_Dirs
+{
+  public static void main(String [] args) {
+    StringBuilder s = new StringBuilder();
+    s.append(System.getProperty("java.ext.dirs"));
+    int i;
+    for (i = 0; i < args.length; i++) {
+      s.append(System.getProperty("path.separator"));
+      s.append(args[i]);
+    }
+    System.out.println(s.toString());
+  }
+}
+
diff -r 15df7bc8e93f -r d6791dc3534d src/Pure/System/cygwin.scala
--- a/src/Pure/System/cygwin.scala	Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Pure/System/cygwin.scala	Thu Jun 23 10:08:35 2011 -0700
@@ -6,6 +6,7 @@
 
 package isabelle
 
+import java.lang.System
 import java.lang.reflect.Method
 import java.io.File
 import java.net.URL
@@ -91,7 +92,7 @@
 
   def check_root(): String =
   {
-    val this_cygwin = java.lang.System.getenv("THIS_CYGWIN")
+    val this_cygwin = System.getenv("THIS_CYGWIN")
     val root =
       if (this_cygwin != null && this_cygwin != "") this_cygwin
       else
diff -r 15df7bc8e93f -r d6791dc3534d src/Pure/System/gui_setup.scala
--- a/src/Pure/System/gui_setup.scala	Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Pure/System/gui_setup.scala	Thu Jun 23 10:08:35 2011 -0700
@@ -6,6 +6,8 @@
 
 package isabelle
 
+import java.lang.System
+
 import scala.swing.{Button, FlowPanel, BorderPanel, MainFrame, TextArea, SwingApplication}
 import scala.swing.event.ButtonClicked
 
diff -r 15df7bc8e93f -r d6791dc3534d src/Pure/System/isabelle_charset.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/isabelle_charset.scala	Thu Jun 23 10:08:35 2011 -0700
@@ -0,0 +1,50 @@
+/*  Title:      Pure/System/isabelle_charset.scala
+    Author:     Makarius
+
+Charset for Isabelle symbols.
+*/
+
+package isabelle
+
+import java.nio.Buffer
+import java.nio.{ByteBuffer, CharBuffer}
+import java.nio.charset.{Charset, CharsetDecoder, CharsetEncoder, CoderResult}
+import java.nio.charset.spi.CharsetProvider
+
+
+object Isabelle_Charset
+{
+  val name: String = "UTF-8-Isabelle-test"  // FIXME
+  lazy val charset: Charset = new Isabelle_Charset
+}
+
+
+class Isabelle_Charset extends Charset(Isabelle_Charset.name, null)
+{
+  override def contains(cs: Charset): Boolean =
+    cs.name.equalsIgnoreCase(Standard_System.charset_name) ||
+    Standard_System.charset.contains(cs)
+
+  override def newDecoder(): CharsetDecoder =
+    Standard_System.charset.newDecoder
+
+  override def newEncoder(): CharsetEncoder =
+    Standard_System.charset.newEncoder
+}
+
+
+class Isabelle_Charset_Provider extends CharsetProvider
+{
+  override def charsetForName(name: String): Charset =
+  {
+    if (name.equalsIgnoreCase(Isabelle_Charset.name)) Isabelle_Charset.charset
+    else null
+  }
+
+  override def charsets(): java.util.Iterator[Charset] =
+  {
+    import scala.collection.JavaConversions._
+    Iterator(Isabelle_Charset.charset)
+  }
+}
+
diff -r 15df7bc8e93f -r d6791dc3534d src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Pure/System/isabelle_process.scala	Thu Jun 23 10:08:35 2011 -0700
@@ -7,6 +7,7 @@
 
 package isabelle
 
+import java.lang.System
 import java.util.concurrent.LinkedBlockingQueue
 import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
   InputStream, OutputStream, BufferedOutputStream, IOException}
diff -r 15df7bc8e93f -r d6791dc3534d src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Pure/System/isabelle_system.scala	Thu Jun 23 10:08:35 2011 -0700
@@ -6,6 +6,7 @@
 
 package isabelle
 
+import java.lang.System
 import java.util.regex.Pattern
 import java.util.Locale
 import java.io.{InputStream, FileInputStream, OutputStream, FileOutputStream, File,
@@ -41,7 +42,7 @@
   {
     import scala.collection.JavaConversions._
 
-    val env0 = Map(java.lang.System.getenv.toList: _*) +
+    val env0 = Map(System.getenv.toList: _*) +
       ("THIS_JAVA" -> this_java())
 
     val isabelle_home =
@@ -49,7 +50,7 @@
       else
         env0.get("ISABELLE_HOME") match {
           case None | Some("") =>
-            val path = java.lang.System.getProperty("isabelle.home")
+            val path = System.getProperty("isabelle.home")
             if (path == null || path == "") error("Unknown Isabelle home directory")
             else path
           case Some(path) => path
@@ -70,8 +71,8 @@
             else (entry.substring(0, i) -> entry.substring(i + 1))
           }
         Map(entries: _*) +
-          ("HOME" -> java.lang.System.getenv("HOME")) +
-          ("PATH" -> java.lang.System.getenv("PATH"))
+          ("HOME" -> System.getenv("HOME")) +
+          ("PATH" -> System.getenv("PATH"))
       }
   }
 
diff -r 15df7bc8e93f -r d6791dc3534d src/Pure/System/platform.scala
--- a/src/Pure/System/platform.scala	Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Pure/System/platform.scala	Thu Jun 23 10:08:35 2011 -0700
@@ -6,6 +6,7 @@
 
 package isabelle
 
+import java.lang.System
 import javax.swing.UIManager
 
 import scala.util.matching.Regex
@@ -34,7 +35,7 @@
   lazy val jvm_platform: String =
   {
     val arch =
-      java.lang.System.getProperty("os.arch") match {
+      System.getProperty("os.arch") match {
         case X86() => "x86"
         case X86_64() => "x86_64"
         case Sparc() => "sparc"
@@ -42,7 +43,7 @@
         case _ => error("Failed to determine CPU architecture")
       }
     val os =
-      java.lang.System.getProperty("os.name") match {
+      System.getProperty("os.name") match {
         case Solaris() => "solaris"
         case Linux() => "linux"
         case Darwin() => "darwin"
@@ -55,7 +56,7 @@
 
   /* JVM name */
 
-  val jvm_name: String = java.lang.System.getProperty("java.vm.name")
+  val jvm_name: String = System.getProperty("java.vm.name")
   val is_hotspot: Boolean = jvm_name.startsWith("Java HotSpot")
 
 
diff -r 15df7bc8e93f -r d6791dc3534d src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Pure/System/session.scala	Thu Jun 23 10:08:35 2011 -0700
@@ -7,6 +7,7 @@
 
 package isabelle
 
+import java.lang.System
 
 import scala.actors.TIMEOUT
 import scala.actors.Actor
diff -r 15df7bc8e93f -r d6791dc3534d src/Pure/System/standard_system.scala
--- a/src/Pure/System/standard_system.scala	Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Pure/System/standard_system.scala	Thu Jun 23 10:08:35 2011 -0700
@@ -6,6 +6,7 @@
 
 package isabelle
 
+import java.lang.System
 import java.util.zip.{ZipEntry, ZipInputStream}
 import java.util.regex.Pattern
 import java.util.Locale
@@ -13,6 +14,7 @@
 import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
   BufferedInputStream, InputStream, FileInputStream, BufferedReader, InputStreamReader,
   File, FileFilter, IOException}
+import java.nio.charset.Charset
 
 import scala.io.{Source, Codec}
 import scala.util.matching.Regex
@@ -23,7 +25,8 @@
 {
   /* UTF-8 charset */
 
-  val charset = "UTF-8"
+  val charset_name: String = "UTF-8"
+  val charset: Charset = Charset.forName(charset_name)
   def codec(): Codec = Codec(charset)
 
   def string_bytes(s: String): Array[Byte] = s.getBytes(charset)
@@ -95,7 +98,8 @@
 
   def write_file(file: File, text: CharSequence)
   {
-    val writer = new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), charset))
+    val writer =
+      new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), charset))
     try { writer.append(text) }
     finally { writer.close }
   }
diff -r 15df7bc8e93f -r d6791dc3534d src/Pure/build-jars
--- a/src/Pure/build-jars	Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Pure/build-jars	Thu Jun 23 10:08:35 2011 -0700
@@ -37,6 +37,7 @@
   System/download.scala
   System/event_bus.scala
   System/gui_setup.scala
+  System/isabelle_charset.scala
   System/isabelle_process.scala
   System/isabelle_syntax.scala
   System/isabelle_system.scala
@@ -106,16 +107,10 @@
 
 
 
-## dependencies
+# build
 
 TARGET_DIR="$ISABELLE_HOME/lib/classes"
-PURE_JAR="$TARGET_DIR/Pure.jar"
-FULL_JAR="$TARGET_DIR/isabelle-scala.jar"
-
-declare -a TARGETS=("$PURE_JAR" "$FULL_JAR")
-
-
-## main
+TARGET="$TARGET_DIR/ext/Pure.jar"
 
 declare -a UPDATED=()
 
@@ -123,23 +118,16 @@
   OUTDATED=true
 else
   OUTDATED=false
-  for TARGET in "${TARGETS[@]}"
-  do
-    [ ! -e "$TARGET" ] && OUTDATED=true
-  done
-  if [ "$OUTDATED" = false ]; then
+  if [ ! -e "$TARGET" ]; then
+    OUTDATED=true
+  else
     for DEP in "${SOURCES[@]}"
     do
       [ ! -e "$DEP" ] && fail "Missing file: $DEP"
-      UPDATE=""
-      for TARGET in "${TARGETS[@]}"
-      do
-        [ "$DEP" -nt "$TARGET" ] && {
-          OUTDATED=true
-          UPDATE=true
-        }
-      done
-      [ -n "$UPDATE" ] && UPDATED["${#UPDATED[@]}"]="$DEP"
+      [ "$DEP" -nt "$TARGET" ] && {
+        OUTDATED=true
+        UPDATED["${#UPDATED[@]}"]="$DEP"
+      }
     done
   fi
 fi
@@ -161,19 +149,18 @@
   rm -rf classes && mkdir classes
   "$SCALA_HOME/bin/scalac" -unchecked -deprecation -d classes -target:jvm-1.5 "${SOURCES[@]}" || \
     fail "Failed to compile sources"
-  mkdir -p "$TARGET_DIR" || fail "Failed to create directory $TARGET_DIR"
+  mkdir -p "$TARGET_DIR/ext" || fail "Failed to create directory $TARGET_DIR/ext"
 
   pushd classes >/dev/null
 
-  jar cfe "$(jvmpath "$PURE_JAR")" isabelle.GUI_Setup isabelle || \
-    fail "Failed to produce $PURE_JAR"
+  CHARSET_SERVICE="META-INF/services/java.nio.charset.spi.CharsetProvider"
+  mkdir -p "$(dirname "$CHARSET_SERVICE")"
+  echo isabelle.Isabelle_Charset_Provider > "$CHARSET_SERVICE"
 
-  cp "$SCALA_HOME/lib/scala-swing.jar" .
-  jar xf scala-swing.jar
+  jar cfe "$(jvmpath "$TARGET")" isabelle.GUI_Setup META-INF isabelle || \
+    fail "Failed to produce $TARGET"
 
-  cp "$SCALA_HOME/lib/scala-library.jar" "$FULL_JAR"
-  jar ufe "$(jvmpath "$FULL_JAR")" isabelle.GUI_Setup isabelle scala || \
-    fail "Failed to produce $FULL_JAR"
+  cp "$SCALA_HOME/lib/scala-swing.jar" "$SCALA_HOME/lib/scala-library.jar" "$TARGET_DIR/ext"
 
   popd >/dev/null
 
diff -r 15df7bc8e93f -r d6791dc3534d src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Tools/jEdit/lib/Tools/jedit	Thu Jun 23 10:08:35 2011 -0700
@@ -146,7 +146,7 @@
 [ -e "$ISABELLE_HOME/Admin/build" ] && \
   { "$ISABELLE_HOME/Admin/build" "$BUILD_JARS" || exit $?; }
 
-PURE_JAR="$ISABELLE_HOME/lib/classes/Pure.jar"
+PURE_JAR="$ISABELLE_HOME/lib/classes/ext/Pure.jar"
 
 pushd "$JEDIT_HOME" >/dev/null || failed
 
@@ -234,14 +234,13 @@
       print qq,<MODE NAME="scala" FILE="scala.xml" FILE_NAME_GLOB="*.scala" />\n\n,; }
     print; }' dist/modes/catalog
 
-  cp -a "${JEDIT_JARS[@]}" "${SCALA_JARS[@]}" "$PURE_JAR" dist/jars/. || failed
+  cp -a "${JEDIT_JARS[@]}" "$SCALA_HOME/lib/scala-compiler.jar" dist/jars/. || failed
   (
-    for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$SCALA_HOME/lib/scala-compiler.jar"
+    for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "$SCALA_HOME/lib/scala-compiler.jar"
     do
       CLASSPATH="$CLASSPATH:$JAR"
     done
     CLASSPATH="$(jvmpath "$CLASSPATH")"
-
     exec "$SCALA_HOME/bin/scalac" -unchecked -deprecation \
       -d dist/classes -target:jvm-1.5 "${SOURCES[@]}"
   ) || fail "Failed to compile sources"
diff -r 15df7bc8e93f -r d6791dc3534d src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Tools/jEdit/src/document_view.scala	Thu Jun 23 10:08:35 2011 -0700
@@ -12,6 +12,7 @@
 
 import scala.actors.Actor._
 
+import java.lang.System
 import java.awt.{BorderLayout, Graphics, Color, Dimension, Graphics2D, Point}
 import java.awt.event.{MouseAdapter, MouseMotionAdapter, MouseEvent,
   FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
diff -r 15df7bc8e93f -r d6791dc3534d src/Tools/jEdit/src/html_panel.scala
--- a/src/Tools/jEdit/src/html_panel.scala	Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Tools/jEdit/src/html_panel.scala	Thu Jun 23 10:08:35 2011 -0700
@@ -9,6 +9,7 @@
 
 import isabelle._
 
+import java.lang.System
 import java.io.StringReader
 import java.awt.{Font, BorderLayout, Dimension, GraphicsEnvironment, Toolkit, FontMetrics}
 import java.awt.event.MouseEvent
diff -r 15df7bc8e93f -r d6791dc3534d src/Tools/jEdit/src/isabelle_encoding.scala
--- a/src/Tools/jEdit/src/isabelle_encoding.scala	Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Tools/jEdit/src/isabelle_encoding.scala	Thu Jun 23 10:08:35 2011 -0700
@@ -29,8 +29,7 @@
 
 class Isabelle_Encoding extends Encoding
 {
-  private val charset = Charset.forName(Standard_System.charset)
-  val BUFSIZE = 32768
+  private val BUFSIZE = 32768
 
   private def text_reader(in: InputStream, codec: Codec): Reader =
   {
@@ -54,12 +53,12 @@
     val buffer = new ByteArrayOutputStream(BUFSIZE) {
       override def flush()
       {
-        val text = Isabelle.system.symbols.encode(toString(Standard_System.charset))
+        val text = Isabelle.system.symbols.encode(toString(Standard_System.charset_name))
         out.write(text.getBytes(Standard_System.charset))
         out.flush()
       }
       override def close() { out.close() }
     }
-    new OutputStreamWriter(buffer, charset.newEncoder())
+    new OutputStreamWriter(buffer, Standard_System.charset.newEncoder())
   }
 }
diff -r 15df7bc8e93f -r d6791dc3534d src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Tools/jEdit/src/output_dockable.scala	Thu Jun 23 10:08:35 2011 -0700
@@ -14,6 +14,7 @@
 import scala.swing.{FlowPanel, Button, CheckBox}
 import scala.swing.event.ButtonClicked
 
+import java.lang.System
 import java.awt.BorderLayout
 import java.awt.event.{ComponentEvent, ComponentAdapter}
 
diff -r 15df7bc8e93f -r d6791dc3534d src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Jun 23 10:08:35 2011 -0700
@@ -9,6 +9,7 @@
 
 import isabelle._
 
+import java.lang.System
 import java.io.{FileInputStream, IOException}
 import java.awt.Font
 
diff -r 15df7bc8e93f -r d6791dc3534d src/Tools/jEdit/src/protocol_dockable.scala
--- a/src/Tools/jEdit/src/protocol_dockable.scala	Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Tools/jEdit/src/protocol_dockable.scala	Thu Jun 23 10:08:35 2011 -0700
@@ -9,6 +9,8 @@
 
 import isabelle._
 
+import java.lang.System
+
 import scala.actors.Actor._
 import scala.swing.{TextArea, ScrollPane}
 
diff -r 15df7bc8e93f -r d6791dc3534d src/Tools/jEdit/src/raw_output_dockable.scala
--- a/src/Tools/jEdit/src/raw_output_dockable.scala	Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala	Thu Jun 23 10:08:35 2011 -0700
@@ -9,6 +9,8 @@
 
 import isabelle._
 
+import java.lang.System
+
 import scala.actors.Actor._
 import scala.swing.{TextArea, ScrollPane}
 
diff -r 15df7bc8e93f -r d6791dc3534d src/Tools/jEdit/src/scala_console.scala
--- a/src/Tools/jEdit/src/scala_console.scala	Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Tools/jEdit/src/scala_console.scala	Thu Jun 23 10:08:35 2011 -0700
@@ -14,6 +14,7 @@
 import org.gjt.sp.jedit.{jEdit, JARClassLoader}
 import org.gjt.sp.jedit.MiscUtilities
 
+import java.lang.System
 import java.io.{File, OutputStream, Writer, PrintWriter}
 
 import scala.tools.nsc.{Interpreter, GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
diff -r 15df7bc8e93f -r d6791dc3534d src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Thu Jun 23 10:07:16 2011 -0700
+++ b/src/Tools/jEdit/src/session_dockable.scala	Thu Jun 23 10:08:35 2011 -0700
@@ -13,6 +13,7 @@
 import scala.swing.{FlowPanel, Button, TextArea, Label, ScrollPane, TabbedPane, Component, Swing}
 import scala.swing.event.{ButtonClicked, SelectionChanged}
 
+import java.lang.System
 import java.awt.BorderLayout
 import javax.swing.border.{BevelBorder, SoftBevelBorder}