treat comments like seperate commands,
as they could also be at the beginning of a document

--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Wed May 27 14:56:49 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Wed May 27 15:24:01 2009 +0200
@@ -175,7 +175,7 @@
       tokens match {
         case Nil => Nil
         case t::ts =>
-          val (cmd,rest) = ts.span(_.kind != Token.Kind.COMMAND_START)
+          val (cmd,rest) = ts.span(t => t.kind != Token.Kind.COMMAND_START && t.kind != Token.Kind.COMMENT)
           new Command(t::cmd, new_token_start) :: tokens_to_commands (rest)
       }
     }

--- a/src/Tools/jEdit/src/prover/Command.scala	Wed May 27 14:56:49 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala	Wed May 27 15:24:01 2009 +0200
@@ -38,7 +38,7 @@
   override def toString = name
 
   val name = tokens.head.content
-  val content:String = Token.string_from_tokens(tokens.takeWhile(_.kind != Token.Kind.COMMENT), starts)
+  val content:String = Token.string_from_tokens(tokens, starts)
 
   def start(doc: ProofDocument) = doc.token_start(tokens.first)
   def stop(doc: ProofDocument) = doc.token_start(tokens.last) + tokens.last.length