src/Tools/jEdit/src/isabelle.scala
author wenzelm
Wed, 16 Dec 2020 13:17:48 +0100
changeset 73168 25cc8f5184e5
parent 73167 69f768aff611
child 73170 0cc298e29aff
permissions -rw-r--r--
clarified select_entity (again): it is meant as approximation to "refactoring" and thus only makes sense for defs within the same buffer;
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
71711
a80fa14bccb8 more Isabelle/jEdit actions;
wenzelm
parents: 71709
diff changeset
    12
import java.awt.{Frame, Point}
57627
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
63455
019856db2bb6 added action "isabelle.newline" (shortcut ENTER);
wenzelm
parents: 63444
diff changeset
    19
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, StructureMatcher, Selection}
58529
cd4439d8799c support for bibtex token markup;
wenzelm
parents: 57861
diff changeset
    20
import org.gjt.sp.jedit.syntax.TokenMarker
63421
3bf02e7fa8a3 basic setup for indentation;
wenzelm
parents: 63236
diff changeset
    21
import org.gjt.sp.jedit.indent.IndentRule
53293
fd27b8f5a479 added action isabelle.complete, using standard jEdit keyboard shortcut;
wenzelm
parents: 53281
diff changeset
    22
import org.gjt.sp.jedit.gui.{DockableWindowManager, CompleteWord}
61024
7b7f01afab71 avoid deprecated PluginOptions with its unbounded window size;
wenzelm
parents: 60890
diff changeset
    23
