/*  Title:      Pure/System/isabelle_system.scala

     Author:     Makarius

 Isabelle system support -- basic Cygwin/Posix compatibility.

 */

 package isabelle

 import java.util.regex.{Pattern, Matcher}

 import java.io.{BufferedReader, InputStreamReader, FileInputStream, File, IOException}

 import scala.io.Source

 class IsabelleSystem {

   val charset = "UTF-8"

   /* Isabelle environment settings */

   private val environment = System.getenv

   def getenv(name: String) = {

     val value = environment.get(if (name == "HOME") "HOME_JVM" else name)

     if (value != null) value else ""

   }

   def getenv_strict(name: String) = {

     val value = getenv(name)

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

   }

   val is_cygwin = Pattern.matches(".*-cygwin", getenv_strict("ML_PLATFORM"))

   /* file path specifications */

   private val cygdrive_pattern = Pattern.compile("/cygdrive/([a-zA-Z])($|/.*)")

   def platform_path(source_path: String) = {

     val result_path = new StringBuilder

     def init(path: String) = {

       val cygdrive = cygdrive_pattern.matcher(path)

       if (cygdrive.matches) {

         result_path.length = 0

         result_path.append(cygdrive.group(1))

         result_path.append(":")

         result_path.append(File.separator)

         cygdrive.group(2)

       }

       else if (path.startsWith("/")) {

         result_path.length = 0

         result_path.append(getenv_strict("ISABELLE_ROOT_JVM"))

         path.substring(1)

       }

       else path

     }

     def append(path: String) = {

       for (p <- init(path).split("/")) {

         if (p != "") {

           val len = result_path.length

           if (len > 0 && result_path(len - 1) != File.separatorChar)

             result_path.append(File.separator)

           result_path.append(p)

         }

       }

     }

     for (p <- init(source_path).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

   }

   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 == "ML") None

     else if (path.startsWith("/") || path == "")

       try_file(platform_file(path))

     else {

       val pure_file = platform_file("~~/src/Pure/" + path)

       if (pure_file.isFile) Some(pure_file)

       else if (getenv("ML_SOURCES") != "")

         try_file(platform_file("$ML_SOURCES/" + path))

       else None

     }

   }

   /* shell processes */

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

     val cmdline = new java.util.LinkedList[String]

     if (is_cygwin) cmdline.add(platform_path("/bin/env"))

     for (s <- args) cmdline.add(s)

     val proc = new ProcessBuilder(cmdline)

     proc.environment.clear

     proc.environment.putAll(environment)

     proc.redirectErrorStream(redirect)

     proc.start

   }

   /* Isabelle tools (non-interactive) */

   def isabelle_tool(args: String*) = {

     val proc =

       try { execute(true, (List(getenv_strict("ISABELLE_TOOL")) ++ args): _*) }

       catch { case e: IOException => error(e.getMessage) }

     proc.getOutputStream.close

     val output = Source.fromInputStream(proc.getInputStream, charset).mkString

     val rc = proc.waitFor

     (output, rc)

   }

   /* named pipes */

   def mk_fifo() = {

     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_reader(fifo: String) = {

     // blocks until writer is ready

     val stream =

       if (is_cygwin) execute(false, "cat", fifo).getInputStream

       else new FileInputStream(fifo)

     new BufferedReader(new InputStreamReader(stream, charset))

   }

   /* find logics */

   def find_logics() = {

     val ml_ident = getenv_strict("ML_IDENTIFIER")

     var logics: Set[String] = Set()

     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.sort(_ < _)

   }

   /* symbols */

   private def read_symbols(path: String) = {

     val file = new File(platform_path(path))

     if (file.isFile) Source.fromFile(file).getLines

     else Iterator.empty

   }

   val symbols = new Symbol.Interpretation(

     read_symbols("$ISABELLE_HOME/etc/symbols") ++

     read_symbols("$ISABELLE_HOME_USER/etc/symbols"))

 }