src/Pure/Tools/main.scala
author wenzelm
Sat, 07 Sep 2013 17:32:55 +0200
changeset 53461 26c609ada983
parent 53460 6015a663b889
child 53462 c531db093680
permissions -rw-r--r--
clarified modules;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
50687
a8db4bf70e90 moved files;
wenzelm
parents: 48275
diff changeset
     1
/*  Title:      Pure/Tools/main.scala
47663
20e0865ae9e7 default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
20e0865ae9e7 default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff changeset
     3
53419
1c87e79bb838 main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
wenzelm
parents: 52675
diff changeset
     4
Main Isabelle application entry point.
47663
20e0865ae9e7 default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff changeset
     5
*/
20e0865ae9e7 default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff changeset
     6
20e0865ae9e7 default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff changeset
     7
package isabelle
20e0865ae9e7 default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff changeset
     8
53419
1c87e79bb838 main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
wenzelm
parents: 52675
diff changeset
     9
53449
913df2adc99c build session before start of jedit;
wenzelm
parents: 53445
diff changeset
    10
import javax.swing.SwingUtilities
53445
811db2b751ed warm start of Isabelle/jEdit from Isabelle/Scala;
wenzelm
parents: 53423
diff changeset
    11
import java.lang.{System, ClassLoader}
53461
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
    12
import java.io.{File => JFile, BufferedReader, InputStreamReader}
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
    13
import java.nio.file.Files
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
    14
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
    15
import scala.annotation.tailrec
47663
20e0865ae9e7 default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff changeset
    16
20e0865ae9e7 default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff changeset
    17
20e0865ae9e7 default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff changeset
    18
object Main
20e0865ae9e7 default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff changeset
    19
{
53461
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
    20
  /** main entry point **/
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
    21
53456
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    22
  def main(args: Array[String])
53449
913df2adc99c build session before start of jedit;
wenzelm
parents: 53445
diff changeset
    23
  {
53456
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    24
    val system_dialog = new System_Dialog
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    25
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    26
    def exit_error(exn: Throwable): Nothing =
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    27
    {
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    28
      GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    29
      system_dialog.return_code(2)
53460
6015a663b889 tuned signature;
wenzelm
parents: 53459
diff changeset
    30
      system_dialog.join_exit
53456
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    31
    }
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    32
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    33
    def build
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    34
    {
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    35
      try {
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    36
        GUI.init_laf()
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    37
        Isabelle_System.init()
53449
913df2adc99c build session before start of jedit;
wenzelm
parents: 53445
diff changeset
    38
53456
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    39
        val mode = Isabelle_System.getenv("JEDIT_BUILD_MODE")
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    40
        if (mode == "none")
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    41
          system_dialog.return_code(0)
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    42
        else {
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    43
          val system_mode = mode == "" || mode == "system"
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    44
          val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    45
          val options = Options.init()
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    46
          val session = Isabelle_System.default_logic(
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    47
            Isabelle_System.getenv("JEDIT_LOGIC"),
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    48
            options.string("jedit_logic"))
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    49
          Build_Dialog.dialog(options, system_dialog, system_mode, dirs, session)
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    50
        }
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    51
      }
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    52
      catch { case exn: Throwable => exit_error(exn) }
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    53
    }
53449
913df2adc99c build session before start of jedit;
wenzelm
parents: 53445
diff changeset
    54
53456
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    55
    def start
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    56
    {
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    57
      val do_start =
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    58
      {
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    59
        try {
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    60
          /* settings directory */
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    61
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    62
          val settings_dir = Path.explode("$JEDIT_SETTINGS")
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    63
          Isabelle_System.mkdirs(settings_dir + Path.explode("DockableWindowManager"))
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    64
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    65
          if (!(settings_dir + Path.explode("perspective.xml")).is_file) {
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    66
            File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"),
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    67
              """<DOCKING LEFT="" TOP="" RIGHT="" BOTTOM="isabelle-readme" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />""")
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    68
            File.write(settings_dir + Path.explode("perspective.xml"),
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    69
              """<?xml version="1.0" encoding="UTF-8" ?>
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    70
<!DOCTYPE PERSPECTIVE SYSTEM "perspective.dtd">
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    71
<PERSPECTIVE>
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    72
<VIEW PLAIN="FALSE">
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    73
<GEOMETRY X="0" Y="35" WIDTH="1072" HEIGHT="787" EXT_STATE="0" />
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    74
</VIEW>
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    75
</PERSPECTIVE>""")
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    76
          }
53449
913df2adc99c build session before start of jedit;
wenzelm
parents: 53445
diff changeset
    77
913df2adc99c build session before start of jedit;
wenzelm
parents: 53445
diff changeset
    78
53456
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    79
          /* args */
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    80
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    81
          val jedit_options =
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    82
            Isabelle_System.getenv_strict("JEDIT_OPTIONS").split(" +")
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    83
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    84
          val jedit_settings =
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    85
            Array("-settings=" + Isabelle_System.platform_path(Path.explode("$JEDIT_SETTINGS")))
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    86
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    87
          val more_args =
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    88
            if (args.isEmpty)
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    89
              Array(Isabelle_System.platform_path(Path.explode("$USER_HOME/Scratch.thy")))
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    90
            else args
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    91
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    92
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    93
          /* startup */
53445
811db2b751ed warm start of Isabelle/jEdit from Isabelle/Scala;
wenzelm
parents: 53423
diff changeset
    94
53456
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    95
          System.setProperty("jedit.home",
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    96
            Isabelle_System.platform_path(Path.explode("$JEDIT_HOME/dist")))
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    97
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    98
          System.setProperty("scala.home",
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    99
            Isabelle_System.platform_path(Path.explode("$SCALA_HOME")))
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
   100
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
   101
          val jedit = ClassLoader.getSystemClassLoader.loadClass("org.gjt.sp.jedit.jEdit")
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
   102
          val jedit_main = jedit.getDeclaredMethod("main", classOf[Array[String]])
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
   103
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
   104
          () => jedit_main.invoke(null, jedit_options ++ jedit_settings ++ more_args)
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
   105
        }
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
   106
        catch { case exn: Throwable => exit_error(exn) }
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
   107
      }
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
   108
      do_start()
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
   109
    }
53419
1c87e79bb838 main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
wenzelm
parents: 52675
diff changeset
   110
1c87e79bb838 main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
wenzelm
parents: 52675
diff changeset
   111
    if (Platform.is_windows) {
53459
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   112
      try {
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   113
        GUI.init_laf()
53419
1c87e79bb838 main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
wenzelm
parents: 52675
diff changeset
   114
53459
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   115
        val isabelle_home0 = System.getenv("ISABELLE_HOME_WINDOWS")
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   116
        val isabelle_home = System.getProperty("isabelle.home")
47663
20e0865ae9e7 default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff changeset
   117
53459
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   118
        if (isabelle_home0 == null || isabelle_home0 == "") {
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   119
          if (isabelle_home == null || isabelle_home == "")
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   120
            error("Unknown Isabelle home directory")
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   121
          if (!(new JFile(isabelle_home)).isDirectory)
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   122
            error("Bad Isabelle home directory: " + quote(isabelle_home))
53419
1c87e79bb838 main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
wenzelm
parents: 52675
diff changeset
   123
53459
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   124
          val cygwin_root = isabelle_home + "\\contrib\\cygwin"
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   125
          if ((new JFile(cygwin_root)).isDirectory)
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   126
            System.setProperty("cygwin.root", cygwin_root)
53422
ec97451fdf2e recovered cygwin.root from 1c87e79bb838;
wenzelm
parents: 53419
diff changeset
   127
53459
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   128
          val uninitialized_file = new JFile(cygwin_root, "isabelle\\uninitialized")
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   129
          val uninitialized = uninitialized_file.isFile && uninitialized_file.delete
53419
1c87e79bb838 main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
wenzelm
parents: 52675
diff changeset
   130
53461
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   131
          if (uninitialized) cygwin_init(system_dialog, isabelle_home, cygwin_root)
53419
1c87e79bb838 main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
wenzelm
parents: 52675
diff changeset
   132
        }
53459
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   133
      }
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   134
      catch { case exn: Throwable => exit_error(exn) }
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   135
    }
53445
811db2b751ed warm start of Isabelle/jEdit from Isabelle/Scala;
wenzelm
parents: 53423
diff changeset
   136
53459
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   137
    build
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   138
    val rc = system_dialog.join
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   139
    if (rc == 0) start else sys.exit(rc)
53445
811db2b751ed warm start of Isabelle/jEdit from Isabelle/Scala;
wenzelm
parents: 53423
diff changeset
   140
  }
