# HG changeset patch # User wenzelm # Date 1263245487 -3600 # Node ID 502f9096748313427bbd2658bd7da85f038bcba7 # Parent c1509b9d624f56e00a34e24be2a04f1f77e9807f# Parent d5bb188b9f9d18720a4ce7c117a30100eee86ee2 merged with converted/relocated copy of http://isabelle.in.tum.de/repos/isabelle-jedit/rev/93d884afa74b diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/README_BUILD --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/README_BUILD Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,73 @@ + +Requirements to build from sources +================================== + +* Proper Java JRE/JDK from Sun, e.g. 1.6.0_17 + http://java.sun.com/javase/downloads/index.jsp + +* Netbeans 6.7 + http://www.netbeans.org/downloads/index.html + +* Scala for Netbeans: version 6.7v1 for NB 6.7 + http://sourceforge.net/project/showfiles.php?group_id=192439&package_id=256544 + http://blogtrader.net/dcaoyuan/category/NetBeans + http://wiki.netbeans.org/Scala + +* jEdit 4.3 (final) + http://www.jedit.org/ + + Netbeans Project "jEdit": install official sources as ./contrib/jEdit/. + +* jEdit plugins: + Netbeans Library "SideKick" = $HOME/.jedit/jars/SideKick.jar + Netbeans Library "ErrorList" = $HOME/.jedit/jars/ErrorList.jar + Netbeans Library "Hyperlinks" = $HOME/.jedit/jars/Hyperlinks.jar + +* Cobra Renderer 0.98.4 + http://lobobrowser.org/cobra.jsp + Netbeans Library "Cobra-Renderer" = .../cobra.jar + Netbenas Library "Rhino-JavaScript" = .../js.jar + +* Isabelle/Pure Scala components + Netbeans Library "Isabelle-Pure" = ~~/lib/classes/Pure.jar + + +Running the application within Netbeans +======================================= + +* Project properties: add "Run" argument like + -noserver -nobackground -settings=/home/makarius/isabelle/isabelle-jedit/dist + +* The Isabelle environment is obtained automatically via + "$ISABELLE_HOME/bin/isabelle getenv", where ISABELLE_HOME is determined as follows: + + (1) via regular Isabelle settings, + e.g. "isabelle env netbeans" + + (2) or via ISABELLE_HOME from raw process environment, + e.g. "env ISABELLE_HOME=.../Isabelle netbeans" + + (3) or via JVM system properties (cf. "Run / VM Options") + e.g. -Disabelle.home=.../Isabelle + + +Misc notes +========== + +- Netbeans config/Editors/Preferences/...-CustomPreferences.xml + + + + + +----------------------------------------------------------------------- +To run jedit with remote debugging enabled, I use the following +command: "java +-agentlib:jdwp=transport=dt_socket,suspend=y,server=y,address=XXXX +-jar jedit.jar" + +where XXXX is any open port number you wish. The above invocation +works for Sun's JDK 5.0. There's an alternate incantation for earlier +releases. (See +http://java.sun.com/j2se/1.5.0/docs/guide/jpda/conninv.html) +----------------------------------------------------------------------- diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/build.xml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/build.xml Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,102 @@ + + + + + + Builds, tests, and runs the project Isabelle-jEdit. + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/contrib/jEdit/build-nb.xml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/contrib/jEdit/build-nb.xml Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,41 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + This target can only run inside the NetBeans IDE. + + + + + + + + + + + + + \ No newline at end of file diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/contrib/jEdit/nbproject/project.xml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/contrib/jEdit/nbproject/project.xml Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,118 @@ + + + org.netbeans.modules.ant.freeform + + + jEdit + + + + jEdit + + build-nb.xml + + + + jEdit + . + UTF-8 + + + Source Packages + java + . + build/** doc/** icons/** macros/** modes/** package-files/** + UTF-8 + + + + + + build + + + + clean + + + + docs-javadoc + + + + run + + + + clean + build + + + + debug-nb + + + + jar + build/jEdit.jar + + build + + + + + Source Packages + . + build/** doc/** icons/** macros/** modes/** package-files/** + + + ${ant.script} + + + + + + + + + + + + + + + + . + . + build/jEdit.jar + 1.5 + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/dist-template/etc/settings --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/dist-template/etc/settings Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,9 @@ +JEDIT_HOME="$COMPONENT" + +JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss2m" +#JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx1024m -Xss4m" +JEDIT_OPTIONS="-reuseview -noserver -nobackground" + +ISABELLE_JEDIT_OPTIONS="-m xsymbols -m no_brackets -m no_type_brackets" + +ISABELLE_TOOLS="$ISABELLE_TOOLS:$JEDIT_HOME/lib/Tools" diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/dist-template/lib/Tools/jedit --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/dist-template/lib/Tools/jedit Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,117 @@ +#!/usr/bin/env bash +# +# Author: Makarius +# +# DESCRIPTION: Isabelle/jEdit interface wrapper + + +## diagnostics + +PRG="$(basename "$0")" + +usage() +{ + echo + echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]" + echo + echo " Options are:" + echo " -J OPTION add JVM runtime option" + echo " (default JEDIT_JAVA_OPTIONS=$JEDIT_JAVA_OPTIONS)" + echo " -d enable debugger" + echo " -j OPTION add jEdit runtime option" + echo " (default JEDIT_OPTIONS=$JEDIT_OPTIONS)" + echo " -l NAME logic image name (default ISABELLE_LOGIC=$ISABELLE_LOGIC)" + echo " -m MODE add print mode for output" + echo + echo "Start jEdit with Isabelle plugin setup and opens theory FILES" + echo "(default ~/Scratch.thy)." + echo + exit 1 +} + +fail() +{ + echo "$1" >&2 + exit 2 +} + + +## process command line + +# options + +JEDIT_LOGIC="$ISABELLE_LOGIC" +JEDIT_PRINT_MODE="" + +getoptions() +{ + OPTIND=1 + while getopts "J:dj:l:m:" OPT + do + case "$OPT" in + J) + JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG" + ;; + d) + JAVA_ARGS["${#JAVA_ARGS[@]}"]="-Xdebug" + JAVA_ARGS["${#JAVA_ARGS[@]}"]="-Xrunjdwp:transport=dt_socket,server=y,suspend=n" + ;; + 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 + ;; + \?) + usage + ;; + esac + done +} + +declare -a JAVA_ARGS; eval "JAVA_ARGS=($JEDIT_JAVA_OPTIONS)" +[ -n "$SCALA_HOME" ] && JAVA_ARGS["${#JAVA_ARGS[@]}"]="-Dscala.home=$SCALA_HOME" + +declare -a ARGS; eval "ARGS=($JEDIT_OPTIONS)" + +declare -a OPTIONS; eval "OPTIONS=($ISABELLE_JEDIT_OPTIONS)" +getoptions "${OPTIONS[@]}" + +getoptions "$@" +shift $(($OPTIND - 1)) + + +# args + +if [ "$#" -eq 0 ]; then + ARGS["${#ARGS[@]}"]="Scratch.thy" +else + while [ "$#" -gt 0 ]; do + ARGS["${#ARGS[@]}"]="$(jvmpath "$1")" + shift + done +fi + + +## main + +case "$JEDIT_LOGIC" in + /*) + ;; + */*) + JEDIT_LOGIC="$(pwd -P)/$JEDIT_LOGIC" + ;; +esac + +export JEDIT_LOGIC JEDIT_PRINT_MODE + +exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \ + -jar "$(jvmpath "$JEDIT_HOME/jedit.jar")" \ + "-settings=$(jvmpath "$ISABELLE_HOME_USER/jedit")" "${ARGS[@]}" diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/dist-template/modes/isabelle-session.xml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/dist-template/modes/isabelle-session.xml Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,41 @@ + + + + + + + + + + + + + + + + + (* + *) + + + {* + *} + + + ` + ` + + + " + " + + + session + parent + imports + uses + options + dependencies + + + diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/dist-template/modes/isabelle.xml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/dist-template/modes/isabelle.xml Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,43 @@ + + + + + + + + + + + + + + + + + + + (* + *) + + + {* + *} + + + ` + ` + + + " + " + + + header + theory + imports + uses + begin + end + + + diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/dist-template/properties/jedit.props --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/dist-template/properties/jedit.props Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,191 @@ +#jEdit properties +buffer.deepIndent=false +buffer.encoding=UTF-8-Isabelle +buffer.indentSize=2 +buffer.lineSeparator=\n +buffer.maxLineLen=100 +buffer.noTabs=true +buffer.sidekick.keystroke-parse=true +buffer.tabSize=2 +delete-line.shortcut=A+d +delete.shortcut2=C+d +encoding.opt-out.Big5-HKSCS=true +encoding.opt-out.Big5=true +encoding.opt-out.COMPOUND_TEXT=true +encoding.opt-out.EUC-JP=true +encoding.opt-out.EUC-KR=true +encoding.opt-out.GB18030=true +encoding.opt-out.GB2312=true +encoding.opt-out.GBK=true +encoding.opt-out.IBM-Thai=true +encoding.opt-out.IBM00858=true +encoding.opt-out.IBM01140=true +encoding.opt-out.IBM01141=true +encoding.opt-out.IBM01142=true +encoding.opt-out.IBM01143=true +encoding.opt-out.IBM01144=true +encoding.opt-out.IBM01145=true +encoding.opt-out.IBM01146=true +encoding.opt-out.IBM01147=true +encoding.opt-out.IBM01148=true +encoding.opt-out.IBM01149=true +encoding.opt-out.IBM037=true +encoding.opt-out.IBM1026=true +encoding.opt-out.IBM1047=true +encoding.opt-out.IBM273=true +encoding.opt-out.IBM277=true +encoding.opt-out.IBM278=true +encoding.opt-out.IBM280=true +encoding.opt-out.IBM284=true +encoding.opt-out.IBM285=true +encoding.opt-out.IBM297=true +encoding.opt-out.IBM420=true +encoding.opt-out.IBM424=true +encoding.opt-out.IBM437=true +encoding.opt-out.IBM500=true +encoding.opt-out.IBM775=true +encoding.opt-out.IBM850=true +encoding.opt-out.IBM852=true +encoding.opt-out.IBM855=true +encoding.opt-out.IBM857=true +encoding.opt-out.IBM860=true +encoding.opt-out.IBM861=true +encoding.opt-out.IBM862=true +encoding.opt-out.IBM863=true +encoding.opt-out.IBM864=true +encoding.opt-out.IBM865=true +encoding.opt-out.IBM866=true +encoding.opt-out.IBM868=true +encoding.opt-out.IBM869=true +encoding.opt-out.IBM870=true +encoding.opt-out.IBM871=true +encoding.opt-out.IBM918=true +encoding.opt-out.ISO-2022-CN=true +encoding.opt-out.ISO-2022-JP-2=true +encoding.opt-out.ISO-2022-JP=true +encoding.opt-out.ISO-2022-KR=true +encoding.opt-out.ISO-8859-13=true +encoding.opt-out.ISO-8859-2=true +encoding.opt-out.ISO-8859-3=true +encoding.opt-out.ISO-8859-4=true +encoding.opt-out.ISO-8859-5=true +encoding.opt-out.ISO-8859-6=true +encoding.opt-out.ISO-8859-7=true +encoding.opt-out.ISO-8859-8=true +encoding.opt-out.ISO-8859-9=true +encoding.opt-out.JIS_X0201=true +encoding.opt-out.JIS_X0212-1990=true +encoding.opt-out.KOI8-R=true +encoding.opt-out.KOI8-U=true +encoding.opt-out.Shift_JIS=true +encoding.opt-out.TIS-620=true +encoding.opt-out.UTF-16=true +encoding.opt-out.UTF-16BE=true +encoding.opt-out.UTF-16LE=true +encoding.opt-out.UTF-32=true +encoding.opt-out.UTF-32BE=true +encoding.opt-out.UTF-32LE=true +encoding.opt-out.X-UTF-32BE-BOM=true +encoding.opt-out.X-UTF-32LE-BOM=true +encoding.opt-out.windows-1250=true +encoding.opt-out.windows-1251=true +encoding.opt-out.windows-1253=true +encoding.opt-out.windows-1254=true +encoding.opt-out.windows-1255=true +encoding.opt-out.windows-1256=true +encoding.opt-out.windows-1257=true +encoding.opt-out.windows-1258=true +encoding.opt-out.windows-31j=true +encoding.opt-out.x-Big5-Solaris=true +encoding.opt-out.x-EUC-TW=true +encoding.opt-out.x-IBM1006=true +encoding.opt-out.x-IBM1025=true +encoding.opt-out.x-IBM1046=true +encoding.opt-out.x-IBM1097=true +encoding.opt-out.x-IBM1098=true +encoding.opt-out.x-IBM1112=true +encoding.opt-out.x-IBM1122=true +encoding.opt-out.x-IBM1123=true +encoding.opt-out.x-IBM1124=true +encoding.opt-out.x-IBM1381=true +encoding.opt-out.x-IBM1383=true +encoding.opt-out.x-IBM33722=true +encoding.opt-out.x-IBM737=true +encoding.opt-out.x-IBM834=true +encoding.opt-out.x-IBM856=true +encoding.opt-out.x-IBM874=true +encoding.opt-out.x-IBM875=true +encoding.opt-out.x-IBM921=true +encoding.opt-out.x-IBM922=true +encoding.opt-out.x-IBM930=true +encoding.opt-out.x-IBM933=true +encoding.opt-out.x-IBM935=true +encoding.opt-out.x-IBM937=true +encoding.opt-out.x-IBM939=true +encoding.opt-out.x-IBM942=true +encoding.opt-out.x-IBM942C=true +encoding.opt-out.x-IBM943=true +encoding.opt-out.x-IBM943C=true +encoding.opt-out.x-IBM948=true +encoding.opt-out.x-IBM949=true +encoding.opt-out.x-IBM949C=true +encoding.opt-out.x-IBM950=true +encoding.opt-out.x-IBM964=true +encoding.opt-out.x-IBM970=true +encoding.opt-out.x-ISCII91=true +encoding.opt-out.x-ISO-2022-CN-CNS=true +encoding.opt-out.x-ISO-2022-CN-GB=true +encoding.opt-out.x-JIS0208=true +encoding.opt-out.x-JISAutoDetect=true +encoding.opt-out.x-Johab=true +encoding.opt-out.x-MS932_0213=true +encoding.opt-out.x-MS950-HKSCS=true +encoding.opt-out.x-MacArabic=true +encoding.opt-out.x-MacCentralEurope=true +encoding.opt-out.x-MacCroatian=true +encoding.opt-out.x-MacCyrillic=true +encoding.opt-out.x-MacDingbat=true +encoding.opt-out.x-MacGreek=true +encoding.opt-out.x-MacHebrew=true +encoding.opt-out.x-MacIceland=true +encoding.opt-out.x-MacRoman=true +encoding.opt-out.x-MacRomania=true +encoding.opt-out.x-MacSymbol=true +encoding.opt-out.x-MacThai=true +encoding.opt-out.x-MacTurkish=true +encoding.opt-out.x-MacUkraine=true +encoding.opt-out.x-PCK=true +encoding.opt-out.x-SJIS_0213=true +encoding.opt-out.x-UTF-16LE-BOM=true +encoding.opt-out.x-euc-jp-linux=true +encoding.opt-out.x-eucJP-Open=true +encoding.opt-out.x-iso-8859-11=true +encoding.opt-out.x-mswin-936=true +encoding.opt-out.x-windows-50220=true +encoding.opt-out.x-windows-50221=true +encoding.opt-out.x-windows-874=true +encoding.opt-out.x-windows-949=true +encoding.opt-out.x-windows-950=true +encoding.opt-out.x-windows-iso2022jp=true +encodingDetectors=BOM XML-PI buffer-local-property +fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII +firstTime=false +isabelle-protocol.dock-position=bottom +isabelle-results.dock-position=bottom +isabelle.activate.shortcut=CS+ENTER +mode.isabelle.sidekick.showStatusWindow.label=true +sidekick-tree.dock-position=right +sidekick.buffer-save-parse=true +sidekick.complete-delay=300 +tip.show=false +view.antiAlias=standard +view.blockCaret=true +view.caretBlink=false +view.eolMarkers=false +view.extendedState=0 +view.font=IsabelleText +view.fontsize=18 +view.fracFontMetrics=false +view.gutter.fontsize=12 +view.middleMousePaste=true +view.showToolbar=false diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/makedist --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/makedist Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,98 @@ +#!/usr/bin/env bash +# +# makedist -- make Isabelle/jEdit distribution + +## self references + +PRG=$(basename "$0") +THIS=$(cd "$(dirname "$0")"; pwd) +SUPER=$(cd "$THIS/.."; pwd) + + +## diagnostics + +JEDIT_HOME="/home/isajedit/jedit-orig/4.3pre17" + +function usage() +{ + echo + echo "Usage: $PRG [OPTIONS]" + echo + echo " Options are:" + echo " -j DIR specify original jEdit distribution" + echo " (default: $JEDIT_HOME)" + echo + echo " Produce Isabelle/jEdit distribution from Netbeans build" + echo " in $THIS/dist" + echo + exit 1 +} + +fail() +{ + echo "$1" >&2 + exit 2 +} + + +## process command line + +# options + +while getopts "j:s:" OPT +do + case "$OPT" in + j) + JEDIT_HOME="$OPTARG" + ;; + \?) + usage + ;; + esac +done + +shift $(($OPTIND - 1)) + + +# args + +[ "$#" -ne 0 ] && usage + + +## main + +cd "$THIS/dist" || fail "Bad directory: $THIS/dist" + + +# target name + +VERSION=$(basename "$JEDIT_HOME") +JEDIT="jedit-${VERSION}" + +rm -rf "$JEDIT" jedit +mkdir "$JEDIT" +ln -s "$JEDIT" jedit + + +# copy stuff + +[ "$JEDIT_HOME/jedit.jar" ] || fail "Bad original jEdit directory: $JEDIT_HOME" +cp -R "$JEDIT_HOME/." "$JEDIT/." +rm -rf "$JEDIT/jEdit" "$JEDIT/build-support" + +mkdir -p "$JEDIT/jars" +cp -R jars/. "$JEDIT/jars/." + +cp -R "$THIS/dist-template/." "$JEDIT/." + +perl -i -e 'while (<>) { if (m/NAME="javacc"/) { + print qq,\n\n,; + print qq,\n\n,; } + print; }' "$JEDIT/modes/catalog" + + +# build archive + +echo "${JEDIT}.tar.gz" +tar czf "${JEDIT}.tar.gz" "$JEDIT" jedit +ln -sf "${JEDIT}.tar.gz" jedit.tar.gz diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/manifest.mf --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/manifest.mf Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,3 @@ +Manifest-Version: 1.0 +X-COMMENT: Main-Class will be added automatically by build + diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/nbproject/build-impl.xml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/nbproject/build-impl.xml Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,709 @@ + + + + + + + + + + + + + + + + + + +You must set SCALA_HOME or environment property and append "-J-Dscala.home=scalahomepath" +property to the end of "netbeans_default_options" in NetBeansInstallationPath/etc/netbeans.conf to point to +Scala installation directory. + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Must set src.dir + Must set build.dir + Must set dist.dir + Must set build.classes.dir + Must set dist.javadoc.dir + Must set build.test.classes.dir + Must set build.test.results.dir + Must set build.classes.excludes + Must set dist.jar + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Must set javac.includes + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Must set javac.includes + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Must select some files in the IDE or set javac.includes + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + To run this application from the command line without Ant, try: + + + + + + + java -cp "${run.classpath.with.dist.jar}" ${main.class} + + + + + + + + + + + + + + + + + + + + + + + + To run this application from the command line without Ant, try: + + java -jar "${dist.jar.resolved}" + + + + + + + + + + + + + + + + + + + + Must select one file in the IDE or set run.class + + + + + + + + + + + + + + + + + + + + Must select one file in the IDE or set debug.class + + + + + Must set fix.includes + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Must select some files in the IDE or set javac.includes + + + + + + + + + + + + + + + + + + Some tests failed; see details above. + + + + + + + + + Must select some files in the IDE or set test.includes + + + + Some tests failed; see details above. + + + + + Must select one file in the IDE or set test.class + + + + + + + + + + + + + + + + + + + + + + + + + + + Must select one file in the IDE or set applet.url + + + + + + + + + Must select one file in the IDE or set applet.url + + + + + + + + + + + + + + + + + + + + + diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/nbproject/genfiles.properties --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/nbproject/genfiles.properties Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,8 @@ +build.xml.data.CRC32=d2379ac2 +build.xml.script.CRC32=2db9d955 +build.xml.stylesheet.CRC32=ca9d572e +# This file is used by a NetBeans-based IDE to track changes in generated files such as build-impl.xml. +# Do not edit this file. You may delete it but then the IDE will never regenerate such files for you. +nbproject/build-impl.xml.data.CRC32=8f41dcce +nbproject/build-impl.xml.script.CRC32=69f2059c +nbproject/build-impl.xml.stylesheet.CRC32=bc42a706@1.3.0 diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/nbproject/project.properties --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/nbproject/project.properties Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,77 @@ +application.title=Isabelle-jEdit +application.vendor=makarius +application.args=-noserver -nobackground +build.classes.dir=${build.dir}/classes +build.classes.excludes=**/*.java,**/*.form,**/*.scala +# This directory is removed when the project is cleaned: +build.dir=build +build.generated.dir=${build.dir}/generated +# Only compile against the classpath explicitly listed here: +build.sysclasspath=ignore +build.test.classes.dir=${build.dir}/test/classes +build.test.results.dir=${build.dir}/test/results +debug.classpath=\ + ${run.classpath} +debug.test.classpath=\ + ${run.test.classpath} +# This directory is removed when the project is cleaned: +dist.dir=dist +# dist can be used as jEdits settings-directory; +# jEdit searches for plugins in the 'jars' subdirectory +# must include something like this to private.properties: +# application.args=-noserver -nobackground -settings=/absolute/path/to/project/dist +# +dist.jar=${dist.dir}/jars/Isabelle-jEdit.jar +dist.javadoc.dir=${dist.dir}/javadoc +excludes= +file.reference.isabelle-jedit-src=src +file.reference.jedit.jar=/home/makarius/lib/jedit/current/jedit.jar +includes=** +jar.compress=false +java.platform.active=java_default_platform +javac.classpath=\ + ${reference.jEdit.build}:\ + ${libs.Isabelle-Pure.classpath}:\ + ${libs.Cobra-Renderer.classpath}:\ + ${libs.Rhino-JavaScript.classpath}:\ + ${libs.ErrorList.classpath}:\ + ${libs.Hyperlinks.classpath}:\ + ${libs.SideKick.classpath}:\ + ${libs.Console.classpath}:\ + ${libs.Scala-compiler.classpath} +# Space-separated list of extra javac options +javac.compilerargs= +javac.deprecation=false +javac.source=1.5 +javac.target=1.5 +javac.test.classpath=\ + ${javac.classpath}:\ + ${build.classes.dir}:\ + ${libs.junit.classpath}:\ + ${libs.junit_4.classpath} +javadoc.additionalparam= +javadoc.author=false +javadoc.encoding=${source.encoding} +javadoc.noindex=false +javadoc.nonavbar=false +javadoc.notree=false +javadoc.private=false +javadoc.splitindex=true +javadoc.use=true +javadoc.version=false +javadoc.windowtitle= +main.class=org.gjt.sp.jedit.jEdit +manifest.file=manifest.mf +meta.inf.dir=${src.dir}/META-INF +platform.active=default_platform +project.jEdit=contrib/jEdit +reference.jEdit.build=${project.jEdit}/build/jEdit.jar +run.classpath=\ + ${javac.classpath}:\ + ${build.classes.dir} +run.jvmargs=-Xms128m -Xmx512m +run.test.classpath=\ + ${javac.test.classpath}:\ + ${build.test.classes.dir} +source.encoding=UTF-8 +src.dir=${file.reference.isabelle-jedit-src} diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/nbproject/project.xml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/nbproject/project.xml Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,24 @@ + + + org.netbeans.modules.scala.project + + + Isabelle-jEdit + 1.6.5 + + + + + + + + jEdit + jar + + build + clean + build + + + + diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/plugin/Isabelle.props --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/plugin/Isabelle.props Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,48 @@ +## Isabelle plugin properties +## +##:encoding=ISO-8859-1: + +#identification +plugin.isabelle.jedit.Plugin.name=Isabelle +plugin.isabelle.jedit.Plugin.author=Johannes H�lzl, Fabian Immler, Makarius Wenzel +plugin.isabelle.jedit.Plugin.version=0.0.1 +plugin.isabelle.jedit.Plugin.description=Isabelle/Isar asynchronous proof processing + +#system parameters +plugin.isabelle.jedit.Plugin.activate=startup +plugin.isabelle.jedit.Plugin.usePluginHome=false + +#dependencies +plugin.isabelle.jedit.Plugin.depend.0=jdk 1.6 +plugin.isabelle.jedit.Plugin.depend.1=jedit 04.03.17.00 +plugin.isabelle.jedit.Plugin.depend.2=plugin errorlist.ErrorListPlugin 1.7 +plugin.isabelle.jedit.Plugin.depend.3=plugin sidekick.SideKickPlugin 0.7.6 +plugin.isabelle.jedit.Plugin.depend.4=plugin gatchan.jedit.hyperlinks.HyperlinksPlugin 1.0.1 + +#options +plugin.isabelle.jedit.Plugin.option-pane=isabelle +options.isabelle.label=Isabelle +options.isabelle.code=new isabelle.jedit.Isabelle_Options(); +options.isabelle.logic.title=Logic +options.isabelle.font-size.title=Font Size +options.isabelle.font-size=14 +options.isabelle.startup-timeout=10000 + +#menu actions +plugin.isabelle.jedit.Plugin.menu.label=Isabelle +plugin.isabelle.jedit.Plugin.menu=isabelle.activate isabelle.show-output isabelle.show-protocol +isabelle.activate.label=Activate current buffer +isabelle.show-output.label=Show Output +isabelle.show-protocol.label=Show Protocol + +#dockables +isabelle-output.title=Output +isabelle-protocol.title=Protocol + +#SideKick +sidekick.parser.isabelle.label=Isabelle +mode.isabelle.sidekick.parser=isabelle +mode.ml.sidekick.parser=isabelle + +#Hyperlinks +mode.isabelle.hyperlink.source=isabelle diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/plugin/actions.xml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/plugin/actions.xml Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,23 @@ + + + + + +


