# HG changeset patch
# User wenzelm
# Date 1232377018 -3600
# Node ID 017fae24829f4ddec8152431d96d9cf073b9d81a
# Parent  c787cbe6cdce866a080677df267bb5ac3dff44ea
simplified implicit convertion Int => Position;

diff -r c787cbe6cdce -r 017fae24829f src/Tools/jEdit/src/prover/MarkupNode.scala
--- a/src/Tools/jEdit/src/prover/MarkupNode.scala	Fri Jan 16 23:00:24 2009 +0100
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala	Mon Jan 19 15:56:58 2009 +0100
@@ -15,13 +15,10 @@
 
   def markup2default_node(node : MarkupNode) : DefaultMutableTreeNode = {
 
-    class MyPos(val o : Int) extends Position {
-      override def getOffset = o
-    }
+    implicit def int2pos(offset: Int): Position =
+      new Position { def getOffset = offset }
 
-    implicit def int2pos(x : Int) : MyPos = new MyPos(x)
-
-    object RelativeAsset extends IAsset{
+    object RelativeAsset extends IAsset {
       override def getIcon : Icon = null
       override def getShortString : String = node.short
       override def getLongString : String = node.long