# HG changeset patch
# User wenzelm
# Date 1273593319 -7200
# Node ID fc672bf92fc2d7d2161caf04aacd3da8c208a77c
# Parent 75d837441aa6c23964cfbcbf662690218b64d876# Parent dc85664dbf6d0b74a2398b7890e8dfae453b3720
merged
diff -r 75d837441aa6 -r fc672bf92fc2 src/HOL/Mirabelle/Tools/mirabelle.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML Tue May 11 08:52:22 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Tue May 11 17:55:19 2010 +0200
@@ -92,7 +92,7 @@
fun log thy s =
let fun append_to n = if n = "" then K () else File.append (Path.explode n)
- in append_to (Config.get_thy thy logfile) (s ^ "\n") end
+ in append_to (Config.get_global thy logfile) (s ^ "\n") end
(* FIXME: with multithreading and parallel proofs enabled, we might need to
encapsulate this inside a critical section *)
@@ -108,7 +108,7 @@
| in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r))
fun only_within_range thy pos f x =
- let val l = Config.get_thy thy start_line and r = Config.get_thy thy end_line
+ let val l = Config.get_global thy start_line and r = Config.get_global thy end_line
in if in_range l r (Position.line_of pos) then f x else () end
in
@@ -118,7 +118,7 @@
val thy = Proof.theory_of pre
val pos = Toplevel.pos_of tr
val name = Toplevel.name_of tr
- val st = (pre, post, Time.fromSeconds (Config.get_thy thy timeout))
+ val st = (pre, post, Time.fromSeconds (Config.get_global thy timeout))
val str0 = string_of_int o the_default 0
val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos)
diff -r 75d837441aa6 -r fc672bf92fc2 src/Provers/blast.ML
--- a/src/Provers/blast.ML Tue May 11 08:52:22 2010 +0100
+++ b/src/Provers/blast.ML Tue May 11 17:55:19 2010 +0200
@@ -1278,7 +1278,7 @@
val (depth_limit, setup_depth_limit) = Attrib.config_int_global "blast_depth_limit" (K 20);
fun blast_tac cs i st =
- ((DEEPEN (1, Config.get_thy (Thm.theory_of_thm st) depth_limit)
+ ((DEEPEN (1, Config.get_global (Thm.theory_of_thm st) depth_limit)
(timing_depth_tac (start_timing ()) cs) 0) i
THEN flexflex_tac) st
handle TRANS s =>
diff -r 75d837441aa6 -r fc672bf92fc2 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML Tue May 11 08:52:22 2010 +0100
+++ b/src/Pure/Isar/attrib.ML Tue May 11 17:55:19 2010 +0200
@@ -355,7 +355,7 @@
| scan_value (Config.String _) = equals |-- Args.name >> Config.String;
fun scan_config thy config =
- let val config_type = Config.get_thy thy config
+ let val config_type = Config.get_global thy config
in scan_value config_type >> (K o Thm.declaration_attribute o K o Config.put_generic config) end;
in
diff -r 75d837441aa6 -r fc672bf92fc2 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala Tue May 11 08:52:22 2010 +0100
+++ b/src/Pure/System/isabelle_system.scala Tue May 11 17:55:19 2010 +0200
@@ -318,7 +318,7 @@
val font_family = "IsabelleText"
- def get_font(bold: Boolean = false, size: Int = 1): Font =
+ def get_font(size: Int = 1, bold: Boolean = false): Font =
new Font(font_family, if (bold) Font.BOLD else Font.PLAIN, size)
def install_fonts()
@@ -330,7 +330,7 @@
else "$ISABELLE_HOME/lib/fonts/IsabelleText.ttf"
Font.createFont(Font.TRUETYPE_FONT, platform_file(name))
}
- def check_font() = get_font(false).getFamily == font_family
+ def check_font() = get_font().getFamily == font_family
if (!check_font()) {
val font = create_font(false)
diff -r 75d837441aa6 -r fc672bf92fc2 src/Pure/config.ML
--- a/src/Pure/config.ML Tue May 11 08:52:22 2010 +0100
+++ b/src/Pure/config.ML Tue May 11 17:55:19 2010 +0200
@@ -16,9 +16,9 @@
val get: Proof.context -> 'a T -> 'a
val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context
val put: 'a T -> 'a -> Proof.context -> Proof.context
- val get_thy: theory -> 'a T -> 'a
- val map_thy: 'a T -> ('a -> 'a) -> theory -> theory
- val put_thy: 'a T -> 'a -> theory -> theory
+ val get_global: theory -> 'a T -> 'a
+ val map_global: 'a T -> ('a -> 'a) -> theory -> theory
+ val put_global: 'a T -> 'a -> theory -> theory
val get_generic: Context.generic -> 'a T -> 'a
val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
@@ -83,9 +83,9 @@
fun map_ctxt config f = Context.proof_map (map_generic config f);
fun put_ctxt config value = map_ctxt config (K value);
-fun get_thy thy = get_generic (Context.Theory thy);
-fun map_thy config f = Context.theory_map (map_generic config f);
-fun put_thy config value = map_thy config (K value);
+fun get_global thy = get_generic (Context.Theory thy);
+fun map_global config f = Context.theory_map (map_generic config f);
+fun put_global config value = map_global config (K value);
(* context information *)
diff -r 75d837441aa6 -r fc672bf92fc2 src/Pure/library.scala
--- a/src/Pure/library.scala Tue May 11 08:52:22 2010 +0100
+++ b/src/Pure/library.scala Tue May 11 17:55:19 2010 +0200
@@ -76,9 +76,11 @@
private def simple_dialog(kind: Int, default_title: String)
(parent: Component, title: String, message: Any*)
{
- JOptionPane.showMessageDialog(parent,
- message.toArray.asInstanceOf[Array[AnyRef]],
- if (title == null) default_title else title, kind)
+ Swing_Thread.now {
+ JOptionPane.showMessageDialog(parent,
+ message.toArray.asInstanceOf[Array[AnyRef]],
+ if (title == null) default_title else title, kind)
+ }
}
def dialog = simple_dialog(JOptionPane.PLAIN_MESSAGE, null) _
diff -r 75d837441aa6 -r fc672bf92fc2 src/Pure/unify.ML
--- a/src/Pure/unify.ML Tue May 11 08:52:22 2010 +0100
+++ b/src/Pure/unify.ML Tue May 11 17:55:19 2010 +0200
@@ -349,7 +349,7 @@
fun matchcopy thy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs))
: (term * (Envir.env * dpair list))Seq.seq =
let
- val trace_tps = Config.get_thy thy trace_types;
+ val trace_tps = Config.get_global thy trace_types;
(*Produce copies of uarg and cons them in front of uargs*)
fun copycons uarg (uargs, (env, dpairs)) =
Seq.map(fn (uarg', ed') => (uarg'::uargs, ed'))
@@ -584,9 +584,9 @@
fun hounifiers (thy,env, tus : (term*term)list)
: (Envir.env * (term*term)list)Seq.seq =
let
- val trace_bnd = Config.get_thy thy trace_bound;
- val search_bnd = Config.get_thy thy search_bound;
- val trace_smp = Config.get_thy thy trace_simp;
+ val trace_bnd = Config.get_global thy trace_bound;
+ val search_bnd = Config.get_global thy search_bound;
+ val trace_smp = Config.get_global thy trace_simp;
fun add_unify tdepth ((env,dpairs), reseq) =
Seq.make (fn()=>
let val (env',flexflex,flexrigid) =
diff -r 75d837441aa6 -r fc672bf92fc2 src/Tools/jEdit/README_BUILD
--- a/src/Tools/jEdit/README_BUILD Tue May 11 08:52:22 2010 +0100
+++ b/src/Tools/jEdit/README_BUILD Tue May 11 17:55:19 2010 +0200
@@ -8,10 +8,10 @@
* Netbeans 6.8
http://www.netbeans.org/downloads/index.html
-* Scala for Netbeans: version 6.8v1.1
- http://sourceforge.net/project/showfiles.php?group_id=192439&package_id=256544
+* Scala for Netbeans: version 6.8v1.1.0rc2
+ http://wiki.netbeans.org/Scala
+ http://sourceforge.net/projects/erlybird/files/nb-scala/6.8v1.1.0rc2
http://blogtrader.net/dcaoyuan/category/NetBeans
- http://wiki.netbeans.org/Scala
* jEdit 4.3.1 or 4.3.2
http://www.jedit.org/
diff -r 75d837441aa6 -r fc672bf92fc2 src/Tools/jEdit/dist-template/properties/jedit.props
--- a/src/Tools/jEdit/dist-template/properties/jedit.props Tue May 11 08:52:22 2010 +0100
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props Tue May 11 17:55:19 2010 +0200
@@ -185,6 +185,7 @@
sidekick.complete-delay=300
sidekick.splitter.location=721
tip.show=false
+twoStageSave=false
view.antiAlias=standard
view.blockCaret=true
view.caretBlink=false
diff -r 75d837441aa6 -r fc672bf92fc2 src/Tools/jEdit/nbproject/build-impl.xml
--- a/src/Tools/jEdit/nbproject/build-impl.xml Tue May 11 08:52:22 2010 +0100
+++ b/src/Tools/jEdit/nbproject/build-impl.xml Tue May 11 17:55:19 2010 +0200
@@ -230,7 +230,7 @@
-
+
@@ -549,7 +549,7 @@
-->
-
+
diff -r 75d837441aa6 -r fc672bf92fc2 src/Tools/jEdit/nbproject/genfiles.properties
--- a/src/Tools/jEdit/nbproject/genfiles.properties Tue May 11 08:52:22 2010 +0100
+++ b/src/Tools/jEdit/nbproject/genfiles.properties Tue May 11 17:55:19 2010 +0200
@@ -4,5 +4,5 @@
# This file is used by a NetBeans-based IDE to track changes in generated files such as build-impl.xml.
# Do not edit this file. You may delete it but then the IDE will never regenerate such files for you.
nbproject/build-impl.xml.data.CRC32=8f41dcce
-nbproject/build-impl.xml.script.CRC32=1c29c971
-nbproject/build-impl.xml.stylesheet.CRC32=8c3c03dd@1.3.4
+nbproject/build-impl.xml.script.CRC32=e3e2a5d5
+nbproject/build-impl.xml.stylesheet.CRC32=5220179f@1.3.5
diff -r 75d837441aa6 -r fc672bf92fc2 src/Tools/jEdit/plugin/Isabelle.props
--- a/src/Tools/jEdit/plugin/Isabelle.props Tue May 11 08:52:22 2010 +0100
+++ b/src/Tools/jEdit/plugin/Isabelle.props Tue May 11 17:55:19 2010 +0200
@@ -25,8 +25,10 @@
options.isabelle.label=Isabelle
options.isabelle.code=new isabelle.jedit.Isabelle_Options();
options.isabelle.logic.title=Logic
-options.isabelle.font-size.title=Font Size
-options.isabelle.font-size=14
+options.isabelle.relative-font-size.title=Relative Font Size
+options.isabelle.relative-font-size=100
+options.isabelle.relative-margin.title=Relative Margin
+options.isabelle.relative-margin=90
options.isabelle.startup-timeout=10000
#menu actions
diff -r 75d837441aa6 -r fc672bf92fc2 src/Tools/jEdit/src/jedit/html_panel.scala
--- a/src/Tools/jEdit/src/jedit/html_panel.scala Tue May 11 08:52:22 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/html_panel.scala Tue May 11 17:55:19 2010 +0200
@@ -10,7 +10,7 @@
import isabelle._
import java.io.StringReader
-import java.awt.{BorderLayout, Dimension}
+import java.awt.{BorderLayout, Dimension, GraphicsEnvironment, Toolkit}
import java.awt.event.MouseEvent
import javax.swing.{JButton, JPanel, JScrollPane}
@@ -40,7 +40,7 @@
class HTML_Panel(
sys: Isabelle_System,
- initial_font_size: Int,
+ font_size0: Int, relative_margin0: Int,
handler: PartialFunction[HTML_Panel.Event, Unit]) extends HtmlPanel
{
// global logging
@@ -56,6 +56,15 @@
}
private def template(font_size: Int): String =
+ {
+ // re-adjustment according to org.lobobrowser.html.style.HtmlValues.getFontSize
+ val dpi =
+ if (GraphicsEnvironment.isHeadless()) 72
+ else Toolkit.getDefaultToolkit().getScreenResolution()
+
+ val size0 = font_size * dpi / 96
+ val size = if (size0 * 96 / dpi == font_size) size0 else size0 + 1
+
"""
@@ -65,13 +74,24 @@
""" +
try_file("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
try_file("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
- "body { font-family: " + sys.font_family + "; font-size: " + font_size + "px }" +
+ "body { font-family: " + sys.font_family + "; font-size: " + size + "px }" +
"""
"""
+ }
+
+
+ def panel_width(font_size: Int, relative_margin: Int): Int =
+ {
+ val font = sys.get_font(font_size)
+ Swing_Thread.now {
+ val char_width = (getFontMetrics(font).stringWidth("mix") / 3) max 1
+ ((getWidth() * relative_margin) / (100 * char_width)) max 20
+ }
+ }
/* actor with local state */
@@ -98,7 +118,7 @@
private val builder = new DocumentBuilderImpl(ucontext, rcontext)
- private case class Init(font_size: Int)
+ private case class Init(font_size: Int, relative_margin: Int)
private case class Render(body: List[XML.Tree])
private val main_actor = actor {
@@ -106,9 +126,15 @@
var doc1: org.w3c.dom.Document = null
var doc2: org.w3c.dom.Document = null
+ var current_font_size = 16
+ var current_relative_margin = 90
+
loop {
react {
- case Init(font_size) =>
+ case Init(font_size, relative_margin) =>
+ current_font_size = font_size
+ current_relative_margin = relative_margin
+
val src = template(font_size)
def parse() =
builder.parse(new InputSourceImpl(new StringReader(src), "http://localhost"))
@@ -118,7 +144,9 @@
case Render(body) =>
val doc = doc2
- val html_body = Pretty.formatted(body).map(t => XML.elem(HTML.PRE, HTML.spans(t)))
+ val html_body =
+ Pretty.formatted(body, panel_width(current_font_size, current_relative_margin))
+ .map(t => XML.elem(HTML.PRE, HTML.spans(t)))
val node = XML.document_node(doc, XML.elem(HTML.BODY, html_body))
doc.removeChild(doc.getLastChild())
doc.appendChild(node)
@@ -131,11 +159,11 @@
}
}
- main_actor ! Init(initial_font_size)
-
/* main method wrappers */
- def init(font_size: Int) { main_actor ! Init(font_size) }
+ def init(font_size: Int, relative_margin: Int) { main_actor ! Init(font_size, relative_margin) }
def render(body: List[XML.Tree]) { main_actor ! Render(body) }
+
+ init(font_size0, relative_margin0)
}
diff -r 75d837441aa6 -r fc672bf92fc2 src/Tools/jEdit/src/jedit/isabelle_options.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_options.scala Tue May 11 08:52:22 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_options.scala Tue May 11 17:55:19 2010 +0200
@@ -15,7 +15,8 @@
class Isabelle_Options extends AbstractOptionPane("isabelle")
{
private val logic_name = new JComboBox()
- private val font_size = new JSpinner()
+ private val relative_font_size = new JSpinner()
+ private val relative_margin = new JSpinner()
private class List_Item(val name: String, val descr: String) {
def this(name: String) = this(name, name)
@@ -36,18 +37,26 @@
logic_name
})
- addComponent(Isabelle.Property("font-size.title"), {
- font_size.setValue(Isabelle.Int_Property("font-size"))
- font_size
+ addComponent(Isabelle.Property("relative-font-size.title"), {
+ relative_font_size.setValue(Isabelle.Int_Property("relative-font-size"))
+ relative_font_size
+ })
+
+ addComponent(Isabelle.Property("relative-margin.title"), {
+ relative_margin.setValue(Isabelle.Int_Property("relative-margin"))
+ relative_margin
})
}
override def _save()
{
- val logic = logic_name.getSelectedItem.asInstanceOf[List_Item].name
- Isabelle.Property("logic") = logic
+ Isabelle.Property("logic") =
+ logic_name.getSelectedItem.asInstanceOf[List_Item].name
- val size = font_size.getValue().asInstanceOf[Int]
- Isabelle.Int_Property("font-size") = size
+ Isabelle.Int_Property("relative-font-size") =
+ relative_font_size.getValue().asInstanceOf[Int]
+
+ Isabelle.Int_Property("relative-margin") =
+ relative_margin.getValue().asInstanceOf[Int]
}
}
diff -r 75d837441aa6 -r fc672bf92fc2 src/Tools/jEdit/src/jedit/output_dockable.scala
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala Tue May 11 08:52:22 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Tue May 11 17:55:19 2010 +0200
@@ -24,8 +24,9 @@
if (position == DockableWindowManager.FLOATING)
setPreferredSize(new Dimension(500, 250))
- private val html_panel =
- new HTML_Panel(Isabelle.system, Isabelle.Int_Property("font-size"), null)
+ val html_panel =
+ new HTML_Panel(Isabelle.system,
+ Isabelle.font_size(), Isabelle.Int_Property("relative-margin"), null)
add(html_panel, BorderLayout.CENTER)
@@ -43,7 +44,7 @@
}
case Session.Global_Settings =>
- html_panel.init(Isabelle.Int_Property("font-size"))
+ html_panel.init(Isabelle.font_size(), Isabelle.Int_Property("relative-margin"))
case bad => System.err.println("output_actor: ignoring bad message " + bad)
}
diff -r 75d837441aa6 -r fc672bf92fc2 src/Tools/jEdit/src/jedit/plugin.scala
--- a/src/Tools/jEdit/src/jedit/plugin.scala Tue May 11 08:52:22 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/plugin.scala Tue May 11 17:55:19 2010 +0200
@@ -42,22 +42,37 @@
object Property
{
- def apply(name: String): String = jEdit.getProperty(OPTION_PREFIX + name)
- def update(name: String, value: String) = jEdit.setProperty(OPTION_PREFIX + name, value)
+ def apply(name: String): String =
+ jEdit.getProperty(OPTION_PREFIX + name)
+ def apply(name: String, default: String): String =
+ jEdit.getProperty(OPTION_PREFIX + name, default)
+ def update(name: String, value: String) =
+ jEdit.setProperty(OPTION_PREFIX + name, value)
}
object Boolean_Property
{
- def apply(name: String): Boolean = jEdit.getBooleanProperty(OPTION_PREFIX + name)
- def update(name: String, value: Boolean) = jEdit.setBooleanProperty(OPTION_PREFIX + name, value)
+ def apply(name: String): Boolean =
+ jEdit.getBooleanProperty(OPTION_PREFIX + name)
+ def apply(name: String, default: Boolean): Boolean =
+ jEdit.getBooleanProperty(OPTION_PREFIX + name, default)
+ def update(name: String, value: Boolean) =
+ jEdit.setBooleanProperty(OPTION_PREFIX + name, value)
}
object Int_Property
{
- def apply(name: String): Int = jEdit.getIntegerProperty(OPTION_PREFIX + name)
- def update(name: String, value: Int) = jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
+ def apply(name: String): Int =
+ jEdit.getIntegerProperty(OPTION_PREFIX + name)
+ def apply(name: String, default: Int): Int =
+ jEdit.getIntegerProperty(OPTION_PREFIX + name, default)
+ def update(name: String, value: Int) =
+ jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
}
+ def font_size(): Int =
+ (jEdit.getIntegerProperty("view.fontsize", 16) * Int_Property("relative-font-size", 100)) / 100
+
/* settings */