[isabelle] Help file for commands such as "declare [[show_types]]" because jEdit lacks PG features



While experimenting, I saw that Linux Proof General provides certain things that jEdit doesn't. Two being that the external provers work, and that Linux PG can do searches on the Isabelle source code.

I don't need either of those, but it would be nice to get all the information features that PG provides through the menus, such as "show types". This is because I would like to exclusively work in Cygwin jEdit.

Below, I reference a mailing list thread, and I give my input, but I'll make my request first.

REQUEST: It would be nice to have a help file that gives a short description of what the commands do that correspond with the many Proof General menu commands, such as "show types". Additionally, in the help file, it would be nice to have a screenshot which shows me what additional information I'm supposed to be looking for when I perform the command.

All that would take time, so I expect that I'll be firing up Proof General, looking for menu commands that give me useful information, and asking the mailing list what command I use to get that information in the source file.

Now, some details from a thread:

Tobias asked, "How can I see the possible cases in an induction, i.e. Show me cases in PG?"
http://www.mail-archive.com/isabelle-dev at mailbroy.informatik.tu-muenchen.de/msg02677.html

Consequently, Larry asked for menus in jEdit that provides such things:
http://www.mail-archive.com/isabelle-dev at mailbroy.informatik.tu-muenchen.de/msg02681.html

Markarius says it's non-trivial to implement diagnostic functions in the Isabelle/jEdit engine:
http://www.mail-archive.com/isabelle-dev at mailbroy.informatik.tu-muenchen.de/msg02683.html

Brian Huffman says <http://www.mail-archive.com/isabelle-dev at mailbroy.informatik.tu-muenchen.de/msg02678.html>:

   You can type the command "print_cases" into your theory file (this
   also works in PG).

   But then the real question is, how do we expect new users to discover
   this feature?

Brian's comment described and describes my situation. I knew I wanted to see types, and that PG would show types, and that "show_types" was being talked about in the tutorial, but I didn't know how to get jEdit to show me types.

I eventually figured out how to do it.

To show types in jEdit, I insert this command:
      declare [[show_types]], or
      ML{* Config.put show_types true;*}

However, I don't know where I found how to do those commands. I've done a grep on the Isablle distribution folder, and though I find "show_types" in certain PDFs, I don't find anything that explicitly tells me how to use it. This kind of thing is a problem for a newbie: I'm on page 3 of the tutorial, I want to see types, I know that Proof General's menus can activate showing types, but I don't want to use Proof General, I want to use jEdit.

Having a description of all the commands like "show_types" would be useful even if the Isabelle/jEdit engine had a menu system like Proof General. Inserting a series of commands like "declare [[show_types]]" into the source code would be useful when creating templates. It would also be useful to be able to put those commands into a source file that's imported by other source files.

As to menus that would insert these commands into the source code, that's very simple to create in jEdit. Any folder and macro files I put in my USER_HOME "Isabelle2012\jedit\macros" will show up under the jEdit/Macros dropdown menu.

Here's a screenshot of my jedit/macros folder. I've created a macro for "declare [[show_types]]":



jEdit allows you to record macros, but all I did was copy a line of macro code from another macro file. Inside "declare [[show_types]].bsh" is this line of code:

      textArea.setSelectedText("declare [[show_types]]");

Through jEdit Options/jEdit/Shortcuts, I assigned a shortcut to this macro. I can delete and insert the command to my heart's content. After I get past page 3 of the tutorial, and I create a foundational theory that everything else imports, I might put these kind of commands in my foundational theory.

To summarize, it would be nice to have a list of commands like "show_types" with a description of what they do, and a screenshot showing the info they provide, if someone has the time to do that.

--GB






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