import org.jedit.options.CombinedOptions
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
    24
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
    25
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    26
object Isabelle
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
    27
{
53274
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    28
  /* editor modes */
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    29
53277
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    30
  val modes =
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    31
    List(
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    32
      "isabelle",         // theory source
55500
cdbbaa3074a8 isabelle-ml mode with separate token marker;
wenzelm
parents: 55316
diff changeset
    33
      "isabelle-ml",      // ML source
53277
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    34
      "isabelle-news",    // NEWS
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    35
      "isabelle-options", // etc/options
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    36
      "isabelle-output",  // pretty text area output
56277
c4f75e733812 separate "sml" mode, suppress old "ml" mode altogether;
wenzelm
parents: 56170
diff changeset
    37
      "isabelle-root",    // session ROOT
c4f75e733812 separate "sml" mode, suppress old "ml" mode altogether;
wenzelm
parents: 56170
diff changeset
    38
      "sml")              // Standard ML (not Isabelle/ML)
53274
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    39
67004
af72fa58f71b clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents: 66984
diff changeset
    40
  private val ml_syntax: Outer_Syntax =
af72fa58f71b clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents: 66984
diff changeset
    41
    Outer_Syntax.empty.no_tokens.
55749
75a48dc4383e tuned signature;
wenzelm
parents: 55666
diff changeset
    42
      set_language_context(Completion.Language_Context.ML_outer)
55616
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55560
diff changeset
    43
67004
af72fa58f71b clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents: 66984
diff changeset
    44
  private val sml_syntax: Outer_Syntax =
af72fa58f71b clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents: 66984
diff changeset
    45
    Outer_Syntax.empty.no_tokens.
56278
2576d3a40ed6 separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents: 56277
diff changeset
    46
      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
    47
67004
af72fa58f71b clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents: 66984
diff changeset
    48
  private val news_syntax: Outer_Syntax =
af72fa58f71b clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents: 66984
diff changeset
    49
    Outer_Syntax.empty.no_tokens
53276
cbed0aa0b0db syntax for isabelle-news with symbol completion;
wenzelm
parents: 53274
diff changeset
    50
59076
65babcd8b0e6 clarified token marker / syntax for mode vs. buffer;
wenzelm
parents: 59075
diff changeset
    51
  def mode_syntax(mode: String): Option[Outer_Syntax] =
65babcd8b0e6 clarified token marker / syntax for mode vs. buffer;
wenzelm
parents: 59075
diff changeset
    52
    mode match {
66720
b07192253605 tuned signature;
wenzelm
parents: 66469
diff changeset
    53
      case "isabelle" => Some(PIDE.resources.session_base.overall_syntax)
53274
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    54
      case "isabelle-options" => Some(Options.options_syntax)
62631
c39614ddb80b clarified modules;
wenzelm
parents: 62104
diff changeset
    55
      case "isabelle-root" => Some(Sessions.root_syntax)
55616
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55560
diff changeset
    56
      case "isabelle-ml" => Some(ml_syntax)
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55560
diff changeset
    57
      case "isabelle-news" => Some(news_syntax)
53277
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    58
      case "isabelle-output" => None
56278
2576d3a40ed6 separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents: 56277
diff changeset
    59
      case "sml" => Some(sml_syntax)
53274
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    60
      case _ => None
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    61
    }
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    62
59074
7836d927ffca tuned signature;
wenzelm
parents: 58804
diff changeset
    63
  def buffer_syntax(buffer: JEditBuffer): Option[Outer_Syntax] =
63868
22037a819276 more robust;
wenzelm
parents: 63865
diff changeset
    64
    if (buffer == null) None
22037a819276 more robust;
wenzelm
parents: 63865
diff changeset
    65
    else
64813
7283f41d05ab manage buffer models as explicit global state;
wenzelm
parents: 64665
diff changeset
    66
      (JEdit_Lib.buffer_mode(buffer), Document_Model.get(buffer)) match {
63868
22037a819276 more robust;
wenzelm
parents: 63865
diff changeset
    67
        case ("isabelle", Some(model)) =>
22037a819276 more robust;
wenzelm
parents: 63865
diff changeset
    68
          Some(PIDE.session.recent_syntax(model.node_name))
22037a819276 more robust;
wenzelm
parents: 63865
diff changeset
    69
        case (mode, _) => mode_syntax(mode)
22037a819276 more robust;
wenzelm
parents: 63865
diff changeset
    70
      }
59074
7836d927ffca tuned signature;
wenzelm
parents: 58804
diff changeset
    71
53274
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    72
53277
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    73
  /* token markers */
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    74
59076
65babcd8b0e6 clarified token marker / syntax for mode vs. buffer;
wenzelm
parents: 59075
diff changeset
    75
  private val mode_markers: Map[String, TokenMarker] =
65babcd8b0e6 clarified token marker / syntax for mode vs. buffer;
wenzelm
parents: 59075
diff changeset
    76
    Map(modes.map(mode => (mode, new Token_Markup.Marker(mode, None))): _*) +
66120
e03ff7e831cc clarified modules;
wenzelm
parents: 66116
diff changeset
    77
      ("bibtex" -> new JEdit_Bibtex.Token_Marker)
53277
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    78
59076
65babcd8b0e6 clarified token marker / syntax for mode vs. buffer;
wenzelm
parents: 59075
diff changeset
    79
  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
    80
65babcd8b0e6 clarified token marker / syntax for mode vs. buffer;
wenzelm
parents: 59075
diff changeset
    81
  def buffer_token_marker(buffer: Buffer): Option[TokenMarker] =
65babcd8b0e6 clarified token marker / syntax for mode vs. buffer;
wenzelm
parents: 59075
diff changeset
    82
  {
65babcd8b0e6 clarified token marker / syntax for mode vs. buffer;
wenzelm
parents: 59075
diff changeset
    83
    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
    84
    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
    85
    else mode_token_marker(mode)
59076
65babcd8b0e6 clarified token marker / syntax for mode vs. buffer;
wenzelm
parents: 59075
diff changeset
    86
  }
53277
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    87
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    88
63422
5cf8dd98a717 clarified modules;
wenzelm
parents: 63421
diff changeset
    89
  /* text structure */
63421
3bf02e7fa8a3 basic setup for indentation;
wenzelm
parents: 63236
diff changeset
    90
63422
5cf8dd98a717 clarified modules;
wenzelm
parents: 63421
diff changeset
    91
  def indent_rule(mode: String): Option[IndentRule] =
63444
8191c3e9f2d3 support more modes;
wenzelm
parents: 63422
diff changeset
    92
    mode match {
8191c3e9f2d3 support more modes;
wenzelm
parents: 63422
diff changeset
    93
      case "isabelle" | "isabelle-options" | "isabelle-root" =>
8191c3e9f2d3 support more modes;
wenzelm
parents: 63422
diff changeset
    94
        Some(Text_Structure.Indent_Rule)
8191c3e9f2d3 support more modes;
wenzelm
parents: 63422
diff changeset
    95
      case _ => None
8191c3e9f2d3 support more modes;
wenzelm
parents: 63422
diff changeset
    96
    }
63421
3bf02e7fa8a3 basic setup for indentation;
wenzelm
parents: 63236
diff changeset
    97
63422
5cf8dd98a717 clarified modules;
wenzelm
parents: 63421
diff changeset
    98
  def structure_matchers(mode: String): List[StructureMatcher] =
5cf8dd98a717 clarified modules;
wenzelm
parents: 63421
diff changeset
    99
    if (mode == "isabelle") List(Text_Structure.Matcher) else Nil
58748
8f92f17d8781 support for structure matching;
wenzelm
parents: 58546
diff changeset
   100
8f92f17d8781 support for structure matching;
wenzelm
parents: 58546
diff changeset
   101
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   102
  /* dockable windows */
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   103
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   104
  private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   105
60749
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents: 60274
diff changeset
   106
  def debugger_dockable(view: View): Option[Debugger_Dockable] =
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents: 60274
diff changeset
   107
    wm(view).getDockableWindow("isabelle-debugger") match {
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents: 60274
diff changeset
   108
      case dockable: Debugger_Dockable => Some(dockable)
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents: 60274
diff changeset
   109
      case _ => None
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents: 60274
diff changeset
   110
    }
f727b99faaf7 skeleton for interactive debugger;
wenzelm
parents: 60274
diff changeset
   111
55560
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   112
  def documentation_dockable(view: View): Option[Documentation_Dockable] =
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   113
    wm(view).getDockableWindow("isabelle-documentation") match {
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   114
      case dockable: Documentation_Dockable => Some(dockable)
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   115
      case _ => None
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   116
    }
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   117
55560
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   118
  def monitor_dockable(view: View): Option[Monitor_Dockable] =
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   119
    wm(view).getDockableWindow("isabelle-monitor") match {
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   120
      case dockable: Monitor_Dockable => Some(dockable)
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   121
      case _ => None
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   122
    }
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   123
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   124
  def output_dockable(view: View): Option[Output_Dockable] =
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   125
    wm(view).getDockableWindow("isabelle-output") match {
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   126
      case dockable: Output_Dockable => Some(dockable)
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   127
      case _ => None
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   128
    }
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   129
55560
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   130
  def protocol_dockable(view: View): Option[Protocol_Dockable] =
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   131
    wm(view).getDockableWindow("isabelle-protocol") match {
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   132
      case dockable: Protocol_Dockable => Some(dockable)
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   133
      case _ => None
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   134
    }
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   135
56879
ee2b61f37ad9 renamed "Find" to "Query", with more general operations;
wenzelm
parents: 56662
diff changeset
   136
  def query_dockable(view: View): Option[Query_Dockable] =
ee2b61f37ad9 renamed "Find" to "Query", with more general operations;
wenzelm
parents: 56662
diff changeset
   137
    wm(view).getDockableWindow("isabelle-query") match {
ee2b61f37ad9 renamed "Find" to "Query", with more general operations;
wenzelm
parents: 56662
diff changeset
   138
      case dockable: Query_Dockable => Some(dockable)
ee2b61f37ad9 renamed "Find" to "Query", with more general operations;
wenzelm
parents: 56662
diff changeset
   139
      case _ => None
ee2b61f37ad9 renamed "Find" to "Query", with more general operations;
wenzelm
parents: 56662
diff changeset
   140
    }
ee2b61f37ad9 renamed "Find" to "Query", with more general operations;
wenzelm
parents: 56662
diff changeset
   141
55560
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   142
  def raw_output_dockable(view: View): Option[Raw_Output_Dockable] =
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   143
    wm(view).getDockableWindow("isabelle-raw-output") match {
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   144
      case dockable: Raw_Output_Dockable => Some(dockable)
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   145
      case _ => None
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   146
    }
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   147
55560
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   148
  def simplifier_trace_dockable(view: View): Option[Simplifier_Trace_Dockable] =
55559
aa1adeca714b standardized action and panel names;
wenzelm
parents: 55500
diff changeset
   149
    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
   150
      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
   151
      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
   152
    }
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
   153
55560
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   154
  def sledgehammer_dockable(view: View): Option[Sledgehammer_Dockable] =
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   155
    wm(view).getDockableWindow("isabelle-sledgehammer") match {
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   156
      case dockable: Sledgehammer_Dockable => Some(dockable)
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   157
      case _ => None
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   158
    }
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   159
61208
19118f9b939d separate panel for proof state output;
wenzelm
parents: 61024
diff changeset
   160
  def state_dockable(view: View): Option[State_Dockable] =
19118f9b939d separate panel for proof state output;
wenzelm
parents: 61024
diff changeset
   161
    wm(view).getDockableWindow("isabelle-state") match {
19118f9b939d separate panel for proof state output;
wenzelm
parents: 61024
diff changeset
   162
      case dockable: State_Dockable => Some(dockable)
19118f9b939d separate panel for proof state output;
wenzelm
parents: 61024
diff changeset
   163
      case _ => None
19118f9b939d separate panel for proof state output;
wenzelm
parents: 61024
diff changeset
   164
    }
19118f9b939d separate panel for proof state output;
wenzelm
parents: 61024
diff changeset
   165
