src/Tools/Code/code_scala.ML
changeset 38779 89f654951200
parent 38778 49b885736e8f
child 38780 910cedb62327
     1.1 --- a/src/Tools/Code/code_scala.ML	Thu Aug 26 12:30:43 2010 +0200
     1.2 +++ b/src/Tools/Code/code_scala.ML	Thu Aug 26 13:50:58 2010 +0200
     1.3 @@ -293,11 +293,10 @@
     1.4  
     1.5  in
     1.6  
     1.7 -fun scala_program_of_program labelled_name module_name reserved raw_module_alias program =
     1.8 +fun scala_program_of_program labelled_name reserved module_alias program =
     1.9    let
    1.10  
    1.11      (* building module name hierarchy *)
    1.12 -    val module_alias = if is_some module_name then K module_name else raw_module_alias;
    1.13      fun alias_fragments name = case module_alias name
    1.14       of SOME name' => Long_Name.explode name'
    1.15        | NONE => map (fn name => fst (yield_singleton Name.variants name reserved))
    1.16 @@ -403,20 +402,15 @@
    1.17  
    1.18    in (deresolve, sca_program) end;
    1.19  
    1.20 -fun serialize_scala raw_module_name labelled_name
    1.21 -    raw_reserved includes raw_module_alias
    1.22 +fun serialize_scala labelled_name raw_reserved includes module_alias
    1.23      _ syntax_tyco syntax_const (code_of_pretty, code_writeln)
    1.24 -    program stmt_names destination =
    1.25 +    program (stmt_names, presentation_stmt_names) destination =
    1.26    let
    1.27  
    1.28 -    (* generic nonsense *)
    1.29 -    val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
    1.30 -    val module_name = if null presentation_stmt_names then raw_module_name else SOME "Code";
    1.31 -
    1.32      (* preprocess program *)
    1.33      val reserved = fold (insert (op =) o fst) includes raw_reserved;
    1.34      val (deresolve, sca_program) = scala_program_of_program labelled_name
    1.35 -      module_name (Name.make_context reserved) raw_module_alias program;
    1.36 +      (Name.make_context reserved) module_alias program;
    1.37  
    1.38      (* print statements *)
    1.39      fun lookup_constr tyco constr = case Graph.get_node program tyco
    1.40 @@ -498,9 +492,9 @@
    1.41  
    1.42  (** Isar setup **)
    1.43  
    1.44 -fun isar_serializer module_name =
    1.45 +fun isar_serializer _ =
    1.46    Code_Target.parse_args (Scan.succeed ())
    1.47 -  #> (fn () => serialize_scala module_name);
    1.48 +  #> (fn () => serialize_scala);
    1.49  
    1.50  val setup =
    1.51    Code_Target.add_target