# HG changeset patch # User wenzelm # Date 1233080879 -3600 # Node ID 7d0726f19d0423116dcca6f21b9e25d6d0856de5 # Parent 7d1d13750890b4fb5e534cbd7bf92c6617034d7d tuned whitespace; diff -r 7d1d13750890 -r 7d0726f19d04 src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala --- 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 diff -r 7d1d13750890 -r 7d0726f19d04 src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala --- 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) } diff -r 7d1d13750890 -r 7d0726f19d04 src/Tools/jEdit/src/jedit/Plugin.scala --- 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 diff -r 7d1d13750890 -r 7d0726f19d04 src/Tools/jEdit/src/jedit/ProverSetup.scala --- 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 diff -r 7d1d13750890 -r 7d0726f19d04 src/Tools/jEdit/src/jedit/ScrollerDockable.scala --- 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 diff -r 7d1d13750890 -r 7d0726f19d04 src/Tools/jEdit/src/jedit/SelectionActions.scala --- 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 } diff -r 7d1d13750890 -r 7d0726f19d04 src/Tools/jEdit/src/prover/MarkupNode.scala --- 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 } } diff -r 7d1d13750890 -r 7d0726f19d04 src/Tools/jEdit/src/prover/Prover.scala --- 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) diff -r 7d1d13750890 -r 7d0726f19d04 src/Tools/jEdit/src/utils/Delay.scala --- 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() }