src/Tools/jEdit/src/document_dockable.scala
author wenzelm
Thu, 10 Nov 2022 12:21:44 +0100
changeset 76504 15b058bb2416
parent 76494 9686049ce988
child 76562 9c5780693350
permissions -rw-r--r--
clarified signature: ensure that entries are well-formed --- no consecutive separators, no separators at start/end;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
75816
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
     1
/*  Title:      Tools/jEdit/src/document_dockable.scala
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
     3
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
     4
Dockable window for document build support.
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
     5
*/
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
     6
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
     8
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
     9
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
    10
import isabelle._
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
    11
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
    12
import java.awt.BorderLayout
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
    13
import java.awt.event.{ComponentEvent, ComponentAdapter}
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
    14
76023
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
    15
import scala.swing.{ScrollPane, TextArea, Label, TabbedPane, BorderPanel, Component}
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
    16
75816
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
    17
import org.gjt.sp.jedit.{jEdit, View}
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
    18
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
    19
76023
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
    20
object Document_Dockable {
76491
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    21
  /* document output */
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    22
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    23
  def document_name: String = "document"
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    24
  def document_output_dir(): Path = Path.explode("$ISABELLE_HOME_USER/document_output")
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    25
  def document_output(): Path = document_output_dir() + Path.basic(document_name)
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    26
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    27
  def view_document(): Unit = {
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    28
    val path = Document_Dockable.document_output().pdf
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    29
    if (path.is_file) Isabelle_System.pdf_viewer(path)
76490
deded566d423 clarified file names;
wenzelm
parents: 76489
diff changeset
    30
  }
76023
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
    31
76491
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    32
  class Log_Progress extends Progress {
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    33
    def show(text: String): Unit = {}
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    34
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    35
    private val syslog = PIDE.session.make_syslog()
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    36
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    37
    private def update(text: String = syslog.content()): Unit = GUI_Thread.require { show(text) }
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    38
    private val delay =
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    39
      Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { update() }
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    40
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    41
    override def echo(msg: String): Unit = { syslog += msg; delay.invoke() }
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    42
    override def theory(theory: Progress.Theory): Unit = echo(theory.message)
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    43
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    44
    def load(): Unit = {
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    45
      val path = document_output().log
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    46
      val text = if (path.is_file) File.read(path) else ""
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    47
      GUI_Thread.later { delay.revoke(); update(text) }
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    48
    }
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    49
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    50
    update()
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    51
  }
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    52
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    53
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    54
  /* state */
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    55
76023
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
    56
  object Status extends Enumeration {
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
    57
    val WAITING = Value("waiting")
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
    58
    val RUNNING = Value("running")
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
    59
    val FINISHED = Value("finished")
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
    60
  }
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
    61
76026
614a8feea80c clarified GUI update;
wenzelm
parents: 76025
diff changeset
    62
  sealed case class Result(output: List[XML.Tree] = Nil) {
614a8feea80c clarified GUI update;
wenzelm
parents: 76025
diff changeset
    63
    def failed: Boolean = output.exists(Protocol.is_error)
614a8feea80c clarified GUI update;
wenzelm
parents: 76025
diff changeset
    64
  }
76023
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
    65
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
    66
  object State {
76491
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    67
    def empty(): State = State()
76026
614a8feea80c clarified GUI update;
wenzelm
parents: 76025
diff changeset
    68
    def finish(result: Result): State = State(output = result.output)
76023
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
    69
  }
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
    70
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
    71
  sealed case class State(
76491
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    72
    progress: Log_Progress = new Log_Progress,
76023
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
    73
    process: Future[Unit] = Future.value(()),
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
    74
    output: List[XML.Tree] = Nil,
76491
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    75
    status: Status.Value = Status.FINISHED)
76023
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
    76
}
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
    77
75816
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
    78
