src/Tools/jEdit/src/active.scala
author wenzelm
Mon, 19 May 2014 15:00:11 +0200
changeset 56999 d926fc73b554
parent 56729 1da2272a06a4
child 57593 2f7d91242b99
permissions -rw-r--r--
re-focus target explicity, e.g. relevant for Sledgehammer panel;
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
  {
56662
f373fb77e0a4 avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
wenzelm
parents: 56428
diff changeset
    19
    Swing_Thread.require {}
49492
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) {
50715
8cfd585b9162 prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents: 50500
diff changeset
    30
            // FIXME avoid hard-wired stuff
50450
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50341
diff changeset
    31
            elem match {
50715
8cfd585b9162 prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents: 50500
diff changeset
    32
              case XML.Elem(Markup(Markup.BROWSER, _), body) =>
56729
1da2272a06a4 prefer Isabelle/Scala operations;
wenzelm
parents: 56662
diff changeset
    33
                Future.fork {
1da2272a06a4 prefer Isabelle/Scala operations;
wenzelm
parents: 56662
diff changeset
    34
                  val graph_file = Isabelle_System.tmp_file("graph")
1da2272a06a4 prefer Isabelle/Scala operations;
wenzelm
parents: 56662
diff changeset
    35
                  File.write(graph_file, XML.content(body))
1da2272a06a4 prefer Isabelle/Scala operations;
wenzelm
parents: 56662
diff changeset
    36
                  Isabelle_System.bash_env(null,
1da2272a06a4 prefer Isabelle/Scala operations;
wenzelm
parents: 56662
diff changeset
    37
                    Map("GRAPH_FILE" -> Isabelle_System.posix_path(graph_file)),
1da2272a06a4 prefer Isabelle/Scala operations;
wenzelm
parents: 56662
diff changeset
    38
                    "\"$ISABELLE_TOOL\" browser -c \"$GRAPH_FILE\" &")
1da2272a06a4 prefer Isabelle/Scala operations;
wenzelm
parents: 56662
diff changeset
    39
                }
50715
8cfd585b9162 prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents: 50500
diff changeset
    40
8cfd585b9162 prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents: 50500
diff changeset
    41
              case XML.Elem(Markup(Markup.GRAPHVIEW, _), body) =>
56729
1da2272a06a4 prefer Isabelle/Scala operations;
wenzelm
parents: 56662
diff changeset
    42
                Future.fork {
1da2272a06a4 prefer Isabelle/Scala operations;
wenzelm
parents: 56662
diff changeset
    43
                  val graph =
1da2272a06a4 prefer Isabelle/Scala operations;
wenzelm
parents: 56662
diff changeset
    44
                    Exn.capture {
1da2272a06a4 prefer Isabelle/Scala operations;
wenzelm
parents: 56662
diff changeset
    45
                      isabelle.graphview.Model.decode_graph(body)
1da2272a06a4 prefer Isabelle/Scala operations;
wenzelm
parents: 56662
diff changeset
    46
                        .transitive_reduction_acyclic
1da2272a06a4 prefer Isabelle/Scala operations;
wenzelm
parents: 56662
diff changeset
    47
                    }
1da2272a06a4 prefer Isabelle/Scala operations;
wenzelm
parents: 56662
diff changeset
    48
                  Swing_Thread.later { Graphview_Dockable(view, snapshot, graph) }
1da2272a06a4 prefer Isabelle/Scala operations;
wenzelm
parents: 56662
diff changeset
    49
                }
50450
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50341
diff changeset
    50
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
    51
              case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
    52
                props match {
54640
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53497
diff changeset
    53
                  case Position.Id(id) =>
53497
07bb77881b8d tuned signature;
wenzelm
parents: 52697
diff changeset
    54
                    Isabelle.edit_command(snapshot, buffer,
54640
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53497
diff changeset
    55
                      props.exists(_ == Markup.PADDING_COMMAND), id, text)
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
    56
                  case _ =>
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
    57
                    if (props.exists(_ == Markup.PADDING_LINE))
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
    58
                      Isabelle.insert_line_padding(text_area, text)
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
    59
                    else text_area.setSelectedText(text)
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
    60
                }
56999
d926fc73b554 re-focus target explicity, e.g. relevant for Sledgehammer panel;
wenzelm
parents: 56729
diff changeset
    61
                text_area.requestFocus
50500
c94bba7906d2 identify dialogs via official serial and maintain as result message;
wenzelm
parents: 50498
diff changeset
    62
55553
99409ccbe04a more standard names for protocol and markup elements;
wenzelm
parents: 55316
diff changeset
    63
              case Simplifier_Trace.Active(serial, answer) =>
55316
885500f4aa6a interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents: 54640
diff changeset
    64
                Simplifier_Trace.send_reply(PIDE.session, serial, answer)
885500f4aa6a interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents: 54640
diff changeset
    65
52081
29566b6810f7 discontinued odd workaround for scala-2.9.2, which is hopefully obsolete in scala-2.10.x;
wenzelm
parents: 50715
diff changeset
    66
              case Protocol.Dialog(id, serial, result) =>
29566b6810f7 discontinued odd workaround for scala-2.9.2, which is hopefully obsolete in scala-2.10.x;
wenzelm
parents: 50715
diff changeset
    67
                model.session.dialog_result(id, serial, result)
29566b6810f7 discontinued odd workaround for scala-2.9.2, which is hopefully obsolete in scala-2.10.x;
wenzelm
parents: 50715
diff changeset
    68
50215
97959912840a more general sendback properties;
wenzelm
parents: 50195
diff changeset
    69
              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
    70
            }
49492
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    71
          }
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    72
        }
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    73
      case None =>
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    74
    }
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    75
  }
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    76
}