--- 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 */
--- 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 {
--- 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))