# HG changeset patch # User wenzelm # Date 1467917681 -7200 # Node ID 5cf8dd98a717a4227a47af0e922620954003fcb8 # Parent 3bf02e7fa8a390ca5de5a6d18c56b61251949c06 clarified modules; diff -r 3bf02e7fa8a3 -r 5cf8dd98a717 src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Thu Jul 07 12:08:00 2016 +0200 +++ b/src/Tools/jEdit/lib/Tools/jedit Thu Jul 07 20:54:41 2016 +0200 @@ -61,10 +61,10 @@ "src/sledgehammer_dockable.scala" "src/spell_checker.scala" "src/state_dockable.scala" - "src/structure_matching.scala" "src/symbols_dockable.scala" "src/syslog_dockable.scala" "src/text_overview.scala" + "src/text_structure.scala" "src/theories_dockable.scala" "src/timing_dockable.scala" "src/token_markup.scala" diff -r 3bf02e7fa8a3 -r 5cf8dd98a717 src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Thu Jul 07 12:08:00 2016 +0200 +++ b/src/Tools/jEdit/src/isabelle.scala Thu Jul 07 20:54:41 2016 +0200 @@ -84,19 +84,13 @@ } - /* indentation */ + /* text structure */ - def mode_indent_rule(mode: String): Option[IndentRule] = - mode match { - case "isabelle" => Some(Token_Markup.Indent_Rule) - case _ => None - } + def indent_rule(mode: String): Option[IndentRule] = + if (mode == "isabelle") Some(Text_Structure.Indent_Rule) else None - - /* structure matchers */ - - def structure_matchers(name: String): List[StructureMatcher] = - if (name == "isabelle") List(Structure_Matching.Isabelle_Matcher) else Nil + def structure_matchers(mode: String): List[StructureMatcher] = + if (mode == "isabelle") List(Text_Structure.Matcher) else Nil /* dockable windows */ diff -r 3bf02e7fa8a3 -r 5cf8dd98a717 src/Tools/jEdit/src/structure_matching.scala --- a/src/Tools/jEdit/src/structure_matching.scala Thu Jul 07 12:08:00 2016 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,167 +0,0 @@ -/* Title: Tools/jEdit/src/structure_matching.scala - Author: Makarius - -Structure matcher for Isabelle/Isar outer syntax. -*/ - -package isabelle.jedit - - -import isabelle._ - -import org.gjt.sp.jedit.textarea.{TextArea, StructureMatcher, Selection} - - -object Structure_Matching -{ - object Isabelle_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 limit = PIDE.options.value.int("jedit_structure_limit") max 0 - - def is_command_kind(token: Token, pred: String => Boolean): Boolean = - token.is_command_kind(syntax.keywords, pred) - - def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] = - Token_Markup.line_token_iterator(syntax, buffer, line, line + lim). - filter(_.info.is_proper) - - def rev_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] = - Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim). - filter(_.info.is_proper) - - def caret_iterator(): Iterator[Text.Info[Token]] = - iterator(caret_line).dropWhile(info => !info.range.touches(caret)) - - def rev_caret_iterator(): Iterator[Text.Info[Token]] = - rev_iterator(caret_line).dropWhile(info => !info.range.touches(caret)) - - iterator(caret_line, 1).find(info => info.range.touches(caret)) - match { - case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.theory_goal) => - find_block( - is_command_kind(_, Keyword.proof_goal), - is_command_kind(_, Keyword.qed), - is_command_kind(_, Keyword.qed_global), - t => - is_command_kind(t, Keyword.diag) || - is_command_kind(t, Keyword.proof), - caret_iterator()) - - case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.proof_goal) => - find_block( - is_command_kind(_, Keyword.proof_goal), - is_command_kind(_, Keyword.qed), - _ => false, - t => - is_command_kind(t, Keyword.diag) || - is_command_kind(t, Keyword.proof), - caret_iterator()) - - case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.qed_global) => - rev_caret_iterator().find(info => is_command_kind(info.info, Keyword.theory)) - match { - case Some(Text.Info(range2, tok)) - if is_command_kind(tok, Keyword.theory_goal) => Some((range1, range2)) - case _ => None - } - - case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.qed) => - find_block( - is_command_kind(_, Keyword.qed), - t => - is_command_kind(t, Keyword.proof_goal) || - is_command_kind(t, Keyword.theory_goal), - _ => false, - t => - is_command_kind(t, Keyword.diag) || - is_command_kind(t, Keyword.proof) || - is_command_kind(t, Keyword.theory_goal), - rev_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, rev_caret_iterator()) - match { - case Some((_, range2)) => - rev_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 (is_command_kind(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(Structure_Matching.Isabelle_Matcher, - line, range.start, line, range.stop) - case None => null - } - - def selectMatch(text_area: TextArea) - { - 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 => - } - } - } -} - diff -r 3bf02e7fa8a3 -r 5cf8dd98a717 src/Tools/jEdit/src/text_structure.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/text_structure.scala Thu Jul 07 20:54:41 2016 +0200 @@ -0,0 +1,184 @@ +/* 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 + + +object Text_Structure +{ + /* indentation */ + + object Indent_Rule extends IndentRule + { + def apply(buffer: JEditBuffer, this_line: Int, prev_line: Int, prev_prev_line: Int, + actions: java.util.List[IndentAction]) + { + val indent = 0 // FIXME + + actions.clear() + actions.add(new IndentAction.AlignOffset(indent)) + } + } + + + /* 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 limit = PIDE.options.value.int("jedit_structure_limit") max 0 + + def is_command_kind(token: Token, pred: String => Boolean): Boolean = + token.is_command_kind(syntax.keywords, pred) + + def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] = + Token_Markup.line_token_iterator(syntax, buffer, line, line + lim). + filter(_.info.is_proper) + + def rev_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] = + Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim). + filter(_.info.is_proper) + + def caret_iterator(): Iterator[Text.Info[Token]] = + iterator(caret_line).dropWhile(info => !info.range.touches(caret)) + + def rev_caret_iterator(): Iterator[Text.Info[Token]] = + rev_iterator(caret_line).dropWhile(info => !info.range.touches(caret)) + + iterator(caret_line, 1).find(info => info.range.touches(caret)) + match { + case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.theory_goal) => + find_block( + is_command_kind(_, Keyword.proof_goal), + is_command_kind(_, Keyword.qed), + is_command_kind(_, Keyword.qed_global), + t => + is_command_kind(t, Keyword.diag) || + is_command_kind(t, Keyword.proof), + caret_iterator()) + + case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.proof_goal) => + find_block( + is_command_kind(_, Keyword.proof_goal), + is_command_kind(_, Keyword.qed), + _ => false, + t => + is_command_kind(t, Keyword.diag) || + is_command_kind(t, Keyword.proof), + caret_iterator()) + + case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.qed_global) => + rev_caret_iterator().find(info => is_command_kind(info.info, Keyword.theory)) + match { + case Some(Text.Info(range2, tok)) + if is_command_kind(tok, Keyword.theory_goal) => Some((range1, range2)) + case _ => None + } + + case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.qed) => + find_block( + is_command_kind(_, Keyword.qed), + t => + is_command_kind(t, Keyword.proof_goal) || + is_command_kind(t, Keyword.theory_goal), + _ => false, + t => + is_command_kind(t, Keyword.diag) || + is_command_kind(t, Keyword.proof) || + is_command_kind(t, Keyword.theory_goal), + rev_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, rev_caret_iterator()) + match { + case Some((_, range2)) => + rev_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 (is_command_kind(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) + { + 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 => + } + } + } +} diff -r 3bf02e7fa8a3 -r 5cf8dd98a717 src/Tools/jEdit/src/token_markup.scala --- a/src/Tools/jEdit/src/token_markup.scala Thu Jul 07 12:08:00 2016 +0200 +++ b/src/Tools/jEdit/src/token_markup.scala Thu Jul 07 20:54:41 2016 +0200 @@ -20,7 +20,7 @@ import org.gjt.sp.jedit.{jEdit, Mode, Buffer} import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, DummyTokenHandler, ParserRuleSet, ModeProvider, XModeHandler, SyntaxStyle} -import org.gjt.sp.jedit.indent.{IndentRule, IndentAction} +import org.gjt.sp.jedit.indent.IndentRule import org.gjt.sp.jedit.textarea.{TextArea, Selection} import org.gjt.sp.jedit.buffer.JEditBuffer @@ -438,15 +438,6 @@ } - /* indentation */ - - object Indent_Rule extends IndentRule - { - def apply(buffer: JEditBuffer, this_line: Int, prev_line: Int, prev_prev_line: Int, - actions: java.util.List[IndentAction]): Unit = () - } - - /* mode provider */ class Mode_Provider(orig_provider: ModeProvider) extends ModeProvider @@ -457,7 +448,7 @@ { super.loadMode(mode, xmh) Isabelle.mode_token_marker(mode.getName).foreach(mode.setTokenMarker _) - Isabelle.mode_indent_rule(mode.getName).foreach(indent_rule => + Isabelle.indent_rule(mode.getName).foreach(indent_rule => Untyped.set[java.util.List[IndentRule]]( mode, "indentRules", WrapAsJava.seqAsJavaList(List(indent_rule)))) }