src/Pure/Tools/main.scala
changeset 53456 d12be8f62285
parent 53449 913df2adc99c
child 53457 b7c15885fd1e
equal deleted inserted replaced
53455:e9a3390217b3 53456:d12be8f62285
    12 import java.io.{File => JFile}
    12 import java.io.{File => JFile}
    13 
    13 
    14 
    14 
    15 object Main
    15 object Main
    16 {
    16 {
    17   /* auxiliary dialogs */
       
    18 
       
    19   private def exit_error(exn: Throwable): Nothing =
       
    20   {
       
    21     GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
       
    22     sys.exit(2)
       
    23   }
       
    24 
       
    25   private def continue(body: => Unit)(rc: Int)
    17   private def continue(body: => Unit)(rc: Int)
    26   {
    18   {
    27     if (rc != 0) sys.exit(rc)
    19     if (rc != 0) sys.exit(rc)
    28     else if (SwingUtilities.isEventDispatchThread())
    20     else if (SwingUtilities.isEventDispatchThread())
    29       Simple_Thread.fork("Isabelle") { body }
    21       Simple_Thread.fork("Isabelle") { body }
    30     else body
    22     else body
    31   }
    23   }
    32 
    24 
    33   private def build_dialog(cont: Int => Unit)
    25   def main(args: Array[String])
    34   {
    26   {
    35     try {
    27     val system_dialog = new System_Dialog
    36       GUI.init_laf()
       
    37       Isabelle_System.init()
       
    38 
    28 
    39       val mode = Isabelle_System.getenv("JEDIT_BUILD_MODE")
    29     def exit_error(exn: Throwable): Nothing =
    40       if (mode == "none") cont(0)
    30     {
    41       else {
    31       GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
    42         val system_mode = mode == "" || mode == "system"
    32       system_dialog.return_code(2)
    43         val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
    33       sys.exit(system_dialog.join)
    44         val options = Options.init()
    34     }
    45         val session = Isabelle_System.default_logic(
       
    46           Isabelle_System.getenv("JEDIT_LOGIC"),
       
    47           options.string("jedit_logic"))
       
    48 
    35 
    49         if (!Build_Dialog.dialog(options, system_mode, dirs, session, cont))
    36     def run
    50           cont(0)
    37     {
       
    38       build
       
    39       if (system_dialog.join == 0) start
       
    40     }
       
    41 
       
    42     def build
       
    43     {
       
    44       try {
       
    45         GUI.init_laf()
       
    46         Isabelle_System.init()
       
    47 
       
    48         val mode = Isabelle_System.getenv("JEDIT_BUILD_MODE")
       
    49         if (mode == "none")
       
    50           system_dialog.return_code(0)
       
    51         else {
       
    52           val system_mode = mode == "" || mode == "system"
       
    53           val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
       
    54           val options = Options.init()
       
    55           val session = Isabelle_System.default_logic(
       
    56             Isabelle_System.getenv("JEDIT_LOGIC"),
       
    57             options.string("jedit_logic"))
       
    58           Build_Dialog.dialog(options, system_dialog, system_mode, dirs, session)
       
    59         }
    51       }
    60       }
       
    61       catch { case exn: Throwable => exit_error(exn) }
    52     }
    62     }
    53     catch { case exn: Throwable => exit_error(exn) }
    63 
    54   }
    64     def start
       
    65     {
       
    66       val do_start =
       
    67       {
       
    68         try {
       
    69           /* settings directory */
       
    70 
       
    71           val settings_dir = Path.explode("$JEDIT_SETTINGS")
       
    72           Isabelle_System.mkdirs(settings_dir + Path.explode("DockableWindowManager"))
       
    73 
       
    74           if (!(settings_dir + Path.explode("perspective.xml")).is_file) {
       
    75             File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"),
       
    76               """<DOCKING LEFT="" TOP="" RIGHT="" BOTTOM="isabelle-readme" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />""")
       
    77             File.write(settings_dir + Path.explode("perspective.xml"),
       
    78               """<?xml version="1.0" encoding="UTF-8" ?>
       
    79 <!DOCTYPE PERSPECTIVE SYSTEM "perspective.dtd">
       
    80 <PERSPECTIVE>
       
    81 <VIEW PLAIN="FALSE">
       
    82 <GEOMETRY X="0" Y="35" WIDTH="1072" HEIGHT="787" EXT_STATE="0" />
       
    83 </VIEW>
       
    84 </PERSPECTIVE>""")
       
    85           }
    55 
    86 
    56 
    87 
    57   /* main entry point */
    88           /* args */
    58 
    89 
    59   def main(args: Array[String])
    90           val jedit_options =
    60   {
    91             Isabelle_System.getenv_strict("JEDIT_OPTIONS").split(" +")
    61     def start { start_jedit(ClassLoader.getSystemClassLoader, args) }
    92 
    62     def build { build_dialog(continue(start)) }
    93           val jedit_settings =
       
    94             Array("-settings=" + Isabelle_System.platform_path(Path.explode("$JEDIT_SETTINGS")))
       
    95 
       
    96           val more_args =
       
    97             if (args.isEmpty)
       
    98               Array(Isabelle_System.platform_path(Path.explode("$USER_HOME/Scratch.thy")))
       
    99             else args
       
   100 
       
   101 
       
   102           /* startup */
       
   103 
       
   104           System.setProperty("jedit.home",
       
   105             Isabelle_System.platform_path(Path.explode("$JEDIT_HOME/dist")))
       
   106 
       
   107           System.setProperty("scala.home",
       
   108             Isabelle_System.platform_path(Path.explode("$SCALA_HOME")))
       
   109 
       
   110           val jedit = ClassLoader.getSystemClassLoader.loadClass("org.gjt.sp.jedit.jEdit")
       
   111           val jedit_main = jedit.getDeclaredMethod("main", classOf[Array[String]])
       
   112 
       
   113           () => jedit_main.invoke(null, jedit_options ++ jedit_settings ++ more_args)
       
   114         }
       
   115         catch { case exn: Throwable => exit_error(exn) }
       
   116       }
       
   117       do_start()
       
   118     }
    63 
   119 
    64     if (Platform.is_windows) {
   120     if (Platform.is_windows) {
    65       val init_isabelle_home =
   121       val init_isabelle_home =
    66         try {
   122         try {
    67           GUI.init_laf()
   123           GUI.init_laf()
    88         }
   144         }
    89         catch { case exn: Throwable => exit_error(exn) }
   145         catch { case exn: Throwable => exit_error(exn) }
    90 
   146 
    91       init_isabelle_home match {
   147       init_isabelle_home match {
    92         case Some(isabelle_home) =>
   148         case Some(isabelle_home) =>
    93           Swing_Thread.later { Cygwin_Init.main_frame(isabelle_home, continue(build)) }
   149           Swing_Thread.later { Cygwin_Init.main_frame(isabelle_home, continue(run)) }
    94         case None => build
   150         case None => run
    95       }
   151       }
    96     }
   152     }
    97     else build
   153     else run
    98   }
       
    99 
       
   100 
       
   101   /* warm start of Isabelle/jEdit */
       
   102 
       
   103   def start_jedit(loader: ClassLoader, args: Array[String])
       
   104   {
       
   105     val start =
       
   106     {
       
   107       try {
       
   108         GUI.init_laf()
       
   109         Isabelle_System.init()
       
   110 
       
   111 
       
   112         /* settings directory */
       
   113 
       
   114         val settings_dir = Path.explode("$JEDIT_SETTINGS")
       
   115         Isabelle_System.mkdirs(settings_dir + Path.explode("DockableWindowManager"))
       
   116 
       
   117         if (!(settings_dir + Path.explode("perspective.xml")).is_file) {
       
   118           File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"),
       
   119             """<DOCKING LEFT="" TOP="" RIGHT="" BOTTOM="isabelle-readme" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />""")
       
   120           File.write(settings_dir + Path.explode("perspective.xml"),
       
   121             """<?xml version="1.0" encoding="UTF-8" ?>
       
   122 <!DOCTYPE PERSPECTIVE SYSTEM "perspective.dtd">
       
   123 <PERSPECTIVE>
       
   124 <VIEW PLAIN="FALSE">
       
   125 <GEOMETRY X="0" Y="35" WIDTH="1072" HEIGHT="787" EXT_STATE="0" />
       
   126 </VIEW>
       
   127 </PERSPECTIVE>""")
       
   128         }
       
   129 
       
   130 
       
   131         /* args */
       
   132 
       
   133         val jedit_options =
       
   134           Isabelle_System.getenv_strict("JEDIT_OPTIONS").split(" +")
       
   135 
       
   136         val jedit_settings =
       
   137           Array("-settings=" + Isabelle_System.platform_path(Path.explode("$JEDIT_SETTINGS")))
       
   138 
       
   139         val more_args =
       
   140           if (args.isEmpty)
       
   141             Array(Isabelle_System.platform_path(Path.explode("$USER_HOME/Scratch.thy")))
       
   142           else args
       
   143 
       
   144 
       
   145         /* startup */
       
   146 
       
   147         System.setProperty("jedit.home",
       
   148           Isabelle_System.platform_path(Path.explode("$JEDIT_HOME/dist")))
       
   149 
       
   150         System.setProperty("scala.home",
       
   151           Isabelle_System.platform_path(Path.explode("$SCALA_HOME")))
       
   152 
       
   153         val jedit = loader.loadClass("org.gjt.sp.jedit.jEdit")
       
   154         val jedit_main = jedit.getDeclaredMethod("main", classOf[Array[String]])
       
   155 
       
   156         () => jedit_main.invoke(null, jedit_options ++ jedit_settings ++ more_args)
       
   157       }
       
   158       catch { case exn: Throwable => exit_error(exn) }
       
   159     }
       
   160     start()
       
   161   }
   154   }
   162 }
   155 }
   163 
   156