생성 된 코드의 헤더와 패키지는 어떻게 지정합니까?

이사벨로 스칼라 코드를 생성하려고합니다. 스칼라 파일의 헤더를 어떻게 지정할 수 있습니까? 예를 들어, 다음과 같이하고 싶습니다.생성 된 코드의 헤더와 패키지는 어떻게 지정합니까?

// 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 명령입니다. 더 긴 두 번째 매개 변수를 선택하면 Efficient_Nat 이론은 먼저 코드를 내 보냅니다. 하지만 필자는 파일의 시작 부분에 글을 써야합니다.

code_include Scala "" 
{*package GENERATED 

// Code generated by Isabelle 
*}

이 솔루션은 얼마나 나쁜 것입니까? 악의가 아닌 경우 현재 날짜, 현재 파일 및 export_code이 발생한 행을 어떻게 추가 할 수 있습니까? 또한 내가 수출 한 코드 방정식을 추가 할 수 있습니까?

출처

2013-03-27 corny

code_include은 당신이 원하는 것입니다. 두 번째 매개 변수는 includes를 식별하고 코드 생성기가 서로 다르게 출력하는 순서를 결정합니다. code_include. 빈 식별자 ""을 선택했기 때문에 텍스트가 항상 먼저 나옵니다. 그러나 동일한 식별자를 가진 code_include을 여러 개 가질 수는 없습니다 (후자는 이전 코드를 덮어 씁니다).

code_include{* 및 *}에 입력하는 텍스트는 해석되지 않으므로 동적 부품을 사용할 수 없습니다. 그러나 코드 생성기의 ML 인터페이스를 사용하는 경우 export_code을 호출하기 직전에 문자열을 생성 할 수 있습니다.

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

이 당신에게 대략 정확한 생성 날짜를 제공합니다 : 이제

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_headerexport_code 전에 호출해야, 다음과 같이이 보일 수 있습니다. 구체적으로 말하자면, setup {* scala_header *}이 실행될 때가 될 것입니다.이 실제로 실행되기 전에 (멀티 스레딩으로 인해) 시간이 걸릴 수 있습니다. 순차적 인 모드에서도 많은 양의 코드를 생성하거나 코드 방정식의 많은 사전 처리를 할 때 갭이 수 분이 될 수 있습니다.

출처

2013-03-28 07:43:58

생성 된 코드의 헤더와 패키지는 어떻게 지정합니까?

답변

관련 문제