src/Tools/jEdit/src/output_dockable.scala
author wenzelm
Sat, 13 Aug 2022 21:23:59 +0200
changeset 75849 dfedac6525d4
parent 75847 93436389db1c
child 75852 fcc25bb49def
permissions -rw-r--r--
clarified modules;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
49494
cbcccf2a0f6f renamed Output to Output1 and Output2 to Output, and thus make the new version the default;
wenzelm
parents: 49473
diff changeset
     1
/*  Title:      Tools/jEdit/src/output_dockable.scala
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
     3
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
     4
Dockable window with result message output.
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
     5
*/
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
     6
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
     8
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
     9
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    10
import isabelle._
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    11
53711
8ce7795256e1 improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents: 53177
diff changeset
    12
import scala.swing.{Button, CheckBox}
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    13
import scala.swing.event.ButtonClicked
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    14
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    15
import java.awt.BorderLayout
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    16
import java.awt.event.{ComponentEvent, ComponentAdapter}
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    17
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    18
import org.gjt.sp.jedit.View
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    19
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    20
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73987
diff changeset
    21
class Output_Dockable(view: View, position: String) extends Dockable(view, position) {
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 57044
diff changeset
    22
  /* component state -- owned by GUI thread */
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    23
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    24
  private var do_update = true
49415
8b402b550a80 proper separation of output messages;
wenzelm
parents: 49414
diff changeset
    25
  private var current_output: List[XML.Tree] = Nil
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    26
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    27
49726
2074197dc274 detach tooltip as dockable window;
wenzelm
parents: 49701
diff changeset
    28
  /* pretty text area */
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    29
50541
021f054ff1fa tuned signature;
wenzelm
parents: 50501
diff changeset
    30
  val pretty_text_area = new Pretty_Text_Area(view)
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    31
  set_content(pretty_text_area)
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    32
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 66591
diff changeset
    33
  override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
56906
408b526911f7 some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
wenzelm
parents: 56886
diff changeset
    34
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    35
75812
d6e8d12494be clarified signature;
wenzelm
parents: 75810
diff changeset
    36
  private def handle_resize(): Unit =
75839
29441f2bfe81 clarified signature: more explicit types;
wenzelm
parents: 75833
diff changeset
    37
    GUI_Thread.require { pretty_text_area.zoom(zoom) }
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    38
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73987
diff changeset
    39
  private def handle_update(follow: Boolean, restriction: Option[Set[Command]]): Unit = {
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 57044
diff changeset
    40
    GUI_Thread.require {}
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    41
65194
6dabae94cf57 misc tuning and simplification;
wenzelm
parents: 65190
diff changeset
    42
    for {
66082
2d12a730a380 clarified modules;
wenzelm
parents: 65246
diff changeset
    43
      snapshot <- PIDE.editor.current_node_snapshot(view)
65194
6dabae94cf57 misc tuning and simplification;
wenzelm
parents: 65190
diff changeset
    44
      if follow && !snapshot.is_outdated
6dabae94cf57 misc tuning and simplification;
wenzelm
parents: 65190
diff changeset
    45
    } {
6dabae94cf57 misc tuning and simplification;
wenzelm
parents: 65190
diff changeset
    46
      val (command, results) =
66082
2d12a730a380 clarified modules;
wenzelm
parents: 65246
diff changeset
    47
        PIDE.editor.current_command(view, snapshot) match {
65195
wenzelm
parents: 65194
diff changeset
    48
          case Some(command) => (command, snapshot.command_results(command))
65194
6dabae94cf57 misc tuning and simplification;
wenzelm
parents: 65190
diff changeset
    49
          case None => (Command.empty, Command.Results.empty)
6dabae94cf57 misc tuning and simplification;
wenzelm
parents: 65190
diff changeset
    50
        }
6dabae94cf57 misc tuning and simplification;
wenzelm
parents: 65190
diff changeset
    51
6dabae94cf57 misc tuning and simplification;
wenzelm
parents: 65190
diff changeset
    52
      val new_output =
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 66591
diff changeset
    53
        if (restriction.isEmpty || restriction.get.contains(command))
75849
dfedac6525d4 clarified modules;
wenzelm
parents: 75847
diff changeset
    54
          Rendering.output_messages(results, JEdit_Options.output_state())
65194
6dabae94cf57 misc tuning and simplification;
wenzelm
parents: 65190
diff changeset
    55
        else current_output
6dabae94cf57 misc tuning and simplification;
wenzelm
parents: 65190
diff changeset
    56
6dabae94cf57 misc tuning and simplification;
wenzelm
parents: 65190
diff changeset
    57
      if (current_output != new_output) {
6dabae94cf57 misc tuning and simplification;
wenzelm
parents: 65190
diff changeset
    58
        pretty_text_area.update(snapshot, results, Pretty.separate(new_output))
6dabae94cf57 misc tuning and simplification;
wenzelm
parents: 65190
diff changeset
    59
        current_output = new_output
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    60
      }
65194
6dabae94cf57 misc tuning and simplification;
wenzelm
parents: 65190
diff changeset
    61
    }
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    62
  }
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    63
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    64
61205
wenzelm
parents: 60750
diff changeset
    65
  /* controls */
wenzelm
parents: 60750
diff changeset
    66
75849
dfedac6525d4 clarified modules;
wenzelm
parents: 75847
diff changeset
    67
  private val output_state_button = new JEdit_Options.output_state.GUI
61717
5922db0430f1 more direct access to option "editor_output_state";
wenzelm
parents: 61205
diff changeset
    68
5922db0430f1 more direct access to option "editor_output_state";
wenzelm
parents: 61205
diff changeset
    69
  private val auto_update_button = new CheckBox("Auto update") {
61205
wenzelm
parents: 60750
diff changeset
    70
    tooltip = "Indicate automatic update following cursor movement"
wenzelm
parents: 60750
diff changeset
    71
    reactions += {
75833
8ffbd9343e91 tuned whitespace;
wenzelm
parents: 75812
diff changeset
    72
      case ButtonClicked(_) => do_update = this.selected; handle_update(do_update, None)
8ffbd9343e91 tuned whitespace;
wenzelm
parents: 75812
diff changeset
    73
    }
61205
wenzelm
parents: 60750
diff changeset
    74
    selected = do_update
wenzelm
parents: 60750
diff changeset
    75
  }
wenzelm
parents: 60750
diff changeset
    76
61717
5922db0430f1 more direct access to option "editor_output_state";
wenzelm
parents: 61205
diff changeset
    77
  private val update_button = new Button("Update") {
61205
wenzelm
parents: 60750
diff changeset
    78
    tooltip = "Update display according to the command at cursor position"
wenzelm
parents: 60750
diff changeset
    79
    reactions += { case ButtonClicked(_) => handle_update(true, None) }
wenzelm
parents: 60750
diff changeset
    80
  }
wenzelm
parents: 60750
diff changeset
    81
75839
29441f2bfe81 clarified signature: more explicit types;
wenzelm
parents: 75833
diff changeset
    82
  private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() }
