From mboxrd@z Thu Jan  1 00:00:00 1970
From: urkud@urkud.name
Subject: Re: Edit whole session with org-edit-src-edit
Date: Mon, 09 Oct 2017 07:28:33 -0400
Message-ID: <7C9EF991-3BA5-46A6-8DC7-C5048DB4FC96@urkud.name>
References: <87vajpl00m.fsf@urkud.name>
	<793E22AA-A516-4DDC-A61C-067D9B4735E3@ucsd.edu>
Mime-Version: 1.0
Content-Type: text/plain;
 charset=utf-8
Content-Transfer-Encoding: quoted-printable
Return-path: <emacs-orgmode-bounces+geo-emacs-orgmode=m.gmane.org@gnu.org>
Received: from eggs.gnu.org ([2001:4830:134:3::10]:58198)
	by lists.gnu.org with esmtp (Exim 4.71)
	(envelope-from <urkud@urkud.name>) id 1e1WFF-0000vL-Cd
	for emacs-orgmode@gnu.org; Mon, 09 Oct 2017 07:29:14 -0400
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
	(envelope-from <urkud@urkud.name>) id 1e1WFC-0001U9-74
	for emacs-orgmode@gnu.org; Mon, 09 Oct 2017 07:29:13 -0400
Received: from mail.urkud.name ([188.166.0.33]:36346)
	by eggs.gnu.org with esmtp (Exim 4.71)
	(envelope-from <urkud@urkud.name>) id 1e1WFB-0001Tn-Ty
	for emacs-orgmode@gnu.org; Mon, 09 Oct 2017 07:29:10 -0400
Received: from [192.168.10.65] (c-73-175-94-59.hsd1.pa.comcast.net
	[73.175.94.59])
	by mail.urkud.name (Postfix) with ESMTPSA id 5DB3F1F5BE
	for <emacs-orgmode@gnu.org>; Mon,  9 Oct 2017 14:28:38 +0300 (MSK)
In-Reply-To: <793E22AA-A516-4DDC-A61C-067D9B4735E3@ucsd.edu>
List-Id: "General discussions about Org-mode." <emacs-orgmode.gnu.org>
List-Unsubscribe: <https://lists.gnu.org/mailman/options/emacs-orgmode>,
	<mailto:emacs-orgmode-request@gnu.org?subject=unsubscribe>
List-Archive: <http://lists.gnu.org/archive/html/emacs-orgmode/>
List-Post: <mailto:emacs-orgmode@gnu.org>
List-Help: <mailto:emacs-orgmode-request@gnu.org?subject=help>
List-Subscribe: <https://lists.gnu.org/mailman/listinfo/emacs-orgmode>,
	<mailto:emacs-orgmode-request@gnu.org?subject=subscribe>
Errors-To: emacs-orgmode-bounces+geo-emacs-orgmode=m.gmane.org@gnu.org
Sender: "Emacs-orgmode"
	<emacs-orgmode-bounces+geo-emacs-orgmode=m.gmane.org@gnu.org>
To: emacs-orgmode@gnu.org

Hello,

On October 8, 2017 10:40:09 PM EDT, "Berry, Charles" <ccberry@ucsd=2Eedu> =
wrote:
>
>> On Oct 8, 2017, at 3:58 PM, Yury G=2E Kudryashov <urkud@urkud=2Ename>
>wrote:
>>=20
>> Hello,
>>=20
>> I want to use orgmode for literate programming with Coq=2E
>> I like the "edit in major mode" org-edit-src-edit feature, but it
>> exports only the current src block to the temprorary buffer, so it's
>> impossible to debug the file in the temporary buffer using coq-mode
>> (proofgeneral) "phrase by phrase" execution=2E
>>=20
>> I think that some other languages may have similar problems=2E Say,
>> code completion works better, if the whole file is available=2E
>
>
>I used the babel jump facility proposed here:
It doesn't help, if I want to debug a Coq proof using proofgeneral=2E I ne=
ed to feed to coqtop all the text that should go before the current "phrase=
" in a file=2E
--=20
Sent from my Android device with K-9 Mail=2E Please excuse my brevity=2E