--- 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"
--- 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 */
--- 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 =>
- }
- }
- }
-}
-
--- /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 =>
+ }
+ }
+ }
+}
--- 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))))
}