diff --git a/src/Pure/General/http.scala b/src/Pure/General/http.scala
--- a/src/Pure/General/http.scala
+++ b/src/Pure/General/http.scala
@@ -1,370 +1,371 @@
 /*  Title:      Pure/General/http.scala
     Author:     Makarius
 
 HTTP client and server support.
 */
 
 package isabelle
 
 
 import java.io.{File => JFile}
 import java.nio.file.Files
 import java.net.{InetSocketAddress, URI, URL, HttpURLConnection}
 import com.sun.net.httpserver.{HttpExchange, HttpHandler, HttpServer}
 
 
 object HTTP
 {
   /** content **/
 
   object Content
   {
     val mime_type_bytes: String = "application/octet-stream"
     val mime_type_text: String = "text/plain; charset=utf-8"
     val mime_type_html: String = "text/html; charset=utf-8"
 
     val default_mime_type: String = mime_type_bytes
     val default_encoding: String = UTF8.charset_name
 
     def apply(
         bytes: Bytes,
         file_name: String = "",
         mime_type: String = default_mime_type,
         encoding: String = default_encoding,
         elapsed_time: Time = Time.zero): Content =
       new Content(bytes, file_name, mime_type, encoding, elapsed_time)
 
     def read(file: JFile): Content =
     {
       val bytes = Bytes.read(file)
       val file_name = file.getName
       val mime_type = Option(Files.probeContentType(file.toPath)).getOrElse(default_mime_type)
       apply(bytes, file_name = file_name, mime_type = mime_type)
     }
 
     def read(path: Path): Content = read(path.file)
   }
 
   class Content private(
     val bytes: Bytes,
     val file_name: String,
     val mime_type: String,
     val encoding: String,
     val elapsed_time: Time)
   {
     def text: String = new String(bytes.array, encoding)
     def json: JSON.T = JSON.parse(text)
   }
 
 
 
   /** client **/
 
   val NEWLINE: String = "\r\n"
 
   object Client
   {
     val default_timeout: Time = Time.seconds(180)
 
     def open_connection(url: URL,
       timeout: Time = default_timeout,
       user_agent: String = ""): HttpURLConnection =
     {
       url.openConnection match {
         case connection: HttpURLConnection =>
           if (0 < timeout.ms && timeout.ms <= Integer.MAX_VALUE) {
             val ms = timeout.ms.toInt
             connection.setConnectTimeout(ms)
             connection.setReadTimeout(ms)
           }
           proper_string(user_agent).foreach(s => connection.setRequestProperty("User-Agent", s))
           connection
         case _ => error("Bad URL (not HTTP): " + quote(url.toString))
       }
     }
 
     def get_content(connection: HttpURLConnection): Content =
     {
       val Charset = """.*\bcharset="?([\S^"]+)"?.*""".r
 
       val start = Time.now()
       using(connection.getInputStream)(stream =>
       {
         val bytes = Bytes.read_stream(stream, hint = connection.getContentLength)
         val stop = Time.now()
 
         val file_name = Url.file_name(connection.getURL)
         val mime_type = Option(connection.getContentType).getOrElse(Content.default_mime_type)
         val encoding =
           (connection.getContentEncoding, mime_type) match {
             case (enc, _) if enc != null => enc
             case (_, Charset(enc)) => enc
             case _ => Content.default_encoding
           }
         Content(bytes, file_name = file_name, mime_type = mime_type,
           encoding = encoding, elapsed_time = stop - start)
       })
     }
 
     def get(url: URL, timeout: Time = default_timeout, user_agent: String = ""): Content =
       get_content(open_connection(url, timeout = timeout, user_agent = user_agent))
 
     def post(url: URL, parameters: List[(String, Any)],
       timeout: Time = default_timeout,
       user_agent: String = ""): Content =
     {
       val connection = open_connection(url, timeout = timeout, user_agent = user_agent)
       connection.setRequestMethod("POST")
       connection.setDoOutput(true)
 
       val boundary = UUID.random().toString
       connection.setRequestProperty(
         "Content-Type", "multipart/form-data; boundary=" + quote(boundary))
 
       using(connection.getOutputStream)(out =>
       {
         def output(s: String): Unit = out.write(UTF8.bytes(s))
         def output_newline(n: Int = 1): Unit = (1 to n).foreach(_ => output(NEWLINE))
         def output_boundary(end: Boolean = false): Unit =
           output("--" + boundary + (if (end) "--" else "") + NEWLINE)
         def output_name(name: String): Unit =
           output("Content-Disposition: form-data; name=" + quote(name))
         def output_value(value: Any): Unit =
         {
           output_newline(2)
           output(value.toString)
         }
         def output_content(content: Content): Unit =
         {
           proper_string(content.file_name).foreach(s => output("; filename=" + quote(s)))
           output_newline()
           proper_string(content.mime_type).foreach(s => output("Content-Type: " + s))
           output_newline(2)
           content.bytes.write_stream(out)
         }
 
         output_newline(2)
 
         for { (name, value) <- parameters } {
           output_boundary()
           output_name(name)
           value match {
             case content: Content => output_content(content)
             case file: JFile => output_content(Content.read(file))
             case path: Path => output_content(Content.read(path))
             case _ => output_value(value)
           }
           output_newline()
         }
         output_boundary(end = true)
         out.flush()
       })
 
       get_content(connection)
     }
   }
 
 
 
   /** server **/
 
   /* request */
 
   def url_path(names: String*): String =
     names.iterator.flatMap(a => if (a.isEmpty) None else Some("/" + a)).mkString
 
   class Request private[HTTP](
     val server: String,
     val service: String,
     val uri: URI,
     val input: Bytes)
   {
     def home: String = url_path(server, service)
     def root: String = home + "/"
     def query: String = home + "?"
 
     def toplevel: Boolean = uri_name == home || uri_name == root
 
     val uri_name: String = uri.toString
 
     def uri_path: Option[Path] =
       for {
         s <- Option(uri.getPath).flatMap(Library.try_unprefix(root, _))
         if Path.is_wellformed(s)
         p = Path.explode(s) if p.all_basic
       } yield p
 
     def decode_query: Option[String] =
       Library.try_unprefix(query, uri_name).map(Url.decode)
 
     def decode_properties: Properties.T =
       space_explode('&', input.text).map(
         {
           case Properties.Eq(a, b) => Url.decode(a) -> Url.decode(b)
           case s => error("Malformed key-value pair in HTTP/POST: " + quote(s))
         })
   }
 
 
   /* response */
 
   object Response
   {
     def apply(
         bytes: Bytes = Bytes.empty,
         content_type: String = Content.mime_type_bytes): Response =
       new Response(bytes, content_type)
 
     val empty: Response = apply()
     def text(s: String): Response = apply(Bytes(s), Content.mime_type_text)
     def html(s: String): Response = apply(Bytes(s), Content.mime_type_html)
 
     def content(content: Content): Response = apply(content.bytes, content.mime_type)
     def read(file: JFile): Response = content(Content.read(file))
     def read(path: Path): Response = content(Content.read(path))
   }
 
   class Response private[HTTP](val output: Bytes, val content_type: String)
   {
     override def toString: String = output.toString
 
     def write(http: HttpExchange, code: Int): Unit =
     {
       http.getResponseHeaders.set("Content-Type", content_type)
       http.sendResponseHeaders(code, output.length.toLong)
       using(http.getResponseBody)(output.write_stream)
     }
   }
 
 
   /* service */
 
   abstract class Service(val service: String, method: String = "GET")
   {
     override def toString: String = service
 
     def apply(request: Request): Option[Response]
 
     def context(server: String): String = proper_string(url_path(server, service)).getOrElse("/")
 
     def handler(server: String): HttpHandler = (http: HttpExchange) => {
       val uri = http.getRequestURI
       val input = using(http.getRequestBody)(Bytes.read_stream(_))
       if (http.getRequestMethod == method) {
         val request = new Request(server, service, uri, input)
         Exn.capture(apply(request)) match {
           case Exn.Res(Some(response)) =>
             response.write(http, 200)
           case Exn.Res(None) =>
             Response.empty.write(http, 404)
           case Exn.Exn(ERROR(msg)) =>
             Response.text(Output.error_message_text(msg)).write(http, 500)
           case Exn.Exn(exn) => throw exn
         }
       }
       else Response.empty.write(http, 400)
     }
   }
 
 
   /* server */
 
   class Server private[HTTP](val name: String, val http_server: HttpServer)
   {
     def += (service: Service): Unit =
       http_server.createContext(service.context(name), service.handler(name))
     def -= (service: Service): Unit =
       http_server.removeContext(service.context(name))
 
     def start(): Unit = http_server.start()
     def stop(): Unit = http_server.stop(0)
 
     def address: InetSocketAddress = http_server.getAddress
 
     def url: String = "http://" + address.getHostName + ":" + address.getPort + url_path(name)
     override def toString: String = url
   }
 
   def server(
     name: String = UUID.random().toString,
     services: List[Service] = isabelle_services): Server =
   {
     val http_server = HttpServer.create(new InetSocketAddress(isabelle.Server.localhost, 0), 0)
     http_server.setExecutor(null)
 
     val server = new Server(name, http_server)
     for (service <- services) server += service
     server
   }
 
 
 
   /** Isabelle services **/
 
   def isabelle_services: List[Service] =
     List(new Welcome(), new Fonts(), new PDFjs(), new Docs())
 
 
   /* welcome */
 
   class Welcome(name: String = "") extends Service(name)
   {
     def apply(request: Request): Option[Response] =
       if (request.toplevel) {
         Some(Response.text("Welcome to " + Isabelle_System.identification()))
       }
       else None
   }
 
 
   /* fonts */
 
   class Fonts(name: String = "fonts") extends Service(name)
   {
     private lazy val html_fonts: List[Isabelle_Fonts.Entry] =
       Isabelle_Fonts.fonts(hidden = true)
 
     def apply(request: Request): Option[Response] =
       if (request.toplevel) {
         Some(Response.text(cat_lines(html_fonts.map(entry => entry.path.file_name))))
       }
       else {
         request.uri_path.flatMap(path =>
           html_fonts.collectFirst(
             { case entry if path == entry.path.base => Response(entry.bytes) }
           ))
       }
   }
 
 
   /* pdfjs */
 
   class PDFjs(name: String = "pdfjs") extends Service(name)
   {
     def apply(request: Request): Option[Response] =
       for {
         p <- request.uri_path
         path = Path.explode("$ISABELLE_PDFJS_HOME") + p if path.is_file
         s = p.implode if s.startsWith("build/") || s.startsWith("web/")
       } yield Response.read(path)
   }
 
 
   /* docs */
 
   class Docs(name: String = "docs") extends PDFjs(name)
   {
     private val doc_contents = isabelle.Doc.main_contents()
 
+    // example: .../docs/web/viewer.html?file=system.pdf
     def doc_request(request: Request): Option[Response] =
       for {
         p <- request.uri_path if p.is_pdf
-        s = p.implode if s.startsWith("pdf/")
+        s = p.implode if s.startsWith("web/")
         name = p.base.split_ext._1.implode
         doc <- doc_contents.docs.find(_.name == name)
       } yield Response.read(doc.path)
 
     override def apply(request: Request): Option[Response] =
       doc_request(request) orElse super.apply(request)
   }
 }