src/Pure/Tools/main.scala
author wenzelm
Wed Nov 26 20:05:34 2014 +0100 (2014-11-26)
changeset 59058 a78612c67ec0
parent 56890 7f120d227ca5
child 59080 611914621edb
permissions -rw-r--r--
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm@50687
     1
/*  Title:      Pure/Tools/main.scala
wenzelm@47663
     2
    Author:     Makarius
wenzelm@47663
     3
wenzelm@53419
     4
Main Isabelle application entry point.
wenzelm@47663
     5
*/
wenzelm@47663
     6
wenzelm@47663
     7
package isabelle
wenzelm@47663
     8
wenzelm@53419
     9
wenzelm@55618
    10
import java.lang.{Class, ClassLoader}
wenzelm@53461
    11
import java.io.{File => JFile, BufferedReader, InputStreamReader}
wenzelm@53461
    12
import java.nio.file.Files
wenzelm@53461
    13
wenzelm@53461
    14
import scala.annotation.tailrec
wenzelm@47663
    15
wenzelm@47663
    16
wenzelm@47663
    17
object Main
wenzelm@47663
    18
{
wenzelm@53461
    19
  /** main entry point **/
wenzelm@53461
    20
wenzelm@53456
    21
  def main(args: Array[String])
wenzelm@53449
    22
  {
wenzelm@53456
    23
    val system_dialog = new System_Dialog
wenzelm@53456
    24
wenzelm@53456
    25
    def exit_error(exn: Throwable): Nothing =
wenzelm@53456
    26
    {
wenzelm@53456
    27
      GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
wenzelm@56667
    28
      system_dialog.return_code(Exn.return_code(exn, 2))
wenzelm@53460
    29
      system_dialog.join_exit
wenzelm@53456
    30
    }
wenzelm@53456
    31
wenzelm@53456
    32
    def build
wenzelm@53456
    33
    {
wenzelm@53456
    34
      try {
wenzelm@53456
    35
        GUI.init_laf()
wenzelm@53456
    36
        Isabelle_System.init()
wenzelm@53449
    37
wenzelm@53456
    38
        val mode = Isabelle_System.getenv("JEDIT_BUILD_MODE")
wenzelm@53456
    39
        if (mode == "none")
wenzelm@53456
    40
          system_dialog.return_code(0)
wenzelm@53456
    41
        else {
wenzelm@53519
    42
          val options = Options.init()
wenzelm@53456
    43
          val system_mode = mode == "" || mode == "system"
wenzelm@56890
    44
          val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
wenzelm@53456
    45
          val session = Isabelle_System.default_logic(
wenzelm@53456
    46
            Isabelle_System.getenv("JEDIT_LOGIC"),
wenzelm@53456
    47
            options.string("jedit_logic"))
wenzelm@53519
    48
wenzelm@53519
    49
          if (Build.build(options = options, build_heap = true, no_build = true,
wenzelm@56890
    50
              dirs = dirs, sessions = List(session)) == 0)
wenzelm@53519
    51
            system_dialog.return_code(0)
wenzelm@53519
    52
          else {
wenzelm@53519
    53
            system_dialog.title("Isabelle build (" + Isabelle_System.getenv("ML_IDENTIFIER") + ")")
wenzelm@53519
    54
            system_dialog.echo("Build started for Isabelle/" + session + " ...")
wenzelm@53519
    55
wenzelm@53519
    56
            val (out, rc) =
wenzelm@53519
    57
              try {
wenzelm@53519
    58
                ("",
wenzelm@56890
    59
                  Build.build(options = options, progress = system_dialog, build_heap = true,
wenzelm@56890
    60
                    dirs = dirs, system_mode = system_mode, sessions = List(session)))
wenzelm@53519
    61
              }
wenzelm@56671
    62
              catch {
wenzelm@56782
    63
                case exn: Throwable =>
wenzelm@56782
    64
                  (Output.error_text(Exn.message(exn)) + "\n", Exn.return_code(exn, 2))
wenzelm@56671
    65
              }
wenzelm@53519
    66
wenzelm@53519
    67
            system_dialog.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))
wenzelm@53519
    68
            system_dialog.return_code(rc)
wenzelm@53519
    69
          }
wenzelm@53456
    70
        }
wenzelm@53456
    71
      }
wenzelm@53456
    72
      catch { case exn: Throwable => exit_error(exn) }
wenzelm@53456
    73
    }
