equal
deleted
inserted
replaced
108 val line = if (prev == null) 0 else previous.line + 1 |
108 val line = if (prev == null) 0 else previous.line + 1 |
109 val context = new Isabelle_Token_Marker.LineContext(line, previous) |
109 val context = new Isabelle_Token_Marker.LineContext(line, previous) |
110 val start = model.buffer.getLineStartOffset(line) |
110 val start = model.buffer.getLineStartOffset(line) |
111 val stop = start + line_segment.count |
111 val stop = start + line_segment.count |
112 |
112 |
113 val document = model.current_document() |
113 val document = model.recent_document() |
114 def to: Int => Int = model.to_current(document, _) |
114 def to: Int => Int = model.to_current(document, _) |
115 def from: Int => Int = model.from_current(document, _) |
115 def from: Int => Int = model.from_current(document, _) |
116 |
116 |
117 var next_x = start |
117 var next_x = start |
118 var cmd = document.command_at(from(start)) |
118 var cmd = document.command_at(from(start)) |