Tue, 02 Jun 2009 22:31:58 +0200 wenzelm superficial tuning;
Tue, 02 Jun 2009 22:00:28 +0200 wenzelm updated versions;
Tue, 02 Jun 2009 21:46:32 +0200 wenzelm type_at: no quotes;
Tue, 02 Jun 2009 21:44:16 +0200 wenzelm tuned;
Tue, 02 Jun 2009 21:36:22 +0200 wenzelm use RichString.* to produce blanks;
Tue, 02 Jun 2009 21:27:51 +0200 wenzelm change_receiver: start only once (already done in actor function);
Tue, 02 Jun 2009 21:20:22 +0200 wenzelm superficial tuning;
Sat, 30 May 2009 23:27:37 +0200 wenzelm slightly more robust treatment of options via arrays;
Sat, 30 May 2009 12:11:40 +0200 wenzelm merged
Wed, 27 May 2009 17:13:58 +0200 immler outer syntax could clash with status on removed commands
Wed, 27 May 2009 17:07:02 +0200 immler no null change
Wed, 27 May 2009 16:23:15 +0200 immler fixed delete markup
Wed, 27 May 2009 15:46:06 +0200 immler check presence of begin, end in attributes
Wed, 27 May 2009 15:24:01 +0200 immler treat comments like seperate commands,
Wed, 27 May 2009 14:56:49 +0200 immler split large changes for faster responses of prover
Mon, 25 May 2009 14:36:40 +0200 immler changed handling of subdirectories
Sat, 30 May 2009 12:11:03 +0200 wenzelm more accurate setup for "jEdit" project;
Sat, 23 May 2009 14:26:51 +0200 wenzelm recovered iso-latin-1 text;
Fri, 22 May 2009 17:36:45 +0200 immler improved handling of markup-information with command=null
Fri, 22 May 2009 16:47:11 +0200 immler implemented links to other files
Fri, 22 May 2009 14:47:57 +0200 immler implemented IsabelleHyperlinkSource (only links inside the current buffer)
Fri, 22 May 2009 13:43:35 +0200 immler corrected offset
Fri, 22 May 2009 13:43:35 +0200 immler fixed duplicate activation
Fri, 22 May 2009 13:43:35 +0200 immler removed debug-painting
Fri, 22 May 2009 13:43:35 +0200 immler let MarkupNode carry arbitrary information
Fri, 22 May 2009 13:43:35 +0200 immler added hyperlink plugin
Fri, 22 May 2009 13:43:35 +0200 immler ML types in tooltip
Fri, 22 May 2009 13:43:34 +0200 immler chaned '+'
Fri, 22 May 2009 13:43:34 +0200 immler reduced to one markup-tree
Fri, 22 May 2009 13:43:34 +0200 immler implemented filter on markup-tree
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip