take content of asset for description in status-view of Sidekick
authorimmler@in.tum.de
Sat, 24 Jan 2009 16:31:04 +0100
changeset 34510 6106e71c6ee5
parent 34496 1b2995592bb9
child 34511 5839e34ef0bd
take content of asset for description in status-view of Sidekick
src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Tue Jan 20 23:13:54 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala	Sat Jan 24 16:31:04 2009 +0100
@@ -100,7 +100,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)
   }
 }