<div dir="ltr">On Fri, Sep 5, 2008 at 11:20 PM, Matthew Fluet <span dir="ltr">&lt;<a href="mailto:fluet@tti-c.org">fluet@tti-c.org</a>&gt;</span> wrote:<br><div class="gmail_quote"><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
I do think the &#39;private/public/external&#39; seem a little nicer.</blockquote><div><br>Committed.<br>&nbsp;<br></div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<div class="Ih2E3d"><br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
Regarding the MLLIB_{PRIVATE/PUBLIC/whatever} macros, somehow what I&#39;d<br>
really like to do is define them based on if the header is used by C-code<br>
within the library or C-code outside the library, eg:<br>
<br>
#ifdef PART_OF_LIBRARY_&lt;NAME-OF-LIBRARY&gt;<br>
#define MLLIB_PRIVATE(x) PRIVATE x<br>
#define MLLIB_PUBLIC(x) PUBLIC x<br>
#else<br>
#define MLLIB_PRIVATE(x)<br>
#define MLLIB_PUBLIC(x) EXTERNAL x<br>
#endif<br>
<br>
MLLIB_PRIVATE(int foo();)<br>
MLLIB_PUBLIC(int bar();)<br>
<br>
#undef MLLIB_PRIVATE<br>
#undef MLLIB_PUBLIC<br>
<br>
This would then need inclusion (or inline-copy) of exports.h.<br>
<br>
A user using FFI as pary of his library would then do this:<br>
#define PART_OF_LIBRARY_FOO<br>
#include &quot;foo.h&quot;<br>
<br>
Meanwhile, anyone using libfoo would just do:<br>
#include &quot;foo.h&quot;<br>
<br>
Thoughts?<br>
</blockquote>
<br></div>
Seems reasonable. &nbsp;The &#39;#define PART_OF_LIBRARY_FOO&#39; idiom would only be needed if the library required a C proxy that itself required access to the _export-ed functions of the SML library --- &nbsp;a sufficiently complex and rare situtation that the extra syntax seems fine.<br>

</blockquote></div><br>Hmm that reasoning suggests to make the #ifdef PART_OF_LIBRARY_XXX into #if 1 when Control.Format = Executable. Done.<br><br></div>