# HG changeset patch # User wenzelm # Date 1260480535 -3600 # Node ID 53a8f294d60f246aa10437841f572ebfcdc32c74 # Parent b2e6245fb3dac7621359e71a4b555241601af887# Parent 2af94d45597ff2e379b894ad9ec5ae41baf806db merged diff -r b2e6245fb3da -r 53a8f294d60f src/Pure/General/markup.scala --- 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" } diff -r b2e6245fb3da -r 53a8f294d60f src/Pure/General/xml.scala --- 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) diff -r b2e6245fb3da -r 53a8f294d60f src/Pure/System/cygwin.scala --- 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 } diff -r b2e6245fb3da -r 53a8f294d60f src/Pure/System/gui_setup.scala --- 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 diff -r b2e6245fb3da -r 53a8f294d60f src/Pure/System/isabelle_system.scala --- 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") + } } } diff -r b2e6245fb3da -r 53a8f294d60f src/Pure/Thy/html.scala --- 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