--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Wed Jul 08 15:15:13 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Wed Jul 08 15:15:15 2009 +0200
@@ -115,7 +115,7 @@
var next_x = start
while (command != null && command.start(document) < from(stop)) {
for {
- markup <- command.highlight_node.flatten
+ markup <- command.highlight_node(document).flatten
if (to(markup.abs_stop(document)) > start)
if (to(markup.abs_start(document)) < stop)
byte = DynamicTokenMarker.choose_byte(markup.info.toString)
--- a/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala Wed Jul 08 15:15:13 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala Wed Jul 08 15:15:15 2009 +0200
@@ -52,8 +52,9 @@
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(offset - cmd.start(document))
+ val ref_o = cmd.ref_at(document, offset - cmd.start(document))
if (!ref_o.isDefined) null
else {
val ref = ref_o.get
--- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala Wed Jul 08 15:15:13 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala Wed Jul 08 15:15:15 2009 +0200
@@ -34,7 +34,7 @@
if (prover_setup.isDefined) {
val document = prover_setup.get.theory_view.current_document()
for (command <- document.commands)
- data.root.add(command.markup_root.swing_node(document))
+ data.root.add(command.markup_root(document).swing_node(document))
if (stopped) data.root.add(new DefaultMutableTreeNode("<parser stopped>"))
}
--- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Wed Jul 08 15:15:13 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Wed Jul 08 15:15:15 2009 +0200
@@ -63,7 +63,7 @@
val line2 = buffer.getLineOfOffset(to_current(doc.id, command.stop(doc))) + 1
val y = lineToY(line1)
val height = lineToY(line2) - y - 1
- val (light, dark) = command.status match {
+ val (light, dark) = command.status(doc) match {
case Command.Status.UNPROCESSED => (Color.yellow, new Color(128,128,0))
case Command.Status.FINISHED => (Color.green, new Color(0, 128, 0))
case Command.Status.FAILED => (Color.red, new Color(128,0,0))
--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala Wed Jul 08 15:15:13 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala Wed Jul 08 15:15:15 2009 +0200
@@ -58,16 +58,17 @@
})
// register for state-view
- state_update += (state => {
+ 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 (state == null)
+ if (cmd == null)
state_panel.setDocument(null: Document)
else
- state_panel.setDocument(state.result_document, UserAgent.base_URL)
+ state_panel.setDocument(cmd.result_document(theory_view.current_document()),
+ UserAgent.base_URL)
}
})
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala Wed Jul 08 15:15:13 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Wed Jul 08 15:15:15 2009 +0200
@@ -11,7 +11,7 @@
import scala.actors.Actor
import scala.actors.Actor._
-import isabelle.proofdocument.Text
+import isabelle.proofdocument.{ProofDocument, Text}
import isabelle.prover.{Prover, ProverEvents, Command}
import java.awt.Graphics2D
@@ -30,15 +30,13 @@
val MAX_CHANGE_LENGTH = 1500
- def choose_color(state: Command): Color = {
- if (state == null) Color.red
- else
- state.status 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, 192, 192)
- case _ => Color.red
- }
+ def choose_color(cmd: Command, doc: ProofDocument): Color = {
+ cmd.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, 192, 192)
+ case _ => Color.red
+ }
}
}
@@ -176,8 +174,11 @@
val content = buffer.getText(0, buffer.getLength)
doc_id = id
- /* listen for changes again (TODO: can it be that Listener gets events that
- happenend prior to registration??) */
+ // invoke repaint
+ update_delay()
+ repaint_delay()
+ phase_overview.repaint_delay()
+
buffer.addBufferListener(this)
}
@@ -238,7 +239,8 @@
while (e != null && e.start(document) < end) {
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, TheoryView.choose_color(e), true)
+ encolor(gfx, y, metrics.getHeight, begin, finish,
+ TheoryView.choose_color(e, document), true)
e = document.commands.next(e).getOrElse(null)
}
@@ -251,7 +253,7 @@
val cmd = document.find_command_at(offset)
if (cmd != null) {
document.token_start(cmd.tokens.first)
- cmd.type_at(offset - cmd.start(document))
+ cmd.type_at(document, offset - cmd.start(document))
} else null
}
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Wed Jul 08 15:15:13 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Wed Jul 08 15:15:15 2009 +0200
@@ -40,7 +40,7 @@
val empty =
new ProofDocument(isabelle.jedit.Isabelle.system.id(),
- LinearSet(), Map(), LinearSet(), _ => false)
+ LinearSet(), Map(), LinearSet(), Map(), _ => false)
}
@@ -49,11 +49,13 @@
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)
{
+
def set_command_keyword(f: String => Boolean): ProofDocument =
- new ProofDocument(id, tokens, token_start, commands, f)
+ new ProofDocument(id, tokens, token_start, commands, states, f)
def content = Token.string_from_tokens(Nil ++ tokens, token_start)
/** token view **/
@@ -214,7 +216,7 @@
val doc =
new ProofDocument(new_id, new_tokenset, new_token_start,
- new_commandset, is_command_keyword)
+ new_commandset, states -- removed_commands, is_command_keyword)
return (doc, change)
}
--- a/src/Tools/jEdit/src/prover/Command.scala Wed Jul 08 15:15:13 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala Wed Jul 08 15:15:15 2009 +0200
@@ -36,7 +36,7 @@
require(!tokens.isEmpty)
val id = Isabelle.system.id()
-
+ override def hashCode = id.hashCode
/* content */
@@ -51,40 +51,42 @@
def contains(p: Token) = tokens.contains(p)
-
- /* command status */ // FIXME class Command_State, multiple states per command
-
- var state_id: IsarDocument.State_ID = null
+ /* states */
+ val states = mutable.Map[IsarDocument.State_ID, Command_State]()
+ private def state(doc: ProofDocument) = doc.states.get(this)
+
+ /* command status */
- private var _status = Command.Status.UNPROCESSED
- def status = _status
- def status_=(st: Command.Status.Value) {
- if (st == Command.Status.UNPROCESSED) {
- state_results.clear
- // delete markup
- markup_root = markup_root.filter(_.info match {
- case RootInfo() | OuterInfo(_) => true
- case _ => false
- }).head
- }
- _status = st
+ def set_status(state: IsarDocument.State_ID, status: Command.Status.Value) = {
+ if (state != null)
+ states.getOrElseUpdate(state, new Command_State(this)).status = status
}
+ def status(doc: ProofDocument) =
+ state(doc) match {
+ case Some(s) => states.getOrElseUpdate(s, new Command_State(this)).status
+ case _ => Command.Status.UNPROCESSED
+ }
/* results */
private val results = new mutable.ListBuffer[XML.Tree]
- private val state_results = new mutable.ListBuffer[XML.Tree]
- def add_result(running: Boolean, tree: XML.Tree) = synchronized {
- (if (running) state_results else results) += tree
+ def add_result(state: IsarDocument.State_ID, tree: XML.Tree) = synchronized {
+ (if (state == null) results else states(state).results) += tree
}
- def result_document = XML.document(
- 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")
+ def result_document(doc: ProofDocument) = {
+ val state_results = state(doc) match {
+ case Some(s) =>
+ states.getOrElseUpdate(s, new Command_State(this)).results
+ case _ => Nil}
+ XML.document(
+ 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 */
@@ -92,13 +94,27 @@
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, node: MarkupNode) = {
+ if (state == null) _markup_root = _markup_root.add(node)
+ else {
+ val cmd_state = states.getOrElseUpdate(state, new Command_State(this))
+ cmd_state.markup_root += node
+ }
+ }
- var markup_root = empty_root_node
+ 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: MarkupNode =
+ def highlight_node(doc: ProofDocument): MarkupNode =
{
import MarkupNode._
- markup_root.filter(_.info match {
+ markup_root(doc).filter(_.info match {
case RootInfo() | OuterInfo(_) | HighlightInfo(_) => true
case _ => false
}).head
@@ -110,6 +126,25 @@
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 })
--- a/src/Tools/jEdit/src/prover/Prover.scala Wed Jul 08 15:15:13 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala Wed Jul 08 15:15:15 2009 +0200
@@ -91,13 +91,13 @@
private def handle_result(result: Isabelle_Process.Result)
{
def command_change(c: Command) = change_receiver ! c
- val (running, command) =
+ val (state, command) =
result.props.find(p => p._1 == Markup.ID) match {
- case None => (false, null)
+ case None => (null, null)
case Some((_, id)) =>
- if (commands.contains(id)) (false, commands(id))
- else if (states.contains(id)) (true, states(id))
- else (false, null)
+ if (commands.contains(id)) (null, commands(id))
+ else if (states.contains(id)) (id, states(id))
+ else (null, null)
}
if (result.kind == Isabelle_Process.Kind.STDOUT ||
@@ -112,8 +112,8 @@
| Isabelle_Process.Kind.ERROR =>
if (command != null) {
if (result.kind == Isabelle_Process.Kind.ERROR)
- command.status = Command.Status.FAILED
- command.add_result(running, process.parse_message(result))
+ command.set_status(state, Command.Status.FAILED)
+ command.add_result(state, process.parse_message(result))
command_change(command)
} else {
output_info.event(result.toString)
@@ -143,16 +143,16 @@
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)
- if (cmd.state_id != null) states -= cmd.state_id
states(state_id) = cmd
- cmd.state_id = state_id
- cmd.status = Command.Status.UNPROCESSED
+ doc.states += (cmd -> state_id)
+ cmd.states += (state_id -> new Command_State(cmd))
command_change(cmd)
}
@@ -161,17 +161,17 @@
case XML.Elem(Markup.UNPROCESSED, _, _)
if command != null =>
output_info.event(result.toString)
- command.status = Command.Status.UNPROCESSED
+ command.set_status(state, Command.Status.UNPROCESSED)
command_change(command)
case XML.Elem(Markup.FINISHED, _, _)
if command != null =>
output_info.event(result.toString)
- command.status = Command.Status.FINISHED
+ command.set_status(state, Command.Status.FINISHED)
command_change(command)
case XML.Elem(Markup.FAILED, _, _)
if command != null =>
output_info.event(result.toString)
- command.status = Command.Status.FAILED
+ command.set_status(state, Command.Status.FAILED)
command_change(command)
case XML.Elem(kind, attr, body)
if command != null =>
@@ -179,23 +179,23 @@
if (begin.isDefined && end.isDefined) {
if (kind == Markup.ML_TYPING) {
val info = body.first.asInstanceOf[XML.Text].content
- command.markup_root +=
- command.markup_node(begin.get - 1, end.get - 1, TypeInfo(info))
+ 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.markup_root += command.markup_node(
+ 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)))
+ Position.offset_of(attr))))
case _ =>
}
} else {
- command.markup_root +=
- command.markup_node(begin.get - 1, end.get - 1, HighlightInfo(kind))
+ command.add_markup(state,
+ command.markup_node(begin.get - 1, end.get - 1, HighlightInfo(kind)))
}
}
command_change(command)
@@ -206,10 +206,10 @@
val (begin, end) = Position.offsets_of(attr)
val markup_id = Position.id_of(attr)
val outer = isabelle.jedit.DynamicTokenMarker.is_outer(kind)
- if (outer && !running && begin.isDefined && end.isDefined && markup_id.isDefined)
+ if (outer && state == null && begin.isDefined && end.isDefined && markup_id.isDefined)
commands.get(markup_id.get).map (cmd => {
- cmd.markup_root +=
- cmd.markup_node(begin.get - 1, end.get - 1, OuterInfo(kind))
+ cmd.add_markup(state,
+ cmd.markup_node(begin.get - 1, end.get - 1, OuterInfo(kind)))
command_change(cmd)
})
case _ =>
@@ -249,7 +249,6 @@
val removes =
for (cmd <- changes.removed_commands) yield {
commands -= cmd.id
- if (cmd.state_id != null) states -= cmd.state_id
changes.before_change.map(_.id).getOrElse(document_0.id) -> None
}
val inserts =