/*  Title:      Pure/System/isabelle_system.scala

     Author:     Makarius

 Fundamental Isabelle system environment: quasi-static module with

 optional init operation.

 */

 package isabelle

 import java.lang.System

 import java.util.regex.Pattern

 import java.util.Locale

 import java.io.{InputStream, OutputStream, File => JFile, BufferedReader, InputStreamReader,

   BufferedWriter, OutputStreamWriter, IOException}

 import java.awt.{GraphicsEnvironment, Font}

 import java.awt.font.TextAttribute

 import scala.io.Source

 import scala.util.matching.Regex

 import scala.collection.mutable

 object Isabelle_System

 {

   /** implicit state **/

   private case class State(standard_system: Standard_System, settings: Map[String, String])

   @volatile private var _state: Option[State] = None

   private def check_state(): State =

   {

     if (_state.isEmpty) init()  // unsynchronized check

     _state.get

   }

   def standard_system: Standard_System = check_state().standard_system

   def settings: Map[String, String] = check_state().settings

   /*

     isabelle_home precedence:

       (1) this_isabelle_home as explicit argument

       (2) ISABELLE_HOME process environment variable (e.g. inherited from running isabelle tool)

       (3) isabelle.home system property (e.g. via JVM application boot process)

   */

   def init(this_isabelle_home: String = null) = synchronized {

     if (_state.isEmpty) {

       import scala.collection.JavaConversions._

       val standard_system = new Standard_System

       val settings =

       {

         val env0 = sys.env + ("ISABELLE_JDK_HOME" -> standard_system.this_jdk_home())

         val user_home = System.getProperty("user.home")

         val env =

           if (user_home == null || env0.isDefinedAt("HOME")) env0

           else env0 + ("HOME" -> user_home)

         val isabelle_home =

           if (this_isabelle_home != null) this_isabelle_home

           else

             env.get("ISABELLE_HOME") match {

               case None | Some("") =>

                 val path = 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(standard_system.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, env, true, cmdline: _*)

               if (rc != 0) error(output)

               val entries =

                 (for (entry <- Standard_System.read_file(dump) split "\0" if entry != "") yield {

                   val i = entry.indexOf('=')

                   if (i <= 0) (entry -> "")

                   else (entry.substring(0, i) -> entry.substring(i + 1))

                 }).toMap

               entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM"

             }

           }

       _state = Some(State(standard_system, settings))

     }

   }

   /* getenv */

   def getenv(name: String): String = settings.getOrElse(name, "")

   def getenv_strict(name: String): String =

   {

     val value = getenv(name)

     if (value != "") value else error("Undefined environment variable: " + name)

   }

   /** file-system operations **/

   /* path specifications */

   def standard_path(path: Path): String = path.expand.implode

   def platform_path(path: Path): String = standard_system.jvm_path(standard_path(path))

   def platform_file(path: Path): JFile = new JFile(platform_path(path))

   def platform_file_url(raw_path: Path): String =

   {

     val path = raw_path.expand

     require(path.is_absolute)

     val s = platform_path(path).replaceAll(" ", "%20")

     if (!Platform.is_windows) "file://" + s

     else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/')

     else "file:///" + s.replace('\\', '/')

   }

   def posix_path(jvm_path: String): String = standard_system.posix_path(jvm_path)

   /* try_read */

   def try_read(paths: Seq[Path]): String =

   {

     val buf = new StringBuilder

     for {

       path <- paths

       file = platform_file(path) if file.isFile

     } { buf.append(Standard_System.read_file(file)); buf.append('\n') }

     buf.toString

   }

   /* source files */

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

   def source_file(path: Path): Option[JFile] =

   {

     if (path.is_absolute || path.is_current)

       try_file(platform_file(path))

     else {

       val pure_file = (Path.explode("~~/src/Pure") + path).file

       if (pure_file.isFile) Some(pure_file)

       else if (getenv("ML_SOURCES") != "") try_file((Path.explode("$ML_SOURCES") + path).file)

       else None

     }

   }

   /** external processes **/

   /* plain execute */

   def execute_env(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =

   {

     val cmdline =

       if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\env.exe") ++ args

       else args

     val env1 = if (env == null) settings else settings ++ env

     Standard_System.raw_execute(cwd, env1, redirect, cmdline: _*)

   }

   def execute(redirect: Boolean, args: String*): Process =

     execute_env(null, null, redirect, args: _*)

   /* managed process */

   class Managed_Process(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)

   {

     private val params =

       List(standard_path(Path.explode("~~/lib/scripts/process")), "group", "-", "no_script")

     private val proc = execute_env(cwd, env, redirect, (params ++ args):_*)

     // channels

     val stdin: BufferedWriter =

       new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, Standard_System.charset))

     val stdout: BufferedReader =

       new BufferedReader(new InputStreamReader(proc.getInputStream, Standard_System.charset))

     val stderr: BufferedReader =

       new BufferedReader(new InputStreamReader(proc.getErrorStream, Standard_System.charset))

     // signals

     private val pid = stdout.readLine

     private def kill(signal: String): Boolean =

     {

       execute(true, "kill", "-" + signal, "-" + pid).waitFor

       execute(true, "kill", "-0", "-" + pid).waitFor == 0

     }

     private def multi_kill(signal: String): Boolean =

     {

       var running = true

       var count = 10

       while (running && count > 0) {

         if (kill(signal)) {

           Thread.sleep(100)

           count -= 1

         }

         else running = false

       }

       running

     }

     def interrupt() { multi_kill("INT") }

     def terminate() { multi_kill("INT") && multi_kill("TERM") && kill("KILL"); proc.destroy }

     // JVM shutdown hook

     private val shutdown_hook = new Thread { override def run = terminate() }

     try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }

     catch { case _: IllegalStateException => }

     private def cleanup() =

       try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }

       catch { case _: IllegalStateException => }

     /* result */

     def join: Int = { val rc = proc.waitFor; cleanup(); rc }

   }

   /* bash */

   def bash_env(cwd: JFile, env: Map[String, String], script: String): (String, String, Int) =

   {

     Standard_System.with_tmp_file("isabelle_script") { script_file =>

       Standard_System.write_file(script_file, script)

       val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file.getPath))

       proc.stdin.close

       val (_, stdout) = Simple_Thread.future("bash_stdout") { Standard_System.slurp(proc.stdout) }

       val (_, stderr) = Simple_Thread.future("bash_stderr") { Standard_System.slurp(proc.stderr) }

       val rc =

         try { proc.join }

         catch { case e: InterruptedException => Thread.interrupted; proc.terminate; 130 }

       (stdout.join, stderr.join, rc)

     }

   }

   def bash(script: String): (String, String, Int) = bash_env(null, null, script)

   class Bash_Job(cwd: JFile, env: Map[String, String], script: String)

   {

     private val (thread, result) = Simple_Thread.future("bash_job") { bash_env(cwd, env, script) }

     def terminate: Unit = thread.interrupt

     def is_finished: Boolean = result.is_finished

     def join: (String, String, Int) = result.join

     override def toString: String = if (is_finished) join._3.toString else "<running>"

   }

   /* system tools */

   def isabelle_tool(name: String, args: String*): (String, Int) =

   {

     Path.split(getenv_strict("ISABELLE_TOOLS")).find { dir =>

       val file = (dir + Path.basic(name)).file

       try {

         file.isFile && file.canRead && file.canExecute &&

           !name.endsWith("~") && !name.endsWith(".orig")

       }

       catch { case _: SecurityException => false }

     } match {

       case Some(dir) =>

         val file = standard_path(dir + Path.basic(name))

         Standard_System.process_output(execute(true, (List(file) ++ args): _*))

       case None => ("Unknown Isabelle tool: " + name, 2)

     }

   }

   /** Isabelle resources **/

   /* components */

   def components(): List[Path] =

     Path.split(getenv_strict("ISABELLE_COMPONENTS"))

   /* find logics */

   def find_logics(): List[String] =

   {

     val ml_ident = getenv_strict("ML_IDENTIFIER")

     val logics = new mutable.ListBuffer[String]

     for (dir <- Path.split(getenv_strict("ISABELLE_PATH"))) {

       val files = (dir + Path.explode(ml_ident)).file.listFiles()

       if (files != null) {

         for (file <- files if file.isFile) logics += file.getName

       }

     }

     logics.toList.sorted

   }

   /* fonts */

   def get_font(family: String = "IsabelleText", size: Int = 1, bold: Boolean = false): Font =

     new Font(family, if (bold) Font.BOLD else Font.PLAIN, size)

   def install_fonts()

   {

     val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()

     for (font <- Path.split(getenv_strict("ISABELLE_FONTS")))

       ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, font.file))

   }

 }