equal
deleted
inserted
replaced
73 } |
73 } |
74 |
74 |
75 val list = new java.util.LinkedList[String] |
75 val list = new java.util.LinkedList[String] |
76 val descriptions = new java.util.LinkedList[String] |
76 val descriptions = new java.util.LinkedList[String] |
77 // compute suggestions |
77 // compute suggestions |
78 val (suggs,text) = suggestions(1) |
78 val (suggs, text) = suggestions(1) |
79 for(s <- suggs) { |
79 for(s <- suggs) { |
80 val decoded = Isabelle.symbols.decode(s) |
80 val decoded = Isabelle.symbols.decode(s) |
81 list.add(decoded) |
81 list.add(decoded) |
82 if(!decoded.equals(s)) descriptions.add(s) else descriptions.add(null) |
82 if(decoded != s) descriptions.add(s) else descriptions.add(null) |
83 } |
83 } |
84 return new IsabelleSideKickCompletion(pane.getView, text, list, descriptions) |
84 return new IsabelleSideKickCompletion(pane.getView, text, list, descriptions) |
85 } else return null |
85 } else return null |
86 } |
86 } |
87 |
87 |