55560
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   166
  def symbols_dockable(view: View): Option[Symbols_Dockable] =
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   167
    wm(view).getDockableWindow("isabelle-symbols") match {
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   168
      case dockable: Symbols_Dockable => Some(dockable)
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   169
      case _ => None
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   170
    }
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   171
55560
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   172
  def syslog_dockable(view: View): Option[Syslog_Dockable] =
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   173
    wm(view).getDockableWindow("isabelle-syslog") match {
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   174
      case dockable: Syslog_Dockable => Some(dockable)
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   175
      case _ => None
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   176
    }
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   177
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   178
  def theories_dockable(view: View): Option[Theories_Dockable] =
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   179
    wm(view).getDockableWindow("isabelle-theories") match {
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   180
      case dockable: Theories_Dockable => Some(dockable)
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   181
      case _ => None
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   182
    }
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   183
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   184
  def timing_dockable(view: View): Option[Timing_Dockable] =
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   185
    wm(view).getDockableWindow("isabelle-timing") match {
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55559
diff changeset
   186
      case dockable: Timing_Dockable => Some(dockable)
50433
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents: 50341
diff changeset
   187
      case _ => None
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents: 50341
diff changeset
   188
    }
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents: 50341
diff changeset
   189
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   190
52815
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   191
  /* continuous checking */
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
  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
   194
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   195
  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
   196
  def continuous_checking_=(b: Boolean): Unit =
38a64cc17403 GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents: 59077
diff changeset
   197
    GUI_Thread.require {
38a64cc17403 GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents: 59077
diff changeset
   198
      if (continuous_checking != b) {
38a64cc17403 GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents: 59077
diff changeset
   199
        PIDE.options.bool(CONTINUOUS_CHECKING) = b
61725
1529c3eb6bac more thorough update of options;
wenzelm
parents: 61483
diff changeset
   200
        PIDE.session.update_options(PIDE.options.value)
60074
38a64cc17403 GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents: 59077
diff changeset
   201
      }
52815
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   202
    }
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   203
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   204
  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
   205
  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
   206
  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
   207
53715
68c664737d04 added option "jedit_auto_load";
wenzelm
parents: 53497
diff changeset
   208
  class Continuous_Checking extends CheckBox("Continuous checking")
68c664737d04 added option "jedit_auto_load";
wenzelm
parents: 53497
diff changeset
   209
  {
68c664737d04 added option "jedit_auto_load";
wenzelm
parents: 53497
diff changeset
   210
    tooltip = "Continuous checking of proof document (visible and required parts)"
68c664737d04 added option "jedit_auto_load";
wenzelm
parents: 53497
diff changeset
   211
    reactions += { case ButtonClicked(_) => continuous_checking = selected }
68c664737d04 added option "jedit_auto_load";
wenzelm
parents: 53497
diff changeset
   212
    def load() { selected = continuous_checking }
68c664737d04 added option "jedit_auto_load";
wenzelm
parents: 53497
diff changeset
   213
    load()
68c664737d04 added option "jedit_auto_load";
wenzelm
parents: 53497
diff changeset
   214
  }
68c664737d04 added option "jedit_auto_load";
wenzelm
parents: 53497
diff changeset
   215
52815
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   216
61211
8a5d5ca5d8bc added action "isabelle-update-state";
wenzelm
parents: 61208
diff changeset
   217
  /* update state */
8a5d5ca5d8bc added action "isabelle-update-state";
wenzelm
parents: 61208
diff changeset
   218
8a5d5ca5d8bc added action "isabelle-update-state";
wenzelm
parents: 61208
diff changeset
   219
  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
   220
    state_dockable(view).foreach(_.update_request())
61211
8a5d5ca5d8bc added action "isabelle-update-state";
wenzelm
parents: 61208
diff changeset
   221
8a5d5ca5d8bc added action "isabelle-update-state";
wenzelm
parents: 61208
diff changeset
   222
52815
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   223
  /* 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
   224
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   225
  def set_node_required(view: View) { Document_Model.view_node_required(view, set = true) }
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   226
  def reset_node_required(view: View) { Document_Model.view_node_required(view, set = false) }
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   227
  def toggle_node_required(view: View) { Document_Model.view_node_required(view, toggle = true) }
52815
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
50198
0c7b351a6871 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents: 50187
diff changeset
   230
  /* font size */
0c7b351a6871 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents: 50187
diff changeset
   231
55827
8a881f83e206 clarified module structure;
wenzelm
parents: 55825
diff changeset
   232
  def reset_font_size() {
8a881f83e206 clarified module structure;
wenzelm
parents: 55825
diff changeset
   233
    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
   234
  }
55827
8a881f83e206 clarified module structure;
wenzelm
parents: 55825
diff changeset
   235
  def increase_font_size() { Font_Info.main_change.step(1) }
8a881f83e206 clarified module structure;
wenzelm
parents: 55825
diff changeset
   236
  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
   237
0c7b351a6871 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents: 50187
diff changeset
   238
53497
07bb77881b8d tuned signature;
wenzelm
parents: 53322
diff changeset
   239
  /* structured edits */
50341
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   240
66180
201d42f67bba indentation of keywords after input;
wenzelm
parents: 66174
diff changeset
   241
  def indent_enabled(buffer: JEditBuffer, option: String): Boolean =
201d42f67bba indentation of keywords after input;
wenzelm
parents: 66174
diff changeset
   242
    indent_rule(JEdit_Lib.buffer_mode(buffer)).isDefined &&
201d42f67bba indentation of keywords after input;
wenzelm
parents: 66174
diff changeset
   243
    buffer.getStringProperty("autoIndent") == "full" &&
201d42f67bba indentation of keywords after input;
wenzelm
parents: 66174
diff changeset
   244
    PIDE.options.bool(option)
201d42f67bba indentation of keywords after input;
wenzelm
parents: 66174
diff changeset
   245
201d42f67bba indentation of keywords after input;
wenzelm
parents: 66174
diff changeset
   246
  def indent_input(text_area: TextArea)
