129 |
129 |
130 |
130 |
131 |
131 |
132 /** semantic completion **/ |
132 /** semantic completion **/ |
133 |
133 |
134 object Names |
134 object Semantic |
135 { |
135 { |
136 object Info |
136 object Info |
137 { |
137 { |
138 def unapply(info: Text.Markup): Option[Names] = |
138 def unapply(info: Text.Markup): Option[Text.Info[Semantic]] = |
139 info.info match { |
139 info.info match { |
140 case XML.Elem(Markup(Markup.COMPLETION, _), body) => |
140 case XML.Elem(Markup(Markup.COMPLETION, _), body) => |
141 try { |
141 try { |
142 val (total, names) = |
142 val (total, names) = |
143 { |
143 { |
144 import XML.Decode._ |
144 import XML.Decode._ |
145 pair(int, list(pair(string, pair(string, string))))(body) |
145 pair(int, list(pair(string, pair(string, string))))(body) |
146 } |
146 } |
147 Some(Names(info.range, total, names)) |
147 Some(Text.Info(info.range, Names(total, names))) |
148 } |
148 } |
149 catch { case _: XML.Error => None } |
149 catch { case _: XML.Error => None } |
150 case XML.Elem(Markup(Markup.NO_COMPLETION, _), _) => |
150 case XML.Elem(Markup(Markup.NO_COMPLETION, _), _) => |
151 Some(Names(info.range, 0, Nil)) |
151 Some(Text.Info(info.range, No_Completion)) |
152 case _ => None |
152 case _ => None |
153 } |
153 } |
154 } |
154 } |
155 } |
155 } |
156 |
156 |
157 sealed case class Names( |
157 sealed abstract class Semantic |
158 range: Text.Range, total: Int, names: List[(String, (String, String))]) |
158 { |
159 { |
159 def no_completion: Boolean = this == No_Completion |
160 def no_completion: Boolean = total == 0 && names.isEmpty |
|
161 |
|
162 def complete( |
160 def complete( |
|
161 range: Text.Range, |
|
162 history: Completion.History, |
|
163 do_decode: Boolean, |
|
164 original: String): Option[Completion.Result] = None |
|
165 } |
|
166 case object No_Completion extends Semantic |
|
167 case class Names( |
|
168 total: Int, |
|
169 names: List[(String, (String, String))]) extends Semantic |
|
170 { |
|
171 override def complete( |
|
172 range: Text.Range, |
163 history: Completion.History, |
173 history: Completion.History, |
164 do_decode: Boolean, |
174 do_decode: Boolean, |
165 original: String): Option[Completion.Result] = |
175 original: String): Option[Completion.Result] = |
166 { |
176 { |
167 def decode(s: String): String = if (do_decode) Symbol.decode(s) else s |
177 def decode(s: String): String = if (do_decode) Symbol.decode(s) else s |