# HG changeset patch # User wenzelm # Date 1274390557 -7200 # Node ID 21010d2b41e72ca211cd3d203b4f43e17e919d97 # Parent e29a115ba58ce92b214de7f622d6fa9d73676165# Parent 8f747cee4e27f327865c7a79b61f0546c11c6c98 merged diff -r e29a115ba58c -r 21010d2b41e7 lib/scripts/isabelle-platform --- 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 # diff -r e29a115ba58c -r 21010d2b41e7 src/Pure/System/isabelle_system.scala --- 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 = diff -r e29a115ba58c -r 21010d2b41e7 src/Pure/library.scala --- 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) = diff -r e29a115ba58c -r 21010d2b41e7 src/Tools/jEdit/src/jedit/html_panel.scala --- 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 = """ @@ -91,22 +90,30 @@ """ - } + + 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) } } diff -r e29a115ba58c -r 21010d2b41e7 src/Tools/jEdit/src/jedit/output_dockable.scala --- 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() } diff -r e29a115ba58c -r 21010d2b41e7 src/Tools/jEdit/src/jedit/plugin.scala --- 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 */