equal
deleted
inserted
replaced
94 completion.complete(text) match { |
94 completion.complete(text) match { |
95 case None => null |
95 case None => null |
96 case Some((word, cs)) => |
96 case Some((word, cs)) => |
97 val ds = |
97 val ds = |
98 (if (Isabelle_Encoding.is_active(buffer)) |
98 (if (Isabelle_Encoding.is_active(buffer)) |
99 cs.map(Isabelle_System.symbols.decode(_)).sortWith(_ < _) |
99 cs.map(Symbol.decode(_)).sortWith(_ < _) |
100 else cs).filter(_ != word) |
100 else cs).filter(_ != word) |
101 if (ds.isEmpty) null |
101 if (ds.isEmpty) null |
102 else new SideKickCompletion( |
102 else new SideKickCompletion( |
103 pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { } |
103 pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { } |
104 } |
104 } |