83 override def toString: String = keywords.toString |
83 override def toString: String = keywords.toString |
84 |
84 |
85 |
85 |
86 /* add keywords */ |
86 /* add keywords */ |
87 |
87 |
88 def + (name: String): Outer_Syntax = this + (name, None, None) |
88 def + (name: String, kind: String = "", tags: List[String] = Nil, replace: Option[String] = None) |
89 def + (name: String, kind: String): Outer_Syntax = this + (name, Some((kind, Nil)), None) |
|
90 def + (name: String, opt_kind: Option[(String, List[String])], replace: Option[String]) |
|
91 : Outer_Syntax = |
89 : Outer_Syntax = |
92 { |
90 { |
93 val keywords1 = |
91 val keywords1 = keywords + (name, kind, tags) |
94 opt_kind match { |
|
95 case None => keywords + name |
|
96 case Some(kind) => keywords + (name, kind) |
|
97 } |
|
98 val completion1 = |
92 val completion1 = |
99 if (replace == Some("")) completion |
93 if (replace == Some("")) completion |
100 else completion + (name, replace getOrElse name) |
94 else completion + (name, replace getOrElse name) |
101 new Outer_Syntax(keywords1, completion1, language_context, true) |
95 new Outer_Syntax(keywords1, completion1, language_context, true) |
102 } |
96 } |
103 |
97 |
104 def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax = |
98 def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax = |
105 (this /: keywords) { |
99 (this /: keywords) { |
106 case (syntax, (name, opt_spec, replace)) => |
100 case (syntax, (name, ((kind, tags), _), replace)) => |
107 val opt_kind = opt_spec.map(_._1) |
|
108 syntax + |
101 syntax + |
109 (Symbol.decode(name), opt_kind, replace) + |
102 (Symbol.decode(name), kind, tags, replace) + |
110 (Symbol.encode(name), opt_kind, replace) |
103 (Symbol.encode(name), kind, tags, replace) |
111 } |
104 } |
112 |
105 |
113 |
106 |
114 /* merge */ |
107 /* merge */ |
115 |
108 |