src/Pure/GUI/system_dialog.scala
author wenzelm
Wed Jul 23 11:19:24 2014 +0200 (2014-07-23)
changeset 57612 990ffb84489b
parent 56662 f373fb77e0a4
child 59201 702e0971d617
permissions -rw-r--r--
clarified module name: facilitate alternative GUI frameworks;
     1 /*  Title:      Pure/GUI/system_dialog.scala
     2     Author:     Makarius
     3 
     4 Dialog for system processes, with optional output window.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import java.awt.{GraphicsEnvironment, Point, Font}
    11 import javax.swing.WindowConstants
    12 import java.io.{File => JFile, BufferedReader, InputStreamReader}
    13 
    14 import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel,
    15   BorderPanel, Frame, TextArea, Component, Label}
    16 import scala.swing.event.ButtonClicked
    17 
    18 
    19 class System_Dialog extends Build.Progress
    20 {
    21   /* component state -- owned by GUI thread */
    22 
    23   private var _title = "Isabelle"
    24   private var _window: Option[Window] = None
    25   private var _return_code: Option[Int] = None
    26 
    27   private def check_window(): Window =
    28   {
    29     GUI_Thread.require {}
    30 
    31     _window match {
    32       case Some(window) => window
    33       case None =>
    34         val window = new Window
    35         _window = Some(window)
    36 
    37         window.pack()
    38         val point = GraphicsEnvironment.getLocalGraphicsEnvironment().getCenterPoint()
    39         window.location =
    40           new Point(point.x - window.size.width / 2, point.y - window.size.height / 2)
    41         window.visible = true
    42 
    43         window
    44       }
    45   }
    46 
    47   private val result = Future.promise[Int]
    48 
    49   private def conclude()
    50   {
    51     GUI_Thread.require {}
    52     require(_return_code.isDefined)
    53 
    54     _window match {
    55       case None =>
    56       case Some(window) =>
    57         window.visible = false
    58         window.dispose
    59         _window = None
    60     }
    61 
    62     try { result.fulfill(_return_code.get) }
    63     catch { case ERROR(_) => }
    64   }
    65 
    66   def join(): Int = result.join
    67   def join_exit(): Nothing = sys.exit(join)
    68 
    69 
    70   /* window */
    71 
    72   private class Window extends Frame
    73   {
    74     title = _title
    75     peer.setIconImages(GUI.isabelle_images())
    76 
    77 
    78     /* text */
    79 
    80     val text = new TextArea {
    81       font = new Font("SansSerif", Font.PLAIN, GUI.resolution_scale(10) max 14)
    82       editable = false
    83       columns = 50
    84       rows = 20
    85     }
    86 
    87     val scroll_text = new ScrollPane(text)
    88 
    89 
    90     /* layout panel with dynamic actions */
    91 
    92     val action_panel = new FlowPanel(FlowPanel.Alignment.Center)()
    93     val layout_panel = new BorderPanel
    94     layout_panel.layout(scroll_text) = BorderPanel.Position.Center
    95     layout_panel.layout(action_panel) = BorderPanel.Position.South
    96 
    97     contents = layout_panel
    98 
    99     def set_actions(cs: Component*)
   100     {
   101       action_panel.contents.clear
   102       action_panel.contents ++= cs
   103       layout_panel.revalidate
   104       layout_panel.repaint
   105     }
   106 
   107 
   108     /* close */
   109 
   110     peer.setDefaultCloseOperation(WindowConstants.DO_NOTHING_ON_CLOSE)
   111 
   112     override def closeOperation {
   113       if (_return_code.isDefined) conclude()
   114       else stopping()
   115     }
   116 
   117     def stopping()
   118     {
   119       is_stopped = true
   120       set_actions(new Label("Stopping ..."))
   121     }
   122 
   123     val stop_button = new Button("Stop") {
   124       reactions += { case ButtonClicked(_) => stopping() }
   125     }
   126 
   127     var do_auto_close = true
   128     def can_auto_close: Boolean = do_auto_close && _return_code == Some(0)
   129 
   130     val auto_close = new CheckBox("Auto close") {
   131       reactions += {
   132         case ButtonClicked(_) => do_auto_close = this.selected
   133         if (can_auto_close) conclude()
   134       }
   135     }
   136     auto_close.selected = do_auto_close
   137     auto_close.tooltip = "Automatically close dialog when finished"
   138 
   139     set_actions(stop_button, auto_close)
   140 
   141 
   142     /* exit */
   143 
   144     val delay_exit =
   145       GUI_Thread.delay_first(Time.seconds(1.0))
   146       {
   147         if (can_auto_close) conclude()
   148         else {
   149           val button =
   150             new Button(if (_return_code == Some(0)) "OK" else "Exit") {
   151               reactions += { case ButtonClicked(_) => conclude() }
   152             }
   153           set_actions(button)
   154           button.peer.getRootPane.setDefaultButton(button.peer)
   155         }
   156       }
   157   }
   158 
   159 
   160   /* progress operations */
   161 
   162   def title(txt: String): Unit =
   163     GUI_Thread.later {
   164       _title = txt
   165       _window.foreach(window => window.title = txt)
   166     }
   167 
   168   def return_code(rc: Int): Unit =
   169     GUI_Thread.later {
   170       _return_code = Some(rc)
   171       _window match {
   172         case None => conclude()
   173         case Some(window) => window.delay_exit.invoke
   174       }
   175     }
   176 
   177   override def echo(txt: String): Unit =
   178     GUI_Thread.later {
   179       val window = check_window()
   180       window.text.append(txt + "\n")
   181       val vertical = window.scroll_text.peer.getVerticalScrollBar
   182       vertical.setValue(vertical.getMaximum)
   183     }
   184 
   185   override def theory(session: String, theory: String): Unit =
   186     echo(session + ": theory " + theory)
   187 
   188   @volatile private var is_stopped = false
   189   override def stopped: Boolean = is_stopped
   190 
   191 
   192   /* system operations */
   193 
   194   def execute(cwd: JFile, env: Map[String, String], args: String*): Int =
   195   {
   196     val proc = Isabelle_System.raw_execute(cwd, env, true, args: _*)
   197     proc.getOutputStream.close
   198 
   199     val stdout = new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset))
   200     try {
   201       var line = stdout.readLine
   202       while (line != null) {
   203         echo(line)
   204         line = stdout.readLine
   205       }
   206     }
   207     finally { stdout.close }
   208 
   209     proc.waitFor
   210   }
   211 }
   212