src/Tools/jEdit/src/active.scala
author wenzelm
Mon, 10 Dec 2012 13:52:33 +0100
changeset 50450 358b6020f8b6
parent 50341 src/Tools/jEdit/src/sendback.scala@0c65a7cfc0f3
child 50452 bfb5964e3041
permissions -rw-r--r--
generalized notion of active area, where sendback is just one application; some support for graphview via active area;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
50450
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50341
diff changeset
     1
/*  Title:      Tools/jEdit/src/active.scala
49492
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
     3
50450
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50341
diff changeset
     4
Active areas within the document.
49492
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
     5
*/
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
     6
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
     8
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
     9
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    10
import isabelle._
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    11
49493
db58490a68ac more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents: 49492
diff changeset
    12
import org.gjt.sp.jedit.View
49492
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    13
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    14
50450
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50341
diff changeset
    15
object Active
49492
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    16
{
50450
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50341
diff changeset
    17
  def action(view: View, text: String, elem: XML.Elem)
49492
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    18
  {
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    19
    Swing_Thread.require()
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    20
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    21
    Document_View(view.getTextArea) match {
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    22
      case Some(doc_view) =>
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    23
        doc_view.rich_text_area.robust_body() {
50215
97959912840a more general sendback properties;
wenzelm
parents: 50195
diff changeset
    24
          val text_area = doc_view.text_area
49492
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    25
          val model = doc_view.model
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    26
          val buffer = model.buffer
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    27
          val snapshot = model.snapshot()
49493
db58490a68ac more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents: 49492
diff changeset
    28
50164
77668b522ffe some support for implicit senback, meaning that it uses the caret position instead of explicit command exec_id;
wenzelm
parents: 49493
diff changeset
    29
          if (!snapshot.is_outdated) {
50450
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50341
diff changeset
    30
            elem match {
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50341
diff changeset
    31
              case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50341
diff changeset
    32
                props match {
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50341
diff changeset
    33
                  case Position.Id(exec_id) =>
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50341
diff changeset
    34
                    snapshot.state.execs.get(exec_id).map(_.command) match {
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50341
diff changeset
    35
                      case Some(command) =>
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50341
diff changeset
    36
                        snapshot.node.command_start(command) match {
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50341
diff changeset
    37
                          case Some(start) =>
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50341
diff changeset
    38
                            JEdit_Lib.buffer_edit(buffer) {
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50341
diff changeset
    39
                              buffer.remove(start, command.proper_range.length)
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50341
diff changeset
    40
                              buffer.insert(start, text)
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50341
diff changeset
    41
                            }
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50341
diff changeset
    42
                          case None =>
50164
77668b522ffe some support for implicit senback, meaning that it uses the caret position instead of explicit command exec_id;
wenzelm
parents: 49493
diff changeset
    43
                        }
77668b522ffe some support for implicit senback, meaning that it uses the caret position instead of explicit command exec_id;
wenzelm
parents: 49493
diff changeset
    44
                      case None =>
77668b522ffe some support for implicit senback, meaning that it uses the caret position instead of explicit command exec_id;
wenzelm
parents: 49493
diff changeset
    45
                    }
50450
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50341
diff changeset
    46
                  case _ =>
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50341
diff changeset
    47
                    if (props.exists(_ == Markup.PADDING_LINE))
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50341
diff changeset
    48
                      Isabelle.insert_line_padding(text_area, text)
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50341
diff changeset
    49
                    else text_area.setSelectedText(text)
50164
77668b522ffe some support for implicit senback, meaning that it uses the caret position instead of explicit command exec_id;
wenzelm
parents: 49493
diff changeset
    50
                }
50450
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50341
diff changeset
    51
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50341
diff changeset
    52
              case XML.Elem(Markup(Markup.GRAPHVIEW, props), body) =>
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50341
diff changeset
    53
                java.lang.System.err.println("graphview " + props)  // FIXME
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50341
diff changeset
    54
50215
97959912840a more general sendback properties;
wenzelm
parents: 50195
diff changeset
    55
              case _ =>
50164
77668b522ffe some support for implicit senback, meaning that it uses the caret position instead of explicit command exec_id;
wenzelm
parents: 49493
diff changeset
    56
            }
49492
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    57
          }
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    58
        }
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    59
      case None =>
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    60
    }
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    61
  }
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    62
}
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    63