src/Pure/Tools/main.scala
author wenzelm
Sat, 07 Sep 2013 17:11:44 +0200
changeset 53459 33f773731f0c
parent 53457 b7c15885fd1e
child 53460 6015a663b889
permissions -rw-r--r--
Cygwin_Init based on System_Dialog;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
50687
a8db4bf70e90 moved files;
wenzelm
parents: 48275
diff changeset
     1
/*  Title:      Pure/Tools/main.scala
47663
20e0865ae9e7 default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
20e0865ae9e7 default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff changeset
     3
53419
1c87e79bb838 main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
wenzelm
parents: 52675
diff changeset
     4
Main Isabelle application entry point.
47663
20e0865ae9e7 default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff changeset
     5
*/
20e0865ae9e7 default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff changeset
     6
20e0865ae9e7 default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff changeset
     7
package isabelle
20e0865ae9e7 default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff changeset
     8
53419
1c87e79bb838 main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
wenzelm
parents: 52675
diff changeset
     9
53449
913df2adc99c build session before start of jedit;
wenzelm
parents: 53445
diff changeset
    10
import javax.swing.SwingUtilities
53445
811db2b751ed warm start of Isabelle/jEdit from Isabelle/Scala;
wenzelm
parents: 53423
diff changeset
    11
import java.lang.{System, ClassLoader}
53419
1c87e79bb838 main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
wenzelm
parents: 52675
diff changeset
    12
import java.io.{File => JFile}
47663
20e0865ae9e7 default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff changeset
    13
20e0865ae9e7 default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff changeset
    14
20e0865ae9e7 default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff changeset
    15
