# HG changeset patch
# User wenzelm
# Date 1315388199 -7200
# Node ID 18b1ba7cfcfeb6a301ac4c476013e80cb85d6c42
# Parent  1afb48f872aeb522787bf7a350ac2cf8d4ef7eda
deactivate unfinished charset provider for now, to avoid user confusion;

diff -r 1afb48f872ae -r 18b1ba7cfcfe src/Pure/System/isabelle_charset.scala
--- a/src/Pure/System/isabelle_charset.scala	Wed Sep 07 11:26:27 2011 +0200
+++ b/src/Pure/System/isabelle_charset.scala	Wed Sep 07 11:36:39 2011 +0200
@@ -37,14 +37,18 @@
 {
   override def charsetForName(name: String): Charset =
   {
-    if (name.equalsIgnoreCase(Isabelle_Charset.name)) Isabelle_Charset.charset
-    else null
+    // FIXME inactive
+    // if (name.equalsIgnoreCase(Isabelle_Charset.name)) Isabelle_Charset.charset
+    // else null
+    null
   }
 
   override def charsets(): java.util.Iterator[Charset] =
   {
     import scala.collection.JavaConversions._
-    Iterator(Isabelle_Charset.charset)
+    // FIXME inactive
+    // Iterator(Isabelle_Charset.charset)
+    Iterator()
   }
 }