Re: [isabelle] Isabelle server: Using JSON to request that a top level command is modified



On 08/07/2019 19:05, Yakoub Nemouchi wrote:
> 
> I am trying to use Isabelle client to talk to Isabelle server. I want to
> send a JSON request to Isabelle server saying  that a given top-level
> command in my theory was edited.
> 
> What is the corresponding JSON request? I imagine, to do such a request, I
> need the Isabelle server command that somehow takes as argument the ID of
> the top-level command !
> 
> In the sequel is a successfully tested example  from
> https://sketis.net/2018/the-isabelle-server-responsive-control-of-prover-sessions

As explained in the documentation ("system" manual chapter 4), the
Isabelle server takes document content from the file-system, e.g. a
temporary directory provided by the session context. PIDE edits are
derived from that for each use_theories protocol command (section 4.4.8).

Fine-grained PIDE command IDs are not directly involved here. The server
protocol imitates old-style REPL interaction in some sense.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.