src/Pure/Admin/other_isabelle.scala
changeset 77042 67da045668cc
parent 77041 4adee07a5e48
child 77044 a4380a2d6d2c
equal deleted inserted replaced
77041:4adee07a5e48 77042:67da045668cc
    23 ) {
    23 ) {
    24   other_isabelle =>
    24   other_isabelle =>
    25 
    25 
    26   override def toString: String = isabelle_home.toString
    26   override def toString: String = isabelle_home.toString
    27 
    27 
    28   if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined)
    28   if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined) {
    29     error("Cannot initialize with enclosing ISABELLE_SETTINGS_PRESENT")
    29     error("Cannot initialize with enclosing ISABELLE_SETTINGS_PRESENT")
       
    30   }
    30 
    31 
    31 
    32 
    32   /* static system */
    33   /* static system */
    33 
    34 
    34   def bash(
    35   def bash(
    35       script: String,
    36     script: String,
    36       redirect: Boolean = false,
    37     redirect: Boolean = false,
    37       echo: Boolean = false,
    38     echo: Boolean = false,
    38       strict: Boolean = true): Process_Result =
    39     strict: Boolean = true
       
    40   ): Process_Result = {
    39     progress.bash(
    41     progress.bash(
    40       "export USER_HOME=" + File.bash_path(user_home) + "\n" +
    42       "export USER_HOME=" + File.bash_path(user_home) + "\n" +
    41       Isabelle_System.export_isabelle_identifier(isabelle_identifier) + script,
    43       Isabelle_System.export_isabelle_identifier(isabelle_identifier) + script,
    42       env = null, cwd = isabelle_home.file, redirect = redirect, echo = echo, strict = strict)
    44       env = null, cwd = isabelle_home.file, redirect = redirect, echo = echo, strict = strict)
       
    45   }
    43 
    46 
    44   def apply(
    47   def apply(
    45       cmdline: String,
    48     cmdline: String,
    46       redirect: Boolean = false,
    49     redirect: Boolean = false,
    47       echo: Boolean = false,
    50     echo: Boolean = false,
    48       strict: Boolean = true): Process_Result =
    51     strict: Boolean = true
       
    52   ): Process_Result = {
    49     bash("bin/isabelle " + cmdline, redirect = redirect, echo = echo, strict = strict)
    53     bash("bin/isabelle " + cmdline, redirect = redirect, echo = echo, strict = strict)
       
    54   }
    50 
    55 
    51   def resolve_components(echo: Boolean): Unit =
    56   def resolve_components(echo: Boolean): Unit = {
    52     other_isabelle(
    57     other_isabelle(
    53       "env ISABELLE_TOOLS=" + Bash.string(Isabelle_System.getenv("ISABELLE_TOOLS")) +
    58       "env ISABELLE_TOOLS=" + Bash.string(Isabelle_System.getenv("ISABELLE_TOOLS")) +
    54       " isabelle components -a", redirect = true, echo = echo).check
    59       " isabelle components -a", redirect = true, echo = echo).check
       
    60   }
    55 
    61 
    56   def getenv(name: String): String =
    62   def getenv(name: String): String =
    57     other_isabelle("getenv -b " + Bash.string(name)).check.out
    63     other_isabelle("getenv -b " + Bash.string(name)).check.out
    58 
    64 
    59   val isabelle_home_user: Path = Path.explode(getenv("ISABELLE_HOME_USER"))
    65   val isabelle_home_user: Path = Path.explode(getenv("ISABELLE_HOME_USER"))
    85   /* settings */
    91   /* settings */
    86 
    92 
    87   def clean_settings(): Boolean =
    93   def clean_settings(): Boolean =
    88     if (!etc_settings.is_file) true
    94     if (!etc_settings.is_file) true
    89     else if (File.read(etc_settings).startsWith("# generated by Isabelle")) {
    95     else if (File.read(etc_settings).startsWith("# generated by Isabelle")) {
    90       etc_settings.file.delete; true
    96       etc_settings.file.delete
       
    97       true
    91     }
    98     }
    92     else false
    99     else false
    93 
   100 
    94   def init_settings(settings: List[String]): Unit = {
   101   def init_settings(settings: List[String]): Unit = {
    95     if (!clean_settings())
   102     if (!clean_settings()) {
    96       error("Cannot proceed with existing user settings file: " + etc_settings)
   103       error("Cannot proceed with existing user settings file: " + etc_settings)
       
   104     }
    97 
   105 
    98     Isabelle_System.make_directory(etc_settings.dir)
   106     Isabelle_System.make_directory(etc_settings.dir)
    99     File.write(etc_settings,
   107     File.write(etc_settings,
   100       "# generated by Isabelle " + Date.now() + "\n" +
   108       "# generated by Isabelle " + Date.now() + "\n" +
   101       "#-*- shell-script -*- :mode=shellscript:\n" +
   109       "#-*- shell-script -*- :mode=shellscript:\n" +