1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Pure/Thy/state.scala Mon Jan 11 23:00:05 2010 +0100
1.3 @@ -0,0 +1,117 @@
1.4 +/*
1.5 + * Accumulating results from prover
1.6 + *
1.7 + * @author Fabian Immler, TU Munich
1.8 + * @author Makarius
1.9 + */
1.10 +
1.11 +package isabelle
1.12 +
1.13 +
1.14 +class State(
1.15 + val command: Command,
1.16 + val status: Command.Status.Value,
1.17 + val rev_results: List[XML.Tree],
1.18 + val markup_root: Markup_Text)
1.19 +{
1.20 + def this(command: Command) =
1.21 + this(command, Command.Status.UNPROCESSED, Nil, command.empty_markup)
1.22 +
1.23 +
1.24 + /* content */
1.25 +
1.26 + private def set_status(st: Command.Status.Value): State =
1.27 + new State(command, st, rev_results, markup_root)
1.28 +
1.29 + private def add_result(res: XML.Tree): State =
1.30 + new State(command, status, res :: rev_results, markup_root)
1.31 +
1.32 + private def add_markup(node: Markup_Tree): State =
1.33 + new State(command, status, rev_results, markup_root + node)
1.34 +
1.35 + lazy val results = rev_results.reverse
1.36 +
1.37 +
1.38 + /* markup */
1.39 +
1.40 + lazy val highlight: Markup_Text =
1.41 + {
1.42 + markup_root.filter(_.info match {
1.43 + case Command.HighlightInfo(_) => true
1.44 + case _ => false
1.45 + })
1.46 + }
1.47 +
1.48 + private lazy val types: List[Markup_Node] =
1.49 + markup_root.filter(_.info match {
1.50 + case Command.TypeInfo(_) => true
1.51 + case _ => false }).flatten
1.52 +
1.53 + def type_at(pos: Int): Option[String] =
1.54 + {
1.55 + types.find(t => t.start <= pos && pos < t.stop) match {
1.56 + case Some(t) =>
1.57 + t.info match {
1.58 + case Command.TypeInfo(ty) => Some(command.source(t.start, t.stop) + ": " + ty)
1.59 + case _ => None
1.60 + }
1.61 + case None => None
1.62 + }
1.63 + }
1.64 +
1.65 + private lazy val refs: List[Markup_Node] =
1.66 + markup_root.filter(_.info match {
1.67 + case Command.RefInfo(_, _, _, _) => true
1.68 + case _ => false }).flatten
1.69 +
1.70 + def ref_at(pos: Int): Option[Markup_Node] =
1.71 + refs.find(t => t.start <= pos && pos < t.stop)
1.72 +
1.73 +
1.74 + /* message dispatch */
1.75 +
1.76 + def + (session: Session, message: XML.Tree): State =
1.77 + {
1.78 + val changed: State =
1.79 + message match {
1.80 + case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) =>
1.81 + (this /: elems)((state, elem) =>
1.82 + elem match {
1.83 + case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
1.84 + case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
1.85 + case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
1.86 + case XML.Elem(kind, atts, body) =>
1.87 + val (begin, end) = Position.get_offsets(atts)
1.88 + if (begin.isEmpty || end.isEmpty) state
1.89 + else if (kind == Markup.ML_TYPING) {
1.90 + val info = body.first.asInstanceOf[XML.Text].content // FIXME proper match!?
1.91 + state.add_markup(
1.92 + command.markup_node(begin.get - 1, end.get - 1, Command.TypeInfo(info)))
1.93 + }
1.94 + else if (kind == Markup.ML_REF) {
1.95 + body match {
1.96 + case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
1.97 + state.add_markup(command.markup_node(
1.98 + begin.get - 1, end.get - 1,
1.99 + Command.RefInfo(
1.100 + Position.get_file(atts),
1.101 + Position.get_line(atts),
1.102 + Position.get_id(atts),
1.103 + Position.get_offset(atts))))
1.104 + case _ => state
1.105 + }
1.106 + }
1.107 + else {
1.108 + state.add_markup(
1.109 + command.markup_node(begin.get - 1, end.get - 1, Command.HighlightInfo(kind)))
1.110 + }
1.111 + case _ =>
1.112 + System.err.println("ignored status report: " + elem)
1.113 + state
1.114 + })
1.115 + case _ => add_result(message)
1.116 + }
1.117 + if (!(this eq changed)) session.command_change.event(command)
1.118 + changed
1.119 + }
1.120 +}