# HG changeset patch
# User immler@in.tum.de
# Date 1243430641 -7200
# Node ID 70d11544685fb199ea20b1fcc5f59fbfa426132f
# Parent  d68352286c9131344251581a2e0d2e3fc4a3a38e
treat comments like seperate commands,
as they could also be at the beginning of a document

diff -r d68352286c91 -r 70d11544685f src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- 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)
       }
     }
diff -r d68352286c91 -r 70d11544685f src/Tools/jEdit/src/prover/Command.scala
--- 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