tuned signature;
authorwenzelm
Tue Sep 10 11:46:51 2013 +0200 (2013-09-10)
changeset 5349707bb77881b8d
parent 53496 cd25f20a797f
child 53498 05313b45a5ae
tuned signature;
src/Tools/jEdit/src/active.scala
src/Tools/jEdit/src/isabelle.scala
     1.1 --- a/src/Tools/jEdit/src/active.scala	Tue Sep 10 00:22:12 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/active.scala	Tue Sep 10 11:46:51 2013 +0200
     1.3 @@ -26,37 +26,8 @@
     1.4            val buffer = model.buffer
     1.5            val snapshot = model.snapshot()
     1.6  
     1.7 -          def try_replace_command(padding: Boolean, exec_id: Document_ID.Exec, s: String)
     1.8 -          {
     1.9 -            snapshot.state.execs.get(exec_id).map(_.command) match {
    1.10 -              case Some(command) =>
    1.11 -                snapshot.node.command_start(command) match {
    1.12 -                  case Some(start) =>
    1.13 -                    JEdit_Lib.buffer_edit(buffer) {
    1.14 -                      val range = command.proper_range + start
    1.15 -                      if (padding) {
    1.16 -                        val pad =
    1.17 -                          JEdit_Lib.try_get_text(buffer, Text.Range(range.length - 1, range.length))
    1.18 -                            match {
    1.19 -                              case None => ""
    1.20 -                              case Some(s) => if (Symbol.is_blank(s)) "" else " "
    1.21 -                            }
    1.22 -                        buffer.insert(start + range.length, pad + s)
    1.23 -                      }
    1.24 -                      else {
    1.25 -                        buffer.remove(start, range.length)
    1.26 -                        buffer.insert(start, s)
    1.27 -                      }
    1.28 -                    }
    1.29 -                  case None =>
    1.30 -                }
    1.31 -              case None =>
    1.32 -            }
    1.33 -          }
    1.34 -
    1.35            if (!snapshot.is_outdated) {
    1.36              // FIXME avoid hard-wired stuff
    1.37 -
    1.38              elem match {
    1.39                case XML.Elem(Markup(Markup.BROWSER, _), body) =>
    1.40                  default_thread_pool.submit(() =>
    1.41 @@ -82,7 +53,8 @@
    1.42                case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
    1.43                  props match {
    1.44                    case Position.Id(exec_id) =>
    1.45 -                    try_replace_command(props.exists(_ == Markup.PADDING_COMMAND), exec_id, text)
    1.46 +                    Isabelle.edit_command(snapshot, buffer,
    1.47 +                      props.exists(_ == Markup.PADDING_COMMAND), exec_id, text)
    1.48                    case _ =>
    1.49                      if (props.exists(_ == Markup.PADDING_LINE))
    1.50                        Isabelle.insert_line_padding(text_area, text)
     2.1 --- a/src/Tools/jEdit/src/isabelle.scala	Tue Sep 10 00:22:12 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Tue Sep 10 11:46:51 2013 +0200
     2.3 @@ -142,7 +142,7 @@
     2.4      Rendering.font_size_change(view, i => i - ((i / 10) max 1))
     2.5  
     2.6  
     2.7 -  /* structured insert */
     2.8 +  /* structured edits */
     2.9  
    2.10    def insert_line_padding(text_area: JEditTextArea, text: String)
    2.11    {
    2.12 @@ -162,6 +162,39 @@
    2.13      }
    2.14    }
    2.15  
    2.16 +  def edit_command(
    2.17 +    snapshot: Document.Snapshot,
    2.18 +    buffer: Buffer,
    2.19 +    padding: Boolean,
    2.20 +    exec_id: Document_ID.Exec,
    2.21 +    s: String)
    2.22 +  {
    2.23 +    snapshot.state.execs.get(exec_id).map(_.command) match {
    2.24 +      case Some(command) =>
    2.25 +        snapshot.node.command_start(command) match {
    2.26 +          case Some(start) =>
    2.27 +            JEdit_Lib.buffer_edit(buffer) {
    2.28 +              val range = command.proper_range + start
    2.29 +              if (padding) {
    2.30 +                val pad =
    2.31 +                  JEdit_Lib.try_get_text(buffer, Text.Range(range.length - 1, range.length))
    2.32 +                    match {
    2.33 +                      case None => ""
    2.34 +                      case Some(s) => if (Symbol.is_blank(s)) "" else " "
    2.35 +                    }
    2.36 +                buffer.insert(start + range.length, pad + s)
    2.37 +              }
    2.38 +              else {
    2.39 +                buffer.remove(start, range.length)
    2.40 +                buffer.insert(start, s)
    2.41 +              }
    2.42 +            }
    2.43 +          case None =>
    2.44 +        }
    2.45 +      case None =>
    2.46 +    }
    2.47 +  }
    2.48 +
    2.49  
    2.50    /* completion */
    2.51