# HG changeset patch # User immler@in.tum.de # Date 1243976113 -7200 # Node ID a0c84b0edb9a5410551d4299bdb88ec890398a43 # Parent 72b02f9c509c983b35ffae91caa75c33dd801cc4# Parent 2b46d92e46429341b3fdfa05283a0e4b63324427 merged; resolved superficial conflicts diff -r 2b46d92e4642 -r a0c84b0edb9a src/Tools/jEdit/README_BUILD --- a/src/Tools/jEdit/README_BUILD Tue Jun 02 22:22:03 2009 +0200 +++ b/src/Tools/jEdit/README_BUILD Tue Jun 02 22:55:13 2009 +0200 @@ -2,16 +2,16 @@ Requirements to build from sources ================================== -* Proper Java JRE/JDK from Sun, e.g. 1.6.0_07 +* Proper Java JRE/JDK from Sun, e.g. 1.6.0_10 http://java.sun.com/javase/downloads/index.jsp * Netbeans 6.5 http://www.netbeans.org/downloads/index.html -* Scala for Netbeans - http://blogtrader.net/page/dcaoyuan/entry/new_scala_plugin_for_netbeans +* Scala for Netbeans: version 0.15.1 for NB 6.5 + http://sourceforge.net/project/showfiles.php?group_id=192439&package_id=256544 + http://blogtrader.net/dcaoyuan/category/NetBeans http://wiki.netbeans.org/Scala - http://plugins.netbeans.org/PluginPortal/faces/PluginDetailPage.jsp?pluginid=11854 * jEdit 4.3pre16 http://www.jedit.org/ @@ -33,4 +33,4 @@ isabelle env netbeans ... * Project properties: add "Run" argument like - -settings=/home/makarius/isabelle/jedit + -noserver -nobackground -settings=/home/makarius/isabelle/isabelle-jedit/dist diff -r 2b46d92e4642 -r a0c84b0edb9a src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala --- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Tue Jun 02 22:22:03 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Tue Jun 02 22:55:13 2009 +0200 @@ -71,9 +71,9 @@ class DynamicTokenMarker(buffer: JEditBuffer, prover: Prover) extends TokenMarker { override def markTokens(prev: TokenMarker.LineContext, - handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext = { + handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext = { val previous = prev.asInstanceOf[IndexLineContext] - val line = if(prev == null) 0 else previous.line + 1 + val line = if (prev == null) 0 else previous.line + 1 val context = new IndexLineContext(line, previous) val start = buffer.getLineStartOffset(line) val stop = start + line_segment.count @@ -89,13 +89,14 @@ while (command != null && command.start(document) < from(stop)) { for { markup <- command.highlight_node.flatten - if(to(markup.abs_stop(document)) > start) - if(to(markup.abs_start(document)) < stop) + if (to(markup.abs_stop(document)) > start) + if (to(markup.abs_start(document)) < stop) byte = DynamicTokenMarker.choose_byte(markup.info.toString) token_start = to(markup.abs_start(document)) - start max 0 - token_length = to(markup.abs_stop(document)) - to(markup.abs_start(document)) - - (start - to(markup.abs_start(document)) max 0) - - (to(markup.abs_stop(document)) - stop max 0) + token_length = + to(markup.abs_stop(document)) - to(markup.abs_start(document)) - + (start - to(markup.abs_start(document)) max 0) - + (to(markup.abs_stop(document)) - stop max 0) } { if (start + token_start > next_x) handler.handleToken(line_segment, 1, next_x - start, start + token_start - next_x, context) diff -r 2b46d92e4642 -r a0c84b0edb9a src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala --- a/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala Tue Jun 02 22:22:03 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala Tue Jun 02 22:55:13 2009 +0200 @@ -23,7 +23,7 @@ class InternalHyperlink(start: Int, end: Int, line: Int, ref_offset: Int) extends AbstractHyperlink(start, end, line, "") { - override def click(view: View) = { + override def click(view: View) { view.getTextArea.moveCaretPosition(ref_offset) } } diff -r 2b46d92e4642 -r a0c84b0edb9a src/Tools/jEdit/src/jedit/ProverSetup.scala --- a/src/Tools/jEdit/src/jedit/ProverSetup.scala Tue Jun 02 22:22:03 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala Tue Jun 02 22:55:13 2009 +0200 @@ -40,13 +40,14 @@ theory_view = new TheoryView(view.getTextArea, prover) prover.set_document(theory_view.change_receiver, - if (path.startsWith(Isabelle.VFS_PREFIX)) path.substring(Isabelle.VFS_PREFIX.length) else path) + if (path.startsWith(Isabelle.VFS_PREFIX)) path.substring(Isabelle.VFS_PREFIX.length) + else path) theory_view.activate val MCL = TheoryView.MAX_CHANGE_LENGTH - for (i <- 0 to buffer.getLength / MCL) prover ! - new isabelle.proofdocument.Text.Change(Isabelle.plugin.id(), i * MCL, - buffer.getText(i * MCL, - MCL min buffer.getLength - i * MCL),0) + for (i <- 0 to buffer.getLength / MCL) + prover ! new isabelle.proofdocument.Text.Change( + Isabelle.plugin.id(), i * MCL, + buffer.getText(i * MCL, MCL min buffer.getLength - i * MCL),0) //register output-view prover.output_info += (text => diff -r 2b46d92e4642 -r a0c84b0edb9a src/Tools/jEdit/src/jedit/TheoryView.scala --- a/src/Tools/jEdit/src/jedit/TheoryView.scala Tue Jun 02 22:22:03 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Tue Jun 02 22:55:13 2009 +0200 @@ -9,6 +9,7 @@ package isabelle.jedit import scala.actors.Actor +import scala.actors.Actor._ import isabelle.proofdocument.Text import isabelle.prover.{Prover, Command} @@ -44,7 +45,7 @@ class TheoryView (text_area: JEditTextArea, document_actor: Actor) extends TextAreaExtension with BufferListener { - def id() = Isabelle.plugin.id(); + def id() = Isabelle.plugin.id() private val buffer = text_area.getBuffer private val prover = Isabelle.prover_setup(buffer).get.prover @@ -76,14 +77,14 @@ } } - def activate() = { + def activate() { text_area.addCaretListener(selected_state_controller) text_area.addLeftOfScrollBar(phase_overview) text_area.getPainter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this) buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover)) } - def deactivate() = { + def deactivate() { text_area.getPainter.removeExtension(this) text_area.removeLeftOfScrollBar(phase_overview) text_area.removeCaretListener(selected_state_controller) @@ -94,10 +95,10 @@ val repaint_delay = new isabelle.utils.Delay(100, () => repaint_all()) - val change_receiver = scala.actors.Actor.actor { - scala.actors.Actor.loop { - scala.actors.Actor.react { - case _ => { + val change_receiver = actor { + loop { + react { + case _ => { // FIXME potentially blocking within loop/react!?!?!?! Swing.now { repaint_delay.delay_or_ignore() phase_overview.repaint_delay.delay_or_ignore() @@ -105,13 +106,14 @@ } } } - }.start + } def _from_current(to_id: String, changes: List[Text.Change], pos: Int): Int = changes match { case Nil => pos case Text.Change(id, start, added, removed) :: rest_changes => { - val shifted = if (start <= pos) + val shifted = + if (start <= pos) if (pos < start + added.length) start else pos - added.length + removed else pos @@ -223,10 +225,10 @@ private def commit: Unit = synchronized { if (col != null) { def split_changes(c: Text.Change): List[Text.Change] = { - val MCL = TheoryView.MAX_CHANGE_LENGTH - if (c.added.length <= MCL) List(c) - else Text.Change(c.id, c.start, c.added.substring(0, MCL), c.removed) :: - split_changes(new Text.Change(id(), c.start + MCL, c.added.substring(MCL), c.removed)) + val MAX = TheoryView.MAX_CHANGE_LENGTH + if (c.added.length <= MAX) List(c) + else Text.Change(c.id, c.start, c.added.substring(0, MAX), c.removed) :: + split_changes(new Text.Change(id(), c.start + MAX, c.added.substring(MAX), c.removed)) } val new_changes = split_changes(col) changes = new_changes.reverse ::: changes diff -r 2b46d92e4642 -r a0c84b0edb9a src/Tools/jEdit/src/proofdocument/ProofDocument.scala --- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Tue Jun 02 22:22:03 2009 +0200 +++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Tue Jun 02 22:55:13 2009 +0200 @@ -22,7 +22,7 @@ object ProofDocument { - // Be carefully when changing this regex. Not only must it handle the + // Be careful when changing this regex. Not only must it handle the // spurious end of a token but also: // Bug ID: 5050507 Pattern.matches throws StackOverflow Error // http://bugs.sun.com/bugdatabase/view_bug.do?bug_id=5050507 @@ -39,16 +39,18 @@ "[()\\[\\]{}:;]", Pattern.MULTILINE) val empty = - new ProofDocument(isabelle.jedit.Isabelle.plugin.id(), LinearSet(), Map(), LinearSet(), false, _ => false) + new ProofDocument(isabelle.jedit.Isabelle.plugin.id(), + LinearSet(), Map(), LinearSet(), false, _ => false) } -class ProofDocument(val id: String, - val tokens: LinearSet[Token], - val token_start: Map[Token, Int], - val commands: LinearSet[Command], - val active: Boolean, - is_command_keyword: String => Boolean) +class ProofDocument( + val id: String, + val tokens: LinearSet[Token], + val token_start: Map[Token, Int], + val commands: LinearSet[Command], + val active: Boolean, + is_command_keyword: String => Boolean) { def mark_active: ProofDocument = @@ -61,7 +63,7 @@ def set_command_keyword(f: String => Boolean): ProofDocument = new ProofDocument(isabelle.jedit.Isabelle.plugin.id(), tokens, token_start, commands, active, f) - def content = Token.string_from_tokens(List() ++ tokens, token_start) + def content = Token.string_from_tokens(Nil ++ tokens, token_start) /** token view **/ def text_changed(change: Text.Change): (ProofDocument, StructureChange) = @@ -70,11 +72,12 @@ var start: Map[Token, Int] = token_start def stop(t: Token) = start(t) + t.length // split old token lists - val tokens = List() ++ this.tokens + val tokens = Nil ++ this.tokens val (begin, remaining) = tokens.span(stop(_) < change.start) val (removed, end) = remaining.span(token_start(_) <= change.start + change.removed) // update indices - start = end.foldLeft (start) ((s, t) => s + (t -> (s(t) + change.added.length - change.removed))) + start = end.foldLeft(start)((s, t) => + s + (t -> (s(t) + change.added.length - change.removed))) val split_begin = removed.takeWhile(start(_) < change.start). map (t => { @@ -85,8 +88,8 @@ val split_end = removed.dropWhile(stop(_) < change.start + change.removed). map (t => { - val split_tok = new Token(t.content.substring(change.start + change.removed - start(t)), - t.kind) + val split_tok = + new Token(t.content.substring(change.start + change.removed - start(t)), t.kind) start += (split_tok -> start(t)) split_tok }) @@ -98,13 +101,13 @@ val ins = new Token(change.added, Token.Kind.OTHER) start += (ins -> change.start) - var invalid_tokens = split_begin ::: - ins :: split_end ::: end - var new_tokens = Nil: List[Token] - var old_suffix = Nil: List[Token] + var invalid_tokens = split_begin ::: ins :: split_end ::: end + var new_tokens: List[Token] = Nil + var old_suffix: List[Token] = Nil val match_start = invalid_tokens.firstOption.map(start(_)).getOrElse(0) - val matcher = ProofDocument.token_pattern.matcher(Token.string_from_tokens(invalid_tokens, start)) + val matcher = + ProofDocument.token_pattern.matcher(Token.string_from_tokens(invalid_tokens, start)) while (matcher.find() && invalid_tokens != Nil) { val kind = @@ -120,9 +123,10 @@ invalid_tokens = invalid_tokens dropWhile (stop(_) < stop(new_token)) invalid_tokens match { - case t::ts => if(start(t) == start(new_token) && - start(t) > change.start + change.added.length) { - old_suffix = t::ts + case t :: ts => + if (start(t) == start(new_token) && + start(t) > change.start + change.added.length) { + old_suffix = t :: ts new_tokens = new_tokens.tail invalid_tokens = Nil } @@ -131,22 +135,20 @@ } val insert = new_tokens.reverse val new_token_list = begin ::: insert ::: old_suffix - token_changed(change.id, - begin.lastOption, - insert, - old_suffix.firstOption, - new_token_list, - start) + token_changed(change.id, begin.lastOption, insert, + old_suffix.firstOption, new_token_list, start) } + /** command view **/ - private def token_changed(new_id: String, - before_change: Option[Token], - inserted_tokens: List[Token], - after_change: Option[Token], - new_tokens: List[Token], - new_token_start: Map[Token, Int]): (ProofDocument, StructureChange) = + private def token_changed( + new_id: String, + before_change: Option[Token], + inserted_tokens: List[Token], + after_change: Option[Token], + new_tokens: List[Token], + new_token_start: Map[Token, Int]): (ProofDocument, StructureChange) = { val new_tokenset = (LinearSet() ++ new_tokens).asInstanceOf[LinearSet[Token]] val cmd_before_change = before_change match { @@ -178,9 +180,10 @@ def tokens_to_commands(tokens: List[Token]): List[Command]= { tokens match { case Nil => Nil - case t::ts => - val (cmd,rest) = ts.span(t => t.kind != Token.Kind.COMMAND_START && t.kind != Token.Kind.COMMENT) - new Command(t::cmd, new_token_start) :: tokens_to_commands (rest) + case t :: ts => + val (cmd, rest) = + ts.span(t => t.kind != Token.Kind.COMMAND_START && t.kind != Token.Kind.COMMENT) + new Command(t :: cmd, new_token_start) :: tokens_to_commands(rest) } } @@ -191,7 +194,8 @@ new_tokens.dropWhile(_ != cmd_before_change.get.tokens.last).drop(1) else new_tokenset if (changed.exists(_ == before_change.get)) - changed.takeWhile(_ != before_change.get).toList ::: List(before_change.get) + changed.takeWhile(_ != before_change.get).toList ::: + List(before_change.get) else Nil } else Nil @@ -203,10 +207,12 @@ else Nil } else Nil - val rescan_begin = split_begin ::: before_change.map(bc => new_tokens.dropWhile(_ != bc).drop(1)). - getOrElse(new_tokens) - val rescanning_tokens = after_change.map(ac => rescan_begin.takeWhile(_ != ac)). - getOrElse(rescan_begin) ::: split_end + val rescan_begin = + split_begin ::: + before_change.map(bc => new_tokens.dropWhile(_ != bc).drop(1)).getOrElse(new_tokens) + val rescanning_tokens = + after_change.map(ac => rescan_begin.takeWhile(_ != ac)).getOrElse(rescan_begin) ::: + split_end val inserted_commands = tokens_to_commands(rescanning_tokens.toList) val change = new StructureChange(cmd_before_change, inserted_commands, removed_commands.toList) @@ -215,7 +221,8 @@ insert_after(cmd_before_change, inserted_commands) val doc = - new ProofDocument(new_id, new_tokenset, new_token_start, new_commandset, active, is_command_keyword) + new ProofDocument(new_id, new_tokenset, new_token_start, + new_commandset, active, is_command_keyword) return (doc, change) } diff -r 2b46d92e4642 -r a0c84b0edb9a src/Tools/jEdit/src/proofdocument/Token.scala --- a/src/Tools/jEdit/src/proofdocument/Token.scala Tue Jun 02 22:22:03 2009 +0200 +++ b/src/Tools/jEdit/src/proofdocument/Token.scala Tue Jun 02 22:55:13 2009 +0200 @@ -18,19 +18,14 @@ val OTHER = Value("OTHER") } - private def fill(n: Int) = { - val blanks = new Array[Char](n) - for(i <- 0 to n - 1) blanks(i) = ' ' - new String(blanks) - } - def string_from_tokens (tokens: List[Token], starts: Map[Token, Int]): String = { + def string_from_tokens(tokens: List[Token], starts: Token => Int): String = { def stop(t: Token) = starts(t) + t.length tokens match { case Nil => "" - case t::tokens => ( tokens.foldLeft - (t.content, stop(t)) - ((a, token) => (a._1 + fill(starts(token) - a._2) + token.content, stop(token))) - )._1 + case t :: tokens => + val (res, _) = tokens.foldLeft(t.content, stop(t))((a, token) => + (a._1 + " " * (starts(token) - a._2) + token.content, stop(token))) + res } } diff -r 2b46d92e4642 -r a0c84b0edb9a src/Tools/jEdit/src/prover/Command.scala --- a/src/Tools/jEdit/src/prover/Command.scala Tue Jun 02 22:22:03 2009 +0200 +++ b/src/Tools/jEdit/src/prover/Command.scala Tue Jun 02 22:55:13 2009 +0200 @@ -38,7 +38,7 @@ override def toString = name val name = tokens.head.content - val content:String = Token.string_from_tokens(tokens, starts) + val content: String = Token.string_from_tokens(tokens, starts) def start(doc: ProofDocument) = doc.token_start(tokens.first) def stop(doc: ProofDocument) = doc.token_start(tokens.last) + tokens.last.length @@ -83,8 +83,8 @@ /* markup */ val empty_root_node = - new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length, Nil, - id, content, RootInfo()) + new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length, + Nil, id, content, RootInfo()) var markup_root = empty_root_node @@ -98,19 +98,20 @@ def markup_node(begin: Int, end: Int, info: MarkupInfo) = new MarkupNode(this, begin, end, Nil, id, - if (end <= content.length && begin >= 0) content.substring(begin, end) else "wrong indices??", - info) + if (end <= content.length && begin >= 0) content.substring(begin, end) + else "wrong indices??", + info) def type_at(pos: Int): String = { - val types = markup_root.filter(_.info match {case TypeInfo(_) => true case _ => false}) + val types = markup_root.filter(_.info match { case TypeInfo(_) => true case _ => false }) types.flatten(_.flatten). find(t => t.start <= pos && t.stop > pos). - map(t => "\"" + t.content + "\" : " + (t.info match {case TypeInfo(i) => i case _ => ""})). + map(t => t.content + ": " + (t.info match { case TypeInfo(i) => i case _ => "" })). getOrElse(null) } def ref_at(pos: Int): Option[MarkupNode] = - markup_root.filter(_.info match {case RefInfo(_,_,_,_) => true case _ => false}). + markup_root.filter(_.info match { case RefInfo(_, _, _, _) => true case _ => false }). flatten(_.flatten). find(t => t.start <= pos && t.stop > pos) } diff -r 2b46d92e4642 -r a0c84b0edb9a src/Tools/jEdit/src/prover/MarkupNode.scala --- a/src/Tools/jEdit/src/prover/MarkupNode.scala Tue Jun 02 22:22:03 2009 +0200 +++ b/src/Tools/jEdit/src/prover/MarkupNode.scala Tue Jun 02 22:55:13 2009 +0200 @@ -15,31 +15,35 @@ abstract class MarkupInfo case class RootInfo() extends MarkupInfo -case class OuterInfo(highlight: String) extends MarkupInfo {override def toString = highlight} -case class HighlightInfo(highlight: String) extends MarkupInfo {override def toString = highlight} -case class TypeInfo(type_kind: String) extends MarkupInfo {override def toString = type_kind} +case class OuterInfo(highlight: String) extends + MarkupInfo { override def toString = highlight } +case class HighlightInfo(highlight: String) extends + MarkupInfo { override def toString = highlight } +case class TypeInfo(type_kind: String) extends + MarkupInfo { override def toString = type_kind } case class RefInfo(file: Option[String], line: Option[Int], - command_id: Option[String], offset: Option[Int]) extends MarkupInfo { - override def toString = (file, line, command_id, offset).toString -} + command_id: Option[String], offset: Option[Int]) extends MarkupInfo { + override def toString = (file, line, command_id, offset).toString + } object MarkupNode { - def markup2default_node(node: MarkupNode, cmd: Command, doc: ProofDocument) : DefaultMutableTreeNode = { + def markup2default_node(node: MarkupNode, cmd: Command, doc: ProofDocument) + : DefaultMutableTreeNode = { implicit def int2pos(offset: Int): Position = - new Position { def getOffset = offset; override def toString = offset.toString} + new Position { def getOffset = offset; override def toString = offset.toString } object RelativeAsset extends IAsset { - override def getIcon : Icon = null - override def getShortString : String = node.content - override def getLongString : String = node.info.toString - override def getName : String = node.id - override def setName (name : String) = () - override def setStart(start : Position) = () - override def getStart : Position = node.abs_start(doc) - override def setEnd(end : Position) = () - override def getEnd : Position = node.abs_stop(doc) + override def getIcon: Icon = null + override def getShortString: String = node.content + override def getLongString: String = node.info.toString + override def getName: String = node.id + override def setName(name: String) = () + override def setStart(start: Position) = () + override def getStart: Position = node.abs_start(doc) + override def setEnd(end: Position) = () + override def getEnd: Position = node.abs_stop(doc) override def toString = node.id + ": " + node.content + "[" + getStart + " - " + getEnd + "]" } @@ -47,11 +51,11 @@ } } -class MarkupNode (val base: Command, val start: Int, val stop: Int, - val children: List[MarkupNode], - val id: String, val content: String, val info: MarkupInfo) { - - def swing_node(doc: ProofDocument) : DefaultMutableTreeNode = { +class MarkupNode(val base: Command, val start: Int, val stop: Int, + val children: List[MarkupNode], + val id: String, val content: String, val info: MarkupInfo) +{ + def swing_node(doc: ProofDocument): DefaultMutableTreeNode = { val node = MarkupNode.markup2default_node (this, base, doc) children.map(node add _.swing_node(doc)) node @@ -63,11 +67,12 @@ def set_children(newchildren: List[MarkupNode]): MarkupNode = new MarkupNode(base, start, stop, newchildren, id, content, info) - def add(child : MarkupNode) = set_children ((child :: children) sort ((a, b) => a.start < b.start)) + def add(child: MarkupNode) = + set_children ((child :: children) sort ((a, b) => a.start < b.start)) - def remove(nodes : List[MarkupNode]) = set_children(children diff nodes) + def remove(nodes: List[MarkupNode]) = set_children(children diff nodes) - def dfs : List[MarkupNode] = { + def dfs: List[MarkupNode] = { var all = Nil : List[MarkupNode] for (child <- children) all = child.dfs ::: all @@ -86,29 +91,35 @@ else { val filled_gaps = for { child <- children - markups = if (next_x < child.start) { - new MarkupNode(base, next_x, child.start, Nil, id, content, info) :: child.flatten - } else child.flatten + markups = + if (next_x < child.start) { + new MarkupNode(base, next_x, child.start, Nil, id, content, info) :: child.flatten + } else child.flatten update = (next_x = child.stop) markup <- markups } yield markup - if (next_x < stop) filled_gaps + new MarkupNode(base, next_x, stop, Nil, id, content, info) + if (next_x < stop) + filled_gaps + new MarkupNode(base, next_x, stop, Nil, id, content, info) else filled_gaps } } - def filter(p: (MarkupNode => Boolean)): List[MarkupNode] = { + def filter(p: MarkupNode => Boolean): List[MarkupNode] = { val filtered = children.flatMap(_.filter(p)) if (p(this)) List(this set_children(filtered)) else filtered } - def +(new_child : MarkupNode) : MarkupNode = { + def +(new_child: MarkupNode): MarkupNode = { if (new_child fitting_into this) { var inserted = false - val new_children = children.map(c => if((new_child fitting_into c) && !inserted) {inserted = true; c + new_child} else c) + val new_children = + children.map(c => + if ((new_child fitting_into c) && !inserted) {inserted = true; c + new_child} + else c) if (!inserted) { - // new_child did not fit into children of this -> insert new_child between this and its children + // new_child did not fit into children of this + // -> insert new_child between this and its children val fitting = children filter(_ fitting_into new_child) (this remove fitting) add ((new_child /: fitting) (_ + _)) } @@ -120,7 +131,8 @@ } // does this fit into node? - def fitting_into(node : MarkupNode) = node.start <= this.start && node.stop >= this.stop + def fitting_into(node: MarkupNode) = node.start <= this.start && node.stop >= this.stop - override def toString = "([" + start + " - " + stop + "] " + id + "( " + content + "): " + info.toString + override def toString = + "([" + start + " - " + stop + "] " + id + "( " + content + "): " + info.toString } diff -r 2b46d92e4642 -r a0c84b0edb9a src/Tools/jEdit/src/prover/Prover.scala --- a/src/Tools/jEdit/src/prover/Prover.scala Tue Jun 02 22:22:03 2009 +0200 +++ b/src/Tools/jEdit/src/prover/Prover.scala Tue Jun 02 22:55:13 2009 +0200 @@ -88,20 +88,20 @@ if (map(xsymb).get("abbrev").isDefined) _completions += map(xsymb)("abbrev") } */ - decl_info += (k_v => _completions += k_v._1) + decl_info += (p => _completions += p._1) /* event handling */ val activated = new EventBus[Unit] val output_info = new EventBus[String] - var change_receiver = null: Actor + var change_receiver: Actor = null private def handle_result(result: IsabelleProcess.Result) { // helper-function (move to XML?) def get_attr(attributes: List[(String, String)], attr: String): Option[String] = - attributes.find(kv => kv._1 == attr).map(_._2) + attributes.find(p => p._1 == attr).map(_._2) def command_change(c: Command) = this ! c val (running, command) = @@ -149,7 +149,7 @@ // document edits case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits) - if document_versions.exists(dv => doc_id == dv.id) => + if document_versions.exists(_.id == doc_id) => output_info.event(result.toString) for { XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _) @@ -194,9 +194,9 @@ case List(XML.Elem(Markup.ML_DEF, attr, _)) => command.markup_root += command.markup_node(begin.get, end.get, RefInfo(get_attr(attr, Markup.FILE), - get_attr(attr, Markup.LINE).map(Integer.parseInt), + get_attr(attr, Markup.LINE).map(_.toInt), get_attr(attr, Markup.ID), - get_attr(attr, Markup.OFFSET).map(Integer.parseInt))) + get_attr(attr, Markup.OFFSET).map(_.toInt))) case _ => } } else {