/*
* Accumulating results from prover
*
* @author Fabian Immler, TU Munich
*/
package isabelle.prover
class State(
val command: Command,
val status: Command.Status.Value,
rev_results: List[XML.Tree],
val markup_root: MarkupNode)
{
def this(command: Command) =
this(command, Command.Status.UNPROCESSED, Nil, command.empty_root_node)
/* content */
private def set_status(st: Command.Status.Value): State =
new State(command, st, rev_results, markup_root)
private def add_result(res: XML.Tree): State =
new State(command, status, res :: rev_results, markup_root)
private def add_markup(markup: MarkupNode): State =
new State(command, status, rev_results, markup_root + markup)
lazy val results = rev_results.reverse
/* markup */
lazy val highlight_node: MarkupNode =
{
markup_root.filter(_.info match {
case RootInfo() | HighlightInfo(_) => true
case _ => false
}).head
}
lazy private val types =
markup_root.filter(_.info match {
case TypeInfo(_) => true
case _ => false }).flatten(_.flatten)
def type_at(pos: Int): String =
{
types.find(t => t.start <= pos && t.stop > pos).map(t =>
t.content + ": " + (t.info match {
case TypeInfo(i) => i
case _ => "" })).
getOrElse(null)
}
lazy private val refs =
markup_root.filter(_.info match {
case RefInfo(_, _, _, _) => true
case _ => false }).flatten(_.flatten)
def ref_at(pos: Int): Option[MarkupNode] =
refs.find(t => t.start <= pos && t.stop > pos)
/* message dispatch */
def + (message: XML.Tree): State =
{
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) ((st, e) =>
e match {
// command status
case XML.Elem(Markup.UNPROCESSED, _, _) =>
st.set_status(Command.Status.UNPROCESSED)
case XML.Elem(Markup.FINISHED, _, _) =>
st.set_status(Command.Status.FINISHED)
case XML.Elem(Markup.FAILED, _, _) =>
st.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
st.add_markup(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, _)) =>
st.add_markup(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 _ => st
}
}
else {
st.add_markup(command.markup_node(begin.get - 1, end.get - 1, HighlightInfo(kind)))
}
}
else st
case _ => st
})
case _ =>
System.err.println("ignored: " + message)
this
}
command.changed()
changed
}
}