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