src/Tools/jEdit/src/jedit_main.scala
author wenzelm
Sat, 25 May 2013 17:40:44 +0200
changeset 52147 9943f8067f11
parent 51617 4e49bba9772d
child 53439 5bef05f5ed58
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
49600
2b114b9d9d34 some support for jEdit warmstart;
wenzelm
parents:
diff changeset
     1
/*  Title:      Tools/jEdit/src/jedit_main.scala
2b114b9d9d34 some support for jEdit warmstart;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
2b114b9d9d34 some support for jEdit warmstart;
wenzelm
parents:
diff changeset
     3
2b114b9d9d34 some support for jEdit warmstart;
wenzelm
parents:
diff changeset
     4
Main entry point from running JVM.
2b114b9d9d34 some support for jEdit warmstart;
wenzelm
parents:
diff changeset
     5
*/
2b114b9d9d34 some support for jEdit warmstart;
wenzelm
parents:
diff changeset
     6
2b114b9d9d34 some support for jEdit warmstart;
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
2b114b9d9d34 some support for jEdit warmstart;
wenzelm
parents:
diff changeset
     8
2b114b9d9d34 some support for jEdit warmstart;
wenzelm
parents:
diff changeset
     9
2b114b9d9d34 some support for jEdit warmstart;
wenzelm
parents:
diff changeset
    10
import isabelle._
2b114b9d9d34 some support for jEdit warmstart;
wenzelm
parents:
diff changeset
    11
2b114b9d9d34 some support for jEdit warmstart;
wenzelm
parents:
diff changeset
    12
2b114b9d9d34 some support for jEdit warmstart;
wenzelm
parents:
diff changeset
    13
import org.gjt.sp.jedit.jEdit
2b114b9d9d34 some support for jEdit warmstart;
wenzelm
parents:
diff changeset
    14
2b114b9d9d34 some support for jEdit warmstart;
wenzelm
parents:
diff changeset
    15
2b114b9d9d34 some support for jEdit warmstart;
wenzelm
parents:
diff changeset
    16
object JEdit_Main
2b114b9d9d34 some support for jEdit warmstart;
wenzelm
parents:
diff changeset
    17
{
2b114b9d9d34 some support for jEdit warmstart;
wenzelm
parents:
diff changeset
    18
  def main(args: Array[String])
2b114b9d9d34 some support for jEdit warmstart;
wenzelm
parents:
diff changeset
    19
  {
51617
4e49bba9772d tuned signature -- concentrate GUI tools;
wenzelm
parents: 49600
diff changeset
    20
    GUI.init_laf()
49600
2b114b9d9d34 some support for jEdit warmstart;
wenzelm
parents:
diff changeset
    21
    Isabelle_System.init()
2b114b9d9d34 some support for jEdit warmstart;
wenzelm
parents:
diff changeset
    22
2b114b9d9d34 some support for jEdit warmstart;
wenzelm
parents:
diff changeset
    23
    System.setProperty("jedit.home",
2b114b9d9d34 some support for jEdit warmstart;
wenzelm
parents:
diff changeset
    24
      Isabelle_System.platform_path(Path.explode("$JEDIT_HOME/dist")))
2b114b9d9d34 some support for jEdit warmstart;
wenzelm
parents:
diff changeset
    25
2b114b9d9d34 some support for jEdit warmstart;
wenzelm
parents:
diff changeset
    26
    // FIXME properties from JEDIT_JAVA_OPTIONS JEDIT_SYSTEM_OPTIONS
2b114b9d9d34 some support for jEdit warmstart;
wenzelm
parents:
diff changeset
    27
    val jedit_options = Isabelle_System.getenv_strict("JEDIT_OPTIONS").split(" +")
2b114b9d9d34 some support for jEdit warmstart;
wenzelm
parents:
diff changeset
    28
    val jedit_settings =
2b114b9d9d34 some support for jEdit warmstart;
wenzelm
parents:
diff changeset
    29
      Array("-settings=" + Isabelle_System.platform_path(Path.explode("$JEDIT_SETTINGS")))
2b114b9d9d34 some support for jEdit warmstart;
wenzelm
parents:
diff changeset
    30
    jEdit.main(jedit_options ++ jedit_settings ++ args)
2b114b9d9d34 some support for jEdit warmstart;
wenzelm
parents:
diff changeset
    31
  }
2b114b9d9d34 some support for jEdit warmstart;
wenzelm
parents:
diff changeset
    32
}
2b114b9d9d34 some support for jEdit warmstart;
wenzelm
parents:
diff changeset
    33