src/Tools/jEdit/src/isabelle.scala
author wenzelm
Sat Mar 01 16:34:30 2014 +0100 (2014-03-01)
changeset 55823 0331b6d2ab0c
parent 55749 75a48dc4383e
child 55824 22bc50a19afa
permissions -rw-r--r--
font size change with delay, to avoid GUI lagging behind user input;
     1 /*  Title:      Tools/jEdit/src/isabelle.scala
     2     Author:     Makarius
     3 
     4 Global configuration and convenience operations for Isabelle/jEdit.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import scala.swing.CheckBox
    13 import scala.swing.event.ButtonClicked
    14 
    15 import org.gjt.sp.jedit.{jEdit, View, Buffer}
    16 import org.gjt.sp.jedit.textarea.JEditTextArea
    17 import org.gjt.sp.jedit.gui.{DockableWindowManager, CompleteWord}
    18 
    19 
    20 object Isabelle
    21 {
    22   /* editor modes */
    23 
    24   val modes =
    25     List(
    26       "isabelle",         // theory source
    27       "isabelle-ml",      // ML source
    28       "isabelle-markup",  // SideKick markup tree
    29       "isabelle-news",    // NEWS
    30       "isabelle-options", // etc/options
    31       "isabelle-output",  // pretty text area output
    32       "isabelle-root")    // session ROOT
    33 
    34   private lazy val ml_syntax: Outer_Syntax =
    35     Outer_Syntax.init().no_tokens.
    36       set_language_context(Completion.Language_Context.ML_outer)
    37 
    38   private lazy val news_syntax: Outer_Syntax =
    39     Outer_Syntax.init().no_tokens
    40 
    41   def mode_syntax(name: String): Option[Outer_Syntax] =
    42     name match {
    43       case "isabelle" | "isabelle-markup" =>
    44         val syntax = PIDE.session.recent_syntax
    45         if (syntax == Outer_Syntax.empty) None else Some(syntax)
    46       case "isabelle-options" => Some(Options.options_syntax)
    47       case "isabelle-root" => Some(Build.root_syntax)
    48       case "isabelle-ml" => Some(ml_syntax)
    49       case "isabelle-news" => Some(news_syntax)
    50       case "isabelle-output" => None
    51       case _ => None
    52     }
    53 
    54 
    55   /* token markers */
    56 
    57   private val markers =
    58     Map(modes.map(name => (name, new Token_Markup.Marker(name))): _*)
    59 
    60   def token_marker(name: String): Option[Token_Markup.Marker] = markers.get(name)
    61 
    62 
    63   /* dockable windows */
    64 
    65   private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
    66 
    67   def documentation_dockable(view: View): Option[Documentation_Dockable] =
    68     wm(view).getDockableWindow("isabelle-documentation") match {
    69       case dockable: Documentation_Dockable => Some(dockable)
    70       case _ => None
    71     }
    72 
    73   def find_dockable(view: View): Option[Find_Dockable] =
    74     wm(view).getDockableWindow("isabelle-find") match {
    75       case dockable: Find_Dockable => Some(dockable)
    76       case _ => None
    77     }
    78 
    79   def monitor_dockable(view: View): Option[Monitor_Dockable] =
    80     wm(view).getDockableWindow("isabelle-monitor") match {
    81       case dockable: Monitor_Dockable => Some(dockable)
    82       case _ => None
    83     }
    84 
    85   def output_dockable(view: View): Option[Output_Dockable] =
    86     wm(view).getDockableWindow("isabelle-output") match {
    87       case dockable: Output_Dockable => Some(dockable)
    88       case _ => None
    89     }
    90 
    91   def protocol_dockable(view: View): Option[Protocol_Dockable] =
    92     wm(view).getDockableWindow("isabelle-protocol") match {
    93       case dockable: Protocol_Dockable => Some(dockable)
    94       case _ => None
    95     }
    96 
    97   def raw_output_dockable(view: View): Option[Raw_Output_Dockable] =
    98     wm(view).getDockableWindow("isabelle-raw-output") match {
    99       case dockable: Raw_Output_Dockable => Some(dockable)
   100       case _ => None
   101     }
   102 
   103   def simplifier_trace_dockable(view: View): Option[Simplifier_Trace_Dockable] =
   104     wm(view).getDockableWindow("isabelle-simplifier-trace") match {
   105       case dockable: Simplifier_Trace_Dockable => Some(dockable)
   106       case _ => None
   107     }
   108 
   109   def sledgehammer_dockable(view: View): Option[Sledgehammer_Dockable] =
   110     wm(view).getDockableWindow("isabelle-sledgehammer") match {
   111       case dockable: Sledgehammer_Dockable => Some(dockable)
   112       case _ => None
   113     }
   114 
   115   def symbols_dockable(view: View): Option[Symbols_Dockable] =
   116     wm(view).getDockableWindow("isabelle-symbols") match {
   117       case dockable: Symbols_Dockable => Some(dockable)
   118       case _ => None
   119     }
   120 
   121   def syslog_dockable(view: View): Option[Syslog_Dockable] =
   122     wm(view).getDockableWindow("isabelle-syslog") match {
   123       case dockable: Syslog_Dockable => Some(dockable)
   124       case _ => None
   125     }
   126 
   127   def theories_dockable(view: View): Option[Theories_Dockable] =
   128     wm(view).getDockableWindow("isabelle-theories") match {
   129       case dockable: Theories_Dockable => Some(dockable)
   130       case _ => None
   131     }
   132 
   133   def timing_dockable(view: View): Option[Timing_Dockable] =
   134     wm(view).getDockableWindow("isabelle-timing") match {
   135       case dockable: Timing_Dockable => Some(dockable)
   136       case _ => None
   137     }
   138 
   139 
   140   /* continuous checking */
   141 
   142   private val CONTINUOUS_CHECKING = "editor_continuous_checking"
   143 
   144   def continuous_checking: Boolean = PIDE.options.bool(CONTINUOUS_CHECKING)
   145 
   146   def continuous_checking_=(b: Boolean)
   147   {
   148     Swing_Thread.require()
   149 
   150     if (continuous_checking != b) {
   151       PIDE.options.bool(CONTINUOUS_CHECKING) = b
   152       PIDE.options_changed()
   153       PIDE.editor.flush()
   154     }
   155   }
   156 
   157   def set_continuous_checking() { continuous_checking = true }
   158   def reset_continuous_checking() { continuous_checking = false }
   159   def toggle_continuous_checking() { continuous_checking = !continuous_checking }
   160 
   161   class Continuous_Checking extends CheckBox("Continuous checking")
   162   {
   163     tooltip = "Continuous checking of proof document (visible and required parts)"
   164     reactions += { case ButtonClicked(_) => continuous_checking = selected }
   165     def load() { selected = continuous_checking }
   166     load()
   167   }
   168 
   169 
   170   /* required document nodes */
   171 
   172   private def node_required_update(view: View, toggle: Boolean = false, set: Boolean = false)
   173   {
   174     Swing_Thread.require()
   175     PIDE.document_model(view.getBuffer) match {
   176       case Some(model) =>
   177         model.node_required = (if (toggle) !model.node_required else set)
   178       case None =>
   179     }
   180   }
   181 
   182   def set_node_required(view: View) { node_required_update(view, set = true) }
   183   def reset_node_required(view: View) { node_required_update(view, set = false) }
   184   def toggle_node_required(view: View) { node_required_update(view, toggle = true) }
   185 
   186 
   187   /* font size */
   188 
   189   private object font_size
   190   {
   191     // owned by Swing thread
   192     private var last_view: Option[View] = None
   193     private var steps = 0
   194     private val delay = Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
   195     {
   196       val view = last_view getOrElse jEdit.getActiveView()
   197       Rendering.font_size_change(view, i =>
   198         {
   199           var j = i
   200           while (steps != 0 && j > 0) {
   201             if (steps > 0)
   202               { j += (j / 10) max 1; steps -= 1 }
   203             else
   204               { j -= (j / 10) max 1; steps += 1 }
   205           }
   206           steps = 0
   207           j
   208         })
   209     }
   210     def step(view: View, i: Int) { last_view = Some(view); steps += i; delay.invoke() }
   211     def reset() { delay.revoke(); last_view = None; steps = 0 }
   212   }
   213 
   214   def reset_font_size(view: View): Unit =
   215   {
   216     font_size.reset()
   217     Rendering.font_size_change(view, _ => PIDE.options.int("jedit_reset_font_size"))
   218   }
   219 
   220   def increase_font_size(view: View): Unit = font_size.step(view, 1)
   221   def decrease_font_size(view: View): Unit = font_size.step(view, -1)
   222 
   223 
   224   /* structured edits */
   225 
   226   def insert_line_padding(text_area: JEditTextArea, text: String)
   227   {
   228     val buffer = text_area.getBuffer
   229     JEdit_Lib.buffer_edit(buffer) {
   230       val text1 =
   231         if (text_area.getSelectionCount == 0) {
   232           def pad(range: Text.Range): String =
   233             if (JEdit_Lib.try_get_text(buffer, range) == Some("\n")) "" else "\n"
   234 
   235           val caret = JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
   236           val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1)
   237           pad(before_caret) + text + pad(caret)
   238         }
   239         else text
   240       text_area.setSelectedText(text1)
   241     }
   242   }
   243 
   244   def edit_command(
   245     snapshot: Document.Snapshot,
   246     buffer: Buffer,
   247     padding: Boolean,
   248     id: Document_ID.Generic,
   249     s: String)
   250   {
   251     if (!snapshot.is_outdated) {
   252       snapshot.state.find_command(snapshot.version, id) match {
   253         case Some((node, command)) =>
   254           node.command_start(command) match {
   255             case Some(start) =>
   256               JEdit_Lib.buffer_edit(buffer) {
   257                 val range = command.proper_range + start
   258                 if (padding) {
   259                   buffer.insert(start + range.length, "\n" + s)
   260                 }
   261                 else {
   262                   buffer.remove(start, range.length)
   263                   buffer.insert(start, s)
   264                 }
   265               }
   266             case None =>
   267           }
   268         case None =>
   269       }
   270     }
   271   }
   272 
   273 
   274   /* completion */
   275 
   276   def complete(view: View)
   277   {
   278     Completion_Popup.Text_Area(view.getTextArea) match {
   279       case Some(text_area_completion) =>
   280         text_area_completion.action(immediate = true, explicit = true)
   281       case None => CompleteWord.completeWord(view)
   282     }
   283   }
   284 
   285 
   286   /* control styles */
   287 
   288   def control_sub(text_area: JEditTextArea)
   289   { Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) }
   290 
   291   def control_sup(text_area: JEditTextArea)
   292   { Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) }
   293 
   294   def control_bold(text_area: JEditTextArea)
   295   { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) }
   296 
   297   def control_reset(text_area: JEditTextArea)
   298   { Token_Markup.edit_control_style(text_area, "") }
   299 
   300 
   301   /* block styles */
   302 
   303   private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
   304   {
   305     s1.foreach(text_area.userInput(_))
   306     s2.foreach(text_area.userInput(_))
   307     s2.foreach(_ => text_area.goToPrevCharacter(false))
   308   }
   309 
   310   def input_bsub(text_area: JEditTextArea)
   311   { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) }
   312 
   313   def input_bsup(text_area: JEditTextArea)
   314   { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
   315 }
   316