# HG changeset patch # User wenzelm # Date 1289341486 -3600 # Node ID 45e7c2889d2f90f9d6437b07a80cc21360212548 # Parent b9beabec9540f1e654b39ede1cf61d15dddaacab misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics); diff -r b9beabec9540 -r 45e7c2889d2f src/Tools/jEdit/src/jedit/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Tue Nov 09 22:37:10 2010 +0100 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Tue Nov 09 23:24:46 2010 +0100 @@ -24,8 +24,25 @@ object Isabelle_Sidekick { - implicit def int_to_pos(offset: Int): Position = + def int_to_pos(offset: Int): Position = new Position { def getOffset = offset; override def toString = offset.toString } + + class Asset(name: String, start: Int, end: Int) extends IAsset + { + protected var _name = name + protected var _start = int_to_pos(start) + protected var _end = int_to_pos(end) + override def getIcon: Icon = null + override def getShortString: String = _name + override def getLongString: String = _name + override def getName: String = _name + override def setName(name: String) = _name = name + override def getStart: Position = _start + override def setStart(start: Position) = _start = start + override def getEnd: Position = _end + override def setEnd(end: Position) = _end = end + override def toString = _name + } } @@ -40,14 +57,12 @@ def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData = { - import Isabelle_Sidekick.int_to_pos - stopped = false // FIXME lock buffer (!??) val data = new SideKickParsedData(buffer.getName) val root = data.root - data.getAsset(root).setEnd(buffer.getLength) + data.getAsset(root).setEnd(Isabelle_Sidekick.int_to_pos(buffer.getLength)) Swing_Thread.now { Document_Model(buffer) } match { case Some(model) => @@ -97,8 +112,6 @@ { def parser(data: SideKickParsedData, model: Document_Model) { - import Isabelle_Sidekick.int_to_pos - val root = data.root val snapshot = Swing_Thread.now { model.snapshot() } // FIXME cover all nodes (!??) for { @@ -106,19 +119,9 @@ if command.is_command && !stopped } { - val name = command.name val node = - new DefaultMutableTreeNode(new IAsset { - override def getIcon: Icon = null - override def getShortString: String = name - override def getLongString: String = name - override def getName: String = name - override def setName(name: String) = () - override def setStart(start: Position) = () - override def getStart: Position = command_start - override def setEnd(end: Position) = () - override def getEnd: Position = command_start + command.length - override def toString = name}) + new DefaultMutableTreeNode( + new Isabelle_Sidekick.Asset(command.name, command_start, command_start + command.length)) root.add(node) } } @@ -129,8 +132,6 @@ { def parser(data: SideKickParsedData, model: Document_Model) { - import Isabelle_Sidekick.int_to_pos - val root = data.root val snapshot = Swing_Thread.now { model.snapshot() } // FIXME cover all nodes (!??) for ((command, command_start) <- snapshot.node.command_range() if !stopped) { @@ -145,18 +146,12 @@ case x => x.toString } - new DefaultMutableTreeNode(new IAsset { - override def getIcon: Icon = null - override def getShortString: String = content - override def getLongString: String = info_text - override def getName: String = command.toString - override def setName(name: String) = () - override def setStart(start: Position) = () - override def getStart: Position = range.start - override def setEnd(end: Position) = () - override def getEnd: Position = range.stop - override def toString = "\"" + content + "\" " + range.toString - }) + new DefaultMutableTreeNode( + new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) { + override def getShortString: String = content + override def getLongString: String = info_text + override def toString = "\"" + content + "\" " + range.toString + }) }) } }