removed unused markup (cf. 2f7d91242b99);
authorwenzelm
Mon, 21 Jul 2014 17:39:20 +0200
changeset 57595 e2305b9d1534
parent 57594 037f3b251df5
child 57596 3a1b1bda702f
removed unused markup (cf. 2f7d91242b99);
src/Pure/PIDE/markup.scala
src/Tools/jEdit/src/rendering.scala
--- a/src/Pure/PIDE/markup.scala	Mon Jul 21 17:37:22 2014 +0200
+++ b/src/Pure/PIDE/markup.scala	Mon Jul 21 17:39:20 2014 +0200
@@ -464,7 +464,6 @@
 
   /* simplifier trace */
 
-  val SIMP_TRACE = "simp_trace"
   val SIMP_TRACE_PANEL = "simp_trace_panel"
 
   val SIMP_TRACE_LOG = "simp_trace_log"
--- a/src/Tools/jEdit/src/rendering.scala	Mon Jul 21 17:37:22 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Mon Jul 21 17:39:20 2014 +0200
@@ -149,7 +149,7 @@
 
   private val active_elements =
     Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
-      Markup.SENDBACK, Markup.SIMP_TRACE, Markup.SIMP_TRACE_PANEL)
+      Markup.SENDBACK, Markup.SIMP_TRACE_PANEL)
 
   private val tooltip_message_elements =
     Markup.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)