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