src/Tools/jEdit/src/isabelle.scala
changeset 53497 07bb77881b8d
parent 53322 a4cd032172e0
child 53715 68c664737d04
     1.1 --- a/src/Tools/jEdit/src/isabelle.scala	Tue Sep 10 00:22:12 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Tue Sep 10 11:46:51 2013 +0200
     1.3 @@ -142,7 +142,7 @@
     1.4      Rendering.font_size_change(view, i => i - ((i / 10) max 1))
     1.5  
     1.6  
     1.7 -  /* structured insert */
     1.8 +  /* structured edits */
     1.9  
    1.10    def insert_line_padding(text_area: JEditTextArea, text: String)
    1.11    {
    1.12 @@ -162,6 +162,39 @@
    1.13      }
    1.14    }
    1.15  
    1.16 +  def edit_command(
    1.17 +    snapshot: Document.Snapshot,
    1.18 +    buffer: Buffer,
    1.19 +    padding: Boolean,
    1.20 +    exec_id: Document_ID.Exec,
    1.21 +    s: String)
    1.22 +  {
    1.23 +    snapshot.state.execs.get(exec_id).map(_.command) match {
    1.24 +      case Some(command) =>
    1.25 +        snapshot.node.command_start(command) match {
    1.26 +          case Some(start) =>
    1.27 +            JEdit_Lib.buffer_edit(buffer) {
    1.28 +              val range = command.proper_range + start
    1.29 +              if (padding) {
    1.30 +                val pad =
    1.31 +                  JEdit_Lib.try_get_text(buffer, Text.Range(range.length - 1, range.length))
    1.32 +                    match {
    1.33 +                      case None => ""
    1.34 +                      case Some(s) => if (Symbol.is_blank(s)) "" else " "
    1.35 +                    }
    1.36 +                buffer.insert(start + range.length, pad + s)
    1.37 +              }
    1.38 +              else {
    1.39 +                buffer.remove(start, range.length)
    1.40 +                buffer.insert(start, s)
    1.41 +              }
    1.42 +            }
    1.43 +          case None =>
    1.44 +        }
    1.45 +      case None =>
    1.46 +    }
    1.47 +  }
    1.48 +
    1.49  
    1.50    /* completion */
    1.51