src/Tools/jEdit/src/isabelle.scala

more Isabelle/jEdit actions;

/*  Title:      Tools/jEdit/src/isabelle.scala
    Author:     Makarius

Global configuration and convenience operations for Isabelle/jEdit.
*/

package isabelle.jedit


import isabelle._

import java.awt.{Frame, Point}

import scala.swing.CheckBox
import scala.swing.event.ButtonClicked

import org.gjt.sp.jedit.{jEdit, View, Buffer}
import org.gjt.sp.jedit.buffer.JEditBuffer
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, StructureMatcher, Selection}
import org.gjt.sp.jedit.syntax.TokenMarker
import org.gjt.sp.jedit.indent.IndentRule
import org.gjt.sp.jedit.gui.{DockableWindowManager, CompleteWord}
import org.jedit.options.CombinedOptions


object Isabelle
{
  /* editor modes */

  val modes =
    List(
      "isabelle",         // theory source
      "isabelle-ml",      // ML source
      "isabelle-news",    // NEWS
      "isabelle-options", // etc/options
      "isabelle-output",  // pretty text area output
      "isabelle-root",    // session ROOT
      "sml")              // Standard ML (not Isabelle/ML)

  private val ml_syntax: Outer_Syntax =
    Outer_Syntax.empty.no_tokens.
      set_language_context(Completion.Language_Context.ML_outer)

  private val sml_syntax: Outer_Syntax =
    Outer_Syntax.empty.no_tokens.
      set_language_context(Completion.Language_Context.SML_outer)

  private val news_syntax: Outer_Syntax =
    Outer_Syntax.empty.no_tokens

  def mode_syntax(mode: String): Option[Outer_Syntax] =
    mode match {
      case "isabelle" => Some(PIDE.resources.session_base.overall_syntax)
      case "isabelle-options" => Some(Options.options_syntax)
      case "isabelle-root" => Some(Sessions.root_syntax)
      case "isabelle-ml" => Some(ml_syntax)
      case "isabelle-news" => Some(news_syntax)
      case "isabelle-output" => None
      case "sml" => Some(sml_syntax)
      case _ => None
    }

  def buffer_syntax(buffer: JEditBuffer): Option[Outer_Syntax] =
    if (buffer == null) None
    else
      (JEdit_Lib.buffer_mode(buffer), Document_Model.get(buffer)) match {
        case ("isabelle", Some(model)) =>
          Some(PIDE.session.recent_syntax(model.node_name))
        case (mode, _) => mode_syntax(mode)
      }


  /* token markers */

  private val mode_markers: Map[String, TokenMarker] =
    Map(modes.map(mode => (mode, new Token_Markup.Marker(mode, None))): _*) +
      ("bibtex" -> new JEdit_Bibtex.Token_Marker)

  def mode_token_marker(mode: String): Option[TokenMarker] = mode_markers.get(mode)

  def buffer_token_marker(buffer: Buffer): Option[TokenMarker] =
  {
    val mode = JEdit_Lib.buffer_mode(buffer)
    if (mode == "isabelle") Some(new Token_Markup.Marker(mode, Some(buffer)))
    else mode_token_marker(mode)
  }


  /* text structure */

  def indent_rule(mode: String): Option[IndentRule] =
    mode match {
      case "isabelle" | "isabelle-options" | "isabelle-root" =>
        Some(Text_Structure.Indent_Rule)
      case _ => None
    }

  def structure_matchers(mode: String): List[StructureMatcher] =
    if (mode == "isabelle") List(Text_Structure.Matcher) else Nil


  /* dockable windows */

  private def wm(view: View): DockableWindowManager = view.getDockableWindowManager

  def debugger_dockable(view: View): Option[Debugger_Dockable] =
    wm(view).getDockableWindow("isabelle-debugger") match {
      case dockable: Debugger_Dockable => Some(dockable)
      case _ => None
    }

  def documentation_dockable(view: View): Option[Documentation_Dockable] =
    wm(view).getDockableWindow("isabelle-documentation") match {
      case dockable: Documentation_Dockable => Some(dockable)
      case _ => None
    }

  def monitor_dockable(view: View): Option[Monitor_Dockable] =
    wm(view).getDockableWindow("isabelle-monitor") match {
      case dockable: Monitor_Dockable => Some(dockable)
      case _ => None
    }

  def output_dockable(view: View): Option[Output_Dockable] =
    wm(view).getDockableWindow("isabelle-output") match {
      case dockable: Output_Dockable => Some(dockable)
      case _ => None
    }

  def protocol_dockable(view: View): Option[Protocol_Dockable] =
    wm(view).getDockableWindow("isabelle-protocol") match {
      case dockable: Protocol_Dockable => Some(dockable)
      case _ => None
    }

