# HG changeset patch # User wenzelm # Date 1405957160 -7200 # Node ID e2305b9d1534486022bf5e175ad8700eb2f57ae7 # Parent 037f3b251df5b70796629d40fdd5794b1dc28dc4 removed unused markup (cf. 2f7d91242b99); diff -r 037f3b251df5 -r e2305b9d1534 src/Pure/PIDE/markup.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" diff -r 037f3b251df5 -r e2305b9d1534 src/Tools/jEdit/src/rendering.scala --- 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)