src/Pure/Admin/other_isabelle.scala
author wenzelm
Sat Nov 11 16:28:15 2017 +0100 (17 months ago)
changeset 67046 897f1ac84aab
parent 67045 6c94f749410a
child 68754 8999f9143e5f
permissions -rw-r--r--
clarified settings environment;
     1 /*  Title:      Pure/Admin/other_isabelle.scala
     2     Author:     Makarius
     3 
     4 Manage other Isabelle distributions.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object Other_Isabelle
    11 {
    12   def apply(isabelle_home: Path,
    13       isabelle_identifier: String = "",
    14       user_home: Path = Path.explode("$USER_HOME"),
    15       progress: Progress = No_Progress): Other_Isabelle =
    16     new Other_Isabelle(isabelle_home, isabelle_identifier, user_home, progress)
    17 }
    18 
    19 class Other_Isabelle(
    20   val isabelle_home: Path,
    21   val isabelle_identifier: String,
    22   user_home: Path,
    23   progress: Progress)
    24 {
    25   other_isabelle =>
    26 
    27   override def toString: String = isabelle_home.toString
    28 
    29   if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined)
    30     error("Cannot initialize with enclosing ISABELLE_SETTINGS_PRESENT")
    31 
    32 
    33   /* static system */
    34 
    35   def bash(
    36       script: String,
    37       redirect: Boolean = false,
    38       echo: Boolean = false,
    39       strict: Boolean = true): Process_Result =
    40     progress.bash(
    41       "export USER_HOME=" + File.bash_path(user_home) + "\n" +
    42       Isabelle_System.export_isabelle_identifier(isabelle_identifier) + script,
    43       env = null, cwd = isabelle_home.file, redirect = redirect, echo = echo, strict = strict)
    44 
    45   def apply(
    46       cmdline: String,
    47       redirect: Boolean = false,
    48       echo: Boolean = false,
    49       strict: Boolean = true): Process_Result =
    50     bash("bin/isabelle " + cmdline, redirect = redirect, echo = echo, strict = strict)
    51 
    52   def resolve_components(echo: Boolean): Unit =
    53     other_isabelle("components -a", redirect = true, echo = echo).check
    54 
    55   val isabelle_home_user: Path =
    56     Path.explode(other_isabelle("getenv -b ISABELLE_HOME_USER").check.out)
    57 
    58   val etc_settings: Path = isabelle_home_user + Path.explode("etc/settings")
    59 
    60 
    61   /* init settings */
    62 
    63   def init_settings(components_base: String, nonfree: Boolean, more_settings: List[String])
    64   {
    65     if (etc_settings.is_file && !File.read(etc_settings).startsWith("# generated by Isabelle"))
    66       error("Cannot proceed with existing user settings file: " + etc_settings)
    67 
    68     Isabelle_System.mkdirs(etc_settings.dir)
    69     File.write(etc_settings,
    70       "# generated by Isabelle " + Date.now() + "\n" +
    71       "#-*- shell-script -*- :mode=shellscript:\n")
    72 
    73     val component_settings =
    74     {
    75       val components_base_path =
    76         if (components_base == "") isabelle_home_user.dir + Path.explode("contrib")
    77         else Path.explode(components_base).expand
    78 
    79       val catalogs =
    80         if (nonfree) List("main", "optional", "nonfree") else List("main", "optional")
    81 
    82       catalogs.map(catalog =>
    83         "init_components " + File.bash_path(components_base_path) +
    84           " \"$ISABELLE_HOME/Admin/components/" + catalog + "\"")
    85     }
    86 
    87     val settings =
    88       List(component_settings) :::
    89       (if (more_settings.isEmpty) Nil else List(more_settings))
    90 
    91     File.append(etc_settings, "\n" + cat_lines(settings.map(terminate_lines(_))))
    92   }
    93 }