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) }