| 83 request.setAttribute(Constants.REQ_ATTR_PAGE_TITLE, value) |
83 request.setAttribute(Constants.REQ_ATTR_PAGE_TITLE, value) |
| 84 } |
84 } |
| 85 |
85 |
| 86 /** |
86 /** |
| 87 * A list of additional style sheets. |
87 * A list of additional style sheets. |
| 88 * TODO: remove this unnecessary attribute and merge all style sheets into one global |
|
| 89 * @see Constants#REQ_ATTR_STYLESHEET |
|
| 90 */ |
|
| 91 var styleSheets = emptyList<String>() |
|
| 92 set(value) { |
|
| 93 field = value |
|
| 94 request.setAttribute(Constants.REQ_ATTR_STYLESHEET, |
|
| 95 value.map { "$it.css" } |
|
| 96 ) |
|
| 97 } |
|
| 98 |
|
| 99 /** |
|
| 100 * A list of additional style sheets. |
|
| 101 * |
88 * |
| 102 * @see Constants#REQ_ATTR_JAVASCRIPT |
89 * @see Constants#REQ_ATTR_JAVASCRIPT |
| 103 */ |
90 */ |
| 104 var javascript = "" |
91 var javascript = "" |
| 105 set(value) { |
92 set(value) { |