--- 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
}
-
--- 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()
}
--- 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)) {