equal
deleted
inserted
replaced
154 |
154 |
155 private def send(cmd: Command) { |
155 private def send(cmd: Command) { |
156 cmd.status = Command.Status.UNPROCESSED |
156 cmd.status = Command.Status.UNPROCESSED |
157 commands.put(cmd.id, cmd) |
157 commands.put(cmd.id, cmd) |
158 |
158 |
159 val props = new Properties |
|
160 props.setProperty(Markup.ID, cmd.id) |
|
161 props.setProperty(Markup.OFFSET, "1") |
|
162 |
|
163 val content = isabelle_symbols.encode(document.getContent(cmd)) |
159 val content = isabelle_symbols.encode(document.getContent(cmd)) |
164 process.create_command(props, content) |
160 process.create_command(cmd.id, content) |
165 process.insert_command(if (cmd.previous == null) "" else cmd.previous.id, cmd.id) |
161 process.insert_command(if (cmd.previous == null) "" else cmd.previous.id, cmd.id) |
166 } |
162 } |
167 |
163 |
168 def remove(cmd: Command) { |
164 def remove(cmd: Command) { |
169 cmd.status = Command.Status.REMOVE |
165 cmd.status = Command.Status.REMOVE |