Re: [isabelle] 2013-1-RC1: how to put generated Scala into a package without using code_include?



Hi Cornelius,

>>> is there a way to translate the following into the new way?
>>> ML {*
>>> val scala_header =
>>>   let
>>>     val package = "package Foo";
>>>     val date = Date.toString (Date.fromTimeLocal (Time.now ()))
>>>     val export_file = Context.theory_name @{theory} ^ ".thy"
>>>     val header = package ^ "\n" ^ "// Generated by Isabelle on " ^
>>> date ^ "\n" ^ "// src: " ^ export_file ^ "\n"
>>>   in
>>>     Code_Target.add_include "Scala" ("", SOME (header, []))
>>>   end
>>> *}
>>>  setup {* scala_header *}

ML {*
fun scala_header thy =
  let
    val date = Date.toString (Date.fromTimeLocal (Time.now ()));
    val package = "package Foo";
    val export_file = Context.theory_name thy ^ ".thy";
    val header = package ^ "\n" ^ "// Generated by Isabelle (" ^
Distribution.version ^ ") on " ^ date ^ "\n" ^ "// src: " ^ export_file
^ "\n";
  in
    Code_Target.set_printings (Code_Symbol.Module ("", [("Scala", SOME
(header, []))])) thy
  end
*}
setup {* scala_header *}

export_code distinct in Scala

;-) Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.