# HG changeset patch
# User immler@in.tum.de
# Date 1233487267 -3600
# Node ID 5839e34ef0bdb6d10fcba16f33f69734b138c4f7
# Parent  6106e71c6ee5b3ef4aec9ad74a90339f203ff07f# Parent  839d1f0b2dd1a72ffa83846ab32b2bd3ed7ab681
merge

diff -r 839d1f0b2dd1 -r 5839e34ef0bd src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Tue Jan 27 22:23:45 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala	Sun Feb 01 12:21:07 2009 +0100
@@ -103,7 +103,7 @@
     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)*/ ""
+    val markup_content = content.substring(begin, end)
     new MarkupNode(this, begin, end, id, kind, markup_content)
   }
 }