1/*  Title:      Pure/Tools/main.scala
2    Author:     Makarius
3
4Main Isabelle application entry point.
5*/
6
7package isabelle
8
9
10import java.lang.{Class, ClassLoader}
11
12
13object 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}
160