# HG changeset patch
# User wenzelm
# Date 1473883631 -7200
# Node ID fd73c5dbaad2aaa280e7f8cd5ea3fe5ee05a922e
# Parent  159882dbb3391b18b243370afa7e91f15e963cbf# Parent  2683c3be36eb5d42e7c8a6672c0a54b0e2844e2a
merged

diff -r 159882dbb339 -r fd73c5dbaad2 NEWS
--- a/NEWS	Wed Sep 14 16:24:51 2016 +0200
+++ b/NEWS	Wed Sep 14 22:07:11 2016 +0200
@@ -79,6 +79,11 @@
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***
 
+* Dockable window "Symbols" also provides access to 'abbrevs' from the
+outer syntax of the current theory buffer. This provides clickable
+syntax templates, including entries with empty abbrevs name (which are
+inaccessible via keyboard completion).
+
 * Cartouche abbreviations work both for " and ` to accomodate typical
 situations where old ASCII notation may be updated.
 
@@ -146,10 +151,13 @@
 e.g. 'context', 'notepad'.
 
 * Additional abbreviations for syntactic completion may be specified
-within the theory header as 'abbrevs', in addition to global
-$ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs as
-before. The theory syntax for 'keywords' has been simplified
-accordingly: optional abbrevs need to go into the new 'abbrevs' section.
+within the theory header as 'abbrevs'. The theory syntax for 'keywords'
+has been simplified accordingly: optional abbrevs need to go into the
+new 'abbrevs' section.
+
+* Global abbreviations via $ISABELLE_HOME/etc/abbrevs and
+$ISABELLE_HOME_USER/etc/abbrevs are no longer supported. Minor
+INCOMPATIBILITY, use 'abbrevs' within theory header instead.
 
 * ML and document antiquotations for file-systems paths are more uniform
 and diverse:
diff -r 159882dbb339 -r fd73c5dbaad2 etc/abbrevs
--- a/etc/abbrevs	Wed Sep 14 16:24:51 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-(* additional abbreviations for syntactic completion *)
-
-(*prevent replacement of very long arrows*)
-"===>" = "===>"
-
-"--->" = "\<midarrow>\<rightarrow>"
diff -r 159882dbb339 -r fd73c5dbaad2 etc/settings
--- a/etc/settings	Wed Sep 14 16:24:51 2016 +0200
+++ b/etc/settings	Wed Sep 14 22:07:11 2016 +0200
@@ -121,11 +121,10 @@
 
 
 ###
-### Symbol rendering and abbreviations
+### Symbol rendering
 ###
 
 ISABELLE_SYMBOLS="$ISABELLE_HOME/etc/symbols:$ISABELLE_HOME_USER/etc/symbols"
-ISABELLE_ABBREVS="$ISABELLE_HOME/etc/abbrevs:$ISABELLE_HOME_USER/etc/abbrevs"
 
 
 ###
diff -r 159882dbb339 -r fd73c5dbaad2 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Wed Sep 14 16:24:51 2016 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Wed Sep 14 22:07:11 2016 +0200
@@ -1266,15 +1266,6 @@
   Backslash sequences also help when input is broken, and thus escapes its
   normal semantic context: e.g.\ antiquotations or string literals in ML,
   which do not allow arbitrary backslash sequences.
-
-  \<^medskip>
-  Additional abbreviations may be specified in \<^file>\<open>$ISABELLE_HOME/etc/abbrevs\<close>
-  and @{path "$ISABELLE_HOME_USER/etc/abbrevs"}. The file content follows
-  general Isar outer syntax @{cite "isabelle-isar-ref"}. Abbreviations are
-  specified as ``\<open>abbrev\<close>~\<^verbatim>\<open>=\<close>~\<open>text\<close>'' pairs. The replacement \<open>text\<close> may
-  consist of more than just one symbol; otherwise the meaning is the same as a
-  symbol specification ``\<open>sym\<close>~\<^verbatim>\<open>abbrev:\<close>~\<open>abbrev\<close>'' within @{path
-  "etc/symbols"}.
 \<close>
 
 
diff -r 159882dbb339 -r fd73c5dbaad2 src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Wed Sep 14 16:24:51 2016 +0200
+++ b/src/Pure/GUI/gui.scala	Wed Sep 14 22:07:11 2016 +0200
@@ -211,6 +211,21 @@
       case _ => None
     }
 
