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