wenzelm@53449
    74
wenzelm@53456
    75
    def start
wenzelm@53456
    76
    {
wenzelm@53456
    77
      val do_start =
wenzelm@53456
    78
      {
wenzelm@53456
    79
        try {
wenzelm@53456
    80
          /* settings directory */
wenzelm@53456
    81
wenzelm@53456
    82
          val settings_dir = Path.explode("$JEDIT_SETTINGS")
wenzelm@53456
    83
          Isabelle_System.mkdirs(settings_dir + Path.explode("DockableWindowManager"))
wenzelm@53456
    84
wenzelm@53456
    85
          if (!(settings_dir + Path.explode("perspective.xml")).is_file) {
wenzelm@53456
    86
            File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"),
wenzelm@53772
    87
              """<DOCKING LEFT="" TOP="" RIGHT="isabelle-documentation" BOTTOM="" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />""")
wenzelm@53456
    88
            File.write(settings_dir + Path.explode("perspective.xml"),
wenzelm@53456
    89
              """<?xml version="1.0" encoding="UTF-8" ?>
wenzelm@53456
    90
<!DOCTYPE PERSPECTIVE SYSTEM "perspective.dtd">
wenzelm@53456
    91
<PERSPECTIVE>
wenzelm@53456
    92
<VIEW PLAIN="FALSE">
wenzelm@53456
    93
<GEOMETRY X="0" Y="35" WIDTH="1072" HEIGHT="787" EXT_STATE="0" />
wenzelm@53456
    94
</VIEW>
wenzelm@53456
    95
</PERSPECTIVE>""")
wenzelm@53456
    96
          }
wenzelm@53449
    97
wenzelm@53449
    98
wenzelm@53456
    99
          /* args */
wenzelm@53456
   100
wenzelm@53456
   101
          val jedit_options =
wenzelm@53456
   102
            Isabelle_System.getenv_strict("JEDIT_OPTIONS").split(" +")
wenzelm@53456
   103
wenzelm@53456
   104
          val jedit_settings =
wenzelm@53456
   105
            Array("-settings=" + Isabelle_System.platform_path(Path.explode("$JEDIT_SETTINGS")))
wenzelm@53456
   106
wenzelm@53456
   107
          val more_args =
wenzelm@53456
   108
            if (args.isEmpty)
wenzelm@53456
   109
              Array(Isabelle_System.platform_path(Path.explode("$USER_HOME/Scratch.thy")))
wenzelm@53456
   110
            else args
wenzelm@53456
   111
wenzelm@53456
   112
wenzelm@53456
   113
          /* startup */
wenzelm@53445
   114
wenzelm@53965
   115
          update_environment()
wenzelm@53965
   116
wenzelm@53456
   117
          System.setProperty("jedit.home",
wenzelm@53456
   118
            Isabelle_System.platform_path(Path.explode("$JEDIT_HOME/dist")))
wenzelm@53456
   119
wenzelm@53456
   120
          System.setProperty("scala.home",
wenzelm@53456
   121
            Isabelle_System.platform_path(Path.explode("$SCALA_HOME")))
wenzelm@53456
   122
wenzelm@53912
   123
          val jedit =
wenzelm@53912
   124
            Class.forName("org.gjt.sp.jedit.jEdit", true, ClassLoader.getSystemClassLoader)
wenzelm@53456
   125
          val jedit_main = jedit.getDeclaredMethod("main", classOf[Array[String]])
wenzelm@53456
   126
wenzelm@53456
   127
          () => jedit_main.invoke(null, jedit_options ++ jedit_settings ++ more_args)
wenzelm@53456
   128
        }
wenzelm@53456
   129
        catch { case exn: Throwable => exit_error(exn) }
wenzelm@53456
   130
      }
wenzelm@53456
   131
      do_start()
wenzelm@53456
   132
    }
wenzelm@53419
   133
