equal
deleted
inserted
replaced
38 buffer <- JEdit_Lib.jedit_buffer(listData(index).node) |
38 buffer <- JEdit_Lib.jedit_buffer(listData(index).node) |
39 model <- PIDE.document_model(buffer) |
39 model <- PIDE.document_model(buffer) |
40 } model.node_required = !model.node_required |
40 } model.node_required = !model.node_required |
41 } |
41 } |
42 } |
42 } |
43 else if (clicks == 2) PIDE.editor.goto(view, listData(index).node) |
43 else if (clicks == 2) PIDE.editor.goto_file(view, listData(index).node) |
44 } |
44 } |
45 case MouseMoved(_, point, _) => |
45 case MouseMoved(_, point, _) => |
46 val index = peer.locationToIndex(point) |
46 val index = peer.locationToIndex(point) |
47 if (index >= 0 && in_checkbox(peer.indexToLocation(index), point)) |
47 if (index >= 0 && in_checkbox(peer.indexToLocation(index), point)) |
48 tooltip = "Mark as required for continuous checking" |
48 tooltip = "Mark as required for continuous checking" |