src/Pure/System/isabelle_system.scala

more convenient get_font;

/*  Title:      Pure/System/isabelle_system.scala
    Author:     Makarius

Isabelle system support (settings environment etc.).
*/

package isabelle

import java.util.regex.Pattern
import java.util.Locale
import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream,
  BufferedInputStream, FileInputStream, BufferedReader, InputStreamReader,
  File, IOException}
import java.awt.{GraphicsEnvironment, Font}

import scala.io.Source
import scala.util.matching.Regex
import scala.collection.mutable


class Isabelle_System extends Standard_System
{
  /** Isabelle environment **/

  private val environment: Map[String, String] =
  {
    import scala.collection.JavaConversions._

    val env0 = Map(java.lang.System.getenv.toList: _*) +
      ("THIS_JAVA" -> this_java())

    val isabelle_home =
      env0.get("ISABELLE_HOME") match {
        case None | Some("") =>
          val path = java.lang.System.getProperty("isabelle.home")
          if (path == null || path == "") error("Unknown Isabelle home directory")
          else path
        case Some(path) => path
      }

    Standard_System.with_tmp_file("settings") { dump =>
        val shell_prefix =
          if (Platform.is_windows) List(platform_root + "\\bin\\bash", "-l") else Nil
        val cmdline =
          shell_prefix ::: List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString)
        val (output, rc) = Standard_System.raw_exec(null, env0, true, cmdline: _*)
        if (rc != 0) error(output)

        val entries =
          for (entry <- Source.fromFile(dump).mkString split "\0" if entry != "") yield {
            val i = entry.indexOf('=')
            if (i <= 0) (entry -> "")
            else (entry.substring(0, i) -> entry.substring(i + 1))
          }
        Map(entries: _*) +
          ("HOME" -> java.lang.System.getenv("HOME")) +
          ("PATH" -> java.lang.System.getenv("PATH"))
      }
  }


  /* external processes */

  def execute(redirect: Boolean, args: String*): Process =
  {
    val cmdline =
      if (Platform.is_windows) List(platform_root + "\\bin\\env.exe") ++ args
      else args
    Standard_System.raw_execute(null, environment, redirect, cmdline: _*)
  }


  /* getenv */

  def getenv(name: String): String =
    environment.getOrElse(if (name == "HOME") "HOME_JVM" else name, "")

  def getenv_strict(name: String): String =
  {
    val value = getenv(name)
    if (value != "") value else error("Undefined environment variable: " + name)
  }

  override def toString = getenv("ISABELLE_HOME")



  /** file path specifications **/

  /* expand_path */

  private val Root = new Regex("(//+[^/]*|/)(.*)")
  private val Only_Root = new Regex("//+[^/]*|/")

  def expand_path(isabelle_path: String): String =
  {
    val result_path = new StringBuilder
    def init(path: String): String =
    {
      path match {
        case Root(root, rest) =>
          result_path.clear
          result_path ++= root
          rest
        case _ => path
      }
    }
    def append(path: String)
    {
      val rest = init(path)
      for (p <- rest.split("/") if p != "" && p != ".") {
        if (p == "..") {
          val result = result_path.toString
          if (!Only_Root.pattern.matcher(result).matches) {
            val i = result.lastIndexOf("/")
            if (result == "")
              result_path ++= ".."
            else if (result.substring(i + 1) == "..")
              result_path ++= "/.."
            else if (i < 0)
              result_path.length = 0
            else
              result_path.length = i
          }
        }
        else {
          val len = result_path.length
          if (len > 0 && result_path(len - 1) != '/')
            result_path += '/'
          result_path ++= p
        }
      }
    }
    val rest = init(isabelle_path)
    for (p <- rest.split("/")) {
      if (p.startsWith("$")) append(getenv_strict(p.substring(1)))
      else if (p == "~") append(getenv_strict("HOME"))
      else if (p == "~~") append(getenv_strict("ISABELLE_HOME"))
      else append(p)
    }
    result_path.toString
  }


  /* platform_path */

  def platform_path(isabelle_path: String): String =
    jvm_path(expand_path(isabelle_path))

  def platform_file(path: String) = new File(platform_path(path))


  /* source files */

  private def try_file(file: File) = if (file.isFile) Some(file) else None

  def source_file(path: String): Option[File] =
  {
    if (path.startsWith("/") || path == "")
      try_file(platform_file(path))
    else {
      val pure_file = platform_file("$ISABELLE_HOME/src/Pure/" + path)
      if (pure_file.isFile) Some(pure_file)
      else if (getenv("ML_SOURCES") != "")
        try_file(platform_file("$ML_SOURCES/" + path))
      else None
    }
  }



  /** system tools **/

  def bash_output(script: String): (String, Int) =
  {
    Standard_System.with_tmp_file("isabelle_script") { script_file =>
      Standard_System.with_tmp_file("isabelle_pid") { pid_file =>
        Standard_System.with_tmp_file("isabelle_output") { output_file =>

          Standard_System.write_file(script_file, script)

          val proc = execute(true, expand_path("$ISABELLE_HOME/lib/scripts/bash"), "group",
            script_file.getPath, pid_file.getPath, output_file.getPath)

          def kill(strict: Boolean) =
          {
            val pid =
              try { Some(Standard_System.read_file(pid_file)) }
              catch { case _: IOException => None }
            if (pid.isDefined) {
              var running = true
              var count = 10
              while (running && count > 0) {
                if (execute(true, "kill", "-INT", "-" + pid.get).waitFor != 0)
                  running = false
                else {
                  Thread.sleep(100)
                  if (!strict) count -= 1
                }
              }
            }
          }

          val shutdown_hook = new Thread { override def run = kill(true) }
          Runtime.getRuntime.addShutdownHook(shutdown_hook)  // FIXME tmp files during shutdown?!?

          def cleanup() =
            try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
            catch { case _: IllegalStateException => }

          val rc =
            try {
              try { proc.waitFor }  // FIXME read stderr (!??)
              catch { case e: InterruptedException => Thread.interrupted; kill(false); throw e }
            }
            finally {
              proc.getOutputStream.close
              proc.getInputStream.close
              proc.getErrorStream.close
              proc.destroy
              cleanup()
            }

          val output =
            try { Standard_System.read_file(output_file) }
            catch { case _: IOException => "" }

          (output, rc)
        }
      }
    }
  }

  def isabelle_tool(name: String, args: String*): (String, Int) =
  {
    getenv_strict("ISABELLE_TOOLS").split(":").find { dir =>
      val file = platform_file(dir + "/" + name)
      try { file.isFile && file.canRead && file.canExecute }
      catch { case _: SecurityException => false }
    } match {
      case Some(dir) =>
        Standard_System.process_output(
          execute(true, (List(expand_path(dir + "/" + name)) ++ args): _*))
      case None => ("Unknown Isabelle tool: " + name, 2)
    }
  }


  /* named pipes */

  def mk_fifo(): String =
  {
    val (result, rc) = isabelle_tool("mkfifo")
    if (rc == 0) result.trim
    else error(result)
  }

  def rm_fifo(fifo: String)
  {
    val (result, rc) = isabelle_tool("rmfifo", fifo)
    if (rc != 0) error(result)
  }

  def fifo_stream(fifo: String): BufferedInputStream =
  {
    // blocks until writer is ready
    val stream =
      if (Platform.is_windows) {
        val proc = execute(false, "cat", fifo)
        proc.getOutputStream.close
        proc.getErrorStream.close
        proc.getInputStream
      }
      else new FileInputStream(fifo)
    new BufferedInputStream(stream)
  }



  /** Isabelle resources **/

  /* components */

  def components(): List[String] =
    getenv("ISABELLE_COMPONENTS").split(":").toList


  /* find logics */

  def find_logics(): List[String] =
  {
    val ml_ident = getenv_strict("ML_IDENTIFIER")
    val logics = new mutable.ListBuffer[String]
    for (dir <- getenv_strict("ISABELLE_PATH").split(":")) {
      val files = platform_file(dir + "/" + ml_ident).listFiles()
      if (files != null) {
        for (file <- files if file.isFile) logics += file.getName
      }
    }
    logics.toList.sortWith(_ < _)
  }


  /* symbols */

  private def read_symbols(path: String): List[String] =
  {
    val file = platform_file(path)
    if (file.isFile) Source.fromFile(file).getLines("\n").toList
    else Nil
  }
  val symbols = new Symbol.Interpretation(
    read_symbols("$ISABELLE_HOME/etc/symbols") :::
    read_symbols("$ISABELLE_HOME_USER/etc/symbols"))


  /* fonts */

  val font_family = "IsabelleText"

  def get_font(size: Int = 1, bold: Boolean = false): Font =
    new Font(font_family, if (bold) Font.BOLD else Font.PLAIN, size)

  def install_fonts()
  {
    def create_font(bold: Boolean): Font =
    {
      val name =
        if (bold) "$ISABELLE_HOME/lib/fonts/IsabelleTextBold.ttf"
        else "$ISABELLE_HOME/lib/fonts/IsabelleText.ttf"
      Font.createFont(Font.TRUETYPE_FONT, platform_file(name))
    }
    def check_font() = get_font().getFamily == font_family

    if (!check_font()) {
      val font = create_font(false)
      val bold_font = create_font(true)

      val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
      ge.registerFont(font)
      // workaround strange problem with Apple's Java 1.6 font manager
      if (bold_font.getFamily == font_family) ge.registerFont(bold_font)
      if (!check_font()) error("Failed to install IsabelleText fonts")
    }
  }
}