1/*  Title:      Tools/jEdit/src/active.scala
2    Author:     Makarius
3
4Active areas within the document.
5*/
6
7package isabelle.jedit
8
9
10import isabelle._
11
12import org.gjt.sp.jedit.View
13
14
15object Active
16{
17  def action(view: View, text: String, elem: XML.Elem)
18  {
19    GUI_Thread.require {}
20
21    Document_View.get(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}
87