# HG changeset patch # User wenzelm # Date 1473875048 -7200 # Node ID 228a85f1d6aff34eaa3a4f68c9c4bc9e08fd82f4 # Parent 7dd5297d87fabc682da8e825d0e76713e12abf9e clarified GUI representation of replacement texts with zero or more abbrevs; diff -r 7dd5297d87fa -r 228a85f1d6af src/Pure/General/completion.scala --- 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 */ diff -r 7dd5297d87fa -r 228a85f1d6af src/Tools/jEdit/src/symbols_dockable.scala --- 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.output(Symbol.decode(txt)) + "" 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