src/Pure/Tools/main.scala
changeset 53419 1c87e79bb838
parent 52675 f3a6b1d0915e
child 53422 ec97451fdf2e
equal deleted inserted replaced
53418:d47a7cebe6b2 53419:1c87e79bb838
     1 /*  Title:      Pure/Tools/main.scala
     1 /*  Title:      Pure/Tools/main.scala
     2     Author:     Makarius
     2     Author:     Makarius
     3 
     3 
     4 Default Isabelle application wrapper.
     4 Main Isabelle application entry point.
     5 */
     5 */
     6 
     6 
     7 package isabelle
     7 package isabelle
     8 
     8 
     9 import scala.swing.TextArea
     9 
       
    10 import java.lang.System
       
    11 import java.io.{File => JFile}
    10 
    12 
    11 
    13 
    12 object Main
    14 object Main
    13 {
    15 {
    14   def main(args: Array[String])
    16   def main(args: Array[String])
    15   {
    17   {
    16     args.toList match {
    18     def start: Unit =
    17       case "-i" :: rest =>
    19     {
    18         if (Platform.is_windows) Cygwin_Init.main(rest.toArray)
    20       val (out, rc) =
       
    21         try {
       
    22           GUI.init_laf()
       
    23           Isabelle_System.init()
       
    24           Isabelle_System.isabelle_tool("jedit", ("-s" :: "--" :: args.toList): _*)
       
    25         }
       
    26         catch { case exn: Throwable => (Exn.message(exn), 2) }
    19 
    27 
    20       case _ =>
    28       if (rc != 0)
    21         val (out, rc) =
    29         GUI.dialog(null, "Isabelle", "Isabelle output",
    22           try {
    30           GUI.scrollable_text(out + "\nReturn code: " + rc))
    23             GUI.init_laf()
    31 
    24             Isabelle_System.init()
    32       sys.exit(rc)
    25             Isabelle_System.isabelle_tool("jedit", ("-s" :: "--" :: args.toList): _*)
    33     }
       
    34 
       
    35     if (Platform.is_windows) {
       
    36       val init_isabelle_home =
       
    37         try {
       
    38           GUI.init_laf()
       
    39 
       
    40           val isabelle_home0 = System.getenv("ISABELLE_HOME_WINDOWS")
       
    41           val isabelle_home = System.getProperty("isabelle.home")
       
    42 
       
    43           if (isabelle_home0 != null && isabelle_home0 != "") None
       
    44           else {
       
    45             if (isabelle_home == null || isabelle_home == "")
       
    46               error("Unknown Isabelle home directory")
       
    47             if (!(new JFile(isabelle_home)).isDirectory)
       
    48               error("Bad Isabelle home directory: " + quote(isabelle_home))
       
    49 
       
    50             val uninitialized_file =
       
    51               new JFile(isabelle_home, "contrib\\cygwin\\isabelle\\uninitialized")
       
    52             val uninitialized = uninitialized_file.isFile && uninitialized_file.delete
       
    53 
       
    54             if (uninitialized) Some(isabelle_home) else None
    26           }
    55           }
    27           catch { case exn: Throwable => (Exn.message(exn), 2) }
    56         }
    28 
    57         catch {
    29         if (rc != 0)
    58           case exn: Throwable =>
    30           GUI.dialog(null, "Isabelle", "Isabelle output",
    59             GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
    31             GUI.scrollable_text(out + "\nReturn code: " + rc))
    60             sys.exit(2)
    32 
    61         }
    33         sys.exit(rc)
    62       init_isabelle_home match {
       
    63         case Some(isabelle_home) =>
       
    64           GUI.dialog(null, "Isabelle", GUI.scrollable_text("OK"))
       
    65           Swing_Thread.later { Cygwin_Init.main_frame(isabelle_home, start) }
       
    66         case None => start
       
    67       }
    34     }
    68     }
       
    69     else start
    35   }
    70   }
    36 }
    71 }
    37 
    72