Hi Lars,
On 29.06.2014 21:35, Lars Noschinski wrote:
On 28.06.2014 17:24, Makarius wrote:
On Sat, 28 Jun 2014, Makarius wrote:
On Sat, 28 Jun 2014, Florian Haftmann wrote:
suggests that something is bad with $JEDIT_HOME in the mira build
environment.
JEDIT_HOME is a normal Isabelle
On 28.06.2014 17:24, Makarius wrote:
On Sat, 28 Jun 2014, Makarius wrote:
On Sat, 28 Jun 2014, Florian Haftmann wrote:
suggests that something is bad with $JEDIT_HOME in the mira build
environment.
JEDIT_HOME is a normal Isabelle setting, provided by the etc/settings
of that component
The problem here is the missing unzip executable on the test machine.
After a second look at the return code 9, I end up with the unzip man
page (on lxbroy10):
9 the specified zipfiles were not found.
Having a look at the code
val jedit_actions =
Lazy.lazy (fn () =
(case
On Sat, 28 Jun 2014, Florian Haftmann wrote:
suggests that something is bad with $JEDIT_HOME in the mira build
environment.
JEDIT_HOME is a normal Isabelle setting, provided by the etc/settings of
that component within Isabelle. So it should normally be there, although
I don't understand
On Sat, 28 Jun 2014, Makarius wrote:
On Sat, 28 Jun 2014, Florian Haftmann wrote:
suggests that something is bad with $JEDIT_HOME in the mira build
environment.
JEDIT_HOME is a normal Isabelle setting, provided by the etc/settings of that
component within Isabelle. So it should normally
On Thu, 19 Sep 2013, Makarius wrote:
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
On Mon, 23 Sep 2013, Makarius wrote:
This is a note on jEdit in general: https://sourceforge.net/projects/jedit/
There is some recent revival of activity around Mac OS X. Hardcore users of
that platform are encouraged to look closely at current jEdit versions --
maybe the daily builds for
This is a note on jEdit in general: https://sourceforge.net/projects/jedit/
There is some recent revival of activity around Mac OS X. Hardcore users
of that platform are encouraged to look closely at current jEdit versions
-- maybe the daily builds for jEdit 5.2pre1 -- to see how it works,
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
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
On Wed, 18 Sep 2013, Tobias Nipkow wrote:
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 seen something like that yesterday, but did not
Am 18/09/2013 17:38, schrieb Makarius:
On Wed, 18 Sep 2013, Tobias Nipkow wrote:
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 seen
On Sat, 31 Aug 2013, Christian Sternagel wrote:
Assuming that the grayish background highlighting really indicates
prover activity in the background
This is outdated_color (RGB=EEE3E3 by default). It means that the
asynchronous protocol is in an intermediate state where the editor has no
Just an observation. Assuming that the grayish background highlighting
really indicates prover activity in the background, I recently noticed
that sometimes a re-check of the whole buffer is done in situations
where this is (as far as I see) not necessary. For example, having
lemma ...
On Sat, 9 Mar 2013, Lars Noschinski wrote:
I'm currently using revision 4b5a5e26161d of Isabelle and after working
with it for one day without stopping jEdit, I noticed a annoying
behaviour of the popup menus which you get automatically by hovering
over a command with a message:
They pop up
On Sat, 9 Mar 2013, Lars Noschinski wrote:
This behaviour only popped up after working with one session for a
longer time and jEdit was having frequent hiccups then, so I guess
this was due to memory pressure (max memory usage was near the limit
of 1600m set for the JVM).
On 03/18/2013 01:29
Hi,
I'm currently using revision 4b5a5e26161d of Isabelle and after working
with it for one day without stopping jEdit, I noticed a annoying
behaviour of the popup menus which you get automatically by hovering
over a command with a message:
They pop up immediately, even if I don't stop over
On Mon, 3 Dec 2012, Makarius wrote:
On Tue, 13 Nov 2012, Lars Noschinski wrote:
Hi,
sometimes, I am encountering some erraneous behaviour of qed when a
structured proof contains some facts for which the final by step failed.
Before the closing block the output buffer reads:
goal:
No
On Thu, 10 Jan 2013, Steffen Juilf Smolka wrote:
Is this the intended behaviour? It used to be different a couple of
month ago. I don't know when it changed exacyly, but I think changeset
a6814de45b69 might be responsible for the change.
Yes, that change is in the vicinity where I was
There might be corner cases where the change of the display leads to odd
effects. Are there concrete incidents already that need to be reconsidered
before the release?
We use Syntax.string_of_term when creating Isar proof scripts in Sledgehammer
and rely on Type.contstraint to introduce
On Fri, 11 Jan 2013, Steffen Juilf Smolka wrote:
We use Syntax.string_of_term when creating Isar proof scripts in
Sledgehammer and rely on Type.contstraint to introduce type annotations
in terms (this does not work with show_markup set to true).
Yes, it is correct to set show_markup=false in
In af8ecf09a58c, type constraints are no longer printed by default in JEdit:
ML {*
@{term f}
| Type.constraint @{typ nat = nat}
| Syntax.string_of_term @{context}
| writeln
*}
# f
Is this the intended behaviour? It used to be different a couple of month ago.
I don't know when it changed
On Tue, 8 Jan 2013, Steffen Juilf Smolka wrote:
The problem is still there on Mountain Lion with an American keyboard.
However, rebinding the kebyoard shortcut locally as you suggested does the
trick - thanks for the tip!
Here is an ugly hack (based on the KeyEventDemo you provided) that
The problem is still there on Mountain Lion with an American keyboard.
However, rebinding the kebyoard shortcut locally as you suggested does the
trick - thanks for the tip!
Here is an ugly hack (based on the KeyEventDemo you provided) that would solve
the problem:
KeyEvent e_ = null;
//
On Wed, 19 Dec 2012, Steffen Juilf Smolka wrote:
in a39250169636, it is possible to increase/decrease the font size in
jedit with cmd++/cmd+- on MacOS (probably ctrl++/ctrl+- on other
plattforms) (nice feature!). However, pressing cmd++ increases the
font size twice on my machine (cmd+- works
On Tue, 13 Nov 2012, Lars Noschinski wrote:
Hi,
sometimes, I am encountering some erraneous behaviour of qed when a
structured proof contains some facts for which the final by step failed.
Before the closing block the output buffer reads:
goal:
No subgoals!
But qed then fails with an
On Sun, 18 Nov 2012, Tobias Nipkow wrote:
Am 16/11/2012 14:47, schrieb Makarius:
On Tue, 2 Oct 2012, Tobias Nipkow wrote:
This is what you should not do: search and replace a string
selectively that occurs many times in a theory. I did this twice (the
second time to see if it was
Am 16/11/2012 14:47, schrieb Makarius:
On Tue, 2 Oct 2012, Tobias Nipkow wrote:
This is what you should not do: search and replace a string selectively that
occurs many times in a theory. I did this twice (the second time to see if it
was repeatable), using Replace Find, and after about 50
Hi everyone,
as can be seen on
http://www21.in.tum.de/~noschinl/jedit-screenshot.png,
(from Isabelle ecffea78d381 on Linux), scroll bars partially obscur the
content of a popup.
BTW, for theorems it would be pretty nifty, if the popup would show the
theorem, not only its name.
--
On Fri, 16 Nov 2012, Lars Noschinski wrote:
Hi everyone,
as can be seen on
http://www21.in.tum.de/~noschinl/jedit-screenshot.png,
(from Isabelle ecffea78d381 on Linux), scroll bars partially obscur the
content of a popup.
BTW, for theorems it would be pretty nifty, if the popup would
On Tue, 2 Oct 2012, Tobias Nipkow wrote:
This is what you should not do: search and replace a string selectively
that occurs many times in a theory. I did this twice (the second time to
see if it was repeatable), using Replace Find, and after about 50
replacements, jedit went all funny and
Hi,
sometimes, I am encountering some erraneous behaviour of qed when a
structured proof contains some facts for which the final by step failed.
Before the closing block the output buffer reads:
goal:
No subgoals!
But qed then fails with an error message:
Failed to finish proof:
goal
On Wed, 24 Oct 2012, Steffen Juilf Smolka wrote:
It seems there is a little (but annoying) issue with the new tooltips in
Isabelle/jEdit when using a font other than IsabelleText. I'm using the
Source Code Pro font and the tooltips are always just a little too small
so that part of the text
First the running gag on isabelle-dev: the new ... or the latest ... is
ill-defined. You have to refer to *the* changeset of the repository version
you are presently testing.
Sorry, I'll keep that in mind.
Concerning Source Code Pro font: I tried it some weeks ago when there was
an
Hi,
It seems there is a little (but annoying) issue with the new tooltips in
Isabelle/jEdit when using a font other than IsabelleText.
I'm using the Source Code Pro font and the tooltips are always just a little
too small so that part of the text is hidden/cut off.
Of course an easy fix would be
On Tue, 2 Oct 2012, Tobias Nipkow wrote:
For example 03bc7afe8814
There is certainly not a general problem of jedit and JVM on Mac OS that covers
all versions of the past and future. Funny things on Mac OS have happened
before, but were sorted out at some point, by looking very closely which
On Tue, 2 Oct 2012, Tobias Nipkow wrote:
This is what you should not do: search and replace a string selectively
that occurs many times in a theory. I did this twice (the second time to
see if it was repeatable), using Replace Find, and after about 50
replacements, jedit went all funny and
For example 03bc7afe8814
Tobias
Am 02/10/2012 20:11, schrieb Makarius:
On Tue, 2 Oct 2012, Tobias Nipkow wrote:
This is what you should not do: search and replace a string selectively that
occurs many times in a theory. I did this twice (the second time to see if it
was repeatable), using
On Tue, 18 Sep 2012, Tobias Nipkow wrote:
When using jedit (development version) I got into the following situation:
partial proof
(* long
comment
*)
Because of the length of the comment (which was a lemma I had to comment
out because due to the partial proof above, proof methods in it
When using jedit (development version) I got into the following situation:
partial proof
(* long
comment
*)
Because of the length of the comment (which was a lemma I had to comment out
because due to the partial proof above, proof methods in it diverged) the end of
the comment was outside
Dear Makarius,
I just started to play around with the latest and greatest
Isabelle/jEdit (there have been several promising commits during my
absence).
Now I wanted to file a bagatelle ;). (I'm on changeset 10b89c127153.)
Minimal example:
- start Isabelle/jEdit
- type theory Scratch
This does work now, maybe my problem was with the repository version.
Larry
On 16 May 2012, at 15:01, Makarius wrote:
I don't see what you mean. In Isabelle2012-RC2 I can type sl, wait 300ms,
press RETURN, and see sledgehammer running and producing Output
incrementally. Then I can click
On Wed, 16 May 2012, Lawrence Paulson wrote:
A quirk of the current setup is that typing “sledgehammer has no
effect; you have to explicitly move the cursor after this keyword before
sledgehammer launches. A menu would solve this problem as well.
I don't see what you mean. In
How can I see the possible cases in an induction, i.e. Show me cases in PG?
Tobias
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
On Tue, May 15, 2012 at 8:18 AM, Tobias Nipkow nip...@in.tum.de wrote:
How can I see the possible cases in an induction, i.e. Show me cases in PG?
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
Am 15/05/2012 08:35, schrieb Brian Huffman:
On Tue, May 15, 2012 at 8:18 AM, Tobias Nipkow nip...@in.tum.de wrote:
How can I see the possible cases in an induction, i.e. Show me cases in PG?
You can type the command print_cases into your theory file (this
also works in PG).
Thanks!
But
On 15.05.2012 08:35, Brian Huffman wrote:
On Tue, May 15, 2012 at 8:18 AM, Tobias Nipkownip...@in.tum.de wrote:
How can I see the possible cases in an induction, i.e. Show me cases in PG?
You can type the command print_cases into your theory file (this
also works in PG).
At least when you
On Wed, 2 May 2012, Christian Sternagel wrote:
would it make sense to introduce some kind of read-only mode for
theory files and then use this mode when jumping to a file that is
already finished (instead of the Attempt to update loaded theory ...
error message)?
Of course I don't know
Dear Makarius,
would it make sense to introduce some kind of read-only mode for
theory files and then use this mode when jumping to a file that is
already finished (instead of the Attempt to update loaded theory ...
error message)?
Of course I don't know whether it is easily possible to
On Fri, 27 Apr 2012, Christian Sternagel wrote:
Maybe I should have tried it myself before posting ;). Yes, it works
with jdk1.6.0_32.
The test website already provides the bundled JDK, which is jdk1.6.0_31
and was produced just before Oracle upgraded to 32 :-(
Fortunately there are hardly
Dear all,
with the current repo head (changeset fe43977e434f) I obtain the
following error when trying to start jEdit (after a successful ./build
-b HOL):
### Building Isabelle/jEdit ...
Changed files:
src/isabelle_sidekick.scala
src/isabelle_sidekick.scala:109: error: trait
Maybe I should have tried it myself before posting ;). Yes, it works
with jdk1.6.0_32.
cheers
chris
On 04/27/2012 01:33 PM, Christian Sternagel wrote:
Dear all,
with the current repo head (changeset fe43977e434f) I obtain the
following error when trying to start jEdit (after a successful
On Wed, 18 Apr 2012, Christian Sternagel wrote:
it's very nice that after sledgehammer found a proof command to finish a
proof, I can simply click on this command in the output buffer to
include it in the main buffer! A slight oddity is that this merges
lines. E.g.,
lemma ⟦xs @ ys = ys @
Dear Makarius,
it's very nice that after sledgehammer found a proof command to finish a
proof, I can simply click on this command in the output buffer to
include it in the main buffer! A slight oddity is that this merges
lines. E.g.,
lemma ⟦xs @ ys = ys @ xs; length xs = length ys⟧ ⟹ xs =
I used a literal ~ and changing this to $HOME solved the problem,
thanks!
cheers
chris
PS: Is it just me or is Isabelle/jEdit really much faster than
ProofGeneral/emacs when loading theories? (Maybe this is due to some
other difference between Isabelle2011-1 and the repo version; I only use
On Wed, 21 Mar 2012, Christian Sternagel wrote:
Is it just me or is Isabelle/jEdit really much faster than
ProofGeneral/emacs when loading theories? (Maybe this is due to some
other difference between Isabelle2011-1 and the repo version; I only use
emacs if I have to stick to Isabelle2011-1.)
On Tue, 20 Mar 2012, Christian Sternagel wrote:
Hi there,
I am using an environment variable in an import statement like
imports $VAR/Theory.thy
in batch-mode this works fine. However, in jEdit I get an error message
indicating Missing theory (file ...) where the path in the error message
On Fri, 2 Mar 2012, Florian Haftmann wrote:
With hg rev 07f9eda810b3: dependencies on ML files declared in theory
header are not resolved properly, e.g. try to edit
src/HOL/Import/HOL4Setup.thy
This is now addressed in 44c28a33c461.
There is a deeper conceptual mismatch behind this recurrent
With hg rev 07f9eda810b3: dependencies on ML files declared in theory
header are not resolved properly, e.g. try to edit
src/HOL/Import/HOL4Setup.thy
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
On 16.01.2012 11:47, Makarius wrote:
On Fri, 13 Jan 2012, Lars Noschinski wrote:
On 13.01.2012 13:49, Lars Noschinski wrote:
lately, Isabelle/jEdit stopped working for me on my work laptop. The
Isabelle process is started (the usual startup phrase is displayed in
the log windows), but the
On Fri, 13 Jan 2012, Lars Noschinski wrote:
On 13.01.2012 13:49, Lars Noschinski wrote:
Hi,
lately, Isabelle/jEdit stopped working for me on my work laptop. The
Isabelle process is started (the usual startup phrase is displayed in
the log windows), but the status is displayed as startup. In
Hi,
lately, Isabelle/jEdit stopped working for me on my work laptop. The
Isabelle process is started (the usual startup phrase is displayed in
the log windows), but the status is displayed as startup. In
particular, no parsing, syntax coloring or proof checking happens; the
polyml processes
On 13.01.2012 13:49, Lars Noschinski wrote:
Hi,
lately, Isabelle/jEdit stopped working for me on my work laptop. The
Isabelle process is started (the usual startup phrase is displayed in
the log windows), but the status is displayed as startup. In
particular, no parsing, syntax coloring or
See also Isabelle/bf7400573617.
Makarius
-- Forwarded message --
Date: Tue, 21 Jun 2011 11:30:19 +0200
From: Vampire vamp...@jedit.org
To: jEdit Announce Mailinglist jedit-annou...@lists.sourceforge.net
Subject: [ jEdit-announce ] jEdit 4.4.1 is out!
Hi all,
I proudly
64 matches
Mail list logo
