--- a/.hgignore Thu Jul 15 16:11:52 2021 +0200
+++ b/.hgignore Thu Jul 15 22:51:49 2021 +0200
@@ -17,7 +17,6 @@
^browser_info/
^doc/.*\.pdf
^lib/classes/
-^src/Tools/jEdit/dist/
^src/Tools/VSCode/out/
^src/Tools/VSCode/extension/node_modules/
^Admin/jenkins/ci-extras/target/
--- a/Admin/Release/CHECKLIST Thu Jul 15 16:11:52 2021 +0200
+++ b/Admin/Release/CHECKLIST Thu Jul 15 22:51:49 2021 +0200
@@ -15,6 +15,8 @@
- test Isabelle/jEdit: print buffer
+- test Isabelle/jEdit: deactivate main plugin;
+
- test "#!/usr/bin/env isabelle_scala_script";
- test Windows 10 subsystem for Linux:
@@ -43,7 +45,7 @@
- update https://isabelle.sketis.net/repos/isabelle-website
-- check doc/Contents, src/Tools/jEdit/dist/doc/Contents;
+- check doc/Contents, $JEDIT_HOME/doc/Contents;
- test old HD display: Linux, Windows, macOS;
--- a/Admin/Windows/launch4j/isabelle.xml Thu Jul 15 16:11:52 2021 +0200
+++ b/Admin/Windows/launch4j/isabelle.xml Thu Jul 15 22:51:49 2021 +0200
@@ -15,7 +15,7 @@
<manifest></manifest>
<icon>{ICON}</icon>
<classPath>
- <mainClass>isabelle.Main</mainClass>
+ <mainClass>isabelle.jedit.Main</mainClass>
{CLASSPATH}
</classPath>
<singleInstance>
--- a/Admin/build Thu Jul 15 16:11:52 2021 +0200
+++ b/Admin/build Thu Jul 15 22:51:49 2021 +0200
@@ -52,7 +52,7 @@
function build_all ()
{
build_browser
- build_jars
+ build_setup build
}
@@ -64,28 +64,25 @@
}
-function build_jars ()
+function build_setup ()
{
- pushd "$ISABELLE_HOME" >/dev/null
- "$ISABELLE_TOOL" env src/Pure/build-jars "$@" || exit $?
- popd >/dev/null
+ rm -rf \
+ "$ISABELLE_HOME/lib/classes/Pure.jar" \
+ "$ISABELLE_HOME/lib/classes/Pure.shasum" \
+ "$ISABELLE_HOME/src/Tools/jEdit/dist"
+ env ISABELLE_SETUP_CLASSPATH_SKIP=true "$ISABELLE_TOOL" java isabelle.setup.Setup "$@"
}
## main
-#FIXME workarounds for scalac 2.11.0
-export CYGWIN="nodosfilewarning"
-function stty() { :; }
-export -f stty
-
for MODULE in $MODULES
do
case $MODULE in
all) build_all;;
browser) build_browser;;
- jars) build_jars;;
- jars_fresh) build_jars -f;;
+ jars) build_setup build;;
+ jars_fresh) build_setup build_fresh;;
*) fail "Bad module $MODULE"
esac
done
--- a/Admin/components/components.sha1 Thu Jul 15 16:11:52 2021 +0200
+++ b/Admin/components/components.sha1 Thu Jul 15 22:51:49 2021 +0200
@@ -125,6 +125,7 @@
c611e363287fcc9bdd93c33bef85fa4e66cd3f37 isabelle_setup-20210701.tar.gz
a0e7527448ef0f7ce164a38a50dc26e98de3cad6 isabelle_setup-20210709.tar.gz
e413706694b0968245ee15183af2d464814ce0a4 isabelle_setup-20210711.tar.gz
+d2c9fd7b73457a460111edd6eb93a133272935fb isabelle_setup-20210715.tar.gz
0b2206f914336dec4923dd0479d8cee4b904f544 jdk-11+28.tar.gz
e12574d838ed55ef2845acf1152329572ab0cc56 jdk-11.0.10+9.tar.gz
3e05213cad47dbef52804fe329395db9b4e57f39 jdk-11.0.2+9.tar.gz
@@ -168,6 +169,7 @@
dfb087bd64c3e5da79430e0ba706b9abc559c090 jdk-8u66.tar.gz
2ac389babd15aa5ddd1a424c1509e1c459e6fbb1 jdk-8u72.tar.gz
caa0cf65481b6207f66437576643f41dabae3c83 jdk-8u92.tar.gz
+778fd85c827ec49d2d658a832d20e63916186b0d jedit-20210715.tar.gz
44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz
a242a688810f2bccf24587b0062ce8027bf77fa2 jedit_build-20120304.tar.gz
4c948dee53f74361c097c08f49a1a5ff9b17bd1d jedit_build-20120307.tar.gz
--- a/Admin/components/main Thu Jul 15 16:11:52 2021 +0200
+++ b/Admin/components/main Thu Jul 15 22:51:49 2021 +0200
@@ -8,9 +8,9 @@
flatlaf-1.2
idea-icons-20210508
isabelle_fonts-20210322
-isabelle_setup-20210711
+isabelle_setup-20210715
jdk-15.0.2+7
-jedit_build-20210708
+jedit-20210715
jfreechart-1.5.1
jortho-1.0-2
kodkodi-1.5.6-1
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/etc/build.props Thu Jul 15 22:51:49 2021 +0200
@@ -0,0 +1,4 @@
+description = Isabelle/Scala/Admin
+lib = $ISABELLE_HOME/lib/classes
+name = isabelle_admin
+services = isabelle.Admin_Tools
--- a/NEWS Thu Jul 15 16:11:52 2021 +0200
+++ b/NEWS Thu Jul 15 22:51:49 2021 +0200
@@ -33,6 +33,9 @@
* Support for built-in font substitution of jEdit text area.
+* The main plugin for Isabelle/jEdit can be deactivated and reactivated
+as documented --- was broken at least since Isabelle2018.
+
*** Document preparation ***
--- a/bin/isabelle_java Thu Jul 15 16:11:52 2021 +0200
+++ b/bin/isabelle_java Thu Jul 15 22:51:49 2021 +0200
@@ -18,11 +18,8 @@
eval "declare -a JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS $ISABELLE_TOOL_JAVA_OPTIONS)"
- if [ -f "$ISABELLE_HOME/src/Tools/jEdit/dist/jedit.jar" ]; then
- classpath "$ISABELLE_HOME/src/Tools/jEdit/dist/jedit.jar"
- fi
-
- [ -n "$CLASSPATH" ] && classpath "$CLASSPATH"
+ classpath "$ISABELLE_SETUP_CLASSPATH"
+ classpath "$CLASSPATH"
echo "$ISABELLE_ROOT"
echo "$CYGWIN_ROOT"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/etc/build.props Thu Jul 15 22:51:49 2021 +0200
@@ -0,0 +1,292 @@
+description = Isabelle/Scala
+lib = lib/classes
+name = isabelle
+main = isabelle.jedit.Main
+resources = \
+ lib/services/java.nio.charset.spi.CharsetProvider:META-INF/services/ \
+ lib/logo/isabelle_transparent-32.gif:isabelle/ \
+ lib/logo/isabelle_transparent.gif:isabelle/
+sources = \
+ src/HOL/SPARK/Tools/spark.scala \
+ src/HOL/Tools/ATP/system_on_tptp.scala \
+ src/HOL/Tools/Mirabelle/mirabelle.scala \
+ src/HOL/Tools/Nitpick/kodkod.scala \
+ src/Pure/Admin/afp.scala \
+ src/Pure/Admin/build_csdp.scala \
+ src/Pure/Admin/build_cygwin.scala \
+ src/Pure/Admin/build_doc.scala \
+ src/Pure/Admin/build_e.scala \
+ src/Pure/Admin/build_fonts.scala \
+ src/Pure/Admin/build_history.scala \
+ src/Pure/Admin/build_jcef.scala \
+ src/Pure/Admin/build_jdk.scala \
+ src/Pure/Admin/build_jedit.scala \
+ src/Pure/Admin/build_log.scala \
+ src/Pure/Admin/build_polyml.scala \
+ src/Pure/Admin/build_release.scala \
+ src/Pure/Admin/build_spass.scala \
+ src/Pure/Admin/build_sqlite.scala \
+ src/Pure/Admin/build_status.scala \
+ src/Pure/Admin/build_vampire.scala \
+ src/Pure/Admin/build_verit.scala \
+ src/Pure/Admin/build_zipperposition.scala \
+ src/Pure/Admin/check_sources.scala \
+ src/Pure/Admin/ci_profile.scala \
+ src/Pure/Admin/isabelle_cronjob.scala \
+ src/Pure/Admin/isabelle_devel.scala \
+ src/Pure/Admin/jenkins.scala \
+ src/Pure/Admin/other_isabelle.scala \
+ src/Pure/Concurrent/consumer_thread.scala \
+ src/Pure/Concurrent/counter.scala \
+ src/Pure/Concurrent/delay.scala \
+ src/Pure/Concurrent/event_timer.scala \
+ src/Pure/Concurrent/future.scala \
+ src/Pure/Concurrent/isabelle_thread.scala \
+ src/Pure/Concurrent/mailbox.scala \
+ src/Pure/Concurrent/par_list.scala \
+ src/Pure/Concurrent/synchronized.scala \
+ src/Pure/GUI/color_value.scala \
+ src/Pure/GUI/desktop_app.scala \
+ src/Pure/GUI/gui.scala \
+ src/Pure/GUI/gui_thread.scala \
+ src/Pure/GUI/popup.scala \
+ src/Pure/GUI/wrap_panel.scala \
+ src/Pure/General/antiquote.scala \
+ src/Pure/General/bytes.scala \
+ src/Pure/General/cache.scala \
+ src/Pure/General/codepoint.scala \
+ src/Pure/General/comment.scala \
+ src/Pure/General/completion.scala \
+ src/Pure/General/csv.scala \
+ src/Pure/General/date.scala \
+ src/Pure/General/exn.scala \
+ src/Pure/General/file.scala \
+ src/Pure/General/file_watcher.scala \
+ src/Pure/General/graph.scala \
+ src/Pure/General/graph_display.scala \
+ src/Pure/General/graphics_file.scala \
+ src/Pure/General/http.scala \
+ src/Pure/General/json.scala \
+ src/Pure/General/linear_set.scala \
+ src/Pure/General/logger.scala \
+ src/Pure/General/long_name.scala \
+ src/Pure/General/mailman.scala \
+ src/Pure/General/mercurial.scala \
+ src/Pure/General/multi_map.scala \
+ src/Pure/General/output.scala \
+ src/Pure/General/path.scala \
+ src/Pure/General/position.scala \
+ src/Pure/General/pretty.scala \
+ src/Pure/General/properties.scala \
+ src/Pure/General/rdf.scala \
+ src/Pure/General/scan.scala \
+ src/Pure/General/sha1.scala \
+ src/Pure/General/sql.scala \
+ src/Pure/General/ssh.scala \
+ src/Pure/General/symbol.scala \
+ src/Pure/General/time.scala \
+ src/Pure/General/timing.scala \
+ src/Pure/General/untyped.scala \
+ src/Pure/General/url.scala \
+ src/Pure/General/utf8.scala \
+ src/Pure/General/uuid.scala \
+ src/Pure/General/value.scala \
+ src/Pure/General/word.scala \
+ src/Pure/General/xz.scala \
+ src/Pure/Isar/document_structure.scala \
+ src/Pure/Isar/keyword.scala \
+ src/Pure/Isar/line_structure.scala \
+ src/Pure/Isar/outer_syntax.scala \
+ src/Pure/Isar/parse.scala \
+ src/Pure/Isar/token.scala \
+ src/Pure/ML/ml_console.scala \
+ src/Pure/ML/ml_lex.scala \
+ src/Pure/ML/ml_process.scala \
+ src/Pure/ML/ml_profiling.scala \
+ src/Pure/ML/ml_statistics.scala \
+ src/Pure/ML/ml_syntax.scala \
+ src/Pure/PIDE/byte_message.scala \
+ src/Pure/PIDE/command.scala \
+ src/Pure/PIDE/command_span.scala \
+ src/Pure/PIDE/document.scala \
+ src/Pure/PIDE/document_id.scala \
+ src/Pure/PIDE/document_status.scala \
+ src/Pure/PIDE/editor.scala \
+ src/Pure/PIDE/headless.scala \
+ src/Pure/PIDE/line.scala \
+ src/Pure/PIDE/markup.scala \
+ src/Pure/PIDE/markup_tree.scala \
+ src/Pure/PIDE/protocol.scala \
+ src/Pure/PIDE/protocol_handlers.scala \
+ src/Pure/PIDE/protocol_message.scala \
+ src/Pure/PIDE/prover.scala \
+ src/Pure/PIDE/query_operation.scala \
+ src/Pure/PIDE/rendering.scala \
+ src/Pure/PIDE/resources.scala \
+ src/Pure/PIDE/session.scala \
+ src/Pure/PIDE/text.scala \
+ src/Pure/PIDE/xml.scala \
+ src/Pure/PIDE/yxml.scala \
+ src/Pure/ROOT.scala \
+ src/Pure/System/bash.scala \
+ src/Pure/System/command_line.scala \
+ src/Pure/System/components.scala \
+ src/Pure/System/executable.scala \
+ src/Pure/System/getopts.scala \
+ src/Pure/System/isabelle_charset.scala \
+ src/Pure/System/isabelle_fonts.scala \
+ src/Pure/System/isabelle_platform.scala \
+ src/Pure/System/isabelle_process.scala \
+ src/Pure/System/isabelle_system.scala \
+ src/Pure/System/isabelle_tool.scala \
+ src/Pure/System/java_statistics.scala \
+ src/Pure/System/linux.scala \
+ src/Pure/System/mingw.scala \
+ src/Pure/System/numa.scala \
+ src/Pure/System/options.scala \
+ src/Pure/System/platform.scala \
+ src/Pure/System/posix_interrupt.scala \
+ src/Pure/System/process_result.scala \
+ src/Pure/System/progress.scala \
+ src/Pure/System/scala.scala \
+ src/Pure/System/system_channel.scala \
+ src/Pure/System/tty_loop.scala \
+ src/Pure/Thy/bibtex.scala \
+ src/Pure/Thy/document_build.scala \
+ src/Pure/Thy/export.scala \
+ src/Pure/Thy/export_theory.scala \
+ src/Pure/Thy/file_format.scala \
+ src/Pure/Thy/html.scala \
+ src/Pure/Thy/latex.scala \
+ src/Pure/Thy/presentation.scala \
+ src/Pure/Thy/sessions.scala \
+ src/Pure/Thy/thy_element.scala \
+ src/Pure/Thy/thy_header.scala \
+ src/Pure/Thy/thy_syntax.scala \
+ src/Pure/Tools/build.scala \
+ src/Pure/Tools/build_docker.scala \
+ src/Pure/Tools/build_job.scala \
+ src/Pure/Tools/check_keywords.scala \
+ src/Pure/Tools/debugger.scala \
+ src/Pure/Tools/doc.scala \
+ src/Pure/Tools/dump.scala \
+ src/Pure/Tools/fontforge.scala \
+ src/Pure/Tools/java_monitor.scala \
+ src/Pure/Tools/logo.scala \
+ src/Pure/Tools/mkroot.scala \
+ src/Pure/Tools/phabricator.scala \
+ src/Pure/Tools/print_operation.scala \
+ src/Pure/Tools/profiling_report.scala \
+ src/Pure/Tools/scala_project.scala \
+ src/Pure/Tools/server.scala \
+ src/Pure/Tools/server_commands.scala \
+ src/Pure/Tools/simplifier_trace.scala \
+ src/Pure/Tools/spell_checker.scala \
+ src/Pure/Tools/task_statistics.scala \
+ src/Pure/Tools/update.scala \
+ src/Pure/Tools/update_cartouches.scala \
+ src/Pure/Tools/update_comments.scala \
+ src/Pure/Tools/update_header.scala \
+ src/Pure/Tools/update_then.scala \
+ src/Pure/Tools/update_theorems.scala \
+ src/Pure/library.scala \
+ src/Pure/pure_thy.scala \
+ src/Pure/term.scala \
+ src/Pure/term_xml.scala \
+ src/Pure/thm_name.scala \
+ src/Tools/Graphview/graph_file.scala \
+ src/Tools/Graphview/graph_panel.scala \
+ src/Tools/Graphview/graphview.scala \
+ src/Tools/Graphview/layout.scala \
+ src/Tools/Graphview/main_panel.scala \
+ src/Tools/Graphview/metrics.scala \
+ src/Tools/Graphview/model.scala \
+ src/Tools/Graphview/mutator.scala \
+ src/Tools/Graphview/mutator_dialog.scala \
+ src/Tools/Graphview/mutator_event.scala \
+ src/Tools/Graphview/popups.scala \
+ src/Tools/Graphview/shapes.scala \
+ src/Tools/Graphview/tree_panel.scala \
+ src/Tools/VSCode/src/build_vscode.scala \
+ src/Tools/VSCode/src/channel.scala \
+ src/Tools/VSCode/src/dynamic_output.scala \
+ src/Tools/VSCode/src/language_server.scala \
+ src/Tools/VSCode/src/lsp.scala \
+ src/Tools/VSCode/src/preview_panel.scala \
+ src/Tools/VSCode/src/state_panel.scala \
+ src/Tools/VSCode/src/textmate_grammar.scala \
+ src/Tools/VSCode/src/vscode_model.scala \
+ src/Tools/VSCode/src/vscode_rendering.scala \
+ src/Tools/VSCode/src/vscode_resources.scala \
+ src/Tools/VSCode/src/vscode_spell_checker.scala \
+ src/Tools/jEdit/src/active.scala \
+ src/Tools/jEdit/src/base_plugin.scala \
+ src/Tools/jEdit/src/completion_popup.scala \
+ src/Tools/jEdit/src/context_menu.scala \
+ src/Tools/jEdit/src/debugger_dockable.scala \
+ src/Tools/jEdit/src/dockable.scala \
+ src/Tools/jEdit/src/document_model.scala \
+ src/Tools/jEdit/src/document_view.scala \
+ src/Tools/jEdit/src/documentation_dockable.scala \
+ src/Tools/jEdit/src/fold_handling.scala \
+ src/Tools/jEdit/src/font_info.scala \
+ src/Tools/jEdit/src/graphview_dockable.scala \
+ src/Tools/jEdit/src/info_dockable.scala \
+ src/Tools/jEdit/src/isabelle.scala \
+ src/Tools/jEdit/src/isabelle_encoding.scala \
+ src/Tools/jEdit/src/isabelle_export.scala \
+ src/Tools/jEdit/src/isabelle_options.scala \
+ src/Tools/jEdit/src/isabelle_session.scala \
+ src/Tools/jEdit/src/isabelle_vfs.scala \
+ src/Tools/jEdit/src/jedit_bibtex.scala \
+ src/Tools/jEdit/src/jedit_editor.scala \
+ src/Tools/jEdit/src/jedit_lib.scala \
+ src/Tools/jEdit/src/jedit_options.scala \
+ src/Tools/jEdit/src/jedit_rendering.scala \
+ src/Tools/jEdit/src/jedit_resources.scala \
+ src/Tools/jEdit/src/jedit_sessions.scala \
+ src/Tools/jEdit/src/jedit_spell_checker.scala \
+ src/Tools/jEdit/src/keymap_merge.scala \
+ src/Tools/jEdit/src/main.scala \
+ src/Tools/jEdit/src/main_plugin.scala \
+ src/Tools/jEdit/src/monitor_dockable.scala \
+ src/Tools/jEdit/src/output_dockable.scala \
+ src/Tools/jEdit/src/pide_docking_framework.scala \
+ src/Tools/jEdit/src/pretty_text_area.scala \
+ src/Tools/jEdit/src/pretty_tooltip.scala \
+ src/Tools/jEdit/src/process_indicator.scala \
+ src/Tools/jEdit/src/protocol_dockable.scala \
+ src/Tools/jEdit/src/query_dockable.scala \
+ src/Tools/jEdit/src/raw_output_dockable.scala \
+ src/Tools/jEdit/src/rich_text_area.scala \
+ src/Tools/jEdit/src/session_build.scala \
+ src/Tools/jEdit/src/simplifier_trace_dockable.scala \
+ src/Tools/jEdit/src/simplifier_trace_window.scala \
+ src/Tools/jEdit/src/sledgehammer_dockable.scala \
+ src/Tools/jEdit/src/state_dockable.scala \
+ src/Tools/jEdit/src/status_widget.scala \
+ src/Tools/jEdit/src/symbols_dockable.scala \
+ src/Tools/jEdit/src/syntax_style.scala \
+ src/Tools/jEdit/src/syslog_dockable.scala \
+ src/Tools/jEdit/src/text_overview.scala \
+ src/Tools/jEdit/src/text_structure.scala \
+ src/Tools/jEdit/src/theories_dockable.scala \
+ src/Tools/jEdit/src/timing_dockable.scala \
+ src/Tools/jEdit/src/token_markup.scala
+services = \
+ isabelle.Bibtex$File_Format \
+ isabelle.Document_Build$Build_Engine \
+ isabelle.Document_Build$LuaLaTeX_Engine \
+ isabelle.Document_Build$PDFLaTeX_Engine \
+ isabelle.ML_Statistics$Handler \
+ isabelle.Print_Operation$Handler \
+ isabelle.Scala$Handler \
+ isabelle.Scala_Functions \
+ isabelle.Server_Commands \
+ isabelle.Sessions$File_Format \
+ isabelle.Simplifier_Trace$Handler \
+ isabelle.Tools \
+ isabelle.nitpick.Kodkod$Handler \
+ isabelle.nitpick.Scala_Functions \
+ isabelle.spark.SPARK$Load_Command1 \
+ isabelle.spark.SPARK$Load_Command2
--- a/etc/settings Thu Jul 15 16:11:52 2021 +0200
+++ b/etc/settings Thu Jul 15 22:51:49 2021 +0200
@@ -19,25 +19,7 @@
ISABELLE_JAVAC_OPTIONS="-encoding UTF-8 -Xlint:-options -deprecation -source 11 -target 11"
ISABELLE_SCALAC_OPTIONS="-encoding UTF-8 -Wconf:cat=other-match-analysis:silent -feature -deprecation -target:11 -Xsource:3 -J-Xms512m -J-Xmx4g -J-Xss16m"
-classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
-
-isabelle_scala_service 'isabelle.Tools'
-[ -d "$ISABELLE_HOME/Admin" ] && isabelle_scala_service 'isabelle.Admin_Tools'
-
-isabelle_scala_service 'isabelle.Scala_Functions'
-
-isabelle_scala_service 'isabelle.Sessions$File_Format'
-isabelle_scala_service 'isabelle.Bibtex$File_Format'
-
-isabelle_scala_service 'isabelle.ML_Statistics$Handler'
-isabelle_scala_service 'isabelle.Scala$Handler'
-isabelle_scala_service 'isabelle.Print_Operation$Handler'
-isabelle_scala_service 'isabelle.Simplifier_Trace$Handler'
-isabelle_scala_service 'isabelle.Server_Commands'
-
-isabelle_scala_service 'isabelle.Document_Build$LuaLaTeX_Engine'
-isabelle_scala_service 'isabelle.Document_Build$PDFLaTeX_Engine'
-isabelle_scala_service 'isabelle.Document_Build$Build_Engine'
+ISABELLE_SCALA_JAR="$ISABELLE_HOME/lib/classes/isabelle.jar"
#paranoia settings -- avoid intrusion of alien options
unset "_JAVA_OPTIONS"
--- a/lib/Tools/java Thu Jul 15 16:11:52 2021 +0200
+++ b/lib/Tools/java Thu Jul 15 22:51:49 2021 +0200
@@ -6,8 +6,12 @@
eval "declare -a JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS)"
-[ -n "$CLASSPATH" ] && classpath "$CLASSPATH"
-unset CLASSPATH
+if [ -z "$ISABELLE_SETUP_CLASSPATH_SKIP" -o "$ISABELLE_SETUP_CLASSPATH_SKIP" = "false" ]
+then
+ classpath "$ISABELLE_SETUP_CLASSPATH"; unset ISABELLE_SETUP_CLASSPATH
+fi
+
+classpath "$CLASSPATH"; unset CLASSPATH
isabelle_java java "${JAVA_ARGS[@]}" \
-classpath "$(platform_path "$ISABELLE_CLASSPATH")" "$@"
--- a/lib/Tools/scala Thu Jul 15 16:11:52 2021 +0200
+++ b/lib/Tools/scala Thu Jul 15 22:51:49 2021 +0200
@@ -13,8 +13,8 @@
SCALA_ARGS["${#SCALA_ARGS[@]}"]="-J$ARG"
done
-[ -n "$CLASSPATH" ] && classpath "$CLASSPATH"
-unset CLASSPATH
+classpath "$ISABELLE_SETUP_CLASSPATH"; unset ISABELLE_SETUP_CLASSPATH
+classpath "$CLASSPATH"; unset CLASSPATH
isabelle_scala scala "${SCALA_ARGS[@]}" \
-classpath "$(platform_path "$ISABELLE_CLASSPATH")" \
--- a/lib/Tools/scalac Thu Jul 15 16:11:52 2021 +0200
+++ b/lib/Tools/scalac Thu Jul 15 22:51:49 2021 +0200
@@ -6,5 +6,8 @@
isabelle_admin_build jars || exit $?
+classpath "$ISABELLE_SETUP_CLASSPATH"; unset ISABELLE_SETUP_CLASSPATH
+classpath "$CLASSPATH"; unset CLASSPATH
+
isabelle_scala scalac -Dfile.encoding=UTF-8 \
-classpath "$(platform_path "$ISABELLE_CLASSPATH")" "$@"
--- a/lib/browser/build Thu Jul 15 16:11:52 2021 +0200
+++ b/lib/browser/build Thu Jul 15 22:51:49 2021 +0200
@@ -63,7 +63,7 @@
rm -rf classes && mkdir classes
- isabelle_jdk javac -d classes -source 7 "${SOURCES[@]}" || \
+ isabelle_jdk javac -d classes -Xlint:-options -source 7 -target 7 "${SOURCES[@]}" || \
fail "Failed to compile sources"
isabelle_jdk jar cf "$(platform_path "$TARGET")" -C classes . ||
fail "Failed to produce $TARGET"
--- a/lib/scripts/getfunctions Thu Jul 15 16:11:52 2021 +0200
+++ b/lib/scripts/getfunctions Thu Jul 15 22:51:49 2021 +0200
@@ -106,7 +106,7 @@
do
if [ -z "$ISABELLE_CLASSPATH" ]; then
ISABELLE_CLASSPATH="$X"
- else
+ elif [ -n "$X" ]; then
ISABELLE_CLASSPATH="$ISABELLE_CLASSPATH:$X"
fi
done
@@ -212,14 +212,12 @@
export -f isabelle_directory
#administrative build
-if [ -e "$ISABELLE_HOME/Admin/build" ]; then
- function isabelle_admin_build ()
- {
+function isabelle_admin_build ()
+{
+ if [ -e "$ISABELLE_HOME/Admin/build" ]; then
"$ISABELLE_HOME/Admin/build" "$@"
- }
-else
- function isabelle_admin_build () { return 0; }
-fi
+ fi
+}
export -f isabelle_admin_build
#arrays
--- a/lib/scripts/getsettings Thu Jul 15 16:11:52 2021 +0200
+++ b/lib/scripts/getsettings Thu Jul 15 22:51:49 2021 +0200
@@ -129,6 +129,10 @@
export JAVA_HOME="$ISABELLE_JDK_HOME"
fi
+if [ -e "$ISABELLE_SETUP_JAR" ]; then
+ ISABELLE_SETUP_CLASSPATH="$(isabelle_java java -jar "$(platform_path "$ISABELLE_SETUP_JAR")" classpath)"
+fi
+
set +o allexport
fi
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/services/java.nio.charset.spi.CharsetProvider Thu Jul 15 22:51:49 2021 +0200
@@ -0,0 +1,1 @@
+isabelle.Isabelle_Charset_Provider
--- a/src/Doc/JEdit/JEdit.thy Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Doc/JEdit/JEdit.thy Thu Jul 15 22:51:49 2021 +0200
@@ -206,7 +206,7 @@
is no longer affected by change of default properties.
Users may modify their keymap later, but this can lead to conflicts with
- \<^verbatim>\<open>shortcut\<close> properties in \<^file>\<open>$JEDIT_HOME/dist/properties/jEdit.props\<close>.
+ \<^verbatim>\<open>shortcut\<close> properties in \<^file>\<open>$JEDIT_HOME/properties/jEdit.props\<close>.
The action @{action_def "isabelle.keymap-merge"} helps to resolve pending
Isabelle keymap changes wrt. the current jEdit keymap; non-conflicting
@@ -282,10 +282,9 @@
directly to the underlying \<^verbatim>\<open>java\<close> process.
The \<^verbatim>\<open>-b\<close> and \<^verbatim>\<open>-f\<close> options control the self-build mechanism of
- Isabelle/jEdit. This is only relevant for building from sources, which also
- requires an auxiliary \<^verbatim>\<open>jedit_build\<close> component from
- \<^url>\<open>https://isabelle.in.tum.de/components\<close>. The official Isabelle release
- already includes a pre-built version of Isabelle/jEdit.
+ Isabelle/Scala/PIDE/jEdit. This is only relevant for building from sources,
+ the official Isabelle release already includes a pre-built version of
+ Isabelle/jEdit.
\<^bigskip>
It is also possible to connect to an already running Isabelle/jEdit process
--- a/src/Doc/System/Environment.thy Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Doc/System/Environment.thy Thu Jul 15 22:51:49 2021 +0200
@@ -459,7 +459,7 @@
text \<open>
The subsequent example creates a raw Java process on the command-line and
invokes the main Isabelle application entry point:
- @{verbatim [display] \<open>isabelle_java isabelle.Main\<close>}
+ @{verbatim [display] \<open>isabelle_java -Djava.awt.headless=false isabelle.jedit.Main\<close>}
\<close>
--- a/src/Doc/System/Scala.thy Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Doc/System/Scala.thy Thu Jul 15 22:51:49 2021 +0200
@@ -31,7 +31,7 @@
operates on the running Java application, using the Scala
read-eval-print-loop (REPL).
- The main Isabelle/Scala functionality is provided by \<^verbatim>\<open>Pure.jar\<close>, but
+ The main Isabelle/Scala functionality is provided by \<^verbatim>\<open>isabelle.jar\<close>, but
further add-ons are bundled with Isabelle, e.g.\ to access SQLite or
PostgreSQL using JDBC (Java Database Connectivity).
@@ -189,7 +189,7 @@
can then register that class via \<^bash_function>\<open>isabelle_scala_service\<close>
in \<^path>\<open>etc/settings\<close> (\secref{sec:components}). An example is the
predefined collection of \<^scala_type>\<open>isabelle.Scala.Functions\<close> in
- Isabelle/\<^verbatim>\<open>Pure.jar\<close> with the following line in
+ \<^verbatim>\<open>isabelle.jar\<close> with the following line in
\<^file>\<open>$ISABELLE_HOME/etc/settings\<close>:
@{verbatim [display, indent = 2] \<open>isabelle_scala_service 'isabelle.Functions'\<close>}
--- a/src/HOL/SPARK/etc/settings Thu Jul 15 16:11:52 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-isabelle_scala_service 'isabelle.spark.SPARK$Load_Command1'
-isabelle_scala_service 'isabelle.spark.SPARK$Load_Command2'
--- a/src/HOL/Tools/etc/settings Thu Jul 15 16:11:52 2021 +0200
+++ b/src/HOL/Tools/etc/settings Thu Jul 15 22:51:49 2021 +0200
@@ -1,6 +1,3 @@
# -*- shell-script -*- :mode=shellscript:
-isabelle_scala_service 'isabelle.nitpick.Kodkod$Handler'
-isabelle_scala_service 'isabelle.nitpick.Scala_Functions'
-
ISABELLE_ATP="$COMPONENT/ATP"
--- a/src/Pure/Admin/build_jedit.scala Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Pure/Admin/build_jedit.scala Thu Jul 15 22:51:49 2021 +0200
@@ -1,12 +1,17 @@
/* Title: Pure/Admin/build_jedit.scala
Author: Makarius
-Build auxiliary jEdit component.
+Build component for jEdit text-editor.
*/
package isabelle
+import java.nio.charset.Charset
+
+import scala.jdk.CollectionConverters._
+
+
object Build_JEdit
{
/* modes */
@@ -197,6 +202,10 @@
/* resources */
+ val keep_encodings = List("ISO-8859-1", "ISO-8859-15", "US-ASCII", "UTF-8", "windows-1252")
+ val drop_encodings =
+ Charset.availableCharsets().keySet().asScala.toList.sorted.filterNot(keep_encodings.contains)
+
File.write(jedit_patched_dir + Path.explode("properties/jEdit.props"),
"""#jEdit properties
autoReloadDialog=false
@@ -217,164 +226,7 @@
console.fontsize=14
delete-line.shortcut=A+d
delete.shortcut2=C+d
-encoding.opt-out.Big5-HKSCS=true
-encoding.opt-out.Big5=true
-encoding.opt-out.COMPOUND_TEXT=true
-encoding.opt-out.EUC-JP=true
-encoding.opt-out.EUC-KR=true
-encoding.opt-out.GB2312=true
-encoding.opt-out.GB18030=true
-encoding.opt-out.GBK=true
-encoding.opt-out.IBM-Thai=true
-encoding.opt-out.IBM00858=true
-encoding.opt-out.IBM037=true
-encoding.opt-out.IBM01140=true
-encoding.opt-out.IBM01141=true
-encoding.opt-out.IBM01142=true
-encoding.opt-out.IBM01143=true
-encoding.opt-out.IBM01144=true
-encoding.opt-out.IBM01145=true
-encoding.opt-out.IBM01146=true
-encoding.opt-out.IBM01147=true
-encoding.opt-out.IBM01148=true
-encoding.opt-out.IBM01149=true
-encoding.opt-out.IBM273=true
-encoding.opt-out.IBM277=true
-encoding.opt-out.IBM278=true
-encoding.opt-out.IBM280=true
-encoding.opt-out.IBM284=true
-encoding.opt-out.IBM285=true
-encoding.opt-out.IBM297=true
-encoding.opt-out.IBM420=true
-encoding.opt-out.IBM424=true
-encoding.opt-out.IBM437=true
-encoding.opt-out.IBM500=true
-encoding.opt-out.IBM775=true
-encoding.opt-out.IBM850=true
-encoding.opt-out.IBM852=true
-encoding.opt-out.IBM855=true
-encoding.opt-out.IBM857=true
-encoding.opt-out.IBM860=true
-encoding.opt-out.IBM861=true
-encoding.opt-out.IBM862=true
-encoding.opt-out.IBM863=true
-encoding.opt-out.IBM864=true
-encoding.opt-out.IBM865=true
-encoding.opt-out.IBM866=true
-encoding.opt-out.IBM868=true
-encoding.opt-out.IBM869=true
-encoding.opt-out.IBM870=true
-encoding.opt-out.IBM871=true
-encoding.opt-out.IBM918=true
-encoding.opt-out.IBM1026=true
-encoding.opt-out.IBM1047=true
-encoding.opt-out.ISO-2022-CN=true
-encoding.opt-out.ISO-2022-JP-2=true
-encoding.opt-out.ISO-2022-JP=true
-encoding.opt-out.ISO-2022-KR=true
-encoding.opt-out.ISO-8859-2=true
-encoding.opt-out.ISO-8859-3=true
-encoding.opt-out.ISO-8859-4=true
-encoding.opt-out.ISO-8859-5=true
-encoding.opt-out.ISO-8859-6=true
-encoding.opt-out.ISO-8859-7=true
-encoding.opt-out.ISO-8859-8=true
-encoding.opt-out.ISO-8859-9=true
-encoding.opt-out.ISO-8859-13=true
-encoding.opt-out.JIS_X0201=true
-encoding.opt-out.JIS_X0212-1990=true
-encoding.opt-out.KOI8-R=true
-encoding.opt-out.KOI8-U=true
-encoding.opt-out.Shift_JIS=true
-encoding.opt-out.TIS-620=true
-encoding.opt-out.UTF-16=true
-encoding.opt-out.UTF-16BE=true
-encoding.opt-out.UTF-16LE=true
-encoding.opt-out.UTF-32=true
-encoding.opt-out.UTF-32BE=true
-encoding.opt-out.UTF-32LE=true
-encoding.opt-out.X-UTF-32BE-BOM=true
-encoding.opt-out.X-UTF-32LE-BOM=true
-encoding.opt-out.windows-31j=true
-encoding.opt-out.windows-1250=true
-encoding.opt-out.windows-1251=true
-encoding.opt-out.windows-1253=true
-encoding.opt-out.windows-1254=true
-encoding.opt-out.windows-1255=true
-encoding.opt-out.windows-1256=true
-encoding.opt-out.windows-1257=true
-encoding.opt-out.windows-1258=true
-encoding.opt-out.x-Big5-Solaris=true
-encoding.opt-out.x-EUC-TW=true
-encoding.opt-out.x-IBM737=true
-encoding.opt-out.x-IBM834=true
-encoding.opt-out.x-IBM856=true
-encoding.opt-out.x-IBM874=true
-encoding.opt-out.x-IBM875=true
-encoding.opt-out.x-IBM921=true
-encoding.opt-out.x-IBM922=true
-encoding.opt-out.x-IBM930=true
-encoding.opt-out.x-IBM933=true
-encoding.opt-out.x-IBM935=true
-encoding.opt-out.x-IBM937=true
-encoding.opt-out.x-IBM939=true
-encoding.opt-out.x-IBM942=true
-encoding.opt-out.x-IBM942C=true
-encoding.opt-out.x-IBM943=true
-encoding.opt-out.x-IBM943C=true
-encoding.opt-out.x-IBM948=true
-encoding.opt-out.x-IBM949=true
-encoding.opt-out.x-IBM949C=true
-encoding.opt-out.x-IBM950=true
-encoding.opt-out.x-IBM964=true
-encoding.opt-out.x-IBM970=true
-encoding.opt-out.x-IBM1006=true
-encoding.opt-out.x-IBM1025=true
-encoding.opt-out.x-IBM1046=true
-encoding.opt-out.x-IBM1097=true
-encoding.opt-out.x-IBM1098=true
-encoding.opt-out.x-IBM1112=true
-encoding.opt-out.x-IBM1122=true
-encoding.opt-out.x-IBM1123=true
-encoding.opt-out.x-IBM1124=true
-encoding.opt-out.x-IBM1381=true
-encoding.opt-out.x-IBM1383=true
-encoding.opt-out.x-IBM33722=true
-encoding.opt-out.x-ISCII91=true
-encoding.opt-out.x-ISO-2022-CN-CNS=true
-encoding.opt-out.x-ISO-2022-CN-GB=true
-encoding.opt-out.x-JIS0208=true
-encoding.opt-out.x-JISAutoDetect=true
-encoding.opt-out.x-Johab=true
-encoding.opt-out.x-MS932_0213=true
-encoding.opt-out.x-MS950-HKSCS=true
-encoding.opt-out.x-MacArabic=true
-encoding.opt-out.x-MacCentralEurope=true
-encoding.opt-out.x-MacCroatian=true
-encoding.opt-out.x-MacCyrillic=true
-encoding.opt-out.x-MacDingbat=true
-encoding.opt-out.x-MacGreek=true
-encoding.opt-out.x-MacHebrew=true
-encoding.opt-out.x-MacIceland=true
-encoding.opt-out.x-MacRoman=true
-encoding.opt-out.x-MacRomania=true
-encoding.opt-out.x-MacSymbol=true
-encoding.opt-out.x-MacThai=true
-encoding.opt-out.x-MacTurkish=true
-encoding.opt-out.x-MacUkraine=true
-encoding.opt-out.x-PCK=true
-encoding.opt-out.x-SJIS_0213=true
-encoding.opt-out.x-UTF-16LE-BOM=true
-encoding.opt-out.x-euc-jp-linux=true
-encoding.opt-out.x-eucJP-Open=true
-encoding.opt-out.x-iso-8859-11=true
-encoding.opt-out.x-mswin-936=true
-encoding.opt-out.x-windows-874=true
-encoding.opt-out.x-windows-949=true
-encoding.opt-out.x-windows-950=true
-encoding.opt-out.x-windows-50220=true
-encoding.opt-out.x-windows-50221=true
-encoding.opt-out.x-windows-iso2022jp=true
+""" + drop_encodings.map(a => "encoding.opt-out." + a + "=true").mkString("\n") + """
encodingDetectors=BOM XML-PI buffer-local-property
end.shortcut=
expand-abbrev.shortcut2=CA+SPACE
@@ -614,10 +466,18 @@
File.write(etc_dir + Path.explode("settings"),
"""# -*- shell-script -*- :mode=shellscript:
-ISABELLE_JEDIT_HOME="$COMPONENT/""" + jedit_patched + """"
-ISABELLE_JEDIT_JARS=""" +
- File.read_dir(jars_dir).map("$ISABELLE_JEDIT_HOME/jars/" + _).mkString("\"", ":", "\"\n")
-)
+JEDIT_HOME="$COMPONENT/""" + jedit_patched + """"
+JEDIT_JARS=""" + quote(File.read_dir(jars_dir).map("$JEDIT_HOME/jars/" + _).mkString(":")) + """
+JEDIT_JAR="$JEDIT_HOME/jedit.jar"
+classpath "$JEDIT_JAR"
+
+JEDIT_SETTINGS="$ISABELLE_HOME_USER/jedit"
+JEDIT_OPTIONS="-reuseview -nobackground -nosplash -log=9"
+JEDIT_JAVA_OPTIONS="-Xms512m -Xmx4g -Xss16m"
+JEDIT_JAVA_SYSTEM_OPTIONS="-Duser.language=en -Dawt.useSystemAAFontSettings=on -Dswing.aatext=true -Dapple.laf.useScreenMenuBar=true -Dapple.awt.application.name=Isabelle"
+
+ISABELLE_DOCS="$ISABELLE_DOCS:$JEDIT_HOME/doc"
+""")
/* README */
@@ -641,7 +501,8 @@
def default_java_home: Path = Path.explode("$JAVA_HOME").expand
val isabelle_tool =
- Isabelle_Tool("build_jedit", "build auxiliary jEdit component", Scala_Project.here, args =>
+ Isabelle_Tool("build_jedit", "build Isabelle component from the jEdit text-editor",
+ Scala_Project.here, args =>
{
var target_dir = Path.current
var java_home = default_java_home
@@ -661,15 +522,13 @@
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
"J:" -> (arg => java_home = Path.explode(arg)),
- "O" -> (arg => original = true),
+ "O" -> (_ => original = true),
"V:" -> (arg => version = arg))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
- val component_dir =
- target_dir + Path.basic("jedit_build-" + Date.Format.alt_date(Date.now()))
-
+ val component_dir = target_dir + Path.basic("jedit-" + Date.Format.alt_date(Date.now()))
val progress = new Console_Progress()
build_jedit(component_dir, version, original = original,
--- a/src/Pure/Admin/build_release.scala Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Pure/Admin/build_release.scala Thu Jul 15 22:51:49 2021 +0200
@@ -188,7 +188,7 @@
path = Components.admin(dir) + Path.basic(catalog)
if path.is_file
line <- split_lines(File.read(path))
- if line.nonEmpty && !line.startsWith("#") && !line.startsWith("jedit_build")
+ if line.nonEmpty && !line.startsWith("#")
} yield bundled(line)).toList))
}
@@ -196,10 +196,7 @@
{
val Bundled = new Bundled(platform = Some(platform))
val components =
- for {
- Bundled(name) <- Components.read_components(dir)
- if !name.startsWith("jedit_build")
- } yield name
+ for { Bundled(name) <- Components.read_components(dir) } yield name
val jdk_component =
components.find(_.startsWith("jdk")) getOrElse error("Missing jdk component")
(components, jdk_component)
@@ -316,7 +313,7 @@
-classpath """" + classpath.map(p => "$ISABELLE_HOME/" + p.implode).mkString(":") + """" \
"-splash:$ISABELLE_HOME/lib/logo/isabelle.gif" \
""" + (if (dock_icon) """"-Xdock:icon=$ISABELLE_HOME/lib/logo/isabelle_transparent-128.png" \
-""" else "") + """isabelle.Main "$@"
+""" else "") + """isabelle.jedit.Main "$@"
"""
val script_path = isabelle_target + Path.explode("lib/scripts/Isabelle_app")
File.write(script_path, script)
@@ -560,8 +557,6 @@
val more_components_names =
more_components.map(Components.unpack(contrib_dir, _, progress = progress))
- Components.purge(contrib_dir, platform)
-
activate_components(isabelle_target, platform, more_components_names)
@@ -584,18 +579,21 @@
val classpath: List[Path] =
{
val base = isabelle_target.absolute
- Path.split(other_isabelle.getenv("ISABELLE_CLASSPATH")).map(path =>
+ val classpath1 = Path.split(other_isabelle.getenv("ISABELLE_CLASSPATH"))
+ val classpath2 = Path.split(other_isabelle.getenv("ISABELLE_SETUP_CLASSPATH"))
+ (classpath1 ::: classpath2).map(path =>
{
val abs_path = path.absolute
File.relative_path(base, abs_path) match {
case Some(rel_path) => rel_path
- case None => error("Bad ISABELLE_CLASSPATH element: " + abs_path)
+ case None => error("Bad classpath element: " + abs_path)
}
- }) ::: List(Path.explode("src/Tools/jEdit/dist/jedit.jar"))
+ })
}
val jedit_options = Path.explode("src/Tools/jEdit/etc/options")
- val jedit_props = Path.explode("src/Tools/jEdit/dist/properties/jEdit.props")
+ val jedit_props =
+ Path.explode(other_isabelle.getenv("JEDIT_HOME") + "/properties/jEdit.props")
// build heaps
@@ -608,6 +606,8 @@
// application bundling
+ Components.purge(contrib_dir, platform)
+
platform match {
case Platform.Family.linux_arm | Platform.Family.linux =>
File.change(isabelle_target + jedit_options,
--- a/src/Pure/System/isabelle_system.scala Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Pure/System/isabelle_system.scala Thu Jul 15 22:51:49 2021 +0200
@@ -13,6 +13,8 @@
StandardCopyOption, FileSystemException}
import java.nio.file.attribute.BasicFileAttributes
+import scala.jdk.CollectionConverters._
+
object Isabelle_System
{
@@ -47,26 +49,35 @@
/* init settings + services */
+ def make_services(): List[Class[Service]] =
+ {
+ def make(where: String, names: List[String]): List[Class[Service]] =
+ {
+ for (name <- names) yield {
+ def err(msg: String): Nothing =
+ error("Bad Isabelle/Scala service " + quote(name) + " in " + where + "\n" + msg)
+ try { Class.forName(name).asInstanceOf[Class[Service]] }
+ catch {
+ case _: ClassNotFoundException => err("Class not found")
+ case exn: Throwable => err(Exn.message(exn))
+ }
+ }
+ }
+
+ def from_env(variable: String): List[Class[Service]] =
+ make(quote(variable), space_explode(':', getenv_strict(variable)))
+
+ def from_jar(platform_jar: String): List[Class[Service]] =
+ make(quote(platform_jar),
+ isabelle.setup.Build.get_services(JPath.of(platform_jar)).asScala.toList)
+
+ from_env("ISABELLE_SCALA_SERVICES") ::: Scala.class_path().flatMap(from_jar)
+ }
+
def init(isabelle_root: String = "", cygwin_root: String = ""): Unit =
{
isabelle.setup.Environment.init(isabelle_root, cygwin_root)
- synchronized {
- if (_services.isEmpty) {
- val variable = "ISABELLE_SCALA_SERVICES"
- val services =
- for (name <- space_explode(':', getenv_strict(variable)))
- yield {
- def err(msg: String): Nothing =
- error("Bad entry " + quote(name) + " in " + variable + "\n" + msg)
- try { Class.forName(name).asInstanceOf[Class[Service]] }
- catch {
- case _: ClassNotFoundException => err("Class not found")
- case exn: Throwable => err(Exn.message(exn))
- }
- }
- _services = Some(services)
- }
- }
+ synchronized { if (_services.isEmpty) { _services = Some(make_services()) } }
}
--- a/src/Pure/System/scala.scala Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Pure/System/scala.scala Thu Jul 15 22:51:49 2021 +0200
@@ -79,6 +79,13 @@
/** compiler **/
+ def class_path(): List[String] =
+ for {
+ prop <- List("isabelle.scala.classpath", "java.class.path")
+ elems = System.getProperty(prop, "") if elems.nonEmpty
+ elem <- space_explode(JFile.pathSeparatorChar, elems) if elem.nonEmpty
+ } yield elem
+
object Compiler
{
def context(
@@ -89,16 +96,9 @@
File.find_files(dir, file => file.getName.endsWith(".jar")).
map(File.absolute_name)
- val class_path =
- for {
- prop <- List("isabelle.scala.classpath", "java.class.path")
- path = System.getProperty(prop, "") if path != "\"\""
- elem <- space_explode(JFile.pathSeparatorChar, path)
- } yield elem
-
val settings = new GenericRunnerSettings(error)
settings.classpath.value =
- (class_path ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator)
+ (class_path() ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator)
new Context(settings)
}
--- a/src/Pure/Tools/jedit.ML Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Pure/Tools/jedit.ML Thu Jul 15 22:51:49 2021 +0200
@@ -36,8 +36,7 @@
fun xml_resource name =
let
- val res =
- Isabelle_System.bash_process ("unzip -p \"$JEDIT_HOME/dist/jedit.jar\" " ^ Bash.string name);
+ val res = Isabelle_System.bash_process ("unzip -p \"$JEDIT_JAR\" " ^ Bash.string name);
val rc = Process_Result.rc res;
in
res |> Process_Result.check |> Process_Result.out |> XML.parse
@@ -49,8 +48,8 @@
val lazy_actions =
Lazy.lazy (fn () =>
- (parse_actions (xml_file \<^file>\<open>~~/src/Tools/jEdit/src/actions.xml\<close>) @
- parse_dockables (xml_file \<^file>\<open>~~/src/Tools/jEdit/src/dockables.xml\<close>) @
+ (parse_actions (xml_file \<^file>\<open>~~/src/Tools/jEdit/jedit_main/actions.xml\<close>) @
+ parse_dockables (xml_file \<^file>\<open>~~/src/Tools/jEdit/jedit_main/dockables.xml\<close>) @
parse_actions (xml_resource "org/gjt/sp/jedit/actions.xml") @
parse_dockables (xml_resource "org/gjt/sp/jedit/dockables.xml"))
|> sort_strings);
--- a/src/Pure/Tools/main.scala Thu Jul 15 16:11:52 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,151 +0,0 @@
-/* Title: Pure/Tools/main.scala
- Author: Makarius
-
-Main Isabelle application entry point.
-*/
-
-package isabelle
-
-
-import java.lang.{Class, ClassLoader}
-
-
-object Main
-{
- /* main entry point */
-
- def main(args: Array[String]): Unit =
- {
- if (args.nonEmpty && args(0) == "-init") {
- Isabelle_System.init()
- }
- else {
- val start =
- {
- try {
- Isabelle_System.init()
- Isabelle_Fonts.init()
-
- GUI.init_lafs()
-
-
- /* ROOTS template */
-
- {
- val roots = Path.explode("$ISABELLE_HOME_USER/ROOTS")
- if (!roots.is_file) File.write(roots, """# Additional session root directories
-#
-# * each line contains one directory entry in Isabelle path notation, e.g.
-#
-# $ISABELLE_HOME/../AFP/thys
-#
-# for a copy of AFP put side-by-side to the Isabelle distribution
-#
-# * Isabelle/jEdit provides formal markup for C-hover-click and completion
-#
-# * lines starting with "#" are stripped
-#
-# * changes require restart of the Isabelle application
-#
-#:mode=text:encoding=UTF-8:
-
-#$ISABELLE_HOME/../AFP/thys
-""")
- }
-
-
- /* settings directory */
-
- val settings_dir = Path.explode("$JEDIT_SETTINGS")
-
- val properties = settings_dir + Path.explode("properties")
- if (properties.is_file) {
- val props1 = split_lines(File.read(properties))
- val props2 = props1.filterNot(_.startsWith("plugin-blacklist.Isabelle-jEdit"))
- if (props1 != props2) File.write(properties, cat_lines(props2))
- }
-
- Isabelle_System.make_directory(settings_dir + Path.explode("DockableWindowManager"))
-
- if (!(settings_dir + Path.explode("perspective.xml")).is_file) {
- File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"),
- """<DOCKING LEFT="isabelle-documentation" TOP="" RIGHT="isabelle-theories" BOTTOM="" LEFT_POS="250" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />""")
- File.write(settings_dir + Path.explode("perspective.xml"),
- XML.header +
-"""<!DOCTYPE PERSPECTIVE SYSTEM "perspective.dtd">
-<PERSPECTIVE>
-<VIEW PLAIN="FALSE">
-<GEOMETRY X="0" Y="35" WIDTH="1200" HEIGHT="850" EXT_STATE="0" />
-</VIEW>
-</PERSPECTIVE>""")
- }
-
-
- /* args */
-
- val jedit_settings =
- "-settings=" + File.platform_path(Path.explode("$JEDIT_SETTINGS"))
-
- val jedit_server =
- System.getProperty("isabelle.jedit_server") match {
- case null | "" => "-noserver"
- case name => "-server=" + name
- }
-
- val jedit_options =
- Isabelle_System.getenv_strict("JEDIT_OPTIONS").split(" +")
-
- val more_args =
- {
- args.toList.dropWhile(arg => arg.startsWith("-") && arg != "--") match {
- case Nil | List("--") =>
- args ++ Array(File.platform_path(Path.explode("$USER_HOME/Scratch.thy")))
- case List(":") => args.slice(0, args.size - 1)
- case _ => args
- }
- }
-
-
- /* environment */
-
- def putenv(name: String, value: String): Unit =
- {
- val misc =
- Class.forName("org.gjt.sp.jedit.MiscUtilities", true, ClassLoader.getSystemClassLoader)
- val putenv = misc.getMethod("putenv", classOf[String], classOf[String])
- putenv.invoke(null, name, value)
- }
-
- for (name <- List("ISABELLE_HOME", "ISABELLE_HOME_USER", "JEDIT_HOME", "JEDIT_SETTINGS")) {
- putenv(name, File.platform_path(Isabelle_System.getenv(name)))
- }
- putenv("ISABELLE_ROOT", null)
-
-
- /* properties */
-
- System.setProperty("jedit.home", File.platform_path(Path.explode("$JEDIT_HOME/dist")))
- System.setProperty("scala.home", File.platform_path(Path.explode("$SCALA_HOME")))
- System.setProperty("scala.color", "false")
-
-
- /* main startup */
-
- val jedit =
- Class.forName("org.gjt.sp.jedit.jEdit", true, ClassLoader.getSystemClassLoader)
- val jedit_main = jedit.getMethod("main", classOf[Array[String]])
-
- () => jedit_main.invoke(
- null, Array(jedit_settings, jedit_server) ++ jedit_options ++ more_args)
- }
- catch {
- case exn: Throwable =>
- GUI.init_laf()
- GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
- sys.exit(2)
- }
- }
- start()
- }
- }
-}
--- a/src/Pure/Tools/scala_project.scala Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Pure/Tools/scala_project.scala Thu Jul 15 22:51:49 2021 +0200
@@ -32,22 +32,17 @@
map(path => File.relative_path(isabelle_home, path).getOrElse(path).implode)
}
+ val isabelle_jar = Path.explode("$ISABELLE_SCALA_JAR").java_path
+ val isabelle_shasum = isabelle.setup.Build.get_shasum(isabelle_jar)
+
val files2 =
- (for {
- path <-
- List(
- Path.explode("~~/lib/classes/Pure.shasum"),
- Path.explode("~~/src/Tools/jEdit/dist/Isabelle-jEdit.shasum"))
- if path.is_file
- line <- Library.trim_split_lines(File.read(path))
+ for {
+ line <- Library.trim_split_lines(isabelle_shasum)
name =
- if (line.length > 42 && line(41) == '*') line.substring(42)
+ if (line.length > 41 && line(40) == ' ') line.substring(41)
else error("Bad shasum entry: " + quote(line))
- if name != "lib/classes/Pure.jar" &&
- name != "src/Tools/jEdit/dist/jedit.jar" &&
- name != "src/Tools/jEdit/dist/jars/Isabelle-jEdit-base.jar" &&
- name != "src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar"
- } yield name)
+ if Path.is_wellformed(name) && name != "<props>"
+ } yield name
files1 ::: files2
}
@@ -114,7 +109,7 @@
val java_src_dir = project_dir + Path.explode("src/main/java")
val scala_src_dir = Isabelle_System.make_directory(project_dir + Path.explode("src/main/scala"))
- Isabelle_System.copy_dir(Path.explode("~~/src/Tools/jEdit/dist/jEdit"), java_src_dir)
+ Isabelle_System.copy_dir(Path.explode("$JEDIT_HOME/jEdit"), java_src_dir)
val isabelle_setup_dir = Path.explode("~~/src/Tools/Setup/isabelle")
if (symlinks) Isabelle_System.symlink(isabelle_setup_dir, java_src_dir)
--- a/src/Pure/build-jars Thu Jul 15 16:11:52 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,328 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# build-jars - build Isabelle/Scala
-#
-# Requires proper Isabelle settings environment.
-
-## sources
-
-declare -a SOURCES=(
- src/HOL/SPARK/Tools/spark.scala
- src/HOL/Tools/ATP/system_on_tptp.scala
- src/HOL/Tools/Mirabelle/mirabelle.scala
- src/HOL/Tools/Nitpick/kodkod.scala
- src/Pure/Admin/afp.scala
- src/Pure/Admin/build_csdp.scala
- src/Pure/Admin/build_cygwin.scala
- src/Pure/Admin/build_doc.scala
- src/Pure/Admin/build_e.scala
- src/Pure/Admin/build_fonts.scala
- src/Pure/Admin/build_history.scala
- src/Pure/Admin/build_jcef.scala
- src/Pure/Admin/build_jdk.scala
- src/Pure/Admin/build_jedit.scala
- src/Pure/Admin/build_log.scala
- src/Pure/Admin/build_polyml.scala
- src/Pure/Admin/build_release.scala
- src/Pure/Admin/build_spass.scala
- src/Pure/Admin/build_sqlite.scala
- src/Pure/Admin/build_status.scala
- src/Pure/Admin/build_vampire.scala
- src/Pure/Admin/build_verit.scala
- src/Pure/Admin/build_zipperposition.scala
- src/Pure/Admin/check_sources.scala
- src/Pure/Admin/ci_profile.scala
- src/Pure/Admin/isabelle_cronjob.scala
- src/Pure/Admin/isabelle_devel.scala
- src/Pure/Admin/jenkins.scala
- src/Pure/Admin/other_isabelle.scala
- src/Pure/Concurrent/consumer_thread.scala
- src/Pure/Concurrent/counter.scala
- src/Pure/Concurrent/delay.scala
- src/Pure/Concurrent/event_timer.scala
- src/Pure/Concurrent/future.scala
- src/Pure/Concurrent/isabelle_thread.scala
- src/Pure/Concurrent/mailbox.scala
- src/Pure/Concurrent/par_list.scala
- src/Pure/Concurrent/synchronized.scala
- src/Pure/GUI/color_value.scala
- src/Pure/GUI/desktop_app.scala
- src/Pure/GUI/gui.scala
- src/Pure/GUI/gui_thread.scala
- src/Pure/GUI/popup.scala
- src/Pure/GUI/wrap_panel.scala
- src/Pure/General/antiquote.scala
- src/Pure/General/bytes.scala
- src/Pure/General/cache.scala
- src/Pure/General/codepoint.scala
- src/Pure/General/comment.scala
- src/Pure/General/completion.scala
- src/Pure/General/csv.scala
- src/Pure/General/date.scala
- src/Pure/General/exn.scala
- src/Pure/General/file.scala
- src/Pure/General/file_watcher.scala
- src/Pure/General/graph.scala
- src/Pure/General/graph_display.scala
- src/Pure/General/graphics_file.scala
- src/Pure/General/http.scala
- src/Pure/General/json.scala
- src/Pure/General/linear_set.scala
- src/Pure/General/logger.scala
- src/Pure/General/long_name.scala
- src/Pure/General/mailman.scala
- src/Pure/General/mercurial.scala
- src/Pure/General/multi_map.scala
- src/Pure/General/output.scala
- src/Pure/General/path.scala
- src/Pure/General/position.scala
- src/Pure/General/pretty.scala
- src/Pure/General/properties.scala
- src/Pure/General/rdf.scala
- src/Pure/General/scan.scala
- src/Pure/General/sha1.scala
- src/Pure/General/sql.scala
- src/Pure/General/ssh.scala
- src/Pure/General/symbol.scala
- src/Pure/General/time.scala
- src/Pure/General/timing.scala
- src/Pure/General/untyped.scala
- src/Pure/General/url.scala
- src/Pure/General/utf8.scala
- src/Pure/General/uuid.scala
- src/Pure/General/value.scala
- src/Pure/General/word.scala
- src/Pure/General/xz.scala
- src/Pure/Isar/document_structure.scala
- src/Pure/Isar/keyword.scala
- src/Pure/Isar/line_structure.scala
- src/Pure/Isar/outer_syntax.scala
- src/Pure/Isar/parse.scala
- src/Pure/Isar/token.scala
- src/Pure/ML/ml_console.scala
- src/Pure/ML/ml_lex.scala
- src/Pure/ML/ml_process.scala
- src/Pure/ML/ml_profiling.scala
- src/Pure/ML/ml_statistics.scala
- src/Pure/ML/ml_syntax.scala
- src/Pure/PIDE/byte_message.scala
- src/Pure/PIDE/command.scala
- src/Pure/PIDE/command_span.scala
- src/Pure/PIDE/document.scala
- src/Pure/PIDE/document_id.scala
- src/Pure/PIDE/document_status.scala
- src/Pure/PIDE/editor.scala
- src/Pure/PIDE/headless.scala
- src/Pure/PIDE/line.scala
- src/Pure/PIDE/markup.scala
- src/Pure/PIDE/markup_tree.scala
- src/Pure/PIDE/protocol.scala
- src/Pure/PIDE/protocol_handlers.scala
- src/Pure/PIDE/protocol_message.scala
- src/Pure/PIDE/prover.scala
- src/Pure/PIDE/query_operation.scala
- src/Pure/PIDE/rendering.scala
- src/Pure/PIDE/resources.scala
- src/Pure/PIDE/session.scala
- src/Pure/PIDE/text.scala
- src/Pure/PIDE/xml.scala
- src/Pure/PIDE/yxml.scala
- src/Pure/ROOT.scala
- src/Pure/System/bash.scala
- src/Pure/System/command_line.scala
- src/Pure/System/components.scala
- src/Pure/System/executable.scala
- src/Pure/System/getopts.scala
- src/Pure/System/isabelle_charset.scala
- src/Pure/System/isabelle_fonts.scala
- src/Pure/System/isabelle_platform.scala
- src/Pure/System/isabelle_process.scala
- src/Pure/System/isabelle_system.scala
- src/Pure/System/isabelle_tool.scala
- src/Pure/System/java_statistics.scala
- src/Pure/System/linux.scala
- src/Pure/System/mingw.scala
- src/Pure/System/numa.scala
- src/Pure/System/options.scala
- src/Pure/System/platform.scala
- src/Pure/System/posix_interrupt.scala
- src/Pure/System/process_result.scala
- src/Pure/System/progress.scala
- src/Pure/System/scala.scala
- src/Pure/System/system_channel.scala
- src/Pure/System/tty_loop.scala
- src/Pure/Thy/bibtex.scala
- src/Pure/Thy/document_build.scala
- src/Pure/Thy/export.scala
- src/Pure/Thy/export_theory.scala
- src/Pure/Thy/file_format.scala
- src/Pure/Thy/html.scala
- src/Pure/Thy/latex.scala
- src/Pure/Thy/presentation.scala
- src/Pure/Thy/sessions.scala
- src/Pure/Thy/thy_element.scala
- src/Pure/Thy/thy_header.scala
- src/Pure/Thy/thy_syntax.scala
- src/Pure/Tools/build.scala
- src/Pure/Tools/build_docker.scala
- src/Pure/Tools/build_job.scala
- src/Pure/Tools/check_keywords.scala
- src/Pure/Tools/debugger.scala
- src/Pure/Tools/doc.scala
- src/Pure/Tools/dump.scala
- src/Pure/Tools/fontforge.scala
- src/Pure/Tools/java_monitor.scala
- src/Pure/Tools/logo.scala
- src/Pure/Tools/main.scala
- src/Pure/Tools/mkroot.scala
- src/Pure/Tools/phabricator.scala
- src/Pure/Tools/print_operation.scala
- src/Pure/Tools/profiling_report.scala
- src/Pure/Tools/scala_project.scala
- src/Pure/Tools/server.scala
- src/Pure/Tools/server_commands.scala
- src/Pure/Tools/simplifier_trace.scala
- src/Pure/Tools/spell_checker.scala
- src/Pure/Tools/task_statistics.scala
- src/Pure/Tools/update.scala
- src/Pure/Tools/update_cartouches.scala
- src/Pure/Tools/update_comments.scala
- src/Pure/Tools/update_header.scala
- src/Pure/Tools/update_then.scala
- src/Pure/Tools/update_theorems.scala
- src/Pure/library.scala
- src/Pure/pure_thy.scala
- src/Pure/term.scala
- src/Pure/term_xml.scala
- src/Pure/thm_name.scala
- src/Tools/Graphview/graph_file.scala
- src/Tools/Graphview/graph_panel.scala
- src/Tools/Graphview/graphview.scala
- src/Tools/Graphview/layout.scala
- src/Tools/Graphview/main_panel.scala
- src/Tools/Graphview/metrics.scala
- src/Tools/Graphview/model.scala
- src/Tools/Graphview/mutator.scala
- src/Tools/Graphview/mutator_dialog.scala
- src/Tools/Graphview/mutator_event.scala
- src/Tools/Graphview/popups.scala
- src/Tools/Graphview/shapes.scala
- src/Tools/Graphview/tree_panel.scala
- src/Tools/VSCode/src/build_vscode.scala
- src/Tools/VSCode/src/channel.scala
- src/Tools/VSCode/src/dynamic_output.scala
- src/Tools/VSCode/src/language_server.scala
- src/Tools/VSCode/src/lsp.scala
- src/Tools/VSCode/src/preview_panel.scala
- src/Tools/VSCode/src/state_panel.scala
- src/Tools/VSCode/src/textmate_grammar.scala
- src/Tools/VSCode/src/vscode_model.scala
- src/Tools/VSCode/src/vscode_rendering.scala
- src/Tools/VSCode/src/vscode_resources.scala
- src/Tools/VSCode/src/vscode_spell_checker.scala
-)
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: isabelle $PRG [OPTIONS]"
- echo
- echo " Options are:"
- echo " -f fresh build"
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-[ -z "$ISABELLE_HOME" ] && fail "Missing Isabelle settings environment"
-
-
-## process command line
-
-# options
-
-FRESH=""
-
-while getopts "f" OPT
-do
- case "$OPT" in
- f)
- FRESH=true
- ;;
- \?)
- usage
- ;;
- esac
-done
-
-shift $(($OPTIND - 1))
-
-
-# args
-
-[ "$#" -ne 0 ] && usage
-
-
-## target
-
-TARGET_DIR="lib/classes"
-TARGET_JAR="$TARGET_DIR/Pure.jar"
-TARGET_SHASUM="$TARGET_DIR/Pure.shasum"
-
-function target_shasum()
-{
- shasum -a1 -b "$TARGET_JAR" "${SOURCES[@]}" 2>/dev/null
-}
-
-function target_clean()
-{
- rm -rf "$TARGET_DIR"
-}
-
-[ -n "$FRESH" ] && target_clean
-
-
-## build
-
-target_shasum | cmp "$TARGET_SHASUM" >/dev/null 2>/dev/null
-if [ "$?" -ne 0 ]; then
- echo "### Building Isabelle/Scala ..."
-
- target_clean
-
- BUILD_DIR="$TARGET_DIR/build"
- mkdir -p "$BUILD_DIR"
-
- (
- export CLASSPATH="$(platform_path "$ISABELLE_CLASSPATH")"
- isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS \
- -d "$BUILD_DIR" "${SOURCES[@]}"
- ) || fail "Failed to compile sources"
-
- CHARSET_SERVICE="META-INF/services/java.nio.charset.spi.CharsetProvider"
- mkdir -p "$BUILD_DIR/$(dirname "$CHARSET_SERVICE")"
- echo isabelle.Isabelle_Charset_Provider > "$BUILD_DIR/$CHARSET_SERVICE"
-
- cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" "$BUILD_DIR/isabelle/."
- cp "$ISABELLE_HOME/lib/logo/isabelle_transparent.gif" "$BUILD_DIR/isabelle/."
-
- isabelle_jdk jar -c -f "$(platform_path "$TARGET_JAR")" -e isabelle.Main \
- -C "$BUILD_DIR" META-INF \
- -C "$BUILD_DIR" isabelle || fail "Failed to produce $TARGET_JAR"
-
- rm -rf "$BUILD_DIR"
-
- target_shasum > "$TARGET_SHASUM"
-fi
--- a/src/Tools/Setup/isabelle/setup/Build.java Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Tools/Setup/isabelle/setup/Build.java Thu Jul 15 22:51:49 2021 +0200
@@ -137,13 +137,6 @@
return Files.exists(path(file));
}
- // historic
- public Path shasum_path()
- throws IOException, InterruptedException
- {
- return path(lib_name() + ".shasum");
- }
-
public String item_name(String s)
{
int i = s.indexOf(':');
@@ -394,8 +387,6 @@
List<String> resources = context.resources();
List<String> sources = context.sources();
- Files.deleteIfExists(context.shasum_path());
-
if (context.is_vacuous()) { Files.deleteIfExists(jar_path); }
else {
String shasum_old = get_shasum(jar_path);
@@ -428,8 +419,8 @@
shasum = _shasum.toString();
}
if (fresh || !shasum_old.equals(shasum)) {
- System.out.println(
- "### Building " + context.description() + " (" + jar_path + ") ...");
+ System.out.print(
+ "### Building " + context.description() + " (" + jar_path + ") ...\n");
String isabelle_class_path = Environment.getenv("ISABELLE_CLASSPATH");
--- a/src/Tools/Setup/isabelle/setup/Library.java Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Tools/Setup/isabelle/setup/Library.java Thu Jul 15 22:51:49 2021 +0200
@@ -37,6 +37,7 @@
for (String s : split_lines(str)) {
result.append(prfx);
result.append(s);
+ result.append('\n');
}
return result.toString();
}
--- a/src/Tools/Setup/isabelle/setup/Setup.java Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Tools/Setup/isabelle/setup/Setup.java Thu Jul 15 22:51:49 2021 +0200
@@ -11,11 +11,11 @@
{
private static void echo(String msg)
{
- System.out.println(msg);
+ System.out.print(msg + "\n");
}
private static void echo_err(String msg)
{
- System.err.println(msg);
+ System.err.print(msg + "\n");
}
private static void fail(String msg)
{
--- a/src/Tools/jEdit/README Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Tools/jEdit/README Thu Jul 15 22:51:49 2021 +0200
@@ -1,12 +1,3 @@
-These are the main sources of Isabelle/jEdit, which is a plugin for
-the jEdit text-editor, with some minor modifications according to
-patches/.
-
-Original jEdit is available from http://www.jedit.org -- it is
-licensed according to GPL, and the derivative version produced in
-directory "dist" inherits that.
-
-Note that Isabelle repository versions refer to a contributed
-component called jedit_build-JJJJMMDD, which also includes the full
-sources after applying the patches, together with further add-on
-modules.
+These are the sources of Isabelle/jEdit. The main jEdit text-editor is
+provided as a separate component: it includes the full sources after
+applying some minor patches, together with further add-on modules.
--- a/src/Tools/jEdit/etc/settings Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Tools/jEdit/etc/settings Thu Jul 15 22:51:49 2021 +0200
@@ -1,14 +1,4 @@
# -*- shell-script -*- :mode=shellscript:
-JEDIT_HOME="$COMPONENT"
-JEDIT_SETTINGS="$ISABELLE_HOME_USER/jedit"
-
-JEDIT_OPTIONS="-reuseview -nobackground -nosplash -log=9"
-
-JEDIT_JAVA_OPTIONS="-Xms512m -Xmx4g -Xss16m"
-JEDIT_JAVA_SYSTEM_OPTIONS="-Duser.language=en -Dawt.useSystemAAFontSettings=on -Dswing.aatext=true -Dapple.laf.useScreenMenuBar=true -Dapple.awt.application.name=Isabelle"
-
ISABELLE_JEDIT_OPTIONS=""
-
-ISABELLE_TOOLS="$ISABELLE_TOOLS:$JEDIT_HOME/lib/Tools"
-ISABELLE_DOCS="$ISABELLE_DOCS:$JEDIT_HOME/dist/doc"
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/jedit_base/build.props Thu Jul 15 22:51:49 2021 +0200
@@ -0,0 +1,11 @@
+description = Isabelle/jEdit base plugin
+lib = $JEDIT_SETTINGS/jars
+name = isabelle_jedit_base
+requirements = \
+ env:ISABELLE_SCALA_JAR \
+ env:JEDIT_JARS
+resources = \
+ plugin.props \
+ services.xml
+sources = \
+ plugin.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/jedit_base/plugin.props Thu Jul 15 22:51:49 2021 +0200
@@ -0,0 +1,17 @@
+## Isabelle/jEdit plugin properties
+##
+##:wrap=soft:maxLineLen=100:
+
+#identification
+plugin.isabelle.jedit_base.Plugin.name=Isabelle Base
+plugin.isabelle.jedit_base.Plugin.author=Makarius Wenzel
+plugin.isabelle.jedit_base.Plugin.version=1.0
+plugin.isabelle.jedit_base.Plugin.description=Isabelle Base: DO NOT UNLOAD!
+
+#system parameters
+plugin.isabelle.jedit_base.Plugin.activate=startup
+plugin.isabelle.jedit_base.Plugin.usePluginHome=false
+
+#dependencies
+plugin.isabelle.jedit_base.Plugin.depend.0=jdk 11
+plugin.isabelle.jedit_base.Plugin.depend.1=jedit 05.05.00.00
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/jedit_base/plugin.scala Thu Jul 15 22:51:49 2021 +0200
@@ -0,0 +1,9 @@
+/* Title: Tools/jEdit/jedit_base/plugin.scala
+ Author: Makarius
+
+Isabelle/jEdit base plugin.
+*/
+
+package isabelle.jedit_base
+
+class Plugin extends isabelle.jedit.Base_Plugin
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/jedit_base/services.xml Thu Jul 15 22:51:49 2021 +0200
@@ -0,0 +1,11 @@
+<?xml version="1.0"?>
+<!DOCTYPE SERVICES SYSTEM "services.dtd">
+
+<SERVICES>
+ <SERVICE NAME="UTF-8-Isabelle" CLASS="org.gjt.sp.jedit.io.Encoding">
+ new isabelle.jedit.Isabelle_Encoding();
+ </SERVICE>
+ <SERVICE CLASS="org.gjt.sp.jedit.gui.DockingFrameworkProvider" NAME="PIDE">
+ new isabelle.jedit.PIDE_Docking_Framework();
+ </SERVICE>
+</SERVICES>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/jedit_main/actions.xml Thu Jul 15 22:51:49 2021 +0200
@@ -0,0 +1,230 @@
+<?xml version="1.0"?>
+<!DOCTYPE ACTIONS SYSTEM "actions.dtd">
+
+<ACTIONS>
+ <ACTION NAME="isabelle.set-continuous-checking">
+ <CODE>
+ isabelle.jedit.Isabelle.set_continuous_checking();
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.reset-continuous-checking">
+ <CODE>
+ isabelle.jedit.Isabelle.reset_continuous_checking();
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.toggle-continuous-checking">
+ <CODE>
+ isabelle.jedit.Isabelle.toggle_continuous_checking();
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.set-node-required">
+ <CODE>
+ isabelle.jedit.Isabelle.set_node_required(view);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.reset-node-required">
+ <CODE>
+ isabelle.jedit.Isabelle.reset_node_required(view);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.toggle-node-required">
+ <CODE>
+ isabelle.jedit.Isabelle.toggle_node_required(view);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.update-state">
+ <CODE>
+ isabelle.jedit.Isabelle.update_state(view);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.reset-font-size">
+ <CODE>
+ isabelle.jedit.Isabelle.reset_font_size();
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.increase-font-size">
+ <CODE>
+ isabelle.jedit.Isabelle.increase_font_size();
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.increase-font-size2">
+ <CODE>
+ isabelle.jedit.Isabelle.increase_font_size();
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.decrease-font-size">
+ <CODE>
+ isabelle.jedit.Isabelle.decrease_font_size();
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.decrease-font-size2">
+ <CODE>
+ isabelle.jedit.Isabelle.decrease_font_size();
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.newline">
+ <CODE>
+ isabelle.jedit.Isabelle.newline(textArea);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="toggle-full-screen">
+ <CODE>
+ isabelle.jedit.Isabelle.toggle_full_screen(view);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.goto-entity">
+ <CODE>
+ isabelle.jedit.Isabelle.goto_entity(view);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.select-entity">
+ <CODE>
+ isabelle.jedit.Isabelle.select_entity(textArea);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.complete">
+ <CODE>
+ isabelle.jedit.Isabelle.complete(view, false);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.tooltip">
+ <CODE>
+ isabelle.jedit.Isabelle.show_tooltip(view, true);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.message">
+ <CODE>
+ isabelle.jedit.Isabelle.show_tooltip(view, false);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.first-error">
+ <CODE>
+ isabelle.jedit.Isabelle.goto_first_error(view);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.last-error">
+ <CODE>
+ isabelle.jedit.Isabelle.goto_last_error(view);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.prev-error">
+ <CODE>
+ isabelle.jedit.Isabelle.goto_prev_error(view);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.next-error">
+ <CODE>
+ isabelle.jedit.Isabelle.goto_next_error(view);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.complete-word">
+ <CODE>
+ isabelle.jedit.Isabelle.complete(view, true);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.control-sub">
+ <CODE>
+ isabelle.jedit.Isabelle.control_sub(textArea);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.control-sup">
+ <CODE>
+ isabelle.jedit.Isabelle.control_sup(textArea);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.control-bold">
+ <CODE>
+ isabelle.jedit.Isabelle.control_bold(textArea);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.control-emph">
+ <CODE>
+ isabelle.jedit.Isabelle.control_emph(textArea);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.control-reset">
+ <CODE>
+ isabelle.jedit.Isabelle.control_reset(textArea);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.input-bsub">
+ <CODE>
+ isabelle.jedit.Isabelle.input_bsub(textArea);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.input-bsup">
+ <CODE>
+ isabelle.jedit.Isabelle.input_bsup(textArea);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.antiquoted_cartouche">
+ <CODE>
+ isabelle.jedit.Isabelle.antiquoted_cartouche(textArea);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.include-word">
+ <CODE>
+ isabelle.jedit.Isabelle.update_dictionary(textArea, true, false);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.include-word-permanently">
+ <CODE>
+ isabelle.jedit.Isabelle.update_dictionary(textArea, true, true);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.exclude-word">
+ <CODE>
+ isabelle.jedit.Isabelle.update_dictionary(textArea, false, false);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.exclude-word-permanently">
+ <CODE>
+ isabelle.jedit.Isabelle.update_dictionary(textArea, false, true);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.reset-words">
+ <CODE>
+ isabelle.jedit.Isabelle.reset_dictionary();
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.toggle-breakpoint">
+ <CODE>
+ isabelle.jedit.Isabelle.toggle_breakpoint(textArea);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.options">
+ <CODE>
+ isabelle.jedit.Isabelle.plugin_options(view);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.preview">
+ <CODE>
+ isabelle.jedit.Document_Model.open_preview(view, false);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.draft">
+ <CODE>
+ isabelle.jedit.Document_Model.open_preview(view, true);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle-export-browser">
+ <CODE>
+ isabelle.jedit.Isabelle_Export.open_browser(view);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle-session-browser">
+ <CODE>
+ isabelle.jedit.Isabelle_Session.open_browser(view);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.keymap-merge">
+ <CODE>
+ isabelle.jedit.Keymap_Merge.check_dialog(view);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.java-monitor">
+ <CODE>
+ isabelle.jedit.Isabelle.java_monitor(view);
+ </CODE>
+ </ACTION>
+</ACTIONS>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/jedit_main/build.props Thu Jul 15 22:51:49 2021 +0200
@@ -0,0 +1,17 @@
+description = Isabelle/jEdit main plugin
+lib = $JEDIT_SETTINGS/jars
+name = isabelle_jedit_main
+requirements = \
+ env:ISABELLE_SCALA_JAR \
+ env:JEDIT_JARS
+resources = \
+ actions.xml \
+ dockables.xml \
+ plugin.props \
+ services.xml
+sources = \
+ isabelle_sidekick.scala \
+ dockables.scala \
+ plugin.scala \
+ scala_console.scala \
+ services.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/jedit_main/dockables.scala Thu Jul 15 22:51:49 2021 +0200
@@ -0,0 +1,59 @@
+/* Title: Tools/jEdit/jedit_main/dockables.scala
+ Author: Makarius
+
+Isabelle/jEdit dockables.
+*/
+
+package isabelle.jedit_main
+
+
+import org.gjt.sp.jedit.View
+
+
+class Debugger_Dockable(view: View, position: String)
+ extends isabelle.jedit.Debugger_Dockable(view, position)
+
+class Documentation_Dockable(view: View, position: String)
+ extends isabelle.jedit.Documentation_Dockable(view, position)
+
+class Info_Dockable(view: View, position: String)
+ extends isabelle.jedit.Info_Dockable(view, position)
+
+class Graphview_Dockable(view: View, position: String)
+ extends isabelle.jedit.Graphview_Dockable(view, position)
+
+class Monitor_Dockable(view: View, position: String)
+ extends isabelle.jedit.Monitor_Dockable(view, position)
+
+class Output_Dockable(view: View, position: String)
+ extends isabelle.jedit.Output_Dockable(view, position)
+
+class Protocol_Dockable(view: View, position: String)
+ extends isabelle.jedit.Protocol_Dockable(view, position)
+
+class Query_Dockable(view: View, position: String)
+ extends isabelle.jedit.Query_Dockable(view, position)
+
+class Raw_Output_Dockable(view: View, position: String)
+ extends isabelle.jedit.Raw_Output_Dockable(view, position)
+
+class Simplifier_Trace_Dockable(view: View, position: String)
+ extends isabelle.jedit.Simplifier_Trace_Dockable(view, position)
+
+class Sledgehammer_Dockable(view: View, position: String)
+ extends isabelle.jedit.Sledgehammer_Dockable(view, position)
+
+class State_Dockable(view: View, position: String)
+ extends isabelle.jedit.State_Dockable(view, position)
+
+class Symbols_Dockable(view: View, position: String)
+ extends isabelle.jedit.Symbols_Dockable(view, position)
+
+class Syslog_Dockable(view: View, position: String)
+ extends isabelle.jedit.Syslog_Dockable(view, position)
+
+class Theories_Dockable(view: View, position: String)
+ extends isabelle.jedit.Theories_Dockable(view, position)
+
+class Timing_Dockable(view: View, position: String)
+ extends isabelle.jedit.Timing_Dockable(view, position)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/jedit_main/dockables.xml Thu Jul 15 22:51:49 2021 +0200
@@ -0,0 +1,53 @@
+<?xml version="1.0"?>
+<!DOCTYPE DOCKABLES SYSTEM "dockables.dtd">
+
+<DOCKABLES>
+ <DOCKABLE NAME="isabelle-debugger" MOVABLE="TRUE">
+ new isabelle.jedit_main.Debugger_Dockable(view, position);
+ </DOCKABLE>
+ <DOCKABLE NAME="isabelle-documentation" MOVABLE="TRUE">
+ new isabelle.jedit_main.Documentation_Dockable(view, position);
+ </DOCKABLE>
+ <DOCKABLE NAME="isabelle-info" MOVABLE="TRUE">
+ new isabelle.jedit_main.Info_Dockable(view, position);
+ </DOCKABLE>
+ <DOCKABLE NAME="isabelle-graphview" MOVABLE="TRUE">
+ new isabelle.jedit_main.Graphview_Dockable(view, position);
+ </DOCKABLE>
+ <DOCKABLE NAME="isabelle-monitor" MOVABLE="TRUE">
+ new isabelle.jedit_main.Monitor_Dockable(view, position);
+ </DOCKABLE>
+ <DOCKABLE NAME="isabelle-output" MOVABLE="TRUE">
+ new isabelle.jedit_main.Output_Dockable(view, position);
+ </DOCKABLE>
+ <DOCKABLE NAME="isabelle-protocol" MOVABLE="TRUE">
+ new isabelle.jedit_main.Protocol_Dockable(view, position);
+ </DOCKABLE>
+ <DOCKABLE NAME="isabelle-query" MOVABLE="TRUE">
+ new isabelle.jedit_main.Query_Dockable(view, position);
+ </DOCKABLE>
+ <DOCKABLE NAME="isabelle-raw-output" MOVABLE="TRUE">
+ new isabelle.jedit_main.Raw_Output_Dockable(view, position);
+ </DOCKABLE>
+ <DOCKABLE NAME="isabelle-simplifier-trace" MOVABLE="TRUE">
+ new isabelle.jedit_main.Simplifier_Trace_Dockable(view, position);
+ </DOCKABLE>
+ <DOCKABLE NAME="isabelle-sledgehammer" MOVABLE="TRUE">
+ new isabelle.jedit_main.Sledgehammer_Dockable(view, position);
+ </DOCKABLE>
+ <DOCKABLE NAME="isabelle-state" MOVABLE="TRUE">
+ new isabelle.jedit_main.State_Dockable(view, position);
+ </DOCKABLE>
+ <DOCKABLE NAME="isabelle-symbols" MOVABLE="TRUE">
+ new isabelle.jedit_main.Symbols_Dockable(view, position);
+ </DOCKABLE>
+ <DOCKABLE NAME="isabelle-syslog" MOVABLE="TRUE">
+ new isabelle.jedit_main.Syslog_Dockable(view, position);
+ </DOCKABLE>
+ <DOCKABLE NAME="isabelle-theories" MOVABLE="TRUE">
+ new isabelle.jedit_main.Theories_Dockable(view, position);
+ </DOCKABLE>
+ <DOCKABLE NAME="isabelle-timing" MOVABLE="TRUE">
+ new isabelle.jedit_main.Timing_Dockable(view, position);
+ </DOCKABLE>
+</DOCKABLES>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala Thu Jul 15 22:51:49 2021 +0200
@@ -0,0 +1,305 @@
+/* Title: Tools/jEdit/src/isabelle_sidekick.scala
+ Author: Fabian Immler, TU Munich
+ Author: Makarius
+
+SideKick parsers for Isabelle proof documents.
+*/
+
+package isabelle.jedit_main
+
+
+import isabelle._
+import isabelle.jedit._
+
+import javax.swing.tree.DefaultMutableTreeNode
+import javax.swing.text.Position
+import javax.swing.{JLabel, Icon}
+
+import org.gjt.sp.jedit.Buffer
+import sidekick.{SideKickParser, SideKickParsedData, IAsset}
+
+
+object Isabelle_Sidekick
+{
+ def int_to_pos(offset: Text.Offset): Position =
+ new Position { def getOffset = offset; override def toString: String = offset.toString }
+
+ def root_data(buffer: Buffer): SideKickParsedData =
+ {
+ val data = new SideKickParsedData(buffer.getName)
+ data.getAsset(data.root).setEnd(int_to_pos(buffer.getLength))
+ data
+ }
+
+ class Keyword_Asset(keyword: String, text: String, range: Text.Range) extends IAsset
+ {
+ private val css = GUI.imitate_font_css(GUI.label_font())
+
+ protected var _name = text
+ protected var _start = int_to_pos(range.start)
+ protected var _end = int_to_pos(range.stop)
+ override def getIcon: Icon = null
+ override def getShortString: String =
+ {
+ val n = keyword.length
+ val s =
+ _name.indexOf(keyword) match {
+ case i if i >= 0 && n > 0 =>
+ HTML.output(_name.substring(0, i)) +
+ "<b>" + HTML.output(keyword) + "</b>" +
+ HTML.output(_name.substring(i + n))
+ case _ => HTML.output(_name)
+ }
+ "<html><span style=\"" + css + "\">" + s + "</span></html>"
+ }
+ override def getLongString: String = _name
+ override def getName: String = _name
+ override def setName(name: String): Unit = _name = name
+ override def getStart: Position = _start
+ override def setStart(start: Position): Unit = _start = start
+ override def getEnd: Position = _end
+ override def setEnd(end: Position): Unit = _end = end
+ override def toString: String = _name
+ }
+
+ class Asset(name: String, range: Text.Range) extends Keyword_Asset("", name, range)
+
+ def swing_markup_tree(tree: Markup_Tree, parent: DefaultMutableTreeNode,
+ swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode): Unit =
+ {
+ for ((_, entry) <- tree.branches) {
+ val node = swing_node(Text.Info(entry.range, entry.markup))
+ swing_markup_tree(entry.subtree, node, swing_node)
+ parent.add(node)
+ }
+ }
+}
+
+
+class Isabelle_Sidekick(name: String) extends SideKickParser(name)
+{
+ override def supportsCompletion = false
+
+
+ /* parsing */
+
+ @volatile protected var stopped = false
+ override def stop() = { stopped = true }
+
+ def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = false
+
+ def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData =
+ {
+ stopped = false
+
+ // FIXME lock buffer (!??)
+ val data = Isabelle_Sidekick.root_data(buffer)
+ val syntax = Isabelle.buffer_syntax(buffer)
+ val ok =
+ if (syntax.isDefined) {
+ val ok = parser(buffer, syntax.get, data)
+ if (stopped) { data.root.add(new DefaultMutableTreeNode("<stopped>")); true }
+ else ok
+ }
+ else false
+ if (!ok) data.root.add(new DefaultMutableTreeNode("<ignored>"))
+
+ data
+ }
+}
+
+
+class Isabelle_Sidekick_Structure(
+ name: String,
+ node_name: Buffer => Option[Document.Node.Name],
+ parse: (Outer_Syntax, Document.Node.Name, CharSequence) => List[Document_Structure.Document])
+ extends Isabelle_Sidekick(name)
+{
+ override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
+ {
+ def make_tree(
+ parent: DefaultMutableTreeNode,
+ offset: Text.Offset,
+ documents: List[Document_Structure.Document]): Unit =
+ {
+ documents.foldLeft(offset) {
+ case (i, document) =>
+ document match {
+ case Document_Structure.Block(name, text, body) =>
+ val range = Text.Range(i, i + document.length)
+ val node =
+ new DefaultMutableTreeNode(
+ new Isabelle_Sidekick.Keyword_Asset(name, Library.first_line(text), range))
+ parent.add(node)
+ make_tree(node, i, body)
+ case _ =>
+ }
+ i + document.length
+ }
+ }
+
+ node_name(buffer) match {
+ case Some(name) =>
+ make_tree(data.root, 0, parse(syntax, name, JEdit_Lib.buffer_text(buffer)))
+ true
+ case None =>
+ false
+ }
+ }
+}
+
+class Isabelle_Sidekick_Default extends
+ Isabelle_Sidekick_Structure("isabelle",
+ PIDE.resources.theory_node_name, Document_Structure.parse_sections)
+
+class Isabelle_Sidekick_Context extends
+ Isabelle_Sidekick_Structure("isabelle-context",
+ PIDE.resources.theory_node_name, Document_Structure.parse_blocks)
+
+class Isabelle_Sidekick_Options extends
+ Isabelle_Sidekick_Structure("isabelle-options",
+ _ => Some(Document.Node.Name("options")), Document_Structure.parse_sections)
+
+class Isabelle_Sidekick_Root extends
+ Isabelle_Sidekick_Structure("isabelle-root",
+ _ => Some(Document.Node.Name("ROOT")), Document_Structure.parse_sections)
+
+class Isabelle_Sidekick_ML extends
+ Isabelle_Sidekick_Structure("isabelle-ml",
+ buffer => Some(PIDE.resources.node_name(buffer)),
+ (_, _, text) => Document_Structure.parse_ml_sections(false, text))
+
+class Isabelle_Sidekick_SML extends
+ Isabelle_Sidekick_Structure("isabelle-sml",
+ buffer => Some(PIDE.resources.node_name(buffer)),
+ (_, _, text) => Document_Structure.parse_ml_sections(true, text))
+
+
+class Isabelle_Sidekick_Markup extends Isabelle_Sidekick("isabelle-markup")
+{
+ override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
+ {
+ val opt_snapshot =
+ Document_Model.get(buffer) match {
+ case Some(model) if model.is_theory => Some(model.snapshot())
+ case _ => None
+ }
+ opt_snapshot match {
+ case Some(snapshot) =>
+ for ((command, command_start) <- snapshot.node.command_iterator() if !stopped) {
+ val markup =
+ snapshot.state.command_markup(
+ snapshot.version, command, Command.Markup_Index.markup,
+ command.range, Markup.Elements.full)
+ Isabelle_Sidekick.swing_markup_tree(markup, data.root,
+ (info: Text.Info[List[XML.Elem]]) =>
+ {
+ val range = info.range + command_start
+ val content = command.source(info.range).replace('\n', ' ')
+ val info_text = Pretty.formatted(Pretty.fbreaks(info.info), margin = 40.0).mkString
+
+ new DefaultMutableTreeNode(
+ new Isabelle_Sidekick.Asset(command.toString, range) {
+ override def getShortString: String = content
+ override def getLongString: String = info_text
+ override def toString: String = quote(content) + " " + range.toString
+ })
+ })
+ }
+ true
+ case None => false
+ }
+ }
+}
+
+
+class Isabelle_Sidekick_News extends Isabelle_Sidekick("isabelle-news")
+{
+ private val Heading1 = """^New in (.*)\w*$""".r
+ private val Heading2 = """^\*\*\*\w*(.*)\w*\*\*\*\w*$""".r
+
+ private def make_node(s: String, start: Text.Offset, stop: Text.Offset): DefaultMutableTreeNode =
+ new DefaultMutableTreeNode(new Isabelle_Sidekick.Asset(s, Text.Range(start, stop)))
+
+ override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
+ {
+ var offset = 0
+ var end_offset = 0
+
+ var start1: Option[(Int, String, Vector[DefaultMutableTreeNode])] = None
+ var start2: Option[(Int, String)] = None
+
+ def close1: Unit =
+ start1 match {
+ case Some((start_offset, s, body)) =>
+ val node = make_node(s, start_offset, end_offset)
+ body.foreach(node.add(_))
+ data.root.add(node)
+ start1 = None
+ case None =>
+ }
+
+ def close2: Unit =
+ start2 match {
+ case Some((start_offset, s)) =>
+ start1 match {
+ case Some((start_offset1, s1, body)) =>
+ val node = make_node(s, start_offset, end_offset)
+ start1 = Some((start_offset1, s1, body :+ node))
+ case None =>
+ }
+ start2 = None
+ case None =>
+ }
+
+ for (line <- split_lines(JEdit_Lib.buffer_text(buffer)) if !stopped) {
+ line match {
+ case Heading1(s) => close2; close1; start1 = Some((offset, s, Vector()))
+ case Heading2(s) => close2; start2 = Some((offset, s))
+ case _ =>
+ }
+ offset += line.length + 1
+ if (!line.forall(Character.isSpaceChar)) end_offset = offset
+ }
+ if (!stopped) { close2; close1 }
+
+ true
+ }
+}
+
+class Isabelle_Sidekick_Bibtex extends SideKickParser("bibtex")
+{
+ override def supportsCompletion = false
+
+ private class Asset(label: String, label_html: String, range: Text.Range, source: String)
+ extends Isabelle_Sidekick.Asset(label, range) {
+ override def getShortString: String = label_html
+ override def getLongString: String = source
+ }
+
+ def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData =
+ {
+ val data = Isabelle_Sidekick.root_data(buffer)
+
+ try {
+ var offset = 0
+ for (chunk <- Bibtex.parse(JEdit_Lib.buffer_text(buffer))) {
+ val kind = chunk.kind
+ val name = chunk.name
+ val source = chunk.source
+ if (kind != "") {
+ val label = kind + (if (name == "") "" else " " + name)
+ val label_html =
+ "<html><b>" + HTML.output(kind) + "</b>" +
+ (if (name == "") "" else " " + HTML.output(name)) + "</html>"
+ val range = Text.Range(offset, offset + source.length)
+ val asset = new Asset(label, label_html, range, source)
+ data.root.add(new DefaultMutableTreeNode(asset))
+ }
+ offset += source.length
+ }
+ data
+ }
+ catch { case ERROR(msg) => Output.warning(msg); null }
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/jedit_main/plugin.props Thu Jul 15 22:51:49 2021 +0200
@@ -0,0 +1,111 @@
+## Isabelle/jEdit plugin properties
+##
+##:wrap=soft:maxLineLen=100:
+
+#identification
+plugin.isabelle.jedit_main.Plugin.name=Isabelle
+plugin.isabelle.jedit_main.Plugin.author=Johannes H\u00F6lzl, Lars Hupel, Fabian Immler, Markus Kaiser, Makarius Wenzel
+plugin.isabelle.jedit_main.Plugin.version=11.2
+plugin.isabelle.jedit_main.Plugin.description=Isabelle Prover IDE
+
+#system parameters
+plugin.isabelle.jedit_main.Plugin.activate=defer
+plugin.isabelle.jedit_main.Plugin.usePluginHome=false
+
+#dependencies
+plugin.isabelle.jedit_main.Plugin.depend.0=jdk 11
+plugin.isabelle.jedit_main.Plugin.depend.1=jedit 05.05.00.00
+plugin.isabelle.jedit_main.Plugin.depend.2=plugin console.ConsolePlugin 5.1.4
+plugin.isabelle.jedit_main.Plugin.depend.3=plugin errorlist.ErrorListPlugin 2.3
+plugin.isabelle.jedit_main.Plugin.depend.4=plugin sidekick.SideKickPlugin 1.8
+plugin.isabelle.jedit_main.Plugin.depend.5=plugin isabelle.jedit_base.Plugin 1.0
+
+#options
+plugin.isabelle.jedit_main.Plugin.option-group=isabelle-general isabelle-rendering
+options.isabelle-general.label=General
+options.isabelle-general.code=new isabelle.jedit.Isabelle_Options1();
+options.isabelle-rendering.label=Rendering
+options.isabelle-rendering.code=new isabelle.jedit.Isabelle_Options2();
+
+#menu actions and dockables
+plugin.isabelle.jedit_main.Plugin.menu.label=Isabelle
+plugin.isabelle.jedit_main.Plugin.menu= \
+ isabelle-export-browser \
+ isabelle-session-browser \
+ isabelle.preview \
+ isabelle.draft \
+ isabelle.java-monitor \
+ - \
+ isabelle-debugger \
+ isabelle-documentation \
+ isabelle-monitor \
+ isabelle-output \
+ isabelle-protocol \
+ isabelle-query \
+ isabelle-raw-output \
+ isabelle-simplifier-trace \
+ isabelle-sledgehammer \
+ isabelle-state \
+ isabelle-symbols \
+ isabelle-syslog \
+ isabelle-theories \
+ isabelle-timing
+isabelle-debugger.label=Debugger panel
+isabelle-debugger.title=Debugger
+isabelle-documentation.label=Documentation panel
+isabelle-documentation.title=Documentation
+isabelle-graphview.label=Graphview panel
+isabelle-graphview.title=Graphview
+isabelle-info.label=Info panel
+isabelle-info.title=Info
+isabelle-monitor.label=Monitor panel
+isabelle-monitor.title=Monitor
+isabelle-output.label=Output panel
+isabelle-output.title=Output
+isabelle-protocol.label=Protocol panel
+isabelle-protocol.title=Protocol
+isabelle-query.label=Query panel
+isabelle-query.title=Query
+isabelle-raw-output.label=Raw Output panel
+isabelle-raw-output.title=Raw Output
+isabelle-simplifier-trace.label=Simplifier Trace panel
+isabelle-simplifier-trace.title=Simplifier Trace
+isabelle-sledgehammer.label=Sledgehammer panel
+isabelle-sledgehammer.title=Sledgehammer
+isabelle-state.label=State panel
+isabelle-state.title=State
+isabelle-symbols.label=Symbols panel
+isabelle-symbols.title=Symbols
+isabelle-syslog.label=Syslog panel
+isabelle-syslog.title=Syslog
+isabelle-theories.label=Theories panel
+isabelle-theories.title=Theories
+isabelle-timing.label=Timing panel
+isabelle-timing.title=Timing
+
+#SideKick
+mode.isabelle-news.folding=sidekick
+mode.isabelle-news.sidekick.parser=isabelle-news
+mode.isabelle-options.folding=sidekick
+mode.isabelle-options.sidekick.parser=isabelle-options
+mode.isabelle-root.folding=sidekick
+mode.isabelle-root.sidekick.parser=isabelle-root
+mode.isabelle.customSettings=true
+mode.isabelle.folding=isabelle
+mode.isabelle.sidekick.parser=isabelle
+mode.isabelle.sidekick.showStatusWindow.label=true
+mode.isabelle-ml.folding=sidekick
+mode.isabelle-ml.sidekick.parser=isabelle-ml
+mode.sml.folding=sidekick
+mode.sml.sidekick.parser=isabelle-sml
+mode.bibtex.folding=sidekick
+mode.bibtex.sidekick.parser=bibtex
+sidekick.parser.isabelle.label=isabelle
+sidekick.parser.isabelle-context.label=isabelle-context
+sidekick.parser.isabelle-markup.label=isabelle-markup
+sidekick.parser.isabelle-ml.label=isabelle-ml
+sidekick.parser.isabelle-sml.label=isabelle-sml
+sidekick.parser.isabelle-news.label=isabelle-news
+sidekick.parser.isabelle-options.label=isabelle-options
+sidekick.parser.isabelle-root.label=isabelle-root
+sidekick.parser.bibtex.label=bibtex
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/jedit_main/plugin.scala Thu Jul 15 22:51:49 2021 +0200
@@ -0,0 +1,9 @@
+/* Title: Tools/jEdit/jedit_main/plugin.scala
+ Author: Makarius
+
+Isabelle/jEdit main plugin.
+*/
+
+package isabelle.jedit_main
+
+class Plugin extends isabelle.jedit.Main_Plugin
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/jedit_main/scala_console.scala Thu Jul 15 22:51:49 2021 +0200
@@ -0,0 +1,182 @@
+/* Title: Tools/jEdit/jedit_main/scala_console.scala
+ Author: Makarius
+
+Scala instance of Console plugin.
+*/
+
+package isabelle.jedit_main
+
+
+import isabelle._
+import isabelle.jedit._
+
+import console.{Console, ConsolePane, Shell, Output}
+import org.gjt.sp.jedit.JARClassLoader
+import java.io.{OutputStream, Writer, PrintWriter}
+
+
+class Scala_Console extends Shell("Scala")
+{
+ /* global state -- owned by GUI thread */
+
+ @volatile private var interpreters = Map.empty[Console, Interpreter]
+
+ @volatile private var global_console: Console = null
+ @volatile private var global_out: Output = null
+ @volatile private var global_err: Output = null
+
+ private val console_stream = new OutputStream
+ {
+ val buf = new StringBuilder(100)
+
+ override def flush(): Unit =
+ {
+ val s = buf.synchronized { val s = buf.toString; buf.clear(); s }
+ val str = UTF8.decode_permissive(s)
+ GUI_Thread.later {
+ if (global_out == null) System.out.print(str)
+ else global_out.writeAttrs(null, str)
+ }
+ Time.seconds(0.01).sleep() // FIXME adhoc delay to avoid loosing output
+ }
+
+ override def close(): Unit = flush()
+
+ def write(byte: Int): Unit =
+ {
+ val c = byte.toChar
+ buf.synchronized { buf.append(c) }
+ if (c == '\n') flush()
+ }
+ }
+
+ private val console_writer = new Writer
+ {
+ def flush(): Unit = console_stream.flush()
+ def close(): Unit = console_stream.flush()
+
+ def write(cbuf: Array[Char], off: Int, len: Int): Unit =
+ {
+ if (len > 0) {
+ UTF8.bytes(new String(cbuf.slice(off, off + len))).foreach(console_stream.write(_))
+ }
+ }
+ }
+
+ private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A =
+ {
+ global_console = console
+ global_out = out
+ global_err = if (err == null) out else err
+ try {
+ scala.Console.withErr(console_stream) {
+ scala.Console.withOut(console_stream) { e }
+ }
+ }
+ finally {
+ console_stream.flush
+ global_console = null
+ global_out = null
+ global_err = null
+ }
+ }
+
+ private def report_error(str: String): Unit =
+ {
+ if (global_console == null || global_err == null) isabelle.Output.writeln(str)
+ else GUI_Thread.later { global_err.print(global_console.getErrorColor, str) }
+ }
+
+
+ /* interpreter thread */
+
+ private abstract class Request
+ private case class Start(console: Console) extends Request
+ private case class Execute(console: Console, out: Output, err: Output, command: String)
+ extends Request
+
+ private class Interpreter
+ {
+ private val running = Synchronized[Option[Thread]](None)
+ def interrupt(): Unit = running.change(opt => { opt.foreach(_.interrupt()); opt })
+
+ private val interp =
+ Scala.Compiler.context(error = report_error, jar_dirs = JEdit_Lib.directories).
+ interpreter(
+ print_writer = new PrintWriter(console_writer, true),
+ class_loader = new JARClassLoader)
+
+ val thread: Consumer_Thread[Request] = Consumer_Thread.fork("Scala_Console")
+ {
+ case Start(console) =>
+ interp.bind("view", "org.gjt.sp.jedit.View", console.getView)
+ interp.bind("console", "console.Console", console)
+ interp.interpret("import isabelle._; import isabelle.jedit._")
+ true
+
+ case Execute(console, out, err, command) =>
+ with_console(console, out, err) {
+ try {
+ running.change(_ => Some(Thread.currentThread()))
+ interp.interpret(command)
+ }
+ finally {
+ running.change(_ => None)
+ Exn.Interrupt.dispose()
+ }
+ GUI_Thread.later {
+ if (err != null) err.commandDone()
+ out.commandDone()
+ }
+ true
+ }
+ }
+ }
+
+
+ /* jEdit console methods */
+
+ override def openConsole(console: Console): Unit =
+ {
+ val interp = new Interpreter
+ interp.thread.send(Start(console))
+ interpreters += (console -> interp)
+ }
+
+ override def closeConsole(console: Console): Unit =
+ {
+ interpreters.get(console) match {
+ case Some(interp) =>
+ interp.interrupt()
+ interp.thread.shutdown()
+ interpreters -= console
+ case None =>
+ }
+ }
+
+ override def printInfoMessage(out: Output): Unit =
+ {
+ out.print(null,
+ "This shell evaluates Isabelle/Scala expressions.\n\n" +
+ "The contents of package isabelle and isabelle.jedit are imported.\n" +
+ "The following special toplevel bindings are provided:\n" +
+ " view -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" +
+ " console -- jEdit Console plugin\n" +
+ " PIDE -- Isabelle/PIDE plugin (e.g. PIDE.session, PIDE.snapshot, PIDE.rendering)\n")
+ }
+
+ override def printPrompt(console: Console, out: Output): Unit =
+ {
+ out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>")
+ out.writeAttrs(ConsolePane.colorAttributes(console.getPlainColor), " ")
+ }
+
+ override def execute(
+ console: Console, input: String, out: Output, err: Output, command: String): Unit =
+ {
+ interpreters(console).thread.send(Execute(console, out, err, command))
+ }
+
+ override def stop(console: Console): Unit =
+ interpreters.get(console).foreach(_.interrupt())
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/jedit_main/services.scala Thu Jul 15 22:51:49 2021 +0200
@@ -0,0 +1,24 @@
+/* Title: Tools/jEdit/jedit_main/services.scala
+ Author: Makarius
+
+Isabelle/jEdit services.
+*/
+
+package isabelle.jedit_main
+
+
+class Fold_Handler extends isabelle.jedit.Fold_Handling.Fold_Handler
+
+class Context_Menu extends isabelle.jedit.Context_Menu
+
+class Isabelle_Export_VFS extends isabelle.jedit.Isabelle_Export.VFS
+
+class Isabelle_Session_VFS extends isabelle.jedit.Isabelle_Session.VFS
+
+class Active_Misc_Handler extends isabelle.jedit.Active.Misc_Handler
+
+class Graphview_Dockable_Handler extends isabelle.jedit.Graphview_Dockable.Handler
+
+class Status_Widget_Java_Factory extends isabelle.jedit.Status_Widget.Java_Factory
+
+class Status_Widget_ML_Factory extends isabelle.jedit.Status_Widget.ML_Factory
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/jedit_main/services.xml Thu Jul 15 22:51:49 2021 +0200
@@ -0,0 +1,59 @@
+<?xml version="1.0"?>
+<!DOCTYPE SERVICES SYSTEM "services.dtd">
+
+<SERVICES>
+ <SERVICE CLASS="org.gjt.sp.jedit.buffer.FoldHandler" NAME="isabelle">
+ new isabelle.jedit_main.Fold_Handler();
+ </SERVICE>
+ <SERVICE CLASS="org.gjt.sp.jedit.gui.DynamicContextMenuService" NAME="Spell_Checker">
+ new isabelle.jedit_main.Context_Menu();
+ </SERVICE>
+ <SERVICE NAME="isabelle-export" CLASS="org.gjt.sp.jedit.io.VFS">
+ new isabelle.jedit_main.Isabelle_Export_VFS();
+ </SERVICE>
+ <SERVICE NAME="isabelle-session" CLASS="org.gjt.sp.jedit.io.VFS">
+ new isabelle.jedit_main.Isabelle_Session_VFS();
+ </SERVICE>
+ <SERVICE NAME="isabelle" CLASS="sidekick.SideKickParser">
+ new isabelle.jedit_main.Isabelle_Sidekick_Default();
+ </SERVICE>
+ <SERVICE NAME="isabelle-context" CLASS="sidekick.SideKickParser">
+ new isabelle.jedit_main.Isabelle_Sidekick_Context();
+ </SERVICE>
+ <SERVICE NAME="isabelle-markup" CLASS="sidekick.SideKickParser">
+ new isabelle.jedit_main.Isabelle_Sidekick_Markup();
+ </SERVICE>
+ <SERVICE NAME="isabelle-ml" CLASS="sidekick.SideKickParser">
+ new isabelle.jedit_main.Isabelle_Sidekick_ML();
+ </SERVICE>
+ <SERVICE NAME="isabelle-sml" CLASS="sidekick.SideKickParser">
+ new isabelle.jedit_main.Isabelle_Sidekick_SML();
+ </SERVICE>
+ <SERVICE NAME="isabelle-news" CLASS="sidekick.SideKickParser">
+ new isabelle.jedit_main.Isabelle_Sidekick_News();
+ </SERVICE>
+ <SERVICE NAME="isabelle-options" CLASS="sidekick.SideKickParser">
+ new isabelle.jedit_main.Isabelle_Sidekick_Options();
+ </SERVICE>
+ <SERVICE NAME="isabelle-root" CLASS="sidekick.SideKickParser">
+ new isabelle.jedit_main.Isabelle_Sidekick_Root();
+ </SERVICE>
+ <SERVICE NAME="bibtex" CLASS="sidekick.SideKickParser">
+ new isabelle.jedit_main.Isabelle_Sidekick_Bibtex();
+ </SERVICE>
+ <SERVICE CLASS="console.Shell" NAME="Scala">
+ new isabelle.jedit_main.Scala_Console();
+ </SERVICE>
+ <SERVICE CLASS="isabelle.jedit.Active$Handler" NAME="misc">
+ new isabelle.jedit_main.Active_Misc_Handler();
+ </SERVICE>
+ <SERVICE CLASS="isabelle.jedit.Active$Handler" NAME="graphview">
+ new isabelle.jedit_main.Graphview_Dockable_Handler()
+ </SERVICE>
+ <SERVICE CLASS="org.gjt.sp.jedit.gui.statusbar.StatusWidgetFactory" NAME="java-status">
+ new isabelle.jedit_main.Status_Widget_Java_Factory();
+ </SERVICE>
+ <SERVICE CLASS="org.gjt.sp.jedit.gui.statusbar.StatusWidgetFactory" NAME="ml-status">
+ new isabelle.jedit_main.Status_Widget_ML_Factory();
+ </SERVICE>
+</SERVICES>
--- a/src/Tools/jEdit/lib/Tools/jedit Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Thu Jul 15 22:51:49 2021 +0200
@@ -4,85 +4,6 @@
#
# DESCRIPTION: Isabelle/jEdit interface wrapper
-## sources
-
-declare -a SOURCES0=(
- "src/Tools/jEdit/src-base/dockable.scala"
- "src/Tools/jEdit/src-base/isabelle_encoding.scala"
- "src/Tools/jEdit/src-base/jedit_lib.scala"
- "src/Tools/jEdit/src-base/pide_docking_framework.scala"
- "src/Tools/jEdit/src-base/plugin.scala"
- "src/Tools/jEdit/src-base/syntax_style.scala"
-)
-
-declare -a RESOURCES0=(
- "src/Tools/jEdit/src-base/Isabelle_Base.props"
- "src/Tools/jEdit/src-base/services.xml"
-)
-
-declare -a SOURCES=(
- "src/Tools/jEdit/src/active.scala"
- "src/Tools/jEdit/src/completion_popup.scala"
- "src/Tools/jEdit/src/context_menu.scala"
- "src/Tools/jEdit/src/debugger_dockable.scala"
- "src/Tools/jEdit/src/document_model.scala"
- "src/Tools/jEdit/src/document_view.scala"
- "src/Tools/jEdit/src/documentation_dockable.scala"
- "src/Tools/jEdit/src/fold_handling.scala"
- "src/Tools/jEdit/src/font_info.scala"
- "src/Tools/jEdit/src/graphview_dockable.scala"
- "src/Tools/jEdit/src/info_dockable.scala"
- "src/Tools/jEdit/src/isabelle.scala"
- "src/Tools/jEdit/src/isabelle_encoding.scala"
- "src/Tools/jEdit/src/isabelle_export.scala"
- "src/Tools/jEdit/src/isabelle_options.scala"
- "src/Tools/jEdit/src/isabelle_session.scala"
- "src/Tools/jEdit/src/isabelle_sidekick.scala"
- "src/Tools/jEdit/src/isabelle_vfs.scala"
- "src/Tools/jEdit/src/jedit_bibtex.scala"
- "src/Tools/jEdit/src/jedit_editor.scala"
- "src/Tools/jEdit/src/jedit_lib.scala"
- "src/Tools/jEdit/src/jedit_options.scala"
- "src/Tools/jEdit/src/jedit_rendering.scala"
- "src/Tools/jEdit/src/jedit_resources.scala"
- "src/Tools/jEdit/src/jedit_sessions.scala"
- "src/Tools/jEdit/src/jedit_spell_checker.scala"
- "src/Tools/jEdit/src/keymap_merge.scala"
- "src/Tools/jEdit/src/monitor_dockable.scala"
- "src/Tools/jEdit/src/output_dockable.scala"
- "src/Tools/jEdit/src/plugin.scala"
- "src/Tools/jEdit/src/pretty_text_area.scala"
- "src/Tools/jEdit/src/pretty_tooltip.scala"
- "src/Tools/jEdit/src/process_indicator.scala"
- "src/Tools/jEdit/src/protocol_dockable.scala"
- "src/Tools/jEdit/src/query_dockable.scala"
- "src/Tools/jEdit/src/raw_output_dockable.scala"
- "src/Tools/jEdit/src/rich_text_area.scala"
- "src/Tools/jEdit/src/scala_console.scala"
- "src/Tools/jEdit/src/session_build.scala"
- "src/Tools/jEdit/src/simplifier_trace_dockable.scala"
- "src/Tools/jEdit/src/simplifier_trace_window.scala"
- "src/Tools/jEdit/src/sledgehammer_dockable.scala"
- "src/Tools/jEdit/src/state_dockable.scala"
- "src/Tools/jEdit/src/status_widget.scala"
- "src/Tools/jEdit/src/symbols_dockable.scala"
- "src/Tools/jEdit/src/syntax_style.scala"
- "src/Tools/jEdit/src/syslog_dockable.scala"
- "src/Tools/jEdit/src/text_overview.scala"
- "src/Tools/jEdit/src/text_structure.scala"
- "src/Tools/jEdit/src/theories_dockable.scala"
- "src/Tools/jEdit/src/timing_dockable.scala"
- "src/Tools/jEdit/src/token_markup.scala"
-)
-
-declare -a RESOURCES=(
- "src/Tools/jEdit/src/actions.xml"
- "src/Tools/jEdit/src/dockables.xml"
- "src/Tools/jEdit/src/Isabelle.props"
- "src/Tools/jEdit/src/services.xml"
-)
-
-
## diagnostics
PRG="$(basename "$0")"
@@ -231,110 +152,15 @@
done
-## dependencies
-
-if [ -e "$ISABELLE_HOME/Admin/build" ]; then
- isabelle browser -b || exit $?
- if [ -n "$FRESH_BUILD" ]; then
- "$ISABELLE_HOME/Admin/build" jars_fresh || exit $?
- else
- "$ISABELLE_HOME/Admin/build" jars || exit $?
- fi
-elif [ -n "$FRESH_BUILD" ]; then
- echo >&2 "### Ignoring fresh build option: not a repository clone"
- FRESH_BUILD=""
-fi
-
-
-# target
-
-pushd "$ISABELLE_HOME" >/dev/null || failed
-
-TARGET_DIR="src/Tools/jEdit/dist"
-TARGET_JAR0="$TARGET_DIR/jars/Isabelle-jEdit-base.jar"
-TARGET_JAR="$TARGET_DIR/jars/Isabelle-jEdit.jar"
-TARGET_SHASUM="$TARGET_DIR/Isabelle-jEdit.shasum"
-
-declare -a TARGET_DEPS=("lib/classes/Pure.jar" "$TARGET_DIR/jedit.jar")
-
-splitarray ":" "$ISABELLE_JEDIT_JARS"
-for DEP in "${SPLITARRAY[@]}"
-do
- TARGET_DEPS["${#TARGET_DEPS[@]}"]="$TARGET_DIR/jars/$(basename "$DEP")"
-done
-
-function target_shasum()
-(
- shasum -a1 -b "$TARGET_JAR0" "$TARGET_JAR" "${TARGET_DEPS[@]}" \
- "${SOURCES0[@]}" "${RESOURCES0[@]}" "${SOURCES[@]}" "${RESOURCES[@]}" 2>/dev/null
-)
-
-function target_clean()
-{
- rm -rf "$ISABELLE_HOME/$TARGET_DIR"
-}
-
-[ -n "$FRESH_BUILD" ] && target_clean
-
-
-## build
-
-BUILD_DIR="$TARGET_DIR/build"
-
-function init_resources ()
-{
- mkdir -p "$BUILD_DIR" || failed
- cp -p -R "$@" "$BUILD_DIR/."
-}
-
-function compile_sources()
-{
- (
- #FIXME workarounds for scalac 2.11.0
- export CYGWIN="nodosfilewarning"
- function stty() { :; }
- export -f stty
-
- for DEP in "${TARGET_DEPS[@]}"
- do
- classpath "$DEP"
- done
- export CLASSPATH="$(platform_path "$ISABELLE_CLASSPATH")"
- isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS -d "$BUILD_DIR" "$@"
- ) || fail "Failed to compile sources"
-}
-
-function make_jar()
-{
- isabelle_jdk jar -c -f "$1" -C "$BUILD_DIR" . || failed
- rm -rf "$ISABELLE_HOME/$BUILD_DIR"
-}
-
-target_shasum | cmp "$TARGET_SHASUM" >/dev/null 2>/dev/null
-if [ -e "$ISABELLE_HOME/Admin/build" -a "$?" -ne 0 ]; then
- echo "### Building Isabelle/jEdit ..."
-
- target_clean || failed
- mkdir -p "$TARGET_DIR" || failed
-
- cp -p -R "$ISABELLE_JEDIT_HOME/." "$TARGET_DIR/."
-
- init_resources "${RESOURCES0[@]}"
- compile_sources "${SOURCES0[@]}"
- make_jar "$TARGET_JAR0"
- classpath "$TARGET_JAR0"
-
- init_resources "${RESOURCES[@]}"
- compile_sources "${SOURCES[@]}"
- make_jar "$TARGET_JAR"
-
- target_shasum > "$TARGET_SHASUM"
-fi
-
-
## main
-popd >/dev/null
+isabelle_admin_build browser || exit "$?"
+
+if [ -n "$FRESH_BUILD" ]; then
+ isabelle_admin_build jars_fresh || exit "$?"
+else
+ isabelle_admin_build jars || exit "$?"
+fi
if [ "$BUILD_ONLY" = false ]
then
@@ -343,7 +169,6 @@
export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_REQUIREMENTS \
JEDIT_INCLUDE_SESSIONS JEDIT_PRINT_MODE JEDIT_NO_BUILD JEDIT_BUILD_MODE
export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY"
- classpath "$JEDIT_HOME/dist/jedit.jar"
exec isabelle java -splash:"$(platform_path "$ISABELLE_HOME/lib/logo/isabelle.gif")" \
- "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
+ "${JAVA_ARGS[@]}" isabelle.jedit.Main "${ARGS[@]}"
fi
--- a/src/Tools/jEdit/lib/Tools/jedit_client Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit_client Thu Jul 15 22:51:49 2021 +0200
@@ -99,8 +99,7 @@
if [ -f "$JEDIT_SETTINGS/$SERVER_NAME" ]
then
- exec isabelle java "${JAVA_ARGS[@]}" \
- -jar $(platform_path "$JEDIT_HOME/dist/jedit.jar") \
+ exec isabelle java "${JAVA_ARGS[@]}" org.gjt.sp.jedit.jEdit \
"-settings=$(platform_path "$JEDIT_SETTINGS")" \
-server="$SERVER_NAME" -reuseview "${ARGS[@]}"
else
--- a/src/Tools/jEdit/src-base/Isabelle_Base.props Thu Jul 15 16:11:52 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-## Isabelle_Base plugin properties
-##
-##:encoding=ISO-8859-1:wrap=soft:maxLineLen=100:
-
-#identification
-plugin.isabelle.jedit_base.Plugin.name=Isabelle Base
-plugin.isabelle.jedit_base.Plugin.author=Makarius Wenzel
-plugin.isabelle.jedit_base.Plugin.version=1.0
-plugin.isabelle.jedit_base.Plugin.description=Isabelle Base: DO NOT UNLOAD!
-
-#system parameters
-plugin.isabelle.jedit_base.Plugin.activate=startup
-plugin.isabelle.jedit_base.Plugin.usePluginHome=false
-
-#dependencies
-plugin.isabelle.jedit_base.Plugin.depend.0=jdk 11
-plugin.isabelle.jedit_base.Plugin.depend.1=jedit 05.05.00.00
--- a/src/Tools/jEdit/src-base/dockable.scala Thu Jul 15 16:11:52 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-/* Title: Tools/jEdit/src-base/dockable.scala
- Author: Makarius
-
-Generic dockable window.
-*/
-
-package isabelle.jedit_base
-
-
-import isabelle._
-
-import java.awt.{Dimension, Component, BorderLayout}
-import javax.swing.JPanel
-
-import org.gjt.sp.jedit.View
-import org.gjt.sp.jedit.gui.{DefaultFocusComponent, DockableWindowManager}
-
-
-class Dockable(view: View, position: String)
- extends JPanel(new BorderLayout) with DefaultFocusComponent
-{
- if (position == DockableWindowManager.FLOATING)
- setPreferredSize(new Dimension(500, 250))
-
- def focusOnDefaultComponent(): Unit = JEdit_Lib.request_focus_view(view)
-
- def set_content(c: Component): Unit = add(c, BorderLayout.CENTER)
- def set_content(c: scala.swing.Component): Unit = add(c.peer, BorderLayout.CENTER)
-
- def detach_operation: Option[() => Unit] = None
-
- protected def init(): Unit = {}
- protected def exit(): Unit = {}
-
- override def addNotify(): Unit =
- {
- super.addNotify()
- init()
- }
-
- override def removeNotify(): Unit =
- {
- exit()
- super.removeNotify()
- }
-}
--- a/src/Tools/jEdit/src-base/isabelle_encoding.scala Thu Jul 15 16:11:52 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,59 +0,0 @@
-/* Title: Tools/jEdit/src-base/isabelle_encoding.scala
- Author: Makarius
-
-Isabelle encoding -- based on UTF-8.
-*/
-
-package isabelle.jedit_base
-
-
-import isabelle._
-
-import org.gjt.sp.jedit.io.Encoding
-
-import java.nio.charset.{Charset, CodingErrorAction, CharacterCodingException}
-import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter,
- CharArrayReader, ByteArrayOutputStream}
-
-import scala.io.{Codec, BufferedSource}
-
-
-class Isabelle_Encoding extends Encoding
-{
- private val BUFSIZE = 32768
-
- private def text_reader(in: InputStream, codec: Codec, strict: Boolean): Reader =
- {
- val source = (new BufferedSource(in)(codec)).mkString
-
- if (strict && Codepoint.iterator(source).exists(Symbol.is_code))
- throw new CharacterCodingException()
-
- new CharArrayReader(Symbol.decode(source).toArray)
- }
-
- override def getTextReader(in: InputStream): Reader =
- text_reader(in, UTF8.codec(), true)
-
- override def getPermissiveTextReader(in: InputStream): Reader =
- {
- val codec = UTF8.codec()
- codec.onMalformedInput(CodingErrorAction.REPLACE)
- codec.onUnmappableCharacter(CodingErrorAction.REPLACE)
- text_reader(in, codec, false)
- }
-
- override def getTextWriter(out: OutputStream): Writer =
- {
- val buffer = new ByteArrayOutputStream(BUFSIZE) {
- override def flush(): Unit =
- {
- val text = Symbol.encode(toString(UTF8.charset_name))
- out.write(UTF8.bytes(text))
- out.flush()
- }
- override def close(): Unit = out.close()
- }
- new OutputStreamWriter(buffer, UTF8.charset.newEncoder())
- }
-}
--- a/src/Tools/jEdit/src-base/jedit_lib.scala Thu Jul 15 16:11:52 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-/* Title: Tools/jEdit/src-base/jedit_lib.scala
- Author: Makarius
-
-Misc library functions for jEdit.
-*/
-
-package isabelle.jedit_base
-
-
-import isabelle._
-
-import org.gjt.sp.jedit.{jEdit, View}
-
-
-object JEdit_Lib
-{
- def request_focus_view(alt_view: View = null): Unit =
- {
- val view = if (alt_view != null) alt_view else jEdit.getActiveView()
- if (view != null) {
- val text_area = view.getTextArea
- if (text_area != null) text_area.requestFocus()
- }
- }
-}
\ No newline at end of file
--- a/src/Tools/jEdit/src-base/pide_docking_framework.scala Thu Jul 15 16:11:52 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,72 +0,0 @@
-/* Title: Tools/jEdit/src-base/pide_docking_framework.scala
- Author: Makarius
-
-PIDE docking framework: "Original" with some add-ons.
-*/
-
-package isabelle.jedit_base
-
-
-import isabelle._
-
-import java.util.{List => JList}
-import java.awt.event.{ActionListener, ActionEvent}
-import javax.swing.{JPopupMenu, JMenuItem}
-
-import org.gjt.sp.jedit.View
-import org.gjt.sp.jedit.gui.{DockableWindowManagerProvider, DockableWindowFactory,
- DockableWindowManager, DockableWindowManagerImpl, DockableWindowContainer,
- FloatingWindowContainer, PanelWindowContainer}
-
-
-class PIDE_Docking_Framework extends DockableWindowManagerProvider
-{
- override def create(
- view: View,
- instance: DockableWindowFactory,
- config: View.ViewConfig): DockableWindowManager =
- new DockableWindowManagerImpl(view, instance, config)
- {
- override def createPopupMenu(
- container: DockableWindowContainer,
- dockable_name: String,
- clone: Boolean): JPopupMenu =
- {
- val menu = super.createPopupMenu(container, dockable_name, clone)
-
- val detach_operation: Option[() => Unit] =
- container match {
- case floating: FloatingWindowContainer =>
- Untyped.get[AnyRef](Untyped.get[AnyRef](floating, "entry"), "win") match {
- case dockable: Dockable => dockable.detach_operation
- case _ => None
- }
-
- case panel: PanelWindowContainer =>
- val entries = Untyped.get[JList[AnyRef]](panel, "dockables").toArray
- val wins =
- (for {
- entry <- entries.iterator
- if Untyped.get[String](Untyped.get(entry, "factory"), "name") == dockable_name
- win = Untyped.get[Any](entry, "win")
- if win != null
- } yield win).toList
- wins match {
- case List(dockable: Dockable) => dockable.detach_operation
- case _ => None
- }
-
- case _ => None
- }
- if (detach_operation.isDefined) {
- val detach_item = new JMenuItem("Detach")
- detach_item.addActionListener(new ActionListener {
- def actionPerformed(evt: ActionEvent): Unit = detach_operation.get.apply()
- })
- menu.add(detach_item)
- }
-
- menu
- }
- }
-}
--- a/src/Tools/jEdit/src-base/plugin.scala Thu Jul 15 16:11:52 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-/* Title: Tools/jEdit/src-base/plugin.scala
- Author: Makarius
-
-Isabelle base environment for jEdit.
-*/
-
-package isabelle.jedit_base
-
-
-import isabelle._
-
-import org.gjt.sp.jedit.{EBMessage, Debug, EBPlugin}
-import org.gjt.sp.util.SyntaxUtilities
-
-
-class Plugin extends EBPlugin
-{
- override def start(): Unit =
- {
- Isabelle_System.init()
-
- GUI.use_isabelle_fonts()
-
- Debug.DISABLE_SEARCH_DIALOG_POOL = true
-
- Syntax_Style.dummy_style_extender()
- }
-
- override def stop(): Unit =
- {
- Syntax_Style.set_style_extender(new SyntaxUtilities.StyleExtender)
- }
-
- override def handleMessage(message: EBMessage): Unit = {}
-}
--- a/src/Tools/jEdit/src-base/services.xml Thu Jul 15 16:11:52 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-<?xml version="1.0"?>
-<!DOCTYPE SERVICES SYSTEM "services.dtd">
-
-<SERVICES>
- <SERVICE NAME="UTF-8-Isabelle" CLASS="org.gjt.sp.jedit.io.Encoding">
- new isabelle.jedit_base.Isabelle_Encoding();
- </SERVICE>
- <SERVICE CLASS="org.gjt.sp.jedit.gui.DockingFrameworkProvider" NAME="PIDE">
- new isabelle.jedit_base.PIDE_Docking_Framework();
- </SERVICE>
-</SERVICES>
--- a/src/Tools/jEdit/src-base/syntax_style.scala Thu Jul 15 16:11:52 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-/* Title: Tools/jEdit/src-base/syntax_style.scala
- Author: Makarius
-
-Extended syntax styles: dummy version.
-*/
-
-package isabelle.jedit_base
-
-
-import isabelle._
-
-import org.gjt.sp.util.SyntaxUtilities
-import org.gjt.sp.jedit.syntax.{Token => JEditToken, SyntaxStyle}
-import org.gjt.sp.jedit.jEdit
-
-
-object Syntax_Style
-{
- private val plain_range: Int = JEditToken.ID_COUNT
- private val full_range = 6 * plain_range + 1
-
- object Dummy_Extender extends SyntaxUtilities.StyleExtender
- {
- override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
- {
- val new_styles = new Array[SyntaxStyle](full_range)
- for (i <- 0 until full_range) {
- new_styles(i) = styles(i % plain_range)
- }
- new_styles
- }
- }
-
- def set_style_extender(extender: SyntaxUtilities.StyleExtender): Unit =
- {
- SyntaxUtilities.setStyleExtender(extender)
- GUI_Thread.later { jEdit.propertiesChanged }
- }
-
- def dummy_style_extender(): Unit = set_style_extender(Dummy_Extender)
-}
--- a/src/Tools/jEdit/src/Isabelle.props Thu Jul 15 16:11:52 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,111 +0,0 @@
-## Isabelle plugin properties
-##
-##:encoding=ISO-8859-1:wrap=soft:maxLineLen=100:
-
-#identification
-plugin.isabelle.jedit.Plugin.name=Isabelle
-plugin.isabelle.jedit.Plugin.author=Johannes Hölzl, Lars Hupel, Fabian Immler, Markus Kaiser, Makarius Wenzel
-plugin.isabelle.jedit.Plugin.version=11.2
-plugin.isabelle.jedit.Plugin.description=Isabelle Prover IDE
-
-#system parameters
-plugin.isabelle.jedit.Plugin.activate=defer
-plugin.isabelle.jedit.Plugin.usePluginHome=false
-
-#dependencies
-plugin.isabelle.jedit.Plugin.depend.0=jdk 11
-plugin.isabelle.jedit.Plugin.depend.1=jedit 05.05.00.00
-plugin.isabelle.jedit.Plugin.depend.2=plugin console.ConsolePlugin 5.1.4
-plugin.isabelle.jedit.Plugin.depend.3=plugin errorlist.ErrorListPlugin 2.3
-plugin.isabelle.jedit.Plugin.depend.4=plugin sidekick.SideKickPlugin 1.8
-plugin.isabelle.jedit.Plugin.depend.5=plugin isabelle.jedit_base.Plugin 1.0
-
-#options
-plugin.isabelle.jedit.Plugin.option-group=isabelle-general isabelle-rendering
-options.isabelle-general.label=General
-options.isabelle-general.code=new isabelle.jedit.Isabelle_Options1();
-options.isabelle-rendering.label=Rendering
-options.isabelle-rendering.code=new isabelle.jedit.Isabelle_Options2();
-
-#menu actions and dockables
-plugin.isabelle.jedit.Plugin.menu.label=Isabelle
-plugin.isabelle.jedit.Plugin.menu= \
- isabelle-export-browser \
- isabelle-session-browser \
- isabelle.preview \
- isabelle.draft \
- isabelle.java-monitor \
- - \
- isabelle-debugger \
- isabelle-documentation \
- isabelle-monitor \
- isabelle-output \
- isabelle-protocol \
- isabelle-query \
- isabelle-raw-output \
- isabelle-simplifier-trace \
- isabelle-sledgehammer \
- isabelle-state \
- isabelle-symbols \
- isabelle-syslog \
- isabelle-theories \
- isabelle-timing
-isabelle-debugger.label=Debugger panel
-isabelle-debugger.title=Debugger
-isabelle-documentation.label=Documentation panel
-isabelle-documentation.title=Documentation
-isabelle-graphview.label=Graphview panel
-isabelle-graphview.title=Graphview
-isabelle-info.label=Info panel
-isabelle-info.title=Info
-isabelle-monitor.label=Monitor panel
-isabelle-monitor.title=Monitor
-isabelle-output.label=Output panel
-isabelle-output.title=Output
-isabelle-protocol.label=Protocol panel
-isabelle-protocol.title=Protocol
-isabelle-query.label=Query panel
-isabelle-query.title=Query
-isabelle-raw-output.label=Raw Output panel
-isabelle-raw-output.title=Raw Output
-isabelle-simplifier-trace.label=Simplifier Trace panel
-isabelle-simplifier-trace.title=Simplifier Trace
-isabelle-sledgehammer.label=Sledgehammer panel
-isabelle-sledgehammer.title=Sledgehammer
-isabelle-state.label=State panel
-isabelle-state.title=State
-isabelle-symbols.label=Symbols panel
-isabelle-symbols.title=Symbols
-isabelle-syslog.label=Syslog panel
-isabelle-syslog.title=Syslog
-isabelle-theories.label=Theories panel
-isabelle-theories.title=Theories
-isabelle-timing.label=Timing panel
-isabelle-timing.title=Timing
-
-#SideKick
-mode.isabelle-news.folding=sidekick
-mode.isabelle-news.sidekick.parser=isabelle-news
-mode.isabelle-options.folding=sidekick
-mode.isabelle-options.sidekick.parser=isabelle-options
-mode.isabelle-root.folding=sidekick
-mode.isabelle-root.sidekick.parser=isabelle-root
-mode.isabelle.customSettings=true
-mode.isabelle.folding=isabelle
-mode.isabelle.sidekick.parser=isabelle
-mode.isabelle.sidekick.showStatusWindow.label=true
-mode.isabelle-ml.folding=sidekick
-mode.isabelle-ml.sidekick.parser=isabelle-ml
-mode.sml.folding=sidekick
-mode.sml.sidekick.parser=isabelle-sml
-mode.bibtex.folding=sidekick
-mode.bibtex.sidekick.parser=bibtex
-sidekick.parser.isabelle.label=isabelle
-sidekick.parser.isabelle-context.label=isabelle-context
-sidekick.parser.isabelle-markup.label=isabelle-markup
-sidekick.parser.isabelle-ml.label=isabelle-ml
-sidekick.parser.isabelle-sml.label=isabelle-sml
-sidekick.parser.isabelle-news.label=isabelle-news
-sidekick.parser.isabelle-options.label=isabelle-options
-sidekick.parser.isabelle-root.label=isabelle-root
-sidekick.parser.bibtex.label=bibtex
--- a/src/Tools/jEdit/src/actions.xml Thu Jul 15 16:11:52 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,230 +0,0 @@
-<?xml version="1.0"?>
-<!DOCTYPE ACTIONS SYSTEM "actions.dtd">
-
-<ACTIONS>
- <ACTION NAME="isabelle.set-continuous-checking">
- <CODE>
- isabelle.jedit.Isabelle.set_continuous_checking();
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.reset-continuous-checking">
- <CODE>
- isabelle.jedit.Isabelle.reset_continuous_checking();
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.toggle-continuous-checking">
- <CODE>
- isabelle.jedit.Isabelle.toggle_continuous_checking();
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.set-node-required">
- <CODE>
- isabelle.jedit.Isabelle.set_node_required(view);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.reset-node-required">
- <CODE>
- isabelle.jedit.Isabelle.reset_node_required(view);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.toggle-node-required">
- <CODE>
- isabelle.jedit.Isabelle.toggle_node_required(view);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.update-state">
- <CODE>
- isabelle.jedit.Isabelle.update_state(view);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.reset-font-size">
- <CODE>
- isabelle.jedit.Isabelle.reset_font_size();
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.increase-font-size">
- <CODE>
- isabelle.jedit.Isabelle.increase_font_size();
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.increase-font-size2">
- <CODE>
- isabelle.jedit.Isabelle.increase_font_size();
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.decrease-font-size">
- <CODE>
- isabelle.jedit.Isabelle.decrease_font_size();
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.decrease-font-size2">
- <CODE>
- isabelle.jedit.Isabelle.decrease_font_size();
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.newline">
- <CODE>
- isabelle.jedit.Isabelle.newline(textArea);
- </CODE>
- </ACTION>
- <ACTION NAME="toggle-full-screen">
- <CODE>
- isabelle.jedit.Isabelle.toggle_full_screen(view);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.goto-entity">
- <CODE>
- isabelle.jedit.Isabelle.goto_entity(view);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.select-entity">
- <CODE>
- isabelle.jedit.Isabelle.select_entity(textArea);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.complete">
- <CODE>
- isabelle.jedit.Isabelle.complete(view, false);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.tooltip">
- <CODE>
- isabelle.jedit.Isabelle.show_tooltip(view, true);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.message">
- <CODE>
- isabelle.jedit.Isabelle.show_tooltip(view, false);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.first-error">
- <CODE>
- isabelle.jedit.Isabelle.goto_first_error(view);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.last-error">
- <CODE>
- isabelle.jedit.Isabelle.goto_last_error(view);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.prev-error">
- <CODE>
- isabelle.jedit.Isabelle.goto_prev_error(view);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.next-error">
- <CODE>
- isabelle.jedit.Isabelle.goto_next_error(view);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.complete-word">
- <CODE>
- isabelle.jedit.Isabelle.complete(view, true);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.control-sub">
- <CODE>
- isabelle.jedit.Isabelle.control_sub(textArea);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.control-sup">
- <CODE>
- isabelle.jedit.Isabelle.control_sup(textArea);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.control-bold">
- <CODE>
- isabelle.jedit.Isabelle.control_bold(textArea);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.control-emph">
- <CODE>
- isabelle.jedit.Isabelle.control_emph(textArea);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.control-reset">
- <CODE>
- isabelle.jedit.Isabelle.control_reset(textArea);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.input-bsub">
- <CODE>
- isabelle.jedit.Isabelle.input_bsub(textArea);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.input-bsup">
- <CODE>
- isabelle.jedit.Isabelle.input_bsup(textArea);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.antiquoted_cartouche">
- <CODE>
- isabelle.jedit.Isabelle.antiquoted_cartouche(textArea);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.include-word">
- <CODE>
- isabelle.jedit.Isabelle.update_dictionary(textArea, true, false);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.include-word-permanently">
- <CODE>
- isabelle.jedit.Isabelle.update_dictionary(textArea, true, true);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.exclude-word">
- <CODE>
- isabelle.jedit.Isabelle.update_dictionary(textArea, false, false);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.exclude-word-permanently">
- <CODE>
- isabelle.jedit.Isabelle.update_dictionary(textArea, false, true);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.reset-words">
- <CODE>
- isabelle.jedit.Isabelle.reset_dictionary();
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.toggle-breakpoint">
- <CODE>
- isabelle.jedit.Isabelle.toggle_breakpoint(textArea);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.options">
- <CODE>
- isabelle.jedit.Isabelle.plugin_options(view);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.preview">
- <CODE>
- isabelle.jedit.Document_Model.open_preview(view, false);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.draft">
- <CODE>
- isabelle.jedit.Document_Model.open_preview(view, true);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle-export-browser">
- <CODE>
- isabelle.jedit.Isabelle_Export.open_browser(view);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle-session-browser">
- <CODE>
- isabelle.jedit.Isabelle_Session.open_browser(view);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.keymap-merge">
- <CODE>
- isabelle.jedit.Keymap_Merge.check_dialog(view);
- </CODE>
- </ACTION>
- <ACTION NAME="isabelle.java-monitor">
- <CODE>
- isabelle.jedit.Isabelle.java_monitor(view);
- </CODE>
- </ACTION>
-</ACTIONS>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/base_plugin.scala Thu Jul 15 22:51:49 2021 +0200
@@ -0,0 +1,35 @@
+/* Title: Tools/jEdit/src/base_plugin.scala
+ Author: Makarius
+
+Isabelle base environment for jEdit.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import org.gjt.sp.jedit.{EBMessage, Debug, EBPlugin}
+import org.gjt.sp.util.SyntaxUtilities
+
+
+class Base_Plugin extends EBPlugin
+{
+ override def start(): Unit =
+ {
+ Isabelle_System.init()
+
+ GUI.use_isabelle_fonts()
+
+ Debug.DISABLE_SEARCH_DIALOG_POOL = true
+
+ Syntax_Style.set_extender(Syntax_Style.Base_Extender)
+ }
+
+ override def stop(): Unit =
+ {
+ Syntax_Style.set_extender(new SyntaxUtilities.StyleExtender)
+ }
+
+ override def handleMessage(message: EBMessage): Unit = {}
+}
--- a/src/Tools/jEdit/src/debugger_dockable.scala Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala Thu Jul 15 22:51:49 2021 +0200
@@ -8,7 +8,6 @@
import isabelle._
-import isabelle.jedit_base.Dockable
import java.awt.{BorderLayout, Dimension}
import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent, FocusAdapter, FocusEvent,
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/dockable.scala Thu Jul 15 22:51:49 2021 +0200
@@ -0,0 +1,46 @@
+/* Title: Tools/jEdit/src/dockable.scala
+ Author: Makarius
+
+Generic dockable window.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.awt.{Dimension, Component, BorderLayout}
+import javax.swing.JPanel
+
+import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.gui.{DefaultFocusComponent, DockableWindowManager}
+
+
+class Dockable(view: View, position: String)
+ extends JPanel(new BorderLayout) with DefaultFocusComponent
+{
+ if (position == DockableWindowManager.FLOATING)
+ setPreferredSize(new Dimension(500, 250))
+
+ def focusOnDefaultComponent(): Unit = JEdit_Lib.request_focus_view(view)
+
+ def set_content(c: Component): Unit = add(c, BorderLayout.CENTER)
+ def set_content(c: scala.swing.Component): Unit = add(c.peer, BorderLayout.CENTER)
+
+ def detach_operation: Option[() => Unit] = None
+
+ protected def init(): Unit = {}
+ protected def exit(): Unit = {}
+
+ override def addNotify(): Unit =
+ {
+ super.addNotify()
+ init()
+ }
+
+ override def removeNotify(): Unit =
+ {
+ exit()
+ super.removeNotify()
+ }
+}
--- a/src/Tools/jEdit/src/dockables.xml Thu Jul 15 16:11:52 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-<?xml version="1.0"?>
-<!DOCTYPE DOCKABLES SYSTEM "dockables.dtd">
-
-<DOCKABLES>
- <DOCKABLE NAME="isabelle-debugger" MOVABLE="TRUE">
- new isabelle.jedit.Debugger_Dockable(view, position);
- </DOCKABLE>
- <DOCKABLE NAME="isabelle-documentation" MOVABLE="TRUE">
- new isabelle.jedit.Documentation_Dockable(view, position);
- </DOCKABLE>
- <DOCKABLE NAME="isabelle-info" MOVABLE="TRUE">
- new isabelle.jedit.Info_Dockable(view, position);
- </DOCKABLE>
- <DOCKABLE NAME="isabelle-graphview" MOVABLE="TRUE">
- new isabelle.jedit.Graphview_Dockable(view, position);
- </DOCKABLE>
- <DOCKABLE NAME="isabelle-monitor" MOVABLE="TRUE">
- new isabelle.jedit.Monitor_Dockable(view, position);
- </DOCKABLE>
- <DOCKABLE NAME="isabelle-output" MOVABLE="TRUE">
- new isabelle.jedit.Output_Dockable(view, position);
- </DOCKABLE>
- <DOCKABLE NAME="isabelle-protocol" MOVABLE="TRUE">
- new isabelle.jedit.Protocol_Dockable(view, position);
- </DOCKABLE>
- <DOCKABLE NAME="isabelle-query" MOVABLE="TRUE">
- new isabelle.jedit.Query_Dockable(view, position);
- </DOCKABLE>
- <DOCKABLE NAME="isabelle-raw-output" MOVABLE="TRUE">
- new isabelle.jedit.Raw_Output_Dockable(view, position);
- </DOCKABLE>
- <DOCKABLE NAME="isabelle-simplifier-trace" MOVABLE="TRUE">
- new isabelle.jedit.Simplifier_Trace_Dockable(view, position);
- </DOCKABLE>
- <DOCKABLE NAME="isabelle-sledgehammer" MOVABLE="TRUE">
- new isabelle.jedit.Sledgehammer_Dockable(view, position);
- </DOCKABLE>
- <DOCKABLE NAME="isabelle-state" MOVABLE="TRUE">
- new isabelle.jedit.State_Dockable(view, position);
- </DOCKABLE>
- <DOCKABLE NAME="isabelle-symbols" MOVABLE="TRUE">
- new isabelle.jedit.Symbols_Dockable(view, position);
- </DOCKABLE>
- <DOCKABLE NAME="isabelle-syslog" MOVABLE="TRUE">
- new isabelle.jedit.Syslog_Dockable(view, position);
- </DOCKABLE>
- <DOCKABLE NAME="isabelle-theories" MOVABLE="TRUE">
- new isabelle.jedit.Theories_Dockable(view, position);
- </DOCKABLE>
- <DOCKABLE NAME="isabelle-timing" MOVABLE="TRUE">
- new isabelle.jedit.Timing_Dockable(view, position);
- </DOCKABLE>
-</DOCKABLES>
--- a/src/Tools/jEdit/src/document_model.scala Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Thu Jul 15 22:51:49 2021 +0200
@@ -80,6 +80,8 @@
private val state = Synchronized(State()) // owned by GUI thread
+ def reset(): Unit = state.change(_ => State())
+
def get_models(): Map[Document.Node.Name, Document_Model] = state.value.models
def get(name: Document.Node.Name): Option[Document_Model] = get_models().get(name)
def get(buffer: JEditBuffer): Option[Buffer_Model] = state.value.buffer_models.get(buffer)
--- a/src/Tools/jEdit/src/documentation_dockable.scala Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Tools/jEdit/src/documentation_dockable.scala Thu Jul 15 22:51:49 2021 +0200
@@ -8,7 +8,6 @@
import isabelle._
-import isabelle.jedit_base.Dockable
import java.awt.Dimension
import java.awt.event.{KeyEvent, KeyAdapter, MouseEvent, MouseAdapter}
--- a/src/Tools/jEdit/src/graphview_dockable.scala Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Thu Jul 15 22:51:49 2021 +0200
@@ -8,7 +8,6 @@
import isabelle._
-import isabelle.jedit_base.Dockable
import javax.swing.JComponent
import java.awt.{Point, Font}
--- a/src/Tools/jEdit/src/info_dockable.scala Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala Thu Jul 15 22:51:49 2021 +0200
@@ -8,7 +8,6 @@
import isabelle._
-import isabelle.jedit_base.Dockable
import java.awt.BorderLayout
import java.awt.event.{ComponentEvent, ComponentAdapter, WindowFocusListener, WindowEvent}
--- a/src/Tools/jEdit/src/isabelle_encoding.scala Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Tools/jEdit/src/isabelle_encoding.scala Thu Jul 15 22:51:49 2021 +0200
@@ -10,6 +10,13 @@
import isabelle._
import org.gjt.sp.jedit.buffer.JEditBuffer
+import org.gjt.sp.jedit.io.Encoding
+
+import java.nio.charset.{Charset, CodingErrorAction, CharacterCodingException}
+import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter,
+ CharArrayReader, ByteArrayOutputStream}
+
+import scala.io.{Codec, BufferedSource}
object Isabelle_Encoding
@@ -20,3 +27,43 @@
def perhaps_decode(buffer: JEditBuffer, s: String): String =
if (is_active(buffer)) Symbol.decode(s) else s
}
+
+class Isabelle_Encoding extends Encoding
+{
+ private val BUFSIZE = 32768
+
+ private def text_reader(in: InputStream, codec: Codec, strict: Boolean): Reader =
+ {
+ val source = (new BufferedSource(in)(codec)).mkString
+
+ if (strict && Codepoint.iterator(source).exists(Symbol.is_code))
+ throw new CharacterCodingException()
+
+ new CharArrayReader(Symbol.decode(source).toArray)
+ }
+
+ override def getTextReader(in: InputStream): Reader =
+ text_reader(in, UTF8.codec(), true)
+
+ override def getPermissiveTextReader(in: InputStream): Reader =
+ {
+ val codec = UTF8.codec()
+ codec.onMalformedInput(CodingErrorAction.REPLACE)
+ codec.onUnmappableCharacter(CodingErrorAction.REPLACE)
+ text_reader(in, codec, false)
+ }
+
+ override def getTextWriter(out: OutputStream): Writer =
+ {
+ val buffer = new ByteArrayOutputStream(BUFSIZE) {
+ override def flush(): Unit =
+ {
+ val text = Symbol.encode(toString(UTF8.charset_name))
+ out.write(UTF8.bytes(text))
+ out.flush()
+ }
+ override def close(): Unit = out.close()
+ }
+ new OutputStreamWriter(buffer, UTF8.charset.newEncoder())
+ }
+}
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Thu Jul 15 16:11:52 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,268 +0,0 @@
-/* Title: Tools/jEdit/src/isabelle_sidekick.scala
- Author: Fabian Immler, TU Munich
- Author: Makarius
-
-SideKick parsers for Isabelle proof documents.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-import javax.swing.tree.DefaultMutableTreeNode
-import javax.swing.text.Position
-import javax.swing.{JLabel, Icon}
-
-import org.gjt.sp.jedit.Buffer
-import sidekick.{SideKickParser, SideKickParsedData, IAsset}
-
-
-object Isabelle_Sidekick
-{
- def int_to_pos(offset: Text.Offset): Position =
- new Position { def getOffset = offset; override def toString: String = offset.toString }
-
- def root_data(buffer: Buffer): SideKickParsedData =
- {
- val data = new SideKickParsedData(buffer.getName)
- data.getAsset(data.root).setEnd(int_to_pos(buffer.getLength))
- data
- }
-
- class Keyword_Asset(keyword: String, text: String, range: Text.Range) extends IAsset
- {
- private val css = GUI.imitate_font_css(GUI.label_font())
-
- protected var _name = text
- protected var _start = int_to_pos(range.start)
- protected var _end = int_to_pos(range.stop)
- override def getIcon: Icon = null
- override def getShortString: String =
- {
- val n = keyword.length
- val s =
- _name.indexOf(keyword) match {
- case i if i >= 0 && n > 0 =>
- HTML.output(_name.substring(0, i)) +
- "<b>" + HTML.output(keyword) + "</b>" +
- HTML.output(_name.substring(i + n))
- case _ => HTML.output(_name)
- }
- "<html><span style=\"" + css + "\">" + s + "</span></html>"
- }
- override def getLongString: String = _name
- override def getName: String = _name
- override def setName(name: String): Unit = _name = name
- override def getStart: Position = _start
- override def setStart(start: Position): Unit = _start = start
- override def getEnd: Position = _end
- override def setEnd(end: Position): Unit = _end = end
- override def toString: String = _name
- }
-
- class Asset(name: String, range: Text.Range) extends Keyword_Asset("", name, range)
-
- def swing_markup_tree(tree: Markup_Tree, parent: DefaultMutableTreeNode,
- swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode): Unit =
- {
- for ((_, entry) <- tree.branches) {
- val node = swing_node(Text.Info(entry.range, entry.markup))
- swing_markup_tree(entry.subtree, node, swing_node)
- parent.add(node)
- }
- }
-}
-
-
-class Isabelle_Sidekick(name: String) extends SideKickParser(name)
-{
- override def supportsCompletion = false
-
-
- /* parsing */
-
- @volatile protected var stopped = false
- override def stop() = { stopped = true }
-
- def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = false
-
- def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData =
- {
- stopped = false
-
- // FIXME lock buffer (!??)
- val data = Isabelle_Sidekick.root_data(buffer)
- val syntax = Isabelle.buffer_syntax(buffer)
- val ok =
- if (syntax.isDefined) {
- val ok = parser(buffer, syntax.get, data)
- if (stopped) { data.root.add(new DefaultMutableTreeNode("<stopped>")); true }
- else ok
- }
- else false
- if (!ok) data.root.add(new DefaultMutableTreeNode("<ignored>"))
-
- data
- }
-}
-
-
-class Isabelle_Sidekick_Structure(
- name: String,
- node_name: Buffer => Option[Document.Node.Name],
- parse: (Outer_Syntax, Document.Node.Name, CharSequence) => List[Document_Structure.Document])
- extends Isabelle_Sidekick(name)
-{
- override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
- {
- def make_tree(
- parent: DefaultMutableTreeNode,
- offset: Text.Offset,
- documents: List[Document_Structure.Document]): Unit =
- {
- documents.foldLeft(offset) {
- case (i, document) =>
- document match {
- case Document_Structure.Block(name, text, body) =>
- val range = Text.Range(i, i + document.length)
- val node =
- new DefaultMutableTreeNode(
- new Isabelle_Sidekick.Keyword_Asset(name, Library.first_line(text), range))
- parent.add(node)
- make_tree(node, i, body)
- case _ =>
- }
- i + document.length
- }
- }
-
- node_name(buffer) match {
- case Some(name) =>
- make_tree(data.root, 0, parse(syntax, name, JEdit_Lib.buffer_text(buffer)))
- true
- case None =>
- false
- }
- }
-}
-
-class Isabelle_Sidekick_Default extends
- Isabelle_Sidekick_Structure("isabelle",
- PIDE.resources.theory_node_name, Document_Structure.parse_sections)
-
-class Isabelle_Sidekick_Context extends
- Isabelle_Sidekick_Structure("isabelle-context",
- PIDE.resources.theory_node_name, Document_Structure.parse_blocks)
-
-class Isabelle_Sidekick_Options extends
- Isabelle_Sidekick_Structure("isabelle-options",
- _ => Some(Document.Node.Name("options")), Document_Structure.parse_sections)
-
-class Isabelle_Sidekick_Root extends
- Isabelle_Sidekick_Structure("isabelle-root",
- _ => Some(Document.Node.Name("ROOT")), Document_Structure.parse_sections)
-
-class Isabelle_Sidekick_ML extends
- Isabelle_Sidekick_Structure("isabelle-ml",
- buffer => Some(PIDE.resources.node_name(buffer)),
- (_, _, text) => Document_Structure.parse_ml_sections(false, text))
-
-class Isabelle_Sidekick_SML extends
- Isabelle_Sidekick_Structure("isabelle-sml",
- buffer => Some(PIDE.resources.node_name(buffer)),
- (_, _, text) => Document_Structure.parse_ml_sections(true, text))
-
-
-class Isabelle_Sidekick_Markup extends Isabelle_Sidekick("isabelle-markup")
-{
- override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
- {
- val opt_snapshot =
- Document_Model.get(buffer) match {
- case Some(model) if model.is_theory => Some(model.snapshot())
- case _ => None
- }
- opt_snapshot match {
- case Some(snapshot) =>
- for ((command, command_start) <- snapshot.node.command_iterator() if !stopped) {
- val markup =
- snapshot.state.command_markup(
- snapshot.version, command, Command.Markup_Index.markup,
- command.range, Markup.Elements.full)
- Isabelle_Sidekick.swing_markup_tree(markup, data.root,
- (info: Text.Info[List[XML.Elem]]) =>
- {
- val range = info.range + command_start
- val content = command.source(info.range).replace('\n', ' ')
- val info_text = Pretty.formatted(Pretty.fbreaks(info.info), margin = 40.0).mkString
-
- new DefaultMutableTreeNode(
- new Isabelle_Sidekick.Asset(command.toString, range) {
- override def getShortString: String = content
- override def getLongString: String = info_text
- override def toString: String = quote(content) + " " + range.toString
- })
- })
- }
- true
- case None => false
- }
- }
-}
-
-
-class Isabelle_Sidekick_News extends Isabelle_Sidekick("isabelle-news")
-{
- private val Heading1 = """^New in (.*)\w*$""".r
- private val Heading2 = """^\*\*\*\w*(.*)\w*\*\*\*\w*$""".r
-
- private def make_node(s: String, start: Text.Offset, stop: Text.Offset): DefaultMutableTreeNode =
- new DefaultMutableTreeNode(new Isabelle_Sidekick.Asset(s, Text.Range(start, stop)))
-
- override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
- {
- var offset = 0
- var end_offset = 0
-
- var start1: Option[(Int, String, Vector[DefaultMutableTreeNode])] = None
- var start2: Option[(Int, String)] = None
-
- def close1: Unit =
- start1 match {
- case Some((start_offset, s, body)) =>
- val node = make_node(s, start_offset, end_offset)
- body.foreach(node.add(_))
- data.root.add(node)
- start1 = None
- case None =>
- }
-
- def close2: Unit =
- start2 match {
- case Some((start_offset, s)) =>
- start1 match {
- case Some((start_offset1, s1, body)) =>
- val node = make_node(s, start_offset, end_offset)
- start1 = Some((start_offset1, s1, body :+ node))
- case None =>
- }
- start2 = None
- case None =>
- }
-
- for (line <- split_lines(JEdit_Lib.buffer_text(buffer)) if !stopped) {
- line match {
- case Heading1(s) => close2; close1; start1 = Some((offset, s, Vector()))
- case Heading2(s) => close2; start2 = Some((offset, s))
- case _ =>
- }
- offset += line.length + 1
- if (!line.forall(Character.isSpaceChar)) end_offset = offset
- }
- if (!stopped) { close2; close1 }
-
- true
- }
-}
-
--- a/src/Tools/jEdit/src/jedit_bibtex.scala Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Tools/jEdit/src/jedit_bibtex.scala Thu Jul 15 22:51:49 2021 +0200
@@ -22,8 +22,6 @@
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler}
-import sidekick.{SideKickParser, SideKickParsedData}
-
object JEdit_Bibtex
{
@@ -155,45 +153,4 @@
context2
}
}
-
-
-
- /** Sidekick parser **/
-
- class Sidekick_Parser extends SideKickParser("bibtex")
- {
- override def supportsCompletion = false
-
- private class Asset(label: String, label_html: String, range: Text.Range, source: String)
- extends Isabelle_Sidekick.Asset(label, range) {
- override def getShortString: String = label_html
- override def getLongString: String = source
- }
-
- def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData =
- {
- val data = Isabelle_Sidekick.root_data(buffer)
-
- try {
- var offset = 0
- for (chunk <- Bibtex.parse(JEdit_Lib.buffer_text(buffer))) {
- val kind = chunk.kind
- val name = chunk.name
- val source = chunk.source
- if (kind != "") {
- val label = kind + (if (name == "") "" else " " + name)
- val label_html =
- "<html><b>" + HTML.output(kind) + "</b>" +
- (if (name == "") "" else " " + HTML.output(name)) + "</html>"
- val range = Text.Range(offset, offset + source.length)
- val asset = new Asset(label, label_html, range, source)
- data.root.add(new DefaultMutableTreeNode(asset))
- }
- offset += source.length
- }
- data
- }
- catch { case ERROR(msg) => Output.warning(msg); null }
- }
- }
}
--- a/src/Tools/jEdit/src/jedit_lib.scala Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala Thu Jul 15 22:51:49 2021 +0200
@@ -320,7 +320,13 @@
/* key event handling */
def request_focus_view(alt_view: View = null): Unit =
- isabelle.jedit_base.JEdit_Lib.request_focus_view(alt_view)
+ {
+ val view = if (alt_view != null) alt_view else jEdit.getActiveView()
+ if (view != null) {
+ val text_area = view.getTextArea
+ if (text_area != null) text_area.requestFocus()
+ }
+ }
def propagate_key(view: View, evt: KeyEvent): Unit =
{
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/main.scala Thu Jul 15 22:51:49 2021 +0200
@@ -0,0 +1,146 @@
+/* Title: src/Tools/jEdit/src/main.scala
+ Author: Makarius
+
+Main Isabelle application entry point.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import org.gjt.sp.jedit.{MiscUtilities, jEdit}
+
+
+object Main
+{
+ /* main entry point */
+
+ def main(args: Array[String]): Unit =
+ {
+ if (args.nonEmpty && args(0) == "-init") {
+ Isabelle_System.init()
+ }
+ else {
+ val start =
+ {
+ try {
+ Isabelle_System.init()
+ Isabelle_Fonts.init()
+
+ GUI.init_lafs()
+
+
+ /* ROOTS template */
+
+ {
+ val roots = Path.explode("$ISABELLE_HOME_USER/ROOTS")
+ if (!roots.is_file) File.write(roots, """# Additional session root directories
+#
+# * each line contains one directory entry in Isabelle path notation, e.g.
+#
+# $ISABELLE_HOME/../AFP/thys
+#
+# for a copy of AFP put side-by-side to the Isabelle distribution
+#
+# * Isabelle/jEdit provides formal markup for C-hover-click and completion
+#
+# * lines starting with "#" are stripped
+#
+# * changes require restart of the Isabelle application
+#
+#:mode=text:encoding=UTF-8:
+
+#$ISABELLE_HOME/../AFP/thys
+""")
+ }
+
+
+ /* settings directory */
+
+ val settings_dir = Path.explode("$JEDIT_SETTINGS")
+
+ val properties = settings_dir + Path.explode("properties")
+ if (properties.is_file) {
+ val props1 = split_lines(File.read(properties))
+ val props2 = props1.filterNot(_.startsWith("plugin-blacklist.isabelle_jedit"))
+ if (props1 != props2) File.write(properties, cat_lines(props2))
+ }
+
+ Isabelle_System.make_directory(settings_dir + Path.explode("DockableWindowManager"))
+
+ if (!(settings_dir + Path.explode("perspective.xml")).is_file) {
+ File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"),
+ """<DOCKING LEFT="isabelle-documentation" TOP="" RIGHT="isabelle-theories" BOTTOM="" LEFT_POS="250" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />""")
+ File.write(settings_dir + Path.explode("perspective.xml"),
+ XML.header +
+"""<!DOCTYPE PERSPECTIVE SYSTEM "perspective.dtd">
+<PERSPECTIVE>
+<VIEW PLAIN="FALSE">
+<GEOMETRY X="0" Y="35" WIDTH="1200" HEIGHT="850" EXT_STATE="0" />
+</VIEW>
+</PERSPECTIVE>""")
+ }
+
+ for (plugin <- List("jedit_base", "jedit_main")) {
+ val dir = Path.explode("$ISABELLE_HOME/src/Tools/jEdit") + Path.basic(plugin)
+ val context = isabelle.setup.Build.directory_context(dir.java_path)
+ isabelle.setup.Build.build(context, false)
+ }
+
+
+ /* args */
+
+ val jedit_settings =
+ "-settings=" + File.platform_path(Path.explode("$JEDIT_SETTINGS"))
+
+ val jedit_server =
+ System.getProperty("isabelle.jedit_server") match {
+ case null | "" => "-noserver"
+ case name => "-server=" + name
+ }
+
+ val jedit_options =
+ Isabelle_System.getenv_strict("JEDIT_OPTIONS").split(" +")
+
+ val more_args =
+ {
+ args.toList.dropWhile(arg => arg.startsWith("-") && arg != "--") match {
+ case Nil | List("--") =>
+ args ++ Array(File.platform_path(Path.explode("$USER_HOME/Scratch.thy")))
+ case List(":") => args.slice(0, args.size - 1)
+ case _ => args
+ }
+ }
+
+
+ /* environment */
+
+ for (name <- List("ISABELLE_HOME", "ISABELLE_HOME_USER", "JEDIT_HOME", "JEDIT_SETTINGS")) {
+ MiscUtilities.putenv(name, File.platform_path(Isabelle_System.getenv(name)))
+ }
+ MiscUtilities.putenv("ISABELLE_ROOT", null)
+
+
+ /* properties */
+
+ System.setProperty("jedit.home", File.platform_path(Path.explode("$JEDIT_HOME")))
+ System.setProperty("scala.home", File.platform_path(Path.explode("$SCALA_HOME")))
+ System.setProperty("scala.color", "false")
+
+
+ /* main startup */
+
+ () => jEdit.main(Array(jedit_settings, jedit_server) ++ jedit_options ++ more_args)
+ }
+ catch {
+ case exn: Throwable =>
+ GUI.init_laf()
+ GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
+ sys.exit(2)
+ }
+ }
+ start()
+ }
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/main_plugin.scala Thu Jul 15 22:51:49 2021 +0200
@@ -0,0 +1,501 @@
+/* Title: Tools/jEdit/src/main_plugin.scala
+ Author: Makarius
+
+Main plumbing for PIDE infrastructure as jEdit plugin.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import javax.swing.JOptionPane
+
+import java.io.{File => JFile}
+
+import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, PerspectiveManager}
+import org.gjt.sp.jedit.textarea.JEditTextArea
+import org.gjt.sp.jedit.syntax.ModeProvider
+import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged,
+ ViewUpdate}
+import org.gjt.sp.util.SyntaxUtilities
+import org.gjt.sp.util.Log
+
+
+object PIDE
+{
+ /* semantic document content */
+
+ def maybe_snapshot(view: View = null): Option[Document.Snapshot] = GUI_Thread.now
+ {
+ val buffer = JEdit_Lib.jedit_view(view).getBuffer
+ Document_Model.get(buffer).map(_.snapshot())
+ }
+
+ def maybe_rendering(view: View = null): Option[JEdit_Rendering] = GUI_Thread.now
+ {
+ val text_area = JEdit_Lib.jedit_view(view).getTextArea
+ Document_View.get(text_area).map(_.get_rendering())
+ }
+
+ def snapshot(view: View = null): Document.Snapshot =
+ maybe_snapshot(view) getOrElse error("No document model for current buffer")
+
+ def rendering(view: View = null): JEdit_Rendering =
+ maybe_rendering(view) getOrElse error("No document view for current text area")
+
+
+ /* plugin instance */
+
+ @volatile var _plugin: Main_Plugin = null
+
+ def plugin: Main_Plugin =
+ if (_plugin == null) error("Uninitialized Isabelle/jEdit plugin")
+ else _plugin
+
+ def options: JEdit_Options = plugin.options
+ def resources: JEdit_Resources = plugin.resources
+ def session: Session = plugin.session
+
+ object editor extends JEdit_Editor
+}
+
+class Main_Plugin extends EBPlugin
+{
+ /* options */
+
+ private var _options: JEdit_Options = null
+ private def init_options(): Unit =
+ _options = new JEdit_Options(Options.init())
+ def options: JEdit_Options = _options
+
+
+ /* resources */
+
+ private var _resources: JEdit_Resources = null
+ private def init_resources(): Unit = _resources = JEdit_Resources(options.value)
+ def resources: JEdit_Resources = _resources
+
+
+ /* session */
+
+ private var _session: Session = null
+ private def init_session(): Unit = _session = new Session(options.value, resources)
+ def session: Session = _session
+
+
+ /* misc support */
+
+ val completion_history = new Completion.History_Variable
+ val spell_checker = new Spell_Checker_Variable
+
+
+ /* global changes */
+
+ def options_changed(): Unit =
+ {
+ session.global_options.post(Session.Global_Options(options.value))
+ delay_load.invoke()
+ }
+
+ def deps_changed(): Unit =
+ {
+ delay_load.invoke()
+ }
+
+
+ /* theory files */
+
+ lazy val delay_init =
+ Delay.last(options.seconds("editor_load_delay"), gui = true)
+ {
+ init_models()
+ }
+
+ private val delay_load_active = Synchronized(false)
+ private def delay_load_activated(): Boolean =
+ delay_load_active.guarded_access(a => Some((!a, true)))
+ private def delay_load_action(): Unit =
+ {
+ if (Isabelle.continuous_checking && delay_load_activated() &&
+ PerspectiveManager.isPerspectiveEnabled)
+ {
+ if (JEdit_Lib.jedit_buffers().exists(_.isLoading)) delay_load.invoke()
+ else {
+ val required_files =
+ {
+ val models = Document_Model.get_models()
+
+ val thys =
+ (for ((node_name, model) <- models.iterator if model.is_theory)
+ yield (node_name, Position.none)).toList
+ val thy_files1 = resources.dependencies(thys).theories
+
+ val thy_files2 =
+ (for {
+ (name, _) <- models.iterator
+ thy_name <- resources.make_theory_name(name)
+ } yield thy_name).toList
+
+ val aux_files =
+ if (options.bool("jedit_auto_resolve")) {
+ val stable_tip_version =
+ if (models.forall(p => p._2.is_stable))
+ session.get_state().stable_tip_version
+ else None
+ stable_tip_version match {
+ case Some(version) => resources.undefined_blobs(version.nodes)
+ case None => delay_load.invoke(); Nil
+ }
+ }
+ else Nil
+
+ (thy_files1 ::: thy_files2 ::: aux_files).filterNot(models.isDefinedAt)
+ }
+ if (required_files.nonEmpty) {
+ try {
+ Isabelle_Thread.fork(name = "resolve_dependencies") {
+ val loaded_files =
+ for {
+ name <- required_files
+ text <- resources.read_file_content(name)
+ } yield (name, text)
+
+ GUI_Thread.later {
+ try {
+ Document_Model.provide_files(session, loaded_files)
+ delay_init.invoke()
+ }
+ finally { delay_load_active.change(_ => false) }
+ }
+ }
+ }
+ catch { case _: Throwable => delay_load_active.change(_ => false) }
+ }
+ else delay_load_active.change(_ => false)
+ }
+ }
+ }
+
+ private lazy val delay_load =
+ Delay.last(options.seconds("editor_load_delay"), gui = true) { delay_load_action() }
+
+ private def file_watcher_action(changed: Set[JFile]): Unit =
+ if (Document_Model.sync_files(changed)) PIDE.editor.invoke_generated()
+
+ lazy val file_watcher: File_Watcher =
+ File_Watcher(file_watcher_action, options.seconds("editor_load_delay"))
+
+
+ /* session phase */
+
+ val session_phase_changed: Session.Consumer[Session.Phase] = Session.Consumer("Isabelle/jEdit")
+ {
+ case Session.Terminated(result) if !result.ok =>
+ GUI_Thread.later {
+ GUI.error_dialog(jEdit.getActiveView, "Prover process terminated with error",
+ "Isabelle Syslog", GUI.scrollable_text(session.syslog_content()))
+ }
+
+ case Session.Ready if !shutting_down.value =>
+ init_models()
+
+ if (!Isabelle.continuous_checking) {
+ GUI_Thread.later {
+ val answer =
+ GUI.confirm_dialog(jEdit.getActiveView,
+ "Continuous checking of PIDE document",
+ JOptionPane.YES_NO_OPTION,
+ "Continuous checking is presently disabled:",
+ "editor buffers will remain inactive!",
+ "Enable continuous checking now?")
+ if (answer == 0) Isabelle.continuous_checking = true
+ }
+ }
+
+ delay_load.invoke()
+
+ case Session.Shutdown =>
+ GUI_Thread.later {
+ delay_load.revoke()
+ delay_init.revoke()
+ PIDE.editor.shutdown()
+ exit_models(JEdit_Lib.jedit_buffers().toList)
+ }
+
+ case _ =>
+ }
+
+
+ /* document model and view */
+
+ def exit_models(buffers: List[Buffer]): Unit =
+ {
+ GUI_Thread.now {
+ buffers.foreach(buffer =>
+ JEdit_Lib.buffer_lock(buffer) {
+ JEdit_Lib.jedit_text_areas(buffer).foreach(Document_View.exit)
+ Document_Model.exit(buffer)
+ })
+ }
+ }
+
+ def init_models(): Unit =
+ {
+ GUI_Thread.now {
+ PIDE.editor.flush()
+
+ for {
+ buffer <- JEdit_Lib.jedit_buffers()
+ if buffer != null && !buffer.getBooleanProperty(Buffer.GZIPPED)
+ } {
+ if (buffer.isLoaded) {
+ JEdit_Lib.buffer_lock(buffer) {
+ val node_name = resources.node_name(buffer)
+ val model = Document_Model.init(session, node_name, buffer)
+ for {
+ text_area <- JEdit_Lib.jedit_text_areas(buffer)
+ if Document_View.get(text_area).map(_.model) != Some(model)
+ } Document_View.init(model, text_area)
+ }
+ }
+ else delay_init.invoke()
+ }
+
+ PIDE.editor.invoke_generated()
+ }
+ }
+
+ def init_view(buffer: Buffer, text_area: JEditTextArea): Unit =
+ GUI_Thread.now {
+ JEdit_Lib.buffer_lock(buffer) {
+ Document_Model.get(buffer) match {
+ case Some(model) => Document_View.init(model, text_area)
+ case None =>
+ }
+ }
+ }
+
+ def exit_view(buffer: Buffer, text_area: JEditTextArea): Unit =
+ GUI_Thread.now {
+ JEdit_Lib.buffer_lock(buffer) {
+ Document_View.exit(text_area)
+ }
+ }
+
+
+ /* main plugin plumbing */
+
+ @volatile private var startup_failure: Option[Throwable] = None
+ @volatile private var startup_notified = false
+
+ private def init_editor(view: View): Unit =
+ {
+ Keymap_Merge.check_dialog(view)
+ Session_Build.check_dialog(view)
+ }
+
+ private def init_title(view: View): Unit =
+ {
+ val title =
+ proper_string(Isabelle_System.getenv("ISABELLE_IDENTIFIER")).getOrElse("Isabelle") +
+ "/" + PIDE.resources.session_name
+ val marker = "\u200B"
+
+ val old_title = view.getViewConfig.title
+ if (old_title == null || old_title.startsWith(marker)) {
+ view.setUserTitle(marker + title)
+ }
+ }
+
+ override def handleMessage(message: EBMessage): Unit =
+ {
+ GUI_Thread.assert {}
+
+ if (startup_failure.isDefined && !startup_notified) {
+ message match {
+ case msg: EditorStarted =>
+ GUI.error_dialog(null, "Isabelle plugin startup failure",
+ GUI.scrollable_text(Exn.message(startup_failure.get)),
+ "Prover IDE inactive!")
+ startup_notified = true
+ case _ =>
+ }
+ }
+
+ if (startup_failure.isEmpty) {
+ message match {
+ case msg: EditorStarted =>
+ if (resources.session_errors.nonEmpty) {
+ GUI.warning_dialog(jEdit.getActiveView,
+ "Bad session structure: may cause problems with theory imports",
+ GUI.scrollable_text(cat_lines(resources.session_errors)))
+ }
+
+ jEdit.propertiesChanged()
+
+ val view = jEdit.getActiveView()
+ init_editor(view)
+
+ PIDE.editor.hyperlink_position(true, Document.Snapshot.init,
+ JEdit_Sessions.logic_root(options.value)).foreach(_.follow(view))
+
+ case msg: ViewUpdate
+ if msg.getWhat == ViewUpdate.CREATED && msg.getView != null =>
+ init_title(msg.getView)
+
+ case msg: BufferUpdate
+ if msg.getWhat == BufferUpdate.LOAD_STARTED || msg.getWhat == BufferUpdate.CLOSING =>
+ if (msg.getBuffer != null) {
+ exit_models(List(msg.getBuffer))
+ PIDE.editor.invoke_generated()
+ }
+
+ case msg: BufferUpdate
+ if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED || msg.getWhat == BufferUpdate.LOADED =>
+ if (session.is_ready) {
+ delay_init.invoke()
+ delay_load.invoke()
+ }
+
+ case msg: EditPaneUpdate
+ if msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
+ msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
+ msg.getWhat == EditPaneUpdate.CREATED ||
+ msg.getWhat == EditPaneUpdate.DESTROYED =>
+ val edit_pane = msg.getEditPane
+ val buffer = edit_pane.getBuffer
+ val text_area = edit_pane.getTextArea
+
+ if (buffer != null && text_area != null) {
+ if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
+ msg.getWhat == EditPaneUpdate.CREATED) {
+ if (session.is_ready)
+ init_view(buffer, text_area)
+ }
+ else {
+ Isabelle.dismissed_popups(text_area.getView)
+ exit_view(buffer, text_area)
+ }
+
+ if (msg.getWhat == EditPaneUpdate.CREATED)
+ Completion_Popup.Text_Area.init(text_area)
+
+ if (msg.getWhat == EditPaneUpdate.DESTROYED)
+ Completion_Popup.Text_Area.exit(text_area)
+ }
+
+ case msg: PropertiesChanged =>
+ for {
+ view <- JEdit_Lib.jedit_views()
+ edit_pane <- JEdit_Lib.jedit_edit_panes(view)
+ } {
+ val buffer = edit_pane.getBuffer
+ val text_area = edit_pane.getTextArea
+ if (buffer != null && text_area != null) init_view(buffer, text_area)
+ }
+
+ spell_checker.update(options.value)
+ session.update_options(options.value)
+
+ case _ =>
+ }
+ }
+ }
+
+
+ /* mode provider */
+
+ private var orig_mode_provider: ModeProvider = null
+ private var pide_mode_provider: ModeProvider = null
+
+ def init_mode_provider(): Unit =
+ {
+ orig_mode_provider = ModeProvider.instance
+ if (orig_mode_provider.isInstanceOf[ModeProvider]) {
+ pide_mode_provider = new Token_Markup.Mode_Provider(orig_mode_provider)
+ ModeProvider.instance = pide_mode_provider
+ }
+ }
+
+ def exit_mode_provider(): Unit =
+ {
+ if (ModeProvider.instance == pide_mode_provider)
+ ModeProvider.instance = orig_mode_provider
+ }
+
+
+ /* HTTP server */
+
+ val http_root: String = "/" + UUID.random()
+
+ val http_server: HTTP.Server = HTTP.server(Document_Model.http_handlers(http_root))
+
+
+ /* start and stop */
+
+ private val shutting_down = Synchronized(false)
+
+ override def start(): Unit =
+ {
+ /* strict initialization */
+
+ init_options()
+ init_resources()
+ init_session()
+ PIDE._plugin = this
+
+
+ /* non-strict initialization */
+
+ try {
+ completion_history.load()
+ spell_checker.update(options.value)
+
+ JEdit_Lib.jedit_views().foreach(init_title)
+
+ Syntax_Style.set_extender(Syntax_Style.Main_Extender)
+ init_mode_provider()
+ JEdit_Lib.jedit_text_areas().foreach(Completion_Popup.Text_Area.init)
+
+ http_server.start()
+
+ startup_failure = None
+ }
+ catch {
+ case exn: Throwable =>
+ startup_failure = Some(exn)
+ startup_notified = false
+ Log.log(Log.ERROR, this, exn)
+ }
+
+ shutting_down.change(_ => false)
+
+ val view = jEdit.getActiveView()
+ if (view != null) init_editor(view)
+ }
+
+ override def stop(): Unit =
+ {
+ http_server.stop()
+
+ Syntax_Style.set_extender(Syntax_Style.Base_Extender)
+
+ exit_mode_provider()
+ JEdit_Lib.jedit_text_areas().foreach(Completion_Popup.Text_Area.exit)
+
+ if (startup_failure.isEmpty) {
+ options.value.save_prefs()
+ completion_history.value.save()
+ }
+
+ exit_models(JEdit_Lib.jedit_buffers().toList)
+
+ shutting_down.change(_ => true)
+ session.stop()
+ file_watcher.shutdown()
+ PIDE.editor.shutdown()
+
+ Document_Model.reset()
+ }
+}
--- a/src/Tools/jEdit/src/monitor_dockable.scala Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Tools/jEdit/src/monitor_dockable.scala Thu Jul 15 22:51:49 2021 +0200
@@ -8,7 +8,6 @@
import isabelle._
-import isabelle.jedit_base.Dockable
import java.awt.BorderLayout
--- a/src/Tools/jEdit/src/output_dockable.scala Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Thu Jul 15 22:51:49 2021 +0200
@@ -8,7 +8,6 @@
import isabelle._
-import isabelle.jedit_base.Dockable
import scala.swing.{Button, CheckBox}
import scala.swing.event.ButtonClicked
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/pide_docking_framework.scala Thu Jul 15 22:51:49 2021 +0200
@@ -0,0 +1,72 @@
+/* Title: Tools/jEdit/src/pide_docking_framework.scala
+ Author: Makarius
+
+PIDE docking framework: "Original" with some add-ons.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.util.{List => JList}
+import java.awt.event.{ActionListener, ActionEvent}
+import javax.swing.{JPopupMenu, JMenuItem}
+
+import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.gui.{DockableWindowManagerProvider, DockableWindowFactory,
+ DockableWindowManager, DockableWindowManagerImpl, DockableWindowContainer,
+ FloatingWindowContainer, PanelWindowContainer}
+
+
+class PIDE_Docking_Framework extends DockableWindowManagerProvider
+{
+ override def create(
+ view: View,
+ instance: DockableWindowFactory,
+ config: View.ViewConfig): DockableWindowManager =
+ new DockableWindowManagerImpl(view, instance, config)
+ {
+ override def createPopupMenu(
+ container: DockableWindowContainer,
+ dockable_name: String,
+ clone: Boolean): JPopupMenu =
+ {
+ val menu = super.createPopupMenu(container, dockable_name, clone)
+
+ val detach_operation: Option[() => Unit] =
+ container match {
+ case floating: FloatingWindowContainer =>
+ Untyped.get[AnyRef](Untyped.get[AnyRef](floating, "entry"), "win") match {
+ case dockable: Dockable => dockable.detach_operation
+ case _ => None
+ }
+
+ case panel: PanelWindowContainer =>
+ val entries = Untyped.get[JList[AnyRef]](panel, "dockables").toArray
+ val wins =
+ (for {
+ entry <- entries.iterator
+ if Untyped.get[String](Untyped.get(entry, "factory"), "name") == dockable_name
+ win = Untyped.get[Any](entry, "win")
+ if win != null
+ } yield win).toList
+ wins match {
+ case List(dockable: Dockable) => dockable.detach_operation
+ case _ => None
+ }
+
+ case _ => None
+ }
+ if (detach_operation.isDefined) {
+ val detach_item = new JMenuItem("Detach")
+ detach_item.addActionListener(new ActionListener {
+ def actionPerformed(evt: ActionEvent): Unit = detach_operation.get.apply()
+ })
+ menu.add(detach_item)
+ }
+
+ menu
+ }
+ }
+}
--- a/src/Tools/jEdit/src/plugin.scala Thu Jul 15 16:11:52 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,499 +0,0 @@
-/* Title: Tools/jEdit/src/plugin.scala
- Author: Makarius
-
-Main plumbing for PIDE infrastructure as jEdit plugin.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-import javax.swing.JOptionPane
-
-import java.io.{File => JFile}
-
-import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, PerspectiveManager}
-import org.gjt.sp.jedit.textarea.JEditTextArea
-import org.gjt.sp.jedit.syntax.ModeProvider
-import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged,
- ViewUpdate}
-import org.gjt.sp.util.SyntaxUtilities
-import org.gjt.sp.util.Log
-
-
-object PIDE
-{
- /* semantic document content */
-
- def maybe_snapshot(view: View = null): Option[Document.Snapshot] = GUI_Thread.now
- {
- val buffer = JEdit_Lib.jedit_view(view).getBuffer
- Document_Model.get(buffer).map(_.snapshot())
- }
-
- def maybe_rendering(view: View = null): Option[JEdit_Rendering] = GUI_Thread.now
- {
- val text_area = JEdit_Lib.jedit_view(view).getTextArea
- Document_View.get(text_area).map(_.get_rendering())
- }
-
- def snapshot(view: View = null): Document.Snapshot =
- maybe_snapshot(view) getOrElse error("No document model for current buffer")
-
- def rendering(view: View = null): JEdit_Rendering =
- maybe_rendering(view) getOrElse error("No document view for current text area")
-
-
- /* plugin instance */
-
- @volatile var _plugin: Plugin = null
-
- def plugin: Plugin =
- if (_plugin == null) error("Uninitialized Isabelle/jEdit plugin")
- else _plugin
-
- def options: JEdit_Options = plugin.options
- def resources: JEdit_Resources = plugin.resources
- def session: Session = plugin.session
-
- object editor extends JEdit_Editor
-}
-
-class Plugin extends EBPlugin
-{
- /* options */
-
- private var _options: JEdit_Options = null
- private def init_options(): Unit =
- _options = new JEdit_Options(Options.init())
- def options: JEdit_Options = _options
-
-
- /* resources */
-
- private var _resources: JEdit_Resources = null
- private def init_resources(): Unit = _resources = JEdit_Resources(options.value)
- def resources: JEdit_Resources = _resources
-
-
- /* session */
-
- private var _session: Session = null
- private def init_session(): Unit = _session = new Session(options.value, resources)
- def session: Session = _session
-
-
- /* misc support */
-
- val completion_history = new Completion.History_Variable
- val spell_checker = new Spell_Checker_Variable
-
-
- /* global changes */
-
- def options_changed(): Unit =
- {
- session.global_options.post(Session.Global_Options(options.value))
- delay_load.invoke()
- }
-
- def deps_changed(): Unit =
- {
- delay_load.invoke()
- }
-
-
- /* theory files */
-
- lazy val delay_init =
- Delay.last(options.seconds("editor_load_delay"), gui = true)
- {
- init_models()
- }
-
- private val delay_load_active = Synchronized(false)
- private def delay_load_activated(): Boolean =
- delay_load_active.guarded_access(a => Some((!a, true)))
- private def delay_load_action(): Unit =
- {
- if (Isabelle.continuous_checking && delay_load_activated() &&
- PerspectiveManager.isPerspectiveEnabled)
- {
- if (JEdit_Lib.jedit_buffers().exists(_.isLoading)) delay_load.invoke()
- else {
- val required_files =
- {
- val models = Document_Model.get_models()
-
- val thys =
- (for ((node_name, model) <- models.iterator if model.is_theory)
- yield (node_name, Position.none)).toList
- val thy_files1 = resources.dependencies(thys).theories
-
- val thy_files2 =
- (for {
- (name, _) <- models.iterator
- thy_name <- resources.make_theory_name(name)
- } yield thy_name).toList
-
- val aux_files =
- if (options.bool("jedit_auto_resolve")) {
- val stable_tip_version =
- if (models.forall(p => p._2.is_stable))
- session.get_state().stable_tip_version
- else None
- stable_tip_version match {
- case Some(version) => resources.undefined_blobs(version.nodes)
- case None => delay_load.invoke(); Nil
- }
- }
- else Nil
-
- (thy_files1 ::: thy_files2 ::: aux_files).filterNot(models.isDefinedAt)
- }
- if (required_files.nonEmpty) {
- try {
- Isabelle_Thread.fork(name = "resolve_dependencies") {
- val loaded_files =
- for {
- name <- required_files
- text <- resources.read_file_content(name)
- } yield (name, text)
-
- GUI_Thread.later {
- try {
- Document_Model.provide_files(session, loaded_files)
- delay_init.invoke()
- }
- finally { delay_load_active.change(_ => false) }
- }
- }
- }
- catch { case _: Throwable => delay_load_active.change(_ => false) }
- }
- else delay_load_active.change(_ => false)
- }
- }
- }
-
- private lazy val delay_load =
- Delay.last(options.seconds("editor_load_delay"), gui = true) { delay_load_action() }
-
- private def file_watcher_action(changed: Set[JFile]): Unit =
- if (Document_Model.sync_files(changed)) PIDE.editor.invoke_generated()
-
- lazy val file_watcher: File_Watcher =
- File_Watcher(file_watcher_action, options.seconds("editor_load_delay"))
-
-
- /* session phase */
-
- val session_phase_changed: Session.Consumer[Session.Phase] = Session.Consumer("Isabelle/jEdit")
- {
- case Session.Terminated(result) if !result.ok =>
- GUI_Thread.later {
- GUI.error_dialog(jEdit.getActiveView, "Prover process terminated with error",
- "Isabelle Syslog", GUI.scrollable_text(session.syslog_content()))
- }
-
- case Session.Ready if !shutting_down.value =>
- init_models()
-
- if (!Isabelle.continuous_checking) {
- GUI_Thread.later {
- val answer =
- GUI.confirm_dialog(jEdit.getActiveView,
- "Continuous checking of PIDE document",
- JOptionPane.YES_NO_OPTION,
- "Continuous checking is presently disabled:",
- "editor buffers will remain inactive!",
- "Enable continuous checking now?")
- if (answer == 0) Isabelle.continuous_checking = true
- }
- }
-
- delay_load.invoke()
-
- case Session.Shutdown =>
- GUI_Thread.later {
- delay_load.revoke()
- delay_init.revoke()
- PIDE.editor.shutdown()
- exit_models(JEdit_Lib.jedit_buffers().toList)
- }
-
- case _ =>
- }
-
-
- /* document model and view */
-
- def exit_models(buffers: List[Buffer]): Unit =
- {
- GUI_Thread.now {
- buffers.foreach(buffer =>
- JEdit_Lib.buffer_lock(buffer) {
- JEdit_Lib.jedit_text_areas(buffer).foreach(Document_View.exit)
- Document_Model.exit(buffer)
- })
- }
- }
-
- def init_models(): Unit =
- {
- GUI_Thread.now {
- PIDE.editor.flush()
-
- for {
- buffer <- JEdit_Lib.jedit_buffers()
- if buffer != null && !buffer.getBooleanProperty(Buffer.GZIPPED)
- } {
- if (buffer.isLoaded) {
- JEdit_Lib.buffer_lock(buffer) {
- val node_name = resources.node_name(buffer)
- val model = Document_Model.init(session, node_name, buffer)
- for {
- text_area <- JEdit_Lib.jedit_text_areas(buffer)
- if Document_View.get(text_area).map(_.model) != Some(model)
- } Document_View.init(model, text_area)
- }
- }
- else delay_init.invoke()
- }
-
- PIDE.editor.invoke_generated()
- }
- }
-
- def init_view(buffer: Buffer, text_area: JEditTextArea): Unit =
- GUI_Thread.now {
- JEdit_Lib.buffer_lock(buffer) {
- Document_Model.get(buffer) match {
- case Some(model) => Document_View.init(model, text_area)
- case None =>
- }
- }
- }
-
- def exit_view(buffer: Buffer, text_area: JEditTextArea): Unit =
- GUI_Thread.now {
- JEdit_Lib.buffer_lock(buffer) {
- Document_View.exit(text_area)
- }
- }
-
-
- /* main plugin plumbing */
-
- @volatile private var startup_failure: Option[Throwable] = None
- @volatile private var startup_notified = false
-
- private def init_editor(view: View): Unit =
- {
- Keymap_Merge.check_dialog(view)
- Session_Build.check_dialog(view)
- }
-
- private def init_title(view: View): Unit =
- {
- val title =
- proper_string(Isabelle_System.getenv("ISABELLE_IDENTIFIER")).getOrElse("Isabelle") +
- "/" + PIDE.resources.session_name
- val marker = "\u200B"
-
- val old_title = view.getViewConfig.title
- if (old_title == null || old_title.startsWith(marker)) {
- view.setUserTitle(marker + title)
- }
- }
-
- override def handleMessage(message: EBMessage): Unit =
- {
- GUI_Thread.assert {}
-
- if (startup_failure.isDefined && !startup_notified) {
- message match {
- case msg: EditorStarted =>
- GUI.error_dialog(null, "Isabelle plugin startup failure",
- GUI.scrollable_text(Exn.message(startup_failure.get)),
- "Prover IDE inactive!")
- startup_notified = true
- case _ =>
- }
- }
-
- if (startup_failure.isEmpty) {
- message match {
- case msg: EditorStarted =>
- if (resources.session_errors.nonEmpty) {
- GUI.warning_dialog(jEdit.getActiveView,
- "Bad session structure: may cause problems with theory imports",
- GUI.scrollable_text(cat_lines(resources.session_errors)))
- }
-
- jEdit.propertiesChanged()
-
- val view = jEdit.getActiveView()
- init_editor(view)
-
- PIDE.editor.hyperlink_position(true, Document.Snapshot.init,
- JEdit_Sessions.logic_root(options.value)).foreach(_.follow(view))
-
- case msg: ViewUpdate
- if msg.getWhat == ViewUpdate.CREATED && msg.getView != null =>
- init_title(msg.getView)
-
- case msg: BufferUpdate
- if msg.getWhat == BufferUpdate.LOAD_STARTED || msg.getWhat == BufferUpdate.CLOSING =>
- if (msg.getBuffer != null) {
- exit_models(List(msg.getBuffer))
- PIDE.editor.invoke_generated()
- }
-
- case msg: BufferUpdate
- if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED || msg.getWhat == BufferUpdate.LOADED =>
- if (session.is_ready) {
- delay_init.invoke()
- delay_load.invoke()
- }
-
- case msg: EditPaneUpdate
- if msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
- msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
- msg.getWhat == EditPaneUpdate.CREATED ||
- msg.getWhat == EditPaneUpdate.DESTROYED =>
- val edit_pane = msg.getEditPane
- val buffer = edit_pane.getBuffer
- val text_area = edit_pane.getTextArea
-
- if (buffer != null && text_area != null) {
- if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
- msg.getWhat == EditPaneUpdate.CREATED) {
- if (session.is_ready)
- init_view(buffer, text_area)
- }
- else {
- Isabelle.dismissed_popups(text_area.getView)
- exit_view(buffer, text_area)
- }
-
- if (msg.getWhat == EditPaneUpdate.CREATED)
- Completion_Popup.Text_Area.init(text_area)
-
- if (msg.getWhat == EditPaneUpdate.DESTROYED)
- Completion_Popup.Text_Area.exit(text_area)
- }
-
- case msg: PropertiesChanged =>
- for {
- view <- JEdit_Lib.jedit_views()
- edit_pane <- JEdit_Lib.jedit_edit_panes(view)
- } {
- val buffer = edit_pane.getBuffer
- val text_area = edit_pane.getTextArea
- if (buffer != null && text_area != null) init_view(buffer, text_area)
- }
-
- spell_checker.update(options.value)
- session.update_options(options.value)
-
- case _ =>
- }
- }
- }
-
-
- /* mode provider */
-
- private var orig_mode_provider: ModeProvider = null
- private var pide_mode_provider: ModeProvider = null
-
- def init_mode_provider(): Unit =
- {
- orig_mode_provider = ModeProvider.instance
- if (orig_mode_provider.isInstanceOf[ModeProvider]) {
- pide_mode_provider = new Token_Markup.Mode_Provider(orig_mode_provider)
- ModeProvider.instance = pide_mode_provider
- }
- }
-
- def exit_mode_provider(): Unit =
- {
- if (ModeProvider.instance == pide_mode_provider)
- ModeProvider.instance = orig_mode_provider
- }
-
-
- /* HTTP server */
-
- val http_root: String = "/" + UUID.random()
-
- val http_server: HTTP.Server = HTTP.server(Document_Model.http_handlers(http_root))
-
-
- /* start and stop */
-
- private val shutting_down = Synchronized(false)
-
- override def start(): Unit =
- {
- /* strict initialization */
-
- init_options()
- init_resources()
- init_session()
- PIDE._plugin = this
-
-
- /* non-strict initialization */
-
- try {
- completion_history.load()
- spell_checker.update(options.value)
-
- JEdit_Lib.jedit_views().foreach(init_title)
-
- isabelle.jedit_base.Syntax_Style.set_style_extender(Syntax_Style.Extender)
- init_mode_provider()
- JEdit_Lib.jedit_text_areas().foreach(Completion_Popup.Text_Area.init)
-
- http_server.start()
-
- startup_failure = None
- }
- catch {
- case exn: Throwable =>
- startup_failure = Some(exn)
- startup_notified = false
- Log.log(Log.ERROR, this, exn)
- }
-
- shutting_down.change(_ => false)
-
- val view = jEdit.getActiveView()
- if (view != null) init_editor(view)
- }
-
- override def stop(): Unit =
- {
- http_server.stop()
-
- isabelle.jedit_base.Syntax_Style.dummy_style_extender()
- exit_mode_provider()
- JEdit_Lib.jedit_text_areas().foreach(Completion_Popup.Text_Area.exit)
-
- if (startup_failure.isEmpty) {
- options.value.save_prefs()
- completion_history.value.save()
- }
-
- exit_models(JEdit_Lib.jedit_buffers().toList)
-
- shutting_down.change(_ => true)
- session.stop()
- file_watcher.shutdown()
- PIDE.editor.shutdown()
- }
-}
-
--- a/src/Tools/jEdit/src/protocol_dockable.scala Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Tools/jEdit/src/protocol_dockable.scala Thu Jul 15 22:51:49 2021 +0200
@@ -8,7 +8,6 @@
import isabelle._
-import isabelle.jedit_base.Dockable
import java.awt.BorderLayout
--- a/src/Tools/jEdit/src/query_dockable.scala Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala Thu Jul 15 22:51:49 2021 +0200
@@ -8,7 +8,6 @@
import isabelle._
-import isabelle.jedit_base.Dockable
import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
import javax.swing.{JComponent, JTextField}
--- a/src/Tools/jEdit/src/raw_output_dockable.scala Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala Thu Jul 15 22:51:49 2021 +0200
@@ -8,7 +8,6 @@
import isabelle._
-import isabelle.jedit_base.Dockable
import scala.swing.{TextArea, ScrollPane}
--- a/src/Tools/jEdit/src/scala_console.scala Thu Jul 15 16:11:52 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,181 +0,0 @@
-/* Title: Tools/jEdit/src/scala_console.scala
- Author: Makarius
-
-Scala instance of Console plugin.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-import console.{Console, ConsolePane, Shell, Output}
-import org.gjt.sp.jedit.JARClassLoader
-import java.io.{OutputStream, Writer, PrintWriter}
-
-
-class Scala_Console extends Shell("Scala")
-{
- /* global state -- owned by GUI thread */
-
- @volatile private var interpreters = Map.empty[Console, Interpreter]
-
- @volatile private var global_console: Console = null
- @volatile private var global_out: Output = null
- @volatile private var global_err: Output = null
-
- private val console_stream = new OutputStream
- {
- val buf = new StringBuilder(100)
-
- override def flush(): Unit =
- {
- val s = buf.synchronized { val s = buf.toString; buf.clear(); s }
- val str = UTF8.decode_permissive(s)
- GUI_Thread.later {
- if (global_out == null) System.out.print(str)
- else global_out.writeAttrs(null, str)
- }
- Time.seconds(0.01).sleep() // FIXME adhoc delay to avoid loosing output
- }
-
- override def close(): Unit = flush()
-
- def write(byte: Int): Unit =
- {
- val c = byte.toChar
- buf.synchronized { buf.append(c) }
- if (c == '\n') flush()
- }
- }
-
- private val console_writer = new Writer
- {
- def flush(): Unit = console_stream.flush()
- def close(): Unit = console_stream.flush()
-
- def write(cbuf: Array[Char], off: Int, len: Int): Unit =
- {
- if (len > 0) {
- UTF8.bytes(new String(cbuf.slice(off, off + len))).foreach(console_stream.write(_))
- }
- }
- }
-
- private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A =
- {
- global_console = console
- global_out = out
- global_err = if (err == null) out else err
- try {
- scala.Console.withErr(console_stream) {
- scala.Console.withOut(console_stream) { e }
- }
- }
- finally {
- console_stream.flush
- global_console = null
- global_out = null
- global_err = null
- }
- }
-
- private def report_error(str: String): Unit =
- {
- if (global_console == null || global_err == null) isabelle.Output.writeln(str)
- else GUI_Thread.later { global_err.print(global_console.getErrorColor, str) }
- }
-
-
- /* interpreter thread */
-
- private abstract class Request
- private case class Start(console: Console) extends Request
- private case class Execute(console: Console, out: Output, err: Output, command: String)
- extends Request
-
- private class Interpreter
- {
- private val running = Synchronized[Option[Thread]](None)
- def interrupt(): Unit = running.change(opt => { opt.foreach(_.interrupt()); opt })
-
- private val interp =
- Scala.Compiler.context(error = report_error, jar_dirs = JEdit_Lib.directories).
- interpreter(
- print_writer = new PrintWriter(console_writer, true),
- class_loader = new JARClassLoader)
-
- val thread: Consumer_Thread[Request] = Consumer_Thread.fork("Scala_Console")
- {
- case Start(console) =>
- interp.bind("view", "org.gjt.sp.jedit.View", console.getView)
- interp.bind("console", "console.Console", console)
- interp.interpret("import isabelle._; import isabelle.jedit._")
- true
-
- case Execute(console, out, err, command) =>
- with_console(console, out, err) {
- try {
- running.change(_ => Some(Thread.currentThread()))
- interp.interpret(command)
- }
- finally {
- running.change(_ => None)
- Exn.Interrupt.dispose()
- }
- GUI_Thread.later {
- if (err != null) err.commandDone()
- out.commandDone()
- }
- true
- }
- }
- }
-
-
- /* jEdit console methods */
-
- override def openConsole(console: Console): Unit =
- {
- val interp = new Interpreter
- interp.thread.send(Start(console))
- interpreters += (console -> interp)
- }
-
- override def closeConsole(console: Console): Unit =
- {
- interpreters.get(console) match {
- case Some(interp) =>
- interp.interrupt()
- interp.thread.shutdown()
- interpreters -= console
- case None =>
- }
- }
-
- override def printInfoMessage(out: Output): Unit =
- {
- out.print(null,
- "This shell evaluates Isabelle/Scala expressions.\n\n" +
- "The contents of package isabelle and isabelle.jedit are imported.\n" +
- "The following special toplevel bindings are provided:\n" +
- " view -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" +
- " console -- jEdit Console plugin\n" +
- " PIDE -- Isabelle/PIDE plugin (e.g. PIDE.session, PIDE.snapshot, PIDE.rendering)\n")
- }
-
- override def printPrompt(console: Console, out: Output): Unit =
- {
- out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>")
- out.writeAttrs(ConsolePane.colorAttributes(console.getPlainColor), " ")
- }
-
- override def execute(
- console: Console, input: String, out: Output, err: Output, command: String): Unit =
- {
- interpreters(console).thread.send(Execute(console, out, err, command))
- }
-
- override def stop(console: Console): Unit =
- interpreters.get(console).foreach(_.interrupt())
-}
--- a/src/Tools/jEdit/src/services.xml Thu Jul 15 16:11:52 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,59 +0,0 @@
-<?xml version="1.0"?>
-<!DOCTYPE SERVICES SYSTEM "services.dtd">
-
-<SERVICES>
- <SERVICE CLASS="org.gjt.sp.jedit.buffer.FoldHandler" NAME="isabelle">
- new isabelle.jedit.Fold_Handling.Fold_Handler();
- </SERVICE>
- <SERVICE CLASS="org.gjt.sp.jedit.gui.DynamicContextMenuService" NAME="Spell_Checker">
- new isabelle.jedit.Context_Menu();
- </SERVICE>
- <SERVICE NAME="isabelle-export" CLASS="org.gjt.sp.jedit.io.VFS">
- new isabelle.jedit.Isabelle_Export.VFS();
- </SERVICE>
- <SERVICE NAME="isabelle-session" CLASS="org.gjt.sp.jedit.io.VFS">
- new isabelle.jedit.Isabelle_Session.VFS();
- </SERVICE>
- <SERVICE NAME="isabelle" CLASS="sidekick.SideKickParser">
- new isabelle.jedit.Isabelle_Sidekick_Default();
- </SERVICE>
- <SERVICE NAME="isabelle-context" CLASS="sidekick.SideKickParser">
- new isabelle.jedit.Isabelle_Sidekick_Context();
- </SERVICE>
- <SERVICE NAME="isabelle-markup" CLASS="sidekick.SideKickParser">
- new isabelle.jedit.Isabelle_Sidekick_Markup();
- </SERVICE>
- <SERVICE NAME="isabelle-ml" CLASS="sidekick.SideKickParser">
- new isabelle.jedit.Isabelle_Sidekick_ML();
- </SERVICE>
- <SERVICE NAME="isabelle-sml" CLASS="sidekick.SideKickParser">
- new isabelle.jedit.Isabelle_Sidekick_SML();
- </SERVICE>
- <SERVICE NAME="isabelle-news" CLASS="sidekick.SideKickParser">
- new isabelle.jedit.Isabelle_Sidekick_News();
- </SERVICE>
- <SERVICE NAME="isabelle-options" CLASS="sidekick.SideKickParser">
- new isabelle.jedit.Isabelle_Sidekick_Options();
- </SERVICE>
- <SERVICE NAME="isabelle-root" CLASS="sidekick.SideKickParser">
- new isabelle.jedit.Isabelle_Sidekick_Root();
- </SERVICE>
- <SERVICE NAME="bibtex" CLASS="sidekick.SideKickParser">
- new isabelle.jedit.JEdit_Bibtex.Sidekick_Parser();
- </SERVICE>
- <SERVICE CLASS="console.Shell" NAME="Scala">
- new isabelle.jedit.Scala_Console();
- </SERVICE>
- <SERVICE CLASS="isabelle.jedit.Active$Handler" NAME="misc">
- new isabelle.jedit.Active$Misc_Handler();
- </SERVICE>
- <SERVICE CLASS="isabelle.jedit.Active$Handler" NAME="graphview">
- new isabelle.jedit.Graphview_Dockable$Handler()
- </SERVICE>
- <SERVICE CLASS="org.gjt.sp.jedit.gui.statusbar.StatusWidgetFactory" NAME="java-status">
- new isabelle.jedit.Status_Widget$Java_Factory();
- </SERVICE>
- <SERVICE CLASS="org.gjt.sp.jedit.gui.statusbar.StatusWidgetFactory" NAME="ml-status">
- new isabelle.jedit.Status_Widget$ML_Factory();
- </SERVICE>
-</SERVICES>
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Thu Jul 15 22:51:49 2021 +0200
@@ -8,7 +8,6 @@
import isabelle._
-import isabelle.jedit_base.Dockable
import scala.swing.{Button, CheckBox, Orientation, Separator}
import scala.swing.event.ButtonClicked
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Thu Jul 15 22:51:49 2021 +0200
@@ -8,7 +8,6 @@
import isabelle._
-import isabelle.jedit_base.Dockable
import scala.swing.{Button, Component, Label, CheckBox}
import scala.swing.event.ButtonClicked
--- a/src/Tools/jEdit/src/state_dockable.scala Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Tools/jEdit/src/state_dockable.scala Thu Jul 15 22:51:49 2021 +0200
@@ -8,7 +8,6 @@
import isabelle._
-import isabelle.jedit_base.Dockable
import scala.swing.{Button, CheckBox}
import scala.swing.event.ButtonClicked
--- a/src/Tools/jEdit/src/symbols_dockable.scala Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Tools/jEdit/src/symbols_dockable.scala Thu Jul 15 22:51:49 2021 +0200
@@ -8,7 +8,6 @@
import isabelle._
-import isabelle.jedit_base.Dockable
import scala.swing.event.{SelectionChanged, ValueChanged}
import scala.swing.{Component, Action, Button, TabbedPane, TextField, BorderPanel,
--- a/src/Tools/jEdit/src/syntax_style.scala Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Tools/jEdit/src/syntax_style.scala Thu Jul 15 22:51:49 2021 +0200
@@ -15,6 +15,7 @@
import java.awt.geom.AffineTransform
import org.gjt.sp.util.SyntaxUtilities
+import org.gjt.sp.jedit.jEdit
import org.gjt.sp.jedit.syntax.{Token => JEditToken, SyntaxStyle}
import org.gjt.sp.jedit.textarea.TextArea
@@ -24,6 +25,7 @@
/* extended syntax styles */
private val plain_range: Int = JEditToken.ID_COUNT
+ private val full_range: Int = 6 * plain_range
private def check_range(i: Int): Unit =
require(0 <= i && i < plain_range, "bad syntax style range")
@@ -31,7 +33,7 @@
def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
def bold(i: Byte): Byte = { check_range(i); (i + 3 * plain_range).toByte }
def user_font(idx: Int, i: Byte): Byte = { check_range(i); (i + (4 + idx) * plain_range).toByte }
- val hidden: Byte = (6 * plain_range).toByte
+ val hidden: Byte = full_range.toByte
val control: Byte = (hidden + JEditToken.DIGIT).toByte
private def font_style(style: SyntaxStyle, f: Font => Font): SyntaxStyle =
@@ -61,7 +63,25 @@
val hidden_color: Color = new Color(255, 255, 255, 0)
- object Extender extends SyntaxUtilities.StyleExtender
+ def set_extender(extender: SyntaxUtilities.StyleExtender): Unit =
+ {
+ SyntaxUtilities.setStyleExtender(extender)
+ GUI_Thread.later { jEdit.propertiesChanged }
+ }
+
+ object Base_Extender extends SyntaxUtilities.StyleExtender
+ {
+ override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
+ {
+ val new_styles = Array.fill[SyntaxStyle](java.lang.Byte.MAX_VALUE)(styles(0))
+ for (i <- 0 until full_range) {
+ new_styles(i) = styles(i % plain_range)
+ }
+ new_styles
+ }
+ }
+
+ object Main_Extender extends SyntaxUtilities.StyleExtender
{
val max_user_fonts = 2
if (Symbol.font_names.length > max_user_fonts)
--- a/src/Tools/jEdit/src/syslog_dockable.scala Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Tools/jEdit/src/syslog_dockable.scala Thu Jul 15 22:51:49 2021 +0200
@@ -8,7 +8,6 @@
import isabelle._
-import isabelle.jedit_base.Dockable
import scala.swing.{TextArea, ScrollPane}
--- a/src/Tools/jEdit/src/theories_dockable.scala Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala Thu Jul 15 22:51:49 2021 +0200
@@ -8,7 +8,6 @@
import isabelle._
-import isabelle.jedit_base.Dockable
import scala.swing.{Button, TextArea, Label, ListView, Alignment,
ScrollPane, Component, CheckBox, BorderPanel}
--- a/src/Tools/jEdit/src/timing_dockable.scala Thu Jul 15 16:11:52 2021 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala Thu Jul 15 22:51:49 2021 +0200
@@ -8,7 +8,6 @@
import isabelle._
-import isabelle.jedit_base.Dockable
import scala.swing.{Label, ListView, Alignment, ScrollPane, Component, TextField}
import scala.swing.event.{MouseClicked, ValueChanged}