class Document_Dockable(view: View, position: String) extends Dockable(view, position) {
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
    79
  GUI_Thread.require {}
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
    80
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
    81
76023
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
    82
  /* component state -- owned by GUI thread */
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
    83
76491
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
    84
  private val current_state = Synchronized(Document_Dockable.State.empty())
76023
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
    85
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
    86
  private val process_indicator = new Process_Indicator
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
    87
  private val pretty_text_area = new Pretty_Text_Area(view)
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
    88
  private val message_pane = new TabbedPane
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
    89
76034
dda3c117f13c clarified GUI behaviour;
wenzelm
parents: 76026
diff changeset
    90
  private def show_state(): Unit = GUI_Thread.later {
76023
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
    91
    val st = current_state.value
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
    92
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
    93
    pretty_text_area.update(Document.Snapshot.init, Command.Results.empty, st.output)
75816
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
    94
76023
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
    95
    st.status match {
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
    96
      case Document_Dockable.Status.WAITING =>
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
    97
        process_indicator.update("Waiting for PIDE document content ...", 5)
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
    98
      case Document_Dockable.Status.RUNNING =>
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
    99
        process_indicator.update("Running document build process ...", 15)
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   100
      case Document_Dockable.Status.FINISHED =>
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   101
        process_indicator.update(null, 0)
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   102
    }
76034
dda3c117f13c clarified GUI behaviour;
wenzelm
parents: 76026
diff changeset
   103
  }
76023
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   104
76034
dda3c117f13c clarified GUI behaviour;
wenzelm
parents: 76026
diff changeset
   105
  private def show_page(page: TabbedPane.Page): Unit = GUI_Thread.later {
dda3c117f13c clarified GUI behaviour;
wenzelm
parents: 76026
diff changeset
   106
    message_pane.selection.page = page
76023
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   107
  }
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   108
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   109
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   110
  /* text area with zoom/resize */
75816
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   111
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   112
  override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   113
76021
752425c69577 clarified component structure, concerning initialization order;
wenzelm
parents: 75853
diff changeset
   114
  private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() }
752425c69577 clarified component structure, concerning initialization order;
wenzelm
parents: 75853
diff changeset
   115
  private def handle_resize(): Unit = GUI_Thread.require { pretty_text_area.zoom(zoom) }
752425c69577 clarified component structure, concerning initialization order;
wenzelm
parents: 75853
diff changeset
   116
752425c69577 clarified component structure, concerning initialization order;
wenzelm
parents: 75853
diff changeset
   117
  private val delay_resize: Delay =
752425c69577 clarified component structure, concerning initialization order;
wenzelm
parents: 75853
diff changeset
   118
    Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
752425c69577 clarified component structure, concerning initialization order;
wenzelm
parents: 75853
diff changeset
   119
752425c69577 clarified component structure, concerning initialization order;
wenzelm
parents: 75853
diff changeset
   120
  addComponentListener(new ComponentAdapter {
752425c69577 clarified component structure, concerning initialization order;
wenzelm
parents: 75853
diff changeset
   121
    override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
752425c69577 clarified component structure, concerning initialization order;
wenzelm
parents: 75853
diff changeset
   122
    override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
752425c69577 clarified component structure, concerning initialization order;
wenzelm
parents: 75853
diff changeset
   123
  })
752425c69577 clarified component structure, concerning initialization order;
wenzelm
parents: 75853
diff changeset
   124
76023
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   125
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   126
  /* progress log */
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   127
76489
8c9830109ab2 clarified Log_Progress vs. GUI: more like Syslog_Dockable;
wenzelm
parents: 76036
diff changeset
   128
  private val log_area =
8c9830109ab2 clarified Log_Progress vs. GUI: more like Syslog_Dockable;
wenzelm
parents: 76036
diff changeset
   129
    new TextArea {
8c9830109ab2 clarified Log_Progress vs. GUI: more like Syslog_Dockable;
wenzelm
parents: 76036
diff changeset
   130
      editable = false
8c9830109ab2 clarified Log_Progress vs. GUI: more like Syslog_Dockable;
wenzelm
parents: 76036
diff changeset
   131
      font = GUI.copy_font((new Label).font)
8c9830109ab2 clarified Log_Progress vs. GUI: more like Syslog_Dockable;
wenzelm
parents: 76036
diff changeset
   132
    }
76023
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   133
  private val scroll_log_area = new ScrollPane(log_area)
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   134
76491
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
   135
  def init_progress(): Document_Dockable.Log_Progress =
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
   136
    new Document_Dockable.Log_Progress {
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
   137
      override def show(text: String): Unit =
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
   138
        if (text != log_area.text) {
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
   139
          log_area.text = text
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
   140
          val vertical = scroll_log_area.peer.getVerticalScrollBar
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
   141
          vertical.setValue(vertical.getMaximum)
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
   142
        }
76023
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   143
    }
76021
752425c69577 clarified component structure, concerning initialization order;
wenzelm
parents: 75853
diff changeset
   144
