# HG changeset patch
# User wenzelm
# Date 1557343714 -7200
# Node ID 4ce07be8ba17d020f2ae3c0a1db17e83042baba8
# Parent  edd3b2e06f902c70c96730a419d786f7f8e2c778
clarified InstallPath: relative to self-extracting exe;
support for AutoInstall (option -ai);

diff -r edd3b2e06f90 -r 4ce07be8ba17 Admin/Windows/Installer/sfx.txt
--- a/Admin/Windows/Installer/sfx.txt	Wed May 08 20:10:13 2019 +0200
+++ b/Admin/Windows/Installer/sfx.txt	Wed May 08 21:28:34 2019 +0200
@@ -1,9 +1,10 @@
 ;!@Install@!UTF-8!
 GUIFlags="64"
-InstallPath="%UserDesktop%"
+InstallPath="%%S"
 BeginPrompt="Unpack {ISABELLE_NAME}?"
 ExtractPathText="Target directory"
 ExtractTitle="Unpacking {ISABELLE_NAME} ..."
 Shortcut="Du,{%%T\{ISABELLE_NAME}\{ISABELLE_NAME}.exe},{},{},{},{{ISABELLE_NAME}},{%%T\{ISABELLE_NAME}}"
 RunProgram="\"%%T\{ISABELLE_NAME}\{ISABELLE_NAME}.exe\""
+AutoInstall="\"%%T\{ISABELLE_NAME}\{ISABELLE_NAME}.exe\" -init"
 ;!@InstallEnd@!
