deactivate unfinished charset provider for now, to avoid user confusion;
authorwenzelm
Wed, 07 Sep 2011 11:36:39 +0200
changeset 44778 18b1ba7cfcfe
parent 44777 1afb48f872ae
child 44779 98d597c4193d
child 44782 ba4c0205267f
child 44788 8b935f1b3cf8
deactivate unfinished charset provider for now, to avoid user confusion;
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()
   }
 }