--- a/src/Pure/General/completion.scala Wed Sep 14 17:14:56 2016 +0200
+++ b/src/Pure/General/completion.scala Wed Sep 14 19:44:08 2016 +0200
@@ -387,23 +387,24 @@
(this /: abbrevs)(_.add_abbrev(_))
private def add_abbrev(abbrev: (String, String)): Completion =
- {
- val (abbr, text) = abbrev
- val rev_abbr = abbr.reverse
- val is_word = Completion.Word_Parsers.is_word(abbr)
+ abbrev match {
+ case ("", _) => this
+ case (abbr, text) =>
+ val rev_abbr = abbr.reverse
+ val is_word = Completion.Word_Parsers.is_word(abbr)
- val (words_lex1, words_map1) =
- if (!is_word) (words_lex, words_map)
- else if (text != "") (words_lex + abbr, words_map + abbrev)
- else (words_lex -- List(abbr), words_map - abbr)
+ val (words_lex1, words_map1) =
+ if (!is_word) (words_lex, words_map)
+ else if (text != "") (words_lex + abbr, words_map + abbrev)
+ else (words_lex -- List(abbr), words_map - abbr)
- val (abbrevs_lex1, abbrevs_map1) =
- if (is_word) (abbrevs_lex, abbrevs_map)
- else if (text != "") (abbrevs_lex + rev_abbr, abbrevs_map + (rev_abbr -> abbrev))
- else (abbrevs_lex -- List(rev_abbr), abbrevs_map - rev_abbr)
+ val (abbrevs_lex1, abbrevs_map1) =
+ if (is_word) (abbrevs_lex, abbrevs_map)
+ else if (text != "") (abbrevs_lex + rev_abbr, abbrevs_map + (rev_abbr -> abbrev))
+ else (abbrevs_lex -- List(rev_abbr), abbrevs_map - rev_abbr)
- new Completion(keywords, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1)
- }
+ new Completion(keywords, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1)
+ }
/* complete */
--- a/src/Tools/jEdit/src/symbols_dockable.scala Wed Sep 14 17:14:56 2016 +0200
+++ b/src/Tools/jEdit/src/symbols_dockable.scala Wed Sep 14 19:44:08 2016 +0200
@@ -28,20 +28,20 @@
private val abbrevs_refresh_delay =
GUI_Thread.delay_last(PIDE.options.seconds("editor_update_delay")) { abbrevs_panel.refresh }
- private class Abbrev_Component(val abbrev: (String, String)) extends Button
+ private class Abbrev_Component(txt: String, abbrs: List[String]) extends Button
{
- text = Symbol.decode(abbrev._2)
+ text = "<html>" + HTML.output(Symbol.decode(txt)) + "</html>"
font = GUI.font(size = font_size)
action =
Action(text) {
val text_area = view.getTextArea
- val (s1, s2) = Completion.split_template(text)
- text_area.setSelectedText(Isabelle_Encoding.maybe_decode(text_area.getBuffer, s1 + s2))
+ val (s1, s2) =
+ Completion.split_template(Isabelle_Encoding.maybe_decode(text_area.getBuffer, txt))
+ text_area.setSelectedText(s1 + s2)
text_area.moveCaretPosition(text_area.getCaretPosition - s2.length)
text_area.requestFocus
}
- tooltip =
- GUI.tooltip_lines(cat_lines(List(abbrev._2, "abbrev: " + abbrev._1)))
+ tooltip = GUI.tooltip_lines(cat_lines(txt :: abbrs.map(a => "abbrev: " + a)))
}
private class Abbrevs_Panel extends Wrap_Panel
@@ -49,17 +49,23 @@
private var abbrevs: Thy_Header.Abbrevs = Nil
def refresh: Unit = GUI_Thread.require {
- val abbrevs1 =
- Isabelle.buffer_syntax(view.getBuffer).getOrElse(Outer_Syntax.empty).abbrevs
+ val abbrevs1 = Isabelle.buffer_syntax(view.getBuffer).getOrElse(Outer_Syntax.empty).abbrevs
+
if (abbrevs != abbrevs1) {
abbrevs = abbrevs1
+ val entries: List[(String, List[String])] =
+ Multi_Map(
+ (for {
+ (abbr, txt0) <- abbrevs
+ val txt = Symbol.encode(txt0)
+ if !Symbol.iterator(txt).
+ forall(s => s.length == 1 && s(0) != Completion.caret_indicator)
+ } yield (txt, abbr)): _*).iterator_list.toList
+
contents.clear
- for {
- abbrev <- abbrevs
- if !Symbol.iterator(Symbol.encode(abbrev._2)).
- forall(s => s.length == 1 && s(0) != Completion.caret_indicator)
- } { contents += new Abbrev_Component(abbrev) }
+ for ((txt, abbrs) <- entries.sortBy(_._1))
+ contents += new Abbrev_Component(txt, abbrs.filterNot(_ == "").sorted)
revalidate
repaint