Re: [isabelle-dev] comparison of bindings

[Alexander Krauss]

Hi,


Given to bindings (i.e., instances of Binding.binding), how are they
supposed to be compared?

Here is a more concrete example.  Assume there is a declaration such
as:

   declare_foo name = ...

which declares "name" as some new foo-entity.  For later reference,
the declared foo-entities are best stored in a table internally,
associated with the declaration data (the omitted right-hand side
above).  Indexing this table with the binding produced from "name" is
not possible, as bindings cannot be compared with each other.


As I understand it, it is not the purpose of a binding to identify an 
object during its whole lifetime, but only as a recipe for producing a 
namespace entry (possibly after applying some modifications via 
morphisms etc.).


So I would expect that at some point you actually produce an actual name 
before you store the foo in the table. Depending on the application, you 
could either just use the base name or qualified name 
(Binding.(qualified_)name_of) or use a full-blown namespace (with 
optional qualifiers, concealed entries etc.). I never did the latter, 
though.


Alex
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] comparison of bindings

[Sascha Boehme]

Hi,

Given to bindings (i.e., instances of Binding.binding), how are they
supposed to be compared?

Here is a more concrete example.  Assume there is a declaration such
as:

  declare_foo name = ...

which declares "name" as some new foo-entity.  For later reference,
the declared foo-entities are best stored in a table internally,
associated with the declaration data (the omitted right-hand side
above).  Indexing this table with the binding produced from "name" is
not possible, as bindings cannot be compared with each other.  Using
Binding.print to turn a binding into a string (and using Symtab.table)
doesn't seem to be the right approach (Binding.print is probably not
meant for this purpose).  What should be used instead?

Thanks,
Sascha
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Feedback from a Isabelle tutorial

[Tobias Nipkow]

Command completion needs to be context aware to work well. Otherwise it 
can indeed become a distraction.


Tobias

Am 24/06/2011 22:01, schrieb Alexander Krauss:

Hi all,

Now that this topic is already active, here is more:

In a small course here at TUM
(http://www4.in.tum.de/lehre/vorlesungen/perlen/SS11/) we are also using
jedit exclusively for the first time, and I can confirm the observation
that it makes it slightly easier for newbies to get started. In
particular, the "How can I copy and paste?", "How do I open a file?"
questions all go away, since the editor commands/key sequences are less
obscure. There are also less installation issues (we have no virtualbox
image, but a custom bundle, which I built from a development version).

Here are two (minor) issues I noticed, which do get in the way and may
be easy to fix:

1) Command completion: This may be one of the features that look nice
but are useless in practice and often get in the way: Some frequent
commands are prefixes of other rather obscure commands, which will then
be suggested by the auto-completion: When I type "apply" and pause for a
moment to think, the editor suggests "apply_end", which many users don't
even know about. This steals (a) the focus, as I cannot move the cursor
up/down at this point and (b) my attention.

Another instance, which comes up in an exploratory/teaching context, is
the following scenario:

lemma "x = y" -- some false conjecture
try -- see if it "works"
^ -> counterexample found immediately
cursor is here

At this point I would like to go up and correct the lemma, but I cannot,
since the editor suggests "try_methods" as a completion of "try". I have
to press escape first.

Of course, in an ideal world, I would not have to type "try" in the
first place, but currently this is our way of working.

Suggestion: Simply kill completion of commands (not symbols)???


2) Since entering non-ascii versions of arrows takes two extra
keystrokes and some attention, students tend to just use the ascii
variants. I don't know if this is good or bad, but when I give them a
file for editing that has nice arrows, after editing, it usually has
both versions, and I have to explain that they are the same. I
principle, this could happen with PG/Emacs too, but it normally
wouldn't, because of the automatic substitution.



It is a known issue (if an issue at all) that in Isabelle/jEdit it is
sometimes necessary to cut-and-paste some lines in order to
"synchronize."



This behaviour is indeed getting in the way in practice. It works
according to the "specification" of the editing model, but


What is actually the specification of the editing model? I am just
curious here, and if you can explain it quickly, it may give me an
intuition of what's happening when something goes "wrong" (i.e., as
specified).

Alex
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev