src/Pure/PIDE/markup.scala
changeset 60882 45bfd18835f1
parent 60842 5510c8444bc4
child 61449 4f31f79cf2d1
     1.1 --- a/src/Pure/PIDE/markup.scala	Mon Aug 10 20:25:04 2015 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Mon Aug 10 20:42:59 2015 +0200
     1.3 @@ -264,7 +264,6 @@
     1.4    val ML_TYPING = "ML_typing"
     1.5  
     1.6    val ML_BREAKPOINT = "ML_breakpoint"
     1.7 -  val ML_Breakpoint = new Markup_Long(ML_BREAKPOINT, SERIAL)
     1.8  
     1.9  
    1.10    /* outer syntax */