src/Tools/jEdit/src/isabelle.scala
author wenzelm
Mon, 06 Jun 2016 16:04:26 +0200
changeset 63236 48bc9045866e
parent 62631 c39614ddb80b
child 63421 3bf02e7fa8a3
permissions -rw-r--r--
added action "isabelle.select-entity";
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
     1
/*  Title:      Tools/jEdit/src/isabelle.scala
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
     3
53277
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
     4
Global configuration and convenience operations for Isabelle/jEdit.
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
     5
*/
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
     6
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
     8
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
     9
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
    10
import isabelle._
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
    11
57627
65fc7ae1bf66 added action "isabelle.options" (despite problems with initial window size);
wenzelm
parents: 57612
diff changeset
    12
import java.awt.Frame
65fc7ae1bf66 added action "isabelle.options" (despite problems with initial window size);
wenzelm
parents: 57612
diff changeset
    13
53715
68c664737d04 added option "jedit_auto_load";
wenzelm
parents: 53497
diff changeset
    14
import scala.swing.CheckBox
68c664737d04 added option "jedit_auto_load";
wenzelm
parents: 53497
diff changeset
    15
import scala.swing.event.ButtonClicked
68c664737d04 added option "jedit_auto_load";
wenzelm
parents: 53497
diff changeset
    16
50198
0c7b351a6871 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents: 50187
diff changeset
    17
import org.gjt.sp.jedit.{jEdit, View, Buffer}
59074
7836d927ffca tuned signature;
wenzelm
parents: 58804
diff changeset
    18
import org.gjt.sp.jedit.buffer.JEditBuffer
63236
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
    19
import org.gjt.sp.jedit.textarea.{JEditTextArea, StructureMatcher, Selection}
58529
cd4439d8799c support for bibtex token markup;
wenzelm
parents: 57861
diff changeset
    20
import org.gjt.sp.jedit.syntax.TokenMarker
53293
fd27b8f5a479 added action isabelle.complete, using standard jEdit keyboard shortcut;
wenzelm
parents: 53281
diff changeset
    21
import org.gjt.sp.jedit.gui.{DockableWindowManager, CompleteWord}
61024
7b7f01afab71 avoid deprecated PluginOptions with its unbounded window size;
wenzelm
parents: 60890
diff changeset
    22