75816
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   145
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   146
  /* document build process */
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   147
76023
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   148
  private def cancel(): Unit =
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   149
    current_state.change { st => st.process.cancel(); st }
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   150
76491
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
   151
  private def init_state(): Unit =
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
   152
    current_state.change { _ => Document_Dockable.State(progress = init_progress()) }
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
   153
76023
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   154
  private def build_document(): Unit = {
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   155
    current_state.change { st =>
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   156
      if (st.process.is_finished) {
76491
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
   157
        val progress = init_progress()
76023
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   158
        val process =
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   159
          Future.thread[Unit](name = "document_build") {
76034
dda3c117f13c clarified GUI behaviour;
wenzelm
parents: 76026
diff changeset
   160
            show_page(log_page)
76023
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   161
            val res =
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   162
              Exn.capture {
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   163
                progress.echo("Start " + Date.now())
76489
8c9830109ab2 clarified Log_Progress vs. GUI: more like Syslog_Dockable;
wenzelm
parents: 76036
diff changeset
   164
                for (i <- 1 to 200) {
8c9830109ab2 clarified Log_Progress vs. GUI: more like Syslog_Dockable;
wenzelm
parents: 76036
diff changeset
   165
                  progress.echo("message " + i)
8c9830109ab2 clarified Log_Progress vs. GUI: more like Syslog_Dockable;
wenzelm
parents: 76036
diff changeset
   166
                  Time.seconds(0.1).sleep()
8c9830109ab2 clarified Log_Progress vs. GUI: more like Syslog_Dockable;
wenzelm
parents: 76036
diff changeset
   167
                }
76023
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   168
                progress.echo("Stop " + Date.now())
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   169
              }
76026
614a8feea80c clarified GUI update;
wenzelm
parents: 76025
diff changeset
   170
            val msg =
76023
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   171
              res match {
76026
614a8feea80c clarified GUI update;
wenzelm
parents: 76025
diff changeset
   172
                case Exn.Res(_) => Protocol.make_message(XML.string("OK"))
614a8feea80c clarified GUI update;
wenzelm
parents: 76025
diff changeset
   173
                case Exn.Exn(exn) => Protocol.error_message(XML.string(Exn.message(exn)))
76023
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   174
              }
76026
614a8feea80c clarified GUI update;
wenzelm
parents: 76025
diff changeset
   175
            val result = Document_Dockable.Result(output = List(msg))
76035
wenzelm
parents: 76034
diff changeset
   176
            current_state.change(_ => Document_Dockable.State.finish(result))
wenzelm
parents: 76034
diff changeset
   177
            show_state()
wenzelm
parents: 76034
diff changeset
   178
            show_page(output_page)
76023
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   179
          }
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   180
        st.copy(progress = progress, process = process, status = Document_Dockable.Status.RUNNING)
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   181
      }
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   182
      else st
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   183
    }
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   184
    show_state()
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   185
  }
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   186
75816
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   187
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   188
  /* controls */
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   189
76492
e228be7cd375 clarified GUI.Selector, with support for separator as pseudo-entry;
wenzelm
parents: 76491
diff changeset
   190
  private val document_session: GUI.Selector[String] = {
e228be7cd375 clarified GUI.Selector, with support for separator as pseudo-entry;
wenzelm
parents: 76491
diff changeset
   191
    val sessions = JEdit_Sessions.sessions_structure()
e228be7cd375 clarified GUI.Selector, with support for separator as pseudo-entry;
wenzelm
parents: 76491
diff changeset
   192
    val all_sessions = sessions.build_topological_order.sorted
e228be7cd375 clarified GUI.Selector, with support for separator as pseudo-entry;
wenzelm
parents: 76491
diff changeset
   193
    val doc_sessions = all_sessions.filter(name => sessions(name).doc_group)
76504
15b058bb2416 clarified signature: ensure that entries are well-formed --- no consecutive separators, no separators at start/end;
wenzelm
parents: 76494
diff changeset
   194
    new GUI.Selector[String](
15b058bb2416 clarified signature: ensure that entries are well-formed --- no consecutive separators, no separators at start/end;
wenzelm
parents: 76494
diff changeset
   195
      doc_sessions.map(GUI.Selector.item),
15b058bb2416 clarified signature: ensure that entries are well-formed --- no consecutive separators, no separators at start/end;
wenzelm
parents: 76494
diff changeset
   196
      all_sessions.map(GUI.Selector.item)
76492
e228be7cd375 clarified GUI.Selector, with support for separator as pseudo-entry;
wenzelm
parents: 76491
diff changeset
   197
    ) {
75830
b054f22efd0d more GUI elements;
wenzelm
parents: 75816
diff changeset
   198
      val title = "Session"
b054f22efd0d more GUI elements;
wenzelm
parents: 75816
diff changeset
   199
    }
76492
e228be7cd375 clarified GUI.Selector, with support for separator as pseudo-entry;
wenzelm
parents: 76491
diff changeset
   200
  }
