# HG changeset patch
# User wenzelm
# Date 1334429093 -7200
# Node ID 80ddf2016b6c82268dd27dd1318e8925d7e82ce8
# Parent  214bfaae738d68685ed949ba220befe42fa32a3c# Parent  ffa6e10df0911679ba7d13be3019d5fc96b98e7c
merged;

diff -r 214bfaae738d -r 80ddf2016b6c Admin/isatest/isatest-makedist
--- 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
diff -r 214bfaae738d -r 80ddf2016b6c Admin/isatest/settings/mac-poly-M4
--- 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
diff -r 214bfaae738d -r 80ddf2016b6c Admin/isatest/settings/mac-poly-M8
--- 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
diff -r 214bfaae738d -r 80ddf2016b6c Admin/isatest/settings/mac-poly64-M4
--- 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
diff -r 214bfaae738d -r 80ddf2016b6c Admin/isatest/settings/mac-poly64-M8
--- 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
diff -r 214bfaae738d -r 80ddf2016b6c src/Pure/Isar/outer_syntax.scala
--- 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)
 {
diff -r 214bfaae738d -r 80ddf2016b6c src/Pure/System/gui_setup.scala
--- 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") }
diff -r 214bfaae738d -r 80ddf2016b6c src/Pure/simplifier.ML
--- 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
 
diff -r 214bfaae738d -r 80ddf2016b6c src/Tools/jEdit/README_BUILD
--- 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
 
diff -r 214bfaae738d -r 80ddf2016b6c src/Tools/jEdit/patches/jedit-4.5.1/caret
--- /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();
+ 	} //}}}
diff -r 214bfaae738d -r 80ddf2016b6c src/Tools/jEdit/patches/jedit-4.5.1/memory
--- /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;
diff -r 214bfaae738d -r 80ddf2016b6c src/Tools/jEdit/src/text_area_painter.scala
--- 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