merged with converted/relocated copy of http://isabelle.in.tum.de/repos/isabelle-jedit/rev/93d884afa74b
1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/jEdit/README_BUILD Mon Jan 11 22:31:27 2010 +0100
1.3 @@ -0,0 +1,73 @@
1.4 +
1.5 +Requirements to build from sources
1.6 +==================================
1.7 +
1.8 +* Proper Java JRE/JDK from Sun, e.g. 1.6.0_17
1.9 + http://java.sun.com/javase/downloads/index.jsp
1.10 +
1.11 +* Netbeans 6.7
1.12 + http://www.netbeans.org/downloads/index.html
1.13 +
1.14 +* Scala for Netbeans: version 6.7v1 for NB 6.7
1.15 + http://sourceforge.net/project/showfiles.php?group_id=192439&package_id=256544
1.16 + http://blogtrader.net/dcaoyuan/category/NetBeans
1.17 + http://wiki.netbeans.org/Scala
1.18 +
1.19 +* jEdit 4.3 (final)
1.20 + http://www.jedit.org/
1.21 +
1.22 + Netbeans Project "jEdit": install official sources as ./contrib/jEdit/.
1.23 +
1.24 +* jEdit plugins:
1.25 + Netbeans Library "SideKick" = $HOME/.jedit/jars/SideKick.jar
1.26 + Netbeans Library "ErrorList" = $HOME/.jedit/jars/ErrorList.jar
1.27 + Netbeans Library "Hyperlinks" = $HOME/.jedit/jars/Hyperlinks.jar
1.28 +
1.29 +* Cobra Renderer 0.98.4
1.30 + http://lobobrowser.org/cobra.jsp
1.31 + Netbeans Library "Cobra-Renderer" = .../cobra.jar
1.32 + Netbenas Library "Rhino-JavaScript" = .../js.jar
1.33 +
1.34 +* Isabelle/Pure Scala components
1.35 + Netbeans Library "Isabelle-Pure" = ~~/lib/classes/Pure.jar
1.36 +
1.37 +
1.38 +Running the application within Netbeans
1.39 +=======================================
1.40 +
1.41 +* Project properties: add "Run" argument like
1.42 + -noserver -nobackground -settings=/home/makarius/isabelle/isabelle-jedit/dist
1.43 +
1.44 +* The Isabelle environment is obtained automatically via
1.45 + "$ISABELLE_HOME/bin/isabelle getenv", where ISABELLE_HOME is determined as follows:
1.46 +
1.47 + (1) via regular Isabelle settings,
1.48 + e.g. "isabelle env netbeans"
1.49 +
1.50 + (2) or via ISABELLE_HOME from raw process environment,
1.51 + e.g. "env ISABELLE_HOME=.../Isabelle netbeans"
1.52 +
1.53 + (3) or via JVM system properties (cf. "Run / VM Options")
1.54 + e.g. -Disabelle.home=.../Isabelle
1.55 +
1.56 +
1.57 +Misc notes
1.58 +==========
1.59 +
1.60 +- Netbeans config/Editors/Preferences/...-CustomPreferences.xml
1.61 +
1.62 + <entry javaType="java.lang.Integer" name="caret-blink-rate" xml:space="preserve">
1.63 + <value><![CDATA[0]]></value>
1.64 + </entry>
1.65 +
1.66 +-----------------------------------------------------------------------
1.67 +To run jedit with remote debugging enabled, I use the following
1.68 +command: "java
1.69 +-agentlib:jdwp=transport=dt_socket,suspend=y,server=y,address=XXXX
1.70 +-jar jedit.jar"
1.71 +
1.72 +where XXXX is any open port number you wish. The above invocation
1.73 +works for Sun's JDK 5.0. There's an alternate incantation for earlier
1.74 +releases. (See
1.75 +http://java.sun.com/j2se/1.5.0/docs/guide/jpda/conninv.html)
1.76 +-----------------------------------------------------------------------
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/Tools/jEdit/build.xml Mon Jan 11 22:31:27 2010 +0100
2.3 @@ -0,0 +1,102 @@
2.4 +<?xml version="1.0" encoding="UTF-8"?>
2.5 +<!-- You may freely edit this file. See commented blocks below for -->
2.6 +<!-- some examples of how to customize the build. -->
2.7 +<!-- (If you delete it and reopen the project it will be recreated.) -->
2.8 +<project name="Isabelle-jEdit" default="default" basedir=".">
2.9 + <description>Builds, tests, and runs the project Isabelle-jEdit.</description>
2.10 + <import file="nbproject/build-impl.xml"/>
2.11 + <!--
2.12 +
2.13 + There exist several targets which are by default empty and which can be
2.14 + used for execution of your tasks. These targets are usually executed
2.15 + before and after some main targets. They are:
2.16 +
2.17 + -pre-init: called before initialization of project properties
2.18 + -post-init: called after initialization of project properties
2.19 + -pre-compile: called before javac compilation
2.20 + -post-compile: called after javac compilation
2.21 + -pre-compile-single: called before javac compilation of single file
2.22 + -post-compile-single: called after javac compilation of single file
2.23 + -pre-compile-test: called before javac compilation of JUnit tests
2.24 + -post-compile-test: called after javac compilation of JUnit tests
2.25 + -pre-compile-test-single: called before javac compilation of single JUnit test
2.26 + -post-compile-test-single: called after javac compilation of single JUunit test
2.27 + -pre-jar: called before JAR building
2.28 + -post-jar: called after JAR building
2.29 + -post-clean: called after cleaning build products
2.30 +
2.31 + (Targets beginning with '-' are not intended to be called on their own.)
2.32 +
2.33 + Example of inserting an obfuscator after compilation could look like this:
2.34 +
2.35 + <target name="-post-compile">
2.36 + <obfuscate>
2.37 + <fileset dir="${build.classes.dir}"/>
2.38 + </obfuscate>
2.39 + </target>
2.40 +
2.41 + For list of available properties check the imported
2.42 + nbproject/build-impl.xml file.
2.43 +
2.44 +
2.45 + Another way to customize the build is by overriding existing main targets.
2.46 + The targets of interest are:
2.47 +
2.48 + -init-macrodef-javac: defines macro for javac compilation
2.49 + -init-macrodef-junit: defines macro for junit execution
2.50 + -init-macrodef-debug: defines macro for class debugging
2.51 + -init-macrodef-java: defines macro for class execution
2.52 + -do-jar-with-manifest: JAR building (if you are using a manifest)
2.53 + -do-jar-without-manifest: JAR building (if you are not using a manifest)
2.54 + run: execution of project
2.55 + -javadoc-build: Javadoc generation
2.56 + test-report: JUnit report generation
2.57 +
2.58 + An example of overriding the target for project execution could look like this:
2.59 +
2.60 + <target name="run" depends="Isabelle-jEdit-impl.jar">
2.61 + <exec dir="bin" executable="launcher.exe">
2.62 + <arg file="${dist.jar}"/>
2.63 + </exec>
2.64 + </target>
2.65 +
2.66 + Notice that the overridden target depends on the jar target and not only on
2.67 + the compile target as the regular run target does. Again, for a list of available
2.68 + properties which you can use, check the target you are overriding in the
2.69 + nbproject/build-impl.xml file.
2.70 +
2.71 + -->
2.72 + <target name="run" depends="Isabelle-jEdit-impl.jar,Isabelle-jEdit-impl.run">
2.73 + </target>
2.74 + <target name="debug" depends="Isabelle-jEdit-impl.jar,Isabelle-jEdit-impl.debug">
2.75 + </target>
2.76 + <target name="-pre-jar">
2.77 + <copy file="plugin/services.xml" todir="${build.classes.dir}" />
2.78 + <copy file="plugin/dockables.xml" todir="${build.classes.dir}" />
2.79 + <copy file="plugin/actions.xml" todir="${build.classes.dir}" />
2.80 + <copy file="plugin/Isabelle.props" todir="${build.classes.dir}" />
2.81 + </target>
2.82 + <target name="-post-jar">
2.83 + <!-- jars -->
2.84 + <delete file="${dist.dir}/jars/lib/jEdit.jar" />
2.85 + <move todir="${dist.dir}/jars">
2.86 + <fileset dir="${dist.dir}/jars/lib" />
2.87 + </move>
2.88 + <copy file="${scala.library}" todir="${dist.dir}/jars" />
2.89 + <copy file="${scala.lib}/scala-swing.jar" todir="${dist.dir}/jars" />
2.90 + <!-- clean up -->
2.91 + <delete dir="{dist.dir}/jars/lib" />
2.92 + <!-- dist-template -->
2.93 + <copy file="dist-template/properties/jedit.props" tofile="${dist.dir}/properties" />
2.94 + <copy todir="${dist.dir}/modes">
2.95 + <fileset dir="dist-template/modes" />
2.96 + </copy>
2.97 + <copy todir="${dist.dir}/modes" overwrite="true">
2.98 + <fileset dir="${project.jEdit}/modes" />
2.99 + </copy>
2.100 + <replaceregexp byline="true" file="${dist.dir}/modes/catalog">
2.101 + <regexp pattern='(^.*NAME="javacc".*$)'/>
2.102 + <substitution expression="<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>${line.separator}${line.separator}\1"/>
2.103 + </replaceregexp>
2.104 + </target>
2.105 +</project>
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/Tools/jEdit/contrib/jEdit/build-nb.xml Mon Jan 11 22:31:27 2010 +0100
3.3 @@ -0,0 +1,41 @@
3.4 +<?xml version="1.0" encoding="UTF-8"?>
3.5 +<project name="jEdit">
3.6 + <import file="./build.xml"/>
3.7 + <property environment="env"/>
3.8 +
3.9 + <target name="run" depends="compile">
3.10 + <java classname="org.gjt.sp.jedit.jEdit" classpath="./build/jEdit.jar" dir="./" fork="true">
3.11 + <arg value="-noserver"/>
3.12 + <arg value="-nobackground"/>
3.13 + <arg value="-settings=${env.ISABELLE_HOME_USER}/jedit"/>
3.14 + </java>
3.15 + </target>
3.16 +
3.17 + <target name="debug-nb" depends="compile">
3.18 + <path id="cp" location="./build/jEdit.jar" />
3.19 +
3.20 + <nbjpdastart addressproperty="jpda.address" name="jEdit" transport="dt_socket">
3.21 + <classpath refid="cp"/>
3.22 + </nbjpdastart>
3.23 +
3.24 + <java classname="org.gjt.sp.jedit.jEdit" classpathref="cp" fork="true" dir="./">
3.25 + <jvmarg value="-Xdebug"/>
3.26 + <jvmarg value="-Xrunjdwp:transport=dt_socket,address=${jpda.address}"/>
3.27 + </java>
3.28 + </target>
3.29 +
3.30 + <target name="profile-nb" depends="compile">
3.31 + <fail unless="netbeans.home">This target can only run inside the NetBeans IDE.</fail>
3.32 +
3.33 + <path id="cp" location="./build/jEdit.jar" />
3.34 +
3.35 + <nbprofiledirect>
3.36 + <classpath refid="cp"/>
3.37 + </nbprofiledirect>
3.38 +
3.39 + <java classname="org.gjt.sp.jedit.jEdit" fork="true" logError="yes" dir="." classpathref="cp">
3.40 + <classpath refid="cp"/>
3.41 + <jvmarg value="${profiler.info.jvmargs.agent}"/>
3.42 + </java>
3.43 + </target>
3.44 +</project>
3.45 \ No newline at end of file
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/Tools/jEdit/contrib/jEdit/nbproject/project.xml Mon Jan 11 22:31:27 2010 +0100
4.3 @@ -0,0 +1,118 @@
4.4 +<?xml version="1.0" encoding="UTF-8"?>
4.5 +<project xmlns="http://www.netbeans.org/ns/project/1">
4.6 + <type>org.netbeans.modules.ant.freeform</type>
4.7 + <configuration>
4.8 + <general-data xmlns="http://www.netbeans.org/ns/freeform-project/1">
4.9 + <name>jEdit</name>
4.10 + </general-data>
4.11 + <general-data xmlns="http://www.netbeans.org/ns/freeform-project/2">
4.12 + <!-- Do not use Project Properties customizer when editing this file manually. -->
4.13 + <name>jEdit</name>
4.14 + <properties>
4.15 + <property name="ant.script">build-nb.xml</property>
4.16 + </properties>
4.17 + <folders>
4.18 + <source-folder>
4.19 + <label>jEdit</label>
4.20 + <location>.</location>
4.21 + <encoding>UTF-8</encoding>
4.22 + </source-folder>
4.23 + <source-folder>
4.24 + <label>Source Packages</label>
4.25 + <type>java</type>
4.26 + <location>.</location>
4.27 + <excludes>build/** doc/** icons/** macros/** modes/** package-files/**</excludes>
4.28 + <encoding>UTF-8</encoding>
4.29 + </source-folder>
4.30 + </folders>
4.31 + <ide-actions>
4.32 + <action name="build">
4.33 + <script>${ant.script}</script>
4.34 + <target>build</target>
4.35 + </action>
4.36 + <action name="clean">
4.37 + <script>${ant.script}</script>
4.38 + <target>clean</target>
4.39 + </action>
4.40 + <action name="javadoc">
4.41 + <script>${ant.script}</script>
4.42 + <target>docs-javadoc</target>
4.43 + </action>
4.44 + <action name="run">
4.45 + <script>${ant.script}</script>
4.46 + <target>run</target>
4.47 + </action>
4.48 + <action name="rebuild">
4.49 + <script>${ant.script}</script>
4.50 + <target>clean</target>
4.51 + <target>build</target>
4.52 + </action>
4.53 + <action name="debug">
4.54 + <script>build-nb.xml</script>
4.55 + <target>debug-nb</target>
4.56 + </action>
4.57 + </ide-actions>
4.58 + <export>
4.59 + <type>jar</type>
4.60 + <location>build/jEdit.jar</location>
4.61 + <script>${ant.script}</script>
4.62 + <build-target>build</build-target>
4.63 + </export>
4.64 + <view>
4.65 + <items>
4.66 + <source-folder style="packages">
4.67 + <label>Source Packages</label>
4.68 + <location>.</location>
4.69 + <excludes>build/** doc/** icons/** macros/** modes/** package-files/**</excludes>
4.70 + </source-folder>
4.71 + <source-file>
4.72 + <location>${ant.script}</location>
4.73 + </source-file>
4.74 + </items>
4.75 + <context-menu>
4.76 + <ide-action name="build"/>
4.77 + <ide-action name="rebuild"/>
4.78 + <ide-action name="clean"/>
4.79 + <ide-action name="javadoc"/>
4.80 + <ide-action name="run"/>
4.81 + <ide-action name="debug"/>
4.82 + </context-menu>
4.83 + </view>
4.84 + <subprojects/>
4.85 + </general-data>
4.86 + <java-data xmlns="http://www.netbeans.org/ns/freeform-project-java/1">
4.87 + <compilation-unit>
4.88 + <package-root>.</package-root>
4.89 + <classpath mode="compile">.</classpath>
4.90 + <built-to>build/jEdit.jar</built-to>
4.91 + <source-level>1.5</source-level>
4.92 + </compilation-unit>
4.93 + </java-data>
4.94 + <preferences xmlns="http://www.netbeans.org/ns/auxiliary-configuration-preferences/1">
4.95 + <module name="org-netbeans-modules-editor-indent">
4.96 + <node name="CodeStyle">
4.97 + <property name="usedProfile" value="default"/>
4.98 + <node name="project">
4.99 + <property name="spaces-per-tab" value="2"/>
4.100 + <property name="tab-size" value="2"/>
4.101 + <property name="indent-shift-width" value="2"/>
4.102 + <property name="text-limit-width" value="100"/>
4.103 + <property name="expand-tabs" value="true"/>
4.104 + </node>
4.105 + </node>
4.106 + <node name="text">
4.107 + <node name="x-java">
4.108 + <node name="CodeStyle">
4.109 + <node name="project">
4.110 + <property name="tab-size" value="4"/>
4.111 + <property name="text-limit-width" value="100"/>
4.112 + <property name="spaces-per-tab" value="2"/>
4.113 + <property name="indent-shift-width" value="2"/>
4.114 + </node>
4.115 + </node>
4.116 + </node>
4.117 + </node>
4.118 + </module>
4.119 + </preferences>
4.120 + </configuration>
4.121 +</project>
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/Tools/jEdit/dist-template/etc/settings Mon Jan 11 22:31:27 2010 +0100
5.3 @@ -0,0 +1,9 @@
5.4 +JEDIT_HOME="$COMPONENT"
5.5 +
5.6 +JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss2m"
5.7 +#JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx1024m -Xss4m"
5.8 +JEDIT_OPTIONS="-reuseview -noserver -nobackground"
5.9 +
5.10 +ISABELLE_JEDIT_OPTIONS="-m xsymbols -m no_brackets -m no_type_brackets"
5.11 +
5.12 +ISABELLE_TOOLS="$ISABELLE_TOOLS:$JEDIT_HOME/lib/Tools"
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/Tools/jEdit/dist-template/lib/Tools/jedit Mon Jan 11 22:31:27 2010 +0100
6.3 @@ -0,0 +1,117 @@
6.4 +#!/usr/bin/env bash
6.5 +#
6.6 +# Author: Makarius
6.7 +#
6.8 +# DESCRIPTION: Isabelle/jEdit interface wrapper
6.9 +
6.10 +
6.11 +## diagnostics
6.12 +
6.13 +PRG="$(basename "$0")"
6.14 +
6.15 +usage()
6.16 +{
6.17 + echo
6.18 + echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]"
6.19 + echo
6.20 + echo " Options are:"
6.21 + echo " -J OPTION add JVM runtime option"
6.22 + echo " (default JEDIT_JAVA_OPTIONS=$JEDIT_JAVA_OPTIONS)"
6.23 + echo " -d enable debugger"
6.24 + echo " -j OPTION add jEdit runtime option"
6.25 + echo " (default JEDIT_OPTIONS=$JEDIT_OPTIONS)"
6.26 + echo " -l NAME logic image name (default ISABELLE_LOGIC=$ISABELLE_LOGIC)"
6.27 + echo " -m MODE add print mode for output"
6.28 + echo
6.29 + echo "Start jEdit with Isabelle plugin setup and opens theory FILES"
6.30 + echo "(default ~/Scratch.thy)."
6.31 + echo
6.32 + exit 1
6.33 +}
6.34 +
6.35 +fail()
6.36 +{
6.37 + echo "$1" >&2
6.38 + exit 2
6.39 +}
6.40 +
6.41 +
6.42 +## process command line
6.43 +
6.44 +# options
6.45 +
6.46 +JEDIT_LOGIC="$ISABELLE_LOGIC"
6.47 +JEDIT_PRINT_MODE=""
6.48 +
6.49 +getoptions()
6.50 +{
6.51 + OPTIND=1
6.52 + while getopts "J:dj:l:m:" OPT
6.53 + do
6.54 + case "$OPT" in
6.55 + J)
6.56 + JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG"
6.57 + ;;
6.58 + d)
6.59 + JAVA_ARGS["${#JAVA_ARGS[@]}"]="-Xdebug"
6.60 + JAVA_ARGS["${#JAVA_ARGS[@]}"]="-Xrunjdwp:transport=dt_socket,server=y,suspend=n"
6.61 + ;;
6.62 + j)
6.63 + ARGS["${#ARGS[@]}"]="$OPTARG"
6.64 + ;;
6.65 + l)
6.66 + JEDIT_LOGIC="$OPTARG"
6.67 + ;;
6.68 + m)
6.69 + if [ -z "$JEDIT_PRINT_MODE" ]; then
6.70 + JEDIT_PRINT_MODE="$OPTARG"
6.71 + else
6.72 + JEDIT_PRINT_MODE="$JEDIT_PRINT_MODE,$OPTARG"
6.73 + fi
6.74 + ;;
6.75 + \?)
6.76 + usage
6.77 + ;;
6.78 + esac
6.79 + done
6.80 +}
6.81 +
6.82 +declare -a JAVA_ARGS; eval "JAVA_ARGS=($JEDIT_JAVA_OPTIONS)"
6.83 +[ -n "$SCALA_HOME" ] && JAVA_ARGS["${#JAVA_ARGS[@]}"]="-Dscala.home=$SCALA_HOME"
6.84 +
6.85 +declare -a ARGS; eval "ARGS=($JEDIT_OPTIONS)"
6.86 +
6.87 +declare -a OPTIONS; eval "OPTIONS=($ISABELLE_JEDIT_OPTIONS)"
6.88 +getoptions "${OPTIONS[@]}"
6.89 +
6.90 +getoptions "$@"
6.91 +shift $(($OPTIND - 1))
6.92 +
6.93 +
6.94 +# args
6.95 +
6.96 +if [ "$#" -eq 0 ]; then
6.97 + ARGS["${#ARGS[@]}"]="Scratch.thy"
6.98 +else
6.99 + while [ "$#" -gt 0 ]; do
6.100 + ARGS["${#ARGS[@]}"]="$(jvmpath "$1")"
6.101 + shift
6.102 + done
6.103 +fi
6.104 +
6.105 +
6.106 +## main
6.107 +
6.108 +case "$JEDIT_LOGIC" in
6.109 + /*)
6.110 + ;;
6.111 + */*)
6.112 + JEDIT_LOGIC="$(pwd -P)/$JEDIT_LOGIC"
6.113 + ;;
6.114 +esac
6.115 +
6.116 +export JEDIT_LOGIC JEDIT_PRINT_MODE
6.117 +
6.118 +exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \
6.119 + -jar "$(jvmpath "$JEDIT_HOME/jedit.jar")" \
6.120 + "-settings=$(jvmpath "$ISABELLE_HOME_USER/jedit")" "${ARGS[@]}"
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/Tools/jEdit/dist-template/modes/isabelle-session.xml Mon Jan 11 22:31:27 2010 +0100
7.3 @@ -0,0 +1,41 @@
7.4 +<?xml version="1.0"?>
7.5 +<!DOCTYPE MODE SYSTEM "xmode.dtd">
7.6 +
7.7 +<!-- Isabelle session mode -->
7.8 +<MODE>
7.9 + <PROPS>
7.10 + <PROPERTY NAME="commentStart" VALUE="(*"/>
7.11 + <PROPERTY NAME="commentEnd" VALUE="*)"/>
7.12 + <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
7.13 + <PROPERTY NAME="unalignedOpenBrackets" VALUE="(" />
7.14 + <PROPERTY NAME="unalignedCloseBrackets" VALUE=")" />
7.15 + <PROPERTY NAME="tabSize" VALUE="2" />
7.16 + <PROPERTY NAME="indentSize" VALUE="2" />
7.17 + </PROPS>
7.18 + <RULES IGNORE_CASE="FALSE" HIGHLIGHT_DIGITS="FALSE" ESCAPE="\">
7.19 + <SPAN TYPE="COMMENT1">
7.20 + <BEGIN>(*</BEGIN>
7.21 + <END>*)</END>
7.22 + </SPAN>
7.23 + <SPAN TYPE="COMMENT3">
7.24 + <BEGIN>{*</BEGIN>
7.25 + <END>*}</END>
7.26 + </SPAN>
7.27 + <SPAN TYPE="LITERAL1">
7.28 + <BEGIN>`</BEGIN>
7.29 + <END>`</END>
7.30 + </SPAN>
7.31 + <SPAN TYPE="LITERAL3">
7.32 + <BEGIN>"</BEGIN>
7.33 + <END>"</END>
7.34 + </SPAN>
7.35 + <KEYWORDS>
7.36 + <KEYWORD1>session</KEYWORD1>
7.37 + <KEYWORD2>parent</KEYWORD2>
7.38 + <KEYWORD2>imports</KEYWORD2>
7.39 + <KEYWORD2>uses</KEYWORD2>
7.40 + <KEYWORD2>options</KEYWORD2>
7.41 + <KEYWORD2>dependencies</KEYWORD2>
7.42 + </KEYWORDS>
7.43 + </RULES>
7.44 +</MODE>
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/Tools/jEdit/dist-template/modes/isabelle.xml Mon Jan 11 22:31:27 2010 +0100
8.3 @@ -0,0 +1,43 @@
8.4 +<?xml version="1.0"?>
8.5 +<!DOCTYPE MODE SYSTEM "xmode.dtd">
8.6 +
8.7 +<!-- Isabelle theory mode -->
8.8 +<MODE>
8.9 + <PROPS>
8.10 + <PROPERTY NAME="commentStart" VALUE="(*"/>
8.11 + <PROPERTY NAME="commentEnd" VALUE="*)"/>
8.12 + <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
8.13 + <PROPERTY NAME="indentOpenBrackets" VALUE="{"/>
8.14 + <PROPERTY NAME="indentCloseBrackets" VALUE="}"/>
8.15 + <PROPERTY NAME="unalignedOpenBrackets" VALUE="(" />
8.16 + <PROPERTY NAME="unalignedCloseBrackets" VALUE=")" />
8.17 + <PROPERTY NAME="tabSize" VALUE="2" />
8.18 + <PROPERTY NAME="indentSize" VALUE="2" />
8.19 + </PROPS>
8.20 + <RULES IGNORE_CASE="FALSE" HIGHLIGHT_DIGITS="FALSE" ESCAPE="\">
8.21 + <SPAN TYPE="COMMENT1">
8.22 + <BEGIN>(*</BEGIN>
8.23 + <END>*)</END>
8.24 + </SPAN>
8.25 + <SPAN TYPE="COMMENT3">
8.26 + <BEGIN>{*</BEGIN>
8.27 + <END>*}</END>
8.28 + </SPAN>
8.29 + <SPAN TYPE="LITERAL1">
8.30 + <BEGIN>`</BEGIN>
8.31 + <END>`</END>
8.32 + </SPAN>
8.33 + <SPAN TYPE="LITERAL3">
8.34 + <BEGIN>"</BEGIN>
8.35 + <END>"</END>
8.36 + </SPAN>
8.37 + <KEYWORDS>
8.38 + <KEYWORD2>header</KEYWORD2>
8.39 + <KEYWORD1>theory</KEYWORD1>
8.40 + <KEYWORD2>imports</KEYWORD2>
8.41 + <KEYWORD2>uses</KEYWORD2>
8.42 + <KEYWORD2>begin</KEYWORD2>
8.43 + <KEYWORD2>end</KEYWORD2>
8.44 + </KEYWORDS>
8.45 + </RULES>
8.46 +</MODE>
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/src/Tools/jEdit/dist-template/properties/jedit.props Mon Jan 11 22:31:27 2010 +0100
9.3 @@ -0,0 +1,191 @@
9.4 +#jEdit properties
9.5 +buffer.deepIndent=false
9.6 +buffer.encoding=UTF-8-Isabelle
9.7 +buffer.indentSize=2
9.8 +buffer.lineSeparator=\n
9.9 +buffer.maxLineLen=100
9.10 +buffer.noTabs=true
9.11 +buffer.sidekick.keystroke-parse=true
9.12 +buffer.tabSize=2
9.13 +delete-line.shortcut=A+d
9.14 +delete.shortcut2=C+d
9.15 +encoding.opt-out.Big5-HKSCS=true
9.16 +encoding.opt-out.Big5=true
9.17 +encoding.opt-out.COMPOUND_TEXT=true
9.18 +encoding.opt-out.EUC-JP=true
9.19 +encoding.opt-out.EUC-KR=true
9.20 +encoding.opt-out.GB18030=true
9.21 +encoding.opt-out.GB2312=true
9.22 +encoding.opt-out.GBK=true
9.23 +encoding.opt-out.IBM-Thai=true
9.24 +encoding.opt-out.IBM00858=true
9.25 +encoding.opt-out.IBM01140=true
9.26 +encoding.opt-out.IBM01141=true
9.27 +encoding.opt-out.IBM01142=true
9.28 +encoding.opt-out.IBM01143=true
9.29 +encoding.opt-out.IBM01144=true
9.30 +encoding.opt-out.IBM01145=true
9.31 +encoding.opt-out.IBM01146=true
9.32 +encoding.opt-out.IBM01147=true
9.33 +encoding.opt-out.IBM01148=true
9.34 +encoding.opt-out.IBM01149=true
9.35 +encoding.opt-out.IBM037=true
9.36 +encoding.opt-out.IBM1026=true
9.37 +encoding.opt-out.IBM1047=true
9.38 +encoding.opt-out.IBM273=true
9.39 +encoding.opt-out.IBM277=true
9.40 +encoding.opt-out.IBM278=true
9.41 +encoding.opt-out.IBM280=true
9.42 +encoding.opt-out.IBM284=true
9.43 +encoding.opt-out.IBM285=true
9.44 +encoding.opt-out.IBM297=true
9.45 +encoding.opt-out.IBM420=true
9.46 +encoding.opt-out.IBM424=true
9.47 +encoding.opt-out.IBM437=true
9.48 +encoding.opt-out.IBM500=true
9.49 +encoding.opt-out.IBM775=true
9.50 +encoding.opt-out.IBM850=true
9.51 +encoding.opt-out.IBM852=true
9.52 +encoding.opt-out.IBM855=true
9.53 +encoding.opt-out.IBM857=true
9.54 +encoding.opt-out.IBM860=true
9.55 +encoding.opt-out.IBM861=true
9.56 +encoding.opt-out.IBM862=true
9.57 +encoding.opt-out.IBM863=true
9.58 +encoding.opt-out.IBM864=true
9.59 +encoding.opt-out.IBM865=true
9.60 +encoding.opt-out.IBM866=true
9.61 +encoding.opt-out.IBM868=true
9.62 +encoding.opt-out.IBM869=true
9.63 +encoding.opt-out.IBM870=true
9.64 +encoding.opt-out.IBM871=true
9.65 +encoding.opt-out.IBM918=true
9.66 +encoding.opt-out.ISO-2022-CN=true
9.67 +encoding.opt-out.ISO-2022-JP-2=true
9.68 +encoding.opt-out.ISO-2022-JP=true
9.69 +encoding.opt-out.ISO-2022-KR=true
9.70 +encoding.opt-out.ISO-8859-13=true
9.71 +encoding.opt-out.ISO-8859-2=true
9.72 +encoding.opt-out.ISO-8859-3=true
9.73 +encoding.opt-out.ISO-8859-4=true
9.74 +encoding.opt-out.ISO-8859-5=true
9.75 +encoding.opt-out.ISO-8859-6=true
9.76 +encoding.opt-out.ISO-8859-7=true
9.77 +encoding.opt-out.ISO-8859-8=true
9.78 +encoding.opt-out.ISO-8859-9=true
9.79 +encoding.opt-out.JIS_X0201=true
9.80 +encoding.opt-out.JIS_X0212-1990=true
9.81 +encoding.opt-out.KOI8-R=true
9.82 +encoding.opt-out.KOI8-U=true
9.83 +encoding.opt-out.Shift_JIS=true
9.84 +encoding.opt-out.TIS-620=true
9.85 +encoding.opt-out.UTF-16=true
9.86 +encoding.opt-out.UTF-16BE=true
9.87 +encoding.opt-out.UTF-16LE=true
9.88 +encoding.opt-out.UTF-32=true
9.89 +encoding.opt-out.UTF-32BE=true
9.90 +encoding.opt-out.UTF-32LE=true
9.91 +encoding.opt-out.X-UTF-32BE-BOM=true
9.92 +encoding.opt-out.X-UTF-32LE-BOM=true
9.93 +encoding.opt-out.windows-1250=true
9.94 +encoding.opt-out.windows-1251=true
9.95 +encoding.opt-out.windows-1253=true
9.96 +encoding.opt-out.windows-1254=true
9.97 +encoding.opt-out.windows-1255=true
9.98 +encoding.opt-out.windows-1256=true
9.99 +encoding.opt-out.windows-1257=true
9.100 +encoding.opt-out.windows-1258=true
9.101 +encoding.opt-out.windows-31j=true
9.102 +encoding.opt-out.x-Big5-Solaris=true
9.103 +encoding.opt-out.x-EUC-TW=true
9.104 +encoding.opt-out.x-IBM1006=true
9.105 +encoding.opt-out.x-IBM1025=true
9.106 +encoding.opt-out.x-IBM1046=true
9.107 +encoding.opt-out.x-IBM1097=true
9.108 +encoding.opt-out.x-IBM1098=true
9.109 +encoding.opt-out.x-IBM1112=true
9.110 +encoding.opt-out.x-IBM1122=true
9.111 +encoding.opt-out.x-IBM1123=true
9.112 +encoding.opt-out.x-IBM1124=true
9.113 +encoding.opt-out.x-IBM1381=true
9.114 +encoding.opt-out.x-IBM1383=true
9.115 +encoding.opt-out.x-IBM33722=true
9.116 +encoding.opt-out.x-IBM737=true
9.117 +encoding.opt-out.x-IBM834=true
9.118 +encoding.opt-out.x-IBM856=true
9.119 +encoding.opt-out.x-IBM874=true
9.120 +encoding.opt-out.x-IBM875=true
9.121 +encoding.opt-out.x-IBM921=true
9.122 +encoding.opt-out.x-IBM922=true
9.123 +encoding.opt-out.x-IBM930=true
9.124 +encoding.opt-out.x-IBM933=true
9.125 +encoding.opt-out.x-IBM935=true
9.126 +encoding.opt-out.x-IBM937=true
9.127 +encoding.opt-out.x-IBM939=true
9.128 +encoding.opt-out.x-IBM942=true
9.129 +encoding.opt-out.x-IBM942C=true
9.130 +encoding.opt-out.x-IBM943=true
9.131 +encoding.opt-out.x-IBM943C=true
9.132 +encoding.opt-out.x-IBM948=true
9.133 +encoding.opt-out.x-IBM949=true
9.134 +encoding.opt-out.x-IBM949C=true
9.135 +encoding.opt-out.x-IBM950=true
9.136 +encoding.opt-out.x-IBM964=true
9.137 +encoding.opt-out.x-IBM970=true
9.138 +encoding.opt-out.x-ISCII91=true
9.139 +encoding.opt-out.x-ISO-2022-CN-CNS=true
9.140 +encoding.opt-out.x-ISO-2022-CN-GB=true
9.141 +encoding.opt-out.x-JIS0208=true
9.142 +encoding.opt-out.x-JISAutoDetect=true
9.143 +encoding.opt-out.x-Johab=true
9.144 +encoding.opt-out.x-MS932_0213=true
9.145 +encoding.opt-out.x-MS950-HKSCS=true
9.146 +encoding.opt-out.x-MacArabic=true
9.147 +encoding.opt-out.x-MacCentralEurope=true
9.148 +encoding.opt-out.x-MacCroatian=true
9.149 +encoding.opt-out.x-MacCyrillic=true
9.150 +encoding.opt-out.x-MacDingbat=true
9.151 +encoding.opt-out.x-MacGreek=true
9.152 +encoding.opt-out.x-MacHebrew=true
9.153 +encoding.opt-out.x-MacIceland=true
9.154 +encoding.opt-out.x-MacRoman=true
9.155 +encoding.opt-out.x-MacRomania=true
9.156 +encoding.opt-out.x-MacSymbol=true
9.157 +encoding.opt-out.x-MacThai=true
9.158 +encoding.opt-out.x-MacTurkish=true
9.159 +encoding.opt-out.x-MacUkraine=true
9.160 +encoding.opt-out.x-PCK=true
9.161 +encoding.opt-out.x-SJIS_0213=true
9.162 +encoding.opt-out.x-UTF-16LE-BOM=true
9.163 +encoding.opt-out.x-euc-jp-linux=true
9.164 +encoding.opt-out.x-eucJP-Open=true
9.165 +encoding.opt-out.x-iso-8859-11=true
9.166 +encoding.opt-out.x-mswin-936=true
9.167 +encoding.opt-out.x-windows-50220=true
9.168 +encoding.opt-out.x-windows-50221=true
9.169 +encoding.opt-out.x-windows-874=true
9.170 +encoding.opt-out.x-windows-949=true
9.171 +encoding.opt-out.x-windows-950=true
9.172 +encoding.opt-out.x-windows-iso2022jp=true
9.173 +encodingDetectors=BOM XML-PI buffer-local-property
9.174 +fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII
9.175 +firstTime=false
9.176 +isabelle-protocol.dock-position=bottom
9.177 +isabelle-results.dock-position=bottom
9.178 +isabelle.activate.shortcut=CS+ENTER
9.179 +mode.isabelle.sidekick.showStatusWindow.label=true
9.180 +sidekick-tree.dock-position=right
9.181 +sidekick.buffer-save-parse=true
9.182 +sidekick.complete-delay=300
9.183 +tip.show=false
9.184 +view.antiAlias=standard
9.185 +view.blockCaret=true
9.186 +view.caretBlink=false
9.187 +view.eolMarkers=false
9.188 +view.extendedState=0
9.189 +view.font=IsabelleText
9.190 +view.fontsize=18
9.191 +view.fracFontMetrics=false
9.192 +view.gutter.fontsize=12
9.193 +view.middleMousePaste=true
9.194 +view.showToolbar=false
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/src/Tools/jEdit/makedist Mon Jan 11 22:31:27 2010 +0100
10.3 @@ -0,0 +1,98 @@
10.4 +#!/usr/bin/env bash
10.5 +#
10.6 +# makedist -- make Isabelle/jEdit distribution
10.7 +
10.8 +## self references
10.9 +
10.10 +PRG=$(basename "$0")
10.11 +THIS=$(cd "$(dirname "$0")"; pwd)
10.12 +SUPER=$(cd "$THIS/.."; pwd)
10.13 +
10.14 +
10.15 +## diagnostics
10.16 +
10.17 +JEDIT_HOME="/home/isajedit/jedit-orig/4.3pre17"
10.18 +
10.19 +function usage()
10.20 +{
10.21 + echo
10.22 + echo "Usage: $PRG [OPTIONS]"
10.23 + echo
10.24 + echo " Options are:"
10.25 + echo " -j DIR specify original jEdit distribution"
10.26 + echo " (default: $JEDIT_HOME)"
10.27 + echo
10.28 + echo " Produce Isabelle/jEdit distribution from Netbeans build"
10.29 + echo " in $THIS/dist"
10.30 + echo
10.31 + exit 1
10.32 +}
10.33 +
10.34 +fail()
10.35 +{
10.36 + echo "$1" >&2
10.37 + exit 2
10.38 +}
10.39 +
10.40 +
10.41 +## process command line
10.42 +
10.43 +# options
10.44 +
10.45 +while getopts "j:s:" OPT
10.46 +do
10.47 + case "$OPT" in
10.48 + j)
10.49 + JEDIT_HOME="$OPTARG"
10.50 + ;;
10.51 + \?)
10.52 + usage
10.53 + ;;
10.54 + esac
10.55 +done
10.56 +
10.57 +shift $(($OPTIND - 1))
10.58 +
10.59 +
10.60 +# args
10.61 +
10.62 +[ "$#" -ne 0 ] && usage
10.63 +
10.64 +
10.65 +## main
10.66 +
10.67 +cd "$THIS/dist" || fail "Bad directory: $THIS/dist"
10.68 +
10.69 +
10.70 +# target name
10.71 +
10.72 +VERSION=$(basename "$JEDIT_HOME")
10.73 +JEDIT="jedit-${VERSION}"
10.74 +
10.75 +rm -rf "$JEDIT" jedit
10.76 +mkdir "$JEDIT"
10.77 +ln -s "$JEDIT" jedit
10.78 +
10.79 +
10.80 +# copy stuff
10.81 +
10.82 +[ "$JEDIT_HOME/jedit.jar" ] || fail "Bad original jEdit directory: $JEDIT_HOME"
10.83 +cp -R "$JEDIT_HOME/." "$JEDIT/."
10.84 +rm -rf "$JEDIT/jEdit" "$JEDIT/build-support"
10.85 +
10.86 +mkdir -p "$JEDIT/jars"
10.87 +cp -R jars/. "$JEDIT/jars/."
10.88 +
10.89 +cp -R "$THIS/dist-template/." "$JEDIT/."
10.90 +
10.91 +perl -i -e 'while (<>) { if (m/NAME="javacc"/) {
10.92 + print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,;
10.93 + print qq,<MODE NAME="isabelle-session" FILE="isabelle-session.xml" FILE_NAME_GLOB="session.root"/>\n\n,; }
10.94 + print; }' "$JEDIT/modes/catalog"
10.95 +
10.96 +
10.97 +# build archive
10.98 +
10.99 +echo "${JEDIT}.tar.gz"
10.100 +tar czf "${JEDIT}.tar.gz" "$JEDIT" jedit
10.101 +ln -sf "${JEDIT}.tar.gz" jedit.tar.gz
11.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
11.2 +++ b/src/Tools/jEdit/manifest.mf Mon Jan 11 22:31:27 2010 +0100
11.3 @@ -0,0 +1,3 @@
11.4 +Manifest-Version: 1.0
11.5 +X-COMMENT: Main-Class will be added automatically by build
11.6 +
12.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
12.2 +++ b/src/Tools/jEdit/nbproject/build-impl.xml Mon Jan 11 22:31:27 2010 +0100
12.3 @@ -0,0 +1,709 @@
12.4 +<?xml version="1.0" encoding="UTF-8"?>
12.5 +<!--
12.6 +*** GENERATED FROM project.xml - DO NOT EDIT ***
12.7 +*** EDIT ../build.xml INSTEAD ***
12.8 +
12.9 +For the purpose of easier reading the script
12.10 +is divided into following sections:
12.11 +
12.12 + - initialization
12.13 + - compilation
12.14 + - jar
12.15 + - execution
12.16 + - debugging
12.17 + - javadoc
12.18 + - junit compilation
12.19 + - junit execution
12.20 + - junit debugging
12.21 + - applet
12.22 + - cleanup
12.23 +
12.24 +
12.25 + -->
12.26 +<project xmlns:jaxrpc="http://www.netbeans.org/ns/scala-project/jax-rpc" xmlns:scalaProject1="http://www.netbeans.org/ns/scala-project/1" basedir=".." default="default" name="Isabelle-jEdit-impl">
12.27 + <target depends="test,jar,javadoc" description="Build and test whole project." name="default"/>
12.28 + <!--
12.29 + ======================
12.30 + INITIALIZATION SECTION
12.31 + ======================
12.32 + -->
12.33 + <target name="-pre-init">
12.34 + <!-- Empty placeholder for easier customization. -->
12.35 + <!-- You can override this target in the ../build.xml file. -->
12.36 + </target>
12.37 + <target depends="-pre-init" name="-init-private">
12.38 + <property file="nbproject/private/config.properties"/>
12.39 + <property file="nbproject/private/configs/${config}.properties"/>
12.40 + <property file="nbproject/private/private.properties"/>
12.41 + <property environment="env"/>
12.42 + <condition property="scala.home" value="${env.SCALA_HOME}">
12.43 + <isset property="env.SCALA_HOME"/>
12.44 + </condition>
12.45 + <fail unless="scala.home">
12.46 +You must set SCALA_HOME or environment property and append "-J-Dscala.home=scalahomepath"
12.47 +property to the end of "netbeans_default_options" in NetBeansInstallationPath/etc/netbeans.conf to point to
12.48 +Scala installation directory.
12.49 + </fail>
12.50 + <property name="scala.compiler" value="${scala.home}/lib/scala-compiler.jar"/>
12.51 + <property name="scala.library" value="${scala.home}/lib/scala-library.jar"/>
12.52 + <property name="scala.lib" value="${scala.home}/lib"/>
12.53 + <taskdef resource="scala/tools/ant/antlib.xml">
12.54 + <classpath>
12.55 + <pathelement location="${scala.compiler}"/>
12.56 + <pathelement location="${scala.library}"/>
12.57 + </classpath>
12.58 + </taskdef>
12.59 + <chmod dir="${scala.home}/bin" includes="**/*" perm="u+rx"/>
12.60 + </target>
12.61 + <target depends="-pre-init,-init-private" name="-init-user">
12.62 + <property file="${user.properties.file}"/>
12.63 + <!-- The two properties below are usually overridden -->
12.64 + <!-- by the active platform. Just a fallback. -->
12.65 + <property name="default.javac.source" value="1.4"/>
12.66 + <property name="default.javac.target" value="1.4"/>
12.67 + </target>
12.68 + <target depends="-pre-init,-init-private,-init-user" name="-init-project">
12.69 + <property file="nbproject/configs/${config}.properties"/>
12.70 + <property file="nbproject/project.properties"/>
12.71 + </target>
12.72 + <target depends="-pre-init,-init-private,-init-user,-init-project,-init-macrodef-property" name="-do-init">
12.73 + <available file="${manifest.file}" property="manifest.available"/>
12.74 + <condition property="manifest.available+main.class">
12.75 + <and>
12.76 + <isset property="manifest.available"/>
12.77 + <isset property="main.class"/>
12.78 + <not>
12.79 + <equals arg1="${main.class}" arg2="" trim="true"/>
12.80 + </not>
12.81 + </and>
12.82 + </condition>
12.83 + <condition property="manifest.available+main.class+mkdist.available">
12.84 + <and>
12.85 + <istrue value="${manifest.available+main.class}"/>
12.86 + <isset property="libs.CopyLibs.classpath"/>
12.87 + </and>
12.88 + </condition>
12.89 + <condition property="have.tests">
12.90 + <or/>
12.91 + </condition>
12.92 + <condition property="have.sources">
12.93 + <or>
12.94 + <available file="${src.dir}"/>
12.95 + </or>
12.96 + </condition>
12.97 + <condition property="netbeans.home+have.tests">
12.98 + <and>
12.99 + <isset property="netbeans.home"/>
12.100 + <isset property="have.tests"/>
12.101 + </and>
12.102 + </condition>
12.103 + <condition property="no.javadoc.preview">
12.104 + <and>
12.105 + <isset property="javadoc.preview"/>
12.106 + <isfalse value="${javadoc.preview}"/>
12.107 + </and>
12.108 + </condition>
12.109 + <property name="run.jvmargs" value=""/>
12.110 + <property name="javac.compilerargs" value=""/>
12.111 + <property name="work.dir" value="${basedir}"/>
12.112 + <condition property="no.deps">
12.113 + <and>
12.114 + <istrue value="${no.dependencies}"/>
12.115 + </and>
12.116 + </condition>
12.117 + <property name="javac.debug" value="true"/>
12.118 + <property name="javadoc.preview" value="true"/>
12.119 + <property name="application.args" value=""/>
12.120 + <property name="source.encoding" value="${file.encoding}"/>
12.121 + <condition property="javadoc.encoding.used" value="${javadoc.encoding}">
12.122 + <and>
12.123 + <isset property="javadoc.encoding"/>
12.124 + <not>
12.125 + <equals arg1="${javadoc.encoding}" arg2=""/>
12.126 + </not>
12.127 + </and>
12.128 + </condition>
12.129 + <property name="javadoc.encoding.used" value="${source.encoding}"/>
12.130 + <property name="includes" value="**"/>
12.131 + <property name="excludes" value=""/>
12.132 + <property name="do.depend" value="false"/>
12.133 + <condition property="do.depend.true">
12.134 + <istrue value="${do.depend}"/>
12.135 + </condition>
12.136 + <condition else="" property="javac.compilerargs.jaxws" value="-Djava.endorsed.dirs='${jaxws.endorsed.dir}'">
12.137 + <and>
12.138 + <isset property="jaxws.endorsed.dir"/>
12.139 + <available file="nbproject/jaxws-build.xml"/>
12.140 + </and>
12.141 + </condition>
12.142 + </target>
12.143 + <target name="-post-init">
12.144 + <!-- Empty placeholder for easier customization. -->
12.145 + <!-- You can override this target in the ../build.xml file. -->
12.146 + </target>
12.147 + <target depends="-pre-init,-init-private,-init-user,-init-project,-do-init" name="-init-check">
12.148 + <fail unless="src.dir">Must set src.dir</fail>
12.149 + <fail unless="build.dir">Must set build.dir</fail>
12.150 + <fail unless="dist.dir">Must set dist.dir</fail>
12.151 + <fail unless="build.classes.dir">Must set build.classes.dir</fail>
12.152 + <fail unless="dist.javadoc.dir">Must set dist.javadoc.dir</fail>
12.153 + <fail unless="build.test.classes.dir">Must set build.test.classes.dir</fail>
12.154 + <fail unless="build.test.results.dir">Must set build.test.results.dir</fail>
12.155 + <fail unless="build.classes.excludes">Must set build.classes.excludes</fail>
12.156 + <fail unless="dist.jar">Must set dist.jar</fail>
12.157 + </target>
12.158 + <target name="-init-macrodef-property">
12.159 + <macrodef name="property" uri="http://www.netbeans.org/ns/scala-project/1">
12.160 + <attribute name="name"/>
12.161 + <attribute name="value"/>
12.162 + <sequential>
12.163 + <property name="@{name}" value="${@{value}}"/>
12.164 + </sequential>
12.165 + </macrodef>
12.166 + </target>
12.167 + <target name="-init-macrodef-javac">
12.168 + <macrodef name="javac" uri="http://www.netbeans.org/ns/scala-project/1">
12.169 + <attribute default="${src.dir}" name="srcdir"/>
12.170 + <attribute default="${build.classes.dir}" name="destdir"/>
12.171 + <attribute default="${javac.classpath}" name="classpath"/>
12.172 + <attribute default="${includes}" name="includes"/>
12.173 + <attribute default="${excludes}" name="excludes"/>
12.174 + <attribute default="${javac.debug}" name="debug"/>
12.175 + <attribute default="" name="sourcepath"/>
12.176 + <element name="customize" optional="true"/>
12.177 + <sequential>
12.178 + <javac debug="@{debug}" deprecation="${javac.deprecation}" destdir="@{destdir}" encoding="${source.encoding}" excludes="@{excludes}" includeantruntime="false" includes="@{includes}" source="${javac.source}" sourcepath="@{sourcepath}" srcdir="@{srcdir}" target="${javac.target}">
12.179 + <classpath>
12.180 + <path path="@{classpath}"/>
12.181 + <fileset dir="${scala.lib}">
12.182 + <include name="**/*.jar"/>
12.183 + </fileset>
12.184 + </classpath>
12.185 + <compilerarg line="${javac.compilerargs} ${javac.compilerargs.jaxws}"/>
12.186 + <customize/>
12.187 + </javac>
12.188 + </sequential>
12.189 + </macrodef>
12.190 + <macrodef name="depend" uri="http://www.netbeans.org/ns/scala-project/1">
12.191 + <attribute default="${src.dir}" name="srcdir"/>
12.192 + <attribute default="${build.classes.dir}" name="destdir"/>
12.193 + <attribute default="${javac.classpath}" name="classpath"/>
12.194 + <sequential>
12.195 + <depend cache="${build.dir}/depcache" destdir="@{destdir}" excludes="${excludes}" includes="${includes}" srcdir="@{srcdir}">
12.196 + <classpath>
12.197 + <path path="@{classpath}"/>
12.198 + </classpath>
12.199 + </depend>
12.200 + </sequential>
12.201 + </macrodef>
12.202 + <macrodef name="force-recompile" uri="http://www.netbeans.org/ns/scala-project/1">
12.203 + <attribute default="${build.classes.dir}" name="destdir"/>
12.204 + <sequential>
12.205 + <fail unless="javac.includes">Must set javac.includes</fail>
12.206 + <pathconvert pathsep="," property="javac.includes.binary">
12.207 + <path>
12.208 + <filelist dir="@{destdir}" files="${javac.includes}"/>
12.209 + </path>
12.210 + <globmapper from="*.java" to="*.class"/>
12.211 + </pathconvert>
12.212 + <delete>
12.213 + <files includes="${javac.includes.binary}"/>
12.214 + </delete>
12.215 + </sequential>
12.216 + </macrodef>
12.217 + </target>
12.218 + <target name="-init-macrodef-scalac">
12.219 + <macrodef name="scalac" uri="http://www.netbeans.org/ns/scala-project/1">
12.220 + <attribute default="${src.dir}" name="srcdir"/>
12.221 + <attribute default="${build.classes.dir}" name="destdir"/>
12.222 + <attribute default="${javac.classpath}" name="classpath"/>
12.223 + <attribute default="${includes}" name="includes"/>
12.224 + <attribute default="${excludes}" name="excludes"/>
12.225 + <attribute default="${javac.compilerargs}" name="addparams"/>
12.226 + <attribute default="" name="sourcepath"/>
12.227 + <element name="customize" optional="true"/>
12.228 + <sequential>
12.229 + <fsc addparams="@{addparams}" destdir="@{destdir}" encoding="${source.encoding}" excludes="@{excludes}" includes="@{includes}" sourcepath="@{sourcepath}" srcdir="@{srcdir}" target="jvm-${javac.target}">
12.230 + <classpath>
12.231 + <path path="@{classpath}"/>
12.232 + <fileset dir="${scala.lib}">
12.233 + <include name="**/*.jar"/>
12.234 + </fileset>
12.235 + </classpath>
12.236 + <customize/>
12.237 + </fsc>
12.238 + </sequential>
12.239 + </macrodef>
12.240 + <macrodef name="depend" uri="http://www.netbeans.org/ns/scala-project/1">
12.241 + <attribute default="${src.dir}" name="srcdir"/>
12.242 + <attribute default="${build.classes.dir}" name="destdir"/>
12.243 + <attribute default="${javac.classpath}" name="classpath"/>
12.244 + <sequential>
12.245 + <depend cache="${build.dir}/depcache" destdir="@{destdir}" excludes="${excludes}" includes="${includes}" srcdir="@{srcdir}">
12.246 + <classpath>
12.247 + <path path="@{classpath}"/>
12.248 + </classpath>
12.249 + </depend>
12.250 + </sequential>
12.251 + </macrodef>
12.252 + <macrodef name="force-recompile" uri="http://www.netbeans.org/ns/scala-project/1">
12.253 + <attribute default="${build.classes.dir}" name="destdir"/>
12.254 + <sequential>
12.255 + <fail unless="javac.includes">Must set javac.includes</fail>
12.256 + <pathconvert pathsep="," property="javac.includes.binary">
12.257 + <path>
12.258 + <filelist dir="@{destdir}" files="${javac.includes}"/>
12.259 + </path>
12.260 + <globmapper from="*.scala" to="*.class"/>
12.261 + </pathconvert>
12.262 + <delete>
12.263 + <files includes="${javac.includes.binary}"/>
12.264 + </delete>
12.265 + </sequential>
12.266 + </macrodef>
12.267 + </target>
12.268 + <target name="-init-macrodef-junit">
12.269 + <macrodef name="junit" uri="http://www.netbeans.org/ns/scala-project/1">
12.270 + <attribute default="${includes}" name="includes"/>
12.271 + <attribute default="${excludes}" name="excludes"/>
12.272 + <attribute default="**" name="testincludes"/>
12.273 + <sequential>
12.274 + <junit dir="${work.dir}" errorproperty="tests.failed" failureproperty="tests.failed" fork="true" showoutput="true">
12.275 + <batchtest todir="${build.test.results.dir}">
12.276 + <fileset dir="${build.test.classes.dir}" excludes="@{excludes},${excludes}" includes="@{includes}">
12.277 + <filename name="@{testincludes}"/>
12.278 + </fileset>
12.279 + </batchtest>
12.280 + <classpath>
12.281 + <path path="${run.test.classpath}"/>
12.282 + <fileset dir="${scala.lib}">
12.283 + <include name="**/*.jar"/>
12.284 + </fileset>
12.285 + </classpath>
12.286 + <syspropertyset>
12.287 + <propertyref prefix="test-sys-prop."/>
12.288 + <mapper from="test-sys-prop.*" to="*" type="glob"/>
12.289 + </syspropertyset>
12.290 + <formatter type="brief" usefile="false"/>
12.291 + <formatter type="xml"/>
12.292 + <jvmarg line="${run.jvmargs}"/>
12.293 + </junit>
12.294 + </sequential>
12.295 + </macrodef>
12.296 + </target>
12.297 + <target name="-init-macrodef-nbjpda">
12.298 + <macrodef name="nbjpdastart" uri="http://www.netbeans.org/ns/scala-project/1">
12.299 + <attribute default="${main.class}" name="name"/>
12.300 + <attribute default="${debug.classpath}" name="classpath"/>
12.301 + <attribute default="" name="stopclassname"/>
12.302 + <sequential>
12.303 + <nbjpdastart addressproperty="jpda.address" name="@{name}" stopclassname="@{stopclassname}" transport="dt_socket">
12.304 + <classpath>
12.305 + <path path="@{classpath}"/>
12.306 + </classpath>
12.307 + </nbjpdastart>
12.308 + </sequential>
12.309 + </macrodef>
12.310 + <macrodef name="nbjpdareload" uri="http://www.netbeans.org/ns/scala-project/1">
12.311 + <attribute default="${build.classes.dir}" name="dir"/>
12.312 + <sequential>
12.313 + <nbjpdareload>
12.314 + <fileset dir="@{dir}" includes="${fix.includes}*.class"/>
12.315 + </nbjpdareload>
12.316 + </sequential>
12.317 + </macrodef>
12.318 + </target>
12.319 + <target name="-init-debug-args">
12.320 + <property name="version-output" value="java version "${ant.java.version}"/>
12.321 + <condition property="have-jdk-older-than-1.4">
12.322 + <or>
12.323 + <contains string="${version-output}" substring="java version "1.0"/>
12.324 + <contains string="${version-output}" substring="java version "1.1"/>
12.325 + <contains string="${version-output}" substring="java version "1.2"/>
12.326 + <contains string="${version-output}" substring="java version "1.3"/>
12.327 + </or>
12.328 + </condition>
12.329 + <condition else="-Xdebug" property="debug-args-line" value="-Xdebug -Xnoagent -Djava.compiler=none">
12.330 + <istrue value="${have-jdk-older-than-1.4}"/>
12.331 + </condition>
12.332 + </target>
12.333 + <target depends="-init-debug-args" name="-init-macrodef-debug">
12.334 + <macrodef name="debug" uri="http://www.netbeans.org/ns/scala-project/1">
12.335 + <attribute default="${main.class}" name="classname"/>
12.336 + <attribute default="${debug.classpath}" name="classpath"/>
12.337 + <element name="customize" optional="true"/>
12.338 + <sequential>
12.339 + <java classname="@{classname}" dir="${work.dir}" fork="true">
12.340 + <jvmarg line="${debug-args-line}"/>
12.341 + <jvmarg value="-Xrunjdwp:transport=dt_socket,address=${jpda.address}"/>
12.342 + <jvmarg line="${run.jvmargs}"/>
12.343 + <classpath>
12.344 + <path path="@{classpath}"/>
12.345 + <fileset dir="${scala.lib}">
12.346 + <include name="**/*.jar"/>
12.347 + </fileset>
12.348 + </classpath>
12.349 + <syspropertyset>
12.350 + <propertyref prefix="run-sys-prop."/>
12.351 + <mapper from="run-sys-prop.*" to="*" type="glob"/>
12.352 + </syspropertyset>
12.353 + <customize/>
12.354 + </java>
12.355 + </sequential>
12.356 + </macrodef>
12.357 + </target>
12.358 + <target name="-init-macrodef-java">
12.359 + <macrodef name="java" uri="http://www.netbeans.org/ns/scala-project/1">
12.360 + <attribute default="${main.class}" name="classname"/>
12.361 + <element name="customize" optional="true"/>
12.362 + <sequential>
12.363 + <java classname="@{classname}" dir="${work.dir}" fork="true">
12.364 + <jvmarg line="${run.jvmargs}"/>
12.365 + <classpath>
12.366 + <path path="${run.classpath}"/>
12.367 + <fileset dir="${scala.lib}">
12.368 + <include name="**/*.jar"/>
12.369 + </fileset>
12.370 + </classpath>
12.371 + <syspropertyset>
12.372 + <propertyref prefix="run-sys-prop."/>
12.373 + <mapper from="run-sys-prop.*" to="*" type="glob"/>
12.374 + </syspropertyset>
12.375 + <customize/>
12.376 + </java>
12.377 + </sequential>
12.378 + </macrodef>
12.379 + </target>
12.380 + <target name="-init-presetdef-jar">
12.381 + <presetdef name="jar" uri="http://www.netbeans.org/ns/scala-project/1">
12.382 + <jar compress="${jar.compress}" jarfile="${dist.jar}">
12.383 + <scalaProject1:fileset dir="${build.classes.dir}"/>
12.384 + </jar>
12.385 + </presetdef>
12.386 + </target>
12.387 + <target depends="-pre-init,-init-private ,-init-user,-init-project,-do-init,-post-init,-init-check,-init-macrodef-property,-init-macrodef-javac,-init-macrodef-scalac,-init-macrodef-junit,-init-macrodef-nbjpda,-init-macrodef-debug,-init-macrodef-java,-init-presetdef-jar" name="init"/>
12.388 + <!--
12.389 + ===================
12.390 + COMPILATION SECTION
12.391 + ===================
12.392 + -->
12.393 + <target depends="init" name="deps-jar" unless="no.deps">
12.394 + <ant antfile="${project.jEdit}/build-nb.xml" inheritall="false" target="build"/>
12.395 + </target>
12.396 + <target depends="init,deps-jar" name="-pre-pre-compile">
12.397 + <mkdir dir="${build.classes.dir}"/>
12.398 + </target>
12.399 + <target name="-pre-compile">
12.400 + <!-- Empty placeholder for easier customization. -->
12.401 + <!-- You can override this target in the ../build.xml file. -->
12.402 + </target>
12.403 + <target if="do.depend.true" name="-compile-depend">
12.404 + <scalaProject1:depend/>
12.405 + </target>
12.406 + <target depends="init,deps-jar,-pre-pre-compile,-pre-compile,-compile-depend" if="have.sources" name="-do-compile">
12.407 + <scalaProject1:scalac/>
12.408 + <scalaProject1:javac/>
12.409 + <copy todir="${build.classes.dir}">
12.410 + <fileset dir="${src.dir}" excludes="${build.classes.excludes},${excludes} " includes="${includes}"/>
12.411 + </copy>
12.412 + </target>
12.413 + <target name="-post-compile">
12.414 + <!-- Empty placeholder for easier customization. -->
12.415 + <!-- You can override this target in the ../build.xml file. -->
12.416 + </target>
12.417 + <target depends="init,deps-jar,-pre-pre-compile,-pre-compile,-do-compile,-post-compile" description="Compile project." name="compile"/>
12.418 + <target name="-pre-compile-single">
12.419 + <!-- Empty placeholder for easier customization. -->
12.420 + <!-- You can override this target in the ../build.xml file. -->
12.421 + </target>
12.422 + <target depends="init,deps-jar,-pre-pre-compile" name="-do-compile-single">
12.423 + <fail unless="javac.includes">Must select some files in the IDE or set javac.includes</fail>
12.424 + <scalaProject1:force-recompile/>
12.425 + <scalaProject1:scalac excludes="" includes="${javac.includes}" sourcepath="${src.dir}"/>
12.426 + </target>
12.427 + <target name="-post-compile-single">
12.428 + <!-- Empty placeholder for easier customization. -->
12.429 + <!-- You can override this target in the ../build.xml file. -->
12.430 + </target>
12.431 + <target depends="init,deps-jar,-pre-pre-compile,-pre-compile-single,-do-compile-single,-post-compile-single" name="compile-single"/>
12.432 + <!--
12.433 + ====================
12.434 + JAR BUILDING SECTION
12.435 + ====================
12.436 + -->
12.437 + <target depends="init" name="-pre-pre-jar">
12.438 + <dirname file="${dist.jar}" property="dist.jar.dir"/>
12.439 + <mkdir dir="${dist.jar.dir}"/>
12.440 + </target>
12.441 + <target name="-pre-jar">
12.442 + <!-- Empty placeholder for easier customization. -->
12.443 + <!-- You can override this target in the ../build.xml file. -->
12.444 + </target>
12.445 + <target depends="init,compile,-pre-pre-jar,-pre-jar" name="-do-jar-without-manifest" unless="manifest.available">
12.446 + <scalaProject1:jar/>
12.447 + </target>
12.448 + <target depends="init,compile,-pre-pre-jar,-pre-jar" if="manifest.available" name="-do-jar-with-manifest" unless="manifest.available+main.class">
12.449 + <scalaProject1:jar manifest="${manifest.file}"/>
12.450 + </target>
12.451 + <target depends="init,compile,-pre-pre-jar,-pre-jar" if="manifest.available+main.class" name="-do-jar-with-mainclass" unless="manifest.available+main.class+mkdist.available">
12.452 + <scalaProject1:jar manifest="${manifest.file}">
12.453 + <scalaProject1:manifest>
12.454 + <scalaProject1:attribute name="Main-Class" value="${main.class}"/>
12.455 + </scalaProject1:manifest>
12.456 + </scalaProject1:jar>
12.457 + <echo>To run this application from the command line without Ant, try:</echo>
12.458 + <property location="${build.classes.dir}" name="build.classes.dir.resolved"/>
12.459 + <property location="${dist.jar}" name="dist.jar.resolved"/>
12.460 + <pathconvert property="run.classpath.with.dist.jar">
12.461 + <path path="${run.classpath}"/>
12.462 + <map from="${build.classes.dir.resolved}" to="${dist.jar.resolved}"/>
12.463 + </pathconvert>
12.464 + <echo>java -cp "${run.classpath.with.dist.jar}" ${main.class}
12.465 + </echo>
12.466 + </target>
12.467 + <target depends="init,compile,-pre-pre-jar,-pre-jar" if="manifest.available+main.class+mkdist.available" name="-do-jar-with-libraries">
12.468 + <property location="${build.classes.dir}" name="build.classes.dir.resolved"/>
12.469 + <pathconvert property="run.classpath.without.build.classes.dir">
12.470 + <path path="${run.classpath}"/>
12.471 + <map from="${build.classes.dir.resolved}" to=""/>
12.472 + </pathconvert>
12.473 + <pathconvert pathsep=" " property="jar.classpath">
12.474 + <path path="${run.classpath.without.build.classes.dir}"/>
12.475 + <chainedmapper>
12.476 + <flattenmapper/>
12.477 + <globmapper from="*" to="lib/*"/>
12.478 + </chainedmapper>
12.479 + </pathconvert>
12.480 + <taskdef classname="org.netbeans.modules.java.j2seproject.copylibstask.CopyLibs" classpath="${libs.CopyLibs.classpath}" name="copylibs"/>
12.481 + <copylibs compress="${jar.compress}" jarfile="${dist.jar}" manifest="${manifest.file}" runtimeclasspath="${run.classpath.without.build.classes.dir}">
12.482 + <fileset dir="${build.classes.dir}"/>
12.483 + <manifest>
12.484 + <attribute name="Main-Class" value="${main.class}"/>
12.485 + <attribute name="Class-Path" value="${jar.classpath}"/>
12.486 + </manifest>
12.487 + </copylibs>
12.488 + <echo>To run this application from the command line without Ant, try:</echo>
12.489 + <property location="${dist.jar}" name="dist.jar.resolved"/>
12.490 + <echo>java -jar "${dist.jar.resolved}"
12.491 + </echo>
12.492 + </target>
12.493 + <target name="-post-jar">
12.494 + <!-- Empty placeholder for easier customization. -->
12.495 + <!-- You can override this target in the ../build.xml file. -->
12.496 + </target>
12.497 + <target depends="init,compile,-pre-jar,-do-jar-with-manifest,-do-jar-without-manifest,-do-jar-with-mainclass,-do-jar-with-libraries,-post-jar" description="Build JAR." name="jar"/>
12.498 + <!--
12.499 + =================
12.500 + EXECUTION SECTION
12.501 + =================
12.502 + -->
12.503 + <target depends="init,compile" description="Run a main class." name="run">
12.504 + <scalaProject1:java>
12.505 + <customize>
12.506 + <arg line="${application.args}"/>
12.507 + </customize>
12.508 + </scalaProject1:java>
12.509 + </target>
12.510 + <target name="-do-not-recompile">
12.511 + <property name="javac.includes.binary" value=""/>
12.512 + </target>
12.513 + <target depends="init,-do-not-recompile,compile-single" name="run-single">
12.514 + <fail unless="run.class">Must select one file in the IDE or set run.class</fail>
12.515 + <scalaProject1:java classname="${run.class}"/>
12.516 + </target>
12.517 + <!--
12.518 + =================
12.519 + DEBUGGING SECTION
12.520 + =================
12.521 + -->
12.522 + <target depends="init" if="netbeans.home" name="-debug-start-debugger">
12.523 + <scalaProject1:nbjpdastart name="${debug.class}"/>
12.524 + </target>
12.525 + <target depends="init,compile" name="-debug-start-debuggee">
12.526 + <scalaProject1:debug>
12.527 + <customize>
12.528 + <arg line="${application.args}"/>
12.529 + </customize>
12.530 + </scalaProject1:debug>
12.531 + </target>
12.532 + <target depends="init,compile,-debug-start-debugger,-debug-start-debuggee" description="Debug project in IDE." if="netbeans.home" name="debug"/>
12.533 + <target depends="init" if="netbeans.home" name="-debug-start-debugger-stepinto">
12.534 + <scalaProject1:nbjpdastart stopclassname="${main.class}"/>
12.535 + </target>
12.536 + <target depends="init,compile,-debug-start-debugger-stepinto,-debug-start-debuggee" if="netbeans.home" name="debug-stepinto"/>
12.537 + <target depends="init,compile-single" if="netbeans.home" name="-debug-start-debuggee-single">
12.538 + <fail unless="debug.class">Must select one file in the IDE or set debug.class</fail>
12.539 + <scalaProject1:debug classname="${debug.class}"/>
12.540 + </target>
12.541 + <target depends="init,-do-not-recompile,compile-single,-debug-start-debugger,-debug-start-debuggee-single" if="netbeans.home" name="debug-single"/>
12.542 + <target depends="init" name="-pre-debug-fix">
12.543 + <fail unless="fix.includes">Must set fix.includes</fail>
12.544 + <property name="javac.includes" value="${fix.includes}.java"/>
12.545 + </target>
12.546 + <target depends="init,-pre-debug-fix,compile-single" if="netbeans.home" name="-do-debug-fix">
12.547 + <scalaProject1:nbjpdareload/>
12.548 + </target>
12.549 + <target depends="init,-pre-debug-fix,-do-debug-fix" if="netbeans.home" name="debug-fix"/>
12.550 + <!--
12.551 + ===============
12.552 + JAVADOC SECTION
12.553 + ===============
12.554 + -->
12.555 + <target depends="init" name="-javadoc-build">
12.556 + <mkdir dir="${dist.javadoc.dir}"/>
12.557 + <javadoc additionalparam="${javadoc.additionalparam}" author="${javadoc.author}" charset="UTF-8" destdir="${dist.javadoc.dir}" docencoding="UTF-8" encoding="${javadoc.encoding.used}" failonerror="true" noindex="${javadoc.noindex}" nonavbar="${javadoc.nonavbar}" notree="${javadoc.notree}" private="${javadoc.private}" source="${javac.source}" splitindex="${javadoc.splitindex}" use="${javadoc.use}" useexternalfile="true" version="${javadoc.version}" windowtitle="${javadoc.windowtitle}">
12.558 + <classpath>
12.559 + <path path="${javac.classpath}"/>
12.560 + </classpath>
12.561 + <fileset dir="${src.dir}" excludes="${excludes}" includes="${includes}">
12.562 + <filename name="**/*.java"/>
12.563 + </fileset>
12.564 + </javadoc>
12.565 + </target>
12.566 + <target depends="init,-javadoc-build" if="netbeans.home" name="-javadoc-browse" unless="no.javadoc.preview">
12.567 + <nbbrowse file="${dist.javadoc.dir}/index.html"/>
12.568 + </target>
12.569 + <target depends="init,-javadoc-build,-javadoc-browse" description="Build Javadoc." name="javadoc"/>
12.570 + <!--
12.571 + =========================
12.572 + JUNIT COMPILATION SECTION
12.573 + =========================
12.574 + -->
12.575 + <target depends="init,compile" if="have.tests" name="-pre-pre-compile-test">
12.576 + <mkdir dir="${build.test.classes.dir}"/>
12.577 + </target>
12.578 + <target name="-pre-compile-test">
12.579 + <!-- Empty placeholder for easier customization. -->
12.580 + <!-- You can override this target in the ../build.xml file. -->
12.581 + </target>
12.582 + <target if="do.depend.true" name="-compile-test-depend">
12.583 + <scalaProject1:depend classpath="${javac.test.classpath}" destdir="${build.test.classes.dir}" srcdir=""/>
12.584 + </target>
12.585 + <target depends="init,compile,-pre-pre-compile-test,-pre-compile-test,-compile-test-depend" if="have.tests" name="-do-compile-test">
12.586 + <scalaProject1:scalac classpath="${javac.test.classpath}" debug="true" destdir="${build.test.classes.dir}" srcdir=""/>
12.587 + <copy todir="${build.test.classes.dir}"/>
12.588 + </target>
12.589 + <target name="-post-compile-test">
12.590 + <!-- Empty placeholder for easier customization. -->
12.591 + <!-- You can override this target in the ../build.xml file. -->
12.592 + </target>
12.593 + <target depends="init,compile,-pre-pre-compile-test,-pre-compile-test,-do-compile-test,-post-compile-test" name="compile-test"/>
12.594 + <target name="-pre-compile-test-single">
12.595 + <!-- Empty placeholder for easier customization. -->
12.596 + <!-- You can override this target in the ../build.xml file. -->
12.597 + </target>
12.598 + <target depends="init,compile,-pre-pre-compile-test,-pre-compile-test-single" if="have.tests" name="-do-compile-test-single">
12.599 + <fail unless="javac.includes">Must select some files in the IDE or set javac.includes</fail>
12.600 + <scalaProject1:force-recompile destdir="${build.test.classes.dir}"/>
12.601 + <scalaProject1:scalac classpath="${javac.test.classpath}" debug="true" destdir="${build.test.classes.dir}" excludes="" includes="${javac.includes}" sourcepath="" srcdir=""/>
12.602 + <copy todir="${build.test.classes.dir}"/>
12.603 + </target>
12.604 + <target name="-post-compile-test-single">
12.605 + <!-- Empty placeholder for easier customization. -->
12.606 + <!-- You can override this target in the ../build.xml file. -->
12.607 + </target>
12.608 + <target depends="init,compile,-pre-pre-compile-test,-pre-compile-test-single,-do-compile-test-single,-post-compile-test-single" name="compile-test-single"/>
12.609 + <!--
12.610 + =======================
12.611 + JUNIT EXECUTION SECTION
12.612 + =======================
12.613 + -->
12.614 + <target depends="init" if="have.tests" name="-pre-test-run">
12.615 + <mkdir dir="${build.test.results.dir}"/>
12.616 + </target>
12.617 + <target depends="init,compile-test,-pre-test-run" if="have.tests" name="-do-test-run">
12.618 + <scalaProject1:junit testincludes="**/*Test.class"/>
12.619 + </target>
12.620 + <target depends="init,compile-test,-pre-test-run,-do-test-run" if="have.tests" name="-post-test-run">
12.621 + <fail if="tests.failed">Some tests failed; see details above.</fail>
12.622 + </target>
12.623 + <target depends="init" if="have.tests" name="test-report"/>
12.624 + <target depends="init" if="netbeans.home+have.tests" name="-test-browse"/>
12.625 + <target depends="init,compile-test,-pre-test-run,-do-test-run,test-report,-post-test-run,-test-browse" description="Run unit tests." name="test"/>
12.626 + <target depends="init" if="have.tests" name="-pre-test-run-single">
12.627 + <mkdir dir="${build.test.results.dir}"/>
12.628 + </target>
12.629 + <target depends="init,compile-test-single,-pre-test-run-single" if="have.tests" name="-do-test-run-single">
12.630 + <fail unless="test.includes">Must select some files in the IDE or set test.includes</fail>
12.631 + <scalaProject1:junit excludes="" includes="${test.includes}"/>
12.632 + </target>
12.633 + <target depends="init,compile-test-single,-pre-test-run-single,-do-test-run-single" if="have.tests" name="-post-test-run-single">
12.634 + <fail if="tests.failed">Some tests failed; see details above.</fail>
12.635 + </target>
12.636 + <target depends="init,-do-not-recompile,compile-test-single,-pre-test-run-single,-do-test-run-single,-post-test-run-single" description="Run single unit test." name="test-single"/>
12.637 + <!--
12.638 + =======================
12.639 + JUNIT DEBUGGING SECTION
12.640 + =======================
12.641 + -->
12.642 + <target depends="init,compile-test" if="have.tests" name="-debug-start-debuggee-test">
12.643 + <fail unless="test.class">Must select one file in the IDE or set test.class</fail>
12.644 + <property location="${build.test.results.dir}/TEST-${test.class}.xml" name="test.report.file"/>
12.645 + <delete file="${test.report.file}"/>
12.646 + <mkdir dir="${build.test.results.dir}"/>
12.647 + <scalaProject1:debug classname="org.apache.tools.ant.taskdefs.optional.junit.JUnitTestRunner" classpath="${ant.home}/lib/ant.jar:${ant.home}/lib/ant-junit.jar:${debug.test.classpath}">
12.648 + <customize>
12.649 + <syspropertyset>
12.650 + <propertyref prefix="test-sys-prop."/>
12.651 + <mapper from="test-sys-prop.*" to="*" type="glob"/>
12.652 + </syspropertyset>
12.653 + <arg value="${test.class}"/>
12.654 + <arg value="showoutput=true"/>
12.655 + <arg value="formatter=org.apache.tools.ant.taskdefs.optional.junit.BriefJUnitResultFormatter"/>
12.656 + <arg value="formatter=org.apache.tools.ant.taskdefs.optional.junit.XMLJUnitResultFormatter,${test.report.file}"/>
12.657 + </customize>
12.658 + </scalaProject1:debug>
12.659 + </target>
12.660 + <target depends="init,compile-test" if="netbeans.home+have.tests" name="-debug-start-debugger-test">
12.661 + <scalaProject1:nbjpdastart classpath="${debug.test.classpath}" name="${test.class}"/>
12.662 + </target>
12.663 + <target depends="init,-do-not-recompile,compile-test-single,-debug-start-debugger-test,-debug-start-debuggee-test" name="debug-test"/>
12.664 + <target depends="init,-pre-debug-fix,compile-test-single" if="netbeans.home" name="-do-debug-fix-test">
12.665 + <scalaProject1:nbjpdareload dir="${build.test.classes.dir}"/>
12.666 + </target>
12.667 + <target depends="init,-pre-debug-fix,-do-debug-fix-test" if="netbeans.home" name="debug-fix-test"/>
12.668 + <!--
12.669 + =========================
12.670 + APPLET EXECUTION SECTION
12.671 + =========================
12.672 + -->
12.673 + <target depends="init,compile-single" name="run-applet">
12.674 + <fail unless="applet.url">Must select one file in the IDE or set applet.url</fail>
12.675 + <scalaProject1:java classname="sun.applet.AppletViewer">
12.676 + <customize>
12.677 + <arg value="${applet.url}"/>
12.678 + </customize>
12.679 + </scalaProject1:java>
12.680 + </target>
12.681 + <!--
12.682 + =========================
12.683 + APPLET DEBUGGING SECTION
12.684 + =========================
12.685 + -->
12.686 + <target depends="init,compile-single" if="netbeans.home" name="-debug-start-debuggee-applet">
12.687 + <fail unless="applet.url">Must select one file in the IDE or set applet.url</fail>
12.688 + <scalaProject1:debug classname="sun.applet.AppletViewer">
12.689 + <customize>
12.690 + <arg value="${applet.url}"/>
12.691 + </customize>
12.692 + </scalaProject1:debug>
12.693 + </target>
12.694 + <target depends="init,compile-single,-debug-start-debugger,-debug-start-debuggee-applet" if="netbeans.home" name="debug-applet"/>
12.695 + <!--
12.696 + ===============
12.697 + CLEANUP SECTION
12.698 + ===============
12.699 + -->
12.700 + <target depends="init" name="deps-clean" unless="no.deps">
12.701 + <ant antfile="${project.jEdit}/build-nb.xml" inheritall="false" target="clean"/>
12.702 + </target>
12.703 + <target depends="init" name="-do-clean">
12.704 + <delete dir="${build.dir}"/>
12.705 + <delete dir="${dist.dir}"/>
12.706 + </target>
12.707 + <target name="-post-clean">
12.708 + <!-- Empty placeholder for easier customization. -->
12.709 + <!-- You can override this target in the ../build.xml file. -->
12.710 + </target>
12.711 + <target depends="init,deps-clean,-do-clean,-post-clean" description="Clean build products." name="clean"/>
12.712 +</project>
13.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
13.2 +++ b/src/Tools/jEdit/nbproject/genfiles.properties Mon Jan 11 22:31:27 2010 +0100
13.3 @@ -0,0 +1,8 @@
13.4 +build.xml.data.CRC32=d2379ac2
13.5 +build.xml.script.CRC32=2db9d955
13.6 +build.xml.stylesheet.CRC32=ca9d572e
13.7 +# This file is used by a NetBeans-based IDE to track changes in generated files such as build-impl.xml.
13.8 +# Do not edit this file. You may delete it but then the IDE will never regenerate such files for you.
13.9 +nbproject/build-impl.xml.data.CRC32=8f41dcce
13.10 +nbproject/build-impl.xml.script.CRC32=69f2059c
13.11 +nbproject/build-impl.xml.stylesheet.CRC32=bc42a706@1.3.0
14.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
14.2 +++ b/src/Tools/jEdit/nbproject/project.properties Mon Jan 11 22:31:27 2010 +0100
14.3 @@ -0,0 +1,77 @@
14.4 +application.title=Isabelle-jEdit
14.5 +application.vendor=makarius
14.6 +application.args=-noserver -nobackground
14.7 +build.classes.dir=${build.dir}/classes
14.8 +build.classes.excludes=**/*.java,**/*.form,**/*.scala
14.9 +# This directory is removed when the project is cleaned:
14.10 +build.dir=build
14.11 +build.generated.dir=${build.dir}/generated
14.12 +# Only compile against the classpath explicitly listed here:
14.13 +build.sysclasspath=ignore
14.14 +build.test.classes.dir=${build.dir}/test/classes
14.15 +build.test.results.dir=${build.dir}/test/results
14.16 +debug.classpath=\
14.17 + ${run.classpath}
14.18 +debug.test.classpath=\
14.19 + ${run.test.classpath}
14.20 +# This directory is removed when the project is cleaned:
14.21 +dist.dir=dist
14.22 +# dist can be used as jEdits settings-directory;
14.23 +# jEdit searches for plugins in the 'jars' subdirectory
14.24 +# must include something like this to private.properties:
14.25 +# application.args=-noserver -nobackground -settings=/absolute/path/to/project/dist
14.26 +#
14.27 +dist.jar=${dist.dir}/jars/Isabelle-jEdit.jar
14.28 +dist.javadoc.dir=${dist.dir}/javadoc
14.29 +excludes=
14.30 +file.reference.isabelle-jedit-src=src
14.31 +file.reference.jedit.jar=/home/makarius/lib/jedit/current/jedit.jar
14.32 +includes=**
14.33 +jar.compress=false
14.34 +java.platform.active=java_default_platform
14.35 +javac.classpath=\
14.36 + ${reference.jEdit.build}:\
14.37 + ${libs.Isabelle-Pure.classpath}:\
14.38 + ${libs.Cobra-Renderer.classpath}:\
14.39 + ${libs.Rhino-JavaScript.classpath}:\
14.40 + ${libs.ErrorList.classpath}:\
14.41 + ${libs.Hyperlinks.classpath}:\
14.42 + ${libs.SideKick.classpath}:\
14.43 + ${libs.Console.classpath}:\
14.44 + ${libs.Scala-compiler.classpath}
14.45 +# Space-separated list of extra javac options
14.46 +javac.compilerargs=
14.47 +javac.deprecation=false
14.48 +javac.source=1.5
14.49 +javac.target=1.5
14.50 +javac.test.classpath=\
14.51 + ${javac.classpath}:\
14.52 + ${build.classes.dir}:\
14.53 + ${libs.junit.classpath}:\
14.54 + ${libs.junit_4.classpath}
14.55 +javadoc.additionalparam=
14.56 +javadoc.author=false
14.57 +javadoc.encoding=${source.encoding}
14.58 +javadoc.noindex=false
14.59 +javadoc.nonavbar=false
14.60 +javadoc.notree=false
14.61 +javadoc.private=false
14.62 +javadoc.splitindex=true
14.63 +javadoc.use=true
14.64 +javadoc.version=false
14.65 +javadoc.windowtitle=
14.66 +main.class=org.gjt.sp.jedit.jEdit
14.67 +manifest.file=manifest.mf
14.68 +meta.inf.dir=${src.dir}/META-INF
14.69 +platform.active=default_platform
14.70 +project.jEdit=contrib/jEdit
14.71 +reference.jEdit.build=${project.jEdit}/build/jEdit.jar
14.72 +run.classpath=\
14.73 + ${javac.classpath}:\
14.74 + ${build.classes.dir}
14.75 +run.jvmargs=-Xms128m -Xmx512m
14.76 +run.test.classpath=\
14.77 + ${javac.test.classpath}:\
14.78 + ${build.test.classes.dir}
14.79 +source.encoding=UTF-8
14.80 +src.dir=${file.reference.isabelle-jedit-src}
15.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
15.2 +++ b/src/Tools/jEdit/nbproject/project.xml Mon Jan 11 22:31:27 2010 +0100
15.3 @@ -0,0 +1,24 @@
15.4 +<?xml version="1.0" encoding="UTF-8"?>
15.5 +<project xmlns="http://www.netbeans.org/ns/project/1">
15.6 + <type>org.netbeans.modules.scala.project</type>
15.7 + <configuration>
15.8 + <data xmlns="http://www.netbeans.org/ns/scala-project/1">
15.9 + <name>Isabelle-jEdit</name>
15.10 + <minimum-ant-version>1.6.5</minimum-ant-version>
15.11 + <source-roots>
15.12 + <root id="src.dir"/>
15.13 + </source-roots>
15.14 + <test-roots/>
15.15 + </data>
15.16 + <references xmlns="http://www.netbeans.org/ns/ant-project-references/1">
15.17 + <reference>
15.18 + <foreign-project>jEdit</foreign-project>
15.19 + <artifact-type>jar</artifact-type>
15.20 + <script>build-nb.xml</script>
15.21 + <target>build</target>
15.22 + <clean-target>clean</clean-target>
15.23 + <id>build</id>
15.24 + </reference>
15.25 + </references>
15.26 + </configuration>
15.27 +</project>
16.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
16.2 +++ b/src/Tools/jEdit/plugin/Isabelle.props Mon Jan 11 22:31:27 2010 +0100
16.3 @@ -0,0 +1,48 @@
16.4 +## Isabelle plugin properties
16.5 +##
16.6 +##:encoding=ISO-8859-1:
16.7 +
16.8 +#identification
16.9 +plugin.isabelle.jedit.Plugin.name=Isabelle
16.10 +plugin.isabelle.jedit.Plugin.author=Johannes Hölzl, Fabian Immler, Makarius Wenzel
16.11 +plugin.isabelle.jedit.Plugin.version=0.0.1
16.12 +plugin.isabelle.jedit.Plugin.description=Isabelle/Isar asynchronous proof processing
16.13 +
16.14 +#system parameters
16.15 +plugin.isabelle.jedit.Plugin.activate=startup
16.16 +plugin.isabelle.jedit.Plugin.usePluginHome=false
16.17 +
16.18 +#dependencies
16.19 +plugin.isabelle.jedit.Plugin.depend.0=jdk 1.6
16.20 +plugin.isabelle.jedit.Plugin.depend.1=jedit 04.03.17.00
16.21 +plugin.isabelle.jedit.Plugin.depend.2=plugin errorlist.ErrorListPlugin 1.7
16.22 +plugin.isabelle.jedit.Plugin.depend.3=plugin sidekick.SideKickPlugin 0.7.6
16.23 +plugin.isabelle.jedit.Plugin.depend.4=plugin gatchan.jedit.hyperlinks.HyperlinksPlugin 1.0.1
16.24 +
16.25 +#options
16.26 +plugin.isabelle.jedit.Plugin.option-pane=isabelle
16.27 +options.isabelle.label=Isabelle
16.28 +options.isabelle.code=new isabelle.jedit.Isabelle_Options();
16.29 +options.isabelle.logic.title=Logic
16.30 +options.isabelle.font-size.title=Font Size
16.31 +options.isabelle.font-size=14
16.32 +options.isabelle.startup-timeout=10000
16.33 +
16.34 +#menu actions
16.35 +plugin.isabelle.jedit.Plugin.menu.label=Isabelle
16.36 +plugin.isabelle.jedit.Plugin.menu=isabelle.activate isabelle.show-output isabelle.show-protocol
16.37 +isabelle.activate.label=Activate current buffer
16.38 +isabelle.show-output.label=Show Output
16.39 +isabelle.show-protocol.label=Show Protocol
16.40 +
16.41 +#dockables
16.42 +isabelle-output.title=Output
16.43 +isabelle-protocol.title=Protocol
16.44 +
16.45 +#SideKick
16.46 +sidekick.parser.isabelle.label=Isabelle
16.47 +mode.isabelle.sidekick.parser=isabelle
16.48 +mode.ml.sidekick.parser=isabelle
16.49 +
16.50 +#Hyperlinks
16.51 +mode.isabelle.hyperlink.source=isabelle
17.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
17.2 +++ b/src/Tools/jEdit/plugin/actions.xml Mon Jan 11 22:31:27 2010 +0100
17.3 @@ -0,0 +1,23 @@
17.4 +<?xml version="1.0"?>
17.5 +<!DOCTYPE ACTIONS SYSTEM "actions.dtd">
17.6 +
17.7 +<ACTIONS>
17.8 + <ACTION NAME="isabelle.activate">
17.9 + <CODE>
17.10 + isabelle.jedit.Isabelle.switch_active(view);
17.11 + </CODE>
17.12 + <IS_SELECTED>
17.13 + return isabelle.jedit.Isabelle.is_active(view);
17.14 + </IS_SELECTED>
17.15 + </ACTION>
17.16 + <ACTION NAME="isabelle.show-output">
17.17 + <CODE>
17.18 + wm.addDockableWindow("isabelle-output");
17.19 + </CODE>
17.20 + </ACTION>
17.21 + <ACTION NAME="isabelle.show-protocol">
17.22 + <CODE>
17.23 + wm.addDockableWindow("isabelle-protocol");
17.24 + </CODE>
17.25 + </ACTION>
17.26 +</ACTIONS>
17.27 \ No newline at end of file
18.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
18.2 +++ b/src/Tools/jEdit/plugin/dockables.xml Mon Jan 11 22:31:27 2010 +0100
18.3 @@ -0,0 +1,11 @@
18.4 +<?xml version="1.0"?>
18.5 +<!DOCTYPE DOCKABLES SYSTEM "dockables.dtd">
18.6 +
18.7 +<DOCKABLES>
18.8 + <DOCKABLE NAME="isabelle-output" MOVABLE="TRUE">
18.9 + new isabelle.jedit.Output_Dockable(view, position);
18.10 + </DOCKABLE>
18.11 + <DOCKABLE NAME="isabelle-protocol" MOVABLE="TRUE">
18.12 + new isabelle.jedit.Protocol_Dockable(view, position);
18.13 + </DOCKABLE>
18.14 +</DOCKABLES>
18.15 \ No newline at end of file
19.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
19.2 +++ b/src/Tools/jEdit/plugin/services.xml Mon Jan 11 22:31:27 2010 +0100
19.3 @@ -0,0 +1,17 @@
19.4 +<?xml version="1.0"?>
19.5 +<!DOCTYPE SERVICES SYSTEM "services.dtd">
19.6 +
19.7 +<SERVICES>
19.8 + <SERVICE NAME="UTF-8-Isabelle" CLASS="org.gjt.sp.jedit.io.Encoding">
19.9 + new isabelle.jedit.Isabelle_Encoding();
19.10 + </SERVICE>
19.11 + <SERVICE NAME="isabelle" CLASS="sidekick.SideKickParser">
19.12 + new isabelle.jedit.Isabelle_Sidekick();
19.13 + </SERVICE>
19.14 + <SERVICE NAME="isabelle" CLASS="gatchan.jedit.hyperlinks.HyperlinkSource">
19.15 + new isabelle.jedit.Isabelle_Hyperlinks();
19.16 + </SERVICE>
19.17 + <SERVICE CLASS="console.Shell" NAME="Scala">
19.18 + new isabelle.jedit.Scala_Console();
19.19 + </SERVICE>
19.20 +</SERVICES>
20.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
20.2 +++ b/src/Tools/jEdit/src/Dummy.java Mon Jan 11 22:31:27 2010 +0100
20.3 @@ -0,0 +1,3 @@
20.4 +/* dummy class to make ant javadoc work */
20.5 +package isabelle;
20.6 +public class Dummy { }
21.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
21.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala Mon Jan 11 22:31:27 2010 +0100
21.3 @@ -0,0 +1,145 @@
21.4 +/*
21.5 + * Document model connected to jEdit buffer
21.6 + *
21.7 + * @author Fabian Immler, TU Munich
21.8 + * @author Makarius
21.9 + */
21.10 +
21.11 +package isabelle.jedit
21.12 +
21.13 +
21.14 +import isabelle.proofdocument.{Change, Command, Document, Session}
21.15 +
21.16 +import scala.actors.Actor, Actor._
21.17 +import scala.collection.mutable
21.18 +
21.19 +import org.gjt.sp.jedit.Buffer
21.20 +import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
21.21 +import org.gjt.sp.jedit.syntax.{ModeProvider, SyntaxStyle}
21.22 +
21.23 +
21.24 +object Document_Model
21.25 +{
21.26 + /* document model of buffer */
21.27 +
21.28 + private val key = "isabelle.document_model"
21.29 +
21.30 + def init(session: Session, buffer: Buffer): Document_Model =
21.31 + {
21.32 + Swing_Thread.assert()
21.33 + val model = new Document_Model(session, buffer)
21.34 + buffer.setProperty(key, model)
21.35 + model.activate()
21.36 + model
21.37 + }
21.38 +
21.39 + def apply(buffer: Buffer): Option[Document_Model] =
21.40 + {
21.41 + Swing_Thread.assert()
21.42 + buffer.getProperty(key) match {
21.43 + case model: Document_Model => Some(model)
21.44 + case _ => None
21.45 + }
21.46 + }
21.47 +
21.48 + def exit(buffer: Buffer)
21.49 + {
21.50 + Swing_Thread.assert()
21.51 + apply(buffer) match {
21.52 + case None => error("No document model for buffer: " + buffer)
21.53 + case Some(model) =>
21.54 + model.deactivate()
21.55 + buffer.unsetProperty(key)
21.56 + }
21.57 + }
21.58 +}
21.59 +
21.60 +class Document_Model(val session: Session, val buffer: Buffer)
21.61 +{
21.62 + /* history */
21.63 +
21.64 + private val document_0 = session.begin_document(buffer.getName)
21.65 +
21.66 + @volatile private var history = // owned by Swing thread
21.67 + new Change(document_0.id, None, Nil, Future.value(Nil, document_0))
21.68 +
21.69 + def current_change(): Change = history
21.70 + def recent_document(): Document = current_change().ancestors.find(_.is_assigned).get.join_document
21.71 +
21.72 +
21.73 + /* transforming offsets */
21.74 +
21.75 + private def changes_from(doc: Document): List[Text_Edit] =
21.76 + {
21.77 + Swing_Thread.assert()
21.78 + (edits_buffer.toList /:
21.79 + current_change.ancestors.takeWhile(_.id != doc.id))((edits, change) => change.edits ::: edits)
21.80 + }
21.81 +
21.82 + def from_current(doc: Document, offset: Int): Int =
21.83 + (offset /: changes_from(doc).reverse) ((i, change) => change before i)
21.84 +
21.85 + def to_current(doc: Document, offset: Int): Int =
21.86 + (offset /: changes_from(doc)) ((i, change) => change after i)
21.87 +
21.88 + def lines_of_command(doc: Document, cmd: Command): (Int, Int) =
21.89 + {
21.90 + val start = doc.command_start(cmd).get // FIXME total?
21.91 + val stop = start + cmd.length
21.92 + (buffer.getLineOfOffset(to_current(doc, start)),
21.93 + buffer.getLineOfOffset(to_current(doc, stop)))
21.94 + }
21.95 +
21.96 +
21.97 + /* text edits */
21.98 +
21.99 + private val edits_buffer = new mutable.ListBuffer[Text_Edit] // owned by Swing thread
21.100 +
21.101 + private val edits_delay = Swing_Thread.delay_last(300) {
21.102 + if (!edits_buffer.isEmpty) {
21.103 + val new_change = current_change().edit(session, edits_buffer.toList)
21.104 + edits_buffer.clear
21.105 + history = new_change
21.106 + new_change.result.map(_ => session.input(new_change))
21.107 + }
21.108 + }
21.109 +
21.110 +
21.111 + /* buffer listener */
21.112 +
21.113 + private val buffer_listener: BufferListener = new BufferAdapter
21.114 + {
21.115 + override def contentInserted(buffer: JEditBuffer,
21.116 + start_line: Int, offset: Int, num_lines: Int, length: Int)
21.117 + {
21.118 + edits_buffer += new Text_Edit(true, offset, buffer.getText(offset, length))
21.119 + edits_delay()
21.120 + }
21.121 +
21.122 + override def preContentRemoved(buffer: JEditBuffer,
21.123 + start_line: Int, start: Int, num_lines: Int, removed_length: Int)
21.124 + {
21.125 + edits_buffer += new Text_Edit(false, start, buffer.getText(start, removed_length))
21.126 + edits_delay()
21.127 + }
21.128 + }
21.129 +
21.130 +
21.131 + /* activation */
21.132 +
21.133 + def activate()
21.134 + {
21.135 + buffer.setTokenMarker(new Isabelle_Token_Marker(this))
21.136 + buffer.addBufferListener(buffer_listener)
21.137 + buffer.propertiesChanged()
21.138 +
21.139 + edits_buffer += new Text_Edit(true, 0, buffer.getText(0, buffer.getLength))
21.140 + edits_delay()
21.141 + }
21.142 +
21.143 + def deactivate()
21.144 + {
21.145 + buffer.setTokenMarker(buffer.getMode.getTokenMarker)
21.146 + buffer.removeBufferListener(buffer_listener)
21.147 + }
21.148 +}
22.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
22.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala Mon Jan 11 22:31:27 2010 +0100
22.3 @@ -0,0 +1,303 @@
22.4 +/*
22.5 + * Document view connected to jEdit text area
22.6 + *
22.7 + * @author Fabian Immler, TU Munich
22.8 + * @author Makarius
22.9 + */
22.10 +
22.11 +package isabelle.jedit
22.12 +
22.13 +
22.14 +import isabelle.proofdocument.{Command, Document, Session}
22.15 +
22.16 +import scala.actors.Actor._
22.17 +
22.18 +import java.awt.event.{MouseAdapter, MouseEvent}
22.19 +import java.awt.{BorderLayout, Graphics, Dimension, Color, Graphics2D}
22.20 +import javax.swing.{JPanel, ToolTipManager}
22.21 +import javax.swing.event.{CaretListener, CaretEvent}
22.22 +
22.23 +import org.gjt.sp.jedit.gui.RolloverButton
22.24 +import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
22.25 +
22.26 +
22.27 +object Document_View
22.28 +{
22.29 + def choose_color(command: Command, doc: Document): Color =
22.30 + {
22.31 + doc.current_state(command).map(_.status) match {
22.32 + case Some(Command.Status.UNPROCESSED) => new Color(255, 228, 225)
22.33 + case Some(Command.Status.FINISHED) => new Color(234, 248, 255)
22.34 + case Some(Command.Status.FAILED) => new Color(255, 193, 193)
22.35 + case _ => Color.red
22.36 + }
22.37 + }
22.38 +
22.39 +
22.40 + /* document view of text area */
22.41 +
22.42 + private val key = new Object
22.43 +
22.44 + def init(model: Document_Model, text_area: TextArea): Document_View =
22.45 + {
22.46 + Swing_Thread.assert()
22.47 + val doc_view = new Document_View(model, text_area)
22.48 + text_area.putClientProperty(key, doc_view)
22.49 + doc_view.activate()
22.50 + doc_view
22.51 + }
22.52 +
22.53 + def apply(text_area: TextArea): Option[Document_View] =
22.54 + {
22.55 + Swing_Thread.assert()
22.56 + text_area.getClientProperty(key) match {
22.57 + case doc_view: Document_View => Some(doc_view)
22.58 + case _ => None
22.59 + }
22.60 + }
22.61 +
22.62 + def exit(text_area: TextArea)
22.63 + {
22.64 + Swing_Thread.assert()
22.65 + apply(text_area) match {
22.66 + case None => error("No document view for text area: " + text_area)
22.67 + case Some(doc_view) =>
22.68 + doc_view.deactivate()
22.69 + text_area.putClientProperty(key, null)
22.70 + }
22.71 + }
22.72 +}
22.73 +
22.74 +
22.75 +class Document_View(model: Document_Model, text_area: TextArea)
22.76 +{
22.77 + private val session = model.session
22.78 +
22.79 +
22.80 + /* visible document -- owned by Swing thread */
22.81 +
22.82 + @volatile private var document = model.recent_document()
22.83 +
22.84 +
22.85 + /* buffer of changed commands -- owned by Swing thread */
22.86 +
22.87 + @volatile private var changed_commands: Set[Command] = Set()
22.88 +
22.89 + private val changed_delay = Swing_Thread.delay_first(100) {
22.90 + if (!changed_commands.isEmpty) {
22.91 + document = model.recent_document()
22.92 + for (cmd <- changed_commands if document.commands.contains(cmd)) { // FIXME cover doc states as well!!?
22.93 + update_syntax(cmd)
22.94 + invalidate_line(cmd)
22.95 + overview.repaint()
22.96 + }
22.97 + changed_commands = Set()
22.98 + }
22.99 + }
22.100 +
22.101 +
22.102 + /* command change actor */
22.103 +
22.104 + private case object Exit
22.105 +
22.106 + private val command_change_actor = actor {
22.107 + loop {
22.108 + react {
22.109 + case command: Command => // FIXME rough filtering according to document family!?
22.110 + Swing_Thread.now {
22.111 + changed_commands += command
22.112 + changed_delay()
22.113 + }
22.114 +
22.115 + case Exit => reply(()); exit()
22.116 +
22.117 + case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
22.118 + }
22.119 + }
22.120 + }
22.121 +
22.122 +
22.123 + /* text_area_extension */
22.124 +
22.125 + private val text_area_extension = new TextAreaExtension
22.126 + {
22.127 + override def paintValidLine(gfx: Graphics2D,
22.128 + screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
22.129 + {
22.130 + def from_current(pos: Int) = model.from_current(document, pos)
22.131 + def to_current(pos: Int) = model.to_current(document, pos)
22.132 + val metrics = text_area.getPainter.getFontMetrics
22.133 + val saved_color = gfx.getColor
22.134 + try {
22.135 + for ((command, command_start) <-
22.136 + document.command_range(from_current(start), from_current(end)))
22.137 + {
22.138 + val begin = start max to_current(command_start)
22.139 + val finish = (end - 1) min to_current(command_start + command.length)
22.140 + encolor(gfx, y, metrics.getHeight, begin, finish,
22.141 + Document_View.choose_color(command, document), true)
22.142 + }
22.143 + }
22.144 + finally { gfx.setColor(saved_color) }
22.145 + }
22.146 +
22.147 + override def getToolTipText(x: Int, y: Int): String =
22.148 + {
22.149 + val offset = model.from_current(document, text_area.xyToOffset(x, y))
22.150 + document.command_at(offset) match {
22.151 + case Some((command, command_start)) =>
22.152 + document.current_state(command).get.type_at(offset - command_start).getOrElse(null)
22.153 + case None => null
22.154 + }
22.155 + }
22.156 + }
22.157 +
22.158 +
22.159 + /* caret_listener */
22.160 +
22.161 + private var _selected_command: Command = null
22.162 + private def selected_command = _selected_command
22.163 + private def selected_command_=(cmd: Command)
22.164 + {
22.165 + _selected_command = cmd
22.166 + session.results.event(cmd)
22.167 + }
22.168 +
22.169 + private val caret_listener = new CaretListener
22.170 + {
22.171 + override def caretUpdate(e: CaretEvent)
22.172 + {
22.173 + document.command_at(e.getDot) match {
22.174 + case Some((command, command_start)) if (selected_command != command) =>
22.175 + selected_command = command
22.176 + case _ =>
22.177 + }
22.178 + }
22.179 + }
22.180 +
22.181 +
22.182 + /* (re)painting */
22.183 +
22.184 + private val update_delay = Swing_Thread.delay_first(500) { model.buffer.propertiesChanged() }
22.185 +
22.186 + private def update_syntax(cmd: Command)
22.187 + {
22.188 + val (line1, line2) = model.lines_of_command(document, cmd)
22.189 + if (line2 >= text_area.getFirstLine &&
22.190 + line1 <= text_area.getFirstLine + text_area.getVisibleLines)
22.191 + update_delay()
22.192 + }
22.193 +
22.194 + private def invalidate_line(cmd: Command) =
22.195 + {
22.196 + val (start, stop) = model.lines_of_command(document, cmd)
22.197 + text_area.invalidateLineRange(start, stop)
22.198 +
22.199 + if (selected_command == cmd)
22.200 + session.results.event(cmd)
22.201 + }
22.202 +
22.203 + private def invalidate_all() =
22.204 + text_area.invalidateLineRange(text_area.getFirstPhysicalLine,
22.205 + text_area.getLastPhysicalLine)
22.206 +
22.207 + private def encolor(gfx: Graphics2D,
22.208 + y: Int, height: Int, begin: Int, finish: Int, color: Color, fill: Boolean)
22.209 + {
22.210 + val start = text_area.offsetToXY(begin)
22.211 + val stop =
22.212 + if (finish < model.buffer.getLength) text_area.offsetToXY(finish)
22.213 + else {
22.214 + val p = text_area.offsetToXY(finish - 1)
22.215 + val metrics = text_area.getPainter.getFontMetrics
22.216 + p.x = p.x + (metrics.charWidth(' ') max metrics.getMaxAdvance)
22.217 + p
22.218 + }
22.219 +
22.220 + if (start != null && stop != null) {
22.221 + gfx.setColor(color)
22.222 + if (fill) gfx.fillRect(start.x, y, stop.x - start.x, height)
22.223 + else gfx.drawRect(start.x, y, stop.x - start.x, height)
22.224 + }
22.225 + }
22.226 +
22.227 +
22.228 + /* overview of command status left of scrollbar */
22.229 +
22.230 + private val overview = new JPanel(new BorderLayout)
22.231 + {
22.232 + private val WIDTH = 10
22.233 + private val HEIGHT = 2
22.234 +
22.235 + setPreferredSize(new Dimension(WIDTH, 0))
22.236 +
22.237 + setRequestFocusEnabled(false)
22.238 +
22.239 + addMouseListener(new MouseAdapter {
22.240 + override def mousePressed(event: MouseEvent) {
22.241 + val line = y_to_line(event.getY)
22.242 + if (line >= 0 && line < text_area.getLineCount)
22.243 + text_area.setCaretPosition(text_area.getLineStartOffset(line))
22.244 + }
22.245 + })
22.246 +
22.247 + override def addNotify() {
22.248 + super.addNotify()
22.249 + ToolTipManager.sharedInstance.registerComponent(this)
22.250 + }
22.251 +
22.252 + override def removeNotify() {
22.253 + ToolTipManager.sharedInstance.unregisterComponent(this)
22.254 + super.removeNotify
22.255 + }
22.256 +
22.257 + override def getToolTipText(event: MouseEvent): String =
22.258 + {
22.259 + val line = y_to_line(event.getY())
22.260 + if (line >= 0 && line < text_area.getLineCount) "<html><b>TODO:</b><br>Tooltip</html>"
22.261 + else ""
22.262 + }
22.263 +
22.264 + override def paintComponent(gfx: Graphics)
22.265 + {
22.266 + super.paintComponent(gfx)
22.267 + val buffer = model.buffer
22.268 +
22.269 + for ((command, start) <- document.command_range(0)) {
22.270 + val line1 = buffer.getLineOfOffset(model.to_current(document, start))
22.271 + val line2 = buffer.getLineOfOffset(model.to_current(document, start + command.length)) + 1
22.272 + val y = line_to_y(line1)
22.273 + val height = HEIGHT * (line2 - line1)
22.274 + gfx.setColor(Document_View.choose_color(command, document))
22.275 + gfx.fillRect(0, y, getWidth - 1, height)
22.276 + }
22.277 + }
22.278 +
22.279 + private def line_to_y(line: Int): Int =
22.280 + (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)
22.281 +
22.282 + private def y_to_line(y: Int): Int =
22.283 + (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight
22.284 + }
22.285 +
22.286 +
22.287 + /* activation */
22.288 +
22.289 + private def activate()
22.290 + {
22.291 + text_area.getPainter.
22.292 + addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
22.293 + text_area.addCaretListener(caret_listener)
22.294 + text_area.addLeftOfScrollBar(overview)
22.295 + session.command_change += command_change_actor
22.296 + }
22.297 +
22.298 + private def deactivate()
22.299 + {
22.300 + session.command_change -= command_change_actor
22.301 + command_change_actor !? Exit
22.302 + text_area.removeLeftOfScrollBar(overview)
22.303 + text_area.removeCaretListener(caret_listener)
22.304 + text_area.getPainter.removeExtension(text_area_extension)
22.305 + }
22.306 +}
22.307 \ No newline at end of file
23.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
23.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_encoding.scala Mon Jan 11 22:31:27 2010 +0100
23.3 @@ -0,0 +1,64 @@
23.4 +/*
23.5 + * Isabelle encoding -- based on utf-8
23.6 + *
23.7 + * @author Makarius
23.8 + */
23.9 +
23.10 +package isabelle.jedit
23.11 +
23.12 +
23.13 +import org.gjt.sp.jedit.io.Encoding
23.14 +import org.gjt.sp.jedit.buffer.JEditBuffer
23.15 +
23.16 +import java.nio.charset.{Charset, CharsetDecoder, CodingErrorAction}
23.17 +import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter,
23.18 + CharArrayReader, ByteArrayOutputStream}
23.19 +
23.20 +import scala.io.{Source, BufferedSource}
23.21 +
23.22 +
23.23 +object Isabelle_Encoding
23.24 +{
23.25 + val NAME = "UTF-8-Isabelle"
23.26 +
23.27 + def is_active(buffer: JEditBuffer): Boolean =
23.28 + buffer.getStringProperty(JEditBuffer.ENCODING).asInstanceOf[String] == NAME
23.29 +}
23.30 +
23.31 +class Isabelle_Encoding extends Encoding
23.32 +{
23.33 + private val charset = Charset.forName(Standard_System.charset)
23.34 + private val BUFSIZE = 32768
23.35 +
23.36 + private def text_reader(in: InputStream, decoder: CharsetDecoder): Reader =
23.37 + {
23.38 + def source(): Source =
23.39 + BufferedSource.fromInputStream(in, decoder, BUFSIZE, { () => source() })
23.40 + new CharArrayReader(Isabelle.system.symbols.decode(source.mkString).toArray)
23.41 + }
23.42 +
23.43 + override def getTextReader(in: InputStream): Reader =
23.44 + text_reader(in, charset.newDecoder())
23.45 +
23.46 + override def getPermissiveTextReader(in: InputStream): Reader =
23.47 + {
23.48 + val decoder = charset.newDecoder()
23.49 + decoder.onMalformedInput(CodingErrorAction.REPLACE)
23.50 + decoder.onUnmappableCharacter(CodingErrorAction.REPLACE)
23.51 + text_reader(in, decoder)
23.52 + }
23.53 +
23.54 + override def getTextWriter(out: OutputStream): Writer =
23.55 + {
23.56 + val buffer = new ByteArrayOutputStream(BUFSIZE) {
23.57 + override def flush()
23.58 + {
23.59 + val text = Isabelle.system.symbols.encode(toString(Standard_System.charset))
23.60 + out.write(text.getBytes(Standard_System.charset))
23.61 + out.flush()
23.62 + }
23.63 + override def close() { out.close() }
23.64 + }
23.65 + new OutputStreamWriter(buffer, charset.newEncoder())
23.66 + }
23.67 +}
24.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
24.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Mon Jan 11 22:31:27 2010 +0100
24.3 @@ -0,0 +1,76 @@
24.4 +/*
24.5 + * Hyperlink setup for Isabelle proof documents
24.6 + *
24.7 + * @author Fabian Immler, TU Munich
24.8 + */
24.9 +
24.10 +package isabelle.jedit
24.11 +
24.12 +import isabelle.proofdocument.Command
24.13 +
24.14 +import java.io.File
24.15 +
24.16 +import gatchan.jedit.hyperlinks.{Hyperlink, HyperlinkSource, AbstractHyperlink}
24.17 +
24.18 +import org.gjt.sp.jedit.{View, jEdit, Buffer, TextUtilities}
24.19 +
24.20 +
24.21 +private class Internal_Hyperlink(start: Int, end: Int, line: Int, ref_offset: Int)
24.22 + extends AbstractHyperlink(start, end, line, "")
24.23 +{
24.24 + override def click(view: View) {
24.25 + view.getTextArea.moveCaretPosition(ref_offset)
24.26 + }
24.27 +}
24.28 +
24.29 +class External_Hyperlink(start: Int, end: Int, line: Int, ref_file: String, ref_line: Int)
24.30 + extends AbstractHyperlink(start, end, line, "")
24.31 +{
24.32 + override def click(view: View) = {
24.33 + Isabelle.system.source_file(ref_file) match {
24.34 + case None => System.err.println("Could not find source file " + ref_file) // FIXME ??
24.35 + case Some(file) =>
24.36 + jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line))
24.37 + }
24.38 + }
24.39 +}
24.40 +
24.41 +class Isabelle_Hyperlinks extends HyperlinkSource
24.42 +{
24.43 + def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink =
24.44 + {
24.45 + Document_Model(buffer) match {
24.46 + case Some(model) =>
24.47 + val document = model.recent_document()
24.48 + val offset = model.from_current(document, original_offset)
24.49 + document.command_at(offset) match {
24.50 + case Some((command, command_start)) =>
24.51 + document.current_state(command).get.ref_at(offset - command_start) match {
24.52 + case Some(ref) =>
24.53 + val begin = model.to_current(document, command_start + ref.start)
24.54 + val line = buffer.getLineOfOffset(begin)
24.55 + val end = model.to_current(document, command_start + ref.stop)
24.56 + ref.info match {
24.57 + case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
24.58 + new External_Hyperlink(begin, end, line, ref_file, ref_line)
24.59 + case Command.RefInfo(_, _, Some(id), Some(offset)) =>
24.60 + Isabelle.session.lookup_entity(id) match {
24.61 + case Some(ref_cmd: Command) =>
24.62 + document.command_start(ref_cmd) match {
24.63 + case Some(ref_cmd_start) =>
24.64 + new Internal_Hyperlink(begin, end, line,
24.65 + model.to_current(document, ref_cmd_start + offset - 1))
24.66 + case None => null // FIXME external ref
24.67 + }
24.68 + case _ => null
24.69 + }
24.70 + case _ => null
24.71 + }
24.72 + case None => null
24.73 + }
24.74 + case None => null
24.75 + }
24.76 + case None => null
24.77 + }
24.78 + }
24.79 +}
25.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
25.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_options.scala Mon Jan 11 22:31:27 2010 +0100
25.3 @@ -0,0 +1,53 @@
25.4 +/*
25.5 + * Editor pane for plugin options
25.6 + *
25.7 + * @author Johannes Hölzl, TU Munich
25.8 + */
25.9 +
25.10 +package isabelle.jedit
25.11 +
25.12 +
25.13 +import javax.swing.{JComboBox, JSpinner}
25.14 +
25.15 +import org.gjt.sp.jedit.AbstractOptionPane
25.16 +
25.17 +
25.18 +class Isabelle_Options extends AbstractOptionPane("isabelle")
25.19 +{
25.20 + private val logic_name = new JComboBox()
25.21 + private val font_size = new JSpinner()
25.22 +
25.23 + private class List_Item(val name: String, val descr: String) {
25.24 + def this(name: String) = this(name, name)
25.25 + override def toString = descr
25.26 + }
25.27 +
25.28 + override def _init()
25.29 + {
25.30 + val logic = Isabelle.Property("logic")
25.31 + addComponent(Isabelle.Property("logic.title"), {
25.32 + logic_name.addItem(new List_Item("", "default (" + Isabelle.default_logic() + ")"))
25.33 + for (name <- Isabelle.system.find_logics()) {
25.34 + val item = new List_Item(name)
25.35 + logic_name.addItem(item)
25.36 + if (name == logic)
25.37 + logic_name.setSelectedItem(item)
25.38 + }
25.39 + logic_name
25.40 + })
25.41 +
25.42 + addComponent(Isabelle.Property("font-size.title"), {
25.43 + font_size.setValue(Isabelle.Int_Property("font-size"))
25.44 + font_size
25.45 + })
25.46 + }
25.47 +
25.48 + override def _save()
25.49 + {
25.50 + val logic = logic_name.getSelectedItem.asInstanceOf[List_Item].name
25.51 + Isabelle.Property("logic") = logic
25.52 +
25.53 + val size = font_size.getValue().asInstanceOf[Int]
25.54 + Isabelle.Int_Property("font-size") = size
25.55 + }
25.56 +}
26.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
26.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Mon Jan 11 22:31:27 2010 +0100
26.3 @@ -0,0 +1,100 @@
26.4 +/*
26.5 + * SideKick parser for Isabelle proof documents
26.6 + *
26.7 + * @author Fabian Immler, TU Munich
26.8 + * @author Makarius
26.9 + */
26.10 +
26.11 +package isabelle.jedit
26.12 +
26.13 +
26.14 +import scala.collection.Set
26.15 +import scala.collection.immutable.TreeSet
26.16 +
26.17 +import javax.swing.tree.DefaultMutableTreeNode
26.18 +import javax.swing.text.Position
26.19 +import javax.swing.Icon
26.20 +
26.21 +import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View}
26.22 +import errorlist.DefaultErrorSource
26.23 +import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset}
26.24 +
26.25 +import isabelle.proofdocument.{Command, Markup_Node, Document}
26.26 +
26.27 +
26.28 +class Isabelle_Sidekick extends SideKickParser("isabelle")
26.29 +{
26.30 + /* parsing */
26.31 +
26.32 + @volatile private var stopped = false
26.33 + override def stop() = { stopped = true }
26.34 +
26.35 + def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData =
26.36 + {
26.37 + implicit def int_to_pos(offset: Int): Position =
26.38 + new Position { def getOffset = offset; override def toString = offset.toString }
26.39 +
26.40 + stopped = false
26.41 +
26.42 + // FIXME lock buffer !??
26.43 + val data = new SideKickParsedData(buffer.getName)
26.44 + val root = data.root
26.45 + data.getAsset(root).setEnd(buffer.getLength)
26.46 +
26.47 + Swing_Thread.now { Document_Model(buffer) } match {
26.48 + case Some(model) =>
26.49 + val document = model.recent_document()
26.50 + for ((command, command_start) <- document.command_range(0) if !stopped) {
26.51 + root.add(document.current_state(command).get.markup_root.swing_tree((node: Markup_Node) =>
26.52 + {
26.53 + val content = command.source(node.start, node.stop)
26.54 + val id = command.id
26.55 +
26.56 + new DefaultMutableTreeNode(new IAsset {
26.57 + override def getIcon: Icon = null
26.58 + override def getShortString: String = content
26.59 + override def getLongString: String = node.info.toString
26.60 + override def getName: String = id
26.61 + override def setName(name: String) = ()
26.62 + override def setStart(start: Position) = ()
26.63 + override def getStart: Position = command_start + node.start
26.64 + override def setEnd(end: Position) = ()
26.65 + override def getEnd: Position = command_start + node.stop
26.66 + override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]"
26.67 + })
26.68 + }))
26.69 + }
26.70 + if (stopped) root.add(new DefaultMutableTreeNode("<parser stopped>"))
26.71 + case None => root.add(new DefaultMutableTreeNode("<buffer inactive>"))
26.72 + }
26.73 + data
26.74 + }
26.75 +
26.76 +
26.77 + /* completion */
26.78 +
26.79 + override def supportsCompletion = true
26.80 + override def canCompleteAnywhere = true
26.81 +
26.82 + override def complete(pane: EditPane, caret: Int): SideKickCompletion =
26.83 + {
26.84 + val buffer = pane.getBuffer
26.85 +
26.86 + val line = buffer.getLineOfOffset(caret)
26.87 + val start = buffer.getLineStartOffset(line)
26.88 + val text = buffer.getSegment(start, caret - start)
26.89 +
26.90 + val completion = Isabelle.session.current_syntax.completion
26.91 +
26.92 + completion.complete(text) match {
26.93 + case None => null
26.94 + case Some((word, cs)) =>
26.95 + val ds =
26.96 + if (Isabelle_Encoding.is_active(buffer))
26.97 + cs.map(Isabelle.system.symbols.decode(_)).sort(_ < _)
26.98 + else cs
26.99 + new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { }
26.100 + }
26.101 + }
26.102 +
26.103 +}
27.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
27.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Mon Jan 11 22:31:27 2010 +0100
27.3 @@ -0,0 +1,145 @@
27.4 +/*
27.5 + * include isabelle's command- and keyword-declarations
27.6 + * live in jEdits syntax-highlighting
27.7 + *
27.8 + * @author Fabian Immler, TU Munich
27.9 + */
27.10 +
27.11 +package isabelle.jedit
27.12 +
27.13 +
27.14 +import isabelle.Markup
27.15 +
27.16 +import org.gjt.sp.jedit.buffer.JEditBuffer
27.17 +import org.gjt.sp.jedit.syntax.{Token, TokenMarker, TokenHandler, SyntaxStyle, ParserRuleSet}
27.18 +
27.19 +import java.awt.Color
27.20 +import java.awt.Font
27.21 +import javax.swing.text.Segment;
27.22 +
27.23 +
27.24 +object Isabelle_Token_Marker
27.25 +{
27.26 + /* line context */
27.27 +
27.28 + private val rule_set = new ParserRuleSet("isabelle", "MAIN")
27.29 + private class LineContext(val line: Int, prev: LineContext)
27.30 + extends TokenMarker.LineContext(rule_set, prev)
27.31 +
27.32 +
27.33 + /* mapping to jEdit token types */
27.34 + // TODO: as properties or CSS style sheet
27.35 +
27.36 + private val choose_byte: Map[String, Byte] =
27.37 + {
27.38 + import Token._
27.39 + Map[String, Byte](
27.40 + // logical entities
27.41 + Markup.TCLASS -> LABEL,
27.42 + Markup.TYCON -> LABEL,
27.43 + Markup.FIXED_DECL -> LABEL,
27.44 + Markup.FIXED -> LABEL,
27.45 + Markup.CONST_DECL -> LABEL,
27.46 + Markup.CONST -> LABEL,
27.47 + Markup.FACT_DECL -> LABEL,
27.48 + Markup.FACT -> LABEL,
27.49 + Markup.DYNAMIC_FACT -> LABEL,
27.50 + Markup.LOCAL_FACT_DECL -> LABEL,
27.51 + Markup.LOCAL_FACT -> LABEL,
27.52 + // inner syntax
27.53 + Markup.TFREE -> LITERAL2,
27.54 + Markup.FREE -> LITERAL2,
27.55 + Markup.TVAR -> LITERAL3,
27.56 + Markup.SKOLEM -> LITERAL3,
27.57 + Markup.BOUND -> LITERAL3,
27.58 + Markup.VAR -> LITERAL3,
27.59 + Markup.NUM -> DIGIT,
27.60 + Markup.FLOAT -> DIGIT,
27.61 + Markup.XNUM -> DIGIT,
27.62 + Markup.XSTR -> LITERAL4,
27.63 + Markup.LITERAL -> LITERAL4,
27.64 + Markup.INNER_COMMENT -> COMMENT1,
27.65 + Markup.SORT -> FUNCTION,
27.66 + Markup.TYP -> FUNCTION,
27.67 + Markup.TERM -> FUNCTION,
27.68 + Markup.PROP -> FUNCTION,
27.69 + Markup.ATTRIBUTE -> FUNCTION,
27.70 + Markup.METHOD -> FUNCTION,
27.71 + // ML syntax
27.72 + Markup.ML_KEYWORD -> KEYWORD2,
27.73 + Markup.ML_IDENT -> NULL,
27.74 + Markup.ML_TVAR -> LITERAL3,
27.75 + Markup.ML_NUMERAL -> DIGIT,
27.76 + Markup.ML_CHAR -> LITERAL1,
27.77 + Markup.ML_STRING -> LITERAL1,
27.78 + Markup.ML_COMMENT -> COMMENT1,
27.79 + Markup.ML_MALFORMED -> INVALID,
27.80 + // embedded source text
27.81 + Markup.ML_SOURCE -> COMMENT4,
27.82 + Markup.DOC_SOURCE -> COMMENT4,
27.83 + Markup.ANTIQ -> COMMENT4,
27.84 + Markup.ML_ANTIQ -> COMMENT4,
27.85 + Markup.DOC_ANTIQ -> COMMENT4,
27.86 + // outer syntax
27.87 + Markup.IDENT -> NULL,
27.88 + Markup.COMMAND -> OPERATOR,
27.89 + Markup.KEYWORD -> KEYWORD4,
27.90 + Markup.VERBATIM -> COMMENT3,
27.91 + Markup.COMMENT -> COMMENT1,
27.92 + Markup.CONTROL -> COMMENT3,
27.93 + Markup.MALFORMED -> INVALID,
27.94 + Markup.STRING -> LITERAL3,
27.95 + Markup.ALTSTRING -> LITERAL1
27.96 + ).withDefaultValue(NULL)
27.97 + }
27.98 +
27.99 + def choose_color(kind: String, styles: Array[SyntaxStyle]): Color =
27.100 + styles(choose_byte(kind)).getForegroundColor
27.101 +}
27.102 +
27.103 +
27.104 +class Isabelle_Token_Marker(model: Document_Model) extends TokenMarker
27.105 +{
27.106 + override def markTokens(prev: TokenMarker.LineContext,
27.107 + handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext =
27.108 + {
27.109 + val previous = prev.asInstanceOf[Isabelle_Token_Marker.LineContext]
27.110 + val line = if (prev == null) 0 else previous.line + 1
27.111 + val context = new Isabelle_Token_Marker.LineContext(line, previous)
27.112 + val start = model.buffer.getLineStartOffset(line)
27.113 + val stop = start + line_segment.count
27.114 +
27.115 + val document = model.recent_document()
27.116 + def to: Int => Int = model.to_current(document, _)
27.117 + def from: Int => Int = model.from_current(document, _)
27.118 +
27.119 + var next_x = start
27.120 + for {
27.121 + (command, command_start) <- document.command_range(from(start), from(stop))
27.122 + markup <- document.current_state(command).get.highlight.flatten
27.123 + val abs_start = to(command_start + markup.start)
27.124 + val abs_stop = to(command_start + markup.stop)
27.125 + if (abs_stop > start)
27.126 + if (abs_start < stop)
27.127 + val byte = Isabelle_Token_Marker.choose_byte(markup.info.toString)
27.128 + val token_start = (abs_start - start) max 0
27.129 + val token_length =
27.130 + (abs_stop - abs_start) -
27.131 + ((start - abs_start) max 0) -
27.132 + ((abs_stop - stop) max 0)
27.133 + }
27.134 + {
27.135 + if (start + token_start > next_x)
27.136 + handler.handleToken(line_segment, 1,
27.137 + next_x - start, start + token_start - next_x, context)
27.138 + handler.handleToken(line_segment, byte, token_start, token_length, context)
27.139 + next_x = start + token_start + token_length
27.140 + }
27.141 + if (next_x < stop)
27.142 + handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
27.143 +
27.144 + handler.handleToken(line_segment, Token.END, line_segment.count, 0, context)
27.145 + handler.setLineContext(context)
27.146 + context
27.147 + }
27.148 +}
28.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
28.2 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Mon Jan 11 22:31:27 2010 +0100
28.3 @@ -0,0 +1,66 @@
28.4 +/*
28.5 + * Dockable window with result message output
28.6 + *
28.7 + * @author Makarius
28.8 + */
28.9 +
28.10 +package isabelle.jedit
28.11 +
28.12 +
28.13 +import isabelle.proofdocument.{Command, HTML_Panel, Session}
28.14 +
28.15 +import scala.actors.Actor._
28.16 +
28.17 +import javax.swing.JPanel
28.18 +import java.awt.{BorderLayout, Dimension}
28.19 +
28.20 +import org.gjt.sp.jedit.View
28.21 +import org.gjt.sp.jedit.gui.DockableWindowManager
28.22 +
28.23 +
28.24 +
28.25 +class Output_Dockable(view: View, position: String) extends JPanel(new BorderLayout)
28.26 +{
28.27 + if (position == DockableWindowManager.FLOATING)
28.28 + setPreferredSize(new Dimension(500, 250))
28.29 +
28.30 + private val html_panel =
28.31 + new HTML_Panel(Isabelle.system, Isabelle.Int_Property("font-size"), null)
28.32 + add(html_panel, BorderLayout.CENTER)
28.33 +
28.34 +
28.35 + /* actor wiring */
28.36 +
28.37 + private val output_actor = actor {
28.38 + loop {
28.39 + react {
28.40 + case cmd: Command =>
28.41 + Swing_Thread.now { Document_Model(view.getBuffer) } match {
28.42 + case None =>
28.43 + case Some(model) =>
28.44 + val body = model.recent_document.current_state(cmd).map(_.results) getOrElse Nil
28.45 + html_panel.render(body)
28.46 + }
28.47 +
28.48 + case Session.Global_Settings =>
28.49 + html_panel.init(Isabelle.Int_Property("font-size"))
28.50 +
28.51 + case bad => System.err.println("output_actor: ignoring bad message " + bad)
28.52 + }
28.53 + }
28.54 + }
28.55 +
28.56 + override def addNotify()
28.57 + {
28.58 + super.addNotify()
28.59 + Isabelle.session.results += output_actor
28.60 + Isabelle.session.global_settings += output_actor
28.61 + }
28.62 +
28.63 + override def removeNotify()
28.64 + {
28.65 + Isabelle.session.results -= output_actor
28.66 + Isabelle.session.global_settings -= output_actor
28.67 + super.removeNotify()
28.68 + }
28.69 +}
29.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
29.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala Mon Jan 11 22:31:27 2010 +0100
29.3 @@ -0,0 +1,197 @@
29.4 +/*
29.5 + * Main Isabelle/jEdit plugin setup
29.6 + *
29.7 + * @author Johannes Hölzl, TU Munich
29.8 + * @author Fabian Immler, TU Munich
29.9 + * @author Makarius
29.10 + */
29.11 +
29.12 +package isabelle.jedit
29.13 +
29.14 +
29.15 +import isabelle.proofdocument.Session
29.16 +
29.17 +import java.io.{FileInputStream, IOException}
29.18 +import java.awt.Font
29.19 +import javax.swing.JTextArea
29.20 +
29.21 +import scala.collection.mutable
29.22 +
29.23 +import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View}
29.24 +import org.gjt.sp.jedit.buffer.JEditBuffer
29.25 +import org.gjt.sp.jedit.textarea.JEditTextArea
29.26 +import org.gjt.sp.jedit.msg.{EditPaneUpdate, PropertiesChanged}
29.27 +
29.28 +
29.29 +object Isabelle
29.30 +{
29.31 + /* plugin instance */
29.32 +
29.33 + var system: Isabelle_System = null
29.34 + var session: Session = null
29.35 +
29.36 +
29.37 + /* name */
29.38 +
29.39 + val NAME = "Isabelle"
29.40 +
29.41 +
29.42 + /* properties */
29.43 +
29.44 + val OPTION_PREFIX = "options.isabelle."
29.45 +
29.46 + object Property
29.47 + {
29.48 + def apply(name: String): String = jEdit.getProperty(OPTION_PREFIX + name)
29.49 + def update(name: String, value: String) = jEdit.setProperty(OPTION_PREFIX + name, value)
29.50 + }
29.51 +
29.52 + object Boolean_Property
29.53 + {
29.54 + def apply(name: String): Boolean = jEdit.getBooleanProperty(OPTION_PREFIX + name)
29.55 + def update(name: String, value: Boolean) = jEdit.setBooleanProperty(OPTION_PREFIX + name, value)
29.56 + }
29.57 +
29.58 + object Int_Property
29.59 + {
29.60 + def apply(name: String): Int = jEdit.getIntegerProperty(OPTION_PREFIX + name)
29.61 + def update(name: String, value: Int) = jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
29.62 + }
29.63 +
29.64 +
29.65 + /* settings */
29.66 +
29.67 + def default_logic(): String =
29.68 + {
29.69 + val logic = system.getenv("JEDIT_LOGIC")
29.70 + if (logic != "") logic
29.71 + else system.getenv_strict("ISABELLE_LOGIC")
29.72 + }
29.73 +
29.74 + def isabelle_args(): List[String] =
29.75 + {
29.76 + val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
29.77 + val logic = {
29.78 + val logic = Property("logic")
29.79 + if (logic != null && logic != "") logic
29.80 + else default_logic()
29.81 + }
29.82 + modes ++ List(logic)
29.83 + }
29.84 +
29.85 +
29.86 + /* main jEdit components */ // FIXME ownership!?
29.87 +
29.88 + def jedit_buffers(): Iterator[Buffer] = Iterator.fromArray(jEdit.getBuffers())
29.89 +
29.90 + def jedit_views(): Iterator[View] = Iterator.fromArray(jEdit.getViews())
29.91 +
29.92 + def jedit_text_areas(view: View): Iterator[JEditTextArea] =
29.93 + Iterator.fromArray(view.getEditPanes).map(_.getTextArea)
29.94 +
29.95 + def jedit_text_areas(): Iterator[JEditTextArea] =
29.96 + jedit_views().flatMap(jedit_text_areas(_))
29.97 +
29.98 + def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
29.99 + jedit_text_areas().filter(_.getBuffer == buffer)
29.100 +
29.101 +
29.102 + /* manage prover */
29.103 +
29.104 + private def prover_started(view: View): Boolean =
29.105 + {
29.106 + val timeout = Int_Property("startup-timeout") max 1000
29.107 + session.start(timeout, Isabelle.isabelle_args()) match {
29.108 + case Some(err) =>
29.109 + val text = new JTextArea(err); text.setEditable(false)
29.110 + Library.error_dialog(view, null, "Failed to start Isabelle process", text)
29.111 + false
29.112 + case None => true
29.113 + }
29.114 + }
29.115 +
29.116 +
29.117 + /* activation */
29.118 +
29.119 + def activate_buffer(view: View, buffer: Buffer)
29.120 + {
29.121 + if (prover_started(view)) {
29.122 + val model = Document_Model.init(session, buffer)
29.123 + for (text_area <- jedit_text_areas(buffer))
29.124 + Document_View.init(model, text_area)
29.125 + }
29.126 + }
29.127 +
29.128 + def deactivate_buffer(buffer: Buffer)
29.129 + {
29.130 + session.stop() // FIXME not yet
29.131 +
29.132 + for (text_area <- jedit_text_areas(buffer))
29.133 + Document_View.exit(text_area)
29.134 + Document_Model.exit(buffer)
29.135 + }
29.136 +
29.137 + def switch_active(view: View) =
29.138 + {
29.139 + val buffer = view.getBuffer
29.140 + if (Document_Model(buffer).isDefined) deactivate_buffer(buffer)
29.141 + else activate_buffer(view, buffer)
29.142 + }
29.143 +
29.144 + def is_active(view: View): Boolean =
29.145 + Document_Model(view.getBuffer).isDefined
29.146 +}
29.147 +
29.148 +
29.149 +class Plugin extends EBPlugin
29.150 +{
29.151 + /* main plugin plumbing */
29.152 +
29.153 + override def handleMessage(message: EBMessage)
29.154 + {
29.155 + message match {
29.156 + case msg: EditPaneUpdate =>
29.157 + val edit_pane = msg.getEditPane
29.158 + val buffer = edit_pane.getBuffer
29.159 + val text_area = edit_pane.getTextArea
29.160 +
29.161 + def init_view()
29.162 + {
29.163 + Document_Model(buffer) match {
29.164 + case Some(model) => Document_View.init(model, text_area)
29.165 + case None =>
29.166 + }
29.167 + }
29.168 + def exit_view()
29.169 + {
29.170 + if (Document_View(text_area).isDefined)
29.171 + Document_View.exit(text_area)
29.172 + }
29.173 + msg.getWhat match {
29.174 + case EditPaneUpdate.BUFFER_CHANGED => exit_view(); init_view()
29.175 + case EditPaneUpdate.CREATED => init_view()
29.176 + case EditPaneUpdate.DESTROYED => exit_view()
29.177 + case _ =>
29.178 + }
29.179 +
29.180 + case msg: PropertiesChanged =>
29.181 + Isabelle.session.global_settings.event(Session.Global_Settings)
29.182 +
29.183 + case _ =>
29.184 + }
29.185 + }
29.186 +
29.187 + override def start()
29.188 + {
29.189 + Isabelle.system = new Isabelle_System
29.190 + Isabelle.system.install_fonts()
29.191 + Isabelle.session = new Session(Isabelle.system) // FIXME dialog!?
29.192 + }
29.193 +
29.194 + override def stop()
29.195 + {
29.196 + Isabelle.session.stop() // FIXME dialog!?
29.197 + Isabelle.session = null
29.198 + Isabelle.system = null
29.199 + }
29.200 +}
30.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
30.2 +++ b/src/Tools/jEdit/src/jedit/protocol_dockable.scala Mon Jan 11 22:31:27 2010 +0100
30.3 @@ -0,0 +1,52 @@
30.4 +/*
30.5 + * Dockable window for raw process output
30.6 + *
30.7 + * @author Makarius
30.8 + */
30.9 +
30.10 +package isabelle.jedit
30.11 +
30.12 +
30.13 +import scala.actors.Actor._
30.14 +
30.15 +import java.awt.{Dimension, Graphics, BorderLayout}
30.16 +import javax.swing.{JPanel, JTextArea, JScrollPane}
30.17 +
30.18 +import org.gjt.sp.jedit.View
30.19 +import org.gjt.sp.jedit.gui.DockableWindowManager
30.20 +
30.21 +
30.22 +class Protocol_Dockable(view: View, position: String) extends JPanel(new BorderLayout)
30.23 +{
30.24 + if (position == DockableWindowManager.FLOATING)
30.25 + setPreferredSize(new Dimension(500, 250))
30.26 +
30.27 + private val text_area = new JTextArea
30.28 + add(new JScrollPane(text_area), BorderLayout.CENTER)
30.29 +
30.30 +
30.31 + /* actor wiring */
30.32 +
30.33 + private val raw_actor = actor {
30.34 + loop {
30.35 + react {
30.36 + case result: Isabelle_Process.Result =>
30.37 + Swing_Thread.now { text_area.append(result.toString + "\n") }
30.38 +
30.39 + case bad => System.err.println("raw_actor: ignoring bad message " + bad)
30.40 + }
30.41 + }
30.42 + }
30.43 +
30.44 + override def addNotify()
30.45 + {
30.46 + super.addNotify()
30.47 + Isabelle.session.raw_results += raw_actor
30.48 + }
30.49 +
30.50 + override def removeNotify()
30.51 + {
30.52 + Isabelle.session.raw_results -= raw_actor
30.53 + super.removeNotify()
30.54 + }
30.55 +}
31.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
31.2 +++ b/src/Tools/jEdit/src/jedit/scala_console.scala Mon Jan 11 22:31:27 2010 +0100
31.3 @@ -0,0 +1,153 @@
31.4 +/*
31.5 + * Scala instance of Console plugin
31.6 + *
31.7 + * @author Makarius
31.8 + */
31.9 +
31.10 +package isabelle.jedit
31.11 +
31.12 +
31.13 +import console.{Console, ConsolePane, Shell, Output}
31.14 +
31.15 +import org.gjt.sp.jedit.{jEdit, JARClassLoader}
31.16 +import org.gjt.sp.jedit.MiscUtilities
31.17 +
31.18 +import java.io.{File, OutputStream, Writer, PrintWriter}
31.19 +
31.20 +import scala.tools.nsc.{Interpreter, GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
31.21 +import scala.collection.mutable
31.22 +
31.23 +
31.24 +class Scala_Console extends Shell("Scala")
31.25 +{
31.26 + /* reconstructed jEdit/plugin classpath */
31.27 +
31.28 + private def reconstruct_classpath(): String =
31.29 + {
31.30 + def find_jars(start: String): List[String] =
31.31 + if (start != null)
31.32 + Standard_System.find_files(new File(start),
31.33 + entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath)
31.34 + else Nil
31.35 + val path = find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome)
31.36 + path.mkString(File.pathSeparator)
31.37 + }
31.38 +
31.39 +
31.40 + /* global state -- owned by Swing thread */
31.41 +
31.42 + private var interpreters = Map[Console, Interpreter]()
31.43 +
31.44 + private var global_console: Console = null
31.45 + private var global_out: Output = null
31.46 + private var global_err: Output = null
31.47 +
31.48 + private val console_stream = new OutputStream
31.49 + {
31.50 + val buf = new StringBuilder
31.51 + override def flush()
31.52 + {
31.53 + val str = Standard_System.decode_permissive_utf8(buf.toString)
31.54 + buf.clear
31.55 + if (global_out == null) System.out.print(str)
31.56 + else Swing_Thread.now { global_out.writeAttrs(null, str) }
31.57 + }
31.58 + override def close() { flush () }
31.59 + def write(byte: Int) { buf.append(byte.toChar) }
31.60 + }
31.61 +
31.62 + private val console_writer = new Writer
31.63 + {
31.64 + def flush() {}
31.65 + def close() {}
31.66 +
31.67 + def write(cbuf: Array[Char], off: Int, len: Int)
31.68 + {
31.69 + if (len > 0) write(new String(cbuf.subArray(off, off + len)))
31.70 + }
31.71 +
31.72 + override def write(str: String)
31.73 + {
31.74 + if (global_out == null) System.out.println(str)
31.75 + else global_out.print(null, str)
31.76 + }
31.77 + }
31.78 +
31.79 + private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A =
31.80 + {
31.81 + global_console = console
31.82 + global_out = out
31.83 + global_err = if (err == null) out else err
31.84 + val res = Exn.capture { scala.Console.withOut(console_stream)(e) }
31.85 + console_stream.flush
31.86 + global_console = null
31.87 + global_out = null
31.88 + global_err = null
31.89 + Exn.release(res)
31.90 + }
31.91 +
31.92 + private def report_error(str: String)
31.93 + {
31.94 + if (global_console == null || global_err == null) System.err.println(str)
31.95 + else Swing_Thread.now { global_err.print(global_console.getErrorColor, str) }
31.96 + }
31.97 +
31.98 +
31.99 + /* jEdit console methods */
31.100 +
31.101 + override def openConsole(console: Console)
31.102 + {
31.103 + val settings = new GenericRunnerSettings(report_error)
31.104 + settings.classpath.value = reconstruct_classpath()
31.105 +
31.106 + val interp = new Interpreter(settings, new PrintWriter(console_writer, true))
31.107 + {
31.108 + override def parentClassLoader = new JARClassLoader
31.109 + }
31.110 + interp.setContextClassLoader
31.111 + interp.bind("view", "org.gjt.sp.jedit.View", console.getView)
31.112 + interp.bind("console", "console.Console", console)
31.113 + interp.interpret("import isabelle.jedit.Isabelle")
31.114 +
31.115 + interpreters += (console -> interp)
31.116 + }
31.117 +
31.118 + override def closeConsole(console: Console)
31.119 + {
31.120 + interpreters -= console
31.121 + }
31.122 +
31.123 + override def printInfoMessage(out: Output)
31.124 + {
31.125 + out.print(null,
31.126 + "This shell evaluates Isabelle/Scala expressions.\n\n" +
31.127 + "The following special toplevel bindings are provided:\n" +
31.128 + " view -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" +
31.129 + " console -- jEdit Console plugin instance\n" +
31.130 + " Isabelle -- Isabelle plugin instance (e.g. Isabelle.system, Isabelle.session)\n")
31.131 + }
31.132 +
31.133 + override def printPrompt(console: Console, out: Output)
31.134 + {
31.135 + out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>")
31.136 + out.writeAttrs(ConsolePane.colorAttributes(console.getPlainColor), " ")
31.137 + }
31.138 +
31.139 + override def execute(console: Console, input: String, out: Output, err: Output, command: String)
31.140 + {
31.141 + val interp = interpreters(console)
31.142 + with_console(console, out, err) { interp.interpret(command) }
31.143 + if (err != null) err.commandDone()
31.144 + out.commandDone()
31.145 + }
31.146 +
31.147 + override def stop(console: Console)
31.148 + {
31.149 + closeConsole(console)
31.150 + console.clear
31.151 + openConsole(console)
31.152 + val out = console.getOutput
31.153 + out.commandDone
31.154 + printPrompt(console, out)
31.155 + }
31.156 +}
32.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
32.2 +++ b/src/Tools/jEdit/src/proofdocument/change.scala Mon Jan 11 22:31:27 2010 +0100
32.3 @@ -0,0 +1,42 @@
32.4 +/*
32.5 + * Changes of plain text
32.6 + *
32.7 + * @author Fabian Immler, TU Munich
32.8 + * @author Makarius
32.9 + */
32.10 +
32.11 +package isabelle.proofdocument
32.12 +
32.13 +
32.14 +class Change(
32.15 + val id: Isar_Document.Document_ID,
32.16 + val parent: Option[Change],
32.17 + val edits: List[Text_Edit],
32.18 + val result: Future[(List[Document.Edit], Document)])
32.19 +{
32.20 + def ancestors: Iterator[Change] = new Iterator[Change]
32.21 + {
32.22 + private var state: Option[Change] = Some(Change.this)
32.23 + def hasNext = state.isDefined
32.24 + def next =
32.25 + state match {
32.26 + case Some(change) => state = change.parent; change
32.27 + case None => throw new NoSuchElementException("next on empty iterator")
32.28 + }
32.29 + }
32.30 +
32.31 + def join_document: Document = result.join._2
32.32 + def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
32.33 +
32.34 + def edit(session: Session, edits: List[Text_Edit]): Change =
32.35 + {
32.36 + val new_id = session.create_id()
32.37 + val result: Future[(List[Document.Edit], Document)] =
32.38 + Future.fork {
32.39 + val old_doc = join_document
32.40 + old_doc.await_assignment
32.41 + Document.text_edits(session, old_doc, new_id, edits)
32.42 + }
32.43 + new Change(new_id, Some(this), edits, result)
32.44 + }
32.45 +}
32.46 \ No newline at end of file
33.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
33.2 +++ b/src/Tools/jEdit/src/proofdocument/command.scala Mon Jan 11 22:31:27 2010 +0100
33.3 @@ -0,0 +1,102 @@
33.4 +/*
33.5 + * Prover commands with semantic state
33.6 + *
33.7 + * @author Johannes Hölzl, TU Munich
33.8 + * @author Fabian Immler, TU Munich
33.9 + */
33.10 +
33.11 +package isabelle.proofdocument
33.12 +
33.13 +
33.14 +import scala.actors.Actor, Actor._
33.15 +import scala.collection.mutable
33.16 +
33.17 +import isabelle.jedit.Isabelle
33.18 +
33.19 +
33.20 +object Command
33.21 +{
33.22 + object Status extends Enumeration
33.23 + {
33.24 + val UNPROCESSED = Value("UNPROCESSED")
33.25 + val FINISHED = Value("FINISHED")
33.26 + val FAILED = Value("FAILED")
33.27 + }
33.28 +
33.29 + case class HighlightInfo(highlight: String) { override def toString = highlight }
33.30 + case class TypeInfo(ty: String)
33.31 + case class RefInfo(file: Option[String], line: Option[Int],
33.32 + command_id: Option[String], offset: Option[Int])
33.33 +}
33.34 +
33.35 +
33.36 +class Command(
33.37 + val id: Isar_Document.Command_ID,
33.38 + val span: Thy_Syntax.Span)
33.39 + extends Session.Entity
33.40 +{
33.41 + /* classification */
33.42 +
33.43 + def is_command: Boolean = !span.isEmpty && span.first.is_command
33.44 + def is_ignored: Boolean = span.forall(_.is_ignored)
33.45 + def is_malformed: Boolean = !is_command && !is_ignored
33.46 +
33.47 + def name: String = if (is_command) span.first.content else ""
33.48 + override def toString = if (is_command) name else if (is_ignored) "<ignored>" else "<malformed>"
33.49 +
33.50 +
33.51 + /* source text */
33.52 +
33.53 + val source: String = span.map(_.source).mkString
33.54 + def source(i: Int, j: Int): String = source.substring(i, j)
33.55 + def length: Int = source.length
33.56 +
33.57 + lazy val symbol_index = new Symbol.Index(source)
33.58 +
33.59 +
33.60 + /* accumulated messages */
33.61 +
33.62 + @volatile protected var state = new State(this)
33.63 + def current_state: State = state
33.64 +
33.65 + private case class Consume(session: Session, message: XML.Tree)
33.66 + private case object Assign
33.67 +
33.68 + private val accumulator = actor {
33.69 + var assigned = false
33.70 + loop {
33.71 + react {
33.72 + case Consume(session: Session, message: XML.Tree) if !assigned =>
33.73 + state = state.+(session, message)
33.74 +
33.75 + case Assign =>
33.76 + assigned = true // single assignment
33.77 + reply(())
33.78 +
33.79 + case bad => System.err.println("command accumulator: ignoring bad message " + bad)
33.80 + }
33.81 + }
33.82 + }
33.83 +
33.84 + def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) }
33.85 +
33.86 + def assign_state(state_id: Isar_Document.State_ID): Command =
33.87 + {
33.88 + val cmd = new Command(state_id, span)
33.89 + accumulator !? Assign
33.90 + cmd.state = current_state
33.91 + cmd
33.92 + }
33.93 +
33.94 +
33.95 + /* markup */
33.96 +
33.97 + lazy val empty_markup = new Markup_Text(Nil, source)
33.98 +
33.99 + def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
33.100 + {
33.101 + val start = symbol_index.decode(begin)
33.102 + val stop = symbol_index.decode(end)
33.103 + new Markup_Tree(new Markup_Node(start, stop, info), Nil)
33.104 + }
33.105 +}
34.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
34.2 +++ b/src/Tools/jEdit/src/proofdocument/document.scala Mon Jan 11 22:31:27 2010 +0100
34.3 @@ -0,0 +1,197 @@
34.4 +/*
34.5 + * Document as editable list of commands
34.6 + *
34.7 + * @author Makarius
34.8 + */
34.9 +
34.10 +package isabelle.proofdocument
34.11 +
34.12 +
34.13 +object Document
34.14 +{
34.15 + /* command start positions */
34.16 +
34.17 + def command_starts(commands: Linear_Set[Command]): Iterator[(Command, Int)] =
34.18 + {
34.19 + var offset = 0
34.20 + for (cmd <- commands.elements) yield {
34.21 + val start = offset
34.22 + offset += cmd.length
34.23 + (cmd, start)
34.24 + }
34.25 + }
34.26 +
34.27 +
34.28 + /* empty document */
34.29 +
34.30 + def empty(id: Isar_Document.Document_ID): Document =
34.31 + {
34.32 + val doc = new Document(id, Linear_Set(), Map())
34.33 + doc.assign_states(Nil)
34.34 + doc
34.35 + }
34.36 +
34.37 +
34.38 + // FIXME
34.39 + var phase0: List[Text_Edit] = null
34.40 + var phase1: Linear_Set[Command] = null
34.41 + var phase2: Linear_Set[Command] = null
34.42 + var phase3: List[Edit] = null
34.43 +
34.44 +
34.45 +
34.46 + /** document edits **/
34.47 +
34.48 + type Edit = (Option[Command], Option[Command])
34.49 +
34.50 + def text_edits(session: Session, old_doc: Document, new_id: Isar_Document.Document_ID,
34.51 + edits: List[Text_Edit]): (List[Edit], Document) =
34.52 + {
34.53 + require(old_doc.assignment.is_finished)
34.54 +
34.55 +
34.56 + /* unparsed dummy commands */
34.57 +
34.58 + def unparsed(source: String) =
34.59 + new Command(null, List(Outer_Lex.Token(Outer_Lex.Token_Kind.UNPARSED, source)))
34.60 +
34.61 + def is_unparsed(command: Command) = command.id == null
34.62 +
34.63 + assert(!old_doc.commands.exists(is_unparsed)) // FIXME remove
34.64 +
34.65 +
34.66 + /* phase 1: edit individual command source */
34.67 +
34.68 + def edit_text(eds: List[Text_Edit], commands: Linear_Set[Command]): Linear_Set[Command] =
34.69 + {
34.70 + eds match {
34.71 + case e :: es =>
34.72 + command_starts(commands).find { // FIXME relative search!
34.73 + case (cmd, cmd_start) =>
34.74 + e.can_edit(cmd.source, cmd_start) || e.is_insert && e.start == cmd_start + cmd.length
34.75 + } match {
34.76 + case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) =>
34.77 + val (rest, text) = e.edit(cmd.source, cmd_start)
34.78 + val new_commands = commands.insert_after(Some(cmd), unparsed(text)) - cmd
34.79 + edit_text(rest.toList ::: es, new_commands)
34.80 +
34.81 + case Some((cmd, cmd_start)) =>
34.82 + edit_text(es, commands.insert_after(Some(cmd), unparsed(e.text)))
34.83 +
34.84 + case None =>
34.85 + require(e.is_insert && e.start == 0)
34.86 + edit_text(es, commands.insert_after(None, unparsed(e.text)))
34.87 + }
34.88 + case Nil => commands
34.89 + }
34.90 + }
34.91 +
34.92 +
34.93 + /* phase 2: recover command spans */
34.94 +
34.95 + def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
34.96 + {
34.97 + // FIXME relative search!
34.98 + commands.elements.find(is_unparsed) match {
34.99 + case Some(first_unparsed) =>
34.100 + val prefix = commands.prev(first_unparsed)
34.101 + val body = commands.elements(first_unparsed).takeWhile(is_unparsed).toList
34.102 + val suffix = commands.next(body.last)
34.103 +
34.104 + val sources = (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source))
34.105 + val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString))
34.106 +
34.107 + val (before_edit, spans1) =
34.108 + if (!spans0.isEmpty && Some(spans0.first) == prefix.map(_.span))
34.109 + (prefix, spans0.tail)
34.110 + else (if (prefix.isDefined) commands.prev(prefix.get) else None, spans0)
34.111 +
34.112 + val (after_edit, spans2) =
34.113 + if (!spans1.isEmpty && Some(spans1.last) == suffix.map(_.span))
34.114 + (suffix, spans1.take(spans1.length - 1))
34.115 + else (if (suffix.isDefined) commands.next(suffix.get) else None, spans1)
34.116 +
34.117 + val inserted = spans2.map(span => new Command(session.create_id(), span))
34.118 + val new_commands =
34.119 + commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
34.120 + parse_spans(new_commands)
34.121 +
34.122 + case None => commands
34.123 + }
34.124 + }
34.125 +
34.126 +
34.127 + /* phase 3: resulting document edits */
34.128 +
34.129 + val result = Library.timeit("text_edits") {
34.130 + val commands0 = old_doc.commands
34.131 + val commands1 = Library.timeit("edit_text") { edit_text(edits, commands0) }
34.132 + val commands2 = Library.timeit("parse_spans") { parse_spans(commands1) }
34.133 +
34.134 + val removed_commands = commands0.elements.filter(!commands2.contains(_)).toList
34.135 + val inserted_commands = commands2.elements.filter(!commands0.contains(_)).toList
34.136 +
34.137 + val doc_edits =
34.138 + removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
34.139 + inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
34.140 +
34.141 + val former_states = old_doc.assignment.join -- removed_commands
34.142 +
34.143 + phase0 = edits
34.144 + phase1 = commands1
34.145 + phase2 = commands2
34.146 + phase3 = doc_edits
34.147 +
34.148 + (doc_edits, new Document(new_id, commands2, former_states))
34.149 + }
34.150 + result
34.151 + }
34.152 +}
34.153 +
34.154 +
34.155 +class Document(
34.156 + val id: Isar_Document.Document_ID,
34.157 + val commands: Linear_Set[Command],
34.158 + former_states: Map[Command, Command])
34.159 +{
34.160 + /* command ranges */
34.161 +
34.162 + def command_starts: Iterator[(Command, Int)] = Document.command_starts(commands)
34.163 +
34.164 + def command_start(cmd: Command): Option[Int] =
34.165 + command_starts.find(_._1 == cmd).map(_._2)
34.166 +
34.167 + def command_range(i: Int): Iterator[(Command, Int)] =
34.168 + command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
34.169 +
34.170 + def command_range(i: Int, j: Int): Iterator[(Command, Int)] =
34.171 + command_range(i) takeWhile { case (_, start) => start < j }
34.172 +
34.173 + def command_at(i: Int): Option[(Command, Int)] =
34.174 + {
34.175 + val range = command_range(i)
34.176 + if (range.hasNext) Some(range.next) else None
34.177 + }
34.178 +
34.179 +
34.180 + /* command state assignment */
34.181 +
34.182 + val assignment = Future.promise[Map[Command, Command]]
34.183 + def await_assignment { assignment.join }
34.184 +
34.185 + @volatile private var tmp_states = former_states
34.186 + private val time0 = System.currentTimeMillis
34.187 +
34.188 + def assign_states(new_states: List[(Command, Command)])
34.189 + {
34.190 + assignment.fulfill(tmp_states ++ new_states)
34.191 + tmp_states = Map()
34.192 + System.err.println("assign_states: " + (System.currentTimeMillis - time0) + " ms elapsed time")
34.193 + }
34.194 +
34.195 + def current_state(cmd: Command): Option[State] =
34.196 + {
34.197 + require(assignment.is_finished)
34.198 + (assignment.join).get(cmd).map(_.current_state)
34.199 + }
34.200 +}
35.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
35.2 +++ b/src/Tools/jEdit/src/proofdocument/html_panel.scala Mon Jan 11 22:31:27 2010 +0100
35.3 @@ -0,0 +1,140 @@
35.4 +/*
35.5 + * HTML panel based on Lobo/Cobra
35.6 + *
35.7 + * @author Makarius
35.8 + */
35.9 +
35.10 +package isabelle.proofdocument
35.11 +
35.12 +
35.13 +import java.io.StringReader
35.14 +import java.awt.{BorderLayout, Dimension}
35.15 +import java.awt.event.MouseEvent
35.16 +
35.17 +import javax.swing.{JButton, JPanel, JScrollPane}
35.18 +import java.util.logging.{Logger, Level}
35.19 +
35.20 +import org.w3c.dom.html2.HTMLElement
35.21 +
35.22 +import org.lobobrowser.html.parser.{DocumentBuilderImpl, InputSourceImpl}
35.23 +import org.lobobrowser.html.gui.HtmlPanel
35.24 +import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl}
35.25 +import org.lobobrowser.html.test.{SimpleHtmlRendererContext, SimpleUserAgentContext}
35.26 +
35.27 +import scala.io.Source
35.28 +import scala.actors.Actor._
35.29 +
35.30 +
35.31 +object HTML_Panel
35.32 +{
35.33 + sealed abstract class Event { val element: HTMLElement; val mouse: MouseEvent }
35.34 + case class Context_Menu(val element: HTMLElement, mouse: MouseEvent) extends Event
35.35 + case class Mouse_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
35.36 + case class Double_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
35.37 + case class Mouse_Over(val element: HTMLElement, mouse: MouseEvent) extends Event
35.38 + case class Mouse_Out(val element: HTMLElement, mouse: MouseEvent) extends Event
35.39 +}
35.40 +
35.41 +
35.42 +class HTML_Panel(
35.43 + sys: Isabelle_System,
35.44 + initial_font_size: Int,
35.45 + handler: PartialFunction[HTML_Panel.Event, Unit]) extends HtmlPanel
35.46 +{
35.47 + // global logging
35.48 + Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
35.49 +
35.50 +
35.51 + /* document template */
35.52 +
35.53 + private def try_file(name: String): String =
35.54 + {
35.55 + val file = sys.platform_file(name)
35.56 + if (file.isFile) Source.fromFile(file).mkString else ""
35.57 + }
35.58 +
35.59 + private def template(font_size: Int): String =
35.60 + """<?xml version="1.0" encoding="utf-8"?>
35.61 +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
35.62 + "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
35.63 +<html xmlns="http://www.w3.org/1999/xhtml">
35.64 +<head>
35.65 +<style media="all" type="text/css">
35.66 +""" +
35.67 + try_file("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
35.68 + try_file("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
35.69 + "body { font-family: " + sys.font_family + "; font-size: " + font_size + "px }" +
35.70 +"""
35.71 +</style>
35.72 +</head>
35.73 +<body/>
35.74 +</html>
35.75 +"""
35.76 +
35.77 +
35.78 + /* actor with local state */
35.79 +
35.80 + private val ucontext = new SimpleUserAgentContext
35.81 +
35.82 + private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
35.83 + {
35.84 + private def handle(event: HTML_Panel.Event): Boolean =
35.85 + if (handler != null && handler.isDefinedAt(event)) { handler(event); true }
35.86 + else false
35.87 +
35.88 + override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean =
35.89 + handle(HTML_Panel.Context_Menu(elem, event))
35.90 + override def onMouseClick(elem: HTMLElement, event: MouseEvent): Boolean =
35.91 + handle(HTML_Panel.Mouse_Click(elem, event))
35.92 + override def onDoubleClick(elem: HTMLElement, event: MouseEvent): Boolean =
35.93 + handle(HTML_Panel.Double_Click(elem, event))
35.94 + override def onMouseOver(elem: HTMLElement, event: MouseEvent)
35.95 + { handle(HTML_Panel.Mouse_Over(elem, event)) }
35.96 + override def onMouseOut(elem: HTMLElement, event: MouseEvent)
35.97 + { handle(HTML_Panel.Mouse_Out(elem, event)) }
35.98 + }
35.99 +
35.100 + private val builder = new DocumentBuilderImpl(ucontext, rcontext)
35.101 +
35.102 + private case class Init(font_size: Int)
35.103 + private case class Render(body: List[XML.Tree])
35.104 +
35.105 + private val main_actor = actor {
35.106 + // crude double buffering
35.107 + var doc1: org.w3c.dom.Document = null
35.108 + var doc2: org.w3c.dom.Document = null
35.109 +
35.110 + loop {
35.111 + react {
35.112 + case Init(font_size) =>
35.113 + val src = template(font_size)
35.114 + def parse() =
35.115 + builder.parse(new InputSourceImpl(new StringReader(src), "http://localhost"))
35.116 + doc1 = parse()
35.117 + doc2 = parse()
35.118 + Swing_Thread.now { setDocument(doc1, rcontext) }
35.119 +
35.120 + case Render(body) =>
35.121 + val doc = doc2
35.122 + val node =
35.123 + XML.document_node(doc,
35.124 + XML.elem(HTML.BODY, body.map((t: XML.Tree) => XML.elem(HTML.PRE, HTML.spans(t)))))
35.125 + doc.removeChild(doc.getLastChild())
35.126 + doc.appendChild(node)
35.127 + doc2 = doc1
35.128 + doc1 = doc
35.129 + Swing_Thread.now { setDocument(doc1, rcontext) }
35.130 +
35.131 + case bad => System.err.println("main_actor: ignoring bad message " + bad)
35.132 + }
35.133 + }
35.134 + }
35.135 +
35.136 + main_actor ! Init(initial_font_size)
35.137 +
35.138 +
35.139 + /* main method wrappers */
35.140 +
35.141 + def init(font_size: Int) { main_actor ! Init(font_size) }
35.142 + def render(body: List[XML.Tree]) { main_actor ! Render(body) }
35.143 +}
36.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
36.2 +++ b/src/Tools/jEdit/src/proofdocument/markup_node.scala Mon Jan 11 22:31:27 2010 +0100
36.3 @@ -0,0 +1,111 @@
36.4 +/*
36.5 + * Document markup nodes, with connection to Swing tree model
36.6 + *
36.7 + * @author Fabian Immler, TU Munich
36.8 + * @author Makarius
36.9 + */
36.10 +
36.11 +package isabelle.proofdocument
36.12 +
36.13 +
36.14 +import javax.swing.tree.DefaultMutableTreeNode
36.15 +
36.16 +
36.17 +
36.18 +class Markup_Node(val start: Int, val stop: Int, val info: Any)
36.19 +{
36.20 + def fits_into(that: Markup_Node): Boolean =
36.21 + that.start <= this.start && this.stop <= that.stop
36.22 +}
36.23 +
36.24 +
36.25 +class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree])
36.26 +{
36.27 + def set_branches(bs: List[Markup_Tree]): Markup_Tree = new Markup_Tree(node, bs)
36.28 +
36.29 + private def add(branch: Markup_Tree) = // FIXME avoid sort
36.30 + set_branches((branch :: branches) sort ((a, b) => a.node.start < b.node.start))
36.31 +
36.32 + private def remove(bs: List[Markup_Tree]) = set_branches(branches -- bs)
36.33 +
36.34 + def + (new_tree: Markup_Tree): Markup_Tree =
36.35 + {
36.36 + val new_node = new_tree.node
36.37 + if (new_node fits_into node) {
36.38 + var inserted = false
36.39 + val new_branches =
36.40 + branches.map(branch =>
36.41 + if ((new_node fits_into branch.node) && !inserted) {
36.42 + inserted = true
36.43 + branch + new_tree
36.44 + }
36.45 + else branch)
36.46 + if (!inserted) {
36.47 + // new_tree did not fit into children of this
36.48 + // -> insert between this and its branches
36.49 + val fitting = branches filter(_.node fits_into new_node)
36.50 + (this remove fitting) add ((new_tree /: fitting)(_ + _))
36.51 + }
36.52 + else set_branches(new_branches)
36.53 + }
36.54 + else {
36.55 + System.err.println("ignored nonfitting markup: " + new_node)
36.56 + this
36.57 + }
36.58 + }
36.59 +
36.60 + def flatten: List[Markup_Node] =
36.61 + {
36.62 + var next_x = node.start
36.63 + if (branches.isEmpty) List(this.node)
36.64 + else {
36.65 + val filled_gaps =
36.66 + for {
36.67 + child <- branches
36.68 + markups =
36.69 + if (next_x < child.node.start)
36.70 + new Markup_Node(next_x, child.node.start, node.info) :: child.flatten
36.71 + else child.flatten
36.72 + update = (next_x = child.node.stop)
36.73 + markup <- markups
36.74 + } yield markup
36.75 + if (next_x < node.stop)
36.76 + filled_gaps + new Markup_Node(next_x, node.stop, node.info)
36.77 + else filled_gaps
36.78 + }
36.79 + }
36.80 +}
36.81 +
36.82 +
36.83 +class Markup_Text(val markup: List[Markup_Tree], val content: String)
36.84 +{
36.85 + private lazy val root =
36.86 + new Markup_Tree(new Markup_Node(0, content.length, None), markup)
36.87 +
36.88 + def + (new_tree: Markup_Tree): Markup_Text =
36.89 + new Markup_Text((root + new_tree).branches, content)
36.90 +
36.91 + def filter(pred: Markup_Node => Boolean): Markup_Text =
36.92 + {
36.93 + def filt(tree: Markup_Tree): List[Markup_Tree] =
36.94 + {
36.95 + val branches = tree.branches.flatMap(filt(_))
36.96 + if (pred(tree.node)) List(tree.set_branches(branches))
36.97 + else branches
36.98 + }
36.99 + new Markup_Text(markup.flatMap(filt(_)), content)
36.100 + }
36.101 +
36.102 + def flatten: List[Markup_Node] = markup.flatten(_.flatten)
36.103 +
36.104 + def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode =
36.105 + {
36.106 + def swing(tree: Markup_Tree): DefaultMutableTreeNode =
36.107 + {
36.108 + val node = swing_node(tree.node)
36.109 + tree.branches foreach ((branch: Markup_Tree) => node.add(swing(branch)))
36.110 + node
36.111 + }
36.112 + swing(root)
36.113 + }
36.114 +}
37.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
37.2 +++ b/src/Tools/jEdit/src/proofdocument/session.scala Mon Jan 11 22:31:27 2010 +0100
37.3 @@ -0,0 +1,250 @@
37.4 +/*
37.5 + * Isabelle session, potentially with running prover
37.6 + *
37.7 + * @author Makarius
37.8 + */
37.9 +
37.10 +package isabelle.proofdocument
37.11 +
37.12 +
37.13 +import scala.actors.TIMEOUT
37.14 +import scala.actors.Actor._
37.15 +
37.16 +
37.17 +object Session
37.18 +{
37.19 + /* events */
37.20 +
37.21 + case object Global_Settings
37.22 +
37.23 +
37.24 + /* managed entities */
37.25 +
37.26 + type Entity_ID = String
37.27 +
37.28 + trait Entity
37.29 + {
37.30 + val id: Entity_ID
37.31 + def consume(session: Session, message: XML.Tree): Unit
37.32 + }
37.33 +}
37.34 +
37.35 +
37.36 +class Session(system: Isabelle_System)
37.37 +{
37.38 + /* pervasive event buses */
37.39 +
37.40 + val global_settings = new Event_Bus[Session.Global_Settings.type]
37.41 + val raw_results = new Event_Bus[Isabelle_Process.Result]
37.42 + val results = new Event_Bus[Command]
37.43 +
37.44 + val command_change = new Event_Bus[Command]
37.45 +
37.46 +
37.47 + /* unique ids */
37.48 +
37.49 + private var id_count: BigInt = 0
37.50 + def create_id(): Session.Entity_ID = synchronized { id_count += 1; "j" + id_count }
37.51 +
37.52 +
37.53 +
37.54 + /** main actor **/
37.55 +
37.56 + @volatile private var syntax = new Outer_Syntax(system.symbols)
37.57 + def current_syntax: Outer_Syntax = syntax
37.58 +
37.59 + @volatile private var entities = Map[Session.Entity_ID, Session.Entity]()
37.60 + def lookup_entity(id: Session.Entity_ID): Option[Session.Entity] = entities.get(id)
37.61 + def lookup_command(id: Session.Entity_ID): Option[Command] =
37.62 + lookup_entity(id) match {
37.63 + case Some(cmd: Command) => Some(cmd)
37.64 + case _ => None
37.65 + }
37.66 +
37.67 + private case class Start(timeout: Int, args: List[String])
37.68 + private case object Stop
37.69 + private case class Begin_Document(path: String)
37.70 +
37.71 + private val session_actor = actor {
37.72 +
37.73 + var prover: Isabelle_Process with Isar_Document = null
37.74 +
37.75 + def register(entity: Session.Entity) { entities += (entity.id -> entity) }
37.76 +
37.77 + var documents = Map[Isar_Document.Document_ID, Document]()
37.78 + def register_document(doc: Document) { documents += (doc.id -> doc) }
37.79 +
37.80 +
37.81 + /* document changes */
37.82 +
37.83 + def handle_change(change: Change)
37.84 + {
37.85 + require(change.parent.isDefined)
37.86 +
37.87 + val (changes, doc) = change.result.join
37.88 + val id_changes = changes map {
37.89 + case (c1, c2) =>
37.90 + (c1.map(_.id).getOrElse(""),
37.91 + c2 match {
37.92 + case None => None
37.93 + case Some(command) =>
37.94 + if (!lookup_command(command.id).isDefined) {
37.95 + register(command)
37.96 + prover.define_command(command.id, system.symbols.encode(command.source))
37.97 + }
37.98 + Some(command.id)
37.99 + })
37.100 + }
37.101 + register_document(doc)
37.102 + prover.edit_document(change.parent.get.id, doc.id, id_changes)
37.103 + }
37.104 +
37.105 +
37.106 + /* prover results */
37.107 +
37.108 + def bad_result(result: Isabelle_Process.Result)
37.109 + {
37.110 + System.err.println("Ignoring prover result: " + result)
37.111 + }
37.112 +
37.113 + def handle_result(result: Isabelle_Process.Result)
37.114 + {
37.115 + raw_results.event(result)
37.116 +
37.117 + val target_id: Option[Session.Entity_ID] = Position.get_id(result.props)
37.118 + val target: Option[Session.Entity] =
37.119 + target_id match {
37.120 + case None => None
37.121 + case Some(id) => lookup_entity(id)
37.122 + }
37.123 + if (target.isDefined) target.get.consume(this, result.message)
37.124 + else if (result.kind == Isabelle_Process.Kind.STATUS) {
37.125 + // global status message
37.126 + result.body match {
37.127 +
37.128 + // document state assigment
37.129 + case List(XML.Elem(Markup.ASSIGN, _, edits)) if target_id.isDefined =>
37.130 + documents.get(target_id.get) match {
37.131 + case Some(doc) =>
37.132 + val states =
37.133 + for {
37.134 + XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
37.135 + <- edits
37.136 + cmd <- lookup_command(cmd_id)
37.137 + } yield {
37.138 + val st = cmd.assign_state(state_id)
37.139 + register(st)
37.140 + (cmd, st)
37.141 + }
37.142 + doc.assign_states(states)
37.143 + case None => bad_result(result)
37.144 + }
37.145 +
37.146 + // command and keyword declarations
37.147 + case List(XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _)) =>
37.148 + syntax += (name, kind)
37.149 + case List(XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _)) =>
37.150 + syntax += name
37.151 +
37.152 + case _ => if (!result.is_ready) bad_result(result)
37.153 + }
37.154 + }
37.155 + else if (result.kind == Isabelle_Process.Kind.EXIT)
37.156 + prover = null
37.157 + else if (result.kind != Isabelle_Process.Kind.STDIN && !result.is_raw)
37.158 + bad_result(result)
37.159 + }
37.160 +
37.161 +
37.162 + /* prover startup */
37.163 +
37.164 + def startup_error(): String =
37.165 + {
37.166 + val buf = new StringBuilder
37.167 + while (
37.168 + receiveWithin(0) {
37.169 + case result: Isabelle_Process.Result =>
37.170 + if (result.is_raw) {
37.171 + for (text <- XML.content(result.message))
37.172 + buf.append(text)
37.173 + }
37.174 + true
37.175 + case TIMEOUT => false
37.176 + }) {}
37.177 + buf.toString
37.178 + }
37.179 +
37.180 + def prover_startup(timeout: Int): Option[String] =
37.181 + {
37.182 + receiveWithin(timeout) {
37.183 + case result: Isabelle_Process.Result
37.184 + if result.kind == Isabelle_Process.Kind.INIT =>
37.185 + while (receive {
37.186 + case result: Isabelle_Process.Result =>
37.187 + handle_result(result); !result.is_ready
37.188 + }) {}
37.189 + None
37.190 +
37.191 + case result: Isabelle_Process.Result
37.192 + if result.kind == Isabelle_Process.Kind.EXIT =>
37.193 + Some(startup_error())
37.194 +
37.195 + case TIMEOUT => // FIXME clarify
37.196 + prover.kill; Some(startup_error())
37.197 + }
37.198 + }
37.199 +
37.200 +
37.201 + /* main loop */
37.202 +
37.203 + val xml_cache = new XML.Cache(131071)
37.204 +
37.205 + loop {
37.206 + react {
37.207 + case Start(timeout, args) =>
37.208 + if (prover == null) {
37.209 + prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
37.210 + val origin = sender
37.211 + val opt_err = prover_startup(timeout)
37.212 + if (opt_err.isDefined) prover = null
37.213 + origin ! opt_err
37.214 + }
37.215 + else reply(None)
37.216 +
37.217 + case Stop => // FIXME clarify; synchronous
37.218 + if (prover != null) {
37.219 + prover.kill
37.220 + prover = null
37.221 + }
37.222 +
37.223 + case Begin_Document(path: String) if prover != null =>
37.224 + val id = create_id()
37.225 + val doc = Document.empty(id)
37.226 + register_document(doc)
37.227 + prover.begin_document(id, path)
37.228 + reply(doc)
37.229 +
37.230 + case change: Change if prover != null =>
37.231 + handle_change(change)
37.232 +
37.233 + case result: Isabelle_Process.Result =>
37.234 + handle_result(result.cache(xml_cache))
37.235 +
37.236 + case bad if prover != null =>
37.237 + System.err.println("session_actor: ignoring bad message " + bad)
37.238 + }
37.239 + }
37.240 + }
37.241 +
37.242 +
37.243 + /* main methods */
37.244 +
37.245 + def start(timeout: Int, args: List[String]): Option[String] =
37.246 + (session_actor !? Start(timeout, args)).asInstanceOf[Option[String]]
37.247 +
37.248 + def stop() { session_actor ! Stop }
37.249 + def input(change: Change) { session_actor ! change }
37.250 +
37.251 + def begin_document(path: String): Document =
37.252 + (session_actor !? Begin_Document(path)).asInstanceOf[Document]
37.253 +}
38.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
38.2 +++ b/src/Tools/jEdit/src/proofdocument/state.scala Mon Jan 11 22:31:27 2010 +0100
38.3 @@ -0,0 +1,117 @@
38.4 +/*
38.5 + * Accumulating results from prover
38.6 + *
38.7 + * @author Fabian Immler, TU Munich
38.8 + * @author Makarius
38.9 + */
38.10 +
38.11 +package isabelle.proofdocument
38.12 +
38.13 +
38.14 +class State(
38.15 + val command: Command,
38.16 + val status: Command.Status.Value,
38.17 + val rev_results: List[XML.Tree],
38.18 + val markup_root: Markup_Text)
38.19 +{
38.20 + def this(command: Command) =
38.21 + this(command, Command.Status.UNPROCESSED, Nil, command.empty_markup)
38.22 +
38.23 +
38.24 + /* content */
38.25 +
38.26 + private def set_status(st: Command.Status.Value): State =
38.27 + new State(command, st, rev_results, markup_root)
38.28 +
38.29 + private def add_result(res: XML.Tree): State =
38.30 + new State(command, status, res :: rev_results, markup_root)
38.31 +
38.32 + private def add_markup(node: Markup_Tree): State =
38.33 + new State(command, status, rev_results, markup_root + node)
38.34 +
38.35 + lazy val results = rev_results.reverse
38.36 +
38.37 +
38.38 + /* markup */
38.39 +
38.40 + lazy val highlight: Markup_Text =
38.41 + {
38.42 + markup_root.filter(_.info match {
38.43 + case Command.HighlightInfo(_) => true
38.44 + case _ => false
38.45 + })
38.46 + }
38.47 +
38.48 + private lazy val types: List[Markup_Node] =
38.49 + markup_root.filter(_.info match {
38.50 + case Command.TypeInfo(_) => true
38.51 + case _ => false }).flatten
38.52 +
38.53 + def type_at(pos: Int): Option[String] =
38.54 + {
38.55 + types.find(t => t.start <= pos && pos < t.stop) match {
38.56 + case Some(t) =>
38.57 + t.info match {
38.58 + case Command.TypeInfo(ty) => Some(command.source(t.start, t.stop) + ": " + ty)
38.59 + case _ => None
38.60 + }
38.61 + case None => None
38.62 + }
38.63 + }
38.64 +
38.65 + private lazy val refs: List[Markup_Node] =
38.66 + markup_root.filter(_.info match {
38.67 + case Command.RefInfo(_, _, _, _) => true
38.68 + case _ => false }).flatten
38.69 +
38.70 + def ref_at(pos: Int): Option[Markup_Node] =
38.71 + refs.find(t => t.start <= pos && pos < t.stop)
38.72 +
38.73 +
38.74 + /* message dispatch */
38.75 +
38.76 + def + (session: Session, message: XML.Tree): State =
38.77 + {
38.78 + val changed: State =
38.79 + message match {
38.80 + case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) =>
38.81 + (this /: elems)((state, elem) =>
38.82 + elem match {
38.83 + case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
38.84 + case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
38.85 + case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
38.86 + case XML.Elem(kind, atts, body) =>
38.87 + val (begin, end) = Position.get_offsets(atts)
38.88 + if (begin.isEmpty || end.isEmpty) state
38.89 + else if (kind == Markup.ML_TYPING) {
38.90 + val info = body.first.asInstanceOf[XML.Text].content // FIXME proper match!?
38.91 + state.add_markup(
38.92 + command.markup_node(begin.get - 1, end.get - 1, Command.TypeInfo(info)))
38.93 + }
38.94 + else if (kind == Markup.ML_REF) {
38.95 + body match {
38.96 + case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
38.97 + state.add_markup(command.markup_node(
38.98 + begin.get - 1, end.get - 1,
38.99 + Command.RefInfo(
38.100 + Position.get_file(atts),
38.101 + Position.get_line(atts),
38.102 + Position.get_id(atts),
38.103 + Position.get_offset(atts))))
38.104 + case _ => state
38.105 + }
38.106 + }
38.107 + else {
38.108 + state.add_markup(
38.109 + command.markup_node(begin.get - 1, end.get - 1, Command.HighlightInfo(kind)))
38.110 + }
38.111 + case _ =>
38.112 + System.err.println("ignored status report: " + elem)
38.113 + state
38.114 + })
38.115 + case _ => add_result(message)
38.116 + }
38.117 + if (!(this eq changed)) session.command_change.event(command)
38.118 + changed
38.119 + }
38.120 +}