src/Tools/jEdit/src/Dummy.java
author wenzelm
Sun, 06 Sep 2009 22:27:32 +0200
changeset 34717 3f32e08bbb6c
parent 34437 4eb1b75c746d
permissions -rw-r--r--
sidekick root data: set buffer length to avoid crash of initial caret move; separate Markup_Node, Markup_Tree, Markup_Text; added Markup_Text.flatten; Command.type_at: null-free version; eliminated Command.RootInfo; simplified printing of TypeInfo, RefInfo; added Command.content(Int, Int);

/* dummy class to make ant javadoc work */
package isabelle;
public class Dummy { }