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 */