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