# HG changeset patch
# User wenzelm
# Date 1232479924 -3600
# Node ID 20e9d420dbbb943b38b89506648ec4751b740709
# Parent  820d0675e7b5fce6702f5de541aa9ff56e22c204
Command: turned content into plain val;

diff -r 820d0675e7b5 -r 20e9d420dbbb src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Tue Jan 20 20:05:21 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Tue Jan 20 20:32:04 2009 +0100
@@ -235,8 +235,6 @@
     def next() = { val s = current.command ; current = s.last.next ; s }
   }
 
-  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 }
     return null
@@ -325,7 +323,7 @@
 
       if (scan.kind == Token.Kind.COMMAND_START && cmdStart != null && !finished) {
         if (!overrun) {
-          addedCommands = new Command(this, cmdStart, cmdStop) :: addedCommands
+          addedCommands = new Command(text, cmdStart, cmdStop) :: addedCommands
           cmdStart = scan
           cmdStop = scan
         }
@@ -348,7 +346,7 @@
     }
 
     if (cmdStart != null)
-      addedCommands = new Command(this, cmdStart, cmdStop) :: addedCommands
+      addedCommands = new Command(text, cmdStart, cmdStop) :: addedCommands
 
     // relink commands
     addedCommands = addedCommands.reverse
diff -r 820d0675e7b5 -r 20e9d420dbbb src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Tue Jan 20 20:05:21 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala	Tue Jan 20 20:32:04 2009 +0100
@@ -13,7 +13,7 @@
 
 import scala.collection.mutable.ListBuffer
 
-import isabelle.proofdocument.{Token, ProofDocument}
+import isabelle.proofdocument.{Text, Token, ProofDocument}
 import isabelle.jedit.{Isabelle, Plugin}
 import isabelle.XML
 
@@ -31,7 +31,7 @@
 }
 
 
-class Command(val document: ProofDocument, val first: Token, val last: Token)
+class Command(text: Text, val first: Token, val last: Token)
 {
   val id = Isabelle.plugin.id()
   
@@ -74,7 +74,7 @@
 
   /* content */
 
-  def content(): String = document.getContent(this)
+  val content = text.content(proper_start, proper_stop)
 
   def next = if (last.next != null) last.next.command else null
   def prev = if (first.prev != null) first.prev.command else null
@@ -94,7 +94,7 @@
   /* markup tree */
 
   val root_node =
-    new MarkupNode(this, 0, stop - start, id, Markup.COMMAND_SPAN, content())
+    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)*/ ""
diff -r 820d0675e7b5 -r 20e9d420dbbb src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Tue Jan 20 20:05:21 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Tue Jan 20 20:32:04 2009 +0100
@@ -196,7 +196,7 @@
     cmd.status = Command.Status.UNPROCESSED
     commands.put(cmd.id, cmd)
 
-    val content = isabelle_system.symbols.encode(document.getContent(cmd))
+    val content = isabelle_system.symbols.encode(cmd.content)
     process.create_command(cmd.id, content)
     process.insert_command(if (cmd.prev == null) "" else cmd.prev.id, cmd.id)
   }