Re: [isabelle-dev] JEdit FAILED
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 setting, provided by the etc/settings of that component within Isabelle. So it should normally be there, although I don't understand the mira setup. Another guess: Isabelle/jEdit is really missing, because of a lacking isabelle jedit -b that is done in regular makedist (e.g. in isatest). mira just executes isabelle build -s -v with job specific options (can be seen in Admin/mira.py). If isabelle jedit -b is a necessary step to setup a fresh Isabelle installation, I can add that to the setup script. I would like to say: go ahead with that. Red signs are supposed to disappear while approaching an release. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] JEdit FAILED
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 within Isabelle. So it should normally be there, although I don't understand the mira setup. Another guess: Isabelle/jEdit is really missing, because of a lacking isabelle jedit -b that is done in regular makedist (e.g. in isatest). mira just executes isabelle build -s -v with job specific options (can be seen in Admin/mira.py). If isabelle jedit -b is a necessary step to setup a fresh Isabelle installation, I can add that to the setup script. BTW: Admin/mira.py is the Isabelle specific part of the mira setup. Unfortunately, the version of the script used is not the one for the version which is tested, but the one which is current on mira startup. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] JEdit FAILED
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 Isabelle_System.bash_output unzip -p \$JEDIT_HOME/dist/jedit.jar\ org/gjt/sp/jedit/actions.xml of (txt, 0) = (case XML.parse txt of XML.Elem ((ACTIONS, _), body) = maps (parse_named ACTION) body | _ = []) | (_, rc) = error (Cannot unzip jedit.jar\nreturn code = ^ string_of_int rc))); suggests that something is bad with $JEDIT_HOME in the mira build environment. Maybe someone of the TUM guys can have a look at that. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] JEdit FAILED
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 the mira setup. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] JEdit FAILED
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 be there, although I don't understand the mira setup. Another guess: Isabelle/jEdit is really missing, because of a lacking isabelle jedit -b that is done in regular makedist (e.g. in isatest). 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 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 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. changeset: 53780:ef62204a126b user:wenzelm date:Sat Sep 21 20:58:32 2013 +0200 files: src/Tools/jEdit/src/document_view.scala description: caret range of active text area counts as visible (e.g. relevant for Output after scrolling outside of text view); It remains to be seen if this is exactly the right notion of visibility to get Output of proof states as expected in most situations. The point here is that the system gives up old prover output when it is considered unreachable by GUI components. This conserves scarce JVM memory resources (see also d598b6231ff7). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jEdit on Mac OS X
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 jEdit 5.2pre1 -- to see how it works, and add items to one of the many trackers of that project. A few more hints: This only makes sense with Oracle Java 7 (e.g. the current 7u40), not the old Apple Java 6. Moreover, it might be actually easier to use the jedit SVN repository with something like ant build, ant run etc. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] jEdit on Mac OS X
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, and add items to one of the many trackers of that project. I have myself submitted various patches already, even though I am only a part-time Mac user myself (since 2008). 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
[isabelle-dev] jedit interface
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 prefer the original behaviour because one often wants to compare the output with some other bits of theory text. Is this an intentional change? Tobias ___ 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: 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 look further. After the update to jdk-7u40 some other fine points suddenly started working, e.g. the persistent window geometry of dockables as on Linux and Windows. Some other things might have stopped working, or just work slightly differently. In both cases I did not ask too many questions yet -- Oracle delivers something and one needs to stomach that, or make worarounds. I prefer the original behaviour because one often wants to compare the output with some other bits of theory text. Is this an intentional change? All this Java + GUI programming is just physics. Not even quantum physics with its clear mathematics behind it, but just classic thermodynamics. I am trying for years to make some island of stability in this world of madness. That is the overall intention behind it. Note that in that respect we are an order of magnitude ahead of anybody else, but it merely shows how crappy all these software frameworks and operating system platforms really are that everybody has to use. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jedit interface
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 something like that yesterday, but did not look further. After the update to jdk-7u40 some other fine points suddenly started working, e.g. the persistent window geometry of dockables as on Linux and Windows. Some other things might have stopped working, or just work slightly differently. In both cases I did not ask too many questions yet -- Oracle delivers something and one needs to stomach that, or make worarounds. Thanks, I expected something like that. If you find time for a workaround it would be appreciated. Tobias I prefer the original behaviour because one often wants to compare the output with some other bits of theory text. Is this an intentional change? All this Java + GUI programming is just physics. Not even quantum physics with its clear mathematics behind it, but just classic thermodynamics. I am trying for years to make some island of stability in this world of madness. That is the overall intention behind it. Note that in that respect we are an order of magnitude ahead of anybody else, but it merely shows how crappy all these software frameworks and operating system platforms really are that everybody has to use. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jEdit: re-checking of main buffer
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 confirmation from the prover about the last round of updates yet. The prover needs to update certain internal administrative structures of the document model until this confirmation (the assignment) can be given back to the editor. This requires usually a few milliseconds, but depends on availability of CPU resources, and can get into the range of 0.5..2 seconds. (What are your hardware parameters?) Until recently (notably in Isabelle2013) these update -- assign cycles of the document model involved explicit cancellation of all running executions of the prover *before* doing anything. There was a restart of transactions that were still needed in the next document version. This was OK for the majority of quick proof commands, but noticable for slow things like 'fun' or heavy proof tools. With the integration of sledgehammer etc. into the document model, the end of this approach was come: accidental cancellation and restart of big ATP jobs was not feasible. So I reworked the whole approach quite substantially. As a consequence the prover never stops, it merely refrains from starting new tasks. Then edits are applied on-line and old tasks are cancelled afterwards if they are no longer needed. This means that there are fewer CPU resources available for doing the administrative update of document content. Often it is just the protocol thread itself, which pretends to be another worker thread for this purpose (this guarantees progress, but a fully saturated worker farm might still work against it). For my part, I've seen the change in behaviour and got used to it after a few days. It is just a matter of tradeoff between seeing more outdated text views vs. long-running tools continuing all the time undisturbed. I am not aware of a genuine problem -- if there is one you should report that again. I recently noticed that sometimes a re-check of the whole buffer An actual re-check would be something else: new execs assigned to existing command transactions, involving a change to pink and purple etc. This should not happen here, unless there is something wrong in the implementation. In fact the new strictly monotonic model should involve fewer re-checks. In the past, a long-running proof step upwards in the buffer could cause a reset to that position with a fresh start of everything in between. when I select the second by auto (typically S+Home, since the courser is positioned directly behind it after just having typed it) and then replace the selected region by something different, the whole buffer is highlighted (thus re-chekced or re-parsed?). Re-parsed is yet another thing: whenever you do some physical edits on the buffer, Isabelle/Scala will check on its side if anything has structurally changed to tell the prover about it. This requires some JVM resources, but it should not be visible in the editing process. Vacous updates in that respect are ignored. On the other hand, just scrolling around is a full update of the document model, and might cause brief appearance of the outdated color scheme. This is particularly relevant to the new print functions and query operations of the document model. Uncovering parts of the text might cause the prover to do anything from plain 'print_state' to 'sledgehammer' (in its auto mode). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] jEdit: re-checking of main buffer
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 ... by auto lemma ... by auto when I select the second by auto (typically S+Home, since the courser is positioned directly behind it after just having typed it) and then replace the selected region by something different, the whole buffer is highlighted (thus re-chekced or re-parsed?). This is not the only such situation, but one that I could reproduce reliably. Note also that -- just making a subjective evaluation by feeling -- that this re-checking happens more frequently in a1cd4126a1c4 (and possibly earlier) than in Isabelle2013. cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jEdit: Automatic popup menus on hovers
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 immediately, even if I don't stop over them. Afterwards, they don't vanish. So if I just want to move the cursor or click on something, these popups get in my way. If I want to do something around a failed proof step, I have to move my mouse very carefully (I got so bad, that I stopped using the mouse and went back to the keyboard). 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). I've spent some days pondering various possibilities and reading sources of Java/Swing libraries. Not everything is clear, but there are various possibilities of memory leaks and timing problems when popping up a new window for each tooltip (in the sense of regular getToolTipText of Swing components). In Isabelle/14e6d761ba1c it is now done in a completely different way. So lets see if this works better. (According to past experience odd corner cases will show up after some weeks or months using it.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jEdit: Automatic popup menus on hovers
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 PM, Makarius wrote: I've spent some days pondering various possibilities and reading sources of Java/Swing libraries. Not everything is clear, but there are various possibilities of memory leaks and timing problems when popping up a new window for each tooltip (in the sense of regular getToolTipText of Swing components). Concerning actual memory leaks, I made the experience that these are rather easy to track down on the JVM: Take a heap dump and analyze it using a suitable tool such as Eclipse Memory Analyzer (http://www.eclipse.org/mat/). The tool has an automated analysis which can usually point out the main sources of memory consumption immediately. Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] jEdit: Automatic popup menus on hovers
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 them. Afterwards, they don't vanish. So if I just want to move the cursor or click on something, these popups get in my way. If I want to do something around a failed proof step, I have to move my mouse very carefully (I got so bad, that I stopped using the mouse and went back to the keyboard). 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). -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jEdit: Inconsistent behaviour with skipped by-proofs
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 subgoals!
But qed then fails with an error message:
Failed to finish proof:
goal (4 subgoals):
{(x, w), (y, w), (w, x), (w, y)} ⊆ edges sG
1. (x, w) ∈ edges (Abs_graph (insert w (verts G), insert (x, w) (insert
(w, x) (insert (w, y) (insert (y, w) (edges G - {(x, y), (y, x)}, fst,
snd))
2. (y, w) ∈ edges (Abs_graph (insert w (verts G), insert (x, w) (insert
(w, x) (insert (w, y) (insert (y, w) (edges G - {(x, y), (y, x)}, fst,
snd))
3. (w, x) ∈ edges (Abs_graph (insert w (verts G), insert (x, w) (insert
(w, x) (insert (w, y) (insert (y, w) (edges G - {(x, y), (y, x)}, fst,
snd))
4. (w, y) ∈ edges (Abs_graph (insert w (verts G), insert (x, w) (insert
(w, x) (insert (w, y) (insert (y, w) (edges G - {(x, y), (y, x)}, fst,
snd))
The subgoals in this message are the remaining goals of a failed qed-step
earlier in this proof.
This is probably an effect of the implicit propagation of exceptions
between task groups, which is essential in batch mode to get all
exceptions together in the end. Here it gets in the way, because the
hopping of failures from one task to another duplicates them in the
document view.
I have made some iterations on it leading up to Isabelle/a7484a7b6c8a, so
there is a chance that it works smoothly for the release.
There is some danger here of provoking odd effects, like loosing errors
that are not officially identified by the position information of the
document model.
Please keep an eye on it for the coming release.
Makarius___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] JEdit: type constraints no longer printed by default
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 working on show_markup. See 1301ed115729 for the first occurrence of the corresponding documentation. So with show_markup enabled, type and sort constraints are moved from the text to the markup over the text. This all works surprisingly well for what it does -- it was considered impossible to do such things a few years ago. 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? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] JEdit: type constraints no longer printed by default
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 type annotations in terms (this does not work with show_markup set to true). Also, we got the error Malformed YXML: multiple results in certain situations. Both problems are solved as of 0583db803066, simply by setting show_markup to false in Sledgehammer. Steffen ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] JEdit: type constraints no longer printed by default
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 the context before printing. Note that this is not specific to jedit, but to Isabelle in general. It is just an accident that jedit is right now the only application that enables show_markup routinely. Also, we got the error Malformed YXML: multiple results in certain situations. In which situations? Do you have an exception trace? The message is from YXML.parse, but in most situations one has YXML.parse_body anyway. And in fact, user code should hardly ever come across anything here, at least in theory. Both problems are solved as of 0583db803066, simply by setting show_markup to false in Sledgehammer. BTW, just formally your data (diff over source) and meta-data (log entry) in the changeset have quite an overlap, close to being a parrot. You should not put historical explanation into the source -- it becomes outdated rather quickly and make the text unreadable. The point where you explain what you think you did is the log. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] JEdit: type constraints no longer printed by default
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 exacyly, but I think changeset a6814de45b69 might
be responsible for the change.
When setting show_markup to false, the behaviour is like it was in the past:
ML {*
@{term f}
| Type.constraint @{typ nat = nat}
| Syntax.string_of_term (@{context} | Config.put show_markup false)
| writeln
*}
# f∷nat ⇒ nat
Regards,
Steffen___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jedit: zoom with cmd++
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 would solve
the problem:
KeyEvent e_ = null;
// pressing a key twice in 5 ms or less is probably impossible
final long eps = 5;
/** Handle the key pressed event from the text field. */
public void keyPressed(final KeyEvent e) {
final boolean process = e_ == null || e.getKeyCode() != e_.getKeyCode()
|| (e.getWhen() - e_.getWhen()) eps;
e_ = e;
if (process) {
displayInfo(e, KEY PRESSED: );
}
}
Before starting such strange patches, we should learn how to submit
reports to Oracle, maybe by taking http://bugreport.sun.com/bugreport/ as
a starting point.
I've never done it for JDK myself so far, and I have no idea how long it
might take for Oracle to move. When Apple was still in charge of its Java
own version (until 1.6), I did file reports occasionally, but it was
hopeleless. Larry Ellison has promised to do better than Steve Jobs.
I won't do anything here myself before the release, though. What is more
immediate for me is to put some (other) patches on some jEdit tracker.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jedit: zoom with cmd++
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;
// pressing a key twice in 5 ms or less is probably impossible
final long eps = 5;
/** Handle the key pressed event from the text field. */
public void keyPressed(final KeyEvent e) {
final boolean process = e_ == null || e.getKeyCode() != e_.getKeyCode()
|| (e.getWhen() - e_.getWhen()) eps;
e_ = e;
if (process) {
displayInfo(e, KEY PRESSED: );
}
}
Steffen
On 07.01.2013, at 11:07, Makarius makar...@sketis.net wrote:
On Sat, 22 Dec 2012, Makarius wrote:
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 fine).
That was one such convenience that I managed to get working after 20min
Windows and Linux, followed by 2 weeks of tinkering on Mac OS X. But that
is not finished yet, and there are remaining problems to treat CTRL, ALT,
COMMAND modifiers properly: it can cause duplication or triplication of key
events.
See also the mail thread on Mac OS X support on Oracle Java 7 that Fabian
Immler has started recently
http://sourceforge.net/mailarchive/message.php?msg_id=30165793
It touches some of the internal issues, including a slightly odd workaround
by myself to modify an older workaround to make it half-working again under
Java 7.
This needs more systematic investigation, by instrumenting the jEdit sources
to produce detailed traces for all critical points where the MacOSX specific
key handling happens. Then it needs to be compared for Java 6 vs. Java 7,
to reconstruct the ideas behind it, which nobody seems to remember on
jedit-devel.
I've spent yet more time on the Mac OS X keyboard problem, which resulted
in change 76ae4e6318fb so far -- you will need the jedit_build update from
the later e7b2cfcef94c to try it yourself.
This now works on all machines I had tried at that point: Windows + Linux +
Mac OS X Mountain Lion, all with German keyboard. Trying it again with Mac
OS X Snow Leopard and English keyboard, I still see the triplication of
COMMAND-EQUALS for the Meta + key, though. Testing that with the low-level
Java key handler that is attached here, it actually shows 3 KEY_PRESSED
events produced by jdk-7u9 on that machine.
So we should blame Oracle or Apple for that ...
If someone comes up with a workaround nonetheless, I will look at it once
more.
Note that by rebinding the keyboard shortcut yourself locally, it will turn
the 3 keystrokes happily into just one editor action.
MakariusKeyEventDemo.java
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jedit: zoom with cmd++
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 fine). That was one such convenience that I managed to get working after 20min Windows and Linux, followed by 2 weeks of tinkering on Mac OS X. But that is not finished yet, and there are remaining problems to treat CTRL, ALT, COMMAND modifiers properly: it can cause duplication or triplication of key events. See also the mail thread on Mac OS X support on Oracle Java 7 that Fabian Immler has started recently http://sourceforge.net/mailarchive/message.php?msg_id=30165793 It touches some of the internal issues, including a slightly odd workaround by myself to modify an older workaround to make it half-working again under Java 7. This needs more systematic investigation, by instrumenting the jEdit sources to produce detailed traces for all critical points where the MacOSX specific key handling happens. Then it needs to be compared for Java 6 vs. Java 7, to reconstruct the ideas behind it, which nobody seems to remember on jedit-devel. I am unsure if I will manage anything like that myself before the Isabelle release. Mac OS X poses a bit too many extra problems, and has a bit too few people actually supporting it actively. On jedit-devel there is right now exactly one Mac OS X guy hanging around. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jEdit: Inconsistent behaviour with skipped by-proofs
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 error message:
Failed to finish proof:
goal (4 subgoals):
{(x, w), (y, w), (w, x), (w, y)} ⊆ edges sG
1. (x, w) ∈ edges (Abs_graph (insert w (verts G), insert (x, w)
(insert (w, x) (insert (w, y) (insert (y, w) (edges G - {(x, y), (y,
x)}, fst, snd))
2. (y, w) ∈ edges (Abs_graph (insert w (verts G), insert (x, w)
(insert (w, x) (insert (w, y) (insert (y, w) (edges G - {(x, y), (y,
x)}, fst, snd))
3. (w, x) ∈ edges (Abs_graph (insert w (verts G), insert (x, w)
(insert (w, x) (insert (w, y) (insert (y, w) (edges G - {(x, y), (y,
x)}, fst, snd))
4. (w, y) ∈ edges (Abs_graph (insert w (verts G), insert (x, w)
(insert (w, x) (insert (w, y) (insert (y, w) (edges G - {(x, y), (y,
x)}, fst, snd))
The subgoals in this message are the remaining goals of a failed
qed-step earlier in this proof.
This is probably an effect of the implicit propagation of exceptions
between task groups, which is essential in batch mode to get all
exceptions together in the end. Here it gets in the way, because the
hopping of failures from one task to another duplicates them in the
document view.
I need to rethink this (again+).
Makarius___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jedit Replace Find
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 repeatable), using Replace Find, and after about 50 replacements, jedit went all funny and screwed up the window manager on my mac. Once I managed to log out (and back in), the window manager was fine again. Did you ever see this incident with Mac OS X again? Yes, I just retried and the beahviour is unchanged (it may have take a bit longer to provoke it). Open Wellfounded.thy and replace wf by something, that does it. This way I managed to reproduce the problem after some rounds of clicking, using Snow Leopard both with the native Mac OS X and Nimbus look feel. Mountain Lion appears to work, at least I did not see anything bad after trying the same 4-5 times longer than on Snow Leopard. So it might be just bad luck of Java 7 on Snow Leopard. Oracle says it does nothing against it nor for it. So if Java 7 happens to work on what Apple considers legacy already, it is mere luck. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jedit Replace Find
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 replacements, jedit went all funny and screwed up the window manager on my mac. Once I managed to log out (and back in), the window manager was fine again. Did you ever see this incident with Mac OS X again? Yes, I just retried and the beahviour is unchanged (it may have take a bit longer to provoke it). Open Wellfounded.thy and replace wf by something, that does it. Tobias Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] jEdit: Scrollbalken in Popups
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. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jEdit: Scrollbalken in Popups
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 show the theorem, not only its name. See also this thread: http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg03350.html It is merely a matter that I did not find time yet to figure out these two main things: (1) precise size of jEdit TextArea inner components (the Painter) (2) control of scrollbars related to that Apart from getting the window size vs TextArea painter size right, I also have the ambition to suppress scrollbars if they are not needed (i.e. in most situations). This requires a very accurate job with the metrics etc. and the scrollbars really need to be there when there are required, otherwise the user won't see parts of the text. If someone else wants to investigate the jEdit sources while I am busy elsewhere, I am keen to get some explanations how I have to approach it. Such jEdit issues typically require 2 hours, 2 days, or 2 weeks to study its sources. I guess this instance is between 2 hours and 2 days. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jedit Replace Find
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 screwed up the window manager on my mac. Once I managed to log out (and back in), the window manager was fine again. Did you ever see this incident with Mac OS X again? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] jEdit: Inconsistent behaviour with skipped by-proofs
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 (4 subgoals):
{(x, w), (y, w), (w, x), (w, y)} ⊆ edges sG
1. (x, w) ∈ edges (Abs_graph (insert w (verts G), insert (x, w)
(insert (w, x) (insert (w, y) (insert (y, w) (edges G - {(x, y), (y,
x)}, fst, snd))
2. (y, w) ∈ edges (Abs_graph (insert w (verts G), insert (x, w)
(insert (w, x) (insert (w, y) (insert (y, w) (edges G - {(x, y), (y,
x)}, fst, snd))
3. (w, x) ∈ edges (Abs_graph (insert w (verts G), insert (x, w)
(insert (w, x) (insert (w, y) (insert (y, w) (edges G - {(x, y), (y,
x)}, fst, snd))
4. (w, y) ∈ edges (Abs_graph (insert w (verts G), insert (x, w)
(insert (w, x) (insert (w, y) (insert (y, w) (edges G - {(x, y), (y,
x)}, fst, snd))
The subgoals in this message are the remaining goals of a failed
qed-step earlier in this proof.
No minimal example yet, I might be able to produce one later this week,
if Makarius does not already now what happens here.
-- Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jEdit: tooltips don't have proper size
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 is hidden/cut off. Of course an easy fix would be to go back to using IsabelleText... 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. Nonetheless, I can guess what you mean and to which version range it might refer: something close to my own latest version of my laptop, which is 8b50286c36d3. (This reference here is important for the mail archive of the list, because in some weeks or months nobody remembers what was current in the past.) These fine points of sizing the Rich_Text_Area are not fully worked out yet, and the next release is still many weeks ahead. I will take your observation is a slight increase of the priority to address it before the release, but this is not sure since many really important things still need to happen elsewhere. Concerning Source Code Pro font: I tried it some weeks ago when there was an announcement somewhere, but dismissed it rather quickly. On JVM/Linux its rendering quality appeared quite weak, and too many of our standard Isabelle symbols are missing. (This can be checked by opening $ISABELLE_HOME_USER/etc/symbols with UTF-8-Isabelle encoding.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jEdit: tooltips don't have proper size
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 announcement somewhere, but dismissed it rather quickly. On JVM/Linux its
rendering quality appeared quite weak, and too many of our standard Isabelle
symbols are missing.
I'm quite happy with the font on MacOS, and the missing symbols haven't been a
problem so far since I usually work in ML{* *}. By the way, the tooltips are
really a great help when programming!
(This can be checked by opening $ISABELLE_HOME_USER/etc/symbols with
UTF-8-Isabelle encoding.)
Ah, good to know!
Steffen
On 27.10.2012, at 16:42, Makarius makar...@sketis.net wrote:
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 is hidden/cut off. Of course an easy fix would be to
go back to using IsabelleText...
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.
Nonetheless, I can guess what you mean and to which version range it might
refer: something close to my own latest version of my laptop, which is
8b50286c36d3. (This reference here is important for the mail archive of the
list, because in some weeks or months nobody remembers what was current in
the past.)
These fine points of sizing the Rich_Text_Area are not fully worked out yet,
and the next release is still many weeks ahead.
I will take your observation is a slight increase of the priority to address
it before the release, but this is not sure since many really important
things still need to happen elsewhere.
Concerning Source Code Pro font: I tried it some weeks ago when there was
an announcement somewhere, but dismissed it rather quickly. On JVM/Linux its
rendering quality appeared quite weak, and too many of our standard Isabelle
symbols are missing. (This can be checked by opening
$ISABELLE_HOME_USER/etc/symbols with UTF-8-Isabelle encoding.)
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] jEdit: tooltips don't have proper size
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 to go back to using IsabelleText... Best Regards Steffen ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jedit Replace Find
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 version of what was used of what component. Actually, what is your Mac OS version? The Mac Pro in my office runs Snow Leopard most of the time, while my MacBook is on Mountain Lion already. I am not testing Lion much. There are two sources of problems with Java/jEdit on Mac OS to be anticipated for the coming months: (1) Special cases in jEdit to accomodate former Apple Java 1.6 now work against Oracle Java 1.7. I've already removed some old key handler workaround to make normal COMMAND-C/X/V work without further ado on Java 1.7. (2) Java 1.7 is officially supported by Oracle only for Lion and Mountain Lion, but usually happens to work on Snow Leopard as well. They don't make plans against it, but they don't support it specifically. In the testing phase of Java 1.7, Oracle had a version for Snow Leopard that was based on a certain update/patch for Apple's Java 1.6. Thus my local machine might now look slightly different to official Java 1.7 and have fewer problems in that respect. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jedit Replace Find
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 screwed up the window manager on my mac. Once I managed to log out (and back in), the window manager was fine again. Can you give your current Isabelle changeset id? Not just as a habit on the isabelle-dev mailing list, but to make any sense for such a report. 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 version of what was used of what component. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jedit Replace Find
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 Replace Find, and after about 50 replacements, jedit went all funny and screwed up the window manager on my mac. Once I managed to log out (and back in), the window manager was fine again. Can you give your current Isabelle changeset id? Not just as a habit on the isabelle-dev mailing list, but to make any sense for such a report. 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 version of what was used of what component. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jedit
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 diverged) the end of the comment was outside the window. Now every time I would extend the partial proof, I would get malformed command syntax and had to scroll down to the end of the comment to make that go away. You have probably noticed that quite a lot has changed here over the summer. I have now tuned the partial comment behaviour again in Isabelle/68796a77c42b. There is an option editor_reparse_limit that is 1 by default, and can be changed in the dialog Plugins / Plugin Options / Isabelle / General. It should be also possible to use the jEdit action Edit / Source / Range Comment to comment out selected areas robustly, although it seems that jEdit does not re-tokenize the result if it happens to cross the visible boundary. It should be correct for the document model nonetheless. The TextTools plugin has a more robust action Toggle Range Comment. Maybe I shall map that to the standard key C-e C-c in the Isabelle/jEdit distribution. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] jedit
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 the window. Now every time I would extend the partial proof, I would get malformed command syntax and had to scroll down to the end of the comment to make that go away. What did I do wrong? (Other than using comments) Tobias ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] jEdit Output Panel
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 (observe the output panel while typing) we get: Outer syntax error: keyword begin expected, but end-of-file was found - continue typing imports Main begin we still have Outer syntax error: keyword begin expected, but end-of-file was found in the output panel (although no errors are indicated in the main buffer or the gutter anymore). It seems as if the output panel is slightly out-of-sync w.r.t. the cursor. cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jedit
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 one of the proposed metis proofs to replace the inlined command by the result -- this was an idea of Alex Krauss to make it work easily without further ado. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jedit
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 Isabelle2012-RC2 I can type sl, wait 300ms, press RETURN, and see sledgehammer running and producing Output incrementally. Then I can click on one of the proposed metis proofs to replace the inlined command by the result -- this was an idea of Alex Krauss to make it work easily without further ado. You should be able to use existing jEdit abbreviations or macro mechanisms to turn this into a single key or menu invocation, but I am not really an expert of this so far. jEdit also has quite good documentation. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] jedit
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
Re: [isabelle-dev] jedit
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 discover this feature? - Brian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jedit
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 then the real question is, how do we expect new users to discover this feature? That is easy: you email the mailing list ;-) Tobias ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jedit
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 once discovered the print_ pattern, auto-completion comes to your rescue ;) -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jEdit
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 whether it is easily possible to distinguish between files that are already loaded as part of a heap image and files that are loaded by hand (which should not be loaded in read-only mode). On a related note: the output of such loaded files is still interesting. Is there any way to make the output immediately available from the heap image, without actually loading the theory (in the end it was already loaded when creating the heap image, but I guess the output is a side-effect and not part of the resulting heap)? This all makes sense, and is in the pipe-line for a long time already. It is all about reforming the old theory loader (and its batch mode) to converge it with the interactive document model that is now seen in the Prover IDE. It will probably take a bit more time to get there, extrapolating from the slow progress of the past 4 years. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] jEdit
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 distinguish between files that are already loaded as part of a heap image and files that are loaded by hand (which should not be loaded in read-only mode). On a related note: the output of such loaded files is still interesting. Is there any way to make the output immediately available from the heap image, without actually loading the theory (in the end it was already loaded when creating the heap image, but I guess the output is a side-effect and not part of the resulting heap)? cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jEdit
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 any significant changes going on the 1.6 branch, so I will probably leave is as is. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] jEdit
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 ListCellRenderer takes
type parameters
new ListCellRenderer {
^
src/isabelle_sidekick.scala:113: error: class JList takes type parameters
list: JList, value: Any, index: Int,
^
src/isabelle_sidekick.scala:109: error: type mismatch;
found : AnyRef{}
required: javax.swing.ListCellRenderer[?: Nothing : Any]
new ListCellRenderer {
^
three errors found
Is this related to the recent change from Java 1.7 to 1.6? In other
words, should I locally fall back to Java 1.6 when using the development
repository?
cheers
chris
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jEdit
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 ./build
-b HOL):
### Building Isabelle/jEdit ...
Changed files:
src/isabelle_sidekick.scala
src/isabelle_sidekick.scala:109: error: trait ListCellRenderer takes
type parameters
new ListCellRenderer {
^
src/isabelle_sidekick.scala:113: error: class JList takes type parameters
list: JList, value: Any, index: Int,
^
src/isabelle_sidekick.scala:109: error: type mismatch;
found : AnyRef{}
required: javax.swing.ListCellRenderer[?: Nothing : Any]
new ListCellRenderer {
^
three errors found
Is this related to the recent change from Java 1.7 to 1.6? In other
words, should I locally fall back to Java 1.6 when using the development
repository?
cheers
chris
___
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
Re: [isabelle-dev] jEdit
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 @ xs; length xs = length ys⟧ ⟹ xs = ys sledgehammer end After sledgehammer reports remote_e: Try this: by (metis append_eq_conv_conj) (21 ms). In the output buffer. I click on by (metis append_eq_conv_conj) and the result is. lemma ⟦xs @ ys = ys @ xs; length xs = length ys⟧ ⟹ xs = ys by (metis append_eq_conv_conj)end Maybe this could be changed such that end stays on its own line? I've destroyed this recently when changing the meaning of a command span, to include its trailing white spans, which miraculously cuts the total number of command transactions in half and thus improves editing performance. In Isabelle/26d0a76fef0a it should work again. I've made further refinements here and in Isabelle/9980c0c094b8 So even without the long anticipated integration of asynchronous agents into the Isabelle/jEdit document model, which I had to cancel again for this release to take place, sledgehammer should work reasonably well. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] jEdit
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 = ys sledgehammer end After sledgehammer reports remote_e: Try this: by (metis append_eq_conv_conj) (21 ms). In the output buffer. I click on by (metis append_eq_conv_conj) and the result is. lemma ⟦xs @ ys = ys @ xs; length xs = length ys⟧ ⟹ xs = ys by (metis append_eq_conv_conj)end Maybe this could be changed such that end stays on its own line? cheers chris ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jEdit import theories
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 emacs if I have to stick to Isabelle2011-1.) On 03/21/2012 01:24 AM, Makarius wrote: 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 shows that $VAR was used relative to the path of the surrounding theory file. $VAR contains something like ~/some-path and was intended as being applied globally. changeset: e3a3f161ad70 jedit_build: 20120313 Odd, I think it should work. There is an explicit treatment of symbolic Isabelle paths (with a certain notion of variables) and the jEdit/JVM platform path notion. See also http://isabelle.in.tum.de/repos/isabelle/file/1ab41ea5b1c6/src/Tools/jEdit/src/jedit_thy_load.scala#l22 What does not work right now is to use VFS paths of jEdit together with Isabelle ones. I would love to see theory sources being loaded via ssh or http at some point ... In the example above, do you have a literal ~ or its expansion by the operating system shell? It is more robust to use $HOME in shell scripts if you mean home. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jEdit import theories
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.) Ça depend, as the French like to say. Isabelle/jEdit in Isabelle2011-1 and repository versions until today (8e1b14bf0190) uses a uniform model to process buffer content, intermixed with potential user edits, with full document markup reports that eventually causes the Haribo effect in the sources. This is done in a reasonably fast way, but there are still situations where too many goal states are printed and thus the prover session gets overloaded. (E.g. in Hoare_Parallel or AFP/JinjaThreads.) In contrast, Proof General / Emacs is very slow in processing the current buffer (especially on Mac OS), but resolves imports via the batch-mode theory loader of Isabelle, which is presently faster than any other way of processing theories. (The same is used for isabelle usedir/make/makeall.) The general direction is to unify old-style batch loading with new-style document processing, such that it is both very fast and produces the full markup. It will also overcome occasional confusions about different behaviour of tools in different modes of theory processing. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jEdit import theories
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 shows that $VAR was used relative to the path of the surrounding theory file. $VAR contains something like ~/some-path and was intended as being applied globally. changeset: e3a3f161ad70 jedit_build: 20120313 Odd, I think it should work. There is an explicit treatment of symbolic Isabelle paths (with a certain notion of variables) and the jEdit/JVM platform path notion. See also http://isabelle.in.tum.de/repos/isabelle/file/1ab41ea5b1c6/src/Tools/jEdit/src/jedit_thy_load.scala#l22 What does not work right now is to use VFS paths of jEdit together with Isabelle ones. I would love to see theory sources being loaded via ssh or http at some point ... In the example above, do you have a literal ~ or its expansion by the operating system shell? It is more robust to use $HOME in shell scripts if you mean home. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jEdit Problem report
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 problem. Theory imports are managed by the editor front-end, but uses by the prover. To get this really right eventually, tools need to load auxiliary files relatively to the master theory source, e.g. via Thy_Load.load_file, but some details are still to be settled. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] jEdit Problem report
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 signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jEdit: Loading theories does not work
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 status is displayed as startup. In particular, no parsing, syntax coloring or proof checking happens; the polyml processes seem to be mostly idle. I bisected the problem down to the following commit: Please ignore this for now; if found an error in my test setup. Will try again on monday. OK, please keep me up to date about the situation. Embarassingly, it seems that I always started jEdit with an out-of-date heap image and did not realize this my whole testing. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jEdit: Loading theories does not work
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 particular, no parsing, syntax coloring or proof checking happens; the polyml processes seem to be mostly idle. I bisected the problem down to the following commit: Please ignore this for now; if found an error in my test setup. Will try again on monday. OK, please keep me up to date about the situation. Last week I've only had a brief look at the change 30a69cd8a9a0 that you've quoted, but did not see anything suspicious and could not reproduce the described problem. Generally, strange phenomena when moving between machines and/or plaforms occasionally did happen in the past. For example, the startup phase and pipe synchronization turned out as unreliable on Windows/Cygwin, so I made and alternative mechanism based on sockets, see http://isabelle.in.tum.de/repos/isabelle/file/f23dc7d16c0b/src/Pure/System/system_channel.scala#l18, but this exposed some oddities with sockets in some Poly/ML versions that we still support officially. I ended up tinkering almost one week on the seemingly trivial problem of connecting too processes by a reliable byte-channel. Those who are brave enough to test the repository verions by using it regularly are welcome to post whatever oddities they observe. This is how things can get ironed out eventually. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] jEdit: Loading theories does not work
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 seem to be mostly idle. I bisected the problem down to the following commit: changeset: 46121:30a69cd8a9a0c9d539fceba286bb93bc0c3154ca Author: wenzelm Date: Thu Jan 05 14:15:37 2012 +0100 prefer raw_message for protocol implementation; As for the dependencies, * scala-2.8.2-final (but happens with 2.9.1-final and 2.8.1-final, too) * my systems java is 1.6.0_26 from Sun * jedit_build-20110622 (but happens with jedit_build-20111217, too) * the contrib/ directory is the one from Isabelle2011-1 I could not reproduce this problem on my other machine, which (apart from scala-2.8.1) uses the same components. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jEdit: Loading theories does not work
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 proof checking happens; the polyml processes seem to be mostly idle. I bisected the problem down to the following commit: Please ignore this for now; if found an error in my test setup. Will try again on monday. Sorry, Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] [ jEdit-announce ] jEdit 4.4.1 is out! (fwd)
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 present 4.4.1, the first official stable release of the
4.4 series of jEdit.
I want to appologize again for the confusion that arised when the faulty
4.4 release was created and then taken back down. To avoid confusion
about what version someone is using, the 4.4 release is skipped
completely.
Here are some convenient links to see the live state of major problems:
- Bugs which are marked as severe:
http://sourceforge.net/tracker/?group_id=588atid=100588status=1artgroup=101607
- Bugs which are marked as regressive:
http://sourceforge.net/tracker/?group_id=588atid=100588status=1artgroup=619797
Volunteers are always welcome to fix these bugs:
http://www.jedit.org/index.php?page=devel
That being said, here is the download link:
http://www.jedit.org/index.php?page=download
FYI, merge requests for the 4.4 series (fix done, but waiting for a review):
http://sourceforge.net/tracker/?group_id=588atid=1235750status=1artgroup=1360914
For those who want to stick with the 4.3 series of jEdit we also
created a new bugfix release 4.3.3. (see separate announcement mail)
Have fun with the new release.
Regards
Björn Vampire Kautler
jEdit 4.4 version history
(changes since jEdit 4.3)
:encoding=UTF-8:
{{{ Version 4.4.1
Thanks to Björn Vampire Kautler, Kazutoshi Satoda, Alan Ezust,
and Matthieu Casanova for contributing to this release.
{{{ Bug Fixes
- Collapsing all folds will move the caret outside any fold if necessary
(Matthieu Casanova)
- Fixed an exception that occurs when opening jEdit from command line
with some files to open as argument if a jEdit server is running
(#3173669 - Matthieu Casanova)
- jEdit now force drops from external applications to be COPY and not
MOVE drops. It prevents ftp explorer from deleting dropped files
(#1208598 - Matthieu Casanova)
- Changing bufferset scopes now saved to properties as default scope.
(#3316329 - Matthieu Casanova)
- Buffersets no longer populated with open files when creating new view.
(#2990965 - Matthieu Casanova and Alan Ezust)
- BufferSet contents of new Plain View #3317405 fixed (Matthieu Casanova)
- When the cursor was at a start (or end) of non-top (non-bottom) line,
Find Next (Previous) for a non-empty regex starting with ^ (ending
with $) wrongly skipped the occurrence at the cursor.
(SF.net bug #2953604 - Kazutoshi Satoda)
- Corrected a wrong specifications (javadoc comments) of
SearchMatcher#nextMatch(). (SF.net bug #2953604 - Kazutoshi Satoda)
- Fixed an exception that prevent from opening properties dialog of non local
files in the VFS Browser (#3199876 - Matthieu Casanova)
- Remove sending to background from the Linux start script, otherwise it cannot
be used properly as commit editor with the -wait option or to get the -usage
output on the commandline properly (Björn Vampire Kautler)
- Improve integration with Unity Launcher. Without this change if you pin jEdit
to the Launcher and then run it, a separate icon for the running instance is
shown. With this change this is correctly merged with the pinned starter.
(Björn Vampire Kautler)
}}}
}}}
jEdit buffer local properties:
:folding=explicit:collapseFolds=2:
--
EditLive Enterprise is the world's most technically advanced content
authoring tool. Experience the power of Track Changes, Inline Image
Editing and ensure content is compliant with Accessibility Checking.
http://p.sf.net/sfu/ephox-dev2dev
___
jEdit Announcement List
jedit-annou...@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/jedit-announce___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
