diff --git a/src/Tools/jEdit/lib/Tools/jedit b/src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit
+++ b/src/Tools/jEdit/lib/Tools/jedit
@@ -1,417 +1,417 @@
#!/usr/bin/env bash
#
# Author: Makarius
#
# DESCRIPTION: Isabelle/jEdit interface wrapper
## sources
declare -a SOURCES0=(
"src/Tools/jEdit/src-base/dockable.scala"
"src/Tools/jEdit/src-base/isabelle_encoding.scala"
"src/Tools/jEdit/src-base/jedit_lib.scala"
"src/Tools/jEdit/src-base/pide_docking_framework.scala"
"src/Tools/jEdit/src-base/plugin.scala"
"src/Tools/jEdit/src-base/syntax_style.scala"
)
declare -a RESOURCES0=(
"src/Tools/jEdit/src-base/Isabelle_Base.props"
"src/Tools/jEdit/src-base/services.xml"
)
declare -a SOURCES=(
"src/Tools/jEdit/src/active.scala"
"src/Tools/jEdit/src/completion_popup.scala"
"src/Tools/jEdit/src/context_menu.scala"
"src/Tools/jEdit/src/debugger_dockable.scala"
"src/Tools/jEdit/src/document_model.scala"
"src/Tools/jEdit/src/document_view.scala"
"src/Tools/jEdit/src/documentation_dockable.scala"
"src/Tools/jEdit/src/fold_handling.scala"
"src/Tools/jEdit/src/font_info.scala"
"src/Tools/jEdit/src/graphview_dockable.scala"
"src/Tools/jEdit/src/info_dockable.scala"
"src/Tools/jEdit/src/isabelle.scala"
"src/Tools/jEdit/src/isabelle_encoding.scala"
"src/Tools/jEdit/src/isabelle_export.scala"
"src/Tools/jEdit/src/isabelle_options.scala"
"src/Tools/jEdit/src/isabelle_session.scala"
"src/Tools/jEdit/src/isabelle_sidekick.scala"
"src/Tools/jEdit/src/isabelle_vfs.scala"
"src/Tools/jEdit/src/jedit_bibtex.scala"
"src/Tools/jEdit/src/jedit_editor.scala"
"src/Tools/jEdit/src/jedit_lib.scala"
"src/Tools/jEdit/src/jedit_options.scala"
"src/Tools/jEdit/src/jedit_rendering.scala"
"src/Tools/jEdit/src/jedit_resources.scala"
"src/Tools/jEdit/src/jedit_sessions.scala"
"src/Tools/jEdit/src/jedit_spell_checker.scala"
"src/Tools/jEdit/src/keymap_merge.scala"
- "src/Tools/jEdit/src/ml_status.scala"
"src/Tools/jEdit/src/monitor_dockable.scala"
"src/Tools/jEdit/src/output_dockable.scala"
"src/Tools/jEdit/src/plugin.scala"
"src/Tools/jEdit/src/pretty_text_area.scala"
"src/Tools/jEdit/src/pretty_tooltip.scala"
"src/Tools/jEdit/src/process_indicator.scala"
"src/Tools/jEdit/src/protocol_dockable.scala"
"src/Tools/jEdit/src/query_dockable.scala"
"src/Tools/jEdit/src/raw_output_dockable.scala"
"src/Tools/jEdit/src/rich_text_area.scala"
"src/Tools/jEdit/src/scala_console.scala"
"src/Tools/jEdit/src/session_build.scala"
"src/Tools/jEdit/src/simplifier_trace_dockable.scala"
"src/Tools/jEdit/src/simplifier_trace_window.scala"
"src/Tools/jEdit/src/sledgehammer_dockable.scala"
"src/Tools/jEdit/src/state_dockable.scala"
+ "src/Tools/jEdit/src/status_widget.scala"
"src/Tools/jEdit/src/symbols_dockable.scala"
"src/Tools/jEdit/src/syntax_style.scala"
"src/Tools/jEdit/src/syslog_dockable.scala"
"src/Tools/jEdit/src/text_overview.scala"
"src/Tools/jEdit/src/text_structure.scala"
"src/Tools/jEdit/src/theories_dockable.scala"
"src/Tools/jEdit/src/timing_dockable.scala"
"src/Tools/jEdit/src/token_markup.scala"
)
declare -a RESOURCES=(
"src/Tools/jEdit/src/actions.xml"
"src/Tools/jEdit/src/dockables.xml"
"src/Tools/jEdit/src/Isabelle.props"
"src/Tools/jEdit/src/jEdit.props"
"src/Tools/jEdit/src/services.xml"
"src/Tools/jEdit/src/modes/isabelle-ml.xml"
"src/Tools/jEdit/src/modes/isabelle-news.xml"
"src/Tools/jEdit/src/modes/isabelle-options.xml"
"src/Tools/jEdit/src/modes/isabelle-root.xml"
"src/Tools/jEdit/src/modes/isabelle.xml"
"src/Tools/jEdit/src/modes/sml.xml"
)
## diagnostics
PRG="$(basename "$0")"
function usage()
{
echo
echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]"
echo
echo " Options are:"
echo " -A NAME ancestor session for option -R (default: parent)"
echo " -D NAME=X set JVM system property"
echo " -J OPTION add JVM runtime option"
echo " (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
echo " -R NAME build image with requirements from other sessions"
echo " -b build only"
echo " -d DIR include session directory"
echo " -f fresh build"
echo " -i NAME include session in name-space of theories"
echo " -j OPTION add jEdit runtime option"
echo " (default $JEDIT_OPTIONS)"
echo " -l NAME logic session name"
echo " -m MODE add print mode for output"
echo " -n no build of session image on startup"
echo " -p CMD ML process command prefix (process policy)"
echo " -s system build mode for session image (system_heaps=true)"
echo " -u user build mode for session image (system_heaps=false)"
echo
echo " Start jEdit with Isabelle plugin setup and open FILES"
echo " (default \"$USER_HOME/Scratch.thy\" or \":\" for empty buffer)."
echo
exit 1
}
function fail()
{
echo "$1" >&2
exit 2
}
function failed()
{
fail "Failed!"
}
## process command line
# options
BUILD_ONLY=false
FRESH_BUILD=""
ML_PROCESS_POLICY=""
JEDIT_LOGIC_ANCESTOR=""
JEDIT_LOGIC_REQUIREMENTS=""
JEDIT_INCLUDE_SESSIONS=""
JEDIT_SESSION_DIRS="-"
JEDIT_LOGIC=""
JEDIT_PRINT_MODE=""
JEDIT_NO_BUILD=""
JEDIT_BUILD_MODE="default"
function getoptions()
{
OPTIND=1
while getopts "A:BFD:J:R:bd:fi:j:l:m:np:su" OPT
do
case "$OPT" in
A)
JEDIT_LOGIC_ANCESTOR="$OPTARG"
;;
D)
JAVA_ARGS["${#JAVA_ARGS[@]}"]="-D$OPTARG"
;;
J)
JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG"
;;
R)
JEDIT_LOGIC="$OPTARG"
JEDIT_LOGIC_REQUIREMENTS="true"
;;
b)
BUILD_ONLY=true
;;
d)
JEDIT_SESSION_DIRS="$JEDIT_SESSION_DIRS:$OPTARG"
;;
i)
if [ -z "$JEDIT_INCLUDE_SESSIONS" ]; then
JEDIT_INCLUDE_SESSIONS="$OPTARG"
else
JEDIT_INCLUDE_SESSIONS="$JEDIT_INCLUDE_SESSIONS:$OPTARG"
fi
;;
f)
FRESH_BUILD="true"
;;
j)
ARGS["${#ARGS[@]}"]="$OPTARG"
;;
l)
JEDIT_LOGIC="$OPTARG"
;;
m)
if [ -z "$JEDIT_PRINT_MODE" ]; then
JEDIT_PRINT_MODE="$OPTARG"
else
JEDIT_PRINT_MODE="$JEDIT_PRINT_MODE,$OPTARG"
fi
;;
n)
JEDIT_NO_BUILD="true"
;;
p)
ML_PROCESS_POLICY="$OPTARG"
;;
s)
JEDIT_BUILD_MODE="system"
;;
u)
JEDIT_BUILD_MODE="user"
;;
\?)
usage
;;
esac
done
}
eval "declare -a JAVA_ARGS=($JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
declare -a ARGS=()
declare -a OPTIONS; eval "OPTIONS=($ISABELLE_JEDIT_OPTIONS)"
getoptions "${OPTIONS[@]}"
getoptions "$@"
shift $(($OPTIND - 1))
# args
while [ "$#" -gt 0 ]; do
ARGS["${#ARGS[@]}"]="$(platform_path "$1")"
shift
done
## dependencies
if [ -e "$ISABELLE_HOME/Admin/build" ]; then
isabelle browser -b || exit $?
if [ -n "$FRESH_BUILD" ]; then
"$ISABELLE_HOME/Admin/build" jars_fresh || exit $?
else
"$ISABELLE_HOME/Admin/build" jars || exit $?
fi
elif [ -n "$FRESH_BUILD" ]; then
echo >&2 "### Ignoring fresh build option: not a repository clone"
FRESH_BUILD=""
fi
JEDIT_BUILD_JAR="$ISABELLE_JEDIT_BUILD_VERSION/jedit.jar"
declare -a JEDIT_BUILD_JARS=(
"Code2HTML.jar"
"CommonControls.jar"
"Console.jar"
"ErrorList.jar"
"Highlight.jar"
"kappalayout.jar"
"Navigator.jar"
"SideKick.jar"
"idea-icons.jar"
"jsr305-2.0.0.jar"
)
# target
pushd "$ISABELLE_HOME" >/dev/null || failed
TARGET_DIR="src/Tools/jEdit/dist"
TARGET_JAR0="$TARGET_DIR/jars/Isabelle-jEdit-base.jar"
TARGET_JAR="$TARGET_DIR/jars/Isabelle-jEdit.jar"
TARGET_SHASUM="$TARGET_DIR/Isabelle-jEdit.shasum"
declare -a TARGET_DEPS=("lib/classes/Pure.jar" "$TARGET_DIR/jedit.jar")
for DEP in "${JEDIT_BUILD_JARS[@]}"
do
TARGET_DEPS["${#TARGET_DEPS[@]}"]="$TARGET_DIR/jars/$DEP"
done
function target_shasum()
(
shasum -a1 -b "$TARGET_JAR0" "$TARGET_JAR" "${TARGET_DEPS[@]}" \
"${SOURCES0[@]}" "${RESOURCES0[@]}" "${SOURCES[@]}" "${RESOURCES[@]}" 2>/dev/null
)
function target_clean()
{
rm -rf "$ISABELLE_HOME/$TARGET_DIR"
}
[ -n "$FRESH_BUILD" ] && target_clean
## build
BUILD_DIR="$TARGET_DIR/build"
function init_resources ()
{
mkdir -p "$BUILD_DIR" || failed
cp -p -R "$@" "$BUILD_DIR/."
}
function compile_sources()
{
(
#FIXME workarounds for scalac 2.11.0
export CYGWIN="nodosfilewarning"
function stty() { :; }
export -f stty
for DEP in "${TARGET_DEPS[@]}"
do
classpath "$DEP"
done
export CLASSPATH="$(platform_path "$ISABELLE_CLASSPATH")"
isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS -d "$BUILD_DIR" "$@"
) || fail "Failed to compile sources"
}
function make_jar()
{
isabelle_jdk jar -c -f "$1" -C "$BUILD_DIR" . || failed
rm -rf "$ISABELLE_HOME/$BUILD_DIR"
}
target_shasum | cmp "$TARGET_SHASUM" >/dev/null 2>/dev/null
if [ -e "$ISABELLE_HOME/Admin/build" -a "$?" -ne 0 ]; then
echo "### Building Isabelle/jEdit ..."
[ -z "$ISABELLE_JEDIT_BUILD_HOME" ] && \
fail "Unknown ISABELLE_JEDIT_BUILD_HOME -- missing auxiliary component"
target_clean || failed
mkdir -p "$TARGET_DIR" || failed
cp -p -R "$ISABELLE_JEDIT_BUILD_HOME/contrib/$ISABELLE_JEDIT_BUILD_VERSION/." "$TARGET_DIR/."
for DEP in "${JEDIT_BUILD_JARS[@]}"
do
cp -p "$ISABELLE_JEDIT_BUILD_HOME/contrib/$DEP" "$TARGET_DIR/jars/."
done
init_resources "${RESOURCES0[@]}"
compile_sources "${SOURCES0[@]}"
make_jar "$TARGET_JAR0"
classpath "$TARGET_JAR0"
init_resources "${RESOURCES[@]}"
cp src/Tools/jEdit/src/jEdit.props "$TARGET_DIR/properties/."
cp -p -R -f "src/Tools/jEdit/src/modes/." "$TARGET_DIR/modes/."
perl -i -e 'while (<>) {
if (m/FILE="ml.xml"/ or m/FILE_NAME_GLOB="...sml,ml."/ or m/FILE_NAME_GLOB="..ftl"/) { }
elsif (m/NAME="javacc"/) {
print qq!\n\n!;
print qq!\n\n!;
print qq!\n\n!;
print qq!\n\n!;
print qq!\n\n!;
print;
}
elsif (m/NAME="sqr"/) {
print qq!\n\n!;
print;
}
else { print; }
}' "$TARGET_DIR/modes/catalog"
(
cd "$TARGET_DIR"
isabelle_jdk jar -x -f jedit.jar
cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" \
"org/gjt/sp/jedit/icons/themes/classic/32x32/apps/isabelle.gif" || failed
cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" \
"org/gjt/sp/jedit/icons/themes/tango/32x32/apps/isabelle.gif" || failed
isabelle_jdk jar -c -f jedit.jar -e org.gjt.sp.jedit.jEdit org || failed
rm -rf META-INF org
)
compile_sources "${SOURCES[@]}"
make_jar "$TARGET_JAR"
target_shasum > "$TARGET_SHASUM"
cp "$ISABELLE_JEDIT_BUILD_HOME/doc/jedit5.6.0manual-a4.pdf" "$TARGET_DIR/doc/jedit-manual.pdf"
cp "$TARGET_DIR/doc/CHANGES.txt" "$TARGET_DIR/doc/jedit-changes"
cat > "$TARGET_DIR/doc/Contents" </dev/null
if [ "$BUILD_ONLY" = false ]
then
export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_REQUIREMENTS \
JEDIT_INCLUDE_SESSIONS JEDIT_PRINT_MODE JEDIT_NO_BUILD JEDIT_BUILD_MODE
export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY"
classpath "$JEDIT_HOME/dist/jedit.jar"
exec isabelle java -splash:"$(platform_path "$ISABELLE_HOME/lib/logo/isabelle.gif")" \
"${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
fi
diff --git a/src/Tools/jEdit/src/services.xml b/src/Tools/jEdit/src/services.xml
--- a/src/Tools/jEdit/src/services.xml
+++ b/src/Tools/jEdit/src/services.xml
@@ -1,56 +1,56 @@
new isabelle.jedit.Fold_Handling.Fold_Handler();
new isabelle.jedit.Isabelle_Export.VFS();
new isabelle.jedit.Isabelle_Session.VFS();
new isabelle.jedit.Isabelle_Sidekick_Default();
new isabelle.jedit.Isabelle_Sidekick_Context();
new isabelle.jedit.Isabelle_Sidekick_Markup();
new isabelle.jedit.Isabelle_Sidekick_ML();
new isabelle.jedit.Isabelle_Sidekick_SML();
new isabelle.jedit.Isabelle_Sidekick_News();
new isabelle.jedit.Isabelle_Sidekick_Options();
new isabelle.jedit.Isabelle_Sidekick_Root();
new isabelle.jedit.JEdit_Bibtex.Sidekick_Parser();
new isabelle.jedit.Scala_Console();
new isabelle.jedit.Active$Misc_Handler();
new isabelle.jedit.Graphview_Dockable$Handler()
- new isabelle.jedit.ML_Status$Widget_Factory();
+ new isabelle.jedit.Status_Widget$ML_Factory();
diff --git a/src/Tools/jEdit/src/ml_status.scala b/src/Tools/jEdit/src/status_widget.scala
rename from src/Tools/jEdit/src/ml_status.scala
rename to src/Tools/jEdit/src/status_widget.scala
--- a/src/Tools/jEdit/src/ml_status.scala
+++ b/src/Tools/jEdit/src/status_widget.scala
@@ -1,144 +1,144 @@
-/* Title: Tools/jEdit/src/ml_status.scala
+/* Title: Tools/jEdit/src/status_widget.scala
Author: Makarius
ML status bar: heap and garbage collection.
*/
package isabelle.jedit
import isabelle._
import java.awt.{Color, Dimension, Graphics, Graphics2D, Insets, RenderingHints}
import java.awt.font.FontRenderContext
import java.awt.event.{MouseAdapter, MouseEvent}
import javax.swing.{JComponent, JLabel}
import org.gjt.sp.jedit.{View, jEdit}
import org.gjt.sp.jedit.gui.statusbar.{StatusWidgetFactory, Widget}
-object ML_Status
+object Status_Widget
{
private val template = "99999/99999MB"
private class GUI(view: View) extends JComponent
{
/* component state -- owned by GUI thread */
private var status = ML_Statistics.memory_status(Nil)
/* init */
setFont(new JLabel().getFont)
setToolTipText("ML heap memory (double-click for monitor panel)")
private val font_render_context = new FontRenderContext(null, true, false)
private val line_metrics = getFont.getLineMetrics(template, font_render_context)
{
val bounds = getFont.getStringBounds(template, font_render_context)
val dim = new Dimension(bounds.getWidth.toInt, bounds.getHeight.toInt)
setPreferredSize(dim)
setMaximumSize(dim)
}
setForeground(jEdit.getColorProperty("view.status.foreground"))
setBackground(jEdit.getColorProperty("view.status.background"))
def progress_foreground: Color = jEdit.getColorProperty("view.status.memory.foreground")
def progress_background: Color = jEdit.getColorProperty("view.status.memory.background")
/* paint */
private def update(new_status: ML_Statistics.Memory_Status)
{
if (status != new_status) {
status = new_status
repaint()
}
}
override def paintComponent(gfx: Graphics)
{
super.paintComponent(gfx)
val insets = new Insets(0, 0, 0, 0)
val width = getWidth - insets.left - insets.right
val height = getHeight - insets.top - insets.bottom - 1
val (text, fraction) =
status.gc_progress match {
case Some(p) => ("ML cleanup", 1.0 - p)
case None =>
((status.heap_used / 1024 / 1024) + "/" + (status.heap_size / 1024 / 1024) + "MB",
status.heap_used_fraction)
}
val width2 = (width * fraction).toInt
val text_bounds = gfx.getFont.getStringBounds(text, font_render_context)
val text_x = insets.left + ((width - text_bounds.getWidth).toInt / 2)
val text_y = (insets.top + line_metrics.getAscent).toInt
gfx.asInstanceOf[Graphics2D].
setRenderingHint(
RenderingHints.KEY_TEXT_ANTIALIASING,
RenderingHints.VALUE_TEXT_ANTIALIAS_ON)
gfx.setColor(progress_background)
gfx.fillRect(insets.left, insets.top, width2, height)
gfx.setColor(progress_foreground)
gfx.setClip(insets.left, insets.top, width2, height)
gfx.drawString(text, text_x, text_y)
gfx.setColor(getForeground)
gfx.setClip(insets.left + width2, insets.top, getWidth - insets.left - width2, height)
gfx.drawString(text, text_x, text_y)
}
/* main */
private val main =
Session.Consumer[Session.Runtime_Statistics](getClass.getName) {
case stats =>
val status = ML_Statistics.memory_status(stats.props)
GUI_Thread.later { update(status) }
}
override def addNotify()
{
super.addNotify()
PIDE.session.runtime_statistics += main
}
override def removeNotify()
{
super.removeNotify()
PIDE.session.runtime_statistics -= main
}
/* mouse listener */
addMouseListener(new MouseAdapter {
override def mouseClicked(evt: MouseEvent)
{
if (evt.getClickCount == 2) {
view.getInputHandler.invokeAction("isabelle-monitor-float")
}
}
})
}
- class Widget_Factory extends StatusWidgetFactory
+ class ML_Factory extends StatusWidgetFactory
{
override def getWidget(view: View): Widget =
new Widget { override def getComponent: JComponent = new GUI(view) }
}
}