| author | wenzelm |
| Sat, 07 Sep 2013 16:33:10 +0200 | |
| changeset 53458 | ddefd18d5ed0 |
| parent 53452 | 8181bc357dc4 |
| child 53459 | 33f773731f0c |
| permissions | -rw-r--r-- |
| 52667 | 1 |
/* Title: Pure/System/cygwin_init.scala |
| 52553 | 2 |
Author: Makarius |
3 |
||
|
52669
fb59e6e9442a
recover Cygwin symlinks via Windows file-system operations;
wenzelm
parents:
52667
diff
changeset
|
4 |
Initialize Isabelle distribution after extracting via 7zip. |
| 52553 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
| 52667 | 10 |
import java.io.{File => JFile, BufferedReader, InputStreamReader}
|
| 52553 | 11 |
import java.nio.file.{Paths, Files}
|
| 52667 | 12 |
import java.awt.{GraphicsEnvironment, Point, Font}
|
13 |
import javax.swing.ImageIcon |
|
14 |
||
|
52669
fb59e6e9442a
recover Cygwin symlinks via Windows file-system operations;
wenzelm
parents:
52667
diff
changeset
|
15 |
import scala.annotation.tailrec |
| 52667 | 16 |
import scala.swing.{ScrollPane, Button, FlowPanel,
|
17 |
BorderPanel, MainFrame, TextArea, SwingApplication} |
|
18 |
import scala.swing.event.ButtonClicked |
|
| 52553 | 19 |
|
20 |
||
| 52667 | 21 |
object Cygwin_Init |
| 52553 | 22 |
{
|
|
53419
1c87e79bb838
main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
wenzelm
parents:
52672
diff
changeset
|
23 |
/* main GUI entry point */ |
| 52667 | 24 |
|
| 53449 | 25 |
def main_frame(isabelle_home: String, continue: Int => Unit) = new MainFrame |
| 52667 | 26 |
{
|
27 |
title = "Isabelle system initialization" |
|
|
53452
8181bc357dc4
more portable access to icon -- avoid Isabelle_System which is not yet initialized in bootstrap;
wenzelm
parents:
53449
diff
changeset
|
28 |
iconImage = GUI.isabelle_image() |
| 52667 | 29 |
|
30 |
val layout_panel = new BorderPanel |
|
31 |
contents = layout_panel |
|
32 |
||
33 |
||
34 |
/* text area */ |
|
35 |
||
36 |
def echo(msg: String) { text_area.append(msg + "\n") }
|
|
37 |
||
38 |
val text_area = new TextArea {
|
|
39 |
font = new Font("SansSerif", Font.PLAIN, GUI.resolution_scale(10) max 14)
|
|
40 |
editable = false |
|
| 52672 | 41 |
columns = 50 |
42 |
rows = 15 |
|
| 52667 | 43 |
} |
44 |
||
45 |
layout_panel.layout(new ScrollPane(text_area)) = BorderPanel.Position.Center |
|
46 |
||
47 |
||
48 |
/* exit button */ |
|
49 |
||
50 |
var _return_code: Option[Int] = None |
|
|
53419
1c87e79bb838
main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
wenzelm
parents:
52672
diff
changeset
|
51 |
def maybe_exit() |
|
1c87e79bb838
main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
wenzelm
parents:
52672
diff
changeset
|
52 |
{
|
|
1c87e79bb838
main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
wenzelm
parents:
52672
diff
changeset
|
53 |
_return_code match {
|
|
1c87e79bb838
main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
wenzelm
parents:
52672
diff
changeset
|
54 |
case None => |
| 53449 | 55 |
case Some(rc) => |
| 53424 | 56 |
visible = false |
| 53449 | 57 |
continue(rc) |
|
53419
1c87e79bb838
main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
wenzelm
parents:
52672
diff
changeset
|
58 |
} |
|
1c87e79bb838
main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
wenzelm
parents:
52672
diff
changeset
|
59 |
} |
| 52667 | 60 |
|
61 |
def return_code(rc: Int): Unit = |
|
62 |
Swing_Thread.later {
|
|
63 |
_return_code = Some(rc) |
|
64 |
button.peer.getRootPane.setDefaultButton(button.peer) |
|
65 |
layout_panel.repaint |
|
66 |
} |
|
67 |
||
68 |
override def closeOperation { maybe_exit() }
|
|
69 |
||
70 |
val button = new Button {
|
|
71 |
text = "Done" |
|
72 |
reactions += { case ButtonClicked(_) => maybe_exit() }
|
|
73 |
} |
|
74 |
val button_panel = new FlowPanel(FlowPanel.Alignment.Center)(button) |
|
75 |
||
76 |
layout_panel.layout(button_panel) = BorderPanel.Position.South |
|
77 |
||
78 |
||
79 |
/* show window */ |
|
80 |
||
81 |
pack() |
|
82 |
val point = GraphicsEnvironment.getLocalGraphicsEnvironment().getCenterPoint() |
|
83 |
location = new Point(point.x - size.width / 2, point.y - size.height / 2) |
|
84 |
visible = true |
|
85 |
||
86 |
default_thread_pool.submit(() => |
|
87 |
try {
|
|
|
53419
1c87e79bb838
main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
wenzelm
parents:
52672
diff
changeset
|
88 |
init_filesystem(isabelle_home, echo) |
| 52667 | 89 |
return_code(0) |
90 |
} |
|
91 |
catch {
|
|
92 |
case exn: Throwable => |
|
93 |
text_area.append("Error:\n" + Exn.message(exn) + "\n")
|
|
94 |
return_code(2) |
|
95 |
} |
|
96 |
) |
|
97 |
} |
|
98 |
||
99 |
||
100 |
/* init Cygwin file-system */ |
|
101 |
||
|
53419
1c87e79bb838
main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
wenzelm
parents:
52672
diff
changeset
|
102 |
private def init_filesystem(isabelle_home: String, echo: String => Unit) |
| 52667 | 103 |
{
|
|
53423
b5a279c7d7f3
more explicit cygwin_root (again) -- do not rely on isabelle_home as cwd;
wenzelm
parents:
53419
diff
changeset
|
104 |
val cygwin_root = isabelle_home + "\\contrib\\cygwin" |
|
b5a279c7d7f3
more explicit cygwin_root (again) -- do not rely on isabelle_home as cwd;
wenzelm
parents:
53419
diff
changeset
|
105 |
|
| 52672 | 106 |
def execute(args: String*): Int = |
107 |
{
|
|
108 |
val cwd = new JFile(isabelle_home) |
|
109 |
val env = Map("CYGWIN" -> "nodosfilewarning")
|
|
110 |
val proc = Isabelle_System.raw_execute(cwd, env, true, args: _*) |
|
111 |
proc.getOutputStream.close |
|
112 |
||
113 |
val stdout = new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset)) |
|
114 |
try {
|
|
115 |
var line = stdout.readLine |
|
116 |
while (line != null) {
|
|
117 |
echo(line) |
|
118 |
line = stdout.readLine |
|
119 |
} |
|
120 |
} |
|
121 |
finally { stdout.close }
|
|
122 |
||
123 |
proc.waitFor |
|
124 |
} |
|
125 |
||
126 |
echo("Initializing Cygwin:")
|
|
|
52669
fb59e6e9442a
recover Cygwin symlinks via Windows file-system operations;
wenzelm
parents:
52667
diff
changeset
|
127 |
|
|
fb59e6e9442a
recover Cygwin symlinks via Windows file-system operations;
wenzelm
parents:
52667
diff
changeset
|
128 |
echo("symlinks ...")
|
|
fb59e6e9442a
recover Cygwin symlinks via Windows file-system operations;
wenzelm
parents:
52667
diff
changeset
|
129 |
val symlinks = |
|
fb59e6e9442a
recover Cygwin symlinks via Windows file-system operations;
wenzelm
parents:
52667
diff
changeset
|
130 |
{
|
|
53423
b5a279c7d7f3
more explicit cygwin_root (again) -- do not rely on isabelle_home as cwd;
wenzelm
parents:
53419
diff
changeset
|
131 |
val path = (new JFile(cygwin_root + "\\isabelle\\symlinks")).toPath |
|
52669
fb59e6e9442a
recover Cygwin symlinks via Windows file-system operations;
wenzelm
parents:
52667
diff
changeset
|
132 |
Files.readAllLines(path, UTF8.charset).toArray.toList.asInstanceOf[List[String]] |
|
fb59e6e9442a
recover Cygwin symlinks via Windows file-system operations;
wenzelm
parents:
52667
diff
changeset
|
133 |
} |
|
fb59e6e9442a
recover Cygwin symlinks via Windows file-system operations;
wenzelm
parents:
52667
diff
changeset
|
134 |
@tailrec def recover_symlinks(list: List[String]): Unit = |
|
fb59e6e9442a
recover Cygwin symlinks via Windows file-system operations;
wenzelm
parents:
52667
diff
changeset
|
135 |
{
|
|
fb59e6e9442a
recover Cygwin symlinks via Windows file-system operations;
wenzelm
parents:
52667
diff
changeset
|
136 |
list match {
|
|
fb59e6e9442a
recover Cygwin symlinks via Windows file-system operations;
wenzelm
parents:
52667
diff
changeset
|
137 |
case Nil | List("") =>
|
|
fb59e6e9442a
recover Cygwin symlinks via Windows file-system operations;
wenzelm
parents:
52667
diff
changeset
|
138 |
case link :: content :: rest => |
|
fb59e6e9442a
recover Cygwin symlinks via Windows file-system operations;
wenzelm
parents:
52667
diff
changeset
|
139 |
val path = (new JFile(isabelle_home, link)).toPath |
|
fb59e6e9442a
recover Cygwin symlinks via Windows file-system operations;
wenzelm
parents:
52667
diff
changeset
|
140 |
|
|
fb59e6e9442a
recover Cygwin symlinks via Windows file-system operations;
wenzelm
parents:
52667
diff
changeset
|
141 |
val writer = Files.newBufferedWriter(path, UTF8.charset) |
|
fb59e6e9442a
recover Cygwin symlinks via Windows file-system operations;
wenzelm
parents:
52667
diff
changeset
|
142 |
try { writer.write("!<symlink>" + content + "\0") }
|
|
fb59e6e9442a
recover Cygwin symlinks via Windows file-system operations;
wenzelm
parents:
52667
diff
changeset
|
143 |
finally { writer.close }
|
|
fb59e6e9442a
recover Cygwin symlinks via Windows file-system operations;
wenzelm
parents:
52667
diff
changeset
|
144 |
|
|
fb59e6e9442a
recover Cygwin symlinks via Windows file-system operations;
wenzelm
parents:
52667
diff
changeset
|
145 |
Files.setAttribute(path, "dos:system", true) |
|
fb59e6e9442a
recover Cygwin symlinks via Windows file-system operations;
wenzelm
parents:
52667
diff
changeset
|
146 |
|
|
fb59e6e9442a
recover Cygwin symlinks via Windows file-system operations;
wenzelm
parents:
52667
diff
changeset
|
147 |
recover_symlinks(rest) |
|
fb59e6e9442a
recover Cygwin symlinks via Windows file-system operations;
wenzelm
parents:
52667
diff
changeset
|
148 |
case _ => error("Unbalanced symlinks list")
|
|
fb59e6e9442a
recover Cygwin symlinks via Windows file-system operations;
wenzelm
parents:
52667
diff
changeset
|
149 |
} |
|
fb59e6e9442a
recover Cygwin symlinks via Windows file-system operations;
wenzelm
parents:
52667
diff
changeset
|
150 |
} |
|
fb59e6e9442a
recover Cygwin symlinks via Windows file-system operations;
wenzelm
parents:
52667
diff
changeset
|
151 |
recover_symlinks(symlinks) |
|
fb59e6e9442a
recover Cygwin symlinks via Windows file-system operations;
wenzelm
parents:
52667
diff
changeset
|
152 |
|
|
fb59e6e9442a
recover Cygwin symlinks via Windows file-system operations;
wenzelm
parents:
52667
diff
changeset
|
153 |
echo("rebaseall ...")
|
|
53423
b5a279c7d7f3
more explicit cygwin_root (again) -- do not rely on isabelle_home as cwd;
wenzelm
parents:
53419
diff
changeset
|
154 |
execute(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall") |
|
52669
fb59e6e9442a
recover Cygwin symlinks via Windows file-system operations;
wenzelm
parents:
52667
diff
changeset
|
155 |
|
|
fb59e6e9442a
recover Cygwin symlinks via Windows file-system operations;
wenzelm
parents:
52667
diff
changeset
|
156 |
echo("postinstall ...")
|
|
53423
b5a279c7d7f3
more explicit cygwin_root (again) -- do not rely on isabelle_home as cwd;
wenzelm
parents:
53419
diff
changeset
|
157 |
execute(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall") |
| 52672 | 158 |
|
159 |
echo("init ...")
|
|
160 |
Isabelle_System.init() |
|
161 |
echo("OK")
|
|
| 52667 | 162 |
} |
| 52553 | 163 |
} |
164 |