# HG changeset patch
# User wenzelm
# Date 1243970422 -7200
# Node ID 5d5d253c7c29633cf82decd48881bb9d5519396a
# Parent  abab3a577e10c400c02bb06b777f83b6541a3a69
superficial tuning;

diff -r abab3a577e10 -r 5d5d253c7c29 src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala
--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Sat May 30 23:27:37 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Tue Jun 02 21:20:22 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
@@ -85,15 +85,18 @@
 
     var next_x = start
     for {
-      command <- document.commands.dropWhile(_.stop(document) <= from(start)).takeWhile(_.start(document) < from(stop))
+      command <- document.commands.
+        dropWhile(_.stop(document) <= from(start)).
+        takeWhile(_.start(document) < from(stop))
       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 abab3a577e10 -r 5d5d253c7c29 src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala
--- a/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala	Sat May 30 23:27:37 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala	Tue Jun 02 21:20:22 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 abab3a577e10 -r 5d5d253c7c29 src/Tools/jEdit/src/jedit/ProverSetup.scala
--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala	Sat May 30 23:27:37 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala	Tue Jun 02 21:20:22 2009 +0200
@@ -40,9 +40,11 @@
 
     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
-    prover ! new isabelle.proofdocument.Text.Change(Isabelle.plugin.id(), 0,buffer.getText(0, buffer.getLength),0)
+    prover ! new isabelle.proofdocument.Text.Change(
+      Isabelle.plugin.id(), 0, buffer.getText(0, buffer.getLength), 0)
 
     //register output-view
     prover.output_info += (text =>
diff -r abab3a577e10 -r 5d5d253c7c29 src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Sat May 30 23:27:37 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Tue Jun 02 21:20:22 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()
@@ -111,7 +112,8 @@
     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 abab3a577e10 -r 5d5d253c7c29 src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Sat May 30 23:27:37 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Tue Jun 02 21:20:22 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(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,8 +123,9 @@
 
       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) {
+        case t :: ts =>
+          if (start(t) == start(new_token) &&
+              start(t) > change.start + change.added.length) {
           old_suffix = ts
           invalid_tokens = Nil
         }
@@ -131,13 +135,10 @@
     val insert = new_tokens.reverse
     val new_token_list = begin ::: insert ::: old_suffix
     val new_tokenset = (LinearSet() ++ new_token_list).asInstanceOf[LinearSet[Token]]
-    token_changed(change.id,
-                  begin.lastOption,
-                  insert,
-                  old_suffix.firstOption,
-                  new_tokenset,
-                  start)
+    token_changed(change.id, begin.lastOption, insert,
+      old_suffix.firstOption, new_tokenset, start)
   }
+
   
   /** command view **/
 
@@ -146,12 +147,13 @@
     return null
   }
 
-  private def token_changed(new_id: String,
-                            before_change: Option[Token],
-                            inserted_tokens: List[Token],
-                            after_change: Option[Token],
-                            new_tokenset: LinearSet[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_tokenset: LinearSet[Token],
+    new_token_start: Map[Token, Int]): (ProofDocument, StructureChange) =
   {
     val cmd_first_changed =
       if (before_change.isDefined) commands.find(_.tokens.contains(before_change.get))
@@ -174,16 +176,18 @@
     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)
       }
     }
 
     val split_begin_tokens =
       if (!cmd_first_changed.isDefined || !before_change.isDefined) Nil
       else {
-        cmd_first_changed.get.tokens.takeWhile(_ != before_change.get) ::: List(before_change.get)
+        cmd_first_changed.get.tokens.takeWhile(_ != before_change.get) :::
+          List(before_change.get)
       }
     val split_end_tokens =
       if (!cmd_last_changed.isDefined || !after_change.isDefined) Nil
@@ -191,7 +195,8 @@
         cmd_last_changed.get.tokens.dropWhile(_ != after_change.get)
       }
 
-    val rescanning_tokens = split_begin_tokens ::: inserted_tokens ::: split_end_tokens
+    val rescanning_tokens =
+      split_begin_tokens ::: inserted_tokens ::: split_end_tokens
     val inserted_commands = tokens_to_commands(rescanning_tokens)
 
     val change = new StructureChange(cmd_before_change, inserted_commands, removed_commands.toList)
@@ -200,7 +205,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 abab3a577e10 -r 5d5d253c7c29 src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Sat May 30 23:27:37 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala	Tue Jun 02 21:20:22 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
@@ -81,8 +81,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
 
@@ -96,19 +96,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 abab3a577e10 -r 5d5d253c7c29 src/Tools/jEdit/src/prover/MarkupNode.scala
--- a/src/Tools/jEdit/src/prover/MarkupNode.scala	Sat May 30 23:27:37 2009 +0200
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala	Tue Jun 02 21:20:22 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,41 +91,48 @@
     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) (_ + _))
       }
       else this set_children new_children
     } else {
-      error("ignored nonfitting markup " + new_child.id + new_child.content + new_child.info.toString
-                         + "(" +new_child.start + ", "+ new_child.stop + ")")
+      error("ignored nonfitting markup " + new_child.id + new_child.content +
+        new_child.info.toString + "(" +new_child.start + ", "+ new_child.stop + ")")
     }
   }
 
   // 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 abab3a577e10 -r 5d5d253c7c29 src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Sat May 30 23:27:37 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Tue Jun 02 21:20:22 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 {