src/Pure/PIDE/command.scala
changeset 38362 754ad6340055
parent 38361 b609d0b271fa
child 38363 af7f41a8a0a8
     1.1 --- a/src/Pure/PIDE/command.scala	Thu Aug 12 13:59:18 2010 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Thu Aug 12 14:22:23 2010 +0200
     1.3 @@ -30,14 +30,15 @@
     1.4      command_id: Option[Document.Command_ID], offset: Option[Int])  // FIXME Command_ID vs. State_ID !?
     1.5  
     1.6  
     1.7 +
     1.8    /** accumulated results from prover **/
     1.9  
    1.10 -  class State(
    1.11 +  case class State(
    1.12      val command: Command,
    1.13      val status: Command.Status.Value,
    1.14      val forks: Int,
    1.15      val reverse_results: List[XML.Tree],
    1.16 -    val markup_root: Markup_Text)
    1.17 +    val markup: Markup_Text)
    1.18    {
    1.19      def this(command: Command) =
    1.20        this(command, Command.Status.UNPROCESSED, 0, Nil, command.empty_markup)
    1.21 @@ -45,33 +46,25 @@
    1.22  
    1.23      /* content */
    1.24  
    1.25 -    private def set_status(st: Command.Status.Value): State =
    1.26 -      new State(command, st, forks, reverse_results, markup_root)
    1.27 -
    1.28 -    private def add_forks(i: Int): State =
    1.29 -      new State(command, status, forks + i, reverse_results, markup_root)
    1.30 +    lazy val results = reverse_results.reverse
    1.31  
    1.32 -    private def add_result(res: XML.Tree): State =
    1.33 -      new State(command, status, forks, res :: reverse_results, markup_root)
    1.34 +    def add_result(result: XML.Tree): State = copy(reverse_results = result :: reverse_results)
    1.35  
    1.36 -    private def add_markup(node: Markup_Tree): State =
    1.37 -      new State(command, status, forks, reverse_results, markup_root + node)
    1.38 -
    1.39 -    lazy val results = reverse_results.reverse
    1.40 +    def add_markup(node: Markup_Tree): State = copy(markup = markup + node)
    1.41  
    1.42  
    1.43      /* markup */
    1.44  
    1.45      lazy val highlight: Markup_Text =
    1.46      {
    1.47 -      markup_root.filter(_.info match {
    1.48 +      markup.filter(_.info match {
    1.49          case Command.HighlightInfo(_, _) => true
    1.50          case _ => false
    1.51        })
    1.52      }
    1.53  
    1.54      private lazy val types: List[Markup_Node] =
    1.55 -      markup_root.filter(_.info match {
    1.56 +      markup.filter(_.info match {
    1.57          case Command.TypeInfo(_) => true
    1.58          case _ => false }).flatten
    1.59  
    1.60 @@ -88,7 +81,7 @@
    1.61      }
    1.62  
    1.63      private lazy val refs: List[Markup_Node] =
    1.64 -      markup_root.filter(_.info match {
    1.65 +      markup.filter(_.info match {
    1.66          case Command.RefInfo(_, _, _, _) => true
    1.67          case _ => false }).flatten
    1.68  
    1.69 @@ -103,11 +96,11 @@
    1.70          case XML.Elem(Markup(Markup.STATUS, _), elems) =>
    1.71            (this /: elems)((state, elem) =>
    1.72              elem match {
    1.73 -              case XML.Elem(Markup(Markup.UNPROCESSED, _), _) => state.set_status(Command.Status.UNPROCESSED)
    1.74 -              case XML.Elem(Markup(Markup.FINISHED, _), _) => state.set_status(Command.Status.FINISHED)
    1.75 -              case XML.Elem(Markup(Markup.FAILED, _), _) => state.set_status(Command.Status.FAILED)
    1.76 -              case XML.Elem(Markup(Markup.FORKED, _), _) => state.add_forks(1)
    1.77 -              case XML.Elem(Markup(Markup.JOINED, _), _) => state.add_forks(-1)
    1.78 +              case XML.Elem(Markup(Markup.UNPROCESSED, _), _) => state.copy(status = Command.Status.UNPROCESSED)
    1.79 +              case XML.Elem(Markup(Markup.FINISHED, _), _) => state.copy(status = Command.Status.FINISHED)
    1.80 +              case XML.Elem(Markup(Markup.FAILED, _), _) => state.copy(status = Command.Status.FAILED)
    1.81 +              case XML.Elem(Markup(Markup.FORKED, _), _) => state.copy(forks = state.forks + 1)
    1.82 +              case XML.Elem(Markup(Markup.JOINED, _), _) => state.copy(forks = state.forks - 1)
    1.83                case _ => System.err.println("Ignored status message: " + elem); state
    1.84              })
    1.85  
    1.86 @@ -125,13 +118,14 @@
    1.87                      else if (kind == Markup.ML_REF) {
    1.88                        body match {
    1.89                          case List(XML.Elem(Markup(Markup.ML_DEF, props), _)) =>
    1.90 -                          state.add_markup(command.markup_node(
    1.91 -                            begin - 1, end - 1,
    1.92 -                            Command.RefInfo(
    1.93 -                              Position.get_file(props),
    1.94 -                              Position.get_line(props),
    1.95 -                              Position.get_id(props),
    1.96 -                              Position.get_offset(props))))
    1.97 +                          state.add_markup(
    1.98 +                            command.markup_node(
    1.99 +                              begin - 1, end - 1,
   1.100 +                              Command.RefInfo(
   1.101 +                                Position.get_file(props),
   1.102 +                                Position.get_line(props),
   1.103 +                                Position.get_id(props),
   1.104 +                                Position.get_offset(props))))
   1.105                          case _ => state
   1.106                        }
   1.107                      }