# 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))