equal
deleted
inserted
replaced
50 else { |
50 else { |
51 val theory_view = theory_view_opt.get |
51 val theory_view = theory_view_opt.get |
52 val document = theory_view.current_document() |
52 val document = theory_view.current_document() |
53 val offset = theory_view.from_current(document, original_offset) |
53 val offset = theory_view.from_current(document, original_offset) |
54 val cmd = document.find_command_at(offset) |
54 val cmd = document.find_command_at(offset) |
55 val state = document.states(cmd) |
|
56 if (cmd != null) { |
55 if (cmd != null) { |
57 val ref_o = cmd.ref_at(document, offset - cmd.start(document)) |
56 val ref_o = cmd.ref_at(document, offset - cmd.start(document)) |
58 if (!ref_o.isDefined) null |
57 if (!ref_o.isDefined) null |
59 else { |
58 else { |
60 val ref = ref_o.get |
59 val ref = ref_o.get |