src/Tools/jEdit/src/proofdocument/state.scala
author wenzelm
Tue Dec 08 16:30:20 2009 +0100 (2009-12-08)
changeset 34760 dc7f5e0d9d27
parent 34759 bfea7839d9e1
child 34777 91d6089cef88
permissions -rw-r--r--
misc modernization of names;
immler@34675
     1
/*
immler@34675
     2
 * Accumulating results from prover
immler@34675
     3
 *
immler@34675
     4
 * @author Fabian Immler, TU Munich
wenzelm@34715
     5
 * @author Makarius
immler@34675
     6
 */
immler@34675
     7
wenzelm@34760
     8
package isabelle.proofdocument
immler@34675
     9
immler@34676
    10
wenzelm@34697
    11
class State(
wenzelm@34697
    12
  val command: Command,
wenzelm@34697
    13
  val status: Command.Status.Value,
wenzelm@34697
    14
  rev_results: List[XML.Tree],
wenzelm@34717
    15
  val markup_root: Markup_Text)
immler@34676
    16
{
wenzelm@34697
    17
  def this(command: Command) =
wenzelm@34717
    18
    this(command, Command.Status.UNPROCESSED, Nil, command.empty_markup)
wenzelm@34697
    19
immler@34676
    20
wenzelm@34697
    21
  /* content */
wenzelm@34697
    22
wenzelm@34697
    23
  private def set_status(st: Command.Status.Value): State =
wenzelm@34697
    24
    new State(command, st, rev_results, markup_root)
immler@34676
    25
wenzelm@34697
    26
  private def add_result(res: XML.Tree): State =
wenzelm@34697
    27
    new State(command, status, res :: rev_results, markup_root)
wenzelm@34697
    28
wenzelm@34717
    29
  private def add_markup(node: Markup_Tree): State =
wenzelm@34717
    30
    new State(command, status, rev_results, markup_root + node)
wenzelm@34697
    31
wenzelm@34697
    32
  lazy val results = rev_results.reverse
wenzelm@34697
    33
immler@34688
    34
immler@34676
    35
  /* markup */
wenzelm@34697
    36
wenzelm@34717
    37
  lazy val highlight: Markup_Text =
immler@34688
    38
  {
immler@34688
    39
    markup_root.filter(_.info match {
wenzelm@34717
    40
      case Command.HighlightInfo(_) => true
immler@34688
    41
      case _ => false
wenzelm@34717
    42
    })
immler@34688
    43
  }
immler@34688
    44
wenzelm@34717
    45
  private lazy val types: List[Markup_Node] =
immler@34688
    46
    markup_root.filter(_.info match {
wenzelm@34707
    47
      case Command.TypeInfo(_) => true
wenzelm@34717
    48
      case _ => false }).flatten
immler@34676
    49
wenzelm@34717
    50
  def type_at(pos: Int): Option[String] =
immler@34676
    51
  {
wenzelm@34717
    52
    types.find(t => t.start <= pos && pos < t.stop) match {
wenzelm@34717
    53
      case Some(t) =>
wenzelm@34717
    54
        t.info match {
wenzelm@34717
    55
          case Command.TypeInfo(ty) => Some(command.content(t.start, t.stop) + ": " + ty)
wenzelm@34717
    56
          case _ => None
wenzelm@34717
    57
        }
wenzelm@34717
    58
      case None => None
wenzelm@34717
    59
    }
immler@34676
    60
  }
immler@34676
    61
wenzelm@34717
    62
  private lazy val refs: List[Markup_Node] =
immler@34688
    63
    markup_root.filter(_.info match {
wenzelm@34707
    64
      case Command.RefInfo(_, _, _, _) => true
wenzelm@34717
    65
      case _ => false }).flatten
immler@34688
    66
wenzelm@34717
    67
  def ref_at(pos: Int): Option[Markup_Node] =
wenzelm@34703
    68
    refs.find(t => t.start <= pos && pos < t.stop)
immler@34688
    69
immler@34688
    70
wenzelm@34697
    71
  /* message dispatch */
wenzelm@34697
    72
wenzelm@34724
    73
  def + (prover: Prover, message: XML.Tree): State =
wenzelm@34697
    74
  {
immler@34676
    75
    val changed: State =
wenzelm@34703
    76
      message match {
wenzelm@34703
    77
        case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) =>
wenzelm@34715
    78
          (this /: elems)((state, elem) =>
wenzelm@34715
    79
            elem match {
wenzelm@34715
    80
              case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
wenzelm@34715
    81
              case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
wenzelm@34715
    82
              case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
wenzelm@34715
    83
              case XML.Elem(kind, atts, body) =>
wenzelm@34715
    84
                val (begin, end) = Position.offsets_of(atts)
wenzelm@34715
    85
                if (begin.isEmpty || end.isEmpty) state
wenzelm@34715
    86
                else if (kind == Markup.ML_TYPING) {
wenzelm@34715
    87
                  val info = body.first.asInstanceOf[XML.Text].content   // FIXME proper match!?
wenzelm@34715
    88
                  state.add_markup(
wenzelm@34715
    89
                    command.markup_node(begin.get - 1, end.get - 1, Command.TypeInfo(info)))
wenzelm@34715
    90
                }
wenzelm@34715
    91
                else if (kind == Markup.ML_REF) {
wenzelm@34715
    92
                  body match {
wenzelm@34715
    93
                    case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
wenzelm@34715
    94
                      state.add_markup(command.markup_node(
wenzelm@34715
    95
                        begin.get - 1, end.get - 1,
wenzelm@34715
    96
                        Command.RefInfo(
wenzelm@34715
    97
                          Position.file_of(atts),
wenzelm@34715
    98
                          Position.line_of(atts),
wenzelm@34715
    99
                          Position.id_of(atts),
wenzelm@34715
   100
                          Position.offset_of(atts))))
wenzelm@34715
   101
                    case _ => state
immler@34676
   102
                  }
wenzelm@34697
   103
                }
wenzelm@34715
   104
                else {
wenzelm@34715
   105
                  state.add_markup(
wenzelm@34715
   106
                    command.markup_node(begin.get - 1, end.get - 1, Command.HighlightInfo(kind)))
wenzelm@34715
   107
                }
wenzelm@34715
   108
              case _ =>
wenzelm@34715
   109
                System.err.println("ignored status report: " + elem)
wenzelm@34715
   110
                state
wenzelm@34703
   111
            })
wenzelm@34715
   112
        case _ => add_result(message)
wenzelm@34703
   113
      }
wenzelm@34724
   114
    if (!(this eq changed)) prover.command_change.event(command)
immler@34676
   115
    changed
immler@34676
   116
  }
immler@34675
   117
}