201d42f67bba indentation of keywords after input;
wenzelm
parents: 66174
diff changeset
   247
  {
201d42f67bba indentation of keywords after input;
wenzelm
parents: 66174
diff changeset
   248
    val buffer = text_area.getBuffer
201d42f67bba indentation of keywords after input;
wenzelm
parents: 66174
diff changeset
   249
    val line = text_area.getCaretLine
201d42f67bba indentation of keywords after input;
wenzelm
parents: 66174
diff changeset
   250
    val caret = text_area.getCaretPosition
201d42f67bba indentation of keywords after input;
wenzelm
parents: 66174
diff changeset
   251
201d42f67bba indentation of keywords after input;
wenzelm
parents: 66174
diff changeset
   252
    if (text_area.isEditable && indent_enabled(buffer, "jedit_indent_input")) {
201d42f67bba indentation of keywords after input;
wenzelm
parents: 66174
diff changeset
   253
      buffer_syntax(buffer) match {
66183
c67933ea9234 tuned signature;
wenzelm
parents: 66182
diff changeset
   254
        case Some(syntax) =>
c67933ea9234 tuned signature;
wenzelm
parents: 66182
diff changeset
   255
          val nav = new Text_Structure.Navigator(syntax, buffer, true)
66180
201d42f67bba indentation of keywords after input;
wenzelm
parents: 66174
diff changeset
   256
          nav.iterator(line, 1).toStream.headOption match {
201d42f67bba indentation of keywords after input;
wenzelm
parents: 66174
diff changeset
   257
            case Some(Text.Info(range, tok))
201d42f67bba indentation of keywords after input;
wenzelm
parents: 66174
diff changeset
   258
            if range.stop == caret && syntax.keywords.is_indent_command(tok) =>
201d42f67bba indentation of keywords after input;
wenzelm
parents: 66174
diff changeset
   259
              buffer.indentLine(line, true)
201d42f67bba indentation of keywords after input;
wenzelm
parents: 66174
diff changeset
   260
            case _ =>
201d42f67bba indentation of keywords after input;
wenzelm
parents: 66174
diff changeset
   261
          }
66183
c67933ea9234 tuned signature;
wenzelm
parents: 66182
diff changeset
   262
        case None =>
66180
201d42f67bba indentation of keywords after input;
wenzelm
parents: 66174
diff changeset
   263
      }
201d42f67bba indentation of keywords after input;
wenzelm
parents: 66174
diff changeset
   264
    }
201d42f67bba indentation of keywords after input;
wenzelm
parents: 66174
diff changeset
   265
  }
201d42f67bba indentation of keywords after input;
wenzelm
parents: 66174
diff changeset
   266
63455
019856db2bb6 added action "isabelle.newline" (shortcut ENTER);
wenzelm
parents: 63444
diff changeset
   267
  def newline(text_area: TextArea)
019856db2bb6 added action "isabelle.newline" (shortcut ENTER);
wenzelm
parents: 63444
diff changeset
   268
  {
019856db2bb6 added action "isabelle.newline" (shortcut ENTER);
wenzelm
parents: 63444
diff changeset
   269
    if (!text_area.isEditable()) text_area.getToolkit().beep()
019856db2bb6 added action "isabelle.newline" (shortcut ENTER);
wenzelm
parents: 63444
diff changeset
   270
    else {
019856db2bb6 added action "isabelle.newline" (shortcut ENTER);
wenzelm
parents: 63444
diff changeset
   271
      val buffer = text_area.getBuffer
66182
wenzelm
parents: 66180
diff changeset
   272
      val line = text_area.getCaretLine
wenzelm
parents: 66180
diff changeset
   273
      val caret = text_area.getCaretPosition
wenzelm
parents: 66180
diff changeset
   274
63455
019856db2bb6 added action "isabelle.newline" (shortcut ENTER);
wenzelm
parents: 63444
diff changeset
   275
      def nl { text_area.userInput('\n') }
019856db2bb6 added action "isabelle.newline" (shortcut ENTER);
wenzelm
parents: 63444
diff changeset
   276
66180
201d42f67bba indentation of keywords after input;
wenzelm
parents: 66174
diff changeset
   277
      if (indent_enabled(buffer, "jedit_indent_newline")) {
201d42f67bba indentation of keywords after input;
wenzelm
parents: 66174
diff changeset
   278
        buffer_syntax(buffer) match {
66182
wenzelm
parents: 66180
diff changeset
   279
          case Some(syntax) =>
63484
2033a3960c36 auto indentation of quasi commands;
wenzelm
parents: 63477
diff changeset
   280
            val keywords = syntax.keywords
2033a3960c36 auto indentation of quasi commands;
wenzelm
parents: 63477
diff changeset
   281
66173
6c71a3af85a3 clarified modules;
wenzelm
parents: 66120
diff changeset
   282
            val (toks1, toks2) = Text_Structure.split_line_content(buffer, keywords, line, caret)
63455
019856db2bb6 added action "isabelle.newline" (shortcut ENTER);
wenzelm
parents: 63444
diff changeset
   283
66174
8903653fc22e avoid trailing spaces;
wenzelm
parents: 66173
diff changeset
   284
            if (toks1.isEmpty) buffer.removeTrailingWhiteSpace(Array(line))
8903653fc22e avoid trailing spaces;
wenzelm
parents: 66173
diff changeset
   285
            else if (keywords.is_indent_command(toks1.head)) buffer.indentLine(line, true)
63455
019856db2bb6 added action "isabelle.newline" (shortcut ENTER);
wenzelm
parents: 63444
diff changeset
   286
66469
a6ec0172211a avoid compound edit: it causes confusion about the context of the last line, e.g. final "end";
wenzelm
parents: 66183
diff changeset
   287
            if (toks2.isEmpty || keywords.is_indent_command(toks2.head)) {
a6ec0172211a avoid compound edit: it causes confusion about the context of the last line, e.g. final "end";
wenzelm
parents: 66183
diff changeset
   288
              text_area.setSelectedText("\n")
a6ec0172211a avoid compound edit: it causes confusion about the context of the last line, e.g. final "end";
wenzelm
parents: 66183
diff changeset
   289
              if (!buffer.indentLine(line + 1, true)) text_area.goToStartOfWhiteSpace(false)
a6ec0172211a avoid compound edit: it causes confusion about the context of the last line, e.g. final "end";
wenzelm
parents: 66183
diff changeset
   290
            }
63455
019856db2bb6 added action "isabelle.newline" (shortcut ENTER);
wenzelm
parents: 63444
diff changeset
   291
            else nl
66182
wenzelm
parents: 66180
diff changeset
   292
          case None => nl
63455
019856db2bb6 added action "isabelle.newline" (shortcut ENTER);
wenzelm
parents: 63444
diff changeset
   293
        }
019856db2bb6 added action "isabelle.newline" (shortcut ENTER);
wenzelm
parents: 63444
diff changeset
   294
      }
019856db2bb6 added action "isabelle.newline" (shortcut ENTER);
wenzelm
parents: 63444
diff changeset
   295
      else nl
019856db2bb6 added action "isabelle.newline" (shortcut ENTER);
wenzelm
parents: 63444
diff changeset
   296
    }
019856db2bb6 added action "isabelle.newline" (shortcut ENTER);
wenzelm
parents: 63444
diff changeset
   297
  }
019856db2bb6 added action "isabelle.newline" (shortcut ENTER);
wenzelm
parents: 63444
diff changeset
   298
50341
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   299
  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
   300
  {
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   301
    val buffer = text_area.getBuffer
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   302
    JEdit_Lib.buffer_edit(buffer) {
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   303
      val text1 =
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   304
        if (text_area.getSelectionCount == 0) {
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   305
          def pad(range: Text.Range): String =
67014
e6a695d6a6b2 tuned signature;
wenzelm
parents: 67004
diff changeset
   306
            if (JEdit_Lib.get_text(buffer, range) == Some("\n")) "" else "\n"
50341
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   307
56592
5157f7615e99 prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents: 56587
diff changeset
   308
          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
   309
          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
   310
          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
   311
        }
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   312
        else text
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   313
      text_area.setSelectedText(text1)
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   314
    }
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   315
  }
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   316
53497
07bb77881b8d tuned signature;
wenzelm
parents: 53322
diff changeset
   317
  def edit_command(
07bb77881b8d tuned signature;
wenzelm
parents: 53322
diff changeset
   318
    snapshot: Document.Snapshot,
63508
348599644887 more structured edit, including indentation;
wenzelm
parents: 63484
diff changeset
   319
    text_area: TextArea,
53497
07bb77881b8d tuned signature;
wenzelm
parents: 53322
diff changeset
   320
    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
   321
    id: Document_ID.Generic,
63508
348599644887 more structured edit, including indentation;
wenzelm
parents: 63484
diff changeset
   322
    text: String)
