diff --git a/src/Examples/Call.agda b/src/Examples/Call.lagda.tex
similarity index 99%
rename from src/Examples/Call.agda
rename to src/Examples/Call.lagda.tex
index 70da44b..77440aa 100644
--- a/src/Examples/Call.agda
+++ b/src/Examples/Call.lagda.tex
@@ -1,3 +1,4 @@
+\begin{code}
 module Examples.Call where
 
 open import ActorMonad public
@@ -115,3 +116,4 @@
     return-result record { msg = (Msg Z (tag ∷ n ∷ [])) } = return n
     return-result record { msg = (Msg (S x) x₁) ; msg-ok = () }
 
+\end{code}
\ No newline at end of file
diff --git a/src/Selective/Examples/Call.agda b/src/Selective/Examples/Call.lagda.tex
similarity index 95%
rename from src/Selective/Examples/Call.agda
rename to src/Selective/Examples/Call.lagda.tex
index 4db6e19..4136696 100644
--- a/src/Selective/Examples/Call.agda
+++ b/src/Selective/Examples/Call.lagda.tex
@@ -1,3 +1,4 @@
+\begin{code}
 module Selective.Examples.Call where
 
 open import Selective.ActorMonad public
@@ -52,11 +53,18 @@
        ∞ActorM i IS
          (SelectedMessage (call-select tag ISsubs whichIn))
          Γ (add-selected-references Γ)
-call {Γ} {IS = IS} var toFi tag vals sub whichIn = do
+call {Γ} {IS = IS} var toFi tag vals sub whichIn =
+\end{code}
+%<*CallComputation>
+\begin{code}
+  do
      self
      S var ![t: toFi ] ((lift tag) ∷ ([ Z ]>: sub) ∷ (translate-fields vals))
      strengthen (⊆-suc ⊆-refl)
      selective-receive (call-select tag sub whichIn)
+\end{code}
+%</CallComputation>
+\begin{code}
   where
     translate-fields : ∀ {MT} →
                        All (send-field-content Γ) MT →
@@ -104,3 +112,4 @@
     return-result record { msg = (Msg Z (tag ∷ n ∷ [])) } = return n
     return-result record { msg = (Msg (S x) x₁) ; msg-ok = () }
 
+\end{code}