+			isabelle.jedit.Isabelle.switch_active(view);
+

+ + return isabelle.jedit.Isabelle.is_active(view); + + + +


+			wm.addDockableWindow("isabelle-output");
+

+ + +


+			wm.addDockableWindow("isabelle-protocol");
+

+ + \ No newline at end of file diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/plugin/dockables.xml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/plugin/dockables.xml Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,11 @@ + + + + + + new isabelle.jedit.Output_Dockable(view, position); + + + new isabelle.jedit.Protocol_Dockable(view, position); + + \ No newline at end of file diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/plugin/services.xml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/plugin/services.xml Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,17 @@ + + + + + + new isabelle.jedit.Isabelle_Encoding(); + + + new isabelle.jedit.Isabelle_Sidekick(); + + + new isabelle.jedit.Isabelle_Hyperlinks(); + + + new isabelle.jedit.Scala_Console(); + + diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/src/Dummy.java --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/Dummy.java Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,3 @@ +/* dummy class to make ant javadoc work */ +package isabelle; +public class Dummy { } diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/src/jedit/document_model.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/jedit/document_model.scala Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,145 @@ +/* + * Document model connected to jEdit buffer + * + * @author Fabian Immler, TU Munich + * @author Makarius + */ + +package isabelle.jedit + + +import isabelle.proofdocument.{Change, Command, Document, Session} + +import scala.actors.Actor, Actor._ +import scala.collection.mutable + +import org.gjt.sp.jedit.Buffer +import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer} +import org.gjt.sp.jedit.syntax.{ModeProvider, SyntaxStyle} + + +object Document_Model +{ + /* document model of buffer */ + + private val key = "isabelle.document_model" + + def init(session: Session, buffer: Buffer): Document_Model = + { + Swing_Thread.assert() + val model = new Document_Model(session, buffer) + buffer.setProperty(key, model) + model.activate() + model + } + + def apply(buffer: Buffer): Option[Document_Model] = + { + Swing_Thread.assert() + buffer.getProperty(key) match { + case model: Document_Model => Some(model) + case _ => None + } + } + + def exit(buffer: Buffer) + { + Swing_Thread.assert() + apply(buffer) match { + case None => error("No document model for buffer: " + buffer) + case Some(model) => + model.deactivate() + buffer.unsetProperty(key) + } + } +} + +class Document_Model(val session: Session, val buffer: Buffer) +{ + /* history */ + + private val document_0 = session.begin_document(buffer.getName) + + @volatile private var history = // owned by Swing thread + new Change(document_0.id, None, Nil, Future.value(Nil, document_0)) + + def current_change(): Change = history + def recent_document(): Document = current_change().ancestors.find(_.is_assigned).get.join_document + + + /* transforming offsets */ + + private def changes_from(doc: Document): List[Text_Edit] = + { + Swing_Thread.assert() + (edits_buffer.toList /: + current_change.ancestors.takeWhile(_.id != doc.id))((edits, change) => change.edits ::: edits) + } + + def from_current(doc: Document, offset: Int): Int = + (offset /: changes_from(doc).reverse) ((i, change) => change before i) + + def to_current(doc: Document, offset: Int): Int = + (offset /: changes_from(doc)) ((i, change) => change after i) + + def lines_of_command(doc: Document, cmd: Command): (Int, Int) = + { + val start = doc.command_start(cmd).get // FIXME total? + val stop = start + cmd.length + (buffer.getLineOfOffset(to_current(doc, start)), + buffer.getLineOfOffset(to_current(doc, stop))) + } + + + /* text edits */ + + private val edits_buffer = new mutable.ListBuffer[Text_Edit] // owned by Swing thread + + private val edits_delay = Swing_Thread.delay_last(300) { + if (!edits_buffer.isEmpty) { + val new_change = current_change().edit(session, edits_buffer.toList) + edits_buffer.clear + history = new_change + new_change.result.map(_ => session.input(new_change)) + } + } + + + /* buffer listener */ + + private val buffer_listener: BufferListener = new BufferAdapter + { + override def contentInserted(buffer: JEditBuffer, + start_line: Int, offset: Int, num_lines: Int, length: Int) + { + edits_buffer += new Text_Edit(true, offset, buffer.getText(offset, length)) + edits_delay() + } + + override def preContentRemoved(buffer: JEditBuffer, + start_line: Int, start: Int, num_lines: Int, removed_length: Int) + { + edits_buffer += new Text_Edit(false, start, buffer.getText(start, removed_length)) + edits_delay() + } + } + + + /* activation */ + + def activate() + { + buffer.setTokenMarker(new Isabelle_Token_Marker(this)) + buffer.addBufferListener(buffer_listener) + buffer.propertiesChanged() + + edits_buffer += new Text_Edit(true, 0, buffer.getText(0, buffer.getLength)) + edits_delay() + } + + def deactivate() + { + buffer.setTokenMarker(buffer.getMode.getTokenMarker) + buffer.removeBufferListener(buffer_listener) + } +} diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/src/jedit/document_view.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/jedit/document_view.scala Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,303 @@ +/* + * Document view connected to jEdit text area + * + * @author Fabian Immler, TU Munich + * @author Makarius + */ + +package isabelle.jedit + + +import isabelle.proofdocument.{Command, Document, Session} + +import scala.actors.Actor._ + +import java.awt.event.{MouseAdapter, MouseEvent} +import java.awt.{BorderLayout, Graphics, Dimension, Color, Graphics2D} +import javax.swing.{JPanel, ToolTipManager} +import javax.swing.event.{CaretListener, CaretEvent} + +import org.gjt.sp.jedit.gui.RolloverButton +import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter} + + +object Document_View +{ + def choose_color(command: Command, doc: Document): Color = + { + doc.current_state(command).map(_.status) match { + case Some(Command.Status.UNPROCESSED) => new Color(255, 228, 225) + case Some(Command.Status.FINISHED) => new Color(234, 248, 255) + case Some(Command.Status.FAILED) => new Color(255, 193, 193) + case _ => Color.red + } + } + + + /* document view of text area */ + + private val key = new Object + + def init(model: Document_Model, text_area: TextArea): Document_View = + { + Swing_Thread.assert() + val doc_view = new Document_View(model, text_area) + text_area.putClientProperty(key, doc_view) + doc_view.activate() + doc_view + } + + def apply(text_area: TextArea): Option[Document_View] = + { + Swing_Thread.assert() + text_area.getClientProperty(key) match { + case doc_view: Document_View => Some(doc_view) + case _ => None + } + } + + def exit(text_area: TextArea) + { + Swing_Thread.assert() + apply(text_area) match { + case None => error("No document view for text area: " + text_area) + case Some(doc_view) => + doc_view.deactivate() + text_area.putClientProperty(key, null) + } + } +} + + +class Document_View(model: Document_Model, text_area: TextArea) +{ + private val session = model.session + + + /* visible document -- owned by Swing thread */ + + @volatile private var document = model.recent_document() + + + /* buffer of changed commands -- owned by Swing thread */ + + @volatile private var changed_commands: Set[Command] = Set() + + private val changed_delay = Swing_Thread.delay_first(100) { + if (!changed_commands.isEmpty) { + document = model.recent_document() + for (cmd <- changed_commands if document.commands.contains(cmd)) { // FIXME cover doc states as well!!? + update_syntax(cmd) + invalidate_line(cmd) + overview.repaint() + } + changed_commands = Set() + } + } + + + /* command change actor */ + + private case object Exit + + private val command_change_actor = actor { + loop { + react { + case command: Command => // FIXME rough filtering according to document family!? + Swing_Thread.now { + changed_commands += command + changed_delay() + } + + case Exit => reply(()); exit() + + case bad => System.err.println("command_change_actor: ignoring bad message " + bad) + } + } + } + + + /* text_area_extension */ + + private val text_area_extension = new TextAreaExtension + { + override def paintValidLine(gfx: Graphics2D, + screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int) + { + def from_current(pos: Int) = model.from_current(document, pos) + def to_current(pos: Int) = model.to_current(document, pos) + val metrics = text_area.getPainter.getFontMetrics + val saved_color = gfx.getColor + try { + for ((command, command_start) <- + document.command_range(from_current(start), from_current(end))) + { + val begin = start max to_current(command_start) + val finish = (end - 1) min to_current(command_start + command.length) + encolor(gfx, y, metrics.getHeight, begin, finish, + Document_View.choose_color(command, document), true) + } + } + finally { gfx.setColor(saved_color) } + } + + override def getToolTipText(x: Int, y: Int): String = + { + val offset = model.from_current(document, text_area.xyToOffset(x, y)) + document.command_at(offset) match { + case Some((command, command_start)) => + document.current_state(command).get.type_at(offset - command_start).getOrElse(null) + case None => null + } + } + } + + + /* caret_listener */ + + private var _selected_command: Command = null + private def selected_command = _selected_command + private def selected_command_=(cmd: Command) + { + _selected_command = cmd + session.results.event(cmd) + } + + private val caret_listener = new CaretListener + { + override def caretUpdate(e: CaretEvent) + { + document.command_at(e.getDot) match { + case Some((command, command_start)) if (selected_command != command) => + selected_command = command + case _ => + } + } + } + + + /* (re)painting */ + + private val update_delay = Swing_Thread.delay_first(500) { model.buffer.propertiesChanged() } + + private def update_syntax(cmd: Command) + { + val (line1, line2) = model.lines_of_command(document, cmd) + if (line2 >= text_area.getFirstLine && + line1 <= text_area.getFirstLine + text_area.getVisibleLines) + update_delay() + } + + private def invalidate_line(cmd: Command) = + { + val (start, stop) = model.lines_of_command(document, cmd) + text_area.invalidateLineRange(start, stop) + + if (selected_command == cmd) + session.results.event(cmd) + } + + private def invalidate_all() = + text_area.invalidateLineRange(text_area.getFirstPhysicalLine, + text_area.getLastPhysicalLine) + + private def encolor(gfx: Graphics2D, + y: Int, height: Int, begin: Int, finish: Int, color: Color, fill: Boolean) + { + val start = text_area.offsetToXY(begin) + val stop = + if (finish < model.buffer.getLength) text_area.offsetToXY(finish) + else { + val p = text_area.offsetToXY(finish - 1) + val metrics = text_area.getPainter.getFontMetrics + p.x = p.x + (metrics.charWidth(' ') max metrics.getMaxAdvance) + p + } + + if (start != null && stop != null) { + gfx.setColor(color) + if (fill) gfx.fillRect(start.x, y, stop.x - start.x, height) + else gfx.drawRect(start.x, y, stop.x - start.x, height) + } + } + + + /* overview of command status left of scrollbar */ + + private val overview = new JPanel(new BorderLayout) + { + private val WIDTH = 10 + private val HEIGHT = 2 + + setPreferredSize(new Dimension(WIDTH, 0)) + + setRequestFocusEnabled(false) + + addMouseListener(new MouseAdapter { + override def mousePressed(event: MouseEvent) { + val line = y_to_line(event.getY) + if (line >= 0 && line < text_area.getLineCount) + text_area.setCaretPosition(text_area.getLineStartOffset(line)) + } + }) + + override def addNotify() { + super.addNotify() + ToolTipManager.sharedInstance.registerComponent(this) + } + + override def removeNotify() { + ToolTipManager.sharedInstance.unregisterComponent(this) + super.removeNotify + } + + override def getToolTipText(event: MouseEvent): String = + { + val line = y_to_line(event.getY()) + if (line >= 0 && line < text_area.getLineCount) "TODO:
Tooltip" + else "" + } + + override def paintComponent(gfx: Graphics) + { + super.paintComponent(gfx) + val buffer = model.buffer + + for ((command, start) <- document.command_range(0)) { + val line1 = buffer.getLineOfOffset(model.to_current(document, start)) + val line2 = buffer.getLineOfOffset(model.to_current(document, start + command.length)) + 1 + val y = line_to_y(line1) + val height = HEIGHT * (line2 - line1) + gfx.setColor(Document_View.choose_color(command, document)) + gfx.fillRect(0, y, getWidth - 1, height) + } + } + + private def line_to_y(line: Int): Int = + (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines) + + private def y_to_line(y: Int): Int = + (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight + } + + + /* activation */ + + private def activate() + { + text_area.getPainter. + addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension) + text_area.addCaretListener(caret_listener) + text_area.addLeftOfScrollBar(overview) + session.command_change += command_change_actor + } + + private def deactivate() + { + session.command_change -= command_change_actor + command_change_actor !? Exit + text_area.removeLeftOfScrollBar(overview) + text_area.removeCaretListener(caret_listener) + text_area.getPainter.removeExtension(text_area_extension) + } +} \ No newline at end of file diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/src/jedit/isabelle_encoding.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/jedit/isabelle_encoding.scala Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,64 @@ +/* + * Isabelle encoding -- based on utf-8 + * + * @author Makarius + */ + +package isabelle.jedit + + +import org.gjt.sp.jedit.io.Encoding +import org.gjt.sp.jedit.buffer.JEditBuffer + +import java.nio.charset.{Charset, CharsetDecoder, CodingErrorAction} +import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter, + CharArrayReader, ByteArrayOutputStream} + +import scala.io.{Source, BufferedSource} + + +object Isabelle_Encoding +{ + val NAME = "UTF-8-Isabelle" + + def is_active(buffer: JEditBuffer): Boolean = + buffer.getStringProperty(JEditBuffer.ENCODING).asInstanceOf[String] == NAME +} + +class Isabelle_Encoding extends Encoding +{ + private val charset = Charset.forName(Standard_System.charset) + private val BUFSIZE = 32768 + + private def text_reader(in: InputStream, decoder: CharsetDecoder): Reader = + { + def source(): Source = + BufferedSource.fromInputStream(in, decoder, BUFSIZE, { () => source() }) + new CharArrayReader(Isabelle.system.symbols.decode(source.mkString).toArray) + } + + override def getTextReader(in: InputStream): Reader = + text_reader(in, charset.newDecoder()) + + override def getPermissiveTextReader(in: InputStream): Reader = + { + val decoder = charset.newDecoder() + decoder.onMalformedInput(CodingErrorAction.REPLACE) + decoder.onUnmappableCharacter(CodingErrorAction.REPLACE) + text_reader(in, decoder) + } + + override def getTextWriter(out: OutputStream): Writer = + { + val buffer = new ByteArrayOutputStream(BUFSIZE) { + override def flush() + { + val text = Isabelle.system.symbols.encode(toString(Standard_System.charset)) + out.write(text.getBytes(Standard_System.charset)) + out.flush() + } + override def close() { out.close() } + } + new OutputStreamWriter(buffer, charset.newEncoder()) + } +} diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,76 @@ +/* + * Hyperlink setup for Isabelle proof documents + * + * @author Fabian Immler, TU Munich + */ + +package isabelle.jedit + +import isabelle.proofdocument.Command + +import java.io.File + +import gatchan.jedit.hyperlinks.{Hyperlink, HyperlinkSource, AbstractHyperlink} + +import org.gjt.sp.jedit.{View, jEdit, Buffer, TextUtilities} + + +private class Internal_Hyperlink(start: Int, end: Int, line: Int, ref_offset: Int) + extends AbstractHyperlink(start, end, line, "") +{ + override def click(view: View) { + view.getTextArea.moveCaretPosition(ref_offset) + } +} + +class External_Hyperlink(start: Int, end: Int, line: Int, ref_file: String, ref_line: Int) + extends AbstractHyperlink(start, end, line, "") +{ + override def click(view: View) = { + Isabelle.system.source_file(ref_file) match { + case None => System.err.println("Could not find source file " + ref_file) // FIXME ?? + case Some(file) => + jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line)) + } + } +} + +class Isabelle_Hyperlinks extends HyperlinkSource +{ + def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink = + { + Document_Model(buffer) match { + case Some(model) => + val document = model.recent_document() + val offset = model.from_current(document, original_offset) + document.command_at(offset) match { + case Some((command, command_start)) => + document.current_state(command).get.ref_at(offset - command_start) match { + case Some(ref) => + val begin = model.to_current(document, command_start + ref.start) + val line = buffer.getLineOfOffset(begin) + val end = model.to_current(document, command_start + ref.stop) + ref.info match { + case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) => + new External_Hyperlink(begin, end, line, ref_file, ref_line) + case Command.RefInfo(_, _, Some(id), Some(offset)) => + Isabelle.session.lookup_entity(id) match { + case Some(ref_cmd: Command) => + document.command_start(ref_cmd) match { + case Some(ref_cmd_start) => + new Internal_Hyperlink(begin, end, line, + model.to_current(document, ref_cmd_start + offset - 1)) + case None => null // FIXME external ref + } + case _ => null + } + case _ => null + } + case None => null + } + case None => null + } + case None => null + } + } +} diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/src/jedit/isabelle_options.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/jedit/isabelle_options.scala Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,53 @@ +/* + * Editor pane for plugin options + * + * @author Johannes Hölzl, TU Munich + */ + +package isabelle.jedit + + +import javax.swing.{JComboBox, JSpinner} + +import org.gjt.sp.jedit.AbstractOptionPane + + +class Isabelle_Options extends AbstractOptionPane("isabelle") +{ + private val logic_name = new JComboBox() + private val font_size = new JSpinner() + + private class List_Item(val name: String, val descr: String) { + def this(name: String) = this(name, name) + override def toString = descr + } + + override def _init() + { + val logic = Isabelle.Property("logic") + addComponent(Isabelle.Property("logic.title"), { + logic_name.addItem(new List_Item("", "default (" + Isabelle.default_logic() + ")")) + for (name <- Isabelle.system.find_logics()) { + val item = new List_Item(name) + logic_name.addItem(item) + if (name == logic) + logic_name.setSelectedItem(item) + } + logic_name + }) + + addComponent(Isabelle.Property("font-size.title"), { + font_size.setValue(Isabelle.Int_Property("font-size")) + font_size + }) + } + + override def _save() + { + val logic = logic_name.getSelectedItem.asInstanceOf[List_Item].name + Isabelle.Property("logic") = logic + + val size = font_size.getValue().asInstanceOf[Int] + Isabelle.Int_Property("font-size") = size + } +} diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,100 @@ +/* + * SideKick parser for Isabelle proof documents + * + * @author Fabian Immler, TU Munich + * @author Makarius + */ + +package isabelle.jedit + + +import scala.collection.Set +import scala.collection.immutable.TreeSet + +import javax.swing.tree.DefaultMutableTreeNode +import javax.swing.text.Position +import javax.swing.Icon + +import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View} +import errorlist.DefaultErrorSource +import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset} + +import isabelle.proofdocument.{Command, Markup_Node, Document} + + +class Isabelle_Sidekick extends SideKickParser("isabelle") +{ + /* parsing */ + + @volatile private var stopped = false + override def stop() = { stopped = true } + + def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData = + { + implicit def int_to_pos(offset: Int): Position = + new Position { def getOffset = offset; override def toString = offset.toString } + + stopped = false + + // FIXME lock buffer !?? + val data = new SideKickParsedData(buffer.getName) + val root = data.root + data.getAsset(root).setEnd(buffer.getLength) + + Swing_Thread.now { Document_Model(buffer) } match { + case Some(model) => + val document = model.recent_document() + for ((command, command_start) <- document.command_range(0) if !stopped) { + root.add(document.current_state(command).get.markup_root.swing_tree((node: Markup_Node) => + { + val content = command.source(node.start, node.stop) + val id = command.id + + new DefaultMutableTreeNode(new IAsset { + override def getIcon: Icon = null + override def getShortString: String = content + override def getLongString: String = node.info.toString + override def getName: String = id + override def setName(name: String) = () + override def setStart(start: Position) = () + override def getStart: Position = command_start + node.start + override def setEnd(end: Position) = () + override def getEnd: Position = command_start + node.stop + override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]" + }) + })) + } + if (stopped) root.add(new DefaultMutableTreeNode("")) + case None => root.add(new DefaultMutableTreeNode("")) + } + data + } + + + /* completion */ + + override def supportsCompletion = true + override def canCompleteAnywhere = true + + override def complete(pane: EditPane, caret: Int): SideKickCompletion = + { + val buffer = pane.getBuffer + + val line = buffer.getLineOfOffset(caret) + val start = buffer.getLineStartOffset(line) + val text = buffer.getSegment(start, caret - start) + + val completion = Isabelle.session.current_syntax.completion + + completion.complete(text) match { + case None => null + case Some((word, cs)) => + val ds = + if (Isabelle_Encoding.is_active(buffer)) + cs.map(Isabelle.system.symbols.decode(_)).sort(_ < _) + else cs + new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { } + } + } + +} diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/src/jedit/isabelle_token_marker.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,145 @@ +/* + * include isabelle's command- and keyword-declarations + * live in jEdits syntax-highlighting + * + * @author Fabian Immler, TU Munich + */ + +package isabelle.jedit + + +import isabelle.Markup + +import org.gjt.sp.jedit.buffer.JEditBuffer +import org.gjt.sp.jedit.syntax.{Token, TokenMarker, TokenHandler, SyntaxStyle, ParserRuleSet} + +import java.awt.Color +import java.awt.Font +import javax.swing.text.Segment; + + +object Isabelle_Token_Marker +{ + /* line context */ + + private val rule_set = new ParserRuleSet("isabelle", "MAIN") + private class LineContext(val line: Int, prev: LineContext) + extends TokenMarker.LineContext(rule_set, prev) + + + /* mapping to jEdit token types */ + // TODO: as properties or CSS style sheet + + private val choose_byte: Map[String, Byte] = + { + import Token._ + Map[String, Byte]( + // logical entities + Markup.TCLASS -> LABEL, + Markup.TYCON -> LABEL, + Markup.FIXED_DECL -> LABEL, + Markup.FIXED -> LABEL, + Markup.CONST_DECL -> LABEL, + Markup.CONST -> LABEL, + Markup.FACT_DECL -> LABEL, + Markup.FACT -> LABEL, + Markup.DYNAMIC_FACT -> LABEL, + Markup.LOCAL_FACT_DECL -> LABEL, + Markup.LOCAL_FACT -> LABEL, + // inner syntax + Markup.TFREE -> LITERAL2, + Markup.FREE -> LITERAL2, + Markup.TVAR -> LITERAL3, + Markup.SKOLEM -> LITERAL3, + Markup.BOUND -> LITERAL3, + Markup.VAR -> LITERAL3, + Markup.NUM -> DIGIT, + Markup.FLOAT -> DIGIT, + Markup.XNUM -> DIGIT, + Markup.XSTR -> LITERAL4, + Markup.LITERAL -> LITERAL4, + Markup.INNER_COMMENT -> COMMENT1, + Markup.SORT -> FUNCTION, + Markup.TYP -> FUNCTION, + Markup.TERM -> FUNCTION, + Markup.PROP -> FUNCTION, + Markup.ATTRIBUTE -> FUNCTION, + Markup.METHOD -> FUNCTION, + // ML syntax + Markup.ML_KEYWORD -> KEYWORD2, + Markup.ML_IDENT -> NULL, + Markup.ML_TVAR -> LITERAL3, + Markup.ML_NUMERAL -> DIGIT, + Markup.ML_CHAR -> LITERAL1, + Markup.ML_STRING -> LITERAL1, + Markup.ML_COMMENT -> COMMENT1, + Markup.ML_MALFORMED -> INVALID, + // embedded source text + Markup.ML_SOURCE -> COMMENT4, + Markup.DOC_SOURCE -> COMMENT4, + Markup.ANTIQ -> COMMENT4, + Markup.ML_ANTIQ -> COMMENT4, + Markup.DOC_ANTIQ -> COMMENT4, + // outer syntax + Markup.IDENT -> NULL, + Markup.COMMAND -> OPERATOR, + Markup.KEYWORD -> KEYWORD4, + Markup.VERBATIM -> COMMENT3, + Markup.COMMENT -> COMMENT1, + Markup.CONTROL -> COMMENT3, + Markup.MALFORMED -> INVALID, + Markup.STRING -> LITERAL3, + Markup.ALTSTRING -> LITERAL1 + ).withDefaultValue(NULL) + } + + def choose_color(kind: String, styles: Array[SyntaxStyle]): Color = + styles(choose_byte(kind)).getForegroundColor +} + + +class Isabelle_Token_Marker(model: Document_Model) extends TokenMarker +{ + override def markTokens(prev: TokenMarker.LineContext, + handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext = + { + val previous = prev.asInstanceOf[Isabelle_Token_Marker.LineContext] + val line = if (prev == null) 0 else previous.line + 1 + val context = new Isabelle_Token_Marker.LineContext(line, previous) + val start = model.buffer.getLineStartOffset(line) + val stop = start + line_segment.count + + val document = model.recent_document() + def to: Int => Int = model.to_current(document, _) + def from: Int => Int = model.from_current(document, _) + + var next_x = start + for { + (command, command_start) <- document.command_range(from(start), from(stop)) + markup <- document.current_state(command).get.highlight.flatten + val abs_start = to(command_start + markup.start) + val abs_stop = to(command_start + markup.stop) + if (abs_stop > start) + if (abs_start < stop) + val byte = Isabelle_Token_Marker.choose_byte(markup.info.toString) + val token_start = (abs_start - start) max 0 + val token_length = + (abs_stop - abs_start) - + ((start - abs_start) max 0) - + ((abs_stop - stop) max 0) + } + { + if (start + token_start > next_x) + handler.handleToken(line_segment, 1, + next_x - start, start + token_start - next_x, context) + handler.handleToken(line_segment, byte, token_start, token_length, context) + next_x = start + token_start + token_length + } + if (next_x < stop) + handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context) + + handler.handleToken(line_segment, Token.END, line_segment.count, 0, context) + handler.setLineContext(context) + context + } +} diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/src/jedit/output_dockable.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,66 @@ +/* + * Dockable window with result message output + * + * @author Makarius + */ + +package isabelle.jedit + + +import isabelle.proofdocument.{Command, HTML_Panel, Session} + +import scala.actors.Actor._ + +import javax.swing.JPanel +import java.awt.{BorderLayout, Dimension} + +import org.gjt.sp.jedit.View +import org.gjt.sp.jedit.gui.DockableWindowManager + + + +class Output_Dockable(view: View, position: String) extends JPanel(new BorderLayout) +{ + if (position == DockableWindowManager.FLOATING) + setPreferredSize(new Dimension(500, 250)) + + private val html_panel = + new HTML_Panel(Isabelle.system, Isabelle.Int_Property("font-size"), null) + add(html_panel, BorderLayout.CENTER) + + + /* actor wiring */ + + private val output_actor = actor { + loop { + react { + case cmd: Command => + Swing_Thread.now { Document_Model(view.getBuffer) } match { + case None => + case Some(model) => + val body = model.recent_document.current_state(cmd).map(_.results) getOrElse Nil + html_panel.render(body) + } + + case Session.Global_Settings => + html_panel.init(Isabelle.Int_Property("font-size")) + + case bad => System.err.println("output_actor: ignoring bad message " + bad) + } + } + } + + override def addNotify() + { + super.addNotify() + Isabelle.session.results += output_actor + Isabelle.session.global_settings += output_actor + } + + override def removeNotify() + { + Isabelle.session.results -= output_actor + Isabelle.session.global_settings -= output_actor + super.removeNotify() + } +} diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/src/jedit/plugin.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/jedit/plugin.scala Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,197 @@ +/* + * Main Isabelle/jEdit plugin setup + * + * @author Johannes Hölzl, TU Munich + * @author Fabian Immler, TU Munich + * @author Makarius + */ + +package isabelle.jedit + + +import isabelle.proofdocument.Session + +import java.io.{FileInputStream, IOException} +import java.awt.Font +import javax.swing.JTextArea + +import scala.collection.mutable + +import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View} +import org.gjt.sp.jedit.buffer.JEditBuffer +import org.gjt.sp.jedit.textarea.JEditTextArea +import org.gjt.sp.jedit.msg.{EditPaneUpdate, PropertiesChanged} + + +object Isabelle +{ + /* plugin instance */ + + var system: Isabelle_System = null + var session: Session = null + + + /* name */ + + val NAME = "Isabelle" + + + /* properties */ + + val OPTION_PREFIX = "options.isabelle." + + object Property + { + def apply(name: String): String = jEdit.getProperty(OPTION_PREFIX + name) + def update(name: String, value: String) = jEdit.setProperty(OPTION_PREFIX + name, value) + } + + object Boolean_Property + { + def apply(name: String): Boolean = jEdit.getBooleanProperty(OPTION_PREFIX + name) + def update(name: String, value: Boolean) = jEdit.setBooleanProperty(OPTION_PREFIX + name, value) + } + + object Int_Property + { + def apply(name: String): Int = jEdit.getIntegerProperty(OPTION_PREFIX + name) + def update(name: String, value: Int) = jEdit.setIntegerProperty(OPTION_PREFIX + name, value) + } + + + /* settings */ + + def default_logic(): String = + { + val logic = system.getenv("JEDIT_LOGIC") + if (logic != "") logic + else system.getenv_strict("ISABELLE_LOGIC") + } + + def isabelle_args(): List[String] = + { + val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _) + val logic = { + val logic = Property("logic") + if (logic != null && logic != "") logic + else default_logic() + } + modes ++ List(logic) + } + + + /* main jEdit components */ // FIXME ownership!? + + def jedit_buffers(): Iterator[Buffer] = Iterator.fromArray(jEdit.getBuffers()) + + def jedit_views(): Iterator[View] = Iterator.fromArray(jEdit.getViews()) + + def jedit_text_areas(view: View): Iterator[JEditTextArea] = + Iterator.fromArray(view.getEditPanes).map(_.getTextArea) + + def jedit_text_areas(): Iterator[JEditTextArea] = + jedit_views().flatMap(jedit_text_areas(_)) + + def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] = + jedit_text_areas().filter(_.getBuffer == buffer) + + + /* manage prover */ + + private def prover_started(view: View): Boolean = + { + val timeout = Int_Property("startup-timeout") max 1000 + session.start(timeout, Isabelle.isabelle_args()) match { + case Some(err) => + val text = new JTextArea(err); text.setEditable(false) + Library.error_dialog(view, null, "Failed to start Isabelle process", text) + false + case None => true + } + } + + + /* activation */ + + def activate_buffer(view: View, buffer: Buffer) + { + if (prover_started(view)) { + val model = Document_Model.init(session, buffer) + for (text_area <- jedit_text_areas(buffer)) + Document_View.init(model, text_area) + } + } + + def deactivate_buffer(buffer: Buffer) + { + session.stop() // FIXME not yet + + for (text_area <- jedit_text_areas(buffer)) + Document_View.exit(text_area) + Document_Model.exit(buffer) + } + + def switch_active(view: View) = + { + val buffer = view.getBuffer + if (Document_Model(buffer).isDefined) deactivate_buffer(buffer) + else activate_buffer(view, buffer) + } + + def is_active(view: View): Boolean = + Document_Model(view.getBuffer).isDefined +} + + +class Plugin extends EBPlugin +{ + /* main plugin plumbing */ + + override def handleMessage(message: EBMessage) + { + message match { + case msg: EditPaneUpdate => + val edit_pane = msg.getEditPane + val buffer = edit_pane.getBuffer + val text_area = edit_pane.getTextArea + + def init_view() + { + Document_Model(buffer) match { + case Some(model) => Document_View.init(model, text_area) + case None => + } + } + def exit_view() + { + if (Document_View(text_area).isDefined) + Document_View.exit(text_area) + } + msg.getWhat match { + case EditPaneUpdate.BUFFER_CHANGED => exit_view(); init_view() + case EditPaneUpdate.CREATED => init_view() + case EditPaneUpdate.DESTROYED => exit_view() + case _ => + } + + case msg: PropertiesChanged => + Isabelle.session.global_settings.event(Session.Global_Settings) + + case _ => + } + } + + override def start() + { + Isabelle.system = new Isabelle_System + Isabelle.system.install_fonts() + Isabelle.session = new Session(Isabelle.system) // FIXME dialog!? + } + + override def stop() + { + Isabelle.session.stop() // FIXME dialog!? + Isabelle.session = null + Isabelle.system = null + } +} diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/src/jedit/protocol_dockable.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/jedit/protocol_dockable.scala Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,52 @@ +/* + * Dockable window for raw process output + * + * @author Makarius + */ + +package isabelle.jedit + + +import scala.actors.Actor._ + +import java.awt.{Dimension, Graphics, BorderLayout} +import javax.swing.{JPanel, JTextArea, JScrollPane} + +import org.gjt.sp.jedit.View +import org.gjt.sp.jedit.gui.DockableWindowManager + + +class Protocol_Dockable(view: View, position: String) extends JPanel(new BorderLayout) +{ + if (position == DockableWindowManager.FLOATING) + setPreferredSize(new Dimension(500, 250)) + + private val text_area = new JTextArea + add(new JScrollPane(text_area), BorderLayout.CENTER) + + + /* actor wiring */ + + private val raw_actor = actor { + loop { + react { + case result: Isabelle_Process.Result => + Swing_Thread.now { text_area.append(result.toString + "\n") } + + case bad => System.err.println("raw_actor: ignoring bad message " + bad) + } + } + } + + override def addNotify() + { + super.addNotify() + Isabelle.session.raw_results += raw_actor + } + + override def removeNotify() + { + Isabelle.session.raw_results -= raw_actor + super.removeNotify() + } +} diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/src/jedit/scala_console.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/jedit/scala_console.scala Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,153 @@ +/* + * Scala instance of Console plugin + * + * @author Makarius + */ + +package isabelle.jedit + + +import console.{Console, ConsolePane, Shell, Output} + +import org.gjt.sp.jedit.{jEdit, JARClassLoader} +import org.gjt.sp.jedit.MiscUtilities + +import java.io.{File, OutputStream, Writer, PrintWriter} + +import scala.tools.nsc.{Interpreter, GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter} +import scala.collection.mutable + + +class Scala_Console extends Shell("Scala") +{ + /* reconstructed jEdit/plugin classpath */ + + private def reconstruct_classpath(): String = + { + def find_jars(start: String): List[String] = + if (start != null) + Standard_System.find_files(new File(start), + entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath) + else Nil + val path = find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome) + path.mkString(File.pathSeparator) + } + + + /* global state -- owned by Swing thread */ + + private var interpreters = Map[Console, Interpreter]() + + private var global_console: Console = null + private var global_out: Output = null + private var global_err: Output = null + + private val console_stream = new OutputStream + { + val buf = new StringBuilder + override def flush() + { + val str = Standard_System.decode_permissive_utf8(buf.toString) + buf.clear + if (global_out == null) System.out.print(str) + else Swing_Thread.now { global_out.writeAttrs(null, str) } + } + override def close() { flush () } + def write(byte: Int) { buf.append(byte.toChar) } + } + + private val console_writer = new Writer + { + def flush() {} + def close() {} + + def write(cbuf: Array[Char], off: Int, len: Int) + { + if (len > 0) write(new String(cbuf.subArray(off, off + len))) + } + + override def write(str: String) + { + if (global_out == null) System.out.println(str) + else global_out.print(null, str) + } + } + + private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A = + { + global_console = console + global_out = out + global_err = if (err == null) out else err + val res = Exn.capture { scala.Console.withOut(console_stream)(e) } + console_stream.flush + global_console = null + global_out = null + global_err = null + Exn.release(res) + } + + private def report_error(str: String) + { + if (global_console == null || global_err == null) System.err.println(str) + else Swing_Thread.now { global_err.print(global_console.getErrorColor, str) } + } + + + /* jEdit console methods */ + + override def openConsole(console: Console) + { + val settings = new GenericRunnerSettings(report_error) + settings.classpath.value = reconstruct_classpath() + + val interp = new Interpreter(settings, new PrintWriter(console_writer, true)) + { + override def parentClassLoader = new JARClassLoader + } + interp.setContextClassLoader + interp.bind("view", "org.gjt.sp.jedit.View", console.getView) + interp.bind("console", "console.Console", console) + interp.interpret("import isabelle.jedit.Isabelle") + + interpreters += (console -> interp) + } + + override def closeConsole(console: Console) + { + interpreters -= console + } + + override def printInfoMessage(out: Output) + { + out.print(null, + "This shell evaluates Isabelle/Scala expressions.\n\n" + + "The following special toplevel bindings are provided:\n" + + " view -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" + + " console -- jEdit Console plugin instance\n" + + " Isabelle -- Isabelle plugin instance (e.g. Isabelle.system, Isabelle.session)\n") + } + + override def printPrompt(console: Console, out: Output) + { + out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>") + out.writeAttrs(ConsolePane.colorAttributes(console.getPlainColor), " ") + } + + override def execute(console: Console, input: String, out: Output, err: Output, command: String) + { + val interp = interpreters(console) + with_console(console, out, err) { interp.interpret(command) } + if (err != null) err.commandDone() + out.commandDone() + } + + override def stop(console: Console) + { + closeConsole(console) + console.clear + openConsole(console) + val out = console.getOutput + out.commandDone + printPrompt(console, out) + } +} diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/src/proofdocument/change.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/proofdocument/change.scala Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,42 @@ +/* + * Changes of plain text + * + * @author Fabian Immler, TU Munich + * @author Makarius + */ + +package isabelle.proofdocument + + +class Change( + val id: Isar_Document.Document_ID, + val parent: Option[Change], + val edits: List[Text_Edit], + val result: Future[(List[Document.Edit], Document)]) +{ + def ancestors: Iterator[Change] = new Iterator[Change] + { + private var state: Option[Change] = Some(Change.this) + def hasNext = state.isDefined + def next = + state match { + case Some(change) => state = change.parent; change + case None => throw new NoSuchElementException("next on empty iterator") + } + } + + def join_document: Document = result.join._2 + def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished + + def edit(session: Session, edits: List[Text_Edit]): Change = + { + val new_id = session.create_id() + val result: Future[(List[Document.Edit], Document)] = + Future.fork { + val old_doc = join_document + old_doc.await_assignment + Document.text_edits(session, old_doc, new_id, edits) + } + new Change(new_id, Some(this), edits, result) + } +} \ No newline at end of file diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/src/proofdocument/command.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/proofdocument/command.scala Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,102 @@ +/* + * Prover commands with semantic state + * + * @author Johannes Hölzl, TU Munich + * @author Fabian Immler, TU Munich + */ + +package isabelle.proofdocument + + +import scala.actors.Actor, Actor._ +import scala.collection.mutable + +import isabelle.jedit.Isabelle + + +object Command +{ + object Status extends Enumeration + { + val UNPROCESSED = Value("UNPROCESSED") + val FINISHED = Value("FINISHED") + val FAILED = Value("FAILED") + } + + case class HighlightInfo(highlight: String) { override def toString = highlight } + case class TypeInfo(ty: String) + case class RefInfo(file: Option[String], line: Option[Int], + command_id: Option[String], offset: Option[Int]) +} + + +class Command( + val id: Isar_Document.Command_ID, + val span: Thy_Syntax.Span) + extends Session.Entity +{ + /* classification */ + + def is_command: Boolean = !span.isEmpty && span.first.is_command + def is_ignored: Boolean = span.forall(_.is_ignored) + def is_malformed: Boolean = !is_command && !is_ignored + + def name: String = if (is_command) span.first.content else "" + override def toString = if (is_command) name else if (is_ignored) "" else "" + + + /* source text */ + + val source: String = span.map(_.source).mkString + def source(i: Int, j: Int): String = source.substring(i, j) + def length: Int = source.length + + lazy val symbol_index = new Symbol.Index(source) + + + /* accumulated messages */ + + @volatile protected var state = new State(this) + def current_state: State = state + + private case class Consume(session: Session, message: XML.Tree) + private case object Assign + + private val accumulator = actor { + var assigned = false + loop { + react { + case Consume(session: Session, message: XML.Tree) if !assigned => + state = state.+(session, message) + + case Assign => + assigned = true // single assignment + reply(()) + + case bad => System.err.println("command accumulator: ignoring bad message " + bad) + } + } + } + + def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) } + + def assign_state(state_id: Isar_Document.State_ID): Command = + { + val cmd = new Command(state_id, span) + accumulator !? Assign + cmd.state = current_state + cmd + } + + + /* markup */ + + lazy val empty_markup = new Markup_Text(Nil, source) + + def markup_node(begin: Int, end: Int, info: Any): Markup_Tree = + { + val start = symbol_index.decode(begin) + val stop = symbol_index.decode(end) + new Markup_Tree(new Markup_Node(start, stop, info), Nil) + } +} diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/src/proofdocument/document.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/proofdocument/document.scala Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,197 @@ +/* + * Document as editable list of commands + * + * @author Makarius + */ + +package isabelle.proofdocument + + +object Document +{ + /* command start positions */ + + def command_starts(commands: Linear_Set[Command]): Iterator[(Command, Int)] = + { + var offset = 0 + for (cmd <- commands.elements) yield { + val start = offset + offset += cmd.length + (cmd, start) + } + } + + + /* empty document */ + + def empty(id: Isar_Document.Document_ID): Document = + { + val doc = new Document(id, Linear_Set(), Map()) + doc.assign_states(Nil) + doc + } + + + // FIXME + var phase0: List[Text_Edit] = null + var phase1: Linear_Set[Command] = null + var phase2: Linear_Set[Command] = null + var phase3: List[Edit] = null + + + + /** document edits **/ + + type Edit = (Option[Command], Option[Command]) + + def text_edits(session: Session, old_doc: Document, new_id: Isar_Document.Document_ID, + edits: List[Text_Edit]): (List[Edit], Document) = + { + require(old_doc.assignment.is_finished) + + + /* unparsed dummy commands */ + + def unparsed(source: String) = + new Command(null, List(Outer_Lex.Token(Outer_Lex.Token_Kind.UNPARSED, source))) + + def is_unparsed(command: Command) = command.id == null + + assert(!old_doc.commands.exists(is_unparsed)) // FIXME remove + + + /* phase 1: edit individual command source */ + + def edit_text(eds: List[Text_Edit], commands: Linear_Set[Command]): Linear_Set[Command] = + { + eds match { + case e :: es => + command_starts(commands).find { // FIXME relative search! + case (cmd, cmd_start) => + e.can_edit(cmd.source, cmd_start) || e.is_insert && e.start == cmd_start + cmd.length + } match { + case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) => + val (rest, text) = e.edit(cmd.source, cmd_start) + val new_commands = commands.insert_after(Some(cmd), unparsed(text)) - cmd + edit_text(rest.toList ::: es, new_commands) + + case Some((cmd, cmd_start)) => + edit_text(es, commands.insert_after(Some(cmd), unparsed(e.text))) + + case None => + require(e.is_insert && e.start == 0) + edit_text(es, commands.insert_after(None, unparsed(e.text))) + } + case Nil => commands + } + } + + + /* phase 2: recover command spans */ + + def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] = + { + // FIXME relative search! + commands.elements.find(is_unparsed) match { + case Some(first_unparsed) => + val prefix = commands.prev(first_unparsed) + val body = commands.elements(first_unparsed).takeWhile(is_unparsed).toList + val suffix = commands.next(body.last) + + val sources = (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source)) + val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString)) + + val (before_edit, spans1) = + if (!spans0.isEmpty && Some(spans0.first) == prefix.map(_.span)) + (prefix, spans0.tail) + else (if (prefix.isDefined) commands.prev(prefix.get) else None, spans0) + + val (after_edit, spans2) = + if (!spans1.isEmpty && Some(spans1.last) == suffix.map(_.span)) + (suffix, spans1.take(spans1.length - 1)) + else (if (suffix.isDefined) commands.next(suffix.get) else None, spans1) + + val inserted = spans2.map(span => new Command(session.create_id(), span)) + val new_commands = + commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted) + parse_spans(new_commands) + + case None => commands + } + } + + + /* phase 3: resulting document edits */ + + val result = Library.timeit("text_edits") { + val commands0 = old_doc.commands + val commands1 = Library.timeit("edit_text") { edit_text(edits, commands0) } + val commands2 = Library.timeit("parse_spans") { parse_spans(commands1) } + + val removed_commands = commands0.elements.filter(!commands2.contains(_)).toList + val inserted_commands = commands2.elements.filter(!commands0.contains(_)).toList + + val doc_edits = + removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) ::: + inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd))) + + val former_states = old_doc.assignment.join -- removed_commands + + phase0 = edits + phase1 = commands1 + phase2 = commands2 + phase3 = doc_edits + + (doc_edits, new Document(new_id, commands2, former_states)) + } + result + } +} + + +class Document( + val id: Isar_Document.Document_ID, + val commands: Linear_Set[Command], + former_states: Map[Command, Command]) +{ + /* command ranges */ + + def command_starts: Iterator[(Command, Int)] = Document.command_starts(commands) + + def command_start(cmd: Command): Option[Int] = + command_starts.find(_._1 == cmd).map(_._2) + + def command_range(i: Int): Iterator[(Command, Int)] = + command_starts dropWhile { case (cmd, start) => start + cmd.length <= i } + + def command_range(i: Int, j: Int): Iterator[(Command, Int)] = + command_range(i) takeWhile { case (_, start) => start < j } + + def command_at(i: Int): Option[(Command, Int)] = + { + val range = command_range(i) + if (range.hasNext) Some(range.next) else None + } + + + /* command state assignment */ + + val assignment = Future.promise[Map[Command, Command]] + def await_assignment { assignment.join } + + @volatile private var tmp_states = former_states + private val time0 = System.currentTimeMillis + + def assign_states(new_states: List[(Command, Command)]) + { + assignment.fulfill(tmp_states ++ new_states) + tmp_states = Map() + System.err.println("assign_states: " + (System.currentTimeMillis - time0) + " ms elapsed time") + } + + def current_state(cmd: Command): Option[State] = + { + require(assignment.is_finished) + (assignment.join).get(cmd).map(_.current_state) + } +} diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/src/proofdocument/html_panel.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/proofdocument/html_panel.scala Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,140 @@ +/* + * HTML panel based on Lobo/Cobra + * + * @author Makarius + */ + +package isabelle.proofdocument + + +import java.io.StringReader +import java.awt.{BorderLayout, Dimension} +import java.awt.event.MouseEvent + +import javax.swing.{JButton, JPanel, JScrollPane} +import java.util.logging.{Logger, Level} + +import org.w3c.dom.html2.HTMLElement + +import org.lobobrowser.html.parser.{DocumentBuilderImpl, InputSourceImpl} +import org.lobobrowser.html.gui.HtmlPanel +import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl} +import org.lobobrowser.html.test.{SimpleHtmlRendererContext, SimpleUserAgentContext} + +import scala.io.Source +import scala.actors.Actor._ + + +object HTML_Panel +{ + sealed abstract class Event { val element: HTMLElement; val mouse: MouseEvent } + case class Context_Menu(val element: HTMLElement, mouse: MouseEvent) extends Event + case class Mouse_Click(val element: HTMLElement, mouse: MouseEvent) extends Event + case class Double_Click(val element: HTMLElement, mouse: MouseEvent) extends Event + case class Mouse_Over(val element: HTMLElement, mouse: MouseEvent) extends Event + case class Mouse_Out(val element: HTMLElement, mouse: MouseEvent) extends Event +} + + +class HTML_Panel( + sys: Isabelle_System, + initial_font_size: Int, + handler: PartialFunction[HTML_Panel.Event, Unit]) extends HtmlPanel +{ + // global logging + Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING) + + + /* document template */ + + private def try_file(name: String): String = + { + val file = sys.platform_file(name) + if (file.isFile) Source.fromFile(file).mkString else "" + } + + private def template(font_size: Int): String = + """ + + + + + + + +""" + + + /* actor with local state */ + + private val ucontext = new SimpleUserAgentContext + + private val rcontext = new SimpleHtmlRendererContext(this, ucontext) + { + private def handle(event: HTML_Panel.Event): Boolean = + if (handler != null && handler.isDefinedAt(event)) { handler(event); true } + else false + + override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean = + handle(HTML_Panel.Context_Menu(elem, event)) + override def onMouseClick(elem: HTMLElement, event: MouseEvent): Boolean = + handle(HTML_Panel.Mouse_Click(elem, event)) + override def onDoubleClick(elem: HTMLElement, event: MouseEvent): Boolean = + handle(HTML_Panel.Double_Click(elem, event)) + override def onMouseOver(elem: HTMLElement, event: MouseEvent) + { handle(HTML_Panel.Mouse_Over(elem, event)) } + override def onMouseOut(elem: HTMLElement, event: MouseEvent) + { handle(HTML_Panel.Mouse_Out(elem, event)) } + } + + private val builder = new DocumentBuilderImpl(ucontext, rcontext) + + private case class Init(font_size: Int) + private case class Render(body: List[XML.Tree]) + + private val main_actor = actor { + // crude double buffering + var doc1: org.w3c.dom.Document = null + var doc2: org.w3c.dom.Document = null + + loop { + react { + case Init(font_size) => + val src = template(font_size) + def parse() = + builder.parse(new InputSourceImpl(new StringReader(src), "http://localhost")) + doc1 = parse() + doc2 = parse() + Swing_Thread.now { setDocument(doc1, rcontext) } + + case Render(body) => + val doc = doc2 + val node = + XML.document_node(doc, + XML.elem(HTML.BODY, body.map((t: XML.Tree) => XML.elem(HTML.PRE, HTML.spans(t))))) + doc.removeChild(doc.getLastChild()) + doc.appendChild(node) + doc2 = doc1 + doc1 = doc + Swing_Thread.now { setDocument(doc1, rcontext) } + + case bad => System.err.println("main_actor: ignoring bad message " + bad) + } + } + } + + main_actor ! Init(initial_font_size) + + + /* main method wrappers */ + + def init(font_size: Int) { main_actor ! Init(font_size) } + def render(body: List[XML.Tree]) { main_actor ! Render(body) } +} diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/src/proofdocument/markup_node.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/proofdocument/markup_node.scala Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,111 @@ +/* + * Document markup nodes, with connection to Swing tree model + * + * @author Fabian Immler, TU Munich + * @author Makarius + */ + +package isabelle.proofdocument + + +import javax.swing.tree.DefaultMutableTreeNode + + + +class Markup_Node(val start: Int, val stop: Int, val info: Any) +{ + def fits_into(that: Markup_Node): Boolean = + that.start <= this.start && this.stop <= that.stop +} + + +class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree]) +{ + def set_branches(bs: List[Markup_Tree]): Markup_Tree = new Markup_Tree(node, bs) + + private def add(branch: Markup_Tree) = // FIXME avoid sort + set_branches((branch :: branches) sort ((a, b) => a.node.start < b.node.start)) + + private def remove(bs: List[Markup_Tree]) = set_branches(branches -- bs) + + def + (new_tree: Markup_Tree): Markup_Tree = + { + val new_node = new_tree.node + if (new_node fits_into node) { + var inserted = false + val new_branches = + branches.map(branch => + if ((new_node fits_into branch.node) && !inserted) { + inserted = true + branch + new_tree + } + else branch) + if (!inserted) { + // new_tree did not fit into children of this + // -> insert between this and its branches + val fitting = branches filter(_.node fits_into new_node) + (this remove fitting) add ((new_tree /: fitting)(_ + _)) + } + else set_branches(new_branches) + } + else { + System.err.println("ignored nonfitting markup: " + new_node) + this + } + } + + def flatten: List[Markup_Node] = + { + var next_x = node.start + if (branches.isEmpty) List(this.node) + else { + val filled_gaps = + for { + child <- branches + markups = + if (next_x < child.node.start) + new Markup_Node(next_x, child.node.start, node.info) :: child.flatten + else child.flatten + update = (next_x = child.node.stop) + markup <- markups + } yield markup + if (next_x < node.stop) + filled_gaps + new Markup_Node(next_x, node.stop, node.info) + else filled_gaps + } + } +} + + +class Markup_Text(val markup: List[Markup_Tree], val content: String) +{ + private lazy val root = + new Markup_Tree(new Markup_Node(0, content.length, None), markup) + + def + (new_tree: Markup_Tree): Markup_Text = + new Markup_Text((root + new_tree).branches, content) + + def filter(pred: Markup_Node => Boolean): Markup_Text = + { + def filt(tree: Markup_Tree): List[Markup_Tree] = + { + val branches = tree.branches.flatMap(filt(_)) + if (pred(tree.node)) List(tree.set_branches(branches)) + else branches + } + new Markup_Text(markup.flatMap(filt(_)), content) + } + + def flatten: List[Markup_Node] = markup.flatten(_.flatten) + + def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode = + { + def swing(tree: Markup_Tree): DefaultMutableTreeNode = + { + val node = swing_node(tree.node) + tree.branches foreach ((branch: Markup_Tree) => node.add(swing(branch))) + node + } + swing(root) + } +} diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/src/proofdocument/session.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/proofdocument/session.scala Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,250 @@ +/* + * Isabelle session, potentially with running prover + * + * @author Makarius + */ + +package isabelle.proofdocument + + +import scala.actors.TIMEOUT +import scala.actors.Actor._ + + +object Session +{ + /* events */ + + case object Global_Settings + + + /* managed entities */ + + type Entity_ID = String + + trait Entity + { + val id: Entity_ID + def consume(session: Session, message: XML.Tree): Unit + } +} + + +class Session(system: Isabelle_System) +{ + /* pervasive event buses */ + + val global_settings = new Event_Bus[Session.Global_Settings.type] + val raw_results = new Event_Bus[Isabelle_Process.Result] + val results = new Event_Bus[Command] + + val command_change = new Event_Bus[Command] + + + /* unique ids */ + + private var id_count: BigInt = 0 + def create_id(): Session.Entity_ID = synchronized { id_count += 1; "j" + id_count } + + + + /** main actor **/ + + @volatile private var syntax = new Outer_Syntax(system.symbols) + def current_syntax: Outer_Syntax = syntax + + @volatile private var entities = Map[Session.Entity_ID, Session.Entity]() + def lookup_entity(id: Session.Entity_ID): Option[Session.Entity] = entities.get(id) + def lookup_command(id: Session.Entity_ID): Option[Command] = + lookup_entity(id) match { + case Some(cmd: Command) => Some(cmd) + case _ => None + } + + private case class Start(timeout: Int, args: List[String]) + private case object Stop + private case class Begin_Document(path: String) + + private val session_actor = actor { + + var prover: Isabelle_Process with Isar_Document = null + + def register(entity: Session.Entity) { entities += (entity.id -> entity) } + + var documents = Map[Isar_Document.Document_ID, Document]() + def register_document(doc: Document) { documents += (doc.id -> doc) } + + + /* document changes */ + + def handle_change(change: Change) + { + require(change.parent.isDefined) + + val (changes, doc) = change.result.join + val id_changes = changes map { + case (c1, c2) => + (c1.map(_.id).getOrElse(""), + c2 match { + case None => None + case Some(command) => + if (!lookup_command(command.id).isDefined) { + register(command) + prover.define_command(command.id, system.symbols.encode(command.source)) + } + Some(command.id) + }) + } + register_document(doc) + prover.edit_document(change.parent.get.id, doc.id, id_changes) + } + + + /* prover results */ + + def bad_result(result: Isabelle_Process.Result) + { + System.err.println("Ignoring prover result: " + result) + } + + def handle_result(result: Isabelle_Process.Result) + { + raw_results.event(result) + + val target_id: Option[Session.Entity_ID] = Position.get_id(result.props) + val target: Option[Session.Entity] = + target_id match { + case None => None + case Some(id) => lookup_entity(id) + } + if (target.isDefined) target.get.consume(this, result.message) + else if (result.kind == Isabelle_Process.Kind.STATUS) { + // global status message + result.body match { + + // document state assigment + case List(XML.Elem(Markup.ASSIGN, _, edits)) if target_id.isDefined => + documents.get(target_id.get) match { + case Some(doc) => + val states = + for { + XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _) + <- edits + cmd <- lookup_command(cmd_id) + } yield { + val st = cmd.assign_state(state_id) + register(st) + (cmd, st) + } + doc.assign_states(states) + case None => bad_result(result) + } + + // command and keyword declarations + case List(XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _)) => + syntax += (name, kind) + case List(XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _)) => + syntax += name + + case _ => if (!result.is_ready) bad_result(result) + } + } + else if (result.kind == Isabelle_Process.Kind.EXIT) + prover = null + else if (result.kind != Isabelle_Process.Kind.STDIN && !result.is_raw) + bad_result(result) + } + + + /* prover startup */ + + def startup_error(): String = + { + val buf = new StringBuilder + while ( + receiveWithin(0) { + case result: Isabelle_Process.Result => + if (result.is_raw) { + for (text <- XML.content(result.message)) + buf.append(text) + } + true + case TIMEOUT => false + }) {} + buf.toString + } + + def prover_startup(timeout: Int): Option[String] = + { + receiveWithin(timeout) { + case result: Isabelle_Process.Result + if result.kind == Isabelle_Process.Kind.INIT => + while (receive { + case result: Isabelle_Process.Result => + handle_result(result); !result.is_ready + }) {} + None + + case result: Isabelle_Process.Result + if result.kind == Isabelle_Process.Kind.EXIT => + Some(startup_error()) + + case TIMEOUT => // FIXME clarify + prover.kill; Some(startup_error()) + } + } + + + /* main loop */ + + val xml_cache = new XML.Cache(131071) + + loop { + react { + case Start(timeout, args) => + if (prover == null) { + prover = new Isabelle_Process(system, self, args:_*) with Isar_Document + val origin = sender + val opt_err = prover_startup(timeout) + if (opt_err.isDefined) prover = null + origin ! opt_err + } + else reply(None) + + case Stop => // FIXME clarify; synchronous + if (prover != null) { + prover.kill + prover = null + } + + case Begin_Document(path: String) if prover != null => + val id = create_id() + val doc = Document.empty(id) + register_document(doc) + prover.begin_document(id, path) + reply(doc) + + case change: Change if prover != null => + handle_change(change) + + case result: Isabelle_Process.Result => + handle_result(result.cache(xml_cache)) + + case bad if prover != null => + System.err.println("session_actor: ignoring bad message " + bad) + } + } + } + + + /* main methods */ + + def start(timeout: Int, args: List[String]): Option[String] = + (session_actor !? Start(timeout, args)).asInstanceOf[Option[String]] + + def stop() { session_actor ! Stop } + def input(change: Change) { session_actor ! change } + + def begin_document(path: String): Document = + (session_actor !? Begin_Document(path)).asInstanceOf[Document] +} diff -r c1509b9d624f -r 502f90967483 src/Tools/jEdit/src/proofdocument/state.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/proofdocument/state.scala Mon Jan 11 22:31:27 2010 +0100 @@ -0,0 +1,117 @@ +/* + * Accumulating results from prover + * + * @author Fabian Immler, TU Munich + * @author Makarius + */ + +package isabelle.proofdocument + + +class State( + val command: Command, + val status: Command.Status.Value, + val rev_results: List[XML.Tree], + val markup_root: Markup_Text) +{ + def this(command: Command) = + this(command, Command.Status.UNPROCESSED, Nil, command.empty_markup) + + + /* content */ + + private def set_status(st: Command.Status.Value): State = + new State(command, st, rev_results, markup_root) + + private def add_result(res: XML.Tree): State = + new State(command, status, res :: rev_results, markup_root) + + private def add_markup(node: Markup_Tree): State = + new State(command, status, rev_results, markup_root + node) + + lazy val results = rev_results.reverse + + + /* markup */ + + lazy val highlight: Markup_Text = + { + markup_root.filter(_.info match { + case Command.HighlightInfo(_) => true + case _ => false + }) + } + + private lazy val types: List[Markup_Node] = + markup_root.filter(_.info match { + case Command.TypeInfo(_) => true + case _ => false }).flatten + + def type_at(pos: Int): Option[String] = + { + types.find(t => t.start <= pos && pos < t.stop) match { + case Some(t) => + t.info match { + case Command.TypeInfo(ty) => Some(command.source(t.start, t.stop) + ": " + ty) + case _ => None + } + case None => None + } + } + + private lazy val refs: List[Markup_Node] = + markup_root.filter(_.info match { + case Command.RefInfo(_, _, _, _) => true + case _ => false }).flatten + + def ref_at(pos: Int): Option[Markup_Node] = + refs.find(t => t.start <= pos && pos < t.stop) + + + /* message dispatch */ + + def + (session: Session, message: XML.Tree): State = + { + val changed: State = + message match { + case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) => + (this /: elems)((state, elem) => + elem match { + case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED) + case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED) + case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED) + case XML.Elem(kind, atts, body) => + val (begin, end) = Position.get_offsets(atts) + if (begin.isEmpty || end.isEmpty) state + else if (kind == Markup.ML_TYPING) { + val info = body.first.asInstanceOf[XML.Text].content // FIXME proper match!? + state.add_markup( + command.markup_node(begin.get - 1, end.get - 1, Command.TypeInfo(info))) + } + else if (kind == Markup.ML_REF) { + body match { + case List(XML.Elem(Markup.ML_DEF, atts, _)) => + state.add_markup(command.markup_node( + begin.get - 1, end.get - 1, + Command.RefInfo( + Position.get_file(atts), + Position.get_line(atts), + Position.get_id(atts), + Position.get_offset(atts)))) + case _ => state + } + } + else { + state.add_markup( + command.markup_node(begin.get - 1, end.get - 1, Command.HighlightInfo(kind))) + } + case _ => + System.err.println("ignored status report: " + elem) + state + }) + case _ => add_result(message) + } + if (!(this eq changed)) session.command_change.event(command) + changed + } +}