tuned;
authorwenzelm
Sun Mar 13 13:57:20 2011 +0100 (2011-03-13)
changeset 41939eb9fb5a4d27f
parent 41938 645cca858c69
child 41940 a3b68a7a0e15
tuned;
src/Tools/Code/code_scala.ML
src/Tools/Code/code_target.ML
     1.1 --- a/src/Tools/Code/code_scala.ML	Sun Mar 13 13:53:54 2011 +0100
     1.2 +++ b/src/Tools/Code/code_scala.ML	Sun Mar 13 13:57:20 2011 +0100
     1.3 @@ -64,7 +64,7 @@
     1.4                str "=>",
     1.5                print_term tyvars false some_thm vars' NOBR t
     1.6              ]
     1.7 -          end 
     1.8 +          end
     1.9        | print_term tyvars is_pat some_thm vars fxy (ICase (cases as (_, t0))) =
    1.10            (case Code_Thingol.unfold_const_app t0
    1.11             of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
    1.12 @@ -133,7 +133,7 @@
    1.13            in brackify_block fxy
    1.14              (concat [print_term tyvars false some_thm vars NOBR t, str "match", str "{"])
    1.15              (map print_select clauses)
    1.16 -            (str "}") 
    1.17 +            (str "}")
    1.18            end
    1.19        | print_case tyvars some_thm vars fxy ((_, []), _) =
    1.20            (brackify fxy o Pretty.breaks o map str) ["error(\"empty case\")"];
    1.21 @@ -273,7 +273,7 @@
    1.22                  val aux_abstr = if null auxs then [] else [enum "," "(" ")"
    1.23                    (map (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
    1.24                    (print_typ tyvars NOBR ty)) aux_tys), str "=>"];
    1.25 -              in 
    1.26 +              in
    1.27                  concat ([str "val", print_method classparam, str "="]
    1.28                    @ aux_abstr @| print_app tyvars false (SOME thm) vars NOBR
    1.29                      (const, map (IVar o SOME) auxs))
    1.30 @@ -329,9 +329,11 @@
    1.31        | modify_stmt (_, Code_Thingol.Classparam _) = NONE
    1.32        | modify_stmt (_, stmt) = SOME stmt;
    1.33    in
    1.34 -    Code_Namespace.hierarchical_program labelled_name { module_alias = module_alias, reserved = reserved,
    1.35 -      empty_nsp = ((reserved, reserved), reserved), namify_module = namify_module, namify_stmt = namify_stmt,
    1.36 -      cyclic_modules = true, empty_data = [], memorize_data = memorize_implicits, modify_stmts = map modify_stmt } program
    1.37 +    Code_Namespace.hierarchical_program labelled_name
    1.38 +      { module_alias = module_alias, reserved = reserved,
    1.39 +        empty_nsp = ((reserved, reserved), reserved), namify_module = namify_module,
    1.40 +        namify_stmt = namify_stmt, cyclic_modules = true, empty_data = [],
    1.41 +        memorize_data = memorize_implicits, modify_stmts = map modify_stmt } program
    1.42    end;
    1.43  
    1.44  fun serialize_scala { labelled_name, reserved_syms, includes,
    1.45 @@ -417,10 +419,12 @@
    1.46  val setup =
    1.47    Code_Target.add_target
    1.48      (target, { serializer = serializer, literals = literals,
    1.49 -      check = { env_var = "SCALA_HOME", make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
    1.50 +      check = { env_var = "SCALA_HOME",
    1.51 +        make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
    1.52          make_command = fn scala_home => fn _ =>
    1.53            "export JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' && "
    1.54 -            ^ Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " ROOT.scala" } })
    1.55 +            ^ Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac"))
    1.56 +            ^ " ROOT.scala" } })
    1.57    #> Code_Target.add_tyco_syntax target "fun"
    1.58       (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
    1.59          brackify_infix (1, R) fxy (
     2.1 --- a/src/Tools/Code/code_target.ML	Sun Mar 13 13:53:54 2011 +0100
     2.2 +++ b/src/Tools/Code/code_target.ML	Sun Mar 13 13:57:20 2011 +0100
     2.3 @@ -393,7 +393,7 @@
     2.4      val { env_var, make_destination, make_command } =
     2.5        (#check o the_fundamental thy) target;
     2.6      val env_param = getenv env_var;
     2.7 -    fun ext_check env_param p =
     2.8 +    fun ext_check p =
     2.9        let 
    2.10          val destination = make_destination p;
    2.11          val _ = export (SOME destination) (invoke_serializer thy target (SOME 80)
    2.12 @@ -407,7 +407,7 @@
    2.13      then if strict
    2.14        then error (env_var ^ " not set; cannot check code for " ^ target)
    2.15        else warning (env_var ^ " not set; skipped checking code for " ^ target)
    2.16 -    else Isabelle_System.with_tmp_dir "Code_Test" (ext_check env_param)
    2.17 +    else Isabelle_System.with_tmp_dir "Code_Test" ext_check
    2.18    end;
    2.19  
    2.20  fun evaluation mounted_serializer prepared_program consts ((vs, ty), t) =