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

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.


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