--- a/src/Pure/General/markup.scala Thu Dec 10 18:10:59 2009 +0100
+++ b/src/Pure/General/markup.scala Thu Dec 10 22:28:55 2009 +0100
@@ -185,6 +185,6 @@
/* content */
val ROOT = "root"
- val RAW = "raw"
val BAD = "bad"
+ val DATA = "data"
}
--- a/src/Pure/General/xml.scala Thu Dec 10 18:10:59 2009 +0100
+++ b/src/Pure/General/xml.scala Thu Dec 10 22:28:55 2009 +0100
@@ -16,7 +16,7 @@
type Attributes = List[(String, String)]
- abstract class Tree {
+ sealed abstract class Tree {
override def toString = {
val s = new StringBuilder
append_tree(this, s)
@@ -94,15 +94,26 @@
/* document object model (W3C DOM) */
+ def get_data(node: Node): Option[XML.Tree] =
+ node.getUserData(Markup.DATA) match {
+ case tree: XML.Tree => Some(tree)
+ case _ => None
+ }
+
def document_node(doc: Document, tree: Tree): Node =
{
def DOM(tr: Tree): Node = tr match {
- case Elem(name, atts, ts) => {
+ case Elem(Markup.DATA, Nil, List(data, t)) =>
+ val node = DOM(t)
+ node.setUserData(Markup.DATA, data, null)
+ node
+ case Elem(name, atts, ts) =>
+ if (name == Markup.DATA)
+ error("Malformed data element: " + tr.toString)
val node = doc.createElement(name)
for ((name, value) <- atts) node.setAttribute(name, value)
for (t <- ts) node.appendChild(DOM(t))
node
- }
case Text(txt) => doc.createTextNode(txt)
}
DOM(tree)
--- a/src/Pure/System/cygwin.scala Thu Dec 10 18:10:59 2009 +0100
+++ b/src/Pure/System/cygwin.scala Thu Dec 10 22:28:55 2009 +0100
@@ -76,36 +76,23 @@
/* Cygwin installation */
- // old-style mount points (Cygwin 1.5)
- private val CYGWIN_MOUNTS = "Software\\Cygnus Solutions\\Cygwin\\mounts v2"
-
- // new-style setup (Cygwin 1.7)
private val CYGWIN_SETUP1 = "Software\\Cygwin\\setup"
private val CYGWIN_SETUP2 = "Software\\Wow6432Node\\Cygwin\\setup"
- def config(): (String, String) =
+ def check_root(): String =
{
- val cygwin_root = java.lang.System.getenv("CYGWIN_ROOT")
-
- (if (cygwin_root != null && cygwin_root != "") Some(cygwin_root) else None) orElse
- query_registry(CYGWIN_SETUP1, "rootdir") orElse
- query_registry(CYGWIN_SETUP2, "rootdir") match
- {
- case Some(root) => (root, "/cygdrive")
- case None =>
- val root =
- query_registry(CYGWIN_MOUNTS + "\\/", "native") getOrElse "C:\\cygwin"
- val cygdrive =
- query_registry(CYGWIN_MOUNTS, "cygdrive prefix") getOrElse "cygdrive"
- (root, cygdrive)
- }
+ val root_env = java.lang.System.getenv("CYGWIN_ROOT")
+ val root =
+ if (root_env != null && root_env != "") root_env
+ else
+ query_registry(CYGWIN_SETUP1, "rootdir") orElse
+ query_registry(CYGWIN_SETUP2, "rootdir") getOrElse
+ error("Failed to determine Cygwin installation -- version 1.7 required")
+ val ok =
+ new File(root + "\\bin\\bash.exe").isFile &&
+ new File(root + "\\bin\\env.exe").isFile
+ if (!ok) error("Bad Cygwin installation: " + root)
+ root
}
-
-
- /* basic sanity check */
-
- def check(root: String): Boolean =
- new File(root + "\\bin\\bash.exe").isFile &&
- new File(root + "\\bin\\env.exe").isFile
}
--- a/src/Pure/System/gui_setup.scala Thu Dec 10 18:10:59 2009 +0100
+++ b/src/Pure/System/gui_setup.scala Thu Dec 10 22:28:55 2009 +0100
@@ -51,7 +51,7 @@
text.append("Alternative platform: " + name2 + "\n")
}
if (Platform.is_windows) {
- text.append("Cygwin root: " + Cygwin.config()._1 + "\n")
+ text.append("Cygwin root: " + Cygwin.check_root() + "\n")
}
try {
val isabelle_system = new Isabelle_System
--- a/src/Pure/System/isabelle_system.scala Thu Dec 10 18:10:59 2009 +0100
+++ b/src/Pure/System/isabelle_system.scala Thu Dec 10 22:28:55 2009 +0100
@@ -62,8 +62,8 @@
private val (platform_root, drive_prefix, shell_prefix) =
{
if (Platform.is_windows) {
- val (root, drive) = Cygwin.config()
- if (!Cygwin.check(root)) error("Bad Cygwin installation: " + root)
+ val root = Cygwin.check_root()
+ val drive = "/cygdrive"
val shell = List(root + "\\bin\\bash", "-l")
(root, drive, shell)
}
@@ -338,14 +338,20 @@
val font_family = "IsabelleText"
+ private def check_font(): Boolean =
+ new Font(font_family, Font.PLAIN, 1).getFamily == font_family
+
private def create_font(name: String) =
Font.createFont(Font.TRUETYPE_FONT, platform_file(name))
- def register_fonts() {
- val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
- val ok1 = ge.registerFont(create_font("~~/lib/fonts/IsabelleText.ttf"))
- val ok2 = ge.registerFont(create_font("~~/lib/fonts/IsabelleTextBold.ttf"))
- if (!(ok1 && ok2) && !ge.getAvailableFontFamilyNames.contains(font_family))
- error("Font family " + font_family + " unavailable")
+ def install_fonts()
+ {
+ if (!check_font()) {
+ val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
+ ge.registerFont(create_font("$ISABELLE_HOME/lib/fonts/IsabelleText.ttf"))
+ ge.registerFont(create_font("$ISABELLE_HOME/lib/fonts/IsabelleTextBold.ttf"))
+ if (!check_font())
+ error("Failed to install IsabelleText fonts")
+ }
}
}
--- a/src/Pure/Thy/html.scala Thu Dec 10 18:10:59 2009 +0100
+++ b/src/Pure/Thy/html.scala Thu Dec 10 22:28:55 2009 +0100
@@ -34,7 +34,8 @@
def spans(tree: XML.Tree): List[XML.Tree] =
tree match {
- case XML.Elem(name, _, ts) => List(span(name, ts.flatMap(spans)))
+ case XML.Elem(name, _, ts) =>
+ List(XML.elem(Markup.DATA, List(tree, span(name, ts.flatMap(spans)))))
case XML.Text(txt) =>
val ts = new ListBuffer[XML.Tree]
val t = new StringBuilder