--- a/src/Pure/System/cygwin_init.scala Sat Sep 07 16:33:10 2013 +0200
+++ b/src/Pure/System/cygwin_init.scala Sat Sep 07 17:11:44 2013 +0200
@@ -1,107 +1,24 @@
/* Title: Pure/System/cygwin_init.scala
Author: Makarius
-Initialize Isabelle distribution after extracting via 7zip.
+Initialize raw Isabelle distribution (e.g. after extraction via 7zip).
*/
package isabelle
import java.io.{File => JFile, BufferedReader, InputStreamReader}
-import java.nio.file.{Paths, Files}
-import java.awt.{GraphicsEnvironment, Point, Font}
-import javax.swing.ImageIcon
+import java.nio.file.Files
import scala.annotation.tailrec
-import scala.swing.{ScrollPane, Button, FlowPanel,
- BorderPanel, MainFrame, TextArea, SwingApplication}
-import scala.swing.event.ButtonClicked
object Cygwin_Init
{
- /* main GUI entry point */
-
- def main_frame(isabelle_home: String, continue: Int => Unit) = new MainFrame
+ def filesystem(system_dialog: System_Dialog, isabelle_home: String)
{
- title = "Isabelle system initialization"
- iconImage = GUI.isabelle_image()
-
- val layout_panel = new BorderPanel
- contents = layout_panel
-
-
- /* text area */
-
- def echo(msg: String) { text_area.append(msg + "\n") }
-
- val text_area = new TextArea {
- font = new Font("SansSerif", Font.PLAIN, GUI.resolution_scale(10) max 14)
- editable = false
- columns = 50
- rows = 15
- }
-
- layout_panel.layout(new ScrollPane(text_area)) = BorderPanel.Position.Center
-
-
- /* exit button */
-
- var _return_code: Option[Int] = None
- def maybe_exit()
- {
- _return_code match {
- case None =>
- case Some(rc) =>
- visible = false
- continue(rc)
- }
- }
-
- def return_code(rc: Int): Unit =
- Swing_Thread.later {
- _return_code = Some(rc)
- button.peer.getRootPane.setDefaultButton(button.peer)
- layout_panel.repaint
- }
-
- override def closeOperation { maybe_exit() }
-
- val button = new Button {
- text = "Done"
- reactions += { case ButtonClicked(_) => maybe_exit() }
- }
- val button_panel = new FlowPanel(FlowPanel.Alignment.Center)(button)
-
- layout_panel.layout(button_panel) = BorderPanel.Position.South
-
-
- /* show window */
-
- pack()
- val point = GraphicsEnvironment.getLocalGraphicsEnvironment().getCenterPoint()
- location = new Point(point.x - size.width / 2, point.y - size.height / 2)
- visible = true
-
- default_thread_pool.submit(() =>
- try {
- init_filesystem(isabelle_home, echo)
- return_code(0)
- }
- catch {
- case exn: Throwable =>
- text_area.append("Error:\n" + Exn.message(exn) + "\n")
- return_code(2)
- }
- )
- }
-
-
- /* init Cygwin file-system */
-
- private def init_filesystem(isabelle_home: String, echo: String => Unit)
- {
- val cygwin_root = isabelle_home + "\\contrib\\cygwin"
+ system_dialog.title("Isabelle system initialization")
+ system_dialog.echo("Initializing Cygwin:")
def execute(args: String*): Int =
{
@@ -114,7 +31,7 @@
try {
var line = stdout.readLine
while (line != null) {
- echo(line)
+ system_dialog.echo(line)
line = stdout.readLine
}
}
@@ -123,9 +40,9 @@
proc.waitFor
}
- echo("Initializing Cygwin:")
+ val cygwin_root = isabelle_home + "\\contrib\\cygwin"
- echo("symlinks ...")
+ system_dialog.echo("symlinks ...")
val symlinks =
{
val path = (new JFile(cygwin_root + "\\isabelle\\symlinks")).toPath
@@ -150,15 +67,15 @@
}
recover_symlinks(symlinks)
- echo("rebaseall ...")
+ system_dialog.echo("rebaseall ...")
execute(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall")
- echo("postinstall ...")
+ system_dialog.echo("postinstall ...")
execute(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall")
- echo("init ...")
+ system_dialog.echo("init ...")
Isabelle_System.init()
- echo("OK")
+ system_dialog.echo("OK")
}
}
--- a/src/Pure/Tools/main.scala Sat Sep 07 16:33:10 2013 +0200
+++ b/src/Pure/Tools/main.scala Sat Sep 07 17:11:44 2013 +0200
@@ -14,14 +14,6 @@
object Main
{
- private def continue(body: => Unit)(rc: Int)
- {
- if (rc != 0) sys.exit(rc)
- else if (SwingUtilities.isEventDispatchThread())
- Simple_Thread.fork("Isabelle") { body }
- else body
- }
-
def main(args: Array[String])
{
val system_dialog = new System_Dialog
@@ -33,14 +25,6 @@
sys.exit(system_dialog.join)
}
- def run
- {
- build
- val rc = system_dialog.join
- if (rc == 0) start
- else sys.exit(rc)
- }
-
def build
{
try {
@@ -120,39 +104,35 @@
}
if (Platform.is_windows) {
- val init_isabelle_home =
- try {
- GUI.init_laf()
+ try {
+ GUI.init_laf()
- val isabelle_home0 = System.getenv("ISABELLE_HOME_WINDOWS")
- val isabelle_home = System.getProperty("isabelle.home")
+ val isabelle_home0 = System.getenv("ISABELLE_HOME_WINDOWS")
+ val isabelle_home = System.getProperty("isabelle.home")
- if (isabelle_home0 != null && isabelle_home0 != "") None
- else {
- if (isabelle_home == null || isabelle_home == "")
- error("Unknown Isabelle home directory")
- if (!(new JFile(isabelle_home)).isDirectory)
- error("Bad Isabelle home directory: " + quote(isabelle_home))
+ if (isabelle_home0 == null || isabelle_home0 == "") {
+ if (isabelle_home == null || isabelle_home == "")
+ error("Unknown Isabelle home directory")
+ if (!(new JFile(isabelle_home)).isDirectory)
+ error("Bad Isabelle home directory: " + quote(isabelle_home))
- val cygwin_root = isabelle_home + "\\contrib\\cygwin"
- if ((new JFile(cygwin_root)).isDirectory)
- System.setProperty("cygwin.root", cygwin_root)
+ val cygwin_root = isabelle_home + "\\contrib\\cygwin"
+ if ((new JFile(cygwin_root)).isDirectory)
+ System.setProperty("cygwin.root", cygwin_root)
- val uninitialized_file = new JFile(cygwin_root, "isabelle\\uninitialized")
- val uninitialized = uninitialized_file.isFile && uninitialized_file.delete
+ val uninitialized_file = new JFile(cygwin_root, "isabelle\\uninitialized")
+ val uninitialized = uninitialized_file.isFile && uninitialized_file.delete
- if (uninitialized) Some(isabelle_home) else None
- }
+ if (uninitialized)
+ Cygwin_Init.filesystem(system_dialog, isabelle_home)
}
- catch { case exn: Throwable => exit_error(exn) }
+ }
+ catch { case exn: Throwable => exit_error(exn) }
+ }
- init_isabelle_home match {
- case Some(isabelle_home) =>
- Swing_Thread.later { Cygwin_Init.main_frame(isabelle_home, continue(run)) }
- case None => run
- }
- }
- else run
+ build
+ val rc = system_dialog.join
+ if (rc == 0) start else sys.exit(rc)
}
}