# HG changeset patch # User wenzelm # Date 1245929806 -7200 # Node ID b97b34e7c853711f4cca1c56918c8a21f0cb444a # Parent 477f2abf90a4940c67b704dc22ad0f2ec853fc0d# Parent 203d5e61e3bcc9cbe924eb123d325106958cb33b merged diff -r 477f2abf90a4 -r b97b34e7c853 bin/isabelle-process --- 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 diff -r 477f2abf90a4 -r b97b34e7c853 src/Pure/Isar/isar.scala --- 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 */ diff -r 477f2abf90a4 -r b97b34e7c853 src/Pure/Isar/isar_document.scala --- 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._ diff -r 477f2abf90a4 -r b97b34e7c853 src/Pure/System/isabelle_process.ML --- 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 *) diff -r 477f2abf90a4 -r b97b34e7c853 src/Pure/System/isabelle_process.scala --- 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 diff -r 477f2abf90a4 -r b97b34e7c853 src/Pure/System/isabelle_system.scala --- 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] =