如何指定標題和生成的代碼包？

我正在用Isabelle生成Scala代碼。我怎樣才能爲我的Scala文件指定一個頭文件？例如，我想有這樣的事情：如何指定標題和生成的代碼包？

// Generated code. Generated with Isabelle/HOL 
// File: blubb.thy line:1234 
// Date: Wed, 27.03.2013 
// exported code equations: bla blub blob ...

如何指定要使用的包？例如，要使用包GENERATED，該文件應以文字package GENERATED開頭。

我走到這一步，最好的辦法是code_include命令與空的第二個參數（""）。如果我選擇較長的第二參數，則理論首先發出其代碼。但我必須寫入文件的開頭。

code_include Scala "" 
{*package GENERATED 

// Code generated by Isabelle 
*}

如何邪惡是該解決方案？如果它不是那麼邪惡，我怎麼能添加諸如當前日期，當前你的文件和export_code發生的行。我還可以添加我輸出的代碼方程，但不添加它們的代碼？

來源

2013-03-27 corny

code_include是你想要的東西的正確的東西。第二個參數標識包含，並確定代碼生成器輸出的順序不同code_include s。由於您選擇了空標識符""，您的文本將始終排在第一位，但不能有多個具有相同標識符的code_include（後者覆蓋前者）。

您在{*和*}之內給code_include的文本沒有被解釋，所以您不能在那裏獲得動態部分。但是，如果使用代碼生成器的ML接口，則可以在調用export_code之前生成該字符串。這可能如下所示：

ML {* 
val scala_header = 
    let 
    val package = "package GENERATED"; 
    val date = Date.toString (Date.fromTimeLocal (Time.now())) 
    val header = package^"\n\n"^"// Generated by Isabelle on "^date^"\n" 
    in 
    Code_Target.add_include "Scala" ("", SOME (header, [])) 
    end 
*}

現在，你只需要調用scala_header前export_code：

setup {* scala_header *} 
export_code ... in Scala file ...

這給你大致正確的生成日期。詳細地說，執行setup {* scala_header *}時的時間將是export_code實際執行前一段時間（由於多線程）。即使在順序模式下，當您生成大量代碼或對代碼方程進行大量預處理時，差距可能會持續幾分鐘。

來源

2013-03-28 07:43:58

如何指定標題和生成的代碼包？

回答

相關問題