diff --git a/src/Pure/General/url.scala b/src/Pure/General/url.scala
--- a/src/Pure/General/url.scala
+++ b/src/Pure/General/url.scala
@@ -1,103 +1,103 @@
 /*  Title:      Pure/General/url.scala
     Author:     Makarius
 
 Basic URL operations.
 */
 
 package isabelle
 
 
 import java.io.{File => JFile}
 import java.nio.file.{Paths, FileSystemNotFoundException}
 import java.net.{URI, URISyntaxException, URL, MalformedURLException, URLDecoder, URLEncoder}
 import java.util.Locale
 import java.util.zip.GZIPInputStream
 
 
 object Url {
   /* special characters */
 
   def escape_special(c: Char): String =
     if ("!#$&'()*+,/:;=?@[]".contains(c)) {
       String.format(Locale.ROOT, "%%%02X", Integer.valueOf(c.toInt))
     }
     else c.toString
 
   def escape_special(s: String): String = s.iterator.map(escape_special).mkString
 
   def escape_name(name: String): String =
     name.iterator.map({ case '\'' => "%27" case c => c.toString }).mkString
 
 
   /* make and check URLs */
 
   def apply(name: String): URL = {
     try { new URL(name) }
     catch { case _: MalformedURLException => error("Malformed URL " + quote(name)) }
   }
 
   def is_wellformed(name: String): Boolean =
     try { Url(name); true }
     catch { case ERROR(_) => false }
 
   def is_readable(name: String): Boolean =
     try { Url(name).openStream.close(); true }
     catch { case ERROR(_) => false }
 
 
   /* file name */
 
   def file_name(url: URL): String =
     Library.take_suffix[Char](c => c != '/' && c != '\\', url.getFile.toString.toList)._2.mkString
 
   def trim_index(url: URL): URL = {
     Library.try_unprefix("/index.html", url.toString) match {
       case Some(u) => Url(u)
       case None =>
         Library.try_unprefix("/index.php", url.toString) match {
           case Some(u) => Url(u)
           case None => url
         }
     }
   }
 
 
   /* strings */
 
-  def decode(s: String): String = URLDecoder.decode(s, UTF8.charset_name)
-  def encode(s: String): String = URLEncoder.encode(s, UTF8.charset_name)
+  def decode(s: String): String = URLDecoder.decode(s, UTF8.charset)
+  def encode(s: String): String = URLEncoder.encode(s, UTF8.charset)
 
 
   /* read */
 
   private def read(url: URL, gzip: Boolean): String =
     using(url.openStream)(stream =>
       File.read_stream(if (gzip) new GZIPInputStream(stream) else stream))
 
   def read(url: URL): String = read(url, false)
   def read_gzip(url: URL): String = read(url, true)
 
   def read(name: String): String = read(Url(name), false)
   def read_gzip(name: String): String = read(Url(name), true)
 
 
   /* file URIs */
 
   def print_file(file: JFile): String = File.absolute(file).toPath.toUri.toString
   def print_file_name(name: String): String = print_file(new JFile(name))
 
   def parse_file(uri: String): JFile = Paths.get(new URI(uri)).toFile
 
   def is_wellformed_file(uri: String): Boolean =
     try { parse_file(uri); true }
     catch {
       case _: URISyntaxException | _: IllegalArgumentException | _: FileSystemNotFoundException =>
         false
     }
 
   def absolute_file(uri: String): JFile = File.absolute(parse_file(uri))
   def absolute_file_name(uri: String): String = absolute_file(uri).getPath
 
   def canonical_file(uri: String): JFile = File.canonical(parse_file(uri))
   def canonical_file_name(uri: String): String = canonical_file(uri).getPath
 }
diff --git a/src/Tools/jEdit/src/isabelle_encoding.scala b/src/Tools/jEdit/src/isabelle_encoding.scala
--- a/src/Tools/jEdit/src/isabelle_encoding.scala
+++ b/src/Tools/jEdit/src/isabelle_encoding.scala
@@ -1,63 +1,63 @@
 /*  Title:      Tools/jEdit/src/isabelle_encoding.scala
     Author:     Makarius
 
 Isabelle encoding -- based on UTF-8.
 */
 
 package isabelle.jedit
 
 
 import isabelle._
 
 import org.gjt.sp.jedit.buffer.JEditBuffer
 import org.gjt.sp.jedit.io.Encoding
 
 import java.nio.charset.{Charset, CodingErrorAction, CharacterCodingException}
 import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter,
   CharArrayReader, ByteArrayOutputStream}
 
 import scala.io.{Codec, BufferedSource}
 
 
 object Isabelle_Encoding {
   def is_active(buffer: JEditBuffer): Boolean =
     buffer.getStringProperty(JEditBuffer.ENCODING).asInstanceOf[String] == "UTF-8-Isabelle"
 
   def perhaps_decode(buffer: JEditBuffer, s: String): String =
     if (is_active(buffer)) Symbol.decode(s) else s
 }
 
 class Isabelle_Encoding extends Encoding {
   private val BUFSIZE = 32768
 
   private def text_reader(in: InputStream, codec: Codec, strict: Boolean): Reader = {
     val source = (new BufferedSource(in)(codec)).mkString
 
     if (strict && Codepoint.iterator(source).exists(Symbol.symbols.code_defined))
       throw new CharacterCodingException()
 
     new CharArrayReader(Symbol.decode(source).toArray)
   }
 
   override def getTextReader(in: InputStream): Reader =
     text_reader(in, UTF8.codec(), true)
 
   override def getPermissiveTextReader(in: InputStream): Reader = {
     val codec = UTF8.codec()
     codec.onMalformedInput(CodingErrorAction.REPLACE)
     codec.onUnmappableCharacter(CodingErrorAction.REPLACE)
     text_reader(in, codec, false)
   }
 
   override def getTextWriter(out: OutputStream): Writer = {
     val buffer = new ByteArrayOutputStream(BUFSIZE) {
       override def flush(): Unit = {
-        val text = Symbol.encode(toString(UTF8.charset_name))
+        val text = Symbol.encode(toString(UTF8.charset))
         out.write(UTF8.bytes(text))
         out.flush()
       }
       override def close(): Unit = out.close()
     }
     new OutputStreamWriter(buffer, UTF8.charset.newEncoder())
   }
 }