1/*  Title:      Pure/Admin/other_isabelle.scala
2    Author:     Makarius
3
4Manage other Isabelle distributions.
5*/
6
7package isabelle
8
9
10object 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.canonical, isabelle_identifier, user_home, progress)
17}
18
19class 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  def getenv(name: String): String =
56    other_isabelle("getenv -b " + Bash.string(name)).check.out
57
58  val isabelle_home_user: Path = Path.explode(getenv("ISABELLE_HOME_USER"))
59
60  val etc: Path = isabelle_home_user + Path.explode("etc")
61  val etc_settings: Path = etc + Path.explode("settings")
62  val etc_preferences: Path = etc + Path.explode("preferences")
63
64  def copy_fonts(target_dir: Path): Unit =
65    Isabelle_Fonts.make_entries(getenv = getenv(_), hidden = true).
66      foreach(entry => File.copy(entry.path, target_dir))
67
68
69  /* components */
70
71  def init_components(
72    components_base: Path = Components.default_components_base,
73    catalogs: List[String] = Nil,
74    components: List[String] = Nil): List[String] =
75  {
76    val dir = Components.admin(isabelle_home)
77    catalogs.map(name =>
78      "init_components " + File.bash_path(components_base) + " " +
79        File.bash_path(dir + Path.basic(name))) :::
80    components.map(name =>
81      "init_component " + File.bash_path(components_base + Path.basic(name)))
82  }
83
84
85  /* settings */
86
87  def clean_settings(): Boolean =
88    if (!etc_settings.is_file) true
89    else if (File.read(etc_settings).startsWith("# generated by Isabelle")) {
90      etc_settings.file.delete; true
91    }
92    else false
93
94  def init_settings(settings: List[String])
95  {
96    if (!clean_settings())
97      error("Cannot proceed with existing user settings file: " + etc_settings)
98
99    Isabelle_System.mkdirs(etc_settings.dir)
100    File.write(etc_settings,
101      "# generated by Isabelle " + Date.now() + "\n" +
102      "#-*- shell-script -*- :mode=shellscript:\n" +
103      settings.mkString("\n", "\n", "\n"))
104  }
105
106
107  /* cleanup */
108
109  def cleanup()
110  {
111    clean_settings()
112    etc.file.delete
113    isabelle_home_user.file.delete
114  }
115}
116