--- a/lib/scripts/isabelle-platform Thu May 20 19:55:42 2010 +0200
+++ b/lib/scripts/isabelle-platform Thu May 20 23:22:37 2010 +0200
@@ -1,3 +1,4 @@
+# -*- shell-script -*- :mode=shellscript:
#
# determine general hardware and operating system type for Isabelle
#
--- a/src/Pure/System/isabelle_system.scala Thu May 20 19:55:42 2010 +0200
+++ b/src/Pure/System/isabelle_system.scala Thu May 20 23:22:37 2010 +0200
@@ -18,10 +18,20 @@
import scala.collection.mutable
-class Isabelle_System extends Standard_System
+class Isabelle_System(this_isabelle_home: String) extends Standard_System
{
+ def this() = this(null)
+
+
/** Isabelle environment **/
+ /*
+ isabelle_home precedence:
+ (1) this_isabelle_home as explicit argument
+ (2) ISABELLE_HOME process environment variable (e.g. inherited from running isabelle tool)
+ (3) isabelle.home system property (e.g. via JVM application boot process)
+ */
+
private val environment: Map[String, String] =
{
import scala.collection.JavaConversions._
@@ -30,13 +40,15 @@
("THIS_JAVA" -> this_java())
val isabelle_home =
- env0.get("ISABELLE_HOME") match {
- case None | Some("") =>
- val path = java.lang.System.getProperty("isabelle.home")
- if (path == null || path == "") error("Unknown Isabelle home directory")
- else path
- case Some(path) => path
- }
+ if (this_isabelle_home != null) this_isabelle_home
+ else
+ env0.get("ISABELLE_HOME") match {
+ case None | Some("") =>
+ val path = java.lang.System.getProperty("isabelle.home")
+ if (path == null || path == "") error("Unknown Isabelle home directory")
+ else path
+ case Some(path) => path
+ }
Standard_System.with_tmp_file("settings") { dump =>
val shell_prefix =
--- a/src/Pure/library.scala Thu May 20 19:55:42 2010 +0200
+++ b/src/Pure/library.scala Thu May 20 23:22:37 2010 +0200
@@ -11,6 +11,10 @@
import javax.swing.JOptionPane
+import scala.swing.ComboBox
+import scala.swing.event.SelectionChanged
+
+
object Library
{
/* separate */
@@ -88,6 +92,31 @@
def error_dialog = simple_dialog(JOptionPane.ERROR_MESSAGE, "Error") _
+ /* zoom box */
+
+ def zoom_box(apply_factor: Int => Unit) =
+ new ComboBox(
+ List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%")) {
+ val Factor = "([0-9]+)%?"r
+ def reset(): Int = { selection.index = 3; 100 }
+
+ reactions += {
+ case SelectionChanged(_) =>
+ val factor =
+ selection.item match {
+ case Factor(s) =>
+ val i = Integer.parseInt(s)
+ if (10 <= i && i <= 1000) i else reset()
+ case _ => reset()
+ }
+ apply_factor(factor)
+ }
+ reset()
+ listenTo(selection)
+ makeEditable()
+ }
+
+
/* timing */
def timeit[A](message: String)(e: => A) =
--- a/src/Tools/jEdit/src/jedit/html_panel.scala Thu May 20 19:55:42 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/html_panel.scala Thu May 20 23:22:37 2010 +0200
@@ -79,10 +79,9 @@
private val builder = new DocumentBuilderImpl(ucontext, rcontext)
- /* physical document */
+ /* document template with style sheets */
- private def template(font_size: Int): String =
- {
+ private val template_head =
"""<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
@@ -91,22 +90,30 @@
<style media="all" type="text/css">
""" +
system.try_read("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
- system.try_read("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
- "body { font-family: " + system.font_family + "; font-size: " + raw_px(font_size) + "px }" +
+ system.try_read("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n"
+
+ private val template_tail =
"""
</style>
</head>
<body/>
</html>
"""
- }
+
+ private def template(font_size: Int): String =
+ template_head +
+ "body { font-family: " + system.font_family + "; font-size: " + raw_px(font_size) + "px }" +
+ template_tail
+
+
+ /* physical document */
private class Doc
{
- var current_font_size: Int = 0
- var current_font_metrics: FontMetrics = null
- var current_body: List[XML.Tree] = Nil
- var current_DOM: org.w3c.dom.Document = null
+ private var current_font_size: Int = 0
+ private var current_font_metrics: FontMetrics = null
+ private var current_body: List[XML.Tree] = Nil
+ private var current_DOM: org.w3c.dom.Document = null
def resize(font_size: Int)
{
@@ -119,10 +126,12 @@
current_DOM =
builder.parse(
new InputSourceImpl(new StringReader(template(font_size)), "http://localhost"))
- render(current_body)
+ refresh()
}
}
+ def refresh() { render(current_body) }
+
def render(body: List[XML.Tree])
{
current_body = body
@@ -134,9 +143,11 @@
.map(t => XML.elem(HTML.PRE, HTML.spans(t))))
val node = XML.document_node(current_DOM, XML.elem(HTML.BODY, html_body))
- current_DOM.removeChild(current_DOM.getLastChild())
- current_DOM.appendChild(node)
- Swing_Thread.now { setDocument(current_DOM, rcontext) }
+ Swing_Thread.now {
+ current_DOM.removeChild(current_DOM.getLastChild())
+ current_DOM.appendChild(node)
+ setDocument(current_DOM, rcontext)
+ }
}
resize(initial_font_size)
@@ -147,12 +158,14 @@
private case class Resize(font_size: Int)
private case class Render(body: List[XML.Tree])
+ private case object Refresh
private val main_actor = actor {
var doc = new Doc
loop {
react {
case Resize(font_size) => doc.resize(font_size)
+ case Refresh => doc.refresh()
case Render(body) => doc.render(body)
case bad => System.err.println("main_actor: ignoring bad message " + bad)
}
@@ -160,5 +173,6 @@
}
def resize(font_size: Int) { main_actor ! Resize(font_size) }
+ def refresh() { main_actor ! Refresh }
def render(body: List[XML.Tree]) { main_actor ! Render(body) }
}
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala Thu May 20 19:55:42 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Thu May 20 23:22:37 2010 +0200
@@ -11,11 +11,12 @@
import scala.actors.Actor._
-import scala.swing.{FlowPanel, Button, ToggleButton}
+import scala.swing.{FlowPanel, Button, CheckBox}
import scala.swing.event.ButtonClicked
import javax.swing.JPanel
import java.awt.{BorderLayout, Dimension}
+import java.awt.event.{ComponentEvent, ComponentAdapter}
import org.gjt.sp.jedit.View
import org.gjt.sp.jedit.gui.DockableWindowManager
@@ -30,7 +31,7 @@
val controls = new FlowPanel(FlowPanel.Alignment.Right)()
add(controls.peer, BorderLayout.NORTH)
- val html_panel = new HTML_Panel(Isabelle.system, Isabelle.font_size(), null)
+ val html_panel = new HTML_Panel(Isabelle.system, scala.math.round(Isabelle.font_size()), null)
add(html_panel, BorderLayout.CENTER)
@@ -54,11 +55,20 @@
}
}
+ private var zoom_factor = 100
+
+ private def handle_resize() =
+ Swing_Thread.now {
+ html_panel.resize(scala.math.round(Isabelle.font_size() * zoom_factor / 100))
+ }
+
+ private val zoom = Library.zoom_box(factor => { zoom_factor = factor; handle_resize() })
+
private val update = new Button("Update") {
reactions += { case ButtonClicked(_) => handle_update() }
}
- val follow = new ToggleButton("Follow")
+ private val follow = new CheckBox("Follow")
follow.selected = true
@@ -67,8 +77,7 @@
private val output_actor = actor {
loop {
react {
- case Session.Global_Settings => html_panel.resize(Isabelle.font_size())
-
+ case Session.Global_Settings => handle_resize()
case Render(body) => html_panel.render(body)
case cmd: Command =>
@@ -99,8 +108,16 @@
}
+ /* resize */
+
+ addComponentListener(new ComponentAdapter {
+ val delay = Swing_Thread.delay_last(500) { html_panel.refresh() }
+ override def componentResized(e: ComponentEvent) { delay() }
+ })
+
+
/* init controls */
- controls.contents ++= List(update, follow)
+ controls.contents ++= List(zoom, update, follow)
handle_update()
}
--- a/src/Tools/jEdit/src/jedit/plugin.scala Thu May 20 19:55:42 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala Thu May 20 23:22:37 2010 +0200
@@ -70,8 +70,9 @@
jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
}
- def font_size(): Int =
- (jEdit.getIntegerProperty("view.fontsize", 16) * Int_Property("relative-font-size", 100)) / 100
+ def font_size(): Float =
+ (jEdit.getIntegerProperty("view.fontsize", 16) *
+ Int_Property("relative-font-size", 100)).toFloat / 100
/* settings */