--- a/model/extra.css Wed Apr 18 10:44:40 2012 +0100
+++ b/model/extra.css Wed Apr 18 12:50:46 2012 +0100
@@ -360,6 +360,19 @@
content: ")*";
}
+div[class="grammar"] span[class="choice"]:before {
+ font-weight: normal;
+ font-size:130%;
+ font-family: monospace;
+ content: "(";
+}
+
+div[class="grammar"] span[class="choice"]:after {
+ font-weight: normal;
+ font-size:130%;
+ font-family: monospace;
+ content: ")";
+
div[class="grammar"] span[class="group"]:before {
font-weight: normal;
font-size:130%;