src/Tools/jEdit/makedist
changeset 34419 30e49efdd4e3
parent 34414 de921b3cb263
child 34461 2dd8ced4f2ae
--- a/src/Tools/jEdit/makedist	Sat Dec 20 14:48:10 2008 +0100
+++ b/src/Tools/jEdit/makedist	Sat Dec 20 16:04:17 2008 +0100
@@ -91,6 +91,10 @@
 
 cp -R "$THIS/dist-template/." "$JEDIT/."
 
+perl -i -e 'while (<>) { if (m/NAME="javacc"/) {
+  print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,; }
+  print; }' "$JEDIT/modes/catalog"
+
 cp jars/Isabelle-jEdit.jar "$JEDIT/jars/isabelle.jar"
 cp jars/lib/Pure.jar "$JEDIT/jars/isabelle-Pure.jar"
 cp jars/lib/core-renderer.jar "$JEDIT/jars/"