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



I thought that Isabelle server is the future for developing Isabelle apps
in a very clean way.
But, if it does not support all the features of PIDE protocol, it does not
make sens to me to use it now!
Maybe it is too early to start using it.
Any further development in the future for Isabelle server or it is meant
for something else?

I have one more question, will the usage of the non fine grained command
"use_theories" affect the the performance of the application?
How scalable it is with regard the fine grained PIDE commands?
The amazing feature of Isabelle is its parallel infrastructure and fine
grained PIDE protocol commands allows to take full advantage of that.
What is the best way to use "use_theories"  to take advantage of the
parallel infrastructure of Isabelle?

It is very important to me to have some numbers on "use_theories", and know
its limitations, in order I take the right decision to develop my next
application.

Best wishes,

Yakoub.

On Mon, Jul 15, 2019 at 10:37 AM Makarius <makarius at sketis.net> wrote:

> 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.