+  def traverse_components(component: Component, apply: Component => Unit)
+  {
+    def traverse(comp: Component)
+    {
+      apply(comp)
+      comp match {
+        case cont: Container =>
+          for (i <- 0 until cont.getComponentCount)
+            traverse(cont.getComponent(i))
+        case _ =>
+      }
+    }
+    traverse(component)
+  }
+
 
   /* font operations */
 
diff -r 159882dbb339 -r fd73c5dbaad2 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Wed Sep 14 16:24:51 2016 +0200
+++ b/src/Pure/General/completion.scala	Wed Sep 14 22:07:11 2016 +0200
@@ -246,7 +246,8 @@
   /* init */
 
   val empty: Completion = new Completion()
-  def init(): Completion = empty.load()
+  def init(): Completion =
+    empty.add_symbols.add_abbrevs(Completion.symbol_abbrevs ::: Completion.default_abbrevs)
 
 
   /* word parsers */
@@ -295,41 +296,22 @@
   }
 
 
+  /* templates */
+
+  val caret_indicator = '\u0007'
+
+  def split_template(s: String): (String, String) =
+    space_explode(caret_indicator, s) match {
+      case List(s1, s2) => (s1, s2)
+      case _ => (s, "")
+    }
+
+
   /* abbreviations */
 
-  private object Abbrevs_Parser extends Parse.Parser
-  {
-    private val syntax = Outer_Syntax.empty + "="
-
-    private val entry: Parser[(String, String)] =
-      text ~ ($$$("=") ~! text) ^^ { case a ~ (_ ~ b) => (a, b) }
-
-    def parse_file(file: Path): List[(String, String)] =
-    {
-      val toks = Token.explode(syntax.keywords, File.read(file))
-      parse_all(rep(entry), Token.reader(toks, Token.Pos.file(file.implode))) match {
-        case Success(result, _) => result
-        case bad => error(bad.toString)
-      }
-    }
-  }
+  private def symbol_abbrevs: Thy_Header.Abbrevs =
+    for ((sym, abbr) <- Symbol.abbrevs.toList) yield (abbr, sym)
 
-  def load_abbrevs(): List[(String, String)] =
-  {
-    val symbol_abbrevs =
-      for ((sym, abbr) <- Symbol.abbrevs.toList) yield (abbr, sym)
-    val more_abbrevs =
-      for {
-        path <- Path.split(Isabelle_System.getenv("ISABELLE_ABBREVS"))
-        if path.is_file
-        entry <- Abbrevs_Parser.parse_file(path)
-      } yield entry
-    val remove_abbrevs = (for { (a, b) <- more_abbrevs if b == "" } yield a).toSet
-
-    (symbol_abbrevs ::: more_abbrevs).filterNot({ case (a, _) => remove_abbrevs.contains(a) })
-  }
-
-  private val caret_indicator = '\u0007'
   private val antiquote = "@{"
 
   private val default_abbrevs =
@@ -387,7 +369,7 @@
 
   /* symbols and abbrevs */
 
-  def add_symbols(): Completion =
+  def add_symbols: Completion =
   {
     val words =
       (for ((sym, _) <- Symbol.names.toList) yield (sym, sym)) :::
@@ -405,26 +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)
-
-    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)
+    abbrev match {
+      case ("", _) => this
+      case (abbr, text) =>
+        val rev_abbr = abbr.reverse
+        val is_word = Completion.Word_Parsers.is_word(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 (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)
 
-    new Completion(keywords, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1)
-  }
+        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)
 
-  private def load(): Completion =
-    add_symbols().add_abbrevs(Completion.load_abbrevs() ::: Completion.default_abbrevs)
+        new Completion(keywords, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1)
+    }
 
 
   /* complete */
@@ -505,11 +485,7 @@
             (complete_word, name0) <- completions
             name1 = decode(name0)
             if name1 != original
-            (s1, s2) =
-              space_explode(Completion.caret_indicator, name1) match {
-                case List(s1, s2) => (s1, s2)
-                case _ => (name1, "")
-              }
+            (s1, s2) = Completion.split_template(name1)
             move = - s2.length
             description =
               if (is_symbol(name0)) {
diff -r 159882dbb339 -r fd73c5dbaad2 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Wed Sep 14 16:24:51 2016 +0200
+++ b/src/Pure/General/path.scala	Wed Sep 14 22:07:11 2016 +0200
@@ -96,7 +96,7 @@
       else (List(root_elem(es.head)), es.tail)
     val elems = raw_elems.filterNot(s => s.isEmpty || s == ".").map(explode_elem)
 
-    new Path(norm_elems(elems.reverse ::: roots))
+    new Path(norm_elems(elems reverse_::: roots))
   }
 
   def is_wellformed(str: String): Boolean =