import org.jedit.options.CombinedOptions
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
    23
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
    24
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    25
object Isabelle
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
    26
{
53274
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    27
  /* editor modes */
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    28
53277
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    29
  val modes =
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    30
    List(
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    31
      "isabelle",         // theory source
55500
cdbbaa3074a8 isabelle-ml mode with separate token marker;
wenzelm
parents: 55316
diff changeset
    32
      "isabelle-ml",      // ML source
53277
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    33
      "isabelle-news",    // NEWS
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    34
      "isabelle-options", // etc/options
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    35
      "isabelle-output",  // pretty text area output
56277
c4f75e733812 separate "sml" mode, suppress old "ml" mode altogether;
wenzelm
parents: 56170
diff changeset
    36
      "isabelle-root",    // session ROOT
c4f75e733812 separate "sml" mode, suppress old "ml" mode altogether;
wenzelm
parents: 56170
diff changeset
    37
      "sml")              // Standard ML (not Isabelle/ML)
53274
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    38
55616
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55558
diff changeset
    39
  private lazy val ml_syntax: Outer_Syntax =
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55558
diff changeset
    40
    Outer_Syntax.init().no_tokens.
55749
75a48dc4383e tuned signature;
wenzelm
parents: 55666
diff changeset
    41
      set_language_context(Completion.Language_Context.ML_outer)
55616
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55558
diff changeset
    42
56278
2576d3a40ed6 separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents: 56277
diff changeset
    43
  private lazy val sml_syntax: Outer_Syntax =
2576d3a40ed6 separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents: 56277
diff changeset
    44
    Outer_Syntax.init().no_tokens.
2576d3a40ed6 separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents: 56277
diff changeset
    45
      set_language_context(Completion.Language_Context.SML_outer)
2576d3a40ed6 separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents: 56277
diff changeset
    46
55616
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55558
diff changeset
    47
  private lazy val news_syntax: Outer_Syntax =
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55558
diff changeset
    48
    Outer_Syntax.init().no_tokens
53276
cbed0aa0b0db syntax for isabelle-news with symbol completion;
wenzelm
parents: 53274
diff changeset
    49
59076
65babcd8b0e6 clarified token marker / syntax for mode vs. buffer;
wenzelm
parents: 59075
diff changeset
    50
  def mode_syntax(mode: String): Option[Outer_Syntax] =
65babcd8b0e6 clarified token marker / syntax for mode vs. buffer;
wenzelm
parents: 59075
diff changeset
    51
    mode match {
59077
7e0d3da6e6d8 node-specific syntax, with base_syntax as default;
wenzelm
parents: 59076
diff changeset
    52
      case "isabelle" => Some(PIDE.resources.base_syntax.asInstanceOf[Outer_Syntax])
53274
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    53
      case "isabelle-options" => Some(Options.options_syntax)
62631
c39614ddb80b clarified modules;
wenzelm
parents: 62104
diff changeset
    54
      case "isabelle-root" => Some(Sessions.root_syntax)
55616
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55558
diff changeset
    55
      case "isabelle-ml" => Some(ml_syntax)
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55558
diff changeset
    56
      case "isabelle-news" => Some(news_syntax)
53277
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    57
      case "isabelle-output" => None
56278
2576d3a40ed6 separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents: 56277
diff changeset
    58
      case "sml" => Some(sml_syntax)
53274
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    59
      case _ => None
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    60
    }
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    61
59074
7836d927ffca tuned signature;
wenzelm
parents: 58804
diff changeset
    62
  def buffer_syntax(buffer: JEditBuffer): Option[Outer_Syntax] =
59077
7e0d3da6e6d8 node-specific syntax, with base_syntax as default;
wenzelm
parents: 59076
diff changeset
    63
    (JEdit_Lib.buffer_mode(buffer), PIDE.document_model(buffer)) match {
7e0d3da6e6d8 node-specific syntax, with base_syntax as default;
wenzelm
parents: 59076
diff changeset
    64
      case ("isabelle", Some(model)) =>
7e0d3da6e6d8 node-specific syntax, with base_syntax as default;
wenzelm
parents: 59076
diff changeset
    65
        Some(PIDE.session.recent_syntax(model.node_name).asInstanceOf[Outer_Syntax])
7e0d3da6e6d8 node-specific syntax, with base_syntax as default;
wenzelm
parents: 59076
diff changeset
    66
      case (mode, _) => mode_syntax(mode)
59076
65babcd8b0e6 clarified token marker / syntax for mode vs. buffer;
wenzelm
parents: 59075
diff changeset
    67
    }
59074
7836d927ffca tuned signature;
wenzelm
parents: 58804
diff changeset
    68
53274
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    69
53277
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    70
  /* token markers */
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    71
59076
65babcd8b0e6 clarified token marker / syntax for mode vs. buffer;
wenzelm
parents: 59075
diff changeset
    72
  private val mode_markers: Map[String, TokenMarker] =
65babcd8b0e6 clarified token marker / syntax for mode vs. buffer;
wenzelm
parents: 59075
diff changeset
    73
    Map(modes.map(mode => (mode, new Token_Markup.Marker(mode, None))): _*) +
58546
72e2b2a609c4 clarified modules;
wenzelm
parents: 58543
diff changeset
    74
      ("bibtex" -> new Bibtex_JEdit.Token_Marker)
53277
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    75
59076
65babcd8b0e6 clarified token marker / syntax for mode vs. buffer;
wenzelm
parents: 59075
diff changeset
    76
  def mode_token_marker(mode: String): Option[TokenMarker] = mode_markers.get(mode)
65babcd8b0e6 clarified token marker / syntax for mode vs. buffer;
wenzelm
parents: 59075
diff changeset
    77
65babcd8b0e6 clarified token marker / syntax for mode vs. buffer;
wenzelm
parents: 59075
diff changeset
    78
  def buffer_token_marker(buffer: Buffer): Option[TokenMarker] =
65babcd8b0e6 clarified token marker / syntax for mode vs. buffer;
wenzelm
parents: 59075
diff changeset
    79
  {
65babcd8b0e6 clarified token marker / syntax for mode vs. buffer;
wenzelm
parents: 59075
diff changeset
    80
    val mode = JEdit_Lib.buffer_mode(buffer)
60274
c2837a39da01 more conservative Document_Model.init: avoid Document.Node.Clear due to change of token marker (e.g. due to change of jEdit mode properties);
wenzelm
parents: 60074
diff changeset
    81
    if (mode == "isabelle") Some(new Token_Markup.Marker(mode, Some(buffer)))
c2837a39da01 more conservative Document_Model.init: avoid Document.Node.Clear due to change of token marker (e.g. due to change of jEdit mode properties);
wenzelm
parents: 60074
diff changeset
    82
    else mode_token_marker(mode)
59076
65babcd8b0e6 clarified token marker / syntax for mode vs. buffer;
wenzelm
parents: 59075
diff changeset
    83
  }
53277
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    84
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    85
58748
8f92f17d8781 support for structure matching;
wenzelm
parents: 58546
diff changeset
    86
  /* structure matchers */
8f92f17d8781 support for structure matching;
wenzelm
parents: 58546
diff changeset
    87
8f92f17d8781 support for structure matching;
wenzelm
parents: 58546
diff changeset
    88
  def structure_matchers(name: String): List[StructureMatcher] =
8f92f17d8781 support for structure matching;
wenzelm
parents: 58546
diff changeset
    89
    if (name == "isabelle") List(Structure_Matching.Isabelle_Matcher) else Nil
8f92f17d8781 support for structure matching;
wenzelm
parents: 58546
diff changeset
    90
8f92f17d8781 support for structure matching;
wenzelm
parents: 58546
diff changeset
    91
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    92
  /* dockable windows */
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    93
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    94
  private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    95
60749
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents: 60274
diff changeset
    96
  def debugger_dockable(view: View): Option[Debugger_Dockable] =
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents: 60274
diff changeset
    97
    wm(view).getDockableWindow("isabelle-debugger") match {
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents: 60274
diff changeset
    98
      case dockable: Debugger_Dockable => Some(dockable)
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents: 60274
diff changeset
    99
      case _ => None
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents: 60274
diff changeset
   100
    }
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents: 60274
diff changeset
   101
55558
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   102
  def documentation_dockable(view: View): Option[Documentation_Dockable] =
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   103
    wm(view).getDockableWindow("isabelle-documentation") match {
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   104
      case dockable: Documentation_Dockable => Some(dockable)
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   105
      case _ => None
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   106
    }
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   107
55558
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   108
  def monitor_dockable(view: View): Option[Monitor_Dockable] =
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   109
    wm(view).getDockableWindow("isabelle-monitor") match {
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   110
      case dockable: Monitor_Dockable => Some(dockable)
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   111
      case _ => None
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   112
    }
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   113
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   114
  def output_dockable(view: View): Option[Output_Dockable] =
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   115
    wm(view).getDockableWindow("isabelle-output") match {
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   116
      case dockable: Output_Dockable => Some(dockable)
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   117
      case _ => None
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   118
    }
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   119
55558
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   120
  def protocol_dockable(view: View): Option[Protocol_Dockable] =
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   121
    wm(view).getDockableWindow("isabelle-protocol") match {
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   122
      case dockable: Protocol_Dockable => Some(dockable)
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   123
      case _ => None
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   124
    }
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   125
56879
ee2b61f37ad9 renamed "Find" to "Query", with more general operations;
wenzelm
parents: 56662
diff changeset
   126
  def query_dockable(view: View): Option[Query_Dockable] =
ee2b61f37ad9 renamed "Find" to "Query", with more general operations;
wenzelm
parents: 56662
diff changeset
   127
    wm(view).getDockableWindow("isabelle-query") match {
ee2b61f37ad9 renamed "Find" to "Query", with more general operations;
wenzelm
parents: 56662
diff changeset
   128
      case dockable: Query_Dockable => Some(dockable)
ee2b61f37ad9 renamed "Find" to "Query", with more general operations;
wenzelm
parents: 56662
diff changeset
   129
      case _ => None
ee2b61f37ad9 renamed "Find" to "Query", with more general operations;
wenzelm
parents: 56662
diff changeset
   130
    }
ee2b61f37ad9 renamed "Find" to "Query", with more general operations;
wenzelm
parents: 56662
diff changeset
   131
55558
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   132
  def raw_output_dockable(view: View): Option[Raw_Output_Dockable] =
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   133
    wm(view).getDockableWindow("isabelle-raw-output") match {
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   134
      case dockable: Raw_Output_Dockable => Some(dockable)
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   135
      case _ => None
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   136
    }
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   137
55558
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   138
  def simplifier_trace_dockable(view: View): Option[Simplifier_Trace_Dockable] =
55557
aa1adeca714b standardized action and panel names;
wenzelm
parents: 55500
diff changeset
   139
    wm(view).getDockableWindow("isabelle-simplifier-trace") match {
55316
885500f4aa6a interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents: 54640
diff changeset
   140
      case dockable: Simplifier_Trace_Dockable => Some(dockable)
885500f4aa6a interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents: 54640
diff changeset
   141
      case _ => None
885500f4aa6a interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents: 54640
diff changeset
   142
    }
885500f4aa6a interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents: 54640
diff changeset
   143
55558
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   144
  def sledgehammer_dockable(view: View): Option[Sledgehammer_Dockable] =
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   145
    wm(view).getDockableWindow("isabelle-sledgehammer") match {
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   146
      case dockable: Sledgehammer_Dockable => Some(dockable)
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   147
      case _ => None
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   148
    }
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   149
61208
19118f9b939d separate panel for proof state output;
wenzelm
parents: 61024
diff changeset
   150
  def state_dockable(view: View): Option[State_Dockable] =
19118f9b939d separate panel for proof state output;
wenzelm
parents: 61024
diff changeset
   151
    wm(view).getDockableWindow("isabelle-state") match {
19118f9b939d separate panel for proof state output;
wenzelm
parents: 61024
diff changeset
   152
      case dockable: State_Dockable => Some(dockable)
19118f9b939d separate panel for proof state output;
wenzelm
parents: 61024
diff changeset
   153
      case _ => None
19118f9b939d separate panel for proof state output;
wenzelm
parents: 61024
diff changeset
   154
    }
19118f9b939d separate panel for proof state output;
wenzelm
parents: 61024
diff changeset
   155
55558
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   156
  def symbols_dockable(view: View): Option[Symbols_Dockable] =
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   157
    wm(view).getDockableWindow("isabelle-symbols") match {
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   158
      case dockable: Symbols_Dockable => Some(dockable)
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   159
      case _ => None
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   160
    }
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   161
55558
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   162
  def syslog_dockable(view: View): Option[Syslog_Dockable] =
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   163
    wm(view).getDockableWindow("isabelle-syslog") match {
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   164
      case dockable: Syslog_Dockable => Some(dockable)
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   165
      case _ => None
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   166
    }
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   167
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   168
  def theories_dockable(view: View): Option[Theories_Dockable] =
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   169
    wm(view).getDockableWindow("isabelle-theories") match {
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   170
      case dockable: Theories_Dockable => Some(dockable)
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   171
      case _ => None
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   172
    }
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   173
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   174
  def timing_dockable(view: View): Option[Timing_Dockable] =
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   175
    wm(view).getDockableWindow("isabelle-timing") match {
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   176
      case dockable: Timing_Dockable => Some(dockable)
50433
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents: 50341
diff changeset
   177
      case _ => None
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents: 50341
diff changeset
   178
    }
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents: 50341
diff changeset
   179
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   180
52815
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   181
  /* continuous checking */
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   182
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   183
  private val CONTINUOUS_CHECKING = "editor_continuous_checking"
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   184
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   185
  def continuous_checking: Boolean = PIDE.options.bool(CONTINUOUS_CHECKING)
60074
38a64cc17403 GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents: 59077
diff changeset
   186
  def continuous_checking_=(b: Boolean): Unit =
38a64cc17403 GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents: 59077
diff changeset
   187
    GUI_Thread.require {
38a64cc17403 GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents: 59077
diff changeset
   188
      if (continuous_checking != b) {
38a64cc17403 GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents: 59077
diff changeset
   189
        PIDE.options.bool(CONTINUOUS_CHECKING) = b
61725
1529c3eb6bac more thorough update of options;
wenzelm
parents: 61483
diff changeset
   190
        PIDE.session.update_options(PIDE.options.value)
60074
38a64cc17403 GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents: 59077
diff changeset
   191
      }
52815
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   192
    }
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   193
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   194
  def set_continuous_checking() { continuous_checking = true }
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   195
  def reset_continuous_checking() { continuous_checking = false }
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   196
  def toggle_continuous_checking() { continuous_checking = !continuous_checking }
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   197
53715
68c664737d04 added option "jedit_auto_load";
wenzelm
parents: 53497
diff changeset
   198
  class Continuous_Checking extends CheckBox("Continuous checking")
68c664737d04 added option "jedit_auto_load";
wenzelm
parents: 53497
diff changeset
   199
  {
68c664737d04 added option "jedit_auto_load";
wenzelm
parents: 53497
diff changeset
   200
    tooltip = "Continuous checking of proof document (visible and required parts)"
68c664737d04 added option "jedit_auto_load";
wenzelm
parents: 53497
diff changeset
   201
    reactions += { case ButtonClicked(_) => continuous_checking = selected }
68c664737d04 added option "jedit_auto_load";
wenzelm
parents: 53497
diff changeset
   202
    def load() { selected = continuous_checking }
68c664737d04 added option "jedit_auto_load";
wenzelm
parents: 53497
diff changeset
   203
    load()
68c664737d04 added option "jedit_auto_load";
wenzelm
parents: 53497
diff changeset
   204
  }
68c664737d04 added option "jedit_auto_load";
wenzelm
parents: 53497
diff changeset
   205
52815
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   206
61211
8a5d5ca5d8bc added action "isabelle-update-state";
wenzelm
parents: 61208
diff changeset
   207
  /* update state */
8a5d5ca5d8bc added action "isabelle-update-state";
wenzelm
parents: 61208
diff changeset
   208
8a5d5ca5d8bc added action "isabelle-update-state";
wenzelm
parents: 61208
diff changeset
   209
  def update_state(view: View): Unit =
61802
1d81de0bddc4 more thorough update request: semantic state of command may have changed elsewise;
wenzelm
parents: 61725
diff changeset
   210
    state_dockable(view).foreach(_.update_request())
61211
8a5d5ca5d8bc added action "isabelle-update-state";
wenzelm
parents: 61208
diff changeset
   211
8a5d5ca5d8bc added action "isabelle-update-state";
wenzelm
parents: 61208
diff changeset
   212
60074
38a64cc17403 GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents: 59077
diff changeset
   213
  /* ML statistics */
38a64cc17403 GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents: 59077
diff changeset
   214
60843
9980f3bcdea2 tuned signature;
wenzelm
parents: 60749
diff changeset
   215
  class ML_Stats extends
9980f3bcdea2 tuned signature;
wenzelm
parents: 60749
diff changeset
   216
    JEdit_Options.Check_Box("ML_statistics", "ML statistics", "Enable ML runtime system statistics")
60074
38a64cc17403 GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents: 59077
diff changeset
   217
38a64cc17403 GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents: 59077
diff changeset
   218
52815
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   219
  /* required document nodes */
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   220
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   221
  private def node_required_update(view: View, toggle: Boolean = false, set: Boolean = false)
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   222
  {
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 57424
diff changeset
   223
    GUI_Thread.require {}
52815
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   224
    PIDE.document_model(view.getBuffer) match {
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   225
      case Some(model) =>
52816
c608e0ade554 home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents: 52815
diff changeset
   226
        model.node_required = (if (toggle) !model.node_required else set)
52815
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   227
      case None =>
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   228
    }
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   229
  }
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   230
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   231
  def set_node_required(view: View) { node_required_update(view, set = true) }
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   232
  def reset_node_required(view: View) { node_required_update(view, set = false) }
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   233
  def toggle_node_required(view: View) { node_required_update(view, toggle = true) }
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   234
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   235
50198
0c7b351a6871 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents: 50187
diff changeset
   236
  /* font size */
0c7b351a6871 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents: 50187
diff changeset
   237
55827
8a881f83e206 clarified module structure;
wenzelm
parents: 55825
diff changeset
   238
  def reset_font_size() {
8a881f83e206 clarified module structure;
wenzelm
parents: 55825
diff changeset
   239
    Font_Info.main_change.reset(PIDE.options.int("jedit_reset_font_size").toFloat)
55823
0331b6d2ab0c font size change with delay, to avoid GUI lagging behind user input;
wenzelm
parents: 55749
diff changeset
   240
  }
55827
8a881f83e206 clarified module structure;
wenzelm
parents: 55825
diff changeset
   241
  def increase_font_size() { Font_Info.main_change.step(1) }
8a881f83e206 clarified module structure;
wenzelm
parents: 55825
diff changeset
   242
  def decrease_font_size() { Font_Info.main_change.step(-1) }
50198
0c7b351a6871 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents: 50187
diff changeset
   243
0c7b351a6871 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents: 50187
diff changeset
   244
53497
07bb77881b8d tuned signature;
wenzelm
parents: 53322
diff changeset
   245
  /* structured edits */
50341
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   246
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   247
  def insert_line_padding(text_area: JEditTextArea, text: String)
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   248
  {
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   249
    val buffer = text_area.getBuffer
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   250
    JEdit_Lib.buffer_edit(buffer) {
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   251
      val text1 =
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   252
        if (text_area.getSelectionCount == 0) {
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   253
          def pad(range: Text.Range): String =
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   254
            if (JEdit_Lib.try_get_text(buffer, range) == Some("\n")) "" else "\n"
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   255
56592
5157f7615e99 prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents: 56587
diff changeset
   256
          val caret = JEdit_Lib.caret_range(text_area)
50341
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   257
          val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1)
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   258
          pad(before_caret) + text + pad(caret)
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   259
        }
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   260
        else text
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   261
      text_area.setSelectedText(text1)
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   262
    }
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   263
  }
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   264
53497
07bb77881b8d tuned signature;
wenzelm
parents: 53322
diff changeset
   265
  def edit_command(
07bb77881b8d tuned signature;
wenzelm
parents: 53322
diff changeset
   266
    snapshot: Document.Snapshot,
07bb77881b8d tuned signature;
wenzelm
parents: 53322
diff changeset
   267
    buffer: Buffer,
07bb77881b8d tuned signature;
wenzelm
parents: 53322
diff changeset
   268
    padding: Boolean,
54640
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   269
    id: Document_ID.Generic,
53497
07bb77881b8d tuned signature;
wenzelm
parents: 53322
diff changeset
   270
    s: String)
