1.1 --- a/lib/scripts/isabelle-platform Thu May 20 19:55:42 2010 +0200
1.2 +++ b/lib/scripts/isabelle-platform Thu May 20 23:22:37 2010 +0200
1.3 @@ -1,3 +1,4 @@
1.4 +# -*- shell-script -*- :mode=shellscript:
1.5 #
1.6 # determine general hardware and operating system type for Isabelle
1.7 #
2.1 --- a/src/Pure/System/isabelle_system.scala Thu May 20 19:55:42 2010 +0200
2.2 +++ b/src/Pure/System/isabelle_system.scala Thu May 20 23:22:37 2010 +0200
2.3 @@ -18,10 +18,20 @@
2.4 import scala.collection.mutable
2.5
2.6
2.7 -class Isabelle_System extends Standard_System
2.8 +class Isabelle_System(this_isabelle_home: String) extends Standard_System
2.9 {
2.10 + def this() = this(null)
2.11 +
2.12 +
2.13 /** Isabelle environment **/
2.14
2.15 + /*
2.16 + isabelle_home precedence:
2.17 + (1) this_isabelle_home as explicit argument
2.18 + (2) ISABELLE_HOME process environment variable (e.g. inherited from running isabelle tool)
2.19 + (3) isabelle.home system property (e.g. via JVM application boot process)
2.20 + */
2.21 +
2.22 private val environment: Map[String, String] =
2.23 {
2.24 import scala.collection.JavaConversions._
2.25 @@ -30,13 +40,15 @@
2.26 ("THIS_JAVA" -> this_java())
2.27
2.28 val isabelle_home =
2.29 - env0.get("ISABELLE_HOME") match {
2.30 - case None | Some("") =>
2.31 - val path = java.lang.System.getProperty("isabelle.home")
2.32 - if (path == null || path == "") error("Unknown Isabelle home directory")
2.33 - else path
2.34 - case Some(path) => path
2.35 - }
2.36 + if (this_isabelle_home != null) this_isabelle_home
2.37 + else
2.38 + env0.get("ISABELLE_HOME") match {
2.39 + case None | Some("") =>
2.40 + val path = java.lang.System.getProperty("isabelle.home")
2.41 + if (path == null || path == "") error("Unknown Isabelle home directory")
2.42 + else path
2.43 + case Some(path) => path
2.44 + }
2.45
2.46 Standard_System.with_tmp_file("settings") { dump =>
2.47 val shell_prefix =
3.1 --- a/src/Pure/library.scala Thu May 20 19:55:42 2010 +0200
3.2 +++ b/src/Pure/library.scala Thu May 20 23:22:37 2010 +0200
3.3 @@ -11,6 +11,10 @@
3.4 import javax.swing.JOptionPane
3.5
3.6
3.7 +import scala.swing.ComboBox
3.8 +import scala.swing.event.SelectionChanged
3.9 +
3.10 +
3.11 object Library
3.12 {
3.13 /* separate */
3.14 @@ -88,6 +92,31 @@
3.15 def error_dialog = simple_dialog(JOptionPane.ERROR_MESSAGE, "Error") _
3.16
3.17
3.18 + /* zoom box */
3.19 +
3.20 + def zoom_box(apply_factor: Int => Unit) =
3.21 + new ComboBox(
3.22 + List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%")) {
3.23 + val Factor = "([0-9]+)%?"r
3.24 + def reset(): Int = { selection.index = 3; 100 }
3.25 +
3.26 + reactions += {
3.27 + case SelectionChanged(_) =>
3.28 + val factor =
3.29 + selection.item match {
3.30 + case Factor(s) =>
3.31 + val i = Integer.parseInt(s)
3.32 + if (10 <= i && i <= 1000) i else reset()
3.33 + case _ => reset()
3.34 + }
3.35 + apply_factor(factor)
3.36 + }
3.37 + reset()
3.38 + listenTo(selection)
3.39 + makeEditable()
3.40 + }
3.41 +
3.42 +
3.43 /* timing */
3.44
3.45 def timeit[A](message: String)(e: => A) =
4.1 --- a/src/Tools/jEdit/src/jedit/html_panel.scala Thu May 20 19:55:42 2010 +0200
4.2 +++ b/src/Tools/jEdit/src/jedit/html_panel.scala Thu May 20 23:22:37 2010 +0200
4.3 @@ -79,10 +79,9 @@
4.4 private val builder = new DocumentBuilderImpl(ucontext, rcontext)
4.5
4.6
4.7 - /* physical document */
4.8 + /* document template with style sheets */
4.9
4.10 - private def template(font_size: Int): String =
4.11 - {
4.12 + private val template_head =
4.13 """<?xml version="1.0" encoding="utf-8"?>
4.14 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
4.15 "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
4.16 @@ -91,22 +90,30 @@
4.17 <style media="all" type="text/css">
4.18 """ +
4.19 system.try_read("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
4.20 - system.try_read("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
4.21 - "body { font-family: " + system.font_family + "; font-size: " + raw_px(font_size) + "px }" +
4.22 + system.try_read("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n"
4.23 +
4.24 + private val template_tail =
4.25 """
4.26 </style>
4.27 </head>
4.28 <body/>
4.29 </html>
4.30 """
4.31 - }
4.32 +
4.33 + private def template(font_size: Int): String =
4.34 + template_head +
4.35 + "body { font-family: " + system.font_family + "; font-size: " + raw_px(font_size) + "px }" +
4.36 + template_tail
4.37 +
4.38 +
4.39 + /* physical document */
4.40
4.41 private class Doc
4.42 {
4.43 - var current_font_size: Int = 0
4.44 - var current_font_metrics: FontMetrics = null
4.45 - var current_body: List[XML.Tree] = Nil
4.46 - var current_DOM: org.w3c.dom.Document = null
4.47 + private var current_font_size: Int = 0
4.48 + private var current_font_metrics: FontMetrics = null
4.49 + private var current_body: List[XML.Tree] = Nil
4.50 + private var current_DOM: org.w3c.dom.Document = null
4.51
4.52 def resize(font_size: Int)
4.53 {
4.54 @@ -119,10 +126,12 @@
4.55 current_DOM =
4.56 builder.parse(
4.57 new InputSourceImpl(new StringReader(template(font_size)), "http://localhost"))
4.58 - render(current_body)
4.59 + refresh()
4.60 }
4.61 }
4.62
4.63 + def refresh() { render(current_body) }
4.64 +
4.65 def render(body: List[XML.Tree])
4.66 {
4.67 current_body = body
4.68 @@ -134,9 +143,11 @@
4.69 .map(t => XML.elem(HTML.PRE, HTML.spans(t))))
4.70
4.71 val node = XML.document_node(current_DOM, XML.elem(HTML.BODY, html_body))
4.72 - current_DOM.removeChild(current_DOM.getLastChild())
4.73 - current_DOM.appendChild(node)
4.74 - Swing_Thread.now { setDocument(current_DOM, rcontext) }
4.75 + Swing_Thread.now {
4.76 + current_DOM.removeChild(current_DOM.getLastChild())
4.77 + current_DOM.appendChild(node)
4.78 + setDocument(current_DOM, rcontext)
4.79 + }
4.80 }
4.81
4.82 resize(initial_font_size)
4.83 @@ -147,12 +158,14 @@
4.84
4.85 private case class Resize(font_size: Int)
4.86 private case class Render(body: List[XML.Tree])
4.87 + private case object Refresh
4.88
4.89 private val main_actor = actor {
4.90 var doc = new Doc
4.91 loop {
4.92 react {
4.93 case Resize(font_size) => doc.resize(font_size)
4.94 + case Refresh => doc.refresh()
4.95 case Render(body) => doc.render(body)
4.96 case bad => System.err.println("main_actor: ignoring bad message " + bad)
4.97 }
4.98 @@ -160,5 +173,6 @@
4.99 }
4.100
4.101 def resize(font_size: Int) { main_actor ! Resize(font_size) }
4.102 + def refresh() { main_actor ! Refresh }
4.103 def render(body: List[XML.Tree]) { main_actor ! Render(body) }
4.104 }
5.1 --- a/src/Tools/jEdit/src/jedit/output_dockable.scala Thu May 20 19:55:42 2010 +0200
5.2 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Thu May 20 23:22:37 2010 +0200
5.3 @@ -11,11 +11,12 @@
5.4
5.5 import scala.actors.Actor._
5.6
5.7 -import scala.swing.{FlowPanel, Button, ToggleButton}
5.8 +import scala.swing.{FlowPanel, Button, CheckBox}
5.9 import scala.swing.event.ButtonClicked
5.10
5.11 import javax.swing.JPanel
5.12 import java.awt.{BorderLayout, Dimension}
5.13 +import java.awt.event.{ComponentEvent, ComponentAdapter}
5.14
5.15 import org.gjt.sp.jedit.View
5.16 import org.gjt.sp.jedit.gui.DockableWindowManager
5.17 @@ -30,7 +31,7 @@
5.18 val controls = new FlowPanel(FlowPanel.Alignment.Right)()
5.19 add(controls.peer, BorderLayout.NORTH)
5.20
5.21 - val html_panel = new HTML_Panel(Isabelle.system, Isabelle.font_size(), null)
5.22 + val html_panel = new HTML_Panel(Isabelle.system, scala.math.round(Isabelle.font_size()), null)
5.23 add(html_panel, BorderLayout.CENTER)
5.24
5.25
5.26 @@ -54,11 +55,20 @@
5.27 }
5.28 }
5.29
5.30 + private var zoom_factor = 100
5.31 +
5.32 + private def handle_resize() =
5.33 + Swing_Thread.now {
5.34 + html_panel.resize(scala.math.round(Isabelle.font_size() * zoom_factor / 100))
5.35 + }
5.36 +
5.37 + private val zoom = Library.zoom_box(factor => { zoom_factor = factor; handle_resize() })
5.38 +
5.39 private val update = new Button("Update") {
5.40 reactions += { case ButtonClicked(_) => handle_update() }
5.41 }
5.42
5.43 - val follow = new ToggleButton("Follow")
5.44 + private val follow = new CheckBox("Follow")
5.45 follow.selected = true
5.46
5.47
5.48 @@ -67,8 +77,7 @@
5.49 private val output_actor = actor {
5.50 loop {
5.51 react {
5.52 - case Session.Global_Settings => html_panel.resize(Isabelle.font_size())
5.53 -
5.54 + case Session.Global_Settings => handle_resize()
5.55 case Render(body) => html_panel.render(body)
5.56
5.57 case cmd: Command =>
5.58 @@ -99,8 +108,16 @@
5.59 }
5.60
5.61
5.62 + /* resize */
5.63 +
5.64 + addComponentListener(new ComponentAdapter {
5.65 + val delay = Swing_Thread.delay_last(500) { html_panel.refresh() }
5.66 + override def componentResized(e: ComponentEvent) { delay() }
5.67 + })
5.68 +
5.69 +
5.70 /* init controls */
5.71
5.72 - controls.contents ++= List(update, follow)
5.73 + controls.contents ++= List(zoom, update, follow)
5.74 handle_update()
5.75 }
6.1 --- a/src/Tools/jEdit/src/jedit/plugin.scala Thu May 20 19:55:42 2010 +0200
6.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala Thu May 20 23:22:37 2010 +0200
6.3 @@ -70,8 +70,9 @@
6.4 jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
6.5 }
6.6
6.7 - def font_size(): Int =
6.8 - (jEdit.getIntegerProperty("view.fontsize", 16) * Int_Property("relative-font-size", 100)) / 100
6.9 + def font_size(): Float =
6.10 + (jEdit.getIntegerProperty("view.fontsize", 16) *
6.11 + Int_Property("relative-font-size", 100)).toFloat / 100
6.12
6.13
6.14 /* settings */