src/Tools/jEdit/src/session_build.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 62973 744266e32612
child 65256 c3d6dd17d626
permissions -rw-r--r--
tuned signature;
     1 /*  Title:      Tools/jEdit/src/session_build.scala
     2     Author:     Makarius
     3 
     4 Session build management.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import java.awt.event.{WindowEvent, WindowAdapter}
    13 import javax.swing.{WindowConstants, JDialog}
    14 
    15 import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel,
    16   BorderPanel, TextArea, Component, Label}
    17 import scala.swing.event.ButtonClicked
    18 
    19 import org.gjt.sp.jedit.View
    20 
    21 
    22 object Session_Build
    23 {
    24   def session_build(view: View)
    25   {
    26     GUI_Thread.require {}
    27 
    28     try {
    29       if (JEdit_Sessions.session_build_mode() == "none" ||
    30           JEdit_Sessions.session_build(no_build = true) == 0) JEdit_Sessions.session_start()
    31       else new Dialog(view)
    32     }
    33     catch {
    34       case exn: Throwable =>
    35         GUI.dialog(view, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
    36     }
    37   }
    38 
    39   private class Dialog(view: View) extends JDialog(view)
    40   {
    41     /* text */
    42 
    43     private val text = new TextArea {
    44       editable = false
    45       columns = 65
    46       rows = 24
    47     }
    48     text.font = GUI.copy_font((new Label).font)
    49 
    50     private val scroll_text = new ScrollPane(text)
    51 
    52 
    53     /* progress */
    54 
    55     @volatile private var is_stopped = false
    56 
    57     private val progress = new Progress {
    58       override def echo(txt: String): Unit =
    59         GUI_Thread.later {
    60           text.append(txt + "\n")
    61           val vertical = scroll_text.peer.getVerticalScrollBar
    62           vertical.setValue(vertical.getMaximum)
    63         }
    64 
    65       override def theory(session: String, theory: String): Unit =
    66         echo(session + ": theory " + theory)
    67 
    68       override def stopped: Boolean = is_stopped
    69     }
    70 
    71 
    72     /* layout panel with dynamic actions */
    73 
    74     private val action_panel = new FlowPanel(FlowPanel.Alignment.Center)()
    75     private val layout_panel = new BorderPanel
    76     layout_panel.layout(scroll_text) = BorderPanel.Position.Center
    77     layout_panel.layout(action_panel) = BorderPanel.Position.South
    78 
    79     setContentPane(layout_panel.peer)
    80 
    81     private def set_actions(cs: Component*)
    82     {
    83       action_panel.contents.clear
    84       action_panel.contents ++= cs
    85       layout_panel.revalidate
    86       layout_panel.repaint
    87     }
    88 
    89 
    90     /* return code and exit */
    91 
    92     private var _return_code: Option[Int] = None
    93 
    94     private def return_code(rc: Int): Unit =
    95       GUI_Thread.later {
    96         _return_code = Some(rc)
    97         delay_exit.invoke
    98       }
    99 
   100     private val delay_exit =
   101       GUI_Thread.delay_first(Time.seconds(1.0))
   102       {
   103         if (can_auto_close) conclude()
   104         else {
   105           val button = new Button("Close") { reactions += { case ButtonClicked(_) => conclude() } }
   106           set_actions(button)
   107           button.peer.getRootPane.setDefaultButton(button.peer)
   108         }
   109       }
   110 
   111     private def conclude()
   112     {
   113       setVisible(false)
   114       dispose()
   115     }
   116 
   117 
   118     /* close */
   119 
   120     setDefaultCloseOperation(WindowConstants.DO_NOTHING_ON_CLOSE)
   121 
   122     addWindowListener(new WindowAdapter {
   123       override def windowClosing(e: WindowEvent) {
   124         if (_return_code.isDefined) conclude()
   125         else stopping()
   126       }
   127     })
   128 
   129     private def stopping()
   130     {
   131       is_stopped = true
   132       set_actions(new Label("Stopping ..."))
   133     }
   134 
   135     private val stop_button = new Button("Stop") {
   136       reactions += { case ButtonClicked(_) => stopping() }
   137     }
   138 
   139     private var do_auto_close = true
   140     private def can_auto_close: Boolean = do_auto_close && _return_code == Some(0)
   141 
   142     private val auto_close = new CheckBox("Auto close") {
   143       reactions += {
   144         case ButtonClicked(_) => do_auto_close = this.selected
   145         if (can_auto_close) conclude()
   146       }
   147     }
   148     auto_close.selected = do_auto_close
   149     auto_close.tooltip = "Automatically close dialog when finished"
   150 
   151     set_actions(stop_button, auto_close)
   152 
   153 
   154     /* main */
   155 
   156     setTitle("Isabelle build (" +
   157       Isabelle_System.getenv("ML_IDENTIFIER") + " / " +
   158       "jdk-" + Platform.jvm_version + "_" + Platform.jvm_platform + ")")
   159 
   160     pack()
   161     setLocationRelativeTo(view)
   162     setVisible(true)
   163 
   164     Standard_Thread.fork("session_build") {
   165       progress.echo("Build started for Isabelle/" + JEdit_Sessions.session_name() + " ...")
   166 
   167       val (out, rc) =
   168         try { ("", JEdit_Sessions.session_build(progress = progress)) }
   169         catch {
   170           case exn: Throwable =>
   171             (Output.error_text(Exn.message(exn)) + "\n", Exn.return_code(exn, 2))
   172         }
   173 
   174       progress.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))
   175 
   176       if (rc == 0) JEdit_Sessions.session_start()
   177       else progress.echo("Session build failed -- prover process remains inactive!")
   178 
   179       return_code(rc)
   180     }
   181   }
   182 }