How to see all the active Isabelle sessions?

By -

This question is connected with my other question How to export Isabelle session from the Windows installation? . Maybe that other question can be solved if I indicate the correct session name.

So - my question is - how to see all the active Isabelle sessions if jEdit if used for the editing of some custom theory file.

I can call jEdit plugin 'Plugins - Isabelle - Browse Session information' and I am getting the tree in left-side panel:

+ isabelle-session:
  - HOL

So - I guess - HOL is the parent session but the concrete session for the current theory file is something other, maybe default, maybe unnamed?

When I export HOL session, then current theory file is not among the exports. So - I have tried to export this unnamed default session, but without result:

tomr@DESKTOP /cygdrive/c/Homes/Isabelle2021/Isabelle2021
$ isabelle export -O /cygdrive/c/test1 -x *:**  Unsorted
*** Undefined session(s): "Unsorted"

tomr@DESKTOP /cygdrive/c/Homes/Isabelle2021/Isabelle2021
$ isabelle export -O /cygdrive/c/test1 -x *:**  isabelle-session
*** Undefined session(s): "isabelle-session"

So - if I could see all the active sessions, including the name of the most concrete, most low-level session (in which the current theory file is processed directly), then I would be able to export this concrete session and hence - my current theory file for the import into mmt.



from Recent Questions - Stack Overflow https://ift.tt/3rlPzre
https://ift.tt/eA8V8J

Comments

Post a Comment

Popular posts from this blog

Spring Elasticsearch Operations

By -
Elasticsearch Operations Spring Data Elasticsearch uses two interfaces to define the operations that can be called against an Elasticsearch index. These are ElasticsearchOperations and ReactiveElasticsearchOperations. Whereas the first is used with the classic synchronous implementations, the second one uses reactive infrastructure. The default implementations of the interfaces offer: Read/Write mapping support for domain types. A rich query and criteria api. Resource management and Exception translation. ElasticsearchTemplate The ElasticsearchTemplate is an implementation of the ElasticsearchOperations interface using the Transport Client. @Configuration public class TransportClientConfig extends ElasticsearchConfigurationSupport {   @Bean   public Client elasticsearchClient() throws UnknownHostException {                      Settings settings = Settings.builder().put("cluster.name", "elasticsearch")....
Read more

Network Error and Timeout on Authorize.net JS

By -
i am using authorize.net acceptUI.js in order to create a hosted payment form for credit card acceptance. The problem arising now is that, going on the checkout page, I have the following console message: GET https://js.authorize.net/v3/AcceptUI.js net::ERR_NAME_NOT_RESOLVED Which is weird, cause I cannot ping the domain or anything, as my computer cannot resolve the domain. However, this issue is also reported by individual customers and it seems to be sporadically and not happening the entire time, cause i can see other orders going through. Does anyone know how such an error can be caused, or any ideas how it can be resolved? Thanks for your help EDIT: I just checked the A DNS record for js.authorize.net and am getting the following result only: js.authorize.net. 100 IN CNAME js.authorize.net.cdn.cloudflare.net. Doing the same for js.authorize.net.cdn.cloudflare.net. does not return an A Record, unless I specifically instruct to use 1.1.1.1 as DNS server I...
Read more

Object oriented programming concepts (OOPs)

By -
Object-oriented programming (OOP) is a programming paradigm based on the concept of "objects". Re-usability is the main concept of Oops. There are few major principles of object-oriented paradigm. If any programming Language supports this principles that programming language called Object-oriented programming. Below are object oriented programming concepts : 1. Object        Read More about Object     http://theprogrammersfirst.blogspot.in/2016/07/java-object-concept.html
Read more