07bb77881b8d tuned signature;
wenzelm
parents: 53322
diff changeset
   271
  {
54640
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   272
    if (!snapshot.is_outdated) {
57861
287e3b1298b3 restrict edit_command (for sendback) to current node -- no attempt to goto target buffer first, which might not be loaded;
wenzelm
parents: 57627
diff changeset
   273
      (snapshot.state.find_command(snapshot.version, id), PIDE.document_model(buffer)) match {
287e3b1298b3 restrict edit_command (for sendback) to current node -- no attempt to goto target buffer first, which might not be loaded;
wenzelm
parents: 57627
diff changeset
   274
        case (Some((node, command)), Some(model)) if command.node_name == model.node_name =>
54640
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   275
          node.command_start(command) match {
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   276
            case Some(start) =>
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   277
              JEdit_Lib.buffer_edit(buffer) {
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   278
                val range = command.proper_range + start
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   279
                if (padding) {
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   280
                  buffer.insert(start + range.length, "\n" + s)
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   281
                }
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   282
                else {
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   283
                  buffer.remove(start, range.length)
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   284
                  buffer.insert(start, s)
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   285
                }
53497
07bb77881b8d tuned signature;
wenzelm
parents: 53322
diff changeset
   286
              }
54640
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   287
            case None =>
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   288
          }
57861
287e3b1298b3 restrict edit_command (for sendback) to current node -- no attempt to goto target buffer first, which might not be loaded;
wenzelm
parents: 57627
diff changeset
   289
        case _ =>
54640
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   290
      }
53497
07bb77881b8d tuned signature;
wenzelm
parents: 53322
diff changeset
   291
    }
07bb77881b8d tuned signature;
wenzelm
parents: 53322
diff changeset
   292
  }
