# HG changeset patch
# User wenzelm
# Date 1407790778 -7200
# Node ID 922273b7bf8af332ec727b3fadf01fd767f9c934
# Parent  ade8d65b212e8f0608c76d679cf542b966415d65
tuned signature;

diff -r ade8d65b212e -r 922273b7bf8a src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Mon Aug 11 22:46:27 2014 +0200
+++ b/src/Pure/PIDE/command.scala	Mon Aug 11 22:59:38 2014 +0200
@@ -317,20 +317,20 @@
     val init_results: Command.Results,
     val init_markup: Markup_Tree)
 {
-  /* classification */
-
-  def is_undefined: Boolean = id == Document_ID.none
-  val is_unparsed: Boolean = span.content.exists(_.is_unparsed)
-  val is_unfinished: Boolean = span.content.exists(_.is_unfinished)
-
-  def is_command: Boolean = span.kind.isInstanceOf[Thy_Syntax.Command_Span]
-  def is_ignored: Boolean = span.kind == Thy_Syntax.Ignored_Span
+  /* name and classification */
 
   def name: String =
     span.kind match { case Thy_Syntax.Command_Span(name) => name case _ => "" }
 
   override def toString = id + "/" + span.kind.toString
 
+  def is_proper: Boolean = span.kind.isInstanceOf[Thy_Syntax.Command_Span]
+  def is_ignored: Boolean = span.kind == Thy_Syntax.Ignored_Span
+
+  def is_undefined: Boolean = id == Document_ID.none
+  val is_unparsed: Boolean = span.content.exists(_.is_unparsed)
+  val is_unfinished: Boolean = span.content.exists(_.is_unfinished)
+
 
   /* blobs */
 
diff -r ade8d65b212e -r 922273b7bf8a src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Mon Aug 11 22:46:27 2014 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Mon Aug 11 22:59:38 2014 +0200
@@ -332,8 +332,8 @@
     val visible = perspective.commands.toSet
 
     def next_invisible_command(cmds: Linear_Set[Command], from: Command): Command =
-      cmds.iterator(from).dropWhile(cmd => !cmd.is_command || visible(cmd))
-        .find(_.is_command) getOrElse cmds.last
+      cmds.iterator(from).dropWhile(cmd => !cmd.is_proper || visible(cmd))
+        .find(_.is_proper) getOrElse cmds.last
 
     @tailrec def recover(cmds: Linear_Set[Command]): Linear_Set[Command] =
       cmds.find(_.is_unparsed) match {
diff -r ade8d65b212e -r 922273b7bf8a src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Mon Aug 11 22:46:27 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Mon Aug 11 22:59:38 2014 +0200
@@ -110,7 +110,7 @@
             })
           List(node)
         case Thy_Structure.Atom(command)
-        if command.is_command && syntax.heading_level(command).isEmpty =>
+        if command.is_proper && syntax.heading_level(command).isEmpty =>
           val node =
             new DefaultMutableTreeNode(
               new Isabelle_Sidekick.Asset(command.name, offset, offset + entry.length))