diff --git a/src/Tools/jEdit/etc/options b/src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options +++ b/src/Tools/jEdit/etc/options @@ -1,164 +1,167 @@ (* :mode=isabelle-options: *) public option jedit_logic : string = "" -- "default logic session" public option jedit_print_mode : string = "" -- "default print modes for output, separated by commas (change requires restart)" public option jedit_auto_resolve : bool = false -- "automatically resolve auxiliary files within the document model" public option jedit_reset_font_size : int = 18 -- "reset main text font size" public option jedit_font_scale : real = 1.0 -- "scale factor of add-on panels wrt. main text font" public option jedit_popup_font_scale : real = 0.85 -- "scale factor of popups wrt. main text font" public option jedit_popup_bounds : real = 0.5 -- "relative bounds of popup window wrt. logical screen size" public option jedit_tooltip_delay : real = 0.75 -- "open/close delay for document tooltips (seconds)" public option jedit_tooltip_margin : int = 60 -- "margin for tooltip pretty-printing" public option jedit_structure_limit : int = 1000 -- "maximum number of lines to scan for language structure" public option jedit_symbols_search_limit : int = 50 -- "maximum number of symbols in search result" public option jedit_timing_threshold : real = 0.1 -- "default threshold for timing display (seconds)" public option jedit_text_overview : bool = true -- "paint text overview column" public option jedit_focus_modifier : string = "CS" -- "keyboard modifier to enable entity focus regardless of def visibility" +public option jedit_toggle_full_screen : bool = false + -- "use original jEdit action toggle-full-screen instead of Isabelle/jEdit variant" + public option isabelle_fonts_hinted : bool = true -- "use hinted Isabelle DejaVu fonts (change requires restart)" section "Indentation" public option jedit_indent_input : bool = true -- "indentation of Isabelle keywords after input (typed character or completion)" public option jedit_indent_newline : bool = true -- "indentation of Isabelle keywords on ENTER (action isabelle.newline)" public option jedit_indent_script : bool = true -- "indent unstructured proof script ('apply' etc.) via number of subgoals" public option jedit_indent_script_limit : int = 20 -- "maximum indentation of unstructured proof script ('apply' etc.)" section "Completion" public option jedit_completion : bool = true -- "enable completion popup" public option jedit_completion_select_enter : bool = false -- "select completion item via ENTER" public option jedit_completion_select_tab : bool = true -- "select completion item via TAB" public option jedit_completion_context : bool = true -- "use semantic language context for completion" public option jedit_completion_delay : real = 0.5 -- "delay for completion popup (seconds)" public option jedit_completion_immediate : bool = true -- "insert uniquely completed abbreviation immediately into buffer" section "Rendering of Document Content" option outdated_color : string = "EEE3E3FF" option unprocessed_color : string = "FFA0A0FF" option unprocessed1_color : string = "FFA0A032" option running_color : string = "610061FF" option running1_color : string = "61006164" option bullet_color : string = "000000FF" option tooltip_color : string = "FFFFE9FF" option writeln_color : string = "C0C0C0FF" option information_color : string = "C1DFEEFF" option warning_color : string = "FF8C00FF" option legacy_color : string = "FF8C00FF" option error_color : string = "B22222FF" option writeln_message_color : string = "F0F0F0FF" option information_message_color : string = "DCEAF3FF" option tracing_message_color : string = "F0F8FFFF" option warning_message_color : string = "EEE8AAFF" option legacy_message_color : string = "EEE8AAFF" option error_message_color : string = "FFC1C1FF" option spell_checker_color : string = "0000FFFF" option bad_color : string = "FF6A6A64" option canceled_color : string = "FF6A6A64" option intensify_color : string = "FFCC6664" option entity_color : string = "CCD9FF80" option entity_ref_color : string = "800080FF" option breakpoint_disabled_color : string = "CCCC0080" option breakpoint_enabled_color : string = "FF9966FF" option quoted_color : string = "8B8B8B19" option antiquoted_color : string = "FFC83219" option antiquote_color : string = "6600CCFF" option raw_text_color : string = "6600CCFF" option plain_text_color : string = "CC6600FF" option highlight_color : string = "50505032" option hyperlink_color : string = "000000FF" option active_color : string = "DCDCDCFF" option active_hover_color : string = "9DC75DFF" option active_result_color : string = "999966FF" option keyword1_color : string = "006699FF" option keyword2_color : string = "009966FF" option keyword3_color : string = "0099FFFF" option quasi_keyword_color : string = "9966FFFF" option improper_color : string = "FF5050FF" option operator_color : string = "323232FF" option comment1_color : string = "CC0000FF" option comment2_color : string = "FF8400FF" option comment3_color : string = "6600CCFF" option caret_debugger_color : string = "FF9966FF" option caret_invisible_color : string = "50000080" option completion_color : string = "0000FFFF" option search_color : string = "66FFFF64" option tfree_color : string = "A020F0FF" option tvar_color : string = "A020F0FF" option free_color : string = "0000FFFF" option skolem_color : string = "D2691EFF" option bound_color : string = "008000FF" option var_color : string = "00009BFF" option inner_numeral_color : string = "FF0000FF" option inner_quoted_color : string = "FF00CCFF" option inner_cartouche_color : string = "CC6600FF" option dynamic_color : string = "7BA428FF" option class_parameter_color : string = "D2691EFF" option markdown_bullet1_color : string = "DAFEDAFF" option markdown_bullet2_color : string = "FFF0CCFF" option markdown_bullet3_color : string = "E7E7FFFF" option markdown_bullet4_color : string = "FFE0F0FF" section "Icons" option tooltip_close_icon : string = "idea-icons/actions/closeHovered.png" option tooltip_detach_icon : string = "idea-icons/actions/nextfile.png" option gutter_information_icon : string = "idea-icons/general/balloonInformation.png" option gutter_warning_icon : string = "idea-icons/runConfigurations/testFailed.png" option gutter_legacy_icon : string = "idea-icons/general/balloonWarning.png" option gutter_error_icon : string = "idea-icons/runConfigurations/testError.png" option process_passive_icon : string = "idea-icons/process/step_passive.png" option process_active_icons : string = "idea-icons/process/step_1.png:idea-icons/process/step_2.png:idea-icons/process/step_3.png:idea-icons/process/step_4.png:idea-icons/process/step_5.png:idea-icons/process/step_6.png:idea-icons/process/step_7.png:idea-icons/process/step_8.png:idea-icons/process/step_9.png:idea-icons/process/step_10.png:idea-icons/process/step_11.png:idea-icons/process/step_12.png" diff --git a/src/Tools/jEdit/src/actions.xml b/src/Tools/jEdit/src/actions.xml --- a/src/Tools/jEdit/src/actions.xml +++ b/src/Tools/jEdit/src/actions.xml @@ -1,230 +1,230 @@ isabelle.jedit.Isabelle.set_continuous_checking(); isabelle.jedit.Isabelle.reset_continuous_checking(); isabelle.jedit.Isabelle.toggle_continuous_checking(); isabelle.jedit.Isabelle.set_node_required(view); isabelle.jedit.Isabelle.reset_node_required(view); isabelle.jedit.Isabelle.toggle_node_required(view); isabelle.jedit.Isabelle.update_state(view); isabelle.jedit.Isabelle.reset_font_size(); isabelle.jedit.Isabelle.increase_font_size(); isabelle.jedit.Isabelle.increase_font_size(); isabelle.jedit.Isabelle.decrease_font_size(); isabelle.jedit.Isabelle.decrease_font_size(); isabelle.jedit.Isabelle.newline(textArea); - + isabelle.jedit.Isabelle.toggle_full_screen(view); isabelle.jedit.Isabelle.goto_entity(view); isabelle.jedit.Isabelle.select_entity(textArea); isabelle.jedit.Isabelle.complete(view, false); isabelle.jedit.Isabelle.show_tooltip(view, true); isabelle.jedit.Isabelle.show_tooltip(view, false); isabelle.jedit.Isabelle.goto_first_error(view); isabelle.jedit.Isabelle.goto_last_error(view); isabelle.jedit.Isabelle.goto_prev_error(view); isabelle.jedit.Isabelle.goto_next_error(view); isabelle.jedit.Isabelle.complete(view, true); isabelle.jedit.Isabelle.control_sub(textArea); isabelle.jedit.Isabelle.control_sup(textArea); isabelle.jedit.Isabelle.control_bold(textArea); isabelle.jedit.Isabelle.control_emph(textArea); isabelle.jedit.Isabelle.control_reset(textArea); isabelle.jedit.Isabelle.input_bsub(textArea); isabelle.jedit.Isabelle.input_bsup(textArea); isabelle.jedit.Isabelle.antiquoted_cartouche(textArea); isabelle.jedit.Isabelle.update_dictionary(textArea, true, false); isabelle.jedit.Isabelle.update_dictionary(textArea, true, true); isabelle.jedit.Isabelle.update_dictionary(textArea, false, false); isabelle.jedit.Isabelle.update_dictionary(textArea, false, true); isabelle.jedit.Isabelle.reset_dictionary(); isabelle.jedit.Isabelle.toggle_breakpoint(textArea); isabelle.jedit.Isabelle.plugin_options(view); isabelle.jedit.Document_Model.open_preview(view, false); isabelle.jedit.Document_Model.open_preview(view, true); isabelle.jedit.Isabelle_Export.open_browser(view); isabelle.jedit.Isabelle_Session.open_browser(view); isabelle.jedit.Keymap_Merge.check_dialog(view); isabelle.jedit.Isabelle.java_monitor(view); 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,622 +1,623 @@ /* 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 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) } } def set_continuous_checking() { continuous_checking = true } def reset_continuous_checking() { continuous_checking = false } def toggle_continuous_checking() { 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() { 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) { Document_Model.view_node_required(view, set = true) } def reset_node_required(view: View) { Document_Model.view_node_required(view, set = false) } def toggle_node_required(view: View) { 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) { - if (Untyped.get[Boolean](view, "fullScreenMode")) view.toggleFullScreen() + 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() { Font_Info.main_change.reset(PIDE.options.int("jedit_reset_font_size").toFloat) } def increase_font_size() { Font_Info.main_change.step(1) } def decrease_font_size() { 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) { 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).toStream.headOption 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) { 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 { 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) { 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) { 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 buffer.indentLines(start_line, end_line) } else { buffer.remove(start, range.length) text_area.moveCaretPosition(start) text_area.setSelectedText(text) } } } case None => } case _ => } } } /* formal entities */ def goto_entity(view: View) { 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) { 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) { Completion_Popup.Text_Area.action(view.getTextArea, word_only) } /* control styles */ def control_sub(text_area: JEditTextArea) { Syntax_Style.edit_control_style(text_area, Symbol.sub) } def control_sup(text_area: JEditTextArea) { Syntax_Style.edit_control_style(text_area, Symbol.sup) } def control_bold(text_area: JEditTextArea) { Syntax_Style.edit_control_style(text_area, Symbol.bold) } def control_emph(text_area: JEditTextArea) { Syntax_Style.edit_control_style(text_area, Symbol.emph) } def control_reset(text_area: JEditTextArea) { Syntax_Style.edit_control_style(text_area, "") } /* block styles */ private def enclose_input(text_area: JEditTextArea, s1: String, s2: String) { s1.foreach(text_area.userInput) s2.foreach(text_area.userInput) s2.foreach(_ => text_area.goToPrevCharacter(false)) } def input_bsub(text_area: JEditTextArea) { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) } def input_bsup(text_area: JEditTextArea) { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) } /* antiquoted cartouche */ def antiquoted_cartouche(text_area: TextArea) { 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) { 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() { 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) { 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) { 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]) { 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) { 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) { 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()) } diff --git a/src/Tools/jEdit/src/jEdit.props b/src/Tools/jEdit/src/jEdit.props --- a/src/Tools/jEdit/src/jEdit.props +++ b/src/Tools/jEdit/src/jEdit.props @@ -1,349 +1,347 @@ #jEdit properties autoReloadDialog=false buffer.deepIndent=false buffer.encoding=UTF-8-Isabelle buffer.indentSize=2 buffer.lineSeparator=\n buffer.maxLineLen=100 buffer.noTabs=true buffer.sidekick.keystroke-parse=false buffer.tabSize=2 buffer.undoCount=1000 close-docking-area.shortcut2=C+e C+CIRCUMFLEX complete-word.shortcut= console.dock-position=floating console.encoding=UTF-8 console.font=Isabelle DejaVu Sans Mono 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 encodingDetectors=BOM XML-PI buffer-local-property end.shortcut= expand-abbrev.shortcut2=CA+SPACE expand-folds.shortcut= fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII firstTime=false focus-buffer-switcher.shortcut2=A+CIRCUMFLEX foldPainter=Circle gatchan.highlight.overview=false helpviewer.font=Isabelle DejaVu Serif helpviewer.fontsize=12 home.shortcut= insert-newline-indent.shortcut= insert-newline.shortcut= isabelle-debugger.dock-position=floating isabelle-documentation.dock-position=left isabelle-export-browser.label=Browse theory exports isabelle-output.dock-position=bottom isabelle-output.height=174 isabelle-output.width=412 isabelle-query.dock-position=bottom isabelle-session-browser.label=Browse session information isabelle-simplifier-trace.dock-position=floating isabelle-sledgehammer.dock-position=bottom isabelle-state.dock-position=right isabelle-symbols.dock-position=bottom isabelle-theories.dock-position=right isabelle.antiquoted_cartouche.label=Make antiquoted cartouche isabelle.complete-word.label=Complete word isabelle.complete.label=Complete Isabelle text isabelle.complete.shortcut2=C+b isabelle.control-bold.label=Control bold isabelle.control-bold.shortcut=C+e RIGHT isabelle.control-emph.label=Control emphasized isabelle.control-emph.shortcut=C+e LEFT isabelle.control-reset.label=Control reset isabelle.control-reset.shortcut=C+e BACK_SPACE isabelle.control-sub.label=Control subscript isabelle.control-sub.shortcut=C+e DOWN isabelle.control-sup.label=Control superscript isabelle.control-sup.shortcut=C+e UP isabelle.decrease-font-size.label=Decrease font size isabelle.decrease-font-size.shortcut2=C+SUBTRACT isabelle.decrease-font-size.shortcut=C+MINUS isabelle.decrease-font-size2.label=Decrease font size (clone) isabelle.draft.label=Show draft in browser isabelle.exclude-word-permanently.label=Exclude word permanently isabelle.exclude-word.label=Exclude word isabelle.first-error.label=Go to first error isabelle.first-error.shortcut=CS+a isabelle.goto-entity.label=Go to definition of formal entity at caret isabelle.goto-entity.shortcut=CS+d isabelle.include-word-permanently.label=Include word permanently isabelle.include-word.label=Include word isabelle.increase-font-size.label=Increase font size isabelle.increase-font-size.shortcut2=C+ADD isabelle.increase-font-size.shortcut=C+PLUS isabelle.increase-font-size2.label=Increase font size (clone) isabelle.increase-font-size2.shortcut=C+EQUALS isabelle.java-monitor.label=Java/VM monitor isabelle.last-error.label=Go to last error isabelle.last-error.shortcut=CS+z isabelle.message.label=Show message isabelle.message.shortcut=CS+m isabelle.newline.label=Newline with indentation of Isabelle keywords isabelle.newline.shortcut=ENTER isabelle.next-error.label=Go to next error isabelle.next-error.shortcut=CS+n isabelle.options.label=Isabelle options isabelle.prev-error.label=Go to previous error isabelle.prev-error.shortcut=CS+p isabelle.preview.label=Show preview in browser isabelle.reset-continuous-checking.label=Reset continuous checking isabelle.reset-font-size.label=Reset font size isabelle.reset-node-required.label=Reset node required isabelle.reset-words.label=Reset non-permanent words isabelle.select-entity.label=Select all occurences of formal entity at caret isabelle.select-entity.shortcut=CS+ENTER isabelle.set-continuous-checking.label=Set continuous checking isabelle.set-node-required.label=Set node required isabelle.toggle-breakpoint.label=Toggle Breakpoint isabelle.toggle-continuous-checking.label=Toggle continuous checking isabelle.toggle-continuous-checking.shortcut=C+e ENTER -isabelle.toggle-full-screen.label=Toggle full-screen mode -isabelle.toggle-full-screen.shortcut=F11 -isabelle.toggle-full-screen.shortcut2=S+F11 isabelle.toggle-node-required.label=Toggle node required isabelle.toggle-node-required.shortcut=C+e SPACE isabelle.tooltip.label=Show tooltip isabelle.tooltip.shortcut=CS+b isabelle.update-state.label=Update state output isabelle.update-state.shortcut=S+ENTER lang.usedefaultlocale=false largefilemode=full line-end.shortcut=END line-home.shortcut=HOME logo.icon.medium=32x32/apps/isabelle.gif lookAndFeel=javax.swing.plaf.metal.MetalLookAndFeel match-bracket.shortcut2=C+9 metal.primary.font=Isabelle DejaVu Sans metal.primary.fontsize=12 metal.secondary.font=Isabelle DejaVu Sans metal.secondary.fontsize=12 navigator.showOnToolbar=true next-bracket.shortcut2=C+e C+9 new-file-in-mode.shortcut= options.shortcuts.deletekeymap.label=Delete options.shortcuts.duplicatekeymap.dialog.title=Keymap name options.shortcuts.duplicatekeymap.label=Duplicate options.shortcuts.resetkeymap.dialog.title=Reset keymap options.shortcuts.resetkeymap.label=Reset options.textarea.lineSpacing=1 plugin-blacklist.MacOSX.jar=true plugin.MacOSXPlugin.altDispatcher=false plugin.MacOSXPlugin.disableOption=true prev-bracket.shortcut2=C+e C+8 print.font=Isabelle DejaVu Sans Mono print.glyphVector=true recent-buffer.shortcut2=C+CIRCUMFLEX restore.remote=false restore=false search.subdirs.toggle=true select-block.shortcut2=C+8 sidekick-tree.dock-position=right sidekick.auto-complete-popup-get-focus=true sidekick.buffer-save-parse=true sidekick.complete-delay=0 sidekick.complete-instant.toggle=false sidekick.complete-popup.accept-characters=\\t sidekick.complete-popup.insert-characters= sidekick.persistentFilter=true sidekick.showFilter=true sidekick.splitter.location=721 systrayicon=false tip.show=false +toggle-full-screen.shortcut2=S+F11 toggle-multi-select.shortcut2=C+NUMBER_SIGN toggle-rect-select.shortcut2=A+NUMBER_SIGN twoStageSave=false vfs.browser.dock-position=left vfs.favorite.0.type=1 vfs.favorite.0=$ISABELLE_HOME vfs.favorite.1.type=1 vfs.favorite.1=$ISABELLE_HOME_USER vfs.favorite.2.type=1 vfs.favorite.2=$JEDIT_HOME vfs.favorite.3.type=1 vfs.favorite.3=$JEDIT_SETTINGS vfs.favorite.4.type=1 vfs.favorite.4=isabelle-export: vfs.favorite.5.type=1 vfs.favorite.5=isabelle-session: view.antiAlias=subpixel HRGB view.blockCaret=true view.caretBlink=false view.docking.framework=PIDE view.eolMarkers=false view.extendedState=0 view.font=Isabelle DejaVu Sans Mono view.fontsize=18 view.fracFontMetrics=false view.gutter.font=Isabelle DejaVu Sans Mono view.gutter.fontsize=12 view.gutter.lineNumbers=false view.gutter.selectionAreaWidth=18 view.height=850 view.middleMousePaste=true view.showToolbar=true view.status.memory.background=#666699 view.status=( mode , fold , encoding ) locked wrap multiSelect rectSelect overwrite lineSep buffersets task-monitor java-status ml-status errors clock view.thickCaret=true view.width=1200 xml-insert-closing-tag.shortcut=