src/Tools/jEdit/src/prover/Command.scala

  * @author Fabian Immler, TU Munich
  */
 
 package isabelle.prover
 
-import isabelle.proofdocument.Token
-import isabelle.jedit.Plugin
-import isabelle.{ YXML, XML }
-import sidekick.{SideKickParsedData, IAsset}
+
 import javax.swing.text.Position
 import javax.swing.tree.DefaultMutableTreeNode
+
+import isabelle.proofdocument.Token
+import isabelle.jedit.{Isabelle, Plugin}
+import isabelle.{YXML, XML}
+
+import sidekick.{SideKickParsedData, IAsset}
+
 
 object Command {
   object Phase extends Enumeration {
     val UNPROCESSED = Value("UNPROCESSED")
     val FINISHED = Value("FINISHED")
     val REMOVE = Value("REMOVE")
     val REMOVED = Value("REMOVED")
     val FAILED = Value("FAILED")
   }
-
-  private var nextId : Long = 0
-  def generateId : Long = {
-    nextId = nextId + 1
-    return nextId
-  }
-  
-  def idFromString(id : String) = Long.unbox(java.lang.Long.valueOf(id, 36))
 }
 
-class Command(val document : Document, val first : Token[Command], val last : Token[Command]) {
-  import Command._
+
+class Command(val document: Document, val first: Token[Command], val last: Token[Command])
+{
+  val id = Isabelle.plugin.id()
   
   {
     var t = first
-    while(t != null) {
+    while (t != null) {
       t.command = this
       t = if (t == last) null else t.next
     }
   }
-  
-  val id : Long = generateId
 
-  private var p = Phase.UNPROCESSED
+
+  /* command phase */
+
+  private var p = Command.Phase.UNPROCESSED
   def phase = p
-  def phase_=(p_new : Phase.Value) = {
-    if(p_new == Phase.UNPROCESSED){
-      //delete inner syntax
-      for(child <- root_node.children){
+  def phase_=(p_new: Command.Phase.Value) = {
+    if (p_new == Command.Phase.UNPROCESSED) {
+      // delete markup
+      for (child <- root_node.children) {
         child.children = Nil
       }
     }
     p = p_new
   }
-	
-  var results = Nil : List[XML.Tree]
 
-  def idString = java.lang.Long.toString(id, 36)
+
+  /* accumulated results */
+
+  var results: List[XML.Tree] = Nil
+
   def results_xml = XML.document(
     results match {
       case Nil => XML.Elem("message", Nil, Nil)
       case List(elem) => elem
-      case _ =>
-        XML.Elem("messages", List(), List(results.first, results.last))
+      case _ => XML.Elem("messages", Nil, List(results.first, results.last))
     }, "style")
-  def addResult(tree : XML.Tree) {
+  def add_result(tree: XML.Tree) {
     results = results ::: List(tree)    // FIXME canonical reverse order
   }
-  
-  val root_node = 
-    new MarkupNode(this, 0, stop - start, idString, "Command", document.getContent(this))
 
-  def node_from(kind : String, begin : Int, end : Int) : MarkupNode = {
-    val markup_content = /*content.substring(begin, end)*/ ""
-    new MarkupNode(this, begin, end, idString, kind, markup_content)
-  }
 
-  def content = document.getContent(this)
+  /* content */
+
+  def content(): String = document.getContent(this)
 
   def next = if (last.next != null) last.next.command else null
   def previous = if (first.previous != null) first.previous.command else null
 
-  def start = first start
-  def stop = last stop
-  
-  def properStart = start
-  def properStop = {
+  def start = first.start
+  def stop = last.stop
+
+  def proper_start = start
+  def proper_stop = {
     var i = last
     while (i != first && i.kind.equals(Token.Kind.COMMENT))
       i = i.previous
     i.stop
-  }  	
+  }
+
+
+  /* markup tree */
+
+  val root_node =
+    new MarkupNode(this, 0, stop - start, id, Markup.COMMAND_SPAN, content())
+
+  def node_from(kind: String, begin: Int, end: Int) = {
+    val markup_content = /*content.substring(begin, end)*/ ""
+    new MarkupNode(this, begin, end, id, kind, markup_content)
+  }
 }