src/Tools/jEdit/src/active.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 64664 951507563033
child 64882 c3b42ac0cf81
permissions -rw-r--r--
tuned signature;
     1 /*  Title:      Tools/jEdit/src/active.scala
     2     Author:     Makarius
     3 
     4 Active areas within the document.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import org.gjt.sp.jedit.View
    13 
    14 
    15 object Active
    16 {
    17   def action(view: View, text: String, elem: XML.Elem)
    18   {
    19     GUI_Thread.require {}
    20 
    21     Document_View(view.getTextArea) match {
    22       case Some(doc_view) =>
    23         doc_view.rich_text_area.robust_body() {
    24           val text_area = doc_view.text_area
    25           val model = doc_view.model
    26           val buffer = model.buffer
    27           val snapshot = model.snapshot()
    28 
    29           if (!snapshot.is_outdated) {
    30             // FIXME avoid hard-wired stuff
    31             elem match {
    32               case XML.Elem(Markup(Markup.BROWSER, _), body) =>
    33                 Standard_Thread.fork("browser") {
    34                   val graph_file = Isabelle_System.tmp_file("graph")
    35                   File.write(graph_file, XML.content(body))
    36                   Isabelle_System.bash("isabelle browser -c " + File.bash_path(graph_file) + " &")
    37                 }
    38 
    39               case XML.Elem(Markup(Markup.GRAPHVIEW, _), body) =>
    40                 Standard_Thread.fork("graphview") {
    41                   val graph =
    42                     Exn.capture { Graph_Display.decode_graph(body).transitive_reduction_acyclic }
    43                   GUI_Thread.later { Graphview_Dockable(view, snapshot, graph) }
    44                 }
    45 
    46               case XML.Elem(Markup(Markup.JEDIT_ACTION, _), body) =>
    47                 GUI_Thread.later {
    48                   view.getInputHandler.invokeAction(XML.content(body))
    49                 }
    50 
    51               case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, props), _) =>
    52                 val link =
    53                   props match {
    54                     case Position.Id(id) => PIDE.editor.hyperlink_command(true, snapshot, id)
    55                     case _ => None
    56                   }
    57                 GUI_Thread.later {
    58                   link.foreach(_.follow(view))
    59                   view.getDockableWindowManager.showDockableWindow("isabelle-simplifier-trace")
    60                 }
    61 
    62               case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
    63                 if (buffer.isEditable) {
    64                   props match {
    65                     case Position.Id(id) =>
    66                       Isabelle.edit_command(snapshot, text_area,
    67                         props.contains(Markup.PADDING_COMMAND), id, text)
    68                     case _ =>
    69                       if (props.contains(Markup.PADDING_LINE))
    70                         Isabelle.insert_line_padding(text_area, text)
    71                       else text_area.setSelectedText(text)
    72                   }
    73                   text_area.requestFocus
    74                 }
    75 
    76               case Protocol.Dialog(id, serial, result) =>
    77                 model.session.dialog_result(id, serial, result)
    78 
    79               case _ =>
    80             }
    81           }
    82         }
    83       case None =>
    84     }
    85   }
    86 }