src/Pure/Tools/main.scala
author wenzelm
Mon Oct 09 21:12:22 2017 +0200 (21 months ago)
changeset 66822 4642cf4a7ebb
parent 66577 6e35cf3ce869
child 69188 2fd73a1a0937
permissions -rw-r--r--
tuned signature;
     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 
    12 
    13 object Main
    14 {
    15   /* main entry point */
    16 
    17   def main(args: Array[String])
    18   {
    19     val start =
    20     {
    21       try {
    22         Isabelle_System.init()
    23         GUI.install_fonts()
    24 
    25 
    26         /* ROOTS template */
    27 
    28         {
    29           val roots = Path.explode("$ISABELLE_HOME_USER/ROOTS")
    30           if (!roots.is_file) File.write(roots, """# Additional session root directories
    31 #
    32 #   * each line contains one directory entry in Isabelle path notation
    33 #   * lines starting with "#" are stripped
    34 #   * changes require application restart
    35 #
    36 #:mode=text:encoding=UTF-8:
    37 """)
    38         }
    39 
    40 
    41         /* settings directory */
    42 
    43         val settings_dir = Path.explode("$JEDIT_SETTINGS")
    44 
    45         val properties = settings_dir + Path.explode("properties")
    46         if (properties.is_file) {
    47           val props1 = split_lines(File.read(properties))
    48           val props2 = props1.filterNot(_.startsWith("plugin-blacklist.Isabelle-jEdit"))
    49           if (props1 != props2) File.write(properties, cat_lines(props2))
    50         }
    51 
    52         Isabelle_System.mkdirs(settings_dir + Path.explode("DockableWindowManager"))
    53 
    54         if (!(settings_dir + Path.explode("perspective.xml")).is_file) {
    55           File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"),
    56             """<DOCKING LEFT="" TOP="" RIGHT="isabelle-documentation" BOTTOM="" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />""")
    57           File.write(settings_dir + Path.explode("perspective.xml"),
    58             """<?xml version="1.0" encoding="UTF-8" ?>
    59 <!DOCTYPE PERSPECTIVE SYSTEM "perspective.dtd">
    60 <PERSPECTIVE>
    61 <VIEW PLAIN="FALSE">
    62 <GEOMETRY X="0" Y="35" WIDTH="1072" HEIGHT="787" EXT_STATE="0" />
    63 </VIEW>
    64 </PERSPECTIVE>""")
    65         }
    66 
    67 
    68         /* args */
    69 
    70         val jedit_settings =
    71           "-settings=" + File.platform_path(Path.explode("$JEDIT_SETTINGS"))
    72 
    73         val jedit_server =
    74           System.getProperty("isabelle.jedit_server") match {
    75             case null | "" => "-noserver"
    76             case name => "-server=" + name
    77           }
    78 
    79         val jedit_options =
    80           Isabelle_System.getenv_strict("JEDIT_OPTIONS").split(" +")
    81 
    82         val more_args =
    83         {
    84           args.toList.dropWhile(arg => arg.startsWith("-") && arg != "--") match {
    85             case Nil | List("--") =>
    86               args ++ Array(File.platform_path(Path.explode("$USER_HOME/Scratch.thy")))
    87             case List(":") => args.slice(0, args.size - 1)
    88             case _ => args
    89           }
    90         }
    91 
    92 
    93         /* main startup */
    94 
    95         update_environment()
    96 
    97         System.setProperty("jedit.home", File.platform_path(Path.explode("$JEDIT_HOME/dist")))
    98         System.setProperty("scala.home", File.platform_path(Path.explode("$SCALA_HOME")))
    99         System.setProperty("scala.color", "false")
   100 
   101         val jedit =
   102           Class.forName("org.gjt.sp.jedit.jEdit", true, ClassLoader.getSystemClassLoader)
   103         val jedit_main = jedit.getMethod("main", classOf[Array[String]])
   104 
   105         () => jedit_main.invoke(
   106           null, Array(jedit_settings, jedit_server) ++ jedit_options ++ more_args)
   107       }
   108       catch {
   109         case exn: Throwable =>
   110           GUI.init_laf()
   111           GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
   112           sys.exit(2)
   113       }
   114     }
   115     start()
   116   }
   117 
   118 
   119   /* adhoc update of JVM environment variables */
   120 
   121   def update_environment()
   122   {
   123     val update =
   124     {
   125       val isabelle_home = Isabelle_System.getenv("ISABELLE_HOME")
   126       val isabelle_home_user = Isabelle_System.getenv("ISABELLE_HOME_USER")
   127       val jedit_home = Isabelle_System.getenv("JEDIT_HOME")
   128       val jedit_settings = Isabelle_System.getenv("JEDIT_SETTINGS")
   129 
   130       (env0: Any) => {
   131         val env = env0.asInstanceOf[java.util.Map[String, String]]
   132         env.put("ISABELLE_HOME", File.platform_path(isabelle_home))
   133         env.put("ISABELLE_HOME_USER", File.platform_path(isabelle_home_user))
   134         env.put("JEDIT_HOME", File.platform_path(jedit_home))
   135         env.put("JEDIT_SETTINGS", File.platform_path(jedit_settings))
   136         env.remove("ISABELLE_ROOT")
   137       }
   138     }
   139 
   140     classOf[java.util.Collections].getDeclaredClasses
   141       .find(c => c.getName == "java.util.Collections$UnmodifiableMap") match
   142     {
   143       case Some(c) =>
   144         val m = c.getDeclaredField("m")
   145         m.setAccessible(true)
   146         update(m.get(System.getenv()))
   147 
   148         if (Platform.is_windows) {
   149           val ProcessEnvironment = Class.forName("java.lang.ProcessEnvironment")
   150           val field = ProcessEnvironment.getDeclaredField("theCaseInsensitiveEnvironment")
   151           field.setAccessible(true)
   152           update(field.get(null))
   153         }
   154 
   155       case None =>
   156         error("Failed to update JVM environment -- platform incompatibility")
   157     }
   158   }
   159 }