wenzelm@53419
   134
    if (Platform.is_windows) {
wenzelm@53459
   135
      try {
wenzelm@53459
   136
        GUI.init_laf()
wenzelm@53419
   137
wenzelm@53967
   138
        val isabelle_home0 = System.getenv("ISABELLE_HOME")
wenzelm@53459
   139
        val isabelle_home = System.getProperty("isabelle.home")
wenzelm@47663
   140
wenzelm@53459
   141
        if (isabelle_home0 == null || isabelle_home0 == "") {
wenzelm@53459
   142
          if (isabelle_home == null || isabelle_home == "")
wenzelm@53459
   143
            error("Unknown Isabelle home directory")
wenzelm@53459
   144
          if (!(new JFile(isabelle_home)).isDirectory)
wenzelm@53459
   145
            error("Bad Isabelle home directory: " + quote(isabelle_home))
wenzelm@53419
   146
wenzelm@53459
   147
          val cygwin_root = isabelle_home + "\\contrib\\cygwin"
wenzelm@53459
   148
          if ((new JFile(cygwin_root)).isDirectory)
wenzelm@53459
   149
            System.setProperty("cygwin.root", cygwin_root)
wenzelm@53422
   150
wenzelm@53459
   151
          val uninitialized_file = new JFile(cygwin_root, "isabelle\\uninitialized")
wenzelm@53459
   152
          val uninitialized = uninitialized_file.isFile && uninitialized_file.delete
wenzelm@53419
   153
wenzelm@53461
   154
          if (uninitialized) cygwin_init(system_dialog, isabelle_home, cygwin_root)
wenzelm@53419
   155
        }
wenzelm@53459
   156
      }
wenzelm@53459
   157
      catch { case exn: Throwable => exit_error(exn) }
wenzelm@53462
   158
wenzelm@53462
   159
      if (system_dialog.stopped) {
wenzelm@56667
   160
        system_dialog.return_code(Exn.Interrupt.return_code)
wenzelm@53462
   161
        system_dialog.join_exit
wenzelm@53462
   162
      }
wenzelm@53459
   163
    }
wenzelm@53445
   164
wenzelm@53459
   165
    build
wenzelm@53459
   166
    val rc = system_dialog.join
wenzelm@53459
   167
    if (rc == 0) start else sys.exit(rc)
wenzelm@53445
   168
  }
wenzelm@53461
   169
wenzelm@53461
   170
wenzelm@53461
   171
wenzelm@53461
   172
  /** Cygwin init (e.g. after extraction via 7zip) **/
wenzelm@53461
   173
wenzelm@53461
   174
  private def cygwin_init(system_dialog: System_Dialog, isabelle_home: String, cygwin_root: String)