61205
wenzelm
parents: 60750
diff changeset
    83
wenzelm
parents: 60750
diff changeset
    84
  private val controls =
66205
e9fa94f43a15 tuned signature;
wenzelm
parents: 66084
diff changeset
    85
    Wrap_Panel(
e9fa94f43a15 tuned signature;
wenzelm
parents: 66084
diff changeset
    86
      List(output_state_button, auto_update_button,
66206
2d2082db735a clarified defaults;
wenzelm
parents: 66205
diff changeset
    87
        update_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom))
66205
e9fa94f43a15 tuned signature;
wenzelm
parents: 66084
diff changeset
    88
61205
wenzelm
parents: 60750
diff changeset
    89
  add(controls.peer, BorderLayout.NORTH)
wenzelm
parents: 60750
diff changeset
    90
wenzelm
parents: 60750
diff changeset
    91
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
    92
  /* main */
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
    93
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
    94
  private val main =
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
    95
    Session.Consumer[Any](getClass.getName) {
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
    96
      case _: Session.Global_Options =>
61717
5922db0430f1 more direct access to option "editor_output_state";
wenzelm
parents: 61205
diff changeset
    97
        GUI_Thread.later {
62259
7afbd7fc32fd recovered handle_resize from 5922db0430f1;
wenzelm
parents: 61728
diff changeset
    98
          handle_resize()
75847
93436389db1c clarified signature: more explicit types;
wenzelm
parents: 75840
diff changeset
    99
          output_state_button.load()
61717
5922db0430f1 more direct access to option "editor_output_state";
wenzelm
parents: 61205
diff changeset
   100
          handle_update(do_update, None)
5922db0430f1 more direct access to option "editor_output_state";
wenzelm
parents: 61205
diff changeset
   101
        }
53177
dcac8d837b9c more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents: 52978
diff changeset
   102
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   103
      case changed: Session.Commands_Changed =>
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   104
        val restriction = if (changed.assignment) None else Some(changed.commands)
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 57044
diff changeset
   105
        GUI_Thread.later { handle_update(do_update, restriction) }
53177
dcac8d837b9c more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents: 52978
diff changeset
   106
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   107
      case Session.Caret_Focus =>
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 57044
diff changeset
   108
        GUI_Thread.later { handle_update(do_update, None) }
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   109
    }
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   110
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73987
diff changeset
   111
  override def init(): Unit = {
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   112
    PIDE.session.global_options += main
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   113
    PIDE.session.commands_changed += main
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   114
    PIDE.session.caret_focus += main
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   115
    handle_update(true, None)
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   116
  }
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   117
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73987
diff changeset
   118
  override def exit(): Unit = {
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   119
    PIDE.session.global_options -= main
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   120
    PIDE.session.commands_changed -= main
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   121
    PIDE.session.caret_focus -= main
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   122
    delay_resize.revoke()
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   123
  }
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   124
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   125
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   126
  /* resize */
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   127
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   128
  private val delay_resize =
71704
b9a5eb0f3b43 clarified modules;
wenzelm
parents: 71601
diff changeset
   129
    Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   130
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   131
  addComponentListener(new ComponentAdapter {
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 71704
diff changeset
   132
    override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 71704
diff changeset
   133
    override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
49398
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   134
  })
0fa4389c04f9 alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff changeset
   135
}