--- a/src/Tools/jEdit/plugin/actions.xml Tue Dec 15 13:39:30 2009 +0100
+++ b/src/Tools/jEdit/plugin/actions.xml Tue Dec 15 19:53:35 2009 +0100
@@ -4,10 +4,10 @@
<ACTIONS>
<ACTION NAME="isabelle.activate">
<CODE>
- isabelle.jedit.Isabelle.plugin().switch_active(view);
+ isabelle.jedit.Isabelle.switch_active(view);
</CODE>
<IS_SELECTED>
- return isabelle.jedit.Isabelle.plugin().is_active(view.getBuffer());
+ return isabelle.jedit.Isabelle.is_active(view);
</IS_SELECTED>
</ACTION>
<ACTION NAME="isabelle.show-output">
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/document_model.scala Tue Dec 15 19:53:35 2009 +0100
@@ -0,0 +1,194 @@
+/*
+ * Document model connected to jEdit buffer
+ *
+ * @author Fabian Immler, TU Munich
+ * @author Makarius
+ */
+
+package isabelle.jedit
+
+
+import isabelle.proofdocument.{Change, Command, Edit, Insert, Remove, Proof_Document, Session}
+
+import scala.actors.Actor, Actor._
+import scala.collection.mutable
+
+import org.gjt.sp.jedit.Buffer
+import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
+import org.gjt.sp.jedit.syntax.{ModeProvider, SyntaxStyle}
+
+
+object Document_Model
+{
+ /* document model of buffer */
+
+ private val key = "isabelle.document_model"
+
+ def init(session: Session, buffer: Buffer): Document_Model =
+ {
+ val model = new Document_Model(session, buffer)
+ buffer.setProperty(key, model)
+ model.activate()
+ model
+ }
+
+ def get(buffer: Buffer): Option[Document_Model] =
+ {
+ buffer.getProperty(key) match {
+ case model: Document_Model => Some(model)
+ case _ => None
+ }
+ }
+
+ def exit(buffer: Buffer)
+ {
+ get(buffer) match {
+ case None => error("No document model for buffer: " + buffer)
+ case Some(model) =>
+ model.deactivate()
+ buffer.unsetProperty(key)
+ }
+ }
+}
+
+class Document_Model(val session: Session, val buffer: Buffer)
+{
+ /* changes vs. edits */
+
+ private val change_0 = new Change(Isabelle.session.document_0.id, None, Nil) // FIXME !?
+ private var _changes = List(change_0) // owned by Swing/AWT thread
+ def changes = _changes
+ private var current_change = change_0
+
+ private val edits = new mutable.ListBuffer[Edit] // owned by Swing thread
+
+ private val edits_delay = Swing_Thread.delay_last(300) {
+ if (!edits.isEmpty) {
+ val change = new Change(session.create_id(), Some(current_change), edits.toList)
+ _changes ::= change
+ session.input(change)
+ current_change = change
+ edits.clear
+ }
+ }
+
+
+ /* buffer listener */
+
+ private val buffer_listener: BufferListener = new BufferAdapter
+ {
+ override def contentInserted(buffer: JEditBuffer,
+ start_line: Int, offset: Int, num_lines: Int, length: Int)
+ {
+ edits += Insert(offset, buffer.getText(offset, length))
+ edits_delay()
+ }
+
+ override def preContentRemoved(buffer: JEditBuffer,
+ start_line: Int, start: Int, num_lines: Int, removed_length: Int)
+ {
+ edits += Remove(start, buffer.getText(start, removed_length))
+ edits_delay()
+ }
+ }
+
+
+ /* history of changes */
+
+ private def doc_or_pred(c: Change): Proof_Document =
+ session.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(buffer_listener)
+
+ def apply(change: Change): Unit =
+ change.edits.foreach {
+ case Insert(start, text) => buffer.insert(start, text)
+ case Remove(start, text) => buffer.remove(start, text.length)
+ }
+
+ def unapply(change: Change): Unit =
+ change.edits.reverse.foreach {
+ case Insert(start, text) => buffer.remove(start, text.length)
+ case Remove(start, text) => buffer.insert(start, text)
+ }
+
+ // 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() FIXME
+ // overview.repaint() FIXME
+
+ // track changes in buffer
+ buffer.addBufferListener(buffer_listener)
+ }
+
+
+ /* transforming offsets */
+
+ private def changes_from(doc: Proof_Document): List[Edit] =
+ List.flatten(current_change.ancestors(_.id == doc.id).reverse.map(_.edits)) :::
+ edits.toList
+
+ def from_current(doc: Proof_Document, offset: Int): Int =
+ (offset /: changes_from(doc).reverse) ((i, change) => change before i)
+
+ def to_current(doc: Proof_Document, offset: Int): Int =
+ (offset /: changes_from(doc)) ((i, change) => change after i)
+
+ def lines_of_command(cmd: Command): (Int, Int) =
+ {
+ val document = current_document()
+ (buffer.getLineOfOffset(to_current(document, cmd.start(document))),
+ buffer.getLineOfOffset(to_current(document, cmd.stop(document))))
+ }
+
+
+ /* activation */
+
+ def activate()
+ {
+ buffer.setTokenMarker(new Isabelle_Token_Marker(this)) // FIXME tune!?
+ buffer.addBufferListener(buffer_listener)
+ buffer.propertiesChanged()
+
+ edits += Insert(0, buffer.getText(0, buffer.getLength))
+ edits_delay()
+ }
+
+ def deactivate()
+ {
+ buffer.setTokenMarker(buffer.getMode.getTokenMarker)
+ buffer.removeBufferListener(buffer_listener)
+ }
+}
--- a/src/Tools/jEdit/src/jedit/document_overview.scala Tue Dec 15 13:39:30 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,81 +0,0 @@
-/*
- * Information on command status left of scrollbar (with panel)
- *
- * @author Fabian Immler, TU Munich
- */
-
-package isabelle.jedit
-
-
-import isabelle.proofdocument.{Command, Proof_Document, Theory_View}
-
-import javax.swing.{JPanel, ToolTipManager}
-import java.awt.event.{MouseAdapter, MouseEvent}
-import java.awt.{BorderLayout, Graphics, Dimension}
-
-import org.gjt.sp.jedit.gui.RolloverButton
-import org.gjt.sp.jedit.textarea.JEditTextArea
-
-
-class Document_Overview(
- text_area: JEditTextArea,
- to_current: (Proof_Document, Int) => Int)
- extends JPanel(new BorderLayout)
-{
- private val WIDTH = 10
- private val HEIGHT = 2
-
- setRequestFocusEnabled(false)
-
- addMouseListener(new MouseAdapter {
- override def mousePressed(event: MouseEvent) {
- val line = y_to_line(event.getY)
- if (line >= 0 && line < text_area.getLineCount)
- text_area.setCaretPosition(text_area.getLineStartOffset(line))
- }
- })
-
- override def addNotify() {
- super.addNotify()
- ToolTipManager.sharedInstance.registerComponent(this)
- }
-
- override def removeNotify() {
- super.removeNotify
- ToolTipManager.sharedInstance.unregisterComponent(this)
- }
-
- override def getToolTipText(event: MouseEvent): String =
- {
- val buffer = text_area.getBuffer
- val lineCount = buffer.getLineCount
- val line = y_to_line(event.getY())
- if (line >= 0 && line < text_area.getLineCount) "<html><b>TODO:</b><br>Tooltip</html>"
- else ""
- }
-
- override def paintComponent(gfx: Graphics)
- {
- super.paintComponent(gfx)
- val buffer = text_area.getBuffer
- val theory_view = Isabelle.plugin.theory_view(buffer).get
- val doc = theory_view.current_document()
-
- for (command <- doc.commands) {
- val line1 = buffer.getLineOfOffset(to_current(doc, command.start(doc)))
- val line2 = buffer.getLineOfOffset(to_current(doc, command.stop(doc))) + 1
- val y = line_to_y(line1)
- val height = HEIGHT * (line2 - line1)
- gfx.setColor(Theory_View.choose_color(command, doc))
- gfx.fillRect(0, y, getWidth - 1, height)
- }
- }
-
- override def getPreferredSize = new Dimension(WIDTH, 0)
-
- private def line_to_y(line: Int): Int =
- (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)
-
- private def y_to_line(y: Int): Int =
- (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight
-}
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Tue Dec 15 19:53:35 2009 +0100
@@ -0,0 +1,279 @@
+/*
+ * Document view connected to jEdit text area
+ *
+ * @author Fabian Immler, TU Munich
+ * @author Makarius
+ */
+
+package isabelle.jedit
+
+
+import isabelle.proofdocument.{Command, Proof_Document, Session}
+
+import scala.actors.Actor._
+
+import java.awt.event.{MouseAdapter, MouseEvent}
+import java.awt.{BorderLayout, Graphics, Dimension, Color, Graphics2D}
+import javax.swing.{JPanel, ToolTipManager}
+import javax.swing.event.{CaretListener, CaretEvent}
+
+import org.gjt.sp.jedit.gui.RolloverButton
+import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
+
+
+object Document_View
+{
+ def choose_color(command: Command, doc: Proof_Document): Color =
+ {
+ command.status(doc) match {
+ case Command.Status.UNPROCESSED => new Color(255, 228, 225)
+ case Command.Status.FINISHED => new Color(234, 248, 255)
+ case Command.Status.FAILED => new Color(255, 106, 106)
+ case _ => Color.red
+ }
+ }
+
+
+ /* document view of text area */
+
+ private val key = new Object
+
+ def init(model: Document_Model, text_area: TextArea): Document_View =
+ {
+ val doc_view = new Document_View(model, text_area)
+ text_area.putClientProperty(key, doc_view)
+ doc_view.activate()
+ doc_view
+ }
+
+ def get(text_area: TextArea): Option[Document_View] =
+ {
+ text_area.getClientProperty(key) match {
+ case doc_view: Document_View => Some(doc_view)
+ case _ => None
+ }
+ }
+
+ def exit(text_area: TextArea)
+ {
+ get(text_area) match {
+ case None => error("No document view for text area: " + text_area)
+ case Some(doc_view) =>
+ doc_view.deactivate()
+ text_area.putClientProperty(key, null)
+ }
+ }
+}
+
+
+class Document_View(model: Document_Model, text_area: TextArea)
+{
+ private val session = model.session
+
+
+ /* command change actor */
+
+ private case object Exit
+
+ private val command_change_actor = actor {
+ loop {
+ react {
+ case command: Command =>
+ if (model.current_document().commands.contains(command))
+ Swing_Thread.now {
+ update_syntax(command)
+ invalidate_line(command)
+ overview.repaint()
+ }
+
+ case Exit => reply(()); exit()
+
+ case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
+ }
+ }
+ }
+
+
+ /* text_area_extension */
+
+ private val text_area_extension = new TextAreaExtension
+ {
+ override def paintValidLine(gfx: Graphics2D,
+ screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
+ {
+ val document = model.current_document()
+ def from_current(pos: Int) = model.from_current(document, pos)
+ def to_current(pos: Int) = model.to_current(document, pos)
+ val saved_color = gfx.getColor
+
+ val metrics = text_area.getPainter.getFontMetrics
+
+ // encolor phase
+ var cmd = document.command_at(from_current(start))
+ while (cmd.isDefined && cmd.get.start(document) < end) {
+ val e = cmd.get
+ val begin = start max to_current(e.start(document))
+ val finish = (end - 1) min to_current(e.stop(document))
+ encolor(gfx, y, metrics.getHeight, begin, finish,
+ Document_View.choose_color(e, document), true)
+ cmd = document.commands.next(e)
+ }
+
+ gfx.setColor(saved_color)
+ }
+
+ override def getToolTipText(x: Int, y: Int): String =
+ {
+ val document = model.current_document()
+ val offset = model.from_current(document, text_area.xyToOffset(x, y))
+ document.command_at(offset) match {
+ case Some(cmd) =>
+ document.token_start(cmd.tokens.first)
+ cmd.type_at(document, offset - cmd.start(document)).getOrElse(null)
+ case None => null
+ }
+ }
+ }
+
+
+ /* (re)painting */
+
+ private val update_delay = Swing_Thread.delay_first(500) { model.buffer.propertiesChanged() }
+
+ private def update_syntax(cmd: Command)
+ {
+ val (line1, line2) = model.lines_of_command(cmd)
+ if (line2 >= text_area.getFirstLine &&
+ line1 <= text_area.getFirstLine + text_area.getVisibleLines)
+ update_delay()
+ }
+
+ private def invalidate_line(cmd: Command) =
+ {
+ val (start, stop) = model.lines_of_command(cmd)
+ text_area.invalidateLineRange(start, stop)
+
+ if (Isabelle.session.selected_state == cmd)
+ Isabelle.session.selected_state = cmd
+ }
+
+ 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)
+ val stop =
+ if (finish < model.buffer.getLength) text_area.offsetToXY(finish)
+ else {
+ val p = text_area.offsetToXY(finish - 1)
+ val metrics = text_area.getPainter.getFontMetrics
+ p.x = p.x + (metrics.charWidth(' ') max metrics.getMaxAdvance)
+ p
+ }
+
+ if (start != null && stop != null) {
+ gfx.setColor(color)
+ if (fill) gfx.fillRect(start.x, y, stop.x - start.x, height)
+ else gfx.drawRect(start.x, y, stop.x - start.x, height)
+ }
+ }
+
+
+ /* overview of command status left of scrollbar */
+
+ val overview = new JPanel(new BorderLayout)
+ {
+ private val WIDTH = 10
+ private val HEIGHT = 2
+
+ setRequestFocusEnabled(false)
+
+ addMouseListener(new MouseAdapter {
+ override def mousePressed(event: MouseEvent) {
+ val line = y_to_line(event.getY)
+ if (line >= 0 && line < text_area.getLineCount)
+ text_area.setCaretPosition(text_area.getLineStartOffset(line))
+ }
+ })
+
+ override def addNotify() {
+ super.addNotify()
+ ToolTipManager.sharedInstance.registerComponent(this)
+ }
+
+ override def removeNotify() {
+ ToolTipManager.sharedInstance.unregisterComponent(this)
+ super.removeNotify
+ }
+
+ override def getToolTipText(event: MouseEvent): String =
+ {
+ val line = y_to_line(event.getY())
+ if (line >= 0 && line < text_area.getLineCount) "<html><b>TODO:</b><br>Tooltip</html>"
+ else ""
+ }
+
+ override def paintComponent(gfx: Graphics)
+ {
+ super.paintComponent(gfx)
+ val doc = model.current_document()
+ val buffer = model.buffer
+
+ for (command <- doc.commands) {
+ val line1 = buffer.getLineOfOffset(model.to_current(doc, command.start(doc)))
+ val line2 = buffer.getLineOfOffset(model.to_current(doc, command.stop(doc))) + 1
+ val y = line_to_y(line1)
+ val height = HEIGHT * (line2 - line1)
+ gfx.setColor(Document_View.choose_color(command, doc))
+ gfx.fillRect(0, y, getWidth - 1, height)
+ }
+ }
+
+ override def getPreferredSize = new Dimension(WIDTH, 0)
+
+ private def line_to_y(line: Int): Int =
+ (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)
+
+ private def y_to_line(y: Int): Int =
+ (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight
+ }
+
+
+ private val selected_state_controller = new CaretListener
+ {
+ override def caretUpdate(e: CaretEvent) {
+ val doc = model.current_document()
+ doc.command_at(e.getDot) match {
+ case Some(cmd)
+ if (doc.token_start(cmd.tokens.first) <= e.getDot &&
+ Isabelle.session.selected_state != cmd) =>
+ Isabelle.session.selected_state = cmd // FIXME !?
+ case _ =>
+ }
+ }
+ }
+
+
+ /* activation */
+
+ def activate()
+ {
+ text_area.addCaretListener(selected_state_controller)
+ text_area.addLeftOfScrollBar(overview)
+ text_area.getPainter.
+ addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
+ session.command_change += command_change_actor
+ }
+
+ def deactivate()
+ {
+ session.command_change -= command_change_actor
+ command_change_actor !? Exit
+ text_area.getPainter.removeExtension(text_area_extension)
+ text_area.removeLeftOfScrollBar(overview)
+ text_area.removeCaretListener(selected_state_controller)
+ }
+}
\ No newline at end of file
--- a/src/Tools/jEdit/src/jedit/history_dockable.scala Tue Dec 15 13:39:30 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/history_dockable.scala Tue Dec 15 19:53:35 2009 +0100
@@ -7,7 +7,7 @@
package isabelle.jedit
-import isabelle.proofdocument.{Change, Theory_View}
+import isabelle.proofdocument.Change
import java.awt.Dimension
import scala.swing.{ListView, FlowPanel}
@@ -22,12 +22,10 @@
if (position == DockableWindowManager.FLOATING)
preferredSize = new Dimension(500, 250)
- def dynamic_theory_view(): Option[Theory_View] =
- Isabelle.plugin.theory_view(view.getBuffer)
def get_versions() =
- dynamic_theory_view() match {
+ Document_Model.get(view.getBuffer) match {
case None => Nil
- case Some(theory_view) => theory_view.changes
+ case Some(model) => model.changes
}
val list = new ListView[Change]
@@ -38,9 +36,9 @@
listenTo(list.selection)
reactions += {
case ListSelectionChanged(source, range, false) =>
- dynamic_theory_view().map(_.set_version(list.listData(range.start)))
+ Document_Model.get(view.getBuffer).map(_.set_version(list.listData(range.start)))
}
- if (dynamic_theory_view().isDefined)
+ if (Document_Model.get(view.getBuffer).isDefined)
Isabelle.session.document_change += (_ => list.listData = get_versions())
}
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Tue Dec 15 13:39:30 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Tue Dec 15 19:53:35 2009 +0100
@@ -45,18 +45,18 @@
{
def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink =
{
- Isabelle.plugin.theory_view(buffer) match {
- case Some(theory_view) =>
- val document = theory_view.current_document()
- val offset = theory_view.from_current(document, original_offset)
+ Document_Model.get(buffer) match {
+ case Some(model) =>
+ val document = model.current_document()
+ val offset = model.from_current(document, original_offset)
document.command_at(offset) match {
case Some(command) =>
command.ref_at(document, offset - command.start(document)) match {
case Some(ref) =>
val command_start = command.start(document)
- val begin = theory_view.to_current(document, command_start + ref.start)
+ val begin = model.to_current(document, command_start + ref.start)
val line = buffer.getLineOfOffset(begin)
- val end = theory_view.to_current(document, command_start + ref.stop)
+ val end = model.to_current(document, command_start + ref.stop)
ref.info match {
case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
new External_Hyperlink(begin, end, line, ref_file, ref_line)
@@ -64,7 +64,7 @@
Isabelle.session.command(id) match {
case Some(ref_cmd) =>
new Internal_Hyperlink(begin, end, line,
- theory_view.to_current(document, ref_cmd.start(document) + offset - 1))
+ model.to_current(document, ref_cmd.start(document) + offset - 1))
case None => null
}
case _ => null
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Tue Dec 15 13:39:30 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Tue Dec 15 19:53:35 2009 +0100
@@ -40,9 +40,9 @@
val root = data.root
data.getAsset(root).setEnd(buffer.getLength)
- Isabelle.plugin.theory_view(buffer) match {
- case Some(theory_view) =>
- val document = theory_view.current_document()
+ Document_Model.get(buffer) match {
+ case Some(model) =>
+ val document = model.current_document()
for (command <- document.commands if !stopped) {
root.add(command.markup_root(document).swing_tree((node: Markup_Node) =>
{
--- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Tue Dec 15 13:39:30 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Tue Dec 15 19:53:35 2009 +0100
@@ -99,7 +99,7 @@
}
-class Isabelle_Token_Marker(buffer: JEditBuffer) extends TokenMarker
+class Isabelle_Token_Marker(model: Document_Model) extends TokenMarker
{
override def markTokens(prev: TokenMarker.LineContext,
handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext =
@@ -107,13 +107,12 @@
val previous = prev.asInstanceOf[Isabelle_Token_Marker.LineContext]
val line = if (prev == null) 0 else previous.line + 1
val context = new Isabelle_Token_Marker.LineContext(line, previous)
- val start = buffer.getLineStartOffset(line)
+ val start = model.buffer.getLineStartOffset(line)
val stop = start + line_segment.count
- val theory_view = Isabelle.plugin.theory_view(buffer).get // FIXME total?
- val document = theory_view.current_document()
- def to: Int => Int = theory_view.to_current(document, _)
- def from: Int => Int = theory_view.from_current(document, _)
+ val document = model.current_document()
+ def to: Int => Int = model.to_current(document, _)
+ def from: Int => Int = model.from_current(document, _)
var next_x = start
var cmd = document.command_at(from(start))
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala Tue Dec 15 13:39:30 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Tue Dec 15 19:53:35 2009 +0100
@@ -42,13 +42,12 @@
loop {
react {
case cmd: Command =>
- Isabelle.plugin.theory_view(view.getBuffer) // FIXME total!?!
- match {
+ Document_Model.get(view.getBuffer) match {
case None =>
- case Some(theory_view) =>
+ case Some(model) =>
val body =
if (cmd == null) Nil // FIXME ??
- else cmd.results(theory_view.current_document)
+ else cmd.results(model.current_document)
html_panel.render(body)
}
--- a/src/Tools/jEdit/src/jedit/plugin.scala Tue Dec 15 13:39:30 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/plugin.scala Tue Dec 15 19:53:35 2009 +0100
@@ -9,7 +9,7 @@
package isabelle.jedit
-import isabelle.proofdocument.{Session, Theory_View}
+import isabelle.proofdocument.Session
import java.io.{FileInputStream, IOException}
import java.awt.Font
@@ -25,6 +25,13 @@
object Isabelle
{
+ /* plugin instance */
+
+ var plugin: Plugin = null
+ var system: Isabelle_System = null
+ var session: Session = null
+
+
/* name */
val NAME = "Isabelle"
@@ -66,7 +73,7 @@
{
val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
val logic = {
- val logic = Isabelle.Property("logic")
+ val logic = Property("logic")
if (logic != null && logic != "") logic
else default_logic()
}
@@ -74,67 +81,87 @@
}
- /* plugin instance */
+ /* main jEdit components */ // FIXME ownership!?
+
+ def jedit_buffers(): Iterator[Buffer] = Iterator.fromArray(jEdit.getBuffers())
+
+ def jedit_views(): Iterator[View] = Iterator.fromArray(jEdit.getViews())
+
+ def jedit_text_areas(view: View): Iterator[JEditTextArea] =
+ Iterator.fromArray(view.getEditPanes).map(_.getTextArea)
+
+ def jedit_text_areas(): Iterator[JEditTextArea] =
+ jedit_views().flatMap(jedit_text_areas(_))
+
+ def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
+ jedit_text_areas().filter(_.getBuffer == buffer)
+
+
+ /* activation */
+
+ def activate_buffer(buffer: Buffer)
+ {
+ val model = Document_Model.init(session, buffer)
+ for (text_area <- jedit_text_areas(buffer))
+ Document_View.init(model, text_area)
- var plugin: Plugin = null
- var system: Isabelle_System = null
- var session: Session = null
+ session.start(Isabelle.isabelle_args())
+ // FIXME theory_view.activate()
+ session.begin_document(buffer.getName)
+ }
+
+ def deactivate_buffer(buffer: Buffer)
+ {
+ session.stop() // FIXME not yet
+
+ for (text_area <- jedit_text_areas(buffer))
+ Document_View.exit(text_area)
+ Document_Model.exit(buffer)
+ }
+
+ def switch_active(view: View) =
+ {
+ val buffer = view.getBuffer
+ if (Document_Model.get(buffer).isDefined) deactivate_buffer(buffer)
+ else activate_buffer(buffer)
+ }
+
+ def is_active(view: View): Boolean =
+ Document_Model.get(view.getBuffer).isDefined
}
class Plugin extends EBPlugin
{
- /* mapping buffer <-> theory view */
-
- private var mapping = Map[JEditBuffer, Theory_View]()
-
- private def install(view: View)
- {
- val text_area = view.getTextArea
- val buffer = view.getBuffer
-
-
- val theory_view = new Theory_View(Isabelle.session, text_area) // FIXME multiple text areas!?
- mapping += (buffer -> theory_view)
-
- Isabelle.session.start(Isabelle.isabelle_args())
- theory_view.activate()
- Isabelle.session.begin_document(buffer.getName)
- }
-
- private def uninstall(view: View)
- {
- val buffer = view.getBuffer
- Isabelle.session.stop()
- mapping(buffer).deactivate()
- mapping -= buffer
- }
-
- def switch_active(view: View) =
- if (mapping.isDefinedAt(view.getBuffer)) uninstall(view)
- else install(view)
-
- def theory_view(buffer: JEditBuffer): Option[Theory_View] = mapping.get(buffer)
- def is_active(buffer: JEditBuffer) = mapping.isDefinedAt(buffer)
-
-
/* main plugin plumbing */
override def handleMessage(message: EBMessage)
{
message match {
case msg: EditPaneUpdate =>
- val buffer = msg.getEditPane.getBuffer
+ val edit_pane = msg.getEditPane
+ val buffer = edit_pane.getBuffer
+ val text_area = edit_pane.getTextArea
+
msg.getWhat match {
case EditPaneUpdate.BUFFER_CHANGED =>
- theory_view(buffer)map(_.activate)
- case EditPaneUpdate.BUFFER_CHANGING =>
- if (buffer != null)
- theory_view(buffer).map(_.deactivate)
+ if (Document_View.get(text_area).isDefined)
+ Document_View.exit(text_area)
+ Document_Model.get(buffer) match {
+ case Some(model) => Document_View.init(model, text_area)
+ case None =>
+ }
+
+ case EditPaneUpdate.DESTROYED =>
+ if (Document_View.get(text_area).isDefined)
+ Document_View.exit(text_area)
+
case _ =>
}
+
case msg: PropertiesChanged =>
Isabelle.session.global_settings.event(())
+
case _ =>
}
}
--- a/src/Tools/jEdit/src/proofdocument/theory_view.scala Tue Dec 15 13:39:30 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,305 +0,0 @@
-/*
- * jEdit text area as document text source
- *
- * @author Fabian Immler, TU Munich
- * @author Johannes Hölzl, TU Munich
- * @author Makarius
- */
-
-package isabelle.proofdocument
-
-
-import isabelle.jedit.{Document_Overview, Isabelle, Isabelle_Token_Marker} // FIXME wrong layer
-
-import scala.actors.Actor, Actor._
-import scala.collection.mutable
-
-import java.awt.{Color, Graphics2D}
-import javax.swing.event.{CaretListener, CaretEvent}
-
-import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
-import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
-import org.gjt.sp.jedit.syntax.{ModeProvider, SyntaxStyle}
-
-
-object Theory_View
-{
- def choose_color(command: Command, doc: Proof_Document): Color =
- {
- command.status(doc) match {
- case Command.Status.UNPROCESSED => new Color(255, 228, 225)
- case Command.Status.FINISHED => new Color(234, 248, 255)
- case Command.Status.FAILED => new Color(255, 106, 106)
- case _ => Color.red
- }
- }
-}
-
-
-class Theory_View(session: Session, text_area: JEditTextArea)
-{
- private val buffer = text_area.getBuffer
-
-
- /* prover setup */
-
- session.command_change += ((command: Command) =>
- if (current_document().commands.contains(command))
- Swing_Thread.later {
- // FIXME proper handling of buffer vs. text areas
- // repaint if buffer is active
- if (text_area.getBuffer == buffer) {
- update_syntax(command)
- invalidate_line(command)
- overview.repaint()
- }
- })
-
-
- /* changes vs. edits */
-
- private val change_0 = new Change(Isabelle.session.document_0.id, None, Nil) // FIXME !?
- private var _changes = List(change_0) // owned by Swing/AWT thread
- def changes = _changes
- private var current_change = change_0
-
- private val edits = new mutable.ListBuffer[Edit] // owned by Swing thread
-
- private val edits_delay = Swing_Thread.delay_last(300) {
- if (!edits.isEmpty) {
- val change = new Change(session.create_id(), Some(current_change), edits.toList)
- _changes ::= change
- session.input(change)
- current_change = change
- edits.clear
- }
- }
-
-
- /* buffer_listener */
-
- private val buffer_listener: BufferListener = new BufferAdapter {
- override def contentInserted(buffer: JEditBuffer,
- start_line: Int, offset: Int, num_lines: Int, length: Int)
- {
- edits += Insert(offset, buffer.getText(offset, length))
- edits_delay()
- }
-
- override def preContentRemoved(buffer: JEditBuffer,
- start_line: Int, start: Int, num_lines: Int, removed_length: Int)
- {
- edits += Remove(start, buffer.getText(start, removed_length))
- edits_delay()
- }
- }
-
-
- /* text_area_extension */
-
- private val text_area_extension = new TextAreaExtension {
- override def paintValidLine(gfx: Graphics2D,
- screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
- {
- val document = current_document()
- def from_current(pos: Int) = Theory_View.this.from_current(document, pos)
- def to_current(pos: Int) = Theory_View.this.to_current(document, pos)
- val saved_color = gfx.getColor
-
- val metrics = text_area.getPainter.getFontMetrics
-
- // encolor phase
- var cmd = document.command_at(from_current(start))
- while (cmd.isDefined && cmd.get.start(document) < end) {
- val e = cmd.get
- val begin = start max to_current(e.start(document))
- val finish = (end - 1) min to_current(e.stop(document))
- encolor(gfx, y, metrics.getHeight, begin, finish,
- Theory_View.choose_color(e, document), true)
- cmd = document.commands.next(e)
- }
-
- gfx.setColor(saved_color)
- }
-
- override def getToolTipText(x: Int, y: Int): String =
- {
- val document = current_document()
- val offset = from_current(document, text_area.xyToOffset(x, y))
- document.command_at(offset) match {
- case Some(cmd) =>
- document.token_start(cmd.tokens.first)
- cmd.type_at(document, offset - cmd.start(document)).getOrElse(null)
- case None => null
- }
- }
- }
-
-
- /* activation */
-
- private val overview = new Document_Overview(text_area, to_current)
-
- private val selected_state_controller = new CaretListener {
- override def caretUpdate(e: CaretEvent) {
- val doc = current_document()
- doc.command_at(e.getDot) match {
- case Some(cmd)
- if (doc.token_start(cmd.tokens.first) <= e.getDot &&
- Isabelle.session.selected_state != cmd) =>
- Isabelle.session.selected_state = cmd
- case _ =>
- }
- }
- }
-
- def activate()
- {
- text_area.addCaretListener(selected_state_controller)
- text_area.addLeftOfScrollBar(overview)
- text_area.getPainter.
- addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
- buffer.setTokenMarker(new Isabelle_Token_Marker(buffer))
- buffer.addBufferListener(buffer_listener)
- buffer.propertiesChanged()
- }
-
- def deactivate()
- {
- buffer.setTokenMarker(buffer.getMode.getTokenMarker)
- buffer.removeBufferListener(buffer_listener)
- text_area.getPainter.removeExtension(text_area_extension)
- text_area.removeLeftOfScrollBar(overview)
- text_area.removeCaretListener(selected_state_controller)
- }
-
-
- /* history of changes */
-
- private def doc_or_pred(c: Change): Proof_Document =
- session.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(buffer_listener)
-
- def apply(change: Change): Unit = change.edits.foreach {
- case Insert(start, text) => buffer.insert(start, text)
- case Remove(start, text) => buffer.remove(start, text.length)
- }
-
- def unapply(change: Change): Unit = change.edits.reverse.foreach {
- case Insert(start, text) => buffer.remove(start, text.length)
- case Remove(start, text) => buffer.insert(start, text)
- }
-
- // 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()
- overview.repaint()
-
- // track changes in buffer
- buffer.addBufferListener(buffer_listener)
- }
-
-
- /* transforming offsets */
-
- private def changes_from(doc: Proof_Document): List[Edit] =
- List.flatten(current_change.ancestors(_.id == doc.id).reverse.map(_.edits)) :::
- edits.toList
-
- def from_current(doc: Proof_Document, offset: Int): Int =
- (offset /: changes_from(doc).reverse) ((i, change) => change before i)
-
- def to_current(doc: Proof_Document, offset: Int): Int =
- (offset /: changes_from(doc)) ((i, change) => change after i)
-
-
- private def lines_of_command(cmd: Command) =
- {
- val document = current_document()
- (buffer.getLineOfOffset(to_current(document, cmd.start(document))),
- buffer.getLineOfOffset(to_current(document, cmd.stop(document))))
- }
-
-
- /* (re)painting */
-
- private val update_delay = Swing_Thread.delay_first(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()
- }
-
- private def invalidate_line(cmd: Command) =
- {
- val (start, stop) = lines_of_command(cmd)
- text_area.invalidateLineRange(start, stop)
-
- if (Isabelle.session.selected_state == cmd)
- Isabelle.session.selected_state = cmd
- }
-
- 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)
- val stop =
- if (finish < buffer.getLength) text_area.offsetToXY(finish)
- else {
- val p = text_area.offsetToXY(finish - 1)
- val metrics = text_area.getPainter.getFontMetrics
- p.x = p.x + (metrics.charWidth(' ') max metrics.getMaxAdvance)
- p
- }
-
- if (start != null && stop != null) {
- gfx.setColor(color)
- if (fill) gfx.fillRect(start.x, y, stop.x - start.x, height)
- else gfx.drawRect(start.x, y, stop.x - start.x, height)
- }
- }
-
-
- /* init */
-
- edits += Insert(0, buffer.getText(0, buffer.getLength))
- edits_delay()
-}