26 private val abbrevs_panel = new Abbrevs_Panel |
26 private val abbrevs_panel = new Abbrevs_Panel |
27 |
27 |
28 private val abbrevs_refresh_delay = |
28 private val abbrevs_refresh_delay = |
29 GUI_Thread.delay_last(PIDE.options.seconds("editor_update_delay")) { abbrevs_panel.refresh } |
29 GUI_Thread.delay_last(PIDE.options.seconds("editor_update_delay")) { abbrevs_panel.refresh } |
30 |
30 |
31 private class Abbrev_Component(val abbrev: (String, String)) extends Button |
31 private class Abbrev_Component(txt: String, abbrs: List[String]) extends Button |
32 { |
32 { |
33 text = Symbol.decode(abbrev._2) |
33 text = "<html>" + HTML.output(Symbol.decode(txt)) + "</html>" |
34 font = GUI.font(size = font_size) |
34 font = GUI.font(size = font_size) |
35 action = |
35 action = |
36 Action(text) { |
36 Action(text) { |
37 val text_area = view.getTextArea |
37 val text_area = view.getTextArea |
38 val (s1, s2) = Completion.split_template(text) |
38 val (s1, s2) = |
39 text_area.setSelectedText(Isabelle_Encoding.maybe_decode(text_area.getBuffer, s1 + s2)) |
39 Completion.split_template(Isabelle_Encoding.maybe_decode(text_area.getBuffer, txt)) |
|
40 text_area.setSelectedText(s1 + s2) |
40 text_area.moveCaretPosition(text_area.getCaretPosition - s2.length) |
41 text_area.moveCaretPosition(text_area.getCaretPosition - s2.length) |
41 text_area.requestFocus |
42 text_area.requestFocus |
42 } |
43 } |
43 tooltip = |
44 tooltip = GUI.tooltip_lines(cat_lines(txt :: abbrs.map(a => "abbrev: " + a))) |
44 GUI.tooltip_lines(cat_lines(List(abbrev._2, "abbrev: " + abbrev._1))) |
|
45 } |
45 } |
46 |
46 |
47 private class Abbrevs_Panel extends Wrap_Panel |
47 private class Abbrevs_Panel extends Wrap_Panel |
48 { |
48 { |
49 private var abbrevs: Thy_Header.Abbrevs = Nil |
49 private var abbrevs: Thy_Header.Abbrevs = Nil |
50 |
50 |
51 def refresh: Unit = GUI_Thread.require { |
51 def refresh: Unit = GUI_Thread.require { |
52 val abbrevs1 = |
52 val abbrevs1 = Isabelle.buffer_syntax(view.getBuffer).getOrElse(Outer_Syntax.empty).abbrevs |
53 Isabelle.buffer_syntax(view.getBuffer).getOrElse(Outer_Syntax.empty).abbrevs |
53 |
54 if (abbrevs != abbrevs1) { |
54 if (abbrevs != abbrevs1) { |
55 abbrevs = abbrevs1 |
55 abbrevs = abbrevs1 |
56 |
56 |
|
57 val entries: List[(String, List[String])] = |
|
58 Multi_Map( |
|
59 (for { |
|
60 (abbr, txt0) <- abbrevs |
|
61 val txt = Symbol.encode(txt0) |
|
62 if !Symbol.iterator(txt). |
|
63 forall(s => s.length == 1 && s(0) != Completion.caret_indicator) |
|
64 } yield (txt, abbr)): _*).iterator_list.toList |
|
65 |
57 contents.clear |
66 contents.clear |
58 for { |
67 for ((txt, abbrs) <- entries.sortBy(_._1)) |
59 abbrev <- abbrevs |
68 contents += new Abbrev_Component(txt, abbrs.filterNot(_ == "").sorted) |
60 if !Symbol.iterator(Symbol.encode(abbrev._2)). |
|
61 forall(s => s.length == 1 && s(0) != Completion.caret_indicator) |
|
62 } { contents += new Abbrev_Component(abbrev) } |
|
63 |
69 |
64 revalidate |
70 revalidate |
65 repaint |
71 repaint |
66 } |
72 } |
67 } |
73 } |