equal
deleted
inserted
replaced
1 package isabelle.jedit |
|
2 |
|
3 import java.io.ByteArrayInputStream |
|
4 import org.xhtmlrenderer.swing.NaiveUserAgent |
|
5 import org.xhtmlrenderer.resource.CSSResource |
|
6 import isabelle.IsabelleSystem.getenv |
|
7 |
|
8 object UserAgent { |
|
9 val baseURL = "file://localhost" + getenv("ISABELLE_HOME") + "/lib/html/" |
|
10 val userStylesheet = "file://localhost" + getenv("ISABELLE_HOME_USER") + "/etc/user.css"; |
|
11 val stylesheet = """ |
|
12 |
|
13 @import "isabelle.css"; |
|
14 |
|
15 @import '""" + userStylesheet + """'; |
|
16 |
|
17 messages, message { |
|
18 display: block; |
|
19 white-space: pre-wrap; |
|
20 font-family: Isabelle; |
|
21 } |
|
22 """ |
|
23 } |
|
24 |
|
25 class UserAgent extends NaiveUserAgent { |
|
26 override def getCSSResource(uri : String) : CSSResource = { |
|
27 if (uri == UserAgent.baseURL + "style") |
|
28 new CSSResource( |
|
29 new ByteArrayInputStream(UserAgent.stylesheet.getBytes())) |
|
30 else { |
|
31 val stream = resolveAndOpenStream(uri) |
|
32 val resource = new CSSResource(stream) |
|
33 if (stream == null) |
|
34 resource.getResourceInputSource().setByteStream( |
|
35 new ByteArrayInputStream(new Array[Byte](0))) |
|
36 resource |
|
37 } |
|
38 } |
|
39 } |
|