more generous memory settings for scala check
authorhaftmann
Thu Jul 22 12:07:30 2010 +0200 (2010-07-22)
changeset 37932d00a3f47b607
parent 37931 7b452ff6bff0
child 37933 b8ca89c45086
child 37934 440114da2488
more generous memory settings for scala check
src/HOL/Library/State_Monad.thy
src/Tools/Code/code_scala.ML
     1.1 --- a/src/HOL/Library/State_Monad.thy	Thu Jul 22 11:29:31 2010 +0200
     1.2 +++ b/src/HOL/Library/State_Monad.thy	Thu Jul 22 12:07:30 2010 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Combinator syntax for generic, open state monads (single threaded monads) *}
     1.5  
     1.6  theory State_Monad
     1.7 -imports Monad_Syntax
     1.8 +imports Main Monad_Syntax
     1.9  begin
    1.10  
    1.11  subsection {* Motivation *}
    1.12 @@ -113,10 +113,32 @@
    1.13  
    1.14  subsection {* Do-syntax *}
    1.15  
    1.16 -setup {*
    1.17 -  Adhoc_Overloading.add_variant @{const_name bind} @{const_name scomp}
    1.18 -*}
    1.19 +nonterminals
    1.20 +  sdo_binds sdo_bind
    1.21 +
    1.22 +syntax
    1.23 +  "_sdo_block" :: "sdo_binds \<Rightarrow> 'a" ("exec {//(2  _)//}" [12] 62)
    1.24 +  "_sdo_bind" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ <-/ _)" 13)
    1.25 +  "_sdo_let" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(2let _ =/ _)" [1000, 13] 13)
    1.26 +  "_sdo_then" :: "'a \<Rightarrow> sdo_bind" ("_" [14] 13)
    1.27 +  "_sdo_final" :: "'a \<Rightarrow> sdo_binds" ("_")
    1.28 +  "_sdo_cons" :: "[sdo_bind, sdo_binds] \<Rightarrow> sdo_binds" ("_;//_" [13, 12] 12)
    1.29  
    1.30 +syntax (xsymbols)
    1.31 +  "_sdo_bind"  :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ \<leftarrow>/ _)" 13)
    1.32 +
    1.33 +translations
    1.34 +  "_sdo_block (_sdo_cons (_sdo_bind p t) (_sdo_final e))"
    1.35 +    == "CONST scomp t (\<lambda>p. e)"
    1.36 +  "_sdo_block (_sdo_cons (_sdo_then t) (_sdo_final e))"
    1.37 +    == "CONST fcomp t e"
    1.38 +  "_sdo_block (_sdo_cons (_sdo_let p t) bs)"
    1.39 +    == "let p = t in _sdo_block bs"
    1.40 +  "_sdo_block (_sdo_cons b (_sdo_cons c cs))"
    1.41 +    == "_sdo_block (_sdo_cons b (_sdo_final (_sdo_block (_sdo_cons c cs))))"
    1.42 +  "_sdo_cons (_sdo_let p t) (_sdo_final s)"
    1.43 +    == "_sdo_final (let p = t in s)"
    1.44 +  "_sdo_block (_sdo_final e)" => "e"
    1.45  
    1.46  text {*
    1.47    For an example, see HOL/Extraction/Higman.thy.
     2.1 --- a/src/Tools/Code/code_scala.ML	Thu Jul 22 11:29:31 2010 +0200
     2.2 +++ b/src/Tools/Code/code_scala.ML	Thu Jul 22 12:07:30 2010 +0200
     2.3 @@ -429,7 +429,8 @@
     2.4      (target, { serializer = isar_serializer, literals = literals,
     2.5        check = { env_var = "SCALA_HOME", make_destination = I,
     2.6          make_command = fn scala_home => fn p => fn _ =>
     2.7 -          Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " *.scala" } })
     2.8 +          "export JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' && "
     2.9 +            ^ Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " *.scala" } })
    2.10    #> Code_Target.add_syntax_tyco target "fun"
    2.11       (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
    2.12          brackify_infix (1, R) fxy (