<commit_before>/*  Title:      Tools/jEdit/src/active.scala
    Author:     Makarius

Active areas within the document.
*/

package isabelle.jedit


import isabelle._

import org.gjt.sp.jedit.View


object Active
{
  def action(view: View, text: String, elem: XML.Elem)
  {
    Swing_Thread.require {}

    Document_View(view.getTextArea) match {
      case Some(doc_view) =>
        doc_view.rich_text_area.robust_body() {
          val text_area = doc_view.text_area
          val model = doc_view.model
          val buffer = model.buffer
          val snapshot = model.snapshot()

          if (!snapshot.is_outdated) {
            // FIXME avoid hard-wired stuff
            elem match {
              case XML.Elem(Markup(Markup.BROWSER, _), body) =>
                Future.fork {
                  val graph_file = Isabelle_System.tmp_file("graph")
                  File.write(graph_file, XML.content(body))
                  Isabelle_System.bash_env(null,
                    Map("GRAPH_FILE" -> Isabelle_System.posix_path(graph_file)),
                    "\"$ISABELLE_TOOL\" browser -c \"$GRAPH_FILE\" &")
                }

              case XML.Elem(Markup(Markup.GRAPHVIEW, _), body) =>
                Future.fork {
                  val graph =
                    Exn.capture {
                      isabelle.graphview.Model.decode_graph(body)
                        .transitive_reduction_acyclic
                    }
                  Swing_Thread.later { Graphview_Dockable(view, snapshot, graph) }
                }

              case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
                props match {
                  case Position.Id(id) =>
                    Isabelle.edit_command(snapshot, buffer,
                      props.exists(_ == Markup.PADDING_COMMAND), id, text)
                  case _ =>
                    if (props.exists(_ == Markup.PADDING_LINE))
                      Isabelle.insert_line_padding(text_area, text)
                    else text_area.setSelectedText(text)
                }

              case Simplifier_Trace.Active(serial, answer) =>
                Simplifier_Trace.send_reply(PIDE.session, serial, answer)

              case Protocol.Dialog(id, serial, result) =>
                model.session.dialog_result(id, serial, result)

              case _ =>
            }
          }
        }
      case None =>
    }
  }
}<commit_msg>re-focus target explicity, e.g. relevant for Sledgehammer panel;<commit_after>/*  Title:      Tools/jEdit/src/active.scala
    Author:     Makarius

Active areas within the document.
*/

package isabelle.jedit


import isabelle._

import org.gjt.sp.jedit.View


object Active
{
  def action(view: View, text: String, elem: XML.Elem)
  {
    Swing_Thread.require {}

    Document_View(view.getTextArea) match {
      case Some(doc_view) =>
        doc_view.rich_text_area.robust_body() {
          val text_area = doc_view.text_area
          val model = doc_view.model
          val buffer = model.buffer
          val snapshot = model.snapshot()

          if (!snapshot.is_outdated) {
            // FIXME avoid hard-wired stuff
            elem match {
              case XML.Elem(Markup(Markup.BROWSER, _), body) =>
                Future.fork {
                  val graph_file = Isabelle_System.tmp_file("graph")
                  File.write(graph_file, XML.content(body))
                  Isabelle_System.bash_env(null,
                    Map("GRAPH_FILE" -> Isabelle_System.posix_path(graph_file)),
                    "\"$ISABELLE_TOOL\" browser -c \"$GRAPH_FILE\" &")
                }

              case XML.Elem(Markup(Markup.GRAPHVIEW, _), body) =>
                Future.fork {
                  val graph =
                    Exn.capture {
                      isabelle.graphview.Model.decode_graph(body)
                        .transitive_reduction_acyclic
                    }
                  Swing_Thread.later { Graphview_Dockable(view, snapshot, graph) }
                }

              case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
                props match {
                  case Position.Id(id) =>
                    Isabelle.edit_command(snapshot, buffer,
                      props.exists(_ == Markup.PADDING_COMMAND), id, text)
                  case _ =>
                    if (props.exists(_ == Markup.PADDING_LINE))
                      Isabelle.insert_line_padding(text_area, text)
                    else text_area.setSelectedText(text)
                }
                text_area.requestFocus

              case Simplifier_Trace.Active(serial, answer) =>
                Simplifier_Trace.send_reply(PIDE.session, serial, answer)

              case Protocol.Dialog(id, serial, result) =>
                model.session.dialog_result(id, serial, result)

              case _ =>
            }
          }
        }
      case None =>
    }
  }
}
{'fraction_non_alphanumeric': 0.09527687296416938, 'fraction_numerical': 0.0, 'mean_word_length': 1.4977122521606507, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 25, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6938193', 'n_tokens_mistral': 1442, 'n_tokens_neox': 1359, 'n_words': 242}