src/Tools/jEdit/src/renderer/UserAgent.scala
changeset 34430 ee19d8ef5dc3
parent 34407 aad6834ba380
child 34442 9e6d80c387e0
equal deleted inserted replaced
34429:03afc73e185f 34430:ee19d8ef5dc3
       
     1 /*
       
     2  * XML/CSS rendering -- user agent
       
     3  *
       
     4  * @author Fabian Immler, TU Munich
       
     5  * @author Johannes Hölzl, TU Munich
       
     6  */
       
     7 
       
     8 package isabelle.renderer
       
     9 
       
    10 
       
    11 import java.io.ByteArrayInputStream
       
    12 import org.xhtmlrenderer.swing.NaiveUserAgent
       
    13 import org.xhtmlrenderer.resource.CSSResource
       
    14 import isabelle.IsabelleSystem.getenv
       
    15 
       
    16 
       
    17 object UserAgent {
       
    18   // FIXME avoid static getenv
       
    19   val baseURL = "file://localhost" + getenv("ISABELLE_HOME") + "/lib/html/"
       
    20   val userStylesheet =  "file://localhost" + getenv("ISABELLE_HOME_USER") + "/etc/user.css"
       
    21   val stylesheet = """
       
    22 
       
    23 @import "isabelle.css";
       
    24 
       
    25 @import '""" + userStylesheet + """';
       
    26 
       
    27 messages, message {
       
    28   display: block;
       
    29   white-space: pre-wrap;
       
    30   font-family: Isabelle;
       
    31 }
       
    32 """ 
       
    33 }
       
    34 
       
    35 class UserAgent extends NaiveUserAgent {
       
    36   override def getCSSResource(uri : String) : CSSResource = {
       
    37     if (uri == UserAgent.baseURL + "style")
       
    38       new CSSResource(
       
    39         new ByteArrayInputStream(UserAgent.stylesheet.getBytes()))
       
    40     else {
       
    41       val stream = resolveAndOpenStream(uri)
       
    42       val resource = new CSSResource(stream)
       
    43       if (stream == null)
       
    44         resource.getResourceInputSource().setByteStream(
       
    45           new ByteArrayInputStream(new Array[Byte](0)))
       
    46       resource
       
    47     }
       
    48   }
       
    49 }