47 if (position == DockableWindowManager.FLOATING) |
47 if (position == DockableWindowManager.FLOATING) |
48 setPreferredSize(new Dimension(1000, 500)) |
48 setPreferredSize(new Dimension(1000, 500)) |
49 |
49 |
50 val doc = pane.getDocument.asInstanceOf[StyledDocument] |
50 val doc = pane.getDocument.asInstanceOf[StyledDocument] |
51 |
51 |
52 def makeStyle(name: String, bg: Boolean, color: Color) = { |
52 def make_style(name: String, bg: Boolean, color: Color) = { |
53 val style = doc.addStyle(name, null) |
53 val style = doc.addStyle(name, null) |
54 if (bg) StyleConstants.setBackground(style, color) |
54 if (bg) StyleConstants.setBackground(style, color) |
55 else StyleConstants.setForeground(style, color) |
55 else StyleConstants.setForeground(style, color) |
56 style |
56 style |
57 } |
57 } |
58 val rawStyle = makeStyle("raw", false, Color.GRAY) |
58 val raw_style = make_style("raw", false, Color.GRAY) |
59 val infoStyle = makeStyle("info", true, new Color(160, 255, 160)) |
59 val info_style = make_style("info", true, new Color(160, 255, 160)) |
60 val warningStyle = makeStyle("warning", true, new Color(255, 255, 160)) |
60 val warning_style = make_style("warning", true, new Color(255, 255, 160)) |
61 val errorStyle = makeStyle("error", true, new Color(255, 160, 160)) |
61 val error_style = make_style("error", true, new Color(255, 160, 160)) |
62 |
62 |
63 IsabellePlugin.addPermanentConsumer (result => |
63 IsabellePlugin.add_permanent_consumer (result => |
64 if (result != null && !result.is_system) { |
64 if (result != null && !result.is_system) { |
65 SwingUtilities.invokeLater(new Runnable { |
65 SwingUtilities.invokeLater(new Runnable { |
66 def run = { |
66 def run = { |
67 val logic = IsabellePlugin.isabelle.session |
67 val logic = IsabellePlugin.isabelle.session |
68 logicCombo.setModel(new DefaultComboBoxModel(Array(logic).asInstanceOf[Array[AnyRef]])) |
68 logic_combo.setModel(new DefaultComboBoxModel(Array(logic).asInstanceOf[Array[AnyRef]])) |
69 logicCombo.setPrototypeDisplayValue("AAAA") // FIXME ?? |
69 logic_combo.setPrototypeDisplayValue("AAAA") // FIXME ?? |
70 |
70 |
71 val doc = pane.getDocument.asInstanceOf[StyledDocument] |
71 val doc = pane.getDocument.asInstanceOf[StyledDocument] |
72 val style = result.kind match { |
72 val style = result.kind match { |
73 case IsabelleProcess.Kind.WARNING => warningStyle |
73 case IsabelleProcess.Kind.WARNING => warning_style |
74 case IsabelleProcess.Kind.ERROR => errorStyle |
74 case IsabelleProcess.Kind.ERROR => error_style |
75 case IsabelleProcess.Kind.TRACING => infoStyle |
75 case IsabelleProcess.Kind.TRACING => info_style |
76 case _ => if (result.is_raw) rawStyle else null |
76 case _ => if (result.is_raw) raw_style else null |
77 } |
77 } |
78 doc.insertString(doc.getLength, IsabellePlugin.result_content(result), style) |
78 doc.insertString(doc.getLength, IsabellePlugin.result_content(result), style) |
79 if (!result.is_raw) doc.insertString(doc.getLength, "\n", style) |
79 if (!result.is_raw) doc.insertString(doc.getLength, "\n", style) |
80 pane.setCaretPosition(doc.getLength) |
80 pane.setCaretPosition(doc.getLength) |
81 } |
81 } |
87 val box = new Box(BoxLayout.X_AXIS) |
87 val box = new Box(BoxLayout.X_AXIS) |
88 add(BorderLayout.SOUTH, box) |
88 add(BorderLayout.SOUTH, box) |
89 |
89 |
90 |
90 |
91 // logic combo |
91 // logic combo |
92 logicCombo.setToolTipText("Isabelle logics") |
92 logic_combo.setToolTipText("Isabelle logics") |
93 logicCombo.setRequestFocusEnabled(false) |
93 logic_combo.setRequestFocusEnabled(false) |
94 logicCombo.setModel(new DefaultComboBoxModel(Array("default").asInstanceOf[Array[AnyRef]])) |
94 logic_combo.setModel(new DefaultComboBoxModel(Array("default").asInstanceOf[Array[AnyRef]])) |
95 box.add(logicCombo) |
95 box.add(logic_combo) |
96 |
96 |
97 |
97 |
98 // mode combo |
98 // mode combo |
99 val modeIsar = "Isar" |
99 val mode_Isar = "Isar" |
100 val modeML = "ML" |
100 val mode_ML = "ML" |
101 val modes = Array(modeIsar, modeML) |
101 val modes = Array(mode_Isar, mode_ML) |
102 var mode = modeIsar |
102 var mode = mode_Isar |
103 |
103 |
104 val modeCombo = new JComboBox |
104 val mode_combo = new JComboBox |
105 modeCombo.setToolTipText("Toplevel mode") |
105 mode_combo.setToolTipText("Toplevel mode") |
106 modeCombo.setRequestFocusEnabled(false) |
106 mode_combo.setRequestFocusEnabled(false) |
107 modeCombo.setModel(new DefaultComboBoxModel(modes.asInstanceOf[Array[AnyRef]])) |
107 mode_combo.setModel(new DefaultComboBoxModel(modes.asInstanceOf[Array[AnyRef]])) |
108 modeCombo.setPrototypeDisplayValue("AAAA") |
108 mode_combo.setPrototypeDisplayValue("AAAA") |
109 modeCombo.addActionListener(new ActionListener { |
109 mode_combo.addActionListener(new ActionListener { |
110 def actionPerformed(evt: ActionEvent): Unit = { |
110 def actionPerformed(evt: ActionEvent): Unit = { |
111 mode = modeCombo.getSelectedItem.asInstanceOf[String] |
111 mode = mode_combo.getSelectedItem.asInstanceOf[String] |
112 } |
112 } |
113 }) |
113 }) |
114 box.add(modeCombo) |
114 box.add(mode_combo) |
115 |
115 |
116 |
116 |
117 // input field |
117 // input field |
118 text.setToolTipText("Command line") |
118 text.setToolTipText("Command line") |
119 text.addActionListener(new ActionListener { |
119 text.addActionListener(new ActionListener { |
120 def actionPerformed(evt: ActionEvent): Unit = { |
120 def actionPerformed(evt: ActionEvent): Unit = { |
121 val command = text.getText |
121 val command = text.getText |
122 if (command.length > 0) { |
122 if (command.length > 0) { |
123 if (mode == modeIsar) |
123 if (mode == mode_Isar) |
124 IsabellePlugin.isabelle.command(command) |
124 IsabellePlugin.isabelle.command(command) |
125 else if (mode == modeML) |
125 else if (mode == mode_ML) |
126 IsabellePlugin.isabelle.ML(command) |
126 IsabellePlugin.isabelle.ML(command) |
127 text.setText("") |
127 text.setText("") |
128 } |
128 } |
129 } |
129 } |
130 }) |
130 }) |