# HG changeset patch
# User wenzelm
# Date 1246709677 -7200
# Node ID f3b5d6e248be47b9c53d1f5a70b61a0396d36066
# Parent  5b42b8725dc72616619354d74855f90a4d7781d2
added symbol_index (presently unused);
misc tuning;

diff -r 5b42b8725dc7 -r f3b5d6e248be src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Sat Jul 04 14:14:07 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala	Sat Jul 04 14:14:37 2009 +0200
@@ -20,8 +20,10 @@
 import sidekick.{SideKickParsedData, IAsset}
 
 
-object Command {
-  object Status extends Enumeration {
+object Command
+{
+  object Status extends Enumeration
+  {
     val UNPROCESSED = Value("UNPROCESSED")
     val FINISHED = Value("FINISHED")
     val FAILED = Value("FAILED")
@@ -31,21 +33,26 @@
 
 class Command(val tokens: List[Token], val starts: Map[Token, Int])
 {
+  require(!tokens.isEmpty)
+
   val id = Isabelle.system.id()
 
+
   /* content */
 
   override def toString = name
 
   val name = tokens.head.content
   val content: String = Token.string_from_tokens(tokens, starts)
+  val symbol_index = new Symbol.Index(content)
 
   def start(doc: ProofDocument) = doc.token_start(tokens.first)
   def stop(doc: ProofDocument) = doc.token_start(tokens.last) + tokens.last.length
 
   def contains(p: Token) = tokens.contains(p)
 
-  /* command status */
+
+  /* command status */   // FIXME class Command_State, multiple states per command
 
   var state_id: IsarDocument.State_ID = null
 
@@ -88,7 +95,8 @@
 
   var markup_root = empty_root_node
 
-  def highlight_node: MarkupNode = {
+  def highlight_node: MarkupNode =
+  {
     import MarkupNode._
     markup_root.filter(_.info match {
       case RootInfo() | OuterInfo(_) | HighlightInfo(_) => true
@@ -102,7 +110,8 @@
       else "wrong indices??",
       info)
 
-  def type_at(pos: Int): String = {
+  def type_at(pos: Int): String =
+  {
     val types = markup_root.filter(_.info match { case TypeInfo(_) => true case _ => false })
     types.flatten(_.flatten).
       find(t => t.start <= pos && t.stop > pos).