# HG changeset patch
# User immler@in.tum.de
# Date 1227880807 -3600
# Node ID 23b8351ecbbe3182891dbf7ebc1d47d4b5b939cc
# Parent  d67fe0cb1106adae48729a992db31021024ae4a8
arbitrary type for tokens

diff -r d67fe0cb1106 -r 23b8351ecbbe src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Thu Nov 27 22:24:53 2008 +0100
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Fri Nov 28 15:00:07 2008 +0100
@@ -106,12 +106,15 @@
     var position = 0 
     while(matcher.find(position) && ! finished) {
       position = matcher.end()
-			
+			val kind = if(isStartKeyword(matcher.group())){
+        Token.Kind.COMMAND_START
+      } else if (matcher.end() - matcher.start() > 2 && matcher.group().substring(0, 2) == "(*"){
+        Token.Kind.COMMENT
+      } else {""}
       val newToken = new Token[C](matcher.start() + matchStart, 
                                   matcher.end() + matchStart,
-                                  isStartKeyword(matcher.group()),
-                                  matcher.end() - matcher.start() > 2 &&
-                                  matcher.group().substring(0, 2) == "(*")
+                                  kind
+                                  )
 
       if (firstAdded == null)
         firstAdded = newToken
diff -r d67fe0cb1106 -r 23b8351ecbbe src/Tools/jEdit/src/proofdocument/Token.scala
--- a/src/Tools/jEdit/src/proofdocument/Token.scala	Thu Nov 27 22:24:53 2008 +0100
+++ b/src/Tools/jEdit/src/proofdocument/Token.scala	Fri Nov 28 15:00:07 2008 +0100
@@ -1,7 +1,13 @@
 package isabelle.proofdocument
 
-class Token[C](var start : Int, var stop : Int, val isCommandStart : Boolean,
-               val isComment : Boolean) {
+object Token {
+  object Kind {
+    val COMMAND_START = "COMMAND_START"
+    val COMMENT = "COMMENT"
+  }
+}
+
+class Token[C](var start : Int, var stop : Int, var kind : String) {
   var next : Token[C] = null
   var previous : Token[C] = null
   var command : C = null.asInstanceOf[C]
diff -r d67fe0cb1106 -r 23b8351ecbbe src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Thu Nov 27 22:24:53 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala	Fri Nov 28 15:00:07 2008 +0100
@@ -58,7 +58,7 @@
   def properStart = start
   def properStop = {
     var i = last
-    while (i != first && i.isComment)
+    while (i != first && i.kind.equals(Token.Kind.COMMENT))
       i = i.previous
     i.stop
   }  	
diff -r d67fe0cb1106 -r 23b8351ecbbe src/Tools/jEdit/src/prover/Document.scala
--- a/src/Tools/jEdit/src/prover/Document.scala	Thu Nov 27 22:24:53 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Document.scala	Fri Nov 28 15:00:07 2008 +0100
@@ -70,7 +70,7 @@
           before = first.previous
       }
       else if (next != null && next != stop) {
-        if (next.isCommandStart) {
+        if (next.kind.equals(Token.Kind.COMMAND_START)) {
           before = start.command
           scan = next
         }
@@ -109,13 +109,13 @@
     var finished = false
     while (scan != null && !finished) {
       if (scan == stopScan)	{
-        if (scan.isCommandStart)
+        if (scan.kind.equals(Token.Kind.COMMAND_START))
           finished = true
         else
           overrun = true
       }
       
-      if (scan.isCommandStart && cmdStart != null && !finished) {
+      if (scan.kind.equals(Token.Kind.COMMAND_START) && cmdStart != null && !finished) {
         if (! overrun) {
           addedCommands = new Command(cmdStart, cmdStop) :: addedCommands
           cmdStart = scan
diff -r d67fe0cb1106 -r 23b8351ecbbe src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Thu Nov 27 22:24:53 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Fri Nov 28 15:00:07 2008 +0100
@@ -105,9 +105,14 @@
         fireChange()
               
       case IsabelleProcess.Kind.STATUS =>
+        System.err.println("ST: " + tree)
         val state = tree match { case Elem("message", _, 
                                            Elem (name, _, _) :: _) => name
                                  case _ => null }
+/*        val markup_type =
+        val markup_begin =
+        val markup_end =*/
+
         if (st.phase != Phase.REMOVED && st.phase != Phase.REMOVE) {
           state match {
             case "finished" => 
@@ -172,7 +177,7 @@
     
     val props = new Properties()
     props.setProperty("id", cmd.idString)
-    props.setProperty("offset", "1")
+    props.setProperty("offset", Integer.toString(cmd.first.start))
 
     val content = converter.encode(document.getContent(cmd))
     process.output_sync("Isar.command "