OpenDolphin日記

スタンプ箱で，項目を選択した状態でスタンプメーカーを起動しても，左矢印が有効にならない。client/StanpBoxPlugin.java の editors.show の後に，スタンプ選択の変更をでっち上げて，EditorsSetPanel の valueChange に処理がわたるようにして対応。

javax.swing.tree.TreePath tp = tree.getSelectionPath();
tree.clearSelection();
tree.setSelectionPath(tp);