  def query_dockable(view: View): Option[Query_Dockable] =
    wm(view).getDockableWindow("isabelle-query") match {
      case dockable: Query_Dockable => Some(dockable)
      case _ => None
    }

  def raw_output_dockable(view: View): Option[Raw_Output_Dockable] =
    wm(view).getDockableWindow("isabelle-raw-output") match {
      case dockable: Raw_Output_Dockable => Some(dockable)
      case _ => None
    }

  def simplifier_trace_dockable(view: View): Option[Simplifier_Trace_Dockable] =
    wm(view).getDockableWindow("isabelle-simplifier-trace") match {
      case dockable: Simplifier_Trace_Dockable => Some(dockable)
      case _ => None
    }

  def sledgehammer_dockable(view: View): Option[Sledgehammer_Dockable] =
    wm(view).getDockableWindow("isabelle-sledgehammer") match {
      case dockable: Sledgehammer_Dockable => Some(dockable)
      case _ => None
    }

  def state_dockable(view: View): Option[State_Dockable] =
    wm(view).getDockableWindow("isabelle-state") match {
      case dockable: State_Dockable => Some(dockable)
      case _ => None
    }

  def symbols_dockable(view: View): Option[Symbols_Dockable] =
    wm(view).getDockableWindow("isabelle-symbols") match {
      case dockable: Symbols_Dockable => Some(dockable)
      case _ => None
    }

  def syslog_dockable(view: View): Option[Syslog_Dockable] =
    wm(view).getDockableWindow("isabelle-syslog") match {
      case dockable: Syslog_Dockable => Some(dockable)
      case _ => None
    }

  def theories_dockable(view: View): Option[Theories_Dockable] =
    wm(view).getDockableWindow("isabelle-theories") match {
      case dockable: Theories_Dockable => Some(dockable)
      case _ => None
    }

  def timing_dockable(view: View): Option[Timing_Dockable] =
    wm(view).getDockableWindow("isabelle-timing") match {
      case dockable: Timing_Dockable => Some(dockable)
      case _ => None
    }


  /* continuous checking */

  private val CONTINUOUS_CHECKING = "editor_continuous_checking"

  def continuous_checking: Boolean = PIDE.options.bool(CONTINUOUS_CHECKING)
  def continuous_checking_=(b: Boolean): Unit =
    GUI_Thread.require {
      if (continuous_checking != b) {
        PIDE.options.bool(CONTINUOUS_CHECKING) = b
        PIDE.session.update_options(PIDE.options.value)
      }
    }

  def set_continuous_checking() { continuous_checking = true }
  def reset_continuous_checking() { continuous_checking = false }
  def toggle_continuous_checking() { continuous_checking = !continuous_checking }

  class Continuous_Checking extends CheckBox("Continuous checking")
  {
    tooltip = "Continuous checking of proof document (visible and required parts)"
    reactions += { case ButtonClicked(_) => continuous_checking = selected }
    def load() { selected = continuous_checking }
    load()
  }


  /* update state */

  def update_state(view: View): Unit =
    state_dockable(view).foreach(_.update_request())


  /* ML statistics */

  class ML_Stats extends
    JEdit_Options.Check_Box("ML_statistics", "ML statistics", "Enable ML runtime system statistics")


  /* required document nodes */

  def set_node_required(view: View) { Document_Model.view_node_required(view, set = true) }
  def reset_node_required(view: View) { Document_Model.view_node_required(view, set = false) }
  def toggle_node_required(view: View) { Document_Model.view_node_required(view, toggle = true) }


  /* font size */

  def reset_font_size() {
    Font_Info.main_change.reset(PIDE.options.int("jedit_reset_font_size").toFloat)
  }
  def increase_font_size() { Font_Info.main_change.step(1) }
  def decrease_font_size() { Font_Info.main_change.step(-1) }


  /* structured edits */

  def indent_enabled(buffer: JEditBuffer, option: String): Boolean =
    indent_rule(JEdit_Lib.buffer_mode(buffer)).isDefined &&
    buffer.getStringProperty("autoIndent") == "full" &&
    PIDE.options.bool(option)

  def indent_input(text_area: TextArea)
  {
    val buffer = text_area.getBuffer
    val line = text_area.getCaretLine
    val caret = text_area.getCaretPosition

    if (text_area.isEditable && indent_enabled(buffer, "jedit_indent_input")) {
      buffer_syntax(buffer) match {
        case Some(syntax) =>
          val nav = new Text_Structure.Navigator(syntax, buffer, true)
          nav.iterator(line, 1).toStream.headOption match {
            case Some(Text.Info(range, tok))
            if range.stop == caret && syntax.keywords.is_indent_command(tok) =>
              buffer.indentLine(line, true)
            case _ =>
          }
        case None =>
      }
    }
  }

