equal
deleted
inserted
replaced
37 Markup.ERROR_MESSAGE -> error_pri) |
37 Markup.ERROR_MESSAGE -> error_pri) |
38 |
38 |
39 |
39 |
40 /* markup elements */ |
40 /* markup elements */ |
41 |
41 |
|
42 private val semantic_completion_elements = |
|
43 Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION) |
|
44 |
42 private val tooltip_descriptions = |
45 private val tooltip_descriptions = |
43 Map( |
46 Map( |
44 Markup.CITATION -> "citation", |
47 Markup.CITATION -> "citation", |
45 Markup.TOKEN_RANGE -> "inner syntax token", |
48 Markup.TOKEN_RANGE -> "inner syntax token", |
46 Markup.FREE -> "free variable", |
49 Markup.FREE -> "free variable", |
66 val snapshot: Document.Snapshot, |
69 val snapshot: Document.Snapshot, |
67 val options: Options, |
70 val options: Options, |
68 val resources: Resources) |
71 val resources: Resources) |
69 { |
72 { |
70 override def toString: String = "Rendering(" + snapshot.toString + ")" |
73 override def toString: String = "Rendering(" + snapshot.toString + ")" |
|
74 |
|
75 |
|
76 /* completion */ |
|
77 |
|
78 def semantic_completion(completed_range: Option[Text.Range], range: Text.Range) |
|
79 : Option[Text.Info[Completion.Semantic]] = |
|
80 if (snapshot.is_outdated) None |
|
81 else { |
|
82 snapshot.select(range, Rendering.semantic_completion_elements, _ => |
|
83 { |
|
84 case Completion.Semantic.Info(info) => |
|
85 completed_range match { |
|
86 case Some(range0) if range0.contains(info.range) && range0 != info.range => None |
|
87 case _ => Some(info) |
|
88 } |
|
89 case _ => None |
|
90 }).headOption.map(_.info) |
|
91 } |
71 |
92 |
72 |
93 |
73 /* tooltips */ |
94 /* tooltips */ |
74 |
95 |
75 def tooltip_margin: Int |
96 def tooltip_margin: Int |