# HG changeset patch
# User wenzelm
# Date 1260903055 -3600
# Node ID 02959dcea7567670bdd86387c0c69d1e62491a28
# Parent  cb95d6bbf5f1c93c9adbe9acc8d8fc13958ac079
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
incorporate Document_Overview into Document_View;
eliminated Plugin.mapping in favour of direct association via generic properties;
support several views per model;
misc tuning;

diff -r cb95d6bbf5f1 -r 02959dcea756 src/Tools/jEdit/plugin/actions.xml
--- a/src/Tools/jEdit/plugin/actions.xml	Tue Dec 15 11:38:01 2009 +0100
+++ b/src/Tools/jEdit/plugin/actions.xml	Tue Dec 15 19:50:55 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">
diff -r cb95d6bbf5f1 -r 02959dcea756 src/Tools/jEdit/src/jedit/document_model.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Tue Dec 15 19:50:55 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)
+  }
+}
diff -r cb95d6bbf5f1 -r 02959dcea756 src/Tools/jEdit/src/jedit/document_overview.scala
--- a/src/Tools/jEdit/src/jedit/document_overview.scala	Tue Dec 15 11:38:01 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
diff -r cb95d6bbf5f1 -r 02959dcea756 src/Tools/jEdit/src/jedit/document_view.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Tue Dec 15 19:50:55 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
diff -r cb95d6bbf5f1 -r 02959dcea756 src/Tools/jEdit/src/jedit/history_dockable.scala
--- a/src/Tools/jEdit/src/jedit/history_dockable.scala	Tue Dec 15 11:38:01 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/history_dockable.scala	Tue Dec 15 19:50:55 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())
 }
diff -r cb95d6bbf5f1 -r 02959dcea756 src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Tue Dec 15 11:38:01 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Tue Dec 15 19:50:55 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
diff -r cb95d6bbf5f1 -r 02959dcea756 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Tue Dec 15 11:38:01 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Tue Dec 15 19:50:55 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) =>
               {
diff -r cb95d6bbf5f1 -r 02959dcea756 src/Tools/jEdit/src/jedit/isabelle_token_marker.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Tue Dec 15 11:38:01 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Tue Dec 15 19:50:55 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))
diff -r cb95d6bbf5f1 -r 02959dcea756 src/Tools/jEdit/src/jedit/output_dockable.scala
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Tue Dec 15 11:38:01 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Tue Dec 15 19:50:55 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)
           }
           
diff -r cb95d6bbf5f1 -r 02959dcea756 src/Tools/jEdit/src/jedit/plugin.scala
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Tue Dec 15 11:38:01 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Tue Dec 15 19:50:55 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 _ =>
     }
   }
diff -r cb95d6bbf5f1 -r 02959dcea756 src/Tools/jEdit/src/proofdocument/theory_view.scala
--- a/src/Tools/jEdit/src/proofdocument/theory_view.scala	Tue Dec 15 11:38:01 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()
-}