07bb77881b8d tuned signature;
wenzelm
parents: 53322
diff changeset
   293
50341
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   294
63236
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
   295
  /* selection */
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
   296
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
   297
  def select_entity(text_area: JEditTextArea)
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
   298
  {
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
   299
    for {
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
   300
      doc_view <- PIDE.document_view(text_area)
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
   301
      rendering = doc_view.get_rendering()
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
   302
    } {
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
   303
      val caret_range = JEdit_Lib.caret_range(text_area)
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
   304
      val buffer_range = JEdit_Lib.buffer_range(text_area.getBuffer)
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
   305
      val active_focus = rendering.caret_focus_ranges(caret_range, buffer_range)
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
   306
      if (active_focus.nonEmpty) {
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
   307
        text_area.selectNone()
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
   308
        for (r <- active_focus)
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
   309
          text_area.addToSelection(new Selection.Range(r.start, r.stop))
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
   310
      }
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
   311
    }
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
   312
  }
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
   313
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
   314
53293
fd27b8f5a479 added action isabelle.complete, using standard jEdit keyboard shortcut;
wenzelm
parents: 53281
diff changeset
   315
  /* completion */
fd27b8f5a479 added action isabelle.complete, using standard jEdit keyboard shortcut;
wenzelm
parents: 53281
diff changeset
   316
