diff --git a/src/Pure/Isar/line_structure.scala b/src/Pure/Isar/line_structure.scala --- a/src/Pure/Isar/line_structure.scala +++ b/src/Pure/Isar/line_structure.scala @@ -1,70 +1,70 @@ /* Title: Pure/Isar/line_structure.scala Author: Makarius Line-oriented document structure, e.g. for fold handling. */ package isabelle object Line_Structure { val init: Line_Structure = Line_Structure() } sealed case class Line_Structure( improper: Boolean = true, blank: Boolean = true, command: Boolean = false, depth: Int = 0, span_depth: Int = 0, after_span_depth: Int = 0, element_depth: Int = 0) { def update(keywords: Keyword.Keywords, tokens: List[Token]): Line_Structure = { val improper1 = tokens.forall(tok => !tok.is_proper) val blank1 = tokens.forall(_.is_space) val command1 = tokens.exists(_.is_begin_or_command) val command_depth = - tokens.iterator.filter(_.is_proper).toStream.headOption match { + tokens.iterator.filter(_.is_proper).nextOption() match { case Some(tok) => if (keywords.is_command(tok, Keyword.close_structure)) Some(after_span_depth - 1) else None case None => None } val depth1 = if (tokens.exists(tok => keywords.is_before_command(tok) || !tok.is_end && keywords.is_command(tok, Keyword.theory))) element_depth else if (command_depth.isDefined) command_depth.get else if (command1) after_span_depth else span_depth val (span_depth1, after_span_depth1, element_depth1) = ((span_depth, after_span_depth, element_depth) /: tokens) { case (depths @ (x, y, z), tok) => if (tok.is_begin) (z + 2, z + 1, z + 1) else if (tok.is_end) (z + 1, z - 1, z - 1) else if (tok.is_command) { val depth0 = element_depth if (keywords.is_command(tok, Keyword.theory_goal)) (depth0 + 2, depth0 + 1, z) else if (keywords.is_command(tok, Keyword.theory)) (depth0 + 1, depth0, z) else if (keywords.is_command(tok, Keyword.proof_open)) (y + 2, y + 1, z) else if (keywords.is_command(tok, Set(Keyword.PRF_BLOCK))) (y + 2, y + 1, z) else if (keywords.is_command(tok, Set(Keyword.QED_BLOCK))) (y - 1, y - 2, z) else if (keywords.is_command(tok, Set(Keyword.PRF_CLOSE))) (y, y - 1, z) else if (keywords.is_command(tok, Keyword.proof_close)) (y + 1, y - 1, z) else if (keywords.is_command(tok, Keyword.qed_global)) (depth0 + 1, depth0, z) else depths } else depths } Line_Structure( improper1, blank1, command1, depth1, span_depth1, after_span_depth1, element_depth1) } } 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,620 +1,620 @@ /* 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(): 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).toStream.headOption match { + 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 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): 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()) } diff --git a/src/Tools/jEdit/src/text_structure.scala b/src/Tools/jEdit/src/text_structure.scala --- a/src/Tools/jEdit/src/text_structure.scala +++ b/src/Tools/jEdit/src/text_structure.scala @@ -1,354 +1,354 @@ /* Title: Tools/jEdit/src/text_structure.scala Author: Makarius Text structure based on Isabelle/Isar outer syntax. */ package isabelle.jedit import isabelle._ import org.gjt.sp.jedit.indent.{IndentRule, IndentAction} import org.gjt.sp.jedit.textarea.{TextArea, StructureMatcher, Selection} import org.gjt.sp.jedit.buffer.JEditBuffer import org.gjt.sp.jedit.Buffer object Text_Structure { /* token navigator */ class Navigator(syntax: Outer_Syntax, buffer: JEditBuffer, comments: Boolean) { val limit: Int = PIDE.options.value.int("jedit_structure_limit") max 0 def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] = { val it = Token_Markup.line_token_iterator(syntax, buffer, line, line + lim) if (comments) it.filterNot(_.info.is_space) else it.filter(_.info.is_proper) } def reverse_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] = { val it = Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim) if (comments) it.filterNot(_.info.is_space) else it.filter(_.info.is_proper) } } /* indentation */ object Indent_Rule extends IndentRule { private val keyword_open = Keyword.theory_goal ++ Keyword.proof_open private val keyword_close = Keyword.proof_close def apply(buffer: JEditBuffer, current_line: Int, prev_line0: Int, prev_prev_line0: Int, actions: java.util.List[IndentAction]): Unit = { Isabelle.buffer_syntax(buffer) match { case Some(syntax) => val keywords = syntax.keywords val nav = new Navigator(syntax, buffer, true) val indent_size = buffer.getIndentSize def line_indent(line: Int): Int = if (line < 0 || line >= buffer.getLineCount) 0 else buffer.getCurrentIndentForLine(line, null) def line_head(line: Int): Option[Text.Info[Token]] = - nav.iterator(line, 1).toStream.headOption + nav.iterator(line, 1).nextOption() def head_is_quasi_command(line: Int): Boolean = line_head(line) match { case None => false case Some(Text.Info(_, tok)) => keywords.is_quasi_command(tok) } val prev_line: Int = Range.inclusive(current_line - 1, 0, -1).find(line => Token_Markup.Line_Context.before(buffer, line).get_context == Scan.Finished && (!Token_Markup.Line_Context.after(buffer, line).structure.improper || Token_Markup.Line_Context.after(buffer, line).structure.blank)) getOrElse -1 def prev_line_command: Option[Token] = nav.reverse_iterator(prev_line, 1). collectFirst({ case Text.Info(_, tok) if tok.is_begin_or_command => tok }) def prev_line_span: Iterator[Token] = nav.reverse_iterator(prev_line, 1).map(_.info).takeWhile(tok => !tok.is_begin_or_command) def prev_span: Iterator[Token] = nav.reverse_iterator(prev_line).map(_.info).takeWhile(tok => !tok.is_begin_or_command) val script_indent: Text.Info[Token] => Int = { val opt_rendering: Option[JEdit_Rendering] = if (PIDE.options.value.bool("jedit_indent_script")) GUI_Thread.now { (for { text_area <- JEdit_Lib.jedit_text_areas(buffer) doc_view <- Document_View.get(text_area) - } yield doc_view.get_rendering).toStream.headOption + } yield doc_view.get_rendering).nextOption() } else None val limit = PIDE.options.value.int("jedit_indent_script_limit") (info: Text.Info[Token]) => opt_rendering match { case Some(rendering) if keywords.is_command(info.info, Keyword.prf_script) => (rendering.indentation(info.range) min limit) max 0 case _ => 0 } } def indent_indent(tok: Token): Int = if (keywords.is_command(tok, keyword_open)) indent_size else if (keywords.is_command(tok, keyword_close)) - indent_size else 0 def indent_offset(tok: Token): Int = if (keywords.is_command(tok, Keyword.proof_enclose)) indent_size else 0 def indent_structure: Int = nav.reverse_iterator(current_line - 1).scanLeft((0, false))( { case ((ind, _), Text.Info(range, tok)) => val ind1 = ind + indent_indent(tok) if (tok.is_begin_or_command && !keywords.is_command(tok, Keyword.prf_script)) { val line = buffer.getLineOfOffset(range.start) line_head(line) match { case Some(info) if info.info == tok => (ind1 + indent_offset(tok) + line_indent(line), true) case _ => (ind1, false) } } else (ind1, false) }).collectFirst({ case (i, true) => i }).getOrElse(0) def indent_brackets: Int = (0 /: prev_line_span)( { case (i, tok) => if (tok.is_open_bracket) i + indent_size else if (tok.is_close_bracket) i - indent_size else i }) def indent_extra: Int = if (prev_span.exists(keywords.is_quasi_command)) indent_size else 0 val indent = if (Token_Markup.Line_Context.before(buffer, current_line).get_context != Scan.Finished) line_indent(current_line) else if (Token_Markup.Line_Context.after(buffer, current_line).structure.blank) 0 else { line_head(current_line) match { case Some(info) => val tok = info.info if (tok.is_begin || keywords.is_before_command(tok) || keywords.is_command(tok, Keyword.theory)) 0 else if (keywords.is_command(tok, Keyword.proof_enclose)) indent_structure + script_indent(info) - indent_offset(tok) else if (keywords.is_command(tok, Keyword.proof)) (indent_structure + script_indent(info) - indent_offset(tok)) max indent_size else if (tok.is_command) indent_structure - indent_offset(tok) else { prev_line_command match { case None => val extra = (keywords.is_quasi_command(tok), head_is_quasi_command(prev_line)) match { case (true, true) | (false, false) => 0 case (true, false) => - indent_extra case (false, true) => indent_extra } line_indent(prev_line) + indent_brackets + extra - indent_offset(tok) case Some(prev_tok) => indent_structure + indent_brackets + indent_size - indent_offset(tok) - indent_offset(prev_tok) - indent_indent(prev_tok) } } case None => prev_line_command match { case None => val extra = if (head_is_quasi_command(prev_line)) indent_extra else 0 line_indent(prev_line) + indent_brackets + extra case Some(prev_tok) => indent_structure + indent_brackets + indent_size - indent_offset(prev_tok) - indent_indent(prev_tok) } } } actions.clear() actions.add(new IndentAction.AlignOffset(indent max 0)) case None => } } } def line_content(buffer: JEditBuffer, keywords: Keyword.Keywords, range: Text.Range, ctxt: Scan.Line_Context): (List[Token], Scan.Line_Context) = { val text = JEdit_Lib.get_text(buffer, range).getOrElse("") val (toks, ctxt1) = Token.explode_line(keywords, text, ctxt) val toks1 = toks.filterNot(_.is_space) (toks1, ctxt1) } def split_line_content(buffer: JEditBuffer, keywords: Keyword.Keywords, line: Int, caret: Int) : (List[Token], List[Token]) = { val line_range = JEdit_Lib.line_range(buffer, line) val ctxt0 = Token_Markup.Line_Context.before(buffer, line).get_context val (toks1, ctxt1) = line_content(buffer, keywords, Text.Range(line_range.start, caret), ctxt0) val (toks2, _) = line_content(buffer, keywords, Text.Range(caret, line_range.stop), ctxt1) (toks1, toks2) } /* structure matching */ object Matcher extends StructureMatcher { private def find_block( open: Token => Boolean, close: Token => Boolean, reset: Token => Boolean, restrict: Token => Boolean, it: Iterator[Text.Info[Token]]): Option[(Text.Range, Text.Range)] = { val range1 = it.next().range it.takeWhile(info => !info.info.is_command || restrict(info.info)). scanLeft((range1, 1))( { case ((r, d), Text.Info(range, tok)) => if (open(tok)) (range, d + 1) else if (close(tok)) (range, d - 1) else if (reset(tok)) (range, 0) else (r, d) } ).collectFirst({ case (range2, 0) => (range1, range2) }) } private def find_pair(text_area: TextArea): Option[(Text.Range, Text.Range)] = { val buffer = text_area.getBuffer val caret_line = text_area.getCaretLine val caret = text_area.getCaretPosition Isabelle.buffer_syntax(text_area.getBuffer) match { case Some(syntax) => val keywords = syntax.keywords val nav = new Navigator(syntax, buffer, false) def caret_iterator(): Iterator[Text.Info[Token]] = nav.iterator(caret_line).dropWhile(info => !info.range.touches(caret)) def reverse_caret_iterator(): Iterator[Text.Info[Token]] = nav.reverse_iterator(caret_line).dropWhile(info => !info.range.touches(caret)) nav.iterator(caret_line, 1).find(info => info.range.touches(caret)) match { case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.theory_goal) => find_block( keywords.is_command(_, Keyword.proof_goal), keywords.is_command(_, Keyword.qed), keywords.is_command(_, Keyword.qed_global), t => keywords.is_command(t, Keyword.diag) || keywords.is_command(t, Keyword.proof), caret_iterator()) case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.proof_goal) => find_block( keywords.is_command(_, Keyword.proof_goal), keywords.is_command(_, Keyword.qed), _ => false, t => keywords.is_command(t, Keyword.diag) || keywords.is_command(t, Keyword.proof), caret_iterator()) case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.qed_global) => reverse_caret_iterator().find(info => keywords.is_command(info.info, Keyword.theory)) match { case Some(Text.Info(range2, tok)) if keywords.is_command(tok, Keyword.theory_goal) => Some((range1, range2)) case _ => None } case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.qed) => find_block( keywords.is_command(_, Keyword.qed), t => keywords.is_command(t, Keyword.proof_goal) || keywords.is_command(t, Keyword.theory_goal), _ => false, t => keywords.is_command(t, Keyword.diag) || keywords.is_command(t, Keyword.proof) || keywords.is_command(t, Keyword.theory_goal), reverse_caret_iterator()) case Some(Text.Info(range1, tok)) if tok.is_begin => find_block(_.is_begin, _.is_end, _ => false, _ => true, caret_iterator()) case Some(Text.Info(range1, tok)) if tok.is_end => find_block(_.is_end, _.is_begin, _ => false, _ => true, reverse_caret_iterator()) match { case Some((_, range2)) => reverse_caret_iterator(). dropWhile(info => info.range != range2). dropWhile(info => info.range == range2). find(info => info.info.is_command || info.info.is_begin) match { case Some(Text.Info(range3, tok)) => if (keywords.is_command(tok, Keyword.theory_block)) Some((range1, range3)) else Some((range1, range2)) case None => None } case None => None } case _ => None } case None => None } } def getMatch(text_area: TextArea): StructureMatcher.Match = find_pair(text_area) match { case Some((_, range)) => val line = text_area.getBuffer.getLineOfOffset(range.start) new StructureMatcher.Match(Matcher, line, range.start, line, range.stop) case None => null } def selectMatch(text_area: TextArea): Unit = { def get_span(offset: Text.Offset): Option[Text.Range] = for { syntax <- Isabelle.buffer_syntax(text_area.getBuffer) span <- Token_Markup.command_span(syntax, text_area.getBuffer, offset) } yield span.range find_pair(text_area) match { case Some((r1, r2)) => (get_span(r1.start), get_span(r2.start)) match { case (Some(range1), Some(range2)) => val start = range1.start min range2.start val stop = range1.stop max range2.stop text_area.moveCaretPosition(stop, false) if (!text_area.isMultipleSelectionEnabled) text_area.selectNone text_area.addToSelection(new Selection.Range(start, stop)) case _ => } case None => } } } }