equal
deleted
inserted
replaced
262 val ML_OPEN = "ML_open" |
262 val ML_OPEN = "ML_open" |
263 val ML_STRUCTURE = "ML_structure" |
263 val ML_STRUCTURE = "ML_structure" |
264 val ML_TYPING = "ML_typing" |
264 val ML_TYPING = "ML_typing" |
265 |
265 |
266 val ML_BREAKPOINT = "ML_breakpoint" |
266 val ML_BREAKPOINT = "ML_breakpoint" |
267 val ML_Breakpoint = new Markup_Long(ML_BREAKPOINT, SERIAL) |
|
268 |
267 |
269 |
268 |
270 /* outer syntax */ |
269 /* outer syntax */ |
271 |
270 |
272 val COMMAND = "command" |
271 val COMMAND = "command" |