56586
5ef60881681d explicit menu action to complete word;
wenzelm
parents: 56578
diff changeset
   317
  def complete(view: View, word_only: Boolean)
53293
fd27b8f5a479 added action isabelle.complete, using standard jEdit keyboard shortcut;
wenzelm
parents: 53281
diff changeset
   318
  {
57424
966b12f636b9 removed slightly odd fall-back on complete-word (NB: connection to default menu action is unclear);
wenzelm
parents: 56879
diff changeset
   319
    Completion_Popup.Text_Area.action(view.getTextArea, word_only)
53293
fd27b8f5a479 added action isabelle.complete, using standard jEdit keyboard shortcut;
wenzelm
parents: 53281
diff changeset
   320
  }
fd27b8f5a479 added action isabelle.complete, using standard jEdit keyboard shortcut;
wenzelm
parents: 53281
diff changeset
   321
fd27b8f5a479 added action isabelle.complete, using standard jEdit keyboard shortcut;
wenzelm
parents: 53281
diff changeset
   322
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   323
  /* control styles */
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   324
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   325
  def control_sub(text_area: JEditTextArea)
62104
fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding;
wenzelm
parents: 61802
diff changeset
   326
  { Token_Markup.edit_control_style(text_area, Symbol.sub) }
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   327
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   328
  def control_sup(text_area: JEditTextArea)