diff -r edd3b2e06f90 -r 4ce07be8ba17 src/Pure/Tools/main.scala
--- a/src/Pure/Tools/main.scala	Wed May 08 20:10:13 2019 +0200
+++ b/src/Pure/Tools/main.scala	Wed May 08 21:28:34 2019 +0200
@@ -16,18 +16,22 @@
 
   def main(args: Array[String])
   {
-    val start =
-    {
-      try {
-        Isabelle_System.init()
-        Isabelle_Fonts.init()
+    if (args.nonEmpty && args(0) == "-init") {
+      Isabelle_System.init()
+    }
+    else {
+      val start =
+      {
+        try {
+          Isabelle_System.init()
+          Isabelle_Fonts.init()
 
 
-        /* ROOTS template */
+          /* ROOTS template */
 
-        {
-          val roots = Path.explode("$ISABELLE_HOME_USER/ROOTS")
-          if (!roots.is_file) File.write(roots, """# Additional session root directories
+          {
+            val roots = Path.explode("$ISABELLE_HOME_USER/ROOTS")
+            if (!roots.is_file) File.write(roots, """# Additional session root directories
 #
 #   * each line contains one directory entry in Isabelle path notation
 #   * lines starting with "#" are stripped
@@ -35,100 +39,101 @@
 #
 #:mode=text:encoding=UTF-8:
 """)
-        }
+          }
 
 
-        /* settings directory */
+          /* settings directory */
 
-        val settings_dir = Path.explode("$JEDIT_SETTINGS")
+          val settings_dir = Path.explode("$JEDIT_SETTINGS")
 
-        val properties = settings_dir + Path.explode("properties")
-        if (properties.is_file) {
-          val props1 = split_lines(File.read(properties))
-          val props2 = props1.filterNot(_.startsWith("plugin-blacklist.Isabelle-jEdit"))
-          if (props1 != props2) File.write(properties, cat_lines(props2))
-        }
+          val properties = settings_dir + Path.explode("properties")
+          if (properties.is_file) {
+            val props1 = split_lines(File.read(properties))
+            val props2 = props1.filterNot(_.startsWith("plugin-blacklist.Isabelle-jEdit"))
+            if (props1 != props2) File.write(properties, cat_lines(props2))
+          }
 
-        Isabelle_System.mkdirs(settings_dir + Path.explode("DockableWindowManager"))
+          Isabelle_System.mkdirs(settings_dir + Path.explode("DockableWindowManager"))
 
-        if (!(settings_dir + Path.explode("perspective.xml")).is_file) {
-          File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"),
-            """<DOCKING LEFT="isabelle-documentation" TOP="" RIGHT="isabelle-theories" BOTTOM="" LEFT_POS="250" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />""")
-          File.write(settings_dir + Path.explode("perspective.xml"),
-            XML.header +
+          if (!(settings_dir + Path.explode("perspective.xml")).is_file) {
+            File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"),
+              """<DOCKING LEFT="isabelle-documentation" TOP="" RIGHT="isabelle-theories" BOTTOM="" LEFT_POS="250" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />""")
+            File.write(settings_dir + Path.explode("perspective.xml"),
+              XML.header +
 """<!DOCTYPE PERSPECTIVE SYSTEM "perspective.dtd">
 <PERSPECTIVE>
 <VIEW PLAIN="FALSE">
 <GEOMETRY X="0" Y="35" WIDTH="1200" HEIGHT="850" EXT_STATE="0" />
 </VIEW>
 </PERSPECTIVE>""")
-        }
+          }
 
 
-        /* args */
+          /* args */
 
-        val jedit_settings =
-          "-settings=" + File.platform_path(Path.explode("$JEDIT_SETTINGS"))
+          val jedit_settings =
+            "-settings=" + File.platform_path(Path.explode("$JEDIT_SETTINGS"))
 
-        val jedit_server =
-          System.getProperty("isabelle.jedit_server") match {
-            case null | "" => "-noserver"
-            case name => "-server=" + name
-          }
+          val jedit_server =
+            System.getProperty("isabelle.jedit_server") match {
+              case null | "" => "-noserver"
+              case name => "-server=" + name
+            }
 
-        val jedit_options =
-          Isabelle_System.getenv_strict("JEDIT_OPTIONS").split(" +")
+          val jedit_options =
+            Isabelle_System.getenv_strict("JEDIT_OPTIONS").split(" +")
 
-        val more_args =
-        {
-          args.toList.dropWhile(arg => arg.startsWith("-") && arg != "--") match {
-            case Nil | List("--") =>
-              args ++ Array(File.platform_path(Path.explode("$USER_HOME/Scratch.thy")))
-            case List(":") => args.slice(0, args.size - 1)
-            case _ => args
+          val more_args =
+          {
+            args.toList.dropWhile(arg => arg.startsWith("-") && arg != "--") match {
+              case Nil | List("--") =>
+                args ++ Array(File.platform_path(Path.explode("$USER_HOME/Scratch.thy")))
+              case List(":") => args.slice(0, args.size - 1)
+              case _ => args
+            }
           }
-        }
 
 
-        /* environment */
+          /* environment */
 
-        def putenv(name: String, value: String)
-        {
-          val misc =
-            Class.forName("org.gjt.sp.jedit.MiscUtilities", true, ClassLoader.getSystemClassLoader)
-          val putenv = misc.getMethod("putenv", classOf[String], classOf[String])
-          putenv.invoke(null, name, value)
-        }
+          def putenv(name: String, value: String)
+          {
+            val misc =
+              Class.forName("org.gjt.sp.jedit.MiscUtilities", true, ClassLoader.getSystemClassLoader)
+            val putenv = misc.getMethod("putenv", classOf[String], classOf[String])
+            putenv.invoke(null, name, value)
+          }
 
-        for (name <- List("ISABELLE_HOME", "ISABELLE_HOME_USER", "JEDIT_HOME", "JEDIT_SETTINGS")) {
-          putenv(name, File.platform_path(Isabelle_System.getenv(name)))
-        }
-        putenv("ISABELLE_ROOT", null)
+          for (name <- List("ISABELLE_HOME", "ISABELLE_HOME_USER", "JEDIT_HOME", "JEDIT_SETTINGS")) {
+            putenv(name, File.platform_path(Isabelle_System.getenv(name)))
+          }
+          putenv("ISABELLE_ROOT", null)
 
 
-        /* properties */
+          /* properties */
 
-        System.setProperty("jedit.home", File.platform_path(Path.explode("$JEDIT_HOME/dist")))
-        System.setProperty("scala.home", File.platform_path(Path.explode("$SCALA_HOME")))
-        System.setProperty("scala.color", "false")
+          System.setProperty("jedit.home", File.platform_path(Path.explode("$JEDIT_HOME/dist")))
+          System.setProperty("scala.home", File.platform_path(Path.explode("$SCALA_HOME")))
+          System.setProperty("scala.color", "false")
 
 
-        /* main startup */
+          /* main startup */
+
+          val jedit =
+            Class.forName("org.gjt.sp.jedit.jEdit", true, ClassLoader.getSystemClassLoader)
+          val jedit_main = jedit.getMethod("main", classOf[Array[String]])
 
-        val jedit =
-          Class.forName("org.gjt.sp.jedit.jEdit", true, ClassLoader.getSystemClassLoader)
-        val jedit_main = jedit.getMethod("main", classOf[Array[String]])
-
-        () => jedit_main.invoke(
-          null, Array(jedit_settings, jedit_server) ++ jedit_options ++ more_args)
+          () => jedit_main.invoke(
+            null, Array(jedit_settings, jedit_server) ++ jedit_options ++ more_args)
+        }
+        catch {
+          case exn: Throwable =>
+            GUI.init_laf()
+            GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
+            sys.exit(2)
+        }
       }
-      catch {
-        case exn: Throwable =>
-          GUI.init_laf()
-          GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
-          sys.exit(2)
-      }
+      start()
     }
-    start()
   }
 }