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