# HG changeset patch
# User wenzelm
# Date 1250975771 -7200
# Node ID d8551606fbab8a9be6f8785dd6ba055ea70b1d4b
# Parent  5b9d7e578756f86daa12f4560d27d7c66fb00a08
removed jedit setup -- now a self-contained component (external);

diff -r 5b9d7e578756 -r d8551606fbab etc/settings
--- a/etc/settings	Sat Aug 22 22:31:00 2009 +0200
+++ b/etc/settings	Sat Aug 22 23:16:11 2009 +0200
@@ -207,22 +207,6 @@
 
 
 ###
-### jEdit
-###
-
-JEDIT_HOME=$(choosefrom \
-  "$ISABELLE_HOME/contrib/jedit" \
-  "$ISABELLE_HOME/../jedit" \
-  "/usr/local/jedit" \
-  "/usr/share/jedit" \
-  "/opt/jedit" \
-  "")
-
-JEDIT_JAVA_OPTIONS=""
-#JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx512m"
-JEDIT_OPTIONS="-reuseview -noserver -nobackground"
-
-###
 ### External reasoning tools
 ###
 
diff -r 5b9d7e578756 -r d8551606fbab lib/Tools/jedit
--- a/lib/Tools/jedit	Sat Aug 22 22:31:00 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: Isabelle/jEdit interface wrapper
-
-
-## diagnostics
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-
-## main
-
-[ -z "$JEDIT_HOME" ] && fail "Missing Isabelle/jEdit installation (JEDIT_HOME)"
-
-INTERFACE="$JEDIT_HOME/interface"
-[ ! -x "$INTERFACE" ] && fail "Bad interface script: \"$INTERFACE\""
-
-exec "$INTERFACE" "$@"