# HG changeset patch
# User haftmann
# Date 1279793250 -7200
# Node ID d00a3f47b6072e9e07a6f6da261a4c15b419e6a7
# Parent  7b452ff6bff074f5ca85f1ac217d94c7ff24215d
more generous memory settings for scala check

diff -r 7b452ff6bff0 -r d00a3f47b607 src/HOL/Library/State_Monad.thy
--- a/src/HOL/Library/State_Monad.thy	Thu Jul 22 11:29:31 2010 +0200
+++ b/src/HOL/Library/State_Monad.thy	Thu Jul 22 12:07:30 2010 +0200
@@ -5,7 +5,7 @@
 header {* Combinator syntax for generic, open state monads (single threaded monads) *}
 
 theory State_Monad
-imports Monad_Syntax
+imports Main Monad_Syntax
 begin
 
 subsection {* Motivation *}
@@ -113,10 +113,32 @@
 
 subsection {* Do-syntax *}
 
-setup {*
-  Adhoc_Overloading.add_variant @{const_name bind} @{const_name scomp}
-*}
+nonterminals
+  sdo_binds sdo_bind
+
+syntax
+  "_sdo_block" :: "sdo_binds \<Rightarrow> 'a" ("exec {//(2  _)//}" [12] 62)
+  "_sdo_bind" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ <-/ _)" 13)
+  "_sdo_let" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(2let _ =/ _)" [1000, 13] 13)
+  "_sdo_then" :: "'a \<Rightarrow> sdo_bind" ("_" [14] 13)
+  "_sdo_final" :: "'a \<Rightarrow> sdo_binds" ("_")
+  "_sdo_cons" :: "[sdo_bind, sdo_binds] \<Rightarrow> sdo_binds" ("_;//_" [13, 12] 12)
 
+syntax (xsymbols)
+  "_sdo_bind"  :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ \<leftarrow>/ _)" 13)
+
+translations
+  "_sdo_block (_sdo_cons (_sdo_bind p t) (_sdo_final e))"
+    == "CONST scomp t (\<lambda>p. e)"
+  "_sdo_block (_sdo_cons (_sdo_then t) (_sdo_final e))"
+    == "CONST fcomp t e"
+  "_sdo_block (_sdo_cons (_sdo_let p t) bs)"
+    == "let p = t in _sdo_block bs"
+  "_sdo_block (_sdo_cons b (_sdo_cons c cs))"
+    == "_sdo_block (_sdo_cons b (_sdo_final (_sdo_block (_sdo_cons c cs))))"
+  "_sdo_cons (_sdo_let p t) (_sdo_final s)"
+    == "_sdo_final (let p = t in s)"
+  "_sdo_block (_sdo_final e)" => "e"
 
 text {*
   For an example, see HOL/Extraction/Higman.thy.
diff -r 7b452ff6bff0 -r d00a3f47b607 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Thu Jul 22 11:29:31 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Thu Jul 22 12:07:30 2010 +0200
@@ -429,7 +429,8 @@
     (target, { serializer = isar_serializer, literals = literals,
       check = { env_var = "SCALA_HOME", make_destination = I,
         make_command = fn scala_home => fn p => fn _ =>
-          Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " *.scala" } })
+          "export JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' && "
+            ^ Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " *.scala" } })
   #> Code_Target.add_syntax_tyco target "fun"
      (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
         brackify_infix (1, R) fxy (