diff -r 159882dbb339 -r fd73c5dbaad2 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Wed Sep 14 16:24:51 2016 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Wed Sep 14 22:07:11 2016 +0200
@@ -46,6 +46,7 @@
 final class Outer_Syntax private(
   val keywords: Keyword.Keywords = Keyword.Keywords.empty,
   val completion: Completion = Completion.empty,
+  val rev_abbrevs: Thy_Header.Abbrevs = Nil,
   val language_context: Completion.Language_Context = Completion.Language_Context.outer,
   val has_tokens: Boolean = true)
 {
@@ -54,7 +55,7 @@
   override def toString: String = keywords.toString
 
 
-  /* add keywords */
+  /* keywords */
 
   def + (name: String, kind: String = "", tags: List[String] = Nil): Outer_Syntax =
   {
@@ -65,7 +66,7 @@
           (if (Keyword.theory_block.contains(kind)) List((name, name + "\nbegin\n\u0007\nend"))
            else Nil) :::
           (if (Completion.Word_Parsers.is_word(name)) List((name, name)) else Nil))
-    new Outer_Syntax(keywords1, completion1, language_context, true)
+    new Outer_Syntax(keywords1, completion1, rev_abbrevs, language_context, true)
   }
 
   def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
@@ -74,18 +75,24 @@
         syntax + (Symbol.decode(name), kind, tags) + (Symbol.encode(name), kind, tags)
     }
 
