removed unused markup (cf. 2f7d91242b99);
authorwenzelm
Mon Jul 21 17:39:20 2014 +0200 (2014-07-21)
changeset 57595e2305b9d1534
parent 57594 037f3b251df5
child 57596 3a1b1bda702f
removed unused markup (cf. 2f7d91242b99);
src/Pure/PIDE/markup.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/PIDE/markup.scala	Mon Jul 21 17:37:22 2014 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Mon Jul 21 17:39:20 2014 +0200
     1.3 @@ -464,7 +464,6 @@
     1.4  
     1.5    /* simplifier trace */
     1.6  
     1.7 -  val SIMP_TRACE = "simp_trace"
     1.8    val SIMP_TRACE_PANEL = "simp_trace_panel"
     1.9  
    1.10    val SIMP_TRACE_LOG = "simp_trace_log"
     2.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Jul 21 17:37:22 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Jul 21 17:39:20 2014 +0200
     2.3 @@ -149,7 +149,7 @@
     2.4  
     2.5    private val active_elements =
     2.6      Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
     2.7 -      Markup.SENDBACK, Markup.SIMP_TRACE, Markup.SIMP_TRACE_PANEL)
     2.8 +      Markup.SENDBACK, Markup.SIMP_TRACE_PANEL)
     2.9  
    2.10    private val tooltip_message_elements =
    2.11      Markup.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)