diff --git a/etc/build.props b/etc/build.props
--- a/etc/build.props
+++ b/etc/build.props
@@ -1,307 +1,308 @@
title = Isabelle/Scala
module = $ISABELLE_HOME/lib/classes/isabelle.jar
main = isabelle.jedit.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_minisat.scala \
src/Pure/Admin/build_pdfjs.scala \
src/Pure/Admin/build_polyml.scala \
src/Pure/Admin/build_release.scala \
src/Pure/Admin/build_scala.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_build_benchmark.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/base64.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/json_api.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/rsync.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/classpath.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/flarum.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_build.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/sync.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_extension.scala \
src/Tools/VSCode/src/build_vscodium.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/vscode_main.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_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_main.scala \
src/Tools/jEdit/src/jedit_options.scala \
src/Tools/jEdit/src/jedit_plugins.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_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.Bash$Handler \
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.jedit.JEdit_Plugin0 \
isabelle.jedit.JEdit_Plugin1 \
isabelle.nitpick.Kodkod$Handler \
isabelle.nitpick.Scala_Functions \
isabelle.spark.SPARK$Load_Command1 \
isabelle.spark.SPARK$Load_Command2
diff --git a/src/Tools/jEdit/jedit_main/dockables.scala b/src/Tools/jEdit/jedit_main/dockables.scala
--- a/src/Tools/jEdit/jedit_main/dockables.scala
+++ b/src/Tools/jEdit/jedit_main/dockables.scala
@@ -1,59 +1,62 @@
/* 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 Document_Dockable(view: View, position: String)
+ extends isabelle.jedit.Document_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)
diff --git a/src/Tools/jEdit/jedit_main/dockables.xml b/src/Tools/jEdit/jedit_main/dockables.xml
--- a/src/Tools/jEdit/jedit_main/dockables.xml
+++ b/src/Tools/jEdit/jedit_main/dockables.xml
@@ -1,53 +1,56 @@
new isabelle.jedit_main.Debugger_Dockable(view, position);
+
+ new isabelle.jedit_main.Document_Dockable(view, position);
+
new isabelle.jedit_main.Documentation_Dockable(view, position);
new isabelle.jedit_main.Info_Dockable(view, position);
new isabelle.jedit_main.Graphview_Dockable(view, position);
new isabelle.jedit_main.Monitor_Dockable(view, position);
new isabelle.jedit_main.Output_Dockable(view, position);
new isabelle.jedit_main.Protocol_Dockable(view, position);
new isabelle.jedit_main.Query_Dockable(view, position);
new isabelle.jedit_main.Raw_Output_Dockable(view, position);
new isabelle.jedit_main.Simplifier_Trace_Dockable(view, position);
new isabelle.jedit_main.Sledgehammer_Dockable(view, position);
new isabelle.jedit_main.State_Dockable(view, position);
new isabelle.jedit_main.Symbols_Dockable(view, position);
new isabelle.jedit_main.Syslog_Dockable(view, position);
new isabelle.jedit_main.Theories_Dockable(view, position);
new isabelle.jedit_main.Timing_Dockable(view, position);
diff --git a/src/Tools/jEdit/jedit_main/plugin.props b/src/Tools/jEdit/jedit_main/plugin.props
--- a/src/Tools/jEdit/jedit_main/plugin.props
+++ b/src/Tools/jEdit/jedit_main/plugin.props
@@ -1,111 +1,114 @@
## 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.3
plugin.isabelle.jedit_main.Plugin.description=Isabelle/jEdit main plugin
#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.06.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.4.0
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-document \
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-document.label=Document panel
+isabelle-document.title=Document
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
diff --git a/src/Tools/jEdit/src/document_dockable.scala b/src/Tools/jEdit/src/document_dockable.scala
new file mode 100644
--- /dev/null
+++ b/src/Tools/jEdit/src/document_dockable.scala
@@ -0,0 +1,92 @@
+/* Title: Tools/jEdit/src/document_dockable.scala
+ Author: Makarius
+
+Dockable window for document build support.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.awt.BorderLayout
+import java.awt.event.{ComponentEvent, ComponentAdapter}
+
+import scala.swing.Button
+import scala.swing.event.ButtonClicked
+
+import org.gjt.sp.jedit.{jEdit, View}
+
+
+class Document_Dockable(view: View, position: String) extends Dockable(view, position) {
+ GUI_Thread.require {}
+
+
+ /* text area */
+
+ val pretty_text_area = new Pretty_Text_Area(view)
+ set_content(pretty_text_area)
+
+ override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
+
+
+ /* document build process */
+
+ private val process_indicator = new Process_Indicator
+
+
+ /* resize */
+
+ private val delay_resize =
+ Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
+
+ addComponentListener(new ComponentAdapter {
+ override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
+ override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
+ })
+
+ private def handle_resize(): Unit =
+ GUI_Thread.require { pretty_text_area.zoom(zoom.factor) }
+
+
+ /* controls */
+
+ private val build_button = new Button("Build") {
+ tooltip = "Build document"
+ reactions += { case ButtonClicked(_) =>
+ pretty_text_area.update(
+ Document.Snapshot.init, Command.Results.empty,
+ List(XML.Text(Date.now().toString))) // FIXME
+ }
+ }
+
+ private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = handle_resize() }
+
+ private val controls =
+ Wrap_Panel(List(process_indicator.component, build_button,
+ pretty_text_area.search_label, pretty_text_area.search_field, zoom))
+
+ add(controls.peer, BorderLayout.NORTH)
+
+ override def focusOnDefaultComponent(): Unit = build_button.requestFocus()
+
+
+ /* main */
+
+ private val main =
+ Session.Consumer[Session.Global_Options](getClass.getName) {
+ case _: Session.Global_Options =>
+ GUI_Thread.later { handle_resize() }
+ }
+
+ override def init(): Unit = {
+ PIDE.session.global_options += main
+ handle_resize()
+ }
+
+ override def exit(): Unit = {
+ PIDE.session.global_options -= main
+ delay_resize.revoke()
+ }
+}
+
diff --git a/src/Tools/jEdit/src/isabelle.scala b/src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala
+++ b/src/Tools/jEdit/src/isabelle.scala
@@ -1,605 +1,611 @@
/* Title: Tools/jEdit/src/isabelle.scala
Author: Makarius
Global configuration and convenience operations for Isabelle/jEdit.
*/
package isabelle.jedit
import isabelle._
import java.awt.{Point, Frame, Rectangle}
import scala.swing.CheckBox
import scala.swing.event.ButtonClicked
import org.gjt.sp.jedit.{jEdit, View, Buffer, EditBus}
import org.gjt.sp.jedit.msg.ViewUpdate
import org.gjt.sp.jedit.buffer.JEditBuffer
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, StructureMatcher, Selection}
import org.gjt.sp.jedit.syntax.TokenMarker
import org.gjt.sp.jedit.indent.IndentRule
import org.gjt.sp.jedit.gui.{DockableWindowManager, CompleteWord}
import org.jedit.options.CombinedOptions
object Isabelle {
/* editor modes */
val modes =
List(
"isabelle", // theory source
"isabelle-ml", // ML source
"isabelle-news", // NEWS
"isabelle-options", // etc/options
"isabelle-output", // pretty text area output
"isabelle-root", // session ROOT
"sml") // Standard ML (not Isabelle/ML)
private val ml_syntax: Outer_Syntax =
Outer_Syntax.empty.no_tokens.
set_language_context(Completion.Language_Context.ML_outer)
private val sml_syntax: Outer_Syntax =
Outer_Syntax.empty.no_tokens.
set_language_context(Completion.Language_Context.SML_outer)
private val news_syntax: Outer_Syntax =
Outer_Syntax.empty.no_tokens
def mode_syntax(mode: String): Option[Outer_Syntax] =
mode match {
case "isabelle" => Some(PIDE.resources.session_base.overall_syntax)
case "isabelle-options" => Some(Options.options_syntax)
case "isabelle-root" => Some(Sessions.root_syntax)
case "isabelle-ml" => Some(ml_syntax)
case "isabelle-news" => Some(news_syntax)
case "isabelle-output" => None
case "sml" => Some(sml_syntax)
case _ => None
}
def buffer_syntax(buffer: JEditBuffer): Option[Outer_Syntax] =
if (buffer == null) None
else
(JEdit_Lib.buffer_mode(buffer), Document_Model.get(buffer)) match {
case ("isabelle", Some(model)) =>
Some(PIDE.session.recent_syntax(model.node_name))
case (mode, _) => mode_syntax(mode)
}
/* token markers */
private val mode_markers: Map[String, TokenMarker] =
Map(modes.map(mode => (mode, new Token_Markup.Marker(mode, None))): _*) +
("bibtex" -> new JEdit_Bibtex.Token_Marker)
def mode_token_marker(mode: String): Option[TokenMarker] = mode_markers.get(mode)
def buffer_token_marker(buffer: Buffer): Option[TokenMarker] = {
val mode = JEdit_Lib.buffer_mode(buffer)
if (mode == "isabelle") Some(new Token_Markup.Marker(mode, Some(buffer)))
else mode_token_marker(mode)
}
/* text structure */
def indent_rule(mode: String): Option[IndentRule] =
mode match {
case "isabelle" | "isabelle-options" | "isabelle-root" =>
Some(Text_Structure.Indent_Rule)
case _ => None
}
def structure_matchers(mode: String): List[StructureMatcher] =
if (mode == "isabelle") List(Text_Structure.Matcher) else Nil
/* dockable windows */
private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
def debugger_dockable(view: View): Option[Debugger_Dockable] =
wm(view).getDockableWindow("isabelle-debugger") match {
case dockable: Debugger_Dockable => Some(dockable)
case _ => None
}
+ def document_dockable(view: View): Option[Document_Dockable] =
+ wm(view).getDockableWindow("isabelle-document") match {
+ case dockable: Document_Dockable => Some(dockable)
+ case _ => None
+ }
+
def documentation_dockable(view: View): Option[Documentation_Dockable] =
wm(view).getDockableWindow("isabelle-documentation") match {
case dockable: Documentation_Dockable => Some(dockable)
case _ => None
}
def monitor_dockable(view: View): Option[Monitor_Dockable] =
wm(view).getDockableWindow("isabelle-monitor") match {
case dockable: Monitor_Dockable => Some(dockable)
case _ => None
}
def output_dockable(view: View): Option[Output_Dockable] =
wm(view).getDockableWindow("isabelle-output") match {
case dockable: Output_Dockable => Some(dockable)
case _ => None
}
def protocol_dockable(view: View): Option[Protocol_Dockable] =
wm(view).getDockableWindow("isabelle-protocol") match {
case dockable: Protocol_Dockable => Some(dockable)
case _ => None
}
def query_dockable(view: View): Option[Query_Dockable] =
wm(view).getDockableWindow("isabelle-query") match {
case dockable: Query_Dockable => Some(dockable)
case _ => None
}
def raw_output_dockable(view: View): Option[Raw_Output_Dockable] =
wm(view).getDockableWindow("isabelle-raw-output") match {
case dockable: Raw_Output_Dockable => Some(dockable)
case _ => None
}
def simplifier_trace_dockable(view: View): Option[Simplifier_Trace_Dockable] =
wm(view).getDockableWindow("isabelle-simplifier-trace") match {
case dockable: Simplifier_Trace_Dockable => Some(dockable)
case _ => None
}
def sledgehammer_dockable(view: View): Option[Sledgehammer_Dockable] =
wm(view).getDockableWindow("isabelle-sledgehammer") match {
case dockable: Sledgehammer_Dockable => Some(dockable)
case _ => None
}
def state_dockable(view: View): Option[State_Dockable] =
wm(view).getDockableWindow("isabelle-state") match {
case dockable: State_Dockable => Some(dockable)
case _ => None
}
def symbols_dockable(view: View): Option[Symbols_Dockable] =
wm(view).getDockableWindow("isabelle-symbols") match {
case dockable: Symbols_Dockable => Some(dockable)
case _ => None
}
def syslog_dockable(view: View): Option[Syslog_Dockable] =
wm(view).getDockableWindow("isabelle-syslog") match {
case dockable: Syslog_Dockable => Some(dockable)
case _ => None
}
def theories_dockable(view: View): Option[Theories_Dockable] =
wm(view).getDockableWindow("isabelle-theories") match {
case dockable: Theories_Dockable => Some(dockable)
case _ => None
}
def timing_dockable(view: View): Option[Timing_Dockable] =
wm(view).getDockableWindow("isabelle-timing") match {
case dockable: Timing_Dockable => Some(dockable)
case _ => None
}
/* continuous checking */
private val CONTINUOUS_CHECKING = "editor_continuous_checking"
def continuous_checking: Boolean = PIDE.options.bool(CONTINUOUS_CHECKING)
def continuous_checking_=(b: Boolean): Unit =
GUI_Thread.require {
if (continuous_checking != b) {
PIDE.options.bool(CONTINUOUS_CHECKING) = b
PIDE.session.update_options(PIDE.options.value)
PIDE.plugin.deps_changed()
}
}
def set_continuous_checking(): Unit = { continuous_checking = true }
def reset_continuous_checking(): Unit = { continuous_checking = false }
def toggle_continuous_checking(): Unit = { continuous_checking = !continuous_checking }
class Continuous_Checking extends CheckBox("Continuous checking") {
tooltip = "Continuous checking of proof document (visible and required parts)"
reactions += { case ButtonClicked(_) => continuous_checking = selected }
def load(): Unit = { selected = continuous_checking }
load()
}
/* update state */
def update_state(view: View): Unit =
state_dockable(view).foreach(_.update_request())
/* required document nodes */
def set_node_required(view: View): Unit = Document_Model.view_node_required(view, set = true)
def reset_node_required(view: View): Unit = Document_Model.view_node_required(view, set = false)
def toggle_node_required(view: View): Unit = Document_Model.view_node_required(view, toggle = true)
/* full screen */
// see toggleFullScreen() method in jEdit/org/gjt/sp/jedit/View.java
def toggle_full_screen(view: View): Unit = {
if (PIDE.options.bool("jedit_toggle_full_screen") ||
Untyped.get[Boolean](view, "fullScreenMode")) view.toggleFullScreen()
else {
Untyped.set[Boolean](view, "fullScreenMode", true)
val screen = GUI.screen_size(view)
view.dispose()
view.updateFullScreenProps()
Untyped.set[Rectangle](view, "windowedBounds", view.getBounds)
view.setUndecorated(true)
view.setBounds(screen.full_screen_bounds)
view.validate()
view.setVisible(true)
view.toFront()
view.closeAllMenus()
view.getEditPane.getTextArea.requestFocus()
EditBus.send(new ViewUpdate(view, ViewUpdate.FULL_SCREEN_TOGGLED))
}
}
/* font size */
def reset_font_size(): Unit =
Font_Info.main_change.reset(PIDE.options.int("jedit_reset_font_size").toFloat)
def increase_font_size(): Unit = Font_Info.main_change.step(1)
def decrease_font_size(): Unit = Font_Info.main_change.step(-1)
/* structured edits */
def indent_enabled(buffer: JEditBuffer, option: String): Boolean =
indent_rule(JEdit_Lib.buffer_mode(buffer)).isDefined &&
buffer.getStringProperty("autoIndent") == "full" &&
PIDE.options.bool(option)
def indent_input(text_area: TextArea): Unit = {
val buffer = text_area.getBuffer
val line = text_area.getCaretLine
val caret = text_area.getCaretPosition
if (text_area.isEditable && indent_enabled(buffer, "jedit_indent_input")) {
buffer_syntax(buffer) match {
case Some(syntax) =>
val nav = new Text_Structure.Navigator(syntax, buffer, true)
nav.iterator(line, 1).nextOption() match {
case Some(Text.Info(range, tok))
if range.stop == caret && syntax.keywords.is_indent_command(tok) =>
buffer.indentLine(line, true)
case _ =>
}
case None =>
}
}
}
def newline(text_area: TextArea): Unit = {
if (!text_area.isEditable()) text_area.getToolkit().beep()
else {
val buffer = text_area.getBuffer
val line = text_area.getCaretLine
val caret = text_area.getCaretPosition
def nl: Unit = text_area.userInput('\n')
if (indent_enabled(buffer, "jedit_indent_newline")) {
buffer_syntax(buffer) match {
case Some(syntax) =>
val keywords = syntax.keywords
val (toks1, toks2) = Text_Structure.split_line_content(buffer, keywords, line, caret)
if (toks1.isEmpty) buffer.removeTrailingWhiteSpace(Array(line))
else if (keywords.is_indent_command(toks1.head)) buffer.indentLine(line, true)
if (toks2.isEmpty || keywords.is_indent_command(toks2.head)) {
text_area.setSelectedText("\n")
if (!buffer.indentLine(line + 1, true)) text_area.goToStartOfWhiteSpace(false)
}
else nl
case None => nl
}
}
else nl
}
}
def insert_line_padding(text_area: JEditTextArea, text: String): Unit = {
val buffer = text_area.getBuffer
JEdit_Lib.buffer_edit(buffer) {
val text1 =
if (text_area.getSelectionCount == 0) {
def pad(range: Text.Range): String =
if (JEdit_Lib.get_text(buffer, range) == Some("\n")) "" else "\n"
val caret = JEdit_Lib.caret_range(text_area)
val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1)
pad(before_caret) + text + pad(caret)
}
else text
text_area.setSelectedText(text1)
}
}
def edit_command(
snapshot: Document.Snapshot,
text_area: TextArea,
padding: Boolean,
id: Document_ID.Generic,
text: String
): Unit = {
val buffer = text_area.getBuffer
if (!snapshot.is_outdated && text != "") {
(snapshot.find_command(id), Document_Model.get(buffer)) match {
case (Some((node, command)), Some(model)) if command.node_name == model.node_name =>
node.command_start(command) match {
case Some(start) =>
JEdit_Lib.buffer_edit(buffer) {
val range = command.core_range + start
JEdit_Lib.buffer_edit(buffer) {
if (padding) {
text_area.moveCaretPosition(start + range.length)
val start_line = text_area.getCaretLine + 1
text_area.setSelectedText("\n" + text)
val end_line = text_area.getCaretLine
for (line <- start_line to end_line) {
Token_Markup.Line_Context.refresh(buffer, line)
buffer.indentLine(line, true)
}
}
else {
buffer.remove(start, range.length)
text_area.moveCaretPosition(start)
text_area.setSelectedText(text)
}
}
}
case None =>
}
case _ =>
}
}
}
/* formal entities */
def goto_entity(view: View): Unit = {
val text_area = view.getTextArea
for {
doc_view <- Document_View.get(text_area)
rendering = doc_view.get_rendering()
caret_range = JEdit_Lib.caret_range(text_area)
link <- rendering.hyperlink_entity(caret_range)
} link.info.follow(view)
}
def select_entity(text_area: JEditTextArea): Unit = {
for (doc_view <- Document_View.get(text_area)) {
val rendering = doc_view.get_rendering()
val caret_range = JEdit_Lib.caret_range(text_area)
val buffer_range = JEdit_Lib.buffer_range(text_area.getBuffer)
val active_focus = rendering.caret_focus_ranges(caret_range, buffer_range)
if (active_focus.nonEmpty) {
text_area.selectNone()
for (r <- active_focus)
text_area.addToSelection(new Selection.Range(r.start, r.stop))
}
}
}
/* completion */
def complete(view: View, word_only: Boolean): Unit =
Completion_Popup.Text_Area.action(view.getTextArea, word_only)
/* control styles */
def control_sub(text_area: JEditTextArea): Unit =
Syntax_Style.edit_control_style(text_area, Symbol.sub)
def control_sup(text_area: JEditTextArea): Unit =
Syntax_Style.edit_control_style(text_area, Symbol.sup)
def control_bold(text_area: JEditTextArea): Unit =
Syntax_Style.edit_control_style(text_area, Symbol.bold)
def control_emph(text_area: JEditTextArea): Unit =
Syntax_Style.edit_control_style(text_area, Symbol.emph)
def control_reset(text_area: JEditTextArea): Unit =
Syntax_Style.edit_control_style(text_area, "")
/* block styles */
private def enclose_input(text_area: JEditTextArea, s1: String, s2: String): Unit = {
s1.foreach(text_area.userInput)
s2.foreach(text_area.userInput)
s2.foreach(_ => text_area.goToPrevCharacter(false))
}
def input_bsub(text_area: JEditTextArea): Unit =
enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded)
def input_bsup(text_area: JEditTextArea): Unit =
enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded)
/* antiquoted cartouche */
def antiquoted_cartouche(text_area: TextArea): Unit = {
val buffer = text_area.getBuffer
for {
doc_view <- Document_View.get(text_area)
rendering = doc_view.get_rendering()
caret_range = JEdit_Lib.caret_range(text_area)
antiq_range <- rendering.antiquoted(caret_range)
antiq_text <- JEdit_Lib.get_text(buffer, antiq_range)
body_text <- Antiquote.read_antiq_body(antiq_text)
(name, arg) <- Token.read_antiq_arg(Keyword.Keywords.empty, body_text)
if Symbol.is_ascii_identifier(name)
} {
val op_text =
Isabelle_Encoding.perhaps_decode(buffer,
Symbol.control_prefix + name + Symbol.control_suffix)
val arg_text =
if (arg.isEmpty) ""
else if (Isabelle_Encoding.is_active(buffer)) Symbol.cartouche_decoded(arg.get)
else Symbol.cartouche(arg.get)
buffer.remove(antiq_range.start, antiq_range.length)
text_area.moveCaretPosition(antiq_range.start)
text_area.selectNone
text_area.setSelectedText(op_text + arg_text)
}
}
/* spell-checker dictionary */
def update_dictionary(text_area: JEditTextArea, include: Boolean, permanent: Boolean): Unit = {
for {
spell_checker <- PIDE.plugin.spell_checker.get
doc_view <- Document_View.get(text_area)
rendering = doc_view.get_rendering()
range = JEdit_Lib.caret_range(text_area)
Text.Info(_, word) <- Spell_Checker.current_word(rendering, range)
} {
spell_checker.update(word, include, permanent)
JEdit_Lib.jedit_views().foreach(_.repaint())
}
}
def reset_dictionary(): Unit = {
for (spell_checker <- PIDE.plugin.spell_checker.get) {
spell_checker.reset()
JEdit_Lib.jedit_views().foreach(_.repaint())
}
}
/* debugger */
def toggle_breakpoint(text_area: JEditTextArea): Unit = {
GUI_Thread.require {}
if (PIDE.session.debugger.is_active()) {
Debugger_Dockable.get_breakpoint(text_area, text_area.getCaretPosition) match {
case Some((command, breakpoint)) =>
PIDE.session.debugger.toggle_breakpoint(command, breakpoint)
jEdit.propertiesChanged()
case None =>
}
}
}
/* plugin options */
def plugin_options(frame: Frame): Unit = {
GUI_Thread.require {}
jEdit.setProperty("Plugin Options.last", "isabelle-general")
new CombinedOptions(frame, 1)
}
/* popups */
def dismissed_popups(view: View): Boolean = {
var dismissed = false
JEdit_Lib.jedit_text_areas(view).foreach(text_area =>
if (Completion_Popup.Text_Area.dismissed(text_area)) dismissed = true)
if (Pretty_Tooltip.dismissed_all()) dismissed = true
dismissed
}
/* tooltips */
def show_tooltip(view: View, control: Boolean): Unit = {
GUI_Thread.require {}
val text_area = view.getTextArea
val painter = text_area.getPainter
val caret_range = JEdit_Lib.caret_range(text_area)
for {
doc_view <- Document_View.get(text_area)
rendering = doc_view.get_rendering()
tip <- rendering.tooltip(caret_range, control)
loc0 <- Option(text_area.offsetToXY(caret_range.start))
} {
val loc = new Point(loc0.x, loc0.y + painter.getLineHeight * 3 / 4)
val results = rendering.snapshot.command_results(tip.range)
Pretty_Tooltip(view, painter, loc, rendering, results, tip)
}
}
/* error navigation */
private def goto_error(
view: View,
range: Text.Range,
avoid_range: Text.Range = Text.Range.offside,
which: String = "")(
get: List[Text.Markup] => Option[Text.Markup]
): Unit = {
GUI_Thread.require {}
val text_area = view.getTextArea
for (doc_view <- Document_View.get(text_area)) {
val rendering = doc_view.get_rendering()
val errs = rendering.errors(range).filterNot(_.range.overlaps(avoid_range))
get(errs) match {
case Some(err) =>
PIDE.editor.goto_buffer(false, view, view.getBuffer, err.range.start)
case None =>
view.getStatus.setMessageAndClear("No " + which + "error in current document snapshot")
}
}
}
def goto_first_error(view: View): Unit =
goto_error(view, JEdit_Lib.buffer_range(view.getBuffer))(_.headOption)
def goto_last_error(view: View): Unit =
goto_error(view, JEdit_Lib.buffer_range(view.getBuffer))(_.lastOption)
def goto_prev_error(view: View): Unit = {
val caret_range = JEdit_Lib.caret_range(view.getTextArea)
val range = Text.Range(0, caret_range.stop)
goto_error(view, range, avoid_range = caret_range, which = "previous ")(_.lastOption)
}
def goto_next_error(view: View): Unit = {
val caret_range = JEdit_Lib.caret_range(view.getTextArea)
val range = Text.Range(caret_range.start, view.getBuffer.getLength)
goto_error(view, range, avoid_range = caret_range, which = "next ")(_.headOption)
}
/* java monitor */
def java_monitor(view: View): Unit =
Java_Monitor.java_monitor_external(view, look_and_feel = GUI.current_laf)
}