src/Tools/jEdit/src/prover/State.scala
changeset 34759 bfea7839d9e1
parent 34758 710e3a9a4c95
child 34760 dc7f5e0d9d27
     1.1 --- a/src/Tools/jEdit/src/prover/State.scala	Tue Dec 08 14:29:29 2009 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,117 +0,0 @@
     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.prover
    1.12 -
    1.13 -
    1.14 -class State(
    1.15 -  val command: Command,
    1.16 -  val status: Command.Status.Value,
    1.17 -  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.content(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 + (prover: Prover, 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.offsets_of(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.file_of(atts),
   1.101 -                          Position.line_of(atts),
   1.102 -                          Position.id_of(atts),
   1.103 -                          Position.offset_of(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)) prover.command_change.event(command)
   1.118 -    changed
   1.119 -  }
   1.120 -}