src/Pure/Admin/other_isabelle.scala
author wenzelm
Tue, 21 Apr 2020 22:19:59 +0200
changeset 71777 3875815f5967
parent 71726 a5fda30edae2
child 72375 e48d93811ed7
permissions -rw-r--r--
clarified signature: avoid clash with Isabelle/Scala Term.OFCLASS on case-insensible file-system;
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
67045
6c94f749410a tuned signature;
wenzelm
parents: 65930
diff changeset
    10
object Other_Isabelle
6c94f749410a tuned signature;
wenzelm
parents: 65930
diff changeset
    11
{
6c94f749410a tuned signature;
wenzelm
parents: 65930
diff changeset
    12
  def apply(isabelle_home: Path,
67046
897f1ac84aab clarified settings environment;
wenzelm
parents: 67045
diff changeset
    13
      isabelle_identifier: String = "",
897f1ac84aab clarified settings environment;
wenzelm
parents: 67045
diff changeset
    14
      user_home: Path = Path.explode("$USER_HOME"),
71726
a5fda30edae2 clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents: 71601
diff changeset
    15
      progress: Progress = new Progress): Other_Isabelle =
69408
fb26935838c7 more robust, notably for macos /var vs. /private/var;
wenzelm
parents: 69404
diff changeset
    16
    new Other_Isabelle(isabelle_home.canonical, isabelle_identifier, user_home, progress)
67045
6c94f749410a tuned signature;
wenzelm
parents: 65930
diff changeset
    17
}
6c94f749410a tuned signature;
wenzelm
parents: 65930
diff changeset
    18
6c94f749410a tuned signature;
wenzelm
parents: 65930
diff changeset
    19
class Other_Isabelle(
6c94f749410a tuned signature;
wenzelm
parents: 65930
diff changeset
    20
  val isabelle_home: Path,
6c94f749410a tuned signature;
wenzelm
parents: 65930
diff changeset
    21
  val isabelle_identifier: String,
67046
897f1ac84aab clarified settings environment;
wenzelm
parents: 67045
diff changeset
    22
  user_home: Path,
67045
6c94f749410a tuned signature;
wenzelm
parents: 65930
diff changeset
    23
  progress: Progress)
64188
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    24
{
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    25
  other_isabelle =>
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    26
69404
de88761edbe2 clarified absolute isabelle_home and (implicitly) isabelle_home_user;
wenzelm
parents: 69401
diff changeset
    27
  override def toString: String = isabelle_home.toString
67046
897f1ac84aab clarified settings environment;
wenzelm
parents: 67045
diff changeset
    28
897f1ac84aab clarified settings environment;
wenzelm
parents: 67045
diff changeset
    29
  if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined)
897f1ac84aab clarified settings environment;
wenzelm
parents: 67045
diff changeset
    30
    error("Cannot initialize with enclosing ISABELLE_SETTINGS_PRESENT")
897f1ac84aab clarified settings environment;
wenzelm
parents: 67045
diff changeset
    31
64188
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    32
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    33
  /* static system */
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    34
65930
9a28fc03c3fe tuned signature;
wenzelm
parents: 65916
diff changeset
    35
  def bash(
9a28fc03c3fe tuned signature;
wenzelm
parents: 65916
diff changeset
    36
      script: String,
9a28fc03c3fe tuned signature;
wenzelm
parents: 65916
diff changeset
    37
      redirect: Boolean = false,
9a28fc03c3fe tuned signature;
wenzelm
parents: 65916
diff changeset
    38
      echo: Boolean = false,
9a28fc03c3fe tuned signature;
wenzelm
parents: 65916
diff changeset
    39
      strict: Boolean = true): Process_Result =
67046
897f1ac84aab clarified settings environment;
wenzelm
parents: 67045
diff changeset
    40
    progress.bash(
897f1ac84aab clarified settings environment;
wenzelm
parents: 67045
diff changeset
    41
      "export USER_HOME=" + File.bash_path(user_home) + "\n" +
897f1ac84aab clarified settings environment;
wenzelm
parents: 67045
diff changeset
    42
      Isabelle_System.export_isabelle_identifier(isabelle_identifier) + script,
65930
9a28fc03c3fe tuned signature;
wenzelm
parents: 65916
diff changeset
    43
      env = null, cwd = isabelle_home.file, redirect = redirect, echo = echo, strict = strict)
64188
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    44
65930
9a28fc03c3fe tuned signature;
wenzelm
parents: 65916
diff changeset
    45
  def apply(
9a28fc03c3fe tuned signature;
wenzelm
parents: 65916
diff changeset
    46
      cmdline: String,
9a28fc03c3fe tuned signature;
wenzelm
parents: 65916
diff changeset
    47
      redirect: Boolean = false,
9a28fc03c3fe tuned signature;
wenzelm
parents: 65916
diff changeset
    48
      echo: Boolean = false,
9a28fc03c3fe tuned signature;
wenzelm
parents: 65916
diff changeset
    49
      strict: Boolean = true): Process_Result =
9a28fc03c3fe tuned signature;
wenzelm
parents: 65916
diff changeset
    50
    bash("bin/isabelle " + cmdline, redirect = redirect, echo = echo, strict = strict)
64188
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    51
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    52
  def resolve_components(echo: Boolean): Unit =
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    53
    other_isabelle("components -a", redirect = true, echo = echo).check
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    54
69166
5c553c48c0e5 tuned signature;
wenzelm
parents: 68754
diff changeset
    55
  def getenv(name: String): String =
5c553c48c0e5 tuned signature;
wenzelm
parents: 68754
diff changeset
    56
    other_isabelle("getenv -b " + Bash.string(name)).check.out
