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