[isabelle-dev] PIDE reports on mixfix annotations (notably for datatype)

2016-04-12 Thread Makarius
Mixfix annotations have gained a more formal status recently, with PIDE markup reports that lead to some highlighting and tooltips in the IDE. In order to make this work cleanly, there needs to be exactly one "interning" of the input given by the user. E.g. for the term language this is done

Re: [isabelle-dev] java.lang.ExceptionInInitializerError when starting Isabelle/jEdit

2016-04-12 Thread Lars Hupel
> In Isabelle/cfbb6a5b427c it is done again differently, and hopefully in > a more robust way. Thanks, that seems to have resolved the matter. Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de

Re: [isabelle-dev] Fwd: [isabelle] TERM exception in fologic.ML

2016-04-12 Thread Makarius
On Tue, 12 Apr 2016, Lawrence Paulson wrote: A relevant past message. We have more messages in the archives, about blast ignoring the distinction of Trueprop vs. non-Trueprop propositions. This boils down to the following example, which is non-terminating in Isabelle2016 and current

Re: [isabelle-dev] NEWS: type-inference for object-logic

2016-04-12 Thread Makarius
On Tue, 12 Apr 2016, Peter Lammich wrote: so we're not going to see the annoying "... not of sort 'type'" error any more, which used to occur occasionally in Isabelle/HOL developments!? Yes, but old tools may get broken, if slightly more general types are expected. E.g. see the record

Re: [isabelle-dev] NEWS: type-inference for object-logic

2016-04-12 Thread Peter Lammich
Nice one, so we're not going to see the annoying "... not of sort 'type'" error any more, which used to occur occasionally in Isabelle/HOL developments!? -- Peter On Di, 2016-04-12 at 16:46 +0200, Makarius wrote: > *** General *** > > * Type-inference improves sorts of newly introduced type

Re: [isabelle-dev] java.lang.ExceptionInInitializerError when starting Isabelle/jEdit

2016-04-12 Thread Makarius
On Mon, 11 Apr 2016, Lars Hupel wrote: I wanted to try out some of the changes you made in the past week, but unfortunately, I'm getting exceptions upon starting Isabelle/jEdit. 12:33:24 [main] [error] Plugin: java.lang.ExceptionInInitializerError Odd. I don't see this problem on my

[isabelle-dev] NEWS: type-inference for object-logic

2016-04-12 Thread Makarius
*** General *** * Type-inference improves sorts of newly introduced type variables for the object-logic, using its base sort (i.e. HOL.type for Isabelle/HOL). Thus terms like "f x" or "⋀x. P x" without any further syntactic context produce x::'a::type in HOL instead of x::'a::{} in Pure. Rare

[isabelle-dev] Fwd: [isabelle] TERM exception in fologic.ML

2016-04-12 Thread Lawrence Paulson
A relevant past message. Larry > Begin forwarded message: > > From: Makarius > Subject: Re: [isabelle] TERM exception in fologic.ML > Date: 27 October 2014 at 20:22:02 GMT > To: Slawomir Kolodynski > Cc: "cl-isabelle-us...@lists.cam.ac.uk"

[isabelle-dev] Fwd: [isabelle] TERM exception in fologic.ML

2016-04-12 Thread Lawrence Paulson
I wonder if we can look at this problem, which has been around for at least 18 months. It seems to be connected with the recent modification to hyp_subst_tac, which now retains the equality. (The workaround of switching off this behaviour is not a true solution.) I took a look at this code