53461
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   141
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   142
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   143
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   144
  /** Cygwin init (e.g. after extraction via 7zip) **/
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   145
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   146
  private def cygwin_init(system_dialog: System_Dialog, isabelle_home: String, cygwin_root: String)
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   147
  {
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   148
    system_dialog.title("Isabelle system initialization")
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   149
    system_dialog.echo("Initializing Cygwin:")
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   150
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   151
    def execute(args: String*): Int =
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   152
    {
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   153
      val cwd = new JFile(isabelle_home)
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   154
      val env = Map("CYGWIN" -> "nodosfilewarning")
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   155
      system_dialog.execute(cwd, env, args: _*)
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   156
    }
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   157
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   158
    system_dialog.echo("symlinks ...")
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   159
    val symlinks =
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   160
    {
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   161
      val path = (new JFile(cygwin_root + "\\isabelle\\symlinks")).toPath
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   162
      Files.readAllLines(path, UTF8.charset).toArray.toList.asInstanceOf[List[String]]
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   163
    }
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   164
    @tailrec def recover_symlinks(list: List[String]): Unit =
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   165
    {
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   166
      list match {
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   167
        case Nil | List("") =>
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   168
        case link :: content :: rest =>
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   169
          val path = (new JFile(isabelle_home, link)).toPath
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   170
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   171
          val writer = Files.newBufferedWriter(path, UTF8.charset)
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   172
          try { writer.write("!<symlink>" + content + "\0") }
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   173
          finally { writer.close }
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   174
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   175
          Files.setAttribute(path, "dos:system", true)
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   176
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   177
          recover_symlinks(rest)
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   178
        case _ => error("Unbalanced symlinks list")
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   179
      }
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   180
    }
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   181
    recover_symlinks(symlinks)
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   182
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   183
    system_dialog.echo("rebaseall ...")
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   184
    execute(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall")
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   185
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   186
    system_dialog.echo("postinstall ...")
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   187
    execute(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall")
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   188
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   189
    system_dialog.echo("init ...")
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   190
    Isabelle_System.init()
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   191
    system_dialog.echo("OK")
26c609ada983 clarified modules;
wenzelm
parents: 53460
diff changeset
   192
  }
47663
20e0865ae9e7 default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff changeset
   193
}
20e0865ae9e7 default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff changeset
   194