# HG changeset patch
# User wenzelm
# Date 1230386250 -3600
# Node ID d4058295affbdc5b4194d57a2dfacec94b23df67
# Parent  c14c9a41f1ac022e18aa9e0dcfa8310e9268596d
proper class IsabelleSystem -- no longer static;
tuned;

diff -r c14c9a41f1ac -r d4058295affb src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Sat Dec 27 11:54:08 2008 +0100
+++ b/src/Pure/General/symbol.scala	Sat Dec 27 14:57:30 2008 +0100
@@ -78,7 +78,7 @@
 
   /** Symbol interpretation **/
 
-  class Interpretation {
+  class Interpretation(isabelle_system: IsabelleSystem) {
 
     private var symbols = new HashMap[String, HashMap[String, String]]
     private var decoder: Recoder = null
@@ -125,7 +125,7 @@
     }
 
     private def read_symbols(path: String) = {
-      val file = new File(IsabelleSystem.platform_path(path))
+      val file = new File(isabelle_system.platform_path(path))
       if (file.canRead) {
         for (line <- Source.fromFile(file).getLines) read_line(line)
       }
diff -r c14c9a41f1ac -r d4058295affb src/Pure/Isar/isar.scala
--- a/src/Pure/Isar/isar.scala	Sat Dec 27 11:54:08 2008 +0100
+++ b/src/Pure/Isar/isar.scala	Sat Dec 27 14:57:30 2008 +0100
@@ -9,7 +9,8 @@
 import java.util.Properties
 
 
-class Isar(args: String*) extends IsabelleProcess(args: _*) {
+class Isar(isabelle_system: IsabelleSystem, args: String*) extends
+    IsabelleProcess(isabelle_system, args: _*) {
 
   /* basic editor commands */
 
diff -r c14c9a41f1ac -r d4058295affb src/Pure/Tools/isabelle_process.scala
--- a/src/Pure/Tools/isabelle_process.scala	Sat Dec 27 11:54:08 2008 +0100
+++ b/src/Pure/Tools/isabelle_process.scala	Sat Dec 27 14:57:30 2008 +0100
@@ -12,8 +12,6 @@
 import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
   InputStream, OutputStream, IOException}
 
-import isabelle.{Symbol, XML}
-
 
 object IsabelleProcess {
 
@@ -69,7 +67,7 @@
 
   class Result(val kind: Kind.Value, val props: Properties, val result: String) {
     override def toString = {
-      val res = XML.content(YXML.parse_failsafe(result)).mkString("")
+      val res = XML.content(YXML.parse_failsafe(result)).mkString
       if (props == null) kind.toString + " [[" + res + "]]"
       else kind.toString + " " + props.toString + " [[" + res + "]]"
     }
@@ -81,11 +79,16 @@
 }
 
 
-class IsabelleProcess(args: String*) {
+class IsabelleProcess(isabelle_system: IsabelleSystem, args: String*) {
 
   import IsabelleProcess._
 
 
+  /* alternative constructors */
+
+  def this(args: String*) = this(new IsabelleSystem, args: _*)
+
+
   /* process information */
 
   private var proc: Process = null
@@ -122,7 +125,7 @@
     if (pid == null) put_result(Kind.SYSTEM, null, "Cannot interrupt: unknown pid")
     else {
       try {
-        if (IsabelleSystem.exec("kill", "-INT", pid).waitFor == 0)
+        if (isabelle_system.exec("kill", "-INT", pid).waitFor == 0)
           put_result(Kind.SIGNAL, null, "INT")
         else
           put_result(Kind.SYSTEM, null, "Cannot interrupt: kill command failed")
@@ -185,7 +188,7 @@
 
   private class StdinThread(out_stream: OutputStream) extends Thread("isabelle: stdin") {
     override def run() = {
-      val writer = new BufferedWriter(new OutputStreamWriter(out_stream, IsabelleSystem.charset))
+      val writer = new BufferedWriter(new OutputStreamWriter(out_stream, isabelle_system.charset))
       var finished = false
       while (!finished) {
         try {
@@ -215,7 +218,7 @@
 
   private class StdoutThread(in_stream: InputStream) extends Thread("isabelle: stdout") {
     override def run() = {
-      val reader = new BufferedReader(new InputStreamReader(in_stream, IsabelleSystem.charset))
+      val reader = new BufferedReader(new InputStreamReader(in_stream, isabelle_system.charset))
       var result = new StringBuilder(100)
 
       var finished = false
@@ -253,7 +256,7 @@
 
   private class MessageThread(fifo: String) extends Thread("isabelle: messages") {
     override def run() = {
-      val reader = IsabelleSystem.fifo_reader(fifo)
+      val reader = isabelle_system.fifo_reader(fifo)
       var kind: Kind.Value = null
       var props: Properties = null
       var result = new StringBuilder
@@ -337,7 +340,7 @@
     /* isabelle version */
 
     {
-      val (msg, rc) = IsabelleSystem.isabelle_tool("version")
+      val (msg, rc) = isabelle_system.isabelle_tool("version")
       if (rc != 0) error("Version check failed -- bad Isabelle installation:\n" + msg)
       put_result(Kind.SYSTEM, null, msg)
     }
@@ -345,8 +348,8 @@
 
     /* message fifo */
 
-    val message_fifo = IsabelleSystem.mk_fifo()
-    def rm_fifo() = IsabelleSystem.rm_fifo(message_fifo)
+    val message_fifo = isabelle_system.mk_fifo()
+    def rm_fifo() = isabelle_system.rm_fifo(message_fifo)
 
     val message_thread = new MessageThread(message_fifo)
     message_thread.start
@@ -356,8 +359,8 @@
 
     try {
       val cmdline =
-        List(IsabelleSystem.getenv_strict("ISABELLE_PROCESS"), "-W", message_fifo) ++ args
-      proc = IsabelleSystem.exec2(cmdline: _*)
+        List(isabelle_system.getenv_strict("ISABELLE_PROCESS"), "-W", message_fifo) ++ args
+      proc = isabelle_system.exec2(cmdline: _*)
     }
     catch {
       case e: IOException =>
diff -r c14c9a41f1ac -r d4058295affb src/Pure/Tools/isabelle_system.scala
--- a/src/Pure/Tools/isabelle_system.scala	Sat Dec 27 11:54:08 2008 +0100
+++ b/src/Pure/Tools/isabelle_system.scala	Sat Dec 27 14:57:30 2008 +0100
@@ -12,7 +12,7 @@
 import scala.io.Source
 
 
-object IsabelleSystem {
+class IsabelleSystem {
 
   val charset = "UTF-8"
 
@@ -98,7 +98,7 @@
       try { exec2((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 output = Source.fromInputStream(proc.getInputStream, charset).mkString
     val rc = proc.waitFor
     (output, rc)
   }