# HG changeset patch # User wenzelm # Date 1446305086 -3600 # Node ID aa1ece0bce629deaff7f0050fd72a5f08ec98e43 # Parent 87244a9cfe40decfd701772eb0db0efd3179e968# Parent 82fc5a6231a2d9defc461976e322f4ae3e32bd70 merged diff -r 87244a9cfe40 -r aa1ece0bce62 NEWS --- 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 *** diff -r 87244a9cfe40 -r aa1ece0bce62 src/Doc/JEdit/JEdit.thy --- 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>\Nimbus\ is used by + \<^descr>[Linux:] The platform-independent \<^emph>\Metal\ is used by default. \<^emph>\GTK+\ 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>\Nimbus\ and \<^emph>\Metal\ should always work. The historic + \<^emph>\Metal\ and \<^emph>\Nimbus\ should always work. The historic \<^emph>\CDE/Motif\ should be ignored. After changing the look-and-feel in \<^emph>\Global Options~/ @@ -353,7 +353,7 @@ \<^item> \<^emph>\Global Options / Appearance / Button, menu and label font\ as well as \<^emph>\List and text field font\: this specifies the primary and - secondary font for the old \<^emph>\Metal\ look-and-feel + secondary font for the traditional \<^emph>\Metal\ look-and-feel (\secref{sec:look-and-feel}), which happens to scale better than newer ones like \<^emph>\Nimbus\. diff -r 87244a9cfe40 -r aa1ece0bce62 src/Pure/GUI/gui.scala --- 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()) diff -r 87244a9cfe40 -r aa1ece0bce62 src/Pure/General/time.scala --- 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]) diff -r 87244a9cfe40 -r aa1ece0bce62 src/Pure/Isar/attrib.ML --- 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 #> diff -r 87244a9cfe40 -r aa1ece0bce62 src/Pure/goal.ML --- 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)) diff -r 87244a9cfe40 -r aa1ece0bce62 src/Pure/skip_proof.ML --- 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 diff -r 87244a9cfe40 -r aa1ece0bce62 src/Tools/jEdit/src/jEdit.props --- 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