src/Pure/Admin/other_isabelle.scala
author wenzelm
Wed, 24 May 2017 11:39:00 +0200
changeset 65916 5b8ed310b31d
parent 65845 b8ff63149256
child 65930 9a28fc03c3fe
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64188
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Admin/other_isabelle.scala
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
     3
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
     4
Manage other Isabelle distributions.
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
     5
*/
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
     6
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
     7
package isabelle
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
     8
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
     9
64315
e48e2532ac17 proper echo;
wenzelm
parents: 64304
diff changeset
    10
class Other_Isabelle(progress: Progress, val isabelle_home: Path, val isabelle_identifier: String)
64188
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    11
{
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    12
  other_isabelle =>
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    13
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    14
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    15
  /* static system */
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    16
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    17
  def bash(script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
65916
wenzelm
parents: 65845
diff changeset
    18
    progress.bash(Isabelle_System.export_isabelle_identifier(isabelle_identifier) + script,
64315
e48e2532ac17 proper echo;
wenzelm
parents: 64304
diff changeset
    19
      env = null, cwd = isabelle_home.file, redirect = redirect, echo = echo)
64188
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    20
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    21
  def apply(cmdline: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    22
    bash("bin/isabelle " + cmdline, redirect, echo)
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    23
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    24
  def resolve_components(echo: Boolean): Unit =
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    25
    other_isabelle("components -a", redirect = true, echo = echo).check
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    26
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    27
  val isabelle_home_user: Path =
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    28
    Path.explode(other_isabelle("getenv -b ISABELLE_HOME_USER").check.out)
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    29
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    30
  val etc_settings: Path = isabelle_home_user + Path.explode("etc/settings")
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    31
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    32
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    33
  /* init settings */
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    34
65845
b8ff63149256 proper init_settings, before inspecting ML_HOME etc;
wenzelm
parents: 64315
diff changeset
    35
  def init_settings(components_base: String, nonfree: Boolean, more_settings: List[String])
64188
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    36
  {
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    37
    if (etc_settings.is_file && !File.read(etc_settings).startsWith("# generated by Isabelle"))
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    38
      error("Cannot proceed with existing user settings file: " + etc_settings)
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    39
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    40
    Isabelle_System.mkdirs(etc_settings.dir)
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    41
    File.write(etc_settings,
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    42
      "# generated by Isabelle " + Date.now() + "\n" +
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    43
      "#-*- shell-script -*- :mode=shellscript:\n")
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    44
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    45
    val component_settings =
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    46
    {
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    47
      val components_base_path =
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    48
        if (components_base == "") isabelle_home_user.dir + Path.explode("contrib")
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    49
        else Path.explode(components_base).expand
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    50
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    51
      val catalogs =
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    52
        if (nonfree) List("main", "optional", "nonfree") else List("main", "optional")
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    53
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    54
      catalogs.map(catalog =>
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    55
        "init_components " + File.bash_path(components_base_path) +
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    56
          " \"$ISABELLE_HOME/Admin/components/" + catalog + "\"")
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    57
    }
65845
b8ff63149256 proper init_settings, before inspecting ML_HOME etc;
wenzelm
parents: 64315
diff changeset
    58
b8ff63149256 proper init_settings, before inspecting ML_HOME etc;
wenzelm
parents: 64315
diff changeset
    59
    val settings =
b8ff63149256 proper init_settings, before inspecting ML_HOME etc;
wenzelm
parents: 64315
diff changeset
    60
      List(component_settings) :::
b8ff63149256 proper init_settings, before inspecting ML_HOME etc;
wenzelm
parents: 64315
diff changeset
    61
      (if (more_settings.isEmpty) Nil else List(more_settings))
b8ff63149256 proper init_settings, before inspecting ML_HOME etc;
wenzelm
parents: 64315
diff changeset
    62
b8ff63149256 proper init_settings, before inspecting ML_HOME etc;
wenzelm
parents: 64315
diff changeset
    63
    File.append(etc_settings, "\n" + cat_lines(settings.map(terminate_lines(_))))
64188
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    64
  }
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    65
}