--- a/lib/scripts/getsettings Tue Jun 09 11:12:08 2009 -0700
+++ b/lib/scripts/getsettings Tue Jun 09 20:41:25 2009 +0200
@@ -51,10 +51,8 @@
if [ "$OSTYPE" = cygwin ]; then
CLASSPATH="$(cygpath -u -p "$CLASSPATH")"
function jvmpath() { cygpath -w -p "$@"; }
- ISABELLE_ROOT_JVM="$(jvmpath /)"
else
function jvmpath() { echo "$@"; }
- ISABELLE_ROOT_JVM=/
fi
HOME_JVM="$HOME"
--- a/src/Pure/General/symbol.scala Tue Jun 09 11:12:08 2009 -0700
+++ b/src/Pure/General/symbol.scala Tue Jun 09 20:41:25 2009 +0200
@@ -6,37 +6,47 @@
package isabelle
-import java.util.regex.Pattern
-import java.io.File
import scala.io.Source
-import scala.collection.jcl.HashMap
+import scala.collection.jcl
+import scala.util.matching.Regex
-object Symbol {
+object Symbol
+{
/** Symbol regexps **/
- private def compile(s: String) =
- Pattern.compile(s, Pattern.COMMENTS | Pattern.DOTALL)
+ private val plain = new Regex("""(?xs)
+ [^\\ \ud800-\udfff] | [\ud800-\udbff][\udc00-\udfff] """)
- private val plain_pattern = compile(""" [^\\ \ud800-\udfff] | [\ud800-\udbff][\udc00-\udfff] """)
-
- private val symbol_pattern = compile(""" \\ \\? < (?:
+ private val symbol = new Regex("""(?xs)
+ \\ \\? < (?:
\^? [A-Za-z][A-Za-z0-9_']* |
\^raw: [\x20-\x7e\u0100-\uffff && [^.>]]* ) >""")
- private val bad_symbol_pattern = compile("(?!" + symbol_pattern + ")" +
+ private val bad_symbol = new Regex("(?xs) (?!" + symbol + ")" +
""" \\ \\? < (?: (?! \s | [\"`\\] | \(\* | \*\) | \{\* | \*\} ) . )*""")
// total pattern
- val pattern = compile(plain_pattern + "|" + symbol_pattern + "|" + bad_symbol_pattern + "| .")
+ val regex = new Regex(plain + "|" + symbol + "|" + bad_symbol + "| .")
+ // prefix of another symbol
+ def is_open(s: String): Boolean =
+ {
+ val len = s.length
+ len == 1 && Character.isHighSurrogate(s(0)) ||
+ s == "\\" ||
+ s == "\\<" ||
+ len > 2 && s(len - 1) != '>'
+ }
/** Recoding **/
- private class Recoder(list: List[(String, String)]) {
- private val (min, max) = {
+ private class Recoder(list: List[(String, String)])
+ {
+ private val (min, max) =
+ {
var min = '\uffff'
var max = '\u0000'
for ((x, _) <- list) {
@@ -46,14 +56,16 @@
}
(min, max)
}
- private val table = {
- val table = new HashMap[String, String]
+ private val table =
+ {
+ val table = new jcl.HashMap[String, String] // reasonably efficient?
for ((x, y) <- list) table + (x -> y)
table
}
- def recode(text: String) = {
+ def recode(text: String): String =
+ {
val len = text.length
- val matcher = pattern.matcher(text)
+ val matcher = regex.pattern.matcher(text)
val result = new StringBuilder(len)
var i = 0
while (i < len) {
@@ -62,10 +74,7 @@
matcher.region(i, len)
matcher.lookingAt
val x = matcher.group
- table.get(x) match {
- case Some(y) => result.append(y)
- case None => result.append(x)
- }
+ result.append(table.get(x) getOrElse x)
i = matcher.end
}
else { result.append(c); i += 1 }
@@ -80,75 +89,56 @@
class Interpretation(symbol_decls: Iterator[String])
{
- private val symbols = new HashMap[String, HashMap[String, String]]
- private var decoder: Recoder = null
- private var encoder: Recoder = null
+ /* read symbols */
+
+ private val empty = new Regex("""(?xs) ^\s* (?: \#.* )? $ """)
+ private val key = new Regex("""(?xs) (.+): """)
+
+ private def read_decl(decl: String): (String, Map[String, String]) =
+ {
+ def err() = error("Bad symbol declaration: " + decl)
+
+ def read_props(props: List[String]): Map[String, String] =
+ {
+ props match {
+ case Nil => Map()
+ case _ :: Nil => err()
+ case key(x) :: y :: rest => read_props(rest) + (x -> y)
+ case _ => err()
+ }
+ }
+ decl.split("\\s+").toList match {
+ case Nil => err()
+ case sym :: props => (sym, read_props(props))
+ }
+ }
+
+ private val symbols: List[(String, Map[String, String])] =
+ for (decl <- symbol_decls.toList if !empty.pattern.matcher(decl).matches)
+ yield read_decl(decl)
+
+
+ /* main recoder methods */
+
+ private val (decoder, encoder) =
+ {
+ val mapping =
+ for {
+ (sym, props) <- symbols
+ val code =
+ try { Integer.decode(props("code")).intValue }
+ catch {
+ case _: NoSuchElementException => error("Missing code for symbol " + sym)
+ case _: NumberFormatException => error("Bad code for symbol " + sym)
+ }
+ val ch = new String(Character.toChars(code))
+ } yield (sym, ch)
+ (new Recoder(mapping ++ (for ((x, y) <- mapping) yield ("\\" + x, y))),
+ new Recoder(for ((x, y) <- mapping) yield (y, x)))
+ }
def decode(text: String) = decoder.recode(text)
def encode(text: String) = encoder.recode(text)
-
- /* read symbols */
-
- private val empty_pattern = compile(""" ^\s* (?: \#.* )? $ """)
- private val blank_pattern = compile(""" \s+ """)
- private val key_pattern = compile(""" (.+): """)
-
- private def read_decl(decl: String) = {
- def err() = error("Bad symbol declaration: " + decl)
-
- def read_props(props: List[String], tab: HashMap[String, String])
- {
- props match {
- case Nil => ()
- case _ :: Nil => err()
- case key :: value :: rest => {
- val key_matcher = key_pattern.matcher(key)
- if (key_matcher.matches) {
- tab + (key_matcher.group(1) -> value)
- read_props(rest, tab)
- }
- else err ()
- }
- }
- }
-
- if (!empty_pattern.matcher(decl).matches) {
- blank_pattern.split(decl).toList match {
- case Nil => err()
- case symbol :: props => {
- val tab = new HashMap[String, String]
- read_props(props, tab)
- symbols + (symbol -> tab)
- }
- }
- }
- }
-
-
- /* init tables */
-
- private def get_code(entry: (String, HashMap[String, String])) = {
- val (symbol, props) = entry
- val code =
- try { Integer.decode(props("code")).intValue }
- catch {
- case _: NoSuchElementException => error("Missing code for symbol " + symbol)
- case _: NumberFormatException => error("Bad code for symbol " + symbol)
- }
- (symbol, new String(Character.toChars(code)))
- }
-
- private def init_recoders() = {
- val list = symbols.elements.toList.map(get_code)
- decoder = new Recoder(list ++ (for ((x, y) <- list) yield ("\\" + x, y)))
- encoder = new Recoder(for ((x, y) <- list) yield (y, x))
- }
-
-
- /* constructor */
-
- symbol_decls.foreach(read_decl)
- init_recoders()
}
}
--- a/src/Pure/General/yxml.scala Tue Jun 09 11:12:08 2009 -0700
+++ b/src/Pure/General/yxml.scala Tue Jun 09 20:41:25 2009 +0200
@@ -6,8 +6,6 @@
package isabelle
-import java.util.regex.Pattern
-
object YXML {
--- a/src/Pure/System/isabelle_system.scala Tue Jun 09 11:12:08 2009 -0700
+++ b/src/Pure/System/isabelle_system.scala Tue Jun 09 20:41:25 2009 +0200
@@ -6,10 +6,11 @@
package isabelle
-import java.util.regex.{Pattern, Matcher}
+import java.util.regex.Pattern
import java.io.{BufferedReader, InputStreamReader, FileInputStream, File, IOException}
import scala.io.Source
+import scala.util.matching.Regex
object IsabelleSystem
@@ -58,16 +59,15 @@
/* Isabelle settings environment */
- private val (cygdrive_pattern, cygwin_root, shell_prefix) =
+ private val (platform_root, drive_prefix, shell_prefix) =
{
if (IsabelleSystem.is_cygwin) {
- val cygdrive = Cygwin.cygdrive getOrElse "/cygdrive"
- val pattern = Pattern.compile(cygdrive + "/([a-zA-Z])($|/.*)")
- val root = Cygwin.root getOrElse "C:\\cygwin"
- val bash = List(root + "\\bin\\bash", "-l")
- (Some(pattern), Some(root), bash)
+ val root = Cygwin.root() getOrElse "C:\\cygwin"
+ val drive = Cygwin.cygdrive() getOrElse "/cygdrive"
+ val shell = List(root + "\\bin\\bash", "-l")
+ (root, drive, shell)
}
- else (None, None, Nil)
+ else ("/", "", Nil)
}
private val environment: Map[String, String] =
@@ -117,39 +117,33 @@
/* file path specifications */
+ private val Cygdrive = new Regex(
+ if (drive_prefix == "") "\0"
+ else Pattern.quote(drive_prefix) + "/([a-zA-Z])($|/.*)")
+
def platform_path(source_path: String): String =
{
val result_path = new StringBuilder
- def init_plain(path: String): String =
- {
- if (path.startsWith("/")) {
- result_path.length = 0
- result_path.append(getenv_strict("ISABELLE_ROOT_JVM"))
- path.substring(1)
- }
- else path
- }
def init(path: String): String =
{
- cygdrive_pattern match {
- case Some(pattern) =>
- val 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 init_plain(path)
- case None => init_plain(path)
+ path match {
+ case Cygdrive(drive, rest) =>
+ result_path.length = 0
+ result_path.append(drive)
+ result_path.append(":")
+ result_path.append(File.separator)
+ rest
+ case _ if (path.startsWith("/")) =>
+ result_path.length = 0
+ result_path.append(platform_root)
+ path.substring(1)
+ case _ => path
}
}
-
def append(path: String)
{
- for (p <- init(path).split("/")) {
+ for (p <- init(path) split "/") {
if (p != "") {
val len = result_path.length
if (len > 0 && result_path(len - 1) != File.separatorChar)
@@ -158,7 +152,7 @@
}
}
}
- for (p <- init(source_path).split("/")) {
+ 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"))