# HG changeset patch
# User immler@in.tum.de
# Date 1243006605 -7200
# Node ID c3bdaea2dd6ae793b8bbc74443f92d6e5430a853
# Parent  15abc5f5f40a8b1d46f1be85f9c778017321f07f
improved handling of markup-information with command=null

diff -r 15abc5f5f40a -r c3bdaea2dd6a src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Fri May 22 16:47:11 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Fri May 22 17:36:45 2009 +0200
@@ -181,34 +181,43 @@
                     output_info.event(result.toString)
                     command.status = Command.Status.FAILED
                     command_change(command)
-                  case XML.Elem(kind, attr, body) =>
+                  case XML.Elem(kind, attr, body)
+                  if command != null =>
                     // TODO: assuming that begin, end, id are present in attributes
                     val begin = get_attr(attr, Markup.OFFSET).get.toInt - 1
                     val end = get_attr(attr, Markup.END_OFFSET).get.toInt - 1
                     val markup_id = get_attr(attr, Markup.ID).get
-                    kind match {
-                      case Markup.ML_TYPING =>
-                        val info = body.first.asInstanceOf[XML.Text].content
-                        command.markup_root += command.markup_node(begin, end, TypeInfo(info))
-                      case Markup.ML_REF =>
-                        body match {
-                          case List(XML.Elem(Markup.ML_DEF, attr, _)) =>
-                            command.markup_root += command.markup_node(begin, end,
-                              RefInfo(get_attr(attr, Markup.FILE),
-                                      get_attr(attr, Markup.LINE).map(Integer.parseInt),
-                                      get_attr(attr, Markup.ID),
-                                      get_attr(attr, Markup.OFFSET).map(Integer.parseInt)))
-                          case _ =>
-                        }
-                      case kind =>
-                        if (!running)
-                          commands.get(markup_id).map (cmd =>
-                          cmd.markup_root += cmd.markup_node(begin, end, OuterInfo(kind)))
-                        else {
-                          command.markup_root += command.markup_node(begin, end, HighlightInfo(kind))
-                        }
+                    if (kind == Markup.ML_TYPING) {
+                      val info = body.first.asInstanceOf[XML.Text].content
+                      command.markup_root += command.markup_node(begin, end, TypeInfo(info))
+                    } else if (kind == Markup.ML_REF) {
+                      body match {
+                        case List(XML.Elem(Markup.ML_DEF, attr, _)) =>
+                          command.markup_root += command.markup_node(begin, end,
+                            RefInfo(get_attr(attr, Markup.FILE),
+                                    get_attr(attr, Markup.LINE).map(Integer.parseInt),
+                                    get_attr(attr, Markup.ID),
+                                    get_attr(attr, Markup.OFFSET).map(Integer.parseInt)))
+                        case _ =>
+                      }
+                    } else {
+                      command.markup_root += command.markup_node(begin, end, HighlightInfo(kind))
                     }
                     command_change(command)
+                  case XML.Elem(kind, attr, body)
+                  if command == null =>
+                    // TODO: This is mostly irrelevant information on removed commands, but it can
+                    // also be outer-syntax-markup since there is no id in props (fix that?)
+                    val begin = get_attr(attr, Markup.OFFSET).map(_.toInt - 1)
+                    val end = get_attr(attr, Markup.END_OFFSET).map(_.toInt - 1)
+                    val markup_id = get_attr(attr, Markup.ID)
+                    if (!running && begin.isDefined && end.isDefined && markup_id.isDefined)
+                      commands.get(markup_id.get).map (cmd => {
+                        cmd.markup_root += cmd.markup_node(begin.get, end.get, OuterInfo(kind))
+                        command_change(cmd)
+                      })
+                    else
+                      command_change(command)
                   case _ =>
                   //}}}
                 }