Command and Command_State handle results from prover as Accumulator
accumulating results in State;
prover outputs any result
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Thu Aug 27 10:51:09 2009 +0200
@@ -48,7 +48,7 @@
val tokens: LinearSet[Token],
val token_start: Map[Token, Int],
val commands: LinearSet[Command],
- var states: Map[Command, IsarDocument.State_ID],
+ var states: Map[Command, Command_State],
is_command_keyword: String => Boolean,
change_receiver: Actor)
{
--- a/src/Tools/jEdit/src/prover/Command.scala Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala Thu Aug 27 10:51:09 2009 +0200
@@ -49,6 +49,7 @@
class Command(val tokens: List[Token], val starts: Map[Token, Int], chg_rec: Actor)
+extends Accumulator
{
require(!tokens.isEmpty)
@@ -71,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 Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala Thu Aug 27 10:51:09 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 Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala Thu Aug 27 10:51:09 2009 +0200
@@ -43,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)
@@ -92,138 +94,72 @@
private def handle_result(result: Isabelle_Process.Result)
{
- def command_change(c: Command) = c.changed()
- 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
}
-
- if (result.kind == Isabelle_Process.Kind.STDOUT ||
- result.kind == Isabelle_Process.Kind.STDIN)
- output_info.event(result)
- 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)
- }
+ output_info.event(result)
+ val message = process.parse_message(result)
+ if (state.isDefined) state.get ! message
+ else result.kind match {
- 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
+ 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
- // 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)
- 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)
- }
+ // 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) =>
+ 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)
- command.set_status(state, Command.Status.UNPROCESSED)
- command_change(command)
- case XML.Elem(Markup.FINISHED, _, _)
- if command != null =>
- output_info.event(result)
- command.set_status(state, Command.Status.FINISHED)
- command_change(command)
- case XML.Elem(Markup.FAILED, _, _)
- if command != null =>
- output_info.event(result)
- 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 _ =>
}
}
--- a/src/Tools/jEdit/src/prover/State.scala Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/prover/State.scala Thu Aug 27 10:51:09 2009 +0200
@@ -6,7 +6,96 @@
package isabelle.prover
-abstract class State
+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
+)
{
- def +(message: XML.Tree): State
+
+ 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
+ }
+
}