-  def add_abbrevs(abbrevs: Thy_Header.Abbrevs): Outer_Syntax =
-    if (abbrevs.isEmpty) this
+
+  /* abbrevs */
+
+  def abbrevs: Thy_Header.Abbrevs = rev_abbrevs.reverse
+
+  def add_abbrevs(new_abbrevs: Thy_Header.Abbrevs): Outer_Syntax =
+    if (new_abbrevs.isEmpty) this
     else {
       val completion1 =
         completion.add_abbrevs(
-          (for ((a, b) <- abbrevs) yield {
+          (for ((a, b) <- new_abbrevs) yield {
             val a1 = Symbol.decode(a)
             val a2 = Symbol.encode(a)
             val b1 = Symbol.decode(b)
             List((a1, b1), (a2, b1))
           }).flatten)
-      new Outer_Syntax(keywords, completion1, language_context, has_tokens)
+      val rev_abbrevs1 = Library.distinct(new_abbrevs) reverse_::: rev_abbrevs
+      new Outer_Syntax(keywords, completion1, rev_abbrevs1, language_context, has_tokens)
     }
 
 
@@ -94,10 +101,11 @@
   def ++ (other: Outer_Syntax): Outer_Syntax =
     if (this eq other) this
     else {
-      val keywords1 = keywords ++ other.asInstanceOf[Outer_Syntax].keywords
-      val completion1 = completion ++ other.asInstanceOf[Outer_Syntax].completion
+      val keywords1 = keywords ++ other.keywords
+      val completion1 = completion ++ other.completion
+      val rev_abbrevs1 = Library.merge(rev_abbrevs, other.rev_abbrevs)
       if ((keywords eq keywords1) && (completion eq completion1)) this
-      else new Outer_Syntax(keywords1, completion1, language_context, has_tokens)
+      else new Outer_Syntax(keywords1, completion1, rev_abbrevs1, language_context, has_tokens)
     }
 
 
@@ -110,13 +118,14 @@
   /* language context */
 
   def set_language_context(context: Completion.Language_Context): Outer_Syntax =
-    new Outer_Syntax(keywords, completion, context, has_tokens)
+    new Outer_Syntax(keywords, completion, rev_abbrevs, context, has_tokens)
 
   def no_tokens: Outer_Syntax =
   {
     require(keywords.is_empty)
     new Outer_Syntax(
       completion = completion,
+      rev_abbrevs = rev_abbrevs,
       language_context = language_context,
       has_tokens = false)
   }
diff -r 159882dbb339 -r fd73c5dbaad2 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Wed Sep 14 16:24:51 2016 +0200
+++ b/src/Pure/Pure.thy	Wed Sep 14 22:07:11 2016 +0200
@@ -92,6 +92,8 @@
   and "find_theorems" "find_consts" :: diag
   and "named_theorems" :: thy_decl
 abbrevs
+  "===>" = "===>"  (*prevent replacement of very long arrows*)
+  "--->" = "\<midarrow>\<rightarrow>"
   "default_sort" = ""
   "simproc_setup" = ""
   "hence" = ""
diff -r 159882dbb339 -r fd73c5dbaad2 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Wed Sep 14 16:24:51 2016 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Wed Sep 14 22:07:11 2016 +0200
@@ -198,7 +198,7 @@
     val removed = old_cmds.iterator.filter(!new_cmds.contains(_)).toList
     val inserted = new_cmds.iterator.filter(!old_cmds.contains(_)).toList
 
-    removed.reverse.map(cmd => (old_cmds.prev(cmd), None)) :::
+    removed.map(cmd => (old_cmds.prev(cmd), None)) reverse_:::
     inserted.map(cmd => (new_cmds.prev(cmd), Some(cmd)))
   }
 
diff -r 159882dbb339 -r fd73c5dbaad2 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Sep 14 16:24:51 2016 +0200
+++ b/src/Pure/Tools/build.scala	Wed Sep 14 22:07:11 2016 +0200
@@ -170,7 +170,7 @@
 
             val loaded_theories = thy_deps.loaded_theories
             val keywords = thy_deps.keywords
-            val syntax = thy_deps.syntax.asInstanceOf[Outer_Syntax]
+            val syntax = thy_deps.syntax
 
             val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
             val loaded_files =
diff -r 159882dbb339 -r fd73c5dbaad2 src/Pure/library.scala
--- a/src/Pure/library.scala	Wed Sep 14 16:24:51 2016 +0200
+++ b/src/Pure/library.scala	Wed Sep 14 22:07:11 2016 +0200
@@ -198,6 +198,11 @@
   def remove[A, B](x: B)(xs: List[A]): List[A] = if (member(xs)(x)) xs.filterNot(_ == x) else xs
   def update[A](x: A)(xs: List[A]): List[A] = x :: remove(x)(xs)
 
+  def merge[A](xs: List[A], ys: List[A]): List[A] =
+    if (xs.eq(ys)) xs
+    else if (xs.isEmpty) ys
+    else ys.foldRight(xs)(Library.insert(_)(_))
+
   def distinct[A](xs: List[A]): List[A] =
   {
     val result = new mutable.ListBuffer[A]
diff -r 159882dbb339 -r fd73c5dbaad2 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Wed Sep 14 16:24:51 2016 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Wed Sep 14 22:07:11 2016 +0200
@@ -50,7 +50,7 @@
 
   def mode_syntax(mode: String): Option[Outer_Syntax] =
     mode match {
-      case "isabelle" => Some(PIDE.resources.base_syntax.asInstanceOf[Outer_Syntax])
+      case "isabelle" => Some(PIDE.resources.base_syntax)
       case "isabelle-options" => Some(Options.options_syntax)
       case "isabelle-root" => Some(Sessions.root_syntax)
       case "isabelle-ml" => Some(ml_syntax)
@@ -61,11 +61,13 @@
     }
 
   def buffer_syntax(buffer: JEditBuffer): Option[Outer_Syntax] =
-    (JEdit_Lib.buffer_mode(buffer), PIDE.document_model(buffer)) match {
-      case ("isabelle", Some(model)) =>
-        Some(PIDE.session.recent_syntax(model.node_name).asInstanceOf[Outer_Syntax])
-      case (mode, _) => mode_syntax(mode)
-    }
+    if (buffer == null) None
+    else
+      (JEdit_Lib.buffer_mode(buffer), PIDE.document_model(buffer)) match {
+        case ("isabelle", Some(model)) =>
+          Some(PIDE.session.recent_syntax(model.node_name))
+        case (mode, _) => mode_syntax(mode)
+      }
 
 
   /* token markers */
diff -r 159882dbb339 -r fd73c5dbaad2 src/Tools/jEdit/src/symbols_dockable.scala
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Wed Sep 14 16:24:51 2016 +0200
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Wed Sep 14 22:07:11 2016 +0200
@@ -10,22 +10,89 @@
 import isabelle._
 
 import scala.swing.event.{SelectionChanged, ValueChanged}
-import scala.swing.{Action, Button, TabbedPane, TextField, BorderPanel, Label, ScrollPane}
+import scala.swing.{Component, Action, Button, TabbedPane, TextField, BorderPanel,
+  Label, ScrollPane}
 
-import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.{EditBus, EBComponent, EBMessage, View}
 
 
 class Symbols_Dockable(view: View, position: String) extends Dockable(view, position)
 {
+  private def font_size: Int =
+    Font_Info.main_size(PIDE.options.real("jedit_font_scale")).round
+
+
+  /* abbreviations */
+
+  private val abbrevs_panel = new Abbrevs_Panel
+
+  private val abbrevs_refresh_delay =
+    GUI_Thread.delay_last(PIDE.options.seconds("editor_update_delay")) { abbrevs_panel.refresh }
+
+  private class Abbrev_Component(txt: String, abbrs: List[String]) extends Button
+  {
+    def update_font { font = GUI.font(size = font_size) }
+    update_font
+
+    text = "<html>" + HTML.output(Symbol.decode(txt)) + "</html>"
+    action =
+      Action(text) {
+        val text_area = view.getTextArea
+        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(txt :: abbrs.map(a => "abbrev: " + a)))
+  }
+
+  private class Abbrevs_Panel extends Wrap_Panel
+  {
+    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
+
+      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 ((txt, abbrs) <- entries.sortBy(_._1))
+          contents += new Abbrev_Component(txt, abbrs.filterNot(_ == "").sorted)
+
+        revalidate
+        repaint
+      }
+    }
+
+    refresh
+  }
+
+
+  /* symbols */
+
   private class Symbol_Component(val symbol: String, is_control: Boolean) extends Button
   {
-    private val font_size = Font_Info.main_size(PIDE.options.real("jedit_font_scale")).round
+    def update_font
+    {
+      font =
+        Symbol.fonts.get(symbol) match {
+          case None => GUI.font(size = font_size)
+          case Some(font_family) => GUI.font(family = font_family, size = font_size)
+        }
+    }
+    update_font
 
-    font =
-      Symbol.fonts.get(symbol) match {
-        case None => GUI.font(size = font_size)
-        case Some(font_family) => GUI.font(family = font_family, size = font_size)
-      }
     action =
       Action(Symbol.decode(symbol)) {
         val text_area = view.getTextArea
@@ -50,7 +117,12 @@
     tooltip = "Reset control symbols within text"
   }
 
+
+  /* tabs */
+
   private val group_tabs: TabbedPane = new TabbedPane {
+    pages += new TabbedPane.Page("abbrevs", abbrevs_panel)
+
     pages ++=
       Symbol.groups.map({ case (group, symbols) =>
         new TabbedPane.Page(group,
@@ -67,7 +139,7 @@
         val results_panel = new Wrap_Panel
         layout(search_field) = BorderPanel.Position.North
         layout(new ScrollPane(results_panel)) = BorderPanel.Position.Center
-  
+
         val search_space =
           (for (sym <- Symbol.names.keysIterator) yield (sym, Word.lowercase(sym))).toList
         val search_delay =
@@ -99,4 +171,46 @@
       page.title = Word.implode(Word.explode('_', page.title).map(Word.perhaps_capitalize(_)))
   }
   set_content(group_tabs)
+
+
+
+  /* main */
+
+  private val edit_bus_handler: EBComponent =
+    new EBComponent { def handleMessage(msg: EBMessage) { abbrevs_refresh_delay.invoke() } }
+
+  private val main =
+    Session.Consumer[Any](getClass.getName) {
+      case _: Session.Global_Options =>
+        GUI_Thread.later {
+          val comp = group_tabs.peer
+          GUI.traverse_components(comp,
+            {
+              case c0: javax.swing.JComponent =>
+                Component.wrap(c0) match {
+                  case c: Abbrev_Component => c.update_font
+                  case c: Symbol_Component => c.update_font
+                  case _ =>
+                }
+              case _ =>
+            })
+          comp.revalidate
+          comp.repaint()
+        }
+      case _: Session.Commands_Changed => abbrevs_refresh_delay.invoke()
+    }
+
+  override def init()
+  {
+    EditBus.addToBus(edit_bus_handler)
+    PIDE.session.global_options += main
+    PIDE.session.commands_changed += main
+  }
+
+  override def exit()
+  {
+    EditBus.removeFromBus(edit_bus_handler)
+    PIDE.session.global_options -= main
+    PIDE.session.commands_changed -= main
+  }
 }