object Main
20e0865ae9e7 default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff changeset
    16
{
53456
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    17
  def main(args: Array[String])
53449
913df2adc99c build session before start of jedit;
wenzelm
parents: 53445
diff changeset
    18
  {
53456
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    19
    val system_dialog = new System_Dialog
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    20
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    21
    def exit_error(exn: Throwable): Nothing =
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    22
    {
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    23
      GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    24
      system_dialog.return_code(2)
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    25
      sys.exit(system_dialog.join)
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    26
    }
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    27
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    28
    def build
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    29
    {
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    30
      try {
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    31
        GUI.init_laf()
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    32
        Isabelle_System.init()
53449
913df2adc99c build session before start of jedit;
wenzelm
parents: 53445
diff changeset
    33
53456
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    34
        val mode = Isabelle_System.getenv("JEDIT_BUILD_MODE")
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    35
        if (mode == "none")
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    36
          system_dialog.return_code(0)
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    37
        else {
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    38
          val system_mode = mode == "" || mode == "system"
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    39
          val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    40
          val options = Options.init()
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    41
          val session = Isabelle_System.default_logic(
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    42
            Isabelle_System.getenv("JEDIT_LOGIC"),
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    43
            options.string("jedit_logic"))
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    44
          Build_Dialog.dialog(options, system_dialog, system_mode, dirs, session)
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    45
        }
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    46
      }
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    47
      catch { case exn: Throwable => exit_error(exn) }
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    48
    }
53449
913df2adc99c build session before start of jedit;
wenzelm
parents: 53445
diff changeset
    49
53456
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    50
    def start
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    51
    {
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    52
      val do_start =
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    53
      {
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    54
        try {
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    55
          /* settings directory */
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    56
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    57
          val settings_dir = Path.explode("$JEDIT_SETTINGS")
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    58
          Isabelle_System.mkdirs(settings_dir + Path.explode("DockableWindowManager"))
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    59
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    60
          if (!(settings_dir + Path.explode("perspective.xml")).is_file) {
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    61
            File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"),
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    62
              """<DOCKING LEFT="" TOP="" RIGHT="" BOTTOM="isabelle-readme" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />""")
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    63
            File.write(settings_dir + Path.explode("perspective.xml"),
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    64
              """<?xml version="1.0" encoding="UTF-8" ?>
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    65
<!DOCTYPE PERSPECTIVE SYSTEM "perspective.dtd">
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    66
<PERSPECTIVE>
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    67
<VIEW PLAIN="FALSE">
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    68
<GEOMETRY X="0" Y="35" WIDTH="1072" HEIGHT="787" EXT_STATE="0" />
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    69
</VIEW>
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    70
</PERSPECTIVE>""")
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    71
          }
53449
913df2adc99c build session before start of jedit;
wenzelm
parents: 53445
diff changeset
    72
913df2adc99c build session before start of jedit;
wenzelm
parents: 53445
diff changeset
    73
53456
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    74
          /* args */
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    75
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    76
          val jedit_options =
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    77
            Isabelle_System.getenv_strict("JEDIT_OPTIONS").split(" +")
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    78
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    79
          val jedit_settings =
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    80
            Array("-settings=" + Isabelle_System.platform_path(Path.explode("$JEDIT_SETTINGS")))
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    81
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    82
          val more_args =
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    83
            if (args.isEmpty)
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    84
              Array(Isabelle_System.platform_path(Path.explode("$USER_HOME/Scratch.thy")))
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    85
            else args
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    86
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    87
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    88
          /* startup */
53445
811db2b751ed warm start of Isabelle/jEdit from Isabelle/Scala;
wenzelm
parents: 53423
diff changeset
    89
53456
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    90
          System.setProperty("jedit.home",
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    91
            Isabelle_System.platform_path(Path.explode("$JEDIT_HOME/dist")))
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    92
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    93
          System.setProperty("scala.home",
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    94
            Isabelle_System.platform_path(Path.explode("$SCALA_HOME")))
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    95
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    96
          val jedit = ClassLoader.getSystemClassLoader.loadClass("org.gjt.sp.jedit.jEdit")
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    97
          val jedit_main = jedit.getDeclaredMethod("main", classOf[Array[String]])
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    98
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
    99
          () => jedit_main.invoke(null, jedit_options ++ jedit_settings ++ more_args)
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
   100
        }
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
   101
        catch { case exn: Throwable => exit_error(exn) }
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
   102
      }
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
   103
      do_start()
d12be8f62285 Build_Dialog based on System_Dialog;
wenzelm
parents: 53449
diff changeset
   104
    }
53419
1c87e79bb838 main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
wenzelm
parents: 52675
diff changeset
   105
1c87e79bb838 main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
wenzelm
parents: 52675
diff changeset
   106
    if (Platform.is_windows) {
53459
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   107
      try {
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   108
        GUI.init_laf()
53419
1c87e79bb838 main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
wenzelm
parents: 52675
diff changeset
   109
53459
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   110
        val isabelle_home0 = System.getenv("ISABELLE_HOME_WINDOWS")
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   111
        val isabelle_home = System.getProperty("isabelle.home")
47663
20e0865ae9e7 default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff changeset
   112
53459
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   113
        if (isabelle_home0 == null || isabelle_home0 == "") {
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   114
          if (isabelle_home == null || isabelle_home == "")
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   115
            error("Unknown Isabelle home directory")
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   116
          if (!(new JFile(isabelle_home)).isDirectory)
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   117
            error("Bad Isabelle home directory: " + quote(isabelle_home))
53419
1c87e79bb838 main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
wenzelm
parents: 52675
diff changeset
   118
53459
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   119
          val cygwin_root = isabelle_home + "\\contrib\\cygwin"
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   120
          if ((new JFile(cygwin_root)).isDirectory)
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   121
            System.setProperty("cygwin.root", cygwin_root)
53422
ec97451fdf2e recovered cygwin.root from 1c87e79bb838;
wenzelm
parents: 53419
diff changeset
   122
53459
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   123
          val uninitialized_file = new JFile(cygwin_root, "isabelle\\uninitialized")
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   124
          val uninitialized = uninitialized_file.isFile && uninitialized_file.delete
53419
1c87e79bb838 main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
wenzelm
parents: 52675
diff changeset
   125
53459
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   126
          if (uninitialized)
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   127
            Cygwin_Init.filesystem(system_dialog, isabelle_home)
53419
1c87e79bb838 main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
wenzelm
parents: 52675
diff changeset
   128
        }
53459
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   129
      }
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   130
      catch { case exn: Throwable => exit_error(exn) }
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   131
    }
53445
811db2b751ed warm start of Isabelle/jEdit from Isabelle/Scala;
wenzelm
parents: 53423
diff changeset
   132
53459
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   133
    build
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   134
    val rc = system_dialog.join
33f773731f0c Cygwin_Init based on System_Dialog;
wenzelm
parents: 53457
diff changeset
   135
    if (rc == 0) start else sys.exit(rc)
53445
811db2b751ed warm start of Isabelle/jEdit from Isabelle/Scala;
wenzelm
parents: 53423
diff changeset
   136
  }
47663
20e0865ae9e7 default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff changeset
   137
}
20e0865ae9e7 default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff changeset
   138