75830
b054f22efd0d more GUI elements;
wenzelm
parents: 75816
diff changeset
   201
75853
f981111768ec clarified signature;
wenzelm
parents: 75839
diff changeset
   202
  private val build_button =
f981111768ec clarified signature;
wenzelm
parents: 75839
diff changeset
   203
    new GUI.Button("<html><b>Build</b></html>") {
75816
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   204
      tooltip = "Build document"
76023
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   205
      override def clicked(): Unit = build_document()
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   206
    }
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   207
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   208
  private val cancel_button =
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   209
    new GUI.Button("Cancel") {
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   210
      tooltip = "Cancel build process"
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   211
      override def clicked(): Unit = cancel()
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   212
    }
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   213
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   214
  private val view_button =
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   215
    new GUI.Button("View") {
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   216
      tooltip = "View document"
76491
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
   217
      override def clicked(): Unit = Document_Dockable.view_document()
75816
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   218
    }
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   219
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   220
  private val controls =
75830
b054f22efd0d more GUI elements;
wenzelm
parents: 75816
diff changeset
   221
    Wrap_Panel(List(document_session, process_indicator.component, build_button,
76023
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   222
      view_button, cancel_button))
75816
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   223
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   224
  add(controls.peer, BorderLayout.NORTH)
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   225
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   226
  override def focusOnDefaultComponent(): Unit = build_button.requestFocus()
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   227
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   228
76023
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   229
  /* message pane with pages */
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   230
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   231
  private val output_controls =
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   232
    Wrap_Panel(List(pretty_text_area.search_label, pretty_text_area.search_field, zoom))
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   233
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   234
  private val output_page =
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   235
    new TabbedPane.Page("Output", new BorderPanel {
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   236
      layout(output_controls) = BorderPanel.Position.North
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   237
      layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   238
    }, "Output from build process")
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   239
76491
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
   240
  private val load_button =
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
   241
    new GUI.Button("Load") {
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
   242
      tooltip = "Load final log file"
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
   243
      override def clicked(): Unit = current_state.value.progress.load()
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
   244
    }
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
   245
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
   246
  private val log_controls =
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
   247
    Wrap_Panel(List(load_button))
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
   248
76023
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   249
  private val log_page =
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   250
    new TabbedPane.Page("Log", new BorderPanel {
76491
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
   251
      layout(log_controls) = BorderPanel.Position.North
76489
8c9830109ab2 clarified Log_Progress vs. GUI: more like Syslog_Dockable;
wenzelm
parents: 76036
diff changeset
   252
      layout(scroll_log_area) = BorderPanel.Position.Center
76023
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   253
    }, "Raw log of build process")
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   254
76036
181bf8567f41 tuned GUI;
wenzelm
parents: 76035
diff changeset
   255
  message_pane.pages ++= List(log_page, output_page)
76023
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   256
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   257
  set_content(message_pane)
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   258
c7fed2fd52f5 more GUI functionality;
wenzelm
parents: 76021
diff changeset
   259
75816
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   260
  /* main */
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   261
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   262
  private val main =
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   263
    Session.Consumer[Session.Global_Options](getClass.getName) {
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   264
      case _: Session.Global_Options =>
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   265
        GUI_Thread.later { handle_resize() }
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   266
    }
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   267
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   268
  override def init(): Unit = {
76491
2c37c10d6884 clarified GUI state;
wenzelm
parents: 76490
diff changeset
   269
    init_state()
75816
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   270
    PIDE.session.global_options += main
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   271
    handle_resize()
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   272
  }
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   273
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   274
  override def exit(): Unit = {
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   275
    PIDE.session.global_options -= main
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   276
    delay_resize.revoke()
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   277
  }
91f02f224b80 basic setup for document build panel;
wenzelm
parents:
diff changeset
   278
}