53497
07bb77881b8d tuned signature;
wenzelm
parents: 53322
diff changeset
   323
  {
63508
348599644887 more structured edit, including indentation;
wenzelm
parents: 63484
diff changeset
   324
    val buffer = text_area.getBuffer
348599644887 more structured edit, including indentation;
wenzelm
parents: 63484
diff changeset
   325
    if (!snapshot.is_outdated && text != "") {
64813
7283f41d05ab manage buffer models as explicit global state;
wenzelm
parents: 64665
diff changeset
   326
      (snapshot.find_command(id), Document_Model.get(buffer)) match {
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
   327
        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
   328
          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
   329
            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
   330
              JEdit_Lib.buffer_edit(buffer) {
68728
c07f6fa02c59 tuned signature;
wenzelm
parents: 67148
diff changeset
   331
                val range = command.core_range + start
63508
348599644887 more structured edit, including indentation;
wenzelm
parents: 63484
diff changeset
   332
                JEdit_Lib.buffer_edit(buffer) {
348599644887 more structured edit, including indentation;
wenzelm
parents: 63484
diff changeset
   333
                  if (padding) {
348599644887 more structured edit, including indentation;
wenzelm
parents: 63484
diff changeset
   334
                    text_area.moveCaretPosition(start + range.length)
64456
f630e9385d7e more accurate start_line: avoid changing the original command (e.g. 'try', 'sledgehammer');
wenzelm
parents: 63868
diff changeset
   335
                    val start_line = text_area.getCaretLine + 1
63508
348599644887 more structured edit, including indentation;
wenzelm
parents: 63484
diff changeset
   336
                    text_area.setSelectedText("\n" + text)
348599644887 more structured edit, including indentation;
wenzelm
parents: 63484
diff changeset
   337
                    val end_line = text_area.getCaretLine
348599644887 more structured edit, including indentation;
wenzelm
parents: 63484
diff changeset
   338
                    buffer.indentLines(start_line, end_line)
348599644887 more structured edit, including indentation;
wenzelm
parents: 63484
diff changeset
   339
                  }
348599644887 more structured edit, including indentation;
wenzelm
parents: 63484
diff changeset
   340
                  else {
348599644887 more structured edit, including indentation;
wenzelm
parents: 63484
diff changeset
   341
                    buffer.remove(start, range.length)
348599644887 more structured edit, including indentation;
wenzelm
parents: 63484
diff changeset
   342
                    text_area.moveCaretPosition(start)
348599644887 more structured edit, including indentation;
wenzelm
parents: 63484
diff changeset
   343
                    text_area.setSelectedText(text)
348599644887 more structured edit, including indentation;
wenzelm
parents: 63484
diff changeset
   344
                  }
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
   345
                }
53497
07bb77881b8d tuned signature;
wenzelm
parents: 53322
diff changeset
   346
              }
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
   347
            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
   348
          }
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
   349
        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
   350
      }
53497
07bb77881b8d tuned signature;
wenzelm
parents: 53322
diff changeset
   351
    }
07bb77881b8d tuned signature;
wenzelm
parents: 53322
diff changeset
   352
  }
07bb77881b8d tuned signature;
wenzelm
parents: 53322
diff changeset
   353
50341
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   354
63236
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
   355
  /* selection */
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
   356
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
   357
  def select_entity(text_area: JEditTextArea)
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
   358
  {
71709
wenzelm
parents: 68728
diff changeset
   359
    for (doc_view <- Document_View.get(text_area)) {
wenzelm
parents: 68728
diff changeset
   360
      val rendering = doc_view.get_rendering()
63236
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
   361
      val caret_range = JEdit_Lib.caret_range(text_area)
73168
25cc8f5184e5 clarified select_entity (again): it is meant as approximation to "refactoring" and thus only makes sense for defs within the same buffer;
wenzelm
parents: 73167
diff changeset
   362
      val buffer_range = JEdit_Lib.buffer_range(text_area.getBuffer)
25cc8f5184e5 clarified select_entity (again): it is meant as approximation to "refactoring" and thus only makes sense for defs within the same buffer;
wenzelm
parents: 73167
diff changeset
   363
      val active_focus = rendering.caret_focus_ranges(caret_range, buffer_range)
63236
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
   364
      if (active_focus.nonEmpty) {
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
   365
        text_area.selectNone()
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
   366
        for (r <- active_focus)
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
   367
          text_area.addToSelection(new Selection.Range(r.start, r.stop))
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
   368
      }
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
   369
    }
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
   370
  }
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
   371
48bc9045866e added action "isabelle.select-entity";
wenzelm
parents: 62631
diff changeset
   372
53293
fd27b8f5a479 added action isabelle.complete, using standard jEdit keyboard shortcut;
wenzelm
parents: 53281
diff changeset
   373
  /* completion */
fd27b8f5a479 added action isabelle.complete, using standard jEdit keyboard shortcut;
wenzelm
parents: 53281
diff changeset
   374
56586
5ef60881681d explicit menu action to complete word;
wenzelm
parents: 56578
diff changeset
   375
  def complete(view: View, word_only: Boolean)
53293
fd27b8f5a479 added action isabelle.complete, using standard jEdit keyboard shortcut;
wenzelm
parents: 53281
diff changeset
   376
  {
57424
966b12f636b9 removed slightly odd fall-back on complete-word (NB: connection to default menu action is unclear);
wenzelm
parents: 56879
diff changeset
   377
    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
   378
  }
fd27b8f5a479 added action isabelle.complete, using standard jEdit keyboard shortcut;
wenzelm
parents: 53281
diff changeset
   379
fd27b8f5a479 added action isabelle.complete, using standard jEdit keyboard shortcut;
wenzelm
parents: 53281
diff changeset
   380
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   381
  /* control styles */
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   382
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   383
  def control_sub(text_area: JEditTextArea)
65259
41d12227d5dc clarified modules;
wenzelm
parents: 65247
diff changeset
   384
  { Syntax_Style.edit_control_style(text_area, Symbol.sub) }
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   385
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   386
  def control_sup(text_area: JEditTextArea)
65259
41d12227d5dc clarified modules;
wenzelm
parents: 65247
diff changeset
   387
  { Syntax_Style.edit_control_style(text_area, Symbol.sup) }
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   388
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   389
  def control_bold(text_area: JEditTextArea)
