24 val text_area = doc_view.text_area |
24 val text_area = doc_view.text_area |
25 val model = doc_view.model |
25 val model = doc_view.model |
26 val buffer = model.buffer |
26 val buffer = model.buffer |
27 val snapshot = model.snapshot() |
27 val snapshot = model.snapshot() |
28 |
28 |
29 def try_replace_command(exec_id: Document_ID.Exec, s: String) |
29 def try_replace_command(padding: Boolean, exec_id: Document_ID.Exec, s: String) |
30 { |
30 { |
31 snapshot.state.execs.get(exec_id).map(_.command) match { |
31 snapshot.state.execs.get(exec_id).map(_.command) match { |
32 case Some(command) => |
32 case Some(command) => |
33 snapshot.node.command_start(command) match { |
33 snapshot.node.command_start(command) match { |
34 case Some(start) => |
34 case Some(start) => |
35 JEdit_Lib.buffer_edit(buffer) { |
35 JEdit_Lib.buffer_edit(buffer) { |
36 buffer.remove(start, command.proper_range.length) |
36 val range = command.proper_range + start |
37 buffer.insert(start, s) |
37 if (padding) { |
|
38 val pad = |
|
39 JEdit_Lib.try_get_text(buffer, Text.Range(range.length - 1, range.length)) |
|
40 match { |
|
41 case None => "" |
|
42 case Some(s) => if (Symbol.is_blank(s)) "" else " " |
|
43 } |
|
44 buffer.insert(start + range.length, pad + s) |
|
45 } |
|
46 else { |
|
47 buffer.remove(start, range.length) |
|
48 buffer.insert(start, s) |
|
49 } |
38 } |
50 } |
39 case None => |
51 case None => |
40 } |
52 } |
41 case None => |
53 case None => |
42 } |
54 } |
68 }) |
80 }) |
69 |
81 |
70 case XML.Elem(Markup(Markup.SENDBACK, props), _) => |
82 case XML.Elem(Markup(Markup.SENDBACK, props), _) => |
71 props match { |
83 props match { |
72 case Position.Id(exec_id) => |
84 case Position.Id(exec_id) => |
73 try_replace_command(exec_id, text) |
85 try_replace_command(props.exists(_ == Markup.PADDING_COMMAND), exec_id, text) |
74 case _ => |
86 case _ => |
75 if (props.exists(_ == Markup.PADDING_LINE)) |
87 if (props.exists(_ == Markup.PADDING_LINE)) |
76 Isabelle.insert_line_padding(text_area, text) |
88 Isabelle.insert_line_padding(text_area, text) |
77 else text_area.setSelectedText(text) |
89 else text_area.setSelectedText(text) |
78 } |
90 } |