--- a/Admin/isatest/isatest-makedist Sat Apr 14 19:29:31 2012 +0200
+++ b/Admin/isatest/isatest-makedist Sat Apr 14 20:44:53 2012 +0200
@@ -59,7 +59,7 @@
echo "### building distribution" >> $DISTLOG 2>&1
mkdir -p $DISTPREFIX
-$MAKEDIST -j "/home/isabelle/contrib_devel/jedit_build-20120327" >> $DISTLOG 2>&1
+$MAKEDIST -j "/home/isabelle/contrib_devel/jedit_build-20120414" >> $DISTLOG 2>&1
if [ $? -ne 0 ]
then
--- a/Admin/isatest/settings/mac-poly-M4 Sat Apr 14 19:29:31 2012 +0200
+++ b/Admin/isatest/settings/mac-poly-M4 Sat Apr 14 20:44:53 2012 +0200
@@ -1,10 +1,10 @@
# -*- shell-script -*- :mode=shellscript:
- POLYML_HOME="/home/polyml/polyml-5.4.1"
- ML_SYSTEM="polyml-5.4.1"
+ POLYML_HOME="/home/polyml/polyml-svn"
+ ML_SYSTEM="polyml-5.4.2"
ML_PLATFORM="x86-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
- ML_OPTIONS="-H 1000"
+ ML_OPTIONS="-H 500 --gcthreads 4 --gcshare 0"
ISABELLE_HOME_USER=~/isabelle-mac-poly-M4
--- a/Admin/isatest/settings/mac-poly-M8 Sat Apr 14 19:29:31 2012 +0200
+++ b/Admin/isatest/settings/mac-poly-M8 Sat Apr 14 20:44:53 2012 +0200
@@ -1,10 +1,10 @@
# -*- shell-script -*- :mode=shellscript:
- POLYML_HOME="/home/polyml/polyml-5.4.1"
- ML_SYSTEM="polyml-5.4.1"
+ POLYML_HOME="/home/polyml/polyml-svn"
+ ML_SYSTEM="polyml-5.4.2"
ML_PLATFORM="x86-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
- ML_OPTIONS="-H 1000"
+ ML_OPTIONS="-H 500 --gcthreads 8 --gcshare 0"
ISABELLE_HOME_USER=~/isabelle-mac-poly-M8
--- a/Admin/isatest/settings/mac-poly64-M4 Sat Apr 14 19:29:31 2012 +0200
+++ b/Admin/isatest/settings/mac-poly64-M4 Sat Apr 14 20:44:53 2012 +0200
@@ -1,10 +1,10 @@
# -*- shell-script -*- :mode=shellscript:
- POLYML_HOME="/home/polyml/polyml-5.4.1"
- ML_SYSTEM="polyml-5.4.1"
+ POLYML_HOME="/home/polyml/polyml-svn"
+ ML_SYSTEM="polyml-5.4.2"
ML_PLATFORM="x86_64-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
- ML_OPTIONS="-H 2000 --gcthreads 4"
+ ML_OPTIONS="-H 1000 --gcthreads 4 --gcshare 0"
ISABELLE_HOME_USER=~/isabelle-mac-poly64-M4
--- a/Admin/isatest/settings/mac-poly64-M8 Sat Apr 14 19:29:31 2012 +0200
+++ b/Admin/isatest/settings/mac-poly64-M8 Sat Apr 14 20:44:53 2012 +0200
@@ -1,10 +1,10 @@
# -*- shell-script -*- :mode=shellscript:
- POLYML_HOME="/home/polyml/polyml-5.4.1"
- ML_SYSTEM="polyml-5.4.1"
+ POLYML_HOME="/home/polyml/polyml-svn"
+ ML_SYSTEM="polyml-5.4.2"
ML_PLATFORM="x86_64-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
- ML_OPTIONS="-H 2000 --gcthreads 8"
+ ML_OPTIONS="-H 1000 --gcthreads 8 --gcshare 0"
ISABELLE_HOME_USER=~/isabelle-mac-poly64-M8
--- a/src/Pure/Isar/outer_syntax.scala Sat Apr 14 19:29:31 2012 +0200
+++ b/src/Pure/Isar/outer_syntax.scala Sat Apr 14 20:44:53 2012 +0200
@@ -41,7 +41,7 @@
}
final class Outer_Syntax private(
- keywords: Map[String, String] = Map((";" -> Keyword.DIAG)),
+ keywords: Map[String, String] = Map.empty,
lexicon: Scan.Lexicon = Scan.Lexicon.empty,
val completion: Completion = Completion.empty)
{
--- a/src/Pure/System/gui_setup.scala Sat Apr 14 19:29:31 2012 +0200
+++ b/src/Pure/System/gui_setup.scala Sat Apr 14 20:44:53 2012 +0200
@@ -51,6 +51,9 @@
val platform64 = Isabelle_System.getenv("ISABELLE_PLATFORM64")
if (platform64 != "") text.append("Isabelle platform (64 bit): " + platform64 + "\n")
text.append("Isabelle home: " + Isabelle_System.getenv("ISABELLE_HOME") + "\n")
+ val isabelle_home_windows = Isabelle_System.getenv("ISABELLE_HOME_WINDOWS")
+ if (isabelle_home_windows != "")
+ text.append("Isabelle home (Windows): " + isabelle_home_windows + "\n")
text.append("Isabelle jdk home: " + Isabelle_System.getenv("ISABELLE_JDK_HOME") + "\n")
}
catch { case ERROR(msg) => text.append(msg + "\n") }
--- a/src/Pure/simplifier.ML Sat Apr 14 19:29:31 2012 +0200
+++ b/src/Pure/simplifier.ML Sat Apr 14 20:44:53 2012 +0200
@@ -240,7 +240,7 @@
fun simp_loop_tac i =
Raw_Simplifier.generic_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN
(solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i));
- in simp_loop_tac end;
+ in SELECT_GOAL (simp_loop_tac 1) end;
local
--- a/src/Tools/jEdit/README_BUILD Sat Apr 14 19:29:31 2012 +0200
+++ b/src/Tools/jEdit/README_BUILD Sat Apr 14 20:44:53 2012 +0200
@@ -12,13 +12,13 @@
(experimental support for Scala 2.10.x milestones)
* Auxiliary jedit_build component
- http://www4.in.tum.de/~wenzelm/test/jedit_build-20120327.tar.gz
+ http://www4.in.tum.de/~wenzelm/test/jedit_build-20120414.tar.gz
Important settings within Isabelle environment
==============================================
-* init_component ".../jedit_build-20120327"
+* init_component ".../jedit_build-20120414"
* ISABELLE_JDK_HOME
* SCALA_HOME
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/jedit-4.5.1/caret Sat Apr 14 20:44:53 2012 +0200
@@ -0,0 +1,12 @@
+diff -ru 4.5.1/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 4.5.1/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
+--- 4.5.1/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2012-03-25 18:51:47.000000000 +0200
++++ 4.5.1/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java 2012-04-14 18:37:11.000000000 +0200
+@@ -4907,7 +4907,7 @@
+ /**
+ * Returns true if the caret is visible, false otherwise.
+ */
+- final boolean isCaretVisible()
++ public final boolean isCaretVisible()
+ {
+ return blink && hasFocus();
+ } //}}}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/jedit-4.5.1/memory Sat Apr 14 20:44:53 2012 +0200
@@ -0,0 +1,12 @@
+diff -ru 4.5.1/jEdit/org/gjt/sp/jedit/gui/statusbar/MemoryStatusWidgetFactory.java 4.5.1/jEdit-patched/org/gjt/sp/jedit/gui/statusbar/MemoryStatusWidgetFactory.java
+--- 4.5.1/jEdit/org/gjt/sp/jedit/gui/statusbar/MemoryStatusWidgetFactory.java 2012-03-25 18:51:51.000000000 +0200
++++ 4.5.1/jEdit-patched/org/gjt/sp/jedit/gui/statusbar/MemoryStatusWidgetFactory.java 2012-04-14 17:47:32.000000000 +0200
+@@ -222,7 +222,7 @@
+ } //}}}
+
+ //{{{ Private members
+- private static final String memoryTestStr = "999/999Mb";
++ private static final String memoryTestStr = "9999/9999Mb";
+
+ private final LineMetrics lm;
+ private final Color progressForeground;
--- a/src/Tools/jEdit/src/text_area_painter.scala Sat Apr 14 19:29:31 2012 +0200
+++ b/src/Tools/jEdit/src/text_area_painter.scala Sat Apr 14 20:44:53 2012 +0200
@@ -220,7 +220,7 @@
else chunk_font.getStringBounds(s, font_context).getWidth.toFloat
val caret_range =
- if (text_area.hasFocus) doc_view.caret_range()
+ if (text_area.isCaretVisible) doc_view.caret_range()
else Text.Range(-1)
val markup =
@@ -373,7 +373,7 @@
screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
{
robust_snapshot { _ =>
- if (text_area.hasFocus) {
+ if (text_area.isCaretVisible) {
val caret = text_area.getCaretPosition
if (start <= caret && caret == end - 1) {
val painter = text_area.getPainter