--- a/NEWS Fri Oct 30 20:01:05 2015 +0100
+++ b/NEWS Sat Oct 31 16:24:46 2015 +0100
@@ -66,6 +66,10 @@
uniformly, and allow the dummy file argument ":" to open an empty buffer
instead.
+* The default look-and-feel for Linux is the traditional "Metal", which
+works better with GUI scaling for very high-resolution displays (e.g.
+4K). Moreover, it is generally more robust than "Nimbus".
+
*** Document preparation ***
--- a/src/Doc/JEdit/JEdit.thy Fri Oct 30 20:01:05 2015 +0100
+++ b/src/Doc/JEdit/JEdit.thy Sat Oct 31 16:24:46 2015 +0100
@@ -283,7 +283,7 @@
Isabelle/jEdit enables platform-specific look-and-feel by default as
follows.
- \<^descr>[Linux:] The platform-independent \<^emph>\<open>Nimbus\<close> is used by
+ \<^descr>[Linux:] The platform-independent \<^emph>\<open>Metal\<close> is used by
default.
\<^emph>\<open>GTK+\<close> also works under the side-condition that the overall GTK theme
@@ -310,7 +310,7 @@
Users may experiment with different look-and-feels, but need to keep
in mind that this extra variance of GUI functionality is unlikely to
work in arbitrary combinations. The platform-independent
- \<^emph>\<open>Nimbus\<close> and \<^emph>\<open>Metal\<close> should always work. The historic
+ \<^emph>\<open>Metal\<close> and \<^emph>\<open>Nimbus\<close> should always work. The historic
\<^emph>\<open>CDE/Motif\<close> should be ignored.
After changing the look-and-feel in \<^emph>\<open>Global Options~/
@@ -353,7 +353,7 @@
\<^item> \<^emph>\<open>Global Options / Appearance / Button, menu and label font\<close> as
well as \<^emph>\<open>List and text field font\<close>: this specifies the primary and
- secondary font for the old \<^emph>\<open>Metal\<close> look-and-feel
+ secondary font for the traditional \<^emph>\<open>Metal\<close> look-and-feel
(\secref{sec:look-and-feel}), which happens to scale better than newer ones
like \<^emph>\<open>Nimbus\<close>.
--- a/src/Pure/GUI/gui.scala Fri Oct 30 20:01:05 2015 +0100
+++ b/src/Pure/GUI/gui.scala Sat Oct 31 16:24:46 2015 +0100
@@ -34,8 +34,7 @@
if (Platform.is_windows || Platform.is_macos)
UIManager.getSystemLookAndFeelClassName()
else
- find_laf("Nimbus") getOrElse
- UIManager.getCrossPlatformLookAndFeelClassName()
+ UIManager.getCrossPlatformLookAndFeelClassName()
}
def init_laf(): Unit = UIManager.setLookAndFeel(get_laf())
--- a/src/Pure/General/time.scala Fri Oct 30 20:01:05 2015 +0100
+++ b/src/Pure/General/time.scala Sat Oct 31 16:24:46 2015 +0100
@@ -15,8 +15,10 @@
{
def seconds(s: Double): Time = new Time((s * 1000.0).round)
def ms(m: Long): Time = new Time(m)
+ def now(): Time = ms(System.currentTimeMillis())
+
val zero: Time = ms(0)
- def now(): Time = ms(System.currentTimeMillis())
+ val start: Time = now()
def print_seconds(s: Double): String =
String.format(Locale.ROOT, "%.3f", s.asInstanceOf[AnyRef])
--- a/src/Pure/Isar/attrib.ML Fri Oct 30 20:01:05 2015 +0100
+++ b/src/Pure/Isar/attrib.ML Sat Oct 31 16:24:46 2015 +0100
@@ -510,7 +510,7 @@
(* theory setup *)
val _ = Theory.setup
- (register_config quick_and_dirty_raw #>
+ (register_config Goal.quick_and_dirty_raw #>
register_config Ast.trace_raw #>
register_config Ast.stats_raw #>
register_config Printer.show_brackets_raw #>
--- a/src/Pure/goal.ML Fri Oct 30 20:01:05 2015 +0100
+++ b/src/Pure/goal.ML Sat Oct 31 16:24:46 2015 +0100
@@ -6,6 +6,7 @@
signature BASIC_GOAL =
sig
+ val quick_and_dirty: bool Config.T
val parallel_proofs: int Unsynchronized.ref
val SELECT_GOAL: tactic -> int -> tactic
val PREFER_GOAL: tactic -> int -> tactic
@@ -38,6 +39,7 @@
({prems: thm list, context: Proof.context} -> tactic) -> thm
val prove_global: theory -> string list -> term list -> term ->
({prems: thm list, context: Proof.context} -> tactic) -> thm
+ val quick_and_dirty_raw: Config.raw
val prove_sorry: Proof.context -> string list -> term list -> term ->
({prems: thm list, context: Proof.context} -> tactic) -> thm
val prove_sorry_global: theory -> string list -> term list -> term ->
@@ -250,6 +252,12 @@
fun prove_global thy xs asms prop tac =
Drule.export_without_context (prove (Proof_Context.init_global thy) xs asms prop tac);
+
+(* skip proofs *)
+
+val quick_and_dirty_raw = Config.declare_option ("quick_and_dirty", @{here});
+val quick_and_dirty = Config.bool quick_and_dirty_raw;
+
fun prove_sorry ctxt xs asms prop tac =
if Config.get ctxt quick_and_dirty then
prove ctxt xs asms prop (fn _ => ALLGOALS (Skip_Proof.cheat_tac ctxt))
--- a/src/Pure/skip_proof.ML Fri Oct 30 20:01:05 2015 +0100
+++ b/src/Pure/skip_proof.ML Sat Oct 31 16:24:46 2015 +0100
@@ -4,9 +4,6 @@
Skip proof via oracle invocation.
*)
-val quick_and_dirty_raw = Config.declare_option ("quick_and_dirty", @{here});
-val quick_and_dirty = Config.bool quick_and_dirty_raw;
-
signature SKIP_PROOF =
sig
val report: Proof.context -> unit
--- a/src/Tools/jEdit/src/jEdit.props Fri Oct 30 20:01:05 2015 +0100
+++ b/src/Tools/jEdit/src/jEdit.props Sat Oct 31 16:24:46 2015 +0100
@@ -1,5 +1,4 @@
#jEdit properties
-action-bar.shortcut=C+ENTER
buffer.deepIndent=false
buffer.encoding=UTF-8-Isabelle
buffer.indentSize=2
@@ -241,7 +240,7 @@
line-end.shortcut=END
line-home.shortcut=HOME
logo.icon.medium=32x32/apps/isabelle.gif
-lookAndFeel=javax.swing.plaf.nimbus.NimbusLookAndFeel
+lookAndFeel=javax.swing.plaf.metal.MetalLookAndFeel
match-bracket.shortcut2=C+9
navigator.showOnToolbar=true
next-bracket.shortcut2=C+e C+9