5c553c48c0e5 tuned signature;
wenzelm
parents: 68754
diff changeset
    57
5c553c48c0e5 tuned signature;
wenzelm
parents: 68754
diff changeset
    58
  val isabelle_home_user: Path = Path.explode(getenv("ISABELLE_HOME_USER"))
64188
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    59
68754
8999f9143e5f clarified signature;
wenzelm
parents: 67046
diff changeset
    60
  val etc: Path = isabelle_home_user + Path.explode("etc")
8999f9143e5f clarified signature;
wenzelm
parents: 67046
diff changeset
    61
  val etc_settings: Path = etc + Path.explode("settings")
8999f9143e5f clarified signature;
wenzelm
parents: 67046
diff changeset
    62
  val etc_preferences: Path = etc + Path.explode("preferences")
64188
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    63
69360
dc9a39c3f75d more explicit Isabelle_Fonts.Entry;
wenzelm
parents: 69355
diff changeset
    64
  def copy_fonts(target_dir: Path): Unit =
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 69434
diff changeset
    65
    Isabelle_Fonts.make_entries(getenv = getenv, hidden = true).
69360
dc9a39c3f75d more explicit Isabelle_Fonts.Entry;
wenzelm
parents: 69355
diff changeset
    66
      foreach(entry => File.copy(entry.path, target_dir))
64188
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    67
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69166
diff changeset
    68
69388
fc58534bc475 clarified component settings;
wenzelm
parents: 69387
diff changeset
    69
  /* components */
fc58534bc475 clarified component settings;
wenzelm
parents: 69387
diff changeset
    70
fc58534bc475 clarified component settings;
wenzelm
parents: 69387
diff changeset
    71
  def init_components(
69434
b93404a4c3dd clarified settings and defaults;
wenzelm
parents: 69408
diff changeset
    72
    components_base: Path = Components.default_components_base,
69396
56bea34e0f8e clarified signature;
wenzelm
parents: 69395
diff changeset
    73
    catalogs: List[String] = Nil,
56bea34e0f8e clarified signature;
wenzelm
parents: 69395
diff changeset
    74
    components: List[String] = Nil): List[String] =
69388
fc58534bc475 clarified component settings;
wenzelm
parents: 69387
diff changeset
    75
  {
69404
de88761edbe2 clarified absolute isabelle_home and (implicitly) isabelle_home_user;
wenzelm
parents: 69401
diff changeset
    76
    val dir = Components.admin(isabelle_home)
69396
56bea34e0f8e clarified signature;
wenzelm
parents: 69395
diff changeset
    77
    catalogs.map(name =>
69434
b93404a4c3dd clarified settings and defaults;
wenzelm
parents: 69408
diff changeset
    78
      "init_components " + File.bash_path(components_base) + " " +
b93404a4c3dd clarified settings and defaults;
wenzelm
parents: 69408
diff changeset
    79
        File.bash_path(dir + Path.basic(name))) :::
69396
56bea34e0f8e clarified signature;
wenzelm
parents: 69395
diff changeset
    80
    components.map(name =>
69434
b93404a4c3dd clarified settings and defaults;
wenzelm
parents: 69408
diff changeset
    81
      "init_component " + File.bash_path(components_base + Path.basic(name)))
69388
fc58534bc475 clarified component settings;
wenzelm
parents: 69387
diff changeset
    82
  }
fc58534bc475 clarified component settings;
wenzelm
parents: 69387
diff changeset
    83
fc58534bc475 clarified component settings;
wenzelm
parents: 69387
diff changeset
    84
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69166
diff changeset
    85
  /* settings */
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69166
diff changeset
    86
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69166
diff changeset
    87
  def clean_settings(): Boolean =
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69166
diff changeset
    88
    if (!etc_settings.is_file) true
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69166
diff changeset
    89
    else if (File.read(etc_settings).startsWith("# generated by Isabelle")) {
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69166
diff changeset
    90
      etc_settings.file.delete; true
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69166
diff changeset
    91
    }
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69166
diff changeset
    92
    else false
64188
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    93
69388
fc58534bc475 clarified component settings;
wenzelm
parents: 69387
diff changeset
    94
  def init_settings(settings: List[String])
64188
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    95
  {
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69166
diff changeset
    96
    if (!clean_settings())
64188
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    97
      error("Cannot proceed with existing user settings file: " + etc_settings)
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    98
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
    99
    Isabelle_System.mkdirs(etc_settings.dir)
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
   100
    File.write(etc_settings,
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
   101
      "# generated by Isabelle " + Date.now() + "\n" +
69388
fc58534bc475 clarified component settings;
wenzelm
parents: 69387
diff changeset
   102
      "#-*- shell-script -*- :mode=shellscript:\n" +
fc58534bc475 clarified component settings;
wenzelm
parents: 69387
diff changeset
   103
      settings.mkString("\n", "\n", "\n"))
64188
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
   104
  }
69168
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69166
diff changeset
   105
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69166
diff changeset
   106
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69166
diff changeset
   107
  /* cleanup */
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69166
diff changeset
   108
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69166
diff changeset
   109
  def cleanup()
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69166
diff changeset
   110
  {
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69166
diff changeset
   111
    clean_settings()
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69166
diff changeset
   112
    etc.file.delete
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69166
diff changeset
   113
    isabelle_home_user.file.delete
68816d1c73a7 eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting;
wenzelm
parents: 69166
diff changeset
   114
  }
64188
f88bae1922c4 clarified modules;
wenzelm
parents:
diff changeset
   115
}