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.Context_Menu(); 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) } } }