65259
41d12227d5dc clarified modules;
wenzelm
parents: 65247
diff changeset
   390
  { Syntax_Style.edit_control_style(text_area, Symbol.bold) }
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   391
61483
07c8d5d8acab added action "isabelle-emph";
wenzelm
parents: 61211
diff changeset
   392
  def control_emph(text_area: JEditTextArea)
65259
41d12227d5dc clarified modules;
wenzelm
parents: 65247
diff changeset
   393
  { Syntax_Style.edit_control_style(text_area, Symbol.emph) }
61483
07c8d5d8acab added action "isabelle-emph";
wenzelm
parents: 61211
diff changeset
   394
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   395
  def control_reset(text_area: JEditTextArea)
65259
41d12227d5dc clarified modules;
wenzelm
parents: 65247
diff changeset
   396
  { Syntax_Style.edit_control_style(text_area, "") }
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   397
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   398
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   399
  /* block styles */
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   400
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   401
  private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   402
  {
71816
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71734
diff changeset
   403
    s1.foreach(text_area.userInput)
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71734
diff changeset
   404
    s2.foreach(text_area.userInput)
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   405
    s2.foreach(_ => text_area.goToPrevCharacter(false))
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   406
  }
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   407
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   408
  def input_bsub(text_area: JEditTextArea)
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   409
  { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) }
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   410
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   411
  def input_bsup(text_area: JEditTextArea)
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   412
  { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
56574
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56394
diff changeset
   413
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56394
diff changeset
   414
67132
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   415
  /* antiquoted cartouche */
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   416
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   417
  def antiquoted_cartouche(text_area: TextArea)
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   418
  {
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   419
    val buffer = text_area.getBuffer
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   420
    for {
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   421
      doc_view <- Document_View.get(text_area)
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   422
      rendering = doc_view.get_rendering()
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   423
      caret_range = JEdit_Lib.caret_range(text_area)
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   424
      antiq_range <- rendering.antiquoted(caret_range)
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   425
      antiq_text <- JEdit_Lib.get_text(buffer, antiq_range)
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   426
      body_text <- Antiquote.read_antiq_body(antiq_text)
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   427
      (name, arg) <- Token.read_antiq_arg(Keyword.Keywords.empty, body_text)
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   428
      if Symbol.is_ascii_identifier(name)
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   429
    } {
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   430
      val op_text =
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   431
        Isabelle_Encoding.perhaps_decode(buffer,
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   432
          Symbol.control_prefix + name + Symbol.control_suffix)
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   433
      val arg_text =
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   434
        if (arg.isEmpty) ""
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   435
        else if (Isabelle_Encoding.is_active(buffer)) Symbol.cartouche_decoded(arg.get)
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   436
        else Symbol.cartouche(arg.get)
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   437
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   438
      buffer.remove(antiq_range.start, antiq_range.length)
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   439
      text_area.moveCaretPosition(antiq_range.start)
67148
d24dcac5eb4c more robust, e.g. when Sidekick produces multi-selection;
wenzelm
parents: 67132
diff changeset
   440
      text_area.selectNone
67132
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   441
      text_area.setSelectedText(op_text + arg_text)
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   442
    }
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   443
  }
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   444
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   445
56574
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56394
diff changeset
   446
  /* spell-checker dictionary */
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56394
diff changeset
   447
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56394
diff changeset
   448
  def update_dictionary(text_area: JEditTextArea, include: Boolean, permanent: Boolean)
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56394
diff changeset
   449
  {
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56394
diff changeset
   450
    for {
65239
509a9b0ad02e avoid global variables with implicit initialization;
wenzelm
parents: 65224
diff changeset
   451
      spell_checker <- PIDE.plugin.spell_checker.get
64882
c3b42ac0cf81 tuned signature;
wenzelm
parents: 64854
diff changeset
   452
      doc_view <- Document_View.get(text_area)
56576
86148ca3c4fd added context menu for spell checker actions;
wenzelm
parents: 56575
diff changeset
   453
      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
   454
      range = JEdit_Lib.caret_range(text_area)
66116
dad409cd3423 clarified modules;
wenzelm
parents: 65361
diff changeset
   455
      Text.Info(_, word) <- Spell_Checker.current_word(rendering, range)
56575
cdd609ea595d full repaint after dictionary update;
wenzelm
parents: 56574
diff changeset
   456
    } {
cdd609ea595d full repaint after dictionary update;
wenzelm
parents: 56574
diff changeset
   457
      spell_checker.update(word, include, permanent)
cdd609ea595d full repaint after dictionary update;
wenzelm
parents: 56574
diff changeset
   458
      JEdit_Lib.jedit_views().foreach(_.repaint())
cdd609ea595d full repaint after dictionary update;
wenzelm
parents: 56574
diff changeset
   459
    }
56574
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56394
diff changeset
   460
  }
2b38472a4695 some actions to maintain spell-checker dictionary;
wenzelm
parents: 56394
diff changeset
   461
56578
e73723b39c82 proper signature for dynamic BeanShell action;
wenzelm
parents: 56576
diff changeset
   462
  def reset_dictionary()
56575
cdd609ea595d full repaint after dictionary update;
wenzelm
parents: 56574
diff changeset
   463
  {
65239
509a9b0ad02e avoid global variables with implicit initialization;
wenzelm
parents: 65224
diff changeset
   464
    for (spell_checker <- PIDE.plugin.spell_checker.get)
56575
cdd609ea595d full repaint after dictionary update;
wenzelm
parents: 56574
diff changeset
   465
    {
cdd609ea595d full repaint after dictionary update;
wenzelm
parents: 56574
diff changeset
   466
      spell_checker.reset()
cdd609ea595d full repaint after dictionary update;
wenzelm
parents: 56574
diff changeset
   467
      JEdit_Lib.jedit_views().foreach(_.repaint())
cdd609ea595d full repaint after dictionary update;
wenzelm
parents: 56574
diff changeset
   468
    }
cdd609ea595d full repaint after dictionary update;
wenzelm
parents: 56574
diff changeset
   469
  }
57627
65fc7ae1bf66 added action "isabelle.options" (despite problems with initial window size);
wenzelm
parents: 57612
diff changeset
   470
65fc7ae1bf66 added action "isabelle.options" (despite problems with initial window size);
wenzelm
parents: 57612
diff changeset
   471
60878
1f0d2bbcf38b added action to toggle breakpoints (on editor side);
wenzelm
parents: 60843
diff changeset
   472
  /* debugger */
1f0d2bbcf38b added action to toggle breakpoints (on editor side);
wenzelm
parents: 60843
diff changeset
   473
60890
e2aeaa397e93 GUI actions depend on active debugger;
wenzelm
parents: 60880
diff changeset
   474
  def toggle_breakpoint(text_area: JEditTextArea): Unit =
65224
wenzelm
parents: 65213
diff changeset
   475
  {
wenzelm
parents: 65213
diff changeset
   476
    GUI_Thread.require {}
wenzelm
parents: 65213
diff changeset
   477
65247
63d91d5de121 tuned signature;
wenzelm
parents: 65240
diff changeset
   478
    if (PIDE.session.debugger.is_active()) {
65224
wenzelm
parents: 65213
diff changeset
   479
      Debugger_Dockable.get_breakpoint(text_area, text_area.getCaretPosition) match {
wenzelm
parents: 65213
diff changeset
   480
        case Some((command, breakpoint)) =>
65247
63d91d5de121 tuned signature;
wenzelm
parents: 65240
diff changeset
   481
          PIDE.session.debugger.toggle_breakpoint(command, breakpoint)
65224
wenzelm
parents: 65213
diff changeset
   482
          jEdit.propertiesChanged()
wenzelm
parents: 65213
diff changeset
   483
        case None =>
wenzelm
parents: 65213
diff changeset
   484
      }
60890
e2aeaa397e93 GUI actions depend on active debugger;
wenzelm
parents: 60880
diff changeset
   485
    }
65224
wenzelm
parents: 65213
diff changeset
   486
  }
60878
1f0d2bbcf38b added action to toggle breakpoints (on editor side);
wenzelm
parents: 60843
diff changeset
   487
1f0d2bbcf38b added action to toggle breakpoints (on editor side);
wenzelm
parents: 60843
diff changeset
   488
57627
65fc7ae1bf66 added action "isabelle.options" (despite problems with initial window size);
wenzelm
parents: 57612
diff changeset
   489
  /* plugin options */
65fc7ae1bf66 added action "isabelle.options" (despite problems with initial window size);
wenzelm
parents: 57612
diff changeset
   490
65fc7ae1bf66 added action "isabelle.options" (despite problems with initial window size);
wenzelm
parents: 57612
diff changeset
   491
  def plugin_options(frame: Frame)
65fc7ae1bf66 added action "isabelle.options" (despite problems with initial window size);
wenzelm
parents: 57612
diff changeset
   492
  {
65fc7ae1bf66 added action "isabelle.options" (despite problems with initial window size);
wenzelm
parents: 57612
diff changeset
   493
    GUI_Thread.require {}
61024
7b7f01afab71 avoid deprecated PluginOptions with its unbounded window size;
wenzelm
parents: 60890
diff changeset
   494
    jEdit.setProperty("Plugin Options.last", "isabelle-general")
7b7f01afab71 avoid deprecated PluginOptions with its unbounded window size;
wenzelm
parents: 60890
diff changeset
   495
    new CombinedOptions(frame, 1)
57627
65fc7ae1bf66 added action "isabelle.options" (despite problems with initial window size);
wenzelm
parents: 57612
diff changeset
   496
  }
65240
fe5a96240749 clarified modules;
wenzelm
parents: 65239
diff changeset
   497
fe5a96240749 clarified modules;
wenzelm
parents: 65239
diff changeset
   498
fe5a96240749 clarified modules;
wenzelm
parents: 65239
diff changeset
   499
  /* popups */
fe5a96240749 clarified modules;
wenzelm
parents: 65239
diff changeset
   500
fe5a96240749 clarified modules;
wenzelm
parents: 65239
diff changeset
   501
  def dismissed_popups(view: View): Boolean =
fe5a96240749 clarified modules;
wenzelm
parents: 65239
diff changeset
   502
  {
fe5a96240749 clarified modules;
wenzelm
parents: 65239
diff changeset
   503
    var dismissed = false
fe5a96240749 clarified modules;
wenzelm
parents: 65239
diff changeset
   504
fe5a96240749 clarified modules;
wenzelm
parents: 65239
diff changeset
   505
    JEdit_Lib.jedit_text_areas(view).foreach(text_area =>
fe5a96240749 clarified modules;
wenzelm
parents: 65239
diff changeset
   506
      if (Completion_Popup.Text_Area.dismissed(text_area)) dismissed = true)
fe5a96240749 clarified modules;
wenzelm
parents: 65239
diff changeset
   507
fe5a96240749 clarified modules;
wenzelm
parents: 65239
diff changeset
   508
    if (Pretty_Tooltip.dismissed_all()) dismissed = true
fe5a96240749 clarified modules;
wenzelm
parents: 65239
diff changeset
   509
fe5a96240749 clarified modules;
wenzelm
parents: 65239
diff changeset
   510
    dismissed
fe5a96240749 clarified modules;
wenzelm
parents: 65239
diff changeset
   511
  }
71711
a80fa14bccb8 more Isabelle/jEdit actions;
wenzelm
parents: 71709
diff changeset
   512
a80fa14bccb8 more Isabelle/jEdit actions;
wenzelm
parents: 71709
diff changeset
   513
a80fa14bccb8 more Isabelle/jEdit actions;
wenzelm
parents: 71709
diff changeset
   514
  /* tooltips */
a80fa14bccb8 more Isabelle/jEdit actions;
wenzelm
parents: 71709
diff changeset
   515
a80fa14bccb8 more Isabelle/jEdit actions;
wenzelm
parents: 71709
diff changeset
   516
  def show_tooltip(view: View, control: Boolean)
a80fa14bccb8 more Isabelle/jEdit actions;
wenzelm
parents: 71709
diff changeset
   517
  {
a80fa14bccb8 more Isabelle/jEdit actions;
wenzelm
parents: 71709
diff changeset
   518
    GUI_Thread.require {}
a80fa14bccb8 more Isabelle/jEdit actions;
wenzelm
parents: 71709
diff changeset
   519
a80fa14bccb8 more Isabelle/jEdit actions;
wenzelm
parents: 71709
diff changeset
   520
    val text_area = view.getTextArea
a80fa14bccb8 more Isabelle/jEdit actions;
wenzelm
parents: 71709
diff changeset
   521
    val painter = text_area.getPainter
a80fa14bccb8 more Isabelle/jEdit actions;
wenzelm
parents: 71709
diff changeset
   522
    val caret_range = JEdit_Lib.caret_range(text_area)
a80fa14bccb8 more Isabelle/jEdit actions;
wenzelm
parents: 71709
diff changeset
   523
    for {
a80fa14bccb8 more Isabelle/jEdit actions;
wenzelm
parents: 71709
diff changeset
   524
      doc_view <- Document_View.get(text_area)
a80fa14bccb8 more Isabelle/jEdit actions;
wenzelm
parents: 71709
diff changeset
   525
      rendering = doc_view.get_rendering()
a80fa14bccb8 more Isabelle/jEdit actions;
wenzelm
parents: 71709
diff changeset
   526
      tip <- rendering.tooltip(caret_range, control)
a80fa14bccb8 more Isabelle/jEdit actions;
wenzelm
parents: 71709
diff changeset
   527
      loc0 <- Option(text_area.offsetToXY(caret_range.start))
a80fa14bccb8 more Isabelle/jEdit actions;
wenzelm
parents: 71709
diff changeset
   528
    } {
71718
f2a79950748e tuned GUI;
wenzelm
parents: 71716
diff changeset
   529
      val loc = new Point(loc0.x, loc0.y + painter.getLineHeight * 3 / 4)
71711
a80fa14bccb8 more Isabelle/jEdit actions;
wenzelm
parents: 71709
diff changeset
   530
      val results = rendering.snapshot.command_results(tip.range)
a80fa14bccb8 more Isabelle/jEdit actions;
wenzelm
parents: 71709
diff changeset
   531
      Pretty_Tooltip(view, painter, loc, rendering, results, tip)
a80fa14bccb8 more Isabelle/jEdit actions;
wenzelm
parents: 71709
diff changeset
   532
    }
a80fa14bccb8 more Isabelle/jEdit actions;
wenzelm
parents: 71709
diff changeset
   533
  }
71713
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71711
diff changeset
   534
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71711
diff changeset
   535
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71711
diff changeset
   536
  /* error navigation */
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71711
diff changeset
   537
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71711
diff changeset
   538
  private def goto_error(
71716
f61e55bab00c proper navigation wrt. caret;
wenzelm
parents: 71713
diff changeset
   539
    view: View,
f61e55bab00c proper navigation wrt. caret;
wenzelm
parents: 71713
diff changeset
   540
    range: Text.Range,
f61e55bab00c proper navigation wrt. caret;
wenzelm
parents: 71713
diff changeset
   541
    avoid_range: Text.Range = Text.Range.offside,
f61e55bab00c proper navigation wrt. caret;
wenzelm
parents: 71713
diff changeset
   542
    which: String = "")(get: List[Text.Markup] => Option[Text.Markup])
71713
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71711
diff changeset
   543
  {
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71711
diff changeset
   544
    GUI_Thread.require {}
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71711
diff changeset
   545
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71711
diff changeset
   546
    val text_area = view.getTextArea
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71711
diff changeset
   547
    for (doc_view <- Document_View.get(text_area)) {
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71711
diff changeset
   548
      val rendering = doc_view.get_rendering()
71716
f61e55bab00c proper navigation wrt. caret;
wenzelm
parents: 71713
diff changeset
   549
      val errs = rendering.errors(range).filterNot(_.range.overlaps(avoid_range))
f61e55bab00c proper navigation wrt. caret;
wenzelm
parents: 71713
diff changeset
   550
      get(errs) match {
71713
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71711
diff changeset
   551
        case Some(err) =>
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71711
diff changeset
   552
          PIDE.editor.goto_buffer(false, view, view.getBuffer, err.range.start)
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71711
diff changeset
   553
        case None =>
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71711
diff changeset
   554
          view.getStatus.setMessageAndClear("No " + which + "error in current document snapshot")
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71711
diff changeset
   555
      }
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71711
diff changeset
   556
    }
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71711
diff changeset
   557
  }
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71711
diff changeset
   558
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71711
diff changeset
   559
  def goto_first_error(view: View): Unit =
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71711
diff changeset
   560
    goto_error(view, JEdit_Lib.buffer_range(view.getBuffer))(_.headOption)
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71711
diff changeset
   561
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71711
diff changeset
   562
  def goto_last_error(view: View): Unit =
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71711
diff changeset
   563
    goto_error(view, JEdit_Lib.buffer_range(view.getBuffer))(_.lastOption)
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71711
diff changeset
   564
71716
f61e55bab00c proper navigation wrt. caret;
wenzelm
parents: 71713
diff changeset
   565
  def goto_prev_error(view: View)
f61e55bab00c proper navigation wrt. caret;
wenzelm
parents: 71713
diff changeset
   566
  {
f61e55bab00c proper navigation wrt. caret;
wenzelm
parents: 71713
diff changeset
   567
    val caret_range = JEdit_Lib.caret_range(view.getTextArea)
f61e55bab00c proper navigation wrt. caret;
wenzelm
parents: 71713
diff changeset
   568
    val range = Text.Range(0, caret_range.stop)
f61e55bab00c proper navigation wrt. caret;
wenzelm
parents: 71713
diff changeset
   569
    goto_error(view, range, avoid_range = caret_range, which = "previous ")(_.lastOption)
f61e55bab00c proper navigation wrt. caret;
wenzelm
parents: 71713
diff changeset
   570
  }
71713
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 71711
diff changeset
   571
71716
f61e55bab00c proper navigation wrt. caret;
wenzelm
parents: 71713
diff changeset
   572
  def goto_next_error(view: View)
f61e55bab00c proper navigation wrt. caret;
wenzelm
parents: 71713
diff changeset
   573
  {
f61e55bab00c proper navigation wrt. caret;
wenzelm
parents: 71713
diff changeset
   574
    val caret_range = JEdit_Lib.caret_range(view.getTextArea)
f61e55bab00c proper navigation wrt. caret;
wenzelm
parents: 71713
diff changeset
   575
    val range = Text.Range(caret_range.start, view.getBuffer.getLength)
f61e55bab00c proper navigation wrt. caret;
wenzelm
parents: 71713
diff changeset
   576
    goto_error(view, range, avoid_range = caret_range, which = "next ")(_.headOption)
f61e55bab00c proper navigation wrt. caret;
wenzelm
parents: 71713
diff changeset
   577
  }
71734
62755ec99671 support Java/VM monitoring via jconsole;
wenzelm
parents: 71718
diff changeset
   578
62755ec99671 support Java/VM monitoring via jconsole;
wenzelm
parents: 71718
diff changeset
   579
62755ec99671 support Java/VM monitoring via jconsole;
wenzelm
parents: 71718
diff changeset
   580
  /* jconsole */
62755ec99671 support Java/VM monitoring via jconsole;
wenzelm
parents: 71718
diff changeset
   581
62755ec99671 support Java/VM monitoring via jconsole;
wenzelm
parents: 71718
diff changeset
   582
  def jconsole(view: View) {
62755ec99671 support Java/VM monitoring via jconsole;
wenzelm
parents: 71718
diff changeset
   583
    Future.thread(name = "jconsole", daemon = true) {
62755ec99671 support Java/VM monitoring via jconsole;
wenzelm
parents: 71718
diff changeset
   584
      try { Isabelle_System.jconsole() }
62755ec99671 support Java/VM monitoring via jconsole;
wenzelm
parents: 71718
diff changeset
   585
      catch {
62755ec99671 support Java/VM monitoring via jconsole;
wenzelm
parents: 71718
diff changeset
   586
        case exn: Throwable =>
62755ec99671 support Java/VM monitoring via jconsole;
wenzelm
parents: 71718
diff changeset
   587
          GUI_Thread.later {
62755ec99671 support Java/VM monitoring via jconsole;
wenzelm
parents: 71718
diff changeset
   588
            GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
62755ec99671 support Java/VM monitoring via jconsole;
wenzelm
parents: 71718
diff changeset
   589
          }
62755ec99671 support Java/VM monitoring via jconsole;
wenzelm
parents: 71718
diff changeset
   590
      }
62755ec99671 support Java/VM monitoring via jconsole;
wenzelm
parents: 71718
diff changeset
   591
    }
62755ec99671 support Java/VM monitoring via jconsole;
wenzelm
parents: 71718
diff changeset
   592
  }
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   593
}