merged

--- a/bin/isabelle-process	Thu Jun 25 13:00:32 2009 +0200
+++ b/bin/isabelle-process	Thu Jun 25 13:36:46 2009 +0200
@@ -214,7 +214,7 @@
 NICE="nice"
 if [ -n "$WRAPPER_OUTPUT" ]; then
   [ "$WRAPPER_OUTPUT" = "-" -o -p "$WRAPPER_OUTPUT" ] || fail "Bad named pipe: $WRAPPER_OUTPUT"
-  MLTEXT="$MLTEXT; IsabelleProcess.init \"$WRAPPER_OUTPUT\";"
+  MLTEXT="$MLTEXT; Isabelle_Process.init \"$WRAPPER_OUTPUT\";"
 elif [ -n "$PGIP" ]; then
   MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;"
 elif [ -n "$PROOFGENERAL" ]; then

--- a/src/Pure/Isar/isar.scala	Thu Jun 25 13:00:32 2009 +0200
+++ b/src/Pure/Isar/isar.scala	Thu Jun 25 13:36:46 2009 +0200
@@ -7,8 +7,9 @@
 package isabelle
 
 
-class Isar(isabelle_system: IsabelleSystem, results: EventBus[IsabelleProcess.Result], args: String*)
-  extends IsabelleProcess(isabelle_system, results, args: _*)
+class Isar(isabelle_system: Isabelle_System,
+    results: EventBus[Isabelle_Process.Result], args: String*)
+  extends Isabelle_Process(isabelle_system, results, args: _*)
 {
   /* basic editor commands */
 

--- a/src/Pure/Isar/isar_document.scala	Thu Jun 25 13:00:32 2009 +0200
+++ b/src/Pure/Isar/isar_document.scala	Thu Jun 25 13:36:46 2009 +0200
@@ -14,7 +14,7 @@
   type Document_ID = String
 }
 
-trait IsarDocument extends IsabelleProcess
+trait IsarDocument extends Isabelle_Process
 {
   import IsarDocument._
 

--- a/src/Pure/System/isabelle_process.ML	Thu Jun 25 13:00:32 2009 +0200
+++ b/src/Pure/System/isabelle_process.ML	Thu Jun 25 13:36:46 2009 +0200
@@ -27,7 +27,7 @@
   val init: string -> unit
 end;
 
-structure IsabelleProcess: ISABELLE_PROCESS =
+structure Isabelle_Process: ISABELLE_PROCESS =
 struct
 
 (* print modes *)

--- a/src/Pure/System/isabelle_process.scala	Thu Jun 25 13:00:32 2009 +0200
+++ b/src/Pure/System/isabelle_process.scala	Thu Jun 25 13:36:46 2009 +0200
@@ -12,7 +12,7 @@
   InputStream, OutputStream, IOException}
 
 
