[isabelle-dev] Abbreviations + Monad_Syntax introduce unit itself additional type variable
Referring to Isabelle_2013 AND Isabelle_12_Sep_2013:
In the following example, using an abbreviation that contains
monad-syntax introduces a superfluous additional itself-parameter, that,
however, is immediately instantiated to unit itself. Note that, when
replacing abbreviation by definition, everything works as expected.
It looks like (see also my previous post) that monad-syntax has some
severe issues with abbreviations, that I would really like to see fixed
in the next release, as they render unusable many of my tools.
--
Peter
theory Scratch
imports
~~/src/HOL/Library/Monad_Syntax
begin
abbreviation abbr1 == Some () = (%_. Some False)
abbreviation abbr2 == do {
Some ();
Some False
}
(* ### Additional type variable(s) in specification of abbr2: 'a *)
term (abbr1, abbr2)
(*
(Some () = (%_::unit. Some False),
%TYPE::unit itself. Some () = (%_::unit. Some False))
:: bool option * (unit itself = bool option)
*)
definition abbr3 == do {
Some ();
Some False
}
(* No additional type parameter *)
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Dockable window Find
On Thu, 19 Sep 2013, Holger Gast wrote: On 09/18/2013 11:07 PM, Makarius wrote: On Wed, 18 Sep 2013, Holger Gast wrote: Well, one more piece of information about Swing gathered. (Not very useful though: like many people nowadays, I have switched to the much faster and more modern SWT/JFace for my projects anyway.) I count Eclipse/SWT also as a legacy thing. In any case this is not relevant for Isabelle/jEdit: at the very starting point of that project was the observation that GUI frameworks don't count, but editor frameworks. Funny you should say that -- especially in the context of several recent threads about layout management, placement of popup windows, font management, etc. ;( Obviously, the choice of UI frameworks does matter in everyday work on UIs. I am not sure you have understood much about Isabelle/Scala + jEdit to implement PIDE -- even after all these years. All UI frameworks I've seen so far are crap. A UI framework alone does not give you a real editor, you would have to implement that yourself. jEdit as editor framework (or quasi IDE) has turned out as somewhere in the middle -- it does many things, and for things it does not it is reasonably flexible to be adapted (although that is not easy). Its Swing foundations are definitely legacy, but we knew that already from the start. (You were actually the one to see good OO design in Swing and its pluggable LAFs.) If we look today at the factual situation of Prover IDE implementations, there is not just Isabelle/jEdit but also Isabelle/Eclipse from Newcastle. Maybe you want to help them getting SWT into a form that they can catch up with the display qualities of Isabelle/jEdit (sub/superscripts, hyperlinks and formal markup in tooltips etc.). I had to bend Java 2D and Swing quite a bit to make this work, but it has to be repeated for SWT -- and all the portability issues will probably come back once again in a different form. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jedit interface
On Wed, 18 Sep 2013, Tobias Nipkow wrote: I just noticed the following behaviour in 705f0b728b1b: When the cursor remains fixed in the theory window and I scroll in that window with the help of the scoll bar, the output window goes blank when the line with the cursor is no longer visible. I have no idea when that changed but in Isabelle 2013 it was not like that - the output would not go blank. I think it is just a consequence of the major reforms of the document execution model from this summer. Since this is my own department it will be easy to address, and not require descending into the dungeons of JDK sources again. I will come back to this within a few days. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Clone attacks
We also have some overlap between Library/Binomial and Number_Theory/Binomial. --lcp On 19 Sep 2013, at 19:05, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: Since, there 92080294beb8 are two clone theories: Library/Univ_Poly.thy Decision_Procs/Polynomial_List.thy From a superficial glimpse, Decision_Procs/Polynomial_List.thy seems to lag behind Library/Univ_Poly.thy already since the time of its addition. Any suggestions? My first idea is to replace Decision_Procs/Polynomial_List.thy by Library/Univ_Poly.thy »as it is«. Cheers, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de ___ 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