  def newline(text_area: TextArea)
  {
    if (!text_area.isEditable()) text_area.getToolkit().beep()
    else {
      val buffer = text_area.getBuffer
      val line = text_area.getCaretLine
      val caret = text_area.getCaretPosition

      def nl { text_area.userInput('\n') }

      if (indent_enabled(buffer, "jedit_indent_newline")) {
        buffer_syntax(buffer) match {
          case Some(syntax) =>
            val keywords = syntax.keywords

            val (toks1, toks2) = Text_Structure.split_line_content(buffer, keywords, line, caret)

            if (toks1.isEmpty) buffer.removeTrailingWhiteSpace(Array(line))
            else if (keywords.is_indent_command(toks1.head)) buffer.indentLine(line, true)

            if (toks2.isEmpty || keywords.is_indent_command(toks2.head)) {
              text_area.setSelectedText("\n")
              if (!buffer.indentLine(line + 1, true)) text_area.goToStartOfWhiteSpace(false)
            }
            else nl
          case None => nl
        }
      }
      else nl
    }
  }

  def insert_line_padding(text_area: JEditTextArea, text: String)
  {
    val buffer = text_area.getBuffer
    JEdit_Lib.buffer_edit(buffer) {
      val text1 =
        if (text_area.getSelectionCount == 0) {
          def pad(range: Text.Range): String =
            if (JEdit_Lib.get_text(buffer, range) == Some("\n")) "" else "\n"

          val caret = JEdit_Lib.caret_range(text_area)
          val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1)
          pad(before_caret) + text + pad(caret)
        }
        else text
      text_area.setSelectedText(text1)
    }
  }

  def edit_command(
    snapshot: Document.Snapshot,
    text_area: TextArea,
    padding: Boolean,
    id: Document_ID.Generic,
    text: String)
  {
    val buffer = text_area.getBuffer
    if (!snapshot.is_outdated && text != "") {
      (snapshot.find_command(id), Document_Model.get(buffer)) match {
        case (Some((node, command)), Some(model)) if command.node_name == model.node_name =>
          node.command_start(command) match {
            case Some(start) =>
              JEdit_Lib.buffer_edit(buffer) {
                val range = command.core_range + start
                JEdit_Lib.buffer_edit(buffer) {
                  if (padding) {
                    text_area.moveCaretPosition(start + range.length)
                    val start_line = text_area.getCaretLine + 1
                    text_area.setSelectedText("\n" + text)
                    val end_line = text_area.getCaretLine
                    buffer.indentLines(start_line, end_line)
                  }
                  else {
                    buffer.remove(start, range.length)
                    text_area.moveCaretPosition(start)
                    text_area.setSelectedText(text)
                  }
                }
              }
            case None =>
          }
        case _ =>
      }
    }
  }


  /* selection */

  def select_entity(text_area: JEditTextArea)
  {
    for (doc_view <- Document_View.get(text_area)) {
      val rendering = doc_view.get_rendering()
      val caret_range = JEdit_Lib.caret_range(text_area)
      val buffer_range = JEdit_Lib.buffer_range(text_area.getBuffer)
      val active_focus = rendering.caret_focus_ranges(caret_range, buffer_range)
      if (active_focus.nonEmpty) {
        text_area.selectNone()
        for (r <- active_focus)
          text_area.addToSelection(new Selection.Range(r.start, r.stop))
      }
    }
  }


  /* completion */

  def complete(view: View, word_only: Boolean)
  {
    Completion_Popup.Text_Area.action(view.getTextArea, word_only)
  }


  /* control styles */

  def control_sub(text_area: JEditTextArea)
  { Syntax_Style.edit_control_style(text_area, Symbol.sub) }

  def control_sup(text_area: JEditTextArea)
  { Syntax_Style.edit_control_style(text_area, Symbol.sup) }

  def control_bold(text_area: JEditTextArea)
  { Syntax_Style.edit_control_style(text_area, Symbol.bold) }

  def control_emph(text_area: JEditTextArea)
  { Syntax_Style.edit_control_style(text_area, Symbol.emph) }

  def control_reset(text_area: JEditTextArea)
  { Syntax_Style.edit_control_style(text_area, "") }


  /* block styles */

  private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
  {
    s1.foreach(text_area.userInput(_))
    s2.foreach(text_area.userInput(_))
    s2.foreach(_ => text_area.goToPrevCharacter(false))
  }

  def input_bsub(text_area: JEditTextArea)
  { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) }

  def input_bsup(text_area: JEditTextArea)
  { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }


  /* antiquoted cartouche */

  def antiquoted_cartouche(text_area: TextArea)
  {
    val buffer = text_area.getBuffer
    for {
      doc_view <- Document_View.get(text_area)
      rendering = doc_view.get_rendering()
      caret_range = JEdit_Lib.caret_range(text_area)
      antiq_range <- rendering.antiquoted(caret_range)
      antiq_text <- JEdit_Lib.get_text(buffer, antiq_range)
      body_text <- Antiquote.read_antiq_body(antiq_text)
      (name, arg) <- Token.read_antiq_arg(Keyword.Keywords.empty, body_text)
      if Symbol.is_ascii_identifier(name)
    } {
      val op_text =
        Isabelle_Encoding.perhaps_decode(buffer,
          Symbol.control_prefix + name + Symbol.control_suffix)
      val arg_text =
        if (arg.isEmpty) ""
        else if (Isabelle_Encoding.is_active(buffer)) Symbol.cartouche_decoded(arg.get)
        else Symbol.cartouche(arg.get)

      buffer.remove(antiq_range.start, antiq_range.length)
      text_area.moveCaretPosition(antiq_range.start)
      text_area.selectNone
      text_area.setSelectedText(op_text + arg_text)
    }
  }


  /* spell-checker dictionary */

  def update_dictionary(text_area: JEditTextArea, include: Boolean, permanent: Boolean)
  {
    for {
      spell_checker <- PIDE.plugin.spell_checker.get
      doc_view <- Document_View.get(text_area)
      rendering = doc_view.get_rendering()
      range = JEdit_Lib.caret_range(text_area)
      Text.Info(_, word) <- Spell_Checker.current_word(rendering, range)
    } {
      spell_checker.update(word, include, permanent)
      JEdit_Lib.jedit_views().foreach(_.repaint())
    }
  }

  def reset_dictionary()
  {
    for (spell_checker <- PIDE.plugin.spell_checker.get)
    {
      spell_checker.reset()
      JEdit_Lib.jedit_views().foreach(_.repaint())
    }
  }


  /* debugger */

  def toggle_breakpoint(text_area: JEditTextArea): Unit =
  {
    GUI_Thread.require {}

    if (PIDE.session.debugger.is_active()) {
      Debugger_Dockable.get_breakpoint(text_area, text_area.getCaretPosition) match {
        case Some((command, breakpoint)) =>
          PIDE.session.debugger.toggle_breakpoint(command, breakpoint)
          jEdit.propertiesChanged()
        case None =>
      }
    }
  }


  /* plugin options */

  def plugin_options(frame: Frame)
  {
    GUI_Thread.require {}
    jEdit.setProperty("Plugin Options.last", "isabelle-general")
    new CombinedOptions(frame, 1)
  }


  /* popups */

  def dismissed_popups(view: View): Boolean =
  {
    var dismissed = false

    JEdit_Lib.jedit_text_areas(view).foreach(text_area =>
      if (Completion_Popup.Text_Area.dismissed(text_area)) dismissed = true)

    if (Pretty_Tooltip.dismissed_all()) dismissed = true

    dismissed
  }


  /* tooltips */

  def show_tooltip(view: View, control: Boolean)
  {
    GUI_Thread.require {}

    val text_area = view.getTextArea
    val painter = text_area.getPainter
    val caret_range = JEdit_Lib.caret_range(text_area)
    for {
      doc_view <- Document_View.get(text_area)
      rendering = doc_view.get_rendering()
      tip <- rendering.tooltip(caret_range, control)
      loc0 <- Option(text_area.offsetToXY(caret_range.start))
    } {
      val loc = new Point(loc0.x, loc0.y + painter.getLineHeight / 2)
      val results = rendering.snapshot.command_results(tip.range)
      Pretty_Tooltip(view, painter, loc, rendering, results, tip)
    }
  }


  /* error navigation */

  private def goto_error(
    view: View, range: Text.Range, which: String = "")(get: List[Text.Markup] => Option[Text.Markup])
  {
    GUI_Thread.require {}

    val text_area = view.getTextArea
    for (doc_view <- Document_View.get(text_area)) {
      val rendering = doc_view.get_rendering()
      get(rendering.errors(range)) match {
        case Some(err) =>
          PIDE.editor.goto_buffer(false, view, view.getBuffer, err.range.start)
        case None =>
          view.getStatus.setMessageAndClear("No " + which + "error in current document snapshot")
      }
    }
  }

  def goto_first_error(view: View): Unit =
    goto_error(view, JEdit_Lib.buffer_range(view.getBuffer))(_.headOption)

  def goto_last_error(view: View): Unit =
    goto_error(view, JEdit_Lib.buffer_range(view.getBuffer))(_.lastOption)

  def goto_prev_error(view: View): Unit =
    goto_error(view, JEdit_Lib.buffer_range_to_caret(view.getTextArea), which = "previous ")(
      list =>
        list.reverse match {
          case _ :: err :: _ => Some(err)
          case _ => None
        })

  def goto_next_error(view: View): Unit =
    goto_error(view, JEdit_Lib.buffer_range_from_caret(view.getTextArea), which = "next ")(
      {
        case _ :: err :: _ => Some(err)
        case _ => None
      })
}