--- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala Tue Jan 27 18:58:16 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala Tue Jan 27 19:27:59 2009 +0100
@@ -22,7 +22,7 @@
/* parsing */
private var stopped = false
- override def stop () = { stopped = true }
+ override def stop() = { stopped = true }
def parse(buffer : Buffer, error_source : DefaultErrorSource): SideKickParsedData = {
stopped = false
@@ -30,7 +30,7 @@
val data = new SideKickParsedData(buffer.getName)
val prover_setup = Isabelle.plugin.prover_setup(buffer)
- if(prover_setup.isDefined){
+ if (prover_setup.isDefined) {
val document = prover_setup.get.prover.document
val commands = document.commands
while (!stopped && commands.hasNext) {
@@ -54,7 +54,7 @@
override def complete(pane: EditPane, caret: Int): SideKickCompletion = {
val buffer = pane.getBuffer
val ps = Isabelle.prover_setup(buffer)
- if(ps.isDefined) {
+ if (ps.isDefined) {
val completions = ps.get.prover.completions
def before_caret(i : Int) = buffer.getText(0 max caret - i, i)
def next_nonfitting(s : String) : String = {
@@ -64,9 +64,9 @@
}
def suggestions(i : Int) : (Set[String], String)= {
val text = before_caret(i)
- if(!text.matches("\\s") && i < 30){
+ if (!text.matches("\\s") && i < 30) {
val larger_results = suggestions(i + 1)
- if(larger_results._1.size > 0) larger_results
+ if (larger_results._1.size > 0) larger_results
else (completions.range(text, next_nonfitting(text)), text)
} else (Set[String](), text)
@@ -76,10 +76,10 @@
val descriptions = new java.util.LinkedList[String]
// compute suggestions
val (suggs, text) = suggestions(1)
- for(s <- suggs) {
+ for (s <- suggs) {
val decoded = Isabelle.symbols.decode(s)
list.add(decoded)
- if(decoded != s) descriptions.add(s) else descriptions.add(null)
+ if (decoded != s) descriptions.add(s) else descriptions.add(null)
}
return new IsabelleSideKickCompletion(pane.getView, text, list, descriptions)
} else return null
--- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Tue Jan 27 18:58:16 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Tue Jan 27 19:27:59 2009 +0100
@@ -31,7 +31,7 @@
addMouseListener(new MouseAdapter {
override def mousePressed(evt : MouseEvent) {
val line = yToLine(evt.getY)
- if(line >= 0 && line < textarea.getLineCount())
+ if (line >= 0 && line < textarea.getLineCount())
textarea.setCaretPosition(textarea.getLineStartOffset(line))
}
})
@@ -52,7 +52,7 @@
val buffer = textarea.getBuffer
val lineCount = buffer.getLineCount
val line = yToLine(evt.getY())
- if(line >= 0 && line < textarea.getLineCount)
+ if (line >= 0 && line < textarea.getLineCount)
{
"TODO: Tooltip"
} else ""
@@ -71,7 +71,7 @@
gfx.setColor(light)
gfx.fillRect(0, y, getWidth - 1, 1 max height)
- if(height > 2){
+ if (height > 2) {
gfx.setColor(dark)
gfx.drawRect(0, y, getWidth - 1, height)
}
@@ -82,7 +82,7 @@
super.paintComponent(gfx)
val buffer = textarea.getBuffer
- for(c <- prover.document.commands)
+ for (c <- prover.document.commands)
paintCommand(c, buffer, gfx)
}
--- a/src/Tools/jEdit/src/jedit/Plugin.scala Tue Jan 27 18:58:16 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/Plugin.scala Tue Jan 27 19:27:59 2009 +0100
@@ -106,9 +106,9 @@
case Some(prover_setup) =>
prover_setup.theory_view.activate
val dockable = epu.getEditPane.getView.getDockableWindowManager.getDockable("isabelle-output")
- if(dockable != null) {
+ if (dockable != null) {
val output_dockable = dockable.asInstanceOf[OutputDockable]
- if(output_dockable.getComponent(0) != prover_setup.output_text_view ) {
+ if (output_dockable.getComponent(0) != prover_setup.output_text_view ) {
output_dockable.asInstanceOf[OutputDockable].removeAll
output_dockable.asInstanceOf[OutputDockable].add(new JScrollPane(prover_setup.output_text_view))
output_dockable.revalidate
@@ -117,7 +117,7 @@
}
case EditPaneUpdate.BUFFER_CHANGING =>
val buffer = epu.getEditPane.getBuffer
- if(buffer != null) mapping get buffer match {
+ if (buffer != null) mapping get buffer match {
//only deactivate 'isabelle'-buffers!
case None =>
case Some(prover_setup) => prover_setup.theory_view.deactivate
--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala Tue Jan 27 18:58:16 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala Tue Jan 27 19:27:59 2009 +0100
@@ -50,9 +50,9 @@
output_text_view.append(text)
val dockable = view.getDockableWindowManager.getDockable("isabelle-output")
//link process output if dockable is active
- if(dockable != null) {
+ if (dockable != null) {
val output_dockable = dockable.asInstanceOf[OutputDockable]
- if(output_dockable.getComponent(0) != output_text_view ) {
+ if (output_dockable.getComponent(0) != output_text_view ) {
output_dockable.asInstanceOf[OutputDockable].removeAll
output_dockable.asInstanceOf[OutputDockable].add(new JScrollPane(output_text_view))
output_dockable.revalidate
@@ -66,7 +66,7 @@
val state_panel =
if (state_view != null) state_view.asInstanceOf[StateViewDockable].panel
else null
- if (state_panel != null){
+ if (state_panel != null) {
if (state == null)
state_panel.setDocument(null: Document)
else
--- a/src/Tools/jEdit/src/jedit/ScrollerDockable.scala Tue Jan 27 18:58:16 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/ScrollerDockable.scala Tue Jan 27 19:27:59 2009 +0100
@@ -60,7 +60,7 @@
//panel has to be displayable before calculating preferred size!
add(panel)
// recalculate preferred size after resizing the message_view
- if(panel.getPreferredSize.getWidth.toInt != getWidth){
+ if (panel.getPreferredSize.getWidth.toInt != getWidth) {
cache.renderer.relayout (panel, getWidth)
}
val width = panel.getPreferredSize.getWidth.toInt
@@ -76,12 +76,12 @@
removeAll()
//calculate offset in pixel
val panel = place_message(no, 0)
- val pixeloffset = if(panel != null) panel.getHeight*offset/100 else 0
+ val pixeloffset = if (panel != null) panel.getHeight*offset/100 else 0
var n = no
var y:Int = getHeight + pixeloffset
- while (y >= 0 && n >= 0){
+ while (y >= 0 && n >= 0) {
val panel = place_message (n, y)
- if(panel != null) {
+ if (panel != null) {
panel.setBorder(javax.swing.border.LineBorder.createBlackLineBorder)
y = y - panel.getHeight
}
@@ -132,9 +132,9 @@
// do not show every new message, wait a certain amount of time
val message_ind_timer : Timer = new Timer(250, new ActionListener {
// this method is called to indicate a new message
- override def actionPerformed(e:ActionEvent){
+ override def actionPerformed(e:ActionEvent) {
//fire scroll-event if necessary and wanted
- if(message_panel.no != buffer.size*subunits - 1 && infopanel.isAutoScroll) {
+ if (message_panel.no != buffer.size*subunits - 1 && infopanel.isAutoScroll) {
vscroll.setValue(buffer.size*subunits - 1)
}
infopanel.setIndicator(false)
@@ -147,15 +147,15 @@
infopanel.setIndicator(true)
infopanel.setText(buffer.size.toString)
- if (! message_ind_timer.isRunning()){
- if(infopanel.isAutoScroll){
+ if (!message_ind_timer.isRunning()) {
+ if (infopanel.isAutoScroll) {
vscroll.setValue(buffer.size*subunits - 1)
}
message_ind_timer.setRepeats(false)
message_ind_timer.start()
}
- if(message_panel.no == -1) {
+ if (message_panel.no == -1) {
message_panel.no = 0
message_panel.revalidate
}
@@ -164,7 +164,7 @@
override def adjustmentValueChanged (e : AdjustmentEvent) = {
//event-handling has to be so general (without UNIT_INCR,...)
// because all events could be sent as TRACK e.g. on my mac
- if (e.getSource == vscroll){
+ if (e.getSource == vscroll) {
message_panel.no = e.getValue / subunits
message_panel.offset = 100 - 100 * (e.getValue % subunits) / subunits
message_panel.revalidate
@@ -183,8 +183,8 @@
override def addUnrendered (id: Int, m: Result) {
update(id, m)
}
- override def getUnrendered (id: Int): Option[Result] = {
- if(id < size && id >= 0 && apply(id) != null) Some (apply(id))
+ override def getUnrendered(id: Int): Option[Result] = {
+ if (id < size && id >= 0 && apply(id) != null) Some (apply(id))
else None
}
override def size = super.size
@@ -196,7 +196,7 @@
override def getRendered (id: Int): Option[XHTMLPanel] = {
//get message from buffer and render it if necessary
- if(!isDefinedAt(id)){
+ if (!isDefinedAt(id)) {
buffer.getUnrendered(id) match {
case Some (message) =>
update (id, renderer.render (message))
@@ -204,7 +204,7 @@
}
}
val result = try {
- Some (apply(id))
+ Some(apply(id))
} catch {
case _ => {
None
--- a/src/Tools/jEdit/src/jedit/SelectionActions.scala Tue Jan 27 18:58:16 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/SelectionActions.scala Tue Jan 27 19:27:59 2009 +0100
@@ -32,7 +32,7 @@
}
override def keyPressed(e: KeyEvent) {
- if(e.getKeyCode == KeyEvent.VK_ENTER) {
+ if (e.getKeyCode == KeyEvent.VK_ENTER) {
copyaction
e.consume
}
--- a/src/Tools/jEdit/src/prover/MarkupNode.scala Tue Jan 27 18:58:16 2009 +0100
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala Tue Jan 27 19:27:59 2009 +0100
@@ -23,7 +23,7 @@
override def getShortString : String = node.short
override def getLongString : String = node.long
override def getName : String = node.name
- override def setName (name : String) = ()
+ override def setName(name : String) = ()
override def setStart(start : Position) = ()
override def getStart : Position = node.base.start + node.start
override def setEnd(end : Position) = ()
@@ -48,7 +48,7 @@
def children = children_cell
def children_= (cs : List[MarkupNode]) = {
swing_node.removeAllChildren
- for(c <- cs) swing_node add c.swing_node
+ for (c <- cs) swing_node add c.swing_node
children_cell = cs
}
@@ -62,7 +62,7 @@
private def remove(nodes : List[MarkupNode]) {
children_cell = children diff nodes
- for(node <- nodes) try {
+ for (node <- nodes) try {
swing_node remove node.swing_node
} catch { case e : IllegalArgumentException =>
System.err.println(e.toString)
@@ -72,23 +72,23 @@
def dfs : List[MarkupNode] = {
var all = Nil : List[MarkupNode]
- for(child <- children)
+ for (child <- children)
all = child.dfs ::: all
all = this :: all
all
}
def insert(new_child : MarkupNode) : Unit = {
- if(new_child fitting_into this){
- for(child <- children){
- if(new_child fitting_into child)
+ if (new_child fitting_into this) {
+ for (child <- children) {
+ if (new_child fitting_into child)
child insert new_child
}
- if(new_child orphan){
+ if (new_child orphan) {
// new_child did not fit into children of this
// -> insert new_child between this and its children
- for(child <- children){
- if(child fitting_into new_child) {
+ for (child <- children) {
+ if (child fitting_into new_child) {
new_child add child
}
}
--- a/src/Tools/jEdit/src/prover/Prover.scala Tue Jan 27 18:58:16 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala Tue Jan 27 19:27:59 2009 +0100
@@ -46,9 +46,9 @@
def completions = _completions
/* // TODO: ask Makarius to make Interpretation.symbols public (here: read-only as 'symbol_map')
val map = isabelle.jedit.Isabelle.symbols.symbol_map
- for(xsymb <- map.keys) {
+ for (xsymb <- map.keys) {
_completions += xsymb
- if(map(xsymb).get("abbrev").isDefined) _completions += map(xsymb)("abbrev")
+ if (map(xsymb).get("abbrev").isDefined) _completions += map(xsymb)("abbrev")
}
*/
decl_info += (k_v => _completions += k_v._1)
--- a/src/Tools/jEdit/src/utils/Delay.scala Tue Jan 27 18:58:16 2009 +0100
+++ b/src/Tools/jEdit/src/utils/Delay.scala Tue Jan 27 19:27:59 2009 +0100
@@ -12,14 +12,14 @@
class Delay(amount : Int, action : () => Unit) {
val timer : Timer = new Timer(amount, new ActionListener {
- override def actionPerformed(e:ActionEvent){
- action ()
+ override def actionPerformed(e:ActionEvent) {
+ action()
}
})
// if called very often, action is executed at most once
// in amount milliseconds
- def delay_or_ignore () = {
- if (! timer.isRunning()){
+ def delay_or_ignore() = {
+ if (!timer.isRunning()) {
timer.setRepeats(false)
timer.start()
}