# HG changeset patch
# User wenzelm
# Date 1378806411 -7200
# Node ID 07bb77881b8d99e3fb5163cd4a24784e87413b0a
# Parent  cd25f20a797f44ceb409f511438968ee5eaad30c
tuned signature;

diff -r cd25f20a797f -r 07bb77881b8d src/Tools/jEdit/src/active.scala
--- 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)
diff -r cd25f20a797f -r 07bb77881b8d src/Tools/jEdit/src/isabelle.scala
--- 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 */