--- a/src/Tools/jEdit/src/active.scala Tue Sep 10 00:22:12 2013 +0200
+++ b/src/Tools/jEdit/src/active.scala Tue Sep 10 11:46:51 2013 +0200
@@ -26,37 +26,8 @@
val buffer = model.buffer
val snapshot = model.snapshot()
- def try_replace_command(padding: Boolean, exec_id: Document_ID.Exec, s: String)
- {
- snapshot.state.execs.get(exec_id).map(_.command) match {
- case Some(command) =>
- snapshot.node.command_start(command) match {
- case Some(start) =>
- JEdit_Lib.buffer_edit(buffer) {
- val range = command.proper_range + start
- if (padding) {
- val pad =
- JEdit_Lib.try_get_text(buffer, Text.Range(range.length - 1, range.length))
- match {
- case None => ""
- case Some(s) => if (Symbol.is_blank(s)) "" else " "
- }
- buffer.insert(start + range.length, pad + s)
- }
- else {
- buffer.remove(start, range.length)
- buffer.insert(start, s)
- }
- }
- case None =>
- }
- case None =>
- }
- }
-
if (!snapshot.is_outdated) {
// FIXME avoid hard-wired stuff
-
elem match {
case XML.Elem(Markup(Markup.BROWSER, _), body) =>
default_thread_pool.submit(() =>
@@ -82,7 +53,8 @@
case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
props match {
case Position.Id(exec_id) =>
- try_replace_command(props.exists(_ == Markup.PADDING_COMMAND), exec_id, text)
+ Isabelle.edit_command(snapshot, buffer,
+ props.exists(_ == Markup.PADDING_COMMAND), exec_id, text)
case _ =>
if (props.exists(_ == Markup.PADDING_LINE))
Isabelle.insert_line_padding(text_area, text)
--- a/src/Tools/jEdit/src/isabelle.scala Tue Sep 10 00:22:12 2013 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala Tue Sep 10 11:46:51 2013 +0200
@@ -142,7 +142,7 @@
Rendering.font_size_change(view, i => i - ((i / 10) max 1))
- /* structured insert */
+ /* structured edits */
def insert_line_padding(text_area: JEditTextArea, text: String)
{
@@ -162,6 +162,39 @@
}
}
+ def edit_command(
+ snapshot: Document.Snapshot,
+ buffer: Buffer,
+ padding: Boolean,
+ exec_id: Document_ID.Exec,
+ s: String)
+ {
+ snapshot.state.execs.get(exec_id).map(_.command) match {
+ case Some(command) =>
+ snapshot.node.command_start(command) match {
+ case Some(start) =>
+ JEdit_Lib.buffer_edit(buffer) {
+ val range = command.proper_range + start
+ if (padding) {
+ val pad =
+ JEdit_Lib.try_get_text(buffer, Text.Range(range.length - 1, range.length))
+ match {
+ case None => ""
+ case Some(s) => if (Symbol.is_blank(s)) "" else " "
+ }
+ buffer.insert(start + range.length, pad + s)
+ }
+ else {
+ buffer.remove(start, range.length)
+ buffer.insert(start, s)
+ }
+ }
+ case None =>
+ }
+ case None =>
+ }
+ }
+
/* completion */