# HG changeset patch
# User wenzelm
# Date 1468613829 -7200
# Node ID 34859964488725f2d5526b08fb73d0c039f901ec
# Parent  79122bdd440447ca2a222172a40b0887b3224fe0
more structured edit, including indentation;

diff -r 79122bdd4404 -r 348599644887 src/Tools/jEdit/src/active.scala
--- a/src/Tools/jEdit/src/active.scala	Fri Jul 15 22:11:54 2016 +0200
+++ b/src/Tools/jEdit/src/active.scala	Fri Jul 15 22:17:09 2016 +0200
@@ -58,7 +58,7 @@
                 if (buffer.isEditable) {
                   props match {
                     case Position.Id(id) =>
-                      Isabelle.edit_command(snapshot, buffer,
+                      Isabelle.edit_command(snapshot, text_area,
                         props.contains(Markup.PADDING_COMMAND), id, text)
                     case _ =>
                       if (props.contains(Markup.PADDING_LINE))
diff -r 79122bdd4404 -r 348599644887 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Fri Jul 15 22:11:54 2016 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Fri Jul 15 22:17:09 2016 +0200
@@ -322,24 +322,32 @@
 
   def edit_command(
     snapshot: Document.Snapshot,
-    buffer: Buffer,
+    text_area: TextArea,
     padding: Boolean,
     id: Document_ID.Generic,
-    s: String)
+    text: String)
   {
-    if (!snapshot.is_outdated) {
+    val buffer = text_area.getBuffer
+    if (!snapshot.is_outdated && text != "") {
       (snapshot.state.find_command(snapshot.version, id), PIDE.document_model(buffer)) match {
         case (Some((node, command)), Some(model)) if command.node_name == model.node_name =>
           node.command_start(command) match {
             case Some(start) =>
               JEdit_Lib.buffer_edit(buffer) {
                 val range = command.proper_range + start
-                if (padding) {
-                  buffer.insert(start + range.length, "\n" + s)
-                }
-                else {
-                  buffer.remove(start, range.length)
-                  buffer.insert(start, s)
+                JEdit_Lib.buffer_edit(buffer) {
+                  if (padding) {
+                    text_area.moveCaretPosition(start + range.length)
+                    text_area.setSelectedText("\n" + text)
+                    val end_line = text_area.getCaretLine
+                    val start_line = end_line - split_lines(text).length
+                    buffer.indentLines(start_line, end_line)
+                  }
+                  else {
+                    buffer.remove(start, range.length)
+                    text_area.moveCaretPosition(start)
+                    text_area.setSelectedText(text)
+                  }
                 }
               }
             case None =>