--- a/src/Tools/jEdit/dist-template/properties/jedit.props Sat Aug 22 23:24:15 2009 +0200
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props Thu Aug 27 11:06:25 2009 +0200
@@ -189,3 +189,4 @@
isabelle-state.dock-position=bottom
isabelle-output.dock-position=bottom
isabelle-browser.dock-position=bottom
+isabelle.activate.shortcut=CS+ENTER
--- a/src/Tools/jEdit/src/jedit/BrowseVersionDockable.scala Sat Aug 22 23:24:15 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/BrowseVersionDockable.scala Thu Aug 27 11:06:25 2009 +0200
@@ -27,7 +27,7 @@
new javax.swing.Timer(1000, new java.awt.event.ActionListener {
override def actionPerformed(evt: java.awt.event.ActionEvent) {
list.listData = Isabelle.prover_setup(view.getBuffer).map(_.
- theory_view.get_changes).getOrElse(Nil)
+ theory_view.changes).getOrElse(Nil)
}
}).start()
--- a/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala Sat Aug 22 23:24:15 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala Thu Aug 27 11:06:25 2009 +0200
@@ -52,7 +52,6 @@
val document = theory_view.current_document()
val offset = theory_view.from_current(document, original_offset)
val cmd = document.find_command_at(offset)
- val state = document.states(cmd)
if (cmd != null) {
val ref_o = cmd.ref_at(document, offset - cmd.start(document))
if (!ref_o.isDefined) null
--- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala Sat Aug 22 23:24:15 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala Thu Aug 27 11:06:25 2009 +0200
@@ -30,7 +30,7 @@
val data = new SideKickParsedData(buffer.getName)
- val prover_setup = Isabelle.plugin.prover_setup(buffer)
+ val prover_setup = Isabelle.prover_setup(buffer)
if (prover_setup.isDefined) {
val document = prover_setup.get.theory_view.current_document()
for (command <- document.commands)
--- a/src/Tools/jEdit/src/jedit/OutputDockable.scala Sat Aug 22 23:24:15 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/OutputDockable.scala Thu Aug 27 11:06:25 2009 +0200
@@ -8,7 +8,7 @@
package isabelle.jedit
-import java.awt.{Dimension, GridLayout}
+import java.awt.{Dimension, Graphics, GridLayout}
import javax.swing.{JPanel, JTextArea, JScrollPane}
import org.gjt.sp.jedit.View
@@ -22,4 +22,10 @@
setLayout(new GridLayout(1, 1))
add(new JScrollPane(new JTextArea))
+
+ def set_text(output_text_view: JTextArea) {
+ removeAll()
+ add(new JScrollPane(output_text_view))
+ revalidate()
+ }
}
--- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Sat Aug 22 23:24:15 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Thu Aug 27 11:06:25 2009 +0200
@@ -25,9 +25,7 @@
{
private val WIDTH = 10
- private val HILITE_HEIGHT = 2
-
- val repaint_delay = Swing_Thread.delay(100){ repaint() }
+ private val HILITE_HEIGHT = 2
setRequestFocusEnabled(false);
@@ -39,27 +37,27 @@
}
})
- override def addNotify {
- super.addNotify();
- ToolTipManager.sharedInstance.registerComponent(this);
- }
+ override def addNotify {
+ super.addNotify();
+ ToolTipManager.sharedInstance.registerComponent(this);
+ }
- override def removeNotify()
- {
- super.removeNotify
- ToolTipManager.sharedInstance.unregisterComponent(this);
- }
+ override def removeNotify()
+ {
+ super.removeNotify
+ ToolTipManager.sharedInstance.unregisterComponent(this);
+ }
- override def getToolTipText(evt : MouseEvent) : String =
- {
- val buffer = textarea.getBuffer
- val lineCount = buffer.getLineCount
- val line = yToLine(evt.getY())
- if (line >= 0 && line < textarea.getLineCount)
- {
+ override def getToolTipText(evt : MouseEvent) : String =
+ {
+ val buffer = textarea.getBuffer
+ val lineCount = buffer.getLineCount
+ val line = yToLine(evt.getY())
+ if (line >= 0 && line < textarea.getLineCount)
+ {
"TODO: Tooltip"
} else ""
- }
+ }
private def paintCommand(command : Command, buffer : JEditBuffer, doc: ProofDocument, gfx : Graphics) {
val line1 = buffer.getLineOfOffset(to_current(doc, command.start(doc)))
@@ -80,22 +78,22 @@
}
}
- override def paintComponent(gfx : Graphics) {
- super.paintComponent(gfx)
- val buffer = textarea.getBuffer
+override def paintComponent(gfx : Graphics) {
+ super.paintComponent(gfx)
+ val buffer = textarea.getBuffer
val theory_view = Isabelle.prover_setup(buffer).get.theory_view
val document = theory_view.current_document()
+
for (c <- document.commands)
paintCommand(c, buffer, document, gfx)
+ }
- }
-
- override def getPreferredSize = new Dimension(10,0)
+override def getPreferredSize = new Dimension(10,0)
- private def lineToY(line : Int) : Int =
- (line * getHeight) / (textarea.getBuffer.getLineCount max textarea.getVisibleLines)
+private def lineToY(line : Int) : Int =
+ (line * getHeight) / (textarea.getBuffer.getLineCount max textarea.getVisibleLines)
- private def yToLine(y : Int) : Int =
- (y * (textarea.getBuffer.getLineCount max textarea.getVisibleLines)) / getHeight
+private def yToLine(y : Int) : Int =
+ (y * (textarea.getBuffer.getLineCount max textarea.getVisibleLines)) / getHeight
}
\ No newline at end of file
--- a/src/Tools/jEdit/src/jedit/Plugin.scala Sat Aug 22 23:24:15 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/Plugin.scala Thu Aug 27 11:06:25 2009 +0200
@@ -96,6 +96,15 @@
}
+ /* selected state */
+
+ val state_update = new EventBus[Command]
+
+ private var _selected_state: Command = null
+ def selected_state = _selected_state
+ def selected_state_=(state: Command) { _selected_state = state; state_update.event(state) }
+
+
/* mapping buffer <-> prover */
private val mapping = new mutable.HashMap[JEditBuffer, ProverSetup]
@@ -124,34 +133,16 @@
override def handleMessage(msg: EBMessage)
{
msg match {
- case epu: EditPaneUpdate => epu.getWhat match {
- case EditPaneUpdate.BUFFER_CHANGED =>
- mapping get epu.getEditPane.getBuffer match {
- // only activate 'isabelle' buffers
- case None =>
- case Some(prover_setup) =>
- prover_setup.theory_view.activate
- val dockable =
- epu.getEditPane.getView.getDockableWindowManager.getDockable("isabelle-output")
- if (dockable != null) {
- val output_dockable = dockable.asInstanceOf[OutputDockable]
- 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
- }
- }
- }
- case EditPaneUpdate.BUFFER_CHANGING =>
- val buffer = epu.getEditPane.getBuffer
- if (buffer != null) mapping get buffer match {
- // only deactivate 'isabelle' buffers
- case None =>
- case Some(prover_setup) => prover_setup.theory_view.deactivate
- }
- case _ =>
- }
+ case epu: EditPaneUpdate =>
+ val buffer = epu.getEditPane.getBuffer
+ epu.getWhat match {
+ case EditPaneUpdate.BUFFER_CHANGED =>
+ (mapping get buffer) map (_.theory_view.activate)
+ case EditPaneUpdate.BUFFER_CHANGING =>
+ if (buffer != null)
+ (mapping get buffer) map (_.theory_view.deactivate)
+ case _ =>
+ }
case _ =>
}
}
--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala Sat Aug 22 23:24:15 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala Thu Aug 27 11:06:25 2009 +0200
@@ -19,58 +19,20 @@
import javax.swing.{JTextArea, JScrollPane}
-class ProverSetup(buffer: JEditBuffer)
+class ProverSetup(buffer: Buffer)
{
var prover: Prover = null
var theory_view: TheoryView = null
- val state_update = new EventBus[Command]
-
- private var _selected_state: Command = null
- def selected_state = _selected_state
- def selected_state_=(state: Command) { _selected_state = state; state_update.event(state) }
-
- val output_text_view = new JTextArea
def activate(view: View)
{
- prover = new Prover(Isabelle.system, Isabelle.default_logic)
- prover.start() // start actor
- val buffer = view.getBuffer
-
- theory_view = new TheoryView(view.getTextArea, prover)
- prover.set_document(theory_view.change_receiver, buffer.getName)
+ // TheoryView starts prover
+ theory_view = new TheoryView(view.getTextArea)
+ prover = theory_view.prover
- // register output-view
- prover.output_info += (text =>
- {
- output_text_view.append(text + "\n")
- val dockable = view.getDockableWindowManager.getDockable("isabelle-output")
- // link process output if dockable is active
- if (dockable != null) {
- val output_dockable = dockable.asInstanceOf[OutputDockable]
- 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
- }
- }
- })
-
- // register for state-view
- state_update += (cmd => {
- val state_view = view.getDockableWindowManager.getDockable("isabelle-state")
- val state_panel =
- if (state_view != null) state_view.asInstanceOf[StateViewDockable].panel
- else null
- if (state_panel != null) {
- if (cmd == null)
- state_panel.setDocument(null: Document)
- else
- state_panel.setDocument(cmd.result_document(theory_view.current_document()),
- UserAgent.base_URL)
- }
- })
+ theory_view.activate()
+ prover.set_document(buffer.getName)
}
--- a/src/Tools/jEdit/src/jedit/StateViewDockable.scala Sat Aug 22 23:24:15 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/StateViewDockable.scala Thu Aug 27 11:06:25 2009 +0200
@@ -59,6 +59,15 @@
// scrolling
add(new FSScrollPane(panel), BorderLayout.CENTER)
+ // register for state-view
+ Isabelle.plugin.state_update += (cmd => {
+ val theory_view = Isabelle.prover_setup(view.getBuffer).get.theory_view
+ if (cmd == null)
+ panel.setDocument(null: org.w3c.dom.Document)
+ else
+ panel.setDocument(cmd.result_document(theory_view.current_document()),
+ UserAgent.base_URL)
+ })
private val fontResolver =
panel.getSharedContext.getFontResolver.asInstanceOf[AWTFontResolver]
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala Sat Aug 22 23:24:15 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Thu Aug 27 11:06:25 2009 +0200
@@ -39,37 +39,28 @@
}
-class TheoryView (text_area: JEditTextArea, document_actor: Actor)
+class TheoryView (text_area: JEditTextArea)
extends TextAreaExtension with BufferListener
{
-
- def id() = Isabelle.system.id()
- private val buffer = text_area.getBuffer
- private val prover = Isabelle.prover_setup(buffer).get.prover
-
+ val buffer = text_area.getBuffer
- private var edits: List[Edit] = Nil
- private val col_timer = new Timer(300, new ActionListener() {
- override def actionPerformed(e: ActionEvent) = commit
- })
-
- col_timer.stop
- col_timer.setRepeats(true)
-
-
- private val phase_overview = new PhaseOverviewPanel(prover, text_area, to_current)
+ // start prover
+ val prover: Prover = new Prover(Isabelle.system, Isabelle.default_logic, change_receiver)
+ prover.start() // start actor
/* activation */
+ private val phase_overview = new PhaseOverviewPanel(prover, text_area, to_current)
+
private val selected_state_controller = new CaretListener {
override def caretUpdate(e: CaretEvent) = {
val doc = current_document()
val cmd = doc.find_command_at(e.getDot)
if (cmd != null && doc.token_start(cmd.tokens.first) <= e.getDot &&
- Isabelle.prover_setup(buffer).get.selected_state != cmd)
- Isabelle.prover_setup(buffer).get.selected_state = cmd
+ Isabelle.plugin.selected_state != cmd)
+ Isabelle.plugin.selected_state = cmd
}
}
@@ -80,8 +71,15 @@
buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover))
buffer.addBufferListener(this)
- edits = List(Insert(0, buffer.getText(0, buffer.getLength)))
- commit
+ val dockable =
+ text_area.getView.getDockableWindowManager.getDockable("isabelle-output")
+ if (dockable != null) {
+ val output_dockable = dockable.asInstanceOf[OutputDockable]
+ val output_text_view = prover.output_text_view
+ output_dockable.set_text(output_text_view)
+ }
+
+ buffer.propertiesChanged()
}
def deactivate() {
@@ -93,27 +91,127 @@
}
- /* painting */
+ /* history of changes - TODO: seperate class?*/
+
+ private val change_0 = new Change(prover.document_0.id, None, Nil)
+ private var _changes = List(change_0)
+ def changes = _changes
+ private var current_change = change_0
+
+ private def doc_or_pred(c: Change): ProofDocument =
+ prover.document(c.id).getOrElse(doc_or_pred(c.parent.get))
+ def current_document() = doc_or_pred(current_change)
+
+ /* update to desired version */
+
+ def set_version(goal: Change) {
+ // changes in buffer must be ignored
+ buffer.removeBufferListener(this)
+
+ def apply(c: Change) = c.map {
+ case Insert(start, added) => buffer.insert(start, added)
+ case Remove(start, removed) => buffer.remove(start, removed.length)
+ }
- val update_delay = Swing_Thread.delay(500){ buffer.propertiesChanged() }
- val repaint_delay = Swing_Thread.delay(100){ repaint_all() }
-
- val change_receiver = actor {
- loop {
- react {
- case ProverEvents.Activate =>
- activate()
- case c: Command =>
- update_delay()
- repaint_delay()
- phase_overview.repaint_delay()
- case x => System.err.println("warning: change_receiver ignored " + x)
+ def unapply(c: Change) = c.toList.reverse.map {
+ case Insert(start, added) => buffer.remove(start, added.length)
+ case Remove(start, removed) => buffer.insert(start, removed)
+ }
+
+ // undo/redo changes
+ val ancs_current = current_change.ancestors
+ val ancs_goal = goal.ancestors
+ val paired = ancs_current.reverse zip ancs_goal.reverse
+ def last_common[A](xs: List[(A, A)]): Option[A] = {
+ xs match {
+ case (x, y) :: xs =>
+ if (x == y)
+ xs match {
+ case (a, b) :: ys =>
+ if (a == b) last_common(xs)
+ else Some(x)
+ case _ => Some(x)
+ }
+ else None
+ case _ => None
}
}
+ val common_anc = last_common(paired).get
+
+ ancs_current.takeWhile(_ != common_anc) map unapply
+ ancs_goal.takeWhile(_ != common_anc).reverse map apply
+
+ current_change = goal
+ // invoke repaint
+ buffer.propertiesChanged()
+ invalidate_all()
+ phase_overview.repaint()
+
+ //track changes in buffer
+ buffer.addBufferListener(this)
+ }
+
+ /* sending edits to prover */
+
+ private var edits: List[Edit] = Nil
+
+ private val col_timer = new Timer(300, new ActionListener() {
+ override def actionPerformed(e: ActionEvent) = commit
+ })
+
+ col_timer.stop
+ col_timer.setRepeats(true)
+
+ private def commit: Unit = synchronized {
+ if (!edits.isEmpty) {
+ val change = new Change(Isabelle.system.id(), Some(current_change), edits)
+ _changes ::= change
+ prover ! change
+ current_change = change
+ }
+ edits = Nil
+ if (col_timer.isRunning())
+ col_timer.stop()
}
+ private def delay_commit {
+ if (col_timer.isRunning())
+ col_timer.restart()
+ else
+ col_timer.start()
+ }
- def changes_to(doc: ProofDocument) =
+ /* BufferListener methods */
+
+ override def contentInserted(buffer: JEditBuffer,
+ start_line: Int, offset: Int, num_lines: Int, length: Int) { }
+
+ override def contentRemoved(buffer: JEditBuffer,
+ start_line: Int, offset: Int, num_lines: Int, length: Int) { }
+
+ override def preContentInserted(buffer: JEditBuffer,
+ start_line: Int, offset: Int, num_lines: Int, length: Int)
+ {
+ edits ::= Insert(offset, buffer.getText(offset, length))
+ delay_commit
+ }
+
+ override def preContentRemoved(buffer: JEditBuffer,
+ start_line: Int, start: Int, num_lines: Int, removed_length: Int)
+ {
+ edits ::= Remove(start, buffer.getText(start, removed_length))
+ delay_commit
+ }
+
+ override def bufferLoaded(buffer: JEditBuffer) { }
+ override def foldHandlerChanged(buffer: JEditBuffer) { }
+ override def foldLevelChanged(buffer: JEditBuffer, start_line: Int, end_line: Int) { }
+ override def transactionComplete(buffer: JEditBuffer) { }
+
+
+ /* transforming offsets */
+
+ private def changes_to(doc: ProofDocument) =
edits ::: current_change.ancestors(_.id == doc.id).flatten(_.toList)
def from_current(doc: ProofDocument, pos: Int) =
@@ -122,26 +220,40 @@
def to_current(doc: ProofDocument, pos: Int) =
(pos /: changes_to(doc).reverse) ((p, c) => c where_to p)
- def repaint(cmd: Command) =
+
+ private def lines_of_command(cmd: Command) =
{
val document = current_document()
- if (text_area != null) {
- val start = text_area.getLineOfOffset(to_current(document, cmd.start(document)))
- val stop = text_area.getLineOfOffset(to_current(document, cmd.stop(document)) - 1)
- text_area.invalidateLineRange(start, stop)
-
- if (Isabelle.prover_setup(buffer).get.selected_state == cmd)
- Isabelle.prover_setup(buffer).get.selected_state = cmd // update State view
- }
+ (buffer.getLineOfOffset(to_current(document, cmd.start(document))),
+ buffer.getLineOfOffset(to_current(document, cmd.stop(document))))
}
- def repaint_all()
- {
- if (text_area != null)
- text_area.invalidateLineRange(text_area.getFirstPhysicalLine, text_area.getLastPhysicalLine)
+
+ /* (re)painting */
+
+ private val update_delay = Swing_Thread.delay(500){ buffer.propertiesChanged() }
+
+ private def update_syntax(cmd: Command) {
+ val (line1, line2) = lines_of_command(cmd)
+ if (line2 >= text_area.getFirstLine &&
+ line1 <= text_area.getFirstLine + text_area.getVisibleLines)
+ update_delay()
}
- def encolor(gfx: Graphics2D,
+ private def invalidate_line(cmd: Command) =
+ {
+ val (start, stop) = lines_of_command(cmd)
+ text_area.invalidateLineRange(start, stop)
+
+ if (Isabelle.plugin.selected_state == cmd)
+ Isabelle.plugin.selected_state = cmd // update State view
+ }
+
+ private def invalidate_all() =
+ text_area.invalidateLineRange(text_area.getFirstPhysicalLine,
+ text_area.getLastPhysicalLine)
+
+ private def encolor(gfx: Graphics2D,
y: Int, height: Int, begin: Int, finish: Int, color: Color, fill: Boolean)
{
val start = text_area.offsetToXY(begin)
@@ -161,7 +273,6 @@
}
}
-
/* TextAreaExtension methods */
override def paintValidLine(gfx: Graphics2D,
@@ -197,111 +308,28 @@
} else null
}
- /* history of changes - TODO: seperate class?*/
- val change_0 = new Change(prover.document_0.id, None, Nil)
- private var changes = List(change_0)
- private var current_change = change_0
- def get_changes = changes
-
- private def doc_or_pred(c: Change): ProofDocument =
- prover.document(c.id).getOrElse(doc_or_pred(c.parent.get))
- def current_document() = doc_or_pred(current_change)
-
- /* update to desired version */
-
- def set_version(goal: Change) {
- // changes in buffer must be ignored
- buffer.removeBufferListener(this)
-
- def apply(c: Change) = c.map {
- case Insert(start, added) => buffer.insert(start, added)
- case Remove(start, removed) => buffer.remove(start, removed.length)
- }
+ /* receiving from prover */
- def unapply(c: Change) = c.map {
- case Insert(start, added) => buffer.remove(start, added.length)
- case Remove(start, removed) => buffer.insert(start, removed)
- }
-
- // undo/redo changes
- val ancs_current = current_change.ancestors
- val ancs_goal = goal.ancestors
- val paired = ancs_current.reverse zip ancs_goal.reverse
- def last_common[A](xs: List[(A, A)]): Option[A] = {
- xs match {
- case (x, y) :: xs =>
- if (x == y)
- xs match {
- case (a, b) :: ys =>
- if (a == b) last_common(xs)
- else Some(x)
- case _ => Some(x)
+ lazy val change_receiver: Actor = actor {
+ loop {
+ react {
+ case ProverEvents.Activate =>
+ edits = List(Insert(0, buffer.getText(0, buffer.getLength)))
+ commit
+ case c: Command =>
+ if(current_document().commands.contains(c))
+ Swing_Thread.later {
+ // repaint if buffer is active
+ if(text_area.getBuffer == buffer) {
+ update_syntax(c)
+ invalidate_line(c)
+ phase_overview.repaint()
}
- else None
- case _ => None
+ }
+ case x => System.err.println("warning: change_receiver ignored " + x)
}
}
- val common_anc = last_common(paired).get
-
- ancs_current.takeWhile(_ != common_anc) map unapply
- ancs_goal.takeWhile(_ != common_anc).reverse map apply
-
- current_change = goal
- // invoke repaint
- update_delay()
- repaint_delay()
- phase_overview.repaint_delay()
-
- //track changes in buffer
- buffer.addBufferListener(this)
- }
-
- /* BufferListener methods */
-
- private def commit: Unit = synchronized {
- if (!edits.isEmpty) {
- val change = new Change(Isabelle.system.id(), Some(current_change), edits)
- changes ::= change
- document_actor ! change
- current_change = change
- }
- edits = Nil
- if (col_timer.isRunning())
- col_timer.stop()
}
- private def delay_commit {
- if (col_timer.isRunning())
- col_timer.restart()
- else
- col_timer.start()
- }
-
-
- override def contentInserted(buffer: JEditBuffer,
- start_line: Int, offset: Int, num_lines: Int, length: Int) { }
-
- override def contentRemoved(buffer: JEditBuffer,
- start_line: Int, offset: Int, num_lines: Int, length: Int) { }
-
- override def preContentInserted(buffer: JEditBuffer,
- start_line: Int, offset: Int, num_lines: Int, length: Int)
- {
- edits ::= Insert(offset, buffer.getText(offset, length))
- delay_commit
- }
-
- override def preContentRemoved(buffer: JEditBuffer,
- start_line: Int, start: Int, num_lines: Int, removed_length: Int)
- {
- edits ::= Remove(start, buffer.getText(start, removed_length))
- delay_commit
- }
-
- override def bufferLoaded(buffer: JEditBuffer) { }
- override def foldHandlerChanged(buffer: JEditBuffer) { }
- override def foldLevelChanged(buffer: JEditBuffer, start_line: Int, end_line: Int) { }
- override def transactionComplete(buffer: JEditBuffer) { }
-
}
--- a/src/Tools/jEdit/src/proofdocument/Change.scala Sat Aug 22 23:24:15 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/Change.scala Thu Aug 27 11:06:25 2009 +0200
@@ -15,7 +15,8 @@
case class Insert(start: Int, added: String) extends Edit {
def from_where(x: Int) =
- if (start <= x && start + added.length <= x) x - added.length else x
+ if (start > x) x
+ else (x - added.length) max start
def where_to(x: Int) =
if (start <= x) x + added.length else x
@@ -26,7 +27,8 @@
if (start <= x) x + removed.length else x
def where_to(x: Int) =
- if (start <= x && start + removed.length <= x) x - removed.length else x
+ if (start > x) x
+ else (x - removed.length) max start
}
// TODO: merge multiple inserts?
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Sat Aug 22 23:24:15 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Thu Aug 27 11:06:25 2009 +0200
@@ -8,9 +8,11 @@
package isabelle.proofdocument
+import scala.actors.Actor
+import scala.actors.Actor._
import scala.collection.mutable.ListBuffer
import java.util.regex.Pattern
-import isabelle.prover.{Prover, Command}
+import isabelle.prover.{Prover, Command, Command_State}
import isabelle.utils.LinearSet
@@ -34,7 +36,8 @@
val empty =
new ProofDocument(isabelle.jedit.Isabelle.system.id(),
- LinearSet(), Map(), LinearSet(), Map(), _ => false)
+ LinearSet(), Map(), LinearSet(), Map(), _ => false,
+ actor(loop(react{case _ =>}))) // ignoring actor
type StructureChange = List[(Option[Command], Option[Command])]
@@ -45,13 +48,17 @@
val tokens: LinearSet[Token],
val token_start: Map[Token, Int],
val commands: LinearSet[Command],
- var states: Map[Command, IsarDocument.State_ID],
- is_command_keyword: String => Boolean)
+ var states: Map[Command, Command_State],
+ is_command_keyword: String => Boolean,
+ change_receiver: Actor)
{
import ProofDocument.StructureChange
def set_command_keyword(f: String => Boolean): ProofDocument =
- new ProofDocument(id, tokens, token_start, commands, states, f)
+ new ProofDocument(id, tokens, token_start, commands, states, f, change_receiver)
+
+ def set_change_receiver(cr: Actor): ProofDocument =
+ new ProofDocument(id, tokens, token_start, commands, states, is_command_keyword, cr)
def content = Token.string_from_tokens(Nil ++ tokens, token_start)
@@ -192,7 +199,7 @@
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)
+ new Command(t :: cmd, new_token_start, change_receiver) :: tokens_to_commands(rest)
}
}
@@ -209,11 +216,15 @@
} else Nil
val split_end =
- if (after_change.isDefined && cmd_after_change.isDefined) {
+ if (after_change.isDefined) {
val unchanged = new_tokens.dropWhile(_ != after_change.get)
- if (unchanged.exists(_ == cmd_after_change.get.tokens.first))
- unchanged.takeWhile(_ != cmd_after_change.get.tokens.first).toList
- else Nil
+ if(cmd_after_change.isDefined) {
+ if (unchanged.exists(_ == cmd_after_change.get.tokens.first))
+ unchanged.takeWhile(_ != cmd_after_change.get.tokens.first).toList
+ else Nil
+ } else {
+ unchanged
+ }
} else Nil
val rescan_begin =
@@ -229,8 +240,8 @@
insert_after(cmd_before_change, inserted_commands)
val doc =
- new ProofDocument(new_id, new_tokenset, new_token_start,
- new_commandset, states -- removed_commands, is_command_keyword)
+ new ProofDocument(new_id, new_tokenset, new_token_start, new_commandset,
+ states -- removed_commands, is_command_keyword, change_receiver)
val removes =
for (cmd <- removed_commands) yield (cmd_before_change -> None)
--- a/src/Tools/jEdit/src/prover/Command.scala Sat Aug 22 23:24:15 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala Thu Aug 27 11:06:25 2009 +0200
@@ -8,8 +8,8 @@
package isabelle.prover
-import javax.swing.text.Position
-import javax.swing.tree.DefaultMutableTreeNode
+import scala.actors.Actor
+import scala.actors.Actor._
import scala.collection.mutable
@@ -19,6 +19,23 @@
import sidekick.{SideKickParsedData, IAsset}
+trait Accumulator extends Actor
+{
+
+ start() // start actor
+
+ protected var _state: State
+ def state = _state
+
+ override def act() {
+ loop {
+ react {
+ case x: XML.Tree => _state += x
+ }
+ }
+ }
+}
+
object Command
{
@@ -31,13 +48,17 @@
}
-class Command(val tokens: List[Token], val starts: Map[Token, Int])
+class Command(val tokens: List[Token], val starts: Map[Token, Int], chg_rec: Actor)
+extends Accumulator
{
require(!tokens.isEmpty)
val id = Isabelle.system.id()
override def hashCode = id.hashCode
+ def changed() = chg_rec ! this
+
+
/* content */
override def toString = name
@@ -51,113 +72,82 @@
def contains(p: Token) = tokens.contains(p)
- /* states */
- val states = mutable.Map[IsarDocument.State_ID, Command_State]()
- private def state(doc: ProofDocument) = doc.states.get(this)
-
- /* command status */
+ protected override var _state = State.empty(this)
+
+
+ /* markup */
- def set_status(state: IsarDocument.State_ID, status: Command.Status.Value) = {
- if (state != null)
- states.getOrElseUpdate(state, new Command_State(this)).status = status
+ lazy val empty_root_node =
+ new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length,
+ Nil, id, content, RootInfo())
+
+ def markup_node(begin: Int, end: Int, info: MarkupInfo) = {
+ new MarkupNode(this, symbol_index.decode(begin), symbol_index.decode(end), Nil, id,
+ content.substring(symbol_index.decode(begin), symbol_index.decode(end)),
+ info)
}
- def status(doc: ProofDocument) =
- state(doc) match {
- case Some(s) => states.getOrElseUpdate(s, new Command_State(this)).status
- case _ => Command.Status.UNPROCESSED
- }
+
+ /* results, markup, ... */
- /* results */
+ private val empty_cmd_state = new Command_State(this)
+ private def cmd_state(doc: ProofDocument) =
+ doc.states.getOrElse(this, empty_cmd_state)
- private val results = new mutable.ListBuffer[XML.Tree]
- def add_result(state: IsarDocument.State_ID, tree: XML.Tree) = synchronized {
- (if (state == null) results else states(state).results) += tree
- }
+ def status(doc: ProofDocument) = cmd_state(doc).state.status
+ def result_document(doc: ProofDocument) = cmd_state(doc).result_document
+ def markup_root(doc: ProofDocument) = cmd_state(doc).markup_root
+ def highlight_node(doc: ProofDocument) = cmd_state(doc).highlight_node
+ def type_at(doc: ProofDocument, offset: Int) = cmd_state(doc).type_at(offset)
+ def ref_at(doc: ProofDocument, offset: Int) = cmd_state(doc).ref_at(offset)
+}
+
- def result_document(doc: ProofDocument) = {
- val state_results = state(doc) match {
- case Some(s) =>
- states.getOrElseUpdate(s, new Command_State(this)).results
- case _ => Nil}
+class Command_State(val cmd: Command)
+extends Accumulator
+{
+
+ protected override var _state = State.empty(cmd)
+
+
+ // combining command and state
+ def result_document = {
+ val cmd_results = cmd.state.results
XML.document(
- results.toList ::: state_results.toList match {
+ cmd_results.toList ::: state.results.toList match {
case Nil => XML.Elem("message", Nil, Nil)
case List(elem) => elem
case elems => XML.Elem("messages", Nil, elems)
}, "style")
}
-
- /* markup */
-
- val empty_root_node =
- new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length,
- Nil, id, content, RootInfo())
- private var _markup_root = empty_root_node
- def add_markup(state: IsarDocument.State_ID, raw_node: MarkupNode) = {
- // decode node
- val node = raw_node transform symbol_index.decode
- if (state == null) _markup_root += node
- else {
- val cmd_state = states.getOrElseUpdate(state, new Command_State(this))
- cmd_state.markup_root += node
- }
+ def markup_root: MarkupNode = {
+ val cmd_markup_root = cmd.state.markup_root
+ (cmd_markup_root /: state.markup_root.children) (_ + _)
}
- def markup_root(doc: ProofDocument): MarkupNode = {
- state(doc) match {
- case Some(s) =>
- (_markup_root /: states(s).markup_root.children) (_ + _)
- case _ => _markup_root
- }
- }
-
- def highlight_node(doc: ProofDocument): MarkupNode =
+ def highlight_node: MarkupNode =
{
import MarkupNode._
- markup_root(doc).filter(_.info match {
- case RootInfo() | OuterInfo(_) | HighlightInfo(_) => true
+ markup_root.filter(_.info match {
+ case RootInfo() | HighlightInfo(_) => true
case _ => false
}).head
}
- 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)
-
- def type_at(doc: ProofDocument, pos: Int) =
- state(doc).map(states(_).type_at(pos)).getOrElse(null)
-
- def ref_at(doc: ProofDocument, pos: Int) =
- state(doc).flatMap(states(_).ref_at(pos))
-
-}
-
-class Command_State(val cmd: Command) {
-
- var status = Command.Status.UNPROCESSED
-
- /* results */
- val results = new mutable.ListBuffer[XML.Tree]
-
- /* markup */
- val empty_root_node = cmd.empty_root_node
- var markup_root = empty_root_node
-
def type_at(pos: Int): String =
{
- val types = markup_root.filter(_.info match { case TypeInfo(_) => true case _ => false })
+ val types = state.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 _ => "" })).
- getOrElse(null)
+ find(t => t.start <= pos && t.stop > pos).
+ 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 }).
+ state.markup_root.
+ filter(_.info match { case RefInfo(_, _, _, _) => true case _ => false }).
flatten(_.flatten).
find(t => t.start <= pos && t.stop > pos)
}
--- a/src/Tools/jEdit/src/prover/MarkupNode.scala Sat Aug 22 23:24:15 2009 +0200
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala Thu Aug 27 11:06:25 2009 +0200
@@ -15,8 +15,6 @@
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
@@ -56,9 +54,6 @@
val id: String, val content: String, val info: MarkupInfo)
{
- def transform(f: Int => Int): MarkupNode = new MarkupNode(base,
- f(start), f(stop), children map (_ transform f), id, content, info)
-
def swing_node(doc: ProofDocument): DefaultMutableTreeNode = {
val node = MarkupNode.markup2default_node (this, base, doc)
children.map(node add _.swing_node(doc))
--- a/src/Tools/jEdit/src/prover/Prover.scala Sat Aug 22 23:24:15 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala Thu Aug 27 11:06:25 2009 +0200
@@ -16,6 +16,7 @@
import scala.actors.Actor._
import org.gjt.sp.util.Log
+import javax.swing.JTextArea
import isabelle.jedit.Isabelle
import isabelle.proofdocument.{ProofDocument, Change, Token}
@@ -25,7 +26,8 @@
case class Activate
}
-class Prover(isabelle_system: Isabelle_System, logic: String) extends Actor
+class Prover(isabelle_system: Isabelle_System, logic: String, change_receiver: Actor)
+extends Actor
{
/* prover process */
@@ -41,12 +43,14 @@
/* document state information */
- private val states = new mutable.HashMap[IsarDocument.State_ID, Command] with
- mutable.SynchronizedMap[IsarDocument.State_ID, Command]
+ private val states = new mutable.HashMap[IsarDocument.State_ID, Command_State] with
+ mutable.SynchronizedMap[IsarDocument.State_ID, Command_State]
private val commands = new mutable.HashMap[IsarDocument.Command_ID, Command] with
mutable.SynchronizedMap[IsarDocument.Command_ID, Command]
val document_0 =
- ProofDocument.empty.set_command_keyword(command_decls.contains)
+ ProofDocument.empty.
+ set_command_keyword(command_decls.contains).
+ set_change_receiver(change_receiver)
private var document_versions = List(document_0)
def command(id: IsarDocument.Command_ID): Option[Command] = commands.get(id)
@@ -83,144 +87,86 @@
/* event handling */
+ lazy val output_info = new EventBus[Isabelle_Process.Result]
- val output_info = new EventBus[String]
- var change_receiver: Actor = null
-
+ val output_text_view = new JTextArea
+ output_info += (result => output_text_view.append(result.toString + "\n"))
+
private def handle_result(result: Isabelle_Process.Result)
{
- def command_change(c: Command) = change_receiver ! c
- val (state, command) =
+ val state =
result.props.find(p => p._1 == Markup.ID) match {
- case None => (null, null)
+ case None => None
case Some((_, id)) =>
- if (commands.contains(id)) (null, commands(id))
- else if (states.contains(id)) (id, states(id))
- else (null, null)
+ if (commands.contains(id)) Some(commands(id))
+ else if (states.contains(id)) Some(states(id))
+ else None
+ }
+ output_info.event(result)
+ val message =
+ try{process.parse_message(result)}
+ /* handle_results can be called before val process is initialized */
+ catch {
+ case e: NullPointerException =>
+ System.err.println("NPE; did not handle_result: " + result)
}
- if (result.kind == Isabelle_Process.Kind.STDOUT ||
- result.kind == Isabelle_Process.Kind.STDIN)
- output_info.event(result.toString)
- else {
- result.kind match {
+ if (state.isDefined) state.get ! message
+ else result.kind match {
- case Isabelle_Process.Kind.WRITELN
- | Isabelle_Process.Kind.PRIORITY
- | Isabelle_Process.Kind.WARNING
- | Isabelle_Process.Kind.ERROR =>
- if (command != null) {
- if (result.kind == Isabelle_Process.Kind.ERROR)
- command.set_status(state, Command.Status.FAILED)
- command.add_result(state, process.parse_message(result))
- command_change(command)
- } else {
- output_info.event(result.toString)
- }
+ case Isabelle_Process.Kind.STATUS =>
+ //{{{ handle all kinds of status messages here
+ message match {
+ case XML.Elem(Markup.MESSAGE, _, elems) =>
+ for (elem <- elems) {
+ elem match {
+ //{{{
+ // command and keyword declarations
+ case XML.Elem(Markup.COMMAND_DECL,
+ (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
+ command_decls += (name -> kind)
+ case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>
+ keyword_decls += name
- case Isabelle_Process.Kind.STATUS =>
- //{{{ handle all kinds of status messages here
- process.parse_message(result) match {
- case XML.Elem(Markup.MESSAGE, _, elems) =>
- for (elem <- elems) {
- elem match {
- //{{{
- // command and keyword declarations
- case XML.Elem(Markup.COMMAND_DECL,
- (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
- command_decls += (name -> kind)
- case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>
- keyword_decls += name
+ // process ready (after initialization)
+ case XML.Elem(Markup.READY, _, _)
+ if !initialized =>
+ initialized = true
+ change_receiver ! ProverEvents.Activate
- // process ready (after initialization)
- case XML.Elem(Markup.READY, _, _)
- if !initialized =>
- initialized = true
- change_receiver ! ProverEvents.Activate
-
- // document edits
- case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits)
- if document_versions.exists(_.id == doc_id) =>
- output_info.event(result.toString)
- val doc = document_versions.find(_.id == doc_id).get
- for {
- XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
- <- edits
- } {
- if (commands.contains(cmd_id)) {
- val cmd = commands(cmd_id)
- states(state_id) = cmd
- doc.states += (cmd -> state_id)
- cmd.states += (state_id -> new Command_State(cmd))
- command_change(cmd)
- }
-
+ // document edits
+ case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits)
+ if document_versions.exists(_.id == doc_id) =>
+ val doc = document_versions.find(_.id == doc_id).get
+ for {
+ XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
+ <- edits
+ } {
+ if (commands.contains(cmd_id)) {
+ val cmd = commands(cmd_id)
+ val state = new Command_State(cmd)
+ states(state_id) = state
+ doc.states += (cmd -> state)
}
- // command status
- case XML.Elem(Markup.UNPROCESSED, _, _)
- if command != null =>
- output_info.event(result.toString)
- command.set_status(state, Command.Status.UNPROCESSED)
- command_change(command)
- case XML.Elem(Markup.FINISHED, _, _)
- if command != null =>
- output_info.event(result.toString)
- command.set_status(state, Command.Status.FINISHED)
- command_change(command)
- case XML.Elem(Markup.FAILED, _, _)
- if command != null =>
- output_info.event(result.toString)
- command.set_status(state, Command.Status.FAILED)
- command_change(command)
- case XML.Elem(kind, attr, body)
- if command != null =>
- val (begin, end) = Position.offsets_of(attr)
- if (begin.isDefined && end.isDefined) {
- if (kind == Markup.ML_TYPING) {
- val info = body.first.asInstanceOf[XML.Text].content
- command.add_markup(state,
- command.markup_node(begin.get - 1, end.get - 1, TypeInfo(info)))
- } else if (kind == Markup.ML_REF) {
- body match {
- case List(XML.Elem(Markup.ML_DEF, attr, _)) =>
- command.add_markup(state, command.markup_node(
- begin.get - 1, end.get - 1,
- RefInfo(
- Position.file_of(attr),
- Position.line_of(attr),
- Position.id_of(attr),
- Position.offset_of(attr))))
- case _ =>
- }
- } else {
- command.add_markup(state,
- command.markup_node(begin.get - 1, end.get - 1, HighlightInfo(kind)))
- }
- }
- command_change(command)
- case XML.Elem(kind, attr, body)
- if command == null =>
- // TODO: This is mostly irrelevant information on removed commands, but it can
- // also be outer-syntax-markup since there is no id in props (fix that?)
- val (begin, end) = Position.offsets_of(attr)
- val markup_id = Position.id_of(attr)
- val outer = isabelle.jedit.DynamicTokenMarker.is_outer(kind)
- if (outer && state == null && begin.isDefined && end.isDefined && markup_id.isDefined)
- commands.get(markup_id.get).map (cmd => {
- cmd.add_markup(state,
- cmd.markup_node(begin.get - 1, end.get - 1, OuterInfo(kind)))
- command_change(cmd)
- })
- case _ =>
- //}}}
- }
+
+ }
+ case XML.Elem(kind, attr, body) =>
+ // TODO: This is mostly irrelevant information on removed commands, but it can
+ // also be outer-syntax-markup since there is no id in props (fix that?)
+ val (begin, end) = Position.offsets_of(attr)
+ val markup_id = Position.id_of(attr)
+ val outer = isabelle.jedit.DynamicTokenMarker.is_outer(kind)
+ if (outer && begin.isDefined && end.isDefined && markup_id.isDefined)
+ commands.get(markup_id.get).map (cmd => cmd ! message)
+ case _ =>
+ //}}}
}
- case _ =>
- }
- //}}}
+ }
+ case _ =>
+ }
+ //}}}
- case _ =>
- }
+ case _ =>
}
}
@@ -239,8 +185,7 @@
}
}
- def set_document(change_receiver: Actor, path: String) {
- this.change_receiver = change_receiver
+ def set_document(path: String) {
process.begin_document(document_0.id, path)
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/prover/State.scala Thu Aug 27 11:06:25 2009 +0200
@@ -0,0 +1,101 @@
+/*
+ * Accumulating results from prover
+ *
+ * @author Fabian Immler, TU Munich
+ */
+
+package isabelle.prover
+
+import scala.collection.mutable
+
+object State
+{
+ def empty(cmd: Command) = State(cmd, Command.Status.UNPROCESSED,
+ new mutable.ListBuffer, cmd.empty_root_node)
+}
+
+case class State(
+ cmd: Command,
+ status: Command.Status.Value,
+ results: mutable.Buffer[XML.Tree],
+ markup_root: MarkupNode
+)
+{
+
+ private def set_status(st: Command.Status.Value):State =
+ State(cmd, st, results, markup_root)
+ private def add_result(res: XML.Tree):State =
+ State(cmd, status, results + res, markup_root)
+ private def add_markup(markup: MarkupNode):State =
+ State(cmd, status, results, markup_root + markup)
+ /* markup */
+
+ def type_at(pos: Int): String =
+ {
+ 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 _ => "" })).
+ getOrElse(null)
+ }
+
+ def ref_at(pos: Int): Option[MarkupNode] =
+ markup_root.filter(_.info match { case RefInfo(_, _, _, _) => true case _ => false }).
+ flatten(_.flatten).
+ find(t => t.start <= pos && t.stop > pos)
+
+ def +(message: XML.Tree) = {
+ val changed: State =
+ message match {
+ case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.WRITELN) :: _, _)
+ | XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.PRIORITY) :: _, _)
+ | XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.WARNING) :: _, _) =>
+ add_result(message)
+ case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.ERROR) :: _, _) =>
+ set_status(Command.Status.FAILED).add_result(message)
+ case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) =>
+ (this /: elems) ((r, e) =>
+ e match {
+ // command status
+ case XML.Elem(Markup.UNPROCESSED, _, _) =>
+ r.set_status(Command.Status.UNPROCESSED)
+ case XML.Elem(Markup.FINISHED, _, _) =>
+ r.set_status(Command.Status.FINISHED)
+ case XML.Elem(Markup.FAILED, _, _) =>
+ r.set_status(Command.Status.FAILED)
+ case XML.Elem(kind, attr, body) =>
+ val (begin, end) = Position.offsets_of(attr)
+ if (begin.isDefined && end.isDefined) {
+ if (kind == Markup.ML_TYPING) {
+ val info = body.first.asInstanceOf[XML.Text].content
+ r.add_markup(cmd.markup_node(begin.get - 1, end.get - 1, TypeInfo(info)))
+ } else if (kind == Markup.ML_REF) {
+ body match {
+ case List(XML.Elem(Markup.ML_DEF, attr, _)) =>
+ r.add_markup(cmd.markup_node(
+ begin.get - 1, end.get - 1,
+ RefInfo(
+ Position.file_of(attr),
+ Position.line_of(attr),
+ Position.id_of(attr),
+ Position.offset_of(attr))))
+ case _ =>
+ r
+ }
+ } else {
+ r.add_markup(cmd.markup_node(begin.get - 1, end.get - 1, HighlightInfo(kind)))
+ }
+ } else
+ r
+ case _ =>
+ r
+ })
+ case _ =>
+ System.err.println("ignored: " + message)
+ this
+ }
+ cmd.changed()
+ changed
+ }
+
+}