src/Tools/jEdit/src/renderer/UserAgent.scala
changeset 34754 e8bb3052f3cb
parent 34753 dd8bdcb7dcba
child 34755 bc255171994b
     1.1 --- a/src/Tools/jEdit/src/renderer/UserAgent.scala	Mon Dec 07 22:59:48 2009 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,75 +0,0 @@
     1.4 -/*
     1.5 - * XML/CSS rendering -- user agent
     1.6 - *
     1.7 - * @author Fabian Immler, TU Munich
     1.8 - * @author Johannes Hölzl, TU Munich
     1.9 - */
    1.10 -
    1.11 -package isabelle.renderer
    1.12 -
    1.13 -import isabelle.jedit.Isabelle
    1.14 -
    1.15 -import scala.io.Source
    1.16 -
    1.17 -import java.io.{InputStream, ByteArrayInputStream, FileInputStream}
    1.18 -
    1.19 -import org.xhtmlrenderer.swing.NaiveUserAgent
    1.20 -import org.xhtmlrenderer.resource.CSSResource
    1.21 -
    1.22 -
    1.23 -object UserAgent
    1.24 -{
    1.25 -  val base_URL = "file://localhost/dummy/"
    1.26 -
    1.27 -  private val style = base_URL + "style"
    1.28 -  private val isabelle_css = base_URL + "isabelle.css"
    1.29 -  private val isabelle_user_css = base_URL + "isabelle_user.css"
    1.30 -  private val stylesheet = """
    1.31 -@import "isabelle.css";
    1.32 -@import 'isabelle_user.css';
    1.33 -
    1.34 -messages, message {
    1.35 -  display: block;
    1.36 -  white-space: pre-wrap;
    1.37 -  font-family: Isabelle;
    1.38 -}
    1.39 -""" 
    1.40 -}
    1.41 -
    1.42 -class UserAgent extends NaiveUserAgent
    1.43 -{
    1.44 -  private def string_content(text: String): Array[Byte] =
    1.45 -    text.getBytes(Isabelle_System.charset)
    1.46 -  
    1.47 -  private def try_file_content(name: String): Array[Byte] =
    1.48 -  {
    1.49 -    val file = Isabelle.system.platform_file(name)
    1.50 -    val text =
    1.51 -      if (file.exists) Source.fromFile(file).mkString
    1.52 -      else ""
    1.53 -    string_content(text)
    1.54 -  }
    1.55 -
    1.56 -  private def CSS(content: Array[Byte]): CSSResource =
    1.57 -    new CSSResource(new ByteArrayInputStream(content))
    1.58 -
    1.59 -  private val stylesheet = string_content(UserAgent.stylesheet)
    1.60 -  private val isabelle_css = try_file_content("~~/lib/html/isabelle.css")
    1.61 -  private val isabelle_user_css = try_file_content("$ISABELLE_HOME_USER/etc/isabelle.css")
    1.62 -
    1.63 -  override def getCSSResource(uri: String): CSSResource =
    1.64 -  {
    1.65 -    uri match {
    1.66 -      case UserAgent.style => CSS(stylesheet)
    1.67 -      case UserAgent.isabelle_css => CSS(isabelle_css)
    1.68 -      case UserAgent.isabelle_user_css => CSS(isabelle_user_css)
    1.69 -      case _ =>
    1.70 -        val stream = resolveAndOpenStream(uri)
    1.71 -        val resource = new CSSResource(stream)
    1.72 -        if (stream == null)
    1.73 -          resource.getResourceInputSource().setByteStream(
    1.74 -            new ByteArrayInputStream(Array()))
    1.75 -        resource
    1.76 -    }
    1.77 -  }
    1.78 -}
    1.79 \ No newline at end of file