24 |
24 |
25 /* basic markup */ |
25 /* basic markup */ |
26 |
26 |
27 val Empty = Markup("", Nil) |
27 val Empty = Markup("", Nil) |
28 val Broken = Markup("broken", Nil) |
28 val Broken = Markup("broken", Nil) |
|
29 |
|
30 class Markup_String(val name: String, prop: String) |
|
31 { |
|
32 private val Prop = new Properties.String(prop) |
|
33 |
|
34 def apply(s: String): Markup = Markup(name, Prop(s)) |
|
35 def unapply(markup: Markup): Option[String] = |
|
36 if (markup.name == name) Prop.unapply(markup.properties) else None |
|
37 } |
|
38 |
|
39 class Markup_Int(val name: String, prop: String) |
|
40 { |
|
41 private val Prop = new Properties.Int(prop) |
|
42 |
|
43 def apply(i: Int): Markup = Markup(name, Prop(i)) |
|
44 def unapply(markup: Markup): Option[Int] = |
|
45 if (markup.name == name) Prop.unapply(markup.properties) else None |
|
46 } |
29 |
47 |
30 |
48 |
31 /* formal entities */ |
49 /* formal entities */ |
32 |
50 |
33 val BINDING = "binding" |
51 val BINDING = "binding" |
37 |
55 |
38 object Entity |
56 object Entity |
39 { |
57 { |
40 def unapply(markup: Markup): Option[(String, String)] = |
58 def unapply(markup: Markup): Option[(String, String)] = |
41 markup match { |
59 markup match { |
42 case Markup(ENTITY, props @ Kind(kind)) => |
60 case Markup(ENTITY, props) => |
43 props match { |
61 (props, props) match { |
44 case Name(name) => Some(kind, name) |
62 case (Kind(kind), Name(name)) => Some(kind, name) |
45 case _ => None |
63 case _ => None |
46 } |
64 } |
47 case _ => None |
65 case _ => None |
48 } |
66 } |
49 } |
67 } |
68 |
86 |
69 |
87 |
70 /* embedded languages */ |
88 /* embedded languages */ |
71 |
89 |
72 val LANGUAGE = "language" |
90 val LANGUAGE = "language" |
73 |
91 val Language = new Markup_String(LANGUAGE, NAME) |
74 object Language |
|
75 { |
|
76 def unapply(markup: Markup): Option[String] = |
|
77 markup match { |
|
78 case Markup(LANGUAGE, Name(name)) => Some(name) |
|
79 case _ => None |
|
80 } |
|
81 } |
|
82 |
92 |
83 |
93 |
84 /* external resources */ |
94 /* external resources */ |
85 |
95 |
86 val PATH = "path" |
96 val PATH = "path" |
87 |
97 val Path = new Markup_String(PATH, NAME) |
88 object Path |
|
89 { |
|
90 def unapply(markup: Markup): Option[String] = |
|
91 markup match { |
|
92 case Markup(PATH, Name(name)) => Some(name) |
|
93 case _ => None |
|
94 } |
|
95 } |
|
96 |
98 |
97 val URL = "url" |
99 val URL = "url" |
98 |
100 val Url = new Markup_String(URL, NAME) |
99 object Url |
|
100 { |
|
101 def unapply(markup: Markup): Option[String] = |
|
102 markup match { |
|
103 case Markup(URL, Name(name)) => Some(name) |
|
104 case _ => None |
|
105 } |
|
106 } |
|
107 |
101 |
108 |
102 |
109 /* pretty printing */ |
103 /* pretty printing */ |
110 |
104 |
111 val Indent = new Properties.Int("indent") |
105 val Block = new Markup_Int("block", "indent") |
112 val BLOCK = "block" |
106 val Break = new Markup_Int("break", "width") |
113 |
|
114 val Width = new Properties.Int("width") |
|
115 val BREAK = "break" |
|
116 |
107 |
117 val ITEM = "item" |
108 val ITEM = "item" |
118 val BULLET = "bullet" |
109 val BULLET = "bullet" |
119 |
110 |
120 val SEPARATOR = "separator" |
111 val SEPARATOR = "separator" |