54 } |
54 } |
55 tooltip = "Reset control symbols within text" |
55 tooltip = "Reset control symbols within text" |
56 } |
56 } |
57 |
57 |
58 val group_tabs: TabbedPane = new TabbedPane { |
58 val group_tabs: TabbedPane = new TabbedPane { |
59 pages ++= (for ((group, symbols) <- Symbol.groups) yield |
59 pages ++= |
60 { |
60 Symbol.groups map { case (group, symbols) => |
61 new TabbedPane.Page(group, |
61 new TabbedPane.Page(group, |
62 new FlowPanel { |
62 new FlowPanel { |
63 contents ++= symbols.map(new Symbol_Component(_)) |
63 contents ++= symbols.map(new Symbol_Component(_)) |
64 if (group == "control") contents += new Reset_Component |
64 if (group == "control") contents += new Reset_Component |
65 }, null) |
65 }, null) |
66 }).toList.sortWith(_.title <= _.title) |
66 } |
67 pages += new TabbedPane.Page("search", new BorderPanel { |
67 pages += new TabbedPane.Page("search", new BorderPanel { |
68 val search = new TextField(10) |
68 val search = new TextField(10) |
69 val results_panel = new FlowPanel |
69 val results_panel = new FlowPanel |
70 add(search, BorderPanel.Position.North) |
70 add(search, BorderPanel.Position.North) |
71 add(results_panel, BorderPanel.Position.Center) |
71 add(results_panel, BorderPanel.Position.Center) |