src/Tools/jEdit/src/active.scala
author wenzelm
Wed Jul 23 11:19:24 2014 +0200 (2014-07-23)
changeset 57612 990ffb84489b
parent 57594 037f3b251df5
child 57878 51a2f9140175
permissions -rw-r--r--
clarified module name: facilitate alternative GUI frameworks;
wenzelm@50450
     1
/*  Title:      Tools/jEdit/src/active.scala
wenzelm@49492
     2
    Author:     Makarius
wenzelm@49492
     3
wenzelm@50450
     4
Active areas within the document.
wenzelm@49492
     5
*/
wenzelm@49492
     6
wenzelm@49492
     7
package isabelle.jedit
wenzelm@49492
     8
wenzelm@49492
     9
wenzelm@49492
    10
import isabelle._
wenzelm@49492
    11
wenzelm@49493
    12
import org.gjt.sp.jedit.View
wenzelm@49492
    13
wenzelm@49492
    14
wenzelm@50450
    15
object Active
wenzelm@49492
    16
{
wenzelm@50450
    17
  def action(view: View, text: String, elem: XML.Elem)
wenzelm@49492
    18
  {
wenzelm@57612
    19
    GUI_Thread.require {}
wenzelm@49492
    20
wenzelm@49492
    21
    Document_View(view.getTextArea) match {
wenzelm@49492
    22
      case Some(doc_view) =>
wenzelm@49492
    23
        doc_view.rich_text_area.robust_body() {
wenzelm@50215
    24
          val text_area = doc_view.text_area
wenzelm@49492
    25
          val model = doc_view.model
wenzelm@49492
    26
          val buffer = model.buffer
wenzelm@49492
    27
          val snapshot = model.snapshot()
wenzelm@49493
    28
wenzelm@50164
    29
          if (!snapshot.is_outdated) {
wenzelm@50715
    30
            // FIXME avoid hard-wired stuff
wenzelm@50450
    31
            elem match {
wenzelm@50715
    32
              case XML.Elem(Markup(Markup.BROWSER, _), body) =>
wenzelm@56729
    33
                Future.fork {
wenzelm@56729
    34
                  val graph_file = Isabelle_System.tmp_file("graph")
wenzelm@56729
    35
                  File.write(graph_file, XML.content(body))
wenzelm@56729
    36
                  Isabelle_System.bash_env(null,
wenzelm@56729
    37
                    Map("GRAPH_FILE" -> Isabelle_System.posix_path(graph_file)),
wenzelm@56729
    38
                    "\"$ISABELLE_TOOL\" browser -c \"$GRAPH_FILE\" &")
wenzelm@56729
    39
                }
wenzelm@50715
    40
wenzelm@50715
    41
              case XML.Elem(Markup(Markup.GRAPHVIEW, _), body) =>
wenzelm@56729
    42
                Future.fork {
wenzelm@56729
    43
                  val graph =
wenzelm@56729
    44
                    Exn.capture {
wenzelm@56729
    45
                      isabelle.graphview.Model.decode_graph(body)
wenzelm@56729
    46
                        .transitive_reduction_acyclic
wenzelm@56729
    47
                    }
wenzelm@57612
    48
                  GUI_Thread.later { Graphview_Dockable(view, snapshot, graph) }
wenzelm@56729
    49
                }
wenzelm@50450
    50
wenzelm@57594
    51
              case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, _), _) =>
wenzelm@57612
    52
                GUI_Thread.later {
wenzelm@57594
    53
                  view.getDockableWindowManager.showDockableWindow("isabelle-simplifier-trace")
wenzelm@57594
    54
                }
wenzelm@57594
    55
wenzelm@50500
    56
              case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
wenzelm@50500
    57
                props match {
wenzelm@54640
    58
                  case Position.Id(id) =>
wenzelm@53497
    59
                    Isabelle.edit_command(snapshot, buffer,
wenzelm@54640
    60
                      props.exists(_ == Markup.PADDING_COMMAND), id, text)
wenzelm@50500
    61
                  case _ =>
wenzelm@50500
    62
                    if (props.exists(_ == Markup.PADDING_LINE))
wenzelm@50500
    63
                      Isabelle.insert_line_padding(text_area, text)
wenzelm@50500
    64
                    else text_area.setSelectedText(text)
wenzelm@50500
    65
                }
wenzelm@56999
    66
                text_area.requestFocus
wenzelm@50500
    67
wenzelm@52081
    68
              case Protocol.Dialog(id, serial, result) =>
wenzelm@52081
    69
                model.session.dialog_result(id, serial, result)
wenzelm@52081
    70
wenzelm@50215
    71
              case _ =>
wenzelm@50164
    72
            }
wenzelm@49492
    73
          }
wenzelm@49492
    74
        }
wenzelm@49492
    75
      case None =>
wenzelm@49492
    76
    }
wenzelm@49492
    77
  }
wenzelm@49492
    78
}