62104
fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding;
wenzelm
parents: 61802
diff changeset
   329
  { Token_Markup.edit_control_style(text_area, Symbol.sup) }
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   330
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   331
  def control_bold(text_area: JEditTextArea)
62104
fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding;
wenzelm
parents: 61802
diff changeset
   332
  { Token_Markup.edit_control_style(text_area, Symbol.bold) }
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   333
61483
07c8d5d8acab added action "isabelle-emph";
wenzelm
parents: 61211
diff changeset
   334
  def control_emph(text_area: JEditTextArea)
62104
fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding;
wenzelm
parents: 61802
diff changeset
   335
  { Token_Markup.edit_control_style(text_area, Symbol.emph) }
61483
07c8d5d8acab added action "isabelle-emph";
wenzelm
parents: 61211
diff changeset
   336
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   337
  def control_reset(text_area: JEditTextArea)
50187
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50183
diff changeset
   338
  { Token_Markup.edit_control_style(text_area, "") }
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   339
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   340
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   341
  /* block styles */
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   342
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   343
  private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   344
  {
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   345
    s1.foreach(text_area.userInput(_))
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   346
    s2.foreach(text_area.userInput(_))
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   347
    s2.foreach(_ => text_area.goToPrevCharacter(false))
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   348
  }
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   349
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   350
  def input_bsub(text_area: JEditTextArea)
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   351
  { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) }
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   352
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   353
  def input_bsup(text_area: JEditTextArea)
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   354
  { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
56574
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56394
diff changeset
   355
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56394
diff changeset
   356
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56394
diff changeset
   357
  /* spell-checker dictionary */
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56394
diff changeset
   358
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56394
diff changeset
   359
  def update_dictionary(text_area: JEditTextArea, include: Boolean, permanent: Boolean)
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56394
diff changeset
   360
  {
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56394
diff changeset
   361
    for {
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56394
diff changeset
   362
      spell_checker <- PIDE.spell_checker.get
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56394
diff changeset
   363
      doc_view <- PIDE.document_view(text_area)
56576
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56575
diff changeset
   364
      rendering = doc_view.get_rendering()
56592
5157f7615e99 prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents: 56587
diff changeset
   365
      range = JEdit_Lib.caret_range(text_area)
56576
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56575
diff changeset
   366
      Text.Info(_, word) <- Spell_Checker.current_word(text_area, rendering, range)
56575
cdd609ea595d full repaint after dictionary update;
wenzelm
parents: 56574
diff changeset
   367
    } {
cdd609ea595d full repaint after dictionary update;
wenzelm
parents: 56574
diff changeset
   368
      spell_checker.update(word, include, permanent)
cdd609ea595d full repaint after dictionary update;
wenzelm
parents: 56574
diff changeset
   369
      JEdit_Lib.jedit_views().foreach(_.repaint())
cdd609ea595d full repaint after dictionary update;
wenzelm
parents: 56574
diff changeset
   370
    }
56574
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56394
diff changeset
   371
  }
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56394
diff changeset
   372
56578
e73723b39c82 proper signature for dynamic BeanShell action;
wenzelm
parents: 56576
diff changeset
   373
  def reset_dictionary()
56575
cdd609ea595d full repaint after dictionary update;
wenzelm
parents: 56574
diff changeset
   374
  {
cdd609ea595d full repaint after dictionary update;
wenzelm
parents: 56574
diff changeset
   375
    for (spell_checker <- PIDE.spell_checker.get)
cdd609ea595d full repaint after dictionary update;
wenzelm
parents: 56574
diff changeset
   376
    {
cdd609ea595d full repaint after dictionary update;
wenzelm
parents: 56574
diff changeset
   377
      spell_checker.reset()
cdd609ea595d full repaint after dictionary update;
wenzelm
parents: 56574
diff changeset
   378
      JEdit_Lib.jedit_views().foreach(_.repaint())
cdd609ea595d full repaint after dictionary update;
wenzelm
parents: 56574
diff changeset
   379
    }
cdd609ea595d full repaint after dictionary update;
wenzelm
parents: 56574
diff changeset
   380
  }
57627
65fc7ae1bf66 added action "isabelle.options" (despite problems with initial window size);
wenzelm
parents: 57612
diff changeset
   381
65fc7ae1bf66 added action "isabelle.options" (despite problems with initial window size);
wenzelm
parents: 57612
diff changeset
   382
60878
1f0d2bbcf38b added action to toggle breakpoints (on editor side);
wenzelm
parents: 60843
diff changeset
   383
  /* debugger */
1f0d2bbcf38b added action to toggle breakpoints (on editor side);
wenzelm
parents: 60843
diff changeset
   384
60890
e2aeaa397e93 GUI actions depend on active debugger;
wenzelm
parents: 60880
diff changeset
   385
  def toggle_breakpoint(text_area: JEditTextArea): Unit =
e2aeaa397e93 GUI actions depend on active debugger;
wenzelm
parents: 60880
diff changeset
   386
    if (Debugger.is_active()) {
e2aeaa397e93 GUI actions depend on active debugger;
wenzelm
parents: 60880
diff changeset
   387
      for {
e2aeaa397e93 GUI actions depend on active debugger;
wenzelm
parents: 60880
diff changeset
   388
        (command, serial) <- Debugger_Dockable.get_breakpoint(text_area, text_area.getCaretPosition)
e2aeaa397e93 GUI actions depend on active debugger;
wenzelm
parents: 60880
diff changeset
   389
      } Debugger_Dockable.toggle_breakpoint(command, serial)
e2aeaa397e93 GUI actions depend on active debugger;
wenzelm
parents: 60880
diff changeset
   390
    }
60878
1f0d2bbcf38b added action to toggle breakpoints (on editor side);
wenzelm
parents: 60843
diff changeset
   391
1f0d2bbcf38b added action to toggle breakpoints (on editor side);
wenzelm
parents: 60843
diff changeset
   392
57627
65fc7ae1bf66 added action "isabelle.options" (despite problems with initial window size);
wenzelm
parents: 57612
diff changeset
   393
  /* plugin options */
65fc7ae1bf66 added action "isabelle.options" (despite problems with initial window size);
wenzelm
parents: 57612
diff changeset
   394
65fc7ae1bf66 added action "isabelle.options" (despite problems with initial window size);
wenzelm
parents: 57612
diff changeset
   395
  def plugin_options(frame: Frame)
65fc7ae1bf66 added action "isabelle.options" (despite problems with initial window size);
wenzelm
parents: 57612
diff changeset
   396
  {
65fc7ae1bf66 added action "isabelle.options" (despite problems with initial window size);
wenzelm
parents: 57612
diff changeset
   397
    GUI_Thread.require {}
61024
7b7f01afab71 avoid deprecated PluginOptions with its unbounded window size;
wenzelm
parents: 60890
diff changeset
   398
    jEdit.setProperty("Plugin Options.last", "isabelle-general")
7b7f01afab71 avoid deprecated PluginOptions with its unbounded window size;
wenzelm
parents: 60890
diff changeset
   399
    new CombinedOptions(frame, 1)
57627
65fc7ae1bf66 added action "isabelle.options" (despite problems with initial window size);
wenzelm
parents: 57612
diff changeset
   400
  }
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   401
}