--- 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
--- 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]
--- 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
}
--- 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
--- 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 "