# HG changeset patch # User wenzelm # Date 1219598667 -7200 # Node ID efc6d38d16d2d35680c1410efe50f5e6cd121652 # Parent c3f7fa72af2ad40d03a09b2ae89d092f619f87b0 misc tuning of names; diff -r c3f7fa72af2a -r efc6d38d16d2 lib/jedit/plugin/isabelle_dock.scala --- a/lib/jedit/plugin/isabelle_dock.scala Sun Aug 24 19:02:22 2008 +0200 +++ b/lib/jedit/plugin/isabelle_dock.scala Sun Aug 24 19:24:27 2008 +0200 @@ -37,7 +37,7 @@ extends JPanel(new BorderLayout) with DefaultFocusComponent { private val text = new HistoryTextField("isabelle", false, true) - private val logicCombo = new JComboBox + private val logic_combo = new JComboBox { // output pane @@ -49,31 +49,31 @@ val doc = pane.getDocument.asInstanceOf[StyledDocument] - def makeStyle(name: String, bg: Boolean, color: Color) = { + def make_style(name: String, bg: Boolean, color: Color) = { val style = doc.addStyle(name, null) if (bg) StyleConstants.setBackground(style, color) else StyleConstants.setForeground(style, color) style } - val rawStyle = makeStyle("raw", false, Color.GRAY) - val infoStyle = makeStyle("info", true, new Color(160, 255, 160)) - val warningStyle = makeStyle("warning", true, new Color(255, 255, 160)) - val errorStyle = makeStyle("error", true, new Color(255, 160, 160)) + val raw_style = make_style("raw", false, Color.GRAY) + val info_style = make_style("info", true, new Color(160, 255, 160)) + val warning_style = make_style("warning", true, new Color(255, 255, 160)) + val error_style = make_style("error", true, new Color(255, 160, 160)) - IsabellePlugin.addPermanentConsumer (result => + IsabellePlugin.add_permanent_consumer (result => if (result != null && !result.is_system) { SwingUtilities.invokeLater(new Runnable { def run = { val logic = IsabellePlugin.isabelle.session - logicCombo.setModel(new DefaultComboBoxModel(Array(logic).asInstanceOf[Array[AnyRef]])) - logicCombo.setPrototypeDisplayValue("AAAA") // FIXME ?? + logic_combo.setModel(new DefaultComboBoxModel(Array(logic).asInstanceOf[Array[AnyRef]])) + logic_combo.setPrototypeDisplayValue("AAAA") // FIXME ?? val doc = pane.getDocument.asInstanceOf[StyledDocument] val style = result.kind match { - case IsabelleProcess.Kind.WARNING => warningStyle - case IsabelleProcess.Kind.ERROR => errorStyle - case IsabelleProcess.Kind.TRACING => infoStyle - case _ => if (result.is_raw) rawStyle else null + case IsabelleProcess.Kind.WARNING => warning_style + case IsabelleProcess.Kind.ERROR => error_style + case IsabelleProcess.Kind.TRACING => info_style + case _ => if (result.is_raw) raw_style else null } doc.insertString(doc.getLength, IsabellePlugin.result_content(result), style) if (!result.is_raw) doc.insertString(doc.getLength, "\n", style) @@ -89,29 +89,29 @@ // logic combo - logicCombo.setToolTipText("Isabelle logics") - logicCombo.setRequestFocusEnabled(false) - logicCombo.setModel(new DefaultComboBoxModel(Array("default").asInstanceOf[Array[AnyRef]])) - box.add(logicCombo) + logic_combo.setToolTipText("Isabelle logics") + logic_combo.setRequestFocusEnabled(false) + logic_combo.setModel(new DefaultComboBoxModel(Array("default").asInstanceOf[Array[AnyRef]])) + box.add(logic_combo) // mode combo - val modeIsar = "Isar" - val modeML = "ML" - val modes = Array(modeIsar, modeML) - var mode = modeIsar + val mode_Isar = "Isar" + val mode_ML = "ML" + val modes = Array(mode_Isar, mode_ML) + var mode = mode_Isar - val modeCombo = new JComboBox - modeCombo.setToolTipText("Toplevel mode") - modeCombo.setRequestFocusEnabled(false) - modeCombo.setModel(new DefaultComboBoxModel(modes.asInstanceOf[Array[AnyRef]])) - modeCombo.setPrototypeDisplayValue("AAAA") - modeCombo.addActionListener(new ActionListener { + val mode_combo = new JComboBox + mode_combo.setToolTipText("Toplevel mode") + mode_combo.setRequestFocusEnabled(false) + mode_combo.setModel(new DefaultComboBoxModel(modes.asInstanceOf[Array[AnyRef]])) + mode_combo.setPrototypeDisplayValue("AAAA") + mode_combo.addActionListener(new ActionListener { def actionPerformed(evt: ActionEvent): Unit = { - mode = modeCombo.getSelectedItem.asInstanceOf[String] + mode = mode_combo.getSelectedItem.asInstanceOf[String] } }) - box.add(modeCombo) + box.add(mode_combo) // input field @@ -120,9 +120,9 @@ def actionPerformed(evt: ActionEvent): Unit = { val command = text.getText if (command.length > 0) { - if (mode == modeIsar) + if (mode == mode_Isar) IsabellePlugin.isabelle.command(command) - else if (mode == modeML) + else if (mode == mode_ML) IsabellePlugin.isabelle.ML(command) text.setText("") } @@ -149,4 +149,3 @@ def focusOnDefaultComponent: Unit = text.requestFocus } - diff -r c3f7fa72af2a -r efc6d38d16d2 lib/jedit/plugin/isabelle_parser.scala --- a/lib/jedit/plugin/isabelle_parser.scala Sun Aug 24 19:02:22 2008 +0200 +++ b/lib/jedit/plugin/isabelle_parser.scala Sun Aug 24 19:24:27 2008 +0200 @@ -41,17 +41,18 @@ try { buffer.readLock() - text = buffer.getText(0, buffer.getLength()) - data = new SideKickParsedData(buffer.getName()) + text = buffer.getText(0, buffer.getLength) + data = new SideKickParsedData(buffer.getName) val asset = new IsabelleAsset("theory", null) asset.setStart(buffer.createPosition(0)) - asset.setEnd(buffer.createPosition(buffer.getLength())) + asset.setEnd(buffer.createPosition(buffer.getLength)) val node = new DefaultMutableTreeNode(asset) - data.root.insert(node, node.getChildCount()) + data.root.insert(node, node.getChildCount) - } finally { + } + finally { buffer.readUnlock() } diff -r c3f7fa72af2a -r efc6d38d16d2 lib/jedit/plugin/isabelle_plugin.scala --- a/lib/jedit/plugin/isabelle_plugin.scala Sun Aug 24 19:02:22 2008 +0200 +++ b/lib/jedit/plugin/isabelle_plugin.scala Sun Aug 24 19:24:27 2008 +0200 @@ -24,26 +24,23 @@ object IsabellePlugin { // unique ids - @volatile - private var idCount = 0 + private var id_count = 0 - def id() : String = synchronized { idCount += 1; "jedit:" + idCount } + def id() : String = synchronized { id_count += 1; "jedit:" + id_count } - def idProperties(value: String) : Properties = { + def id_properties(value: String) : Properties = { val props = new Properties props.setProperty(Markup.ID, value) props } - def idProperties() : Properties = { idProperties(id()) } + def id_properties() : Properties = { id_properties(id()) } // the error source - @volatile var errors: DefaultErrorSource = null // the Isabelle process - @volatile var isabelle: IsabelleProcess = null @@ -56,13 +53,13 @@ type consumer = IsabelleProcess.Result => Boolean private var consumers = new ListBuffer[consumer] - def addConsumer(consumer: consumer) = synchronized { consumers += consumer } + def add_consumer(consumer: consumer) = synchronized { consumers += consumer } - def addPermanentConsumer(consumer: IsabelleProcess.Result => Unit) = { - addConsumer(result => { consumer(result); false }) + def add_permanent_consumer(consumer: IsabelleProcess.Result => Unit) = { + add_consumer(result => { consumer(result); false }) } - def delConsumer(consumer: consumer) = synchronized { consumers -= consumer } + def del_consumer(consumer: consumer) = synchronized { consumers -= consumer } def consume(result: IsabelleProcess.Result) : Unit = { synchronized { consumers.elements.toList } foreach (consumer => @@ -71,7 +68,7 @@ try { consumer(result) } catch { case e: Throwable => Log.log(Log.ERROR, this, e); true } if (finished || result == null) - delConsumer(consumer) + del_consumer(consumer) }) } } @@ -87,7 +84,7 @@ IsabellePlugin.errors = new DefaultErrorSource("isabelle") ErrorSource.registerErrorSource(IsabellePlugin.errors) - IsabellePlugin.addPermanentConsumer (result => + IsabellePlugin.add_permanent_consumer (result => if (result != null && result.props != null && (result.kind == IsabelleProcess.Kind.WARNING || result.kind == IsabelleProcess.Kind.ERROR)) {