src/Pure/Admin/other_isabelle.scala
author wenzelm
Thu Oct 13 15:17:10 2016 +0200 (2016-10-13)
changeset 64189 dfb63036c4f6
parent 64188 f88bae1922c4
child 64201 c3edc64e219d
permissions -rw-r--r--
tuned signature;
copy_dir using *this* Isabelle_System: note that File.bash_path is already expanded, but no variables are used here;
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@64188
    10
private class Other_Isabelle(progress: Progress, isabelle_home: Path, isabelle_identifier: String)
wenzelm@64188
    11
{
wenzelm@64188
    12
  other_isabelle =>
wenzelm@64188
    13
wenzelm@64188
    14
wenzelm@64188
    15
  /* static system */
wenzelm@64188
    16
wenzelm@64188
    17
  def bash(script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
wenzelm@64188
    18
    Isabelle_System.bash(
wenzelm@64188
    19
      "export ISABELLE_IDENTIFIER=" + File.bash_string(isabelle_identifier) + "\n" + script,
wenzelm@64188
    20
      env = null, cwd = isabelle_home.file, redirect = redirect,
wenzelm@64188
    21
      progress_stdout = progress.echo_if(echo, _),
wenzelm@64188
    22
      progress_stderr = progress.echo_if(echo, _))
wenzelm@64188
    23
wenzelm@64188
    24
  def apply(cmdline: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
wenzelm@64188
    25
    bash("bin/isabelle " + cmdline, redirect, echo)
wenzelm@64188
    26
wenzelm@64188
    27
  def resolve_components(echo: Boolean): Unit =
wenzelm@64188
    28
    other_isabelle("components -a", redirect = true, echo = echo).check
wenzelm@64188
    29
wenzelm@64188
    30
  val isabelle_home_user: Path =
wenzelm@64188
    31
    Path.explode(other_isabelle("getenv -b ISABELLE_HOME_USER").check.out)
wenzelm@64188
    32
wenzelm@64188
    33
  val etc_settings: Path = isabelle_home_user + Path.explode("etc/settings")
wenzelm@64188
    34
wenzelm@64188
    35
wenzelm@64188
    36
  /* init settings */
wenzelm@64188
    37
wenzelm@64188
    38
  def init_settings(components_base: String, nonfree: Boolean)
wenzelm@64188
    39
  {
wenzelm@64188
    40
    if (etc_settings.is_file && !File.read(etc_settings).startsWith("# generated by Isabelle"))
wenzelm@64188
    41
      error("Cannot proceed with existing user settings file: " + etc_settings)
wenzelm@64188
    42
wenzelm@64188
    43
    Isabelle_System.mkdirs(etc_settings.dir)
wenzelm@64188
    44
    File.write(etc_settings,
wenzelm@64188
    45
      "# generated by Isabelle " + Date.now() + "\n" +
wenzelm@64188
    46
      "#-*- shell-script -*- :mode=shellscript:\n")
wenzelm@64188
    47
wenzelm@64188
    48
    val component_settings =
wenzelm@64188
    49
    {
wenzelm@64188
    50
      val components_base_path =
wenzelm@64188
    51
        if (components_base == "") isabelle_home_user.dir + Path.explode("contrib")
wenzelm@64188
    52
        else Path.explode(components_base).expand
wenzelm@64188
    53
wenzelm@64188
    54
      val catalogs =
wenzelm@64188
    55
        if (nonfree) List("main", "optional", "nonfree") else List("main", "optional")
wenzelm@64188
    56
wenzelm@64188
    57
      catalogs.map(catalog =>
wenzelm@64188
    58
        "init_components " + File.bash_path(components_base_path) +
wenzelm@64188
    59
          " \"$ISABELLE_HOME/Admin/components/" + catalog + "\"")
wenzelm@64188
    60
    }
wenzelm@64188
    61
    File.append(etc_settings, "\n" + terminate_lines(component_settings))
wenzelm@64188
    62
  }
wenzelm@64188
    63
}