--- a/src/Tools/jEdit/src/token_markup.scala Wed Mar 15 13:35:14 2017 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala Wed Mar 15 13:49:39 2017 +0100
@@ -9,65 +9,19 @@
import isabelle._
-import java.awt.{Font, Color}
-import java.awt.font.TextAttribute
-import java.awt.geom.AffineTransform
import javax.swing.text.Segment
import scala.collection.convert.WrapAsJava
-import org.gjt.sp.util.SyntaxUtilities
-import org.gjt.sp.jedit.{jEdit, Mode, Buffer}
+import org.gjt.sp.jedit.{Mode, Buffer}
import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, DummyTokenHandler,
- ParserRuleSet, ModeProvider, XModeHandler, SyntaxStyle}
+ ParserRuleSet, ModeProvider, XModeHandler}
import org.gjt.sp.jedit.indent.IndentRule
-import org.gjt.sp.jedit.textarea.{TextArea, Selection}
import org.gjt.sp.jedit.buffer.JEditBuffer
object Token_Markup
{
- /* editing support for control symbols */
-
- def edit_control_style(text_area: TextArea, control: String)
- {
- GUI_Thread.assert {}
-
- val buffer = text_area.getBuffer
-
- val control_decoded = Isabelle_Encoding.maybe_decode(buffer, control)
-
- def update_style(text: String): String =
- {
- val result = new StringBuilder
- for (sym <- Symbol.iterator(text) if !HTML.control.isDefinedAt(sym)) {
- if (Symbol.is_controllable(sym)) result ++= control_decoded
- result ++= sym
- }
- result.toString
- }
-
- text_area.getSelection.foreach(sel => {
- val before = JEdit_Lib.point_range(buffer, sel.getStart - 1)
- JEdit_Lib.try_get_text(buffer, before) match {
- case Some(s) if HTML.control.isDefinedAt(s) =>
- text_area.extendSelection(before.start, before.stop)
- case _ =>
- }
- })
-
- text_area.getSelection.toList match {
- case Nil =>
- text_area.setSelectedText(control_decoded)
- case sels =>
- JEdit_Lib.buffer_edit(buffer) {
- sels.foreach(sel =>
- text_area.setSelectedText(sel, update_style(text_area.getSelectedText(sel))))
- }
- }
- }
-
-
/* line context */
object Line_Context