--- a/src/Tools/jEdit/build.xml Sun Jul 05 17:53:27 2009 +0200
+++ b/src/Tools/jEdit/build.xml Wed Jul 08 13:29:42 2009 +0200
@@ -88,10 +88,14 @@
<!-- dist-template -->
<copy file="dist-template/properties/jedit.props" tofile="${dist.dir}/properties" />
<copy todir="${dist.dir}/modes">
- <fileset dir="dist-template/modes">
- <exclude name="catalog-template" />
- </fileset>
+ <fileset dir="dist-template/modes" />
+ </copy>
+ <copy todir="${dist.dir}/modes" overwrite="true">
+ <fileset dir="${project.jEdit}/modes" />
</copy>
- <copy file="dist-template/modes/catalog-template" tofile="${dist.dir}/modes/catalog" />
+ <replaceregexp byline="true" file="${dist.dir}/modes/catalog">
+ <regexp pattern='(^.*NAME="javacc".*$)'/>
+ <substitution expression="<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>${line.separator}${line.separator}\1"/>
+ </replaceregexp>
</target>
</project>