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



Dear users(ccing other interested users),

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

Best wishes,

Yakoub

************EXAMPLE******************
isabelle client
server "isabelle" = 127.0.0.1:34329 (password
"e64b1abe-1b8a-4c61-b4c5-fbe7eb04b350")
OK {"isabelle_id":"91162dd89571","isabelle_version":"Isabelle2018: August
2018"}
session_start {"session": "HOL"}
OK {"task":"8b1d25b4-dc1e-420d-b377-72d419fdded0"}
NOTE {"kind":"writeln","message":"Starting HOL
...","task":"8b1d25b4-dc1e-420d-b377-72d419fdded0"}
177
FINISHED
{"session_id":"b11041f2-ac33-43c0-94ac-715d6f26fd41","tmp_dir":"/tmp/isabelle-yakoubn/server_session1411428207973312821","task":"8b1d25b4-dc1e-420d-b377-72d419fdded0"}
use_theories {"session_id": "b11041f2-ac33-43c0-94ac-715d6f26fd41",
"theories":["~~/src/HOL/ex/Seq"]}
OK {"task":"70b9abee-bfa2-428c-b8b2-b5b08119be0c"}
133
NOTE
{"task":"70b9abee-bfa2-428c-b8b2-b5b08119be0c","session":"","theory":"Draft.Seq","message":"theory
Draft.Seq","kind":"writeln"}
838
FINISHED
{"ok":true,"errors":[],"nodes":[{"messages":[{"kind":"writeln","message":"Found
termination order: \"(\\<lambda>p. size (fst p)) <*mlex*>
{}\"","pos":{"line":13,"offset":163,"end_offset":166,"file":"/home/yakoubn/Desktop/Work/Practice/Isabelle2018_app/Isabelle2018/src/HOL/ex/Seq.thy"}},{"kind":"writeln","message":"Found
termination order: \"size <*mlex*>
{}\"","pos":{"line":18,"offset":276,"end_offset":279,"file":"/home/yakoubn/Desktop/Work/Practice/Isabelle2018_app/Isabelle2018/src/HOL/ex/Seq.thy"}}],"theory_name":"Draft.Seq","node_name":"/home/yakoubn/Desktop/Work/Practice/Isabelle2018_app/Isabelle2018/src/HOL/ex/Seq.thy","exports":[],"status":{"unprocessed":0,"initialized":true,"running":0,"finished":29,"failed":0,"total":29,"consolidated":true,"ok":true,"warned":0}}],"task":"70b9abee-bfa2-428c-b8b2-b5b08119be0c"}
session_stop {"session_id":"70b9abee-bfa2-428c-b8b2-b5b08119be0c"}
OK {"task":"4f792742-0f98-4b94-bc63-c048bc9e3d82"}
132
FAILED {"kind":"error","message":"No session
'70b9abee-bfa2-428c-b8b2-b5b08119be0c'","task":"4f792742-0f98-4b94-bc63-c048bc9e3d82"}
session_stop {"session_id":"b11041f2-ac33-43c0-94ac-715d6f26fd41"}
OK {"task":"3330a613-28cd-4d17-aa70-d42a15ee0575"}
FINISHED
{"ok":true,"return_code":0,"task":"3330a613-28cd-4d17-aa70-d42a15ee0575"}
shutdown
OK



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