Alan Schmitt wrote:
> t...@tsdye.com writes:
>> Alan Schmitt <alan.schm...@polytechnique.org> writes:
>>
>>> I tried this alternate approach, to directly generate the block:
>>>
>>> #+name: fetchcoq2
>>> #+BEGIN_SRC sh :exports none :results raw :var f="demo.v"
>>> echo "#+BEGIN_SRC coq"
>>> head $f
>>> echo
>>> echo "#+END_SRC"
>>> #+END_SRC
>>>
>>> #+call: fetchcoq2("demo.v")
>>>
>>> But then I get a result like this, with extra quoting:
>>>
>>> #+RESULTS:
>>> : #+BEGIN_SRC coq
>>> : Definition toto : forall x, exists y, x = y.
>>> :
>>> : Lemma foo: forall x, x=x.
>>> : #+END_SRC
>>>
>>> I feel like I'm missing something obvious. ":results code" is exactly
>>> what I want (put the results in a SRC block), but I don't know how to
>>> specify the headers of the generated code block.
>>
>> You need :results raw at the end of the call line.
>>
>> #+name: fetchcoq2
>> #+BEGIN_SRC sh :exports none :results raw :var f="demo.v"
>> echo "#+BEGIN_SRC coq"
>> echo $f
>> echo "#+END_SRC"
>> #+END_SRC
>>
>> #+results: fetchcoq2
>> #+BEGIN_SRC coq
>> demo.v
>> #+END_SRC
>>
>> #+call: fetchcoq2("demo.v") :results raw
>>
>> #+results:
>> #+BEGIN_SRC coq
>> demo.v
>> #+END_SRC
>
> Thanks, this is helping me much.
>
> There are still one thing that I don't understand: I cannot make this
> work when I have already evaluated the call in the buffer. More
> precisely, if I have the following:
>
> #+name: fetchcoq
> #+BEGIN_SRC sh :exports none :results raw :var f="foo.v"
> echo "#+BEGIN_SRC coq"
> head $f
> echo
> echo "#+END_SRC"
> #+END_SRC
>
> #+call: fetchcoq(f="demo.v") :results raw
>
> when I evaluate the call line, I get this (as expected):
>
> #+name: fetchcoq
> #+BEGIN_SRC sh :exports none :results raw :var f="foo.v"
> echo "#+BEGIN_SRC coq"
> head $f
> echo
> echo "#+END_SRC"
> #+END_SRC
>
> #+call: fetchcoq(f="demo.v") :results raw
>
> #+RESULTS:
> #+BEGIN_SRC coq
> Definition toto : forall x, exists y, x = y.
>
> Lemma foo: forall x, x=x.
> #+END_SRC
>
> Unfortunately, if I export this, the code is duplicated. Here is the
> generated html, for instance:
>
> ,----
> | <pre class="src src-coq"><span style="color: #FBDE2D;">Definition</span>
> | <span style="color: #ff1493;">toto</span> : <span style="color:
> | #D8FA3C;">forall</span> <span style="color: #D8FA3C;">x</span>, <span
> | style="color: #9370db;">exists</span> y, x = y.
> |
> | <span style="color: #FBDE2D;">Lemma</span> <span style="color:
> #ff1493;">foo</span>: <span style="color: #D8FA3C;">forall</span> <span
> style="color: #D8FA3C;">x</span>, x=x.
> | #+END_SRC#+BEGIN_SRC coq
> | <span style="color: #FBDE2D;">Definition</span> <span style="color:
> | #ff1493;">toto</span> : <span style="color: #D8FA3C;">forall</span> <span
> | style="color: #D8FA3C;">x</span>, <span style="color:
> #9370db;">exists</span>
> | y, x = y.
> |
> | <span style="color: #FBDE2D;">Lemma</span> <span style="color:
> #ff1493;">foo</span>: <span style="color: #D8FA3C;">forall</span> <span
> style="color: #D8FA3C;">x</span>, x=x.
> | </pre>
> `----
>
> Exporting if the result is not in the buffer is fine. I tried adding a
> ":results replace" as inner header argument to the call line and to the
> fetchcoq block, but it does not change anything.
>
> How can I tell the call line to replace the results when exporting?
The syntax of the call line is:
#+call: <NAME>[<HEADER-ARGS-FOR-BLOCK>](<ARGUMENTS>)
<HEADER-ARGS-FOR-CALL-LINE>
So, you should add your option either in [] after the name, or at the end of
the line -- I'm always hesitating about where to put the right stuff (not so
enough clear yet in my mind)...
Best regards,
Seb
--
Sebastien Vauban
