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