wenzelm@53461
   175
  {
wenzelm@53461
   176
    system_dialog.title("Isabelle system initialization")
wenzelm@53466
   177
    system_dialog.echo("Initializing Cygwin ...")
wenzelm@53461
   178
wenzelm@53461
   179
    def execute(args: String*): Int =
wenzelm@53461
   180
    {
wenzelm@53461
   181
      val cwd = new JFile(isabelle_home)
wenzelm@53461
   182
      val env = Map("CYGWIN" -> "nodosfilewarning")
wenzelm@53461
   183
      system_dialog.execute(cwd, env, args: _*)
wenzelm@53461
   184
    }
wenzelm@53461
   185
wenzelm@53461
   186
    system_dialog.echo("symlinks ...")
wenzelm@53461
   187
    val symlinks =
wenzelm@53461
   188
    {
wenzelm@53461
   189
      val path = (new JFile(cygwin_root + "\\isabelle\\symlinks")).toPath
wenzelm@53461
   190
      Files.readAllLines(path, UTF8.charset).toArray.toList.asInstanceOf[List[String]]
wenzelm@53461
   191
    }
wenzelm@53461
   192
    @tailrec def recover_symlinks(list: List[String]): Unit =
wenzelm@53461
   193
    {
wenzelm@53461
   194
      list match {
wenzelm@53461
   195
        case Nil | List("") =>
wenzelm@53461
   196
        case link :: content :: rest =>
wenzelm@53461
   197
          val path = (new JFile(isabelle_home, link)).toPath
wenzelm@53461
   198
wenzelm@53461
   199
          val writer = Files.newBufferedWriter(path, UTF8.charset)
wenzelm@56661
   200
          try { writer.write("!<symlink>" + content + "\u0000") }
wenzelm@53461
   201
          finally { writer.close }
wenzelm@53461
   202
wenzelm@53461
   203
          Files.setAttribute(path, "dos:system", true)
wenzelm@53461
   204
wenzelm@53461
   205
          recover_symlinks(rest)
wenzelm@53461
   206
        case _ => error("Unbalanced symlinks list")
wenzelm@53461
   207
      }
wenzelm@53461
   208
    }
wenzelm@53461
   209
    recover_symlinks(symlinks)
wenzelm@53461
   210
wenzelm@53461
   211
    system_dialog.echo("rebaseall ...")
wenzelm@53461
   212
    execute(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall")
wenzelm@53461
   213
wenzelm@53461
   214
    system_dialog.echo("postinstall ...")
wenzelm@53461
   215
    execute(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall")
wenzelm@53461
   216
wenzelm@53461
   217
    system_dialog.echo("init ...")
wenzelm@53461
   218
    Isabelle_System.init()
wenzelm@53461
   219
  }
wenzelm@53965
   220
wenzelm@53965
   221
wenzelm@53965
   222
wenzelm@53965
   223
  /** adhoc update of JVM environment variables **/
wenzelm@53965
   224
wenzelm@53965
   225
  def update_environment()
wenzelm@53965
   226
  {
wenzelm@53965
   227
    val update =
wenzelm@53966
   228
    {
wenzelm@53966
   229
      val isabelle_home = Isabelle_System.getenv("ISABELLE_HOME")
wenzelm@54351
   230
      val isabelle_home_user = Isabelle_System.getenv("ISABELLE_HOME_USER")
wenzelm@53966
   231
      val upd =
wenzelm@53966
   232
        if (Platform.is_windows)
wenzelm@54351
   233
          List(
wenzelm@54351
   234
            "ISABELLE_HOME" -> Isabelle_System.jvm_path(isabelle_home),
wenzelm@54351
   235
            "ISABELLE_HOME_USER" -> Isabelle_System.jvm_path(isabelle_home_user),
wenzelm@54351
   236
            "INI_DIR" -> "")
wenzelm@53966
   237
        else
wenzelm@54351
   238
          List(
wenzelm@54351
   239
            "ISABELLE_HOME" -> isabelle_home,
wenzelm@54351
   240
            "ISABELLE_HOME_USER" -> isabelle_home_user)
wenzelm@53965
   241
wenzelm@53966
   242
      (env0: Any) => {
wenzelm@53966
   243
        val env = env0.asInstanceOf[java.util.Map[String, String]]
wenzelm@53966
   244
        upd.foreach {
wenzelm@53966
   245
          case (x, "") => env.remove(x)
wenzelm@53966
   246
          case (x, y) => env.put(x, y)
wenzelm@53966
   247
        }
wenzelm@53966
   248
      }
wenzelm@53966
   249
    }
wenzelm@53965
   250
wenzelm@53965
   251
    classOf[java.util.Collections].getDeclaredClasses
wenzelm@53965
   252
      .find(c => c.getName == "java.util.Collections$UnmodifiableMap") match
wenzelm@53965
   253
    {
wenzelm@53965
   254
      case Some(c) =>
wenzelm@53965
   255
        val m = c.getDeclaredField("m")
wenzelm@53965
   256
        m.setAccessible(true)
wenzelm@53966
   257
        update(m.get(System.getenv()))
wenzelm@53966
   258
wenzelm@53966
   259
        if (Platform.is_windows) {
wenzelm@53966
   260
          val ProcessEnvironment = Class.forName("java.lang.ProcessEnvironment")
wenzelm@53966
   261
          val field = ProcessEnvironment.getDeclaredField("theCaseInsensitiveEnvironment")
wenzelm@53966
   262
          field.setAccessible(true)
wenzelm@53966
   263
          update(field.get(null))
wenzelm@53965
   264
        }
wenzelm@53966
   265
wenzelm@53966
   266
      case None =>
wenzelm@53966
   267
        error("Failed to update JVM environment -- platform incompatibility")
wenzelm@53965
   268
    }
wenzelm@53965
   269
  }
wenzelm@47663
   270
}
wenzelm@47663
   271