Duplication of some special messages

[Makarius]

Special messages, such as priority ones, but probably also tracing, are often duplicated in the output. The *isabelle* buffer contains messages only once, as expected.

This has been reported on Ubuntu with Emacs 23, but also other combinations.

[David Aspinall]

Can you provide a test case?

[Alexander Krauss]

Test case:

• Load the theory "$ISABELLE_HOME/src/HOL/Library/Fundamental_Theorem_Algebra.thy" (as of Isabelle 2009-1)

• Do "Next" three times (the third one actually processes the theory header)

-> In the response buffer, the message 'Loading theory "Polynomial"' appears multiple times (5 times for me), but it should only appear once.

I have this behaviour in many situations with different theories, so this is just an example, and there is nothing special with these concrete theories.

Observed with PG CVS 2009-12-07 12:24 both with and without the patch you send to us last Friday. GNU Emacs 23.1.1 on Debian

[Alexander Krauss]

I noticed now that this behaviour does *not* occur with Isabelle 2009. So there may actually be a change in Isabelle which causes this...

[Makarius]

The above test case works by accident in Isabelle2009, because the warning messages produced by the loaded theory are slightly different.

The following diff applied to Isabelle2009 will reproduce the same problem for the example of Fundamental_Theorem_Algebra.thy above:

diff -r 5c8618f95d24 src/Pure/Isar/code_unit.ML
--- a/src/Pure/Isar/code_unit.ML	Thu Apr 16 17:29:56 2009 +0200
+++ b/src/Pure/Isar/code_unit.ML	Mon May 17 17:33:09 2010 +0200
@@ -61,7 +61,7 @@
 fun bad_thm msg = raise BAD_THM msg;
 fun error_thm f thm = f thm handle BAD_THM msg => error msg;
 fun warning_thm f thm = SOME (f thm) handle BAD_THM msg
-  => (warning ("code generator: " ^ msg); NONE);
+  => NONE;
 fun try_thm f thm = SOME (f thm) handle BAD_THM _ => NONE;
 
 fun string_of_typ thy = setmp show_sorts true (Syntax.string_of_typ_global thy);

Platform note: Mac OS Snow Leopard, Aquamacs 2.0, Poly/ML 5.2.1.

[David Aspinall]

Repeated, thanks for info. Experimental fix in CVS head.

[David Aspinall]

Fix confirmed by a second person, so closing now.