author | wenzelm |
Sat, 07 Sep 2013 11:36:03 +0200 | |
changeset 53452 | 8181bc357dc4 |
parent 53449 | 913df2adc99c |
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 |