-object IsabelleProcess {
+object Isabelle_Process {
 
   /* results */
 
@@ -96,7 +96,7 @@
     def is_system = Kind.is_system(kind)
   }
 
-  def parse_message(isabelle_system: IsabelleSystem, result: Result) =
+  def parse_message(isabelle_system: Isabelle_System, result: Result) =
   {
     XML.Elem(Markup.MESSAGE, (Markup.CLASS, Kind.markup(result.kind)) :: result.props,
       YXML.parse_body_failsafe(isabelle_system.symbols.decode(result.result)))
@@ -104,16 +104,16 @@
 }
 
 
-class IsabelleProcess(isabelle_system: IsabelleSystem,
-  results: EventBus[IsabelleProcess.Result], args: String*)
+class Isabelle_Process(isabelle_system: Isabelle_System,
+  results: EventBus[Isabelle_Process.Result], args: String*)
 {
-  import IsabelleProcess._
+  import Isabelle_Process._
 
 
   /* demo constructor */
 
   def this(args: String*) =
-    this(new IsabelleSystem, new EventBus[IsabelleProcess.Result] + Console.println, args: _*)
+    this(new Isabelle_System, new EventBus[Isabelle_Process.Result] + Console.println, args: _*)
 
 
   /* process information */
@@ -128,7 +128,7 @@
   /* results */
 
   def parse_message(result: Result): XML.Tree =
-    IsabelleProcess.parse_message(isabelle_system, result)
+    Isabelle_Process.parse_message(isabelle_system, result)
 
   private val result_queue = new LinkedBlockingQueue[Result]
 
@@ -230,7 +230,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 {
@@ -260,7 +260,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

--- a/src/Pure/System/isabelle_system.scala	Thu Jun 25 13:00:32 2009 +0200
+++ b/src/Pure/System/isabelle_system.scala	Thu Jun 25 13:36:46 2009 +0200
@@ -1,7 +1,7 @@
 /*  Title:      Pure/System/isabelle_system.scala
     Author:     Makarius
 
-Isabelle system support -- basic Cygwin/Posix compatibility.
+Isabelle system support, with basic Cygwin/Posix compatibility.
 */
 
 package isabelle
@@ -13,7 +13,7 @@
 import scala.util.matching.Regex
 
 
-object IsabelleSystem
+object Isabelle_System
 {
 
   val charset = "UTF-8"
@@ -48,20 +48,23 @@
 }
 
 
-class IsabelleSystem
+class Isabelle_System
 {
 
-  /* unique ids */
+  /** unique ids **/
 
   private var id_count: BigInt = 0
   def id(): String = synchronized { id_count += 1; "j" + id_count }
 
 
-  /* Isabelle settings environment */
+
+  /** Isabelle environment **/
+
+  /* platform prefixes */
 
   private val (platform_root, drive_prefix, shell_prefix) =
   {
-    if (IsabelleSystem.is_cygwin) {
+    if (Isabelle_System.is_cygwin) {
       val root = Cygwin.root() getOrElse "C:\\cygwin"
       val drive = Cygwin.cygdrive() getOrElse "/cygdrive"
       val shell = List(root + "\\bin\\bash", "-l")
@@ -70,6 +73,9 @@
     else ("/", "", Nil)
   }
 
+
+  /* bash environment */
+
   private val environment: Map[String, String] =
   {
     import scala.collection.jcl.Conversions._
@@ -88,8 +94,8 @@
     val dump = File.createTempFile("isabelle", null)
     try {
       val cmdline = shell_prefix ::: List(isabelle, "getenv", "-d", dump.toString)
-      val proc = IsabelleSystem.raw_execute(env0, true, cmdline: _*)
-      val (output, rc) = IsabelleSystem.process_output(proc)
+      val proc = Isabelle_System.raw_execute(env0, true, cmdline: _*)
+      val (output, rc) = Isabelle_System.process_output(proc)
       if (rc != 0) error(output)
 
       val entries =
@@ -105,10 +111,11 @@
     finally { dump.delete }
   }
 
+
+  /* getenv */
+
   def getenv(name: String): String =
-  {
     environment.getOrElse(if (name == "HOME") "HOME_JVM" else name, "")
-  }
 
   def getenv_strict(name: String): String =
   {
@@ -119,7 +126,43 @@
   override def toString = getenv("ISABELLE_HOME")
 
 
-  /* file path specifications */
+
+  /** file path specifications **/
+
+  /* Isabelle paths */
+
+  def expand_path(source_path: String): String =
+  {
+    val result_path = new StringBuilder
+    def init(path: String)
+    {
+      if (path.startsWith("/")) {
+        result_path.clear
+        result_path += '/'
+      }
+    }
+    def append(path: String)
+    {
+      init(path)
+      for (p <- path.split("/") if p != "") {
+        val len = result_path.length
+        if (len > 0 && result_path(len - 1) != '/')
+          result_path += '/'
+        result_path ++= p
+      }
+    }
+    init(source_path)
+    for (p <- 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
+  }
+
+
+  /* platform paths */
 
   private val Cygdrive = new Regex(
     if (drive_prefix == "") "\0"
@@ -128,39 +171,21 @@
   def platform_path(source_path: String): String =
   {
     val result_path = new StringBuilder
-
-    def init(path: String): String =
-    {
-      path match {
+    val rest =
+      expand_path(source_path) match {
         case Cygdrive(drive, rest) =>
-          result_path.length = 0
-          result_path.append(drive)
-          result_path.append(":")
-          result_path.append(File.separator)
+          result_path ++= (drive + ":" + File.separator)
           rest
-        case _ if (path.startsWith("/")) =>
-          result_path.length = 0
-          result_path.append(platform_root)
-          path.substring(1)
-        case _ => path
+        case path if path.startsWith("/") =>
+          result_path ++= platform_root
+          path
+        case path => 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)
+    for (p <- rest.split("/") if p != "") {
+      val len = result_path.length
+      if (len > 0 && result_path(len - 1) != File.separatorChar)
+        result_path += File.separatorChar
+      result_path ++= p
     }
     result_path.toString
   }
@@ -186,20 +211,22 @@
   }
 
 
+  /** system tools **/
+
   /* external processes */
 
   def execute(redirect: Boolean, args: String*): Process =
   {
     val cmdline =
-      if (IsabelleSystem.is_cygwin) List(platform_path("/bin/env")) ++ args
+      if (Isabelle_System.is_cygwin) List(platform_path("/bin/env")) ++ args
       else args
-    IsabelleSystem.raw_execute(environment, redirect, cmdline: _*)
+    Isabelle_System.raw_execute(environment, redirect, cmdline: _*)
   }
 
   def isabelle_tool(args: String*): (String, Int) =
   {
     val proc = execute(true, (List(getenv_strict("ISABELLE_TOOL")) ++ args): _*)
-    IsabelleSystem.process_output(proc)
+    Isabelle_System.process_output(proc)
   }
 
 
@@ -222,12 +249,14 @@
   {
     // blocks until writer is ready
     val stream =
-      if (IsabelleSystem.is_cygwin) execute(false, "cat", fifo).getInputStream
+      if (Isabelle_System.is_cygwin) execute(false, "cat", fifo).getInputStream
       else new FileInputStream(fifo)
-    new BufferedReader(new InputStreamReader(stream, IsabelleSystem.charset))
+    new BufferedReader(new InputStreamReader(stream, Isabelle_System.charset))
   }
 
 
+  /** Isabelle resources **/
+
   /* find logics */
 
   def find_logics(): List[String] =