# HG changeset patch
# User immler@in.tum.de
# Date 1243437238 -7200
# Node ID f5c3ad245539efd7db0f6c4d3533ecdb2d4d5f44
# Parent  7a0531f2be616ea6cfe84ecbcaa9a9e924bf3277
outer syntax could clash with status on removed commands

diff -r 7a0531f2be61 -r f5c3ad245539 src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala
--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Wed May 27 17:07:02 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Wed May 27 17:13:58 2009 +0200
@@ -59,6 +59,10 @@
     }
   }
 
+  def is_outer(kind: String) =
+    List(Markup.IDENT, Markup.COMMAND, Markup.KEYWORD, Markup.VERBATIM, Markup.COMMENT,
+         Markup.CONTROL, Markup.MALFORMED, Markup.STRING, Markup.ALTSTRING).exists(kind == _)
+
   def choose_color(kind : String, styles: Array[SyntaxStyle]) : Color =
     styles((choose_byte(kind).asInstanceOf[Byte])).getForegroundColor
 
diff -r 7a0531f2be61 -r f5c3ad245539 src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Wed May 27 17:07:02 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Wed May 27 17:13:58 2009 +0200
@@ -211,7 +211,8 @@
                     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)
+                    val outer = isabelle.jedit.DynamicTokenMarker.is_outer(kind)
+                    if (outer && !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)