src/Tools/jEdit/src/jedit/UserAgent.scala
author wenzelm
Fri, 19 Dec 2008 22:24:32 +0100
changeset 34407 aad6834ba380
parent 34353 aa0d2f0bde83
permissions -rw-r--r--
added some headers and comments;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34407
aad6834ba380 added some headers and comments;
wenzelm
parents: 34353
diff changeset
     1
/*
aad6834ba380 added some headers and comments;
wenzelm
parents: 34353
diff changeset
     2
 * XML/CSS rendering -- user agent
aad6834ba380 added some headers and comments;
wenzelm
parents: 34353
diff changeset
     3
 *
aad6834ba380 added some headers and comments;
wenzelm
parents: 34353
diff changeset
     4
 * @author Fabian Immler, TU Munich
aad6834ba380 added some headers and comments;
wenzelm
parents: 34353
diff changeset
     5
 * @author Johannes Hölzl, TU Munich
aad6834ba380 added some headers and comments;
wenzelm
parents: 34353
diff changeset
     6
 */
aad6834ba380 added some headers and comments;
wenzelm
parents: 34353
diff changeset
     7
34353
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
     8
package isabelle.jedit
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
     9
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    10
import java.io.ByteArrayInputStream
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    11
import org.xhtmlrenderer.swing.NaiveUserAgent
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    12
import org.xhtmlrenderer.resource.CSSResource
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    13
import isabelle.IsabelleSystem.getenv
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    14
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    15
object UserAgent {
34407
aad6834ba380 added some headers and comments;
wenzelm
parents: 34353
diff changeset
    16
  // FIXME avoid static getenv
34353
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    17
  val baseURL = "file://localhost" + getenv("ISABELLE_HOME") + "/lib/html/"
34407
aad6834ba380 added some headers and comments;
wenzelm
parents: 34353
diff changeset
    18
  val userStylesheet =  "file://localhost" + getenv("ISABELLE_HOME_USER") + "/etc/user.css"
34353
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    19
  val stylesheet = """
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    20
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    21
@import "isabelle.css";
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    22
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    23
@import '""" + userStylesheet + """';
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    24
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    25
messages, message {
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    26
  display: block;
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    27
  white-space: pre-wrap;
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    28
  font-family: Isabelle;
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    29
}
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    30
""" 
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    31
}
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    32
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    33
class UserAgent extends NaiveUserAgent {
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    34
  override def getCSSResource(uri : String) : CSSResource = {
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    35
    if (uri == UserAgent.baseURL + "style")
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    36
      new CSSResource(
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    37
        new ByteArrayInputStream(UserAgent.stylesheet.getBytes()))
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    38
    else {
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    39
      val stream = resolveAndOpenStream(uri)
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    40
      val resource = new CSSResource(stream)
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    41
      if (stream == null)
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    42
        resource.getResourceInputSource().setByteStream(
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    43
          new ByteArrayInputStream(new Array[Byte](0)))
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    44
      resource
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    45
    }
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    46
  }
aa0d2f0bde83 UserAgent as seperate class, moved stylesheets, baseURL to UserAgent
immler@in.tum.de
parents:
diff changeset
    47
}