1.1 --- a/src/Tools/jEdit/src/prover/Prover.scala	Fri May 22 16:47:11 2009 +0200
     1.2 +++ b/src/Tools/jEdit/src/prover/Prover.scala	Fri May 22 17:36:45 2009 +0200
     1.3 @@ -181,34 +181,43 @@
     1.4                      output_info.event(result.toString)
     1.5                      command.status = Command.Status.FAILED
     1.6                      command_change(command)
     1.7 -                  case XML.Elem(kind, attr, body) =>
     1.8 +                  case XML.Elem(kind, attr, body)
     1.9 +                  if command != null =>
    1.10                      // TODO: assuming that begin, end, id are present in attributes
    1.11                      val begin = get_attr(attr, Markup.OFFSET).get.toInt - 1
    1.12                      val end = get_attr(attr, Markup.END_OFFSET).get.toInt - 1
    1.13                      val markup_id = get_attr(attr, Markup.ID).get
    1.14 -                    kind match {
    1.15 -                      case Markup.ML_TYPING =>
    1.16 -                        val info = body.first.asInstanceOf[XML.Text].content
    1.17 -                        command.markup_root += command.markup_node(begin, end, TypeInfo(info))
    1.18 -                      case Markup.ML_REF =>
    1.19 -                        body match {
    1.20 -                          case List(XML.Elem(Markup.ML_DEF, attr, _)) =>
    1.21 -                            command.markup_root += command.markup_node(begin, end,
    1.22 -                              RefInfo(get_attr(attr, Markup.FILE),
    1.23 -                                      get_attr(attr, Markup.LINE).map(Integer.parseInt),
    1.24 -                                      get_attr(attr, Markup.ID),
    1.25 -                                      get_attr(attr, Markup.OFFSET).map(Integer.parseInt)))
    1.26 -                          case _ =>
    1.27 -                        }
    1.28 -                      case kind =>
    1.29 -                        if (!running)
    1.30 -                          commands.get(markup_id).map (cmd =>
    1.31 -                          cmd.markup_root += cmd.markup_node(begin, end, OuterInfo(kind)))
    1.32 -                        else {
    1.33 -                          command.markup_root += command.markup_node(begin, end, HighlightInfo(kind))
    1.34 -                        }
    1.35 +                    if (kind == Markup.ML_TYPING) {
    1.36 +                      val info = body.first.asInstanceOf[XML.Text].content
    1.37 +                      command.markup_root += command.markup_node(begin, end, TypeInfo(info))
    1.38 +                    } else if (kind == Markup.ML_REF) {
    1.39 +                      body match {
    1.40 +                        case List(XML.Elem(Markup.ML_DEF, attr, _)) =>
    1.41 +                          command.markup_root += command.markup_node(begin, end,
    1.42 +                            RefInfo(get_attr(attr, Markup.FILE),
    1.43 +                                    get_attr(attr, Markup.LINE).map(Integer.parseInt),
    1.44 +                                    get_attr(attr, Markup.ID),
    1.45 +                                    get_attr(attr, Markup.OFFSET).map(Integer.parseInt)))
    1.46 +                        case _ =>
    1.47 +                      }
    1.48 +                    } else {
    1.49 +                      command.markup_root += command.markup_node(begin, end, HighlightInfo(kind))
    1.50                      }
    1.51                      command_change(command)
    1.52 +                  case XML.Elem(kind, attr, body)
    1.53 +                  if command == null =>
    1.54 +                    // TODO: This is mostly irrelevant information on removed commands, but it can
    1.55 +                    // also be outer-syntax-markup since there is no id in props (fix that?)
    1.56 +                    val begin = get_attr(attr, Markup.OFFSET).map(_.toInt - 1)
    1.57 +                    val end = get_attr(attr, Markup.END_OFFSET).map(_.toInt - 1)
    1.58 +                    val markup_id = get_attr(attr, Markup.ID)
    1.59 +                    if (!running && begin.isDefined && end.isDefined && markup_id.isDefined)
    1.60 +                      commands.get(markup_id.get).map (cmd => {
    1.61 +                        cmd.markup_root += cmd.markup_node(begin.get, end.get, OuterInfo(kind))
    1.62 +                        command_change(cmd)
    1.63 +                      })
    1.64 +                    else
    1.65 +                      command_change(command)
    1.66                    case _ =>
    1.67                    //}}}
    1.68                  }