# HG changeset patch
# User wenzelm
# Date 1230492934 -3600
# Node ID 3b9d0074ed447af4c5ce5e81e7377930b87c0c9d
# Parent  db45b50cd361b8ac7dd7f2f16c05ab18d0f495e6
command id via Isabelle.plugin;
tuned command interface;
tuned;

diff -r db45b50cd361 -r 3b9d0074ed44 src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Sun Dec 28 20:31:13 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala	Sun Dec 28 20:35:34 2008 +0100
@@ -7,13 +7,17 @@
 
 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")
@@ -22,76 +26,78 @@
     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)
-  }
+  /* content */
 
-  def content = document.getContent(this)
+  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
-  }  	
-}
\ No newline at end of file
+  }
+
+
+  /* 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)
+  }
+}
diff -r db45b50cd361 -r 3b9d0074ed44 src/Tools/jEdit/src/prover/Document.scala
--- a/src/Tools/jEdit/src/prover/Document.scala	Sun Dec 28 20:31:13 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Document.scala	Sun Dec 28 20:35:34 2008 +0100
@@ -33,7 +33,7 @@
     }
   }
 
-  def getContent(cmd : Command) = text.content(cmd.properStart, cmd.properStop)
+  def getContent(cmd : Command) = text.content(cmd.proper_start, cmd.proper_stop)
 
   def getNextCommandContaining(pos : Int) : Command = {
     for( cmd <- commands()) { if (pos < cmd.stop) return cmd }
diff -r db45b50cd361 -r 3b9d0074ed44 src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Sun Dec 28 20:31:13 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Sun Dec 28 20:35:34 2008 +0100
@@ -111,7 +111,7 @@
                     st.phase = Phase.FAILED
                     fireChange(st)
                   case Elem("removed", _, _) =>
-                    document.prover.commands.removeKey(st.idString)
+                    document.prover.commands.removeKey(st.id)
                     st.phase = Phase.REMOVED
                     fireChange(st)
                   case _ =>
@@ -134,19 +134,19 @@
       case IsabelleProcess.Kind.ERROR => 
         if (st.phase != Phase.REMOVED && st.phase != Phase.REMOVE)
           st.phase = Phase.FAILED
-        st.addResult(tree)
+        st.add_result(tree)
         fireChange(st)
         
       case IsabelleProcess.Kind.WRITELN =>
-        st.addResult(tree)
+        st.add_result(tree)
         fireChange(st)
         
       case IsabelleProcess.Kind.PRIORITY =>
-        st.addResult(tree)
+        st.add_result(tree)
         fireChange(st)
 
       case IsabelleProcess.Kind.WARNING =>
-        st.addResult(tree)
+        st.add_result(tree)
         fireChange(st)
               
       case IsabelleProcess.Kind.STATUS =>
@@ -184,11 +184,11 @@
   }
   
   private def send(cmd : Command) {
-    commands.put(cmd.idString, cmd)
+    commands.put(cmd.id, cmd)
     
-    val props = new Properties()
-    props.setProperty("id", cmd.idString)
-    props.setProperty("offset", Integer.toString(1))
+    val props = new Properties
+    props.setProperty("id", cmd.id)
+    props.setProperty("offset", "1")
 
     val content = isabelle_symbols.encode(document.getContent(cmd))
     process.output_sync("Isar.command " 
@@ -198,15 +198,15 @@
     
     process.output_sync("Isar.insert "
                         + encode_string(if (cmd.previous == null) "" 
-                                        else cmd.previous.idString)
+                                        else cmd.previous.id)
                         + " "
-                        + encode_string(cmd.idString))
+                        + encode_string(cmd.id))
     
     cmd.phase = Phase.UNPROCESSED
   }
   
   def remove(cmd : Command) {
     cmd.phase = Phase.REMOVE
-    process.output_sync("Isar.remove " + encode_string(cmd.idString))
+    process.output_sync("Isar.remove " + encode_string(cmd.id))
   }
 }
\ No newline at end of file