equal
deleted
inserted
replaced
104 |
104 |
105 |
105 |
106 |
106 |
107 /** keyword tables **/ |
107 /** keyword tables **/ |
108 |
108 |
109 object Spec |
109 sealed case class Spec( |
|
110 kind: String = "", |
|
111 load_command: String = "", |
|
112 tags: List[String] = Nil) |
110 { |
113 { |
111 val none: Spec = Spec("") |
|
112 } |
|
113 sealed case class Spec(kind: String, load_command: String = "", tags: List[String] = Nil) |
|
114 { |
|
115 def is_none: Boolean = kind == "" |
|
116 |
|
117 override def toString: String = |
114 override def toString: String = |
118 kind + |
115 kind + |
119 (if (load_command.isEmpty) "" else " (" + quote(load_command) + ")") + |
116 (if (load_command.isEmpty) "" else " (" + quote(load_command) + ")") + |
120 (if (tags.isEmpty) "" else tags.map(quote).mkString(" % ", " % ", "")) |
117 (if (tags.isEmpty) "" else tags.map(quote).mkString(" % ", " % ", "")) |
|
118 |
|
119 def map(f: String => String): Spec = |
|
120 copy(kind = f(kind), load_command = f(load_command), tags = tags.map(f)) |
121 } |
121 } |
122 |
122 |
123 object Keywords |
123 object Keywords |
124 { |
124 { |
125 def empty: Keywords = new Keywords() |
125 def empty: Keywords = new Keywords() |
185 } |
185 } |
186 |
186 |
187 def add_keywords(header: Thy_Header.Keywords): Keywords = |
187 def add_keywords(header: Thy_Header.Keywords): Keywords = |
188 (this /: header) { |
188 (this /: header) { |
189 case (keywords, (name, spec)) => |
189 case (keywords, (name, spec)) => |
190 if (spec.is_none) |
190 if (spec.kind.isEmpty) |
191 keywords + Symbol.decode(name) + Symbol.encode(name) |
191 keywords + Symbol.decode(name) + Symbol.encode(name) |
192 else |
192 else |
193 keywords + |
193 keywords + |
194 (Symbol.decode(name), spec.kind, spec.load_command) + |
194 (Symbol.decode(name), spec.kind, spec.load_command) + |
195 (Symbol.encode(name), spec.kind, spec.load_command) |
195 (Symbol.encode(name), spec.kind, spec.load_command) |