1.1 --- a/src/Tools/jEdit/src/prover/Command.scala	Sat Jul 04 14:14:07 2009 +0200
     1.2 +++ b/src/Tools/jEdit/src/prover/Command.scala	Sat Jul 04 14:14:37 2009 +0200
     1.3 @@ -20,8 +20,10 @@
     1.4  import sidekick.{SideKickParsedData, IAsset}
     1.5  
     1.6  
     1.7 -object Command {
     1.8 -  object Status extends Enumeration {
     1.9 +object Command
    1.10 +{
    1.11 +  object Status extends Enumeration
    1.12 +  {
    1.13      val UNPROCESSED = Value("UNPROCESSED")
    1.14      val FINISHED = Value("FINISHED")
    1.15      val FAILED = Value("FAILED")
    1.16 @@ -31,21 +33,26 @@
    1.17  
    1.18  class Command(val tokens: List[Token], val starts: Map[Token, Int])
    1.19  {
    1.20 +  require(!tokens.isEmpty)
    1.21 +
    1.22    val id = Isabelle.system.id()
    1.23  
    1.24 +
    1.25    /* content */
    1.26  
    1.27    override def toString = name
    1.28  
    1.29    val name = tokens.head.content
    1.30    val content: String = Token.string_from_tokens(tokens, starts)
    1.31 +  val symbol_index = new Symbol.Index(content)
    1.32  
    1.33    def start(doc: ProofDocument) = doc.token_start(tokens.first)
    1.34    def stop(doc: ProofDocument) = doc.token_start(tokens.last) + tokens.last.length
    1.35  
    1.36    def contains(p: Token) = tokens.contains(p)
    1.37  
    1.38 -  /* command status */
    1.39 +
    1.40 +  /* command status */   // FIXME class Command_State, multiple states per command
    1.41  
    1.42    var state_id: IsarDocument.State_ID = null
    1.43  
    1.44 @@ -88,7 +95,8 @@
    1.45  
    1.46    var markup_root = empty_root_node
    1.47  
    1.48 -  def highlight_node: MarkupNode = {
    1.49 +  def highlight_node: MarkupNode =
    1.50 +  {
    1.51      import MarkupNode._
    1.52      markup_root.filter(_.info match {
    1.53        case RootInfo() | OuterInfo(_) | HighlightInfo(_) => true
    1.54 @@ -102,7 +110,8 @@
    1.55        else "wrong indices??",
    1.56        info)
    1.57  
    1.58 -  def type_at(pos: Int): String = {
    1.59 +  def type_at(pos: Int): String =
    1.60 +  {
    1.61      val types = markup_root.filter(_.info match { case TypeInfo(_) => true case _ => false })
    1.62      types.flatten(_.flatten).
    1.63        find(t => t.start <= pos && t.stop > pos).